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 #include <libsmtutil/CHCSmtLib2Interface.h>
20
21 #include <libsolutil/Keccak256.h>
22
23 #include <boost/algorithm/string/join.hpp>
24 #include <boost/algorithm/string/predicate.hpp>
25
26 #include <range/v3/view.hpp>
27
28 #include <array>
29 #include <fstream>
30 #include <iostream>
31 #include <memory>
32 #include <stdexcept>
33
34 using namespace std;
35 using namespace solidity;
36 using namespace solidity::util;
37 using namespace solidity::frontend;
38 using namespace solidity::smtutil;
39
CHCSmtLib2Interface(map<h256,string> const & _queryResponses,ReadCallback::Callback _smtCallback,optional<unsigned> _queryTimeout)40 CHCSmtLib2Interface::CHCSmtLib2Interface(
41 map<h256, string> const& _queryResponses,
42 ReadCallback::Callback _smtCallback,
43 optional<unsigned> _queryTimeout
44 ):
45 CHCSolverInterface(_queryTimeout),
46 m_smtlib2(make_unique<SMTLib2Interface>(_queryResponses, _smtCallback, m_queryTimeout)),
47 m_queryResponses(move(_queryResponses)),
48 m_smtCallback(_smtCallback)
49 {
50 reset();
51 }
52
reset()53 void CHCSmtLib2Interface::reset()
54 {
55 m_accumulatedOutput.clear();
56 m_variables.clear();
57 m_unhandledQueries.clear();
58 m_sortNames.clear();
59 }
60
registerRelation(Expression const & _expr)61 void CHCSmtLib2Interface::registerRelation(Expression const& _expr)
62 {
63 smtAssert(_expr.sort);
64 smtAssert(_expr.sort->kind == Kind::Function);
65 if (!m_variables.count(_expr.name))
66 {
67 auto fSort = dynamic_pointer_cast<FunctionSort>(_expr.sort);
68 string domain = toSmtLibSort(fSort->domain);
69 // Relations are predicates which have implicit codomain Bool.
70 m_variables.insert(_expr.name);
71 write(
72 "(declare-fun |" +
73 _expr.name +
74 "| " +
75 domain +
76 " Bool)"
77 );
78 }
79 }
80
addRule(Expression const & _expr,std::string const &)81 void CHCSmtLib2Interface::addRule(Expression const& _expr, std::string const& /*_name*/)
82 {
83 write(
84 "(assert\n(forall " + forall() + "\n" +
85 m_smtlib2->toSExpr(_expr) +
86 "))\n\n"
87 );
88 }
89
query(Expression const & _block)90 tuple<CheckResult, Expression, CHCSolverInterface::CexGraph> CHCSmtLib2Interface::query(Expression const& _block)
91 {
92 string accumulated{};
93 swap(m_accumulatedOutput, accumulated);
94 solAssert(m_smtlib2, "");
95 writeHeader();
96 for (auto const& decl: m_smtlib2->userSorts() | ranges::views::values)
97 write(decl);
98 m_accumulatedOutput += accumulated;
99
100 string queryRule = "(assert\n(forall " + forall() + "\n" +
101 "(=> " + _block.name + " false)"
102 "))";
103 string response = querySolver(
104 m_accumulatedOutput +
105 queryRule +
106 "\n(check-sat)"
107 );
108 swap(m_accumulatedOutput, accumulated);
109
110 CheckResult result;
111 // TODO proper parsing
112 if (boost::starts_with(response, "sat"))
113 result = CheckResult::UNSATISFIABLE;
114 else if (boost::starts_with(response, "unsat"))
115 result = CheckResult::SATISFIABLE;
116 else if (boost::starts_with(response, "unknown"))
117 result = CheckResult::UNKNOWN;
118 else
119 result = CheckResult::ERROR;
120
121 return {result, Expression(true), {}};
122 }
123
declareVariable(string const & _name,SortPointer const & _sort)124 void CHCSmtLib2Interface::declareVariable(string const& _name, SortPointer const& _sort)
125 {
126 smtAssert(_sort);
127 if (_sort->kind == Kind::Function)
128 declareFunction(_name, _sort);
129 else if (!m_variables.count(_name))
130 {
131 m_variables.insert(_name);
132 write("(declare-var |" + _name + "| " + toSmtLibSort(*_sort) + ')');
133 }
134 }
135
toSmtLibSort(Sort const & _sort)136 string CHCSmtLib2Interface::toSmtLibSort(Sort const& _sort)
137 {
138 if (!m_sortNames.count(&_sort))
139 m_sortNames[&_sort] = m_smtlib2->toSmtLibSort(_sort);
140 return m_sortNames.at(&_sort);
141 }
142
toSmtLibSort(vector<SortPointer> const & _sorts)143 string CHCSmtLib2Interface::toSmtLibSort(vector<SortPointer> const& _sorts)
144 {
145 string ssort("(");
146 for (auto const& sort: _sorts)
147 ssort += toSmtLibSort(*sort) + " ";
148 ssort += ")";
149 return ssort;
150 }
151
writeHeader()152 void CHCSmtLib2Interface::writeHeader()
153 {
154 if (m_queryTimeout)
155 write("(set-option :timeout " + to_string(*m_queryTimeout) + ")");
156 write("(set-logic HORN)\n");
157 }
158
forall()159 string CHCSmtLib2Interface::forall()
160 {
161 string vars("(");
162 for (auto const& [name, sort]: m_smtlib2->variables())
163 {
164 solAssert(sort, "");
165 if (sort->kind != Kind::Function)
166 vars += " (" + name + " " + toSmtLibSort(*sort) + ")";
167 }
168 vars += ")";
169 return vars;
170 }
171
declareFunction(string const & _name,SortPointer const & _sort)172 void CHCSmtLib2Interface::declareFunction(string const& _name, SortPointer const& _sort)
173 {
174 smtAssert(_sort);
175 smtAssert(_sort->kind == Kind::Function);
176 // TODO Use domain and codomain as key as well
177 if (!m_variables.count(_name))
178 {
179 auto fSort = dynamic_pointer_cast<FunctionSort>(_sort);
180 smtAssert(fSort->codomain);
181 string domain = toSmtLibSort(fSort->domain);
182 string codomain = toSmtLibSort(*fSort->codomain);
183 m_variables.insert(_name);
184 write(
185 "(declare-fun |" +
186 _name +
187 "| " +
188 domain +
189 " " +
190 codomain +
191 ")"
192 );
193 }
194 }
195
write(string _data)196 void CHCSmtLib2Interface::write(string _data)
197 {
198 m_accumulatedOutput += move(_data) + "\n";
199 }
200
querySolver(string const & _input)201 string CHCSmtLib2Interface::querySolver(string const& _input)
202 {
203 util::h256 inputHash = util::keccak256(_input);
204 if (m_queryResponses.count(inputHash))
205 return m_queryResponses.at(inputHash);
206 if (m_smtCallback)
207 {
208 auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery), _input);
209 if (result.success)
210 return result.responseOrErrorMessage;
211 }
212 m_unhandledQueries.push_back(_input);
213 return "unknown\n";
214 }
215