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

Assertion error when trying to use const seq comprehension as witness #405

Closed
robin-aws opened this issue Oct 25, 2019 · 2 comments · Fixed by #671
Closed

Assertion error when trying to use const seq comprehension as witness #405

robin-aws opened this issue Oct 25, 2019 · 2 comments · Fixed by #671

Comments

@robin-aws
Copy link
Member

To reproduce:

const WITNESS := seq(10, i => 0)
type Seq10 = s: seq<int> | |s| == 10 witness WITNESS

The error:

[ERROR] FATAL UNHANDLED EXCEPTION: System.Diagnostics.Contracts.ContractException: Assertion failed.
  at System.Runtime.CompilerServices.ContractHelper.TriggerFailureImplementation (System.Diagnostics.Contracts.ContractFailureKind kind, System.String displayMessage, System.String userMessage, System.String conditionText, System.Exception innerException) [0x0002f] in <b814b509d4ad406fb40c6c93e38929e7>:0 
  at System.Runtime.CompilerServices.ContractHelper.TriggerFailure (System.Diagnostics.Contracts.ContractFailureKind kind, System.String displayMessage, System.String userMessage, System.String conditionText, System.Exception innerException) [0x00000] in <b814b509d4ad406fb40c6c93e38929e7>:0 
  at System.Diagnostics.Contracts.Contract.ReportFailure (System.Diagnostics.Contracts.ContractFailureKind failureKind, System.String userMessage, System.String conditionText, System.Exception innerException) [0x0003a] in <b814b509d4ad406fb40c6c93e38929e7>:0 
  at System.Diagnostics.Contracts.Contract.Assert (System.Boolean condition) [0x00003] in <b814b509d4ad406fb40c6c93e38929e7>:0 
  at Microsoft.Boogie.NAryExpr..ctor (Microsoft.Boogie.IToken tok, Microsoft.Boogie.IAppliable fun, System.Collections.Generic.IList`1[T] args, System.Boolean immutable) [0x00043] in <30742c4912ce4f9d9ecac1dc3cfa27dc>:0 
  at Microsoft.Dafny.Translator.FunctionCall (Microsoft.Boogie.IToken tok, System.String function, Microsoft.Boogie.Type returnType, Microsoft.Boogie.Expr[] args) [0x00017] in <0e77b85e438844fcb706a98562f68691>:0 
  at Microsoft.Dafny.Translator+ExpressionTranslator.TrExpr (Microsoft.Dafny.Expression expr) [0x01a49] in <0e77b85e438844fcb706a98562f68691>:0 
  at Microsoft.Dafny.Translator.GetReadonlyField (Microsoft.Dafny.Field f) [0x00452] in <0e77b85e438844fcb706a98562f68691>:0 
  at Microsoft.Dafny.Translator+ExpressionTranslator+<>c__DisplayClass45_1.<TrExpr>b__0 (Microsoft.Dafny.Field field) [0x000d5] in <0e77b85e438844fcb706a98562f68691>:0 
  at Microsoft.Dafny.MemberSelectExpr.MemberSelectCase[A] (System.Func`2[T,TResult] fieldK, System.Func`2[T,TResult] functionK) [0x00022] in <0e77b85e438844fcb706a98562f68691>:0 
  at Microsoft.Dafny.Translator+ExpressionTranslator.TrExpr (Microsoft.Dafny.Expression expr) [0x00b9e] in <0e77b85e438844fcb706a98562f68691>:0 
  at Microsoft.Dafny.Translator+ExpressionTranslator.TrExpr (Microsoft.Dafny.Expression expr) [0x054a4] in <0e77b85e438844fcb706a98562f68691>:0 
  at Microsoft.Dafny.Translator+ExpressionTranslator.TrExpr (Microsoft.Dafny.Expression expr) [0x01c4a] in <0e77b85e438844fcb706a98562f68691>:0 
  at Microsoft.Dafny.Translator+ExpressionTranslator.TrExpr (Microsoft.Dafny.Expression expr) [0x02272] in <0e77b85e438844fcb706a98562f68691>:0 
  at Microsoft.Dafny.Translator.AddWellformednessCheck (Microsoft.Dafny.RedirectingTypeDecl decl) [0x0041c] in <0e77b85e438844fcb706a98562f68691>:0 
  at Microsoft.Dafny.Translator.AddTypeDecl (Microsoft.Dafny.SubsetTypeDecl dd) [0x0002c] in <0e77b85e438844fcb706a98562f68691>:0 
  at Microsoft.Dafny.Translator.AddTypeDecl (Microsoft.Dafny.RevealableTypeDecl d) [0x00075] in <0e77b85e438844fcb706a98562f68691>:0 
  at Microsoft.Dafny.Translator.DoTranslation (Microsoft.Dafny.Program p, Microsoft.Dafny.ModuleDefinition forModule) [0x00429] in <0e77b85e438844fcb706a98562f68691>:0 
  at Microsoft.Dafny.Translator+<Translate>d__47.MoveNext () [0x000ea] in <0e77b85e438844fcb706a98562f68691>:0 
  at Microsoft.Dafny.DafnyDriver+<Translate>d__6.MoveNext () [0x00119] in <c9e5fdb7261143f1ba3cff517b570207>:0 
  at Microsoft.Dafny.DafnyDriver.Boogie (System.String baseName, System.Collections.Generic.IEnumerable`1[T] boogiePrograms, System.String programId, System.Collections.Generic.Dictionary`2[System.String,Microsoft.Boogie.PipelineStatistics]& statss, Microsoft.Boogie.PipelineOutcome& oc) [0x0012f] in <c9e5fdb7261143f1ba3cff517b570207>:0 
  at Microsoft.Dafny.DafnyDriver.ProcessFiles (System.Collections.Generic.IList`1[T] dafnyFiles, System.Collections.ObjectModel.ReadOnlyCollection`1[T] otherFileNames, Microsoft.Dafny.ErrorReporter reporter, System.Boolean lookForSnapshots, System.String programId) [0x00222] in <c9e5fdb7261143f1ba3cff517b570207>:0 
  at Microsoft.Dafny.DafnyDriver.ThreadMain (System.String[] args) [0x0003a] in <c9e5fdb7261143f1ba3cff517b570207>:0 
  at Microsoft.Dafny.DafnyDriver+<>c__DisplayClass1_0.<Main>b__0 () [0x00001] in <c9e5fdb7261143f1ba3cff517b570207>:0 
  at System.Threading.ThreadHelper.ThreadStart_Context (System.Object state) [0x00014] in <b814b509d4ad406fb40c6c93e38929e7>:0 
  at System.Threading.ExecutionContext.RunInternal (System.Threading.ExecutionContext executionContext, System.Threading.ContextCallback callback, System.Object state, System.Boolean preserveSyncCtx) [0x00071] in <b814b509d4ad406fb40c6c93e38929e7>:0 
  at System.Threading.ExecutionContext.Run (System.Threading.ExecutionContext executionContext, System.Threading.ContextCallback callback, System.Object state, System.Boolean preserveSyncCtx) [0x00000] in <b814b509d4ad406fb40c6c93e38929e7>:0 
  at System.Threading.ExecutionContext.Run (System.Threading.ExecutionContext executionContext, System.Threading.ContextCallback callback, System.Object state) [0x0002b] in <b814b509d4ad406fb40c6c93e38929e7>:0 
  at System.Threading.ThreadHelper.ThreadStart () [0x00008] in <b814b509d4ad406fb40c6c93e38929e7>:0

Either changing the sequence comprehension to a sequence display or inlining the value into the type declaration avoids the bug.

Probably related to #339 - this is likely not supported, but an earlier phase is failing to catch it and raise an error.
@RustanLeino
Copy link
Collaborator

Thanks for the bug report. Here's a workaround:

function method WITNESS(): seq<int> {
  seq(10, i => 0)
}
type Seq10 = s: seq<int> | |s| == 10 witness WITNESS()

davidcok pushed a commit to davidcok/dafny that referenced this issue Jun 15, 2020
fix: Fixed dafny-lang#405 by adding a 'modifies ' spec to the WITNESS…
706b9ea 
…'s wellformedness check
@davidcok davidcok mentioned this issue Jun 15, 2020
Merged
@davidcok
Copy link
Collaborator

Fixed in PR #671

davidcok pushed a commit to davidcok/dafny that referenced this issue Jun 19, 2020
fix: Fixed dafny-lang#405 by adding a 'modifies ' spec to the WITNESS…
ff1db26 
…'s wellformedness check
davidcok pushed a commit to davidcok/dafny that referenced this issue Jun 19, 2020
fix: Fixed dafny-lang#405 by adding a 'modifies ' spec to the WITNESS…
41001c2 
…'s wellformedness check
RustanLeino pushed a commit that referenced this issue Jun 23, 2020
@davidcok
#405: Fixed Mal-formed boogie produced in checking sequence comprehen…
e18c2be 
…sions (#671)

Fixes #405
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

#405: Fixed Mal-formed boogie produced in checking sequence comprehensions davidcok/dafny
3 participants
@davidcok @RustanLeino @robin-aws