ExprEngine: Add --debug-verify, fixed handling of global arrays

cli/cmdlineparser.cpp

@@ -192,6 +192,8 @@ bool CmdLineParser::parseFromArgs(int argc, const char* const argv[])
             // Experimental: Verify
             else if (std::strcmp(argv[i], "--verify") == 0)
                 mSettings->verification = true;
+            else if (std::strcmp(argv[i], "--debug-verify") == 0)
+                mSettings->debugVerification = true;
 
             // Enforce language (--language=, -x)
             else if (std::strncmp(argv[i], "--language=", 11) == 0 || std::strcmp(argv[i], "-x") == 0) {

lib/exprengine.cpp

@@ -78,7 +78,7 @@ namespace {
             map[tok].push_back(s);
         }
 
-        void print() {
+        void print(std::ostream &out) {
             std::set<std::pair<int,int>> locations;
             for (auto it : map) {
                 locations.insert(std::pair<int,int>(it.first->linenr(), it.first->column()));
@@ -94,7 +94,7 @@ namespace {
                         continue;
                     const std::vector<std::string> &dumps = it.second;
                     for (const std::string &dump : dumps)
-                        std::cout << lineNumber << ":" << column << ": " << dump << "\n";
+                        out << lineNumber << ":" << column << ": " << dump << "\n";
                 }
             }
         }
@@ -103,12 +103,12 @@ namespace {
         std::set<std::string> mSymbols;
     };
 
-    class Data {
+    class Data : public ExprEngine::DataBase {
     public:
         Data(int *symbolValueIndex, const Tokenizer *tokenizer, const Settings *settings, const std::vector<ExprEngine::Callback> &callbacks, TrackExecution *trackExecution)
-            : symbolValueIndex(symbolValueIndex)
+            : DataBase(settings)
+            , symbolValueIndex(symbolValueIndex)
             , tokenizer(tokenizer)
-            , settings(settings)
             , callbacks(callbacks)
             , mTrackExecution(trackExecution)
             , mDataIndex(trackExecution->getNewDataIndex()) {}
@@ -116,7 +116,6 @@ namespace {
         Memory memory;
         int * const symbolValueIndex;
         const Tokenizer * const tokenizer;
-        const Settings * const settings;
         const std::vector<ExprEngine::Callback> &callbacks;
 
         void assignValue(const Token *tok, unsigned int varId, ExprEngine::ValuePtr value) {
@@ -196,7 +195,7 @@ namespace {
             return ret;
         }
 
-        std::string getNewSymbolName() {
+        std::string getNewSymbolName() override {
             return "$" + std::to_string(++(*symbolValueIndex));
         }
 
@@ -206,8 +205,8 @@ namespace {
                 return std::dynamic_pointer_cast<ExprEngine::ArrayValue>(it->second);
             if (tok->varId() == 0)
                 return std::shared_ptr<ExprEngine::ArrayValue>();
-            auto val = std::make_shared<ExprEngine::ArrayValue>(getNewSymbolName(), tok->variable());
+            auto val = std::make_shared<ExprEngine::ArrayValue>(this, tok->variable());
-            memory[tok->varId()] = val;
+            assignValue(tok, tok->varId(), val);
             return val;
         }
 
@@ -316,8 +315,8 @@ ExprEngine::ArrayValue::ArrayValue(const std::string &name, ExprEngine::ValuePtr
     assign(ExprEngine::ValuePtr(), value);
 }
 
-ExprEngine::ArrayValue::ArrayValue(const std::string &name, const Variable *var)
+ExprEngine::ArrayValue::ArrayValue(DataBase *data, const Variable *var)
-    : Value(name, ExprEngine::ValueType::ArrayValue)
+    : Value(data->getNewSymbolName(), ExprEngine::ValueType::ArrayValue)
 {
     if (var) {
         int sz = 1;
@@ -331,7 +330,17 @@ ExprEngine::ArrayValue::ArrayValue(const std::string &name, const Variable *var)
         if (sz >= 1)
             size = std::make_shared<ExprEngine::IntRange>(std::to_string(sz), sz, sz);
     }
-    assign(ExprEngine::ValuePtr(), std::make_shared<ExprEngine::UninitValue>());
+    ValuePtr val;
+    if (!var->isGlobal() && !var->isStatic())
+        val = std::make_shared<ExprEngine::UninitValue>();
+    else {
+        if (var->valueType()) {
+            ::ValueType vt(*var->valueType());
+            vt.pointer = 0;
+            val = getValueRangeFromValueType(data->getNewSymbolName(), &vt, *data->settings);
+        }
+    }
+    assign(ExprEngine::ValuePtr(), val);
 }
 
 void ExprEngine::ArrayValue::assign(ExprEngine::ValuePtr index, ExprEngine::ValuePtr value)
@@ -1072,7 +1081,7 @@ static void execute(const Token *start, const Token *end, Data &data)
                 }
             }
             if (tok->variable()->isArray()) {
-                data.assignValue(tok, tok->varId(), std::make_shared<ExprEngine::ArrayValue>(data.getNewSymbolName(), tok->variable()));
+                data.assignValue(tok, tok->varId(), std::make_shared<ExprEngine::ArrayValue>(&data, tok->variable()));
                 if (Token::Match(tok, "%name% ["))
                     tok = tok->linkAt(1);
             } else if (Token::Match(tok, "%var% ;"))
@@ -1105,12 +1114,12 @@ static void execute(const Token *start, const Token *end, Data &data)
     }
 }
 
-void ExprEngine::executeAllFunctions(const Tokenizer *tokenizer, const Settings *settings, const std::vector<ExprEngine::Callback> &callbacks)
+void ExprEngine::executeAllFunctions(const Tokenizer *tokenizer, const Settings *settings, const std::vector<ExprEngine::Callback> &callbacks, std::ostream &trace)
 {
     const SymbolDatabase *symbolDatabase = tokenizer->getSymbolDatabase();
     for (const Scope *functionScope : symbolDatabase->functionScopes) {
         try {
-            executeFunction(functionScope, tokenizer, settings, callbacks);
+            executeFunction(functionScope, tokenizer, settings, callbacks, trace);
         } catch (const std::exception &e) {
             // FIXME.. there should not be exceptions
             std::string functionName = functionScope->function->name();
@@ -1166,7 +1175,7 @@ static ExprEngine::ValuePtr createVariableValue(const Variable &var, Data &data)
         return std::make_shared<ExprEngine::PointerValue>(data.getNewSymbolName(), range, true, true);
     }
     if (var.isArray())
-        return std::make_shared<ExprEngine::ArrayValue>(data.getNewSymbolName(), &var);
+        return std::make_shared<ExprEngine::ArrayValue>(&data, &var);
     if (valueType->isIntegral())
         return getValueRangeFromValueType(data.getNewSymbolName(), valueType, *data.settings);
     if (valueType->type == ValueType::Type::RECORD)
@@ -1183,7 +1192,7 @@ static ExprEngine::ValuePtr createVariableValue(const Variable &var, Data &data)
     return ExprEngine::ValuePtr();
 }
 
-void ExprEngine::executeFunction(const Scope *functionScope, const Tokenizer *tokenizer, const Settings *settings, const std::vector<ExprEngine::Callback> &callbacks)
+void ExprEngine::executeFunction(const Scope *functionScope, const Tokenizer *tokenizer, const Settings *settings, const std::vector<ExprEngine::Callback> &callbacks, std::ostream &trace)
 {
     if (!functionScope->bodyStart)
         return;
@@ -1203,9 +1212,9 @@ void ExprEngine::executeFunction(const Scope *functionScope, const Tokenizer *to
 
     execute(functionScope->bodyStart, functionScope->bodyEnd, data);
 
-    if (settings->verification) {
+    if (settings->debugVerification) {
         // TODO generate better output!!
-        trackExecution.print();
+        trackExecution.print(trace);
     }
 }
 
@@ -1291,5 +1300,5 @@ void ExprEngine::runChecks(ErrorLogger *errorLogger, const Tokenizer *tokenizer,
 #ifdef VERIFY_INTEGEROVERFLOW
     callbacks.push_back(integerOverflow);
 #endif
-    ExprEngine::executeAllFunctions(tokenizer, settings, callbacks);
+    ExprEngine::executeAllFunctions(tokenizer, settings, callbacks, std::cout);
 }

lib/exprengine.h

@@ -70,6 +70,13 @@ namespace ExprEngine {
     class Value;
     typedef std::shared_ptr<Value> ValuePtr;
 
+    class DataBase {
+    public:
+        explicit DataBase(const Settings *settings) : settings(settings) {}
+        virtual std::string getNewSymbolName() = 0;
+        const Settings * const settings;
+    };
+
     class Value {
     public:
         Value(const std::string &name, const ValueType type) : name(name), type(type) {}
@@ -159,7 +166,7 @@ namespace ExprEngine {
         const int MAXSIZE = 0x100000;
 
         ArrayValue(const std::string &name, ValuePtr size, ValuePtr value);
-        ArrayValue(const std::string &name, const Variable *var);
+        ArrayValue(DataBase *data, const Variable *var);
 
         std::string getSymbolicExpression() const override;
 
@@ -294,8 +301,8 @@ namespace ExprEngine {
     typedef std::function<void(const Token *, const ExprEngine::Value &)> Callback;
 
     /** Execute all functions */
-    void CPPCHECKLIB executeAllFunctions(const Tokenizer *tokenizer, const Settings *settings, const std::vector<Callback> &callbacks);
+    void CPPCHECKLIB executeAllFunctions(const Tokenizer *tokenizer, const Settings *settings, const std::vector<Callback> &callbacks, std::ostream &trace);
-    void executeFunction(const Scope *functionScope, const Tokenizer *tokenizer, const Settings *settings, const std::vector<Callback> &callbacks);
+    void executeFunction(const Scope *functionScope, const Tokenizer *tokenizer, const Settings *settings, const std::vector<Callback> &callbacks, std::ostream &trace);
 
     void runChecks(ErrorLogger *errorLogger, const Tokenizer *tokenizer, const Settings *settings);
 }

lib/settings.cpp

@@ -46,6 +46,7 @@ Settings::Settings()
       force(false),
       inconclusive(false),
       verification(false),
+      debugVerification(false),
       inlineSuppressions(false),
       jobs(1),
       jointSuppressionReport(false),

lib/settings.h

@@ -190,6 +190,8 @@ public:
     /** @brief Enable verification analysis */
     bool verification;
 
+    bool debugVerification;
+
     /** @brief check unknown function return values */
     std::set<std::string> checkUnknownFunctionReturn;
 

test/testexprengine.cpp

@@ -44,6 +44,21 @@ private:
         TEST_CASE(exprAssign1);
         TEST_CASE(exprAssign2); // Truncation
 
+        TEST_CASE(if1);
+        TEST_CASE(if2);
+        TEST_CASE(if3);
+        TEST_CASE(if4);
+        TEST_CASE(if5);
+        TEST_CASE(ifelse1);
+
+        TEST_CASE(array1);
+        TEST_CASE(array2);
+        TEST_CASE(array3);
+        TEST_CASE(array4);
+        TEST_CASE(arrayInit1);
+        TEST_CASE(arrayInit2);
+        TEST_CASE(arrayUninit);
+
         TEST_CASE(floatValue1);
         TEST_CASE(floatValue2);
 
@@ -51,21 +66,6 @@ private:
         TEST_CASE(functionCall2);
         TEST_CASE(functionCall3);
 
-        TEST_CASE(if1);
-        TEST_CASE(if2);
-        TEST_CASE(if3);
-        TEST_CASE(if4);
-        TEST_CASE(if5);
-
-        TEST_CASE(ifelse1);
-
-        TEST_CASE(localArray1);
-        TEST_CASE(localArray2);
-        TEST_CASE(localArray3);
-        TEST_CASE(localArrayInit1);
-        TEST_CASE(localArrayInit2);
-        TEST_CASE(localArrayUninit);
-
         TEST_CASE(pointer1);
         TEST_CASE(pointer2);
 
@@ -93,10 +93,25 @@ private:
         };
         std::vector<ExprEngine::Callback> callbacks;
         callbacks.push_back(f);
-        ExprEngine::executeAllFunctions(&tokenizer, &settings, callbacks);
+        std::ostringstream dummy;
+        ExprEngine::executeAllFunctions(&tokenizer, &settings, callbacks, dummy);
         return ret;
     }
 
+    std::string trackExecution(const char code[]) {
+        Settings settings;
+        settings.debugVerification = true;
+        settings.platform(cppcheck::Platform::Unix64);
+        settings.library.smartPointers.insert("std::shared_ptr");
+        Tokenizer tokenizer(&settings, this);
+        std::istringstream istr(code);
+        tokenizer.tokenize(istr, "test.cpp");
+        std::vector<ExprEngine::Callback> dummy;
+        std::ostringstream ret;
+        ExprEngine::executeAllFunctions(&tokenizer, &settings, dummy, ret);
+        return ret.str();
+    }
+
     void argPointer() {
         ASSERT_EQUALS("->$1,null,->?", getRange("void f(unsigned char *p) { a = *p; }", "p"));
     }
@@ -142,32 +157,6 @@ private:
         ASSERT_EQUALS("2", getRange("void f(unsigned char x) { x = 258; int a = x }", "a=x"));
     }
 
-    void floatValue1() {
-        ASSERT_EQUALS(std::to_string(std::numeric_limits<float>::min()) + ":" + std::to_string(std::numeric_limits<float>::max()), getRange("float f; void func() { f=f; }", "f=f"));
-    }
-
-    void floatValue2() {
-        ASSERT_EQUALS("14.500000", getRange("void func() { float f = 29.0; f = f / 2.0; }", "f/2.0"));
-    }
-
-    void functionCall1() {
-        ASSERT_EQUALS("-2147483648:2147483647", getRange("int atoi(const char *p); void f() { int x = atoi(a); x = x; }", "x=x"));
-    }
-
-    void functionCall2() {
-        const char code[] = "namespace NS {\n"
-                            "    short getValue();\n"
-                            "}"
-                            "void f() {\n"
-                            "    short value = NS::getValue();\n"
-                            "    value = value;\n"
-                            "}";
-        ASSERT_EQUALS("-32768:32767", getRange(code, "value=value"));
-    }
-
-    void functionCall3() {
-        ASSERT_EQUALS("-2147483648:2147483647", getRange("int fgets(int, const char *, void *); void f() { int x = -1; fgets(stdin, \"%d\", &x); x=x; }", "x=x"));
-    }
 
     void if1() {
         ASSERT_EQUALS("7:32768", getRange("inf f(short x) { if (x > 5) a = x + 1; }", "x+1"));
@@ -193,30 +182,66 @@ private:
         ASSERT_EQUALS("-32767:6", getRange("inf f(short x) { if (x > 5) ; else a = x + 1; }", "x+1"));
     }
 
-    void localArray1() {
+
+    void array1() {
         ASSERT_EQUALS("5", getRange("inf f() { int arr[10]; arr[4] = 5; return arr[4]; }", "arr[4]"));
     }
 
-    void localArray2() {
+    void array2() {
         ASSERT_EQUALS("0:255", getRange("void dostuff(unsigned char *); int f() { unsigned char arr[10] = \"\"; dostuff(arr); return arr[4]; }", "arr[4]"));
     }
 
-    void localArray3() {
+    void array3() {
         ASSERT_EQUALS("?,43", getRange("int f(unsigned char x) { int arr[10]; arr[4] = 43; int vx = arr[x]; }", "arr[x]"));
     }
 
-    void localArrayInit1() {
+    void array4() {
+        const char code[] = "int buf[10];\n"
+                            "void f() { int x = buf[0]; }";
+        ASSERT_EQUALS("2:20: $2=-2147483648:2147483647\n"
+                      "2:26: { buf=($1,size=10,[:]=$2) x=($3,{{(null),$2}})}\n",
+                      trackExecution(code));
+    }
+
+    void arrayInit1() {
         ASSERT_EQUALS("0", getRange("inf f() { char arr[10] = \"\"; return arr[4]; }", "arr[4]"));
     }
 
-    void localArrayInit2() {
+    void arrayInit2() {
         ASSERT_EQUALS("66", getRange("void f() { char str[] = \"hello\"; str[0] = \'B\'; }", "str[0]=\'B\'"));
     }
 
-    void localArrayUninit() {
+    void arrayUninit() {
         ASSERT_EQUALS("?", getRange("int f() { int arr[10]; return arr[4]; }", "arr[4]"));
     }
 
+    void floatValue1() {
+        ASSERT_EQUALS(std::to_string(std::numeric_limits<float>::min()) + ":" + std::to_string(std::numeric_limits<float>::max()), getRange("float f; void func() { f=f; }", "f=f"));
+    }
+
+    void floatValue2() {
+        ASSERT_EQUALS("14.500000", getRange("void func() { float f = 29.0; f = f / 2.0; }", "f/2.0"));
+    }
+
+    void functionCall1() {
+        ASSERT_EQUALS("-2147483648:2147483647", getRange("int atoi(const char *p); void f() { int x = atoi(a); x = x; }", "x=x"));
+    }
+
+    void functionCall2() {
+        const char code[] = "namespace NS {\n"
+                            "    short getValue();\n"
+                            "}"
+                            "void f() {\n"
+                            "    short value = NS::getValue();\n"
+                            "    value = value;\n"
+                            "}";
+        ASSERT_EQUALS("-32768:32767", getRange(code, "value=value"));
+    }
+
+    void functionCall3() {
+        ASSERT_EQUALS("-2147483648:2147483647", getRange("int fgets(int, const char *, void *); void f() { int x = -1; fgets(stdin, \"%d\", &x); x=x; }", "x=x"));
+    }
+
     void pointer1() {
         ASSERT_EQUALS("?", getRange("int f() { int *x; x = x; }", "x=x"));
     }