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

[Balázs Benics via Phabricator via cfe-commits]

steakhal added a comment.

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.


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

https://reviews.llvm.org/D124244