cprover
Loading...
Searching...
No Matches
flow_insensitive_analysis.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Flow Insensitive Static Analysis
4
5Author: Daniel Kroening, kroening@kroening.com
6 CM Wintersteiger
7
8\*******************************************************************/
9
12
14
15#include <util/expr_util.h>
16#include <util/pointer_expr.h>
17#include <util/std_code.h>
18
20 locationt from,
21 locationt to) const
22{
23 if(!from->is_goto())
24 return true_exprt();
25 else if(std::next(from) == to)
26 return boolean_negate(from->get_condition());
27 else
28 return from->get_condition();
29}
30
32{
33 // get predecessor of "to"
34 to--;
35
36 if(to->is_end_function())
37 return static_cast<const exprt &>(get_nil_irep());
38
39 // must be the function call
40 return to->call_lhs();
41}
42
44 const goto_functionst &goto_functions)
45{
46 initialize(goto_functions);
47 fixedpoint(goto_functions);
48}
49
51operator()(const irep_idt &function_id, const goto_programt &goto_program)
52{
53 initialize(goto_program);
54 goto_functionst goto_functions;
55 fixedpoint(function_id, goto_program, goto_functions);
56}
57
59 const goto_functionst &goto_functions,
60 std::ostream &out)
61{
62 for(const auto &gf_entry : goto_functions.function_map)
63 {
64 out << "////\n"
65 << "//// Function: " << gf_entry.first << "\n////\n\n";
66
67 output(gf_entry.first, gf_entry.second.body, out);
68 }
69}
70
72 const irep_idt &,
73 const goto_programt &,
74 std::ostream &out)
75{
76 get_state().output(ns, out);
77}
78
82{
83 assert(!working_set.empty());
84
85// working_sett::iterator i=working_set.begin();
86// locationt l=i->second;
87// working_set.erase(i);
88
89// pop_heap(working_set.begin(), working_set.end());
90 locationt l=working_set.top();
91 working_set.pop();
92
93 return l;
94}
95
97 const irep_idt &function_id,
98 const goto_programt &goto_program,
99 const goto_functionst &goto_functions)
100{
101 if(goto_program.instructions.empty())
102 return false;
103
105
106// make_heap(working_set.begin(), working_set.end());
107
110 goto_program.instructions.begin());
111
112 bool new_data=false;
113
114 while(!working_set.empty())
115 {
117
118 if(visit(function_id, l, working_set, goto_program, goto_functions))
119 new_data=true;
120 }
121
122 return new_data;
123}
124
126 const irep_idt &function_id,
127 locationt l,
129 const goto_programt &goto_program,
130 const goto_functionst &goto_functions)
131{
132 bool new_data=false;
133
134 #if 0
135 std::cout << "Visiting: " << l->function << " " <<
136 l->location_number << '\n';
137 #endif
138
139 seen_locations.insert(l);
140 if(statistics.find(l)==statistics.end())
141 statistics[l]=1;
142 else
143 statistics[l]++;
144
145 for(const auto &to_l : goto_program.get_successors(l))
146 {
147 if(to_l==goto_program.instructions.end())
148 continue;
149
150 bool changed=false;
151
152 if(l->is_function_call())
153 {
154 // this is a big special case
155 changed = do_function_call_rec(
156 function_id,
157 l,
158 l->call_function(),
159 l->call_arguments(),
160 get_state(),
161 goto_functions);
162 }
163 else
164 changed = get_state().transform(ns, function_id, l, function_id, to_l);
165
166 if(changed || !seen(to_l))
167 {
168 new_data=true;
170 }
171 }
172
173// if (id2string(l->function).find("debug")!=std::string::npos)
174// std::cout << l->function << '\n'; //=="messages::debug")
175
176// {
177// static unsigned state_cntr=0;
178// std::string s("pastate"); s += std::to_string(state_cntr);
179// std::ofstream f(s.c_str());
180// goto_program.output_instruction(ns, "", f, l);
181// f << '\n';
182// get_state().output(ns, f);
183// f.close();
184// state_cntr++;
185// }
186
187 return new_data;
188}
189
191 const irep_idt &calling_function,
193 const goto_functionst &goto_functions,
194 const goto_functionst::function_mapt::const_iterator f_it,
195 const exprt::operandst &,
196 statet &state)
197{
198 const goto_functionst::goto_functiont &goto_function=f_it->second;
199
200 if(!goto_function.body_available())
201 {
203
206 l_call->call_lhs().type(), l_call->source_location())));
207 r->location_number=0;
208
210 t->location_number=1;
211
213 // do the edge from the call site to the simulated function (the artificial
214 // return statement that we just generated)
215 bool new_data =
216 state.transform(ns, calling_function, l_call, f_it->first, r);
217 // do the edge from the return to the artificial end-of-function
218 new_data = state.transform(ns, f_it->first, r, f_it->first, t) || new_data;
219 // do edge from (artificial) end of function to instruction after call
220 new_data =
221 state.transform(ns, f_it->first, t, calling_function, l_next) || new_data;
222
223 return new_data;
224 }
225
226 assert(!goto_function.body.instructions.empty());
227
228 bool new_data=false;
229
230 {
231 // get the state at the beginning of the function
232 locationt l_begin=goto_function.body.instructions.begin();
233
234 // do the edge from the call site to the beginning of the function
235 new_data =
236 state.transform(ns, calling_function, l_call, f_it->first, l_begin);
237
238 // do each function at least once
239 if(functions_done.find(f_it->first)==
240 functions_done.end())
241 {
242 new_data=true;
243 functions_done.insert(f_it->first);
244 }
245
246 // do we need to do the fixedpoint of the body?
247 if(new_data)
248 {
249 // recursive call
250 fixedpoint(f_it->first, goto_function.body, goto_functions);
251 new_data=true; // could be reset by fixedpoint
252 }
253 }
254
255 {
256 // get location at end of procedure
257 locationt l_end=--goto_function.body.instructions.end();
258
259 assert(l_end->is_end_function());
260
261 // do edge from end of function to instruction after call
263 l_next++;
264 new_data =
265 state.transform(ns, f_it->first, l_end, calling_function, l_next) ||
266 new_data;
267 }
268
269 return new_data;
270}
271
273 const irep_idt &calling_function,
275 const exprt &function,
276 const exprt::operandst &arguments,
277 statet &state,
278 const goto_functionst &goto_functions)
279{
280 bool new_data = false;
281
282 if(function.id()==ID_symbol)
283 {
284 const irep_idt &identifier = to_symbol_expr(function).get_identifier();
285
286 if(recursion_set.find(identifier)!=recursion_set.end())
287 {
288 // recursion detected!
289 return false;
290 }
291 else
292 recursion_set.insert(identifier);
293
294 goto_functionst::function_mapt::const_iterator it=
295 goto_functions.function_map.find(identifier);
296
297 if(it==goto_functions.function_map.end())
298 throw "failed to find function "+id2string(identifier);
299
301 calling_function, l_call, goto_functions, it, arguments, state);
302
303 recursion_set.erase(identifier);
304 }
305 else if(function.id()==ID_if)
306 {
307 const auto &if_expr = to_if_expr(function);
308
310 calling_function,
311 l_call,
312 if_expr.true_case(),
313 arguments,
314 state,
315 goto_functions);
316
318 calling_function,
319 l_call,
320 if_expr.false_case(),
321 arguments,
322 state,
323 goto_functions) ||
324 new_data;
325 }
326 else if(function.id()==ID_dereference)
327 {
328 // get value set
329 expr_sett values;
330
331 get_reference_set(function, values);
332
333 // now call all of these
334 for(const auto &v : values)
335 {
336 if(v.id()==ID_object_descriptor)
337 {
339
340 // ... but only if they are actually functions.
341 goto_functionst::function_mapt::const_iterator it=
342 goto_functions.function_map.find(o.object().get(ID_identifier));
343
344 if(it!=goto_functions.function_map.end())
345 {
347 calling_function,
348 l_call,
349 o.object(),
350 arguments,
351 state,
352 goto_functions) ||
353 new_data;
354 }
355 }
356 }
357 }
358 else if(function.id() == ID_null_object)
359 {
360 // ignore, can't be a function
361 }
362 else if(function.id()==ID_member || function.id()==ID_index)
363 {
364 // ignore, can't be a function
365 }
366 else if(function.id()=="builtin-function")
367 {
368 // ignore
369 }
370 else
371 {
372 throw "unexpected function_call argument: "+
373 function.id_string();
374 }
375 return new_data;
376}
377
379 const goto_functionst &goto_functions)
380{
381 // do each function at least once
382
383 for(const auto &gf_entry : goto_functions.function_map)
384 {
385 if(functions_done.find(gf_entry.first) == functions_done.end())
386 {
387 functions_done.insert(gf_entry.first);
388 fixedpoint(gf_entry.first, gf_entry.second.body, goto_functions);
389 }
390 }
391}
392
394{
395 // no need to copy value sets around
396}
397
399{
400 // no need to copy value sets around
401}
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition ai.cpp:40
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
exprt get_guard(locationt from, locationt to) const
virtual bool transform(const namespacet &ns, const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to)=0
virtual void output(const goto_functionst &goto_functions, std::ostream &out)
virtual void operator()(const irep_idt &function_id, const goto_programt &goto_program)
virtual void get_reference_set(const exprt &expr, expr_sett &expr_set)=0
locationt get_next(working_sett &working_set)
bool fixedpoint(const irep_idt &function_id, const goto_programt &goto_program, const goto_functionst &goto_functions)
bool visit(const irep_idt &function_id, locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions)
virtual void update(const goto_programt &goto_program)
flow_insensitive_abstract_domain_baset::expr_sett expr_sett
bool do_function_call_rec(const irep_idt &calling_function, locationt l_call, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions)
goto_programt::const_targett locationt
virtual void initialize(const goto_programt &)
std::priority_queue< locationt > working_sett
std::map< locationt, unsigned > statistics
void put_in_working_set(working_sett &working_set, locationt l)
bool do_function_call(const irep_idt &calling_function, locationt l_call, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, statet &new_state)
virtual statet & get_state()=0
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
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
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:45
const std::string & id_string() const
Definition irep.h:399
const irep_idt & id() const
Definition irep.h:396
Split an expression into a base object and a (byte) offset.
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
const irep_idt & get_identifier() const
Definition std_expr.h:109
The Boolean constant true.
Definition std_expr.h:2856
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Deprecated expression utility functions.
Flow Insensitive Static Analysis.
const irept & get_nil_irep()
Definition irep.cpp:20
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
static int8_t r
Definition irep_hash.h:60
API to expression classes for Pointers.
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2291
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189