Skip to content

Commit

Permalink
Merge pull request #15032 from ethereum/smt-eld-invariants
Browse files Browse the repository at this point in the history 
SMTChecker: Parse invariants from SMT-LIB response
  • Loading branch information
@blishko
blishko committed Apr 30, 2024
2 parents d74b8af + 048ce0b commit 5afa25e
Show file tree
Hide file tree
Showing 13 changed files with 536 additions and 32 deletions.
304 changes: 290 additions & 14 deletions libsmtutil/CHCSmtLib2Interface.cpp
View file
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;
{
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
{
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);
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
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;
};

}

0 comments on commit 5afa25e

Please sign in to comment.