1 /* 2 This file is part of solidity. 3 4 solidity is free software: you can redistribute it and/or modify 5 it under the terms of the GNU General Public License as published by 6 the Free Software Foundation, either version 3 of the License, or 7 (at your option) any later version. 8 9 solidity is distributed in the hope that it will be useful, 10 but WITHOUT ANY WARRANTY; without even the implied warranty of 11 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 12 GNU General Public License for more details. 13 14 You should have received a copy of the GNU General Public License 15 along with solidity. If not, see <http://www.gnu.org/licenses/>. 16 */ 17 // SPDX-License-Identifier: GPL-3.0 18 19 /** 20 * Interface for solving Horn systems via smtlib2. 21 */ 22 23 #pragma once 24 25 #include <libsmtutil/CHCSolverInterface.h> 26 27 #include <libsmtutil/SMTLib2Interface.h> 28 29 namespace solidity::smtutil 30 { 31 32 class CHCSmtLib2Interface: public CHCSolverInterface 33 { 34 public: 35 explicit CHCSmtLib2Interface( 36 std::map<util::h256, std::string> const& _queryResponses = {}, 37 frontend::ReadCallback::Callback _smtCallback = {}, 38 std::optional<unsigned> _queryTimeout = {} 39 ); 40 41 void reset(); 42 43 void registerRelation(Expression const& _expr) override; 44 45 void addRule(Expression const& _expr, std::string const& _name) override; 46 47 /// Takes a function application _expr and checks for reachability. 48 /// @returns solving result, an invariant, and counterexample graph, if possible. 49 std::tuple<CheckResult, Expression, CexGraph> query(Expression const& _expr) override; 50 51 void declareVariable(std::string const& _name, SortPointer const& _sort) override; 52 unhandledQueries()53 std::vector<std::string> unhandledQueries() const { return m_unhandledQueries; } 54 smtlib2Interface()55 SMTLib2Interface* smtlib2Interface() const { return m_smtlib2.get(); } 56 57 private: 58 std::string toSmtLibSort(Sort const& _sort); 59 std::string toSmtLibSort(std::vector<SortPointer> const& _sort); 60 61 void writeHeader(); 62 std::string forall(); 63 64 void declareFunction(std::string const& _name, SortPointer const& _sort); 65 66 void write(std::string _data); 67 68 /// Communicates with the solver via the callback. Throws SMTSolverError on error. 69 std::string querySolver(std::string const& _input); 70 71 /// Used to access toSmtLibSort, SExpr, and handle variables. 72 std::unique_ptr<SMTLib2Interface> m_smtlib2; 73 74 std::string m_accumulatedOutput; 75 std::set<std::string> m_variables; 76 77 std::map<util::h256, std::string> const& m_queryResponses; 78 std::vector<std::string> m_unhandledQueries; 79 80 frontend::ReadCallback::Callback m_smtCallback; 81 82 std::map<Sort const*, std::string> m_sortNames; 83 }; 84 85 } 86