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

"Fatal Unhandled Exception" error for Sequence Construction Expressions #334

Closed
JunyoungLim opened this issue Aug 1, 2019 · 1 comment · Fixed by #335
Closed

"Fatal Unhandled Exception" error for Sequence Construction Expressions #334

JunyoungLim opened this issue Aug 1, 2019 · 1 comment · Fixed by #335
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Comments

@JunyoungLim
Copy link
Collaborator

The following code generates the fatal unhandled exception:

function method FromAtoB(a: seq<int>): (b: seq<int>) {
    seq(|a|, i => a[i])
}
[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 <f7cedb26ce694cd281e4450870c6fe49>: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 <f7cedb26ce694cd281e4450870c6fe49>:0
  at System.Diagnostics.Contracts.Contract.ReportFailure (System.Diagnostics.Contracts.ContractFailureKind failureKind, System.String userMessage, System.String conditionText, System.Exception innerException) [0x0003a] in <f7cedb26ce694cd281e4450870c6fe49>:0
  at System.Diagnostics.Contracts.Contract.Assert (System.Boolean condition) [0x00003] in <f7cedb26ce694cd281e4450870c6fe49>: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 <451e59e8cecd4b8a8d901251129e1be1>:0
  at Microsoft.Dafny.Translator.FunctionCall (Microsoft.Boogie.IToken tok, System.String function, Microsoft.Boogie.Type returnType, Microsoft.Boogie.Expr[] args) [0x00017] in <6511abc92ea846e0b34f20222561029d>:0
  at Microsoft.Dafny.Translator+ExpressionTranslator.TrExpr (Microsoft.Dafny.Expression expr) [0x01a54] in <6511abc92ea846e0b34f20222561029d>:0
  at Microsoft.Dafny.Translator.FunctionAxiom (Microsoft.Dafny.Function f, Microsoft.Dafny.Expression body, System.Collections.Generic.ICollection`1[T] lits, Microsoft.Dafny.TopLevelDecl overridingClass) [0x00ab1] in <6511abc92ea846e0b34f20222561029d>:0
  at Microsoft.Dafny.Translator.AddFunctionAxiom (Microsoft.Dafny.Function f, Microsoft.Dafny.Expression body) [0x00001] in <6511abc92ea846e0b34f20222561029d>:0
  at Microsoft.Dafny.Translator.AddClassMember_Function (Microsoft.Dafny.Function f) [0x0008d] in <6511abc92ea846e0b34f20222561029d>:0
  at Microsoft.Dafny.Translator.AddFunction_Top (Microsoft.Dafny.Function f) [0x00020] in <6511abc92ea846e0b34f20222561029d>:0
  at Microsoft.Dafny.Translator.AddClassMembers (Microsoft.Dafny.ClassDecl c, System.Boolean includeMethods) [0x0034a] in <6511abc92ea846e0b34f20222561029d>:0
  at Microsoft.Dafny.Translator.DoTranslation (Microsoft.Dafny.Program p, Microsoft.Dafny.ModuleDefinition forModule) [0x00457] in <6511abc92ea846e0b34f20222561029d>:0
  at Microsoft.Dafny.Translator+<Translate>d__47.MoveNext () [0x000ea] in <6511abc92ea846e0b34f20222561029d>:0
  at Microsoft.Dafny.DafnyDriver+<Translate>d__6.MoveNext () [0x00119] in <1726fb2ac8b046fb9f3fa158ff53a56f>: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 <1726fb2ac8b046fb9f3fa158ff53a56f>: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 <1726fb2ac8b046fb9f3fa158ff53a56f>:0
  at Microsoft.Dafny.DafnyDriver.ThreadMain (System.String[] args) [0x0003a] in <1726fb2ac8b046fb9f3fa158ff53a56f>:0
  at Microsoft.Dafny.DafnyDriver+<>c__DisplayClass1_0.<Main>b__0 () [0x00001] in <1726fb2ac8b046fb9f3fa158ff53a56f>:0
  at System.Threading.ThreadHelper.ThreadStart_Context (System.Object state) [0x00014] in <f7cedb26ce694cd281e4450870c6fe49>:0
  at System.Threading.ExecutionContext.RunInternal (System.Threading.ExecutionContext executionContext, System.Threading.ContextCallback callback, System.Object state, System.Boolean preserveSyncCtx) [0x00071] in <f7cedb26ce694cd281e4450870c6fe49>:0
  at System.Threading.ExecutionContext.Run (System.Threading.ExecutionContext executionContext, System.Threading.ContextCallback callback, System.Object state, System.Boolean preserveSyncCtx) [0x00000] in <f7cedb26ce694cd281e4450870c6fe49>:0
  at System.Threading.ExecutionContext.Run (System.Threading.ExecutionContext executionContext, System.Threading.ContextCallback callback, System.Object state) [0x0002b] in <f7cedb26ce694cd281e4450870c6fe49>:0
  at System.Threading.ThreadHelper.ThreadStart () [0x00008] in <f7cedb26ce694cd281e4450870c6fe49>:0
@mschlaipfer mschlaipfer added boogie kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label and removed boogie labels Aug 1, 2019
@samuelgruetter
Copy link
Collaborator

The bug only appears inside functions, not inside methods, and unfortunately, the test suite only tests this feature inside methods, but not inside functions.

// works
method testMethod(a: seq<int>) returns (b: seq<int>)
    ensures a == b;
{
    return seq(|a|, i requires 0 <= i < |a| => a[i]);
}

// crashes Dafny, only difference is going from method to function
function testFunction(a: seq<int>): (b: seq<int>)
    ensures a == b;
{
    seq(|a|, i requires 0 <= i < |a| => a[i])
}

The problem is that inside functions which don't read the heap, ExpressionTranslator.HeapExpr is null, and passed to Seq#Create, but Boogie requires that all arguments passed are non-null, so this assertion fails.

RustanLeino added a commit to RustanLeino/dafny that referenced this issue Aug 2, 2019
@RustanLeino
Note that seq-construction needs heap argument
ebb1f22 
Fixes dafny-lang#334
@RustanLeino RustanLeino mentioned this issue Aug 2, 2019
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
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.

Note that seq-construction needs heap argument RustanLeino/dafny
3 participants
@samuelgruetter @mschlaipfer @JunyoungLim