cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Add error IDs to BMC

Browse Source
This commit is contained in:
a3d4 2020-05-12 02:29:54 +02:00
parent 1d5350e32f
commit 7cae074b8a
2 changed files with 29 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

40
libsolidity/formal/BMC.cpp
View File

@ -21,8 +21,6 @@
#include <libsolidity/formal/SymbolicState.h> #include <libsolidity/formal/SymbolicState.h>
#include <libsolidity/formal/SymbolicTypes.h> #include <libsolidity/formal/SymbolicTypes.h>
#include <boost/algorithm/string/replace.hpp>
using namespace std; using namespace std;
using namespace solidity; using namespace solidity;
using namespace solidity::util; using namespace solidity::util;
@ -594,8 +592,7 @@ void BMC::checkConstantCondition(BMCVerificationTarget& _target)
*_target.expression, *_target.expression,
_target.constraints, _target.constraints,
_target.value, _target.value,
_target.callStack, _target.callStack
"Condition is always $VALUE."
); );
} }
@ -613,6 +610,8 @@ void BMC::checkUnderflow(BMCVerificationTarget& _target, smt::Expression const&
_target.callStack, _target.callStack,
_target.modelExpressions, _target.modelExpressions,
_target.expression->location(), _target.expression->location(),
4144_error,
8312_error,
"Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ")", "Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ")",
"<result>", "<result>",
&_target.value &_target.value
@ -633,6 +632,8 @@ void BMC::checkOverflow(BMCVerificationTarget& _target, smt::Expression const& _
_target.callStack, _target.callStack,
_target.modelExpressions, _target.modelExpressions,
_target.expression->location(), _target.expression->location(),
2661_error,
8065_error,
"Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ")", "Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ")",
"<result>", "<result>",
&_target.value &_target.value
@ -647,6 +648,8 @@ void BMC::checkDivByZero(BMCVerificationTarget& _target)
_target.callStack, _target.callStack,
_target.modelExpressions, _target.modelExpressions,
_target.expression->location(), _target.expression->location(),
3046_error,
5272_error,
"Division by zero", "Division by zero",
"<result>", "<result>",
&_target.value &_target.value
@ -661,6 +664,8 @@ void BMC::checkBalance(BMCVerificationTarget& _target)
_target.callStack, _target.callStack,
_target.modelExpressions, _target.modelExpressions,
_target.expression->location(), _target.expression->location(),
1236_error,
4010_error,
"Insufficient funds", "Insufficient funds",
"address(this).balance" "address(this).balance"
); );
@ -675,6 +680,8 @@ void BMC::checkAssert(BMCVerificationTarget& _target)
_target.callStack, _target.callStack,
_target.modelExpressions, _target.modelExpressions,
_target.expression->location(), _target.expression->location(),
4661_error,
7812_error,
"Assertion violation" "Assertion violation"
); );
} }
@ -705,9 +712,11 @@ void BMC::addVerificationTarget(
void BMC::checkCondition( void BMC::checkCondition(
smt::Expression _condition, smt::Expression _condition,
vector<SMTEncoder::CallStackEntry> const& callStack, vector<SMTEncoder::CallStackEntry> const& _callStack,
pair<vector<smt::Expression>, vector<string>> const& _modelExpressions, pair<vector<smt::Expression>, vector<string>> const& _modelExpressions,
SourceLocation const& _location, SourceLocation const& _location,
ErrorId _errorHappens,
ErrorId _errorMightHappen,
string const& _description, string const& _description,
string const& _additionalValueName, string const& _additionalValueName,
smt::Expression const* _additionalValue smt::Expression const* _additionalValue
@ -719,7 +728,7 @@ void BMC::checkCondition(
vector<smt::Expression> expressionsToEvaluate; vector<smt::Expression> expressionsToEvaluate;
vector<string> expressionNames; vector<string> expressionNames;
tie(expressionsToEvaluate, expressionNames) = _modelExpressions; tie(expressionsToEvaluate, expressionNames) = _modelExpressions;
if (callStack.size()) if (_callStack.size())
if (_additionalValue) if (_additionalValue)
{ {
expressionsToEvaluate.emplace_back(*_additionalValue); expressionsToEvaluate.emplace_back(*_additionalValue);
@ -750,7 +759,7 @@ void BMC::checkCondition(
{ {
std::ostringstream message; std::ostringstream message;
message << _description << " happens here"; message << _description << " happens here";
if (callStack.size()) if (_callStack.size())
{ {
std::ostringstream modelMessage; std::ostringstream modelMessage;
modelMessage << " for:\n"; modelMessage << " for:\n";
@ -763,11 +772,11 @@ void BMC::checkCondition(
for (auto const& eval: sortedModel) for (auto const& eval: sortedModel)
modelMessage << " " << eval.first << " = " << eval.second << "\n"; modelMessage << " " << eval.first << " = " << eval.second << "\n";
m_errorReporter.warning( m_errorReporter.warning(
4334_error, _errorHappens,
_location, _location,
message.str(), message.str(),
SecondarySourceLocation().append(modelMessage.str(), SourceLocation{}) SecondarySourceLocation().append(modelMessage.str(), SourceLocation{})
.append(SMTEncoder::callStackMessage(callStack)) .append(SMTEncoder::callStackMessage(_callStack))
.append(move(secondaryLocation)) .append(move(secondaryLocation))
); );
} }
@ -781,7 +790,7 @@ void BMC::checkCondition(
case smt::CheckResult::UNSATISFIABLE: case smt::CheckResult::UNSATISFIABLE:
break; break;
case smt::CheckResult::UNKNOWN: case smt::CheckResult::UNKNOWN:
m_errorReporter.warning(5225_error, _location, _description + " might happen here.", secondaryLocation); m_errorReporter.warning(_errorMightHappen, _location, _description + " might happen here.", secondaryLocation);
break; break;
case smt::CheckResult::CONFLICTING: case smt::CheckResult::CONFLICTING:
m_errorReporter.warning(1584_error, _location, "At least two SMT solvers provided conflicting answers. Results might not be sound."); m_errorReporter.warning(1584_error, _location, "At least two SMT solvers provided conflicting answers. Results might not be sound.");
@ -798,8 +807,7 @@ void BMC::checkBooleanNotConstant(
Expression const& _condition, Expression const& _condition,
smt::Expression const& _constraints, smt::Expression const& _constraints,
smt::Expression const& _value, smt::Expression const& _value,
vector<SMTEncoder::CallStackEntry> const& _callStack, vector<SMTEncoder::CallStackEntry> const& _callStack
string const& _description
) )
{ {
// Do not check for const-ness if this is a constant. // Do not check for const-ness if this is a constant.
@ -832,22 +840,22 @@ void BMC::checkBooleanNotConstant(
m_errorReporter.warning(2512_error, _condition.location(), "Condition unreachable.", SMTEncoder::callStackMessage(_callStack)); m_errorReporter.warning(2512_error, _condition.location(), "Condition unreachable.", SMTEncoder::callStackMessage(_callStack));
else else
{ {
string value; string description;
if (positiveResult == smt::CheckResult::SATISFIABLE) if (positiveResult == smt::CheckResult::SATISFIABLE)
{ {
solAssert(negatedResult == smt::CheckResult::UNSATISFIABLE, ""); solAssert(negatedResult == smt::CheckResult::UNSATISFIABLE, "");
value = "true"; description = "Condition is always true.";
} }
else else
{ {
solAssert(positiveResult == smt::CheckResult::UNSATISFIABLE, ""); solAssert(positiveResult == smt::CheckResult::UNSATISFIABLE, "");
solAssert(negatedResult == smt::CheckResult::SATISFIABLE, ""); solAssert(negatedResult == smt::CheckResult::SATISFIABLE, "");
value = "false"; description = "Condition is always false.";
} }
m_errorReporter.warning( m_errorReporter.warning(
6838_error, 6838_error,
_condition.location(), _condition.location(),
boost::algorithm::replace_all_copy(_description, "$VALUE", value), description,
SMTEncoder::callStackMessage(_callStack) SMTEncoder::callStackMessage(_callStack)
); );
} }

9
libsolidity/formal/BMC.h
View File

@ -44,6 +44,7 @@ using solidity::util::h256;
namespace solidity::langutil namespace solidity::langutil
{ {
class ErrorReporter; class ErrorReporter;
struct ErrorId;
struct SourceLocation; struct SourceLocation;
} }
@ -144,22 +145,22 @@ private:
/// Check that a condition can be satisfied. /// Check that a condition can be satisfied.
void checkCondition( void checkCondition(
smt::Expression _condition, smt::Expression _condition,
std::vector<CallStackEntry> const& callStack, std::vector<CallStackEntry> const& _callStack,
std::pair<std::vector<smt::Expression>, std::vector<std::string>> const& _modelExpressions, std::pair<std::vector<smt::Expression>, std::vector<std::string>> const& _modelExpressions,
langutil::SourceLocation const& _location, langutil::SourceLocation const& _location,
langutil::ErrorId _errorHappens,
langutil::ErrorId _errorMightHappen,
std::string const& _description, std::string const& _description,
std::string const& _additionalValueName = "", std::string const& _additionalValueName = "",
smt::Expression const* _additionalValue = nullptr smt::Expression const* _additionalValue = nullptr
); );
/// Checks that a boolean condition is not constant. Do not warn if the expression /// Checks that a boolean condition is not constant. Do not warn if the expression
/// is a literal constant. /// is a literal constant.
/// @param _description the warning string, $VALUE will be replaced by the constant value.
void checkBooleanNotConstant( void checkBooleanNotConstant(
Expression const& _condition, Expression const& _condition,
smt::Expression const& _constraints, smt::Expression const& _constraints,
smt::Expression const& _value, smt::Expression const& _value,
std::vector<CallStackEntry> const& _callStack, std::vector<CallStackEntry> const& _callStack
std::string const& _description
); );
std::pair<smt::CheckResult, std::vector<std::string>> std::pair<smt::CheckResult, std::vector<std::string>>
checkSatisfiableAndGenerateModel(std::vector<smt::Expression> const& _expressionsToEvaluate); checkSatisfiableAndGenerateModel(std::vector<smt::Expression> const& _expressionsToEvaluate);