CBMC
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/std_code.h>
15 
17 
18 #include "goto_model.h"
19 
21  symbol_table_baset &_symbol_table,
22  message_handlert &_message_handler)
23  : goto_convertt(_symbol_table, _message_handler)
24 {
25 }
26 
28 {
29 }
30 
32 {
33  // warning! hash-table iterators are not stable
34 
35  typedef std::list<irep_idt> symbol_listt;
36  symbol_listt symbol_list;
37 
38  for(const auto &symbol_pair : symbol_table.symbols)
39  {
40  if(
41  !symbol_pair.second.is_type && !symbol_pair.second.is_macro &&
42  symbol_pair.second.type.id() == ID_code &&
43  (symbol_pair.second.mode == ID_C || symbol_pair.second.mode == ID_cpp ||
44  symbol_pair.second.mode == ID_java ||
45  symbol_pair.second.mode == ID_statement_list))
46  {
47  symbol_list.push_back(symbol_pair.first);
48  }
49  }
50 
51  for(const auto &id : symbol_list)
52  {
53  convert_function(id, functions.function_map[id]);
54  }
55 
56  functions.compute_location_numbers();
57 
58 // this removes the parse tree of the bodies from memory
59 #if 0
60  for(const auto &symbol_pair, symbol_table.symbols)
61  {
62  if(!symbol_pair.second.is_type &&
63  symbol_pair.second.type.id()==ID_code &&
64  symbol_pair.second.value.is_not_nil())
65  {
66  symbol_pair.second.value=codet();
67  }
68  }
69 #endif
70 }
71 
73 {
74  for(const auto &instruction : goto_program.instructions)
75  {
76  for(const auto &label : instruction.labels)
77  {
78  if(label == CPROVER_PREFIX "HIDE")
79  return true;
80  }
81  }
82 
83  return false;
84 }
85 
88  const typet &return_type,
89  const source_locationt &source_location)
90 {
91 #if 0
92  if(!f.body.instructions.empty() &&
93  f.body.instructions.back().is_return())
94  return; // not needed, we have one already
95 
96  // see if we have an unconditional goto at the end
97  if(!f.body.instructions.empty() &&
98  f.body.instructions.back().is_goto() &&
99  f.body.instructions.back().guard.is_true())
100  return;
101 #else
102 
103  if(!f.body.instructions.empty())
104  {
105  goto_programt::const_targett last_instruction = 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() && last_instruction->condition().is_true())
112  {
113  return;
114  }
115 
116  // return?
117  if(last_instruction->is_set_return_value())
118  return;
119 
120  // advance if it's a 'dead' without branch target
121  if(
122  last_instruction->is_dead() &&
123  last_instruction != f.body.instructions.begin() &&
124  !last_instruction->is_target())
125  last_instruction--;
126  else
127  break; // give up
128  }
129  }
130 
131 #endif
132 
133  side_effect_expr_nondett rhs(return_type, source_location);
134 
135  f.body.add(
136  goto_programt::make_set_return_value(std::move(rhs), 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  // store the parameter identifiers in the goto functions
153  const code_typet &code_type = to_code_type(symbol.type);
154  f.set_parameter_identifiers(code_type);
155 
156  if(
157  symbol.value.is_nil() ||
158  symbol.is_compiled()) /* goto_inline may have removed the body */
159  return;
160 
161  // we have a body, make sure all parameter names are valid
162  for(const auto &p : f.parameter_identifiers)
163  {
165  !p.empty(),
166  "parameter identifier should not be empty",
167  "function:",
168  identifier);
169 
172  "parameter identifier must be a known symbol",
173  "function:",
174  identifier,
175  "parameter:",
176  p);
177  }
178 
179  lifetimet parent_lifetime = lifetime;
182 
183  const codet &code = to_code(symbol.value);
184 
185  source_locationt end_location;
186 
187  if(code.get_statement() == ID_block)
188  end_location = to_code_block(code).end_location();
189  else
190  end_location.make_nil();
191 
192  goto_programt tmp_end_function;
193  goto_programt::targett end_function =
194  tmp_end_function.add(goto_programt::make_end_function(end_location));
195 
196  targets = targetst();
197  targets.prefix = &f.body;
198  targets.suffix = &tmp_end_function;
199  targets.set_return(end_function);
200  targets.has_return_value = code_type.return_type().id() != ID_empty &&
201  code_type.return_type().id() != ID_constructor &&
202  code_type.return_type().id() != ID_destructor;
203 
204  goto_convert_rec(code, f.body, mode);
205 
206  // add non-det return value, if needed
208  add_return(f, code_type.return_type(), end_location);
209 
210  // handle SV-COMP's __VERIFIER_atomic_
211  if(
212  !f.body.instructions.empty() &&
213  identifier.starts_with("__VERIFIER_atomic_"))
214  {
216  f.body.instructions.front().source_location());
217  f.body.insert_before_swap(f.body.instructions.begin(), a_begin);
218 
219  goto_programt::targett a_end =
220  f.body.add(goto_programt::make_atomic_end(end_location));
221 
222  for(auto &instruction : f.body.instructions)
223  {
224  if(instruction.is_goto() && instruction.get_target()->is_end_function())
225  instruction.set_target(a_end);
226  }
227  }
228 
229  // add "end of function"
230  f.body.destructive_append(tmp_end_function);
231 
232  f.body.update();
233 
234  if(hide(f.body))
235  f.make_hidden();
236 
237  lifetime = parent_lifetime;
238 
239  targets.prefix = nullptr;
240  targets.suffix = nullptr;
241 }
242 
243 void goto_convert(goto_modelt &goto_model, message_handlert &message_handler)
244 {
245  symbol_table_buildert symbol_table_builder =
247 
248  goto_convert(
249  symbol_table_builder, goto_model.goto_functions, message_handler);
250 }
251 
253  symbol_table_baset &symbol_table,
254  goto_functionst &functions,
255  message_handlert &message_handler)
256 {
257  symbol_table_buildert symbol_table_builder =
258  symbol_table_buildert::wrap(symbol_table);
259 
260  goto_convert_functionst goto_convert_functions(
261  symbol_table_builder, message_handler);
262 
263  goto_convert_functions.goto_convert(functions);
264 }
265 
267  const irep_idt &identifier,
268  symbol_table_baset &symbol_table,
269  goto_functionst &functions,
270  message_handlert &message_handler)
271 {
272  symbol_table_buildert symbol_table_builder =
273  symbol_table_buildert::wrap(symbol_table);
274 
275  goto_convert_functionst goto_convert_functions(
276  symbol_table_builder, message_handler);
277 
278  goto_convert_functions.convert_function(
279  identifier, functions.function_map[identifier]);
280 }
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:583
const typet & return_type() const
Definition: std_types.h:689
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:38
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
Definition: dstring.h:95
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:31
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:181
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:622
static instructiont make_set_return_value(exprt return_value, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:874
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
instructionst::iterator targett
Definition: goto_program.h:614
instructionst::const_iterator const_targett
Definition: goto_program.h:615
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:990
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:979
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:739
const irep_idt & id() const
Definition: irep.h:384
void make_nil()
Definition: irep.h:442
bool is_nil() const
Definition: irep.h:364
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:148
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:113
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
#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:40
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition: invariant.h:535
#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:788
void set_return(goto_programt::targett _return_target)