Merge pull request #8916 from ethereum/smt_array_push_pop

[SMTChecker] Support array push/pop
This commit is contained in:
chriseth 2020-05-19 15:41:10 +02:00 committed by GitHub
commit 3b27b4347c
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
27 changed files with 426 additions and 22 deletions

View File

@ -6,6 +6,7 @@ Language Features:
Compiler Features:
* Build system: Update the soljson.js build to emscripten 1.39.15 and boost 1.73.0 and include Z3 for integrated SMTChecker support without the callback mechanism.
* SMTChecker: Support array ``length``.
* SMTChecker: Support array ``push`` and ``pop``.
Bugfixes:

View File

@ -657,3 +657,14 @@ Notice that we do not clear knowledge about ``array`` and ``d`` because they
are located in storage, even though they also have type ``uint[]``. However,
if ``d`` was assigned, we would need to clear knowledge about ``array`` and
vice-versa.
Real World Assumptions
======================
Some scenarios can be expressed in Solidity and the EVM, but are expected to
never occur in practice.
One of such cases is the length of a dynamic storage array overflowing during a
push: If the ``push`` operation is applied to an array of length 2^256 - 1, its
length silently overflows.
However, this is unlikely to happen in practice, since the operations required
to grow the array to that point would take billions of years to execute.

View File

@ -98,17 +98,45 @@ void CHC::analyze(SourceUnit const& _source)
for (auto const& [scope, target]: m_verificationTargets)
{
auto assertions = transactionAssertions(scope);
for (auto const* assertion: assertions)
if (target.type == VerificationTarget::Type::Assert)
{
auto assertions = transactionAssertions(scope);
for (auto const* assertion: assertions)
{
createErrorBlock();
connectBlocks(target.value, error(), target.constraints && (target.errorId == assertion->id()));
auto [result, model] = query(error(), assertion->location());
// This should be fine but it's a bug in the old compiler
(void)model;
if (result == smt::CheckResult::UNSATISFIABLE)
m_safeAssertions.insert(assertion);
}
}
else if (target.type == VerificationTarget::Type::PopEmptyArray)
{
solAssert(dynamic_cast<FunctionCall const*>(scope), "");
createErrorBlock();
connectBlocks(target.value, error(), target.constraints && (target.errorId == assertion->id()));
auto [result, model] = query(error(), assertion->location());
connectBlocks(target.value, error(), target.constraints && (target.errorId == scope->id()));
auto [result, model] = query(error(), scope->location());
// This should be fine but it's a bug in the old compiler
(void)model;
if (result == smt::CheckResult::UNSATISFIABLE)
m_safeAssertions.insert(assertion);
if (result != smt::CheckResult::UNSATISFIABLE)
{
string msg = "Empty array \"pop\" ";
if (result == smt::CheckResult::SATISFIABLE)
msg += "detected here.";
else
msg += "might happen here.";
m_unsafeTargets.insert(scope);
m_outerErrorReporter.warning(
2529_error,
scope->location(),
msg
);
}
}
else
solAssert(false, "");
}
}
@ -161,7 +189,7 @@ void CHC::endVisit(ContractDefinition const& _contract)
auto stateExprs = vector<smt::Expression>{m_error.currentValue()} + currentStateVariables();
setCurrentBlock(*m_constructorSummaryPredicate, &stateExprs);
addVerificationTarget(m_currentContract, m_currentBlock, smt::Expression(true), m_error.currentValue());
addAssertVerificationTarget(m_currentContract, m_currentBlock, smt::Expression(true), m_error.currentValue());
connectBlocks(m_currentBlock, interface(), m_error.currentValue() == 0);
SMTEncoder::endVisit(_contract);
@ -256,7 +284,7 @@ void CHC::endVisit(FunctionDefinition const& _function)
if (_function.isPublic())
{
addVerificationTarget(&_function, m_currentBlock, sum, assertionError);
addAssertVerificationTarget(&_function, m_currentBlock, sum, assertionError);
connectBlocks(m_currentBlock, iface, sum && (assertionError == 0));
}
}
@ -556,10 +584,34 @@ void CHC::unknownFunctionCall(FunctionCall const&)
m_unknownFunctionCallSeen = true;
}
void CHC::makeArrayPopVerificationTarget(FunctionCall const& _arrayPop)
{
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_arrayPop.expression().annotation().type);
solAssert(funType.kind() == FunctionType::Kind::ArrayPop, "");
auto memberAccess = dynamic_cast<MemberAccess const*>(&_arrayPop.expression());
solAssert(memberAccess, "");
auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
solAssert(symbArray, "");
auto previousError = m_error.currentValue();
m_error.increaseIndex();
addArrayPopVerificationTarget(&_arrayPop, m_error.currentValue());
connectBlocks(
m_currentBlock,
m_currentFunction->isConstructor() ? summary(*m_currentContract) : summary(*m_currentFunction),
currentPathConditions() && symbArray->length() <= 0 && m_error.currentValue() == _arrayPop.id()
);
m_context.addAssertion(m_error.currentValue() == previousError);
}
void CHC::resetSourceAnalysis()
{
m_verificationTargets.clear();
m_safeAssertions.clear();
m_unsafeTargets.clear();
m_functionAssertions.clear();
m_callGraph.clear();
m_summaries.clear();
@ -974,9 +1026,35 @@ pair<smt::CheckResult, vector<string>> CHC::query(smt::Expression const& _query,
return {result, values};
}
void CHC::addVerificationTarget(ASTNode const* _scope, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId)
void CHC::addVerificationTarget(
ASTNode const* _scope,
VerificationTarget::Type _type,
smt::Expression _from,
smt::Expression _constraints,
smt::Expression _errorId
)
{
m_verificationTargets.emplace(_scope, CHCVerificationTarget{{VerificationTarget::Type::Assert, _from, _constraints}, _errorId});
m_verificationTargets.emplace(_scope, CHCVerificationTarget{{_type, _from, _constraints}, _errorId});
}
void CHC::addAssertVerificationTarget(ASTNode const* _scope, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId)
{
addVerificationTarget(_scope, VerificationTarget::Type::Assert, _from, _constraints, _errorId);
}
void CHC::addArrayPopVerificationTarget(ASTNode const* _scope, smt::Expression _errorId)
{
solAssert(m_currentContract, "");
solAssert(m_currentFunction, "");
if (m_currentFunction->isConstructor())
addVerificationTarget(_scope, VerificationTarget::Type::PopEmptyArray, summary(*m_currentContract), smt::Expression(true), _errorId);
else
{
auto iface = (*m_interfaces.at(m_currentContract))(initialStateVariables());
auto sum = summary(*m_currentFunction);
addVerificationTarget(_scope, VerificationTarget::Type::PopEmptyArray, iface, sum, _errorId);
}
}
string CHC::uniquePrefix()

View File

@ -78,6 +78,7 @@ private:
void visitAssert(FunctionCall const& _funCall);
void internalFunctionCall(FunctionCall const& _funCall);
void unknownFunctionCall(FunctionCall const& _funCall);
void makeArrayPopVerificationTarget(FunctionCall const& _arrayPop) override;
//@}
struct IdCompare
@ -182,7 +183,9 @@ private:
/// @returns <false, model> otherwise.
std::pair<smt::CheckResult, std::vector<std::string>> query(smt::Expression const& _query, langutil::SourceLocation const& _location);
void addVerificationTarget(ASTNode const* _scope, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId);
void addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId);
void addAssertVerificationTarget(ASTNode const* _scope, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId);
void addArrayPopVerificationTarget(ASTNode const* _scope, smt::Expression _errorId);
//@}
/// Misc.
@ -245,6 +248,8 @@ private:
/// Assertions proven safe.
std::set<Expression const*> m_safeAssertions;
/// Targets proven unsafe.
std::set<ASTNode const*> m_unsafeTargets;
//@}
/// Control-flow.

View File

@ -646,6 +646,12 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
m_context.state().transfer(m_context.state().thisAddress(), expr(address), expr(*value));
break;
}
case FunctionType::Kind::ArrayPush:
arrayPush(_funCall);
break;
case FunctionType::Kind::ArrayPop:
arrayPop(_funCall);
break;
default:
m_errorReporter.warning(
4588_error,
@ -905,16 +911,6 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
m_context
);
}
else
{
auto const& name = _memberAccess.memberName();
solAssert(name == "push" || name == "pop", "");
m_errorReporter.warning(
9098_error,
_memberAccess.location(),
"Assertion checker does not yet support array member \"" + name + "\"."
);
}
return false;
}
else
@ -1082,6 +1078,76 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smt::Expression c
}
}
void SMTEncoder::arrayPush(FunctionCall const& _funCall)
{
auto memberAccess = dynamic_cast<MemberAccess const*>(&_funCall.expression());
solAssert(memberAccess, "");
auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
solAssert(symbArray, "");
auto oldLength = symbArray->length();
m_context.addAssertion(oldLength >= 0);
// Real world assumption: the array length is assumed to not overflow.
// This assertion guarantees that both the current and updated lengths have the above property.
m_context.addAssertion(oldLength + 1 < (smt::maxValue(*TypeProvider::uint256()) - 1));
auto const& arguments = _funCall.arguments();
smt::Expression element = arguments.empty() ?
smt::zeroValue(_funCall.annotation().type) :
expr(*arguments.front());
smt::Expression store = smt::Expression::store(
symbArray->elements(),
oldLength,
element
);
symbArray->increaseIndex();
m_context.addAssertion(symbArray->elements() == store);
m_context.addAssertion(symbArray->length() == oldLength + 1);
if (arguments.empty())
defineExpr(_funCall, element);
arrayPushPopAssign(memberAccess->expression(), symbArray->currentValue());
}
void SMTEncoder::arrayPop(FunctionCall const& _funCall)
{
auto memberAccess = dynamic_cast<MemberAccess const*>(&_funCall.expression());
solAssert(memberAccess, "");
auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
solAssert(symbArray, "");
makeArrayPopVerificationTarget(_funCall);
auto oldElements = symbArray->elements();
auto oldLength = symbArray->length();
m_context.addAssertion(oldLength > 0);
symbArray->increaseIndex();
m_context.addAssertion(symbArray->elements() == oldElements);
auto newLength = smt::Expression::ite(
oldLength == 0,
smt::maxValue(*TypeProvider::uint256()),
oldLength - 1
);
m_context.addAssertion(symbArray->length() == oldLength - 1);
arrayPushPopAssign(memberAccess->expression(), symbArray->currentValue());
}
void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smt::Expression const& _array)
{
if (auto const* id = dynamic_cast<Identifier const*>(&_expr))
{
auto varDecl = identifierToVariable(*id);
solAssert(varDecl, "");
m_context.addAssertion(m_context.newValue(*varDecl) == _array);
}
else if (auto const* indexAccess = dynamic_cast<IndexAccess const*>(&_expr))
arrayIndexAssignment(*indexAccess, _array);
else
solAssert(false, "");
}
void SMTEncoder::defineGlobalVariable(string const& _name, Expression const& _expr, bool _increaseIndex)
{
if (!m_context.knownGlobalSymbol(_name))

View File

@ -137,6 +137,13 @@ protected:
/// Handles assignment to SMT array index.
void arrayIndexAssignment(Expression const& _expr, smt::Expression const& _rightHandSide);
void arrayPush(FunctionCall const& _funCall);
void arrayPop(FunctionCall const& _funCall);
void arrayPushPopAssign(Expression const& _expr, smt::Expression const& _array);
/// Allows BMC and CHC to create verification targets for popping
/// an empty array.
virtual void makeArrayPopVerificationTarget(FunctionCall const&) {}
/// Division expression in the given type. Requires special treatment because
/// of rounding for signed division.
smt::Expression division(smt::Expression _left, smt::Expression _right, IntegerType const& _type);
@ -240,7 +247,7 @@ protected:
struct VerificationTarget
{
enum class Type { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert } type;
enum class Type { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert, PopEmptyArray } type;
smt::Expression value;
smt::Expression constraints;
};

View File

@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract C {
uint[] a;
function f() public {
a.push();
a.pop();
}
}

View File

@ -0,0 +1,10 @@
pragma experimental SMTChecker;
contract C {
uint[] a;
function f() public {
a.pop();
}
}
// ----
// Warning: (82-89): Empty array "pop" detected here.

View File

@ -0,0 +1,10 @@
pragma experimental SMTChecker;
contract C {
uint[][] a;
function f() public {
a.push();
a[0].push();
a[0].pop();
}
}

View File

@ -0,0 +1,12 @@
pragma experimental SMTChecker;
contract C {
uint[][] a;
function f() public {
a.push();
a[0].push();
a[1].pop();
}
}
// ----
// Warning: (111-121): Empty array "pop" detected here.

View File

@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract C {
uint[] a;
constructor() public {
a.push();
a.pop();
}
}

View File

@ -0,0 +1,10 @@
pragma experimental SMTChecker;
contract C {
uint[] a;
constructor() public {
a.pop();
}
}
// ----
// Warning: (83-90): Empty array "pop" detected here.

View File

@ -0,0 +1,11 @@
pragma experimental SMTChecker;
contract C {
uint[] a;
function f(uint l) public {
for (uint i = 0; i < l; ++i) {
a.push();
a.pop();
}
}
}

View File

@ -0,0 +1,14 @@
pragma experimental SMTChecker;
contract C {
uint[] a;
function f(uint l) public {
for (uint i = 0; i < l; ++i) {
a.push();
a.pop();
}
a.pop();
}
}
// ----
// Warning: (150-157): Empty array "pop" detected here.

View File

@ -0,0 +1,10 @@
pragma experimental SMTChecker;
contract C {
uint[][] a;
function f(uint[] memory x, uint y) public {
a.push(x);
a[0].push(y);
assert(a[0][a[0].length - 1] == y);
}
}

View File

@ -0,0 +1,14 @@
pragma experimental SMTChecker;
contract C {
uint[][] a;
function f(uint[] memory x, uint y) public {
a.push(x);
a[0].push(y);
a[0].pop();
assert(a[0][a[0].length - 1] == y);
}
}
// ----
// Warning: (162-177): Underflow (resulting value less than 0) happens here
// Warning: (150-184): Assertion violation happens here

View File

@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract C {
uint[] a;
function f(uint x) public {
a.push(x);
assert(a[a.length - 1] == x);
}
}

View File

@ -0,0 +1,10 @@
pragma experimental SMTChecker;
contract C {
uint256[] x;
constructor() public { x.push(42); }
function f() public {
x.push(23);
assert(x[0] == 42 || x[0] == 23);
}
}

View File

@ -0,0 +1,10 @@
pragma experimental SMTChecker;
contract C {
uint256[] x;
constructor() public { x.push(42); }
function f() public {
x.push(23);
assert(x[0] == 42);
}
}

View File

@ -0,0 +1,12 @@
contract C {
uint256[] x;
function f(uint256 l) public {
require(x.length == 0);
x.push(42);
x.push(84);
for(uint256 i = 0; i < l; ++i)
x.push(23);
assert(x[0] == 42 || x[0] == 23);
}
}

View File

@ -0,0 +1,13 @@
pragma experimental SMTChecker;
contract C {
uint256[] x;
function f(uint256 l) public {
require(x.length == 0);
x.push(42);
x.push(84);
for(uint256 i = 0; i < l; ++i)
x.push(23);
assert(x[0] == 42);
}
}

View File

@ -0,0 +1,16 @@
pragma experimental SMTChecker;
contract C {
uint[][] a;
function f() public {
a.push();
uint[] storage b = a[0];
b.push(8);
assert(b[b.length - 1] == 8);
// Safe but fails due to aliasing.
assert(a[0][a[0].length - 1] == 8);
}
}
// ----
// Warning: (217-232): Underflow (resulting value less than 0) happens here
// Warning: (205-239): Assertion violation happens here

View File

@ -0,0 +1,15 @@
pragma experimental SMTChecker;
contract C {
uint[][] a;
function f() public {
a.push();
a[0].push();
a[0][0] = 16;
uint[] storage b = a[0];
b[0] = 32;
assert(a[0][0] == 16);
}
}
// ----
// Warning: (167-188): Assertion violation happens here

View File

@ -0,0 +1,10 @@
pragma experimental SMTChecker;
contract C {
uint[][] a;
function f() public {
a.push();
a[0].push();
assert(a[a.length - 1][0] == 0);
}
}

View File

@ -0,0 +1,12 @@
pragma experimental SMTChecker;
contract C {
uint[][] a;
function f() public {
a.push();
a[0].push();
assert(a[a.length - 1][0] == 100);
}
}
// ----
// Warning: (111-144): Assertion violation happens here

View File

@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract C {
uint[] a;
function f() public {
a.push();
assert(a[a.length - 1] == 0);
}
}

View File

@ -0,0 +1,11 @@
pragma experimental SMTChecker;
contract C {
uint[] a;
function f() public {
a.push();
assert(a[a.length - 1] == 100);
}
}
// ----
// Warning: (94-124): Assertion violation happens here