[PATCH] D103096: [analyzer] Implement cast for ranges of symbolic integers

[Gabor Marton via Phabricator via cfe-commits]

martong added a comment.

Thanks Denys for your continued work on this. These are very good questions that must be answered, we need exactly such thinking to implement this properly. I believe we can advance gradually.

In D103096#3642681 <https://reviews.llvm.org/D103096#3642681>, @ASDenysPetrov wrote:

> @martong Thank you for your patience. I started moving to a bit another direction that we can improving it iteratively.
> Just spoiling, in my latest solution a single symbol will be associated to many classes. Here are also tricky cases:
>
> ---
>
> Consider equalities
>
>   a32 == (int8)b32
>   b32 == c32
>
> Class-Symbol map is:
>
>   class1 { a32 , (int8)b32 }
>   class2 { b32 , c32 }
>
> Symbol-Class map is:
>
>   a32 { 32 : class1 }
>   b32 {  8 : class1, 32 : class2  }
>   c32 { 32 : class2 }
>
> If we know:
>
>   (int8)c32 == -1
>
> then what is:
>
>   (int8)a32 - ?
>
> Should we traverse like `a ->  32 -> class1 -> (int8)b32 -> b32 ->  class2 -> c32 -> (int8)c32 ` ?

I think, we should have only `a ->  32 -> class1 -> (int8)b32`. The `(int8)b32 -> b32` step would be incorrect according to the modulo logic.
With other words, we should check the equivalence class of the root symbol (and no other eq classes should be considered), in this case this is only `class1`. (More precisely we should check the `SymCastMap` of `class1`.)

> ---
>
> The `x8 == y32` we can treat as a range of `int8` ( {-128, 127} or  {0, 255} ).

I am not sure what you mean here.
You mean, when we bifurcate on `x8 == y32` ? Then we have two branches, the false case `x8 == y32`: [0, 0] and `x8 == y32`: [[INT_MIN, -1], [1,INT_MAX]]

> ---
>
> For `(int8)x32 == (int16)x32` we can eliminate one of the symbols in the class a s a redundant one.

Yes, but this is more like an optimization step. I'd handle this with low priority and with a FIXME comment.

> ---
>
> If `x32 == 0` then we can simplify next classes `(int16)x32 == y` and `(int8)x32 == z` merging them into a single class {x32, y, z}.

Good point. This is an optimization for precision. I'd like to have this, but in a subsequent patch. Let's try to have the absolute simplest working version in this patch.
Also, this can extend to any concrete value that is meaningful in the smaller types. E.g. any single value of x32 in [0,127] could simplify (int8)x32.

> I believe there are more cases.

Yes. Consider liveness for example. We should remove the class from `SymCastMap` if the class itself becomes dead. This should be part of this patch.


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

https://reviews.llvm.org/D103096