From d82b1b29cee8a69e8a67d69912ac479957db7f77 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Daniel=20Marjam=C3=A4ki?= <daniel.marjamaki@gmail.com>
Date: Sun, 6 Oct 2019 19:58:51 +0200
Subject: [PATCH] ExprEngine: Initial handling of switch

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

diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp
index 48bf50ea7..39b05e4f6 100644
--- a/lib/exprengine.cpp
+++ b/lib/exprengine.cpp
@@ -225,6 +225,13 @@ namespace {
             else
                 constraints.push_back(notValue(condValue));
         }
+
+        void addConstraint(ExprEngine::ValuePtr lhsValue, ExprEngine::ValuePtr rhsValue, bool equals) {
+            if (!lhsValue || !rhsValue)
+                return;
+            constraints.push_back(std::make_shared<ExprEngine::BinOpResult>(equals?"==":"!=", lhsValue, rhsValue));
+        }
+
     private:
         TrackExecution * const mTrackExecution;
         const int mDataIndex;
@@ -1051,10 +1058,18 @@ static void execute(const Token *start, const Token *end, Data &data)
             continue;
         }
 
-        if (tok->str() == "break")
-            return;
+        if (tok->str() == "break") {
+            const Scope *scope = tok->scope();
+            while (scope->type == Scope::eIf || scope->type == Scope::eElse)
+                scope = scope->nestedIn;
+            tok = scope->bodyEnd;
+        }
 
-        if (Token::Match(tok, "for|while|switch ("))
+        if (Token::simpleMatch(tok, "try"))
+            // TODO this is a bailout
+            throw std::runtime_error("Unhandled:" + tok->str());
+
+        if (Token::Match(tok, "for|while ("))
             // TODO this is a bailout
             throw std::runtime_error("Unhandled:" + tok->str());
 
@@ -1081,11 +1096,14 @@ static void execute(const Token *start, const Token *end, Data &data)
                     tok = tok->linkAt(1);
             } else if (Token::Match(tok, "%var% ;"))
                 data.assignValue(tok, tok->varId(), createVariableValue(*tok->variable(), data));
-        } else if (!tok->astParent() && (tok->astOperand1() || tok->astOperand2()))
+        } else if (!tok->astParent() && (tok->astOperand1() || tok->astOperand2())) {
             executeExpression(tok, data);
+            if (Token::Match(tok, "throw|return"))
+                return;
+        }
 
         else if (Token::simpleMatch(tok, "if (")) {
-            const Token *cond = tok->next()->astOperand2();
+            const Token *cond = tok->next()->astOperand2(); // TODO: C++17 condition
             const ExprEngine::ValuePtr condValue = executeExpression(cond, data);
             Data ifData(data);
             Data elseData(data);
@@ -1104,6 +1122,28 @@ static void execute(const Token *start, const Token *end, Data &data)
             return;
         }
 
+        else if (Token::simpleMatch(tok, "switch (")) {
+            auto condValue = executeExpression(tok->next()->astOperand2(), data); // TODO: C++17 condition
+            const Token *bodyStart = tok->linkAt(1)->next();
+            const Token *bodyEnd = bodyStart->link();
+            const Token *defaultStart = nullptr;
+            Data defaultData(data);
+            for (const Token *tok2 = bodyStart->next(); tok2 != bodyEnd; tok2 = tok2->next()) {
+                if (tok2->str() == "{")
+                    tok2 = tok2->link();
+                else if (Token::Match(tok2, "case %num% :")) {
+                    auto caseValue = std::make_shared<ExprEngine::IntRange>(tok2->strAt(1), MathLib::toLongNumber(tok2->strAt(1)), MathLib::toLongNumber(tok2->strAt(1)));
+                    Data caseData(data);
+                    caseData.addConstraint(condValue, caseValue, true);
+                    defaultData.addConstraint(condValue, caseValue, false);
+                    execute(tok2->tokAt(2), end, caseData);
+                } else if (Token::simpleMatch(tok2, "default :"))
+                    defaultStart = tok2;
+            }
+            execute(defaultStart ? defaultStart : bodyEnd, end, defaultData);
+            return;
+        }
+
         if (Token::simpleMatch(tok, "} else {"))
             tok = tok->linkAt(2);
     }
diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp
index 6063862a6..a6af2ec94 100644
--- a/test/testexprengine.cpp
+++ b/test/testexprengine.cpp
@@ -44,6 +44,8 @@ private:
         TEST_CASE(if1);
         TEST_CASE(ifelse1);
 
+        TEST_CASE(switch1);
+
         TEST_CASE(array1);
         TEST_CASE(array2);
         TEST_CASE(array3);
@@ -85,7 +87,9 @@ private:
             auto b = dynamic_cast<const ExprEngine::BinOpResult *>(&value);
             if (!b)
                 return;
-            ret = b->getExpr(dataBase);
+            if (!ret.empty())
+                ret += "\n";
+            ret += b->getExpr(dataBase);
         };
         std::vector<ExprEngine::Callback> callbacks;
         callbacks.push_back(f);
@@ -181,6 +185,23 @@ private:
     }
 
 
+    void switch1() {
+        const char code[] = "void f(int x) {\n"
+                            "    switch (x) {\n"
+                            "    case 1: x==3; break;\n"
+                            "    case 2: x>0; break;\n"
+                            "    };\n"
+                            "    x<=4;\n"
+                            "}";
+        ASSERT_EQUALS("(declare-fun $1 () Int)\n"
+                      "(assert (<= $1 2147483647))\n"
+                      "(assert (>= $1 (- 2147483648)))\n"
+                      "(assert (= $1 1))\n"
+                      "(assert (= $1 3))\n",
+                      expr(code, "=="));
+    }
+
+
     void array1() {
         ASSERT_EQUALS("(assert (= 5 0))\n",
                       expr("int f() { int arr[10]; arr[4] = 5; return arr[4]==0; }", "=="));