[llvm-branch-commits] [clang] c8d5733 - [analyzer] Fix assertion failure in SMT conversion for unary operator on floats

[Tom Stellard via llvm-branch-commits]

Author: Tomasz Kamiński
Date: 2023-03-03T23:48:04-08:00
New Revision: c8d5733b81b7534b91c3602ad96053b4ba0b638b

URL: https://github.com/llvm/llvm-project/commit/c8d5733b81b7534b91c3602ad96053b4ba0b638b
DIFF: https://github.com/llvm/llvm-project/commit/c8d5733b81b7534b91c3602ad96053b4ba0b638b.diff

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

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 D125318
and their handling for Z3 in D125547.

Patch by Tomasz Kamiński.

Reviewed By: mikhail.ramalho

Differential Revision: https://reviews.llvm.org/D140891

(cherry picked from commit 3674421c4bc0cd3b65b8f1feaaf7038ac2d47ca8)

Added: 
    

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

Removed: 
    


################################################################################
diff  --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index ea05b9f8ee3fe..fcc9c02999b3b 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -454,7 +454,9 @@ class SMTConv {
       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.

diff  --git a/clang/test/Analysis/z3-crosscheck.c b/clang/test/Analysis/z3-crosscheck.c
index 7711597eb9ec8..e0ec028c518d3 100644
--- a/clang/test/Analysis/z3-crosscheck.c
+++ b/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 @@ void i() {
     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}}
+  }
+}