[analyzer] Fix assertion failure in SMT conversion for unary operator on floats.

[tomasz-kaminski-sonarsource]

Summary

In the handling of the Symbols from the RangExpr, the code assumed that the operands of the unary operators need to have integral type.
However, the CSA can create SymExpr with a floating point operand, when the integer value is cast into it, like (float)h == (float)l where both of h and l are integers.

This patch handles such situations, by using fromFloatUnOp instead of fromUnOp, when the operand have a floating point type.

I have investigated all other calls of fromUnOp, and for one in:

• getZeroExpr is applied only on boolean types, so it correct
• fromBinOp is not invoked for floating points
• fromFloatUnOp I am uncertain about this case and I was not able to produce a test that would reach this point, as a negation of floating points numbers seem to produce Unknown symbols.,

This issue exists since the introduction of UnarySymExpr in https://reviews.llvm.org/D125318 and their handling for Z3 in https://reviews.llvm.org/D125547.

[mikhail.ramalho]

LGTM.

[steakhal]

I'm proposing to backport this fix to clang-16.
https://github.com/llvm/llvm-project/issues/61097

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

static inline llvm::SMTExprRef getSymExpr(llvm::SMTSolverRef &Solver,
     if (const UnarySymExpr *USE = dyn_cast<UnarySymExpr>(Sym)) {
       if (RetTy)
         *RetTy = Sym->getType();
 
       QualType OperandTy;
       llvm::SMTExprRef OperandExp =
           getSymExpr(Solver, Ctx, USE->getOperand(), &OperandTy, hasComparison);
       llvm::SMTExprRef UnaryExp =
-          fromUnOp(Solver, USE->getOpcode(), OperandExp);
+          OperandTy->isRealFloatingType()
+              ? fromFloatUnOp(Solver, USE->getOpcode(), OperandExp)
+              : fromUnOp(Solver, USE->getOpcode(), OperandExp);
 
       // Currently, without the `support-symbolic-integer-casts=true` option,
       // we do not emit `SymbolCast`s for implicit casts.
       // One such implicit cast is missing if the operand of the unary operator
       // has a different type than the unary itself.
       if (Ctx.getTypeSize(OperandTy) != Ctx.getTypeSize(Sym->getType())) {
         if (hasComparison)
           *hasComparison = false;

clang/test/Analysis/z3-crosscheck.c

-// RUN: %clang_cc1 -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -DNO_CROSSCHECK -verify %s
-// RUN: %clang_cc1 -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -analyzer-config crosscheck-with-z3=true -verify %s
+// RUN: %clang_cc1 -triple x86_64-pc-linux-gnu -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -DNO_CROSSCHECK -verify %s
+// RUN: %clang_cc1 -triple x86_64-pc-linux-gnu -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -analyzer-config crosscheck-with-z3=true -verify %s
 // REQUIRES: z3
 
+void clang_analyzer_dump(float);
+
 int foo(int x) 
 {
   int *z = 0;
   if ((x & 1) && ((x & 1) ^ 1))
 #ifdef NO_CROSSCHECK
       return *z; // expected-warning {{Dereference of null pointer (loaded from variable 'z')}}
 #else
       return *z; // no-warning

 void i() {
   _Bool c = nondet_bool();
   if (c) {
     h(1);
   } else {
     h(2);
   }
 }
+
+void floatUnaryNegInEq(int h, int l) {
+  int j;
+  clang_analyzer_dump(-(float)h); // expected-warning-re{{-(float) (reg_${{[0-9]+}}<int h>)}}
+  clang_analyzer_dump((float)l); // expected-warning-re {{(float) (reg_${{[0-9]+}}<int l>)}}
+  if (-(float)h != (float)l) {  // should not crash
+    j += 10;
+    // expected-warning@-1{{garbage}}
+  }
+}
+
+void floatUnaryLNotInEq(int h, int l) {
+  int j;
+  clang_analyzer_dump(!(float)h); // expected-warning{{Unknown}}
+  clang_analyzer_dump((float)l); // expected-warning-re {{(float) (reg_${{[0-9]+}}<int l>)}}
+  if ((!(float)h) != (float)l) {  // should not crash
+    j += 10;
+    // expected-warning@-1{{garbage}}
+  }
+}