[PATCH] D30489: [analyzer] catch out of bounds for VLA

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

xazax.hun added a comment.

In https://reviews.llvm.org/D30489#769916, @NoQ wrote:

> An idea. I believe the safest way to find the bugs you mentioned would be to replace extent-as-a-symbol with extent-as-a-trait.
>
> I.e., currently we construct `extent_$3{SymRegion{conj_$1{char *}}}`, assume that it is equal to `reg_$0<int X>` (which produces a `SymSymExpr`) and then catch more `SymSymExpr`s along the path and compare them to the first one.
>
> Instead, i believe that from the start we should have done something like
>
>   REGISTER_MAP_WITH_PROGRAMSTATE(RegionExtent, const SubRegion *, NonLoc);
>
>
> Then when the VLA is constructed (or memory is malloc'ed or something like that), we just set the `RegionExtent` trait directly to `reg_$0<int X>` and later easily compare it to anything. The region's `getExtent()` method would be modified to consult this trait instead of (or, at least, before) constructing a new symbol.
>
> Ideologically it is the same thing. Technically it produces simpler symbolic expressions, and i believe that both RangeConstraintManager and Z3 would benefit from simpler symbolic expressions.


+1, I like this approach!


Repository:
  rL LLVM

https://reviews.llvm.org/D30489