Merge pull request #7171 from ethereum/smt_fix_compound_bitwise

[SMTChecker] Fix ICE compound bitwise op inside branch

Changelog.md

@@ -21,6 +21,7 @@ Compiler Features:
 Bugfixes:
  * SMTChecker: Fix internal error when inlining functions that contain tuple expressions.
  * SMTChecker: Fix pointer knowledge erasing in loops.
+ * SMTChecker: Fix internal error when using compound bitwise assignment operators inside branches.
  * View/Pure Checker: Properly detect state variable access through base class.
  * Yul analyzer: Check availability of data objects already in analysis phase.
  * Yul Optimizer: Fix an issue where memory-accessing code was removed even though ``msize`` was used in the program.

libsolidity/formal/SMTEncoder.cpp

@@ -214,10 +214,16 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
 	};
 	Token op = _assignment.assignmentOperator();
 	if (op != Token::Assign && !compoundOps.count(op))
+	{
+		// Give it a new index anyway to keep the SSA scheme sound.
+		if (auto varDecl = identifierToVariable(_assignment.leftHandSide()))
+			m_context.newValue(*varDecl);
+
 		m_errorReporter.warning(
 			_assignment.location(),
 			"Assertion checker does not yet implement this assignment operator."
 		);
+	}
 	else if (!smt::isSupportedType(_assignment.annotation().type->category()))
 	{
 		// Give it a new index anyway to keep the SSA scheme sound.
@@ -1031,10 +1037,16 @@ void SMTEncoder::assignment(
 )
 {
 	if (!smt::isSupportedType(_type->category()))
+	{
+		// Give it a new index anyway to keep the SSA scheme sound.
+		if (auto varDecl = identifierToVariable(_left))
+			m_context.newValue(*varDecl);
+
 		m_errorReporter.warning(
 			_location,
 			"Assertion checker does not yet implement type " + _type->toString()
 		);
+	}
 	else if (auto varDecl = identifierToVariable(_left))
 	{
 		solAssert(_right.size() == 1, "");

test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_1.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f(bool b) public pure {
+		uint v = 1;
+		if (b)
+			v &= 1;
+		assert(v == 1);
+	}
+}
+// ----
+// Warning: (106-112): Assertion checker does not yet implement this assignment operator.
+// Warning: (116-130): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_1.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f(bool b) public pure {
+		uint v = 0;
+		if (b)
+			v |= 1;
+		assert(v == 1);
+	}
+}
+// ----
+// Warning: (106-112): Assertion checker does not yet implement this assignment operator.
+// Warning: (116-130): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_1.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f(bool b) public pure {
+		uint v = 0;
+		if (b)
+			v ^= 1;
+		assert(v == 1);
+	}
+}
+// ----
+// Warning: (106-112): Assertion checker does not yet implement this assignment operator.
+// Warning: (116-130): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_shl_1.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f(bool b) public pure {
+		uint v = 1000000;
+		if (b)
+			v <<= 2;
+		assert(v > 0);
+	}
+}
+// ----
+// Warning: (112-119): Assertion checker does not yet implement this assignment operator.
+// Warning: (123-136): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_shr_1.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f(bool b) public pure {
+		uint v = 1;
+		if (b)
+			v >>= 2;
+		assert(v > 0);
+	}
+}
+// ----
+// Warning: (106-113): Assertion checker does not yet implement this assignment operator.
+// Warning: (117-130): Assertion violation happens here