cprover
goto_convert_functions.cpp
Go to the documentation of this file.
1/********************************************************************\
2
3Module: Goto Programs with Functions
4
5Author: Daniel Kroening
6
7Date: June 2003
8
9\*******************************************************************/
10
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
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
245void goto_convert(goto_modelt &goto_model, message_handlert &message_handler)
246{
247 symbol_table_buildert symbol_table_builder =
249
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
void make_nil()
Definition: irep.h:454
const irep_idt & id() const
Definition: irep.h:396
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.