contrib/llvm/tools/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

   1 //== Z3ConstraintManager.cpp --------------------------------*- C++ -*--==//
   2 //
   3 //                     The LLVM Compiler Infrastructure
   4 //
   5 // This file is distributed under the University of Illinois Open Source
   6 // License. See LICENSE.TXT for details.
   7 //
   8 //===----------------------------------------------------------------------===//
   9
  10 #include "clang/Basic/TargetInfo.h"
  11 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
  12 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
  13 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
  14 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h"
  15 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h"
  16 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h"
  17 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h"
  18
  19 #include "clang/Config/config.h"
  20
  21 using namespace clang;
  22 using namespace ento;
  23
  24 #if CLANG_ANALYZER_WITH_Z3
  25
  26 #include <z3.h>
  27
  28 namespace {
  29
  30 /// Configuration class for Z3
  31 class Z3Config {
  32   friend class Z3Context;
  33
  34   Z3_config Config;
  35
  36 public:
  37   Z3Config() : Config(Z3_mk_config()) {
  38     // Enable model finding
  39     Z3_set_param_value(Config, "model", "true");
  40     // Disable proof generation
  41     Z3_set_param_value(Config, "proof", "false");
  42     // Set timeout to 15000ms = 15s
  43     Z3_set_param_value(Config, "timeout", "15000");
  44   }
  45
  46   ~Z3Config() { Z3_del_config(Config); }
  47 }; // end class Z3Config
  48
  49 // Function used to report errors
  50 void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) {
  51   llvm::report_fatal_error("Z3 error: " +
  52                            llvm::Twine(Z3_get_error_msg_ex(Context, Error)));
  53 }
  54
  55 /// Wrapper for Z3 context
  56 class Z3Context : public SMTContext {
  57 public:
  58   Z3_context Context;
  59
  60   Z3Context() : SMTContext() {
  61     Context = Z3_mk_context_rc(Z3Config().Config);
  62     // The error function is set here because the context is the first object
  63     // created by the backend
  64     Z3_set_error_handler(Context, Z3ErrorHandler);
  65   }
  66
  67   virtual ~Z3Context() {
  68     Z3_del_context(Context);
  69     Context = nullptr;
  70   }
  71 }; // end class Z3Context
  72
  73 /// Wrapper for Z3 Sort
  74 class Z3Sort : public SMTSort {
  75   friend class Z3Solver;
  76
  77   Z3Context &Context;
  78
  79   Z3_sort Sort;
  80
  81 public:
  82   /// Default constructor, mainly used by make_shared
  83   Z3Sort(Z3Context &C, Z3_sort ZS) : SMTSort(), Context(C), Sort(ZS) {
  84     Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
  85   }
  86
  87   /// Override implicit copy constructor for correct reference counting.
  88   Z3Sort(const Z3Sort &Copy)
  89       : SMTSort(), Context(Copy.Context), Sort(Copy.Sort) {
  90     Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
  91   }
  92
  93   /// Provide move constructor
  94   Z3Sort(Z3Sort &&Move) : SMTSort(), Context(Move.Context), Sort(nullptr) {
  95     *this = std::move(Move);
  96   }
  97
  98   /// Provide move assignment constructor
  99   Z3Sort &operator=(Z3Sort &&Move) {
 100     if (this != &Move) {
 101       if (Sort)
 102         Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
 103       Sort = Move.Sort;
 104       Move.Sort = nullptr;
 105     }
 106     return *this;
 107   }
 108
 109   ~Z3Sort() {
 110     if (Sort)
 111       Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
 112   }
 113
 114   bool isBitvectorSortImpl() const override {
 115     return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BV_SORT);
 116   }
 117
 118   bool isFloatSortImpl() const override {
 119     return (Z3_get_sort_kind(Context.Context, Sort) == Z3_FLOATING_POINT_SORT);
 120   }
 121
 122   bool isBooleanSortImpl() const override {
 123     return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BOOL_SORT);
 124   }
 125
 126   unsigned getBitvectorSortSizeImpl() const override {
 127     return Z3_get_bv_sort_size(Context.Context, Sort);
 128   }
 129
 130   unsigned getFloatSortSizeImpl() const override {
 131     return Z3_fpa_get_ebits(Context.Context, Sort) +
 132            Z3_fpa_get_sbits(Context.Context, Sort);
 133   }
 134
 135   bool equal_to(SMTSort const &Other) const override {
 136     return Z3_is_eq_sort(Context.Context, Sort,
 137                          static_cast<const Z3Sort &>(Other).Sort);
 138   }
 139
 140   Z3Sort &operator=(const Z3Sort &Move) {
 141     Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Move.Sort));
 142     Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
 143     Sort = Move.Sort;
 144     return *this;
 145   }
 146
 147   void print(raw_ostream &OS) const override {
 148     OS << Z3_sort_to_string(Context.Context, Sort);
 149   }
 150 }; // end class Z3Sort
 151
 152 static const Z3Sort &toZ3Sort(const SMTSort &S) {
 153   return static_cast<const Z3Sort &>(S);
 154 }
 155
 156 class Z3Expr : public SMTExpr {
 157   friend class Z3Solver;
 158
 159   Z3Context &Context;
 160
 161   Z3_ast AST;
 162
 163 public:
 164   Z3Expr(Z3Context &C, Z3_ast ZA) : SMTExpr(), Context(C), AST(ZA) {
 165     Z3_inc_ref(Context.Context, AST);
 166   }
 167
 168   /// Override implicit copy constructor for correct reference counting.
 169   Z3Expr(const Z3Expr &Copy) : SMTExpr(), Context(Copy.Context), AST(Copy.AST) {
 170     Z3_inc_ref(Context.Context, AST);
 171   }
 172
 173   /// Provide move constructor
 174   Z3Expr(Z3Expr &&Move) : SMTExpr(), Context(Move.Context), AST(nullptr) {
 175     *this = std::move(Move);
 176   }
 177
 178   /// Provide move assignment constructor
 179   Z3Expr &operator=(Z3Expr &&Move) {
 180     if (this != &Move) {
 181       if (AST)
 182         Z3_dec_ref(Context.Context, AST);
 183       AST = Move.AST;
 184       Move.AST = nullptr;
 185     }
 186     return *this;
 187   }
 188
 189   ~Z3Expr() {
 190     if (AST)
 191       Z3_dec_ref(Context.Context, AST);
 192   }
 193
 194   void Profile(llvm::FoldingSetNodeID &ID) const override {
 195     ID.AddInteger(Z3_get_ast_hash(Context.Context, AST));
 196   }
 197
 198   /// Comparison of AST equality, not model equivalence.
 199   bool equal_to(SMTExpr const &Other) const override {
 200     assert(Z3_is_eq_sort(Context.Context, Z3_get_sort(Context.Context, AST),
 201                          Z3_get_sort(Context.Context,
 202                                      static_cast<const Z3Expr &>(Other).AST)) &&
 203            "AST's must have the same sort");
 204     return Z3_is_eq_ast(Context.Context, AST,
 205                         static_cast<const Z3Expr &>(Other).AST);
 206   }
 207
 208   /// Override implicit move constructor for correct reference counting.
 209   Z3Expr &operator=(const Z3Expr &Move) {
 210     Z3_inc_ref(Context.Context, Move.AST);
 211     Z3_dec_ref(Context.Context, AST);
 212     AST = Move.AST;
 213     return *this;
 214   }
 215
 216   void print(raw_ostream &OS) const override {
 217     OS << Z3_ast_to_string(Context.Context, AST);
 218   }
 219 }; // end class Z3Expr
 220
 221 static const Z3Expr &toZ3Expr(const SMTExpr &E) {
 222   return static_cast<const Z3Expr &>(E);
 223 }
 224
 225 class Z3Model {
 226   friend class Z3Solver;
 227
 228   Z3Context &Context;
 229
 230   Z3_model Model;
 231
 232 public:
 233   Z3Model(Z3Context &C, Z3_model ZM) : Context(C), Model(ZM) {
 234     assert(C.Context != nullptr);
 235     Z3_model_inc_ref(Context.Context, Model);
 236   }
 237
 238   /// Override implicit copy constructor for correct reference counting.
 239   Z3Model(const Z3Model &Copy) : Context(Copy.Context), Model(Copy.Model) {
 240     Z3_model_inc_ref(Context.Context, Model);
 241   }
 242
 243   /// Provide move constructor
 244   Z3Model(Z3Model &&Move) : Context(Move.Context), Model(nullptr) {
 245     *this = std::move(Move);
 246   }
 247
 248   /// Provide move assignment constructor
 249   Z3Model &operator=(Z3Model &&Move) {
 250     if (this != &Move) {
 251       if (Model)
 252         Z3_model_dec_ref(Context.Context, Model);
 253       Model = Move.Model;
 254       Move.Model = nullptr;
 255     }
 256     return *this;
 257   }
 258
 259   ~Z3Model() {
 260     if (Model)
 261       Z3_model_dec_ref(Context.Context, Model);
 262   }
 263
 264   void print(raw_ostream &OS) const {
 265     OS << Z3_model_to_string(Context.Context, Model);
 266   }
 267
 268   LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
 269 }; // end class Z3Model
 270
 271 /// Get the corresponding IEEE floating-point type for a given bitwidth.
 272 static const llvm::fltSemantics &getFloatSemantics(unsigned BitWidth) {
 273   switch (BitWidth) {
 274   default:
 275     llvm_unreachable("Unsupported floating-point semantics!");
 276     break;
 277   case 16:
 278     return llvm::APFloat::IEEEhalf();
 279   case 32:
 280     return llvm::APFloat::IEEEsingle();
 281   case 64:
 282     return llvm::APFloat::IEEEdouble();
 283   case 128:
 284     return llvm::APFloat::IEEEquad();
 285   }
 286 }
 287
 288 // Determine whether two float semantics are equivalent
 289 static bool areEquivalent(const llvm::fltSemantics &LHS,
 290                           const llvm::fltSemantics &RHS) {
 291   return (llvm::APFloat::semanticsPrecision(LHS) ==
 292           llvm::APFloat::semanticsPrecision(RHS)) &&
 293          (llvm::APFloat::semanticsMinExponent(LHS) ==
 294           llvm::APFloat::semanticsMinExponent(RHS)) &&
 295          (llvm::APFloat::semanticsMaxExponent(LHS) ==
 296           llvm::APFloat::semanticsMaxExponent(RHS)) &&
 297          (llvm::APFloat::semanticsSizeInBits(LHS) ==
 298           llvm::APFloat::semanticsSizeInBits(RHS));
 299 }
 300
 301 } // end anonymous namespace
 302
 303 typedef llvm::ImmutableSet<std::pair<SymbolRef, Z3Expr>> ConstraintZ3Ty;
 304 REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintZ3, ConstraintZ3Ty)
 305
 306 namespace {
 307
 308 class Z3Solver : public SMTSolver {
 309   friend class Z3ConstraintManager;
 310
 311   Z3Context Context;
 312
 313   Z3_solver Solver;
 314
 315 public:
 316   Z3Solver() : SMTSolver(), Solver(Z3_mk_simple_solver(Context.Context)) {
 317     Z3_solver_inc_ref(Context.Context, Solver);
 318   }
 319
 320   /// Override implicit copy constructor for correct reference counting.
 321   Z3Solver(const Z3Solver &Copy)
 322       : SMTSolver(), Context(Copy.Context), Solver(Copy.Solver) {
 323     Z3_solver_inc_ref(Context.Context, Solver);
 324   }
 325
 326   /// Provide move constructor
 327   Z3Solver(Z3Solver &&Move)
 328       : SMTSolver(), Context(Move.Context), Solver(nullptr) {
 329     *this = std::move(Move);
 330   }
 331
 332   /// Provide move assignment constructor
 333   Z3Solver &operator=(Z3Solver &&Move) {
 334     if (this != &Move) {
 335       if (Solver)
 336         Z3_solver_dec_ref(Context.Context, Solver);
 337       Solver = Move.Solver;
 338       Move.Solver = nullptr;
 339     }
 340     return *this;
 341   }
 342
 343   ~Z3Solver() {
 344     if (Solver)
 345       Z3_solver_dec_ref(Context.Context, Solver);
 346   }
 347
 348   void addConstraint(const SMTExprRef &Exp) const override {
 349     Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST);
 350   }
 351
 352   SMTSortRef getBoolSort() override {
 353     return std::make_shared<Z3Sort>(Context, Z3_mk_bool_sort(Context.Context));
 354   }
 355
 356   SMTSortRef getBitvectorSort(unsigned BitWidth) override {
 357     return std::make_shared<Z3Sort>(Context,
 358                                     Z3_mk_bv_sort(Context.Context, BitWidth));
 359   }
 360
 361   SMTSortRef getSort(const SMTExprRef &Exp) override {
 362     return std::make_shared<Z3Sort>(
 363         Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST));
 364   }
 365
 366   SMTSortRef getFloat16Sort() override {
 367     return std::make_shared<Z3Sort>(Context,
 368                                     Z3_mk_fpa_sort_16(Context.Context));
 369   }
 370
 371   SMTSortRef getFloat32Sort() override {
 372     return std::make_shared<Z3Sort>(Context,
 373                                     Z3_mk_fpa_sort_32(Context.Context));
 374   }
 375
 376   SMTSortRef getFloat64Sort() override {
 377     return std::make_shared<Z3Sort>(Context,
 378                                     Z3_mk_fpa_sort_64(Context.Context));
 379   }
 380
 381   SMTSortRef getFloat128Sort() override {
 382     return std::make_shared<Z3Sort>(Context,
 383                                     Z3_mk_fpa_sort_128(Context.Context));
 384   }
 385
 386   SMTExprRef newExprRef(const SMTExpr &E) const override {
 387     return std::make_shared<Z3Expr>(toZ3Expr(E));
 388   }
 389
 390   SMTExprRef mkBVNeg(const SMTExprRef &Exp) override {
 391     return newExprRef(
 392         Z3Expr(Context, Z3_mk_bvneg(Context.Context, toZ3Expr(*Exp).AST)));
 393   }
 394
 395   SMTExprRef mkBVNot(const SMTExprRef &Exp) override {
 396     return newExprRef(
 397         Z3Expr(Context, Z3_mk_bvnot(Context.Context, toZ3Expr(*Exp).AST)));
 398   }
 399
 400   SMTExprRef mkNot(const SMTExprRef &Exp) override {
 401     return newExprRef(
 402         Z3Expr(Context, Z3_mk_not(Context.Context, toZ3Expr(*Exp).AST)));
 403   }
 404
 405   SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 406     return newExprRef(
 407         Z3Expr(Context, Z3_mk_bvadd(Context.Context, toZ3Expr(*LHS).AST,
 408                                     toZ3Expr(*RHS).AST)));
 409   }
 410
 411   SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 412     return newExprRef(
 413         Z3Expr(Context, Z3_mk_bvsub(Context.Context, toZ3Expr(*LHS).AST,
 414                                     toZ3Expr(*RHS).AST)));
 415   }
 416
 417   SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 418     return newExprRef(
 419         Z3Expr(Context, Z3_mk_bvmul(Context.Context, toZ3Expr(*LHS).AST,
 420                                     toZ3Expr(*RHS).AST)));
 421   }
 422
 423   SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 424     return newExprRef(
 425         Z3Expr(Context, Z3_mk_bvsrem(Context.Context, toZ3Expr(*LHS).AST,
 426                                      toZ3Expr(*RHS).AST)));
 427   }
 428
 429   SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 430     return newExprRef(
 431         Z3Expr(Context, Z3_mk_bvurem(Context.Context, toZ3Expr(*LHS).AST,
 432                                      toZ3Expr(*RHS).AST)));
 433   }
 434
 435   SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 436     return newExprRef(
 437         Z3Expr(Context, Z3_mk_bvsdiv(Context.Context, toZ3Expr(*LHS).AST,
 438                                      toZ3Expr(*RHS).AST)));
 439   }
 440
 441   SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 442     return newExprRef(
 443         Z3Expr(Context, Z3_mk_bvudiv(Context.Context, toZ3Expr(*LHS).AST,
 444                                      toZ3Expr(*RHS).AST)));
 445   }
 446
 447   SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 448     return newExprRef(
 449         Z3Expr(Context, Z3_mk_bvshl(Context.Context, toZ3Expr(*LHS).AST,
 450                                     toZ3Expr(*RHS).AST)));
 451   }
 452
 453   SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 454     return newExprRef(
 455         Z3Expr(Context, Z3_mk_bvashr(Context.Context, toZ3Expr(*LHS).AST,
 456                                      toZ3Expr(*RHS).AST)));
 457   }
 458
 459   SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 460     return newExprRef(
 461         Z3Expr(Context, Z3_mk_bvlshr(Context.Context, toZ3Expr(*LHS).AST,
 462                                      toZ3Expr(*RHS).AST)));
 463   }
 464
 465   SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 466     return newExprRef(
 467         Z3Expr(Context, Z3_mk_bvxor(Context.Context, toZ3Expr(*LHS).AST,
 468                                     toZ3Expr(*RHS).AST)));
 469   }
 470
 471   SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 472     return newExprRef(
 473         Z3Expr(Context, Z3_mk_bvor(Context.Context, toZ3Expr(*LHS).AST,
 474                                    toZ3Expr(*RHS).AST)));
 475   }
 476
 477   SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 478     return newExprRef(
 479         Z3Expr(Context, Z3_mk_bvand(Context.Context, toZ3Expr(*LHS).AST,
 480                                     toZ3Expr(*RHS).AST)));
 481   }
 482
 483   SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 484     return newExprRef(
 485         Z3Expr(Context, Z3_mk_bvult(Context.Context, toZ3Expr(*LHS).AST,
 486                                     toZ3Expr(*RHS).AST)));
 487   }
 488
 489   SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 490     return newExprRef(
 491         Z3Expr(Context, Z3_mk_bvslt(Context.Context, toZ3Expr(*LHS).AST,
 492                                     toZ3Expr(*RHS).AST)));
 493   }
 494
 495   SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 496     return newExprRef(
 497         Z3Expr(Context, Z3_mk_bvugt(Context.Context, toZ3Expr(*LHS).AST,
 498                                     toZ3Expr(*RHS).AST)));
 499   }
 500
 501   SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 502     return newExprRef(
 503         Z3Expr(Context, Z3_mk_bvsgt(Context.Context, toZ3Expr(*LHS).AST,
 504                                     toZ3Expr(*RHS).AST)));
 505   }
 506
 507   SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 508     return newExprRef(
 509         Z3Expr(Context, Z3_mk_bvule(Context.Context, toZ3Expr(*LHS).AST,
 510                                     toZ3Expr(*RHS).AST)));
 511   }
 512
 513   SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 514     return newExprRef(
 515         Z3Expr(Context, Z3_mk_bvsle(Context.Context, toZ3Expr(*LHS).AST,
 516                                     toZ3Expr(*RHS).AST)));
 517   }
 518
 519   SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 520     return newExprRef(
 521         Z3Expr(Context, Z3_mk_bvuge(Context.Context, toZ3Expr(*LHS).AST,
 522                                     toZ3Expr(*RHS).AST)));
 523   }
 524
 525   SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 526     return newExprRef(
 527         Z3Expr(Context, Z3_mk_bvsge(Context.Context, toZ3Expr(*LHS).AST,
 528                                     toZ3Expr(*RHS).AST)));
 529   }
 530
 531   SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 532     Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST};
 533     return newExprRef(Z3Expr(Context, Z3_mk_and(Context.Context, 2, Args)));
 534   }
 535
 536   SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 537     Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST};
 538     return newExprRef(Z3Expr(Context, Z3_mk_or(Context.Context, 2, Args)));
 539   }
 540
 541   SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 542     return newExprRef(
 543         Z3Expr(Context, Z3_mk_eq(Context.Context, toZ3Expr(*LHS).AST,
 544                                  toZ3Expr(*RHS).AST)));
 545   }
 546
 547   SMTExprRef mkFPNeg(const SMTExprRef &Exp) override {
 548     return newExprRef(
 549         Z3Expr(Context, Z3_mk_fpa_neg(Context.Context, toZ3Expr(*Exp).AST)));
 550   }
 551
 552   SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) override {
 553     return newExprRef(Z3Expr(
 554         Context, Z3_mk_fpa_is_infinite(Context.Context, toZ3Expr(*Exp).AST)));
 555   }
 556
 557   SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) override {
 558     return newExprRef(
 559         Z3Expr(Context, Z3_mk_fpa_is_nan(Context.Context, toZ3Expr(*Exp).AST)));
 560   }
 561
 562   SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) override {
 563     return newExprRef(Z3Expr(
 564         Context, Z3_mk_fpa_is_normal(Context.Context, toZ3Expr(*Exp).AST)));
 565   }
 566
 567   SMTExprRef mkFPIsZero(const SMTExprRef &Exp) override {
 568     return newExprRef(Z3Expr(
 569         Context, Z3_mk_fpa_is_zero(Context.Context, toZ3Expr(*Exp).AST)));
 570   }
 571
 572   SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 573     SMTExprRef RoundingMode = getFloatRoundingMode();
 574     return newExprRef(
 575         Z3Expr(Context,
 576                Z3_mk_fpa_mul(Context.Context, toZ3Expr(*LHS).AST,
 577                              toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST)));
 578   }
 579
 580   SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 581     SMTExprRef RoundingMode = getFloatRoundingMode();
 582     return newExprRef(
 583         Z3Expr(Context,
 584                Z3_mk_fpa_div(Context.Context, toZ3Expr(*LHS).AST,
 585                              toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST)));
 586   }
 587
 588   SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 589     return newExprRef(
 590         Z3Expr(Context, Z3_mk_fpa_rem(Context.Context, toZ3Expr(*LHS).AST,
 591                                       toZ3Expr(*RHS).AST)));
 592   }
 593
 594   SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 595     SMTExprRef RoundingMode = getFloatRoundingMode();
 596     return newExprRef(
 597         Z3Expr(Context,
 598                Z3_mk_fpa_add(Context.Context, toZ3Expr(*LHS).AST,
 599                              toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST)));
 600   }
 601
 602   SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 603     SMTExprRef RoundingMode = getFloatRoundingMode();
 604     return newExprRef(
 605         Z3Expr(Context,
 606                Z3_mk_fpa_sub(Context.Context, toZ3Expr(*LHS).AST,
 607                              toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST)));
 608   }
 609
 610   SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 611     return newExprRef(
 612         Z3Expr(Context, Z3_mk_fpa_lt(Context.Context, toZ3Expr(*LHS).AST,
 613                                      toZ3Expr(*RHS).AST)));
 614   }
 615
 616   SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 617     return newExprRef(
 618         Z3Expr(Context, Z3_mk_fpa_gt(Context.Context, toZ3Expr(*LHS).AST,
 619                                      toZ3Expr(*RHS).AST)));
 620   }
 621
 622   SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 623     return newExprRef(
 624         Z3Expr(Context, Z3_mk_fpa_leq(Context.Context, toZ3Expr(*LHS).AST,
 625                                       toZ3Expr(*RHS).AST)));
 626   }
 627
 628   SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 629     return newExprRef(
 630         Z3Expr(Context, Z3_mk_fpa_geq(Context.Context, toZ3Expr(*LHS).AST,
 631                                       toZ3Expr(*RHS).AST)));
 632   }
 633
 634   SMTExprRef mkFPEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 635     return newExprRef(
 636         Z3Expr(Context, Z3_mk_fpa_eq(Context.Context, toZ3Expr(*LHS).AST,
 637                                      toZ3Expr(*RHS).AST)));
 638   }
 639
 640   SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
 641                    const SMTExprRef &F) override {
 642     return newExprRef(
 643         Z3Expr(Context, Z3_mk_ite(Context.Context, toZ3Expr(*Cond).AST,
 644                                   toZ3Expr(*T).AST, toZ3Expr(*F).AST)));
 645   }
 646
 647   SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) override {
 648     return newExprRef(Z3Expr(
 649         Context, Z3_mk_sign_ext(Context.Context, i, toZ3Expr(*Exp).AST)));
 650   }
 651
 652   SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) override {
 653     return newExprRef(Z3Expr(
 654         Context, Z3_mk_zero_ext(Context.Context, i, toZ3Expr(*Exp).AST)));
 655   }
 656
 657   SMTExprRef mkBVExtract(unsigned High, unsigned Low,
 658                          const SMTExprRef &Exp) override {
 659     return newExprRef(Z3Expr(Context, Z3_mk_extract(Context.Context, High, Low,
 660                                                     toZ3Expr(*Exp).AST)));
 661   }
 662
 663   SMTExprRef mkBVConcat(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 664     return newExprRef(
 665         Z3Expr(Context, Z3_mk_concat(Context.Context, toZ3Expr(*LHS).AST,
 666                                      toZ3Expr(*RHS).AST)));
 667   }
 668
 669   SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) override {
 670     SMTExprRef RoundingMode = getFloatRoundingMode();
 671     return newExprRef(Z3Expr(
 672         Context,
 673         Z3_mk_fpa_to_fp_float(Context.Context, toZ3Expr(*RoundingMode).AST,
 674                               toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
 675   }
 676
 677   SMTExprRef mkFPtoSBV(const SMTExprRef &From, const SMTSortRef &To) override {
 678     SMTExprRef RoundingMode = getFloatRoundingMode();
 679     return newExprRef(Z3Expr(
 680         Context,
 681         Z3_mk_fpa_to_fp_signed(Context.Context, toZ3Expr(*RoundingMode).AST,
 682                                toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
 683   }
 684
 685   SMTExprRef mkFPtoUBV(const SMTExprRef &From, const SMTSortRef &To) override {
 686     SMTExprRef RoundingMode = getFloatRoundingMode();
 687     return newExprRef(Z3Expr(
 688         Context,
 689         Z3_mk_fpa_to_fp_unsigned(Context.Context, toZ3Expr(*RoundingMode).AST,
 690                                  toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
 691   }
 692
 693   SMTExprRef mkSBVtoFP(const SMTExprRef &From, unsigned ToWidth) override {
 694     SMTExprRef RoundingMode = getFloatRoundingMode();
 695     return newExprRef(Z3Expr(
 696         Context, Z3_mk_fpa_to_sbv(Context.Context, toZ3Expr(*RoundingMode).AST,
 697                                   toZ3Expr(*From).AST, ToWidth)));
 698   }
 699
 700   SMTExprRef mkUBVtoFP(const SMTExprRef &From, unsigned ToWidth) override {
 701     SMTExprRef RoundingMode = getFloatRoundingMode();
 702     return newExprRef(Z3Expr(
 703         Context, Z3_mk_fpa_to_ubv(Context.Context, toZ3Expr(*RoundingMode).AST,
 704                                   toZ3Expr(*From).AST, ToWidth)));
 705   }
 706
 707   SMTExprRef mkBoolean(const bool b) override {
 708     return newExprRef(Z3Expr(Context, b ? Z3_mk_true(Context.Context)
 709                                         : Z3_mk_false(Context.Context)));
 710   }
 711
 712   SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) override {
 713     const SMTSortRef Sort = getBitvectorSort(BitWidth);
 714     return newExprRef(
 715         Z3Expr(Context, Z3_mk_numeral(Context.Context, Int.toString(10).c_str(),
 716                                       toZ3Sort(*Sort).Sort)));
 717   }
 718
 719   SMTExprRef mkFloat(const llvm::APFloat Float) override {
 720     SMTSortRef Sort =
 721         getFloatSort(llvm::APFloat::semanticsSizeInBits(Float.getSemantics()));
 722
 723     llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), false);
 724     SMTExprRef Z3Int = mkBitvector(Int, Int.getBitWidth());
 725     return newExprRef(Z3Expr(
 726         Context, Z3_mk_fpa_to_fp_bv(Context.Context, toZ3Expr(*Z3Int).AST,
 727                                     toZ3Sort(*Sort).Sort)));
 728   }
 729
 730   SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) override {
 731     return newExprRef(
 732         Z3Expr(Context, Z3_mk_const(Context.Context,
 733                                     Z3_mk_string_symbol(Context.Context, Name),
 734                                     toZ3Sort(*Sort).Sort)));
 735   }
 736
 737   llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth,
 738                             bool isUnsigned) override {
 739     return llvm::APSInt(llvm::APInt(
 740         BitWidth, Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST),
 741         10));
 742   }
 743
 744   bool getBoolean(const SMTExprRef &Exp) override {
 745     return Z3_get_bool_value(Context.Context, toZ3Expr(*Exp).AST) == Z3_L_TRUE;
 746   }
 747
 748   SMTExprRef getFloatRoundingMode() override {
 749     // TODO: Don't assume nearest ties to even rounding mode
 750     return newExprRef(Z3Expr(Context, Z3_mk_fpa_rne(Context.Context)));
 751   }
 752
 753   SMTExprRef fromData(const SymbolID ID, const QualType &Ty,
 754                       uint64_t BitWidth) override {
 755     llvm::Twine Name = "$" + llvm::Twine(ID);
 756     return mkSymbol(Name.str().c_str(), mkSort(Ty, BitWidth));
 757   }
 758
 759   SMTExprRef fromBoolean(const bool Bool) override {
 760     Z3_ast AST =
 761         Bool ? Z3_mk_true(Context.Context) : Z3_mk_false(Context.Context);
 762     return newExprRef(Z3Expr(Context, AST));
 763   }
 764
 765   SMTExprRef fromAPFloat(const llvm::APFloat &Float) override {
 766     SMTSortRef Sort =
 767         getFloatSort(llvm::APFloat::semanticsSizeInBits(Float.getSemantics()));
 768
 769     llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), false);
 770     SMTExprRef Z3Int = fromAPSInt(Int);
 771     return newExprRef(Z3Expr(
 772         Context, Z3_mk_fpa_to_fp_bv(Context.Context, toZ3Expr(*Z3Int).AST,
 773                                     toZ3Sort(*Sort).Sort)));
 774   }
 775
 776   SMTExprRef fromAPSInt(const llvm::APSInt &Int) override {
 777     SMTSortRef Sort = getBitvectorSort(Int.getBitWidth());
 778     Z3_ast AST = Z3_mk_numeral(Context.Context, Int.toString(10).c_str(),
 779                                toZ3Sort(*Sort).Sort);
 780     return newExprRef(Z3Expr(Context, AST));
 781   }
 782
 783   SMTExprRef fromInt(const char *Int, uint64_t BitWidth) override {
 784     SMTSortRef Sort = getBitvectorSort(BitWidth);
 785     Z3_ast AST = Z3_mk_numeral(Context.Context, Int, toZ3Sort(*Sort).Sort);
 786     return newExprRef(Z3Expr(Context, AST));
 787   }
 788
 789   bool toAPFloat(const SMTSortRef &Sort, const SMTExprRef &AST,
 790                  llvm::APFloat &Float, bool useSemantics) {
 791     assert(Sort->isFloatSort() && "Unsupported sort to floating-point!");
 792
 793     llvm::APSInt Int(Sort->getFloatSortSize(), true);
 794     const llvm::fltSemantics &Semantics =
 795         getFloatSemantics(Sort->getFloatSortSize());
 796     SMTSortRef BVSort = getBitvectorSort(Sort->getFloatSortSize());
 797     if (!toAPSInt(BVSort, AST, Int, true)) {
 798       return false;
 799     }
 800
 801     if (useSemantics && !areEquivalent(Float.getSemantics(), Semantics)) {
 802       assert(false && "Floating-point types don't match!");
 803       return false;
 804     }
 805
 806     Float = llvm::APFloat(Semantics, Int);
 807     return true;
 808   }
 809
 810   bool toAPSInt(const SMTSortRef &Sort, const SMTExprRef &AST,
 811                 llvm::APSInt &Int, bool useSemantics) {
 812     if (Sort->isBitvectorSort()) {
 813       if (useSemantics && Int.getBitWidth() != Sort->getBitvectorSortSize()) {
 814         assert(false && "Bitvector types don't match!");
 815         return false;
 816       }
 817
 818       // FIXME: This function is also used to retrieve floating-point values,
 819       // which can be 16, 32, 64 or 128 bits long. Bitvectors can be anything
 820       // between 1 and 64 bits long, which is the reason we have this weird
 821       // guard. In the future, we need proper calls in the backend to retrieve
 822       // floating-points and its special values (NaN, +/-infinity, +/-zero),
 823       // then we can drop this weird condition.
 824       if (Sort->getBitvectorSortSize() <= 64 ||
 825           Sort->getBitvectorSortSize() == 128) {
 826         Int = getBitvector(AST, Int.getBitWidth(), Int.isUnsigned());
 827         return true;
 828       }
 829
 830       assert(false && "Bitwidth not supported!");
 831       return false;
 832     }
 833
 834     if (Sort->isBooleanSort()) {
 835       if (useSemantics && Int.getBitWidth() < 1) {
 836         assert(false && "Boolean type doesn't match!");
 837         return false;
 838       }
 839
 840       Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), getBoolean(AST)),
 841                          Int.isUnsigned());
 842       return true;
 843     }
 844
 845     llvm_unreachable("Unsupported sort to integer!");
 846   }
 847
 848   bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) override {
 849     Z3Model Model = getModel();
 850     Z3_func_decl Func = Z3_get_app_decl(
 851         Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));
 852     if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE)
 853       return false;
 854
 855     SMTExprRef Assign = newExprRef(
 856         Z3Expr(Context,
 857                Z3_model_get_const_interp(Context.Context, Model.Model, Func)));
 858     SMTSortRef Sort = getSort(Assign);
 859     return toAPSInt(Sort, Assign, Int, true);
 860   }
 861
 862   bool getInterpretation(const SMTExprRef &Exp, llvm::APFloat &Float) override {
 863     Z3Model Model = getModel();
 864     Z3_func_decl Func = Z3_get_app_decl(
 865         Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));
 866     if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE)
 867       return false;
 868
 869     SMTExprRef Assign = newExprRef(
 870         Z3Expr(Context,
 871                Z3_model_get_const_interp(Context.Context, Model.Model, Func)));
 872     SMTSortRef Sort = getSort(Assign);
 873     return toAPFloat(Sort, Assign, Float, true);
 874   }
 875
 876   ConditionTruthVal check() const override {
 877     Z3_lbool res = Z3_solver_check(Context.Context, Solver);
 878     if (res == Z3_L_TRUE)
 879       return true;
 880
 881     if (res == Z3_L_FALSE)
 882       return false;
 883
 884     return ConditionTruthVal();
 885   }
 886
 887   void push() override { return Z3_solver_push(Context.Context, Solver); }
 888
 889   void pop(unsigned NumStates = 1) override {
 890     assert(Z3_solver_get_num_scopes(Context.Context, Solver) >= NumStates);
 891     return Z3_solver_pop(Context.Context, Solver, NumStates);
 892   }
 893
 894   /// Get a model from the solver. Caller should check the model is
 895   /// satisfiable.
 896   Z3Model getModel() {
 897     return Z3Model(Context, Z3_solver_get_model(Context.Context, Solver));
 898   }
 899
 900   /// Reset the solver and remove all constraints.
 901   void reset() const override { Z3_solver_reset(Context.Context, Solver); }
 902
 903   void print(raw_ostream &OS) const override {
 904     OS << Z3_solver_to_string(Context.Context, Solver);
 905   }
 906 }; // end class Z3Solver
 907
 908 class Z3ConstraintManager : public SMTConstraintManager {
 909   SMTSolverRef Solver = CreateZ3Solver();
 910
 911 public:
 912   Z3ConstraintManager(SubEngine *SE, SValBuilder &SB)
 913       : SMTConstraintManager(SE, SB, Solver) {}
 914
 915   void addStateConstraints(ProgramStateRef State) const override {
 916     // TODO: Don't add all the constraints, only the relevant ones
 917     ConstraintZ3Ty CZ = State->get<ConstraintZ3>();
 918     ConstraintZ3Ty::iterator I = CZ.begin(), IE = CZ.end();
 919
 920     // Construct the logical AND of all the constraints
 921     if (I != IE) {
 922       std::vector<SMTExprRef> ASTs;
 923
 924       SMTExprRef Constraint = Solver->newExprRef(I++->second);
 925       while (I != IE) {
 926         Constraint = Solver->mkAnd(Constraint, Solver->newExprRef(I++->second));
 927       }
 928
 929       Solver->addConstraint(Constraint);
 930     }
 931   }
 932
 933   bool canReasonAbout(SVal X) const override {
 934     const TargetInfo &TI = getBasicVals().getContext().getTargetInfo();
 935
 936     Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
 937     if (!SymVal)
 938       return true;
 939
 940     const SymExpr *Sym = SymVal->getSymbol();
 941     QualType Ty = Sym->getType();
 942
 943     // Complex types are not modeled
 944     if (Ty->isComplexType() || Ty->isComplexIntegerType())
 945       return false;
 946
 947     // Non-IEEE 754 floating-point types are not modeled
 948     if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) &&
 949          (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() ||
 950           &TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble())))
 951       return false;
 952
 953     if (isa<SymbolData>(Sym))
 954       return true;
 955
 956     SValBuilder &SVB = getSValBuilder();
 957
 958     if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
 959       return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
 960
 961     if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
 962       if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE))
 963         return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS()));
 964
 965       if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE))
 966         return canReasonAbout(SVB.makeSymbolVal(ISE->getRHS()));
 967
 968       if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(BSE))
 969         return canReasonAbout(SVB.makeSymbolVal(SSE->getLHS())) &&
 970                canReasonAbout(SVB.makeSymbolVal(SSE->getRHS()));
 971     }
 972
 973     llvm_unreachable("Unsupported expression to reason about!");
 974   }
 975
 976   ProgramStateRef removeDeadBindings(ProgramStateRef State,
 977                                      SymbolReaper &SymReaper) override {
 978     ConstraintZ3Ty CZ = State->get<ConstraintZ3>();
 979     ConstraintZ3Ty::Factory &CZFactory = State->get_context<ConstraintZ3>();
 980
 981     for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) {
 982       if (SymReaper.maybeDead(I->first))
 983         CZ = CZFactory.remove(CZ, *I);
 984     }
 985
 986     return State->set<ConstraintZ3>(CZ);
 987   }
 988
 989   ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym,
 990                              const SMTExprRef &Exp) override {
 991     // Check the model, avoid simplifying AST to save time
 992     if (checkModel(State, Exp).isConstrainedTrue())
 993       return State->add<ConstraintZ3>(std::make_pair(Sym, toZ3Expr(*Exp)));
 994
 995     return nullptr;
 996   }
 997
 998   //==------------------------------------------------------------------------==/
 999   // Pretty-printing.
1000   //==------------------------------------------------------------------------==/
1001
1002   void print(ProgramStateRef St, raw_ostream &OS, const char *nl,
1003              const char *sep) override {
1004
1005     ConstraintZ3Ty CZ = St->get<ConstraintZ3>();
1006
1007     OS << nl << sep << "Constraints:";
1008     for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) {
1009       OS << nl << ' ' << I->first << " : ";
1010       I->second.print(OS);
1011     }
1012     OS << nl;
1013   }
1014 }; // end class Z3ConstraintManager
1015
1016 } // end anonymous namespace
1017
1018 #endif
1019
1020 std::unique_ptr<SMTSolver> clang::ento::CreateZ3Solver() {
1021 #if CLANG_ANALYZER_WITH_Z3
1022   return llvm::make_unique<Z3Solver>();
1023 #else
1024   llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
1025                            "with -DCLANG_ANALYZER_BUILD_Z3=ON",
1026                            false);
1027   return nullptr;
1028 #endif
1029 }
1030
1031 std::unique_ptr<ConstraintManager>
1032 ento::CreateZ3ConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
1033 #if CLANG_ANALYZER_WITH_Z3
1034   return llvm::make_unique<Z3ConstraintManager>(Eng, StMgr.getSValBuilder());
1035 #else
1036   llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
1037                            "with -DCLANG_ANALYZER_BUILD_Z3=ON",
1038                            false);
1039   return nullptr;
1040 #endif
1041 }