diff --git a/Changelog.md b/Changelog.md index fe6baf4de..1fa3ee987 100644 --- a/Changelog.md +++ b/Changelog.md @@ -19,6 +19,7 @@ Compiler Features: Bugfixes: * Code Generator: Fix a crash when using ``@use-src`` and compiling from Yul to ewasm. * SMTChecker: Fix internal error when an unsafe target is solved more than once and the counterexample messages are different. + * SMTChecker: Fix soundness of assigned storage/memory local pointers that were not erasing enough knowledge. * Fix internal error when a function has a calldata struct argument with an internal type inside. diff --git a/docs/yul.rst b/docs/yul.rst index 219905cd5..60a2da5b9 100644 --- a/docs/yul.rst +++ b/docs/yul.rst @@ -541,10 +541,24 @@ evaluate to zero values. In all other situations, expressions have to evaluate to exactly one value. -The ``continue`` and ``break`` statements can only be used inside loop bodies -and have to be in the same function as the loop (or both have to be at the -top level). The ``continue`` and ``break`` statements cannot be used -in other parts of a loop, not even when it is scoped inside a second loop's body. +A ``continue`` or ``break`` statement can only be used inside the body of a for-loop, as follows. +Consider the innermost loop that contains the statement. +The loop and the statement must be in the same function, or both must be at the top level. +The statement must be in the loop's body block; +it cannot be in the loop's initialization block or update block. +It is worth emphasizing that this restriction applies just +to the innermost loop that contains the ``continue`` or ``break`` statement: +this innermost loop, and therefore the ``continue`` or ``break`` statement, +may appear anywhere in an outer loop, possibly in an outer loop's initialization block or update block. +For example, the following is legal, +because the ``break`` occurs in the body block of the inner loop, +despite also occurring in the update block of the outer loop: + +.. code-block:: yul + + for {} true { for {} true {} { break } } + { + } The condition part of the for-loop has to evaluate to exactly one value. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 11ac5ab7a..8326b6b2f 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -32,6 +32,8 @@ #include +#include + #include #include @@ -2371,28 +2373,25 @@ void SMTEncoder::resetReferences(Type const* _type) bool SMTEncoder::sameTypeOrSubtype(Type const* _a, Type const* _b) { - Type const* 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) + bool foundSame = false; + + solidity::util::BreadthFirstSearch bfs{{_a}}; + bfs.run([&](auto _type, auto&& _addChild) { + if (*typeWithoutPointer(_b) == *typeWithoutPointer(_type)) { - auto mapPrefix = dynamic_cast(prefix); - solAssert(mapPrefix, ""); - prefix = mapPrefix->valueType(); + foundSame = true; + bfs.abort(); } - else - { - auto arrayPrefix = dynamic_cast(prefix); - solAssert(arrayPrefix, ""); - prefix = arrayPrefix->baseType(); - } - } - return false; + if (auto const* mapType = dynamic_cast(_type)) + _addChild(mapType->valueType()); + else if (auto const* arrayType = dynamic_cast(_type)) + _addChild(arrayType->baseType()); + else if (auto const* structType = dynamic_cast(_type)) + for (auto const& member: structType->nativeMembers(nullptr)) + _addChild(member.type); + }); + + return foundSame; } bool SMTEncoder::isSupportedType(Type const& _type) const diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp index 4b7faf496..5292d5329 100644 --- a/libsolidity/interface/CompilerStack.cpp +++ b/libsolidity/interface/CompilerStack.cpp @@ -1447,7 +1447,7 @@ CompilerStack::Source const& CompilerStack::source(string const& _sourceName) co { auto it = m_sources.find(_sourceName); if (it == m_sources.end()) - solThrow(CompilerError, "Given source file not found."); + solThrow(CompilerError, "Given source file not found: " + _sourceName); return it->second; } diff --git a/libsolidity/interface/FileReader.cpp b/libsolidity/interface/FileReader.cpp index cfd1feb33..47f4d2b5a 100644 --- a/libsolidity/interface/FileReader.cpp +++ b/libsolidity/interface/FileReader.cpp @@ -84,7 +84,7 @@ void FileReader::allowDirectory(boost::filesystem::path _path) m_allowedDirectories.insert(std::move(_path)); } -void FileReader::setSource(boost::filesystem::path const& _path, SourceCode _source) +void FileReader::addOrUpdateFile(boost::filesystem::path const& _path, SourceCode _source) { m_sourceCodes[cliPathToSourceUnitName(_path)] = std::move(_source); } @@ -94,7 +94,7 @@ void FileReader::setStdin(SourceCode _source) m_sourceCodes[""] = std::move(_source); } -void FileReader::setSources(StringMap _sources) +void FileReader::setSourceUnits(StringMap _sources) { m_sourceCodes = std::move(_sources); } @@ -172,7 +172,7 @@ ReadCallback::Result FileReader::readFile(string const& _kind, string const& _so } } -string FileReader::cliPathToSourceUnitName(boost::filesystem::path const& _cliPath) +string FileReader::cliPathToSourceUnitName(boost::filesystem::path const& _cliPath) const { vector prefixes = {m_basePath.empty() ? normalizeCLIPathForVFS(".") : m_basePath}; prefixes += m_includePaths; @@ -189,7 +189,7 @@ string FileReader::cliPathToSourceUnitName(boost::filesystem::path const& _cliPa return normalizedPath.generic_string(); } -map FileReader::detectSourceUnitNameCollisions(FileSystemPathSet const& _cliPaths) +map FileReader::detectSourceUnitNameCollisions(FileSystemPathSet const& _cliPaths) const { map nameToPaths; for (boost::filesystem::path const& cliPath: _cliPaths) diff --git a/libsolidity/interface/FileReader.h b/libsolidity/interface/FileReader.h index 71f5819df..3892e9826 100644 --- a/libsolidity/interface/FileReader.h +++ b/libsolidity/interface/FileReader.h @@ -61,18 +61,17 @@ public: void allowDirectory(boost::filesystem::path _path); FileSystemPathSet const& allowedDirectories() const noexcept { return m_allowedDirectories; } - StringMap const& sourceCodes() const noexcept { return m_sourceCodes; } - - /// Retrieves the source code for a given source unit name. - SourceCode const& sourceCode(SourceUnitName const& _sourceUnitName) const { return m_sourceCodes.at(_sourceUnitName); } + /// @returns all sources by their internal source unit names. + StringMap const& sourceUnits() const noexcept { return m_sourceCodes; } /// Resets all sources to the given map of source unit name to source codes. /// Does not enforce @a allowedDirectories(). - void setSources(StringMap _sources); + void setSourceUnits(StringMap _sources); - /// Adds the source code under a source unit name created by normalizing the file path. + /// Adds the source code under a source unit name created by normalizing the file path + /// or changes an existing source. /// Does not enforce @a allowedDirectories(). - void setSource(boost::filesystem::path const& _path, SourceCode _source); + void addOrUpdateFile(boost::filesystem::path const& _path, SourceCode _source); /// Adds the source code under the source unit name of @a . /// Does not enforce @a allowedDirectories(). @@ -83,7 +82,7 @@ public: /// The read will only succeed if the canonical path of the file is within one of the @a allowedDirectories(). /// @param _kind must be equal to "source". Other values are not supported. /// @return Content of the loaded file or an error message. If the operation succeeds, a copy of - /// the content is retained in @a sourceCodes() under the key of @a _sourceUnitName. If the key + /// the content is retained in @a sourceUnits() under the key of @a _sourceUnitName. If the key /// already exists, previous content is discarded. frontend::ReadCallback::Result readFile(std::string const& _kind, std::string const& _sourceUnitName); @@ -94,14 +93,14 @@ public: /// Creates a source unit name by normalizing a path given on the command line and, if possible, /// making it relative to base path or one of the include directories. - std::string cliPathToSourceUnitName(boost::filesystem::path const& _cliPath); + std::string cliPathToSourceUnitName(boost::filesystem::path const& _cliPath) const; /// Checks if a set contains any paths that lead to different files but would receive identical /// source unit names. Files are considered the same if their paths are exactly the same after /// normalization (without following symlinks). /// @returns a map containing all the conflicting source unit names and the paths that would /// receive them. The returned paths are normalized. - std::map detectSourceUnitNameCollisions(FileSystemPathSet const& _cliPaths); + std::map detectSourceUnitNameCollisions(FileSystemPathSet const& _cliPaths) const; /// Normalizes a filesystem path to make it include all components up to the filesystem root, /// remove small, inconsequential differences that do not affect the meaning and make it look diff --git a/solc/CommandLineInterface.cpp b/solc/CommandLineInterface.cpp index 5fbdfd08d..aecc49d81 100644 --- a/solc/CommandLineInterface.cpp +++ b/solc/CommandLineInterface.cpp @@ -483,7 +483,7 @@ void CommandLineInterface::readInputFiles() } else { - m_fileReader.setSource(infile, move(fileContent)); + m_fileReader.addOrUpdateFile(infile, move(fileContent)); m_fileReader.allowDirectory(boost::filesystem::canonical(infile).remove_filename()); } } @@ -499,7 +499,7 @@ void CommandLineInterface::readInputFiles() m_fileReader.setStdin(readUntilEnd(m_sin)); } - if (m_fileReader.sourceCodes().empty() && !m_standardJsonInput.has_value()) + if (m_fileReader.sourceUnits().empty() && !m_standardJsonInput.has_value()) solThrow(CommandLineValidationError, "All specified input files either do not exist or are not regular files."); } @@ -510,7 +510,7 @@ map CommandLineInterface::parseAstFromInput() map sourceJsons; map tmpSources; - for (SourceCode const& sourceCode: m_fileReader.sourceCodes() | ranges::views::values) + for (SourceCode const& sourceCode: m_fileReader.sourceUnits() | ranges::views::values) { Json::Value ast; astAssert(jsonParseStrict(sourceCode, ast), "Input file could not be parsed to JSON"); @@ -528,7 +528,7 @@ map CommandLineInterface::parseAstFromInput() } } - m_fileReader.setSources(tmpSources); + m_fileReader.setSourceUnits(tmpSources); return sourceJsons; } @@ -721,7 +721,7 @@ void CommandLineInterface::compile() } else { - m_compiler->setSources(m_fileReader.sourceCodes()); + m_compiler->setSources(m_fileReader.sourceUnits()); m_compiler->setParserErrorRecovery(m_options.input.errorRecovery); } @@ -835,7 +835,7 @@ void CommandLineInterface::handleCombinedJSON() if (m_options.compiler.combinedJsonRequests->ast) { output[g_strSources] = Json::Value(Json::objectValue); - for (auto const& sourceCode: m_fileReader.sourceCodes()) + for (auto const& sourceCode: m_fileReader.sourceUnits()) { ASTJsonConverter converter(m_compiler->state(), m_compiler->sourceIndices()); output[g_strSources][sourceCode.first] = Json::Value(Json::objectValue); @@ -858,12 +858,12 @@ void CommandLineInterface::handleAst() return; vector asts; - for (auto const& sourceCode: m_fileReader.sourceCodes()) + for (auto const& sourceCode: m_fileReader.sourceUnits()) asts.push_back(&m_compiler->ast(sourceCode.first)); if (!m_options.output.dir.empty()) { - for (auto const& sourceCode: m_fileReader.sourceCodes()) + for (auto const& sourceCode: m_fileReader.sourceUnits()) { stringstream data; string postfix = ""; @@ -876,7 +876,7 @@ void CommandLineInterface::handleAst() else { sout() << "JSON AST (compact format):" << endl << endl; - for (auto const& sourceCode: m_fileReader.sourceCodes()) + for (auto const& sourceCode: m_fileReader.sourceUnits()) { sout() << endl << "======= " << sourceCode.first << " =======" << endl; ASTJsonConverter(m_compiler->state(), m_compiler->sourceIndices()).print(sout(), m_compiler->ast(sourceCode.first)); @@ -908,7 +908,7 @@ void CommandLineInterface::link() librariesReplacements[replacement] = library.second; } - FileReader::StringMap sourceCodes = m_fileReader.sourceCodes(); + FileReader::StringMap sourceCodes = m_fileReader.sourceUnits(); for (auto& src: sourceCodes) { auto end = src.second.end(); @@ -944,14 +944,14 @@ void CommandLineInterface::link() while (!src.second.empty() && *prev(src.second.end()) == '\n') src.second.resize(src.second.size() - 1); } - m_fileReader.setSources(move(sourceCodes)); + m_fileReader.setSourceUnits(move(sourceCodes)); } void CommandLineInterface::writeLinkedFiles() { solAssert(m_options.input.mode == InputMode::Linker, ""); - for (auto const& src: m_fileReader.sourceCodes()) + for (auto const& src: m_fileReader.sourceUnits()) if (src.first == g_stdinFileName) sout() << src.second << endl; else @@ -989,7 +989,7 @@ void CommandLineInterface::assemble(yul::AssemblyStack::Language _language, yul: bool successful = true; map assemblyStacks; - for (auto const& src: m_fileReader.sourceCodes()) + for (auto const& src: m_fileReader.sourceUnits()) { // --no-optimize-yul option is not accepted in assembly mode. solAssert(!m_options.optimizer.noOptimizeYul, ""); @@ -1029,7 +1029,7 @@ void CommandLineInterface::assemble(yul::AssemblyStack::Language _language, yul: solThrow(CommandLineExecutionError, ""); } - for (auto const& src: m_fileReader.sourceCodes()) + for (auto const& src: m_fileReader.sourceUnits()) { string machine = _targetMachine == yul::AssemblyStack::Machine::EVM ? "EVM" : @@ -1121,7 +1121,7 @@ void CommandLineInterface::outputCompilationResults() if (m_options.compiler.outputs.asmJson) ret = jsonPrettyPrint(removeNullMembers(m_compiler->assemblyJSON(contract))); else - ret = m_compiler->assemblyString(contract, m_fileReader.sourceCodes()); + ret = m_compiler->assemblyString(contract, m_fileReader.sourceUnits()); if (!m_options.output.dir.empty()) createFile(m_compiler->filesystemFriendlyName(contract) + (m_options.compiler.outputs.asmJson ? "_evm.json" : ".evm"), ret); diff --git a/test/externalTests/colony.sh b/test/externalTests/colony.sh index dff745d68..65a2183bc 100755 --- a/test/externalTests/colony.sh +++ b/test/externalTests/colony.sh @@ -36,6 +36,7 @@ function colony_test local repo="https://github.com/solidity-external-tests/colonyNetwork.git" local branch=develop_080 local config_file="truffle.js" + # On levels 1 and 2 it compiles but tests run out of gas local min_optimizer_level=3 local max_optimizer_level=3 @@ -49,7 +50,7 @@ function colony_test neutralize_package_json_hooks force_truffle_compiler_settings "$config_file" "$BINARY_TYPE" "${DIR}/solc" "$min_optimizer_level" - yarn + yarn install git submodule update --init cd lib diff --git a/test/externalTests/common.sh b/test/externalTests/common.sh index b36861d07..80a9dec32 100644 --- a/test/externalTests/common.sh +++ b/test/externalTests/common.sh @@ -248,7 +248,7 @@ function optimizer_settings_for_level case "$level" in 1) echo "{enabled: false}" ;; - 2) echo "{enabled: true}" ;; + 2) echo "{enabled: true, details: {yul: false}}" ;; 3) echo "{enabled: true, details: {yul: true}}" ;; *) fail "Optimizer level not found. Please define OPTIMIZER_LEVEL=[1, 2, 3]" diff --git a/test/externalTests/ens.sh b/test/externalTests/ens.sh index 5c7d58270..7b354acde 100755 --- a/test/externalTests/ens.sh +++ b/test/externalTests/ens.sh @@ -35,7 +35,7 @@ function ens_test { local repo="https://github.com/ensdomains/ens.git" local branch=master - local config_file="truffle-config.js" + local config_file="truffle.js" local min_optimizer_level=1 local max_optimizer_level=3 diff --git a/test/externalTests/gnosis-v2.sh b/test/externalTests/gnosis-v2.sh index b2f6c4a83..b71749a06 100755 --- a/test/externalTests/gnosis-v2.sh +++ b/test/externalTests/gnosis-v2.sh @@ -36,6 +36,7 @@ function gnosis_safe_test local repo="https://github.com/solidity-external-tests/safe-contracts.git" local branch=v2_080 local config_file="truffle-config.js" + # level 1: "Error: while migrating GnosisSafe: Returned error: base fee exceeds gas limit" local min_optimizer_level=2 local max_optimizer_level=3 @@ -63,4 +64,4 @@ function gnosis_safe_test done } -external_test Gnosis-Safe gnosis_safe_test +external_test Gnosis-Safe-V2 gnosis_safe_test diff --git a/test/externalTests/gnosis.sh b/test/externalTests/gnosis.sh index 69d068474..97208660b 100755 --- a/test/externalTests/gnosis.sh +++ b/test/externalTests/gnosis.sh @@ -36,7 +36,8 @@ function gnosis_safe_test local repo="https://github.com/solidity-external-tests/safe-contracts.git" local branch=development_080 local config_file="truffle-config.js" - local min_optimizer_level=2 + # levels 1 and 2: "Stack too deep" error + local min_optimizer_level=3 local max_optimizer_level=3 local selected_optimizer_levels diff --git a/test/libsolidity/smtCheckerTests/file_level/import.sol b/test/libsolidity/smtCheckerTests/file_level/import.sol index a67ee4eb6..85ae71293 100644 --- a/test/libsolidity/smtCheckerTests/file_level/import.sol +++ b/test/libsolidity/smtCheckerTests/file_level/import.sol @@ -22,5 +22,5 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (B:238-252): CHC: Assertion violation happens here.\nCounterexample:\ndata = {x: 0}\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: data = {x: 0}\nC.g()\n C.f(7) -- internal call\n A:set({x: 0}, 7) -- internal call\n A:set({x: 0}, 8) -- internal call -// Warning 6328: (B:308-322): CHC: Assertion violation happens here.\nCounterexample:\ndata = {x: 0}\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: data = {x: 0}\nC.g()\n C.f(7) -- internal call\n A:set({x: 0}, 7) -- internal call\n A:set({x: 0}, 8) -- internal call +// Warning 6328: (B:238-252): CHC: Assertion violation happens here.\nCounterexample:\ndata = {x: 21238}\nx = 8\ny = 21238\n\nTransaction trace:\nC.constructor()\nState: data = {x: 0}\nC.g()\n C.f(7) -- internal call\n A:set({x: 0}, 7) -- internal call\n A:set({x: 8}, 8) -- internal call +// Warning 6328: (B:308-322): CHC: Assertion violation happens here.\nCounterexample:\ndata = {x: 6}\nx = 0\ny = 6\n\nTransaction trace:\nC.constructor()\nState: data = {x: 0}\nC.g()\n C.f(7) -- internal call\n A:set({x: 0}, 7) -- internal call\n A:set({x: 0}, 8) -- internal call diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_memory_1.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_memory_1.sol new file mode 100644 index 000000000..edb1e1b40 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_memory_1.sol @@ -0,0 +1,21 @@ +contract C { + struct S { + uint sum; + uint[] a; + } + + function f(S memory m, uint v) internal pure { + m.sum = v; + m.a = new uint[](2); + } + + constructor(uint amt) { + S memory s; + f(s, amt); + assert(s.a.length == 2); // should hold but no aliasing support means it fails for now + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 6328: (201-224): CHC: Assertion violation happens here.\nCounterexample:\n\namt = 0\ns = {sum: 0, a: []}\n\nTransaction trace:\nC.constructor(0) diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_memory_2.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_memory_2.sol new file mode 100644 index 000000000..28da83700 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_memory_2.sol @@ -0,0 +1,26 @@ +contract C { + struct S { + uint sum; + uint[] a; + } + + struct T { + S s; + uint x; + } + + function f(S memory m, uint v) internal pure { + m.sum = v; + m.a = new uint[](2); + } + + constructor(uint amt) { + T memory t; + f(t.s, amt); + assert(t.s.a.length == 2); // should hold but no aliasing support means it fails for now + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 6328: (236-261): CHC: Assertion violation happens here.\nCounterexample:\n\namt = 0\nt = {s: {sum: 0, a: []}, x: 0}\n\nTransaction trace:\nC.constructor(0) diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_memory_3.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_memory_3.sol new file mode 100644 index 000000000..36890f03e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_memory_3.sol @@ -0,0 +1,26 @@ +contract C { + struct S { + uint sum; + uint[] a; + } + + struct T { + S s; + uint x; + } + + function f(T memory m, uint v) internal pure { + m.s.sum = v; + m.s.a = new uint[](2); + } + + constructor(uint amt) { + T memory t; + f(t, amt); + assert(t.s.a.length == 2); // should hold but no aliasing support means it fails for now + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 6328: (238-263): CHC: Assertion violation happens here.\nCounterexample:\n\namt = 0\nt = {s: {sum: 0, a: []}, x: 0}\n\nTransaction trace:\nC.constructor(0) diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_1.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_1.sol new file mode 100644 index 000000000..3fd0c0d87 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_1.sol @@ -0,0 +1,24 @@ +contract C { + struct S { + mapping(address => uint) innerM; + uint sum; + } + + function f(S storage m, address i, uint v) internal { + m.innerM[i] = v; + m.sum += v; + } + + S s; + + constructor(uint amt) { + f(s, msg.sender, amt); + } + function g() public view { + assert(s.sum == 0); // should hold but no aliasing support means it fails for now + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 6328: (270-288): CHC: Assertion violation happens here.\nCounterexample:\ns = {innerM, sum: 21239}\n\nTransaction trace:\nC.constructor(0){ msg.sender: 0x6dc4 }\nState: s = {innerM, sum: 21239}\nC.g() diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_2.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_2.sol new file mode 100644 index 000000000..9d4623ae0 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_2.sol @@ -0,0 +1,23 @@ +contract C { + struct S { + mapping(address => uint) innerM; + uint sum; + } + + function f(mapping(address => uint) storage innerM, address i, uint v) internal { + innerM[i] = v; + } + + S s; + + constructor(uint amt) { + f(s.innerM, msg.sender, amt); + } + function g() public view { + assert(s.innerM[msg.sender] == 0); // should hold but no aliasing support means it fails for now + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 6328: (289-322): CHC: Assertion violation happens here.\nCounterexample:\ns = {innerM, sum: 10}\n\nTransaction trace:\nC.constructor(0){ msg.sender: 0x6dc4 }\nState: s = {innerM, sum: 10}\nC.g(){ msg.sender: 0x0985 } diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_3.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_3.sol new file mode 100644 index 000000000..8779cd095 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_3.sol @@ -0,0 +1,29 @@ +contract C { + struct S { + mapping(address => uint) innerM; + uint sum; + } + + struct T { + uint x; + S s; + } + + function f(T storage m, address i, uint v) internal { + m.s.innerM[i] = v; + m.s.sum += v; + } + + T t; + + constructor(uint amt) { + f(t, msg.sender, amt); + } + function g() public view { + assert(t.s.sum == 0); // should hold but no aliasing support means it fails for now + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 6328: (307-327): CHC: Assertion violation happens here.\nCounterexample:\nt = {x: 10, s: {innerM, sum: 21239}}\n\nTransaction trace:\nC.constructor(0){ msg.sender: 0x6dc4 }\nState: t = {x: 10, s: {innerM, sum: 21239}}\nC.g() diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_4.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_4.sol new file mode 100644 index 000000000..957c72c12 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_4.sol @@ -0,0 +1,29 @@ +contract C { + struct S { + mapping(address => uint) innerM; + uint sum; + } + + struct T { + uint x; + S s; + } + + function f(S storage m, address i, uint v) internal { + m.innerM[i] = v; + m.sum += v; + } + + T t; + + constructor(uint amt) { + f(t.s, msg.sender, amt); + } + function g() public view { + assert(t.s.sum == 0); // should hold but no aliasing support means it fails for now + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 6328: (305-325): CHC: Assertion violation happens here.\nCounterexample:\nt = {x: 10, s: {innerM, sum: 21239}}\n\nTransaction trace:\nC.constructor(0){ msg.sender: 0x6dc4 }\nState: t = {x: 10, s: {innerM, sum: 21239}}\nC.g() diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_storage.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_storage.sol index 4c13699e2..e5d9d60ab 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_storage.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_storage.sol @@ -25,5 +25,6 @@ contract C { } // ==== // SMTEngine: all +// SMTIgnoreCex: yes // ---- -// Warning 6328: (369-405): CHC: Assertion violation happens here.\nCounterexample:\ns1 = {x: 0, a: []}, s2 = {x: 0, a: []}\nb = false\ns3 = {x: 42, a: []}\n\nTransaction trace:\nC.constructor()\nState: s1 = {x: 0, a: []}, s2 = {x: 0, a: []}\nC.f(false) +// Warning 6328: (369-405): CHC: Assertion violation happens here. diff --git a/test/solc/CommandLineInterface.cpp b/test/solc/CommandLineInterface.cpp index bdc5fceec..b5fcbee57 100644 --- a/test/solc/CommandLineInterface.cpp +++ b/test/solc/CommandLineInterface.cpp @@ -211,7 +211,7 @@ BOOST_AUTO_TEST_CASE(cli_input) BOOST_TEST(result.options.input.mode == InputMode::Compiler); BOOST_TEST(result.options.input.addStdin); BOOST_CHECK_EQUAL(result.options.input.remappings, expectedRemappings); - BOOST_CHECK_EQUAL(result.reader.sourceCodes(), expectedSources); + BOOST_CHECK_EQUAL(result.reader.sourceUnits(), expectedSources); BOOST_CHECK_EQUAL(result.reader.allowedDirectories(), expectedAllowedPaths); } @@ -238,7 +238,7 @@ BOOST_AUTO_TEST_CASE(cli_ignore_missing_some_files_exist) BOOST_TEST(result.stderrContent == "\"" + (tempDir2.path() / "input2.sol").string() + "\" is not found. Skipping.\n"); BOOST_TEST(result.options.input.mode == InputMode::Compiler); BOOST_TEST(!result.options.input.addStdin); - BOOST_CHECK_EQUAL(result.reader.sourceCodes(), expectedSources); + BOOST_CHECK_EQUAL(result.reader.sourceUnits(), expectedSources); BOOST_CHECK_EQUAL(result.reader.allowedDirectories(), expectedAllowedPaths); } @@ -289,7 +289,7 @@ BOOST_AUTO_TEST_CASE(standard_json_base_path) BOOST_TEST(result.options.input.mode == InputMode::StandardJson); BOOST_TEST(result.options.input.addStdin); BOOST_TEST(result.options.input.paths.empty()); - BOOST_TEST(result.reader.sourceCodes().empty()); + BOOST_TEST(result.reader.sourceUnits().empty()); BOOST_TEST(result.reader.allowedDirectories().empty()); BOOST_TEST(result.reader.basePath() == "/" / tempDir.path().relative_path()); } @@ -302,7 +302,7 @@ BOOST_AUTO_TEST_CASE(standard_json_no_input_file) BOOST_TEST(result.options.input.mode == InputMode::StandardJson); BOOST_TEST(result.options.input.addStdin); BOOST_TEST(result.options.input.paths.empty()); - BOOST_TEST(result.reader.sourceCodes().empty()); + BOOST_TEST(result.reader.sourceUnits().empty()); BOOST_TEST(result.reader.allowedDirectories().empty()); } @@ -313,7 +313,7 @@ BOOST_AUTO_TEST_CASE(standard_json_dash) BOOST_TEST(result.stderrContent == ""); BOOST_TEST(result.options.input.mode == InputMode::StandardJson); BOOST_TEST(result.options.input.addStdin); - BOOST_TEST(result.reader.sourceCodes().empty()); + BOOST_TEST(result.reader.sourceUnits().empty()); BOOST_TEST(result.reader.allowedDirectories().empty()); } @@ -444,7 +444,7 @@ BOOST_AUTO_TEST_CASE(cli_paths_to_source_unit_names_no_base_path) BOOST_TEST(result.stdoutContent == ""); BOOST_REQUIRE(result.success); BOOST_TEST(result.options == expectedOptions); - BOOST_TEST(result.reader.sourceCodes() == expectedSources); + BOOST_TEST(result.reader.sourceUnits() == expectedSources); BOOST_TEST(result.reader.allowedDirectories() == expectedAllowedDirectories); BOOST_TEST(result.reader.basePath() == ""); } @@ -506,7 +506,7 @@ BOOST_AUTO_TEST_CASE(cli_paths_to_source_unit_names_base_path_same_as_work_dir) BOOST_TEST(result.stdoutContent == ""); BOOST_REQUIRE(result.success); BOOST_TEST(result.options == expectedOptions); - BOOST_TEST(result.reader.sourceCodes() == expectedSources); + BOOST_TEST(result.reader.sourceUnits() == expectedSources); BOOST_TEST(result.reader.allowedDirectories() == expectedAllowedDirectories); BOOST_TEST(result.reader.basePath() == expectedWorkDir); } @@ -579,7 +579,7 @@ BOOST_AUTO_TEST_CASE(cli_paths_to_source_unit_names_base_path_different_from_wor BOOST_TEST(result.stdoutContent == ""); BOOST_REQUIRE(result.success); BOOST_TEST(result.options == expectedOptions); - BOOST_TEST(result.reader.sourceCodes() == expectedSources); + BOOST_TEST(result.reader.sourceUnits() == expectedSources); BOOST_TEST(result.reader.allowedDirectories() == expectedAllowedDirectories); BOOST_TEST(result.reader.basePath() == expectedBaseDir); } @@ -648,7 +648,7 @@ BOOST_AUTO_TEST_CASE(cli_paths_to_source_unit_names_relative_base_path) BOOST_TEST(result.stdoutContent == ""); BOOST_REQUIRE(result.success); BOOST_TEST(result.options == expectedOptions); - BOOST_TEST(result.reader.sourceCodes() == expectedSources); + BOOST_TEST(result.reader.sourceUnits() == expectedSources); BOOST_TEST(result.reader.allowedDirectories() == expectedAllowedDirectories); BOOST_TEST(result.reader.basePath() == expectedWorkDir / "base"); } @@ -815,7 +815,7 @@ BOOST_AUTO_TEST_CASE(cli_paths_to_source_unit_names_normalization_and_weird_name BOOST_TEST(result.stdoutContent == ""); BOOST_REQUIRE(result.success); BOOST_TEST(result.options == expectedOptions); - BOOST_TEST(result.reader.sourceCodes() == expectedSources); + BOOST_TEST(result.reader.sourceUnits() == expectedSources); BOOST_TEST(result.reader.allowedDirectories() == expectedAllowedDirectories); BOOST_TEST(result.reader.basePath() == expectedOptions.input.basePath); } @@ -872,7 +872,7 @@ BOOST_AUTO_TEST_CASE(cli_paths_to_source_unit_names_symlinks) BOOST_TEST(result.stdoutContent == ""); BOOST_REQUIRE(result.success); BOOST_TEST(result.options == expectedOptions); - BOOST_TEST(result.reader.sourceCodes() == expectedSources); + BOOST_TEST(result.reader.sourceUnits() == expectedSources); BOOST_TEST(result.reader.allowedDirectories() == expectedAllowedDirectories); BOOST_TEST(result.reader.basePath() == expectedWorkDir / "sym/z/"); } @@ -904,7 +904,7 @@ BOOST_AUTO_TEST_CASE(cli_paths_to_source_unit_names_base_path_and_stdin) BOOST_TEST(result.stdoutContent == ""); BOOST_REQUIRE(result.success); BOOST_TEST(result.options == expectedOptions); - BOOST_TEST(result.reader.sourceCodes() == expectedSources); + BOOST_TEST(result.reader.sourceUnits() == expectedSources); BOOST_TEST(result.reader.allowedDirectories() == expectedAllowedDirectories); BOOST_TEST(result.reader.basePath() == expectedWorkDir / "base"); } @@ -1007,7 +1007,7 @@ BOOST_AUTO_TEST_CASE(cli_include_paths) BOOST_TEST(result.stdoutContent == ""); BOOST_REQUIRE(result.success); BOOST_TEST(result.options == expectedOptions); - BOOST_TEST(result.reader.sourceCodes() == expectedSources); + BOOST_TEST(result.reader.sourceUnits() == expectedSources); BOOST_TEST(result.reader.includePaths() == expectedIncludePaths); BOOST_TEST(result.reader.allowedDirectories() == expectedAllowedDirectories); BOOST_TEST(result.reader.basePath() == expectedWorkDir / "base/"); @@ -1103,7 +1103,7 @@ BOOST_AUTO_TEST_CASE(standard_json_include_paths) BOOST_REQUIRE(result.success); BOOST_TEST(result.options == expectedOptions); - BOOST_TEST(result.reader.sourceCodes() == expectedSources); + BOOST_TEST(result.reader.sourceUnits() == expectedSources); BOOST_TEST(result.reader.includePaths() == expectedIncludePaths); BOOST_TEST(result.reader.allowedDirectories() == expectedAllowedDirectories); BOOST_TEST(result.reader.basePath() == expectedWorkDir / "base/");