From 773e000227db1cdd9164d6d58a9f5c4c01c672fc Mon Sep 17 00:00:00 2001
From: Djordje Mijovic <djordje.mijovic@gmail.com>
Date: Mon, 21 Sep 2020 16:54:58 +0200
Subject: [PATCH] [SMTChecker] Implementing compound bitwise And/Or/Xor
 operators

---
 Changelog.md                      |   1 +
 libsolidity/formal/SMTEncoder.cpp | 114 +++++++++++++++++++++---------
 libsolidity/formal/SMTEncoder.h   |   8 +++
 3 files changed, 88 insertions(+), 35 deletions(-)

diff --git a/Changelog.md b/Changelog.md
index fb05610a5..c994a90f6 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -8,6 +8,7 @@ Compiler Features:
  * SMTChecker: Support events and low-level logs.
  * SMTChecker: Support ``revert()``.
  * SMTChecker: Support shifts.
+ * SMTChecker: Support compound and, or, and xor operators.
  * SMTChecker: Support structs.
  * SMTChecker: Support ``type(T).min``, ``type(T).max``, and ``type(I).interfaceId``.
  * Yul Optimizer: Prune unused parameters in functions.
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 90df7a908..f9c7cce50 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -357,7 +357,10 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
 		Token::AssignSub,
 		Token::AssignMul,
 		Token::AssignDiv,
-		Token::AssignMod
+		Token::AssignMod,
+		Token::AssignBitAnd,
+		Token::AssignBitOr,
+		Token::AssignBitXor
 	};
 	Token op = _assignment.assignmentOperator();
 	if (op != Token::Assign && !compoundOps.count(op))
@@ -1381,6 +1384,59 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
 	return {value, valueUnbounded};
 }
 
+smtutil::Expression SMTEncoder::bitwiseOperation(
+	Token _op,
+	smtutil::Expression const& _left,
+	smtutil::Expression const& _right,
+	TypePointer const& _commonType
+)
+{
+	static set<Token> validOperators{
+		Token::BitAnd,
+		Token::BitOr,
+		Token::BitXor,
+		Token::SHL,
+		Token::SHR,
+		Token::SAR
+	};
+	solAssert(validOperators.count(_op), "");
+	solAssert(_commonType, "");
+
+	auto [bvSize, isSigned] = smt::typeBvSizeAndSignedness(_commonType);
+
+	auto bvLeft = smtutil::Expression::int2bv(_left, bvSize);
+	auto bvRight = smtutil::Expression::int2bv(_right, bvSize);
+
+	optional<smtutil::Expression> result;
+	switch (_op)
+	{
+		case Token::BitAnd:
+			result = bvLeft & bvRight;
+			break;
+		case Token::BitOr:
+			result = bvLeft | bvRight;
+			break;
+		case Token::BitXor:
+			result = bvLeft ^ bvRight;
+			break;
+		case Token::SHL:
+			result = bvLeft << bvRight;
+			break;
+		case Token::SHR:
+			solAssert(false, "");
+		case Token::SAR:
+			result = isSigned ?
+				smtutil::Expression::ashr(bvLeft, bvRight) :
+				bvLeft >> bvRight;
+			break;
+		default:
+			solAssert(false, "");
+	}
+
+	solAssert(result.has_value(), "");
+	return smtutil::Expression::bv2int(*result, isSigned);
+}
+
 void SMTEncoder::compareOperation(BinaryOperation const& _op)
 {
 	auto const& commonType = _op.annotation().commonType;
@@ -1457,39 +1513,12 @@ void SMTEncoder::bitwiseOperation(BinaryOperation const& _op)
 	auto commonType = _op.annotation().commonType;
 	solAssert(commonType, "");
 
-	auto [bvSize, isSigned] = smt::typeBvSizeAndSignedness(commonType);
-
-	auto bvLeft = smtutil::Expression::int2bv(expr(_op.leftExpression(), commonType), bvSize);
-	auto bvRight = smtutil::Expression::int2bv(expr(_op.rightExpression(), commonType), bvSize);
-
-	optional<smtutil::Expression> result;
-	switch (op)
-	{
-	case Token::BitAnd:
-		result = bvLeft & bvRight;
-		break;
-	case Token::BitOr:
-		result = bvLeft | bvRight;
-		break;
-	case Token::BitXor:
-		result = bvLeft ^ bvRight;
-		break;
-	case Token::SHL:
-		result = bvLeft << bvRight;
-		break;
-	case Token::SHR:
-		solAssert(false, "");
-	case Token::SAR:
-		result = isSigned ?
-			smtutil::Expression::ashr(bvLeft, bvRight) :
-			bvLeft >> bvRight;
-		break;
-	default:
-		solAssert(false, "");
-	}
-
-	solAssert(result, "");
-	defineExpr(_op, smtutil::Expression::bv2int(*result, isSigned));
+	defineExpr(_op, bitwiseOperation(
+		_op.getOperator(),
+		expr(_op.leftExpression(), commonType),
+		expr(_op.rightExpression(), commonType),
+		commonType
+	));
 }
 
 void SMTEncoder::bitwiseNotOperation(UnaryOperation const& _op)
@@ -1597,9 +1626,24 @@ smtutil::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment
 		{Token::AssignDiv, Token::Div},
 		{Token::AssignMod, Token::Mod}
 	};
+	static map<Token, Token> const compoundToBitwise{
+		{Token::AssignBitAnd, Token::BitAnd},
+		{Token::AssignBitOr, Token::BitOr},
+		{Token::AssignBitXor, Token::BitXor}
+	};
 	Token op = _assignment.assignmentOperator();
-	solAssert(compoundToArithmetic.count(op), "");
+	solAssert(compoundToArithmetic.count(op) || compoundToBitwise.count(op), "");
+
 	auto decl = identifierToVariable(_assignment.leftHandSide());
+
+	if (compoundToBitwise.count(op))
+		return bitwiseOperation(
+			compoundToBitwise.at(op),
+			decl ? currentValue(*decl) : expr(_assignment.leftHandSide()),
+			expr(_assignment.rightHandSide()),
+			_assignment.annotation().type
+		);
+
 	auto values = arithmeticOperation(
 		compoundToArithmetic.at(op),
 		decl ? currentValue(*decl) : expr(_assignment.leftHandSide()),
diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h
index 9bb7b81ce..454f8777c 100644
--- a/libsolidity/formal/SMTEncoder.h
+++ b/libsolidity/formal/SMTEncoder.h
@@ -119,6 +119,14 @@ protected:
 		TypePointer const& _commonType,
 		Expression const& _expression
 	);
+
+	smtutil::Expression bitwiseOperation(
+		Token _op,
+		smtutil::Expression const& _left,
+		smtutil::Expression const& _right,
+		TypePointer const& _commonType
+	);
+
 	void compareOperation(BinaryOperation const& _op);
 	void booleanOperation(BinaryOperation const& _op);
 	void bitwiseOperation(BinaryOperation const& _op);