Type Parameters in Automatically Generated Tests

[Dargones]

Fixes #2222 and #2221 by adding support for type parameters to counterexample extraction and test generation.

Test generator will replace all type variables with int. This should be a valid solution, I think, because all permitted type parameter characteristics apply toint (i.e. it is equality-supporting, auto-initializable, nonempty, and non-heap based)

Regarding the example in the linked issues, the tool will now generate the following:



include "tmp.dfy"
module tmpUnitTests {
  import Test
  method test0() returns (r0:bool)  {
    r0 := Test.IsEvenLength<int,int>(map[0 := 1, 2 := 3, 4 := 5]);
  }
  method test1() returns (r0:bool)  {
    r0 := Test.IsEvenLength<int,int>(map[]);
  }
}

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

[Dargones]

@tbean79, does this seem to address the issue?

[tbean79]

@Dargones Indeed, this PR solves both issues, I was able to run generated tests in both Block and Path mode.

[MikaelMayer]

Great job solving two problems at once !
At least update the release notes, but otherwise, I have a few clarifying questions to understand your solution.

[MikaelMayer]

Can you please explain me why datatypes are not supported? What was happening before?

[Dargones]

I have code that supports algebraic datatypes on my fork and can make another PR to add them but for know I just wanted to make it easier for a potential user to figure out why test generation might not work for them. Let me know if I should remove this case from this PR / make another PR specifically for datatypes.

[Dargones]

To answer your second question, datatypes were never supported (as per this README) and would potentially lead to unspecified behavior. Now the behavior is specified even though the support is not there yet.

[MikaelMayer]

Ok thanks, It's ok to keep this case in this PR I think. I'm happy to have a look at your other PR about datatypes.

[Dargones]

Thank you, @MikaelMayer! Let me know if there is anything else. I could also bundle support for datatypes with this PR or make a separate PR about them.

[MikaelMayer]

Great work, thanks!