cprover
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 
16 #include <util/namespace.h>
17 #include <util/message.h>
18 #include <util/symbol_table.h>
20 
21 #include "goto_functions.h"
22 #include "write_goto_binary.h"
23 
28  std::istream &in,
29  symbol_tablet &symbol_table,
30  goto_functionst &functions,
31  irep_serializationt &irepconverter)
32 {
33  std::size_t count = irepconverter.read_gb_word(in); // # of symbols
34 
35  for(std::size_t i=0; i<count; i++)
36  {
37  symbolt sym;
38 
39  sym.type = static_cast<const typet &>(irepconverter.reference_convert(in));
40  sym.value = static_cast<const exprt &>(irepconverter.reference_convert(in));
41  sym.location = static_cast<const source_locationt &>(
42  irepconverter.reference_convert(in));
43 
44  sym.name = irepconverter.read_string_ref(in);
45  sym.module = irepconverter.read_string_ref(in);
46  sym.base_name = irepconverter.read_string_ref(in);
47  sym.mode = irepconverter.read_string_ref(in);
48  sym.pretty_name = irepconverter.read_string_ref(in);
49 
50  // obsolete: symordering
51  irepconverter.read_gb_word(in);
52 
53  std::size_t flags=irepconverter.read_gb_word(in);
54 
55  sym.is_weak = (flags &(1 << 16))!=0;
56  sym.is_type = (flags &(1 << 15))!=0;
57  sym.is_property = (flags &(1 << 14))!=0;
58  sym.is_macro = (flags &(1 << 13))!=0;
59  sym.is_exported = (flags &(1 << 12))!=0;
60  sym.is_input = (flags &(1 << 11))!=0;
61  sym.is_output = (flags &(1 << 10))!=0;
62  sym.is_state_var = (flags &(1 << 9))!=0;
63  sym.is_parameter = (flags &(1 << 8))!=0;
64  sym.is_auxiliary = (flags &(1 << 7))!=0;
65  // sym.binding = (flags &(1 << 6))!=0;
66  sym.is_lvalue = (flags &(1 << 5))!=0;
67  sym.is_static_lifetime = (flags &(1 << 4))!=0;
68  sym.is_thread_local = (flags &(1 << 3))!=0;
69  sym.is_file_local = (flags &(1 << 2))!=0;
70  sym.is_extern = (flags &(1 << 1))!=0;
71  sym.is_volatile = (flags &1)!=0;
72 
73  if(!sym.is_type && sym.type.id()==ID_code)
74  {
75  // makes sure there is an empty function for every function symbol
76  auto entry = functions.function_map.emplace(sym.name, goto_functiont());
77 
78  const code_typet &code_type = to_code_type(sym.type);
79  entry.first->second.type = code_type;
80  entry.first->second.set_parameter_identifiers(code_type);
81  }
82 
83  symbol_table.add(sym);
84  }
85 
86  count=irepconverter.read_gb_word(in); // # of functions
87 
88  for(std::size_t fct_index = 0; fct_index < count; ++fct_index)
89  {
90  irep_idt fname=irepconverter.read_gb_string(in);
91  goto_functionst::goto_functiont &f = functions.function_map[fname];
92 
93  typedef std::map<goto_programt::targett, std::list<unsigned> > target_mapt;
94  target_mapt target_map;
95  typedef std::map<unsigned, goto_programt::targett> rev_target_mapt;
96  rev_target_mapt rev_target_map;
97 
98  bool hidden=false;
99 
100  std::size_t ins_count = irepconverter.read_gb_word(in); // # of instructions
101  for(std::size_t ins_index = 0; ins_index < ins_count; ++ins_index)
102  {
103  goto_programt::targett itarget = f.body.add_instruction();
104  goto_programt::instructiont &instruction=*itarget;
105 
106  instruction.code =
107  static_cast<const codet &>(irepconverter.reference_convert(in));
108  instruction.source_location = static_cast<const source_locationt &>(
109  irepconverter.reference_convert(in));
110  instruction.type = (goto_program_instruction_typet)
111  irepconverter.read_gb_word(in);
112  instruction.guard =
113  static_cast<const exprt &>(irepconverter.reference_convert(in));
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)
119  UNREACHABLE;
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 normally in the type of the goto_functiont object,
135  // which should likely be stored in the binary.
136  }
137  }
138 
139  // Resolve targets
140  for(target_mapt::iterator tit = target_map.begin();
141  tit!=target_map.end();
142  tit++)
143  {
144  goto_programt::targett ins = tit->first;
145 
146  for(std::list<unsigned>::iterator nit = tit->second.begin();
147  nit!=tit->second.end();
148  nit++)
149  {
150  unsigned n=*nit;
151  rev_target_mapt::const_iterator entry=rev_target_map.find(n);
152  INVARIANT(
153  entry != rev_target_map.end(),
154  "something from the target map should also be in the reverse target "
155  "map");
156  ins->targets.push_back(entry->second);
157  }
158  }
159 
160  f.body.update();
161 
162  if(hidden)
163  {
164  f.make_hidden();
165  // can be removed with the next goto-binary version update as the
166  // information is guaranteed to be stored in the symbol table
167 #if GOTO_BINARY_VERSION > 5
168 #error This code should be removed
169 #endif
170  symbol_table.get_writeable_ref(fname).set_hidden();
171  }
172  }
173 
174  functions.compute_location_numbers();
175 
176  return false;
177 }
178 
183  std::istream &in,
184  const std::string &filename,
185  symbol_tablet &symbol_table,
186  goto_functionst &functions,
187  message_handlert &message_handler)
188 {
189  messaget message(message_handler);
190 
191  {
192  char hdr[4];
193  hdr[0]=static_cast<char>(in.get());
194  hdr[1]=static_cast<char>(in.get());
195  hdr[2]=static_cast<char>(in.get());
196 
197  if(hdr[0]=='G' && hdr[1]=='B' && hdr[2]=='F')
198  {
199  // OK!
200  }
201  else
202  {
203  hdr[3]=static_cast<char>(in.get());
204  if(hdr[0]==0x7f && hdr[1]=='G' && hdr[2]=='B' && hdr[3]=='F')
205  {
206  // OK!
207  }
208  else if(hdr[0]==0x7f && hdr[1]=='E' && hdr[2]=='L' && hdr[3]=='F')
209  {
210  if(!filename.empty())
211  message.error() << "Sorry, but I can't read ELF binary '" << filename
212  << "'" << messaget::eom;
213  else
214  message.error() << "Sorry, but I can't read ELF binaries"
215  << messaget::eom;
216 
217  return true;
218  }
219  else
220  {
221  message.error() << "'" << filename << "' is not a goto-binary"
222  << messaget::eom;
223  return true;
224  }
225  }
226  }
227 
229  irep_serializationt irepconverter(ic);
230  // symbol_serializationt symbolconverter(ic);
231 
232  {
233  std::size_t version=irepconverter.read_gb_word(in);
234 
235  if(version < GOTO_BINARY_VERSION)
236  {
237  message.error() <<
238  "The input was compiled with an old version of "
239  "goto-cc; please recompile" << messaget::eom;
240  return true;
241  }
242  else if(version == GOTO_BINARY_VERSION)
243  {
244  return read_bin_goto_object(in, symbol_table, functions, irepconverter);
245  }
246  else
247  {
248  message.error() <<
249  "The input was compiled with an unsupported version of "
250  "goto-cc; please recompile" << messaget::eom;
251  return true;
252  }
253  }
254 
255  return false;
256 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
GOTO_BINARY_VERSION
#define GOTO_BINARY_VERSION
Definition: write_goto_binary.h:15
symbolt::is_state_var
bool is_state_var
Definition: symbol.h:62
irep_serialization.h
binary irep conversions with hashing
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
goto_programt::instructiont::source_location
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:269
read_bin_goto_object.h
Read goto object files.
read_bin_goto_object
static bool read_bin_goto_object(std::istream &in, symbol_tablet &symbol_table, goto_functionst &functions, irep_serializationt &irepconverter)
read goto binary format
Definition: read_bin_goto_object.cpp:27
symbolt::is_macro
bool is_macro
Definition: symbol.h:61
irep_serializationt::read_gb_string
irep_idt read_gb_string(std::istream &)
reads a string from the stream
Definition: irep_serialization.cpp:200
typet
The type of an expression, extends irept.
Definition: type.h:29
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
goto_programt::instructiont::type
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:272
symbolt::is_input
bool is_input
Definition: symbol.h:62
irep_serializationt::reference_convert
const irept & reference_convert(std::istream &)
Definition: irep_serialization.cpp:44
goto_functionst::compute_location_numbers
void compute_location_numbers()
Definition: goto_functions.cpp:18
exprt
Base class for all expressions.
Definition: expr.h:53
irep_serializationt::ireps_containert
Definition: irep_serialization.h:32
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
irep_serializationt::read_gb_word
static std::size_t read_gb_word(std::istream &)
Interpret a stream of byte as a 7-bit encoded unsigned number.
Definition: irep_serialization.cpp:156
messaget::eom
static eomt eom
Definition: message.h:297
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
namespace.h
write_goto_binary.h
Write GOTO binaries.
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
message
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
Definition: static_verifier.cpp:74
symbolt::set_hidden
void set_hidden()
Mark a symbol for internal use.
Definition: symbol.h:128
symbolt::is_thread_local
bool is_thread_local
Definition: symbol.h:65
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
symbol_table_baset::get_writeable_ref
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
Definition: symbol_table_base.h:121
goto_programt::instructiont::code
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:182
goto_programt::instructiont::labels
labelst labels
Definition: goto_program.h:331
symbolt::is_exported
bool is_exported
Definition: symbol.h:61
code_typet
Base type of functions.
Definition: std_types.h:736
symbolt::is_parameter
bool is_parameter
Definition: symbol.h:67
irept::id
const irep_idt & id() const
Definition: irep.h:418
message_handlert
Definition: message.h:28
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:28
goto_program_instruction_typet
goto_program_instruction_typet
The type of an instruction in a GOTO program.
Definition: goto_program.h:32
source_locationt
Definition: source_location.h:20
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
goto_programt::instructiont::target_number
unsigned target_number
A number to identify branch targets.
Definition: goto_program.h:534
symbolt::is_output
bool is_output
Definition: symbol.h:62
symbolt::is_extern
bool is_extern
Definition: symbol.h:66
symbolt::is_volatile
bool is_volatile
Definition: symbol.h:66
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
symbolt
Symbol table entry.
Definition: symbol.h:28
symbolt::is_type
bool is_type
Definition: symbol.h:61
goto_programt::instructiont::guard
exprt guard
Guard for gotos, assume, assert Use get_condition() to read, and set_condition(c) to write.
Definition: goto_program.h:276
symbolt::is_auxiliary
bool is_auxiliary
Definition: symbol.h:67
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
goto_functions.h
Goto Programs with Functions.
irep_serializationt::read_string_ref
irep_idt read_string_ref(std::istream &)
Read a string reference from the stream.
Definition: irep_serialization.cpp:245
symbolt::is_file_local
bool is_file_local
Definition: symbol.h:66
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
symbol_table.h
Author: Diffblue Ltd.
message.h
symbolt::module
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179
irep_serializationt
Definition: irep_serialization.h:29
goto_programt::instructiont::is_target
bool is_target() const
Is this node a branch target?
Definition: goto_program.h:337
symbolt::is_weak
bool is_weak
Definition: symbol.h:67
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
symbolt::is_property
bool is_property
Definition: symbol.h:62
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35