CBMC: /home/runner/work/cbmc/cbmc/src/analyses/ai.h Source File

CBMC
Loading...
Searching...
No Matches
ai.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Abstract Interpretation
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
44
45#ifndef CPROVER_ANALYSES_AI_H
46#define CPROVER_ANALYSES_AI_H
47
48#include <iosfwd>
49#include <memory>
50
51#include <util/deprecate.h>
52#include <util/json.h>
53#include <util/message.h>
54#include <util/xml.h>
55
56#include <goto-programs/goto_model.h>
57
58#include "ai_domain.h"
59#include "ai_history.h"
60#include "ai_storage.h"
61#include "is_threaded.h"
62
115
116 class ai_baset
117{
118public:
125
127 std::unique_ptr<ai_history_factory_baset> &&hf,
128 std::unique_ptr<ai_domain_factory_baset> &&df,
129 std::unique_ptr<ai_storage_baset> &&st,
131 : history_factory(std::move(hf)),
132 domain_factory(std::move(df)),
133 storage(std::move(st)),
135 {
136 }
137
138 virtual ~ai_baset()
139 {
140 }
141
144 const irep_idt &function_id,
145 const goto_programt &goto_program,
146 const namespacet &ns)
147 {
148 goto_functionst goto_functions;
149 initialize(function_id, goto_program);
150 trace_ptrt p = entry_state(goto_program);
151 if(p != nullptr)
152 fixedpoint(p, function_id, goto_program, goto_functions, ns);
153 finalize();
154 }
155
158 const goto_functionst &goto_functions,
159 const namespacet &ns)
160 {
161 initialize(goto_functions);
162 trace_ptrt p = entry_state(goto_functions);
163 if(p != nullptr)
164 fixedpoint(p, goto_functions, ns);
165 finalize();
166 }
167
169 void operator()(const abstract_goto_modelt &goto_model)
170 {
171 const namespacet ns(goto_model.get_symbol_table());
172 initialize(goto_model.get_goto_functions());
173 trace_ptrt p = entry_state(goto_model.get_goto_functions());
174 if(p != nullptr)
175 fixedpoint(p, goto_model.get_goto_functions(), ns);
176 finalize();
177 }
178
181 const irep_idt &function_id,
182 const goto_functionst::goto_functiont &goto_function,
183 const namespacet &ns)
184 {
185 goto_functionst goto_functions;
186 initialize(function_id, goto_function);
187 trace_ptrt p = entry_state(goto_function.body);
188 if(p != nullptr)
189 fixedpoint(p, function_id, goto_function.body, goto_functions, ns);
190 finalize();
191 }
192
202
209{
212 INVARIANT(!l->is_end_function(), "No state after the last instruction");
213 return storage->abstract_traces_before(std::next(l));
214 }
215
229
239{
242 INVARIANT(!l->is_end_function(), "No state after the last instruction");
243 return abstract_state_before(std::next(l));
244 }
245
248{
250 }
251
253{
254 locationt l = p->current_location();
255 INVARIANT(!l->is_end_function(), "No state after the last instruction");
256
257 locationt n = std::next(l);
258
259 auto step_return = p->step(
260 n,
261 *(storage->abstract_traces_before(n)),
263 // Caller history not needed as this is a local step
264
266 }
267
269 virtual void clear()
270 {
271 storage->clear();
272 }
273
280 virtual void output(
281 const namespacet &ns,
282 const irep_idt &function_id,
283 const goto_programt &goto_program,
284 std::ostream &out) const;
285
292 virtual jsont output_json(
293 const namespacet &ns,
294 const irep_idt &function_id,
295 const goto_programt &goto_program) const;
296
303 virtual xmlt output_xml(
304 const namespacet &ns,
305 const irep_idt &function_id,
306 const goto_programt &goto_program) const;
307
309 virtual void output(
310 const namespacet &ns,
311 const goto_functionst &goto_functions,
312 std::ostream &out) const;
313
315 void output(
316 const goto_modelt &goto_model,
317 std::ostream &out) const
318{
319 const namespacet ns(goto_model.symbol_table);
320 output(ns, goto_model.goto_functions, out);
321 }
322
324 void output(
325 const namespacet &ns,
326 const goto_functionst::goto_functiont &goto_function,
327 std::ostream &out) const
328{
329 output(ns, irep_idt(), goto_function.body, out);
330 }
331
333 virtual jsont output_json(
334 const namespacet &ns,
335 const goto_functionst &goto_functions) const;
336
339 const goto_modelt &goto_model) const
340{
341 const namespacet ns(goto_model.symbol_table);
342 return output_json(ns, goto_model.goto_functions);
343 }
344
347 const namespacet &ns,
348 const goto_programt &goto_program) const
349{
350 return output_json(ns, irep_idt(), goto_program);
351 }
352
355 const namespacet &ns,
356 const goto_functionst::goto_functiont &goto_function) const
357{
358 return output_json(ns, irep_idt(), goto_function.body);
359 }
360
362 virtual xmlt output_xml(
363 const namespacet &ns,
364 const goto_functionst &goto_functions) const;
365
368 const goto_modelt &goto_model) const
369{
370 const namespacet ns(goto_model.symbol_table);
371 return output_xml(ns, goto_model.goto_functions);
372 }
373
376 const namespacet &ns,
377 const goto_programt &goto_program) const
378{
379 return output_xml(ns, irep_idt(), goto_program);
380 }
381
384 const namespacet &ns,
385 const goto_functionst::goto_functiont &goto_function) const
386{
387 return output_xml(ns, irep_idt(), goto_function.body);
388 }
389
390protected:
393 virtual void
394 initialize(const irep_idt &function_id, const goto_programt &goto_program);
395
397 virtual void initialize(
398 const irep_idt &function_id,
399 const goto_functionst::goto_functiont &goto_function);
400
403 virtual void initialize(const goto_functionst &goto_functions);
404
407 virtual void finalize();
408
411 trace_ptrt entry_state(const goto_programt &goto_program);
412
415 trace_ptrt entry_state(const goto_functionst &goto_functions);
416
419
422
427
430 virtual bool fixedpoint(
432 const irep_idt &function_id,
433 const goto_programt &goto_program,
434 const goto_functionst &goto_functions,
435 const namespacet &ns);
436
437 virtual void fixedpoint(
439 const goto_functionst &goto_functions,
440 const namespacet &ns);
441
446 virtual bool visit(
447 const irep_idt &function_id,
448 trace_ptrt p,
450 const goto_programt &goto_program,
451 const goto_functionst &goto_functions,
452 const namespacet &ns);
453
454 // function calls and return are special cases
455 // different kinds of analysis handle these differently so these are virtual
456 // visit_function_call handles which function(s) to call,
457 // while visit_edge_function_call handles a single call
458 virtual bool visit_function_call(
459 const irep_idt &function_id,
462 const goto_programt &goto_program,
463 const goto_functionst &goto_functions,
464 const namespacet &ns);
465
466 virtual bool visit_end_function(
467 const irep_idt &function_id,
468 trace_ptrt p,
470 const goto_programt &goto_program,
471 const goto_functionst &goto_functions,
472 const namespacet &ns);
473
474 // The most basic step, computing one edge / transformer application.
475 bool visit_edge(
476 const irep_idt &function_id,
477 trace_ptrt p,
481 const namespacet &ns,
483
484 virtual bool visit_edge_function_call(
490 const goto_programt &callee,
491 const goto_functionst &goto_functions,
492 const namespacet &ns);
493
495 std::unique_ptr<ai_history_factory_baset> history_factory;
496
498 std::unique_ptr<ai_domain_factory_baset> domain_factory;
499
502 virtual bool merge(const statet &src, trace_ptrt from, trace_ptrt to)
503 {
504 statet &dest = get_state(to);
505 return domain_factory->merge(dest, src, from, to);
506 }
507
509 virtual std::unique_ptr<statet> make_temporary_state(const statet &s)
510 {
511 return domain_factory->copy(s);
512 }
513
514 // Domain and history storage
515 std::unique_ptr<ai_storage_baset> storage;
516
520 {
521 return storage->get_state(p, *domain_factory);
522 }
523
524 // Logging
526};
527
528// Perform interprocedural analysis by simply recursing in the interpreter
529// This can lead to a call stack overflow if the domain has a large height
531{
532public:
534 std::unique_ptr<ai_history_factory_baset> &&hf,
535 std::unique_ptr<ai_domain_factory_baset> &&df,
536 std::unique_ptr<ai_storage_baset> &&st,
538 : ai_baset(std::move(hf), std::move(df), std::move(st), mh)
539 {
540 }
541
542protected:
543 // Override the function that handles a single function call edge
550 const goto_programt &callee,
551 const goto_functionst &goto_functions,
552 const namespacet &ns) override;
553};
554
564template <typename domainT>
566{
567public:
568 // constructor
578
579 explicit ait(std::unique_ptr<ai_domain_factory_baset> &&df)
583 std::move(df),
586 {
587 }
588
590
592 // The older interface for non-modifying access
593 // Not recommended as it will throw an exception if a location has not
594 // been reached in an analysis and there is no (other) way of telling
595 // if a location has been reached.
596 DEPRECATED(SINCE(2019, 08, 01, "use abstract_state_{before,after} instead"))
598{
600
601 if(p.use_count() == 1)
602 {
603 // Would be unsafe to return the dereferenced object
604 throw std::out_of_range("failed to find state");
605 }
606
607 return static_cast<const domainT &>(*p);
608 }
609
610protected:
611 // Support the legacy get_state interface which is needed for a few domains
612 // This is one of the few users of the legacy get_state(locationt) method
613 // in location_sensitive_storaget.
614 DEPRECATED(SINCE(2019, 08, 01, "use get_state(trace_ptrt p) instead"))
616 {
617 auto &s = dynamic_cast<location_sensitive_storaget &>(*storage);
618 return s.get_state(l, *domain_factory);
619 }
620
622
623private:
626 void dummy(const domainT &s) { const statet &x=s; (void)x; }
627
628 // To keep the old constructor interface we disable logging
630};
631
653template<typename domainT>
654 class concurrency_aware_ait:public ait<domainT>
655{
656public:
657 using statet = typename ait<domainT>::statet;
658 using locationt = typename statet::locationt;
659
660 // constructor
664 explicit concurrency_aware_ait(std::unique_ptr<ai_domain_factory_baset> &&df)
665 : ait<domainT>(std::move(df))
666 {
667 }
668
669 virtual bool merge_shared(
670 const statet &src,
671 locationt from,
672 locationt to,
673 const namespacet &ns)
674 {
675 statet &dest=this->get_state(to);
676 return static_cast<domainT &>(dest).merge_shared(
677 static_cast<const domainT &>(src), from, to, ns);
678 }
679
680protected:
682
685 const goto_functionst &goto_functions,
686 const namespacet &ns) override
687{
688 ai_baset::fixedpoint(start_trace, goto_functions, ns);
689
690 is_threadedt is_threaded(goto_functions);
691
692 // construct an initial shared state collecting the results of all
693 // functions
695 tmp.add_instruction();
696 goto_programt::const_targett sh_target = tmp.instructions.begin();
700
701 struct wl_entryt
702 {
703 wl_entryt(
704 const irep_idt &_function_id,
707 : function_id(_function_id),
708 goto_program(&_goto_program),
709 location(_location)
710 {
711 }
712
713 irep_idt function_id;
714 const goto_programt *goto_program;
715 locationt location;
716 };
717
718 typedef std::list<wl_entryt> thread_wlt;
720
721 for(const auto &gf_entry : goto_functions.function_map)
722 {
724 {
725 if(is_threaded(t_it))
726 {
727 thread_wl.push_back(
728 wl_entryt(gf_entry.first, gf_entry.second.body, t_it));
729
731 gf_entry.second.body.instructions.end();
732 --l_end;
733
735 }
736 }
737 }
738
739 // now feed in the shared state into all concurrently executing
740 // functions, and iterate until the shared state stabilizes
741 bool new_shared = true;
742 while(new_shared)
743 {
744 new_shared = false;
745
746 for(const auto &wl_entry : thread_wl)
747 {
750 ai_baset::history_factory->epoch(wl_entry.location));
752
755
756 while(!working_set.empty())
757 {
759 goto_programt::const_targett l = p->current_location();
760
762 wl_entry.function_id,
763 p,
765 *(wl_entry.goto_program),
766 goto_functions,
767 ns);
768
769 // the underlying domain must make sure that the final state
770 // carries all possible values; otherwise we would need to
771 // merge over each and every state
772 if(l->is_end_function())
774 }
775 }
776 }
777 }
778};
779
780#endif // CPROVER_ANALYSES_AI_H
Abstract Interpretation Domain.
Abstract Interpretation history.
Abstract Interpretation Storage.
Abstract interface to eager or lazy GOTO models.
virtual const symbol_tablet & get_symbol_table() const =0
Accessor to get the symbol table.
virtual const goto_functionst & get_goto_functions() const =0
Accessor to get a raw goto_functionst.
The common case of history is to only care about where you are now, not how you got there!...
Definition ai_history.h:155
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition ai.h:117
virtual ~ai_baset()
Definition ai.h:138
virtual cstate_ptrt abstract_state_after(const trace_ptrt &p) const
Definition ai.h:252
xmlt output_xml(const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
Output the abstract states for a single function as XML.
Definition ai.h:383
goto_programt::const_targett locationt
Definition ai.h:124
ai_baset(std::unique_ptr< ai_history_factory_baset > &&hf, std::unique_ptr< ai_domain_factory_baset > &&df, std::unique_ptr< ai_storage_baset > &&st, message_handlert &mh)
Definition ai.h:126
void operator()(const goto_functionst &goto_functions, const namespacet &ns)
Run abstract interpretation on a whole program.
Definition ai.h:157
virtual ctrace_set_ptrt abstract_traces_after(locationt l) const
Returns all of the histories that have reached the end of the instruction.
Definition ai.h:208
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:270
std::unique_ptr< ai_storage_baset > storage
Definition ai.h:515
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:519
ai_history_baset::trace_sett trace_sett
Definition ai.h:122
jsont output_json(const namespacet &ns, const goto_programt &goto_program) const
Output the abstract states for a single function as JSON.
Definition ai.h:346
void operator()(const irep_idt &function_id, const goto_programt &goto_program, const namespacet &ns)
Run abstract interpretation on a single function.
Definition ai.h:143
virtual ctrace_set_ptrt abstract_traces_before(locationt l) const
Returns all of the histories that have reached the start of the instruction.
Definition ai.h:198
virtual cstate_ptrt abstract_state_after(locationt l) const
Get a copy of the abstract state after the given instruction, without needing to know what kind of do...
Definition ai.h:238
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:331
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:39
xmlt output_xml(const namespacet &ns, const goto_programt &goto_program) const
Output the abstract states for a single function as XML.
Definition ai.h:375
jsont output_json(const goto_modelt &goto_model) const
Output the abstract states for a whole program as JSON.
Definition ai.h:338
message_handlert & message_handler
Definition ai.h:525
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:523
virtual cstate_ptrt abstract_state_before(const trace_ptrt &p) const
The same interfaces but with histories.
Definition ai.h:247
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:444
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:179
void operator()(const abstract_goto_modelt &goto_model)
Run abstract interpretation on a whole program.
Definition ai.h:169
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:416
void output(const goto_modelt &goto_model, std::ostream &out) const
Output the abstract states for a whole program.
Definition ai.h:315
virtual void clear()
Reset the abstract state.
Definition ai.h:269
std::unique_ptr< ai_domain_factory_baset > domain_factory
For creating domain objects.
Definition ai.h:498
ai_domain_baset statet
Definition ai.h:119
ai_storage_baset::ctrace_set_ptrt ctrace_set_ptrt
Definition ai.h:123
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:197
xmlt output_xml(const goto_modelt &goto_model) const
Output the abstract states for the whole program as XML.
Definition ai.h:367
jsont output_json(const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
Output the abstract states for a single function as JSON.
Definition ai.h:354
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:232
virtual std::unique_ptr< statet > make_temporary_state(const statet &s)
Make a copy of a state.
Definition ai.h:509
ai_history_baset::trace_ptrt trace_ptrt
Definition ai.h:121
void put_in_working_set(working_sett &working_set, trace_ptrt t)
Definition ai.h:423
trace_ptrt get_next(working_sett &working_set)
Get the next location from the work queue.
Definition ai.cpp:214
trace_sett working_sett
The work queue, sorted using the history's ordering operator.
Definition ai.h:418
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:502
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:225
virtual xmlt output_xml(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program) const
Output the abstract states for a single function as XML.
Definition ai.cpp:136
void operator()(const irep_idt &function_id, const goto_functionst::goto_functiont &goto_function, const namespacet &ns)
Run abstract interpretation on a single function.
Definition ai.h:180
void output(const namespacet &ns, const goto_functionst::goto_functiont &goto_function, std::ostream &out) const
Output the abstract states for a function.
Definition ai.h:324
virtual jsont output_json(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program) const
Output the abstract states for a single function as JSON.
Definition ai.cpp:83
std::unique_ptr< ai_history_factory_baset > history_factory
For creating history objects.
Definition ai.h:495
virtual void finalize()
Override this to add a cleanup or post-processing step after fixedpoint has run.
Definition ai.cpp:209
ai_storage_baset::cstate_ptrt cstate_ptrt
Definition ai.h:120
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition ai_domain.h:54
goto_programt::const_targett locationt
Definition ai_domain.h:72
Definition ai_domain.h:223
std::shared_ptr< const ai_history_baset > trace_ptrt
History objects are intended to be immutable so they can be shared to reduce memory overhead.
Definition ai_history.h:43
static const trace_ptrt no_caller_history
Definition ai_history.h:121
std::set< trace_ptrt, compare_historyt > trace_sett
Definition ai_history.h:79
An easy factory implementation for histories that don't need parameters.
Definition ai_history.h:255
Definition ai.h:531
ai_recursive_interproceduralt(std::unique_ptr< ai_history_factory_baset > &&hf, std::unique_ptr< ai_domain_factory_baset > &&df, std::unique_ptr< ai_storage_baset > &&st, message_handlert &mh)
Definition ai.h:533
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:542
std::shared_ptr< const trace_sett > ctrace_set_ptrt
Definition ai_storage.h:54
std::shared_ptr< const statet > cstate_ptrt
Definition ai_storage.h:49
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
ait(std::unique_ptr< ai_domain_factory_baset > &&df)
Definition ai.h:579
goto_programt::const_targett locationt
Definition ai.h:589
null_message_handlert no_logging
Definition ai.h:629
void dummy(const domainT &s)
This function exists to enforce that domainT is derived from ai_domain_baset.
Definition ai.h:626
virtual statet & get_state(locationt l)
Definition ai.h:615
ait()
Definition ai.h:569
Base class for concurrency-aware abstract interpretation.
Definition ai.h:655
ai_baset::working_sett working_sett
Definition ai.h:681
concurrency_aware_ait(std::unique_ptr< ai_domain_factory_baset > &&df)
Definition ai.h:664
virtual bool merge_shared(const statet &src, locationt from, locationt to, const namespacet &ns)
Definition ai.h:669
concurrency_aware_ait()
Definition ai.h:661
void fixedpoint(ai_baset::trace_ptrt start_trace, const goto_functionst &goto_functions, const namespacet &ns) override
Definition ai.h:683
typename statet::locationt locationt
Definition ai.h:658
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
Definition goto_model.h:27
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
A generic container class for the GOTO intermediate representation of one function.
Definition goto_program.h:72
instructionst::const_iterator const_targett
Definition goto_program.h:614
Definition is_threaded.h:22
Definition json.h:27
The most conventional storage; one domain per location.
Definition ai_storage.h:154
statet & get_state(trace_ptrt p, const ai_domain_factory_baset &fac) override
Look up the analysis state for a given history, instantiating a new domain if required.
Definition ai_storage.h:193
Definition message.h:27
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Definition message.h:76
Definition xml.h:21
#define SINCE(year, month, day, msg)
Definition deprecate.h:26
#define DEPRECATED(msg)
Definition deprecate.h:23
Symbol Table + CFG.
#define forall_goto_program_instructions(it, program)
Over-approximate Concurrency for Threaded Goto Programs.
STL namespace.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
dstringt irep_idt

AltStyle によって変換されたページ (->オリジナル) /