45#ifndef CPROVER_ANALYSES_AI_H
46#define CPROVER_ANALYSES_AI_H
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,
151 fixedpoint(p, function_id, goto_program, goto_functions, ns);
185 fixedpoint(p, function_id, goto_function.body, goto_functions, ns);
196 return storage->abstract_traces_before(l);
208 INVARIANT(!l->is_end_function(),
"No state after the last instruction");
209 return storage->abstract_traces_before(std::next(l));
238 INVARIANT(!l->is_end_function(),
"No state after the last instruction");
251 INVARIANT(!l->is_end_function(),
"No state after the last instruction");
255 auto step_return = p->
step(
257 *(
storage->abstract_traces_before(n)),
280 std::ostream &out)
const;
308 std::ostream &out)
const;
313 std::ostream &out)
const
323 std::ostream &out)
const
421 working_set.insert(t);
481 const irep_idt &calling_function_id,
530 std::unique_ptr<ai_history_factory_baset> &&hf,
531 std::unique_ptr<ai_domain_factory_baset> &&df,
532 std::unique_ptr<ai_storage_baset> &&st,
541 const irep_idt &calling_function_id,
560template <
typename domainT>
575 explicit ait(std::unique_ptr<ai_domain_factory_baset> &&df)
592 DEPRECATED(
SINCE(2019, 08, 01,
"use abstract_state_{before,after} instead"))
597 if(p.use_count() == 1)
600 throw std::out_of_range(
"failed to find state");
603 return static_cast<const domainT &
>(*p);
649template<
typename domainT>
661 :
ait<domainT>(
std::move(df))
673 static_cast<const domainT &
>(src), from, to, ns);
703 : function_id(_function_id),
704 goto_program(&_goto_program),
714 typedef std::list<wl_entryt> thread_wlt;
715 thread_wlt thread_wl;
721 if(is_threaded(t_it))
724 wl_entryt(gf_entry.first, gf_entry.second.body, t_it));
727 gf_entry.second.body.instructions.end();
737 bool new_shared =
true;
742 for(
const auto &wl_entry : thread_wl)
752 while(!working_set.empty())
758 wl_entry.function_id,
761 *(wl_entry.goto_program),
768 if(l->is_end_function())
769 new_shared |=
merge_shared(shared_state, l, sh_target, ns);
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!
virtual cstate_ptrt abstract_state_after(const trace_ptrt &p) const
xmlt output_xml(const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
Output the abstract states for a single function as XML.
goto_programt::const_targett locationt
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)
void operator()(const goto_functionst &goto_functions, const namespacet &ns)
Run abstract interpretation on a whole program.
virtual ctrace_set_ptrt abstract_traces_after(locationt l) const
Returns all of the histories that have reached the end of the instruction.
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...
std::unique_ptr< ai_storage_baset > storage
virtual statet & get_state(trace_ptrt p)
Get the state for the given history, creating it with the factory if it doesn't exist.
ai_history_baset::trace_sett trace_sett
jsont output_json(const namespacet &ns, const goto_programt &goto_program) const
Output the abstract states for a single function as JSON.
void operator()(const irep_idt &function_id, const goto_programt &goto_program, const namespacet &ns)
Run abstract interpretation on a single function.
virtual ctrace_set_ptrt abstract_traces_before(locationt l) const
Returns all of the histories that have reached the start of the instruction.
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...
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)
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.
xmlt output_xml(const namespacet &ns, const goto_programt &goto_program) const
Output the abstract states for a single function as XML.
jsont output_json(const goto_modelt &goto_model) const
Output the abstract states for a whole program as JSON.
message_handlert & message_handler
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)
virtual cstate_ptrt abstract_state_before(const trace_ptrt &p) const
The same interfaces but with histories.
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)
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 ...
void operator()(const abstract_goto_modelt &goto_model)
Run abstract interpretation on a whole program.
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)
void output(const goto_modelt &goto_model, std::ostream &out) const
Output the abstract states for a whole program.
virtual void clear()
Reset the abstract state.
std::unique_ptr< ai_domain_factory_baset > domain_factory
For creating domain objects.
ai_storage_baset::ctrace_set_ptrt ctrace_set_ptrt
virtual void initialize(const irep_idt &function_id, const goto_programt &goto_program)
Initialize all the abstract states for a single function.
xmlt output_xml(const goto_modelt &goto_model) const
Output the abstract states for the whole program as XML.
jsont output_json(const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
Output the abstract states for a single function as JSON.
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.
virtual std::unique_ptr< statet > make_temporary_state(const statet &s)
Make a copy of a state.
ai_history_baset::trace_ptrt trace_ptrt
void put_in_working_set(working_sett &working_set, trace_ptrt t)
trace_ptrt get_next(working_sett &working_set)
Get the next location from the work queue.
trace_sett working_sett
The work queue, sorted using the history's ordering operator.
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...
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...
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.
void operator()(const irep_idt &function_id, const goto_functionst::goto_functiont &goto_function, const namespacet &ns)
Run abstract interpretation on a single function.
void output(const namespacet &ns, const goto_functionst::goto_functiont &goto_function, std::ostream &out) const
Output the abstract states for a function.
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.
std::unique_ptr< ai_history_factory_baset > history_factory
For creating history objects.
virtual void finalize()
Override this to add a cleanup or post-processing step after fixedpoint has run.
ai_storage_baset::cstate_ptrt cstate_ptrt
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
virtual const locationt & current_location(void) const =0
The current location in the history, used to compute the transformer POSTCONDITION(return value is de...
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.
static const trace_ptrt no_caller_history
virtual step_returnt step(locationt to, const trace_sett &others, trace_ptrt caller_hist) const =0
Step creates a new history by advancing the current one to location "to" It is given the set of all o...
std::set< trace_ptrt, compare_historyt > trace_sett
An easy factory implementation for histories that don't need parameters.
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)
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
std::shared_ptr< const trace_sett > ctrace_set_ptrt
std::shared_ptr< const statet > cstate_ptrt
ait(std::unique_ptr< ai_domain_factory_baset > &&df)
goto_programt::const_targett locationt
null_message_handlert no_logging
void dummy(const domainT &s)
This function exists to enforce that domainT is derived from ai_domain_baset.
virtual statet & get_state(locationt l)
ai_baset::working_sett working_sett
typename ait< domainT >::statet statet
concurrency_aware_ait(std::unique_ptr< ai_domain_factory_baset > &&df)
virtual bool merge_shared(const statet &src, locationt from, locationt to, const namespacet &ns)
void fixedpoint(ai_baset::trace_ptrt start_trace, const goto_functionst &goto_functions, const namespacet &ns) override
typename statet::locationt locationt
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
targett add_instruction()
Adds an instruction at the end.
The most conventional storage; one domain per location.
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.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
#define SINCE(year, month, day, msg)
#define forall_goto_program_instructions(it, program)
Over-approximate Concurrency for Threaded Goto Programs.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.