1 | //== Z3Solver.cpp -----------------------------------------------*- C++ -*--==// |
2 | // |
3 | // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. |
4 | // See https://llvm.org/LICENSE.txt for license information. |
5 | // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception |
6 | // |
7 | //===----------------------------------------------------------------------===// |
8 | |
9 | #include "llvm/Config/config.h" |
10 | #include "llvm/Support/SMTAPI.h" |
11 | |
12 | using namespace llvm; |
13 | |
14 | #if LLVM_WITH_Z3 |
15 | |
16 | #include "llvm/ADT/SmallString.h" |
17 | #include "llvm/ADT/Twine.h" |
18 | |
19 | #include <set> |
20 | |
21 | #include <z3.h> |
22 | |
23 | namespace { |
24 | |
25 | /// Configuration class for Z3 |
26 | class Z3Config { |
27 | friend class Z3Context; |
28 | |
29 | Z3_config Config; |
30 | |
31 | public: |
32 | Z3Config() : Config(Z3_mk_config()) { |
33 | // Enable model finding |
34 | Z3_set_param_value(Config, "model" , "true" ); |
35 | // Disable proof generation |
36 | Z3_set_param_value(Config, "proof" , "false" ); |
37 | // Set timeout to 15000ms = 15s |
38 | Z3_set_param_value(Config, "timeout" , "15000" ); |
39 | } |
40 | |
41 | ~Z3Config() { Z3_del_config(Config); } |
42 | }; // end class Z3Config |
43 | |
44 | // Function used to report errors |
45 | void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) { |
46 | llvm::report_fatal_error("Z3 error: " + |
47 | llvm::Twine(Z3_get_error_msg(Context, Error))); |
48 | } |
49 | |
50 | /// Wrapper for Z3 context |
51 | class Z3Context { |
52 | public: |
53 | Z3_context Context; |
54 | |
55 | Z3Context() { |
56 | Context = Z3_mk_context_rc(Z3Config().Config); |
57 | // The error function is set here because the context is the first object |
58 | // created by the backend |
59 | Z3_set_error_handler(Context, Z3ErrorHandler); |
60 | } |
61 | |
62 | virtual ~Z3Context() { |
63 | Z3_del_context(Context); |
64 | Context = nullptr; |
65 | } |
66 | }; // end class Z3Context |
67 | |
68 | /// Wrapper for Z3 Sort |
69 | class Z3Sort : public SMTSort { |
70 | friend class Z3Solver; |
71 | |
72 | Z3Context &Context; |
73 | |
74 | Z3_sort Sort; |
75 | |
76 | public: |
77 | /// Default constructor, mainly used by make_shared |
78 | Z3Sort(Z3Context &C, Z3_sort ZS) : Context(C), Sort(ZS) { |
79 | Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort)); |
80 | } |
81 | |
82 | /// Override implicit copy constructor for correct reference counting. |
83 | Z3Sort(const Z3Sort &Other) : Context(Other.Context), Sort(Other.Sort) { |
84 | Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort)); |
85 | } |
86 | |
87 | /// Override implicit copy assignment constructor for correct reference |
88 | /// counting. |
89 | Z3Sort &operator=(const Z3Sort &Other) { |
90 | Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Other.Sort)); |
91 | Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort)); |
92 | Sort = Other.Sort; |
93 | return *this; |
94 | } |
95 | |
96 | Z3Sort(Z3Sort &&Other) = delete; |
97 | Z3Sort &operator=(Z3Sort &&Other) = delete; |
98 | |
99 | ~Z3Sort() { |
100 | if (Sort) |
101 | Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort)); |
102 | } |
103 | |
104 | void Profile(llvm::FoldingSetNodeID &ID) const override { |
105 | ID.AddInteger( |
106 | Z3_get_ast_id(Context.Context, reinterpret_cast<Z3_ast>(Sort))); |
107 | } |
108 | |
109 | bool isBitvectorSortImpl() const override { |
110 | return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BV_SORT); |
111 | } |
112 | |
113 | bool isFloatSortImpl() const override { |
114 | return (Z3_get_sort_kind(Context.Context, Sort) == Z3_FLOATING_POINT_SORT); |
115 | } |
116 | |
117 | bool isBooleanSortImpl() const override { |
118 | return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BOOL_SORT); |
119 | } |
120 | |
121 | unsigned getBitvectorSortSizeImpl() const override { |
122 | return Z3_get_bv_sort_size(Context.Context, Sort); |
123 | } |
124 | |
125 | unsigned getFloatSortSizeImpl() const override { |
126 | return Z3_fpa_get_ebits(Context.Context, Sort) + |
127 | Z3_fpa_get_sbits(Context.Context, Sort); |
128 | } |
129 | |
130 | bool equal_to(SMTSort const &Other) const override { |
131 | return Z3_is_eq_sort(Context.Context, Sort, |
132 | static_cast<const Z3Sort &>(Other).Sort); |
133 | } |
134 | |
135 | void print(raw_ostream &OS) const override { |
136 | OS << Z3_sort_to_string(Context.Context, Sort); |
137 | } |
138 | }; // end class Z3Sort |
139 | |
140 | static const Z3Sort &toZ3Sort(const SMTSort &S) { |
141 | return static_cast<const Z3Sort &>(S); |
142 | } |
143 | |
144 | class Z3Expr : public SMTExpr { |
145 | friend class Z3Solver; |
146 | |
147 | Z3Context &Context; |
148 | |
149 | Z3_ast AST; |
150 | |
151 | public: |
152 | Z3Expr(Z3Context &C, Z3_ast ZA) : SMTExpr(), Context(C), AST(ZA) { |
153 | Z3_inc_ref(Context.Context, AST); |
154 | } |
155 | |
156 | /// Override implicit copy constructor for correct reference counting. |
157 | Z3Expr(const Z3Expr &Copy) : SMTExpr(), Context(Copy.Context), AST(Copy.AST) { |
158 | Z3_inc_ref(Context.Context, AST); |
159 | } |
160 | |
161 | /// Override implicit copy assignment constructor for correct reference |
162 | /// counting. |
163 | Z3Expr &operator=(const Z3Expr &Other) { |
164 | Z3_inc_ref(Context.Context, Other.AST); |
165 | Z3_dec_ref(Context.Context, AST); |
166 | AST = Other.AST; |
167 | return *this; |
168 | } |
169 | |
170 | Z3Expr(Z3Expr &&Other) = delete; |
171 | Z3Expr &operator=(Z3Expr &&Other) = delete; |
172 | |
173 | ~Z3Expr() { |
174 | if (AST) |
175 | Z3_dec_ref(Context.Context, AST); |
176 | } |
177 | |
178 | void Profile(llvm::FoldingSetNodeID &ID) const override { |
179 | ID.AddInteger(Z3_get_ast_id(Context.Context, AST)); |
180 | } |
181 | |
182 | /// Comparison of AST equality, not model equivalence. |
183 | bool equal_to(SMTExpr const &Other) const override { |
184 | assert(Z3_is_eq_sort(Context.Context, Z3_get_sort(Context.Context, AST), |
185 | Z3_get_sort(Context.Context, |
186 | static_cast<const Z3Expr &>(Other).AST)) && |
187 | "AST's must have the same sort" ); |
188 | return Z3_is_eq_ast(Context.Context, AST, |
189 | static_cast<const Z3Expr &>(Other).AST); |
190 | } |
191 | |
192 | void print(raw_ostream &OS) const override { |
193 | OS << Z3_ast_to_string(Context.Context, AST); |
194 | } |
195 | }; // end class Z3Expr |
196 | |
197 | static const Z3Expr &toZ3Expr(const SMTExpr &E) { |
198 | return static_cast<const Z3Expr &>(E); |
199 | } |
200 | |
201 | class Z3Model { |
202 | friend class Z3Solver; |
203 | |
204 | Z3Context &Context; |
205 | |
206 | Z3_model Model; |
207 | |
208 | public: |
209 | Z3Model(Z3Context &C, Z3_model ZM) : Context(C), Model(ZM) { |
210 | Z3_model_inc_ref(Context.Context, Model); |
211 | } |
212 | |
213 | Z3Model(const Z3Model &Other) = delete; |
214 | Z3Model(Z3Model &&Other) = delete; |
215 | Z3Model &operator=(Z3Model &Other) = delete; |
216 | Z3Model &operator=(Z3Model &&Other) = delete; |
217 | |
218 | ~Z3Model() { |
219 | if (Model) |
220 | Z3_model_dec_ref(Context.Context, Model); |
221 | } |
222 | |
223 | void print(raw_ostream &OS) const { |
224 | OS << Z3_model_to_string(Context.Context, Model); |
225 | } |
226 | |
227 | LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); } |
228 | }; // end class Z3Model |
229 | |
230 | /// Get the corresponding IEEE floating-point type for a given bitwidth. |
231 | static const llvm::fltSemantics &getFloatSemantics(unsigned BitWidth) { |
232 | switch (BitWidth) { |
233 | default: |
234 | llvm_unreachable("Unsupported floating-point semantics!" ); |
235 | break; |
236 | case 16: |
237 | return llvm::APFloat::IEEEhalf(); |
238 | case 32: |
239 | return llvm::APFloat::IEEEsingle(); |
240 | case 64: |
241 | return llvm::APFloat::IEEEdouble(); |
242 | case 128: |
243 | return llvm::APFloat::IEEEquad(); |
244 | } |
245 | } |
246 | |
247 | // Determine whether two float semantics are equivalent |
248 | static bool areEquivalent(const llvm::fltSemantics &LHS, |
249 | const llvm::fltSemantics &RHS) { |
250 | return (llvm::APFloat::semanticsPrecision(LHS) == |
251 | llvm::APFloat::semanticsPrecision(RHS)) && |
252 | (llvm::APFloat::semanticsMinExponent(LHS) == |
253 | llvm::APFloat::semanticsMinExponent(RHS)) && |
254 | (llvm::APFloat::semanticsMaxExponent(LHS) == |
255 | llvm::APFloat::semanticsMaxExponent(RHS)) && |
256 | (llvm::APFloat::semanticsSizeInBits(LHS) == |
257 | llvm::APFloat::semanticsSizeInBits(RHS)); |
258 | } |
259 | |
260 | class Z3Solver : public SMTSolver { |
261 | friend class Z3ConstraintManager; |
262 | |
263 | Z3Context Context; |
264 | |
265 | Z3_solver Solver; |
266 | |
267 | // Cache Sorts |
268 | std::set<Z3Sort> CachedSorts; |
269 | |
270 | // Cache Exprs |
271 | std::set<Z3Expr> CachedExprs; |
272 | |
273 | public: |
274 | Z3Solver() : Solver(Z3_mk_simple_solver(Context.Context)) { |
275 | Z3_solver_inc_ref(Context.Context, Solver); |
276 | } |
277 | |
278 | Z3Solver(const Z3Solver &Other) = delete; |
279 | Z3Solver(Z3Solver &&Other) = delete; |
280 | Z3Solver &operator=(Z3Solver &Other) = delete; |
281 | Z3Solver &operator=(Z3Solver &&Other) = delete; |
282 | |
283 | ~Z3Solver() { |
284 | if (Solver) |
285 | Z3_solver_dec_ref(Context.Context, Solver); |
286 | } |
287 | |
288 | void addConstraint(const SMTExprRef &Exp) const override { |
289 | Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST); |
290 | } |
291 | |
292 | // Given an SMTSort, adds/retrives it from the cache and returns |
293 | // an SMTSortRef to the SMTSort in the cache |
294 | SMTSortRef newSortRef(const SMTSort &Sort) { |
295 | auto It = CachedSorts.insert(toZ3Sort(Sort)); |
296 | return &(*It.first); |
297 | } |
298 | |
299 | // Given an SMTExpr, adds/retrives it from the cache and returns |
300 | // an SMTExprRef to the SMTExpr in the cache |
301 | SMTExprRef newExprRef(const SMTExpr &Exp) { |
302 | auto It = CachedExprs.insert(toZ3Expr(Exp)); |
303 | return &(*It.first); |
304 | } |
305 | |
306 | SMTSortRef getBoolSort() override { |
307 | return newSortRef(Z3Sort(Context, Z3_mk_bool_sort(Context.Context))); |
308 | } |
309 | |
310 | SMTSortRef getBitvectorSort(unsigned BitWidth) override { |
311 | return newSortRef( |
312 | Z3Sort(Context, Z3_mk_bv_sort(Context.Context, BitWidth))); |
313 | } |
314 | |
315 | SMTSortRef getSort(const SMTExprRef &Exp) override { |
316 | return newSortRef( |
317 | Z3Sort(Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST))); |
318 | } |
319 | |
320 | SMTSortRef getFloat16Sort() override { |
321 | return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_16(Context.Context))); |
322 | } |
323 | |
324 | SMTSortRef getFloat32Sort() override { |
325 | return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_32(Context.Context))); |
326 | } |
327 | |
328 | SMTSortRef getFloat64Sort() override { |
329 | return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_64(Context.Context))); |
330 | } |
331 | |
332 | SMTSortRef getFloat128Sort() override { |
333 | return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_128(Context.Context))); |
334 | } |
335 | |
336 | SMTExprRef mkBVNeg(const SMTExprRef &Exp) override { |
337 | return newExprRef( |
338 | Z3Expr(Context, Z3_mk_bvneg(Context.Context, toZ3Expr(*Exp).AST))); |
339 | } |
340 | |
341 | SMTExprRef mkBVNot(const SMTExprRef &Exp) override { |
342 | return newExprRef( |
343 | Z3Expr(Context, Z3_mk_bvnot(Context.Context, toZ3Expr(*Exp).AST))); |
344 | } |
345 | |
346 | SMTExprRef mkNot(const SMTExprRef &Exp) override { |
347 | return newExprRef( |
348 | Z3Expr(Context, Z3_mk_not(Context.Context, toZ3Expr(*Exp).AST))); |
349 | } |
350 | |
351 | SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
352 | return newExprRef( |
353 | Z3Expr(Context, Z3_mk_bvadd(Context.Context, toZ3Expr(*LHS).AST, |
354 | toZ3Expr(*RHS).AST))); |
355 | } |
356 | |
357 | SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
358 | return newExprRef( |
359 | Z3Expr(Context, Z3_mk_bvsub(Context.Context, toZ3Expr(*LHS).AST, |
360 | toZ3Expr(*RHS).AST))); |
361 | } |
362 | |
363 | SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
364 | return newExprRef( |
365 | Z3Expr(Context, Z3_mk_bvmul(Context.Context, toZ3Expr(*LHS).AST, |
366 | toZ3Expr(*RHS).AST))); |
367 | } |
368 | |
369 | SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
370 | return newExprRef( |
371 | Z3Expr(Context, Z3_mk_bvsrem(Context.Context, toZ3Expr(*LHS).AST, |
372 | toZ3Expr(*RHS).AST))); |
373 | } |
374 | |
375 | SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
376 | return newExprRef( |
377 | Z3Expr(Context, Z3_mk_bvurem(Context.Context, toZ3Expr(*LHS).AST, |
378 | toZ3Expr(*RHS).AST))); |
379 | } |
380 | |
381 | SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
382 | return newExprRef( |
383 | Z3Expr(Context, Z3_mk_bvsdiv(Context.Context, toZ3Expr(*LHS).AST, |
384 | toZ3Expr(*RHS).AST))); |
385 | } |
386 | |
387 | SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
388 | return newExprRef( |
389 | Z3Expr(Context, Z3_mk_bvudiv(Context.Context, toZ3Expr(*LHS).AST, |
390 | toZ3Expr(*RHS).AST))); |
391 | } |
392 | |
393 | SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
394 | return newExprRef( |
395 | Z3Expr(Context, Z3_mk_bvshl(Context.Context, toZ3Expr(*LHS).AST, |
396 | toZ3Expr(*RHS).AST))); |
397 | } |
398 | |
399 | SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
400 | return newExprRef( |
401 | Z3Expr(Context, Z3_mk_bvashr(Context.Context, toZ3Expr(*LHS).AST, |
402 | toZ3Expr(*RHS).AST))); |
403 | } |
404 | |
405 | SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
406 | return newExprRef( |
407 | Z3Expr(Context, Z3_mk_bvlshr(Context.Context, toZ3Expr(*LHS).AST, |
408 | toZ3Expr(*RHS).AST))); |
409 | } |
410 | |
411 | SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
412 | return newExprRef( |
413 | Z3Expr(Context, Z3_mk_bvxor(Context.Context, toZ3Expr(*LHS).AST, |
414 | toZ3Expr(*RHS).AST))); |
415 | } |
416 | |
417 | SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
418 | return newExprRef( |
419 | Z3Expr(Context, Z3_mk_bvor(Context.Context, toZ3Expr(*LHS).AST, |
420 | toZ3Expr(*RHS).AST))); |
421 | } |
422 | |
423 | SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
424 | return newExprRef( |
425 | Z3Expr(Context, Z3_mk_bvand(Context.Context, toZ3Expr(*LHS).AST, |
426 | toZ3Expr(*RHS).AST))); |
427 | } |
428 | |
429 | SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
430 | return newExprRef( |
431 | Z3Expr(Context, Z3_mk_bvult(Context.Context, toZ3Expr(*LHS).AST, |
432 | toZ3Expr(*RHS).AST))); |
433 | } |
434 | |
435 | SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
436 | return newExprRef( |
437 | Z3Expr(Context, Z3_mk_bvslt(Context.Context, toZ3Expr(*LHS).AST, |
438 | toZ3Expr(*RHS).AST))); |
439 | } |
440 | |
441 | SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
442 | return newExprRef( |
443 | Z3Expr(Context, Z3_mk_bvugt(Context.Context, toZ3Expr(*LHS).AST, |
444 | toZ3Expr(*RHS).AST))); |
445 | } |
446 | |
447 | SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
448 | return newExprRef( |
449 | Z3Expr(Context, Z3_mk_bvsgt(Context.Context, toZ3Expr(*LHS).AST, |
450 | toZ3Expr(*RHS).AST))); |
451 | } |
452 | |
453 | SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
454 | return newExprRef( |
455 | Z3Expr(Context, Z3_mk_bvule(Context.Context, toZ3Expr(*LHS).AST, |
456 | toZ3Expr(*RHS).AST))); |
457 | } |
458 | |
459 | SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
460 | return newExprRef( |
461 | Z3Expr(Context, Z3_mk_bvsle(Context.Context, toZ3Expr(*LHS).AST, |
462 | toZ3Expr(*RHS).AST))); |
463 | } |
464 | |
465 | SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
466 | return newExprRef( |
467 | Z3Expr(Context, Z3_mk_bvuge(Context.Context, toZ3Expr(*LHS).AST, |
468 | toZ3Expr(*RHS).AST))); |
469 | } |
470 | |
471 | SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
472 | return newExprRef( |
473 | Z3Expr(Context, Z3_mk_bvsge(Context.Context, toZ3Expr(*LHS).AST, |
474 | toZ3Expr(*RHS).AST))); |
475 | } |
476 | |
477 | SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
478 | Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST}; |
479 | return newExprRef(Z3Expr(Context, Z3_mk_and(Context.Context, 2, Args))); |
480 | } |
481 | |
482 | SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
483 | Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST}; |
484 | return newExprRef(Z3Expr(Context, Z3_mk_or(Context.Context, 2, Args))); |
485 | } |
486 | |
487 | SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
488 | return newExprRef( |
489 | Z3Expr(Context, Z3_mk_eq(Context.Context, toZ3Expr(*LHS).AST, |
490 | toZ3Expr(*RHS).AST))); |
491 | } |
492 | |
493 | SMTExprRef mkFPNeg(const SMTExprRef &Exp) override { |
494 | return newExprRef( |
495 | Z3Expr(Context, Z3_mk_fpa_neg(Context.Context, toZ3Expr(*Exp).AST))); |
496 | } |
497 | |
498 | SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) override { |
499 | return newExprRef(Z3Expr( |
500 | Context, Z3_mk_fpa_is_infinite(Context.Context, toZ3Expr(*Exp).AST))); |
501 | } |
502 | |
503 | SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) override { |
504 | return newExprRef( |
505 | Z3Expr(Context, Z3_mk_fpa_is_nan(Context.Context, toZ3Expr(*Exp).AST))); |
506 | } |
507 | |
508 | SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) override { |
509 | return newExprRef(Z3Expr( |
510 | Context, Z3_mk_fpa_is_normal(Context.Context, toZ3Expr(*Exp).AST))); |
511 | } |
512 | |
513 | SMTExprRef mkFPIsZero(const SMTExprRef &Exp) override { |
514 | return newExprRef(Z3Expr( |
515 | Context, Z3_mk_fpa_is_zero(Context.Context, toZ3Expr(*Exp).AST))); |
516 | } |
517 | |
518 | SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
519 | SMTExprRef RoundingMode = getFloatRoundingMode(); |
520 | return newExprRef( |
521 | Z3Expr(Context, |
522 | Z3_mk_fpa_mul(Context.Context, toZ3Expr(*RoundingMode).AST, |
523 | toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST))); |
524 | } |
525 | |
526 | SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
527 | SMTExprRef RoundingMode = getFloatRoundingMode(); |
528 | return newExprRef( |
529 | Z3Expr(Context, |
530 | Z3_mk_fpa_div(Context.Context, toZ3Expr(*RoundingMode).AST, |
531 | toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST))); |
532 | } |
533 | |
534 | SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
535 | return newExprRef( |
536 | Z3Expr(Context, Z3_mk_fpa_rem(Context.Context, toZ3Expr(*LHS).AST, |
537 | toZ3Expr(*RHS).AST))); |
538 | } |
539 | |
540 | SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
541 | SMTExprRef RoundingMode = getFloatRoundingMode(); |
542 | return newExprRef( |
543 | Z3Expr(Context, |
544 | Z3_mk_fpa_add(Context.Context, toZ3Expr(*RoundingMode).AST, |
545 | toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST))); |
546 | } |
547 | |
548 | SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
549 | SMTExprRef RoundingMode = getFloatRoundingMode(); |
550 | return newExprRef( |
551 | Z3Expr(Context, |
552 | Z3_mk_fpa_sub(Context.Context, toZ3Expr(*RoundingMode).AST, |
553 | toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST))); |
554 | } |
555 | |
556 | SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
557 | return newExprRef( |
558 | Z3Expr(Context, Z3_mk_fpa_lt(Context.Context, toZ3Expr(*LHS).AST, |
559 | toZ3Expr(*RHS).AST))); |
560 | } |
561 | |
562 | SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
563 | return newExprRef( |
564 | Z3Expr(Context, Z3_mk_fpa_gt(Context.Context, toZ3Expr(*LHS).AST, |
565 | toZ3Expr(*RHS).AST))); |
566 | } |
567 | |
568 | SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
569 | return newExprRef( |
570 | Z3Expr(Context, Z3_mk_fpa_leq(Context.Context, toZ3Expr(*LHS).AST, |
571 | toZ3Expr(*RHS).AST))); |
572 | } |
573 | |
574 | SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
575 | return newExprRef( |
576 | Z3Expr(Context, Z3_mk_fpa_geq(Context.Context, toZ3Expr(*LHS).AST, |
577 | toZ3Expr(*RHS).AST))); |
578 | } |
579 | |
580 | SMTExprRef mkFPEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
581 | return newExprRef( |
582 | Z3Expr(Context, Z3_mk_fpa_eq(Context.Context, toZ3Expr(*LHS).AST, |
583 | toZ3Expr(*RHS).AST))); |
584 | } |
585 | |
586 | SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T, |
587 | const SMTExprRef &F) override { |
588 | return newExprRef( |
589 | Z3Expr(Context, Z3_mk_ite(Context.Context, toZ3Expr(*Cond).AST, |
590 | toZ3Expr(*T).AST, toZ3Expr(*F).AST))); |
591 | } |
592 | |
593 | SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) override { |
594 | return newExprRef(Z3Expr( |
595 | Context, Z3_mk_sign_ext(Context.Context, i, toZ3Expr(*Exp).AST))); |
596 | } |
597 | |
598 | SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) override { |
599 | return newExprRef(Z3Expr( |
600 | Context, Z3_mk_zero_ext(Context.Context, i, toZ3Expr(*Exp).AST))); |
601 | } |
602 | |
603 | SMTExprRef mkBVExtract(unsigned High, unsigned Low, |
604 | const SMTExprRef &Exp) override { |
605 | return newExprRef(Z3Expr(Context, Z3_mk_extract(Context.Context, High, Low, |
606 | toZ3Expr(*Exp).AST))); |
607 | } |
608 | |
609 | /// Creates a predicate that checks for overflow in a bitvector addition |
610 | /// operation |
611 | SMTExprRef mkBVAddNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS, |
612 | bool isSigned) override { |
613 | return newExprRef(Z3Expr( |
614 | Context, Z3_mk_bvadd_no_overflow(Context.Context, toZ3Expr(*LHS).AST, |
615 | toZ3Expr(*RHS).AST, isSigned))); |
616 | } |
617 | |
618 | /// Creates a predicate that checks for underflow in a signed bitvector |
619 | /// addition operation |
620 | SMTExprRef mkBVAddNoUnderflow(const SMTExprRef &LHS, |
621 | const SMTExprRef &RHS) override { |
622 | return newExprRef(Z3Expr( |
623 | Context, Z3_mk_bvadd_no_underflow(Context.Context, toZ3Expr(*LHS).AST, |
624 | toZ3Expr(*RHS).AST))); |
625 | } |
626 | |
627 | /// Creates a predicate that checks for overflow in a signed bitvector |
628 | /// subtraction operation |
629 | SMTExprRef mkBVSubNoOverflow(const SMTExprRef &LHS, |
630 | const SMTExprRef &RHS) override { |
631 | return newExprRef(Z3Expr( |
632 | Context, Z3_mk_bvsub_no_overflow(Context.Context, toZ3Expr(*LHS).AST, |
633 | toZ3Expr(*RHS).AST))); |
634 | } |
635 | |
636 | /// Creates a predicate that checks for underflow in a bitvector subtraction |
637 | /// operation |
638 | SMTExprRef mkBVSubNoUnderflow(const SMTExprRef &LHS, const SMTExprRef &RHS, |
639 | bool isSigned) override { |
640 | return newExprRef(Z3Expr( |
641 | Context, Z3_mk_bvsub_no_underflow(Context.Context, toZ3Expr(*LHS).AST, |
642 | toZ3Expr(*RHS).AST, isSigned))); |
643 | } |
644 | |
645 | /// Creates a predicate that checks for overflow in a signed bitvector |
646 | /// division/modulus operation |
647 | SMTExprRef mkBVSDivNoOverflow(const SMTExprRef &LHS, |
648 | const SMTExprRef &RHS) override { |
649 | return newExprRef(Z3Expr( |
650 | Context, Z3_mk_bvsdiv_no_overflow(Context.Context, toZ3Expr(*LHS).AST, |
651 | toZ3Expr(*RHS).AST))); |
652 | } |
653 | |
654 | /// Creates a predicate that checks for overflow in a bitvector negation |
655 | /// operation |
656 | SMTExprRef mkBVNegNoOverflow(const SMTExprRef &Exp) override { |
657 | return newExprRef(Z3Expr( |
658 | Context, Z3_mk_bvneg_no_overflow(Context.Context, toZ3Expr(*Exp).AST))); |
659 | } |
660 | |
661 | /// Creates a predicate that checks for overflow in a bitvector multiplication |
662 | /// operation |
663 | SMTExprRef mkBVMulNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS, |
664 | bool isSigned) override { |
665 | return newExprRef(Z3Expr( |
666 | Context, Z3_mk_bvmul_no_overflow(Context.Context, toZ3Expr(*LHS).AST, |
667 | toZ3Expr(*RHS).AST, isSigned))); |
668 | } |
669 | |
670 | /// Creates a predicate that checks for underflow in a signed bitvector |
671 | /// multiplication operation |
672 | SMTExprRef mkBVMulNoUnderflow(const SMTExprRef &LHS, |
673 | const SMTExprRef &RHS) override { |
674 | return newExprRef(Z3Expr( |
675 | Context, Z3_mk_bvmul_no_underflow(Context.Context, toZ3Expr(*LHS).AST, |
676 | toZ3Expr(*RHS).AST))); |
677 | } |
678 | |
679 | SMTExprRef mkBVConcat(const SMTExprRef &LHS, const SMTExprRef &RHS) override { |
680 | return newExprRef( |
681 | Z3Expr(Context, Z3_mk_concat(Context.Context, toZ3Expr(*LHS).AST, |
682 | toZ3Expr(*RHS).AST))); |
683 | } |
684 | |
685 | SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) override { |
686 | SMTExprRef RoundingMode = getFloatRoundingMode(); |
687 | return newExprRef(Z3Expr( |
688 | Context, |
689 | Z3_mk_fpa_to_fp_float(Context.Context, toZ3Expr(*RoundingMode).AST, |
690 | toZ3Expr(*From).AST, toZ3Sort(*To).Sort))); |
691 | } |
692 | |
693 | SMTExprRef mkSBVtoFP(const SMTExprRef &From, const SMTSortRef &To) override { |
694 | SMTExprRef RoundingMode = getFloatRoundingMode(); |
695 | return newExprRef(Z3Expr( |
696 | Context, |
697 | Z3_mk_fpa_to_fp_signed(Context.Context, toZ3Expr(*RoundingMode).AST, |
698 | toZ3Expr(*From).AST, toZ3Sort(*To).Sort))); |
699 | } |
700 | |
701 | SMTExprRef mkUBVtoFP(const SMTExprRef &From, const SMTSortRef &To) override { |
702 | SMTExprRef RoundingMode = getFloatRoundingMode(); |
703 | return newExprRef(Z3Expr( |
704 | Context, |
705 | Z3_mk_fpa_to_fp_unsigned(Context.Context, toZ3Expr(*RoundingMode).AST, |
706 | toZ3Expr(*From).AST, toZ3Sort(*To).Sort))); |
707 | } |
708 | |
709 | SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth) override { |
710 | SMTExprRef RoundingMode = getFloatRoundingMode(); |
711 | return newExprRef(Z3Expr( |
712 | Context, Z3_mk_fpa_to_sbv(Context.Context, toZ3Expr(*RoundingMode).AST, |
713 | toZ3Expr(*From).AST, ToWidth))); |
714 | } |
715 | |
716 | SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth) override { |
717 | SMTExprRef RoundingMode = getFloatRoundingMode(); |
718 | return newExprRef(Z3Expr( |
719 | Context, Z3_mk_fpa_to_ubv(Context.Context, toZ3Expr(*RoundingMode).AST, |
720 | toZ3Expr(*From).AST, ToWidth))); |
721 | } |
722 | |
723 | SMTExprRef mkBoolean(const bool b) override { |
724 | return newExprRef(Z3Expr(Context, b ? Z3_mk_true(Context.Context) |
725 | : Z3_mk_false(Context.Context))); |
726 | } |
727 | |
728 | SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) override { |
729 | const Z3_sort Z3Sort = toZ3Sort(*getBitvectorSort(BitWidth)).Sort; |
730 | |
731 | // Slow path, when 64 bits are not enough. |
732 | if (LLVM_UNLIKELY(!Int.isRepresentableByInt64())) { |
733 | SmallString<40> Buffer; |
734 | Int.toString(Buffer, 10); |
735 | return newExprRef(Z3Expr( |
736 | Context, Z3_mk_numeral(Context.Context, Buffer.c_str(), Z3Sort))); |
737 | } |
738 | |
739 | const int64_t BitReprAsSigned = Int.getExtValue(); |
740 | const uint64_t BitReprAsUnsigned = |
741 | reinterpret_cast<const uint64_t &>(BitReprAsSigned); |
742 | |
743 | Z3_ast Literal = |
744 | Int.isSigned() |
745 | ? Z3_mk_int64(Context.Context, BitReprAsSigned, Z3Sort) |
746 | : Z3_mk_unsigned_int64(Context.Context, BitReprAsUnsigned, Z3Sort); |
747 | return newExprRef(Z3Expr(Context, Literal)); |
748 | } |
749 | |
750 | SMTExprRef mkFloat(const llvm::APFloat Float) override { |
751 | SMTSortRef Sort = |
752 | getFloatSort(llvm::APFloat::semanticsSizeInBits(Float.getSemantics())); |
753 | |
754 | llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), false); |
755 | SMTExprRef Z3Int = mkBitvector(Int, Int.getBitWidth()); |
756 | return newExprRef(Z3Expr( |
757 | Context, Z3_mk_fpa_to_fp_bv(Context.Context, toZ3Expr(*Z3Int).AST, |
758 | toZ3Sort(*Sort).Sort))); |
759 | } |
760 | |
761 | SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) override { |
762 | return newExprRef( |
763 | Z3Expr(Context, Z3_mk_const(Context.Context, |
764 | Z3_mk_string_symbol(Context.Context, Name), |
765 | toZ3Sort(*Sort).Sort))); |
766 | } |
767 | |
768 | llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth, |
769 | bool isUnsigned) override { |
770 | return llvm::APSInt( |
771 | llvm::APInt(BitWidth, |
772 | Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST), |
773 | 10), |
774 | isUnsigned); |
775 | } |
776 | |
777 | bool getBoolean(const SMTExprRef &Exp) override { |
778 | return Z3_get_bool_value(Context.Context, toZ3Expr(*Exp).AST) == Z3_L_TRUE; |
779 | } |
780 | |
781 | SMTExprRef getFloatRoundingMode() override { |
782 | // TODO: Don't assume nearest ties to even rounding mode |
783 | return newExprRef(Z3Expr(Context, Z3_mk_fpa_rne(Context.Context))); |
784 | } |
785 | |
786 | bool toAPFloat(const SMTSortRef &Sort, const SMTExprRef &AST, |
787 | llvm::APFloat &Float, bool useSemantics) { |
788 | assert(Sort->isFloatSort() && "Unsupported sort to floating-point!" ); |
789 | |
790 | llvm::APSInt Int(Sort->getFloatSortSize(), true); |
791 | const llvm::fltSemantics &Semantics = |
792 | getFloatSemantics(Sort->getFloatSortSize()); |
793 | SMTSortRef BVSort = getBitvectorSort(Sort->getFloatSortSize()); |
794 | if (!toAPSInt(BVSort, AST, Int, true)) { |
795 | return false; |
796 | } |
797 | |
798 | if (useSemantics && !areEquivalent(Float.getSemantics(), Semantics)) { |
799 | assert(false && "Floating-point types don't match!" ); |
800 | return false; |
801 | } |
802 | |
803 | Float = llvm::APFloat(Semantics, Int); |
804 | return true; |
805 | } |
806 | |
807 | bool toAPSInt(const SMTSortRef &Sort, const SMTExprRef &AST, |
808 | llvm::APSInt &Int, bool useSemantics) { |
809 | if (Sort->isBitvectorSort()) { |
810 | if (useSemantics && Int.getBitWidth() != Sort->getBitvectorSortSize()) { |
811 | assert(false && "Bitvector types don't match!" ); |
812 | return false; |
813 | } |
814 | |
815 | // FIXME: This function is also used to retrieve floating-point values, |
816 | // which can be 16, 32, 64 or 128 bits long. Bitvectors can be anything |
817 | // between 1 and 64 bits long, which is the reason we have this weird |
818 | // guard. In the future, we need proper calls in the backend to retrieve |
819 | // floating-points and its special values (NaN, +/-infinity, +/-zero), |
820 | // then we can drop this weird condition. |
821 | if (Sort->getBitvectorSortSize() <= 64 || |
822 | Sort->getBitvectorSortSize() == 128) { |
823 | Int = getBitvector(AST, Int.getBitWidth(), Int.isUnsigned()); |
824 | return true; |
825 | } |
826 | |
827 | assert(false && "Bitwidth not supported!" ); |
828 | return false; |
829 | } |
830 | |
831 | if (Sort->isBooleanSort()) { |
832 | if (useSemantics && Int.getBitWidth() < 1) { |
833 | assert(false && "Boolean type doesn't match!" ); |
834 | return false; |
835 | } |
836 | |
837 | Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), getBoolean(AST)), |
838 | Int.isUnsigned()); |
839 | return true; |
840 | } |
841 | |
842 | llvm_unreachable("Unsupported sort to integer!" ); |
843 | } |
844 | |
845 | bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) override { |
846 | Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver)); |
847 | Z3_func_decl Func = Z3_get_app_decl( |
848 | Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST)); |
849 | if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE) |
850 | return false; |
851 | |
852 | SMTExprRef Assign = newExprRef( |
853 | Z3Expr(Context, |
854 | Z3_model_get_const_interp(Context.Context, Model.Model, Func))); |
855 | SMTSortRef Sort = getSort(Assign); |
856 | return toAPSInt(Sort, Assign, Int, true); |
857 | } |
858 | |
859 | bool getInterpretation(const SMTExprRef &Exp, llvm::APFloat &Float) override { |
860 | Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver)); |
861 | Z3_func_decl Func = Z3_get_app_decl( |
862 | Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST)); |
863 | if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE) |
864 | return false; |
865 | |
866 | SMTExprRef Assign = newExprRef( |
867 | Z3Expr(Context, |
868 | Z3_model_get_const_interp(Context.Context, Model.Model, Func))); |
869 | SMTSortRef Sort = getSort(Assign); |
870 | return toAPFloat(Sort, Assign, Float, true); |
871 | } |
872 | |
873 | std::optional<bool> check() const override { |
874 | Z3_lbool res = Z3_solver_check(Context.Context, Solver); |
875 | if (res == Z3_L_TRUE) |
876 | return true; |
877 | |
878 | if (res == Z3_L_FALSE) |
879 | return false; |
880 | |
881 | return std::nullopt; |
882 | } |
883 | |
884 | void push() override { return Z3_solver_push(Context.Context, Solver); } |
885 | |
886 | void pop(unsigned NumStates = 1) override { |
887 | assert(Z3_solver_get_num_scopes(Context.Context, Solver) >= NumStates); |
888 | return Z3_solver_pop(Context.Context, Solver, NumStates); |
889 | } |
890 | |
891 | bool isFPSupported() override { return true; } |
892 | |
893 | /// Reset the solver and remove all constraints. |
894 | void reset() override { Z3_solver_reset(Context.Context, Solver); } |
895 | |
896 | void print(raw_ostream &OS) const override { |
897 | OS << Z3_solver_to_string(Context.Context, Solver); |
898 | } |
899 | }; // end class Z3Solver |
900 | |
901 | } // end anonymous namespace |
902 | |
903 | #endif |
904 | |
905 | llvm::SMTSolverRef llvm::CreateZ3Solver() { |
906 | #if LLVM_WITH_Z3 |
907 | return std::make_unique<Z3Solver>(); |
908 | #else |
909 | llvm::report_fatal_error(reason: "LLVM was not compiled with Z3 support, rebuild " |
910 | "with -DLLVM_ENABLE_Z3_SOLVER=ON" , |
911 | gen_crash_diag: false); |
912 | return nullptr; |
913 | #endif |
914 | } |
915 | |
916 | LLVM_DUMP_METHOD void SMTSort::dump() const { print(OS&: llvm::errs()); } |
917 | LLVM_DUMP_METHOD void SMTExpr::dump() const { print(OS&: llvm::errs()); } |
918 | LLVM_DUMP_METHOD void SMTSolver::dump() const { print(OS&: llvm::errs()); } |
919 | |