From e2e0b33ee7a204c316c72e1562e89e5347285281 Mon Sep 17 00:00:00 2001
From: Djordje Mijovic <djordje.mijovic@gmail.com>
Date: Tue, 22 Sep 2020 10:14:31 +0200
Subject: [PATCH] [SMTChecker] Updating old and adding new tests for compound
 bitwise or operator.

---
 .../operators/compound_bitwise_or_1.sol       | 10 -------
 .../operators/compound_bitwise_or_2.sol       | 10 -------
 .../operators/compound_bitwise_or_3.sol       | 13 ---------
 .../operators/compound_bitwise_or_4.sol       | 13 ---------
 .../compound_bitwise_or_fixed_bytes.sol       | 14 +++++++++
 .../operators/compound_bitwise_or_int.sol     | 21 ++++++++++++++
 .../operators/compound_bitwise_or_int_1.sol   | 11 +++++++
 .../operators/compound_bitwise_or_uint.sol    | 29 +++++++++++++++++++
 .../operators/compound_bitwise_or_uint_1.sol  | 11 +++++++
 .../operators/compound_bitwise_or_uint_2.sol  | 14 +++++++++
 .../operators/compound_bitwise_or_uint_3.sol  | 12 ++++++++
 11 files changed, 112 insertions(+), 46 deletions(-)
 delete mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_1.sol
 delete mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_2.sol
 delete mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_3.sol
 delete mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_4.sol
 create mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_fixed_bytes.sol
 create mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int.sol
 create mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol
 create mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint.sol
 create mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol
 create mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol
 create mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol

diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_1.sol
deleted file mode 100644
index 24e61cf58..000000000
--- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_1.sol
+++ /dev/null
@@ -1,10 +0,0 @@
-pragma experimental SMTChecker;
-contract C {
-	int[1] c;
-	function f(bool b) public {
-		if (b)
-			c[0] |= 1;
-	}
-}
-// ----
-// Warning 9149: (97-106): Assertion checker does not yet implement this assignment operator.
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_2.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_2.sol
deleted file mode 100644
index 4569afa88..000000000
--- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_2.sol
+++ /dev/null
@@ -1,10 +0,0 @@
-pragma experimental SMTChecker;
-contract C {
-	int[1][20] c;
-	function f(bool b) public {
-		if (b)
-			c[10][0] |= 1;
-	}
-}
-// ----
-// Warning 9149: (101-114): Assertion checker does not yet implement this assignment operator.
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_3.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_3.sol
deleted file mode 100644
index fdcfa3e14..000000000
--- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_3.sol
+++ /dev/null
@@ -1,13 +0,0 @@
-pragma experimental SMTChecker;
-contract C {
-	struct S {
-		uint x;
-	}
-	S s;
-	function f(bool b) public {
-		if (b)
-			s.x |= 1;
-	}
-}
-// ----
-// Warning 9149: (117-125): Assertion checker does not yet implement this assignment operator.
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_4.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_4.sol
deleted file mode 100644
index 00e32d0d1..000000000
--- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_4.sol
+++ /dev/null
@@ -1,13 +0,0 @@
-pragma experimental SMTChecker;
-contract C {
-	struct S {
-		uint[] x;
-	}
-	S s;
-	function f(bool b) public {
-		if (b)
-			s.x[2] |= 1;
-	}
-}
-// ----
-// Warning 9149: (119-130): Assertion checker does not yet implement this assignment operator.
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_fixed_bytes.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_fixed_bytes.sol
new file mode 100644
index 000000000..8be3855b0
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_fixed_bytes.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract C {
+    function f() public pure returns (byte) {
+        byte a = 0xff;
+        byte b = 0xf0;
+        b |= a;
+        assert(a == b);
+
+        a |= ~b;
+        assert(a == 0); // fails
+    }
+}
+// ----
+// Warning 6328: (203-217): Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int.sol
new file mode 100644
index 000000000..b6fd90ce7
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int.sol
@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		int8 x = 1;
+		int8 y = 0;
+		x |= y;
+		assert(x == 0); // fails
+		x = -1; y = 3;
+		x |= y;
+		assert(x == -1);
+		x = 4;
+		y |= x;
+		assert(y == 7);
+		y = 127;
+		x |= y;
+		assert(x == 127);
+	}
+}
+// ----
+// Warning 6328: (114-128): Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol
new file mode 100644
index 000000000..e25ae354d
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol
@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+contract C {
+    int[1][20] c;
+    function f(bool b) public {
+	    require(c[10][0] == 0);
+        if (b)
+            c[10][0] |= 1;
+        assert(c[10][0] == 0 || c[10][0] == 1);
+    }
+}
+// ----
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint.sol
new file mode 100644
index 000000000..ddc0c4376
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint.sol
@@ -0,0 +1,29 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f() public pure {
+        uint v = 7;
+        v |= 3;
+        assert(v != 7); // fails, as 7 | 3 = 7
+
+        uint c = 0;
+        c |= v;
+        assert(c == 7);
+
+        uint16 x = 0xff;
+        uint16 y = 0xffff;
+        y |= x;
+        assert(y == 0xff); // fails
+        assert(y == 0xffff);
+
+        y = 0xf1ff;
+        x = 0xff00;
+        x |= y & x;
+        assert(y == 0xffff); // fails
+        assert(x == 0xff00);
+    }
+}
+// ----
+// Warning 6328: (121-135): Assertion violation happens here.
+// Warning 6328: (298-315): Assertion violation happens here.
+// Warning 6328: (424-443): Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol
new file mode 100644
index 000000000..790d30a76
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol
@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+contract C {
+    uint[1] c;
+    function f(bool b) public {
+        require(c[0] == 0);
+        if (b)
+            c[0] |= 1;
+        assert(c[0] <= 1);
+    }
+}
+// ----
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol
new file mode 100644
index 000000000..04d907cf4
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract C {
+    struct S {
+        uint[] x;
+    }
+    S s;
+    function f(bool b) public {
+        if (b)
+            s.x[2] |= 1;
+        assert(s.x[2] != 1);
+    }
+}
+// ----
+// Warning 6328: (173-192): Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol
new file mode 100644
index 000000000..8132ae773
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol
@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+contract C {
+    struct S {
+        uint x;
+    }
+    S s;
+    function f(bool b) public {
+        s.x |= b ? 1 : 2;
+        assert(s.x > 0);
+    }
+}
+// ----