Go to the documentation of this file.
12 #ifndef CPROVER_ANALYSES_AI_H
13 #define CPROVER_ANALYSES_AI_H
55 fixedpoint(function_identifier, goto_program, goto_functions, ns);
89 fixedpoint(function_identifier, goto_function.body, goto_functions, ns);
118 INVARIANT(!l->is_end_function(),
"No state after the last instruction");
131 std::ostream &out)
const;
136 std::ostream &out)
const
146 std::ostream &out)
const
148 output(ns, goto_program,
"", out);
155 std::ostream &out)
const
157 output(ns, goto_function.body,
"", out);
215 return output_xml(ns, goto_function.body,
"");
252 std::ostream &out)
const;
287 std::pair<unsigned, locationt>(l->location_number, l));
293 const irep_idt &function_identifier,
315 const irep_idt &function_identifier,
324 const irep_idt &calling_function_identifier,
327 const exprt &
function,
333 const irep_idt &calling_function_identifier,
337 const goto_functionst::function_mapt::const_iterator f_it,
364 template<
typename domainT>
377 typename state_mapt::iterator it=
state_map.find(l);
379 throw std::out_of_range(
"failed to find state");
386 typename state_mapt::const_iterator it=
state_map.find(l);
388 throw std::out_of_range(
"failed to find state");
395 typename state_mapt::const_iterator it =
state_map.find(t);
398 std::unique_ptr<statet> d = util_make_unique<domainT>();
403 return util_make_unique<domainT>(it->second);
414 unordered_map<locationt, domainT, const_target_hash, pointee_address_equalt>
427 typename state_mapt::const_iterator it=
state_map.find(l);
429 throw std::out_of_range(
"failed to find state");
437 return static_cast<domainT &
>(dest).
merge(
438 static_cast<const domainT &
>(src), from, to);
443 return util_make_unique<domainT>(
static_cast<const domainT &
>(s));
462 throw "not implemented";
466 template<
typename domainT>
486 static_cast<const domainT &
>(src), from, to, ns);
498 #endif // CPROVER_ANALYSES_AI_H
xmlt output_xml(const namespacet &ns, const goto_programt &goto_program) const
Output the abstract states for a single function as XML.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
virtual jsont output_json(const namespacet &ns, const goto_functionst &goto_functions) const
Output the abstract states for the whole program as JSON.
bool merge_shared(const statet &, locationt, locationt, const namespacet &) override
This function should not be implemented in sequential analyses.
bool fixedpoint(const irep_idt &function_identifier, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
Run the fixedpoint algorithm until it reaches a fixed point.
bool visit(const irep_idt &function_identifier, locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
Perform one step of abstract interpretation from location l Depending on the instruction type it may ...
virtual std::unique_ptr< statet > make_temporary_state(const statet &s)=0
Make a copy of a state.
goto_programt::const_targett locationt
const domainT & operator[](locationt l) const
void dummy(const domainT &s)
This function exists to enforce that domainT is derived from ai_domain_baset.
void fixedpoint(const goto_functionst &goto_functions, const namespacet &ns) override
virtual statet & get_state(locationt l) override
Get the state for the given location, creating it in a default way if it doesn't exist.
void sequential_fixedpoint(const goto_functionst &goto_functions, const namespacet &ns)
virtual xmlt output_xml(const namespacet &ns, const goto_functionst &goto_functions) const
Output the abstract states for the whole program as XML.
Base class for all expressions.
void operator()(const goto_modelt &goto_model)
Run abstract interpretation on a whole program.
virtual const statet & find_state(locationt l) const =0
Get the state for the given location if it already exists; throw an exception if it doesn't.
virtual bool is_bottom() const =0
std::unique_ptr< statet > abstract_state_before(locationt t) const override
Get a copy of the abstract state before the given instruction, without needing to know what kind of d...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void concurrent_fixedpoint(const goto_functionst &goto_functions, const namespacet &ns)
virtual statet & get_state(locationt l)=0
Get the state for the given location, creating it in a default way if it doesn't exist.
goto_programt::const_targett locationt
virtual bool merge(const statet &src, locationt from, locationt to)=0
locationt get_next(working_sett &working_set)
Get the next location from the work queue.
void operator()(const goto_functionst &goto_functions, const namespacet &ns)
Run abstract interpretation on a whole program.
virtual void output(const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
Output the abstract states for a whole program.
void 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 ...
jsont output_json(const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
Output the abstract states for a single function as JSON.
void output(const goto_modelt &goto_model, std::ostream &out) const
Output the abstract states for a whole program.
void put_in_working_set(working_sett &working_set, locationt l)
virtual std::unique_ptr< statet > abstract_state_before(locationt l) const =0
Get a copy of the abstract state before the given instruction, without needing to know what kind of d...
bool merge_shared(const statet &src, locationt from, locationt to, const namespacet &ns) override
This function should not be implemented in sequential analyses.
void fixedpoint(const goto_functionst &goto_functions, const namespacet &ns) override
void operator()(const irep_idt &function_identifier, const goto_programt &goto_program, const namespacet &ns)
Run abstract interpretation on a single function.
virtual bool merge_shared(const statet &src, locationt from, locationt to, const namespacet &ns)=0
bool merge(const statet &src, locationt from, locationt to) override
jsont output_json(const namespacet &ns, const goto_programt &goto_program) const
Output the abstract states for a single function as JSON.
std::vector< exprt > operandst
virtual std::unique_ptr< statet > 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...
virtual void finalize()
Override this to add a cleanup or post-processing step after fixedpoint has run.
bool do_function_call(const irep_idt &calling_function_identifier, locationt l_call, locationt l_return, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, const namespacet &ns)
void output(const namespacet &ns, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a function.
::goto_functiont goto_functiont
A collection of goto functions.
domainT & operator[](locationt l)
void output(const namespacet &ns, const goto_functionst::goto_functiont &goto_function, std::ostream &out) const
Output the abstract states for a function.
goto_programt::const_targett locationt
goto_functionst goto_functions
GOTO functions.
bool do_function_call_rec(const irep_idt &calling_function_identifier, locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, const goto_functionst &goto_functions, const namespacet &ns)
The basic interface of an abstract interpreter.
jsont output_json(const goto_modelt &goto_model) const
Output the abstract states for a whole program as JSON.
A generic container class for the GOTO intermediate representation of one function.
virtual void clear()
Reset the abstract state.
instructionst::const_iterator const_targett
const statet & find_state(locationt l) const override
Get the state for the given location if it already exists; throw an exception if it doesn't.
virtual void initialize(const goto_programt &goto_program)
Initialize all the abstract states for a single function.
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
void clear() override
Reset the abstract state.
std::map< unsigned, locationt > working_sett
The work queue, sorted by location number.
xmlt output_xml(const goto_modelt &goto_model) const
Output the abstract states for the whole program as 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.
std::unique_ptr< statet > make_temporary_state(const statet &s) override
Make a copy of a state.
symbol_tablet symbol_table
Symbol table.
void operator()(const irep_idt &function_identifier, const goto_functionst::goto_functiont &goto_function, const namespacet &ns)
Run abstract interpretation on a single function.
std::unordered_map< locationt, domainT, const_target_hash, pointee_address_equalt > state_mapt
#define CHECK_RETURN(CONDITION)