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

Crash when running -testContracts on refinement of abstract module #4845

Closed
atomb opened this issue Dec 4, 2023 · 3 comments · Fixed by #4910
Closed

Crash when running -testContracts on refinement of abstract module #4845

atomb opened this issue Dec 4, 2023 · 3 comments · Fixed by #4910
Assignees
@atomb
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

Comments

@atomb
Copy link
Member

atomb commented Dec 4, 2023 •
edited
Loading

Dafny version

4.3.0

Code to produce this issue

https://github.com/aws/aws-cryptographic-material-providers-library-java/blob/main/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Index.dfy

Command to run and resulting output

$ dafny -noVerify \
      -vcsCores:1 \
      -compileTarget:java \
      -spillTargetCode:3 \
      -compile:0 \
      -optimizeErasableDatatypeWrapper:0 \
      -compileSuffix:1 \
      -quantifierSyntax:3 \
      -unicodeChar:0 \
      -functionSyntax:3 \
      -useRuntimeLib \
      -testContracts:Externs \
      -library:StandardLibrary/src/Index.dfy \
      AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Index.dfy

...
Unhandled exception. System.AggregateException: One or more errors occurred. (One or more errors occurred. (One or more errors occurred. (Object reference not set to an instance of an object.)))
 ---> System.AggregateException: One or more errors occurred. (One or more errors occurred. (Object reference not set to an instance of an object.))
 ---> 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.ModuleResolver.ResolveCallStmt(CallStmt s, ResolutionContext resolutionContext, Type receiverType)
   at Microsoft.Dafny.ModuleResolver.ResolveStatement(Statement stmt, ResolutionContext resolutionContext)
   at Microsoft.Dafny.ModuleResolver.ResolveStatementWithLabels(Statement stmt, ResolutionContext resolutionContext)
   at Microsoft.Dafny.ModuleResolver.ResolveBlockStatement(BlockStmt blockStmt, ResolutionContext resolutionContext)
   at Microsoft.Dafny.Method.Resolve(ModuleResolver resolver)
   at Microsoft.Dafny.ModuleResolver.ResolveClassMemberBodies(TopLevelDeclWithMembers cl)
   at Microsoft.Dafny.ModuleResolver.ResolveNamesAndInferTypesForOneDeclaration(TopLevelDecl topd)
   at Microsoft.Dafny.ModuleResolver.ResolveNamesAndInferTypes(List`1 declarations, Boolean initialRound)
   at Microsoft.Dafny.ModuleResolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies, String moduleName, Boolean isAnExport)
   at Microsoft.Dafny.ModuleDefinition.Resolve(ModuleSignature sig, ModuleResolver resolver, Boolean isAnExport)
   at Microsoft.Dafny.LiteralModuleDecl.Resolve(ModuleResolver resolver, CompilationData compilation)
   at Microsoft.Dafny.ModuleResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl)
   at Microsoft.Dafny.ProgramResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl)
   at Microsoft.Dafny.ProgramResolver.Resolve(CancellationToken cancellationToken)
   at Microsoft.Dafny.DafnyMain.<>c__DisplayClass5_0.<Resolve>b__0()
   at System.Threading.Tasks.Task.InnerInvoke()
   at System.Threading.Tasks.Task.<>c.<.cctor>b__272_0(Object obj)
   at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state)
--- End of stack trace from previous location ---
   at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state)
   at System.Threading.Tasks.Task.ExecuteWithThreadLocal(Task& currentTaskSlot, Thread threadPoolThread)
   --- End of inner exception stack trace ---
   at System.Threading.Tasks.Task.ThrowIfExceptional(Boolean includeTaskCanceledExceptions)
   at System.Threading.Tasks.Task.Wait(Int32 millisecondsTimeout, CancellationToken cancellationToken)
   at System.Threading.Tasks.Task.Wait()
   at Microsoft.Dafny.DafnyMain.Resolve(Program program)
   at Microsoft.Dafny.DafnyDriver.ProcessFilesAsync(IReadOnlyList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, DafnyOptions options, Boolean lookForSnapshots, String programId)
   --- End of inner exception stack trace ---
   at System.Threading.Tasks.Task.ThrowIfExceptional(Boolean includeTaskCanceledExceptions)
   at System.Threading.Tasks.Task`1.GetResultCore(Boolean waitCompletionNotification)
   at System.Threading.Tasks.Task`1.get_Result()
   at Microsoft.Dafny.DafnyDriver.ThreadMain(TextWriter outputWriter, TextWriter errorWriter, TextReader inputReader, String[] args)
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass11_0.<MainWithWriters>b__0()
   at System.Threading.Tasks.Task`1.InnerInvoke()
   at System.Threading.Tasks.Task.<>c.<.cctor>b__272_0(Object obj)
   at System.Threading.ExecutionContext.RunFromThreadPoolDispatchLoop(Thread threadPoolThread, ExecutionContext executionContext, ContextCallback callback, Object state)
--- End of stack trace from previous location ---
   at System.Threading.ExecutionContext.RunFromThreadPoolDispatchLoop(Thread threadPoolThread, ExecutionContext executionContext, ContextCallback callback, Object state)
   at System.Threading.Tasks.Task.ExecuteWithThreadLocal(Task& currentTaskSlot, Thread threadPoolThread)
   --- End of inner exception stack trace ---
   at System.Threading.Tasks.Task`1.GetResultCore(Boolean waitCompletionNotification)
   at System.Threading.Tasks.Task`1.get_Result()
   at Microsoft.Dafny.DafnyDriver.MainWithWriters(TextWriter outputWriter, TextWriter errorWriter, TextReader inputReader, String[] args)
   at Microsoft.Dafny.DafnyDriver.Main(String[] args)
   at Dafny.Dafny.Main(String[] args)
...

What happened?

It should have successfully generated target code without throwing an exception.

The exception comes from trying to dereference callee, asserted to be non-null here

(I used a release build above, so it's a later null dereference that fails. With a debug build, the assertion fails.)

The crash is happening on wrapper code generated by the implementation of testContracts, but I've done some debugging of the generation, and the Method property is set to a non-null value there when running on thins example. So somewhere later, perhaps during cloning, property becomes null.

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

Mac
@atomb atomb added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label Dec 4, 2023
@atomb atomb changed the title Crash when running -testContracts on abstract module Crash when running -testContracts on refinement of abstract module Dec 4, 2023
@atomb
Copy link
Member Author

atomb commented Dec 4, 2023

Running with Dafny 4.1.0 results in a different error:

Unhandled exception. System.AggregateException: One or more errors occurred. (An item with the same key has already been added. Key: Com.Amazonaws.software.amazon.cryptography.services.dynamodb.internaldafny._default.DynamoDBClient__dafny_checked)
 ---> System.ArgumentException: An item with the same key has already been added. Key: Com.Amazonaws.software.amazon.cryptography.services.dynamodb.internaldafny._default.DynamoDBClient__dafny_checked
   at System.Collections.Generic.Dictionary`2.TryInsert(TKey key, TValue value, InsertionBehavior behavior)
   at Microsoft.Dafny.ExpectContracts.PostCompileCloneAndResolve(ModuleDefinition moduleDefinition)
   at Microsoft.Dafny.Resolver.ResolveProgram(Program prog)
   at Microsoft.Dafny.Main.Resolve(Program program, ErrorReporter reporter)
   at Microsoft.Dafny.DafnyDriver.ProcessFilesAsync(IList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, ErrorReporter reporter, Boolean lookForSnapshots, String programId)
   --- End of inner exception stack trace ---
   at System.Threading.Tasks.Task.ThrowIfExceptional(Boolean includeTaskCanceledExceptions)
   at System.Threading.Tasks.Task`1.GetResultCore(Boolean waitCompletionNotification)
   at System.Threading.Tasks.Task`1.get_Result()
   at Microsoft.Dafny.DafnyDriver.ThreadMain(String[] args)
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass10_0.<Main>b__0()
   at System.Threading.Thread.StartCallback()

Dafny 4.2.0 gives the same error as 4.3.0.

@atomb atomb self-assigned this Dec 7, 2023
@atomb
Copy link
Member Author

atomb commented Dec 11, 2023

Some more detail. This error comes up when processing the wrapper around AbstractComAmazonawsKmsService.KmsClient(). When the wrapper is generated, it includes a call statement to KmsClient() in which the MethodSelect.Member field is non-null. This call statement gets cloned in a context in which CloneResolvedFields is false, so that Member field is not copied and the resulting MemberSelectExpr has a null Member field.

@keyboardDrummer keyboardDrummer added the crash Dafny crashes on this input, or generates malformed code that can not be executed label Dec 18, 2023
@atomb
Copy link
Member Author

atomb commented Dec 20, 2023 •
edited
Loading

I've narrowed this down to a smaller example.

abstract module A {
    method {:extern "AA"} A() returns (r: int)
      ensures r > 0
}

module M refines A {
}

If this code is in RefineContract.dfy, then dafny /testContracts:Externs RefineContract.dfy yields the following:

Process terminated. Assertion failed.
   at Microsoft.Dafny.ModuleResolver.ResolveCallStmt(CallStmt s, ResolutionContext resolutionContext, Type receiverType) in /Users/aarotomb/Repositories/dafny/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs:line 3137
   at Microsoft.Dafny.ModuleResolver.ResolveStatement(Statement stmt, ResolutionContext resolutionContext) in /Users/aarotomb/Repositories/dafny/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs:line 3824
   at Microsoft.Dafny.ModuleResolver.ResolveStatementWithLabels(Statement stmt, ResolutionContext resolutionContext) in /Users/aarotomb/Repositories/dafny/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs:line 3086
   at Microsoft.Dafny.ModuleResolver.ResolveBlockStatement(BlockStmt blockStmt, ResolutionContext resolutionContext) in /Users/aarotomb/Repositories/dafny/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs:line 3056
   at Microsoft.Dafny.Method.Resolve(ModuleResolver resolver) in /Users/aarotomb/Repositories/dafny/Source/DafnyCore/AST/Members/Method.cs:line 358
   at Microsoft.Dafny.ModuleResolver.ResolveClassMemberBodies(TopLevelDeclWithMembers cl) in /Users/aarotomb/Repositories/dafny/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs:line 2788
   at Microsoft.Dafny.ModuleResolver.ResolveNamesAndInferTypesForOneDeclaration(TopLevelDecl topd) in /Users/aarotomb/Repositories/dafny/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs:line 154
   at Microsoft.Dafny.ModuleResolver.ResolveNamesAndInferTypes(List`1 declarations, Boolean initialRound) in /Users/aarotomb/Repositories/dafny/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs:line 61
   at Microsoft.Dafny.ModuleResolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies, String moduleDescription, Boolean isAnExport) in /Users/aarotomb/Repositories/dafny/Source/DafnyCore/Resolver/ModuleResolver.cs:line 1106
   at Microsoft.Dafny.ModuleDefinition.Resolve(ModuleSignature sig, ModuleResolver resolver, String exportSetName) in /Users/aarotomb/Repositories/dafny/Source/DafnyCore/AST/Modules/ModuleDefinition.cs:line 484
   at Microsoft.Dafny.LiteralModuleDecl.Resolve(ModuleResolver resolver, CompilationData compilation) in /Users/aarotomb/Repositories/dafny/Source/DafnyCore/AST/Modules/LiteralModuleDecl.cs:line 123
   at Microsoft.Dafny.ModuleResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl) in /Users/aarotomb/Repositories/dafny/Source/DafnyCore/Resolver/ModuleResolver.cs:line 180
   at Microsoft.Dafny.ProgramResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl) in /Users/aarotomb/Repositories/dafny/Source/DafnyCore/Resolver/ProgramResolver.cs:line 175
   at Microsoft.Dafny.ProgramResolver.Resolve(CancellationToken cancellationToken) in /Users/aarotomb/Repositories/dafny/Source/DafnyCore/Resolver/ProgramResolver.cs:line 69
   at Microsoft.Dafny.DafnyMain.<>c__DisplayClass8_0.<Resolve>b__0() in /Users/aarotomb/Repositories/dafny/Source/DafnyCore/DafnyMain.cs:line 87
   at System.Threading.Tasks.Task.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.Boogie.CustomStackSizePoolTaskScheduler.WorkLoop()
   at System.Threading.Thread.StartCallback()

atomb added a commit to atomb/dafny that referenced this issue Dec 20, 2023
@atomb
Fix dafny-lang#4845
9f768f9
@atomb atomb mentioned this issue Dec 20, 2023
Merged
atomb added a commit that referenced this issue Jan 4, 2024
@atomb
Fix extern contract checking on abstract modules (#4910)
ab22a7d 
### Description

Previously, compiling an abstract module with an `{:extern}` method
using `--test-assumptions Externs` would cause an assertion failure.
This was due to interleaving between the contract checking wrapper
generator and the module refinement rewriter. This PR fixes the problem
by generating contract checking wrappers for the whole program after
resolution is finished, rather than as each module finishes resolution.

Fixes #4845

### How has this been tested?

Tested by `contract-wrappers/RefineContract.dfy`.

By submitting this pull request, I confirm that my contribution is made
under the terms of the MIT license.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@atomb atomb

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
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix extern contract checking on abstract modules atomb/dafny
2 participants
@atomb @keyboardDrummer