cprover
Loading...
Searching...
No Matches
static_analysis.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Value Set Propagation
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#define USE_DEPRECATED_STATIC_ANALYSIS_H
13#include "static_analysis.h"
14
15#include <memory>
16
17#include <util/expr_util.h>
18#include <util/pointer_expr.h>
19#include <util/std_code.h>
20
21#include "is_threaded.h"
22
24 locationt from,
25 locationt to)
26{
27 if(!from->is_goto())
28 return true_exprt();
29 else if(std::next(from) == to)
30 return boolean_negate(from->get_condition());
31 else
32 return from->get_condition();
33}
34
36{
37 // get predecessor of "to"
38
39 to--;
40
41 if(to->is_end_function())
42 return static_cast<const exprt &>(get_nil_irep());
43
44 // must be the function call
45 assert(to->is_function_call());
46
47 return to->call_lhs();
48}
49
51 const goto_functionst &goto_functions)
52{
53 initialize(goto_functions);
54 fixedpoint(goto_functions);
55}
56
58 const irep_idt &function_identifier,
59 const goto_programt &goto_program)
60{
61 initialize(goto_program);
62 goto_functionst goto_functions;
63 fixedpoint(function_identifier, goto_program, goto_functions);
64}
65
67 const goto_functionst &goto_functions,
68 std::ostream &out) const
69{
70 for(const auto &gf_entry : goto_functions.function_map)
71 {
72 if(gf_entry.second.body_available())
73 {
74 out << "////\n";
75 out << "//// Function: " << gf_entry.first << "\n";
76 out << "////\n";
77 out << "\n";
78
79 output(gf_entry.second.body, gf_entry.first, out);
80 }
81 }
82}
83
85 const goto_programt &goto_program,
86 const irep_idt &,
87 std::ostream &out) const
88{
90 {
91 out << "**** " << i_it->location_number << " " << i_it->source_location()
92 << "\n";
93
94 get_state(i_it).output(ns, out);
95 out << "\n";
96 #if 0
97 goto_program.output_instruction(ns, identifier, out, i_it);
98 out << "\n";
99 #endif
100 }
101}
102
104 const goto_functionst &goto_functions)
105{
106 for(const auto &gf_entry : goto_functions.function_map)
107 generate_states(gf_entry.second.body);
108}
109
116
118 const goto_functionst &goto_functions)
119{
120 for(const auto &gf_entry : goto_functions.function_map)
121 update(gf_entry.second.body);
122}
123
125 const goto_programt &goto_program)
126{
127 locationt previous;
128 bool first=true;
129
131 {
132 // do we have it already?
133 if(!has_location(i_it))
134 {
136
137 if(!first)
138 merge(get_state(i_it), get_state(previous), i_it);
139 }
140
141 first=false;
142 previous=i_it;
143 }
144}
145
148{
149 assert(!working_set.empty());
150
151 working_sett::iterator i=working_set.begin();
152 locationt l=i->second;
153 working_set.erase(i);
154
155 return l;
156}
157
159 const irep_idt &function_identifier,
160 const goto_programt &goto_program,
161 const goto_functionst &goto_functions)
162{
163 if(goto_program.instructions.empty())
164 return false;
165
167
170 goto_program.instructions.begin());
171
172 bool new_data=false;
173
174 while(!working_set.empty())
175 {
177
178 if(visit(function_identifier, l, working_set, goto_program, goto_functions))
179 new_data=true;
180 }
181
182 return new_data;
183}
184
186 const irep_idt &function_identifier,
187 locationt l,
189 const goto_programt &goto_program,
190 const goto_functionst &goto_functions)
191{
192 bool new_data=false;
193
194 statet &current=get_state(l);
195
196 current.seen=true;
197
198 for(const auto &to_l : goto_program.get_successors(l))
199 {
200 if(to_l==goto_program.instructions.end())
201 continue;
202
203 std::unique_ptr<statet> tmp_state(
204 make_temporary_state(current));
205
207
208 if(l->is_function_call())
209 {
210 // this is a big special case
212 function_identifier,
213 l,
214 to_l,
215 l->call_function(),
216 l->call_arguments(),
218 goto_functions);
219 }
220 else
221 new_values.transform(
222 ns, function_identifier, l, function_identifier, to_l);
223
224 statet &other=get_state(to_l);
225
226 bool have_new_values=
227 merge(other, new_values, to_l);
228
230 new_data=true;
231
232 if(have_new_values || !other.seen)
234 }
235
236 return new_data;
237}
238
240 const irep_idt &calling_function,
243 const goto_functionst &goto_functions,
244 const goto_functionst::function_mapt::const_iterator f_it,
245 const exprt::operandst &,
247{
248 const goto_functionst::goto_functiont &goto_function=f_it->second;
249
250 if(!goto_function.body_available())
251 return; // do nothing
252
253 assert(!goto_function.body.instructions.empty());
254
255 {
256 // get the state at the beginning of the function
257 locationt l_begin=goto_function.body.instructions.begin();
258
259 // do the edge from the call site to the beginning of the function
260 std::unique_ptr<statet> tmp_state(make_temporary_state(new_state));
261 tmp_state->transform(ns, calling_function, l_call, f_it->first, l_begin);
262
264
265 bool new_data=false;
266
267 // merge the new stuff
269 new_data=true;
270
271 // do each function at least once
272 if(functions_done.find(f_it->first)==
273 functions_done.end())
274 {
275 new_data=true;
276 functions_done.insert(f_it->first);
277 }
278
279 // do we need to do the fixedpoint of the body?
280 if(new_data)
281 {
282 // recursive call
283 fixedpoint(f_it->first, goto_function.body, goto_functions);
284 }
285 }
286
287 {
288 // get location at end of procedure
289 locationt l_end=--goto_function.body.instructions.end();
290
291 assert(l_end->is_end_function());
292
293 statet &end_of_function=get_state(l_end);
294
295 // do edge from end of function to instruction after call
296 std::unique_ptr<statet> tmp_state(
297 make_temporary_state(end_of_function));
298 tmp_state->transform(ns, f_it->first, l_end, calling_function, l_return);
299
300 // propagate those -- not exceedingly precise, this is,
301 // as still it contains all the state from the
302 // call site
304 }
305
306 {
307 // effect on current procedure (if any)
308 new_state.transform(
309 ns, calling_function, l_call, calling_function, l_return);
310 }
311}
312
314 const irep_idt &calling_function,
317 const exprt &function,
318 const exprt::operandst &arguments,
320 const goto_functionst &goto_functions)
321{
322 // see if we have the functions at all
323 if(goto_functions.function_map.empty())
324 return;
325
326 if(function.id()==ID_symbol)
327 {
328 const irep_idt &identifier = to_symbol_expr(function).get_identifier();
329
330 if(recursion_set.find(identifier)!=recursion_set.end())
331 {
332 // recursion detected!
333 return;
334 }
335 else
336 recursion_set.insert(identifier);
337
338 goto_functionst::function_mapt::const_iterator it=
339 goto_functions.function_map.find(identifier);
340
341 if(it==goto_functions.function_map.end())
342 throw "failed to find function "+id2string(identifier);
343
345 calling_function,
346 l_call,
347 l_return,
348 goto_functions,
349 it,
350 arguments,
351 new_state);
352
353 recursion_set.erase(identifier);
354 }
355 else if(function.id()==ID_if)
356 {
357 if(function.operands().size()!=3)
358 throw "if takes three arguments";
359
360 std::unique_ptr<statet> n2(make_temporary_state(new_state));
361
363 calling_function,
364 l_call,
365 l_return,
366 to_if_expr(function).true_case(),
367 arguments,
368 new_state,
369 goto_functions);
370
372 calling_function,
373 l_call,
374 l_return,
375 to_if_expr(function).false_case(),
376 arguments,
377 *n2,
378 goto_functions);
379
381 }
382 else if(function.id()==ID_dereference)
383 {
384 // get value set
385 std::list<exprt> values;
386 get_reference_set(l_call, function, values);
387
388 std::unique_ptr<statet> state_from(make_temporary_state(new_state));
389
390 // now call all of these
391 for(const auto &value : values)
392 {
393 if(value.id()==ID_object_descriptor)
394 {
396 std::unique_ptr<statet> n2(make_temporary_state(new_state));
398 calling_function,
399 l_call,
400 l_return,
401 o.object(),
402 arguments,
403 *n2,
404 goto_functions);
406 }
407 }
408 }
409 else if(function.id() == ID_null_object ||
410 function.id() == ID_integer_address)
411 {
412 // ignore, can't be a function
413 }
414 else if(function.id()==ID_member || function.id()==ID_index)
415 {
416 // ignore, can't be a function
417 }
418 else if(function.id()=="builtin-function")
419 {
420 // ignore, someone else needs to worry about this
421 }
422 else
423 {
424 throw "unexpected function_call argument: "+
425 function.id_string();
426 }
427}
428
430 const goto_functionst &goto_functions)
431{
432 // do each function at least once
433
434 for(const auto &gf_entry : goto_functions.function_map)
435 {
436 if(functions_done.insert(gf_entry.first).second)
437 fixedpoint(gf_entry.first, gf_entry.second.body, goto_functions);
438 }
439}
440
442 const goto_functionst &goto_functions)
443{
444 sequential_fixedpoint(goto_functions);
445
446 is_threadedt is_threaded(goto_functions);
447
448 // construct an initial shared state collecting the results of all
449 // functions
451 tmp.add_instruction();
452 goto_programt::const_targett sh_target=tmp.instructions.begin();
455
456 struct wl_entryt
457 {
458 wl_entryt(
462 : function_identifier(_function_identifier),
463 goto_program(&_goto_program),
464 location(_location)
465 {
466 }
467
468 irep_idt function_identifier;
469 const goto_programt *goto_program;
470 locationt location;
471 };
472
473 typedef std::list<wl_entryt> thread_wlt;
475
476 for(const auto &gf_entry : goto_functions.function_map)
477 {
479 {
480 if(is_threaded(t_it))
481 {
482 thread_wl.push_back(
483 wl_entryt(gf_entry.first, gf_entry.second.body, t_it));
484
486 gf_entry.second.body.instructions.end();
487 --l_end;
488
491 }
492 }
493 }
494
495 // new feed in the shared state into all concurrently executing
496 // functions, and iterate until the shared state stabilizes
497 bool new_shared=true;
498 while(new_shared)
499 {
500 new_shared=false;
501
502 for(const auto &thread : thread_wl)
503 {
505 put_in_working_set(working_set, thread.location);
506
507 statet &begin_state = get_state(thread.location);
508 merge(begin_state, shared_state, thread.location);
509
510 while(!working_set.empty())
511 {
513
514 visit(
515 thread.function_identifier,
516 l,
518 *thread.goto_program,
519 goto_functions);
520
521 // the underlying domain must make sure that the final state
522 // carries all possible values; otherwise we would need to
523 // merge over each and every state
524 if(l->is_end_function())
525 {
528 }
529 }
530 }
531 }
532}
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
operandst & operands()
Definition expr.h:92
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.
instructionst::const_iterator const_targett
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
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.
const namespacet & ns
virtual std::unique_ptr< statet > make_temporary_state(statet &s)=0
void generate_states(const goto_functionst &goto_functions)
void do_function_call(const irep_idt &calling_function, locationt l_call, locationt l_return, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, statet &new_state)
locationt get_next(working_sett &working_set)
virtual bool has_location(locationt l) const =0
bool visit(const irep_idt &function_identifier, locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions)
bool fixedpoint(const irep_idt &function_identifier, const goto_programt &goto_program, const goto_functionst &goto_functions)
virtual void get_reference_set(locationt l, const exprt &expr, std::list< exprt > &dest)=0
void put_in_working_set(working_sett &working_set, locationt l)
void sequential_fixedpoint(const goto_functionst &goto_functions)
void concurrent_fixedpoint(const goto_functionst &goto_functions)
virtual void operator()(const irep_idt &function_identifier, const goto_programt &goto_program)
static exprt get_return_lhs(locationt to)
virtual void generate_state(locationt l)=0
virtual void update(const goto_programt &goto_program)
void do_function_call_rec(const irep_idt &calling_function, locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions)
static exprt get_guard(locationt from, locationt to)
functions_donet functions_done
virtual statet & get_state(locationt l)=0
virtual void initialize(const goto_programt &goto_program)
std::map< unsigned, locationt > working_sett
goto_programt::const_targett locationt
virtual bool merge_shared(statet &a, const statet &b, locationt to)=0
virtual bool merge(statet &a, const statet &b, locationt to)=0
virtual void output(const goto_functionst &goto_functions, std::ostream &out) const
recursion_sett recursion_set
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.
#define forall_goto_program_instructions(it, program)
const irept & get_nil_irep()
Definition irep.cpp:20
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
Over-approximate Concurrency for Threaded Goto Programs.
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.
Static Analysis.
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