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.

Sign up for GitHub

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

Jump to bottom

Crash on refinement #2402

Closed
MikaelMayer opened this issue Jul 13, 2022 · 0 comments · Fixed by #2990
Closed

Crash on refinement #2402

MikaelMayer opened this issue Jul 13, 2022 · 0 comments · Fixed by #2990
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

Comments

@MikaelMayer
Copy link
Member

The following code crashes Dafny on VSCode with an error on the t:

abstract module M 
{ 
    type T
    const t : T
    lemma Randomlemma()
    {
        forall i:int {}
    }
}

module N refines M 
{ 
}
Dafny encountered an internal error. Please report it at <https://github.com/dafny-lang/dafny/issues>.
System.AggregateException: One or more errors occurred. (Object reference not set to an instance of an object.)
 ---> System.NullReferenceException: Object reference not set to an instance of an object.
   at Microsoft.Dafny.Translator.TrForallProof(ForallStmt s, BoogieStmtListBuilder definedness, BoogieStmtListBuilder exporter, List`1 locals, ExpressionTranslator etran) in dafny\Source\Dafny\Verifier\Translator.TrStatement.cs:line 1047
   at Microsoft.Dafny.Translator.TrStmt(Statement stmt, BoogieStmtListBuilder builder, List`1 locals, ExpressionTranslator etran) in dafny\Source\Dafny\Verifier\Translator.TrStatement.cs:line 413
   at Microsoft.Dafny.Translator.TrStmtList(List`1 stmts, BoogieStmtListBuilder builder, List`1 locals, ExpressionTranslator etran) in dafny\Source\Dafny\Verifier\Translator.cs:line 8580
   at Microsoft.Dafny.Translator.TrStmt(Statement stmt, BoogieStmtListBuilder builder, List`1 locals, ExpressionTranslator etran) in dafny\Source\Dafny\Verifier\Translator.TrStatement.cs:line 302
   at Microsoft.Dafny.Translator.AddMethodImpl(Method m, Procedure proc, Boolean wellformednessProc) in dafny\Source\Dafny\Verifier\Translator.ClassMembers.cs:line 647
   at Microsoft.Dafny.Translator.AddMethod_Top(Method m, Boolean isByMethod, Boolean includeAllMethods) in dafny\Source\Dafny\Verifier\Translator.ClassMembers.cs:line 198
   at Microsoft.Dafny.Translator.AddClassMembers(TopLevelDeclWithMembers c, Boolean includeAllMethods, Boolean includeInformationAboutType) in dafny\Source\Dafny\Verifier\Translator.ClassMembers.cs:line 71
   at Microsoft.Dafny.Translator.AddTypeDecl(RevealableTypeDecl d) in dafny\Source\Dafny\Verifier\Translator.cs:line 1198
   at Microsoft.Dafny.Translator.DoTranslation(Program p, ModuleDefinition forModule) in dafny\Source\Dafny\Verifier\Translator.cs:line 782
   at Microsoft.Dafny.Translator.Translate(Program p, ErrorReporter reporter, TranslatorFlags flags)+MoveNext() in dafny\Source\Dafny\Verifier\Translator.cs:line 854
   at System.Collections.Generic.List`1..ctor(IEnumerable`1 collection)
   at System.Linq.Enumerable.ToList[TSource](IEnumerable`1 source)
   at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.<>c__DisplayClass9_0.<GetVerificationTasksAsync>b__3() in dafny\Source\DafnyLanguageServer\Language\DafnyProgramVerifier.cs:line 59
   at System.Threading.Tasks.Task`1.InnerInvoke()
   at System.Threading.Tasks.Task.<>c.<.cctor>b__272_0(Object obj)
   at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state)
--- End of stack trace from previous location ---
   at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state)
   at System.Threading.Tasks.Task.ExecuteWithThreadLocal(Task& currentTaskSlot, Thread threadPoolThread)
--- End of stack trace from previous location ---
   at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(DafnyDocument document, CancellationToken cancellationToken) in dafny\Source\DafnyLanguageServer\Language\DafnyProgramVerifier.cs:line 59
   at Microsoft.Dafny.LanguageServer.Workspace.TextDocumentLoader.PrepareVerificationTasksAsync(DafnyDocument loaded, CancellationToken cancellationToken) in dafny\Source\DafnyLanguageServer\Workspace\TextDocumentLoader.cs:line 108
   at Microsoft.Dafny.LanguageServer.Workspace.DocumentDatabase.LoadVerificationTasksAsync(Task`1 resolvedDocumentTask, CancellationToken cancellationToken) in dafny\Source\DafnyLanguageServer\Workspace\DocumentDatabase.cs:line 245
   --- End of inner exception stack trace ---
@MikaelMayer MikaelMayer added the crash Dafny crashes on this input, or generates malformed code that can not be executed label Jul 13, 2022
@MikaelMayer MikaelMayer changed the title Crash Crash on refinement Jul 13, 2022
@cpitclaudel cpitclaudel added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label Sep 20, 2022
MikaelMayer added a commit that referenced this issue Nov 4, 2022
@MikaelMayer
Add test for issue #2402
145754e
@MikaelMayer MikaelMayer mentioned this issue Nov 4, 2022
Merged
keyboardDrummer added a commit that referenced this issue Nov 9, 2022
@MikaelMayer @keyboardDrummer
Fix: Refinements get errors at the correct place in LSP (#2990)
10bb18d 
This PR fixes #2402
The problem was that errors reported on refined modules used refinement
tokens.
Refined tokens are like tokens, except that the actual file name is in
ActualFileName and the FileName is the previous filename + "[" + name of
refining module + "]"
The Language server was creating Uris from FileName, no matter the token
type, which led it to not find the document and report the errors.
That means it was launching verification when resolution fails on
refined modules.

This PR solves the problem by making the Language server aware of
Refinement tokens and extract the underlying token for reporting
purposes, rather than taking the FileName of the refined token.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Co-authored-by: Remy Willems <[email protected]>
prvshah51 pushed a commit to prvshah51/dafny that referenced this issue Nov 9, 2022
@MikaelMayer @keyboardDrummer @prvshah51
Fix: Refinements get errors at the correct place in LSP (dafny-lang#2990
b3549fe 
)

This PR fixes dafny-lang#2402
The problem was that errors reported on refined modules used refinement
tokens.
Refined tokens are like tokens, except that the actual file name is in
ActualFileName and the FileName is the previous filename + "[" + name of
refining module + "]"
The Language server was creating Uris from FileName, no matter the token
type, which led it to not find the document and report the errors.
That means it was launching verification when resolution fails on
refined modules.

This PR solves the problem by making the Language server aware of
Refinement tokens and extract the underlying token for reporting
purposes, rather than taking the FileName of the refined token.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Co-authored-by: Remy Willems <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
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
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix: Refinements get errors at the correct place in LSP dafny-lang/dafny
2 participants
@MikaelMayer @cpitclaudel