[analyzer] Fix crash in Z3 SMTConv when negating a boolean expression (#165779) (#168034)

Refer to #158276 for previous hotfix.

In Z3, boolean expressions are incompatible with bitvec operators.
However, C expressions like `-(5 && a)` will generate such symbolic
expressions, which will be further used as an integer. To be compatible
with such usages, this fix converts such expressions to integer using
the existing `fromCast`.

Author: Snape3058

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h

@@ -456,17 +456,15 @@ class SMTConv {
       llvm::SMTExprRef OperandExp =
           getSymExpr(Solver, Ctx, USE->getOperand(), &OperandTy, hasComparison);
 
-      if (const BinarySymExpr *BSE =
-              dyn_cast<BinarySymExpr>(USE->getOperand())) {
-        if (USE->getOpcode() == UO_Minus &&
-            BinaryOperator::isComparisonOp(BSE->getOpcode()))
-          // The comparison operator yields a boolean value in the Z3
-          // language and applying the unary minus operator on a boolean
-          // crashes Z3. However, the unary minus does nothing in this
-          // context (a number is truthy if and only if its negative is
-          // truthy), so let's just ignore the unary minus.
-          // TODO: Replace this with a more general solution.
-          return OperandExp;
+      // When the operand is a bool expr, but the operator is an integeral
+      // operator, casting the bool expr to the integer before creating the
+      // unary operator.
+      // E.g. -(5 && a)
+      if (OperandTy == Ctx.BoolTy && OperandTy != *RetTy &&
+          (*RetTy)->isIntegerType()) {
+        OperandExp = fromCast(Solver, OperandExp, (*RetTy),
+                              Ctx.getTypeSize(*RetTy), OperandTy, 1);
+        OperandTy = (*RetTy);
       }
 
       llvm::SMTExprRef UnaryExp =

clang/test/Analysis/z3-unarysymexpr.c

@@ -47,3 +47,11 @@ int z3_crash2(int a) {
     return *d; // expected-warning{{Dereference of undefined pointer value}}
   return 0;
 }
+
+// Refer to issue 165779
+void z3_crash3(long a) {
+  if (~-(5 && a)) {
+    long *c;
+    *c; // expected-warning{{Dereference of undefined pointer value (loaded from variable 'c')}}
+  }
+}