Merge pull request #5390 from ethereum/smt_one_loop

[SMTChecker] Unroll loops once

17 files changed, 177 insertions, 8 deletions

diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol b/test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol
new file mode 100644
index 00000000..ea5bf044
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol
@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x) public pure {
+		require(x < 100);
+		do {
+			// Overflows due to resetting x.
+			x = x + 1;
+		} while (x < 10);
+		assert(x < 14);
+	}
+}
+// ----
+// Warning: (150-155): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
+// Warning: (146-155): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
+// Warning: (179-193): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol b/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol
new file mode 100644
index 00000000..33e598b6
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol
@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x) public pure {
+		require(x < 100);
+		do {
+			// Overflows due to resetting x.
+			x = x + 1;
+		} while (x < 1000);
+		// The assertion is true but we can't infer so
+		// because x is touched in the loop.
+		assert(x > 0);
+	}
+}
+// ----
+// Warning: (150-155): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
+// Warning: (146-155): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
+// Warning: (269-282): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol b/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol
new file mode 100644
index 00000000..3858403a
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol
@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x) public pure {
+		require(x < 100);
+		for(uint i = 0; i < 10; ++i) {
+			// Overflows due to resetting x.
+			x = x + 1;
+		}
+		assert(x < 14);
+	}
+}
+// ----
+// Warning: (176-181): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
+// Warning: (172-181): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
+// Warning: (189-203): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol
new file mode 100644
index 00000000..7d7b7015
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol
@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x) public pure {
+		require(x < 100);
+		for(uint i = 0; i < 10; ++i) {
+			// Overflows due to resetting x.
+			x = x + 1;
+		}
+		// The assertion is true but x is touched and reset.
+		assert(x > 0);
+	}
+}
+// ----
+// Warning: (176-181): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
+// Warning: (172-181): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
+// Warning: (244-257): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_5.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_5.sol
index 2c84960f..eb62d36e 100644
--- a/test/libsolidity/smtCheckerTests/loops/for_loop_5.sol
+++ b/test/libsolidity/smtCheckerTests/loops/for_loop_5.sol
@@ -9,4 +9,4 @@ contract C {
     }
 }
 // ----
-// Warning: (167-181): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require().
+// Warning: (167-181): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_6.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_6.sol
index 90c4c328..b0c3cae4 100644
--- a/test/libsolidity/smtCheckerTests/loops/for_loop_6.sol
+++ b/test/libsolidity/smtCheckerTests/loops/for_loop_6.sol
@@ -5,8 +5,9 @@ contract C {
         for (y = 2; x < 10; ) {
             y = 3;
         }
-        assert(y == 2);
+        // False positive due to resetting y.
+        assert(y < 4);
     }
 }
 // ----
-// Warning: (167-181): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require().
+// Warning: (213-226): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_1.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_1.sol
new file mode 100644
index 00000000..21e6c91e
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_1.sol
@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+contract C {
+    function f(uint x) public pure {
+        require(x == 2);
+        for (; x == 2;) {}
+        assert(x == 2);
+    }
+}
+// ----
+// Warning: (122-128): For loop condition is always true.
diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_2.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_2.sol
new file mode 100644
index 00000000..6184c441
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_2.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+contract C {
+    function f(uint x) public pure {
+        require(x == 2);
+        uint y;
+        for (; x == 2;) {
+            y = 7;
+        }
+        assert(x == 2);
+    }
+}
+// ----
+// Warning: (138-144): For loop condition is always true.
diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_3.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_3.sol
new file mode 100644
index 00000000..eec59ded
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_3.sol
@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+contract C {
+    function f(uint x) public pure {
+        require(x == 2);
+        uint y;
+        // The loop condition is always true,
+        // but since x is touched in the body
+        // we can't infer that.
+        for (; x == 2;) {
+            x = 2;
+        }
+        // False positive due to resetting x.
+        assert(x == 2);
+    }
+}
+// ----
+// Warning: (115-121): Unused local variable.
+// Warning: (356-370): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_unreachable_1.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_unreachable_1.sol
new file mode 100644
index 00000000..f367d8d9
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/loops/for_loop_unreachable_1.sol
@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+contract C {
+    function f(uint x) public pure {
+        require(x == 2);
+        for (; x > 2;) {}
+        assert(x == 2);
+    }
+}
+// ----
+// Warning: (122-127): For loop condition is always false.
diff --git a/test/libsolidity/smtCheckerTests/loops/while_1.sol b/test/libsolidity/smtCheckerTests/loops/while_1.sol
new file mode 100644
index 00000000..871ed929
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/loops/while_1.sol
@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x, bool b) public pure {
+		require(x < 100);
+		while (x < 10) {
+			if (b)
+				x = x + 1;
+			else
+				x = 0;
+		}
+		assert(x > 0);
+	}
+}
+// ----
+// Warning: (177-190): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/loops/while_1_fail.sol b/test/libsolidity/smtCheckerTests/loops/while_1_fail.sol
new file mode 100644
index 00000000..6964f7c8
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/loops/while_1_fail.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x) public pure {
+		require(x < 100);
+		while (x < 10) {
+			x = x + 1;
+		}
+		assert(x < 14);
+	}
+}
+// ----
+// Warning: (139-153): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/loops/while_2_fail.sol b/test/libsolidity/smtCheckerTests/loops/while_2_fail.sol
new file mode 100644
index 00000000..4c52287d
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/loops/while_2_fail.sol
@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+contract C {
+	function f(uint x) public pure {
+		x = 2;
+		while (x > 1) {
+			if (x > 10)
+				x = 2;
+			else
+				x = 10;
+		}
+		assert(x == 2);
+	}
+}
+// ----
+// Warning: (158-172): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_1.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_1.sol
index 074be86f..9b5d04c3 100644
--- a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_1.sol
+++ b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_1.sol
@@ -4,10 +4,10 @@ contract C {
     function f(uint x) public pure {
         x = 2;
         while (x > 1) {
-            x = 2;
+            x = 1;
         }
         assert(x == 2);
     }
 }
 // ----
-// Warning: (194-208): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require().
+// Warning: (194-208): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_3.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_3.sol
index a37df888..f3634edb 100644
--- a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_3.sol
+++ b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_3.sol
@@ -8,4 +8,4 @@ contract C {
     }
 }
 // ----
-// Warning: (187-201): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require().
+// Warning: (187-201): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_4.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_4.sol
index f71da865..5a3aee9e 100644
--- a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_4.sol
+++ b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_4.sol
@@ -8,4 +8,4 @@ contract C {
     }
 }
 // ----
-// Warning: (199-213): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require().
+// Warning: (199-213): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_5.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_5.sol
index 41559c99..6c81e36f 100644
--- a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_5.sol
+++ b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_5.sol
@@ -9,4 +9,4 @@ contract C {
     }
 }
 // ----
-// Warning: (216-230): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require().
+// Warning: (216-230): Assertion violation happens here