cprover
write_goto_binary.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Write GOTO binaries
4 
5 Author: CM Wintersteiger
6 
7 \*******************************************************************/
8 
11 
12 #include "write_goto_binary.h"
13 
14 #include <fstream>
15 
16 #include <util/message.h>
18 #include <util/symbol_table.h>
19 
22  std::ostream &out,
23  const symbol_tablet &lsymbol_table,
24  const goto_functionst &functions,
25  irep_serializationt &irepconverter)
26 {
27  // first write symbol table
28 
29  write_gb_word(out, lsymbol_table.symbols.size());
30 
31  forall_symbols(it, lsymbol_table.symbols)
32  {
33  // Since version 2, symbols are not converted to ireps,
34  // instead they are saved in a custom binary format
35 
36  const symbolt &sym = it->second;
37 
38  irepconverter.reference_convert(sym.type, out);
39  irepconverter.reference_convert(sym.value, out);
40  irepconverter.reference_convert(sym.location, out);
41 
42  irepconverter.write_string_ref(out, sym.name);
43  irepconverter.write_string_ref(out, sym.module);
44  irepconverter.write_string_ref(out, sym.base_name);
45  irepconverter.write_string_ref(out, sym.mode);
46  irepconverter.write_string_ref(out, sym.pretty_name);
47 
48  write_gb_word(out, 0); // old: sym.ordering
49 
50  unsigned flags=0;
51  flags = (flags << 1) | static_cast<int>(sym.is_weak);
52  flags = (flags << 1) | static_cast<int>(sym.is_type);
53  flags = (flags << 1) | static_cast<int>(sym.is_property);
54  flags = (flags << 1) | static_cast<int>(sym.is_macro);
55  flags = (flags << 1) | static_cast<int>(sym.is_exported);
56  flags = (flags << 1) | static_cast<int>(sym.is_input);
57  flags = (flags << 1) | static_cast<int>(sym.is_output);
58  flags = (flags << 1) | static_cast<int>(sym.is_state_var);
59  flags = (flags << 1) | static_cast<int>(sym.is_parameter);
60  flags = (flags << 1) | static_cast<int>(sym.is_auxiliary);
61  flags = (flags << 1) | static_cast<int>(false); // sym.binding;
62  flags = (flags << 1) | static_cast<int>(sym.is_lvalue);
63  flags = (flags << 1) | static_cast<int>(sym.is_static_lifetime);
64  flags = (flags << 1) | static_cast<int>(sym.is_thread_local);
65  flags = (flags << 1) | static_cast<int>(sym.is_file_local);
66  flags = (flags << 1) | static_cast<int>(sym.is_extern);
67  flags = (flags << 1) | static_cast<int>(sym.is_volatile);
68 
69  write_gb_word(out, flags);
70  }
71 
72  // now write functions, but only those with body
73 
74  unsigned cnt=0;
75  forall_goto_functions(it, functions)
76  if(it->second.body_available())
77  cnt++;
78 
79  write_gb_word(out, cnt);
80 
81  for(const auto &fct : functions.function_map)
82  {
83  if(fct.second.body_available())
84  {
85  // Since version 2, goto functions are not converted to ireps,
86  // instead they are saved in a custom binary format
87 
88  write_gb_string(out, id2string(fct.first)); // name
89  write_gb_word(out, fct.second.body.instructions.size()); // # instructions
90 
91  forall_goto_program_instructions(i_it, fct.second.body)
92  {
93  const goto_programt::instructiont &instruction = *i_it;
94 
95  irepconverter.reference_convert(instruction.code, out);
96  irepconverter.write_string_ref(out, instruction.function);
97  irepconverter.reference_convert(instruction.source_location, out);
98  write_gb_word(out, (long)instruction.type);
99  irepconverter.reference_convert(instruction.guard, out);
100  irepconverter.write_string_ref(out, irep_idt()); // former event
101  write_gb_word(out, instruction.target_number);
102 
103  write_gb_word(out, instruction.targets.size());
104 
105  for(const auto &t_it : instruction.targets)
106  write_gb_word(out, t_it->target_number);
107 
108  write_gb_word(out, instruction.labels.size());
109 
110  for(const auto &l_it : instruction.labels)
111  irepconverter.write_string_ref(out, l_it);
112  }
113  }
114  }
115 
116  // irepconverter.output_map(f);
117  // irepconverter.output_string_map(f);
118 
119  return false;
120 }
121 
124  std::ostream &out,
125  const symbol_tablet &lsymbol_table,
126  const goto_functionst &functions,
127  int version)
128 {
129  // header
130  out << char(0x7f) << "GBF";
131  write_gb_word(out, version);
132 
134  irep_serializationt irepconverter(irepc);
135 
136  switch(version)
137  {
138  case 1:
139  throw "version 1 no longer supported";
140 
141  case 2:
142  throw "version 2 no longer supported";
143 
144  case 3:
145  return write_goto_binary_v3(
146  out, lsymbol_table, functions,
147  irepconverter);
148 
149  default:
150  throw "unknown goto binary version";
151  }
152 
153  return false;
154 }
155 
158  const std::string &filename,
159  const symbol_tablet &symbol_table,
160  const goto_functionst &goto_functions,
161  message_handlert &message_handler)
162 {
163  std::ofstream out(filename, std::ios::binary);
164 
165  if(!out)
166  {
167  messaget message(message_handler);
168  message.error() <<
169  "Failed to open `" << filename << "'";
170  return true;
171  }
172 
173  return write_goto_binary(out, symbol_table, goto_functions);
174 }
irep_idt name
The unique identifier.
Definition: symbol.h:46
bool is_output
Definition: symbol.h:66
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_thread_local
Definition: symbol.h:70
#define forall_symbols(it, expr)
Definition: symbol_table.h:28
irep_idt mode
Language mode.
Definition: symbol.h:55
exprt value
Initial value of symbol.
Definition: symbol.h:40
void write_gb_word(std::ostream &out, std::size_t u)
outputs 4 characters for a long, most-significant byte first
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:49
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:58
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
bool is_static_lifetime
Definition: symbol.h:70
bool is_input
Definition: symbol.h:66
symbolst symbols
Definition: symbol_table.h:57
bool is_exported
Definition: symbol.h:66
bool is_parameter
Definition: symbol.h:71
The symbol table.
Definition: symbol_table.h:52
void reference_convert(std::istream &, irept &irep)
Symbol table.
void write_gb_string(std::ostream &out, const std::string &s)
outputs the string and then a zero byte.
binary irep conversions with hashing
bool is_volatile
Definition: symbol.h:71
bool is_extern
Definition: symbol.h:71
typet type
Type of symbol.
Definition: symbol.h:37
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:43
void write_string_ref(std::ostream &, const irep_idt &)
outputs the string reference
bool is_state_var
Definition: symbol.h:66
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
bool is_file_local
Definition: symbol.h:71
mstreamt & error()
Definition: message.h:223
bool is_weak
Definition: symbol.h:71
bool is_auxiliary
Definition: symbol.h:71
dstringt irep_idt
Definition: irep.h:32
bool write_goto_binary(std::ostream &out, const symbol_tablet &lsymbol_table, const goto_functionst &functions, int version)
Writes a goto program to disc.
bool is_type
Definition: symbol.h:66
bool is_property
Definition: symbol.h:66
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
Write GOTO binaries.
bool is_macro
Definition: symbol.h:66
bool write_goto_binary_v3(std::ostream &out, const symbol_tablet &lsymbol_table, const goto_functionst &functions, irep_serializationt &irepconverter)
Writes a goto program to disc, using goto binary format ver 2.
bool is_lvalue
Definition: symbol.h:71