ExprEngine: Add FP and String literals in determining that condition can (danmar#2969)

jubnzv · web-flow · commit 0731df7d2dcb · 2020-12-22T09:25:54.000+01:00
diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp
@@ -1404,13 +1404,13 @@ bool ExprEngine::IntRange::isLessThan(DataBase *dataBase, int value) const
 
 bool ExprEngine::FloatRange::isEqual(DataBase *dataBase, int value) const
 {
-    const Data *data = dynamic_cast<Data *>(dataBase);
-    if (data->constraints.empty())
-        return true;
     if (MathLib::isFloat(name)) {
         float f = MathLib::toDoubleNumber(name);
         return value >= f - 0.00001 && value <= f + 0.00001;
     }
+    const Data *data = dynamic_cast<Data *>(dataBase);
+    if (data->constraints.empty())
+        return true;
 #ifdef USE_Z3
     // Check the value against the constraints
     ExprData exprData;
@@ -2555,6 +2555,12 @@ static std::string execute(const Token *start, const Token *end, Data &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);
+            } else if (std::dynamic_pointer_cast<ExprEngine::StringLiteralValue>(condValue)) {
+                canBeFalse = false;
+                canBeTrue = true;
+            } else if (auto f = std::dynamic_pointer_cast<ExprEngine::FloatRange>(condValue)) {
+                canBeFalse = f->isEqual(&data, 0);
+                canBeTrue = ExprEngine::BinOpResult("!=", f, std::make_shared<ExprEngine::FloatRange>("0.0", 0.0, 0.0)).isTrue(&data);
             }
 
             Data &thenData(data);
diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp
@@ -62,6 +62,11 @@ class TestExprEngine : public TestFixture {
         TEST_CASE(if3);
         TEST_CASE(if4);
         TEST_CASE(if5);
+        TEST_CASE(ifAlwaysTrue1);
+        TEST_CASE(ifAlwaysTrue2);
+        TEST_CASE(ifAlwaysTrue3);
+        TEST_CASE(ifAlwaysFalse1);
+        TEST_CASE(ifAlwaysFalse2);
         TEST_CASE(ifelse1);
         TEST_CASE(ifif);
         TEST_CASE(ifreturn);
@@ -152,6 +157,7 @@ class TestExprEngine : public TestFixture {
             }
             replace(line, "(fp.gt ", "(> ");
             replace(line, "(fp.lt ", "(< ");
+            replace(line, "(_ +zero 11 53)", "0.0");
             replace(line, "(fp #b0 #b10000000010 #x899999999999a)", "12.3");
             replace(line, "(/ 123.0 10.0)", "12.3");
             int par = 0;
@@ -448,6 +454,73 @@ class TestExprEngine : public TestFixture {
                       expr("void foo(const int *x) { if (f1() && *x > 12) dostuff(*x == 5); }", "=="));
     }
 
+    void ifAlwaysTrue1() {
+        const char code[] = "int foo() {\n"
+                            "  int a = 42;\n"
+                            "  if (1) {\n"
+                            "    a = 0;\n"
+                            "  }\n"
+                            "  return a == 0;\n"
+                            "}";
+        const char expected[] = "(distinct 1 0)\n"
+                                "(= 0 0)\n"
+                                "z3::sat\n";
+        ASSERT_EQUALS(expected, expr(code, "=="));
+    }
+
+    void ifAlwaysTrue2() {
+        const char code[] = "int foo() {\n"
+                            "  int a = 42;\n"
+                            "  if (12.3) {\n"
+                            "    a = 0;\n"
+                            "  }\n"
+                            "  return a == 0;\n"
+                            "}";
+        const char expected[] = "(distinct 12.3 0.0)\n"
+                                "(= 0 0)\n"
+                                "z3::sat\n";
+        ASSERT_EQUALS(expected, expr(code, "=="));
+    }
+
+    void ifAlwaysTrue3() {
+        const char code[] = "int foo() {\n"
+                            "  int a = 42;\n"
+                            "  if (\"test\") {\n"
+                            "    a = 0;\n"
+                            "  }\n"
+                            "  return a == 0;\n"
+                            "}";
+        // String literals are always true. z3 will not be involved.
+        ASSERT_EQUALS("", expr(code, "=="));
+    }
+
+    void ifAlwaysFalse1() {
+        const char code[] = "int foo() {\n"
+                            "  int a = 42;\n"
+                            "  if (0) {\n"
+                            "    a = 0;\n"
+                            "  }\n"
+                            "  return a == 0;\n"
+                            "}";
+        const char expected[] = "(= 0 0)\n"
+                                "(= 42 0)\n"
+                                "z3::unsat\n";
+        ASSERT_EQUALS(expected, expr(code, "=="));
+    }
+
+    void ifAlwaysFalse2() {
+        const char code[] = "int foo() {\n"
+                            "  int a = 42;\n"
+                            "  if (0.0) {\n"
+                            "    a = 0;\n"
+                            "  }\n"
+                            "  return a == 0;\n"
+                            "}";
+        const char expected[] = "(= 0.0 0.0)\n"
+                                "(= 42 0)\n"
+                                "z3::unsat\n";
+        ASSERT_EQUALS(expected, expr(code, "=="));
+    }
 
     void ifelse1() {
         ASSERT_EQUALS("(<= $1 5)\n"
