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

Assumption failed from too deeply nested AST, resulting in a hard crash #1331

Open
sorawee opened this issue Jul 27, 2021 · 2 comments
Open

Assumption failed from too deeply nested AST, resulting in a hard crash #1331

sorawee opened this issue Jul 27, 2021 · 2 comments
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: resolver Resolution and typechecking

Comments

@sorawee
Copy link
Contributor

sorawee commented Jul 27, 2021 

method Main () 
{
  var x := [[[[(() => () => [[[[[1]]]]])]]]];
  var _ := [[[[(() => () => [[[[[1]]]]])]]]] + x;
}

results in:

Process terminated. Assumption failed.
   at Microsoft.Dafny.Resolver.Reaches(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6198
   at Microsoft.Dafny.Resolver.<>c__DisplayClass112_0.<Reaches_aux>b__0(Type su) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6227
   at System.Linq.Enumerable.Any[TSource](IEnumerable`1 source, Func`2 predicate)
   at Microsoft.Dafny.Resolver.Reaches_aux(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6227
   at Microsoft.Dafny.Resolver.Reaches(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6201
   at Microsoft.Dafny.Resolver.<>c__DisplayClass112_0.<Reaches_aux>b__0(Type su) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6227
   at System.Linq.Enumerable.Any[TSource](IEnumerable`1 source, Func`2 predicate)
   at Microsoft.Dafny.Resolver.Reaches_aux(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6227
   at Microsoft.Dafny.Resolver.Reaches(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6201
   at Microsoft.Dafny.Resolver.<>c__DisplayClass112_0.<Reaches_aux>b__0(Type su) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6227
   at System.Linq.Enumerable.Any[TSource](IEnumerable`1 source, Func`2 predicate)
   at Microsoft.Dafny.Resolver.Reaches_aux(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6227
   at Microsoft.Dafny.Resolver.Reaches(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6201
   at Microsoft.Dafny.Resolver.<>c__DisplayClass112_0.<Reaches_aux>b__0(Type su) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6227
   at System.Linq.Enumerable.Any[TSource](IEnumerable`1 source, Func`2 predicate)
   at Microsoft.Dafny.Resolver.Reaches_aux(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6227
   at Microsoft.Dafny.Resolver.Reaches(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6201
   at Microsoft.Dafny.Resolver.<>c__DisplayClass112_0.<Reaches_aux>b__0(Type su) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6227
   at System.Linq.Enumerable.Any[TSource](IEnumerable`1 source, Func`2 predicate)
   at Microsoft.Dafny.Resolver.Reaches_aux(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6227
   at Microsoft.Dafny.Resolver.Reaches(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6201
   at Microsoft.Dafny.Resolver.Reaches_aux(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6216
   at Microsoft.Dafny.Resolver.Reaches(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6201
   at Microsoft.Dafny.Resolver.Reaches_aux(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6216
   at Microsoft.Dafny.Resolver.Reaches(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6201
   at Microsoft.Dafny.Resolver.Reaches_aux(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6216
   at Microsoft.Dafny.Resolver.Reaches(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6201
   at Microsoft.Dafny.Resolver.Reaches_aux(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6216
   at Microsoft.Dafny.Resolver.Reaches(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6201
   at Microsoft.Dafny.Resolver.Reaches_aux(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6216
   at Microsoft.Dafny.Resolver.Reaches(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6201
   at Microsoft.Dafny.Resolver.Reaches_aux(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6216
   at Microsoft.Dafny.Resolver.Reaches(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6201
   at Microsoft.Dafny.Resolver.Reaches_aux(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6216
   at Microsoft.Dafny.Resolver.Reaches(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6201
   at Microsoft.Dafny.Resolver.<>c__DisplayClass112_0.<Reaches_aux>b__0(Type su) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6227
   at System.Linq.Enumerable.Any[TSource](IEnumerable`1 source, Func`2 predicate)
   at Microsoft.Dafny.Resolver.Reaches_aux(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6227
   at Microsoft.Dafny.Resolver.Reaches(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6201
   at Microsoft.Dafny.Resolver.<>c__DisplayClass112_0.<Reaches_aux>b__0(Type su) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6227
   at System.Linq.Enumerable.Any[TSource](IEnumerable`1 source, Func`2 predicate)
   at Microsoft.Dafny.Resolver.Reaches_aux(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6227
   at Microsoft.Dafny.Resolver.Reaches(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6201
   at Microsoft.Dafny.Resolver.<>c__DisplayClass112_0.<Reaches_aux>b__0(Type su) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6227
   at System.Linq.Enumerable.Any[TSource](IEnumerable`1 source, Func`2 predicate)
   at Microsoft.Dafny.Resolver.Reaches_aux(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6227
   at Microsoft.Dafny.Resolver.Reaches(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6201
   at Microsoft.Dafny.Resolver.<>c__DisplayClass112_0.<Reaches_aux>b__0(Type su) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6227
   at System.Linq.Enumerable.Any[TSource](IEnumerable`1 source, Func`2 predicate)
   at Microsoft.Dafny.Resolver.Reaches_aux(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6227
   at Microsoft.Dafny.Resolver.Reaches(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6201
   at Microsoft.Dafny.Resolver.Reaches_aux(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6216
   at Microsoft.Dafny.Resolver.Reaches(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6201
   at Microsoft.Dafny.Resolver.Reaches_aux(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6216
   at Microsoft.Dafny.Resolver.Reaches(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6201
   at Microsoft.Dafny.Resolver.Reaches_aux(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6216
   at Microsoft.Dafny.Resolver.Reaches(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6201
   at Microsoft.Dafny.Resolver.Reaches_aux(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6216
   at Microsoft.Dafny.Resolver.Reaches(Type t, TypeProxy proxy, Int32 direction, HashSet`1 visited) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 6201
   at Microsoft.Dafny.Resolver.AssignKnownEnd(TypeProxy proxy, Boolean keepConstraints, Boolean fullStrength) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 5933
   at Microsoft.Dafny.Resolver.ConstrainSubtypeRelation_Aux(Type super, Type sub, TypeConstraint c, Boolean keepConstraints, Boolean allowDecisions) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 4327
   at Microsoft.Dafny.Resolver.ConstrainSubtypeRelation(Type super, Type sub, ErrorMsg errMsg, Boolean keepConstraints, Boolean allowDecisions) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 4303
   at Microsoft.Dafny.Resolver.ConstrainSubtypeRelation(Type super, Type sub, IToken tok, String msg, Object[] msgArgs) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 4171
   at Microsoft.Dafny.Resolver.ResolveExpression(Expression expr, ResolveOpts opts) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 14957
   at Microsoft.Dafny.Resolver.ResolveUpdateStmt(UpdateStmt update, ICodeContext codeContext, Int32 errorCountBeforeCheckingLhs) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 12654
   at Microsoft.Dafny.Resolver.ResolveConcreteUpdateStmt(ConcreteUpdateStatement s, ICodeContext codeContext) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 12619
   at Microsoft.Dafny.Resolver.ResolveStatement(Statement stmt, ICodeContext codeContext) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 10895
   at Microsoft.Dafny.Resolver.ResolveStatementWithLabels(Statement stmt, ICodeContext codeContext) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 13272
   at Microsoft.Dafny.Resolver.ResolveBlockStatement(BlockStmt blockStmt, ICodeContext codeContext) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 13242
   at Microsoft.Dafny.Resolver.ResolveMethod(Method m) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 10091
   at Microsoft.Dafny.Resolver.ResolveClassMemberBodies(TopLevelDeclWithMembers cl) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 9322
   at Microsoft.Dafny.Resolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies, Boolean isAnExport) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 2755
   at Microsoft.Dafny.Resolver.ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig, Boolean isAnExport) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 1004
   at Microsoft.Dafny.Resolver.ResolveProgram(Program prog) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 487
   at Microsoft.Dafny.Main.Resolve(Program program, ErrorReporter reporter) in /Users/sorawee/projects/dafny/Source/Dafny/DafnyMain.cs:line 165
   at Microsoft.Dafny.Main.ParseCheck(IList`1 files, String programName, ErrorReporter reporter, Program& program) in /Users/sorawee/projects/dafny/Source/Dafny/DafnyMain.cs:line 113
   at Microsoft.Dafny.DafnyDriver.ProcessFiles(IList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, ErrorReporter reporter, Boolean lookForSnapshots, String programId) in /Users/sorawee/projects/dafny/Source/DafnyDriver/DafnyDriver.cs:line 265
   at Microsoft.Dafny.DafnyDriver.ThreadMain(String[] args) in /Users/sorawee/projects/dafny/Source/DafnyDriver/DafnyDriver.cs:line 57
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass1_0.<Main>b__0() in /Users/sorawee/projects/dafny/Source/DafnyDriver/DafnyDriver.cs:line 36
   at System.Threading.ThreadHelper.ThreadStart_Context(Object state)
   at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state)
   at System.Threading.ThreadHelper.ThreadStart()
../Dafny/Scripts/dafny: line 34: 13110 Abort trap: 6           "$DOTNET" "$DAFNY" "$@"

Note that

method Main () 
{
  var x := [[[[(() => () => [[[[[1]]]]])]]]];
  var _ := x + x;
}

works fine.
@sorawee
Copy link
Contributor Author

sorawee commented Jul 27, 2021

Ah, well, looks like this is expected, though the error message perhaps could be improved.

https://github.com/dafny-lang/dafny/blob/master/Source/Dafny/Resolver.cs#L6197

@keyboardDrummer keyboardDrummer added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking labels Jul 27, 2021
@keyboardDrummer
Copy link
Member

I think this is a bug, at least the reporting should be better :) Thanks for reporting.

@sorawee sorawee changed the title Assumption failed from sequence append, resulting in a hard crash Assumption failed from too deeply nested AST, resulting in a hard crash Sep 13, 2021
@cpitclaudel cpitclaudel added the crash Dafny crashes on this input, or generates malformed code that can not be executed label May 7, 2022
@sorawee sorawee mentioned this issue Jun 17, 2022
Open
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 part: resolver Resolution and typechecking
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@keyboardDrummer @cpitclaudel @sorawee