[SwayamInSync]

The only view of a solver query was --dump-ir=4: Z3 terms without declarations, options, or a check, which no solver reads. A solver bug, a version differential (D1), or a query that takes too long could not be handed to anyone without cpp-verify and the source. This is plan item D7, stacked on #107 (D6).

--dump-smt2=DIR writes every query cpp-verify sends to Z3 or cvc5 as a script that z3 FILE or cvc5 FILE runs on its own.

What a file is

On the clamp.cpp of chapter 17:

$ cpp-verify --dump-smt2=queries clamp.cpp
$ find queries -type f | sort
queries/clamp-14e9c9/missing-return-7-3.z3-c326aaab.smt2
queries/clamp-14e9c9/overflow-8-5.z3-19b38e3e.smt2
queries/clamp-14e9c9/postcondition-5-23.z3-d86b7e26.smt2
queries/clamp-14e9c9/whole.z3-3a4644f7.smt2

; cpp-verify 0.2.0-dev, z3 4.13.4
; clamp: the postcondition check at clamp.cpp:5:23 (fn_5f5a35636c616d7069::postcondition@5:23)
; replay: z3 clamp-14e9c9/postcondition-5-23.z3-d86b7e26.smt2
(set-option :timeout 30000)
(set-option :rlimit 6000000)
(set-option :smt.mbqi true)
(set-option :smt.qi.eager_threshold 0.0)
(declare-fun __result_1 () Int)
(declare-fun x_0 () Int)
...
(check-sat)
(get-model)
; cpp-verify: sat

z3 clamp-14e9c9/postcondition-5-23.z3-d86b7e26.smt2 prints sat and the model x_0 = -2, __result_1 = -1.

Design, from the references

• Boogie and Dafny (/proverLog, --solver-log):
  • write a session transcript per procedure, named by @PROC@ and, with @TIME@, by time;
  • put the options in the file;
  • record the verdict as a comment (; Invalid).
• Verus (--log smt):
  • logs exactly what was piped, one file per module, with no time or global counter in the names;
  • its options are set-option lines, but the solver's command-line flags are not, so z3 FILE does not reproduce every query.
• Frama-C's WP (-wp-out):
  • writes one file per goal and prover, <propid>_<prover>.smt2;
  • leaves the time and step limits on the prover's command line;
  • keys its cache by the file's digest.

This PR takes from each:

• One file per check. Every Z3 check goes through Z3Encoder::check, and every cvc5 run through runCVC5. A file is a query, not a session.
• Standalone. The options cpp-verify sets on Z3's API, or on cvc5's command line, are set-option commands in the file, which Verus and Frama-C leave out:
  • for Z3, the check's timeout, the resource limit, and the quantifier settings. A quantified query, whose solver is the smt tactic, ends with (check-sat-using smt);
  • for cvc5, its flags (cvc5Options now builds both the command line and the commands).
• Deterministic names. The name is <function>-<h6>/<query>.<solver>-<h8>.smt2:
  • <h6> hashes the function's identity, so overloads stay apart;
  • <query> is whole or the obligation's stable id as kind-line-col;
  • <h8> hashes the script, so two checks of one obligation (refinement rounds) are two files and a repeated check is one.
  • Names depend only on the query, never on time or --jobs.
• The verdict at the end (Dafny): ; cpp-verify: sat, unsat, unknown (timeout), or for cvc5 no answer (...). The script is written before the check, so a check that hangs or crashes leaves its query; the verdict is appended after it. A sat check also gets (get-model).

Two printer problems the replays found

Z3's benchmark printer (to_smt2) leaves symbols unquoted. Our quantifier ids q@24:11 are not SMT-LIB symbols (the colon starts a keyword), so 1,373 of the first 7,239 dumped scripts did not parse. The dump uses the solver's own printer, Z3_solver_to_string, which quotes them (|q@24:11|). It also prints recursive definitions (define-funs-rec).

That printer also writes the model converter that preprocessing left on a solver that has checked before: model-add of symbols such as k!0 that it never declares. 829 scripts did not parse because of it. The dump now prints a solver that holds only the checked solver's assertions.

Replaying every query of the suite

Every file of clang/test/Verify/suite was run with --jobs=4 --timeout=5000 --dump-smt2, on Z3 and on cvc5, and every script was replayed with replay_smt2.py. That helper runs Z3 4.13.4's own shell, or cvc5 1.1.2. It compares each answer with the one cpp-verify recorded where that was sat or unsat, and only parses the others.

• cvc5: 17,945 scripts, 17,565 with a recorded sat or unsat. One replay differs: unknown where cpp-verify got sat.
• Z3, before the second fix: 17,271 scripts, 921 differing:
  • 829 parse errors from the model converter;
  • 92 others.
• Z3, after it: the 37 files with a difference were run again: 7,899 scripts, 52 differing. All 52 replay to unknown; none contradicts the answer cpp-verify got:
  • 28 are checks cpp-verify gave 1 to 4 ms, the time left of a query's budget;
  • 24 had 124 to 5000 ms, 16 of them quantified queries solved by the smt tactic.

The last group is a property of Z3, not of the files. Z3's search on a quantified query depends on the order in which its terms were created, and a replay creates them in another order.

The vacuity query of constructors.cpp's Copy4 is sat in cpp-verify. Its assertions, re-added to a fresh smt-tactic solver in the same Z3 context, are also sat, and so is the dumped text parsed back into that context. In a fresh context (Z3's API in another program, or the z3 shell) they are unknown (incomplete quantifiers). The documentation says so: replaying gives the answer cpp-verify got for most queries, and a quantified one can end differently.

The dumps already paid off while writing #106 and the H5 case study:

• the exact cvc5 query behind cvc5_memory_limit.cpp showed that cvc5 1.4.2 solves it in less than 5 MB;
• a class-invariant query that timed out turned out to be one the default solver answers sat in 24 ms, but that the smt tactic, chosen for its loop frame's quantifier, gives up on after 20 s.

Testing

The vendored Z3 now builds its shell too (Z3_BUILD_EXECUTABLE=ON, installed into the build's cppverify-z3/install/bin, not into release archives). lit has a z3-shell feature and %cppverify-z3; a system Z3 build uses z3 on PATH.

suite/smt2_dumps.test (new) checks:

• the files of a run:
  • each obligation's file;
  • a query checked again with definition instances, which is two files;
  • the vacuity, contract, and termination checks;
  • two overloads in two directories;
• the content of a failure's file: header, options, check, (get-model), verdict;
• (check-sat-using smt) for a quantified query;
• that a second run writes the same files;
• that every Z3 script replays in Z3's shell with the answer cpp-verify got, and every cvc5 script in cvc5 (when installed);
• that a query checked again on its solver has no model-add;
• that archive replay writes its queries;
• that an unwritable directory is a warning and leaves the verdicts as they are.

It passes five runs out of five. On the base it fails at its first line (--dump-smt2 is unknown).

Each mutant below, applied alone and rebuilt, is caught by smt2_dumps.test, or for Q13 by failure_notes_cvc5.test (17 of 17):

Mutant	Change
Q1	Z3 checks are not written
Q2	no answer after a Z3 check
Q3	no (get-model) after sat
Q4	no Z3 options
Q5	Z3's benchmark printer
Q6	a quantified query ends with a plain (check-sat)
Q7	the module is not recorded (no names)
Q8	every check of a query is one file
Q9	obligations are not named
Q10	overloads share a directory
Q11	cvc5 runs are not written
Q12	cvc5 options are not commands
Q13	cvc5 flags without a value are dropped
Q14	a write error is silent
Q15	the header names no obligation
Q16	the option is ignored
Q17	the checked solver is printed with its model converter

On a release build of the top of this stack (#111, which contains this branch), the whole Verify suite of 503 tests passes but one, docs_examples.test, whose failure was a docs example on #111's new page, fixed there.

Docs: tooling (the option, the layout, a file, a replay, and what replaying may give), chapter 15's flag list, chapter 16 (how to report a solver problem), release notes, README, ARCHITECTURE, and DESIGN.

Stacked on #107.