Requesting counterexample generates Internal Error in VSCode

[hmijail]

When requesting a counterexample, an Internal Error is shown in VSCode.

Code:

method test(a: seq<int>) returns (b: seq<int>)
    ensures |a| >= |b|
{
  return b;
}

Error:

CounterExample request failed: Internal Error - System.ArgumentException: state does not contain position: bug_counterexample.d..(4,0):initial state at Microsoft.Dafny.LanguageServer.Handlers.Custom.DafnyCounterExampleHandler.CounterExampleLoader.GetPositionFromInitialState(IState state) in /Users/runner/work/language-server-csharp/language-server-csharp/Source/DafnyLS/Handlers/Custom/DafnyCounterExampleHandler.cs:line 97 at Microsoft.Dafny.LanguageServer.Handlers.Custom.DafnyCounterExampleHandler.CounterExampleLoader.GetCounterExample(StateNode state) in /Users/runner/work/language-server-csharp/language-server-csharp/Source/DafnyLS/Handlers/Custom/DafnyCounterExampleHandler.cs:line 90 at System.Linq.Enumerable.WhereSelectEnumerableIterator`2.MoveNext() at System.Collections.Generic.LargeArrayBuilder`1.AddRange(IEnumerable`1 items) at System.Collections.Generic.SparseArrayBuilder`1.ReserveOrAdd(IEnumerable`1 items) at System.Linq.Enumerable.SelectManySingleSelectorIt...

[hmijail]

In case it helps: before I reduced the bug-triggering code, the error reported was different:

CounterExample request failed: Internal Error - System.ArgumentException: function 'Seq#Index' previously created with arity 1, now trying to recreate with arity 2 at Microsoft.Boogie.Model.MkFunc(String name, Int32 arity) at Microsoft.Boogie.ModelViewer.Dafny.DafnyModel..ctor(Model m, ViewOptions opts) in /Users/runner/work/language-server-csharp/language-server-csharp/dafny/Source/DafnyServer/boogie/DafnyProvider.cs:line 45 at Microsoft.Boogie.ModelViewer.Dafny.Provider.GetLanguageSpecificModel(Model m, ViewOptions opts) in /Users/runner/work/language-server-csharp/language-server-csharp/dafny/Source/DafnyServer/boogie/DafnyProvider.cs:line 25 at Microsoft.Dafny.LanguageServer.Handlers.Custom.DafnyCounterExampleHandler.CounterExampleLoader.GetLanguagSpecificModel(Model model) in /Users/runner/work/language-server-csharp/language-server-csharp/Source/DafnyLS/Handlers/Custom/DafnyCounterExampleHandler.cs:line 74 at System.Linq.Enumerable.SelectEnumerableIterator`2.MoveNe...

[hmijail]

On second thought, looks like this issue should be reported to the VSCode integration repo.
I did so and am closing this one. dafny-lang/ide-vscode#25

[camrein]

I am reopening this issue as it fits better to the language server than the VSCode extension.

Quote from the last comment of dafny-lang/ide-vscode/issues/25

I removed the log.txt file and requested the counterexample. Resulting log follows:

2021-03-14 22:48:52.4911|FATAL|OmniSharp.Extensions.JsonRpc.InputHandler|Failed to handle request dafny/counterExample 8 System.ArgumentException: state does not contain position: bug_counterexample.d..(4,0):initial state
   at Microsoft.Dafny.LanguageServer.Handlers.Custom.DafnyCounterExampleHandler.CounterExampleLoader.GetPositionFromInitialState(IState state) in /Users/runner/work/language-server-csharp/language-server-csharp/Source/DafnyLS/Handlers/Custom/DafnyCounterExampleHandler.cs:line 99
   at Microsoft.Dafny.LanguageServer.Handlers.Custom.DafnyCounterExampleHandler.CounterExampleLoader.GetCounterExample(StateNode state) in /Users/runner/work/language-server-csharp/language-server-csharp/Source/DafnyLS/Handlers/Custom/DafnyCounterExampleHandler.cs:line 90
   at System.Linq.Enumerable.WhereSelectEnumerableIterator`2.MoveNext()
   at System.Collections.Generic.LargeArrayBuilder`1.AddRange(IEnumerable`1 items)
   at System.Collections.Generic.SparseArrayBuilder`1.ReserveOrAdd(IEnumerable`1 items)
   at System.Linq.Enumerable.SelectManySingleSelectorIterator`2.ToArray()
   at Microsoft.Dafny.LanguageServer.Handlers.Custom.DafnyCounterExampleHandler.CounterExampleLoader.GetCounterExamples() in /Users/runner/work/language-server-csharp/language-server-csharp/Source/DafnyLS/Handlers/Custom/DafnyCounterExampleHandler.cs:line 58
   at Microsoft.Dafny.LanguageServer.Handlers.Custom.DafnyCounterExampleHandler.Handle(CounterExampleParams request, CancellationToken cancellationToken) in /Users/runner/work/language-server-csharp/language-server-csharp/Source/DafnyLS/Handlers/Custom/DafnyCounterExampleHandler.cs:line 33
   at MediatR.Internal.RequestHandlerWrapperImpl`2.<>c__DisplayClass1_0.<Handle>g__Handler|0()
   at MediatR.Pipeline.RequestExceptionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at MediatR.Pipeline.RequestExceptionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at MediatR.Pipeline.RequestExceptionActionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at MediatR.Pipeline.RequestExceptionActionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at MediatR.Pipeline.RequestPostProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at MediatR.Pipeline.RequestPreProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at OmniSharp.Extensions.LanguageServer.Server.Pipelines.ResolveCommandPipeline`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at OmniSharp.Extensions.JsonRpc.RequestRouterBase`1.RouteRequest(TDescriptor descriptor, Request request, CancellationToken token)
   at OmniSharp.Extensions.JsonRpc.InputHandler.<>c__DisplayClass38_0.<<RouteRequest>b__5>d.MoveNext()

Does the automatic verification work as expected?

I'm a beginner at Dafny, but yes, it seems to work as expected when following various tutorials.

I have added your example to the integration test solution of the language server. However, it does not appear that it yields an error on any of the tested platforms (macos-10.15, ubuntu-16.04, windows-2019). Would you mind telling me a bit more about your setup? For example a screenshot of your VSCode workspace. Does the error happen no matter what you do? E.g., you open your test file and immediately request the counterexample? What about editing the code a little bit and then request the counterexample? And do you have an example that produces your original error? It appears to me that the provided counterexample information from Boogie is incomplete.

[hmijail]

Does the error happen no matter what you do? E.g., you open your test file and immediately request the counterexample?

For completeness, I just uninstalled my existing "dotnet", "dotnet-sdk" and "dafny" packages from brew, and the dafny extension in VSC. I then reinstalled the VSC extension, let it do its downloads, and manually installed the suggested official .NET package.

Then I restarted VSC, opened a file with the snippet I reported, and requested the counterexample.

The result is the same. See screenshot.

What about editing the code a little bit and then request the counterexample?

I have tried adding some empty new lines around. Nothing seems to change.

And do you have an example that produces your original error?

Yes.

predicate sorted (a: seq<int>)
{
    forall j, k::0 <= j < k < |a|  ==> a[j] <= a[k]
}

method unique(a: seq<int>) returns (b: seq<int>)
    requires sorted(a)
    ensures sorted(b)
    ensures |a| == 0 ==> b == []
    ensures |a| >= |b|
{
    if (|a| == 0) {
        return [];
    }
    assert |a| > 0;

    b:=[a[0]];
    var i := 1;
    assert |b| > 0;

    while (i < |a|)
        invariant i <= |a|
        invariant i >= |b|
        //invariant |b| > 0
        invariant |b| <= |a|
        //decreases |a| - i
    {
        assert |b| > 0;
        if(a[i] != b[|b|-1]){
            b := b + [a[i]];
        }
        //i := i+1;
    }
    assert i == |a|;
    assert |b| > 0;

    return b;
}

[hmijail]

Also: I seem to remember that at various points of editing a file the counterexamples appear or trigger the internal error. Next time I find the situation I'll try to isolate an example.

[hmijail]

Actually, in that last code example if you uncomment the line

        //invariant |b| > 0

the counterexamples work.

[camrein]

Thank you very much for the detailed information. I finally managed to reproduce the error with your second example. Unfortunately, I still do not have luck in reproducing the error of your condensed example. Just to make sure: Does the error happen there always or only sporadically?

@RustanLeino It appears that the issue resolves around DafnyServer's DafnyProvider.cs. Do you have any idea what the reason might be?

2021-03-16 08:48:06.5383|FATAL|OmniSharp.Extensions.JsonRpc.InputHandler|Failed to handle request dafny/counterExample 16 System.ArgumentException: function 'Seq#Index' previously created with arity 1, now trying to recreate with arity 2
   at Microsoft.Boogie.Model.MkFunc(String name, Int32 arity)
   at Microsoft.Boogie.ModelViewer.Dafny.DafnyModel..ctor(Model m, ViewOptions opts) in D:\Data\Development\git\language-server-csharp\dafny\Source\DafnyServer\boogie\DafnyProvider.cs:line 50
   at Microsoft.Boogie.ModelViewer.Dafny.Provider.GetLanguageSpecificModel(Model m, ViewOptions opts) in D:\Data\Development\git\language-server-csharp\dafny\Source\DafnyServer\boogie\DafnyProvider.cs:line 25
   at Microsoft.Dafny.LanguageServer.Handlers.Custom.DafnyCounterExampleHandler.CounterExampleLoader.GetLanguagSpecificModel(Model model) in D:\Data\Development\git\language-server-csharp\Source\DafnyLS\Handlers\Custom\DafnyCounterExampleHandler.cs:line 74
   at System.Linq.Enumerable.SelectEnumerableIterator`2.MoveNext()
   at System.Linq.Enumerable.SelectManySingleSelectorIterator`2.ToArray()
   at Microsoft.Dafny.LanguageServer.Handlers.Custom.DafnyCounterExampleHandler.CounterExampleLoader.GetCounterExamples() in D:\Data\Development\git\language-server-csharp\Source\DafnyLS\Handlers\Custom\DafnyCounterExampleHandler.cs:line 58
   at Microsoft.Dafny.LanguageServer.Handlers.Custom.DafnyCounterExampleHandler.Handle(CounterExampleParams request, CancellationToken cancellationToken) in D:\Data\Development\git\language-server-csharp\Source\DafnyLS\Handlers\Custom\DafnyCounterExampleHandler.cs:line 33
   at MediatR.Internal.RequestHandlerWrapperImpl`2.<>c__DisplayClass1_0.<Handle>g__Handler|0()
   at MediatR.Pipeline.RequestExceptionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at MediatR.Pipeline.RequestExceptionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at MediatR.Pipeline.RequestExceptionActionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at MediatR.Pipeline.RequestExceptionActionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at MediatR.Pipeline.RequestPostProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at MediatR.Pipeline.RequestPreProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at OmniSharp.Extensions.LanguageServer.Server.Pipelines.ResolveCommandPipeline`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at OmniSharp.Extensions.JsonRpc.RequestRouterBase`1.RouteRequest(TDescriptor descriptor, Request request, CancellationToken token)
   at OmniSharp.Extensions.JsonRpc.InputHandler.<>c__DisplayClass38_0.<<RouteRequest>b__5>d.MoveNext()

[hmijail]

Does the error happen there always or only sporadically?

Always.