diff --git a/Changelog.md b/Changelog.md index e79b13e6e..c5211922d 100644 --- a/Changelog.md +++ b/Changelog.md @@ -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. diff --git a/docs/smtchecker.rst b/docs/smtchecker.rst index a9732d05e..791659897 100644 --- a/docs/smtchecker.rst +++ b/docs/smtchecker.rst @@ -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`. +By default the SMTChecker does not report invariants. + Division and Modulo With Slack Variables ======================================== diff --git a/docs/using-the-compiler.rst b/docs/using-the-compiler.rst index 88da5d5e6..c6c40cacc 100644 --- a/docs/using-the-compiler.rst +++ b/docs/using-the-compiler.rst @@ -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. diff --git a/liblangutil/ErrorReporter.cpp b/liblangutil/ErrorReporter.cpp index 02487034a..f99247b32 100644 --- a/liblangutil/ErrorReporter.cpp +++ b/liblangutil/ErrorReporter.cpp @@ -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); +} diff --git a/liblangutil/ErrorReporter.h b/liblangutil/ErrorReporter.h index 6f91f0713..67fc76e83 100644 --- a/liblangutil/ErrorReporter.h +++ b/liblangutil/ErrorReporter.h @@ -72,6 +72,8 @@ public: std::string const& _description ); + void info(ErrorId _error, std::string const& _description); + void declarationError( ErrorId _error, SourceLocation const& _location, diff --git a/liblangutil/UniqueErrorReporter.h b/liblangutil/UniqueErrorReporter.h index 886720568..fd91b87dc 100644 --- a/liblangutil/UniqueErrorReporter.h +++ b/liblangutil/UniqueErrorReporter.h @@ -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})) diff --git a/libsmtutil/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp index 48fdbd328..630eb0619 100644 --- a/libsmtutil/CHCSmtLib2Interface.cpp +++ b/libsmtutil/CHCSmtLib2Interface.cpp @@ -87,7 +87,7 @@ void CHCSmtLib2Interface::addRule(Expression const& _expr, std::string const& /* ); } -pair CHCSmtLib2Interface::query(Expression const& _block) +tuple CHCSmtLib2Interface::query(Expression const& _block) { string accumulated{}; swap(m_accumulatedOutput, accumulated); @@ -118,8 +118,7 @@ pair 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) diff --git a/libsmtutil/CHCSmtLib2Interface.h b/libsmtutil/CHCSmtLib2Interface.h index 460895e3b..a7dfb7692 100644 --- a/libsmtutil/CHCSmtLib2Interface.h +++ b/libsmtutil/CHCSmtLib2Interface.h @@ -44,7 +44,9 @@ public: void addRule(Expression const& _expr, std::string const& _name) override; - std::pair 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 query(Expression const& _expr) override; void declareVariable(std::string const& _name, SortPointer const& _sort) override; diff --git a/libsmtutil/CHCSolverInterface.h b/libsmtutil/CHCSolverInterface.h index 203255345..8385c1c40 100644 --- a/libsmtutil/CHCSolverInterface.h +++ b/libsmtutil/CHCSolverInterface.h @@ -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 query( + /// @returns solving result, an invariant, and counterexample graph, if possible. + virtual std::tuple query( Expression const& _expr ) = 0; diff --git a/libsmtutil/SolverInterface.h b/libsmtutil/SolverInterface.h index 87ee78013..ca4c497de 100644 --- a/libsmtutil/SolverInterface.h +++ b/libsmtutil/SolverInterface.h @@ -23,7 +23,9 @@ #include #include +#include +#include #include #include @@ -305,6 +307,64 @@ public: ); } + static bool sameSort(std::vector 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 _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 _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 _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 _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) diff --git a/libsmtutil/Z3CHCInterface.cpp b/libsmtutil/Z3CHCInterface.cpp index 1196b27ff..82dca4878 100644 --- a/libsmtutil/Z3CHCInterface.cpp +++ b/libsmtutil/Z3CHCInterface.cpp @@ -77,7 +77,7 @@ void Z3CHCInterface::addRule(Expression const& _expr, string const& _name) } } -pair Z3CHCInterface::query(Expression const& _expr) +tuple Z3CHCInterface::query(Expression const& _expr) { CheckResult result; try @@ -93,15 +93,15 @@ pair 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 Z3CHCInterface::query(Expression result = CheckResult::ERROR; } - return {result, {}}; + return {result, Expression(true), {}}; } void Z3CHCInterface::setSpacerOptions(bool _preProcessing) diff --git a/libsmtutil/Z3CHCInterface.h b/libsmtutil/Z3CHCInterface.h index a0e4bfa67..5a768f65c 100644 --- a/libsmtutil/Z3CHCInterface.h +++ b/libsmtutil/Z3CHCInterface.h @@ -43,7 +43,7 @@ public: void addRule(Expression const& _expr, std::string const& _name) override; - std::pair query(Expression const& _expr) override; + std::tuple query(Expression const& _expr) override; Z3Interface* z3Interface() const { return m_z3Interface.get(); } diff --git a/libsmtutil/Z3Interface.cpp b/libsmtutil/Z3Interface.cpp index 03105a172..3a5c75bf3 100644 --- a/libsmtutil/Z3Interface.cpp +++ b/libsmtutil/Z3Interface.cpp @@ -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 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())); diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt index a1cb68c35..7e3791eab 100644 --- a/libsolidity/CMakeLists.txt +++ b/libsolidity/CMakeLists.txt @@ -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 diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index f0072313b..bfdb0b428 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -23,6 +23,7 @@ #endif #include +#include #include #include #include @@ -30,17 +31,20 @@ #include #include +#include #include -#include - -#include -#include - #ifdef HAVE_Z3_DLOPEN #include #endif +#include + +#include +#include +#include +#include + #include #include @@ -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(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 CHC::query(smtutil::Expression const& _query, langutil::SourceLocation const& _location) +tuple 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 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 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(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("") != string::npos) + { + set seenErrors; + msg += " = 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 += " = " + 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 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> 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(), ""); diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 24b27c55b..d9e27a89c 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -245,9 +245,9 @@ private: //@{ /// Adds Horn rule to the solver. void addRule(smtutil::Expression const& _rule, std::string const& _ruleName); - /// @returns if query is unsatisfiable (safe). - /// @returns otherwise. - std::pair query(smtutil::Expression const& _query, langutil::SourceLocation const& _location); + /// @returns if query is unsatisfiable (safe). + /// @returns otherwise. + std::tuple 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, smt::EncodingContext::IdCompare> m_unsafeTargets; /// Targets not proved. std::map, smt::EncodingContext::IdCompare> m_unprovedTargets; + + /// Inferred invariants. + std::map, PredicateCompare> m_invariants; //@} /// Control-flow. diff --git a/libsolidity/formal/ExpressionFormatter.cpp b/libsolidity/formal/ExpressionFormatter.cpp new file mode 100644 index 000000000..2591328f8 --- /dev/null +++ b/libsolidity/formal/ExpressionFormatter.cpp @@ -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 . +*/ +// SPDX-License-Identifier: GPL-3.0 + +#include + +#include +#include + +#include + +#include + +#include +#include +#include + +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 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 (, ..., ) + // - 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 (, ..., ). + 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_". + 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 const& _args) +{ + return _expr.name + "(" + boost::algorithm::join(_args, ", ") + ")"; +} + +string formatInfixOp(string const& _op, vector const& _args) +{ + return "(" + boost::algorithm::join(_args, " " + _op + " ") + ")"; +} + +string formatArrayOp(smtutil::Expression const& _expr, vector const& _args) +{ + if (_expr.name == "select") + { + auto const& a0 = _args.at(0); + static set 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 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 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 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 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, ", ") + ")"; +} + +} diff --git a/libsolidity/formal/ExpressionFormatter.h b/libsolidity/formal/ExpressionFormatter.h new file mode 100644 index 000000000..3efbeb781 --- /dev/null +++ b/libsolidity/formal/ExpressionFormatter.h @@ -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 . +*/ +// SPDX-License-Identifier: GPL-3.0 + +#pragma once + +/** + * Formats SMT expressions into Solidity-like strings. + */ + +#include + +#include +#include + +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 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); + +} diff --git a/libsolidity/formal/Invariants.cpp b/libsolidity/formal/Invariants.cpp new file mode 100644 index 000000000..9dad0722c --- /dev/null +++ b/libsolidity/formal/Invariants.cpp @@ -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 . +*/ +// SPDX-License-Identifier: GPL-3.0 + +#include + +#include +#include + +#include + +#include + +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> collectInvariants( + smtutil::Expression const& _proof, + set const& _predicates, + ModelCheckerInvariants const& _invariantsSetting +) +{ + set targets; + if (_invariantsSetting.has(InvariantType::Contract)) + targets.insert("interface_"); + if (_invariantsSetting.has(InvariantType::Reentrancy)) + targets.insert("nondet_interface_"); + + map> equalities; + // Collect equalities where one of the sides is a predicate we're interested in. + BreadthFirstSearch{{&_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> 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 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; +} + +} diff --git a/libsolidity/formal/Invariants.h b/libsolidity/formal/Invariants.h new file mode 100644 index 000000000..b6459fccd --- /dev/null +++ b/libsolidity/formal/Invariants.h @@ -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 . +*/ +// SPDX-License-Identifier: GPL-3.0 + +#pragma once + +#include +#include + +#include +#include +#include + +namespace solidity::frontend::smt +{ + +std::map> collectInvariants( + smtutil::Expression const& _proof, + std::set const& _predicates, + ModelCheckerInvariants const& _invariantsSettings +); + +} diff --git a/libsolidity/formal/ModelCheckerSettings.cpp b/libsolidity/formal/ModelCheckerSettings.cpp index 207894d39..274571a15 100644 --- a/libsolidity/formal/ModelCheckerSettings.cpp +++ b/libsolidity/formal/ModelCheckerSettings.cpp @@ -25,6 +25,40 @@ using namespace std; using namespace solidity; using namespace solidity::frontend; +map const ModelCheckerInvariants::validInvariants{ + {"contract", InvariantType::Contract}, + {"reentrancy", InvariantType::Reentrancy} +}; + +std::optional ModelCheckerInvariants::fromString(string const& _invs) +{ + set 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>()) + { + 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 const ModelCheckerTargets::targetStrings{ {"constantCondition", TargetType::ConstantCondition}, @@ -37,6 +71,17 @@ map const ModelCheckerTargets::targetStrings{ {"outOfBounds", TargetType::OutOfBounds} }; +map 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::fromString(string const& _targets) { set chosenTargets; diff --git a/libsolidity/formal/ModelCheckerSettings.h b/libsolidity/formal/ModelCheckerSettings.h index a01985fcb..e3e93fcf4 100644 --- a/libsolidity/formal/ModelCheckerSettings.h +++ b/libsolidity/formal/ModelCheckerSettings.h @@ -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 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 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 invariants; +}; + enum class VerificationTargetType { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert, PopEmptyArray, OutOfBounds }; struct ModelCheckerTargets @@ -106,6 +132,8 @@ struct ModelCheckerTargets static std::map const targetStrings; + static std::map 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 && diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp index 23aa7590e..6e0eb4f3b 100644 --- a/libsolidity/formal/Predicate.cpp +++ b/libsolidity/formal/Predicate.cpp @@ -26,10 +26,13 @@ #include #include +#include + #include #include 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 const& _args, langutil::CharStreamProvider const& _charStreamProvider, @@ -418,6 +426,50 @@ pair>, vector> Predicate::lo return {formatExpressions(outValuesInScope, outTypes), localVarsInScope}; } +map Predicate::expressionSubstitution(smtutil::Expression const& _predExpr) const +{ + map 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] = ""; + 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> Predicate::formatExpressions(vector const& _exprs, vector const& _types) const { solAssert(_exprs.size() == _types.size(), ""); diff --git a/libsolidity/formal/Predicate.h b/libsolidity/formal/Predicate.h index 7357c9beb..16af42f45 100644 --- a/libsolidity/formal/Predicate.h +++ b/libsolidity/formal/Predicate.h @@ -21,6 +21,8 @@ #include #include +#include + #include #include @@ -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> localVariableValues(std::vector const& _args) const; + /// @returns a substitution map from the arguments of _predExpr + /// to a Solidity-like expression. + std::map expressionSubstitution(smtutil::Expression const& _predExpr) const; + private: /// @returns the formatted version of the given SMT expressions. Those expressions must be SMT constants. std::vector> formatExpressions(std::vector const& _exprs, std::vector const& _types) const; @@ -208,4 +217,16 @@ private: std::vector 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; + } +}; + } diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp index 66f5dc4e5..da28cf29f 100644 --- a/libsolidity/interface/StandardCompiler.cpp +++ b/libsolidity/interface/StandardCompiler.cpp @@ -445,7 +445,7 @@ std::optional checkSettingsKeys(Json::Value const& _input) std::optional checkModelCheckerSettingsKeys(Json::Value const& _input) { - static set keys{"contracts", "divModNoSlacks", "engine", "showUnproved", "solvers", "targets", "timeout"}; + static set keys{"contracts", "divModNoSlacks", "engine", "invariants", "showUnproved", "solvers", "targets", "timeout"}; return checkKeys(_input, keys, "modelChecker"); } @@ -987,6 +987,27 @@ std::variant 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"]; diff --git a/scripts/error_codes.py b/scripts/error_codes.py index 9290211a2..fe9c73b04 100755 --- a/scripts/error_codes.py +++ b/scripts/error_codes.py @@ -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)} diff --git a/solc/CommandLineParser.cpp b/solc/CommandLineParser.cpp index 6b1fc1526..22d92d463 100644 --- a/solc/CommandLineParser.cpp +++ b/solc/CommandLineParser.cpp @@ -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()->value_name("all,bmc,chc,none")->default_value("none"), "Select model checker engine." ) + ( + g_strModelCheckerInvariants.c_str(), + po::value()->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(); + optional 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) || diff --git a/test/cmdlineTests/model_checker_invariants_all/args b/test/cmdlineTests/model_checker_invariants_all/args new file mode 100644 index 000000000..389acc647 --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_all/args @@ -0,0 +1 @@ +--model-checker-engine chc --model-checker-invariants all diff --git a/test/cmdlineTests/model_checker_invariants_all/err b/test/cmdlineTests/model_checker_invariants_all/err new file mode 100644 index 000000000..47bc04256 --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_all/err @@ -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) || !( >= 3)) && (!(x <= 0) || (x' <= 0))) +((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) + = 0 -> no errors + = 1 -> Assertion failed at assert(x < 10) + = 3 -> Assertion failed at assert(x < 10) diff --git a/test/cmdlineTests/model_checker_invariants_all/input.sol b/test/cmdlineTests/model_checker_invariants_all/input.sol new file mode 100644 index 000000000..f8601cf4f --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_all/input.sol @@ -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); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_invariants_contract/args b/test/cmdlineTests/model_checker_invariants_contract/args new file mode 100644 index 000000000..e856a73b9 --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_contract/args @@ -0,0 +1 @@ +--model-checker-engine chc --model-checker-invariants contract diff --git a/test/cmdlineTests/model_checker_invariants_contract/err b/test/cmdlineTests/model_checker_invariants_contract/err new file mode 100644 index 000000000..a5277bebf --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_contract/err @@ -0,0 +1,2 @@ +Info: Contract invariant(s) for model_checker_invariants_contract/input.sol:test: +(x <= 0) diff --git a/test/cmdlineTests/model_checker_invariants_contract/input.sol b/test/cmdlineTests/model_checker_invariants_contract/input.sol new file mode 100644 index 000000000..3a857d484 --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_contract/input.sol @@ -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); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_invariants_contract_reentrancy/args b/test/cmdlineTests/model_checker_invariants_contract_reentrancy/args new file mode 100644 index 000000000..90591a5ae --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_contract_reentrancy/args @@ -0,0 +1 @@ +--model-checker-engine chc --model-checker-invariants contract,reentrancy diff --git a/test/cmdlineTests/model_checker_invariants_contract_reentrancy/err b/test/cmdlineTests/model_checker_invariants_contract_reentrancy/err new file mode 100644 index 000000000..372143657 --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_contract_reentrancy/err @@ -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) || !( >= 3)) && (!(x <= 0) || (x' <= 0))) +((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) + = 0 -> no errors + = 1 -> Assertion failed at assert(x < 10) + = 3 -> Assertion failed at assert(x < 10) diff --git a/test/cmdlineTests/model_checker_invariants_contract_reentrancy/input.sol b/test/cmdlineTests/model_checker_invariants_contract_reentrancy/input.sol new file mode 100644 index 000000000..f8601cf4f --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_contract_reentrancy/input.sol @@ -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); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_invariants_reentrancy/args b/test/cmdlineTests/model_checker_invariants_reentrancy/args new file mode 100644 index 000000000..904defe84 --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_reentrancy/args @@ -0,0 +1 @@ +--model-checker-engine chc --model-checker-invariants reentrancy diff --git a/test/cmdlineTests/model_checker_invariants_reentrancy/err b/test/cmdlineTests/model_checker_invariants_reentrancy/err new file mode 100644 index 000000000..a2fd6075a --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_reentrancy/err @@ -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) || ( <= 0))) + = 0 -> no errors + = 1 -> Assertion failed at assert(x < 10) diff --git a/test/cmdlineTests/model_checker_invariants_reentrancy/input.sol b/test/cmdlineTests/model_checker_invariants_reentrancy/input.sol new file mode 100644 index 000000000..f21d4d4c8 --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_reentrancy/input.sol @@ -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); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_invariants_wrong/args b/test/cmdlineTests/model_checker_invariants_wrong/args new file mode 100644 index 000000000..ae601a044 --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_wrong/args @@ -0,0 +1 @@ +--model-checker-engine chc --model-checker-invariants what diff --git a/test/cmdlineTests/model_checker_invariants_wrong/err b/test/cmdlineTests/model_checker_invariants_wrong/err new file mode 100644 index 000000000..1dc94780d --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_wrong/err @@ -0,0 +1 @@ +Invalid option for --model-checker-invariants: what diff --git a/test/cmdlineTests/model_checker_invariants_wrong/exit b/test/cmdlineTests/model_checker_invariants_wrong/exit new file mode 100644 index 000000000..d00491fd7 --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_wrong/exit @@ -0,0 +1 @@ +1 diff --git a/test/cmdlineTests/model_checker_invariants_wrong/input.sol b/test/cmdlineTests/model_checker_invariants_wrong/input.sol new file mode 100644 index 000000000..17bf3b749 --- /dev/null +++ b/test/cmdlineTests/model_checker_invariants_wrong/input.sol @@ -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); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/standard_model_checker_invariants_contract/input.json b/test/cmdlineTests/standard_model_checker_invariants_contract/input.json new file mode 100644 index 000000000..d47c93de2 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_invariants_contract/input.json @@ -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"] + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_invariants_contract/output.json b/test/cmdlineTests/standard_model_checker_invariants_contract/output.json new file mode 100644 index 000000000..1cd236baf --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_invariants_contract/output.json @@ -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}}} diff --git a/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/input.json b/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/input.json new file mode 100644 index 000000000..56139e6a5 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/input.json @@ -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"] + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/output.json b/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/output.json new file mode 100644 index 000000000..433648d0b --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/output.json @@ -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) || !( >= 3)) && (!(x <= 0) || (x' <= 0))) +((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) + = 0 -> no errors + = 1 -> Assertion failed at assert(x < 10) + = 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) || !( >= 3)) && (!(x <= 0) || (x' <= 0))) +((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) + = 0 -> no errors + = 1 -> Assertion failed at assert(x < 10) + = 3 -> Assertion failed at assert(x < 10) +","severity":"info","type":"Info"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_invariants_reentrancy/input.json b/test/cmdlineTests/standard_model_checker_invariants_reentrancy/input.json new file mode 100644 index 000000000..1f98000b0 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_invariants_reentrancy/input.json @@ -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"] + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_invariants_reentrancy/output.json b/test/cmdlineTests/standard_model_checker_invariants_reentrancy/output.json new file mode 100644 index 000000000..4158c3ae1 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_invariants_reentrancy/output.json @@ -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) || ( <= 0))) + = 0 -> no errors + = 1 -> Assertion failed at assert(x < 10) + + +","message":"Reentrancy property(ies) for A:test: +((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) + = 0 -> no errors + = 1 -> Assertion failed at assert(x < 10) +","severity":"info","type":"Info"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_invariants_wrong_key/input.json b/test/cmdlineTests/standard_model_checker_invariants_wrong_key/input.json new file mode 100644 index 000000000..e8ee6aba6 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_invariants_wrong_key/input.json @@ -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"] + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_invariants_wrong_key/output.json b/test/cmdlineTests/standard_model_checker_invariants_wrong_key/output.json new file mode 100644 index 000000000..7758b29ca --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_invariants_wrong_key/output.json @@ -0,0 +1 @@ +{"errors":[{"component":"general","formattedMessage":"Invalid model checker invariants requested.","message":"Invalid model checker invariants requested.","severity":"error","type":"JSONError"}]} diff --git a/test/cmdlineTests/standard_model_checker_invariants_wrong_type/input.json b/test/cmdlineTests/standard_model_checker_invariants_wrong_type/input.json new file mode 100644 index 000000000..54fc96d46 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_invariants_wrong_type/input.json @@ -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] + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_invariants_wrong_type/output.json b/test/cmdlineTests/standard_model_checker_invariants_wrong_type/output.json new file mode 100644 index 000000000..5ad18a3b1 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_invariants_wrong_type/output.json @@ -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"}]} diff --git a/test/cmdlineTests/standard_model_checker_invariants_wrong_type_2/input.json b/test/cmdlineTests/standard_model_checker_invariants_wrong_type_2/input.json new file mode 100644 index 000000000..f7522e6e5 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_invariants_wrong_type_2/input.json @@ -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 + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_invariants_wrong_type_2/output.json b/test/cmdlineTests/standard_model_checker_invariants_wrong_type_2/output.json new file mode 100644 index 000000000..b4fba3576 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_invariants_wrong_type_2/output.json @@ -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"}]} diff --git a/test/libsolidity/SMTCheckerTest.cpp b/test/libsolidity/SMTCheckerTest.cpp index 5606b0bfe..3b6b8e1b8 100644 --- a/test/libsolidity/SMTCheckerTest.cpp +++ b/test/libsolidity/SMTCheckerTest.cpp @@ -19,6 +19,8 @@ #include #include +#include + 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>()) { diff --git a/test/libsolidity/SMTCheckerTest.h b/test/libsolidity/SMTCheckerTest.h index 9cc4e5751..54d23c74f 100644 --- a/test/libsolidity/SMTCheckerTest.h +++ b/test/libsolidity/SMTCheckerTest.h @@ -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`. diff --git a/test/libsolidity/smtCheckerTests/array_members/array_push_string_literal.sol b/test/libsolidity/smtCheckerTests/array_members/array_push_string_literal.sol index 55b2160c4..5ed512278 100644 --- a/test/libsolidity/smtCheckerTests/array_members/array_push_string_literal.sol +++ b/test/libsolidity/smtCheckerTests/array_members/array_push_string_literal.sol @@ -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() diff --git a/test/libsolidity/smtCheckerTests/array_members/length_1d_assignment_2d_storage_to_storage.sol b/test/libsolidity/smtCheckerTests/array_members/length_1d_assignment_2d_storage_to_storage.sol index 4796e3a81..294038399 100644 --- a/test/libsolidity/smtCheckerTests/array_members/length_1d_assignment_2d_storage_to_storage.sol +++ b/test/libsolidity/smtCheckerTests/array_members/length_1d_assignment_2d_storage_to_storage.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/array_members/length_1d_copy_2d_storage_to_memory.sol b/test/libsolidity/smtCheckerTests/array_members/length_1d_copy_2d_storage_to_memory.sol index 5ad65991a..468f34257 100644 --- a/test/libsolidity/smtCheckerTests/array_members/length_1d_copy_2d_storage_to_memory.sol +++ b/test/libsolidity/smtCheckerTests/array_members/length_1d_copy_2d_storage_to_memory.sol @@ -17,3 +17,4 @@ contract C { // ==== // SMTEngine: all // ---- +// Info 1180: Contract invariant(s) for :C:\n!(arr.length <= 1)\n diff --git a/test/libsolidity/smtCheckerTests/array_members/length_1d_mapping_array_1.sol b/test/libsolidity/smtCheckerTests/array_members/length_1d_mapping_array_1.sol index c6e695f24..48e0f73bf 100644 --- a/test/libsolidity/smtCheckerTests/array_members/length_1d_mapping_array_1.sol +++ b/test/libsolidity/smtCheckerTests/array_members/length_1d_mapping_array_1.sol @@ -7,3 +7,4 @@ contract C { // ==== // SMTEngine: all // ---- +// Info 1180: Contract invariant(s) for :C:\n(true && (map[1].length <= 0))\n diff --git a/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_1.sol b/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_1.sol index 3ab218741..833caa24f 100644 --- a/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_1.sol +++ b/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_1.sol @@ -11,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 diff --git a/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol b/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol index cd9b6690d..71571d944 100644 --- a/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol +++ b/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/array_members/length_function_call.sol b/test/libsolidity/smtCheckerTests/array_members/length_function_call.sol index a51c7aa7d..c96d53047 100644 --- a/test/libsolidity/smtCheckerTests/array_members/length_function_call.sol +++ b/test/libsolidity/smtCheckerTests/array_members/length_function_call.sol @@ -9,3 +9,4 @@ contract C { // ==== // SMTEngine: all // ---- +// Info 1180: Contract invariant(s) for :C:\n(arr.length <= 0)\n diff --git a/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment.sol b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment.sol index 5756c7aff..4f1cf701b 100644 --- a/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment.sol +++ b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment.sol @@ -15,3 +15,4 @@ contract C { // ==== // SMTEngine: all // ---- +// Info 1180: Contract invariant(s) for :C:\n!(arr.length <= 2)\n diff --git a/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2.sol b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2.sol index 525c704e1..66dad8412 100644 --- a/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2.sol +++ b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2_fail.sol b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2_fail.sol index 086224a11..0023906fe 100644 --- a/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2_fail.sol +++ b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2_fail.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3.sol b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3.sol index 78a020e05..caafcbd39 100644 --- a/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3.sol +++ b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol index f4d5c889c..062b668c3 100644 --- a/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol +++ b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol index 5920a4e74..30f194eb7 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_1d.sol b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_1d.sol index 6b23ac1d4..ad3ba7823 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_1d.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_1d.sol @@ -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() diff --git a/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe.sol b/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe.sol index 0a440e7a4..930736ce8 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe.sol @@ -8,4 +8,5 @@ contract C { } // ==== // SMTEngine: all +// SMTIgnoreInv: yes // ---- diff --git a/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe_no_overflow_assumption.sol b/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe_no_overflow_assumption.sol index 6992ca1e4..9cc3f2e37 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe_no_overflow_assumption.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe_no_overflow_assumption.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe_no_overflow_assumption.sol b/test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe_no_overflow_assumption.sol index 1b241745a..60b11c91a 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe_no_overflow_assumption.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe_no_overflow_assumption.sol @@ -11,4 +11,6 @@ contract C { } // ==== // SMTEngine: all +// SMTIgnoreOS: macos // ---- +// Info 1180: Contract invariant(s) for :C:\n(x.length >= 0)\n diff --git a/test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2_fail.sol b/test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2_fail.sol index c29c34f62..dcda253ce 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2_fail.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2_fail.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol index 43eebddcf..87b9d92bf 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol @@ -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() diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_non_zero_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_non_zero_2.sol index 100f11066..f88eab0bf 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_non_zero_2.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_non_zero_2.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive.sol index ea5947d01..fc4719cef 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_2.sol index c561179ec..c4714e2e3 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_2.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_2.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol index 183e60d95..e8f750d07 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_5.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_5.sol index e703c65c3..1885a60c8 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_5.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_5.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_calls.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_calls.sol index 3bc569997..263a90b08 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_calls.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_calls.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls.sol index 6144056a8..e46dfda34 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls.sol @@ -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(!( >= 2) && (((:var 0).balances[address(this)] + ((- 1) * (:var 1).balances[address(this)])) >= 0))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(address(this).balance == x)\n = 2 -> Assertion failed at assert(address(this).balance >= x)\n // Warning 4661: (131-165): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_2.sol index e0da57fb2..28c4734bd 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_2.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_2.sol @@ -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) && !( >= 2))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(address(this).balance == x)\n = 2 -> Assertion failed at assert(address(this).balance >= x)\n diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_mutex.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_mutex.sol index 59c123429..559f67e19 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_mutex.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_mutex.sol @@ -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)) && !( = 1) && (lock' || !lock) && (!lock || (((:var 3).balances[address(this)] + ((- 1) * (:var 1).balances[address(this)])) >= 0)))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(address(this).balance == x)\n = 2 -> Assertion failed at assert(address(this).balance < x)\n diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend.sol index 72755cc35..1e4ec7a32 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/free_function_1.sol b/test/libsolidity/smtCheckerTests/blockchain_state/free_function_1.sol index 9b40afa2e..260d3c942 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/free_function_1.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/free_function_1.sol @@ -13,3 +13,5 @@ contract C { } // ==== // SMTEngine: all +// ---- +// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\n diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol index 6c3d12026..50081bc5a 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_1.sol b/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_1.sol index 4f7497625..9df3aa27a 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_1.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_1.sol @@ -16,3 +16,5 @@ contract C { } // ==== // SMTEngine: all +// ---- +// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\n diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol index 8fca1916f..f32652da9 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change.sol b/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change.sol index 7e233950c..0b66b2791 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_external_call.sol b/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_external_call.sol index f3abd33c9..0b5136dca 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_external_call.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_external_call.sol @@ -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((!( >= 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((( <= 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 = 0 -> no errors\n = 1 -> Assertion failed at assert(address(this) == t)\n = 2 -> Assertion failed at assert(a == t)\n diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_internal_call.sol b/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_internal_call.sol index 3c7b1214e..0ffe43469 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_internal_call.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_internal_call.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_1.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_1.sol index 097637168..21f1f5c7f 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_1.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_1.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_2.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_2.sol index 458c78081..bf1da4275 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_2.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_2.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_3.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_3.sol index b8323501c..ace158bb9 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_3.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_3.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_4.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_4.sol index 81f8b3d7c..44910fa62 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_4.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_4.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers.sol index aa8199cd0..32d647762 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol index 4241fa9e2..9765fc1f9 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/triple_nested_if.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/triple_nested_if.sol index 9ca87a4b0..09ee2b2b2 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/triple_nested_if.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/triple_nested_if.sol @@ -18,3 +18,4 @@ contract C { // ==== // SMTEngine: all // ---- +// Info 1180: Contract invariant(s) for :C:\n((c <= 0) && (a <= 0) && (b <= 0))\n diff --git a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output.sol b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output.sol index aae296695..228f9d580 100644 --- a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output.sol +++ b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output.sol @@ -37,3 +37,4 @@ contract C { // ==== // SMTEngine: all // ---- +// Info 1180: Contract invariant(s) for :C:\n(((erc + ((- 1) * ecrecover(tuple_constructor(h, v, r, s)))) <= 0) && ((erc + ((- 1) * ecrecover(tuple_constructor(h, v, r, s)))) >= 0))\n(((kec + ((- 1) * keccak256(data))) >= 0) && ((kec + ((- 1) * keccak256(data))) <= 0))\n(((rip + ((- 1) * ripemd160(data))) <= 0) && ((rip + ((- 1) * ripemd160(data))) >= 0))\n(((sha + ((- 1) * sha256(data))) <= 0) && ((sha + ((- 1) * sha256(data))) >= 0))\n diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_mutex.sol b/test/libsolidity/smtCheckerTests/external_calls/call_mutex.sol index 4352a7e95..a31093924 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/call_mutex.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/call_mutex.sol @@ -23,3 +23,4 @@ contract C { // SMTEngine: all // ---- // Warning 9302: (218-234): Return value of low-level calls not used. +// Info 1180: Reentrancy property(ies) for :C:\n((!lock || ((x' + ((- 1) * x)) = 0)) && ( <= 0) && (lock' || !lock))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(y == x)\n diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_view.sol b/test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_view.sol index 69c2e2953..f0f844fff 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_view.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_view.sol @@ -10,7 +10,9 @@ contract C { } // ==== // SMTEngine: all +// SMTIgnoreOS: macos // ---- // Warning 2519: (106-112): This declaration shadows an existing declaration. // Warning 2072: (106-112): Unused local variable. // Warning 2072: (114-131): Unused local variable. +// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\nReentrancy property(ies) for :C:\n((!(x <= 0) || (x' <= 0)) && (( <= 0) || !(x <= 0)))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(x == 0)\n diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_safe.sol b/test/libsolidity/smtCheckerTests/external_calls/call_safe.sol index 33791dd0d..09d3a2592 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/call_safe.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/call_safe.sol @@ -10,3 +10,4 @@ contract C { // ---- // Warning 2072: (57-63): Unused local variable. // Warning 2072: (65-82): Unused local variable. +// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\nReentrancy property(ies) for :C:\n((!(x <= 0) || (x' <= 0)) && (( <= 0) || !(x <= 0)))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(x == 0)\n diff --git a/test/libsolidity/smtCheckerTests/external_calls/external.sol b/test/libsolidity/smtCheckerTests/external_calls/external.sol index 8dd0f404a..659329e0b 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external.sol @@ -18,3 +18,4 @@ contract C { // SMTEngine: all // ---- // Warning 6328: (167-181): CHC: Assertion violation happens here. +// Info 1180: Reentrancy property(ies) for :C:\n!( = 1)\n = 0 -> no errors\n = 1 -> Overflow at ++x\n = 3 -> Assertion failed at assert(x < 10)\n diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_2.sol index cfd56271b..3fbdd8511 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_2.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_2.sol @@ -14,3 +14,4 @@ contract C { // SMTEngine: all // ---- // Warning 6328: (87-101): CHC: Assertion violation happens here.\nCounterexample:\nz = 2\n_x = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: z = 2\nC.g(0) +// Info 1180: Contract invariant(s) for :C:\n(!(z >= 3) && !(z <= 1))\n diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash.sol index 3464874c8..8f5b162a0 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_hash.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash.sol @@ -28,3 +28,4 @@ contract C { // SMTIgnoreCex: yes // ---- // Warning 6328: (390-412): CHC: Assertion violation happens here. +// Info 1180: Reentrancy property(ies) for :C:\n!( = 1)\n = 0 -> no errors\n = 1 -> Assertion failed at assert(prevOwner == owner)\n = 3 -> Assertion failed at assert(sig_1 == sig_2)\n diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure.sol index e1273a299..2e837478d 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure.sol @@ -30,3 +30,4 @@ contract C { // SMTIgnoreCex: yes // ---- // Warning 6328: (398-420): CHC: Assertion violation happens here. +// Info 1180: Reentrancy property(ies) for :C:\n!( = 1)\n = 0 -> no errors\n = 1 -> Assertion failed at assert(prevOwner == owner)\n = 3 -> Assertion failed at assert(sig_1 == sig_2)\n diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol index ecf7ff5ad..317400e1d 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol @@ -36,3 +36,4 @@ contract C { // SMTIgnoreCex: yes // ---- // Warning 6328: (495-532): CHC: Assertion violation happens here. +// Info 1180: Reentrancy property(ies) for :C:\n(((owner + ((- 1) * owner')) >= 0) && !( = 1) && ((owner + ((- 1) * owner')) <= 0))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(prevOwner == owner)\n = 3 -> Assertion failed at assert(owner == address(0) || y != z)\n diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2.sol index a90e87cb3..be9f698e1 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2.sol @@ -38,6 +38,8 @@ contract C { } // ==== // SMTEngine: all +// SMTIgnoreInv: yes +// SMTIgnoreOS: macos // ---- // Warning 2018: (33-88): Function state mutability can be restricted to view // Warning 6328: (367-381): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_3.sol index 83ab8873b..e5259c6c4 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_3.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_3.sol @@ -41,3 +41,4 @@ contract C { // ==== // SMTEngine: all // ---- +// Info 1180: Contract invariant(s) for :C:\n((insidef || (z <= 0)) && (y <= 0))\nReentrancy property(ies) for :C:\n((!insidef || !( >= 2)) && (!(y <= 0) || (y' <= 0)) && (insidef' || !insidef))\n((!insidef || !( >= 3)) && (insidef' || !insidef))\n = 0 -> no errors\n = 2 -> Assertion failed at assert(z == y)\n = 3 -> Assertion failed at assert(prevOwner == owner)\n diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_3.sol index ff2cd7c85..590133a78 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_3.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_3.sol @@ -28,5 +28,7 @@ contract C is A { // ==== // SMTEngine: all // SMTIgnoreCex: yes +// SMTIgnoreInv: yes +// SMTIgnoreOS: macos // ---- // Warning 6328: (154-168): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol index 98f6d80be..627f79763 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol @@ -28,4 +28,5 @@ contract C { // ---- // Warning 1218: (302-333): CHC: Error trying to invoke SMT solver. // Warning 6328: (302-333): CHC: Assertion violation might happen here. +// Info 1180: Contract invariant(s) for :C:\n(((kec + ((- 1) * keccak256(data))) >= 0) && ((kec + ((- 1) * keccak256(data))) <= 0))\nReentrancy property(ies) for :C:\n((!((kec + ((- 1) * keccak256(data))) >= 0) || ((kec' + ((- 1) * keccak256(data'))) >= 0)) && (!((kec + ((- 1) * keccak256(data))) <= 0) || ((kec' + ((- 1) * keccak256(data'))) <= 0)))\n((!( = 1) || !((kec + ((- 1) * keccak256(data))) = 0)) && (!((kec + ((- 1) * keccak256(data))) <= 0) || ((kec' + ((- 1) * keccak256(data'))) <= 0)) && (!((kec + ((- 1) * keccak256(data))) >= 0) || ((kec' + ((- 1) * keccak256(data'))) >= 0)))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(_kec == kec)\n = 2 -> Assertion failed at assert(kec == keccak256(_data))\n // Warning 4661: (302-333): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_safe.sol b/test/libsolidity/smtCheckerTests/external_calls/external_safe.sol index a2b0f1363..5921189b7 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_safe.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_safe.sol @@ -17,3 +17,4 @@ contract C { // ==== // SMTEngine: all // ---- +// Info 1180: Contract invariant(s) for :C:\n!(x >= 11)\nReentrancy property(ies) for :C:\n!( = 1)\n((!(x <= 10) || !( >= 3)) && (!(x <= 10) || !(x' >= 11)))\n = 0 -> no errors\n = 1 -> Overflow at ++x\n = 3 -> Assertion failed at assert(x < 11)\n diff --git a/test/libsolidity/smtCheckerTests/external_calls/mutex.sol b/test/libsolidity/smtCheckerTests/external_calls/mutex.sol index 977115ec0..79b5ac153 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/mutex.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/mutex.sol @@ -26,4 +26,5 @@ contract C { } // ==== // SMTEngine: all +// SMTIgnoreInv: yes // ---- diff --git a/test/libsolidity/smtCheckerTests/external_calls/staticcall_mutex.sol b/test/libsolidity/smtCheckerTests/external_calls/staticcall_mutex.sol index 30f4392c5..b7fa57197 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/staticcall_mutex.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/staticcall_mutex.sol @@ -23,3 +23,4 @@ contract C { // SMTEngine: all // ---- // Warning 9302: (218-240): Return value of low-level calls not used. +// Info 1180: Reentrancy property(ies) for :C:\n((!lock || ( <= 0)) && (lock' || !lock))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(y == x)\n diff --git a/test/libsolidity/smtCheckerTests/external_calls/staticcall_mutex_2.sol b/test/libsolidity/smtCheckerTests/external_calls/staticcall_mutex_2.sol index bccf18caf..f87cf5f74 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/staticcall_mutex_2.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/staticcall_mutex_2.sol @@ -24,3 +24,4 @@ contract C { // ---- // Warning 9302: (212-234): Return value of low-level calls not used. // Warning 2018: (164-271): Function state mutability can be restricted to view +// Info 1180: Reentrancy property(ies) for :C:\n( <= 0)\n = 0 -> no errors\n = 1 -> Assertion failed at assert(y == x)\n diff --git a/test/libsolidity/smtCheckerTests/external_calls/staticcall_reentrancy_view.sol b/test/libsolidity/smtCheckerTests/external_calls/staticcall_reentrancy_view.sol index 96a73cb5d..ee9e57189 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/staticcall_reentrancy_view.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/staticcall_reentrancy_view.sol @@ -15,3 +15,4 @@ contract C { // Warning 2072: (106-112): Unused local variable. // Warning 2072: (114-131): Unused local variable. // Warning 2018: (72-188): Function state mutability can be restricted to view +// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\nReentrancy property(ies) for :C:\n((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0)))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(x == 0)\n diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_1.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_1.sol index 6887c00db..ace2d56f2 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_external_1.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_external_1.sol @@ -16,4 +16,6 @@ contract C } // ==== // SMTEngine: all +// SMTIgnoreOS: macos // ---- +// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\nReentrancy property(ies) for :C:\n!( = 1)\n((!(x <= 0) || !( >= 2)) && (!(x <= 0) || (x' <= 0)))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(x == y)\n = 2 -> Assertion failed at assert(x == y)\n diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol index bc2fa2dc3..5efcb2da1 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol @@ -22,5 +22,7 @@ contract C // ==== // SMTEngine: all // SMTIgnoreCex: yes +// SMTIgnoreOS: macos // ---- // Warning 6328: (234-253): CHC: Assertion violation happens here. +// Info 1180: Reentrancy property(ies) for :C:\n!( = 1)\n((!((map[1] + ((- 1) * map[0])) <= 0) || ((map'[1] + ((- 1) * map'[0])) <= 0)) && !( = 2) && (!((map[1] + ((- 1) * map[0])) >= 0) || ((map'[0] + ((- 1) * map'[1])) <= 0)))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(map[0] == map[1])\n = 2 -> Assertion failed at assert(map[0] == map[1])\n = 3 -> Assertion failed at assert(map[0] == 0)\n diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_3.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_3.sol index 93273800e..d83970977 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_external_3.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_external_3.sol @@ -18,3 +18,4 @@ contract C // ==== // SMTEngine: all // ---- +// Info 1180: Reentrancy property(ies) for :C:\n!( >= 2)\n( <= 0)\n = 0 -> no errors\n = 1 -> Assertion failed at assert(map[0] == map[1])\n = 2 -> Assertion failed at assert(map[0] == map[1])\n diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identifier_nested_tuple_1.sol b/test/libsolidity/smtCheckerTests/functions/functions_identifier_nested_tuple_1.sol index 2afe4b1ff..fb3228aca 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_identifier_nested_tuple_1.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_identifier_nested_tuple_1.sol @@ -14,3 +14,4 @@ contract C { // ==== // SMTEngine: all // ---- +// Info 1180: Contract invariant(s) for :C:\n((x = 0) || (x = 1))\n diff --git a/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol b/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol index 8b4218b45..530b46900 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol @@ -23,3 +23,4 @@ contract C // ==== // SMTEngine: all // ---- +// Info 1180: Contract invariant(s) for :C:\n(a <= 0)\n diff --git a/test/libsolidity/smtCheckerTests/functions/getters/array_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/array_1.sol index b3f6cad02..421c4fd4f 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/array_1.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/array_1.sol @@ -16,3 +16,4 @@ contract C { // SMTEngine: all // ---- // Warning 6328: (187-201): CHC: Assertion violation happens here.\nCounterexample:\na = [0, 0, 0, 0]\ny = 0\n\nTransaction trace:\nC.constructor()\nState: a = [0, 0, 0, 0]\nC.f() +// Info 1180: Contract invariant(s) for :C:\n!(a.length <= 2)\n diff --git a/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol b/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol index d4e1dc147..ebc7877f0 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol @@ -20,3 +20,4 @@ contract C { // SMTIgnoreCex: yes // ---- // Warning 6328: (242-256): CHC: Assertion violation happens here. +// Info 1180: Contract invariant(s) for :C:\n!(a.length <= 2)\n!(a[2].length <= 3)\n diff --git a/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_1.sol index 5a9b13aff..5038294ed 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_1.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_1.sol @@ -15,3 +15,4 @@ contract D { // ==== // SMTEngine: all // ---- +// Info 1180: Contract invariant(s) for :D:\n(items[1][2][3].y <= 0)\n diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_1.sol index b90bc412a..30907bd67 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_1.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_1.sol @@ -17,3 +17,4 @@ contract C { // SMTEngine: all // ---- // Warning 6328: (210-224): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 42\n\nTransaction trace:\nC.constructor()\nC.f() +// Info 1180: Contract invariant(s) for :C:\n!(m[0].length <= 1)\n diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_10.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_10.sol index 7fa0381b6..56032d9d5 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_10.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_10.sol @@ -20,3 +20,4 @@ contract C { // SMTIgnoreCex: yes // ---- // Warning 6328: (256-270): CHC: Assertion violation happens here. +// Info 1180: Contract invariant(s) for :C:\n!(m.length <= 0)\n!(m[0][1].length <= 2)\n diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_2.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_2.sol index f1afc6e80..c3a3d660d 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_2.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_2.sol @@ -21,3 +21,4 @@ contract C { // SMTIgnoreCex: yes // ---- // Warning 6328: (274-288): CHC: Assertion violation happens here. +// Info 1180: Contract invariant(s) for :C:\n!(m[0].length <= 1)\n!(m[0][1].length <= 2)\n diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_3.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_3.sol index 97cc03919..0083f92d8 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_3.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_3.sol @@ -24,3 +24,4 @@ contract C { // ==== // SMTEngine: all // ---- +// Info 1180: Contract invariant(s) for :C:\n!(m[0].length <= 1)\n!(m[0][1].length <= 2)\n!(m[0][1][2].length <= 3)\n diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_4.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_4.sol index 4aca89ef7..43047758e 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_4.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_4.sol @@ -19,3 +19,4 @@ contract C { // SMTIgnoreCex: yes // ---- // Warning 6328: (260-274): CHC: Assertion violation happens here. +// Info 1180: Contract invariant(s) for :C:\n!(m[0][1].length <= 2)\n diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_5.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_5.sol index ce22da600..2e8abe5dc 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_5.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_5.sol @@ -23,3 +23,4 @@ contract C { // SMTIgnoreCex: yes // ---- // Warning 6328: (354-368): CHC: Assertion violation happens here. +// Info 1180: Contract invariant(s) for :C:\n!(m[0][1].length <= 2)\n!(m[0][1][2].length <= 3)\n diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_6.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_6.sol index 3ad4d94ae..d7964552d 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_6.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_6.sol @@ -19,3 +19,4 @@ contract C { // ==== // SMTEngine: all // ---- +// Info 1180: Contract invariant(s) for :C:\n!(m[0][1][2].length <= 3)\n diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_7.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_7.sol index 5c5af070e..fc4c9efcf 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_7.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_7.sol @@ -16,3 +16,4 @@ contract C { // SMTEngine: all // ---- // Warning 6328: (192-206): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 42\n\nTransaction trace:\nC.constructor()\nC.f() +// Info 1180: Contract invariant(s) for :C:\n!(m.length <= 0)\n diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_8.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_8.sol index 1a0f9a799..0b2b6fadf 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_8.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_8.sol @@ -18,3 +18,4 @@ contract C { // SMTEngine: all // ---- // Warning 6328: (232-246): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 42\n\nTransaction trace:\nC.constructor()\nC.f() +// Info 1180: Contract invariant(s) for :C:\n!(m.length <= 0)\n!(m[0].length <= 1)\n diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_9.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_9.sol index 8df8edad4..be6bc2383 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_9.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_9.sol @@ -16,3 +16,4 @@ contract C { // SMTEngine: all // ---- // Warning 6328: (218-232): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 42\n\nTransaction trace:\nC.constructor()\nC.f() +// Info 1180: Contract invariant(s) for :C:\n!(m.length <= 0)\n diff --git a/test/libsolidity/smtCheckerTests/functions/getters/static_array.sol b/test/libsolidity/smtCheckerTests/functions/getters/static_array.sol index d77ab04e3..d66545e43 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/static_array.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/static_array.sol @@ -13,3 +13,4 @@ contract C { // SMTEngine: all // ---- // Warning 6328: (162-184): CHC: Assertion violation happens here.\nCounterexample:\nx = [42, 1]\n\nTransaction trace:\nC.constructor()\nState: x = [42, 1]\nC.f() +// Info 1180: Contract invariant(s) for :C:\n!(x.length <= 1)\n diff --git a/test/libsolidity/smtCheckerTests/functions/getters/struct_3.sol b/test/libsolidity/smtCheckerTests/functions/getters/struct_3.sol index ddeaa655b..ea433b786 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/struct_3.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/struct_3.sol @@ -22,3 +22,4 @@ contract C { // SMTEngine: all // ---- // Warning 6328: (307-326): CHC: Assertion violation happens here. +// Info 1180: Contract invariant(s) for :C:\n!(m.b.length <= 2)\n diff --git a/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1.sol b/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1.sol index 308332700..c3c231ede 100644 --- a/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1.sol +++ b/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1.sol @@ -19,5 +19,7 @@ contract C{ } // ==== // SMTEngine: all +// SMTIgnoreOS: macos // ---- // Warning 5667: (37-43): Unused function parameter. Remove or comment out the variable name to silence this warning. +// Info 1180: Contract invariant(s) for :C:\n!(x >= 2)\n(!(x <= 0) && !(x >= 2))\n(!(x >= 2) && !(x <= 0))\n diff --git a/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol index 1fe537aad..d067795ac 100644 --- a/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol @@ -26,3 +26,4 @@ contract C{ // Warning 6328: (137-151): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n C.g() -- internal call // Warning 6328: (187-201): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n C.g() -- internal call // Warning 6328: (212-226): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n C.g() -- internal call +// Info 1180: Contract invariant(s) for :C:\n!(x >= 2)\n diff --git a/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1.sol b/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1.sol index 3f17744fb..4bca2544e 100644 --- a/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1.sol +++ b/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1.sol @@ -21,3 +21,4 @@ contract C{ // SMTEngine: all // ---- // Warning 5667: (37-43): Unused function parameter. Remove or comment out the variable name to silence this warning. +// Info 1180: Contract invariant(s) for :C:\n!(x <= 0)\n!(x >= 2)\n(!(x <= 0) && !(x >= 2))\n diff --git a/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1_fail.sol index f03e1b4eb..c0f524e10 100644 --- a/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1_fail.sol @@ -24,3 +24,4 @@ contract C{ // Warning 6328: (49-63): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor(0) // Warning 6328: (105-119): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f() // Warning 6328: (151-165): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n C.g() -- internal call\n C.g() -- internal call +// Info 1180: Contract invariant(s) for :C:\n!(x <= 0)\n!(x >= 2)\n diff --git a/test/libsolidity/smtCheckerTests/functions/super_function_assert.sol b/test/libsolidity/smtCheckerTests/functions/super_function_assert.sol index 58d541a8a..85e97661c 100644 --- a/test/libsolidity/smtCheckerTests/functions/super_function_assert.sol +++ b/test/libsolidity/smtCheckerTests/functions/super_function_assert.sol @@ -31,3 +31,4 @@ contract D is C { // ---- // Warning 6328: (205-219): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nA.proxy()\n C.f() -- internal call\n A.f() -- internal call // Warning 6328: (328-342): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nD.constructor()\nState: x = 0\nA.proxy()\n D.f() -- internal call\n C.f() -- internal call\n A.f() -- internal call +// Info 1180: Contract invariant(s) for :A:\n((x = 0) || (x = 2))\nContract invariant(s) for :D:\n((x = 0) || (x = 2))\n diff --git a/test/libsolidity/smtCheckerTests/functions/this_state.sol b/test/libsolidity/smtCheckerTests/functions/this_state.sol index 4d69e4815..126add640 100644 --- a/test/libsolidity/smtCheckerTests/functions/this_state.sol +++ b/test/libsolidity/smtCheckerTests/functions/this_state.sol @@ -13,3 +13,4 @@ contract C // ==== // SMTEngine: all // ---- +// Info 1180: Contract invariant(s) for :C:\n((x = 0) || (x = 2))\n diff --git a/test/libsolidity/smtCheckerTests/functions/virtual_function_assert.sol b/test/libsolidity/smtCheckerTests/functions/virtual_function_assert.sol index 4c4a8b246..4c5e38131 100644 --- a/test/libsolidity/smtCheckerTests/functions/virtual_function_assert.sol +++ b/test/libsolidity/smtCheckerTests/functions/virtual_function_assert.sol @@ -20,3 +20,4 @@ contract C is A { // SMTEngine: all // ---- // Warning 6328: (227-241): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nA.proxy()\n C.f() -- internal call +// Info 1180: Contract invariant(s) for :A:\n((x >= 0) && (x <= 0))\n diff --git a/test/libsolidity/smtCheckerTests/functions/virtual_function_called_by_constructor.sol b/test/libsolidity/smtCheckerTests/functions/virtual_function_called_by_constructor.sol index 17f3daa79..0117f9b49 100644 --- a/test/libsolidity/smtCheckerTests/functions/virtual_function_called_by_constructor.sol +++ b/test/libsolidity/smtCheckerTests/functions/virtual_function_called_by_constructor.sol @@ -23,6 +23,8 @@ contract C is A { } // ==== // SMTEngine: all +// SMTIgnoreOS: macos // ---- // Warning 6328: (199-214): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nA.constructor()\nState: x = 2\nA.i() // Warning 6328: (387-401): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\n\nTransaction trace:\nC.constructor()\nState: x = 10\nC.i() +// Info 1180: Contract invariant(s) for :A:\n(!(x <= 1) && !(x >= 3))\nContract invariant(s) for :C:\n(!(x >= 11) && !(x <= 9))\n diff --git a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_1.sol b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_1.sol index c86ea3e59..1f05d1176 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_1.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_1.sol @@ -16,3 +16,4 @@ contract C is B { // SMTEngine: all // ---- // Warning 6328: (52-66): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, x = 1\n\nTransaction trace:\nC.constructor()\nState: y = 0, x = 0\nC.g()\n B.f() -- internal call\nState: y = 0, x = 1\nB.f() +// Info 1180: Contract invariant(s) for :B:\n(x <= 0)\n diff --git a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_9.sol b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_9.sol index f97bae5cd..a87a8eeb6 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_9.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_9.sol @@ -30,3 +30,4 @@ contract C is B { // ---- // Warning 6328: (62-76): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nB.f()\n A.f() -- internal call\n C.v() -- internal call // Warning 6328: (131-145): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.f()\n A.v() -- internal call +// Info 1180: Contract invariant(s) for :A:\n(x = 0)\n diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_uses_function_base.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_uses_function_base.sol index e70d37230..0a4599a3d 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/constructor_uses_function_base.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_uses_function_base.sol @@ -18,3 +18,4 @@ contract C is B { // ==== // SMTEngine: all // ---- +// Info 1180: Contract invariant(s) for :C:\n(!(y <= 41) && !(y >= 43))\n diff --git a/test/libsolidity/smtCheckerTests/inheritance/diamond_super_3.sol b/test/libsolidity/smtCheckerTests/inheritance/diamond_super_3.sol index 959e53d45..b8487e321 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/diamond_super_3.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/diamond_super_3.sol @@ -33,3 +33,4 @@ contract E is C,D { // SMTEngine: all // ---- // Warning 6328: (379-394): CHC: Assertion violation happens here.\nCounterexample:\nx = 111\n\nTransaction trace:\nE.constructor()\nState: x = 0\nE.f()\n C.f() -- internal call\n B.f() -- internal call\n A.f() -- internal call +// Info 1180: Contract invariant(s) for :C:\n((x = 0) || (x = 111))\nContract invariant(s) for :D:\n((x = 0) || (x = 101))\nContract invariant(s) for :E:\n((x = 0) || (x = 111))\nContract invariant(s) for :B:\n((x = 0) || (x = 101))\n diff --git a/test/libsolidity/smtCheckerTests/inheritance/implicit_constructor_hierarchy.sol b/test/libsolidity/smtCheckerTests/inheritance/implicit_constructor_hierarchy.sol index 149027691..59d042302 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/implicit_constructor_hierarchy.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/implicit_constructor_hierarchy.sol @@ -16,3 +16,4 @@ contract C is B { // SMTEngine: all // SMTSolvers: z3 // ---- +// Info 1180: Contract invariant(s) for :C:\n(!(x <= 1) && !(x >= 3))\n diff --git a/test/libsolidity/smtCheckerTests/inheritance/implicit_only_constructor_hierarchy.sol b/test/libsolidity/smtCheckerTests/inheritance/implicit_only_constructor_hierarchy.sol index 2b1de17cb..653bb23b7 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/implicit_only_constructor_hierarchy.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/implicit_only_constructor_hierarchy.sol @@ -20,3 +20,4 @@ contract C is B { // SMTEngine: all // SMTSolvers: z3 // ---- +// Info 1180: Contract invariant(s) for :A:\n(x <= 0)\nContract invariant(s) for :C:\n(x <= 0)\nContract invariant(s) for :B:\n(x <= 0)\n diff --git a/test/libsolidity/smtCheckerTests/invariants/state_machine_1.sol b/test/libsolidity/smtCheckerTests/invariants/state_machine_1.sol index beafa4af0..91b96f78c 100644 --- a/test/libsolidity/smtCheckerTests/invariants/state_machine_1.sol +++ b/test/libsolidity/smtCheckerTests/invariants/state_machine_1.sol @@ -32,3 +32,4 @@ contract C { // SMTEngine: all // SMTSolvers: z3 // ---- +// Info 1180: Contract invariant(s) for :C:\n!(x >= 7)\n diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment_multi_branches.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment_multi_branches.sol index 9a578cf89..d3467d0b8 100644 --- a/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment_multi_branches.sol +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment_multi_branches.sol @@ -35,3 +35,4 @@ contract C { // SMTEngine: all // ---- // Warning 6328: (540-554): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, owner = 0x0\ny = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0, owner = 0x0\nC.g(1){ msg.sender: 0x0 } +// Info 1180: Contract invariant(s) for :C:\n(owner <= 0)\n diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_overflow.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_overflow.sol index 13a83ee55..25141b8bf 100644 --- a/test/libsolidity/smtCheckerTests/modifiers/modifier_overflow.sol +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_overflow.sol @@ -15,3 +15,4 @@ contract C // ==== // SMTEngine: all // ---- +// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\n diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_4.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_4.sol index 7da8d0f6a..39be35cb6 100644 --- a/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_4.sol +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_4.sol @@ -39,3 +39,4 @@ contract D is B,C { // Warning 6328: (160-174): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nB.constructor()\nState: x = 0\nA.f() // Warning 6328: (193-207): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nA.f() // Warning 6328: (226-240): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nD.constructor()\nState: x = 0\nA.f() +// Info 1180: Contract invariant(s) for :C:\n((x = 0) || (x = 2))\nContract invariant(s) for :D:\n((x = 0) || (x = 3))\nContract invariant(s) for :B:\n((x = 0) || (x = 1))\n diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_two_invocations_2.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_two_invocations_2.sol index 0a63ed321..5641e2812 100644 --- a/test/libsolidity/smtCheckerTests/modifiers/modifier_two_invocations_2.sol +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_two_invocations_2.sol @@ -17,3 +17,4 @@ contract C // SMTEngine: all // ---- // Warning 6328: (76-90): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f() +// Info 1180: Contract invariant(s) for :C:\n(x = 3)\n diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_virtual_static_call_2.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_virtual_static_call_2.sol index 4bd8f328f..43d41f755 100644 --- a/test/libsolidity/smtCheckerTests/modifiers/modifier_virtual_static_call_2.sol +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_virtual_static_call_2.sol @@ -21,3 +21,4 @@ contract C is A { // SMTEngine: all // ---- // Warning 6328: (83-98): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f() +// Info 1180: Contract invariant(s) for :C:\n((x >= 0) && (x <= 0))\n diff --git a/test/libsolidity/smtCheckerTests/natspec/safe_assert_false_positive_pure.sol b/test/libsolidity/smtCheckerTests/natspec/safe_assert_false_positive_pure.sol index 11fcbf6f6..ed160d95c 100644 --- a/test/libsolidity/smtCheckerTests/natspec/safe_assert_false_positive_pure.sol +++ b/test/libsolidity/smtCheckerTests/natspec/safe_assert_false_positive_pure.sol @@ -28,3 +28,4 @@ contract C { // Warning 2018: (33-335): Function state mutability can be restricted to view // Warning 2018: (457-524): Function state mutability can be restricted to pure // Warning 6328: (135-150): CHC: Assertion violation happens here. +// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\n(y <= 0)\n diff --git a/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol b/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol index 3331b57de..284f9bcbd 100644 --- a/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol +++ b/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol @@ -29,3 +29,4 @@ contract A { // SMTIgnoreCex: yes // ---- // Warning 6328: (392-408): CHC: Assertion violation happens here. +// Info 1180: Contract invariant(s) for :A:\n(((x = (- 2)) && (y = (- 2))) || ((x = 0) && (y = 0)))\n(((x = 0) && (y = 0)) || ((x = (- 2)) && (y = (- 2))))\n diff --git a/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array.sol b/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array.sol index 3df77d2fb..292eab85d 100644 --- a/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array.sol +++ b/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array.sol @@ -13,3 +13,4 @@ contract A { // SMTEngine: all // ---- // Warning 6328: (124-146): CHC: Assertion violation happens here.\nCounterexample:\na = []\n\nTransaction trace:\nA.constructor()\nState: a = []\nA.f() +// Info 1180: Contract invariant(s) for :A:\n(a.length <= 0)\n diff --git a/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array_3.sol b/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array_3.sol index fac19a6ff..7a925d134 100644 --- a/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array_3.sol +++ b/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array_3.sol @@ -30,3 +30,4 @@ contract A { // Warning 6328: (311-328): CHC: Assertion violation happens here.\nCounterexample:\na = [0, 0]\nb = [0, 0]\n\nTransaction trace:\nA.constructor()\nState: a = [1]\nA.f() // Warning 6368: (422-426): CHC: Out of bounds access happens here.\nCounterexample:\na = [0, 0]\nu = []\nb = [0, 0]\n\nTransaction trace:\nA.constructor()\nState: a = [1]\nA.f() // Warning 6328: (415-432): CHC: Assertion violation happens here.\nCounterexample:\na = [0, 0]\nb = [0, 0]\n\nTransaction trace:\nA.constructor()\nState: a = [1]\nA.f() +// Info 1180: Contract invariant(s) for :A:\n!(a.length <= 0)\n diff --git a/test/libsolidity/smtCheckerTests/operators/assignment_module_contract_member_variable.sol b/test/libsolidity/smtCheckerTests/operators/assignment_module_contract_member_variable.sol index d1387ee8e..e4b764686 100644 --- a/test/libsolidity/smtCheckerTests/operators/assignment_module_contract_member_variable.sol +++ b/test/libsolidity/smtCheckerTests/operators/assignment_module_contract_member_variable.sol @@ -30,3 +30,4 @@ contract A { // ---- // Warning 6328: (AASource:159-178): CHC: Assertion violation happens here.\nCounterexample:\nx = (- 1), y = (- 2)\n\nTransaction trace:\nA.constructor()\nState: x = 0, y = 0\nA.a()\nState: x = (- 2), y = (- 2)\nA.a() // Warning 6328: (AASource:370-386): CHC: Assertion violation happens here.\nCounterexample:\nx = 8, y = (- 2)\n\nTransaction trace:\nA.constructor()\nState: x = 0, y = 0\nA.a() +// Info 1180: Contract invariant(s) for AASource:A:\n(((x = (- 2)) && (y = (- 2))) || ((x = 0) && (y = 0)))\n(((x = 0) && (y = 0)) || ((x = (- 2)) && (y = (- 2))))\n diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol index 17c812aec..9b27a277b 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol @@ -19,3 +19,4 @@ contract C { // ==== // SMTEngine: all // ---- +// Info 1180: Contract invariant(s) for :C:\n!(s.x.length <= 2)\n diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol index 58afa2413..e37d3f84c 100644 --- a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol +++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol @@ -22,5 +22,7 @@ contract C { } // ==== // SMTEngine: all +// SMTIgnoreOS: macos // ---- // Warning 2072: (255-261): Unused local variable. +// Info 1180: Reentrancy property(ies) for :C:\n((!(x <= 2) || !(x' >= 3)) && ( <= 0) && (!(x' <= 0) || !(x >= 2)))\n((!(x' <= 0) || ((x' + ((- 1) * x)) = 0)) && ( <= 0) && (!(x' >= 3) || ((x' + ((- 1) * x)) = 0)))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(x == 2 || x == 1)\n diff --git a/test/libsolidity/smtCheckerTests/operators/delete_array_2d.sol b/test/libsolidity/smtCheckerTests/operators/delete_array_2d.sol index bda1c07f2..32f2526cc 100644 --- a/test/libsolidity/smtCheckerTests/operators/delete_array_2d.sol +++ b/test/libsolidity/smtCheckerTests/operators/delete_array_2d.sol @@ -17,3 +17,4 @@ contract C // ==== // SMTEngine: all // ---- +// Info 1180: Contract invariant(s) for :C:\n(true && !(a.length <= 2))\n(true && !(a[2].length <= 3))\n diff --git a/test/libsolidity/smtCheckerTests/operators/delete_array_index.sol b/test/libsolidity/smtCheckerTests/operators/delete_array_index.sol index ea9c4f55a..4f9001115 100644 --- a/test/libsolidity/smtCheckerTests/operators/delete_array_index.sol +++ b/test/libsolidity/smtCheckerTests/operators/delete_array_index.sol @@ -20,4 +20,5 @@ contract C // ==== // SMTEngine: all // ---- +// Info 1180: Contract invariant(s) for :C:\n!(a.length <= 2)\n // Warning 6838: (154-155): BMC: Condition is always false. diff --git a/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol b/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol index b0ec97d98..80a692429 100644 --- a/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol +++ b/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol @@ -27,4 +27,5 @@ contract C // SMTIgnoreCex: yes // ---- // Warning 6328: (315-335): CHC: Assertion violation might happen here. +// Info 1180: Contract invariant(s) for :C:\n!(a.length <= 1)\n // Warning 4661: (315-335): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/delete_function.sol b/test/libsolidity/smtCheckerTests/operators/delete_function.sol index f40a02c93..63dad1ab0 100644 --- a/test/libsolidity/smtCheckerTests/operators/delete_function.sol +++ b/test/libsolidity/smtCheckerTests/operators/delete_function.sol @@ -28,4 +28,5 @@ contract C // ==== // SMTEngine: all // ---- +// Info 1180: Contract invariant(s) for :C:\n!(a.length <= 2)\n // Warning 6838: (262-263): BMC: Condition is always true. diff --git a/test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol b/test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol index 6de2c9c61..ae526775f 100644 --- a/test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol +++ b/test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol @@ -23,4 +23,5 @@ contract C { // SMTIgnoreCex: yes // ---- // Warning 6328: (335-354): CHC: Assertion violation might happen here. +// Info 1180: Contract invariant(s) for :C:\n!(a.length <= 2)\n!(a.length <= 3)\n // Warning 4661: (335-354): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/unary_add_array_push_2.sol b/test/libsolidity/smtCheckerTests/operators/unary_add_array_push_2.sol index 0c2fdba6f..b1cef5e40 100644 --- a/test/libsolidity/smtCheckerTests/operators/unary_add_array_push_2.sol +++ b/test/libsolidity/smtCheckerTests/operators/unary_add_array_push_2.sol @@ -18,3 +18,4 @@ contract C { // ==== // SMTEngine: all // ---- +// Info 1180: Contract invariant(s) for :C:\n!(data.length <= 1)\n!(data[1].d.length <= 3)\n diff --git a/test/libsolidity/smtCheckerTests/out_of_bounds/array_1.sol b/test/libsolidity/smtCheckerTests/out_of_bounds/array_1.sol index 8997abbe6..ee57f069d 100644 --- a/test/libsolidity/smtCheckerTests/out_of_bounds/array_1.sol +++ b/test/libsolidity/smtCheckerTests/out_of_bounds/array_1.sol @@ -18,7 +18,10 @@ contract C { } // ==== // SMTEngine: all +// SMTIgnoreOS: macos // ---- // Warning 4984: (112-115): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. +// Warning 3944: (181-184): CHC: Underflow (resulting value less than 0) might happen here. // Warning 6368: (259-263): CHC: Out of bounds access happens here.\nCounterexample:\na = [0], l = 1\n = 0\n\nTransaction trace:\nC.constructor()\nState: a = [], l = 0\nC.p()\nState: a = [0], l = 1\nC.r() // Warning 2661: (112-115): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 4144: (181-184): BMC: Underflow (resulting value less than 0) happens here. diff --git a/test/libsolidity/smtCheckerTests/out_of_bounds/array_2.sol b/test/libsolidity/smtCheckerTests/out_of_bounds/array_2.sol index 6adc6273c..d331abef7 100644 --- a/test/libsolidity/smtCheckerTests/out_of_bounds/array_2.sol +++ b/test/libsolidity/smtCheckerTests/out_of_bounds/array_2.sol @@ -21,3 +21,4 @@ contract C { // ==== // SMTEngine: all // ---- +// Info 1180: Contract invariant(s) for :C:\n((l + ((- 1) * a.length)) <= 0)\n diff --git a/test/libsolidity/smtCheckerTests/overflow/signed_guard_sub_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/signed_guard_sub_overflow.sol index afaeb5448..b28b6598c 100644 --- a/test/libsolidity/smtCheckerTests/overflow/signed_guard_sub_overflow.sol +++ b/test/libsolidity/smtCheckerTests/overflow/signed_guard_sub_overflow.sol @@ -6,5 +6,6 @@ contract C { } // ==== // SMTEngine: all +// SMTIgnoreOS: macos // ---- // Warning 4984: (96-101): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\nx = 0\ny = (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)) diff --git a/test/libsolidity/smtCheckerTests/special/msg_value_3.sol b/test/libsolidity/smtCheckerTests/special/msg_value_3.sol index 8d35e1754..79302b142 100644 --- a/test/libsolidity/smtCheckerTests/special/msg_value_3.sol +++ b/test/libsolidity/smtCheckerTests/special/msg_value_3.sol @@ -13,3 +13,4 @@ contract C { // ==== // SMTEngine: all // ---- +// Info 1180: Contract invariant(s) for :C:\nlock\n diff --git a/test/libsolidity/smtCheckerTests/special/msg_vars_chc_internal.sol b/test/libsolidity/smtCheckerTests/special/msg_vars_chc_internal.sol index b7984d21e..475cc2291 100644 --- a/test/libsolidity/smtCheckerTests/special/msg_vars_chc_internal.sol +++ b/test/libsolidity/smtCheckerTests/special/msg_vars_chc_internal.sol @@ -8,6 +8,7 @@ contract C { sender = msg.sender; sig = msg.sig; value = msg.value; + require(value == 42); g(); } @@ -28,4 +29,4 @@ contract C { // ==== // SMTEngine: chc // ---- -// Warning 6328: (621-644): CHC: Assertion violation happens here.\nCounterexample:\ndata = [0x26, 0x12, 0x1f, 0xf0], sender = 0x0, sig = 0x26121ff0, value = 0\n\nTransaction trace:\nC.constructor()\nState: data = [], sender = 0x0, sig = 0x0, value = 0\nC.f(){ msg.data: [0x26, 0x12, 0x1f, 0xf0], msg.sender: 0x0, msg.sig: 0x26121ff0, msg.value: 0 }\n C.g() -- internal call +// Warning 6328: (645-668): CHC: Assertion violation happens here.\nCounterexample:\ndata = [0x26, 0x12, 0x1f, 0xf0], sender = 0x0, sig = 0x26121ff0, value = 42\n\nTransaction trace:\nC.constructor()\nState: data = [], sender = 0x0, sig = 0x0, value = 0\nC.f(){ msg.data: [0x26, 0x12, 0x1f, 0xf0], msg.sender: 0x0, msg.sig: 0x26121ff0, msg.value: 42 }\n C.g() -- internal call diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_4.sol b/test/libsolidity/smtCheckerTests/try_catch/try_4.sol index 6988906a2..0abf62df8 100644 --- a/test/libsolidity/smtCheckerTests/try_catch/try_4.sol +++ b/test/libsolidity/smtCheckerTests/try_catch/try_4.sol @@ -28,4 +28,5 @@ contract C { // Warning 1218: (178-192): CHC: Error trying to invoke SMT solver. // Warning 6328: (178-192): CHC: Assertion violation might happen here. // Warning 6328: (318-332): CHC: Assertion violation happens here. +// Info 1180: Reentrancy property(ies) for :C:\n!( = 2)\n = 0 -> no errors\n = 1 -> Assertion failed at assert(x == 0)\n = 2 -> Assertion failed at assert(x == 0)\n = 3 -> Assertion failed at assert(x == 1)\n // Warning 4661: (178-192): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_5.sol b/test/libsolidity/smtCheckerTests/try_catch/try_5.sol index 6c9b776c4..236a26f1b 100644 --- a/test/libsolidity/smtCheckerTests/try_catch/try_5.sol +++ b/test/libsolidity/smtCheckerTests/try_catch/try_5.sol @@ -26,3 +26,4 @@ contract C { // SMTEngine: all // ---- // Warning 6328: (315-329): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f() +// Info 1180: Reentrancy property(ies) for :C:\n!( = 2)\n((!(x' >= 100) || ((x' + ((- 1) * x)) = 0)) && !( = 1))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(x < 100)\n = 2 -> Assertion failed at assert(x == 0)\n = 3 -> Assertion failed at assert(x == 1)\n diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values.sol b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values.sol index 80ebe0d93..abef4c76a 100644 --- a/test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values.sol +++ b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values.sol @@ -25,3 +25,4 @@ contract C { // Warning 6328: (185-199): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\nx = 1\nc = false\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f()\n d.d() -- untrusted external call // Warning 6328: (273-283): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\nx = 1\nc = true\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f()\n d.d() -- untrusted external call // Warning 6328: (393-407): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f() +// Info 1180: Reentrancy property(ies) for :C:\n!( = 3)\n = 0 -> no errors\n = 1 -> Assertion failed at assert(x == 0)\n = 2 -> Assertion failed at assert(!c)\n = 3 -> Assertion failed at assert(x == 0)\n = 4 -> Assertion failed at assert(x == 1)\n diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_public_var_mapping.sol b/test/libsolidity/smtCheckerTests/try_catch/try_public_var_mapping.sol index 3048558e7..0854dedd1 100644 --- a/test/libsolidity/smtCheckerTests/try_catch/try_public_var_mapping.sol +++ b/test/libsolidity/smtCheckerTests/try_catch/try_public_var_mapping.sol @@ -19,5 +19,7 @@ contract C { } // ==== // SMTEngine: all +// SMTIgnoreOS: macos // ---- // Warning 6328: (280-300): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Info 1180: Contract invariant(s) for :C:\n!(m[0].length <= 1)\n(!(m[0][1] >= 43) && !(m[0][1] <= 41))\n diff --git a/test/libsolidity/smtCheckerTests/typecast/address_literal.sol b/test/libsolidity/smtCheckerTests/typecast/address_literal.sol index d56275fed..40540bb51 100644 --- a/test/libsolidity/smtCheckerTests/typecast/address_literal.sol +++ b/test/libsolidity/smtCheckerTests/typecast/address_literal.sol @@ -23,3 +23,4 @@ contract C { // SMTEngine: all // ---- // Warning 6328: (454-468): CHC: Assertion violation happens here.\nCounterexample:\nx = 0x0\na = 0x0\nb = 0x01\nc = 0x0\nd = 0x0\ne = 0x12345678\n\nTransaction trace:\nC.constructor()\nState: x = 0x0\nC.g() +// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\n diff --git a/test/libsolidity/smtCheckerTests/types/address_call.sol b/test/libsolidity/smtCheckerTests/types/address_call.sol index 568ab91e1..8ea389482 100644 --- a/test/libsolidity/smtCheckerTests/types/address_call.sol +++ b/test/libsolidity/smtCheckerTests/types/address_call.sol @@ -19,6 +19,8 @@ contract C // EVMVersion: >spuriousDragon // SMTEngine: all // SMTIgnoreCex: yes +// SMTIgnoreInv: yes +// SMTIgnoreOS: macos // ---- // Warning 2072: (127-166): Unused local variable. // Warning 2072: (191-207): Unused local variable. diff --git a/test/libsolidity/smtCheckerTests/types/address_staticcall.sol b/test/libsolidity/smtCheckerTests/types/address_staticcall.sol index 40d867fa0..11b862a10 100644 --- a/test/libsolidity/smtCheckerTests/types/address_staticcall.sol +++ b/test/libsolidity/smtCheckerTests/types/address_staticcall.sol @@ -20,3 +20,4 @@ contract C // ---- // Warning 2072: (191-207): Unused local variable. // Warning 6328: (233-248): CHC: Assertion violation happens here. +// Info 1180: Reentrancy property(ies) for :C:\n!( >= 2)\n!( >= 3)\n!( >= 4)\n = 0 -> no errors\n = 1 -> Assertion failed at assert(success)\n = 2 -> Assertion failed at assert(x == 0)\n = 3 -> Assertion failed at assert(map[0] == 0)\n = 4 -> Assertion failed at assert(localMap[0] == 0)\n diff --git a/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_3.sol b/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_3.sol index 36b851ff3..7e89f1c9d 100644 --- a/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_3.sol +++ b/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_3.sol @@ -28,3 +28,4 @@ contract C // ==== // SMTEngine: all // ---- +// Info 1180: Contract invariant(s) for :C:\n!(array.length <= 0)\n diff --git a/test/libsolidity/smtCheckerTests/types/array_branch_3d.sol b/test/libsolidity/smtCheckerTests/types/array_branch_3d.sol index c13842daa..fad9d2bba 100644 --- a/test/libsolidity/smtCheckerTests/types/array_branch_3d.sol +++ b/test/libsolidity/smtCheckerTests/types/array_branch_3d.sol @@ -23,3 +23,4 @@ contract C // Warning 6368: (177-184): CHC: Out of bounds access might happen here. // Warning 6368: (177-187): CHC: Out of bounds access might happen here. // Warning 6328: (170-192): CHC: Assertion violation happens here.\nCounterexample:\nc = [[[0]]]\nb = false\n\nTransaction trace:\nC.constructor()\nState: c = [[[0]]]\nC.f(false) +// Info 1180: Contract invariant(s) for :C:\n!(c.length <= 0)\n diff --git a/test/libsolidity/smtCheckerTests/types/array_branches_3d.sol b/test/libsolidity/smtCheckerTests/types/array_branches_3d.sol index ebd28101d..b2fd91327 100644 --- a/test/libsolidity/smtCheckerTests/types/array_branches_3d.sol +++ b/test/libsolidity/smtCheckerTests/types/array_branches_3d.sol @@ -22,3 +22,4 @@ contract C // Warning 6368: (152-162): CHC: Out of bounds access might happen here. // Warning 6368: (177-184): CHC: Out of bounds access might happen here. // Warning 6368: (177-187): CHC: Out of bounds access might happen here. +// Info 1180: Contract invariant(s) for :C:\n!(c.length <= 0)\n diff --git a/test/libsolidity/smtCheckerTests/types/array_branches_3d_show_unproved.sol b/test/libsolidity/smtCheckerTests/types/array_branches_3d_show_unproved.sol index 6ec629c9f..689fc045d 100644 --- a/test/libsolidity/smtCheckerTests/types/array_branches_3d_show_unproved.sol +++ b/test/libsolidity/smtCheckerTests/types/array_branches_3d_show_unproved.sol @@ -23,3 +23,4 @@ contract C // Warning 6368: (152-162): CHC: Out of bounds access might happen here. // Warning 6368: (177-184): CHC: Out of bounds access might happen here. // Warning 6368: (177-187): CHC: Out of bounds access might happen here. +// Info 1180: Contract invariant(s) for :C:\n!(c.length <= 0)\n diff --git a/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol b/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol index 07e09a9e8..dd0d8e004 100644 --- a/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol +++ b/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol @@ -43,3 +43,4 @@ contract C // Warning 6368: (850-869): CHC: Out of bounds access happens here. // Warning 6328: (936-956): CHC: Assertion violation happens here. // Warning 6368: (1029-1043): CHC: Out of bounds access might happen here. +// Info 1180: Contract invariant(s) for :C:\n!(severalMaps8.length <= 0)\n diff --git a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol index cde229e4f..f415cfd95 100644 --- a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol +++ b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol @@ -28,3 +28,4 @@ contract C // SMTIgnoreCex: yes // ---- // Warning 6328: (456-487): CHC: Assertion violation happens here. +// Info 1180: Contract invariant(s) for :C:\n!(severalMaps3d.length <= 1)\n!(severalMaps8.length <= 1)\n diff --git a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol index 8ebd7025d..f9aa3a650 100644 --- a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol +++ b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol @@ -33,3 +33,4 @@ contract C // Warning 6328: (860-880): CHC: Assertion violation happens here. // Warning 6368: (936-952): CHC: Out of bounds access might happen here. // Warning 6368: (936-955): CHC: Out of bounds access might happen here. +// Info 1180: Contract invariant(s) for :C:\n!(severalMaps8.length <= 1)\n diff --git a/test/libsolidity/smtCheckerTests/types/enum_explicit_values.sol b/test/libsolidity/smtCheckerTests/types/enum_explicit_values.sol index fda74030e..edc35f802 100644 --- a/test/libsolidity/smtCheckerTests/types/enum_explicit_values.sol +++ b/test/libsolidity/smtCheckerTests/types/enum_explicit_values.sol @@ -11,3 +11,4 @@ contract C // ==== // SMTEngine: all // ---- +// Info 1180: Contract invariant(s) for :C:\n((d = 0) || (d = 1))\n diff --git a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_1.sol b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_1.sol index 2aee19042..6a24c1e9c 100644 --- a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_1.sol +++ b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_1.sol @@ -7,3 +7,4 @@ contract c { // ==== // SMTEngine: all // ---- +// Info 1180: Contract invariant(s) for :c:\n!(data2.length <= 5)\n diff --git a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol index 941cfd237..b55293231 100644 --- a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol +++ b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol @@ -30,5 +30,8 @@ contract C { } // ==== // SMTEngine: all +// SMTIgnoreOS: macos // ---- +// Warning 6368: (374-381): CHC: Out of bounds access might happen here. // Warning 6368: (456-462): CHC: Out of bounds access happens here. +// Info 1180: Contract invariant(s) for :C:\n!(a.length <= 4)\n diff --git a/test/libsolidity/smtCheckerTests/types/mapping_4.sol b/test/libsolidity/smtCheckerTests/types/mapping_4.sol index c5b035740..ba6688cd5 100644 --- a/test/libsolidity/smtCheckerTests/types/mapping_4.sol +++ b/test/libsolidity/smtCheckerTests/types/mapping_4.sol @@ -10,3 +10,4 @@ contract C // SMTEngine: all // SMTSolvers: z3 // ---- +// Info 1180: Contract invariant(s) for :C:\n!map[true]\n diff --git a/test/libsolidity/smtCheckerTests/types/static_array_length_5.sol b/test/libsolidity/smtCheckerTests/types/static_array_length_5.sol index f632f3bc8..e3ab2189c 100644 --- a/test/libsolidity/smtCheckerTests/types/static_array_length_5.sol +++ b/test/libsolidity/smtCheckerTests/types/static_array_length_5.sol @@ -11,3 +11,4 @@ contract C { // ---- // Warning 6328: (95-115): CHC: Assertion violation happens here.\nCounterexample:\na = [0, 0]\n\nTransaction trace:\nC.constructor()\nState: a = [0, 0]\nC.f() // Warning 6328: (134-154): CHC: Assertion violation happens here.\nCounterexample:\na = [0, 0]\n\nTransaction trace:\nC.constructor()\nState: a = [0, 0]\nC.f() +// Info 1180: Contract invariant(s) for :C:\n(!(a.length <= 1) && !(a.length >= 3))\n diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_state_constructor.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_state_constructor.sol index 7c31c616c..986781b77 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_state_constructor.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_state_constructor.sol @@ -13,3 +13,4 @@ contract C { // ==== // SMTEngine: all // ---- +// Info 1180: Contract invariant(s) for :C:\n(!(s.x <= 41) && !(s.x >= 43))\n diff --git a/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_7.sol b/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_7.sol index f1b128162..60b305402 100644 --- a/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_7.sol +++ b/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_7.sol @@ -12,3 +12,4 @@ contract C { // ==== // SMTEngine: all // ---- +// Info 1180: Reentrancy property(ies) for :C:\n!( >= 2)\n( <= 0)\n = 0 -> no errors\n = 1 -> Assertion failed at assert(x == 2)\n = 2 -> Assertion failed at assert(y == 3)\n diff --git a/test/libsolidity/smtCheckerTests/userTypes/mapping_1.sol b/test/libsolidity/smtCheckerTests/userTypes/mapping_1.sol index 52ea82800..120348a04 100644 --- a/test/libsolidity/smtCheckerTests/userTypes/mapping_1.sol +++ b/test/libsolidity/smtCheckerTests/userTypes/mapping_1.sol @@ -6,5 +6,8 @@ contract C { assert(m[a] != 0); // should fail } } +// ==== +// SMTEngine: all +// SMTIgnoreInv: yes // ---- // Warning 6328: (134-151): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\n\nTransaction trace:\nC.constructor()\nC.f(0) diff --git a/test/solc/CommandLineParser.cpp b/test/solc/CommandLineParser.cpp index 3b2998ce1..663bf022c 100644 --- a/test/solc/CommandLineParser.cpp +++ b/test/solc/CommandLineParser.cpp @@ -149,6 +149,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options) "--model-checker-contracts=contract1.yul:A,contract2.yul:B", "--model-checker-div-mod-no-slacks", "--model-checker-engine=bmc", + "--model-checker-invariants=contract,reentrancy", "--model-checker-show-unproved", "--model-checker-solvers=z3,smtlib2", "--model-checker-targets=underflow,divByZero", @@ -212,6 +213,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options) {{{"contract1.yul", {"A"}}, {"contract2.yul", {"B"}}}}, true, {true, false}, + {{InvariantType::Contract, InvariantType::Reentrancy}}, true, {false, true, true}, {{VerificationTargetType::Underflow, VerificationTargetType::DivByZero}}, @@ -285,6 +287,7 @@ BOOST_AUTO_TEST_CASE(assembly_mode_options) "contract2.yul:B", "--model-checker-div-mod-no-slacks", // Ignored in assembly mode "--model-checker-engine=bmc", // Ignored in assembly mode + "--model-checker-invariants=contract,reentrancy", // Ignored in assembly mode "--model-checker-show-unproved", // Ignored in assembly mode "--model-checker-solvers=z3,smtlib2", // Ignored in assembly mode "--model-checker-targets=" // Ignored in assembly mode @@ -375,6 +378,7 @@ BOOST_AUTO_TEST_CASE(standard_json_mode_options) "contract2.yul:B", "--model-checker-div-mod-no-slacks", // Ignored in Standard JSON mode "--model-checker-engine=bmc", // Ignored in Standard JSON mode + "--model-checker-invariants=contract,reentrancy", // Ignored in Standard JSON mode "--model-checker-show-unproved", // Ignored in Standard JSON mode "--model-checker-solvers=z3,smtlib2", // Ignored in Standard JSON mode "--model-checker-targets=" // Ignored in Standard JSON mode diff --git a/test/tools/fuzzer_common.cpp b/test/tools/fuzzer_common.cpp index 332b9fc04..82066bf52 100644 --- a/test/tools/fuzzer_common.cpp +++ b/test/tools/fuzzer_common.cpp @@ -106,6 +106,7 @@ void FuzzerUtil::testCompiler( frontend::ModelCheckerContracts::Default(), /*divModWithSlacks*/true, frontend::ModelCheckerEngine::All(), + frontend::ModelCheckerInvariants::All(), /*showUnproved=*/false, smtutil::SMTSolverChoice::All(), frontend::ModelCheckerTargets::Default(),