[analyzer] Fix the Z3 backend always generating unsigned APSInt

Summary:
In `toAPSInt`, the Z3 backend was not checking the variable `Int`'s type and was always generating unsigned `APSInt`s.

This was found by accident when I removed:
```
    llvm::APSInt ConvertedLHS, ConvertedRHS;
    QualType LTy, RTy;
    std::tie(ConvertedLHS, LTy) = fixAPSInt(*LHS);
    std::tie(ConvertedRHS, RTy) = fixAPSInt(*RHS);
-    doIntTypePromotion<llvm::APSInt, Z3ConstraintManager::castAPSInt>(
-        ConvertedLHS, LTy, ConvertedRHS, RTy);
    return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
```

And the `BasicValueFactory` started to complain about different `signedness`.

Reviewers: george.karpenkov, NoQ, ddcc

Reviewed By: ddcc

Subscribers: xazax.hun, szepet, a.sidorin

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

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

diff --git a/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp b/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
index 9e975676ccd51662cb7ba65aac91eab446dd10b4..721e17759fb2208d782223f677f74d1700884677 100644 (file)
--- a/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ b/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -681,12 +681,14 @@ public:
       Z3_get_numeral_uint64(Z3Context::ZC, AST,
                             reinterpret_cast<__uint64 *>(&Value[0]));
       if (Sort.getBitvectorSortSize() <= 64) {
-        Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value[0]), true);
+        Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value[0]),
+                           Int.isUnsigned());
       } else if (Sort.getBitvectorSortSize() == 128) {
         Z3Expr ASTHigh = Z3Expr(Z3_mk_extract(Z3Context::ZC, 127, 64, AST));
         Z3_get_numeral_uint64(Z3Context::ZC, AST,
                               reinterpret_cast<__uint64 *>(&Value[1]));
-        Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value), true);
+        Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value),
+                           Int.isUnsigned());
       } else {
         assert(false && "Bitwidth not supported!");
         return false;
@@ -702,7 +704,7 @@ public:
           llvm::APInt(Int.getBitWidth(),
                       Z3_get_bool_value(Z3Context::ZC, AST) == Z3_L_TRUE ? 1
                                                                          : 0),
-          true);
+          Int.isUnsigned());
       return true;
     }
   }