search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.88k stars 256 forks source link

Crash during translation #3792

Closed MikaelMayer closed 1 year ago

MikaelMayer commented 1 year ago

Dafny version

4.0.1

Code to produce this issue

/// # Random variable. extracted from any number of bits
  datatype ImapSimulator_<!A, B> = ImapSimulator(
    input: iset<A>,
    apply: A --> B)
  {
    ghost predicate Valid() {
      forall i <- input :: apply.requires(i)
    }
  }

  type ImapSimulator<!A, B> =
    X: ImapSimulator_<A, B> |
    X.Valid() witness ImapSimulator(iset{}, (x: A) requires false => match() {})
//                  error probably comes from here                   ^^^^^^^^^^

Command to run and resulting output

Process terminated. Assertion failed.
   at Microsoft.Dafny.Translator.<>c__DisplayClass428_7.<CheckWellformedWithResult>b__9(BoogieStmtListBuilder b) in dafny\Source\DafnyCore\Verifier\Translator.ExpressionWellformed.cs:line 1040
   at Microsoft.Dafny.Translator.BplIfIf(IToken tk, Boolean yes, Expr guard, BoogieStmtListBuilder builder, Action`1 k) in dafny\Source\DafnyCore\Verifier\Translator.BoogieFactory.cs:line 784
   at Microsoft.Dafny.Translator.<>c__DisplayClass428_6.<CheckWellformedWithResult>b__7(BoogieStmtListBuilder newBuilder) in dafny\Source\DafnyCore\Verifier\Translator.ExpressionWellformed.cs:line 1030
   at Microsoft.Dafny.Translator.BplIfIf(IToken tk, Boolean yes, Expr guard, BoogieStmtListBuilder builder, Action`1 k) in dafny\Source\DafnyCore\Verifier\Translator.BoogieFactory.cs:line 784
   at Microsoft.Dafny.Translator.<>c__DisplayClass428_5.<CheckWellformedWithResult>b__6(BoogieStmtListBuilder nextBuilder) in dafny\Source\DafnyCore\Verifier\Translator.ExpressionWellformed.cs:line 991
   at Microsoft.Dafny.Translator.BplIfIf(IToken tk, Boolean yes, Expr guard, BoogieStmtListBuilder builder, Action`1 k) in dafny\Source\DafnyCore\Verifier\Translator.BoogieFactory.cs:line 784
   at Microsoft.Dafny.Translator.CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Expr result, Type resultType, List`1 locals, BoogieStmtListBuilder builder, ExpressionTranslator etran) in dafny\Source\DafnyCore\Verifier\Translator.ExpressionWellformed.cs:line 979
   at Microsoft.Dafny.Translator.CheckWellformed(Expression expr, WFOptions options, List`1 locals, BoogieStmtListBuilder builder, ExpressionTranslator etran) in dafny\Source\DafnyCore\Verifier\Translator.ExpressionWellformed.cs:line 238
   at Microsoft.Dafny.Translator.CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Expr result, Type resultType, List`1 locals, BoogieStmtListBuilder builder, ExpressionTranslator etran) in dafny\Source\DafnyCore\Verifier\Translator.ExpressionWellformed.cs:line 752
   at Microsoft.Dafny.Translator.CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Expr result, Type resultType, List`1 locals, BoogieStmtListBuilder builder, ExpressionTranslator etran) in dafny\Source\DafnyCore\Verifier\Translator.ExpressionWellformed.cs:line 1114
   at Microsoft.Dafny.Translator.CheckWellformed(Expression expr, WFOptions options, List`1 locals, BoogieStmtListBuilder builder, ExpressionTranslator etran) in dafny\Source\DafnyCore\Verifier\Translator.ExpressionWellformed.cs:line 238
   at Microsoft.Dafny.Translator.AddWellformednessCheck(RedirectingTypeDecl decl) in dafny\Source\DafnyCore\Verifier\Translator.cs:line 4477
   at Microsoft.Dafny.Translator.AddTypeDecl(SubsetTypeDecl dd) in dafny\Source\DafnyCore\Verifier\Translator.cs:line 1273
   at Microsoft.Dafny.Translator.AddTypeDecl(RevealableTypeDecl d) in dafny\Source\DafnyCore\Verifier\Translator.cs:line 1232
   at Microsoft.Dafny.Translator.DoTranslation(Program p, ModuleDefinition forModule) in dafny\Source\DafnyCore\Verifier\Translator.cs:line 805
   at Microsoft.Dafny.Translator.Translate(Program p, ErrorReporter reporter, TranslatorFlags flags)+MoveNext() in dafny\Source\DafnyCore\Verifier\Translator.cs:line 876
   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__DisplayClass8_0.<GetVerificationTasksAsync>b__1() in dafny\Source\DafnyLanguageServer\Language\DafnyProgramVerifier.cs:line 51
   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)
   at System.Threading.Tasks.Task.ExecuteWithThreadLocal(Task& currentTaskSlot, Thread threadPoolThread)
   at System.Threading.Tasks.Task.ExecuteEntry()
   at System.Threading.Tasks.TaskScheduler.TryExecuteTask(Task task)
   at Microsoft.Dafny.LanguageServer.Workspace.ThreadTaskScheduler.TaskMain(Object data) in dafny\Source\DafnyLanguageServer\Workspace\ThreadTaskScheduler.cs:line 40
   at System.Threading.Thread.StartHelper.Callback(Object state)
   at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state)
   at System.Threading.Thread.StartCallback()

What happened?

A crash occurred and no translation/verification was made.

What type of operating system are you experiencing the problem on?

Windows

MikaelMayer commented 1 year ago

I got errors I could not find a simple way to fix, besides the obvious fix of adding Witness as a child to SubsetTypeDecl Basically, Dafny is creating a trigger like this: ImapSimulator(iset{}, (x: A) requires false => match() {}).apply.requires(i) Which, translated to Boogie, creates tons of error like

3792module.bpl(3299,31): Error: quantifiers are not allowed in triggers 3792module.bpl(3300,35): Error: quantifiers are not allowed in triggers 3792module.bpl(3301,29): Error: quantifiers are not allowed in triggers 3792module.bpl(3302,72): Error: boolean operators are not allowed in triggers looking at the generated code, I see in a trigger AtLayer((lambda $l#9#ly#0: LayerType :: ... and ...$IsBox($l#9#x#0, _module.ImapSimulator$A) && false), which are responsible for the boogie errors. Now, removing these triggers in Boogie make the code to verify without issue. On the dafny side, there is a test if (!CanSafelyInline(fexp, f)) { that is taking the "else" branch, but if I had take it the "then" branch, it verifies without error. Obviously, I would like to tell Dafny that it's not safe to inline (fexp, f) where fexp isImapSimulator(iset{}, (x: A) requires false => match () { }).Valid() and f is the Valid predicate. But the check tests only variables, not the presence of lambda expressions. @leino why is it failing and what is the best course forward? I thought of either Saying it's never safe to inline a function Creating a test on the object to ensure it can be converted to trigger (do we have a function like that) Something else that works.