Collecting .smt2 files from F*'s regression suite

A basic run

This make invocation shown below will cause F* to verify a bunch of files, emitting a separate .smt2 file for each verification condition it produces.

I usually first remove all .smt2 files from the FStar working tree and then start the regression run.

make -C src utest -j 6 OTHERFLAGS='--hint_info --log_queries' HINTS_ENABLED= # regenerate all of them 

• The --hint_info option causes F* to create a separate .smt2 file for each problem.
• The --log_queries causes it to actually write out the .smt2 files to disk.
• The -j 6 says to use 6 cores; tune it to the number of cores you actually want to use.
• The HINTS_ENABLED= flag disables hints (CH: we need a better way to do this even after someone has already passed -use-hints)

The generated files are named like

./ulib/queries-FStar.Int32-55.smt2
./ulib/queries-FStar.Int32-56.smt2
./ulib/queries-FStar.Int32-57.smt2
./ulib/queries-FStar.Int32-58.smt2
./ulib/queries-FStar.Int32-59.smt2
./ulib/queries-FStar.Int32-6.smt2
./ulib/queries-FStar.Int32-60.smt2
./ulib/queries-FStar.Int32-61.smt2
./ulib/queries-FStar.Int32-62.smt2
./ulib/queries-FStar.Int32-63.smt2
./ulib/queries-FStar.Int32-64.smt2
./ulib/queries-FStar.Int32-65.smt2
./ulib/queries-FStar.Int32-66.smt2
./ulib/queries-FStar.Int32-67.smt2
...

i.e., they have the form queries-<moduleName>-<queryNumber>.smt2

Logging hint behavior

The --hint_info option when additionally passed in OTHERFLAGS above, causes F* to write on stdout some information about each query, hint replay etc.

For example, you will see output of the form:

(.\FStar.Integers.fst(275,50-275,53)@queries-FStar.Integers-98.smt2)
        Query (FStar.Integers.f_uint_8, 5)      succeeded (with hint) in 74 milliseconds with fuel 1 and ifuel 1

This mentions the F* source file and position that produced the query; the .smt2 file that corresponds to it; the query identifier (FStar.Integers.f_uint_8, 5, in this case), and info about whether it succeeded while using a hint or not, the time it took and the fuel parameters that were used.

Here is a snippet of queries that failed hint replay.

$ grep -B 1 "failed (with hint)" dump | head -10
(.\FStar.BitVector.fst(74,0-74,34)@queries-FStar.BitVector-42.smt2)
        Query (FStar.BitVector.lemma_xor_bounded, 5)    failed (with hint) in 44 milliseconds with fuel 2 and ifuel 1
--
(.\FStar.SquashProperties.fst(48,0-53,94)@queries-FStar.SquashProperties-4.smt2)
        Query (FStar.SquashProperties.excluded_middle_squash, 1)        failed (with hint) in 37 milliseconds with fuel 2 and ifuel 1
--
(.\FStar.HyperHeap.fst(211,0-211,25)@queries-FStar.HyperHeap-84.smt2)
        Query (FStar.HyperHeap.lemma_modset, 4) failed (with hint) in 54 milliseconds with fuel 2 and ifuel 1
--
(.\FStar.HyperHeap.fst(217,0-217,44)@queries-FStar.HyperHeap-88.smt2)

Correlating hint failures with their subsequent no-hint versions

Each query that fails with a hint is immediately reattempted by F* without a hint.

So, if you see, e.g.,

(.\FStar.HyperHeap.fst(211,0-211,25)@queries-FStar.HyperHeap-84.smt2)
        Query (FStar.HyperHeap.lemma_modset, 4) failed (with hint) in 54 milliseconds with fuel 2 and ifuel 1

Then queries-FStar.HyperHeap-85.smt2 contains the same query re-attempted without a hint. For example:

$ grep -A 3 'FStar.HyperHeap-84.smt2' dump
(.\FStar.HyperHeap.fst(211,0-211,25)@queries-FStar.HyperHeap-84.smt2)
        Query (FStar.HyperHeap.lemma_modset, 4) failed (with hint) in 54 milliseconds with fuel 2 and ifuel 1
(.\FStar.HyperHeap.fst(211,0-211,25)@queries-FStar.HyperHeap-85.smt2)
        Query (FStar.HyperHeap.lemma_modset, 4) succeeded in 547 milliseconds with fuel 2 and ifuel 1

It would be nice to have a more systematic way of correlating hints and no-hints versions of the same queries. Although, it should be possible to write some simple scripts to do this correlation based on the above information.