diff --git a/Changelog.md b/Changelog.md index 01a098d8f..000b23945 100644 --- a/Changelog.md +++ b/Changelog.md @@ -2,24 +2,39 @@ -### 0.7.1 (unreleased) +### 0.7.2 (unreleased) Language Features: - * Allow function definitions outside of contracts, behaving much like internal library functions. +Compiler Features: + * SMTChecker: Support structs. + * Yul Optimizer: Prune unused parameters in functions. + +Bugfixes: + + +### 0.7.1 (2020-09-02) + +Language Features: + * Allow function definitions outside of contracts, behaving much like internal library functions. + * Code generator: Implementing copying structs from calldata to storage. + Compiler Features: * SMTChecker: Add underflow and overflow as verification conditions in the CHC engine. - * Standard JSON Interface: Do not run EVM bytecode code generation, if only Yul IR or EWasm output is requested. - * Yul: Report error when using non-string literals for ``datasize()``, ``dataoffset()``, ``linkersymbol()``, ``loadimmutable()``, ``setimmutable()``. - * Yul Optimizer: LoopInvariantCodeMotion can move reading operations outside for-loops as long as the affected area is not modified inside the loop. - * SMTChecker: Support conditional operator. * SMTChecker: Support bitwise or, xor and not operators. + * SMTChecker: Support conditional operator. + * Standard JSON Interface: Do not run EVM bytecode code generation, if only Yul IR or EWasm output is requested. + * Yul Optimizer: LoopInvariantCodeMotion can move reading operations outside for-loops as long as the affected area is not modified inside the loop. + * Yul: Report error when using non-string literals for ``datasize()``, ``dataoffset()``, ``linkersymbol()``, ``loadimmutable()``, ``setimmutable()``. Bugfixes: * AST: Remove ``null`` member values also when the compiler is used in standard-json-mode. + * General: Allow `type(Contract).name` for abstract contracts and interfaces. + * Immutables: Disallow assigning immutables more than once during their declaration. * Immutables: Properly treat complex assignment and increment/decrement as both reading and writing and thus disallow it everywhere for immutable variables. * Optimizer: Keep side-effects of ``x`` in ``byte(a, shr(b, x))`` even if the constants ``a`` and ``b`` would make the expression zero unconditionally. This optimizer rule is very hard if not impossible to trigger in a way that it can result in invalid code, though. + * References Resolver: Fix internal bug when using constructor for library. * Scanner: Fix bug where whitespace would be allowed within the ``->`` token (e.g. ``function f() - > x {}`` becomes invalid in inline assembly and Yul). * SMTChecker: Fix internal error in BMC function inlining. * SMTChecker: Fix internal error on array implicit conversion. @@ -28,14 +43,11 @@ Bugfixes: * SMTChecker: Fix internal error on tuple assignment. * SMTChecker: Fix internal error on tuples of one element that have tuple type. * SMTChecker: Fix soundness of array ``pop``. - * References Resolver: Fix internal bug when using constructor for library. - * Yul Optimizer: Make function inlining order more resilient to whether or not unrelated source files are present. - * Yul Optimizer: Ensure that Yul keywords are not mistakenly used by the NameDispenser and VarNameCleaners. The bug would manifest as uncompilable code. - * Type Checker: Disallow signed literals as exponent in exponentiation operator. - * Allow `type(Contract).name` for abstract contracts and interfaces. - * Type Checker: Disallow structs containing nested mapping in memory as parameters for library functions. * Type Checker: Disallow ``using for`` directive inside interfaces. - * Immutables: Disallow assigning immutables more than once during their declaration. + * Type Checker: Disallow signed literals as exponent in exponentiation operator. + * Type Checker: Disallow structs containing nested mapping in memory as parameters for library functions. + * Yul Optimizer: Ensure that Yul keywords are not mistakenly used by the NameDispenser and VarNameCleaners. The bug would manifest as uncompilable code. + * Yul Optimizer: Make function inlining order more resilient to whether or not unrelated source files are present. ### 0.7.0 (2020-07-28) diff --git a/cmake/EthToolchains.cmake b/cmake/EthToolchains.cmake index adf0a20a5..c2306bd75 100644 --- a/cmake/EthToolchains.cmake +++ b/cmake/EthToolchains.cmake @@ -1,5 +1,7 @@ # Require C++17. -set(CMAKE_CXX_STANDARD 17) # This requires at least CMake 3.8 to accept this C++17 flag. +if (NOT DEFINED CMAKE_CXX_STANDARD) + set(CMAKE_CXX_STANDARD 17) # This requires at least CMake 3.8 to accept this C++17 flag. +endif () set(CMAKE_CXX_STANDARD_REQUIRED TRUE) set(CMAKE_CXX_EXTENSIONS OFF) diff --git a/docs/bugs_by_version.json b/docs/bugs_by_version.json index fc7191322..4acdc7701 100644 --- a/docs/bugs_by_version.json +++ b/docs/bugs_by_version.json @@ -1185,5 +1185,9 @@ "0.7.0": { "bugs": [], "released": "2020-07-28" + }, + "0.7.1": { + "bugs": [], + "released": "2020-09-02" } } \ No newline at end of file diff --git a/docs/contracts/functions.rst b/docs/contracts/functions.rst index e7c97c33d..cb6b30df5 100644 --- a/docs/contracts/functions.rst +++ b/docs/contracts/functions.rst @@ -277,7 +277,7 @@ neither a receive Ether nor a payable fallback function is present, the contract cannot receive Ether through regular transactions and throws an exception. -In the worst case, the fallback function can only rely on 2300 gas being +In the worst case, the ``receive`` function can only rely on 2300 gas being available (for example when ``send`` or ``transfer`` is used), leaving little room to perform other operations except basic logging. The following operations will consume more gas than the 2300 gas stipend: diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt index 74f4a9a21..5e823d8ee 100644 --- a/libsolidity/CMakeLists.txt +++ b/libsolidity/CMakeLists.txt @@ -100,6 +100,8 @@ set(sources formal/EncodingContext.h formal/ModelChecker.cpp formal/ModelChecker.h + formal/Predicate.cpp + formal/Predicate.h formal/SMTEncoder.cpp formal/SMTEncoder.h formal/SSAVariable.cpp diff --git a/libsolidity/codegen/LValue.cpp b/libsolidity/codegen/LValue.cpp index f4fdd0cbb..576a2d4c0 100644 --- a/libsolidity/codegen/LValue.cpp +++ b/libsolidity/codegen/LValue.cpp @@ -357,38 +357,47 @@ void StorageItem::storeValue(Type const& _sourceType, SourceLocation const& _loc "Struct assignment with conversion." ); solAssert(!structType.containsNestedMapping(), ""); - solAssert(sourceType.location() != DataLocation::CallData, "Structs in calldata not supported."); - for (auto const& member: structType.members(nullptr)) + if (sourceType.location() == DataLocation::CallData) { - // assign each member that can live outside of storage - TypePointer const& memberType = member.type; - solAssert(memberType->nameable(), ""); - TypePointer sourceMemberType = sourceType.memberType(member.name); - if (sourceType.location() == DataLocation::Storage) + solAssert(sourceType.sizeOnStack() == 1, ""); + solAssert(structType.sizeOnStack() == 1, ""); + m_context << Instruction::DUP2 << Instruction::DUP2; + m_context.callYulFunction(m_context.utilFunctions().updateStorageValueFunction(sourceType, structType, 0), 2, 0); + } + else + { + for (auto const& member: structType.members(nullptr)) { - // stack layout: source_ref target_ref - pair const& offsets = sourceType.storageOffsetsOfMember(member.name); - m_context << offsets.first << Instruction::DUP3 << Instruction::ADD; + // assign each member that can live outside of storage + TypePointer const& memberType = member.type; + solAssert(memberType->nameable(), ""); + TypePointer sourceMemberType = sourceType.memberType(member.name); + if (sourceType.location() == DataLocation::Storage) + { + // stack layout: source_ref target_ref + pair const& offsets = sourceType.storageOffsetsOfMember(member.name); + m_context << offsets.first << Instruction::DUP3 << Instruction::ADD; + m_context << u256(offsets.second); + // stack: source_ref target_ref source_member_ref source_member_off + StorageItem(m_context, *sourceMemberType).retrieveValue(_location, true); + // stack: source_ref target_ref source_value... + } + else + { + solAssert(sourceType.location() == DataLocation::Memory, ""); + // stack layout: source_ref target_ref + m_context << sourceType.memoryOffsetOfMember(member.name); + m_context << Instruction::DUP3 << Instruction::ADD; + MemoryItem(m_context, *sourceMemberType).retrieveValue(_location, true); + // stack layout: source_ref target_ref source_value... + } + unsigned stackSize = sourceMemberType->sizeOnStack(); + pair const& offsets = structType.storageOffsetsOfMember(member.name); + m_context << dupInstruction(1 + stackSize) << offsets.first << Instruction::ADD; m_context << u256(offsets.second); - // stack: source_ref target_ref source_member_ref source_member_off - StorageItem(m_context, *sourceMemberType).retrieveValue(_location, true); - // stack: source_ref target_ref source_value... + // stack: source_ref target_ref target_off source_value... target_member_ref target_member_byte_off + StorageItem(m_context, *memberType).storeValue(*sourceMemberType, _location, true); } - else - { - solAssert(sourceType.location() == DataLocation::Memory, ""); - // stack layout: source_ref target_ref - m_context << sourceType.memoryOffsetOfMember(member.name); - m_context << Instruction::DUP3 << Instruction::ADD; - MemoryItem(m_context, *sourceMemberType).retrieveValue(_location, true); - // stack layout: source_ref target_ref source_value... - } - unsigned stackSize = sourceMemberType->sizeOnStack(); - pair const& offsets = structType.storageOffsetsOfMember(member.name); - m_context << dupInstruction(1 + stackSize) << offsets.first << Instruction::ADD; - m_context << u256(offsets.second); - // stack: source_ref target_ref target_off source_value... target_member_ref target_member_byte_off - StorageItem(m_context, *memberType).storeValue(*sourceMemberType, _location, true); } // stack layout: source_ref target_ref solAssert(sourceType.sizeOnStack() == 1, "Unexpected source size."); diff --git a/libsolidity/codegen/YulUtilFunctions.cpp b/libsolidity/codegen/YulUtilFunctions.cpp index 542a67613..b2f3ad8dd 100644 --- a/libsolidity/codegen/YulUtilFunctions.cpp +++ b/libsolidity/codegen/YulUtilFunctions.cpp @@ -964,7 +964,7 @@ string YulUtilFunctions::storageArrayPushFunction(ArrayType const& _type) ("dataAreaFunction", arrayDataAreaFunction(_type)) ("isByteArray", _type.isByteArray()) ("indexAccess", storageArrayIndexAccessFunction(_type)) - ("storeValue", updateStorageValueFunction(*_type.baseType())) + ("storeValue", updateStorageValueFunction(*_type.baseType(), *_type.baseType())) ("maxArrayLength", (u256(1) << 64).str()) ("shl", shiftLeftFunctionDynamic()) ("shr", shiftRightFunction(248)) @@ -994,7 +994,7 @@ string YulUtilFunctions::storageArrayPushZeroFunction(ArrayType const& _type) ("functionName", functionName) ("fetchLength", arrayLengthFunction(_type)) ("indexAccess", storageArrayIndexAccessFunction(_type)) - ("storeValue", updateStorageValueFunction(*_type.baseType())) + ("storeValue", updateStorageValueFunction(*_type.baseType(), *_type.baseType())) ("maxArrayLength", (u256(1) << 64).str()) ("zeroValueFunction", zeroValueFunction(*_type.baseType())) .render(); @@ -1404,15 +1404,35 @@ string YulUtilFunctions::mappingIndexAccessFunction(MappingType const& _mappingT string YulUtilFunctions::readFromStorage(Type const& _type, size_t _offset, bool _splitFunctionTypes) { + if (_type.isValueType()) + return readFromStorageValueType(_type, _offset, _splitFunctionTypes); + else + { + solAssert(_offset == 0, ""); + return readFromStorageReferenceType(_type); + } +} + +string YulUtilFunctions::readFromStorageDynamic(Type const& _type, bool _splitFunctionTypes) +{ + solAssert(_type.isValueType(), ""); + return readFromStorageValueTypeDynamic(_type, _splitFunctionTypes); +} + +string YulUtilFunctions::readFromStorageValueType(Type const& _type, size_t _offset, bool _splitFunctionTypes) +{ + solAssert(_type.isValueType(), ""); + if (_type.category() == Type::Category::Function) solUnimplementedAssert(!_splitFunctionTypes, ""); string functionName = - "read_from_storage_" + - string(_splitFunctionTypes ? "split_" : "") + - "offset_" + - to_string(_offset) + - "_" + - _type.identifier(); + "read_from_storage_" + + string(_splitFunctionTypes ? "split_" : "") + + "offset_" + + to_string(_offset) + + "_" + + _type.identifier(); + return m_functionCollector.createFunction(functionName, [&] { solAssert(_type.sizeOnStack() == 1, ""); return Whiskers(R"( @@ -1420,18 +1440,19 @@ string YulUtilFunctions::readFromStorage(Type const& _type, size_t _offset, bool value := (sload(slot)) } )") - ("functionName", functionName) - ("extract", extractFromStorageValue(_type, _offset, false)) - .render(); + ("functionName", functionName) + ("extract", extractFromStorageValue(_type, _offset, false)) + .render(); }); } - -string YulUtilFunctions::readFromStorageDynamic(Type const& _type, bool _splitFunctionTypes) +string YulUtilFunctions::readFromStorageValueTypeDynamic(Type const& _type, bool _splitFunctionTypes) { + solAssert(_type.isValueType(), ""); if (_type.category() == Type::Category::Function) solUnimplementedAssert(!_splitFunctionTypes, ""); + string functionName = - "read_from_storage_dynamic" + + "read_from_storage_value_type_dynamic" + string(_splitFunctionTypes ? "split_" : "") + "_" + _type.identifier(); @@ -1447,6 +1468,55 @@ string YulUtilFunctions::readFromStorageDynamic(Type const& _type, bool _splitFu .render(); }); } +string YulUtilFunctions::readFromStorageReferenceType(Type const& _type) +{ + solUnimplementedAssert(_type.category() == Type::Category::Struct, ""); + + string functionName = "read_from_storage_reference_type_" + _type.identifier(); + + auto const& structType = dynamic_cast(_type); + solAssert(structType.location() == DataLocation::Memory, ""); + MemberList::MemberMap structMembers = structType.nativeMembers(nullptr); + vector> memberSetValues(structMembers.size()); + for (size_t i = 0; i < structMembers.size(); ++i) + { + auto const& [memberSlotDiff, memberStorageOffset] = structType.storageOffsetsOfMember(structMembers[i].name); + + memberSetValues[i]["setMember"] = Whiskers(R"( + { + let := (add(slot, ), ) + (add(value, ), ) + } + )") + ("memberValues", suffixedVariableNameList("memberValue_", 0, structMembers[i].type->stackItems().size())) + ("memberMemoryOffset", structType.memoryOffsetOfMember(structMembers[i].name).str()) + ("memberSlotDiff", memberSlotDiff.str()) + ("memberStorageOffset", to_string(memberStorageOffset)) + ("readFromStorage", + structMembers[i].type->isValueType() ? + readFromStorageDynamic(*structMembers[i].type, true) : + readFromStorage(*structMembers[i].type, memberStorageOffset, true) + ) + ("writeToMemory", writeToMemoryFunction(*structMembers[i].type)) + ("hasOffset", structMembers[i].type->isValueType()) + .render(); + } + + return m_functionCollector.createFunction(functionName, [&] { + return Whiskers(R"( + function (slot) -> value { + value := () + <#member> + + + } + )") + ("functionName", functionName) + ("allocStruct", allocateMemoryStructFunction(structType)) + ("member", memberSetValues) + .render(); + }); +} string YulUtilFunctions::readFromMemory(Type const& _type) { @@ -1458,18 +1528,25 @@ string YulUtilFunctions::readFromCalldata(Type const& _type) return readFromMemoryOrCalldata(_type, true); } -string YulUtilFunctions::updateStorageValueFunction(Type const& _type, std::optional const& _offset) +string YulUtilFunctions::updateStorageValueFunction( + Type const& _fromType, + Type const& _toType, + std::optional const& _offset +) { string const functionName = "update_storage_value_" + (_offset.has_value() ? ("offset_" + to_string(*_offset)) : "") + - _type.identifier(); + _fromType.identifier() + + "_to_" + + _toType.identifier(); return m_functionCollector.createFunction(functionName, [&] { - if (_type.isValueType()) + if (_toType.isValueType()) { - solAssert(_type.storageBytes() <= 32, "Invalid storage bytes size."); - solAssert(_type.storageBytes() > 0, "Invalid storage bytes size."); + solAssert(_fromType.isImplicitlyConvertibleTo(_toType), ""); + solAssert(_toType.storageBytes() <= 32, "Invalid storage bytes size."); + solAssert(_toType.storageBytes() > 0, "Invalid storage bytes size."); return Whiskers(R"( function (slot, value) { @@ -1480,19 +1557,83 @@ string YulUtilFunctions::updateStorageValueFunction(Type const& _type, std::opti ("functionName", functionName) ("update", _offset.has_value() ? - updateByteSliceFunction(_type.storageBytes(), *_offset) : - updateByteSliceFunctionDynamic(_type.storageBytes()) + updateByteSliceFunction(_toType.storageBytes(), *_offset) : + updateByteSliceFunctionDynamic(_toType.storageBytes()) ) ("offset", _offset.has_value() ? "" : "offset, ") - ("prepare", prepareStoreFunction(_type)) + ("prepare", prepareStoreFunction(_toType)) .render(); } else { - if (_type.category() == Type::Category::Array) - solUnimplementedAssert(false, ""); - else if (_type.category() == Type::Category::Struct) + auto const* toReferenceType = dynamic_cast(&_toType); + auto const* fromReferenceType = dynamic_cast(&_toType); + solAssert(fromReferenceType && toReferenceType, ""); + solAssert(*toReferenceType->copyForLocation( + fromReferenceType->location(), + fromReferenceType->isPointer() + ).get() == *fromReferenceType, ""); + + if (_toType.category() == Type::Category::Array) solUnimplementedAssert(false, ""); + else if (_toType.category() == Type::Category::Struct) + { + solAssert(_fromType.category() == Type::Category::Struct, ""); + auto const& fromStructType = dynamic_cast(_fromType); + auto const& toStructType = dynamic_cast(_toType); + solAssert(fromStructType.structDefinition() == toStructType.structDefinition(), ""); + solAssert(fromStructType.location() != DataLocation::Storage, ""); + solUnimplementedAssert(_offset.has_value() && _offset.value() == 0, ""); + + Whiskers templ(R"( + function (slot, value) { + <#member> + { + + } + + } + )"); + templ("functionName", functionName); + + MemberList::MemberMap structMembers = fromStructType.nativeMembers(nullptr); + + vector> memberParams(structMembers.size()); + for (size_t i = 0; i < structMembers.size(); ++i) + { + solAssert(structMembers[i].type->memoryHeadSize() == 32, ""); + bool fromCalldata = fromStructType.location() == DataLocation::CallData; + auto const& [slotDiff, offset] = toStructType.storageOffsetsOfMember(structMembers[i].name); + memberParams[i]["updateMemberCall"] = Whiskers(R"( + let := (add(value, )) + (add(slot, ), , ) + )") + ("memberValues", suffixedVariableNameList( + "memberValue_", + 0, + structMembers[i].type->stackItems().size() + )) + ("hasOffset", structMembers[i].type->isValueType()) + ( + "updateMember", + structMembers[i].type->isValueType() ? + updateStorageValueFunction(*structMembers[i].type, *structMembers[i].type) : + updateStorageValueFunction(*structMembers[i].type, *structMembers[i].type, offset) + ) + ("memberStorageSlotDiff", slotDiff.str()) + ("memberStorageOffset", to_string(offset)) + ("memberOffset", + fromCalldata ? + to_string(fromStructType.calldataOffsetOfMember(structMembers[i].name)) : + fromStructType.memoryOffsetOfMember(structMembers[i].name).str() + ) + ("loadFromMemoryOrCalldata", readFromMemoryOrCalldata(*structMembers[i].type, fromCalldata)) + .render(); + } + templ("member", memberParams); + + return templ.render(); + } else solAssert(false, "Invalid non-value type for assignment."); } @@ -2052,13 +2193,27 @@ string YulUtilFunctions::conversionFunction(Type const& _from, Type const& _to) solUnimplementedAssert(!fromStructType.isDynamicallyEncoded(), ""); solUnimplementedAssert(toStructType.location() == DataLocation::Memory, ""); - solUnimplementedAssert(fromStructType.location() == DataLocation::CallData, ""); + solUnimplementedAssert(fromStructType.location() != DataLocation::Memory, ""); + + if (fromStructType.location() == DataLocation::CallData) + { + body = Whiskers(R"( + converted := (value, calldatasize()) + )")("abiDecode", ABIFunctions(m_evmVersion, m_revertStrings, m_functionCollector).tupleDecoder( + {&toStructType} + )).render(); + } + else + { + solAssert(fromStructType.location() == DataLocation::Storage, ""); + + body = Whiskers(R"( + converted := (value) + )") + ("readFromStorage", readFromStorage(toStructType, 0, true)) + .render(); + } - body = Whiskers(R"( - converted := (value, calldatasize()) - )")("abiDecode", ABIFunctions(m_evmVersion, m_revertStrings, m_functionCollector).tupleDecoder( - {&toStructType} - )).render(); break; } case Type::Category::FixedBytes: @@ -2490,7 +2645,7 @@ string YulUtilFunctions::storageSetToZeroFunction(Type const& _type) } )") ("functionName", functionName) - ("store", updateStorageValueFunction(_type)) + ("store", updateStorageValueFunction(_type, _type)) ("zeroValue", zeroValueFunction(_type)) .render(); else if (_type.category() == Type::Category::Array) diff --git a/libsolidity/codegen/YulUtilFunctions.h b/libsolidity/codegen/YulUtilFunctions.h index 7af910a6d..8394c33af 100644 --- a/libsolidity/codegen/YulUtilFunctions.h +++ b/libsolidity/codegen/YulUtilFunctions.h @@ -221,8 +221,7 @@ public: /// @param _keyType the type of the value provided std::string mappingIndexAccessFunction(MappingType const& _mappingType, Type const& _keyType); - /// @returns a function that reads a value type from storage. - /// Performs bit mask/sign extend cleanup and appropriate left / right shift, but not validation. + /// @returns a function that reads a type from storage. /// @param _splitFunctionTypes if false, returns the address and function signature in a /// single variable. std::string readFromStorage(Type const& _type, size_t _offset, bool _splitFunctionTypes); @@ -248,7 +247,11 @@ public: /// the specified slot and offset. If offset is not given, it is expected as /// runtime parameter. /// signature: (slot, [offset,] value) - std::string updateStorageValueFunction(Type const& _type, std::optional const& _offset = std::optional()); + std::string updateStorageValueFunction( + Type const& _fromType, + Type const& _toType, + std::optional const& _offset = std::optional() + ); /// Returns the name of a function that will write the given value to /// the specified address. @@ -401,6 +404,16 @@ private: std::string readFromMemoryOrCalldata(Type const& _type, bool _fromCalldata); + /// @returns a function that reads a value type from storage. + /// Performs bit mask/sign extend cleanup and appropriate left / right shift, but not validation. + /// @param _splitFunctionTypes if false, returns the address and function signature in a + /// single variable. + std::string readFromStorageValueType(Type const& _type, size_t _offset, bool _splitFunctionTypes); + std::string readFromStorageValueTypeDynamic(Type const& _type, bool _splitFunctionTypes); + + /// @returns a function that reads a reference type from storage to memory (performing a deep copy). + std::string readFromStorageReferenceType(Type const& _type); + langutil::EVMVersion m_evmVersion; RevertStrings m_revertStrings; MultiUseYulFunctionCollector& m_functionCollector; diff --git a/libsolidity/codegen/ir/IRGeneratorForStatements.cpp b/libsolidity/codegen/ir/IRGeneratorForStatements.cpp index 3ab3c8888..cacfade33 100644 --- a/libsolidity/codegen/ir/IRGeneratorForStatements.cpp +++ b/libsolidity/codegen/ir/IRGeneratorForStatements.cpp @@ -314,9 +314,9 @@ bool IRGeneratorForStatements::visit(Assignment const& _assignment) writeToLValue(*m_currentLValue, value); - m_currentLValue.reset(); - if (*_assignment.annotation().type != *TypeProvider::emptyTuple()) + if (m_currentLValue->type.category() != Type::Category::Struct && *_assignment.annotation().type != *TypeProvider::emptyTuple()) define(_assignment, value); + m_currentLValue.reset(); return false; } @@ -749,8 +749,18 @@ void IRGeneratorForStatements::endVisit(FunctionCall const& _functionCall) if (identifier) functionDef = &functionDef->resolveVirtual(m_context.mostDerivedContract()); + else + { + ContractType const* type = dynamic_cast(memberAccess->expression().annotation().type); + if (type && type->isSuper()) + { + ContractDefinition const* super = type->contractDefinition().superContract(m_context.mostDerivedContract()); + solAssert(super, "Super contract not available."); + functionDef = &functionDef->resolveVirtual(m_context.mostDerivedContract(), super); + } + } - solAssert(functionDef->isImplemented(), ""); + solAssert(functionDef && functionDef->isImplemented(), ""); } solAssert(!functionType->takesArbitraryParameters(), ""); @@ -1397,7 +1407,17 @@ void IRGeneratorForStatements::endVisit(MemberAccess const& _memberAccess) ContractType const& type = dynamic_cast(*_memberAccess.expression().annotation().type); if (type.isSuper()) { - solUnimplementedAssert(false, ""); + solAssert(!!_memberAccess.annotation().referencedDeclaration, "Referenced declaration not resolved."); + ContractDefinition const* super = type.contractDefinition().superContract(m_context.mostDerivedContract()); + solAssert(super, "Super contract not available."); + FunctionDefinition const& resolvedFunctionDef = dynamic_cast( + *_memberAccess.annotation().referencedDeclaration + ).resolveVirtual(m_context.mostDerivedContract(), super); + + define(_memberAccess) << to_string(resolvedFunctionDef.id()) << "\n"; + solAssert(resolvedFunctionDef.functionType(true), ""); + solAssert(resolvedFunctionDef.functionType(true)->kind() == FunctionType::Kind::Internal, ""); + m_context.internalFunctionAccessed(_memberAccess, resolvedFunctionDef); } // ordinary contract type else if (Declaration const* declaration = _memberAccess.annotation().referencedDeclaration) @@ -2486,7 +2506,7 @@ void IRGeneratorForStatements::writeToLValue(IRLValue const& _lvalue, IRVariable offset = std::get(_storage.offset); m_code << - m_utils.updateStorageValueFunction(_lvalue.type, offset) << + m_utils.updateStorageValueFunction(_value.type(), _lvalue.type, offset) << "(" << _storage.slot << ( diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index 503f48da8..a47ca647f 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -580,7 +580,7 @@ pair, vector> BMC::modelExpressions() auto const& type = var.second->type(); if ( type->isValueType() && - smt::smtKind(type->category()) != smtutil::Kind::Function + smt::smtKind(*type) != smtutil::Kind::Function ) { expressionsToEvaluate.emplace_back(var.second->currentValue()); diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 65df7e203..f6a3b5aae 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -29,7 +29,6 @@ #include #include -#include #include #include @@ -85,11 +84,7 @@ void CHC::analyze(SourceUnit const& _source) resetSourceAnalysis(); - auto genesisSort = make_shared( - vector(), - smtutil::SortProvider::boolSort - ); - m_genesisPredicate = createSymbolicBlock(genesisSort, "genesis"); + m_genesisPredicate = createSymbolicBlock(arity0FunctionSort(), "genesis"); addRule(genesis(), "genesis"); set sources; @@ -118,16 +113,14 @@ bool CHC::visit(ContractDefinition const& _contract) initContract(_contract); - m_stateVariables = stateVariablesIncludingInheritedAndPrivate(_contract); + m_stateVariables = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract); m_stateSorts = stateSorts(_contract); clearIndices(&_contract); string suffix = _contract.name() + "_" + to_string(_contract.id()); - m_errorPredicate = createSymbolicBlock(arity0FunctionSort(), "error_" + suffix); - m_constructorSummaryPredicate = createSymbolicBlock(constructorSort(), "summary_constructor_" + suffix); - m_symbolFunction[m_constructorSummaryPredicate->currentFunctionValue().name] = &_contract; - m_implicitConstructorPredicate = createSymbolicBlock(arity0FunctionSort(), "implicit_constructor_" + suffix); + m_constructorSummaryPredicate = createSymbolicBlock(constructorSort(), "summary_constructor_" + suffix, &_contract); + m_implicitConstructorPredicate = createSymbolicBlock(arity0FunctionSort(), "implicit_constructor_" + suffix, &_contract); auto stateExprs = currentStateVariables(); setCurrentBlock(*m_interfaces.at(m_currentContract), &stateExprs); @@ -233,7 +226,7 @@ void CHC::endVisit(FunctionDefinition const& _function) if (_function.isConstructor()) { string suffix = m_currentContract->name() + "_" + to_string(m_currentContract->id()); - auto constructorExit = createSymbolicBlock(constructorSort(), "constructor_exit_" + suffix); + auto constructorExit = createSymbolicBlock(constructorSort(), "constructor_exit_" + suffix, m_currentContract); connectBlocks(m_currentBlock, predicate(*constructorExit, currentFunctionVariables(*m_currentContract))); clearIndices(m_currentContract, m_currentFunction); @@ -326,8 +319,8 @@ bool CHC::visit(WhileStatement const& _while) auto outerBreakDest = m_breakDest; auto outerContinueDest = m_continueDest; - m_breakDest = afterLoopBlock.get(); - m_continueDest = loopHeaderBlock.get(); + m_breakDest = afterLoopBlock; + m_continueDest = loopHeaderBlock; if (_while.isDoWhile()) _while.body().accept(*this); @@ -377,8 +370,8 @@ bool CHC::visit(ForStatement const& _for) auto outerBreakDest = m_breakDest; auto outerContinueDest = m_continueDest; - m_breakDest = afterLoopBlock.get(); - m_continueDest = postLoop ? postLoopBlock.get() : loopHeaderBlock.get(); + m_breakDest = afterLoopBlock; + m_continueDest = postLoop ? postLoopBlock : loopHeaderBlock; if (auto init = _for.initializationExpression()) init->accept(*this); @@ -571,7 +564,6 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall) m_context.variable(*var)->increaseIndex(); auto nondet = (*m_nondetInterfaces.at(m_currentContract))(preCallState + currentStateVariables()); - m_symbolFunction[nondet.name] = &_funCall; m_context.addAssertion(nondet); m_context.addAssertion(m_error.currentValue() == 0); @@ -681,7 +673,9 @@ void CHC::resetSourceAnalysis() m_errorIds.clear(); m_callGraph.clear(); m_summaries.clear(); - m_symbolFunction.clear(); + m_interfaces.clear(); + m_nondetInterfaces.clear(); + Predicate::reset(); } void CHC::resetContractAnalysis() @@ -717,7 +711,7 @@ void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition c } void CHC::setCurrentBlock( - smt::SymbolicFunctionVariable const& _block, + Predicate const& _block, vector const* _arguments ) { @@ -743,24 +737,10 @@ set CHC::transactionAssertions(ASTN return assertions; } -vector CHC::stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract) -{ - return fold( - _contract.annotation().linearizedBaseContracts, - vector{}, - [](auto&& _acc, auto _contract) { return _acc + _contract->stateVariables(); } - ); -} - -vector CHC::stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function) -{ - return stateVariablesIncludingInheritedAndPrivate(dynamic_cast(*_function.scope())); -} - vector CHC::stateSorts(ContractDefinition const& _contract) { return applyMap( - stateVariablesIncludingInheritedAndPrivate(_contract), + SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); } ); } @@ -806,7 +786,7 @@ smtutil::SortPointer CHC::nondetInterfaceSort(ContractDefinition const& _contrac ); } -smtutil::SortPointer CHC::arity0FunctionSort() +smtutil::SortPointer CHC::arity0FunctionSort() const { return make_shared( vector(), @@ -853,7 +833,7 @@ smtutil::SortPointer CHC::sort(ASTNode const* _node) smtutil::SortPointer CHC::summarySort(FunctionDefinition const& _function, ContractDefinition const& _contract) { - auto stateVariables = stateVariablesIncludingInheritedAndPrivate(_contract); + auto stateVariables = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract); auto sorts = stateSorts(_contract); auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); }; @@ -870,14 +850,10 @@ smtutil::SortPointer CHC::summarySort(FunctionDefinition const& _function, Contr ); } -unique_ptr CHC::createSymbolicBlock(smtutil::SortPointer _sort, string const& _name) +Predicate const* CHC::createSymbolicBlock(SortPointer _sort, string const& _name, ASTNode const* _node) { - auto block = make_unique( - _sort, - _name, - m_context - ); - m_interface->registerRelation(block->currentFunctionValue()); + auto const* block = Predicate::create(_sort, _name, m_context, _node); + m_interface->registerRelation(block->functor()); return block; } @@ -887,20 +863,24 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source) if (auto const* contract = dynamic_cast(node.get())) for (auto const* base: contract->annotation().linearizedBaseContracts) { - string suffix = base->name() + "_" + to_string(base->id()); - m_interfaces[base] = createSymbolicBlock(interfaceSort(*base), "interface_" + suffix); - m_nondetInterfaces[base] = createSymbolicBlock(nondetInterfaceSort(*base), "nondet_interface_" + suffix); - - for (auto const* var: stateVariablesIncludingInheritedAndPrivate(*base)) + for (auto const* var: SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*base)) if (!m_context.knownVariable(*var)) createVariable(*var); - /// Base nondeterministic interface that allows - /// 0 steps to be taken, used as base for the inductive - /// rule for each function. - auto const& iface = *m_nondetInterfaces.at(base); - auto state0 = stateVariablesAtIndex(0, *base); - addRule(iface(state0 + state0), "base_nondet"); + if (!m_interfaces.count(base)) + { + solAssert(!m_nondetInterfaces.count(base), ""); + string suffix = base->name() + "_" + to_string(base->id()); + m_interfaces.emplace(base, createSymbolicBlock(interfaceSort(*base), "interface_" + suffix, base)); + m_nondetInterfaces.emplace(base, createSymbolicBlock(nondetInterfaceSort(*base), "nondet_interface_" + suffix, base)); + + /// Base nondeterministic interface that allows + /// 0 steps to be taken, used as base for the inductive + /// rule for each function. + auto const* iface = m_nondetInterfaces.at(base); + auto state0 = stateVariablesAtIndex(0, *base); + addRule((*iface)(state0 + state0), "base_nondet"); + } for (auto const* function: base->definedFunctions()) { @@ -923,8 +903,10 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source) auto state1 = stateVariablesAtIndex(1, *base); auto state2 = stateVariablesAtIndex(2, *base); - auto nondetPre = iface(state0 + state1); - auto nondetPost = iface(state0 + state2); + auto const* iface = m_nondetInterfaces.at(base); + auto state0 = stateVariablesAtIndex(0, *base); + auto nondetPre = (*iface)(state0 + state1); + auto nondetPost = (*iface)(state0 + state2); vector args{m_error.currentValue()}; args += state1 + @@ -960,7 +942,7 @@ smtutil::Expression CHC::error() smtutil::Expression CHC::error(unsigned _idx) { - return m_errorPredicate->functionValueAtIndex(_idx)({}); + return m_errorPredicate->functor(_idx)({}); } smtutil::Expression CHC::summary(ContractDefinition const& _contract) @@ -994,37 +976,33 @@ smtutil::Expression CHC::summary(FunctionDefinition const& _function) return summary(_function, *m_currentContract); } -unique_ptr CHC::createBlock(ASTNode const* _node, string const& _prefix) +Predicate const* CHC::createBlock(ASTNode const* _node, string const& _prefix) { - auto block = createSymbolicBlock(sort(_node), - "block_" + - uniquePrefix() + - "_" + - _prefix + - predicateName(_node)); + auto block = createSymbolicBlock( + sort(_node), + "block_" + uniquePrefix() + "_" + _prefix + predicateName(_node), + _node + ); solAssert(m_currentFunction, ""); - m_symbolFunction[block->currentFunctionValue().name] = m_currentFunction; return block; } -unique_ptr CHC::createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract) +Predicate const* CHC::createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract) { - auto block = createSymbolicBlock(summarySort(_function, _contract), - "summary_" + - uniquePrefix() + - "_" + - predicateName(&_function, &_contract)); + auto block = createSymbolicBlock( + summarySort(_function, _contract), + "summary_" + uniquePrefix() + "_" + predicateName(&_function, &_contract), + &_function + ); - m_symbolFunction[block->currentFunctionValue().name] = &_function; return block; } void CHC::createErrorBlock() { - solAssert(m_errorPredicate, ""); - m_errorPredicate->increaseIndex(); - m_interface->registerRelation(m_errorPredicate->currentFunctionValue()); + m_errorPredicate = createSymbolicBlock(arity0FunctionSort(), "error_target_" + to_string(m_context.newUniqueId())); + m_interface->registerRelation(m_errorPredicate->functor()); } void CHC::connectBlocks(smtutil::Expression const& _from, smtutil::Expression const& _to, smtutil::Expression const& _constraints) @@ -1055,7 +1033,7 @@ vector CHC::stateVariablesAtIndex(unsigned _index) vector CHC::stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract) { return applyMap( - stateVariablesIncludingInheritedAndPrivate(_contract), + SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), [&](auto _var) { return valueAtIndex(*_var, _index); } ); } @@ -1068,7 +1046,7 @@ vector CHC::currentStateVariables() vector CHC::currentStateVariables(ContractDefinition const& _contract) { - return applyMap(stateVariablesIncludingInheritedAndPrivate(_contract), [this](auto _var) { return currentValue(*_var); }); + return applyMap(SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), [this](auto _var) { return currentValue(*_var); }); } vector CHC::currentFunctionVariables() @@ -1128,13 +1106,13 @@ string CHC::predicateName(ASTNode const* _node, ContractDefinition const* _contr return prefix + "_" + to_string(_node->id()) + "_" + to_string(contract->id()); } -smtutil::Expression CHC::predicate(smt::SymbolicFunctionVariable const& _block) +smtutil::Expression CHC::predicate(Predicate const& _block) { return _block(currentBlockVariables()); } smtutil::Expression CHC::predicate( - smt::SymbolicFunctionVariable const& _block, + Predicate const& _block, vector const& _arguments ) { @@ -1425,42 +1403,31 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& solAssert(edges.size() <= 2, ""); unsigned summaryId = edges.at(0); - optional interfaceId; if (edges.size() == 2) { interfaceId = edges.at(1); - if (_graph.nodes.at(summaryId).first.rfind("summary", 0) != 0) + if (!Predicate::predicate(_graph.nodes.at(summaryId).first)->isSummary()) swap(summaryId, *interfaceId); - solAssert(_graph.nodes.at(*interfaceId).first.rfind("interface", 0) == 0, ""); + auto interfacePredicate = Predicate::predicate(_graph.nodes.at(*interfaceId).first); + solAssert(interfacePredicate && interfacePredicate->isInterface(), ""); } /// The children are unordered, so we need to check which is the summary and /// which is the interface. - solAssert(_graph.nodes.at(summaryId).first.rfind("summary", 0) == 0, ""); + Predicate const* summaryPredicate = Predicate::predicate(_graph.nodes.at(summaryId).first); + solAssert(summaryPredicate && summaryPredicate->isSummary(), ""); /// At this point property 2 from the function description is verified for this node. + auto summaryArgs = _graph.nodes.at(summaryId).second; - auto const& summaryNode = _graph.nodes.at(summaryId); - solAssert(m_symbolFunction.count(summaryNode.first), ""); - - FunctionDefinition const* calledFun = nullptr; - ContractDefinition const* calledContract = nullptr; - if (auto const* contract = dynamic_cast(m_symbolFunction.at(summaryNode.first))) - { - if (auto const* constructor = contract->constructor()) - calledFun = constructor; - else - calledContract = contract; - } - else if (auto const* fun = dynamic_cast(m_symbolFunction.at(summaryNode.first))) - calledFun = fun; - else - solAssert(false, ""); + FunctionDefinition const* calledFun = summaryPredicate->programFunction(); + ContractDefinition const* calledContract = summaryPredicate->programContract(); solAssert((calledFun && !calledContract) || (!calledFun && calledContract), ""); - auto const& stateVars = calledFun ? stateVariablesIncludingInheritedAndPrivate(*calledFun) : stateVariablesIncludingInheritedAndPrivate(*calledContract); - /// calledContract != nullptr implies that the constructor of the analyzed contract is implicit and - /// therefore takes no parameters. + auto stateVars = summaryPredicate->stateVariables(); + solAssert(stateVars.has_value(), ""); + auto stateValues = summaryPredicate->summaryStateValues(summaryArgs); + solAssert(stateValues.size() == stateVars->size(), ""); /// This summary node is the end of a tx. /// If it is the first summary node seen in this loop, it is the summary @@ -1470,36 +1437,23 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& { lastTxSeen = true; /// Generate counterexample message local to the failed target. - localState = formatStateCounterexample(stateVars, calledFun, summaryNode.second) + "\n"; + localState = formatVariableModel(*stateVars, stateValues, ", ") + "\n"; if (calledFun) { - /// The signature of a summary predicate is: summary(error, preStateVars, preInputVars, postInputVars, outputVars). + auto inValues = summaryPredicate->summaryPostInputValues(summaryArgs); auto const& inParams = calledFun->parameters(); - unsigned initLocals = stateVars.size() * 2 + 1 + inParams.size(); - /// In this loop we are interested in postInputVars. - for (unsigned i = initLocals; i < initLocals + inParams.size(); ++i) - { - auto param = inParams.at(i - initLocals); - if (param->type()->isValueType()) - localState += param->name() + " = " + summaryNode.second.at(i) + "\n"; - } + localState += formatVariableModel(inParams, inValues, "\n") + "\n"; + auto outValues = summaryPredicate->summaryPostOutputValues(summaryArgs); auto const& outParams = calledFun->returnParameters(); - initLocals += inParams.size(); - /// In this loop we are interested in outputVars. - for (unsigned i = initLocals; i < initLocals + outParams.size(); ++i) - { - auto param = outParams.at(i - initLocals); - if (param->type()->isValueType()) - localState += param->name() + " = " + summaryNode.second.at(i) + "\n"; - } + localState += formatVariableModel(outParams, outValues, "\n") + "\n"; } } else /// We report the state after every tx in the trace except for the last, which is reported /// first in the code above. - path.emplace_back("State: " + formatStateCounterexample(stateVars, calledFun, summaryNode.second)); + path.emplace_back("State: " + formatVariableModel(*stateVars, stateValues, ", ")); - string txCex = calledContract ? "constructor()" : formatFunctionCallCounterexample(stateVars, *calledFun, summaryNode.second); + string txCex = summaryPredicate->formatSummaryCall(summaryArgs); path.emplace_back(txCex); /// Recurse on the next interface node which represents the previous transaction @@ -1513,66 +1467,6 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& return localState + "\nTransaction trace:\n" + boost::algorithm::join(boost::adaptors::reverse(path), "\n"); } -string CHC::formatStateCounterexample(vector const& _stateVars, FunctionDefinition const* _function, vector const& _summaryValues) -{ - /// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postInputVars, outputVars). - /// The signature of an implicit constructor summary predicate is: summary(error, postStateVars). - /// Here we are interested in postStateVars. - vector::const_iterator stateFirst; - vector::const_iterator stateLast; - if (_function) - { - stateFirst = _summaryValues.begin() + 1 + static_cast(_stateVars.size()) + static_cast(_function->parameters().size()); - stateLast = stateFirst + static_cast(_stateVars.size()); - } - else - { - stateFirst = _summaryValues.begin() + 1; - stateLast = stateFirst + static_cast(_stateVars.size()); - } - - solAssert(stateFirst >= _summaryValues.begin() && stateFirst <= _summaryValues.end(), ""); - solAssert(stateLast >= _summaryValues.begin() && stateLast <= _summaryValues.end(), ""); - vector stateArgs(stateFirst, stateLast); - solAssert(stateArgs.size() == _stateVars.size(), ""); - - vector stateCex; - for (unsigned i = 0; i < stateArgs.size(); ++i) - { - auto var = _stateVars.at(i); - if (var->type()->isValueType()) - stateCex.emplace_back(var->name() + " = " + stateArgs.at(i)); - } - - return boost::algorithm::join(stateCex, ", "); -} - -string CHC::formatFunctionCallCounterexample(vector const& _stateVars, FunctionDefinition const& _function, vector const& _summaryValues) -{ - /// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postInputVars, outputVars). - /// Here we are interested in preInputVars. - vector::const_iterator first = _summaryValues.begin() + static_cast(_stateVars.size()) + 1; - vector::const_iterator last = first + static_cast(_function.parameters().size()); - solAssert(first >= _summaryValues.begin() && first <= _summaryValues.end(), ""); - solAssert(last >= _summaryValues.begin() && last <= _summaryValues.end(), ""); - vector functionArgsCex(first, last); - vector functionArgs; - - auto const& params = _function.parameters(); - solAssert(params.size() == functionArgsCex.size(), ""); - for (unsigned i = 0; i < params.size(); ++i) - if (params[i]->type()->isValueType()) - functionArgs.emplace_back(functionArgsCex[i]); - else - functionArgs.emplace_back(params[i]->name()); - - string fName = _function.isConstructor() ? "constructor" : - _function.isFallback() ? "fallback" : - _function.isReceive() ? "receive" : - _function.name(); - return fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")"; -} - string CHC::cex2dot(smtutil::CHCSolverInterface::CexGraph const& _cex) { string dot = "digraph {\n"; diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index ac1315317..d555f19e7 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -31,12 +31,15 @@ #pragma once +#include #include #include #include +#include + #include #include #include @@ -108,10 +111,8 @@ private: void resetContractAnalysis(); void eraseKnowledge(); void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override; - void setCurrentBlock(smt::SymbolicFunctionVariable const& _block, std::vector const* _arguments = nullptr); + void setCurrentBlock(Predicate const& _block, std::vector const* _arguments = nullptr); std::set transactionAssertions(ASTNode const* _txRoot); - static std::vector stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract); - static std::vector stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function); //@} /// Sort helpers. @@ -122,7 +123,7 @@ private: smtutil::SortPointer nondetInterfaceSort(); static smtutil::SortPointer interfaceSort(ContractDefinition const& _const); static smtutil::SortPointer nondetInterfaceSort(ContractDefinition const& _const); - smtutil::SortPointer arity0FunctionSort(); + smtutil::SortPointer arity0FunctionSort() const; smtutil::SortPointer sort(FunctionDefinition const& _function); smtutil::SortPointer sort(ASTNode const* _block); /// @returns the sort of a predicate that represents the summary of _function in the scope of _contract. @@ -134,7 +135,7 @@ private: /// Predicate helpers. //@{ /// @returns a new block of given _sort and _name. - std::unique_ptr createSymbolicBlock(smtutil::SortPointer _sort, std::string const& _name); + Predicate const* createSymbolicBlock(smtutil::SortPointer _sort, std::string const& _name, ASTNode const* _node = nullptr); /// Creates summary predicates for all functions of all contracts /// in a given _source. @@ -150,10 +151,10 @@ private: smtutil::Expression error(unsigned _idx); /// Creates a block for the given _node. - std::unique_ptr createBlock(ASTNode const* _node, std::string const& _prefix = ""); + Predicate const* createBlock(ASTNode const* _node, std::string const& _prefix = ""); /// Creates a call block for the given function _function from contract _contract. /// The contract is needed here because of inheritance. - std::unique_ptr createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract); + Predicate const* createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract); /// Creates a new error block to be used by an assertion. /// Also registers the predicate. @@ -184,9 +185,9 @@ private: /// @returns the predicate name for a given node. std::string predicateName(ASTNode const* _node, ContractDefinition const* _contract = nullptr); /// @returns a predicate application over the current scoped variables. - smtutil::Expression predicate(smt::SymbolicFunctionVariable const& _block); + smtutil::Expression predicate(Predicate const& _block); /// @returns a predicate application over @param _arguments. - smtutil::Expression predicate(smt::SymbolicFunctionVariable const& _block, std::vector const& _arguments); + smtutil::Expression predicate(Predicate const& _block, std::vector const& _arguments); /// @returns the summary predicate for the called function. smtutil::Expression predicate(FunctionCall const& _funCall); /// @returns a predicate that defines a constructor summary. @@ -222,15 +223,23 @@ private: ); std::optional generateCounterexample(smtutil::CHCSolverInterface::CexGraph const& _graph, std::string const& _root); - /// @returns values for the _stateVariables after a transaction calling - /// _function was executed. - /// _function = nullptr means the transaction was the deployment of a - /// contract without an explicit constructor. - std::string formatStateCounterexample(std::vector const& _stateVariables, FunctionDefinition const* _function, std::vector const& _summaryValues); - /// @returns a formatted text representing a call to _function - /// with the concrete values for value type parameters and - /// the parameter name for reference types. - std::string formatFunctionCallCounterexample(std::vector const& _stateVariables, FunctionDefinition const& _function, std::vector const& _summaryValues); + + /// @returns a set of pairs _var = _value separated by _separator. + template + std::string formatVariableModel(std::vector const& _variables, std::vector const& _values, std::string const& _separator) const + { + solAssert(_variables.size() == _values.size(), ""); + + std::vector assignments; + for (unsigned i = 0; i < _values.size(); ++i) + { + auto var = _variables.at(i); + if (var && var->type()->isValueType()) + assignments.emplace_back(var->name() + " = " + _values.at(i)); + } + + return boost::algorithm::join(assignments, _separator); + } /// @returns a DAG in the dot format. /// Used for debugging purposes. @@ -251,32 +260,32 @@ private: /// Predicates. //@{ /// Genesis predicate. - std::unique_ptr m_genesisPredicate; + Predicate const* m_genesisPredicate = nullptr; /// Implicit constructor predicate. /// Explicit constructors are handled as functions. - std::unique_ptr m_implicitConstructorPredicate; + Predicate const* m_implicitConstructorPredicate = nullptr; /// Constructor summary predicate, exists after the constructor /// (implicit or explicit) and before the interface. - std::unique_ptr m_constructorSummaryPredicate; + Predicate const* m_constructorSummaryPredicate = nullptr; /// Artificial Interface predicate. /// Single entry block for all functions. - std::map> m_interfaces; + std::map m_interfaces; /// Nondeterministic interfaces. /// These are used when the analyzed contract makes external calls to unknown code, /// which means that the analyzed contract can potentially be called /// nondeterministically. - std::map> m_nondetInterfaces; + std::map m_nondetInterfaces; /// Artificial Error predicate. /// Single error block for all assertions. - std::unique_ptr m_errorPredicate; + Predicate const* m_errorPredicate = nullptr; /// Function predicates. - std::map>> m_summaries; + std::map> m_summaries; smt::SymbolicIntVariable m_error{ TypeProvider::uint256(), @@ -337,9 +346,9 @@ private: bool m_unknownFunctionCallSeen = false; /// Block where a loop break should go to. - smt::SymbolicFunctionVariable const* m_breakDest = nullptr; + Predicate const* m_breakDest; /// Block where a loop continue should go to. - smt::SymbolicFunctionVariable const* m_continueDest = nullptr; + Predicate const* m_continueDest; //@} /// CHC solver. diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp new file mode 100644 index 000000000..9f897d63f --- /dev/null +++ b/libsolidity/formal/Predicate.cpp @@ -0,0 +1,260 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see . +*/ +// SPDX-License-Identifier: GPL-3.0 + +#include + +#include + +#include + +#include +#include + +using namespace std; +using namespace solidity; +using namespace solidity::smtutil; +using namespace solidity::frontend; +using namespace solidity::frontend::smt; + +map Predicate::m_predicates; + +Predicate const* Predicate::create( + SortPointer _sort, + string _name, + EncodingContext& _context, + ASTNode const* _node +) +{ + smt::SymbolicFunctionVariable predicate{_sort, move(_name), _context}; + string functorName = predicate.currentName(); + solAssert(!m_predicates.count(functorName), ""); + return &m_predicates.emplace( + std::piecewise_construct, + std::forward_as_tuple(functorName), + std::forward_as_tuple(move(predicate), _node) + ).first->second; +} + +Predicate::Predicate( + smt::SymbolicFunctionVariable&& _predicate, + ASTNode const* _node +): + m_predicate(move(_predicate)), + m_node(_node) +{ +} + +Predicate const* Predicate::predicate(string const& _name) +{ + return &m_predicates.at(_name); +} + +void Predicate::reset() +{ + m_predicates.clear(); +} + +smtutil::Expression Predicate::operator()(vector const& _args) const +{ + return m_predicate(_args); +} + +smtutil::Expression Predicate::functor() const +{ + return m_predicate.currentFunctionValue(); +} + +smtutil::Expression Predicate::functor(unsigned _idx) const +{ + return m_predicate.functionValueAtIndex(_idx); +} + +void Predicate::newFunctor() +{ + m_predicate.increaseIndex(); +} + +ASTNode const* Predicate::programNode() const +{ + return m_node; +} + +ContractDefinition const* Predicate::programContract() const +{ + if (auto const* contract = dynamic_cast(m_node)) + if (!contract->constructor()) + return contract; + + return nullptr; +} + +FunctionDefinition const* Predicate::programFunction() const +{ + if (auto const* contract = dynamic_cast(m_node)) + { + if (contract->constructor()) + return contract->constructor(); + return nullptr; + } + + if (auto const* fun = dynamic_cast(m_node)) + return fun; + + return nullptr; +} + +optional> Predicate::stateVariables() const +{ + if (auto const* fun = programFunction()) + return SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*fun); + if (auto const* contract = programContract()) + return SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*contract); + + auto const* node = m_node; + while (auto const* scopable = dynamic_cast(node)) + { + node = scopable->scope(); + if (auto const* fun = dynamic_cast(node)) + return SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*fun); + } + + return nullopt; +} + +bool Predicate::isSummary() const +{ + return functor().name.rfind("summary", 0) == 0; +} + +bool Predicate::isInterface() const +{ + return functor().name.rfind("interface", 0) == 0; +} + +string Predicate::formatSummaryCall(vector const& _args) const +{ + if (programContract()) + return "constructor()"; + + solAssert(isSummary(), ""); + + auto stateVars = stateVariables(); + solAssert(stateVars.has_value(), ""); + auto const* fun = programFunction(); + solAssert(fun, ""); + + /// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars). + /// Here we are interested in preInputVars. + vector::const_iterator first = _args.begin() + static_cast(stateVars->size()) + 1; + vector::const_iterator last = first + static_cast(fun->parameters().size()); + solAssert(first >= _args.begin() && first <= _args.end(), ""); + solAssert(last >= _args.begin() && last <= _args.end(), ""); + vector functionArgsCex(first, last); + vector functionArgs; + + auto const& params = fun->parameters(); + solAssert(params.size() == functionArgsCex.size(), ""); + for (unsigned i = 0; i < params.size(); ++i) + if (params[i]->type()->isValueType()) + functionArgs.emplace_back(functionArgsCex[i]); + else + functionArgs.emplace_back(params[i]->name()); + + string fName = fun->isConstructor() ? "constructor" : + fun->isFallback() ? "fallback" : + fun->isReceive() ? "receive" : + fun->name(); + return fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")"; + +} + +vector Predicate::summaryStateValues(vector const& _args) const +{ + /// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars). + /// The signature of an implicit constructor summary predicate is: summary(error, postStateVars). + /// Here we are interested in postStateVars. + + auto stateVars = stateVariables(); + solAssert(stateVars.has_value(), ""); + + vector::const_iterator stateFirst; + vector::const_iterator stateLast; + if (auto const* function = programFunction()) + { + stateFirst = _args.begin() + 1 + static_cast(stateVars->size()) + static_cast(function->parameters().size()); + stateLast = stateFirst + static_cast(stateVars->size()); + } + else if (programContract()) + { + stateFirst = _args.begin() + 1; + stateLast = stateFirst + static_cast(stateVars->size()); + } + else + solAssert(false, ""); + + solAssert(stateFirst >= _args.begin() && stateFirst <= _args.end(), ""); + solAssert(stateLast >= _args.begin() && stateLast <= _args.end(), ""); + + vector stateArgs(stateFirst, stateLast); + solAssert(stateArgs.size() == stateVars->size(), ""); + return stateArgs; +} + +vector Predicate::summaryPostInputValues(vector const& _args) const +{ + /// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars). + /// Here we are interested in postInputVars. + auto const* function = programFunction(); + solAssert(function, ""); + + auto stateVars = stateVariables(); + solAssert(stateVars.has_value(), ""); + + auto const& inParams = function->parameters(); + + vector::const_iterator first = _args.begin() + 1 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()); + vector::const_iterator last = first + static_cast(inParams.size()); + + solAssert(first >= _args.begin() && first <= _args.end(), ""); + solAssert(last >= _args.begin() && last <= _args.end(), ""); + + vector inValues(first, last); + solAssert(inValues.size() == inParams.size(), ""); + return inValues; +} + +vector Predicate::summaryPostOutputValues(vector const& _args) const +{ + /// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars). + /// Here we are interested in outputVars. + auto const* function = programFunction(); + solAssert(function, ""); + + auto stateVars = stateVariables(); + solAssert(stateVars.has_value(), ""); + + auto const& inParams = function->parameters(); + + vector::const_iterator first = _args.begin() + 1 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()) * 2; + + solAssert(first >= _args.begin() && first <= _args.end(), ""); + + vector outValues(first, _args.end()); + solAssert(outValues.size() == function->returnParameters().size(), ""); + return outValues; +} diff --git a/libsolidity/formal/Predicate.h b/libsolidity/formal/Predicate.h new file mode 100644 index 000000000..3da5ad453 --- /dev/null +++ b/libsolidity/formal/Predicate.h @@ -0,0 +1,120 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see . +*/ +// SPDX-License-Identifier: GPL-3.0 + +#pragma once + +#include +#include + +#include + +#include +#include +#include + +namespace solidity::frontend +{ + +/** + * Represents a predicate used by the CHC engine. + */ +class Predicate +{ +public: + static Predicate const* create( + smtutil::SortPointer _sort, + std::string _name, + smt::EncodingContext& _context, + ASTNode const* _node = nullptr + ); + + Predicate( + smt::SymbolicFunctionVariable&& _predicate, + ASTNode const* _node = nullptr + ); + + /// Predicate should not be copiable. + Predicate(Predicate const&) = delete; + Predicate& operator=(Predicate const&) = delete; + + /// @returns the Predicate associated with _name. + static Predicate const* predicate(std::string const& _name); + + /// Resets all the allocated predicates. + static void reset(); + + /// @returns a function application of the predicate over _args. + smtutil::Expression operator()(std::vector const& _args) const; + + /// @returns the function declaration of the predicate. + smtutil::Expression functor() const; + /// @returns the function declaration of the predicate with index _idx. + smtutil::Expression functor(unsigned _idx) const; + /// Increases the index of the function declaration of the predicate. + void newFunctor(); + + /// @returns the program node this predicate represents. + ASTNode const* programNode() const; + + /// @returns the ContractDefinition that this predicate represents + /// or nullptr otherwise. + ContractDefinition const* programContract() const; + + /// @returns the FunctionDefinition that this predicate represents + /// or nullptr otherwise. + FunctionDefinition const* programFunction() const; + + /// @returns the program state variables in the scope of this predicate. + std::optional> stateVariables() const; + + /// @returns true if this predicate represents a summary. + bool isSummary() const; + + /// @returns true if this predicate represents an interface. + bool isInterface() const; + + /// @returns a formatted string representing a call to this predicate + /// with _args. + std::string formatSummaryCall(std::vector const& _args) const; + + /// @returns the values of the state variables from _args at the point + /// where this summary was reached. + std::vector summaryStateValues(std::vector const& _args) const; + + /// @returns the values of the function input variables from _args at the point + /// where this summary was reached. + std::vector summaryPostInputValues(std::vector const& _args) const; + + /// @returns the values of the function output variables from _args at the point + /// where this summary was reached. + std::vector summaryPostOutputValues(std::vector const& _args) const; + +private: + /// The actual SMT expression. + smt::SymbolicFunctionVariable m_predicate; + + /// The ASTNode that this predicate represents. + /// nullptr if this predicate is not associated with a specific program AST node. + ASTNode const* m_node = nullptr; + + /// Maps the name of the predicate to the actual Predicate. + /// Used in counterexample generation. + static std::map m_predicates; +}; + +} diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 8cbed6712..b8e5ac791 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -378,7 +378,7 @@ void SMTEncoder::endVisit(Assignment const& _assignment) "Assertion checker does not yet implement this assignment operator." ); } - else if (!smt::isSupportedType(_assignment.annotation().type->category())) + else if (!smt::isSupportedType(*_assignment.annotation().type)) { // Give it a new index anyway to keep the SSA scheme sound. @@ -403,8 +403,7 @@ void SMTEncoder::endVisit(Assignment const& _assignment) assignment( _assignment.leftHandSide(), expr(_assignment, type), - type, - _assignment.location() + type ); } } @@ -452,28 +451,30 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple) void SMTEncoder::endVisit(UnaryOperation const& _op) { - if (TokenTraits::isBitOp(_op.getOperator())) - return bitwiseNotOperation(_op); + /// We need to shortcut here due to potentially unknown + /// rational number sizes. if (_op.annotation().type->category() == Type::Category::RationalNumber) return; + if (TokenTraits::isBitOp(_op.getOperator())) + return bitwiseNotOperation(_op); + createExpr(_op); auto const* subExpr = innermostTuple(_op.subExpression()); - + auto type = _op.annotation().type; switch (_op.getOperator()) { case Token::Not: // ! { - solAssert(smt::isBool(_op.annotation().type->category()), ""); + solAssert(smt::isBool(*type), ""); defineExpr(_op, !expr(*subExpr)); break; } case Token::Inc: // ++ (pre- or postfix) case Token::Dec: // -- (pre- or postfix) { - auto cat = _op.annotation().type->category(); - solAssert(smt::isInteger(cat) || smt::isFixedPoint(cat), ""); + solAssert(smt::isInteger(*type) || smt::isFixedPoint(*type), ""); solAssert(subExpr->annotation().willBeWrittenTo, ""); if (auto identifier = dynamic_cast(subExpr)) { @@ -484,12 +485,15 @@ void SMTEncoder::endVisit(UnaryOperation const& _op) defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue); assignment(*decl, newValue); } - else if (dynamic_cast(subExpr)) + else if ( + dynamic_cast(&_op.subExpression()) || + dynamic_cast(&_op.subExpression()) + ) { auto innerValue = expr(*subExpr); auto newValue = _op.getOperator() == Token::Inc ? innerValue + 1 : innerValue - 1; defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue); - arrayIndexAssignment(*subExpr, newValue); + indexOrMemberAssignment(_op.subExpression(), newValue); } else m_errorReporter.warning( @@ -518,14 +522,13 @@ void SMTEncoder::endVisit(UnaryOperation const& _op) auto const& symbVar = m_context.expression(*subExpr); symbVar->increaseIndex(); m_context.setZeroValue(*symbVar); - if (dynamic_cast(subExpr)) - arrayIndexAssignment(*subExpr, symbVar->currentValue()); + if ( + dynamic_cast(&_op.subExpression()) || + dynamic_cast(&_op.subExpression()) + ) + indexOrMemberAssignment(_op.subExpression(), symbVar->currentValue()); else - m_errorReporter.warning( - 2683_error, - _op.location(), - "Assertion checker does not yet implement \"delete\" for this expression." - ); + solAssert(false, ""); } break; } @@ -823,11 +826,11 @@ void SMTEncoder::endVisit(Literal const& _literal) { solAssert(_literal.annotation().type, "Expected type for AST node"); Type const& type = *_literal.annotation().type; - if (smt::isNumber(type.category())) + if (smt::isNumber(type)) defineExpr(_literal, smtutil::Expression(type.literalValue(&_literal))); - else if (smt::isBool(type.category())) + else if (smt::isBool(type)) defineExpr(_literal, smtutil::Expression(_literal.token() == Token::TrueLiteral ? true : false)); - else if (smt::isStringLiteral(type.category())) + else if (smt::isStringLiteral(type)) createExpr(_literal); else { @@ -890,6 +893,13 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess) defineGlobalVariable(accessedName + "." + _memberAccess.memberName(), _memberAccess); return false; } + else if (smt::isNonRecursiveStruct(*exprType)) + { + _memberAccess.expression().accept(*this); + auto const& symbStruct = dynamic_pointer_cast(m_context.expression(_memberAccess.expression())); + defineExpr(_memberAccess, symbStruct->member(_memberAccess.memberName())); + return false; + } else if (exprType->category() == Type::Category::TypeType) { if (identifier && dynamic_cast(identifier->annotation().referencedDeclaration)) @@ -961,19 +971,10 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess) solAssert(varDecl, ""); array = m_context.variable(*varDecl); } - else if (auto const* innerAccess = dynamic_cast(&_indexAccess.baseExpression())) - { - solAssert(m_context.knownExpression(*innerAccess), ""); - array = m_context.expression(*innerAccess); - } else { - m_errorReporter.warning( - 9118_error, - _indexAccess.location(), - "Assertion checker does not yet implement this expression." - ); - return; + solAssert(m_context.knownExpression(_indexAccess.baseExpression()), ""); + array = m_context.expression(_indexAccess.baseExpression()); } auto arrayVar = dynamic_pointer_cast(array); @@ -1005,14 +1006,58 @@ void SMTEncoder::arrayAssignment() m_arrayAssignmentHappened = true; } -void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide) +void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide) { auto toStore = _rightHandSide; - auto indexAccess = dynamic_cast(&_expr); - solAssert(indexAccess, ""); + auto const* lastExpr = &_expr; while (true) { - if (auto const& id = dynamic_cast(&indexAccess->baseExpression())) + if (auto const* indexAccess = dynamic_cast(lastExpr)) + { + auto const& base = indexAccess->baseExpression(); + if (dynamic_cast(&base)) + base.accept(*this); + 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()} + ); + m_context.expression(*indexAccess)->increaseIndex(); + defineExpr(*indexAccess, smtutil::Expression::select( + symbArray->elements(), + expr(*indexAccess->indexExpression()) + )); + lastExpr = &indexAccess->baseExpression(); + } + else if (auto const* memberAccess = dynamic_cast(lastExpr)) + { + auto const& base = memberAccess->expression(); + if (dynamic_cast(&base)) + base.accept(*this); + + if ( + auto const* structType = dynamic_cast(base.annotation().type); + structType && structType->recursive() + ) + { + m_errorReporter.warning( + 4375_error, + memberAccess->location(), + "Assertion checker does not support recursive structs." + ); + return; + } + + auto symbStruct = dynamic_pointer_cast(m_context.expression(base)); + solAssert(symbStruct, ""); + symbStruct->assignMember(memberAccess->memberName(), toStore); + toStore = symbStruct->currentValue(); + defineExpr(*memberAccess, symbStruct->member(memberAccess->memberName())); + lastExpr = &memberAccess->expression(); + } + else if (auto const& id = dynamic_cast(lastExpr)) { auto varDecl = identifierToVariable(*id); solAssert(varDecl, ""); @@ -1020,43 +1065,22 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smtutil::Expressi if (varDecl->hasReferenceOrMappingType()) resetReferences(*varDecl); - auto symbArray = dynamic_pointer_cast(m_context.variable(*varDecl)); - smtutil::Expression store = smtutil::Expression::store( - symbArray->elements(), - expr(*indexAccess->indexExpression()), - toStore - ); - auto oldLength = symbArray->length(); - symbArray->increaseIndex(); - m_context.addAssertion(symbArray->elements() == store); - m_context.addAssertion(symbArray->length() == oldLength); - // Update the SMT select value after the assignment, - // necessary for sound models. - defineExpr(*indexAccess, smtutil::Expression::select( - symbArray->elements(), - expr(*indexAccess->indexExpression()) - )); - + m_context.addAssertion(m_context.newValue(*varDecl) == toStore); + m_context.expression(*id)->increaseIndex(); + defineExpr(*id,currentValue(*varDecl)); break; } - else if (auto base = dynamic_cast(&indexAccess->baseExpression())) - { - auto symbArray = dynamic_pointer_cast(m_context.expression(*base)); - solAssert(symbArray, ""); - auto baseType = base->annotation().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()} - ); - indexAccess = base; - } else { - m_errorReporter.warning( - 9056_error, - _expr.location(), - "Assertion checker does not yet implement this expression." - ); + auto type = lastExpr->annotation().type; + if ( + dynamic_cast(type) || + dynamic_cast(type) + ) + resetReferences(type); + + m_context.expression(*lastExpr)->increaseIndex(); + m_context.addAssertion(expr(*lastExpr) == toStore); break; } } @@ -1128,9 +1152,14 @@ void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression if (varDecl->hasReferenceOrMappingType()) resetReferences(*varDecl); m_context.addAssertion(m_context.newValue(*varDecl) == _array); + m_context.expression(*id)->increaseIndex(); + defineExpr(*id,currentValue(*varDecl)); } - else if (auto const* indexAccess = dynamic_cast(expr)) - arrayIndexAssignment(*indexAccess, _array); + else if ( + dynamic_cast(expr) || + dynamic_cast(expr) + ) + indexOrMemberAssignment(_expr, _array); else if (auto const* funCall = dynamic_cast(expr)) { FunctionType const& funType = dynamic_cast(*funCall->expression().annotation().type); @@ -1153,12 +1182,6 @@ void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression arrayPushPopAssign(memberAccess->expression(), symbArray->currentValue()); } } - else if (dynamic_cast(expr)) - m_errorReporter.warning( - 9599_error, - _expr.location(), - "Assertion checker does not yet implement this expression." - ); else solAssert(false, ""); } @@ -1179,7 +1202,7 @@ void SMTEncoder::defineGlobalVariable(string const& _name, Expression const& _ex m_context.globalSymbol(_name)->increaseIndex(); // The default behavior is not to increase the index since // most of the global values stay the same throughout a tx. - if (smt::isSupportedType(_expr.annotation().type->category())) + if (smt::isSupportedType(*_expr.annotation().type)) defineExpr(_expr, m_context.globalSymbol(_name)->currentValue()); } @@ -1332,13 +1355,13 @@ void SMTEncoder::compareOperation(BinaryOperation const& _op) { auto const& commonType = _op.annotation().commonType; solAssert(commonType, ""); - if (smt::isSupportedType(commonType->category())) + if (smt::isSupportedType(*commonType)) { smtutil::Expression left(expr(_op.leftExpression(), commonType)); smtutil::Expression right(expr(_op.rightExpression(), commonType)); Token op = _op.getOperator(); shared_ptr value; - if (smt::isNumber(commonType->category())) + if (smt::isNumber(*commonType)) { value = make_shared( op == Token::Equal ? (left == right) : @@ -1351,7 +1374,7 @@ void SMTEncoder::compareOperation(BinaryOperation const& _op) } else // Bool { - solUnimplementedAssert(smt::isBool(commonType->category()), "Operation not yet supported"); + solUnimplementedAssert(smt::isBool(*commonType), "Operation not yet supported"); value = make_shared( op == Token::Equal ? (left == right) : /*op == Token::NotEqual*/ (left != right) @@ -1447,8 +1470,7 @@ smtutil::Expression SMTEncoder::division(smtutil::Expression _left, smtutil::Exp void SMTEncoder::assignment( Expression const& _left, smtutil::Expression const& _right, - TypePointer const& _type, - langutil::SourceLocation const& _location + TypePointer const& _type ) { solAssert( @@ -1458,28 +1480,21 @@ void SMTEncoder::assignment( Expression const* left = innermostTuple(_left); - if (!smt::isSupportedType(_type->category())) + if (!smt::isSupportedType(*_type)) { // Give it a new index anyway to keep the SSA scheme sound. if (auto varDecl = identifierToVariable(*left)) m_context.newValue(*varDecl); - - m_errorReporter.warning( - 6191_error, - _location, - "Assertion checker does not yet implement type " + _type->toString() - ); } else if (auto varDecl = identifierToVariable(*left)) assignment(*varDecl, _right); - else if (dynamic_cast(left)) - arrayIndexAssignment(*left, _right); + else if ( + dynamic_cast(left) || + dynamic_cast(left) + ) + indexOrMemberAssignment(*left, _right); else - m_errorReporter.warning( - 8182_error, - _location, - "Assertion checker does not yet implement such assignments." - ); + solAssert(false, ""); } void SMTEncoder::tupleAssignment(Expression const& _left, Expression const& _right) @@ -1508,7 +1523,7 @@ void SMTEncoder::tupleAssignment(Expression const& _left, Expression const& _rig else { auto type = lExpr.annotation().type; - assignment(lExpr, expr(rExpr, type), type, lExpr.location()); + assignment(lExpr, expr(rExpr, type), type); } } } @@ -1525,7 +1540,7 @@ void SMTEncoder::tupleAssignment(Expression const& _left, Expression const& _rig for (unsigned i = 0; i < lComponents.size(); ++i) if (auto component = lComponents.at(i); component && rComponents.at(i)) - assignment(*component, smtutil::Expression::tuple_get(symbRight, i), component->annotation().type, component->location()); + assignment(*component, smtutil::Expression::tuple_get(symbRight, i), component->annotation().type); } } @@ -1689,32 +1704,43 @@ void SMTEncoder::resetReferences(VariableDeclaration const& _varDecl) if (_var.isStateVariable() && _varDecl.isStateVariable()) return false; - TypePointer prefix = _var.type(); - TypePointer originalType = typeWithoutPointer(_varDecl.type()); - while ( - prefix->category() == Type::Category::Mapping || - prefix->category() == Type::Category::Array - ) - { - if (*originalType == *typeWithoutPointer(prefix)) - return true; - if (prefix->category() == Type::Category::Mapping) - { - auto mapPrefix = dynamic_cast(prefix); - solAssert(mapPrefix, ""); - prefix = mapPrefix->valueType(); - } - else - { - auto arrayPrefix = dynamic_cast(prefix); - solAssert(arrayPrefix, ""); - prefix = arrayPrefix->baseType(); - } - } - return false; + return sameTypeOrSubtype(_var.type(), _varDecl.type()); }); } +void SMTEncoder::resetReferences(TypePointer _type) +{ + m_context.resetVariables([&](VariableDeclaration const& _var) { + return sameTypeOrSubtype(_var.type(), _type); + }); +} + +bool SMTEncoder::sameTypeOrSubtype(TypePointer _a, TypePointer _b) +{ + TypePointer prefix = _a; + while ( + prefix->category() == Type::Category::Mapping || + prefix->category() == Type::Category::Array + ) + { + if (*typeWithoutPointer(_b) == *typeWithoutPointer(prefix)) + return true; + if (prefix->category() == Type::Category::Mapping) + { + auto mapPrefix = dynamic_cast(prefix); + solAssert(mapPrefix, ""); + prefix = mapPrefix->valueType(); + } + else + { + auto arrayPrefix = dynamic_cast(prefix); + solAssert(arrayPrefix, ""); + prefix = arrayPrefix->baseType(); + } + } + return false; +} + TypePointer SMTEncoder::typeWithoutPointer(TypePointer const& _type) { if (auto refType = dynamic_cast(_type)) @@ -1982,6 +2008,20 @@ FunctionDefinition const* SMTEncoder::functionCallToDefinition(FunctionCall cons return funDef; } +vector SMTEncoder::stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract) +{ + return fold( + _contract.annotation().linearizedBaseContracts, + vector{}, + [](auto&& _acc, auto _contract) { return _acc + _contract->stateVariables(); } + ); +} + +vector SMTEncoder::stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function) +{ + return stateVariablesIncludingInheritedAndPrivate(dynamic_cast(*_function.scope())); +} + void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall) { FunctionDefinition const* funDef = functionCallToDefinition(_funCall); diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index fb5dce405..a87af642f 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -62,6 +62,9 @@ public: /// if possible or nullptr. static FunctionDefinition const* functionCallToDefinition(FunctionCall const& _funCall); + static std::vector stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract); + static std::vector stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function); + protected: // TODO: Check that we do not have concurrent reads and writes to a variable, // because the order of expression evaluation is undefined @@ -143,8 +146,8 @@ protected: /// to variable of some SMT array type /// while aliasing is not supported. void arrayAssignment(); - /// Handles assignment to SMT array index. - void arrayIndexAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide); + /// Handles assignments to index or member access. + void indexOrMemberAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide); void arrayPush(FunctionCall const& _funCall); void arrayPop(FunctionCall const& _funCall); @@ -165,8 +168,7 @@ protected: void assignment( Expression const& _left, smtutil::Expression const& _right, - TypePointer const& _type, - langutil::SourceLocation const& _location + TypePointer const& _type ); /// Handle assignments between tuples. void tupleAssignment(Expression const& _left, Expression const& _right); @@ -193,8 +195,12 @@ protected: /// Resets all references/pointers that have the same type or have /// a subexpression of the same type as _varDecl. void resetReferences(VariableDeclaration const& _varDecl); + /// Resets all references/pointers that have type _type. + void resetReferences(TypePointer _type); /// @returns the type without storage pointer information if it has it. TypePointer typeWithoutPointer(TypePointer const& _type); + /// @returns whether _a or a subtype of _a is the same as _b. + bool sameTypeOrSubtype(TypePointer _a, TypePointer _b); /// Given two different branches and the touched variables, /// merge the touched variables into after-branch ite variables diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index 965130bb7..d363ea0e2 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -25,6 +25,7 @@ #include using namespace std; +using namespace solidity::util; using namespace solidity::smtutil; namespace solidity::frontend::smt @@ -32,7 +33,7 @@ namespace solidity::frontend::smt SortPointer smtSort(frontend::Type const& _type) { - switch (smtKind(_type.category())) + switch (smtKind(_type)) { case Kind::Int: if (auto const* intType = dynamic_cast(&_type)) @@ -63,13 +64,13 @@ SortPointer smtSort(frontend::Type const& _type) case Kind::Array: { shared_ptr array; - if (isMapping(_type.category())) + if (isMapping(_type)) { auto mapType = dynamic_cast(&_type); solAssert(mapType, ""); array = make_shared(smtSortAbstractFunction(*mapType->keyType()), smtSortAbstractFunction(*mapType->valueType())); } - else if (isStringLiteral(_type.category())) + else if (isStringLiteral(_type)) { auto stringLitType = dynamic_cast(&_type); solAssert(stringLitType, ""); @@ -130,18 +131,32 @@ SortPointer smtSort(frontend::Type const& _type) } case Kind::Tuple: { - auto tupleType = dynamic_cast(&_type); - solAssert(tupleType, ""); vector members; - auto const& tupleName = _type.identifier(); - auto const& components = tupleType->components(); - for (unsigned i = 0; i < components.size(); ++i) - members.emplace_back(tupleName + "_accessor_" + to_string(i)); - return make_shared( - tupleName, - members, - smtSortAbstractFunction(tupleType->components()) - ); + auto const& tupleName = _type.toString(true); + vector sorts; + + if (auto const* tupleType = dynamic_cast(&_type)) + { + auto const& components = tupleType->components(); + for (unsigned i = 0; i < components.size(); ++i) + members.emplace_back(tupleName + "_accessor_" + to_string(i)); + sorts = smtSortAbstractFunction(tupleType->components()); + } + else if (auto const* structType = dynamic_cast(&_type)) + { + solAssert(!structType->recursive(), ""); + auto const& structMembers = structType->structDefinition().members(); + for (auto member: structMembers) + members.emplace_back(tupleName + "_accessor_" + member->name()); + sorts = smtSortAbstractFunction(applyMap( + structMembers, + [](auto var) { return var->type(); } + )); + } + else + solAssert(false, ""); + + return make_shared(tupleName, members, sorts); } default: // Abstract case. @@ -159,7 +174,7 @@ vector smtSort(vector const& _types) SortPointer smtSortAbstractFunction(frontend::Type const& _type) { - if (isFunction(_type.category())) + if (isFunction(_type)) return SortProvider::uintSort; return smtSort(_type); } @@ -175,35 +190,36 @@ vector smtSortAbstractFunction(vector const& return sorts; } -Kind smtKind(frontend::Type::Category _category) +Kind smtKind(frontend::Type const& _type) { - if (isNumber(_category)) + if (isNumber(_type)) return Kind::Int; - else if (isBool(_category)) + else if (isBool(_type)) return Kind::Bool; - else if (isFunction(_category)) + else if (isFunction(_type)) return Kind::Function; - else if (isMapping(_category) || isArray(_category)) + else if (isMapping(_type) || isArray(_type)) return Kind::Array; - else if (isTuple(_category)) + else if (isTuple(_type) || isNonRecursiveStruct(_type)) return Kind::Tuple; // Abstract case. return Kind::Int; } -bool isSupportedType(frontend::Type::Category _category) +bool isSupportedType(frontend::Type const& _type) { - return isNumber(_category) || - isBool(_category) || - isMapping(_category) || - isArray(_category) || - isTuple(_category); + return isNumber(_type) || + isBool(_type) || + isMapping(_type) || + isArray(_type) || + isTuple(_type) || + isNonRecursiveStruct(_type); } -bool isSupportedTypeDeclaration(frontend::Type::Category _category) +bool isSupportedTypeDeclaration(frontend::Type const& _type) { - return isSupportedType(_category) || - isFunction(_category); + return isSupportedType(_type) || + isFunction(_type); } pair> newSymbolicVariable( @@ -220,9 +236,9 @@ pair> newSymbolicVariable( abstract = true; var = make_shared(frontend::TypeProvider::uint256(), type, _uniqueName, _context); } - else if (isBool(_type.category())) + else if (isBool(_type)) var = make_shared(type, _uniqueName, _context); - else if (isFunction(_type.category())) + else if (isFunction(_type)) { auto const& fType = dynamic_cast(type); auto const& paramsIn = fType->parameterTypes(); @@ -245,21 +261,21 @@ pair> newSymbolicVariable( else var = make_shared(type, _uniqueName, _context); } - else if (isInteger(_type.category())) + else if (isInteger(_type)) var = make_shared(type, type, _uniqueName, _context); - else if (isFixedPoint(_type.category())) + else if (isFixedPoint(_type)) var = make_shared(type, type, _uniqueName, _context); - else if (isFixedBytes(_type.category())) + else if (isFixedBytes(_type)) { auto fixedBytesType = dynamic_cast(type); solAssert(fixedBytesType, ""); var = make_shared(type, fixedBytesType->numBytes(), _uniqueName, _context); } - else if (isAddress(_type.category()) || isContract(_type.category())) + else if (isAddress(_type) || isContract(_type)) var = make_shared(_uniqueName, _context); - else if (isEnum(_type.category())) + else if (isEnum(_type)) var = make_shared(type, _uniqueName, _context); - else if (isRational(_type.category())) + else if (isRational(_type)) { auto rational = dynamic_cast(&_type); solAssert(rational, ""); @@ -268,106 +284,104 @@ pair> newSymbolicVariable( else var = make_shared(type, type, _uniqueName, _context); } - else if (isMapping(_type.category()) || isArray(_type.category())) + else if (isMapping(_type) || isArray(_type)) var = make_shared(type, type, _uniqueName, _context); - else if (isTuple(_type.category())) + else if (isTuple(_type)) var = make_shared(type, _uniqueName, _context); - else if (isStringLiteral(_type.category())) + else if (isStringLiteral(_type)) { auto stringType = TypeProvider::stringMemory(); var = make_shared(stringType, type, _uniqueName, _context); } + else if (isNonRecursiveStruct(_type)) + var = make_shared(type, _uniqueName, _context); else solAssert(false, ""); return make_pair(abstract, var); } -bool isSupportedType(frontend::Type const& _type) +bool isInteger(frontend::Type const& _type) { - return isSupportedType(_type.category()); + return _type.category() == frontend::Type::Category::Integer; } -bool isSupportedTypeDeclaration(frontend::Type const& _type) +bool isFixedPoint(frontend::Type const& _type) { - return isSupportedTypeDeclaration(_type.category()); + return _type.category() == frontend::Type::Category::FixedPoint; } -bool isInteger(frontend::Type::Category _category) +bool isRational(frontend::Type const& _type) { - return _category == frontend::Type::Category::Integer; + return _type.category() == frontend::Type::Category::RationalNumber; } -bool isFixedPoint(frontend::Type::Category _category) +bool isFixedBytes(frontend::Type const& _type) { - return _category == frontend::Type::Category::FixedPoint; + return _type.category() == frontend::Type::Category::FixedBytes; } -bool isRational(frontend::Type::Category _category) +bool isAddress(frontend::Type const& _type) { - return _category == frontend::Type::Category::RationalNumber; + return _type.category() == frontend::Type::Category::Address; } -bool isFixedBytes(frontend::Type::Category _category) +bool isContract(frontend::Type const& _type) { - return _category == frontend::Type::Category::FixedBytes; + return _type.category() == frontend::Type::Category::Contract; } -bool isAddress(frontend::Type::Category _category) +bool isEnum(frontend::Type const& _type) { - return _category == frontend::Type::Category::Address; + return _type.category() == frontend::Type::Category::Enum; } -bool isContract(frontend::Type::Category _category) +bool isNumber(frontend::Type const& _type) { - return _category == frontend::Type::Category::Contract; + return isInteger(_type) || + isFixedPoint(_type) || + isRational(_type) || + isFixedBytes(_type) || + isAddress(_type) || + isContract(_type) || + isEnum(_type); } -bool isEnum(frontend::Type::Category _category) +bool isBool(frontend::Type const& _type) { - return _category == frontend::Type::Category::Enum; + return _type.category() == frontend::Type::Category::Bool; } -bool isNumber(frontend::Type::Category _category) +bool isFunction(frontend::Type const& _type) { - return isInteger(_category) || - isFixedPoint(_category) || - isRational(_category) || - isFixedBytes(_category) || - isAddress(_category) || - isContract(_category) || - isEnum(_category); + return _type.category() == frontend::Type::Category::Function; } -bool isBool(frontend::Type::Category _category) +bool isMapping(frontend::Type const& _type) { - return _category == frontend::Type::Category::Bool; + return _type.category() == frontend::Type::Category::Mapping; } -bool isFunction(frontend::Type::Category _category) +bool isArray(frontend::Type const& _type) { - return _category == frontend::Type::Category::Function; + return _type.category() == frontend::Type::Category::Array || + _type.category() == frontend::Type::Category::StringLiteral || + _type.category() == frontend::Type::Category::ArraySlice; } -bool isMapping(frontend::Type::Category _category) +bool isTuple(frontend::Type const& _type) { - return _category == frontend::Type::Category::Mapping; + return _type.category() == frontend::Type::Category::Tuple; } -bool isArray(frontend::Type::Category _category) +bool isStringLiteral(frontend::Type const& _type) { - return _category == frontend::Type::Category::Array || - _category == frontend::Type::Category::StringLiteral || - _category == frontend::Type::Category::ArraySlice; + return _type.category() == frontend::Type::Category::StringLiteral; } -bool isTuple(frontend::Type::Category _category) +bool isNonRecursiveStruct(frontend::Type const& _type) { - return _category == frontend::Type::Category::Tuple; -} - -bool isStringLiteral(frontend::Type::Category _category) -{ - return _category == frontend::Type::Category::StringLiteral; + auto structType = dynamic_cast(&_type); + return structType && !structType->recursive(); } smtutil::Expression minValue(frontend::IntegerType const& _type) @@ -394,13 +408,13 @@ void setSymbolicZeroValue(smtutil::Expression _expr, frontend::TypePointer const smtutil::Expression zeroValue(frontend::TypePointer const& _type) { solAssert(_type, ""); - if (isSupportedType(_type->category())) + if (isSupportedType(*_type)) { - if (isNumber(_type->category())) + if (isNumber(*_type)) return 0; - if (isBool(_type->category())) + if (isBool(*_type)) return smtutil::Expression(false); - if (isArray(_type->category()) || isMapping(_type->category())) + if (isArray(*_type) || isMapping(*_type)) { auto tupleSort = dynamic_pointer_cast(smtSort(*_type)); solAssert(tupleSort, ""); @@ -421,11 +435,23 @@ smtutil::Expression zeroValue(frontend::TypePointer const& _type) solAssert(zeroArray, ""); return smtutil::Expression::tuple_constructor( - smtutil::Expression(std::make_shared(smtSort(*_type)), _type->toString(true)), + smtutil::Expression(std::make_shared(tupleSort), tupleSort->name), vector{*zeroArray, length} ); } + if (isNonRecursiveStruct(*_type)) + { + auto const* structType = dynamic_cast(_type); + auto structSort = dynamic_pointer_cast(smtSort(*_type)); + return smtutil::Expression::tuple_constructor( + smtutil::Expression(make_shared(structSort), structSort->name), + applyMap( + structType->structDefinition().members(), + [](auto var) { return zeroValue(var->type()); } + ) + ); + } solAssert(false, ""); } // Unsupported types are abstracted as Int. @@ -452,14 +478,14 @@ void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext& void setSymbolicUnknownValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context) { solAssert(_type, ""); - if (isEnum(_type->category())) + if (isEnum(*_type)) { auto enumType = dynamic_cast(_type); solAssert(enumType, ""); _context.addAssertion(_expr >= 0); _context.addAssertion(_expr < enumType->numberOfMembers()); } - else if (isInteger(_type->category())) + else if (isInteger(*_type)) { auto intType = dynamic_cast(_type); solAssert(intType, ""); diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h index 8e08783d8..01bbe4d2c 100644 --- a/libsolidity/formal/SymbolicTypes.h +++ b/libsolidity/formal/SymbolicTypes.h @@ -34,29 +34,30 @@ std::vector smtSort(std::vector con smtutil::SortPointer smtSortAbstractFunction(frontend::Type const& _type); std::vector smtSortAbstractFunction(std::vector const& _types); /// Returns the SMT kind that models the Solidity type type category _category. -smtutil::Kind smtKind(frontend::Type::Category _category); +smtutil::Kind smtKind(frontend::Type const& _type); /// Returns true if type is fully supported (declaration and operations). -bool isSupportedType(frontend::Type::Category _category); +bool isSupportedType(frontend::Type const& _type); bool isSupportedType(frontend::Type const& _type); /// Returns true if type is partially supported (declaration). -bool isSupportedTypeDeclaration(frontend::Type::Category _category); +bool isSupportedTypeDeclaration(frontend::Type const& _type); bool isSupportedTypeDeclaration(frontend::Type const& _type); -bool isInteger(frontend::Type::Category _category); -bool isFixedPoint(frontend::Type::Category _category); -bool isRational(frontend::Type::Category _category); -bool isFixedBytes(frontend::Type::Category _category); -bool isAddress(frontend::Type::Category _category); -bool isContract(frontend::Type::Category _category); -bool isEnum(frontend::Type::Category _category); -bool isNumber(frontend::Type::Category _category); -bool isBool(frontend::Type::Category _category); -bool isFunction(frontend::Type::Category _category); -bool isMapping(frontend::Type::Category _category); -bool isArray(frontend::Type::Category _category); -bool isTuple(frontend::Type::Category _category); -bool isStringLiteral(frontend::Type::Category _category); +bool isInteger(frontend::Type const& _type); +bool isFixedPoint(frontend::Type const& _type); +bool isRational(frontend::Type const& _type); +bool isFixedBytes(frontend::Type const& _type); +bool isAddress(frontend::Type const& _type); +bool isContract(frontend::Type const& _type); +bool isEnum(frontend::Type const& _type); +bool isNumber(frontend::Type const& _type); +bool isBool(frontend::Type const& _type); +bool isFunction(frontend::Type const& _type); +bool isMapping(frontend::Type const& _type); +bool isArray(frontend::Type const& _type); +bool isTuple(frontend::Type const& _type); +bool isStringLiteral(frontend::Type const& _type); +bool isNonRecursiveStruct(frontend::Type const& _type); /// 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 b09938e63..51711b383 100644 --- a/libsolidity/formal/SymbolicVariables.cpp +++ b/libsolidity/formal/SymbolicVariables.cpp @@ -21,8 +21,11 @@ #include #include +#include + using namespace std; using namespace solidity; +using namespace solidity::util; using namespace solidity::smtutil; using namespace solidity::frontend; using namespace solidity::frontend::smt; @@ -118,7 +121,7 @@ SymbolicIntVariable::SymbolicIntVariable( ): SymbolicVariable(_type, _originalType, move(_uniqueName), _context) { - solAssert(isNumber(m_type->category()), ""); + solAssert(isNumber(*m_type), ""); } SymbolicAddressVariable::SymbolicAddressVariable( @@ -218,7 +221,7 @@ SymbolicEnumVariable::SymbolicEnumVariable( ): SymbolicVariable(_type, _type, move(_uniqueName), _context) { - solAssert(isEnum(m_type->category()), ""); + solAssert(isEnum(*m_type), ""); } SymbolicTupleVariable::SymbolicTupleVariable( @@ -228,7 +231,7 @@ SymbolicTupleVariable::SymbolicTupleVariable( ): SymbolicVariable(_type, _type, move(_uniqueName), _context) { - solAssert(isTuple(m_type->category()), ""); + solAssert(isTuple(*m_type), ""); } SymbolicTupleVariable::SymbolicTupleVariable( @@ -274,7 +277,7 @@ SymbolicArrayVariable::SymbolicArrayVariable( m_context ) { - solAssert(isArray(m_type->category()) || isMapping(m_type->category()), ""); + solAssert(isArray(*m_type) || isMapping(*m_type), ""); } SymbolicArrayVariable::SymbolicArrayVariable( @@ -319,3 +322,47 @@ smtutil::Expression SymbolicArrayVariable::length() { return m_pair.component(1); } + +SymbolicStructVariable::SymbolicStructVariable( + frontend::TypePointer _type, + string _uniqueName, + EncodingContext& _context +): + SymbolicVariable(_type, _type, move(_uniqueName), _context) +{ + solAssert(isNonRecursiveStruct(*m_type), ""); + auto const* structType = dynamic_cast(_type); + solAssert(structType, ""); + auto const& members = structType->structDefinition().members(); + for (unsigned i = 0; i < members.size(); ++i) + { + solAssert(members.at(i), ""); + m_memberIndices.emplace(members.at(i)->name(), i); + } +} + +smtutil::Expression SymbolicStructVariable::member(string const& _member) +{ + return smtutil::Expression::tuple_get(currentValue(), m_memberIndices.at(_member)); +} + +smtutil::Expression SymbolicStructVariable::assignMember(string const& _member, smtutil::Expression const& _memberValue) +{ + auto const* structType = dynamic_cast(m_type); + solAssert(structType, ""); + auto const& structDef = structType->structDefinition(); + auto const& structMembers = structDef.members(); + auto oldMembers = applyMap( + structMembers, + [&](auto _member) { return member(_member->name()); } + ); + increaseIndex(); + for (unsigned i = 0; i < structMembers.size(); ++i) + { + auto const& memberName = structMembers.at(i)->name(); + auto newMember = memberName == _member ? _memberValue : oldMembers.at(i); + m_context.addAssertion(member(memberName) == newMember); + } + + return currentValue(); +} diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h index bdf36afd0..843043c9d 100644 --- a/libsolidity/formal/SymbolicVariables.h +++ b/libsolidity/formal/SymbolicVariables.h @@ -23,6 +23,8 @@ #include #include + +#include #include namespace solidity::frontend::smt @@ -265,4 +267,29 @@ private: SymbolicTupleVariable m_pair; }; +/** + * Specialization of SymbolicVariable for Struct. + */ +class SymbolicStructVariable: public SymbolicVariable +{ +public: + SymbolicStructVariable( + frontend::TypePointer _type, + std::string _uniqueName, + EncodingContext& _context + ); + + /// @returns the symbolic expression representing _member. + smtutil::Expression member(std::string const& _member); + + /// @returns the symbolic expression representing this struct + /// with field _member updated. + smtutil::Expression assignMember(std::string const& _member, smtutil::Expression const& _memberValue); + +private: + std::map m_memberIndices; +}; + + + } diff --git a/libsolidity/interface/OptimiserSettings.h b/libsolidity/interface/OptimiserSettings.h index 67007fc4c..4b1cd7c4e 100644 --- a/libsolidity/interface/OptimiserSettings.h +++ b/libsolidity/interface/OptimiserSettings.h @@ -41,7 +41,7 @@ struct OptimiserSettings // should have good "compilability" property here. - "eul" // Run functional expression inliner + "Tpeul" // Run functional expression inliner "xarulrul" // Prune a bit more in SSA "xarrcL" // Turn into SSA again and simplify "gvif" // Run full inliner diff --git a/libsolutil/CommonData.h b/libsolutil/CommonData.h index b01e24c38..4ab824791 100644 --- a/libsolutil/CommonData.h +++ b/libsolutil/CommonData.h @@ -209,6 +209,13 @@ std::map invertMap(std::map const& originalMap) return inverseMap; } +/// Returns a set of keys of a map. +template +std::set keys(std::map const& _map) +{ + return applyMap(_map, [](auto const& _elem) { return _elem.first; }, std::set{}); +} + // String conversion functions, mainly to/from hex/nibble/byte representations. enum class WhenError diff --git a/libyul/CMakeLists.txt b/libyul/CMakeLists.txt index 65269e9e0..f3318bd84 100644 --- a/libyul/CMakeLists.txt +++ b/libyul/CMakeLists.txt @@ -156,6 +156,9 @@ add_library(yul optimiser/SyntacticalEquality.h optimiser/TypeInfo.cpp optimiser/TypeInfo.h + optimiser/UnusedFunctionParameterPruner.cpp + optimiser/UnusedFunctionParameterPruner.h + optimiser/UnusedFunctionsCommon.h optimiser/UnusedPruner.cpp optimiser/UnusedPruner.h optimiser/VarDeclInitializer.cpp diff --git a/libyul/optimiser/NameDisplacer.h b/libyul/optimiser/NameDisplacer.h index d1b3e4363..336dd04e4 100644 --- a/libyul/optimiser/NameDisplacer.h +++ b/libyul/optimiser/NameDisplacer.h @@ -60,6 +60,8 @@ public: void operator()(FunctionCall& _funCall) override; void operator()(Block& _block) override; + std::map const& translations() const { return m_translations; } + protected: /// Check if the newly introduced identifier @a _name has to be replaced. void checkAndReplaceNew(YulString& _name); diff --git a/libyul/optimiser/Suite.cpp b/libyul/optimiser/Suite.cpp index a12ecd194..eca34fa81 100644 --- a/libyul/optimiser/Suite.cpp +++ b/libyul/optimiser/Suite.cpp @@ -42,6 +42,7 @@ #include #include #include +#include #include #include #include @@ -185,6 +186,7 @@ map> const& OptimiserSuite::allSteps() SSAReverser, SSATransform, StructuralSimplifier, + UnusedFunctionParameterPruner, UnusedPruner, VarDeclInitializer >(); @@ -221,6 +223,7 @@ map const& OptimiserSuite::stepNameToAbbreviationMap() {SSAReverser::name, 'V'}, {SSATransform::name, 'a'}, {StructuralSimplifier::name, 't'}, + {UnusedFunctionParameterPruner::name, 'p'}, {UnusedPruner::name, 'u'}, {VarDeclInitializer::name, 'd'}, }; diff --git a/libyul/optimiser/UnusedFunctionParameterPruner.cpp b/libyul/optimiser/UnusedFunctionParameterPruner.cpp new file mode 100644 index 000000000..d103e9c6f --- /dev/null +++ b/libyul/optimiser/UnusedFunctionParameterPruner.cpp @@ -0,0 +1,127 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see . +*/ +// SPDX-License-Identifier: GPL-3.0 +/** + * UnusedFunctionParameterPruner: Optimiser step that removes unused parameters from function + * definition. + */ + +#include +#include +#include +#include +#include +#include +#include +#include + +#include + +#include + +#include +#include + +using namespace std; +using namespace solidity::util; +using namespace solidity::yul; +using namespace solidity::yul::unusedFunctionsCommon; + +void UnusedFunctionParameterPruner::run(OptimiserStepContext& _context, Block& _ast) +{ + map references = ReferencesCounter::countReferences(_ast); + auto used = [&](auto v) -> bool { return references.count(v.name); }; + + // Function name and a pair of boolean masks, the first corresponds to parameters and the second + // corresponds to returnVariables. + // + // For the first vector in the pair, a value `false` at index `i` indicates that the function + // argument at index `i` in `FunctionDefinition::parameters` is unused inside the function body. + // + // Similarly for the second vector in the pair, a value `false` at index `i` indicates that the + // return parameter at index `i` in `FunctionDefinition::returnVariables` is unused inside + // function body. + map, vector>> usedParametersAndReturnVariables; + + // Step 1 of UnusedFunctionParameterPruner: Find functions whose parameters (both arguments and + // return-parameters) are not used in its body. + for (auto const& statement: _ast.statements) + if (holds_alternative(statement)) + { + FunctionDefinition const& f = std::get(statement); + + if (tooSimpleToBePruned(f) || boost::algorithm::all_of(f.parameters + f.returnVariables, used)) + continue; + + usedParametersAndReturnVariables[f.name] = { + applyMap(f.parameters, used), + applyMap(f.returnVariables, used) + }; + } + + set functionNamesToFree = util::keys(usedParametersAndReturnVariables); + + // Step 2 of UnusedFunctionParameterPruner: Renames the function and replaces all references to + // the function, say `f`, by its new name, say `f_1`. + NameDisplacer replace{_context.dispenser, functionNamesToFree}; + replace(_ast); + + // Inverse-Map of the above translations. In the above example, this will store an element with + // key `f_1` and value `f`. + std::map newToOriginalNames = invertMap(replace.translations()); + + // Step 3 of UnusedFunctionParameterPruner: introduce a new function in the block with body of + // the old one. Replace the body of the old one with a function call to the new one with reduced + // parameters. + // + // For example: introduce a new 'linking' function `f` with the same the body as `f_1`, but with + // reduced parameters, i.e., `function f() -> y { y := 1 }`. Now replace the body of `f_1` with + // a call to `f`, i.e., `f_1(x) -> y { y := f() }`. + iterateReplacing(_ast.statements, [&](Statement& _s) -> optional> { + if (holds_alternative(_s)) + { + // The original function except that it has a new name (e.g., `f_1`) + FunctionDefinition& originalFunction = get(_s); + if (newToOriginalNames.count(originalFunction.name)) + { + + YulString linkingFunctionName = originalFunction.name; + YulString originalFunctionName = newToOriginalNames.at(linkingFunctionName); + pair, vector> used = + usedParametersAndReturnVariables.at(originalFunctionName); + + FunctionDefinition linkingFunction = createLinkingFunction( + originalFunction, + used, + originalFunctionName, + linkingFunctionName, + _context.dispenser + ); + + originalFunction.name = originalFunctionName; + originalFunction.parameters = + filter(originalFunction.parameters, used.first); + originalFunction.returnVariables = + filter(originalFunction.returnVariables, used.second); + + return make_vector(move(originalFunction), move(linkingFunction)); + } + } + + return nullopt; + }); +} diff --git a/libyul/optimiser/UnusedFunctionParameterPruner.h b/libyul/optimiser/UnusedFunctionParameterPruner.h new file mode 100644 index 000000000..1f62a8b08 --- /dev/null +++ b/libyul/optimiser/UnusedFunctionParameterPruner.h @@ -0,0 +1,52 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see . +*/ +// SPDX-License-Identifier: GPL-3.0 + +#pragma once + +#include + +namespace solidity::yul +{ + +/** + * UnusedFunctionParameterPruner: Optimiser step that removes unused parameters in a function. + * + * If a parameter is unused, like `c` and `y` in, `function f(a,b,c) -> x, y { x := div(a,b) }` + * + * We remove the parameter and create a new "linking" function as follows: + * + * `function f(a,b) -> x { x := div(a,b) }` + * `function f2(a,b,c) -> x, y { x := f(a,b) }` + * + * and replace all references to `f` by `f2`. + * The inliner should be run afterwards to make sure that all references to `f2` are replaced by + * `f`. + * + * Prerequisites: Disambiguator, FunctionHoister, LiteralRematerialiser + * + * The step LiteralRematerialiser is not required for correctness. It helps deal with cases such as: + * `function f(x) -> y { revert(y, y} }` where the literal `y` will be replaced by its value `0`, + * allowing us to rewrite the function. + */ +struct UnusedFunctionParameterPruner +{ + static constexpr char const* name{"UnusedFunctionParameterPruner"}; + static void run(OptimiserStepContext& _context, Block& _ast); +}; + +} diff --git a/libyul/optimiser/UnusedFunctionsCommon.h b/libyul/optimiser/UnusedFunctionsCommon.h new file mode 100644 index 000000000..aaa8180f7 --- /dev/null +++ b/libyul/optimiser/UnusedFunctionsCommon.h @@ -0,0 +1,103 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see . +*/ +// SPDX-License-Identifier: GPL-3.0 +#pragma once + +#include +#include +#include +#include +#include + +#include + +#include + +#include + +namespace solidity::yul::unusedFunctionsCommon +{ + +template +std::vector filter(std::vector const& _vec, std::vector const& _mask) +{ + yulAssert(_vec.size() == _mask.size(), ""); + + std::vector ret; + + for (size_t i = 0; i < _mask.size(); ++i) + if (_mask[i]) + ret.push_back(_vec[i]); + + return ret; +} + +/// Returns true if applying UnusedFunctionParameterPruner is not helpful or redundant because the +/// inliner will be able to handle it anyway. +bool tooSimpleToBePruned(FunctionDefinition const& _f) +{ + return _f.body.statements.size() <= 1 && CodeSize::codeSize(_f.body) <= 1; +} + +FunctionDefinition createLinkingFunction( + FunctionDefinition const& _original, + std::pair, std::vector> const& _usedParametersAndReturns, + YulString const& _originalFunctionName, + YulString const& _linkingFunctionName, + NameDispenser& _nameDispenser +) +{ + auto generateTypedName = [&](TypedName t) + { + return TypedName{ + t.location, + _nameDispenser.newName(t.name), + t.type + }; + }; + + langutil::SourceLocation loc = _original.location; + + FunctionDefinition linkingFunction{ + loc, + _linkingFunctionName, + util::applyMap(_original.parameters, generateTypedName), + util::applyMap(_original.returnVariables, generateTypedName), + {loc, {}} // body + }; + + FunctionCall call{loc, Identifier{loc, _originalFunctionName}, {}}; + for (auto const& p: filter(linkingFunction.parameters, _usedParametersAndReturns.first)) + call.arguments.emplace_back(Identifier{loc, p.name}); + + Assignment assignment{loc, {}, nullptr}; + + for (auto const& r: filter(linkingFunction.returnVariables, _usedParametersAndReturns.second)) + assignment.variableNames.emplace_back(Identifier{loc, r.name}); + + if (assignment.variableNames.empty()) + linkingFunction.body.statements.emplace_back(ExpressionStatement{loc, std::move(call)}); + else + { + assignment.value = std::make_unique(std::move(call)); + linkingFunction.body.statements.emplace_back(std::move(assignment)); + } + + return linkingFunction; +} + +} diff --git a/scripts/ASTImportTest.sh b/scripts/ASTImportTest.sh index 6f8d8b06e..02125c921 100755 --- a/scripts/ASTImportTest.sh +++ b/scripts/ASTImportTest.sh @@ -1,10 +1,15 @@ #!/usr/bin/env bash +set -e + # Bash script to test the ast-import option of the compiler by # first exporting a .sol file to JSON, then loading it into the compiler # and exporting it again. The second JSON should be identical to the first - -REPO_ROOT=$(readlink -f "$(dirname "$0")"/..) +READLINK=readlink +if [[ "$OSTYPE" == "darwin"* ]]; then + READLINK=greadlink +fi +REPO_ROOT=$(${READLINK} -f "$(dirname "$0")"/..) SOLIDITY_BUILD_DIR=${SOLIDITY_BUILD_DIR:-${REPO_ROOT}/build} SOLC=${SOLIDITY_BUILD_DIR}/solc/solc SPLITSOURCES=${REPO_ROOT}/scripts/splitSources.py @@ -83,8 +88,11 @@ do FILETMP=$(mktemp -d) cd $FILETMP + set +e OUTPUT=$($SPLITSOURCES $solfile) - if [ $? != 1 ] + SPLITSOURCES_RC=$? + set -e + if [ ${SPLITSOURCES_RC} == 0 ] then # echo $OUTPUT NSOURCES=$((NSOURCES - 1)) @@ -93,9 +101,26 @@ do testImportExportEquivalence $i $OUTPUT NSOURCES=$((NSOURCES + 1)) done - - else + elif [ ${SPLITSOURCES_RC} == 1 ] + then testImportExportEquivalence $solfile + elif [ ${SPLITSOURCES_RC} == 2 ] + then + # The script will exit with return code 2, if an UnicodeDecodeError occurred. + # This is the case if e.g. some tests are using invalid utf-8 sequences. We will ignore + # these errors, but print the actual output of the script. + echo -e "\n${OUTPUT}\n" + testImportExportEquivalence $solfile + else + # All other return codes will be treated as critical errors. The script will exit. + echo -e "\nGot unexpected return code ${SPLITSOURCES_RC} from ${SPLITSOURCES}. Aborting." + echo -e "\n${OUTPUT}\n" + + cd $WORKINGDIR + # Delete temporary files + rm -rf $FILETMP + + exit 1 fi cd $WORKINGDIR diff --git a/scripts/release_ppa.sh b/scripts/release_ppa.sh index 3017692cc..965dace68 100755 --- a/scripts/release_ppa.sh +++ b/scripts/release_ppa.sh @@ -158,7 +158,7 @@ Vcs-Git: git://github.com/ethereum/solidity.git Vcs-Browser: https://github.com/ethereum/solidity Package: solc -Architecture: any-i386 any-amd64 +Architecture: any-amd64 Multi-Arch: same Depends: \${shlibs:Depends}, \${misc:Depends} Conflicts: libethereum (<= 1.2.9) diff --git a/scripts/splitSources.py b/scripts/splitSources.py index 01a9f9278..54ddb2f38 100755 --- a/scripts/splitSources.py +++ b/scripts/splitSources.py @@ -11,10 +11,20 @@ import sys import os +import traceback hasMultipleSources = False createdSources = [] + +def uncaught_exception_hook(exc_type, exc_value, exc_traceback): + # The script `scripts/ASTImportTest.sh` will interpret return code 3 + # as a critical error (because of the uncaught exception) and will + # terminate further execution. + print("Unhandled exception: %s", "".join(traceback.format_exception(exc_type, exc_value, exc_traceback))) + sys.exit(3) + + def extractSourceName(line): if line.find("/") > -1: filePath = line[13: line.rindex("/")] @@ -23,6 +33,7 @@ def extractSourceName(line): return filePath, srcName return False, line[line.find(":")+2 : line.find(" ====")] + # expects the first line of lines to be "==== Source: sourceName ====" # writes the following source into a file named sourceName def writeSourceToFile(lines): @@ -45,18 +56,29 @@ def writeSourceToFile(lines): writeSourceToFile(lines[1+idx:]) break + if __name__ == '__main__': filePath = sys.argv[1] - # decide if file has multiple sources - lines = open(filePath, mode='r', encoding='utf8').read().splitlines() - if lines[0][:12] == "==== Source:": - hasMultipleSources = True - writeSourceToFile(lines) + sys.excepthook = uncaught_exception_hook - if hasMultipleSources: - srcString = "" - for src in createdSources: - srcString += src + ' ' - print(srcString) - else: - sys.exit(1) + try: + # decide if file has multiple sources + lines = open(filePath, mode='r', encoding='utf8').read().splitlines() + if lines[0][:12] == "==== Source:": + hasMultipleSources = True + writeSourceToFile(lines) + + if hasMultipleSources: + srcString = "" + for src in createdSources: + srcString += src + ' ' + print(srcString) + sys.exit(0) + else: + sys.exit(1) + + except UnicodeDecodeError as ude: + print("UnicodeDecodeError in '" + filePath + "': " + str(ude)) + print("This is expected for some tests containing invalid utf8 sequences. " + "Exception will be ignored.") + sys.exit(2) diff --git a/scripts/test_antlr_grammar.sh b/scripts/test_antlr_grammar.sh index 846cecf80..a41387ee9 100755 --- a/scripts/test_antlr_grammar.sh +++ b/scripts/test_antlr_grammar.sh @@ -2,7 +2,11 @@ set -e -ROOT_DIR=$(readlink -f "$(dirname "$0")"/..) +READLINK=readlink +if [[ "$OSTYPE" == "darwin"* ]]; then + READLINK=greadlink +fi +ROOT_DIR=$(${READLINK} -f "$(dirname "$0")"/..) WORKDIR="${ROOT_DIR}/build/antlr" ANTLR_JAR="${ROOT_DIR}/build/deps/antlr4.jar" ANTLR_JAR_URI="https://www.antlr.org/download/antlr-4.8-complete.jar" @@ -54,7 +58,7 @@ failed_count=0 test_file() { local SOL_FILE - SOL_FILE="$(readlink -m "${1}")" + SOL_FILE="$(${READLINK} -m "${1}")" local cur=${2} local max=${3} local solOrYul=${4} diff --git a/test/cmdlineTests/evm_to_wasm_break/output b/test/cmdlineTests/evm_to_wasm_break/output index ddeb04529..ecb9a9ce3 100644 --- a/test/cmdlineTests/evm_to_wasm_break/output +++ b/test/cmdlineTests/evm_to_wasm_break/output @@ -31,9 +31,10 @@ object "object" { let x_6 := x_2 let x_7 := x_3 let _2 := 1 - let _3:i32 := i32.eqz(i32.eqz(i64.eqz(i64.or(i64.or(_1, _1), i64.or(_1, _2))))) + let _3 := i64.or(_1, _1) + let _4:i32 := i32.eqz(i32.eqz(i64.eqz(i64.or(_3, i64.or(_1, _2))))) for { } - i32.eqz(_3) + i32.eqz(_4) { let x_8, x_9, x_10, x_11 := add(x_4, x_5, x_6, x_7, _1, _1, _1, _2) x_4 := x_8 @@ -42,13 +43,10 @@ object "object" { x_7 := x_11 } { - let _4, _5, _6, _7 := lt(x_4, x_5, x_6, x_7, _1, _1, _1, 10) - let _8, _9, _10, _11 := iszero(_4, _5, _6, _7) - if i32.eqz(i64.eqz(i64.or(i64.or(_8, _9), i64.or(_10, _11)))) { break } - let _12, _13, _14, _15 := eq(x_4, x_5, x_6, x_7, _1, _1, _1, 2) - if i32.eqz(i64.eqz(i64.or(i64.or(_12, _13), i64.or(_14, _15)))) { break } - let _16, _17, _18, _19 := eq(x_4, x_5, x_6, x_7, _1, _1, _1, 4) - if i32.eqz(i64.eqz(i64.or(i64.or(_16, _17), i64.or(_18, _19)))) { continue } + let _5, _6, _7, _8 := iszero_170_789(_1, _1, _1, lt_172(x_4, x_5, x_6, x_7, _1, _1, _1, 10)) + if i32.eqz(i64.eqz(i64.or(i64.or(_5, _6), i64.or(_7, _8)))) { break } + if i32.eqz(i64.eqz(i64.or(_3, i64.or(_1, eq(x_4, x_5, x_6, x_7, _1, _1, _1, 2))))) { break } + if i32.eqz(i64.eqz(i64.or(_3, i64.or(_1, eq(x_4, x_5, x_6, x_7, _1, _1, _1, 4))))) { continue } } sstore(_1, _1, _1, _1, x_4, x_5, x_6, x_7) } @@ -69,11 +67,11 @@ object "object" { let r1_1, carry_2 := add_carry(x1, y1, carry_1) r1 := r1_1 } - function iszero(x1, x2, x3, x4) -> r1, r2, r3, r4 + function iszero_170_789(x1, x2, x3, x4) -> r1, r2, r3, r4 { r4 := i64.extend_i32_u(i64.eqz(i64.or(i64.or(x1, x2), i64.or(x3, x4)))) } - function eq(x1, x2, x3, x4, y1, y2, y3, y4) -> r1, r2, r3, r4 + function eq(x1, x2, x3, x4, y1, y2, y3, y4) -> r4 { if i64.eq(x1, y1) { @@ -89,7 +87,7 @@ object "object" { case 1:i32 { r := 0xffffffff:i32 } default { r := i64.ne(a, b) } } - function lt(x1, x2, x3, x4, y1, y2, y3, y4) -> z1, z2, z3, z4 + function lt_172(x1, x2, x3, x4, y1, y2, y3, y4) -> z4 { let z:i32 := false switch cmp(x1, y1) @@ -154,7 +152,7 @@ object "object" { Binary representation: -0061736d0100000001480a60000060017e017e60027e7e017f60037e7e7e017e60047e7e7e7e017e60087e7e7e7e7e7e7e7e0060087e7e7e7e7e7e7e7e017e60057f7e7e7e7e0060027f7f0060037f7f7f0002310208657468657265756d0c73746f7261676553746f7265000808657468657265756d0c63616c6c44617461436f70790009030e0d0003060406020604010101070505030100010610037e0142000b7e0142000b7e0142000b071102066d656d6f72790200046d61696e00020ac3080dde02030a7e017f147e02404200210002402000200020002000100921012300210223012103230221040b20012105200221062003210720042108420121092000200084200020098484504545210a02400340200a45450d01024002402005200620072008200020002000420a1008210b2300210c2301210d2302210e0b0240200b200c200d200e1005210f2300211023012111230221120b200f201084201120128484504504400c030b024020052006200720082000200020004202100621132300211423012115230221160b2013201484201520168484504504400c030b0240200520062007200820002000200042041006211723002118230121192302211a0b20172018842019201a8484504504400c010b0b0240200520062007200820002000200020091004211b2300211c2301211d2302211e0b201b2105201c2106201d2107201e21080c000b0b20002000200020002005200620072008100e0b0b2901037e0240200020017c2105200520027c21032005200054200320055472ad21040b2004240020030b6c010b7e0240200320077c210c200c42007c210b024020022006200c200354200b200c5472ad1003210d2300210e0b200d210a024020012005200e1003210f230021100b200f2109024020002004201010032111230021120b201121080b20092400200a2401200b240220080b2401047e0240200020018420022003848450ad21070b20052400200624012007240220040b3901047e0240200020045104402001200551044020022006510440200320075104404201210b0b0b0b0b0b20092400200a2401200b240220080b2701027f024002402000200154210320034101460440417f210205200020015221020b0b0b20020b960102047e047f02404100210c0240200020041007210d200d41004604400240200120051007210e200e41004604400240200220061007210f200f41004604402003200754210c05200f41014604404100210c054101210c0b0b0b05200e41014604404100210c054101210c0b0b0b05200d41014604404100210c054101210c0b0b0b200cad210b0b20092400200a2401200b240220080b7601087e024042002000200184200284520440000b42002003422088520440000b41002003a7412010014100290000100c2108410041086a290000100c2109410041106a290000100c210a410041186a290000100c210b2008210420092105200a2106200b21070b20052400200624012007240220040b1f01017e024020004208864280fe0383200042088842ff01838421010b20010b1e01027e02402000100a421086210220022000421088100a8421010b20010b1e01027e02402000100b422086210220022000422088100b8421010b20010b3200024020002001100c370000200041086a2002100c370000200041106a2003100c370000200041186a2004100c3700000b0b2300024041002000200120022003100d41202004200520062007100d4100412010000b0b +0061736d0100000001480a60000060017e017e60027e7e017f60037e7e7e017e60047e7e7e7e017e60087e7e7e7e7e7e7e7e0060087e7e7e7e7e7e7e7e017e60057f7e7e7e7e0060027f7f0060037f7f7f0002310208657468657265756d0c73746f7261676553746f7265000808657468657265756d0c63616c6c44617461436f70790009030e0d0003060406020604010101070505030100010610037e0142000b7e0142000b7e0142000b071102066d656d6f72790200046d61696e00020af0070da302030b7e017f087e02404200210002402000200020002000100921012300210223012103230221040b20012105200221062003210720042108420121092000200084210a200a200020098484504545210b02400340200b45450d01024002402000200020002005200620072008200020002000420a10081005210c2300210d2301210e2302210f0b200c200d84200e200f8484504504400c030b200a20002005200620072008200020002000420210068484504504400c030b200a20002005200620072008200020002000420410068484504504400c010b0b024020052006200720082000200020002009100421102300211123012112230221130b201021052011210620122107201321080c000b0b20002000200020002005200620072008100e0b0b2901037e0240200020017c2105200520027c21032005200054200320055472ad21040b2004240020030b6c010b7e0240200320077c210c200c42007c210b024020022006200c200354200b200c5472ad1003210d2300210e0b200d210a024020012005200e1003210f230021100b200f2109024020002004201010032111230021120b201121080b20092400200a2401200b240220080b2401047e0240200020018420022003848450ad21070b20052400200624012007240220040b2d01017e024020002004510440200120055104402002200651044020032007510440420121080b0b0b0b0b20080b2701027f024002402000200154210320034101460440417f210205200020015221020b0b0b20020b8a0102017e047f0240410021090240200020041007210a200a41004604400240200120051007210b200b41004604400240200220061007210c200c41004604402003200754210905200c41014604404100210905410121090b0b0b05200b41014604404100210905410121090b0b0b05200a41014604404100210905410121090b0b0b2009ad21080b20080b7601087e024042002000200184200284520440000b42002003422088520440000b41002003a7412010014100290000100c2108410041086a290000100c2109410041106a290000100c210a410041186a290000100c210b2008210420092105200a2106200b21070b20052400200624012007240220040b1f01017e024020004208864280fe0383200042088842ff01838421010b20010b1e01027e02402000100a421086210220022000421088100a8421010b20010b1e01027e02402000100b422086210220022000422088100b8421010b20010b3200024020002001100c370000200041086a2002100c370000200041106a2003100c370000200041186a2004100c3700000b0b2300024041002000200120022003100d41202004200520062007100d4100412010000b0b Text representation: (module @@ -177,23 +175,12 @@ Text representation: (local $x_6 i64) (local $x_7 i64) (local $_2 i64) - (local $_3 i32) - (local $_4 i64) + (local $_3 i64) + (local $_4 i32) (local $_5 i64) (local $_6 i64) (local $_7 i64) (local $_8 i64) - (local $_9 i64) - (local $_10 i64) - (local $_11 i64) - (local $_12 i64) - (local $_13 i64) - (local $_14 i64) - (local $_15 i64) - (local $_16 i64) - (local $_17 i64) - (local $_18 i64) - (local $_19 i64) (local $x_8 i64) (local $x_9 i64) (local $x_10 i64) @@ -212,46 +199,26 @@ Text representation: (local.set $x_6 (local.get $x_2)) (local.set $x_7 (local.get $x_3)) (local.set $_2 (i64.const 1)) - (local.set $_3 (i32.eqz (i32.eqz (i64.eqz (i64.or (i64.or (local.get $_1) (local.get $_1)) (i64.or (local.get $_1) (local.get $_2))))))) + (local.set $_3 (i64.or (local.get $_1) (local.get $_1))) + (local.set $_4 (i32.eqz (i32.eqz (i64.eqz (i64.or (local.get $_3) (i64.or (local.get $_1) (local.get $_2))))))) (block $label__3 (loop $label__5 - (br_if $label__3 (i32.eqz (i32.eqz (local.get $_3)))) + (br_if $label__3 (i32.eqz (i32.eqz (local.get $_4)))) (block $label__4 (block - (local.set $_4 (call $lt (local.get $x_4) (local.get $x_5) (local.get $x_6) (local.get $x_7) (local.get $_1) (local.get $_1) (local.get $_1) (i64.const 10))) - (local.set $_5 (global.get $global_)) - (local.set $_6 (global.get $global__1)) - (local.set $_7 (global.get $global__2)) + (local.set $_5 (call $iszero_170_789 (local.get $_1) (local.get $_1) (local.get $_1) (call $lt_172 (local.get $x_4) (local.get $x_5) (local.get $x_6) (local.get $x_7) (local.get $_1) (local.get $_1) (local.get $_1) (i64.const 10)))) + (local.set $_6 (global.get $global_)) + (local.set $_7 (global.get $global__1)) + (local.set $_8 (global.get $global__2)) ) - (block - (local.set $_8 (call $iszero (local.get $_4) (local.get $_5) (local.get $_6) (local.get $_7))) - (local.set $_9 (global.get $global_)) - (local.set $_10 (global.get $global__1)) - (local.set $_11 (global.get $global__2)) - - ) - (if (i32.eqz (i64.eqz (i64.or (i64.or (local.get $_8) (local.get $_9)) (i64.or (local.get $_10) (local.get $_11))))) (then + (if (i32.eqz (i64.eqz (i64.or (i64.or (local.get $_5) (local.get $_6)) (i64.or (local.get $_7) (local.get $_8))))) (then (br $label__3) )) - (block - (local.set $_12 (call $eq (local.get $x_4) (local.get $x_5) (local.get $x_6) (local.get $x_7) (local.get $_1) (local.get $_1) (local.get $_1) (i64.const 2))) - (local.set $_13 (global.get $global_)) - (local.set $_14 (global.get $global__1)) - (local.set $_15 (global.get $global__2)) - - ) - (if (i32.eqz (i64.eqz (i64.or (i64.or (local.get $_12) (local.get $_13)) (i64.or (local.get $_14) (local.get $_15))))) (then + (if (i32.eqz (i64.eqz (i64.or (local.get $_3) (i64.or (local.get $_1) (call $eq (local.get $x_4) (local.get $x_5) (local.get $x_6) (local.get $x_7) (local.get $_1) (local.get $_1) (local.get $_1) (i64.const 2)))))) (then (br $label__3) )) - (block - (local.set $_16 (call $eq (local.get $x_4) (local.get $x_5) (local.get $x_6) (local.get $x_7) (local.get $_1) (local.get $_1) (local.get $_1) (i64.const 4))) - (local.set $_17 (global.get $global_)) - (local.set $_18 (global.get $global__1)) - (local.set $_19 (global.get $global__2)) - - ) - (if (i32.eqz (i64.eqz (i64.or (i64.or (local.get $_16) (local.get $_17)) (i64.or (local.get $_18) (local.get $_19))))) (then + (if (i32.eqz (i64.eqz (i64.or (local.get $_3) (i64.or (local.get $_1) (call $eq (local.get $x_4) (local.get $x_5) (local.get $x_6) (local.get $x_7) (local.get $_1) (local.get $_1) (local.get $_1) (i64.const 4)))))) (then (br $label__4) )) @@ -343,7 +310,7 @@ Text representation: (local.get $r1) ) -(func $iszero +(func $iszero_170_789 (param $x1 i64) (param $x2 i64) (param $x3 i64) @@ -373,9 +340,6 @@ Text representation: (param $y3 i64) (param $y4 i64) (result i64) - (local $r1 i64) - (local $r2 i64) - (local $r3 i64) (local $r4 i64) (block $label__9 (if (i64.eq (local.get $x1) (local.get $y1)) (then @@ -389,10 +353,7 @@ Text representation: )) ) - (global.set $global_ (local.get $r2)) - (global.set $global__1 (local.get $r3)) - (global.set $global__2 (local.get $r4)) - (local.get $r1) + (local.get $r4) ) (func $cmp @@ -416,7 +377,7 @@ Text representation: (local.get $r) ) -(func $lt +(func $lt_172 (param $x1 i64) (param $x2 i64) (param $x3 i64) @@ -426,9 +387,6 @@ Text representation: (param $y3 i64) (param $y4 i64) (result i64) - (local $z1 i64) - (local $z2 i64) - (local $z3 i64) (local $z4 i64) (local $z i32) (local $condition_12 i32) @@ -476,10 +434,7 @@ Text representation: (local.set $z4 (i64.extend_i32_u (local.get $z))) ) - (global.set $global_ (local.get $z2)) - (global.set $global__1 (local.get $z3)) - (global.set $global__2 (local.get $z4)) - (local.get $z1) + (local.get $z4) ) (func $calldataload diff --git a/test/cmdlineTests/yul_stack_opt/input.sol b/test/cmdlineTests/yul_stack_opt/input.sol index 772a6d4df..d60620ecf 100644 --- a/test/cmdlineTests/yul_stack_opt/input.sol +++ b/test/cmdlineTests/yul_stack_opt/input.sol @@ -17,6 +17,21 @@ sstore(add(a, 10), b) sstore(add(a, 11), b) sstore(add(a, 12), b) + a3 := 1 + b3 := 1 + c3 := 1 + d3 := 1 + e3 := 1 + f3 := 1 + g3 := 1 + h3 := 1 + i3 := 1 + j3 := 1 + k3 := 1 + l3 := 1 + m3 := 1 + o3 := 1 + p3 := 1 } let a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1 := fun() let a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2, n2, o2, p2 := fun() diff --git a/test/cmdlineTests/yul_stack_opt/output b/test/cmdlineTests/yul_stack_opt/output index e5731f1e1..a02859f1e 100644 --- a/test/cmdlineTests/yul_stack_opt/output +++ b/test/cmdlineTests/yul_stack_opt/output @@ -5,11 +5,11 @@ Pretty printed source: object "object" { code { { - let a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1 := fun() - let a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2, n2, o2, p2 := fun() - sstore(a1, a2) + let a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, o3, p3 := fun() + let a3_1, b3_1, c3_1, d3_1, e3_1, f3_1, g3_1, h3_1, i3_1, j3_1, k3_1, l3_1, m3_1, o3_1, p3_1 := fun() + sstore(a3, a3_1) } - function fun() -> a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3 + function fun() -> a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, o3, p3 { let _1 := 1 sstore(_1, _1) @@ -25,21 +25,35 @@ object "object" { sstore(11, _1) sstore(12, _1) sstore(13, _1) + a3 := _1 + b3 := _1 + c3 := _1 + d3 := _1 + e3 := _1 + f3 := _1 + g3 := _1 + h3 := _1 + i3 := _1 + j3 := _1 + k3 := _1 + l3 := _1 + m3 := _1 + o3 := _1 + p3 := _1 } } } Binary representation: -60056032565b505050505050505050505050505050601a6032565b5050505050505050505050505050508082555050609b565b60006000600060006000600060006000600060006000600060006000600060006001808155806002558060035580600455806005558060065580600755806008558060095580600a5580600b5580600c5580600d55505b909192939495969798999a9b9c9d9e9f565b +60056030565b505050505050505050505050505060196030565b5050505050505050505050505050808255505060c3565b6000600060006000600060006000600060006000600060006000600060006001808155806002558060035580600455806005558060065580600755806008558060095580600a5580600b5580600c5580600d55809f50809e50809d50809c50809b50809a50809950809850809750809650809550809450809350809250809150505b909192939495969798999a9b9c9d9e565b Text representation: - /* "yul_stack_opt/input.sol":495:500 */ + /* "yul_stack_opt/input.sol":3:573 */ tag_1 tag_2 jump // in tag_1: - /* "yul_stack_opt/input.sol":425:500 */ pop pop pop @@ -54,13 +68,10 @@ tag_1: pop pop pop - pop - /* "yul_stack_opt/input.sol":572:577 */ tag_3 tag_2 jump // in tag_3: - /* "yul_stack_opt/input.sol":502:577 */ pop pop pop @@ -75,16 +86,15 @@ tag_3: pop pop pop - pop - /* "yul_stack_opt/input.sol":590:592 */ + /* "yul_stack_opt/input.sol":740:742 */ dup1 - /* "yul_stack_opt/input.sol":586:588 */ + /* "yul_stack_opt/input.sol":736:738 */ dup3 - /* "yul_stack_opt/input.sol":579:593 */ + /* "yul_stack_opt/input.sol":729:743 */ sstore pop pop - /* "yul_stack_opt/input.sol":3:423 */ + /* "yul_stack_opt/input.sol":3:573 */ jump(tag_4) tag_2: 0x00 @@ -101,7 +111,6 @@ tag_2: 0x00 0x00 0x00 - 0x00 0x00 /* "yul_stack_opt/input.sol":98:99 */ 0x01 @@ -181,8 +190,83 @@ tag_2: 0x0d /* "yul_stack_opt/input.sol":399:420 */ sstore + /* "yul_stack_opt/input.sol":98:99 */ + dup1 + /* "yul_stack_opt/input.sol":423:430 */ + swap16 pop - /* "yul_stack_opt/input.sol":85:423 */ + /* "yul_stack_opt/input.sol":98:99 */ + dup1 + /* "yul_stack_opt/input.sol":433:440 */ + swap15 + pop + /* "yul_stack_opt/input.sol":98:99 */ + dup1 + /* "yul_stack_opt/input.sol":443:450 */ + swap14 + pop + /* "yul_stack_opt/input.sol":98:99 */ + dup1 + /* "yul_stack_opt/input.sol":453:460 */ + swap13 + pop + /* "yul_stack_opt/input.sol":98:99 */ + dup1 + /* "yul_stack_opt/input.sol":463:470 */ + swap12 + pop + /* "yul_stack_opt/input.sol":98:99 */ + dup1 + /* "yul_stack_opt/input.sol":473:480 */ + swap11 + pop + /* "yul_stack_opt/input.sol":98:99 */ + dup1 + /* "yul_stack_opt/input.sol":483:490 */ + swap10 + pop + /* "yul_stack_opt/input.sol":98:99 */ + dup1 + /* "yul_stack_opt/input.sol":493:500 */ + swap9 + pop + /* "yul_stack_opt/input.sol":98:99 */ + dup1 + /* "yul_stack_opt/input.sol":503:510 */ + swap8 + pop + /* "yul_stack_opt/input.sol":98:99 */ + dup1 + /* "yul_stack_opt/input.sol":513:520 */ + swap7 + pop + /* "yul_stack_opt/input.sol":98:99 */ + dup1 + /* "yul_stack_opt/input.sol":523:530 */ + swap6 + pop + /* "yul_stack_opt/input.sol":98:99 */ + dup1 + /* "yul_stack_opt/input.sol":533:540 */ + swap5 + pop + /* "yul_stack_opt/input.sol":98:99 */ + dup1 + /* "yul_stack_opt/input.sol":543:550 */ + swap4 + pop + /* "yul_stack_opt/input.sol":98:99 */ + dup1 + /* "yul_stack_opt/input.sol":553:560 */ + swap3 + pop + /* "yul_stack_opt/input.sol":98:99 */ + dup1 + /* "yul_stack_opt/input.sol":563:570 */ + swap2 + pop + pop + /* "yul_stack_opt/input.sol":85:573 */ tag_5: swap1 swap2 @@ -199,6 +283,5 @@ tag_5: swap13 swap14 swap15 - swap16 jump // out tag_4: diff --git a/test/libsolidity/StandardCompiler.cpp b/test/libsolidity/StandardCompiler.cpp index d71cf10f1..b02ebbe2e 100644 --- a/test/libsolidity/StandardCompiler.cpp +++ b/test/libsolidity/StandardCompiler.cpp @@ -29,6 +29,7 @@ #include #include +#include #include using namespace std; @@ -1235,9 +1236,16 @@ BOOST_AUTO_TEST_CASE(use_stack_optimization) BOOST_REQUIRE(contract["evm"]["bytecode"]["object"].isString()); BOOST_CHECK(contract["evm"]["bytecode"]["object"].asString().length() > 20); - // Now disable stack optimizations + // Now disable stack optimizations and UnusedFunctionParameterPruner (p) // results in "stack too deep" + string optimiserSteps = OptimiserSettings::DefaultYulOptimiserSteps; + optimiserSteps.erase( + remove_if(optimiserSteps.begin(), optimiserSteps.end(), [](char ch) { return ch == 'p'; }), + optimiserSteps.end() + ); parsedInput["settings"]["optimizer"]["details"]["yulDetails"]["stackAllocation"] = false; + parsedInput["settings"]["optimizer"]["details"]["yulDetails"]["optimizerSteps"] = optimiserSteps; + result = compiler.compile(parsedInput); BOOST_REQUIRE(result["errors"].isArray()); BOOST_CHECK(result["errors"][0]["severity"] == "error"); diff --git a/test/libsolidity/gasTests/abiv2_optimised.sol b/test/libsolidity/gasTests/abiv2_optimised.sol index 74cd89a42..47eaeaceb 100644 --- a/test/libsolidity/gasTests/abiv2_optimised.sol +++ b/test/libsolidity/gasTests/abiv2_optimised.sol @@ -17,9 +17,9 @@ contract C { // optimize-yul: true // ---- // creation: -// codeDepositCost: 616600 +// codeDepositCost: 614600 // executionCost: 651 -// totalCost: 617251 +// totalCost: 615251 // external: // a(): 1029 // b(uint256): 2084 diff --git a/test/libsolidity/semanticTests/array/array_copy_memory_to_storage.sol b/test/libsolidity/semanticTests/array/array_copy_memory_to_storage.sol new file mode 100644 index 000000000..3055b0fa8 --- /dev/null +++ b/test/libsolidity/semanticTests/array/array_copy_memory_to_storage.sol @@ -0,0 +1,11 @@ +contract C { + uint[] a; + function f() public returns (uint, uint) { + uint[] memory b = new uint[](3); + b[0] = 1; + a = b; + return (a[0], a.length); + } +} +// ---- +// f() -> 1, 3 diff --git a/test/libsolidity/semanticTests/array/array_copy_storage_to_memory.sol b/test/libsolidity/semanticTests/array/array_copy_storage_to_memory.sol new file mode 100644 index 000000000..8bc6b86a2 --- /dev/null +++ b/test/libsolidity/semanticTests/array/array_copy_storage_to_memory.sol @@ -0,0 +1,10 @@ +contract C { + uint[] a; + function f() public returns (uint, uint) { + a.push(1); a.push(0); a.push(0); + uint[] memory b = a; + return (b[0], b.length); + } +} +// ---- +// f() -> 1, 3 diff --git a/test/libsolidity/semanticTests/array/bytes_memory_to_storage.sol b/test/libsolidity/semanticTests/array/bytes_memory_to_storage.sol new file mode 100644 index 000000000..eebdb7e9b --- /dev/null +++ b/test/libsolidity/semanticTests/array/bytes_memory_to_storage.sol @@ -0,0 +1,10 @@ +contract C { + bytes s; + function f() external returns (byte) { + bytes memory data = "abcd"; + s = data; + return s[0]; + } +} +// ---- +// f() -> "a" diff --git a/test/libsolidity/semanticTests/array/bytes_storage_to_memory.sol b/test/libsolidity/semanticTests/array/bytes_storage_to_memory.sol new file mode 100644 index 000000000..13932a2cc --- /dev/null +++ b/test/libsolidity/semanticTests/array/bytes_storage_to_memory.sol @@ -0,0 +1,9 @@ +contract C { + bytes s = "abcd"; + function f() external returns (byte) { + bytes memory data = s; + return data[0]; + } +} +// ---- +// f() -> "a" diff --git a/test/libsolidity/semanticTests/calldata/calldata_bytes_to_storage.sol b/test/libsolidity/semanticTests/calldata/calldata_bytes_to_storage.sol new file mode 100644 index 000000000..07041910d --- /dev/null +++ b/test/libsolidity/semanticTests/calldata/calldata_bytes_to_storage.sol @@ -0,0 +1,9 @@ +contract C { + bytes s; + function f(bytes calldata data) external returns (byte) { + s = data; + return s[0]; + } +} +// ---- +// f(bytes): 0x20, 0x08, "abcdefgh" -> "a" diff --git a/test/libsolidity/semanticTests/intheritance/super_in_constructor.sol b/test/libsolidity/semanticTests/intheritance/super_in_constructor.sol index 5be2158a2..24f1f1e17 100644 --- a/test/libsolidity/semanticTests/intheritance/super_in_constructor.sol +++ b/test/libsolidity/semanticTests/intheritance/super_in_constructor.sol @@ -30,6 +30,7 @@ contract D is B, C { return data; } } - +// ==== +// compileViaYul: also // ---- // f() -> 15 diff --git a/test/libsolidity/semanticTests/intheritance/super_in_constructor_assignment.sol b/test/libsolidity/semanticTests/intheritance/super_in_constructor_assignment.sol new file mode 100644 index 000000000..46acb36d0 --- /dev/null +++ b/test/libsolidity/semanticTests/intheritance/super_in_constructor_assignment.sol @@ -0,0 +1,39 @@ +contract A { + function f() public virtual returns (uint256 r) { + return 1; + } +} + + +contract B is A { + function f() public virtual override returns (uint256 r) { + function() internal returns (uint) x = super.f; + return x() | 2; + } +} + + +contract C is A { + function f() public virtual override returns (uint256 r) { + function() internal returns (uint) x = super.f; + return x() | 4; + } +} + + +contract D is B, C { + uint256 data; + + constructor() { + function() internal returns (uint) x = super.f; + data = x() | 8; + } + + function f() public override (B, C) returns (uint256 r) { + return data; + } +} +// ==== +// compileViaYul: also +// ---- +// f() -> 15 diff --git a/test/libsolidity/semanticTests/intheritance/super_overload.sol b/test/libsolidity/semanticTests/intheritance/super_overload.sol index 6a1f6dc3d..b7cbf10b3 100644 --- a/test/libsolidity/semanticTests/intheritance/super_overload.sol +++ b/test/libsolidity/semanticTests/intheritance/super_overload.sol @@ -22,6 +22,8 @@ contract C is A, B { } } +// ==== +// compileViaYul: also // ---- // g() -> 10 // h() -> 2 diff --git a/test/libsolidity/semanticTests/structs/calldata/calldata_struct_to_memory.sol b/test/libsolidity/semanticTests/structs/calldata/calldata_struct_to_memory.sol index 04d675371..1841d4fc1 100644 --- a/test/libsolidity/semanticTests/structs/calldata/calldata_struct_to_memory.sol +++ b/test/libsolidity/semanticTests/structs/calldata/calldata_struct_to_memory.sol @@ -4,15 +4,16 @@ contract C { struct S { uint256 a; uint256 b; + bytes2 c; } - function f(S calldata s) external pure returns (uint256, uint256) { + function f(S calldata s) external pure returns (uint256, uint256, byte) { S memory m = s; - return (m.a, m.b); + return (m.a, m.b, m.c[1]); } } // ==== // compileViaYul: also // ---- -// f((uint256,uint256)): 42, 23 -> 42, 23 +// f((uint256,uint256, bytes2)): 42, 23, "ab" -> 42, 23, "b" diff --git a/test/libsolidity/semanticTests/structs/calldata/calldata_struct_to_storage.sol b/test/libsolidity/semanticTests/structs/calldata/calldata_struct_to_storage.sol new file mode 100644 index 000000000..b97ff80c4 --- /dev/null +++ b/test/libsolidity/semanticTests/structs/calldata/calldata_struct_to_storage.sol @@ -0,0 +1,22 @@ +pragma experimental ABIEncoderV2; + +contract C { + struct S { + uint256 a; + uint64 b; + bytes2 c; + } + + uint[153] r; + S s; + + function f(uint32 a, S calldata c, uint256 b) external returns (uint256, uint256, byte) { + s = c; + return (s.a, s.b, s.c[1]); + } +} + +// ==== +// compileViaYul: also +// ---- +// f(uint32, (uint256, uint64, bytes2), uint256): 1, 42, 23, "ab", 1 -> 42, 23, "b" \ No newline at end of file diff --git a/test/libsolidity/semanticTests/structs/struct_copy_via_local.sol b/test/libsolidity/semanticTests/structs/struct_copy_via_local.sol index a1cfcac05..bc2ade361 100644 --- a/test/libsolidity/semanticTests/structs/struct_copy_via_local.sol +++ b/test/libsolidity/semanticTests/structs/struct_copy_via_local.sol @@ -3,6 +3,7 @@ contract c { uint256 a; uint256 b; } + uint[75] r; Struct data1; Struct data2; @@ -15,5 +16,7 @@ contract c { } } +// ==== +// compileViaYul: also // ---- // test() -> true diff --git a/test/libsolidity/semanticTests/structs/struct_memory_to_storage.sol b/test/libsolidity/semanticTests/structs/struct_memory_to_storage.sol new file mode 100644 index 000000000..fd965f12b --- /dev/null +++ b/test/libsolidity/semanticTests/structs/struct_memory_to_storage.sol @@ -0,0 +1,28 @@ +pragma experimental ABIEncoderV2; + +contract C { + struct S { + uint32 a; + uint128 b; + uint256 c; + } + + struct X { + uint256 a; + S s; + } + + uint[79] r; + X x; + + function f() external returns (uint32, uint128, uint256) { + X memory m = X(12, S(42, 23, 34)); + x = m; + return (x.s.a, x.s.b, x.s.c); + } +} + +// ==== +// compileViaYul: also +// ---- +// f() -> 42, 23, 34 diff --git a/test/libsolidity/semanticTests/structs/struct_memory_to_storage_function_ptr.sol b/test/libsolidity/semanticTests/structs/struct_memory_to_storage_function_ptr.sol new file mode 100644 index 000000000..2a8b36f36 --- /dev/null +++ b/test/libsolidity/semanticTests/structs/struct_memory_to_storage_function_ptr.sol @@ -0,0 +1,33 @@ +pragma experimental ABIEncoderV2; + +contract C { + struct S { + uint32 a; + uint128 b; + uint256 c; + function() internal returns (uint32) f; + } + + struct X { + uint256 a; + S s; + } + + uint[79] r; + X x; + + function f() external returns (uint32, uint128, uint256, uint32, uint32) { + X memory m = X(12, S(42, 23, 34, g)); + x = m; + return (x.s.a, x.s.b, x.s.c, x.s.f(), m.s.f()); + } + + function g() internal returns (uint32) { + return x.s.a; + } +} + +// ==== +// compileViaYul: false +// ---- +// f() -> 42, 23, 34, 42, 42 diff --git a/test/libsolidity/semanticTests/structs/struct_named_constructor.sol b/test/libsolidity/semanticTests/structs/struct_named_constructor.sol index f74cc90bd..12e69bdfc 100644 --- a/test/libsolidity/semanticTests/structs/struct_named_constructor.sol +++ b/test/libsolidity/semanticTests/structs/struct_named_constructor.sol @@ -10,5 +10,7 @@ contract C { } } +// ==== +// compileViaYul: also // ---- // s() -> 1, true diff --git a/test/libsolidity/semanticTests/structs/struct_storage_to_memory.sol b/test/libsolidity/semanticTests/structs/struct_storage_to_memory.sol new file mode 100644 index 000000000..28c6284ee --- /dev/null +++ b/test/libsolidity/semanticTests/structs/struct_storage_to_memory.sol @@ -0,0 +1,26 @@ +pragma experimental ABIEncoderV2; + +contract C { + struct S { + uint32 a; + uint128 b; + uint256 c; + } + struct X { + uint32 a; + S s; + } + + uint[79] arr; + X x = X(12, S(42, 23, 34)); + + function f() external returns (uint32, uint128, uint256) { + X memory m = x; + return (m.s.a, m.s.b, m.s.c); + } +} + +// ==== +// compileViaYul: also +// ---- +// f() -> 42, 23, 34 diff --git a/test/libsolidity/semanticTests/structs/struct_storage_to_memory_function_ptr.sol b/test/libsolidity/semanticTests/structs/struct_storage_to_memory_function_ptr.sol new file mode 100644 index 000000000..12ba289ea --- /dev/null +++ b/test/libsolidity/semanticTests/structs/struct_storage_to_memory_function_ptr.sol @@ -0,0 +1,32 @@ +pragma experimental ABIEncoderV2; + +contract C { + struct S { + uint32 a; + uint128 b; + uint256 c; + function() internal returns (uint32) f; + } + + struct X { + uint256 a; + S s; + } + + uint[79] arr; + X x = X(12, S(42, 23, 34, g)); + + function f() external returns (uint32, uint128, uint256, uint32, uint32) { + X memory m = x; + return (m.s.a, m.s.b, m.s.c, m.s.f(), x.s.f()); + } + + function g() internal returns (uint32) { + return x.s.a; + } +} + +// ==== +// compileViaYul: false +// ---- +// f() -> 42, 23, 34, 42, 42 diff --git a/test/libsolidity/semanticTests/various/super.sol b/test/libsolidity/semanticTests/various/super.sol index 16e4257e1..cfaa0204c 100644 --- a/test/libsolidity/semanticTests/various/super.sol +++ b/test/libsolidity/semanticTests/various/super.sol @@ -25,5 +25,7 @@ contract D is B, C { } } +// ==== +// compileViaYul: also // ---- // f() -> 15 diff --git a/test/libsolidity/semanticTests/various/super_parentheses.sol b/test/libsolidity/semanticTests/various/super_parentheses.sol new file mode 100644 index 000000000..e5d07f10d --- /dev/null +++ b/test/libsolidity/semanticTests/various/super_parentheses.sol @@ -0,0 +1,31 @@ +contract A { + function f() public virtual returns (uint256 r) { + return 1; + } +} + + +contract B is A { + function f() public virtual override returns (uint256 r) { + return ((super).f)() | 2; + } +} + + +contract C is A { + function f() public virtual override returns (uint256 r) { + return ((super).f)() | 4; + } +} + + +contract D is B, C { + function f() public override(B, C) returns (uint256 r) { + return ((super).f)() | 8; + } +} + +// ==== +// compileViaYul: also +// ---- +// f() -> 15 diff --git a/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_1.sol b/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_1.sol index 3312aede3..8857b91db 100644 --- a/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_1.sol +++ b/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_1.sol @@ -11,10 +11,3 @@ contract C { } } // ---- -// Warning 6328: (119-157): Assertion violation happens here -// Warning 8115: (76-80): Assertion checker does not yet support the type of this variable. -// Warning 8115: (83-87): Assertion checker does not yet support the type of this variable. -// Warning 7650: (126-132): Assertion checker does not yet support this expression. -// Warning 8364: (126-128): Assertion checker does not yet implement type struct C.S storage ref -// Warning 7650: (143-149): Assertion checker does not yet support this expression. -// Warning 8364: (143-145): Assertion checker does not yet implement type struct C.S storage ref diff --git a/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol b/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol index c07ab4aad..67852d556 100644 --- a/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol +++ b/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol @@ -11,12 +11,3 @@ contract C { } } // ---- -// Warning 6328: (121-165): Assertion violation happens here -// Warning 8115: (78-82): Assertion checker does not yet support the type of this variable. -// Warning 8115: (85-89): Assertion checker does not yet support the type of this variable. -// Warning 7650: (128-134): Assertion checker does not yet support this expression. -// Warning 8364: (128-130): Assertion checker does not yet implement type struct C.S storage ref -// Warning 9118: (128-137): Assertion checker does not yet implement this expression. -// Warning 7650: (148-154): Assertion checker does not yet support this expression. -// Warning 8364: (148-150): Assertion checker does not yet implement type struct C.S storage ref -// Warning 9118: (148-157): Assertion checker does not yet implement this expression. diff --git a/test/libsolidity/smtCheckerTests/array_members/push_struct_member_1.sol b/test/libsolidity/smtCheckerTests/array_members/push_struct_member_1.sol index f2c30c84d..b2e500c74 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_struct_member_1.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_struct_member_1.sol @@ -15,13 +15,3 @@ contract C { } // ---- -// Warning 8115: (72-75): Assertion checker does not yet support the type of this variable. -// Warning 8115: (100-103): Assertion checker does not yet support the type of this variable. -// Warning 7650: (130-133): Assertion checker does not yet support this expression. -// Warning 8364: (130-131): Assertion checker does not yet implement type struct C.S storage ref -// Warning 9599: (130-133): Assertion checker does not yet implement this expression. -// Warning 7650: (144-149): Assertion checker does not yet support this expression. -// Warning 8364: (144-147): Assertion checker does not yet implement type struct C.S storage ref -// Warning 7650: (144-147): Assertion checker does not yet support this expression. -// Warning 8364: (144-145): Assertion checker does not yet implement type struct C.T storage ref -// Warning 9599: (144-149): Assertion checker does not yet implement this expression. diff --git a/test/libsolidity/smtCheckerTests/array_members/push_struct_member_2.sol b/test/libsolidity/smtCheckerTests/array_members/push_struct_member_2.sol index a717c8d4b..ba9a84713 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_struct_member_2.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_struct_member_2.sol @@ -16,18 +16,3 @@ contract C { } // ---- -// Warning 8115: (72-75): Assertion checker does not yet support the type of this variable. -// Warning 8115: (102-105): Assertion checker does not yet support the type of this variable. -// Warning 7650: (132-135): Assertion checker does not yet support this expression. -// Warning 8364: (132-133): Assertion checker does not yet implement type struct C.S storage ref -// Warning 9599: (132-135): Assertion checker does not yet implement this expression. -// Warning 7650: (146-149): Assertion checker does not yet support this expression. -// Warning 8364: (146-147): Assertion checker does not yet implement type struct C.T storage ref -// Warning 8364: (146-156): Assertion checker does not yet implement type struct C.S storage ref -// Warning 9599: (146-149): Assertion checker does not yet implement this expression. -// Warning 7650: (160-168): Assertion checker does not yet support this expression. -// Warning 7650: (160-163): Assertion checker does not yet support this expression. -// Warning 8364: (160-161): Assertion checker does not yet implement type struct C.T storage ref -// Warning 8364: (160-166): Assertion checker does not yet implement type struct C.S storage ref -// Warning 9118: (160-166): Assertion checker does not yet implement this expression. -// Warning 9599: (160-168): Assertion checker does not yet implement this expression. diff --git a/test/libsolidity/smtCheckerTests/complex/slither/data_dependency.sol b/test/libsolidity/smtCheckerTests/complex/slither/data_dependency.sol index 6fc041fb1..074bc5b10 100644 --- a/test/libsolidity/smtCheckerTests/complex/slither/data_dependency.sol +++ b/test/libsolidity/smtCheckerTests/complex/slither/data_dependency.sol @@ -118,23 +118,3 @@ contract PropagateThroughReturnValue { } // ---- // Warning 2018: (1879-1947): Function state mutability can be restricted to view -// Warning 8115: (318-332): Assertion checker does not yet support the type of this variable. -// Warning 8115: (338-347): Assertion checker does not yet support the type of this variable. -// Warning 8115: (353-378): Assertion checker does not yet support the type of this variable. -// Warning 8115: (384-409): Assertion checker does not yet support the type of this variable. -// Warning 7650: (464-479): Assertion checker does not yet support this expression. -// Warning 8364: (464-475): Assertion checker does not yet implement type struct Reference.St storage ref -// Warning 8182: (464-494): Assertion checker does not yet implement such assignments. -// Warning 7650: (539-554): Assertion checker does not yet support this expression. -// Warning 8364: (539-550): Assertion checker does not yet implement type struct Reference.St storage ref -// Warning 7650: (557-567): Assertion checker does not yet support this expression. -// Warning 8364: (557-563): Assertion checker does not yet implement type struct Reference.St storage ref -// Warning 8182: (539-567): Assertion checker does not yet implement such assignments. -// Warning 8115: (629-643): Assertion checker does not yet support the type of this variable. -// Warning 8364: (646-668): Assertion checker does not yet implement type struct Reference.St storage ref -// Warning 8364: (700-703): Assertion checker does not yet implement type struct Reference.St storage pointer -// Warning 8364: (706-728): Assertion checker does not yet implement type struct Reference.St storage ref -// Warning 8364: (700-728): Assertion checker does not yet implement type struct Reference.St storage pointer -// Warning 7650: (748-755): Assertion checker does not yet support this expression. -// Warning 8364: (748-751): Assertion checker does not yet implement type struct Reference.St storage pointer -// Warning 8182: (748-770): Assertion checker does not yet implement such assignments. diff --git a/test/libsolidity/smtCheckerTests/complex/warn_on_struct.sol b/test/libsolidity/smtCheckerTests/complex/warn_on_struct.sol index 287e7e8f6..0bbf08c56 100644 --- a/test/libsolidity/smtCheckerTests/complex/warn_on_struct.sol +++ b/test/libsolidity/smtCheckerTests/complex/warn_on_struct.sol @@ -8,7 +8,5 @@ contract C { } // ---- // Warning 2072: (133-143): Unused local variable. -// Warning 8115: (133-143): Assertion checker does not yet support the type of this variable. // Warning 8364: (146-147): Assertion checker does not yet implement type type(struct C.A storage pointer) -// Warning 8364: (146-163): Assertion checker does not yet implement type struct C.A memory // Warning 4639: (146-163): Assertion checker does not yet implement this expression. diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol index 7f859ef82..4f68132ab 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol @@ -20,3 +20,4 @@ contract LoopFor2 { } // ---- // Warning 6328: (363-382): Assertion violation happens here +// Warning 4661: (316-336): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol index b8cf6aef4..faf0ee71b 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol @@ -21,3 +21,4 @@ contract LoopFor2 { // ---- // Warning 6328: (341-360): Assertion violation happens here // Warning 6328: (364-383): Assertion violation happens here +// Warning 4661: (317-337): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_code_after_placeholder.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_code_after_placeholder.sol index f543be8db..6f3701d41 100644 --- a/test/libsolidity/smtCheckerTests/modifiers/modifier_code_after_placeholder.sol +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_code_after_placeholder.sol @@ -21,5 +21,5 @@ contract C } } // ---- -// Warning 4984: (203-208): Overflow (resulting value larger than 2**256 - 1) happens here +// Warning 4984: (203-208): Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 6328: (136-149): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_rational_1.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_rational_1.sol new file mode 100644 index 000000000..97343e235 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_rational_1.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; + +contract C { + function f() public pure { + uint x = uint(~1); + // This assertion fails because type conversion is still unsupported. + assert(x == 2**256 - 2); + assert(~1 == -2); + } +} +// ---- +// Warning 6328: (169-192): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_rational_2.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_rational_2.sol new file mode 100644 index 000000000..94bb5cc83 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_rational_2.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; + +contract C { + function f() public pure { + assert(~1 | (~0xff & 0) == -2); + int x = ~1 | (~0xff ^ 0); + /// Result is negative, assertion fails. + assert(x > 0); + int y = ~x | (0xff & 1); + assert(y > 0); + assert(y & (0xffffffffffffffffff & 1) == 1); + } +} +// ---- +// Warning 6328: (181-194): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_3.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_3.sol index 617ae7af3..fdcfa3e14 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_3.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_3.sol @@ -10,7 +10,4 @@ contract C { } } // ---- -// Warning 8115: (71-74): Assertion checker does not yet support the type of this variable. -// Warning 7650: (117-120): Assertion checker does not yet support this expression. -// Warning 8364: (117-118): Assertion checker does not yet implement type struct C.S storage ref // Warning 9149: (117-125): Assertion checker does not yet implement this assignment operator. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_4.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_4.sol index 091f0ca0d..00e32d0d1 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_4.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_4.sol @@ -10,8 +10,4 @@ contract C { } } // ---- -// Warning 8115: (73-76): Assertion checker does not yet support the type of this variable. -// Warning 7650: (119-122): Assertion checker does not yet support this expression. -// Warning 8364: (119-120): Assertion checker does not yet implement type struct C.S storage ref -// Warning 9118: (119-125): Assertion checker does not yet implement this expression. // Warning 9149: (119-130): Assertion checker does not yet implement this assignment operator. diff --git a/test/libsolidity/smtCheckerTests/operators/delete_struct.sol b/test/libsolidity/smtCheckerTests/operators/delete_struct.sol index 5b7be5add..01fa7558b 100644 --- a/test/libsolidity/smtCheckerTests/operators/delete_struct.sol +++ b/test/libsolidity/smtCheckerTests/operators/delete_struct.sol @@ -6,7 +6,7 @@ contract C { uint x; } - function f(bool b) public { + function f(bool b) public pure { S memory s; s.x = 2; if (b) @@ -17,15 +17,3 @@ contract C } } // ---- -// Warning 2018: (73-192): Function state mutability can be restricted to pure -// Warning 6328: (172-188): Assertion violation happens here -// Warning 8115: (103-113): Assertion checker does not yet support the type of this variable. -// Warning 7650: (117-120): Assertion checker does not yet support this expression. -// Warning 8364: (117-118): Assertion checker does not yet implement type struct C.S memory -// Warning 8182: (117-124): Assertion checker does not yet implement such assignments. -// Warning 8364: (145-146): Assertion checker does not yet implement type struct C.S memory -// Warning 7650: (165-168): Assertion checker does not yet support this expression. -// Warning 8364: (165-166): Assertion checker does not yet implement type struct C.S memory -// Warning 2683: (158-168): Assertion checker does not yet implement "delete" for this expression. -// Warning 7650: (179-182): Assertion checker does not yet support this expression. -// Warning 8364: (179-180): Assertion checker does not yet implement type struct C.S memory diff --git a/test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol b/test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol new file mode 100644 index 000000000..3ddbe5390 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; + +contract C { + uint[] a; + function h() internal returns (uint[] storage) { + if (a[2] == 0) + a[2] = 3; + return a; + } + function g() public { + h()[2] = 4; + assert(h()[2] == 3); + } +} +// ---- +// Warning 6328: (191-210): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol b/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol index 513166872..1e2c354c9 100644 --- a/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol +++ b/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol @@ -8,7 +8,6 @@ contract C { } } // ---- -// Warning 8115: (151-159): Assertion checker does not yet support the type of this variable. // Warning 8364: (206-209): Assertion checker does not yet implement type abi // Warning 8364: (225-226): Assertion checker does not yet implement type type(struct C.S storage pointer) // Warning 8364: (235-241): Assertion checker does not yet implement type type(uint256[] memory) diff --git a/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_1.sol b/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_1.sol index f267f0b99..6b09f780d 100644 --- a/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_1.sol +++ b/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_1.sol @@ -26,4 +26,4 @@ contract C } } // ---- -// Warning 6328: (400-457): Assertion violation happens here. +// Warning 6328: (400-457): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/array_struct_array_branches_2d.sol b/test/libsolidity/smtCheckerTests/types/array_struct_array_branches_2d.sol index f7cb6f957..a4531079b 100644 --- a/test/libsolidity/smtCheckerTests/types/array_struct_array_branches_2d.sol +++ b/test/libsolidity/smtCheckerTests/types/array_struct_array_branches_2d.sol @@ -14,19 +14,3 @@ contract C } } // ---- -// Warning 6328: (202-226): Assertion violation happens here -// Warning 7650: (124-130): Assertion checker does not yet support this expression. -// Warning 8364: (124-128): Assertion checker does not yet implement type struct C.S memory -// Warning 9118: (124-133): Assertion checker does not yet implement this expression. -// Warning 9056: (124-136): Assertion checker does not yet implement this expression. -// Warning 7650: (154-160): Assertion checker does not yet support this expression. -// Warning 8364: (154-158): Assertion checker does not yet implement type struct C.S memory -// Warning 9118: (154-163): Assertion checker does not yet implement this expression. -// Warning 9056: (154-166): Assertion checker does not yet implement this expression. -// Warning 7650: (182-188): Assertion checker does not yet support this expression. -// Warning 8364: (182-186): Assertion checker does not yet implement type struct C.S memory -// Warning 9118: (182-191): Assertion checker does not yet implement this expression. -// Warning 9056: (182-194): Assertion checker does not yet implement this expression. -// Warning 7650: (209-215): Assertion checker does not yet support this expression. -// Warning 8364: (209-213): Assertion checker does not yet implement type struct C.S memory -// Warning 9118: (209-218): Assertion checker does not yet implement this expression. diff --git a/test/libsolidity/smtCheckerTests/types/enum_in_struct.sol b/test/libsolidity/smtCheckerTests/types/enum_in_struct.sol index 8c8636e59..ffe5dfd95 100644 --- a/test/libsolidity/smtCheckerTests/types/enum_in_struct.sol +++ b/test/libsolidity/smtCheckerTests/types/enum_in_struct.sol @@ -11,10 +11,3 @@ contract C } } // ---- -// Warning 6328: (187-208): Assertion violation happens here -// Warning 8115: (143-153): Assertion checker does not yet support the type of this variable. -// Warning 7650: (171-174): Assertion checker does not yet support this expression. -// Warning 8364: (171-172): Assertion checker does not yet implement type struct C.S memory -// Warning 8182: (171-183): Assertion checker does not yet implement such assignments. -// Warning 7650: (194-197): Assertion checker does not yet support this expression. -// Warning 8364: (194-195): Assertion checker does not yet implement type struct C.S memory diff --git a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol index 5348ca1b4..4cd0ddb66 100644 --- a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol +++ b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol @@ -13,6 +13,5 @@ contract C { } } // ---- -// Warning 9118: (238-244): Assertion checker does not yet implement this expression. // Warning 7989: (238-247): Assertion checker does not yet support index accessing fixed bytes. // Warning 7989: (251-257): Assertion checker does not yet support index accessing fixed bytes. diff --git a/test/libsolidity/smtCheckerTests/types/mapping_struct_assignment.sol b/test/libsolidity/smtCheckerTests/types/mapping_struct_assignment.sol index ec9ca8145..214c0930c 100644 --- a/test/libsolidity/smtCheckerTests/types/mapping_struct_assignment.sol +++ b/test/libsolidity/smtCheckerTests/types/mapping_struct_assignment.sol @@ -12,8 +12,5 @@ contract C } // ---- // Warning 6838: (140-144): Condition is always false. -// Warning 8364: (149-156): Assertion checker does not yet implement type struct C.S storage ref // Warning 8364: (159-160): Assertion checker does not yet implement type type(struct C.S storage pointer) -// Warning 8364: (159-163): Assertion checker does not yet implement type struct C.S memory // Warning 4639: (159-163): Assertion checker does not yet implement this expression. -// Warning 8364: (149-163): Assertion checker does not yet implement type struct C.S storage ref diff --git a/test/libsolidity/smtCheckerTests/types/no_effect_statements.sol b/test/libsolidity/smtCheckerTests/types/no_effect_statements.sol index 761b401c2..d97d33cbe 100644 --- a/test/libsolidity/smtCheckerTests/types/no_effect_statements.sol +++ b/test/libsolidity/smtCheckerTests/types/no_effect_statements.sol @@ -17,7 +17,6 @@ contract test { // Warning 6133: (156-163): Statement has no effect. // Warning 8364: (125-126): Assertion checker does not yet implement type type(struct test.s storage pointer) // Warning 8364: (130-131): Assertion checker does not yet implement type type(struct test.s storage pointer) -// Warning 8364: (130-136): Assertion checker does not yet implement type struct test.s memory // Warning 4639: (130-136): Assertion checker does not yet implement this expression. // Warning 8364: (140-141): Assertion checker does not yet implement type type(struct test.s storage pointer) // Warning 8364: (140-144): Assertion checker does not yet implement type type(struct test.s memory[7] memory) diff --git a/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_safe.sol b/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_safe.sol new file mode 100644 index 000000000..08cb807a2 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_safe.sol @@ -0,0 +1,30 @@ +pragma experimental SMTChecker; +pragma experimental ABIEncoderV2; + +contract C { + struct T { + uint y; + uint[] a; + } + struct S { + uint x; + T t; + uint[] a; + T[] ts; + } + function f() public pure { + S[] memory s1 = new S[](3); + s1[0].x = 2; + assert(s1[0].x == 2); + s1[1].t.y = 3; + assert(s1[1].t.y == 3); + s1[2].a[2] = 4; + assert(s1[2].a[2] == 4); + s1[0].ts[3].y = 5; + assert(s1[0].ts[3].y == 5); + s1[1].ts[4].a[5] = 6; + assert(s1[1].ts[4].a[5] == 6); + } +} +// ---- +// Warning 4588: (217-227): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_unsafe.sol b/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_unsafe.sol new file mode 100644 index 000000000..759538fd3 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_unsafe.sol @@ -0,0 +1,35 @@ +pragma experimental SMTChecker; +pragma experimental ABIEncoderV2; + +contract C { + struct T { + uint y; + uint[] a; + } + struct S { + uint x; + T t; + uint[] a; + T[] ts; + } + function f(S memory s2) public pure { + S[] memory s1 = new S[](3); + s1[0].x = 2; + assert(s1[0].x == s2.x); + s1[1].t.y = 3; + assert(s1[1].t.y == s2.t.y); + s1[2].a[2] = 4; + assert(s1[2].a[2] == s2.a[2]); + s1[0].ts[3].y = 5; + assert(s1[0].ts[3].y == s2.ts[3].y); + s1[1].ts[4].a[5] = 6; + assert(s1[1].ts[4].a[5] == s2.ts[4].a[5]); + } +} +// ---- +// Warning 6328: (257-280): Assertion violation happens here +// Warning 6328: (301-328): Assertion violation happens here +// Warning 6328: (350-379): Assertion violation happens here +// Warning 6328: (404-439): Assertion violation happens here +// Warning 6328: (467-508): Assertion violation happens here +// Warning 4588: (228-238): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_storage_safe.sol b/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_storage_safe.sol new file mode 100644 index 000000000..bfa45c90f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_storage_safe.sol @@ -0,0 +1,34 @@ +pragma experimental SMTChecker; +pragma experimental ABIEncoderV2; + +contract C { + struct T { + uint y; + uint[] a; + } + struct S { + uint x; + T t; + uint[] a; + T[] ts; + } + S[] s1; + function f() public { + s1.push(); + s1.push(); + s1.push(); + s1[0].x = 2; + assert(s1[0].x == 2); + s1[1].t.y = 3; + assert(s1[1].t.y == 3); + s1[2].a[2] = 4; + assert(s1[2].a[2] == 4); + s1[0].ts[3].y = 5; + assert(s1[0].ts[3].y == 5); + s1[1].ts[4].a[5] = 6; + assert(s1[1].ts[4].a[5] == 6); + s1.pop(); + s1.pop(); + s1.pop(); + } +} diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_memory.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_memory.sol new file mode 100644 index 000000000..d34abd154 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_memory.sol @@ -0,0 +1,23 @@ +pragma experimental SMTChecker; +pragma experimental ABIEncoderV2; + +contract C { + struct S { + uint x; + uint[] a; + } + function f(S memory s1, S memory s2, bool b) public pure { + S memory s3 = b ? s1 : s2; + assert(s3.x == s1.x); + assert(s3.x == s2.x); + // This is safe. + assert(s3.x == s1.x || s3.x == s2.x); + // This fails as false positive because of lack of support to aliasing. + s3.x = 42; + assert(s3.x == s1.x || s3.x == s2.x); + } +} +// ---- +// Warning 6328: (208-228): Assertion violation happens here +// Warning 6328: (232-252): Assertion violation happens here +// Warning 6328: (402-438): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_storage.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_storage.sol new file mode 100644 index 000000000..2e03f04c0 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_storage.sol @@ -0,0 +1,30 @@ +pragma experimental SMTChecker; + +contract C { + struct S { + uint x; + uint[] a; + } + S s1; + S s2; + function f(bool b) public { + S storage s3 = b ? s1 : s2; + assert(s3.x == s1.x); + assert(s3.x == s2.x); + // This is safe. + assert(s3.x == s1.x || s3.x == s2.x); + // This fails as false positive because of lack of support to aliasing. + s3.x = 42; + assert(s3.x == s1.x || s3.x == s2.x); + } + function g(bool b, uint _x) public { + if (b) + s1.x = _x; + else + s2.x = _x; + } +} +// ---- +// Warning 6328: (158-178): Assertion violation happens here +// Warning 6328: (182-202): Assertion violation happens here +// Warning 6328: (352-388): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_safe.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_safe.sol new file mode 100644 index 000000000..ed8d97905 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_safe.sol @@ -0,0 +1,28 @@ +pragma experimental SMTChecker; +pragma experimental ABIEncoderV2; + +contract C { + struct T { + uint y; + uint[] a; + } + struct S { + uint x; + T t; + uint[] a; + T[] ts; + } + function f() public pure { + S memory s1; + s1.x = 2; + assert(s1.x == 2); + s1.t.y = 3; + assert(s1.t.y == 3); + s1.a[2] = 4; + assert(s1.a[2] == 4); + s1.ts[3].y = 5; + assert(s1.ts[3].y == 5); + s1.ts[4].a[5] = 6; + assert(s1.ts[4].a[5] == 6); + } +} diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_1.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_1.sol new file mode 100644 index 000000000..88dac27ac --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_1.sol @@ -0,0 +1,34 @@ +pragma experimental SMTChecker; +pragma experimental ABIEncoderV2; + +contract C { + struct T { + uint y; + uint[] a; + } + struct S { + uint x; + T t; + uint[] a; + T[] ts; + } + function f() public pure { + S memory s1; + s1.x = 2; + assert(s1.x != 2); + s1.t.y = 3; + assert(s1.t.y != 3); + s1.a[2] = 4; + assert(s1.a[2] != 4); + s1.ts[3].y = 5; + assert(s1.ts[3].y != 5); + s1.ts[4].a[5] = 6; + assert(s1.ts[4].a[5] != 6); + } +} +// ---- +// Warning 6328: (228-245): Assertion violation happens here +// Warning 6328: (263-282): Assertion violation happens here +// Warning 6328: (301-321): Assertion violation happens here +// Warning 6328: (343-366): Assertion violation happens here +// Warning 6328: (391-417): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_2.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_2.sol new file mode 100644 index 000000000..4524d55d5 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_2.sol @@ -0,0 +1,34 @@ +pragma experimental SMTChecker; +pragma experimental ABIEncoderV2; + +contract C { + struct T { + uint y; + uint[] a; + } + struct S { + uint x; + T t; + uint[] a; + T[] ts; + } + function f(S memory s2) public pure { + S memory s1; + s1.x = 2; + assert(s1.x == s2.x); + s1.t.y = 3; + assert(s1.t.y == s2.t.y); + s1.a[2] = 4; + assert(s1.a[2] == s2.a[2]); + s1.ts[3].y = 5; + assert(s1.ts[3].y == s2.ts[3].y); + s1.ts[4].a[5] = 6; + assert(s1.ts[4].a[5] == s2.ts[4].a[5]); + } +} +// ---- +// Warning 6328: (239-259): Assertion violation happens here +// Warning 6328: (277-301): Assertion violation happens here +// Warning 6328: (320-346): Assertion violation happens here +// Warning 6328: (368-400): Assertion violation happens here +// Warning 6328: (425-463): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_safe.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_safe.sol new file mode 100644 index 000000000..4240f6267 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_safe.sol @@ -0,0 +1,27 @@ +pragma experimental SMTChecker; + +contract C { + struct T { + uint y; + uint[] a; + } + struct S { + uint x; + T t; + uint[] a; + T[] ts; + } + S s1; + function f() public { + s1.x = 2; + assert(s1.x == 2); + s1.t.y = 3; + assert(s1.t.y == 3); + s1.a[2] = 4; + assert(s1.a[2] == 4); + s1.ts[3].y = 5; + assert(s1.ts[3].y == 5); + s1.ts[4].a[5] = 6; + assert(s1.ts[4].a[5] == 6); + } +} diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_unsafe_1.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_unsafe_1.sol new file mode 100644 index 000000000..a09f9caff --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_unsafe_1.sol @@ -0,0 +1,33 @@ +pragma experimental SMTChecker; + +contract C { + struct T { + uint y; + uint[] a; + } + struct S { + uint x; + T t; + uint[] a; + T[] ts; + } + S s1; + function f() public { + s1.x = 2; + assert(s1.x != 2); + s1.t.y = 3; + assert(s1.t.y != 3); + s1.a[2] = 4; + assert(s1.a[2] != 4); + s1.ts[3].y = 5; + assert(s1.ts[3].y != 5); + s1.ts[4].a[5] = 6; + assert(s1.ts[4].a[5] != 6); + } +} +// ---- +// Warning 6328: (181-198): Assertion violation happens here +// Warning 6328: (216-235): Assertion violation happens here +// Warning 6328: (254-274): Assertion violation happens here +// Warning 6328: (296-319): Assertion violation happens here +// Warning 6328: (344-370): Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_delete_memory.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_delete_memory.sol new file mode 100644 index 000000000..2c169e587 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_delete_memory.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; +pragma experimental ABIEncoderV2; + +contract C { + struct S { + uint x; + uint[] a; + } + function f(S memory s1, S memory s2) public pure { + delete s1; + assert(s1.x == s2.x); + assert(s1.a.length == s2.a.length); + assert(s1.a.length == 0); + } +} +// ---- +// Warning 6328: (184-204): Assertion violation happens here +// Warning 6328: (208-242): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_delete_storage.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_delete_storage.sol new file mode 100644 index 000000000..560a6a298 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_delete_storage.sol @@ -0,0 +1,23 @@ +pragma experimental SMTChecker; +pragma experimental ABIEncoderV2; + +contract C { + struct S { + uint x; + uint[] a; + } + S s1; + function g(S memory s2) public { + s1.x = s2.x; + s1.a = s2.a; + } + function f(S memory s2) public { + delete s1; + assert(s1.x == s2.x); + assert(s1.a.length == s2.a.length); + assert(s1.a.length == 0); + } +} +// ---- +// Warning 6328: (240-260): Assertion violation happens here +// Warning 6328: (264-298): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_mapping.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_mapping.sol new file mode 100644 index 000000000..55a2df245 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_mapping.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; + +contract C { + struct S { + uint x; + mapping (uint => uint) m; + } + S s1; + S s2; + function f() public view { + assert(s1.m[0] == s2.m[0]); + } + function g(uint a, uint b) public { + s1.m[a] = b; + } +} +// ---- +// Warning 4661: (143-169): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_1.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_1.sol new file mode 100644 index 000000000..a862dc0fc --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_1.sol @@ -0,0 +1,27 @@ +pragma experimental SMTChecker; + +contract C { + struct S { + uint x; + S[] a; + } + S s1; + S s2; + function f() public view { + assert(s1.x == s2.x); + assert(s1.a.length == s2.a.length); + } +} +// ---- +// Warning 6328: (124-144): Assertion violation happens here +// Warning 6328: (148-182): Assertion violation happens here +// Warning 8115: (81-85): Assertion checker does not yet support the type of this variable. +// Warning 8115: (88-92): Assertion checker does not yet support the type of this variable. +// Warning 7650: (131-135): Assertion checker does not yet support this expression. +// Warning 8364: (131-133): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (139-143): Assertion checker does not yet support this expression. +// Warning 8364: (139-141): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (155-159): Assertion checker does not yet support this expression. +// Warning 8364: (155-157): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (170-174): Assertion checker does not yet support this expression. +// Warning 8364: (170-172): Assertion checker does not yet implement type struct C.S storage ref diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_2.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_2.sol new file mode 100644 index 000000000..33f35d0ac --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_2.sol @@ -0,0 +1,69 @@ +pragma experimental SMTChecker; + +contract C { + struct S { + uint x; + S[] a; + } + S s1; + S s2; + function f() public view { + assert(s1.x == s2.x); + assert(s1.a.length == s2.a.length); + assert(s1.a[0].x == s2.a[0].x); + } + function g() public { + s1.x = 42; + s2.x = 42; + s1.a.push(); + s2.a.push(); + s1.a[0].x = 43; + s2.a[0].x = 43; + } +} +// ---- +// Warning 6328: (124-144): Assertion violation happens here +// Warning 6328: (148-182): Assertion violation happens here +// Warning 6328: (186-216): Assertion violation happens here +// Warning 8115: (81-85): Assertion checker does not yet support the type of this variable. +// Warning 8115: (88-92): Assertion checker does not yet support the type of this variable. +// Warning 7650: (131-135): Assertion checker does not yet support this expression. +// Warning 8364: (131-133): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (139-143): Assertion checker does not yet support this expression. +// Warning 8364: (139-141): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (155-159): Assertion checker does not yet support this expression. +// Warning 8364: (155-157): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (170-174): Assertion checker does not yet support this expression. +// Warning 8364: (170-172): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (193-202): Assertion checker does not yet support this expression. +// Warning 7650: (193-197): Assertion checker does not yet support this expression. +// Warning 8364: (193-195): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (193-200): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (206-215): Assertion checker does not yet support this expression. +// Warning 7650: (206-210): Assertion checker does not yet support this expression. +// Warning 8364: (206-208): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (206-213): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (246-250): Assertion checker does not yet support this expression. +// Warning 8364: (246-248): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (246-250): Assertion checker does not support recursive structs. +// Warning 7650: (259-263): Assertion checker does not yet support this expression. +// Warning 8364: (259-261): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (259-263): Assertion checker does not support recursive structs. +// Warning 7650: (272-276): Assertion checker does not yet support this expression. +// Warning 8364: (272-274): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (272-283): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (272-276): Assertion checker does not support recursive structs. +// Warning 7650: (287-291): Assertion checker does not yet support this expression. +// Warning 8364: (287-289): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (287-298): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (287-291): Assertion checker does not support recursive structs. +// Warning 7650: (302-311): Assertion checker does not yet support this expression. +// Warning 7650: (302-306): Assertion checker does not yet support this expression. +// Warning 8364: (302-304): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (302-309): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (302-311): Assertion checker does not support recursive structs. +// Warning 7650: (320-329): Assertion checker does not yet support this expression. +// Warning 7650: (320-324): Assertion checker does not yet support this expression. +// Warning 8364: (320-322): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (320-327): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (320-329): Assertion checker does not support recursive structs. diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_3.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_3.sol new file mode 100644 index 000000000..a3f859b71 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_3.sol @@ -0,0 +1,123 @@ +pragma experimental SMTChecker; + +contract C { + struct S { + uint x; + S[] a; + } + S s1; + S s2; + function f() public view { + assert(s1.x == s2.x); + assert(s1.a.length == s2.a.length); + assert(s1.a[0].x == s2.a[0].x); + assert(s1.a[0].a.length == s2.a[0].a.length); + assert(s1.a[0].a[0].x == s2.a[0].a[0].x); + } + function g() public { + s1.x = 42; + s2.x = 42; + s1.a.push(); + s2.a.push(); + s1.a[0].x = 43; + s2.a[0].x = 43; + s1.a[0].a.push(); + s2.a[0].a.push(); + s1.a[0].a[0].x = 44; + s2.a[0].a[0].x = 44; + } +} +// ---- +// Warning 6328: (124-144): Assertion violation happens here +// Warning 6328: (148-182): Assertion violation happens here +// Warning 6328: (186-216): Assertion violation happens here +// Warning 6328: (220-264): Assertion violation happens here +// Warning 6328: (268-308): Assertion violation happens here +// Warning 8115: (81-85): Assertion checker does not yet support the type of this variable. +// Warning 8115: (88-92): Assertion checker does not yet support the type of this variable. +// Warning 7650: (131-135): Assertion checker does not yet support this expression. +// Warning 8364: (131-133): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (139-143): Assertion checker does not yet support this expression. +// Warning 8364: (139-141): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (155-159): Assertion checker does not yet support this expression. +// Warning 8364: (155-157): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (170-174): Assertion checker does not yet support this expression. +// Warning 8364: (170-172): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (193-202): Assertion checker does not yet support this expression. +// Warning 7650: (193-197): Assertion checker does not yet support this expression. +// Warning 8364: (193-195): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (193-200): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (206-215): Assertion checker does not yet support this expression. +// Warning 7650: (206-210): Assertion checker does not yet support this expression. +// Warning 8364: (206-208): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (206-213): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (227-236): Assertion checker does not yet support this expression. +// Warning 7650: (227-231): Assertion checker does not yet support this expression. +// Warning 8364: (227-229): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (227-234): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (247-256): Assertion checker does not yet support this expression. +// Warning 7650: (247-251): Assertion checker does not yet support this expression. +// Warning 8364: (247-249): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (247-254): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (275-289): Assertion checker does not yet support this expression. +// Warning 7650: (275-284): Assertion checker does not yet support this expression. +// Warning 7650: (275-279): Assertion checker does not yet support this expression. +// Warning 8364: (275-277): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (275-282): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (275-287): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (293-307): Assertion checker does not yet support this expression. +// Warning 7650: (293-302): Assertion checker does not yet support this expression. +// Warning 7650: (293-297): Assertion checker does not yet support this expression. +// Warning 8364: (293-295): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (293-300): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (293-305): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (338-342): Assertion checker does not yet support this expression. +// Warning 8364: (338-340): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (338-342): Assertion checker does not support recursive structs. +// Warning 7650: (351-355): Assertion checker does not yet support this expression. +// Warning 8364: (351-353): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (351-355): Assertion checker does not support recursive structs. +// Warning 7650: (364-368): Assertion checker does not yet support this expression. +// Warning 8364: (364-366): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (364-375): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (364-368): Assertion checker does not support recursive structs. +// Warning 7650: (379-383): Assertion checker does not yet support this expression. +// Warning 8364: (379-381): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (379-390): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (379-383): Assertion checker does not support recursive structs. +// Warning 7650: (394-403): Assertion checker does not yet support this expression. +// Warning 7650: (394-398): Assertion checker does not yet support this expression. +// Warning 8364: (394-396): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (394-401): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (394-403): Assertion checker does not support recursive structs. +// Warning 7650: (412-421): Assertion checker does not yet support this expression. +// Warning 7650: (412-416): Assertion checker does not yet support this expression. +// Warning 8364: (412-414): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (412-419): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (412-421): Assertion checker does not support recursive structs. +// Warning 7650: (430-439): Assertion checker does not yet support this expression. +// Warning 7650: (430-434): Assertion checker does not yet support this expression. +// Warning 8364: (430-432): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (430-437): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (430-446): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (430-439): Assertion checker does not support recursive structs. +// Warning 7650: (450-459): Assertion checker does not yet support this expression. +// Warning 7650: (450-454): Assertion checker does not yet support this expression. +// Warning 8364: (450-452): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (450-457): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (450-466): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (450-459): Assertion checker does not support recursive structs. +// Warning 7650: (470-484): Assertion checker does not yet support this expression. +// Warning 7650: (470-479): Assertion checker does not yet support this expression. +// Warning 7650: (470-474): Assertion checker does not yet support this expression. +// Warning 8364: (470-472): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (470-477): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (470-482): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (470-484): Assertion checker does not support recursive structs. +// Warning 7650: (493-507): Assertion checker does not yet support this expression. +// Warning 7650: (493-502): Assertion checker does not yet support this expression. +// Warning 7650: (493-497): Assertion checker does not yet support this expression. +// Warning 8364: (493-495): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (493-500): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (493-505): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (493-507): Assertion checker does not support recursive structs. diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_4.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_4.sol new file mode 100644 index 000000000..9e627ebce --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_4.sol @@ -0,0 +1,56 @@ +pragma experimental SMTChecker; + +contract C { + struct S { + uint x; + S[] a; + } + S s1; + S s2; + function f(bool b1, bool b2) public { + S storage s3 = b1 ? s1 : s2; + S storage s4 = b2 ? s1 : s2; + assert(s3.x == s1.x || s3.x == s2.x); + assert(s4.x == s1.x || s4.x == s2.x); + s3.x = 44; + // Fails as false positive because of lack of support to aliasing. + assert(s1.x == 44 || s2.x == 44); + } +} +// ---- +// Warning 6328: (197-233): Assertion violation happens here +// Warning 6328: (237-273): Assertion violation happens here +// Warning 6328: (359-391): Assertion violation happens here +// Warning 8115: (81-85): Assertion checker does not yet support the type of this variable. +// Warning 8115: (88-92): Assertion checker does not yet support the type of this variable. +// Warning 8115: (135-147): Assertion checker does not yet support the type of this variable. +// Warning 8115: (166-178): Assertion checker does not yet support the type of this variable. +// Warning 8364: (155-157): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (160-162): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (150-162): Assertion checker does not yet implement type struct C.S storage pointer +// Warning 8364: (186-188): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (191-193): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (181-193): Assertion checker does not yet implement type struct C.S storage pointer +// Warning 7650: (204-208): Assertion checker does not yet support this expression. +// Warning 8364: (204-206): Assertion checker does not yet implement type struct C.S storage pointer +// Warning 7650: (212-216): Assertion checker does not yet support this expression. +// Warning 8364: (212-214): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (220-224): Assertion checker does not yet support this expression. +// Warning 8364: (220-222): Assertion checker does not yet implement type struct C.S storage pointer +// Warning 7650: (228-232): Assertion checker does not yet support this expression. +// Warning 8364: (228-230): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (244-248): Assertion checker does not yet support this expression. +// Warning 8364: (244-246): Assertion checker does not yet implement type struct C.S storage pointer +// Warning 7650: (252-256): Assertion checker does not yet support this expression. +// Warning 8364: (252-254): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (260-264): Assertion checker does not yet support this expression. +// Warning 8364: (260-262): Assertion checker does not yet implement type struct C.S storage pointer +// Warning 7650: (268-272): Assertion checker does not yet support this expression. +// Warning 8364: (268-270): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (277-281): Assertion checker does not yet support this expression. +// Warning 8364: (277-279): Assertion checker does not yet implement type struct C.S storage pointer +// Warning 4375: (277-281): Assertion checker does not support recursive structs. +// Warning 7650: (366-370): Assertion checker does not yet support this expression. +// Warning 8364: (366-368): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (380-384): Assertion checker does not yet support this expression. +// Warning 8364: (380-382): Assertion checker does not yet implement type struct C.S storage ref diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_5.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_5.sol new file mode 100644 index 000000000..079066bbb --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_5.sol @@ -0,0 +1,29 @@ +pragma experimental SMTChecker; + +contract C { + struct S { + uint x; + S[] a; + } + S[] sa; + S[][] sa2; + function f() public { + sa.push(); + sa2.push(); + sa2[0].push(); + sa2[0][0].a.push(); + assert(sa2[0][0].a.length == sa[0].a.length); + } +} +// ---- +// Warning 6328: (192-236): Assertion violation happens here +// Warning 8364: (126-135): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (153-166): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (170-181): Assertion checker does not yet support this expression. +// Warning 8364: (170-179): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (170-188): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (170-181): Assertion checker does not support recursive structs. +// Warning 7650: (199-210): Assertion checker does not yet support this expression. +// Warning 8364: (199-208): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (221-228): Assertion checker does not yet support this expression. +// Warning 8364: (221-226): Assertion checker does not yet implement type struct C.S storage ref diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_6.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_6.sol new file mode 100644 index 000000000..961dd1562 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_6.sol @@ -0,0 +1,66 @@ +pragma experimental SMTChecker; + +contract C { + struct S { + uint x; + S[] a; + } + S s1; + S s2; + function f() public { + s1.x = 10; + ++s1.x; + s1.x++; + s2.x = 20; + --s2.x; + s2.x--; + assert(s1.x == s2.x + 6); + assert(s1.a.length == s2.a.length); + delete s1; + assert(s1.x == 0); + } +} +// ---- +// Warning 4984: (200-208): Overflow (resulting value larger than 2**256 - 1) happens here +// Warning 6328: (185-209): Assertion violation happens here +// Warning 6328: (213-247): Assertion violation happens here +// Warning 6328: (264-281): Assertion violation happens here +// Warning 8115: (81-85): Assertion checker does not yet support the type of this variable. +// Warning 8115: (88-92): Assertion checker does not yet support the type of this variable. +// Warning 7650: (119-123): Assertion checker does not yet support this expression. +// Warning 8364: (119-121): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (119-123): Assertion checker does not support recursive structs. +// Warning 7650: (134-138): Assertion checker does not yet support this expression. +// Warning 8364: (134-136): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (134-138): Assertion checker does not support recursive structs. +// Warning 7650: (142-146): Assertion checker does not yet support this expression. +// Warning 8364: (142-144): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (142-146): Assertion checker does not support recursive structs. +// Warning 7650: (152-156): Assertion checker does not yet support this expression. +// Warning 8364: (152-154): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (152-156): Assertion checker does not support recursive structs. +// Warning 7650: (167-171): Assertion checker does not yet support this expression. +// Warning 8364: (167-169): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (167-171): Assertion checker does not support recursive structs. +// Warning 7650: (175-179): Assertion checker does not yet support this expression. +// Warning 8364: (175-177): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (175-179): Assertion checker does not support recursive structs. +// Warning 7650: (192-196): Assertion checker does not yet support this expression. +// Warning 8364: (192-194): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (200-204): Assertion checker does not yet support this expression. +// Warning 8364: (200-202): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (220-224): Assertion checker does not yet support this expression. +// Warning 8364: (220-222): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (235-239): Assertion checker does not yet support this expression. +// Warning 8364: (235-237): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (258-260): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (271-275): Assertion checker does not yet support this expression. +// Warning 8364: (271-273): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4144: (132-138): Underflow (resulting value less than 0) happens here +// Warning 2661: (132-138): Overflow (resulting value larger than 2**256 - 1) happens here +// Warning 4144: (142-148): Underflow (resulting value less than 0) happens here +// Warning 2661: (142-148): Overflow (resulting value larger than 2**256 - 1) happens here +// Warning 4144: (165-171): Underflow (resulting value less than 0) happens here +// Warning 2661: (165-171): Overflow (resulting value larger than 2**256 - 1) happens here +// Warning 4144: (175-181): Underflow (resulting value less than 0) happens here +// Warning 2661: (175-181): Overflow (resulting value larger than 2**256 - 1) happens here diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_indirect_1.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_indirect_1.sol new file mode 100644 index 000000000..e157edca2 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_indirect_1.sol @@ -0,0 +1,31 @@ +pragma experimental SMTChecker; + +contract C { + struct S { + uint x; + T[] a; + } + struct T { + uint y; + S[] a; + } + S s1; + S s2; + function f() public view { + assert(s1.x == s2.x); + assert(s1.a.length == s2.a.length); + } +} +// ---- +// Warning 6328: (158-178): Assertion violation happens here +// Warning 6328: (182-216): Assertion violation happens here +// Warning 8115: (115-119): Assertion checker does not yet support the type of this variable. +// Warning 8115: (122-126): Assertion checker does not yet support the type of this variable. +// Warning 7650: (165-169): Assertion checker does not yet support this expression. +// Warning 8364: (165-167): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (173-177): Assertion checker does not yet support this expression. +// Warning 8364: (173-175): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (189-193): Assertion checker does not yet support this expression. +// Warning 8364: (189-191): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (204-208): Assertion checker does not yet support this expression. +// Warning 8364: (204-206): Assertion checker does not yet implement type struct C.S storage ref diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_indirect_2.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_indirect_2.sol new file mode 100644 index 000000000..2d8d9660d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_indirect_2.sol @@ -0,0 +1,57 @@ +pragma experimental SMTChecker; + +contract C { + struct S { + uint x; + T[] a; + } + struct T { + uint y; + S[] a; + } + S s1; + S s2; + function f() public { + s1.a.push(); + s2.a.push(); + s1.a[0].a.push(); + s2.a[0].a.push(); + assert(s1.a[0].a[0].x == s2.a[0].a[0].x); + } +} +// ---- +// Warning 6328: (223-263): Assertion violation happens here +// Warning 8115: (115-119): Assertion checker does not yet support the type of this variable. +// Warning 8115: (122-126): Assertion checker does not yet support the type of this variable. +// Warning 7650: (153-157): Assertion checker does not yet support this expression. +// Warning 8364: (153-155): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (153-164): Assertion checker does not yet implement type struct C.T storage ref +// Warning 4375: (153-157): Assertion checker does not support recursive structs. +// Warning 7650: (168-172): Assertion checker does not yet support this expression. +// Warning 8364: (168-170): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (168-179): Assertion checker does not yet implement type struct C.T storage ref +// Warning 4375: (168-172): Assertion checker does not support recursive structs. +// Warning 7650: (183-192): Assertion checker does not yet support this expression. +// Warning 7650: (183-187): Assertion checker does not yet support this expression. +// Warning 8364: (183-185): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (183-190): Assertion checker does not yet implement type struct C.T storage ref +// Warning 8364: (183-199): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (183-192): Assertion checker does not support recursive structs. +// Warning 7650: (203-212): Assertion checker does not yet support this expression. +// Warning 7650: (203-207): Assertion checker does not yet support this expression. +// Warning 8364: (203-205): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (203-210): Assertion checker does not yet implement type struct C.T storage ref +// Warning 8364: (203-219): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (203-212): Assertion checker does not support recursive structs. +// Warning 7650: (230-244): Assertion checker does not yet support this expression. +// Warning 7650: (230-239): Assertion checker does not yet support this expression. +// Warning 7650: (230-234): Assertion checker does not yet support this expression. +// Warning 8364: (230-232): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (230-237): Assertion checker does not yet implement type struct C.T storage ref +// Warning 8364: (230-242): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (248-262): Assertion checker does not yet support this expression. +// Warning 7650: (248-257): Assertion checker does not yet support this expression. +// Warning 7650: (248-252): Assertion checker does not yet support this expression. +// Warning 8364: (248-250): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (248-255): Assertion checker does not yet implement type struct C.T storage ref +// Warning 8364: (248-260): Assertion checker does not yet implement type struct C.S storage ref diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_return.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_return.sol new file mode 100644 index 000000000..c7b7a5d5c --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_return.sol @@ -0,0 +1,20 @@ +pragma experimental SMTChecker; + +contract C { + struct S { + uint x; + uint[] a; + } + function s() internal pure returns (S memory s1) { + s1.x = 42; + s1.a[2] = 43; + } + function f() public pure { + S memory s2 = s(); + assert(s2.x == 42); + assert(s2.a[2] == 43); + assert(s2.a[3] == 43); + } +} +// ---- +// Warning 6328: (265-286): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_state_var.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_state_var.sol new file mode 100644 index 000000000..878d1e372 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_state_var.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; + +contract C { + struct S { + uint x; + uint[] a; + } + S s; + function f(uint _x) public { + s.x = _x; + s.a[0] = _x; + assert(s.a[1] == s.a[0]); + } +} +// ---- +// Warning 6328: (148-172): Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_state_var_array_pop_1.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_state_var_array_pop_1.sol new file mode 100644 index 000000000..7d2a34855 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_state_var_array_pop_1.sol @@ -0,0 +1,25 @@ +pragma experimental SMTChecker; + +contract C { + struct S { + uint x; + uint[] a; + } + S s; + function f(uint _x) public { + s.a.pop(); + s.a.length; + s.a.push(); + s.x = _x; + s.a.pop(); + s.a.push(); + s.a.push(); + s.a[0] = _x; + assert(s.a[1] == s.a[0]); + s.a.pop(); + s.a.pop(); + } +} +// ---- +// Warning 2529: (121-130): Empty array "pop" detected here +// Warning 6328: (230-254): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_state_var_array_pop_2.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_state_var_array_pop_2.sol new file mode 100644 index 000000000..c0cd9daa2 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_state_var_array_pop_2.sol @@ -0,0 +1,22 @@ +pragma experimental SMTChecker; + +contract C { + struct S { + uint x; + uint[] a; + } + S s; + function f(uint _x) public { + s.x = _x; + s.a.pop(); + s.a.push(); + s.a.push(); + s.a[0] = _x; + assert(s.a[1] == s.a[0]); + s.a.pop(); + s.a.pop(); + } +} +// ---- +// Warning 2529: (133-142): Empty array "pop" detected here. +// Warning 6328: (189-213): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_unary_add.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_unary_add.sol new file mode 100644 index 000000000..ef9344861 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_unary_add.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; +pragma experimental ABIEncoderV2; + +contract C { + struct S { + uint x; + uint[] a; + } + function f(S memory s1, S memory s2) public pure { + delete s1; + s1.x++; + ++s1.x; + assert(s1.x == 2); + assert(s1.x == s2.x); + } +} +// ---- +// Warning 6328: (225-245): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_unary_sub.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_unary_sub.sol new file mode 100644 index 000000000..265a0b6a2 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_unary_sub.sol @@ -0,0 +1,19 @@ +pragma experimental SMTChecker; +pragma experimental ABIEncoderV2; + +contract C { + struct S { + uint x; + uint[] a; + } + function f(S memory s1, S memory s2) public pure { + delete s1; + s1.x = 100; + s1.x--; + --s1.x; + assert(s1.x == 98); + assert(s1.x == s2.x); + } +} +// ---- +// Warning 6328: (240-260): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/struct_1.sol b/test/libsolidity/smtCheckerTests/types/struct_1.sol index e58d5c18f..99dc2b149 100644 --- a/test/libsolidity/smtCheckerTests/types/struct_1.sol +++ b/test/libsolidity/smtCheckerTests/types/struct_1.sol @@ -15,12 +15,7 @@ contract C } // ---- // Warning 2072: (157-170): Unused local variable. -// Warning 8115: (157-170): Assertion checker does not yet support the type of this variable. -// Warning 8364: (139-146): Assertion checker does not yet implement type struct C.S storage ref // Warning 8364: (149-150): Assertion checker does not yet implement type type(struct C.S storage pointer) -// Warning 8364: (149-153): Assertion checker does not yet implement type struct C.S memory // Warning 4639: (149-153): Assertion checker does not yet implement this expression. -// Warning 8364: (139-153): Assertion checker does not yet implement type struct C.S storage ref // Warning 8364: (173-174): Assertion checker does not yet implement type type(struct C.S storage pointer) -// Warning 8364: (173-177): Assertion checker does not yet implement type struct C.S memory // Warning 4639: (173-177): Assertion checker does not yet implement this expression. diff --git a/test/libsolidity/smtCheckerTests/types/struct_array_branches_1d.sol b/test/libsolidity/smtCheckerTests/types/struct_array_branches_1d.sol index 7d5752c2b..96f8b1b7e 100644 --- a/test/libsolidity/smtCheckerTests/types/struct_array_branches_1d.sol +++ b/test/libsolidity/smtCheckerTests/types/struct_array_branches_1d.sol @@ -3,7 +3,7 @@ pragma experimental SMTChecker; contract C { struct S { uint[] a; } - function f(bool b) public { + function f(bool b) public pure { S memory c; c.a[0] = 0; if (b) @@ -14,21 +14,3 @@ contract C } } // ---- -// Warning 2018: (71-197): Function state mutability can be restricted to pure -// Warning 6328: (175-193): Assertion violation happens here -// Warning 8115: (101-111): Assertion checker does not yet support the type of this variable. -// Warning 7650: (115-118): Assertion checker does not yet support this expression. -// Warning 8364: (115-116): Assertion checker does not yet implement type struct C.S memory -// Warning 9118: (115-121): Assertion checker does not yet implement this expression. -// Warning 9056: (115-121): Assertion checker does not yet implement this expression. -// Warning 7650: (139-142): Assertion checker does not yet support this expression. -// Warning 8364: (139-140): Assertion checker does not yet implement type struct C.S memory -// Warning 9118: (139-145): Assertion checker does not yet implement this expression. -// Warning 9056: (139-145): Assertion checker does not yet implement this expression. -// Warning 7650: (161-164): Assertion checker does not yet support this expression. -// Warning 8364: (161-162): Assertion checker does not yet implement type struct C.S memory -// Warning 9118: (161-167): Assertion checker does not yet implement this expression. -// Warning 9056: (161-167): Assertion checker does not yet implement this expression. -// Warning 7650: (182-185): Assertion checker does not yet support this expression. -// Warning 8364: (182-183): Assertion checker does not yet implement type struct C.S memory -// Warning 9118: (182-188): Assertion checker does not yet implement this expression. diff --git a/test/libsolidity/smtCheckerTests/types/struct_array_branches_2d.sol b/test/libsolidity/smtCheckerTests/types/struct_array_branches_2d.sol index d5fa12ed4..a1ceb4e80 100644 --- a/test/libsolidity/smtCheckerTests/types/struct_array_branches_2d.sol +++ b/test/libsolidity/smtCheckerTests/types/struct_array_branches_2d.sol @@ -3,7 +3,7 @@ pragma experimental SMTChecker; contract C { struct S { uint[][] a; } - function f(bool b) public { + function f(bool b) public pure { S memory c; c.a[0][0] = 0; if (b) @@ -14,21 +14,3 @@ contract C } } // ---- -// Warning 2018: (73-211): Function state mutability can be restricted to pure -// Warning 6328: (186-207): Assertion violation happens here -// Warning 8115: (103-113): Assertion checker does not yet support the type of this variable. -// Warning 7650: (117-120): Assertion checker does not yet support this expression. -// Warning 8364: (117-118): Assertion checker does not yet implement type struct C.S memory -// Warning 9118: (117-123): Assertion checker does not yet implement this expression. -// Warning 9056: (117-126): Assertion checker does not yet implement this expression. -// Warning 7650: (144-147): Assertion checker does not yet support this expression. -// Warning 8364: (144-145): Assertion checker does not yet implement type struct C.S memory -// Warning 9118: (144-150): Assertion checker does not yet implement this expression. -// Warning 9056: (144-153): Assertion checker does not yet implement this expression. -// Warning 7650: (169-172): Assertion checker does not yet support this expression. -// Warning 8364: (169-170): Assertion checker does not yet implement type struct C.S memory -// Warning 9118: (169-175): Assertion checker does not yet implement this expression. -// Warning 9056: (169-178): Assertion checker does not yet implement this expression. -// Warning 7650: (193-196): Assertion checker does not yet support this expression. -// Warning 8364: (193-194): Assertion checker does not yet implement type struct C.S memory -// Warning 9118: (193-199): Assertion checker does not yet implement this expression. diff --git a/test/libsolidity/smtCheckerTests/types/struct_array_branches_3d.sol b/test/libsolidity/smtCheckerTests/types/struct_array_branches_3d.sol index 16b5fef4e..d23a95463 100644 --- a/test/libsolidity/smtCheckerTests/types/struct_array_branches_3d.sol +++ b/test/libsolidity/smtCheckerTests/types/struct_array_branches_3d.sol @@ -14,20 +14,3 @@ contract C } } // ---- -// Warning 6328: (202-226): Assertion violation happens here -// Warning 8115: (110-120): Assertion checker does not yet support the type of this variable. -// Warning 7650: (124-127): Assertion checker does not yet support this expression. -// Warning 8364: (124-125): Assertion checker does not yet implement type struct C.S memory -// Warning 9118: (124-130): Assertion checker does not yet implement this expression. -// Warning 9056: (124-136): Assertion checker does not yet implement this expression. -// Warning 7650: (154-157): Assertion checker does not yet support this expression. -// Warning 8364: (154-155): Assertion checker does not yet implement type struct C.S memory -// Warning 9118: (154-160): Assertion checker does not yet implement this expression. -// Warning 9056: (154-166): Assertion checker does not yet implement this expression. -// Warning 7650: (182-185): Assertion checker does not yet support this expression. -// Warning 8364: (182-183): Assertion checker does not yet implement type struct C.S memory -// Warning 9118: (182-188): Assertion checker does not yet implement this expression. -// Warning 9056: (182-194): Assertion checker does not yet implement this expression. -// Warning 7650: (209-212): Assertion checker does not yet support this expression. -// Warning 8364: (209-210): Assertion checker does not yet implement type struct C.S memory -// Warning 9118: (209-215): Assertion checker does not yet implement this expression. diff --git a/test/libsolidity/smtCheckerTests/types/tuple_return_branch.sol b/test/libsolidity/smtCheckerTests/types/tuple_return_branch.sol index 1489eb87f..3ed532ccb 100644 --- a/test/libsolidity/smtCheckerTests/types/tuple_return_branch.sol +++ b/test/libsolidity/smtCheckerTests/types/tuple_return_branch.sol @@ -14,11 +14,6 @@ contract C { } } // ---- -// Warning 8115: (112-120): Assertion checker does not yet support the type of this variable. // Warning 8364: (137-138): Assertion checker does not yet implement type type(struct C.S storage pointer) -// Warning 8364: (137-141): Assertion checker does not yet implement type struct C.S memory // Warning 4639: (137-141): Assertion checker does not yet implement this expression. -// Warning 8115: (193-203): Assertion checker does not yet support the type of this variable. -// Warning 8364: (227-228): Assertion checker does not yet implement type struct C.S memory // Warning 4639: (137-141): Assertion checker does not yet implement this expression. -// Warning 6191: (227-228): Assertion checker does not yet implement type struct C.S memory diff --git a/test/libyul/YulOptimizerTest.cpp b/test/libyul/YulOptimizerTest.cpp index 13c9ed5c7..2f9f4c75e 100644 --- a/test/libyul/YulOptimizerTest.cpp +++ b/test/libyul/YulOptimizerTest.cpp @@ -49,6 +49,7 @@ #include #include #include +#include #include #include #include @@ -241,6 +242,13 @@ TestCase::TestResult YulOptimizerTest::run(ostream& _stream, string const& _line ExpressionJoiner::run(*m_context, *m_object->code); ExpressionJoiner::run(*m_context, *m_object->code); } + else if (m_optimizerStep == "unusedFunctionParameterPruner") + { + disambiguate(); + FunctionHoister::run(*m_context, *m_object->code); + LiteralRematerialiser::run(*m_context, *m_object->code); + UnusedFunctionParameterPruner::run(*m_context, *m_object->code); + } else if (m_optimizerStep == "unusedPruner") { disambiguate(); diff --git a/test/libyul/yulOptimizerTests/fullSuite/stack_compressor_msize.yul b/test/libyul/yulOptimizerTests/fullSuite/stack_compressor_msize.yul index 56a2d6cfe..b417991c2 100644 --- a/test/libyul/yulOptimizerTests/fullSuite/stack_compressor_msize.yul +++ b/test/libyul/yulOptimizerTests/fullSuite/stack_compressor_msize.yul @@ -49,7 +49,7 @@ // sstore(not(gcd(10, 15)), 1) // sstore(0, 0) // sstore(2, 1) -// pop(foo_singlereturn_1(calldataload(0), calldataload(3))) +// extcodecopy(1, msize(), 1, 1) // sstore(0, 0) // sstore(3, 1) // } @@ -59,6 +59,4 @@ // case 0 { out := _a } // default { out := gcd(_b, mod(_a, _b)) } // } -// function foo_singlereturn_1(in, in_1) -> out -// { extcodecopy(1, msize(), 1, 1) } // } diff --git a/test/libyul/yulOptimizerTests/fullSuite/unusedFunctionParameterPruner.yul b/test/libyul/yulOptimizerTests/fullSuite/unusedFunctionParameterPruner.yul new file mode 100644 index 000000000..8fb84fb49 --- /dev/null +++ b/test/libyul/yulOptimizerTests/fullSuite/unusedFunctionParameterPruner.yul @@ -0,0 +1,31 @@ +{ + let x, y := foo(sload(0),sload(32)) + sstore(0, x) + sstore(0, y) + x, y := foo(sload(32), sload(8)) + + function foo(a, b) -> out1, out2 + { + out1 := mload(32) + out1 := sload(out1) + out2 := add(out1, 1) + extcodecopy(out1, out2, 1, b) + } +} +// ---- +// step: fullSuite +// +// { +// { +// let out1, out2 := foo(sload(32)) +// sstore(0, out1) +// sstore(0, out2) +// let out1_1, out2_1 := foo(sload(8)) +// } +// function foo(b) -> out1, out2 +// { +// out1 := sload(mload(32)) +// out2 := add(out1, 1) +// extcodecopy(out1, out2, 1, b) +// } +// } diff --git a/test/libyul/yulOptimizerTests/fullSuite/unusedFunctionParameterPruner_loop.yul b/test/libyul/yulOptimizerTests/fullSuite/unusedFunctionParameterPruner_loop.yul new file mode 100644 index 000000000..47635e415 --- /dev/null +++ b/test/libyul/yulOptimizerTests/fullSuite/unusedFunctionParameterPruner_loop.yul @@ -0,0 +1,33 @@ +{ + sstore(f(1), 1) + sstore(f(2), 1) + sstore(f(3), 1) + function f(a) -> x { + for {let b := 10} iszero(b) { b := sub(b, 1) } + { + a := calldataload(0) + mstore(a, x) + } + } +} +// ---- +// step: fullSuite +// +// { +// { +// f() +// sstore(0, 1) +// f() +// sstore(0, 1) +// f() +// sstore(0, 1) +// } +// function f() +// { +// let b := 10 +// let _1 := 0 +// let a := calldataload(_1) +// for { } iszero(b) { b := add(b, not(0)) } +// { mstore(a, _1) } +// } +// } diff --git a/test/libyul/yulOptimizerTests/fullSuite/unusedFunctionParameterPruner_recursion.yul b/test/libyul/yulOptimizerTests/fullSuite/unusedFunctionParameterPruner_recursion.yul new file mode 100644 index 000000000..69b4517eb --- /dev/null +++ b/test/libyul/yulOptimizerTests/fullSuite/unusedFunctionParameterPruner_recursion.yul @@ -0,0 +1,29 @@ +{ + let j, k, l := f(1, 2, 3) + sstore(0, j) + sstore(1, k) + sstore(1, l) + function f(a, b, c) -> x, y, z + { + x, y, z := f(1, 2, 3) + x := add(x, 1) + } +} +// ---- +// step: fullSuite +// +// { +// { +// let x, y, z := f() +// sstore(0, x) +// sstore(1, y) +// sstore(1, z) +// } +// function f() -> x, y, z +// { +// let x_1, y_1, z_1 := f() +// y := y_1 +// z := z_1 +// x := add(x_1, 1) +// } +// } diff --git a/test/libyul/yulOptimizerTests/fullSuite/unusedFunctionParameterPruner_return.yul b/test/libyul/yulOptimizerTests/fullSuite/unusedFunctionParameterPruner_return.yul new file mode 100644 index 000000000..aed7406be --- /dev/null +++ b/test/libyul/yulOptimizerTests/fullSuite/unusedFunctionParameterPruner_return.yul @@ -0,0 +1,34 @@ +{ + let x, y, z := foo(sload(0),sload(32)) + sstore(0, x) + sstore(0, y) + sstore(0, z) + x, y, z := foo(sload(32), sload(8)) + + // out3 is unassigned. + function foo(a, b) -> out1, out2, out3 + { + out1 := mload(32) + out1 := sload(out1) + out2 := add(out1, 1) + extcodecopy(out1, out1, 1, b) + } +} +// ---- +// step: fullSuite +// +// { +// { +// let out1, out2 := foo(sload(32)) +// sstore(0, out1) +// sstore(0, out2) +// sstore(0, 0) +// let out1_1, out2_1 := foo(sload(8)) +// } +// function foo(b) -> out1, out2 +// { +// out1 := sload(mload(32)) +// out2 := add(out1, 1) +// extcodecopy(out1, out1, 1, b) +// } +// } diff --git a/test/libyul/yulOptimizerTests/fullSuite/unusedFunctionParameterPruner_simple.yul b/test/libyul/yulOptimizerTests/fullSuite/unusedFunctionParameterPruner_simple.yul new file mode 100644 index 000000000..a50257b2b --- /dev/null +++ b/test/libyul/yulOptimizerTests/fullSuite/unusedFunctionParameterPruner_simple.yul @@ -0,0 +1,36 @@ +{ + sstore(f(1), 1) + sstore(f(2), 1) + sstore(f(3), 1) + function f(a) -> x { + // The usage of a is redundant + a := calldataload(0) + mstore(a, x) + // to prevent getting fully inlined + sstore(1, 1) + sstore(2, 2) + sstore(3, 3) + sstore(3, 3) + } +} +// ---- +// step: fullSuite +// +// { +// { +// f() +// sstore(0, 1) +// f() +// sstore(0, 1) +// f() +// sstore(0, 1) +// } +// function f() +// { +// mstore(calldataload(0), 0) +// sstore(1, 1) +// sstore(2, 2) +// sstore(3, 3) +// sstore(3, 3) +// } +// } diff --git a/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/LiteralRematerialiser.yul b/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/LiteralRematerialiser.yul new file mode 100644 index 000000000..e11ea2a96 --- /dev/null +++ b/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/LiteralRematerialiser.yul @@ -0,0 +1,27 @@ +{ + let a := f(mload(1)) + let b := f(a) + sstore(a, b) + function f(x) -> y + { + // Test if LiteralRematerializer can convert `y` to `0` and therefore allowing us to + // rewrite the function f + if iszero(x) { revert(y, y)} + if iszero(add(x, 1)) { revert(y, y)} + } +} +// ---- +// step: unusedFunctionParameterPruner +// +// { +// let a := f_1(mload(1)) +// let b := f_1(a) +// sstore(a, b) +// function f(x) +// { +// if iszero(x) { revert(0, 0) } +// if iszero(add(x, 1)) { revert(0, 0) } +// } +// function f_1(x_2) -> y_3 +// { f(x_2) } +// } diff --git a/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/multiple_param.yul b/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/multiple_param.yul new file mode 100644 index 000000000..f2a036459 --- /dev/null +++ b/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/multiple_param.yul @@ -0,0 +1,24 @@ +{ + let d, e, i := f(1, 2, 3) + sstore(d, 0) + // b and x are unused + function f(a, b, c) -> x, y, z + { + y := mload(a) + z := mload(c) + } +} +// ---- +// step: unusedFunctionParameterPruner +// +// { +// let d, e, i := f_1(1, 2, 3) +// sstore(d, 0) +// function f(a, c) -> y, z +// { +// y := mload(a) +// z := mload(c) +// } +// function f_1(a_2, b_3, c_4) -> x_5, y_6, z_7 +// { y_6, z_7 := f(a_2, c_4) } +// } diff --git a/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/multiple_return.yul b/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/multiple_return.yul new file mode 100644 index 000000000..51612a699 --- /dev/null +++ b/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/multiple_return.yul @@ -0,0 +1,24 @@ +{ + let a, b, c := f(sload(0)) + sstore(a, 0) + // d is unused, x is unassigned + function f(d) -> x, y, z + { + y := mload(1) + z := mload(2) + } +} +// ---- +// step: unusedFunctionParameterPruner +// +// { +// let a, b, c := f_1(sload(0)) +// sstore(a, 0) +// function f() -> y, z +// { +// y := mload(1) +// z := mload(2) +// } +// function f_1(d_2) -> x_3, y_4, z_5 +// { y_4, z_5 := f() } +// } diff --git a/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/nested_function.yul b/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/nested_function.yul new file mode 100644 index 000000000..d09ba44a6 --- /dev/null +++ b/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/nested_function.yul @@ -0,0 +1,56 @@ +// Test case to see if the step applies for nested functions. The function `j` has an unused argument. +{ + sstore(f(1), 0) + sstore(h(1), 0) + + function f(a) -> x + { + x := g(1) + x := add(x, 1) + function g(b) -> y + { + b := add(b, 1) + y := mload(b) + } + } + + function h(c) -> u + { + u := j(c) + // d is unused + function j(d) -> w + { + w := 13 + w := add(w, 1) + } + } + +} +// ---- +// step: unusedFunctionParameterPruner +// +// { +// sstore(f_1(1), 0) +// sstore(h(1), 0) +// function g(b) -> y +// { +// b := add(b, 1) +// y := mload(b) +// } +// function f() -> x +// { +// x := g(1) +// x := add(x, 1) +// } +// function f_1(a_3) -> x_4 +// { x_4 := f() } +// function j() -> w +// { +// w := 13 +// w := add(13, 1) +// } +// function j_2(d_5) -> w_6 +// { w_6 := j() } +// function h(c) -> u +// { u := j_2(c) } +// } diff --git a/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/nested_function_name_collision.yul b/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/nested_function_name_collision.yul new file mode 100644 index 000000000..8ce80f140 --- /dev/null +++ b/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/nested_function_name_collision.yul @@ -0,0 +1,52 @@ +// Test case where the name `g` occurs at two different places. Test to see if name-collision can +// cause issues. +{ + sstore(h(1), 0) + sstore(f(1), 0) + + function f(c) -> u + { + u := g(c) + function g(d) -> w + { + w := 13 + sstore(0, w) + } + } + + function h(c) -> u + { + u := g(c) + function g(d) -> w + { + w := 13 + sstore(0, w) + } + } + +} +// ---- +// step: unusedFunctionParameterPruner +// +// { +// sstore(h(1), 0) +// sstore(f(1), 0) +// function g() -> w +// { +// w := 13 +// sstore(0, 13) +// } +// function g_1(d_3) -> w_4 +// { w_4 := g() } +// function f(c) -> u +// { u := g_1(c) } +// function g_3() -> w_5 +// { +// w_5 := 13 +// sstore(0, 13) +// } +// function g_3_2(d_4_5) -> w_5_6 +// { w_5_6 := g_3() } +// function h(c_1) -> u_2 +// { u_2 := g_3_2(c_1) } +// } diff --git a/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/no_return.yul b/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/no_return.yul new file mode 100644 index 000000000..1cf059da2 --- /dev/null +++ b/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/no_return.yul @@ -0,0 +1,21 @@ +{ + f(1, 2) + function f(a, b) + { + sstore(a, 0) + a := add(a, 1) + } +} +// ---- +// step: unusedFunctionParameterPruner +// +// { +// f_1(1, 2) +// function f(a) +// { +// sstore(a, 0) +// a := add(a, 1) +// } +// function f_1(a_2, b_3) +// { f(a_2) } +// } diff --git a/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/no_unused.yul b/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/no_unused.yul new file mode 100644 index 000000000..ebbb70536 --- /dev/null +++ b/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/no_unused.yul @@ -0,0 +1,16 @@ +// A test where all parameters are used +{ + sstore(f(1), 0) + function f(a) -> x { x := a } + function g(b) -> y { y := g(b) } +} +// ---- +// step: unusedFunctionParameterPruner +// +// { +// sstore(f(1), 0) +// function f(a) -> x +// { x := a } +// function g(b) -> y +// { y := g(b) } +// } diff --git a/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/recursion.yul b/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/recursion.yul new file mode 100644 index 000000000..4a2c5b6cc --- /dev/null +++ b/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/recursion.yul @@ -0,0 +1,21 @@ +{ + let a1, b1, c1 := f(1, 2, 3) + function f(a, b, c) -> x, y, z + { + x, y, z := f(1, 2, 3) + x := add(x, 1) + } +} +// ---- +// step: unusedFunctionParameterPruner +// +// { +// let a1, b1, c1 := f_1(1, 2, 3) +// function f() -> x, y, z +// { +// x, y, z := f_1(1, 2, 3) +// x := add(x, 1) +// } +// function f_1(a_2, b_3, c_4) -> x_5, y_6, z_7 +// { x_5, y_6, z_7 := f() } +// } diff --git a/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/simple.yul b/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/simple.yul new file mode 100644 index 000000000..873eef977 --- /dev/null +++ b/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/simple.yul @@ -0,0 +1,21 @@ +{ + sstore(f(1), 0) + function f(x) -> y + { + let w := mload(1) + y := mload(w) + } +} +// ---- +// step: unusedFunctionParameterPruner +// +// { +// sstore(f_1(1), 0) +// function f() -> y +// { +// let w := mload(1) +// y := mload(w) +// } +// function f_1(x_2) -> y_3 +// { y_3 := f() } +// } diff --git a/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/smoke.yul b/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/smoke.yul new file mode 100644 index 000000000..1e0f9eb61 --- /dev/null +++ b/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/smoke.yul @@ -0,0 +1,5 @@ +{} +// ---- +// step: unusedFunctionParameterPruner +// +// { } diff --git a/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/too_many_arguments.yul b/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/too_many_arguments.yul new file mode 100644 index 000000000..720489d57 --- /dev/null +++ b/test/libyul/yulOptimizerTests/unusedFunctionParameterPruner/too_many_arguments.yul @@ -0,0 +1,23 @@ +{ + let a, b := f(1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18) + sstore(a, b) + function f(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18) -> y, z + { + y := mload(x3) + z := mload(x7) + } +} +// ---- +// step: unusedFunctionParameterPruner +// +// { +// let a, b := f_1(1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18) +// sstore(a, b) +// function f(x3, x7) -> y, z +// { +// y := mload(x3) +// z := mload(x7) +// } +// function f_1(x1_2, x2_3, x3_4, x4_5, x5_6, x6_7, x7_8, x8_9, x9_10, x10_11, x11_12, x12_13, x13_14, x14_15, x15_16, x16_17, x17_18, x18_19) -> y_20, z_21 +// { y_20, z_21 := f(x3_4, x7_8) } +// } diff --git a/test/yulPhaser/Chromosome.cpp b/test/yulPhaser/Chromosome.cpp index ecf754e8e..2c201990f 100644 --- a/test/yulPhaser/Chromosome.cpp +++ b/test/yulPhaser/Chromosome.cpp @@ -130,7 +130,7 @@ BOOST_AUTO_TEST_CASE(output_operator_should_create_concise_and_unambiguous_strin BOOST_TEST(chromosome.length() == allSteps.size()); BOOST_TEST(chromosome.optimisationSteps() == allSteps); - BOOST_TEST(toString(chromosome) == "flcCUnDvejsxIOoighTLMrmVatud"); + BOOST_TEST(toString(chromosome) == "flcCUnDvejsxIOoighTLMrmVatpud"); } BOOST_AUTO_TEST_CASE(randomOptimisationStep_should_return_each_step_with_same_probability) diff --git a/test/yulPhaser/Mutations.cpp b/test/yulPhaser/Mutations.cpp index dfdd600a3..eaf64cafa 100644 --- a/test/yulPhaser/Mutations.cpp +++ b/test/yulPhaser/Mutations.cpp @@ -103,10 +103,10 @@ BOOST_AUTO_TEST_CASE(geneAddition_should_iterate_over_gene_positions_and_insert_ SimulationRNG::reset(1); // f c C U n D v e j s BOOST_TEST(mutation01(chromosome) == Chromosome(stripWhitespace(" f c C UC n D v e jx s"))); // 20% more - BOOST_TEST(mutation05(chromosome) == Chromosome(stripWhitespace("j f cu C U ne D v eI j sf"))); // 50% more + BOOST_TEST(mutation05(chromosome) == Chromosome(stripWhitespace("s f cu C U nj D v eI j sf"))); // 50% more SimulationRNG::reset(2); BOOST_TEST(mutation01(chromosome) == Chromosome(stripWhitespace(" f cu C U n D v e j s"))); // 10% more - BOOST_TEST(mutation05(chromosome) == Chromosome(stripWhitespace("L f ce Cv U n D v e jO s"))); // 40% more + BOOST_TEST(mutation05(chromosome) == Chromosome(stripWhitespace("M f ce Cv U n D v e jo s"))); // 40% more } BOOST_AUTO_TEST_CASE(geneAddition_should_be_able_to_insert_before_first_position)