exprengine; add CONTRACT #define so contract-handling can be enabled/disabled
This commit is contained in:
parent
33305ef4ec
commit
33446d0c75
|
@ -151,6 +151,7 @@
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
constexpr auto MAX_BUFFER_SIZE = ~0UL;
|
constexpr auto MAX_BUFFER_SIZE = ~0UL;
|
||||||
|
#define CONTRACT 1
|
||||||
|
|
||||||
namespace {
|
namespace {
|
||||||
struct ExprEngineException {
|
struct ExprEngineException {
|
||||||
|
@ -412,6 +413,7 @@ namespace {
|
||||||
return tokenizer->isCPP();
|
return tokenizer->isCPP();
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#ifdef CONTRACT
|
||||||
ExprEngine::ValuePtr executeContract(const Function *function, ExprEngine::ValuePtr (*executeExpression)(const Token*, Data&)) {
|
ExprEngine::ValuePtr executeContract(const Function *function, ExprEngine::ValuePtr (*executeExpression)(const Token*, Data&)) {
|
||||||
const auto it = settings->functionContracts.find(function->fullName());
|
const auto it = settings->functionContracts.find(function->fullName());
|
||||||
if (it == settings->functionContracts.end())
|
if (it == settings->functionContracts.end())
|
||||||
|
@ -439,6 +441,7 @@ namespace {
|
||||||
if (value)
|
if (value)
|
||||||
constraints.push_back(value);
|
constraints.push_back(value);
|
||||||
}
|
}
|
||||||
|
#endif
|
||||||
|
|
||||||
void assignValue(const Token *tok, unsigned int varId, ExprEngine::ValuePtr value) {
|
void assignValue(const Token *tok, unsigned int varId, ExprEngine::ValuePtr value) {
|
||||||
if (varId == 0)
|
if (varId == 0)
|
||||||
|
@ -617,6 +620,7 @@ namespace {
|
||||||
}
|
}
|
||||||
|
|
||||||
void addConstraints(ExprEngine::ValuePtr value, const Token *tok) {
|
void addConstraints(ExprEngine::ValuePtr value, const Token *tok) {
|
||||||
|
#ifdef CONTRACT
|
||||||
MathLib::bigint low;
|
MathLib::bigint low;
|
||||||
if (tok->getCppcheckAttribute(TokenImpl::CppcheckAttributes::Type::LOW, &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);
|
addConstraint(std::make_shared<ExprEngine::BinOpResult>(">=", value, std::make_shared<ExprEngine::IntRange>(std::to_string(low), low, low)), true);
|
||||||
|
@ -624,6 +628,7 @@ namespace {
|
||||||
MathLib::bigint high;
|
MathLib::bigint high;
|
||||||
if (tok->getCppcheckAttribute(TokenImpl::CppcheckAttributes::Type::HIGH, &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);
|
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,
|
void reportError(const Token *tok,
|
||||||
|
@ -1968,6 +1973,7 @@ static ExprEngine::ValuePtr executeIncDec(const Token *tok, Data &data)
|
||||||
#ifdef USE_Z3
|
#ifdef USE_Z3
|
||||||
static void checkContract(Data &data, const Token *tok, const Function *function, const std::vector<ExprEngine::ValuePtr> &argValues)
|
static void checkContract(Data &data, const Token *tok, const Function *function, const std::vector<ExprEngine::ValuePtr> &argValues)
|
||||||
{
|
{
|
||||||
|
#ifdef CONTRACT
|
||||||
ExprData exprData;
|
ExprData exprData;
|
||||||
z3::solver solver(exprData.context);
|
z3::solver solver(exprData.context);
|
||||||
try {
|
try {
|
||||||
|
@ -2037,6 +2043,7 @@ static void checkContract(Data &data, const Token *tok, const Function *function
|
||||||
true,
|
true,
|
||||||
functionName);
|
functionName);
|
||||||
}
|
}
|
||||||
|
#endif
|
||||||
}
|
}
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
|
@ -2096,6 +2103,7 @@ static ExprEngine::ValuePtr executeFunctionCall(const Token *tok, Data &data)
|
||||||
if (tok->astOperand1()->function()) {
|
if (tok->astOperand1()->function()) {
|
||||||
const Function *function = tok->astOperand1()->function();
|
const Function *function = tok->astOperand1()->function();
|
||||||
const std::string &functionName = function->fullName();
|
const std::string &functionName = function->fullName();
|
||||||
|
#ifdef CONTRACT
|
||||||
const auto contractIt = data.settings->functionContracts.find(functionName);
|
const auto contractIt = data.settings->functionContracts.find(functionName);
|
||||||
if (contractIt != data.settings->functionContracts.end()) {
|
if (contractIt != data.settings->functionContracts.end()) {
|
||||||
#ifdef USE_Z3
|
#ifdef USE_Z3
|
||||||
|
@ -2108,6 +2116,7 @@ static ExprEngine::ValuePtr executeFunctionCall(const Token *tok, Data &data)
|
||||||
if (!bailout)
|
if (!bailout)
|
||||||
data.addMissingContract(functionName);
|
data.addMissingContract(functionName);
|
||||||
}
|
}
|
||||||
|
#endif
|
||||||
|
|
||||||
// Execute subfunction..
|
// Execute subfunction..
|
||||||
if (hasBody) {
|
if (hasBody) {
|
||||||
|
@ -2996,7 +3005,9 @@ void ExprEngine::executeFunction(const Scope *functionScope, ErrorLogger *errorL
|
||||||
for (const Variable &arg : function->argumentList)
|
for (const Variable &arg : function->argumentList)
|
||||||
data.assignValue(functionScope->bodyStart, arg.declarationId(), createVariableValue(arg, data));
|
data.assignValue(functionScope->bodyStart, arg.declarationId(), createVariableValue(arg, data));
|
||||||
|
|
||||||
|
#ifdef CONTRACT
|
||||||
data.contractConstraints(function, executeExpression1);
|
data.contractConstraints(function, executeExpression1);
|
||||||
|
#endif
|
||||||
|
|
||||||
const std::time_t stopTime = data.startTime + data.settings->bugHuntingCheckFunctionMaxTime;
|
const std::time_t stopTime = data.startTime + data.settings->bugHuntingCheckFunctionMaxTime;
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue