[analyzer] Improvements to the SMT API

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.

Reviewers: george.karpenkov, NoQ

Reviewed By: george.karpenkov

Subscribers: xazax.hun, szepet, a.sidorin, Szelethus

Differential Revision: https://reviews.llvm.org/D52365

git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@343581 91177308-0d34-0410-b5e6-96231b3b80d8

diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
index 1a645cb8701154d6c2c29958ea3ac3f775c4a6e0..db05bdaa4d68a9d3921098026d6fb57a186213e9 100644 (file)
--- a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -134,9 +134,9 @@ public:
       // 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);
 

diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index 8be7d4c4678b3468e0a69e90317003741b2810f2..cdca2a09700dd5131b2cdbb4ed1c4fd6e778cc79 100644 (file)
--- a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -246,7 +246,7 @@ public:
       // Logical operators
     case BO_LAnd:
     case BO_LOr:
-      return fromBinOp(Solver, LHS, Op, RHS, false);
+      return fromBinOp(Solver, LHS, Op, RHS, /*isSigned=*/false);
 
     default:;
     }
@@ -294,14 +294,14 @@ public:
     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!");
   }
@@ -379,14 +379,14 @@ public:
           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);
@@ -466,7 +466,7 @@ public:
       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() ||
@@ -477,8 +477,10 @@ public:
       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!");
@@ -493,7 +495,8 @@ public:
     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;
@@ -507,7 +510,7 @@ public:
     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

diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
index 71bfb400fc91309fc89add7059151847bc195a95..62d1d6548564e9eeff1a14578338b2fc035f9f92 100644 (file)
--- a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
+++ b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
@@ -226,23 +226,23 @@ public:
   /// 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;
@@ -273,18 +273,6 @@ public:
   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;
 

diff --git a/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp b/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
index 1e2939b79df96f665e5971a647e2cc63d35ac519..b79cc9cc09ac7abdf98ccac62cddae3dc45d57d5 100644 (file)
--- a/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
+++ b/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
@@ -2448,15 +2448,19 @@ void FalsePositiveRefutationBRVisitor::finalizeVisitor(
 
   // 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);
   }
 

diff --git a/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp b/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
index 16ab6a33ebe3969664412401e095455ae1ac89d8..f1938057b83de8bfde3ae964d2b1f538cb5f1da2 100644 (file)
--- a/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ b/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -671,7 +671,7 @@ public:
                               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,
@@ -679,7 +679,7 @@ public:
                                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,
@@ -687,14 +687,14 @@ public:
                                  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,
@@ -747,36 +747,6 @@ public:
     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!");