[PATCH] D12358: [Analyzer] Handling constant bound loops

[Ted Kremenek via cfe-commits]

krememek added a comment.

In http://reviews.llvm.org/D12358#235142, @seaneveson wrote:

> If I refactor this patch in its current state into a separate file and put it behind a flag, would it then be acceptable?  I would then like to take some time to look at the invalidation improvements as discussed in this thread.


I think I'd like to see two things, primarily:

1. The logic behind and -analyzer-config option.
2. Very basic invalidation of values, as Anna suggests, to make this patch minimally viable.

For the latter, I think there is a simple solution.  Notice on ProgramState there is a method called `invalidateRegions`.  This is a worklist algorithm that takes a set of memory regions, and invalidates all memory regions (including checker state) that is touched by those regions, or reachable via memory bindings, etc.  It's the complete transitive closure.  To get the conservative invalidation that Anna suggests (actually, a little less conservative), I think you can just pass in a two MemRegions as the input to that method and get a new ProgramState with the appropriate regions invalidated.  That MemRegions are the MemRegion corresponding to the current stack frame, specifically divided into locals and parameters.  You can get them by getting the current StackFrameContext (which you get from the LocationContext), and using the following two methods form MemRegionManager:

  getStackLocalsRegion(const StackFrameContext *STC);
  getStackArgumentsRegion(const StackFrameContext *STC);

Those two MemRegions will be the parent regions of all VarRegions, etc. on the current stack frame.  If you pass those to `invalidateRegions`, that will invalidate all memory on the current stack frame, and anything they reference.

Actually, it would probably be also good to pass in the MemRegion returned by `getGlobalsRegion()` as well, to invalidate all global memory.  But just those three will give the conservative invalidation Anna suggested, and would give a viable initial version of the patch (which should still be guarded under a flag).  All told, that's probably about 10 lines of code.

With that, I think you would have a viable initial patch, and something that would be meaningfully testable.

Thank you for working on this!


http://reviews.llvm.org/D12358