Allow for user-defined entity creation in test generation

[Dargones]

Fixes #4543

This PR lets users specify how to generate a given argument for the test entry method using a :testGenerators attribute. Here is the description of the attribute I propose to put in the Reference Manual:

This attribute instructs Dafny test generation to override an input parameter with a value obtained by calling the specified generator function or method. A method annotated with {:testGenerators} must always be a test entry method.

For example, consider the following Dafny code:

module M {
  method {:extern} CoinFlip() returns (b:bool)
  method {:testEntry} {:testGenerators "b", "M.CoinFlip"} ToTest(b: bool) {
    // Do Something Here
  }
}

In the code snippet above, method ToTest is annotated with {:testGenerators "b", "M.CoinFlip"} which means that Dafny test generation will produce a test that calls theM.CoinFlip method to obtain a value for the input parameter b. In particular, running dafny generate-tests Block FILE.dfy on the file above, will produce the following:

method {:test} Test0() {
  var bool0 : bool := M.flipCoin();
  M.m(bool0);
}

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[keyboardDrummer]

Why wouldn't you just write

method {:test} Test0() {
  var bool0 : bool := M.flipCoin();
  M.m(bool0);
}

Instead of

{:testGenerators "b", "M.CoinFlip"}

?

[Dargones]

I think the motivation behind the corresponding issue has a lot to do with how these tests end up being compiled and run. The goal is to not modify the code under test and at the same time to preserve M.m as an entry point for the tests (in particular so that it can be easily substituted with a similarly named method in the implementation to which Dafny is being compared). An annotation tells test generation what to do without affecting verification or runtime behavior of the method itself. @codyroux, does this sound correct? Do leave a comment if you have had a chance to test this out!

[keyboardDrummer]

The goal is to not modify the code under test

A wrapper test method such as

method {:test} Test0() {
  var bool0 : bool := M.flipCoin();
  M.m(bool0);
}

does not modify the code under test

and at the same time to preserve M.m as an entry point for the tests (in particular so that it can be easily substituted with a similarly named method in the implementation to which Dafny is being compared).

Why do want M.m to be the entry point? Even if it is not, could you not still substitute it with a similarly named method in the implementation to which Dafny is being compared?

[robin-aws]

If I'm following correctly, the motivation is clearer once you have more than one input parameter and want to allow test generation to control what other arguments are passed in. Runnin dafny generate-tests Block FILE.dfy on this:

module M {
  method {:extern} CoinFlip() returns (b:bool)
  method {:testEntry} {:testGenerators "b", "M.CoinFlip"} ToTest(b: bool, c: bool) {
    // Do Something Here
  }
}

Would produce something like:

method {:test} Test0() {
  var bool0 : bool := M.flipCoin();
  M.m(bool0, true);
}

method {:test} Test1() {
  var bool0 : bool := M.flipCoin();
  M.m(bool0, false);
}

In other words, {:testGenerators} is useful for controlling how tests are generated, so you don't have to do a ton of post-processing on the generated tests to make them runnable/practical.

[keyboardDrummer]

If I'm following correctly, the motivation is clearer once you have more than one input parameter and want to allow test generation to control what other arguments are passed in.

Why not write the following, for your example?

module M {
  method {:extern} CoinFlip() returns (b:bool)

  method {:testEntry} ToTestWrapper(c: bool) {
    var bool0 : bool := M.flipCoin();
    ToTest(bool0, c);
  }

  method ToTest(b: bool, c: bool) {
    // Do Something Here
  }
}

[robin-aws]

If I'm following correctly, the motivation is clearer once you have more than one input parameter and want to allow test generation to control what other arguments are passed in.

Why not write the following, for your example?

module M {
  method {:extern} CoinFlip() returns (b:bool)

  method {:testEntry} ToTestWrapper(c: bool) {
    var bool0 : bool := M.flipCoin();
    ToTest(bool0, c);
  }

  method ToTest(b: bool, c: bool) {
    // Do Something Here
  }
}

Fair point, it seems like the extra wrapper shouldn't change the coverage of the generated tests - @Dargones or @codyroux?

[Dargones]

Using a wrapper method in this way makes sense to me when the goal is to test the Dafny code directly.

That said, I do see a potential issue when the goal is to perform model-based testing, i.e. when we want to generate tests from the Dafny model to run on another implementation written in a different language. Ideally, we would want to (1) generate the tests, (2) switch the call to the method from which we generated the tests to the method that will be tested at runtime, and (3) run the tests. The use of a wrapper method complicates things in this scenario because now the switch has to happen within the wrapper method itself meaning that the user has to constantly modify the wrapper method between generating tests and running them.

I do like the wrapper solution more because it does not require any new features but I am wondering to what extent it is feasible in practice in the model-based testing scenario. @codyroux, do you have a take on this?

[Dargones]

Closing in favor of #5226