diff --git a/Changelog.md b/Changelog.md index 97935a9c4..24e2b005b 100644 --- a/Changelog.md +++ b/Changelog.md @@ -14,6 +14,7 @@ Compiler Features: * Standard JSON Interface: Compile only selected sources and contracts. * Standard JSON Interface: Provide secondary error locations (e.g. the source position of other conflicting declarations). * SMTChecker: Do not erase knowledge about storage pointers if another storage pointer is assigned. + * SMTChecker: Support string literal type. * Standard JSON Interface: Provide AST even on errors if ``--error-recovery`` commandline switch or StandardCompiler `settings.parserErrorRecovery` is true. * Yul Optimizer: Do not inline function if it would result in expressions being duplicated that are not cheap. @@ -29,6 +30,7 @@ Bugfixes: * SMTChecker: Fix internal error when inlining a function that returns a tuple containing an unsupported type inside a branch. * SMTChecker: Fix internal error when inlining functions that use state variables and belong to a different source. * SMTChecker: Fix internal error when reporting counterexamples concerning state variables from different source files. + * SMTChecker: Fix SMT sort mismatch when using string literals. * View/Pure Checker: Properly detect state variable access through base class. * Yul analyzer: Check availability of data objects already in analysis phase. * Yul Optimizer: Fix an issue where memory-accessing code was removed even though ``msize`` was used in the program. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index ea78e640d..eb1d1bdec 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -187,7 +187,7 @@ void SMTEncoder::endVisit(VariableDeclarationStatement const& _varDecl) declarations.at(i) && m_context.knownVariable(*declarations.at(i)) ) - assignment(*declarations.at(i), components.at(i)->currentValue()); + assignment(*declarations.at(i), components.at(i)->currentValue(declarations.at(i)->type())); } } } @@ -235,30 +235,43 @@ void SMTEncoder::endVisit(Assignment const& _assignment) } else { + auto const& type = _assignment.annotation().type; vector rightArguments; if (_assignment.rightHandSide().annotation().type->category() == Type::Category::Tuple) { - auto symbTuple = dynamic_pointer_cast(m_context.expression(_assignment.rightHandSide())); - solAssert(symbTuple, ""); - for (auto const& component: symbTuple->components()) + auto symbTupleLeft = dynamic_pointer_cast(m_context.expression(_assignment.leftHandSide())); + solAssert(symbTupleLeft, ""); + auto symbTupleRight = dynamic_pointer_cast(m_context.expression(_assignment.rightHandSide())); + solAssert(symbTupleRight, ""); + + auto const& leftComponents = symbTupleLeft->components(); + auto const& rightComponents = symbTupleRight->components(); + solAssert(leftComponents.size() == rightComponents.size(), ""); + + for (unsigned i = 0; i < leftComponents.size(); ++i) { + auto const& left = leftComponents.at(i); + auto const& right = rightComponents.at(i); /// Right hand side tuple component cannot be empty. - solAssert(component, ""); - rightArguments.push_back(component->currentValue()); + solAssert(right, ""); + if (left) + rightArguments.push_back(right->currentValue(left->originalType())); + else + rightArguments.push_back(right->currentValue()); } } else { auto rightHandSide = compoundOps.count(op) ? compoundAssignment(_assignment) : - expr(_assignment.rightHandSide()); + expr(_assignment.rightHandSide(), type); defineExpr(_assignment, rightHandSide); - rightArguments.push_back(expr(_assignment)); + rightArguments.push_back(expr(_assignment, type)); } assignment( _assignment.leftHandSide(), rightArguments, - _assignment.annotation().type, + type, _assignment.location() ); } @@ -620,16 +633,10 @@ void SMTEncoder::endVisit(Literal const& _literal) defineExpr(_literal, smt::Expression(type.literalValue(&_literal))); else if (smt::isBool(type.category())) defineExpr(_literal, smt::Expression(_literal.token() == Token::TrueLiteral ? true : false)); + else if (smt::isStringLiteral(type.category())) + createExpr(_literal); else { - if (type.category() == Type::Category::StringLiteral) - { - auto stringType = TypeProvider::stringMemory(); - auto stringLit = dynamic_cast(_literal.annotation().type); - solAssert(stringLit, ""); - auto result = smt::newSymbolicVariable(*stringType, stringLit->richIdentifier(), m_context); - m_context.createExpression(_literal, result.second); - } m_errorReporter.warning( _literal.location(), "Assertion checker does not yet support the type of this literal (" + @@ -653,7 +660,7 @@ void SMTEncoder::endVisit(Return const& _return) for (unsigned i = 0; i < returnParams.size(); ++i) { solAssert(components.at(i), ""); - m_context.addAssertion(components.at(i)->currentValue() == m_context.newValue(*returnParams.at(i))); + m_context.addAssertion(components.at(i)->currentValue(returnParams.at(i)->type()) == m_context.newValue(*returnParams.at(i))); } } else if (returnParams.size() == 1) @@ -957,14 +964,15 @@ pair SMTEncoder::arithmeticOperation( void SMTEncoder::compareOperation(BinaryOperation const& _op) { - solAssert(_op.annotation().commonType, ""); - if (smt::isSupportedType(_op.annotation().commonType->category())) + auto const& commonType = _op.annotation().commonType; + solAssert(commonType, ""); + if (smt::isSupportedType(commonType->category())) { - smt::Expression left(expr(_op.leftExpression())); - smt::Expression right(expr(_op.rightExpression())); + smt::Expression left(expr(_op.leftExpression(), commonType)); + smt::Expression right(expr(_op.rightExpression(), commonType)); Token op = _op.getOperator(); shared_ptr value; - if (smt::isNumber(_op.annotation().commonType->category())) + if (smt::isNumber(commonType->category())) { value = make_shared( op == Token::Equal ? (left == right) : @@ -977,7 +985,7 @@ void SMTEncoder::compareOperation(BinaryOperation const& _op) } else // Bool { - solUnimplementedAssert(smt::isBool(_op.annotation().commonType->category()), "Operation not yet supported"); + solUnimplementedAssert(smt::isBool(commonType->category()), "Operation not yet supported"); value = make_shared( op == Token::Equal ? (left == right) : /*op == Token::NotEqual*/ (left != right) @@ -1104,7 +1112,7 @@ smt::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment) void SMTEncoder::assignment(VariableDeclaration const& _variable, Expression const& _value) { - assignment(_variable, expr(_value)); + assignment(_variable, expr(_value, _variable.type())); } void SMTEncoder::assignment(VariableDeclaration const& _variable, smt::Expression const& _value) @@ -1258,14 +1266,15 @@ bool SMTEncoder::createVariable(VariableDeclaration const& _varDecl) return true; } -smt::Expression SMTEncoder::expr(Expression const& _e) +smt::Expression SMTEncoder::expr(Expression const& _e, TypePointer _targetType) { if (!m_context.knownExpression(_e)) { m_errorReporter.warning(_e.location(), "Internal error: Expression undefined for SMT solver." ); createExpr(_e); } - return m_context.expression(_e)->currentValue(); + + return m_context.expression(_e)->currentValue(_targetType); } void SMTEncoder::createExpr(Expression const& _e) diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 6342ca617..6ccbe9bcc 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -175,8 +175,10 @@ protected: /// @returns an expression denoting the value of the variable declared in @a _decl /// at the given index. Does not ensure that this index exists. smt::Expression valueAtIndex(VariableDeclaration const& _decl, int _index); - /// Returns the expression corresponding to the AST node. Throws if the expression does not exist. - smt::Expression expr(Expression const& _e); + /// Returns the expression corresponding to the AST node. + /// If _targetType is not null apply conversion. + /// Throws if the expression does not exist. + smt::Expression expr(Expression const& _e, TypePointer _targetType = nullptr); /// Creates the expression (value can be arbitrary) void createExpr(Expression const& _e); /// Creates the expression and sets its value. diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index 40999ea15..6b9f26d82 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -64,6 +64,13 @@ SortPointer smtSort(solidity::Type const& _type) solAssert(mapType, ""); return make_shared(smtSort(*mapType->keyType()), smtSort(*mapType->valueType())); } + else if (isStringLiteral(_type.category())) + { + auto stringLitType = dynamic_cast(&_type); + solAssert(stringLitType, ""); + auto intSort = make_shared(Kind::Int); + return make_shared(intSort, intSort); + } else { solAssert(isArray(_type.category()), ""); @@ -127,19 +134,19 @@ pair> newSymbolicVariable( if (!isSupportedTypeDeclaration(_type)) { abstract = true; - var = make_shared(solidity::TypeProvider::uint256(), _uniqueName, _context); + var = make_shared(solidity::TypeProvider::uint256(), type, _uniqueName, _context); } else if (isBool(_type.category())) var = make_shared(type, _uniqueName, _context); else if (isFunction(_type.category())) var = make_shared(type, _uniqueName, _context); else if (isInteger(_type.category())) - var = make_shared(type, _uniqueName, _context); + var = make_shared(type, type, _uniqueName, _context); else if (isFixedBytes(_type.category())) { auto fixedBytesType = dynamic_cast(type); solAssert(fixedBytesType, ""); - var = make_shared(fixedBytesType->numBytes(), _uniqueName, _context); + var = make_shared(type, fixedBytesType->numBytes(), _uniqueName, _context); } else if (isAddress(_type.category()) || isContract(_type.category())) var = make_shared(_uniqueName, _context); @@ -150,16 +157,21 @@ pair> newSymbolicVariable( auto rational = dynamic_cast(&_type); solAssert(rational, ""); if (rational->isFractional()) - var = make_shared(solidity::TypeProvider::uint256(), _uniqueName, _context); + var = make_shared(solidity::TypeProvider::uint256(), type, _uniqueName, _context); else - var = make_shared(type, _uniqueName, _context); + var = make_shared(type, type, _uniqueName, _context); } else if (isMapping(_type.category())) var = make_shared(type, _uniqueName, _context); else if (isArray(_type.category())) - var = make_shared(type, _uniqueName, _context); + var = make_shared(type, type, _uniqueName, _context); else if (isTuple(_type.category())) var = make_shared(type, _uniqueName, _context); + else if (isStringLiteral(_type.category())) + { + auto stringType = TypeProvider::stringMemory(); + var = make_shared(stringType, type, _uniqueName, _context); + } else solAssert(false, ""); return make_pair(abstract, var); @@ -232,7 +244,8 @@ bool isMapping(solidity::Type::Category _category) bool isArray(solidity::Type::Category _category) { - return _category == solidity::Type::Category::Array; + return _category == solidity::Type::Category::Array || + _category == solidity::Type::Category::StringLiteral; } bool isTuple(solidity::Type::Category _category) @@ -240,6 +253,11 @@ bool isTuple(solidity::Type::Category _category) return _category == solidity::Type::Category::Tuple; } +bool isStringLiteral(solidity::Type::Category _category) +{ + return _category == solidity::Type::Category::StringLiteral; +} + Expression minValue(solidity::IntegerType const& _type) { return Expression(_type.minValue()); diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h index 666cc0f38..355c25328 100644 --- a/libsolidity/formal/SymbolicTypes.h +++ b/libsolidity/formal/SymbolicTypes.h @@ -54,6 +54,7 @@ bool isFunction(solidity::Type::Category _category); bool isMapping(solidity::Type::Category _category); bool isArray(solidity::Type::Category _category); bool isTuple(solidity::Type::Category _category); +bool isStringLiteral(solidity::Type::Category _category); /// Returns a new symbolic variable, according to _type. /// Also returns whether the type is abstract or not, diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp index 907e62f64..3190cc6c6 100644 --- a/libsolidity/formal/SymbolicVariables.cpp +++ b/libsolidity/formal/SymbolicVariables.cpp @@ -27,10 +27,12 @@ using namespace dev::solidity::smt; SymbolicVariable::SymbolicVariable( solidity::TypePointer _type, + solidity::TypePointer _originalType, string _uniqueName, EncodingContext& _context ): - m_type(move(_type)), + m_type(_type), + m_originalType(_originalType), m_uniqueName(move(_uniqueName)), m_context(_context), m_ssa(make_unique()) @@ -53,7 +55,7 @@ SymbolicVariable::SymbolicVariable( solAssert(m_sort, ""); } -Expression SymbolicVariable::currentValue() const +Expression SymbolicVariable::currentValue(solidity::TypePointer const&) const { return valueAtIndex(m_ssa->index()); } @@ -95,17 +97,18 @@ SymbolicBoolVariable::SymbolicBoolVariable( string _uniqueName, EncodingContext& _context ): - SymbolicVariable(move(_type), move(_uniqueName), _context) + SymbolicVariable(_type, _type, move(_uniqueName), _context) { solAssert(m_type->category() == solidity::Type::Category::Bool, ""); } SymbolicIntVariable::SymbolicIntVariable( solidity::TypePointer _type, + solidity::TypePointer _originalType, string _uniqueName, EncodingContext& _context ): - SymbolicVariable(move(_type), move(_uniqueName), _context) + SymbolicVariable(_type, _originalType, move(_uniqueName), _context) { solAssert(isNumber(m_type->category()), ""); } @@ -114,16 +117,17 @@ SymbolicAddressVariable::SymbolicAddressVariable( string _uniqueName, EncodingContext& _context ): - SymbolicIntVariable(TypeProvider::uint(160), move(_uniqueName), _context) + SymbolicIntVariable(TypeProvider::uint(160), TypeProvider::uint(160), move(_uniqueName), _context) { } SymbolicFixedBytesVariable::SymbolicFixedBytesVariable( + solidity::TypePointer _originalType, unsigned _numBytes, string _uniqueName, EncodingContext& _context ): - SymbolicIntVariable(TypeProvider::uint(_numBytes * 8), move(_uniqueName), _context) + SymbolicIntVariable(TypeProvider::uint(_numBytes * 8), _originalType, move(_uniqueName), _context) { } @@ -132,7 +136,7 @@ SymbolicFunctionVariable::SymbolicFunctionVariable( string _uniqueName, EncodingContext& _context ): - SymbolicVariable(move(_type), move(_uniqueName), _context), + SymbolicVariable(_type, _type, move(_uniqueName), _context), m_declaration(m_context.newVariable(currentName(), m_sort)) { solAssert(m_type->category() == solidity::Type::Category::Function, ""); @@ -171,27 +175,41 @@ SymbolicMappingVariable::SymbolicMappingVariable( string _uniqueName, EncodingContext& _context ): - SymbolicVariable(move(_type), move(_uniqueName), _context) + SymbolicVariable(_type, _type, move(_uniqueName), _context) { solAssert(isMapping(m_type->category()), ""); } SymbolicArrayVariable::SymbolicArrayVariable( solidity::TypePointer _type, + solidity::TypePointer _originalType, string _uniqueName, EncodingContext& _context ): - SymbolicVariable(move(_type), move(_uniqueName), _context) + SymbolicVariable(_type, _originalType, move(_uniqueName), _context) { solAssert(isArray(m_type->category()), ""); } +Expression SymbolicArrayVariable::currentValue(solidity::TypePointer const& _targetType) const +{ + if (_targetType) + // StringLiterals are encoded as SMT arrays in the generic case, + // but they can also be compared/assigned to fixed bytes, in which + // case they'd need to be encoded as numbers. + if (auto strType = dynamic_cast(m_originalType)) + if (_targetType->category() == solidity::Type::Category::FixedBytes) + return smt::Expression(u256(toHex(asBytes(strType->value()), HexPrefix::Add))); + + return SymbolicVariable::currentValue(_targetType); +} + SymbolicEnumVariable::SymbolicEnumVariable( solidity::TypePointer _type, string _uniqueName, EncodingContext& _context ): - SymbolicVariable(move(_type), move(_uniqueName), _context) + SymbolicVariable(_type, _type, move(_uniqueName), _context) { solAssert(isEnum(m_type->category()), ""); } @@ -201,7 +219,7 @@ SymbolicTupleVariable::SymbolicTupleVariable( string _uniqueName, EncodingContext& _context ): - SymbolicVariable(move(_type), move(_uniqueName), _context) + SymbolicVariable(_type, _type, move(_uniqueName), _context) { solAssert(isTuple(m_type->category()), ""); } diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h index e6ebb8127..c65a26326 100644 --- a/libsolidity/formal/SymbolicVariables.h +++ b/libsolidity/formal/SymbolicVariables.h @@ -40,6 +40,7 @@ class SymbolicVariable public: SymbolicVariable( solidity::TypePointer _type, + solidity::TypePointer _originalType, std::string _uniqueName, EncodingContext& _context ); @@ -51,7 +52,7 @@ public: virtual ~SymbolicVariable() = default; - Expression currentValue() const; + virtual Expression currentValue(solidity::TypePointer const& _targetType = TypePointer{}) const; std::string currentName() const; virtual Expression valueAtIndex(int _index) const; virtual std::string nameAtIndex(int _index) const; @@ -67,6 +68,7 @@ public: SortPointer const& sort() const { return m_sort; } solidity::TypePointer const& type() const { return m_type; } + solidity::TypePointer const& originalType() const { return m_originalType; } protected: std::string uniqueSymbol(unsigned _index) const; @@ -75,6 +77,8 @@ protected: SortPointer m_sort; /// Solidity type, used for size and range in number types. solidity::TypePointer m_type; + /// Solidity original type, used for type conversion if necessary. + solidity::TypePointer m_originalType; std::string m_uniqueName; EncodingContext& m_context; std::unique_ptr m_ssa; @@ -101,6 +105,7 @@ class SymbolicIntVariable: public SymbolicVariable public: SymbolicIntVariable( solidity::TypePointer _type, + solidity::TypePointer _originalType, std::string _uniqueName, EncodingContext& _context ); @@ -125,6 +130,7 @@ class SymbolicFixedBytesVariable: public SymbolicIntVariable { public: SymbolicFixedBytesVariable( + solidity::TypePointer _originalType, unsigned _numBytes, std::string _uniqueName, EncodingContext& _context @@ -180,9 +186,12 @@ class SymbolicArrayVariable: public SymbolicVariable public: SymbolicArrayVariable( solidity::TypePointer _type, + solidity::TypePointer _originalTtype, std::string _uniqueName, EncodingContext& _context ); + + Expression currentValue(solidity::TypePointer const& _targetType = TypePointer{}) const override; }; /** diff --git a/test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol b/test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol index e1cd1f0de..8404c1a89 100644 --- a/test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol +++ b/test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol @@ -53,9 +53,6 @@ contract MyConc{ // ---- // Warning: (773-792): This declaration shadows an existing declaration. // Warning: (1009-1086): Function state mutability can be restricted to view -// Warning: (327-332): Assertion checker does not yet support the type of this literal (literal_string "abc"). -// Warning: (353-358): Assertion checker does not yet support the type of this literal (literal_string "xyz"). -// Warning: (834-839): Assertion checker does not yet support the type of this literal (literal_string "abc"). // Warning: (874-879): Underflow (resulting value less than 0) happens here. // Warning: (874-879): Overflow (resulting value larger than 2**256 - 1) happens here. // Warning: (985-1002): Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol b/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol index a3ac97dba..6db44a5ef 100644 --- a/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol +++ b/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol @@ -83,7 +83,6 @@ contract InternalCall { // Warning: (1144-1206): Function state mutability can be restricted to pure // Warning: (1212-1274): Function state mutability can be restricted to pure // Warning: (1280-1342): Function state mutability can be restricted to pure -// Warning: (799-811): Assertion checker does not yet support the type of this literal (literal_string "helloTwo()"). // Warning: (782-813): Type conversion is not yet fully supported and might yield false positives. // Warning: (771-814): Assertion checker does not yet implement this type of function call. // Warning: (825-830): Assertion checker does not yet support the type of this variable. diff --git a/test/libsolidity/smtCheckerTests/functions/abi_encode_functions.sol b/test/libsolidity/smtCheckerTests/functions/abi_encode_functions.sol index 6c54e0986..8c3ef4aff 100644 --- a/test/libsolidity/smtCheckerTests/functions/abi_encode_functions.sol +++ b/test/libsolidity/smtCheckerTests/functions/abi_encode_functions.sol @@ -6,7 +6,5 @@ contract C { } // ---- // Warning: (31-64): Experimental features are turned on. Do not use experimental features on live deployments. -// Warning: (173-175): Assertion checker does not yet support the type of this literal (literal_string ""). // Warning: (162-176): Assertion checker does not yet implement this type of function call. -// Warning: (196-202): Assertion checker does not yet support the type of this literal (literal_string "7?8r"). // Warning: (178-203): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/types/string_2.sol b/test/libsolidity/smtCheckerTests/types/string_2.sol index 68f6861b4..44909afd5 100644 --- a/test/libsolidity/smtCheckerTests/types/string_2.sol +++ b/test/libsolidity/smtCheckerTests/types/string_2.sol @@ -8,4 +8,3 @@ contract C } // ---- // Warning: (76-91): Unused local variable. -// Warning: (94-107): Assertion checker does not yet support the type of this literal (literal_string "Hello World"). diff --git a/test/libsolidity/smtCheckerTests/types/string_literal_assignment_1.sol b/test/libsolidity/smtCheckerTests/types/string_literal_assignment_1.sol new file mode 100644 index 000000000..2e805ab7e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/string_literal_assignment_1.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C { + function f(bytes32 _x) public pure { + require(_x == "test"); + bytes32 y = "test"; + bytes16 z = "testz"; + assert(_x == y); + assert(_x == z); + } +} +// ---- +// Warning: (175-190): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/string_literal_assignment_2.sol b/test/libsolidity/smtCheckerTests/types/string_literal_assignment_2.sol new file mode 100644 index 000000000..bd9efea5e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/string_literal_assignment_2.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; + +contract C { + function f(bytes32 _x) public pure { + require(_x == "test"); + (bytes32 y, bytes16 z) = ("test", "testz"); + assert(_x == y); + assert(_x == z); + } +} +// ---- +// Warning: (176-191): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/string_literal_assignment_3.sol b/test/libsolidity/smtCheckerTests/types/string_literal_assignment_3.sol new file mode 100644 index 000000000..730f05cd5 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/string_literal_assignment_3.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; + +contract C { + function f(bytes32 _x) public pure { + require(_x == "test"); + bytes32 y; + bytes16 z; + (y, z) = ("test", "testz"); + assert(_x == y); + assert(_x == z); + } +} +// ---- +// Warning: (186-201): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/string_literal_assignment_4.sol b/test/libsolidity/smtCheckerTests/types/string_literal_assignment_4.sol new file mode 100644 index 000000000..5c1ae89b9 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/string_literal_assignment_4.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; + +contract C { + function g() internal pure returns (bytes32, bytes16) { + return ("test", "testz"); + } + + function f(bytes32 _x) public pure { + require(_x == "test"); + bytes32 y; + bytes16 z; + (y, z) = g(); + assert(_x == y); + assert(_x == z); + } +} +// ---- +// Warning: (261-276): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/string_literal_assignment_5.sol b/test/libsolidity/smtCheckerTests/types/string_literal_assignment_5.sol new file mode 100644 index 000000000..668246647 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/string_literal_assignment_5.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; + +contract C { + function g() internal pure returns (bytes32, bytes16) { + return ("test", "testz"); + } + + function f(bytes32 _x) public pure { + require(_x == "test"); + (bytes32 y, bytes16 z) = g(); + assert(_x == y); + assert(_x == z); + } +} +// ---- +// Warning: (251-266): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/string_literal_comparison_1.sol b/test/libsolidity/smtCheckerTests/types/string_literal_comparison_1.sol new file mode 100644 index 000000000..5f79de141 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/string_literal_comparison_1.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C { + function f(bytes32 _x) public pure { + require(_x == "test"); + bytes32 y = _x; + bytes32 z = _x; + assert(z == "test"); + assert(y == "testx"); + } +} +// ---- +// Warning: (170-190): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/string_literal_comparison_2.sol b/test/libsolidity/smtCheckerTests/types/string_literal_comparison_2.sol new file mode 100644 index 000000000..4a9291f89 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/string_literal_comparison_2.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C { + function f(bytes32 _x) public pure { + require(_x != "test"); + bytes32 y = _x; + bytes32 z = _x; + assert(z == "test"); + assert(y != "testx"); + } +} +// ---- +// Warning: (147-166): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/verification_target/simple_assert_with_require_message.sol b/test/libsolidity/smtCheckerTests/verification_target/simple_assert_with_require_message.sol index bf77fe015..e2fcac7b6 100644 --- a/test/libsolidity/smtCheckerTests/verification_target/simple_assert_with_require_message.sol +++ b/test/libsolidity/smtCheckerTests/verification_target/simple_assert_with_require_message.sol @@ -6,4 +6,3 @@ contract C { } } // ---- -// Warning: (97-125): Assertion checker does not yet support the type of this literal (literal_string "Input number is too large.").