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