diff --git a/CMakeLists.txt b/CMakeLists.txt index 73e7930b7..29a23a20e 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -75,63 +75,6 @@ configure_file("${PROJECT_SOURCE_DIR}/cmake/templates/license.h.in" include/lice include(EthOptions) configure_project(TESTS) -set(LATEST_Z3_VERSION "4.12.1") -set(MINIMUM_Z3_VERSION "4.8.16") -find_package(Z3) -if (${Z3_FOUND}) - if (${STRICT_Z3_VERSION}) - if (NOT ("${Z3_VERSION_STRING}" VERSION_EQUAL ${LATEST_Z3_VERSION})) - message( - FATAL_ERROR - "SMTChecker tests require Z3 ${LATEST_Z3_VERSION} for all tests to pass.\n\ -Build with -DSTRICT_Z3_VERSION=OFF if you want to use a different version. \ -You can also use -DUSE_Z3=OFF to build without Z3. In both cases use --no-smt when running tests." - ) - endif() - else() - if ("${Z3_VERSION_STRING}" VERSION_LESS ${MINIMUM_Z3_VERSION}) - message( - FATAL_ERROR - "Solidity requires Z3 ${MINIMUM_Z3_VERSION} or newer. You can also use -DUSE_Z3=OFF to build without Z3." - ) - endif() - endif() -endif() - -if(${USE_Z3_DLOPEN}) - add_definitions(-DHAVE_Z3) - add_definitions(-DHAVE_Z3_DLOPEN) - find_package(Python3 COMPONENTS Interpreter) - if(${Z3_FOUND}) - get_target_property(Z3_HEADER_HINTS z3::libz3 INTERFACE_INCLUDE_DIRECTORIES) - endif() - find_path(Z3_HEADER_PATH z3.h HINTS ${Z3_HEADER_HINTS}) - if(Z3_HEADER_PATH) - set(Z3_FOUND TRUE) - else() - message(SEND_ERROR "Dynamic loading of Z3 requires Z3 headers to be present at build time.") - endif() - if(NOT ${Python3_FOUND}) - message(SEND_ERROR "Dynamic loading of Z3 requires Python 3 to be present at build time.") - endif() - if(${SOLC_LINK_STATIC}) - message(SEND_ERROR "solc cannot be linked statically when dynamically loading Z3.") - endif() -elseif (${Z3_FOUND}) - add_definitions(-DHAVE_Z3) - message("Z3 SMT solver found. This enables optional SMT checking with Z3.") -endif() - -find_package(CVC4 QUIET) -if (${CVC4_FOUND}) - add_definitions(-DHAVE_CVC4) - message("CVC4 SMT solver found. This enables optional SMT checking with CVC4.") -endif() - -if (NOT (${Z3_FOUND} OR ${CVC4_FOUND})) - message("No SMT solver found (or it has been forcefully disabled). Optional SMT checking will not be available.\ - \nPlease install Z3 or CVC4 or remove the option disabling them (USE_Z3, USE_CVC4).") -endif() add_subdirectory(libsolutil) add_subdirectory(liblangutil) diff --git a/libsmtutil/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp index ef7c56ac0..c3e763841 100644 --- a/libsmtutil/CHCSmtLib2Interface.cpp +++ b/libsmtutil/CHCSmtLib2Interface.cpp @@ -18,22 +18,35 @@ #include +#include + #include +#include +#include + +#include + #include #include #include +#include +#include #include #include #include #include +#include #include +#include +#include using namespace solidity; using namespace solidity::util; using namespace solidity::frontend; +using namespace solidity::langutil; using namespace solidity::smtutil; CHCSmtLib2Interface::CHCSmtLib2Interface( @@ -43,7 +56,7 @@ CHCSmtLib2Interface::CHCSmtLib2Interface( std::optional _queryTimeout ): CHCSolverInterface(_queryTimeout), - m_smtlib2(std::make_unique(_queryResponses, _smtCallback, m_queryTimeout)), + m_smtlib2(std::make_unique(_queryResponses, _smtCallback, _enabledSolvers, m_queryTimeout)), m_queryResponses(std::move(_queryResponses)), m_smtCallback(_smtCallback), m_enabledSolvers(_enabledSolvers) @@ -56,7 +69,6 @@ void CHCSmtLib2Interface::reset() m_accumulatedOutput.clear(); m_variables.clear(); m_unhandledQueries.clear(); - m_sortNames.clear(); } void CHCSmtLib2Interface::registerRelation(Expression const& _expr) @@ -96,9 +108,15 @@ std::tuple CHCSmtLib2Inte CheckResult result; // TODO proper parsing if (boost::starts_with(response, "sat")) + { result = CheckResult::UNSATISFIABLE; + return {result, invariantsFromSMTLib(response), {}}; + } else if (boost::starts_with(response, "unsat")) + { result = CheckResult::SATISFIABLE; + return {result, Expression(true), graphFromZ3Proof(response)}; + } else if (boost::starts_with(response, "unknown")) result = CheckResult::UNKNOWN; else @@ -115,24 +133,18 @@ void CHCSmtLib2Interface::declareVariable(std::string const& _name, SortPointer else if (!m_variables.count(_name)) { m_variables.insert(_name); - write("(declare-var |" + _name + "| " + toSmtLibSort(*_sort) + ')'); + write("(declare-var |" + _name + "| " + toSmtLibSort(_sort) + ')'); } } -std::string CHCSmtLib2Interface::toSmtLibSort(Sort const& _sort) +std::string CHCSmtLib2Interface::toSmtLibSort(SortPointer _sort) { - if (!m_sortNames.count(&_sort)) - m_sortNames[&_sort] = m_smtlib2->toSmtLibSort(_sort); - return m_sortNames.at(&_sort); + return m_smtlib2->toSmtLibSort(_sort); } std::string CHCSmtLib2Interface::toSmtLibSort(std::vector const& _sorts) { - std::string ssort("("); - for (auto const& sort: _sorts) - ssort += toSmtLibSort(*sort) + " "; - ssort += ")"; - return ssort; + return m_smtlib2->toSmtLibSort(_sorts); } std::string CHCSmtLib2Interface::forall() @@ -142,7 +154,7 @@ std::string CHCSmtLib2Interface::forall() { solAssert(sort, ""); if (sort->kind != Kind::Function) - vars += " (" + name + " " + toSmtLibSort(*sort) + ")"; + vars += " (" + name + " " + toSmtLibSort(sort) + ")"; } vars += ")"; return vars; @@ -158,7 +170,7 @@ void CHCSmtLib2Interface::declareFunction(std::string const& _name, SortPointer auto fSort = std::dynamic_pointer_cast(_sort); smtAssert(fSort->codomain); std::string domain = toSmtLibSort(fSort->domain); - std::string codomain = toSmtLibSort(*fSort->codomain); + std::string codomain = toSmtLibSort(fSort->codomain); m_variables.insert(_name); write( "(declare-fun |" + @@ -183,12 +195,41 @@ std::string CHCSmtLib2Interface::querySolver(std::string const& _input) if (m_queryResponses.count(inputHash)) return m_queryResponses.at(inputHash); - smtAssert(m_enabledSolvers.smtlib2 || m_enabledSolvers.eld); - if (m_smtCallback) + smtAssert(m_enabledSolvers.eld || m_enabledSolvers.z3); + smtAssert(m_smtCallback, "Callback must be set!"); + std::string solverBinary = [&](){ + if (m_enabledSolvers.eld) + return "eld -ssol"; // TODO: Use -scex to get counterexamples, but Eldarica uses different format than Z3 + if (m_enabledSolvers.z3) + return "z3 -in rlimit=1000000 fp.spacer.q3.use_qgen=true fp.spacer.mbqi=false fp.spacer.ground_pobs=false"; + return ""; + }(); + std::string z3Input = _input + "(get-model)\n"; + auto const& query = boost::starts_with(solverBinary, "z3") ? z3Input : _input; + auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery) + ":" + solverBinary, query); + if (result.success) { - auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery), _input); - if (result.success) - return result.responseOrErrorMessage; + if (m_enabledSolvers.z3 and boost::starts_with(result.responseOrErrorMessage, "unsat")) + { + solverBinary += " fp.xform.slice=false fp.xform.inline_linear=false fp.xform.inline_eager=false"; + std::string extendedQuery = "(set-option :produce-proofs true)" + _input + "\n(get-proof)"; + auto secondResult = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery) + ":" + solverBinary, extendedQuery); + if (secondResult.success and boost::starts_with(secondResult.responseOrErrorMessage, "unsat")) + return secondResult.responseOrErrorMessage; + } + else if (m_enabledSolvers.eld and boost::starts_with(result.responseOrErrorMessage, "sat")) + { + // Wrap Eldarica model in a pair of parentheses to treat is a single (list) s-expression + // That's the SMTLIB way to print a model (i.e., respond to a get-model command). + auto afterSat = result.responseOrErrorMessage.find('\n'); + if (afterSat != std::string::npos) // if there is more than just "sat" + { + result.responseOrErrorMessage.insert(afterSat + 1, "("); + result.responseOrErrorMessage.push_back(')'); + return result.responseOrErrorMessage; + } + } + return result.responseOrErrorMessage; } m_unhandledQueries.push_back(_input); @@ -223,3 +264,530 @@ std::string CHCSmtLib2Interface::createHeaderAndDeclarations() { std::string CHCSmtLib2Interface::createQueryAssertion(std::string name) { return "(assert\n(forall " + forall() + "\n" + "(=> " + name + " false)))"; } + +namespace +{ + bool isNumber(std::string const& _expr) + { + for (char c: _expr) + if (!isDigit(c) && c != '.') + return false; + return true; + } + + class SMTLibTranslationContext + { + SMTLib2Interface const& m_smtlib2Interface; + std::map knownVariables; + + public: + SMTLibTranslationContext(SMTLib2Interface const& _smtlib2Interface) : m_smtlib2Interface(_smtlib2Interface) + { + // fill user defined sorts and constructors + auto const& userSorts = _smtlib2Interface.userSorts(); // TODO: It would be better to remember userSorts as SortPointers + for (auto const& [_, definition] : userSorts) + { + std::stringstream ss(definition); + SMTLib2Parser parser(ss); + auto expr = parser.parseExpression(); + solAssert(parser.isEOF()); + solAssert(!isAtom(expr)); + auto const& args = asSubExpressions(expr); + solAssert(args.size() == 3); + solAssert(isAtom(args[0]) && asAtom(args[0]) == "declare-datatypes"); + // args[1] is the name of the type + // args[2] is the constructor with the members + solAssert(!isAtom(args[2]) && asSubExpressions(args[2]).size() == 1 && !isAtom(asSubExpressions(args[2])[0])); + auto const& constructors = asSubExpressions(asSubExpressions(args[2])[0]); + solAssert(constructors.size() == 1); + auto const& constructor = constructors[0]; + // constructor is a list: name + members + solAssert(!isAtom(constructor)); + auto const& constructorArgs = asSubExpressions(constructor); + for (unsigned i = 1u; i < constructorArgs.size(); ++i) + { + auto const& carg = constructorArgs[i]; + solAssert(!isAtom(carg) && asSubExpressions(carg).size() == 2); + auto const& nameSortPair = asSubExpressions(carg); + solAssert(isAtom(nameSortPair[0])); + knownVariables.insert({asAtom(nameSortPair[0]), toSort(nameSortPair[1])}); + } + } + } + + void addVariableDeclaration(std::string name, SortPointer sort) + { + solAssert(knownVariables.find(name) == knownVariables.end()); + knownVariables.insert({std::move(name), std::move(sort)}); + } + + std::optional lookupKnownTupleSort(std::string const& name) { + std::string quotedName = "|" + name + "|"; + auto it = ranges::find_if(m_smtlib2Interface.sortNames(), [&](auto const& entry) { + return entry.second == name || entry.second == quotedName; + }); + if (it != m_smtlib2Interface.sortNames().end() && it->first->kind == Kind::Tuple) + { + auto tupleSort = std::dynamic_pointer_cast(it->first); + smtAssert(tupleSort); + return tupleSort; + } + return {}; + } + + SortPointer toSort(SMTLib2Expression const& expr) + { + if (isAtom(expr)) + { + auto const& name = asAtom(expr); + if (name == "Int") + return SortProvider::sintSort; + if (name == "Bool") + return SortProvider::boolSort; + auto tupleSort = lookupKnownTupleSort(name); + if (tupleSort) + return tupleSort.value(); + } else { + auto const& args = asSubExpressions(expr); + if (asAtom(args[0]) == "Array") + { + assert(args.size() == 3); + auto domainSort = toSort(args[1]); + auto codomainSort = toSort(args[2]); + return std::make_shared(std::move(domainSort), std::move(codomainSort)); + } + if (args.size() == 3 && isAtom(args[0]) && asAtom(args[0]) == "_" && isAtom(args[1]) && asAtom(args[1]) == "int2bv") + { + solAssert(isAtom(args[2])); + return std::make_shared(std::stoul(asAtom(args[2]))); + } + } + smtAssert(false, "Unknown sort encountered"); + } + + smtutil::Expression parseQuantifier( + std::string const& quantifierName, + std::vector const& varList, + SMTLib2Expression const& coreExpression + ) + { + std::vector> boundVariables; + for (auto const& sortedVar: varList) + { + solAssert(!isAtom(sortedVar)); + auto varSortPair = asSubExpressions(sortedVar); + solAssert(varSortPair.size() == 2); + solAssert(isAtom(varSortPair[0])); + boundVariables.emplace_back(asAtom(varSortPair[0]), toSort(varSortPair[1])); + } + for (auto const& [var, sort] : boundVariables) + { + solAssert(knownVariables.find(var) == knownVariables.end()); // TODO: deal with shadowing? + knownVariables.insert({var, sort}); + } + auto core = toSMTUtilExpression(coreExpression); + for (auto const& [var, sort] : boundVariables) + { + solAssert(knownVariables.find(var) != knownVariables.end()); + knownVariables.erase(var); + } + return Expression(quantifierName, {core}, SortProvider::boolSort); // TODO: what about the bound variables? + + } + + smtutil::Expression toSMTUtilExpression(SMTLib2Expression const& _expr) + { + return std::visit(GenericVisitor{ + [&](std::string const& _atom) { + if (_atom == "true" || _atom == "false") + return smtutil::Expression(_atom == "true"); + else if (isNumber(_atom)) + return smtutil::Expression(_atom, {}, SortProvider::sintSort); + else if (knownVariables.find(_atom) != knownVariables.end()) + return smtutil::Expression(_atom, {}, knownVariables.at(_atom)); + else // assume this is a predicate, so has sort bool; TODO: Context should be aware of the predicates! + return smtutil::Expression(_atom, {}, SortProvider::boolSort); + }, + [&](std::vector const& _subExpr) { + SortPointer sort; + std::vector arguments; + if (isAtom(_subExpr.front())) + { + std::string const& op = asAtom(_subExpr.front()); + if (op == "!") + { + // named term, we ignore the name + solAssert(_subExpr.size() > 2); + return toSMTUtilExpression(_subExpr[1]); + } + if (op == "exists" || op == "forall") + { + solAssert(_subExpr.size() == 3); + solAssert(!isAtom(_subExpr[1])); + return parseQuantifier(op, asSubExpressions(_subExpr[1]), _subExpr[2]); + } + for (size_t i = 1; i < _subExpr.size(); i++) + arguments.emplace_back(toSMTUtilExpression(_subExpr[i])); + if (auto tupleSort = lookupKnownTupleSort(op); tupleSort) + { + auto sortSort = std::make_shared(tupleSort.value()); + return Expression::tuple_constructor(Expression(sortSort), arguments); + } + if (knownVariables.find(op) != knownVariables.end()) + { + return smtutil::Expression(op, std::move(arguments), knownVariables.at(op)); + } + else { + std::set boolOperators{"and", "or", "not", "=", "<", ">", "<=", ">=", + "=>"}; + sort = contains(boolOperators, op) ? SortProvider::boolSort : arguments.back().sort; + return smtutil::Expression(op, std::move(arguments), std::move(sort)); + } + smtAssert(false, "Unhandled case in expression conversion"); + } else { + // check for const array + if (_subExpr.size() == 2 and !isAtom(_subExpr[0])) + { + auto const& typeArgs = asSubExpressions(_subExpr.front()); + if (typeArgs.size() == 3 && typeArgs[0].toString() == "as" && typeArgs[1].toString() == "const") + { + auto arraySort = toSort(typeArgs[2]); + auto sortSort = std::make_shared(arraySort); + return smtutil::Expression::const_array(Expression(sortSort), toSMTUtilExpression(_subExpr[1])); + } + if (typeArgs.size() == 3 && typeArgs[0].toString() == "_" && typeArgs[1].toString() == "int2bv") + { + auto bvSort = std::dynamic_pointer_cast(toSort(_subExpr[0])); + solAssert(bvSort); + return smtutil::Expression::int2bv(toSMTUtilExpression(_subExpr[1]), bvSort->size); + } + if (typeArgs.size() == 4 && typeArgs[0].toString() == "_") + { + if (typeArgs[1].toString() == "extract") + { + return smtutil::Expression( + "extract", + {toSMTUtilExpression(typeArgs[2]), toSMTUtilExpression(typeArgs[3])}, + SortProvider::bitVectorSort // TODO: Compute bit size properly? + ); + } + } + } + + smtAssert(false, "Unhandled case in expression conversion"); + } + } + }, _expr.data); + } + }; + + + struct LetBindings { + using BindingRecord = std::vector; + std::unordered_map bindings; + std::vector varNames; + std::vector scopeBounds; + + bool has(std::string const& varName) + { + return bindings.find(varName) != bindings.end(); + } + + SMTLib2Expression & operator[](std::string const& varName) + { + auto it = bindings.find(varName); + solAssert(it != bindings.end()); + solAssert(!it->second.empty()); + return it->second.back(); + } + + void pushScope() + { + scopeBounds.push_back(varNames.size()); + } + + void popScope() + { + smtAssert(scopeBounds.size() > 0); + auto bound = scopeBounds.back(); + while (varNames.size() > bound) { + auto const& varName = varNames.back(); + auto it = bindings.find(varName); + smtAssert(it != bindings.end()); + auto & record = it->second; + record.pop_back(); + if (record.empty()) + bindings.erase(it); + varNames.pop_back(); + } + scopeBounds.pop_back(); + } + + void addBinding(std::string name, SMTLib2Expression expression) + { + auto it = bindings.find(name); + if (it == bindings.end()) + bindings.insert({name, {std::move(expression)}}); + else + it->second.push_back(std::move(expression)); + varNames.push_back(std::move(name)); + } + }; + + void inlineLetExpressions(SMTLib2Expression& expr, LetBindings & bindings) + { + if (isAtom(expr)) + { + auto const& atom = asAtom(expr); + if (bindings.has(atom)) + expr = bindings[atom]; + return; + } + auto& subexprs = asSubExpressions(expr); + solAssert(!subexprs.empty()); + auto const& first = subexprs.at(0); + if (isAtom(first) && asAtom(first) == "let") + { + solAssert(subexprs.size() >= 3); + solAssert(!isAtom(subexprs[1])); + auto& bindingExpressions = asSubExpressions(subexprs[1]); + // process new bindings + std::vector> newBindings; + for (auto& binding: bindingExpressions) + { + solAssert(!isAtom(binding)); + auto& bindingPair = asSubExpressions(binding); + solAssert(bindingPair.size() == 2); + solAssert(isAtom(bindingPair.at(0))); + inlineLetExpressions(bindingPair.at(1), bindings); + newBindings.emplace_back(asAtom(bindingPair.at(0)), bindingPair.at(1)); + } + bindings.pushScope(); + for (auto&& [name, expr]: newBindings) + bindings.addBinding(std::move(name), std::move(expr)); + newBindings.clear(); + + // get new subexpression + inlineLetExpressions(subexprs.at(2), bindings); + // remove the new bindings + bindings.popScope(); + + // update the expression + auto tmp = std::move(subexprs.at(2)); + expr = std::move(tmp); + return; + } + // not a let expression, just process all arguments + for (auto& subexpr: subexprs) + { + inlineLetExpressions(subexpr, bindings); + } + } + + void inlineLetExpressions(SMTLib2Expression& expr) + { + LetBindings bindings; + inlineLetExpressions(expr, bindings); + } + + SMTLib2Expression const& fact(SMTLib2Expression const& _node) + { + if (isAtom(_node)) + return _node; + solAssert(!asSubExpressions(_node).empty()); + return asSubExpressions(_node).back(); + } + + CHCSolverInterface::CexGraph graphFromSMTLib2Expression(SMTLib2Expression const& _proof, SMTLibTranslationContext & context) + { + assert(!isAtom(_proof)); + auto const& args = asSubExpressions(_proof); + smtAssert(args.size() == 2); + smtAssert(isAtom(args.at(0)) && asAtom(args.at(0)) == "proof"); + auto const& proofNode = args.at(1); + auto derivedFact = fact(proofNode); + if (isAtom(proofNode) || !isAtom(derivedFact) || asAtom(derivedFact) != "false") + return {}; + + CHCSolverInterface::CexGraph graph; + + std::stack proofStack; + proofStack.push(&asSubExpressions(proofNode).at(1)); + + std::map visitedIds; + unsigned nextId = 0; + + + auto const* root = proofStack.top(); + auto const& derivedRootFact = fact(*root); + visitedIds.insert({root, nextId++}); + graph.nodes.emplace(visitedIds.at(root), context.toSMTUtilExpression(derivedRootFact)); + + auto isHyperRes = [](SMTLib2Expression const& expr) { + if (isAtom(expr)) return false; + auto const& subExprs = asSubExpressions(expr); + solAssert(!subExprs.empty()); + auto const& op = subExprs.at(0); + if (isAtom(op)) return false; + auto const& opExprs = asSubExpressions(op); + if (opExprs.size() < 2) return false; + auto const& ruleName = opExprs.at(1); + return isAtom(ruleName) && asAtom(ruleName) == "hyper-res"; + }; + + while (!proofStack.empty()) + { + auto const* proofNode = proofStack.top(); + smtAssert(visitedIds.find(proofNode) != visitedIds.end(), ""); + auto id = visitedIds.at(proofNode); + smtAssert(graph.nodes.count(id), ""); + proofStack.pop(); + + if (isHyperRes(*proofNode)) + { + auto const& args = asSubExpressions(*proofNode); + smtAssert(args.size() > 1, ""); + // args[0] is the name of the rule + // args[1] is the clause used + // last argument is the derived fact + // the arguments in the middle are the facts where we need to recurse + for (unsigned i = 2; i < args.size() - 1; ++i) + { + auto const* child = &args[i]; + if (!visitedIds.count(child)) + { + visitedIds.insert({child, nextId++}); + proofStack.push(child); + } + + auto childId = visitedIds.at(child); + if (!graph.nodes.count(childId)) + { + graph.nodes.emplace(childId, context.toSMTUtilExpression(fact(*child))); + graph.edges[childId] = {}; + } + + graph.edges[id].push_back(childId); + } + } + } + return graph; + } +} + + +CHCSolverInterface::CexGraph CHCSmtLib2Interface::graphFromZ3Proof(std::string const& _proof) +{ + std::stringstream ss(_proof); + std::string answer; + ss >> answer; + solAssert(answer == "unsat"); + + SMTLib2Parser parser(ss); + if (parser.isEOF()) // No proof from Z3 + return {}; + // For some reason Z3 outputs everything as a single s-expression + SMTLib2Expression parsedOutput; + try + { + parsedOutput = parser.parseExpression(); + } + catch (SMTLib2Parser::ParsingException&) + { + // TODO: What should we do in this case? + smtAssert(false, "SMTLIb2Parser: Error parsing input"); + } + solAssert(parser.isEOF()); + solAssert(!isAtom(parsedOutput)); + auto& commands = asSubExpressions(parsedOutput); + SMTLibTranslationContext context(*m_smtlib2); + for (auto& command: commands) + { + if (isAtom(command)) + continue; + + auto const& args = asSubExpressions(command); + auto const& head = args[0]; + if (!isAtom(head)) + continue; + + if (asAtom(head) == "declare-fun") + { + solAssert(args.size() == 4); + auto const& name = args[1]; + auto const& domainSorts = args[2]; + auto const& codomainSort = args[3]; + solAssert(isAtom(name)); + solAssert(!isAtom(domainSorts)); + context.addVariableDeclaration(asAtom(name), context.toSort(codomainSort)); + } + else if (asAtom(head) == "proof") + { +// std::cout << "Proof expression!\n" << command.toString() << std::endl; + inlineLetExpressions(command); +// std::cout << "Cleaned Proof expression!\n" << command.toString() << std::endl; + return graphFromSMTLib2Expression(command, context); + } + } + return {}; +} + +smtutil::Expression CHCSmtLib2Interface::invariantsFromSMTLib(std::string const& _invariants) { + std::stringstream ss(_invariants); + std::string answer; + ss >> answer; + solAssert(answer == "sat"); + SMTLib2Parser parser(ss); + if (parser.isEOF()) // No model + return Expression(true); + // For some reason Z3 outputs everything as a single s-expression + SMTLib2Expression parsedOutput; + try { + parsedOutput = parser.parseExpression(); + } catch(SMTLib2Parser::ParsingException&) + { + // TODO: What should we do in this case? + smtAssert(false, "SMTLIb2Parser: Error parsing input"); + } + solAssert(parser.isEOF()); + solAssert(!isAtom(parsedOutput)); + auto& commands = asSubExpressions(parsedOutput); + std::vector definitions; + for (auto& command: commands) + { + solAssert(!isAtom(command)); + auto& args = asSubExpressions(command); + solAssert(args.size() == 5); + // args[0] = "define-fun" + // args[1] = predicate name + // args[2] = formal arguments of the predicate + // args[3] = return sort + // args[4] = body of the predicate's interpretation + solAssert(isAtom(args[0]) && asAtom(args[0]) == "define-fun"); + solAssert(isAtom(args[1])); + solAssert(!isAtom(args[2])); + solAssert(isAtom(args[3]) && asAtom(args[3]) == "Bool"); + auto& interpretation = args[4]; + inlineLetExpressions(interpretation); + SMTLibTranslationContext context(*m_smtlib2); + auto const& formalArguments = asSubExpressions(args[2]); + std::vector predicateArgs; + for (auto const& formalArgument: formalArguments) + { + solAssert(!isAtom(formalArgument)); + auto const& nameSortPair = asSubExpressions(formalArgument); + solAssert(nameSortPair.size() == 2); + solAssert(isAtom(nameSortPair[0])); + SortPointer varSort = context.toSort(nameSortPair[1]); + context.addVariableDeclaration(asAtom(nameSortPair[0]), varSort); + Expression arg = context.toSMTUtilExpression(nameSortPair[0]); + predicateArgs.push_back(arg); + } + + auto parsedInterpretation = context.toSMTUtilExpression(interpretation); + + Expression predicate(asAtom(args[1]), predicateArgs, SortProvider::boolSort); + definitions.push_back(predicate == parsedInterpretation); + } + return Expression::mkAnd(std::move(definitions)); +} diff --git a/libsmtutil/CHCSmtLib2Interface.h b/libsmtutil/CHCSmtLib2Interface.h index 0f3a68ee4..03d10ed28 100644 --- a/libsmtutil/CHCSmtLib2Interface.h +++ b/libsmtutil/CHCSmtLib2Interface.h @@ -32,6 +32,7 @@ namespace solidity::smtutil class CHCSmtLib2Interface: public CHCSolverInterface { public: + explicit CHCSmtLib2Interface( std::map const& _queryResponses = {}, frontend::ReadCallback::Callback _smtCallback = {}, @@ -58,7 +59,7 @@ public: SMTLib2Interface* smtlib2Interface() const { return m_smtlib2.get(); } private: - std::string toSmtLibSort(Sort const& _sort); + std::string toSmtLibSort(SortPointer _sort); std::string toSmtLibSort(std::vector const& _sort); void writeHeader(); @@ -74,6 +75,10 @@ private: /// Communicates with the solver via the callback. Throws SMTSolverError on error. std::string querySolver(std::string const& _input); + CexGraph graphFromZ3Proof(std::string const& _proof); + + smtutil::Expression invariantsFromSMTLib(std::string const& _invariants); + /// Used to access toSmtLibSort, SExpr, and handle variables. std::unique_ptr m_smtlib2; @@ -85,8 +90,6 @@ private: frontend::ReadCallback::Callback m_smtCallback; SMTSolverChoice m_enabledSolvers; - - std::map m_sortNames; }; } diff --git a/libsmtutil/CMakeLists.txt b/libsmtutil/CMakeLists.txt index af7f47b60..a5402d59a 100644 --- a/libsmtutil/CMakeLists.txt +++ b/libsmtutil/CMakeLists.txt @@ -4,48 +4,16 @@ set(sources Exceptions.h SMTLib2Interface.cpp SMTLib2Interface.h - SMTPortfolio.cpp - SMTPortfolio.h + SMTLibParser.cpp + SMTLibParser.h SolverInterface.h Sorts.cpp Sorts.h Helpers.h ) -if (${Z3_FOUND}) - set(z3_SRCS Z3Interface.cpp Z3Interface.h Z3CHCInterface.cpp Z3CHCInterface.h) -else() - set(z3_SRCS) -endif() -if (${CVC4_FOUND}) - set(cvc4_SRCS CVC4Interface.cpp CVC4Interface.h) -else() - set(cvc4_SRCS) -endif() -if (${USE_Z3_DLOPEN}) - file(GLOB Z3_HEADERS ${Z3_HEADER_PATH}/z3*.h) - set(Z3_WRAPPER ${CMAKE_CURRENT_BINARY_DIR}/z3wrapper.cpp) - add_custom_command( - OUTPUT ${Z3_WRAPPER} - COMMAND ${Python3_EXECUTABLE} genz3wrapper.py ${Z3_HEADERS} > ${Z3_WRAPPER} - DEPENDS ${Z3_HEADERS} genz3wrapper.py - WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR} - ) - set(z3_SRCS ${z3_SRCS} ${Z3_WRAPPER} Z3Loader.cpp Z3Loader.h) -endif() -add_library(smtutil ${sources} ${z3_SRCS} ${cvc4_SRCS}) +add_library(smtutil ${sources}) target_link_libraries(smtutil PUBLIC solutil Boost::boost) - -if (${USE_Z3_DLOPEN}) - target_include_directories(smtutil PUBLIC ${Z3_HEADER_PATH}) - target_link_libraries(smtutil PUBLIC ${CMAKE_DL_LIBS}) -elseif (${Z3_FOUND}) - target_link_libraries(smtutil PUBLIC z3::libz3) -endif() - -if (${CVC4_FOUND}) - target_link_libraries(smtutil PUBLIC CVC4::CVC4) -endif() diff --git a/libsmtutil/CVC4Interface.cpp b/libsmtutil/CVC4Interface.cpp deleted file mode 100644 index f53c92ab5..000000000 --- a/libsmtutil/CVC4Interface.cpp +++ /dev/null @@ -1,336 +0,0 @@ -/* - 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 - -using namespace solidity; -using namespace solidity::util; -using namespace solidity::smtutil; - -CVC4Interface::CVC4Interface(std::optional _queryTimeout): - SolverInterface(_queryTimeout), - m_solver(&m_context) -{ - reset(); -} - -void CVC4Interface::reset() -{ - m_variables.clear(); - m_solver.reset(); - m_solver.setOption("produce-models", true); - if (m_queryTimeout) - m_solver.setTimeLimit(*m_queryTimeout); - else - m_solver.setResourceLimit(resourceLimit); -} - -void CVC4Interface::push() -{ - m_solver.push(); -} - -void CVC4Interface::pop() -{ - m_solver.pop(); -} - -void CVC4Interface::declareVariable(std::string const& _name, SortPointer const& _sort) -{ - smtAssert(_sort, ""); - m_variables[_name] = m_context.mkVar(_name.c_str(), cvc4Sort(*_sort)); -} - -void CVC4Interface::addAssertion(Expression const& _expr) -{ - try - { - m_solver.assertFormula(toCVC4Expr(_expr)); - } - catch (CVC4::TypeCheckingException const& _e) - { - smtAssert(false, _e.what()); - } - catch (CVC4::LogicException const& _e) - { - smtAssert(false, _e.what()); - } - catch (CVC4::UnsafeInterruptException const& _e) - { - smtAssert(false, _e.what()); - } - catch (CVC4::Exception const& _e) - { - smtAssert(false, _e.what()); - } -} - -std::pair> CVC4Interface::check(std::vector const& _expressionsToEvaluate) -{ - CheckResult result; - std::vector values; - try - { - switch (m_solver.checkSat().isSat()) - { - case CVC4::Result::SAT: - result = CheckResult::SATISFIABLE; - break; - case CVC4::Result::UNSAT: - result = CheckResult::UNSATISFIABLE; - break; - case CVC4::Result::SAT_UNKNOWN: - result = CheckResult::UNKNOWN; - break; - default: - smtAssert(false, ""); - } - - if (result == CheckResult::SATISFIABLE && !_expressionsToEvaluate.empty()) - { - for (Expression const& e: _expressionsToEvaluate) - values.push_back(toString(m_solver.getValue(toCVC4Expr(e)))); - } - } - catch (CVC4::Exception const&) - { - result = CheckResult::ERROR; - values.clear(); - } - - return std::make_pair(result, values); -} - -CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr) -{ - // Variable - if (_expr.arguments.empty() && m_variables.count(_expr.name)) - return m_variables.at(_expr.name); - - std::vector arguments; - for (auto const& arg: _expr.arguments) - arguments.push_back(toCVC4Expr(arg)); - - try - { - std::string const& n = _expr.name; - // Function application - if (!arguments.empty() && m_variables.count(_expr.name)) - return m_context.mkExpr(CVC4::kind::APPLY_UF, m_variables.at(n), arguments); - // Literal - else if (arguments.empty()) - { - if (n == "true") - return m_context.mkConst(true); - else if (n == "false") - return m_context.mkConst(false); - else if (auto sortSort = std::dynamic_pointer_cast(_expr.sort)) - return m_context.mkVar(n, cvc4Sort(*sortSort->inner)); - else - try - { - return m_context.mkConst(CVC4::Rational(n)); - } - catch (CVC4::TypeCheckingException const& _e) - { - smtAssert(false, _e.what()); - } - catch (CVC4::Exception const& _e) - { - smtAssert(false, _e.what()); - } - } - - smtAssert(_expr.hasCorrectArity(), ""); - if (n == "ite") - return arguments[0].iteExpr(arguments[1], arguments[2]); - else if (n == "not") - return arguments[0].notExpr(); - else if (n == "and") - return arguments[0].andExpr(arguments[1]); - else if (n == "or") - return arguments[0].orExpr(arguments[1]); - else if (n == "=>") - return m_context.mkExpr(CVC4::kind::IMPLIES, arguments[0], arguments[1]); - else if (n == "=") - return m_context.mkExpr(CVC4::kind::EQUAL, arguments[0], arguments[1]); - else if (n == "<") - return m_context.mkExpr(CVC4::kind::LT, arguments[0], arguments[1]); - else if (n == "<=") - return m_context.mkExpr(CVC4::kind::LEQ, arguments[0], arguments[1]); - else if (n == ">") - return m_context.mkExpr(CVC4::kind::GT, arguments[0], arguments[1]); - else if (n == ">=") - return m_context.mkExpr(CVC4::kind::GEQ, arguments[0], arguments[1]); - else if (n == "+") - return m_context.mkExpr(CVC4::kind::PLUS, arguments[0], arguments[1]); - else if (n == "-") - return m_context.mkExpr(CVC4::kind::MINUS, arguments[0], arguments[1]); - else if (n == "*") - return m_context.mkExpr(CVC4::kind::MULT, arguments[0], arguments[1]); - else if (n == "div") - return m_context.mkExpr(CVC4::kind::INTS_DIVISION_TOTAL, arguments[0], arguments[1]); - else if (n == "mod") - return m_context.mkExpr(CVC4::kind::INTS_MODULUS, arguments[0], arguments[1]); - else if (n == "bvnot") - return m_context.mkExpr(CVC4::kind::BITVECTOR_NOT, arguments[0]); - else if (n == "bvand") - return m_context.mkExpr(CVC4::kind::BITVECTOR_AND, arguments[0], arguments[1]); - else if (n == "bvor") - return m_context.mkExpr(CVC4::kind::BITVECTOR_OR, arguments[0], arguments[1]); - else if (n == "bvxor") - return m_context.mkExpr(CVC4::kind::BITVECTOR_XOR, arguments[0], arguments[1]); - else if (n == "bvshl") - return m_context.mkExpr(CVC4::kind::BITVECTOR_SHL, arguments[0], arguments[1]); - else if (n == "bvlshr") - return m_context.mkExpr(CVC4::kind::BITVECTOR_LSHR, arguments[0], arguments[1]); - else if (n == "bvashr") - return m_context.mkExpr(CVC4::kind::BITVECTOR_ASHR, arguments[0], arguments[1]); - else if (n == "int2bv") - { - size_t size = std::stoul(_expr.arguments[1].name); - auto i2bvOp = m_context.mkConst(CVC4::IntToBitVector(static_cast(size))); - // CVC4 treats all BVs as unsigned, so we need to manually apply 2's complement if needed. - return m_context.mkExpr( - CVC4::kind::ITE, - m_context.mkExpr(CVC4::kind::GEQ, arguments[0], m_context.mkConst(CVC4::Rational(0))), - m_context.mkExpr(CVC4::kind::INT_TO_BITVECTOR, i2bvOp, arguments[0]), - m_context.mkExpr( - CVC4::kind::BITVECTOR_NEG, - m_context.mkExpr(CVC4::kind::INT_TO_BITVECTOR, i2bvOp, m_context.mkExpr(CVC4::kind::UMINUS, arguments[0])) - ) - ); - } - else if (n == "bv2int") - { - auto intSort = std::dynamic_pointer_cast(_expr.sort); - smtAssert(intSort, ""); - auto nat = m_context.mkExpr(CVC4::kind::BITVECTOR_TO_NAT, arguments[0]); - if (!intSort->isSigned) - return nat; - - auto type = arguments[0].getType(); - smtAssert(type.isBitVector(), ""); - auto size = CVC4::BitVectorType(type).getSize(); - // CVC4 treats all BVs as unsigned, so we need to manually apply 2's complement if needed. - auto extractOp = m_context.mkConst(CVC4::BitVectorExtract(size - 1, size - 1)); - return m_context.mkExpr(CVC4::kind::ITE, - m_context.mkExpr( - CVC4::kind::EQUAL, - m_context.mkExpr(CVC4::kind::BITVECTOR_EXTRACT, extractOp, arguments[0]), - m_context.mkConst(CVC4::BitVector(1, uint64_t{0})) - ), - nat, - m_context.mkExpr( - CVC4::kind::UMINUS, - m_context.mkExpr(CVC4::kind::BITVECTOR_TO_NAT, m_context.mkExpr(CVC4::kind::BITVECTOR_NEG, arguments[0])) - ) - ); - } - else if (n == "select") - return m_context.mkExpr(CVC4::kind::SELECT, arguments[0], arguments[1]); - else if (n == "store") - return m_context.mkExpr(CVC4::kind::STORE, arguments[0], arguments[1], arguments[2]); - else if (n == "const_array") - { - std::shared_ptr sortSort = std::dynamic_pointer_cast(_expr.arguments[0].sort); - smtAssert(sortSort, ""); - return m_context.mkConst(CVC4::ArrayStoreAll(cvc4Sort(*sortSort->inner), arguments[1])); - } - else if (n == "tuple_get") - { - std::shared_ptr tupleSort = std::dynamic_pointer_cast(_expr.arguments[0].sort); - smtAssert(tupleSort, ""); - CVC4::DatatypeType tt = m_context.mkTupleType(cvc4Sort(tupleSort->components)); - CVC4::Datatype const& dt = tt.getDatatype(); - size_t index = std::stoul(_expr.arguments[1].name); - CVC4::Expr s = dt[0][index].getSelector(); - return m_context.mkExpr(CVC4::kind::APPLY_SELECTOR, s, arguments[0]); - } - else if (n == "tuple_constructor") - { - std::shared_ptr tupleSort = std::dynamic_pointer_cast(_expr.sort); - smtAssert(tupleSort, ""); - CVC4::DatatypeType tt = m_context.mkTupleType(cvc4Sort(tupleSort->components)); - CVC4::Datatype const& dt = tt.getDatatype(); - CVC4::Expr c = dt[0].getConstructor(); - return m_context.mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, c, arguments); - } - - smtAssert(false); - } - catch (CVC4::TypeCheckingException const& _e) - { - smtAssert(false, _e.what()); - } - catch (CVC4::Exception const& _e) - { - smtAssert(false, _e.what()); - } - - smtAssert(false); - - // FIXME: Workaround for spurious GCC 12.1 warning (https://gcc.gnu.org/bugzilla/show_bug.cgi?id=105794) - util::unreachable(); -} - -CVC4::Type CVC4Interface::cvc4Sort(Sort const& _sort) -{ - switch (_sort.kind) - { - case Kind::Bool: - return m_context.booleanType(); - case Kind::Int: - return m_context.integerType(); - case Kind::BitVector: - return m_context.mkBitVectorType(dynamic_cast(_sort).size); - case Kind::Function: - { - FunctionSort const& fSort = dynamic_cast(_sort); - return m_context.mkFunctionType(cvc4Sort(fSort.domain), cvc4Sort(*fSort.codomain)); - } - case Kind::Array: - { - auto const& arraySort = dynamic_cast(_sort); - return m_context.mkArrayType(cvc4Sort(*arraySort.domain), cvc4Sort(*arraySort.range)); - } - case Kind::Tuple: - { - auto const& tupleSort = dynamic_cast(_sort); - return m_context.mkTupleType(cvc4Sort(tupleSort.components)); - } - default: - break; - } - smtAssert(false, ""); - // Cannot be reached. - return m_context.integerType(); -} - -std::vector CVC4Interface::cvc4Sort(std::vector const& _sorts) -{ - std::vector cvc4Sorts; - for (auto const& _sort: _sorts) - cvc4Sorts.push_back(cvc4Sort(*_sort)); - return cvc4Sorts; -} diff --git a/libsmtutil/CVC4Interface.h b/libsmtutil/CVC4Interface.h deleted file mode 100644 index cc3c0577c..000000000 --- a/libsmtutil/CVC4Interface.h +++ /dev/null @@ -1,74 +0,0 @@ -/* - 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 - -#if defined(__GLIBC__) -// The CVC4 headers includes the deprecated system headers -// and . These headers cause a warning that will break the -// build, unless _GLIBCXX_PERMIT_BACKWARD_HASH is set. -#define _GLIBCXX_PERMIT_BACKWARD_HASH -#endif - -#include - -#if defined(__GLIBC__) -#undef _GLIBCXX_PERMIT_BACKWARD_HASH -#endif - -namespace solidity::smtutil -{ - -class CVC4Interface: public SolverInterface -{ -public: - /// Noncopyable. - CVC4Interface(CVC4Interface const&) = delete; - CVC4Interface& operator=(CVC4Interface const&) = delete; - - CVC4Interface(std::optional _queryTimeout = {}); - - void reset() override; - - void push() override; - void pop() override; - - void declareVariable(std::string const&, SortPointer const&) override; - - void addAssertion(Expression const& _expr) override; - std::pair> check(std::vector const& _expressionsToEvaluate) override; - -private: - CVC4::Expr toCVC4Expr(Expression const& _expr); - CVC4::Type cvc4Sort(Sort const& _sort); - std::vector cvc4Sort(std::vector const& _sorts); - - CVC4::ExprManager m_context; - CVC4::SmtEngine m_solver; - std::map m_variables; - - // CVC4 "basic resources" limit. - // This is used to make the runs more deterministic and platform/machine independent. - // The tests start failing for CVC4 with less than 6000, - // so using double that. - static int const resourceLimit = 12000; -}; - -} diff --git a/libsmtutil/SMTLib2Interface.cpp b/libsmtutil/SMTLib2Interface.cpp index ac5645bf1..6f52589df 100644 --- a/libsmtutil/SMTLib2Interface.cpp +++ b/libsmtutil/SMTLib2Interface.cpp @@ -18,6 +18,8 @@ #include +#include + #include #include @@ -39,13 +41,14 @@ using namespace solidity::frontend; using namespace solidity::smtutil; SMTLib2Interface::SMTLib2Interface( - std::map _queryResponses, + [[maybe_unused]] std::map _queryResponses, ReadCallback::Callback _smtCallback, + SMTSolverChoice _enabledSolvers, std::optional _queryTimeout ): SolverInterface(_queryTimeout), - m_queryResponses(std::move(_queryResponses)), - m_smtCallback(std::move(_smtCallback)) + m_smtCallback(std::move(_smtCallback)), + m_enabledSolvers(_enabledSolvers) { reset(); } @@ -56,6 +59,7 @@ void SMTLib2Interface::reset() m_accumulatedOutput.emplace_back(); m_variables.clear(); m_userSorts.clear(); + m_sortNames.clear(); write("(set-option :produce-models true)"); if (m_queryTimeout) write("(set-option :timeout " + std::to_string(*m_queryTimeout) + ")"); @@ -81,7 +85,7 @@ void SMTLib2Interface::declareVariable(std::string const& _name, SortPointer con else if (!m_variables.count(_name)) { m_variables.emplace(_name, _sort); - write("(declare-fun |" + _name + "| () " + toSmtLibSort(*_sort) + ')'); + write("(declare-fun |" + _name + "| () " + toSmtLibSort(_sort) + ')'); } } @@ -94,7 +98,7 @@ void SMTLib2Interface::declareFunction(std::string const& _name, SortPointer con { auto const& fSort = std::dynamic_pointer_cast(_sort); std::string domain = toSmtLibSort(fSort->domain); - std::string codomain = toSmtLibSort(*fSort->codomain); + std::string codomain = toSmtLibSort(fSort->codomain); m_variables.emplace(_name, _sort); write( "(declare-fun |" + @@ -113,28 +117,91 @@ void SMTLib2Interface::addAssertion(Expression const& _expr) write("(assert " + toSExpr(_expr) + ")"); } +namespace // Helpers for querying solvers using SMT callback +{ + auto resultFromSolverResponse (std::string const& response) { + CheckResult result; + // TODO proper parsing + if (boost::starts_with(response, "sat")) + result = CheckResult::SATISFIABLE; + else if (boost::starts_with(response, "unsat")) + result = CheckResult::UNSATISFIABLE; + else if (boost::starts_with(response, "unknown")) + result = CheckResult::UNKNOWN; + else + result = CheckResult::ERROR; + return result; + } + + bool solverAnswered(CheckResult result) + { + return result == CheckResult::SATISFIABLE || result == CheckResult::UNSATISFIABLE; + } + + std::vector parseValues(std::string const& solverAnswer) + { + std::vector parsedValues; + std::stringstream ss(solverAnswer); + std::string answer; + ss >> answer; + solAssert(answer == "sat"); + SMTLib2Parser parser(ss); + if (parser.isEOF()) + return parsedValues; + auto values = parser.parseExpression(); + solAssert(!isAtom(values)); + auto const& valuesExpr = asSubExpressions(values); + for (auto const& valueExpr: valuesExpr) + { + solAssert(!isAtom(valueExpr)); + auto const& nameValuePair = asSubExpressions(valueExpr); + solAssert(nameValuePair.size() == 2); + parsedValues.push_back(nameValuePair[1].toString()); + } + return parsedValues; + } +} + std::pair> SMTLib2Interface::check(std::vector const& _expressionsToEvaluate) { - std::string response = querySolver( - boost::algorithm::join(m_accumulatedOutput, "\n") + - checkSatAndGetValuesCommand(_expressionsToEvaluate) - ); + auto query = boost::algorithm::join(m_accumulatedOutput, "\n") + checkSatAndGetValuesCommand(_expressionsToEvaluate); - CheckResult result; - // TODO proper parsing - if (boost::starts_with(response, "sat\n")) - result = CheckResult::SATISFIABLE; - else if (boost::starts_with(response, "unsat\n")) - result = CheckResult::UNSATISFIABLE; - else if (boost::starts_with(response, "unknown\n")) - result = CheckResult::UNKNOWN; - else - result = CheckResult::ERROR; + std::vector solverCommands; + if (m_enabledSolvers.z3) + solverCommands.emplace_back("z3 -in rlimit=1000000"); + if (m_enabledSolvers.cvc4) + solverCommands.emplace_back("cvc4 --lang smtlib2.6 --output-lang smtlib2.6"); - std::vector values; - if (result == CheckResult::SATISFIABLE && !_expressionsToEvaluate.empty()) - values = parseValues(find(response.cbegin(), response.cend(), '\n'), response.cend()); - return std::make_pair(result, values); + CheckResult lastResult = CheckResult::ERROR; + std::vector finalValues; + smtAssert(m_smtCallback); + for (auto const& s: solverCommands) + { + auto callBackResult = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery) + ":" + s, query); + if (not callBackResult.success) + continue; + auto const& response = callBackResult.responseOrErrorMessage; + CheckResult result = resultFromSolverResponse(response); + if (solverAnswered(result)) + { + if (!solverAnswered(lastResult)) + { + lastResult = result; + if (result == CheckResult::SATISFIABLE) + finalValues = parseValues(response); + } + else if (lastResult != result) + { + lastResult = CheckResult::CONFLICTING; + break; + } + } + else if (result == CheckResult::UNKNOWN && lastResult == CheckResult::ERROR) + lastResult = result; + } + if (lastResult == CheckResult::ERROR) + m_unhandledQueries.push_back(query); + return std::make_pair(lastResult, finalValues); } std::string SMTLib2Interface::toSExpr(Expression const& _expr) @@ -183,7 +250,7 @@ std::string SMTLib2Interface::toSExpr(Expression const& _expr) smtAssert(sortSort, ""); auto arraySort = std::dynamic_pointer_cast(sortSort->inner); smtAssert(arraySort, ""); - sexpr += "(as const " + toSmtLibSort(*arraySort) + ") "; + sexpr += "(as const " + toSmtLibSort(arraySort) + ") "; sexpr += toSExpr(_expr.arguments.at(1)); } else if (_expr.name == "tuple_get") @@ -212,7 +279,17 @@ std::string SMTLib2Interface::toSExpr(Expression const& _expr) return sexpr; } -std::string SMTLib2Interface::toSmtLibSort(Sort const& _sort) +std::string SMTLib2Interface::toSmtLibSort(SortPointer _sort) +{ + if (!m_sortNames.count(_sort)) + { + auto smtLibName = sortToString(*_sort); + m_sortNames[_sort] = smtLibName; + } + return m_sortNames.at(_sort); +} + +std::string SMTLib2Interface::sortToString(Sort const& _sort) { switch (_sort.kind) { @@ -226,7 +303,7 @@ std::string SMTLib2Interface::toSmtLibSort(Sort const& _sort) { auto const& arraySort = dynamic_cast(_sort); smtAssert(arraySort.domain && arraySort.range, ""); - return "(Array " + toSmtLibSort(*arraySort.domain) + ' ' + toSmtLibSort(*arraySort.range) + ')'; + return "(Array " + toSmtLibSort(arraySort.domain) + ' ' + toSmtLibSort(arraySort.range) + ')'; } case Kind::Tuple: { @@ -238,7 +315,7 @@ std::string SMTLib2Interface::toSmtLibSort(Sort const& _sort) std::string decl("(declare-datatypes ((" + tupleName + " 0)) (((" + tupleName); smtAssert(tupleSort.members.size() == tupleSort.components.size(), ""); for (unsigned i = 0; i < tupleSort.members.size(); ++i) - decl += " (|" + tupleSort.members.at(i) + "| " + toSmtLibSort(*tupleSort.components.at(i)) + ")"; + decl += " (|" + tupleSort.members.at(i) + "| " + toSmtLibSort(tupleSort.components.at(i)) + ")"; decl += "))))"; m_userSorts.emplace_back(tupleName, decl); write(decl); @@ -255,7 +332,7 @@ std::string SMTLib2Interface::toSmtLibSort(std::vector const& _sort { std::string ssort("("); for (auto const& sort: _sorts) - ssort += toSmtLibSort(*sort) + " "; + ssort += toSmtLibSort(sort) + " "; ssort += ")"; return ssort; } @@ -291,37 +368,6 @@ std::string SMTLib2Interface::checkSatAndGetValuesCommand(std::vector SMTLib2Interface::parseValues(std::string::const_iterator _start, std::string::const_iterator _end) -{ - std::vector values; - while (_start < _end) - { - auto valStart = find(_start, _end, ' '); - if (valStart < _end) - ++valStart; - auto valEnd = find(valStart, _end, ')'); - values.emplace_back(valStart, valEnd); - _start = find(valEnd, _end, '('); - } - - return values; -} - -std::string SMTLib2Interface::querySolver(std::string const& _input) -{ - h256 inputHash = keccak256(_input); - if (m_queryResponses.count(inputHash)) - return m_queryResponses.at(inputHash); - if (m_smtCallback) - { - auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery), _input); - if (result.success) - return result.responseOrErrorMessage; - } - m_unhandledQueries.push_back(_input); - return "unknown\n"; -} - std::string SMTLib2Interface::dumpQuery(std::vector const& _expressionsToEvaluate) { return boost::algorithm::join(m_accumulatedOutput, "\n") + diff --git a/libsmtutil/SMTLib2Interface.h b/libsmtutil/SMTLib2Interface.h index 9ef8e94a8..39d73e0d1 100644 --- a/libsmtutil/SMTLib2Interface.h +++ b/libsmtutil/SMTLib2Interface.h @@ -44,6 +44,7 @@ public: explicit SMTLib2Interface( std::map _queryResponses = {}, frontend::ReadCallback::Callback _smtCallback = {}, + SMTSolverChoice _enabledSolvers = SMTSolverChoice::None(), std::optional _queryTimeout = {} ); @@ -61,25 +62,25 @@ public: // Used by CHCSmtLib2Interface std::string toSExpr(Expression const& _expr); - std::string toSmtLibSort(Sort const& _sort); + std::string toSmtLibSort(SortPointer _sort); std::string toSmtLibSort(std::vector const& _sort); std::map variables() { return m_variables; } std::vector> const& userSorts() const { return m_userSorts; } + auto const& sortNames() const { return m_sortNames; } + std::string dumpQuery(std::vector const& _expressionsToEvaluate); private: + std::string sortToString(Sort const& _sort); + void declareFunction(std::string const& _name, SortPointer const& _sort); void write(std::string _data); std::string checkSatAndGetValuesCommand(std::vector const& _expressionsToEvaluate); - std::vector parseValues(std::string::const_iterator _start, std::string::const_iterator _end); - - /// Communicates with the solver via the callback. Throws SMTSolverError on error. - std::string querySolver(std::string const& _input); std::vector m_accumulatedOutput; std::map m_variables; @@ -89,11 +90,14 @@ private: /// It needs to be a vector so that the declaration order is kept, /// otherwise solvers cannot parse the queries. std::vector> m_userSorts; + // TODO: Shouldn't sorts be unique objects? + std::map m_sortNames; + - std::map m_queryResponses; std::vector m_unhandledQueries; frontend::ReadCallback::Callback m_smtCallback; + SMTSolverChoice m_enabledSolvers; }; } diff --git a/libsmtutil/SMTLibParser.cpp b/libsmtutil/SMTLibParser.cpp new file mode 100644 index 000000000..3812f2f6a --- /dev/null +++ b/libsmtutil/SMTLibParser.cpp @@ -0,0 +1,79 @@ +#include + +#include + +#include +#include + + +using namespace solidity::langutil; +using namespace solidity::smtutil; + +std::string SMTLib2Expression::toString() const { + return std::visit(solidity::util::GenericVisitor{ + [](std::string const& _sv) { return _sv; }, + [](std::vector const& _subExpr) { + std::vector formatted; + for (auto const& item: _subExpr) + formatted.emplace_back(item.toString()); + return "(" + solidity::util::joinHumanReadable(formatted, " ") + ")"; + } + }, data); +} + +SMTLib2Expression SMTLib2Parser::parseExpression() { + skipWhitespace(); + if (token() == '(') + { + advance(); + skipWhitespace(); + std::vector subExpressions; + while (token() != 0 && token() != ')') + { + subExpressions.emplace_back(parseExpression()); + skipWhitespace(); + } + solAssert(token() == ')'); + // simulate whitespace because we do not want to read the next token + // since it might block. + m_token = ' '; + return {std::move(subExpressions)}; + } else + return {parseToken()}; +} + +std::string SMTLib2Parser::parseToken() { + std::string result; + + skipWhitespace(); + bool isPipe = token() == '|'; + if (isPipe) + advance(); + while (token() != 0) + { + char c = token(); + if (isPipe && c == '|') + { + advance(); + break; + } else if (!isPipe && (isWhiteSpace(c) || c == '(' || c == ')')) + break; + result.push_back(c); + advance(); + } + return result; +} + +void SMTLib2Parser::advance() { + if (!m_input.good()) + throw ParsingException{}; + m_token = static_cast(m_input.get()); + if (token() == ';') + while (token() != '\n' && token() != 0) + m_token = static_cast(m_input.get()); +} + +void SMTLib2Parser::skipWhitespace() { + while (isWhiteSpace(token())) + advance(); +} diff --git a/libsmtutil/SMTLibParser.h b/libsmtutil/SMTLibParser.h new file mode 100644 index 000000000..fed05d0e8 --- /dev/null +++ b/libsmtutil/SMTLibParser.h @@ -0,0 +1,90 @@ +/* + 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::smtutil +{ + +struct SMTLib2Expression { + using args_t = std::vector; + std::variant data; + + std::string toString() const; +}; + +inline bool isAtom(SMTLib2Expression const & expr) +{ + return std::holds_alternative(expr.data); +} + +inline std::string const& asAtom(SMTLib2Expression const& expr) +{ + solAssert(isAtom(expr)); + return std::get(expr.data); +} + +inline auto const& asSubExpressions(SMTLib2Expression const& expr) +{ + solAssert(!isAtom(expr)); + return std::get(expr.data); +} + +inline auto& asSubExpressions(SMTLib2Expression& expr) +{ + solAssert(!isAtom(expr)); + return std::get(expr.data); +} + +class SMTLib2Parser { +public: + class ParsingException {}; + + SMTLib2Parser(std::istream& _input) : + m_input(_input), + m_token(static_cast(m_input.get())) {} + + SMTLib2Expression parseExpression(); + + bool isEOF() { + skipWhitespace(); + return m_input.eof(); + } + +private: + std::string parseToken(); + + void skipWhitespace(); + + char token() const { + return m_token; + } + + void advance(); + + std::istream& m_input; + char m_token = 0; +}; +} diff --git a/libsmtutil/SMTPortfolio.cpp b/libsmtutil/SMTPortfolio.cpp deleted file mode 100644 index 76c69d018..000000000 --- a/libsmtutil/SMTPortfolio.cpp +++ /dev/null @@ -1,167 +0,0 @@ -/* - 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 - -#ifdef HAVE_Z3 -#include -#endif -#ifdef HAVE_CVC4 -#include -#endif -#include - -using namespace solidity; -using namespace solidity::util; -using namespace solidity::frontend; -using namespace solidity::smtutil; - -SMTPortfolio::SMTPortfolio( - std::map _smtlib2Responses, - frontend::ReadCallback::Callback _smtCallback, - [[maybe_unused]] SMTSolverChoice _enabledSolvers, - std::optional _queryTimeout, - bool _printQuery -): - SolverInterface(_queryTimeout) -{ - solAssert(!_printQuery || _enabledSolvers == smtutil::SMTSolverChoice::SMTLIB2(), "Only SMTLib2 solver can be enabled to print queries"); - if (_enabledSolvers.smtlib2) - m_solvers.emplace_back(std::make_unique(std::move(_smtlib2Responses), std::move(_smtCallback), m_queryTimeout)); -#ifdef HAVE_Z3 - if (_enabledSolvers.z3 && Z3Interface::available()) - m_solvers.emplace_back(std::make_unique(m_queryTimeout)); -#endif -#ifdef HAVE_CVC4 - if (_enabledSolvers.cvc4) - m_solvers.emplace_back(std::make_unique(m_queryTimeout)); -#endif -} - -void SMTPortfolio::reset() -{ - for (auto const& s: m_solvers) - s->reset(); -} - -void SMTPortfolio::push() -{ - for (auto const& s: m_solvers) - s->push(); -} - -void SMTPortfolio::pop() -{ - for (auto const& s: m_solvers) - s->pop(); -} - -void SMTPortfolio::declareVariable(std::string const& _name, SortPointer const& _sort) -{ - smtAssert(_sort, ""); - for (auto const& s: m_solvers) - s->declareVariable(_name, _sort); -} - -void SMTPortfolio::addAssertion(Expression const& _expr) -{ - for (auto const& s: m_solvers) - s->addAssertion(_expr); -} - -/* - * Broadcasts the SMT query to all solvers and returns a single result. - * This comment explains how this result is decided. - * - * When a solver is queried, there are four possible answers: - * SATISFIABLE (SAT), UNSATISFIABLE (UNSAT), UNKNOWN, CONFLICTING, ERROR - * We say that a solver _answered_ the query if it returns either: - * SAT or UNSAT - * A solver did not answer the query if it returns either: - * UNKNOWN (it tried but couldn't solve it) or ERROR (crash, internal error, API error, etc). - * - * Ideally all solvers answer the query and agree on what the answer is - * (all say SAT or all say UNSAT). - * - * The actual logic as as follows: - * 1) If at least one solver answers the query, all the non-answer results are ignored. - * Here SAT/UNSAT is preferred over UNKNOWN since it's an actual answer, and over ERROR - * because one buggy solver/integration shouldn't break the portfolio. - * - * 2) If at least one solver answers SAT and at least one answers UNSAT, at least one of them is buggy - * and the result is CONFLICTING. - * In the future if we have more than 2 solvers enabled we could go with the majority. - * - * 3) If NO solver answers the query: - * If at least one solver returned UNKNOWN (where the rest returned ERROR), the result is UNKNOWN. - * This is preferred over ERROR since the SMTChecker might decide to abstract the query - * when it is told that this is a hard query to solve. - * - * If all solvers return ERROR, the result is ERROR. -*/ -std::pair> SMTPortfolio::check(std::vector const& _expressionsToEvaluate) -{ - CheckResult lastResult = CheckResult::ERROR; - std::vector finalValues; - for (auto const& s: m_solvers) - { - CheckResult result; - std::vector values; - tie(result, values) = s->check(_expressionsToEvaluate); - if (solverAnswered(result)) - { - if (!solverAnswered(lastResult)) - { - lastResult = result; - finalValues = std::move(values); - } - else if (lastResult != result) - { - lastResult = CheckResult::CONFLICTING; - break; - } - } - else if (result == CheckResult::UNKNOWN && lastResult == CheckResult::ERROR) - lastResult = result; - } - return std::make_pair(lastResult, finalValues); -} - -std::vector SMTPortfolio::unhandledQueries() -{ - // This code assumes that the constructor guarantees that - // SmtLib2Interface is in position 0, if enabled. - if (!m_solvers.empty()) - if (auto smtlib2 = dynamic_cast(m_solvers.front().get())) - return smtlib2->unhandledQueries(); - return {}; -} - -bool SMTPortfolio::solverAnswered(CheckResult result) -{ - return result == CheckResult::SATISFIABLE || result == CheckResult::UNSATISFIABLE; -} - -std::string SMTPortfolio::dumpQuery(std::vector const& _expressionsToEvaluate) -{ - // This code assumes that the constructor guarantees that - // SmtLib2Interface is in position 0, if enabled. - auto smtlib2 = dynamic_cast(m_solvers.front().get()); - solAssert(smtlib2, "Must use SMTLib2 solver to dump queries"); - return smtlib2->dumpQuery(_expressionsToEvaluate); -} diff --git a/libsmtutil/SMTPortfolio.h b/libsmtutil/SMTPortfolio.h deleted file mode 100644 index cdb33368e..000000000 --- a/libsmtutil/SMTPortfolio.h +++ /dev/null @@ -1,77 +0,0 @@ -/* - 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::smtutil -{ - -/** - * The SMTPortfolio wraps all available solvers within a single interface, - * propagating the functionalities to all solvers. - * It also checks whether different solvers give conflicting answers - * to SMT queries. - */ -class SMTPortfolio: public SolverInterface -{ -public: - /// Noncopyable. - SMTPortfolio(SMTPortfolio const&) = delete; - SMTPortfolio& operator=(SMTPortfolio const&) = delete; - - SMTPortfolio( - std::map _smtlib2Responses = {}, - frontend::ReadCallback::Callback _smtCallback = {}, - SMTSolverChoice _enabledSolvers = SMTSolverChoice::All(), - std::optional _queryTimeout = {}, - bool _printQuery = false - ); - - void reset() override; - - void push() override; - void pop() override; - - void declareVariable(std::string const&, SortPointer const&) override; - - void addAssertion(Expression const& _expr) override; - - std::pair> check(std::vector const& _expressionsToEvaluate) override; - - std::vector unhandledQueries() override; - size_t solvers() override { return m_solvers.size(); } - - std::string dumpQuery(std::vector const& _expressionsToEvaluate); - -private: - static bool solverAnswered(CheckResult result); - - std::vector> m_solvers; - - std::vector m_assertions; -}; - -} diff --git a/libsmtutil/SolverInterface.h b/libsmtutil/SolverInterface.h index 4a21f1841..6778a4371 100644 --- a/libsmtutil/SolverInterface.h +++ b/libsmtutil/SolverInterface.h @@ -43,15 +43,13 @@ struct SMTSolverChoice { bool cvc4 = false; bool eld = false; - bool smtlib2 = false; bool z3 = false; - static constexpr SMTSolverChoice All() noexcept { return {true, true, true, true}; } - static constexpr SMTSolverChoice CVC4() noexcept { return {true, false, false, false}; } - static constexpr SMTSolverChoice ELD() noexcept { return {false, true, false, false}; } - static constexpr SMTSolverChoice SMTLIB2() noexcept { return {false, false, true, false}; } - static constexpr SMTSolverChoice Z3() noexcept { return {false, false, false, true}; } - static constexpr SMTSolverChoice None() noexcept { return {false, false, false, false}; } + static constexpr SMTSolverChoice All() noexcept { return {true, true, true}; } + static constexpr SMTSolverChoice CVC4() noexcept { return {true, false, false}; } + static constexpr SMTSolverChoice ELD() noexcept { return {false, true, false}; } + static constexpr SMTSolverChoice Z3() noexcept { return {false, false, true}; } + static constexpr SMTSolverChoice None() noexcept { return {false, false, false}; } static std::optional fromString(std::string const& _solvers) { @@ -67,7 +65,6 @@ struct SMTSolverChoice { cvc4 &= _other.cvc4; eld &= _other.eld; - smtlib2 &= _other.smtlib2; z3 &= _other.z3; return *this; } @@ -84,29 +81,26 @@ struct SMTSolverChoice { return cvc4 == _other.cvc4 && eld == _other.eld && - smtlib2 == _other.smtlib2 && z3 == _other.z3; } bool setSolver(std::string const& _solver) { - static std::set const solvers{"cvc4", "eld", "smtlib2", "z3"}; + static std::set const solvers{"cvc4", "eld", "z3"}; if (!solvers.count(_solver)) return false; if (_solver == "cvc4") cvc4 = true; if (_solver == "eld") eld = true; - else if (_solver == "smtlib2") - smtlib2 = true; else if (_solver == "z3") z3 = true; return true; } bool none() const noexcept { return !some(); } - bool some() const noexcept { return cvc4 || eld || smtlib2 || z3; } - bool all() const noexcept { return cvc4 && eld && smtlib2 && z3; } + bool some() const noexcept { return cvc4 || eld || z3; } + bool all() const noexcept { return cvc4 && eld && z3; } }; enum class CheckResult diff --git a/libsmtutil/Z3CHCInterface.cpp b/libsmtutil/Z3CHCInterface.cpp deleted file mode 100644 index a25890e8d..000000000 --- a/libsmtutil/Z3CHCInterface.cpp +++ /dev/null @@ -1,242 +0,0 @@ -/* - 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 - -using namespace solidity; -using namespace solidity::smtutil; - -Z3CHCInterface::Z3CHCInterface(std::optional _queryTimeout): - CHCSolverInterface(_queryTimeout), - m_z3Interface(std::make_unique(m_queryTimeout)), - m_context(m_z3Interface->context()), - m_solver(*m_context) -{ - Z3_get_version( - &std::get<0>(m_version), - &std::get<1>(m_version), - &std::get<2>(m_version), - &std::get<3>(m_version) - ); - - // These need to be set globally. - z3::set_param("rewriter.pull_cheap_ite", true); - - if (m_queryTimeout) - m_context->set("timeout", int(*m_queryTimeout)); - else - z3::set_param("rlimit", Z3Interface::resourceLimit); - - setSpacerOptions(); -} - -void Z3CHCInterface::declareVariable(std::string const& _name, SortPointer const& _sort) -{ - smtAssert(_sort, ""); - m_z3Interface->declareVariable(_name, _sort); -} - -void Z3CHCInterface::registerRelation(Expression const& _expr) -{ - m_solver.register_relation(m_z3Interface->functions().at(_expr.name)); -} - -void Z3CHCInterface::addRule(Expression const& _expr, std::string const& _name) -{ - z3::expr rule = m_z3Interface->toZ3Expr(_expr); - if (m_z3Interface->constants().empty()) - m_solver.add_rule(rule, m_context->str_symbol(_name.c_str())); - else - { - z3::expr_vector variables(*m_context); - for (auto const& var: m_z3Interface->constants()) - variables.push_back(var.second); - z3::expr boundRule = z3::forall(variables, rule); - m_solver.add_rule(boundRule, m_context->str_symbol(_name.c_str())); - } -} - -std::tuple Z3CHCInterface::query(Expression const& _expr) -{ - CheckResult result; - try - { - z3::expr z3Expr = m_z3Interface->toZ3Expr(_expr); - switch (m_solver.query(z3Expr)) - { - case z3::check_result::sat: - { - result = CheckResult::SATISFIABLE; - // z3 version 4.8.8 modified Spacer to also return - // proofs containing nonlinear clauses. - if (m_version >= std::tuple(4, 8, 8, 0)) - { - auto proof = m_solver.get_answer(); - return {result, Expression(true), cexGraph(proof)}; - } - break; - } - case z3::check_result::unsat: - { - result = CheckResult::UNSATISFIABLE; - auto invariants = m_z3Interface->fromZ3Expr(m_solver.get_answer()); - return {result, std::move(invariants), {}}; - } - case z3::check_result::unknown: - { - result = CheckResult::UNKNOWN; - break; - } - } - // TODO retrieve model / invariants - } - catch (z3::exception const& _err) - { - std::set msgs{ - /// Resource limit (rlimit) exhausted. - "max. resource limit exceeded", - /// User given timeout exhausted. - "canceled" - }; - if (msgs.count(_err.msg())) - result = CheckResult::UNKNOWN; - else - result = CheckResult::ERROR; - } - - return {result, Expression(true), {}}; -} - -void Z3CHCInterface::setSpacerOptions(bool _preProcessing) -{ - // Spacer options. - // These needs to be set in the solver. - // https://github.com/Z3Prover/z3/blob/master/src/muz/base/fp_params.pyg - z3::params p(*m_context); - // These are useful for solving problems with arrays and loops. - // Use quantified lemma generalizer. - p.set("fp.spacer.q3.use_qgen", true); - p.set("fp.spacer.mbqi", false); - // Ground pobs by using values from a model. - p.set("fp.spacer.ground_pobs", false); - - // Spacer optimization should be - // - enabled for better solving (default) - // - disable for counterexample generation - p.set("fp.xform.slice", _preProcessing); - p.set("fp.xform.inline_linear", _preProcessing); - p.set("fp.xform.inline_eager", _preProcessing); - - m_solver.set(p); -} - -/** -Convert a ground refutation into a linear or nonlinear counterexample. -The counterexample is given as an implication graph of the form -`premises => conclusion` where `premises` are the predicates -from the body of nonlinear clauses, representing the proof graph. - -This function is based on and similar to -https://github.com/Z3Prover/z3/blob/z3-4.8.8/src/muz/spacer/spacer_context.cpp#L2919 -(spacer::context::get_ground_sat_answer) -which generates linear counterexamples. -It is modified here to accept nonlinear CHCs as well, generating a DAG -instead of a path. -*/ -CHCSolverInterface::CexGraph Z3CHCInterface::cexGraph(z3::expr const& _proof) -{ - /// The root fact of the refutation proof is `false`. - /// The node itself is not a hyper resolution, so we need to - /// extract the `query` hyper resolution node from the - /// `false` node (the first child). - /// The proof has the shape above for z3 >=4.8.8. - /// If an older version is used, this check will fail and no - /// counterexample will be generated. - if (!_proof.is_app() || fact(_proof).decl().decl_kind() != Z3_OP_FALSE) - return {}; - - CexGraph graph; - - std::stack proofStack; - proofStack.push(_proof.arg(0)); - - auto const& root = proofStack.top(); - graph.nodes.emplace(root.id(), m_z3Interface->fromZ3Expr(fact(root))); - - std::set visited; - visited.insert(root.id()); - - while (!proofStack.empty()) - { - z3::expr proofNode = proofStack.top(); - smtAssert(graph.nodes.count(proofNode.id()), ""); - proofStack.pop(); - - if (proofNode.is_app() && proofNode.decl().decl_kind() == Z3_OP_PR_HYPER_RESOLVE) - { - smtAssert(proofNode.num_args() > 0, ""); - for (unsigned i = 1; i < proofNode.num_args() - 1; ++i) - { - z3::expr child = proofNode.arg(i); - if (!visited.count(child.id())) - { - visited.insert(child.id()); - proofStack.push(child); - } - - if (!graph.nodes.count(child.id())) - { - graph.nodes.emplace(child.id(), m_z3Interface->fromZ3Expr(fact(child))); - graph.edges[child.id()] = {}; - } - - graph.edges[proofNode.id()].push_back(child.id()); - } - } - } - - return graph; -} - -z3::expr Z3CHCInterface::fact(z3::expr const& _node) -{ - smtAssert(_node.is_app(), ""); - if (_node.num_args() == 0) - return _node; - return _node.arg(_node.num_args() - 1); -} - -std::string Z3CHCInterface::name(z3::expr const& _predicate) -{ - smtAssert(_predicate.is_app(), ""); - return _predicate.decl().name().str(); -} - -std::vector Z3CHCInterface::arguments(z3::expr const& _predicate) -{ - smtAssert(_predicate.is_app(), ""); - std::vector args; - for (unsigned i = 0; i < _predicate.num_args(); ++i) - args.emplace_back(_predicate.arg(i).to_string()); - return args; -} diff --git a/libsmtutil/Z3CHCInterface.h b/libsmtutil/Z3CHCInterface.h deleted file mode 100644 index 5a768f65c..000000000 --- a/libsmtutil/Z3CHCInterface.h +++ /dev/null @@ -1,72 +0,0 @@ -/* - 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 - -/** - * Z3 specific Horn solver interface. - */ - -#pragma once - -#include -#include - -#include -#include - -namespace solidity::smtutil -{ - -class Z3CHCInterface: public CHCSolverInterface -{ -public: - Z3CHCInterface(std::optional _queryTimeout = {}); - - /// Forwards variable declaration to Z3Interface. - void declareVariable(std::string const& _name, SortPointer const& _sort) override; - - void registerRelation(Expression const& _expr) override; - - void addRule(Expression const& _expr, std::string const& _name) override; - - std::tuple query(Expression const& _expr) override; - - Z3Interface* z3Interface() const { return m_z3Interface.get(); } - - void setSpacerOptions(bool _preProcessing = true); - -private: - /// Constructs a nonlinear counterexample graph from the refutation. - CHCSolverInterface::CexGraph cexGraph(z3::expr const& _proof); - /// @returns the fact from a proof node. - z3::expr fact(z3::expr const& _node); - /// @returns @a _predicate's name. - std::string name(z3::expr const& _predicate); - /// @returns the arguments of @a _predicate. - std::vector arguments(z3::expr const& _predicate); - - // Used to handle variables. - std::unique_ptr m_z3Interface; - - z3::context* m_context; - // Horn solver. - z3::fixedpoint m_solver; - - std::tuple m_version = std::tuple(0, 0, 0, 0); -}; - -} diff --git a/libsmtutil/Z3Interface.cpp b/libsmtutil/Z3Interface.cpp deleted file mode 100644 index a16e75668..000000000 --- a/libsmtutil/Z3Interface.cpp +++ /dev/null @@ -1,479 +0,0 @@ -/* - 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 - -#ifdef HAVE_Z3_DLOPEN -#include -#endif - -using namespace solidity::smtutil; -using namespace solidity::util; - -bool Z3Interface::available() -{ -#ifdef HAVE_Z3_DLOPEN - return Z3Loader::get().available(); -#else - return true; -#endif -} - -Z3Interface::Z3Interface(std::optional _queryTimeout): - SolverInterface(_queryTimeout), - m_solver(m_context) -{ - // These need to be set globally. - z3::set_param("rewriter.pull_cheap_ite", true); - - if (m_queryTimeout) - m_context.set("timeout", int(*m_queryTimeout)); - else - z3::set_param("rlimit", resourceLimit); -} - -void Z3Interface::reset() -{ - m_constants.clear(); - m_functions.clear(); - m_solver.reset(); -} - -void Z3Interface::push() -{ - m_solver.push(); -} - -void Z3Interface::pop() -{ - m_solver.pop(); -} - -void Z3Interface::declareVariable(std::string const& _name, SortPointer const& _sort) -{ - smtAssert(_sort, ""); - if (_sort->kind == Kind::Function) - declareFunction(_name, *_sort); - else if (m_constants.count(_name)) - m_constants.at(_name) = m_context.constant(_name.c_str(), z3Sort(*_sort)); - else - m_constants.emplace(_name, m_context.constant(_name.c_str(), z3Sort(*_sort))); -} - -void Z3Interface::declareFunction(std::string const& _name, Sort const& _sort) -{ - smtAssert(_sort.kind == Kind::Function, ""); - FunctionSort fSort = dynamic_cast(_sort); - if (m_functions.count(_name)) - m_functions.at(_name) = m_context.function(_name.c_str(), z3Sort(fSort.domain), z3Sort(*fSort.codomain)); - else - m_functions.emplace(_name, m_context.function(_name.c_str(), z3Sort(fSort.domain), z3Sort(*fSort.codomain))); -} - -void Z3Interface::addAssertion(Expression const& _expr) -{ - m_solver.add(toZ3Expr(_expr)); -} - -std::pair> Z3Interface::check(std::vector const& _expressionsToEvaluate) -{ - CheckResult result; - std::vector values; - try - { - switch (m_solver.check()) - { - case z3::check_result::sat: - result = CheckResult::SATISFIABLE; - break; - case z3::check_result::unsat: - result = CheckResult::UNSATISFIABLE; - break; - case z3::check_result::unknown: - result = CheckResult::UNKNOWN; - break; - } - - if (result == CheckResult::SATISFIABLE && !_expressionsToEvaluate.empty()) - { - z3::model m = m_solver.get_model(); - for (Expression const& e: _expressionsToEvaluate) - values.push_back(util::toString(m.eval(toZ3Expr(e)))); - } - } - catch (z3::exception const& _err) - { - std::set msgs{ - /// Resource limit (rlimit) exhausted. - "max. resource limit exceeded", - /// User given timeout exhausted. - "canceled" - }; - - if (msgs.count(_err.msg())) - result = CheckResult::UNKNOWN; - else - result = CheckResult::ERROR; - values.clear(); - } - - return std::make_pair(result, values); -} - -z3::expr Z3Interface::toZ3Expr(Expression const& _expr) -{ - if (_expr.arguments.empty() && m_constants.count(_expr.name)) - return m_constants.at(_expr.name); - z3::expr_vector arguments(m_context); - for (auto const& arg: _expr.arguments) - arguments.push_back(toZ3Expr(arg)); - - try - { - std::string const& n = _expr.name; - if (m_functions.count(n)) - return m_functions.at(n)(arguments); - else if (m_constants.count(n)) - { - smtAssert(arguments.empty(), ""); - return m_constants.at(n); - } - else if (arguments.empty()) - { - if (n == "true") - return m_context.bool_val(true); - else if (n == "false") - return m_context.bool_val(false); - else if (_expr.sort->kind == Kind::Sort) - { - auto sortSort = std::dynamic_pointer_cast(_expr.sort); - smtAssert(sortSort, ""); - return m_context.constant(n.c_str(), z3Sort(*sortSort->inner)); - } - else - try - { - return m_context.int_val(n.c_str()); - } - catch (z3::exception const& _e) - { - smtAssert(false, _e.msg()); - } - } - - smtAssert(_expr.hasCorrectArity(), ""); - if (n == "ite") - return z3::ite(arguments[0], arguments[1], arguments[2]); - else if (n == "not") - return !arguments[0]; - else if (n == "and") - return arguments[0] && arguments[1]; - else if (n == "or") - return arguments[0] || arguments[1]; - else if (n == "=>") - return z3::implies(arguments[0], arguments[1]); - else if (n == "=") - return arguments[0] == arguments[1]; - else if (n == "<") - return arguments[0] < arguments[1]; - else if (n == "<=") - return arguments[0] <= arguments[1]; - else if (n == ">") - return arguments[0] > arguments[1]; - else if (n == ">=") - return arguments[0] >= arguments[1]; - else if (n == "+") - return arguments[0] + arguments[1]; - else if (n == "-") - return arguments[0] - arguments[1]; - else if (n == "*") - return arguments[0] * arguments[1]; - else if (n == "div") - return arguments[0] / arguments[1]; - else if (n == "mod") - return z3::mod(arguments[0], arguments[1]); - else if (n == "bvnot") - return ~arguments[0]; - else if (n == "bvand") - return arguments[0] & arguments[1]; - else if (n == "bvor") - return arguments[0] | arguments[1]; - else if (n == "bvxor") - return arguments[0] ^ arguments[1]; - else if (n == "bvshl") - return z3::shl(arguments[0], arguments[1]); - else if (n == "bvlshr") - return z3::lshr(arguments[0], arguments[1]); - else if (n == "bvashr") - return z3::ashr(arguments[0], arguments[1]); - else if (n == "int2bv") - { - size_t size = std::stoul(_expr.arguments[1].name); - return z3::int2bv(static_cast(size), arguments[0]); - } - else if (n == "bv2int") - { - auto intSort = std::dynamic_pointer_cast(_expr.sort); - smtAssert(intSort, ""); - return z3::bv2int(arguments[0], intSort->isSigned); - } - else if (n == "select") - return z3::select(arguments[0], arguments[1]); - else if (n == "store") - return z3::store(arguments[0], arguments[1], arguments[2]); - else if (n == "const_array") - { - std::shared_ptr sortSort = std::dynamic_pointer_cast(_expr.arguments[0].sort); - smtAssert(sortSort, ""); - auto arraySort = std::dynamic_pointer_cast(sortSort->inner); - smtAssert(arraySort && arraySort->domain, ""); - return z3::const_array(z3Sort(*arraySort->domain), arguments[1]); - } - else if (n == "tuple_get") - { - size_t index = stoul(_expr.arguments[1].name); - return z3::func_decl(m_context, Z3_get_tuple_sort_field_decl(m_context, z3Sort(*_expr.arguments[0].sort), static_cast(index)))(arguments[0]); - } - else if (n == "tuple_constructor") - { - auto constructor = z3::func_decl(m_context, Z3_get_tuple_sort_mk_decl(m_context, z3Sort(*_expr.sort))); - smtAssert(constructor.arity() == arguments.size(), ""); - z3::expr_vector args(m_context); - for (auto const& arg: arguments) - args.push_back(arg); - return constructor(args); - } - - smtAssert(false); - } - catch (z3::exception const& _e) - { - smtAssert(false, _e.msg()); - } - - smtAssert(false); - - // FIXME: Workaround for spurious GCC 12.1 warning (https://gcc.gnu.org/bugzilla/show_bug.cgi?id=105794) - util::unreachable(); -} - -Expression Z3Interface::fromZ3Expr(z3::expr const& _expr) -{ - auto sort = fromZ3Sort(_expr.get_sort()); - if (_expr.is_const() || _expr.is_var()) - return Expression(_expr.to_string(), {}, sort); - - if (_expr.is_quantifier()) - { - std::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(), ""); - std::vector arguments; - for (unsigned i = 0; i < _expr.num_args(); ++i) - arguments.push_back(fromZ3Expr(_expr.arg(i))); - - auto kind = _expr.decl().decl_kind(); - - if (_expr.is_ite()) - return Expression::ite(arguments[0], arguments[1], arguments[2]); - else if (_expr.is_not()) - return !arguments[0]; - else if (_expr.is_and()) - return Expression::mkAnd(arguments); - else if (_expr.is_or()) - 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_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_GE || kind == Z3_OP_UGEQ || kind == Z3_OP_SGEQ) - return arguments[0] >= arguments[1]; - else if (kind == Z3_OP_ADD) - 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 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_BOR) - return arguments[0] | arguments[1]; - else if (kind == Z3_OP_BAND) - return arguments[0] & arguments[1]; - else if (kind == Z3_OP_BXOR) - 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) - return arguments[0] >> arguments[1]; - else if (kind == Z3_OP_BASHR) - return Expression::ashr(arguments[0], arguments[1]); - else if (kind == Z3_OP_INT2BV) - return Expression::int2bv(arguments[0], _expr.get_sort().bv_size()); - else if (kind == Z3_OP_BV2INT) - 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) - return Expression::store(arguments[0], arguments[1], arguments[2]); - else if (kind == Z3_OP_CONST_ARRAY) - { - auto sortSort = std::make_shared(fromZ3Sort(_expr.get_sort())); - return Expression::const_array(Expression(sortSort), arguments[0]); - } - else if (kind == Z3_OP_DT_CONSTRUCTOR) - { - auto sortSort = std::make_shared(fromZ3Sort(_expr.get_sort())); - return Expression::tuple_constructor(Expression(sortSort), arguments); - } - else if (kind == Z3_OP_DT_ACCESSOR) - 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 || - kind == Z3_OP_RECURSIVE - ) - return Expression(_expr.decl().name().str(), arguments, fromZ3Sort(_expr.get_sort())); - - smtAssert(false); - - // FIXME: Workaround for spurious GCC 12.1 warning (https://gcc.gnu.org/bugzilla/show_bug.cgi?id=105794) - util::unreachable(); -} - -z3::sort Z3Interface::z3Sort(Sort const& _sort) -{ - switch (_sort.kind) - { - case Kind::Bool: - return m_context.bool_sort(); - case Kind::Int: - return m_context.int_sort(); - case Kind::BitVector: - return m_context.bv_sort(dynamic_cast(_sort).size); - case Kind::Array: - { - auto const& arraySort = dynamic_cast(_sort); - return m_context.array_sort(z3Sort(*arraySort.domain), z3Sort(*arraySort.range)); - } - case Kind::Tuple: - { - auto const& tupleSort = dynamic_cast(_sort); - std::vector cMembers; - for (auto const& member: tupleSort.members) - cMembers.emplace_back(member.c_str()); - /// Using this instead of the function below because with that one - /// we can't use `&sorts[0]` here. - std::vector sorts; - for (auto const& sort: tupleSort.components) - sorts.push_back(z3Sort(*sort)); - z3::func_decl_vector projs(m_context); - z3::func_decl tupleConstructor = m_context.tuple_sort( - tupleSort.name.c_str(), - static_cast(tupleSort.members.size()), - cMembers.data(), - sorts.data(), - projs - ); - return tupleConstructor.range(); - } - - default: - break; - } - smtAssert(false, ""); - // Cannot be reached. - return m_context.int_sort(); -} - -z3::sort_vector Z3Interface::z3Sort(std::vector const& _sorts) -{ - z3::sort_vector z3Sorts(m_context); - for (auto const& _sort: _sorts) - z3Sorts.push_back(z3Sort(*_sort)); - return z3Sorts; -} - -SortPointer Z3Interface::fromZ3Sort(z3::sort const& _sort) -{ - if (_sort.is_bool()) - return SortProvider::boolSort; - if (_sort.is_int()) - return SortProvider::sintSort; - if (_sort.is_bv()) - return std::make_shared(_sort.bv_size()); - if (_sort.is_array()) - return std::make_shared(fromZ3Sort(_sort.array_domain()), fromZ3Sort(_sort.array_range())); - if (_sort.is_datatype()) - { - auto name = _sort.name().str(); - auto constructor = z3::func_decl(m_context, Z3_get_tuple_sort_mk_decl(m_context, _sort)); - std::vector memberNames; - std::vector memberSorts; - for (unsigned i = 0; i < constructor.arity(); ++i) - { - auto accessor = z3::func_decl(m_context, Z3_get_tuple_sort_field_decl(m_context, _sort, i)); - memberNames.push_back(accessor.name().str()); - memberSorts.push_back(fromZ3Sort(accessor.range())); - } - return std::make_shared(name, memberNames, memberSorts); - } - smtAssert(false, ""); -} - -std::vector Z3Interface::fromZ3Sort(z3::sort_vector const& _sorts) -{ - return applyMap(_sorts, [this](auto const& sort) { return fromZ3Sort(sort); }); -} diff --git a/libsmtutil/Z3Interface.h b/libsmtutil/Z3Interface.h deleted file mode 100644 index ee268ac41..000000000 --- a/libsmtutil/Z3Interface.h +++ /dev/null @@ -1,75 +0,0 @@ -/* - 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 - -namespace solidity::smtutil -{ - -class Z3Interface: public SolverInterface -{ -public: - /// Noncopyable. - Z3Interface(Z3Interface const&) = delete; - Z3Interface& operator=(Z3Interface const&) = delete; - - Z3Interface(std::optional _queryTimeout = {}); - - static bool available(); - - void reset() override; - - void push() override; - void pop() override; - - void declareVariable(std::string const& _name, SortPointer const& _sort) override; - - void addAssertion(Expression const& _expr) override; - std::pair> check(std::vector const& _expressionsToEvaluate) override; - - z3::expr toZ3Expr(Expression const& _expr); - smtutil::Expression fromZ3Expr(z3::expr const& _expr); - - std::map constants() const { return m_constants; } - std::map functions() const { return m_functions; } - - z3::context* context() { return &m_context; } - - // Z3 "basic resources" limit. - // This is used to make the runs more deterministic and platform/machine independent. - static int const resourceLimit = 1000000; - -private: - void declareFunction(std::string const& _name, Sort const& _sort); - - z3::sort z3Sort(Sort const& _sort); - z3::sort_vector z3Sort(std::vector const& _sorts); - smtutil::SortPointer fromZ3Sort(z3::sort const& _sort); - std::vector fromZ3Sort(z3::sort_vector const& _sorts); - - z3::context m_context; - z3::solver m_solver; - - std::map m_constants; - std::map m_functions; -}; - -} diff --git a/libsmtutil/Z3Loader.cpp b/libsmtutil/Z3Loader.cpp deleted file mode 100644 index 0211f600d..000000000 --- a/libsmtutil/Z3Loader.cpp +++ /dev/null @@ -1,69 +0,0 @@ -/* - 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 - -#ifndef _GNU_SOURCE -#define _GNU_SOURCE -#endif -#include - -using namespace solidity; -using namespace solidity::smtutil; - -Z3Loader const& Z3Loader::get() -{ - static Z3Loader z3; - return z3; -} - -void* Z3Loader::loadSymbol(char const* _name) const -{ - smtAssert(m_handle, "Attempted to use dynamically loaded Z3, even though it is not available."); - void* sym = dlsym(m_handle, _name); - smtAssert(sym, std::string("Symbol \"") + _name + "\" not found in libz3.so"); - return sym; -} - -bool Z3Loader::available() const -{ - if (m_handle == nullptr) - return false; - unsigned major = 0; - unsigned minor = 0; - unsigned build = 0; - unsigned rev = 0; - Z3_get_version(&major, &minor, &build, &rev); - return major == Z3_MAJOR_VERSION && minor == Z3_MINOR_VERSION; -} - -Z3Loader::Z3Loader() -{ - std::string libname{"libz3.so." + std::to_string(Z3_MAJOR_VERSION) + "." + std::to_string(Z3_MINOR_VERSION)}; - m_handle = dlmopen(LM_ID_NEWLM, libname.c_str(), RTLD_NOW); -} - -Z3Loader::~Z3Loader() -{ - if (m_handle) - dlclose(m_handle); -} diff --git a/libsmtutil/Z3Loader.h b/libsmtutil/Z3Loader.h deleted file mode 100644 index 5e755cb24..000000000 --- a/libsmtutil/Z3Loader.h +++ /dev/null @@ -1,38 +0,0 @@ -/* - 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 - -namespace solidity::smtutil -{ - -class Z3Loader -{ -public: - Z3Loader(Z3Loader const&) = delete; - Z3Loader& operator=(Z3Loader const&) = delete; - static Z3Loader const& get(); - void* loadSymbol(char const* _name) const; - bool available() const; -private: - Z3Loader(); - ~Z3Loader(); - void* m_handle = nullptr; -}; - -} \ No newline at end of file diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index dede97cc0..8ece98388 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -20,16 +20,13 @@ #include -#include +#include #include #include #include -#ifdef HAVE_Z3_DLOPEN -#include -#endif using namespace solidity; using namespace solidity::util; @@ -46,12 +43,10 @@ BMC::BMC( CharStreamProvider const& _charStreamProvider ): SMTEncoder(_context, _settings, _errorReporter, _unsupportedErrorReporter, _charStreamProvider), - m_interface(std::make_unique( - _smtlib2Responses, _smtCallback, _settings.solvers, _settings.timeout, _settings.printQuery + m_interface(std::make_unique( + _smtlib2Responses, _smtCallback, _settings.solvers, _settings.timeout )) { - solAssert(!_settings.printQuery || _settings.solvers == smtutil::SMTSolverChoice::SMTLIB2(), "Only SMTLib2 solver can be enabled to print queries"); -#if defined (HAVE_Z3) || defined (HAVE_CVC4) if (m_settings.solvers.cvc4 || m_settings.solvers.z3) if (!_smtlib2Responses.empty()) m_errorReporter.warning( @@ -61,13 +56,12 @@ BMC::BMC( "These responses will be ignored." "Consider disabling Z3/CVC4 at compilation time in order to use SMT-LIB2 responses." ); -#endif } void BMC::analyze(SourceUnit const& _source, std::map, smt::EncodingContext::IdCompare> _solvedTargets) { // At this point every enabled solver is available. - if (!m_settings.solvers.cvc4 && !m_settings.solvers.smtlib2 && !m_settings.solvers.z3) + if (!m_settings.solvers.cvc4 && !m_settings.solvers.z3) { m_errorReporter.warning( 7710_error, @@ -126,19 +120,12 @@ void BMC::analyze(SourceUnit const& _source, std::mapunhandledQueries().empty() && - m_interface->solvers() == 1 && - m_settings.solvers.smtlib2 - ) + if (!m_interface->unhandledQueries().empty()) m_errorReporter.warning( 8084_error, SourceLocation(), "BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available." " None of the installed solvers was enabled." -#ifdef HAVE_Z3_DLOPEN - " Install libz3.so." + std::to_string(Z3_MAJOR_VERSION) + "." + std::to_string(Z3_MINOR_VERSION) + " to enable Z3." -#endif ); } @@ -1227,8 +1214,9 @@ BMC::checkSatisfiableAndGenerateModel(std::vector const& _e { if (m_settings.printQuery) { - auto portfolio = dynamic_cast(m_interface.get()); - std::string smtlibCode = portfolio->dumpQuery(_expressionsToEvaluate); + auto smtlibInterface = dynamic_cast(m_interface.get()); + solAssert(smtlibInterface, "Must use SMTLib2 solver to dump queries"); + std::string smtlibCode = smtlibInterface->dumpQuery(_expressionsToEvaluate); m_errorReporter.info( 6240_error, "BMC: Requested query:\n" + smtlibCode diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index a803f87d0..5f97ccc6b 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -37,10 +37,6 @@ #include #include -#ifdef HAVE_Z3_DLOPEN -#include -#endif - #include #include @@ -70,14 +66,12 @@ CHC::CHC( SMTEncoder(_context, _settings, _errorReporter, _unsupportedErrorReporter, _charStreamProvider), m_smtlib2Responses(_smtlib2Responses), m_smtCallback(_smtCallback) -{ - solAssert(!_settings.printQuery || _settings.solvers == smtutil::SMTSolverChoice::SMTLIB2(), "Only SMTLib2 solver can be enabled to print queries"); -} +{} void CHC::analyze(SourceUnit const& _source) { // At this point every enabled solver is available. - if (!m_settings.solvers.eld && !m_settings.solvers.smtlib2 && !m_settings.solvers.z3) + if (!m_settings.solvers.eld && !m_settings.solvers.z3) { m_errorReporter.warning( 7649_error, @@ -1172,32 +1166,15 @@ void CHC::resetSourceAnalysis() m_blockCounter = 0; // At this point every enabled solver is available. - // If more than one Horn solver is selected we go with z3. - // We still need the ifdef because of Z3CHCInterface. - if (m_settings.solvers.z3) - { -#ifdef HAVE_Z3 - // z3::fixedpoint does not have a reset mechanism, so we need to create another. - m_interface = std::make_unique(m_settings.timeout); - auto z3Interface = dynamic_cast(m_interface.get()); - solAssert(z3Interface, ""); - m_context.setSolver(z3Interface->z3Interface()); -#else - solAssert(false); -#endif - } - if (!m_settings.solvers.z3) - { - solAssert(m_settings.solvers.smtlib2 || m_settings.solvers.eld); + solAssert(m_settings.solvers.eld || m_settings.solvers.z3); - if (!m_interface) - m_interface = std::make_unique(m_smtlib2Responses, m_smtCallback, m_settings.solvers, m_settings.timeout); + if (!m_interface) + m_interface = std::make_unique(m_smtlib2Responses, m_smtCallback, m_settings.solvers, m_settings.timeout); - auto smtlib2Interface = dynamic_cast(m_interface.get()); - solAssert(smtlib2Interface, ""); - smtlib2Interface->reset(); - m_context.setSolver(smtlib2Interface->smtlib2Interface()); - } + auto smtlib2Interface = dynamic_cast(m_interface.get()); + solAssert(smtlib2Interface, ""); + smtlib2Interface->reset(); + m_context.setSolver(smtlib2Interface->smtlib2Interface()); m_context.reset(); m_context.resetUniqueId(); @@ -1821,32 +1798,7 @@ std::tuple CHC:: switch (result) { case CheckResult::SATISFIABLE: - { - // We still need the ifdef because of Z3CHCInterface. - if (m_settings.solvers.z3) - { -#ifdef HAVE_Z3 - // Even though the problem is SAT, Spacer's pre processing makes counterexamples incomplete. - // We now disable those optimizations and check whether we can still solve the problem. - auto* spacer = dynamic_cast(m_interface.get()); - solAssert(spacer, ""); - spacer->setSpacerOptions(false); - - CheckResult resultNoOpt; - smtutil::Expression invariantNoOpt(true); - CHCSolverInterface::CexGraph cexNoOpt; - std::tie(resultNoOpt, invariantNoOpt, cexNoOpt) = m_interface->query(_query); - - if (resultNoOpt == CheckResult::SATISFIABLE) - cex = std::move(cexNoOpt); - - spacer->setSpacerOptions(true); -#else - solAssert(false); -#endif - } break; - } case CheckResult::UNSATISFIABLE: break; case CheckResult::UNKNOWN: diff --git a/libsolidity/formal/ModelChecker.cpp b/libsolidity/formal/ModelChecker.cpp index 5632ff5c4..eb90694b2 100644 --- a/libsolidity/formal/ModelChecker.cpp +++ b/libsolidity/formal/ModelChecker.cpp @@ -162,15 +162,11 @@ std::vector ModelChecker::unhandledQueries() SMTSolverChoice ModelChecker::availableSolvers() { - smtutil::SMTSolverChoice available = smtutil::SMTSolverChoice::SMTLIB2(); + smtutil::SMTSolverChoice available = smtutil::SMTSolverChoice::None(); #if defined(__linux) || defined(__APPLE__) available.eld = !boost::process::search_path("eld").empty(); -#endif -#ifdef HAVE_Z3 - available.z3 = solidity::smtutil::Z3Interface::available(); -#endif -#ifdef HAVE_CVC4 - available.cvc4 = true; + available.z3 = !boost::process::search_path("z3").empty(); + available.cvc4 = !boost::process::search_path("cvc4").empty(); #endif return available; } @@ -210,9 +206,6 @@ SMTSolverChoice ModelChecker::checkRequestedSolvers(SMTSolverChoice _enabled, Er 8158_error, SourceLocation(), "Solver z3 was selected for SMTChecker but it is not available." -#ifdef HAVE_Z3_DLOPEN - " libz3.so." + std::to_string(Z3_MAJOR_VERSION) + "." + std::to_string(Z3_MINOR_VERSION) + " was not found." -#endif ); } diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp index 2ab494fc4..4e0ea7ef4 100644 --- a/libsolidity/formal/Predicate.cpp +++ b/libsolidity/formal/Predicate.cpp @@ -499,7 +499,15 @@ std::optional Predicate::expressionToString(smtutil::Expression con if (smt::isNumber(*_type)) { solAssert(_expr.sort->kind == Kind::Int, ""); - solAssert(_expr.arguments.empty(), ""); + solAssert(_expr.arguments.empty() || _expr.name == "-", ""); + + if (_expr.name == "-") + { + solAssert(_expr.arguments.size() == 1); + smtutil::Expression const& val = _expr.arguments[0]; + solAssert(val.sort->kind == Kind::Int && val.arguments.empty()); + return "(- " + val.name + ")"; + } if ( _type->category() == Type::Category::Address || diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index d985e359e..656926a58 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -27,7 +27,6 @@ #include #include -#include #include #include diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index 45b872b3d..ad001e8e5 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -23,12 +23,24 @@ #include #include #include +#include #include #include using namespace solidity::util; using namespace solidity::smtutil; +namespace +{ + // HACK to get around Z3 bug in printing type names with spaces (https://github.com/Z3Prover/z3/issues/6850) + void sanitizeTypeName(std::string& name) + { + std::replace(name.begin(), name.end(), ' ', '_'); + std::replace(name.begin(), name.end(), '(', '['); + std::replace(name.begin(), name.end(), ')', ']'); + } +} + namespace solidity::frontend::smt { @@ -118,13 +130,16 @@ SortPointer smtSort(frontend::Type const& _type) else if (baseType->category() == frontend::Type::Category::FixedBytes) tupleName = "fixedbytes"; else + { tupleName = arrayType->baseType()->toString(true); + } tupleName += "_array"; } else tupleName = _type.toString(true); + sanitizeTypeName(tupleName); tupleName += "_tuple"; return std::make_shared( @@ -136,7 +151,9 @@ SortPointer smtSort(frontend::Type const& _type) case Kind::Tuple: { std::vector members; - auto const& tupleName = _type.toString(true); + auto tupleName = _type.toString(true); + sanitizeTypeName(tupleName); + std::vector sorts; if (auto const* tupleType = dynamic_cast(&_type)) diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp index f646ff014..5aa9d2c13 100644 --- a/libsolidity/interface/CompilerStack.cpp +++ b/libsolidity/interface/CompilerStack.cpp @@ -608,12 +608,21 @@ bool CompilerStack::analyze() if (m_modelCheckerSettings.engine.any()) m_modelCheckerSettings.solvers = ModelChecker::checkRequestedSolvers(m_modelCheckerSettings.solvers, m_errorReporter); - ModelChecker modelChecker(m_errorReporter, *this, m_smtlib2Responses, m_modelCheckerSettings, m_readFile); - modelChecker.checkRequestedSourcesAndContracts(allSources); - for (Source const* source: m_sourceOrder) - if (source->ast) - modelChecker.analyze(*source->ast); - m_unhandledSMTLib2Queries += modelChecker.unhandledQueries(); + if (m_modelCheckerSettings.engine.any() && !m_readFile) + m_errorReporter.warning( + 7126_error, + SourceLocation(), + "Model checker analysis requested but no callback for SMT queries was provided, ignoring!" + ); + else + { + ModelChecker modelChecker(m_errorReporter, *this, m_smtlib2Responses, m_modelCheckerSettings, m_readFile); + modelChecker.checkRequestedSourcesAndContracts(allSources); + for (Source const* source: m_sourceOrder) + if (source->ast) + modelChecker.analyze(*source->ast); + m_unhandledSMTLib2Queries += modelChecker.unhandledQueries(); + } } } catch (FatalError const&) diff --git a/libsolidity/interface/SMTSolverCommand.cpp b/libsolidity/interface/SMTSolverCommand.cpp index 92e0485b8..36e7ed176 100644 --- a/libsolidity/interface/SMTSolverCommand.cpp +++ b/libsolidity/interface/SMTSolverCommand.cpp @@ -37,43 +37,97 @@ using solidity::util::errinfo_comment; namespace solidity::frontend { -SMTSolverCommand::SMTSolverCommand(std::string _solverCmd) : m_solverCmd(_solverCmd) {} +namespace +{ +ReadCallback::Result solveWithTemporaryFile( + boost::filesystem::path const& _pathToBinary, + std::vector _commandArgs, + std::string const& _query + ) +{ + auto tempDir = solidity::util::TemporaryDirectory("smt"); + util::h256 queryHash = util::keccak256(_query); + auto queryFileName = tempDir.path() / ("query_" + queryHash.hex() + ".smt2"); + auto queryFile = boost::filesystem::ofstream(queryFileName); + queryFile << _query << std::flush; + + _commandArgs.push_back(queryFileName.string()); + + boost::process::ipstream out; // output from subprocess read by main process + boost::process::child solver( + _pathToBinary, + boost::process::args(_commandArgs), + boost::process::std_out > out, + boost::process::std_err > boost::process::null + ); + + std::vector data; + std::string line; + while (std::getline(out, line)) + if (!line.empty()) + data.push_back(line); + + solver.wait(); + + return ReadCallback::Result{true, boost::join(data, "\n")}; +} + +ReadCallback::Result solveWithPipe( + boost::filesystem::path const& _pathToBinary, + std::vector _commandArgs, + std::string const& _query + ) +{ + boost::process::opstream in; // input to subprocess written to by main process + boost::process::ipstream out; // output from subprocess read by main process + boost::process::child solver( + _pathToBinary, + boost::process::args(_commandArgs), + boost::process::std_out > out, + boost::process::std_in < in, + boost::process::std_err > boost::process::null + ); + + in << _query << std::flush; + in.pipe().close(); + in.close(); + + std::vector data; + std::string line; + while (std::getline(out, line)) + if (!line.empty()) + data.push_back(line); + + solver.wait(); + + return ReadCallback::Result{true, boost::join(data, "\n")}; +} +} // namespace ReadCallback::Result SMTSolverCommand::solve(std::string const& _kind, std::string const& _query) { try { - if (_kind != ReadCallback::kindString(ReadCallback::Kind::SMTQuery)) - solAssert(false, "SMTQuery callback used as callback kind " + _kind); + auto pos = _kind.find(":"); + solAssert(pos != std::string::npos); + auto kind = _kind.substr(0, pos); + auto solverCommand = _kind.substr(pos + 1); + solAssert(kind == ReadCallback::kindString(ReadCallback::Kind::SMTQuery), "SMTQuery callback used as callback kind " + kind); - auto tempDir = solidity::util::TemporaryDirectory("smt"); - util::h256 queryHash = util::keccak256(_query); - auto queryFileName = tempDir.path() / ("query_" + queryHash.hex() + ".smt2"); + std::vector commandArgs; + boost::split(commandArgs, solverCommand, boost::is_any_of(" ")); + solAssert(commandArgs.size() > 0, "SMT command was empty"); + auto solverBinary = commandArgs[0]; + auto pathToBinary = boost::process::search_path(solverBinary); - auto queryFile = boost::filesystem::ofstream(queryFileName); - queryFile << _query; + if (pathToBinary.empty()) + return ReadCallback::Result{false, solverBinary + " binary not found."}; - auto eldBin = boost::process::search_path(m_solverCmd); + commandArgs.erase(commandArgs.begin()); - if (eldBin.empty()) - return ReadCallback::Result{false, m_solverCmd + " binary not found."}; - - boost::process::ipstream pipe; - boost::process::child eld( - eldBin, - queryFileName, - boost::process::std_out > pipe - ); - - std::vector data; - std::string line; - while (eld.running() && std::getline(pipe, line)) - if (!line.empty()) - data.push_back(line); - - eld.wait(); - - return ReadCallback::Result{true, boost::join(data, "\n")}; + if (solverBinary == "eld") + return solveWithTemporaryFile(pathToBinary, std::move(commandArgs), _query); + return solveWithPipe(pathToBinary, std::move(commandArgs), _query); } catch (...) { diff --git a/libsolidity/interface/SMTSolverCommand.h b/libsolidity/interface/SMTSolverCommand.h index 56a6ba171..e3f037519 100644 --- a/libsolidity/interface/SMTSolverCommand.h +++ b/libsolidity/interface/SMTSolverCommand.h @@ -19,8 +19,6 @@ #include -#include - namespace solidity::frontend { @@ -28,19 +26,21 @@ namespace solidity::frontend class SMTSolverCommand { public: - SMTSolverCommand(std::string _solverCmd); + SMTSolverCommand() = default; /// Calls an SMT solver with the given query. + /// The whole command line for invoking the solver is part of @p _kind frontend::ReadCallback::Result solve(std::string const& _kind, std::string const& _query); frontend::ReadCallback::Callback solver() { - return [this](std::string const& _kind, std::string const& _query) { return solve(_kind, _query); }; + return [this](std::string const& _kind, std::string const& _query) { + // TODO: Should be equal + solAssert(_kind.rfind(ReadCallback::kindString(ReadCallback::Kind::SMTQuery), 0) == 0); + return solve(_kind, _query); + }; } -private: - /// The name of the solver's binary. - std::string const m_solverCmd; }; } diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp index c46be3b22..1e0b34a60 100644 --- a/libsolidity/interface/StandardCompiler.cpp +++ b/libsolidity/interface/StandardCompiler.cpp @@ -1094,9 +1094,6 @@ std::variant StandardCompiler: if (!printQuery.isBool()) return formatFatalError(Error::Type::JSONError, "settings.modelChecker.printQuery must be a Boolean value."); - if (!(ret.modelCheckerSettings.solvers == smtutil::SMTSolverChoice::SMTLIB2())) - return formatFatalError(Error::Type::JSONError, "Only SMTLib2 solver can be enabled to print queries"); - ret.modelCheckerSettings.printQuery = printQuery.asBool(); } diff --git a/libsolidity/interface/UniversalCallback.h b/libsolidity/interface/UniversalCallback.h index 1c7888f39..cd787571f 100644 --- a/libsolidity/interface/UniversalCallback.h +++ b/libsolidity/interface/UniversalCallback.h @@ -39,7 +39,7 @@ public: return [this](std::string const& _kind, std::string const& _data) -> ReadCallback::Result { if (_kind == ReadCallback::kindString(ReadCallback::Kind::ReadFile)) return m_fileReader.readFile(_kind, _data); - else if (_kind == ReadCallback::kindString(ReadCallback::Kind::SMTQuery)) + else if (_kind.rfind(ReadCallback::kindString(ReadCallback::Kind::SMTQuery), 0) == 0) // starts with SMTQuery return m_solver.solve(_kind, _data); solAssert(false, "Unknown callback kind."); }; diff --git a/scripts/error_codes.py b/scripts/error_codes.py index 8fe2c4c1b..41efb6f80 100755 --- a/scripts/error_codes.py +++ b/scripts/error_codes.py @@ -208,6 +208,7 @@ def examine_id_coverage(top_dir, source_id_to_file_names, new_ids_only=False): "2961", # SMTChecker, covered by CL tests "6240", # SMTChecker, covered by CL tests "9576", # SMTChecker, covered by CL tests + "7126", # SMTChecker, analysis without callback (not sure how to cover this) } assert len(test_ids & white_ids) == 0, "The sets are not supposed to intersect" test_ids |= white_ids diff --git a/solc/CommandLineInterface.h b/solc/CommandLineInterface.h index 5de69270b..22ac6023a 100644 --- a/solc/CommandLineInterface.h +++ b/solc/CommandLineInterface.h @@ -141,7 +141,7 @@ private: std::ostream& m_serr; bool m_hasOutput = false; FileReader m_fileReader; - SMTSolverCommand m_solverCommand{"eld"}; + SMTSolverCommand m_solverCommand; UniversalCallback m_universalCallback{m_fileReader, m_solverCommand}; std::optional m_standardJsonInput; std::unique_ptr m_compiler; diff --git a/solc/CommandLineParser.cpp b/solc/CommandLineParser.cpp index 53f481ae8..264602c88 100644 --- a/solc/CommandLineParser.cpp +++ b/solc/CommandLineParser.cpp @@ -853,7 +853,7 @@ General Information)").c_str(), ) ( g_strModelCheckerSolvers.c_str(), - po::value()->value_name("cvc4,eld,z3,smtlib2")->default_value("z3"), + po::value()->value_name("cvc4,eld,z3")->default_value("z3"), "Select model checker solvers." ) ( @@ -1323,8 +1323,6 @@ void CommandLineParser::processArgs() if (m_args.count(g_strModelCheckerPrintQuery)) { - if (!(m_options.modelChecker.settings.solvers == smtutil::SMTSolverChoice::SMTLIB2())) - solThrow(CommandLineValidationError, "Only SMTLib2 solver can be enabled to print queries"); m_options.modelChecker.settings.printQuery = true; } diff --git a/test/cmdlineTests/model_checker_divModSlacks_false_all/err b/test/cmdlineTests/model_checker_divModSlacks_false_all/err index 8de36b1ee..bf4337810 100644 --- a/test/cmdlineTests/model_checker_divModSlacks_false_all/err +++ b/test/cmdlineTests/model_checker_divModSlacks_false_all/err @@ -1,15 +1,3 @@ -Warning: CHC: Error trying to invoke SMT solver. - --> model_checker_divModSlacks_false_all/input.sol:6:11: - | -6 | return (a / b, a % b); - | ^^^^^ - -Warning: CHC: Error trying to invoke SMT solver. - --> model_checker_divModSlacks_false_all/input.sol:6:18: - | -6 | return (a / b, a % b); - | ^^^^^ - Warning: CHC: 2 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. Info: BMC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/cmdlineTests/model_checker_divModSlacks_false_chc/err b/test/cmdlineTests/model_checker_divModSlacks_false_chc/err index 56cca82c0..0d6d7341e 100644 --- a/test/cmdlineTests/model_checker_divModSlacks_false_chc/err +++ b/test/cmdlineTests/model_checker_divModSlacks_false_chc/err @@ -1,13 +1 @@ -Warning: CHC: Error trying to invoke SMT solver. - --> model_checker_divModSlacks_false_chc/input.sol:6:11: - | -6 | return (a / b, a % b); - | ^^^^^ - -Warning: CHC: Error trying to invoke SMT solver. - --> model_checker_divModSlacks_false_chc/input.sol:6:18: - | -6 | return (a / b, a % b); - | ^^^^^ - Warning: CHC: 2 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. diff --git a/test/cmdlineTests/model_checker_print_query_all/args b/test/cmdlineTests/model_checker_print_query_all/args index d0b07d5af..af110c121 100644 --- a/test/cmdlineTests/model_checker_print_query_all/args +++ b/test/cmdlineTests/model_checker_print_query_all/args @@ -1 +1 @@ ---model-checker-engine all --model-checker-print-query --model-checker-solvers smtlib2 --model-checker-timeout 1000 +--model-checker-engine all --model-checker-print-query --model-checker-solvers z3 --model-checker-timeout 1000 diff --git a/test/cmdlineTests/model_checker_print_query_all/err b/test/cmdlineTests/model_checker_print_query_all/err index 1a04042cd..b9b8a716d 100644 --- a/test/cmdlineTests/model_checker_print_query_all/err +++ b/test/cmdlineTests/model_checker_print_query_all/err @@ -124,42 +124,4 @@ Info: CHC: Requested query: (check-sat) -Warning: CHC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. - -Warning: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled. - -Info: BMC: Requested query: -(set-option :produce-models true) -(set-option :timeout 1000) -(set-logic ALL) -(declare-fun |x_5_3| () Int) -(declare-fun |error_0| () Int) -(declare-fun |this_0| () Int) -(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) -(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.basefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.prevrandao| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) -(declare-fun |tx_0| () |tx_type|) -(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) -(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) -(declare-fun |crypto_0| () |crypto_type|) -(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) -(declare-fun |abi_0| () |abi_type|) -(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) -(declare-fun |state_0| () |state_type|) -(declare-fun |x_5_4| () Int) -(declare-fun |x_5_0| () Int) -(declare-fun |expr_6_0| () Int) -(declare-fun |x_5_1| () Int) -(declare-fun |expr_9_0| () Int) -(declare-fun |expr_10_0| () Int) -(declare-fun |expr_11_1| () Bool) - -(assert (and (and (and true true) (and (= expr_11_1 (= expr_9_0 expr_10_0)) (and (=> (and true true) true) (and (= expr_10_0 0) (and (=> (and true true) (and (>= expr_9_0 0) (<= expr_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_9_0 x_5_1) (and (ite (and true true) (= x_5_1 expr_6_0) (= x_5_1 x_5_0)) (and (=> (and true true) true) (and (= expr_6_0 0) (and (= x_5_0 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (> (|block.prevrandao| tx_0) 18446744073709551616) (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.prevrandao| tx_0) 0) (<= (|block.prevrandao| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 638722032)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 38)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 18)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 31)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 240)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) (not expr_11_1))) -(declare-const |EVALEXPR_0| Int) -(assert (= |EVALEXPR_0| x_5_1)) -(check-sat) -(get-value (|EVALEXPR_0| )) - - -Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. - -Warning: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled. +Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/cmdlineTests/model_checker_print_query_bmc/args b/test/cmdlineTests/model_checker_print_query_bmc/args index d13bdc43b..12b7c3245 100644 --- a/test/cmdlineTests/model_checker_print_query_bmc/args +++ b/test/cmdlineTests/model_checker_print_query_bmc/args @@ -1 +1 @@ ---model-checker-engine bmc --model-checker-print-query --model-checker-solvers smtlib2 +--model-checker-engine bmc --model-checker-print-query --model-checker-solvers z3 diff --git a/test/cmdlineTests/model_checker_print_query_bmc/err b/test/cmdlineTests/model_checker_print_query_bmc/err index 1a59f87b0..fda2db572 100644 --- a/test/cmdlineTests/model_checker_print_query_bmc/err +++ b/test/cmdlineTests/model_checker_print_query_bmc/err @@ -27,6 +27,4 @@ Info: BMC: Requested query: (get-value (|EVALEXPR_0| )) -Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. - -Warning: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled. +Info: BMC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/cmdlineTests/model_checker_print_query_chc/args b/test/cmdlineTests/model_checker_print_query_chc/args index 752709efb..1260a0874 100644 --- a/test/cmdlineTests/model_checker_print_query_chc/args +++ b/test/cmdlineTests/model_checker_print_query_chc/args @@ -1 +1 @@ ---model-checker-engine chc --model-checker-print-query --model-checker-solvers smtlib2 --model-checker-timeout 1000 +--model-checker-engine chc --model-checker-print-query --model-checker-solvers z3 --model-checker-timeout 1000 diff --git a/test/cmdlineTests/model_checker_print_query_chc/err b/test/cmdlineTests/model_checker_print_query_chc/err index 1dd7f0c98..b9b8a716d 100644 --- a/test/cmdlineTests/model_checker_print_query_chc/err +++ b/test/cmdlineTests/model_checker_print_query_chc/err @@ -124,6 +124,4 @@ Info: CHC: Requested query: (check-sat) -Warning: CHC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. - -Warning: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled. +Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_bmc/args b/test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_bmc/args deleted file mode 100644 index 12b7c3245..000000000 --- a/test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_bmc/args +++ /dev/null @@ -1 +0,0 @@ ---model-checker-engine bmc --model-checker-print-query --model-checker-solvers z3 diff --git a/test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_bmc/err b/test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_bmc/err deleted file mode 100644 index db94bc9ba..000000000 --- a/test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_bmc/err +++ /dev/null @@ -1 +0,0 @@ -Only SMTLib2 solver can be enabled to print queries diff --git a/test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_bmc/exit b/test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_bmc/exit deleted file mode 100644 index d00491fd7..000000000 --- a/test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_bmc/exit +++ /dev/null @@ -1 +0,0 @@ -1 diff --git a/test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_bmc/input.sol b/test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_bmc/input.sol deleted file mode 100644 index eb4cd572a..000000000 --- a/test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_bmc/input.sol +++ /dev/null @@ -1,9 +0,0 @@ -// SPDX-License-Identifier: GPL-3.0 -pragma solidity >=0.0; -contract C -{ - function f() public pure { - uint x = 0; - assert(x == 0); - } -} diff --git a/test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_chc/args b/test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_chc/args deleted file mode 100644 index e3a8c32d4..000000000 --- a/test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_chc/args +++ /dev/null @@ -1 +0,0 @@ ---model-checker-engine chc --model-checker-print-query --model-checker-solvers z3 diff --git a/test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_chc/err b/test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_chc/err deleted file mode 100644 index db94bc9ba..000000000 --- a/test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_chc/err +++ /dev/null @@ -1 +0,0 @@ -Only SMTLib2 solver can be enabled to print queries diff --git a/test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_chc/exit b/test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_chc/exit deleted file mode 100644 index d00491fd7..000000000 --- a/test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_chc/exit +++ /dev/null @@ -1 +0,0 @@ -1 diff --git a/test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_chc/input.sol b/test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_chc/input.sol deleted file mode 100644 index eb4cd572a..000000000 --- a/test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_chc/input.sol +++ /dev/null @@ -1,9 +0,0 @@ -// SPDX-License-Identifier: GPL-3.0 -pragma solidity >=0.0; -contract C -{ - function f() public pure { - uint x = 0; - assert(x == 0); - } -} diff --git a/test/cmdlineTests/model_checker_print_query_superflous_solver/args b/test/cmdlineTests/model_checker_print_query_superflous_solver/args deleted file mode 100644 index 64e5d8872..000000000 --- a/test/cmdlineTests/model_checker_print_query_superflous_solver/args +++ /dev/null @@ -1 +0,0 @@ ---model-checker-engine bmc --model-checker-print-query --model-checker-solvers z3,smtlib2 diff --git a/test/cmdlineTests/model_checker_print_query_superflous_solver/err b/test/cmdlineTests/model_checker_print_query_superflous_solver/err deleted file mode 100644 index db94bc9ba..000000000 --- a/test/cmdlineTests/model_checker_print_query_superflous_solver/err +++ /dev/null @@ -1 +0,0 @@ -Only SMTLib2 solver can be enabled to print queries diff --git a/test/cmdlineTests/model_checker_print_query_superflous_solver/exit b/test/cmdlineTests/model_checker_print_query_superflous_solver/exit deleted file mode 100644 index d00491fd7..000000000 --- a/test/cmdlineTests/model_checker_print_query_superflous_solver/exit +++ /dev/null @@ -1 +0,0 @@ -1 diff --git a/test/cmdlineTests/model_checker_print_query_superflous_solver/input.sol b/test/cmdlineTests/model_checker_print_query_superflous_solver/input.sol deleted file mode 100644 index eb4cd572a..000000000 --- a/test/cmdlineTests/model_checker_print_query_superflous_solver/input.sol +++ /dev/null @@ -1,9 +0,0 @@ -// SPDX-License-Identifier: GPL-3.0 -pragma solidity >=0.0; -contract C -{ - function f() public pure { - uint x = 0; - assert(x == 0); - } -} diff --git a/test/cmdlineTests/model_checker_solvers_smtlib2/args b/test/cmdlineTests/model_checker_solvers_smtlib2/args deleted file mode 100644 index 3d90e9161..000000000 --- a/test/cmdlineTests/model_checker_solvers_smtlib2/args +++ /dev/null @@ -1 +0,0 @@ ---model-checker-engine all --model-checker-solvers smtlib2 diff --git a/test/cmdlineTests/model_checker_solvers_smtlib2/err b/test/cmdlineTests/model_checker_solvers_smtlib2/err deleted file mode 100644 index 3aa989348..000000000 --- a/test/cmdlineTests/model_checker_solvers_smtlib2/err +++ /dev/null @@ -1,7 +0,0 @@ -Warning: CHC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. - -Warning: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled. - -Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. - -Warning: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled. diff --git a/test/cmdlineTests/model_checker_solvers_smtlib2/input.sol b/test/cmdlineTests/model_checker_solvers_smtlib2/input.sol deleted file mode 100644 index 7d05ef6e5..000000000 --- a/test/cmdlineTests/model_checker_solvers_smtlib2/input.sol +++ /dev/null @@ -1,7 +0,0 @@ -// SPDX-License-Identifier: GPL-3.0 -pragma solidity >=0.0; -contract test { - function f(uint x) public pure { - assert(x > 0); - } -} \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_solvers_z3_smtlib2/args b/test/cmdlineTests/model_checker_solvers_z3_smtlib2/args deleted file mode 100644 index 889888874..000000000 --- a/test/cmdlineTests/model_checker_solvers_z3_smtlib2/args +++ /dev/null @@ -1 +0,0 @@ ---model-checker-engine all --model-checker-solvers z3,smtlib2 diff --git a/test/cmdlineTests/model_checker_solvers_z3_smtlib2/err b/test/cmdlineTests/model_checker_solvers_z3_smtlib2/err deleted file mode 100644 index 5699afcde..000000000 --- a/test/cmdlineTests/model_checker_solvers_z3_smtlib2/err +++ /dev/null @@ -1,12 +0,0 @@ -Warning: CHC: Assertion violation happens here. -Counterexample: - -x = 0 - -Transaction trace: -test.constructor() -test.f(0) - --> model_checker_solvers_z3_smtlib2/input.sol:5:3: - | -5 | assert(x > 0); - | ^^^^^^^^^^^^^ diff --git a/test/cmdlineTests/model_checker_solvers_z3_smtlib2/input.sol b/test/cmdlineTests/model_checker_solvers_z3_smtlib2/input.sol deleted file mode 100644 index 7d05ef6e5..000000000 --- a/test/cmdlineTests/model_checker_solvers_z3_smtlib2/input.sol +++ /dev/null @@ -1,7 +0,0 @@ -// SPDX-License-Identifier: GPL-3.0 -pragma solidity >=0.0; -contract test { - function f(uint x) public pure { - assert(x > 0); - } -} \ No newline at end of file diff --git a/test/cmdlineTests/standard_model_checker_divModSlacks_false_all/output.json b/test/cmdlineTests/standard_model_checker_divModSlacks_false_all/output.json index f7ecf690d..16956a2fb 100644 --- a/test/cmdlineTests/standard_model_checker_divModSlacks_false_all/output.json +++ b/test/cmdlineTests/standard_model_checker_divModSlacks_false_all/output.json @@ -1,46 +1,6 @@ { "errors": [ - { - "component": "general", - "errorCode": "1218", - "formattedMessage": "Warning: CHC: Error trying to invoke SMT solver. - --> A:7:15: - | -7 | \t\t\t\t\t\treturn (a / b, a % b); - | \t\t\t\t\t\t ^^^^^ - -", - "message": "CHC: Error trying to invoke SMT solver.", - "severity": "warning", - "sourceLocation": - { - "end": 182, - "file": "A", - "start": 177 - }, - "type": "Warning" - }, - { - "component": "general", - "errorCode": "1218", - "formattedMessage": "Warning: CHC: Error trying to invoke SMT solver. - --> A:7:22: - | -7 | \t\t\t\t\t\treturn (a / b, a % b); - | \t\t\t\t\t\t ^^^^^ - -", - "message": "CHC: Error trying to invoke SMT solver.", - "severity": "warning", - "sourceLocation": - { - "end": 189, - "file": "A", - "start": 184 - }, - "type": "Warning" - }, { "component": "general", "errorCode": "5840", diff --git a/test/cmdlineTests/standard_model_checker_divModSlacks_false_chc/output.json b/test/cmdlineTests/standard_model_checker_divModSlacks_false_chc/output.json index fccd15838..9d04eabff 100644 --- a/test/cmdlineTests/standard_model_checker_divModSlacks_false_chc/output.json +++ b/test/cmdlineTests/standard_model_checker_divModSlacks_false_chc/output.json @@ -1,46 +1,6 @@ { "errors": [ - { - "component": "general", - "errorCode": "1218", - "formattedMessage": "Warning: CHC: Error trying to invoke SMT solver. - --> A:7:15: - | -7 | \t\t\t\t\t\treturn (a / b, a % b); - | \t\t\t\t\t\t ^^^^^ - -", - "message": "CHC: Error trying to invoke SMT solver.", - "severity": "warning", - "sourceLocation": - { - "end": 182, - "file": "A", - "start": 177 - }, - "type": "Warning" - }, - { - "component": "general", - "errorCode": "1218", - "formattedMessage": "Warning: CHC: Error trying to invoke SMT solver. - --> A:7:22: - | -7 | \t\t\t\t\t\treturn (a / b, a % b); - | \t\t\t\t\t\t ^^^^^ - -", - "message": "CHC: Error trying to invoke SMT solver.", - "severity": "warning", - "sourceLocation": - { - "end": 189, - "file": "A", - "start": 184 - }, - "type": "Warning" - }, { "component": "general", "errorCode": "5840", diff --git a/test/cmdlineTests/standard_model_checker_print_query_all/input.json b/test/cmdlineTests/standard_model_checker_print_query_all/input.json index 67fc5d8c7..b1f95688e 100644 --- a/test/cmdlineTests/standard_model_checker_print_query_all/input.json +++ b/test/cmdlineTests/standard_model_checker_print_query_all/input.json @@ -20,7 +20,7 @@ { "engine": "all", "printQuery": true, - "solvers": ["smtlib2"], + "solvers": ["z3"], "timeout": 1000 } } diff --git a/test/cmdlineTests/standard_model_checker_print_query_all/output.json b/test/cmdlineTests/standard_model_checker_print_query_all/output.json index b8e11ced7..a3cd2955a 100644 --- a/test/cmdlineTests/standard_model_checker_print_query_all/output.json +++ b/test/cmdlineTests/standard_model_checker_print_query_all/output.json @@ -1,164 +1,4 @@ { - "auxiliaryInputRequested": - { - "smtlib2queries": - { - "0x1880095c52d8681601c6821e4a5c29740649509af99947bce54102546dd3376a": "(set-option :timeout 1000) -(set-logic HORN) -(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) -(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.basefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.prevrandao| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) -(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) -(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) -(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) -(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) -(declare-fun |interface_0_C_16_0| (Int |abi_type| |crypto_type| |state_type| ) Bool) -(declare-fun |nondet_interface_1_C_16_0| (Int Int |abi_type| |crypto_type| |state_type| |state_type| ) Bool) -(declare-fun |summary_constructor_2_C_16_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (state_0 |state_type|) (this_0 Int) (tx_0 |tx_type|)) -(=> (= error_0 0) (nondet_interface_1_C_16_0 error_0 this_0 abi_0 crypto_0 state_0 state_0)))) - - -(declare-fun |summary_3_function_f__15_16_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) -(declare-fun |summary_4_function_f__15_16_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|)) -(=> (and (and (nondet_interface_1_C_16_0 error_0 this_0 abi_0 crypto_0 state_0 state_1) true) (and (= error_0 0) (summary_4_function_f__15_16_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2))) (nondet_interface_1_C_16_0 error_1 this_0 abi_0 crypto_0 state_0 state_2)))) - - -(declare-fun |block_5_function_f__15_16_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| Int ) Bool) -(declare-fun |block_6_f_14_16_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| Int ) Bool) -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int)) -(block_5_function_f__15_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1 x_5_1))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int)) -(=> (and (and (block_5_function_f__15_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1 x_5_1) (and (and (and (and (= state_1 state_0) (= error_0 0)) true) true) true)) true) (block_6_f_14_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1 x_5_1)))) - - -(declare-fun |block_7_return_function_f__15_16_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| Int ) Bool) -(declare-fun |block_8_function_f__15_16_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| Int ) Bool) -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> (and (and (block_6_f_14_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1 x_5_1) (and (= expr_11_1 (= expr_9_0 expr_10_0)) (and (=> true true) (and (= expr_10_0 0) (and (=> true (and (>= expr_9_0 0) (<= expr_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_9_0 x_5_2) (and (= x_5_2 expr_6_0) (and (=> true true) (and (= expr_6_0 0) (and (= x_5_1 0) true)))))))))) (and (and true (not expr_11_1)) (= error_1 1))) (block_8_function_f__15_16_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_1 x_5_2)))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> (block_8_function_f__15_16_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_1 x_5_2) (summary_3_function_f__15_16_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> (and (and (block_6_f_14_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1 x_5_1) (and (= error_1 error_0) (and (= expr_11_1 (= expr_9_0 expr_10_0)) (and (=> true true) (and (= expr_10_0 0) (and (=> true (and (>= expr_9_0 0) (<= expr_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_9_0 x_5_2) (and (= x_5_2 expr_6_0) (and (=> true true) (and (= expr_6_0 0) (and (= x_5_1 0) true))))))))))) true) (block_7_return_function_f__15_16_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_1 x_5_2)))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> (and (and (block_7_return_function_f__15_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1 x_5_1) true) true) (summary_3_function_f__15_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) - - -(declare-fun |block_9_function_f__15_16_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| Int ) Bool) -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(block_9_function_f__15_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1 x_5_1))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> (and (and (block_9_function_f__15_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1 x_5_1) (and (summary_3_function_f__15_16_0 error_1 this_0 abi_0 crypto_0 tx_0 state_2 state_3) (and (= state_2 (|state_type| (store (|balances| state_1) this_0 (+ (select (|balances| state_1) this_0) funds_2_0)))) (and (and (>= (+ (select (|balances| state_1) this_0) funds_2_0) 0) (<= (+ (select (|balances| state_1) this_0) funds_2_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= funds_2_0 (|msg.value| tx_0)) (and (and (and (and (and (and (and (and (and (and (and (and (and (> (|block.prevrandao| tx_0) 18446744073709551616) (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.prevrandao| tx_0) 0) (<= (|block.prevrandao| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 638722032)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 38)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 18)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 31)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 240)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) (and (and (and (and (= state_1 state_0) (= error_0 0)) true) true) true))))))) true) (summary_4_function_f__15_16_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_3)))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> (and (and (interface_0_C_16_0 this_0 abi_0 crypto_0 state_0) true) (and (summary_4_function_f__15_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (= error_0 0))) (interface_0_C_16_0 this_0 abi_0 crypto_0 state_1)))) - - -(declare-fun |contract_initializer_10_C_16_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) -(declare-fun |contract_initializer_entry_11_C_16_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> (and (and (= state_1 state_0) (= error_0 0)) true) (contract_initializer_entry_11_C_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) - - -(declare-fun |contract_initializer_after_init_12_C_16_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> (and (and (contract_initializer_entry_11_C_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) true) (contract_initializer_after_init_12_C_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> (and (and (contract_initializer_after_init_12_C_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) true) (contract_initializer_10_C_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) - - -(declare-fun |implicit_constructor_entry_13_C_16_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> (and (and (and (and (and (= state_1 state_0) (= error_0 0)) true) true) true) (>= (select (|balances| state_1) this_0) (|msg.value| tx_0))) (implicit_constructor_entry_13_C_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> (and (and (implicit_constructor_entry_13_C_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (and (contract_initializer_10_C_16_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2) true)) (> error_1 0)) (summary_constructor_2_C_16_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_2)))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> (and (and (implicit_constructor_entry_13_C_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (and (= error_1 0) (and (contract_initializer_10_C_16_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2) true))) true) (summary_constructor_2_C_16_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_2)))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> (and (and (summary_constructor_2_C_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) (and (and (and (and (and (and (and (and (and (and (and (and (and (> (|block.prevrandao| tx_0) 18446744073709551616) (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.prevrandao| tx_0) 0) (<= (|block.prevrandao| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.value| tx_0) 0)) (= error_0 0))) (interface_0_C_16_0 this_0 abi_0 crypto_0 state_1)))) - - -(declare-fun |error_target_3_0| () Bool) -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> (and (and (interface_0_C_16_0 this_0 abi_0 crypto_0 state_0) true) (and (summary_4_function_f__15_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (= error_0 1))) error_target_3_0))) - - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> error_target_3_0 false))) -(check-sat) -", - "0xcbfcc2413b217c6564ee01f322c9ca1f34fd79d19961dc3e62aa9c2e5dcb6efc": "(set-option :produce-models true) -(set-option :timeout 1000) -(set-logic ALL) -(declare-fun |x_5_3| () Int) -(declare-fun |error_0| () Int) -(declare-fun |this_0| () Int) -(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) -(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.basefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.prevrandao| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) -(declare-fun |tx_0| () |tx_type|) -(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) -(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) -(declare-fun |crypto_0| () |crypto_type|) -(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) -(declare-fun |abi_0| () |abi_type|) -(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) -(declare-fun |state_0| () |state_type|) -(declare-fun |x_5_4| () Int) -(declare-fun |x_5_0| () Int) -(declare-fun |expr_6_0| () Int) -(declare-fun |x_5_1| () Int) -(declare-fun |expr_9_0| () Int) -(declare-fun |expr_10_0| () Int) -(declare-fun |expr_11_1| () Bool) - -(assert (and (and (and true true) (and (= expr_11_1 (= expr_9_0 expr_10_0)) (and (=> (and true true) true) (and (= expr_10_0 0) (and (=> (and true true) (and (>= expr_9_0 0) (<= expr_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_9_0 x_5_1) (and (ite (and true true) (= x_5_1 expr_6_0) (= x_5_1 x_5_0)) (and (=> (and true true) true) (and (= expr_6_0 0) (and (= x_5_0 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (> (|block.prevrandao| tx_0) 18446744073709551616) (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.prevrandao| tx_0) 0) (<= (|block.prevrandao| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 638722032)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 38)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 18)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 31)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 240)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) (not expr_11_1))) -(declare-const |EVALEXPR_0| Int) -(assert (= |EVALEXPR_0| x_5_1)) -(check-sat) -(get-value (|EVALEXPR_0| )) -" - } - }, "errors": [ { @@ -421,113 +261,13 @@ }, { "component": "general", - "errorCode": "5840", - "formattedMessage": "Warning: CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. + "errorCode": "1391", + "formattedMessage": "Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option \"show proved safe\" to see all of them. ", - "message": "CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.", - "severity": "warning", - "type": "Warning" - }, - { - "component": "general", - "errorCode": "3996", - "formattedMessage": "Warning: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled. - -", - "message": "CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.", - "severity": "warning", - "type": "Warning" - }, - { - "component": "general", - "errorCode": "6240", - "formattedMessage": "Info: BMC: Requested query: -(set-option :produce-models true) -(set-option :timeout 1000) -(set-logic ALL) -(declare-fun |x_5_3| () Int) -(declare-fun |error_0| () Int) -(declare-fun |this_0| () Int) -(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) -(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.basefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.prevrandao| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) -(declare-fun |tx_0| () |tx_type|) -(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) -(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) -(declare-fun |crypto_0| () |crypto_type|) -(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) -(declare-fun |abi_0| () |abi_type|) -(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) -(declare-fun |state_0| () |state_type|) -(declare-fun |x_5_4| () Int) -(declare-fun |x_5_0| () Int) -(declare-fun |expr_6_0| () Int) -(declare-fun |x_5_1| () Int) -(declare-fun |expr_9_0| () Int) -(declare-fun |expr_10_0| () Int) -(declare-fun |expr_11_1| () Bool) - -(assert (and (and (and true true) (and (= expr_11_1 (= expr_9_0 expr_10_0)) (and (=> (and true true) true) (and (= expr_10_0 0) (and (=> (and true true) (and (>= expr_9_0 0) (<= expr_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_9_0 x_5_1) (and (ite (and true true) (= x_5_1 expr_6_0) (= x_5_1 x_5_0)) (and (=> (and true true) true) (and (= expr_6_0 0) (and (= x_5_0 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (> (|block.prevrandao| tx_0) 18446744073709551616) (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.prevrandao| tx_0) 0) (<= (|block.prevrandao| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 638722032)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 38)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 18)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 31)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 240)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) (not expr_11_1))) -(declare-const |EVALEXPR_0| Int) -(assert (= |EVALEXPR_0| x_5_1)) -(check-sat) -(get-value (|EVALEXPR_0| )) - - -", - "message": "BMC: Requested query: -(set-option :produce-models true) -(set-option :timeout 1000) -(set-logic ALL) -(declare-fun |x_5_3| () Int) -(declare-fun |error_0| () Int) -(declare-fun |this_0| () Int) -(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) -(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.basefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.prevrandao| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) -(declare-fun |tx_0| () |tx_type|) -(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) -(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) -(declare-fun |crypto_0| () |crypto_type|) -(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) -(declare-fun |abi_0| () |abi_type|) -(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) -(declare-fun |state_0| () |state_type|) -(declare-fun |x_5_4| () Int) -(declare-fun |x_5_0| () Int) -(declare-fun |expr_6_0| () Int) -(declare-fun |x_5_1| () Int) -(declare-fun |expr_9_0| () Int) -(declare-fun |expr_10_0| () Int) -(declare-fun |expr_11_1| () Bool) - -(assert (and (and (and true true) (and (= expr_11_1 (= expr_9_0 expr_10_0)) (and (=> (and true true) true) (and (= expr_10_0 0) (and (=> (and true true) (and (>= expr_9_0 0) (<= expr_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_9_0 x_5_1) (and (ite (and true true) (= x_5_1 expr_6_0) (= x_5_1 x_5_0)) (and (=> (and true true) true) (and (= expr_6_0 0) (and (= x_5_0 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (> (|block.prevrandao| tx_0) 18446744073709551616) (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.prevrandao| tx_0) 0) (<= (|block.prevrandao| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 638722032)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 38)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 18)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 31)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 240)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) (not expr_11_1))) -(declare-const |EVALEXPR_0| Int) -(assert (= |EVALEXPR_0| x_5_1)) -(check-sat) -(get-value (|EVALEXPR_0| )) -", + "message": "CHC: 1 verification condition(s) proved safe! Enable the model checker option \"show proved safe\" to see all of them.", "severity": "info", "type": "Info" - }, - { - "component": "general", - "errorCode": "2788", - "formattedMessage": "Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. - -", - "message": "BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.", - "severity": "warning", - "type": "Warning" - }, - { - "component": "general", - "errorCode": "8084", - "formattedMessage": "Warning: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled. - -", - "message": "BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled.", - "severity": "warning", - "type": "Warning" } ], "sources": diff --git a/test/cmdlineTests/standard_model_checker_print_query_bmc/input.json b/test/cmdlineTests/standard_model_checker_print_query_bmc/input.json index 7957a58e3..6278950d0 100644 --- a/test/cmdlineTests/standard_model_checker_print_query_bmc/input.json +++ b/test/cmdlineTests/standard_model_checker_print_query_bmc/input.json @@ -20,7 +20,7 @@ { "engine": "bmc", "printQuery": true, - "solvers": ["smtlib2"] + "solvers": ["z3"] } } } diff --git a/test/cmdlineTests/standard_model_checker_print_query_bmc/output.json b/test/cmdlineTests/standard_model_checker_print_query_bmc/output.json index f7b4dc7e2..11d8ad69e 100644 --- a/test/cmdlineTests/standard_model_checker_print_query_bmc/output.json +++ b/test/cmdlineTests/standard_model_checker_print_query_bmc/output.json @@ -1,37 +1,4 @@ { - "auxiliaryInputRequested": - { - "smtlib2queries": - { - "0x8704a7b848b706ef33cbfc06e4f185636f568a29621126b7244355dd0de956bb": "(set-option :produce-models true) -(set-logic ALL) -(declare-fun |error_0| () Int) -(declare-fun |this_0| () Int) -(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) -(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.basefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.prevrandao| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) -(declare-fun |tx_0| () |tx_type|) -(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) -(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) -(declare-fun |crypto_0| () |crypto_type|) -(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) -(declare-fun |abi_0| () |abi_type|) -(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) -(declare-fun |state_0| () |state_type|) -(declare-fun |x_5_0| () Int) -(declare-fun |expr_6_0| () Int) -(declare-fun |x_5_1| () Int) -(declare-fun |expr_9_0| () Int) -(declare-fun |expr_10_0| () Int) -(declare-fun |expr_11_1| () Bool) - -(assert (and (and (and true true) (and (= expr_11_1 (= expr_9_0 expr_10_0)) (and (=> (and true true) true) (and (= expr_10_0 0) (and (=> (and true true) (and (>= expr_9_0 0) (<= expr_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_9_0 x_5_1) (and (ite (and true true) (= x_5_1 expr_6_0) (= x_5_1 x_5_0)) (and (=> (and true true) true) (and (= expr_6_0 0) (and (= x_5_0 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (> (|block.prevrandao| tx_0) 18446744073709551616) (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.prevrandao| tx_0) 0) (<= (|block.prevrandao| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 638722032)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 38)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 18)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 31)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 240)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) (not expr_11_1))) -(declare-const |EVALEXPR_0| Int) -(assert (= |EVALEXPR_0| x_5_1)) -(check-sat) -(get-value (|EVALEXPR_0| )) -" - } - }, "errors": [ { @@ -100,23 +67,13 @@ }, { "component": "general", - "errorCode": "2788", - "formattedMessage": "Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. + "errorCode": "6002", + "formattedMessage": "Info: BMC: 1 verification condition(s) proved safe! Enable the model checker option \"show proved safe\" to see all of them. ", - "message": "BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.", - "severity": "warning", - "type": "Warning" - }, - { - "component": "general", - "errorCode": "8084", - "formattedMessage": "Warning: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled. - -", - "message": "BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled.", - "severity": "warning", - "type": "Warning" + "message": "BMC: 1 verification condition(s) proved safe! Enable the model checker option \"show proved safe\" to see all of them.", + "severity": "info", + "type": "Info" } ], "sources": diff --git a/test/cmdlineTests/standard_model_checker_print_query_chc/input.json b/test/cmdlineTests/standard_model_checker_print_query_chc/input.json index d5801ef26..7a2d1fe79 100644 --- a/test/cmdlineTests/standard_model_checker_print_query_chc/input.json +++ b/test/cmdlineTests/standard_model_checker_print_query_chc/input.json @@ -20,7 +20,7 @@ { "engine": "chc", "printQuery": true, - "solvers": ["smtlib2"], + "solvers": ["z3"], "timeout": 1000 } } diff --git a/test/cmdlineTests/standard_model_checker_print_query_chc/output.json b/test/cmdlineTests/standard_model_checker_print_query_chc/output.json index 9ef925b20..a3cd2955a 100644 --- a/test/cmdlineTests/standard_model_checker_print_query_chc/output.json +++ b/test/cmdlineTests/standard_model_checker_print_query_chc/output.json @@ -1,134 +1,4 @@ { - "auxiliaryInputRequested": - { - "smtlib2queries": - { - "0x1880095c52d8681601c6821e4a5c29740649509af99947bce54102546dd3376a": "(set-option :timeout 1000) -(set-logic HORN) -(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) -(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.basefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.prevrandao| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) -(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) -(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) -(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) -(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) -(declare-fun |interface_0_C_16_0| (Int |abi_type| |crypto_type| |state_type| ) Bool) -(declare-fun |nondet_interface_1_C_16_0| (Int Int |abi_type| |crypto_type| |state_type| |state_type| ) Bool) -(declare-fun |summary_constructor_2_C_16_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (state_0 |state_type|) (this_0 Int) (tx_0 |tx_type|)) -(=> (= error_0 0) (nondet_interface_1_C_16_0 error_0 this_0 abi_0 crypto_0 state_0 state_0)))) - - -(declare-fun |summary_3_function_f__15_16_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) -(declare-fun |summary_4_function_f__15_16_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|)) -(=> (and (and (nondet_interface_1_C_16_0 error_0 this_0 abi_0 crypto_0 state_0 state_1) true) (and (= error_0 0) (summary_4_function_f__15_16_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2))) (nondet_interface_1_C_16_0 error_1 this_0 abi_0 crypto_0 state_0 state_2)))) - - -(declare-fun |block_5_function_f__15_16_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| Int ) Bool) -(declare-fun |block_6_f_14_16_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| Int ) Bool) -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int)) -(block_5_function_f__15_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1 x_5_1))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int)) -(=> (and (and (block_5_function_f__15_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1 x_5_1) (and (and (and (and (= state_1 state_0) (= error_0 0)) true) true) true)) true) (block_6_f_14_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1 x_5_1)))) - - -(declare-fun |block_7_return_function_f__15_16_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| Int ) Bool) -(declare-fun |block_8_function_f__15_16_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| Int ) Bool) -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> (and (and (block_6_f_14_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1 x_5_1) (and (= expr_11_1 (= expr_9_0 expr_10_0)) (and (=> true true) (and (= expr_10_0 0) (and (=> true (and (>= expr_9_0 0) (<= expr_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_9_0 x_5_2) (and (= x_5_2 expr_6_0) (and (=> true true) (and (= expr_6_0 0) (and (= x_5_1 0) true)))))))))) (and (and true (not expr_11_1)) (= error_1 1))) (block_8_function_f__15_16_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_1 x_5_2)))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> (block_8_function_f__15_16_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_1 x_5_2) (summary_3_function_f__15_16_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> (and (and (block_6_f_14_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1 x_5_1) (and (= error_1 error_0) (and (= expr_11_1 (= expr_9_0 expr_10_0)) (and (=> true true) (and (= expr_10_0 0) (and (=> true (and (>= expr_9_0 0) (<= expr_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_9_0 x_5_2) (and (= x_5_2 expr_6_0) (and (=> true true) (and (= expr_6_0 0) (and (= x_5_1 0) true))))))))))) true) (block_7_return_function_f__15_16_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_1 x_5_2)))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> (and (and (block_7_return_function_f__15_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1 x_5_1) true) true) (summary_3_function_f__15_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) - - -(declare-fun |block_9_function_f__15_16_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| Int ) Bool) -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(block_9_function_f__15_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1 x_5_1))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> (and (and (block_9_function_f__15_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1 x_5_1) (and (summary_3_function_f__15_16_0 error_1 this_0 abi_0 crypto_0 tx_0 state_2 state_3) (and (= state_2 (|state_type| (store (|balances| state_1) this_0 (+ (select (|balances| state_1) this_0) funds_2_0)))) (and (and (>= (+ (select (|balances| state_1) this_0) funds_2_0) 0) (<= (+ (select (|balances| state_1) this_0) funds_2_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= funds_2_0 (|msg.value| tx_0)) (and (and (and (and (and (and (and (and (and (and (and (and (and (> (|block.prevrandao| tx_0) 18446744073709551616) (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.prevrandao| tx_0) 0) (<= (|block.prevrandao| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 638722032)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 38)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 18)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 31)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 240)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) (and (and (and (and (= state_1 state_0) (= error_0 0)) true) true) true))))))) true) (summary_4_function_f__15_16_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_3)))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> (and (and (interface_0_C_16_0 this_0 abi_0 crypto_0 state_0) true) (and (summary_4_function_f__15_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (= error_0 0))) (interface_0_C_16_0 this_0 abi_0 crypto_0 state_1)))) - - -(declare-fun |contract_initializer_10_C_16_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) -(declare-fun |contract_initializer_entry_11_C_16_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> (and (and (= state_1 state_0) (= error_0 0)) true) (contract_initializer_entry_11_C_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) - - -(declare-fun |contract_initializer_after_init_12_C_16_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> (and (and (contract_initializer_entry_11_C_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) true) (contract_initializer_after_init_12_C_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> (and (and (contract_initializer_after_init_12_C_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) true) (contract_initializer_10_C_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) - - -(declare-fun |implicit_constructor_entry_13_C_16_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> (and (and (and (and (and (= state_1 state_0) (= error_0 0)) true) true) true) (>= (select (|balances| state_1) this_0) (|msg.value| tx_0))) (implicit_constructor_entry_13_C_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> (and (and (implicit_constructor_entry_13_C_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (and (contract_initializer_10_C_16_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2) true)) (> error_1 0)) (summary_constructor_2_C_16_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_2)))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> (and (and (implicit_constructor_entry_13_C_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (and (= error_1 0) (and (contract_initializer_10_C_16_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2) true))) true) (summary_constructor_2_C_16_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_2)))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> (and (and (summary_constructor_2_C_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) (and (and (and (and (and (and (and (and (and (and (and (and (and (> (|block.prevrandao| tx_0) 18446744073709551616) (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.prevrandao| tx_0) 0) (<= (|block.prevrandao| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.value| tx_0) 0)) (= error_0 0))) (interface_0_C_16_0 this_0 abi_0 crypto_0 state_1)))) - - -(declare-fun |error_target_3_0| () Bool) -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> (and (and (interface_0_C_16_0 this_0 abi_0 crypto_0 state_0) true) (and (summary_4_function_f__15_16_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (= error_0 1))) error_target_3_0))) - - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_1 Bool) (expr_6_0 Int) (expr_9_0 Int) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) -(=> error_target_3_0 false))) -(check-sat) -" - } - }, "errors": [ { @@ -391,23 +261,13 @@ }, { "component": "general", - "errorCode": "5840", - "formattedMessage": "Warning: CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. + "errorCode": "1391", + "formattedMessage": "Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option \"show proved safe\" to see all of them. ", - "message": "CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.", - "severity": "warning", - "type": "Warning" - }, - { - "component": "general", - "errorCode": "3996", - "formattedMessage": "Warning: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled. - -", - "message": "CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.", - "severity": "warning", - "type": "Warning" + "message": "CHC: 1 verification condition(s) proved safe! Enable the model checker option \"show proved safe\" to see all of them.", + "severity": "info", + "type": "Info" } ], "sources": diff --git a/test/cmdlineTests/standard_model_checker_print_query_no_smtlib2_solver/input.json b/test/cmdlineTests/standard_model_checker_print_query_no_smtlib2_solver/input.json deleted file mode 100644 index 0159c256e..000000000 --- a/test/cmdlineTests/standard_model_checker_print_query_no_smtlib2_solver/input.json +++ /dev/null @@ -1,25 +0,0 @@ -{ - "language": "Solidity", - "sources": - { - "A": - { - "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n - contract C - { - function f() public pure { - uint x = 0; - assert(x == 0); - } - }" - } - }, - "settings": - { - "modelChecker": - { - "engine": "all", - "printQuery": true - } - } -} diff --git a/test/cmdlineTests/standard_model_checker_print_query_no_smtlib2_solver/output.json b/test/cmdlineTests/standard_model_checker_print_query_no_smtlib2_solver/output.json deleted file mode 100644 index 42d4b5b2d..000000000 --- a/test/cmdlineTests/standard_model_checker_print_query_no_smtlib2_solver/output.json +++ /dev/null @@ -1,12 +0,0 @@ -{ - "errors": - [ - { - "component": "general", - "formattedMessage": "Only SMTLib2 solver can be enabled to print queries", - "message": "Only SMTLib2 solver can be enabled to print queries", - "severity": "error", - "type": "JSONError" - } - ] -} diff --git a/test/cmdlineTests/standard_model_checker_print_query_superflous_solver/input.json b/test/cmdlineTests/standard_model_checker_print_query_superflous_solver/input.json deleted file mode 100644 index 9ebda0017..000000000 --- a/test/cmdlineTests/standard_model_checker_print_query_superflous_solver/input.json +++ /dev/null @@ -1,26 +0,0 @@ -{ - "language": "Solidity", - "sources": - { - "A": - { - "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n - contract C - { - function f() public pure { - uint x = 0; - assert(x == 0); - } - }" - } - }, - "settings": - { - "modelChecker": - { - "engine": "all", - "printQuery": true, - "solvers": ["smtlib2", "z3"] - } - } -} diff --git a/test/cmdlineTests/standard_model_checker_print_query_superflous_solver/output.json b/test/cmdlineTests/standard_model_checker_print_query_superflous_solver/output.json deleted file mode 100644 index 42d4b5b2d..000000000 --- a/test/cmdlineTests/standard_model_checker_print_query_superflous_solver/output.json +++ /dev/null @@ -1,12 +0,0 @@ -{ - "errors": - [ - { - "component": "general", - "formattedMessage": "Only SMTLib2 solver can be enabled to print queries", - "message": "Only SMTLib2 solver can be enabled to print queries", - "severity": "error", - "type": "JSONError" - } - ] -} diff --git a/test/cmdlineTests/standard_model_checker_solvers_smtlib2/input.json b/test/cmdlineTests/standard_model_checker_solvers_smtlib2/input.json deleted file mode 100644 index 8903ec016..000000000 --- a/test/cmdlineTests/standard_model_checker_solvers_smtlib2/input.json +++ /dev/null @@ -1,18 +0,0 @@ -{ - "language": "Solidity", - "sources": - { - "A": - { - "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract C { function f(uint x) public pure { assert(x > 0); } }" - } - }, - "settings": - { - "modelChecker": - { - "engine": "all", - "solvers": ["smtlib2"] - } - } -} diff --git a/test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json b/test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json deleted file mode 100644 index ebeca53f5..000000000 --- a/test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json +++ /dev/null @@ -1,208 +0,0 @@ -{ - "auxiliaryInputRequested": - { - "smtlib2queries": - { - "0x75b95497d56c30e254a59358d72ddd4e78f9e90db621cfe677e85d05b2252411": "(set-option :produce-models true) -(set-logic ALL) -(declare-fun |x_3_3| () Int) -(declare-fun |error_0| () Int) -(declare-fun |this_0| () Int) -(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) -(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.basefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.prevrandao| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) -(declare-fun |tx_0| () |tx_type|) -(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) -(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) -(declare-fun |crypto_0| () |crypto_type|) -(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) -(declare-fun |abi_0| () |abi_type|) -(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) -(declare-fun |state_0| () |state_type|) -(declare-fun |x_3_4| () Int) -(declare-fun |x_3_0| () Int) -(declare-fun |expr_7_0| () Int) -(declare-fun |expr_8_0| () Int) -(declare-fun |expr_9_1| () Bool) - -(assert (and (and (and true true) (and (= expr_9_1 (> expr_7_0 expr_8_0)) (and (=> (and true true) true) (and (= expr_8_0 0) (and (=> (and true true) (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_3_0) (and (and (>= x_3_0 0) (<= x_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (and (> (|block.prevrandao| tx_0) 18446744073709551616) (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.prevrandao| tx_0) 0) (<= (|block.prevrandao| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 3017696395)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))) (not expr_9_1))) -(declare-const |EVALEXPR_0| Int) -(assert (= |EVALEXPR_0| x_3_0)) -(check-sat) -(get-value (|EVALEXPR_0| )) -", - "0xe3dc20257e2b1bd9c6eb77b75913ec3a5752be174e0fd56af16d9fc95afa1b15": "(set-logic HORN) -(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) -(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.basefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.prevrandao| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) -(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) -(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) -(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) -(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) -(declare-fun |interface_0_C_14_0| (Int |abi_type| |crypto_type| |state_type| ) Bool) -(declare-fun |nondet_interface_1_C_14_0| (Int Int |abi_type| |crypto_type| |state_type| |state_type| ) Bool) -(declare-fun |summary_constructor_2_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (state_0 |state_type|) (this_0 Int) (tx_0 |tx_type|)) -(=> (= error_0 0) (nondet_interface_1_C_14_0 error_0 this_0 abi_0 crypto_0 state_0 state_0)))) - - -(declare-fun |summary_3_function_f__13_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool) -(declare-fun |summary_4_function_f__13_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool) -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int)) -(=> (and (and (nondet_interface_1_C_14_0 error_0 this_0 abi_0 crypto_0 state_0 state_1) true) (and (= error_0 0) (summary_4_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 x_3_0 state_2 x_3_1))) (nondet_interface_1_C_14_0 error_1 this_0 abi_0 crypto_0 state_0 state_2)))) - - -(declare-fun |block_5_function_f__13_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool) -(declare-fun |block_6_f_12_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool) -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int)) -(block_5_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int)) -(=> (and (and (block_5_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (and (and (and (and (= state_1 state_0) (= error_0 0)) true) (and true (= x_3_1 x_3_0))) true)) true) (block_6_f_12_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1)))) - - -(declare-fun |block_7_return_function_f__13_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool) -(declare-fun |block_8_function_f__13_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool) -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int)) -(=> (and (and (block_6_f_12_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (and (= expr_9_1 (> expr_7_0 expr_8_0)) (and (=> true true) (and (= expr_8_0 0) (and (=> true (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_3_1) (and (and (>= x_3_1 0) (<= x_3_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true))))))) (and (and true (not expr_9_1)) (= error_1 1))) (block_8_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1)))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int)) -(=> (block_8_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (summary_3_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1)))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int)) -(=> (and (and (block_6_f_12_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (and (= error_1 error_0) (and (= expr_9_1 (> expr_7_0 expr_8_0)) (and (=> true true) (and (= expr_8_0 0) (and (=> true (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_3_1) (and (and (>= x_3_1 0) (<= x_3_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true)))))))) true) (block_7_return_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1)))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int)) -(=> (and (and (block_7_return_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) true) true) (summary_3_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1)))) - - -(declare-fun |block_9_function_f__13_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool) -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int)) -(block_9_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int)) -(=> (and (and (block_9_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (and (summary_3_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_2 x_3_1 state_3 x_3_2) (and (= state_2 (|state_type| (store (|balances| state_1) this_0 (+ (select (|balances| state_1) this_0) funds_2_0)))) (and (and (>= (+ (select (|balances| state_1) this_0) funds_2_0) 0) (<= (+ (select (|balances| state_1) this_0) funds_2_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= funds_2_0 (|msg.value| tx_0)) (and (and (and (and (and (and (and (and (and (and (and (and (and (> (|block.prevrandao| tx_0) 18446744073709551616) (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.prevrandao| tx_0) 0) (<= (|block.prevrandao| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 3017696395)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) (and (and (and (and (= state_1 state_0) (= error_0 0)) true) (and true (= x_3_1 x_3_0))) true))))))) true) (summary_4_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_3 x_3_2)))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int)) -(=> (and (and (interface_0_C_14_0 this_0 abi_0 crypto_0 state_0) true) (and (summary_4_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (= error_0 0))) (interface_0_C_14_0 this_0 abi_0 crypto_0 state_1)))) - - -(declare-fun |contract_initializer_10_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) -(declare-fun |contract_initializer_entry_11_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int)) -(=> (and (and (= state_1 state_0) (= error_0 0)) true) (contract_initializer_entry_11_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) - - -(declare-fun |contract_initializer_after_init_12_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int)) -(=> (and (and (contract_initializer_entry_11_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) true) (contract_initializer_after_init_12_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int)) -(=> (and (and (contract_initializer_after_init_12_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) true) (contract_initializer_10_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) - - -(declare-fun |implicit_constructor_entry_13_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int)) -(=> (and (and (and (and (and (= state_1 state_0) (= error_0 0)) true) true) true) (>= (select (|balances| state_1) this_0) (|msg.value| tx_0))) (implicit_constructor_entry_13_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int)) -(=> (and (and (implicit_constructor_entry_13_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (and (contract_initializer_10_C_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2) true)) (> error_1 0)) (summary_constructor_2_C_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_2)))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int)) -(=> (and (and (implicit_constructor_entry_13_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (and (= error_1 0) (and (contract_initializer_10_C_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2) true))) true) (summary_constructor_2_C_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_2)))) - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int)) -(=> (and (and (summary_constructor_2_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) (and (and (and (and (and (and (and (and (and (and (and (and (and (> (|block.prevrandao| tx_0) 18446744073709551616) (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.prevrandao| tx_0) 0) (<= (|block.prevrandao| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.value| tx_0) 0)) (= error_0 0))) (interface_0_C_14_0 this_0 abi_0 crypto_0 state_1)))) - - -(declare-fun |error_target_3_0| () Bool) -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int)) -(=> (and (and (interface_0_C_14_0 this_0 abi_0 crypto_0 state_0) true) (and (summary_4_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (= error_0 1))) error_target_3_0))) - - - -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int)) -(=> error_target_3_0 false))) -(check-sat) -" - } - }, - "errors": - [ - { - "component": "general", - "errorCode": "5840", - "formattedMessage": "Warning: CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. - -", - "message": "CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.", - "severity": "warning", - "type": "Warning" - }, - { - "component": "general", - "errorCode": "3996", - "formattedMessage": "Warning: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled. - -", - "message": "CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.", - "severity": "warning", - "type": "Warning" - }, - { - "component": "general", - "errorCode": "2788", - "formattedMessage": "Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. - -", - "message": "BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.", - "severity": "warning", - "type": "Warning" - }, - { - "component": "general", - "errorCode": "8084", - "formattedMessage": "Warning: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled. - -", - "message": "BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled.", - "severity": "warning", - "type": "Warning" - } - ], - "sources": - { - "A": - { - "id": 0 - } - } -} diff --git a/test/cmdlineTests/standard_model_checker_solvers_z3_smtlib2/input.json b/test/cmdlineTests/standard_model_checker_solvers_z3_smtlib2/input.json deleted file mode 100644 index 19913a562..000000000 --- a/test/cmdlineTests/standard_model_checker_solvers_z3_smtlib2/input.json +++ /dev/null @@ -1,18 +0,0 @@ -{ - "language": "Solidity", - "sources": - { - "A": - { - "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract C { function f(uint x) public pure { assert(x > 0); } }" - } - }, - "settings": - { - "modelChecker": - { - "engine": "all", - "solvers": ["z3", "smtlib2"] - } - } -} diff --git a/test/cmdlineTests/standard_model_checker_solvers_z3_smtlib2/output.json b/test/cmdlineTests/standard_model_checker_solvers_z3_smtlib2/output.json deleted file mode 100644 index 2a2c394fd..000000000 --- a/test/cmdlineTests/standard_model_checker_solvers_z3_smtlib2/output.json +++ /dev/null @@ -1,46 +0,0 @@ -{ - "errors": - [ - { - "component": "general", - "errorCode": "6328", - "formattedMessage": "Warning: CHC: Assertion violation happens here. -Counterexample: - -x = 0 - -Transaction trace: -C.constructor() -C.f(0) - --> A:4:47: - | -4 | contract C { function f(uint x) public pure { assert(x > 0); } } - | ^^^^^^^^^^^^^ - -", - "message": "CHC: Assertion violation happens here. -Counterexample: - -x = 0 - -Transaction trace: -C.constructor() -C.f(0)", - "severity": "warning", - "sourceLocation": - { - "end": 119, - "file": "A", - "start": 106 - }, - "type": "Warning" - } - ], - "sources": - { - "A": - { - "id": 0 - } - } -} diff --git a/test/libsolidity/SMTCheckerTest.cpp b/test/libsolidity/SMTCheckerTest.cpp index 6368bfa4f..aa5a36872 100644 --- a/test/libsolidity/SMTCheckerTest.cpp +++ b/test/libsolidity/SMTCheckerTest.cpp @@ -133,6 +133,11 @@ void SMTCheckerTest::setupCompiler() compiler().setModelCheckerSettings(m_modelCheckerSettings); } +std::unique_ptr SMTCheckerTest::createStack() const +{ + return std::make_unique(m_smtCommand.solver()); +} + void SMTCheckerTest::filterObtainedErrors() { SyntaxTest::filterObtainedErrors(); diff --git a/test/libsolidity/SMTCheckerTest.h b/test/libsolidity/SMTCheckerTest.h index 3e8d8238b..011ce6cc8 100644 --- a/test/libsolidity/SMTCheckerTest.h +++ b/test/libsolidity/SMTCheckerTest.h @@ -23,6 +23,7 @@ #include #include +#include #include @@ -39,6 +40,9 @@ public: SMTCheckerTest(std::string const& _filename); void setupCompiler() override; + + std::unique_ptr createStack() const override; + void filterObtainedErrors() override; void printUpdatedExpectations(std::ostream& _stream, std::string const& _linePrefix) const override; @@ -65,6 +69,8 @@ protected: bool m_ignoreCex = false; std::vector m_unfilteredErrorList; + + mutable SMTSolverCommand m_smtCommand; }; } diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol index fad743744..b231ee7ce 100644 --- a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol @@ -28,6 +28,8 @@ contract C { // ---- // Warning 6328: (334-364): CHC: Assertion violation happens here. // Warning 6328: (588-618): CHC: Assertion violation happens here. +// Warning 6328: (971-1001): CHC: Assertion violation might happen here. // Warning 6328: (1086-1116): CHC: Assertion violation might happen here. -// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Warning 4661: (971-1001): BMC: Assertion violation happens here. // Warning 4661: (1086-1116): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol index 41e71ee5b..163caaa73 100644 --- a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol @@ -28,6 +28,8 @@ contract C { // ---- // Warning 6328: (335-365): CHC: Assertion violation happens here. // Warning 6328: (589-619): CHC: Assertion violation happens here. +// Warning 6328: (972-1002): CHC: Assertion violation might happen here. // Warning 6328: (1087-1117): CHC: Assertion violation might happen here. -// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Warning 4661: (972-1002): BMC: Assertion violation happens here. // Warning 4661: (1087-1117): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend_2.sol index 5df0b9995..b662ca2ec 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend_2.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend_2.sol @@ -7,7 +7,7 @@ contract C { _a.transfer(_v); } function inv() public view { - assert(address(this).balance > 0); // should fail + //assert(address(this).balance > 0); // should fail, but commented out because of Spacer nondeterminism assert(address(this).balance > 80); // should fail assert(address(this).balance > 90); // should fail } @@ -16,8 +16,6 @@ contract C { // SMTEngine: all // SMTIgnoreCex: yes // ---- -// Warning 6328: (193-226): CHC: Assertion violation might happen here. -// Warning 6328: (245-279): CHC: Assertion violation happens here. -// Warning 6328: (298-332): CHC: Assertion violation happens here. +// Warning 6328: (299-333): CHC: Assertion violation happens here. +// Warning 6328: (352-386): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor(){ msg.value: 101 }\nC.f(0x11, 5)\nC.f(0x11, 9)\nC.inv() // Warning 1236: (141-156): BMC: Insufficient funds happens here. -// Warning 4661: (193-226): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol index eb0a0c049..6a0f9de7b 100644 --- a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol @@ -21,8 +21,10 @@ contract C { // SMTIgnoreOS: macos // ---- // Warning 4984: (47-50): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. -// Warning 6328: (215-233): CHC: Assertion violation might happen here. +// Warning 6328: (167-185): CHC: Assertion violation might happen here. +// Warning 6328: (267-285): CHC: Assertion violation might happen here. // Warning 6328: (304-322): CHC: Assertion violation happens here. -// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. // Warning 2661: (47-50): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. -// Warning 4661: (215-233): BMC: Assertion violation happens here. +// Warning 4661: (167-185): BMC: Assertion violation happens here. +// Warning 4661: (267-285): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol b/test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol index e8c17d3eb..6c7e7ac59 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol @@ -14,6 +14,7 @@ contract C { } function f(address _a) public { + require(x == 0); uint y = x; _a.call("aaaaa"); assert(y == x); // should fail @@ -23,5 +24,5 @@ contract C { // SMTEngine: all // SMTIgnoreCex: no // ---- -// Warning 9302: (212-228): Return value of low-level calls not used. -// Warning 6328: (232-246): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, lock = false\n_a = 0x0\ny = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0, lock = false\nC.set(1)\nState: x = 1, lock = false\nC.f(0x0)\n _a.call("aaaaa") -- untrusted external call, synthesized as:\n C.set(0) -- reentrant call +// Warning 9302: (231-247): Return value of low-level calls not used. +// Warning 6328: (251-265): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, lock = false\n_a = 0x0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, lock = false\nC.f(0x0)\n _a.call("aaaaa") -- untrusted external call, synthesized as:\n C.set(1) -- reentrant call diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_trusted.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_trusted.sol index 1c557f7a6..b5cd7bf78 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_trusted.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_trusted.sol @@ -32,5 +32,5 @@ contract C { // SMTEngine: chc // SMTExtCalls: trusted // ---- -// Warning 6328: (355-381): CHC: Assertion violation might happen here. // Warning 6328: (385-399): CHC: Assertion violation might happen here. +// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_safe.sol b/test/libsolidity/smtCheckerTests/external_calls/external_safe.sol index 593aba289..fd45ef2d7 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_safe.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_safe.sol @@ -18,4 +18,6 @@ contract C { // SMTEngine: all // SMTIgnoreOS: macos // ---- -// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Warning 6328: (167-181): CHC: Assertion violation might happen here. +// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Warning 4661: (167-181): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol b/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol index 2d92413d5..bf57291b9 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol @@ -17,7 +17,7 @@ contract C { } // ==== // SMTEngine: all -// SMTIgnoreCex: no +// SMTIgnoreCex: yes // ---- // Warning 6328: (242-256): 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 1391: CHC: 7 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/imports/duplicated_errors_1.sol b/test/libsolidity/smtCheckerTests/imports/duplicated_errors_1.sol index a98ba962a..63bc8f79f 100644 --- a/test/libsolidity/smtCheckerTests/imports/duplicated_errors_1.sol +++ b/test/libsolidity/smtCheckerTests/imports/duplicated_errors_1.sol @@ -14,13 +14,7 @@ contract C is B { } // ==== // SMTEngine: all -// SMTSolvers: smtlib2 +// SMTSolvers: z3 // ---- -// Warning 6328: (b.sol:62-75): CHC: Assertion violation might happen here. -// Warning 3996: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled. -// Warning 7812: (b.sol:62-75): BMC: Assertion violation might happen here. -// Warning 8084: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled. -// Warning 6328: (c.sol:68-81): CHC: Assertion violation might happen here. -// Warning 3996: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled. -// Warning 7812: (c.sol:68-81): BMC: Assertion violation might happen here. -// Warning 8084: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled. +// Warning 6328: (b.sol:62-75): CHC: Assertion violation happens here. +// Warning 6328: (c.sol:68-81): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol index ed7ebdfba..024df6ce3 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol @@ -8,8 +8,8 @@ contract LoopFor2 { function testUnboundedForLoop(uint n) public { require(n < b.length); require(n < c.length); - require(n > 0 && n < 100); - b[0] = 900; + require(n > 0 && n < 10); + //b[0] = 900; // Removed because of Spacer's nondeterminism uint[] storage a = b; uint i; while (i < n) { @@ -25,8 +25,7 @@ contract LoopFor2 { // ==== // SMTEngine: all // ---- -// Warning 6368: (288-292): CHC: Out of bounds access might happen here. -// Warning 6368: (459-463): CHC: Out of bounds access happens here. -// Warning 6328: (452-471): CHC: Assertion violation happens here. -// Warning 6328: (475-494): CHC: Assertion violation happens here. +// Warning 6368: (506-510): CHC: Out of bounds access happens here.\nCounterexample:\nb = [1, 0], c = [0, 0]\nn = 1\na = []\ni = 1\n\nTransaction trace:\nLoopFor2.constructor()\nState: b = [], c = []\nLoopFor2.p()\nState: b = [0], c = [0]\nLoopFor2.p()\nState: b = [0, 0], c = [0, 0]\nLoopFor2.testUnboundedForLoop(1) +// Warning 6328: (499-518): CHC: Assertion violation happens here.\nCounterexample:\nb = [1, 0], c = [0, 0]\nn = 1\ni = 1\n\nTransaction trace:\nLoopFor2.constructor()\nState: b = [], c = []\nLoopFor2.p()\nState: b = [0], c = [0]\nLoopFor2.p()\nState: b = [0, 0], c = [0, 0]\nLoopFor2.testUnboundedForLoop(1) +// Warning 6328: (522-541): CHC: Assertion violation happens here.\nCounterexample:\nb = [1, 0], c = [0, 0]\nn = 1\ni = 1\n\nTransaction trace:\nLoopFor2.constructor()\nState: b = [], c = []\nLoopFor2.p()\nState: b = [0], c = [0]\nLoopFor2.p()\nState: b = [0, 0], c = [0, 0]\nLoopFor2.testUnboundedForLoop(1) // Info 1391: CHC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol b/test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol index d18f605f7..32c9780d1 100644 --- a/test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol +++ b/test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol @@ -23,6 +23,4 @@ contract C { // SMTIgnoreCex: yes // SMTIgnoreOS: macos // ---- -// Warning 6328: (335-354): CHC: Assertion violation might happen here. -// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. -// Warning 4661: (335-354): BMC: Assertion violation happens here. +// Info 1391: CHC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol b/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol index 5ac20c96f..25c48b130 100644 --- a/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol +++ b/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol @@ -36,11 +36,11 @@ contract C // SMTIgnoreCex: yes // SMTIgnoreOS: macos // ---- -// Warning 6368: (439-453): CHC: Out of bounds access happens here. +// Warning 6368: (439-453): CHC: Out of bounds access happens here.\nCounterexample:\n\nx = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n C.f(map) -- internal call // Warning 6368: (465-480): CHC: Out of bounds access might happen here. -// Warning 6368: (492-508): CHC: Out of bounds access happens here. -// Warning 6368: (492-511): CHC: Out of bounds access happens here. -// Warning 6368: (622-636): CHC: Out of bounds access happens here. +// Warning 6368: (492-508): CHC: Out of bounds access happens here.\nCounterexample:\n\nx = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n C.f(map) -- internal call +// Warning 6368: (492-511): CHC: Out of bounds access happens here.\nCounterexample:\n\nx = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n C.f(map) -- internal call +// Warning 6368: (622-636): CHC: Out of bounds access happens here.\nCounterexample:\n\nx = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n C.f(map) -- internal call // Warning 6368: (737-752): CHC: Out of bounds access might happen here. // Warning 6368: (850-866): CHC: Out of bounds access happens here. // Warning 6368: (850-869): CHC: Out of bounds access happens here. diff --git a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol index bb4ef0342..d89f020ae 100644 --- a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol +++ b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol @@ -32,5 +32,6 @@ 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 1391: CHC: 13 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Info 1391: CHC: 12 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_storage_safe.sol b/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_storage_safe.sol index b2f7b9825..7b3ff5115 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_storage_safe.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_storage_safe.sol @@ -53,4 +53,55 @@ contract C { // ==== // SMTEngine: all // ---- -// Info 1391: CHC: 51 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Warning 6368: (212-217): CHC: Out of bounds access might happen here. +// Warning 6368: (234-239): CHC: Out of bounds access might happen here. +// Warning 6328: (227-247): CHC: Assertion violation might happen here. +// Warning 6368: (251-256): CHC: Out of bounds access might happen here. +// Warning 6368: (275-280): CHC: Out of bounds access might happen here. +// Warning 6328: (268-290): CHC: Assertion violation might happen here. +// Warning 6368: (294-299): CHC: Out of bounds access might happen here. +// Warning 6368: (312-317): CHC: Out of bounds access might happen here. +// Warning 6368: (330-335): CHC: Out of bounds access might happen here. +// Warning 6368: (348-353): CHC: Out of bounds access might happen here. +// Warning 6368: (348-358): CHC: Out of bounds access might happen here. +// Warning 6368: (373-378): CHC: Out of bounds access might happen here. +// Warning 6368: (373-383): CHC: Out of bounds access might happen here. +// Warning 6328: (366-389): CHC: Assertion violation might happen here. +// Warning 6368: (393-398): CHC: Out of bounds access might happen here. +// Warning 6368: (412-417): CHC: Out of bounds access might happen here. +// Warning 6368: (431-436): CHC: Out of bounds access might happen here. +// Warning 6368: (450-455): CHC: Out of bounds access might happen here. +// Warning 6368: (469-474): CHC: Out of bounds access might happen here. +// Warning 6368: (488-493): CHC: Out of bounds access might happen here. +// Warning 6368: (488-499): CHC: Out of bounds access might happen here. +// Warning 6368: (516-521): CHC: Out of bounds access might happen here. +// Warning 6368: (516-527): CHC: Out of bounds access might happen here. +// Warning 6328: (509-535): CHC: Assertion violation might happen here. +// Warning 6368: (539-544): CHC: Out of bounds access might happen here. +// Warning 6368: (558-563): CHC: Out of bounds access might happen here. +// Warning 6368: (577-582): CHC: Out of bounds access might happen here. +// Warning 6368: (596-601): CHC: Out of bounds access might happen here. +// Warning 6368: (615-620): CHC: Out of bounds access might happen here. +// Warning 6368: (634-639): CHC: Out of bounds access might happen here. +// Warning 6368: (634-645): CHC: Out of bounds access might happen here. +// Warning 6368: (658-663): CHC: Out of bounds access might happen here. +// Warning 6368: (658-669): CHC: Out of bounds access might happen here. +// Warning 6368: (682-687): CHC: Out of bounds access might happen here. +// Warning 6368: (682-693): CHC: Out of bounds access might happen here. +// Warning 6368: (706-711): CHC: Out of bounds access might happen here. +// Warning 6368: (706-717): CHC: Out of bounds access might happen here. +// Warning 6368: (730-735): CHC: Out of bounds access might happen here. +// Warning 6368: (730-741): CHC: Out of bounds access might happen here. +// Warning 6368: (754-759): CHC: Out of bounds access might happen here. +// Warning 6368: (754-765): CHC: Out of bounds access might happen here. +// Warning 6368: (778-783): CHC: Out of bounds access might happen here. +// Warning 6368: (778-789): CHC: Out of bounds access might happen here. +// Warning 6368: (778-794): CHC: Out of bounds access might happen here. +// Warning 6368: (809-814): CHC: Out of bounds access might happen here. +// Warning 6368: (809-820): CHC: Out of bounds access might happen here. +// Warning 6368: (809-825): CHC: Out of bounds access might happen here. +// Warning 6328: (802-831): CHC: Assertion violation might happen here. +// Warning 2529: (835-843): CHC: Empty array "pop" might happen here. +// Warning 2529: (847-855): CHC: Empty array "pop" might happen here. +// Warning 2529: (859-867): CHC: Empty array "pop" might happen here. +// Info 6002: BMC: 5 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/types/struct_array_branches_2d.sol b/test/libsolidity/smtCheckerTests/types/struct_array_branches_2d.sol index 0d45aee14..7f7e06a06 100644 --- a/test/libsolidity/smtCheckerTests/types/struct_array_branches_2d.sol +++ b/test/libsolidity/smtCheckerTests/types/struct_array_branches_2d.sol @@ -17,5 +17,4 @@ contract C // SMTEngine: all // SMTIgnoreOS: macos // ---- -// Warning 6368: (216-225): CHC: Out of bounds access might happen here. -// Info 1391: CHC: 9 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Info 1391: CHC: 10 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/types/type_minmax.sol b/test/libsolidity/smtCheckerTests/types/type_minmax.sol index da9bb1b6d..ea0cf0591 100644 --- a/test/libsolidity/smtCheckerTests/types/type_minmax.sol +++ b/test/libsolidity/smtCheckerTests/types/type_minmax.sol @@ -82,4 +82,18 @@ contract C { // SMTEngine: all // ---- // Warning 6328: (178-207): CHC: Assertion violation happens here. -// Info 1391: CHC: 24 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Warning 6328: (872-900): CHC: Assertion violation might happen here. +// Warning 6328: (942-970): CHC: Assertion violation might happen here. +// Warning 6328: (1015-1045): CHC: Assertion violation might happen here. +// Warning 6328: (1125-1147): CHC: Assertion violation might happen here. +// Warning 6328: (1192-1215): CHC: Assertion violation might happen here. +// Warning 6328: (1260-1283): CHC: Assertion violation might happen here. +// Warning 6328: (1328-1351): CHC: Assertion violation might happen here. +// Warning 6328: (1399-1423): CHC: Assertion violation might happen here. +// Warning 6328: (1503-1530): CHC: Assertion violation might happen here. +// Warning 6328: (1575-1604): CHC: Assertion violation might happen here. +// Warning 6328: (1649-1678): CHC: Assertion violation might happen here. +// Warning 6328: (1723-1752): CHC: Assertion violation might happen here. +// Warning 6328: (1800-1831): CHC: Assertion violation might happen here. +// Info 1391: CHC: 11 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Info 6002: BMC: 13 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/solc/CommandLineParser.cpp b/test/solc/CommandLineParser.cpp index 43cef9d27..818ae8af5 100644 --- a/test/solc/CommandLineParser.cpp +++ b/test/solc/CommandLineParser.cpp @@ -151,7 +151,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options) "--model-checker-show-proved-safe", "--model-checker-show-unproved", "--model-checker-show-unsupported", - "--model-checker-solvers=z3,smtlib2", + "--model-checker-solvers=z3", "--model-checker-targets=underflow,divByZero", "--model-checker-timeout=5" }; @@ -221,7 +221,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options) true, true, true, - {false, false, true, true}, + {false, false, true}, {{VerificationTargetType::Underflow, VerificationTargetType::DivByZero}}, 5, }; @@ -413,7 +413,7 @@ BOOST_AUTO_TEST_CASE(invalid_options_input_modes_combinations) {"--model-checker-div-mod-no-slacks", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}}, {"--model-checker-engine=bmc", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}}, {"--model-checker-invariants=contract,reentrancy", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}}, - {"--model-checker-solvers=z3,smtlib2", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}}, + {"--model-checker-solvers=z3", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}}, {"--model-checker-timeout=5", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}}, {"--model-checker-contracts=contract1.yul:A,contract2.yul:B", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}}, {"--model-checker-targets=underflow,divByZero", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}}