From 63bd182e8309a8eb5c2a95d7ee8dc1c39a88605c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Daniel=20Marjam=C3=A4ki?= <daniel.marjamaki@gmail.com>
Date: Wed, 9 Oct 2019 20:17:26 +0200
Subject: [PATCH] ExprEngine: Adapt to z3 handling of bool/int expressions

---
 lib/exprengine.cpp      | 67 +++++++++++++++++++++++++++--------------
 test/testexprengine.cpp | 24 +++++++++++++++
 2 files changed, 68 insertions(+), 23 deletions(-)

diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp
index a0d8a8bef..a54f8128c 100644
--- a/lib/exprengine.cpp
+++ b/lib/exprengine.cpp
@@ -533,7 +533,7 @@ struct ExprData {
         if (b->binop == "%")
             return op1 % op2;
         if (b->binop == "==")
-            return op1 == op2;
+            return int_expr(op1) == int_expr(op2);
         if (b->binop == "!=")
             return op1 != op2;
         if (b->binop == ">=")
@@ -545,9 +545,9 @@ struct ExprData {
         if (b->binop == "<")
             return op1 < op2;
         if (b->binop == "&&")
-            return op1 && op2;
+            return bool_expr(op1) && bool_expr(op2);
         if (b->binop == "||")
-            return op1 || op2;
+            return bool_expr(op1) || bool_expr(op2);
         if (b->binop == "<<")
             return z3::shl(op1, op2);
         if (b->binop == ">>")
@@ -602,6 +602,21 @@ struct ExprData {
             return (getExpr(v) != 0);
         return getExpr(v);
     }
+
+private:
+
+    z3::expr bool_expr(z3::expr e) {
+        if (e.is_bool())
+            return e;
+        return e != 0;
+    }
+
+    z3::expr int_expr(z3::expr e) {
+        if (e.is_bool())
+            return z3::ite(e, context.int_val(1), context.int_val(0));
+        return e;
+    }
+
 };
 #endif
 
@@ -701,27 +716,33 @@ bool ExprEngine::BinOpResult::isLessThan(ExprEngine::DataBase *dataBase, int val
 std::string ExprEngine::BinOpResult::getExpr(ExprEngine::DataBase *dataBase) const
 {
 #ifdef USE_Z3
-    ExprData exprData;
-    z3::solver solver(exprData.context);
-    z3::expr e = exprData.getExpr(this);
-    exprData.addAssertions(solver);
-    for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
-        solver.add(exprData.getConstraintExpr(constraint));
-    solver.add(e);
-    std::ostringstream os;
-    os << solver;
-    switch (solver.check()) {
-    case z3::sat:
-        os << "z3::sat";
-        break;
-    case z3::unsat:
-        os << "z3::unsat";
-        break;
-    case z3::unknown:
-        os << "z3::unknown";
-        break;
+    try {
+        ExprData exprData;
+        z3::solver solver(exprData.context);
+        z3::expr e = exprData.getExpr(this);
+        exprData.addAssertions(solver);
+        for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
+            solver.add(exprData.getConstraintExpr(constraint));
+        solver.add(e);
+        std::ostringstream os;
+        os << solver;
+        switch (solver.check()) {
+        case z3::sat:
+            os << "z3::sat";
+            break;
+        case z3::unsat:
+            os << "z3::unsat";
+            break;
+        case z3::unknown:
+            os << "z3::unknown";
+            break;
+        }
+        return os.str();
+    } catch (const z3::exception &exception) {
+        std::ostringstream os;
+        os << "z3:" << exception;
+        return os.str();
     }
-    return os.str();
 #else
     (void)dataBase;
     return "";
diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp
index f0a74e725..20d153984 100644
--- a/test/testexprengine.cpp
+++ b/test/testexprengine.cpp
@@ -39,6 +39,7 @@ private:
         TEST_CASE(expr4);
         TEST_CASE(expr5);
         TEST_CASE(expr6);
+        TEST_CASE(expr7);
         TEST_CASE(exprAssign1);
         TEST_CASE(exprAssign2); // Truncation
 
@@ -174,6 +175,29 @@ private:
                       expr(code, ">"));
     }
 
+    void expr7() {
+        const char code[] = "void f(bool a, bool b, int c) {\n"
+                            "    if (a||b) {}\n"
+                            "    c > 1000;"
+                            "}";
+
+        ASSERT_EQUALS("(declare-fun $3 () Int)\n"
+                      "(declare-fun $2 () Int)\n"
+                      "(declare-fun $1 () Int)\n"
+                      "(assert (and (>= $3 (- 2147483648)) (<= $3 2147483647)))\n"
+                      "(assert (or (distinct $1 0) (distinct $2 0)))\n"
+                      "(assert (> $3 1000))\n"
+                      "z3::sat\n"
+                      "(declare-fun $3 () Int)\n"
+                      "(declare-fun $2 () Int)\n"
+                      "(declare-fun $1 () Int)\n"
+                      "(assert (and (>= $3 (- 2147483648)) (<= $3 2147483647)))\n"
+                      "(assert (= (ite (or (distinct $1 0) (distinct $2 0)) 1 0) 0))\n"
+                      "(assert (> $3 1000))\n"
+                      "z3::sat",
+                      expr(code, ">"));
+    }
+
     void exprAssign1() {
         ASSERT_EQUALS("($1)+(1)", getRange("void f(unsigned char a) { a += 1; }", "a+=1"));
     }