exprengine: better checking for uninit variables

lib/bughuntingchecks.cpp

@@ -199,7 +199,7 @@ static void divByZero(const Token *tok, const ExprEngine::Value &value, ExprEngi
         return;
     if (tok->isImpossibleIntValue(0))
         return;
-    if (value.isUninit() && value.type != ExprEngine::ValueType::BailoutValue)
+    if (value.isUninit(dataBase) && value.type != ExprEngine::ValueType::BailoutValue)
         return;
     float f = getKnownFloatValue(tok, 0.0f);
     if (f > 0.0f || f < 0.0f)
@@ -315,7 +315,7 @@ static void uninit(const Token *tok, const ExprEngine::Value &value, ExprEngine:
 
     std::string uninitStructMember;
     if (const auto* structValue = dynamic_cast<const ExprEngine::StructValue*>(&value)) {
-        uninitStructMember = structValue->getUninitStructMember();
+        uninitStructMember = structValue->getUninitStructMember(dataBase);
 
         // uninitialized struct member => is there data copy of struct..
         if (!uninitStructMember.empty()) {
@@ -325,10 +325,10 @@ static void uninit(const Token *tok, const ExprEngine::Value &value, ExprEngine:
     }
 
     bool uninitData = false;
-    if (!value.isUninit() && uninitStructMember.empty()) {
+    if (!value.isUninit(dataBase) && uninitStructMember.empty()) {
         if (Token::Match(tok->astParent(), "[(,]")) {
             if (const auto* arrayValue = dynamic_cast<const ExprEngine::ArrayValue*>(&value)) {
-                uninitData = arrayValue->data.size() >= 1 && arrayValue->data[0].value->isUninit();
+                uninitData = arrayValue->data.size() >= 1 && arrayValue->data[0].value->isUninit(dataBase);
             }
         }
 
@@ -627,7 +627,7 @@ static void checkFunctionCall(const Token *tok, const ExprEngine::Value &value,
         const ExprEngine::ArrayValue &arrayValue = static_cast<const ExprEngine::ArrayValue &>(value);
         auto index0 = std::make_shared<ExprEngine::IntRange>("0", 0, 0);
         for (const auto &v: arrayValue.read(index0)) {
-            if (v.second->isUninit()) {
+            if (v.second->isUninit(dataBase)) {
                 dataBase->reportError(tok, Severity::SeverityType::error, "bughuntingUninitArg", "There is function call, cannot determine that " + std::to_string(num) + getOrdinalText(num) + " argument is initialized.", CWE_USE_OF_UNINITIALIZED_VARIABLE, false);
                 break;
             }

lib/exprengine.cpp

@@ -150,6 +150,8 @@
 #define Z3_VERSION_INT             GET_VERSION_INT(Z3_MAJOR_VERSION, Z3_MINOR_VERSION, Z3_BUILD_NUMBER)
 #endif
 
+constexpr auto MAX_BUFFER_SIZE = ~0UL;
+
 namespace {
     struct ExprEngineException {
         ExprEngineException(const Token *tok, const std::string &what) : tok(tok), what(what) {}
@@ -201,9 +203,7 @@ static std::string str(ExprEngine::ValuePtr val)
         break;
     }
 
-    std::ostringstream ret;
+    return val->name + "=" + std::string(typestr) + "(" + val->getRange() + ")";
-    ret << val->name << "=" << typestr << "(" << val->getRange() << ")";
-    return ret.str();
 }
 
 static size_t extfind(const std::string &str, const std::string &what, size_t pos)
@@ -341,7 +341,7 @@ namespace {
         }
 
         void ifSplit(const Token *tok, unsigned int thenIndex, unsigned int elseIndex) {
-            mMap[tok].push_back(std::to_string(thenIndex) + ": Split. Then:" + std::to_string(thenIndex) + " Else:" + std::to_string(elseIndex));
+            mMap[tok].push_back("D" + std::to_string(thenIndex) + ": Split. Then:D" + std::to_string(thenIndex) + " Else:D" + std::to_string(elseIndex));
         }
 
     private:
@@ -536,7 +536,7 @@ namespace {
                 return;
             const SymbolDatabase * const symbolDatabase = tokenizer->getSymbolDatabase();
             std::ostringstream s;
-            s << mDataIndex << ":" << "memory:{";
+            s << "D" << mDataIndex << ":" << "memory:{";
             bool first = true;
             for (auto mem : memory) {
                 ExprEngine::ValuePtr value = mem.second;
@@ -1305,6 +1305,32 @@ public:
 };
 #endif
 
+bool ExprEngine::UninitValue::isUninit(const DataBase *dataBase) const {
+    const Data *data = dynamic_cast<const Data *>(dataBase);
+    if (data->constraints.empty())
+        return true;
+#ifdef USE_Z3
+    // Check the value against the constraints
+    ExprData exprData;
+    z3::solver solver(exprData.context);
+    try {
+        exprData.addConstraints(solver, data);
+        exprData.addAssertions(solver);
+        return solver.check() == z3::sat;
+    } catch (const z3::exception &exception) {
+        std::cerr << "z3: " << exception << std::endl;
+        return true;  // Safe option is to return true
+    } catch (const ExprData::BailoutValueException &) {
+        return true;  // Safe option is to return true
+    } catch (const ExprEngineException &) {
+        return true;  // Safe option is to return true
+    }
+#else
+    // The value may or may not be uninitialized
+    return false;
+#endif
+}
+
 bool ExprEngine::IntRange::isEqual(const DataBase *dataBase, int value) const
 {
     if (value < minValue || value > maxValue)
@@ -2180,7 +2206,7 @@ static ExprEngine::ValuePtr executeCast(const Token *tok, Data &data)
             uninitPointer = std::static_pointer_cast<ExprEngine::ArrayValue>(val)->uninitPointer;
         }
 
-        auto bufferSize = std::make_shared<ExprEngine::IntRange>(data.getNewSymbolName(), 1, ~0UL);
+        auto bufferSize = std::make_shared<ExprEngine::IntRange>(data.getNewSymbolName(), 1, MAX_BUFFER_SIZE);
         return std::make_shared<ExprEngine::ArrayValue>(data.getNewSymbolName(), bufferSize, range, true, nullPointer, uninitPointer);
     }
 
@@ -2241,6 +2267,11 @@ static void streamReadSetValue(const Token *tok, Data &data)
 {
     if (!tok || !tok->valueType())
         return;
+    if (tok->varId() > 0 && tok->valueType()->pointer) {
+        const auto oldValue = data.getValue(tok->varId(), tok->valueType(), tok);
+        if (oldValue && (oldValue->isUninit(&data)))
+            call(data.callbacks, tok, oldValue, &data);
+    }
     auto rangeValue = getValueRangeFromValueType(tok->valueType(), data);
     if (rangeValue)
         assignExprValue(tok, rangeValue, data);
@@ -2363,7 +2394,8 @@ static ExprEngine::ValuePtr executeVariable(const Token *tok, Data &data)
 
 static ExprEngine::ValuePtr executeKnownMacro(const Token *tok, Data &data)
 {
-    auto val = std::make_shared<ExprEngine::IntRange>(data.getNewSymbolName(), tok->getKnownIntValue(), tok->getKnownIntValue());
+    const auto intval = tok->getKnownIntValue();
+    auto val = std::make_shared<ExprEngine::IntRange>(std::to_string(intval), intval, intval);
     call(data.callbacks, tok, val, &data);
     return val;
 }
@@ -2508,6 +2540,9 @@ static std::string execute(const Token *start, const Token *end, Data &data)
                 if (Token::Match(prev, "[;{}] return|throw"))
                     return data.str();
             }
+            while (Token::simpleMatch(tok, "} catch (") && Token::simpleMatch(tok->linkAt(2), ") {")) {
+                tok = tok->linkAt(2)->next()->link();
+            }
             if (std::time(nullptr) > stopTime)
                 return "";
         }
@@ -2530,9 +2565,15 @@ static std::string execute(const Token *start, const Token *end, Data &data)
                 return data.str();
         }
 
-        if (Token::simpleMatch(tok, "try"))
+        if (Token::simpleMatch(tok, "try {") && Token::simpleMatch(tok->linkAt(1), "} catch (")) {
-            // TODO this is a bailout
+            const Token *catchTok = tok->linkAt(1);
-            throw ExprEngineException(tok, "Unhandled:" + tok->str());
+            while (Token::simpleMatch(catchTok, "} catch (")) {
+                Data catchData(data);
+                catchTok = catchTok->linkAt(2)->next();
+                execute(catchTok, end, catchData);
+                catchTok = catchTok->link();
+            }
+        }
 
         // Variable declaration..
         if (tok->variable() && tok->variable()->nameToken() == tok) {
@@ -2771,7 +2812,7 @@ static std::string execute(const Token *start, const Token *end, Data &data)
                             continue;
                         changedVariables.insert(varid);
                         auto oldValue = bodyData.getValue(varid, nullptr, nullptr);
-                        if (oldValue && oldValue->isUninit())
+                        if (oldValue && oldValue->isUninit(&bodyData))
                             call(bodyData.callbacks, lhs, oldValue, &bodyData);
                         if (oldValue && oldValue->type == ExprEngine::ValueType::ArrayValue) {
                             // Try to assign "any" value

lib/exprengine.h

@@ -116,7 +116,8 @@ namespace ExprEngine {
             (void)value;
             return false;
         }
-        virtual bool isUninit() const {
+        virtual bool isUninit(const DataBase *dataBase) const {
+            (void)dataBase;
             return false;
         }
 
@@ -132,9 +133,7 @@ namespace ExprEngine {
             (void)value;
             return true;
         }
-        bool isUninit() const OVERRIDE {
+        bool isUninit(const DataBase *dataBase) const OVERRIDE;
-            return true;
-        }
     };
 
     class IntRange : public Value {
@@ -245,9 +244,9 @@ namespace ExprEngine {
             return (it == member.end()) ? ValuePtr() : it->second;
         }
 
-        std::string getUninitStructMember() const {
+        std::string getUninitStructMember(const DataBase *dataBase) const {
             for (auto memberNameValue: member) {
-                if (memberNameValue.second && memberNameValue.second->isUninit())
+                if (memberNameValue.second && memberNameValue.second->isUninit(dataBase))
                     return memberNameValue.first;
             }
             return std::string();
@@ -327,7 +326,8 @@ namespace ExprEngine {
         bool isEqual(const DataBase * /*dataBase*/, int /*value*/) const OVERRIDE {
             return true;
         }
-        bool isUninit() const OVERRIDE {
+        bool isUninit(const DataBase *dataBase) const OVERRIDE {
+            (void)dataBase;
             return true;
         }
     };

test/testexprengine.cpp

@@ -359,14 +359,14 @@ private:
         ASSERT_EQUALS("1:26: $4=ArrayValue([$3],[:]=$2)\n"
                       "1:26: $3=IntRange(0:2147483647)\n"
                       "1:26: $2=IntRange(-128:127)\n"
-                      "1:27: 0:memory:{s=($4,[$3],[:]=$2)}\n",
+                      "1:27: D0:memory:{s=($4,[$3],[:]=$2)}\n",
                       trackExecution("void foo() { std::string s; }", &settings));
 
 
         ASSERT_EQUALS("1:52: $4=ArrayValue([$3],[:]=$2)\n"
                       "1:52: $3=IntRange(0:2147483647)\n"
                       "1:52: $2=IntRange(-128:127)\n"
-                      "1:66: 0:memory:{s=($4,[$3],[:]=$2)}\n",
+                      "1:66: D0:memory:{s=($4,[$3],[:]=$2)}\n",
                       trackExecution("std::string getName(int); void foo() { std::string s = getName(1); }", &settings));
     }
 
@@ -780,7 +780,7 @@ private:
         ASSERT_EQUALS("2:16: $2:0=IntRange(-2147483648:2147483647)\n"
                       "2:20: $1=ArrayValue([10],[:]=$2)\n"
                       "2:20: $2=IntRange(-2147483648:2147483647)\n"
-                      "2:26: 0:memory:{buf=($1,[10],[:]=$2) x=$2:0}\n",
+                      "2:26: D0:memory:{buf=($1,[10],[:]=$2) x=$2:0}\n",
                       trackExecution(code));
     }
 
@@ -791,10 +791,10 @@ private:
                             "  return buf[0][1][2];\n"
                             "}";
         ASSERT_EQUALS("1:14: $1=IntRange(-2147483648:2147483647)\n"
-                      "1:14: 0:memory:{x=$1}\n"
+                      "1:14: D0:memory:{x=$1}\n"
                       "2:7: $2=ArrayValue([3][4][5],[:]=?)\n"
-                      "2:19: 0:memory:{x=$1 buf=($2,[3][4][5],[:]=?)}\n"
+                      "2:19: D0:memory:{x=$1 buf=($2,[3][4][5],[:]=?)}\n"
-                      "3:20: 0:memory:{x=$1 buf=($2,[3][4][5],[:]=?,[((20)*($1))+(7)]=10)}\n",
+                      "3:20: D0:memory:{x=$1 buf=($2,[3][4][5],[:]=?,[((20)*($1))+(7)]=10)}\n",
                       trackExecution(code));
     }
 
@@ -815,9 +815,9 @@ private:
                             "}";
         ASSERT_EQUALS("1:28: $2=ArrayValue([$1],[:]=?,null)\n"
                       "1:28: $1=IntRange(1:ffffffffffffffff)\n"
-                      "1:28: 0:memory:{x=($2,[$1],[:]=?)}\n"
+                      "1:28: D0:memory:{x=($2,[$1],[:]=?)}\n"
-                      "2:9: 0:memory:{x=($2,[$1],[:]=?,[0]=2)}\n"
+                      "2:9: D0:memory:{x=($2,[$1],[:]=?,[0]=2)}\n"
-                      "3:9: 0:memory:{x=($2,[$1],[:]=?,[0]=1)}\n",
+                      "3:9: D0:memory:{x=($2,[$1],[:]=?,[0]=1)}\n",
                       trackExecution(code));
     }
 
@@ -903,7 +903,7 @@ private:
         ASSERT_EQUALS("1:36: $3=ArrayValue([$2],[:]=bailout,null)\n"
                       "1:36: $2=IntRange(1:2147483647)\n"
                       "1:36: bailout=BailoutValue(bailout)\n"
-                      "1:46: 0:memory:{p=($3,[$2],[:]=bailout)}\n",
+                      "1:46: D0:memory:{p=($3,[$2],[:]=bailout)}\n",
                       trackExecution("char *foo(int); void bar() { char *p = foo(1); }"));
     }