Merge pull request #5717 from ethereum/smt_typecast

[SMTChecker] Support basic typecast without truncation

11 files changed, 135 insertions, 3 deletions

diff --git a/test/libsolidity/smtCheckerTests/complex/warn_on_typecast.sol b/test/libsolidity/smtCheckerTests/complex/warn_on_typecast.sol
index be785414..8ecfe41e 100644
--- a/test/libsolidity/smtCheckerTests/complex/warn_on_typecast.sol
+++ b/test/libsolidity/smtCheckerTests/complex/warn_on_typecast.sol
@@ -5,4 +5,4 @@ contract C {
     }
 }
 // ----
-// Warning: (106-114): Assertion checker does not yet implement this expression.
+// Warning: (106-114): Type conversion is not yet fully supported and might yield false positives.
diff --git a/test/libsolidity/smtCheckerTests/special/msg_sender_2.sol b/test/libsolidity/smtCheckerTests/special/msg_sender_2.sol
index ad45d076..f122f4f2 100644
--- a/test/libsolidity/smtCheckerTests/special/msg_sender_2.sol
+++ b/test/libsolidity/smtCheckerTests/special/msg_sender_2.sol
@@ -10,5 +10,4 @@ contract C
 	}
 }
 // ----
-// Warning: (98-108): Assertion checker does not yet implement this expression.
-// Warning: (98-108): Internal error: Expression undefined for SMT solver.
+// Warning: (98-108): Type conversion is not yet fully supported and might yield false positives.
diff --git a/test/libsolidity/smtCheckerTests/typecast/cast_address_1.sol b/test/libsolidity/smtCheckerTests/typecast/cast_address_1.sol
new file mode 100644
index 00000000..885118a5
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/typecast/cast_address_1.sol
@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(address a) public pure {
+		require(a != address(0));
+		assert(a != address(0));
+	}
+}
+// ----
+// Warning: (98-108): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (125-135): Type conversion is not yet fully supported and might yield false positives.
diff --git a/test/libsolidity/smtCheckerTests/typecast/cast_different_size_1.sol b/test/libsolidity/smtCheckerTests/typecast/cast_different_size_1.sol
new file mode 100644
index 00000000..baacaef1
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/typecast/cast_different_size_1.sol
@@ -0,0 +1,26 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		bytes2 a = 0x1234;
+		uint32 b = uint16(a); // b will be 0x00001234
+		assert(b == 0x1234);
+		uint32 c = uint32(bytes4(a)); // c will be 0x12340000
+		// This fails because right padding is not supported.
+		assert(c == 0x12340000);
+		uint8 d = uint8(uint16(a)); // d will be 0x34
+		// False positive since truncating is not supported yet.
+		assert(d == 0x34);
+		uint8 e = uint8(bytes1(a)); // e will be 0x12
+		// False positive since truncating is not supported yet.
+		assert(e == 0x12);
+	}
+}
+// ----
+// Warning: (186-195): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (280-303): Assertion violation happens here
+// Warning: (317-333): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (414-431): Assertion violation happens here
+// Warning: (451-460): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (542-559): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/typecast/cast_larger_1.sol b/test/libsolidity/smtCheckerTests/typecast/cast_larger_1.sol
new file mode 100644
index 00000000..4b0f42e7
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/typecast/cast_larger_1.sol
@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint8 x) public pure {
+		uint16 y = uint16(x);
+		// True because of x's type
+		assert(y < 300);
+	}
+}
+// ----
+// Warning: (94-103): Type conversion is not yet fully supported and might yield false positives.
diff --git a/test/libsolidity/smtCheckerTests/typecast/cast_larger_2.sol b/test/libsolidity/smtCheckerTests/typecast/cast_larger_2.sol
new file mode 100644
index 00000000..1f981c8c
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/typecast/cast_larger_2.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		uint16 a = 0x1234;
+		uint32 b = uint32(a); // b will be 0x00001234 now
+		// This is correct (left padding).
+		assert(a == b);
+	}
+}
+// ----
+// Warning: (108-117): Type conversion is not yet fully supported and might yield false positives.
diff --git a/test/libsolidity/smtCheckerTests/typecast/cast_larger_2_fail.sol b/test/libsolidity/smtCheckerTests/typecast/cast_larger_2_fail.sol
new file mode 100644
index 00000000..7f707381
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/typecast/cast_larger_2_fail.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		uint16 a = 0x1234;
+		uint32 b = uint32(a); // b will be 0x00001234 now
+		assert(a != b);
+	}
+}
+// ----
+// Warning: (108-117): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (149-163): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/typecast/cast_larger_3.sol b/test/libsolidity/smtCheckerTests/typecast/cast_larger_3.sol
new file mode 100644
index 00000000..cc51639e
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/typecast/cast_larger_3.sol
@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		bytes2 a = 0x1234;
+		bytes4 b = bytes4(a); // b will be 0x12340000
+		// False positive since right padding is not supported yet.
+		assert(b == 0x12340000);
+		// This should fail (right padding).
+		assert(a == b);
+	}
+}
+// ----
+// Warning: (108-117): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (207-230): Assertion violation happens here
+// Warning: (273-287): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/typecast/cast_smaller_1.sol b/test/libsolidity/smtCheckerTests/typecast/cast_smaller_1.sol
new file mode 100644
index 00000000..3e964dfd
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/typecast/cast_smaller_1.sol
@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint16 x) public pure {
+		uint8 y = uint8(x);
+		// True because of y's type
+		assert(y < 300);
+	}
+}
+// ----
+// Warning: (94-102): Type conversion is not yet fully supported and might yield false positives.
diff --git a/test/libsolidity/smtCheckerTests/typecast/cast_smaller_2.sol b/test/libsolidity/smtCheckerTests/typecast/cast_smaller_2.sol
new file mode 100644
index 00000000..25270108
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/typecast/cast_smaller_2.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		uint32 a = 0x12345678;
+		uint16 b = uint16(a); // b will be 0x5678 now
+		// False positive since truncation is not supported yet.
+		assert(b == 0x5678);
+	}
+}
+// ----
+// Warning: (112-121): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (208-227): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/typecast/cast_smaller_3.sol b/test/libsolidity/smtCheckerTests/typecast/cast_smaller_3.sol
new file mode 100644
index 00000000..1c9ea545
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/typecast/cast_smaller_3.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		bytes2 a = 0x1234;
+		bytes1 b = bytes1(a); // b will be 0x12
+		// False positive since truncation is not supported yet.
+		assert(b == 0x12);
+	}
+}
+// ----
+// Warning: (108-117): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (198-215): Assertion violation happens here