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/exception_utils.h>
17 #include <util/invariant.h>
19 #include <util/message.h>
20 #include <util/symbol_table.h>
21 
23 
26  std::ostream &out,
27  const symbol_tablet &symbol_table,
28  const goto_functionst &goto_functions,
29  irep_serializationt &irepconverter)
30 {
31  // first write symbol table
32 
33  write_gb_word(out, symbol_table.symbols.size());
34 
35  for(const auto &symbol_pair : symbol_table.symbols)
36  {
37  // Since version 2, symbols are not converted to ireps,
38  // instead they are saved in a custom binary format
39 
40  const symbolt &sym = symbol_pair.second;
41 
42  irepconverter.reference_convert(sym.type, out);
43  irepconverter.reference_convert(sym.value, out);
44  irepconverter.reference_convert(sym.location, out);
45 
46  irepconverter.write_string_ref(out, sym.name);
47  irepconverter.write_string_ref(out, sym.module);
48  irepconverter.write_string_ref(out, sym.base_name);
49  irepconverter.write_string_ref(out, sym.mode);
50  irepconverter.write_string_ref(out, sym.pretty_name);
51 
52  write_gb_word(out, 0); // old: sym.ordering
53 
54  unsigned flags=0;
55  flags = (flags << 1) | static_cast<int>(sym.is_weak);
56  flags = (flags << 1) | static_cast<int>(sym.is_type);
57  flags = (flags << 1) | static_cast<int>(sym.is_property);
58  flags = (flags << 1) | static_cast<int>(sym.is_macro);
59  flags = (flags << 1) | static_cast<int>(sym.is_exported);
60  flags = (flags << 1) | static_cast<int>(sym.is_input);
61  flags = (flags << 1) | static_cast<int>(sym.is_output);
62  flags = (flags << 1) | static_cast<int>(sym.is_state_var);
63  flags = (flags << 1) | static_cast<int>(sym.is_parameter);
64  flags = (flags << 1) | static_cast<int>(sym.is_auxiliary);
65  flags = (flags << 1) | static_cast<int>(false); // sym.binding;
66  flags = (flags << 1) | static_cast<int>(sym.is_lvalue);
67  flags = (flags << 1) | static_cast<int>(sym.is_static_lifetime);
68  flags = (flags << 1) | static_cast<int>(sym.is_thread_local);
69  flags = (flags << 1) | static_cast<int>(sym.is_file_local);
70  flags = (flags << 1) | static_cast<int>(sym.is_extern);
71  flags = (flags << 1) | static_cast<int>(sym.is_volatile);
72 
73  write_gb_word(out, flags);
74  }
75 
76  // now write functions, but only those with body
77 
78  unsigned cnt=0;
79  forall_goto_functions(it, goto_functions)
80  if(it->second.body_available())
81  cnt++;
82 
83  write_gb_word(out, cnt);
84 
85  for(const auto &fct : goto_functions.function_map)
86  {
87  if(fct.second.body_available())
88  {
89  // Since version 2, goto functions are not converted to ireps,
90  // instead they are saved in a custom binary format
91 
92  write_gb_string(out, id2string(fct.first)); // name
93  write_gb_word(out, fct.second.body.instructions.size()); // # instructions
94 
95  forall_goto_program_instructions(i_it, fct.second.body)
96  {
97  const goto_programt::instructiont &instruction = *i_it;
98 
99  irepconverter.reference_convert(instruction.code, out);
100  irepconverter.write_string_ref(out, instruction.function);
101  irepconverter.reference_convert(instruction.source_location, out);
102  write_gb_word(out, (long)instruction.type);
103  irepconverter.reference_convert(instruction.guard, out);
104  irepconverter.write_string_ref(out, irep_idt()); // former event
105  write_gb_word(out, instruction.target_number);
106 
107  write_gb_word(out, instruction.targets.size());
108 
109  for(const auto &t_it : instruction.targets)
110  write_gb_word(out, t_it->target_number);
111 
112  write_gb_word(out, instruction.labels.size());
113 
114  for(const auto &l_it : instruction.labels)
115  irepconverter.write_string_ref(out, l_it);
116  }
117  }
118  }
119 
120  // irepconverter.output_map(f);
121  // irepconverter.output_string_map(f);
122 
123  return false;
124 }
125 
128  std::ostream &out,
129  const goto_modelt &goto_model,
130  int version)
131 {
132  return write_goto_binary(
133  out,
134  goto_model.symbol_table,
135  goto_model.goto_functions,
136  version);
137 }
138 
141  std::ostream &out,
142  const symbol_tablet &symbol_table,
143  const goto_functionst &goto_functions,
144  int version)
145 {
146  // header
147  out << char(0x7f) << "GBF";
148  write_gb_word(out, version);
149 
151  irep_serializationt irepconverter(irepc);
152 
153  const int current_goto_version = 4;
154  if(version < current_goto_version)
156  "version " + std::to_string(version) + " no longer supported",
157  "supported version = " + std::to_string(current_goto_version));
158  else if(version > current_goto_version)
160  "unknown goto binary version " + std::to_string(version),
161  "supported version = " + std::to_string(current_goto_version));
162  else
163  return write_goto_binary_v4(
164  out, symbol_table, goto_functions, irepconverter);
165 }
166 
169  const std::string &filename,
170  const goto_modelt &goto_model,
171  message_handlert &message_handler)
172 {
173  std::ofstream out(filename, std::ios::binary);
174 
175  if(!out)
176  {
177  messaget message(message_handler);
178  message.error() <<
179  "Failed to open `" << filename << "'";
180  return true;
181  }
182 
183  return write_goto_binary(out, goto_model);
184 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
exception_utils.h
symbolt::is_state_var
bool is_state_var
Definition: symbol.h:61
irep_serialization.h
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
goto_programt::instructiont::source_location
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:187
irep_serializationt::reference_convert
void reference_convert(std::istream &, irept &irep)
Definition: irep_serialization.cpp:51
symbolt::is_macro
bool is_macro
Definition: symbol.h:61
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
goto_programt::instructiont::type
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:190
symbolt::is_input
bool is_input
Definition: symbol.h:61
goto_model.h
goto_modelt
Definition: goto_model.h:24
irep_serializationt::ireps_containert
Definition: irep_serialization.h:31
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
invariant.h
irep_idt
dstringt irep_idt
Definition: irep.h:32
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:53
goto_programt::instructiont::targets
targetst targets
The list of successor instructions.
Definition: goto_program.h:203
write_goto_binary_v4
bool write_goto_binary_v4(std::ostream &out, const symbol_tablet &symbol_table, const goto_functionst &goto_functions, irep_serializationt &irepconverter)
Writes a goto program to disc, using goto binary format ver 4.
Definition: write_goto_binary.cpp:25
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
write_goto_binary.h
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
symbolt::is_thread_local
bool is_thread_local
Definition: symbol.h:65
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
messaget::error
mstreamt & error() const
Definition: message.h:386
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
goto_programt::instructiont::code
codet code
Definition: goto_program.h:181
write_gb_string
void write_gb_string(std::ostream &out, const std::string &s)
outputs the string and then a zero byte.
Definition: irep_serialization.cpp:180
goto_programt::instructiont::labels
labelst labels
Definition: goto_program.h:228
write_gb_word
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.
Definition: irep_serialization.cpp:132
symbolt::is_exported
bool is_exported
Definition: symbol.h:61
symbolt::is_parameter
bool is_parameter
Definition: symbol.h:66
message_handlert
Definition: message.h:24
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
goto_programt::instructiont::target_number
unsigned target_number
A number to identify branch targets.
Definition: goto_program.h:376
symbolt::is_output
bool is_output
Definition: symbol.h:61
symbolt::is_extern
bool is_extern
Definition: symbol.h:66
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
goto_programt::instructiont::function
irep_idt function
The function this instruction belongs to.
Definition: goto_program.h:184
symbolt::is_volatile
bool is_volatile
Definition: symbol.h:66
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
symbolt
Symbol table entry.
Definition: symbol.h:27
symbol_table_baset::symbols
const symbolst & symbols
Definition: symbol_table_base.h:27
symbolt::is_type
bool is_type
Definition: symbol.h:61
goto_programt::instructiont::guard
exprt guard
Guard for gotos, assume, assert.
Definition: goto_program.h:193
symbolt::is_auxiliary
bool is_auxiliary
Definition: symbol.h:66
binary
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:224
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:149
symbolt::is_file_local
bool is_file_local
Definition: symbol.h:66
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
write_goto_binary
bool write_goto_binary(std::ostream &out, const goto_modelt &goto_model, int version)
Writes a goto program to disc.
Definition: write_goto_binary.cpp:127
symbol_table.h
Author: Diffblue Ltd.
message.h
symbolt::module
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
invalid_command_line_argument_exceptiont
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition: exception_utils.h:37
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
irep_serializationt
Definition: irep_serialization.h:28
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
symbolt::is_weak
bool is_weak
Definition: symbol.h:66
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
symbolt::is_property
bool is_property
Definition: symbol.h:61
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:804
irep_serializationt::write_string_ref
void write_string_ref(std::ostream &, const irep_idt &)
Output a string and maintain a reference to it.
Definition: irep_serialization.cpp:221