From ab22a7d85c0707d86c6d4eaa0fae0bf89dbff762 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Thu, 4 Jan 2024 06:21:22 -0800 Subject: [PATCH] Fix extern contract checking on abstract modules (#4910) ### 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. --- Source/DafnyCore/Rewriters/ExpectContracts.cs | 66 +++++++++++-------- .../contract-wrappers/AbstractExtern1.cs | 10 +++ .../contract-wrappers/AbstractExtern2.cs | 10 +++ .../LitTest/contract-wrappers/AllExterns.dfy | 2 +- .../contract-wrappers/AllExterns.dfy.expect | 4 +- .../contract-wrappers/RefineContract.dfy | 14 ++++ .../contract-wrappers/TestedExterns.dfy | 2 +- .../TestedExterns.dfy.expect | 4 +- 8 files changed, 78 insertions(+), 34 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AbstractExtern1.cs create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AbstractExtern2.cs create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/RefineContract.dfy diff --git a/Source/DafnyCore/Rewriters/ExpectContracts.cs b/Source/DafnyCore/Rewriters/ExpectContracts.cs index 79feda0ddb0..738996a2523 100644 --- a/Source/DafnyCore/Rewriters/ExpectContracts.cs +++ b/Source/DafnyCore/Rewriters/ExpectContracts.cs @@ -1,7 +1,6 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; -using Microsoft.Extensions.Logging.Abstractions; using static Microsoft.Dafny.RewriterErrors; namespace Microsoft.Dafny; @@ -222,39 +221,50 @@ private static void RegisterResolvedByMethod(Function f, TopLevelDeclWithMembers } /// - /// Add wrappers for certain top-level declarations in the given module. - /// This runs after the first pass of resolution so that it has access to - /// ghostness information, attributes and call targets. + /// Adds wrappers for certain top-level declarations in the given + /// program and redirects callers to call those wrappers instead of + /// the original members. + /// + /// This runs after resolution so that it has access to ghostness + /// information, attributes and call targets and after verification + /// because that makes the interaction with the refinement transformer + /// more straightforward. /// - /// The module to generate wrappers for and in. - internal override void PostResolveIntermediate(ModuleDefinition moduleDefinition) { - // Keep a list of members to wrap so that we don't modify the collection we're iterating over. - List<(TopLevelDeclWithMembers, MemberDecl)> membersToWrap = new(); - - moduleDefinition.CallRedirector = new(Reporter); - - // Find module members to wrap. - foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType()) { - foreach (var decl in topLevelDecl.Members) { - if (ShouldGenerateWrapper(decl)) { - membersToWrap.Add((topLevelDecl, decl)); + /// The program to generate wrappers for and in. + public override void PostVerification(Program program) { + // Create wrappers + foreach (var moduleDefinition in program.Modules()) { + + // Keep a list of members to wrap so that we don't modify the collection we're iterating over. + List<(TopLevelDeclWithMembers, MemberDecl)> membersToWrap = new(); + + moduleDefinition.CallRedirector = new(Reporter); + + // Find module members to wrap. + foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType()) { + foreach (var decl in topLevelDecl.Members) { + if (ShouldGenerateWrapper(decl)) { + membersToWrap.Add((topLevelDecl, decl)); + } } } - } - // Generate a wrapper for each of the members identified above. - foreach (var (topLevelDecl, decl) in membersToWrap) { - GenerateWrapper(moduleDefinition, topLevelDecl, decl); - } - moduleDefinition.CallRedirector.NewRedirections = wrappedDeclarations; - } + // Generate a wrapper for each of the members identified above. This + // need to happen after all declarations to wrap have been identified + // because it adds new declarations and would invalidate the iterator + // used during identification. + foreach (var (topLevelDecl, decl) in membersToWrap) { + GenerateWrapper(moduleDefinition, topLevelDecl, decl); + } + moduleDefinition.CallRedirector.NewRedirections = wrappedDeclarations; - public override void PostVerification(Program program) { - foreach (var module in program.CompileModules) { - foreach (var topLevelDecl in module.TopLevelDecls.OfType()) { + // Put redirections in place. Any wrappers to call will be in either + // this module or to a previously-processed module, so they'll already + // exist. + foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType()) { foreach (var decl in topLevelDecl.Members) { if (decl is ICallable callable) { - module.CallRedirector?.Visit(callable, decl); + moduleDefinition.CallRedirector?.Visit(callable, decl); } } } @@ -264,7 +274,7 @@ public override void PostVerification(Program program) { return; } - foreach (var module in program.CompileModules) { + foreach (var module in program.Modules()) { if (module.CallRedirector == null) { continue; } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AbstractExtern1.cs b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AbstractExtern1.cs new file mode 100644 index 00000000000..c6d90d8e167 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AbstractExtern1.cs @@ -0,0 +1,10 @@ +using System.Numerics; + +namespace M { + + public partial class __default { + public static BigInteger ExternMethod() { + return new BigInteger(5); + } + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AbstractExtern2.cs b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AbstractExtern2.cs new file mode 100644 index 00000000000..efd74ded43c --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AbstractExtern2.cs @@ -0,0 +1,10 @@ +using System.Numerics; + +namespace M { + + public partial class __default { + public static BigInteger ExternMethod() { + return new BigInteger(-5); + } + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy index eeabf52dd95..b9d761d7589 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy @@ -1,4 +1,4 @@ -// RUN: ! %baredafny test %args --no-verify --unicode-char:false --test-assumptions=externs %s %s.externs.cs > %t +// RUN: ! %baredafny test %args --unicode-char:false --test-assumptions=externs %s %s.externs.cs > %t // RUN: %diff "%s.expect" "%t" // RUN: %OutputCheck --file-to-check "%S/AllExterns.cs" "%s" // CHECK: .*Foo____dafny__checked\(x\).* diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy.expect index 347491a3cca..0cf0890ae3d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy.expect @@ -1,7 +1,7 @@ + +Dafny program verifier finished with 0 verified, 0 errors CheckExtern.dfy(20,13): Warning: The requires clause at this location cannot be compiled to be tested at runtime because it references ghost state. CheckExtern.dfy(22,12): Warning: The ensures clause at this location cannot be compiled to be tested at runtime because it references ghost state. - -Dafny program verifier did not attempt verification FooTest: FAILED CheckExtern.dfy(3,12): Runtime failure of ensures clause from CheckExtern.dfy(3,12) BarTest: FAILED diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/RefineContract.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/RefineContract.dfy new file mode 100644 index 00000000000..499fdeab85e --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/RefineContract.dfy @@ -0,0 +1,14 @@ +// RUN: %run "%s" --input "%S/AbstractExtern1.cs" --test-assumptions Externs +// RUN: %exits-with 3 %run "%s" --input "%S/AbstractExtern2.cs" --test-assumptions Externs +abstract module A { + method {:extern "ExternMethod"} Method() returns (r: int) + ensures r > 0 +} + +module M refines A { +} + +method Main() { + var x := M.Method(); + print x, "\n"; +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy index 4cd380a97da..89863747538 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy @@ -1,4 +1,4 @@ -// RUN: ! %dafny /compile:4 /noVerify /runAllTests:1 /spillTargetCode:3 /testContracts:TestedExterns %s %s.externs.cs > %t +// RUN: ! %dafny /compile:4 /runAllTests:1 /spillTargetCode:3 /testContracts:TestedExterns %s %s.externs.cs > %t // RUN: %diff "%s.expect" "%t" // RUN: %OutputCheck --file-to-check "%S/TestedExterns.cs" "%s" // CHECK-NOT: .*Foo____dafny__checked\(x\).* diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy.expect index 489654892ad..3d25b4f5879 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy.expect @@ -1,7 +1,7 @@ + +Dafny program verifier finished with 0 verified, 0 errors CheckExtern.dfy(20,13): Warning: The requires clause at this location cannot be compiled to be tested at runtime because it references ghost state. CheckExtern.dfy(22,12): Warning: The ensures clause at this location cannot be compiled to be tested at runtime because it references ghost state. - -Dafny program verifier did not attempt verification TestedExterns.dfy(10,17): Warning: No :test code calls NotCalled FooTest: FAILED CheckExtern.dfy(3,12): Runtime failure of ensures clause from CheckExtern.dfy(3,12)