fix: mocking objects in Dafny tests

[Dargones]

This PR makes a few modifications to the way the {:test}-annotated methods are compiled to C#, which should make it possible to use this attribute with tests generated by Dafny's Test Generation module as previously suggested by Robin here (#1385 (comment)). If these modifications seem adequate, I am planning to make {:test} compilable to Java as well. The changes are:

• If the tested method takes parameters, mock them using C#'s FormatterServices.GetUninitializedObject method. This is useful in situations in which you know the state of the object you would like to test and can set its fields accordingly but don't know what constructor to use to allocate the object without running into a runtime exception. In other target languages, the mocking could be done by exploiting the zero constructor.

• Allow tested methods to return non failure-compatible values. Only call IsFailure on the first returned value if it is failure-compatible. This is useful as it allows using methods annotated with {:test} for other purposes, e.g. for printing the returned values.

• Not sure if this is important but the previous version of the code would only call IsFailure on the first returned value of a method if there were more than one returned value. Is there any reason for requiring two or more returned values? I removed this condition and the tests pass but do let me know if it should still be there.

Thank you!

[MikaelMayer]

Thanks for submitting this. I saw that you wrote a test file, could you also please write the "expected output" of this test file and have the test verify that the output is correct?

[Dargones]

Thank you, Mikael! The Dafny tests that I have added are expected to pass so the output of the corresponding lit test should stay the same (it only reports the failed tests) - hence no modifications to the .expect file on my part.

On another note, I can't seem to make the "Semantic Pull Request" check pass although I believe both the PR and at least on of the commits should be "semantic" - would be grateful for any hints about what I should change to make this work!

[MikaelMayer]

We don't know what went wrong with semantic PR. It looks like there is no way to decipher their error message.

[robin-aws]

This PR makes a few modifications to the way the {:test}-annotated methods are compiled to C#, which should make it possible to use this attribute with tests generated by Dafny's Test Generation module as previously suggested by Robin here (#1385 (comment)). If these modifications seem adequate, I am planning to make {:test} compilable to Java as well. The changes are:

• If the tested method takes parameters, mock them using C#'s FormatterServices.GetUninitializedObject method. This is useful in situations in which you know the state of the object you would like to test and can set its fields accordingly but don't know what constructor to use to allocate the object without running into a runtime exception. In other target languages, the mocking could be done by exploiting the zero constructor.

I'm definitely wary about this. It introduces unsoundness into Dafny programs in potentially very subtle ways, given that the compilers are not built with the requirement that this approach has to work.

FYI I experimented a little myself with whether we could just declare a variable v: Value without initializing it instead, that is, to use the semantics of assigning it a non-deterministic value. This doesn't work even if you use /definiteAssignment:0, though, because if Dafny doesn't "see" the constructor call for an object it doesn't know how to reason about framing for modification: there's no way to define a modifies on a method correctly that has an object value that was never constructed.

I can appreciate that it's difficult to figure out what constructor to use in generated tests, but I wouldn't want to encourage this pattern in any other manually-crafted tests. Also, if it's impossible to construct an object with the values you need for a generated test case to hit a certain code branch, for example, that's a deeper issue in the code we should communicate to the user anyway! :)

• Allow tested methods to return non failure-compatible values. Only call IsFailure on the first returned value if it is failure-compatible. This is useful as it allows using methods annotated with {:test} for other purposes, e.g. for printing the returned values.

Is there any need for returning a value from {:test} methods, though, if they don't represent the result of the test? Or are you thinking of calling {:test} methods directly from other code as well?

• Not sure if this is important but the previous version of the code would only call IsFailure on the first returned value of a method if there were more than one returned value. Is there any reason for requiring two or more returned values? I removed this condition and the tests pass but do let me know if it should still be there.

That's just a flat out off-by-one error, and thanks for fixing it. Looks like I got unlucky and didn't have any {:test} methods (rather than functions) with return values.

Thank you!

Right back at you! I'm definitely hoping to find a solution to my worry above, especially since I would love to unblock you from getting {:test} to work with Java as well.

[robin-aws]

See top-level reply comment

[robin-aws]

Just for the record, I'm fine with losing this TODO even through this PR doesn't address it (as it really should be the resolver's job instead of each compiler, and should result in an error rather than just not generating the needed shim code), because it's already tracked in #451 instead

[keyboardDrummer]

Instead of changing how the compiler handles {:test}, could you not place the call to FormatterServices.GetUninitializedObject in an external method? I think this would alleviate @robin-aws's soundness concerns.

Bundle a 'testing runtime' together with the generated tests that allows you to create the parameter values you need to execute the tests, then make the generated tests have 0 arguments.

Instead of

include "object.dfy"
module objectUnitTests {
  import M
  method test0(v0:M.Value) returns (r0:int)  modifies v0 {
    v0.v := -39;
    r0 := M.compareToZero(v0);
  }
}

Have

include "object.dfy"
include "testRuntime.dfy"

module objectUnitTests {
  import M
  method test0() returns (r0:int) {
    var v0:M.Value = TestRuntime.CreateUnitialized<M.Value>();
    v0.v := -39;
    r0 := M.compareToZero(v0);
  }
}

[Dargones]

Thank you for the input on this, @robin-aws and @keyboardDrummer ! I will experiment with either inferring constructor arguments or adding an external method. If using an external method, is the idea to provide the c# code it corresponds to in a separate file? This approach would still use GetUninitializedObject object, however, so the runtime behavior will still rely on mocking.

Inferring relevant constructor arguments may be possible but the caveat is that constructor calls might alter the state of other objects in the program and taking into account the side-effects would be difficult. This approach will also be restricted to cases when the constructor has no loops or only has loops that are easy to unroll. I will try to find a solution but am not sure that it is possible to make it work in a general case.

Is there any need for returning a value from {:test} methods, though, if they don't represent the result of the test? Or are you thinking of calling {:test} methods directly from other code as well

The test methods currently generated by the Test Generation module can serve two purposes. You can either call them to make sure the code runs with no exceptions or you can call them to produce an oracle (e.g. if you have another implementation of the same functionality that you would like to test using this oracle). Allowing test methods to return non failure-compatible values would make it possible to reuse one method for these two purposes.

Let me change this PR to draft until I come up with another solution for mocking and then I will change this one accordingly!

[keyboardDrummer]

If using an external method, is the idea to provide the c# code it corresponds to in a separate file? This approach would still use GetUninitializedObject object, however, so the runtime behavior will still rely on mocking.

Yes that's the idea. @robin-aws would that alleviate your soundness concerns? I thought they came from changes the compilation of {:test}

[robin-aws]

If using an external method, is the idea to provide the c# code it corresponds to in a separate file? This approach would still use GetUninitializedObject object, however, so the runtime behavior will still rely on mocking.

Yes that's the idea. @robin-aws would that alleviate your soundness concerns? I thought they came from changes the compilation of {:test}

Yeah, I like this! Would the test generation also spit out the testRuntime.dfy "header" file with the extern method declaration? I like that since it puts that declaration in the right scope - I still don't love the idea of encouraging that approach for non-generated test code.

The test methods currently generated by the Test Generation module can serve two purposes. You can either call them to make sure the code runs with no exceptions or you can call them to produce an oracle (e.g. if you have another implementation of the same functionality that you would like to test using this oracle). Allowing test methods to return non failure-compatible values would make it possible to reuse one method for these two purposes.

Okay I'll buy that. :)

[Dargones]

I have looked at this problem further and I think I don't quite understand the unsoundness problem. @robin-aws, would you have a moment to take a look at this? I have been working on the solution @keyboardDrummer proposed but it would require more changes to the compiler (see below), so I wanted to make certain I understand what is the issue with the approach using {:test} first. Suppose we want to test the following functionality:

class Prime {
    var value:int;
    function IsValid():bool {
        // return true if value is prime
    }
    method Next() returns (p:Prime) 
        requires this.IsValid() 
        ensures p.IsValid() // + more postconditions
    {
        // compute and return next prime number
    }
}

The TestGeneration (or a human developer) would generate a test like the one below:

method {:test} test(p:Prime) returns (o: VoidOutcome) modifies p {
    p.value := 5;
    var next:Prime := p.Next();
    if next.value == 7 {
        return VoidSuccess;
    } else {
        return VoidFailure("Next prime number is not computed correctly");
    }
}

This method should be sound from the Dafny perspective. If it passes an invalid object to Next(), the verifier will complain. One can safely use modifies, since it is applied to the argument of a method. The only potential problem with setting the fields of an object in this manner is that some of them might be hidden due to encapsulation. But this only means that we won't be able to always generate tests like this. All tests generated in this way should be sound.

Now the suggestion is to generate an XUnit.Fact method that calls the test method like so:

[Xunit.Fact]
public static void test_CheckForFailureForXunit() {
    // in all other target languages, GetUninitializedObject can be replaced with zero constructor
    var p0 = FormatterServices.GetUninitializedObject(typeof(Prime)) as Prime;
    var r0 = test(p0);
    Xunit.Assert.False(r0.IsFailure(), "Dafny test failed: " + r0);
}

The only concern I see is that GetUninitializedObject might not return an object that is valid. In our case, it quite likely sets p0.value to 0, which is not a prime number. However, the test has been verified by Dafny meaning that Dafny provides a guarantee that by the time Next is called on the object, the object is valid. In a sense, it is the burden of the original developer of the Next method and not of the testing module to specify the pre- and postconditions.

The solution that uses {:extern} would still have the same caveat. There is no way to know what the state of the object after the call to GetUninitializedObject is but we can set its fields in a way to make the object valid.

[Dargones]

TestRuntime.CreateUnitialized<M.Value>();

It appears that, unfortunately, one cannot pass a type parameter to such a CreateUninitialized method. You would need to ensure that the generated value is fresh and doing so with a type parameter makes Resolver give the the argument of a fresh expression must denote an object or a set or sequence of objects (instead got T) error. So this means that one would have to define a separate extern method for every user-defined class and the compilation of these methods would have to be handled by the Dafny-to-the-language-of-choice compiler. So it won't be possible to remove the generation of the mocking code from the compiler, if that is the concern. Otherwise, sill working on implementing this!

[rakamaric]

Just catching up with this thread. I think one issue here is that we are making a distinction between human-written test cases and the ones generated by an automatic test case generator. I already discussed this separately with @Dargones.

In short, there should be no features being added to the Dafny unit testing framework solely to be used by the automatic test case generator. For example, methods annotated with {:test} should not be taking any arguments and should not have a return value. I still don't understand @Dargones argument for why a test method would ever need to return a value. Typically, the oracle is a part of the unit test method, and not a separate entity. Basically, I don't understand why we need this [Xunit.Fact] thingy to be a separate method.

Instead, this is how the test method should look like (and how a programmer would write it anyways):

method {:test} test(p:Prime) returns (o: VoidOutcome) modifies p {
    p.value := 5;
    var next:Prime := p.Next();
    assert(next.value == 7);
}

Am I missing something here?

[keyboardDrummer]

It appears that, unfortunately, one cannot pass a type parameter to such a CreateUninitialized method.

You're right. The problem is that the argument of fresh must be a reference type but there's currently no way to constraint a type parameter to be a reference type.

[keyboardDrummer]

For example, methods annotated with {:test} should not be taking any arguments and should not have a return value.

I'm confused, doesn't your example contain a method annotated with {:test} that does take an argument?

method {:test} test(p:Prime) returns (o: VoidOutcome) modifies p {
    p.value := 5;
    var next:Prime := p.Next();
    assert(next.value == 7);
}

[rakamaric]

Yes, the initial message does have an example with arguments. But I discussed this with @Dargones since then, and we agreed that we do not need arguments after all, which should simplify the implementation.
I had a chat with @Dargones just now, and I really like the solution that he's been working on with your help. He'll update the pull request soon. Thx!

[Dargones]

Closing, since this is an earlier version of PR#1809, which has now been merged. Thank you to everyone for all the feedback.