[PATCH] D120310: [clang][analyzer] Add modeling of 'errno' (work-in-progress).

[Artem Dergachev via Phabricator via cfe-commits]

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