Merge pull request #9661 from ethereum/smtBitwiseOr

[SMTChecker] Support bitwise or, xor and not operator

Changelog.md

@@ -10,6 +10,7 @@ Compiler Features:
  * Yul: Report error when using non-string literals for ``datasize()``, ``dataoffset()``, ``linkersymbol()``, ``loadimmutable()``, ``setimmutable()``.
  * Yul Optimizer: LoopInvariantCodeMotion can move reading operations outside for-loops as long as the affected area is not modified inside the loop.
  * SMTChecker: Support conditional operator.
+ * SMTChecker: Support bitwise or, xor and not operators.
 
 Bugfixes:
  * AST: Remove ``null`` member values also when the compiler is used in standard-json-mode.

libsmtutil/CVC4Interface.cpp

@@ -188,8 +188,14 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
 			return m_context.mkExpr(CVC4::kind::INTS_DIVISION_TOTAL, arguments[0], arguments[1]);
 		else if (n == "mod")
 			return m_context.mkExpr(CVC4::kind::INTS_MODULUS, arguments[0], arguments[1]);
+		else if (n == "bvnot")
+			return m_context.mkExpr(CVC4::kind::BITVECTOR_NOT, arguments[0]);
 		else if (n == "bvand")
 			return m_context.mkExpr(CVC4::kind::BITVECTOR_AND, arguments[0], arguments[1]);
+		else if (n == "bvor")
+			return m_context.mkExpr(CVC4::kind::BITVECTOR_OR, arguments[0], arguments[1]);
+		else if (n == "bvxor")
+			return m_context.mkExpr(CVC4::kind::BITVECTOR_XOR, arguments[0], arguments[1]);
 		else if (n == "int2bv")
 		{
 			size_t size = std::stoul(_expr.arguments[1].name);

libsmtutil/SolverInterface.h

@@ -95,7 +95,10 @@ public:
 			{"*", 2},
 			{"/", 2},
 			{"mod", 2},
+			{"bvnot", 1},
 			{"bvand", 2},
+			{"bvor", 2},
+			{"bvxor", 2},
 			{"int2bv", 2},
 			{"bv2int", 1},
 			{"select", 2},
@@ -286,11 +289,26 @@ public:
 		auto intSort = _a.sort;
 		return Expression("mod", {std::move(_a), std::move(_b)}, intSort);
 	}
+	friend Expression operator~(Expression _a)
+	{
+		auto bvSort = _a.sort;
+		return Expression("bvnot", {std::move(_a)}, bvSort);
+	}
 	friend Expression operator&(Expression _a, Expression _b)
 	{
 		auto bvSort = _a.sort;
 		return Expression("bvand", {std::move(_a), std::move(_b)}, bvSort);
 	}
+	friend Expression operator^(Expression _a, Expression _b)
+	{
+		auto bvSort = _a.sort;
+		return Expression("bvxor", {std::move(_a), std::move(_b)}, bvSort);
+	}
+	friend Expression operator|(Expression _a, Expression _b)
+	{
+		auto bvSort = _a.sort;
+		return Expression("bvor", {std::move(_a), std::move(_b)}, bvSort);
+	}
 	Expression operator()(std::vector<Expression> _arguments) const
 	{
 		smtAssert(

libsmtutil/Z3Interface.cpp

@@ -181,8 +181,14 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 			return arguments[0] / arguments[1];
 		else if (n == "mod")
 			return z3::mod(arguments[0], arguments[1]);
+		else if (n == "bvnot")
+			return ~arguments[0];
 		else if (n == "bvand")
 			return arguments[0] & arguments[1];
+		else if (n == "bvor")
+			return arguments[0] | arguments[1];
+		else if (n == "bvxor")
+			return arguments[0] ^ arguments[1];
 		else if (n == "int2bv")
 		{
 			size_t size = std::stoul(_expr.arguments[1].name);

libsolidity/formal/SMTEncoder.cpp

@@ -456,6 +456,8 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple)
 
 void SMTEncoder::endVisit(UnaryOperation const& _op)
 {
+	if (TokenTraits::isBitOp(_op.getOperator()))
+		return bitwiseNotOperation(_op);
 	if (_op.annotation().type->category() == Type::Category::RationalNumber)
 		return;
 
@@ -1406,20 +1408,7 @@ void SMTEncoder::bitwiseOperation(BinaryOperation const& _op)
 	auto commonType = _op.annotation().commonType;
 	solAssert(commonType, "");
 
-	unsigned bvSize = 256;
-	bool isSigned = false;
-	if (auto const* intType = dynamic_cast<IntegerType const*>(commonType))
-	{
-		bvSize = intType->numBits();
-		isSigned = intType->isSigned();
-	}
-	else if (auto const* fixedType = dynamic_cast<FixedPointType const*>(commonType))
-	{
-		bvSize = fixedType->numBits();
-		isSigned = fixedType->isSigned();
-	}
-	else if (auto const* fixedBytesType = dynamic_cast<FixedBytesType const*>(commonType))
-		bvSize = fixedBytesType->numBytes() * 8;
+	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);
@@ -1427,18 +1416,26 @@ void SMTEncoder::bitwiseOperation(BinaryOperation const& _op)
 	optional<smtutil::Expression> result;
 	if (_op.getOperator() == Token::BitAnd)
 		result = bvLeft & bvRight;
-	// TODO implement the other operators
-	else
-		m_errorReporter.warning(
-			1093_error,
-			_op.location(),
-			"Assertion checker does not yet implement this bitwise operator."
-		);
+	else if (_op.getOperator() == Token::BitOr)
+		result = bvLeft | bvRight;
+	else if (_op.getOperator() == Token::BitXor)
+		result = bvLeft ^ bvRight;
 
+	solAssert(result, "");
 	if (result)
 		defineExpr(_op, smtutil::Expression::bv2int(*result, isSigned));
 }
 
+void SMTEncoder::bitwiseNotOperation(UnaryOperation const& _op)
+{
+	solAssert(_op.getOperator() == Token::BitNot, "");
+
+	auto [bvSize, isSigned] = smt::typeBvSizeAndSignedness(_op.annotation().type);
+
+	auto bvOperand = smtutil::Expression::int2bv(expr(_op.subExpression(), _op.annotation().type), bvSize);
+	defineExpr(_op, smtutil::Expression::bv2int(~bvOperand, isSigned));
+}
+
 smtutil::Expression SMTEncoder::division(smtutil::Expression _left, smtutil::Expression _right, IntegerType const& _type)
 {
 	// Signed division in SMTLIB2 rounds differently for negative division.

libsolidity/formal/SMTEncoder.h

@@ -115,6 +115,7 @@ protected:
 	void compareOperation(BinaryOperation const& _op);
 	void booleanOperation(BinaryOperation const& _op);
 	void bitwiseOperation(BinaryOperation const& _op);
+	void bitwiseNotOperation(UnaryOperation const& _op);
 
 	void initContract(ContractDefinition const& _contract);
 	void initFunction(FunctionDefinition const& _function);

libsolidity/formal/SymbolicTypes.cpp

@@ -432,6 +432,18 @@ smtutil::Expression zeroValue(frontend::TypePointer const& _type)
 	return 0;
 }
 
+pair<unsigned, bool> typeBvSizeAndSignedness(frontend::TypePointer const& _type)
+{
+	if (auto const* intType = dynamic_cast<IntegerType const*>(_type))
+		return {intType->numBits(), intType->isSigned()};
+	else if (auto const* fixedType = dynamic_cast<FixedPointType const*>(_type))
+		return {fixedType->numBits(), fixedType->isSigned()};
+	else if (auto const* fixedBytesType = dynamic_cast<FixedBytesType const*>(_type))
+		return {fixedBytesType->numBytes() * 8, false};
+	else
+		solAssert(false, "");
+}
+
 void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext& _context)
 {
 	setSymbolicUnknownValue(_variable.currentValue(), _variable.type(), _context);

libsolidity/formal/SymbolicTypes.h

@@ -67,6 +67,8 @@ smtutil::Expression minValue(frontend::IntegerType const& _type);
 smtutil::Expression maxValue(frontend::IntegerType const& _type);
 smtutil::Expression zeroValue(frontend::TypePointer const& _type);
 
+std::pair<unsigned, bool> typeBvSizeAndSignedness(frontend::TypePointer const& type);
+
 void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _context);
 void setSymbolicZeroValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context);
 void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext& _context);

test/libsolidity/smtCheckerTests/operators/bitwise_combo.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		uint8 x = 0xff;
+		uint8 y = ~x;
+		assert(x & y == 0);
+		assert(x | y == 0xff);
+		assert(x ^ y == 0xff);
+	}
+}
+// ----

test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol

@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+contract C {
+  function f() public pure returns (byte) {
+    return (~byte(0xFF));
+  }
+}
+// ----
+// Warning 5084: (102-112): Type conversion is not yet fully supported and might yield false positives.

test/libsolidity/smtCheckerTests/operators/bitwise_not_int.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		int16 x = 1;
+		assert(~x == 0);
+		x = 0xff;
+		assert(~x == 0);
+		x = 0x0f;
+		assert(~x == 0xf0);
+		x = -1;
+		assert(~x != 0);
+		x = -2;
+		assert(~x == 1);
+	}
+}
+// ----
+// Warning 6328: (91-106): Assertion violation happens here
+// Warning 6328: (122-137): Assertion violation happens here
+// Warning 6328: (153-171): Assertion violation happens here
+// Warning 6328: (185-200): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/bitwise_not_uint.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		uint8 x = 0xff;
+		assert(~x == 0x00);
+		uint16 y = 0xff00;
+		assert(~y == 0xff);
+		assert(~y == 0xffff);
+		assert(~y == 0x0000);
+	}
+}
+// ----
+// Warning 6328: (159-179): Assertion violation happens here
+// Warning 6328: (183-203): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/bitwise_or_fixed_bytes.sol

@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+contract C {
+  function f() public pure returns (byte) {
+    return (byte(0x0F) | (byte(0xF0)));
+  }
+}
+// ----
+// Warning 5084: (101-111): Type conversion is not yet fully supported and might yield false positives.
+// Warning 5084: (115-125): Type conversion is not yet fully supported and might yield false positives.

test/libsolidity/smtCheckerTests/operators/bitwise_or_int.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		int16 x = 1;
+		int16 y = 0;
+		assert(x | y == 1);
+		x = 0; y = 0;
+		assert(x | y != 0);
+		y = 240;
+		x = 15;
+		int16 z = x | y;
+		assert(z == 255);
+		x = -1; y = 200;
+		assert(x | y == x);
+		assert(x | z != -1);
+	}
+}
+// ----
+// Warning 6328: (144-162): Assertion violation happens here
+// Warning 6328: (267-286): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/bitwise_or_uint.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		uint8 x = 1;
+		uint16 y = 0;
+		assert(x | y != 0);
+		x = 0xff;
+		y = 0xff00;
+		assert(x | y == 0xff);
+		assert(x | y == 0xffff);
+		assert(x | y == 0x0000);
+	}
+}
+// ----
+// Warning 6328: (155-176): Assertion violation happens here
+// Warning 6328: (207-230): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/bitwise_xor_fixed_bytes.sol

@@ -6,4 +6,3 @@ contract Simp {
     }
 }
 // ----
-// Warning 1093: (142-152): Assertion checker does not yet implement this bitwise operator.

test/libsolidity/smtCheckerTests/operators/bitwise_xor_int.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		int8 x = 1;
+		int16 y = 0;
+		assert(x ^ y == 1);
+		int16 z = -1;
+		assert(x ^ z == -2);
+		assert(y ^ z == -1);
+		assert(y ^ z > 0);
+		x = 7; y = 3;
+		assert(x ^ y < 5);
+		assert(x ^ y > 5);
+	}
+}
+// ----
+// Warning 6328: (189-206): Assertion violation happens here
+// Warning 6328: (247-264): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/bitwise_xor_uint.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		uint8 x = 1;
+		uint16 y = 0;
+		assert(x ^ y != 0);
+		x = 0xff;
+		y = 0xff00;
+		assert(x ^ y == 0xff);
+		assert(x ^ y == 0xffff);
+		assert(x ^ y == 0x0000);
+	}
+}
+// ----
+// Warning 6328: (155-176): Assertion violation happens here
+// Warning 6328: (207-230): Assertion violation happens here