Remove default implementation of `Expr::compareContents(const Expr&)`

and make it a pure virtual method. Also make it protected rather than
public because it is an implementation detail of `Expr::compare()`.

This means that sub classes must implement it so this commit also
provides implementations. The comparision behaves as before except
for `ConcatExpr` where its `width` attribute is now used (previously
it wasn't).

This commit also documents the semantics of `Expr::compareContents(const Expr&)`
which was clearly needed because it has been incorrectly implemented
in the past and has gone unnoticed for several years.

This partially addresses #515 .

1 files changed, 114 insertions, 55 deletions

diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index 500d7d46..26c91ae3 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -176,7 +176,31 @@ public:
 
 protected:  
   unsigned hashValue;
-  
+
+  /// Compares `b` to `this` Expr and determines how they are ordered
+  /// (ignoring their kid expressions - i.e. those returned by `getKid()`).
+  ///
+  /// Typically this requires comparing internal attributes of the Expr.
+  ///
+  /// Implementations can assume that `b` and `this` are of the same kind.
+  ///
+  /// This method effectively defines a partial order over Expr of the same
+  /// kind (partial because kid Expr are not compared).
+  ///
+  /// This method should not be called directly. Instead `compare()` should
+  /// be used.
+  ///
+  /// \param [in] b Expr to compare `this` to.
+  ///
+  /// \return One of the following values:
+  ///
+  /// * -1 if `this` is `<` `b` ignoring kid expressions.
+  /// * 1 if `this` is `>` `b` ignoring kid expressions.
+  /// * 0 if `this` and `b` are not ordered.
+  ///
+  /// `<` and `>` are binary relations that express the partial order.
+  virtual int compareContents(const Expr &b) const = 0;
+
 public:
   Expr() : refCount(0) { Expr::count++; }
   virtual ~Expr() { Expr::count--; } 
@@ -208,7 +232,6 @@ public:
     equivs.clear();
     return r;
   }
-  virtual int compareContents(const Expr &b) const { return 0; }
 
   // Given an array of new kids return a copy of the expression
   // but using those children. 
@@ -404,6 +427,12 @@ public:
 private:
   NotOptimizedExpr(const ref<Expr> &_src) : src(_src) {}
 
+protected:
+  virtual int compareContents(const Expr &b) const {
+    // No attributes to compare.
+    return 0;
+  }
+
 public:
   static bool classof(const Expr *E) {
     return E->getKind() == Expr::NotOptimized;
@@ -625,6 +654,12 @@ public:
     return E->getKind() == Expr::Select;
   }
   static bool classof(const SelectExpr *) { return true; }
+
+protected:
+  virtual int compareContents(const Expr &b) const {
+    // No attributes to compare.
+    return 0;
+  }
 };
 
 
@@ -682,6 +717,14 @@ public:
     return E->getKind() == Expr::Concat;
   }
   static bool classof(const ConcatExpr *) { return true; }
+
+protected:
+  virtual int compareContents(const Expr &b) const {
+    const ConcatExpr &eb = static_cast<const ConcatExpr &>(b);
+    if (width != eb.width)
+      return width < eb.width ? -1 : 1;
+    return 0;
+  }
 };
 
 
@@ -779,6 +822,12 @@ public:
 
 private:
   NotExpr(const ref<Expr> &e) : expr(e) {}
+
+protected:
+  virtual int compareContents(const Expr &b) const {
+    // No attributes to compare.
+    return 0;
+  }
 };
 
 
@@ -846,33 +895,38 @@ CAST_EXPR_CLASS(ZExt)
 
 // Arithmetic/Bit Exprs
 
-#define ARITHMETIC_EXPR_CLASS(_class_kind)                           \
-class _class_kind ## Expr : public BinaryExpr {                      \
-public:                                                              \
-  static const Kind kind = _class_kind;                              \
-  static const unsigned numKids = 2;                                 \
-public:                                                              \
-    _class_kind ## Expr(const ref<Expr> &l,                          \
-                        const ref<Expr> &r) : BinaryExpr(l,r) {}     \
-    static ref<Expr> alloc(const ref<Expr> &l, const ref<Expr> &r) { \
-      ref<Expr> res(new _class_kind ## Expr (l, r));                 \
-      res->computeHash();                                            \
-      return res;                                                    \
-    }                                                                \
-    static ref<Expr> create(const ref<Expr> &l, const ref<Expr> &r); \
-    Width getWidth() const { return left->getWidth(); }              \
-    Kind getKind() const { return _class_kind; }                     \
-    virtual ref<Expr> rebuild(ref<Expr> kids[]) const {              \
-      return create(kids[0], kids[1]);                               \
-    }                                                                \
-                                                                     \
-    static bool classof(const Expr *E) {                             \
-      return E->getKind() == Expr::_class_kind;                      \
-    }                                                                \
-    static bool classof(const  _class_kind ## Expr *) {              \
-      return true;                                                   \
-    }                                                                \
-};                                                                   \
+#define ARITHMETIC_EXPR_CLASS(_class_kind)                                     \
+  class _class_kind##Expr : public BinaryExpr {                                \
+  public:                                                                      \
+    static const Kind kind = _class_kind;                                      \
+    static const unsigned numKids = 2;                                         \
+                                                                               \
+  public:                                                                      \
+    _class_kind##Expr(const ref<Expr> &l, const ref<Expr> &r)                  \
+        : BinaryExpr(l, r) {}                                                  \
+    static ref<Expr> alloc(const ref<Expr> &l, const ref<Expr> &r) {           \
+      ref<Expr> res(new _class_kind##Expr(l, r));                              \
+      res->computeHash();                                                      \
+      return res;                                                              \
+    }                                                                          \
+    static ref<Expr> create(const ref<Expr> &l, const ref<Expr> &r);           \
+    Width getWidth() const { return left->getWidth(); }                        \
+    Kind getKind() const { return _class_kind; }                               \
+    virtual ref<Expr> rebuild(ref<Expr> kids[]) const {                        \
+      return create(kids[0], kids[1]);                                         \
+    }                                                                          \
+                                                                               \
+    static bool classof(const Expr *E) {                                       \
+      return E->getKind() == Expr::_class_kind;                                \
+    }                                                                          \
+    static bool classof(const _class_kind##Expr *) { return true; }            \
+                                                                               \
+  protected:                                                                   \
+    virtual int compareContents(const Expr &b) const {                         \
+      /* No attributes to compare.*/                                           \
+      return 0;                                                                \
+    }                                                                          \
+  };
 
 ARITHMETIC_EXPR_CLASS(Add)
 ARITHMETIC_EXPR_CLASS(Sub)
@@ -890,32 +944,37 @@ ARITHMETIC_EXPR_CLASS(AShr)
 
 // Comparison Exprs
 
-#define COMPARISON_EXPR_CLASS(_class_kind)                           \
-class _class_kind ## Expr : public CmpExpr {                         \
-public:                                                              \
-  static const Kind kind = _class_kind;                              \
-  static const unsigned numKids = 2;                                 \
-public:                                                              \
-    _class_kind ## Expr(const ref<Expr> &l,                          \
-                        const ref<Expr> &r) : CmpExpr(l,r) {}        \
-    static ref<Expr> alloc(const ref<Expr> &l, const ref<Expr> &r) { \
-      ref<Expr> res(new _class_kind ## Expr (l, r));                 \
-      res->computeHash();                                            \
-      return res;                                                    \
-    }                                                                \
-    static ref<Expr> create(const ref<Expr> &l, const ref<Expr> &r); \
-    Kind getKind() const { return _class_kind; }                     \
-    virtual ref<Expr> rebuild(ref<Expr> kids[]) const {              \
-      return create(kids[0], kids[1]);                               \
-    }                                                                \
-                                                                     \
-    static bool classof(const Expr *E) {                             \
-      return E->getKind() == Expr::_class_kind;                      \
-    }                                                                \
-    static bool classof(const  _class_kind ## Expr *) {              \
-      return true;                                                   \
-    }                                                                \
-};                                                                   \
+#define COMPARISON_EXPR_CLASS(_class_kind)                                     \
+  class _class_kind##Expr : public CmpExpr {                                   \
+  public:                                                                      \
+    static const Kind kind = _class_kind;                                      \
+    static const unsigned numKids = 2;                                         \
+                                                                               \
+  public:                                                                      \
+    _class_kind##Expr(const ref<Expr> &l, const ref<Expr> &r)                  \
+        : CmpExpr(l, r) {}                                                     \
+    static ref<Expr> alloc(const ref<Expr> &l, const ref<Expr> &r) {           \
+      ref<Expr> res(new _class_kind##Expr(l, r));                              \
+      res->computeHash();                                                      \
+      return res;                                                              \
+    }                                                                          \
+    static ref<Expr> create(const ref<Expr> &l, const ref<Expr> &r);           \
+    Kind getKind() const { return _class_kind; }                               \
+    virtual ref<Expr> rebuild(ref<Expr> kids[]) const {                        \
+      return create(kids[0], kids[1]);                                         \
+    }                                                                          \
+                                                                               \
+    static bool classof(const Expr *E) {                                       \
+      return E->getKind() == Expr::_class_kind;                                \
+    }                                                                          \
+    static bool classof(const _class_kind##Expr *) { return true; }            \
+                                                                               \
+  protected:                                                                   \
+    virtual int compareContents(const Expr &b) const {                         \
+      /* No attributes to compare. */                                          \
+      return 0;                                                                \
+    }                                                                          \
+  };
 
 COMPARISON_EXPR_CLASS(Eq)
 COMPARISON_EXPR_CLASS(Ne)