[SMTChecker] Fix internal error when array.push() is used as LHS of assignment

Changelog.md

@@ -13,6 +13,7 @@ Bugfixes:
  * SMTChecker: Fix incorrect counterexamples reported by the CHC engine.
  * SMTChecker: Fix false negative in modifier applied multiple times.
  * SMTChecker: Fix internal error in the BMC engine when inherited contract from a different source unit has private state variables.
+ * SMTChecker: Fix internal error when ``array.push()`` is used as the LHS of an assignment.
  * Code generator: Fix missing creation dependency tracking for abstract contracts.
 
 

libsolidity/formal/SMTEncoder.cpp

@@ -348,6 +348,36 @@ void SMTEncoder::endVisit(VariableDeclarationStatement const& _varDecl)
 
 }
 
+bool SMTEncoder::visit(Assignment const& _assignment)
+{
+	auto const& left = _assignment.leftHandSide();
+	auto const& right = _assignment.rightHandSide();
+
+	if (auto const* memberAccess = isEmptyPush(left))
+	{
+		right.accept(*this);
+		left.accept(*this);
+
+		auto const& memberExpr = memberAccess->expression();
+		auto& symbArray = dynamic_cast<smt::SymbolicArrayVariable&>(*m_context.expression(memberExpr));
+		smtutil::Expression oldElements = symbArray.elements();
+		smtutil::Expression length = symbArray.length();
+		symbArray.increaseIndex();
+		m_context.addAssertion(symbArray.elements() == smtutil::Expression::store(
+			oldElements,
+			length - 1,
+			expr(right)
+		));
+		m_context.addAssertion(symbArray.length() == length);
+
+		arrayPushPopAssign(memberExpr, symbArray.currentValue());
+		defineExpr(_assignment, expr(left));
+		return false;
+	}
+
+	return true;
+}
+
 void SMTEncoder::endVisit(Assignment const& _assignment)
 {
 	createExpr(_assignment);
@@ -355,6 +385,9 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
 	Token op = _assignment.assignmentOperator();
 	solAssert(TokenTraits::isAssignmentOp(op), "");
 
+	if (isEmptyPush(_assignment.leftHandSide()))
+		return;
+
 	if (!smt::isSupportedType(*_assignment.annotation().type))
 	{
 		// Give it a new index anyway to keep the SSA scheme sound.
@@ -465,14 +498,14 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
 			assignment(*decl, newValue);
 		}
 		else if (
-			dynamic_cast<IndexAccess const*>(&_op.subExpression()) ||
-			dynamic_cast<MemberAccess const*>(&_op.subExpression())
+			dynamic_cast<IndexAccess const*>(subExpr) ||
+			dynamic_cast<MemberAccess const*>(subExpr)
 		)
 		{
 			auto innerValue = expr(*subExpr);
 			auto newValue = _op.getOperator() == Token::Inc ? innerValue + 1 : innerValue - 1;
 			defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue);
-			indexOrMemberAssignment(_op.subExpression(), newValue);
+			indexOrMemberAssignment(*subExpr, newValue);
 		}
 		else
 			m_errorReporter.warning(
@@ -502,11 +535,12 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
 			symbVar->increaseIndex();
 			m_context.setZeroValue(*symbVar);
 			if (
-				dynamic_cast<IndexAccess const*>(&_op.subExpression()) ||
-				dynamic_cast<MemberAccess const*>(&_op.subExpression())
+				dynamic_cast<IndexAccess const*>(subExpr) ||
+				dynamic_cast<MemberAccess const*>(subExpr)
 			)
-				indexOrMemberAssignment(_op.subExpression(), symbVar->currentValue());
-			else
+				indexOrMemberAssignment(*subExpr, symbVar->currentValue());
+			// Empty push added a zero value anyway, so no need to delete extra.
+			else if (!isEmptyPush(*subExpr))
 				solAssert(false, "");
 		}
 		break;
@@ -2314,7 +2348,7 @@ set<VariableDeclaration const*> SMTEncoder::touchedVariables(ASTNode const& _nod
 	return m_variableUsage.touchedVariables(_node, callStack);
 }
 
-Declaration const* SMTEncoder::expressionToDeclaration(Expression const& _expr)
+Declaration const* SMTEncoder::expressionToDeclaration(Expression const& _expr) const
 {
 	if (auto const* identifier = dynamic_cast<Identifier const*>(&_expr))
 		return identifier->annotation().referencedDeclaration;
@@ -2323,7 +2357,7 @@ Declaration const* SMTEncoder::expressionToDeclaration(Expression const& _expr)
 	return nullptr;
 }
 
-VariableDeclaration const* SMTEncoder::identifierToVariable(Expression const& _expr)
+VariableDeclaration const* SMTEncoder::identifierToVariable(Expression const& _expr) const
 {
 	// We do not use `expressionToDeclaration` here because we are not interested in
 	// struct.field, for example.
@@ -2336,6 +2370,20 @@ VariableDeclaration const* SMTEncoder::identifierToVariable(Expression const& _e
 	return nullptr;
 }
 
+MemberAccess const* SMTEncoder::isEmptyPush(Expression const& _expr) const
+{
+	if (
+		auto const* funCall = dynamic_cast<FunctionCall const*>(&_expr);
+		funCall && funCall->arguments().empty()
+	)
+	{
+		auto const& funType = dynamic_cast<FunctionType const&>(*funCall->expression().annotation().type);
+		if (funType.kind() == FunctionType::Kind::ArrayPush)
+			return &dynamic_cast<MemberAccess const&>(funCall->expression());
+	}
+	return nullptr;
+}
+
 string SMTEncoder::extraComment()
 {
 	string extra;

libsolidity/formal/SMTEncoder.h

@@ -90,6 +90,7 @@ protected:
 	bool visit(WhileStatement const&) override { return false; }
 	bool visit(ForStatement const&) override { return false; }
 	void endVisit(VariableDeclarationStatement const& _node) override;
+	bool visit(Assignment const& _node) override;
 	void endVisit(Assignment const& _node) override;
 	void endVisit(TupleExpression const& _node) override;
 	bool visit(UnaryOperation const& _node) override;
@@ -282,10 +283,14 @@ protected:
 
 	/// @returns the declaration referenced by _expr, if any,
 	/// and nullptr otherwise.
-	Declaration const* expressionToDeclaration(Expression const& _expr);
+	Declaration const* expressionToDeclaration(Expression const& _expr) const;
 
 	/// @returns the VariableDeclaration referenced by an Expression or nullptr.
-	VariableDeclaration const* identifierToVariable(Expression const& _expr);
+	VariableDeclaration const* identifierToVariable(Expression const& _expr) const;
+
+	/// @returns the MemberAccess <expression>.push if _expr is an empty array push call,
+	/// otherwise nullptr.
+	MemberAccess const* isEmptyPush(Expression const& _expr) const;
 
 	/// Creates symbolic expressions for the returned values
 	/// and set them as the components of the symbolic tuple.

libsolidity/formal/SymbolicVariables.cpp

@@ -332,12 +332,12 @@ smtutil::Expression SymbolicArrayVariable::valueAtIndex(unsigned _index) const
 	return m_pair.valueAtIndex(_index);
 }
 
-smtutil::Expression SymbolicArrayVariable::elements()
+smtutil::Expression SymbolicArrayVariable::elements() const
 {
 	return m_pair.component(0);
 }
 
-smtutil::Expression SymbolicArrayVariable::length()
+smtutil::Expression SymbolicArrayVariable::length() const
 {
 	return m_pair.component(1);
 }

libsolidity/formal/SymbolicVariables.h

@@ -260,8 +260,8 @@ public:
 	smtutil::Expression resetIndex() override { SymbolicVariable::resetIndex(); return m_pair.resetIndex(); }
 	smtutil::Expression setIndex(unsigned _index) override { SymbolicVariable::setIndex(_index); return m_pair.setIndex(_index); }
 	smtutil::Expression increaseIndex() override { SymbolicVariable::increaseIndex(); return m_pair.increaseIndex(); }
-	smtutil::Expression elements();
-	smtutil::Expression length();
+	smtutil::Expression elements() const;
+	smtutil::Expression length() const;
 
 	smtutil::SortPointer tupleSort() { return m_pair.sort(); }
 

test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[] b;
+
+	function f() public {
+		require(b.length == 0);
+		b.push() = 1;
+		assert(b[0] == 1);
+	}
+
+	function g() public {
+		b.push() = 1;
+		assert(b[b.length - 1] == 1);
+		// Fails
+		assert(b[b.length - 1] == 100);
+	}
+
+}
+// ----
+// Warning 6328: (232-262): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/array_members/push_as_lhs_2d.sol

@@ -0,0 +1,24 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[][] c;
+
+	function f() public {
+		require(c.length == 0);
+		c.push().push() = 2;
+		assert(c.length == 1);
+		assert(c[0].length == 1);
+		assert(c[0][0] == 2);
+	}
+
+	function g() public {
+		c.push().push() = 2;
+		assert(c.length > 0);
+		assert(c[c.length - 1].length == 1);
+		assert(c[c.length - 1][c[c.length - 1].length - 1] == 2);
+		// Fails
+		assert(c[c.length - 1][c[c.length - 1].length - 1] == 200);
+	}
+}
+// ----
+// Warning 6328: (395-453): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/array_members/push_as_lhs_2d_2.sol

@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+contract C {
+	int[][] array2d;
+	function s() public returns (int[] memory) {
+		array2d.push() = array2d.push();
+		assert(array2d[array2d.length - 1].length == array2d[array2d.length - 2].length);
+		return array2d[2];
+	}
+}

test/libsolidity/smtCheckerTests/array_members/push_as_lhs_3d.sol

@@ -0,0 +1,30 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[][][] c;
+
+	function f() public {
+		require(c.length == 0);
+		c.push().push().push() = 2;
+		assert(c.length == 1);
+		assert(c[0].length == 1);
+		assert(c[0][0].length == 1);
+		assert(c[0][0][0] == 2);
+	}
+
+	function g() public {
+		c.push().push().push() = 2;
+		uint length1 = c.length;
+		uint length2 = c[length1 - 1].length;
+		uint length3 = c[length1 - 1][length2 - 1].length;
+		assert(length1 > 0);
+		assert(length2 == 1);
+		assert(length3 == 1);
+		assert(c[length1 - 1][length2 - 1][length3 - 1] == 2);
+		// Fails
+		assert(c[length1 - 1][length2 - 1][length3 - 1] == 200);
+	}
+}
+// ----
+// Warning 6328: (570-625): CHC: Assertion violation might happen here.
+// Warning 4661: (570-625): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_1d.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[] 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] == 1);
+	}
+}
+// ----
+// Warning 6328: (237-263): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_2d_1.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[][] b;
+	function f() public {
+		require(b.length == 0);
+		b.push().push() = b.push().push();
+		assert(b.length == 2);
+		assert(b[0].length == 1);
+		assert(b[0].length == 1);
+		assert(b[0][0] == 0);
+		assert(b[1][0] == 0);
+		assert(b[0][0] == b[1][0]);
+		// Fails
+		assert(b[0][0] != b[1][0]);
+	}
+}
+// ----
+// Warning 6328: (317-343): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_2d_2.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[][] b;
+	function f() public {
+		b.push().push() = b.push().push();
+		uint length = b.length;
+		assert(length >= 2);
+		uint length1 = b[length - 1].length;
+		uint length2 = b[length - 2].length;
+		assert(length1 == 1);
+		assert(length2 == 1);
+		assert(b[length - 1][length1 - 1] == 0);
+	}
+}

test/libsolidity/smtCheckerTests/array_members/push_as_lhs_struct.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+contract C {
+	struct S {
+		int[] b;
+	}
+	S s;
+	struct T {
+		S s;
+	}
+	T t;
+	function f() public {
+		s.b.push() = t.s.b.push();
+		assert(s.b[s.b.length -1] == t.s.b[t.s.b.length - 1]);
+	}
+}

test/libsolidity/smtCheckerTests/operators/delete_array_push.sol

@@ -0,0 +1,20 @@
+pragma experimental SMTChecker;
+contract C {
+	int[][] array2d;
+	function s() public returns (int[] memory) {
+		delete array2d.push();
+		assert(array2d[array2d.length - 1].length == 0);
+		// Fails
+		assert(array2d[array2d.length - 1].length != 0);
+		delete array2d.push().push();
+		uint length = array2d.length;
+		uint length2 = array2d[length - 1].length;
+		assert(array2d[length - 1][length2 - 1] == 0);
+		// Fails
+		assert(array2d[length - 1][length2 - 1] != 0);
+		return array2d[2];
+	}
+}
+// ----
+// Warning 6328: (198-245): CHC: Assertion violation happens here.
+// Warning 6328: (418-463): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/delete_tuple.sol

@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+
+contract A{
+	function f() public pure {
+		delete ([""][0]);
+	}
+}