ExprEngine: Added ifIntRangeAlwaysFalse and ifIntRangeAlwaysTrue tests

danmar · danmar · commit 5701f6d36877 · 2020-12-20T19:04:46.000+01:00
diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp
@@ -2504,6 +2504,9 @@ static std::string execute(const Token *start, const Token *end, Data &data)
             if (auto b = std::dynamic_pointer_cast<ExprEngine::BinOpResult>(condValue)) {
                 canBeFalse = b->isEqual(&data, 0);
                 canBeTrue = b->isTrue(&data);
+            } else if (auto i = std::dynamic_pointer_cast<ExprEngine::IntRange>(condValue)) {
+                canBeFalse = i->isEqual(&data, 0);
+                canBeTrue = ExprEngine::BinOpResult("!=", i, std::make_shared<ExprEngine::IntRange>("0", 0, 0)).isTrue(&data);
             }
 
             Data &thenData(data);
diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp
@@ -65,6 +65,8 @@ class TestExprEngine : public TestFixture {
         TEST_CASE(ifelse1);
         TEST_CASE(ifif);
         TEST_CASE(ifreturn);
+        TEST_CASE(ifIntRangeAlwaysFalse);
+        TEST_CASE(ifIntRangeAlwaysTrue);
 
         TEST_CASE(istream);
 
@@ -487,6 +489,40 @@ class TestExprEngine : public TestFixture {
                       expr(code, "=="));
     }
 
+    void ifIntRangeAlwaysFalse() {
+        const char code[] = "void foo(unsigned char x) {\n"
+                            "  if (x > 0)\n"
+                            "      return;\n"
+                            "  if (x) {\n"  // <-- condition should be "always false".
+                            "      x++;\n"
+                            "  }\n"
+                            "  return x == 0;\n" // <- sat
+                            "}";
+        ASSERT_EQUALS("(<= $1 0)\n"
+                      "(= $1 0)\n"
+                      "(and (>= $1 0) (<= $1 255))\n"
+                      "(= $1 0)\n"
+                      "z3::sat\n",
+                      expr(code, "=="));
+    }
+
+    void ifIntRangeAlwaysTrue() {
+        const char code[] = "void foo(unsigned char x) {\n"
+                            "  if (x < 1)\n"
+                            "      return;\n"
+                            "  if (x) {\n"  // <-- condition should be "always true".
+                            "      x++;\n"
+                            "  }\n"
+                            "  return x == 0;\n" // <- unsat
+                            "}";
+        ASSERT_EQUALS("(>= $1 1)\n"
+                      "(distinct $1 0)\n"
+                      "(and (>= $1 0) (<= $1 255))\n"
+                      "(= (+ $1 1) 0)\n"
+                      "z3::unsat\n",
+                      expr(code, "=="));
+    }
+
     void istream() {
         const char code[] = "void foo(const std::string& in) {\n"
                             "    std::istringstream istr(in);\n"

Original file line number	Diff line number	Diff line change
`@@ -2504,6 +2504,9 @@ static std::string execute(const Token start, const Token end, Data &data)`
`2504`	`2504`	`if (auto b = std::dynamic_pointer_cast<ExprEngine::BinOpResult>(condValue)) {`
`2505`	`2505`	`canBeFalse = b->isEqual(&data, 0);`
`2506`	`2506`	`canBeTrue = b->isTrue(&data);`
	`2507`	`+ } else if (auto i = std::dynamic_pointer_cast<ExprEngine::IntRange>(condValue)) {`
	`2508`	`+ canBeFalse = i->isEqual(&data, 0);`
	`2509`	`+ canBeTrue = ExprEngine::BinOpResult("!=", i, std::make_shared<ExprEngine::IntRange>("0", 0, 0)).isTrue(&data);`
`2507`	`2510`	`}`
`2508`	`2511`
`2509`	`2512`	`Data &thenData(data);`