CBMC
Loading...
Searching...
No Matches
read_bin_goto_object.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Read goto object files.
4
5Author: CM Wintersteiger
6
7Date: June 2006
8
9\*******************************************************************/
10
13
15
17#include <util/message.h>
19
20#include "goto_functions.h"
21#include "write_goto_binary.h"
22
24 std::istream &in,
25 symbol_table_baset &symbol_table,
27{
28 const std::size_t count = irepconverter.read_gb_word(in); // # of symbols
29
30 for(std::size_t i=0; i<count; i++)
31 {
33
34 sym.type = static_cast<const typet &>(irepconverter.reference_convert(in));
35 sym.value = static_cast<const exprt &>(irepconverter.reference_convert(in));
36 sym.location = static_cast<const source_locationt &>(
37 irepconverter.reference_convert(in));
38
39 sym.name = irepconverter.read_string_ref(in);
40 sym.module = irepconverter.read_string_ref(in);
41 sym.base_name = irepconverter.read_string_ref(in);
42 sym.mode = irepconverter.read_string_ref(in);
43 sym.pretty_name = irepconverter.read_string_ref(in);
44
45 // obsolete: symordering
46 irepconverter.read_gb_word(in);
47
48 std::size_t flags=irepconverter.read_gb_word(in);
49
50 sym.is_weak = (flags &(1 << 16))!=0;
51 sym.is_type = (flags &(1 << 15))!=0;
52 sym.is_property = (flags &(1 << 14))!=0;
53 sym.is_macro = (flags &(1 << 13))!=0;
54 sym.is_exported = (flags &(1 << 12))!=0;
55 sym.is_input = (flags &(1 << 11))!=0;
56 sym.is_output = (flags &(1 << 10))!=0;
57 sym.is_state_var = (flags &(1 << 9))!=0;
58 sym.is_parameter = (flags &(1 << 8))!=0;
59 sym.is_auxiliary = (flags &(1 << 7))!=0;
60 // sym.binding = (flags &(1 << 6))!=0;
61 sym.is_lvalue = (flags &(1 << 5))!=0;
62 sym.is_static_lifetime = (flags &(1 << 4))!=0;
63 sym.is_thread_local = (flags &(1 << 3))!=0;
64 sym.is_file_local = (flags &(1 << 2))!=0;
65 sym.is_extern = (flags &(1 << 1))!=0;
66 sym.is_volatile = (flags &1)!=0;
67
68 symbol_table.add(sym);
69 }
70}
71
78 const symbol_table_baset &symbol_table,
79 goto_functionst &functions)
80{
81 for(const auto &name_symbol : symbol_table)
82 {
83 const auto &symbol = name_symbol.second;
84 if(symbol.is_type)
85 continue;
86
87 const auto code_type = type_try_dynamic_cast<code_typet>(symbol.type);
88 if(!code_type)
89 continue;
90
91 // Makes sure there is an empty function for every function symbol.
92 auto emplaced =
93 functions.function_map.emplace(symbol.name, goto_functiont());
94 emplaced.first->second.set_parameter_identifiers(*code_type);
95 }
96}
97
99 std::istream &in,
100 goto_functionst &functions,
102{
103 const std::size_t count = irepconverter.read_gb_word(in); // # of functions
104
105 for(std::size_t fct_index = 0; fct_index < count; ++fct_index)
106 {
107 irep_idt fname=irepconverter.read_gb_string(in);
109
110 typedef std::map<
112 std::list<unsigned>,
114 target_mapt;
115 target_mapt target_map;
116 typedef std::map<unsigned, goto_programt::targett> rev_target_mapt;
118
119 bool hidden=false;
120
121 std::size_t ins_count = irepconverter.read_gb_word(in); // # of instructions
122 for(std::size_t ins_index = 0; ins_index < ins_count; ++ins_index)
123 {
124 goto_programt::targett itarget = f.body.add_instruction();
125
126 // take copies as references into irepconverter are not stable
127 codet code =
128 static_cast<const codet &>(irepconverter.reference_convert(in));
129 source_locationt source_location = static_cast<const source_locationt &>(
130 irepconverter.reference_convert(in));
133 exprt guard =
134 static_cast<const exprt &>(irepconverter.reference_convert(in));
135
136 goto_programt::instructiont instruction{
137 code, source_location, instruction_type, guard, {}};
138
139 instruction.target_number = irepconverter.read_gb_word(in);
140 if(instruction.is_target() &&
141 rev_target_map.insert(
142 rev_target_map.end(),
143 std::make_pair(instruction.target_number, itarget))->second!=itarget)
145
146 std::size_t t_count = irepconverter.read_gb_word(in); // # of targets
147 for(std::size_t i=0; i<t_count; i++)
148 // just save the target numbers
149 target_map[itarget].push_back(irepconverter.read_gb_word(in));
150
151 std::size_t l_count = irepconverter.read_gb_word(in); // # of labels
152
153 for(std::size_t i=0; i<l_count; i++)
154 {
155 irep_idt label=irepconverter.read_string_ref(in);
156 instruction.labels.push_back(label);
157 if(label == CPROVER_PREFIX "HIDE")
158 hidden=true;
159 // The above info is also held in the goto_functiont object, and could
160 // be stored in the binary.
161 }
162
163 itarget->swap(instruction);
164 }
165
166 // Resolve targets
167 for(target_mapt::iterator tit = target_map.begin();
168 tit!=target_map.end();
169 tit++)
170 {
172
173 for(std::list<unsigned>::iterator nit = tit->second.begin();
174 nit!=tit->second.end();
175 nit++)
176 {
177 unsigned n=*nit;
178 rev_target_mapt::const_iterator entry=rev_target_map.find(n);
179 INVARIANT(
180 entry != rev_target_map.end(),
181 "something from the target map should also be in the reverse target "
182 "map");
183 ins->targets.push_back(entry->second);
184 }
185 }
186
187 f.body.update();
188
189 if(hidden)
190 f.make_hidden();
191 }
192
193 functions.compute_location_numbers();
194}
195
199 std::istream &in,
200 symbol_table_baset &symbol_table,
201 goto_functionst &functions,
203{
205 copy_parameter_identifiers(symbol_table, functions);
207}
208
213 std::istream &in,
214 const std::string &filename,
215 symbol_table_baset &symbol_table,
216 goto_functionst &functions,
217 message_handlert &message_handler)
218{
219 messaget message(message_handler);
220
221 char hdr[4];
222 hdr[0] = static_cast<char>(in.get());
223 hdr[1] = static_cast<char>(in.get());
224 hdr[2] = static_cast<char>(in.get());
225
226 if(hdr[0] == 'G' && hdr[1] == 'B' && hdr[2] == 'F')
227 {
228 // OK!
229 }
230 else
231 {
232 hdr[3] = static_cast<char>(in.get());
233 if(hdr[0] == 0x7f && hdr[1] == 'G' && hdr[2] == 'B' && hdr[3] == 'F')
234 {
235 // OK!
236 }
237 else if(hdr[0] == 0x7f && hdr[1] == 'E' && hdr[2] == 'L' && hdr[3] == 'F')
238 {
239 if(!filename.empty())
240 message.error() << "Sorry, but I can't read ELF binary '" << filename
241 << "'" << messaget::eom;
242 else
243 message.error() << "Sorry, but I can't read ELF binaries"
244 << messaget::eom;
245
246 return true;
247 }
248 else
249 {
250 message.error() << "'" << filename << "' is not a goto-binary"
251 << messaget::eom;
252 return true;
253 }
254 }
255
258
259 const std::size_t version = irepconverter.read_gb_word(in);
260
261 if(version < GOTO_BINARY_VERSION)
262 {
263 message.error() << "The input was compiled with an old version of "
264 "goto-cc; please recompile"
265 << messaget::eom;
266 return true;
267 }
268 else if(version == GOTO_BINARY_VERSION)
269 {
270 read_bin_goto_object(in, symbol_table, functions, irepconverter);
271 return false;
272 }
273 else
274 {
275 message.error() << "The input was compiled with an unsupported version of "
276 "goto-cc; please recompile"
277 << messaget::eom;
278 return true;
279 }
280}
static exprt guard(const exprt::operandst &guards, exprt cond)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Data structure for representing an arbitrary statement in a program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
void compute_location_numbers()
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
This class represents an instruction in the GOTO intermediate representation.
instructionst::iterator targett
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
mstreamt & error() const
Definition message.h:391
static eomt eom
Definition message.h:289
The symbol table base class interface.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Symbol table entry.
Definition symbol.h:28
The type of an expression, extends irept.
Definition type.h:29
#define CPROVER_PREFIX
Goto Programs with Functions.
goto_program_instruction_typet
The type of an instruction in a GOTO program.
binary irep conversions with hashing
static void copy_parameter_identifiers(const symbol_table_baset &symbol_table, goto_functionst &functions)
The serialised form of the goto-model currently includes the parameter identifiers in the symbol tabl...
static void read_bin_goto_object(std::istream &in, symbol_table_baset &symbol_table, goto_functionst &functions, irep_serializationt &irepconverter)
read goto binary format
static void read_bin_functions_object(std::istream &in, goto_functionst &functions, irep_serializationt &irepconverter)
static void read_bin_symbol_table_object(std::istream &in, symbol_table_baset &symbol_table, irep_serializationt &irepconverter)
Read goto object files.
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
A total order over targett and const_targett.
Author: Diffblue Ltd.
Write GOTO binaries.
#define GOTO_BINARY_VERSION