Merge pull request #10835 from blishko/smt-assembly

[SMTChecker] Basic support for inline assembly that over-approximates its effects.

Changelog.md

@@ -24,6 +24,7 @@ Bugfixes:
  * Code Generator: Fix length check when decoding malformed error data in catch clause.
  * Control Flow Graph: Fix missing error caused by read from/write to uninitialized variables.
  * SMTChecker: Fix false negatives in overriding modifiers and functions.
+ * SMTChecker: Fix false negatives in the presence of inline assembly.
  * SMTChecker: Fix false negatives when analyzing external function calls.
  * SMTChecker: Fix internal error on ``block.chainid``.
  * SMTChecker: Fix internal error on pushing string literal to ``bytes`` array.

libsolidity/formal/SMTEncoder.cpp

@@ -24,6 +24,9 @@
 
 #include <libsolidity/analysis/ConstantEvaluator.h>
 
+#include <libyul/AST.h>
+#include <libyul/optimiser/Semantics.h>
+
 #include <libsmtutil/SMTPortfolio.h>
 #include <libsmtutil/Helpers.h>
 
@@ -304,10 +307,46 @@ void SMTEncoder::endVisit(Block const& _block)
 
 bool SMTEncoder::visit(InlineAssembly const& _inlineAsm)
 {
+	/// This is very similar to `yul::Assignments`, except I need to collect `Identifier`s and not just names as `YulString`s.
+	struct AssignedExternalsCollector: public yul::ASTWalker
+	{
+		AssignedExternalsCollector(InlineAssembly const& _inlineAsm): externalReferences(_inlineAsm.annotation().externalReferences)
+		{
+			this->operator()(_inlineAsm.operations());
+		}
+
+		map<yul::Identifier const*, InlineAssemblyAnnotation::ExternalIdentifierInfo> const& externalReferences;
+		set<VariableDeclaration const*> assignedVars;
+
+		using yul::ASTWalker::operator();
+		void operator()(yul::Assignment const& _assignment)
+		{
+			auto const& vars = _assignment.variableNames;
+			for (auto const& identifier: vars)
+				if (auto externalInfo = valueOrNullptr(externalReferences, &identifier))
+					if (auto varDecl = dynamic_cast<VariableDeclaration const*>(externalInfo->declaration))
+						assignedVars.insert(varDecl);
+		}
+	};
+
+	yul::SideEffectsCollector sideEffectsCollector(_inlineAsm.dialect(), _inlineAsm.operations());
+	if (sideEffectsCollector.invalidatesMemory())
+		resetMemoryVariables();
+	if (sideEffectsCollector.invalidatesStorage())
+		resetStorageVariables();
+
+	auto assignedVars = AssignedExternalsCollector(_inlineAsm).assignedVars;
+	for (auto const* var: assignedVars)
+	{
+		solAssert(var, "");
+		solAssert(var->isLocalVariable(), "Non-local variable assigned in inlined assembly");
+		m_context.resetVariable(*var);
+	}
+
 	m_errorReporter.warning(
 		7737_error,
 		_inlineAsm.location(),
-		"Assertion checker does not support inline assembly."
+		"Inline assembly may cause SMTChecker to produce spurious warnings (false positives)."
 	);
 	return false;
 }
@@ -2256,6 +2295,20 @@ void SMTEncoder::resetStateVariables()
 	m_context.resetVariables([&](VariableDeclaration const& _variable) { return _variable.isStateVariable(); });
 }
 
+void SMTEncoder::resetMemoryVariables()
+{
+	m_context.resetVariables([&](VariableDeclaration const& _variable) {
+		return _variable.referenceLocation() == VariableDeclaration::Location::Memory;
+	});
+}
+
+void SMTEncoder::resetStorageVariables()
+{
+	m_context.resetVariables([&](VariableDeclaration const& _variable) {
+		return _variable.referenceLocation() == VariableDeclaration::Location::Storage || _variable.isStateVariable();
+	});
+}
+
 void SMTEncoder::resetReferences(VariableDeclaration const& _varDecl)
 {
 	m_context.resetVariables([&](VariableDeclaration const& _var) {

libsolidity/formal/SMTEncoder.h

@@ -260,6 +260,8 @@ protected:
 	void initializeLocalVariables(FunctionDefinition const& _function);
 	void initializeFunctionCallParameters(CallableDeclaration const& _function, std::vector<smtutil::Expression> const& _callArgs);
 	void resetStateVariables();
+	void resetStorageVariables();
+	void resetMemoryVariables();
 	/// Resets all references/pointers that have the same type or have
 	/// a subexpression of the same type as _varDecl.
 	void resetReferences(VariableDeclaration const& _varDecl);

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).