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/CVC4Interface.h>
20
21 #include <libsolutil/CommonIO.h>
22
23 #include <cvc4/util/bitvector.h>
24
25 using namespace std;
26 using namespace solidity;
27 using namespace solidity::util;
28 using namespace solidity::smtutil;
29
CVC4Interface(optional<unsigned> _queryTimeout)30 CVC4Interface::CVC4Interface(optional<unsigned> _queryTimeout):
31 SolverInterface(_queryTimeout),
32 m_solver(&m_context)
33 {
34 reset();
35 }
36
reset()37 void CVC4Interface::reset()
38 {
39 m_variables.clear();
40 m_solver.reset();
41 m_solver.setOption("produce-models", true);
42 if (m_queryTimeout)
43 m_solver.setTimeLimit(*m_queryTimeout);
44 else
45 m_solver.setResourceLimit(resourceLimit);
46 }
47
push()48 void CVC4Interface::push()
49 {
50 m_solver.push();
51 }
52
pop()53 void CVC4Interface::pop()
54 {
55 m_solver.pop();
56 }
57
declareVariable(string const & _name,SortPointer const & _sort)58 void CVC4Interface::declareVariable(string const& _name, SortPointer const& _sort)
59 {
60 smtAssert(_sort, "");
61 m_variables[_name] = m_context.mkVar(_name.c_str(), cvc4Sort(*_sort));
62 }
63
addAssertion(Expression const & _expr)64 void CVC4Interface::addAssertion(Expression const& _expr)
65 {
66 try
67 {
68 m_solver.assertFormula(toCVC4Expr(_expr));
69 }
70 catch (CVC4::TypeCheckingException const& _e)
71 {
72 smtAssert(false, _e.what());
73 }
74 catch (CVC4::LogicException const& _e)
75 {
76 smtAssert(false, _e.what());
77 }
78 catch (CVC4::UnsafeInterruptException const& _e)
79 {
80 smtAssert(false, _e.what());
81 }
82 catch (CVC4::Exception const& _e)
83 {
84 smtAssert(false, _e.what());
85 }
86 }
87
check(vector<Expression> const & _expressionsToEvaluate)88 pair<CheckResult, vector<string>> CVC4Interface::check(vector<Expression> const& _expressionsToEvaluate)
89 {
90 CheckResult result;
91 vector<string> values;
92 try
93 {
94 switch (m_solver.checkSat().isSat())
95 {
96 case CVC4::Result::SAT:
97 result = CheckResult::SATISFIABLE;
98 break;
99 case CVC4::Result::UNSAT:
100 result = CheckResult::UNSATISFIABLE;
101 break;
102 case CVC4::Result::SAT_UNKNOWN:
103 result = CheckResult::UNKNOWN;
104 break;
105 default:
106 smtAssert(false, "");
107 }
108
109 if (result == CheckResult::SATISFIABLE && !_expressionsToEvaluate.empty())
110 {
111 for (Expression const& e: _expressionsToEvaluate)
112 values.push_back(toString(m_solver.getValue(toCVC4Expr(e))));
113 }
114 }
115 catch (CVC4::Exception const&)
116 {
117 result = CheckResult::ERROR;
118 values.clear();
119 }
120
121 return make_pair(result, values);
122 }
123
toCVC4Expr(Expression const & _expr)124 CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
125 {
126 // Variable
127 if (_expr.arguments.empty() && m_variables.count(_expr.name))
128 return m_variables.at(_expr.name);
129
130 vector<CVC4::Expr> arguments;
131 for (auto const& arg: _expr.arguments)
132 arguments.push_back(toCVC4Expr(arg));
133
134 try
135 {
136 string const& n = _expr.name;
137 // Function application
138 if (!arguments.empty() && m_variables.count(_expr.name))
139 return m_context.mkExpr(CVC4::kind::APPLY_UF, m_variables.at(n), arguments);
140 // Literal
141 else if (arguments.empty())
142 {
143 if (n == "true")
144 return m_context.mkConst(true);
145 else if (n == "false")
146 return m_context.mkConst(false);
147 else if (auto sortSort = dynamic_pointer_cast<SortSort>(_expr.sort))
148 return m_context.mkVar(n, cvc4Sort(*sortSort->inner));
149 else
150 try
151 {
152 return m_context.mkConst(CVC4::Rational(n));
153 }
154 catch (CVC4::TypeCheckingException const& _e)
155 {
156 smtAssert(false, _e.what());
157 }
158 catch (CVC4::Exception const& _e)
159 {
160 smtAssert(false, _e.what());
161 }
162 }
163
164 smtAssert(_expr.hasCorrectArity(), "");
165 if (n == "ite")
166 return arguments[0].iteExpr(arguments[1], arguments[2]);
167 else if (n == "not")
168 return arguments[0].notExpr();
169 else if (n == "and")
170 return arguments[0].andExpr(arguments[1]);
171 else if (n == "or")
172 return arguments[0].orExpr(arguments[1]);
173 else if (n == "=>")
174 return m_context.mkExpr(CVC4::kind::IMPLIES, arguments[0], arguments[1]);
175 else if (n == "=")
176 return m_context.mkExpr(CVC4::kind::EQUAL, arguments[0], arguments[1]);
177 else if (n == "<")
178 return m_context.mkExpr(CVC4::kind::LT, arguments[0], arguments[1]);
179 else if (n == "<=")
180 return m_context.mkExpr(CVC4::kind::LEQ, arguments[0], arguments[1]);
181 else if (n == ">")
182 return m_context.mkExpr(CVC4::kind::GT, arguments[0], arguments[1]);
183 else if (n == ">=")
184 return m_context.mkExpr(CVC4::kind::GEQ, arguments[0], arguments[1]);
185 else if (n == "+")
186 return m_context.mkExpr(CVC4::kind::PLUS, arguments[0], arguments[1]);
187 else if (n == "-")
188 return m_context.mkExpr(CVC4::kind::MINUS, arguments[0], arguments[1]);
189 else if (n == "*")
190 return m_context.mkExpr(CVC4::kind::MULT, arguments[0], arguments[1]);
191 else if (n == "div")
192 return m_context.mkExpr(CVC4::kind::INTS_DIVISION_TOTAL, arguments[0], arguments[1]);
193 else if (n == "mod")
194 return m_context.mkExpr(CVC4::kind::INTS_MODULUS, arguments[0], arguments[1]);
195 else if (n == "bvnot")
196 return m_context.mkExpr(CVC4::kind::BITVECTOR_NOT, arguments[0]);
197 else if (n == "bvand")
198 return m_context.mkExpr(CVC4::kind::BITVECTOR_AND, arguments[0], arguments[1]);
199 else if (n == "bvor")
200 return m_context.mkExpr(CVC4::kind::BITVECTOR_OR, arguments[0], arguments[1]);
201 else if (n == "bvxor")
202 return m_context.mkExpr(CVC4::kind::BITVECTOR_XOR, arguments[0], arguments[1]);
203 else if (n == "bvshl")
204 return m_context.mkExpr(CVC4::kind::BITVECTOR_SHL, arguments[0], arguments[1]);
205 else if (n == "bvlshr")
206 return m_context.mkExpr(CVC4::kind::BITVECTOR_LSHR, arguments[0], arguments[1]);
207 else if (n == "bvashr")
208 return m_context.mkExpr(CVC4::kind::BITVECTOR_ASHR, arguments[0], arguments[1]);
209 else if (n == "int2bv")
210 {
211 size_t size = std::stoul(_expr.arguments[1].name);
212 auto i2bvOp = m_context.mkConst(CVC4::IntToBitVector(static_cast<unsigned>(size)));
213 // CVC4 treats all BVs as unsigned, so we need to manually apply 2's complement if needed.
214 return m_context.mkExpr(
215 CVC4::kind::ITE,
216 m_context.mkExpr(CVC4::kind::GEQ, arguments[0], m_context.mkConst(CVC4::Rational(0))),
217 m_context.mkExpr(CVC4::kind::INT_TO_BITVECTOR, i2bvOp, arguments[0]),
218 m_context.mkExpr(
219 CVC4::kind::BITVECTOR_NEG,
220 m_context.mkExpr(CVC4::kind::INT_TO_BITVECTOR, i2bvOp, m_context.mkExpr(CVC4::kind::UMINUS, arguments[0]))
221 )
222 );
223 }
224 else if (n == "bv2int")
225 {
226 auto intSort = dynamic_pointer_cast<IntSort>(_expr.sort);
227 smtAssert(intSort, "");
228 auto nat = m_context.mkExpr(CVC4::kind::BITVECTOR_TO_NAT, arguments[0]);
229 if (!intSort->isSigned)
230 return nat;
231
232 auto type = arguments[0].getType();
233 smtAssert(type.isBitVector(), "");
234 auto size = CVC4::BitVectorType(type).getSize();
235 // CVC4 treats all BVs as unsigned, so we need to manually apply 2's complement if needed.
236 auto extractOp = m_context.mkConst(CVC4::BitVectorExtract(size - 1, size - 1));
237 return m_context.mkExpr(CVC4::kind::ITE,
238 m_context.mkExpr(
239 CVC4::kind::EQUAL,
240 m_context.mkExpr(CVC4::kind::BITVECTOR_EXTRACT, extractOp, arguments[0]),
241 m_context.mkConst(CVC4::BitVector(1, size_t(0)))
242 ),
243 nat,
244 m_context.mkExpr(
245 CVC4::kind::UMINUS,
246 m_context.mkExpr(CVC4::kind::BITVECTOR_TO_NAT, m_context.mkExpr(CVC4::kind::BITVECTOR_NEG, arguments[0]))
247 )
248 );
249 }
250 else if (n == "select")
251 return m_context.mkExpr(CVC4::kind::SELECT, arguments[0], arguments[1]);
252 else if (n == "store")
253 return m_context.mkExpr(CVC4::kind::STORE, arguments[0], arguments[1], arguments[2]);
254 else if (n == "const_array")
255 {
256 shared_ptr<SortSort> sortSort = std::dynamic_pointer_cast<SortSort>(_expr.arguments[0].sort);
257 smtAssert(sortSort, "");
258 return m_context.mkConst(CVC4::ArrayStoreAll(cvc4Sort(*sortSort->inner), arguments[1]));
259 }
260 else if (n == "tuple_get")
261 {
262 shared_ptr<TupleSort> tupleSort = std::dynamic_pointer_cast<TupleSort>(_expr.arguments[0].sort);
263 smtAssert(tupleSort, "");
264 CVC4::DatatypeType tt = m_context.mkTupleType(cvc4Sort(tupleSort->components));
265 CVC4::Datatype const& dt = tt.getDatatype();
266 size_t index = std::stoul(_expr.arguments[1].name);
267 CVC4::Expr s = dt[0][index].getSelector();
268 return m_context.mkExpr(CVC4::kind::APPLY_SELECTOR, s, arguments[0]);
269 }
270 else if (n == "tuple_constructor")
271 {
272 shared_ptr<TupleSort> tupleSort = std::dynamic_pointer_cast<TupleSort>(_expr.sort);
273 smtAssert(tupleSort, "");
274 CVC4::DatatypeType tt = m_context.mkTupleType(cvc4Sort(tupleSort->components));
275 CVC4::Datatype const& dt = tt.getDatatype();
276 CVC4::Expr c = dt[0].getConstructor();
277 return m_context.mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, c, arguments);
278 }
279
280 smtAssert(false, "");
281 }
282 catch (CVC4::TypeCheckingException const& _e)
283 {
284 smtAssert(false, _e.what());
285 }
286 catch (CVC4::Exception const& _e)
287 {
288 smtAssert(false, _e.what());
289 }
290
291 smtAssert(false, "");
292 }
293
cvc4Sort(Sort const & _sort)294 CVC4::Type CVC4Interface::cvc4Sort(Sort const& _sort)
295 {
296 switch (_sort.kind)
297 {
298 case Kind::Bool:
299 return m_context.booleanType();
300 case Kind::Int:
301 return m_context.integerType();
302 case Kind::BitVector:
303 return m_context.mkBitVectorType(dynamic_cast<BitVectorSort const&>(_sort).size);
304 case Kind::Function:
305 {
306 FunctionSort const& fSort = dynamic_cast<FunctionSort const&>(_sort);
307 return m_context.mkFunctionType(cvc4Sort(fSort.domain), cvc4Sort(*fSort.codomain));
308 }
309 case Kind::Array:
310 {
311 auto const& arraySort = dynamic_cast<ArraySort const&>(_sort);
312 return m_context.mkArrayType(cvc4Sort(*arraySort.domain), cvc4Sort(*arraySort.range));
313 }
314 case Kind::Tuple:
315 {
316 auto const& tupleSort = dynamic_cast<TupleSort const&>(_sort);
317 return m_context.mkTupleType(cvc4Sort(tupleSort.components));
318 }
319 default:
320 break;
321 }
322 smtAssert(false, "");
323 // Cannot be reached.
324 return m_context.integerType();
325 }
326
cvc4Sort(vector<SortPointer> const & _sorts)327 vector<CVC4::Type> CVC4Interface::cvc4Sort(vector<SortPointer> const& _sorts)
328 {
329 vector<CVC4::Type> cvc4Sorts;
330 for (auto const& _sort: _sorts)
331 cvc4Sorts.push_back(cvc4Sort(*_sort));
332 return cvc4Sorts;
333 }
334