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