From c8cc73c80c994f84563ac474a455521d38fbcc8f Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Thu, 24 Sep 2020 19:24:33 +0200 Subject: [PATCH] Support array slices --- Changelog.md | 1 + libsolidity/CMakeLists.txt | 2 + libsolidity/formal/ArraySlicePredicate.cpp | 91 +++++++++++++++++++ libsolidity/formal/ArraySlicePredicate.h | 62 +++++++++++++ libsolidity/formal/CHC.cpp | 35 +++++++ libsolidity/formal/CHC.h | 1 + libsolidity/formal/Predicate.h | 3 +- libsolidity/formal/SMTEncoder.cpp | 6 +- .../smtCheckerTests/operators/slice.sol | 12 +++ .../operators/slice_default_end.sol | 17 ++++ .../operators/slice_default_start.sol | 13 +++ .../smtCheckerTests/operators/slices_1.sol | 3 - .../special/abi_encode_slice.sol | 1 - .../typecast/slice_to_bytes.sol | 3 - 14 files changed, 237 insertions(+), 13 deletions(-) create mode 100644 libsolidity/formal/ArraySlicePredicate.cpp create mode 100644 libsolidity/formal/ArraySlicePredicate.h create mode 100644 test/libsolidity/smtCheckerTests/operators/slice.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/slice_default_end.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/slice_default_start.sol diff --git a/Changelog.md b/Changelog.md index 72f2f25e6..eb5090c2c 100644 --- a/Changelog.md +++ b/Changelog.md @@ -2,6 +2,7 @@ Compiler Features: * SMTChecker: Support ``addmod`` and ``mulmod``. + * SMTChecker: Support array slices. * Optimizer: Optimize ``exp`` when base is -1. * Code generator: Implemented events with function type as one of its indexed parameters. * General: Option to stop compilation after parsing stage. Can be used with ``solc --stop-after parsing`` diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt index a6ea34c29..2fe3c3941 100644 --- a/libsolidity/CMakeLists.txt +++ b/libsolidity/CMakeLists.txt @@ -94,6 +94,8 @@ set(sources codegen/ir/IRLValue.h codegen/ir/IRVariable.cpp codegen/ir/IRVariable.h + formal/ArraySlicePredicate.cpp + formal/ArraySlicePredicate.h formal/BMC.cpp formal/BMC.h formal/CHC.cpp diff --git a/libsolidity/formal/ArraySlicePredicate.cpp b/libsolidity/formal/ArraySlicePredicate.cpp new file mode 100644 index 000000000..85fced906 --- /dev/null +++ b/libsolidity/formal/ArraySlicePredicate.cpp @@ -0,0 +1,91 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see . +*/ +// SPDX-License-Identifier: GPL-3.0 + +#include + +#include + +using namespace std; +using namespace solidity; +using namespace solidity::smtutil; +using namespace solidity::frontend; +using namespace solidity::frontend::smt; + +map ArraySlicePredicate::m_slicePredicates; + +pair ArraySlicePredicate::create(SortPointer _sort, EncodingContext& _context) +{ + solAssert(_sort->kind == Kind::Tuple, ""); + auto tupleSort = dynamic_pointer_cast(_sort); + solAssert(tupleSort, ""); + + auto tupleName = tupleSort->name; + if (m_slicePredicates.count(tupleName)) + return {true, m_slicePredicates.at(tupleName)}; + + auto sort = tupleSort->components.at(0); + solAssert(sort->kind == Kind::Array, ""); + + smt::SymbolicArrayVariable aVar{sort, "a_" + tupleName, _context }; + smt::SymbolicArrayVariable bVar{sort, "b_" + tupleName, _context}; + smt::SymbolicIntVariable startVar{TypeProvider::uint256(), TypeProvider::uint256(), "start_" + tupleName, _context}; + smt::SymbolicIntVariable endVar{TypeProvider::uint256(), TypeProvider::uint256(), "end_" + tupleName, _context }; + smt::SymbolicIntVariable iVar{TypeProvider::uint256(), TypeProvider::uint256(), "i_" + tupleName, _context}; + + vector domain{sort, sort, startVar.sort(), endVar.sort()}; + auto sliceSort = make_shared(domain, SortProvider::boolSort); + Predicate const& slice = *Predicate::create(sliceSort, "array_slice_" + tupleName, PredicateType::Custom, _context); + + domain.emplace_back(iVar.sort()); + auto predSort = make_shared(domain, SortProvider::boolSort); + Predicate const& header = *Predicate::create(predSort, "array_slice_header_" + tupleName, PredicateType::Custom, _context); + Predicate const& loop = *Predicate::create(predSort, "array_slice_loop_" + tupleName, PredicateType::Custom, _context); + + auto a = aVar.elements(); + auto b = bVar.elements(); + auto start = startVar.currentValue(); + auto end = endVar.currentValue(); + auto i = iVar.currentValue(); + + auto rule1 = smtutil::Expression::implies( + end > start, + header({a, b, start, end, 0}) + ); + + auto rule2 = smtutil::Expression::implies( + header({a, b, start, end, i}) && i >= (end - start), + slice({a, b, start, end}) + ); + + auto rule3 = smtutil::Expression::implies( + header({a, b, start, end, i}) && i >= 0 && i < (end - start), + loop({a, b, start, end, i}) + ); + + auto b_i = smtutil::Expression::select(b, i); + auto a_start_i = smtutil::Expression::select(a, start + i); + auto rule4 = smtutil::Expression::implies( + loop({a, b, start, end, i}) && b_i == a_start_i, + header({a, b, start, end, i + 1}) + ); + + return {false, m_slicePredicates[tupleName] = { + {&slice, &header, &loop}, + {move(rule1), move(rule2), move(rule3), move(rule4)} + }}; +} diff --git a/libsolidity/formal/ArraySlicePredicate.h b/libsolidity/formal/ArraySlicePredicate.h new file mode 100644 index 000000000..180a9d189 --- /dev/null +++ b/libsolidity/formal/ArraySlicePredicate.h @@ -0,0 +1,62 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see . +*/ +// SPDX-License-Identifier: GPL-3.0 + +#include +#include +#include + +#include + +#include + +namespace solidity::frontend +{ + +/** + * Contains the set of rules to compute an array slice. + * Rules: + * 1. end > start => ArraySliceHeader(a, b, start, end, 0) + * 2. ArraySliceHeader(a, b, start, end, i) && i >= (end - start) => ArraySlice(a, b, start, end) + * 3. ArraySliceHeader(a, b, start, end, i) && i >= 0 && i < (end - start) => ArraySliceLoop(a, b, start, end, i) + * 4. ArraySliceLoop(a, b, start, end, i) && b[i] = a[start + i] => ArraySliceHeader(a, b, start, end, i + 1) + * + * The rule to be used by CHC is ArraySlice(a, b, start, end). + */ + +struct ArraySlicePredicate +{ + /// Contains the predicates and rules created to compute + /// array slices for a given sort. + struct SliceData + { + std::vector predicates; + std::vector rules; + }; + + /// @returns a flag representing whether the array slice predicates had already been created before for this sort, + /// and the corresponding slice data. + static std::pair create(smtutil::SortPointer _sort, smt::EncodingContext& _context); + + static void reset() { m_slicePredicates.clear(); } + +private: + /// Maps a unique sort name to its slice data. + static std::map m_slicePredicates; +}; + +} diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 67e935ac6..bb7382565 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -22,6 +22,7 @@ #include #endif +#include #include #include #include @@ -470,6 +471,36 @@ void CHC::endVisit(Continue const& _continue) m_currentBlock = predicate(*continueGhost); } +void CHC::endVisit(IndexRangeAccess const& _range) +{ + createExpr(_range); + + auto baseArray = dynamic_pointer_cast(m_context.expression(_range.baseExpression())); + auto sliceArray = dynamic_pointer_cast(m_context.expression(_range)); + solAssert(baseArray && sliceArray, ""); + + auto const& sliceData = ArraySlicePredicate::create(sliceArray->sort(), m_context); + if (!sliceData.first) + { + for (auto pred: sliceData.second.predicates) + m_interface->registerRelation(pred->functor()); + for (auto const& rule: sliceData.second.rules) + addRule(rule, ""); + } + + auto start = _range.startExpression() ? expr(*_range.startExpression()) : 0; + auto end = _range.endExpression() ? expr(*_range.endExpression()) : baseArray->length(); + auto slicePred = (*sliceData.second.predicates.at(0))({ + baseArray->elements(), + sliceArray->elements(), + start, + end + }); + + m_context.addAssertion(slicePred); + m_context.addAssertion(sliceArray->length() == end - start); +} + void CHC::visitAssert(FunctionCall const& _funCall) { auto const& args = _funCall.arguments(); @@ -688,6 +719,7 @@ void CHC::resetSourceAnalysis() m_interfaces.clear(); m_nondetInterfaces.clear(); Predicate::reset(); + ArraySlicePredicate::reset(); m_blockCounter = 0; bool usesZ3 = false; @@ -994,6 +1026,9 @@ smtutil::Expression CHC::predicate(Predicate const& _block) case PredicateType::NondetInterface: // Nondeterministic interface predicates are handled differently. solAssert(false, ""); + case PredicateType::Custom: + // Custom rules are handled separately. + solAssert(false, ""); } solAssert(false, ""); } diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 5dc996c29..e76f75c89 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -81,6 +81,7 @@ private: void endVisit(FunctionCall const& _node) override; void endVisit(Break const& _node) override; void endVisit(Continue const& _node) override; + void endVisit(IndexRangeAccess const& _node) override; void visitAssert(FunctionCall const& _funCall); void visitAddMulMod(FunctionCall const& _funCall) override; diff --git a/libsolidity/formal/Predicate.h b/libsolidity/formal/Predicate.h index addf5ea32..a87e81afa 100644 --- a/libsolidity/formal/Predicate.h +++ b/libsolidity/formal/Predicate.h @@ -39,7 +39,8 @@ enum class PredicateType FunctionEntry, FunctionSummary, FunctionBlock, - Error + Error, + Custom }; /** diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index ba6833e3a..993f49442 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -1095,11 +1095,7 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess) void SMTEncoder::endVisit(IndexRangeAccess const& _indexRangeAccess) { createExpr(_indexRangeAccess); - m_errorReporter.warning( - 2923_error, - _indexRangeAccess.location(), - "Assertion checker does not yet implement this expression." - ); + /// The actual slice is created by CHC which also assigns the length. } void SMTEncoder::arrayAssignment() diff --git a/test/libsolidity/smtCheckerTests/operators/slice.sol b/test/libsolidity/smtCheckerTests/operators/slice.sol new file mode 100644 index 000000000..41c5dbd56 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/slice.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; + +contract C { + function f(bytes calldata b) external pure { + require(b[10] == 0xff); + assert(bytes(b[10:20]).length == 10); + assert(bytes(b[10:20])[0] == 0xff); + assert(bytes(b[10:20])[5] == 0xff); + } +} +// ---- +// Warning 6328: (198-232): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/slice_default_end.sol b/test/libsolidity/smtCheckerTests/operators/slice_default_end.sol new file mode 100644 index 000000000..1681c0ca5 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/slice_default_end.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; + +contract C { + function f(bytes calldata b) external pure { + require(b.length == 30); + require(b[10] == 0xff); + require(b[b.length - 1] == 0xaa); + assert(bytes(b[10:]).length == 20); + assert(bytes(b[10:])[0] == 0xff); + assert(bytes(b[10:])[5] == 0xff); + assert(bytes(b[10:])[19] == 0xaa); + } +} +// ---- +// Warning 4661: (221-253): BMC: Assertion violation happens here. +// Warning 4661: (257-289): BMC: Assertion violation happens here. +// Warning 4661: (293-326): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/slice_default_start.sol b/test/libsolidity/smtCheckerTests/operators/slice_default_start.sol new file mode 100644 index 000000000..61aa3ba2a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/slice_default_start.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C { + function f(bytes calldata b) external pure { + require(b[0] == 0xff); + assert(bytes(b[:20]).length == 20); + assert(bytes(b[:20])[0] == 0xff); + assert(bytes(b[:20])[5] == 0xff); + } +} +// ---- +// Warning 6328: (193-225): CHC: Assertion violation happens here. +// Warning 4661: (157-189): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/slices_1.sol b/test/libsolidity/smtCheckerTests/operators/slices_1.sol index 15e3c8e17..1f5fcf4e1 100644 --- a/test/libsolidity/smtCheckerTests/operators/slices_1.sol +++ b/test/libsolidity/smtCheckerTests/operators/slices_1.sol @@ -8,6 +8,3 @@ contract C { } } // ---- -// Warning 2923: (94-109): Assertion checker does not yet implement this expression. -// Warning 2923: (113-128): Assertion checker does not yet implement this expression. -// Warning 2923: (132-165): Assertion checker does not yet implement this expression. diff --git a/test/libsolidity/smtCheckerTests/special/abi_encode_slice.sol b/test/libsolidity/smtCheckerTests/special/abi_encode_slice.sol index 6a61a2618..927ecf631 100644 --- a/test/libsolidity/smtCheckerTests/special/abi_encode_slice.sol +++ b/test/libsolidity/smtCheckerTests/special/abi_encode_slice.sol @@ -5,5 +5,4 @@ contract C { } } // ---- -// Warning 2923: (143-152): Assertion checker does not yet implement this expression. // Warning 4588: (126-154): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/typecast/slice_to_bytes.sol b/test/libsolidity/smtCheckerTests/typecast/slice_to_bytes.sol index ff3760dd4..bae24de4c 100644 --- a/test/libsolidity/smtCheckerTests/typecast/slice_to_bytes.sol +++ b/test/libsolidity/smtCheckerTests/typecast/slice_to_bytes.sol @@ -8,6 +8,3 @@ contract C { } } // ---- -// Warning 2923: (100-115): Assertion checker does not yet implement this expression. -// Warning 2923: (126-141): Assertion checker does not yet implement this expression. -// Warning 2923: (152-185): Assertion checker does not yet implement this expression.