NullReferenceException during counterexample generation

dijkstracula commented 2 years ago

On Dafny with /Version output Dafny 3.5.0.40314:

Consider the following Dafny program:

method foo(n: nat) returns (ret: array<string>)
{
    ret := new string[n];

    var i := 0;
    while i < n
        invariant 0 <= i <= n
        invariant forall j :: 0 <= j < i ==> j % 2 == 0 ==> ret[j] == "even"
        invariant forall j :: 0 <= j < i ==> j % 2 == 1 ==> ret[j] == "odd"
    {
        if i % 2 == 0 {
            ret[i] := "odd";
        } else {
            ret[i] := "even";
        }
        i := i + 1;
    }
}

Dafny correctly indicates that our loop invariants are incorrect (as the implementation swapped the cases). The VS Code plugin is able to show counterexamples, but the CLI interface has a few problems:

1. Outdated documentation string for the `/extractCounterexample` flag:

The CLI interface explicitly states that some additional flags need to be set.

$ ~/code/dafny/Binaries/Dafny Foo.dfy /help | grep -A4 '/extractCounter'
/extractCounterexample
    If verification fails, report a detailed counterexample for the first
    failing assertion. Requires specifying the /mv option as well as
    /proverOpt:0:model_compress=false and /proverOpt:0:model.completion=true.
/verificationLogger:<configuration string>
➜  fizzbuzz git:(main) ✗

However, the model_compress option is no longer known to Dafny:

$ ~/code/dafny/Binaries/Dafny Foo.dfy /extractCounterexample /mv model /proverOpt:0:model_compress=false
/proverOpt:0:model.completion=true
Fatal Error: ProverException: Unrecognised prover option: 0:model_compress=false

Crash during counterexample generation

More seriously, a null pointer exception is raised while attempting to extract a counterexample (irrespective of whether or not those unknown flags are present):

$ ~/code/dafny/Binaries/Dafny Foo.dfy /extractCounterexample /mv model
/Users/ntaylor/school/phd/projects/dafny_sandbox/fizzbuzz/Foo.dfy(8,18): Error: This loop invariant might not be maintained by the loop.
/Users/ntaylor/school/phd/projects/dafny_sandbox/fizzbuzz/Foo.dfy(8,18): Related message: loop invariant violation
Execution trace:
    (0,0): anon0
    /Users/ntaylor/school/phd/projects/dafny_sandbox/fizzbuzz/Foo.dfy(6,5): anon23_LoopHead
    (0,0): anon23_LoopBody
    /Users/ntaylor/school/phd/projects/dafny_sandbox/fizzbuzz/Foo.dfy(6,5): anon24_Else
    /Users/ntaylor/school/phd/projects/dafny_sandbox/fizzbuzz/Foo.dfy(6,5): anon34_Else
    (0,0): anon35_Then
    (0,0): anon22
/Users/ntaylor/school/phd/projects/dafny_sandbox/fizzbuzz/Foo.dfy(9,18): Error: This loop invariant might not be maintained by the loop.
/Users/ntaylor/school/phd/projects/dafny_sandbox/fizzbuzz/Foo.dfy(9,18): Related message: loop invariant violation
Execution trace:
    (0,0): anon0
    /Users/ntaylor/school/phd/projects/dafny_sandbox/fizzbuzz/Foo.dfy(6,5): anon23_LoopHead
    (0,0): anon23_LoopBody
    /Users/ntaylor/school/phd/projects/dafny_sandbox/fizzbuzz/Foo.dfy(6,5): anon24_Else
    /Users/ntaylor/school/phd/projects/dafny_sandbox/fizzbuzz/Foo.dfy(6,5): anon34_Else
    (0,0): anon35_Else
    (0,0): anon22

Dafny program verifier finished with 0 verified, 2 errors
Counterexample for first failing assertion:
/Users/ntaylor/school/phd/projects/dafny_sandbox/fizzbuzz/Foo.dfy(2,0): initial state:
        n : int = 5854
        ret : ? = ()
/Users/ntaylor/school/phd/projects/dafny_sandbox/fizzbuzz/Foo.dfy(3,24):
Unhandled exception. System.NullReferenceException: Object reference not set to an instance of an object.
   at DafnyServer.CounterexampleGeneration.DafnyModel.GetFieldName(Element elt) in /Users/ntaylor/code/dafny/Source/DafnyServer/CounterExampleGeneration/DafnyModel.cs:line 659
   at DafnyServer.CounterexampleGeneration.DafnyModel.GetExpansion(DafnyModelState state, DafnyModelVariable var) in /Users/ntaylor/code/dafny/Source/DafnyServer/CounterExampleGeneration/DafnyModel.cs:line 614
   at DafnyServer.CounterexampleGeneration.DafnyModelVariable.GetExpansion() in /Users/ntaylor/code/dafny/Source/DafnyServer/CounterExampleGeneration/DafnyModelVariable.cs:line 91
   at DafnyServer.CounterexampleGeneration.DafnyModelState.ExpandedVariableSet(Nullable`1 maxDepth) in /Users/ntaylor/code/dafny/Source/DafnyServer/CounterExampleGeneration/DafnyModelState.cs:line 73
   at Microsoft.Dafny.DafnyDriver.PrintCounterexample(String modelViewFile) in /Users/ntaylor/code/dafny/Source/DafnyDriver/DafnyDriver.cs:line 281
   at Microsoft.Dafny.DafnyDriver.ProcessFiles(ExecutionEngineOptions options, IList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, ErrorReporter reporter, Boolean lookForSnapshots, String programId) in /Users/ntaylor/code/dafny/Source/DafnyDriver/DafnyDriver.cs:line 265
   at Microsoft.Dafny.DafnyDriver.ThreadMain(String[] args) in /Users/ntaylor/code/dafny/Source/DafnyDriver/DafnyDriver.cs:line 57
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass1_0.<Main>b__0() in /Users/ntaylor/code/dafny/Source/DafnyDriver/DafnyDriver.cs:line 37
   at System.Threading.Thread.StartCallback()
[2]    37646 abort      ~/code/dafny/Binaries/Dafny Foo.dfy /extractCounterexample /mv model
$

I can't figure out exactly how the VSCode plugin or the language server is driving the Dafny counterexample generator here, but since this doesn't seem to be a problem in the IDE, I guess something specific to the CLI is broken.

Thanks!

atomb commented 2 years ago

My first hypothesis here is that, when model compression is enabled, variables that Dafny expects to exist in the model are not available, and therefore it crashes. Disabling model compression (as described here) allows Dafny to complete. However, it should at the very least produce a useful error message when used with model compression, and ideally still produce some useful output.

atomb commented 2 years ago

I suspect that the appropriate fix for this is to automatically enable the necessary prover options, as described in #2029.

MikaelMayer commented 2 years ago

The documentation was fixed, so this issue is no longer an issue. However, I'm adding a recovery mechanism now so that 1) No more null pointer exception is thrown 2) If a null pointer exception was thrown previously, an error depicting the missing command-line flag is shown on the command line.

dafny-lang / dafny