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/SMTPortfolio.h>
20
21 #ifdef HAVE_Z3
22 #include <libsmtutil/Z3Interface.h>
23 #endif
24 #ifdef HAVE_CVC4
25 #include <libsmtutil/CVC4Interface.h>
26 #endif
27 #include <libsmtutil/SMTLib2Interface.h>
28
29 using namespace std;
30 using namespace solidity;
31 using namespace solidity::util;
32 using namespace solidity::frontend;
33 using namespace solidity::smtutil;
34
SMTPortfolio(map<h256,string> _smtlib2Responses,frontend::ReadCallback::Callback _smtCallback,SMTSolverChoice _enabledSolvers,optional<unsigned> _queryTimeout)35 SMTPortfolio::SMTPortfolio(
36 map<h256, string> _smtlib2Responses,
37 frontend::ReadCallback::Callback _smtCallback,
38 [[maybe_unused]] SMTSolverChoice _enabledSolvers,
39 optional<unsigned> _queryTimeout
40 ):
41 SolverInterface(_queryTimeout)
42 {
43 if (_enabledSolvers.smtlib2)
44 m_solvers.emplace_back(make_unique<SMTLib2Interface>(move(_smtlib2Responses), move(_smtCallback), m_queryTimeout));
45 #ifdef HAVE_Z3
46 if (_enabledSolvers.z3 && Z3Interface::available())
47 m_solvers.emplace_back(make_unique<Z3Interface>(m_queryTimeout));
48 #endif
49 #ifdef HAVE_CVC4
50 if (_enabledSolvers.cvc4)
51 m_solvers.emplace_back(make_unique<CVC4Interface>(m_queryTimeout));
52 #endif
53 }
54
reset()55 void SMTPortfolio::reset()
56 {
57 for (auto const& s: m_solvers)
58 s->reset();
59 }
60
push()61 void SMTPortfolio::push()
62 {
63 for (auto const& s: m_solvers)
64 s->push();
65 }
66
pop()67 void SMTPortfolio::pop()
68 {
69 for (auto const& s: m_solvers)
70 s->pop();
71 }
72
declareVariable(string const & _name,SortPointer const & _sort)73 void SMTPortfolio::declareVariable(string const& _name, SortPointer const& _sort)
74 {
75 smtAssert(_sort, "");
76 for (auto const& s: m_solvers)
77 s->declareVariable(_name, _sort);
78 }
79
addAssertion(Expression const & _expr)80 void SMTPortfolio::addAssertion(Expression const& _expr)
81 {
82 for (auto const& s: m_solvers)
83 s->addAssertion(_expr);
84 }
85
86 /*
87 * Broadcasts the SMT query to all solvers and returns a single result.
88 * This comment explains how this result is decided.
89 *
90 * When a solver is queried, there are four possible answers:
91 * SATISFIABLE (SAT), UNSATISFIABLE (UNSAT), UNKNOWN, CONFLICTING, ERROR
92 * We say that a solver _answered_ the query if it returns either:
93 * SAT or UNSAT
94 * A solver did not answer the query if it returns either:
95 * UNKNOWN (it tried but couldn't solve it) or ERROR (crash, internal error, API error, etc).
96 *
97 * Ideally all solvers answer the query and agree on what the answer is
98 * (all say SAT or all say UNSAT).
99 *
100 * The actual logic as as follows:
101 * 1) If at least one solver answers the query, all the non-answer results are ignored.
102 * Here SAT/UNSAT is preferred over UNKNOWN since it's an actual answer, and over ERROR
103 * because one buggy solver/integration shouldn't break the portfolio.
104 *
105 * 2) If at least one solver answers SAT and at least one answers UNSAT, at least one of them is buggy
106 * and the result is CONFLICTING.
107 * In the future if we have more than 2 solvers enabled we could go with the majority.
108 *
109 * 3) If NO solver answers the query:
110 * If at least one solver returned UNKNOWN (where the rest returned ERROR), the result is UNKNOWN.
111 * This is preferred over ERROR since the SMTChecker might decide to abstract the query
112 * when it is told that this is a hard query to solve.
113 *
114 * If all solvers return ERROR, the result is ERROR.
115 */
check(vector<Expression> const & _expressionsToEvaluate)116 pair<CheckResult, vector<string>> SMTPortfolio::check(vector<Expression> const& _expressionsToEvaluate)
117 {
118 CheckResult lastResult = CheckResult::ERROR;
119 vector<string> finalValues;
120 for (auto const& s: m_solvers)
121 {
122 CheckResult result;
123 vector<string> values;
124 tie(result, values) = s->check(_expressionsToEvaluate);
125 if (solverAnswered(result))
126 {
127 if (!solverAnswered(lastResult))
128 {
129 lastResult = result;
130 finalValues = std::move(values);
131 }
132 else if (lastResult != result)
133 {
134 lastResult = CheckResult::CONFLICTING;
135 break;
136 }
137 }
138 else if (result == CheckResult::UNKNOWN && lastResult == CheckResult::ERROR)
139 lastResult = result;
140 }
141 return make_pair(lastResult, finalValues);
142 }
143
unhandledQueries()144 vector<string> SMTPortfolio::unhandledQueries()
145 {
146 // This code assumes that the constructor guarantees that
147 // SmtLib2Interface is in position 0, if enabled.
148 if (!m_solvers.empty())
149 if (auto smtlib2 = dynamic_cast<SMTLib2Interface*>(m_solvers.front().get()))
150 return smtlib2->unhandledQueries();
151 return {};
152 }
153
solverAnswered(CheckResult result)154 bool SMTPortfolio::solverAnswered(CheckResult result)
155 {
156 return result == CheckResult::SATISFIABLE || result == CheckResult::UNSATISFIABLE;
157 }
158