CBMC
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/exception_utils.h>
18 #include <util/message.h>
19 
21 
24  std::ostream &out,
25  const symbol_table_baset &symbol_table,
26  irep_serializationt &irepconverter)
27 {
28  write_gb_word(out, symbol_table.symbols.size());
29 
30  for(const auto &symbol_pair : symbol_table.symbols)
31  {
32  // Since version 2, symbols are not converted to ireps,
33  // instead they are saved in a custom binary format
34 
35  const symbolt &sym = symbol_pair.second;
36 
37  irepconverter.reference_convert(sym.type, out);
38  irepconverter.reference_convert(sym.value, out);
39  irepconverter.reference_convert(sym.location, out);
40 
41  irepconverter.write_string_ref(out, sym.name);
42  irepconverter.write_string_ref(out, sym.module);
43  irepconverter.write_string_ref(out, sym.base_name);
44  irepconverter.write_string_ref(out, sym.mode);
45  irepconverter.write_string_ref(out, sym.pretty_name);
46 
47  write_gb_word(out, 0); // old: sym.ordering
48 
49  unsigned flags=0;
50  flags = (flags << 1) | static_cast<int>(sym.is_weak);
51  flags = (flags << 1) | static_cast<int>(sym.is_type);
52  flags = (flags << 1) | static_cast<int>(sym.is_property);
53  flags = (flags << 1) | static_cast<int>(sym.is_macro);
54  flags = (flags << 1) | static_cast<int>(sym.is_exported);
55  flags = (flags << 1) | static_cast<int>(sym.is_input);
56  flags = (flags << 1) | static_cast<int>(sym.is_output);
57  flags = (flags << 1) | static_cast<int>(sym.is_state_var);
58  flags = (flags << 1) | static_cast<int>(sym.is_parameter);
59  flags = (flags << 1) | static_cast<int>(sym.is_auxiliary);
60  flags = (flags << 1) | static_cast<int>(false); // sym.binding;
61  flags = (flags << 1) | static_cast<int>(sym.is_lvalue);
62  flags = (flags << 1) | static_cast<int>(sym.is_static_lifetime);
63  flags = (flags << 1) | static_cast<int>(sym.is_thread_local);
64  flags = (flags << 1) | static_cast<int>(sym.is_file_local);
65  flags = (flags << 1) | static_cast<int>(sym.is_extern);
66  flags = (flags << 1) | static_cast<int>(sym.is_volatile);
67 
68  write_gb_word(out, flags);
69  }
70 }
71 
73  std::ostream &out,
74  irep_serializationt &irepconverter,
75  const std::pair<const irep_idt, goto_functiont> &fct)
76 {
77  write_gb_word(out, fct.second.body.instructions.size());
78 
79  for(const auto &instruction : fct.second.body.instructions)
80  {
81  irepconverter.reference_convert(instruction.code(), out);
82  irepconverter.reference_convert(instruction.source_location(), out);
83  write_gb_word(out, (long)instruction.type());
84 
85  const auto condition =
86  instruction.has_condition() ? instruction.condition() : true_exprt();
87  irepconverter.reference_convert(condition, out);
88 
89  write_gb_word(out, instruction.target_number);
90 
91  write_gb_word(out, instruction.targets.size());
92 
93  for(const auto &t_it : instruction.targets)
94  write_gb_word(out, t_it->target_number);
95 
96  write_gb_word(out, instruction.labels.size());
97 
98  for(const auto &l_it : instruction.labels)
99  irepconverter.write_string_ref(out, l_it);
100  }
101 }
102 
105  std::ostream &out,
106  const goto_functionst &goto_functions,
107  irep_serializationt &irepconverter)
108 {
109  unsigned cnt=0;
110  for(const auto &gf_entry : goto_functions.function_map)
111  {
112  if(gf_entry.second.body_available())
113  cnt++;
114  }
115 
116  write_gb_word(out, cnt);
117 
118  for(const auto &fct : goto_functions.function_map)
119  {
120  if(!fct.second.body_available())
121  continue;
122 
123  // Since version 2, goto functions are not converted to ireps,
124  // instead they are saved in a custom binary format
125 
126  const auto function_name = id2string(fct.first);
127  write_gb_string(out, function_name);
128  write_instructions_binary(out, irepconverter, fct);
129  }
130 }
131 
133 static void write_goto_binary(
134  std::ostream &out,
135  const symbol_table_baset &symbol_table,
136  const goto_functionst &goto_functions,
137  irep_serializationt &irepconverter)
138 {
139  write_symbol_table_binary(out, symbol_table, irepconverter);
140  write_goto_functions_binary(out, goto_functions, irepconverter);
141 }
142 
145  std::ostream &out,
146  const goto_modelt &goto_model,
147  int version)
148 {
149  return write_goto_binary(
150  out,
151  goto_model.symbol_table,
152  goto_model.goto_functions,
153  version);
154 }
155 
158  std::ostream &out,
159  const symbol_table_baset &symbol_table,
160  const goto_functionst &goto_functions,
161  int version)
162 {
163  // header
164  out << char(0x7f) << "GBF";
165  write_gb_word(out, version);
166 
168  irep_serializationt irepconverter(irepc);
169 
170  if(version < GOTO_BINARY_VERSION)
171  {
173  "version " + std::to_string(version) + " no longer supported",
174  "supported version = " + std::to_string(GOTO_BINARY_VERSION));
175  }
176  if(version > GOTO_BINARY_VERSION)
177  {
179  "unknown goto binary version " + std::to_string(version),
180  "supported version = " + std::to_string(GOTO_BINARY_VERSION));
181  }
182  write_goto_binary(out, symbol_table, goto_functions, irepconverter);
183  return false;
184 }
185 
188  const std::string &filename,
189  const goto_modelt &goto_model,
190  message_handlert &message_handler)
191 {
192  std::ofstream out(filename, std::ios::binary);
193 
194  if(!out)
195  {
196  messaget message(message_handler);
197  message.error() << "Failed to open '" << filename << "'";
198  return true;
199  }
200 
201  return write_goto_binary(out, goto_model);
202 }
A collection of goto functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
void write_string_ref(std::ostream &, const irep_idt &)
Output a string and maintain a reference to it.
const irept & reference_convert(std::istream &)
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & error() const
Definition: message.h:399
The symbol table base class interface.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_auxiliary
Definition: symbol.h:77
bool is_volatile
Definition: symbol.h:75
bool is_extern
Definition: symbol.h:74
bool is_macro
Definition: symbol.h:62
bool is_file_local
Definition: symbol.h:73
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
bool is_static_lifetime
Definition: symbol.h:70
bool is_property
Definition: symbol.h:67
bool is_parameter
Definition: symbol.h:76
bool is_thread_local
Definition: symbol.h:71
bool is_type
Definition: symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
bool is_state_var
Definition: symbol.h:66
bool is_output
Definition: symbol.h:65
typet type
Type of symbol.
Definition: symbol.h:31
bool is_weak
Definition: symbol.h:78
irep_idt name
The unique identifier.
Definition: symbol.h:40
bool is_exported
Definition: symbol.h:63
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
bool is_lvalue
Definition: symbol.h:72
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
bool is_input
Definition: symbol.h:64
The Boolean constant true.
Definition: std_expr.h:3055
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:40
void write_gb_string(std::ostream &out, const std::string &s)
outputs the string and then a zero byte.
void write_gb_word(std::ostream &out, std::size_t u)
Write 7 bits of u each time, least-significant byte first, until we have zero.
binary irep conversions with hashing
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:187
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
static void write_instructions_binary(std::ostream &out, irep_serializationt &irepconverter, const std::pair< const irep_idt, goto_functiont > &fct)
static void write_goto_functions_binary(std::ostream &out, const goto_functionst &goto_functions, irep_serializationt &irepconverter)
Writes the functions to file, but only those with non-empty body.
static void write_goto_binary(std::ostream &out, const symbol_table_baset &symbol_table, const goto_functionst &goto_functions, irep_serializationt &irepconverter)
Writes a goto program to disc, using goto binary format.
static void write_symbol_table_binary(std::ostream &out, const symbol_table_baset &symbol_table, irep_serializationt &irepconverter)
Writes the symbol table to file.
Write GOTO binaries.
#define GOTO_BINARY_VERSION