diff --git a/src/analyses/Makefile b/src/analyses/Makefile index 350a526f70c..dbab82bda96 100644 --- a/src/analyses/Makefile +++ b/src/analyses/Makefile @@ -1,4 +1,5 @@ SRC = ai.cpp \ + ai_domain.cpp \ call_graph.cpp \ call_graph_helpers.cpp \ constant_propagator.cpp \ diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp index f0fcb99b189..d2aa0c14bbb 100644 --- a/src/analyses/ai.cpp +++ b/src/analyses/ai.cpp @@ -15,80 +15,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include "is_threaded.h" -jsont ai_domain_baset::output_json( - const ai_baset &ai, - const namespacet &ns) const -{ - std::ostringstream out; - output(out, ai, ns); - json_stringt json(out.str()); - return json; -} - -xmlt ai_domain_baset::output_xml( - const ai_baset &ai, - const namespacet &ns) const -{ - std::ostringstream out; - output(out, ai, ns); - xmlt xml("abstract_state"); - xml.data=out.str(); - return xml; -} - -/// Use the information in the domain to simplify the expression on the LHS of -/// an assignment. This for example won't simplify symbols to their values, but -/// does simplify indices in arrays, members of structs and dereferencing of -/// pointers -/// \param condition: the expression to simplify -/// \param ns: the namespace -/// \return True if condition did not change. False otherwise. condition will be -/// updated with the simplified condition if it has worked -bool ai_domain_baset::ai_simplify_lhs( - exprt &condition, const namespacet &ns) const -{ - // Care must be taken here to give something that is still writable - if(condition.id()==ID_index) - { - index_exprt ie=to_index_expr(condition); - bool no_simplification=ai_simplify(ie.index(), ns); - if(!no_simplification) - condition=simplify_expr(ie, ns); - - return no_simplification; - } - else if(condition.id()==ID_dereference) - { - dereference_exprt de=to_dereference_expr(condition); - bool no_simplification=ai_simplify(de.pointer(), ns); - if(!no_simplification) - condition=simplify_expr(de, ns); // So *(&x) -> x - - return no_simplification; - } - else if(condition.id()==ID_member) - { - member_exprt me=to_member_expr(condition); - // Since simplify_ai_lhs is required to return an addressable object - // (so remains a valid left hand side), to simplify - // `(something_simplifiable).b` we require that `something_simplifiable` - // must also be addressable - bool no_simplification=ai_simplify_lhs(me.compound(), ns); - if(!no_simplification) - condition=simplify_expr(me, ns); - - return no_simplification; - } - else - return true; -} - void ai_baset::output( const namespacet &ns, const goto_functionst &goto_functions, diff --git a/src/analyses/ai.h b/src/analyses/ai.h index dfe5e183a3d..aea76ea7480 100644 --- a/src/analyses/ai.h +++ b/src/analyses/ai.h @@ -23,105 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com #include -// forward reference -class ai_baset; - -// don't use me -- I am just a base class -// please derive from me -class ai_domain_baset -{ -public: - // The constructor is expected to produce 'false' - // or 'bottom' - ai_domain_baset() - { - } - - virtual ~ai_domain_baset() - { - } - - typedef goto_programt::const_targett locationt; - - // how function calls are treated: - // a) there is an edge from each call site to the function head - // b) there is an edge from the last instruction (END_FUNCTION) - // of the function to the instruction _following_ the call site - // (this also needs to set the LHS, if applicable) - // - // "this" is the domain before the instruction "from" - // "from" is the instruction to be interpretted - // "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION) - // - // PRECONDITION(from.is_dereferenceable(), "Must not be _::end()") - // PRECONDITION(to.is_dereferenceable(), "Must not be _::end()") - // PRECONDITION(are_comparable(from,to) || - // (from->is_function_call() || from->is_end_function()) - - virtual void transform( - locationt from, - locationt to, - ai_baset &ai, - const namespacet &ns) = 0; - - virtual void output( - std::ostream &out, - const ai_baset &ai, - const namespacet &ns) const - { - } - - virtual jsont output_json( - const ai_baset &ai, - const namespacet &ns) const; - - virtual xmlt output_xml( - const ai_baset &ai, - const namespacet &ns) const; - - // no states - virtual void make_bottom()=0; - - // all states -- the analysis doesn't use this, - // and domains may refuse to implement it. - virtual void make_top()=0; - - // a reasonable entry-point state - virtual void make_entry()=0; - - virtual bool is_bottom() const=0; - - virtual bool is_top() const=0; - - // also add - // - // bool merge(const T &b, locationt from, locationt to); - // - // This computes the join between "this" and "b". - // Return true if "this" has changed. - // In the usual case, "b" is the updated state after "from" - // and "this" is the state before "to". - // - // PRECONDITION(from.is_dereferenceable(), "Must not be _::end()") - // PRECONDITION(to.is_dereferenceable(), "Must not be _::end()") - - // This method allows an expression to be simplified / evaluated using the - // current state. It is used to evaluate assertions and in program - // simplification - - // return true if unchanged - virtual bool ai_simplify( - exprt &condition, - const namespacet &ns) const - { - return true; - } - - // Simplifies the expression but keeps it as an l-value - virtual bool ai_simplify_lhs( - exprt &condition, - const namespacet &ns) const; -}; +#include "ai_domain.h" // don't use me -- I am just a base class // use ait instead diff --git a/src/analyses/ai_domain.cpp b/src/analyses/ai_domain.cpp new file mode 100644 index 00000000000..93a6dfe7542 --- /dev/null +++ b/src/analyses/ai_domain.cpp @@ -0,0 +1,79 @@ +/*******************************************************************\ + +Module: Abstract Interpretation + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +/// \file +/// Abstract Interpretation Domain + +#include "ai_domain.h" + +#include + +jsont ai_domain_baset::output_json(const ai_baset &ai, const namespacet &ns) + const +{ + std::ostringstream out; + output(out, ai, ns); + json_stringt json(out.str()); + return json; +} + +xmlt ai_domain_baset::output_xml(const ai_baset &ai, const namespacet &ns) const +{ + std::ostringstream out; + output(out, ai, ns); + xmlt xml("abstract_state"); + xml.data = out.str(); + return xml; +} + +/// Use the information in the domain to simplify the expression on the LHS of +/// an assignment. This for example won't simplify symbols to their values, but +/// does simplify indices in arrays, members of structs and dereferencing of +/// pointers +/// \param condition: the expression to simplify +/// \param ns: the namespace +/// \return True if condition did not change. False otherwise. condition will be +/// updated with the simplified condition if it has worked +bool ai_domain_baset::ai_simplify_lhs(exprt &condition, const namespacet &ns) + const +{ + // Care must be taken here to give something that is still writable + if(condition.id() == ID_index) + { + index_exprt ie = to_index_expr(condition); + bool no_simplification = ai_simplify(ie.index(), ns); + if(!no_simplification) + condition = simplify_expr(ie, ns); + + return no_simplification; + } + else if(condition.id() == ID_dereference) + { + dereference_exprt de = to_dereference_expr(condition); + bool no_simplification = ai_simplify(de.pointer(), ns); + if(!no_simplification) + condition = simplify_expr(de, ns); // So *(&x) -> x + + return no_simplification; + } + else if(condition.id() == ID_member) + { + member_exprt me = to_member_expr(condition); + // Since simplify_ai_lhs is required to return an addressable object + // (so remains a valid left hand side), to simplify + // `(something_simplifiable).b` we require that `something_simplifiable` + // must also be addressable + bool no_simplification = ai_simplify_lhs(me.compound(), ns); + if(!no_simplification) + condition = simplify_expr(me, ns); + + return no_simplification; + } + else + return true; +} diff --git a/src/analyses/ai_domain.h b/src/analyses/ai_domain.h new file mode 100644 index 00000000000..2dc1b6e33ec --- /dev/null +++ b/src/analyses/ai_domain.h @@ -0,0 +1,122 @@ +/*******************************************************************\ + +Module: Abstract Interpretation + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +/// \file +/// Abstract Interpretation Domain + +#ifndef CPROVER_ANALYSES_AI_DOMAIN_H +#define CPROVER_ANALYSES_AI_DOMAIN_H + +#include +#include +#include +#include + +#include + +// forward reference the abstract interpreter interface +class ai_baset; + +/// The interface offered by a domain, allows code to manipulate domains without +/// knowing their exact type. Derive from this to implement domains. +class ai_domain_baset +{ +protected: + /// The constructor is expected to produce 'false' or 'bottom' + ai_domain_baset() + { + } + +public: + virtual ~ai_domain_baset() + { + } + + typedef goto_programt::const_targett locationt; + + /// how function calls are treated: + /// a) there is an edge from each call site to the function head + /// b) there is an edge from the last instruction (END_FUNCTION) + /// of the function to the instruction _following_ the call site + /// (this also needs to set the LHS, if applicable) + /// + /// "this" is the domain before the instruction "from" + /// "from" is the instruction to be interpretted + /// "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION) + /// + /// PRECONDITION(from.is_dereferenceable(), "Must not be _::end()") + /// PRECONDITION(to.is_dereferenceable(), "Must not be _::end()") + /// PRECONDITION(are_comparable(from,to) || + /// (from->is_function_call() || from->is_end_function()) + + virtual void transform( + locationt from, + locationt to, + ai_baset &ai, + const namespacet &ns) = 0; + + virtual void + output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const + { + } + + virtual jsont output_json(const ai_baset &ai, const namespacet &ns) const; + + virtual xmlt output_xml(const ai_baset &ai, const namespacet &ns) const; + + /// no states + virtual void make_bottom() = 0; + + /// all states -- the analysis doesn't use this, + /// and domains may refuse to implement it. + virtual void make_top() = 0; + + /// a reasonable entry-point state + virtual void make_entry() = 0; + + virtual bool is_bottom() const = 0; + + virtual bool is_top() const = 0; + + /// also add + /// + /// bool merge(const T &b, locationt from, locationt to); + /// + /// This computes the join between "this" and "b". + /// Return true if "this" has changed. + /// In the usual case, "b" is the updated state after "from" + /// and "this" is the state before "to". + /// + /// PRECONDITION(from.is_dereferenceable(), "Must not be _::end()") + /// PRECONDITION(to.is_dereferenceable(), "Must not be _::end()") + + /// This method allows an expression to be simplified / evaluated using the + /// current state. It is used to evaluate assertions and in program + /// simplification + + /// return true if unchanged + virtual bool ai_simplify(exprt &condition, const namespacet &ns) const + { + return true; + } + + /// Simplifies the expression but keeps it as an l-value + virtual bool ai_simplify_lhs(exprt &condition, const namespacet &ns) const; + + /// Gives a Boolean condition that is true for all values represented by the + /// domain. This allows domains to be converted into program invariants. + virtual exprt to_predicate(void) const + { + if(is_bottom()) + return false_exprt(); + else + return true_exprt(); + } +}; + +#endif