CBMC
read_bin_goto_object.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Read goto object files.
4 
5 Author: CM Wintersteiger
6 
7 Date: June 2006
8 
9 \*******************************************************************/
10 
13 
14 #include "read_bin_goto_object.h"
15 
17 #include <util/message.h>
18 #include <util/symbol_table_base.h>
19 
20 #include "goto_functions.h"
21 #include "write_goto_binary.h"
22 
24  std::istream &in,
25  symbol_table_baset &symbol_table,
26  irep_serializationt &irepconverter)
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  {
32  symbolt sym;
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,
101  irep_serializationt &irepconverter)
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);
108  goto_functionst::goto_functiont &f = functions.function_map[fname];
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;
117  rev_target_mapt rev_target_map;
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));
131  goto_program_instruction_typet instruction_type =
132  (goto_program_instruction_typet)irepconverter.read_gb_word(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)
144  UNREACHABLE;
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  {
171  goto_programt::targett ins = tit->first;
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,
202  irep_serializationt &irepconverter)
203 {
204  read_bin_symbol_table_object(in, symbol_table, irepconverter);
205  copy_parameter_identifiers(symbol_table, functions);
206  read_bin_functions_object(in, functions, irepconverter);
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 
257  irep_serializationt irepconverter(ic);
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)
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
void swap(dstringt &b)
Definition: dstring.h:162
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...
Definition: goto_function.h:24
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:181
instructionst::iterator targett
Definition: goto_program.h:614
static std::size_t read_gb_word(std::istream &)
Interpret a stream of byte as a 7-bit encoded unsigned number.
const irept & reference_convert(std::istream &)
irep_idt read_string_ref(std::istream &)
Read a string reference from the stream.
irep_idt read_gb_string(std::istream &)
reads a string from the stream
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
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_auxiliary
Definition: symbol.h:77
bool is_volatile
Definition: symbol.h:75
bool is_extern
Definition: symbol.h:74
bool is_macro
Definition: symbol.h:62
bool is_file_local
Definition: symbol.h:73
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
bool is_static_lifetime
Definition: symbol.h:70
bool is_property
Definition: symbol.h:67
bool is_parameter
Definition: symbol.h:76
bool is_thread_local
Definition: symbol.h:71
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:66
bool is_output
Definition: symbol.h:65
typet type
Type of symbol.
Definition: symbol.h:31
bool is_weak
Definition: symbol.h:78
irep_idt name
The unique identifier.
Definition: symbol.h:40
bool is_exported
Definition: symbol.h:63
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
bool is_lvalue
Definition: symbol.h:72
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:64
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.
Definition: goto_program.h:32
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.
Definition: goto_program.h:392
Author: Diffblue Ltd.
Write GOTO binaries.
#define GOTO_BINARY_VERSION