Profiling Z3 queries

Profiling Z3 queries

Collecting the Z3 queries produced by F*

Shape of the F* invocation:

fstar --z3refresh --log_queries --hint_info [--record_hints | --use_hints] Test.fst

• --z3refresh: fstar calls a fresh Z3 instance for each query, instead of reusing the same for all queries. This is a bit slower, but good for robustness/reproducibility;
• --log_queries: store the queries sent to z3 in .smt2 files (in the current directory). Will overwrite the .smt2 files generated by previous runs;
• --hint_info: print general info to stdout about the queries run, the time taken by z3 to solve them, and whether the hints worked;
• --record_hints: records hints;
• --use_hints: after a previous invocation with --record_hints, try to use the recorded hints.

The smt2 files produced by a run with --use_hints should be smaller, as F* can rely on the hints to prune the context.

Interpreting the results

• Note the difference in verification time per query based on whether or not hint successfully replays.

  If there is a large discrepancy in time, then this suggests that there are assertions in the context that are causing Z3 to search and instantiate quantifiers needlessly.

  We can profile two runs of Z3, using the pruned and non-pruned smt2 files produced by two runs of F*, without hints and with hints. Then diff the two profiles to see what part of the context is causing on of the proofs to go slowly, using qprofdiff.

  z3 smt.qi.profile=true a.smt2 > a.prof
  z3 smt.qi.profile=true b.smt2 > b.prof
  qprofdiff -si a.prof b.prof
  

• More thorough profiling can be achieved using the Z3 Axiom profiler.

  To produce an execution trace, run:

  z3 trace=true foo.smt2
  

  This will produce a z3.log file, which can be fed to the profiler (the trace_file_name option can be used to change the trace filename).

• If there are any queries whose hints fail to replay, then it is generally useful to understand exactly why this is the case.

  Suppose query q.smt2 has an unsat core u. And suppose q-u.smt2, the pruning of q to only include those assertions from u, cannot be proven unsat by Z3.

  We'd like to find out a minimal set of assertions from q, which when added to q-u allow it to be proven unsat. Call this set the "completions" of u.

  Using Z3 4.5.1, we can pass these options to F*:

  --z3cliopt smt.core.extend_patterns=true --z3cliopt smt.core.extend_patterns.max_distance=n
  

  to get it to try to compute a completion of u, for some metric n (larger n should produce larger completions; so we want to try with the smallest n first).

  Sometimes, the completion reported by Z3 will be too large to be of much use.
  In such cases, resorting to bisection search through q to help find a completion of u may help...