diff --git a/libsmtutil/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp index 7e643abac809..73cf8e12f9fb 100644 --- a/libsmtutil/CHCSmtLib2Interface.cpp +++ b/libsmtutil/CHCSmtLib2Interface.cpp @@ -18,7 +18,11 @@ #include +#include + #include +#include +#include #include #include @@ -29,6 +33,7 @@ #include #include #include +#include #include using namespace solidity; @@ -96,7 +101,10 @@ std::tuple CHCSmtLib2Inte CheckResult result; // TODO proper parsing if (boost::starts_with(response, "sat")) - result = CheckResult::UNSATISFIABLE; + { + auto maybeInvariants = invariantsFromSolverResponse(response); + return {CheckResult::UNSATISFIABLE, maybeInvariants.has_value() ? maybeInvariants.value() : Expression(true), {}}; + } else if (boost::starts_with(response, "unsat")) result = CheckResult::SATISFIABLE; else if (boost::starts_with(response, "unknown")) @@ -217,3 +225,289 @@ std::string CHCSmtLib2Interface::createHeaderAndDeclarations() { std::string CHCSmtLib2Interface::createQueryAssertion(std::string name) { return "(assert\n(forall " + forall() + "\n" + "(=> " + name + " false)))"; } + +class SMTLibTranslationContext + { + CHCSmtLib2Interface const& m_chcInterface; + std::map knownVariables; + + bool isNumber(std::string const& _expr) + { + for (char c: _expr) + if (!isDigit(c) && c != '.') + return false; + return true; + } + + + public: + explicit SMTLibTranslationContext(CHCSmtLib2Interface const& _chcInterface) : m_chcInterface(_chcInterface) + { + // fill user defined sorts and constructors + auto const& userSorts = m_chcInterface.smtlib2Interface()->userSorts(); + for (auto const& declaration: userSorts | ranges::views::values) + { + std::stringstream ss(declaration); + SMTLib2Parser parser(ss); + auto expr = parser.parseExpression(); + solAssert(parser.isEOF()); + solAssert(!isAtom(expr)); + auto const& args = asSubExpressions(expr); + solAssert(args.size() == 3); + solAssert(isAtom(args[0]) && asAtom(args[0]) == "declare-datatypes"); + // args[1] is the name of the type + // args[2] is the constructor with the members + solAssert(!isAtom(args[2]) && asSubExpressions(args[2]).size() == 1 && !isAtom(asSubExpressions(args[2])[0])); + auto const& constructors = asSubExpressions(asSubExpressions(args[2])[0]); + solAssert(constructors.size() == 1); + auto const& constructor = constructors[0]; + // constructor is a list: name + members + solAssert(!isAtom(constructor)); + auto const& constructorArgs = asSubExpressions(constructor); + for (unsigned i = 1u; i < constructorArgs.size(); ++i) + { + auto const& carg = constructorArgs[i]; + solAssert(!isAtom(carg) && asSubExpressions(carg).size() == 2); + auto const& nameSortPair = asSubExpressions(carg); + solAssert(isAtom(nameSortPair[0])); + knownVariables.insert({asAtom(nameSortPair[0]), toSort(nameSortPair[1])}); + } + } + } + + void addVariableDeclaration(std::string name, SortPointer sort) + { + solAssert(knownVariables.find(name) == knownVariables.end()); + knownVariables.insert({std::move(name), std::move(sort)}); + } + + std::optional lookupKnownTupleSort(std::string const& name) { + auto const& userSorts = m_chcInterface.sortNames(); + auto findByName = [&userSorts](std::string const& name) { + auto it = userSorts.begin(); + for (; it != userSorts.end(); ++it) { + if (it->second == name) + break; + } + return it; + }; + std::string quotedName = "|" + name + "|"; + + auto it = findByName(quotedName); + if (it != userSorts.end() && it->first->kind == Kind::Tuple) + { + auto tupleSort = std::dynamic_pointer_cast(it->first); + smtAssert(tupleSort); + return tupleSort; + } + return {}; + } + + SortPointer toSort(SMTLib2Expression const& expr) + { + if (isAtom(expr)) + { + auto const& name = asAtom(expr); + if (name == "Int") + return SortProvider::sintSort; + if (name == "Bool") + return SortProvider::boolSort; + auto tupleSort = lookupKnownTupleSort(name); + if (tupleSort) + return tupleSort.value(); + } else { + auto const& args = asSubExpressions(expr); + if (asAtom(args[0]) == "Array") + { + smtAssert(args.size() == 3); + auto domainSort = toSort(args[1]); + auto codomainSort = toSort(args[2]); + return std::make_shared(std::move(domainSort), std::move(codomainSort)); + } + if (args.size() == 3 && isAtom(args[0]) && asAtom(args[0]) == "_" && isAtom(args[1]) && asAtom(args[1]) == "int2bv") + { + smtAssert(isAtom(args[2])); + return std::make_shared(std::stoul(asAtom(args[2]))); + } + } + smtAssert(false, "Unknown sort encountered"); + } + + smtutil::Expression parseQuantifier( + std::string const& quantifierName, + std::vector const& varList, + SMTLib2Expression const& coreExpression + ) + { + std::vector> boundVariables; + for (auto const& sortedVar: varList) + { + solAssert(!isAtom(sortedVar)); + auto varSortPair = asSubExpressions(sortedVar); + solAssert(varSortPair.size() == 2); + solAssert(isAtom(varSortPair[0])); + boundVariables.emplace_back(asAtom(varSortPair[0]), toSort(varSortPair[1])); + } + for (auto const& [var, sort] : boundVariables) + { + solAssert(knownVariables.find(var) == knownVariables.end()); // TODO: deal with shadowing? + knownVariables.insert({var, sort}); + } + auto core = toSMTUtilExpression(coreExpression); + for (auto const& [var, sort] : boundVariables) + { + solAssert(knownVariables.find(var) != knownVariables.end()); + knownVariables.erase(var); + } + return Expression(quantifierName, {core}, SortProvider::boolSort); // TODO: what about the bound variables? + + } + + smtutil::Expression toSMTUtilExpression(SMTLib2Expression const& _expr) + { + return std::visit(GenericVisitor{ + [&](std::string const& _atom) { + if (_atom == "true" || _atom == "false") + return smtutil::Expression(_atom == "true"); + else if (isNumber(_atom)) + return smtutil::Expression(_atom, {}, SortProvider::sintSort); + else if (knownVariables.find(_atom) != knownVariables.end()) + return smtutil::Expression(_atom, {}, knownVariables.at(_atom)); + else // assume this is a predicate, so has sort bool; TODO: Context should be aware of the predicates! + return smtutil::Expression(_atom, {}, SortProvider::boolSort); + }, + [&](std::vector const& _subExpr) { + SortPointer sort; + std::vector arguments; + if (isAtom(_subExpr.front())) + { + std::string const& op = asAtom(_subExpr.front()); + if (op == "!") + { + // named term, we ignore the name + solAssert(_subExpr.size() > 2); + return toSMTUtilExpression(_subExpr[1]); + } + if (op == "exists" || op == "forall") + { + solAssert(_subExpr.size() == 3); + solAssert(!isAtom(_subExpr[1])); + return parseQuantifier(op, asSubExpressions(_subExpr[1]), _subExpr[2]); + } + for (size_t i = 1; i < _subExpr.size(); i++) + arguments.emplace_back(toSMTUtilExpression(_subExpr[i])); + if (auto tupleSort = lookupKnownTupleSort(op); tupleSort) + { + auto sortSort = std::make_shared(tupleSort.value()); + return Expression::tuple_constructor(Expression(sortSort), arguments); + } + if (knownVariables.find(op) != knownVariables.end()) + { + return smtutil::Expression(op, std::move(arguments), knownVariables.at(op)); + } + else { + std::set boolOperators{"and", "or", "not", "=", "<", ">", "<=", ">=", + "=>"}; + sort = contains(boolOperators, op) ? SortProvider::boolSort : arguments.back().sort; + return smtutil::Expression(op, std::move(arguments), std::move(sort)); + } + smtAssert(false, "Unhandled case in expression conversion"); + } else { + // check for const array + if (_subExpr.size() == 2 and !isAtom(_subExpr[0])) + { + auto const& typeArgs = asSubExpressions(_subExpr.front()); + if (typeArgs.size() == 3 && typeArgs[0].toString() == "as" && typeArgs[1].toString() == "const") + { + auto arraySort = toSort(typeArgs[2]); + auto sortSort = std::make_shared(arraySort); + return smtutil::Expression::const_array(Expression(sortSort), toSMTUtilExpression(_subExpr[1])); + } + if (typeArgs.size() == 3 && typeArgs[0].toString() == "_" && typeArgs[1].toString() == "int2bv") + { + auto bvSort = std::dynamic_pointer_cast(toSort(_subExpr[0])); + solAssert(bvSort); + return smtutil::Expression::int2bv(toSMTUtilExpression(_subExpr[1]), bvSort->size); + } + if (typeArgs.size() == 4 && typeArgs[0].toString() == "_") + { + if (typeArgs[1].toString() == "extract") + { + return smtutil::Expression( + "extract", + {toSMTUtilExpression(typeArgs[2]), toSMTUtilExpression(typeArgs[3])}, + SortProvider::bitVectorSort // TODO: Compute bit size properly? + ); + } + } + } + + smtAssert(false, "Unhandled case in expression conversion"); + } + } + }, _expr.data); + } + }; + + +#define precondition(CONDITION) if(!(CONDITION)) return {} +std::optional CHCSmtLib2Interface::invariantsFromSolverResponse(std::string const& _response) const +{ + std::stringstream ss(_response); + std::string answer; + ss >> answer; + precondition(answer == "sat"); + SMTLib2Parser parser(ss); + precondition(!parser.isEOF()); // There has to be a model + std::vector parsedOutput; + try + { + while(!parser.isEOF()) + parsedOutput.push_back(parser.parseExpression()); + } + catch(SMTLib2Parser::ParsingException&) + { + return {}; + } + precondition(parser.isEOF()); + precondition(!parsedOutput.empty()); + auto& commands = parsedOutput.size() == 1 ? asSubExpressions(parsedOutput[0]) : parsedOutput; + std::vector definitions; + for (auto& command: commands) + { + auto& args = asSubExpressions(command); + precondition(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 + precondition(isAtom(args[0]) && asAtom(args[0]) == "define-fun"); + precondition(isAtom(args[1])); + precondition(!isAtom(args[2])); + precondition(isAtom(args[3]) && asAtom(args[3]) == "Bool"); + auto& interpretation = args[4]; +// inlineLetExpressions(interpretation); + SMTLibTranslationContext context(*this); + auto const& formalArguments = asSubExpressions(args[2]); + std::vector predicateArgs; + for (auto const& formalArgument: formalArguments) + { + precondition(!isAtom(formalArgument)); + auto const& nameSortPair = asSubExpressions(formalArgument); + precondition(nameSortPair.size() == 2); + precondition(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)); +} +#undef precondition diff --git a/libsmtutil/CHCSmtLib2Interface.h b/libsmtutil/CHCSmtLib2Interface.h index b133c485e095..f7f656fd0b49 100644 --- a/libsmtutil/CHCSmtLib2Interface.h +++ b/libsmtutil/CHCSmtLib2Interface.h @@ -76,6 +76,9 @@ class CHCSmtLib2Interface: public CHCSolverInterface /// Communicates with the solver via the callback. Throws SMTSolverError on error. std::string querySolver(std::string const& _input); + /// Translates CHC solver response with a model to our representation of invariants. Returns None on error. + std::optional invariantsFromSolverResponse(std::string const& response) const; + /// Used to access toSmtLibSort, SExpr, and handle variables. std::unique_ptr m_smtlib2;