From 4b5585e75b11b0b3dfce9649de7c916933cdd713 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Marjam=C3=A4ki?= Date: Mon, 30 Dec 2019 19:47:18 +0100 Subject: [PATCH] Verification; floating point division by zero --- lib/exprengine.cpp | 120 +++++++++++++++++--- lib/exprengine.h | 9 +- test/testexprengine.cpp | 12 +- test/testsuites/danmar-verify/divbyzero.cpp | 5 + 4 files changed, 125 insertions(+), 21 deletions(-) diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp index a7ddaa489..0f43f331c 100644 --- a/lib/exprengine.cpp +++ b/lib/exprengine.cpp @@ -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(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(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(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(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(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(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(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(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(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(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(name, std::numeric_limits::min(), std::numeric_limits::max()); - case ValueType::Type::DOUBLE: - return std::make_shared(name, std::numeric_limits::min(), std::numeric_limits::max()); - case ValueType::Type::LONGDOUBLE: - return std::make_shared(name, std::numeric_limits::min(), std::numeric_limits::max()); - default: - return ExprEngine::ValuePtr(); - }; + if (vt->isFloat()) + return std::make_shared(name, -std::numeric_limits::infinity(), std::numeric_limits::infinity()); + + return ExprEngine::ValuePtr(); } static void call(const std::vector &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(&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; diff --git a/lib/exprengine.h b/lib/exprengine.h index 463fe08c2..a4236bca7 100644 --- a/lib/exprengine.h +++ b/lib/exprengine.h @@ -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; }; diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp index 9c92781f6..2ea8a1a8b 100644 --- a/test/testexprengine.cpp +++ b/test/testexprengine.cpp @@ -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::min()) + ":" + std::to_string(std::numeric_limits::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")); diff --git a/test/testsuites/danmar-verify/divbyzero.cpp b/test/testsuites/danmar-verify/divbyzero.cpp index c2c3fc737..d75b5a557 100644 --- a/test/testsuites/danmar-verify/divbyzero.cpp +++ b/test/testsuites/danmar-verify/divbyzero.cpp @@ -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 &data) { // cppcheck-suppress verificationDivByZero return 100000 / data[43];