cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge remote-tracking branch 'origin/develop' into breaking

Browse Source
This commit is contained in:
chriseth 2021-10-27 18:09:13 +02:00
commit 8c6e5e501b
280 changed files with 2237 additions and 239 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

114
.circleci/config.yml
View File

@ -30,6 +30,45 @@ parameters:
orbs:
win: circleci/windows@2.2.0
commands:
gitter_notify:
description: "Posts a notification to the main room on Gitter (if not running on a PR)."
parameters:
event:
type: enum
enum: ["failure", "success"]
condition:
type: string
steps:
- run:
name: "Gitter notification"
when: << parameters.condition >>
command: |
[[ "<< parameters.event >>" == "failure" ]] && message=" ❌ Nightly job **${CIRCLE_JOB}** failed on **${CIRCLE_BRANCH}**. Please see [build #${CIRCLE_BUILD_NUM}](${CIRCLE_BUILD_URL}) for details."
[[ "<< parameters.event >>" == "success" ]] && message=" ✅ Nightly job **${CIRCLE_JOB}** succeeded on **${CIRCLE_BRANCH}**. Please see [build #${CIRCLE_BUILD_NUM}](${CIRCLE_BUILD_URL}) for details."
curl "https://api.gitter.im/v1/rooms/${GITTER_NOTIFY_ROOM_ID}/chatMessages" \
--request POST \
--include \
--header "Content-Type: application/json" \
--header "Accept: application/json" \
--header "Authorization: Bearer ${GITTER_API_TOKEN}" \
--data "{\"text\":\"${message}\"}"
gitter_notify_failure:
description: "Posts a failure notification to the main room on Gitter (if not running on a PR)."
steps:
- gitter_notify:
event: failure
condition: on_fail
gitter_notify_success:
description: "Posts a success notification to the main room on Gitter (if not running on a PR)."
steps:
- gitter_notify:
event: success
condition: on_success
defaults:
# --------------------------------------------------------------------------
@ -91,10 +130,14 @@ defaults:
path: upload/
# compiled tool executable target
- artifacts_tools: &artifacts_tools
- artifact_solidity_upgrade: &artifact_solidity_upgrade
path: build/tools/solidity-upgrade
destination: solidity-upgrade
- artifact_yul_phaser: &artifact_yul_phaser
path: build/tools/yul-phaser
destination: yul-phaser
# compiled executable targets
- artifacts_executables: &artifacts_executables
root: build
@ -263,28 +306,6 @@ defaults:
requires:
- b_win_release
# --------------------------------------------------------------------------
# Notification Templates
- gitter_notify_failure: &gitter_notify_failure
name: Gitter notify failure
command: >-
curl -X POST -i
-i -H "Content-Type: application/json"
-H "Accept: application/json"
-H "Authorization: Bearer $GITTER_API_TOKEN" "https://api.gitter.im/v1/rooms/$GITTER_NOTIFY_ROOM_ID/chatMessages"
-d '{"text":" ❌ Nightly job **'$CIRCLE_JOB'** failed on **'$CIRCLE_BRANCH'**. Please see '$CIRCLE_BUILD_URL' for details."}'
when: on_fail
- gitter_notify_success: &gitter_notify_success
name: Gitter notify success
command: >-
curl -X POST -i
-i -H "Content-Type: application/json"
-H "Accept: application/json"
-H "Authorization: Bearer $GITTER_API_TOKEN" "https://api.gitter.im/v1/rooms/$GITTER_NOTIFY_ROOM_ID/chatMessages"
-d '{"text":" ✅ Nightly job **'$CIRCLE_JOB'** succeeded on **'$CIRCLE_BRANCH'**. Please see '$CIRCLE_BUILD_URL' for details."}'
when: on_success
# -----------------------------------------------------------------------------------------------
jobs:
@ -447,7 +468,8 @@ jobs:
- checkout
- run: *run_build
- store_artifacts: *artifacts_solc
- store_artifacts: *artifacts_tools
- store_artifacts: *artifact_solidity_upgrade
- store_artifacts: *artifact_yul_phaser
- persist_to_workspace: *artifacts_executables
# x64 ASAN build, for testing for memory related bugs
@ -502,7 +524,7 @@ jobs:
steps:
- checkout
- run: *run_build
- run: *gitter_notify_failure
- gitter_notify_failure
- store_artifacts: *artifacts_solc
- persist_to_workspace: *artifacts_executables
@ -595,8 +617,8 @@ jobs:
git clone https://github.com/ethereum/solidity-fuzzing-corpus /tmp/solidity-fuzzing-corpus
mkdir -p test_results
scripts/regressions.py -o test_results
- run: *gitter_notify_failure
- run: *gitter_notify_success
- gitter_notify_failure
- gitter_notify_success
- store_test_results: *store_test_results
- store_artifacts: *artifacts_test_results
@ -644,7 +666,8 @@ jobs:
- /usr/local/Homebrew
- run: *run_build
- store_artifacts: *artifacts_solc
- store_artifacts: *artifacts_tools
- store_artifacts: *artifact_solidity_upgrade
- store_artifacts: *artifact_yul_phaser
- persist_to_workspace:
root: .
paths:
@ -807,7 +830,7 @@ jobs:
- when:
condition: true
<<: *steps_soltest
- run: *gitter_notify_failure
- gitter_notify_failure
t_ubu_ubsan_clang_cli:
docker:
@ -816,7 +839,7 @@ jobs:
- when:
condition: true
<<: *steps_cmdline_tests
- run: *gitter_notify_failure
- gitter_notify_failure
t_ems_solcjs:
docker:
@ -840,6 +863,32 @@ jobs:
npm --version
test/externalTests/solc-js/solc-js.sh /tmp/workspace/soljson.js $(cat /tmp/workspace/version.txt)
t_ems_ext_hardhat:
docker:
- image: circleci/node
environment:
TERM: xterm
HARDHAT_TESTS_SOLC_PATH: /tmp/workspace/soljson.js
steps:
- checkout
- attach_workspace:
at: /tmp/workspace
- run: git clone --depth 1 https://github.com/nomiclabs/hardhat.git
- run:
name: Install dependencies
command: |
cd hardhat
yarn
- run:
name: Run hardhat-core test suite
command: |
HARDHAT_TESTS_SOLC_VERSION=$(scripts/get_version.sh)
export HARDHAT_TESTS_SOLC_VERSION
# NOTE: This is expected to work without running `yarn build` first.
cd hardhat/packages/hardhat-core
yarn test
t_ems_ext:
parameters:
project:
@ -874,8 +923,8 @@ jobs:
- when:
condition: <<parameters.gitter_notify>>
steps:
- run: *gitter_notify_failure
- run: *gitter_notify_success
- gitter_notify_failure
- gitter_notify_success
b_win: &b_win
executor:
@ -1110,6 +1159,7 @@ workflows:
# Emscripten build and tests that take 15 minutes or less
- b_ems: *workflow_trigger_on_tags
- t_ems_solcjs: *workflow_emscripten
- t_ems_ext_hardhat: *workflow_emscripten
- t_ems_ext:
<<: *workflow_emscripten

10
Changelog.md
View File

@ -16,23 +16,29 @@ Language Features:
Compiler Features:
* Commandline Interface: Accept nested brackets in step sequences passed to ``--yul-optimizations``.
* Commandline Interface: Add ``--debug-info`` option for selecting how much extra debug information should be included in the produced EVM assembly and Yul code.
* Commandline Interface: Use different colors when printing errors, warnings and infos.
* SMTChecker: Output values for ``block.*``, ``msg.*`` and ``tx.*`` variables that are present in the called functions.
* SMTChecker: Report contract invariants and reentrancy properties. This can be enabled via the CLI option ``--model-checker-invariants`` or the Standard JSON option ``settings.modelChecker.invariants``.
* Standard JSON: Accept nested brackets in step sequences passed to ``settings.optimizer.details.yulDetails.optimizerSteps``.
* Standard JSON: Add ``settings.debug.debugInfo`` option for selecting how much extra debug information should be included in the produced EVM assembly and Yul code.
Bugfixes:
* Code Generator: Fix constructor source mappings for immutables.
* Commandline Interface: Disallow ``--error-recovery`` option outside of the compiler mode.
* Commandline Interface: Don't return zero exit code when writing linked files to disk fails.
* Commandline Interface: Fix extra newline character being appended to sources passed through standard input, affecting their hashes.
* Commandline Interface: Report output selection options unsupported by the selected input mode instead of ignoring them.
* Commandline Interface: Don't return zero exit code when writing linked files to disk fails.
* Commandline Interface: When linking only accept exact matches for library names passed to the ``--libraries`` option. Library names not prefixed with a file name used to match any library with that name.
* SMTChecker: Fix internal error in magic type access (``block``, ``msg``, ``tx``).
* TypeChecker: Fix internal error when using user defined value types in public library functions.
* TypeChecker: Fix internal error when using arrays and structs with user defined value types before declaration.
* TypeChecker: Improved error message for constant variables with (nested) mapping types.
* Yul Assembler: Fix internal error when function names are not unique.
* Yul IR Generator: Do not output empty switches/if-bodies for empty contracts.
### 0.8.9 (2021-09-29)
Important Bugfixes:

2
docs/contributing.rst
View File

@ -212,7 +212,7 @@ editing of failing contracts using your preferred text editor. Let's try to brea
// ----
// DeclarationError: (36-52): Identifier already declared.
Running ``./build/test/isoltest`` again results in a test failure:
Running ``./build/test/tools/isoltest`` again results in a test failure:
.. code-block:: text

2
docs/control-structures.rst
View File

@ -288,7 +288,7 @@ which only need to be created if there is a dispute.
re-created at the same address after having been destroyed. Yet, it is possible
for that newly created contract to have a different deployed bytecode even
though the creation bytecode has been the same (which is a requirement because
otherwise the address would change). This is due to the fact that the compiler
otherwise the address would change). This is due to the fact that the constructor
can query external state that might have changed between the two creations
and incorporate that into the deployed bytecode before it is stored.

2
docs/index.rst
View File

@ -18,7 +18,7 @@ and multi-signature wallets.
When deploying contracts, you should use the latest released
version of Solidity. Apart from exceptional cases, only the latest version receives
`security fixes<https://github.com/ethereum/solidity/security/policy#supported-versions>`.
`security fixes <https://github.com/ethereum/solidity/security/policy#supported-versions>`_.
Furthermore, breaking changes as well as
new features are introduced regularly. We currently use
a 0.x version number `to indicate this fast pace of change <https://semver.org/#spec-item-4>`_.

2
docs/ir/ir-breaking-changes.rst
View File

@ -268,7 +268,7 @@ In the new code generator, function pointers use the AST IDs of the functions as
calls through function pointers always have to use an internal dispatch function that uses the ``switch`` statement to select
the right function.
The ID ``0`` is reserved for uninitialized function pointers which then cause a panic in the disptach function when called.
The ID ``0`` is reserved for uninitialized function pointers which then cause a panic in the dispatch function when called.
In the old code generator, internal function pointers are initialized with a special function that always causes a panic.
This causes a storage write at construction time for internal function pointers in storage.

19
docs/smtchecker.rst
View File

@ -412,7 +412,7 @@ is already "locked", so it would not be possible to change the value of ``x``,
regardless of what the unknown called code does.
If we "forget" to use the ``mutex`` modifier on function ``set``, the
SMTChecker is able to synthesize the behavior of the externally called code so
SMTChecker is able to synthesize the behaviour of the externally called code so
that the assertion fails:
.. code-block:: text
@ -518,6 +518,23 @@ which has the following form:
"source2.sol": ["contract2", "contract3"]
}
Reported Inferred Inductive Invariants
======================================
For properties that were proved safe with the CHC engine,
the SMTChecker can retrieve inductive invariants that were inferred by the Horn
solver as part of the proof.
Currently two types of invariants can be reported to the user:
- Contract Invariants: these are properties over the contract's state variables
that are true before and after every possible transaction that the contract may ever run. For example, ``x >= y``, where ``x`` and ``y`` are a contract's state variables.
- Reentrancy Properties: they represent the behavior of the contract
in the presence of external calls to unknown code. These properties can express a relation
between the value of the state variables before and after the external call, where the external call is free to do anything, including making reentrant calls to the analyzed contract. Primed variables represent the state variables' values after said external call. Example: ``lock -> x = x'``.
The user can choose the type of invariants to be reported using the CLI option ``--model-checker-invariants "contract,reentrancy"`` or as an array in the field ``settings.modelChecker.invariants`` in the :ref:`JSON input<compiler-api>`.
By default the SMTChecker does not report invariants.
Division and Modulo With Slack Variables
========================================

2
docs/using-the-compiler.rst
View File

@ -417,6 +417,8 @@ Input Description
"divModWithSlacks": true,
// Choose which model checker engine to use: all (default), bmc, chc, none.
"engine": "chc",
// Choose which types of invariants should be reported to the user: contract, reentrancy.
"invariants": ["contract", "reentrancy"],
// Choose whether to output all unproved targets. The default is `false`.
"showUnproved": true,
// Choose which solvers should be used, if available.

11
docs/yul.rst
View File

@ -959,10 +959,13 @@ to ``loadimmutable("name")`` in the runtime code.
linkersymbol
^^^^^^^^^^^^
The function ``linkersymbol("fq_library_name")`` is a placeholder for an address literal to be
substituted by the linker. Its first and only argument must be a string literal and represents the
fully qualified library name used with the ``--libraries`` option.
The function ``linkersymbol("library_id")`` is a placeholder for an address literal to be substituted
by the linker.
Its first and only argument must be a string literal and uniquely represents the address to be inserted.
Identifiers can be arbitrary but when the compiler produces Yul code from Solidity sources,
it uses a library name qualified with the name of the source unit that defines that library.
To link the code with a particular library address, the same identifier must be provided to the
``--libraries`` option on the command line.
For example this code

8
libevmasm/LinkerObject.cpp
View File

@ -73,14 +73,6 @@ LinkerObject::matchLibrary(
)
{
auto it = _libraryAddresses.find(_linkRefName);
if (it != _libraryAddresses.end())
return &it->second;
// If the user did not supply a fully qualified library name,
// try to match only the simple library name
size_t colon = _linkRefName.find(':');
if (colon == string::npos)
return nullptr;
it = _libraryAddresses.find(_linkRefName.substr(colon + 1));
if (it != _libraryAddresses.end())
return &it->second;
return nullptr;

5
liblangutil/ErrorReporter.cpp
View File

@ -261,3 +261,8 @@ void ErrorReporter::info(
{
error(_error, Error::Type::Info, _location, _description);
}
void ErrorReporter::info(ErrorId _error, string const& _description)
{
error(_error, Error::Type::Info, SourceLocation(), _description);
}

2
liblangutil/ErrorReporter.h
View File

@ -72,6 +72,8 @@ public:
std::string const& _description
);
void info(ErrorId _error, std::string const& _description);
void declarationError(
ErrorId _error,
SourceLocation const& _location,

15
liblangutil/Exceptions.cpp
View File

@ -23,6 +23,9 @@
#include <liblangutil/Exceptions.h>
#include <boost/algorithm/string/case_conv.hpp>
#include <boost/algorithm/string/trim.hpp>
using namespace std;
using namespace solidity;
using namespace solidity::langutil;
@ -71,3 +74,15 @@ Error::Error(
if (!_description.empty())
*this << util::errinfo_comment(_description);
}
optional<Error::Severity> Error::severityFromString(string _input)
{
boost::algorithm::to_lower(_input);
boost::algorithm::trim(_input);
for (Severity severity: {Severity::Error, Severity::Warning, Severity::Info})
if (_input == formatErrorSeverityLowercase(severity))
return severity;
return nullopt;
}

2
liblangutil/Exceptions.h
View File

@ -258,6 +258,8 @@ public:
solAssert(false, "");
}
static std::optional<Severity> severityFromString(std::string _input);
private:
ErrorId m_errorId;
Type m_type;

21
liblangutil/SourceReferenceFormatter.cpp
View File

@ -65,9 +65,21 @@ AnsiColorized SourceReferenceFormatter::frameColored() const
return AnsiColorized(m_stream, m_colored, {BOLD, BLUE});
}
AnsiColorized SourceReferenceFormatter::errorColored() const
AnsiColorized SourceReferenceFormatter::errorColored(optional<Error::Severity> _severity) const
{
return AnsiColorized(m_stream, m_colored, {BOLD, RED});
// We used to color messages of any severity as errors so this seems like a good default
// for cases where severity cannot be determined.
char const* textColor = RED;
if (_severity.has_value())
switch (_severity.value())
{
case Error::Severity::Error: textColor = RED; break;
case Error::Severity::Warning: textColor = YELLOW; break;
case Error::Severity::Info: textColor = WHITE; break;
}
return AnsiColorized(m_stream, m_colored, {BOLD, textColor});
}
AnsiColorized SourceReferenceFormatter::messageColored() const
@ -164,9 +176,10 @@ void SourceReferenceFormatter::printSourceLocation(SourceReference const& _ref)
void SourceReferenceFormatter::printExceptionInformation(SourceReferenceExtractor::Message const& _msg)
{
// exception header line
errorColored() << _msg.severity;
optional<Error::Severity> severity = Error::severityFromString(_msg.severity);
errorColored(severity) << _msg.severity;
if (m_withErrorIds && _msg.errorId.has_value())
errorColored() << " (" << _msg.errorId.value().error << ")";
errorColored(severity) << " (" << _msg.errorId.value().error << ")";
messageColored() << ": " << _msg.primary.message << '\n';
printSourceLocation(_msg.primary);

2
liblangutil/SourceReferenceFormatter.h
View File

@ -87,7 +87,7 @@ public:
private:
util::AnsiColorized normalColored() const;
util::AnsiColorized frameColored() const;
util::AnsiColorized errorColored() const;
util::AnsiColorized errorColored(std::optional<langutil::Error::Severity> _severity) const;
util::AnsiColorized messageColored() const;
util::AnsiColorized secondaryColored() const;
util::AnsiColorized highlightColored() const;

14
liblangutil/UniqueErrorReporter.h
View File

@ -61,6 +61,20 @@ public:
m_errorReporter.warning(_error, _description);
}
void info(ErrorId _error, SourceLocation const& _location, std::string const& _description)
{
if (!seen(_error, _location, _description))
{
m_errorReporter.info(_error, _location, _description);
markAsSeen(_error, _location, _description);
}
}
void info(ErrorId _error, std::string const& _description)
{
m_errorReporter.info(_error, _description);
}
bool seen(ErrorId _error, SourceLocation const& _location, std::string const& _description) const
{
if (m_seenErrors.count({_error, _location}))

5
libsmtutil/CHCSmtLib2Interface.cpp
View File

@ -87,7 +87,7 @@ void CHCSmtLib2Interface::addRule(Expression const& _expr, std::string const& /*
);
}
pair<CheckResult, CHCSolverInterface::CexGraph> CHCSmtLib2Interface::query(Expression const& _block)
tuple<CheckResult, Expression, CHCSolverInterface::CexGraph> CHCSmtLib2Interface::query(Expression const& _block)
{
string accumulated{};
swap(m_accumulatedOutput, accumulated);
@ -118,8 +118,7 @@ pair<CheckResult, CHCSolverInterface::CexGraph> CHCSmtLib2Interface::query(Expre
else
result = CheckResult::ERROR;
// TODO collect invariants or counterexamples.
return {result, {}};
return {result, Expression(true), {}};
}
void CHCSmtLib2Interface::declareVariable(string const& _name, SortPointer const& _sort)

4
libsmtutil/CHCSmtLib2Interface.h
View File

@ -44,7 +44,9 @@ public:
void addRule(Expression const& _expr, std::string const& _name) override;
std::pair<CheckResult, CexGraph> query(Expression const& _expr) override;
/// Takes a function application _expr and checks for reachability.
/// @returns solving result, an invariant, and counterexample graph, if possible.
std::tuple<CheckResult, Expression, CexGraph> query(Expression const& _expr) override;
void declareVariable(std::string const& _name, SortPointer const& _sort) override;

4
libsmtutil/CHCSolverInterface.h
View File

@ -54,8 +54,8 @@ public:
};
/// Takes a function application _expr and checks for reachability.
/// @returns solving result and a counterexample graph, if possible.
virtual std::pair<CheckResult, CexGraph> query(
/// @returns solving result, an invariant, and counterexample graph, if possible.
virtual std::tuple<CheckResult, Expression, CexGraph> query(
Expression const& _expr
) = 0;

60
libsmtutil/SolverInterface.h
View File

@ -23,7 +23,9 @@
#include <libsolutil/Common.h>
#include <libsolutil/Numeric.h>
#include <libsolutil/CommonData.h>
#include <range/v3/algorithm/all_of.hpp>
#include <range/v3/view.hpp>
#include <cstdio>
@ -305,6 +307,64 @@ public:
);
}
static bool sameSort(std::vector<Expression> const& _args)
{
if (_args.empty())
return true;
auto sort = _args.front().sort;
return ranges::all_of(
_args,
[&](auto const& _expr){ return _expr.sort->kind == sort->kind; }
);
}
static Expression mkAnd(std::vector<Expression> _args)
{
smtAssert(!_args.empty(), "");
smtAssert(sameSort(_args), "");
auto sort = _args.front().sort;
if (sort->kind == Kind::BitVector)
return Expression("bvand", std::move(_args), sort);
smtAssert(sort->kind == Kind::Bool, "");
return Expression("and", std::move(_args), Kind::Bool);
}
static Expression mkOr(std::vector<Expression> _args)
{
smtAssert(!_args.empty(), "");
smtAssert(sameSort(_args), "");
auto sort = _args.front().sort;
if (sort->kind == Kind::BitVector)
return Expression("bvor", std::move(_args), sort);
smtAssert(sort->kind == Kind::Bool, "");
return Expression("or", std::move(_args), Kind::Bool);
}
static Expression mkPlus(std::vector<Expression> _args)
{
smtAssert(!_args.empty(), "");
smtAssert(sameSort(_args), "");
auto sort = _args.front().sort;
smtAssert(sort->kind == Kind::BitVector || sort->kind == Kind::Int, "");
return Expression("+", std::move(_args), sort);
}
static Expression mkMul(std::vector<Expression> _args)
{
smtAssert(!_args.empty(), "");
smtAssert(sameSort(_args), "");
auto sort = _args.front().sort;
smtAssert(sort->kind == Kind::BitVector || sort->kind == Kind::Int, "");
return Expression("*", std::move(_args), sort);
}
friend Expression operator!(Expression _a)
{
if (_a.sort->kind == Kind::BitVector)

10
libsmtutil/Z3CHCInterface.cpp
View File

@ -77,7 +77,7 @@ void Z3CHCInterface::addRule(Expression const& _expr, string const& _name)
}
}
pair<CheckResult, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression const& _expr)
tuple<CheckResult, Expression, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression const& _expr)
{
CheckResult result;
try
@ -93,15 +93,15 @@ pair<CheckResult, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression
if (m_version >= tuple(4, 8, 8, 0))
{
auto proof = m_solver.get_answer();
return {result, cexGraph(proof)};
return {result, Expression(true), cexGraph(proof)};
}
break;
}
case z3::check_result::unsat:
{
result = CheckResult::UNSATISFIABLE;
// TODO retrieve invariants.
break;
auto invariants = m_z3Interface->fromZ3Expr(m_solver.get_answer());
return {result, move(invariants), {}};
}
case z3::check_result::unknown:
{
@ -125,7 +125,7 @@ pair<CheckResult, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression
result = CheckResult::ERROR;
}
return {result, {}};
return {result, Expression(true), {}};
}
void Z3CHCInterface::setSpacerOptions(bool _preProcessing)

2
libsmtutil/Z3CHCInterface.h
View File

@ -43,7 +43,7 @@ public:
void addRule(Expression const& _expr, std::string const& _name) override;
std::pair<CheckResult, CexGraph> query(Expression const& _expr) override;
std::tuple<CheckResult, Expression, CexGraph> query(Expression const& _expr) override;
Z3Interface* z3Interface() const { return m_z3Interface.get(); }

46
libsmtutil/Z3Interface.cpp
View File

@ -279,6 +279,19 @@ Expression Z3Interface::fromZ3Expr(z3::expr const& _expr)
if (_expr.is_const() || _expr.is_var())
return Expression(_expr.to_string(), {}, sort);
if (_expr.is_quantifier())
{
string quantifierName;
if (_expr.is_exists())
quantifierName = "exists";
else if (_expr.is_forall())
quantifierName = "forall";
else if (_expr.is_lambda())
quantifierName = "lambda";
else
smtAssert(false, "");
return Expression(quantifierName, {fromZ3Expr(_expr.body())}, sort);
}
smtAssert(_expr.is_app(), "");
vector<Expression> arguments;
for (unsigned i = 0; i < _expr.num_args(); ++i)
@ -290,33 +303,44 @@ Expression Z3Interface::fromZ3Expr(z3::expr const& _expr)
else if (_expr.is_not())
return !arguments[0];
else if (_expr.is_and())
return arguments[0] && arguments[1];
return Expression::mkAnd(arguments);
else if (_expr.is_or())
return arguments[0] || arguments[1];
return Expression::mkOr(arguments);
else if (_expr.is_implies())
return Expression::implies(arguments[0], arguments[1]);
else if (_expr.is_eq())
{
smtAssert(arguments.size() == 2, "");
return arguments[0] == arguments[1];
}
else if (kind == Z3_OP_ULT || kind == Z3_OP_SLT)
return arguments[0] < arguments[1];
else if (kind == Z3_OP_ULEQ || kind == Z3_OP_SLEQ)
else if (kind == Z3_OP_LE || kind == Z3_OP_ULEQ || kind == Z3_OP_SLEQ)
return arguments[0] <= arguments[1];
else if (kind == Z3_OP_GT || kind == Z3_OP_SGT)
return arguments[0] > arguments[1];
else if (kind == Z3_OP_UGEQ || kind == Z3_OP_SGEQ)
else if (kind == Z3_OP_GE || kind == Z3_OP_UGEQ || kind == Z3_OP_SGEQ)
return arguments[0] >= arguments[1];
else if (kind == Z3_OP_ADD)
return arguments[0] + arguments[1];
return Expression::mkPlus(arguments);
else if (kind == Z3_OP_SUB)
{
smtAssert(arguments.size() == 2, "");
return arguments[0] - arguments[1];
}
else if (kind == Z3_OP_MUL)
return arguments[0] * arguments[1];
return Expression::mkMul(arguments);
else if (kind == Z3_OP_DIV)
{
smtAssert(arguments.size() == 2, "");
return arguments[0] / arguments[1];
}
else if (kind == Z3_OP_MOD)
return arguments[0] % arguments[1];
else if (kind == Z3_OP_XOR)
return arguments[0] ^ arguments[1];
else if (kind == Z3_OP_BNOT)
return !arguments[0];
else if (kind == Z3_OP_BSHL)
return arguments[0] << arguments[1];
else if (kind == Z3_OP_BLSHR)
@ -324,9 +348,11 @@ Expression Z3Interface::fromZ3Expr(z3::expr const& _expr)
else if (kind == Z3_OP_BASHR)
return Expression::ashr(arguments[0], arguments[1]);
else if (kind == Z3_OP_INT2BV)
smtAssert(false, "");
return Expression::int2bv(arguments[0], _expr.get_sort().bv_size());
else if (kind == Z3_OP_BV2INT)
smtAssert(false, "");
return Expression::bv2int(arguments[0]);
else if (kind == Z3_OP_EXTRACT)
return Expression("extract", arguments, sort);
else if (kind == Z3_OP_SELECT)
return Expression::select(arguments[0], arguments[1]);
else if (kind == Z3_OP_STORE)
@ -342,7 +368,9 @@ Expression Z3Interface::fromZ3Expr(z3::expr const& _expr)
return Expression::tuple_constructor(Expression(sortSort), arguments);
}
else if (kind == Z3_OP_DT_ACCESSOR)
smtAssert(false, "");
return Expression("dt_accessor_" + _expr.decl().name().str(), arguments, sort);
else if (kind == Z3_OP_DT_IS)
return Expression("dt_is", {arguments.at(0)}, sort);
else if (kind == Z3_OP_UNINTERPRETED)
return Expression(_expr.decl().name().str(), arguments, fromZ3Sort(_expr.get_sort()));

4
libsolidity/CMakeLists.txt
View File

@ -108,6 +108,10 @@ set(sources
formal/CHC.h
formal/EncodingContext.cpp
formal/EncodingContext.h
formal/ExpressionFormatter.cpp
formal/ExpressionFormatter.h
formal/Invariants.cpp
formal/Invariants.h
formal/ModelChecker.cpp
formal/ModelChecker.h
formal/ModelCheckerSettings.cpp

20
libsolidity/analysis/DeclarationTypeChecker.cpp
View File

@ -100,7 +100,6 @@ bool DeclarationTypeChecker::visit(StructDefinition const& _struct)
m_recursiveStructSeen = false;
member->accept(*this);
solAssert(member->annotation().type, "");
solAssert(member->annotation().type->canBeStored(), "Type cannot be used in struct.");
if (m_recursiveStructSeen)
hasRecursiveChild = true;
}
@ -289,7 +288,6 @@ void DeclarationTypeChecker::endVisit(ArrayTypeName const& _typeName)
return;
}
solAssert(baseType->storageBytes() != 0, "Illegal base type of storage size zero for array.");
if (Expression const* length = _typeName.length())
{
optional<rational> lengthValue;
@ -439,14 +437,16 @@ void DeclarationTypeChecker::endVisit(VariableDeclaration const& _variable)
type = TypeProvider::withLocation(ref, typeLoc, isPointer);
}
if (_variable.isConstant() && !type->isValueType())
{
bool allowed = false;
if (auto arrayType = dynamic_cast<ArrayType const*>(type))
allowed = arrayType->isByteArray();
if (!allowed)
m_errorReporter.fatalDeclarationError(9259_error, _variable.location(), "Constants of non-value type not yet implemented.");
}
if (
_variable.isConstant() &&
!dynamic_cast<UserDefinedValueType const*>(type) &&
type->containsNestedMapping()
)
m_errorReporter.fatalDeclarationError(
3530_error,
_variable.location(),
"The type contains a (nested) mapping and therefore cannot be a constant."
);
_variable.annotation().type = type;
}

27
libsolidity/analysis/TypeChecker.cpp
View File

@ -530,6 +530,15 @@ bool TypeChecker::visit(VariableDeclaration const& _variable)
}
if (_variable.isConstant())
{
if (!varType->isValueType())
{
bool allowed = false;
if (auto arrayType = dynamic_cast<ArrayType const*>(varType))
allowed = arrayType->isByteArray();
if (!allowed)
m_errorReporter.fatalTypeError(9259_error, _variable.location(), "Constants of non-value type not yet implemented.");
}
if (!_variable.value())
m_errorReporter.typeError(4266_error, _variable.location(), "Uninitialized \"constant\" variable.");
else if (!*_variable.value()->annotation().isPure)
@ -621,6 +630,16 @@ bool TypeChecker::visit(VariableDeclaration const& _variable)
return false;
}
void TypeChecker::endVisit(StructDefinition const& _struct)
{
for (auto const& member: _struct.members())
solAssert(
member->annotation().type &&
member->annotation().type->canBeStored(),
"Type cannot be used in struct."
);
}
void TypeChecker::visitManually(
ModifierInvocation const& _modifier,
vector<ContractDefinition const*> const& _bases
@ -1213,6 +1232,14 @@ void TypeChecker::endVisit(RevertStatement const& _revert)
m_errorReporter.typeError(1885_error, errorCall.expression().location(), "Expression has to be an error.");
}
void TypeChecker::endVisit(ArrayTypeName const& _typeName)
{
solAssert(
_typeName.baseType().annotation().type &&
_typeName.baseType().annotation().type->storageBytes() != 0,
"Illegal base type of storage size zero for array."
);
}
bool TypeChecker::visit(VariableDeclarationStatement const& _statement)
{

2
libsolidity/analysis/TypeChecker.h
View File

@ -119,7 +119,9 @@ private:
void endVisit(InheritanceSpecifier const& _inheritance) override;
void endVisit(ModifierDefinition const& _modifier) override;
bool visit(FunctionDefinition const& _function) override;
void endVisit(ArrayTypeName const& _typeName) override;
bool visit(VariableDeclaration const& _variable) override;
void endVisit(StructDefinition const& _struct) override;
/// We need to do this manually because we want to pass the bases of the current contract in
/// case this is a base constructor call.
void visitManually(ModifierInvocation const& _modifier, std::vector<ContractDefinition const*> const& _bases);

2
libsolidity/ast/Types.h
View File

@ -1124,6 +1124,8 @@ public:
bool containsNestedMapping() const override
{
solAssert(nameable(), "Called for a non nameable type.");
// DeclarationTypeChecker::endVisit(VariableDeclaration const&)
// assumes that this will never be true.
solAssert(!underlyingType().containsNestedMapping(), "");
return false;
}

82
libsolidity/formal/CHC.cpp
View File

@ -23,6 +23,7 @@
#endif
#include <libsolidity/formal/ArraySlicePredicate.h>
#include <libsolidity/formal/Invariants.h>
#include <libsolidity/formal/PredicateInstance.h>
#include <libsolidity/formal/PredicateSort.h>
#include <libsolidity/formal/SymbolicTypes.h>
@ -30,17 +31,20 @@
#include <libsolidity/ast/TypeProvider.h>
#include <libsmtutil/CHCSmtLib2Interface.h>
#include <liblangutil/CharStreamProvider.h>
#include <libsolutil/Algorithms.h>
#include <range/v3/algorithm/for_each.hpp>
#include <range/v3/view/enumerate.hpp>
#include <range/v3/view/reverse.hpp>
#ifdef HAVE_Z3_DLOPEN
#include <z3_version.h>
#endif
#include <boost/algorithm/string.hpp>
#include <range/v3/algorithm/for_each.hpp>
#include <range/v3/view.hpp>
#include <range/v3/view/enumerate.hpp>
#include <range/v3/view/reverse.hpp>
#include <charconv>
#include <queue>
@ -971,6 +975,7 @@ void CHC::resetSourceAnalysis()
m_safeTargets.clear();
m_unsafeTargets.clear();
m_unprovedTargets.clear();
m_invariants.clear();
m_functionTargetIds.clear();
m_verificationTargets.clear();
m_queryPlaceholders.clear();
@ -1128,8 +1133,8 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
if (auto const* contract = dynamic_cast<ContractDefinition const*>(node.get()))
{
string suffix = contract->name() + "_" + to_string(contract->id());
m_interfaces[contract] = createSymbolicBlock(interfaceSort(*contract, state()), "interface_" + uniquePrefix() + "_" + suffix, PredicateType::Interface, contract);
m_nondetInterfaces[contract] = createSymbolicBlock(nondetInterfaceSort(*contract, state()), "nondet_interface_" + uniquePrefix() + "_" + suffix, PredicateType::NondetInterface, contract);
m_interfaces[contract] = createSymbolicBlock(interfaceSort(*contract, state()), "interface_" + uniquePrefix() + "_" + suffix, PredicateType::Interface, contract, contract);
m_nondetInterfaces[contract] = createSymbolicBlock(nondetInterfaceSort(*contract, state()), "nondet_interface_" + uniquePrefix() + "_" + suffix, PredicateType::NondetInterface, contract, contract);
m_constructorSummaries[contract] = createConstructorBlock(*contract, "summary_constructor");
for (auto const* var: stateVariablesIncludingInheritedAndPrivate(*contract))
@ -1527,11 +1532,12 @@ void CHC::addRule(smtutil::Expression const& _rule, string const& _ruleName)
m_interface->addRule(_rule, _ruleName);
}
pair<CheckResult, CHCSolverInterface::CexGraph> CHC::query(smtutil::Expression const& _query, langutil::SourceLocation const& _location)
tuple<CheckResult, smtutil::Expression, CHCSolverInterface::CexGraph> CHC::query(smtutil::Expression const& _query, langutil::SourceLocation const& _location)
{
CheckResult result;
smtutil::Expression invariant(true);
CHCSolverInterface::CexGraph cex;
tie(result, cex) = m_interface->query(_query);
tie(result, invariant, cex) = m_interface->query(_query);
switch (result)
{
case CheckResult::SATISFIABLE:
@ -1546,8 +1552,9 @@ pair<CheckResult, CHCSolverInterface::CexGraph> CHC::query(smtutil::Expression c
spacer->setSpacerOptions(false);
CheckResult resultNoOpt;
smtutil::Expression invariantNoOpt(true);
CHCSolverInterface::CexGraph cexNoOpt;
tie(resultNoOpt, cexNoOpt) = m_interface->query(_query);
tie(resultNoOpt, invariantNoOpt, cexNoOpt) = m_interface->query(_query);
if (resultNoOpt == CheckResult::SATISFIABLE)
cex = move(cexNoOpt);
@ -1568,7 +1575,7 @@ pair<CheckResult, CHCSolverInterface::CexGraph> CHC::query(smtutil::Expression c
m_errorReporter.warning(1218_error, _location, "CHC: Error trying to invoke SMT solver.");
break;
}
return {result, cex};
return {result, invariant, cex};
}
void CHC::verificationTargetEncountered(
@ -1715,6 +1722,47 @@ void CHC::checkVerificationTargets()
" Consider increasing the timeout per query."
);
if (!m_settings.invariants.invariants.empty())
{
string msg;
for (auto pred: m_invariants | ranges::views::keys)
{
ASTNode const* node = pred->programNode();
string what;
if (auto contract = dynamic_cast<ContractDefinition const*>(node))
what = contract->fullyQualifiedName();
else
solAssert(false, "");
string invType;
if (pred->type() == PredicateType::Interface)
invType = "Contract invariant(s)";
else if (pred->type() == PredicateType::NondetInterface)
invType = "Reentrancy property(ies)";
else
solAssert(false, "");
msg += invType + " for " + what + ":\n";
for (auto const& inv: m_invariants.at(pred))
msg += inv + "\n";
}
if (msg.find("<errorCode>") != string::npos)
{
set<unsigned> seenErrors;
msg += "<errorCode> = 0 -> no errors\n";
for (auto const& target: verificationTargets)
if (!seenErrors.count(target.errorId))
{
seenErrors.insert(target.errorId);
string loc = string(m_charStreamProvider.charStream(*target.errorNode->location().sourceName).text(target.errorNode->location()));
msg += "<errorCode> = " + to_string(target.errorId) + " -> " + ModelCheckerTargets::targetTypeToString.at(target.type) + " at " + loc + "\n";
}
}
if (!msg.empty())
m_errorReporter.info(1180_error, msg);
}
// There can be targets in internal functions that are not reachable from the external interface.
// These are safe by definition and are not even checked by the CHC engine, but this information
// must still be reported safe by the BMC engine.
@ -1748,9 +1796,19 @@ void CHC::checkAndReportTarget(
createErrorBlock();
connectBlocks(_target.value, error(), _target.constraints);
auto const& location = _target.errorNode->location();
auto const& [result, model] = query(error(), location);
auto [result, invariant, model] = query(error(), location);
if (result == CheckResult::UNSATISFIABLE)
{
m_safeTargets[_target.errorNode].insert(_target.type);
set<Predicate const*> predicates;
for (auto const* pred: m_interfaces | ranges::views::values)
predicates.insert(pred);
for (auto const* pred: m_nondetInterfaces | ranges::views::values)
predicates.insert(pred);
map<Predicate const*, set<string>> invariants = collectInvariants(invariant, predicates, m_settings.invariants);
for (auto pred: invariants | ranges::views::keys)
m_invariants[pred] += move(invariants.at(pred));
}
else if (result == CheckResult::SATISFIABLE)
{
solAssert(!_satMsg.empty(), "");

9
libsolidity/formal/CHC.h
View File

@ -245,9 +245,9 @@ private:
//@{
/// Adds Horn rule to the solver.
void addRule(smtutil::Expression const& _rule, std::string const& _ruleName);
/// @returns <true, empty> if query is unsatisfiable (safe).
/// @returns <false, model> otherwise.
std::pair<smtutil::CheckResult, smtutil::CHCSolverInterface::CexGraph> query(smtutil::Expression const& _query, langutil::SourceLocation const& _location);
/// @returns <true, invariant, empty> if query is unsatisfiable (safe).
/// @returns <false, Expression(true), model> otherwise.
std::tuple<smtutil::CheckResult, smtutil::Expression, smtutil::CHCSolverInterface::CexGraph> query(smtutil::Expression const& _query, langutil::SourceLocation const& _location);
void verificationTargetEncountered(ASTNode const* const _errorNode, VerificationTargetType _type, smtutil::Expression const& _errorCondition);
@ -378,6 +378,9 @@ private:
std::map<ASTNode const*, std::map<VerificationTargetType, ReportTargetInfo>, smt::EncodingContext::IdCompare> m_unsafeTargets;
/// Targets not proved.
std::map<ASTNode const*, std::map<VerificationTargetType, ReportTargetInfo>, smt::EncodingContext::IdCompare> m_unprovedTargets;
/// Inferred invariants.
std::map<Predicate const*, std::set<std::string>, PredicateCompare> m_invariants;
//@}
/// Control-flow.

184
libsolidity/formal/ExpressionFormatter.cpp Normal file
View File

@ -0,0 +1,184 @@
/*
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 <http://www.gnu.org/licenses/>.
*/
// SPDX-License-Identifier: GPL-3.0
#include <libsolidity/formal/ExpressionFormatter.h>
#include <libsolutil/Algorithms.h>
#include <libsolutil/CommonData.h>
#include <boost/algorithm/string.hpp>
#include <range/v3/algorithm/for_each.hpp>
#include <map>
#include <vector>
#include <string>
using namespace std;
using boost::algorithm::starts_with;
using namespace solidity;
using namespace solidity::util;
using namespace solidity::smtutil;
using namespace solidity::frontend::smt;
namespace solidity::frontend::smt
{
namespace
{
string formatDatatypeAccessor(smtutil::Expression const& _expr, vector<string> const& _args)
{
auto const& op = _expr.name;
// This is the most complicated part of the translation.
// Datatype accessor means access to a field of a datatype.
// In our encoding, datatypes are used to encode:
// - arrays/mappings as the tuple (array, length)
// - structs as the tuple (<member1>, ..., <memberK>)
// - hash and signature functions as the tuple (keccak256, sha256, ripemd160, ecrecover),
// where each element is an array emulating an UF
// - abi.* functions as the tuple (<abiCall1>, ..., <abiCallK>).
if (op == "dt_accessor_keccak256")
return "keccak256";
if (op == "dt_accessor_sha256")
return "sha256";
if (op == "dt_accessor_ripemd160")
return "ripemd160";
if (op == "dt_accessor_ecrecover")
return "ecrecover";
string accessorStr = "accessor_";
// Struct members have suffix "accessor_<memberName>".
string type = op.substr(op.rfind(accessorStr) + accessorStr.size());
solAssert(_expr.arguments.size() == 1, "");
if (type == "length")
return _args.at(0) + ".length";
if (type == "array")
return _args.at(0);
if (
starts_with(type, "block") ||
starts_with(type, "msg") ||
starts_with(type, "tx") ||
starts_with(type, "abi")
)
return type;
if (starts_with(type, "t_function_abi"))
return type;
return _args.at(0) + "." + type;
}
string formatGenericOp(smtutil::Expression const& _expr, vector<string> const& _args)
{
return _expr.name + "(" + boost::algorithm::join(_args, ", ") + ")";
}
string formatInfixOp(string const& _op, vector<string> const& _args)
{
return "(" + boost::algorithm::join(_args, " " + _op + " ") + ")";
}
string formatArrayOp(smtutil::Expression const& _expr, vector<string> const& _args)
{
if (_expr.name == "select")
{
auto const& a0 = _args.at(0);
static set<string> const ufs{"keccak256", "sha256", "ripemd160", "ecrecover"};
if (ufs.count(a0) || starts_with(a0, "t_function_abi"))
return _args.at(0) + "(" + _args.at(1) + ")";
return _args.at(0) + "[" + _args.at(1) + "]";
}
if (_expr.name == "store")
return "(" + _args.at(0) + "[" + _args.at(1) + "] := " + _args.at(2) + ")";
return formatGenericOp(_expr, _args);
}
string formatUnaryOp(smtutil::Expression const& _expr, vector<string> const& _args)
{
if (_expr.name == "not")
return "!" + _args.at(0);
// Other operators such as exists may end up here.
return formatGenericOp(_expr, _args);
}
}
smtutil::Expression substitute(smtutil::Expression _from, map<string, string> const& _subst)
{
// TODO For now we ignore nested quantifier expressions,
// but we should support them in the future.
if (_from.name == "forall" || _from.name == "exists")
return smtutil::Expression(true);
if (_subst.count(_from.name))
_from.name = _subst.at(_from.name);
for (auto& arg: _from.arguments)
arg = substitute(arg, _subst);
return _from;
}
string toSolidityStr(smtutil::Expression const& _expr)
{
auto const& op = _expr.name;
auto const& args = _expr.arguments;
auto strArgs = util::applyMap(args, [](auto const& _arg) { return toSolidityStr(_arg); });
// Constant or variable.
if (args.empty())
return op;
if (starts_with(op, "dt_accessor"))
return formatDatatypeAccessor(_expr, strArgs);
// Infix operators with format replacements.
static map<string, string> const infixOps{
{"and", "&&"},
{"or", "||"},
{"implies", "=>"},
{"=", "="},
{">", ">"},
{">=", ">="},
{"<", "<"},
{"<=", "<="},
{"+", "+"},
{"-", "-"},
{"*", "*"},
{"/", "/"},
{"div", "/"},
{"mod", "%"}
};
// Some of these (and, or, +, *) may have >= 2 arguments from z3.
if (infixOps.count(op))
return formatInfixOp(infixOps.at(op), strArgs);
static set<string> const arrayOps{"select", "store", "const_array"};
if (arrayOps.count(op))
return formatArrayOp(_expr, strArgs);
if (args.size() == 1)
return formatUnaryOp(_expr, strArgs);
// Other operators such as bv2int, int2bv may end up here.
return op + "(" + boost::algorithm::join(strArgs, ", ") + ")";
}
}

41
libsolidity/formal/ExpressionFormatter.h Normal file
View File

@ -0,0 +1,41 @@
/*
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 <http://www.gnu.org/licenses/>.
*/
// SPDX-License-Identifier: GPL-3.0
#pragma once
/**
* Formats SMT expressions into Solidity-like strings.
*/
#include <libsolidity/formal/Predicate.h>
#include <map>
#include <string>
namespace solidity::frontend::smt
{
/// @returns another smtutil::Expressions where every term in _from
/// may be replaced if it is in the substitution map _subst.
smtutil::Expression substitute(smtutil::Expression _from, std::map<std::string, std::string> const& _subst);
/// @returns a Solidity-like expression string built from _expr.
/// This is done at best-effort and is not guaranteed to always create a perfect Solidity expression string.
std::string toSolidityStr(smtutil::Expression const& _expr);
}

86
libsolidity/formal/Invariants.cpp Normal file
View File

@ -0,0 +1,86 @@
/*
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 <http://www.gnu.org/licenses/>.
*/
// SPDX-License-Identifier: GPL-3.0
#include <libsolidity/formal/Invariants.h>
#include <libsolidity/formal/ExpressionFormatter.h>
#include <libsolidity/formal/SMTEncoder.h>
#include <libsolutil/Algorithms.h>
#include <boost/algorithm/string.hpp>
using namespace std;
using boost::algorithm::starts_with;
using namespace solidity;
using namespace solidity::smtutil;
using namespace solidity::frontend::smt;
namespace solidity::frontend::smt
{
map<Predicate const*, set<string>> collectInvariants(
smtutil::Expression const& _proof,
set<Predicate const*> const& _predicates,
ModelCheckerInvariants const& _invariantsSetting
)
{
set<string> targets;
if (_invariantsSetting.has(InvariantType::Contract))
targets.insert("interface_");
if (_invariantsSetting.has(InvariantType::Reentrancy))
targets.insert("nondet_interface_");
map<string, pair<smtutil::Expression, smtutil::Expression>> equalities;
// Collect equalities where one of the sides is a predicate we're interested in.
BreadthFirstSearch<smtutil::Expression const*>{{&_proof}}.run([&](auto&& _expr, auto&& _addChild) {
if (_expr->name == "=")
for (auto const& t: targets)
{
auto arg0 = _expr->arguments.at(0);
auto arg1 = _expr->arguments.at(1);
if (starts_with(arg0.name, t))
equalities.insert({arg0.name, {arg0, move(arg1)}});
else if (starts_with(arg1.name, t))
equalities.insert({arg1.name, {arg1, move(arg0)}});
}
for (auto const& arg: _expr->arguments)
_addChild(&arg);
});
map<Predicate const*, set<string>> invariants;
for (auto pred: _predicates)
{
auto predName = pred->functor().name;
if (!equalities.count(predName))
continue;
solAssert(pred->contextContract(), "");
auto const& [predExpr, invExpr] = equalities.at(predName);
static set<string> const ignore{"true", "false"};
auto r = substitute(invExpr, pred->expressionSubstitution(predExpr));
// No point in reporting true/false as invariants.
if (!ignore.count(r.name))
invariants[pred].insert(toSolidityStr(r));
}
return invariants;
}
}

37
libsolidity/formal/Invariants.h Normal file
View File

@ -0,0 +1,37 @@
/*
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 <http://www.gnu.org/licenses/>.
*/
// SPDX-License-Identifier: GPL-3.0
#pragma once
#include <libsolidity/formal/ModelCheckerSettings.h>
#include <libsolidity/formal/Predicate.h>
#include <map>
#include <set>
#include <string>
namespace solidity::frontend::smt
{
std::map<Predicate const*, std::set<std::string>> collectInvariants(
smtutil::Expression const& _proof,
std::set<Predicate const*> const& _predicates,
ModelCheckerInvariants const& _invariantsSettings
);
}

45
libsolidity/formal/ModelCheckerSettings.cpp
View File

@ -25,6 +25,40 @@ using namespace std;
using namespace solidity;
using namespace solidity::frontend;
map<string, InvariantType> const ModelCheckerInvariants::validInvariants{
{"contract", InvariantType::Contract},
{"reentrancy", InvariantType::Reentrancy}
};
std::optional<ModelCheckerInvariants> ModelCheckerInvariants::fromString(string const& _invs)
{
set<InvariantType> chosenInvs;
if (_invs == "default")
{
// The default is that no invariants are reported.
}
else if (_invs == "all")
for (auto&& v: validInvariants | ranges::views::values)
chosenInvs.insert(v);
else
for (auto&& t: _invs | ranges::views::split(',') | ranges::to<vector<string>>())
{
if (!validInvariants.count(t))
return {};
chosenInvs.insert(validInvariants.at(t));
}
return ModelCheckerInvariants{chosenInvs};
}
bool ModelCheckerInvariants::setFromString(string const& _inv)
{
if (!validInvariants.count(_inv))
return false;
invariants.insert(validInvariants.at(_inv));
return true;
}
using TargetType = VerificationTargetType;
map<string, TargetType> const ModelCheckerTargets::targetStrings{
{"constantCondition", TargetType::ConstantCondition},
@ -37,6 +71,17 @@ map<string, TargetType> const ModelCheckerTargets::targetStrings{
{"outOfBounds", TargetType::OutOfBounds}
};
map<TargetType, string> const ModelCheckerTargets::targetTypeToString{
{TargetType::ConstantCondition, "Constant condition"},
{TargetType::Underflow, "Underflow"},
{TargetType::Overflow, "Overflow"},
{TargetType::DivByZero, "Division by zero"},
{TargetType::Balance, "Insufficient balance"},
{TargetType::Assert, "Assertion failed"},
{TargetType::PopEmptyArray, "Empty array pop"},
{TargetType::OutOfBounds, "Out of bounds access"}
};
std::optional<ModelCheckerTargets> ModelCheckerTargets::fromString(string const& _targets)
{
set<TargetType> chosenTargets;

30
libsolidity/formal/ModelCheckerSettings.h
View File

@ -87,6 +87,32 @@ struct ModelCheckerEngine
bool operator==(ModelCheckerEngine const& _other) const noexcept { return bmc == _other.bmc && chc == _other.chc; }
};
enum class InvariantType { Contract, Reentrancy };
struct ModelCheckerInvariants
{
/// Adds the default targets, that is, all except underflow and overflow.
static ModelCheckerInvariants Default() { return *fromString("default"); }
/// Adds all targets, including underflow and overflow.
static ModelCheckerInvariants All() { return *fromString("all"); }
static ModelCheckerInvariants None() { return {{}}; }
static std::optional<ModelCheckerInvariants> fromString(std::string const& _invs);
bool has(InvariantType _inv) const { return invariants.count(_inv); }
/// @returns true if the @p _target is valid,
/// and false otherwise.
bool setFromString(std::string const& _target);
static std::map<std::string, InvariantType> const validInvariants;
bool operator!=(ModelCheckerInvariants const& _other) const noexcept { return !(*this == _other); }
bool operator==(ModelCheckerInvariants const& _other) const noexcept { return invariants == _other.invariants; }
std::set<InvariantType> invariants;
};
enum class VerificationTargetType { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert, PopEmptyArray, OutOfBounds };
struct ModelCheckerTargets
@ -106,6 +132,8 @@ struct ModelCheckerTargets
static std::map<std::string, VerificationTargetType> const targetStrings;
static std::map<VerificationTargetType, std::string> const targetTypeToString;
bool operator!=(ModelCheckerTargets const& _other) const noexcept { return !(*this == _other); }
bool operator==(ModelCheckerTargets const& _other) const noexcept { return targets == _other.targets; }
@ -123,6 +151,7 @@ struct ModelCheckerSettings
/// might prefer the precise encoding.
bool divModNoSlacks = false;
ModelCheckerEngine engine = ModelCheckerEngine::None();
ModelCheckerInvariants invariants = ModelCheckerInvariants::Default();
bool showUnproved = false;
smtutil::SMTSolverChoice solvers = smtutil::SMTSolverChoice::All();
ModelCheckerTargets targets = ModelCheckerTargets::Default();
@ -135,6 +164,7 @@ struct ModelCheckerSettings
contracts == _other.contracts &&
divModNoSlacks == _other.divModNoSlacks &&
engine == _other.engine &&
invariants == _other.invariants &&
showUnproved == _other.showUnproved &&
solvers == _other.solvers &&
targets == _other.targets &&

52
libsolidity/formal/Predicate.cpp
View File

@ -26,10 +26,13 @@
#include <libsolidity/ast/TypeProvider.h>
#include <boost/algorithm/string/join.hpp>
#include <boost/algorithm/string.hpp>
#include <range/v3/view.hpp>
#include <utility>
using namespace std;
using boost::algorithm::starts_with;
using namespace solidity;
using namespace solidity::smtutil;
using namespace solidity::frontend;
@ -198,6 +201,11 @@ bool Predicate::isInterface() const
return m_type == PredicateType::Interface;
}
bool Predicate::isNondetInterface() const
{
return m_type == PredicateType::NondetInterface;
}
string Predicate::formatSummaryCall(
vector<smtutil::Expression> const& _args,
langutil::CharStreamProvider const& _charStreamProvider,
@ -418,6 +426,50 @@ pair<vector<optional<string>>, vector<VariableDeclaration const*>> Predicate::lo
return {formatExpressions(outValuesInScope, outTypes), localVarsInScope};
}
map<string, string> Predicate::expressionSubstitution(smtutil::Expression const& _predExpr) const
{
map<string, string> subst;
string predName = functor().name;
solAssert(contextContract(), "");
auto const& stateVars = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*contextContract());
auto nArgs = _predExpr.arguments.size();
// The signature of an interface predicate is
// interface(this, abiFunctions, cryptoFunctions, blockchainState, stateVariables).
// An invariant for an interface predicate is a contract
// invariant over its state, for example `x <= 0`.
if (isInterface())
{
solAssert(starts_with(predName, "interface"), "");
subst[_predExpr.arguments.at(0).name] = "address(this)";
solAssert(nArgs == stateVars.size() + 4, "");
for (size_t i = nArgs - stateVars.size(); i < nArgs; ++i)
subst[_predExpr.arguments.at(i).name] = stateVars.at(i - 4)->name();
}
// The signature of a nondet interface predicate is
// nondet_interface(error, this, abiFunctions, cryptoFunctions, blockchainState, stateVariables, blockchainState', stateVariables').
// An invariant for a nondet interface predicate is a reentrancy property
// over the pre and post state variables of a contract, where pre state vars
// are represented by the variable's name and post state vars are represented
// by the primed variable's name, for example
// `(x <= 0) => (x' <= 100)`.
else if (isNondetInterface())
{
solAssert(starts_with(predName, "nondet_interface"), "");
subst[_predExpr.arguments.at(0).name] = "<errorCode>";
subst[_predExpr.arguments.at(1).name] = "address(this)";
solAssert(nArgs == stateVars.size() * 2 + 6, "");
for (size_t i = nArgs - stateVars.size(), s = 0; i < nArgs; ++i, ++s)
subst[_predExpr.arguments.at(i).name] = stateVars.at(s)->name() + "'";
for (size_t i = nArgs - (stateVars.size() * 2 + 1), s = 0; i < nArgs - (stateVars.size() + 1); ++i, ++s)
subst[_predExpr.arguments.at(i).name] = stateVars.at(s)->name();
}
return subst;
}
vector<optional<string>> Predicate::formatExpressions(vector<smtutil::Expression> const& _exprs, vector<Type const*> const& _types) const
{
solAssert(_exprs.size() == _types.size(), "");

21
libsolidity/formal/Predicate.h
View File

@ -21,6 +21,8 @@
#include <libsolidity/formal/SymbolicVariables.h>
#include <libsolidity/formal/SymbolicVariables.h>
#include <libsolidity/ast/AST.h>
#include <libsmtutil/Sorts.h>
#include <map>
@ -143,6 +145,9 @@ public:
/// @returns true if this predicate represents an interface.
bool isInterface() const;
/// @returns true if this predicate represents a nondeterministic interface.
bool isNondetInterface() const;
PredicateType type() const { return m_type; }
/// @returns a formatted string representing a call to this predicate
@ -168,6 +173,10 @@ public:
/// @returns the values of the local variables used by this predicate.
std::pair<std::vector<std::optional<std::string>>, std::vector<VariableDeclaration const*>> localVariableValues(std::vector<smtutil::Expression> const& _args) const;
/// @returns a substitution map from the arguments of _predExpr
/// to a Solidity-like expression.
std::map<std::string, std::string> expressionSubstitution(smtutil::Expression const& _predExpr) const;
private:
/// @returns the formatted version of the given SMT expressions. Those expressions must be SMT constants.
std::vector<std::optional<std::string>> formatExpressions(std::vector<smtutil::Expression> const& _exprs, std::vector<Type const*> const& _types) const;
@ -208,4 +217,16 @@ private:
std::vector<ScopeOpener const*> const m_scopeStack;
};
struct PredicateCompare
{
bool operator()(Predicate const* lhs, Predicate const* rhs) const
{
// We cannot use m_node->id() because different predicates may
// represent the same program node.
// We use the symbolic name since it is unique per predicate and
// the order does not really matter.
return lhs->functor().name < rhs->functor().name;
}
};
}

23
libsolidity/interface/StandardCompiler.cpp
View File

@ -445,7 +445,7 @@ std::optional<Json::Value> checkSettingsKeys(Json::Value const& _input)
std::optional<Json::Value> checkModelCheckerSettingsKeys(Json::Value const& _input)
{
static set<string> keys{"contracts", "divModNoSlacks", "engine", "showUnproved", "solvers", "targets", "timeout"};
static set<string> keys{"contracts", "divModNoSlacks", "engine", "invariants", "showUnproved", "solvers", "targets", "timeout"};
return checkKeys(_input, keys, "modelChecker");
}
@ -987,6 +987,27 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
ret.modelCheckerSettings.engine = *engine;
}
if (modelCheckerSettings.isMember("invariants"))
{
auto const& invariantsArray = modelCheckerSettings["invariants"];
if (!invariantsArray.isArray())
return formatFatalError("JSONError", "settings.modelChecker.invariants must be an array.");
ModelCheckerInvariants invariants;
for (auto const& i: invariantsArray)
{
if (!i.isString())
return formatFatalError("JSONError", "Every invariant type in settings.modelChecker.invariants must be a string.");
if (!invariants.setFromString(i.asString()))
return formatFatalError("JSONError", "Invalid model checker invariants requested.");
}
if (invariants.invariants.empty())
return formatFatalError("JSONError", "settings.modelChecker.invariants must be a non-empty array.");
ret.modelCheckerSettings.invariants = invariants;
}
if (modelCheckerSettings.isMember("showUnproved"))
{
auto const& showUnproved = modelCheckerSettings["showUnproved"];

3
libyul/ControlFlowSideEffectsCollector.cpp
View File

@ -212,7 +212,8 @@ ControlFlowSideEffectsCollector::ControlFlowSideEffectsCollector(
if (calledSideEffects->canRevert)
sideEffects.canRevert = true;
for (YulString callee: util::valueOrDefault(m_functionCalls, _function))
set<YulString> emptySet;
for (YulString callee: util::valueOrDefault(m_functionCalls, _function, emptySet))
_recurse(callee, _recurse);
};
for (auto const& call: calls)

4
libyul/backends/evm/AsmCodeGen.cpp
View File

@ -52,7 +52,9 @@ void CodeGenerator::assemble(
builtinContext,
_optimizeStackAllocation,
_identifierAccessCodeGen,
_useNamedLabelsForFunctions
_useNamedLabelsForFunctions ?
CodeTransform::UseNamedLabels::YesAndForceUnique :
CodeTransform::UseNamedLabels::Never
);
transform(_parsedData);
if (!transform.stackErrors().empty())

16
libyul/backends/evm/EVMCodeTransform.cpp
View File

@ -52,7 +52,7 @@ CodeTransform::CodeTransform(
EVMDialect const& _dialect,
BuiltinContext& _builtinContext,
ExternalIdentifierAccess::CodeGenerator _identifierAccessCodeGen,
bool _useNamedLabelsForFunctions,
UseNamedLabels _useNamedLabelsForFunctions,
shared_ptr<Context> _context,
vector<TypedName> _delayedReturnVariables,
optional<AbstractAssembly::LabelID> _functionExitLabel
@ -405,8 +405,12 @@ void CodeTransform::operator()(FunctionDefinition const& _function)
if (!m_allowStackOpt)
subTransform.setupReturnVariablesAndFunctionExit();
subTransform.m_assignedNamedLabels = move(m_assignedNamedLabels);
subTransform(_function.body);
m_assignedNamedLabels = move(subTransform.m_assignedNamedLabels);
m_assembly.setSourceLocation(originLocationOf(_function));
if (!subTransform.m_stackErrors.empty())
{
@ -585,8 +589,16 @@ void CodeTransform::createFunctionEntryID(FunctionDefinition const& _function)
if (_function.debugData)
astID = _function.debugData->astID;
bool nameAlreadySeen = !m_assignedNamedLabels.insert(_function.name).second;
if (m_useNamedLabelsForFunctions == UseNamedLabels::YesAndForceUnique)
yulAssert(!nameAlreadySeen);
m_context->functionEntryIDs[&scopeFunction] =
m_useNamedLabelsForFunctions ?
(
m_useNamedLabelsForFunctions != UseNamedLabels::Never &&
!nameAlreadySeen
) ?
m_assembly.namedLabel(
_function.name.str(),
_function.parameters.size(),

11
libyul/backends/evm/EVMCodeTransform.h
View File

@ -64,6 +64,10 @@ struct CodeTransformContext
class CodeTransform
{
public:
/// Use named labels for functions 1) Yes and check that the names are unique
/// 2) For none of the functions 3) for the first function of each name.
enum class UseNamedLabels { YesAndForceUnique, Never, ForFirstFunctionOfEachName };
/// Create the code transformer.
/// @param _identifierAccessCodeGen used to generate code for identifiers external to the inline assembly
/// As a side-effect of its construction, translates the Yul code and appends it to the
@ -78,7 +82,7 @@ public:
BuiltinContext& _builtinContext,
bool _allowStackOpt = false,
ExternalIdentifierAccess::CodeGenerator const& _identifierAccessCodeGen = {},
bool _useNamedLabelsForFunctions = false
UseNamedLabels _useNamedLabelsForFunctions = UseNamedLabels::Never
): CodeTransform(
_assembly,
_analysisInfo,
@ -108,7 +112,7 @@ protected:
EVMDialect const& _dialect,
BuiltinContext& _builtinContext,
ExternalIdentifierAccess::CodeGenerator _identifierAccessCodeGen,
bool _useNamedLabelsForFunctions,
UseNamedLabels _useNamedLabelsForFunctions,
std::shared_ptr<Context> _context,
std::vector<TypedName> _delayedReturnVariables,
std::optional<AbstractAssembly::LabelID> _functionExitLabel
@ -193,7 +197,8 @@ private:
EVMDialect const& m_dialect;
BuiltinContext& m_builtinContext;
bool const m_allowStackOpt = true;
bool const m_useNamedLabelsForFunctions = false;
UseNamedLabels const m_useNamedLabelsForFunctions = UseNamedLabels::Never;
std::set<YulString> m_assignedNamedLabels;
ExternalIdentifierAccess::CodeGenerator m_identifierAccessCodeGen;
std::shared_ptr<Context> m_context;

2
libyul/backends/evm/EVMObjectCompiler.cpp
View File

@ -72,7 +72,7 @@ void EVMObjectCompiler::run(Object& _object, bool _optimize)
context,
_optimize,
{},
true /* _useNamedLabelsForFunctions */
CodeTransform::UseNamedLabels::ForFirstFunctionOfEachName
};
transform(*_object.code);
if (!transform.stackErrors().empty())

74
scripts/common.sh
View File

@ -19,6 +19,13 @@
# (c) 2016-2019 solidity contributors.
# ------------------------------------------------------------------------------
# The fail() function defined below requires set -e to be enabled.
set -e
# Save the initial working directory so that printStackTrace() can access it even if the sourcing
# changes directory. The paths returned by `caller` are relative to it.
_initial_work_dir=$(pwd)
if [ "$CIRCLECI" ]
then
export TERM="${TERM:-xterm}"
@ -33,12 +40,63 @@ else
function printLog() { echo "$(tput setaf 3)$1$(tput sgr0)"; }
fi
function printStackTrace
{
printWarning ""
printWarning "Stack trace:"
local frame=1
while caller "$frame" > /dev/null
do
local lineNumber line file function
# `caller` returns something that could already be printed as a stacktrace but we can make
# it more readable by rearranging the components.
# NOTE: This assumes that paths do not contain spaces.
lineNumber=$(caller "$frame" | cut --delimiter " " --field 1)
function=$(caller "$frame" | cut --delimiter " " --field 2)
file=$(caller "$frame" | cut --delimiter " " --field 3)
# Paths in the output from `caller` can be relative or absolute (depends on how the path
# with which the script was invoked) and if they're relative, they're not necessarily
# relative to the current working dir. This is a heuristic that will work if they're absolute,
# relative to current dir, or relative to the dir that was current when the script started.
# If neither works, it gives up.
line=$(
{
tail "--lines=+${lineNumber}" "$file" ||
tail "--lines=+${lineNumber}" "${_initial_work_dir}/${file}"
} 2> /dev/null |
head --lines=1 |
sed -e 's/^[[:space:]]*//'
) || line="<failed to find source line>"
>&2 printf " %s:%d in function %s()\n" "$file" "$lineNumber" "$function"
>&2 printf " %s\n" "$line"
((frame++))
done
}
function fail()
{
printError "$@"
# Using return rather than exit lets the invoking code handle the failure by suppressing the exit code.
return 1
}
function assertFail()
{
printError ""
(( $# == 0 )) && printError "Assertion failed."
(( $# == 1 )) && printError "Assertion failed: $1"
printStackTrace
# Intentionally using exit here because assertion failures are not supposed to be handled.
exit 2
}
function msg_on_error()
{
local error_message
@ -67,7 +125,7 @@ function msg_on_error()
shift
;;
*)
fail "Invalid option for msg_on_error: $1"
assertFail "Invalid option for msg_on_error: $1"
;;
esac
done
@ -85,24 +143,30 @@ function msg_on_error()
rm "$stdout_file" "$stderr_file"
return 0
else
printError "Command failed: $SOLC ${command[*]}"
printError ""
printError "Command failed: ${error_message}"
printError " command: $SOLC ${command[*]}"
if [[ -s "$stdout_file" ]]
then
printError "stdout:"
printError "--- stdout ---"
printError "-----------"
>&2 cat "$stdout_file"
printError "--------------"
else
printError " stdout: <EMPTY>"
fi
if [[ -s "$stderr_file" ]]
then
printError "stderr:"
printError "--- stderr ---"
>&2 cat "$stderr_file"
printError "--------------"
else
printError " stderr: <EMPTY>"
fi
printError "$error_message"
rm "$stdout_file" "$stderr_file"
printStackTrace
return 1
fi
}

2
scripts/error_codes.py
View File

@ -125,7 +125,7 @@ def find_files(top_dir, sub_dirs, extensions):
def find_ids_in_test_file(file_name):
source = read_file(file_name)
pattern = r"^// (.*Error|Warning) \d\d\d\d:"
pattern = r"^// (.*Error|Warning|Info) \d\d\d\d:"
return {m.group(0)[-5:-1] for m in re.finditer(pattern, source, flags=re.MULTILINE)}

41
solc/CommandLineParser.cpp
View File

@ -78,6 +78,7 @@ static string const g_strMetadataLiteral = "metadata-literal";
static string const g_strModelCheckerContracts = "model-checker-contracts";
static string const g_strModelCheckerDivModNoSlacks = "model-checker-div-mod-no-slacks";
static string const g_strModelCheckerEngine = "model-checker-engine";
static string const g_strModelCheckerInvariants = "model-checker-invariants";
static string const g_strModelCheckerShowUnproved = "model-checker-show-unproved";
static string const g_strModelCheckerSolvers = "model-checker-solvers";
static string const g_strModelCheckerTargets = "model-checker-targets";
@ -789,6 +790,13 @@ General Information)").c_str(),
po::value<string>()->value_name("all,bmc,chc,none")->default_value("none"),
"Select model checker engine."
)
(
g_strModelCheckerInvariants.c_str(),
po::value<string>()->value_name("default,all,contract,reentrancy")->default_value("default"),
"Select whether to report inferred contract inductive invariants."
" Multiple types of invariants can be selected at the same time, separated by a comma and no spaces."
" By default no invariants are reported."
)
(
g_strModelCheckerShowUnproved.c_str(),
"Show all unproved targets separately."
@ -886,13 +894,21 @@ bool CommandLineParser::processArgs()
else
m_options.input.mode = InputMode::Compiler;
if (
m_args.count(g_strExperimentalViaIR) > 0 &&
m_options.input.mode != InputMode::Compiler &&
m_options.input.mode != InputMode::CompilerWithASTImport
)
map<string, set<InputMode>> validOptionInputModeCombinations = {
// TODO: This should eventually contain all options.
{g_strErrorRecovery, {InputMode::Compiler, InputMode::CompilerWithASTImport}},
{g_strExperimentalViaIR, {InputMode::Compiler, InputMode::CompilerWithASTImport}},
};
vector<string> invalidOptionsForCurrentInputMode;
for (auto const& [optionName, inputModes]: validOptionInputModeCombinations)
{
serr() << "The option --" << g_strExperimentalViaIR << " is only supported in the compiler mode." << endl;
if (m_args.count(optionName) > 0 && inputModes.count(m_options.input.mode) == 0)
invalidOptionsForCurrentInputMode.push_back(optionName);
}
if (!invalidOptionsForCurrentInputMode.empty())
{
serr() << "The following options are not supported in the current input mode: " << joinOptionNames(invalidOptionsForCurrentInputMode) << endl;
return false;
}
@ -1233,6 +1249,18 @@ bool CommandLineParser::processArgs()
m_options.modelChecker.settings.engine = *engine;
}
if (m_args.count(g_strModelCheckerInvariants))
{
string invsStr = m_args[g_strModelCheckerInvariants].as<string>();
optional<ModelCheckerInvariants> invs = ModelCheckerInvariants::fromString(invsStr);
if (!invs)
{
serr() << "Invalid option for --" << g_strModelCheckerInvariants << ": " << invsStr << endl;
return false;
}
m_options.modelChecker.settings.invariants = *invs;
}
if (m_args.count(g_strModelCheckerShowUnproved))
m_options.modelChecker.settings.showUnproved = true;
@ -1268,6 +1296,7 @@ bool CommandLineParser::processArgs()
m_args.count(g_strModelCheckerContracts) ||
m_args.count(g_strModelCheckerDivModNoSlacks) ||
m_args.count(g_strModelCheckerEngine) ||
m_args.count(g_strModelCheckerInvariants) ||
m_args.count(g_strModelCheckerShowUnproved) ||
m_args.count(g_strModelCheckerSolvers) ||
m_args.count(g_strModelCheckerTargets) ||

37
test/cmdlineTests.sh
View File

@ -92,7 +92,7 @@ echo "Using solc binary at ${SOLC}"
INTERACTIVE=true
if ! tty -s || [ "$CI" ]
then
INTERACTIVE=""
INTERACTIVE=false
fi
# extend stack size in case we run via ASAN
@ -123,7 +123,7 @@ function update_expectation {
function ask_expectation_update
{
if [[ $INTERACTIVE != "" ]]
if [[ $INTERACTIVE == true ]]
then
local newExpectation="${1}"
local expectationFile="${2}"
@ -142,12 +142,13 @@ function ask_expectation_update
e*) "$editor" "$expectationFile"; break;;
u*) update_expectation "$newExpectation" "$expectationFile"; break;;
s*) return;;
q*) exit 1;;
q*) fail;;
esac
done
fi
else
exit 1
[[ $INTERACTIVE == false ]] || assertFail
fail
fi
}
@ -252,7 +253,7 @@ EOF
printError "Incorrect exit code. Expected $exit_code_expected but got $exitCode."
[[ $exit_code_expectation_file != "" ]] && ask_expectation_update "$exitCode" "$exit_code_expectation_file"
[[ $exit_code_expectation_file == "" ]] && exit 1
[[ $exit_code_expectation_file == "" ]] && fail
fi
if [[ "$(cat "$stdout_path")" != "${stdout_expected}" ]]
@ -266,7 +267,7 @@ EOF
printError "When running $solc_command"
[[ $stdout_expectation_file != "" ]] && ask_expectation_update "$(cat "$stdout_path")" "$stdout_expectation_file"
[[ $stdout_expectation_file == "" ]] && exit 1
[[ $stdout_expectation_file == "" ]] && fail
fi
if [[ "$(cat "$stderr_path")" != "${stderr_expected}" ]]
@ -280,7 +281,7 @@ EOF
printError "When running $solc_command"
[[ $stderr_expectation_file != "" ]] && ask_expectation_update "$(cat "$stderr_path")" "$stderr_expectation_file"
[[ $stderr_expectation_file == "" ]] && exit 1
[[ $stderr_expectation_file == "" ]] && fail
fi
rm "$stdout_path" "$stderr_path"
@ -300,10 +301,10 @@ function test_solc_assembly_output()
if [ -z "$empty" ]
then
printError "Incorrect assembly output. Expected: "
echo -e "${expected}"
>&2 echo -e "${expected}"
printError "with arguments ${solc_args[*]}, but got:"
echo "${output}"
exit 1
>&2 echo "${output}"
fail
fi
}
@ -373,7 +374,7 @@ printTask "Running general commandline tests..."
then
printError "Ambiguous input. Found input files in multiple formats:"
echo -e "${inputFiles}"
exit 1
fail
fi
# Use printf to get rid of the trailing newline
@ -475,7 +476,8 @@ echo "Done."
printTask "Testing library checksum..."
echo '' | msg_on_error --no-stdout "$SOLC" - --link --libraries a=0x90f20564390eAe531E810af625A22f51385Cd222
echo '' | "$SOLC" - --link --libraries a=0x80f20564390eAe531E810af625A22f51385Cd222 &>/dev/null && exit 1
echo '' | "$SOLC" - --link --libraries a=0x80f20564390eAe531E810af625A22f51385Cd222 &>/dev/null && \
fail "solc --link did not reject a library address with an invalid checksum."
printTask "Testing long library names..."
echo '' | msg_on_error --no-stdout "$SOLC" - --link --libraries aveeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeerylonglibraryname=0x90f20564390eAe531E810af625A22f51385Cd222
@ -503,7 +505,8 @@ SOLTMPDIR=$(mktemp -d)
# First time it works
echo 'contract C {}' | msg_on_error --no-stderr "$SOLC" - --bin -o "$SOLTMPDIR/non-existing-stuff-to-create"
# Second time it fails
echo 'contract C {}' | "$SOLC" - --bin -o "$SOLTMPDIR/non-existing-stuff-to-create" 2>/dev/null && exit 1
echo 'contract C {}' | "$SOLC" - --bin -o "$SOLTMPDIR/non-existing-stuff-to-create" 2>/dev/null && \
fail "solc did not refuse to overwrite $SOLTMPDIR/non-existing-stuff-to-create."
# Unless we force
echo 'contract C {}' | msg_on_error --no-stderr "$SOLC" - --overwrite --bin -o "$SOLTMPDIR/non-existing-stuff-to-create"
)
@ -517,8 +520,8 @@ printTask "Testing assemble, yul, strict-assembly and optimize..."
# Test options above in conjunction with --optimize.
# Using both, --assemble and --optimize should fail.
echo '{}' | "$SOLC" - --assemble --optimize &>/dev/null && exit 1
echo '{}' | "$SOLC" - --yul --optimize &>/dev/null && exit 1
echo '{}' | "$SOLC" - --assemble --optimize &>/dev/null && fail "solc --assemble --optimize did not fail as expected."
echo '{}' | "$SOLC" - --yul --optimize &>/dev/null && fail "solc --yul --optimize did not fail as expected."
# Test yul and strict assembly output
# Non-empty code results in non-empty binary representation with optimizations turned off,
@ -563,8 +566,8 @@ SOLTMPDIR=$(mktemp -d)
cd "$SOLTMPDIR"
if ! "$REPO_ROOT/scripts/ASTImportTest.sh"
then
rm -rf "$SOLTMPDIR"
exit 1
rm -r "$SOLTMPDIR"
fail
fi
)
rm -r "$SOLTMPDIR"

1
test/cmdlineTests/inline_assembly_function_name_clash/args Normal file
View File

@ -0,0 +1 @@
--experimental-via-ir --combined-json function-debug-runtime --pretty-json --json-indent 4

5
test/cmdlineTests/inline_assembly_function_name_clash/err Normal file
View File

@ -0,0 +1,5 @@
Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: <SPDX-License>" to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information.
--> inline_assembly_function_name_clash/input.sol
Warning: Source file does not specify required compiler version!
--> inline_assembly_function_name_clash/input.sol

18
test/cmdlineTests/inline_assembly_function_name_clash/input.sol Normal file
View File

@ -0,0 +1,18 @@
contract C {
uint x;
modifier m() {
uint t;
assembly {
function f() -> x { x := 8 }
t := f()
}
x = t;
_;
}
function f() m m public returns (uint r) {
assembly { function f() -> x { x := 1 } r := f() }
}
function g() m m public returns (uint r) {
assembly { function f() -> x { x := 2 } r := f() }
}
}

168
test/cmdlineTests/inline_assembly_function_name_clash/output Normal file
View File

@ -0,0 +1,168 @@
{
"contracts":
{
"inline_assembly_function_name_clash/input.sol:C":
{
"function-debug-runtime":
{
"abi_decode_tuple_":
{
"entryPoint": 216,
"parameterSlots": 2,
"returnSlots": 0
},
"abi_encode_t_uint256_to_t_uint256_fromStack":
{
"entryPoint": 250,
"parameterSlots": 2,
"returnSlots": 0
},
"abi_encode_tuple_t_uint256__to_t_uint256__fromStack":
{
"entryPoint": 265,
"parameterSlots": 2,
"returnSlots": 1
},
"allocate_unbounded":
{
"entryPoint": 196,
"parameterSlots": 0,
"returnSlots": 1
},
"cleanup_t_uint256":
{
"entryPoint": 240,
"parameterSlots": 1,
"returnSlots": 1
},
"convert_t_uint256_to_t_uint256":
{
"entryPoint": 391,
"parameterSlots": 1,
"returnSlots": 1
},
"fun_f_25":
{
"entryPoint": 658,
"id": 25,
"parameterSlots": 0,
"returnSlots": 1
},
"fun_f_25_inner":
{
"entryPoint": 624,
"parameterSlots": 1,
"returnSlots": 1
},
"fun_g_36":
{
"entryPoint": 874,
"id": 36,
"parameterSlots": 0,
"returnSlots": 1
},
"fun_g_36_inner":
{
"entryPoint": 840,
"parameterSlots": 1,
"returnSlots": 1
},
"identity":
{
"entryPoint": 381,
"parameterSlots": 1,
"returnSlots": 1
},
"modifier_m_17":
{
"entryPoint": 470,
"id": 14,
"parameterSlots": 1,
"returnSlots": 1
},
"modifier_m_19":
{
"entryPoint": 547,
"id": 14,
"parameterSlots": 1,
"returnSlots": 1
},
"modifier_m_28":
{
"entryPoint": 686,
"id": 14,
"parameterSlots": 1,
"returnSlots": 1
},
"modifier_m_30":
{
"entryPoint": 763,
"id": 14,
"parameterSlots": 1,
"returnSlots": 1
},
"prepare_store_t_uint256":
{
"entryPoint": 425,
"parameterSlots": 1,
"returnSlots": 1
},
"revert_error_42b3090547df1d2001c96683413b8cf91c1b902ef5e3cb8d9f6f304cf7446f74":
{
"entryPoint": 292,
"parameterSlots": 0,
"returnSlots": 0
},
"revert_error_ca66f745a3ce8ff40e2ccaf1ad45db7774001b90d25810abd9040049be7bf4bb":
{
"entryPoint": 206,
"parameterSlots": 0,
"returnSlots": 0
},
"revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b":
{
"entryPoint": 211,
"parameterSlots": 0,
"returnSlots": 0
},
"shift_left_0":
{
"entryPoint": 302,
"parameterSlots": 1,
"returnSlots": 1
},
"shift_right_224_unsigned":
{
"entryPoint": 183,
"parameterSlots": 1,
"returnSlots": 1
},
"update_byte_slice_32_shift_0":
{
"entryPoint": 315,
"parameterSlots": 2,
"returnSlots": 1
},
"update_storage_value_offset_0t_uint256_to_t_uint256":
{
"entryPoint": 435,
"parameterSlots": 2,
"returnSlots": 0
},
"usr$f":
{
"entryPoint": 493,
"parameterSlots": 0,
"returnSlots": 1
},
"zero_value_for_split_t_uint256":
{
"entryPoint": 297,
"parameterSlots": 0,
"returnSlots": 1
}
}
}
},
"version": "<VERSION REMOVED>"
}

1
test/cmdlineTests/linking_qualified_library_name/args Normal file
View File

@ -0,0 +1 @@
linking_qualified_library_name/contract1.sol --bin --libraries linking_qualified_library_name/math.sol:Log:0x7777777777777777777777777777777777777777

10
test/cmdlineTests/linking_qualified_library_name/contract1.sol Normal file
View File

@ -0,0 +1,10 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
import "linking_qualified_library_name/math.sol";
contract C {
function foo() public {
Log.log10();
}
}

6
test/cmdlineTests/linking_qualified_library_name/math.sol Normal file
View File

@ -0,0 +1,6 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
library Log {
function log10() external {}
}

8
test/cmdlineTests/linking_qualified_library_name/output Normal file
View File

@ -0,0 +1,8 @@
======= linking_qualified_library_name/contract1.sol:C =======
Binary:
<BYTECODE REMOVED>
======= linking_qualified_library_name/math.sol:Log =======
Binary:
<BYTECODE REMOVED>

26
test/cmdlineTests/linking_strict_assembly_no_file_name_in_link_reference/output
View File

@ -1,26 +0,0 @@
======= linking_strict_assembly_no_file_name_in_link_reference/input.yul (EVM) =======
Pretty printed source:
object "a" {
code {
let addr := linkersymbol("L")
sstore(0, addr)
}
}
Binary representation:
7312345678901234567890123456789012345678908060005550
Text representation:
/* "linking_strict_assembly_no_file_name_in_link_reference/input.yul":44:61 */
linkerSymbol("8aa64f937099b65a4febc243a5ae0f2d6416bb9e473c30dd29c1ee498fb7c5a8")
/* "linking_strict_assembly_no_file_name_in_link_reference/input.yul":80:84 */
dup1
/* "linking_strict_assembly_no_file_name_in_link_reference/input.yul":77:78 */
0x00
/* "linking_strict_assembly_no_file_name_in_link_reference/input.yul":70:85 */
sstore
/* "linking_strict_assembly_no_file_name_in_link_reference/input.yul":22:91 */
pop

1
test/cmdlineTests/linking_strict_assembly_qualified_library_qualified_reference/args Normal file
View File

@ -0,0 +1 @@
--strict-assembly --libraries :L=0x1234567890123456789012345678901234567890 --debug-info none

0
test/cmdlineTests/linking_strict_assembly_no_file_name_in_link_reference/err → test/cmdlineTests/linking_strict_assembly_qualified_library_qualified_reference/err
View File

6
test/cmdlineTests/linking_strict_assembly_qualified_library_qualified_reference/input.yul Normal file
View File

@ -0,0 +1,6 @@
object "a" {
code {
let addr := linkersymbol(":L")
sstore(0, addr)
}
}

21
test/cmdlineTests/linking_strict_assembly_qualified_library_qualified_reference/output Normal file
View File

@ -0,0 +1,21 @@
======= linking_strict_assembly_qualified_library_qualified_reference/input.yul (EVM) =======
Pretty printed source:
object "a" {
code {
let addr := linkersymbol(":L")
sstore(0, addr)
}
}
Binary representation:
7312345678901234567890123456789012345678908060005550
Text representation:
linkerSymbol("20a18a9bf97d889dcf77111b674da319a4e9e3e05d3f4df9e0bf5c588dd4f0f8")
dup1
0x00
sstore
pop

1
test/cmdlineTests/linking_strict_assembly_qualified_library_unqualified_reference/args Normal file
View File

@ -0,0 +1 @@
--strict-assembly --libraries :L=0x1234567890123456789012345678901234567890 --debug-info none

1
test/cmdlineTests/linking_strict_assembly_qualified_library_unqualified_reference/err Normal file
View File

@ -0,0 +1 @@
Warning: Yul is still experimental. Please use the output with care.

0
test/cmdlineTests/linking_strict_assembly_no_file_name_in_link_reference/input.yul → test/cmdlineTests/linking_strict_assembly_qualified_library_unqualified_reference/input.yul
View File

21
test/cmdlineTests/linking_strict_assembly_qualified_library_unqualified_reference/output Normal file
View File

@ -0,0 +1,21 @@
======= linking_strict_assembly_qualified_library_unqualified_reference/input.yul (EVM) =======
Pretty printed source:
object "a" {
code {
let addr := linkersymbol("L")
sstore(0, addr)
}
}
Binary representation:
73__$8aa64f937099b65a4febc243a5ae0f2d64$__8060005550
Text representation:
linkerSymbol("8aa64f937099b65a4febc243a5ae0f2d6416bb9e473c30dd29c1ee498fb7c5a8")
dup1
0x00
sstore
pop

2
test/cmdlineTests/linking_strict_assembly_no_file_name_in_link_reference/args → test/cmdlineTests/linking_strict_assembly_unqualified_library_qualified_reference/args
View File

@ -1 +1 @@
--strict-assembly --libraries L=0x1234567890123456789012345678901234567890
--strict-assembly --libraries L=0x1234567890123456789012345678901234567890 --debug-info none

1
test/cmdlineTests/linking_strict_assembly_unqualified_library_qualified_reference/err Normal file
View File

@ -0,0 +1 @@
Warning: Yul is still experimental. Please use the output with care.

6
test/cmdlineTests/linking_strict_assembly_unqualified_library_qualified_reference/input.yul Normal file
View File

@ -0,0 +1,6 @@
object "a" {
code {
let addr := linkersymbol(":L")
sstore(0, addr)
}
}

21
test/cmdlineTests/linking_strict_assembly_unqualified_library_qualified_reference/output Normal file
View File

@ -0,0 +1,21 @@
======= linking_strict_assembly_unqualified_library_qualified_reference/input.yul (EVM) =======
Pretty printed source:
object "a" {
code {
let addr := linkersymbol(":L")
sstore(0, addr)
}
}
Binary representation:
73__$20a18a9bf97d889dcf77111b674da319a4$__8060005550
Text representation:
linkerSymbol("20a18a9bf97d889dcf77111b674da319a4e9e3e05d3f4df9e0bf5c588dd4f0f8")
dup1
0x00
sstore
pop

1
test/cmdlineTests/linking_strict_assembly_unqualified_library_unqualified_reference/args Normal file
View File

@ -0,0 +1 @@
--strict-assembly --libraries L=0x1234567890123456789012345678901234567890 --debug-info none

1
test/cmdlineTests/linking_strict_assembly_unqualified_library_unqualified_reference/err Normal file
View File

@ -0,0 +1 @@
Warning: Yul is still experimental. Please use the output with care.

6
test/cmdlineTests/linking_strict_assembly_unqualified_library_unqualified_reference/input.yul Normal file
View File

@ -0,0 +1,6 @@
object "a" {
code {
let addr := linkersymbol("L")
sstore(0, addr)
}
}

21
test/cmdlineTests/linking_strict_assembly_unqualified_library_unqualified_reference/output Normal file
View File

@ -0,0 +1,21 @@
======= linking_strict_assembly_unqualified_library_unqualified_reference/input.yul (EVM) =======
Pretty printed source:
object "a" {
code {
let addr := linkersymbol("L")
sstore(0, addr)
}
}
Binary representation:
7312345678901234567890123456789012345678908060005550
Text representation:
linkerSymbol("8aa64f937099b65a4febc243a5ae0f2d6416bb9e473c30dd29c1ee498fb7c5a8")
dup1
0x00
sstore
pop

1
test/cmdlineTests/linking_unqualified_library_name/args Normal file
View File

@ -0,0 +1 @@
linking_unqualified_library_name/contract1.sol linking_unqualified_library_name/contract2.sol --bin --libraries Log:0x7777777777777777777777777777777777777777

11
test/cmdlineTests/linking_unqualified_library_name/contract1.sol Normal file
View File

@ -0,0 +1,11 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
import "linking_unqualified_library_name/error.sol";
contract C {
function foo() public {
Log.print();
}
}

10
test/cmdlineTests/linking_unqualified_library_name/contract2.sol Normal file
View File

@ -0,0 +1,10 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
import "linking_unqualified_library_name/math.sol";
contract C {
function foo() public {
Log.log10();
}
}

6
test/cmdlineTests/linking_unqualified_library_name/error.sol Normal file
View File

@ -0,0 +1,6 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
library Log {
function print() external {}
}

6
test/cmdlineTests/linking_unqualified_library_name/math.sol Normal file
View File

@ -0,0 +1,6 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
library Log {
function log10() external {}
}

20
test/cmdlineTests/linking_unqualified_library_name/output Normal file
View File

@ -0,0 +1,20 @@
======= linking_unqualified_library_name/contract1.sol:C =======
Binary:
<BYTECODE REMOVED>__$cdf6d5ab08a9335b02e7c2475aa27d04fa$__<BYTECODE REMOVED>
// $cdf6d5ab08a9335b02e7c2475aa27d04fa$ -> linking_unqualified_library_name/error.sol:Log
======= linking_unqualified_library_name/contract2.sol:C =======
Binary:
<BYTECODE REMOVED>__$22584241c2fc4f2884d5222245463779a8$__<BYTECODE REMOVED>
// $22584241c2fc4f2884d5222245463779a8$ -> linking_unqualified_library_name/math.sol:Log
======= linking_unqualified_library_name/error.sol:Log =======
Binary:
<BYTECODE REMOVED>
======= linking_unqualified_library_name/math.sol:Log =======
Binary:
<BYTECODE REMOVED>

1
test/cmdlineTests/model_checker_invariants_all/args Normal file
View File

@ -0,0 +1 @@
--model-checker-engine chc --model-checker-invariants all

15
test/cmdlineTests/model_checker_invariants_all/err Normal file
View File

@ -0,0 +1,15 @@
Warning: Return value of low-level calls not used.
--> model_checker_invariants_all/input.sol:6:3:
|
6 | _a.call("");
| ^^^^^^^^^^^
Info: Contract invariant(s) for model_checker_invariants_all/input.sol:test:
(x <= 0)
Reentrancy property(ies) for model_checker_invariants_all/input.sol:test:
(!(x <= 0) || (x' <= 0))
((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))
((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
<errorCode> = 0 -> no errors
<errorCode> = 1 -> Assertion failed at assert(x < 10)
<errorCode> = 3 -> Assertion failed at assert(x < 10)

12
test/cmdlineTests/model_checker_invariants_all/input.sol Normal file
View File

@ -0,0 +1,12 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
contract test {
uint x;
function f(address _a) public {
_a.call("");
assert(x < 10);
}
function g() public view {
assert(x < 10);
}
}

1
test/cmdlineTests/model_checker_invariants_contract/args Normal file
View File

@ -0,0 +1 @@
--model-checker-engine chc --model-checker-invariants contract

2
test/cmdlineTests/model_checker_invariants_contract/err Normal file
View File

@ -0,0 +1,2 @@
Info: Contract invariant(s) for model_checker_invariants_contract/input.sol:test:
(x <= 0)

8
test/cmdlineTests/model_checker_invariants_contract/input.sol Normal file
View File

@ -0,0 +1,8 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
contract test {
uint x;
function f() public view {
assert(x < 10);
}
}

1
test/cmdlineTests/model_checker_invariants_contract_reentrancy/args Normal file
View File

@ -0,0 +1 @@
--model-checker-engine chc --model-checker-invariants contract,reentrancy

15
test/cmdlineTests/model_checker_invariants_contract_reentrancy/err Normal file
View File

@ -0,0 +1,15 @@
Warning: Return value of low-level calls not used.
--> model_checker_invariants_contract_reentrancy/input.sol:6:3:
|
6 | _a.call("");
| ^^^^^^^^^^^
Info: Contract invariant(s) for model_checker_invariants_contract_reentrancy/input.sol:test:
(x <= 0)
Reentrancy property(ies) for model_checker_invariants_contract_reentrancy/input.sol:test:
(!(x <= 0) || (x' <= 0))
((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))
((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
<errorCode> = 0 -> no errors
<errorCode> = 1 -> Assertion failed at assert(x < 10)
<errorCode> = 3 -> Assertion failed at assert(x < 10)

12
test/cmdlineTests/model_checker_invariants_contract_reentrancy/input.sol Normal file
View File

@ -0,0 +1,12 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
contract test {
uint x;
function f(address _a) public {
_a.call("");
assert(x < 10);
}
function g() public view {
assert(x < 10);
}
}

1
test/cmdlineTests/model_checker_invariants_reentrancy/args Normal file
View File

@ -0,0 +1 @@
--model-checker-engine chc --model-checker-invariants reentrancy

10
test/cmdlineTests/model_checker_invariants_reentrancy/err Normal file
View File

@ -0,0 +1,10 @@
Warning: Return value of low-level calls not used.
--> model_checker_invariants_reentrancy/input.sol:6:3:
|
6 | _a.call("");
| ^^^^^^^^^^^
Info: Reentrancy property(ies) for model_checker_invariants_reentrancy/input.sol:test:
((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
<errorCode> = 0 -> no errors
<errorCode> = 1 -> Assertion failed at assert(x < 10)

9
test/cmdlineTests/model_checker_invariants_reentrancy/input.sol Normal file
View File

@ -0,0 +1,9 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
contract test {
uint x;
function f(address _a) public {
_a.call("");
assert(x < 10);
}
}

1
test/cmdlineTests/model_checker_invariants_wrong/args Normal file
View File

@ -0,0 +1 @@
--model-checker-engine chc --model-checker-invariants what

1
test/cmdlineTests/model_checker_invariants_wrong/err Normal file
View File

@ -0,0 +1 @@
Invalid option for --model-checker-invariants: what

1
test/cmdlineTests/model_checker_invariants_wrong/exit Normal file
View File

@ -0,0 +1 @@
1

8
test/cmdlineTests/model_checker_invariants_wrong/input.sol Normal file
View File

@ -0,0 +1,8 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
contract test {
uint x;
function g() public view {
assert(x < 10);
}
}

23
test/cmdlineTests/standard_model_checker_invariants_contract/input.json Normal file
View File

@ -0,0 +1,23 @@
{
"language": "Solidity",
"sources":
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint x;
function f() public view {
assert(x < 10);
}
}"
}
},
"settings":
{
"modelChecker":
{
"engine": "chc",
"invariants": ["contract"]
}
}
}

7
test/cmdlineTests/standard_model_checker_invariants_contract/output.json Normal file
View File

@ -0,0 +1,7 @@
{"errors":[{"component":"general","errorCode":"1180","formattedMessage":"Info: Contract invariant(s) for A:test:
(x <= 0)
","message":"Contract invariant(s) for A:test:
(x <= 0)
","severity":"info","type":"Info"}],"sources":{"A":{"id":0}}}

27
test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/input.json Normal file
View File

@ -0,0 +1,27 @@
{
"language": "Solidity",
"sources":
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint x;
function f(address _a) public {
_a.call(\"\");
assert(x < 10);
}
function g() public view {
assert(x < 10);
}
}"
}
},
"settings":
{
"modelChecker":
{
"engine": "chc",
"invariants": ["contract", "reentrancy"]
}
}
}

27
test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/output.json Normal file
View File

@ -0,0 +1,27 @@
{"errors":[{"component":"general","errorCode":"9302","formattedMessage":"Warning: Return value of low-level calls not used.
--> A:7:7:
|
7 | \t\t\t\t\t\t_a.call(\"\");
| \t\t\t\t\t\t^^^^^^^^^^^
","message":"Return value of low-level calls not used.","severity":"warning","sourceLocation":{"end":143,"file":"A","start":132},"type":"Warning"},{"component":"general","errorCode":"1180","formattedMessage":"Info: Contract invariant(s) for A:test:
(x <= 0)
Reentrancy property(ies) for A:test:
(!(x <= 0) || (x' <= 0))
((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))
((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
<errorCode> = 0 -> no errors
<errorCode> = 1 -> Assertion failed at assert(x < 10)
<errorCode> = 3 -> Assertion failed at assert(x < 10)
","message":"Contract invariant(s) for A:test:
(x <= 0)
Reentrancy property(ies) for A:test:
(!(x <= 0) || (x' <= 0))
((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))
((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
<errorCode> = 0 -> no errors
<errorCode> = 1 -> Assertion failed at assert(x < 10)
<errorCode> = 3 -> Assertion failed at assert(x < 10)
","severity":"info","type":"Info"}],"sources":{"A":{"id":0}}}

Some files were not shown because too many files have changed in this diff Show More