OSchip
/
llvm-project
mirror of https://github.com/THU-DSP-LAB/llvm-project.git
13
0
Fork 6
Code Issues Packages Projects Releases Wiki Activity
llvm-project/llvm/lib/Support/Z3Solver.cpp

919 lines
31 KiB
C++
Raw Blame History

//== Z3Solver.cpp -----------------------------------------------*- C++ -*--==//
//
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
// See https://llvm.org/LICENSE.txt for license information.
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
//
//===----------------------------------------------------------------------===//
#include "llvm/Config/config.h"
#include "llvm/Support/SMTAPI.h"
using namespace llvm;
#if LLVM_WITH_Z3
#include "llvm/ADT/SmallString.h"
#include "llvm/ADT/Twine.h"
#include <set>
#include <z3.h>
namespace {
/// Configuration class for Z3
class Z3Config {
friend class Z3Context;
Z3_config Config;
public:
Z3Config() : Config(Z3_mk_config()) {
// Enable model finding
Z3_set_param_value(Config, "model", "true");
// Disable proof generation
Z3_set_param_value(Config, "proof", "false");
// Set timeout to 15000ms = 15s
Z3_set_param_value(Config, "timeout", "15000");
}
~Z3Config() { Z3_del_config(Config); }
}; // end class Z3Config
// Function used to report errors
void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) {
llvm::report_fatal_error("Z3 error: " +
llvm::Twine(Z3_get_error_msg(Context, Error)));
}
/// Wrapper for Z3 context
class Z3Context {
public:
Z3_context Context;
Z3Context() {
Context = Z3_mk_context_rc(Z3Config().Config);
// The error function is set here because the context is the first object
// created by the backend
Z3_set_error_handler(Context, Z3ErrorHandler);
}
virtual ~Z3Context() {
Z3_del_context(Context);
Context = nullptr;
}
}; // end class Z3Context
/// Wrapper for Z3 Sort
class Z3Sort : public SMTSort {
friend class Z3Solver;
Z3Context &Context;
Z3_sort Sort;
public:
/// Default constructor, mainly used by make_shared
Z3Sort(Z3Context &C, Z3_sort ZS) : Context(C), Sort(ZS) {
Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
}
/// Override implicit copy constructor for correct reference counting.
Z3Sort(const Z3Sort &Other) : Context(Other.Context), Sort(Other.Sort) {
Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
}
/// Override implicit copy assignment constructor for correct reference
/// counting.
Z3Sort &operator=(const Z3Sort &Other) {
Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Other.Sort));
Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
Sort = Other.Sort;
return *this;
}
Z3Sort(Z3Sort &&Other) = delete;
Z3Sort &operator=(Z3Sort &&Other) = delete;
~Z3Sort() {
if (Sort)
Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
}
void Profile(llvm::FoldingSetNodeID &ID) const override {
ID.AddInteger(
Z3_get_ast_id(Context.Context, reinterpret_cast<Z3_ast>(Sort)));
}
bool isBitvectorSortImpl() const override {
return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BV_SORT);
}
bool isFloatSortImpl() const override {
return (Z3_get_sort_kind(Context.Context, Sort) == Z3_FLOATING_POINT_SORT);
}
bool isBooleanSortImpl() const override {
return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BOOL_SORT);
}
unsigned getBitvectorSortSizeImpl() const override {
return Z3_get_bv_sort_size(Context.Context, Sort);
}
unsigned getFloatSortSizeImpl() const override {
return Z3_fpa_get_ebits(Context.Context, Sort) +
Z3_fpa_get_sbits(Context.Context, Sort);
}
bool equal_to(SMTSort const &Other) const override {
return Z3_is_eq_sort(Context.Context, Sort,
static_cast<const Z3Sort &>(Other).Sort);
}
void print(raw_ostream &OS) const override {
OS << Z3_sort_to_string(Context.Context, Sort);
}
}; // end class Z3Sort
static const Z3Sort &toZ3Sort(const SMTSort &S) {
return static_cast<const Z3Sort &>(S);
}
class Z3Expr : public SMTExpr {
friend class Z3Solver;
Z3Context &Context;
Z3_ast AST;
public:
Z3Expr(Z3Context &C, Z3_ast ZA) : SMTExpr(), Context(C), AST(ZA) {
Z3_inc_ref(Context.Context, AST);
}
/// Override implicit copy constructor for correct reference counting.
Z3Expr(const Z3Expr &Copy) : SMTExpr(), Context(Copy.Context), AST(Copy.AST) {
Z3_inc_ref(Context.Context, AST);
}
/// Override implicit copy assignment constructor for correct reference
/// counting.
Z3Expr &operator=(const Z3Expr &Other) {
Z3_inc_ref(Context.Context, Other.AST);
Z3_dec_ref(Context.Context, AST);
AST = Other.AST;
return *this;
}
Z3Expr(Z3Expr &&Other) = delete;
Z3Expr &operator=(Z3Expr &&Other) = delete;
~Z3Expr() {
if (AST)
Z3_dec_ref(Context.Context, AST);
}
void Profile(llvm::FoldingSetNodeID &ID) const override {
ID.AddInteger(Z3_get_ast_id(Context.Context, AST));
}
/// Comparison of AST equality, not model equivalence.
bool equal_to(SMTExpr const &Other) const override {
assert(Z3_is_eq_sort(Context.Context, Z3_get_sort(Context.Context, AST),
Z3_get_sort(Context.Context,
static_cast<const Z3Expr &>(Other).AST)) &&
"AST's must have the same sort");
return Z3_is_eq_ast(Context.Context, AST,
static_cast<const Z3Expr &>(Other).AST);
}
void print(raw_ostream &OS) const override {
OS << Z3_ast_to_string(Context.Context, AST);
}
}; // end class Z3Expr
static const Z3Expr &toZ3Expr(const SMTExpr &E) {
return static_cast<const Z3Expr &>(E);
}
class Z3Model {
friend class Z3Solver;
Z3Context &Context;
Z3_model Model;
public:
Z3Model(Z3Context &C, Z3_model ZM) : Context(C), Model(ZM) {
Z3_model_inc_ref(Context.Context, Model);
}
Z3Model(const Z3Model &Other) = delete;
Z3Model(Z3Model &&Other) = delete;
Z3Model &operator=(Z3Model &Other) = delete;
Z3Model &operator=(Z3Model &&Other) = delete;
~Z3Model() {
if (Model)
Z3_model_dec_ref(Context.Context, Model);
}
void print(raw_ostream &OS) const {
OS << Z3_model_to_string(Context.Context, Model);
}
LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
}; // end class Z3Model
/// Get the corresponding IEEE floating-point type for a given bitwidth.
static const llvm::fltSemantics &getFloatSemantics(unsigned BitWidth) {
switch (BitWidth) {
default:
llvm_unreachable("Unsupported floating-point semantics!");
break;
case 16:
return llvm::APFloat::IEEEhalf();
case 32:
return llvm::APFloat::IEEEsingle();
case 64:
return llvm::APFloat::IEEEdouble();
case 128:
return llvm::APFloat::IEEEquad();
}
}
// Determine whether two float semantics are equivalent
static bool areEquivalent(const llvm::fltSemantics &LHS,
const llvm::fltSemantics &RHS) {
return (llvm::APFloat::semanticsPrecision(LHS) ==
llvm::APFloat::semanticsPrecision(RHS)) &&
(llvm::APFloat::semanticsMinExponent(LHS) ==
llvm::APFloat::semanticsMinExponent(RHS)) &&
(llvm::APFloat::semanticsMaxExponent(LHS) ==
llvm::APFloat::semanticsMaxExponent(RHS)) &&
(llvm::APFloat::semanticsSizeInBits(LHS) ==
llvm::APFloat::semanticsSizeInBits(RHS));
}
class Z3Solver : public SMTSolver {
friend class Z3ConstraintManager;
Z3Context Context;
Z3_solver Solver;
// Cache Sorts
std::set<Z3Sort> CachedSorts;
// Cache Exprs
std::set<Z3Expr> CachedExprs;
public:
Z3Solver() : Solver(Z3_mk_simple_solver(Context.Context)) {
Z3_solver_inc_ref(Context.Context, Solver);
}
Z3Solver(const Z3Solver &Other) = delete;
Z3Solver(Z3Solver &&Other) = delete;
Z3Solver &operator=(Z3Solver &Other) = delete;
Z3Solver &operator=(Z3Solver &&Other) = delete;
~Z3Solver() {
if (Solver)
Z3_solver_dec_ref(Context.Context, Solver);
}
void addConstraint(const SMTExprRef &Exp) const override {
Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST);
}
// Given an SMTSort, adds/retrives it from the cache and returns
// an SMTSortRef to the SMTSort in the cache
SMTSortRef newSortRef(const SMTSort &Sort) {
auto It = CachedSorts.insert(toZ3Sort(Sort));
return &(*It.first);
}
// Given an SMTExpr, adds/retrives it from the cache and returns
// an SMTExprRef to the SMTExpr in the cache
SMTExprRef newExprRef(const SMTExpr &Exp) {
auto It = CachedExprs.insert(toZ3Expr(Exp));
return &(*It.first);
}
SMTSortRef getBoolSort() override {
return newSortRef(Z3Sort(Context, Z3_mk_bool_sort(Context.Context)));
}
SMTSortRef getBitvectorSort(unsigned BitWidth) override {
return newSortRef(
Z3Sort(Context, Z3_mk_bv_sort(Context.Context, BitWidth)));
}
SMTSortRef getSort(const SMTExprRef &Exp) override {
return newSortRef(
Z3Sort(Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST)));
}
SMTSortRef getFloat16Sort() override {
return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_16(Context.Context)));
}
SMTSortRef getFloat32Sort() override {
return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_32(Context.Context)));
}
SMTSortRef getFloat64Sort() override {
return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_64(Context.Context)));
}
SMTSortRef getFloat128Sort() override {
return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_128(Context.Context)));
}
SMTExprRef mkBVNeg(const SMTExprRef &Exp) override {
return newExprRef(
Z3Expr(Context, Z3_mk_bvneg(Context.Context, toZ3Expr(*Exp).AST)));
}
SMTExprRef mkBVNot(const SMTExprRef &Exp) override {
return newExprRef(
Z3Expr(Context, Z3_mk_bvnot(Context.Context, toZ3Expr(*Exp).AST)));
}
SMTExprRef mkNot(const SMTExprRef &Exp) override {
return newExprRef(
Z3Expr(Context, Z3_mk_not(Context.Context, toZ3Expr(*Exp).AST)));
}
SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_bvadd(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_bvsub(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_bvmul(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_bvsrem(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_bvurem(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_bvsdiv(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_bvudiv(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_bvshl(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_bvashr(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_bvlshr(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_bvxor(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_bvor(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_bvand(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_bvult(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_bvslt(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_bvugt(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_bvsgt(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_bvule(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_bvsle(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_bvuge(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_bvsge(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST};
return newExprRef(Z3Expr(Context, Z3_mk_and(Context.Context, 2, Args)));
}
SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST};
return newExprRef(Z3Expr(Context, Z3_mk_or(Context.Context, 2, Args)));
}
SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_eq(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkFPNeg(const SMTExprRef &Exp) override {
return newExprRef(
Z3Expr(Context, Z3_mk_fpa_neg(Context.Context, toZ3Expr(*Exp).AST)));
}
SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) override {
return newExprRef(Z3Expr(
Context, Z3_mk_fpa_is_infinite(Context.Context, toZ3Expr(*Exp).AST)));
}
SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) override {
return newExprRef(
Z3Expr(Context, Z3_mk_fpa_is_nan(Context.Context, toZ3Expr(*Exp).AST)));
}
SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) override {
return newExprRef(Z3Expr(
Context, Z3_mk_fpa_is_normal(Context.Context, toZ3Expr(*Exp).AST)));
}
SMTExprRef mkFPIsZero(const SMTExprRef &Exp) override {
return newExprRef(Z3Expr(
Context, Z3_mk_fpa_is_zero(Context.Context, toZ3Expr(*Exp).AST)));
}
SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
SMTExprRef RoundingMode = getFloatRoundingMode();
return newExprRef(
Z3Expr(Context,
Z3_mk_fpa_mul(Context.Context, toZ3Expr(*RoundingMode).AST,
toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
}
SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
SMTExprRef RoundingMode = getFloatRoundingMode();
return newExprRef(
Z3Expr(Context,
Z3_mk_fpa_div(Context.Context, toZ3Expr(*RoundingMode).AST,
toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
}
SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_fpa_rem(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
SMTExprRef RoundingMode = getFloatRoundingMode();
return newExprRef(
Z3Expr(Context,
Z3_mk_fpa_add(Context.Context, toZ3Expr(*RoundingMode).AST,
toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
}
SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
SMTExprRef RoundingMode = getFloatRoundingMode();
return newExprRef(
Z3Expr(Context,
Z3_mk_fpa_sub(Context.Context, toZ3Expr(*RoundingMode).AST,
toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
}
SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_fpa_lt(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_fpa_gt(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_fpa_leq(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_fpa_geq(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkFPEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_fpa_eq(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
const SMTExprRef &F) override {
return newExprRef(
Z3Expr(Context, Z3_mk_ite(Context.Context, toZ3Expr(*Cond).AST,
toZ3Expr(*T).AST, toZ3Expr(*F).AST)));
}
SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) override {
return newExprRef(Z3Expr(
Context, Z3_mk_sign_ext(Context.Context, i, toZ3Expr(*Exp).AST)));
}
SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) override {
return newExprRef(Z3Expr(
Context, Z3_mk_zero_ext(Context.Context, i, toZ3Expr(*Exp).AST)));
}
SMTExprRef mkBVExtract(unsigned High, unsigned Low,
const SMTExprRef &Exp) override {
return newExprRef(Z3Expr(Context, Z3_mk_extract(Context.Context, High, Low,
toZ3Expr(*Exp).AST)));
}
/// Creates a predicate that checks for overflow in a bitvector addition
/// operation
SMTExprRef mkBVAddNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS,
bool isSigned) override {
return newExprRef(Z3Expr(
Context, Z3_mk_bvadd_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST, isSigned)));
}
/// Creates a predicate that checks for underflow in a signed bitvector
/// addition operation
SMTExprRef mkBVAddNoUnderflow(const SMTExprRef &LHS,
const SMTExprRef &RHS) override {
return newExprRef(Z3Expr(
Context, Z3_mk_bvadd_no_underflow(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
/// Creates a predicate that checks for overflow in a signed bitvector
/// subtraction operation
SMTExprRef mkBVSubNoOverflow(const SMTExprRef &LHS,
const SMTExprRef &RHS) override {
return newExprRef(Z3Expr(
Context, Z3_mk_bvsub_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
/// Creates a predicate that checks for underflow in a bitvector subtraction
/// operation
SMTExprRef mkBVSubNoUnderflow(const SMTExprRef &LHS, const SMTExprRef &RHS,
bool isSigned) override {
return newExprRef(Z3Expr(
Context, Z3_mk_bvsub_no_underflow(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST, isSigned)));
}
/// Creates a predicate that checks for overflow in a signed bitvector
/// division/modulus operation
SMTExprRef mkBVSDivNoOverflow(const SMTExprRef &LHS,
const SMTExprRef &RHS) override {
return newExprRef(Z3Expr(
Context, Z3_mk_bvsdiv_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
/// Creates a predicate that checks for overflow in a bitvector negation
/// operation
SMTExprRef mkBVNegNoOverflow(const SMTExprRef &Exp) override {
return newExprRef(Z3Expr(
Context, Z3_mk_bvneg_no_overflow(Context.Context, toZ3Expr(*Exp).AST)));
}
/// Creates a predicate that checks for overflow in a bitvector multiplication
/// operation
SMTExprRef mkBVMulNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS,
bool isSigned) override {
return newExprRef(Z3Expr(
Context, Z3_mk_bvmul_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST, isSigned)));
}
/// Creates a predicate that checks for underflow in a signed bitvector
/// multiplication operation
SMTExprRef mkBVMulNoUnderflow(const SMTExprRef &LHS,
const SMTExprRef &RHS) override {
return newExprRef(Z3Expr(
Context, Z3_mk_bvmul_no_underflow(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkBVConcat(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_concat(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
}
SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) override {
SMTExprRef RoundingMode = getFloatRoundingMode();
return newExprRef(Z3Expr(
Context,
Z3_mk_fpa_to_fp_float(Context.Context, toZ3Expr(*RoundingMode).AST,
toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
}
SMTExprRef mkSBVtoFP(const SMTExprRef &From, const SMTSortRef &To) override {
SMTExprRef RoundingMode = getFloatRoundingMode();
return newExprRef(Z3Expr(
Context,
Z3_mk_fpa_to_fp_signed(Context.Context, toZ3Expr(*RoundingMode).AST,
toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
}
SMTExprRef mkUBVtoFP(const SMTExprRef &From, const SMTSortRef &To) override {
SMTExprRef RoundingMode = getFloatRoundingMode();
return newExprRef(Z3Expr(
Context,
Z3_mk_fpa_to_fp_unsigned(Context.Context, toZ3Expr(*RoundingMode).AST,
toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
}
SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth) override {
SMTExprRef RoundingMode = getFloatRoundingMode();
return newExprRef(Z3Expr(
Context, Z3_mk_fpa_to_sbv(Context.Context, toZ3Expr(*RoundingMode).AST,
toZ3Expr(*From).AST, ToWidth)));
}
SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth) override {
SMTExprRef RoundingMode = getFloatRoundingMode();
return newExprRef(Z3Expr(
Context, Z3_mk_fpa_to_ubv(Context.Context, toZ3Expr(*RoundingMode).AST,
toZ3Expr(*From).AST, ToWidth)));
}
SMTExprRef mkBoolean(const bool b) override {
return newExprRef(Z3Expr(Context, b ? Z3_mk_true(Context.Context)
: Z3_mk_false(Context.Context)));
}
SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) override {
const Z3_sort Z3Sort = toZ3Sort(*getBitvectorSort(BitWidth)).Sort;
// Slow path, when 64 bits are not enough.
if (LLVM_UNLIKELY(Int.getBitWidth() > 64u)) {
SmallString<40> Buffer;
Int.toString(Buffer, 10);
return newExprRef(Z3Expr(
Context, Z3_mk_numeral(Context.Context, Buffer.c_str(), Z3Sort)));
}
const int64_t BitReprAsSigned = Int.getExtValue();
const uint64_t BitReprAsUnsigned =
reinterpret_cast<const uint64_t &>(BitReprAsSigned);
Z3_ast Literal =
Int.isSigned()
? Z3_mk_int64(Context.Context, BitReprAsSigned, Z3Sort)
: Z3_mk_unsigned_int64(Context.Context, BitReprAsUnsigned, Z3Sort);
return newExprRef(Z3Expr(Context, Literal));
}
SMTExprRef mkFloat(const llvm::APFloat Float) override {
SMTSortRef Sort =
getFloatSort(llvm::APFloat::semanticsSizeInBits(Float.getSemantics()));
llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), false);
SMTExprRef Z3Int = mkBitvector(Int, Int.getBitWidth());
return newExprRef(Z3Expr(
Context, Z3_mk_fpa_to_fp_bv(Context.Context, toZ3Expr(*Z3Int).AST,
toZ3Sort(*Sort).Sort)));
}
SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) override {
return newExprRef(
Z3Expr(Context, Z3_mk_const(Context.Context,
Z3_mk_string_symbol(Context.Context, Name),
toZ3Sort(*Sort).Sort)));
}
llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth,
bool isUnsigned) override {
return llvm::APSInt(
llvm::APInt(BitWidth,
Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST),
10),
isUnsigned);
}
bool getBoolean(const SMTExprRef &Exp) override {
return Z3_get_bool_value(Context.Context, toZ3Expr(*Exp).AST) == Z3_L_TRUE;
}
SMTExprRef getFloatRoundingMode() override {
// TODO: Don't assume nearest ties to even rounding mode
return newExprRef(Z3Expr(Context, Z3_mk_fpa_rne(Context.Context)));
}
bool toAPFloat(const SMTSortRef &Sort, const SMTExprRef &AST,
llvm::APFloat &Float, bool useSemantics) {
assert(Sort->isFloatSort() && "Unsupported sort to floating-point!");
llvm::APSInt Int(Sort->getFloatSortSize(), true);
const llvm::fltSemantics &Semantics =
getFloatSemantics(Sort->getFloatSortSize());
SMTSortRef BVSort = getBitvectorSort(Sort->getFloatSortSize());
if (!toAPSInt(BVSort, AST, Int, true)) {
return false;
}
if (useSemantics && !areEquivalent(Float.getSemantics(), Semantics)) {
assert(false && "Floating-point types don't match!");
return false;
}
Float = llvm::APFloat(Semantics, Int);
return true;
}
bool toAPSInt(const SMTSortRef &Sort, const SMTExprRef &AST,
llvm::APSInt &Int, bool useSemantics) {
if (Sort->isBitvectorSort()) {
if (useSemantics && Int.getBitWidth() != Sort->getBitvectorSortSize()) {
assert(false && "Bitvector types don't match!");
return false;
}
// FIXME: This function is also used to retrieve floating-point values,
// which can be 16, 32, 64 or 128 bits long. Bitvectors can be anything
// between 1 and 64 bits long, which is the reason we have this weird
// guard. In the future, we need proper calls in the backend to retrieve
// floating-points and its special values (NaN, +/-infinity, +/-zero),
// then we can drop this weird condition.
if (Sort->getBitvectorSortSize() <= 64 ||
Sort->getBitvectorSortSize() == 128) {
Int = getBitvector(AST, Int.getBitWidth(), Int.isUnsigned());
return true;
}
assert(false && "Bitwidth not supported!");
return false;
}
if (Sort->isBooleanSort()) {
if (useSemantics && Int.getBitWidth() < 1) {
assert(false && "Boolean type doesn't match!");
return false;
}
Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), getBoolean(AST)),
Int.isUnsigned());
return true;
}
llvm_unreachable("Unsupported sort to integer!");
}
bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) override {
Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver));
Z3_func_decl Func = Z3_get_app_decl(
Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));
if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE)
return false;
SMTExprRef Assign = newExprRef(
Z3Expr(Context,
Z3_model_get_const_interp(Context.Context, Model.Model, Func)));
SMTSortRef Sort = getSort(Assign);
return toAPSInt(Sort, Assign, Int, true);
}
bool getInterpretation(const SMTExprRef &Exp, llvm::APFloat &Float) override {
Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver));
Z3_func_decl Func = Z3_get_app_decl(
Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));
if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE)
return false;
SMTExprRef Assign = newExprRef(
Z3Expr(Context,
Z3_model_get_const_interp(Context.Context, Model.Model, Func)));
SMTSortRef Sort = getSort(Assign);
return toAPFloat(Sort, Assign, Float, true);
}
Optional<bool> check() const override {
Z3_lbool res = Z3_solver_check(Context.Context, Solver);
if (res == Z3_L_TRUE)
return true;
if (res == Z3_L_FALSE)
return false;
return Optional<bool>();
}
void push() override { return Z3_solver_push(Context.Context, Solver); }
void pop(unsigned NumStates = 1) override {
assert(Z3_solver_get_num_scopes(Context.Context, Solver) >= NumStates);
return Z3_solver_pop(Context.Context, Solver, NumStates);
}
bool isFPSupported() override { return true; }
/// Reset the solver and remove all constraints.
void reset() override { Z3_solver_reset(Context.Context, Solver); }
void print(raw_ostream &OS) const override {
OS << Z3_solver_to_string(Context.Context, Solver);
}
}; // end class Z3Solver
} // end anonymous namespace
#endif
llvm::SMTSolverRef llvm::CreateZ3Solver() {
#if LLVM_WITH_Z3
return std::make_unique<Z3Solver>();
#else
llvm::report_fatal_error("LLVM was not compiled with Z3 support, rebuild "
"with -DLLVM_ENABLE_Z3_SOLVER=ON",
false);
return nullptr;
#endif
}
LLVM_DUMP_METHOD void SMTSort::dump() const { print(llvm::errs()); }
LLVM_DUMP_METHOD void SMTExpr::dump() const { print(llvm::errs()); }
LLVM_DUMP_METHOD void SMTSolver::dump() const { print(llvm::errs()); }
Reference in New Issue View Git Blame Copy Permalink