Add replaceable modules #4681

keyboardDrummer · 2023-10-18T16:43:32Z

Description

Move some C# code from Dafny.atg and Parser.frame to a new file named ParserNonGeneratedPart.cs, so C# IDEs can provide tooling for this code.
Enable the following syntax

replaceable module FooModule {
  method Foo() returns (i: int) 
    ensures i >= 2
}

module Nesting {
  module ConcreteFoo replaces FooModule {
    method Foo() returns (i: int) {
      return 3;
    }
  }
}

method Main() {
  var x := FooModule.Foo();
  print x; // Prints 3
}

Check out one the test-cases for an example of how you define a multi-target application using this feature: https://github.com/dafny-lang/dafny/blob/66c1b1ee414bb4a5060507dbb0dd333697968e02/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/placeholders/complex/user.dfy

Caveats

Refining the replaceable module is not supported, and it will not be supported for some time. There's a conflict between how refinement works and how replaceable modules work.

Replaceable modules are implemented as a post-resolution feature. It swaps out references to the replaceable with the replacement. It has to work like this because dafny verify should work without the replacement being part of the source, so refinement can not rely on the replacement module being present.

Refinement, as it is currently implemented, copies non-abstract parts of the refinee into the refiner during resolution, so you would need access to the replacement module during resolution, if you want to further refine it.

We could change refinement so it does use the replacement module if its available, to influence refinement, but I consider that detrimental to maintainability so I think we should not do this. Refinement being implemented using copying is already problematic because it increases compilation time and generated code size. I think we should change refinement so it uses references to the refinee's members instead of copying them, and then we can also implement refinement of placeholders.

How has this been tested?

Add a happy flow test containing:
- A placeholder module that is replaced
- A placeholder module that refines an abstract module, and is replaced
- A placeholder module that replaces another placeholder module, and is replaced
- Various abstract imports using placeholders
Add complex tests that use different back-ends for a common library, showing off the main driver behind the feature.
Add a test that exposes all added errors
- A placeholder module can not be refined
- A placeholder module was not replaced
- A placeholder module was replaced more than once
- Cycle of replacement

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

…atedPart.cs

…into placeholderModule

robin-aws

Loving this feature, and I'm getting pretty comfortable with the terminology/syntax, although I want to give other core maintainers the chance to object.

Just reviewed the feature design and tests/documentation for now, can circle back to review the actual implementation.

robin-aws · 2023-10-19T21:32:29Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/placeholders/complex/wrappers.dfy

+The module also defines two forms of `Need`, that check the truth of a predicate and
+return a failure value if false.
+ */
+module DafnyStdLibs.Wrappers {


A bit silly I'd admit, but we should probably stop adding copies of Wrappers all over the place in the integration tests since #4678 will add an official copy, and having decoys will make searching for the real one annoying. :)

Totally, but your PR isn't merged yet ! I planned on removing this later.

Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs

robin-aws · 2023-10-19T22:42:21Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/placeholders/complex/user.dfy

+ var areEqual := x == y;
+ print "areEqual: ", areEqual;


This is a good case for using expect instead of printing and comparing, I think.

Also I don't love the idea of a test that by design could non-deterministically fail, no matter how small the probability. :) How about expect 0 <= x < 1000000 instead?

Also I don't love the idea of a test that by design could non-deterministically fail

I changed the chance to 10^-30, so it won't fail before our planet disintegrates

This is a good case for using expect instead of printing and comparing, I think.

Not sure what the advantage is, but sure !

...tionTests/TestFiles/LitTests/LitTest/comp/placeholders/placeholderExecutionErrors.dfy.expect

robin-aws · 2023-10-19T22:48:31Z

docs/DafnyRef/UserGuide.md

@@ -1727,7 +1727,31 @@ Detailed description of the `dafny build` and `dafny run` commands and
 the `--input` option (needed when `dafny run` has more than one input file)
 is contained [in the section on command-line structure](#command-line).

-### 13.7.2. C\#
+### 13.7.2. Placeholder modules
+To allow defining behavior that depending on which target language Dafny is translated to, requires different Dafny code to be implemented, Dafny has placeholder modules. Here follows an example:


nit: I'd like to tweak this a little to describe the abstract feature first, then the primary motivation. Something like like "To support customizing behavior differently at compile-time for different contexts, Dafny has placeholder modules... This is particularly useful for defining behavior that depends on which target language Dafny is translated to".

I really like that the feature is generic enough to apply to other use cases so let's not sell it short!

In fact I'd promote at least most of this section to the reference manual since it is in fact a language feature, not just a tool feature.

In fact I'd promote at least most of this section to the reference manual since it is in fact a language feature, not just a tool feature.

Not sure where to put it then, there is no "runtime behavior" section, and I think this is a pretty good spot for now.

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/placeholders/placeholderHappyflow.dfy

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/placeholders/complex/randomJava.dfy

robin-aws · 2023-10-19T22:55:54Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/placeholders/complex/user.dfy

+// RUN: %baredafny run %args %s --target=java --build=%S/Build/build --input %S/wrappers.dfy --input %S/random.dfy --input %S/randomJava.dfy --input %S/Interop/__default.java --spill-target-code > "%t"
+// RUN: %baredafny run %args %s --build=%S/Build/build --input %S/wrappers.dfy --input %S/random.dfy --input %S/randomCSharp.dfy --input %S/Interop.cs --spill-target-code >> "%t"


You can definitely see how nice it would be to have the project file specify all this, and even better to have a default convention for the code layout of a Dafny project with extern code. :)

MikaelMayer

Looks great! A few tweaks but otherwise the documentation is good, the tests are good (I would like to see at least one test where the replaceable module is already 100% defined by itself, whatever semantics you think you'd choose)

Source/DafnyCore/AST/Modules/ModuleDefinition.cs

Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs

Source/DafnyCore/Compilers/ExecutableBackend.cs

Source/DafnyCore/Rewriters/RefinementTransformer.cs

...ntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/Inputs/randomCSharp.dfy

MikaelMayer · 2023-11-15T18:03:26Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/user.dfy

+ y := DfyRandom.GetRandomNat(1000000);
+ i := i - 1;
+ }
+ expect x != y;


Suggested change

expect x != y;

expect i == 0 || x != y;

I hope you don't mind too much but I'd feel better for maintenance if the expect was always true :-)

but then it doesn't test the randomness, and in any practical sense it already was always true. Anyways, made the change.

hmmm. Ok. In that case, can you mark Main as decreases * and that way you can also mark the loop as decreases *. Then you are truly testing for randomness, but now it's no longer a probability on the test failing or not, it's how long it will take.

docs/DafnyRef/UserGuide.md

docs/dev/news/4681.feat

…4790) ### Description Adds build support for standard libraries with different Dafny and target language source code per backend, and imports the `FileIO` library. The build support mainly adds a set of `DafnyStandardLibraries-<target>.doo` files, and a common `DafnyStandardLibraries-notarget.doo` file with only the abstract interface. The pattern looks a lot like [replaceable modules](#4681), but is less efficient for now because it re-verifies common code rather than relying on refinement. Please pay particular attention to the documentation updates as this does slightly affect the user experience with standard libraries! Major changes to `FileIO` on the way in: * Refactored to separate the externs into its own module, so it could be defined differently per backend without duplicating the common wrapper logic. * Added support for Go and Javascript. * Removed the comments about additional source files in the `README.md` since it's all automatic now (yay!) Other supporting changes: * Fixes #4782, as otherwise Go was messy to implement and Python nearly impossible. * Added utilities in the Go runtime for converting between `_dafny.Sequence` and `[]byte`. * Added an automatic build of Dafny itself at the end of `make update-binary`, since failing to do that and therefore not picking up the new versions of the `.doo` files was a common gotcha. * Switched CI job that tests the standard libraries from Ubuntu to Mac OS: diffing checked in `.doo` files against fresh builds of them was failing for what looks like whitespace/newline variation. It makes more sense to stick to Mac OS for verification of production Dafny code anyway, however, since most contributors are developing on macs and [verification is not guaranteed to be consistent across platforms](#1807). ### How has this been tested? `StandardLibraries_TargetSpecific.dfy` for the general support, `FileIOExamples.dfy` for `FileIO` itself (mainly the same as the original library, adapted as Dafny tests instead of lit tests) --------- Co-authored-by: Alex Chew <alex-chew@users.noreply.github.com>

MikaelMayer

Good for me. Thanks.

MikaelMayer · 2023-11-20T12:03:07Z

Source/DafnyCore/Compilers/ExecutableBackend.cs

@@ -30,10 +30,36 @@ public abstract class ExecutableBackend : IExecutableBackend {
 public override string ModuleSeparator => Compiler.ModuleSeparator;

 public override void Compile(Program dafnyProgram, ConcreteSyntaxTree output) {
+ InstantiatePlaceholders(dafnyProgram);


Suggested change

InstantiatePlaceholders(dafnyProgram);

InstantiateReplaceableModules(dafnyProgram);

One name per concept makes the code easier to read

…into placeholderModule

…just already did a regular build

stefan-aws

Previously approved. Small changes since.

other reviewers got a chance to object

keyboardDrummer added 23 commits October 18, 2023 16:12

Move some code out of Dafny.atg and Parser.frame, into ParserNonGener…

2c9f144

…atedPart.cs

Introduce placeholder modifier, as alternative to abstract

510c2ef

Add InstantiatingModule field and use it to customize GetCompileName

d99bb3d

Introduce instantiates keyword

2d580bd

Instantiating placeholder modules

4cbf9d6

Add placeholder/instantiate test and run formatter

1f1fb5b

Merge remote-tracking branch 'origin/master' into placeholderModule

e804d11

Use replaces instead of instantiates

9e1b62e

Fix compilation errors

53ac4c6

Fix big bug

aad3ecf

Add complex test

f258127

Update complex C# test and start Java one

ed1c41b

Java complex test works now

93b50d2

Clean up C# complex test

f54567a

Add comment

c557c60

Add error are tested

f9e7ec2

More testing

f26e934

Add abstract import to happy flow test

af0bf1f

Various printing fixes

eac3cf5

Merge branch 'master' into placeholderModule

9af3ca1

Add some documentation

c231454

Add release note

c41c0bd

Merge branch 'placeholderModule' of github.com:keyboardDrummer/dafny …

66c1b1e

…into placeholderModule

keyboardDrummer requested review from robin-aws, RustanLeino and MikaelMayer October 19, 2023 21:19

keyboardDrummer added 3 commits October 19, 2023 23:25

Reduce chance of collision

2fbda30

Remove bad comment

7c833e3

Simplify test

8e84ac7

robin-aws previously requested changes Oct 19, 2023

View reviewed changes

keyboardDrummer dismissed RustanLeino’s stale review via 3bd86a8 October 27, 2023 11:09

Replace remaining occurrences of placeholder with replaceable

4229dcd

keyboardDrummer force-pushed the placeholderModule branch from 3bd86a8 to 4229dcd Compare October 27, 2023 12:21

Merge branch 'master' into placeholderModule

e3a2011

keyboardDrummer changed the title ~~Add placeholder modules~~ Add replaceable modules Nov 10, 2023

MikaelMayer reviewed Nov 15, 2023

View reviewed changes

robin-aws mentioned this pull request Nov 16, 2023

feat: Per-backend code support in standard libraries, FileIO library #4790

Merged

keyboardDrummer added 2 commits November 17, 2023 13:23

Tweaks

0aced1e

Merge remote-tracking branch 'origin/master' into placeholderModule

04cac67

keyboardDrummer enabled auto-merge (squash) November 17, 2023 12:28

keyboardDrummer requested a review from MikaelMayer November 17, 2023 12:28

Remove ending dot

a160d2d

MikaelMayer previously approved these changes Nov 17, 2023

View reviewed changes

Fix comp error

85fbd9c

keyboardDrummer dismissed MikaelMayer’s stale review via 85fbd9c November 17, 2023 18:39

keyboardDrummer requested a review from MikaelMayer November 17, 2023 18:39

keyboardDrummer added 3 commits November 17, 2023 22:01

Fix expect file

7bd1fb9

Fix rust compiler replaceable and outer-module feature

ee8593f

Merge branch 'master' into placeholderModule

a3d6573

MikaelMayer reviewed Nov 20, 2023

View reviewed changes

keyboardDrummer added 5 commits November 20, 2023 15:07

Fix errors

b7a8186

Merge branch 'placeholderModule' of github.com:keyboardDrummer/dafny …

e8f117d

…into placeholderModule

Remove --no-build that for some reason fails the pack even though we …

5228048

…just already did a regular build

Merge branch 'master' into placeholderModule

2e8d8ff

Merge branch 'master' into placeholderModule

7681a65

stefan-aws approved these changes Nov 21, 2023

View reviewed changes

keyboardDrummer merged commit fd75d96 into dafny-lang:master Nov 21, 2023
20 checks passed

keyboardDrummer mentioned this pull request Feb 5, 2024

Feature request: support implementing a Dafny abstraction differently for different backends #4640

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add replaceable modules #4681

Add replaceable modules #4681

keyboardDrummer commented Oct 18, 2023 •

edited

Loading

robin-aws left a comment

robin-aws Oct 19, 2023

keyboardDrummer Oct 20, 2023

robin-aws Oct 19, 2023

keyboardDrummer Oct 20, 2023 •

edited

Loading

keyboardDrummer Oct 20, 2023

robin-aws Oct 19, 2023

robin-aws Oct 19, 2023

keyboardDrummer Oct 20, 2023

robin-aws Oct 19, 2023

MikaelMayer left a comment

MikaelMayer Nov 15, 2023

keyboardDrummer Nov 17, 2023 •

edited

Loading

MikaelMayer Nov 17, 2023

MikaelMayer left a comment

MikaelMayer Nov 20, 2023

stefan-aws left a comment

		// RUN: %baredafny run %args %s --target=java --build=%S/Build/build --input %S/wrappers.dfy --input %S/random.dfy --input %S/randomJava.dfy --input %S/Interop/__default.java --spill-target-code > "%t"
		// RUN: %baredafny run %args %s --build=%S/Build/build --input %S/wrappers.dfy --input %S/random.dfy --input %S/randomCSharp.dfy --input %S/Interop.cs --spill-target-code >> "%t"

	InstantiatePlaceholders(dafnyProgram);
	InstantiateReplaceableModules(dafnyProgram);

Add replaceable modules #4681

Add replaceable modules #4681

Conversation

keyboardDrummer commented Oct 18, 2023 • edited Loading

Description

Caveats

How has this been tested?

robin-aws left a 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 Oct 20, 2023 • 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

MikaelMayer left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Nov 17, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MikaelMayer left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

stefan-aws left a comment

Choose a reason for hiding this comment

keyboardDrummer commented Oct 18, 2023 •

edited

Loading

keyboardDrummer Oct 20, 2023 •

edited

Loading

keyboardDrummer Nov 17, 2023 •

edited

Loading