cprover
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
16#include <util/message.h>
17#include <util/symbol_table.h>
19
20#include "goto_functions.h"
21#include "write_goto_binary.h"
22
27 std::istream &in,
28 symbol_tablet &symbol_table,
29 goto_functionst &functions,
31{
32 std::size_t count = irepconverter.read_gb_word(in); // # of symbols
33
34 for(std::size_t i=0; i<count; i++)
35 {
37
38 sym.type = static_cast<const typet &>(irepconverter.reference_convert(in));
39 sym.value = static_cast<const exprt &>(irepconverter.reference_convert(in));
40 sym.location = static_cast<const source_locationt &>(
41 irepconverter.reference_convert(in));
42
43 sym.name = irepconverter.read_string_ref(in);
44 sym.module = irepconverter.read_string_ref(in);
45 sym.base_name = irepconverter.read_string_ref(in);
46 sym.mode = irepconverter.read_string_ref(in);
47 sym.pretty_name = irepconverter.read_string_ref(in);
48
49 // obsolete: symordering
50 irepconverter.read_gb_word(in);
51
52 std::size_t flags=irepconverter.read_gb_word(in);
53
54 sym.is_weak = (flags &(1 << 16))!=0;
55 sym.is_type = (flags &(1 << 15))!=0;
56 sym.is_property = (flags &(1 << 14))!=0;
57 sym.is_macro = (flags &(1 << 13))!=0;
58 sym.is_exported = (flags &(1 << 12))!=0;
59 sym.is_input = (flags &(1 << 11))!=0;
60 sym.is_output = (flags &(1 << 10))!=0;
61 sym.is_state_var = (flags &(1 << 9))!=0;
62 sym.is_parameter = (flags &(1 << 8))!=0;
63 sym.is_auxiliary = (flags &(1 << 7))!=0;
64 // sym.binding = (flags &(1 << 6))!=0;
65 sym.is_lvalue = (flags &(1 << 5))!=0;
66 sym.is_static_lifetime = (flags &(1 << 4))!=0;
67 sym.is_thread_local = (flags &(1 << 3))!=0;
68 sym.is_file_local = (flags &(1 << 2))!=0;
69 sym.is_extern = (flags &(1 << 1))!=0;
70 sym.is_volatile = (flags &1)!=0;
71
72 if(!sym.is_type && sym.type.id()==ID_code)
73 {
74 // makes sure there is an empty function for every function symbol
75 auto entry = functions.function_map.emplace(sym.name, goto_functiont());
76 entry.first->second.set_parameter_identifiers(to_code_type(sym.type));
77 }
78
79 symbol_table.add(sym);
80 }
81
82 count=irepconverter.read_gb_word(in); // # of functions
83
84 for(std::size_t fct_index = 0; fct_index < count; ++fct_index)
85 {
86 irep_idt fname=irepconverter.read_gb_string(in);
88
89 typedef std::map<goto_programt::targett, std::list<unsigned> > target_mapt;
90 target_mapt target_map;
91 typedef std::map<unsigned, goto_programt::targett> rev_target_mapt;
93
94 bool hidden=false;
95
96 std::size_t ins_count = irepconverter.read_gb_word(in); // # of instructions
97 for(std::size_t ins_index = 0; ins_index < ins_count; ++ins_index)
98 {
99 goto_programt::targett itarget = f.body.add_instruction();
100
101 // take copies as references into irepconverter are not stable
102 codet code =
103 static_cast<const codet &>(irepconverter.reference_convert(in));
104 source_locationt source_location = static_cast<const source_locationt &>(
105 irepconverter.reference_convert(in));
108 exprt guard =
109 static_cast<const exprt &>(irepconverter.reference_convert(in));
110
111 goto_programt::instructiont instruction{
112 code, source_location, instruction_type, guard, {}};
113
114 instruction.target_number = irepconverter.read_gb_word(in);
115 if(instruction.is_target() &&
116 rev_target_map.insert(
117 rev_target_map.end(),
118 std::make_pair(instruction.target_number, itarget))->second!=itarget)
120
121 std::size_t t_count = irepconverter.read_gb_word(in); // # of targets
122 for(std::size_t i=0; i<t_count; i++)
123 // just save the target numbers
124 target_map[itarget].push_back(irepconverter.read_gb_word(in));
125
126 std::size_t l_count = irepconverter.read_gb_word(in); // # of labels
127
128 for(std::size_t i=0; i<l_count; i++)
129 {
130 irep_idt label=irepconverter.read_string_ref(in);
131 instruction.labels.push_back(label);
132 if(label == CPROVER_PREFIX "HIDE")
133 hidden=true;
134 // The above info is also held in the goto_functiont object, and could
135 // be stored in the binary.
136 }
137
138 itarget->swap(instruction);
139 }
140
141 // Resolve targets
142 for(target_mapt::iterator tit = target_map.begin();
143 tit!=target_map.end();
144 tit++)
145 {
147
148 for(std::list<unsigned>::iterator nit = tit->second.begin();
149 nit!=tit->second.end();
150 nit++)
151 {
152 unsigned n=*nit;
153 rev_target_mapt::const_iterator entry=rev_target_map.find(n);
154 INVARIANT(
155 entry != rev_target_map.end(),
156 "something from the target map should also be in the reverse target "
157 "map");
158 ins->targets.push_back(entry->second);
159 }
160 }
161
162 f.body.update();
163
164 if(hidden)
165 f.make_hidden();
166 }
167
168 functions.compute_location_numbers();
169
170 return false;
171}
172
177 std::istream &in,
178 const std::string &filename,
179 symbol_tablet &symbol_table,
180 goto_functionst &functions,
181 message_handlert &message_handler)
182{
183 messaget message(message_handler);
184
185 {
186 char hdr[4];
187 hdr[0]=static_cast<char>(in.get());
188 hdr[1]=static_cast<char>(in.get());
189 hdr[2]=static_cast<char>(in.get());
190
191 if(hdr[0]=='G' && hdr[1]=='B' && hdr[2]=='F')
192 {
193 // OK!
194 }
195 else
196 {
197 hdr[3]=static_cast<char>(in.get());
198 if(hdr[0]==0x7f && hdr[1]=='G' && hdr[2]=='B' && hdr[3]=='F')
199 {
200 // OK!
201 }
202 else if(hdr[0]==0x7f && hdr[1]=='E' && hdr[2]=='L' && hdr[3]=='F')
203 {
204 if(!filename.empty())
205 message.error() << "Sorry, but I can't read ELF binary '" << filename
206 << "'" << messaget::eom;
207 else
208 message.error() << "Sorry, but I can't read ELF binaries"
209 << messaget::eom;
210
211 return true;
212 }
213 else
214 {
215 message.error() << "'" << filename << "' is not a goto-binary"
216 << messaget::eom;
217 return true;
218 }
219 }
220 }
221
224 // symbol_serializationt symbolconverter(ic);
225
226 {
227 std::size_t version=irepconverter.read_gb_word(in);
228
229 if(version < GOTO_BINARY_VERSION)
230 {
231 message.error() <<
232 "The input was compiled with an old version of "
233 "goto-cc; please recompile" << messaget::eom;
234 return true;
235 }
236 else if(version == GOTO_BINARY_VERSION)
237 {
238 return read_bin_goto_object(in, symbol_table, functions, irepconverter);
239 }
240 else
241 {
242 message.error() <<
243 "The input was compiled with an unsupported version of "
244 "goto-cc; please recompile" << messaget::eom;
245 return true;
246 }
247 }
248
249 return false;
250}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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:37
Base class for all expressions.
Definition expr.h:54
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:155
mstreamt & error() const
Definition message.h:399
static eomt eom
Definition message.h:297
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
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 bool read_bin_goto_object(std::istream &in, symbol_tablet &symbol_table, goto_functionst &functions, irep_serializationt &irepconverter)
read goto binary format
Read goto object files.
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:503
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
Author: Diffblue Ltd.
Write GOTO binaries.
#define GOTO_BINARY_VERSION