CBMC
Loading...
Searching...
No Matches
write_goto_binary.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Write GOTO binaries
4
5Author: CM Wintersteiger
6
7\*******************************************************************/
8
11
12#include "write_goto_binary.h"
13
14#include <fstream>
15
18#include <util/message.h>
19
21
24 std::ostream &out,
25 const symbol_table_baset &symbol_table,
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,
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,
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);
129 }
130}
131
134 std::ostream &out,
135 const symbol_table_baset &symbol_table,
136 const goto_functionst &goto_functions,
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
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}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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 ...
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
mstreamt & error() const
Definition message.h:391
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
The Boolean constant true.
Definition std_expr.h:3190
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
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 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