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

[Dominic Chen via Phabricator via cfe-commits]

ddcc added inline comments.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:60
+    // Set timeout to 15000ms = 15s
+    Z3_set_param_value(Config, "timeout", "15000");
+  }
----------------
xazax.hun wrote:
> Sorry for being a bit late in the party, I was wondering whether this timeout can be a source of non-determinism. The constraint solver might get lucky or unlucky based on the load or the underlying hardware to solve some of the constraints. We might end up with different results over different runs which can be confusing for the users. Is there any other way, to set something like a timeout, like limiting the number of steps inside the solver?
I believe Z3 uses various heuristics internally, so the exact execution trace can differ between multiple executions. However, I don't believe that this would be a common issue, since queries on fixed-width bitvector are decidable. The 15 sec timeout is intended to prevent a single query from stalling the static analyzer; I've only experienced this with complex queries over floating-point types (e.g. D28953 + D28954 + D28955), which can degenerate to bitblasting. I don't have the exact numbers right now, but given that the 200+ tests in the testsuite complete in ~90 secs with this patch, the average time per test is < 0.5 sec, which includes tens if not hundreds of individual SMT queries. As far as I know, this timeout parameter is the only support configuration parameter. I'd also like to point out that this solver isn't used unless the user both builds with it and specifies it at runtime.


https://reviews.llvm.org/D28952