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 
20 #include "goto_inline.h"
21 
23  symbol_tablet &_symbol_table,
24  goto_functionst &_functions,
25  message_handlert &_message_handler):
26  goto_convertt(_symbol_table, _message_handler),
27  functions(_functions)
28 {
29 }
30 
32 {
33 }
34 
36 {
37  // warning! hash-table iterators are not stable
38 
39  typedef std::list<irep_idt> symbol_listt;
40  symbol_listt symbol_list;
41 
43  {
44  if(!it->second.is_type &&
45  !it->second.is_macro &&
46  it->second.type.id()==ID_code &&
47  (it->second.mode==ID_C ||
48  it->second.mode==ID_cpp ||
49  it->second.mode==ID_java ||
50  it->second.mode=="jsil"))
51  symbol_list.push_back(it->first);
52  }
53 
54  for(const auto &id : symbol_list)
55  {
56  convert_function(id);
57  }
58 
60 
61  // this removes the parse tree of the bodies from memory
62  #if 0
64  {
65  if(!it->second.is_type &&
66  it->second.type.id()==ID_code &&
67  it->second.value.is_not_nil())
68  it->second.value=codet();
69  }
70  #endif
71 }
72 
74 {
75  forall_goto_program_instructions(i_it, goto_program)
76  {
77  for(const auto &label : i_it->labels)
78  if(label=="__CPROVER_HIDE")
79  return true;
80  }
81 
82  return false;
83 }
84 
87  const source_locationt &source_location)
88 {
89  #if 0
90  if(!f.body.instructions.empty() &&
91  f.body.instructions.back().is_return())
92  return; // not needed, we have one already
93 
94  // see if we have an unconditional goto at the end
95  if(!f.body.instructions.empty() &&
96  f.body.instructions.back().is_goto() &&
97  f.body.instructions.back().guard.is_true())
98  return;
99  #else
100 
101  if(!f.body.instructions.empty())
102  {
103  goto_programt::const_targett last_instruction=
104  f.body.instructions.end();
105  last_instruction--;
106 
107  while(true)
108  {
109  // unconditional goto, say from while(1)?
110  if(last_instruction->is_goto() &&
111  last_instruction->guard.is_true())
112  return;
113 
114  // return?
115  if(last_instruction->is_return())
116  return;
117 
118  // advance if it's a 'dead' without branch target
119  if(last_instruction->is_dead() &&
120  last_instruction!=f.body.instructions.begin() &&
121  !last_instruction->is_target())
122  last_instruction--;
123  else
124  break; // give up
125  }
126  }
127 
128  #endif
129 
130  side_effect_expr_nondett rhs(f.type.return_type());
131 
132  goto_programt::targett t=f.body.add_instruction();
133  t->make_return();
134  t->code=code_returnt(rhs);
135  t->source_location=source_location;
136 }
137 
139 {
140  const symbolt &symbol=ns.lookup(identifier);
142 
143  // make tmp variables local to function
144  tmp_symbol_prefix=id2string(symbol.name)+"::$tmp::";
146 
147  f.type=to_code_type(symbol.type);
148  if(f.body_available())
149  return; // already converted
150 
151  if(symbol.value.is_nil() ||
152  symbol.value.id()=="compiled") /* goto_inline may have removed the body */
153  return;
154 
155  if(symbol.value.id()!=ID_code)
156  {
158  error() << "got invalid code for function `" << identifier << "'"
159  << eom;
160  throw 0;
161  }
162 
163  const codet &code=to_code(symbol.value);
164 
165  source_locationt end_location;
166 
167  if(code.get_statement()==ID_block)
168  end_location=to_code_block(code).end_location();
169  else
170  end_location.make_nil();
171 
172  goto_programt tmp_end_function;
173  goto_programt::targett end_function=tmp_end_function.add_instruction();
174  end_function->type=END_FUNCTION;
175  end_function->source_location=end_location;
176  end_function->code.set(ID_identifier, identifier);
177 
178  targets=targetst();
179  targets.set_return(end_function);
181  f.type.return_type().id()!=ID_empty &&
182  f.type.return_type().id()!=ID_constructor &&
183  f.type.return_type().id()!=ID_destructor;
184 
185  goto_convert_rec(code, f.body);
186 
187  // add non-det return value, if needed
189  add_return(f, end_location);
190 
191  // handle SV-COMP's __VERIFIER_atomic_
192  if(!f.body.instructions.empty() &&
193  has_prefix(id2string(identifier), "__VERIFIER_atomic_"))
194  {
195  goto_programt::instructiont a_begin;
196  a_begin.make_atomic_begin();
197  a_begin.source_location=f.body.instructions.front().source_location;
198  f.body.insert_before_swap(f.body.instructions.begin(), a_begin);
199 
200  goto_programt::targett a_end=f.body.add_instruction();
201  a_end->make_atomic_end();
202  a_end->source_location=end_location;
203 
205  {
206  if(i_it->is_goto() && i_it->get_target()->is_end_function())
207  i_it->set_target(a_end);
208  }
209  }
210 
211  // add "end of function"
212  f.body.destructive_append(tmp_end_function);
213 
214  // do function tags
216  i_it->function=identifier;
217 
218  f.body.update();
219 
220  if(hide(f.body))
221  f.make_hidden();
222 }
223 
226  goto_modelt &goto_model,
228 {
229  goto_convert(symbol_table, goto_model.goto_functions, message_handler);
230  goto_model.symbol_table.swap(symbol_table);
231 }
232 
237 {
238  const unsigned errors_before=
239  message_handler.get_message_count(messaget::M_ERROR);
240 
241  goto_convert_functionst goto_convert_functions(
242  symbol_table, functions, message_handler);
243 
244  try
245  {
246  goto_convert_functions.goto_convert();
247  }
248 
249  catch(int)
250  {
251  goto_convert_functions.error();
252  }
253 
254  catch(const char *e)
255  {
256  goto_convert_functions.error() << e << messaget::eom;
257  }
258 
259  catch(const std::string &e)
260  {
261  goto_convert_functions.error() << e << messaget::eom;
262  }
263 
264  if(message_handler.get_message_count(messaget::M_ERROR)!=errors_before)
265  throw 0;
266 }
267 
269  const irep_idt &identifier,
273 {
274  const unsigned errors_before=
275  message_handler.get_message_count(messaget::M_ERROR);
276 
277  goto_convert_functionst goto_convert_functions(
278  symbol_table, functions, message_handler);
279 
280  try
281  {
282  goto_convert_functions.convert_function(identifier);
283  }
284 
285  catch(int)
286  {
287  goto_convert_functions.error();
288  }
289 
290  catch(const char *e)
291  {
292  goto_convert_functions.error() << e << messaget::eom;
293  }
294 
295  catch(const std::string &e)
296  {
297  goto_convert_functions.error() << e << messaget::eom;
298  }
299 
300  if(message_handler.get_message_count(messaget::M_ERROR)!=errors_before)
301  throw 0;
302 }
const irep_idt & get_statement() const
Definition: std_code.h:37
irep_idt name
The unique identifier.
Definition: symbol.h:46
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
targett add_instruction()
Adds an instruction at the end.
bool is_nil() const
Definition: irep.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
symbol_tablet & symbol_table
#define forall_symbols(it, expr)
Definition: symbol_table.h:28
struct goto_convertt::targetst targets
source_locationt end_location() const
Definition: std_code.h:89
exprt value
Initial value of symbol.
Definition: symbol.h:40
symbol_tablet symbol_table
Definition: goto_model.h:25
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
#define Forall_symbols(it, expr)
Definition: symbol_table.h:32
const irep_idt & id() const
Definition: irep.h:189
instructionst::const_iterator const_targett
symbolst symbols
Definition: symbol_table.h:57
std::string tmp_symbol_prefix
const source_locationt & find_source_location() const
Definition: expr.cpp:466
source_locationt source_location
Definition: message.h:175
The symbol table.
Definition: symbol_table.h:52
Function Inlining.
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1037
goto_function_templatet< goto_programt > goto_functiont
Symbol table.
void goto_convert_rec(const codet &code, goto_programt &dest)
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
typet type
Type of symbol.
Definition: symbol.h:37
Goto Programs with Functions.
static bool hide(const goto_programt &goto_program)
goto_convert_functionst(symbol_tablet &_symbol_table, goto_functionst &_functions, message_handlert &_message_handler)
unsigned temporary_counter
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
void make_nil()
Definition: irep.h:243
mstreamt & error()
Definition: message.h:223
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
const codet & to_code(const exprt &expr)
Definition: std_code.h:49
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:120
void swap(symbol_tablet &other)
Definition: symbol_table.h:80
A statement in a programming language.
Definition: std_code.h:19
void add_return(goto_functionst::goto_functiont &, const source_locationt &)
Return from a function.
Definition: std_code.h:714
Base Type Computation.
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
void set_return(goto_programt::targett _return_target)
void convert_function(const irep_idt &identifier)
message_handlert * message_handler
Definition: message.h:259
goto_functionst goto_functions
Definition: goto_model.h:26
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
unsigned get_message_count(unsigned level) const
Definition: message.h:47