[PATCH] D83660: [analyzer] Fix a crash for dereferencing an empty llvm::Optional variable in SMTConstraintManager.h.

[Balázs Benics via Phabricator via cfe-commits]

steakhal added inline comments.


================
Comment at: clang/test/Analysis/z3/Inputs/MockZ3_solver_check.c:6
+
+// Mock implementation: return UNDEF for the 5th invocation, otherwise it just
+// returns the result of the real invocation.
----------------
martong wrote:
> It's not clear why we have to wait for the 5th invocation. Can't we return UNDEF for the first time? That would eliminate the need to call the originalFN. 
> 
> By the way why do we have call the original, can't we just return immediately with Z3_L_TRUE?
Excellent questions, I should have clarified these upfront!

> It's not clear why we have to wait for the 5th invocation.
Probably lies in how the exploded graph is built up. I was also surprised that it was hit exactly 5 times.

> Can't we return UNDEF for the first time?
That way we would not reach the 2nd `Solver->check()` call, just simply early return.

> That would eliminate the need to call the originalFN.
Unfortunately, the side-effect is also required. `Solver->check()` creates a model which is accessed by `Solver->getInterpretation(Exp, Value)`. I don't really want to mock that representation as well. We could though.
I'm gonna have a look at that.

> By the way why do we have call the original, can't we just return immediately with Z3_L_TRUE?
We could, but as we have to call the original regardless, there is no point doing that.
This way it can mimic the exact behavior that the Z3 would do, and diverge only for the 5th time.


CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D83660/new/

https://reviews.llvm.org/D83660