cprover
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#include <util/symbol_table.h>
20
22
25 std::ostream &out,
26 const symbol_tablet &symbol_table,
27 const goto_functionst &goto_functions,
28 irep_serializationt &irepconverter)
29{
30 // first write symbol table
31
32 write_gb_word(out, symbol_table.symbols.size());
33
34 for(const auto &symbol_pair : symbol_table.symbols)
35 {
36 // Since version 2, symbols are not converted to ireps,
37 // instead they are saved in a custom binary format
38
39 const symbolt &sym = symbol_pair.second;
40
41 irepconverter.reference_convert(sym.type, out);
42 irepconverter.reference_convert(sym.value, out);
43 irepconverter.reference_convert(sym.location, out);
44
45 irepconverter.write_string_ref(out, sym.name);
46 irepconverter.write_string_ref(out, sym.module);
47 irepconverter.write_string_ref(out, sym.base_name);
48 irepconverter.write_string_ref(out, sym.mode);
49 irepconverter.write_string_ref(out, sym.pretty_name);
50
51 write_gb_word(out, 0); // old: sym.ordering
52
53 unsigned flags=0;
54 flags = (flags << 1) | static_cast<int>(sym.is_weak);
55 flags = (flags << 1) | static_cast<int>(sym.is_type);
56 flags = (flags << 1) | static_cast<int>(sym.is_property);
57 flags = (flags << 1) | static_cast<int>(sym.is_macro);
58 flags = (flags << 1) | static_cast<int>(sym.is_exported);
59 flags = (flags << 1) | static_cast<int>(sym.is_input);
60 flags = (flags << 1) | static_cast<int>(sym.is_output);
61 flags = (flags << 1) | static_cast<int>(sym.is_state_var);
62 flags = (flags << 1) | static_cast<int>(sym.is_parameter);
63 flags = (flags << 1) | static_cast<int>(sym.is_auxiliary);
64 flags = (flags << 1) | static_cast<int>(false); // sym.binding;
65 flags = (flags << 1) | static_cast<int>(sym.is_lvalue);
66 flags = (flags << 1) | static_cast<int>(sym.is_static_lifetime);
67 flags = (flags << 1) | static_cast<int>(sym.is_thread_local);
68 flags = (flags << 1) | static_cast<int>(sym.is_file_local);
69 flags = (flags << 1) | static_cast<int>(sym.is_extern);
70 flags = (flags << 1) | static_cast<int>(sym.is_volatile);
71
72 write_gb_word(out, flags);
73 }
74
75 // now write functions, but only those with body
76
77 unsigned cnt=0;
78 for(const auto &gf_entry : goto_functions.function_map)
79 {
80 if(gf_entry.second.body_available())
81 cnt++;
82 }
83
84 write_gb_word(out, cnt);
85
86 for(const auto &fct : goto_functions.function_map)
87 {
88 if(fct.second.body_available())
89 {
90 // Since version 2, goto functions are not converted to ireps,
91 // instead they are saved in a custom binary format
92
93 write_gb_string(out, id2string(fct.first)); // name
94 write_gb_word(out, fct.second.body.instructions.size()); // # instructions
95
96 for(const auto &instruction : fct.second.body.instructions)
97 {
98 irepconverter.reference_convert(instruction.get_code(), out);
99 irepconverter.reference_convert(instruction.source_location(), out);
100 write_gb_word(out, (long)instruction.type());
101
102 const auto condition =
103 instruction.has_condition() ? instruction.condition() : true_exprt();
104 irepconverter.reference_convert(condition, out);
105
106 write_gb_word(out, instruction.target_number);
107
108 write_gb_word(out, instruction.targets.size());
109
110 for(const auto &t_it : instruction.targets)
111 write_gb_word(out, t_it->target_number);
112
113 write_gb_word(out, instruction.labels.size());
114
115 for(const auto &l_it : instruction.labels)
116 irepconverter.write_string_ref(out, l_it);
117 }
118 }
119 }
120
121 // irepconverter.output_map(f);
122 // irepconverter.output_string_map(f);
123
124 return false;
125}
126
129 std::ostream &out,
130 const goto_modelt &goto_model,
131 int version)
132{
133 return write_goto_binary(
134 out,
135 goto_model.symbol_table,
136 goto_model.goto_functions,
137 version);
138}
139
142 std::ostream &out,
143 const symbol_tablet &symbol_table,
144 const goto_functionst &goto_functions,
145 int version)
146{
147 // header
148 out << char(0x7f) << "GBF";
149 write_gb_word(out, version);
150
152 irep_serializationt irepconverter(irepc);
153
154 if(version < GOTO_BINARY_VERSION)
156 "version " + std::to_string(version) + " no longer supported",
157 "supported version = " + std::to_string(GOTO_BINARY_VERSION));
158 else if(version > GOTO_BINARY_VERSION)
160 "unknown goto binary version " + std::to_string(version),
161 "supported version = " + std::to_string(GOTO_BINARY_VERSION));
162 else
163 return write_goto_binary(out, symbol_table, goto_functions, irepconverter);
164}
165
168 const std::string &filename,
169 const goto_modelt &goto_model,
170 message_handlert &message_handler)
171{
172 std::ofstream out(filename, std::ios::binary);
173
174 if(!out)
175 {
176 messaget message(message_handler);
177 message.error() << "Failed to open '" << filename << "'";
178 return true;
179 }
180
181 return write_goto_binary(out, goto_model);
182}
A collection of goto functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:33
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
const symbolst & symbols
Read-only field, used to look up symbols given their names.
The symbol table.
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:67
bool is_volatile
Definition symbol.h:66
bool is_extern
Definition symbol.h:66
bool is_macro
Definition symbol.h:61
bool is_file_local
Definition symbol.h:66
irep_idt module
Name of module the symbol belongs to.
Definition symbol.h:43
bool is_static_lifetime
Definition symbol.h:65
bool is_property
Definition symbol.h:62
bool is_parameter
Definition symbol.h:67
bool is_thread_local
Definition symbol.h:65
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:62
bool is_output
Definition symbol.h:62
typet type
Type of symbol.
Definition symbol.h:31
bool is_weak
Definition symbol.h:67
irep_idt name
The unique identifier.
Definition symbol.h:40
bool is_exported
Definition symbol.h:61
irep_idt pretty_name
Language-specific display name.
Definition symbol.h:52
bool is_lvalue
Definition symbol.h:66
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:62
The Boolean constant true.
Definition std_expr.h:2856
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
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
Author: Diffblue Ltd.
bool write_goto_binary(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.
Write GOTO binaries.
#define GOTO_BINARY_VERSION