cprover
ai.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Abstract Interpretation
4 
5 Author: 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 <map>
50 #include <memory>
51 
52 #include <util/json.h>
53 #include <util/xml.h>
54 #include <util/expr.h>
55 #include <util/make_unique.h>
56 
58 
59 #include "ai_domain.h"
60 #include "ai_history.h"
61 #include "ai_storage.h"
62 #include "is_threaded.h"
63 
117 
118 class ai_baset
119 {
120 public:
127 
129  std::unique_ptr<ai_history_factory_baset> &&hf,
130  std::unique_ptr<ai_domain_factory_baset> &&df,
131  std::unique_ptr<ai_storage_baset> &&st)
132  : history_factory(std::move(hf)),
133  domain_factory(std::move(df)),
134  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  fixedpoint(p, function_id, goto_program, goto_functions, ns);
152  finalize();
153  }
154 
157  const goto_functionst &goto_functions,
158  const namespacet &ns)
159  {
160  initialize(goto_functions);
161  trace_ptrt p = entry_state(goto_functions);
162  fixedpoint(p, goto_functions, ns);
163  finalize();
164  }
165 
167  void operator()(const abstract_goto_modelt &goto_model)
168  {
169  const namespacet ns(goto_model.get_symbol_table());
170  initialize(goto_model.get_goto_functions());
171  trace_ptrt p = entry_state(goto_model.get_goto_functions());
172  fixedpoint(p, goto_model.get_goto_functions(), ns);
173  finalize();
174  }
175 
178  const irep_idt &function_id,
179  const goto_functionst::goto_functiont &goto_function,
180  const namespacet &ns)
181  {
182  goto_functionst goto_functions;
183  initialize(function_id, goto_function);
184  trace_ptrt p = entry_state(goto_function.body);
185  fixedpoint(p, function_id, goto_function.body, goto_functions, ns);
186  finalize();
187  }
188 
195  {
196  return storage->abstract_traces_before(l);
197  }
198 
205  {
208  INVARIANT(!l->is_end_function(), "No state after the last instruction");
209  return storage->abstract_traces_before(std::next(l));
210  }
211 
222  {
223  return storage->abstract_state_before(l, *domain_factory);
224  }
225 
235  {
238  INVARIANT(!l->is_end_function(), "No state after the last instruction");
239  return abstract_state_before(std::next(l));
240  }
241 
244  {
245  return storage->abstract_state_before(p, *domain_factory);
246  }
247 
249  {
250  locationt l = p->current_location();
251  INVARIANT(!l->is_end_function(), "No state after the last instruction");
252 
253  locationt n = std::next(l);
254 
255  auto step_return = p->step(n, *(storage->abstract_traces_before(n)));
256 
257  return storage->abstract_state_before(step_return.second, *domain_factory);
258  }
259 
261  virtual void clear()
262  {
263  storage->clear();
264  }
265 
272  virtual void output(
273  const namespacet &ns,
274  const irep_idt &function_id,
275  const goto_programt &goto_program,
276  std::ostream &out) const;
277 
279  virtual void output(
280  const namespacet &ns,
281  const goto_functionst &goto_functions,
282  std::ostream &out) const;
283 
285  void output(
286  const goto_modelt &goto_model,
287  std::ostream &out) const
288  {
289  const namespacet ns(goto_model.symbol_table);
290  output(ns, goto_model.goto_functions, out);
291  }
292 
294  void output(
295  const namespacet &ns,
296  const goto_functionst::goto_functiont &goto_function,
297  std::ostream &out) const
298  {
299  output(ns, irep_idt(), goto_function.body, out);
300  }
301 
303  virtual jsont output_json(
304  const namespacet &ns,
305  const goto_functionst &goto_functions) const;
306 
309  const goto_modelt &goto_model) const
310  {
311  const namespacet ns(goto_model.symbol_table);
312  return output_json(ns, goto_model.goto_functions);
313  }
314 
317  const namespacet &ns,
318  const goto_programt &goto_program) const
319  {
320  return output_json(ns, irep_idt(), goto_program);
321  }
322 
325  const namespacet &ns,
326  const goto_functionst::goto_functiont &goto_function) const
327  {
328  return output_json(ns, irep_idt(), goto_function.body);
329  }
330 
332  virtual xmlt output_xml(
333  const namespacet &ns,
334  const goto_functionst &goto_functions) const;
335 
338  const goto_modelt &goto_model) const
339  {
340  const namespacet ns(goto_model.symbol_table);
341  return output_xml(ns, goto_model.goto_functions);
342  }
343 
346  const namespacet &ns,
347  const goto_programt &goto_program) const
348  {
349  return output_xml(ns, irep_idt(), goto_program);
350  }
351 
354  const namespacet &ns,
355  const goto_functionst::goto_functiont &goto_function) const
356  {
357  return output_xml(ns, irep_idt(), goto_function.body);
358  }
359 
360 protected:
363  virtual void
364  initialize(const irep_idt &function_id, const goto_programt &goto_program);
365 
367  virtual void initialize(
368  const irep_idt &function_id,
369  const goto_functionst::goto_functiont &goto_function);
370 
373  virtual void initialize(const goto_functionst &goto_functions);
374 
377  virtual void finalize();
378 
381  trace_ptrt entry_state(const goto_programt &goto_program);
382 
385  trace_ptrt entry_state(const goto_functionst &goto_functions);
386 
393  virtual jsont output_json(
394  const namespacet &ns,
395  const irep_idt &function_id,
396  const goto_programt &goto_program) const;
397 
404  virtual xmlt output_xml(
405  const namespacet &ns,
406  const irep_idt &function_id,
407  const goto_programt &goto_program) const;
408 
411 
413  trace_ptrt get_next(working_sett &working_set);
414 
416  {
417  working_set.insert(t);
418  }
419 
422  virtual bool fixedpoint(
423  trace_ptrt starting_trace,
424  const irep_idt &function_id,
425  const goto_programt &goto_program,
426  const goto_functionst &goto_functions,
427  const namespacet &ns);
428 
429  virtual void fixedpoint(
430  trace_ptrt starting_trace,
431  const goto_functionst &goto_functions,
432  const namespacet &ns);
433 
438  virtual bool visit(
439  const irep_idt &function_id,
440  trace_ptrt p,
441  working_sett &working_set,
442  const goto_programt &goto_program,
443  const goto_functionst &goto_functions,
444  const namespacet &ns);
445 
446  // function calls and return are special cases
447  // different kinds of analysis handle these differently so these are virtual
448  // visit_function_call handles which function(s) to call,
449  // while visit_edge_function_call handles a single call
450  virtual bool visit_function_call(
451  const irep_idt &function_id,
452  trace_ptrt p_call,
453  working_sett &working_set,
454  const goto_programt &goto_program,
455  const goto_functionst &goto_functions,
456  const namespacet &ns);
457 
458  virtual bool visit_end_function(
459  const irep_idt &function_id,
460  trace_ptrt p,
461  working_sett &working_set,
462  const goto_programt &goto_program,
463  const goto_functionst &goto_functions,
464  const namespacet &ns);
465 
466  // The most basic step, computing one edge / transformer application.
467  bool visit_edge(
468  const irep_idt &function_id,
469  trace_ptrt p,
470  const irep_idt &to_function_id,
471  locationt to_l,
472  const namespacet &ns,
473  working_sett &working_set);
474 
475  virtual bool visit_edge_function_call(
476  const irep_idt &calling_function_id,
477  trace_ptrt p_call,
478  locationt l_return,
479  const irep_idt &callee_function_id,
480  working_sett &working_set,
481  const goto_programt &callee,
482  const goto_functionst &goto_functions,
483  const namespacet &ns);
484 
486  std::unique_ptr<ai_history_factory_baset> history_factory;
487 
489  std::unique_ptr<ai_domain_factory_baset> domain_factory;
490 
493  virtual bool merge(const statet &src, trace_ptrt from, trace_ptrt to)
494  {
495  statet &dest = get_state(to);
496  return domain_factory->merge(dest, src, from, to);
497  }
498 
500  virtual std::unique_ptr<statet> make_temporary_state(const statet &s)
501  {
502  return domain_factory->copy(s);
503  }
504 
505  // Domain and history storage
506  std::unique_ptr<ai_storage_baset> storage;
507 
511  {
512  return storage->get_state(p, *domain_factory);
513  }
514 };
515 
516 // Perform interprocedural analysis by simply recursing in the interpreter
517 // This can lead to a call stack overflow if the domain has a large height
519 {
520 public:
522  std::unique_ptr<ai_history_factory_baset> &&hf,
523  std::unique_ptr<ai_domain_factory_baset> &&df,
524  std::unique_ptr<ai_storage_baset> &&st)
525  : ai_baset(std::move(hf), std::move(df), std::move(st))
526  {
527  }
528 
529 protected:
530  // Override the function that handles a single function call edge
532  const irep_idt &calling_function_id,
533  trace_ptrt p_call,
534  locationt l_return,
535  const irep_idt &callee_function_id,
536  working_sett &working_set,
537  const goto_programt &callee,
538  const goto_functionst &goto_functions,
539  const namespacet &ns) override;
540 };
541 
551 template <typename domainT>
553 {
554 public:
555  // constructor
556  ait()
562  {
563  }
564 
565  explicit ait(std::unique_ptr<ai_domain_factory_baset> &&df)
569  std::move(df),
571  {
572  }
573 
575 
577  // The older interface for non-modifying access
578  // Not recommended as it will throw an exception if a location has not
579  // been reached in an analysis and there is no (other) way of telling
580  // if a location has been reached.
581  DEPRECATED(SINCE(2019, 08, 01, "use abstract_state_{before,after} instead"))
582  const domainT &operator[](locationt l) const
583  {
584  auto p = storage->abstract_state_before(l, *domain_factory);
585 
586  if(p.use_count() == 1)
587  {
588  // Would be unsafe to return the dereferenced object
589  throw std::out_of_range("failed to find state");
590  }
591 
592  return static_cast<const domainT &>(*p);
593  }
594 
595 protected:
596  // Support the legacy get_state interface which is needed for a few domains
597  // This is one of the few users of the legacy get_state(locationt) method
598  // in location_sensitive_storaget.
599  DEPRECATED(SINCE(2019, 08, 01, "use get_state(trace_ptrt p) instead"))
601  {
602  auto &s = dynamic_cast<location_sensitive_storaget &>(*storage);
603  return s.get_state(l, *domain_factory);
604  }
605 
607 
608 private:
611  void dummy(const domainT &s) { const statet &x=s; (void)x; }
612 };
613 
635 template<typename domainT>
636 class concurrency_aware_ait:public ait<domainT>
637 {
638 public:
639  using statet = typename ait<domainT>::statet;
640  using locationt = typename statet::locationt;
641 
642  // constructor
644  {
645  }
646  explicit concurrency_aware_ait(std::unique_ptr<ai_domain_factory_baset> &&df)
647  : ait<domainT>(std::move(df))
648  {
649  }
650 
651  virtual bool merge_shared(
652  const statet &src,
653  locationt from,
654  locationt to,
655  const namespacet &ns)
656  {
657  statet &dest=this->get_state(to);
658  return static_cast<domainT &>(dest).merge_shared(
659  static_cast<const domainT &>(src), from, to, ns);
660  }
661 
662 protected:
664 
666  ai_baset::trace_ptrt start_trace,
667  const goto_functionst &goto_functions,
668  const namespacet &ns) override
669  {
670  ai_baset::fixedpoint(start_trace, goto_functions, ns);
671 
672  is_threadedt is_threaded(goto_functions);
673 
674  // construct an initial shared state collecting the results of all
675  // functions
676  goto_programt tmp;
677  tmp.add_instruction();
678  goto_programt::const_targett sh_target = tmp.instructions.begin();
679  ai_baset::trace_ptrt target_hist =
680  ai_baset::history_factory->epoch(sh_target);
681  statet &shared_state = ait<domainT>::get_state(sh_target);
682 
683  struct wl_entryt
684  {
685  wl_entryt(
686  const irep_idt &_function_id,
687  const goto_programt &_goto_program,
688  locationt _location)
689  : function_id(_function_id),
690  goto_program(&_goto_program),
691  location(_location)
692  {
693  }
694 
695  irep_idt function_id;
696  const goto_programt *goto_program;
697  locationt location;
698  };
699 
700  typedef std::list<wl_entryt> thread_wlt;
701  thread_wlt thread_wl;
702 
703  forall_goto_functions(it, goto_functions)
704  forall_goto_program_instructions(t_it, it->second.body)
705  {
706  if(is_threaded(t_it))
707  {
708  thread_wl.push_back(wl_entryt(it->first, it->second.body, t_it));
709 
711  it->second.body.instructions.end();
712  --l_end;
713 
714  merge_shared(shared_state, l_end, sh_target, ns);
715  }
716  }
717 
718  // now feed in the shared state into all concurrently executing
719  // functions, and iterate until the shared state stabilizes
720  bool new_shared = true;
721  while(new_shared)
722  {
723  new_shared = false;
724 
725  for(const auto &wl_entry : thread_wl)
726  {
727  working_sett working_set;
729  ai_baset::history_factory->epoch(wl_entry.location));
730  ai_baset::put_in_working_set(working_set, t);
731 
732  statet &begin_state = ait<domainT>::get_state(wl_entry.location);
733  ait<domainT>::merge(begin_state, target_hist, t);
734 
735  while(!working_set.empty())
736  {
737  ai_baset::trace_ptrt p = ai_baset::get_next(working_set);
738  goto_programt::const_targett l = p->current_location();
739 
741  wl_entry.function_id,
742  p,
743  working_set,
744  *(wl_entry.goto_program),
745  goto_functions,
746  ns);
747 
748  // the underlying domain must make sure that the final state
749  // carries all possible values; otherwise we would need to
750  // merge over each and every state
751  if(l->is_end_function())
752  new_shared |= merge_shared(shared_state, l, sh_target, ns);
753  }
754  }
755  }
756  }
757 };
758 
759 #endif // CPROVER_ANALYSES_AI_H
ai_domain_factory_default_constructort
Definition: ai_domain.h:243
ai_baset::output_xml
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:345
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
ai_baset::abstract_state_after
virtual cstate_ptrt abstract_state_after(const trace_ptrt &p) const
Definition: ai.h:248
ai_baset::output_json
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:62
ai_baset::get_next
trace_ptrt get_next(working_sett &working_set)
Get the next location from the work queue.
Definition: ai.cpp:207
abstract_goto_modelt::get_symbol_table
virtual const symbol_tablet & get_symbol_table() const =0
Accessor to get the symbol table.
ai_baset::abstract_traces_after
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:204
concurrency_aware_ait::fixedpoint
void fixedpoint(ai_baset::trace_ptrt start_trace, const goto_functionst &goto_functions, const namespacet &ns) override
Definition: ai.h:665
ai_baset::visit_end_function
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:446
ai_baset::locationt
goto_programt::const_targett locationt
Definition: ai.h:126
ai_domain.h
ai_baset::working_sett
trace_sett working_sett
The work queue, sorted using the history's ordering operator.
Definition: ai.h:410
concurrency_aware_ait::merge_shared
virtual bool merge_shared(const statet &src, locationt from, locationt to, const namespacet &ns)
Definition: ai.h:651
ahistoricalt
The common case of history is to only care about where you are now, not how you got there!...
Definition: ai_history.h:145
ai_recursive_interproceduralt
Definition: ai.h:519
ai_baset::visit_function_call
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:373
ait::dummy
void dummy(const domainT &s)
This function exists to enforce that domainT is derived from ai_domain_baset.
Definition: ai.h:611
ai_baset::operator()
void operator()(const abstract_goto_modelt &goto_model)
Run abstract interpretation on a whole program.
Definition: ai.h:167
ai_baset::make_temporary_state
virtual std::unique_ptr< statet > make_temporary_state(const statet &s)
Make a copy of a state.
Definition: ai.h:500
ai_baset::visit
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:263
ai_baset::put_in_working_set
void put_in_working_set(working_sett &working_set, trace_ptrt t)
Definition: ai.h:415
ai_baset::output_xml
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:109
goto_model.h
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition: ai.h:553
goto_modelt
Definition: goto_model.h:26
ai_baset::abstract_state_before
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:221
irep_idt
dstringt irep_idt
Definition: irep.h:32
ait::ait
ait()
Definition: ai.h:556
jsont
Definition: json.h:25
xml.h
location_sensitive_storaget::get_state
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:188
ai_baset::~ai_baset
virtual ~ai_baset()
Definition: ai.h:138
expr.h
is_threadedt
Definition: is_threaded.h:22
ai_baset::abstract_state_after
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:234
ai_baset::ai_baset
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)
Definition: ai.h:128
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
ai_baset::statet
ai_domain_baset statet
Definition: ai.h:121
goto_programt::add_instruction
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:694
util_make_unique
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition: make_unique.h:19
ai_baset::get_state
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:510
ai_history_baset::trace_sett
std::set< trace_ptrt, compare_historyt > trace_sett
Definition: ai_history.h:79
make_unique.h
ait::locationt
goto_programt::const_targett locationt
Definition: ai.h:574
ai_baset::operator()
void operator()(const goto_functionst &goto_functions, const namespacet &ns)
Run abstract interpretation on a whole program.
Definition: ai.h:156
ai_history_factory_default_constructort
An easy factory implementation for histories that don't need parameters.
Definition: ai_history.h:329
ai_baset::output_json
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:324
ait::get_state
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:510
ai_baset::output
void output(const goto_modelt &goto_model, std::ostream &out) const
Output the abstract states for a whole program.
Definition: ai.h:285
ai_baset::domain_factory
std::unique_ptr< ai_domain_factory_baset > domain_factory
For creating domain objects.
Definition: ai.h:489
ai_storage_baset::ctrace_set_ptrt
std::shared_ptr< const trace_sett > ctrace_set_ptrt
Definition: ai_storage.h:52
is_threaded.h
ai_baset::storage
std::unique_ptr< ai_storage_baset > storage
Definition: ai.h:506
concurrency_aware_ait::concurrency_aware_ait
concurrency_aware_ait(std::unique_ptr< ai_domain_factory_baset > &&df)
Definition: ai.h:646
ai_baset::abstract_traces_before
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:194
ai_baset::output_json
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:316
ai_baset::cstate_ptrt
ai_storage_baset::cstate_ptrt cstate_ptrt
Definition: ai.h:122
ai_baset::history_factory
std::unique_ptr< ai_history_factory_baset > history_factory
For creating history objects.
Definition: ai.h:486
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
ai_baset::finalize
virtual void finalize()
Override this to add a cleanup or post-processing step after fixedpoint has run.
Definition: ai.cpp:202
xmlt
Definition: xml.h:19
location_sensitive_storaget
The most conventional storage; one domain per location.
Definition: ai_storage.h:150
ai_baset::entry_state
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:175
ai_baset::merge
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:493
ai_baset::abstract_state_before
virtual cstate_ptrt abstract_state_before(const trace_ptrt &p) const
The same interfaces but with histories.
Definition: ai.h:243
ai_history.h
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
ai_baset::initialize
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:190
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
ai_baset::output
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:294
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition: ai_domain.h:76
abstract_goto_modelt::get_goto_functions
virtual const goto_functionst & get_goto_functions() const =0
Accessor to get a raw goto_functionst.
ai_storage.h
ai_baset::fixedpoint
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:225
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
ai_baset::trace_sett
ai_history_baset::trace_sett trace_sett
Definition: ai.h:124
ai_baset::output
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:42
ai_history_baset::trace_ptrt
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
ai_storage_baset::cstate_ptrt
std::shared_ptr< const statet > cstate_ptrt
Definition: ai_storage.h:47
concurrency_aware_ait
Base class for concurrency-aware abstract interpretation.
Definition: ai.h:637
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
ai_baset::output_json
jsont output_json(const goto_modelt &goto_model) const
Output the abstract states for a whole program as JSON.
Definition: ai.h:308
json.h
ai_baset::operator()
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
ait::ait
ait(std::unique_ptr< ai_domain_factory_baset > &&df)
Definition: ai.h:565
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
ai_baset::visit_edge_function_call
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:352
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:122
ai_baset::trace_ptrt
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai.h:123
ai_baset::clear
virtual void clear()
Reset the abstract state.
Definition: ai.h:261
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
ai_baset::ctrace_set_ptrt
ai_storage_baset::ctrace_set_ptrt ctrace_set_ptrt
Definition: ai.h:125
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition: abstract_goto_model.h:21
ai_recursive_interproceduralt::ai_recursive_interproceduralt
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)
Definition: ai.h:521
ai_domain_baset
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:58
ai_baset::output_xml
xmlt output_xml(const goto_modelt &goto_model) const
Output the abstract states for the whole program as XML.
Definition: ai.h:337
ai_baset::output_xml
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:353
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
ai_baset::operator()
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:177
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1172
validation_modet::INVARIANT
@ INVARIANT
ai_recursive_interproceduralt::visit_edge_function_call
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:461
ai_baset::visit_edge
bool visit_edge(const irep_idt &function_id, trace_ptrt p, const irep_idt &to_function_id, locationt to_l, const namespacet &ns, working_sett &working_set)
Definition: ai.cpp:314
concurrency_aware_ait::concurrency_aware_ait
concurrency_aware_ait()
Definition: ai.h:643