Merge pull request #11059 from blishko/smt-array_of_structs-getter

[SMTChecker] Fix public getter for array of structs.

Changelog.md

@@ -8,10 +8,10 @@ Compiler Features:
 
 Bugfixes:
  * SMTChecker: Fix internal error on ``FixedBytes`` constant initialized with string literal.
+ * SMTChecker: Fix internal error on calling public getter on a state variable of type array (possibly nested) of structs.
  * SMTChecker: Fix internal error on pushing to ``string`` casted to ``bytes``.
 AST Changes:
 
-
 ### 0.8.2 (2021-03-02)
 
 Compiler Features:

libsolidity/formal/SMTEncoder.cpp

@@ -35,6 +35,8 @@
 #include <boost/range/adaptors.hpp>
 #include <boost/range/adaptor/reversed.hpp>
 
+#include <deque>
+
 using namespace std;
 using namespace solidity;
 using namespace solidity::util;
@@ -1016,18 +1018,23 @@ void SMTEncoder::visitPublicGetter(FunctionCall const& _funCall)
 	auto paramExpectedTypes = FunctionType(*var).parameterTypes();
 	auto actualArguments = _funCall.arguments();
 	solAssert(actualArguments.size() == paramExpectedTypes.size(), "");
-	vector<smtutil::Expression> symbArguments;
+	deque<smtutil::Expression> symbArguments;
 	for (unsigned i = 0; i < paramExpectedTypes.size(); ++i)
 		symbArguments.push_back(expr(*actualArguments[i], paramExpectedTypes[i]));
 
+	// See FunctionType::FunctionType(VariableDeclaration const& _varDecl)
+	// to understand the return types of public getters.
 	TypePointer type = var->type();
+	smtutil::Expression currentExpr = currentValue(*var);
+	while (true)
+	{
 		if (
 			type->isValueType() ||
 			(type->category() == Type::Category::Array && dynamic_cast<ArrayType const&>(*type).isByteArray())
 		)
 		{
 			solAssert(symbArguments.empty(), "");
-		defineExpr(_funCall, currentValue(*var));
+			defineExpr(_funCall, currentExpr);
 			return;
 		}
 		switch (type->category())
@@ -1035,26 +1042,27 @@ void SMTEncoder::visitPublicGetter(FunctionCall const& _funCall)
 			case Type::Category::Array:
 			case Type::Category::Mapping:
 			{
+				solAssert(!symbArguments.empty(), "");
 				// For nested arrays/mappings, each argument in the call is an index to the next layer.
 				// We mirror this with `select` after unpacking the SMT-LIB array expression.
-			smtutil::Expression exprVal = currentValue(*var);
+				currentExpr = smtutil::Expression::select(smtutil::Expression::tuple_get(currentExpr, 0), symbArguments.front());
-			for (auto const& arg: symbArguments)
+				symbArguments.pop_front();
-			{
+				if (auto arrayType = dynamic_cast<ArrayType const*>(type))
-				exprVal = smtutil::Expression::select(
+					type = arrayType->baseType();
-					smtutil::Expression::tuple_get(exprVal, 0),
+				else if (auto mappingType = dynamic_cast<MappingType const*>(type))
-					arg
+					type = mappingType->valueType();
-				);
+				else
-			}
+					solAssert(false, "");
-			defineExpr(_funCall, exprVal);
 				break;
 			}
 			case Type::Category::Struct:
 			{
-			auto returnedMembers = structGetterReturnedMembers(dynamic_cast<StructType const&>(*type));
+				solAssert(symbArguments.empty(), "");
+				smt::SymbolicStructVariable structVar(dynamic_cast<StructType const*>(type), "struct_temp_" + to_string(_funCall.id()), m_context);
+				m_context.addAssertion(structVar.currentValue() == currentExpr);
+				auto returnedMembers = structGetterReturnedMembers(dynamic_cast<StructType const&>(*structVar.type()));
 				solAssert(!returnedMembers.empty(), "");
-			auto structVar = dynamic_pointer_cast<smt::SymbolicStructVariable>(m_context.variable(*var));
+				auto returnedValues = applyMap(returnedMembers, [&](string const& memberName) { return structVar.member(memberName); });
-			solAssert(structVar, "");
-			auto returnedValues = applyMap(returnedMembers, [&](string const& memberName) { return structVar->member(memberName); });
 				if (returnedValues.size() == 1)
 					defineExpr(_funCall, returnedValues.front());
 				else
@@ -1067,9 +1075,14 @@ void SMTEncoder::visitPublicGetter(FunctionCall const& _funCall)
 					for (unsigned i = 0; i < symbComponents.size(); ++i)
 						m_context.addAssertion(symbTuple->component(i) == returnedValues.at(i));
 				}
-			break;
+				return;
+			}
+			default:
+			{
+				// Unsupported cases, do nothing and the getter will be abstracted.
+				return;
+			}
 		}
-		default: {} // Unsupported cases, do nothing and the getter will be abstracted.
 	}
 }
 

libsolidity/formal/SMTEncoder.h

@@ -311,7 +311,6 @@ protected:
 	void createExpr(Expression const& _e);
 	/// Creates the expression and sets its value.
 	void defineExpr(Expression const& _e, smtutil::Expression _value);
-
 	/// Overwrites the current path condition
 	void setPathCondition(smtutil::Expression const& _e);
 	/// Adds a new path condition

test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_1.sol

@@ -0,0 +1,16 @@
+pragma abicoder v1;
+pragma experimental SMTChecker;
+
+struct Item {
+	uint x;
+	uint y;
+}
+
+contract D {
+	Item[][][] public items;
+
+	function test() public view returns (uint) {
+		(uint a, uint b) = this.items(1, 2, 3);
+		return a + b;
+	}
+}

test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_2.sol

@@ -0,0 +1,22 @@
+pragma abicoder v1;
+pragma experimental SMTChecker;
+
+struct Item {
+	uint x;
+	uint y;
+}
+
+contract D {
+	Item[] public items;
+
+	function test() public {
+		delete items;
+		items.push(Item(42, 43));
+		(uint a, uint b) = this.items(0);
+		assert(a == 42); // should hold
+		assert(b == 43); // should hold
+		assert(b == 0); // should fail
+	}
+}
+// ----
+// Warning 6328: (300-314): CHC: Assertion violation happens here.\nCounterexample:\nitems = [{x: 42, y: 43}]\n\nTransaction trace:\nD.constructor()\nState: items = []\nD.test()

test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_3.sol

@@ -0,0 +1,24 @@
+pragma abicoder v1;
+pragma experimental SMTChecker;
+
+struct Item {
+	uint x;
+	uint y;
+	uint[] arr;
+}
+
+contract D {
+	Item[] public items;
+
+	function test() public {
+		delete items;
+		uint[] memory tmp = new uint[](1);
+		items.push(Item(42, 43, tmp));
+		(uint a, uint b) = this.items(0);
+		assert(a == 42); // should hold
+		assert(b == 43); // should hold
+		assert(b == 0); // should fail
+	}
+}
+// ----
+// Warning 6328: (355-369): CHC: Assertion violation happens here.\nCounterexample:\nitems = [{x: 42, y: 43, arr: [0]}]\n\nTransaction trace:\nD.constructor()\nState: items = []\nD.test()