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 
27  std::istream &in,
28  const std::string &filename,
29  symbol_tablet &symbol_table,
30  goto_functionst &functions,
32  irep_serializationt &irepconverter)
33 {
34  std::size_t count = irepconverter.read_gb_word(in); // # of symbols
35 
36  for(std::size_t i=0; i<count; i++)
37  {
38  symbolt sym;
39 
40  irepconverter.reference_convert(in, sym.type);
41  irepconverter.reference_convert(in, sym.value);
42  irepconverter.reference_convert(in, sym.location);
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
76  // for every function symbol and fixes
77  // the function types.
78  functions.function_map[sym.name].type=to_code_type(sym.type);
79  }
80 
81  symbol_table.add(sym);
82  }
83 
84  count=irepconverter.read_gb_word(in); // # of functions
85 
86  for(std::size_t i=0; i<count; i++)
87  {
88  irep_idt fname=irepconverter.read_gb_string(in);
89  goto_functionst::goto_functiont &f = functions.function_map[fname];
90 
91  typedef std::map<goto_programt::targett, std::list<unsigned> > target_mapt;
92  target_mapt target_map;
93  typedef std::map<unsigned, goto_programt::targett> rev_target_mapt;
94  rev_target_mapt rev_target_map;
95 
96  bool hidden=false;
97 
98  std::size_t ins_count = irepconverter.read_gb_word(in); // # of instructions
99  for(std::size_t i=0; i<ins_count; i++)
100  {
101  goto_programt::targett itarget = f.body.add_instruction();
102  goto_programt::instructiont &instruction=*itarget;
103 
104  irepconverter.reference_convert(in, instruction.code);
105  instruction.function = irepconverter.read_string_ref(in);
106  irepconverter.reference_convert(in, instruction.source_location);
107  instruction.type = (goto_program_instruction_typet)
108  irepconverter.read_gb_word(in);
109  instruction.guard.make_nil();
110  irepconverter.reference_convert(in, instruction.guard);
111  irepconverter.read_string_ref(in); // former event
112  instruction.target_number = irepconverter.read_gb_word(in);
113  if(instruction.is_target() &&
114  rev_target_map.insert(
115  rev_target_map.end(),
116  std::make_pair(instruction.target_number, itarget))->second!=itarget)
117  UNREACHABLE;
118 
119  std::size_t t_count = irepconverter.read_gb_word(in); // # of targets
120  for(std::size_t i=0; i<t_count; i++)
121  // just save the target numbers
122  target_map[itarget].push_back(irepconverter.read_gb_word(in));
123 
124  std::size_t l_count = irepconverter.read_gb_word(in); // # of labels
125 
126  for(std::size_t i=0; i<l_count; i++)
127  {
128  irep_idt label=irepconverter.read_string_ref(in);
129  instruction.labels.push_back(label);
130  if(label=="__CPROVER_HIDE")
131  hidden=true;
132  // The above info is normally in the type of the goto_functiont object,
133  // which should likely be stored in the binary.
134  }
135  }
136 
137  // Resolve targets
138  for(target_mapt::iterator tit = target_map.begin();
139  tit!=target_map.end();
140  tit++)
141  {
142  goto_programt::targett ins = tit->first;
143 
144  for(std::list<unsigned>::iterator nit = tit->second.begin();
145  nit!=tit->second.end();
146  nit++)
147  {
148  unsigned n=*nit;
149  rev_target_mapt::const_iterator entry=rev_target_map.find(n);
150  assert(entry!=rev_target_map.end());
151  ins->targets.push_back(entry->second);
152  }
153  }
154 
155  f.body.update();
156 
157  if(hidden)
158  f.make_hidden();
159  }
160 
161  functions.compute_location_numbers();
162 
163  return false;
164 }
165 
170  std::istream &in,
171  const std::string &filename,
172  symbol_tablet &symbol_table,
173  goto_functionst &functions,
175 {
176  messaget message(message_handler);
177 
178  {
179  char hdr[4];
180  hdr[0]=static_cast<char>(in.get());
181  hdr[1]=static_cast<char>(in.get());
182  hdr[2]=static_cast<char>(in.get());
183 
184  if(hdr[0]=='G' && hdr[1]=='B' && hdr[2]=='F')
185  {
186  // OK!
187  }
188  else
189  {
190  hdr[3]=static_cast<char>(in.get());
191  if(hdr[0]==0x7f && hdr[1]=='G' && hdr[2]=='B' && hdr[3]=='F')
192  {
193  // OK!
194  }
195  else if(hdr[0]==0x7f && hdr[1]=='E' && hdr[2]=='L' && hdr[3]=='F')
196  {
197  if(filename!="")
198  message.error() << "Sorry, but I can't read ELF binary `"
199  << filename << "'" << messaget::eom;
200  else
201  message.error() << "Sorry, but I can't read ELF binaries"
202  << messaget::eom;
203 
204  return true;
205  }
206  else
207  {
208  message.error() << "`" << filename << "' is not a goto-binary"
209  << messaget::eom;
210  return true;
211  }
212  }
213  }
214 
216  irep_serializationt irepconverter(ic);
217  // symbol_serializationt symbolconverter(ic);
218 
219  {
220  std::size_t version=irepconverter.read_gb_word(in);
221 
222  switch(version)
223  {
224  case 1:
225  case 2:
226  message.error() <<
227  "The input was compiled with an old version of "
228  "goto-cc; please recompile" << messaget::eom;
229  return true;
230 
231  case 3:
232  return read_bin_goto_object_v3(in, filename,
233  symbol_table, functions,
235  irepconverter);
236  break;
237 
238  default:
239  message.error() <<
240  "The input was compiled with an unsupported version of "
241  "goto-cc; please recompile" << messaget::eom;
242  return true;
243  }
244  }
245 
246  return false;
247 }
exprt guard
Guard for gotos, assume, assert.
Definition: goto_program.h:188
irep_idt function
The function this instruction belongs to.
Definition: goto_program.h:179
irep_idt name
The unique identifier.
Definition: symbol.h:43
bool is_output
Definition: symbol.h:63
bool is_thread_local
Definition: symbol.h:67
irep_idt mode
Language mode.
Definition: symbol.h:52
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:185
Read goto object files.
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:987
Goto Programs with Functions.
exprt value
Initial value of symbol.
Definition: symbol.h:37
irep_idt read_string_ref(std::istream &)
reads a string reference from the stream
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:46
function_mapt function_map
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:55
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
bool is_static_lifetime
Definition: symbol.h:67
bool is_input
Definition: symbol.h:63
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
unsigned target_number
A number to identify branch targets.
Definition: goto_program.h:371
bool read_bin_goto_object_v3(std::istream &in, const std::string &filename, symbol_tablet &symbol_table, goto_functionst &functions, message_handlert &message_handler, irep_serializationt &irepconverter)
read goto binary format v3
const irep_idt & id() const
Definition: irep.h:189
void compute_location_numbers()
instructionst::iterator targett
Definition: goto_program.h:397
bool is_exported
Definition: symbol.h:63
bool is_parameter
Definition: symbol.h:68
The symbol table.
Definition: symbol_table.h:19
mstreamt & error() const
Definition: message.h:302
::goto_functiont goto_functiont
void reference_convert(std::istream &, irept &irep)
goto_program_instruction_typet
The type of an instruction in a GOTO program.
Definition: goto_program.h:29
Author: Diffblue Ltd.
binary irep conversions with hashing
bool is_volatile
Definition: symbol.h:68
bool read_bin_goto_object(std::istream &in, const std::string &filename, symbol_tablet &symbol_table, goto_functionst &functions, message_handlert &message_handler)
reads a goto binary file back into a symbol and a function table
bool is_extern
Definition: symbol.h:68
irep_idt read_gb_string(std::istream &)
reads a string from the stream
typet type
Type of symbol.
Definition: symbol.h:34
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:182
bool is_state_var
Definition: symbol.h:63
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
#define UNREACHABLE
Definition: invariant.h:250
bool is_file_local
Definition: symbol.h:68
void make_nil()
Definition: irep.h:243
bool is_weak
Definition: symbol.h:68
static std::size_t read_gb_word(std::istream &)
reads 4 characters and builds a long int from them
bool is_auxiliary
Definition: symbol.h:68
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
bool is_type
Definition: symbol.h:63
bool is_property
Definition: symbol.h:63
bool is_target() const
Is this node a branch target?
Definition: goto_program.h:229
bool is_macro
Definition: symbol.h:63
bool is_lvalue
Definition: symbol.h:68