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/deprecate.h>
53 #include <util/expr.h>
54 #include <util/json.h>
55 #include <util/make_unique.h>
56 #include <util/xml.h>
57 
59 
60 #include "ai_domain.h"
61 #include "ai_history.h"
62 #include "ai_storage.h"
63 #include "is_threaded.h"
64 
118 
119 class ai_baset
120 {
121 public:
128 
130  std::unique_ptr<ai_history_factory_baset> &&hf,
131  std::unique_ptr<ai_domain_factory_baset> &&df,
132  std::unique_ptr<ai_storage_baset> &&st)
133  : history_factory(std::move(hf)),
134  domain_factory(std::move(df)),
135  storage(std::move(st))
136  {
137  }
138 
139  virtual ~ai_baset()
140  {
141  }
142 
145  const irep_idt &function_id,
146  const goto_programt &goto_program,
147  const namespacet &ns)
148  {
149  goto_functionst goto_functions;
150  initialize(function_id, goto_program);
151  trace_ptrt p = entry_state(goto_program);
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  fixedpoint(p, goto_functions, ns);
164  finalize();
165  }
166 
168  void operator()(const abstract_goto_modelt &goto_model)
169  {
170  const namespacet ns(goto_model.get_symbol_table());
171  initialize(goto_model.get_goto_functions());
172  trace_ptrt p = entry_state(goto_model.get_goto_functions());
173  fixedpoint(p, goto_model.get_goto_functions(), ns);
174  finalize();
175  }
176 
179  const irep_idt &function_id,
180  const goto_functionst::goto_functiont &goto_function,
181  const namespacet &ns)
182  {
183  goto_functionst goto_functions;
184  initialize(function_id, goto_function);
185  trace_ptrt p = entry_state(goto_function.body);
186  fixedpoint(p, function_id, goto_function.body, goto_functions, ns);
187  finalize();
188  }
189 
196  {
197  return storage->abstract_traces_before(l);
198  }
199 
206  {
209  INVARIANT(!l->is_end_function(), "No state after the last instruction");
210  return storage->abstract_traces_before(std::next(l));
211  }
212 
223  {
224  return storage->abstract_state_before(l, *domain_factory);
225  }
226 
236  {
239  INVARIANT(!l->is_end_function(), "No state after the last instruction");
240  return abstract_state_before(std::next(l));
241  }
242 
245  {
246  return storage->abstract_state_before(p, *domain_factory);
247  }
248 
250  {
251  locationt l = p->current_location();
252  INVARIANT(!l->is_end_function(), "No state after the last instruction");
253 
254  locationt n = std::next(l);
255 
256  auto step_return = p->step(
257  n,
258  *(storage->abstract_traces_before(n)),
260  // Caller history not needed as this is a local step
261 
262  return storage->abstract_state_before(step_return.second, *domain_factory);
263  }
264 
266  virtual void clear()
267  {
268  storage->clear();
269  }
270 
277  virtual void output(
278  const namespacet &ns,
279  const irep_idt &function_id,
280  const goto_programt &goto_program,
281  std::ostream &out) const;
282 
284  virtual void output(
285  const namespacet &ns,
286  const goto_functionst &goto_functions,
287  std::ostream &out) const;
288 
290  void output(
291  const goto_modelt &goto_model,
292  std::ostream &out) const
293  {
294  const namespacet ns(goto_model.symbol_table);
295  output(ns, goto_model.goto_functions, out);
296  }
297 
299  void output(
300  const namespacet &ns,
301  const goto_functionst::goto_functiont &goto_function,
302  std::ostream &out) const
303  {
304  output(ns, irep_idt(), goto_function.body, out);
305  }
306 
308  virtual jsont output_json(
309  const namespacet &ns,
310  const goto_functionst &goto_functions) const;
311 
314  const goto_modelt &goto_model) const
315  {
316  const namespacet ns(goto_model.symbol_table);
317  return output_json(ns, goto_model.goto_functions);
318  }
319 
322  const namespacet &ns,
323  const goto_programt &goto_program) const
324  {
325  return output_json(ns, irep_idt(), goto_program);
326  }
327 
330  const namespacet &ns,
331  const goto_functionst::goto_functiont &goto_function) const
332  {
333  return output_json(ns, irep_idt(), goto_function.body);
334  }
335 
337  virtual xmlt output_xml(
338  const namespacet &ns,
339  const goto_functionst &goto_functions) const;
340 
343  const goto_modelt &goto_model) const
344  {
345  const namespacet ns(goto_model.symbol_table);
346  return output_xml(ns, goto_model.goto_functions);
347  }
348 
351  const namespacet &ns,
352  const goto_programt &goto_program) const
353  {
354  return output_xml(ns, irep_idt(), goto_program);
355  }
356 
359  const namespacet &ns,
360  const goto_functionst::goto_functiont &goto_function) const
361  {
362  return output_xml(ns, irep_idt(), goto_function.body);
363  }
364 
365 protected:
368  virtual void
369  initialize(const irep_idt &function_id, const goto_programt &goto_program);
370 
372  virtual void initialize(
373  const irep_idt &function_id,
374  const goto_functionst::goto_functiont &goto_function);
375 
378  virtual void initialize(const goto_functionst &goto_functions);
379 
382  virtual void finalize();
383 
386  trace_ptrt entry_state(const goto_programt &goto_program);
387 
390  trace_ptrt entry_state(const goto_functionst &goto_functions);
391 
398  virtual jsont output_json(
399  const namespacet &ns,
400  const irep_idt &function_id,
401  const goto_programt &goto_program) const;
402 
409  virtual xmlt output_xml(
410  const namespacet &ns,
411  const irep_idt &function_id,
412  const goto_programt &goto_program) const;
413 
416 
418  trace_ptrt get_next(working_sett &working_set);
419 
421  {
422  working_set.insert(t);
423  }
424 
427  virtual bool fixedpoint(
428  trace_ptrt starting_trace,
429  const irep_idt &function_id,
430  const goto_programt &goto_program,
431  const goto_functionst &goto_functions,
432  const namespacet &ns);
433 
434  virtual void fixedpoint(
435  trace_ptrt starting_trace,
436  const goto_functionst &goto_functions,
437  const namespacet &ns);
438 
443  virtual bool visit(
444  const irep_idt &function_id,
445  trace_ptrt p,
446  working_sett &working_set,
447  const goto_programt &goto_program,
448  const goto_functionst &goto_functions,
449  const namespacet &ns);
450 
451  // function calls and return are special cases
452  // different kinds of analysis handle these differently so these are virtual
453  // visit_function_call handles which function(s) to call,
454  // while visit_edge_function_call handles a single call
455  virtual bool visit_function_call(
456  const irep_idt &function_id,
457  trace_ptrt p_call,
458  working_sett &working_set,
459  const goto_programt &goto_program,
460  const goto_functionst &goto_functions,
461  const namespacet &ns);
462 
463  virtual bool visit_end_function(
464  const irep_idt &function_id,
465  trace_ptrt p,
466  working_sett &working_set,
467  const goto_programt &goto_program,
468  const goto_functionst &goto_functions,
469  const namespacet &ns);
470 
471  // The most basic step, computing one edge / transformer application.
472  bool visit_edge(
473  const irep_idt &function_id,
474  trace_ptrt p,
475  const irep_idt &to_function_id,
476  locationt to_l,
477  trace_ptrt caller_history,
478  const namespacet &ns,
479  working_sett &working_set);
480 
481  virtual bool visit_edge_function_call(
482  const irep_idt &calling_function_id,
483  trace_ptrt p_call,
484  locationt l_return,
485  const irep_idt &callee_function_id,
486  working_sett &working_set,
487  const goto_programt &callee,
488  const goto_functionst &goto_functions,
489  const namespacet &ns);
490 
492  std::unique_ptr<ai_history_factory_baset> history_factory;
493 
495  std::unique_ptr<ai_domain_factory_baset> domain_factory;
496 
499  virtual bool merge(const statet &src, trace_ptrt from, trace_ptrt to)
500  {
501  statet &dest = get_state(to);
502  return domain_factory->merge(dest, src, from, to);
503  }
504 
506  virtual std::unique_ptr<statet> make_temporary_state(const statet &s)
507  {
508  return domain_factory->copy(s);
509  }
510 
511  // Domain and history storage
512  std::unique_ptr<ai_storage_baset> storage;
513 
517  {
518  return storage->get_state(p, *domain_factory);
519  }
520 };
521 
522 // Perform interprocedural analysis by simply recursing in the interpreter
523 // This can lead to a call stack overflow if the domain has a large height
525 {
526 public:
528  std::unique_ptr<ai_history_factory_baset> &&hf,
529  std::unique_ptr<ai_domain_factory_baset> &&df,
530  std::unique_ptr<ai_storage_baset> &&st)
531  : ai_baset(std::move(hf), std::move(df), std::move(st))
532  {
533  }
534 
535 protected:
536  // Override the function that handles a single function call edge
538  const irep_idt &calling_function_id,
539  trace_ptrt p_call,
540  locationt l_return,
541  const irep_idt &callee_function_id,
542  working_sett &working_set,
543  const goto_programt &callee,
544  const goto_functionst &goto_functions,
545  const namespacet &ns) override;
546 };
547 
557 template <typename domainT>
559 {
560 public:
561  // constructor
562  ait()
568  {
569  }
570 
571  explicit ait(std::unique_ptr<ai_domain_factory_baset> &&df)
575  std::move(df),
577  {
578  }
579 
581 
583  // The older interface for non-modifying access
584  // Not recommended as it will throw an exception if a location has not
585  // been reached in an analysis and there is no (other) way of telling
586  // if a location has been reached.
587  DEPRECATED(SINCE(2019, 08, 01, "use abstract_state_{before,after} instead"))
588  const domainT &operator[](locationt l) const
589  {
590  auto p = storage->abstract_state_before(l, *domain_factory);
591 
592  if(p.use_count() == 1)
593  {
594  // Would be unsafe to return the dereferenced object
595  throw std::out_of_range("failed to find state");
596  }
597 
598  return static_cast<const domainT &>(*p);
599  }
600 
601 protected:
602  // Support the legacy get_state interface which is needed for a few domains
603  // This is one of the few users of the legacy get_state(locationt) method
604  // in location_sensitive_storaget.
605  DEPRECATED(SINCE(2019, 08, 01, "use get_state(trace_ptrt p) instead"))
607  {
608  auto &s = dynamic_cast<location_sensitive_storaget &>(*storage);
609  return s.get_state(l, *domain_factory);
610  }
611 
613 
614 private:
617  void dummy(const domainT &s) { const statet &x=s; (void)x; }
618 };
619 
641 template<typename domainT>
642 class concurrency_aware_ait:public ait<domainT>
643 {
644 public:
645  using statet = typename ait<domainT>::statet;
646  using locationt = typename statet::locationt;
647 
648  // constructor
650  {
651  }
652  explicit concurrency_aware_ait(std::unique_ptr<ai_domain_factory_baset> &&df)
653  : ait<domainT>(std::move(df))
654  {
655  }
656 
657  virtual bool merge_shared(
658  const statet &src,
659  locationt from,
660  locationt to,
661  const namespacet &ns)
662  {
663  statet &dest=this->get_state(to);
664  return static_cast<domainT &>(dest).merge_shared(
665  static_cast<const domainT &>(src), from, to, ns);
666  }
667 
668 protected:
670 
672  ai_baset::trace_ptrt start_trace,
673  const goto_functionst &goto_functions,
674  const namespacet &ns) override
675  {
676  ai_baset::fixedpoint(start_trace, goto_functions, ns);
677 
678  is_threadedt is_threaded(goto_functions);
679 
680  // construct an initial shared state collecting the results of all
681  // functions
682  goto_programt tmp;
683  tmp.add_instruction();
684  goto_programt::const_targett sh_target = tmp.instructions.begin();
685  ai_baset::trace_ptrt target_hist =
686  ai_baset::history_factory->epoch(sh_target);
687  statet &shared_state = ait<domainT>::get_state(sh_target);
688 
689  struct wl_entryt
690  {
691  wl_entryt(
692  const irep_idt &_function_id,
693  const goto_programt &_goto_program,
694  locationt _location)
695  : function_id(_function_id),
696  goto_program(&_goto_program),
697  location(_location)
698  {
699  }
700 
701  irep_idt function_id;
702  const goto_programt *goto_program;
703  locationt location;
704  };
705 
706  typedef std::list<wl_entryt> thread_wlt;
707  thread_wlt thread_wl;
708 
709  for(const auto &gf_entry : goto_functions.function_map)
710  {
711  forall_goto_program_instructions(t_it, gf_entry.second.body)
712  {
713  if(is_threaded(t_it))
714  {
715  thread_wl.push_back(
716  wl_entryt(gf_entry.first, gf_entry.second.body, t_it));
717 
719  gf_entry.second.body.instructions.end();
720  --l_end;
721 
722  merge_shared(shared_state, l_end, sh_target, ns);
723  }
724  }
725  }
726 
727  // now feed in the shared state into all concurrently executing
728  // functions, and iterate until the shared state stabilizes
729  bool new_shared = true;
730  while(new_shared)
731  {
732  new_shared = false;
733 
734  for(const auto &wl_entry : thread_wl)
735  {
736  working_sett working_set;
738  ai_baset::history_factory->epoch(wl_entry.location));
739  ai_baset::put_in_working_set(working_set, t);
740 
741  statet &begin_state = ait<domainT>::get_state(wl_entry.location);
742  ait<domainT>::merge(begin_state, target_hist, t);
743 
744  while(!working_set.empty())
745  {
746  ai_baset::trace_ptrt p = ai_baset::get_next(working_set);
747  goto_programt::const_targett l = p->current_location();
748 
750  wl_entry.function_id,
751  p,
752  working_set,
753  *(wl_entry.goto_program),
754  goto_functions,
755  ns);
756 
757  // the underlying domain must make sure that the final state
758  // carries all possible values; otherwise we would need to
759  // merge over each and every state
760  if(l->is_end_function())
761  new_shared |= merge_shared(shared_state, l, sh_target, ns);
762  }
763  }
764  }
765  }
766 };
767 
768 #endif // CPROVER_ANALYSES_AI_H
ai_domain_factory_default_constructort
Definition: ai_domain.h:226
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:350
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:249
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:61
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:205
concurrency_aware_ait::fixedpoint
void fixedpoint(ai_baset::trace_ptrt start_trace, const goto_functionst &goto_functions, const namespacet &ns) override
Definition: ai.h:671
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:457
ai_baset::locationt
goto_programt::const_targett locationt
Definition: ai.h:127
ai_domain.h
Abstract Interpretation Domain.
ai_baset::working_sett
trace_sett working_sett
The work queue, sorted using the history's ordering operator.
Definition: ai.h:415
concurrency_aware_ait::merge_shared
virtual bool merge_shared(const statet &src, locationt from, locationt to, const namespacet &ns)
Definition: ai.h:657
ahistoricalt
The common case of history is to only care about where you are now, not how you got there!...
Definition: ai_history.h:155
ai_recursive_interproceduralt
Definition: ai.h:525
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:383
ait::dummy
void dummy(const domainT &s)
This function exists to enforce that domainT is derived from ai_domain_baset.
Definition: ai.h:617
ai_baset::operator()
void operator()(const abstract_goto_modelt &goto_model)
Run abstract interpretation on a whole program.
Definition: ai.h:168
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:506
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:420
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:108
goto_model.h
Symbol Table + CFG.
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition: ai.h:559
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:222
irep_idt
dstringt irep_idt
Definition: irep.h:37
ai_history_baset::no_caller_history
static const trace_ptrt no_caller_history
Definition: ai_history.h:121
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
ait::ait
ait()
Definition: ai.h:562
jsont
Definition: json.h:27
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:192
ai_baset::~ai_baset
virtual ~ai_baset()
Definition: ai.h:139
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:235
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:129
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:122
goto_programt::add_instruction
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:665
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:516
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:580
deprecate.h
ai_baset::operator()
void operator()(const goto_functionst &goto_functions, const namespacet &ns)
Run abstract interpretation on a whole program.
Definition: ai.h:157
ai_history_factory_default_constructort
An easy factory implementation for histories that don't need parameters.
Definition: ai_history.h:255
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:329
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:516
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:290
ai_baset::domain_factory
std::unique_ptr< ai_domain_factory_baset > domain_factory
For creating domain objects.
Definition: ai.h:495
ai_storage_baset::ctrace_set_ptrt
std::shared_ptr< const trace_sett > ctrace_set_ptrt
Definition: ai_storage.h:54
is_threaded.h
Over-approximate Concurrency for Threaded Goto Programs.
ai_baset::storage
std::unique_ptr< ai_storage_baset > storage
Definition: ai.h:512
concurrency_aware_ait::concurrency_aware_ait
concurrency_aware_ait(std::unique_ptr< ai_domain_factory_baset > &&df)
Definition: ai.h:652
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:195
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:321
ai_baset::cstate_ptrt
ai_storage_baset::cstate_ptrt cstate_ptrt
Definition: ai.h:123
ai_baset::history_factory
std::unique_ptr< ai_history_factory_baset > history_factory
For creating history objects.
Definition: ai.h:492
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:21
location_sensitive_storaget
The most conventional storage; one domain per location.
Definition: ai_storage.h:153
ai_baset::visit_edge
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:320
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:499
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:244
ai_history.h
Abstract Interpretation history.
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:556
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:299
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition: ai_domain.h:77
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
Abstract Interpretation Storage.
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:125
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:41
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:49
concurrency_aware_ait
Base class for concurrency-aware abstract interpretation.
Definition: ai.h:643
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
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:313
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:144
ait::ait
ait(std::unique_ptr< ai_domain_factory_baset > &&df)
Definition: ai.h:571
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
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:360
ai_baset::trace_ptrt
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai.h:124
ai_baset::clear
virtual void clear()
Reset the abstract state.
Definition: ai.h:266
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:551
ai_baset::ctrace_set_ptrt
ai_storage_baset::ctrace_set_ptrt ctrace_set_ptrt
Definition: ai.h:126
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition: abstract_goto_model.h:21
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
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:527
ai_domain_baset
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:59
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:342
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:358
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:178
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1167
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:472
concurrency_aware_ait::concurrency_aware_ait
concurrency_aware_ait()
Definition: ai.h:649