Hybrid Test Generation

[Dargones]

Description

This PR provides a way to combine symbolic test generation with QuickCheck-style input enumeration approach. The idea is to let the user specify generator methods via the {:testGenerators} attribute which Dafny should then use to construct values that are not constrained by the solver. For example, in the code snippet above, the value of the e1 argument in the ToTest method does not affect the path that execution takes at runtime, whereas the value of e0 does. Therefore, Dafny will rely on the counterexample model to reconstruct the value of e0 but it will rely on the user-provided generator method to construct e1.

module M {
    datatype D = D1 | D2
    datatype E = E(d:D)
    method {:extern} DGenerator() returns (d:D)
    method {:testEntry} {:testGenerators "M.DGenerator"} ToTest(e0:E, e1:E) {
        if (e0.d.D1?) {
            print "D1";
        } else {
            print "D2";
        }
    }
}

Running dafny generate-tests Block FILE.dfy on the file above,
produces the following tests:

import M
method {:test} Test0() {
  var d0 : M.D := M.D.D2;
  var e0 : M.E := M.E.E(d:=d0);
  var d1 : M.D := M.GenerateValue();
  var e1 : M.E := M.E.E(d:=d1);
  M.ToTest(e0, e1);
}
method {:test} Test1() {
  var d0 : M.D := M.D.D1;
  var e0 : M.E := M.E.E(d:=d0);
  var d1 : M.D := M.GenerateValue();
  var e1 : M.E := M.E.E(d:=d1);
  M.ToTest(e0, e1);
}

How has this been tested?

I added several tests to DafnyTestGeneration.Test.WarningTests to check wellformedness of the attribute and to alert the user if Dafny cannot locate the specified generator methods; there is also a test in DafnyTestGeneration.Test.Various for the functionality that the attribute provides.

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

[robin-aws]

Just offering feedback on the feature UX for now.

Judging by the example in the description, we will end up with highly non-deterministic and ordering-sensitive test methods: if the testing framework happened to run test1 before test0, the behavior of each will be completely different.

Ideally we would have test generation actually evaluate the generator and produce separate test methods for each value, but that's obviously a huge amount of work since we don't even have enough static evaluation support for even a purely functional definition of a generator, much less a method.

Instead I'd suggest we emit one test method that iterates over the generates values in an outer loop. It's not the ideal UX but it's at least well-formed.

[Dargones]

@robin-aws, are you thinking of something like this?

import M
method {:test} RunAllTests() {
  Test0();
  Test1();
}
method Test0() {
  var d0 : M.D := M.D.D2;
  var e0 : M.E := M.E.E(d:=d0);
  var d1 : M.D := M.GenerateValue();
  var e1 : M.E := M.E.E(d:=d1);
  M.ToTest(e0, e1);
}
method Test1() {
  var d0 : M.D := M.D.D1;
  var e0 : M.E := M.E.E(d:=d0);
  var d1 : M.D := M.GenerateValue();
  var e1 : M.E := M.E.E(d:=d1);
  M.ToTest(e0, e1);
}