[WIP] Sketch Z3 custom tactic

[delcypher]

This depends on #658 EDIT: Now merged

This PR sketches implementing a custom tactic for using Z3 which I suspect will give us a performance boost. The tactic is the one sketched in #653 .

The implementation isn't really ideal

• We should just reset the solver rather than re-constructing it for every query. Without measuring I don't know which is faster though.
• The tactic builder API is a little clumsy. If this PR seems useful we should probably give Z3TacticHandle a "fluent" API so we write things like t.then(x).then(y).then(z).

What we need to do now is benchmark this. I'd like to know

• What is the performance of -z3-custom-tactic=array_ackermannize_to_qfbv vs -z3-custom-tactic=none.
• How both of the above compare to STP.

@MartinNowack / @andreamattavelli : Seeing as you have the infrastructure for this when you have time would you be able to conduct these experiments?

Please use a recent version of Z3 for this ( 2834fea9b3977f2988c528e221ff51fa12bfbe52 ). I suspect the one we use in TravisCI is too old

[delcypher]

Hmm

-z3-custom-tactic=array_ackermannize_to_qfbv

Seems to break the Feature/StatesCoveringNew.c test. The requested counter example value (klee_prefer_cex(&x, x == 0)) is not respected and the test fails.

I think this is exposing a bug the in CounterExampleCache somewhere. If I pass -use-cex-cache=false to KLEE for this test, it passes.

When using -search=dfs I don't see any divergence in the recorded instructions between -z3-custom-tactic=array_ackermannize_to_qfbv and -z3-custom-tactic=none.

I also took at the queries Z3 was receiving with -use-cex-cache=true. None of them reflect KLEE checking to see if x == 0 is satisfiable.

[delcypher]

Note. Might also be related to tactic option for bvarray2uf.

- bvarray2uf Rewrite bit-vector arrays into bit-vector (uninterpreted) functions.
    produce_models (bool) (default: false) model generation.

[delcypher]

@ccadar @andreamattavelli @MartinNowack
This looks promising. The custom tactic makes the tests run noticeably faster.

$ lit -vs --param klee_opts=-z3-custom-tactic=none test
Testing Time: 25.17s
....

$ lit -vs --param klee_opts=-z3-custom-tactic=array_ackermannize_to_qfbv test/
Testing Time: 15.74s
....

[ccadar]

Cool. I guess there might be an argument here for performing "ackermannization" in KLEE directly.

[delcypher]

@ccadar

Cool. I guess there might be an argument here for performing "ackermannization" in KLEE directly.

I'm not completely convinced that there is. What we are seeing here is the internal implementation details of Z3 manifesting as performance differences. The array ackermannization we are performing here is reducing the QF_ABV problem to QF_BV problem which lets Z3 use its faster SAT solver. For QF_ABV queries Z3 I think Z3 uses its slower smt tactic. IIRC the STP paper actually talks about this saying that the nelson oppen approach (I think this is the same as the smt tactic) is slow and that bit blasting to a SAT problem can be faster.

Even though we implemented "array ackermannization" in our fork of KLEE that added floating point support it's not as sophisticated as what Z3's tactic does here. My implementation of "array ackermannization" in our fork of KLEE can only ackermannize arrays if all reads are performed at constant indices and there are no symbolic writes performed to array being read. Z3's tactic seems to be able to handle the non-symbolic case too (see Z3Prover/z3#1150 (comment) ). My implementation in our fork of KLEE is also crude and only works with Z3 anyway. This is because KLEE's expression language doesn't have bitvector variables (it only supports arrays) I am forced to do the expression transformation at the level of Z3 expressions.

I'd also argue that what this PR doing is exactly what Z3's tactic interface was built for: customising Z3's strategy for solving queries for a particular use case.

I'd like to see something resembling this PR merged in the not to distant future but there are a few things to do.

• Benchmark this. I'd like @andreamattavelli to run this PR (with and without the option enabled) so we can compare the performance. I'd also be interested to see how this compares against STP.
• Clean up the code. This code is a little bit hacky (e.g. uses C++11 feature) so it needs cleaning up. We also need to enforce the Z3 version is >= 4.5 or add some runtime checks because the ackermannize_bv tactic is only available in Z3 4.5 and newer
• Decide whether or not we want to use this custom tactic by default

[delcypher]

@andreamattavelli Any chance you could benchmark this PR using your infrastructure?

Configuration

• Current Z3 implementation: -solver-backend=z3 -z3-custom-tactic=none
• Custom Z3 tactic: -solver-backend=z3 -z3-custom-tactic=array_ackermannize_to_qfbv
• STP: -solver-backend=stp

If you do this please use a very recent Z3 build (i.e. 0f1583309d0813e87d6003fe46cf8bb32899d773).

[andreamattavelli]

@delcypher yes, I can. I can not promise I will do it this week, sorry.

(The problem is that the infrastructure runs STP only, so I also need to modify the build scripts. It is not an impossible job, it is just time-consuming)

[delcypher]

@andreamattavelli

@delcypher yes, I can. I can not promise I will do it this week, sorry.

Okay thanks. I was hoping for this week because I'm giving a talk about Z3 tactics on Thursday and a performance win/loss would be interesting to discuss but it's not that important :)

[andreamattavelli]

@delcypher

Okay thanks. I was hoping for this week because I'm giving a talk about Z3 tactics on Thursday and a performance win/loss would be interesting to discuss but it's not that important :)

I'll try to update and run everything, but I'm not 100% sure to finish by Thursday.

[ccadar]

Given the age of the PR, I will close it, but place it in the Extensions project at https://github.com/klee/klee/projects/4, so that others can build up on it if there is interest.