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.

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

Resolver crash #2068

Closed
erniecohen opened this issue Apr 26, 2022 · 1 comment · Fixed by #2994
Closed

Resolver crash #2068

erniecohen opened this issue Apr 26, 2022 · 1 comment · Fixed by #2994
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

@erniecohen
Copy link

erniecohen commented Apr 26, 2022

The following crashes for me in 3.5.0.40314:

type St = s:St_ | (forall o | o in s :: o.i(this))
type St_ = map<nat,Ob>
type Ob {
    predicate i(s:St_)
}
@robin-aws robin-aws added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking labels Apr 26, 2022
@robin-aws
Copy link
Member

The exception this triggers:

Unhandled exception. 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.Resolver.GetThisType(IToken tok, TopLevelDeclWithMembers cl) in /Users/salkeldr/Documents/GitHub/dafny/Source/Dafny/Resolver.cs:line 14514
   at Microsoft.Dafny.Resolver.ResolveExpression(Expression expr, ResolveOpts opts) in /Users/salkeldr/Documents/GitHub/dafny/Source/Dafny/Resolver.cs:line 14636
   at Microsoft.Dafny.Resolver.ResolveActualParameters(ActualBindings bindings, List`1 formals, IToken callTok, Object context, ResolveOpts opts, Dictionary`2 typeMap, Expression receiver) in /Users/salkeldr/Documents/GitHub/dafny/Source/Dafny/Resolver.cs:line 16871
   at Microsoft.Dafny.Resolver.ResolveApplySuffix(ApplySuffix e, ResolveOpts opts, Boolean allowMethodCall) in /Users/salkeldr/Documents/GitHub/dafny/Source/Dafny/Resolver.cs:line 16731
   at Microsoft.Dafny.Resolver.ResolveExpression(Expression expr, ResolveOpts opts) in /Users/salkeldr/Documents/GitHub/dafny/Source/Dafny/Resolver.cs:line 14716
   at Microsoft.Dafny.Resolver.ResolveExpression(Expression expr, ResolveOpts opts) in /Users/salkeldr/Documents/GitHub/dafny/Source/Dafny/Resolver.cs:line 15203
   at Microsoft.Dafny.Resolver.ResolveExpression(Expression expr, ResolveOpts opts) in /Users/salkeldr/Documents/GitHub/dafny/Source/Dafny/Resolver.cs:line 14582
   at Microsoft.Dafny.Resolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies, Boolean isAnExport) in /Users/salkeldr/Documents/GitHub/dafny/Source/Dafny/Resolver.cs:line 2703
   at Microsoft.Dafny.Resolver.ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig, Boolean isAnExport) in /Users/salkeldr/Documents/GitHub/dafny/Source/Dafny/Resolver.cs:line 1032
   at Microsoft.Dafny.Resolver.ResolveProgram(Program prog) in /Users/salkeldr/Documents/GitHub/dafny/Source/Dafny/Resolver.cs:line 507
   at Microsoft.Dafny.Main.Resolve(Program program, ErrorReporter reporter) in /Users/salkeldr/Documents/GitHub/dafny/Source/Dafny/DafnyMain.cs:line 162
   at Microsoft.Dafny.Main.ParseCheck(IList`1 files, String programName, ErrorReporter reporter, Program& program) in /Users/salkeldr/Documents/GitHub/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/salkeldr/Documents/GitHub/dafny/Source/DafnyDriver/DafnyDriver.cs:line 249

Note the original example also has an explicit error: Scratch.dfy(1,42): Error: type int does not have a member i. This is because o in s is the same as o in s.Keys rather than o in s.Values, so o gets the type int rather than Ob. But fixing that doesn't change the crash so it doesn't seem relevant.

@cpitclaudel cpitclaudel added the crash Dafny crashes on this input, or generates malformed code that can not be executed label May 7, 2022
@fabiomadge fabiomadge removed their assignment Aug 9, 2022
MikaelMayer added a commit that referenced this issue Nov 4, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
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
Development

Successfully merging a pull request may close this issue.

4 participants