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