From cba8b99095c2df133048ee6b7dc4a9061d83514f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Marjam=C3=A4ki?= Date: Sat, 12 Dec 2020 17:33:10 +0100 Subject: [PATCH] ExprEngine: Catch and handle exceptions in ExprData --- lib/exprengine.cpp | 61 ++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 53 insertions(+), 8 deletions(-) diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp index 6cba2f79d..07bbd7a3d 100644 --- a/lib/exprengine.cpp +++ b/lib/exprengine.cpp @@ -1213,6 +1213,10 @@ bool ExprEngine::IntRange::isEqual(DataBase *dataBase, int value) const } 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 in range @@ -1241,6 +1245,10 @@ bool ExprEngine::IntRange::isGreaterThan(DataBase *dataBase, int value) const } 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 in range @@ -1269,6 +1277,10 @@ bool ExprEngine::IntRange::isLessThan(DataBase *dataBase, int value) const } 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 in range @@ -1298,6 +1310,10 @@ bool ExprEngine::FloatRange::isEqual(DataBase *dataBase, int value) const } 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 in range @@ -1328,6 +1344,10 @@ bool ExprEngine::FloatRange::isGreaterThan(DataBase *dataBase, int value) const } 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 in range @@ -1358,6 +1378,10 @@ bool ExprEngine::FloatRange::isLessThan(DataBase *dataBase, int value) const } 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 in range @@ -1369,13 +1393,22 @@ bool ExprEngine::FloatRange::isLessThan(DataBase *dataBase, int value) const bool ExprEngine::BinOpResult::isEqual(ExprEngine::DataBase *dataBase, int value) const { #ifdef USE_Z3 - ExprData exprData; - z3::solver solver(exprData.context); - z3::expr e = exprData.getExpr(this); - exprData.addConstraints(solver, dynamic_cast(dataBase)); - exprData.addAssertions(solver); - solver.add(exprData.int_expr(e) == value); - return solver.check() == z3::sat; + try { + ExprData exprData; + z3::solver solver(exprData.context); + z3::expr e = exprData.getExpr(this); + exprData.addConstraints(solver, dynamic_cast(dataBase)); + exprData.addAssertions(solver); + solver.add(exprData.int_expr(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 + } catch (const ExprData::BailoutValueException &) { + return true; // Safe option is to return true + } catch (const ExprEngineException &) { + return true; // Safe option is to return true + } #else (void)dataBase; (void)value; @@ -1397,6 +1430,10 @@ bool ExprEngine::BinOpResult::isGreaterThan(ExprEngine::DataBase *dataBase, int } 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 (void)dataBase; @@ -1419,6 +1456,10 @@ bool ExprEngine::BinOpResult::isLessThan(ExprEngine::DataBase *dataBase, int val } 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 (void)dataBase; @@ -1441,6 +1482,10 @@ bool ExprEngine::BinOpResult::isTrue(ExprEngine::DataBase *dataBase) const } 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 (void)dataBase; @@ -2688,7 +2733,7 @@ void ExprEngine::executeFunction(const Scope *functionScope, ErrorLogger *errorL try { execute(functionScope->bodyStart, functionScope->bodyEnd, data); - } catch (ExprEngineException &e) { + } catch (const ExprEngineException &e) { if (settings->debugBugHunting) report << "ExprEngineException tok.line:" << e.tok->linenr() << " what:" << e.what << "\n"; trackExecution.setAbortLine(e.tok->linenr());