Skip to content

Revert exprengine changes to fix CI on appveyor#3668

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
pfultz2 wants to merge 2 commits into from
Closed

Revert exprengine changes to fix CI on appveyor #3668

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
9d52861
Revert "exprengine; add CONTRACT #define so contract-handling can be …
pfultz2 Jan 3, 2022
5811b0e
Revert "exprengine: better checking for uninit variables"
pfultz2 Jan 3, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 5 additions & 5 deletions lib/bughuntingchecks.cpp
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -199,7 +199,7 @@ static void divByZero(const Token *tok, const ExprEngine::Value &value, ExprEngi
return;
if (tok->isImpossibleIntValue(0))
return;
if (value.isUninit(dataBase) && value.type != ExprEngine::ValueType::BailoutValue)
if (value.isUninit() && value.type != ExprEngine::ValueType::BailoutValue)
return;
float f = getKnownFloatValue(tok, 0.0f);
if (f > 0.0f || f < 0.0f)
Expand DownExpand Up@@ -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(dataBase);
uninitStructMember = structValue->getUninitStructMember();

// uninitialized struct member => is there data copy of struct..
if (!uninitStructMember.empty()) {
Expand All@@ -325,10 +325,10 @@ static void uninit(const Token *tok, const ExprEngine::Value &value, ExprEngine:
}

bool uninitData = false;
if (!value.isUninit(dataBase) && uninitStructMember.empty()) {
if (!value.isUninit() && 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(dataBase);
uninitData = arrayValue->data.size() >= 1 && arrayValue->data[0].value->isUninit();
}
}

Expand DownExpand Up@@ -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(dataBase)) {
if (v.second->isUninit()) {
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;
}
Expand Down
74 changes: 11 additions & 63 deletions lib/exprengine.cpp
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -150,9 +150,6 @@
#define Z3_VERSION_INT GET_VERSION_INT(Z3_MAJOR_VERSION, Z3_MINOR_VERSION, Z3_BUILD_NUMBER)
#endif

constexpr auto MAX_BUFFER_SIZE = ~0UL;
#define CONTRACT 1

namespace {
struct ExprEngineException {
ExprEngineException(const Token *tok, const std::string &what) : tok(tok), what(what) {}
Expand DownExpand Up@@ -204,7 +201,9 @@ static std::string str(ExprEngine::ValuePtr val)
break;
}

return val->name + "=" + std::string(typestr) + "(" + val->getRange() + ")";
std::ostringstream ret;
ret << val->name << "=" << typestr << "(" << val->getRange() << ")";
return ret.str();
}

static size_t extfind(const std::string &str, const std::string &what, size_t pos)
Expand DownExpand Up@@ -342,7 +341,7 @@ namespace {
}

void ifSplit(const Token *tok, unsigned int thenIndex, unsigned int elseIndex) {
mMap[tok].push_back("D" + std::to_string(thenIndex) + ": Split. Then:D" + std::to_string(thenIndex) + " Else:D" + std::to_string(elseIndex));
mMap[tok].push_back(std::to_string(thenIndex) + ": Split. Then:" + std::to_string(thenIndex) + " Else:" + std::to_string(elseIndex));
}

private:
Expand DownExpand Up@@ -413,7 +412,6 @@ namespace {
return tokenizer->isCPP();
}

#ifdef CONTRACT
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())
Expand DownExpand Up@@ -441,7 +439,6 @@ namespace {
if (value)
constraints.push_back(value);
}
#endif

void assignValue(const Token *tok, unsigned int varId, ExprEngine::ValuePtr value) {
if (varId == 0)
Expand DownExpand Up@@ -539,7 +536,7 @@ namespace {
return;
const SymbolDatabase * const symbolDatabase = tokenizer->getSymbolDatabase();
std::ostringstream s;
s << "D" << mDataIndex << ":" << "memory:{";
s << mDataIndex << ":" << "memory:{";
bool first = true;
for (auto mem : memory) {
ExprEngine::ValuePtr value = mem.second;
Expand DownExpand Up@@ -620,15 +617,13 @@ namespace {
}

void addConstraints(ExprEngine::ValuePtr value, const Token *tok) {
#ifdef CONTRACT
MathLib::bigint low;
if (tok->getCppcheckAttribute(TokenImpl::CppcheckAttributes::Type::LOW, &low))
addConstraint(std::make_shared<ExprEngine::BinOpResult>(">=", value, std::make_shared<ExprEngine::IntRange>(std::to_string(low), low, low)), true);

MathLib::bigint high;
if (tok->getCppcheckAttribute(TokenImpl::CppcheckAttributes::Type::HIGH, &high))
addConstraint(std::make_shared<ExprEngine::BinOpResult>("<=", value, std::make_shared<ExprEngine::IntRange>(std::to_string(high), high, high)), true);
#endif
}

void reportError(const Token *tok,
Expand DownExpand Up@@ -1310,32 +1305,6 @@ class ExprData {
};
#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)
Expand DownExpand Up@@ -1973,7 +1942,6 @@ static ExprEngine::ValuePtr executeIncDec(const Token *tok, Data &data)
#ifdef USE_Z3
static void checkContract(Data &data, const Token *tok, const Function *function, const std::vector<ExprEngine::ValuePtr> &argValues)
{
#ifdef CONTRACT
ExprData exprData;
z3::solver solver(exprData.context);
try {
Expand DownExpand Up@@ -2043,7 +2011,6 @@ static void checkContract(Data &data, const Token *tok, const Function *function
true,
functionName);
}
#endif
}
#endif

Expand DownExpand Up@@ -2103,7 +2070,6 @@ static ExprEngine::ValuePtr executeFunctionCall(const Token *tok, Data &data)
if (tok->astOperand1()->function()) {
const Function *function = tok->astOperand1()->function();
const std::string &functionName = function->fullName();
#ifdef CONTRACT
const auto contractIt = data.settings->functionContracts.find(functionName);
if (contractIt != data.settings->functionContracts.end()) {
#ifdef USE_Z3
Expand All@@ -2116,7 +2082,6 @@ static ExprEngine::ValuePtr executeFunctionCall(const Token *tok, Data &data)
if (!bailout)
data.addMissingContract(functionName);
}
#endif

// Execute subfunction..
if (hasBody) {
Expand DownExpand Up@@ -2215,7 +2180,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, MAX_BUFFER_SIZE);
auto bufferSize = std::make_shared<ExprEngine::IntRange>(data.getNewSymbolName(), 1, ~0UL);
return std::make_shared<ExprEngine::ArrayValue>(data.getNewSymbolName(), bufferSize, range, true, nullPointer, uninitPointer);
}

Expand DownExpand Up@@ -2276,11 +2241,6 @@ 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);
Expand DownExpand Up@@ -2403,8 +2363,7 @@ static ExprEngine::ValuePtr executeVariable(const Token *tok, Data &data)

static ExprEngine::ValuePtr executeKnownMacro(const Token *tok, Data &data)
{
const auto intval = tok->getKnownIntValue();
auto val = std::make_shared<ExprEngine::IntRange>(std::to_string(intval), intval, intval);
auto val = std::make_shared<ExprEngine::IntRange>(data.getNewSymbolName(), tok->getKnownIntValue(), tok->getKnownIntValue());
call(data.callbacks, tok, val, &data);
return val;
}
Expand DownExpand Up@@ -2549,9 +2508,6 @@ 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 "";
}
Expand All@@ -2574,15 +2530,9 @@ static std::string execute(const Token *start, const Token *end, Data &data)
return data.str();
}

if (Token::simpleMatch(tok, "try {") && Token::simpleMatch(tok->linkAt(1), "} catch (")) {
const Token *catchTok = tok->linkAt(1);
while (Token::simpleMatch(catchTok, "} catch (")) {
Data catchData(data);
catchTok = catchTok->linkAt(2)->next();
execute(catchTok, end, catchData);
catchTok = catchTok->link();
}
}
if (Token::simpleMatch(tok, "try"))
// TODO this is a bailout
throw ExprEngineException(tok, "Unhandled:" + tok->str());

// Variable declaration..
if (tok->variable() && tok->variable()->nameToken() == tok) {
Expand DownExpand Up@@ -2821,7 +2771,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(&bodyData))
if (oldValue && oldValue->isUninit())
call(bodyData.callbacks, lhs, oldValue, &bodyData);
if (oldValue && oldValue->type == ExprEngine::ValueType::ArrayValue) {
// Try to assign "any" value
Expand DownExpand Up@@ -3005,9 +2955,7 @@ void ExprEngine::executeFunction(const Scope *functionScope, ErrorLogger *errorL
for (const Variable &arg : function->argumentList)
data.assignValue(functionScope->bodyStart, arg.declarationId(), createVariableValue(arg, data));

#ifdef CONTRACT
data.contractConstraints(function, executeExpression1);
#endif

const std::time_t stopTime = data.startTime + data.settings->bugHuntingCheckFunctionMaxTime;

Expand Down
14 changes: 7 additions & 7 deletions lib/exprengine.h
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -116,8 +116,7 @@ namespace ExprEngine {
(void)value;
return false;
}
virtual bool isUninit(const DataBase *dataBase) const {
(void)dataBase;
virtual bool isUninit() const {
return false;
}

Expand All@@ -133,7 +132,9 @@ namespace ExprEngine {
(void)value;
return true;
}
bool isUninit(const DataBase *dataBase) const OVERRIDE;
bool isUninit() const OVERRIDE {
return true;
}
};

class IntRange : public Value {
Expand DownExpand Up@@ -244,9 +245,9 @@ namespace ExprEngine {
return (it == member.end()) ? ValuePtr() : it->second;
}

std::string getUninitStructMember(const DataBase *dataBase) const {
std::string getUninitStructMember() const {
for (auto memberNameValue: member) {
if (memberNameValue.second && memberNameValue.second->isUninit(dataBase))
if (memberNameValue.second && memberNameValue.second->isUninit())
return memberNameValue.first;
}
return std::string();
Expand DownExpand Up@@ -326,8 +327,7 @@ namespace ExprEngine {
bool isEqual(const DataBase * /*dataBase*/, int /*value*/) const OVERRIDE {
return true;
}
bool isUninit(const DataBase *dataBase) const OVERRIDE {
(void)dataBase;
bool isUninit() const OVERRIDE {
return true;
}
};
Expand Down
20 changes: 10 additions & 10 deletions test/testexprengine.cpp
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -359,14 +359,14 @@ class TestExprEngine : public TestFixture {
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: D0:memory:{s=($4,[$3],[:]=$2)}\n",
"1:27: 0: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: D0:memory:{s=($4,[$3],[:]=$2)}\n",
"1:66: 0:memory:{s=($4,[$3],[:]=$2)}\n",
trackExecution("std::string getName(int); void foo() { std::string s = getName(1); }", &settings));
}

Expand DownExpand Up@@ -780,7 +780,7 @@ class TestExprEngine : public TestFixture {
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: D0:memory:{buf=($1,[10],[:]=$2) x=$2:0}\n",
"2:26: 0:memory:{buf=($1,[10],[:]=$2) x=$2:0}\n",
trackExecution(code));
}

Expand All@@ -791,10 +791,10 @@ class TestExprEngine : public TestFixture {
" return buf[0][1][2];\n"
"}";
ASSERT_EQUALS("1:14: $1=IntRange(-2147483648:2147483647)\n"
"1:14: D0:memory:{x=$1}\n"
"1:14: 0:memory:{x=$1}\n"
"2:7: $2=ArrayValue([3][4][5],[:]=?)\n"
"2:19: D0:memory:{x=$1 buf=($2,[3][4][5],[:]=?)}\n"
"3:20: D0:memory:{x=$1 buf=($2,[3][4][5],[:]=?,[((20)*($1))+(7)]=10)}\n",
"2:19: 0: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",
trackExecution(code));
}

Expand All@@ -815,9 +815,9 @@ class TestExprEngine : public TestFixture {
"}";
ASSERT_EQUALS("1:28: $2=ArrayValue([$1],[:]=?,null)\n"
"1:28: $1=IntRange(1:ffffffffffffffff)\n"
"1:28: D0:memory:{x=($2,[$1],[:]=?)}\n"
"2:9: D0:memory:{x=($2,[$1],[:]=?,[0]=2)}\n"
"3:9: D0:memory:{x=($2,[$1],[:]=?,[0]=1)}\n",
"1:28: 0:memory:{x=($2,[$1],[:]=?)}\n"
"2:9: 0:memory:{x=($2,[$1],[:]=?,[0]=2)}\n"
"3:9: 0:memory:{x=($2,[$1],[:]=?,[0]=1)}\n",
trackExecution(code));
}

Expand DownExpand Up@@ -903,7 +903,7 @@ class TestExprEngine : public TestFixture {
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: D0:memory:{p=($3,[$2],[:]=bailout)}\n",
"1:46: 0:memory:{p=($3,[$2],[:]=bailout)}\n",
trackExecution("char *foo(int); void bar() { char *p = foo(1); }"));
}

Expand Down