Merge pull request #961 from martin-cs/goto-analyzer-5-part2

Goto analyzer 5 part2

Author: kroening

src/analyses/ai.cpp

@@ -8,7 +8,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <cassert>
 #include <memory>
+#include <sstream>
 
+#include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/std_code.h>
 
@@ -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:

src/analyses/ai.h

@@ -11,10 +11,10 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <map>
 #include <iosfwd>
-#include <sstream>
 
 #include <util/json.h>
 #include <util/xml.h>
+#include <util/expr.h>
 
 #include <goto-programs/goto_model.h>
 
@@ -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

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:

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:

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;
+}

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<irep_idt, integer_intervalt> int_mapt;

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)

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();