From b4771f2a1c8413f85894004b7472a167938ec377 Mon Sep 17 00:00:00 2001 From: chriseth Date: Wed, 21 Oct 2020 19:03:51 +0200 Subject: [PATCH 01/18] Clarify evaluation of arguments to require. --- docs/control-structures.rst | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/docs/control-structures.rst b/docs/control-structures.rst index 41b704665..836584a95 100644 --- a/docs/control-structures.rst +++ b/docs/control-structures.rst @@ -615,7 +615,13 @@ The following example shows how to use an error string together with ``revert`` } } -The two syntax options are equivalent, it's developer preference which to use. +If you provide the reason string directly, then the two syntax options are equivalent, it is the developer's preference which one to use. + +.. note:: + The ``require`` function is evaluated just as any other function. + This means that all arguments are evaluated before the function itself is executed. + In particular, in ``require(condition, f())`` the function ``f`` is executed even if + ``condition`` is true. The provided string is :ref:`abi-encoded ` as if it were a call to a function ``Error(string)``. In the above example, ``revert("Not enough Ether provided.");`` returns the following hexadecimal as error return data: From d3d77e482cbd10d5228a47f077ebe8e4c60a3d90 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 21 Oct 2020 22:04:34 +0100 Subject: [PATCH 02/18] Fix ICE on conditions with tuples of rationals --- Changelog.md | 1 + libsolidity/formal/SMTEncoder.cpp | 4 ++-- libsolidity/formal/SymbolicVariables.cpp | 22 +++++++++++++++++-- libsolidity/formal/SymbolicVariables.h | 6 +++-- .../operators/tuple_rationals_conditional.sol | 11 ++++++++++ 5 files changed, 38 insertions(+), 6 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/operators/tuple_rationals_conditional.sol diff --git a/Changelog.md b/Changelog.md index 9c5ea16ea..f602e41d6 100644 --- a/Changelog.md +++ b/Changelog.md @@ -8,6 +8,7 @@ Compiler Features: Bugfixes: * SMTChecker: Fix lack of reporting potential violations when using only the CHC engine. * SMTChecker: Fix internal error on conversion from string literal to byte. + * SMTChecker: Fix internal error when using tuples of rational literals inside the conditional operator. * Code generator: Fix missing creation dependency tracking for abstract contracts. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index efd712644..7efb78205 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -574,8 +574,8 @@ bool SMTEncoder::visit(Conditional const& _op) defineExpr(_op, smtutil::Expression::ite( expr(_op.condition()), - expr(_op.trueExpression()), - expr(_op.falseExpression()) + expr(_op.trueExpression(), _op.annotation().type), + expr(_op.falseExpression(), _op.annotation().type) )); return false; diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp index cff0efdac..2d6eaa748 100644 --- a/libsolidity/formal/SymbolicVariables.cpp +++ b/libsolidity/formal/SymbolicVariables.cpp @@ -245,7 +245,25 @@ SymbolicTupleVariable::SymbolicTupleVariable( solAssert(m_sort->kind == Kind::Tuple, ""); } -vector const& SymbolicTupleVariable::components() +smtutil::Expression SymbolicTupleVariable::currentValue(frontend::TypePointer const& _targetType) const +{ + if (!_targetType || sort() == smtSort(*_targetType)) + return SymbolicVariable::currentValue(); + + auto thisTuple = dynamic_pointer_cast(sort()); + auto otherTuple = dynamic_pointer_cast(smtSort(*_targetType)); + solAssert(thisTuple && otherTuple, ""); + solAssert(thisTuple->components.size() == otherTuple->components.size(), ""); + vector args; + for (size_t i = 0; i < thisTuple->components.size(); ++i) + args.emplace_back(component(i, type(), _targetType)); + return smtutil::Expression::tuple_constructor( + smtutil::Expression(make_shared(smtSort(*_targetType)), ""), + args + ); +} + +vector const& SymbolicTupleVariable::components() const { auto tupleSort = dynamic_pointer_cast(m_sort); solAssert(tupleSort, ""); @@ -256,7 +274,7 @@ smtutil::Expression SymbolicTupleVariable::component( size_t _index, TypePointer _fromType, TypePointer _toType -) +) const { optional conversion = symbolicTypeConversion(_fromType, _toType); if (conversion) diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h index 843043c9d..d81f770a5 100644 --- a/libsolidity/formal/SymbolicVariables.h +++ b/libsolidity/formal/SymbolicVariables.h @@ -225,12 +225,14 @@ public: EncodingContext& _context ); - std::vector const& components(); + smtutil::Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override; + + std::vector const& components() const; smtutil::Expression component( size_t _index, TypePointer _fromType = nullptr, TypePointer _toType = nullptr - ); + ) const; }; /** diff --git a/test/libsolidity/smtCheckerTests/operators/tuple_rationals_conditional.sol b/test/libsolidity/smtCheckerTests/operators/tuple_rationals_conditional.sol new file mode 100644 index 000000000..cdcff3f4f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/tuple_rationals_conditional.sol @@ -0,0 +1,11 @@ +pragma experimental SMTChecker; + +contract C { + function f(bool x) public pure { + (uint a, uint b) = x ? (10000000001, 2) : (3, 4); + assert(a != 0); + assert(b != 0); + assert(a % 2 == 1); + assert(b % 2 == 0); + } +} From 4755cfe157d0b077a895e292a370b434c4bb43ca Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Fri, 23 Oct 2020 11:44:04 +0100 Subject: [PATCH 03/18] Fix assignment to contract member access --- Changelog.md | 1 + libsolidity/formal/SMTEncoder.cpp | 57 +++++++++++++++---- libsolidity/formal/SMTEncoder.h | 6 +- .../assignment_contract_member_variable.sol | 30 ++++++++++ ...ignment_contract_member_variable_array.sol | 14 +++++ ...gnment_module_contract_member_variable.sol | 31 ++++++++++ 6 files changed, 127 insertions(+), 12 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/assignment_module_contract_member_variable.sol diff --git a/Changelog.md b/Changelog.md index f602e41d6..6f32ca053 100644 --- a/Changelog.md +++ b/Changelog.md @@ -9,6 +9,7 @@ Bugfixes: * SMTChecker: Fix lack of reporting potential violations when using only the CHC engine. * SMTChecker: Fix internal error on conversion from string literal to byte. * SMTChecker: Fix internal error when using tuples of rational literals inside the conditional operator. + * SMTChecker: Fix internal error when assigning state variable via contract's name. * Code generator: Fix missing creation dependency tracking for abstract contracts. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 7efb78205..d6019eeea 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -1061,10 +1061,9 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess) auto const& exprType = _memberAccess.expression().annotation().type; solAssert(exprType, ""); - auto identifier = dynamic_cast(&_memberAccess.expression()); if (exprType->category() == Type::Category::Magic) { - if (identifier) + if (auto const* identifier = dynamic_cast(&_memberAccess.expression())) { auto const& name = identifier->name(); solAssert(name == "block" || name == "msg" || name == "tx", ""); @@ -1109,13 +1108,23 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess) } else if (exprType->category() == Type::Category::TypeType) { - if (identifier && dynamic_cast(identifier->annotation().referencedDeclaration)) + auto const* decl = expressionToDeclaration(_memberAccess.expression()); + if (dynamic_cast(decl)) { auto enumType = dynamic_cast(accessType); solAssert(enumType, ""); defineExpr(_memberAccess, enumType->memberValue(_memberAccess.memberName())); + + return false; + } + else if (dynamic_cast(decl)) + { + if (auto const* var = dynamic_cast(_memberAccess.annotation().referencedDeclaration)) + { + defineExpr(_memberAccess, currentValue(*var)); + return false; + } } - return false; } else if (exprType->category() == Type::Category::Address) { @@ -1245,6 +1254,23 @@ void SMTEncoder::arrayAssignment() void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide) { + if (auto const* memberAccess = dynamic_cast(&_expr)) + { + if (dynamic_cast(expressionToDeclaration(memberAccess->expression()))) + { + if (auto const* var = dynamic_cast(memberAccess->annotation().referencedDeclaration)) + { + if (var->hasReferenceOrMappingType()) + resetReferences(*var); + + m_context.addAssertion(m_context.newValue(*var) == _rightHandSide); + m_context.expression(_expr)->increaseIndex(); + defineExpr(_expr, currentValue(*var)); + return; + } + } + } + auto toStore = _rightHandSide; auto const* lastExpr = &_expr; while (true) @@ -1306,7 +1332,7 @@ void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expre m_context.addAssertion(m_context.newValue(*varDecl) == toStore); m_context.expression(*id)->increaseIndex(); - defineExpr(*id,currentValue(*varDecl)); + defineExpr(*id, currentValue(*varDecl)); break; } else @@ -2287,16 +2313,25 @@ set SMTEncoder::touchedVariables(ASTNode const& _nod return m_variableUsage.touchedVariables(_node, callStack); } +Declaration const* SMTEncoder::expressionToDeclaration(Expression const& _expr) +{ + if (auto const* identifier = dynamic_cast(&_expr)) + return identifier->annotation().referencedDeclaration; + if (auto const* outerMemberAccess = dynamic_cast(&_expr)) + return outerMemberAccess->annotation().referencedDeclaration; + return nullptr; +} + VariableDeclaration const* SMTEncoder::identifierToVariable(Expression const& _expr) { - if (auto identifier = dynamic_cast(&_expr)) - { - if (auto decl = dynamic_cast(identifier->annotation().referencedDeclaration)) + // We do not use `expressionToDeclaration` here because we are not interested in + // struct.field, for example. + if (auto const* identifier = dynamic_cast(&_expr)) + if (auto const* varDecl = dynamic_cast(identifier->annotation().referencedDeclaration)) { - solAssert(m_context.knownVariable(*decl), ""); - return decl; + solAssert(m_context.knownVariable(*varDecl), ""); + return varDecl; } - } return nullptr; } diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index fb563412f..748dcc80b 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -280,7 +280,11 @@ protected: /// @returns variables that are touched in _node's subtree. std::set touchedVariables(ASTNode const& _node); - /// @returns the VariableDeclaration referenced by an Identifier or nullptr. + /// @returns the declaration referenced by _expr, if any, + /// and nullptr otherwise. + Declaration const* expressionToDeclaration(Expression const& _expr); + + /// @returns the VariableDeclaration referenced by an Expression or nullptr. VariableDeclaration const* identifierToVariable(Expression const& _expr); /// Creates symbolic expressions for the returned values diff --git a/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol b/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol new file mode 100644 index 000000000..68b05367f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol @@ -0,0 +1,30 @@ +pragma experimental SMTChecker; +contract A { + int x; + int y; + function a() public { + require(A.x < 100); + A.y = A.x++; + assert(A.y == A.x - 1); + // Fails + assert(A.y == 0); + A.y = ++A.x; + assert(A.y == A.x); + delete A.x; + assert(A.x == 0); + A.y = A.x--; + assert(A.y == A.x + 1); + assert(A.y == 0); + A.y = --A.x; + assert(A.y == A.x); + A.x += 10; + // Fails + assert(A.y == 0); + assert(A.y + 10 == A.x); + A.x -= 10; + assert(A.y == A.x); + } +} +// ---- +// Warning 6328: (160-176): CHC: Assertion violation happens here. +// Warning 6328: (373-389): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array.sol b/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array.sol new file mode 100644 index 000000000..124be3f7a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; +contract A { + uint[] a; + function f() public { + A.a.push(2); + assert(A.a[A.a.length - 1] == 2); + A.a.pop(); + // Fails + assert(A.a.length > 0); + assert(A.a.length == 0); + } +} +// ---- +// Warning 6328: (156-178): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/assignment_module_contract_member_variable.sol b/test/libsolidity/smtCheckerTests/operators/assignment_module_contract_member_variable.sol new file mode 100644 index 000000000..3f5243105 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/assignment_module_contract_member_variable.sol @@ -0,0 +1,31 @@ +==== Source: AASource ==== +pragma experimental SMTChecker; +import "AASource" as AA; +contract A { + int x; + int y; + function a() public { + require(A.x < 100); + AA.A.y = A.x++; + assert(A.y == AA.A.x - 1); + // Fails + assert(AA.A.y == 0); + A.y = ++AA.A.x; + assert(A.y == A.x); + delete AA.A.x; + assert(A.x == 0); + A.y = A.x--; + assert(AA.A.y == AA.A.x + 1); + A.y = --A.x; + assert(A.y == A.x); + AA.A.x += 10; + // Fails + assert(A.y == 0); + assert(A.y + 10 == A.x); + A.x -= 10; + assert(AA.A.y == A.x); + } +} +// ---- +// Warning 6328: (AASource:191-210): CHC: Assertion violation happens here. +// Warning 6328: (AASource:402-418): CHC: Assertion violation happens here. From 72b052eae7752828534e18bb47bb553fcb391c32 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Sat, 17 Oct 2020 19:38:54 +0100 Subject: [PATCH 04/18] Convert z3::expr to smtutil::Expression --- libsmtutil/SolverInterface.h | 16 ++++- libsmtutil/Z3Interface.cpp | 112 +++++++++++++++++++++++++++++++++++ libsmtutil/Z3Interface.h | 3 + 3 files changed, 129 insertions(+), 2 deletions(-) diff --git a/libsmtutil/SolverInterface.h b/libsmtutil/SolverInterface.h index 314039260..8ea0c5250 100644 --- a/libsmtutil/SolverInterface.h +++ b/libsmtutil/SolverInterface.h @@ -60,6 +60,8 @@ class Expression public: explicit Expression(bool _v): Expression(_v ? "true" : "false", Kind::Bool) {} explicit Expression(std::shared_ptr _sort, std::string _name = ""): Expression(std::move(_name), {}, _sort) {} + explicit Expression(std::string _name, std::vector _arguments, SortPointer _sort): + name(std::move(_name)), arguments(std::move(_arguments)), sort(std::move(_sort)) {} Expression(size_t _number): Expression(std::to_string(_number), {}, SortProvider::sintSort) {} Expression(u256 const& _number): Expression(_number.str(), {}, SortProvider::sintSort) {} Expression(s256 const& _number): Expression(_number.str(), {}, SortProvider::sintSort) {} @@ -233,14 +235,26 @@ public: friend Expression operator!(Expression _a) { + if (_a.sort->kind == Kind::BitVector) + return ~_a; return Expression("not", std::move(_a), Kind::Bool); } friend Expression operator&&(Expression _a, Expression _b) { + if (_a.sort->kind == Kind::BitVector) + { + smtAssert(_b.sort->kind == Kind::BitVector, ""); + return _a & _b; + } return Expression("and", std::move(_a), std::move(_b), Kind::Bool); } friend Expression operator||(Expression _a, Expression _b) { + if (_a.sort->kind == Kind::BitVector) + { + smtAssert(_b.sort->kind == Kind::BitVector, ""); + return _a | _b; + } return Expression("or", std::move(_a), std::move(_b), Kind::Bool); } friend Expression operator==(Expression _a, Expression _b) @@ -344,8 +358,6 @@ public: private: /// Manual constructors, should only be used by SolverInterface and this class itself. - Expression(std::string _name, std::vector _arguments, SortPointer _sort): - name(std::move(_name)), arguments(std::move(_arguments)), sort(std::move(_sort)) {} Expression(std::string _name, std::vector _arguments, Kind _kind): Expression(std::move(_name), std::move(_arguments), std::make_shared(_kind)) {} diff --git a/libsmtutil/Z3Interface.cpp b/libsmtutil/Z3Interface.cpp index 89d378fe1..cfef7db72 100644 --- a/libsmtutil/Z3Interface.cpp +++ b/libsmtutil/Z3Interface.cpp @@ -18,10 +18,14 @@ #include +#include #include +#include + using namespace std; using namespace solidity::smtutil; +using namespace solidity::util; Z3Interface::Z3Interface(): m_solver(m_context) @@ -243,6 +247,82 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr) smtAssert(false, ""); } +Expression Z3Interface::fromZ3Expr(z3::expr const& _expr) +{ + auto sort = fromZ3Sort(_expr.get_sort()); + if (_expr.is_const() || _expr.is_var()) + return Expression(_expr.to_string(), {}, sort); + + smtAssert(_expr.is_app(), ""); + vector arguments; + for (unsigned i = 0; i < _expr.num_args(); ++i) + arguments.push_back(fromZ3Expr(_expr.arg(i))); + + auto kind = _expr.decl().decl_kind(); + if (_expr.is_ite()) + return Expression::ite(arguments[0], arguments[1], arguments[2]); + else if (_expr.is_not()) + return !arguments[0]; + else if (_expr.is_and()) + return arguments[0] && arguments[1]; + else if (_expr.is_or()) + return arguments[0] || arguments[1]; + else if (_expr.is_implies()) + return Expression::implies(arguments[0], arguments[1]); + else if (_expr.is_eq()) + return arguments[0] == arguments[1]; + else if (kind == Z3_OP_ULT || kind == Z3_OP_SLT) + return arguments[0] < arguments[1]; + else if (kind == Z3_OP_ULEQ || kind == Z3_OP_SLEQ) + return arguments[0] <= arguments[1]; + else if (kind == Z3_OP_GT || kind == Z3_OP_SGT) + return arguments[0] > arguments[1]; + else if (kind == Z3_OP_UGEQ || kind == Z3_OP_SGEQ) + return arguments[0] >= arguments[1]; + else if (kind == Z3_OP_ADD) + return arguments[0] + arguments[1]; + else if (kind == Z3_OP_SUB) + return arguments[0] - arguments[1]; + else if (kind == Z3_OP_MUL) + return arguments[0] * arguments[1]; + else if (kind == Z3_OP_DIV) + return arguments[0] / arguments[1]; + else if (kind == Z3_OP_MOD) + return arguments[0] % arguments[1]; + else if (kind == Z3_OP_XOR) + return arguments[0] ^ arguments[1]; + else if (kind == Z3_OP_BSHL) + return arguments[0] << arguments[1]; + else if (kind == Z3_OP_BLSHR) + return arguments[0] >> arguments[1]; + else if (kind == Z3_OP_BASHR) + return Expression::ashr(arguments[0], arguments[1]); + else if (kind == Z3_OP_INT2BV) + smtAssert(false, ""); + else if (kind == Z3_OP_BV2INT) + smtAssert(false, ""); + else if (kind == Z3_OP_SELECT) + return Expression::select(arguments[0], arguments[1]); + else if (kind == Z3_OP_STORE) + return Expression::store(arguments[0], arguments[1], arguments[2]); + else if (kind == Z3_OP_CONST_ARRAY) + { + auto sortSort = make_shared(fromZ3Sort(_expr.get_sort())); + return Expression::const_array(Expression(sortSort), arguments[0]); + } + else if (kind == Z3_OP_DT_CONSTRUCTOR) + { + auto sortSort = make_shared(fromZ3Sort(_expr.get_sort())); + return Expression::tuple_constructor(Expression(sortSort), arguments); + } + else if (kind == Z3_OP_DT_ACCESSOR) + smtAssert(false, ""); + else if (kind == Z3_OP_UNINTERPRETED) + return Expression(_expr.decl().name().str(), arguments, fromZ3Sort(_expr.get_sort())); + + smtAssert(false, ""); +} + z3::sort Z3Interface::z3Sort(Sort const& _sort) { switch (_sort.kind) @@ -295,3 +375,35 @@ z3::sort_vector Z3Interface::z3Sort(vector const& _sorts) z3Sorts.push_back(z3Sort(*_sort)); return z3Sorts; } + +SortPointer Z3Interface::fromZ3Sort(z3::sort const& _sort) +{ + if (_sort.is_bool()) + return SortProvider::boolSort; + if (_sort.is_int()) + return SortProvider::sintSort; + if (_sort.is_bv()) + return make_shared(_sort.bv_size()); + if (_sort.is_array()) + return make_shared(fromZ3Sort(_sort.array_domain()), fromZ3Sort(_sort.array_range())); + if (_sort.is_datatype()) + { + auto name = _sort.name().str(); + auto constructor = z3::func_decl(m_context, Z3_get_tuple_sort_mk_decl(m_context, _sort)); + vector memberNames; + vector memberSorts; + for (unsigned i = 0; i < constructor.arity(); ++i) + { + auto accessor = z3::func_decl(m_context, Z3_get_tuple_sort_field_decl(m_context, _sort, i)); + memberNames.push_back(accessor.name().str()); + memberSorts.push_back(fromZ3Sort(accessor.range())); + } + return make_shared(name, memberNames, memberSorts); + } + smtAssert(false, ""); +} + +vector Z3Interface::fromZ3Sort(z3::sort_vector const& _sorts) +{ + return applyMap(_sorts, [this](auto const& sort) { return fromZ3Sort(sort); }); +} diff --git a/libsmtutil/Z3Interface.h b/libsmtutil/Z3Interface.h index a44bfafcd..487723416 100644 --- a/libsmtutil/Z3Interface.h +++ b/libsmtutil/Z3Interface.h @@ -41,6 +41,7 @@ public: std::pair> check(std::vector const& _expressionsToEvaluate) override; z3::expr toZ3Expr(Expression const& _expr); + smtutil::Expression fromZ3Expr(z3::expr const& _expr); std::map constants() const { return m_constants; } std::map functions() const { return m_functions; } @@ -56,6 +57,8 @@ private: z3::sort z3Sort(Sort const& _sort); z3::sort_vector z3Sort(std::vector const& _sorts); + smtutil::SortPointer fromZ3Sort(z3::sort const& _sort); + std::vector fromZ3Sort(z3::sort_vector const& _sorts); z3::context m_context; z3::solver m_solver; From 446e46fe06e9945f9de53fd07b7293aa2dbccfb4 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 19 Oct 2020 12:21:05 +0100 Subject: [PATCH 05/18] Use Expression instead of plain strings for counterexamples --- libsmtutil/CHCSolverInterface.h | 4 +- libsmtutil/Z3CHCInterface.cpp | 4 +- libsolidity/formal/CHC.cpp | 21 ++++++--- libsolidity/formal/CHC.h | 7 ++- libsolidity/formal/Predicate.cpp | 79 ++++++++++++++++++++++++-------- libsolidity/formal/Predicate.h | 14 ++++-- 6 files changed, 92 insertions(+), 37 deletions(-) diff --git a/libsmtutil/CHCSolverInterface.h b/libsmtutil/CHCSolverInterface.h index 1fe279a8b..c088f3d0f 100644 --- a/libsmtutil/CHCSolverInterface.h +++ b/libsmtutil/CHCSolverInterface.h @@ -44,9 +44,7 @@ public: /// Needs to bound all vars as universally quantified. virtual void addRule(Expression const& _expr, std::string const& _name) = 0; - /// first: predicate name - /// second: predicate arguments - using CexNode = std::pair>; + using CexNode = Expression; struct CexGraph { std::map nodes; diff --git a/libsmtutil/Z3CHCInterface.cpp b/libsmtutil/Z3CHCInterface.cpp index 35b3556d9..e2b933b68 100644 --- a/libsmtutil/Z3CHCInterface.cpp +++ b/libsmtutil/Z3CHCInterface.cpp @@ -161,7 +161,7 @@ CHCSolverInterface::CexGraph Z3CHCInterface::cexGraph(z3::expr const& _proof) proofStack.push(_proof.arg(0)); auto const& root = proofStack.top(); - graph.nodes[root.id()] = {name(fact(root)), arguments(fact(root))}; + graph.nodes.emplace(root.id(), m_z3Interface->fromZ3Expr(fact(root))); set visited; visited.insert(root.id()); @@ -186,7 +186,7 @@ CHCSolverInterface::CexGraph Z3CHCInterface::cexGraph(z3::expr const& _proof) if (!graph.nodes.count(child.id())) { - graph.nodes[child.id()] = {name(fact(child)), arguments(fact(child))}; + graph.nodes.emplace(child.id(), m_z3Interface->fromZ3Expr(fact(child))); graph.edges[child.id()] = {}; } diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 7bedc8a65..e10785093 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -1306,7 +1306,7 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& { optional rootId; for (auto const& [id, node]: _graph.nodes) - if (node.first == _root) + if (node.name == _root) { rootId = id; break; @@ -1330,18 +1330,18 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& if (edges.size() == 2) { interfaceId = edges.at(1); - if (!Predicate::predicate(_graph.nodes.at(summaryId).first)->isSummary()) + if (!Predicate::predicate(_graph.nodes.at(summaryId).name)->isSummary()) swap(summaryId, *interfaceId); - auto interfacePredicate = Predicate::predicate(_graph.nodes.at(*interfaceId).first); + auto interfacePredicate = Predicate::predicate(_graph.nodes.at(*interfaceId).name); solAssert(interfacePredicate && interfacePredicate->isInterface(), ""); } /// The children are unordered, so we need to check which is the summary and /// which is the interface. - Predicate const* summaryPredicate = Predicate::predicate(_graph.nodes.at(summaryId).first); + Predicate const* summaryPredicate = Predicate::predicate(_graph.nodes.at(summaryId).name); solAssert(summaryPredicate && summaryPredicate->isSummary(), ""); /// At this point property 2 from the function description is verified for this node. - auto summaryArgs = _graph.nodes.at(summaryId).second; + vector summaryArgs = _graph.nodes.at(summaryId).arguments; FunctionDefinition const* calledFun = summaryPredicate->programFunction(); ContractDefinition const* calledContract = summaryPredicate->programContract(); @@ -1387,7 +1387,7 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& /// or stop. if (interfaceId) { - Predicate const* interfacePredicate = Predicate::predicate(_graph.nodes.at(*interfaceId).first); + Predicate const* interfacePredicate = Predicate::predicate(_graph.nodes.at(*interfaceId).name); solAssert(interfacePredicate && interfacePredicate->isInterface(), ""); node = *interfaceId; } @@ -1403,7 +1403,14 @@ string CHC::cex2dot(CHCSolverInterface::CexGraph const& _cex) string dot = "digraph {\n"; auto pred = [&](CHCSolverInterface::CexNode const& _node) { - return "\"" + _node.first + "(" + boost::algorithm::join(_node.second, ", ") + ")\""; + vector args = applyMap( + _node.arguments, + [&](auto const& arg) { + solAssert(arg.arguments.empty(), ""); + return arg.name; + } + ); + return "\"" + _node.name + "(" + boost::algorithm::join(args, ", ") + ")\""; }; for (auto const& [u, vs]: _cex.edges) diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 0bae37084..8d801ccb8 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -203,7 +203,7 @@ private: /// @returns a set of pairs _var = _value separated by _separator. template - std::string formatVariableModel(std::vector const& _variables, std::vector const& _values, std::string const& _separator) const + std::string formatVariableModel(std::vector const& _variables, std::vector> const& _values, std::string const& _separator) const { solAssert(_variables.size() == _values.size(), ""); @@ -212,7 +212,10 @@ private: { auto var = _variables.at(i); if (var && var->type()->isValueType()) - assignments.emplace_back(var->name() + " = " + _values.at(i)); + { + solAssert(_values.at(i), ""); + assignments.emplace_back(var->name() + " = " + *_values.at(i)); + } } return boost::algorithm::join(assignments, _separator); diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp index b1fa9b19d..d3deaa141 100644 --- a/libsolidity/formal/Predicate.cpp +++ b/libsolidity/formal/Predicate.cpp @@ -149,7 +149,7 @@ bool Predicate::isInterface() const return functor().name.rfind("interface", 0) == 0; } -string Predicate::formatSummaryCall(vector const& _args) const +string Predicate::formatSummaryCall(vector const& _args) const { if (programContract()) return "constructor()"; @@ -163,18 +163,22 @@ string Predicate::formatSummaryCall(vector const& _args) const /// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockChainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars). /// Here we are interested in preInputVars. - vector::const_iterator first = _args.begin() + 5 + static_cast(stateVars->size()); - vector::const_iterator last = first + static_cast(fun->parameters().size()); + auto first = _args.begin() + 5 + static_cast(stateVars->size()); + auto last = first + static_cast(fun->parameters().size()); solAssert(first >= _args.begin() && first <= _args.end(), ""); solAssert(last >= _args.begin() && last <= _args.end(), ""); - vector functionArgsCex(first, last); + auto inTypes = FunctionType(*fun).parameterTypes(); + vector> functionArgsCex = formatExpressions(vector(first, last), inTypes); vector functionArgs; auto const& params = fun->parameters(); solAssert(params.size() == functionArgsCex.size(), ""); for (unsigned i = 0; i < params.size(); ++i) if (params[i]->type()->isValueType()) - functionArgs.emplace_back(functionArgsCex[i]); + { + solAssert(functionArgsCex.at(i), ""); + functionArgs.emplace_back(*functionArgsCex.at(i)); + } else functionArgs.emplace_back(params[i]->name()); @@ -186,7 +190,7 @@ string Predicate::formatSummaryCall(vector const& _args) const } -vector Predicate::summaryStateValues(vector const& _args) const +vector> Predicate::summaryStateValues(vector const& _args) const { /// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars). /// The signature of an implicit constructor summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, postBlockchainState, postStateVars). @@ -194,8 +198,8 @@ vector Predicate::summaryStateValues(vector const& _args) const auto stateVars = stateVariables(); solAssert(stateVars.has_value(), ""); - vector::const_iterator stateFirst; - vector::const_iterator stateLast; + vector::const_iterator stateFirst; + vector::const_iterator stateLast; if (auto const* function = programFunction()) { stateFirst = _args.begin() + 5 + static_cast(stateVars->size()) + static_cast(function->parameters().size()) + 1; @@ -212,12 +216,13 @@ vector Predicate::summaryStateValues(vector const& _args) const solAssert(stateFirst >= _args.begin() && stateFirst <= _args.end(), ""); solAssert(stateLast >= _args.begin() && stateLast <= _args.end(), ""); - vector stateArgs(stateFirst, stateLast); + vector stateArgs(stateFirst, stateLast); solAssert(stateArgs.size() == stateVars->size(), ""); - return stateArgs; + auto stateTypes = applyMap(*stateVars, [&](auto const& _var) { return _var->type(); }); + return formatExpressions(stateArgs, stateTypes); } -vector Predicate::summaryPostInputValues(vector const& _args) const +vector> Predicate::summaryPostInputValues(vector const& _args) const { /// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars). /// Here we are interested in postInputVars. @@ -229,18 +234,19 @@ vector Predicate::summaryPostInputValues(vector const& _args) co auto const& inParams = function->parameters(); - vector::const_iterator first = _args.begin() + 5 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()) + 1; - vector::const_iterator last = first + static_cast(inParams.size()); + auto first = _args.begin() + 5 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()) + 1; + auto last = first + static_cast(inParams.size()); solAssert(first >= _args.begin() && first <= _args.end(), ""); solAssert(last >= _args.begin() && last <= _args.end(), ""); - vector inValues(first, last); + vector inValues(first, last); solAssert(inValues.size() == inParams.size(), ""); - return inValues; + auto inTypes = FunctionType(*function).parameterTypes(); + return formatExpressions(inValues, inTypes); } -vector Predicate::summaryPostOutputValues(vector const& _args) const +vector> Predicate::summaryPostOutputValues(vector const& _args) const { /// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars). /// Here we are interested in outputVars. @@ -252,11 +258,46 @@ vector Predicate::summaryPostOutputValues(vector const& _args) c auto const& inParams = function->parameters(); - vector::const_iterator first = _args.begin() + 5 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()) * 2 + 1; + auto first = _args.begin() + 5 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()) * 2 + 1; solAssert(first >= _args.begin() && first <= _args.end(), ""); - vector outValues(first, _args.end()); + vector outValues(first, _args.end()); solAssert(outValues.size() == function->returnParameters().size(), ""); - return outValues; + auto outTypes = FunctionType(*function).returnParameterTypes(); + return formatExpressions(outValues, outTypes); +} + +vector> Predicate::formatExpressions(vector const& _exprs, vector const& _types) const +{ + solAssert(_exprs.size() == _types.size(), ""); + vector> strExprs; + for (unsigned i = 0; i < _exprs.size(); ++i) + strExprs.push_back(expressionToString(_exprs.at(i), _types.at(i))); + return strExprs; +} + +optional Predicate::expressionToString(smtutil::Expression const& _expr, TypePointer _type) const +{ + if (smt::isNumber(*_type)) + { + solAssert(_expr.sort->kind == Kind::Int, ""); + solAssert(_expr.arguments.empty(), ""); + // TODO assert that _expr.name is a number. + return _expr.name; + } + if (smt::isBool(*_type)) + { + solAssert(_expr.sort->kind == Kind::Bool, ""); + solAssert(_expr.arguments.empty(), ""); + solAssert(_expr.name == "true" || _expr.name == "false", ""); + return _expr.name; + } + if (smt::isFunction(*_type)) + { + solAssert(_expr.arguments.empty(), ""); + return _expr.name; + } + + return {}; } diff --git a/libsolidity/formal/Predicate.h b/libsolidity/formal/Predicate.h index a87e81afa..9a05c3008 100644 --- a/libsolidity/formal/Predicate.h +++ b/libsolidity/formal/Predicate.h @@ -107,21 +107,27 @@ public: /// @returns a formatted string representing a call to this predicate /// with _args. - std::string formatSummaryCall(std::vector const& _args) const; + std::string formatSummaryCall(std::vector const& _args) const; /// @returns the values of the state variables from _args at the point /// where this summary was reached. - std::vector summaryStateValues(std::vector const& _args) const; + std::vector> summaryStateValues(std::vector const& _args) const; /// @returns the values of the function input variables from _args at the point /// where this summary was reached. - std::vector summaryPostInputValues(std::vector const& _args) const; + std::vector> summaryPostInputValues(std::vector const& _args) const; /// @returns the values of the function output variables from _args at the point /// where this summary was reached. - std::vector summaryPostOutputValues(std::vector const& _args) const; + std::vector> summaryPostOutputValues(std::vector const& _args) const; private: + /// @returns the formatted version of the given SMT expressions. Those expressions must be SMT constants. + std::vector> formatExpressions(std::vector const& _exprs, std::vector const& _types) const; + + /// @returns a string representation of the SMT expression based on a Solidity type. + std::optional expressionToString(smtutil::Expression const& _expr, TypePointer _type) const; + /// The actual SMT expression. smt::SymbolicFunctionVariable m_predicate; From f2f84a7f97ed0bc429eb52858b3731949f181f90 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 19 Oct 2020 16:13:21 +0100 Subject: [PATCH 06/18] Format array cex --- libsolidity/formal/CHC.h | 5 +-- libsolidity/formal/Predicate.cpp | 67 ++++++++++++++++++++++++++++++-- libsolidity/formal/Predicate.h | 6 +++ 3 files changed, 70 insertions(+), 8 deletions(-) diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 8d801ccb8..f82b2f64f 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -211,11 +211,8 @@ private: for (unsigned i = 0; i < _values.size(); ++i) { auto var = _variables.at(i); - if (var && var->type()->isValueType()) - { - solAssert(_values.at(i), ""); + if (var && _values.at(i)) assignments.emplace_back(var->name() + " = " + *_values.at(i)); - } } return boost::algorithm::join(assignments, _separator); diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp index d3deaa141..352a69b61 100644 --- a/libsolidity/formal/Predicate.cpp +++ b/libsolidity/formal/Predicate.cpp @@ -174,11 +174,8 @@ string Predicate::formatSummaryCall(vector const& _args) co auto const& params = fun->parameters(); solAssert(params.size() == functionArgsCex.size(), ""); for (unsigned i = 0; i < params.size(); ++i) - if (params[i]->type()->isValueType()) - { - solAssert(functionArgsCex.at(i), ""); + if (params.at(i) && functionArgsCex.at(i)) functionArgs.emplace_back(*functionArgsCex.at(i)); - } else functionArgs.emplace_back(params[i]->name()); @@ -298,6 +295,68 @@ optional Predicate::expressionToString(smtutil::Expression const& _expr, solAssert(_expr.arguments.empty(), ""); return _expr.name; } + if (smt::isArray(*_type)) + { + auto const& arrayType = dynamic_cast(*_type); + solAssert(_expr.name == "tuple_constructor", ""); + auto const& tupleSort = dynamic_cast(*_expr.sort); + solAssert(tupleSort.components.size() == 2, ""); + try + { + vector array(stoul(_expr.arguments.at(1).name)); + if (!fillArray(_expr.arguments.at(0), array, arrayType)) + return {}; + return "[" + boost::algorithm::join(array, ", ") + "]"; + } + catch (bad_alloc const&) + { + // Solver gave a concrete array but length is too large. + } + } return {}; } + +bool Predicate::fillArray(smtutil::Expression const& _expr, vector& _array, ArrayType const& _type) const +{ + // Base case + if (_expr.name == "const_array") + { + auto length = _array.size(); + optional elemStr = expressionToString(_expr.arguments.at(1), _type.baseType()); + if (!elemStr) + return false; + _array.clear(); + _array.resize(length, *elemStr); + return true; + } + + // Recursive case. + if (_expr.name == "store") + { + if (!fillArray(_expr.arguments.at(0), _array, _type)) + return false; + optional indexStr = expressionToString(_expr.arguments.at(1), TypeProvider::uint256()); + if (!indexStr) + return false; + // Sometimes the solver assigns huge lengths that are not related, + // we should catch and ignore those. + unsigned index; + try + { + index = stoul(*indexStr); + } + catch (out_of_range const&) + { + return true; + } + optional elemStr = expressionToString(_expr.arguments.at(2), _type.baseType()); + if (!elemStr) + return false; + if (index < _array.size()) + _array.at(index) = *elemStr; + return true; + } + + solAssert(false, ""); +} diff --git a/libsolidity/formal/Predicate.h b/libsolidity/formal/Predicate.h index 9a05c3008..3be3d4927 100644 --- a/libsolidity/formal/Predicate.h +++ b/libsolidity/formal/Predicate.h @@ -128,6 +128,12 @@ private: /// @returns a string representation of the SMT expression based on a Solidity type. std::optional expressionToString(smtutil::Expression const& _expr, TypePointer _type) const; + /// Recursively fills _array from _expr. + /// _expr should have the form `store(store(...(const_array(x_0), i_0, e_0), i_m, e_m), i_k, e_k)`. + /// @returns true if the construction worked, + /// and false if at least one element could not be built. + bool fillArray(smtutil::Expression const& _expr, std::vector& _array, ArrayType const& _type) const; + /// The actual SMT expression. smt::SymbolicFunctionVariable m_predicate; From 6d79a8885f2de38de9d830dd39d8cce40aa1ffcf Mon Sep 17 00:00:00 2001 From: Alex Beregszaszi Date: Tue, 27 Oct 2020 17:09:30 +0000 Subject: [PATCH 07/18] [ewasm] Implement stop() in EVM->Ewasm translator --- libyul/backends/wasm/EVMToEwasmTranslator.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/libyul/backends/wasm/EVMToEwasmTranslator.cpp b/libyul/backends/wasm/EVMToEwasmTranslator.cpp index 4f9b0ed08..c92cd6652 100644 --- a/libyul/backends/wasm/EVMToEwasmTranslator.cpp +++ b/libyul/backends/wasm/EVMToEwasmTranslator.cpp @@ -1211,6 +1211,9 @@ function revert(x1, x2, x3, x4, y1, y2, y3, y4) { function invalid() { unreachable() } +function stop() { + eth.finish(0:i32, 0:i32) +} function memoryguard(x:i64) -> y1, y2, y3, y4 { y4 := x } From 13652bd4a9c95223162bf4a7f924bd1434ec99ca Mon Sep 17 00:00:00 2001 From: Alex Beregszaszi Date: Tue, 27 Oct 2020 17:43:27 +0000 Subject: [PATCH 08/18] [ewasm] Add assertion for datasize/dataoffset in BinaryTransform --- libyul/backends/wasm/BinaryTransform.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/libyul/backends/wasm/BinaryTransform.cpp b/libyul/backends/wasm/BinaryTransform.cpp index 148ed2786..6c19b19f5 100644 --- a/libyul/backends/wasm/BinaryTransform.cpp +++ b/libyul/backends/wasm/BinaryTransform.cpp @@ -356,11 +356,15 @@ bytes BinaryTransform::operator()(BuiltinCall const& _call) if (_call.functionName == "dataoffset") { string name = get(_call.arguments.at(0)).value; + // TODO: support the case where name refers to the current object + yulAssert(m_subModulePosAndSize.count(name), ""); return toBytes(Opcode::I64Const) + lebEncodeSigned(static_cast(m_subModulePosAndSize.at(name).first)); } else if (_call.functionName == "datasize") { string name = get(_call.arguments.at(0)).value; + // TODO: support the case where name refers to the current object + yulAssert(m_subModulePosAndSize.count(name), ""); return toBytes(Opcode::I64Const) + lebEncodeSigned(static_cast(m_subModulePosAndSize.at(name).second)); } From 9cc37c3fa4480ae02a1d5d08755749442deae32f Mon Sep 17 00:00:00 2001 From: Djordje Mijovic Date: Wed, 28 Oct 2020 09:25:14 +0100 Subject: [PATCH 09/18] [SMTChecker] Fix ICE when using >>> --- libsolidity/formal/SMTEncoder.cpp | 3 ++- .../smtCheckerTests/operators/shifts/shr_unused.sol | 10 ++++++++++ 2 files changed, 12 insertions(+), 1 deletion(-) create mode 100644 test/libsolidity/smtCheckerTests/operators/shifts/shr_unused.sol diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 7efb78205..75c18f87b 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -1627,7 +1627,8 @@ smtutil::Expression SMTEncoder::bitwiseOperation( result = bvLeft << bvRight; break; case Token::SHR: - solAssert(false, ""); + result = bvLeft >> bvRight; + break; case Token::SAR: result = isSigned ? smtutil::Expression::ashr(bvLeft, bvRight) : diff --git a/test/libsolidity/smtCheckerTests/operators/shifts/shr_unused.sol b/test/libsolidity/smtCheckerTests/operators/shifts/shr_unused.sol new file mode 100644 index 000000000..d9e78865f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/shifts/shr_unused.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; + +contract C { + function f() public pure { + fixed x; + assert(x >>> 6 == 0); + } +} +// ---- +// UnimplementedFeatureError: Not yet implemented - FixedPointType. From 28f92064b9c5cdaa710b6dec0cb32fdc5f4550f0 Mon Sep 17 00:00:00 2001 From: Djordje Mijovic Date: Wed, 28 Oct 2020 09:02:06 +0100 Subject: [PATCH 10/18] [Sol->Yul] Fixing ice when copying struct that contains nested array to storage --- libsolidity/codegen/YulUtilFunctions.cpp | 2 +- .../array_nested_calldata_to_storage.sol | 41 +++++++++++++++---- ...ta_struct_with_nested_array_to_storage.sol | 20 +++++++++ 3 files changed, 55 insertions(+), 8 deletions(-) create mode 100644 test/libsolidity/semanticTests/structs/calldata/calldata_struct_with_nested_array_to_storage.sol diff --git a/libsolidity/codegen/YulUtilFunctions.cpp b/libsolidity/codegen/YulUtilFunctions.cpp index a4bd0a0aa..051b4bf99 100644 --- a/libsolidity/codegen/YulUtilFunctions.cpp +++ b/libsolidity/codegen/YulUtilFunctions.cpp @@ -2220,7 +2220,7 @@ string YulUtilFunctions::updateStorageValueFunction( structMembers[i].type->stackItems().size() )); t("dynamicallyEncodedMember", structMembers[i].type->isDynamicallyEncoded()); - if (structMembers[i].type->isDynamicallySized()) + if (structMembers[i].type->isDynamicallyEncoded()) t("accessCalldataTail", accessCalldataTailFunction(*structMembers[i].type)); } t("isValueType", structMembers[i].type->isValueType()); diff --git a/test/libsolidity/semanticTests/array/copying/array_nested_calldata_to_storage.sol b/test/libsolidity/semanticTests/array/copying/array_nested_calldata_to_storage.sol index 5421eb7a0..279237836 100644 --- a/test/libsolidity/semanticTests/array/copying/array_nested_calldata_to_storage.sol +++ b/test/libsolidity/semanticTests/array/copying/array_nested_calldata_to_storage.sol @@ -1,16 +1,43 @@ pragma experimental ABIEncoderV2; contract c { - uint256[][] a; + uint256[][] a1; + uint256[][2] a2; + uint256[2][] a3; + uint256[2][2] a4; - function test(uint256[][] calldata d) external returns (uint256, uint256) { - a = d; - assert(a[0][0] == d[0][0]); - assert(a[0][1] == d[0][1]); - return (a.length, a[1][0] + a[1][1]); + function test1(uint256[][] calldata c) external returns (uint256, uint256) { + a1 = c; + assert(a1[0][0] == c[0][0]); + assert(a1[0][1] == c[0][1]); + return (a1.length, a1[1][0] + a1[1][1]); + } + + function test2(uint256[][2] calldata c) external returns (uint256, uint256) { + a2 = c; + assert(a2[0][0] == c[0][0]); + assert(a2[0][1] == c[0][1]); + return (a2[0].length, a2[1][0] + a2[1][1]); + } + + function test3(uint256[2][] calldata c) external returns (uint256, uint256) { + a3 = c; + assert(a3[0][0] == c[0][0]); + assert(a3[0][1] == c[0][1]); + return (a3.length, a3[1][0] + a3[1][1]); + } + + function test4(uint256[2][2] calldata c) external returns (uint256) { + a4 = c; + assert(a4[0][0] == c[0][0]); + assert(a4[0][1] == c[0][1]); + return (a4[1][0] + a4[1][1]); } } // ==== // compileViaYul: true // ---- -// test(uint256[][]): 0x20, 2, 0x40, 0x40, 2, 23, 42 -> 2, 65 +// test1(uint256[][]): 0x20, 2, 0x40, 0x40, 2, 23, 42 -> 2, 65 +// test2(uint256[][2]): 0x20, 0x40, 0x40, 2, 23, 42 -> 2, 65 +// test3(uint256[2][]): 0x20, 2, 0x40, 0x40, 23, 42 -> 2, 65 +// test4(uint256[2][2]): 23, 42, 23, 42 -> 65 diff --git a/test/libsolidity/semanticTests/structs/calldata/calldata_struct_with_nested_array_to_storage.sol b/test/libsolidity/semanticTests/structs/calldata/calldata_struct_with_nested_array_to_storage.sol new file mode 100644 index 000000000..5e4c35e7f --- /dev/null +++ b/test/libsolidity/semanticTests/structs/calldata/calldata_struct_with_nested_array_to_storage.sol @@ -0,0 +1,20 @@ +pragma experimental ABIEncoderV2; + +contract C { + struct S { + uint128 p1; + uint256[][2] a; + uint32 p2; + } + S s; + function f(uint32 p1, S calldata c) external returns(uint32, uint128, uint256, uint256, uint32) { + s = c; + assert(s.a[0][0] == c.a[0][0]); + assert(s.a[1][1] == c.a[1][1]); + return (p1, s.p1, s.a[0][0], s.a[1][1], s.p2); + } +} +// ==== +// compileViaYul: true +// ---- +// f(uint32, (uint128, uint256[][2], uint32)): 55, 0x40, 77, 0x60, 88, 0x40, 0x40, 2, 1, 2 -> 55, 77, 1, 2, 88 From e5faea5f350815caba4b846e969b950ea644b23a Mon Sep 17 00:00:00 2001 From: Alex Beregszaszi Date: Wed, 28 Oct 2020 09:59:35 +0000 Subject: [PATCH 11/18] Make use of pushInstruction() helper in libevmasm --- libevmasm/Assembly.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/libevmasm/Assembly.cpp b/libevmasm/Assembly.cpp index c729a4eb4..d899b8ff7 100644 --- a/libevmasm/Assembly.cpp +++ b/libevmasm/Assembly.cpp @@ -580,14 +580,14 @@ LinkerObject const& Assembly::assemble() const multimap subRef; vector sizeRef; ///< Pointers to code locations where the size of the program is inserted unsigned bytesPerTag = util::bytesRequired(bytesRequiredForCode); - uint8_t tagPush = (uint8_t)Instruction::PUSH1 - 1 + bytesPerTag; + uint8_t tagPush = (uint8_t)pushInstruction(bytesPerTag); unsigned bytesRequiredIncludingData = bytesRequiredForCode + 1 + m_auxiliaryData.size(); for (auto const& sub: m_subs) bytesRequiredIncludingData += sub->assemble().bytecode.size(); unsigned bytesPerDataRef = util::bytesRequired(bytesRequiredIncludingData); - uint8_t dataRefPush = (uint8_t)Instruction::PUSH1 - 1 + bytesPerDataRef; + uint8_t dataRefPush = (uint8_t)pushInstruction(bytesPerDataRef); ret.bytecode.reserve(bytesRequiredIncludingData); for (AssemblyItem const& i: m_items) @@ -617,7 +617,7 @@ LinkerObject const& Assembly::assemble() const case Push: { uint8_t b = max(1, util::bytesRequired(i.data())); - ret.bytecode.push_back((uint8_t)Instruction::PUSH1 - 1 + b); + ret.bytecode.push_back((uint8_t)pushInstruction(b)); ret.bytecode.resize(ret.bytecode.size() + b); bytesRef byr(&ret.bytecode.back() + 1 - b, b); toBigEndian(i.data(), byr); @@ -647,7 +647,7 @@ LinkerObject const& Assembly::assemble() const auto s = subAssemblyById(static_cast(i.data()))->assemble().bytecode.size(); i.setPushedValue(u256(s)); uint8_t b = max(1, util::bytesRequired(s)); - ret.bytecode.push_back((uint8_t)Instruction::PUSH1 - 1 + b); + ret.bytecode.push_back((uint8_t)pushInstruction(b)); ret.bytecode.resize(ret.bytecode.size() + b); bytesRef byr(&ret.bytecode.back() + 1 - b, b); toBigEndian(s, byr); @@ -677,7 +677,7 @@ LinkerObject const& Assembly::assemble() const ret.bytecode.push_back(uint8_t(Instruction::DUP1)); // TODO: should we make use of the constant optimizer methods for pushing the offsets? bytes offsetBytes = toCompactBigEndian(u256(offset)); - ret.bytecode.push_back(uint8_t(Instruction::PUSH1) - 1 + offsetBytes.size()); + ret.bytecode.push_back(uint8_t(pushInstruction(offsetBytes.size()))); ret.bytecode += offsetBytes; ret.bytecode.push_back(uint8_t(Instruction::MSTORE)); } From 25f75ce547b1a639abd0da8a2621cd5ec7923cec Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 27 Oct 2020 17:48:12 +0000 Subject: [PATCH 12/18] Remove nondet tests --- libsolidity/formal/Predicate.cpp | 10 +++++++++- .../operators/compound_bitwise_or_uint_2.sol | 6 ++---- .../types/array_static_mapping_aliasing_2.sol | 5 +++-- 3 files changed, 14 insertions(+), 7 deletions(-) diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp index 352a69b61..8d1eba1b4 100644 --- a/libsolidity/formal/Predicate.cpp +++ b/libsolidity/formal/Predicate.cpp @@ -301,9 +301,17 @@ optional Predicate::expressionToString(smtutil::Expression const& _expr, solAssert(_expr.name == "tuple_constructor", ""); auto const& tupleSort = dynamic_cast(*_expr.sort); solAssert(tupleSort.components.size() == 2, ""); + + auto length = stoul(_expr.arguments.at(1).name); + // Limit this counterexample size to 1k. + // Some OSs give you "unlimited" memory through swap and other virtual memory, + // so purely relying on bad_alloc being thrown is not a good idea. + // In that case, the array allocation might cause OOM and the program is killed. + if (length >= 1024) + return {}; try { - vector array(stoul(_expr.arguments.at(1).name)); + vector array(length); if (!fillArray(_expr.arguments.at(0), array, arrayType)) return {}; return "[" + boost::algorithm::join(array, ", ") + "]"; diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol index 6e62d8148..b27b468a9 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol @@ -7,9 +7,7 @@ contract C { function f(bool b) public { if (b) s.x[2] |= 1; - assert(s.x[2] != 1); + // Removed because of Spacer nondeterminism. + //assert(s.x[2] != 1); } } -// ---- -// Warning 6328: (173-192): CHC: Assertion violation might happen here. -// Warning 7812: (173-192): BMC: Assertion violation might happen here. diff --git a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol index f27c21fb4..94dee80ee 100644 --- a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol +++ b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol @@ -17,7 +17,8 @@ contract C // Should not fail since knowledge is erased only for mapping (uint => uint). assert(severalMaps8[0][0] == 42); // Should not fail since singleMap == severalMaps3d[0][0] is not possible. - assert(severalMaps3d[0][0][0] == 42); + // Removed because of Spacer nondeterminism. + //assert(severalMaps3d[0][0][0] == 42); // Should fail since singleMap == map is possible. assert(map[0] == 42); } @@ -26,4 +27,4 @@ contract C } } // ---- -// Warning 6328: (781-801): CHC: Assertion violation happens here. +// Warning 6328: (830-850): CHC: Assertion violation happens here. From 24d8c2ed9036f4583e83ece941b215763a026d62 Mon Sep 17 00:00:00 2001 From: Alex Beregszaszi Date: Fri, 3 Jul 2020 13:27:32 +0100 Subject: [PATCH 13/18] Split error codes for EVM opcodes --- libyul/AsmAnalysis.cpp | 17 ++++++++--------- .../evm_byzantium_on_homestead.sol | 2 +- .../evm_constantinople_on_byzantium.sol | 4 ++-- 3 files changed, 11 insertions(+), 12 deletions(-) diff --git a/libyul/AsmAnalysis.cpp b/libyul/AsmAnalysis.cpp index bf968d950..631d0881c 100644 --- a/libyul/AsmAnalysis.cpp +++ b/libyul/AsmAnalysis.cpp @@ -635,19 +635,18 @@ bool AsmAnalyzer::validateInstructions(evmasm::Instruction _instr, SourceLocatio ); }; - if (( - _instr == evmasm::Instruction::RETURNDATACOPY || - _instr == evmasm::Instruction::RETURNDATASIZE - ) && !m_evmVersion.supportsReturndata()) + if (_instr == evmasm::Instruction::RETURNDATACOPY && !m_evmVersion.supportsReturndata()) errorForVM(7756_error, "only available for Byzantium-compatible"); + else if (_instr == evmasm::Instruction::RETURNDATASIZE && !m_evmVersion.supportsReturndata()) + errorForVM(4778_error, "only available for Byzantium-compatible"); else if (_instr == evmasm::Instruction::STATICCALL && !m_evmVersion.hasStaticCall()) errorForVM(1503_error, "only available for Byzantium-compatible"); - else if (( - _instr == evmasm::Instruction::SHL || - _instr == evmasm::Instruction::SHR || - _instr == evmasm::Instruction::SAR - ) && !m_evmVersion.hasBitwiseShifting()) + else if (_instr == evmasm::Instruction::SHL && !m_evmVersion.hasBitwiseShifting()) errorForVM(6612_error, "only available for Constantinople-compatible"); + else if (_instr == evmasm::Instruction::SHR && !m_evmVersion.hasBitwiseShifting()) + errorForVM(7458_error, "only available for Constantinople-compatible"); + else if (_instr == evmasm::Instruction::SAR && !m_evmVersion.hasBitwiseShifting()) + errorForVM(2054_error, "only available for Constantinople-compatible"); else if (_instr == evmasm::Instruction::CREATE2 && !m_evmVersion.hasCreate2()) errorForVM(6166_error, "only available for Constantinople-compatible"); else if (_instr == evmasm::Instruction::EXTCODEHASH && !m_evmVersion.hasExtCodeHash()) diff --git a/test/libsolidity/syntaxTests/inlineAssembly/evm_byzantium_on_homestead.sol b/test/libsolidity/syntaxTests/inlineAssembly/evm_byzantium_on_homestead.sol index bbb32299f..4c6525116 100644 --- a/test/libsolidity/syntaxTests/inlineAssembly/evm_byzantium_on_homestead.sol +++ b/test/libsolidity/syntaxTests/inlineAssembly/evm_byzantium_on_homestead.sol @@ -14,7 +14,7 @@ contract C { // ==== // EVMVersion: =homestead // ---- -// TypeError 7756: (86-100): The "returndatasize" instruction is only available for Byzantium-compatible VMs (you are currently compiling for "homestead"). +// TypeError 4778: (86-100): The "returndatasize" instruction is only available for Byzantium-compatible VMs (you are currently compiling for "homestead"). // DeclarationError 3812: (77-102): Variable count mismatch: 1 variables and 0 values. // TypeError 7756: (115-129): The "returndatacopy" instruction is only available for Byzantium-compatible VMs (you are currently compiling for "homestead"). // TypeError 1503: (245-255): The "staticcall" instruction is only available for Byzantium-compatible VMs (you are currently compiling for "homestead"). diff --git a/test/libsolidity/syntaxTests/inlineAssembly/evm_constantinople_on_byzantium.sol b/test/libsolidity/syntaxTests/inlineAssembly/evm_constantinople_on_byzantium.sol index 1e6d85bf1..95f25c384 100644 --- a/test/libsolidity/syntaxTests/inlineAssembly/evm_constantinople_on_byzantium.sol +++ b/test/libsolidity/syntaxTests/inlineAssembly/evm_constantinople_on_byzantium.sol @@ -17,9 +17,9 @@ contract C { // ---- // TypeError 6612: (103-106): The "shl" instruction is only available for Constantinople-compatible VMs (you are currently compiling for "byzantium"). // DeclarationError 8678: (96-116): Variable count does not match number of values (1 vs. 0) -// TypeError 6612: (136-139): The "shr" instruction is only available for Constantinople-compatible VMs (you are currently compiling for "byzantium"). +// TypeError 7458: (136-139): The "shr" instruction is only available for Constantinople-compatible VMs (you are currently compiling for "byzantium"). // DeclarationError 8678: (129-147): Variable count does not match number of values (1 vs. 0) -// TypeError 6612: (167-170): The "sar" instruction is only available for Constantinople-compatible VMs (you are currently compiling for "byzantium"). +// TypeError 2054: (167-170): The "sar" instruction is only available for Constantinople-compatible VMs (you are currently compiling for "byzantium"). // DeclarationError 8678: (160-178): Variable count does not match number of values (1 vs. 0) // TypeError 6166: (283-290): The "create2" instruction is only available for Constantinople-compatible VMs (you are currently compiling for "byzantium"). // DeclarationError 8678: (276-302): Variable count does not match number of values (1 vs. 0) From 62028c90f04e3628c67e4efc1bd09d32368a774c Mon Sep 17 00:00:00 2001 From: Alex Beregszaszi Date: Tue, 27 Oct 2020 19:26:00 +0000 Subject: [PATCH 14/18] [ewasm] Overhaul memory handling in EwasmInterpreter Introduce writeMemory and read/writeBytes32/Address helpers. Fix read/writeU128/U256 to be little-endian. Update each instruction to follow the specification. --- test/libyul/ewasmTranslationTests/balance.yul | 6 ++--- .../ewasmTranslationTests/callvalue.yul | 4 ++-- .../ewasmTranslationTests/difficulty.yul | 4 ++-- .../ewasmTranslationTests/extcodesize.yul | 4 ++-- .../libyul/ewasmTranslationTests/gasprice.yul | 4 ++-- .../EwasmBuiltinInterpreter.cpp | 24 ++++++++++++------- .../yulInterpreter/EwasmBuiltinInterpreter.h | 18 ++++++++++---- 7 files changed, 40 insertions(+), 24 deletions(-) diff --git a/test/libyul/ewasmTranslationTests/balance.yul b/test/libyul/ewasmTranslationTests/balance.yul index f8bb5017a..e9adc3470 100644 --- a/test/libyul/ewasmTranslationTests/balance.yul +++ b/test/libyul/ewasmTranslationTests/balance.yul @@ -6,7 +6,7 @@ // Trace: // Memory dump: // 0: 0000000000000000000000000000000000000000000000000000000000000001 -// 20: 0000000000000000000000000000000000000000000000000000000022222222 +// 20: 0000000000000000000000000000000022222222000000000000000000000000 // Storage dump: -// 0000000000000000000000000000000000000000000000000000000000000000: 0000000000000000000000000000000000000000000000000000000022222222 -// 0000000000000000000000000000000000000000000000000000000000000001: 0000000000000000000000000000000000000000000000000000000022222222 +// 0000000000000000000000000000000000000000000000000000000000000000: 0000000000000000000000000000000022222222000000000000000000000000 +// 0000000000000000000000000000000000000000000000000000000000000001: 0000000000000000000000000000000022222222000000000000000000000000 diff --git a/test/libyul/ewasmTranslationTests/callvalue.yul b/test/libyul/ewasmTranslationTests/callvalue.yul index cf9104f7a..99bfa0f31 100644 --- a/test/libyul/ewasmTranslationTests/callvalue.yul +++ b/test/libyul/ewasmTranslationTests/callvalue.yul @@ -4,6 +4,6 @@ // ---- // Trace: // Memory dump: -// 20: 0000000000000000000000005555555500000000000000000000000000000000 +// 20: 5555555500000000000000000000000000000000000000000000000000000000 // Storage dump: -// 0000000000000000000000000000000000000000000000000000000000000000: 0000000000000000000000005555555500000000000000000000000000000000 +// 0000000000000000000000000000000000000000000000000000000000000000: 5555555500000000000000000000000000000000000000000000000000000000 diff --git a/test/libyul/ewasmTranslationTests/difficulty.yul b/test/libyul/ewasmTranslationTests/difficulty.yul index c467d51a7..fe706155d 100644 --- a/test/libyul/ewasmTranslationTests/difficulty.yul +++ b/test/libyul/ewasmTranslationTests/difficulty.yul @@ -4,6 +4,6 @@ // ---- // Trace: // Memory dump: -// 20: 0000000000000000000000000000000000000000000000000000000009999999 +// 20: 9999990900000000000000000000000000000000000000000000000000000000 // Storage dump: -// 0000000000000000000000000000000000000000000000000000000000000000: 0000000000000000000000000000000000000000000000000000000009999999 +// 0000000000000000000000000000000000000000000000000000000000000000: 9999990900000000000000000000000000000000000000000000000000000000 diff --git a/test/libyul/ewasmTranslationTests/extcodesize.yul b/test/libyul/ewasmTranslationTests/extcodesize.yul index fb12db5ea..99df58cbc 100644 --- a/test/libyul/ewasmTranslationTests/extcodesize.yul +++ b/test/libyul/ewasmTranslationTests/extcodesize.yul @@ -4,6 +4,6 @@ // ---- // Trace: // Memory dump: -// 20: 000000000000000000000000000000000000000000000000000000000000077b +// 20: 0000000000000000000000000000000000000000000000000000000000000dd6 // Storage dump: -// 0000000000000000000000000000000000000000000000000000000000000000: 000000000000000000000000000000000000000000000000000000000000077b +// 0000000000000000000000000000000000000000000000000000000000000000: 0000000000000000000000000000000000000000000000000000000000000dd6 diff --git a/test/libyul/ewasmTranslationTests/gasprice.yul b/test/libyul/ewasmTranslationTests/gasprice.yul index 97334e442..1d668fa6f 100644 --- a/test/libyul/ewasmTranslationTests/gasprice.yul +++ b/test/libyul/ewasmTranslationTests/gasprice.yul @@ -4,6 +4,6 @@ // ---- // Trace: // Memory dump: -// 20: 0000000000000000000000006666666600000000000000000000000000000000 +// 20: 6666666600000000000000000000000000000000000000000000000000000000 // Storage dump: -// 0000000000000000000000000000000000000000000000000000000000000000: 0000000000000000000000006666666600000000000000000000000000000000 +// 0000000000000000000000000000000000000000000000000000000000000000: 6666666600000000000000000000000000000000000000000000000000000000 diff --git a/test/tools/yulInterpreter/EwasmBuiltinInterpreter.cpp b/test/tools/yulInterpreter/EwasmBuiltinInterpreter.cpp index 3ec9a84a7..bf0c01491 100644 --- a/test/tools/yulInterpreter/EwasmBuiltinInterpreter.cpp +++ b/test/tools/yulInterpreter/EwasmBuiltinInterpreter.cpp @@ -35,6 +35,7 @@ using namespace solidity; using namespace solidity::yul; using namespace solidity::yul::test; +using solidity::util::h160; using solidity::util::h256; namespace @@ -309,7 +310,7 @@ u256 EwasmBuiltinInterpreter::evalEthBuiltin(string const& _fun, vector>= 8; } } @@ -553,9 +559,9 @@ void EwasmBuiltinInterpreter::writeU256(uint64_t _offset, u256 _value, size_t _c u256 EwasmBuiltinInterpreter::readU256(uint64_t _offset, size_t _croppedTo) { accessMemory(_offset, _croppedTo); - u256 value; + u256 value{0}; for (size_t i = 0; i < _croppedTo; i++) - value = (value << 8) | m_state.memory[_offset + i]; + value = (value << 8) | m_state.memory[_offset + _croppedTo - 1 - i]; return value; } diff --git a/test/tools/yulInterpreter/EwasmBuiltinInterpreter.h b/test/tools/yulInterpreter/EwasmBuiltinInterpreter.h index 5a855932d..44037a083 100644 --- a/test/tools/yulInterpreter/EwasmBuiltinInterpreter.h +++ b/test/tools/yulInterpreter/EwasmBuiltinInterpreter.h @@ -24,6 +24,7 @@ #include #include +#include #include @@ -61,6 +62,8 @@ struct InterpreterState; * * The main focus is that the generated execution trace is the same for equivalent executions * and likely to be different for non-equivalent executions. + * + * The type names are following the Ewasm specification (https://github.com/ewasm/design/blob/master/eth_interface.md). */ class EwasmBuiltinInterpreter { @@ -99,6 +102,9 @@ private: /// @returns the memory contents (4 bytes) at the provided address (little-endian). /// Does not adjust msize, use @a accessMemory for that uint32_t readMemoryHalfWord(uint64_t _offset); + /// Writes bytes to memory. + /// Does not adjust msize, use @a accessMemory for that + void writeMemory(uint64_t _offset, bytes const& _value); /// Writes a word to memory (little-endian) /// Does not adjust msize, use @a accessMemory for that void writeMemoryWord(uint64_t _offset, uint64_t _value); @@ -109,14 +115,18 @@ private: /// Does not adjust msize, use @a accessMemory for that void writeMemoryByte(uint64_t _offset, uint8_t _value); - /// Helper for eth.* builtins. Writes to memory (big-endian) and always returns zero. + /// Helper for eth.* builtins. Writes to memory (little-endian) and always returns zero. void writeU256(uint64_t _offset, u256 _value, size_t _croppedTo = 32); void writeU128(uint64_t _offset, u256 _value) { writeU256(_offset, std::move(_value), 16); } - void writeAddress(uint64_t _offset, u256 _value) { writeU256(_offset, std::move(_value), 20); } - /// Helper for eth.* builtins. Reads from memory (big-endian) and returns the value; + /// Helper for eth.* builtins. Writes to memory (as a byte string). + void writeBytes32(uint64_t _offset, util::h256 _value) { accessMemory(_offset, 32); writeMemory(_offset, _value.asBytes()); } + void writeAddress(uint64_t _offset, util::h160 _value) { accessMemory(_offset, 20); writeMemory(_offset, _value.asBytes()); } + /// Helper for eth.* builtins. Reads from memory (little-endian) and returns the value. u256 readU256(uint64_t _offset, size_t _croppedTo = 32); u256 readU128(uint64_t _offset) { return readU256(_offset, 16); } - u256 readAddress(uint64_t _offset) { return readU256(_offset, 20); } + /// Helper for eth.* builtins. Reads from memory (as a byte string). + util::h256 readBytes32(uint64_t _offset) { accessMemory(_offset, 32); return util::h256(readMemory(_offset, 32)); } + util::h160 readAddress(uint64_t _offset) { accessMemory(_offset, 20); return util::h160(readMemory(_offset, 20)); } void logTrace(evmasm::Instruction _instruction, std::vector const& _arguments = {}, bytes const& _data = {}); /// Appends a log to the trace representing an instruction or similar operation by string, From 9dc5ceae94999318a8a14d15d744c349bf8001be Mon Sep 17 00:00:00 2001 From: Alex Beregszaszi Date: Tue, 27 Oct 2020 20:13:12 +0000 Subject: [PATCH 15/18] [ewasm] Implement "create" properly in EwasmInterpreter --- test/tools/yulInterpreter/EwasmBuiltinInterpreter.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/test/tools/yulInterpreter/EwasmBuiltinInterpreter.cpp b/test/tools/yulInterpreter/EwasmBuiltinInterpreter.cpp index bf0c01491..39ec8ecfd 100644 --- a/test/tools/yulInterpreter/EwasmBuiltinInterpreter.cpp +++ b/test/tools/yulInterpreter/EwasmBuiltinInterpreter.cpp @@ -396,7 +396,8 @@ u256 EwasmBuiltinInterpreter::evalEthBuiltin(string const& _fun, vector Date: Tue, 27 Oct 2020 20:11:03 +0000 Subject: [PATCH 16/18] [ewasm] Properly touch memory in EwasmInterpreter --- .../EwasmBuiltinInterpreter.cpp | 39 ++++++++++++------- 1 file changed, 24 insertions(+), 15 deletions(-) diff --git a/test/tools/yulInterpreter/EwasmBuiltinInterpreter.cpp b/test/tools/yulInterpreter/EwasmBuiltinInterpreter.cpp index 39ec8ecfd..6d3f3a5f4 100644 --- a/test/tools/yulInterpreter/EwasmBuiltinInterpreter.cpp +++ b/test/tools/yulInterpreter/EwasmBuiltinInterpreter.cpp @@ -298,9 +298,7 @@ u256 EwasmBuiltinInterpreter::evalEthBuiltin(string const& _fun, vector 4) throw ExplicitlyTerminated(); + if (numberOfTopics > 0) + readBytes32(arg[3]); + if (numberOfTopics > 1) + readBytes32(arg[4]); + if (numberOfTopics > 2) + readBytes32(arg[5]); + if (numberOfTopics > 3) + readBytes32(arg[6]); logTrace(evmasm::logInstruction(numberOfTopics), {}); return 0; } @@ -473,7 +482,7 @@ u256 EwasmBuiltinInterpreter::evalEthBuiltin(string const& _fun, vector Date: Wed, 28 Oct 2020 11:45:54 +0000 Subject: [PATCH 17/18] Update SMT types docs --- docs/security-considerations.rst | 28 +++++++++++++++------------- 1 file changed, 15 insertions(+), 13 deletions(-) diff --git a/docs/security-considerations.rst b/docs/security-considerations.rst index d8e04a81f..921aac20e 100644 --- a/docs/security-considerations.rst +++ b/docs/security-considerations.rst @@ -448,19 +448,21 @@ The SMT encoding tries to be as precise as possible, mapping Solidity types and expressions to their closest `SMT-LIB `_ representation, as shown in the table below. -+-----------------------+--------------+-----------------------------+ -|Solidity type |SMT sort |Theories (quantifier-free) | -+=======================+==============+=============================+ -|Boolean |Bool |Bool | -+-----------------------+--------------+-----------------------------+ -|intN, uintN, address, |Integer |LIA, NIA | -|bytesN, enum | | | -+-----------------------+--------------+-----------------------------+ -|array, mapping, bytes, |Array |Arrays | -|string | | | -+-----------------------+--------------+-----------------------------+ -|other types |Integer |LIA | -+-----------------------+--------------+-----------------------------+ ++-----------------------+--------------------------------+-----------------------------+ +|Solidity type |SMT sort |Theories (quantifier-free) | ++=======================+================================+=============================+ +|Boolean |Bool |Bool | ++-----------------------+--------------------------------+-----------------------------+ +|intN, uintN, address, |Integer |LIA, NIA | +|bytesN, enum | | | ++-----------------------+--------------------------------+-----------------------------+ +|array, mapping, bytes, |Tuple |Datatypes, Arrays, LIA | +|string |(Array elements, Integer length)| | ++-----------------------+--------------------------------+-----------------------------+ +|struct |Tuple |Datatypes | ++-----------------------+--------------------------------+-----------------------------+ +|other types |Integer |LIA | ++-----------------------+--------------------------------+-----------------------------+ Types that are not yet supported are abstracted by a single 256-bit unsigned integer, where their unsupported operations are ignored. From b18d5ab257554bcb06d43bdbe757f38a576f9a27 Mon Sep 17 00:00:00 2001 From: chriseth Date: Wed, 28 Oct 2020 17:21:08 +0100 Subject: [PATCH 18/18] Fix move bug. --- libyul/optimiser/SSAReverser.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libyul/optimiser/SSAReverser.cpp b/libyul/optimiser/SSAReverser.cpp index decdc4ea4..e1902608d 100644 --- a/libyul/optimiser/SSAReverser.cpp +++ b/libyul/optimiser/SSAReverser.cpp @@ -73,7 +73,7 @@ void SSAReverser::operator()(Block& _block) VariableDeclaration{ std::move(varDecl->location), std::move(varDecl->variables), - std::make_unique(std::move(assignment->variableNames.front())) + std::make_unique(assignment->variableNames.front()) } ); }