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

Merge 475cfe2532 into 64a0f62700

Browse Source
This commit is contained in:
Martin Blicha 2023-09-11 11:58:07 -07:00 committed by GitHub
commit b9c41c21bf
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
94 changed files with 1184 additions and 3053 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

57
CMakeLists.txt
View File

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

606
libsmtutil/CHCSmtLib2Interface.cpp
View File

@ -18,22 +18,35 @@
#include <libsmtutil/CHCSmtLib2Interface.h>
#include <libsmtutil/SMTLibParser.h>
#include <libsolutil/Keccak256.h>
#include <libsolutil/StringUtils.h>
#include <libsolutil/Visitor.h>
#include <liblangutil/Common.h>
#include <boost/algorithm/string/join.hpp>
#include <boost/algorithm/string/predicate.hpp>
#include <range/v3/view.hpp>
#include <range/v3/algorithm/find.hpp>
#include <range/v3/algorithm/find_if.hpp>
#include <array>
#include <fstream>
#include <iostream>
#include <memory>
#include <stack>
#include <stdexcept>
#include <unordered_map>
#include <variant>
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<unsigned> _queryTimeout
):
CHCSolverInterface(_queryTimeout),
m_smtlib2(std::make_unique<SMTLib2Interface>(_queryResponses, _smtCallback, m_queryTimeout)),
m_smtlib2(std::make_unique<SMTLib2Interface>(_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<CheckResult, Expression, CHCSolverInterface::CexGraph> 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<SortPointer> 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<FunctionSort>(_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<std::string, SortPointer> 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<SortPointer> 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<TupleSort>(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<ArraySort>(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<BitVectorSort>(std::stoul(asAtom(args[2])));
}
}
smtAssert(false, "Unknown sort encountered");
}
smtutil::Expression parseQuantifier(
std::string const& quantifierName,
std::vector<SMTLib2Expression> const& varList,
SMTLib2Expression const& coreExpression
)
{
std::vector<std::pair<std::string, SortPointer>> 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<SMTLib2Expression> const& _subExpr) {
SortPointer sort;
std::vector<smtutil::Expression> 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<SortSort>(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<std::string> 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<SortSort>(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<BitVectorSort>(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<SMTLib2Expression>;
std::unordered_map<std::string, BindingRecord> bindings;
std::vector<std::string> varNames;
std::vector<std::size_t> 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<std::pair<std::string, SMTLib2Expression>> 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<SMTLib2Expression const*> proofStack;
proofStack.push(&asSubExpressions(proofNode).at(1));
std::map<SMTLib2Expression const*, unsigned> 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<Expression> 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<Expression> 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));
}

9
libsmtutil/CHCSmtLib2Interface.h
View File

@ -32,6 +32,7 @@ namespace solidity::smtutil
class CHCSmtLib2Interface: public CHCSolverInterface
{
public:
explicit CHCSmtLib2Interface(
std::map<util::h256, std::string> 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<SortPointer> 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<SMTLib2Interface> m_smtlib2;
@ -85,8 +90,6 @@ private:
frontend::ReadCallback::Callback m_smtCallback;
SMTSolverChoice m_enabledSolvers;
std::map<Sort const*, std::string> m_sortNames;
};
}

38
libsmtutil/CMakeLists.txt
View File

@ -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()

336
libsmtutil/CVC4Interface.cpp
View File

@ -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 <http://www.gnu.org/licenses/>.
*/
// SPDX-License-Identifier: GPL-3.0
#include <libsmtutil/CVC4Interface.h>
#include <libsolutil/CommonIO.h>
#include <libsolutil/Exceptions.h>
#include <cvc4/util/bitvector.h>
using namespace solidity;
using namespace solidity::util;
using namespace solidity::smtutil;
CVC4Interface::CVC4Interface(std::optional<unsigned> _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<CheckResult, std::vector<std::string>> CVC4Interface::check(std::vector<Expression> const& _expressionsToEvaluate)
{
CheckResult result;
std::vector<std::string> 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<CVC4::Expr> 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<SortSort>(_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<unsigned>(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<IntSort>(_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> sortSort = std::dynamic_pointer_cast<SortSort>(_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> tupleSort = std::dynamic_pointer_cast<TupleSort>(_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> tupleSort = std::dynamic_pointer_cast<TupleSort>(_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<BitVectorSort const&>(_sort).size);
case Kind::Function:
{
FunctionSort const& fSort = dynamic_cast<FunctionSort const&>(_sort);
return m_context.mkFunctionType(cvc4Sort(fSort.domain), cvc4Sort(*fSort.codomain));
}
case Kind::Array:
{
auto const& arraySort = dynamic_cast<ArraySort const&>(_sort);
return m_context.mkArrayType(cvc4Sort(*arraySort.domain), cvc4Sort(*arraySort.range));
}
case Kind::Tuple:
{
auto const& tupleSort = dynamic_cast<TupleSort const&>(_sort);
return m_context.mkTupleType(cvc4Sort(tupleSort.components));
}
default:
break;
}
smtAssert(false, "");
// Cannot be reached.
return m_context.integerType();
}
std::vector<CVC4::Type> CVC4Interface::cvc4Sort(std::vector<SortPointer> const& _sorts)
{
std::vector<CVC4::Type> cvc4Sorts;
for (auto const& _sort: _sorts)
cvc4Sorts.push_back(cvc4Sort(*_sort));
return cvc4Sorts;
}

74
libsmtutil/CVC4Interface.h
View File

@ -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 <http://www.gnu.org/licenses/>.
*/
// SPDX-License-Identifier: GPL-3.0
#pragma once
#include <libsmtutil/SolverInterface.h>
#if defined(__GLIBC__)
// The CVC4 headers includes the deprecated system headers <ext/hash_map>
// and <ext/hash_set>. These headers cause a warning that will break the
// build, unless _GLIBCXX_PERMIT_BACKWARD_HASH is set.
#define _GLIBCXX_PERMIT_BACKWARD_HASH
#endif
#include <cvc4/cvc4.h>
#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<unsigned> _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<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
private:
CVC4::Expr toCVC4Expr(Expression const& _expr);
CVC4::Type cvc4Sort(Sort const& _sort);
std::vector<CVC4::Type> cvc4Sort(std::vector<SortPointer> const& _sorts);
CVC4::ExprManager m_context;
CVC4::SmtEngine m_solver;
std::map<std::string, CVC4::Expr> 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;
};
}

164
libsmtutil/SMTLib2Interface.cpp
View File

@ -18,6 +18,8 @@
#include <libsmtutil/SMTLib2Interface.h>
#include <libsmtutil/SMTLibParser.h>
#include <libsolutil/Keccak256.h>
#include <boost/algorithm/string/join.hpp>
@ -39,13 +41,14 @@ using namespace solidity::frontend;
using namespace solidity::smtutil;
SMTLib2Interface::SMTLib2Interface(
std::map<h256, std::string> _queryResponses,
[[maybe_unused]] std::map<h256, std::string> _queryResponses,
ReadCallback::Callback _smtCallback,
SMTSolverChoice _enabledSolvers,
std::optional<unsigned> _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<FunctionSort>(_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<std::string> parseValues(std::string const& solverAnswer)
{
std::vector<std::string> 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<CheckResult, std::vector<std::string>> SMTLib2Interface::check(std::vector<Expression> 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<std::string> 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<std::string> 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<std::string> 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<ArraySort>(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<ArraySort const&>(_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<SortPointer> 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<Expression
return command;
}
std::vector<std::string> SMTLib2Interface::parseValues(std::string::const_iterator _start, std::string::const_iterator _end)
{
std::vector<std::string> 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<Expression> const& _expressionsToEvaluate)
{
return boost::algorithm::join(m_accumulatedOutput, "\n") +

16
libsmtutil/SMTLib2Interface.h
View File

@ -44,6 +44,7 @@ public:
explicit SMTLib2Interface(
std::map<util::h256, std::string> _queryResponses = {},
frontend::ReadCallback::Callback _smtCallback = {},
SMTSolverChoice _enabledSolvers = SMTSolverChoice::None(),
std::optional<unsigned> _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<SortPointer> const& _sort);
std::map<std::string, SortPointer> variables() { return m_variables; }
std::vector<std::pair<std::string, std::string>> const& userSorts() const { return m_userSorts; }
auto const& sortNames() const { return m_sortNames; }
std::string dumpQuery(std::vector<Expression> 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<Expression> const& _expressionsToEvaluate);
std::vector<std::string> 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<std::string> m_accumulatedOutput;
std::map<std::string, SortPointer> 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<std::pair<std::string, std::string>> m_userSorts;
// TODO: Shouldn't sorts be unique objects?
std::map<SortPointer, std::string> m_sortNames;
std::map<util::h256, std::string> m_queryResponses;
std::vector<std::string> m_unhandledQueries;
frontend::ReadCallback::Callback m_smtCallback;
SMTSolverChoice m_enabledSolvers;
};
}

79
libsmtutil/SMTLibParser.cpp Normal file
View File

@ -0,0 +1,79 @@
#include <libsmtutil/SMTLibParser.h>
#include <liblangutil/Common.h>
#include <libsolutil/Visitor.h>
#include <libsolutil/StringUtils.h>
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<SMTLib2Expression> const& _subExpr) {
std::vector<std::string> 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<SMTLib2Expression> 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<char>(m_input.get());
if (token() == ';')
while (token() != '\n' && token() != 0)
m_token = static_cast<char>(m_input.get());
}
void SMTLib2Parser::skipWhitespace() {
while (isWhiteSpace(token()))
advance();
}

90
libsmtutil/SMTLibParser.h Normal file
View File

@ -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 <http://www.gnu.org/licenses/>.
*/
// SPDX-License-Identifier: GPL-3.0
#pragma once
#include <liblangutil/Exceptions.h>
#include <iostream>
#include <string>
#include <variant>
#include <vector>
namespace solidity::smtutil
{
struct SMTLib2Expression {
using args_t = std::vector<SMTLib2Expression>;
std::variant<std::string, args_t> data;
std::string toString() const;
};
inline bool isAtom(SMTLib2Expression const & expr)
{
return std::holds_alternative<std::string>(expr.data);
}
inline std::string const& asAtom(SMTLib2Expression const& expr)
{
solAssert(isAtom(expr));
return std::get<std::string>(expr.data);
}
inline auto const& asSubExpressions(SMTLib2Expression const& expr)
{
solAssert(!isAtom(expr));
return std::get<SMTLib2Expression::args_t>(expr.data);
}
inline auto& asSubExpressions(SMTLib2Expression& expr)
{
solAssert(!isAtom(expr));
return std::get<SMTLib2Expression::args_t>(expr.data);
}
class SMTLib2Parser {
public:
class ParsingException {};
SMTLib2Parser(std::istream& _input) :
m_input(_input),
m_token(static_cast<char>(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;
};
}

167
libsmtutil/SMTPortfolio.cpp
View File

@ -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 <http://www.gnu.org/licenses/>.
*/
// SPDX-License-Identifier: GPL-3.0
#include <libsmtutil/SMTPortfolio.h>
#ifdef HAVE_Z3
#include <libsmtutil/Z3Interface.h>
#endif
#ifdef HAVE_CVC4
#include <libsmtutil/CVC4Interface.h>
#endif
#include <libsmtutil/SMTLib2Interface.h>
using namespace solidity;
using namespace solidity::util;
using namespace solidity::frontend;
using namespace solidity::smtutil;
SMTPortfolio::SMTPortfolio(
std::map<h256, std::string> _smtlib2Responses,
frontend::ReadCallback::Callback _smtCallback,
[[maybe_unused]] SMTSolverChoice _enabledSolvers,
std::optional<unsigned> _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<SMTLib2Interface>(std::move(_smtlib2Responses), std::move(_smtCallback), m_queryTimeout));
#ifdef HAVE_Z3
if (_enabledSolvers.z3 && Z3Interface::available())
m_solvers.emplace_back(std::make_unique<Z3Interface>(m_queryTimeout));
#endif
#ifdef HAVE_CVC4
if (_enabledSolvers.cvc4)
m_solvers.emplace_back(std::make_unique<CVC4Interface>(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<CheckResult, std::vector<std::string>> SMTPortfolio::check(std::vector<Expression> const& _expressionsToEvaluate)
{
CheckResult lastResult = CheckResult::ERROR;
std::vector<std::string> finalValues;
for (auto const& s: m_solvers)
{
CheckResult result;
std::vector<std::string> 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<std::string> 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<SMTLib2Interface*>(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<Expression> const& _expressionsToEvaluate)
{
// This code assumes that the constructor guarantees that
// SmtLib2Interface is in position 0, if enabled.
auto smtlib2 = dynamic_cast<SMTLib2Interface*>(m_solvers.front().get());
solAssert(smtlib2, "Must use SMTLib2 solver to dump queries");
return smtlib2->dumpQuery(_expressionsToEvaluate);
}

77
libsmtutil/SMTPortfolio.h
View File

@ -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 <http://www.gnu.org/licenses/>.
*/
// SPDX-License-Identifier: GPL-3.0
#pragma once
#include <libsmtutil/SolverInterface.h>
#include <libsolidity/interface/ReadFile.h>
#include <libsolutil/FixedHash.h>
#include <map>
#include <vector>
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<util::h256, std::string> _smtlib2Responses = {},
frontend::ReadCallback::Callback _smtCallback = {},
SMTSolverChoice _enabledSolvers = SMTSolverChoice::All(),
std::optional<unsigned> _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<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
std::vector<std::string> unhandledQueries() override;
size_t solvers() override { return m_solvers.size(); }
std::string dumpQuery(std::vector<Expression> const& _expressionsToEvaluate);
private:
static bool solverAnswered(CheckResult result);
std::vector<std::unique_ptr<SolverInterface>> m_solvers;
std::vector<Expression> m_assertions;
};
}

22
libsmtutil/SolverInterface.h
View File

@ -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<SMTSolverChoice> 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<std::string> const solvers{"cvc4", "eld", "smtlib2", "z3"};
static std::set<std::string> 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

242
libsmtutil/Z3CHCInterface.cpp
View File

@ -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 <http://www.gnu.org/licenses/>.
*/
// SPDX-License-Identifier: GPL-3.0
#include <libsmtutil/Z3CHCInterface.h>
#include <libsolutil/CommonIO.h>
#include <set>
#include <stack>
using namespace solidity;
using namespace solidity::smtutil;
Z3CHCInterface::Z3CHCInterface(std::optional<unsigned> _queryTimeout):
CHCSolverInterface(_queryTimeout),
m_z3Interface(std::make_unique<Z3Interface>(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<CheckResult, Expression, CHCSolverInterface::CexGraph> 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<std::string> 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<z3::expr> proofStack;
proofStack.push(_proof.arg(0));
auto const& root = proofStack.top();
graph.nodes.emplace(root.id(), m_z3Interface->fromZ3Expr(fact(root)));
std::set<unsigned> 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<std::string> Z3CHCInterface::arguments(z3::expr const& _predicate)
{
smtAssert(_predicate.is_app(), "");
std::vector<std::string> args;
for (unsigned i = 0; i < _predicate.num_args(); ++i)
args.emplace_back(_predicate.arg(i).to_string());
return args;
}

72
libsmtutil/Z3CHCInterface.h
View File

@ -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 <http://www.gnu.org/licenses/>.
*/
// SPDX-License-Identifier: GPL-3.0
/**
* Z3 specific Horn solver interface.
*/
#pragma once
#include <libsmtutil/CHCSolverInterface.h>
#include <libsmtutil/Z3Interface.h>
#include <tuple>
#include <vector>
namespace solidity::smtutil
{
class Z3CHCInterface: public CHCSolverInterface
{
public:
Z3CHCInterface(std::optional<unsigned> _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<CheckResult, Expression, CexGraph> 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<std::string> arguments(z3::expr const& _predicate);
// Used to handle variables.
std::unique_ptr<Z3Interface> m_z3Interface;
z3::context* m_context;
// Horn solver.
z3::fixedpoint m_solver;
std::tuple<unsigned, unsigned, unsigned, unsigned> m_version = std::tuple(0, 0, 0, 0);
};
}

479
libsmtutil/Z3Interface.cpp
View File

@ -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 <http://www.gnu.org/licenses/>.
*/
// SPDX-License-Identifier: GPL-3.0
#include <libsmtutil/Z3Interface.h>
#include <libsolutil/CommonData.h>
#include <libsolutil/CommonIO.h>
#include <libsolutil/Exceptions.h>
#ifdef HAVE_Z3_DLOPEN
#include <libsmtutil/Z3Loader.h>
#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<unsigned> _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<FunctionSort const&>(_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<CheckResult, std::vector<std::string>> Z3Interface::check(std::vector<Expression> const& _expressionsToEvaluate)
{
CheckResult result;
std::vector<std::string> 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<std::string> 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<SortSort>(_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<unsigned>(size), arguments[0]);
}
else if (n == "bv2int")
{
auto intSort = std::dynamic_pointer_cast<IntSort>(_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> sortSort = std::dynamic_pointer_cast<SortSort>(_expr.arguments[0].sort);
smtAssert(sortSort, "");
auto arraySort = std::dynamic_pointer_cast<ArraySort>(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<unsigned>(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<Expression> 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<SortSort>(fromZ3Sort(_expr.get_sort()));
return Expression::const_array(Expression(sortSort), arguments[0]);
}
else if (kind == Z3_OP_DT_CONSTRUCTOR)
{
auto sortSort = std::make_shared<SortSort>(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<BitVectorSort const&>(_sort).size);
case Kind::Array:
{
auto const& arraySort = dynamic_cast<ArraySort const&>(_sort);
return m_context.array_sort(z3Sort(*arraySort.domain), z3Sort(*arraySort.range));
}
case Kind::Tuple:
{
auto const& tupleSort = dynamic_cast<TupleSort const&>(_sort);
std::vector<char const*> 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<z3::sort> 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<unsigned>(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<SortPointer> 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<BitVectorSort>(_sort.bv_size());
if (_sort.is_array())
return std::make_shared<ArraySort>(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<std::string> memberNames;
std::vector<SortPointer> 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<TupleSort>(name, memberNames, memberSorts);
}
smtAssert(false, "");
}
std::vector<SortPointer> Z3Interface::fromZ3Sort(z3::sort_vector const& _sorts)
{
return applyMap(_sorts, [this](auto const& sort) { return fromZ3Sort(sort); });
}

75
libsmtutil/Z3Interface.h
View File

@ -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 <http://www.gnu.org/licenses/>.
*/
// SPDX-License-Identifier: GPL-3.0
#pragma once
#include <libsmtutil/SolverInterface.h>
#include <z3++.h>
namespace solidity::smtutil
{
class Z3Interface: public SolverInterface
{
public:
/// Noncopyable.
Z3Interface(Z3Interface const&) = delete;
Z3Interface& operator=(Z3Interface const&) = delete;
Z3Interface(std::optional<unsigned> _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<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
z3::expr toZ3Expr(Expression const& _expr);
smtutil::Expression fromZ3Expr(z3::expr const& _expr);
std::map<std::string, z3::expr> constants() const { return m_constants; }
std::map<std::string, z3::func_decl> 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<SortPointer> const& _sorts);
smtutil::SortPointer fromZ3Sort(z3::sort const& _sort);
std::vector<smtutil::SortPointer> fromZ3Sort(z3::sort_vector const& _sorts);
z3::context m_context;
z3::solver m_solver;
std::map<std::string, z3::expr> m_constants;
std::map<std::string, z3::func_decl> m_functions;
};
}

69
libsmtutil/Z3Loader.cpp
View File

@ -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 <http://www.gnu.org/licenses/>.
*/
// SPDX-License-Identifier: GPL-3.0
#include <libsmtutil/Z3Loader.h>
#include <libsmtutil/Exceptions.h>
#include <z3.h>
#include <z3_version.h>
#include <vector>
#ifndef _GNU_SOURCE
#define _GNU_SOURCE
#endif
#include <dlfcn.h>
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);
}

38
libsmtutil/Z3Loader.h
View File

@ -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 <http://www.gnu.org/licenses/>.
*/
// 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;
};
}

28
libsolidity/formal/BMC.cpp
View File

@ -20,16 +20,13 @@
#include <libsolidity/formal/SymbolicTypes.h>
#include <libsmtutil/SMTPortfolio.h>
#include <libsmtutil/SMTLib2Interface.h>
#include <liblangutil/CharStream.h>
#include <liblangutil/CharStreamProvider.h>
#include <utility>
#ifdef HAVE_Z3_DLOPEN
#include <z3_version.h>
#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<smtutil::SMTPortfolio>(
_smtlib2Responses, _smtCallback, _settings.solvers, _settings.timeout, _settings.printQuery
m_interface(std::make_unique<smtutil::SMTLib2Interface>(
_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<ASTNode const*, std::set<VerificationTargetType>, 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::map<ASTNode const*, std::set<V
// If this check is true, Z3 and CVC4 are not available
// and the query answers were not provided, since SMTPortfolio
// guarantees that SmtLib2Interface is the first solver, if enabled.
if (
!m_interface->unhandledQueries().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<smtutil::Expression> const& _e
{
if (m_settings.printQuery)
{
auto portfolio = dynamic_cast<smtutil::SMTPortfolio*>(m_interface.get());
std::string smtlibCode = portfolio->dumpQuery(_expressionsToEvaluate);
auto smtlibInterface = dynamic_cast<smtutil::SMTLib2Interface*>(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

66
libsolidity/formal/CHC.cpp
View File

@ -37,10 +37,6 @@
#include <libsolutil/Algorithms.h>
#include <libsolutil/StringUtils.h>
#ifdef HAVE_Z3_DLOPEN
#include <z3_version.h>
#endif
#include <boost/algorithm/string.hpp>
#include <range/v3/algorithm/for_each.hpp>
@ -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<Z3CHCInterface>(m_settings.timeout);
auto z3Interface = dynamic_cast<Z3CHCInterface const*>(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<CHCSmtLib2Interface>(m_smtlib2Responses, m_smtCallback, m_settings.solvers, m_settings.timeout);
if (!m_interface)
m_interface = std::make_unique<CHCSmtLib2Interface>(m_smtlib2Responses, m_smtCallback, m_settings.solvers, m_settings.timeout);
auto smtlib2Interface = dynamic_cast<CHCSmtLib2Interface*>(m_interface.get());
solAssert(smtlib2Interface, "");
smtlib2Interface->reset();
m_context.setSolver(smtlib2Interface->smtlib2Interface());
}
auto smtlib2Interface = dynamic_cast<CHCSmtLib2Interface*>(m_interface.get());
solAssert(smtlib2Interface, "");
smtlib2Interface->reset();
m_context.setSolver(smtlib2Interface->smtlib2Interface());
m_context.reset();
m_context.resetUniqueId();
@ -1821,32 +1798,7 @@ std::tuple<CheckResult, smtutil::Expression, CHCSolverInterface::CexGraph> 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<Z3CHCInterface*>(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:

13
libsolidity/formal/ModelChecker.cpp
View File

@ -162,15 +162,11 @@ std::vector<std::string> 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
);
}

10
libsolidity/formal/Predicate.cpp
View File

@ -499,7 +499,15 @@ std::optional<std::string> 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 ||

1
libsolidity/formal/SMTEncoder.cpp
View File

@ -27,7 +27,6 @@
#include <libyul/AST.h>
#include <libyul/optimiser/Semantics.h>
#include <libsmtutil/SMTPortfolio.h>
#include <libsmtutil/Helpers.h>
#include <liblangutil/CharStreamProvider.h>

19
libsolidity/formal/SymbolicTypes.cpp
View File

@ -23,12 +23,24 @@
#include <libsolidity/ast/TypeProvider.h>
#include <libsolidity/ast/Types.h>
#include <libsolutil/CommonData.h>
#include <algorithm>
#include <memory>
#include <vector>
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<TupleSort>(
@ -136,7 +151,9 @@ SortPointer smtSort(frontend::Type const& _type)
case Kind::Tuple:
{
std::vector<std::string> members;
auto const& tupleName = _type.toString(true);
auto tupleName = _type.toString(true);
sanitizeTypeName(tupleName);
std::vector<SortPointer> sorts;
if (auto const* tupleType = dynamic_cast<frontend::TupleType const*>(&_type))

21
libsolidity/interface/CompilerStack.cpp
View File

@ -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&)

110
libsolidity/interface/SMTSolverCommand.cpp
View File

@ -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<std::string> _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<std::string> 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<std::string> _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<std::string> 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<std::string> 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<std::string> 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 (...)
{

14
libsolidity/interface/SMTSolverCommand.h
View File

@ -19,8 +19,6 @@
#include <libsolidity/interface/ReadFile.h>
#include <boost/filesystem.hpp>
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;
};
}

3
libsolidity/interface/StandardCompiler.cpp
View File

@ -1094,9 +1094,6 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> 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();
}

2
libsolidity/interface/UniversalCallback.h
View File

@ -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.");
};

1
scripts/error_codes.py
View File

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

2
solc/CommandLineInterface.h
View File

@ -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<std::string> m_standardJsonInput;
std::unique_ptr<frontend::CompilerStack> m_compiler;

4
solc/CommandLineParser.cpp
View File

@ -853,7 +853,7 @@ General Information)").c_str(),
)
(
g_strModelCheckerSolvers.c_str(),
po::value<std::string>()->value_name("cvc4,eld,z3,smtlib2")->default_value("z3"),
po::value<std::string>()->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;
}

12
test/cmdlineTests/model_checker_divModSlacks_false_all/err
View File

@ -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.

12
test/cmdlineTests/model_checker_divModSlacks_false_chc/err
View File

@ -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.

2
test/cmdlineTests/model_checker_print_query_all/args
View File

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

40
test/cmdlineTests/model_checker_print_query_all/err
View File

@ -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.

2
test/cmdlineTests/model_checker_print_query_bmc/args
View File

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

4
test/cmdlineTests/model_checker_print_query_bmc/err
View File

@ -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.

2
test/cmdlineTests/model_checker_print_query_chc/args
View File

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

4
test/cmdlineTests/model_checker_print_query_chc/err
View File

@ -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.

1
test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_bmc/args
View File

@ -1 +0,0 @@
--model-checker-engine bmc --model-checker-print-query --model-checker-solvers z3

1
test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_bmc/err
View File

@ -1 +0,0 @@
Only SMTLib2 solver can be enabled to print queries

1
test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_bmc/exit
View File

@ -1 +0,0 @@
1

9
test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_bmc/input.sol
View File

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

1
test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_chc/args
View File

@ -1 +0,0 @@
--model-checker-engine chc --model-checker-print-query --model-checker-solvers z3

1
test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_chc/err
View File

@ -1 +0,0 @@
Only SMTLib2 solver can be enabled to print queries

1
test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_chc/exit
View File

@ -1 +0,0 @@
1

9
test/cmdlineTests/model_checker_print_query_no_smtlib2_solver_chc/input.sol
View File

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

1
test/cmdlineTests/model_checker_print_query_superflous_solver/args
View File

@ -1 +0,0 @@
--model-checker-engine bmc --model-checker-print-query --model-checker-solvers z3,smtlib2

1
test/cmdlineTests/model_checker_print_query_superflous_solver/err
View File

@ -1 +0,0 @@
Only SMTLib2 solver can be enabled to print queries

1
test/cmdlineTests/model_checker_print_query_superflous_solver/exit
View File

@ -1 +0,0 @@
1

9
test/cmdlineTests/model_checker_print_query_superflous_solver/input.sol
View File

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

1
test/cmdlineTests/model_checker_solvers_smtlib2/args
View File

@ -1 +0,0 @@
--model-checker-engine all --model-checker-solvers smtlib2

7
test/cmdlineTests/model_checker_solvers_smtlib2/err
View File

@ -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.

7
test/cmdlineTests/model_checker_solvers_smtlib2/input.sol
View File

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

1
test/cmdlineTests/model_checker_solvers_z3_smtlib2/args
View File

@ -1 +0,0 @@
--model-checker-engine all --model-checker-solvers z3,smtlib2

12
test/cmdlineTests/model_checker_solvers_z3_smtlib2/err
View File

@ -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);
| ^^^^^^^^^^^^^

7
test/cmdlineTests/model_checker_solvers_z3_smtlib2/input.sol
View File

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

40
test/cmdlineTests/standard_model_checker_divModSlacks_false_all/output.json
View File

@ -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",

40
test/cmdlineTests/standard_model_checker_divModSlacks_false_chc/output.json
View File

@ -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",

2
test/cmdlineTests/standard_model_checker_print_query_all/input.json
View File

@ -20,7 +20,7 @@
{
"engine": "all",
"printQuery": true,
"solvers": ["smtlib2"],
"solvers": ["z3"],
"timeout": 1000
}
}

266
test/cmdlineTests/standard_model_checker_print_query_all/output.json
View File

@ -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":

2
test/cmdlineTests/standard_model_checker_print_query_bmc/input.json
View File

@ -20,7 +20,7 @@
{
"engine": "bmc",
"printQuery": true,
"solvers": ["smtlib2"]
"solvers": ["z3"]
}
}
}

53
test/cmdlineTests/standard_model_checker_print_query_bmc/output.json
View File

@ -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":

2
test/cmdlineTests/standard_model_checker_print_query_chc/input.json
View File

@ -20,7 +20,7 @@
{
"engine": "chc",
"printQuery": true,
"solvers": ["smtlib2"],
"solvers": ["z3"],
"timeout": 1000
}
}

150
test/cmdlineTests/standard_model_checker_print_query_chc/output.json
View File

@ -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":

25
test/cmdlineTests/standard_model_checker_print_query_no_smtlib2_solver/input.json
View File

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

12
test/cmdlineTests/standard_model_checker_print_query_no_smtlib2_solver/output.json
View File

@ -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"
}
]
}

26
test/cmdlineTests/standard_model_checker_print_query_superflous_solver/input.json
View File

@ -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"]
}
}
}

12
test/cmdlineTests/standard_model_checker_print_query_superflous_solver/output.json
View File

@ -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"
}
]
}

18
test/cmdlineTests/standard_model_checker_solvers_smtlib2/input.json
View File

@ -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"]
}
}
}

208
test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json
View File

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

18
test/cmdlineTests/standard_model_checker_solvers_z3_smtlib2/input.json
View File

@ -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"]
}
}
}

46
test/cmdlineTests/standard_model_checker_solvers_z3_smtlib2/output.json
View File

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

5
test/libsolidity/SMTCheckerTest.cpp
View File

@ -133,6 +133,11 @@ void SMTCheckerTest::setupCompiler()
compiler().setModelCheckerSettings(m_modelCheckerSettings);
}
std::unique_ptr<CompilerStack> SMTCheckerTest::createStack() const
{
return std::make_unique<CompilerStack>(m_smtCommand.solver());
}
void SMTCheckerTest::filterObtainedErrors()
{
SyntaxTest::filterObtainedErrors();

6
test/libsolidity/SMTCheckerTest.h
View File

@ -23,6 +23,7 @@
#include <libsmtutil/SolverInterface.h>
#include <libsolidity/formal/ModelChecker.h>
#include <libsolidity/interface/SMTSolverCommand.h>
#include <string>
@ -39,6 +40,9 @@ public:
SMTCheckerTest(std::string const& _filename);
void setupCompiler() override;
std::unique_ptr<CompilerStack> 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<SyntaxTestError> m_unfilteredErrorList;
mutable SMTSolverCommand m_smtCommand;
};
}

4
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol
View File

@ -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.

4
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol
View File

@ -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.

8
test/libsolidity/smtCheckerTests/blockchain_state/balance_spend_2.sol
View File

@ -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.

8
test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol
View File

@ -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.

5
test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol
View File

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

2
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_trusted.sol
View File

@ -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.

4
test/libsolidity/smtCheckerTests/external_calls/external_safe.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/functions/getters/array_2.sol
View File

@ -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.

12
test/libsolidity/smtCheckerTests/imports/duplicated_errors_1.sol
View File

@ -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.

11
test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol
View File

@ -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.

4
test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol
View File

@ -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.

8
test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol
View File

@ -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.

3
test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol
View File

@ -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.

53
test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_storage_safe.sol
View File

@ -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.

3
test/libsolidity/smtCheckerTests/types/struct_array_branches_2d.sol
View File

@ -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.

16
test/libsolidity/smtCheckerTests/types/type_minmax.sol
View File

@ -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.

6
test/solc/CommandLineParser.cpp
View File

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