[SMTChecker] Support shifts

Changelog.md

@@ -4,6 +4,7 @@ Language Features:
 
 
 Compiler Features:
+ * SMTChecker: Support shifts.
  * SMTChecker: Support structs.
  * Yul Optimizer: Prune unused parameters in functions.
 

libsmtutil/CVC4Interface.cpp

@@ -196,6 +196,12 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
 			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 == "bvshl")
+			return m_context.mkExpr(CVC4::kind::BITVECTOR_SHL, arguments[0], arguments[1]);
+		else if (n == "bvlshr")
+			return m_context.mkExpr(CVC4::kind::BITVECTOR_LSHR, arguments[0], arguments[1]);
+		else if (n == "bvashr")
+			return m_context.mkExpr(CVC4::kind::BITVECTOR_ASHR, arguments[0], arguments[1]);
 		else if (n == "int2bv")
 		{
 			size_t size = std::stoul(_expr.arguments[1].name);

libsmtutil/SolverInterface.h

@@ -99,6 +99,9 @@ public:
 			{"bvand", 2},
 			{"bvor", 2},
 			{"bvxor", 2},
+			{"bvshl", 2},
+			{"bvlshr", 2},
+			{"bvashr", 2},
 			{"int2bv", 2},
 			{"bv2int", 1},
 			{"select", 2},
@@ -299,15 +302,30 @@ public:
 		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("bvor", {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)
+	friend Expression operator<<(Expression _a, Expression _b)
 	{
 		auto bvSort = _a.sort;
-		return Expression("bvor", {std::move(_a), std::move(_b)}, bvSort);
+		return Expression("bvshl", {std::move(_a), std::move(_b)}, bvSort);
+	}
+	friend Expression operator>>(Expression _a, Expression _b)
+	{
+		auto bvSort = _a.sort;
+		return Expression("bvlshr", {std::move(_a), std::move(_b)}, bvSort);
+	}
+	static Expression ashr(Expression _a, Expression _b)
+	{
+		auto bvSort = _a.sort;
+		return Expression("bvashr", {std::move(_a), std::move(_b)}, bvSort);
 	}
 	Expression operator()(std::vector<Expression> _arguments) const
 	{

libsmtutil/Z3Interface.cpp

@@ -189,6 +189,12 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 			return arguments[0] | arguments[1];
 		else if (n == "bvxor")
 			return arguments[0] ^ arguments[1];
+		else if (n == "bvshl")
+			return z3::shl(arguments[0], arguments[1]);
+		else if (n == "bvlshr")
+			return z3::lshr(arguments[0], arguments[1]);
+		else if (n == "bvashr")
+			return z3::ashr(arguments[0], arguments[1]);
 		else if (n == "int2bv")
 		{
 			size_t size = std::stoul(_expr.arguments[1].name);

libsolidity/formal/SMTEncoder.cpp

@@ -571,7 +571,7 @@ void SMTEncoder::endVisit(BinaryOperation const& _op)
 		arithmeticOperation(_op);
 	else if (TokenTraits::isCompareOp(_op.getOperator()))
 		compareOperation(_op);
-	else if (TokenTraits::isBitOp(_op.getOperator()))
+	else if (TokenTraits::isBitOp(_op.getOperator()) || TokenTraits::isShiftOp(_op.getOperator()))
 		bitwiseOperation(_op);
 	else
 		m_errorReporter.warning(
@@ -1422,7 +1422,8 @@ void SMTEncoder::booleanOperation(BinaryOperation const& _op)
 
 void SMTEncoder::bitwiseOperation(BinaryOperation const& _op)
 {
-	solAssert(TokenTraits::isBitOp(_op.getOperator()), "");
+	auto op = _op.getOperator();
+	solAssert(TokenTraits::isBitOp(op) || TokenTraits::isShiftOp(op), "");
 	auto commonType = _op.annotation().commonType;
 	solAssert(commonType, "");
 
@@ -1432,16 +1433,33 @@ void SMTEncoder::bitwiseOperation(BinaryOperation const& _op)
 	auto bvRight = smtutil::Expression::int2bv(expr(_op.rightExpression(), commonType), bvSize);
 
 	optional<smtutil::Expression> result;
-	if (_op.getOperator() == Token::BitAnd)
+	switch (op)
+	{
+	case Token::BitAnd:
 		result = bvLeft & bvRight;
-	else if (_op.getOperator() == Token::BitOr)
+		break;
+	case Token::BitOr:
 		result = bvLeft | bvRight;
-	else if (_op.getOperator() == Token::BitXor)
+		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, "");
-	if (result)
+	defineExpr(_op, smtutil::Expression::bv2int(*result, isSigned));
-		defineExpr(_op, smtutil::Expression::bv2int(*result, isSigned));
 }
 
 void SMTEncoder::bitwiseNotOperation(UnaryOperation const& _op)

test/libsolidity/smtCheckerTests/operators/shifts/shift_cleanup.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure returns (uint16 x) {
+		x = 0xffff;
+		x += 32;
+		x = x << 8;
+		x = x >> 16;
+		assert(x == 0);
+		// Fails because x = 0.
+		assert(x == 10);
+	}
+}
+// ----
+// Warning 4984: (109-116): Overflow (resulting value larger than 65535) happens here.
+// Warning 6328: (193-208): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/shifts/shift_left.sol

@@ -0,0 +1,29 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f(uint256 a, uint256 b) internal pure returns (uint256) {
+        return a << b;
+    }
+	function t() public pure {
+		assert(f(0x4266, 0x0) == 0x4266);
+		// Fails because the above is true.
+		assert(f(0x4266, 0x0) == 0x4268);
+
+		assert(f(0x4266, 0x8) == 0x426600);
+		// Fails because the above is true.
+		assert(f(0x4266, 0x8) == 0x120939);
+
+		assert(f(0x4266, 0xf0) == 0x4266000000000000000000000000000000000000000000000000000000000000);
+		// Fails because the above is true.
+		assert(f(0x4266, 0xf0) == 0x4266000000000000000000000000000000000000000000000000000000000001);
+
+		assert(f(0x4266, 0x4266) == 0);
+		// Fails because the above is true.
+		assert(f(0x4266, 0x4266) == 1);
+	}
+}
+// ----
+// Warning 6328: (250-282): Assertion violation happens here.
+// Warning 6328: (363-397): Assertion violation happens here.
+// Warning 6328: (537-630): Assertion violation happens here.
+// Warning 6328: (707-737): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/shifts/shift_left_larger_type.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure returns (int8) {
+		uint8 x = 254;
+		int8 y = 1;
+		assert(y << x == 0);
+		// Fails because z = 0.
+		assert(y << x == 10);
+		return y << x;
+	}
+}
+// ----
+// Warning 6328: (171-191): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/shifts/shift_left_uint32.sol

@@ -0,0 +1,29 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f(uint32 a, uint32 b) internal pure returns (uint256) {
+        return a << b;
+    }
+	function t() public pure {
+		assert(f(0x4266, 0) == 0x4266);
+		// Fails because the above is true.
+		assert(f(0x4266, 0) == 0x4267);
+
+		assert(f(0x4266, 0x10) == 0x42660000);
+		// Fails because the above is true.
+		assert(f(0x4266, 0x10) == 0x426600000);
+
+		assert(f(0x4266, 0x11) == 0x84cc0000);
+		// Fails because the above is true.
+		assert(f(0x4266, 0x11) == 0x84cc000);
+
+		assert(f(0x4266, 0x20) == 0);
+		// Fails because the above is true.
+		assert(f(0x4266, 0x20) == 1);
+	}
+}
+// ----
+// Warning 6328: (246-276): Assertion violation happens here.
+// Warning 6328: (360-398): Assertion violation happens here.
+// Warning 6328: (482-518): Assertion violation happens here.
+// Warning 6328: (593-621): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/shifts/shift_left_uint8.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f(uint8 a, uint8 b) internal pure returns (uint256) {
+        return a << b;
+    }
+	function t() public pure {
+		assert(f(0x66, 0x0) == 0x66);
+		// Fails because the above is true.
+		assert(f(0x66, 0x0) == 0x660);
+
+		assert(f(0x66, 0x8) == 0);
+		// Fails because the above is true.
+		assert(f(0x66, 0x8) == 1);
+	}
+}
+// ----
+// Warning 6328: (242-271): Assertion violation happens here.
+// Warning 6328: (343-368): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/shifts/shift_overflow.sol

@@ -0,0 +1,39 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function leftU(uint8 x, uint8 y) internal pure returns (uint8) {
+        return x << y;
+    }
+
+    function leftS(int8 x, uint8 y) internal pure returns (int8) {
+        return x << y;
+    }
+
+	function t() public pure {
+		assert(leftU(255, 8) == 0);
+		// Fails because the above is true.
+		assert(leftU(255, 8) == 1);
+
+		assert(leftU(255, 1) == 254);
+		// Fails because the above is true.
+		assert(leftU(255, 1) == 255);
+
+		assert(leftU(255, 0) == 255);
+		// Fails because the above is true.
+		assert(leftU(255, 0) == 0);
+
+		assert(leftS(1, 7) == -128);
+		// Fails because the above is true.
+		assert(leftS(1, 7) == 127);
+
+		assert(leftS(1, 6) == 64);
+		// Fails because the above is true.
+		assert(leftS(1, 6) == -64);
+	}
+}
+// ----
+// Warning 6328: (340-366): Assertion violation happens here.
+// Warning 6328: (441-469): Assertion violation happens here.
+// Warning 6328: (544-570): Assertion violation happens here.
+// Warning 6328: (644-670): Assertion violation happens here.
+// Warning 6328: (742-768): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/shifts/shift_right.sol

@@ -0,0 +1,29 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f(uint256 a, uint256 b) internal pure returns (uint256) {
+        return a >> b;
+    }
+	function t() public pure {
+		assert(f(0x4266, 0) == 0x4266);
+		// Fails because the above is true.
+		assert(f(0x4266, 0) == 0x426);
+
+		assert(f(0x4266, 0x8) == 0x42);
+		// Fails because the above is true.
+		assert(f(0x4266, 0x8) == 0x420);
+
+		assert(f(0x4266, 0x11) == 0);
+		// Fails because the above is true.
+		assert(f(0x4266, 0x11) == 1);
+
+		assert(f(57896044618658097711785492504343953926634992332820282019728792003956564819968, 5) == 1809251394333065553493296640760748560207343510400633813116524750123642650624);
+		// Fails because the above is true.
+		assert(f(57896044618658097711785492504343953926634992332820282019728792003956564819968, 5) == 0);
+	}
+}
+// ----
+// Warning 6328: (248-277): Assertion violation happens here.
+// Warning 6328: (354-385): Assertion violation happens here.
+// Warning 6328: (460-488): Assertion violation happens here.
+// Warning 6328: (706-802): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/shifts/shift_right_negative_literal.sol

@@ -0,0 +1,40 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f(int16 x, uint16 y, int16 z) internal pure returns (bool) {
+		return x >> y == z;
+	}
+
+	function t() public pure {
+		assert(f(-4266, 0, -4266));
+		// Fails because the above is true.
+		assert(f(-4266, 0, -426));
+
+		assert(f(-4266, 1, -2133));
+		// Fails because the above is true.
+		assert(f(-4266, 1, -2134));
+
+		assert(f(-4266, 4, -267));
+		// Fails because the above is true.
+		assert(f(-4266, 4, -2670));
+
+		assert(f(-4266, 8, -17));
+		// Fails because the above is true.
+		assert(f(-4266, 8, -1));
+
+		assert(f(-4266, 16, -1));
+		// Fails because the above is true.
+		assert(f(-4266, 16, -0));
+
+		assert(f(-4266, 17, -1));
+		// Fails because the above is true.
+		assert(f(-4266, 17, -0));
+	}
+}
+// ----
+// Warning 6328: (241-266): Assertion violation happens here.
+// Warning 6328: (339-365): Assertion violation happens here.
+// Warning 6328: (437-463): Assertion violation happens here.
+// Warning 6328: (534-557): Assertion violation happens here.
+// Warning 6328: (628-652): Assertion violation happens here.
+// Warning 6328: (723-747): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/shifts/shift_right_negative_lvalue.sol

@@ -0,0 +1,40 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f(int256 a, uint256 b) internal pure returns (int256) {
+        return a >> b;
+    }
+	function t() public pure {
+		assert(f(-4266, 0) == -4266);
+		// Fails because the above is true.
+		assert(f(-4266, 0) == -426);
+
+		assert(f(-4266, 1) == -2133);
+		// Fails because the above is true.
+		assert(f(-4266, 1) == -21330);
+
+		assert(f(-4266, 4) == -267);
+		// Fails because the above is true.
+		assert(f(-4266, 4) == -255);
+
+		assert(f(-4266, 8) == -17);
+		// Fails because the above is true.
+		assert(f(-4266, 8) == -1);
+
+		assert(f(-4266, 16) == -1);
+		// Fails because the above is true.
+		assert(f(-4266, 16) == 0);
+
+		assert(f(-4266, 17) == -1);
+		// Fails because the above is true.
+		assert(f(-4266, 17) == 0);
+	}
+
+}
+// ----
+// Warning 6328: (244-271): Assertion violation happens here.
+// Warning 6328: (346-375): Assertion violation happens here.
+// Warning 6328: (449-476): Assertion violation happens here.
+// Warning 6328: (549-574): Assertion violation happens here.
+// Warning 6328: (647-672): Assertion violation happens here.
+// Warning 6328: (745-770): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/shifts/shift_right_negative_lvalue_int16.sol

@@ -0,0 +1,39 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f(int16 a, uint16 b) internal pure returns (int256) {
+        return a >> b;
+    }
+	function t() public pure {
+		assert(f(-4266, 0) == -4266);
+		// Fails because the above is true.
+		assert(f(-4266, 0) == -426);
+
+		assert(f(-4266, 1) == -2133);
+		// Fails because the above is true.
+		assert(f(-4266, 1) == -21330);
+
+		assert(f(-4266, 4) == -267);
+		// Fails because the above is true.
+		assert(f(-4266, 4) == -255);
+
+		assert(f(-4266, 8) == -17);
+		// Fails because the above is true.
+		assert(f(-4266, 8) == -1);
+
+		assert(f(-4266, 16) == -1);
+		// Fails because the above is true.
+		assert(f(-4266, 16) == 0);
+
+		assert(f(-4266, 17) == -1);
+		// Fails because the above is true.
+		assert(f(-4266, 17) == 0);
+	}
+}
+// ----
+// Warning 6328: (242-269): Assertion violation happens here.
+// Warning 6328: (344-373): Assertion violation happens here.
+// Warning 6328: (447-474): Assertion violation happens here.
+// Warning 6328: (547-572): Assertion violation happens here.
+// Warning 6328: (645-670): Assertion violation happens here.
+// Warning 6328: (743-768): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/shifts/shift_right_negative_lvalue_int32.sol

@@ -0,0 +1,39 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f(int32 a, uint32 b) internal pure returns (int256) {
+        return a >> b;
+    }
+	function t() public pure {
+		assert(f(-4266, 0) == -4266);
+		// Fails because the above is true.
+		assert(f(-4266, 0) == -426);
+
+		assert(f(-4266, 1) == -2133);
+		// Fails because the above is true.
+		assert(f(-4266, 1) == -21330);
+
+		assert(f(-4266, 4) == -267);
+		// Fails because the above is true.
+		assert(f(-4266, 4) == -255);
+
+		assert(f(-4266, 8) == -17);
+		// Fails because the above is true.
+		assert(f(-4266, 8) == -1);
+
+		assert(f(-4266, 16) == -1);
+		// Fails because the above is true.
+		assert(f(-4266, 16) == 0);
+
+		assert(f(-4266, 17) == -1);
+		// Fails because the above is true.
+		assert(f(-4266, 17) == 0);
+	}
+}
+// ----
+// Warning 6328: (242-269): Assertion violation happens here.
+// Warning 6328: (344-373): Assertion violation happens here.
+// Warning 6328: (447-474): Assertion violation happens here.
+// Warning 6328: (547-572): Assertion violation happens here.
+// Warning 6328: (645-670): Assertion violation happens here.
+// Warning 6328: (743-768): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/shifts/shift_right_negative_lvalue_int8.sol

@@ -0,0 +1,39 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f(int8 a, uint8 b) internal pure returns (int256) {
+        return a >> b;
+    }
+	function t() public pure {
+		assert(f(-66, 0) == -66);
+		// Fails because the above is true.
+		assert(f(-66, 0) == -6);
+
+		assert(f(-66, 1) == -33);
+		// Fails because the above is true.
+		assert(f(-66, 1) == -3);
+
+		assert(f(-66, 4) == -5);
+		// Fails because the above is true.
+		assert(f(-66, 4) == -2);
+
+		assert(f(-66, 8) == -1);
+		// Fails because the above is true.
+		assert(f(-66, 8) == -2);
+
+		assert(f(-66, 16) == -1);
+		// Fails because the above is true.
+		assert(f(-66, 16) == 0);
+
+		assert(f(-66, 17) == -1);
+		// Fails because the above is true.
+		assert(f(-66, 17) == 0);
+	}
+}
+// ----
+// Warning 6328: (236-259): Assertion violation happens here.
+// Warning 6328: (330-353): Assertion violation happens here.
+// Warning 6328: (423-446): Assertion violation happens here.
+// Warning 6328: (516-539): Assertion violation happens here.
+// Warning 6328: (610-633): Assertion violation happens here.
+// Warning 6328: (704-727): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/shifts/shift_right_uint32.sol

@@ -0,0 +1,29 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f(uint32 a, uint32 b) internal pure returns (uint256) {
+        return a >> b;
+    }
+	function t() public pure {
+		assert(f(0x4266, 0) == 0x4266);
+		// Fails because the above is true.
+		assert(f(0x4266, 0) == 0x426);
+
+		assert(f(0x4266, 8) == 0x42);
+		// Fails because the above is true.
+		assert(f(0x4266, 8) == 0x420);
+
+		assert(f(0x4266, 0x10) == 0);
+		// Fails because the above is true.
+		assert(f(0x4266, 0x10) == 255);
+
+		assert(f(0x4266, 0x11) == 0);
+		// Fails because the above is true.
+		assert(f(0x4266, 0x11) == 255);
+	}
+}
+// ----
+// Warning 6328: (246-275): Assertion violation happens here.
+// Warning 6328: (350-379): Assertion violation happens here.
+// Warning 6328: (454-484): Assertion violation happens here.
+// Warning 6328: (559-589): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/shifts/shift_right_uint8.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f(uint8 a, uint8 b) internal pure returns (uint256) {
+        return a >> b;
+    }
+	function t() public pure {
+		assert(f(0x66, 0) == 0x66);
+		// Fails because the above is true.
+		assert(f(0x66, 0) == 0x6);
+
+		assert(f(0x66, 8) == 0);
+		// Fails because the above is true.
+		assert(f(0x66, 8) == 1);
+	}
+}
+// ----
+// Warning 6328: (240-265): Assertion violation happens here.
+// Warning 6328: (335-358): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/shifts/shift_underflow_negative_rvalue.sol

@@ -0,0 +1,24 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f(int256 a, uint256 b) internal pure returns (int256) {
+        return a << b;
+    }
+
+    function g(int256 a, uint256 b) internal pure returns (int256) {
+        return a >> b;
+    }
+
+	function t() public pure {
+		assert(f(1, 2**256 - 1) == 0);
+		// Fails because the above is true.
+		assert(f(1, 2**256 - 1) == 1);
+
+		assert(g(1, 2**256 - 1) == 0);
+		// Fails because the above is true.
+		assert(g(1, 2**256 - 1) == 1);
+	}
+}
+// ----
+// Warning 6328: (345-374): Assertion violation happens here.
+// Warning 6328: (450-479): Assertion violation happens here.