From d0f700305c11d636b9bc42e15001e71c8bf54c1c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Daniel=20Marjam=C3=A4ki?= <daniel.marjamaki@gmail.com>
Date: Sat, 12 Dec 2020 15:22:33 +0100
Subject: [PATCH] ExprEngine: Avoid analyzing unreachable execution paths

---
 lib/exprengine.cpp      | 31 +++++++++++++++++++++++--------
 test/testexprengine.cpp | 22 ++++++++++++++++++++++
 2 files changed, 45 insertions(+), 8 deletions(-)

diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp
index 933490df2..6cba2f79d 100644
--- a/lib/exprengine.cpp
+++ b/lib/exprengine.cpp
@@ -1178,7 +1178,6 @@ public:
         return bool_expr(getExpr(v));
     }
 
-private:
     z3::expr bool_expr(z3::expr e) {
         if (e.is_bool())
             return e;
@@ -1375,7 +1374,7 @@ bool ExprEngine::BinOpResult::isEqual(ExprEngine::DataBase *dataBase, int value)
     z3::expr e = exprData.getExpr(this);
     exprData.addConstraints(solver, dynamic_cast<const Data *>(dataBase));
     exprData.addAssertions(solver);
-    solver.add(e == value);
+    solver.add(exprData.int_expr(e) == value);
     return solver.check() == z3::sat;
 #else
     (void)dataBase;
@@ -1437,6 +1436,7 @@ bool ExprEngine::BinOpResult::isTrue(ExprEngine::DataBase *dataBase) const
         z3::expr e = exprData.getExpr(this);
         exprData.addConstraints(solver, dynamic_cast<const Data *>(dataBase));
         exprData.addAssertions(solver);
+        solver.add(exprData.int_expr(e) != 0);
         return solver.check() == z3::sat;
     } catch (const z3::exception &exception) {
         std::cerr << "z3:" << exception << std::endl;
@@ -2343,6 +2343,14 @@ static std::string execute(const Token *start, const Token *end, Data &data)
         else if (Token::simpleMatch(tok, "if (")) {
             const Token *cond = tok->next()->astOperand2(); // TODO: C++17 condition
             const ExprEngine::ValuePtr condValue = executeExpression(cond, data);
+
+            bool alwaysFalse = false;
+            bool alwaysTrue = false;
+            if (auto b = std::dynamic_pointer_cast<ExprEngine::BinOpResult>(condValue)) {
+                alwaysFalse = !b->isTrue(&data);
+                alwaysTrue = !alwaysFalse && !b->isEqual(&data, 0);
+            }
+
             Data &thenData(data);
             Data elseData(data);
             thenData.addConstraint(condValue, true);
@@ -2364,18 +2372,25 @@ static std::string execute(const Token *start, const Token *end, Data &data)
                 }
             };
 
-            exec(thenStart->next(), end, thenData);
+            if (!alwaysFalse)
+                exec(thenStart->next(), end, thenData);
 
-            if (Token::simpleMatch(thenEnd, "} else {")) {
-                const Token *elseStart = thenEnd->tokAt(2);
-                exec(elseStart->next(), end, elseData);
-            } else {
-                exec(thenEnd, end, elseData);
+            if (!alwaysTrue) {
+                if (Token::simpleMatch(thenEnd, "} else {")) {
+                    const Token *elseStart = thenEnd->tokAt(2);
+                    exec(elseStart->next(), end, elseData);
+                } else {
+                    exec(thenEnd, end, elseData);
+                }
             }
 
             if (exceptionToken)
                 throw ExprEngineException(exceptionToken, exceptionMessage);
 
+            if (alwaysTrue)
+                return thenData.str();
+            else if (alwaysFalse)
+                return elseData.str();
             return thenData.str() + elseData.str();
         }
 
diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp
index 12b3636b1..32cfde7e1 100644
--- a/test/testexprengine.cpp
+++ b/test/testexprengine.cpp
@@ -62,6 +62,7 @@ private:
         TEST_CASE(if4);
         TEST_CASE(if5);
         TEST_CASE(ifelse1);
+        TEST_CASE(ifif);
 
         TEST_CASE(istream);
 
@@ -438,6 +439,27 @@ private:
     }
 
 
+    void ifif() {
+        const char code[] = "void foo(unsigned char x) {\n"
+                            "    if (x > 5) {}\n"
+                            "    if (x > 5) {}\n"
+                            "    return x == 13;\n"
+                            "}";
+
+        ASSERT_EQUALS("(> $1 5)\n"
+                      "(> $1 5)\n"
+                      "(and (>= $1 0) (<= $1 255))\n"
+                      "(= $1 13)\n"
+                      "z3::sat\n"
+                      "(<= $1 5)\n"
+                      "(<= $1 5)\n"
+                      "(and (>= $1 0) (<= $1 255))\n"
+                      "(= $1 13)\n"
+                      "z3::unsat\n",
+                      expr(code, "=="));
+    }
+
+
     void istream() {
         const char code[] = "void foo(const std::string& in) {\n"
                             "    std::istringstream istr(in);\n"