Fix extern contract checking on abstract modules #4910

atomb · 2023-12-20T21:49:46Z

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.

MikaelMayer

Sounds reasonable. Thanks for writing the tests.

Source/DafnyCore/Rewriters/ExpectContracts.cs

keyboardDrummer

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.

What is the problem caused by interleaving?

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.

Resolution caching is done on a per-module level. Any operation done in internal override void PostResolve(Program program) { is not cached, so we shouldn't have such methods unless they don't relate to a particular module, like RunAllTestsMainMethod which adds a single main method for the whole program.

atomb · 2023-12-21T16:24:53Z

Resolution caching is done on a per-module level. Any operation done in internal override void PostResolve(Program program) { is not cached, so we shouldn't have such methods unless they don't relate to a particular module, like RunAllTestsMainMethod which adds a single main method for the whole program.

It seems right to me that this shouldn't be cached as part of resolution. I'd consider it to essentially be part of the compiler, and not something that it would make sense to enable in the IDE, for example. It really is a whole-program transformation, in essence, because it introduces wrappers in one module that are then called (by redirection) from other modules.

@MikaelMayer

Apply suggestion from @MikaelMayer Co-authored-by: Mikaël Mayer <[email protected]>

atomb · 2023-12-21T16:37:01Z

What is the problem caused by interleaving?

The contract checking code creates a resolved wrapper in the abstract module, which is then copied, with resolution information removed, to the refining module, which hasn't yet been resolved. The removal of the resolution information causes the resolver to crash when checking the refining module. That, on its own, could perhaps be fixed in other ways. But even if it was, the contract checking code would then try to create that wrapper again after resolving the refining module. That could be fixed by adding a special case, but that would additionally complicate the code. By running after all modules are revolved, the approach can be straightforward, without complicating special cases that we could easily get wrong.

keyboardDrummer · 2023-12-22T10:52:27Z

It seems right to me that this shouldn't be cached as part of resolution. I'd consider it to essentially be part of the compiler, and not something that it would make sense to enable in the IDE, for example.

Fair, if you do it in internal override void PostResolve(Program program) though, it will be part of resolution and be run by the IDE.

It really is a whole-program transformation, in essence, because it introduces wrappers in one module that are then called (by redirection) from other modules.

In my experience the term whole-program analysis is used when the analysis of a definition (often a callee, but in this case an imported module) is affected by the usages (often the caller, but in this case an importing module), which I think is not the case here. Case in point: leaving out the refinement related bug, contract-wrapping is already working and it is done one module at a time.

It seems right to me that this shouldn't be cached as part of resolution. I'd consider it to essentially be part of the compiler

But it should be cached! Everything should be cached. We should design the whole compilation pipeline (by compilation pipeline I mean everything from parsing to code generation) with caching in mind. I'll admit that caching is less important for code generation, but I would still argue that it is better if it is designed so that it could be cached. If code generation can be done for modules independently, then it could also be run in parallel.

No need to take action for this now though.

The contract checking code creates a resolved wrapper in the abstract module, which is then copied, with resolution information removed, to the refining module, which hasn't yet been resolved. The removal of the resolution information causes the resolver to crash when checking the refining module. That, on its own, could perhaps be fixed in other ways.

Seems like a general bug not tied to contract-checking

But even if it was, the contract checking code would then try to create that wrapper again after resolving the refining module. That could be fixed by adding a special case, but that would additionally complicate the code. By running after all modules are revolved, the approach can be straightforward, without complicating special cases that we could easily get wrong.

Refinement modules in general collide with meta-programming transformations. Attributes such as {:autocontracts} and {:autoReq} have a similar problem.

They contains code such as

if (member.RefinementBase != null) {
  // member is inherited from a module where it was already processed
  continue;
}

to deal with this.

That said, those contracts need to be part of refinement, and contract wrapping does not. I think it is indeed easier to do the wrapping transformation after all refinement is done. Could you move the transformation to the compilers/code-generators? It seems there's already a handle void PostVerification(Program program) that allows this.

atomb · 2023-12-22T16:13:13Z

It seems right to me that this shouldn't be cached as part of resolution. I'd consider it to essentially be part of the compiler, and not something that it would make sense to enable in the IDE, for example.

Fair, if you do it in internal override void PostResolve(Program program) though, it will be part of resolution and be run by the IDE.

But it won't do anything unless the option is enabled, which only makes sense when you're compiling.

It really is a whole-program transformation, in essence, because it introduces wrappers in one module that are then called (by redirection) from other modules.

In my experience the term whole-program analysis is used when the analysis of a definition (often a callee, but in this case an imported module) is affected by the usages (often the caller, but in this case an importing module), which I think is not the case here. Case in point: leaving out the refinement related bug, contract-wrapping is already working and it is done one module at a time.

It processes one module at a time, but it generates calls that go between modules and need to be consistent between them.

That said, those contracts need to be part of refinement, and contract wrapping does not. I think it is indeed easier to do the wrapping transformation after all refinement is done. Could you move the transformation to the compilers/code-generators? It seems there's already a handle void PostVerification(Program program) that allows this.

That seems reasonable. Part of the process already happens in PostVerification(Program), and the rest could be moved. I think the fact that it's separate is, IIRC, an artifact of the fact that it used to run pre-resolution in an attempt to have resolution help detect cases where we generate badly-structured code. But we already had to move it after resolution to get ghostness information, so that's no longer a consideration.

When it comes to finishing this PR, is moving the code to all run in PostVerification the one change you'd concretely like to see in place?

keyboardDrummer · 2023-12-23T20:11:24Z

But it won't do anything unless the option is enabled, which only makes sense when you're compiling.

I see. That helps but I'd rather not depend on that.

When it comes to finishing this PR, is moving the code to all run in PostVerification the one change you'd concretely like to see in place?

Yes

atomb · 2024-01-02T23:41:42Z

When it comes to finishing this PR, is moving the code to all run in PostVerification the one change you'd concretely like to see in place?

Yes

Got it. The latest commit makes that change. Let me know what you think.

keyboardDrummer · 2024-01-03T10:01:56Z

Source/DafnyCore/Rewriters/ExpectContracts.cs

+ /// the original members.
+ ///
+ /// This runs after resolution so that it has access to ghostness
+ /// information, attributes and call targets. It runs on the entire


The sentence 'it runs on the entire program' doesn't make sense to me.

I think this is a transformation where modules are only affected by modules they import, but not the other way around, so you can do it module by module, which the existing loops indicate. I think you can also cache the results of processing a module, even though we don't need to do that now.

I guess that comment isn't as relevant as it was before. When running after resolution, there are two possible methods to override, and this was an explanation for why the code overrides the Program version instead of the Module version. After verification, there's only one option, though.

keyboardDrummer · 2024-01-03T10:03:28Z

Source/DafnyCore/Rewriters/ExpectContracts.cs

- if (ShouldGenerateWrapper(decl)) {
- membersToWrap.Add((topLevelDecl, decl));
+ /// <param name="program">The program to generate wrappers for and in.</param>
+ public override void PostVerification(Program program) {


Should

if (Reporter.Options.TestContracts != DafnyOptions.ContractTestingMode.TestedExterns) { return; }

on line 270, be moved to the top of the method?

No. The first two loops should run regardless of that option.

keyboardDrummer · 2024-01-03T10:03:30Z

Source/DafnyCore/Rewriters/ExpectContracts.cs

+ /// <param name="program">The program to generate wrappers for and in.</param>
+ public override void PostVerification(Program program) {
+ // Create wrappers
+ foreach (var moduleDefinition in program.Modules()) {


Sometimes I see program.CompileModules being used and sometimes program.Modules(). Is this difference intentional? They're very similar but one also includes the system module.

Ah, good catch. I think they should all be program.Modules().

keyboardDrummer · 2024-01-03T10:03:59Z

Source/DafnyCore/Rewriters/ExpectContracts.cs

- if (ShouldGenerateWrapper(decl)) {
- membersToWrap.Add((topLevelDecl, decl));
+ /// <param name="program">The program to generate wrappers for and in.</param>
+ public override void PostVerification(Program program) {


There are three loops in this method that all iterate over modules. Can they be merged into one loop?

Not without more complex logic that would be easy to get wrong. It needs to ensure that wrappers exist before they're called. The most straightforward way to do that is to construct them all before redirecting calls.

But the modules returned by .Modules() are already sorted in topological order of the import graph. How would having a single loop be able to get the order wrong?

You can't call a wrapper from a module unless you imported that module, and the imported module has already been processed so its wrappers exist.

Ah, right! I hadn't realized it was already sorted. So, yes, the first two loops can be merged. I'll do that.

The final loop is checking for whether any extern exists that hasn't been called by a test, and a test could always show up in a later module in the dependency chain, so I think it still needs to run last.

Sounds good

Fix dafny-lang#4845

9f768f9

atomb requested a review from keyboardDrummer December 20, 2023 21:49

atomb self-assigned this Dec 20, 2023

atomb enabled auto-merge (squash) December 20, 2023 22:17

Merge branch 'master' into fix-issue-4845

6eb8549

atomb requested review from fabiomadge and MikaelMayer December 20, 2023 22:21

MikaelMayer reviewed Dec 21, 2023

View reviewed changes

Source/DafnyCore/Rewriters/ExpectContracts.cs Outdated Show resolved Hide resolved

keyboardDrummer requested changes Dec 21, 2023

View reviewed changes

Update Source/DafnyCore/Rewriters/ExpectContracts.cs

c2e0a9e

Apply suggestion from @MikaelMayer Co-authored-by: Mikaël Mayer <[email protected]>

atomb added 2 commits January 2, 2024 15:22

Merge remote-tracking branch 'upstream/master' into fix-issue-4845

b7980c1

Move all of ExpectContracts into PostVerification

babae0d

keyboardDrummer reviewed Jan 3, 2024

View reviewed changes

keyboardDrummer disabled auto-merge January 3, 2024 10:05

keyboardDrummer reviewed Jan 3, 2024

View reviewed changes

atomb added 4 commits January 3, 2024 08:29

Use Modules() instead of CompileModules

2a33ec6

Improve comments

3ce2b80

Merge remote-tracking branch 'upstream/master' into fix-issue-4845

6d207a4

Merge two loops

a70b1f7

atomb enabled auto-merge (squash) January 3, 2024 17:16

Merge branch 'master' into fix-issue-4845

b9ae7d9

atomb requested a review from keyboardDrummer January 3, 2024 23:32

keyboardDrummer approved these changes Jan 4, 2024

View reviewed changes

Merge branch 'master' into fix-issue-4845

76bdff9

atomb merged commit ab22a7d into dafny-lang:master Jan 4, 2024
20 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix extern contract checking on abstract modules #4910

Fix extern contract checking on abstract modules #4910

atomb commented Dec 20, 2023

MikaelMayer left a comment

keyboardDrummer left a comment •

edited

Loading

atomb commented Dec 21, 2023

atomb commented Dec 21, 2023

keyboardDrummer commented Dec 22, 2023 •

edited

Loading

atomb commented Dec 22, 2023

keyboardDrummer commented Dec 23, 2023

atomb commented Jan 2, 2024

keyboardDrummer Jan 3, 2024 •

edited

Loading

atomb Jan 3, 2024

keyboardDrummer Jan 3, 2024

atomb Jan 3, 2024

keyboardDrummer Jan 3, 2024

keyboardDrummer Jan 3, 2024

atomb Jan 3, 2024

keyboardDrummer Jan 3, 2024

atomb Jan 3, 2024

keyboardDrummer Jan 3, 2024 •

edited

Loading

atomb Jan 3, 2024

keyboardDrummer Jan 3, 2024

Fix extern contract checking on abstract modules #4910

Fix extern contract checking on abstract modules #4910

Conversation

atomb commented Dec 20, 2023

Description

How has this been tested?

MikaelMayer left a comment

Choose a reason for hiding this comment

keyboardDrummer left a comment • edited Loading

Choose a reason for hiding this comment

atomb commented Dec 21, 2023

atomb commented Dec 21, 2023

keyboardDrummer commented Dec 22, 2023 • edited Loading

atomb commented Dec 22, 2023

keyboardDrummer commented Dec 23, 2023

atomb commented Jan 2, 2024

keyboardDrummer Jan 3, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Jan 3, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer left a comment •

edited

Loading

keyboardDrummer commented Dec 22, 2023 •

edited

Loading

keyboardDrummer Jan 3, 2024 •

edited

Loading

keyboardDrummer Jan 3, 2024 •

edited

Loading