[PATCH] D28952: [analyzer] Add new Z3 constraint manager backend

[Nuno Lopes via Phabricator via cfe-commits]

nlopes added a comment.

Cool work Dominic!
Just a few random comments from the peanut gallery regarding the usage of Z3:

- I would definitely split the Z3Expr into expr/solver/model classes. Several advantages: plugging in new solvers becomes easier and reference counting can be handled more safely and automatically. Right now your solver+model related code handled ref-counting "by hand", which can easily lead to bugs.
- I would add an rvalue constructor to the expr class to avoid ref-counting when unneeded.
- Function z3Expr::fromData() seems to be able to create arbitrarily-sized bit-vectors.  I would limit to e.g. 512 bits or something like that.  Z3 is super slow with huge bit-vectors. If you feel fancy (for a following version of this feature), you could encode this information lazily (based on the model).
- Z3Expr::fromInt() -- why take a string as input and not a uin64_t?
- Why call simplify before asserting a constraint?  That's usually a pretty slow thing to do (in my experience).
- You should replace Z3_mk_solver() with something fancier.  If you don't feel fancy, just use Z3_mk_simple_solver()  (simple is short for simplifying btw).  If you know the theory of the constraints (e.g., without floats, it would be QF_BV), you should use Z3_mk_solver_for_theory()  (or whatever the name was).  If you feel really fancy, you could roll your own tactic (in my tools I often have a tactic class to build my own tactics; Z3 even allows you to case split on the theory after simplifications)
- Instead of asserting multiple constraints to the solver, I would and() them and assert just once (plays nicer with some preprocessors of Z3)
- Timeout: SMT solvers sometimes go crazy and take forever.  I would advise to add a timeout to the solver to avoid getting caught on a trap.  This timeout can be different for the two use cases: check if a path is feasible (lower timeout), or check if you actually have a bug (higher timeout)
- Also, I didn't see anything regarding memory (I might have missed yet).  Are you using the array theory?  If so, I would probably advise benchmarking it carefully since Z3's support for arrays is not great (even though it has improved a bit in the last year or so).

BTW, adding small amount of constant folding in the expression builder is usually good, since you save time in Z3 preprocessor. Especially if you want to go for smallish timeouts (likely).  If you want to be fancy, you can also canonicalize expressions like Z3 likes (e.g., only ule/sle, no slt, sgt, etc).


https://reviews.llvm.org/D28952