Skip to content

Commit

Permalink
SMTChecker: Support retrieving invariants from Eldarica
Browse files Browse the repository at this point in the history 
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.
  • Loading branch information
@blishko
blishko committed Apr 16, 2024
1 parent 0eef360 commit 921240a
Show file tree
Hide file tree
Showing 2 changed files with 298 additions and 1 deletion.
296 changes: 295 additions & 1 deletion libsmtutil/CHCSmtLib2Interface.cpp
View file
Expand Up @@ -18,7 +18,11 @@

#include <libsmtutil/CHCSmtLib2Interface.h>

#include <libsmtutil/SMTLib2Parser.h>

#include <libsolutil/Keccak256.h>
#include <libsolutil/StringUtils.h>
#include <libsolutil/Visitor.h>

#include <boost/algorithm/string/join.hpp>
#include <boost/algorithm/string/predicate.hpp>
Expand All @@ -29,6 +33,7 @@
#include <fstream>
#include <iostream>
#include <memory>
#include <range/v3/algorithm/find_if.hpp>
#include <stdexcept>

using namespace solidity;
Expand Down Expand Up @@ -96,7 +101,10 @@ std::tuple<CheckResult, Expression, CHCSolverInterface::CexGraph> 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"))
Expand Down Expand Up @@ -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<std::string, SortPointer> 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<SortPointer> 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<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")
{
smtAssert(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")
{
smtAssert(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);
}
};


#define precondition(CONDITION) if(!(CONDITION)) return {}
std::optional<smtutil::Expression> 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<SMTLib2Expression> 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<Expression> 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<Expression> 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
3 changes: 3 additions & 0 deletions libsmtutil/CHCSmtLib2Interface.h
View file
Expand Up @@ -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<smtutil::Expression> invariantsFromSolverResponse(std::string const& response) const;

/// Used to access toSmtLibSort, SExpr, and handle variables.
std::unique_ptr<SMTLib2Interface> m_smtlib2;

Expand Down

0 comments on commit 921240a

Please sign in to comment.