xazax.hun marked an inline comment as done.
xazax.hun added inline comments.
================
Comment at: clang/lib/StaticAnalyzer/Checkers/FuchsiaHandleChecker.cpp:336-338
+ProgramStateRef FuchsiaHandleChecker::evalAssume(ProgramStateRef State,
+ SVal Cond,
+ bool Assumption) const {
----------------
xazax.hun wrote:
> NoQ wrote:
> > Ok, so you're basically saying that whenever the code under analysis does
> > anything to check the return value, this callback will fire immediately?
> > Thus guaranteeing that whenever the Schrödinger state is accessed, it's
> > either already collapsed or indeed not checked yet?
> >
> > This sounds right but i wish i had your confidence :D
> >
> > My usual approach to Schrödinger states will be to do the same thing but in
> > `checkDeadSymbols()`. I.e., when the return value symbol dies, see if it's
> > constrained and collapse the state accordingly. If the access occurs
> > earlier than symbol death, update the state according to the current
> > constraints and forget about the symbol. If current constraints are
> > insufficient, conservatively mark it as a successful release (as that's how
> > non-paranoid code under analysis would behave).
> >
> > Regardless of the approach, you still need to update the state upon access
> > as if the release has succeeded (when the current state is a Schrödinger
> > state). But with your approach you can avoid checking the constraints upon
> > access, and instead blindly assume that the symbol is underconstrained.
> >
> > I like this! Can we prove that it works by adding an assertion that the
> > return value symbol is underconstrained upon every access to the
> > potentially Schrödinger state?
> Yeah, you got my intention right! I was also thinking about doing this in
> `checkDeadSymbols`, but I was wondering if that is ultimately the right thing
> to do. It might be possible to write code where the symbol for the error code
> becomes dead too late, so we keep the Schrödinger state longer than
> necessary. Redoing this when we access the handle makes sense though! I think
> that could probably perform better compared to my approach with `evalAssume`.
>
> My only problem at this point do not really know when is a handle in a
> Schrödinger state. Do you recommend specifying a distinct state for that?
Hmm, `evalAssume` does not get a `CheckerContext`, so it cannot really use
`SValBuilder` to do more complicated queries, like check if a symbol is greater
or equal to zero rather than just equal to.
I wonder, is this intentional? Should I just use the `checkDeadSymbol` method
instead or should I add `CheckerContext` to `evalAssume`?
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D70470/new/
https://reviews.llvm.org/D70470
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
