cprover
Loading...
Searching...
No Matches
ai.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Abstract Interpretation
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "ai.h"
13
14#include <memory>
15#include <sstream>
16#include <type_traits>
17
18#include <util/invariant.h>
19#include <util/std_code.h>
20
22 const namespacet &ns,
23 const goto_functionst &goto_functions,
24 std::ostream &out) const
25{
26 for(const auto &gf_entry : goto_functions.function_map)
27 {
28 if(gf_entry.second.body_available())
29 {
30 out << "////\n";
31 out << "//// Function: " << gf_entry.first << "\n";
32 out << "////\n";
33 out << "\n";
34
35 output(ns, gf_entry.first, gf_entry.second.body, out);
36 }
37 }
38}
39
41 const namespacet &ns,
42 const irep_idt &function_id,
43 const goto_programt &goto_program,
44 std::ostream &out) const
45{
47 {
48 out << "**** " << i_it->location_number << " " << i_it->source_location()
49 << "\n";
50
51 abstract_state_before(i_it)->output(out, *this, ns);
52 out << "\n";
53 #if 1
54 goto_program.output_instruction(ns, function_id, out, *i_it);
55 out << "\n";
56 #endif
57 }
58}
59
61 const namespacet &ns,
62 const goto_functionst &goto_functions) const
63{
64 json_objectt result;
65
66 for(const auto &gf_entry : goto_functions.function_map)
67 {
68 if(gf_entry.second.body_available())
69 {
70 result[id2string(gf_entry.first)] =
71 output_json(ns, gf_entry.first, gf_entry.second.body);
72 }
73 else
74 {
75 result[id2string(gf_entry.first)] = json_arrayt();
76 }
77 }
78
79 return std::move(result);
80}
81
83 const namespacet &ns,
84 const irep_idt &function_id,
85 const goto_programt &goto_program) const
86{
88
90 {
91 // Ideally we need output_instruction_json
92 std::ostringstream out;
93 goto_program.output_instruction(ns, function_id, out, *i_it);
94
95 json_objectt location{
96 {"locationNumber", json_numbert(std::to_string(i_it->location_number))},
97 {"sourceLocation", json_stringt(i_it->source_location().as_string())},
98 {"abstractState", abstract_state_before(i_it)->output_json(*this, ns)},
99 {"instruction", json_stringt(out.str())}};
100
101 contents.push_back(std::move(location));
102 }
103
104 return std::move(contents);
105}
106
108 const namespacet &ns,
109 const goto_functionst &goto_functions) const
110{
111 xmlt program("program");
112
113 for(const auto &gf_entry : goto_functions.function_map)
114 {
115 xmlt function(
116 "function",
117 {{"name", id2string(gf_entry.first)},
118 {"body_available", gf_entry.second.body_available() ? "true" : "false"}},
119 {});
120
121 if(gf_entry.second.body_available())
122 {
123 function.new_element(
124 output_xml(ns, gf_entry.first, gf_entry.second.body));
125 }
126
127 program.new_element(function);
128 }
129
130 return program;
131}
132
134 const namespacet &ns,
135 const irep_idt &function_id,
136 const goto_programt &goto_program) const
137{
139
141 {
142 xmlt location(
143 "",
144 {{"location_number", std::to_string(i_it->location_number)},
145 {"source_location", i_it->source_location().as_string()}},
146 {abstract_state_before(i_it)->output_xml(*this, ns)});
147
148 // Ideally we need output_instruction_xml
149 std::ostringstream out;
150 goto_program.output_instruction(ns, function_id, out, *i_it);
151 location.set_attribute("instruction", out.str());
152
153 function_body.new_element(location);
154 }
155
156 return function_body;
157}
158
161{
162 // find the 'entry function'
163
164 goto_functionst::function_mapt::const_iterator
165 f_it=goto_functions.function_map.find(goto_functions.entry_point());
166
167 if(f_it!=goto_functions.function_map.end())
168 return entry_state(f_it->second.body);
169
170 // It is not clear if this is even a well-structured goto_functionst object
171 return nullptr;
172}
173
175{
176 // The first instruction of 'goto_program' is the entry point
177 trace_ptrt p = history_factory->epoch(goto_program.instructions.begin());
178 get_state(p).make_entry();
179 return p;
180}
181
183 const irep_idt &function_id,
184 const goto_functionst::goto_functiont &goto_function)
185{
186 initialize(function_id, goto_function.body);
187}
188
189void ai_baset::initialize(const irep_idt &, const goto_programt &goto_program)
190{
191 // Domains are created and set to bottom on access.
192 // So we do not need to set them to be bottom before hand.
193}
194
195void ai_baset::initialize(const goto_functionst &goto_functions)
196{
197 for(const auto &gf_entry : goto_functions.function_map)
198 initialize(gf_entry.first, gf_entry.second);
199}
200
202{
203 // Nothing to do per default
204}
205
207{
208 PRECONDITION(!working_set.empty());
209
210 static_assert(
211 std::is_same<
213 std::set<trace_ptrt, ai_history_baset::compare_historyt>>::value,
214 "begin must return the minimal entry");
215 auto first = working_set.begin();
216
217 trace_ptrt t = *first;
218
219 working_set.erase(first);
220
221 return t;
222}
223
226 const irep_idt &function_id,
227 const goto_programt &goto_program,
228 const goto_functionst &goto_functions,
229 const namespacet &ns)
230{
231 PRECONDITION(start_trace != nullptr);
232
235
236 bool new_data=false;
237
238 while(!working_set.empty())
239 {
241
242 // goto_program is really only needed for iterator manipulation
243 if(visit(function_id, p, working_set, goto_program, goto_functions, ns))
244 new_data=true;
245 }
246
247 return new_data;
248}
249
252 const goto_functionst &goto_functions,
253 const namespacet &ns)
254{
255 goto_functionst::function_mapt::const_iterator f_it =
256 goto_functions.function_map.find(goto_functions.entry_point());
257
258 if(f_it != goto_functions.function_map.end())
259 fixedpoint(start_trace, f_it->first, f_it->second.body, goto_functions, ns);
260}
261
263 const irep_idt &function_id,
264 trace_ptrt p,
266 const goto_programt &goto_program,
267 const goto_functionst &goto_functions,
268 const namespacet &ns)
269{
270 bool new_data=false;
271 locationt l = p->current_location();
273
274 log.progress() << "ai_baset::visit " << l->location_number << " in "
275 << function_id << messaget::eom;
276
277 // Function call and end are special cases
278 if(l->is_function_call())
279 {
281 goto_program.get_successors(l).size() == 1,
282 "function calls only have one successor");
283
285 *(goto_program.get_successors(l).begin()) == std::next(l),
286 "function call successor / return location must be the next instruction");
287
289 function_id, p, working_set, goto_program, goto_functions, ns);
290 }
291 else if(l->is_end_function())
292 {
294 goto_program.get_successors(l).empty(),
295 "The end function instruction should have no successors.");
296
298 function_id, p, working_set, goto_program, goto_functions, ns);
299 }
300 else
301 {
302 // Successors can be empty, for example assume(0).
303 // Successors can contain duplicates, for example GOTO next;
304 for(const auto &to_l : goto_program.get_successors(l))
305 {
306 if(to_l == goto_program.instructions.end())
307 continue;
308
310 function_id,
311 p,
312 function_id,
313 to_l,
315 ns,
316 working_set); // Local steps so no caller history needed
317 }
318 }
319
320 return new_data;
321}
322
324 const irep_idt &function_id,
325 trace_ptrt p,
329 const namespacet &ns,
331{
333 log.progress() << "ai_baset::visit_edge from "
334 << p->current_location()->location_number << " to "
335 << to_l->location_number << "... ";
336
337 // Has history taught us not to step here...
338 auto next =
339 p->step(to_l, *(storage->abstract_traces_before(to_l)), caller_history);
341 {
342 log.progress() << "blocked by history" << messaget::eom;
343 return false;
344 }
345 else if(next.first == ai_history_baset::step_statust::NEW)
346 {
347 log.progress() << "gives a new history... ";
348 }
349 else
350 {
351 log.progress() << "merges with existing history... ";
352 }
353 trace_ptrt to_p = next.second;
354
355 // Abstract domains are mutable so we must copy before we transform
356 statet &current = get_state(p);
357
358 std::unique_ptr<statet> tmp_state(make_temporary_state(current));
360
361 // Apply transformer
362 log.progress() << "applying transformer... ";
363 new_values.transform(function_id, p, to_function_id, to_p, *this, ns);
364
365 // Expanding a domain means that it has to be analysed again
366 // Likewise if the history insists that it is a new trace
367 // (assuming it is actually reachable).
368 log.progress() << "merging... ";
369 bool return_value = false;
370 if(
371 merge(new_values, p, to_p) ||
373 !new_values.is_bottom()))
374 {
376 log.progress() << "result queued." << messaget::eom;
377 return_value = true;
378 }
379 else
380 {
381 log.progress() << "domain unchanged." << messaget::eom;
382 }
383
384 // Branch because printing some histories and domains can be expensive
385 // esp. if the output is then just discarded and this is a critical path.
387 {
388 log.debug() << "p = ";
389 p->output(log.debug());
390 log.debug() << messaget::eom;
391
392 log.debug() << "current = ";
393 current.output(log.debug(), *this, ns);
394 log.debug() << messaget::eom;
395
396 log.debug() << "to_p = ";
397 to_p->output(log.debug());
398 log.debug() << messaget::eom;
399
400 log.debug() << "new_values = ";
401 new_values.output(log.debug(), *this, ns);
402 log.debug() << messaget::eom;
403 }
404
405 return return_value;
406}
407
412 const irep_idt &,
414 const goto_programt &,
415 const goto_functionst &,
416 const namespacet &ns)
417{
419 log.progress() << "ai_baset::visit_edge_function_call from "
420 << p_call->current_location()->location_number << " to "
421 << l_return->location_number << messaget::eom;
422
423 // The default implementation is not interprocedural
424 // so the effects of the call are approximated but nothing else
425 return visit_edge(
427 p_call,
429 l_return,
431 no_caller_history, // Not needed as we are skipping the function call
432 ns,
434}
435
440 const goto_programt &caller,
441 const goto_functionst &goto_functions,
442 const namespacet &ns)
443{
444 locationt l_call = p_call->current_location();
445
446 PRECONDITION(l_call->is_function_call());
447
449 log.progress() << "ai_baset::visit_function_call at "
450 << l_call->location_number << messaget::eom;
451
452 locationt l_return = std::next(l_call);
453
454 // operator() allows analysis of a single goto_program independently
455 // it generates a synthetic goto_functions object for this
456 if(!goto_functions.function_map.empty())
457 {
458 const exprt &callee_expression = l_call->call_function();
459
460 if(callee_expression.id() == ID_symbol)
461 {
464
465 log.progress() << "Calling " << callee_function_id << messaget::eom;
466
467 goto_functionst::function_mapt::const_iterator it =
468 goto_functions.function_map.find(callee_function_id);
469
471 it != goto_functions.function_map.end(),
472 "Function " + id2string(callee_function_id) + "not in function map");
473
475
476 if(callee_fun.body_available())
477 {
480 p_call,
481 l_return,
484 callee_fun.body,
485 goto_functions,
486 ns);
487 }
488 else
489 {
490 // Fall through to the default, body not available, case
491 }
492 }
493 else
494 {
495 // Function pointers are not currently supported and must be removed
498 "Function pointers and indirect calls must be removed before "
499 "analysis.");
500 }
501 }
502
503 // If the body is not available then we just do the edge from call to return
504 // in the caller. Domains should over-approximate what the function might do.
505 return visit_edge(
507 p_call,
509 l_return,
510 ai_history_baset::no_caller_history, // Would be the same as p_call...
511 ns,
513}
514
516 const irep_idt &function_id,
517 trace_ptrt p,
519 const goto_programt &goto_program,
520 const goto_functionst &goto_functions,
521 const namespacet &ns)
522{
523 locationt l = p->current_location();
524 PRECONDITION(l->is_end_function());
525
527 log.progress() << "ai_baset::visit_end_function " << function_id
528 << messaget::eom;
529
530 // Do nothing
531 return false;
532}
533
540 const goto_programt &callee,
541 const goto_functionst &goto_functions,
542 const namespacet &ns)
543{
545 log.progress() << "ai_recursive_interproceduralt::visit_edge_function_call"
546 << " from " << p_call->current_location()->location_number
547 << " to " << l_return->location_number << messaget::eom;
548
549 // This is the edge from call site to function head.
550 {
551 locationt l_begin = callee.instructions.begin();
552
553 working_sett catch_working_set; // The trace from the next fixpoint
554
555 // Do the edge from the call site to the beginning of the function
556 bool new_data = visit_edge(
558 p_call,
560 l_begin,
562 no_caller_history, // Not needed as p_call already has the info
563 ns,
565
566 log.progress() << "Handle " << callee_function_id << " recursively"
567 << messaget::eom;
568
569 // do we need to do/re-do the fixedpoint of the body?
570 if(new_data)
574 callee,
575 goto_functions,
576 ns);
577 }
578
579 // This is the edge from function end to return site.
580 {
581 log.progress() << "Handle return edges" << messaget::eom;
582
583 // get location at end of the procedure we have called
584 locationt l_end = --callee.instructions.end();
586 l_end->is_end_function(),
587 "The last instruction of a goto_program must be END_FUNCTION");
588
589 // Find the histories for a location
590 auto traces = storage->abstract_traces_before(l_end);
591
592 bool new_data = false;
593
594 // The history used may mean there are multiple histories at the end of the
595 // function. Some of these can be progressed (for example, if the history
596 // tracks paths within functions), some can't be (for example, not all
597 // calling contexts will be appropriate). We rely on the history's step,
598 // called from visit_edge to prune as applicable.
599 for(auto p_end : *traces)
600 {
601 // do edge from end of function to instruction after call
603
604 if(!end_state.is_bottom())
605 {
606 // function exit point reachable in that history
607
610 p_end,
612 l_return,
613 p_call, // To allow function-local history
614 ns,
616 }
617 }
618
619 return new_data;
620 }
621}
Abstract Interpretation.
goto_programt::const_targett locationt
Definition ai.h:126
virtual bool visit(const irep_idt &function_id, trace_ptrt p, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
Perform one step of abstract interpretation from trace t Depending on the instruction type it may com...
Definition ai.cpp:262
virtual jsont output_json(const namespacet &ns, const goto_functionst &goto_functions) const
Output the abstract states for the whole program as JSON.
Definition ai.cpp:60
std::unique_ptr< ai_storage_baset > storage
Definition ai.h:513
virtual xmlt output_xml(const namespacet &ns, const goto_functionst &goto_functions) const
Output the abstract states for the whole program as XML.
Definition ai.cpp:107
virtual statet & get_state(trace_ptrt p)
Get the state for the given history, creating it with the factory if it doesn't exist.
Definition ai.h:517
bool visit_edge(const irep_idt &function_id, trace_ptrt p, const irep_idt &to_function_id, locationt to_l, trace_ptrt caller_history, const namespacet &ns, working_sett &working_set)
Definition ai.cpp:323
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
message_handlert & message_handler
Definition ai.h:523
virtual bool visit_end_function(const irep_idt &function_id, trace_ptrt p, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
Definition ai.cpp:515
virtual bool visit_function_call(const irep_idt &function_id, trace_ptrt p_call, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
Definition ai.cpp:436
trace_ptrt entry_state(const goto_programt &goto_program)
Set the abstract state of the entry location of a single function to the entry state required by the ...
Definition ai.cpp:174
virtual bool visit_edge_function_call(const irep_idt &calling_function_id, trace_ptrt p_call, locationt l_return, const irep_idt &callee_function_id, working_sett &working_set, const goto_programt &callee, const goto_functionst &goto_functions, const namespacet &ns)
Definition ai.cpp:408
virtual void initialize(const irep_idt &function_id, const goto_programt &goto_program)
Initialize all the abstract states for a single function.
Definition ai.cpp:189
virtual bool fixedpoint(trace_ptrt starting_trace, const irep_idt &function_id, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
Run the fixedpoint algorithm until it reaches a fixed point.
Definition ai.cpp:224
virtual std::unique_ptr< statet > make_temporary_state(const statet &s)
Make a copy of a state.
Definition ai.h:507
ai_history_baset::trace_ptrt trace_ptrt
Definition ai.h:123
void put_in_working_set(working_sett &working_set, trace_ptrt t)
Definition ai.h:421
trace_ptrt get_next(working_sett &working_set)
Get the next location from the work queue.
Definition ai.cpp:206
trace_sett working_sett
The work queue, sorted using the history's ordering operator.
Definition ai.h:416
virtual bool merge(const statet &src, trace_ptrt from, trace_ptrt to)
Merge the state src, flowing from tracet from to tracet to, into the state currently stored for trace...
Definition ai.h:500
virtual cstate_ptrt abstract_state_before(locationt l) const
Get a copy of the abstract state before the given instruction, without needing to know what kind of d...
Definition ai.h:223
std::unique_ptr< ai_history_factory_baset > history_factory
For creating history objects.
Definition ai.h:493
virtual void finalize()
Override this to add a cleanup or post-processing step after fixedpoint has run.
Definition ai.cpp:201
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition ai_domain.h:55
virtual void output(std::ostream &, const ai_baset &, const namespacet &) const
Definition ai_domain.h:105
A history object is an abstraction / representation of the control-flow part of a set of traces.
Definition ai_history.h:37
static const trace_ptrt no_caller_history
Definition ai_history.h:121
bool visit_edge_function_call(const irep_idt &calling_function_id, trace_ptrt p_call, locationt l_return, const irep_idt &callee_function_id, working_sett &working_set, const goto_programt &callee, const goto_functionst &goto_functions, const namespacet &ns) override
Definition ai.cpp:534
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
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
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.
Definition json.h:27
unsigned get_verbosity() const
Definition message.h:54
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
mstreamt & debug() const
Definition message.h:429
mstreamt & progress() const
Definition message.h:424
@ M_DEBUG
Definition message.h:171
static eomt eom
Definition message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
const irep_idt & get_identifier() const
Definition std_expr.h:109
Definition xml.h:21
xmlt & new_element(const std::string &key)
Definition xml.h:95
#define forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:510
#define PRECONDITION(CONDITION)
Definition invariant.h:463
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189