cerc-io/solidity
16
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

[SMTChecker] Adding a dummy frame to the call stack for the implicit constructor

Browse Source
This commit is contained in:
Martin Blicha 2020-11-16 17:52:06 +01:00
parent d7814358a6
commit 07427c798c
4 changed files with 62 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

43
libsolidity/formal/BMC.cpp
View File

@ -120,7 +120,10 @@ void BMC::endVisit(ContractDefinition const& _contract)
constructor->accept(*this);
else
{
/// Visiting implicit constructor - we need a dummy callstack frame
pushCallStack({nullptr, nullptr});
inlineConstructorHierarchy(_contract);
popCallStack();
/// Check targets created by state variable initialization.
smtutil::Expression constraints = m_context.assertions();
checkVerificationTargets(constraints);
@ -831,32 +834,28 @@ void BMC::checkCondition(
{
case smtutil::CheckResult::SATISFIABLE:
{
solAssert(!_callStack.empty(), "");
std::ostringstream message;
message << "BMC: " << _description << " happens here.";
if (_callStack.size())
{
std::ostringstream modelMessage;
modelMessage << "Counterexample:\n";
solAssert(values.size() == expressionNames.size(), "");
map<string, string> sortedModel;
for (size_t i = 0; i < values.size(); ++i)
if (expressionsToEvaluate.at(i).name != values.at(i))
sortedModel[expressionNames.at(i)] = values.at(i);
std::ostringstream modelMessage;
modelMessage << "Counterexample:\n";
solAssert(values.size() == expressionNames.size(), "");
map<string, string> sortedModel;
for (size_t i = 0; i < values.size(); ++i)
if (expressionsToEvaluate.at(i).name != values.at(i))
sortedModel[expressionNames.at(i)] = values.at(i);
for (auto const& eval: sortedModel)
modelMessage << " " << eval.first << " = " << eval.second << "\n";
for (auto const& eval: sortedModel)
modelMessage << " " << eval.first << " = " << eval.second << "\n";
m_errorReporter.warning(
_errorHappens,
_location,
message.str(),
SecondarySourceLocation().append(modelMessage.str(), SourceLocation{})
.append(SMTEncoder::callStackMessage(_callStack))
.append(move(secondaryLocation))
);
}
else
m_errorReporter.warning(6084_error, _location, message.str(), secondaryLocation);
m_errorReporter.warning(
_errorHappens,
_location,
message.str(),
SecondarySourceLocation().append(modelMessage.str(), SourceLocation{})
.append(SMTEncoder::callStackMessage(_callStack))
.append(move(secondaryLocation))
);
break;
}
case smtutil::CheckResult::UNSATISFIABLE:

21
test/libsolidity/smtCheckerTests/bmc_coverage/assert_in_constructor.sol Normal file
View File

@ -0,0 +1,21 @@
pragma experimental SMTChecker;
contract C {
uint x = initX();
function initX() internal pure returns (uint) {
return 42;
}
}
contract D is C {
uint y;
constructor() {
assert(x == 42);
y = x;
}
}
// ====
// SMTEngine: bmc
// ----

19
test/libsolidity/smtCheckerTests/bmc_coverage/implicit_constructor_with_function_calls.sol Normal file
View File

@ -0,0 +1,19 @@
pragma experimental SMTChecker;
contract C {
uint x = initX();
uint y = initY();
function initX() internal pure returns (uint) {
return 42;
}
function initY() internal view returns (uint) {
assert(x == 42);
return x;
}
}
// ====
// SMTEngine: bmc
// ----
// Warning 4661: (205-220): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/bmc_coverage/math.sol
View File

@ -22,4 +22,4 @@ contract C {
// Warning 4144: (217-222): BMC: Underflow (resulting value less than 0) happens here.
// Warning 2661: (293-298): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 3046: (369-374): BMC: Division by zero happens here.
// Warning 6084: (68-73): BMC: Underflow (resulting value less than 0) happens here.
// Warning 4144: (68-73): BMC: Underflow (resulting value less than 0) happens here.