diff --git a/Changelog.md b/Changelog.md index 95d2bfd74..84bf50e70 100644 --- a/Changelog.md +++ b/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 diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 679cf7dd3..5853eb97a 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/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(&_memberAccess.expression()); if (exprType->category() == Type::Category::Magic) { - auto identifier = dynamic_cast(&_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(identifier->annotation().referencedDeclaration)) + { + auto enumType = dynamic_cast(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; } diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index 9ee4f726a..e72e22339 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -135,6 +135,8 @@ pair> dev::solidity::newSymbolicVariable( } else if (isAddress(_type.category())) var = make_shared(_uniqueName, _solver); + else if (isEnum(_type.category())) + var = make_shared(type, _uniqueName, _solver); else if (isRational(_type.category())) { auto rational = dynamic_cast(&_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(_type.get()); + solAssert(enumType, ""); + _interface.addAssertion(_expr >= 0); + _interface.addAssertion(_expr < enumType->numberOfMembers()); + } + else if (isInteger(_type->category())) { auto intType = dynamic_cast(_type.get()); solAssert(intType, ""); diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h index 72f6232da..23a0e93d6 100644 --- a/libsolidity/formal/SymbolicTypes.h +++ b/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); diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp index a0a4fcefb..bdc341c43 100644 --- a/libsolidity/formal/SymbolicVariables.cpp +++ b/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()), ""); +} diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h index 9397865ec..89df13f35 100644 --- a/libsolidity/formal/SymbolicVariables.h +++ b/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 + ); +}; + } } diff --git a/test/libsolidity/smtCheckerTests/special/msg_data.sol b/test/libsolidity/smtCheckerTests/special/msg_data.sol index 75bc8e2ba..dff997395 100644 --- a/test/libsolidity/smtCheckerTests/special/msg_data.sol +++ b/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 diff --git a/test/libsolidity/smtCheckerTests/typecast/enum_from_uint.sol b/test/libsolidity/smtCheckerTests/typecast/enum_from_uint.sol new file mode 100644 index 000000000..44c252868 --- /dev/null +++ b/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 diff --git a/test/libsolidity/smtCheckerTests/typecast/enum_to_uint_max_value.sol b/test/libsolidity/smtCheckerTests/typecast/enum_to_uint_max_value.sol new file mode 100644 index 000000000..b061777f9 --- /dev/null +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/types/enum_explicit_values.sol b/test/libsolidity/smtCheckerTests/types/enum_explicit_values.sol new file mode 100644 index 000000000..a474da41f --- /dev/null +++ b/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); + } +} diff --git a/test/libsolidity/smtCheckerTests/types/enum_explicit_values_2.sol b/test/libsolidity/smtCheckerTests/types/enum_explicit_values_2.sol new file mode 100644 index 000000000..3fd43ac9f --- /dev/null +++ b/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 diff --git a/test/libsolidity/smtCheckerTests/types/enum_in_library.sol b/test/libsolidity/smtCheckerTests/types/enum_in_library.sol new file mode 100644 index 000000000..a1648c66e --- /dev/null +++ b/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); + } +} diff --git a/test/libsolidity/smtCheckerTests/types/enum_in_library_2.sol b/test/libsolidity/smtCheckerTests/types/enum_in_library_2.sol new file mode 100644 index 000000000..2bd2afbda --- /dev/null +++ b/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 diff --git a/test/libsolidity/smtCheckerTests/types/enum_in_struct.sol b/test/libsolidity/smtCheckerTests/types/enum_in_struct.sol new file mode 100644 index 000000000..5218683f4 --- /dev/null +++ b/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 diff --git a/test/libsolidity/smtCheckerTests/types/enum_storage_eq.sol b/test/libsolidity/smtCheckerTests/types/enum_storage_eq.sol new file mode 100644 index 000000000..0d8b13627 --- /dev/null +++ b/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 diff --git a/test/libsolidity/smtCheckerTests/types/enum_transitivity.sol b/test/libsolidity/smtCheckerTests/types/enum_transitivity.sol new file mode 100644 index 000000000..8946aae52 --- /dev/null +++ b/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); + } +} diff --git a/test/libsolidity/smtCheckerTests/types/string_1.sol b/test/libsolidity/smtCheckerTests/types/string_1.sol index 0ac635c6c..7f03c29da 100644 --- a/test/libsolidity/smtCheckerTests/types/string_1.sol +++ 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