QI profiling

[arpj-rebola]

This version enables the --report_qi flag. Each query sequence generates a report when Z3 is killed (this limitation cannot be bypassed, although Z3 can be killed for every query, and the checked queries can be restricted with the "admit" options). The report contains quantifier IDs, number of instantiations, and origins (including module, source file and lines).

[msftclas]

All CLA requirements met.

[nikswamy]

FYI, Adrian and I are discussing this offline and working towards scoping this P.R more tightly to the --report_qi feature

[arpj-rebola]

src/basic/FStar.Options.fs / .fsi : adding --report_qi option

src/basic/FStar.Range.fs / .fsi : adding a distinct range to identify QI ranges coming from the prelude

src/basic/boot/NotFStar.Util.fs / .fsi : this is one of the main issues. Z3 generates output labeled with [quantifier_instances] at any point while it's running, including right before it exits. The previous infrastructure for processes was not able to extract this information, and adapting it requires some nontrivial changes. I also added a few utility functions that could be useful to other people like repeat : int -> string -> string ; I could move those out if needed.

src/basic/ml/FStar_Util.ml : same for OCaml.

src/smtencoding/FStar.SMTEncoding.Encode.fs:1084, 1165 : some terms were created without a range, which would be problematic as this is what I use to extract range information in the QI report. I force term-generating functions to include a range; then I manually added it in the encoding.

src/smtencoding/FStar.SMTEncoding.ErrorReporting.fs : several changes due to a change in the signature of some term-producing functions and the Quant constructor

src/smtencoding/FStar.SMTEncoding.Solver.fs Instead of just calling Z3.ask with a query range, now we pass a record with some data that is useful when generating the QI profile. I also added a few type annotations - I found those quite useful, but if this could be a problem in the future I can take those out.

src//smtencoding/FStar.SMTEncoding.Term.fs :

• One of the main changes here is the internal representation of the prelude. Instead of a decl case for the prelude, now the prelude is a list of decls. The string generated is essentially equivalent to the hardcoded prelude, up to whitespace and alpha-conversion. The reason why I did this is because I need to get the names and ranges of all quantifiers, and doing it this way allows to process every declaration in the same way. For QI profiling it could have probably been done in a few different ways, but once proof processing is added I will really need to access the prelude as a data structure rather than a string.
• The Quant constructor now has a new argument which holds the quantifier id.
• fresh_token must now be given a range, to comply with the aforementioned use of ranges for quantifier ids.
• A minor change: implication is now encoded as "=>" instead of "implies". The reason is that the SMT2 standard does not technically support "implies" as a synonym for "=>".
• Again, lots of type annotations were added. If necessary, they can be removed.
• A function called assign_qids is called when converting a decl to a string. This traverses the SMT internal data structure and assigns a new quantifier id to any quantifier which doesn't yet have one.

src/smtencoding/FStar.SMTEncoding.Z3.fs :

• Several type annotations as above.
• Calls to process functions from FStar.Util have been modified to pass filters
• bgproc now has new functions. "kill" kills the current Z3 process without creating a new one; this is intended to be the last action in F* before producing the last QI profile. "store" saves the current "linearized" query ; "extract" retrieves all linearized queries since the current Z3 process was created. More on linearized queries is written below.
• Many changes were needed to support query linearization. This is probably a target for optimization if QI profile generation becomes a burden.

On linearized queries: one of the problems I found is that declarations, and quantifier IDs within them, can be added and removed through pop and push. This is a problem because I can only analyze QIs after I kill Z3, and there can be several queries until this happens. There are two options here:

• Save every declaration sent to Z3 since the last time it was killed; then, when QIs are analyzed, reconstruct each query according to each pop/push.
• Reconstruct each (complete, without pops/pushes) query at query time, and store them until Z3 is killed.
  The latter is not only easier to implement, but also more compatible with proof analysis (unlike QI profiling, proof analysis triggers after every query). The main tradeoff here is memory - we need enough memory to store the whole relevant history for every query, which is significantly more than just relying on pop/push structure.

[nikswamy]

What is the additional field?

[nikswamy]

remove?

[nikswamy]

style change ... why?

[nikswamy]

There are some stylistic issues with this PR that I would like to discuss. I especially welcome input from @aseemr and @mtzguido, who maintain this code regularly along with myself.

1. Adrian has added type annotations in many places. In some places, I can see it is desirable. Primarily, I see the value of annotations for top-level lets that are not already specified in an interface. However, there are many other places where the annotations arguably add clutter, including many annotations on locally bound lets, e.g, to pick on one example among many:

    let res : string = List.map (declToSmt' z3options print_captions) decls |> String.concat "\n" in

What do you think we should do? Ideally, I would prefer to scope this pull request to strictly what is necessary for the required functionality, leaving stylistic changes to a separate PR. But, that is probably a lot of work. Though it would also produce a smaller and easier to review diff.

2. Another main stylistic change here in FStar.SMTEncoding.Term.fs is the move from a prelude given in Z3 concrete syntax (a string) to one built in abstract syntax. See https://github.com/FStarLang/FStar/pull/1687/files?file-filters%5B%5D=.fs&file-filters%5B%5D=.fsi#diff-545d33165a075bd87a9b5b5d7c399e05R927 Is it an improvement? I guess I'm fine with it. Though it's a bit harder to maintain, this code is not meant to change much. WDYT?

[aseemr]

1. Usually I only annotate top-level definitions, that too only if they are not present in the interface (see e.g. fstar/FStar.CheckedFiles.fs). For locals, my personal preference is also to leave them unannotated (for the same cluttering reason that Nik mentions). This is the same style that we use for F* source files. So if it is not too much work for Adrian, it would be good to be consistent.

2. Yeah, no strong preference here. This code is rarely changed, so even the string was fine. The string representation is probably easier to read and find/debug for this prelude. I would be more worried about making some mistake in this change and then having to dig through the Everest failures to discover it.

Happy to make a reviewing pass myself if you think that's helpful, please let me know.

[arpj-rebola]

Done. Let me know if I can help with something else.

[nikswamy]

Once conflicts and resolved and we have a green from CI, I'd be happy to review further and try to accept.

[nikswamy]

hi Adrian,

Thanks for all the work!

I merged master into this branch and pushed it to nik_1687.

I tried running fstar --report_qi FirstProofs.fst --query_stats in examples/micro-benchmarks, but it seemed to just hang after the last proof was completed without generating any output. I killed the process after waiting for a bit.

Any idea what might be up?

Thanks,
Nik

[nikswamy]

FYI, I also reformatted QIReport.fs in nik_1687, to clean up whitespace, format according to https://github.com/FStarLang/FStar/wiki/Style-guide.

[nikswamy]

About --report_qi hanging. On Windows with Cygwin and OCaml-4.0.5, it seems that the new implementation of kill_process invoked from https://github.com/FStarLang/FStar/blob/nik_1687/src/smtencoding/FStar.SMTEncoding.Z3.fs#L265 just hangs in case there is any quantifier_instance output.

If I kill the z3 process manually, then this unblocks and the process runs to completion (except it produces Failure("could not parse quantifier instantiation info"), which is not surprising, since I killed it unexpectedly).

[nikswamy]

@protz @wintersteiger : Any advice about Adrian's implementation of kill_process here:
https://github.com/FStarLang/FStar/blob/nik_1687/src/basic/ml/FStar_Util.ml#L269

The process emits some output (quantifier instances) before exiting and Adrian needs to read that output. Killing the process apparently (according to the comments there) closes the channels before allowing to read the final output from it.

Any suggestions for how to implement this robustly? The current implementation just hangs on cygwin/OCaml-4.0.5.

[nikswamy]

Maybe @ad-l has some thoughts about it too?

[msprotz]

Reading output from a process properly on all platforms is totally non-trivial. In Kremlin, I use the Process package from OPAM to do that for me, it's nearly impossible to get it right otherwise. Since it's already installed via the Everest script, it might be good to rely on it here too, assuming that solves the problem? I don't know enough about this particular use-case to know if it's applicable.

[wintersteiger]

Darn, I didn't think that bit would create problems! It's correct that we need to wait for Z3 to output the actual, final quantifier stats (which for global quantifiers happens upon exit). @arpj-rebola is there a way to check whether the stream we're reading from is still alive, or perhaps a version of the async read with a timeout? @msprotz the process package might work for the ML part, but I don't know whether there's an F# equivalent.

[arpj-rebola]

The issue is caused by my implementation closing Z3 rather than killing it, so that I can retrieve the final output that is generated after Z3 exits. It seems that when Z3 is run in Cygwin, closing the input channel into Z3 is a no-op, and then F* just keeps waiting forever.

I have a workaround: closing Z3 by sending (exit) to Z3. I'll be back to you when it works.

[arpj-rebola]

I think it should work now.

[nikswamy]

I wonder what the status of this PR is.

I like the idea of sending an (exit) to the Z3 before killing it.

However, it seems that FStar_Util.ml is a bit broken (it's missing some functions, e.g., kill_process_for_good). Meanwhile NotFStar.Util.fs also looks a bit odd, since it implements kill_process in terms of kill_z3_process and I don't see the same behavior there of sending an (exit) to Z3 before killing it.

Wouldn't all of this be simpler if we just kept the process management stuff unchanged and standard in FStar.Util. And then in FStar.SMTEncoding.Z3.fs, just before killing the Z3 process there, we do an ask_process there sending it the (exit) command?