From 82a3071b854a7051899e2fc09cc7aa29439f4e70 Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Mon, 19 Aug 2024 21:59:09 +0200 Subject: [PATCH] SMTChecker: Introduce first draft of Z3CHCSmtlib2Interface This commit introduces the interface class without actually using it. The actual switch will be done later, after all things are set up. --- libsmtutil/CHCSmtLib2Interface.cpp | 4 +- libsolidity/formal/Z3CHCSmtLib2Interface.cpp | 222 +++++++++++++++++++ libsolidity/formal/Z3CHCSmtLib2Interface.h | 50 +++++ 3 files changed, 275 insertions(+), 1 deletion(-) create mode 100644 libsolidity/formal/Z3CHCSmtLib2Interface.cpp create mode 100644 libsolidity/formal/Z3CHCSmtLib2Interface.h diff --git a/libsmtutil/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp index 6db1c6e876d0..6e535f09930f 100644 --- a/libsmtutil/CHCSmtLib2Interface.cpp +++ b/libsmtutil/CHCSmtLib2Interface.cpp @@ -96,7 +96,9 @@ std::tuple CHCSmtLib2Inte std::string response = querySolver(query); CheckResult result; - // TODO proper parsing + // NOTE: Our internal semantics is UNSAT -> SAFE and SAT -> UNSAFE, which corresponds to usual SMT-based model checking + // However, with CHC solvers, the meaning is flipped, UNSAT -> UNSAFE and SAT -> SAFE. + // So we have to flip the answer. if (boost::starts_with(response, "sat")) { auto maybeInvariants = invariantsFromSolverResponse(response); diff --git a/libsolidity/formal/Z3CHCSmtLib2Interface.cpp b/libsolidity/formal/Z3CHCSmtLib2Interface.cpp new file mode 100644 index 000000000000..cd06a9d3313a --- /dev/null +++ b/libsolidity/formal/Z3CHCSmtLib2Interface.cpp @@ -0,0 +1,222 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see . +*/ +// SPDX-License-Identifier: GPL-3.0 + +#include + +#include + +#include + +#include + +#include + +using namespace solidity::frontend::smt; +using namespace solidity::smtutil; + +Z3CHCSmtLib2Interface::Z3CHCSmtLib2Interface( + frontend::ReadCallback::Callback _smtCallback, + std::optional _queryTimeout, + bool _computeInvariants +): CHCSmtLib2Interface({}, std::move(_smtCallback), _queryTimeout), m_computeInvariants(_computeInvariants) +{ +} + +void Z3CHCSmtLib2Interface::setupSmtCallback(bool _enablePreprocessing) +{ + if (auto* universalCallback = m_smtCallback.target()) + universalCallback->smtCommand().setZ3(m_queryTimeout, _enablePreprocessing, m_computeInvariants); +} + +std::tuple Z3CHCSmtLib2Interface::query(smtutil::Expression const& _block) +{ + setupSmtCallback(true); + std::string query = dumpQuery(_block); + std::string response = querySolver(query); + // NOTE: Our internal semantics is UNSAT -> SAFE and SAT -> UNSAFE, which corresponds to usual SMT-based model checking + // However, with CHC solvers, the meaning is flipped, UNSAT -> UNSAFE and SAT -> SAFE. + // So we have to flip the answer. + if (boost::starts_with(response, "unsat")) + { + // Repeat the query with preprocessing disabled, to get the full proof + setupSmtCallback(false); + query = "(set-option :produce-proofs true)" + query + "\n(get-proof)"; + response = querySolver(query); + setupSmtCallback(true); + if (!boost::starts_with(response, "unsat")) + return {CheckResult::SATISFIABLE, Expression(true), {}}; + return {CheckResult::SATISFIABLE, Expression(true), graphFromZ3Answer(response)}; + } + + CheckResult result; + if (boost::starts_with(response, "sat")) + { + auto maybeInvariants = invariantsFromSolverResponse(response); + return {CheckResult::UNSATISFIABLE, maybeInvariants.value_or(Expression(true)), {}}; + } + else if (boost::starts_with(response, "unknown")) + result = CheckResult::UNKNOWN; + else + result = CheckResult::ERROR; + + return {result, Expression(true), {}}; +} + + +CHCSolverInterface::CexGraph Z3CHCSmtLib2Interface::graphFromZ3Answer(std::string const& _proof) const +{ + std::stringstream ss(_proof); + std::string answer; + ss >> answer; + smtAssert(answer == "unsat"); + + SMTLib2Parser parser(ss); + if (parser.isEOF()) // No proof from Z3 + return {}; + // For some reason Z3 outputs everything as a single s-expression + SMTLib2Expression parsedOutput; + try + { + parsedOutput = parser.parseExpression(); + } + catch (SMTLib2Parser::ParsingException&) + { + return {}; + } + solAssert(parser.isEOF()); + solAssert(!isAtom(parsedOutput)); + auto& commands = asSubExpressions(parsedOutput); + ScopedParser expressionParser(m_context); + for (auto& command: commands) + { + if (isAtom(command)) + continue; + + auto const& args = asSubExpressions(command); + solAssert(args.size() > 0); + auto const& head = args[0]; + if (!isAtom(head)) + continue; + + // Z3 can introduce new helper predicates to be used in the proof + // e.g., "(declare-fun query!0 (Bool Bool Bool Int Int Bool Bool Bool Bool Bool Bool Bool Int) Bool)" + if (asAtom(head) == "declare-fun") + { + solAssert(args.size() == 4); + auto const& name = args[1]; + auto const& domainSorts = args[2]; + auto const& codomainSort = args[3]; + solAssert(isAtom(name)); + solAssert(!isAtom(domainSorts)); + expressionParser.addVariableDeclaration(asAtom(name), expressionParser.toSort(codomainSort)); + } + // The subexpression starting with "proof" contains the whole proof, which we need to transform to our internal + // representation + else if (asAtom(head) == "proof") + { + inlineLetExpressions(command); + return graphFromSMTLib2Expression(command, expressionParser); + } + } + return {}; +} + +CHCSolverInterface::CexGraph Z3CHCSmtLib2Interface::graphFromSMTLib2Expression( + SMTLib2Expression const& _proof, + ScopedParser& _context +) +{ + auto fact = [](SMTLib2Expression const& _node) -> SMTLib2Expression const& { + if (isAtom(_node)) + return _node; + smtAssert(!asSubExpressions(_node).empty()); + return asSubExpressions(_node).back(); + }; + smtAssert(!isAtom(_proof)); + auto const& proofArgs = asSubExpressions(_proof); + smtAssert(proofArgs.size() == 2); + smtAssert(isAtom(proofArgs.at(0)) && asAtom(proofArgs.at(0)) == "proof"); + auto const& proofNode = proofArgs.at(1); + auto const& derivedFact = fact(proofNode); + if (isAtom(proofNode) || !isAtom(derivedFact) || asAtom(derivedFact) != "false") + return {}; + + CHCSolverInterface::CexGraph graph; + + std::stack proofStack; + proofStack.push(&asSubExpressions(proofNode).at(1)); + + std::map visitedIds; + unsigned nextId = 0; + + auto const* root = proofStack.top(); + auto const& derivedRootFact = fact(*root); + visitedIds.emplace(root, nextId++); + graph.nodes.emplace(visitedIds.at(root), _context.toSMTUtilExpression(derivedRootFact)); + + auto isHyperRes = [](SMTLib2Expression const& expr) { + if (isAtom(expr)) return false; + auto const& subExprs = asSubExpressions(expr); + smtAssert(!subExprs.empty()); + auto const& op = subExprs.at(0); + if (isAtom(op)) return false; + auto const& opExprs = asSubExpressions(op); + if (opExprs.size() < 2) return false; + auto const& ruleName = opExprs.at(1); + return isAtom(ruleName) && asAtom(ruleName) == "hyper-res"; + }; + + while (!proofStack.empty()) + { + auto const* currentNode = proofStack.top(); + smtAssert(visitedIds.find(currentNode) != visitedIds.end()); + auto id = visitedIds.at(currentNode); + smtAssert(graph.nodes.count(id)); + proofStack.pop(); + + if (isHyperRes(*currentNode)) + { + auto const& args = asSubExpressions(*currentNode); + smtAssert(args.size() > 1); + // args[0] is the name of the rule + // args[1] is the clause used + // last argument is the derived fact + // the arguments in the middle are the facts where we need to recurse + for (unsigned i = 2; i < args.size() - 1; ++i) + { + auto const* child = &args[i]; + if (!visitedIds.count(child)) + { + visitedIds.emplace(child, nextId++); + proofStack.push(child); + } + + auto childId = visitedIds.at(child); + if (!graph.nodes.count(childId)) + { + graph.nodes.emplace(childId, _context.toSMTUtilExpression(fact(*child))); + graph.edges[childId] = {}; + } + + graph.edges[id].push_back(childId); + } + } + } + return graph; +} + diff --git a/libsolidity/formal/Z3CHCSmtLib2Interface.h b/libsolidity/formal/Z3CHCSmtLib2Interface.h new file mode 100644 index 000000000000..39456cde0c1b --- /dev/null +++ b/libsolidity/formal/Z3CHCSmtLib2Interface.h @@ -0,0 +1,50 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see . +*/ +// SPDX-License-Identifier: GPL-3.0 + +#pragma once + +#include + +namespace solidity::frontend::smt +{ + +class Z3CHCSmtLib2Interface: public smtutil::CHCSmtLib2Interface +{ +public: + Z3CHCSmtLib2Interface( + frontend::ReadCallback::Callback _smtCallback, + std::optional _queryTimeout, + bool _computeInvariants + ); + +private: + void setupSmtCallback(bool _disablePreprocessing); + + std::tuple query(smtutil::Expression const& _expr) override; + + CHCSolverInterface::CexGraph graphFromZ3Answer(std::string const& _proof) const; + + static CHCSolverInterface::CexGraph graphFromSMTLib2Expression( + smtutil::SMTLib2Expression const& _proof, + ScopedParser& _context + ); + + bool m_computeInvariants; +}; + +}