diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp index 45d4b83c92c..6c0ff3eb225 100644 --- a/src/analyses/ai.cpp +++ b/src/analyses/ai.cpp @@ -8,7 +8,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include +#include #include #include @@ -18,6 +20,103 @@ Author: Daniel Kroening, kroening@kroening.com /*******************************************************************\ +Function: ai_domain_baset::output_json + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +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; +} + +/*******************************************************************\ + +Function: ai_domain_baset::output_xml + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +xmlt ai_domain_baset::output_xml( + const ai_baset &ai, + const namespacet &ns) const +{ + std::ostringstream out; + output(out, ai, ns); + xmlt xml("domain"); + xml.data=out.str(); + return xml; +} + +/*******************************************************************\ + +Function: variable_sensitivity_domaint::ai_simplify_lhs + + Inputs: + condition - the expression to simplify + ns - the namespace + + Outputs: True if condition did not change. False otherwise. condition + will be updated with the simplified condition if it has worked + + Purpose: 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 +\*******************************************************************/ + +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 changed=ai_simplify(ie.index(), ns); + if(changed) + condition=simplify_expr(ie, ns); + + return !changed; + } + else if(condition.id()==ID_dereference) + { + dereference_exprt de=to_dereference_expr(condition); + bool changed=ai_simplify(de.pointer(), ns); + if(changed) + condition=simplify_expr(de, ns); // So *(&x) -> x + + return !changed; + } + else if(condition.id()==ID_member) + { + member_exprt me=to_member_expr(condition); + bool changed=ai_simplify_lhs(me.compound(), ns); // <-- lhs! + if(changed) + condition=simplify_expr(me, ns); + + return !changed; + } + else + return true; +} + +/*******************************************************************\ + Function: ai_baset::output Inputs: diff --git a/src/analyses/ai.h b/src/analyses/ai.h index 2894cde3b10..50838f8ee51 100644 --- a/src/analyses/ai.h +++ b/src/analyses/ai.h @@ -11,10 +11,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include +#include #include @@ -59,24 +59,11 @@ class ai_domain_baset virtual jsont output_json( const ai_baset &ai, - const namespacet &ns) const - { - std::ostringstream out; - output(out, ai, ns); - json_stringt json(out.str()); - return json; - } + const namespacet &ns) const; virtual xmlt output_xml( const ai_baset &ai, - const namespacet &ns) const - { - std::ostringstream out; - output(out, ai, ns); - xmlt xml("domain"); - xml.data=out.str(); - return xml; - } + const namespacet &ns) const; // no states virtual void make_bottom()=0; @@ -94,6 +81,23 @@ class ai_domain_baset // // This computes the join between "this" and "b". // Return true if "this" has changed. + + // 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; }; // don't use me -- I am just a base class diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index 322004a67b5..aa4129faae2 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -333,6 +333,29 @@ void constant_propagator_domaint::assign( /*******************************************************************\ +Function: constant_propagator_domaint::ai_simplify + + Inputs: The condition to simplify and its namespace. + + Outputs: The simplified condition. + + Purpose: Simplify the condition given context-sensitive knowledge + from the abstract state. + +\*******************************************************************/ + +bool constant_propagator_domaint::ai_simplify( + exprt &condition, + const namespacet &ns) const +{ + bool b=values.replace_const.replace(condition); + b&=simplify(condition, ns); + + return b; +} + +/*******************************************************************\ + Function: constant_propagator_domaint::is_array_constant Inputs: diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h index 0766b458f7d..e4a1e147525 100644 --- a/src/analyses/constant_propagator.h +++ b/src/analyses/constant_propagator.h @@ -30,6 +30,10 @@ class constant_propagator_domaint:public ai_domain_baset void make_entry() final { values.set_to_top(); } bool merge(const constant_propagator_domaint &, locationt, locationt); + virtual bool ai_simplify( + exprt &condition, + const namespacet &ns) const override; + struct valuest { public: diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index 7ac597bb6ca..8dc49db8b4e 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -129,20 +129,29 @@ void interval_domaint::transform( /*******************************************************************\ -Function: interval_domaint::merge +Function: interval_domaint::join - Inputs: + Inputs: The interval domain, b, to join to this domain. - Outputs: + Outputs: True if the join increases the set represented by *this, + False if there is no change. - Purpose: + Purpose: Sets *this to the mathematical join between the two domains. + This can be thought of as an abstract version of union; + *this is increased so that it contains all of the values that + are represented by b as well as its original intervals. + The result is an overapproximation, for example: + "[0,1]".join("[3,4]") --> "[0,4]" + includes 2 which isn't in [0,1] or [3,4]. + + Join is used in several places, the most significant being + merge, which uses it to bring together two different paths + of analysis. \*******************************************************************/ -bool interval_domaint::merge( - const interval_domaint &b, - locationt from, - locationt to) +bool interval_domaint::join( + const interval_domaint &b) { if(b.bottom) return false; @@ -527,3 +536,67 @@ exprt interval_domaint::make_expression(const symbol_exprt &src) const else return true_exprt(); } + +/*******************************************************************\ + +Function: interval_domaint::simplify + + Inputs: The expression to simplify. + + Outputs: A simplified version of the expression. + + Purpose: Uses the abstract state to simplify a given expression + using context-specific information. + +\*******************************************************************/ + +/* + * This implementation is aimed at reducing assertions to true, particularly + * range checks for arrays and other bounds checks. + * + * Rather than work with the various kinds of exprt directly, we use assume, + * join and is_bottom. It is sufficient for the use case and avoids duplicating + * functionality that is in assume anyway. + * + * As some expressions (1<=a && a<=2) can be represented exactly as intervals + * and some can't (a<1 || a>2), the way these operations are used varies + * depending on the structure of the expression to try to give the best results. + * For example negating a disjunction makes it easier for assume to handle. + */ + +bool interval_domaint::ai_simplify( + exprt &condition, + const namespacet &ns) const +{ + bool unchanged=true; + interval_domaint d(*this); + + // merge intervals to properly handle conjunction + if(condition.id()==ID_and) // May be directly representable + { + interval_domaint a; + a.make_top(); // a is everything + a.assume(condition, ns); // Restrict a to an over-approximation + // of when condition is true + if(!a.join(d)) // If d (this) is included in a... + { // Then the condition is always true + unchanged=condition.is_true(); + condition.make_true(); + } + } + else if(condition.id()==ID_symbol) + { + // TODO: we have to handle symbol expression + } + else // Less likely to be representable + { + d.assume(not_exprt(condition), ns); // Restrict to when condition is false + if(d.is_bottom()) // If there there are none... + { // Then the condition is always true + unchanged=condition.is_true(); + condition.make_true(); + } + } + + return unchanged; +} diff --git a/src/analyses/interval_domain.h b/src/analyses/interval_domain.h index 7e95c65e9de..388107e7233 100644 --- a/src/analyses/interval_domain.h +++ b/src/analyses/interval_domain.h @@ -40,10 +40,17 @@ class interval_domaint:public ai_domain_baset const ai_baset &ai, const namespacet &ns) const final; +protected: + bool join(const interval_domaint &b); + +public: bool merge( const interval_domaint &b, locationt from, - locationt to); + locationt to) + { + return join(b); + } // no states void make_bottom() final @@ -85,7 +92,11 @@ class interval_domaint:public ai_domain_baset return bottom; } -private: + virtual bool ai_simplify( + exprt &condition, + const namespacet &ns) const override; + +protected: bool bottom; typedef std::map int_mapt; diff --git a/src/goto-programs/remove_unreachable.cpp b/src/goto-programs/remove_unreachable.cpp index ac6df4261a8..57211e8ad9b 100644 --- a/src/goto-programs/remove_unreachable.cpp +++ b/src/goto-programs/remove_unreachable.cpp @@ -56,6 +56,19 @@ void remove_unreachable(goto_programt &goto_program) } } +/*******************************************************************\ + +Function: remove_unreachable + + Inputs: The goto functions from which the unreachable functions are + to be removed. + + Outputs: None. + + Purpose: Removes unreachable instructions from all functions. + +\*******************************************************************/ + void remove_unreachable(goto_functionst &goto_functions) { Forall_goto_functions(f_it, goto_functions) diff --git a/src/util/replace_symbol.h b/src/util/replace_symbol.h index f26c8eb067a..525bdd3be09 100644 --- a/src/util/replace_symbol.h +++ b/src/util/replace_symbol.h @@ -56,6 +56,11 @@ class replace_symbolt type_map.clear(); } + bool empty() const + { + return expr_map.empty() && type_map.empty(); + } + replace_symbolt(); virtual ~replace_symbolt();