Ortac/QCheck-STM

Overview

The qcheck-stm plugin for ortac (called Ortac/QCheck-STM in order to avoid ambiguities) generates a standalone executable using QCheck-STM to perform model-based state-machine testing of a module, building up the model from its Gospel specifications.

In order to be able to generate the STM module, the plugin will need five pieces of information:

1. What type do we want to test? This is called system under test or SUT by QCheck-STM.
2. How to generate a value of this type? The init_sut function.
3. What is the model of this type? This is what is taken as the state by QCheck-STM.
4. How to generate the said model? The init_state function.
5. How does the model change when calling a function? The next_state function.

Answering these five questions is done part in a configuration module and part in the Gospel specifications that we will have to write in a specific style.

This tutorial aims at showing how to write Gospel specifications for our modules in order to be able to automatically generate the QCheck-STM tests with the ortac command-line tool and its Ortac/QCheck-STM plugin.

We are going to build an example for a simple fixed-size container library.

How to write Gospel specifications?

In order to use the Ortac/QCheck-STM, the module we want to test must contain three kinds of items:

1. The type declaration for SUT
2. The function used to generate the initial value of SUT
3. Functions to be tested

Here is an example for the declaration of type SUT:

type 'a t
(*@ model size : int
    mutable model contents : 'a list *)

we can see the Gospel specifications under the type declaration, in the special Gospel comments. These specifications give two models to the type, one non mutable and one mutable. These models are necessary (or at least some models) in order to give enough information to the qcheck-stm plugin to build the functional state that QCheck-STM will be using. This item is then bringing two needed pieces of information: what are the type of the SUT and the type of the state.

The second item is the function used for generating the inital value for SUT. Here again, this item will bring two needed pieces of information: how to build the initial value of SUT and the corresponding state. This is the role of the make function along with its specification.

val make : int -> 'a -> 'a t
(*@ t = make i a
    checks i >= 0
    ensures t.size = i
    ensures t.contents = List.init i (fun j -> a) *)

Obviously, the function should return a value of type SUT. But more importantly, the specification has to give a value to each of the models that were given to the type SUT in its specification. Here, this means we need to give a value to t.size and to t.contents. The checks clause is part of the Gospel specification of the function, but it won't be used by the plugin to generate any code. We can give more information that the plugin needs, for example if we are also using another tool based on Gospel specifications. The plugin will simply ignore them.

Now that Ortac/QCheck-STM is able to generate an initial value for the type under test and its model, we can turn our attention to the functions we will want to test. Here is the example of the classic set function along with its Gospel specification written with the qcheck-stm ortac plugin in mind:

val set : 'a t -> int -> 'a -> unit
(*@ set t i a
    checks 0 <= i < t.size
    modifies t.contents
    ensures t.contents = List.mapi (fun j x -> if j = (i : integer) then a else x) (old t.contents) *)

The most important purpose of the specifications (in the context of this tutorial) is to bring the last piece of information. That is to answer the question about how the model changes when calling the specified function. This is done in two steps.

First, we have to declare which of the model's field are modified in the modifies clause. Let's note that if, like in the case of the set function, the function is returning unit, it is a Gospel error to not give any modifies clause. But Gospel lets us write modifies () in order to express the fact that the function is modifying something that is not in the model of any of the argument. However, Ortac/QCheck-STM will read the modifies clauses (if any) in order to determine which model's fields are modified when the function is called. The model's fields that don't appear in any of the modifies clauses will be considered as not modified.

Then, the plugin will look at the ensures clauses (the postconditions) in order to find one clause per modified field that expresses how to compute the modification. For now, the tool is not very smart. The basic rule of thumb is that we need to write down a computable description of the new model's field as a function of the old one. This will often mean that we need to write stronger postconditions that what would be necessary in another context. If the plugin can't find any suitable ensures clause, it will raise a warning and skip the function for test.

We can see again the checks clause. This time, as the function is a candidate for test, the checks clause will be used by the tool to check that if the condition of the clause is not respected, the function raises the Invalid_arg exception.

Now that the set function is ready to be tested, let's turn our attention to another example. Here is the example of the get function along with its Gospel specifications:

val get : 'a t -> int -> 'a
(*@ a = get t i
    checks 0 <= i < t.size
    ensures a = List.nth t.contents i *)

Here, the ensures clause has another use. As the get function does not modifies anything, there is no need to give the values of the model’s fields after the function. Note that the ensures clause wouldn't have been fit for this purpose anyway. The ensures clauses that are not used for the next_state function are used for checking postconditions, here a postcondition stating a relation between the returned value and the function arguments. These ensures clauses are not necessary to generate the QCheck-STM tests, but they will bring strength to our tests.

In order to generate postcondition-checking, Ortac/QCheck-STM uses the ensures clauses that were not used for the next_state function but it also uses the checks clauses and the raises ones.

How to configure the generated tests?

Now we need a configuration file. Configuration files for Ortac/QCheck-STM are OCaml modules containing at least a type declaration for `sut` (usually the type `t` of the module under test with all the type parameters instantiated) and a value declaration for `init_sut` (a call to a function from the module under test returning a value of type `sut`)

open Example

type sut = char t

let init_sut = make 42 'a'

Then, we can generate the QCheck-STM file by running the following command where we indicate the file we want to test and the configuration file. We can write the generated code into a file, using the -o option.

$ ortac qcheck-stm example.mli example_config.ml -o stm_example.ml

The other information we can put in the configuration file are:

• custom QCheck generators in a Gen module
• custom STM printers in a Pp module
• custom STM.ty extensions and its functional constructors in a Ty module

These additional information are mostly necessary when the tested library exposes other types than the one used as SUT.

The Gen module should contain a QCheck.Gen.t for each of these types. It is also possible to shadow already defined generators. One use case for this last possibility is to limit the size of the generated integers.

As explained in the returning-sut section, integers as argument of a function returning a SUT are generated with QCheck.Gen.small_signed_int. When we want to customize the generation of those arguments, we need to overwrite this generator.

The Pp module should contain a Util.Pp.t for each of these types. These values are used to print the runnable scenario if the test fails. We can refer to the module documentation for more details.

The Ty module should contain an STM.ty extension and a corresponding STM.ty_show smart constructor for each of these types. An 'a STM.ty_show is a pair of an 'a ty value and an 'a -> string function.

Dependencies of the generated tests

The generated OCaml file has a bunch of dependencies:

• qcheck-core
• qcheck-core.runner
• qcheck-stm.stm
• qcheck-stm.sequential
• qckeck-multicoretests-util
• ortac-runtime

Using the dune build system, our dune rule for the example above would look like the following:

(test
 (name stm_example)
 (libraries
  qcheck-core
  qcheck-core.runner
  qcheck-stm.stm
  qcheck-stm.sequential
  qcheck-multicoretests-util
  ortac-runtime
  example)
 (action
  (run %{test} --verbose)))

Warning system

Now that we know what Gospel specifications for the qcheck-stm plugin should look like and how to generate the QCheck-STM file, let's focus on what can go wrong. The qcheck-stm plugin has an extensive set of warnings to help us formulate our specifications in a way it can use.

Most of the time, Ortac/QCheck-STM will skip a function if it can't generate one of the elements needed by QCheck-STM. Doing so, it will display a warning on stderr in order for us to be able to get an idea about test coverage.

Ortac/QCheck-STM specifics

Let's start with the warnings specific to the plugin.

The principle at the core of Ortac/QCheck-STM is to turn the Gospel specifications into OCaml code needed by the QCheck-STM test framework. This means that we need to provide these pieces of information into the specification in a style that allows the plugin to understand them.

The most delicate piece of information we have to give is how the function modifies the model of the SUT. As stated above, the plugin is looking for this information in the ensures clauses.

If Ortac/QCheck-STM doesn't have enough information in the specifications in order to compute the next value for every model's field appearing in a modifies clause, it won't be able to test the function and inform us with a warning.

For example, the following specifications are not enough for Ortac/QCheck-STM.

val ensures_not_found_for_next_state : 'a t -> unit
(*@ ensures_not_found_for_next_state t
    modifies t.contents
    ensures List.length t.contents = List.length (old t.contents) *)

Ortac/QCheck-STM will look at the modifies clause and then look for an ensures clause for each of the modified models that allows to compute its new value. Here, it won't find any and warn us with the following message:

$ ortac qcheck-stm example_next_state.mli example_config.ml -o foo.ml
File "example_next_state.mli", line 15, characters 13-23:
15 |     modifies t.contents
                  ^^^^^^^^^^
Warning: Skipping ensures_not_found_for_next_state: model contents is
         declared as modified by the function but no suitable ensures clause
         was found. Specifications should contain at least one "ensures
         x.contents = expr" where x is the SUT and expr can refer to the SUT
         only under an old operator and can't refer to the returned value.

That doesn't mean that we have to rewrite the clause. Maybe it contains information we still want to state in the specifications. You can then add another ensures clause with the relevant information in order to compute the new value of the modified model. The warning message gives us the form in which the plugin expects to find the information, namely a description of the new state by an expression in which any reference to the state should be to the old state (that is the state before the function is called).

Note also that if we write modifies t, the plugin assumes that all the mutable fields are modified and will try to find a description for all of them. So we'll need to avoid being too general in the modifies clauses.

In Gospel, we have the possibility to use ghost values, as arguments and/or as returned values. As those values don’t exist in the actual code that will be called during the test, Ortac/QCheck-STM doesn't support Gospel specifications with ghost values in the header.

If we add the following declaration to our example file,

val ghost_arg : char -> 'a t -> bool
(*@ b = ghost_arg [ i : integer] c t *)

the command will generate the following warning:

$ ortac qcheck-stm example_ghost.mli example_config.ml -o foo.ml
File "example_ghost.mli", line 18, characters 20-21:
18 | (*@ b = ghost_arg [ i : integer] c t *)
                         ^
Warning: Skipping ghost_arg: functions with a ghost argument are not
         supported.

You'll need to write the specifications without using ghost arguments or returned value if we want to test this function with Ortac/QCheck-STM.

Finally, when we want to test a library with a parameterized type, we need to instantiate the type parameter in order to generate the QCheck-STM tests. Choosing the right instantiation implies to be careful when the library contains specialized functions.

For example, if we add the following declaration to our example file,

val incompatible_type : char -> string t -> bool
(*@ b = incompatible_type c t *)

the plugin will generate a warning for this function and skip it.

$ ortac qcheck-stm example_incompatible_type.mli example_config.ml -o foo.ml
File "example_incompatible_type.mli", line 17, characters 32-40:
17 | val incompatible_type : char -> string t -> bool
                                     ^^^^^^^^
Warning: Skipping incompatible_type: the type of its SUT-type argument is
         incompatible with the configured SUT type: char t.

In the case we have functions specialized with different instantiations, we can always generate one test per possible instantiation, of course.

ortac limitations

The second source of limitations is the ocaml_of_gospel translation provided by the ortac-core package. Gospel being a logical language, it is not fully executable. ortac-core identifies an executable subset of Gospel and translates it to OCaml. But there are still some limitations, in particular concerning quantification. For now, only well-bounded quantifications over integers are supported.

If we add the following declaration to our example file,

val unsupported_quantification : 'a t -> bool
(*@ b = unsupported_quantification t
    ensures b = forall a. List.mem a t.contents -> a = a *)

the command will generate the following warning:

$ ortac qcheck-stm example_ill_formed_quantification.mli example_config.ml -o foo.ml
File "example_ill_formed_quantification.mli", line 13, characters 0-142:
13 | val unsupported_quantification : 'a t -> bool
14 | (*@ b = unsupported_quantification t
15 |     ensures b = forall a. List.mem a t.contents -> a = a *)
Warning: Incomplete computation of the returned value in the specification of unsupported_quantification. Failure message won't be able to display the expected returned value.
File "example_ill_formed_quantification.mli", line 15, characters 16-56:
15 |     ensures b = forall a. List.mem a t.contents -> a = a *)
                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Warning: Skipping clause: unsupported quantification.

Note that only the clause involving the unsupported quantification has not been translated. If the function's specification contains other clauses that can be translated and contain enough information for the plugin to do its job, then we will be able to test the function. If not, maybe we can rewrite the clause without involving this sort of quantification. In this particular example, we can use the List.for_all combinator from the Gospel standard library List module:

val for_all : 'a t -> bool
(*@ b = for_all t
    ensures b = List.for_all (fun x -> x = x) t.contents *)

Other limitations

Finally, note that this tool is still fairly new and comes with limitations that should be lifted in the future. Fow now, we only support tuples with less than 10 elements and we only support first-order functions.

If we add the following declarations to our example file,

val of_list : 'a list -> 'a t
(*@ t = of_list xs *)

val g : 'a t -> 'a * 'a * 'a * 'a * 'a * 'a * 'a * 'a * 'a * 'a -> bool
(*@ b = g t x *)

val for_all : ('a -> bool) -> 'a t -> bool
(*@ b = for_all p t *)

Ortac/QCheck-STM will generate the following warnings:

$ ortac qcheck-stm example_limitations.mli example_config.ml -o foo.ml
File "example_limitations.mli", line 18, characters 3-19:
18 | (*@ t = of_list xs *)
        ^^^^^^^^^^^^^^^^
Warning: Skipping of_list: the specification of the function does not specify
         all fields of the model for the returned SUT value. Specifications
         should contain at least one "ensures x.size = expr" and
         "ensures x.contents = expr" where x is the returned SUT and expr can
         refer to other SUTs only under an old operator.
File "example_limitations.mli", line 20, characters 16-63:
20 | val g : 'a t -> 'a * 'a * 'a * 'a * 'a * 'a * 'a * 'a * 'a * 'a -> bool
                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Warning: Skipping g: Can only test tuples with arity < 10.
File "example_limitations.mli", line 23, characters 15-25:
23 | val for_all : ('a -> bool) -> 'a t -> bool
                    ^^^^^^^^^^
Warning: Skipping for_all: functions are not supported yet as arguments.

Functions returning a SUT

Functions returning a SUT will be tested, however, there are some restrictions and peculiarities:

• Only functions returning a single SUT value are tested, if the SUT is nested inside another structure (e.g., a tuple or a list) the function will be skipped
• Many init/create like functions take an integer relating to the initial size of the datastructure as an argument. In order to keep the size of the created data structure manageable, a heuristic is used. Whenever a functions returns a SUT, but does not take a SUT as an input argument, any Gen.int generators in Spec.arb_cmd are automatically exchanged with Gen.small_signed_int

Segmentation faults and non-termination

In the standard configuration, the code generated by the qcheck-stm plugin will run a number of tests in sequence in the same process. If one of those test runs crashes (e.g. by incorrectly using Obj.magic), this automatically also kills the overall process, therefore no trace can be shown to the user of which series of commands lead to the crashing scenario. Similarily, if one of the functions under test does not return, the overall test suite is stalled indefinitely.

It is possible to instruct the underlying runtime to instead run all tests in separate processes with a given timeout, so that in case of a segmentation fault the runtime can still recover a trace leading to said crash, and non-terminating computations are automatically stopped after the given timeout has passed.

This is done by setting the environment variable ORTAC_QCHECK_STM_TIMEOUT to a timeout value in seconds, after which the runtime will automatically kill the process running the test.

For example when using dune to run the test, this can be achieved in the following way:

(test
 (name stm_example)
 (libraries
  qcheck-core
  qcheck-core.runner
  qcheck-stm.stm
  qcheck-stm.sequential
  qcheck-multicoretests-util
  ortac-runtime
  example)
 (action
  (setenv
   ORTAC_QCHECK_STM_TIMEOUT
   10
    (run %{test} --verbose)))

This would automatically end each test after 10 seconds.

Instead of setting the timeout permanently in the dune file, one can also set the environment variable when running tests from the command-line:

$ ORTAC_QCHECK_STM_TIMEOUT=10 dune runtest