From 9f3d5d3e2f18684e033ca61f90d97660f458dfd2 Mon Sep 17 00:00:00 2001 From: Alex Beregszaszi Date: Fri, 25 Sep 2020 13:00:32 +0100 Subject: [PATCH] [SMTChecker] Implement support for memory allocation --- Changelog.md | 1 + libsolidity/formal/SMTEncoder.cpp | 22 ++++++++++++ libsolidity/formal/SMTEncoder.h | 1 + .../smtCheckerTests/operators/bytes_new.sol | 36 +++++++++++++++++++ .../smtCheckerTests/operators/integer_new.sol | 36 +++++++++++++++++++ .../types/function_type_arrays.sol | 2 +- .../array_struct_array_struct_memory_safe.sol | 2 +- ...rray_struct_array_struct_memory_unsafe.sol | 12 +++---- 8 files changed, 104 insertions(+), 8 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/operators/bytes_new.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/integer_new.sol diff --git a/Changelog.md b/Changelog.md index bb1b2c7b4..723f54a06 100644 --- a/Changelog.md +++ b/Changelog.md @@ -10,6 +10,7 @@ Compiler Features: * SMTChecker: Support ``revert()``. * SMTChecker: Support shifts. * SMTChecker: Support compound and, or, and xor operators. + * SMTChecker: Support memory allocation, e.g. ``new bytes(123)``. * SMTChecker: Support structs. * SMTChecker: Support ``type(T).min``, ``type(T).max``, and ``type(I).interfaceId``. * SMTChecker: Support ``address`` type conversion with literals, e.g. ``address(0)``. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 540c2a7dc..fd599e3db 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -663,6 +663,9 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall) case FunctionType::Kind::Event: // These can be safely ignored. break; + case FunctionType::Kind::ObjectCreation: + visitObjectCreation(_funCall); + return; default: m_errorReporter.warning( 4588_error, @@ -735,6 +738,25 @@ void SMTEncoder::visitGasLeft(FunctionCall const& _funCall) m_context.addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1)); } +void SMTEncoder::visitObjectCreation(FunctionCall const& _funCall) +{ + auto const& args = _funCall.arguments(); + solAssert(args.size() >= 1, ""); + auto argType = args.front()->annotation().type->category(); + solAssert(argType == Type::Category::Integer || argType == Type::Category::RationalNumber, ""); + + smtutil::Expression arraySize = expr(*args.front()); + setSymbolicUnknownValue(arraySize, TypeProvider::uint256(), m_context); + + auto symbArray = dynamic_pointer_cast(m_context.expression(_funCall)); + solAssert(symbArray, ""); + smt::setSymbolicZeroValue(*symbArray, m_context); + auto zeroElements = symbArray->elements(); + symbArray->increaseIndex(); + m_context.addAssertion(symbArray->length() == arraySize); + m_context.addAssertion(symbArray->elements() == zeroElements); +} + void SMTEncoder::endVisit(Identifier const& _identifier) { if (auto decl = identifierToVariable(_identifier)) diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 454f8777c..adce5439b 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -137,6 +137,7 @@ protected: void visitAssert(FunctionCall const& _funCall); void visitRequire(FunctionCall const& _funCall); void visitGasLeft(FunctionCall const& _funCall); + void visitObjectCreation(FunctionCall const& _funCall); void visitTypeConversion(FunctionCall const& _funCall); void visitFunctionIdentifier(Identifier const& _identifier); diff --git a/test/libsolidity/smtCheckerTests/operators/bytes_new.sol b/test/libsolidity/smtCheckerTests/operators/bytes_new.sol new file mode 100644 index 000000000..968a0935b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/bytes_new.sol @@ -0,0 +1,36 @@ +pragma experimental SMTChecker; + +contract C { + function f() public pure { + bytes memory x = new bytes(0); + assert(x.length == 0); + } + function g() public pure { + bytes memory x = new bytes(3); + assert(x.length == 3); + assert(x[0] == 0); + assert(x[1] == 0); + assert(x[2] == 0); + } + function h() public pure { + bytes memory x = new bytes(3); + assert(x.length == 3); + x[0] = 0x12; + x[1] = 0x34; + assert(x[0] == 0x12); + assert(x[1] == 0x34); + // This should be an out-of-bounds assertion. + x[5] = 0xff; + assert(x[5] == 0xff); + } + function h(uint size) public pure { + bytes memory x = new bytes(size); + assert(x.length == size); + require(size >= 2); + x[0] = 0x12; + x[1] = 0x34; + assert(x[0] == 0x12); + assert(x[1] == 0x34); + } +} +// ---- diff --git a/test/libsolidity/smtCheckerTests/operators/integer_new.sol b/test/libsolidity/smtCheckerTests/operators/integer_new.sol new file mode 100644 index 000000000..53db42141 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/integer_new.sol @@ -0,0 +1,36 @@ +pragma experimental SMTChecker; + +contract C { + function f() public pure { + uint[] memory x = new uint[](0); + assert(x.length == 0); + } + function g() public pure { + uint[] memory x = new uint[](3); + assert(x.length == 3); + assert(x[0] == 0); + assert(x[1] == 0); + assert(x[2] == 0); + } + function h() public pure { + uint[] memory x = new uint[](3); + assert(x.length == 3); + x[0] = 0x12; + x[1] = 0x34; + assert(x[0] == 0x12); + assert(x[1] == 0x34); + // This should be an out-of-bounds assertion. + x[5] = 0xff; + assert(x[5] == 0xff); + } + function h(uint size) public pure { + uint[] memory x = new uint[](size); + assert(x.length == size); + require(size >= 2); + x[0] = 0x12; + x[1] = 0x34; + assert(x[0] == 0x12); + assert(x[1] == 0x34); + } +} +// ---- diff --git a/test/libsolidity/smtCheckerTests/types/function_type_arrays.sol b/test/libsolidity/smtCheckerTests/types/function_type_arrays.sol index e2810721b..a0ebf4379 100644 --- a/test/libsolidity/smtCheckerTests/types/function_type_arrays.sol +++ b/test/libsolidity/smtCheckerTests/types/function_type_arrays.sol @@ -7,8 +7,8 @@ contract C { function(uint) returns (uint)[10] storage b = y; function(uint) external returns (uint)[] memory c; c = new function(uint) external returns (uint)[](200); + assert(c.length == 200); a; b; } } // ---- -// Warning 4588: (361-410): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_safe.sol b/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_safe.sol index 08cb807a2..c7524fb64 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_safe.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_safe.sol @@ -14,6 +14,7 @@ contract C { } function f() public pure { S[] memory s1 = new S[](3); + assert(s1.length == 3); s1[0].x = 2; assert(s1[0].x == 2); s1[1].t.y = 3; @@ -27,4 +28,3 @@ contract C { } } // ---- -// Warning 4588: (217-227): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_unsafe.sol b/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_unsafe.sol index 04b8a5620..f78c760b9 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_unsafe.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_unsafe.sol @@ -14,6 +14,7 @@ contract C { } function f(S memory s2) public pure { S[] memory s1 = new S[](3); + assert(s1.length == 3); s1[0].x = 2; assert(s1[0].x == s2.x); s1[1].t.y = 3; @@ -27,9 +28,8 @@ contract C { } } // ---- -// Warning 6328: (257-280): Assertion violation happens here. -// Warning 6328: (301-328): Assertion violation happens here. -// Warning 6328: (350-379): Assertion violation happens here. -// Warning 6328: (404-439): Assertion violation happens here. -// Warning 6328: (467-508): Assertion violation happens here. -// Warning 4588: (228-238): Assertion checker does not yet implement this type of function call. +// Warning 6328: (283-306): Assertion violation happens here. +// Warning 6328: (327-354): Assertion violation happens here. +// Warning 6328: (376-405): Assertion violation happens here. +// Warning 6328: (430-465): Assertion violation happens here. +// Warning 6328: (493-534): Assertion violation happens here.