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

[Balázs Benics via Phabricator via cfe-commits]

This revision was landed with ongoing or failed builds.
This revision was automatically updated to reflect the committed changes.
Closed by commit rG3674421c4bc0: [analyzer] Fix assertion failure in SMT 
conversion for unary operator on floats (authored by 
tomasz-kaminski-sonarsource, committed by steakhal).

Changed prior to commit:
  https://reviews.llvm.org/D140891?vs=485977&id=492466#toc

Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D140891/new/

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@-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}}
+  }
+}
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,7 +454,9 @@
       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.



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@-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}}
+  }
+}
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,7 +454,9 @@
       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.

_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits