Merge pull request #5717 from ethereum/smt_typecast

[SMTChecker] Support basic typecast without truncation

14 files changed, 181 insertions, 4 deletions

diff --git a/Changelog.md b/Changelog.md
index 56577f63..d3bb8e10 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -6,6 +6,7 @@ Language Features:
 
 Compiler Features:
  * Control Flow Graph: Warn about unreachable code.
+ * SMTChecker: Support basic typecasts without truncation.
 
 
 Bugfixes:
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 35c1e2f1..38715289 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -386,7 +386,7 @@ void SMTChecker::endVisit(BinaryOperation const& _op)
 void SMTChecker::endVisit(FunctionCall const& _funCall)
 {
 	solAssert(_funCall.annotation().kind != FunctionCallKind::Unset, "");
-	if (_funCall.annotation().kind != FunctionCallKind::FunctionCall)
+	if (_funCall.annotation().kind == FunctionCallKind::StructConstructorCall)
 	{
 		m_errorReporter.warning(
 			_funCall.location(),
@@ -395,6 +395,12 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
 		return;
 	}
 
+	if (_funCall.annotation().kind == FunctionCallKind::TypeConversion)
+	{
+		visitTypeConversion(_funCall);
+		return;
+	}
+
 	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
 
 	std::vector<ASTPointer<Expression const>> const args = _funCall.arguments();
@@ -571,6 +577,43 @@ void SMTChecker::endVisit(Identifier const& _identifier)
 	}
 }
 
+void SMTChecker::visitTypeConversion(FunctionCall const& _funCall)
+{
+	solAssert(_funCall.annotation().kind == FunctionCallKind::TypeConversion, "");
+	solAssert(_funCall.arguments().size() == 1, "");
+	auto argument = _funCall.arguments().at(0);
+	unsigned argSize = argument->annotation().type->storageBytes();
+	unsigned castSize = _funCall.annotation().type->storageBytes();
+	if (argSize == castSize)
+		defineExpr(_funCall, expr(*argument));
+	else
+	{
+		createExpr(_funCall);
+		setUnknownValue(*m_expressions.at(&_funCall));
+		auto const& funCallCategory = _funCall.annotation().type->category();
+		// TODO: truncating and bytesX needs a different approach because of right padding.
+		if (funCallCategory == Type::Category::Integer || funCallCategory == Type::Category::Address)
+		{
+			if (argSize < castSize)
+				defineExpr(_funCall, expr(*argument));
+			else
+			{
+				auto const& intType = dynamic_cast<IntegerType const&>(*m_expressions.at(&_funCall)->type());
+				defineExpr(_funCall, smt::Expression::ite(
+					expr(*argument) >= minValue(intType) && expr(*argument) <= maxValue(intType),
+					expr(*argument),
+					expr(_funCall)
+				));
+			}
+		}
+
+		m_errorReporter.warning(
+			_funCall.location(),
+			"Type conversion is not yet fully supported and might yield false positives."
+		);
+	}
+}
+
 void SMTChecker::visitFunctionIdentifier(Identifier const& _identifier)
 {
 	auto const& fType = dynamic_cast<FunctionType const&>(*_identifier.annotation().type);
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index f14d2ac0..caa83764 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -86,6 +86,7 @@ private:
 	void visitAssert(FunctionCall const& _funCall);
 	void visitRequire(FunctionCall const& _funCall);
 	void visitGasLeft(FunctionCall const& _funCall);
+	void visitTypeConversion(FunctionCall const& _funCall);
 	/// Visits the FunctionDefinition of the called function
 	/// if available and inlines the return value.
 	void inlineFunctionCall(FunctionCall const& _funCall);
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