[SMTChecker] Fixed crash on push to bytes on lhs of an assignment

Changelog.md

@@ -25,6 +25,7 @@ Bugfixes:
  * SMTChecker: Fix internal compiler error when doing bitwise compound assignment with string literals.
  * SMTChecker: Fix internal error when trying to generate counterexamples with old z3.
  * SMTChecker: Fix segmentation fault that could occur on certain SMT-enabled sources when no SMT solver was available.
+ * SMTChecker: Fix internal error when ``bytes.push()`` is used as the LHS of an assignment.
  * Type Checker: ``super`` is not available in libraries.
  * Type Checker: Disallow leading zeroes in sized-types (e.g. ``bytes000032``), but allow them to be treated as identifiers.
  * Yul Optimizer: Fix a bug in NameSimplifier where a new name created by NameSimplifier could also be created by NameDispenser.

libsolidity/formal/SMTEncoder.cpp

@@ -709,6 +709,7 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 		break;
 	}
 	case FunctionType::Kind::ArrayPush:
+	case FunctionType::Kind::ByteArrayPush:
 		arrayPush(_funCall);
 		break;
 	case FunctionType::Kind::ArrayPop:
@@ -1572,6 +1573,8 @@ void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression
 	else if (auto const* funCall = dynamic_cast<FunctionCall const*>(expr))
 	{
 		FunctionType const& funType = dynamic_cast<FunctionType const&>(*funCall->expression().annotation().type);
+		// Push cannot occur on an expression that is itself a ByteArrayPush, i.e., bytes.push().push() is not possible.
+		solAssert(funType.kind() != FunctionType::Kind::ByteArrayPush, "");
 		if (funType.kind() == FunctionType::Kind::ArrayPush)
 		{
 			auto memberAccess = dynamic_cast<MemberAccess const*>(&funCall->expression());
@@ -2499,7 +2502,7 @@ MemberAccess const* SMTEncoder::isEmptyPush(Expression const& _expr) const
 	)
 	{
 		auto const& funType = dynamic_cast<FunctionType const&>(*funCall->expression().annotation().type);
-		if (funType.kind() == FunctionType::Kind::ArrayPush)
+		if (funType.kind() == FunctionType::Kind::ArrayPush || funType.kind() == FunctionType::Kind::ByteArrayPush)
 			return &dynamic_cast<MemberAccess const&>(funCall->expression());
 	}
 	return nullptr;

test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_bytes.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C {
+	bytes b;
+	function f() public {
+		b.push() = b.push();
+		uint length = b.length;
+		assert(length >= 2);
+		assert(b[length - 1] == 0);
+		assert(b[length - 1] == b[length - 2]);
+		// Fails
+		assert(b[length - 1] == byte(uint8(1)));
+	}
+}
+// ----
+// Warning 6328: (236-275): CHC: Assertion violation happens here.\nCounterexample:\nb = [0, 0]\n\n\n\nTransaction trace:\nconstructor()\nState: b = []\nf()

test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes.sol

@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+
+contract C {
+	bytes b;
+
+	function f() public {
+		require(b.length == 0);
+		b.push() = byte(uint8(1));
+		assert(b[0] == byte(uint8(1)));
+	}
+
+	function g() public {
+		byte one = byte(uint8(1));
+		b.push() = one;
+		assert(b[b.length - 1] == one);
+		// Fails
+		assert(b[b.length - 1] == byte(uint8(100)));
+	}
+
+}
+// ----
+// Warning 6328: (290-333): CHC: Assertion violation happens here.\nCounterexample:\nb = [1]\n\n\n\nTransaction trace:\nconstructor()\nState: b = []\ng()

test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes_2d.sol

@@ -0,0 +1,26 @@
+pragma experimental SMTChecker;
+
+contract C {
+	bytes[] c;
+
+	function f() public {
+		bytes1 val = bytes1(uint8(2));
+		require(c.length == 0);
+		c.push().push() = val;
+		assert(c.length == 1);
+		assert(c[0].length == 1);
+		assert(c[0][0] == val);
+	}
+
+	function g() public {
+		bytes1 val = bytes1(uint8(2));
+		c.push().push() = val;
+		assert(c.length > 0);
+		assert(c[c.length - 1].length == 1);
+		assert(c[c.length - 1][c[c.length - 1].length - 1] == val);
+		// Fails
+		assert(c[c.length - 1][c[c.length - 1].length - 1] == bytes1(uint8(100)));
+	}
+}
+// ----
+// Warning 6328: (468-541): CHC: Assertion violation happens here.\nCounterexample:\nc = [[2]]\n\n\n\nTransaction trace:\nconstructor()\nState: c = []\ng()