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@-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,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,
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,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,
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
