[PATCH] D105340: [analyzer] Produce SymbolCast symbols for integral types in SValBuilder::evalCast

[Denys Petrov via Phabricator via cfe-commits]

ASDenysPetrov added a comment.

Thank you @martong.
I'll load it ASAP. It's great to see symcasts is closer.

Shame on me :) I'm mixed up in my own patches. I forgot that I separated them 
consciously for this purpose.


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

https://reviews.llvm.org/D105340

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

[PATCH] D105340: [analyzer] Produce SymbolCast symbols for integral types in SValBuilder::evalCast

[Gabor Marton via Phabricator via cfe-commits]

martong added a comment.

In D105340#3237430 , @ASDenysPetrov 
wrote:

> In D105340#3232671 , @NoQ wrote:
>
>> This looks great with the option flag. Landing this patch will enable more 
>> people to test the new mode and produce feedback on whether the constraint 
>> solver keeps working well enough in presence of the new symbols.
>
> Many thanks for your approval, @NoQ! The upset thing is that to get this 
> loaded we also should close this parent revision D103094 
>  :-(

Actually, this patch does not depend on `castTo` and thus it is independent 
from the rest of the patch stack. So we could just land it as it is. (In this 
patch, you just create the `SymbolCast`s but there is no handling of that in 
the constraint manager which needs the `castTo`.)


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

https://reviews.llvm.org/D105340

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

[PATCH] D105340: [analyzer] Produce SymbolCast symbols for integral types in SValBuilder::evalCast

[Denys Petrov via Phabricator via cfe-commits]

ASDenysPetrov added a comment.

In D105340#3232671 , @NoQ wrote:

> This looks great with the option flag. Landing this patch will enable more 
> people to test the new mode and produce feedback on whether the constraint 
> solver keeps working well enough in presence of the new symbols.

Many thanks for your approval, @NoQ! The upset thing is that to get this loaded 
we also should close this parent revision D103094 
 :-(


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

https://reviews.llvm.org/D105340

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

[PATCH] D105340: [analyzer] Produce SymbolCast symbols for integral types in SValBuilder::evalCast

[Artem Dergachev via Phabricator via cfe-commits]

NoQ accepted this revision.
NoQ added a comment.
This revision is now accepted and ready to land.

This looks great with the option flag. Landing this patch will enable more 
people to test the new mode and produce feedback on whether the constraint 
solver keeps working well enough in presence of the new symbols.




Comment at: clang/lib/StaticAnalyzer/Core/SValBuilder.cpp:1004
+  QualType CastTy) {
+  // We use seven conditions to recognize a simplification case.
+  // For the clarity let `CastTy` be `C`, SE->getType() - `T`, root type - `R`,

I really hope these are correct with respect to sign extension 爛



Comment at: clang/test/Analysis/produce-symbolcast_x64.cpp:15
+void test_schar(schar x) {
+  clang_analyzer_dump(x); // expected-warning{{reg_$0}}
+

There's `clang_analyzer_denote()`/`clang_analyzer_express()` which is slightly 
better because it avoids testing the specific dump format (so we could change 
it more easily if we want). No pressure though, if it's too much work to re-do 
then let's keep them as is.


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

https://reviews.llvm.org/D105340

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

[PATCH] D105340: [analyzer] Produce SymbolCast symbols for integral types in SValBuilder::evalCast

[Denys Petrov via Phabricator via cfe-commits]

ASDenysPetrov added a comment.

Just a ping. I'd like to have this patch stack loaded somewhen :)


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

https://reviews.llvm.org/D105340

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

[PATCH] D105340: [analyzer] Produce SymbolCast symbols for integral types in SValBuilder::evalCast

[Denys Petrov via Phabricator via cfe-commits]

ASDenysPetrov updated this revision to Diff 374270.
ASDenysPetrov added a comment.

Rebased.


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

https://reviews.llvm.org/D105340

Files:
  clang/include/clang/StaticAnalyzer/Checkers/SValExplainer.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h
  clang/lib/StaticAnalyzer/Checkers/ExprInspectionChecker.cpp
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
  clang/lib/StaticAnalyzer/Core/SymbolManager.cpp
  clang/test/Analysis/symbol-integral-cast.cpp

Index: clang/test/Analysis/symbol-integral-cast.cpp
===
--- /dev/null
+++ clang/test/Analysis/symbol-integral-cast.cpp
@@ -0,0 +1,374 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection -analyzer-config eagerly-assume=false -analyzer-config support-symbolic-integer-casts=true -verify %s
+
+template 
+void clang_analyzer_eval(T);
+void clang_analyzer_warnIfReached();
+
+typedef short int16_t;
+typedef int int32_t;
+typedef unsigned short uint16_t;
+typedef unsigned int uint32_t;
+
+void test1(int x) {
+  // Even if two lower bytes of `x` equal to zero, it doesn't mean that
+  // the entire `x` is zero. We are not able to know the exact value of x.
+  // It can be one of  65536 possible values like [0, 65536, 131072, ...]
+  // and so on. To avoid huge range sets we still assume `x` in the range
+  // [INT_MIN, INT_MAX].
+  if (!(short)x) {
+if (!x)
+  clang_analyzer_warnIfReached(); // expected-warning {{REACHABLE}}
+else
+  clang_analyzer_warnIfReached(); // expected-warning {{REACHABLE}}
+  }
+}
+
+void test2(int x) {
+  // If two lower bytes of `x` equal to zero, and we know x to be 65537,
+  // which is not truncated to short as zero. Thus the branch is infisible.
+  short s = x;
+  if (!s) {
+if (x == 65537)
+  clang_analyzer_warnIfReached(); // no-warning
+else
+  clang_analyzer_warnIfReached(); // expected-warning {{REACHABLE}}
+  }
+}
+
+void test3(int x, short s) {
+  s = x;
+  if ((short)x > -10 && s < 10) {
+if (x > 0 && x < 10) {
+  // If the range of the whole variable was constrained then reason again
+  // about truncated bytes to make the ranges more precise.
+  clang_analyzer_eval((short)x <= 0); // expected-warning {{FALSE}}
+}
+  }
+}
+
+void test4(unsigned x) {
+  if ((char)x > 8) {
+// Constraint the range of the lowest byte of `x` to [9, CHAR_MAX].
+// The original range of `x` still remains [0, UINT_MAX].
+clang_analyzer_eval((char)x < 42); // expected-warning {{UNKNOWN}}
+if (x < 42) {
+  // Constraint the original range to [0, 42] and update (re-constraint)
+  // the range of the lowest byte of 'x' to [9, 42].
+  clang_analyzer_eval((char)x < 42); // expected-warning {{TRUE}}
+}
+  }
+}
+
+void test5(unsigned x) {
+  if ((char)x > -10 && (char)x < 10) {
+if ((short)x == 8) {
+  // If the range of higher bytes(short) was constrained then reason again
+  // about smaller truncated ranges(char) to make it more precise.
+  clang_analyzer_eval((char)x == 8);  // expected-warning {{TRUE}}
+  clang_analyzer_eval((short)x == 8); // expected-warning {{TRUE}}
+  // We still assume full version of `x` in the range [INT_MIN, INT_MAX].
+  clang_analyzer_eval(x == 8); // expected-warning {{UNKNOWN}}
+}
+  }
+}
+
+void test6(int x) {
+  // Even if two lower bytes of `x` less than zero, it doesn't mean that `x`
+  // can't be greater than zero. Thence we don't change the native range of
+  // `x` and this branch is feasible.
+  if (x > 0)
+if ((short)x < 0)
+  clang_analyzer_eval(x > 0); // expected-warning {{TRUE}}
+}
+
+void test7(int x) {
+  // The range of two lower bytes of `x` [1, SHORT_MAX] is enough to cover
+  // all possible values of char [CHAR_MIN, CHAR_MAX]. So the lowest byte
+  // can be lower than zero.
+  if ((short)x > 0) {
+if ((char)x < 0)
+  clang_analyzer_warnIfReached(); // expected-warning {{REACHABLE}}
+else
+  clang_analyzer_warnIfReached(); // expected-warning {{REACHABLE}}
+  }
+}
+
+void test8(int x) {
+  // Promotion from `signed int` to `signed long long` also reasoning about the
+  // original range, because we know the fact that even after promotion it
+  // remains in the range [INT_MIN, INT_MAX].
+  if ((long long)x < 0)
+clang_analyzer_eval(x < 0); // expected-warning {{TRUE}}
+}
+
+void test9(signed int x) {
+  // Any cast `signed` to `unsigned` produces an unsigned range, which is
+  // [0, UNSIGNED_MAX] and can not be lower than zero.
+  if ((unsigned long long)x < 0)
+clang_analyzer_warnIfReached(); // no-warning
+  else
+clang_analyzer_warnIfReached(); // expected-warning {{REACHABLE}}
+
+  if ((unsigned int)x < 0)
+clang_analyzer_warnIfReached(); // no-warning
+  else
+clang_analyzer_warnIfReached(); // expected-warning 

[PATCH] D105340: [analyzer] Produce SymbolCast symbols for integral types in SValBuilder::evalCast

[Denys Petrov via Phabricator via cfe-commits]

ASDenysPetrov added a comment.

In D105340#2855387 , @vsavchenko 
wrote:

> Also, although the test is very extensive, it is pretty lopsided at the same 
> time.  C-style cast is only one case out of the myriad of all explicit and, 
> more importantly, implicit casts.

I agree in a part of size, but these C-style casts generates the same AST tree 
as all other ex/implicit forms of casts . Though, casts can look completely 
differently but at a low level they are very similar.
Here is an example:

  void test(long x) {
(llong)(short)(char)x; 
  }
  
  FunctionDecl 0xbc306b8  line:1:6 test 'void (long)'
|-ParmVarDecl 0xbc305f0  col:16 used x 'long'
`-CompoundStmt 0xbc9f4b0 
  `-CStyleCastExpr 0xbc9f488  'long long' 
`-ImplicitCastExpr 0xbc9f470  'long long' 
 part_of_explicit_cast
  `-CStyleCastExpr 0xbc9f430  'short' 
`-ImplicitCastExpr 0xbc9f418  'short' 
 part_of_explicit_cast
  `-CStyleCastExpr 0xbc9f3d8  'char' 
`-ImplicitCastExpr 0xbc9f3c0  'char'  
part_of_explicit_cast
  `-ImplicitCastExpr 0xbc9f3a8  'long'  
part_of_explicit_cast
`-DeclRefExpr 0xbc9f378  'long' lvalue ParmVar 
0xbc305f0 'x' 'long'

and

  void test(long x) {  
char c = x;
if(static_cast(c) == -1ll);
  }
  
  `-FunctionDecl 0xbc606b8  line:1:6 test 'void (long)'
|-ParmVarDecl 0xbc605f0  col:16 used x 'long'
`-CompoundStmt 0xbcd0598 
  |-DeclStmt 0xbcd0450 
  | `-VarDecl 0xbcd0398  col:8 used c 'char' cinit
  |   `-ImplicitCastExpr 0xbcd0438  'char' 
  | `-ImplicitCastExpr 0xbcd0420  'long' 
  |   `-DeclRefExpr 0xbcd0400  'long' lvalue ParmVar 0xbc605f0 
'x' 'long'
  `-IfStmt 0xbcd0578 
|-BinaryOperator 0xbcd0550  'bool' '=='
| |-ImplicitCastExpr 0xbcd0538  'long long' 

| | `-CXXStaticCastExpr 0xbcd04d0  'short' 
static_cast 
| |   `-ImplicitCastExpr 0xbcd04b8  'short'  
part_of_explicit_cast
| | `-ImplicitCastExpr 0xbcd04a0  'char'  
part_of_explicit_cast
| |   `-DeclRefExpr 0xbcd0468  'char' lvalue Var 0xbcd0398 
'c' 'char'
| `-UnaryOperator 0xbcd0520  'long long' prefix '-'
|   `-IntegerLiteral 0xbcd0500  'long long' 1
`-NullStmt 0xbcd0570 

We can see similar `IntegralCast` for both variants. I was aiming to generate 
all the cases of `IntegralCast` and C-style cast is enough for me.




Comment at: clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def:318
+ANALYZER_OPTION(bool, ShouldHandleIntegralCastForRanges,
+"handle-integral-cast-for-ranges",
+"Handle truncations, promotions and conversions for ranges of "

vsavchenko wrote:
> BTW, mb it should be less specific?  Something like 
> `ShouldSupportSymbolicIntegerCasts`?
> BTW 2, do you even plan on supporting symbolic casts in other cases?
> ShouldSupportSymbolicIntegerCasts?
Thanks. I thought about an appropriate name but failed to come up. That's what 
we need!
> BTW 2, do you even plan on supporting symbolic casts in other cases?
I think about adding //bool-int//, //int-bool//, //ptr-int//, //int-ptr// to 
the list.


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

https://reviews.llvm.org/D105340

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

[PATCH] D105340: [analyzer] Produce SymbolCast symbols for integral types in SValBuilder::evalCast

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko added inline comments.



Comment at: clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def:318
+ANALYZER_OPTION(bool, ShouldHandleIntegralCastForRanges,
+"handle-integral-cast-for-ranges",
+"Handle truncations, promotions and conversions for ranges of "

BTW, mb it should be less specific?  Something like 
`ShouldSupportSymbolicIntegerCasts`?
BTW 2, do you even plan on supporting symbolic casts in other cases?


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

https://reviews.llvm.org/D105340

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

[PATCH] D105340: [analyzer] Produce SymbolCast symbols for integral types in SValBuilder::evalCast

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko added a comment.

Also, even though the test is very extensive it is pretty lopsided at the same 
time.  C-style cast is only one case out of the myriad of all explicit and, 
more importantly, implicit casts.


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

https://reviews.llvm.org/D105340

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

[PATCH] D105340: [analyzer] Produce SymbolCast symbols for integral types in SValBuilder::evalCast

[Denys Petrov via Phabricator via cfe-commits]

ASDenysPetrov added inline comments.



Comment at: clang/test/Analysis/produce-symbolcast.cpp:1
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection 
-analyzer-config handle-integral-cast-for-ranges=true -verify %s
+

steakhal wrote:
> vsavchenko wrote:
> > ASDenysPetrov wrote:
> > > vsavchenko wrote:
> > > > This test is failing on my desktop, when I downloaded your patch:
> > > > ```
> > > > error: 'warning' diagnostics expected but not seen: 
> > > >   File .../produce-symbolcast.cpp Line 67: (long) (reg_$0)
> > > >   File .../produce-symbolcast.cpp Line 79: (long long) ((unsigned long) 
> > > > (reg_$0))
> > > >   File .../produce-symbolcast.cpp Line 122: (unsigned long) 
> > > > (reg_$0)
> > > >   File .../produce-symbolcast.cpp Line 134: (unsigned long long) 
> > > > ((unsigned long) (reg_$0))
> > > >   File .../produce-symbolcast.cpp Line 192: (long) (reg_$0)
> > > >   File .../produce-symbolcast.cpp Line 204: (long long) ((unsigned 
> > > > long) (reg_$0))
> > > >   File .../produce-symbolcast.cpp Line 247: (unsigned long) 
> > > > (reg_$0)
> > > >   File .../produce-symbolcast.cpp Line 259: (unsigned long long) 
> > > > ((unsigned long) (reg_$0))
> > > >   File .../produce-symbolcast.cpp Line 317: (long) (reg_$0)
> > > >   File .../produce-symbolcast.cpp Line 329: (long long) ((unsigned 
> > > > long) (reg_$0))
> > > >   File .../produce-symbolcast.cpp Line 372: (unsigned long) (reg_$0 > > > x>)
> > > >   File .../produce-symbolcast.cpp Line 384: (unsigned long long) 
> > > > ((unsigned long) (reg_$0))
> > > >   File .../produce-symbolcast.cpp Line 448: (long long) (reg_$0)
> > > >   File .../produce-symbolcast.cpp Line 454: (long long) ((unsigned 
> > > > long) (reg_$0))
> > > >   File .../produce-symbolcast.cpp Line 492: (unsigned long) 
> > > > (reg_$0)
> > > >   File .../produce-symbolcast.cpp Line 497: (unsigned long) 
> > > > (reg_$0)
> > > >   File .../produce-symbolcast.cpp Line 503: (unsigned long long) 
> > > > (reg_$0)
> > > >   File .../produce-symbolcast.cpp Line 509: (unsigned long long) 
> > > > ((unsigned long) (reg_$0))
> > > >   File .../produce-symbolcast.cpp Line 562: (long) (reg_$0)
> > > >   File .../produce-symbolcast.cpp Line 567: (long) (reg_$0)
> > > >   File .../produce-symbolcast.cpp Line 574: (long) (reg_$0)
> > > >   File .../produce-symbolcast.cpp Line 579: (unsigned long) 
> > > > (reg_$0)
> > > >   File .../produce-symbolcast.cpp Line 617: (unsigned long) 
> > > > (reg_$0)
> > > >   File .../produce-symbolcast.cpp Line 622: (unsigned long) 
> > > > (reg_$0)
> > > >   File .../produce-symbolcast.cpp Line 629: (unsigned long long) 
> > > > ((long) (reg_$0))
> > > >   File .../produce-symbolcast.cpp Line 634: (unsigned long long) 
> > > > ((unsigned long) (reg_$0))
> > > >   File .../produce-symbolcast.cpp Line 937: (long) (reg_$0)
> > > >   File .../produce-symbolcast.cpp Line 949: (long long) ((long) 
> > > > (reg_$0))
> > > >   File .../produce-symbolcast.cpp Line 992: (unsigned long) 
> > > > (reg_$0)
> > > >   File .../produce-symbolcast.cpp Line 1004: (unsigned long long) 
> > > > ((long) (reg_$0))
> > > >   File .../produce-symbolcast.cpp Line 1062: (long) (reg_$0)
> > > >   File .../produce-symbolcast.cpp Line 1067: (long) (reg_$0)
> > > >   File .../produce-symbolcast.cpp Line 1074: (long long) ((long) 
> > > > (reg_$0))
> > > >   File .../produce-symbolcast.cpp Line 1078: (long long) (reg_$0 > > > x>)
> > > >   File .../produce-symbolcast.cpp Line 1129: (unsigned long long) 
> > > > ((long) (reg_$0))
> > > >   File .../produce-symbolcast.cpp Line 1133: (unsigned long long) 
> > > > (reg_$0)
> > > >   File .../produce-symbolcast.cpp Line 1187: (long) (reg_$0)
> > > >   File .../produce-symbolcast.cpp Line 1192: (long) (reg_$0)
> > > >   File .../produce-symbolcast.cpp Line 1199: (long long) ((long) 
> > > > (reg_$0))
> > > >   File .../produce-symbolcast.cpp Line 1204: (long long) ((unsigned 
> > > > long) (reg_$0))
> > > >   File .../produce-symbolcast.cpp Line 1242: (unsigned long) 
> > > > (reg_$0)
> > > >   File .../produce-symbolcast.cpp Line 1247: (unsigned long) 
> > > > (reg_$0)
> > > >   File .../produce-symbolcast.cpp Line 1254: (unsigned long long) 
> > > > ((long) (reg_$0))
> > > >   File .../produce-symbolcast.cpp Line 1259: (unsigned long long) 
> > > > ((unsigned long) (reg_$0))
> > > > error: 'warning' diagnostics seen but not expected: 
> > > >   File .../produce-symbolcast.cpp Line 67: (long) ((unsigned int) 
> > > > (reg_$0)) [debug.ExprInspection]
> > > >   File .../produce-symbolcast.cpp Line 79: (long long) (reg_$0) 
> > > > [debug.ExprInspection]
> > > >   File .../produce-symbolcast.cpp Line 122: (unsigned long) ((unsigned 
> > > > int) (reg_$0)) [debug.ExprInspection]
> > > >   File .../produce-symbolcast.cpp Line 134: (unsigned long long) 
> > > > (reg_$0) [debug.ExprInspection]
> > > >   File .../produce-symbolcast.cpp Line 192: (long) ((unsigned int) 
> > > > (reg_$0)) 

[PATCH] D105340: [analyzer] Produce SymbolCast symbols for integral types in SValBuilder::evalCast

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

steakhal added inline comments.



Comment at: clang/test/Analysis/produce-symbolcast.cpp:1
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection 
-analyzer-config handle-integral-cast-for-ranges=true -verify %s
+

vsavchenko wrote:
> ASDenysPetrov wrote:
> > vsavchenko wrote:
> > > This test is failing on my desktop, when I downloaded your patch:
> > > ```
> > > error: 'warning' diagnostics expected but not seen: 
> > >   File .../produce-symbolcast.cpp Line 67: (long) (reg_$0)
> > >   File .../produce-symbolcast.cpp Line 79: (long long) ((unsigned long) 
> > > (reg_$0))
> > >   File .../produce-symbolcast.cpp Line 122: (unsigned long) (reg_$0 > > x>)
> > >   File .../produce-symbolcast.cpp Line 134: (unsigned long long) 
> > > ((unsigned long) (reg_$0))
> > >   File .../produce-symbolcast.cpp Line 192: (long) (reg_$0)
> > >   File .../produce-symbolcast.cpp Line 204: (long long) ((unsigned long) 
> > > (reg_$0))
> > >   File .../produce-symbolcast.cpp Line 247: (unsigned long) (reg_$0 > > x>)
> > >   File .../produce-symbolcast.cpp Line 259: (unsigned long long) 
> > > ((unsigned long) (reg_$0))
> > >   File .../produce-symbolcast.cpp Line 317: (long) (reg_$0)
> > >   File .../produce-symbolcast.cpp Line 329: (long long) ((unsigned long) 
> > > (reg_$0))
> > >   File .../produce-symbolcast.cpp Line 372: (unsigned long) (reg_$0 > > x>)
> > >   File .../produce-symbolcast.cpp Line 384: (unsigned long long) 
> > > ((unsigned long) (reg_$0))
> > >   File .../produce-symbolcast.cpp Line 448: (long long) (reg_$0)
> > >   File .../produce-symbolcast.cpp Line 454: (long long) ((unsigned long) 
> > > (reg_$0))
> > >   File .../produce-symbolcast.cpp Line 492: (unsigned long) (reg_$0 > > x>)
> > >   File .../produce-symbolcast.cpp Line 497: (unsigned long) (reg_$0 > > x>)
> > >   File .../produce-symbolcast.cpp Line 503: (unsigned long long) 
> > > (reg_$0)
> > >   File .../produce-symbolcast.cpp Line 509: (unsigned long long) 
> > > ((unsigned long) (reg_$0))
> > >   File .../produce-symbolcast.cpp Line 562: (long) (reg_$0)
> > >   File .../produce-symbolcast.cpp Line 567: (long) (reg_$0)
> > >   File .../produce-symbolcast.cpp Line 574: (long) (reg_$0)
> > >   File .../produce-symbolcast.cpp Line 579: (unsigned long) (reg_$0 > > x>)
> > >   File .../produce-symbolcast.cpp Line 617: (unsigned long) (reg_$0 > > x>)
> > >   File .../produce-symbolcast.cpp Line 622: (unsigned long) (reg_$0 > > x>)
> > >   File .../produce-symbolcast.cpp Line 629: (unsigned long long) ((long) 
> > > (reg_$0))
> > >   File .../produce-symbolcast.cpp Line 634: (unsigned long long) 
> > > ((unsigned long) (reg_$0))
> > >   File .../produce-symbolcast.cpp Line 937: (long) (reg_$0)
> > >   File .../produce-symbolcast.cpp Line 949: (long long) ((long) 
> > > (reg_$0))
> > >   File .../produce-symbolcast.cpp Line 992: (unsigned long) (reg_$0 > > x>)
> > >   File .../produce-symbolcast.cpp Line 1004: (unsigned long long) ((long) 
> > > (reg_$0))
> > >   File .../produce-symbolcast.cpp Line 1062: (long) (reg_$0)
> > >   File .../produce-symbolcast.cpp Line 1067: (long) (reg_$0)
> > >   File .../produce-symbolcast.cpp Line 1074: (long long) ((long) 
> > > (reg_$0))
> > >   File .../produce-symbolcast.cpp Line 1078: (long long) (reg_$0)
> > >   File .../produce-symbolcast.cpp Line 1129: (unsigned long long) ((long) 
> > > (reg_$0))
> > >   File .../produce-symbolcast.cpp Line 1133: (unsigned long long) 
> > > (reg_$0)
> > >   File .../produce-symbolcast.cpp Line 1187: (long) (reg_$0)
> > >   File .../produce-symbolcast.cpp Line 1192: (long) (reg_$0)
> > >   File .../produce-symbolcast.cpp Line 1199: (long long) ((long) 
> > > (reg_$0))
> > >   File .../produce-symbolcast.cpp Line 1204: (long long) ((unsigned long) 
> > > (reg_$0))
> > >   File .../produce-symbolcast.cpp Line 1242: (unsigned long) 
> > > (reg_$0)
> > >   File .../produce-symbolcast.cpp Line 1247: (unsigned long) 
> > > (reg_$0)
> > >   File .../produce-symbolcast.cpp Line 1254: (unsigned long long) ((long) 
> > > (reg_$0))
> > >   File .../produce-symbolcast.cpp Line 1259: (unsigned long long) 
> > > ((unsigned long) (reg_$0))
> > > error: 'warning' diagnostics seen but not expected: 
> > >   File .../produce-symbolcast.cpp Line 67: (long) ((unsigned int) 
> > > (reg_$0)) [debug.ExprInspection]
> > >   File .../produce-symbolcast.cpp Line 79: (long long) (reg_$0) 
> > > [debug.ExprInspection]
> > >   File .../produce-symbolcast.cpp Line 122: (unsigned long) ((unsigned 
> > > int) (reg_$0)) [debug.ExprInspection]
> > >   File .../produce-symbolcast.cpp Line 134: (unsigned long long) 
> > > (reg_$0) [debug.ExprInspection]
> > >   File .../produce-symbolcast.cpp Line 192: (long) ((unsigned int) 
> > > (reg_$0)) [debug.ExprInspection]
> > >   File .../produce-symbolcast.cpp Line 204: (long long) (reg_$0) 
> > > [debug.ExprInspection]
> > >   File .../produce-symbolcast.cpp Line 247: (unsigned long) ((unsigned 
> > > int) (reg_$0)) 

[PATCH] D105340: [analyzer] Produce SymbolCast symbols for integral types in SValBuilder::evalCast

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko added inline comments.



Comment at: clang/test/Analysis/produce-symbolcast.cpp:1
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection 
-analyzer-config handle-integral-cast-for-ranges=true -verify %s
+

ASDenysPetrov wrote:
> vsavchenko wrote:
> > This test is failing on my desktop, when I downloaded your patch:
> > ```
> > error: 'warning' diagnostics expected but not seen: 
> >   File .../produce-symbolcast.cpp Line 67: (long) (reg_$0)
> >   File .../produce-symbolcast.cpp Line 79: (long long) ((unsigned long) 
> > (reg_$0))
> >   File .../produce-symbolcast.cpp Line 122: (unsigned long) (reg_$0)
> >   File .../produce-symbolcast.cpp Line 134: (unsigned long long) ((unsigned 
> > long) (reg_$0))
> >   File .../produce-symbolcast.cpp Line 192: (long) (reg_$0)
> >   File .../produce-symbolcast.cpp Line 204: (long long) ((unsigned long) 
> > (reg_$0))
> >   File .../produce-symbolcast.cpp Line 247: (unsigned long) (reg_$0 > x>)
> >   File .../produce-symbolcast.cpp Line 259: (unsigned long long) ((unsigned 
> > long) (reg_$0))
> >   File .../produce-symbolcast.cpp Line 317: (long) (reg_$0)
> >   File .../produce-symbolcast.cpp Line 329: (long long) ((unsigned long) 
> > (reg_$0))
> >   File .../produce-symbolcast.cpp Line 372: (unsigned long) (reg_$0)
> >   File .../produce-symbolcast.cpp Line 384: (unsigned long long) ((unsigned 
> > long) (reg_$0))
> >   File .../produce-symbolcast.cpp Line 448: (long long) (reg_$0)
> >   File .../produce-symbolcast.cpp Line 454: (long long) ((unsigned long) 
> > (reg_$0))
> >   File .../produce-symbolcast.cpp Line 492: (unsigned long) (reg_$0)
> >   File .../produce-symbolcast.cpp Line 497: (unsigned long) (reg_$0)
> >   File .../produce-symbolcast.cpp Line 503: (unsigned long long) 
> > (reg_$0)
> >   File .../produce-symbolcast.cpp Line 509: (unsigned long long) ((unsigned 
> > long) (reg_$0))
> >   File .../produce-symbolcast.cpp Line 562: (long) (reg_$0)
> >   File .../produce-symbolcast.cpp Line 567: (long) (reg_$0)
> >   File .../produce-symbolcast.cpp Line 574: (long) (reg_$0)
> >   File .../produce-symbolcast.cpp Line 579: (unsigned long) (reg_$0 > x>)
> >   File .../produce-symbolcast.cpp Line 617: (unsigned long) (reg_$0 > x>)
> >   File .../produce-symbolcast.cpp Line 622: (unsigned long) (reg_$0 > x>)
> >   File .../produce-symbolcast.cpp Line 629: (unsigned long long) ((long) 
> > (reg_$0))
> >   File .../produce-symbolcast.cpp Line 634: (unsigned long long) ((unsigned 
> > long) (reg_$0))
> >   File .../produce-symbolcast.cpp Line 937: (long) (reg_$0)
> >   File .../produce-symbolcast.cpp Line 949: (long long) ((long) 
> > (reg_$0))
> >   File .../produce-symbolcast.cpp Line 992: (unsigned long) (reg_$0)
> >   File .../produce-symbolcast.cpp Line 1004: (unsigned long long) ((long) 
> > (reg_$0))
> >   File .../produce-symbolcast.cpp Line 1062: (long) (reg_$0)
> >   File .../produce-symbolcast.cpp Line 1067: (long) (reg_$0)
> >   File .../produce-symbolcast.cpp Line 1074: (long long) ((long) 
> > (reg_$0))
> >   File .../produce-symbolcast.cpp Line 1078: (long long) (reg_$0)
> >   File .../produce-symbolcast.cpp Line 1129: (unsigned long long) ((long) 
> > (reg_$0))
> >   File .../produce-symbolcast.cpp Line 1133: (unsigned long long) 
> > (reg_$0)
> >   File .../produce-symbolcast.cpp Line 1187: (long) (reg_$0)
> >   File .../produce-symbolcast.cpp Line 1192: (long) (reg_$0)
> >   File .../produce-symbolcast.cpp Line 1199: (long long) ((long) 
> > (reg_$0))
> >   File .../produce-symbolcast.cpp Line 1204: (long long) ((unsigned long) 
> > (reg_$0))
> >   File .../produce-symbolcast.cpp Line 1242: (unsigned long) (reg_$0 > x>)
> >   File .../produce-symbolcast.cpp Line 1247: (unsigned long) (reg_$0 > x>)
> >   File .../produce-symbolcast.cpp Line 1254: (unsigned long long) ((long) 
> > (reg_$0))
> >   File .../produce-symbolcast.cpp Line 1259: (unsigned long long) 
> > ((unsigned long) (reg_$0))
> > error: 'warning' diagnostics seen but not expected: 
> >   File .../produce-symbolcast.cpp Line 67: (long) ((unsigned int) 
> > (reg_$0)) [debug.ExprInspection]
> >   File .../produce-symbolcast.cpp Line 79: (long long) (reg_$0) 
> > [debug.ExprInspection]
> >   File .../produce-symbolcast.cpp Line 122: (unsigned long) ((unsigned int) 
> > (reg_$0)) [debug.ExprInspection]
> >   File .../produce-symbolcast.cpp Line 134: (unsigned long long) 
> > (reg_$0) [debug.ExprInspection]
> >   File .../produce-symbolcast.cpp Line 192: (long) ((unsigned int) 
> > (reg_$0)) [debug.ExprInspection]
> >   File .../produce-symbolcast.cpp Line 204: (long long) (reg_$0) 
> > [debug.ExprInspection]
> >   File .../produce-symbolcast.cpp Line 247: (unsigned long) ((unsigned int) 
> > (reg_$0)) [debug.ExprInspection]
> >   File .../produce-symbolcast.cpp Line 259: (unsigned long long) 
> > (reg_$0) [debug.ExprInspection]
> >   File .../produce-symbolcast.cpp Line 317: (long) ((unsigned int) 
> > (reg_$0)) [debug.ExprInspection]

[PATCH] D105340: [analyzer] Produce SymbolCast symbols for integral types in SValBuilder::evalCast

[Denys Petrov via Phabricator via cfe-commits]

ASDenysPetrov added a comment.

I will update the patch soon according to your suggestions.




Comment at: clang/test/Analysis/bool-assignment.c:46-50
 #ifdef ANALYZER_CM_Z3
 BOOL x = y; // expected-warning {{Assignment of a non-Boolean value}}
 #else
-BOOL x = y; // no-warning
+BOOL x = y; // expected-warning {{Assignment of a non-Boolean value}}
 #endif

vsavchenko wrote:
> If Z3 and not Z3 are the same now, we can simply merge two cases and remove 
> preprocessor directive.
+1



Comment at: clang/test/Analysis/produce-symbolcast.cpp:1
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection 
-analyzer-config handle-integral-cast-for-ranges=true -verify %s
+

vsavchenko wrote:
> This test is failing on my desktop, when I downloaded your patch:
> ```
> error: 'warning' diagnostics expected but not seen: 
>   File .../produce-symbolcast.cpp Line 67: (long) (reg_$0)
>   File .../produce-symbolcast.cpp Line 79: (long long) ((unsigned long) 
> (reg_$0))
>   File .../produce-symbolcast.cpp Line 122: (unsigned long) (reg_$0)
>   File .../produce-symbolcast.cpp Line 134: (unsigned long long) ((unsigned 
> long) (reg_$0))
>   File .../produce-symbolcast.cpp Line 192: (long) (reg_$0)
>   File .../produce-symbolcast.cpp Line 204: (long long) ((unsigned long) 
> (reg_$0))
>   File .../produce-symbolcast.cpp Line 247: (unsigned long) (reg_$0)
>   File .../produce-symbolcast.cpp Line 259: (unsigned long long) ((unsigned 
> long) (reg_$0))
>   File .../produce-symbolcast.cpp Line 317: (long) (reg_$0)
>   File .../produce-symbolcast.cpp Line 329: (long long) ((unsigned long) 
> (reg_$0))
>   File .../produce-symbolcast.cpp Line 372: (unsigned long) (reg_$0)
>   File .../produce-symbolcast.cpp Line 384: (unsigned long long) ((unsigned 
> long) (reg_$0))
>   File .../produce-symbolcast.cpp Line 448: (long long) (reg_$0)
>   File .../produce-symbolcast.cpp Line 454: (long long) ((unsigned long) 
> (reg_$0))
>   File .../produce-symbolcast.cpp Line 492: (unsigned long) (reg_$0)
>   File .../produce-symbolcast.cpp Line 497: (unsigned long) (reg_$0)
>   File .../produce-symbolcast.cpp Line 503: (unsigned long long) (reg_$0 x>)
>   File .../produce-symbolcast.cpp Line 509: (unsigned long long) ((unsigned 
> long) (reg_$0))
>   File .../produce-symbolcast.cpp Line 562: (long) (reg_$0)
>   File .../produce-symbolcast.cpp Line 567: (long) (reg_$0)
>   File .../produce-symbolcast.cpp Line 574: (long) (reg_$0)
>   File .../produce-symbolcast.cpp Line 579: (unsigned long) (reg_$0)
>   File .../produce-symbolcast.cpp Line 617: (unsigned long) (reg_$0)
>   File .../produce-symbolcast.cpp Line 622: (unsigned long) (reg_$0)
>   File .../produce-symbolcast.cpp Line 629: (unsigned long long) ((long) 
> (reg_$0))
>   File .../produce-symbolcast.cpp Line 634: (unsigned long long) ((unsigned 
> long) (reg_$0))
>   File .../produce-symbolcast.cpp Line 937: (long) (reg_$0)
>   File .../produce-symbolcast.cpp Line 949: (long long) ((long) (reg_$0 x>))
>   File .../produce-symbolcast.cpp Line 992: (unsigned long) (reg_$0)
>   File .../produce-symbolcast.cpp Line 1004: (unsigned long long) ((long) 
> (reg_$0))
>   File .../produce-symbolcast.cpp Line 1062: (long) (reg_$0)
>   File .../produce-symbolcast.cpp Line 1067: (long) (reg_$0)
>   File .../produce-symbolcast.cpp Line 1074: (long long) ((long) 
> (reg_$0))
>   File .../produce-symbolcast.cpp Line 1078: (long long) (reg_$0)
>   File .../produce-symbolcast.cpp Line 1129: (unsigned long long) ((long) 
> (reg_$0))
>   File .../produce-symbolcast.cpp Line 1133: (unsigned long long) 
> (reg_$0)
>   File .../produce-symbolcast.cpp Line 1187: (long) (reg_$0)
>   File .../produce-symbolcast.cpp Line 1192: (long) (reg_$0)
>   File .../produce-symbolcast.cpp Line 1199: (long long) ((long) 
> (reg_$0))
>   File .../produce-symbolcast.cpp Line 1204: (long long) ((unsigned long) 
> (reg_$0))
>   File .../produce-symbolcast.cpp Line 1242: (unsigned long) (reg_$0 x>)
>   File .../produce-symbolcast.cpp Line 1247: (unsigned long) (reg_$0 x>)
>   File .../produce-symbolcast.cpp Line 1254: (unsigned long long) ((long) 
> (reg_$0))
>   File .../produce-symbolcast.cpp Line 1259: (unsigned long long) ((unsigned 
> long) (reg_$0))
> error: 'warning' diagnostics seen but not expected: 
>   File .../produce-symbolcast.cpp Line 67: (long) ((unsigned int) 
> (reg_$0)) [debug.ExprInspection]
>   File .../produce-symbolcast.cpp Line 79: (long long) (reg_$0) 
> [debug.ExprInspection]
>   File .../produce-symbolcast.cpp Line 122: (unsigned long) ((unsigned int) 
> (reg_$0)) [debug.ExprInspection]
>   File .../produce-symbolcast.cpp Line 134: (unsigned long long) (reg_$0 x>) [debug.ExprInspection]
>   File .../produce-symbolcast.cpp Line 192: (long) ((unsigned int) 
> (reg_$0)) [debug.ExprInspection]
>   File .../produce-symbolcast.cpp Line 204: (long long) (reg_$0) 
> [debug.ExprInspection]
>   File .../produce-symbolcast.cpp Line 

[PATCH] D105340: [analyzer] Produce SymbolCast symbols for integral types in SValBuilder::evalCast

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko added inline comments.



Comment at: clang/test/Analysis/range_casts.c:125-126
   if (index - 1UL == 0L) // Was not reached prior fix.
-clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+// Tempopary regression in scope of implementing integral cast.
+// This will be restored as soon as all commits are loaded.
+clang_analyzer_warnIfReached(); // no-warning

The main purpose of the new option is exactly to prevent "temporary 
regressions" so that everything works just as it did before


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D105340

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

[PATCH] D105340: [analyzer] Produce SymbolCast symbols for integral types in SValBuilder::evalCast

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko added a comment.

Hey, thanks for starting on splitting into more pieces!




Comment at: 
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h:96
QualType OriginalTy);
+  SVal simplifySymbolCast(nonloc::SymbolVal V, QualType CastTy);
 

What does it do and what should I give it?



Comment at: clang/lib/StaticAnalyzer/Core/SValBuilder.cpp:510-546
-// Handles casts of type CK_IntegralCast.
-// At the moment, this function will redirect to evalCast, except when the 
range
-// of the original value is known to be greater than the max of the target 
type.
-SVal SValBuilder::evalIntegralCast(ProgramStateRef state, SVal val,
-   QualType castTy, QualType originalTy) {
-  // No truncations if target type is big enough.
-  if (getContext().getTypeSize(castTy) >= getContext().getTypeSize(originalTy))

I'd like to see the motivation about why this code is removed.
My main concern is this:
  * If removing `evalIntegralCast` is essential for this feature and is not an 
NFC: it should also obey the new analyzer option.
  * If it is NFC, and we can safely remove this function no matter what the 
value of the option is, it should be a separate patch.



Comment at: clang/test/Analysis/bool-assignment.c:46-50
 #ifdef ANALYZER_CM_Z3
 BOOL x = y; // expected-warning {{Assignment of a non-Boolean value}}
 #else
-BOOL x = y; // no-warning
+BOOL x = y; // expected-warning {{Assignment of a non-Boolean value}}
 #endif

If Z3 and not Z3 are the same now, we can simply merge two cases and remove 
preprocessor directive.



Comment at: clang/test/Analysis/produce-symbolcast.cpp:1
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection 
-analyzer-config handle-integral-cast-for-ranges=true -verify %s
+

This test is failing on my desktop, when I downloaded your patch:
```
error: 'warning' diagnostics expected but not seen: 
  File .../produce-symbolcast.cpp Line 67: (long) (reg_$0)
  File .../produce-symbolcast.cpp Line 79: (long long) ((unsigned long) 
(reg_$0))
  File .../produce-symbolcast.cpp Line 122: (unsigned long) (reg_$0)
  File .../produce-symbolcast.cpp Line 134: (unsigned long long) ((unsigned 
long) (reg_$0))
  File .../produce-symbolcast.cpp Line 192: (long) (reg_$0)
  File .../produce-symbolcast.cpp Line 204: (long long) ((unsigned long) 
(reg_$0))
  File .../produce-symbolcast.cpp Line 247: (unsigned long) (reg_$0)
  File .../produce-symbolcast.cpp Line 259: (unsigned long long) ((unsigned 
long) (reg_$0))
  File .../produce-symbolcast.cpp Line 317: (long) (reg_$0)
  File .../produce-symbolcast.cpp Line 329: (long long) ((unsigned long) 
(reg_$0))
  File .../produce-symbolcast.cpp Line 372: (unsigned long) (reg_$0)
  File .../produce-symbolcast.cpp Line 384: (unsigned long long) ((unsigned 
long) (reg_$0))
  File .../produce-symbolcast.cpp Line 448: (long long) (reg_$0)
  File .../produce-symbolcast.cpp Line 454: (long long) ((unsigned long) 
(reg_$0))
  File .../produce-symbolcast.cpp Line 492: (unsigned long) (reg_$0)
  File .../produce-symbolcast.cpp Line 497: (unsigned long) (reg_$0)
  File .../produce-symbolcast.cpp Line 503: (unsigned long long) (reg_$0)
  File .../produce-symbolcast.cpp Line 509: (unsigned long long) ((unsigned 
long) (reg_$0))
  File .../produce-symbolcast.cpp Line 562: (long) (reg_$0)
  File .../produce-symbolcast.cpp Line 567: (long) (reg_$0)
  File .../produce-symbolcast.cpp Line 574: (long) (reg_$0)
  File .../produce-symbolcast.cpp Line 579: (unsigned long) (reg_$0)
  File .../produce-symbolcast.cpp Line 617: (unsigned long) (reg_$0)
  File .../produce-symbolcast.cpp Line 622: (unsigned long) (reg_$0)
  File .../produce-symbolcast.cpp Line 629: (unsigned long long) ((long) 
(reg_$0))
  File .../produce-symbolcast.cpp Line 634: (unsigned long long) ((unsigned 
long) (reg_$0))
  File .../produce-symbolcast.cpp Line 937: (long) (reg_$0)
  File .../produce-symbolcast.cpp Line 949: (long long) ((long) (reg_$0))
  File .../produce-symbolcast.cpp Line 992: (unsigned long) (reg_$0)
  File .../produce-symbolcast.cpp Line 1004: (unsigned long long) ((long) 
(reg_$0))
  File .../produce-symbolcast.cpp Line 1062: (long) (reg_$0)
  File .../produce-symbolcast.cpp Line 1067: (long) (reg_$0)
  File .../produce-symbolcast.cpp Line 1074: (long long) ((long) (reg_$0))
  File .../produce-symbolcast.cpp Line 1078: (long long) (reg_$0)
  File .../produce-symbolcast.cpp Line 1129: (unsigned long long) ((long) 
(reg_$0))
  File .../produce-symbolcast.cpp Line 1133: (unsigned long long) (reg_$0)
  File .../produce-symbolcast.cpp Line 1187: (long) (reg_$0)
  File .../produce-symbolcast.cpp Line 1192: (long) (reg_$0)
  File .../produce-symbolcast.cpp Line 1199: (long long) ((long) (reg_$0))
  File .../produce-symbolcast.cpp Line 1204: (long long) ((unsigned long) 
(reg_$0))
  File