Bug hunting: Better analysis of BailoutValue
This commit is contained in:
parent
7e9cbda2d5
commit
39a9350f6e
|
@ -1029,10 +1029,16 @@ std::string ExprEngine::IntegerTruncation::getSymbolicExpression() const
|
||||||
|
|
||||||
#ifdef USE_Z3
|
#ifdef USE_Z3
|
||||||
|
|
||||||
struct ExprData {
|
class ExprData {
|
||||||
|
public:
|
||||||
typedef std::map<std::string, z3::expr> ValueExpr;
|
typedef std::map<std::string, z3::expr> ValueExpr;
|
||||||
typedef std::vector<z3::expr> AssertionList;
|
typedef std::vector<z3::expr> AssertionList;
|
||||||
|
|
||||||
|
class BailoutValueException: public ExprEngineException {
|
||||||
|
public:
|
||||||
|
BailoutValueException() : ExprEngineException(nullptr, "Incomplete analysis") {}
|
||||||
|
};
|
||||||
|
|
||||||
z3::context context;
|
z3::context context;
|
||||||
ValueExpr valueExpr;
|
ValueExpr valueExpr;
|
||||||
AssertionList assertionList;
|
AssertionList assertionList;
|
||||||
|
@ -1042,6 +1048,15 @@ struct ExprData {
|
||||||
solver.add(assertExpr);
|
solver.add(assertExpr);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
void addConstraints(z3::solver &solver, const Data* data) {
|
||||||
|
for (auto constraint : data->constraints) {
|
||||||
|
try {
|
||||||
|
solver.add(getConstraintExpr(constraint));
|
||||||
|
} catch (const BailoutValueException &) {
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
z3::expr addInt(const std::string &name, int128_t minValue, int128_t maxValue) {
|
z3::expr addInt(const std::string &name, int128_t minValue, int128_t maxValue) {
|
||||||
z3::expr e = context.int_const(name.c_str());
|
z3::expr e = context.int_const(name.c_str());
|
||||||
valueExpr.emplace(name, e);
|
valueExpr.emplace(name, e);
|
||||||
|
@ -1108,6 +1123,8 @@ struct ExprData {
|
||||||
z3::expr getExpr(ExprEngine::ValuePtr v) {
|
z3::expr getExpr(ExprEngine::ValuePtr v) {
|
||||||
if (!v)
|
if (!v)
|
||||||
throw ExprEngineException(nullptr, "Can not solve expressions, operand value is null");
|
throw ExprEngineException(nullptr, "Can not solve expressions, operand value is null");
|
||||||
|
if (v->type == ExprEngine::ValueType::BailoutValue)
|
||||||
|
throw BailoutValueException();
|
||||||
if (auto intRange = std::dynamic_pointer_cast<ExprEngine::IntRange>(v)) {
|
if (auto intRange = std::dynamic_pointer_cast<ExprEngine::IntRange>(v)) {
|
||||||
if (intRange->name[0] != '$')
|
if (intRange->name[0] != '$')
|
||||||
#if Z3_VERSION_INT >= GET_VERSION_INT(4,7,1)
|
#if Z3_VERSION_INT >= GET_VERSION_INT(4,7,1)
|
||||||
|
@ -1162,7 +1179,6 @@ struct ExprData {
|
||||||
}
|
}
|
||||||
|
|
||||||
private:
|
private:
|
||||||
|
|
||||||
z3::expr bool_expr(z3::expr e) {
|
z3::expr bool_expr(z3::expr e) {
|
||||||
if (e.is_bool())
|
if (e.is_bool())
|
||||||
return e;
|
return e;
|
||||||
|
@ -1191,8 +1207,7 @@ bool ExprEngine::IntRange::isEqual(DataBase *dataBase, int value) const
|
||||||
z3::solver solver(exprData.context);
|
z3::solver solver(exprData.context);
|
||||||
try {
|
try {
|
||||||
z3::expr e = exprData.addInt(name, minValue, maxValue);
|
z3::expr e = exprData.addInt(name, minValue, maxValue);
|
||||||
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
|
exprData.addConstraints(solver, data);
|
||||||
solver.add(exprData.getConstraintExpr(constraint));
|
|
||||||
exprData.addAssertions(solver);
|
exprData.addAssertions(solver);
|
||||||
solver.add(e == value);
|
solver.add(e == value);
|
||||||
return solver.check() == z3::sat;
|
return solver.check() == z3::sat;
|
||||||
|
@ -1220,8 +1235,7 @@ bool ExprEngine::IntRange::isGreaterThan(DataBase *dataBase, int value) const
|
||||||
z3::solver solver(exprData.context);
|
z3::solver solver(exprData.context);
|
||||||
try {
|
try {
|
||||||
z3::expr e = exprData.addInt(name, minValue, maxValue);
|
z3::expr e = exprData.addInt(name, minValue, maxValue);
|
||||||
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
|
exprData.addConstraints(solver, data);
|
||||||
solver.add(exprData.getConstraintExpr(constraint));
|
|
||||||
exprData.addAssertions(solver);
|
exprData.addAssertions(solver);
|
||||||
solver.add(e > value);
|
solver.add(e > value);
|
||||||
return solver.check() == z3::sat;
|
return solver.check() == z3::sat;
|
||||||
|
@ -1249,8 +1263,7 @@ bool ExprEngine::IntRange::isLessThan(DataBase *dataBase, int value) const
|
||||||
z3::solver solver(exprData.context);
|
z3::solver solver(exprData.context);
|
||||||
try {
|
try {
|
||||||
z3::expr e = exprData.addInt(name, minValue, maxValue);
|
z3::expr e = exprData.addInt(name, minValue, maxValue);
|
||||||
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
|
exprData.addConstraints(solver, data);
|
||||||
solver.add(exprData.getConstraintExpr(constraint));
|
|
||||||
exprData.addAssertions(solver);
|
exprData.addAssertions(solver);
|
||||||
solver.add(e < value);
|
solver.add(e < value);
|
||||||
return solver.check() == z3::sat;
|
return solver.check() == z3::sat;
|
||||||
|
@ -1279,8 +1292,7 @@ bool ExprEngine::FloatRange::isEqual(DataBase *dataBase, int value) const
|
||||||
z3::solver solver(exprData.context);
|
z3::solver solver(exprData.context);
|
||||||
try {
|
try {
|
||||||
z3::expr e = exprData.addFloat(name);
|
z3::expr e = exprData.addFloat(name);
|
||||||
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
|
exprData.addConstraints(solver, data);
|
||||||
solver.add(exprData.getConstraintExpr(constraint));
|
|
||||||
exprData.addAssertions(solver);
|
exprData.addAssertions(solver);
|
||||||
solver.add(e >= value && e <= value);
|
solver.add(e >= value && e <= value);
|
||||||
return solver.check() != z3::unsat;
|
return solver.check() != z3::unsat;
|
||||||
|
@ -1310,8 +1322,7 @@ bool ExprEngine::FloatRange::isGreaterThan(DataBase *dataBase, int value) const
|
||||||
z3::solver solver(exprData.context);
|
z3::solver solver(exprData.context);
|
||||||
try {
|
try {
|
||||||
z3::expr e = exprData.addFloat(name);
|
z3::expr e = exprData.addFloat(name);
|
||||||
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
|
exprData.addConstraints(solver, data);
|
||||||
solver.add(exprData.getConstraintExpr(constraint));
|
|
||||||
exprData.addAssertions(solver);
|
exprData.addAssertions(solver);
|
||||||
solver.add(e > value);
|
solver.add(e > value);
|
||||||
return solver.check() == z3::sat;
|
return solver.check() == z3::sat;
|
||||||
|
@ -1341,8 +1352,7 @@ bool ExprEngine::FloatRange::isLessThan(DataBase *dataBase, int value) const
|
||||||
z3::solver solver(exprData.context);
|
z3::solver solver(exprData.context);
|
||||||
try {
|
try {
|
||||||
z3::expr e = exprData.addFloat(name);
|
z3::expr e = exprData.addFloat(name);
|
||||||
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
|
exprData.addConstraints(solver, data);
|
||||||
solver.add(exprData.getConstraintExpr(constraint));
|
|
||||||
exprData.addAssertions(solver);
|
exprData.addAssertions(solver);
|
||||||
solver.add(e < value);
|
solver.add(e < value);
|
||||||
return solver.check() == z3::sat;
|
return solver.check() == z3::sat;
|
||||||
|
@ -1363,8 +1373,7 @@ bool ExprEngine::BinOpResult::isEqual(ExprEngine::DataBase *dataBase, int value)
|
||||||
ExprData exprData;
|
ExprData exprData;
|
||||||
z3::solver solver(exprData.context);
|
z3::solver solver(exprData.context);
|
||||||
z3::expr e = exprData.getExpr(this);
|
z3::expr e = exprData.getExpr(this);
|
||||||
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
|
exprData.addConstraints(solver, dynamic_cast<const Data *>(dataBase));
|
||||||
solver.add(exprData.getConstraintExpr(constraint));
|
|
||||||
exprData.addAssertions(solver);
|
exprData.addAssertions(solver);
|
||||||
solver.add(e == value);
|
solver.add(e == value);
|
||||||
return solver.check() == z3::sat;
|
return solver.check() == z3::sat;
|
||||||
|
@ -1382,8 +1391,7 @@ bool ExprEngine::BinOpResult::isGreaterThan(ExprEngine::DataBase *dataBase, int
|
||||||
ExprData exprData;
|
ExprData exprData;
|
||||||
z3::solver solver(exprData.context);
|
z3::solver solver(exprData.context);
|
||||||
z3::expr e = exprData.getExpr(this);
|
z3::expr e = exprData.getExpr(this);
|
||||||
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
|
exprData.addConstraints(solver, dynamic_cast<const Data *>(dataBase));
|
||||||
solver.add(exprData.getConstraintExpr(constraint));
|
|
||||||
exprData.addAssertions(solver);
|
exprData.addAssertions(solver);
|
||||||
solver.add(e > value);
|
solver.add(e > value);
|
||||||
return solver.check() == z3::sat;
|
return solver.check() == z3::sat;
|
||||||
|
@ -1405,8 +1413,7 @@ bool ExprEngine::BinOpResult::isLessThan(ExprEngine::DataBase *dataBase, int val
|
||||||
ExprData exprData;
|
ExprData exprData;
|
||||||
z3::solver solver(exprData.context);
|
z3::solver solver(exprData.context);
|
||||||
z3::expr e = exprData.getExpr(this);
|
z3::expr e = exprData.getExpr(this);
|
||||||
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
|
exprData.addConstraints(solver, dynamic_cast<const Data *>(dataBase));
|
||||||
solver.add(exprData.getConstraintExpr(constraint));
|
|
||||||
exprData.addAssertions(solver);
|
exprData.addAssertions(solver);
|
||||||
solver.add(e < value);
|
solver.add(e < value);
|
||||||
return solver.check() == z3::sat;
|
return solver.check() == z3::sat;
|
||||||
|
@ -1428,8 +1435,7 @@ bool ExprEngine::BinOpResult::isTrue(ExprEngine::DataBase *dataBase) const
|
||||||
ExprData exprData;
|
ExprData exprData;
|
||||||
z3::solver solver(exprData.context);
|
z3::solver solver(exprData.context);
|
||||||
z3::expr e = exprData.getExpr(this);
|
z3::expr e = exprData.getExpr(this);
|
||||||
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
|
exprData.addConstraints(solver, dynamic_cast<const Data *>(dataBase));
|
||||||
solver.add(exprData.getConstraintExpr(constraint));
|
|
||||||
exprData.addAssertions(solver);
|
exprData.addAssertions(solver);
|
||||||
return solver.check() == z3::sat;
|
return solver.check() == z3::sat;
|
||||||
} catch (const z3::exception &exception) {
|
} catch (const z3::exception &exception) {
|
||||||
|
@ -1449,8 +1455,7 @@ std::string ExprEngine::BinOpResult::getExpr(ExprEngine::DataBase *dataBase) con
|
||||||
ExprData exprData;
|
ExprData exprData;
|
||||||
z3::solver solver(exprData.context);
|
z3::solver solver(exprData.context);
|
||||||
z3::expr e = exprData.getExpr(this);
|
z3::expr e = exprData.getExpr(this);
|
||||||
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
|
exprData.addConstraints(solver, dynamic_cast<const Data *>(dataBase));
|
||||||
solver.add(exprData.getConstraintExpr(constraint));
|
|
||||||
exprData.addAssertions(solver);
|
exprData.addAssertions(solver);
|
||||||
solver.add(e);
|
solver.add(e);
|
||||||
std::ostringstream os;
|
std::ostringstream os;
|
||||||
|
@ -1767,7 +1772,11 @@ static void checkContract(Data &data, const Token *tok, const Function *function
|
||||||
z3::solver solver(exprData.context);
|
z3::solver solver(exprData.context);
|
||||||
try {
|
try {
|
||||||
// Invert contract, we want to know if the contract might not be met
|
// Invert contract, we want to know if the contract might not be met
|
||||||
|
try {
|
||||||
solver.add(z3::ite(exprData.getConstraintExpr(data.executeContract(function, executeExpression1)), exprData.context.bool_val(false), exprData.context.bool_val(true)));
|
solver.add(z3::ite(exprData.getConstraintExpr(data.executeContract(function, executeExpression1)), exprData.context.bool_val(false), exprData.context.bool_val(true)));
|
||||||
|
} catch (const ExprData::BailoutValueException &) {
|
||||||
|
throw ExprEngineException(tok, "Internal error: Bailout value used");
|
||||||
|
}
|
||||||
|
|
||||||
bool bailoutValue = false;
|
bool bailoutValue = false;
|
||||||
for (nonneg int i = 0; i < argValues.size(); ++i) {
|
for (nonneg int i = 0; i < argValues.size(); ++i) {
|
||||||
|
@ -1814,7 +1823,7 @@ static void checkContract(Data &data, const Token *tok, const Function *function
|
||||||
}
|
}
|
||||||
} catch (const z3::exception &exception) {
|
} catch (const z3::exception &exception) {
|
||||||
std::cerr << "z3: " << exception << std::endl;
|
std::cerr << "z3: " << exception << std::endl;
|
||||||
} catch (const ExprEngineException &e) {
|
} catch (const ExprEngineException &) {
|
||||||
const char id[] = "internalErrorInExprEngine";
|
const char id[] = "internalErrorInExprEngine";
|
||||||
const auto contractIt = data.settings->functionContracts.find(function->fullName());
|
const auto contractIt = data.settings->functionContracts.find(function->fullName());
|
||||||
const std::string functionName = contractIt->first;
|
const std::string functionName = contractIt->first;
|
||||||
|
|
|
@ -39,6 +39,7 @@ private:
|
||||||
TEST_CASE(arrayIndexOutOfBounds1);
|
TEST_CASE(arrayIndexOutOfBounds1);
|
||||||
TEST_CASE(arrayIndexOutOfBounds2);
|
TEST_CASE(arrayIndexOutOfBounds2);
|
||||||
TEST_CASE(arrayIndexOutOfBounds3);
|
TEST_CASE(arrayIndexOutOfBounds3);
|
||||||
|
TEST_CASE(arrayIndexOutOfBounds4);
|
||||||
TEST_CASE(bufferOverflowMemCmp1);
|
TEST_CASE(bufferOverflowMemCmp1);
|
||||||
TEST_CASE(bufferOverflowMemCmp2);
|
TEST_CASE(bufferOverflowMemCmp2);
|
||||||
TEST_CASE(bufferOverflowStrcpy1);
|
TEST_CASE(bufferOverflowStrcpy1);
|
||||||
|
@ -119,6 +120,21 @@ private:
|
||||||
errout.str());
|
errout.str());
|
||||||
}
|
}
|
||||||
|
|
||||||
|
void arrayIndexOutOfBounds4() { // ensure there are warnings for bailout value
|
||||||
|
check("void foo(short i) {\n"
|
||||||
|
" int buf[8];\n"
|
||||||
|
"\n"
|
||||||
|
" data *d = x;\n"
|
||||||
|
" switch (d->layout) { case 0: break; }\n"
|
||||||
|
"\n"
|
||||||
|
" if (buf[i] > 0) {}\n"
|
||||||
|
"}");
|
||||||
|
ASSERT_EQUALS("[test.cpp:7]: (error) Array index out of bounds, cannot determine that i is less than 8\n"
|
||||||
|
"[test.cpp:7]: (error) Array index out of bounds, cannot determine that i is not negative\n"
|
||||||
|
"[test.cpp:7]: (error) Cannot determine that 'buf[i]' is initialized\n",
|
||||||
|
errout.str());
|
||||||
|
}
|
||||||
|
|
||||||
void bufferOverflowMemCmp1() {
|
void bufferOverflowMemCmp1() {
|
||||||
// CVE-2020-24265
|
// CVE-2020-24265
|
||||||
check("void foo(const char *pktdata, int datalen) {\n"
|
check("void foo(const char *pktdata, int datalen) {\n"
|
||||||
|
|
Loading…
Reference in New Issue