[analyzer] Fixed method to get APSInt model

Summary:
This patch replaces the current method of getting an `APSInt` from Z3's model by calling generic API method `getBitvector` instead of `Z3_get_numeral_uint64`.

By calling `getBitvector`, there's no need to handle bitvectors with bit width == 128 separately.

And, as a bonus, clang now compiles correctly with Z3 4.7.1.

Reviewers: NoQ, george.karpenkov

Reviewed By: george.karpenkov

Subscribers: xazax.hun, szepet, a.sidorin

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

llvm-svn: 338020

diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
index d10e697..a43ca48 100644 (file)
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
@@ -931,7 +931,8 @@ public:
   virtual SMTExprRef getFloatRoundingMode() = 0;
 
   // If the a model is available, returns the value of a given bitvector symbol
-  virtual const llvm::APSInt getBitvector(const SMTExprRef &Exp) = 0;
+  virtual llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth,
+                                    bool isUnsigned) = 0;
 
   // If the a model is available, returns the value of a given boolean symbol
   virtual bool getBoolean(const SMTExprRef &Exp) = 0;

diff --git a/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
index 4613ae7..7379ded 100644 (file)
--- a/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -734,10 +734,11 @@ public:
                                     toZ3Sort(*Sort).Sort)));
   }
 
-  const llvm::APSInt getBitvector(const SMTExprRef &Exp) override {
-    // FIXME: this returns a string and the bitWidth is overridden
-    return llvm::APSInt(
-        Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST));
+  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));
   }
 
   bool getBoolean(const SMTExprRef &Exp) override {
@@ -814,26 +815,20 @@ public:
         return false;
       }
 
-      uint64_t Value[2];
-      // Force cast because Z3 defines __uint64 to be a unsigned long long
-      // type, which isn't compatible with a unsigned long type, even if they
-      // are the same size.
-      Z3_get_numeral_uint64(Context.Context, toZ3Expr(*AST).AST,
-                            reinterpret_cast<__uint64 *>(&Value[0]));
-      if (Sort->getBitvectorSortSize() <= 64) {
-        Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value[0]),
-                           Int.isUnsigned());
-      } else if (Sort->getBitvectorSortSize() == 128) {
-        SMTExprRef ASTHigh = mkBVExtract(127, 64, AST);
-        Z3_get_numeral_uint64(Context.Context, toZ3Expr(*AST).AST,
-                              reinterpret_cast<__uint64 *>(&Value[1]));
-        Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value),
-                           Int.isUnsigned());
-      } else {
-        assert(false && "Bitwidth not supported!");
-        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;
       }
-      return true;
+
+      assert(false && "Bitwidth not supported!");
+      return false;
     }
 
     if (Sort->isBooleanSort()) {