[analyzer] Fixed method to get APSInt model

[mikhail.ramalho]

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.

[george.karpenkov]

requesting clarification

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

737 ↗

(On Diff #157345)

should const be dropped from signature?

818 ↗

(On Diff #157345)

what is this branch doing? What's special about bitvector sort size <= 64 or exactly 128?

[mikhail.ramalho]

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

737 ↗

(On Diff #157345)

On the function where getBitvector is called (get interpretation), the value is assigned to a llvm::APSInt. I removed it so we don't an error that const was dropped.

818 ↗

(On Diff #157345)

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.

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. I didn't implement them because the floating-point part of the backend is not being used.

[george.karpenkov]

LGTM, but could you also add the response you have written regarding 128/<=64 bits objects as a comment.

[mikhail.ramalho]

Added a comment explaining why we have a weird if condition in toAPSInt.

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

public:
 
   /// 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
-  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;
 
   /// Constructs an SMTExprRef from a boolean.
   virtual SMTExprRef mkBoolean(const bool b) = 0;
 
   /// Constructs an SMTExprRef from a finite APFloat.

cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

public:
 
   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)));
   }
 
-  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 {
     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
public:
   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;
       }
 
-      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;
-      }
-      return true;
-    }
+      // 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;
+      }
+
 
     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)),