Feature/context sensitive ait merge 1

src/analyses/Makefile

@@ -1,4 +1,5 @@
 SRC = ai.cpp \
+      ai_domain.cpp \
       call_graph.cpp \
       call_graph_helpers.cpp \
       constant_propagator.cpp \

src/analyses/ai.cpp

@@ -15,80 +15,11 @@ Author: Daniel Kroening, [email protected]
 #include <memory>
 #include <sstream>
 
-#include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/std_code.h>
 
 #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,

src/analyses/ai.h

@@ -23,105 +23,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/goto_model.h>
 
-// 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

src/analyses/ai_domain.cpp

@@ -0,0 +1,79 @@
+/*******************************************************************\
+
+Module: Abstract Interpretation
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Abstract Interpretation Domain
+
+#include "ai_domain.h"
+
+#include <util/simplify_expr.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;
+}

src/analyses/ai_domain.h

@@ -0,0 +1,122 @@
+/*******************************************************************\
+
+Module: Abstract Interpretation
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Abstract Interpretation Domain
+
+#ifndef CPROVER_ANALYSES_AI_DOMAIN_H
+#define CPROVER_ANALYSES_AI_DOMAIN_H
+
+#include <util/expr.h>
+#include <util/json.h>
+#include <util/make_unique.h>
+#include <util/xml.h>
+
+#include <goto-programs/goto_model.h>
+
+// 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