feat: add type descriptors for data constructors in Java, when necess…

…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 <5892063+texastony@users.noreply.github.com>
ShubhamChaturvedi7 · Feb 24, 2024 · e027e4d · e027e4d
1 parent 420dac3
commit e027e4d
Show file tree

Hide file tree

Showing 72 changed files with 1,093 additions and 264 deletions.
diff --git a/.github/workflows/manual.yml b/.github/workflows/manual.yml
@@ -0,0 +1,26 @@
+# This workflow invokes other workflows with the requested Dafny build.
+# It is primarily meant for manual compatibility testing,
+# such as trying out what the next pending nightly build will do ahead of time.
+name: Manual CI
+
+on:
+  workflow_dispatch:
+    inputs:
+      dafny:
+        description: 'The Dafny version to use'
+        required: true
+        type: string
+
+jobs:
+  manual-ci-verification:
+    uses: ./.github/workflows/test_models_dafny_verification.yml
+    with:
+      dafny: ${{ inputs.dafny }}
+  manual-ci-java:
+    uses: ./.github/workflows/test_models_java_tests.yml
+    with:
+      dafny: ${{ inputs.dafny }}
+  manual-ci-net:
+    uses: ./.github/workflows/test_models_net_tests.yml
+    with:
+      dafny: ${{ inputs.dafny }}
diff --git a/.github/workflows/nightly_dafny.yml b/.github/workflows/nightly_dafny.yml
@@ -0,0 +1,29 @@
+# This workflow invokes other workflows with the nightly Dafny build
+name: Dafny Nightly
+
+on:
+  schedule:
+    # Nightly build against Dafny's nightly prereleases,
+    # for early warning of verification issues or regressions.
+    # Timing chosen to be adequately after Dafny's own nightly build,
+    # but this might need to be tweaked:
+    # https://github.com/dafny-lang/dafny/blob/master/.github/workflows/deep-tests.yml#L16
+    - cron: "30 16 * * *"
+
+jobs:
+  dafny-nightly-verification:
+    # Don't run the cron builds on forks
+    if: github.event_name != 'schedule' || github.repository_owner == 'smithy-lang'
+    uses: ./.github/workflows/test_models_dafny_verification.yml
+    with:
+      dafny: 'nightly-latest'
+  dafny-nightly-java:
+    if: github.event_name != 'schedule' || github.repository_owner == 'smithy-lang'
+    uses: ./.github/workflows/test_models_java_tests.yml
+    with:
+      dafny: 'nightly-latest'
+  dafny-nightly-net:
+    if: github.event_name != 'schedule' || github.repository_owner == 'smithy-lang'
+    uses: ./.github/workflows/test_models_net_tests.yml
+    with:
+      dafny: 'nightly-latest'
diff --git a/.github/workflows/pull.yml b/.github/workflows/pull.yml
@@ -0,0 +1,43 @@
+# This workflow runs for every pull request
+name: PR CI
+
+on:
+  pull_request:
+
+jobs:
+  pr-populate-dafny-versions:
+    runs-on: ubuntu-latest
+    steps:
+    - name: Populate Dafny versions list
+      id: populate-dafny-versions-list
+      run: echo "dafny-versions-list=['4.1.0', '4.3.0']" >> $GITHUB_OUTPUT
+    outputs:
+      dafny-version-list: ${{ steps.populate-dafny-versions-list.outputs.dafny-versions-list }}
+
+  pr-ci-verification:
+    needs: pr-populate-dafny-versions
+    strategy:
+      fail-fast: false
+      matrix:
+        dafny-version: ${{ fromJson(needs.pr-populate-dafny-versions.outputs.dafny-version-list) }}
+    uses: ./.github/workflows/test_models_dafny_verification.yml
+    with:
+      dafny: ${{ matrix.dafny-version }}
+  pr-ci-java:
+    needs: pr-populate-dafny-versions
+    strategy:
+      fail-fast: false
+      matrix:
+        dafny-version: ${{ fromJson(needs.pr-populate-dafny-versions.outputs.dafny-version-list) }}
+    uses: ./.github/workflows/test_models_java_tests.yml
+    with:
+      dafny: ${{ matrix.dafny-version }}
+  pr-ci-net:
+    needs: pr-populate-dafny-versions
+    strategy:
+      fail-fast: false
+      matrix:
+        dafny-version: ${{ fromJson(needs.pr-populate-dafny-versions.outputs.dafny-version-list) }}
+    uses: ./.github/workflows/test_models_net_tests.yml
+    with:
+      dafny: ${{ matrix.dafny-version }}
diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
@@ -0,0 +1,45 @@
+# This workflow runs for every push to main-1.x
+name: Push CI
+
+on:
+  push:
+    branches:
+      - main-1.x    
+
+jobs:
+  pr-populate-dafny-versions:
+    runs-on: ubuntu-latest
+    steps:
+    - name: Populate Dafny versions list
+      id: populate-dafny-versions-list
+      run: echo "dafny-versions-list=['4.1.0', '4.3.0']" >> $GITHUB_OUTPUT
+    outputs:
+      dafny-version-list: ${{ steps.populate-dafny-versions-list.outputs.dafny-versions-list }}
+
+  push-ci-verification:
+    needs: pr-populate-dafny-versions
+    strategy:
+      fail-fast: false
+      matrix:
+        dafny-version: ${{ fromJson(needs.pr-populate-dafny-versions.outputs.dafny-version-list) }}
+    uses: ./.github/workflows/test_models_dafny_verification.yml
+    with:
+      dafny: ${{ matrix.dafny-version }}
+  push-ci-java:
+    needs: pr-populate-dafny-versions
+    strategy:
+      fail-fast: false
+      matrix:
+        dafny-version: ${{ fromJson(needs.pr-populate-dafny-versions.outputs.dafny-version-list) }}
+    uses: ./.github/workflows/test_models_java_tests.yml
+    with:
+      dafny: ${{ matrix.dafny-version }}
+  push-ci-net:
+    needs: pr-populate-dafny-versions
+    strategy:
+      fail-fast: false
+      matrix:
+        dafny-version: ${{ fromJson(needs.pr-populate-dafny-versions.outputs.dafny-version-list) }}
+    uses: ./.github/workflows/test_models_net_tests.yml
+    with:
+      dafny: ${{ matrix.dafny-version }}
diff --git a/.github/workflows/test_models_dafny_verification.yml b/.github/workflows/test_models_dafny_verification.yml
@@ -2,33 +2,20 @@
 name: Library Dafny verification
 
 on:
-  pull_request:
-  push:
-    branches:
-      - main-1.x
-  workflow_dispatch:
-    # Manual trigger for this workflow, either the normal version
-    # or the nightly build that uses the latest Dafny prerelease
-    # (accordingly to the "nightly" parameter).
+  workflow_call:
     inputs:
-      nightly:
-        description: 'Run the nightly build'
-        required: false
-        type: boolean
-  schedule:
-    # Nightly build against Dafny's nightly prereleases,
-    # for early warning of verification issues or regressions.
-    # Timing chosen to be adequately after Dafny's own nightly build,
-    # but this might need to be tweaked:
-    # https://github.com/dafny-lang/dafny/blob/master/.github/workflows/deep-tests.yml#L16
-    - cron: "30 16 * * *"
+      dafny:
+        description: 'The Dafny version to run'
+        required: true
+        type: string
 
 jobs:
   verification:
-    # Don't run the nightly build on forks
-    if: github.event_name != 'schedule' || github.repository_owner == 'smithy-lang'
     strategy:
+      fail-fast: false
       matrix:
+        dafny: 
+          - ${{ inputs.dafny }}
         library: [
           TestModels/dafny-dependencies/StandardLibrary, # This stores current Polymorph dependencies that all TestModels depend on
           TestModels/Aggregate,
@@ -62,6 +49,11 @@ jobs:
           TestModels/aws-sdks/sqs-via-cli,
         ]
         os: [ ubuntu-latest ]
+        exclude:
+          # This model tickles a tricky Dafny verification regression to be fixed in 4.4
+          # https://github.com/dafny-lang/dafny/pull/4800
+          - dafny: 4.3.0
+            library: TestModels/Extendable
     runs-on: ${{ matrix.os }}
     env:
       DOTNET_CLI_TELEMETRY_OPTOUT: 1
@@ -74,16 +66,15 @@ jobs:
       - uses: actions/checkout@v2
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.6.1
+        uses: dafny-lang/setup-dafny-action@v1.7.0
         with:
-          # A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports.
-          dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.1.0' }}
+          dafny-version: ${{ inputs.dafny }}
 
       - name: Generate Polymorph Wrapper Dafny code
         shell: bash
         working-directory: ./${{ matrix.library }}
         run: |
-          make polymorph_dafny
+          make polymorph_dafny DAFNY_VERSION_OPTION="--dafny-version $DAFNY_VERSION"
 
       - name: Verify ${{ matrix.library }} Dafny code
         shell: bash

diff --git a/.github/workflows/test_models_java_tests.yml b/.github/workflows/test_models_java_tests.yml
@@ -2,33 +2,24 @@
 name: Library Java tests
 
 on:
-  pull_request:
-  push:
-    branches:
-      - main-1.x
-  workflow_dispatch:
-    # Manual trigger for this workflow, either the normal version
-    # or the nightly build that uses the latest Dafny prerelease
-    # (accordingly to the "nightly" parameter).
+  workflow_call:
     inputs:
-      nightly:
-        description: 'Run the nightly build'
-        required: false
-        type: boolean
-  schedule:
-    # Nightly build against Dafny's nightly prereleases,
-    # for early warning of verification issues or regressions.
-    # Timing chosen to be adequately after Dafny's own nightly build,
-    # but this might need to be tweaked:
-    # https://github.com/dafny-lang/dafny/blob/master/.github/workflows/deep-tests.yml#L16
-    - cron: "30 16 * * *"
+      dafny:
+        description: 'The Dafny version to run'
+        required: true
+        type: string
 
 jobs:
   testJava:
     # Don't run the nightly build on forks
     if: github.event_name != 'schedule' || github.repository_owner == 'smithy-lang'
     strategy:
+      fail-fast: false
       matrix:
+        dafny-version: [
+          4.1.0,
+          4.3.0
+        ]
         library: [
           TestModels/dafny-dependencies/StandardLibrary, # This stores current Polymorph dependencies that all TestModels depend on
           # TestModels/Aggregate,
@@ -82,10 +73,9 @@ jobs:
       - uses: actions/checkout@v3
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.6.1
+        uses: dafny-lang/setup-dafny-action@v1.7.0
         with:
-          # A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports.
-          dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.1.0' }}
+          dafny-version: ${{ inputs.dafny }}
 
       - name: Setup Java 
         uses: actions/setup-java@v3
@@ -108,9 +98,10 @@ jobs:
       - name: Generate Polymorph Dafny and Java code
         shell: bash
         working-directory: ./${{ matrix.library }}
+        # Use $DAFNY_VERSION from setup-dafny-action to handle nightlies correctly
         run: |
-          make polymorph_dafny
-          make polymorph_java
+          make polymorph_dafny DAFNY_VERSION_OPTION="--dafny-version $DAFNY_VERSION"
+          make polymorph_java DAFNY_VERSION_OPTION="--dafny-version $DAFNY_VERSION"
 
       - name: Setup Java 8 for running tests
         uses: actions/setup-java@v3

diff --git a/.github/workflows/test_models_net_tests.yml b/.github/workflows/test_models_net_tests.yml
@@ -2,32 +2,17 @@
 name: Library net tests
 
 on:
-  pull_request:
-  push:
-    branches:
-      - main-1.x
-  workflow_dispatch:
-    # Manual trigger for this workflow, either the normal version
-    # or the nightly build that uses the latest Dafny prerelease
-    # (accordingly to the "nightly" parameter).
+  workflow_call:
     inputs:
-      nightly:
-        description: 'Run the nightly build'
-        required: false
-        type: boolean
-  schedule:
-    # Nightly build against Dafny's nightly prereleases,
-    # for early warning of verification issues or regressions.
-    # Timing chosen to be adequately after Dafny's own nightly build,
-    # but this might need to be tweaked:
-    # https://github.com/dafny-lang/dafny/blob/master/.github/workflows/deep-tests.yml#L16
-    - cron: "30 16 * * *"
+      dafny:
+        description: 'The Dafny version to run'
+        required: true
+        type: string
 
 jobs:
   testDotNet:
-    # Don't run the nightly build on forks
-    if: github.event_name != 'schedule' || github.repository_owner == 'smithy-lang'
     strategy:
+      fail-fast: false
       matrix:
         library: [
           TestModels/dafny-dependencies/StandardLibrary, # This stores current Polymorph dependencies that all TestModels depend on
@@ -85,10 +70,9 @@ jobs:
       - uses: actions/checkout@v3
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.6.1
+        uses: dafny-lang/setup-dafny-action@v1.7.0
         with:
-          # A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports.
-          dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.1.0' }}
+          dafny-version: ${{ inputs.dafny }}
 
       - name: Setup .NET Core SDK ${{ matrix.dotnet-version }}
         uses: actions/setup-dotnet@v3
@@ -116,8 +100,8 @@ jobs:
         shell: bash
         working-directory: ./${{ matrix.library }}
         run: |
-          make polymorph_dafny
-          make polymorph_net
+          make polymorph_dafny DAFNY_VERSION_OPTION="--dafny-version $DAFNY_VERSION"
+          make polymorph_net DAFNY_VERSION_OPTION="--dafny-version $DAFNY_VERSION"
 
       - name: Compile ${{ matrix.library }} implementation
         shell: bash

diff --git a/.gitignore b/.gitignore
@@ -3,4 +3,7 @@
 /.history
 /.smithy.lsp.log
 
-*/**/.idea
+*/**/.idea
+/codegen/smithy-dafny-codegen/bin
+/codegen/smithy-dafny-codegen-cli/bin
+/smithy-dafny-conversion/bin
diff --git a/TestModels/Aggregate/src/Index.dfy b/TestModels/Aggregate/src/Index.dfy
@@ -10,7 +10,7 @@ module {:extern "simple.aggregate.internaldafny"} SimpleAggregate refines Abstra
     }
 
     method SimpleAggregate(config: SimpleAggregateConfig)
-    returns (res: Result<SimpleAggregateClient, Error>) {
+    returns (res: Result<ISimpleAggregateClient, Error>) {
         var client := new SimpleAggregateClient(Operations.Config);
         return Success(client);
     }

diff --git a/...aints/runtimes/java/src/test/java/simple/constraints/internaldafny/wrapped/__default.java b/...aints/runtimes/java/src/test/java/simple/constraints/internaldafny/wrapped/__default.java
@@ -16,6 +16,6 @@ public static Result<ISimpleConstraintsClient, Error> WrappedSimpleConstraints(S
         simple.constraints.model.SimpleConstraintsConfig wrappedConfig = ToNative.SimpleConstraintsConfig(config);
         simple.constraints.SimpleConstraints impl = SimpleConstraints.builder().SimpleConstraintsConfig(wrappedConfig).build();
         TestSimpleConstraints wrappedClient = TestSimpleConstraints.builder().impl(impl).build();
-        return Result.create_Success(wrappedClient);
+        return simple.constraints.internaldafny.__default.CreateSuccessOfClient(wrappedClient);
     }
 }
diff --git a/TestModels/Constraints/src/Index.dfy b/TestModels/Constraints/src/Index.dfy
@@ -10,7 +10,7 @@ module {:extern "simple.constraints.internaldafny" } SimpleConstraints refines A
   }
 
   method SimpleConstraints(config: SimpleConstraintsConfig)
-    returns (res: Result<SimpleConstraintsClient, Error>)
+    returns (res: Result<ISimpleConstraintsClient, Error>)
   {
     var client := new SimpleConstraintsClient(Operations.Config);
     return Success(client);

diff --git a/TestModels/Constructor/src/Index.dfy b/TestModels/Constructor/src/Index.dfy
@@ -16,7 +16,7 @@ module {:extern "simple.constructor.internaldafny" } SimpleConstructor refines A
     }
 
     method SimpleConstructor(config: SimpleConstructorConfig)
-        returns (res: Result<SimpleConstructorClient, Error>)
+        returns (res: Result<ISimpleConstructorClient, Error>)
     {
         var configToAssign := Operations.Config(
             blobValue := config.blobValue.UnwrapOr([0]),