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 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
