walkero
/
cppcheck
1
0
Fork 0
Code Issues Pull Requests Projects Releases 1 Wiki Activity

Verification; floating point division by zero

This commit is contained in:
Daniel Marjamäki 2019-12-30 19:47:18 +01:00
parent a60efa6774
commit 4b5585e75b
4 changed files with 125 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

120
lib/exprengine.cpp
View File

@ -585,6 +585,12 @@ struct ExprData {
return e;
}
z3::expr addFloat(const std::string &name) {
z3::expr e = context.fpa_const(name.c_str(), 11, 53);
valueExpr.emplace(name, e);
return e;
}
z3::expr getExpr(const ExprEngine::BinOpResult *b) {
auto op1 = getExpr(b->op1);
auto op2 = getExpr(b->op2);
@ -634,6 +640,13 @@ struct ExprData {
return addInt(v->name, intRange->minValue, intRange->maxValue);
}
if (auto floatRange = std::dynamic_pointer_cast<ExprEngine::FloatRange>(v)) {
auto it = valueExpr.find(v->name);
if (it != valueExpr.end())
return it->second;
return addFloat(v->name);
}
if (auto b = std::dynamic_pointer_cast<ExprEngine::BinOpResult>(v)) {
return getExpr(b.get());
}
@ -725,8 +738,7 @@ bool ExprEngine::IntRange::isGreaterThan(DataBase *dataBase, int value) const
ExprData exprData;
z3::solver solver(exprData.context);
try {
z3::expr e = exprData.context.int_const(name.c_str());
exprData.valueExpr.emplace(name, e);
z3::expr e = exprData.addInt(name, minValue, maxValue);
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
solver.add(exprData.getConstraintExpr(constraint));
exprData.addAssertions(solver);
@ -755,8 +767,7 @@ bool ExprEngine::IntRange::isLessThan(DataBase *dataBase, int value) const
ExprData exprData;
z3::solver solver(exprData.context);
try {
z3::expr e = exprData.context.int_const(name.c_str());
exprData.valueExpr.emplace(name, e);
z3::expr e = exprData.addInt(name, minValue, maxValue);
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
solver.add(exprData.getConstraintExpr(constraint));
exprData.addAssertions(solver);
@ -772,6 +783,91 @@ bool ExprEngine::IntRange::isLessThan(DataBase *dataBase, int value) const
#endif
}
bool ExprEngine::FloatRange::isEqual(DataBase *dataBase, int value) const
{
const Data *data = dynamic_cast<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 {
z3::expr e = exprData.addFloat(name);
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
solver.add(exprData.getConstraintExpr(constraint));
exprData.addAssertions(solver);
solver.add(e == value);
return solver.check() != z3::unsat;
} catch (const z3::exception &exception) {
std::cerr << "z3: " << exception << std::endl;
return true; // Safe option is to return true
}
#else
// The value may or may not be in range
return false;
#endif
}
bool ExprEngine::FloatRange::isGreaterThan(DataBase *dataBase, int value) const
{
if (value < minValue || value > maxValue)
return false;
const Data *data = dynamic_cast<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 {
z3::expr e = exprData.addFloat(name);
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
solver.add(exprData.getConstraintExpr(constraint));
exprData.addAssertions(solver);
solver.add(e > value);
return solver.check() == z3::sat;
} catch (const z3::exception &exception) {
std::cerr << "z3: " << exception << std::endl;
return true; // Safe option is to return true
}
#else
// The value may or may not be in range
return false;
#endif
}
bool ExprEngine::FloatRange::isLessThan(DataBase *dataBase, int value) const
{
if (value < minValue || value > maxValue)
return false;
const Data *data = dynamic_cast<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 {
z3::expr e = exprData.addFloat(name);
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
solver.add(exprData.getConstraintExpr(constraint));
exprData.addAssertions(solver);
solver.add(e < value);
return solver.check() == z3::sat;
} catch (const z3::exception &exception) {
std::cerr << "z3: " << exception << std::endl;
return true; // Safe option is to return true
}
#else
// The value may or may not be in range
return false;
#endif
}
bool ExprEngine::BinOpResult::isEqual(ExprEngine::DataBase *dataBase, int value) const
{
#ifdef USE_Z3
@ -913,16 +1009,10 @@ static ExprEngine::ValuePtr getValueRangeFromValueType(const std::string &name,
}
}
switch (vt->type) {
case ValueType::Type::FLOAT:
return std::make_shared<ExprEngine::FloatRange>(name, std::numeric_limits<float>::min(), std::numeric_limits<float>::max());
case ValueType::Type::DOUBLE:
return std::make_shared<ExprEngine::FloatRange>(name, std::numeric_limits<double>::min(), std::numeric_limits<double>::max());
case ValueType::Type::LONGDOUBLE:
return std::make_shared<ExprEngine::FloatRange>(name, std::numeric_limits<long double>::min(), std::numeric_limits<long double>::max());
default:
return ExprEngine::ValuePtr();
};
if (vt->isFloat())
return std::make_shared<ExprEngine::FloatRange>(name, -std::numeric_limits<float>::infinity(), std::numeric_limits<float>::infinity());
return ExprEngine::ValuePtr();
}
static void call(const std::vector<ExprEngine::Callback> &callbacks, const Token *tok, ExprEngine::ValuePtr value, Data *dataBase)
@ -1558,7 +1648,7 @@ static ExprEngine::ValuePtr createVariableValue(const Variable &var, Data &data)
}
if (var.isArray())
return std::make_shared<ExprEngine::ArrayValue>(&data, &var);
if (valueType->isIntegral()) {
if (valueType->isIntegral() || valueType->isFloat()) {
auto value = getValueRangeFromValueType(data.getNewSymbolName(), valueType, *data.settings);
data.addConstraints(value, var.nameToken());
return value;

9
lib/exprengine.h
View File

@ -149,15 +149,14 @@ namespace ExprEngine {
, maxValue(maxValue) {
}
bool isEqual(DataBase *dataBase, int value) const OVERRIDE {
(void)dataBase;
return value >= minValue && value <= maxValue;
}
std::string getRange() const OVERRIDE {
return std::to_string(minValue) + ":" + std::to_string(maxValue);
}
bool isEqual(DataBase *dataBase, int value) const OVERRIDE;
bool isGreaterThan(DataBase *dataBase, int value) const OVERRIDE;
bool isLessThan(DataBase *dataBase, int value) const OVERRIDE;
long double minValue;
long double maxValue;
};

12
test/testexprengine.cpp
View File

@ -67,6 +67,7 @@ private:
TEST_CASE(floatValue1);
TEST_CASE(floatValue2);
TEST_CASE(floatValue3);
TEST_CASE(functionCall1);
TEST_CASE(functionCall2);
@ -397,13 +398,22 @@ private:
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"));
ASSERT_EQUALS("-inf:inf", getRange("float f; void func() { f=f; }", "f=f"));
}
void floatValue2() {
ASSERT_EQUALS("(29.0)/(2.0)", getRange("void func() { float f = 29.0; f = f / 2.0; }", "f/2.0"));
}
void floatValue3() {
const char code[] = "void foo(float f) { return f > 12.0; }";
const char expected[] = "(declare-fun |12.0| () (_ FloatingPoint 11 53))\n"
"(declare-fun $1 () (_ FloatingPoint 11 53))\n"
"(assert (fp.gt $1 |12.0|))\n"
"z3::sat";
ASSERT_EQUALS(expected, expr(code, ">"));
}
void functionCall1() {
ASSERT_EQUALS("-2147483648:2147483647", getRange("int atoi(const char *p); void f() { int x = atoi(a); x = x; }", "x=x"));

5
test/testsuites/danmar-verify/divbyzero.cpp
View File

@ -30,6 +30,11 @@ void float1(float f) {
return 100000 / (int)f;
}
void float2(float f) {
// cppcheck-suppress verificationDivByZero
return 100000 / f;
}
void stdmap(std::map<int,int> &data) {
// cppcheck-suppress verificationDivByZero
return 100000 / data[43];