Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Language server crashes on elephant operator #2667

Closed
MikaelMayer opened this issue Aug 31, 2022 · 0 comments · Fixed by #2668
Closed

Language server crashes on elephant operator #2667

MikaelMayer opened this issue Aug 31, 2022 · 0 comments · Fixed by #2668
Labels
crash Dafny crashes on this input, or generates malformed code that can not be executed kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo)

Comments

@MikaelMayer
Copy link
Member

The following block crashes the language server on verification

module {:options "/functionSyntax:4"} Library {
  // Library
  datatype Option<T> = Some(value: T) | None
  datatype Result<T> = Success(value: T) | Failure(s: string, pos: int) {
    predicate IsFailure() {
      Failure?
    }
    function PropagateFailure<U>(): Result<U>
      requires IsFailure()
    {
      Failure(s, pos)
    }
    function Extract(): T
      requires !IsFailure()
    {
      value
    }
  }
}
module Parser {
  import opened Library

  datatype Parser = Parser(expected: string) | Log(p: Parser, message: string)
  {
    method {:termination false} Parse(s: string, i: nat)
      returns (result: Result<(string, nat)>)
    {
      if Log? {
        var v1 :- p.Parse(s, i); // Removing this line makes the language server not crash anymore.
      }
      
      result := Failure("bam", i);
    }
  }
}

Error thrown:

at System.String.Ctor(Char c, Int32 count)
   at Microsoft.Dafny.RangeToken.get_val() in dafny\Source\Dafny\AST\DafnyAst.cs:line 8814
   at Microsoft.Dafny.TokenWrapper.get_val() in dafny\Source\Dafny\AST\DafnyAst.cs:line 8791
   at Microsoft.Dafny.LanguageServer.Language.BoogieExtensions.GetLspRange(IToken startToken, IToken endToken) in dafny\Source\DafnyLanguageServer\Language\BoogieExtensions.cs:line 28
   at Microsoft.Dafny.LanguageServer.Workspace.VerificationProgressReporter.<ReportAssertionBatchResult>g__AddChildOutcome|14_0(Counterexample counterexample, AssertCmd assertCmd, IToken token, GutterVerificationStatus status, IToken secondaryToken, String assertDisplay, String assertIdentifier, <>c__DisplayClass14_0& , <>c__DisplayClass14_1& ) in dafny\Source\DafnyLanguageServer\Workspace\VerificationProgressReporter.cs:line 373
...
@MikaelMayer MikaelMayer added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo) crash Dafny crashes on this input, or generates malformed code that can not be executed labels Aug 31, 2022
MikaelMayer added a commit that referenced this issue Aug 31, 2022
Fixes #2667 by remarking that sometimes, Tok is before EndTok for an obscure reason.
In the case of the elephant operator in `var x :- Parse()`, Tok designates `:-` and EndTok designates `x`, probably because the declaration is the same as the update.
I fixed the generation of faulty rangeToken like this for all statements.
Tested in the language server tests directly.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
crash Dafny crashes on this input, or generates malformed code that can not be executed kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo)
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant