diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp index de34210af..e8be95ca2 100644 --- a/lib/exprengine.cpp +++ b/lib/exprengine.cpp @@ -70,7 +70,7 @@ namespace { class TrackExecution { public: TrackExecution() : mDataIndex(0), mAbortLine(-1) {} - std::map> map; + int getNewDataIndex() { return mDataIndex++; } @@ -78,6 +78,8 @@ namespace { void symbolRange(const Token *tok, ExprEngine::ValuePtr value) { if (!tok || !value) return; + if (tok->index() == 0) + return; const std::string &symbolicExpression = value->getSymbolicExpression(); if (symbolicExpression[0] != '$') return; @@ -150,6 +152,8 @@ namespace { return "ok"; } + std::map> map; + int mDataIndex; int mAbortLine; std::set mSymbols; @@ -158,9 +162,10 @@ namespace { class Data : public ExprEngine::DataBase { public: - Data(int *symbolValueIndex, const Tokenizer *tokenizer, const Settings *settings, const std::string ¤tFunction, const std::vector &callbacks, TrackExecution *trackExecution) + Data(int *symbolValueIndex, ErrorLogger *errorLogger, const Tokenizer *tokenizer, const Settings *settings, const std::string ¤tFunction, const std::vector &callbacks, TrackExecution *trackExecution) : DataBase(currentFunction, settings) , symbolValueIndex(symbolValueIndex) + , errorLogger(errorLogger) , tokenizer(tokenizer) , callbacks(callbacks) , mTrackExecution(trackExecution) @@ -168,14 +173,15 @@ namespace { typedef std::map Memory; Memory memory; int * const symbolValueIndex; + ErrorLogger *errorLogger; const Tokenizer * const tokenizer; const std::vector &callbacks; std::vector constraints; - void contractConstraints(const Function *function, ExprEngine::ValuePtr(*executeExpression)(const Token*, Data&)) { - const auto it = settings->functionContracts.find(currentFunction); + ExprEngine::ValuePtr executeContract(const Function *function, ExprEngine::ValuePtr(*executeExpression)(const Token*, Data&)) { + const auto it = settings->functionContracts.find(function->fullName()); if (it == settings->functionContracts.end()) - return; + return ExprEngine::ValuePtr(); const std::string &expects = it->second; TokenList tokenList(settings); std::istringstream istr(expects); @@ -191,7 +197,13 @@ namespace { } } symbolDatabase->setValueTypeInTokenList(false, tokenList.front()); - constraints.push_back(executeExpression(tokenList.front()->astTop(), *this)); + return executeExpression(tokenList.front()->astTop(), *this); + } + + void contractConstraints(const Function *function, ExprEngine::ValuePtr(*executeExpression)(const Token*, Data&)) { + auto value = executeContract(function, executeExpression); + if (value) + constraints.push_back(value); } void addError(int linenr) OVERRIDE { @@ -263,6 +275,20 @@ namespace { return value; } + void trackCheckContract(const Token *tok, const std::string &solverOutput) { + std::ostringstream os; + os << "checkContract:{\n"; + + std::string line; + std::istringstream istr(solverOutput); + while (std::getline(istr, line)) + os << " " << line << "\n"; + + os << "}"; + + mTrackExecution->state(tok, os.str()); + } + void trackProgramState(const Token *tok) { if (memory.empty()) return; @@ -1090,6 +1116,7 @@ static void call(const std::vector &callbacks, const Token } static ExprEngine::ValuePtr executeExpression(const Token *tok, Data &data); +static ExprEngine::ValuePtr executeExpression1(const Token *tok, Data &data); static ExprEngine::ValuePtr executeReturn(const Token *tok, Data &data) { @@ -1208,6 +1235,73 @@ static ExprEngine::ValuePtr executeAssign(const Token *tok, Data &data) return assignValue; } +static void checkContract(Data &data, const Token *tok, const Function *function, const std::vector &argValues) +{ + (void)data; + (void)tok; + (void)function; + (void)argValues; + +#ifdef USE_Z3 + ExprData exprData; + z3::solver solver(exprData.context); + try { + // Invert contract, we want to know if the contract might not be met + solver.add(z3::ite(exprData.getConstraintExpr(data.executeContract(function, executeExpression1)), exprData.context.bool_val(false), exprData.context.bool_val(true))); + + bool bailoutValue = false; + for (nonneg int i = 0; i < argValues.size(); ++i) { + const Variable *argvar = function->getArgumentVar(i); + if (!argvar || !argvar->nameToken()) + continue; + + ExprEngine::ValuePtr argValue = argValues[i]; + if (!argValue || argValue->type == ExprEngine::ValueType::BailoutValue) { + bailoutValue = true; + break; + } + + if (argValue && argValue->type == ExprEngine::ValueType::IntRange) { + solver.add(exprData.getExpr(data.getValue(argvar->declarationId(), nullptr, nullptr)) == exprData.getExpr(argValue)); + } + } + + if (!bailoutValue) { + for (auto constraint : data.constraints) + solver.add(exprData.getConstraintExpr(constraint)); + + exprData.addAssertions(solver); + + // Log solver expressions for debugging/testing purposes + std::ostringstream os; + os << solver; + data.trackCheckContract(tok, os.str()); + } + + if (bailoutValue || solver.check() == z3::sat) { + data.addError(tok->linenr()); + std::list callstack{tok}; + const char * const id = "bughuntingFunctionCall"; + const auto contractIt = data.settings->functionContracts.find(function->fullName()); + const std::string functionName = contractIt->first; + const std::string functionExpects = contractIt->second; + ErrorLogger::ErrorMessage errmsg(callstack, + &data.tokenizer->list, + Severity::SeverityType::error, + id, + "Function '" + functionName + "' is called, can not determine that its contract '" + functionExpects + "' is always met.", + CWE(0), + bailoutValue); + if (!bailoutValue) + errmsg.function = data.currentFunction; + data.errorLogger->reportErr(errmsg); + } + } catch (const z3::exception &exception) { + std::cerr << "z3: " << exception << std::endl; + } +#endif +} + static ExprEngine::ValuePtr executeFunctionCall(const Token *tok, Data &data) { if (Token::simpleMatch(tok->previous(), "sizeof (")) { @@ -1244,6 +1338,12 @@ static ExprEngine::ValuePtr executeFunctionCall(const Token *tok, Data &data) if (!tok->valueType() && tok->astParent()) throw VerifyException(tok, "Expression '" + tok->expressionString() + "' has unknown type!"); + if (tok->astOperand1()->function()) { + const auto contractIt = data.settings->functionContracts.find(tok->astOperand1()->function()->fullName()); + if (contractIt != data.settings->functionContracts.end()) + checkContract(data, tok, tok->astOperand1()->function(), argValues); + } + auto val = getValueRangeFromValueType(data.getNewSymbolName(), tok->valueType(), *data.settings); call(data.callbacks, tok, val, &data); data.functionCall(); @@ -1659,12 +1759,12 @@ static void execute(const Token *start, const Token *end, Data &data) } } -void ExprEngine::executeAllFunctions(const Tokenizer *tokenizer, const Settings *settings, const std::vector &callbacks, std::ostream &report) +void ExprEngine::executeAllFunctions(ErrorLogger *errorLogger, const Tokenizer *tokenizer, const Settings *settings, const std::vector &callbacks, std::ostream &report) { const SymbolDatabase *symbolDatabase = tokenizer->getSymbolDatabase(); for (const Scope *functionScope : symbolDatabase->functionScopes) { try { - executeFunction(functionScope, tokenizer, settings, callbacks, report); + executeFunction(functionScope, errorLogger, tokenizer, settings, callbacks, report); } catch (const VerifyException &e) { // FIXME.. there should not be exceptions std::string functionName = functionScope->function->name(); @@ -1767,7 +1867,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 &callbacks, std::ostream &report) +void ExprEngine::executeFunction(const Scope *functionScope, ErrorLogger *errorLogger, const Tokenizer *tokenizer, const Settings *settings, const std::vector &callbacks, std::ostream &report) { if (!functionScope->bodyStart) return; @@ -1782,7 +1882,7 @@ void ExprEngine::executeFunction(const Scope *functionScope, const Tokenizer *to int symbolValueIndex = 0; TrackExecution trackExecution; - Data data(&symbolValueIndex, tokenizer, settings, currentFunction, callbacks, &trackExecution); + Data data(&symbolValueIndex, errorLogger, tokenizer, settings, currentFunction, callbacks, &trackExecution); for (const Variable &arg : function->argumentList) data.assignValue(functionScope->bodyStart, arg.declarationId(), createVariableValue(arg, data)); @@ -2136,7 +2236,7 @@ void ExprEngine::runChecks(ErrorLogger *errorLogger, const Tokenizer *tokenizer, #endif std::ostringstream report; - ExprEngine::executeAllFunctions(tokenizer, settings, callbacks, report); + ExprEngine::executeAllFunctions(errorLogger, tokenizer, settings, callbacks, report); if (settings->bugHuntingReport.empty()) std::cout << report.str(); else if (errorLogger) diff --git a/lib/exprengine.h b/lib/exprengine.h index 062fa3e12..3ca5fdba0 100644 --- a/lib/exprengine.h +++ b/lib/exprengine.h @@ -306,8 +306,8 @@ namespace ExprEngine { typedef std::function Callback; /** Execute all functions */ - void CPPCHECKLIB executeAllFunctions(const Tokenizer *tokenizer, const Settings *settings, const std::vector &callbacks, std::ostream &report); - void executeFunction(const Scope *functionScope, const Tokenizer *tokenizer, const Settings *settings, const std::vector &callbacks, std::ostream &report); + void CPPCHECKLIB executeAllFunctions(ErrorLogger *errorLogger, const Tokenizer *tokenizer, const Settings *settings, const std::vector &callbacks, std::ostream &report); + void executeFunction(const Scope *functionScope, ErrorLogger *errorLogger, const Tokenizer *tokenizer, const Settings *settings, const std::vector &callbacks, std::ostream &report); void runChecks(ErrorLogger *errorLogger, const Tokenizer *tokenizer, const Settings *settings); } diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp index d5b1703ad..f943fe77a 100644 --- a/test/testexprengine.cpp +++ b/test/testexprengine.cpp @@ -78,6 +78,8 @@ private: TEST_CASE(functionCall3); TEST_CASE(functionCall4); + TEST_CASE(functionCallContract1); + TEST_CASE(int1); TEST_CASE(pointer1); @@ -113,10 +115,30 @@ private: std::vector callbacks; callbacks.push_back(f); std::ostringstream trace; - ExprEngine::executeAllFunctions(&tokenizer, &settings, callbacks, trace); + ExprEngine::executeAllFunctions(this, &tokenizer, &settings, callbacks, trace); return ret; } + std::string functionCallContractExpr(const char code[], const Settings &s) { + Settings settings; + settings.bugHunting = true; + settings.debugBugHunting = true; + settings.functionContracts = s.functionContracts; + settings.platform(cppcheck::Platform::Unix64); + Tokenizer tokenizer(&settings, this); + std::istringstream istr(code); + tokenizer.tokenize(istr, "test.cpp"); + std::vector callbacks; + std::ostringstream trace; + ExprEngine::executeAllFunctions(this, &tokenizer, &settings, callbacks, trace); + std::string ret = trace.str(); + std::string::size_type pos1 = ret.find("checkContract:{"); + std::string::size_type pos2 = ret.find("}", pos1); + if (pos2 == std::string::npos) + return "Error:" + ret; + return ret.substr(pos1, pos2+1-pos1); + } + std::string getRange(const char code[], const std::string &str, int linenr = 0) { Settings settings; settings.platform(cppcheck::Platform::Unix64); @@ -136,7 +158,7 @@ private: std::vector callbacks; callbacks.push_back(f); std::ostringstream trace; - ExprEngine::executeAllFunctions(&tokenizer, &settings, callbacks, trace); + ExprEngine::executeAllFunctions(this, &tokenizer, &settings, callbacks, trace); return ret; } @@ -151,7 +173,7 @@ private: tokenizer.tokenize(istr, "test.cpp"); std::vector callbacks; std::ostringstream ret; - ExprEngine::executeAllFunctions(&tokenizer, &settings, callbacks, ret); + ExprEngine::executeAllFunctions(this, &tokenizer, &settings, callbacks, ret); return ret.str(); } @@ -460,6 +482,25 @@ private: } + void functionCallContract1() { + const char code[] = "void foo(int x);\n" + "void bar(unsigned short x) { foo(x); }"; + + Settings s; + s.functionContracts["foo(x)"] = "x < 1000"; + + ASSERT_EQUALS("checkContract:{\n" + " (declare-fun $2 () Int)\n" + " (declare-fun $1 () Int)\n" + " (assert (ite (< $2 1000) false true))\n" + " (assert (= $2 $1))\n" + " (assert (and (>= $2 (- 2147483648)) (<= $2 2147483647)))\n" + " (assert (and (>= $1 0) (<= $1 65535)))\n" + "}", + functionCallContractExpr(code, s)); + } + + void int1() { ASSERT_EQUALS("(declare-fun $1 () Int)\n" "(assert (and (>= $1 (- 2147483648)) (<= $1 2147483647)))\n"