Handle aliasing

libsolidity/formal/SMTChecker.cpp

@@ -535,13 +535,6 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
 		m_interface->addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1));
 }
 
-void SMTChecker::eraseArrayKnowledge()
-{
-	for (auto const& var: m_variables)
-		if (var.first->annotation().type->category() == Type::Category::Mapping)
-			newValue(*var.first);
-}
-
 void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
 {
 	FunctionDefinition const* _funDef = nullptr;
@@ -805,7 +798,6 @@ void SMTChecker::endVisit(IndexAccess const& _indexAccess)
 void SMTChecker::arrayAssignment()
 {
 	m_arrayAssignmentHappened = true;
-	eraseArrayKnowledge();
 }
 
 void SMTChecker::arrayIndexAssignment(Assignment const& _assignment)
@@ -815,6 +807,36 @@ void SMTChecker::arrayIndexAssignment(Assignment const& _assignment)
 	{
 		auto const& varDecl = dynamic_cast<VariableDeclaration const&>(*id->annotation().referencedDeclaration);
 		solAssert(knownVariable(varDecl), "");
+
+		if (varDecl.hasReferenceOrMappingType())
+			resetVariables([&](VariableDeclaration const& _var) {
+				if (_var == varDecl)
+					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.get());
+						solAssert(mapPrefix, "");
+						prefix = mapPrefix->valueType();
+					}
+					else
+					{
+						auto arrayPrefix = dynamic_cast<ArrayType const*>(prefix.get());
+						solAssert(arrayPrefix, "");
+						prefix = arrayPrefix->baseType();
+					}
+				}
+				return false;
+			});
+
 		smt::Expression store = smt::Expression::store(
 			m_variables[&varDecl]->currentValue(),
 			expr(*indexAccess.indexExpression()),
@@ -1325,6 +1347,13 @@ void SMTChecker::resetVariables(function<bool(VariableDeclaration const&)> const
 	});
 }
 
+TypePointer SMTChecker::typeWithoutPointer(TypePointer const& _type)
+{
+	if (auto refType = dynamic_cast<ReferenceType const*>(_type.get()))
+		return ReferenceType::copyForLocationIfReference(refType->location(), _type);
+	return _type;
+}
+
 void SMTChecker::mergeVariables(vector<VariableDeclaration const*> const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse)
 {
 	set<VariableDeclaration const*> uniqueVars(_variables.begin(), _variables.end());

libsolidity/formal/SMTChecker.h

@@ -103,8 +103,6 @@ private:
 	void arrayAssignment();
 	/// Handles assignment to SMT array index.
 	void arrayIndexAssignment(Assignment const& _assignment);
-	/// Erases information about SMT arrays.
-	void eraseArrayKnowledge();
 
 	/// Division expression in the given type. Requires special treatment because
 	/// of rounding for signed division.
@@ -177,6 +175,9 @@ private:
 	void resetStorageReferences();
 	void resetVariables(std::vector<VariableDeclaration const*> _variables);
 	void resetVariables(std::function<bool(VariableDeclaration const&)> const& _filter);
+	/// @returns the type without storage pointer information if it has it.
+	TypePointer typeWithoutPointer(TypePointer const& _type);
+
 	/// Given two different branches and the touched variables,
 	/// merge the touched variables into after-branch ite variables
 	/// using the branch condition as guard.

test/libsolidity/smtCheckerTests/simple/static_array.sol

@@ -7,3 +7,4 @@ contract C
 	int[3*1] x;
 }
 // ----
+// Warning: (153-156): Assertion checker does not yet implement this operator on non-integer types.

test/libsolidity/smtCheckerTests/types/array_aliasing_memory_1.sol

@@ -0,0 +1,31 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(
+		uint[] memory a,
+		uint[] memory b,
+		uint[][] memory cc,
+		uint8[][] memory dd,
+		uint[][][] memory eee
+	) internal pure {
+		require(a[0] == 2);
+		require(cc[0][0] == 50);
+		require(dd[0][0] == 10);
+		require(eee[0][0][0] == 50);
+		b[0] = 1;
+		// Fails because b == a is possible.
+		assert(a[0] == 2);
+		// Fails because b == cc[0] is possible.
+		assert(cc[0][0] == 50);
+		// Should not fail since knowledge is erased only for uint[].
+		assert(dd[0][0] == 10);
+		// Fails because b == ee[0][0] is possible.
+		assert(eee[0][0][0] == 50);
+		assert(b[0] == 1);
+	}
+}
+// ----
+// Warning: (345-362): Assertion violation happens here
+// Warning: (409-431): Assertion violation happens here
+// Warning: (571-597): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_aliasing_memory_2.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[] array;
+	function f(uint[] memory a, uint[] memory b) internal view {
+		require(array[0] == 42);
+		require(a[0] == 2);
+		b[0] = 1;
+		// Erasing knowledge about memory references should not
+		// erase knowledge about state variables.
+		assert(array[0] == 42);
+		assert(a[0] == 2);
+		assert(b[0] == 1);
+	}
+}
+// ----
+// Warning: (314-331): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_aliasing_memory_3.sol

@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[] array;
+	function f(uint[] memory a, uint[] memory b) internal view {
+		require(array[0] == 42);
+		uint[] storage c = array;
+		require(a[0] == 2);
+		b[0] = 1;
+		// Erasing knowledge about memory references should not
+		// erase knowledge about state variables.
+		assert(array[0] == 42);
+		// Erasing knowledge about memory references should not
+		// erase knowledge about storage references.
+		assert(c[0] == 42);
+		assert(a[0] == 2);
+		assert(b[0] == 1);
+	}
+}
+// ----
+// Warning: (469-486): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_aliasing_storage_1.sol

@@ -0,0 +1,45 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[] array;
+	uint[][] array2d;
+	uint8[] tinyArray;
+	function f(
+		uint[] storage a,
+		uint[] storage b,
+		uint[][] storage cc,
+		uint8[][] storage dd,
+		uint[][][] storage eee
+	) internal {
+		require(a[0] == 2);
+		require(array[0] == 42);
+		require(array2d[0][0] == 42);
+		require(tinyArray[0] == 42);
+		require(cc[0][0] == 42);
+		require(dd[0][0] == 42);
+		require(eee[0][0][0] == 42);
+		b[0] = 1;
+		// Fails because b == a is possible.
+		assert(a[0] == 2);
+		// Fails because b == array is possible.
+		assert(array[0] == 42);
+		// Fails because b == array2d[0] is possible.
+		assert(array2d[0][0] == 42);
+		// Should not fail since knowledge is erased only for uint[].
+		assert(tinyArray[0] == 42);
+		// Fails because b == cc[0] is possible.
+		assert(cc[0][0] == 42);
+		// Should not fail since knowledge is erased only for uint[].
+		assert(dd[0][0] == 42);
+		// Fails because b == ee[0][0] is possible.
+		assert(eee[0][0][0] == 42);
+		assert(b[0] == 1);
+	}
+}
+// ----
+// Warning: (489-506): Assertion violation happens here
+// Warning: (553-575): Assertion violation happens here
+// Warning: (627-654): Assertion violation happens here
+// Warning: (795-817): Assertion violation happens here
+// Warning: (957-983): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_aliasing_storage_2.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint[] storage a, uint[] storage b, uint[] memory c) internal {
+		require(c[0] == 42);
+		require(a[0] == 2);
+		b[0] = 1;
+		// Erasing knowledge about storage references should not
+		// erase knowledge about memory references.
+		assert(c[0] == 42);
+		// Fails because b == a is possible.
+		assert(a[0] == 2);
+		assert(b[0] == 1);
+	}
+}
+// ----
+// Warning: (347-364): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_aliasing_storage_3.sol

@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint[] storage a, uint[] storage b, uint[] memory c) internal {
+		uint[] memory d = c;
+		require(c[0] == 42);
+		require(a[0] == 2);
+		b[0] = 1;
+		// Erasing knowledge about storage references should not
+		// erase knowledge about memory references.
+		assert(c[0] == 42);
+		// Erasing knowledge about storage references should not
+		// erase knowledge about memory references.
+		assert(d[0] == 42);
+		// Fails because b == a is possible.
+		assert(a[0] == 2);
+		assert(b[0] == 1);
+	}
+}
+// ----
+// Warning: (497-514): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_aliasing_storage_4.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[] array;
+	function f(uint[] storage a, uint[] storage b) internal {
+		require(a[0] == 2);
+		require(b[0] == 42);
+		array[0] = 1;
+		// Fails because array == a is possible.
+		assert(a[0] == 2);
+		// Fails because array == b is possible.
+		assert(b[0] == 42);
+		assert(array[0] == 1);
+	}
+}
+// ----
+// Warning: (226-243): Assertion violation happens here
+// Warning: (290-308): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_1.sol

@@ -0,0 +1,24 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	mapping (uint => uint) singleMap;
+	mapping (uint => uint)[] severalMaps;
+	mapping (uint => uint8)[] severalMaps8;
+	mapping (uint => uint)[][] severalMaps3d;
+	function f(mapping (uint => uint) storage map) internal {
+		require(severalMaps[0][0] == 42);
+		require(severalMaps8[0][0] == 42);
+		require(severalMaps3d[0][0][0] == 42);
+		map[0] = 2;
+		// Should fail since map == severalMaps[0] is possible.
+		assert(severalMaps[0][0] == 42);
+		// Should not fail since knowledge is erase only for mapping (uint => uint).
+		assert(severalMaps8[0][0] == 42);
+		// Should fail since map == severalMaps3d[0][0] is possible.
+		assert(severalMaps3d[0][0][0] == 42);
+	}
+}
+// ----
+// Warning: (451-482): Assertion violation happens here
+// Warning: (664-700): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/mapping_aliasing_2.sol

@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	mapping (uint => uint) a;
+	mapping (uint => mapping (uint => uint)) maps;
+	mapping (uint => mapping (uint => uint8)) maps8;
+	function f(mapping (uint => uint) storage map1, mapping (uint => uint) storage map2) internal {
+		require(map1[0] == 2);
+		require(a[0] == 42);
+		require(maps[0][0] == 42);
+		require(maps8[0][0] == 42);
+		map2[0] = 1;
+		// Fails because map2 == map1 is possible.
+		assert(map1[0] == 2);
+		// Fails because map2 == a is possible.
+		assert(a[0] == 42);
+		// Fails because map2 == maps[0] is possible.
+		assert(maps[0][0] == 42);
+		// Should not fail since knowledge is erased only for mapping (uint => uint).
+		assert(maps8[0][0] == 42);
+		assert(map2[0] == 1);
+	}
+}
+// ----
+// Warning: (437-457): Assertion violation happens here
+// Warning: (503-521): Assertion violation happens here
+// Warning: (573-597): Assertion violation happens here