[analyzer] Improvements to the SMT API

[mikhail.ramalho]

Summary

Several improvements in preparation for the new backends.

Refactoring:

• Removed duplicated methods fromBoolean, fromAPSInt, fromInt and fromAPFloat. The methods mkBoolean, mkBitvector and mkFloat are now used instead.
• The names of the functions that convert BVs to FPs were swapped (mkSBVtoFP, mkUBVtoFP, mkFPtoSBV, mkFPtoUBV).
• Added a couple of comments in function calls.

Crosscheck encoding:

• Changed how constraints are encoded in the refutation manager so it doesn't start with (false OR ...). This change introduces one duplicated line (see file BugReporterVisitors.cpp, the `SMTConv::getRangeExpr is called twice, so I can remove this change if the duplication is a problem.

include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h

if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
 
       // Model does not assign interpretation
       if (!Solver->getInterpretation(Exp, Value))
         return nullptr;
 
       // A value has been obtained, check if it is the only value
       SMTExprRef NotExp = SMTConv::fromBinOp(
           Solver, Exp, BO_NE,
-          Ty->isBooleanType() ? Solver->fromBoolean(Value.getBoolValue())
-                              : Solver->fromAPSInt(Value),
-          false);
+          Ty->isBooleanType() ? Solver->mkBoolean(Value.getBoolValue())
+                              : Solver->mkBitvector(Value, Value.getBitWidth()),
+          /*isSigned=*/false);
 
       Solver->addConstraint(NotExp);
 
       Optional<bool> isNotSat = Solver->check();
       if (!isSat.hasValue() || isNotSat.getValue())
         return nullptr;
 
       // This is the only solution, store it

include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h

static inline SMTExprRef fromFloatBinOp(SMTSolverRef &Solver,
 
     case BO_NE:
       return fromFloatUnOp(Solver, UO_LNot,
                            fromFloatBinOp(Solver, LHS, BO_EQ, RHS));
 
       // Logical operators
     case BO_LAnd:
     case BO_LOr:
-      return fromBinOp(Solver, LHS, Op, RHS, false);
+      return fromBinOp(Solver, LHS, Op, RHS, /*isSigned=*/false);
 
     default:;
     }
 
     llvm_unreachable("Unimplemented opcode");
   }
 
   /// Construct an SMTExprRef from a QualType FromTy to a QualType ToTy, and
if (FromTy->isRealFloatingType() && ToTy->isRealFloatingType()) {
         return Solver->mkFPtoFP(Exp, Solver->getFloatSort(ToBitWidth));
 
       return Exp;
     }
 
     if (FromTy->isIntegralOrEnumerationType() && ToTy->isRealFloatingType()) {
       SMTSortRef Sort = Solver->getFloatSort(ToBitWidth);
       return FromTy->isSignedIntegerOrEnumerationType()
-                 ? Solver->mkFPtoSBV(Exp, Sort)
-                 : Solver->mkFPtoUBV(Exp, Sort);
+                 ? Solver->mkSBVtoFP(Exp, Sort)
+                 : Solver->mkUBVtoFP(Exp, Sort);
     }
 
     if (FromTy->isRealFloatingType() && ToTy->isIntegralOrEnumerationType())
       return ToTy->isSignedIntegerOrEnumerationType()
-                 ? Solver->mkSBVtoFP(Exp, ToBitWidth)
-                 : Solver->mkUBVtoFP(Exp, ToBitWidth);
+                 ? Solver->mkFPtoSBV(Exp, ToBitWidth)
+                 : Solver->mkFPtoUBV(Exp, ToBitWidth);
 
     llvm_unreachable("Unsupported explicit type cast!");
   }
 
   // Callback function for doCast parameter on APSInt type.
   static inline llvm::APSInt castAPSInt(SMTSolverRef &Solver,
                                         const llvm::APSInt &V, QualType ToTy,
                                         uint64_t ToWidth, QualType FromTy,
static inline SMTExprRef getSymBinExpr(SMTSolverRef &Solver, ASTContext &Ctx,
     QualType LTy, RTy;
     BinaryOperator::Opcode Op = BSE->getOpcode();
 
     if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
       SMTExprRef LHS =
           getSymExpr(Solver, Ctx, SIE->getLHS(), &LTy, hasComparison);
       llvm::APSInt NewRInt;
       std::tie(NewRInt, RTy) = fixAPSInt(Ctx, SIE->getRHS());
-      SMTExprRef RHS = Solver->fromAPSInt(NewRInt);
+      SMTExprRef RHS = Solver->mkBitvector(NewRInt, NewRInt.getBitWidth());
       return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
     }
 
     if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
       llvm::APSInt NewLInt;
       std::tie(NewLInt, LTy) = fixAPSInt(Ctx, ISE->getLHS());
-      SMTExprRef LHS = Solver->fromAPSInt(NewLInt);
+      SMTExprRef LHS = Solver->mkBitvector(NewLInt, NewLInt.getBitWidth());
       SMTExprRef RHS =
           getSymExpr(Solver, Ctx, ISE->getRHS(), &RTy, hasComparison);
       return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
     }
 
     if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
       SMTExprRef LHS =
           getSymExpr(Solver, Ctx, SSM->getLHS(), &LTy, hasComparison);
public:
   static inline SMTExprRef getZeroExpr(SMTSolverRef &Solver, ASTContext &Ctx,
                                        const SMTExprRef &Exp, QualType Ty,
                                        bool Assumption) {
 
     if (Ty->isRealFloatingType()) {
       llvm::APFloat Zero =
           llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
       return fromFloatBinOp(Solver, Exp, Assumption ? BO_EQ : BO_NE,
-                            Solver->fromAPFloat(Zero));
+                            Solver->mkFloat(Zero));
     }
 
     if (Ty->isIntegralOrEnumerationType() || Ty->isAnyPointerType() ||
         Ty->isBlockPointerType() || Ty->isReferenceType()) {
 
       // Skip explicit comparison for boolean types
       bool isSigned = Ty->isSignedIntegerOrEnumerationType();
       if (Ty->isBooleanType())
         return Assumption ? fromUnOp(Solver, UO_LNot, Exp) : Exp;
 
-      return fromBinOp(Solver, Exp, Assumption ? BO_EQ : BO_NE,
-                       Solver->fromInt("0", Ctx.getTypeSize(Ty)), isSigned);
+      return fromBinOp(
+          Solver, Exp, Assumption ? BO_EQ : BO_NE,
+          Solver->mkBitvector(llvm::APSInt("0"), Ctx.getTypeSize(Ty)),
+          isSigned);
     }
 
     llvm_unreachable("Unsupported type for zero value!");
   }
 
   // Wrapper to generate SMTExprRef from a range. If From == To, an equality
   // will be created instead.
   static inline SMTExprRef getRangeExpr(SMTSolverRef &Solver, ASTContext &Ctx,
                                         SymbolRef Sym, const llvm::APSInt &From,
                                         const llvm::APSInt &To, bool InRange) {
     // Convert lower bound
     QualType FromTy;
     llvm::APSInt NewFromInt;
     std::tie(NewFromInt, FromTy) = fixAPSInt(Ctx, From);
-    SMTExprRef FromExp = Solver->fromAPSInt(NewFromInt);
+    SMTExprRef FromExp =
+        Solver->mkBitvector(NewFromInt, NewFromInt.getBitWidth());
 
     // Convert symbol
     QualType SymTy;
     SMTExprRef Exp = getExpr(Solver, Ctx, Sym, &SymTy);
 
     // Construct single (in)equality
     if (From == To)
       return getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_EQ : BO_NE,
                         FromExp, FromTy, /*RetTy=*/nullptr);
 
     QualType ToTy;
     llvm::APSInt NewToInt;
     std::tie(NewToInt, ToTy) = fixAPSInt(Ctx, To);
-    SMTExprRef ToExp = Solver->fromAPSInt(NewToInt);
+    SMTExprRef ToExp = Solver->mkBitvector(NewToInt, NewToInt.getBitWidth());
     assert(FromTy == ToTy && "Range values have different types!");
 
     // Construct two (in)equalities, and a logical and/or
     SMTExprRef LHS =
         getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp,
                    FromTy, /*RetTy=*/nullptr);
     SMTExprRef RHS = getBinExpr(Solver, Ctx, Exp, SymTy,
                                 InRange ? BO_LE : BO_GT, ToExp, ToTy,
if (order > 0) {
       llvm_unreachable("Unsupported floating-point type cast!");
     }
   }
 };
 } // namespace ento
 } // namespace clang
 
 #endif
 No newline at end of file

include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h

public:
   /// Creates a floating-point equality operation
   virtual SMTExprRef mkFPEqual(const SMTExprRef &LHS,
                                const SMTExprRef &RHS) = 0;
 
   /// Creates a floating-point conversion from floatint-point to floating-point
   /// operation
   virtual SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) = 0;
 
-  /// Creates a floating-point conversion from floatint-point to signed
-  /// bitvector operation
-  virtual SMTExprRef mkFPtoSBV(const SMTExprRef &From,
-                               const SMTSortRef &To) = 0;
-
-  /// Creates a floating-point conversion from floatint-point to unsigned
-  /// bitvector operation
-  virtual SMTExprRef mkFPtoUBV(const SMTExprRef &From,
-                               const SMTSortRef &To) = 0;
-
   /// Creates a floating-point conversion from signed bitvector to
   /// floatint-point operation
-  virtual SMTExprRef mkSBVtoFP(const SMTExprRef &From, unsigned ToWidth) = 0;
+  virtual SMTExprRef mkSBVtoFP(const SMTExprRef &From,
+                               const SMTSortRef &To) = 0;
 
   /// Creates a floating-point conversion from unsigned bitvector to
   /// floatint-point operation
-  virtual SMTExprRef mkUBVtoFP(const SMTExprRef &From, unsigned ToWidth) = 0;
+  virtual SMTExprRef mkUBVtoFP(const SMTExprRef &From,
+                               const SMTSortRef &To) = 0;
+
+  /// Creates a floating-point conversion from floatint-point to signed
+  /// bitvector operation
+  virtual SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth) = 0;
+
+  /// Creates a floating-point conversion from floatint-point to unsigned
+  /// bitvector operation
+  virtual SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth) = 0;
 
   /// Creates a new symbol, given a name and a sort
   virtual SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) = 0;
 
   // Returns an appropriate floating-point rounding mode.
   virtual SMTExprRef getFloatRoundingMode() = 0;
 
   // If the a model is available, returns the value of a given bitvector symbol
public:
 
   /// Given an expression, extract the value of this operand in the model.
   virtual bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) = 0;
 
   /// Given an expression extract the value of this operand in the model.
   virtual bool getInterpretation(const SMTExprRef &Exp,
                                  llvm::APFloat &Float) = 0;
 
-  /// Construct an SMTExprRef value from a boolean.
-  virtual SMTExprRef fromBoolean(const bool Bool) = 0;
-
-  /// Construct an SMTExprRef value from a finite APFloat.
-  virtual SMTExprRef fromAPFloat(const llvm::APFloat &Float) = 0;
-
-  /// Construct an SMTExprRef value from an APSInt.
-  virtual SMTExprRef fromAPSInt(const llvm::APSInt &Int) = 0;
-
-  /// Construct an SMTExprRef value from an integer.
-  virtual SMTExprRef fromInt(const char *Int, uint64_t BitWidth) = 0;
-
   /// Check if the constraints are satisfiable
   virtual Optional<bool> check() const = 0;
 
   /// Push the current solver state
   virtual void push() = 0;
 
   /// Pop the previous solver state
   virtual void pop(unsigned NumStates = 1) = 0;

lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

void FalsePositiveRefutationBRVisitor::finalizeVisitor(
   VisitNode(EndPathNode, nullptr, BRC, BR);
 
   // Create a refutation manager
   SMTSolverRef RefutationSolver = CreateZ3Solver();
   ASTContext &Ctx = BRC.getASTContext();
 
   // Add constraints to the solver
   for (const auto &I : Constraints) {
-    SymbolRef Sym = I.first;
+    const SymbolRef Sym = I.first;
+    auto RangeIt = I.second.begin();
 
-    SMTExprRef Constraints = RefutationSolver->fromBoolean(false);
-    for (const auto &Range : I.second) {
+    SMTExprRef Constraints = SMTConv::getRangeExpr(
+        RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(),
+        /*InRange=*/true);
+    while ((++RangeIt) != I.second.end()) {
       Constraints = RefutationSolver->mkOr(
           Constraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym,
-                                             Range.From(), Range.To(),
+                                             RangeIt->From(), RangeIt->To(),
                                              /*InRange=*/true));
     }
+
     RefutationSolver->addConstraint(Constraints);
   }
 
   // And check for satisfiability
   Optional<bool> isSat = RefutationSolver->check();
   if (!isSat.hasValue())
     return;
 

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

public:
   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 mkFPtoSBV(const SMTExprRef &From, const SMTSortRef &To) override {
+  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 mkFPtoUBV(const SMTExprRef &From, const SMTSortRef &To) override {
+  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 mkSBVtoFP(const SMTExprRef &From, unsigned ToWidth) override {
+  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 mkUBVtoFP(const SMTExprRef &From, unsigned ToWidth) override {
+  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)
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)));
   }
 
-  SMTExprRef fromBoolean(const bool Bool) override {
-    Z3_ast AST =
-        Bool ? Z3_mk_true(Context.Context) : Z3_mk_false(Context.Context);
-    return newExprRef(Z3Expr(Context, AST));
-  }
-
-  SMTExprRef fromAPFloat(const llvm::APFloat &Float) override {
-    SMTSortRef Sort =
-        getFloatSort(llvm::APFloat::semanticsSizeInBits(Float.getSemantics()));
-
-    llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), false);
-    SMTExprRef Z3Int = fromAPSInt(Int);
-    return newExprRef(Z3Expr(
-        Context, Z3_mk_fpa_to_fp_bv(Context.Context, toZ3Expr(*Z3Int).AST,
-                                    toZ3Sort(*Sort).Sort)));
-  }
-
-  SMTExprRef fromAPSInt(const llvm::APSInt &Int) override {
-    SMTSortRef Sort = getBitvectorSort(Int.getBitWidth());
-    Z3_ast AST = Z3_mk_numeral(Context.Context, Int.toString(10).c_str(),
-                               toZ3Sort(*Sort).Sort);
-    return newExprRef(Z3Expr(Context, AST));
-  }
-
-  SMTExprRef fromInt(const char *Int, uint64_t BitWidth) override {
-    SMTSortRef Sort = getBitvectorSort(BitWidth);
-    Z3_ast AST = Z3_mk_numeral(Context.Context, Int, toZ3Sort(*Sort).Sort);
-    return newExprRef(Z3Expr(Context, AST));
-  }
-
   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());