cerc-io/solidity
16
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 pull request #11451 from ethereum/smt_report_invariants

Browse Source 
[SMTChecker] Report contract invariants
This commit is contained in:
Harikrishnan Mulackal 2021-10-26 12:41:36 +02:00 committed by GitHub
commit 401dd4337a
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
200 changed files with 1253 additions and 45 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -9,6 +9,7 @@ Compiler Features:
* 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.

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

@ -418,6 +418,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.

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,

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

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"];

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)}

21
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";
@ -801,6 +802,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."
@ -1253,6 +1261,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;
@ -1288,6 +1308,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) ||

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}}}

24
test/cmdlineTests/standard_model_checker_invariants_reentrancy/input.json Normal file
View File

@ -0,0 +1,24 @@
{
"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);
}
}"
}
},
"settings":
{
"modelChecker":
{
"engine": "chc",
"invariants": ["reentrancy"]
}
}
}

17
test/cmdlineTests/standard_model_checker_invariants_reentrancy/output.json Normal file
View File

@ -0,0 +1,17 @@
{"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: Reentrancy property(ies) for A:test:
((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
<errorCode> = 0 -> no errors
<errorCode> = 1 -> Assertion failed at assert(x < 10)
","message":"Reentrancy property(ies) for A:test:
((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
<errorCode> = 0 -> no errors
<errorCode> = 1 -> Assertion failed at assert(x < 10)
","severity":"info","type":"Info"}],"sources":{"A":{"id":0}}}

23
test/cmdlineTests/standard_model_checker_invariants_wrong_key/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": ["what"]
}
}
}

1
test/cmdlineTests/standard_model_checker_invariants_wrong_key/output.json Normal file
View File

@ -0,0 +1 @@
{"errors":[{"component":"general","formattedMessage":"Invalid model checker invariants requested.","message":"Invalid model checker invariants requested.","severity":"error","type":"JSONError"}]}

23
test/cmdlineTests/standard_model_checker_invariants_wrong_type/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": [2]
}
}
}

1
test/cmdlineTests/standard_model_checker_invariants_wrong_type/output.json Normal file
View File

@ -0,0 +1 @@
{"errors":[{"component":"general","formattedMessage":"Every invariant type in settings.modelChecker.invariants must be a string.","message":"Every invariant type in settings.modelChecker.invariants must be a string.","severity":"error","type":"JSONError"}]}

23
test/cmdlineTests/standard_model_checker_invariants_wrong_type_2/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": 2
}
}
}

1
test/cmdlineTests/standard_model_checker_invariants_wrong_type_2/output.json Normal file
View File

@ -0,0 +1 @@
{"errors":[{"component":"general","formattedMessage":"settings.modelChecker.invariants must be an array.","message":"settings.modelChecker.invariants must be an array.","severity":"error","type":"JSONError"}]}

10
test/libsolidity/SMTCheckerTest.cpp
View File

@ -19,6 +19,8 @@
#include <test/libsolidity/SMTCheckerTest.h>
#include <test/Common.h>
#include <range/v3/action/remove_if.hpp>
using namespace std;
using namespace solidity;
using namespace solidity::langutil;
@ -67,6 +69,14 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, E
else
BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT counterexample choice."));
auto const& ignoreInv = m_reader.stringSetting("SMTIgnoreInv", "no");
if (ignoreInv == "no")
m_modelCheckerSettings.invariants = ModelCheckerInvariants::All();
else if (ignoreInv == "yes")
m_modelCheckerSettings.invariants = ModelCheckerInvariants::None();
else
BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT invariant choice."));
auto const& ignoreOSSetting = m_reader.stringSetting("SMTIgnoreOS", "none");
for (string const& os: ignoreOSSetting | ranges::views::split(',') | ranges::to<vector<string>>())
{

2
test/libsolidity/SMTCheckerTest.h
View File

@ -49,6 +49,8 @@ protected:
Set in m_modelCheckerSettings.
SMTIgnoreCex: `yes`, `no`, where the default is `no`.
Set in m_ignoreCex.
SMTIgnoreInv: `yes`, `no`, where the default is `no`.
Set in m_modelCheckerSettings.
SMTShowUnproved: `yes`, `no`, where the default is `yes`.
Set in m_modelCheckerSettings.
SMTSolvers: `all`, `cvc4`, `z3`, `none`, where the default is `all`.

3
test/libsolidity/smtCheckerTests/array_members/array_push_string_literal.sol
View File

@ -13,6 +13,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (139-161): CHC: Assertion violation happens here.
// Warning 6328: (139-161): CHC: Assertion violation happens here.\nCounterexample:\ndata = [0x62]\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.g()
// Warning 6328: (263-290): CHC: Assertion violation happens here.\nCounterexample:\ndata = [0x01]\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.g()

2
test/libsolidity/smtCheckerTests/array_members/length_1d_assignment_2d_storage_to_storage.sol
View File

@ -16,4 +16,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Info 1180: Contract invariant(s) for :C:\n!(arr.length <= 0)\n!(arr2.length <= 0)\n(((arr.length + ((- 1) * arr2.length)) <= 0) && ((arr2.length + ((- 1) * arr.length)) <= 0))\n(((arr2[0].length + ((- 1) * arr[0].length)) >= 0) && ((arr2[0].length + ((- 1) * arr[0].length)) <= 0))\n

1
test/libsolidity/smtCheckerTests/array_members/length_1d_copy_2d_storage_to_memory.sol
View File

@ -17,3 +17,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Info 1180: Contract invariant(s) for :C:\n!(arr.length <= 1)\n

1
test/libsolidity/smtCheckerTests/array_members/length_1d_mapping_array_1.sol
View File

@ -7,3 +7,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Info 1180: Contract invariant(s) for :C:\n(true && (map[1].length <= 0))\n

1
test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_1.sol
View File

@ -11,3 +11,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Info 1180: Contract invariant(s) for :C:\n(((s1.arr.length + ((- 1) * s2.arr.length)) >= 0) && ((s1.arr.length + ((- 1) * s2.arr.length)) <= 0))\n

1
test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol
View File

@ -21,3 +21,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Info 1180: Contract invariant(s) for :C:\n!(s1.arr.length <= 0)\n!(s2.arr.length <= 0)\n(((s2.arr[0].length + ((- 1) * s1.arr[0].length)) <= 0) && ((s1.arr[0].length + ((- 1) * s2.arr[0].length)) <= 0))\n

1
test/libsolidity/smtCheckerTests/array_members/length_function_call.sol
View File

@ -9,3 +9,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Info 1180: Contract invariant(s) for :C:\n(arr.length <= 0)\n

1
test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment.sol
View File

@ -15,3 +15,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Info 1180: Contract invariant(s) for :C:\n!(arr.length <= 2)\n

1
test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2.sol
View File

@ -23,3 +23,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Info 1180: Contract invariant(s) for :C:\n!(arr.length <= 2)\n!(arr.length <= 3)\n!(arr[2].length <= 3)\n

1
test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2_fail.sol
View File

@ -27,3 +27,4 @@ contract C {
// Warning 6328: (291-317): CHC: Assertion violation happens here.
// Warning 6328: (321-347): CHC: Assertion violation happens here.
// Warning 6328: (351-374): CHC: Assertion violation happens here.
// Info 1180: Contract invariant(s) for :C:\n!(arr.length <= 2)\n!(arr.length <= 3)\n!(arr[2].length <= 3)\n

1
test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3.sol
View File

@ -28,3 +28,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Info 1180: Contract invariant(s) for :C:\n!(arr.length <= 7)\n!(arr.length <= 8)\n((arr[5].length <= 0) && (arr[8].length <= 0))\n

2
test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol
View File

@ -25,8 +25,10 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (319-345): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f()
// Warning 6328: (349-375): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f()
// Warning 6328: (379-402): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f()
// Warning 6328: (406-432): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f()
// Info 1180: Contract invariant(s) for :C:\n!(arr.length <= 3)\n!(arr.length <= 5)\n!(arr.length <= 7)\n!(arr.length <= 8)\n

2
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol
View File

@ -18,4 +18,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (199-229): CHC: Assertion violation happens here.\nCounterexample:\nb = [1]\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.g()
// Warning 6328: (199-229): CHC: Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_1d.sol
View File

@ -12,5 +12,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (204-230): CHC: Assertion violation happens here.
// Warning 6328: (204-230): CHC: Assertion violation happens here.\nCounterexample:\nb = [0, 0]\nlength = 2\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.f()

1
test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe.sol
View File

@ -8,4 +8,5 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreInv: yes
// ----

1
test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe_no_overflow_assumption.sol
View File

@ -9,3 +9,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Info 1180: Contract invariant(s) for :C:\n(!((x[x.length] := 23)[0] >= 43) && !((x[x.length] := 23)[0] <= 41))\n

2
test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe_no_overflow_assumption.sol
View File

@ -11,4 +11,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Info 1180: Contract invariant(s) for :C:\n(x.length >= 0)\n

1
test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2_fail.sol
View File

@ -10,6 +10,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (90-116): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[[0]]]\nlast = 0\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()
// Warning 6328: (170-186): CHC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol
View File

@ -12,6 +12,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6368: (188-192): CHC: Out of bounds access happens here.\nCounterexample:\na = []\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 6368: (188-195): CHC: Out of bounds access happens here.\nCounterexample:\n\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()

1
test/libsolidity/smtCheckerTests/blockchain_state/balance_non_zero_2.sol
View File

@ -11,3 +11,4 @@ contract C {
// SMTEngine: all
// ----
// Warning 6328: (153-188): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor(){ msg.value: 101 }\nC.f()
// Info 1180: Contract invariant(s) for :C:\n!((:var 0).balances[address(this)] <= 100)\n

1
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive.sol
View File

@ -16,3 +16,4 @@ contract C {
// ----
// Warning 6328: (132-188): CHC: Assertion violation happens here.
// Warning 6328: (269-324): CHC: Assertion violation happens here.
// Info 1180: Contract invariant(s) for :C:\n((prevBalance + ((- 1) * (:var 1).balances[address(this)])) <= 0)\n

1
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_2.sol
View File

@ -17,3 +17,4 @@ contract C {
// ----
// Warning 4984: (266-272): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639926, once = true\n\nTransaction trace:\nC.constructor(){ msg.value: 28100 }\nState: x = 115792089237316195423570985008687907853269984665640564039457584007913129639926, once = false\nC.f(){ msg.value: 8 }
// Warning 6328: (235-273): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, once = true\n\nTransaction trace:\nC.constructor(){ msg.value: 0 }\nState: x = 0, once = false\nC.f(){ msg.value: 8 }
// Info 1180: Contract invariant(s) for :C:\nonce\n

3
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol
View File

@ -15,7 +15,8 @@ contract C {
// Warning 4984: (82-85): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (154-160): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (212-218): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6328: (180-219): CHC: Assertion violation happens here.\nCounterexample:\nc = 1\n\nTransaction trace:\nC.constructor()\nState: c = 0\nC.f(){ msg.value: 11 }\nState: c = 1\nC.inv()
// Warning 6328: (180-219): CHC: Assertion violation happens here.
// Info 1180: Contract invariant(s) for :C:\n(((11 * c) + ((- 1) * (:var 1).balances[address(this)])) <= 0)\n
// Warning 2661: (82-85): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 2661: (154-160): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 2661: (212-218): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

1
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_5.sol
View File

@ -12,3 +12,4 @@ contract C {
// SMTEngine: all
// ----
// Warning 6328: (122-158): CHC: Assertion violation happens here.\nCounterexample:\nsum = 0\n\nTransaction trace:\nC.constructor()\nState: sum = 0\nC.inv()
// Info 1180: Contract invariant(s) for :C:\n((sum + ((- 1) * (:var 1).balances[address(this)])) <= 0)\n

2
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_calls.sol
View File

@ -20,7 +20,9 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (173-208): CHC: Assertion violation happens here.\nCounterexample:\nonce = true\n\nTransaction trace:\nC.constructor()\nState: once = false\nC.f(){ msg.value: 10 }
// Warning 6328: (321-356): CHC: Assertion violation happens here.\nCounterexample:\nonce = true\n\nTransaction trace:\nC.constructor()\nState: once = false\nC.f(){ msg.value: 10 }\n C.g() -- internal call
// Warning 6328: (469-504): CHC: Assertion violation happens here.\nCounterexample:\nonce = true\n\nTransaction trace:\nC.constructor()\nState: once = false\nC.f(){ msg.value: 10 }\n C.g() -- internal call\n C.h() -- internal call
// Info 1180: Contract invariant(s) for :C:\n((:var 1).balances[address(this)] >= 0)\nonce\n

1
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls.sol
View File

@ -15,4 +15,5 @@ contract C {
// ----
// Warning 1218: (131-165): CHC: Error trying to invoke SMT solver.
// Warning 6328: (131-165): CHC: Assertion violation might happen here.
// Info 1180: Reentrancy property(ies) for :C:\n(!(<errorCode> >= 2) && (((:var 0).balances[address(this)] + ((- 1) * (:var 1).balances[address(this)])) >= 0))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(address(this).balance == x)\n<errorCode> = 2 -> Assertion failed at assert(address(this).balance >= x)\n
// Warning 4661: (131-165): BMC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_2.sol
View File

@ -12,3 +12,4 @@ contract C {
// ----
// Warning 9302: (82-93): Return value of low-level calls not used.
// Warning 6328: (97-131): CHC: Assertion violation happens here.
// Info 1180: Reentrancy property(ies) for :C:\n((((:var 1).balances[address(this)] + ((- 1) * (:var 0).balances[address(this)])) <= 0) && !(<errorCode> >= 2))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(address(this).balance == x)\n<errorCode> = 2 -> Assertion failed at assert(address(this).balance >= x)\n

1
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_mutex.sol
View File

@ -22,3 +22,4 @@ contract C {
// SMTIgnoreCex: yes
// ----
// Warning 6328: (277-310): CHC: Assertion violation happens here.
// Info 1180: Reentrancy property(ies) for :C:\n((!lock || (((:var 3).balances[address(this)] + ((- 1) * (:var 1).balances[address(this)])) <= 0)) && !(<errorCode> = 1) && (lock' || !lock) && (!lock || (((:var 3).balances[address(this)] + ((- 1) * (:var 1).balances[address(this)])) >= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(address(this).balance == x)\n<errorCode> = 2 -> Assertion failed at assert(address(this).balance < x)\n

1
test/libsolidity/smtCheckerTests/blockchain_state/balance_spend.sol
View File

@ -19,4 +19,5 @@ contract C {
// SMTIgnoreCex: yes
// ----
// Warning 6328: (280-314): CHC: Assertion violation happens here.
// Info 1180: Contract invariant(s) for :C:\n((!(c <= 1) || !((:var 1).balances[address(this)] <= 91)) && !((:var 1).balances[address(this)] <= 82) && (!(c <= 0) || !((:var 1).balances[address(this)] <= 100)))\n
// Warning 1236: (175-190): BMC: Insufficient funds happens here.

2
test/libsolidity/smtCheckerTests/blockchain_state/free_function_1.sol
View File

@ -13,3 +13,5 @@ contract C {
}
// ====
// SMTEngine: all
// ----
// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\n

1
test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol
View File

@ -20,4 +20,5 @@ contract C {
// SMTIgnoreCex: yes
// ----
// Warning 6328: (258-274): CHC: Assertion violation happens here.
// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\n
// Warning 1236: (33-46): BMC: Insufficient funds happens here.

2
test/libsolidity/smtCheckerTests/blockchain_state/library_internal_1.sol
View File

@ -16,3 +16,5 @@ contract C {
}
// ====
// SMTEngine: all
// ----
// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\n

1
test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol
View File

@ -23,4 +23,5 @@ contract C {
// SMTIgnoreCex: yes
// ----
// Warning 6328: (315-331): CHC: Assertion violation happens here.
// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\n
// Warning 1236: (87-100): BMC: Insufficient funds happens here.

2
test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change.sol
View File

@ -9,4 +9,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Info 1180: Contract invariant(s) for :C:\n(((address(this) + ((- 1) * t)) <= 0) && ((address(this) + ((- 1) * t)) >= 0))\n

2
test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_external_call.sol
View File

@ -16,4 +16,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Info 1180: Contract invariant(s) for :C:\n(((address(this) + ((- 1) * t)) <= 0) && ((address(this) + ((- 1) * t)) >= 0))\nReentrancy property(ies) for :C:\n((!(<errorCode> >= 2) || !((t + ((- 1) * address(this))) = 0)) && (!((t + ((- 1) * address(this))) <= 0) || ((t' + ((- 1) * address(this))) <= 0)) && (!((t + ((- 1) * address(this))) >= 0) || ((address(this) + ((- 1) * t')) <= 0)))\n(((<errorCode> <= 0) || !((t + ((- 1) * address(this))) = 0)) && (!((t + ((- 1) * address(this))) <= 0) || ((t' + ((- 1) * address(this))) <= 0)) && (!((t + ((- 1) * address(this))) >= 0) || ((address(this) + ((- 1) * t')) <= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(address(this) == t)\n<errorCode> = 2 -> Assertion failed at assert(a == t)\n

1
test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_internal_call.sol
View File

@ -14,3 +14,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Info 1180: Contract invariant(s) for :C:\n(((t + ((- 1) * address(this))) >= 0) && ((t + ((- 1) * address(this))) <= 0))\n

1
test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_1.sol
View File

@ -23,3 +23,4 @@ contract C {
// SMTEngine: all
// ----
// Warning 6328: (327-341): CHC: Assertion violation happens here.\nCounterexample:\nx = 7\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n C.f() -- internal call
// Info 1180: Contract invariant(s) for :C:\n((x = 0) || (x = 7))\n

1
test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_2.sol
View File

@ -23,3 +23,4 @@ contract C {
// SMTEngine: all
// ----
// Warning 6328: (333-347): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n C.f() -- internal call
// Info 1180: Contract invariant(s) for :C:\n((x = 0) || (x = 3))\n

1
test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_3.sol
View File

@ -23,3 +23,4 @@ contract C {
// SMTEngine: all
// ----
// Warning 6328: (326-340): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n C.f() -- internal call
// Info 1180: Contract invariant(s) for :C:\n((x = 0) || (x = 3))\n

1
test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_4.sol
View File

@ -24,3 +24,4 @@ contract C {
// SMTIgnoreCex: yes
// ----
// Warning 6328: (333-347): CHC: Assertion violation happens here.
// Info 1180: Contract invariant(s) for :C:\n((x = 0) || (x = 7))\n

1
test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers.sol
View File

@ -24,3 +24,4 @@ contract C {
// SMTEngine: all
// ----
// Warning 6328: (70-84): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.test()
// Info 1180: Contract invariant(s) for :C:\n(x = 0)\n

2
test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol
View File

@ -44,5 +44,5 @@ contract C {
// SMTEngine: all
// ----
// Warning 6328: (255-269): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.test()\n C.reset_if_overflow() -- internal call
// Warning 6328: (502-519): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\noldx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.set(1)\nState: x = 1\nC.test()\n C.reset_if_overflow() -- internal call
// Warning 6328: (502-519): CHC: Assertion violation happens here.
// Warning 6328: (615-629): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.set(10)\nState: x = 10\nC.test()\n C.reset_if_overflow() -- internal call

1
test/libsolidity/smtCheckerTests/control_flow/branches_with_return/triple_nested_if.sol
View File

@ -18,3 +18,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Info 1180: Contract invariant(s) for :C:\n((c <= 0) && (a <= 0) && (b <= 0))\n

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