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 
21 
24  std::ostream &out,
25  const symbol_tablet &symbol_table,
26  const goto_functionst &goto_functions,
27  irep_serializationt &irepconverter)
28 {
29  // first write symbol table
30 
31  write_gb_word(out, symbol_table.symbols.size());
32 
33  for(const auto &symbol_pair : symbol_table.symbols)
34  {
35  // Since version 2, symbols are not converted to ireps,
36  // instead they are saved in a custom binary format
37 
38  const symbolt &sym = symbol_pair.second;
39 
40  irepconverter.reference_convert(sym.type, out);
41  irepconverter.reference_convert(sym.value, out);
42  irepconverter.reference_convert(sym.location, out);
43 
44  irepconverter.write_string_ref(out, sym.name);
45  irepconverter.write_string_ref(out, sym.module);
46  irepconverter.write_string_ref(out, sym.base_name);
47  irepconverter.write_string_ref(out, sym.mode);
48  irepconverter.write_string_ref(out, sym.pretty_name);
49 
50  write_gb_word(out, 0); // old: sym.ordering
51 
52  unsigned flags=0;
53  flags = (flags << 1) | static_cast<int>(sym.is_weak);
54  flags = (flags << 1) | static_cast<int>(sym.is_type);
55  flags = (flags << 1) | static_cast<int>(sym.is_property);
56  flags = (flags << 1) | static_cast<int>(sym.is_macro);
57  flags = (flags << 1) | static_cast<int>(sym.is_exported);
58  flags = (flags << 1) | static_cast<int>(sym.is_input);
59  flags = (flags << 1) | static_cast<int>(sym.is_output);
60  flags = (flags << 1) | static_cast<int>(sym.is_state_var);
61  flags = (flags << 1) | static_cast<int>(sym.is_parameter);
62  flags = (flags << 1) | static_cast<int>(sym.is_auxiliary);
63  flags = (flags << 1) | static_cast<int>(false); // sym.binding;
64  flags = (flags << 1) | static_cast<int>(sym.is_lvalue);
65  flags = (flags << 1) | static_cast<int>(sym.is_static_lifetime);
66  flags = (flags << 1) | static_cast<int>(sym.is_thread_local);
67  flags = (flags << 1) | static_cast<int>(sym.is_file_local);
68  flags = (flags << 1) | static_cast<int>(sym.is_extern);
69  flags = (flags << 1) | static_cast<int>(sym.is_volatile);
70 
71  write_gb_word(out, flags);
72  }
73 
74  // now write functions, but only those with body
75 
76  unsigned cnt=0;
77  forall_goto_functions(it, goto_functions)
78  if(it->second.body_available())
79  cnt++;
80 
81  write_gb_word(out, cnt);
82 
83  for(const auto &fct : goto_functions.function_map)
84  {
85  if(fct.second.body_available())
86  {
87  // Since version 2, goto functions are not converted to ireps,
88  // instead they are saved in a custom binary format
89 
90  write_gb_string(out, id2string(fct.first)); // name
91  write_gb_word(out, fct.second.body.instructions.size()); // # instructions
92 
93  forall_goto_program_instructions(i_it, fct.second.body)
94  {
95  const goto_programt::instructiont &instruction = *i_it;
96 
97  irepconverter.reference_convert(instruction.code, out);
98  irepconverter.write_string_ref(out, instruction.function);
99  irepconverter.reference_convert(instruction.source_location, out);
100  write_gb_word(out, (long)instruction.type);
101  irepconverter.reference_convert(instruction.guard, out);
102  irepconverter.write_string_ref(out, irep_idt()); // former event
103  write_gb_word(out, instruction.target_number);
104 
105  write_gb_word(out, instruction.targets.size());
106 
107  for(const auto &t_it : instruction.targets)
108  write_gb_word(out, t_it->target_number);
109 
110  write_gb_word(out, instruction.labels.size());
111 
112  for(const auto &l_it : instruction.labels)
113  irepconverter.write_string_ref(out, l_it);
114  }
115  }
116  }
117 
118  // irepconverter.output_map(f);
119  // irepconverter.output_string_map(f);
120 
121  return false;
122 }
123 
126  std::ostream &out,
127  const goto_modelt &goto_model,
128  int version)
129 {
130  return write_goto_binary(
131  out,
132  goto_model.symbol_table,
133  goto_model.goto_functions,
134  version);
135 }
136 
139  std::ostream &out,
140  const symbol_tablet &symbol_table,
141  const goto_functionst &goto_functions,
142  int version)
143 {
144  // header
145  out << char(0x7f) << "GBF";
146  write_gb_word(out, version);
147 
149  irep_serializationt irepconverter(irepc);
150 
151  switch(version)
152  {
153  case 1:
154  throw "version 1 no longer supported";
155 
156  case 2:
157  throw "version 2 no longer supported";
158 
159  case 3:
160  return write_goto_binary_v3(
161  out, symbol_table, goto_functions, irepconverter);
162 
163  default:
164  throw "unknown goto binary version";
165  }
166 
167  return false;
168 }
169 
172  const std::string &filename,
173  const goto_modelt &goto_model,
175 {
176  std::ofstream out(filename, std::ios::binary);
177 
178  if(!out)
179  {
180  messaget message(message_handler);
181  message.error() <<
182  "Failed to open `" << filename << "'";
183  return true;
184  }
185 
186  return write_goto_binary(out, goto_model);
187 }
exprt guard
Guard for gotos, assume, assert.
Definition: goto_program.h:188
irep_idt function
The function this instruction belongs to.
Definition: goto_program.h:179
irep_idt name
The unique identifier.
Definition: symbol.h:43
bool is_output
Definition: symbol.h:63
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
bool is_thread_local
Definition: symbol.h:67
irep_idt mode
Language mode.
Definition: symbol.h:52
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:185
exprt value
Initial value of symbol.
Definition: symbol.h:37
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:46
function_mapt function_map
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:55
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
bool is_static_lifetime
Definition: symbol.h:67
bool is_input
Definition: symbol.h:63
targetst targets
The list of successor instructions.
Definition: goto_program.h:198
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
unsigned target_number
A number to identify branch targets.
Definition: goto_program.h:371
Symbol Table + CFG.
bool write_goto_binary(std::ostream &out, const goto_modelt &goto_model, int version)
Writes a goto program to disc.
bool is_exported
Definition: symbol.h:63
bool is_parameter
Definition: symbol.h:68
The symbol table.
Definition: symbol_table.h:19
mstreamt & error() const
Definition: message.h:302
void reference_convert(std::istream &, irept &irep)
Author: Diffblue Ltd.
const symbolst & symbols
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:68
bool is_extern
Definition: symbol.h:68
bool write_goto_binary_v3(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 2.
typet type
Type of symbol.
Definition: symbol.h:34
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
void write_string_ref(std::ostream &, const irep_idt &)
outputs the string reference
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:182
bool is_state_var
Definition: symbol.h:63
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
bool is_file_local
Definition: symbol.h:68
bool is_weak
Definition: symbol.h:68
bool is_auxiliary
Definition: symbol.h:68
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
dstringt irep_idt
Definition: irep.h:31
bool is_type
Definition: symbol.h:63
bool is_property
Definition: symbol.h:63
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:735
Write GOTO binaries.
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
bool is_macro
Definition: symbol.h:63
bool is_lvalue
Definition: symbol.h:68