From 921240adc53fe5d824cef78d57e9ca63b1a6ae66 Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Tue, 16 Apr 2024 13:52:22 +0200 Subject: [PATCH] SMTChecker: Support retrieving invariants from Eldarica We add support for parsing CHC solver response containing a model, i.e., invariants. We utilise our SMT parser to build S-expression representation which we then interpret using the context we remembered while building the query. We have to rememeber all predicates declared to the solver, and, consequently, all sorts we have declared to the solver. --- libsmtutil/CHCSmtLib2Interface.cpp | 296 ++++++++++++++++++++++++++++- libsmtutil/CHCSmtLib2Interface.h | 3 + 2 files changed, 298 insertions(+), 1 deletion(-) 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;