Merge pull request #9137 from ethereum/smt_fix_aliasing

[SMTChecker] Erase knowledge when array variable is pushed/popped

Changelog.md

@@ -8,6 +8,7 @@ Compiler Features:
 
 Bugfixes:
  * SMTChecker: Fix internal error when encoding tuples of tuples.
+ * SMTChecker: Fix aliasing soundness after pushing to an array pointer.
 
 
 ### 0.6.9 (2020-06-04)

libsolidity/formal/SMTEncoder.cpp

@@ -1001,38 +1001,7 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smtutil::Expressi
 			solAssert(varDecl, "");
 
 			if (varDecl->hasReferenceOrMappingType())
-				m_context.resetVariables([&](VariableDeclaration const& _var) {
+				resetReferences(*varDecl);
-					if (_var == *varDecl)
-						return false;
-
-					// If both are state variables no need to clear knowledge.
-					if (_var.isStateVariable() && varDecl->isStateVariable())
-						return false;
-
-					TypePointer prefix = _var.type();
-					TypePointer originalType = typeWithoutPointer(varDecl->type());
-					while (
-						prefix->category() == Type::Category::Mapping ||
-						prefix->category() == Type::Category::Array
-					)
-					{
-						if (*originalType == *typeWithoutPointer(prefix))
-							return true;
-						if (prefix->category() == Type::Category::Mapping)
-						{
-							auto mapPrefix = dynamic_cast<MappingType const*>(prefix);
-							solAssert(mapPrefix, "");
-							prefix = mapPrefix->valueType();
-						}
-						else
-						{
-							auto arrayPrefix = dynamic_cast<ArrayType const*>(prefix);
-							solAssert(arrayPrefix, "");
-							prefix = arrayPrefix->baseType();
-						}
-					}
-					return false;
-				});
 
 			auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.variable(*varDecl));
 			smtutil::Expression store = smtutil::Expression::store(
@@ -1138,6 +1107,8 @@ void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression
 	{
 		auto varDecl = identifierToVariable(*id);
 		solAssert(varDecl, "");
+		if (varDecl->hasReferenceOrMappingType())
+			resetReferences(*varDecl);
 		m_context.addAssertion(m_context.newValue(*varDecl) == _array);
 	}
 	else if (auto const* indexAccess = dynamic_cast<IndexAccess const*>(&_expr))
@@ -1641,6 +1612,42 @@ void SMTEncoder::resetStateVariables()
 	m_context.resetVariables([&](VariableDeclaration const& _variable) { return _variable.isStateVariable(); });
 }
 
+void SMTEncoder::resetReferences(VariableDeclaration const& _varDecl)
+{
+	m_context.resetVariables([&](VariableDeclaration const& _var) {
+		if (_var == _varDecl)
+			return false;
+
+		// If both are state variables no need to clear knowledge.
+		if (_var.isStateVariable() && _varDecl.isStateVariable())
+			return false;
+
+		TypePointer prefix = _var.type();
+		TypePointer originalType = typeWithoutPointer(_varDecl.type());
+		while (
+			prefix->category() == Type::Category::Mapping ||
+			prefix->category() == Type::Category::Array
+		)
+		{
+			if (*originalType == *typeWithoutPointer(prefix))
+				return true;
+			if (prefix->category() == Type::Category::Mapping)
+			{
+				auto mapPrefix = dynamic_cast<MappingType const*>(prefix);
+				solAssert(mapPrefix, "");
+				prefix = mapPrefix->valueType();
+			}
+			else
+			{
+				auto arrayPrefix = dynamic_cast<ArrayType const*>(prefix);
+				solAssert(arrayPrefix, "");
+				prefix = arrayPrefix->baseType();
+			}
+		}
+		return false;
+	});
+}
+
 TypePointer SMTEncoder::typeWithoutPointer(TypePointer const& _type)
 {
 	if (auto refType = dynamic_cast<ReferenceType const*>(_type))

libsolidity/formal/SMTEncoder.h

@@ -183,6 +183,9 @@ protected:
 	void initializeLocalVariables(FunctionDefinition const& _function);
 	void initializeFunctionCallParameters(CallableDeclaration const& _function, std::vector<smtutil::Expression> const& _callArgs);
 	void resetStateVariables();
+	/// Resets all references/pointers that have the same type or have
+	/// a subexpression of the same type as _varDecl.
+	void resetReferences(VariableDeclaration const& _varDecl);
 	/// @returns the type without storage pointer information if it has it.
 	TypePointer typeWithoutPointer(TypePointer const& _type);
 

test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_length.sol

@@ -0,0 +1,23 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[][] a;
+	uint[][][] c;
+	uint[] d;
+	function f() public {
+		a.push();
+		uint[] storage b = a[0];
+		c[0][0][0] = 12;
+		d[5] = 7;
+		b.push(8);
+		assert(a[0].length == 0);
+		// Safe but knowledge about `c` is erased because `b` could be pointing to `c[x][y]`.
+		assert(c[0][0][0] == 12);
+		// Safe but knowledge about `d` is erased because `b` could be pointing to `d`.
+		assert(d[5] == 7);
+	}
+}
+// ----
+// Warning: (193-217): Assertion violation happens here
+// Warning: (309-333): Assertion violation happens here
+// Warning: (419-436): Assertion violation happens here