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 <util/prefix.h>
14 #include <util/std_code.h>
15 #include <util/symbol_table.h>
17 
19 
20 #include "goto_model.h"
21 
23  symbol_table_baset &_symbol_table,
24  message_handlert &_message_handler)
25  : goto_convertt(_symbol_table, _message_handler)
26 {
27 }
28 
30 {
31 }
32 
34 {
35  // warning! hash-table iterators are not stable
36 
37  typedef std::list<irep_idt> symbol_listt;
38  symbol_listt symbol_list;
39 
40  for(const auto &symbol_pair : symbol_table.symbols)
41  {
42  if(
43  !symbol_pair.second.is_type && !symbol_pair.second.is_macro &&
44  symbol_pair.second.type.id() == ID_code &&
45  (symbol_pair.second.mode == ID_C || symbol_pair.second.mode == ID_cpp ||
46  symbol_pair.second.mode == ID_java ||
47  symbol_pair.second.mode == "jsil" ||
48  symbol_pair.second.mode == ID_statement_list))
49  {
50  symbol_list.push_back(symbol_pair.first);
51  }
52  }
53 
54  for(const auto &id : symbol_list)
55  {
56  convert_function(id, functions.function_map[id]);
57  }
58 
59  functions.compute_location_numbers();
60 
61 // this removes the parse tree of the bodies from memory
62 #if 0
63  for(const auto &symbol_pair, symbol_table.symbols)
64  {
65  if(!symbol_pair.second.is_type &&
66  symbol_pair.second.type.id()==ID_code &&
67  symbol_pair.second.value.is_not_nil())
68  {
69  symbol_pair.second.value=codet();
70  }
71  }
72 #endif
73 }
74 
76 {
77  for(const auto &instruction : goto_program.instructions)
78  {
79  for(const auto &label : instruction.labels)
80  {
81  if(label == CPROVER_PREFIX "HIDE")
82  return true;
83  }
84  }
85 
86  return false;
87 }
88 
91  const typet &return_type,
92  const source_locationt &source_location)
93 {
94 #if 0
95  if(!f.body.instructions.empty() &&
96  f.body.instructions.back().is_return())
97  return; // not needed, we have one already
98 
99  // see if we have an unconditional goto at the end
100  if(!f.body.instructions.empty() &&
101  f.body.instructions.back().is_goto() &&
102  f.body.instructions.back().guard.is_true())
103  return;
104 #else
105 
106  if(!f.body.instructions.empty())
107  {
108  goto_programt::const_targett last_instruction = f.body.instructions.end();
109  last_instruction--;
110 
111  while(true)
112  {
113  // unconditional goto, say from while(1)?
114  if(
115  last_instruction->is_goto() &&
116  last_instruction->get_condition().is_true())
117  {
118  return;
119  }
120 
121  // return?
122  if(last_instruction->is_set_return_value())
123  return;
124 
125  // advance if it's a 'dead' without branch target
126  if(
127  last_instruction->is_dead() &&
128  last_instruction != f.body.instructions.begin() &&
129  !last_instruction->is_target())
130  last_instruction--;
131  else
132  break; // give up
133  }
134  }
135 
136 #endif
137 
138  side_effect_expr_nondett rhs(return_type, source_location);
139 
140  f.body.add(
141  goto_programt::make_set_return_value(std::move(rhs), source_location));
142 }
143 
145  const irep_idt &identifier,
147 {
148  const symbolt &symbol = ns.lookup(identifier);
149  const irep_idt mode = symbol.mode;
150 
151  if(f.body_available())
152  return; // already converted
153 
154  // make tmp variables local to function
155  tmp_symbol_prefix = id2string(symbol.name) + "::$tmp";
156 
157  // store the parameter identifiers in the goto functions
158  const code_typet &code_type = to_code_type(symbol.type);
159  f.set_parameter_identifiers(code_type);
160 
161  if(
162  symbol.value.is_nil() ||
163  symbol.is_compiled()) /* goto_inline may have removed the body */
164  return;
165 
166  // we have a body, make sure all parameter names are valid
167  for(const auto &p : f.parameter_identifiers)
168  {
170  !p.empty(),
171  "parameter identifier should not be empty",
172  "function:",
173  identifier);
174 
177  "parameter identifier must be a known symbol",
178  "function:",
179  identifier,
180  "parameter:",
181  p);
182  }
183 
184  lifetimet parent_lifetime = lifetime;
187 
188  const codet &code = to_code(symbol.value);
189 
190  source_locationt end_location;
191 
192  if(code.get_statement() == ID_block)
193  end_location = to_code_block(code).end_location();
194  else
195  end_location.make_nil();
196 
197  goto_programt tmp_end_function;
198  goto_programt::targett end_function =
199  tmp_end_function.add(goto_programt::make_end_function(end_location));
200 
201  targets = targetst();
202  targets.set_return(end_function);
203  targets.has_return_value = code_type.return_type().id() != ID_empty &&
204  code_type.return_type().id() != ID_constructor &&
205  code_type.return_type().id() != ID_destructor;
206 
207  goto_convert_rec(code, f.body, mode);
208 
209  // add non-det return value, if needed
211  add_return(f, code_type.return_type(), end_location);
212 
213  // handle SV-COMP's __VERIFIER_atomic_
214  if(
215  !f.body.instructions.empty() &&
216  has_prefix(id2string(identifier), "__VERIFIER_atomic_"))
217  {
220  a_begin.source_location_nonconst() =
221  f.body.instructions.front().source_location();
222  f.body.insert_before_swap(f.body.instructions.begin(), a_begin);
223 
224  goto_programt::targett a_end =
225  f.body.add(goto_programt::make_atomic_end(end_location));
226 
227  for(auto &instruction : f.body.instructions)
228  {
229  if(instruction.is_goto() && instruction.get_target()->is_end_function())
230  instruction.set_target(a_end);
231  }
232  }
233 
234  // add "end of function"
235  f.body.destructive_append(tmp_end_function);
236 
237  f.body.update();
238 
239  if(hide(f.body))
240  f.make_hidden();
241 
242  lifetime = parent_lifetime;
243 }
244 
245 void goto_convert(goto_modelt &goto_model, message_handlert &message_handler)
246 {
247  symbol_table_buildert symbol_table_builder =
249 
250  goto_convert(
251  symbol_table_builder, goto_model.goto_functions, message_handler);
252 }
253 
255  symbol_table_baset &symbol_table,
256  goto_functionst &functions,
257  message_handlert &message_handler)
258 {
259  symbol_table_buildert symbol_table_builder =
260  symbol_table_buildert::wrap(symbol_table);
261 
262  goto_convert_functionst goto_convert_functions(
263  symbol_table_builder, message_handler);
264 
265  goto_convert_functions.goto_convert(functions);
266 }
267 
269  const irep_idt &identifier,
270  symbol_table_baset &symbol_table,
271  goto_functionst &functions,
272  message_handlert &message_handler)
273 {
274  symbol_table_buildert symbol_table_builder =
275  symbol_table_buildert::wrap(symbol_table);
276 
277  goto_convert_functionst goto_convert_functions(
278  symbol_table_builder, message_handler);
279 
280  goto_convert_functions.convert_function(
281  identifier, functions.function_map[identifier]);
282 }
lifetimet
Selects the kind of objects allocated.
@ STATIC_GLOBAL
Allocate global objects with static lifetime.
@ AUTOMATIC_LOCAL
Allocate local objects with automatic lifetime.
source_locationt end_location() const
Definition: std_code.h:187
Base type of functions.
Definition: std_types.h:539
const typet & return_type() const
Definition: std_types.h:645
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
const irep_idt & get_statement() const
Definition: std_code_base.h:65
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
goto_convert_functionst(symbol_table_baset &_symbol_table, message_handlert &_message_handler)
void add_return(goto_functionst::goto_functiont &, const typet &return_type, const source_locationt &)
void goto_convert(goto_functionst &functions)
void convert_function(const irep_idt &identifier, goto_functionst::goto_functiont &result)
static bool hide(const goto_programt &)
symbol_table_baset & symbol_table
void goto_convert_rec(const codet &code, goto_programt &dest, const irep_idt &mode)
std::string tmp_symbol_prefix
struct goto_convertt::targetst targets
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
void compute_location_numbers()
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
source_locationt & source_location_nonconst()
Definition: goto_program.h:337
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
static instructiont make_set_return_value(exprt return_value, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:863
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:986
instructionst::iterator targett
Definition: goto_program.h:592
instructionst::const_iterator const_targett
Definition: goto_program.h:593
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:975
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:964
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:715
const irep_idt & id() const
Definition: irep.h:396
void make_nil()
Definition: irep.h:454
irept & add(const irep_idt &name)
Definition: irep.cpp:116
bool is_nil() const
Definition: irep.h:376
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1520
The symbol table base class interface.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Author: Diffblue Ltd.
static symbol_table_buildert wrap(symbol_table_baset &base_symbol_table)
Symbol table entry.
Definition: symbol.h:28
bool is_compiled() const
Returns true iff the the symbol's value has been compiled to a goto program.
Definition: symbol.h:107
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
The type of an expression, extends irept.
Definition: type.h:29
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
#define CPROVER_PREFIX
void goto_convert(goto_modelt &goto_model, message_handlert &message_handler)
Goto Programs with Functions.
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition: invariant.h:511
#define INITIALIZE_FUNCTION
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:203
const codet & to_code(const exprt &expr)
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
void set_return(goto_programt::targett _return_target)
Author: Diffblue Ltd.