feat: add type descriptors for data constructors in Java, when necessary #301

robin-aws · 2023-10-20T20:47:15Z

Description of changes:
As part of the progress towards supporting traits on non-reference types, the Java backend in Dafny 4.2 changed datatype constructors to require type descriptors for any generic type parameters: dafny-lang/dafny#4240.

This change fixes a big chunk of the failing nightly build failures by augmenting the Java code generation to conditionally provide these type descriptors when creating Result and Option values. In most cases this is handled by the new nameresolver.Dafny.createSuccess/Failure/Some/None helper methods, but in some cases some new Dafny helper methods are added to StandardLibrary or emitted as well, so that TestModels can provide the same Java code for any Dafny version.

It also adds a parameter for the target Dafny version so it knows when to emit them, exposed both as a --dafny-version option for the CLI and a dafnyVersion configuration value on smithy-build.json file. This defaults to 4.1.0, but the latter knob is actually required when using the latest "edition" of the Smithy plugin (now 2023.10 instead of 2023), as this is exactly the kind of otherwise-breaking change editions are designed to support!

Finally, it refactors the CI to test all Dafny-relevant things on multiple versions of Dafny. It follows the same workflow template as https://github.com/aws/aws-cryptographic-material-providers-library-java/tree/main/.github/workflows (and kudos to @texastony!). This exposed one verification regression on 4.3 that I'm looking into, and may factor out of this PR if it's not quick to fix. ~~Note the nightly build depends on a pending patch to setup-dafny-action to provide the actual version when using nightly-latest: dafny-lang/setup-dafny-action#19~~

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

…awslabs/polymorph into robin-aws/add-type-descriptors-for-java

…module

seebees · 2023-11-22T17:07:15Z

TestModels/dafny-dependencies/StandardLibrary/src/WrappersInterop.dfy

+
+  class WrappersInterop {
+
+    static function method CreateStringSome(s: string): Option<string> {


Generics? CreateSome<T>(t: T): Option<T>?

Unfortunately no, but I beefed up the module comment to explain why better.

seebees · 2023-11-22T17:20:57Z

...mithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java

            "ensures res.Success? ==> ",
            "&& fresh(res.value)",
            "&& fresh(res.value.%s)".formatted(nameResolver.mutableStateFunctionName()),
            "&& fresh(res.value.%s)".formatted(nameResolver.callHistoryFieldName()),
            "&& res.value.%s()".formatted(nameResolver.validStateInvariantName())
          ).lineSeparated();

+        final TokenTree createSuccessOfClient = TokenTree


I'm a little confused about where this is getting emitted.
On the one hand, I see additions in the "StandardLibrary" but I also see this getting written here?

Similarly added more comments to explain better.

…awslabs/polymorph into robin-aws/add-type-descriptors-for-java

Potentially radically different from when I blocked.

texastony

Java docs on new public methods is the only blocking comment.

texastony · 2023-11-27T20:49:31Z

.github/workflows/pull.yml

+          4.1.0,
+          4.3.0


Note: I am still learning how to best utilize GHA/Ws,
and it seems that GitHub is evolving them as well.

And our test models need to be refactored to an integration test project...

texastony · 2023-11-27T20:50:35Z

.github/workflows/pull.yml

+        dafny-version: [
+          4.1.0,
+          4.3.0
+        ]


Nit: Is there no way to declare this once and reference it elsewhere in this file?

Definitely possible but not nearly as simple as you'd think :) I made the change as I already had to do something similar for Dafny (where we needed a lot more dynamic calculation)

...mithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java

...n/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyVersion.java

...dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Constants.java

...thy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Dafny.java

texastony · 2023-11-27T21:26:19Z

...thy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Dafny.java

+    public CodeBlock createNone(CodeBlock typeDescriptor) {
+        if (datatypeConstructorsNeedTypeDescriptors()) {
+            return CodeBlock.of(
+                    "$T.create_None($L)",
+                    ClassName.get("Wrappers_Compile", "Option"),
+                    typeDescriptor);
+        } else {
+            return CodeBlock.of(
+                    "$T.create_None()",
+                    ClassName.get("Wrappers_Compile", "Option"));
+        }
+    }
+
+    public CodeBlock createSome(CodeBlock typeDescriptor, CodeBlock value) {
+        if (datatypeConstructorsNeedTypeDescriptors()) {
+            return CodeBlock.of(
+                    "$T.create_Some($L, $L)",
+                    Constants.DAFNY_OPTION_CLASS_NAME,
+                    typeDescriptor,
+                    value);
+        } else {
+            return CodeBlock.of(
+                    "$T.create_Some($L)",
+                    Constants.DAFNY_OPTION_CLASS_NAME,
+                    value);
+        }
+    }
+
+    public CodeBlock createSuccess(CodeBlock valueTypeDescriptor, CodeBlock value) {
+        if (datatypeConstructorsNeedTypeDescriptors()) {
+            return CodeBlock.of(
+                    "$T.create_Success($L, Error._typeDescriptor(), $L)",
+                    Constants.DAFNY_RESULT_CLASS_NAME,
+                    valueTypeDescriptor,
+                    value);
+        } else {
+            return CodeBlock.of(
+                    "$T.create_Success($L)",
+                    Constants.DAFNY_RESULT_CLASS_NAME,
+                    value);
+        }
+    }
+
+    public CodeBlock createFailure(CodeBlock typeDescriptor, CodeBlock error) {
+        if (datatypeConstructorsNeedTypeDescriptors()) {
+            return CodeBlock.of(
+                    "$T.create_Failure($L, Error._typeDescriptor(), $L)",
+                    Constants.DAFNY_RESULT_CLASS_NAME,
+                    typeDescriptor,
+                    error);
+        } else {
+            return CodeBlock.of(
+                    "$T.create_Failure($L)",
+                    Constants.DAFNY_RESULT_CLASS_NAME,
+                    error);
+        }
+    }
+


Blocking: Add Java docs.
Smithy-Dafny is a wildly confusing project with many hands contributing functionality.
We MUST describe what our methods do.

I checked, its true, all of these method names are unique.
But they are barely unique.

We need to java docs so future us know when to invoke this these methods.

...thy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Dafny.java

Co-authored-by: Tony Knapp <[email protected]>

.github/workflows/pull.yml

This is necessary for Dafny 4.3 and higher, as Dafny no longer adds this method on reference types. The explicit construction of the right kind of TypeDescriptor (which works both before and after 4.3) was already implemented for other shapes in typeDescriptor(ShapeId), so I just tweaked the case identification, and scoped the default case more explicitly to shapes we know it works for, and now raise an exception for unrecognized shape types. Unfortunately not covered by any TestModels (which is why #301 didn't fix this as well), but tested on MPL: aws/aws-cryptographic-material-providers-library#195

#195) Applies several fixes/improvements in order to work with newer Dafny versions. * Adds `smithy-dafny` as a submodule so that we can lock down the exact commit used to generate code, and use the tool in CI. * Updates the shared makefile with similar improvements to smithy-dafny's (hook up `--library-root` and `--patch-files-dir`, generate dependencies first) * Regenerates the checked-in code using a newer `smithy-dafny` to abstract away from the changes in Java TypeDescriptors when constructing datatypes in Dafny 4.3. This includes adding some helper methods to Dafny code for the benefit of Java external code, in the same style as smithy-lang/smithy-dafny#301 did. * Also updated various `__default` classes to use the above to avoid constructing Dafny datatypes directly. * Regenerating means that the effect of smithy-lang/smithy-dafny#311 on C# code shows up too. * Introduced `InternalResult<T, R>` to replace some internal-only uses of Dafny's compiled `Result` type, to avoid even more Dafny helper methods. * Leverage the `smithy-dafny` `<library-root>/codegen-patches[/<service>]` feature to extract out manual patch files. * This allows building with a newer version of Dafny to work despite having to regenerate code differently, in some cases by providing different patch files for different version ranges. * Cheated slightly by using this to conditionally remove an instance of `{:vcs_split_on_every_assert}` on `AwsKmsKeyring.OnDecrypt'` that is necessary on Dafny 4.2 but makes things work on Dafny 4.4 (which was not the intention of the patching feature, but also solves this problem much more cheaply than having to refactor the code to work in both versions :) * Add regenerating code to CI, either to verify that it matches what's checked in, or to pick up the necessary changes to work with newer Dafny versions. Manually verified the CI passes on the source branch with the latest Dafny nightly prerelease: https://github.com/aws/aws-cryptographic-material-providers-library/actions/runs/8039889665 Note that CI will now reject making further manual edits to generated files without capturing those edits in patch files. The error message will suggest how to update the patch files accordingly. See also https://github.com/smithy-lang/smithy-dafny/tree/main-1.x/TestModels/CodegenPatches

…crete class) (#331) *Description of changes:* Reverts the part of #301 that changed the result type of constructing services from the concrete class type to the trait type, which turned out to be breaking in .NET as well as Dafny and was manually reverted in aws/aws-cryptographic-material-providers-library#257. See aws/aws-cryptographic-material-providers-library#267 for the upcoming proper fix to the MPL using this change. As it turns out this change wasn't necessary in the first place, and the `CreateSuccessOfClient/CreateFailureOfError` helpers are unchanged and still use the trait type, because these helpers are only needed for services that are created by target language code, i.e. SDK-style services and `--local-service-test` wrapped services. Regular local services are constructed in Dafny code so they never need the helper methods.

@texastony

…ary (smithy-lang#301) *Description of changes:* As part of the progress towards supporting traits on non-reference types, the Java backend in Dafny 4.2 changed datatype constructors to require type descriptors for any generic type parameters: dafny-lang/dafny#4240. This change fixes a big chunk of the failing nightly build failures by augmenting the Java code generation to conditionally provide these type descriptors when creating `Result` and `Option` values. In most cases this is handled by the new `nameresolver.Dafny.createSuccess/Failure/Some/None` helper methods, but in some cases some new Dafny helper methods are added to `StandardLibrary` or emitted as well, so that TestModels can provide the same Java code for any Dafny version. It also adds a parameter for the target Dafny version so it knows when to emit them, exposed both as a `--dafny-version` option for the CLI and a `dafnyVersion` configuration value on `smithy-build.json` file. This defaults to `4.1.0`, but the latter knob is actually required when using the latest "edition" of the Smithy plugin (now `2023.10` instead of `2023`), as this is exactly the kind of otherwise-breaking change editions are designed to support! Finally, it refactors the CI to test all Dafny-relevant things on multiple versions of Dafny. It follows the same workflow template as https://github.com/aws/aws-cryptographic-material-providers-library-java/tree/main/.github/workflows (and kudos to @texastony!). This exposed one verification regression on 4.3 that I'm looking into, and may factor out of this PR if it's not quick to fix. --------- Co-authored-by: Tony Knapp <[email protected]>

#195) Applies several fixes/improvements in order to work with newer Dafny versions. * Adds `smithy-dafny` as a submodule so that we can lock down the exact commit used to generate code, and use the tool in CI. * Updates the shared makefile with similar improvements to smithy-dafny's (hook up `--library-root` and `--patch-files-dir`, generate dependencies first) * Regenerates the checked-in code using a newer `smithy-dafny` to abstract away from the changes in Java TypeDescriptors when constructing datatypes in Dafny 4.3. This includes adding some helper methods to Dafny code for the benefit of Java external code, in the same style as smithy-lang/smithy-dafny#301 did. * Also updated various `__default` classes to use the above to avoid constructing Dafny datatypes directly. * Regenerating means that the effect of smithy-lang/smithy-dafny#311 on C# code shows up too. * Introduced `InternalResult<T, R>` to replace some internal-only uses of Dafny's compiled `Result` type, to avoid even more Dafny helper methods. * Leverage the `smithy-dafny` `<library-root>/codegen-patches[/<service>]` feature to extract out manual patch files. * This allows building with a newer version of Dafny to work despite having to regenerate code differently, in some cases by providing different patch files for different version ranges. * Cheated slightly by using this to conditionally remove an instance of `{:vcs_split_on_every_assert}` on `AwsKmsKeyring.OnDecrypt'` that is necessary on Dafny 4.2 but makes things work on Dafny 4.4 (which was not the intention of the patching feature, but also solves this problem much more cheaply than having to refactor the code to work in both versions :) * Add regenerating code to CI, either to verify that it matches what's checked in, or to pick up the necessary changes to work with newer Dafny versions. Manually verified the CI passes on the source branch with the latest Dafny nightly prerelease: https://github.com/aws/aws-cryptographic-material-providers-library/actions/runs/8039889665 Note that CI will now reject making further manual edits to generated files without capturing those edits in patch files. The error message will suggest how to update the patch files accordingly. See also https://github.com/smithy-lang/smithy-dafny/tree/main-1.x/TestModels/CodegenPatches

robin-aws added 8 commits October 20, 2023 13:35

Fix UTF8

461dd3d

Temporarily try CI on 4.3

c31cee8

Merge branch 'main-1.x' into robin-aws/add-type-descriptors-for-java

45ee695

Get Resource test model working

478c043

Merge branch 'robin-aws/add-type-descriptors-for-java' of github.com:…

8f40bb7

…awslabs/polymorph into robin-aws/add-type-descriptors-for-java

Handle aggregate type descriptors in general

fe5f975

Fix KMS

ea48656

Fix a few more model tests

6ba962d

robin-aws changed the title ~~feat: add type descriptors for java (WIP)~~ feat: add type descriptors for data constructors in Java (WIP) Oct 23, 2023

robin-aws added 3 commits October 23, 2023 15:14

Missing file

e841a8a

Missed one in DDB

213da2b

Add dafnyVersion parameter, make type descriptors conditional

0a24bc8

robin-aws force-pushed the robin-aws/add-type-descriptors-for-java branch from a116040 to 0a24bc8 Compare October 29, 2023 16:02

robin-aws added 16 commits October 29, 2023 09:09

Add —dafny-version to CLI

6d8b292

Test multiple Dafny versions in CI

180d29c

Specify —dafny-version

5c65aa7

Avoid conditional type descriptors in UTF8

05327d8

Working around create_Success in test services

4d67a3d

Fix KMS

ad4ac89

Fix test shim type descriptor

49c7de3

public

ae8d542

Fix unit tests and local service

9e2cb47

Fix DDB and Errors

33f74af

License headers, typos

f0493fb

Shim.createFailureOfException -> Shim.createFailureOfError

efed9b2

Typo

b6f4f09

Typos, typos everywhere…

fb538e0

Fix test

c8f245e

Cleanup

8a1786b

robin-aws marked this pull request as ready for review October 31, 2023 19:30

robin-aws added 8 commits November 2, 2023 14:57

Upgrade setup-dafny-action to 1.7.0

6c3ac1a

Fix import statements for WrappersInterop

31595e5

Getting tired of only getting partial CI results

9305206

Using service client interface instead of concrete class in abstract …

f20738b

…module

Should be traitForServiceClient after all

3d3e52f

Fix remaining models

28adebb

Fix Dependencies

183b0fa

I said, FIX DEPENDENCIES

937bda6

robin-aws marked this pull request as ready for review November 3, 2023 00:03

robin-aws added 2 commits November 21, 2023 15:34

Skip Extendable model on 4.3

b0527ea

Merge branch 'main-1.x' into robin-aws/add-type-descriptors-for-java

3752aa6

seebees reviewed Nov 22, 2023

View reviewed changes

robin-aws added 2 commits November 22, 2023 09:39

Remove dead code, more comments on the helper methods

6eed666

Merge branch 'robin-aws/add-type-descriptors-for-java' of github.com:…

6f66074

…awslabs/polymorph into robin-aws/add-type-descriptors-for-java

texastony requested changes Nov 27, 2023

View reviewed changes

robin-aws and others added 2 commits November 27, 2023 14:20

Apply suggestions from code review

0db5dec

Co-authored-by: Tony Knapp <[email protected]>

PR feedback

855d329

texastony reviewed Nov 27, 2023

View reviewed changes

.github/workflows/pull.yml Show resolved Hide resolved

texastony approved these changes Nov 27, 2023

View reviewed changes

robin-aws merged commit 8106b08 into main-1.x Nov 27, 2023
122 checks passed

robin-aws deleted the robin-aws/add-type-descriptors-for-java branch November 27, 2023 23:17

robin-aws mentioned this pull request Feb 6, 2024

chore: Forwards compatibility with Dafny > 4.2 (including pending 4.5) aws/aws-cryptographic-material-providers-library#195

Merged

robin-aws mentioned this pull request Feb 26, 2024

fix: Don't call _typeDescriptor() on reference types in Java #321

Merged

robin-aws mentioned this pull request Apr 9, 2024

chore: Change service constructor result type back (from trait to concrete class) #331

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: add type descriptors for data constructors in Java, when necessary #301

feat: add type descriptors for data constructors in Java, when necessary #301

robin-aws commented Oct 20, 2023 •

edited

Loading

seebees Nov 22, 2023

robin-aws Nov 22, 2023

seebees Nov 22, 2023

robin-aws Nov 22, 2023

texastony left a comment

texastony Nov 27, 2023

texastony Nov 27, 2023

robin-aws Nov 27, 2023

texastony Nov 27, 2023


		class WrappersInterop {

		static function method CreateStringSome(s: string): Option<string> {

feat: add type descriptors for data constructors in Java, when necessary #301

feat: add type descriptors for data constructors in Java, when necessary #301

Conversation

robin-aws commented 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

texastony 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

Choose a reason for hiding this comment

robin-aws commented Oct 20, 2023 •

edited

Loading