From e23d8f559370f5aa740782d22048a1d16fd6e4aa Mon Sep 17 00:00:00 2001 From: Djordje Mijovic Date: Wed, 7 Oct 2020 13:28:35 +0200 Subject: [PATCH] [SMTChecker] Supporting inline arrays. --- Changelog.md | 2 +- libsolidity/formal/SMTEncoder.cpp | 32 ++++++++++++------- libsolidity/formal/SMTEncoder.h | 5 +++ .../smtCheckerTests/types/array_literal_1.sol | 5 +-- .../smtCheckerTests/types/array_literal_2.sol | 14 ++++++++ .../smtCheckerTests/types/array_literal_3.sol | 13 ++++++++ .../smtCheckerTests/types/array_literal_4.sol | 13 ++++++++ .../smtCheckerTests/types/array_literal_5.sol | 16 ++++++++++ .../smtCheckerTests/types/array_literal_6.sol | 18 +++++++++++ .../smtCheckerTests/types/array_literal_7.sol | 23 +++++++++++++ 10 files changed, 127 insertions(+), 14 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/types/array_literal_2.sol create mode 100644 test/libsolidity/smtCheckerTests/types/array_literal_3.sol create mode 100644 test/libsolidity/smtCheckerTests/types/array_literal_4.sol create mode 100644 test/libsolidity/smtCheckerTests/types/array_literal_5.sol create mode 100644 test/libsolidity/smtCheckerTests/types/array_literal_6.sol create mode 100644 test/libsolidity/smtCheckerTests/types/array_literal_7.sol diff --git a/Changelog.md b/Changelog.md index cfc218237..6266da9a9 100644 --- a/Changelog.md +++ b/Changelog.md @@ -5,7 +5,7 @@ Language Features: Compiler Features: - + * SMTChecker: Support inline arrays. Bugfixes: * Code generator: Fix internal compiler error when referencing members via module name but not using the reference. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 118cb5308..6ecf215b8 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -391,11 +391,13 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple) createExpr(_tuple); if (_tuple.isInlineArray()) - m_errorReporter.warning( - 2177_error, - _tuple.location(), - "Assertion checker does not yet implement inline arrays." - ); + { + // Add constraints for the length and values as it is known. + auto symbArray = dynamic_pointer_cast(m_context.expression(_tuple)); + solAssert(symbArray, ""); + + addArrayLiteralAssertions(*symbArray, applyMap(_tuple.components(), [&](auto const& c) { return expr(*c); })); + } else if (_tuple.components().size() == 1) defineExpr(_tuple, expr(*_tuple.components().front())); else @@ -965,12 +967,10 @@ void SMTEncoder::endVisit(Literal const& _literal) auto symbArray = dynamic_pointer_cast(m_context.expression(_literal)); solAssert(symbArray, ""); - auto value = _literal.value(); - m_context.addAssertion(symbArray->length() == value.length()); - for (size_t i = 0; i < value.length(); i++) - m_context.addAssertion( - smtutil::Expression::select(symbArray->elements(), i) == size_t(value[i]) - ); + addArrayLiteralAssertions( + *symbArray, + applyMap(_literal.value(), [&](auto const& c) { return smtutil::Expression{size_t(c)}; }) + ); } else { @@ -984,6 +984,16 @@ void SMTEncoder::endVisit(Literal const& _literal) } } +void SMTEncoder::addArrayLiteralAssertions( + smt::SymbolicArrayVariable& _symArray, + vector const& _elementValues +) +{ + m_context.addAssertion(_symArray.length() == _elementValues.size()); + for (size_t i = 0; i < _elementValues.size(); i++) + m_context.addAssertion(smtutil::Expression::select(_symArray.elements(), i) == _elementValues[i]); +} + void SMTEncoder::endVisit(Return const& _return) { if (_return.expression() && m_context.knownExpression(*_return.expression())) diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index f15225a08..c39042fbb 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -169,6 +169,11 @@ protected: /// an empty array. virtual void makeArrayPopVerificationTarget(FunctionCall const&) {} + void addArrayLiteralAssertions( + smt::SymbolicArrayVariable& _symArray, + std::vector const& _elementValues + ); + /// Division expression in the given type. Requires special treatment because /// of rounding for signed division. smtutil::Expression division(smtutil::Expression _left, smtutil::Expression _right, IntegerType const& _type); diff --git a/test/libsolidity/smtCheckerTests/types/array_literal_1.sol b/test/libsolidity/smtCheckerTests/types/array_literal_1.sol index a72031f1d..1a6fb3b51 100644 --- a/test/libsolidity/smtCheckerTests/types/array_literal_1.sol +++ b/test/libsolidity/smtCheckerTests/types/array_literal_1.sol @@ -4,8 +4,9 @@ contract C { function f() public pure { uint[3] memory array = [uint(1), 2, 3]; + assert(array[0] == 1); + assert(array[1] == 2); + assert(array[2] == 3); } } // ---- -// Warning 2072: (76-96): Unused local variable. -// Warning 2177: (99-114): Assertion checker does not yet implement inline arrays. diff --git a/test/libsolidity/smtCheckerTests/types/array_literal_2.sol b/test/libsolidity/smtCheckerTests/types/array_literal_2.sol new file mode 100644 index 000000000..8e5915f35 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_literal_2.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public pure { + uint[3] memory a = [uint(1), 2, 3]; + uint[3] memory b = [uint(1), 2, 4]; + assert(a[0] == b[0]); + assert(a[1] == b[1]); + assert(a[2] == b[2]); // fails + } +} +// ---- +// Warning 6328: (200-220): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/array_literal_3.sol b/test/libsolidity/smtCheckerTests/types/array_literal_3.sol new file mode 100644 index 000000000..6d25027b7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_literal_3.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public pure { + (uint[3] memory a, uint[3] memory b) = ([uint(1), 2, 3], [uint(1), 2, 4]); + assert(a[0] == b[0]); + assert(a[1] == b[1]); + assert(a[2] == b[2]); // fails + } +} +// ---- +// Warning 6328: (201-221): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/array_literal_4.sol b/test/libsolidity/smtCheckerTests/types/array_literal_4.sol new file mode 100644 index 000000000..1606c43fa --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_literal_4.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(bool c) public pure { + uint[3] memory a = c ? [uint(1), 2, 3] : [uint(1), 2, 4]; + uint[3] memory b = [uint(1), 2, c ? 3 : 4]; + assert(a[0] == b[0]); + assert(a[1] == b[1]); + assert(a[2] == b[2]); + } +} +// ---- diff --git a/test/libsolidity/smtCheckerTests/types/array_literal_5.sol b/test/libsolidity/smtCheckerTests/types/array_literal_5.sol new file mode 100644 index 000000000..c0017d14a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_literal_5.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; + +contract C +{ + uint[] s; + function f() public { + uint[3] memory a = [uint(1), 2, 3]; + s = a; + assert(s.length == a.length); + assert(s[0] == a[0]); + assert(s[1] == a[1]); + assert(s[2] != a[2]); // fails + } +} +// ---- +// Warning 6328: (209-229): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/array_literal_6.sol b/test/libsolidity/smtCheckerTests/types/array_literal_6.sol new file mode 100644 index 000000000..bbcdff3dd --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_literal_6.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public pure { + uint[3] memory a = [uint(1), 2, 3]; + uint[4] memory b = [uint(1), 2, 4, 3]; + uint[4] memory c = b; + assert(a.length == c.length); // fails + assert(a[0] == c[0]); + assert(a[1] == c[1]); + assert(a[2] == c[2]); // fails + assert(a[2] == c[3]); + } +} +// ---- +// Warning 6328: (179-207): CHC: Assertion violation happens here. +// Warning 6328: (268-288): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/array_literal_7.sol b/test/libsolidity/smtCheckerTests/types/array_literal_7.sol new file mode 100644 index 000000000..964c265b0 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_literal_7.sol @@ -0,0 +1,23 @@ +pragma experimental SMTChecker; + +contract C +{ + uint[] s; + function f() public { + uint[3] memory a = [uint(1), 2, 3]; + uint[4] memory b = [uint(1), 2, 4, 3]; + uint[4] memory c = b; + assert(c.length == b.length); + s = a; + assert(s.length == a.length); + + assert(s.length == c.length); // fails + assert(s[0] == c[0]); + assert(s[1] == c[1]); + assert(s[2] == c[2]); // fails + assert(s[2] == c[3]); + } +} +// ---- +// Warning 6328: (259-287): CHC: Assertion violation happens here. +// Warning 6328: (348-368): CHC: Assertion violation happens here.