9#include "llvm/Config/config.h"
27 friend class Z3Context;
32 Z3Config() :
Config(Z3_mk_config()) {
34 Z3_set_param_value(
Config,
"model",
"true");
36 Z3_set_param_value(
Config,
"proof",
"false");
38 Z3_set_param_value(
Config,
"timeout",
"15000");
41 ~Z3Config() { Z3_del_config(
Config); }
45void Z3ErrorHandler(Z3_context Context, Z3_error_code
Error) {
59 Z3_set_error_handler(Context, Z3ErrorHandler);
62 virtual ~Z3Context() {
63 Z3_del_context(Context);
70 friend class Z3Solver;
78 Z3Sort(Z3Context &
C, Z3_sort ZS) :
Context(
C), Sort(ZS) {
79 Z3_inc_ref(
Context.Context,
reinterpret_cast<Z3_ast
>(Sort));
84 Z3_inc_ref(
Context.Context,
reinterpret_cast<Z3_ast
>(Sort));
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));
96 Z3Sort(Z3Sort &&
Other) =
delete;
97 Z3Sort &operator=(Z3Sort &&
Other) =
delete;
101 Z3_dec_ref(
Context.Context,
reinterpret_cast<Z3_ast
>(Sort));
106 Z3_get_ast_id(
Context.Context,
reinterpret_cast<Z3_ast
>(Sort)));
109 bool isBitvectorSortImpl()
const override {
110 return (Z3_get_sort_kind(
Context.Context, Sort) == Z3_BV_SORT);
113 bool isFloatSortImpl()
const override {
114 return (Z3_get_sort_kind(
Context.Context, Sort) == Z3_FLOATING_POINT_SORT);
117 bool isBooleanSortImpl()
const override {
118 return (Z3_get_sort_kind(
Context.Context, Sort) == Z3_BOOL_SORT);
121 unsigned getBitvectorSortSizeImpl()
const override {
122 return Z3_get_bv_sort_size(
Context.Context, Sort);
125 unsigned getFloatSortSizeImpl()
const override {
126 return Z3_fpa_get_ebits(
Context.Context, Sort) +
127 Z3_fpa_get_sbits(
Context.Context, Sort);
131 return Z3_is_eq_sort(
Context.Context, Sort,
132 static_cast<const Z3Sort &
>(
Other).Sort);
136 OS << Z3_sort_to_string(
Context.Context, Sort);
140static const Z3Sort &toZ3Sort(
const SMTSort &S) {
141 return static_cast<const Z3Sort &
>(S);
145 friend class Z3Solver;
153 Z3_inc_ref(
Context.Context, AST);
158 Z3_inc_ref(
Context.Context, AST);
163 Z3Expr &operator=(
const Z3Expr &
Other) {
165 Z3_dec_ref(
Context.Context, AST);
170 Z3Expr(Z3Expr &&
Other) =
delete;
171 Z3Expr &operator=(Z3Expr &&
Other) =
delete;
175 Z3_dec_ref(
Context.Context, AST);
179 ID.AddInteger(Z3_get_ast_id(
Context.Context, AST));
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);
193 OS << Z3_ast_to_string(
Context.Context, AST);
197static const Z3Expr &toZ3Expr(
const SMTExpr &
E) {
198 return static_cast<const Z3Expr &
>(
E);
202 friend class Z3Solver;
210 Z3_model_inc_ref(
Context.Context, Model);
213 Z3Model(
const Z3Model &
Other) =
delete;
214 Z3Model(Z3Model &&
Other) =
delete;
215 Z3Model &operator=(Z3Model &
Other) =
delete;
216 Z3Model &operator=(Z3Model &&
Other) =
delete;
220 Z3_model_dec_ref(
Context.Context, Model);
224 OS << Z3_model_to_string(
Context.Context, Model);
261 friend class Z3ConstraintManager;
268 std::set<Z3Sort> CachedSorts;
271 std::set<Z3Expr> CachedExprs;
275 Z3_solver_inc_ref(
Context.Context, Solver);
278 Z3Solver(
const Z3Solver &
Other) =
delete;
279 Z3Solver(Z3Solver &&
Other) =
delete;
280 Z3Solver &operator=(Z3Solver &
Other) =
delete;
281 Z3Solver &operator=(Z3Solver &&
Other) =
delete;
285 Z3_solver_dec_ref(
Context.Context, Solver);
288 void addConstraint(
const SMTExprRef &Exp)
const override {
289 Z3_solver_assert(
Context.Context, Solver, toZ3Expr(*Exp).AST);
295 auto It = CachedSorts.insert(toZ3Sort(Sort));
302 auto It = CachedExprs.insert(toZ3Expr(Exp));
307 return newSortRef(Z3Sort(Context, Z3_mk_bool_sort(
Context.Context)));
317 Z3Sort(Context, Z3_get_sort(
Context.Context, toZ3Expr(*Exp).AST)));
321 return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_16(
Context.Context)));
325 return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_32(
Context.Context)));
329 return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_64(
Context.Context)));
333 return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_128(
Context.Context)));
338 Z3Expr(Context, Z3_mk_bvneg(
Context.Context, toZ3Expr(*Exp).AST)));
343 Z3Expr(Context, Z3_mk_bvnot(
Context.Context, toZ3Expr(*Exp).AST)));
348 Z3Expr(Context, Z3_mk_not(
Context.Context, toZ3Expr(*Exp).AST)));
353 Z3Expr(Context, Z3_mk_bvadd(
Context.Context, toZ3Expr(*LHS).AST,
354 toZ3Expr(*RHS).AST)));
359 Z3Expr(Context, Z3_mk_bvsub(
Context.Context, toZ3Expr(*LHS).AST,
360 toZ3Expr(*RHS).AST)));
365 Z3Expr(Context, Z3_mk_bvmul(
Context.Context, toZ3Expr(*LHS).AST,
366 toZ3Expr(*RHS).AST)));
371 Z3Expr(Context, Z3_mk_bvsrem(
Context.Context, toZ3Expr(*LHS).AST,
372 toZ3Expr(*RHS).AST)));
377 Z3Expr(Context, Z3_mk_bvurem(
Context.Context, toZ3Expr(*LHS).AST,
378 toZ3Expr(*RHS).AST)));
383 Z3Expr(Context, Z3_mk_bvsdiv(
Context.Context, toZ3Expr(*LHS).AST,
384 toZ3Expr(*RHS).AST)));
389 Z3Expr(Context, Z3_mk_bvudiv(
Context.Context, toZ3Expr(*LHS).AST,
390 toZ3Expr(*RHS).AST)));
395 Z3Expr(Context, Z3_mk_bvshl(
Context.Context, toZ3Expr(*LHS).AST,
396 toZ3Expr(*RHS).AST)));
401 Z3Expr(Context, Z3_mk_bvashr(
Context.Context, toZ3Expr(*LHS).AST,
402 toZ3Expr(*RHS).AST)));
407 Z3Expr(Context, Z3_mk_bvlshr(
Context.Context, toZ3Expr(*LHS).AST,
408 toZ3Expr(*RHS).AST)));
413 Z3Expr(Context, Z3_mk_bvxor(
Context.Context, toZ3Expr(*LHS).AST,
414 toZ3Expr(*RHS).AST)));
419 Z3Expr(Context, Z3_mk_bvor(
Context.Context, toZ3Expr(*LHS).AST,
420 toZ3Expr(*RHS).AST)));
425 Z3Expr(Context, Z3_mk_bvand(
Context.Context, toZ3Expr(*LHS).AST,
426 toZ3Expr(*RHS).AST)));
431 Z3Expr(Context, Z3_mk_bvult(
Context.Context, toZ3Expr(*LHS).AST,
432 toZ3Expr(*RHS).AST)));
437 Z3Expr(Context, Z3_mk_bvslt(
Context.Context, toZ3Expr(*LHS).AST,
438 toZ3Expr(*RHS).AST)));
443 Z3Expr(Context, Z3_mk_bvugt(
Context.Context, toZ3Expr(*LHS).AST,
444 toZ3Expr(*RHS).AST)));
449 Z3Expr(Context, Z3_mk_bvsgt(
Context.Context, toZ3Expr(*LHS).AST,
450 toZ3Expr(*RHS).AST)));
455 Z3Expr(Context, Z3_mk_bvule(
Context.Context, toZ3Expr(*LHS).AST,
456 toZ3Expr(*RHS).AST)));
461 Z3Expr(Context, Z3_mk_bvsle(
Context.Context, toZ3Expr(*LHS).AST,
462 toZ3Expr(*RHS).AST)));
467 Z3Expr(Context, Z3_mk_bvuge(
Context.Context, toZ3Expr(*LHS).AST,
468 toZ3Expr(*RHS).AST)));
473 Z3Expr(Context, Z3_mk_bvsge(
Context.Context, toZ3Expr(*LHS).AST,
474 toZ3Expr(*RHS).AST)));
478 Z3_ast
Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST};
479 return newExprRef(Z3Expr(Context, Z3_mk_and(
Context.Context, 2, Args)));
483 Z3_ast
Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST};
484 return newExprRef(Z3Expr(Context, Z3_mk_or(
Context.Context, 2, Args)));
489 Z3Expr(Context, Z3_mk_eq(
Context.Context, toZ3Expr(*LHS).AST,
490 toZ3Expr(*RHS).AST)));
495 Z3Expr(Context, Z3_mk_fpa_neg(
Context.Context, toZ3Expr(*Exp).AST)));
499 return newExprRef(Z3Expr(
500 Context, Z3_mk_fpa_is_infinite(
Context.Context, toZ3Expr(*Exp).AST)));
505 Z3Expr(Context, Z3_mk_fpa_is_nan(
Context.Context, toZ3Expr(*Exp).AST)));
509 return newExprRef(Z3Expr(
510 Context, Z3_mk_fpa_is_normal(
Context.Context, toZ3Expr(*Exp).AST)));
514 return newExprRef(Z3Expr(
515 Context, Z3_mk_fpa_is_zero(
Context.Context, toZ3Expr(*Exp).AST)));
522 Z3_mk_fpa_mul(
Context.Context, toZ3Expr(*RoundingMode).AST,
523 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
530 Z3_mk_fpa_div(
Context.Context, toZ3Expr(*RoundingMode).AST,
531 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
536 Z3Expr(Context, Z3_mk_fpa_rem(
Context.Context, toZ3Expr(*LHS).AST,
537 toZ3Expr(*RHS).AST)));
544 Z3_mk_fpa_add(
Context.Context, toZ3Expr(*RoundingMode).AST,
545 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
552 Z3_mk_fpa_sub(
Context.Context, toZ3Expr(*RoundingMode).AST,
553 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
558 Z3Expr(Context, Z3_mk_fpa_lt(
Context.Context, toZ3Expr(*LHS).AST,
559 toZ3Expr(*RHS).AST)));
564 Z3Expr(Context, Z3_mk_fpa_gt(
Context.Context, toZ3Expr(*LHS).AST,
565 toZ3Expr(*RHS).AST)));
570 Z3Expr(Context, Z3_mk_fpa_leq(
Context.Context, toZ3Expr(*LHS).AST,
571 toZ3Expr(*RHS).AST)));
576 Z3Expr(Context, Z3_mk_fpa_geq(
Context.Context, toZ3Expr(*LHS).AST,
577 toZ3Expr(*RHS).AST)));
582 Z3Expr(Context, Z3_mk_fpa_eq(
Context.Context, toZ3Expr(*LHS).AST,
583 toZ3Expr(*RHS).AST)));
589 Z3Expr(Context, Z3_mk_ite(
Context.Context, toZ3Expr(*Cond).AST,
590 toZ3Expr(*T).AST, toZ3Expr(*F).AST)));
594 return newExprRef(Z3Expr(
595 Context, Z3_mk_sign_ext(
Context.Context, i, toZ3Expr(*Exp).AST)));
599 return newExprRef(Z3Expr(
600 Context, Z3_mk_zero_ext(
Context.Context, i, toZ3Expr(*Exp).AST)));
605 return newExprRef(Z3Expr(Context, Z3_mk_extract(
Context.Context,
High,
Low,
606 toZ3Expr(*Exp).AST)));
613 return newExprRef(Z3Expr(
614 Context, Z3_mk_bvadd_no_overflow(
Context.Context, toZ3Expr(*LHS).AST,
622 return newExprRef(Z3Expr(
623 Context, Z3_mk_bvadd_no_underflow(
Context.Context, toZ3Expr(*LHS).AST,
624 toZ3Expr(*RHS).AST)));
631 return newExprRef(Z3Expr(
632 Context, Z3_mk_bvsub_no_overflow(
Context.Context, toZ3Expr(*LHS).AST,
633 toZ3Expr(*RHS).AST)));
640 return newExprRef(Z3Expr(
641 Context, Z3_mk_bvsub_no_underflow(
Context.Context, toZ3Expr(*LHS).AST,
649 return newExprRef(Z3Expr(
650 Context, Z3_mk_bvsdiv_no_overflow(
Context.Context, toZ3Expr(*LHS).AST,
651 toZ3Expr(*RHS).AST)));
657 return newExprRef(Z3Expr(
658 Context, Z3_mk_bvneg_no_overflow(
Context.Context, toZ3Expr(*Exp).AST)));
665 return newExprRef(Z3Expr(
666 Context, Z3_mk_bvmul_no_overflow(
Context.Context, toZ3Expr(*LHS).AST,
674 return newExprRef(Z3Expr(
675 Context, Z3_mk_bvmul_no_underflow(
Context.Context, toZ3Expr(*LHS).AST,
676 toZ3Expr(*RHS).AST)));
681 Z3Expr(Context, Z3_mk_concat(
Context.Context, toZ3Expr(*LHS).AST,
682 toZ3Expr(*RHS).AST)));
687 return newExprRef(Z3Expr(
689 Z3_mk_fpa_to_fp_float(
Context.Context, toZ3Expr(*RoundingMode).AST,
690 toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
695 return newExprRef(Z3Expr(
697 Z3_mk_fpa_to_fp_signed(
Context.Context, toZ3Expr(*RoundingMode).AST,
698 toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
703 return newExprRef(Z3Expr(
705 Z3_mk_fpa_to_fp_unsigned(
Context.Context, toZ3Expr(*RoundingMode).AST,
706 toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
711 return newExprRef(Z3Expr(
712 Context, Z3_mk_fpa_to_sbv(
Context.Context, toZ3Expr(*RoundingMode).AST,
713 toZ3Expr(*From).AST, ToWidth)));
718 return newExprRef(Z3Expr(
719 Context, Z3_mk_fpa_to_ubv(
Context.Context, toZ3Expr(*RoundingMode).AST,
720 toZ3Expr(*From).AST, ToWidth)));
724 return newExprRef(Z3Expr(Context, b ? Z3_mk_true(
Context.Context)
725 : Z3_mk_false(
Context.Context)));
729 const Z3_sort Z3Sort = toZ3Sort(*getBitvectorSort(
BitWidth)).Sort;
734 Int.toString(Buffer, 10);
735 return newExprRef(Z3Expr(
736 Context, Z3_mk_numeral(
Context.Context, Buffer.
c_str(), Z3Sort)));
739 const int64_t BitReprAsSigned =
Int.getExtValue();
741 reinterpret_cast<const uint64_t &
>(BitReprAsSigned);
745 ? Z3_mk_int64(
Context.Context, BitReprAsSigned, Z3Sort)
746 : Z3_mk_unsigned_int64(
Context.
Context, BitReprAsUnsigned, Z3Sort);
747 return newExprRef(Z3Expr(Context,
Literal));
756 return newExprRef(Z3Expr(
757 Context, Z3_mk_fpa_to_fp_bv(
Context.Context, toZ3Expr(*Z3Int).AST,
758 toZ3Sort(*Sort).Sort)));
763 Z3Expr(Context, Z3_mk_const(
Context.Context,
765 toZ3Sort(*Sort).Sort)));
769 bool isUnsigned)
override {
772 Z3_get_numeral_string(
Context.Context, toZ3Expr(*Exp).AST),
777 bool getBoolean(
const SMTExprRef &Exp)
override {
778 return Z3_get_bool_value(
Context.Context, toZ3Expr(*Exp).AST) == Z3_L_TRUE;
783 return newExprRef(Z3Expr(Context, Z3_mk_fpa_rne(
Context.Context)));
794 if (!toAPSInt(BVSort, AST,
Int,
true)) {
798 if (useSemantics && !areEquivalent(
Float.getSemantics(), Semantics)) {
799 assert(
false &&
"Floating-point types don't match!");
811 assert(
false &&
"Bitvector types don't match!");
823 Int = getBitvector(AST,
Int.getBitWidth(),
Int.isUnsigned());
827 assert(
false &&
"Bitwidth not supported!");
832 if (useSemantics &&
Int.getBitWidth() < 1) {
833 assert(
false &&
"Boolean type doesn't match!");
846 Z3Model
Model(Context, Z3_solver_get_model(
Context.Context, Solver));
847 Z3_func_decl
Func = Z3_get_app_decl(
849 if (Z3_model_has_interp(
Context.Context,
Model.Model, Func) != Z3_L_TRUE)
854 Z3_model_get_const_interp(
Context.Context,
Model.Model, Func)));
856 return toAPSInt(Sort, Assign,
Int,
true);
860 Z3Model
Model(Context, Z3_solver_get_model(
Context.Context, Solver));
861 Z3_func_decl
Func = Z3_get_app_decl(
863 if (Z3_model_has_interp(
Context.Context,
Model.Model, Func) != Z3_L_TRUE)
868 Z3_model_get_const_interp(
Context.Context,
Model.Model, Func)));
870 return toAPFloat(Sort, Assign, Float,
true);
873 std::optional<bool>
check()
const override {
874 Z3_lbool res = Z3_solver_check(
Context.Context, Solver);
875 if (res == Z3_L_TRUE)
878 if (res == Z3_L_FALSE)
884 void push()
override {
return Z3_solver_push(
Context.Context, Solver); }
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);
891 bool isFPSupported()
override {
return true; }
894 void reset()
override { Z3_solver_reset(
Context.Context, Solver); }
897 OS << Z3_solver_to_string(
Context.Context, Solver);
907 return std::make_unique<Z3Solver>();
910 "with -DLLVM_ENABLE_Z3_SOLVER=ON",
static void print(raw_ostream &Out, object::Archive::Kind Kind, T Val)
SmallVector< MachineOperand, 4 > Cond
BlockVerifier::State From
static GCRegistry::Add< CoreCLRGC > E("coreclr", "CoreCLR-compatible GC")
#define LLVM_UNLIKELY(EXPR)
#define LLVM_DUMP_METHOD
Mark debug helper function definitions like dump() that should not be stripped from debug builds.
std::optional< std::vector< StOtherPiece > > Other
static bool isSigned(unsigned int Opcode)
assert(ImpDefSCC.getReg()==AMDGPU::SCC &&ImpDefSCC.isDef())
This file defines the SmallString class.
Class for arbitrary precision integers.
An arbitrary precision integer that knows its signedness.
Lightweight error class with error context and mandatory checking.
FoldingSetNodeID - This class is used to gather all the unique data bits of a node.
Generic base class for SMT exprs.
LLVM_DUMP_METHOD void dump() const
virtual void print(raw_ostream &OS) const =0
Generic base class for SMT Solvers.
virtual void print(raw_ostream &OS) const =0
LLVM_DUMP_METHOD void dump() const
Generic base class for SMT sorts.
virtual void print(raw_ostream &OS) const =0
virtual bool isBitvectorSort() const
Returns true if the sort is a bitvector, calls isBitvectorSortImpl().
virtual bool isFloatSort() const
Returns true if the sort is a floating-point, calls isFloatSortImpl().
virtual unsigned getFloatSortSize() const
Returns the floating-point size, fails if the sort is not a floating-point Calls getFloatSortSizeImpl...
virtual unsigned getBitvectorSortSize() const
Returns the bitvector size, fails if the sort is not a bitvector Calls getBitvectorSortSizeImpl().
virtual bool isBooleanSort() const
Returns true if the sort is a boolean, calls isBooleanSortImpl().
LLVM_DUMP_METHOD void dump() const
SmallString - A SmallString is just a SmallVector with methods and accessors that make it work better...
Twine - A lightweight data structure for efficiently representing the concatenation of temporary valu...
This class implements an extremely fast bulk output stream that can only output to a stream.
#define llvm_unreachable(msg)
Marks that the current location is not supposed to be reachable.
constexpr char Args[]
Key for Kernel::Metadata::mArgs.
@ C
The default llvm calling convention, compatible with C.
NodeAddr< FuncNode * > Func
This is an optimization pass for GlobalISel generic memory operations.
void dump(const SparseBitVector< ElementSize > &LHS, raw_ostream &out)
@ Low
Lower the current thread's priority such that it does not affect foreground tasks significantly.
void report_fatal_error(Error Err, bool gen_crash_diag=true)
Report a serious error, calling any installed error handler.
raw_fd_ostream & errs()
This returns a reference to a raw_ostream for standard error.
RoundingMode
Rounding mode.
constexpr unsigned BitWidth
std::shared_ptr< SMTSolver > SMTSolverRef
Shared pointer for SMTSolvers.
SMTSolverRef CreateZ3Solver()
Convenience method to create and Z3Solver object.
static const fltSemantics & IEEEsingle() LLVM_READNONE
static ExponentType semanticsMinExponent(const fltSemantics &)
static unsigned int semanticsSizeInBits(const fltSemantics &)
static const fltSemantics & IEEEquad() LLVM_READNONE
static ExponentType semanticsMaxExponent(const fltSemantics &)
static unsigned int semanticsPrecision(const fltSemantics &)
static const fltSemantics & IEEEdouble() LLVM_READNONE
static const fltSemantics & IEEEhalf() LLVM_READNONE