[SMTChecker] Support enums

Changelog.md

@@ -5,6 +5,7 @@ Language Features:
 
 
 Compiler Features:
+ * SMTChecker: Support enums without typecast.
  * SMTChecker: Support one-dimensional arrays.
  * Yul Optimizer: Add rule to remove empty default switch cases
  * Yul Optimizer: Add rule to remove empty cases if no default exists

libsolidity/formal/SMTChecker.cpp

@@ -736,9 +736,9 @@ bool SMTChecker::visit(MemberAccess const& _memberAccess)
 
 	auto const& exprType = _memberAccess.expression().annotation().type;
 	solAssert(exprType, "");
+	auto identifier = dynamic_cast<Identifier const*>(&_memberAccess.expression());
 	if (exprType->category() == Type::Category::Magic)
 	{
-		auto identifier = dynamic_cast<Identifier const*>(&_memberAccess.expression());
 		string accessedName;
 		if (identifier)
 			accessedName = identifier->name();
@@ -750,12 +750,23 @@ bool SMTChecker::visit(MemberAccess const& _memberAccess)
 		defineGlobalVariable(accessedName + "." + _memberAccess.memberName(), _memberAccess);
 		return false;
 	}
+	else if (exprType->category() == Type::Category::TypeType)
+	{
+		if (identifier && dynamic_cast<EnumDefinition const*>(identifier->annotation().referencedDeclaration))
+		{
+			auto enumType = dynamic_cast<EnumType const*>(accessType.get());
+			solAssert(enumType, "");
+			defineExpr(_memberAccess, enumType->memberValue(_memberAccess.memberName()));
+		}
+		return false;
+	}
 	else
 		m_errorReporter.warning(
 			_memberAccess.location(),
 			"Assertion checker does not yet support this expression."
 		);
 
+	createExpr(_memberAccess);
 	return true;
 }
 

libsolidity/formal/SymbolicTypes.cpp

@@ -135,6 +135,8 @@ pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable(
 	}
 	else if (isAddress(_type.category()))
 		var = make_shared<SymbolicAddressVariable>(_uniqueName, _solver);
+	else if (isEnum(_type.category()))
+		var = make_shared<SymbolicEnumVariable>(type, _uniqueName, _solver);
 	else if (isRational(_type.category()))
 	{
 		auto rational = dynamic_cast<RationalNumberType const*>(&_type);
@@ -183,12 +185,18 @@ bool dev::solidity::isAddress(Type::Category _category)
 	return _category == Type::Category::Address;
 }
 
+bool dev::solidity::isEnum(Type::Category _category)
+{
+	return _category == Type::Category::Enum;
+}
+
 bool dev::solidity::isNumber(Type::Category _category)
 {
 	return isInteger(_category) ||
 		isRational(_category) ||
 		isFixedBytes(_category) ||
-		isAddress(_category);
+		isAddress(_category) ||
+		isEnum(_category);
 }
 
 bool dev::solidity::isBool(Type::Category _category)
@@ -241,7 +249,14 @@ void dev::solidity::smt::setSymbolicUnknownValue(SymbolicVariable const& _variab
 
 void dev::solidity::smt::setSymbolicUnknownValue(smt::Expression _expr, TypePointer const& _type, smt::SolverInterface& _interface)
 {
-	if (isInteger(_type->category()))
+	if (isEnum(_type->category()))
+	{
+		auto enumType = dynamic_cast<EnumType const*>(_type.get());
+		solAssert(enumType, "");
+		_interface.addAssertion(_expr >= 0);
+		_interface.addAssertion(_expr < enumType->numberOfMembers());
+	}
+	else if (isInteger(_type->category()))
 	{
 		auto intType = dynamic_cast<IntegerType const*>(_type.get());
 		solAssert(intType, "");

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 isEnum(Type::Category _category);
 bool isNumber(Type::Category _category);
 bool isBool(Type::Category _category);
 bool isFunction(Type::Category _category);

libsolidity/formal/SymbolicVariables.cpp

@@ -146,3 +146,13 @@ SymbolicArrayVariable::SymbolicArrayVariable(
 {
 	solAssert(isArray(m_type->category()), "");
 }
+
+SymbolicEnumVariable::SymbolicEnumVariable(
+	TypePointer _type,
+	string const& _uniqueName,
+	smt::SolverInterface& _interface
+):
+	SymbolicVariable(move(_type), _uniqueName, _interface)
+{
+	solAssert(isEnum(m_type->category()), "");
+}

libsolidity/formal/SymbolicVariables.h

@@ -166,5 +166,18 @@ public:
 	);
 };
 
+/**
+ * Specialization of SymbolicVariable for Enum
+ */
+class SymbolicEnumVariable: public SymbolicVariable
+{
+public:
+	SymbolicEnumVariable(
+		TypePointer _type,
+		std::string const& _uniqueName,
+		smt::SolverInterface& _interface
+	);
+};
+
 }
 }

test/libsolidity/smtCheckerTests/special/msg_data.sol

@@ -8,5 +8,4 @@ contract C
 }
 // ----
 // Warning: (86-101): Assertion checker does not yet support this expression.
-// Warning: (86-101): Internal error: Expression undefined for SMT solver.
 // Warning: (79-106): Assertion violation happens here

test/libsolidity/smtCheckerTests/typecast/enum_from_uint.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	enum D { Left, Right }
+	function f(uint x) public pure {
+		require(x == 0);
+		D _a = D(x);
+		assert(_a == D.Left);
+	}
+}
+// ----
+// Warning: (132-136): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (140-160): Assertion violation happens here

test/libsolidity/smtCheckerTests/typecast/enum_to_uint_max_value.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	enum D { Left, Right }
+	function f(D _a) public pure {
+		uint x = uint(_a);
+		assert(x < 10);
+	}
+}
+// ----
+// Warning: (113-121): Type conversion is not yet fully supported and might yield false positives.

test/libsolidity/smtCheckerTests/types/enum_explicit_values.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	enum D { Left, Right }
+	D d;
+	function f(D _a) public {
+		require(_a == D.Left);
+		d = D.Right;
+		assert(d != _a);
+	}
+}

test/libsolidity/smtCheckerTests/types/enum_explicit_values_2.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	enum D { Left, Right }
+	D d;
+	function f(D _a) public {
+		require(_a == D.Left);
+		d = D.Left;
+		assert(d != _a);
+	}
+}
+// ----
+// Warning: (144-159): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/enum_in_library.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+library L
+{
+	enum D { Left, Right }
+}
+
+contract C
+{
+	enum E { Left, Right }
+	function f(E _d) internal pure {
+		_d = E.Left;
+		assert(_d == E.Left);
+	}
+}

test/libsolidity/smtCheckerTests/types/enum_in_library_2.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+library L
+{
+	enum D { Left, Right }
+}
+
+contract C
+{
+	enum E { Left, Right }
+	function f(E _d) internal pure {
+		_d = E.Right;
+		assert(_d == E.Left);
+	}
+}
+// ----
+// Warning: (161-181): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/enum_in_struct.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	enum D { Left, Right }
+	struct S { uint x; D d; }
+	function f(S memory s) internal pure {
+		s.d = D.Left;
+		assert(s.d == D.Left);
+	}
+}
+// ----
+// Warning: (109-119): Assertion checker does not yet support the type of this variable.
+// Warning: (139-142): Assertion checker does not yet support this expression.
+// Warning: (139-151): Assertion checker does not yet implement such assignments.
+// Warning: (162-165): Assertion checker does not yet support this expression.
+// Warning: (155-176): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/enum_storage_eq.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	enum D { Left, Right }
+	D d;
+	function f(D _d) public {
+		d = _d;
+		assert(d != _d);
+	}
+}
+// ----
+// Warning: (115-130): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/enum_transitivity.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	enum D { Left, Right }
+	D d;
+	function f(D _a, D _b) public view {
+		require(_a == _b);
+		require(_a == d);
+		assert(d == _b);
+	}
+}

test/libsolidity/smtCheckerTests/types/string_1.sol

@@ -9,6 +9,4 @@ contract C
 // ----
 // Warning: (117-133): Assertion checker does not yet support this expression.
 // Warning: (137-153): Assertion checker does not yet support this expression.
-// Warning: (117-133): Internal error: Expression undefined for SMT solver.
-// Warning: (137-153): Internal error: Expression undefined for SMT solver.
 // Warning: (110-154): Assertion violation happens here