[PATCH] D124244: [analyzer] add StoreToImmutable and ModelConstQualifiedReturn checkers

[Zurab Tsinadze via Phabricator via cfe-commits]

zukatsinadze added a comment.

In D124244#3588671 <https://reviews.llvm.org/D124244#3588671>, @steakhal wrote:

> Sorry for my late reply.
>
> It feels like we have some serious obstacles.
> The `check::PostCall` handler wants to mark some memory region immutable. Currently, the checker creates a new //symbolic// memregion, spawned into the //immutable// memory space. After this it simply re-binds the return value.
> However, only `eval::Call` handler is supposed (**must**) to bind the return value, so the current implementation cannot land.
>
> I played with the trait idea, which was this:
>
> 1. Introduce a new program state trait with the `REGISTER_SET_WITH_PROGRAMSTATE(ImmutableRegions, const ento::MemRegion *)`. One should not bind values to these regions. (*)
> 2. The `check::PostCall` would simply insert into this set.
> 3. The `StoreToImmutableChecker`, at the `check::Bind` handler, would verify that the region is not contained by the set - otherwise emit a report...
> 4. Surface this new trait to be reachable by the `Core` infrastructure.
> 5. Refactor all the `Core` functions introducing or expecting `MemRegionManager::getGlobalsRegion`s to insert the region in question into this `ImmutableRegions` set associated with the current `State`, producing some new `State`.
>
> The last point is the most critical. Now, by design, `MemRegionManager` does not refer to the `ProgramState`, hence we don't have one that we could mutate by inserting into the `ImmutableRegions` set. Passing a `ProgramStateRef` along all the functions is a nightmare. Trust me, I've tried it.
> That being said, eradicating `GlobalImmutableSpaceRegion` seems to be challenging.
>
> I've settled on using the custom trait, and the `GlobalImmutableSpaceRegion` memspace kind to detect if the store (bind) should be allowed or not.
> F23475561: UsingTraitsForTrackingImmutability.patch <https://reviews.llvm.org/F23475561>
>
> WDYT @NoQ, how could we get rid of the `GlobalImmutableSpaceRegion`?
>
> ---
>
> (*): Originally I wanted a set of `const MemSpaceRegion *`, but it turns out a default eval called function which returns a plain old mutable pointer is of `SymRegion{conj{}}` at the `UnknownSpaceRegion`. And we probably don't want to mark immutable the whole `UnknownSpaceRegion` xD.

@NoQ what do you think about steakhal's proposal?


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

https://reviews.llvm.org/D124244