A test/benchmark in the source repository?

[gasche]

I looked at the Qed implementation out of curiosity. There are a couple places where I wondered if writing things slightly differently could make a difference for performance. (Performance of the simplification, without changing its behavior.) But it's very hard to tell without measuring the performance on a realistic use-case, and I couldn't find any example use-case in https://git.frama-c.com/pub/frama-c/-/tree/master/src/plugins/qed.

The code is very self-contained and fairly easy to understand, but it looks like testing it currently requires running the full Frama-C platform, and possibly inventing my own examples to get tests/benchmarks.

Would it be possible to distribute a small set of representative (complex) terms to be used as input for Qed? (I guess they could either be distributed as large OCaml values, or in text format with a parser.) This could be used to test the correctness of a small change to Qed, the performance impact of changes, and possibly improvements to the simplifications as well.

[bobot]

It should be possible to produce a sequence of API call from a run of Frama-C, but the functorization doesn't make that straight forward. I wonder if it should be done by hand or if it already exists tools for that.

CC @correnson

[correnson]

Indeed, it is possible write a Frama-C plugin for doing that. Here is my suggestion:

1. Use the Wp.VC api to obtain a collection of proof obligations of type Wp.VC.t
2. Use the Wp.VC.get_sequent or Wp.VC.get_formula to obtain the associated Qed formulae
3. Use the Wp.Repr api to de-structure the internal representation of Qed formulae

The disadvantage of this approach is that you will only obtained already normalized Qed formulae, not all the calls to the API.

Be aware that Qed formula can have a huge amount of sharing, which requires some care when dumping them recursively on disk for instance. Use memoization as most as you can by using Qed.Tmap maps or Qed API for computing the set of shared sub-terms like Qed pretty printer does.

[correnson]

Alternatively, you can instrument the Qed calls from WP by hacking in the Lang.F module itself.
Actually, the Lang.F already builds « smart » constructors for predicates by means of term constructors.
You can use the same trick to instrument the « normal » smart constructors of Qed and store their result somewhere. Typically:

module Lang.F =
struct
  type term = Q.term
  type pred = Q.term
…
  let e_and (a : term) (b : term) : term = (* do something with a and b *) Q.e_and a b
  let p_and (a : pred) (b : pred) : pred = e_and a b
…
end

The advantage of this approach is that you can choose to only instrument some of the constructors.

[correnson]

Of course, the approaches described above would combine very well with each others!

[correnson]

You can also pretty-print a Qed formula in barely any language by instantiating the Qed.Engine class appropriately.
For instance, you could pretty-print a Qed formula into OCaml source calls to the Qed API!