[PATCH] D78933: [analyzer] RangeConstraintManager optimizations in comparison expressions

[Gábor Horváth via Phabricator via cfe-commits]

xazax.hun added inline comments.


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:588
+  // AnyX2 means that two expressions marked as `Any` are met in code,
+  // and there is a special column for that, for example:
+  // if (x >= y)
----------------
xazax.hun wrote:
> ASDenysPetrov wrote:
> > xazax.hun wrote:
> > > I have really hard time processing how to interpret `AnyX2`.
> > > 
> > > For example in the code below:
> > > ```
> > >    if (x >= y)
> > >      if (x != y)
> > >        if (x <= y)
> > >          return false
> > > ```
> > > 
> > > ```
> > >    if (x >= y)
> > >      if (x == y)
> > >        if (x <= y)
> > >          return true
> > > ```
> > > 
> > > We would get different results for `<=`. So I do not really get how I should read the `AnyX2` column.
> > I'm sorry for the obscure explanation. I was really thinking about how to explain it more clear.
> > Let's consider this code:
> > ```
> > if (x >= y)
> >   if (x != y)
> >     if (x <= y)
> > ```
> > If 'x >= y' is //true//, then following `x <= y` is  `Any` ( can be //true// or //false// ). //See table in the summary.//
> > If 'x != y' is //true//, then following `x <= y` is  `Any` ( can be //true// or //false// ).
> > If 'x >= y && x != y' is //true//, then following `x <= y` is `False` only (it means that we previously met two Any states, what I've called as **AnyX2**).
> > 
> > 
> > 
> > 
> Could you tell me how the reasoning would be different for 
> ```
> if (x >= y)
>   if (x == y)
>     if (x <= y)
> ```
> ?
Oh never mind, after `x == y` the `x <= y` would be `true`. But still, I find this logic hard to explain, understand, and prove correct.
I'd like to see at least some informal reasoning why will it always work. Also, if someone would like to extend this table in the future (e.g. with operator <=>), how to make it in such a way that does not break this logic.


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

https://reviews.llvm.org/D78933