Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

SMTChecker: Parse invariants from SMT-LIB response #15032

Merged
merged 5 commits into from Apr 30, 2024
Merged

SMTChecker: Parse invariants from SMT-LIB response #15032

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
7fb6222
SMTChecker: First version of SMTLIB2 parser
blishko Mar 13, 2024
eb11819
SMTChecker: Instruct Eldarica to produce invariants if requested
blishko Mar 13, 2024
1fcaec5
SMTChecker: Remember sorts already in SMTLibInterface
blishko Apr 16, 2024
384f005
SMTChecker: Support retrieving invariants from Eldarica
blishko Apr 16, 2024
048ce0b
SMTChecker: Add command-line test for invariants from Eldarica
blishko Apr 16, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
304 changes: 290 additions & 14 deletions libsmtutil/CHCSmtLib2Interface.cpp
View file
Open in desktop
Expand Up @@ -18,11 +18,17 @@

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

#include <range/v3/algorithm/find_if.hpp>
#include <range/v3/algorithm/all_of.hpp>
#include <range/v3/view.hpp>

#include <array>
Expand Down Expand Up @@ -56,7 +62,7 @@ void CHCSmtLib2Interface::reset()
m_accumulatedOutput.clear();
m_variables.clear();
m_unhandledQueries.clear();
m_sortNames.clear();
m_smtlib2->reset();
}

void CHCSmtLib2Interface::registerRelation(Expression const& _expr)
Expand Down Expand Up @@ -96,7 +102,10 @@ std::tuple<CheckResult, Expression, CHCSolverInterface::CexGraph> CHCSmtLib2Inte
CheckResult result;
// TODO proper parsing
if (boost::starts_with(response, "sat"))
result = CheckResult::UNSATISFIABLE;
{
pgebal marked this conversation as resolved.
Show resolved Hide resolved
auto maybeInvariants = invariantsFromSolverResponse(response);
return {CheckResult::UNSATISFIABLE, maybeInvariants.value_or(Expression(true)), {}};
}
else if (boost::starts_with(response, "unsat"))
result = CheckResult::SATISFIABLE;
else if (boost::starts_with(response, "unknown"))
Expand All @@ -115,24 +124,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()
Expand All @@ -142,7 +145,7 @@ std::string CHCSmtLib2Interface::forall()
{
solAssert(sort, "");
if (sort->kind != Kind::Function)
vars += " (" + name + " " + toSmtLibSort(*sort) + ")";
vars += " (" + name + " " + toSmtLibSort(sort) + ")";
}
vars += ")";
return vars;
Expand All @@ -158,7 +161,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 |" +
Expand Down Expand Up @@ -223,3 +226,276 @@ std::string CHCSmtLib2Interface::createHeaderAndDeclarations() {
std::string CHCSmtLib2Interface::createQueryAssertion(std::string name) {
return "(assert\n(forall " + forall() + "\n" + "(=> " + name + " false)))";
}

class SMTLibTranslationContext
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Uh, everything in the class has an extra indent by the way.

{
CHCSmtLib2Interface const& m_chcInterface;
std::map<std::string, SortPointer> m_knownVariables;

static bool isNumber(std::string const& _expr)
{
return ranges::all_of(_expr, [](char c) { return isDigit(c) || c == '.'; });
}


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();
smtAssert(parser.isEOF());
smtAssert(!isAtom(expr));
auto const& args = asSubExpressions(expr);
smtAssert(args.size() == 3);
smtAssert(isAtom(args[0]) && asAtom(args[0]) == "declare-datatypes");
// args[1] is the name of the type
// args[2] is the constructor with the members
smtAssert(!isAtom(args[2]) && asSubExpressions(args[2]).size() == 1 && !isAtom(asSubExpressions(args[2])[0]));
auto const& constructors = asSubExpressions(asSubExpressions(args[2])[0]);
smtAssert(constructors.size() == 1);
auto const& constructor = constructors[0];
// constructor is a list: name + members
smtAssert(!isAtom(constructor));
auto const& constructorArgs = asSubExpressions(constructor);
for (unsigned i = 1u; i < constructorArgs.size(); ++i)
{
auto const& carg = constructorArgs[i];
smtAssert(!isAtom(carg) && asSubExpressions(carg).size() == 2);
auto const& nameSortPair = asSubExpressions(carg);
m_knownVariables.emplace(asAtom(nameSortPair[0]), toSort(nameSortPair[1]));
}
}
}

void addVariableDeclaration(std::string name, SortPointer sort)
{
smtAssert(m_knownVariables.find(name) == m_knownVariables.end());
m_knownVariables.emplace(std::move(name), std::move(sort));
}

std::optional<SortPointer> lookupKnownTupleSort(std::string const& name) {
auto const& userSorts = m_chcInterface.sortNames();
std::string quotedName = "|" + name + "|";
auto it = ranges::find_if(userSorts, [&](auto const& entry) { return entry.second == 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")
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)
{
smtAssert(!isAtom(sortedVar));
auto varSortPair = asSubExpressions(sortedVar);
smtAssert(varSortPair.size() == 2);
boundVariables.emplace_back(asAtom(varSortPair[0]), toSort(varSortPair[1]));
}
for (auto const& [var, sort] : boundVariables)
{
smtAssert(m_knownVariables.find(var) == m_knownVariables.end()); // TODO: deal with shadowing?
m_knownVariables.emplace(var, sort);
}
auto core = toSMTUtilExpression(coreExpression);
for (auto const& [var, sort] : boundVariables)
{
smtAssert(m_knownVariables.find(var) != m_knownVariables.end());
m_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 (auto it = m_knownVariables.find(_atom); it != m_knownVariables.end())
return smtutil::Expression(_atom, {}, it->second);
else // assume this is a predicate with sort bool; TODO: Context should be aware of 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
smtAssert(_subExpr.size() > 2);
return toSMTUtilExpression(_subExpr[1]);
}
if (op == "exists" || op == "forall")
{
smtAssert(_subExpr.size() == 3);
smtAssert(!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 (auto it = m_knownVariables.find(op); it != m_knownVariables.end())
return smtutil::Expression(op, std::move(arguments), it->second);
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]));
smtAssert(bvSort);
return smtutil::Expression::int2bv(toSMTUtilExpression(_subExpr[1]), bvSort->size);
}
if (typeArgs.size() == 4 && typeArgs[0].toString() == "_"
&& 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 {};
}
smtAssert(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);
pgebal marked this conversation as resolved.
Show resolved Hide resolved
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
9 changes: 6 additions & 3 deletions libsmtutil/CHCSmtLib2Interface.h
View file
Open in desktop
Expand Up @@ -57,8 +57,10 @@ class CHCSmtLib2Interface: public CHCSolverInterface

SMTLib2Interface* smtlib2Interface() const { return m_smtlib2.get(); }

auto const& sortNames() const { return m_smtlib2->sortNames(); }

private:
std::string toSmtLibSort(Sort const& _sort);
std::string toSmtLibSort(SortPointer _sort);
std::string toSmtLibSort(std::vector<SortPointer> const& _sort);

void writeHeader();
Expand All @@ -74,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 All @@ -85,8 +90,6 @@ class CHCSmtLib2Interface: public CHCSolverInterface

frontend::ReadCallback::Callback m_smtCallback;
SMTSolverChoice m_enabledSolvers;

std::map<Sort const*, std::string> m_sortNames;
};

}