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
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
