From f60027b778d894242699a2ccbad1685ce3350470 Mon Sep 17 00:00:00 2001 From: martin Date: Mon, 23 Jul 2018 15:49:22 +0100 Subject: [PATCH 1/6] Move the interface of domains to it's own header file. ai.{h,cpp} is already crowded with two different interfaces. The following patch set will make this much worse, thus we start by refactoring. --- src/analyses/Makefile | 1 + src/analyses/ai.cpp | 69 --------------------- src/analyses/ai.h | 100 +----------------------------- src/analyses/ai_domain.cpp | 82 +++++++++++++++++++++++++ src/analyses/ai_domain.h | 122 +++++++++++++++++++++++++++++++++++++ 5 files changed, 206 insertions(+), 168 deletions(-) create mode 100644 src/analyses/ai_domain.cpp create mode 100644 src/analyses/ai_domain.h 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..c8d95afc050 --- /dev/null +++ b/src/analyses/ai_domain.cpp @@ -0,0 +1,82 @@ +/*******************************************************************\ + +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..76e73604ce1 --- /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 +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; +}; + +#endif From 918e94706818a76776d3079c7c9c0b104dcb1164 Mon Sep 17 00:00:00 2001 From: martin Date: Mon, 23 Jul 2018 15:58:52 +0100 Subject: [PATCH 2/6] Expand the comments describing the base domain interface. --- src/analyses/ai_domain.h | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/analyses/ai_domain.h b/src/analyses/ai_domain.h index 76e73604ce1..15b6046145e 100644 --- a/src/analyses/ai_domain.h +++ b/src/analyses/ai_domain.h @@ -19,16 +19,17 @@ Author: Daniel Kroening, kroening@kroening.com #include -// forward reference +// 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. // 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' + // The constructor is expected to produce 'false' or 'bottom' ai_domain_baset() { } @@ -101,6 +102,7 @@ class ai_domain_baset // 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 From 028d8b648ed9cc06d14bb4592198db3236146976 Mon Sep 17 00:00:00 2001 From: martin Date: Mon, 23 Jul 2018 16:02:37 +0100 Subject: [PATCH 3/6] Add a method to convert the domain to a predicate to the basic domain API. This allows the domain to be converted to an assumption or an assertion amongst other applications. --- src/analyses/ai_domain.h | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/analyses/ai_domain.h b/src/analyses/ai_domain.h index 15b6046145e..6554fda837c 100644 --- a/src/analyses/ai_domain.h +++ b/src/analyses/ai_domain.h @@ -119,6 +119,16 @@ class ai_domain_baset 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 From 2b9c8803aa99380754037db48a088a1e8b0359b8 Mon Sep 17 00:00:00 2001 From: martin Date: Tue, 24 Jul 2018 14:59:21 +0100 Subject: [PATCH 4/6] Clang format the domain files. --- src/analyses/ai_domain.cpp | 39 ++++++++++++++++++-------------------- src/analyses/ai_domain.h | 37 +++++++++++++----------------------- 2 files changed, 31 insertions(+), 45 deletions(-) diff --git a/src/analyses/ai_domain.cpp b/src/analyses/ai_domain.cpp index c8d95afc050..93a6dfe7542 100644 --- a/src/analyses/ai_domain.cpp +++ b/src/analyses/ai_domain.cpp @@ -13,9 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com #include -jsont ai_domain_baset::output_json( - const ai_baset &ai, - const namespacet &ns) const +jsont ai_domain_baset::output_json(const ai_baset &ai, const namespacet &ns) + const { std::ostringstream out; output(out, ai, ns); @@ -23,14 +22,12 @@ jsont ai_domain_baset::output_json( return json; } -xmlt ai_domain_baset::output_xml( - const ai_baset &ai, - const namespacet &ns) const +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(); + xml.data = out.str(); return xml; } @@ -42,38 +39,38 @@ xmlt ai_domain_baset::output_xml( /// \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 +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) + if(condition.id() == ID_index) { - index_exprt ie=to_index_expr(condition); - bool no_simplification=ai_simplify(ie.index(), ns); + index_exprt ie = to_index_expr(condition); + bool no_simplification = ai_simplify(ie.index(), ns); if(!no_simplification) - condition=simplify_expr(ie, ns); + condition = simplify_expr(ie, ns); return no_simplification; } - else if(condition.id()==ID_dereference) + else if(condition.id() == ID_dereference) { - dereference_exprt de=to_dereference_expr(condition); - bool no_simplification=ai_simplify(de.pointer(), ns); + 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 + condition = simplify_expr(de, ns); // So *(&x) -> x return no_simplification; } - else if(condition.id()==ID_member) + else if(condition.id() == ID_member) { - member_exprt me=to_member_expr(condition); + 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); + bool no_simplification = ai_simplify_lhs(me.compound(), ns); if(!no_simplification) - condition=simplify_expr(me, ns); + condition = simplify_expr(me, ns); return no_simplification; } diff --git a/src/analyses/ai_domain.h b/src/analyses/ai_domain.h index 6554fda837c..055fa982b00 100644 --- a/src/analyses/ai_domain.h +++ b/src/analyses/ai_domain.h @@ -12,10 +12,10 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_ANALYSES_AI_DOMAIN_H #define CPROVER_ANALYSES_AI_DOMAIN_H -#include -#include #include +#include #include +#include #include @@ -61,34 +61,28 @@ class ai_domain_baset ai_baset &ai, const namespacet &ns) = 0; - virtual void output( - std::ostream &out, - const ai_baset &ai, - const namespacet &ns) const + 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 jsont output_json(const ai_baset &ai, const namespacet &ns) const; - virtual xmlt output_xml( - 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; + 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; + virtual void make_top() = 0; // a reasonable entry-point state - virtual void make_entry()=0; + virtual void make_entry() = 0; - virtual bool is_bottom() const=0; + virtual bool is_bottom() const = 0; - virtual bool is_top() const=0; + virtual bool is_top() const = 0; // also add // @@ -102,23 +96,18 @@ class ai_domain_baset // 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 + 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; + 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. From 4f8d44571eb8966ba1d9ed25cba94fdd48df45f4 Mon Sep 17 00:00:00 2001 From: martin Date: Tue, 24 Jul 2018 15:30:29 +0100 Subject: [PATCH 5/6] Upgrade from a warning in the comments to a protected constructor. --- src/analyses/ai_domain.h | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/analyses/ai_domain.h b/src/analyses/ai_domain.h index 055fa982b00..7cb245cbf8a 100644 --- a/src/analyses/ai_domain.h +++ b/src/analyses/ai_domain.h @@ -23,17 +23,16 @@ Author: Daniel Kroening, kroening@kroening.com class ai_baset; /// The interface offered by a domain, allows code to manipulate domains without -/// knowing their exact type. -// don't use me -- I am just a base class -// please derive from me +/// knowing their exact type. Derive from this to implement domains. class ai_domain_baset { -public: +protected: // The constructor is expected to produce 'false' or 'bottom' ai_domain_baset() { } +public: virtual ~ai_domain_baset() { } From 3e0b2a532883c94cf9f7cbaac5312d975b2bac82 Mon Sep 17 00:00:00 2001 From: martin Date: Tue, 24 Jul 2018 15:33:44 +0100 Subject: [PATCH 6/6] Doxygen the comments describing the abstract domain interface. --- src/analyses/ai_domain.h | 78 ++++++++++++++++++++-------------------- 1 file changed, 39 insertions(+), 39 deletions(-) diff --git a/src/analyses/ai_domain.h b/src/analyses/ai_domain.h index 7cb245cbf8a..2dc1b6e33ec 100644 --- a/src/analyses/ai_domain.h +++ b/src/analyses/ai_domain.h @@ -27,7 +27,7 @@ class ai_baset; class ai_domain_baset { protected: - // The constructor is expected to produce 'false' or 'bottom' + /// The constructor is expected to produce 'false' or 'bottom' ai_domain_baset() { } @@ -39,20 +39,20 @@ class 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()) + /// 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, @@ -69,47 +69,47 @@ class ai_domain_baset virtual xmlt output_xml(const ai_baset &ai, const namespacet &ns) const; - // no states + /// no states virtual void make_bottom() = 0; - // all states -- the analysis doesn't use this, - // and domains may refuse to implement it. + /// 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 + /// 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 + /// 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 + /// 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. + /// 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())