[analyzer] Hotfix a boolean conversion crash in the Z3 SMTConv

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

@@ -455,6 +455,20 @@ class SMTConv {
       QualType OperandTy;
       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;
+      }
+
       llvm::SMTExprRef UnaryExp =
           OperandTy->isRealFloatingType()
               ? fromFloatUnOp(Solver, USE->getOpcode(), OperandExp)

clang/test/Analysis/z3-unarysymexpr.c

@@ -1,15 +1,49 @@
 // RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify %s \
 // RUN:  -analyzer-constraints=z3 
+// RUN: %clang_analyze_cc1 -verify %s \
+// RUN:  -analyzer-checker=core,debug.ExprInspection \
+// RUN:  -analyzer-config crosscheck-with-z3=true
 
 // REQUIRES: Z3
 //
 // Previously Z3 analysis crashed when it encountered an UnarySymExpr, validate
 // that this no longer happens.
 //
 
-// expected-no-diagnostics
 int negate(int x, int y) {
   if ( ~(x && y))
     return 0;
   return 1;
 }
+
+// Z3 is presented with a SymExpr like this : -((reg_$0<int a>) != 0) :
+// from the Z3 refutation wrapper, that it attempts to convert to a
+// SMTRefExpr, then crashes inside of Z3. The "not zero" portion
+// of that expression is converted to the SMTRefExpr
+// "(not (= reg_$1 #x00000000))", which is a boolean result then the
+// "negative" operator (unary '-', UO_Minus) is attempted to be applied which
+// then causes Z3 to crash. The accompanying patch just strips the negative
+// operator before submitting to Z3 to avoid the crash.
+//
+// TODO: Find the root cause of this and fix it in symbol manager
+//
+void c();
+
+int z3crash(int a, int b) {
+  b = a || b;
+  return (-b == a) / a; // expected-warning{{Division by zero [core.DivideZero]}}
+}
+
+// Floats are handled specifically, and differently in the Z3 refutation layer
+// Just cover that code path
+int z3_nocrash(float a, float b) {
+  b = a || b;
+  return (-b == a) / a;
+}
+
+int z3_crash2(int a) {
+  int *d;
+  if (-(&c && a))
+    return *d; // expected-warning{{Dereference of undefined pointer value}}
+  return 0;
+}