NoQ added inline comments.
================
Comment at:
clang/include/clang/StaticAnalyzer/Core/PathSensitive/MemRegion.h:767-768
s->getType()->isBlockPointerType());
- assert(isa<UnknownSpaceRegion>(sreg) || isa<HeapSpaceRegion>(sreg));
+ assert(isa<UnknownSpaceRegion>(sreg) || isa<HeapSpaceRegion>(sreg) ||
+ isa<GlobalSystemSpaceRegion>(sreg));
}
----------------
steakhal wrote:
> NoQ wrote:
> > steakhal wrote:
> > > At this point, I'm not even sure if we should assert any of these.
> > I mean, ideally this should be just `UnknownSpaceRegion`. For everything
> > else we should have made a fresh `MemRegion` class. It is absurd that the
> > same numeric address value (represented the symbol `s`) can correspond to
> > two (now three) different locations in memory.
> From my perspective, a symbolic region is just a region that we don't know
> what its parent region is - let it be part of an object or an entire memory
> space.
> The memory space is what we use for communicating some constraints on where
> that symbolic region.
> E.g. a symbolic region of a stack memory space should never alias with any
> memory region of the heap memory space.
>
> > It is absurd that the same numeric address value (represented the symbol s)
> > can correspond to two (now three) different locations in memory.
> IMO a given `s` should indeed refer to a single location in memory, but
> that's not a property we can enforce here in the constructor.
> And my guess is that by removing this assertion, we would still have this
> invariant. What we should do instead, put an assertion into the
> `SymbolManager`, to enforce that with the same `s` symbol, one cannot
> construct two `SymbolicRegions` with different memory spaces.
> Alternatively, we could remove the memory space from the `Profile` to map to
> the same entity in the Map; which would enforce this invariant on its own.
> WDYT?
> The memory space is what we use for communicating some constraints on where
> that symbolic region.
I agree that it's a constraint. And as such, I believe it shouldn't be made
part of the region's //identity//. Just like "$x < 5" is not a field inside
symbol $x but a separate state trait. Similarly we can turn `SymbolicRegion`'s
memory space constraint into a state trait. Then we can express more
sophisticated constraints ("this symbolic region is either on the heap or a
global variable but definitely not a local variable"), or we can have
constraints become more precise over time ("this symbolic region was compared
as "less than" another heap region, therefore it itself must be on the heap").
> What we should do instead, put an assertion into the `SymbolManager`, to
> enforce that with the same `s` symbol, one cannot construct two
> `SymbolicRegions` with different memory spaces.
This could be a nice temporary solution.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D120310/new/
https://reviews.llvm.org/D120310
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
