[analyzer] Fix the Z3 backend always generating unsigned APSInt

[mikhail.ramalho]

Summary

In toAPSInt, the Z3 backend was not checking the variable Int's type and was always generating unsigned APSInts.

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.

[ddcc]

I recall that this problem extends beyond the Z3ConstraintManager. Have you looked at D28955, specifically the changes to BasicValueFactory.h?

[mikhail.ramalho]

In D49305#1161850, @ddcc wrote:

I recall that this problem extends beyond the Z3ConstraintManager. Have you looked at D28955, specifically the changes to BasicValueFactory.h?

I did but the changes in this patch fix all the "wrong signedness" crashes in our regressions (when we remove the doIntTypeConversion call).

It doesn't solve all the issues though, as the CSA seems to ignore a number of type casts, but that's not the goal of this patch.

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

case Z3_BV_SORT: {
 
       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(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;
       }
       return true;
     }
     case Z3_BOOL_SORT:
       if (useSemantics && Int.getBitWidth() < 1) {
         assert(false && "Boolean type doesn't match!");
         return false;
       }
       Int = llvm::APSInt(
           llvm::APInt(Int.getBitWidth(),
                       Z3_get_bool_value(Z3Context::ZC, AST) == Z3_L_TRUE ? 1
                                                                          : 0),
-          true);
+          Int.isUnsigned());
       return true;
     }
   }
 
   void Profile(llvm::FoldingSetNodeID &ID) const {
     ID.AddInteger(Z3_get_ast_hash(Z3Context::ZC, AST));
   }