Merge pull request #9885 from ethereum/smt_array_slices

[SMTChecker] Support array slices

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``

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

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 <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#include <libsolidity/formal/ArraySlicePredicate.h>
+
+#include <liblangutil/Exceptions.h>
+
+using namespace std;
+using namespace solidity;
+using namespace solidity::smtutil;
+using namespace solidity::frontend;
+using namespace solidity::frontend::smt;
+
+map<string, ArraySlicePredicate::SliceData> ArraySlicePredicate::m_slicePredicates;
+
+pair<bool, ArraySlicePredicate::SliceData const&> ArraySlicePredicate::create(SortPointer _sort, EncodingContext& _context)
+{
+	solAssert(_sort->kind == Kind::Tuple, "");
+	auto tupleSort = dynamic_pointer_cast<TupleSort>(_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<SortPointer> domain{sort, sort, startVar.sort(), endVar.sort()};
+	auto sliceSort = make_shared<FunctionSort>(domain, SortProvider::boolSort);
+	Predicate const& slice = *Predicate::create(sliceSort, "array_slice_" + tupleName, PredicateType::Custom, _context);
+
+	domain.emplace_back(iVar.sort());
+	auto predSort = make_shared<FunctionSort>(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)}
+	}};
+}

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 <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#include <libsolidity/formal/EncodingContext.h>
+#include <libsolidity/formal/Predicate.h>
+#include <libsolidity/formal/SymbolicVariables.h>
+
+#include <libsmtutil/Sorts.h>
+
+#include <vector>
+
+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<Predicate const*> predicates;
+		std::vector<smtutil::Expression> 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<bool, SliceData const&> 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<std::string, SliceData> m_slicePredicates;
+};
+
+}

libsolidity/formal/CHC.cpp

@@ -22,6 +22,7 @@
 #include <libsmtutil/Z3CHCInterface.h>
 #endif
 
+#include <libsolidity/formal/ArraySlicePredicate.h>
 #include <libsolidity/formal/PredicateInstance.h>
 #include <libsolidity/formal/PredicateSort.h>
 #include <libsolidity/formal/SymbolicTypes.h>
@@ -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<SymbolicArrayVariable>(m_context.expression(_range.baseExpression()));
+	auto sliceArray = dynamic_pointer_cast<SymbolicArrayVariable>(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, "");
 }

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;

libsolidity/formal/Predicate.h

@@ -39,7 +39,8 @@ enum class PredicateType
 	FunctionEntry,
 	FunctionSummary,
 	FunctionBlock,
-	Error
+	Error,
+	Custom
 };
 
 /**

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()

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.

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.

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.

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.

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.

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.