From b087fa975072bd214aba3b75b578092ebee39411 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 19 Oct 2020 21:46:15 +0100 Subject: [PATCH] [SMTChecker] Fix ICE implicit conversion string literal -> byte --- Changelog.md | 1 + libsolidity/formal/SMTEncoder.cpp | 28 ++++++++++++++----- libsolidity/formal/SMTEncoder.h | 5 ++++ .../smtCheckerTests/operators/slice_bytes.sol | 6 ++++ .../implicit_cast_string_literal_byte.sol | 16 +++++++++++ ...string_literal_to_fixed_bytes_explicit.sol | 4 +++ 6 files changed, 53 insertions(+), 7 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/operators/slice_bytes.sol create mode 100644 test/libsolidity/smtCheckerTests/typecast/implicit_cast_string_literal_byte.sol create mode 100644 test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_explicit.sol diff --git a/Changelog.md b/Changelog.md index f02123341..176137b31 100644 --- a/Changelog.md +++ b/Changelog.md @@ -5,6 +5,7 @@ Compiler Features: Bugfixes: * SMTChecker: Fix lack of reporting potential violations when using only the CHC engine. + * SMTChecker: Fix internal error on conversion from string literal to byte. * Code generator: Fix missing creation dependency tracking for abstract contracts. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index c114b75be..4e338ab5d 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -878,10 +878,8 @@ void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall) if (argSize == castSize) { // If sizes are the same, it's possible that the signs are different. - if (smt::isNumber(*funCallType)) + if (smt::isNumber(*funCallType) && smt::isNumber(*argType)) { - solAssert(smt::isNumber(*argType), ""); - // castIsSigned && !argIsSigned => might overflow if arg > castType.max // !castIsSigned && argIsSigned => might underflow if arg < castType.min // !castIsSigned && !argIsSigned => ok @@ -1211,9 +1209,10 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess) auto arrayVar = dynamic_pointer_cast(array); solAssert(arrayVar, ""); + TypePointer baseType = _indexAccess.baseExpression().annotation().type; defineExpr(_indexAccess, smtutil::Expression::select( arrayVar->elements(), - expr(*_indexAccess.indexExpression()) + expr(*_indexAccess.indexExpression(), keyType(baseType)) )); setSymbolicUnknownValue( expr(_indexAccess), @@ -1245,17 +1244,19 @@ void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expre auto const& base = indexAccess->baseExpression(); if (dynamic_cast(&base)) base.accept(*this); + + TypePointer baseType = base.annotation().type; + auto indexExpr = expr(*indexAccess->indexExpression(), keyType(baseType)); auto symbArray = dynamic_pointer_cast(m_context.expression(base)); solAssert(symbArray, ""); - auto baseType = symbArray->type(); toStore = smtutil::Expression::tuple_constructor( smtutil::Expression(make_shared(smt::smtSort(*baseType)), baseType->toString(true)), - {smtutil::Expression::store(symbArray->elements(), expr(*indexAccess->indexExpression()), toStore), symbArray->length()} + {smtutil::Expression::store(symbArray->elements(), indexExpr, toStore), symbArray->length()} ); m_context.expression(*indexAccess)->increaseIndex(); defineExpr(*indexAccess, smtutil::Expression::select( symbArray->elements(), - expr(*indexAccess->indexExpression()) + indexExpr )); lastExpr = &indexAccess->baseExpression(); } @@ -2239,6 +2240,19 @@ Expression const* SMTEncoder::leftmostBase(IndexAccess const& _indexAccess) return base; } +TypePointer SMTEncoder::keyType(TypePointer _type) +{ + if (auto const* mappingType = dynamic_cast(_type)) + return mappingType->keyType(); + if ( + dynamic_cast(_type) || + dynamic_cast(_type) + ) + return TypeProvider::uint256(); + else + solAssert(false, ""); +} + Expression const* SMTEncoder::innermostTuple(Expression const& _expr) { auto const* tuple = dynamic_cast(&_expr); diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 1fe4e1dcd..fb563412f 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -55,6 +55,11 @@ public: /// @returns the leftmost identifier in a multi-d IndexAccess. static Expression const* leftmostBase(IndexAccess const& _indexAccess); + /// @returns the key type in _type. + /// _type must allow IndexAccess, that is, + /// it must be either ArrayType or MappingType + static TypePointer keyType(TypePointer _type); + /// @returns the innermost element in a chain of 1-tuples if applicable, /// otherwise _expr. static Expression const* innermostTuple(Expression const& _expr); diff --git a/test/libsolidity/smtCheckerTests/operators/slice_bytes.sol b/test/libsolidity/smtCheckerTests/operators/slice_bytes.sol new file mode 100644 index 000000000..d52106e6b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/slice_bytes.sol @@ -0,0 +1,6 @@ +pragma experimental SMTChecker; +contract C { + function f(bytes calldata b) external pure { + ((b[:])[5]); + } +} diff --git a/test/libsolidity/smtCheckerTests/typecast/implicit_cast_string_literal_byte.sol b/test/libsolidity/smtCheckerTests/typecast/implicit_cast_string_literal_byte.sol new file mode 100644 index 000000000..382078ea3 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/typecast/implicit_cast_string_literal_byte.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; + +contract C { + mapping (byte => uint) map; + function f() public { + map[""] = 2; + uint x = map[""]; + g(""); + byte b = ""; + assert(x == map[b]); + assert(x == map["x"]); + } + function g(byte b) internal pure {} +} +// ---- +// Warning 6328: (182-203): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_explicit.sol b/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_explicit.sol new file mode 100644 index 000000000..8c454474b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_explicit.sol @@ -0,0 +1,4 @@ +pragma experimental SMTChecker; +contract SMT { + bytes32 constant internal NULL_BYTES32 = bytes32(''); +}