From 871cf379d5dd923e30d2301bb012dac76ee6782f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Daniel=20Marjam=C3=A4ki?= <daniel.marjamaki@gmail.com>
Date: Fri, 15 May 2020 21:34:52 +0200
Subject: [PATCH] ExprData: Better handling of ternary operator

---
 lib/exprengine.cpp      | 29 ++++++++++++++++++++++-------
 test/testexprengine.cpp | 16 ++++++++++++++++
 2 files changed, 38 insertions(+), 7 deletions(-)

diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp
index 50595b462..5900fa5a4 100644
--- a/lib/exprengine.cpp
+++ b/lib/exprengine.cpp
@@ -1613,13 +1613,28 @@ static ExprEngine::ValuePtr executeBinaryOp(const Token *tok, Data &data)
     ExprEngine::ValuePtr v1 = executeExpression(tok->astOperand1(), data);
     ExprEngine::ValuePtr v2;
 
-    if (tok->str() == "?" && tok->astOperand1()->hasKnownIntValue()) {
-        if (tok->astOperand1()->getKnownIntValue())
-            v2 = executeExpression(tok->astOperand2()->astOperand1(), data);
-        else
-            v2 = executeExpression(tok->astOperand2()->astOperand2(), data);
-        call(data.callbacks, tok, v2, &data);
-        return v2;
+    if (tok->str() == "?") {
+        if (tok->astOperand1()->hasKnownIntValue()) {
+            if (tok->astOperand1()->getKnownIntValue())
+                v2 = executeExpression(tok->astOperand2()->astOperand1(), data);
+            else
+                v2 = executeExpression(tok->astOperand2()->astOperand2(), data);
+            call(data.callbacks, tok, v2, &data);
+            return v2;
+        }
+
+        Data trueData(data);
+        trueData.addConstraint(v1, true);
+        auto trueValue = simplifyValue(executeExpression(tok->astOperand2()->astOperand1(), trueData));
+
+        Data falseData(data);
+        falseData.addConstraint(v1, false);
+        auto falseValue = simplifyValue(executeExpression(tok->astOperand2()->astOperand2(), falseData));
+
+        auto result = simplifyValue(std::make_shared<ExprEngine::BinOpResult>("?", v1, std::make_shared<ExprEngine::BinOpResult>(":", trueValue, falseValue)));
+        call(data.callbacks, tok, result, &data);
+        return result;
+
     } else if (tok->str() == "&&" || tok->str() == "||") {
         Data data2(data);
         data2.addConstraint(v1, tok->str() == "&&");
diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp
index 5a70a8f26..bb7dc3373 100644
--- a/test/testexprengine.cpp
+++ b/test/testexprengine.cpp
@@ -97,6 +97,8 @@ private:
         TEST_CASE(structMember1);
         TEST_CASE(structMember2);
         TEST_CASE(structMember3);
+
+        TEST_CASE(ternaryOperator1);
 #endif
     }
 
@@ -656,6 +658,20 @@ private:
 
         ASSERT_EQUALS(expected, expr(code, "=="));
     }
+
+
+    void ternaryOperator1() {
+        const char code[] = "void foo(signed char x) {\n"
+                            "  x = (x > 0) ? (0==x) : 0;\n"
+                            "}";
+
+        const char expected[] = "(> $1 0)\n"
+                                "(and (>= $1 (- 128)) (<= $1 127))\n"
+                                "(= 0 $1)\n"
+                                "z3::unsat\n";
+
+        ASSERT_EQUALS(expected, expr(code, "=="));
+    }
 };
 
 REGISTER_TEST(TestExprEngine)