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