[SMTChecker] Support contract type

Changelog.md

@@ -16,6 +16,7 @@ Compiler Features:
  * SMTChecker: Support unary increment and decrement for array and mapping access.
  * SMTChecker: Show unsupported warning for inline assembly blocks.
  * SMTChecker: Support mod.
+ * SMTChecker: Support ``contract`` type.
  * Optimizer: Add rule for shifts by constants larger than 255 for Constantinople.
  * Optimizer: Add rule to simplify certain ANDs and SHL combinations
  * Yul: Adds break and continue keywords to for-loop syntax.

libsolidity/formal/SymbolicTypes.cpp

@@ -134,7 +134,7 @@ pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable(
 		solAssert(fixedBytesType, "");
 		var = make_shared<SymbolicFixedBytesVariable>(fixedBytesType->numBytes(), _uniqueName, _solver);
 	}
-	else if (isAddress(_type.category()))
+	else if (isAddress(_type.category()) || isContract(_type.category()))
 		var = make_shared<SymbolicAddressVariable>(_uniqueName, _solver);
 	else if (isEnum(_type.category()))
 		var = make_shared<SymbolicEnumVariable>(type, _uniqueName, _solver);
@@ -186,6 +186,11 @@ bool dev::solidity::isAddress(Type::Category _category)
 	return _category == Type::Category::Address;
 }
 
+bool dev::solidity::isContract(Type::Category _category)
+{
+	return _category == Type::Category::Contract;
+}
+
 bool dev::solidity::isEnum(Type::Category _category)
 {
 	return _category == Type::Category::Enum;
@@ -197,6 +202,7 @@ bool dev::solidity::isNumber(Type::Category _category)
 		isRational(_category) ||
 		isFixedBytes(_category) ||
 		isAddress(_category) ||
+		isContract(_category) ||
 		isEnum(_category);
 }
 

libsolidity/formal/SymbolicTypes.h

@@ -44,6 +44,7 @@ bool isInteger(Type::Category _category);
 bool isRational(Type::Category _category);
 bool isFixedBytes(Type::Category _category);
 bool isAddress(Type::Category _category);
+bool isContract(Type::Category _category);
 bool isEnum(Type::Category _category);
 bool isNumber(Type::Category _category);
 bool isBool(Type::Category _category);

test/libsolidity/smtCheckerTests/functions/function_call_does_not_clear_local_vars.sol

@@ -9,4 +9,5 @@ contract C {
     }
 }
 // ----
+// Warning: (99-103): Assertion checker does not yet support the type of this variable.
 // Warning: (141-144): Assertion checker does not support recursive function calls.

test/libsolidity/smtCheckerTests/functions/functions_external_1.sol

@@ -17,5 +17,4 @@ contract C
 	}
 }
 // ----
-// Warning: (119-122): Assertion checker does not yet support the type of this variable.
 // Warning: (240-254): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_external_2.sol

@@ -17,5 +17,4 @@ contract C
 	}
 }
 // ----
-// Warning: (139-142): Assertion checker does not yet support the type of this variable.
 // Warning: (280-304): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_external_3.sol

@@ -18,5 +18,4 @@ contract C
 	}
 }
 // ----
-// Warning: (146-149): Assertion checker does not yet support the type of this variable.
 // Warning: (338-362): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/contract.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(C c, C d) public pure {
+		assert(c == d);
+	}
+}
+// ----
+// Warning: (84-98): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/contract_2.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract D
+{
+	uint x;
+}
+
+contract C
+{
+	function f(D c, D d) public pure {
+		assert(c == d);
+	}
+}
+// ----
+// Warning: (109-123): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/contract_3.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(C c, C d, C e) public pure {
+		require(c == d);
+		require(d == e);
+		assert(c == e);
+	}
+}

test/libsolidity/smtCheckerTests/types/contract_address_conversion.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(C c, address a) public pure {
+		assert(address(c) == a);
+	}
+}
+// ----
+// Warning: (90-113): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/contract_address_conversion_2.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(C c, C d) public pure {
+		assert(address(c) == address(c));
+		address a = address(c);
+		require(c == d);
+		assert(a == address(d));
+	}
+}