Merge pull request #12404 from ethereum/smt_fix_havocing

[SMTChecker] Fix soundness of struct storage/memory pointers

Author: Leo

Changelog.md

@@ -9,6 +9,7 @@ Compiler Features:
 Bugfixes:
  * Code Generator: Fix a crash when using ``@use-src`` and compiling from Yul to ewasm.
  * SMTChecker: Fix internal error when an unsafe target is solved more than once and the counterexample messages are different.
+ * SMTChecker: Fix soundness of assigned storage/memory local pointers that were not erasing enough knowledge.
  * Fix internal error when a function has a calldata struct argument with an internal type inside.
 
 

libsolidity/formal/SMTEncoder.cpp

@@ -32,6 +32,8 @@
 
 #include <liblangutil/CharStreamProvider.h>
 
+#include <libsolutil/Algorithms.h>
+
 #include <range/v3/view.hpp>
 
 #include <limits>
@@ -2371,28 +2373,25 @@ void SMTEncoder::resetReferences(Type const* _type)
 
 bool SMTEncoder::sameTypeOrSubtype(Type const* _a, Type const* _b)
 {
-	Type const* prefix = _a;
-	while (
-		prefix->category() == Type::Category::Mapping ||
-		prefix->category() == Type::Category::Array
-	)
-	{
-		if (*typeWithoutPointer(_b) == *typeWithoutPointer(prefix))
-			return true;
-		if (prefix->category() == Type::Category::Mapping)
-		{
-			auto mapPrefix = dynamic_cast<MappingType const*>(prefix);
-			solAssert(mapPrefix, "");
-			prefix = mapPrefix->valueType();
-		}
-		else
+	bool foundSame = false;
+
+	solidity::util::BreadthFirstSearch<Type const*> bfs{{_a}};
+	bfs.run([&](auto _type, auto&& _addChild) {
+		if (*typeWithoutPointer(_b) == *typeWithoutPointer(_type))
 		{
-			auto arrayPrefix = dynamic_cast<ArrayType const*>(prefix);
-			solAssert(arrayPrefix, "");
-			prefix = arrayPrefix->baseType();
+			foundSame = true;
+			bfs.abort();
 		}
-	}
-	return false;
+		if (auto const* mapType = dynamic_cast<MappingType const*>(_type))
+			_addChild(mapType->valueType());
+		else if (auto const* arrayType = dynamic_cast<ArrayType const*>(_type))
+			_addChild(arrayType->baseType());
+		else if (auto const* structType = dynamic_cast<StructType const*>(_type))
+			for (auto const& member: structType->nativeMembers(nullptr))
+				_addChild(member.type);
+	});
+
+	return foundSame;
 }
 
 bool SMTEncoder::isSupportedType(Type const& _type) const

test/libsolidity/smtCheckerTests/file_level/import.sol

@@ -22,5 +22,5 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (B:238-252): CHC: Assertion violation happens here.\nCounterexample:\ndata = {x: 0}\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: data = {x: 0}\nC.g()\n    C.f(7) -- internal call\n        A:set({x: 0}, 7) -- internal call\n        A:set({x: 0}, 8) -- internal call
-// Warning 6328: (B:308-322): CHC: Assertion violation happens here.\nCounterexample:\ndata = {x: 0}\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: data = {x: 0}\nC.g()\n    C.f(7) -- internal call\n        A:set({x: 0}, 7) -- internal call\n        A:set({x: 0}, 8) -- internal call
+// Warning 6328: (B:238-252): CHC: Assertion violation happens here.\nCounterexample:\ndata = {x: 21238}\nx = 8\ny = 21238\n\nTransaction trace:\nC.constructor()\nState: data = {x: 0}\nC.g()\n    C.f(7) -- internal call\n        A:set({x: 0}, 7) -- internal call\n        A:set({x: 8}, 8) -- internal call
+// Warning 6328: (B:308-322): CHC: Assertion violation happens here.\nCounterexample:\ndata = {x: 6}\nx = 0\ny = 6\n\nTransaction trace:\nC.constructor()\nState: data = {x: 0}\nC.g()\n    C.f(7) -- internal call\n        A:set({x: 0}, 7) -- internal call\n        A:set({x: 0}, 8) -- internal call

test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_memory_1.sol

@@ -0,0 +1,21 @@
+contract C {
+    struct S {
+		uint sum;
+		uint[] a;
+    }
+
+	function f(S memory m, uint v) internal pure {
+		m.sum = v;
+		m.a = new uint[](2);
+	}
+
+	constructor(uint amt) {
+		S memory s;
+		f(s, amt);
+		assert(s.a.length == 2); // should hold but no aliasing support means it fails for now
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (201-224): CHC: Assertion violation happens here.\nCounterexample:\n\namt = 0\ns = {sum: 0, a: []}\n\nTransaction trace:\nC.constructor(0)

test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_memory_2.sol

@@ -0,0 +1,26 @@
+contract C {
+    struct S {
+		uint sum;
+		uint[] a;
+    }
+
+	struct T {
+		S s;
+		uint x;
+	}
+
+	function f(S memory m, uint v) internal pure {
+		m.sum = v;
+		m.a = new uint[](2);
+	}
+
+	constructor(uint amt) {
+		T memory t;
+		f(t.s, amt);
+		assert(t.s.a.length == 2); // should hold but no aliasing support means it fails for now
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (236-261): CHC: Assertion violation happens here.\nCounterexample:\n\namt = 0\nt = {s: {sum: 0, a: []}, x: 0}\n\nTransaction trace:\nC.constructor(0)

test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_memory_3.sol

@@ -0,0 +1,26 @@
+contract C {
+    struct S {
+		uint sum;
+		uint[] a;
+    }
+
+	struct T {
+		S s;
+		uint x;
+	}
+
+	function f(T memory m, uint v) internal pure {
+		m.s.sum = v;
+		m.s.a = new uint[](2);
+	}
+
+	constructor(uint amt) {
+		T memory t;
+		f(t, amt);
+		assert(t.s.a.length == 2); // should hold but no aliasing support means it fails for now
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (238-263): CHC: Assertion violation happens here.\nCounterexample:\n\namt = 0\nt = {s: {sum: 0, a: []}, x: 0}\n\nTransaction trace:\nC.constructor(0)

test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_1.sol

@@ -0,0 +1,24 @@
+contract C {
+    struct S {
+        mapping(address => uint) innerM;
+		uint sum;
+    }
+
+	function f(S storage m, address i, uint v) internal {
+		m.innerM[i] = v;
+		m.sum += v;
+	}
+
+	S s;
+
+	constructor(uint amt) {
+		f(s, msg.sender, amt);
+	}
+	function g() public view {
+		assert(s.sum == 0); // should hold but no aliasing support means it fails for now
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (270-288): CHC: Assertion violation happens here.\nCounterexample:\ns = {innerM, sum: 21239}\n\nTransaction trace:\nC.constructor(0){ msg.sender: 0x6dc4 }\nState: s = {innerM, sum: 21239}\nC.g()

test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_2.sol

@@ -0,0 +1,23 @@
+contract C {
+    struct S {
+        mapping(address => uint) innerM;
+		uint sum;
+    }
+
+	function f(mapping(address => uint) storage innerM, address i, uint v) internal {
+		innerM[i] = v;
+	}
+
+	S s;
+
+	constructor(uint amt) {
+		f(s.innerM, msg.sender, amt);
+	}
+	function g() public view {
+		assert(s.innerM[msg.sender] == 0); // should hold but no aliasing support means it fails for now
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (289-322): CHC: Assertion violation happens here.\nCounterexample:\ns = {innerM, sum: 10}\n\nTransaction trace:\nC.constructor(0){ msg.sender: 0x6dc4 }\nState: s = {innerM, sum: 10}\nC.g(){ msg.sender: 0x0985 }

test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_3.sol

@@ -0,0 +1,29 @@
+contract C {
+    struct S {
+        mapping(address => uint) innerM;
+		uint sum;
+    }
+
+	struct T {
+		uint x;
+		S s;
+	}
+
+	function f(T storage m, address i, uint v) internal {
+		m.s.innerM[i] = v;
+		m.s.sum += v;
+	}
+
+	T t;
+
+	constructor(uint amt) {
+		f(t, msg.sender, amt);
+	}
+	function g() public view {
+		assert(t.s.sum == 0); // should hold but no aliasing support means it fails for now
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (307-327): CHC: Assertion violation happens here.\nCounterexample:\nt = {x: 10, s: {innerM, sum: 21239}}\n\nTransaction trace:\nC.constructor(0){ msg.sender: 0x6dc4 }\nState: t = {x: 10, s: {innerM, sum: 21239}}\nC.g()

test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_4.sol

@@ -0,0 +1,29 @@
+contract C {
+    struct S {
+        mapping(address => uint) innerM;
+		uint sum;
+    }
+
+	struct T {
+		uint x;
+		S s;
+	}
+
+	function f(S storage m, address i, uint v) internal {
+		m.innerM[i] = v;
+		m.sum += v;
+	}
+
+	T t;
+
+	constructor(uint amt) {
+		f(t.s, msg.sender, amt);
+	}
+	function g() public view {
+		assert(t.s.sum == 0); // should hold but no aliasing support means it fails for now
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (305-325): CHC: Assertion violation happens here.\nCounterexample:\nt = {x: 10, s: {innerM, sum: 21239}}\n\nTransaction trace:\nC.constructor(0){ msg.sender: 0x6dc4 }\nState: t = {x: 10, s: {innerM, sum: 21239}}\nC.g()