Merge pull request #10111 from ethereum/smt_fix_assignment

[SMTChecker] Fix assignment to contract member access

Changelog.md

@@ -9,6 +9,7 @@ Bugfixes:
  * SMTChecker: Fix lack of reporting potential violations when using only the CHC engine.
  * SMTChecker: Fix internal error on conversion from string literal to byte.
  * SMTChecker: Fix internal error when using tuples of rational literals inside the conditional operator.
+ * SMTChecker: Fix internal error when assigning state variable via contract's name.
  * Code generator: Fix missing creation dependency tracking for abstract contracts.
 
 

libsolidity/formal/SMTEncoder.cpp

@@ -1061,10 +1061,9 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 
 	auto const& exprType = _memberAccess.expression().annotation().type;
 	solAssert(exprType, "");
-	auto identifier = dynamic_cast<Identifier const*>(&_memberAccess.expression());
 	if (exprType->category() == Type::Category::Magic)
 	{
-		if (identifier)
+		if (auto const* identifier = dynamic_cast<Identifier const*>(&_memberAccess.expression()))
 		{
 			auto const& name = identifier->name();
 			solAssert(name == "block" || name == "msg" || name == "tx", "");
@@ -1109,13 +1108,23 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 	}
 	else if (exprType->category() == Type::Category::TypeType)
 	{
-		if (identifier && dynamic_cast<EnumDefinition const*>(identifier->annotation().referencedDeclaration))
+		auto const* decl = expressionToDeclaration(_memberAccess.expression());
+		if (dynamic_cast<EnumDefinition const*>(decl))
 		{
 			auto enumType = dynamic_cast<EnumType const*>(accessType);
 			solAssert(enumType, "");
 			defineExpr(_memberAccess, enumType->memberValue(_memberAccess.memberName()));
+
+			return false;
+		}
+		else if (dynamic_cast<ContractDefinition const*>(decl))
+		{
+			if (auto const* var = dynamic_cast<VariableDeclaration const*>(_memberAccess.annotation().referencedDeclaration))
+			{
+				defineExpr(_memberAccess, currentValue(*var));
+				return false;
+			}
 		}
-		return false;
 	}
 	else if (exprType->category() == Type::Category::Address)
 	{
@@ -1245,6 +1254,23 @@ void SMTEncoder::arrayAssignment()
 
 void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide)
 {
+	if (auto const* memberAccess = dynamic_cast<MemberAccess const*>(&_expr))
+	{
+		if (dynamic_cast<ContractDefinition const*>(expressionToDeclaration(memberAccess->expression())))
+		{
+			if (auto const* var = dynamic_cast<VariableDeclaration const*>(memberAccess->annotation().referencedDeclaration))
+			{
+				if (var->hasReferenceOrMappingType())
+					resetReferences(*var);
+
+				m_context.addAssertion(m_context.newValue(*var) == _rightHandSide);
+				m_context.expression(_expr)->increaseIndex();
+				defineExpr(_expr, currentValue(*var));
+				return;
+			}
+		}
+	}
+
 	auto toStore = _rightHandSide;
 	auto const* lastExpr = &_expr;
 	while (true)
@@ -1306,7 +1332,7 @@ void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expre
 
 			m_context.addAssertion(m_context.newValue(*varDecl) == toStore);
 			m_context.expression(*id)->increaseIndex();
-			defineExpr(*id,currentValue(*varDecl));
+			defineExpr(*id, currentValue(*varDecl));
 			break;
 		}
 		else
@@ -2287,16 +2313,25 @@ set<VariableDeclaration const*> SMTEncoder::touchedVariables(ASTNode const& _nod
 	return m_variableUsage.touchedVariables(_node, callStack);
 }
 
+Declaration const* SMTEncoder::expressionToDeclaration(Expression const& _expr)
+{
+	if (auto const* identifier = dynamic_cast<Identifier const*>(&_expr))
+		return identifier->annotation().referencedDeclaration;
+	if (auto const* outerMemberAccess = dynamic_cast<MemberAccess const*>(&_expr))
+		return outerMemberAccess->annotation().referencedDeclaration;
+	return nullptr;
+}
+
 VariableDeclaration const* SMTEncoder::identifierToVariable(Expression const& _expr)
 {
-	if (auto identifier = dynamic_cast<Identifier const*>(&_expr))
-	{
-		if (auto decl = dynamic_cast<VariableDeclaration const*>(identifier->annotation().referencedDeclaration))
+	// We do not use `expressionToDeclaration` here because we are not interested in
+	// struct.field, for example.
+	if (auto const* identifier = dynamic_cast<Identifier const*>(&_expr))
+		if (auto const* varDecl = dynamic_cast<VariableDeclaration const*>(identifier->annotation().referencedDeclaration))
 		{
-			solAssert(m_context.knownVariable(*decl), "");
-			return decl;
+			solAssert(m_context.knownVariable(*varDecl), "");
+			return varDecl;
 		}
-	}
 	return nullptr;
 }
 

libsolidity/formal/SMTEncoder.h

@@ -280,7 +280,11 @@ protected:
 	/// @returns variables that are touched in _node's subtree.
 	std::set<VariableDeclaration const*> touchedVariables(ASTNode const& _node);
 
-	/// @returns the VariableDeclaration referenced by an Identifier or nullptr.
+	/// @returns the declaration referenced by _expr, if any,
+	/// and nullptr otherwise.
+	Declaration const* expressionToDeclaration(Expression const& _expr);
+
+	/// @returns the VariableDeclaration referenced by an Expression or nullptr.
 	VariableDeclaration const* identifierToVariable(Expression const& _expr);
 
 	/// Creates symbolic expressions for the returned values

test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol

@@ -0,0 +1,30 @@
+pragma experimental SMTChecker;
+contract A {
+	int x;
+	int y;
+	function a() public {
+		require(A.x < 100);
+		A.y = A.x++;
+		assert(A.y == A.x - 1);
+		// Fails
+		assert(A.y == 0);
+		A.y = ++A.x;
+		assert(A.y == A.x);
+		delete A.x;
+		assert(A.x == 0);
+		A.y = A.x--;
+		assert(A.y == A.x + 1);
+		assert(A.y == 0);
+		A.y = --A.x;
+		assert(A.y == A.x);
+		A.x += 10;
+		// Fails
+		assert(A.y == 0);
+		assert(A.y + 10 == A.x);
+		A.x -= 10;
+		assert(A.y == A.x);
+	}
+}
+// ----
+// Warning 6328: (160-176): CHC: Assertion violation happens here.
+// Warning 6328: (373-389): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract A {
+	uint[] a;
+	function f() public {
+		A.a.push(2);
+		assert(A.a[A.a.length - 1] == 2);
+		A.a.pop();
+		// Fails
+		assert(A.a.length > 0);
+		assert(A.a.length == 0);
+	}
+}
+// ----
+// Warning 6328: (156-178): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/assignment_module_contract_member_variable.sol

@@ -0,0 +1,31 @@
+==== Source: AASource ====
+pragma experimental SMTChecker;
+import "AASource" as AA;
+contract A {
+	int x;
+	int y;
+	function a() public {
+		require(A.x < 100);
+		AA.A.y = A.x++;
+		assert(A.y == AA.A.x - 1);
+		// Fails
+		assert(AA.A.y == 0);
+		A.y = ++AA.A.x;
+		assert(A.y == A.x);
+		delete AA.A.x;
+		assert(A.x == 0);
+		A.y = A.x--;
+		assert(AA.A.y == AA.A.x + 1);
+		A.y = --A.x;
+		assert(A.y == A.x);
+		AA.A.x += 10;
+		// Fails
+		assert(A.y == 0);
+		assert(A.y + 10 == A.x);
+		A.x -= 10;
+		assert(AA.A.y == A.x);
+	}
+}
+// ----
+// Warning 6328: (AASource:191-210): CHC: Assertion violation happens here.
+// Warning 6328: (AASource:402-418): CHC: Assertion violation happens here.