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

Thu Sep 10 00:56:02 PDT 2020

steakhal added a comment.

In D83660#2264963 <https://reviews.llvm.org/D83660#2264963>, @OikawaKirie wrote:

> After reviewing the code of this snippet, I think it would be very difficult to make a regression test case for the crash, as far as what I know about Z3 and SMT solvers.
>
> First of all, all calls to `Solver->check()` will return `true` for sat, `false` for unsat, and empty for a timeout.
> On line 132, the manager invokes Z3 for solving the constraints under the current state.
> On line 137, the manager invokes Z3 for getting a model (a valid result) satisfying the constraints.
> On line 141, the manager adds another constraint to exclude the model gotten from the model.
> On line 149, the manager invokes Z3 for solving the excluded constraint.
> In summary, the manager will first solver the constraint for a result of the queried symbolic variable. If there is a valid value, it excludes the value and solves again to check whether it is the only valid result.
>
> To trigger the crash, we need to construct a group of constraints that are sat. Then, we need to exclude a valid value for a symbolic variable and make the constraints lead to a **timeout** (rather than an unsat). Simple linear constraints have very few chances to lead to a timeout. I tried to create a group of constraints from https://stackoverflow.com/questions/20536435/z3-what-might-be-the-reason-for-timeout, which are a group of non-linear unsat constraints that can trigger a timeout (under a timeout of 10 seconds). However, I have not successfully made one, as it has too many things to do with mathematics. And my SMT solver colleagues also think it is quite difficult to make one.

I suspected this one due to my previous investigation.

> As far as I am thinking, it is also very tricky to trigger a constraint solver timeout. Since it can be impacted by which version of the constraint solver is used, how much time is set for the timeout, how fast your computer runs, and so on. Chances are that even if I reproduced the crash with a test case, the same test case may not work on your computer.

I highly agree.
This was the exact reason why I raised a discussion on the mailing list <http://lists.llvm.org/pipermail/cfe-dev/2020-August/066557.html> about //Limit Z3 without timeouts//.
That way we could reproduce this crash without depending on the actual machine.
However, we would still depend on an implementation detail of the solver - and I suspect that this option is highly Z3 specific, so would not fit into the solver-agnostic API very well.
I'm still open to discuss any ideas regarding this, but I can't put any effort into that :|

> Is it possible to hack the SMT solver creator to make a mock solver for triggering the problem?

I suspect, no. We don't have a mechanism to do dependency injection into the SMT constant manager implementation. It would be nice to have IMO.

I see two options here:

1. Implement the dependency injection to let the //SMT constant manager implementation// use the given //SMT solver//. Create a mock solver and a unit-test.
2. Implement the //resource limit// option in the API. Introduce a flag driving this option and create a LIT test where we set this limit to a really small one, and check a toy example.

I think the second option is easier and the preferred one. At the same time, that would require a greater consensus about changing the corresponding API since that is potentially used by different out-of-tree projects of LLVM.

Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D83660