[SMTChecker] Basic support for inline assembly using over-approximating analysis

test/libsolidity/smtCheckerTests/inline_assembly/assembly_1.sol

@@ -0,0 +1,24 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() internal pure returns (bool) {
+		bool b;
+		assembly { b := 1 } // This assignment is overapproximated at the moment, we don't know value of b after the assembly block
+		return b;
+	}
+	function g() public pure {
+		assert(f()); // False positive currently
+		assert(!f()); // should fail, now because of overapproximation in the analysis
+		require(f()); // BMC constant value not detected at the moment
+		require(!f()); // BMC constant value not ddetected at the moment
+	}
+}
+// ----
+// Warning 7737: (103-122): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
+// Warning 6328: (272-283): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n    C.f() -- internal call
+// Warning 6328: (315-327): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n    C.f() -- internal call\n    C.f() -- internal call
+// Warning 7737: (103-122): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
+// Warning 7737: (103-122): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
+// Warning 7737: (103-122): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
+// Warning 7737: (103-122): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
+// Warning 7737: (103-122): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).

test/libsolidity/smtCheckerTests/inline_assembly/assembly_2.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure returns (bool) {
+		bool b;
+		int x = 42;
+		assembly { b := 1 }
+		assert(x == 42); // should hold
+		assert(b); // should hold, but fails due to overapproximation
+		return b;
+	}
+}
+// ----
+// Warning 7737: (115-134): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
+// Warning 6328: (171-180): CHC: Assertion violation happens here.\nCounterexample:\n\n = false\n\nTransaction trace:\nC.constructor()\nC.f()
+// Warning 7737: (115-134): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).

test/libsolidity/smtCheckerTests/inline_assembly/assembly_3.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f() public pure returns (bool) {
+        bool b;
+        bool c = true;
+        assembly { b := c }
+        assert(c); // should hold, c is not assigned in the assembly
+        assert(b); // should hold, but fails currently because of overapproximation
+        return b;
+    }
+}
+// ----
+// Warning 7737: (139-158): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
+// Warning 6328: (236-245): CHC: Assertion violation happens here.\nCounterexample:\n\n = false\n\nTransaction trace:\nC.constructor()\nC.f()
+// Warning 7737: (139-158): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).

test/libsolidity/smtCheckerTests/inline_assembly/assembly_4.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure returns (bool) {
+		bool b;
+		int x = 42;
+		assembly { b := 1 }
+		b = true;
+		assert(x == 42); // should hold
+		assert(b); // should hold
+		return b;
+	}
+}
+// ----
+// Warning 7737: (115-134): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
+// Warning 7737: (115-134): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).

test/libsolidity/smtCheckerTests/inline_assembly/assembly_5.sol

@@ -0,0 +1,26 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+	}
+
+	S s;
+
+	function f() public {
+		s.x = 42;
+		S memory sm = s;
+		assert(sm.x == 42); // should hold
+		uint256 i = 7;
+		assembly {
+			mstore(sm, i)
+		}
+		sm.x = 10;
+		assert(sm.x == 10); // should hold
+		assert(s.x == 42); // should hold, storage not changed by the assembly
+		assert(i == 7); // should hold, not changed by the assembly
+	}
+}
+// ----
+// Warning 7737: (189-220): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
+// Warning 7737: (189-220): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).

test/libsolidity/smtCheckerTests/inline_assembly/assembly_6.sol

@@ -0,0 +1,25 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+	}
+
+	S s;
+
+	function f() public {
+		s.x = 42;
+		S storage sm = s;
+		assert(sm.x == 42); // should hold
+		uint256 i = 7;
+		assembly {
+			sstore(sm.slot, i)
+		}
+		sm.x = 10;
+		assert(sm.x == 10); // should hold
+		assert(i == 7); // should hold, not changed by the assembly
+	}
+}
+// ----
+// Warning 7737: (190-226): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
+// Warning 7737: (190-226): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).

test/libsolidity/smtCheckerTests/inline_assembly/assembly_local_storage_access_inside_function.sol

@@ -0,0 +1,24 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint256 public z;
+
+	function f() public {
+		z = 42;
+		uint i = 32;
+		assembly {
+			function f() {
+				sstore(z.slot, 7)
+			}
+			f()
+		}
+		assert(z == 42); // should fail
+		assert(z == 7); // should hold, but the analysis cannot know this yet
+		assert(i == 32); // should hold, not changed by the assembly
+	}
+}
+// ----
+// Warning 7737: (116-182): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
+// Warning 6328: (185-200): CHC: Assertion violation happens here.\nCounterexample:\nz = 0\n\nTransaction trace:\nC.constructor()\nState: z = 0\nC.f()
+// Warning 6328: (219-233): CHC: Assertion violation happens here.\nCounterexample:\nz = 0\n\nTransaction trace:\nC.constructor()\nState: z = 0\nC.f()
+// Warning 7737: (116-182): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).

test/libsolidity/smtCheckerTests/inline_assembly/assembly_local_storage_pointer.sol

@@ -0,0 +1,25 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint256[] public a;
+
+	function f() public {
+		require(a.length == 0);
+		uint256[] storage x = a;
+		assert(x.length == 0); // should hold
+		uint256 i = 7;
+		assembly {
+			sstore(x.slot, 7)
+		}
+		assert(x.length == 0); // should fail
+		assert(x.length == 7); // should hold, but the analysis cannot know this yet
+		assert(i == 7); // should hold, not changed by the assembly
+	}
+}
+// ====
+// SMTIgnoreCex: yes
+// ----
+// Warning 7737: (203-238): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
+// Warning 6328: (241-262): CHC: Assertion violation happens here.
+// Warning 6328: (281-302): CHC: Assertion violation happens here.
+// Warning 7737: (203-238): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).

test/libsolidity/smtCheckerTests/inline_assembly/assembly_memory_write.sol

@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+	}
+
+	S s;
+
+	function f() public {
+		s.x = 42;
+		S memory sm = s;
+		assert(sm.x == 42); // should hold
+		uint256 i = 7;
+		assembly {
+			mstore(sm, i)
+		}
+		assert(sm.x == 42); // should fail
+		assert(sm.x == 7); // should hold, but the analysis cannot know this yet
+		assert(s.x == 42); // should hold, storage not changed by the assembly
+		assert(i == 7); // should hold, not changed by the assembly
+	}
+}
+// ----
+// Warning 7737: (189-220): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
+// Warning 6328: (223-241): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 42}\n\nTransaction trace:\nC.constructor()\nState: s = {x: 0}\nC.f()
+// Warning 6328: (260-277): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 42}\n\nTransaction trace:\nC.constructor()\nState: s = {x: 0}\nC.f()
+// Warning 7737: (189-220): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).

test/libsolidity/smtCheckerTests/inline_assembly/empty.sol

@@ -8,5 +8,5 @@ contract C
 	}
 }
 // ----
-// Warning 7737: (76-90): Assertion checker does not support inline assembly.
-// Warning 7737: (76-90): Assertion checker does not support inline assembly.
+// Warning 7737: (76-90): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
+// Warning 7737: (76-90): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).

test/libsolidity/smtCheckerTests/inline_assembly/local_var.sol

@@ -10,5 +10,5 @@ contract C
 	}
 }
 // ----
-// Warning 7737: (97-121): Assertion checker does not support inline assembly.
-// Warning 7737: (97-121): Assertion checker does not support inline assembly.
+// Warning 7737: (97-121): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
+// Warning 7737: (97-121): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).