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

[SMTChecker] Support array push/pop

Browse Source
This commit is contained in:
Leonardo Alt 2020-05-12 00:39:00 +02:00
parent 142a6b0d4f
commit 82db35e563
3 changed files with 76 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -6,6 +6,7 @@ Language Features:
Compiler 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. * 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 ``length``.
* SMTChecker: Support array ``push`` and ``pop``.
Bugfixes: Bugfixes:

81
libsolidity/formal/SMTEncoder.cpp
View File

@ -646,6 +646,12 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
m_context.state().transfer(m_context.state().thisAddress(), expr(address), expr(*value)); m_context.state().transfer(m_context.state().thisAddress(), expr(address), expr(*value));
break; break;
} }
case FunctionType::Kind::ArrayPush:
arrayPush(_funCall);
break;
case FunctionType::Kind::ArrayPop:
arrayPop(_funCall);
break;
default: default:
m_errorReporter.warning( m_errorReporter.warning(
4588_error, 4588_error,
@ -905,16 +911,6 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
m_context 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; return false;
} }
else else
@ -1082,6 +1078,71 @@ 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();
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);
auto newLength = smt::Expression::ite(
oldLength == smt::maxValue(*TypeProvider::uint256()),
0,
oldLength + 1
);
m_context.addAssertion(symbArray->length() == newLength);
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, "");
auto oldElements = symbArray->elements();
auto oldLength = symbArray->length();
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() == newLength);
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) void SMTEncoder::defineGlobalVariable(string const& _name, Expression const& _expr, bool _increaseIndex)
{ {
if (!m_context.knownGlobalSymbol(_name)) if (!m_context.knownGlobalSymbol(_name))

4
libsolidity/formal/SMTEncoder.h
View File

@ -137,6 +137,10 @@ protected:
/// Handles assignment to SMT array index. /// Handles assignment to SMT array index.
void arrayIndexAssignment(Expression const& _expr, smt::Expression const& _rightHandSide); 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);
/// Division expression in the given type. Requires special treatment because /// Division expression in the given type. Requires special treatment because
/// of rounding for signed division. /// of rounding for signed division.
smt::Expression division(smt::Expression _left, smt::Expression _right, IntegerType const& _type); smt::Expression division(smt::Expression _left, smt::Expression _right, IntegerType const& _type);