cprover
goto_convert_functions.cpp
Go to the documentation of this file.
1 /********************************************************************\
2 
3 Module: Goto Programs with Functions
4 
5 Author: Daniel Kroening
6 
7 Date: June 2003
8 
9 \*******************************************************************/
10 
11 #include "goto_convert_functions.h"
12 
13 #include <cassert>
14 
15 #include <util/base_type.h>
16 #include <util/std_code.h>
17 #include <util/symbol_table.h>
18 #include <util/prefix.h>
19 #include <util/fresh_symbol.h>
20 
21 #include "goto_inline.h"
22 
24  symbol_table_baset &_symbol_table,
25  message_handlert &_message_handler):
26  goto_convertt(_symbol_table, _message_handler)
27 {
28 }
29 
31 {
32 }
33 
35 {
36  // warning! hash-table iterators are not stable
37 
38  typedef std::list<irep_idt> symbol_listt;
39  symbol_listt symbol_list;
40 
41  for(const auto &symbol_pair : symbol_table.symbols)
42  {
43  if(
44  !symbol_pair.second.is_type && !symbol_pair.second.is_macro &&
45  symbol_pair.second.type.id() == ID_code &&
46  (symbol_pair.second.mode == ID_C || symbol_pair.second.mode == ID_cpp ||
47  symbol_pair.second.mode == ID_java || symbol_pair.second.mode == "jsil"))
48  {
49  symbol_list.push_back(symbol_pair.first);
50  }
51  }
52 
53  for(const auto &id : symbol_list)
54  {
55  convert_function(id, functions.function_map[id]);
56  }
57 
58  functions.compute_location_numbers();
59 
60  // this removes the parse tree of the bodies from memory
61  #if 0
62  for(const auto &symbol_pair, symbol_table.symbols)
63  {
64  if(!symbol_pair.second.is_type &&
65  symbol_pair.second.type.id()==ID_code &&
66  symbol_pair.second.value.is_not_nil())
67  {
68  symbol_pair.second.value=codet();
69  }
70  }
71  #endif
72 }
73 
75 {
77  {
78  for(const auto &label : i_it->labels)
79  if(label=="__CPROVER_HIDE")
80  return true;
81  }
82 
83  return false;
84 }
85 
88  const source_locationt &source_location)
89 {
90  #if 0
91  if(!f.body.instructions.empty() &&
92  f.body.instructions.back().is_return())
93  return; // not needed, we have one already
94 
95  // see if we have an unconditional goto at the end
96  if(!f.body.instructions.empty() &&
97  f.body.instructions.back().is_goto() &&
98  f.body.instructions.back().guard.is_true())
99  return;
100  #else
101 
102  if(!f.body.instructions.empty())
103  {
104  goto_programt::const_targett last_instruction=
105  f.body.instructions.end();
106  last_instruction--;
107 
108  while(true)
109  {
110  // unconditional goto, say from while(1)?
111  if(last_instruction->is_goto() &&
112  last_instruction->guard.is_true())
113  return;
114 
115  // return?
116  if(last_instruction->is_return())
117  return;
118 
119  // advance if it's a 'dead' without branch target
120  if(last_instruction->is_dead() &&
121  last_instruction!=f.body.instructions.begin() &&
122  !last_instruction->is_target())
123  last_instruction--;
124  else
125  break; // give up
126  }
127  }
128 
129  #endif
130 
131  const side_effect_expr_nondett rhs(f.type.return_type(), source_location);
132 
133  goto_programt::targett t=f.body.add_instruction();
134  t->make_return();
135  t->code=code_returnt(rhs);
136  t->source_location=source_location;
137 }
138 
140  const irep_idt &identifier,
142 {
143  const symbolt &symbol=ns.lookup(identifier);
144  const irep_idt mode = symbol.mode;
145 
146  if(f.body_available())
147  return; // already converted
148 
149  // make tmp variables local to function
150  tmp_symbol_prefix=id2string(symbol.name)+"::$tmp";
151 
152  f.type=to_code_type(symbol.type);
153 
154  if(symbol.value.is_nil() ||
155  symbol.value.id()=="compiled") /* goto_inline may have removed the body */
156  return;
157 
158  if(symbol.value.id()!=ID_code)
159  {
161  error() << "got invalid code for function `" << identifier << "'"
162  << eom;
163  throw 0;
164  }
165 
166  const codet &code=to_code(symbol.value);
167 
168  source_locationt end_location;
169 
170  if(code.get_statement()==ID_block)
171  end_location=to_code_block(code).end_location();
172  else
173  end_location.make_nil();
174 
175  goto_programt tmp_end_function;
176  goto_programt::targett end_function=tmp_end_function.add_instruction();
177  end_function->type=END_FUNCTION;
178  end_function->source_location=end_location;
179  end_function->code.set(ID_identifier, identifier);
180 
181  targets=targetst();
182  targets.set_return(end_function);
184  f.type.return_type().id()!=ID_empty &&
185  f.type.return_type().id()!=ID_constructor &&
186  f.type.return_type().id()!=ID_destructor;
187 
188  goto_convert_rec(code, f.body, mode);
189 
190  // add non-det return value, if needed
192  add_return(f, end_location);
193 
194  // handle SV-COMP's __VERIFIER_atomic_
195  if(!f.body.instructions.empty() &&
196  has_prefix(id2string(identifier), "__VERIFIER_atomic_"))
197  {
199  a_begin.make_atomic_begin();
200  a_begin.source_location=f.body.instructions.front().source_location;
201  f.body.insert_before_swap(f.body.instructions.begin(), a_begin);
202 
203  goto_programt::targett a_end=f.body.add_instruction();
204  a_end->make_atomic_end();
205  a_end->source_location=end_location;
206 
208  {
209  if(i_it->is_goto() && i_it->get_target()->is_end_function())
210  i_it->set_target(a_end);
211  }
212  }
213 
214  // add "end of function"
215  f.body.destructive_append(tmp_end_function);
216 
217  // do function tags (they are empty at this point)
218  f.update_instructions_function(identifier);
219 
220  f.body.update();
221 
222  if(hide(f.body))
223  f.make_hidden();
224 }
225 
227  goto_modelt &goto_model,
229 {
230  goto_convert(
231  goto_model.symbol_table,
232  goto_model.goto_functions,
234 }
235 
237  symbol_table_baset &symbol_table,
238  goto_functionst &functions,
240 {
241  const unsigned errors_before=
242  message_handler.get_message_count(messaget::M_ERROR);
243 
244  goto_convert_functionst goto_convert_functions(symbol_table, message_handler);
245 
246  try
247  {
248  goto_convert_functions.goto_convert(functions);
249  }
250 
251  catch(int)
252  {
253  goto_convert_functions.error();
254  }
255 
256  catch(const char *e)
257  {
258  goto_convert_functions.error() << e << messaget::eom;
259  }
260 
261  catch(const std::string &e)
262  {
263  goto_convert_functions.error() << e << messaget::eom;
264  }
265 
266  if(message_handler.get_message_count(messaget::M_ERROR)!=errors_before)
267  throw 0;
268 }
269 
271  const irep_idt &identifier,
272  symbol_table_baset &symbol_table,
273  goto_functionst &functions,
275 {
276  const unsigned errors_before=
277  message_handler.get_message_count(messaget::M_ERROR);
278 
279  goto_convert_functionst goto_convert_functions(symbol_table, message_handler);
280 
281  try
282  {
283  goto_convert_functions.convert_function(
284  identifier, functions.function_map[identifier]);
285  }
286 
287  catch(int)
288  {
289  goto_convert_functions.error();
290  }
291 
292  catch(const char *e)
293  {
294  goto_convert_functions.error() << e << messaget::eom;
295  }
296 
297  catch(const std::string &e)
298  {
299  goto_convert_functions.error() << e << messaget::eom;
300  }
301 
302  if(message_handler.get_message_count(messaget::M_ERROR)!=errors_before)
303  throw 0;
304 }
const irep_idt & get_statement() const
Definition: std_code.h:40
irep_idt name
The unique identifier.
Definition: symbol.h:43
bool is_nil() const
Definition: irep.h:172
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
struct goto_convertt::targetst targets
irep_idt mode
Language mode.
Definition: symbol.h:52
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:993
source_locationt end_location() const
Definition: std_code.h:126
Fresh auxiliary symbol creation.
exprt value
Initial value of symbol.
Definition: symbol.h:37
function_mapt function_map
void convert_function(const irep_idt &identifier, goto_functionst::goto_functiont &result)
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
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
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
const irep_idt & id() const
Definition: irep.h:259
void compute_location_numbers()
std::string tmp_symbol_prefix
instructionst::iterator targett
Definition: goto_program.h:397
const source_locationt & find_source_location() const
Definition: expr.cpp:246
source_locationt source_location
Definition: message.h:214
void goto_convert_rec(const codet &code, goto_programt &dest, const irep_idt &mode)
instructionst::const_iterator const_targett
Definition: goto_program.h:398
goto_convert_functionst(symbol_table_baset &_symbol_table, message_handlert &_message_handler)
mstreamt & error() const
Definition: message.h:302
Function Inlining.
::goto_functiont goto_functiont
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1340
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Author: Diffblue Ltd.
const symbolst & symbols
static bool hide(const goto_programt &)
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
typet type
Type of symbol.
Definition: symbol.h:34
Goto Programs with Functions.
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:182
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
The symbol table base class interface.
void goto_convert(goto_modelt &goto_model, message_handlert &message_handler)
void goto_convert(goto_functionst &functions)
symbol_table_baset & symbol_table
void make_nil()
Definition: irep.h:315
goto_programt & goto_program
Definition: cover.cpp:63
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
const codet & to_code(const exprt &expr)
Definition: std_code.h:75
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:165
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
A statement in a programming language.
Definition: std_code.h:21
void add_return(goto_functionst::goto_functiont &, const source_locationt &)
Return from a function.
Definition: std_code.h:923
Base Type Computation.
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:735
void set_return(goto_programt::targett _return_target)
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:136
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286