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

[Tomasz Kamiński via Phabricator via cfe-commits]

tomasz-kaminski-sonarsource created this revision.
Herald added subscribers: steakhal, manas, ASDenysPetrov, dkrupp, donat.nagy, Szelethus, mikhail.ramalho, a.sidorin, szepet, baloghadamsoftware, xazax.hun.
Herald added a reviewer: NoQ.
Herald added a project: All.
tomasz-kaminski-sonarsource requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.

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 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.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D140891

Files:
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
  clang/test/Analysis/z3-crosscheck.c


Index: clang/test/Analysis/z3-crosscheck.c
===================================================================
--- clang/test/Analysis/z3-crosscheck.c
+++ clang/test/Analysis/z3-crosscheck.c
@@ -1,7 +1,9 @@
-// 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;
@@ -55,3 +57,23 @@
     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 at -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 at -1{{garbage}}
+  }
+}
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
===================================================================
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -454,6 +454,8 @@
       llvm::SMTExprRef OperandExp =
           getSymExpr(Solver, Ctx, USE->getOperand(), &OperandTy, hasComparison);
       llvm::SMTExprRef UnaryExp =
+          OperandTy->isRealFloatingType() ?
+          fromFloatUnOp(Solver, USE->getOpcode(), OperandExp) :
           fromUnOp(Solver, USE->getOpcode(), OperandExp);
 
       // Currently, without the `support-symbolic-integer-casts=true` option,


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D140891.485977.patch
Type: text/x-patch
Size: 2272 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20230103/70152b46/attachment.bin>