From 9723b28385b1fe3d82c93faf179f146a8a961134 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Daniel=20Marjam=C3=A4ki?= <daniel.marjamaki@gmail.com>
Date: Sun, 29 Dec 2019 18:42:35 +0100
Subject: [PATCH] Verification; struct pointer member

---
 lib/exprengine.cpp      | 30 +++++++++++++++++++++++-------
 test/testexprengine.cpp | 30 +++++++++++++++++++++---------
 2 files changed, 44 insertions(+), 16 deletions(-)

diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp
index fefe4a239..1b5c51c0d 100644
--- a/lib/exprengine.cpp
+++ b/lib/exprengine.cpp
@@ -1142,9 +1142,20 @@ static ExprEngine::ValuePtr executeDot(const Token *tok, Data &data)
     if (!structValue) {
         if (tok->originalName() == "->") {
             std::shared_ptr<ExprEngine::ArrayValue> pointerValue = std::dynamic_pointer_cast<ExprEngine::ArrayValue>(data.getValue(tok->astOperand1()->varId(), nullptr, nullptr));
-            if (pointerValue && pointerValue->pointer && pointerValue->data.size() == 1) {
+            if (pointerValue && pointerValue->pointer && !pointerValue->data.empty()) {
                 call(data.callbacks, tok->astOperand1(), pointerValue, &data);
-                structValue = std::dynamic_pointer_cast<ExprEngine::StructValue>(pointerValue->data[0].value);
+                auto indexValue = std::make_shared<ExprEngine::IntRange>("0", 0, 0);
+                ExprEngine::ValuePtr ret;
+                for (auto val: pointerValue->read(indexValue)) {
+                    structValue = std::dynamic_pointer_cast<ExprEngine::StructValue>(val.second);
+                    if (structValue) {
+                        auto memberValue = structValue->getValueOfMember(tok->astOperand2()->str());
+                        call(data.callbacks, tok, memberValue, &data);
+                        if (!ret)
+                            ret = memberValue;
+                    }
+                }
+                return ret;
             } else {
                 call(data.callbacks, tok->astOperand1(), data.getValue(tok->astOperand1()->varId(), nullptr, nullptr), &data);
             }
@@ -1524,11 +1535,16 @@ static ExprEngine::ValuePtr createVariableValue(const Variable &var, Data &data)
     if (valueType->pointer > 0) {
         if (var.isLocal())
             return std::make_shared<ExprEngine::UninitValue>();
-        ValueType vt(*valueType);
-        vt.pointer = 0;
-        auto range = getValueRangeFromValueType(data.getNewSymbolName(), &vt, *data.settings);
-        auto size = std::make_shared<ExprEngine::IntRange>(data.getNewSymbolName(), 1, ~0UL);
-        return std::make_shared<ExprEngine::ArrayValue>(data.getNewSymbolName(), size, range, true, true, true);
+        auto bufferSize = std::make_shared<ExprEngine::IntRange>(data.getNewSymbolName(), 1, ~0UL);
+        ExprEngine::ValuePtr pointerValue;
+        if (valueType->type == ValueType::Type::RECORD)
+            pointerValue = createStructVal(valueType->typeScope, var.isLocal() && !var.isStatic(), data);
+        else {
+            ValueType vt(*valueType);
+            vt.pointer = 0;
+            pointerValue = getValueRangeFromValueType(data.getNewSymbolName(), &vt, *data.settings);
+        }
+        return std::make_shared<ExprEngine::ArrayValue>(data.getNewSymbolName(), bufferSize, pointerValue, true, true, true);
     }
     if (var.isArray())
         return std::make_shared<ExprEngine::ArrayValue>(&data, &var);
diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp
index f2a4d8031..0b7e1b944 100644
--- a/test/testexprengine.cpp
+++ b/test/testexprengine.cpp
@@ -81,7 +81,8 @@ private:
         TEST_CASE(pointerAlias4);
         TEST_CASE(pointerNull1);
 
-        TEST_CASE(structMember);
+        TEST_CASE(structMember1);
+        TEST_CASE(structMember2);
 #endif
     }
 
@@ -415,19 +416,19 @@ private:
 
     void pointer1() {
         const char code[] = "void f(unsigned char *p) { return *p == 7; }";
-        ASSERT_EQUALS("size=$2,[:]=$1,null,->?", getRange(code, "p"));
-        ASSERT_EQUALS("(declare-fun |$1:0| () Int)\n"
-                      "(assert (and (>= |$1:0| 0) (<= |$1:0| 255)))\n"
-                      "(assert (= |$1:0| 7))\n"
+        ASSERT_EQUALS("size=$1,[:]=$2,null,->?", getRange(code, "p"));
+        ASSERT_EQUALS("(declare-fun |$2:0| () Int)\n"
+                      "(assert (and (>= |$2:0| 0) (<= |$2:0| 255)))\n"
+                      "(assert (= |$2:0| 7))\n"
                       "z3::sat",
                       expr(code, "=="));
     }
 
     void pointer2() {
         const char code[] = "void f(unsigned char *p) { return p[2] == 7; }";
-        ASSERT_EQUALS("(declare-fun |$1:2| () Int)\n"
-                      "(assert (and (>= |$1:2| 0) (<= |$1:2| 255)))\n"
-                      "(assert (= |$1:2| 7))\n"
+        ASSERT_EQUALS("(declare-fun |$2:2| () Int)\n"
+                      "(assert (and (>= |$2:2| 0) (<= |$2:2| 255)))\n"
+                      "(assert (= |$2:2| 7))\n"
                       "z3::sat",
                       expr(code, "=="));
     }
@@ -458,7 +459,7 @@ private:
     }
 
 
-    void structMember() {
+    void structMember1() {
         ASSERT_EQUALS("(declare-fun $2 () Int)\n"
                       "(declare-fun $3 () Int)\n"
                       "(assert (and (>= $2 0) (<= $2 255)))\n"
@@ -472,6 +473,17 @@ private:
                            "void f(struct S s) { return s.a + s.b == 0; }", "=="));
     }
 
+    void structMember2() {
+        const char code[] = "struct S { int x; };\n"
+                            "void foo(struct S *s) { return s->x == 123; }";
+
+        const char expected[] = "(declare-fun $3 () Int)\n"
+                                "(assert (and (>= $3 (- 2147483648)) (<= $3 2147483647)))\n"
+                                "(assert (= $3 123))\n"
+                                "z3::sat";
+
+        ASSERT_EQUALS(expected, expr(code, "=="));
+    }
 };
 
 REGISTER_TEST(TestExprEngine)