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

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

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.


Repository:
  rL LLVM

https://reviews.llvm.org/D30489