Merge pull request #10380 from ethereum/smtLogicErrorInt2Bv

[SMTChecker] Fix SMT logic error when doing compound assignment with string literals

Changelog.md

@@ -8,6 +8,8 @@ Compiler Features:
  * SMTChecker: Support named arguments in function calls.
  * SMTChecker: Support struct constructor.
 
+Bugfixes:
+ * SMTChecker: Fix internal compiler error when doing bitwise compound assignment with string literals.
 
 ### 0.7.5 (2020-11-18)
 

libsolidity/formal/SMTEncoder.cpp

@@ -1927,18 +1927,24 @@ smtutil::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment
 
 	auto decl = identifierToVariable(_assignment.leftHandSide());
 
+	TypePointer commonType = Type::commonType(
+		_assignment.leftHandSide().annotation().type,
+		_assignment.rightHandSide().annotation().type
+	);
+	solAssert(commonType == _assignment.annotation().type, "");
+
 	if (compoundToBitwise.count(op))
 		return bitwiseOperation(
 			compoundToBitwise.at(op),
-			decl ? currentValue(*decl) : expr(_assignment.leftHandSide()),
-			expr(_assignment.rightHandSide()),
+			decl ? currentValue(*decl) : expr(_assignment.leftHandSide(), _assignment.annotation().type),
+			expr(_assignment.rightHandSide(), _assignment.annotation().type),
 			_assignment.annotation().type
 		);
 
 	auto values = arithmeticOperation(
 		compoundToArithmetic.at(op),
-		decl ? currentValue(*decl) : expr(_assignment.leftHandSide()),
-		expr(_assignment.rightHandSide()),
+		decl ? currentValue(*decl) : expr(_assignment.leftHandSide(), _assignment.annotation().type),
+		expr(_assignment.rightHandSide(), _assignment.annotation().type),
 		_assignment.annotation().type,
 		_assignment
 	);

test/libsolidity/smtCheckerTests/operators/compound_bitwise_string_literal.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f() public pure {
+        bytes memory y = "def";
+        y[0] &= "d";
+        assert(y[0] == "d");
+
+        y[0] |= "e";
+        assert(y[0] == "d"); // fails
+
+        y[0] ^= "f";
+        assert(y[0] == (byte("d") | byte("e")) ^ byte("f"));
+    }
+}
+// ----
+// Warning 6328: (189-208): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_string_literal_2.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f() public pure {
+        bytes3 y = "def";
+        y &= "def";
+        assert(y == "def");
+
+        y |= "dee";
+        assert(y == "def"); // fails
+
+        y ^= "fed";
+        assert(y == (bytes3("def") | bytes3("dee")) ^ bytes3("fed"));
+    }
+}
+// ----
+// Warning 6328: (180-198): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_string_literal_3.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f() public pure {
+        bytes32 y = "abcdefghabcdefghabcdefghabcdefgh";
+        bytes32 z = y;
+        y &= "bcdefghabcdefghabcdefghabcdefgha";
+        z &= "bcdefghabcdefghabcdefghabcdefgha";
+        assert(y == "abcdefghabcdefghabcdefghabcdefgh"); // fails
+
+        y |= "cdefghabcdefghabcdefghabcdefghab";
+        z |= "cdefghabcdefghabcdefghabcdefghab";
+        assert(y == "abcdefghabcdefghabcdefghabcd"); // fails
+
+        y ^= "abcdefghabcdefghabcdefghabcdefgh";
+        assert(y == z ^ "abcdefghabcdefghabcdefghabcdefgh");
+    }
+}
+// ----
+// Warning 6328: (262-309): CHC: Assertion violation happens here.
+// Warning 6328: (427-470): CHC: Assertion violation happens here.