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

[Ella Ma via Phabricator via cfe-commits]

OikawaKirie added a comment.

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.

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.

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


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D83660