mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
Merge pull request #12407 from ethereum/develop
Merge develop into breaking.
This commit is contained in:
commit
c79ced0558
@ -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.
|
||||
|
||||
|
||||
|
22
docs/yul.rst
22
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.
|
||||
|
||||
|
@ -32,6 +32,8 @@
|
||||
|
||||
#include <liblangutil/CharStreamProvider.h>
|
||||
|
||||
#include <libsolutil/Algorithms.h>
|
||||
|
||||
#include <range/v3/view.hpp>
|
||||
|
||||
#include <limits>
|
||||
@ -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<Type const*> bfs{{_a}};
|
||||
bfs.run([&](auto _type, auto&& _addChild) {
|
||||
if (*typeWithoutPointer(_b) == *typeWithoutPointer(_type))
|
||||
{
|
||||
auto mapPrefix = dynamic_cast<MappingType const*>(prefix);
|
||||
solAssert(mapPrefix, "");
|
||||
prefix = mapPrefix->valueType();
|
||||
foundSame = true;
|
||||
bfs.abort();
|
||||
}
|
||||
else
|
||||
{
|
||||
auto arrayPrefix = dynamic_cast<ArrayType const*>(prefix);
|
||||
solAssert(arrayPrefix, "");
|
||||
prefix = arrayPrefix->baseType();
|
||||
}
|
||||
}
|
||||
return false;
|
||||
if (auto const* mapType = dynamic_cast<MappingType const*>(_type))
|
||||
_addChild(mapType->valueType());
|
||||
else if (auto const* arrayType = dynamic_cast<ArrayType const*>(_type))
|
||||
_addChild(arrayType->baseType());
|
||||
else if (auto const* structType = dynamic_cast<StructType const*>(_type))
|
||||
for (auto const& member: structType->nativeMembers(nullptr))
|
||||
_addChild(member.type);
|
||||
});
|
||||
|
||||
return foundSame;
|
||||
}
|
||||
|
||||
bool SMTEncoder::isSupportedType(Type const& _type) const
|
||||
|
@ -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;
|
||||
}
|
||||
|
@ -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["<stdin>"] = 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<boost::filesystem::path> 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<string, FileReader::FileSystemPathSet> FileReader::detectSourceUnitNameCollisions(FileSystemPathSet const& _cliPaths)
|
||||
map<string, FileReader::FileSystemPathSet> FileReader::detectSourceUnitNameCollisions(FileSystemPathSet const& _cliPaths) const
|
||||
{
|
||||
map<string, FileReader::FileSystemPathSet> nameToPaths;
|
||||
for (boost::filesystem::path const& cliPath: _cliPaths)
|
||||
|
@ -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 <stdin>.
|
||||
/// 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<std::string, FileSystemPathSet> detectSourceUnitNameCollisions(FileSystemPathSet const& _cliPaths);
|
||||
std::map<std::string, FileSystemPathSet> 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
|
||||
|
@ -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<string, Json::Value> CommandLineInterface::parseAstFromInput()
|
||||
map<string, Json::Value> sourceJsons;
|
||||
map<string, string> 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<string, Json::Value> 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<ASTNode const*> 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<string, yul::AssemblyStack> 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);
|
||||
|
@ -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
|
||||
|
@ -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]"
|
||||
|
@ -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
|
||||
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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)
|
@ -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)
|
@ -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)
|
@ -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()
|
@ -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 }
|
@ -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()
|
@ -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()
|
@ -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.
|
||||
|
@ -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/");
|
||||
|
Loading…
Reference in New Issue
Block a user