cprover
Loading...
Searching...
No Matches
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>
16
18
19#include "goto_model.h"
20
22 symbol_table_baset &_symbol_table,
23 message_handlert &_message_handler)
24 : goto_convertt(_symbol_table, _message_handler)
25{
26}
27
31
33{
34 // warning! hash-table iterators are not stable
35
36 typedef std::list<irep_idt> symbol_listt;
37 symbol_listt symbol_list;
38
39 for(const auto &symbol_pair : symbol_table.symbols)
40 {
41 if(
42 !symbol_pair.second.is_type && !symbol_pair.second.is_macro &&
43 symbol_pair.second.type.id() == ID_code &&
44 (symbol_pair.second.mode == ID_C || symbol_pair.second.mode == ID_cpp ||
45 symbol_pair.second.mode == ID_java ||
46 symbol_pair.second.mode == "jsil" ||
47 symbol_pair.second.mode == ID_statement_list))
48 {
49 symbol_list.push_back(symbol_pair.first);
50 }
51 }
52
53 for(const auto &id : symbol_list)
54 {
55 convert_function(id, functions.function_map[id]);
56 }
57
58 functions.compute_location_numbers();
59
60// this removes the parse tree of the bodies from memory
61#if 0
62 for(const auto &symbol_pair, symbol_table.symbols)
63 {
64 if(!symbol_pair.second.is_type &&
65 symbol_pair.second.type.id()==ID_code &&
66 symbol_pair.second.value.is_not_nil())
67 {
68 symbol_pair.second.value=codet();
69 }
70 }
71#endif
72}
73
75{
76 for(const auto &instruction : goto_program.instructions)
77 {
78 for(const auto &label : instruction.labels)
79 {
80 if(label == CPROVER_PREFIX "HIDE")
81 return true;
82 }
83 }
84
85 return false;
86}
87
90 const typet &return_type,
91 const source_locationt &source_location)
92{
93#if 0
94 if(!f.body.instructions.empty() &&
95 f.body.instructions.back().is_return())
96 return; // not needed, we have one already
97
98 // see if we have an unconditional goto at the end
99 if(!f.body.instructions.empty() &&
100 f.body.instructions.back().is_goto() &&
101 f.body.instructions.back().guard.is_true())
102 return;
103#else
104
105 if(!f.body.instructions.empty())
106 {
107 goto_programt::const_targett last_instruction = f.body.instructions.end();
108 last_instruction--;
109
110 while(true)
111 {
112 // unconditional goto, say from while(1)?
113 if(last_instruction->is_goto() && last_instruction->condition().is_true())
114 {
115 return;
116 }
117
118 // return?
119 if(last_instruction->is_set_return_value())
120 return;
121
122 // advance if it's a 'dead' without branch target
123 if(
124 last_instruction->is_dead() &&
125 last_instruction != f.body.instructions.begin() &&
126 !last_instruction->is_target())
127 last_instruction--;
128 else
129 break; // give up
130 }
131 }
132
133#endif
134
135 side_effect_expr_nondett rhs(return_type, source_location);
136
137 f.body.add(
138 goto_programt::make_set_return_value(std::move(rhs), source_location));
139}
140
142 const irep_idt &identifier,
144{
145 const symbolt &symbol = ns.lookup(identifier);
146 const irep_idt mode = symbol.mode;
147
148 if(f.body_available())
149 return; // already converted
150
151 // make tmp variables local to function
152 tmp_symbol_prefix = id2string(symbol.name) + "::$tmp";
153
154 // store the parameter identifiers in the goto functions
155 const code_typet &code_type = to_code_type(symbol.type);
156 f.set_parameter_identifiers(code_type);
157
158 if(
159 symbol.value.is_nil() ||
160 symbol.is_compiled()) /* goto_inline may have removed the body */
161 return;
162
163 // we have a body, make sure all parameter names are valid
164 for(const auto &p : f.parameter_identifiers)
165 {
167 !p.empty(),
168 "parameter identifier should not be empty",
169 "function:",
170 identifier);
171
174 "parameter identifier must be a known symbol",
175 "function:",
176 identifier,
177 "parameter:",
178 p);
179 }
180
181 lifetimet parent_lifetime = lifetime;
184
185 const codet &code = to_code(symbol.value);
186
187 source_locationt end_location;
188
189 if(code.get_statement() == ID_block)
190 end_location = to_code_block(code).end_location();
191 else
192 end_location.make_nil();
193
194 goto_programt tmp_end_function;
195 goto_programt::targett end_function =
196 tmp_end_function.add(goto_programt::make_end_function(end_location));
197
198 targets = targetst();
199 targets.prefix = &f.body;
200 targets.suffix = &tmp_end_function;
201 targets.set_return(end_function);
202 targets.has_return_value = code_type.return_type().id() != ID_empty &&
203 code_type.return_type().id() != ID_constructor &&
204 code_type.return_type().id() != ID_destructor;
205
206 goto_convert_rec(code, f.body, mode);
207
208 // add non-det return value, if needed
210 add_return(f, code_type.return_type(), end_location);
211
212 // handle SV-COMP's __VERIFIER_atomic_
213 if(
214 !f.body.instructions.empty() &&
215 has_prefix(id2string(identifier), "__VERIFIER_atomic_"))
216 {
218 f.body.instructions.front().source_location());
219 f.body.insert_before_swap(f.body.instructions.begin(), a_begin);
220
222 f.body.add(goto_programt::make_atomic_end(end_location));
223
224 for(auto &instruction : f.body.instructions)
225 {
226 if(instruction.is_goto() && instruction.get_target()->is_end_function())
227 instruction.set_target(a_end);
228 }
229 }
230
231 // add "end of function"
232 f.body.destructive_append(tmp_end_function);
233
234 f.body.update();
235
236 if(hide(f.body))
237 f.make_hidden();
238
239 lifetime = parent_lifetime;
240
241 targets.prefix = nullptr;
242 targets.suffix = nullptr;
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.
const irep_idt & get_statement() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
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
void compute_location_numbers()
::goto_functiont goto_functiont
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.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
static instructiont make_set_return_value(exprt return_value, const source_locationt &l=source_locationt::nil())
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
instructionst::iterator targett
instructionst::const_iterator const_targett
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
void make_nil()
Definition irep.h:454
const irep_idt & id() const
Definition irep.h:396
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().
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
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: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:744
void set_return(goto_programt::targett _return_target)