Merge pull request #5388 from ethereum/smt_mapping

[SMTChecker] Support for mapping

16 files changed, 218 insertions, 0 deletions

diff --git a/test/libsolidity/smtCheckerTests/types/mapping_1.sol b/test/libsolidity/smtCheckerTests/types/mapping_1.sol
new file mode 100644
index 00000000..4d71ff38
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/mapping_1.sol
@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	mapping (uint => uint) map;
+	function f(uint x) public {
+		map[2] = x;
+		assert(x == map[2]);
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/types/mapping_1_fail.sol b/test/libsolidity/smtCheckerTests/types/mapping_1_fail.sol
new file mode 100644
index 00000000..83c963ad
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/mapping_1_fail.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	mapping (uint => uint) map;
+	function f(uint x) public {
+		map[2] = x;
+		map[2] = 3;
+		assert(x != map[2]);
+	}
+}
+// ----
+// Warning: (134-153): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/types/mapping_2.sol b/test/libsolidity/smtCheckerTests/types/mapping_2.sol
new file mode 100644
index 00000000..06d618bd
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/mapping_2.sol
@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	mapping (uint => bool) map;
+	function f(bool x) public view {
+		assert(x != map[2]);
+	}
+}
+// ----
+// Warning: (111-130): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/types/mapping_2d_1.sol b/test/libsolidity/smtCheckerTests/types/mapping_2d_1.sol
new file mode 100644
index 00000000..b6474903
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/mapping_2d_1.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	mapping (uint => mapping (uint => uint)) map;
+	function f(uint x) public {
+		x = 42;
+		map[13][14] = 42;
+		assert(x == map[13][14]);
+	}
+}
+// ----
+// Warning: (134-145): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
+// Warning: (154-178): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/types/mapping_2d_1_fail.sol b/test/libsolidity/smtCheckerTests/types/mapping_2d_1_fail.sol
new file mode 100644
index 00000000..dd4d568e
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/mapping_2d_1_fail.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	mapping (uint => mapping (uint => uint)) map;
+	function f(uint x) public {
+		x = 41;
+		map[13][14] = 42;
+		assert(x == map[13][14]);
+	}
+}
+// ----
+// Warning: (134-145): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
+// Warning: (154-178): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/types/mapping_3.sol b/test/libsolidity/smtCheckerTests/types/mapping_3.sol
new file mode 100644
index 00000000..985ed3a3
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/mapping_3.sol
@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	mapping (uint => uint) map;
+	function f() public {
+		map[1] = 111;
+		uint x = map[2];
+		map[1] = 112;
+		assert(map[2] == x);
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/types/mapping_3d_1.sol b/test/libsolidity/smtCheckerTests/types/mapping_3d_1.sol
new file mode 100644
index 00000000..6c5f439a
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/mapping_3d_1.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	mapping (uint => mapping (uint => mapping (uint => uint))) map;
+	function f(uint x) public {
+		x = 42;
+		map[13][14][15] = 42;
+		assert(x == map[13][14][15]);
+	}
+}
+// ----
+// Warning: (152-167): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
+// Warning: (176-204): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/types/mapping_3d_1_fail.sol b/test/libsolidity/smtCheckerTests/types/mapping_3d_1_fail.sol
new file mode 100644
index 00000000..dfd4ddaf
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/mapping_3d_1_fail.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	mapping (uint => mapping (uint => mapping (uint => uint))) map;
+	function f(uint x) public {
+		x = 41;
+		map[13][14][15] = 42;
+		assert(x == map[13][14][15]);
+	}
+}
+// ----
+// Warning: (152-167): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
+// Warning: (176-204): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/types/mapping_4.sol b/test/libsolidity/smtCheckerTests/types/mapping_4.sol
new file mode 100644
index 00000000..d0204211
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/mapping_4.sol
@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	mapping (bool => bool) map;
+	function f(bool x) public view {
+		require(x);
+		assert(x != map[x]);
+	}
+}
+// ----
+// Warning: (125-144): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/types/mapping_5.sol b/test/libsolidity/smtCheckerTests/types/mapping_5.sol
new file mode 100644
index 00000000..4acea501
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/mapping_5.sol
@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	mapping (address => uint) map;
+	function f(address a, uint x) public view {
+		assert(x != map[a]);
+	}
+}
+// ----
+// Warning: (125-144): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/types/mapping_aliasing_1.sol b/test/libsolidity/smtCheckerTests/types/mapping_aliasing_1.sol
new file mode 100644
index 00000000..39d096f5
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/mapping_aliasing_1.sol
@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	mapping (uint => uint) a;
+	mapping (uint => uint) b;
+
+	function f() public {
+		require(a[1] == b[1]);
+		a[1] = 2;
+		mapping (uint => uint) storage c = a;
+		assert(c[1] == 2);
+		// False negative! Needs aliasing.
+		assert(a[1] == b[1]);
+	}
+}
+// ----
+// Warning: (261-281): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/types/mapping_as_local_var_1.sol b/test/libsolidity/smtCheckerTests/types/mapping_as_local_var_1.sol
new file mode 100644
index 00000000..e005fbef
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/mapping_as_local_var_1.sol
@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract c {
+	mapping(uint => uint) x;
+	mapping(uint => uint) y;
+	function f(bool cond) public {
+		mapping(uint => uint) storage a = cond ? x : y;
+		x[2] = 1;
+		y[2] = 2;
+		a[2] = 3;
+		// False positive since aliasing is not yet supported.
+		if (cond)
+			assert(a[2] == x[2] && a[2] != y[2]);
+		else
+			assert(a[2] == y[2] && a[2] != x[2]);
+	}
+}
+// ----
+// Warning: (166-178): Internal error: Expression undefined for SMT solver.
+// Warning: (288-324): Assertion violation happens here
+// Warning: (336-372): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/types/mapping_as_parameter_1.sol b/test/libsolidity/smtCheckerTests/types/mapping_as_parameter_1.sol
new file mode 100644
index 00000000..9aeed32b
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/mapping_as_parameter_1.sol
@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract c {
+	mapping(uint => uint) x;
+	function f(mapping(uint => uint) storage map, uint index, uint value) internal {
+		map[index] = value;
+	}
+	function g(uint a, uint b) public {
+		f(x, a, b);
+		// False positive since aliasing is not yet supported.
+		assert(x[a] == b);
+	}
+}
+// ----
+// Warning: (289-306): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/types/mapping_equal_keys_1.sol b/test/libsolidity/smtCheckerTests/types/mapping_equal_keys_1.sol
new file mode 100644
index 00000000..188bc59a
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/mapping_equal_keys_1.sol
@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	mapping (uint => uint) map;
+	function f(uint x, uint y) public view {
+		require(x == y);
+		assert(map[x] == map[y]);
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/types/mapping_equal_keys_2.sol b/test/libsolidity/smtCheckerTests/types/mapping_equal_keys_2.sol
new file mode 100644
index 00000000..93b249df
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/mapping_equal_keys_2.sol
@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	mapping (uint => uint) map;
+	function f(uint x, uint y) public view {
+		assert(x == y);
+		assert(map[x] == map[y]);
+	}
+}
+// ----
+// Warning: (119-133): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/types/mapping_unsupported_key_type_1.sol b/test/libsolidity/smtCheckerTests/types/mapping_unsupported_key_type_1.sol
new file mode 100644
index 00000000..f4e3a65f
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/mapping_unsupported_key_type_1.sol
@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	mapping (string => uint) map;
+	function f(string memory s, uint x) public {
+		map[s] = x;
+		assert(x == map[s]);
+	}
+}
+// ----
+// Warning: (89-104): Assertion checker does not yet support the type of this variable.
+// Warning: (129-130): Internal error: Expression undefined for SMT solver.
+// Warning: (129-130): Assertion checker does not yet implement this type.
+// Warning: (155-156): Internal error: Expression undefined for SMT solver.
+// Warning: (155-156): Assertion checker does not yet implement this type.
+// Warning: (139-158): Assertion violation happens here