[SMTChecker] Support unary inc/dec for array/mapping access

Changelog.md

@@ -5,6 +5,7 @@ Language Features:
 
 Compiler Features:
  * SMTChecker: Support arithmetic compound assignment operators.
+ * SMTChecker: Support unary increment and decrement for array and mapping access.
  * Optimizer: Add rule for shifts by constants larger than 255 for Constantinople.
  * Optimizer: Add rule to simplify certain ANDs and SHL combinations
  * Yul: Adds break and continue keywords to for-loop syntax.

libsolidity/formal/SMTChecker.cpp

@@ -386,7 +386,7 @@ void SMTChecker::endVisit(Assignment const& _assignment)
 		if (identifier)
 			assignment(*decl, _assignment, _assignment.location());
 		else
-			arrayIndexAssignment(_assignment, expr(_assignment));
+			arrayIndexAssignment(_assignment.leftHandSide(), expr(_assignment));
 	}
 	else
 		m_errorReporter.warning(
@@ -485,21 +485,22 @@ void SMTChecker::endVisit(UnaryOperation const& _op)
 
 		solAssert(isInteger(_op.annotation().type->category()), "");
 		solAssert(_op.subExpression().annotation().lValueRequested, "");
-		if (Identifier const* identifier = dynamic_cast<Identifier const*>(&_op.subExpression()))
+		if (auto identifier = dynamic_cast<Identifier const*>(&_op.subExpression()))
 		{
-			VariableDeclaration const& decl = dynamic_cast<VariableDeclaration const&>(*identifier->annotation().referencedDeclaration);
+			auto decl = dynamic_cast<VariableDeclaration const*>(identifier->annotation().referencedDeclaration);
-			if (knownVariable(decl))
+			solAssert(decl, "");
-			{
+			solAssert(knownVariable(*decl), "");
-				auto innerValue = currentValue(decl);
+			auto innerValue = currentValue(*decl);
-				auto newValue = _op.getOperator() == Token::Inc ? innerValue + 1 : innerValue - 1;
+			auto newValue = _op.getOperator() == Token::Inc ? innerValue + 1 : innerValue - 1;
-				assignment(decl, newValue, _op.location());
+			defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue);
-				defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue);
+			assignment(*decl, newValue, _op.location());
-			}
+		}
-			else
+		else if (dynamic_cast<IndexAccess const*>(&_op.subExpression()))
-				m_errorReporter.warning(
+		{
-					_op.location(),
+			auto innerValue = expr(_op.subExpression());
-					"Assertion checker does not yet implement such assignments."
+			auto newValue = _op.getOperator() == Token::Inc ? innerValue + 1 : innerValue - 1;
-				);
+			defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue);
+			arrayIndexAssignment(_op.subExpression(), newValue);
 		}
 		else
 			m_errorReporter.warning(
@@ -911,9 +912,9 @@ void SMTChecker::arrayAssignment()
 	m_arrayAssignmentHappened = true;
 }
 
-void SMTChecker::arrayIndexAssignment(Assignment const& _assignment, smt::Expression const& _rightHandSide)
+void SMTChecker::arrayIndexAssignment(Expression const& _expr, smt::Expression const& _rightHandSide)
 {
-	auto const& indexAccess = dynamic_cast<IndexAccess const&>(_assignment.leftHandSide());
+	auto const& indexAccess = dynamic_cast<IndexAccess const&>(_expr);
 	if (auto const& id = dynamic_cast<Identifier const*>(&indexAccess.baseExpression()))
 	{
 		auto const& varDecl = dynamic_cast<VariableDeclaration const&>(*id->annotation().referencedDeclaration);
@@ -968,7 +969,7 @@ void SMTChecker::arrayIndexAssignment(Assignment const& _assignment, smt::Expres
 		);
 	else
 		m_errorReporter.warning(
-			_assignment.location(),
+			_expr.location(),
 			"Assertion checker does not yet implement this expression."
 		);
 }

libsolidity/formal/SMTChecker.h

@@ -127,7 +127,7 @@ private:
 	/// while aliasing is not supported.
 	void arrayAssignment();
 	/// Handles assignment to SMT array index.
-	void arrayIndexAssignment(Assignment const& _assignment, smt::Expression const& _rightHandSide);
+	void arrayIndexAssignment(Expression const& _expr, smt::Expression const& _rightHandSide);
 
 	/// Division expression in the given type. Requires special treatment because
 	/// of rounding for signed division.

test/libsolidity/smtCheckerTests/operators/unary_add.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		uint x = 2;
+		uint a = ++x;
+		assert(x == 3);
+		assert(a == 3);
+		uint b = x++;
+		assert(x == 4);
+		// Should fail.
+		assert(b < 3);
+	}
+}
+// ----
+// Warning: (194-207): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/unary_add_array.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[] array;
+	function f(uint x) public {
+		array[x] = 2;
+		uint a = ++array[x];
+		assert(array[x] == 3);
+		assert(a == 3);
+		uint b = array[x]++;
+		assert(array[x] == 4);
+		// Should fail.
+		assert(b < 3);
+	}
+}
+// ----
+// Warning: (240-253): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/unary_add_mapping.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	mapping (uint => uint) map;
+	function f(uint x) public {
+		map[x] = 2;
+		uint a = ++map[x];
+		assert(map[x] == 3);
+		assert(a == 3);
+		uint b = map[x]++;
+		assert(map[x] == 4);
+		// Should fail.
+		assert(b < 3);
+	}
+}
+// ----
+// Warning: (244-257): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/unary_sub.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		uint x = 5;
+		uint a = --x;
+		assert(x == 4);
+		assert(a == 4);
+		uint b = x--;
+		assert(x == 3);
+		// Should fail.
+		assert(b > 4);
+	}
+}
+// ----
+// Warning: (194-207): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/unary_sub_array.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[] array;
+	function f(uint x) public {
+		array[x] = 5;
+		uint a = --array[x];
+		assert(array[x] == 4);
+		assert(a == 4);
+		uint b = array[x]--;
+		assert(array[x] == 3);
+		// Should fail.
+		assert(b > 4);
+	}
+}
+// ----
+// Warning: (240-253): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/unary_sub_mapping.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	mapping (uint => uint) map;
+	function f(uint x) public {
+		map[x] = 5;
+		uint a = --map[x];
+		assert(map[x] == 4);
+		assert(a == 4);
+		uint b = map[x]--;
+		assert(map[x] == 3);
+		// Should fail.
+		assert(b > 4);
+	}
+}
+// ----
+// Warning: (244-257): Assertion violation happens here