diff --git a/.github/workflows/manual.yml b/.github/workflows/manual.yml new file mode 100644 index 000000000..22febd0bd --- /dev/null +++ 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 new file mode 100644 index 000000000..f202460f0 --- /dev/null +++ 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 new file mode 100644 index 000000000..9eb93e9f5 --- /dev/null +++ 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 new file mode 100644 index 000000000..40021d927 --- /dev/null +++ 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 index 683a95b18..436bc306f 100644 --- 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 index 4fcc1bd19..9bbac33c5 100644 --- 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 index 65dca60b7..cc18675e5 100644 --- 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 index 3acc1c840..4dfaf7fad 100644 --- a/.gitignore +++ b/.gitignore @@ -3,4 +3,7 @@ /.history /.smithy.lsp.log -*/**/.idea \ No newline at end of file +*/**/.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 index dcc2cda02..5e845b0df 100644 --- 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) { + returns (res: Result) { var client := new SimpleAggregateClient(Operations.Config); return Success(client); } diff --git a/TestModels/Constraints/runtimes/java/src/test/java/simple/constraints/internaldafny/wrapped/__default.java b/TestModels/Constraints/runtimes/java/src/test/java/simple/constraints/internaldafny/wrapped/__default.java index 56499c7b9..d3f1b383a 100644 --- a/TestModels/Constraints/runtimes/java/src/test/java/simple/constraints/internaldafny/wrapped/__default.java +++ b/TestModels/Constraints/runtimes/java/src/test/java/simple/constraints/internaldafny/wrapped/__default.java @@ -16,6 +16,6 @@ public static Result 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 index f8979e553..c1967d888 100644 --- 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) + returns (res: Result) { var client := new SimpleConstraintsClient(Operations.Config); return Success(client); diff --git a/TestModels/Constructor/src/Index.dfy b/TestModels/Constructor/src/Index.dfy index 93aed973c..c7bc34faf 100644 --- 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) + returns (res: Result) { var configToAssign := Operations.Config( blobValue := config.blobValue.UnwrapOr([0]), diff --git a/TestModels/Dependencies/src/Index.dfy b/TestModels/Dependencies/src/Index.dfy index 5f4ee12b5..3320e9820 100644 --- a/TestModels/Dependencies/src/Index.dfy +++ b/TestModels/Dependencies/src/Index.dfy @@ -25,7 +25,7 @@ module {:extern "simple.dependencies.internaldafny" } SimpleDependencies refines } method SimpleDependencies(config: SimpleDependenciesConfig) - returns (res: Result) + returns (res: Result) { expect config.simpleResourcesConfig.Some?; expect config.specialString.Some?; diff --git a/TestModels/Dependencies/src/SimpleDependenciesImpl.dfy b/TestModels/Dependencies/src/SimpleDependenciesImpl.dfy index 6a0a6cabd..e04099ef1 100644 --- a/TestModels/Dependencies/src/SimpleDependenciesImpl.dfy +++ b/TestModels/Dependencies/src/SimpleDependenciesImpl.dfy @@ -85,7 +85,7 @@ module SimpleDependenciesImpl refines AbstractSimpleDependenciesOperations { var simpleResourcesConfig := config.simpleResourcesConfig; - var client: SimpleResources.SimpleResourcesClient :- expect SimpleResources.SimpleResources( + var client: SimpleResourcesTypes.ISimpleResourcesClient :- expect SimpleResources.SimpleResources( simpleResourcesConfig ); diff --git a/TestModels/Errors/runtimes/java/src/test/java/simple/errors/internaldafny/wrapped/__default.java b/TestModels/Errors/runtimes/java/src/test/java/simple/errors/internaldafny/wrapped/__default.java index 36610d07d..eaa10a352 100644 --- a/TestModels/Errors/runtimes/java/src/test/java/simple/errors/internaldafny/wrapped/__default.java +++ b/TestModels/Errors/runtimes/java/src/test/java/simple/errors/internaldafny/wrapped/__default.java @@ -16,6 +16,6 @@ public static Result WrappedSimpleErrors(SimpleError simple.errors.model.SimpleErrorsConfig wrappedConfig = ToNative.SimpleErrorsConfig(config); simple.errors.SimpleErrors impl = SimpleErrors.builder().SimpleErrorsConfig(wrappedConfig).build(); TestSimpleErrors wrappedClient = TestSimpleErrors.builder().impl(impl).build(); - return Result.create_Success(wrappedClient); + return simple.errors.internaldafny.__default.CreateSuccessOfClient(wrappedClient); } } diff --git a/TestModels/Errors/src/Index.dfy b/TestModels/Errors/src/Index.dfy index 4588871b9..b39ad4b7b 100644 --- a/TestModels/Errors/src/Index.dfy +++ b/TestModels/Errors/src/Index.dfy @@ -10,7 +10,7 @@ module {:extern "simple.errors.internaldafny" } SimpleErrors refines AbstractSim } method SimpleErrors(config: SimpleErrorsConfig) - returns (res: Result) + returns (res: Result) { var client := new SimpleErrorsClient(Operations.Config); return Success(client); diff --git a/TestModels/Extendable/runtimes/java/src/test/java/software/simple/extendable/resources/internaldafny/wrapped/__default.java b/TestModels/Extendable/runtimes/java/src/test/java/software/simple/extendable/resources/internaldafny/wrapped/__default.java index 43c0d85f4..48539bd0e 100644 --- a/TestModels/Extendable/runtimes/java/src/test/java/software/simple/extendable/resources/internaldafny/wrapped/__default.java +++ b/TestModels/Extendable/runtimes/java/src/test/java/software/simple/extendable/resources/internaldafny/wrapped/__default.java @@ -22,7 +22,7 @@ public static Result WrappedSimpleExten simple.extendable.resources.model.SimpleExtendableResourcesConfig wrappedConfig = ToNative.SimpleExtendableResourcesConfig(config); simple.extendable.resources.SimpleExtendableResources impl = SimpleExtendableResources.builder().SimpleExtendableResourcesConfig(wrappedConfig).build(); TestSimpleExtendableResources wrappedClient = TestSimpleExtendableResources.builder().impl(impl).build(); - return Result.create_Success(wrappedClient); + return simple.extendable.resources.internaldafny.__default.CreateSuccessOfClient(wrappedClient); } /** diff --git a/TestModels/Extendable/src/Index.dfy b/TestModels/Extendable/src/Index.dfy index d3ccc91d8..5ab67455a 100644 --- a/TestModels/Extendable/src/Index.dfy +++ b/TestModels/Extendable/src/Index.dfy @@ -20,7 +20,7 @@ module // so the implementation MUST have it. config: SimpleExtendableResourcesConfig ) returns ( - res: Result + res: Result ) { var internalConfig := Operations.Config(); diff --git a/TestModels/Extern/src/Index.dfy b/TestModels/Extern/src/Index.dfy index cc8c5b101..845fc23cf 100644 --- a/TestModels/Extern/src/Index.dfy +++ b/TestModels/Extern/src/Index.dfy @@ -10,7 +10,7 @@ module {:extern "simple.dafnyextern.internaldafny" } SimpleExtern refines Abstra } method SimpleExtern(config: SimpleExternConfig) - returns (res: Result) + returns (res: Result) { var client := new SimpleExternClient(Operations.Config); return Success(client); diff --git a/TestModels/LocalService/runtimes/java/src/test/java/simple/localservice/internaldafny/wrapped/__default.java b/TestModels/LocalService/runtimes/java/src/test/java/simple/localservice/internaldafny/wrapped/__default.java index 51e85a21f..8f85fc96a 100644 --- a/TestModels/LocalService/runtimes/java/src/test/java/simple/localservice/internaldafny/wrapped/__default.java +++ b/TestModels/LocalService/runtimes/java/src/test/java/simple/localservice/internaldafny/wrapped/__default.java @@ -18,7 +18,7 @@ public static Result WrappedSimpleLocalService simple.localservice.SimpleLocalService impl = SimpleLocalService.builder().SimpleLocalServiceConfig(wrappedConfig).build(); TestToNativeAndToDafnyLocalService(impl); TestSimpleLocalService wrappedClient = TestSimpleLocalService.builder().impl(impl).build(); - return Result.create_Success(wrappedClient); + return simple.localservice.internaldafny.__default.CreateSuccessOfClient(wrappedClient); } // TODO: Determine how to replace this test with Dafny Source Code diff --git a/TestModels/LocalService/src/Index.dfy b/TestModels/LocalService/src/Index.dfy index 9a566b871..9d59225fd 100644 --- a/TestModels/LocalService/src/Index.dfy +++ b/TestModels/LocalService/src/Index.dfy @@ -18,7 +18,7 @@ module method SimpleLocalService( config: SimpleLocalServiceConfig ) returns ( - res: Result + res: Result ) { var client := new SimpleLocalServiceClient(Operations.Config); diff --git a/TestModels/Refinement/src/Index.dfy b/TestModels/Refinement/src/Index.dfy index 51b23ccc7..06205012a 100644 --- a/TestModels/Refinement/src/Index.dfy +++ b/TestModels/Refinement/src/Index.dfy @@ -12,7 +12,7 @@ module {:extern "simple.refinement.internaldafny"} SimpleRefinement refines Abst method SimpleRefinement( config: SimpleRefinementConfig ) returns ( - res: Result + res: Result ) { var client := new SimpleRefinementClient(Operations.Config); return Success(client); diff --git a/TestModels/Resource/runtimes/java/src/test/java/simple/resources/internaldafny/wrapped/__default.java b/TestModels/Resource/runtimes/java/src/test/java/simple/resources/internaldafny/wrapped/__default.java index c77ce7d4d..c6bcb7541 100644 --- a/TestModels/Resource/runtimes/java/src/test/java/simple/resources/internaldafny/wrapped/__default.java +++ b/TestModels/Resource/runtimes/java/src/test/java/simple/resources/internaldafny/wrapped/__default.java @@ -16,6 +16,6 @@ public static Result WrappedSimpleResources(Simpl simple.resources.model.SimpleResourcesConfig wrappedConfig = ToNative.SimpleResourcesConfig(config); simple.resources.SimpleResources impl = SimpleResources.builder().SimpleResourcesConfig(wrappedConfig).build(); TestSimpleResources wrappedClient = TestSimpleResources.builder().impl(impl).build(); - return Result.create_Success(wrappedClient); + return simple.resources.internaldafny.__default.CreateSuccessOfClient(wrappedClient); } } diff --git a/TestModels/Resource/src/Index.dfy b/TestModels/Resource/src/Index.dfy index 6df0f8d08..ab1be9fec 100644 --- a/TestModels/Resource/src/Index.dfy +++ b/TestModels/Resource/src/Index.dfy @@ -20,7 +20,7 @@ module method SimpleResources( config: SimpleResourcesConfig ) returns ( - res: Result + res: Result ) { var internalConfig: Operations.InternalConfig := Operations.Config( diff --git a/TestModels/SharedMakefile.mk b/TestModels/SharedMakefile.mk index d2cdb7c25..d71267049 100644 --- a/TestModels/SharedMakefile.mk +++ b/TestModels/SharedMakefile.mk @@ -151,6 +151,7 @@ _polymorph: @: $(if ${CODEGEN_CLI_ROOT},,$(error You must pass the path CODEGEN_CLI_ROOT: CODEGEN_CLI_ROOT=/path/to/smithy-dafny/codegen/smithy-dafny-codegen-cli)); cd $(CODEGEN_CLI_ROOT); \ $(GRADLEW) run --args="\ + $(DAFNY_VERSION_OPTION) \ $(OUTPUT_DAFNY) \ $(OUTPUT_DOTNET) \ $(OUTPUT_JAVA) \ @@ -164,6 +165,7 @@ _polymorph_wrapped: @: $(if ${CODEGEN_CLI_ROOT},,$(error You must pass the path CODEGEN_CLI_ROOT: CODEGEN_CLI_ROOT=/path/to/smithy-dafny/codegen/smithy-dafny-codegen-cli)); cd $(CODEGEN_CLI_ROOT); \ $(GRADLEW) run --args="\ + $(DAFNY_VERSION_OPTION) \ $(OUTPUT_DAFNY_WRAPPED) \ $(OUTPUT_DOTNET_WRAPPED) \ $(OUTPUT_JAVA_WRAPPED) \ diff --git a/TestModels/SimpleTypes/SimpleBlob/src/Index.dfy b/TestModels/SimpleTypes/SimpleBlob/src/Index.dfy index ec82dd2e4..5baa61e60 100644 --- a/TestModels/SimpleTypes/SimpleBlob/src/Index.dfy +++ b/TestModels/SimpleTypes/SimpleBlob/src/Index.dfy @@ -10,7 +10,7 @@ module {:extern "simple.types.blob.internaldafny" } SimpleBlob refines AbstractS } method SimpleBlob(config: SimpleBlobConfig) - returns (res: Result) { + returns (res: Result) { var client := new SimpleBlobClient(Operations.Config); return Success(client); } diff --git a/TestModels/SimpleTypes/SimpleBoolean/src/Index.dfy b/TestModels/SimpleTypes/SimpleBoolean/src/Index.dfy index 0c068e575..3284fd21f 100644 --- a/TestModels/SimpleTypes/SimpleBoolean/src/Index.dfy +++ b/TestModels/SimpleTypes/SimpleBoolean/src/Index.dfy @@ -10,7 +10,7 @@ module {:extern "simple.types.boolean.internaldafny" } SimpleBoolean refines Abs } method SimpleBoolean(config: SimpleBooleanConfig) - returns (res: Result) { + returns (res: Result) { var client := new SimpleBooleanClient(Operations.Config); return Success(client); } diff --git a/TestModels/SimpleTypes/SimpleDouble/src/Index.dfy b/TestModels/SimpleTypes/SimpleDouble/src/Index.dfy index b7a48b6b6..98b617c6d 100644 --- a/TestModels/SimpleTypes/SimpleDouble/src/Index.dfy +++ b/TestModels/SimpleTypes/SimpleDouble/src/Index.dfy @@ -12,7 +12,7 @@ module {:extern "simple.types.smithydouble.internaldafny" } SimpleDouble refines } method SimpleDouble(config: SimpleDoubleConfig) - returns (res: Result) { + returns (res: Result) { var client := new SimpleDoubleClient(Operations.Config); return Success(client); } diff --git a/TestModels/SimpleTypes/SimpleEnum/src/Index.dfy b/TestModels/SimpleTypes/SimpleEnum/src/Index.dfy index ae668b750..ef894dbeb 100644 --- a/TestModels/SimpleTypes/SimpleEnum/src/Index.dfy +++ b/TestModels/SimpleTypes/SimpleEnum/src/Index.dfy @@ -10,7 +10,7 @@ module {:extern "simple.types.smithyenum.internaldafny" } SimpleEnum refines Abs } method SimpleEnum(config: SimpleEnumConfig) - returns (res: Result) { + returns (res: Result) { var client := new SimpleEnumClient(Operations.Config); return Success(client); } diff --git a/TestModels/SimpleTypes/SimpleInteger/src/Index.dfy b/TestModels/SimpleTypes/SimpleInteger/src/Index.dfy index 3dd7ea75f..f092c0e6f 100644 --- a/TestModels/SimpleTypes/SimpleInteger/src/Index.dfy +++ b/TestModels/SimpleTypes/SimpleInteger/src/Index.dfy @@ -10,7 +10,7 @@ module {:extern "simple.types.integer.internaldafny" } SimpleInteger refines Abs } method SimpleInteger(config: SimpleIntegerConfig) - returns (res: Result) { + returns (res: Result) { var client := new SimpleIntegerClient(Operations.Config); return Success(client); } diff --git a/TestModels/SimpleTypes/SimpleLong/src/Index.dfy b/TestModels/SimpleTypes/SimpleLong/src/Index.dfy index 0680c3a1e..44ed0d0ee 100644 --- a/TestModels/SimpleTypes/SimpleLong/src/Index.dfy +++ b/TestModels/SimpleTypes/SimpleLong/src/Index.dfy @@ -10,7 +10,7 @@ module {:extern "simple.types.smithylong.internaldafny" } SimpleLong refines Abs } method SimpleLong(config: SimpleLongConfig) - returns (res: Result) { + returns (res: Result) { var client := new SimpleLongClient(Operations.Config); return Success(client); } diff --git a/TestModels/SimpleTypes/SimpleString/src/Index.dfy b/TestModels/SimpleTypes/SimpleString/src/Index.dfy index d0d265219..e0fed14bb 100644 --- a/TestModels/SimpleTypes/SimpleString/src/Index.dfy +++ b/TestModels/SimpleTypes/SimpleString/src/Index.dfy @@ -10,7 +10,7 @@ module {:extern "simple.types.smithystring.internaldafny" } SimpleString refines } method SimpleString(config: SimpleStringConfig) - returns (res: Result) { + returns (res: Result) { var client := new SimpleStringClient(Operations.Config); return Success(client); } diff --git a/TestModels/Union/src/Index.dfy b/TestModels/Union/src/Index.dfy index 37ae46b2d..ba859b1c5 100644 --- a/TestModels/Union/src/Index.dfy +++ b/TestModels/Union/src/Index.dfy @@ -10,7 +10,7 @@ module {:extern "simple.union.internaldafny" } SimpleUnion refines AbstractSimpl } method SimpleUnion(config: SimpleUnionConfig) - returns (res: Result) + returns (res: Result) { var client := new SimpleUnionClient(Operations.Config); return Success(client); diff --git a/TestModels/aws-sdks/ddb/runtimes/java/src/main/java/software/amazon/cryptography/services/dynamodb/internaldafny/__default.java b/TestModels/aws-sdks/ddb/runtimes/java/src/main/java/software/amazon/cryptography/services/dynamodb/internaldafny/__default.java index 926b5bd27..2640a177f 100644 --- a/TestModels/aws-sdks/ddb/runtimes/java/src/main/java/software/amazon/cryptography/services/dynamodb/internaldafny/__default.java +++ b/TestModels/aws-sdks/ddb/runtimes/java/src/main/java/software/amazon/cryptography/services/dynamodb/internaldafny/__default.java @@ -4,6 +4,7 @@ import software.amazon.cryptography.services.dynamodb.internaldafny.types.IDynamoDBClient; import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error; +import StandardLibrary_mInterop_Compile.WrappersInterop; import Wrappers_Compile.Option; import Wrappers_Compile.Result; import software.amazon.awssdk.auth.credentials.ProfileCredentialsProvider; @@ -25,11 +26,11 @@ public static Result DynamoDBClient() { .build(); IDynamoDBClient shim = new Shim(ddbClient, region.toString()); - return Result.create_Success(shim); + return CreateSuccessOfClient(shim); } catch (Exception e) { Error dafny_error = Error.create_InternalServerError( - Option.create_Some(CharacterSequence(e.getMessage()))); - return Result.create_Failure(dafny_error); + WrappersInterop.CreateStringSome(CharacterSequence(e.getMessage()))); + return CreateFailureOfError(dafny_error); } } } diff --git a/TestModels/aws-sdks/kms/runtimes/java/src/main/java/software/amazon/cryptography/services/kms/internal/__default.java b/TestModels/aws-sdks/kms/runtimes/java/src/main/java/software/amazon/cryptography/services/kms/internal/__default.java index 80d531aea..60c2c0047 100644 --- a/TestModels/aws-sdks/kms/runtimes/java/src/main/java/software/amazon/cryptography/services/kms/internal/__default.java +++ b/TestModels/aws-sdks/kms/runtimes/java/src/main/java/software/amazon/cryptography/services/kms/internal/__default.java @@ -12,6 +12,7 @@ import software.amazon.cryptography.services.kms.internaldafny.types.Error; import software.amazon.cryptography.services.kms.internaldafny.types.IKMSClient; +import StandardLibrary_mInterop_Compile.WrappersInterop; import Wrappers_Compile.Option; import Wrappers_Compile.Result; @@ -26,11 +27,11 @@ public static Result KMSClient() { String region = regionProvider.getRegion().toString(); KmsClient client = builder.build(); IKMSClient shim = new Shim(client, region); - return Result.create_Success(shim); + return CreateSuccessOfClient(shim); } catch (Exception e) { Error dafny_error = Error.create_KMSInternalException( - Option.create_Some(CharacterSequence(e.getMessage()))); - return Result.create_Failure(dafny_error); + WrappersInterop.CreateStringSome(CharacterSequence(e.getMessage()))); + return CreateFailureOfError(dafny_error); } } @@ -39,11 +40,11 @@ public static Result KMSClient(final String region) { KmsClientBuilder builder = KmsClient.builder(); KmsClient client = builder.region(Region.of(region)).build(); IKMSClient shim = new Shim(client, region); - return Result.create_Success(shim); + return CreateSuccessOfClient(shim); } catch (Exception e) { Error dafny_error = Error.create_KMSInternalException( - Option.create_Some(CharacterSequence(e.getMessage()))); - return Result.create_Failure(dafny_error); + WrappersInterop.CreateStringSome(CharacterSequence(e.getMessage()))); + return CreateFailureOfError(dafny_error); } } @@ -60,13 +61,13 @@ public static Wrappers_Compile.Option RegionMatch( // have no way to determine what region it is // configured with. if (shim.region() == null) { - return Option.create_None(); + return WrappersInterop.CreateBooleanNone(); } // Otherwise we kept record of the region // when we created the client. String shimRegion = shim.region(); String regionStr = String(region); - return Option.create_Some(regionStr.equals(shimRegion)); + return WrappersInterop.CreateBooleanSome(regionStr.equals(shimRegion)); } } diff --git a/TestModels/dafny-dependencies/StandardLibrary/runtimes/java/src/main/java/UTF8/__default.java b/TestModels/dafny-dependencies/StandardLibrary/runtimes/java/src/main/java/UTF8/__default.java index b39b871ec..c3171cdd8 100644 --- a/TestModels/dafny-dependencies/StandardLibrary/runtimes/java/src/main/java/UTF8/__default.java +++ b/TestModels/dafny-dependencies/StandardLibrary/runtimes/java/src/main/java/UTF8/__default.java @@ -41,10 +41,10 @@ DafnySequence> Encode( // outBuffer's capacity can be much higher than the limit. // By taking just the limit, we ensure we do not include // any allocated but un-filled space. - return Result.create_Success( + return CreateEncodeSuccess( (DafnySequence) ByteSequence(outBuffer, 0, outBuffer.limit())); } catch (CharacterCodingException ex) { - return Result.create_Failure( + return CreateEncodeFailure( (DafnySequence) CharacterSequence("Could not encode input to Dafny Bytes.")); } } @@ -63,10 +63,10 @@ DafnySequence> Decode( try { CharBuffer outBuffer = coder.decode(inBuffer); outBuffer.position(0); - return Result.create_Success( + return CreateDecodeSuccess( (DafnySequence) CharacterSequence(outBuffer.toString())); } catch (CharacterCodingException ex) { - return Result.create_Failure( + return CreateDecodeFailure( (DafnySequence) CharacterSequence("Could not encode input to Dafny Bytes.")); } } diff --git a/TestModels/dafny-dependencies/StandardLibrary/src/Index.dfy b/TestModels/dafny-dependencies/StandardLibrary/src/Index.dfy index 1b47b6c9f..e9c061a82 100644 --- a/TestModels/dafny-dependencies/StandardLibrary/src/Index.dfy +++ b/TestModels/dafny-dependencies/StandardLibrary/src/Index.dfy @@ -1,6 +1,7 @@ // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 +include "./WrappersInterop.dfy" include "./StandardLibrary.dfy" include "./UInt.dfy" include "./UTF8.dfy" \ No newline at end of file diff --git a/TestModels/dafny-dependencies/StandardLibrary/src/UTF8.dfy b/TestModels/dafny-dependencies/StandardLibrary/src/UTF8.dfy index cabfe05d1..ca889813e 100644 --- a/TestModels/dafny-dependencies/StandardLibrary/src/UTF8.dfy +++ b/TestModels/dafny-dependencies/StandardLibrary/src/UTF8.dfy @@ -33,6 +33,27 @@ module {:extern "UTF8"} UTF8 { function method {:extern "Decode"} Decode(b: seq): (res: Result) ensures res.Success? ==> ValidUTF8Seq(b) + // The next four functions are for the benefit of the extern implementation to call, + // avoiding direct references to generic datatype constructors + // since their calling pattern is different between different versions of Dafny + // (i.e. after 4.2, explicit type descriptors are required). + + function method CreateEncodeSuccess(bytes: ValidUTF8Bytes): Result { + Success(bytes) + } + + function method CreateEncodeFailure(error: string): Result { + Failure(error) + } + + function method CreateDecodeSuccess(s: string): Result { + Success(s) + } + + function method CreateDecodeFailure(error: string): Result { + Failure(error) + } + predicate method IsASCIIString(s: string) { forall i :: 0 <= i < |s| ==> s[i] as int < 128 } diff --git a/TestModels/dafny-dependencies/StandardLibrary/src/WrappersInterop.dfy b/TestModels/dafny-dependencies/StandardLibrary/src/WrappersInterop.dfy new file mode 100644 index 000000000..84e91c4a2 --- /dev/null +++ b/TestModels/dafny-dependencies/StandardLibrary/src/WrappersInterop.dfy @@ -0,0 +1,48 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +include "../../libraries/src/Wrappers.dfy" + +// +// Helper functions for extern code to call in order to create common wrapper types. +// +// This is currently necessary to abstract away from differences in TypeDescriptor usage +// in the Java backend across different versions of Dafny: +// after Dafny 4.2 methods like Option.create_Some() +// also require explicit TypeDescriptor arguments. +// If we declare a `CreateSome(t: T)` function, +// the compiled version may or may not need a type descriptor, +// which means test models would need to have different Java code for different Dafny versions. +// But if we define a non-generic version for a specific type, +// Dafny will emit the right type descriptor instances inside the compiled method, +// so the calling signature is the same across Dafny versions. +// +// These may be useful for other target languages in the future as well, +// to similarly abstract away from Dafny compilation internal details. +// +// See also DafnyApiCodegen.generateResultOfClientHelperFunctions(), +// which solves the same problem by emitting similar helper methods for each client type. +// +module StandardLibrary.Interop { + + import opened Wrappers + + class WrappersInterop { + + static function method CreateStringSome(s: string): Option { + Some(s) + } + + static function method CreateStringNone(): Option { + None + } + + static function method CreateBooleanSome(b: bool): Option { + Some(b) + } + + static function method CreateBooleanNone(): Option { + None + } + } +} \ No newline at end of file diff --git a/codegen/smithy-dafny-codegen-cli/src/main/java/software/amazon/polymorph/CodegenCli.java b/codegen/smithy-dafny-codegen-cli/src/main/java/software/amazon/polymorph/CodegenCli.java index 2e3869077..87f9d7ed6 100644 --- a/codegen/smithy-dafny-codegen-cli/src/main/java/software/amazon/polymorph/CodegenCli.java +++ b/codegen/smithy-dafny-codegen-cli/src/main/java/software/amazon/polymorph/CodegenCli.java @@ -4,6 +4,7 @@ package software.amazon.polymorph; import software.amazon.polymorph.CodegenEngine.TargetLanguage; +import software.amazon.polymorph.smithydafny.DafnyVersion; import software.amazon.polymorph.smithyjava.generator.CodegenSubject.AwsSdkVersion; import org.apache.commons.cli.CommandLine; @@ -73,7 +74,8 @@ public static void main(String[] args) { .withNamespace(cliArguments.namespace) .withTargetLangOutputDirs(outputDirs) .withAwsSdkStyle(cliArguments.awsSdkStyle) - .withLocalServiceTest(cliArguments.localServiceTest); + .withLocalServiceTest(cliArguments.localServiceTest) + .withDafnyVersion(cliArguments.dafnyVersion); cliArguments.javaAwsSdkVersion.ifPresent(engineBuilder::withJavaAwsSdkVersion); cliArguments.includeDafnyFile.ifPresent(engineBuilder::withIncludeDafnyFile); final CodegenEngine engine = engineBuilder.build(); @@ -119,6 +121,11 @@ private static Options getCliOptions() { .desc(" AWS SDK for Java version to use: v1, or v2 (default)") .hasArg() .build()) + .addOption(Option.builder() + .longOpt("dafny-version") + .desc("Dafny version to generate code for") + .hasArg() + .build()) .addOption(Option.builder() .longOpt("aws-sdk") .desc(" generate AWS SDK-style API and shims") @@ -152,6 +159,7 @@ private record CliArguments( Optional outputJavaDir, Optional outputDafnyDir, Optional javaAwsSdkVersion, + DafnyVersion dafnyVersion, Optional includeDafnyFile, boolean awsSdkStyle, boolean localServiceTest @@ -205,6 +213,19 @@ static Optional parse(String[] args) throws ParseException { } } + DafnyVersion dafnyVersion; + String versionStr = commandLine.getOptionValue("dafny-version"); + if (versionStr == null) { + LOGGER.error("--dafny-version option is required"); + System.exit(-1); + } + try { + dafnyVersion = DafnyVersion.parse(versionStr.trim()); + } catch (IllegalArgumentException ex) { + LOGGER.error("Could not parse --dafny-version: {}", versionStr); + throw ex; + } + Optional includeDafnyFile = Optional.empty(); if (outputDafnyDir.isPresent()) { includeDafnyFile = Optional.of(Paths.get(commandLine.getOptionValue("include-dafny"))); @@ -213,7 +234,7 @@ static Optional parse(String[] args) throws ParseException { return Optional.of(new CliArguments( modelPath, dependentModelPaths, namespace, outputDotnetDir, outputJavaDir, outputDafnyDir, - javaAwsSdkVersion, includeDafnyFile, awsSdkStyle, + javaAwsSdkVersion, dafnyVersion, includeDafnyFile, awsSdkStyle, localServiceTest )); } diff --git a/codegen/smithy-dafny-codegen/README.md b/codegen/smithy-dafny-codegen/README.md index 467f3a0b3..642bef8e8 100644 --- a/codegen/smithy-dafny-codegen/README.md +++ b/codegen/smithy-dafny-codegen/README.md @@ -86,9 +86,10 @@ are as follows: "version": "1.0", "plugins": { "dafny-client-codegen": { - "edition": "2023", + "edition": "2023.10", "service": "smithy.example#ExampleService", "targetLanguages": ["dotnet"], + "dafnyVersion": "4.3.0", "includeDafnyFile": "[relative]/[path]/[to]/StandardLibrary/src/Index.dfy" } } diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/CodegenEngine.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/CodegenEngine.java index 556d07511..cbdf075e3 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/CodegenEngine.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/CodegenEngine.java @@ -8,6 +8,7 @@ import org.slf4j.Logger; import org.slf4j.LoggerFactory; import software.amazon.polymorph.smithydafny.DafnyApiCodegen; +import software.amazon.polymorph.smithydafny.DafnyVersion; import software.amazon.polymorph.smithydotnet.AwsSdkShimCodegen; import software.amazon.polymorph.smithydotnet.AwsSdkTypeConversionCodegen; import software.amazon.polymorph.smithydotnet.ServiceCodegen; @@ -21,6 +22,7 @@ import software.amazon.polymorph.smithyjava.generator.awssdk.v2.JavaAwsSdkV2; import software.amazon.polymorph.smithyjava.generator.library.JavaLibrary; import software.amazon.polymorph.smithyjava.generator.library.TestJavaLibrary; +import software.amazon.polymorph.smithyjava.nameresolver.Dafny; import software.amazon.polymorph.utils.IOUtils; import software.amazon.polymorph.utils.ModelUtils; import software.amazon.smithy.aws.traits.ServiceTrait; @@ -41,6 +43,7 @@ public class CodegenEngine { private final Path[] dependentModelPaths; private final String namespace; private final Map targetLangOutputDirs; + private final DafnyVersion dafnyVersion; // refactor this to only be required if generating Java private final AwsSdkVersion javaAwsSdkVersion; private final Optional includeDafnyFile; @@ -62,6 +65,7 @@ private CodegenEngine( final Path[] dependentModelPaths, final String namespace, final Map targetLangOutputDirs, + final DafnyVersion dafnyVersion, final AwsSdkVersion javaAwsSdkVersion, final Optional includeDafnyFile, final boolean awsSdkStyle, @@ -72,6 +76,7 @@ private CodegenEngine( this.dependentModelPaths = dependentModelPaths; this.namespace = namespace; this.targetLangOutputDirs = targetLangOutputDirs; + this.dafnyVersion = dafnyVersion; this.javaAwsSdkVersion = javaAwsSdkVersion; this.includeDafnyFile = includeDafnyFile; this.awsSdkStyle = awsSdkStyle; @@ -150,13 +155,13 @@ private void generateJava(final Path outputDir) { } private void javaLocalService(final Path outputDir) { - final JavaLibrary javaLibrary = new JavaLibrary(this.model, this.serviceShape, this.javaAwsSdkVersion); + final JavaLibrary javaLibrary = new JavaLibrary(this.model, this.serviceShape, this.javaAwsSdkVersion, this.dafnyVersion); IOUtils.writeTokenTreesIntoDir(javaLibrary.generate(), outputDir); LOGGER.info("Java code generated in {}", outputDir); } private void javaWrappedLocalService(final Path outputDir) { - final TestJavaLibrary testJavaLibrary = new TestJavaLibrary(model, serviceShape, this.javaAwsSdkVersion); + final TestJavaLibrary testJavaLibrary = new TestJavaLibrary(model, serviceShape, this.javaAwsSdkVersion, this.dafnyVersion); IOUtils.writeTokenTreesIntoDir(testJavaLibrary.generate(), outputDir); LOGGER.info("Java that tests a local service generated in {}", outputDir); } @@ -168,7 +173,7 @@ private void javaAwsSdkV1(Path outputDir) { } private void javaAwsSdkV2(final Path outputDir) { - final JavaAwsSdkV2 javaV2ShimCodegen = JavaAwsSdkV2.createJavaAwsSdkV2(serviceShape, model); + final JavaAwsSdkV2 javaV2ShimCodegen = JavaAwsSdkV2.createJavaAwsSdkV2(serviceShape, model, dafnyVersion); IOUtils.writeTokenTreesIntoDir(javaV2ShimCodegen.generate(), outputDir); LOGGER.info("Java V2 code generated in {}", outputDir); } @@ -245,6 +250,7 @@ public static class Builder { private Path[] dependentModelPaths; private String namespace; private Map targetLangOutputDirs; + private DafnyVersion dafnyVersion = new DafnyVersion(4, 1, 0); private AwsSdkVersion javaAwsSdkVersion = AwsSdkVersion.V2; private Path includeDafnyFile; private boolean awsSdkStyle = false; @@ -286,6 +292,17 @@ public Builder withTargetLangOutputDirs(final Map targetLa return this; } + /** + * Sets the Dafny version for which generated code should be compatible. + * This is used to ensure both Dafny source compatibility + * and compatibility with the Dafny compiler and runtime internals, + * which shim code generation currently depends on. + */ + public Builder withDafnyVersion(final DafnyVersion dafnyVersion) { + this.dafnyVersion = dafnyVersion; + return this; + } + /** * Sets the version of the AWS SDK for Java for which generated code should be compatible. * This has no effect unless the engine is configured to generate Java code. @@ -341,6 +358,7 @@ public CodegenEngine build() { targetLangOutputDirsRaw.replaceAll((_lang, path) -> path.toAbsolutePath().normalize()); final Map targetLangOutputDirs = ImmutableMap.copyOf(targetLangOutputDirsRaw); + final DafnyVersion dafnyVersion = Objects.requireNonNull(this.dafnyVersion); final AwsSdkVersion javaAwsSdkVersion = Objects.requireNonNull(this.javaAwsSdkVersion); if (targetLangOutputDirs.containsKey(TargetLanguage.DAFNY) @@ -360,6 +378,7 @@ public CodegenEngine build() { dependentModelPaths, this.namespace, targetLangOutputDirs, + dafnyVersion, javaAwsSdkVersion, includeDafnyFile, this.awsSdkStyle, diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java index 632d86eaf..d8afb4859 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java @@ -1859,6 +1859,7 @@ private TokenTree modifiesClauseForPathToReference( public TokenTree generateAbstractLocalService(ServiceShape serviceShape) { if (!serviceShape.hasTrait(LocalServiceTrait.class)) throw new IllegalStateException("MUST be an LocalService"); final LocalServiceTrait localServiceTrait = serviceShape.expectTrait(LocalServiceTrait.class); + final String dafnyClientTrait = nameResolver.traitForServiceClient(serviceShape); final String configTypeName = nameResolver.baseTypeForShape(localServiceTrait.getConfigId()); final String defaultFunctionMethodName = "Default%s".formatted(localServiceTrait.getConfigId().getName()); @@ -1883,8 +1884,7 @@ public TokenTree generateAbstractLocalService(ServiceShape serviceShape) { ), // Yes, Error is hard coded // this can work because we need to be able Errors from other modules... - "returns (res: Result<%sClient, Error>)\n" - .formatted(localServiceTrait.getSdkId()) + "returns (res: Result<%s, Error>)\n".formatted(dafnyClientTrait) ).lineSeparated(); // Add `requires` clauses @@ -1953,7 +1953,8 @@ public TokenTree generateAbstractLocalService(ServiceShape serviceShape) { return TokenTree .of( defaultConfig, - serviceMethod + serviceMethod, + generateResultOfClientHelperFunctions(dafnyClientTrait) ) .lineSeparated(); } @@ -2013,6 +2014,7 @@ public TokenTree generateAbstractAwsServiceClass(ServiceShape serviceShape) { if (!serviceShape.hasTrait(ServiceTrait.class)) throw new IllegalStateException("MUST be an AWS Service API"); final ServiceTrait serviceTrait = serviceShape.expectTrait(ServiceTrait.class); final String sdkId = serviceTrait.getSdkId(); + final String dafnyClientTrait = nameResolver.traitForServiceClient(serviceShape); final String configTypeName = "%sClientConfigType".formatted(sdkId); final TokenTree configType = TokenTree @@ -2026,7 +2028,7 @@ public TokenTree generateAbstractAwsServiceClass(ServiceShape serviceShape) { final TokenTree factory = TokenTree .of( "method {:extern} %sClient()".formatted(serviceTrait.getSdkId()), - "returns (res: Result<%s, Error>)".formatted(nameResolver.traitForServiceClient(serviceShape)), + "returns (res: Result<%s, Error>)".formatted(dafnyClientTrait), "ensures res.Success? ==> ", "&& fresh(res.value)", "&& fresh(res.value.%s)".formatted(nameResolver.mutableStateFunctionName()), @@ -2038,11 +2040,36 @@ public TokenTree generateAbstractAwsServiceClass(ServiceShape serviceShape) { .of( configType, defaultConfig, - factory + factory, + generateResultOfClientHelperFunctions(dafnyClientTrait) ) .lineSeparated(); } + /** + * Generates Dafny methods that don't need to accept TypeDescriptors in some versions of Dafny, + * so that test models can have a single copy of Java code across multiple versions of Dafny. + * + * See also TestModels/dafny-dependencies/StandardLibrary/src/WrappersInterop.dfy. + */ + private static TokenTree generateResultOfClientHelperFunctions(String dafnyClientTrait) { + final TokenTree createSuccessOfClient = TokenTree + .of( + "// Helper function for the benefit of native code to create a Success(client) without referring to Dafny internals", + "function method CreateSuccessOfClient(client: %s): Result<%s, Error> {".formatted(dafnyClientTrait, dafnyClientTrait), + " Success(client)", + "}" + ).lineSeparated(); + final TokenTree createFailureOfError = TokenTree + .of( + "// Helper function for the benefit of native code to create a Failure(error) without referring to Dafny internals", + "function method CreateFailureOfError(error: Error): Result<%s, Error> {".formatted(dafnyClientTrait), + " Failure(error)", + "}" + ).lineSeparated(); + return TokenTree.of(createSuccessOfClient, createFailureOfError); + } + private static TokenTree generateLengthConstraint(final LengthTrait lengthTrait) { final String min = lengthTrait.getMin().map("%s <="::formatted).orElse(""); final String max = lengthTrait.getMax().map("<= %s"::formatted).orElse(""); diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyVersion.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyVersion.java new file mode 100644 index 000000000..dbbdbe726 --- /dev/null +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyVersion.java @@ -0,0 +1,132 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +package software.amazon.polymorph.smithydafny; + +import java.util.Comparator; +import java.util.Objects; + +/** + * Representation of a Dafny version number, according to SemVer 1.0 semantics. + * + * Note that Dafny pre-releases historically have used pre-release suffixes slightly wrong: + * after releasing 4.2 for example, the nightly pre-releases will have version numbers like + * "4.2.0-nightly-2023-08-04-656a114", but that should actually be interpreted as a pre-release + * for 4.2 rather than 4.3. So far that's immaterial for this code base, + * but if it becomes relevant the better solution is for Dafny pre-releases to correct this instead. + */ +public class DafnyVersion implements Comparable { + + private final int major; + private final int minor; + private final int patch; + // Will be non-null only if there was a pre-release suffix + private final String suffix; + + // Anything with a pre-release suffix should be considered less + // than a matching version without one. + private static final Comparator SUFFIX_COMPARATOR = Comparator.nullsLast(Comparator.naturalOrder()); + + public static DafnyVersion parse(String versionString) { + if (!versionString.matches("[0-9\\.A-Za-z\\-]*")) { + throw new IllegalArgumentException(); + } + int firstHyphenIndex = versionString.indexOf("-"); + String majorMinorPatch = versionString; + String suffix = null; + if (firstHyphenIndex >= 0) { + majorMinorPatch = versionString.substring(0, firstHyphenIndex); + suffix = versionString.substring(firstHyphenIndex + 1); + } + String[] splitByDots = majorMinorPatch.split("\\."); + switch (splitByDots.length) { + case 1: + return new DafnyVersion( + Integer.parseInt(splitByDots[0]), + 0, + 0, + suffix); + case 2: + return new DafnyVersion( + Integer.parseInt(splitByDots[0]), + Integer.parseInt(splitByDots[1]), + 0, + suffix); + case 3: + return new DafnyVersion( + Integer.parseInt(splitByDots[0]), + Integer.parseInt(splitByDots[1]), + Integer.parseInt(splitByDots[2]), + suffix); + default: + throw new IllegalArgumentException(); + } + } + + public DafnyVersion(int major, int minor, int patch) { + this(major, minor, patch, null); + } + + public DafnyVersion(int major, int minor, int patch, String suffix) { + this.major = requireNonNegative(major); + this.minor = requireNonNegative(minor); + this.patch = requireNonNegative(patch); + this.suffix = suffix; + } + + private int requireNonNegative(int value) { + if (value < 0) { + throw new IllegalArgumentException(); + } + return value; + } + + @Override + public boolean equals(Object o) { + if (this == o) { + return true; + } + if (o == null || getClass() != o.getClass()) { + return false; + } + DafnyVersion that = (DafnyVersion) o; + return major == that.major + && minor == that.minor + && patch == that.patch + && Objects.equals(suffix, that.suffix); + } + + @Override + public int hashCode() { + return Objects.hash(major, minor, patch, suffix); + } + + @Override + public int compareTo(DafnyVersion other) { + int majorComparison = Integer.compare(this.major, other.major); + if (majorComparison != 0) { + return majorComparison; + } + + int minorComparison = Integer.compare(this.minor, other.minor); + if (minorComparison != 0) { + return minorComparison; + } + + int patchComparison = Integer.compare(this.patch, other.patch); + if (patchComparison != 0) { + return patchComparison; + } + + return SUFFIX_COMPARATOR.compare(this.suffix, other.suffix); + } + + @Override + public String toString() { + return "DafnyVersion{" + + "major=" + major + + ", minor=" + minor + + ", patch=" + patch + + ", suffix='" + suffix + '\'' + + '}'; + } +} diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/ToDafny.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/ToDafny.java index 705cd5c4c..18908b869 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/ToDafny.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/ToDafny.java @@ -194,13 +194,13 @@ protected CodeBlock memberAssign( isNullCheck, inputVar); } + CodeBlock typeDescriptor = subject.dafnyNameResolver.typeDescriptor(memberShape.getTarget()); return CodeBlock.of( - "$L = $L ?\n$T.create_Some($L)\n: $T.create_None()", + "$L = $L ?\n$L\n: $L", outputVar, isSetCheck, - ClassName.get("Wrappers_Compile", "Option"), - memberConversion, - ClassName.get("Wrappers_Compile", "Option") + subject.dafnyNameResolver.createSome(typeDescriptor, memberConversion), + subject.dafnyNameResolver.createNone(typeDescriptor) ); } diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/ShimV1.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/ShimV1.java index fbfe15fc9..bd80be583 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/ShimV1.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/ShimV1.java @@ -3,6 +3,7 @@ package software.amazon.polymorph.smithyjava.generator.awssdk.v1; import com.squareup.javapoet.ClassName; +import com.squareup.javapoet.CodeBlock; import com.squareup.javapoet.JavaFile; import com.squareup.javapoet.MethodSpec; import com.squareup.javapoet.TypeName; @@ -26,7 +27,6 @@ import software.amazon.smithy.model.shapes.ShapeId; import software.amazon.smithy.utils.StringUtils; -import static software.amazon.polymorph.smithyjava.nameresolver.Constants.DAFNY_RESULT_CLASS_NAME; import static software.amazon.polymorph.smithyjava.nameresolver.Constants.DAFNY_TUPLE0_CLASS_NAME; import static software.amazon.polymorph.smithyjava.nameresolver.Constants.SMITHY_API_UNIT; @@ -138,32 +138,43 @@ Optional operation(final ShapeId operationShapeId) { subject.nativeNameResolver.typeForShape(inputShapeId), StringUtils.capitalize(inputShapeId.getName())) .beginControlFlow("try"); + CodeBlock successTypeDescriptor; if (outputShapeId.equals(SMITHY_API_UNIT)) { + successTypeDescriptor = CodeBlock.of(DAFNY_TUPLE0_CLASS_NAME + "._typeDescriptor()"); builder.addStatement("_impl.$L(converted)", StringUtils.uncapitalize(operationName)) - .addStatement("return $T.create_Success($T.create())", - DAFNY_RESULT_CLASS_NAME, DAFNY_TUPLE0_CLASS_NAME); + .addStatement("return $L", + subject.dafnyNameResolver.createSuccess( + successTypeDescriptor, + CodeBlock.of("$T.create()", DAFNY_TUPLE0_CLASS_NAME))); } else { + successTypeDescriptor = subject.dafnyNameResolver.typeDescriptor(outputShapeId); builder.addStatement("$T result = _impl.$L(converted)", subject.nativeNameResolver.typeForOperationOutput(outputShapeId), StringUtils.uncapitalize(operationName)) .addStatement("$T dafnyResponse = ToDafny.$L(result)", dafnyOutput, StringUtils.capitalize(outputShapeId.getName())) - .addStatement("return $T.create_Success(dafnyResponse)", - DAFNY_RESULT_CLASS_NAME); + .addStatement("return $L", + subject.dafnyNameResolver.createSuccess( + successTypeDescriptor, + CodeBlock.of("dafnyResponse"))); } operationShape.getErrors().stream().sorted().forEach(shapeId -> builder .nextControlFlow("catch ($T ex)", subject.nativeNameResolver.typeForShape(shapeId)) - .addStatement("return $T.create_Failure(ToDafny.Error(ex))", - DAFNY_RESULT_CLASS_NAME) + .addStatement("return $L", + subject.dafnyNameResolver.createFailure( + successTypeDescriptor, + CodeBlock.of("ToDafny.Error(ex)"))) ); return Optional.of(builder .nextControlFlow("catch ($T ex)", subject.nativeNameResolver.baseErrorForService()) - .addStatement("return $T.create_Failure(ToDafny.Error(ex))", - DAFNY_RESULT_CLASS_NAME) + .addStatement("return $L", + subject.dafnyNameResolver.createFailure( + successTypeDescriptor, + CodeBlock.of("ToDafny.Error(ex)"))) .endControlFlow() .build()); } diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/ToDafnyAwsV1.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/ToDafnyAwsV1.java index 816a2e0fd..36f28c5de 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/ToDafnyAwsV1.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/ToDafnyAwsV1.java @@ -24,6 +24,7 @@ import software.amazon.polymorph.smithyjava.generator.ToDafny; import software.amazon.polymorph.smithyjava.nameresolver.Constants; +import software.amazon.polymorph.smithyjava.nameresolver.Dafny; import software.amazon.polymorph.utils.AwsSdkNameResolverHelpers; import software.amazon.polymorph.utils.DafnyNameResolverHelpers; import software.amazon.polymorph.utils.ModelUtils; @@ -346,16 +347,19 @@ MethodSpec generateConvertOpaqueError() { ); // This is memberAssignment from above, // but with calls to dafnyNameResolver replaced with their expected response. + CodeBlock stringTypeDescriptor = Dafny.TYPE_DESCRIPTOR_BY_SHAPE_TYPE.get(ShapeType.STRING); CodeBlock memberAssignment = CodeBlock.of( - "$L = $T.nonNull($L) ?\n$T.create_Some($T.$L($L))\n: $T.create_None()", + "$L = $T.nonNull($L) ?\n$T.create_Some($L, $T.$L($L))\n: $T.create_None($L)", "message", ClassName.get(Objects.class), "nativeValue.getMessage()", ClassName.get("Wrappers_Compile", "Option"), + stringTypeDescriptor, COMMON_TO_DAFNY_SIMPLE, SIMPLE_CONVERSION_METHOD_FROM_SHAPE_TYPE.get(ShapeType.STRING).methodName(), "nativeValue.getMessage()", - ClassName.get("Wrappers_Compile", "Option") + ClassName.get("Wrappers_Compile", "Option"), + stringTypeDescriptor ); return MethodSpec.methodBuilder("Error") .addModifiers(Modifier.PUBLIC, Modifier.STATIC) diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/JavaAwsSdkV2.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/JavaAwsSdkV2.java index 28e45b6a2..99308f814 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/JavaAwsSdkV2.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/JavaAwsSdkV2.java @@ -8,6 +8,7 @@ import java.util.HashMap; import java.util.Map; +import software.amazon.polymorph.smithydafny.DafnyVersion; import software.amazon.polymorph.smithyjava.MethodReference; import software.amazon.polymorph.smithyjava.generator.CodegenSubject; import software.amazon.polymorph.utils.TokenTree; @@ -47,8 +48,8 @@ private JavaAwsSdkV2( this.packageName = dafnyNameResolver.packageName(); } - public static JavaAwsSdkV2 createJavaAwsSdkV2(ServiceShape serviceShape, Model model) { - final AwsSdkDafnyV2 dafnyNameResolver = new AwsSdkDafnyV2(serviceShape, model); + public static JavaAwsSdkV2 createJavaAwsSdkV2(ServiceShape serviceShape, Model model, DafnyVersion dafnyVersion) { + final AwsSdkDafnyV2 dafnyNameResolver = new AwsSdkDafnyV2(serviceShape, model, dafnyVersion); final AwsSdkNativeV2 nativeNameResolver = new AwsSdkNativeV2(serviceShape, model); return new JavaAwsSdkV2(serviceShape, model, dafnyNameResolver, nativeNameResolver); } diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ShimV2.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ShimV2.java index 26cd5f267..577ab5a9b 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ShimV2.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ShimV2.java @@ -3,6 +3,7 @@ package software.amazon.polymorph.smithyjava.generator.awssdk.v2; import com.squareup.javapoet.ClassName; +import com.squareup.javapoet.CodeBlock; import com.squareup.javapoet.JavaFile; import com.squareup.javapoet.MethodSpec; import com.squareup.javapoet.TypeName; @@ -26,7 +27,6 @@ import software.amazon.smithy.model.shapes.ShapeId; import software.amazon.smithy.utils.StringUtils; -import static software.amazon.polymorph.smithyjava.nameresolver.Constants.DAFNY_RESULT_CLASS_NAME; import static software.amazon.polymorph.smithyjava.nameresolver.Constants.DAFNY_TUPLE0_CLASS_NAME; import static software.amazon.polymorph.smithyjava.nameresolver.Constants.SMITHY_API_UNIT; @@ -138,20 +138,27 @@ Optional operation(final ShapeId operationShapeId) { subject.nativeNameResolver.typeForShape(inputShapeId), StringUtils.capitalize(inputShapeId.getName())) .beginControlFlow("try"); + CodeBlock successTypeDescriptor; if (outputShapeId.equals(SMITHY_API_UNIT)) { + successTypeDescriptor = CodeBlock.of(DAFNY_TUPLE0_CLASS_NAME + "._typeDescriptor()"); builder.addStatement("_impl.$L(converted)", StringUtils.uncapitalize(operationName)) - .addStatement("return $T.create_Success($T.create())", - DAFNY_RESULT_CLASS_NAME, DAFNY_TUPLE0_CLASS_NAME); + .addStatement("return $L", + subject.dafnyNameResolver.createSuccess( + successTypeDescriptor, + CodeBlock.of("$T.create()", DAFNY_TUPLE0_CLASS_NAME))); } else { + successTypeDescriptor = subject.dafnyNameResolver.typeDescriptor(outputShapeId); builder.addStatement("$T result = _impl.$L(converted)", subject.nativeNameResolver.typeForOperationOutput(outputShapeId), StringUtils.uncapitalize(operationName)) .addStatement("$T dafnyResponse = ToDafny.$L(result)", dafnyOutput, StringUtils.capitalize(outputShapeId.getName())) - .addStatement("return $T.create_Success(dafnyResponse)", - DAFNY_RESULT_CLASS_NAME); + .addStatement("return $L", + subject.dafnyNameResolver.createSuccess( + successTypeDescriptor, + CodeBlock.of("dafnyResponse"))); } operationShape.getErrors().stream().sorted().forEach(shapeId -> { @@ -164,13 +171,17 @@ Optional operation(final ShapeId operationShapeId) { builder .nextControlFlow("catch ($T ex)", subject.nativeNameResolver.typeForShape(shapeId)) - .addStatement("return $T.create_Failure(ToDafny.Error(ex))", - DAFNY_RESULT_CLASS_NAME); + .addStatement("return $L", + subject.dafnyNameResolver.createFailure( + successTypeDescriptor, + CodeBlock.of("ToDafny.Error(ex)"))); }); return Optional.of(builder .nextControlFlow("catch ($T ex)", subject.nativeNameResolver.baseErrorForService()) - .addStatement("return $T.create_Failure(ToDafny.Error(ex))", - DAFNY_RESULT_CLASS_NAME) + .addStatement("return $L", + subject.dafnyNameResolver.createFailure( + successTypeDescriptor, + CodeBlock.of("ToDafny.Error(ex)"))) .endControlFlow() .build()); } diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2.java index e2e24c408..1d830b5d4 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2.java @@ -520,16 +520,18 @@ MethodSpec generateConvertOpaqueError() { ); // This is memberAssignment from above, // but with calls to dafnyNameResolver replaced with their expected response. + CodeBlock stringTypeDescriptor = Dafny.TYPE_DESCRIPTOR_BY_SHAPE_TYPE.get(ShapeType.STRING); CodeBlock memberAssignment = CodeBlock.of( - "$L = $T.nonNull($L) ?\n$T.create_Some($T.$L($L))\n: $T.create_None()", + "$L = $T.nonNull($L) ?\n$L\n: $L", "message", ClassName.get(Objects.class), "nativeValue.getMessage()", - ClassName.get("Wrappers_Compile", "Option"), - COMMON_TO_DAFNY_SIMPLE, - SIMPLE_CONVERSION_METHOD_FROM_SHAPE_TYPE.get(ShapeType.STRING).methodName(), - "nativeValue.getMessage()", - ClassName.get("Wrappers_Compile", "Option") + subject.dafnyNameResolver.createSome(stringTypeDescriptor, + CodeBlock.of("$T.$L($L)", + COMMON_TO_DAFNY_SIMPLE, + SIMPLE_CONVERSION_METHOD_FROM_SHAPE_TYPE.get(ShapeType.STRING).methodName(), + "nativeValue.getMessage()")), + subject.dafnyNameResolver.createNone(stringTypeDescriptor) ); return MethodSpec.methodBuilder("Error") .addModifiers(Modifier.PUBLIC, Modifier.STATIC) diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/JavaLibrary.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/JavaLibrary.java index 4c29f856f..b3ac9a26e 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/JavaLibrary.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/JavaLibrary.java @@ -15,6 +15,7 @@ import org.slf4j.Logger; import org.slf4j.LoggerFactory; +import software.amazon.polymorph.smithydafny.DafnyVersion; import software.amazon.polymorph.smithyjava.NamespaceHelper; import software.amazon.polymorph.smithyjava.generator.CodegenSubject; import software.amazon.polymorph.smithyjava.generator.Generator; @@ -61,8 +62,8 @@ public class JavaLibrary extends CodegenSubject { public final ToDafnyLibrary toDafnyLibrary; public final ToNativeLibrary toNativeLibrary; - public JavaLibrary(Model model, ServiceShape serviceShape, AwsSdkVersion sdkVersion) { - super(model, serviceShape, initDafny(model, serviceShape, sdkVersion), initNative(model, serviceShape, sdkVersion), sdkVersion); + public JavaLibrary(Model model, ServiceShape serviceShape, AwsSdkVersion sdkVersion, DafnyVersion dafnyVersion) { + super(model, serviceShape, initDafny(model, serviceShape, sdkVersion, dafnyVersion), initNative(model, serviceShape, sdkVersion), sdkVersion); packageName = NamespaceHelper.standardize(serviceShape.getId().getNamespace()); modelPackageName = packageName + ".model"; try { @@ -77,9 +78,9 @@ public JavaLibrary(Model model, ServiceShape serviceShape, AwsSdkVersion sdkVers toNativeLibrary = new ToNativeLibrary(this); } - static Dafny initDafny(Model model, ServiceShape serviceShape, AwsSdkVersion awsSdkVersion) { + static Dafny initDafny(Model model, ServiceShape serviceShape, AwsSdkVersion awsSdkVersion, DafnyVersion dafnyVersion) { String packageName = DafnyNameResolverHelpers.packageNameForNamespace(serviceShape.getId().getNamespace()); - return new Dafny(packageName, model, serviceShape, awsSdkVersion); + return new Dafny(packageName, model, serviceShape, awsSdkVersion, dafnyVersion); } static Native initNative(Model model, ServiceShape serviceShape, AwsSdkVersion awsSdkVersion) { diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/TestJavaLibrary.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/TestJavaLibrary.java index d2926fc38..afe33cd25 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/TestJavaLibrary.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/TestJavaLibrary.java @@ -9,6 +9,7 @@ import org.slf4j.Logger; import org.slf4j.LoggerFactory; +import software.amazon.polymorph.smithydafny.DafnyVersion; import software.amazon.polymorph.smithyjava.generator.library.shims.TestServiceShim; import software.amazon.polymorph.utils.TokenTree; @@ -19,8 +20,8 @@ public class TestJavaLibrary extends JavaLibrary { @SuppressWarnings("unused") private static final Logger LOGGER = LoggerFactory.getLogger(TestJavaLibrary.class); - public TestJavaLibrary(Model model, ServiceShape serviceShape, AwsSdkVersion sdkVersion) { - super(model, serviceShape, sdkVersion); + public TestJavaLibrary(Model model, ServiceShape serviceShape, AwsSdkVersion sdkVersion, DafnyVersion dafnyVersion) { + super(model, serviceShape, sdkVersion, dafnyVersion); } @Override diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/shims/ServiceShim.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/shims/ServiceShim.java index 5dcbc4738..96ef98e26 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/shims/ServiceShim.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/shims/ServiceShim.java @@ -125,7 +125,7 @@ private MethodSpec serviceConstructor(BuilderSpecs builderSpecs) { method.addStatement(dafnyDeclareAndConvert(trait.getConfigId())); // Invoke client creation // i.e.: Result result = software.amazon.cryptography.primitives.internaldafny.__default.AtomicPrimitives(dafnyValue); - TypeName success = subject.dafnyNameResolver.classNameForConcreteServiceClient(subject.serviceShape); + TypeName success = subject.dafnyNameResolver.classNameForInterface(subject.serviceShape); TypeName failure = subject.dafnyNameResolver.abstractClassForError(); TypeName result = Dafny.asDafnyResult(success, failure); method.addStatement("$T $L = $T.$L($L)", diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/Operation.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/Operation.java index 27361229f..ef75c1283 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/Operation.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/Operation.java @@ -57,27 +57,36 @@ public static MethodSpec operation( method.addStatement(declareNativeInputAndCovert(inputResolved, subject)); // Try native implementation method.beginControlFlow("try"); + CodeBlock successTypeDescriptor; if (outputResolved.resolvedId().equals(SMITHY_API_UNIT)) { // if operation is void + successTypeDescriptor = CodeBlock.of("dafny.Tuple0._typeDescriptor()"); method .addStatement(invoke(operationName)) - .addStatement("return $T.create_Success($T.create())", - DAFNY_RESULT_CLASS_NAME, DAFNY_TUPLE0_CLASS_NAME); + .addStatement("return $L", + subject.dafnyNameResolver.createSuccess( + successTypeDescriptor, + CodeBlock.of("$T.create()", DAFNY_TUPLE0_CLASS_NAME))); } else { // operation is not void + successTypeDescriptor = subject.dafnyNameResolver.typeDescriptor(outputResolved.resolvedId()); TypeName nativeOutputType = preferNativeInterface(outputResolved, subject); method .addStatement(declareNativeOutputAndInvoke(operationName, nativeOutputType)) .addStatement(declareDafnyOutputAndConvert(outputResolved, subject)) - .addStatement("return $T.create_Success($L)", - DAFNY_RESULT_CLASS_NAME, DAFNY_OUTPUT); + .addStatement("return $L", + subject.dafnyNameResolver.createSuccess( + successTypeDescriptor, + CodeBlock.of(DAFNY_OUTPUT))); } // catch Errors in this Namespace method .nextControlFlow("catch ($T ex)", ClassName.get(RuntimeException.class)) - .addStatement("return $T.create_Failure($T.Error(ex))", - DAFNY_RESULT_CLASS_NAME, shimLibrary.toDafnyClassName) + .addStatement("return $L", + subject.dafnyNameResolver.createFailure( + successTypeDescriptor, + CodeBlock.of("$T.Error(ex)", shimLibrary.toDafnyClassName))) .endControlFlow(); return method.build(); } diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/AwsSdkDafnyV1.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/AwsSdkDafnyV1.java index e1bdfa790..d71a7edbe 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/AwsSdkDafnyV1.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/AwsSdkDafnyV1.java @@ -4,6 +4,7 @@ import com.squareup.javapoet.ClassName; +import software.amazon.polymorph.smithydafny.DafnyVersion; import software.amazon.polymorph.smithyjava.generator.CodegenSubject; import software.amazon.polymorph.utils.AwsSdkNameResolverHelpers; import software.amazon.polymorph.utils.DafnyNameResolverHelpers; @@ -18,8 +19,8 @@ public class AwsSdkDafnyV1 extends Dafny { - public AwsSdkDafnyV1(ServiceShape serviceShape, Model model) { - super(packageNameForServiceShape(serviceShape), model, serviceShape, CodegenSubject.AwsSdkVersion.V1); + public AwsSdkDafnyV1(ServiceShape serviceShape, Model model, DafnyVersion dafnyVersion) { + super(packageNameForServiceShape(serviceShape), model, serviceShape, CodegenSubject.AwsSdkVersion.V1, dafnyVersion); } @Override diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/AwsSdkDafnyV2.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/AwsSdkDafnyV2.java index 496ddbc16..72c57fe0e 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/AwsSdkDafnyV2.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/AwsSdkDafnyV2.java @@ -9,6 +9,7 @@ import com.squareup.javapoet.TypeName; import software.amazon.polymorph.smithydafny.DafnyNameResolver; +import software.amazon.polymorph.smithydafny.DafnyVersion; import software.amazon.polymorph.smithyjava.generator.CodegenSubject; import software.amazon.polymorph.utils.AwsSdkNameResolverHelpers; import software.amazon.polymorph.utils.DafnyNameResolverHelpers; @@ -25,8 +26,8 @@ public class AwsSdkDafnyV2 extends Dafny { - public AwsSdkDafnyV2(ServiceShape serviceShape, Model model) { - super(packageNameForServiceShape(serviceShape), model, serviceShape, CodegenSubject.AwsSdkVersion.V2); + public AwsSdkDafnyV2(ServiceShape serviceShape, Model model, DafnyVersion dafnyVersion) { + super(packageNameForServiceShape(serviceShape), model, serviceShape, CodegenSubject.AwsSdkVersion.V2, dafnyVersion); } @Override diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Constants.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Constants.java index de79b77c8..9739abe8e 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Constants.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Constants.java @@ -11,6 +11,7 @@ public class Constants { public static final ShapeId SMITHY_API_UNIT = ShapeId.fromParts("smithy.api", "Unit"); + public static final ClassName DAFNY_OPTION_CLASS_NAME = ClassName.get("Wrappers_Compile", "Option"); public static final ClassName DAFNY_RESULT_CLASS_NAME = ClassName.get("Wrappers_Compile", "Result"); public static final ClassName DAFNY_TUPLE0_CLASS_NAME = ClassName.get("dafny", "Tuple0"); public static final ClassName DAFNY_TYPE_DESCRIPTOR_CLASS_NAME = ClassName.get("dafny", "TypeDescriptor"); diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Dafny.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Dafny.java index c80a984c7..550047a9a 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Dafny.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Dafny.java @@ -19,6 +19,7 @@ import javax.annotation.Nullable; import software.amazon.polymorph.smithydafny.DafnyNameResolver; +import software.amazon.polymorph.smithydafny.DafnyVersion; import software.amazon.polymorph.smithyjava.MethodReference; import software.amazon.polymorph.smithyjava.generator.CodegenSubject; import software.amazon.polymorph.smithyjava.generator.Generator; @@ -49,7 +50,7 @@ public class Dafny extends NameResolver { @SuppressWarnings("unused") private static final Logger LOGGER = LoggerFactory.getLogger(Dafny.class); - protected static final Map TYPE_DESCRIPTOR_BY_SHAPE_TYPE; + public static final Map TYPE_DESCRIPTOR_BY_SHAPE_TYPE; static { TYPE_DESCRIPTOR_BY_SHAPE_TYPE = Map.ofEntries( Map.entry(ShapeType.STRING, CodeBlock.of("$T._typeDescriptor($T.CHAR)", Constants.DAFNY_SEQUENCE_CLASS_NAME, Constants.DAFNY_TYPE_DESCRIPTOR_CLASS_NAME)), @@ -65,17 +66,21 @@ public class Dafny extends NameResolver { ); } + private final DafnyVersion dafnyVersion; + public Dafny( final String packageName, final Model model, final ServiceShape serviceShape, - CodegenSubject.AwsSdkVersion awsSdkVersion) { + final CodegenSubject.AwsSdkVersion awsSdkVersion, + final DafnyVersion dafnyVersion) { super( packageName, serviceShape, model, modelPackageNameForServiceShape(serviceShape), awsSdkVersion); + this.dafnyVersion = dafnyVersion; } /** @@ -92,6 +97,98 @@ public static String datatypeConstructorCreate(String name, boolean isRecordType return "create_" + DafnyNameResolverHelpers.dafnyCompilesExtra_(name); } + // Dafnys greater than or equal to this will need Type Descriptors for constructing datatypes + private static final DafnyVersion NEEDS_TYPE_DESCRIPTORS_WHEN_CONSTRUCTING_DATATYPES = new DafnyVersion(4, 2, 0); + + /** + * @return Whether the given Dafny version requires type descriptor values when instantiating datatype constructors. + */ + public static boolean datatypeConstructorsNeedTypeDescriptors(DafnyVersion dafnyVersion) { + return dafnyVersion.compareTo(NEEDS_TYPE_DESCRIPTORS_WHEN_CONSTRUCTING_DATATYPES) >= 0; + } + + private boolean datatypeConstructorsNeedTypeDescriptors() { + return datatypeConstructorsNeedTypeDescriptors(dafnyVersion); + } + + /** + * Code to create an instance of the None constructor of Wrappers.Option. + * @param typeDescriptor the code to create a TypeDescriptor for the type T, + * which is needed if datatypeConstructorsNeedTypeDescriptors() + */ + 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")); + } + } + + /** + * Code to create an instance of the Some(value: T) constructor of Wrappers.Option. + * @param typeDescriptor the code to create a TypeDescriptor for the type T, + * which is needed if datatypeConstructorsNeedTypeDescriptors() + */ + 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); + } + } + + /** + * Code to create an instance of the Success(value: T) constructor of Wrappers.Result. + * @param valueTypeDescriptor the code to create a TypeDescriptor for the type T, + * which is needed if datatypeConstructorsNeedTypeDescriptors() + */ + 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); + } + } + + /** + * Code to create an instance of the Failure(error: Error) constructor of Wrappers.Result. + * @param valueTypeDescriptor the code to create a TypeDescriptor for the type T, + * which is needed if datatypeConstructorsNeedTypeDescriptors() + */ + public CodeBlock createFailure(CodeBlock valueTypeDescriptor, CodeBlock error) { + if (datatypeConstructorsNeedTypeDescriptors()) { + return CodeBlock.of( + "$T.create_Failure($L, Error._typeDescriptor(), $L)", + Constants.DAFNY_RESULT_CLASS_NAME, + valueTypeDescriptor, + error); + } else { + return CodeBlock.of( + "$T.create_Failure($L)", + Constants.DAFNY_RESULT_CLASS_NAME, + error); + } + } + public static String datatypeConstructorIs(String name) { String dafnyEnumName = DafnyNameResolverHelpers.dafnyCompilesExtra_(name); return "is_" + dafnyEnumName; @@ -146,6 +243,13 @@ public static TypeName asDafnyResult(TypeName success, TypeName failure) { ); } + public static TypeName asDafnyOption(TypeName value) { + return ParameterizedTypeName.get( + Constants.DAFNY_OPTION_CLASS_NAME, + value + ); + } + public String packageName() { return this.packageName; } @@ -239,7 +343,7 @@ public CodeBlock typeDescriptor(ShapeId shapeId) { return CodeBlock.of("$L()", new MethodReference(abstractClassForError(), "_typeDescriptor").asNormalReference()); } - if (shape.hasTrait(ReferenceTrait.class)) { + if (shape.hasTrait(ReferenceTrait.class) || shape.isServiceShape()) { // It is safe to use typeForShape here, as ReferenceTrait will always turn into a Resource or Service TypeName interfaceClassName = typeForShape(shapeId); return CodeBlock.of("$T.reference($T.class)", Constants.DAFNY_TYPE_DESCRIPTOR_CLASS_NAME, interfaceClassName); @@ -259,6 +363,19 @@ public CodeBlock typeDescriptor(ShapeId shapeId) { return CodeBlock.of("$L", typeDescriptor); } } + if (shape.getType().isShapeType(ShapeType.LIST)) { + CodeBlock elementTypeDescriptor = typeDescriptor(shape.asListShape().get().getMember().getTarget()); + return CodeBlock.of("$T._typeDescriptor($L)", Constants.DAFNY_SEQUENCE_CLASS_NAME, elementTypeDescriptor); + } + if (shape.getType().isShapeType(ShapeType.SET)) { + CodeBlock elementTypeDescriptor = typeDescriptor(shape.asSetShape().get().getMember().getTarget()); + return CodeBlock.of("$T._typeDescriptor($L)", Constants.DAFNY_SET_CLASS_NAME, elementTypeDescriptor); + } + if (shape.getType().isShapeType(ShapeType.MAP)) { + CodeBlock keyTypeDescriptor = typeDescriptor(shape.asMapShape().get().getKey().getTarget()); + CodeBlock valueTypeDescriptor = typeDescriptor(shape.asMapShape().get().getValue().getTarget()); + return CodeBlock.of("$T._typeDescriptor($L, $L)", Constants.DAFNY_MAP_CLASS_NAME, keyTypeDescriptor, valueTypeDescriptor); + } return CodeBlock.of("$L()", new MethodReference(classForNotErrorNotUnitShape(shape), "_typeDescriptor").asNormalReference()); } @@ -304,7 +421,7 @@ TypeName typeForString(StringShape shape) { return typeForCharacterSequence(); } - TypeName typeForCharacterSequence() { + TypeName typeForCharacterSequence() { return ParameterizedTypeName.get( Constants.DAFNY_SEQUENCE_CLASS_NAME, WildcardTypeName.subtypeOf(Character.class) diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/smithy/dafny/codegen/DafnyClientCodegenEdition.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/smithy/dafny/codegen/DafnyClientCodegenEdition.java index 5cb4dd0f6..a38214176 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/smithy/dafny/codegen/DafnyClientCodegenEdition.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/smithy/dafny/codegen/DafnyClientCodegenEdition.java @@ -6,7 +6,8 @@ public enum DafnyClientCodegenEdition { // Java identifiers (including enum values) cannot start with a number, but edition names are typically numeric. - EDITION_2023; + EDITION_2023, + EDITION_2023_10; // 2023.10 /** * Returns the enum value corresponding to the given numeric string, e.g. "2023". @@ -15,6 +16,6 @@ public enum DafnyClientCodegenEdition { */ public static DafnyClientCodegenEdition fromNumeric(final String edition) { Objects.requireNonNull(edition); - return DafnyClientCodegenEdition.valueOf("EDITION_" + edition); + return DafnyClientCodegenEdition.valueOf("EDITION_" + edition.replace(".", "_")); } } diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/smithy/dafny/codegen/DafnyClientCodegenPluginSettings.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/smithy/dafny/codegen/DafnyClientCodegenPluginSettings.java index 92b85a11b..de57e4f24 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/smithy/dafny/codegen/DafnyClientCodegenPluginSettings.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/smithy/dafny/codegen/DafnyClientCodegenPluginSettings.java @@ -5,7 +5,9 @@ import org.slf4j.Logger; import org.slf4j.LoggerFactory; import software.amazon.polymorph.CodegenEngine; +import software.amazon.polymorph.smithydafny.DafnyVersion; import software.amazon.smithy.build.FileManifest; +import software.amazon.smithy.model.node.Node; import software.amazon.smithy.model.node.ObjectNode; import software.amazon.smithy.model.node.StringNode; import software.amazon.smithy.model.shapes.ShapeId; @@ -52,16 +54,27 @@ class DafnyClientCodegenPluginSettings { */ public final Path includeDafnyFile; + /** + * The Dafny version to generate code compatible with. + * This is used to ensure both Dafny source compatibility + * and compatibility with the Dafny compiler and runtime internals, + * which shim code generation currently depends on. + * Required when the edition is 2023.10 or later. + */ + public final DafnyVersion dafnyVersion; + private DafnyClientCodegenPluginSettings( final DafnyClientCodegenEdition edition, final ShapeId serviceId, final Set targetLanguages, - final Path includeDafnyFile + final Path includeDafnyFile, + final DafnyVersion dafnyVersion ) { this.edition = edition; this.serviceId = serviceId; this.targetLanguages = targetLanguages; this.includeDafnyFile = includeDafnyFile; + this.dafnyVersion = dafnyVersion; } static Optional fromObject(final ObjectNode node, final FileManifest manifest) { @@ -107,8 +120,17 @@ static Optional fromObject(final ObjectNode no includeDafnyFileNormalized); } + final String dafnyVersionString; + if (edition.ordinal() >= DafnyClientCodegenEdition.EDITION_2023_10.ordinal()) { + // Required from this edition on + dafnyVersionString = node.expectStringMember("dafnyVersion").getValue(); + } else { + dafnyVersionString = node.getStringMemberOrDefault("dafnyVersion", "4.1"); + } + return Optional.of( - new DafnyClientCodegenPluginSettings(edition, serviceId, targetLanguages, includeDafnyFileNormalized)); + new DafnyClientCodegenPluginSettings(edition, serviceId, targetLanguages, includeDafnyFileNormalized, + DafnyVersion.parse(dafnyVersionString))); } /** diff --git a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithydafny/DafnyVersionCompareToTest.java b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithydafny/DafnyVersionCompareToTest.java new file mode 100644 index 000000000..c99e7fa03 --- /dev/null +++ b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithydafny/DafnyVersionCompareToTest.java @@ -0,0 +1,52 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +package software.amazon.polymorph.smithydafny; + +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; + +import java.util.Arrays; +import java.util.Collection; + +import static org.junit.Assert.assertEquals; + +@RunWith(Parameterized.class) +public class DafnyVersionCompareToTest { + + @Parameterized.Parameters(name = "{0} compareTo {1} == {2}") + public static Collection data() { + return Arrays.asList(new Object[][] { + { "4.1", "4", 1 }, + { "4.0", "4", 0 }, + { "4", "4.0.0", 0 }, + { "4.1.3", "4", 1 }, + { "3.11", "4", -1 }, + { "4.1", "4", 1 }, + { "4.1.1", "4.1.2", -1 }, + { "4.1.1", "4.1.1", 0 }, + { "4.1.2", "4.1.1", 1 }, + { "4-alpha", "4", -1 }, + { "4-alpha", "4.0", -1 }, + { "4-alpha", "4-alpha", 0 }, + { "4-alpha", "4-beta", -1 }, + }); + } + + public DafnyVersionCompareToTest(String lhs, String rhs, int expected) { + this.lhs = lhs; + this.rhs = rhs; + this.expected = expected; + } + + private final String lhs; + private final String rhs; + private final int expected; + + @Test + public void testCompareTo() { + DafnyVersion left = DafnyVersion.parse(lhs); + DafnyVersion right = DafnyVersion.parse(rhs); + assertEquals(expected, left.compareTo(right)); + } +} diff --git a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithydafny/DafnyVersionParsingTest.java b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithydafny/DafnyVersionParsingTest.java new file mode 100644 index 000000000..80be8805d --- /dev/null +++ b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithydafny/DafnyVersionParsingTest.java @@ -0,0 +1,54 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +package software.amazon.polymorph.smithydafny; + +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import software.amazon.polymorph.smithyjava.nameresolver.Dafny; + +import java.util.Arrays; +import java.util.Collection; + +import static org.junit.Assert.assertEquals; + +@RunWith(Parameterized.class) +public class DafnyVersionParsingTest { + + public DafnyVersionParsingTest(String versionString, DafnyVersion expected) { + this.versionString = versionString; + this.expected = expected; + } + + @Parameterized.Parameters(name = "{0} ==> {1}") + public static Collection data() { + return Arrays.asList(new Object[][] { + // Valid + { "4", new DafnyVersion(4, 0, 0) }, + { "4.1", new DafnyVersion(4, 1, 0) }, + { "4.1.4", new DafnyVersion(4, 1, 4) }, + { "4-almost", new DafnyVersion(4, 0, 0, "almost") }, + { "4.1-beta", new DafnyVersion(4, 1, 0, "beta") }, + { "4.1.4-any-day-now", new DafnyVersion(4, 1, 4, "any-day-now") }, + // Invalid + { "", null }, + { "$@%!", null }, + { "1.2.3.4", null }, + { "not.even.numbers", null } + }); + } + + private final String versionString; + private final DafnyVersion expected; + + @Test + public void testParsing() { + try { + DafnyVersion parsed = DafnyVersion.parse(versionString); + assertEquals(expected, parsed); + } catch (IllegalArgumentException e) { + assertEquals(null, expected); + } + + } +} diff --git a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/ForEachDafnyTest.java b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/ForEachDafnyTest.java new file mode 100644 index 000000000..37021333f --- /dev/null +++ b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/ForEachDafnyTest.java @@ -0,0 +1,22 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +package software.amazon.polymorph.smithyjava; + +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import software.amazon.polymorph.smithydafny.DafnyVersion; + +import java.util.Arrays; +import java.util.Collection; + +@RunWith(Parameterized.class) +public abstract class ForEachDafnyTest { + + @Parameterized.Parameters(name = "dafnyVersion = {0}") + public static Collection dafnies() { + return Arrays.asList(new Object[][] { + { new DafnyVersion(4, 1, 0) }, + { new DafnyVersion(4, 3, 0) }, + }); + } +} diff --git a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/TestSetupUtils.java b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/TestSetupUtils.java index a9f1a0632..457db6056 100644 --- a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/TestSetupUtils.java +++ b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/TestSetupUtils.java @@ -4,6 +4,7 @@ import java.util.function.BiConsumer; +import software.amazon.polymorph.smithydafny.DafnyVersion; import software.amazon.polymorph.smithyjava.generator.awssdk.v1.JavaAwsSdkV1; import software.amazon.polymorph.smithyjava.generator.awssdk.v2.JavaAwsSdkV2; import software.amazon.polymorph.smithyjava.generator.CodegenSubject; @@ -32,13 +33,13 @@ public static JavaAwsSdkV1 setupAwsSdkV1(Model localModel, String awsName) { localModel, namespaceForService(awsName)); return JavaAwsSdkV1.createJavaAwsSdkV1(serviceShape, localModel); } - public static JavaAwsSdkV2 setupAwsSdkV2(Model localModel, String awsName) { + public static JavaAwsSdkV2 setupAwsSdkV2(Model localModel, String awsName, DafnyVersion dafnyVersion) { ServiceShape serviceShape = serviceFromNamespace( localModel, namespaceForService(awsName)); - return JavaAwsSdkV2.createJavaAwsSdkV2(serviceShape, localModel); + return JavaAwsSdkV2.createJavaAwsSdkV2(serviceShape, localModel, dafnyVersion); } - public static JavaLibrary setupLibrary(Model localModel, String namespace) { + public static JavaLibrary setupLibrary(Model localModel, String namespace, DafnyVersion dafnyVersion) { ServiceShape serviceShape = serviceFromNamespace(localModel, namespace); - return new JavaLibrary(localModel, serviceShape, CodegenSubject.AwsSdkVersion.V1); + return new JavaLibrary(localModel, serviceShape, CodegenSubject.AwsSdkVersion.V1, dafnyVersion); } } diff --git a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/Constants.java b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/Constants.java index bdd7f39b1..74c15969a 100644 --- a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/Constants.java +++ b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/Constants.java @@ -2,6 +2,9 @@ // SPDX-License-Identifier: Apache-2.0 package software.amazon.polymorph.smithyjava.generator.awssdk.v2; +import software.amazon.polymorph.smithydafny.DafnyVersion; +import software.amazon.polymorph.smithyjava.nameresolver.Dafny; + public class Constants { static String DoSomethingOperation = """ @Override @@ -19,6 +22,27 @@ public Result DoSomething(DoSomethingRequest input) } """; + static String DoSomethingOperationWithTypeDescriptors = """ + @Override + public Result DoSomething(DoSomethingRequest input) { + software.amazon.awssdk.services.kms.model.DoSomethingRequest converted = ToNative.DoSomethingRequest(input); + try { + software.amazon.awssdk.services.kms.model.DoSomethingResponse result = _impl.doSomething(converted); + DoSomethingResponse dafnyResponse = ToDafny.DoSomethingResponse(result); + return Result.create_Success(DoSomethingResponse._typeDescriptor(), Error._typeDescriptor(), dafnyResponse); + } catch (DependencyTimeoutException ex) { + return Result.create_Failure(DoSomethingResponse._typeDescriptor(), Error._typeDescriptor(), ToDafny.Error(ex)); + } catch (KmsException ex) { + return Result.create_Failure(DoSomethingResponse._typeDescriptor(), Error._typeDescriptor(), ToDafny.Error(ex)); + } + } + """; + + static String DoSomethingOperation(DafnyVersion dafnyVersion) { + return Dafny.datatypeConstructorsNeedTypeDescriptors(dafnyVersion) ? + DoSomethingOperationWithTypeDescriptors : DoSomethingOperation; + } + static String DoVoidOperation = """ @Override public Result DoVoid(DoVoidRequest input) { @@ -34,43 +58,106 @@ public Result DoVoid(DoVoidRequest input) { } """; - static String MockKmsShim = """ - package software.amazon.cryptography.services.kms.internaldafny; - - import Wrappers_Compile.Result; - import dafny.Tuple0; - import java.lang.Override; - import java.lang.String; - import software.amazon.awssdk.services.kms.KmsClient; - import software.amazon.awssdk.services.kms.model.DependencyTimeoutException; - import software.amazon.awssdk.services.kms.model.KmsException; - import software.amazon.cryptography.services.kms.internaldafny.types.DoSomethingRequest; - import software.amazon.cryptography.services.kms.internaldafny.types.DoSomethingResponse; - import software.amazon.cryptography.services.kms.internaldafny.types.DoVoidRequest; - import software.amazon.cryptography.services.kms.internaldafny.types.Error; - import software.amazon.cryptography.services.kms.internaldafny.types.IKeyManagementServiceClient; - - public class Shim implements IKeyManagementServiceClient { - private final KmsClient _impl; - - private final String region; - - public Shim(final KmsClient impl, final String region) { - this._impl = impl; - this.region = region; - } - - public KmsClient impl() { - return this._impl; - } - - public String region() { - return this.region; + static String DoVoidOperationWithTypeDescriptors = """ + @Override + public Result DoVoid(DoVoidRequest input) { + software.amazon.awssdk.services.kms.model.DoVoidRequest converted = ToNative.DoVoidRequest(input); + try { + _impl.doVoid(converted); + return Result.create_Success(dafny.Tuple0._typeDescriptor(), Error._typeDescriptor(), Tuple0.create()); + } catch (DependencyTimeoutException ex) { + return Result.create_Failure(dafny.Tuple0._typeDescriptor(), Error._typeDescriptor(), ToDafny.Error(ex)); + } catch (KmsException ex) { + return Result.create_Failure(dafny.Tuple0._typeDescriptor(), Error._typeDescriptor(), ToDafny.Error(ex)); + } } - - %s - %s - } - """.formatted(DoSomethingOperation, DoVoidOperation); + """; + + static String DoVoidOperation(DafnyVersion dafnyVersion) { + return Dafny.datatypeConstructorsNeedTypeDescriptors(dafnyVersion) ? + DoVoidOperationWithTypeDescriptors : DoVoidOperation; + } + + static String MockKmsShim = """ + package software.amazon.cryptography.services.kms.internaldafny; + + import Wrappers_Compile.Result; + import dafny.Tuple0; + import java.lang.Override; + import java.lang.String; + import software.amazon.awssdk.services.kms.KmsClient; + import software.amazon.awssdk.services.kms.model.DependencyTimeoutException; + import software.amazon.awssdk.services.kms.model.KmsException; + import software.amazon.cryptography.services.kms.internaldafny.types.DoSomethingRequest; + import software.amazon.cryptography.services.kms.internaldafny.types.DoSomethingResponse; + import software.amazon.cryptography.services.kms.internaldafny.types.DoVoidRequest; + import software.amazon.cryptography.services.kms.internaldafny.types.Error; + import software.amazon.cryptography.services.kms.internaldafny.types.IKeyManagementServiceClient; + + public class Shim implements IKeyManagementServiceClient { + private final KmsClient _impl; + + private final String region; + + public Shim(final KmsClient impl, final String region) { + this._impl = impl; + this.region = region; + } + + public KmsClient impl() { + return this._impl; + } + + public String region() { + return this.region; + } + + %s + %s + } + """.formatted(DoSomethingOperation, DoVoidOperation); + + static String MockKmsShimWithTypeDescriptors = """ + package software.amazon.cryptography.services.kms.internaldafny; + + import Wrappers_Compile.Result; + import dafny.Tuple0; + import java.lang.Override; + import java.lang.String; + import software.amazon.awssdk.services.kms.KmsClient; + import software.amazon.awssdk.services.kms.model.DependencyTimeoutException; + import software.amazon.awssdk.services.kms.model.KmsException; + import software.amazon.cryptography.services.kms.internaldafny.types.DoSomethingRequest; + import software.amazon.cryptography.services.kms.internaldafny.types.DoSomethingResponse; + import software.amazon.cryptography.services.kms.internaldafny.types.DoVoidRequest; + import software.amazon.cryptography.services.kms.internaldafny.types.Error; + import software.amazon.cryptography.services.kms.internaldafny.types.IKeyManagementServiceClient; + + public class Shim implements IKeyManagementServiceClient { + private final KmsClient _impl; + + private final String region; + + public Shim(final KmsClient impl, final String region) { + this._impl = impl; + this.region = region; + } + + public KmsClient impl() { + return this._impl; + } + + public String region() { + return this.region; + } + + %s + %s + } + """.formatted(DoSomethingOperationWithTypeDescriptors, DoVoidOperationWithTypeDescriptors); + static String MockKmsShim(DafnyVersion dafnyVersion) { + return Dafny.datatypeConstructorsNeedTypeDescriptors(dafnyVersion) ? + MockKmsShimWithTypeDescriptors : MockKmsShim; + } } diff --git a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ShimTest.java b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ShimTest.java index 2b674170e..e5185f10a 100644 --- a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ShimTest.java +++ b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ShimTest.java @@ -14,6 +14,10 @@ import javax.lang.model.element.Modifier; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import software.amazon.polymorph.smithydafny.DafnyVersion; +import software.amazon.polymorph.smithyjava.ForEachDafnyTest; import software.amazon.polymorph.smithyjava.ModelConstants; import software.amazon.polymorph.smithyjava.generator.awssdk.TestSetupUtils; import software.amazon.polymorph.util.Tokenizer; @@ -27,15 +31,16 @@ import static software.amazon.polymorph.smithyjava.generator.awssdk.v2.Constants.DoVoidOperation; import static software.amazon.polymorph.smithyjava.generator.awssdk.v2.Constants.MockKmsShim; -public class ShimTest { +public class ShimTest extends ForEachDafnyTest { protected ShimV2 underTest; protected Model model; protected JavaAwsSdkV2 subject; + protected final DafnyVersion dafnyVersion; - @Before - public void setup() { + public ShimTest(DafnyVersion dafnyVersion) { + this.dafnyVersion = dafnyVersion; model = TestSetupUtils.setupLocalModel(ModelConstants.MOCK_KMS); - subject = TestSetupUtils.setupAwsSdkV2(model, "kms"); + subject = TestSetupUtils.setupAwsSdkV2(model, "kms", dafnyVersion); underTest = new ShimV2(subject); } @@ -67,9 +72,9 @@ public void operation() { Expected: %s""").formatted( - actualString, DoSomethingOperation + actualString, DoSomethingOperation(dafnyVersion) ), - actualString.contains(DoSomethingOperation) + actualString.contains(DoSomethingOperation(dafnyVersion)) ); } @@ -101,9 +106,9 @@ public void operationVoid() { Expected: %s""").formatted( - actualString, DoVoidOperation + actualString, DoVoidOperation(dafnyVersion) ), - actualString.contains(DoVoidOperation) + actualString.contains(DoVoidOperation(dafnyVersion)) ); } @@ -117,8 +122,7 @@ public void generate() { final Path actualPath = actual.keySet().toArray(temp)[0]; assertEquals(expectedPath, actualPath); final String actualSource = actual.get(actualPath).toString(); - System.out.println(actualSource); - System.out.print(MockKmsShim); - Tokenizer.tokenizeAndAssertEqual(MockKmsShim, actualSource); + final String mockKmsShim = MockKmsShim(dafnyVersion); + Tokenizer.tokenizeAndAssertEqual(mockKmsShim, actualSource); } } diff --git a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2Constants.java b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2Constants.java index 25db5d140..8fcc67b2d 100644 --- a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2Constants.java +++ b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2Constants.java @@ -108,6 +108,18 @@ public static software.amazon.cryptography.services.kms.internaldafny.types.Erro } """; + protected static String GENERATE_CONVERT_OPAQUE_ERROR_WITH_TYPE_DESCRIPTORS = """ + public static software.amazon.cryptography.services.kms.internaldafny.types.Error Error( + software.amazon.awssdk.services.kms.model.KmsException nativeValue + ) { + Wrappers_Compile.Option> message; + message = java.util.Objects.nonNull(nativeValue.getMessage()) ? + Wrappers_Compile.Option.create_Some(dafny.DafnySequence._typeDescriptor(dafny.TypeDescriptor.CHAR), software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(nativeValue.getMessage())) + : Wrappers_Compile.Option.create_None(dafny.DafnySequence._typeDescriptor(dafny.TypeDescriptor.CHAR)); + return new software.amazon.cryptography.services.kms.internaldafny.types.Error_Opaque(message); + } + """; + protected static final String KMS_A_STRING_OPERATION_JAVA_FILE = """ package software.amazon.cryptography.services.kms.internaldafny; diff --git a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2Test.java b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2Test.java index 63f97ab54..47b5dda3d 100644 --- a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2Test.java +++ b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2Test.java @@ -10,8 +10,11 @@ import java.nio.file.Path; import java.util.Map; +import software.amazon.polymorph.smithydafny.DafnyVersion; +import software.amazon.polymorph.smithyjava.ForEachDafnyTest; import software.amazon.polymorph.smithyjava.ModelConstants; import software.amazon.polymorph.smithyjava.generator.awssdk.TestSetupUtils; +import software.amazon.polymorph.smithyjava.nameresolver.Dafny; import software.amazon.polymorph.utils.TokenTree; import software.amazon.smithy.model.Model; import software.amazon.smithy.model.shapes.ShapeId; @@ -21,14 +24,15 @@ import static org.junit.Assert.assertThrows; import static software.amazon.polymorph.util.Tokenizer.tokenizeAndAssertEqual; -public class ToDafnyAwsV2Test { - protected ToDafnyAwsV2 underTest; - protected Model model; +public class ToDafnyAwsV2Test extends ForEachDafnyTest { + protected final ToDafnyAwsV2 underTest; + protected final Model model; + protected final DafnyVersion dafnyVersion; - @Before - public void setup() { + public ToDafnyAwsV2Test(DafnyVersion dafnyVersion) { + this.dafnyVersion = dafnyVersion; model = TestSetupUtils.setupTwoLocalModel(ModelConstants.KMS_KITCHEN, ModelConstants.OTHER_NAMESPACE); - underTest = new ToDafnyAwsV2(TestSetupUtils.setupAwsSdkV2(model, "kms")); + underTest = new ToDafnyAwsV2(TestSetupUtils.setupAwsSdkV2(model, "kms", dafnyVersion)); } @Test @@ -74,13 +78,16 @@ public void generateConvert() { @Test public void generateConvertOpaqueError() { - tokenizeAndAssertEqual(ToDafnyAwsV2Constants.GENERATE_CONVERT_OPAQUE_ERROR, underTest.generateConvertOpaqueError().toString()); + final String expected = Dafny.datatypeConstructorsNeedTypeDescriptors(dafnyVersion) ? + ToDafnyAwsV2Constants.GENERATE_CONVERT_OPAQUE_ERROR_WITH_TYPE_DESCRIPTORS + : ToDafnyAwsV2Constants.GENERATE_CONVERT_OPAQUE_ERROR; + tokenizeAndAssertEqual(expected, underTest.generateConvertOpaqueError().toString()); } @Test public void generate() { Model localModel = TestSetupUtils.setupLocalModel(ModelConstants.KMS_A_STRING_OPERATION); - ToDafnyAwsV2 localUnderTest = new ToDafnyAwsV2(TestSetupUtils.setupAwsSdkV2(localModel, "kms")); + ToDafnyAwsV2 localUnderTest = new ToDafnyAwsV2(TestSetupUtils.setupAwsSdkV2(localModel, "kms", dafnyVersion)); final Map actual = localUnderTest.generate(); final Path expectedPath = Path.of("software/amazon/cryptography/services/kms/internaldafny/ToDafny.java"); Path[] temp = new Path[1]; diff --git a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToNativeTest.java b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToNativeTest.java index 6d7c3ac1c..a60c073a3 100644 --- a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToNativeTest.java +++ b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToNativeTest.java @@ -10,9 +10,15 @@ import org.junit.Test; import java.nio.file.Path; +import java.util.Arrays; +import java.util.Collection; import java.util.Map; import java.util.Set; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import software.amazon.polymorph.smithydafny.DafnyVersion; +import software.amazon.polymorph.smithyjava.ForEachDafnyTest; import software.amazon.polymorph.smithyjava.MethodReference; import software.amazon.polymorph.smithyjava.ModelConstants; import software.amazon.polymorph.smithyjava.generator.awssdk.TestSetupUtils; @@ -35,7 +41,7 @@ import static software.amazon.polymorph.util.Tokenizer.tokenizeAndAssertEqual; @SuppressWarnings("OptionalGetWithoutIsPresent") -public class ToNativeTest { +public class ToNativeTest extends ForEachDafnyTest { // Why two underTests? // As we refactor ToNativeAwsV2 and abstract ToNative, // we are going to bump into permission issues in unit tests @@ -49,6 +55,7 @@ public class ToNativeTest { protected ToNativeAwsV2 underTest; protected ToNativeTestImpl underTestAbstract; protected Model model; + protected final DafnyVersion dafnyVersion; class ToNativeTestImpl extends ToNativeAwsV2 { @@ -93,11 +100,11 @@ protected CodeBlock setWithConversionCall(MemberShape member, CodeBlock getMembe } } - @Before - public void setup() { + public ToNativeTest(DafnyVersion dafnyVersion) { + this.dafnyVersion = dafnyVersion; model = TestSetupUtils.setupTwoLocalModel(ModelConstants.KMS_KITCHEN, ModelConstants.OTHER_NAMESPACE); - underTest = new ToNativeAwsV2(TestSetupUtils.setupAwsSdkV2(model, "kms")); - underTestAbstract = new ToNativeTestImpl(TestSetupUtils.setupAwsSdkV2(model, "kms")); + underTest = new ToNativeAwsV2(TestSetupUtils.setupAwsSdkV2(model, "kms", dafnyVersion)); + underTestAbstract = new ToNativeTestImpl(TestSetupUtils.setupAwsSdkV2(model, "kms", dafnyVersion)); } @Test @@ -231,7 +238,7 @@ public void generateConvert() { @Test public void generate() { Model model = TestSetupUtils.setupLocalModel(ModelConstants.KMS_A_STRING_OPERATION); - ToNativeAwsV2 underTest = new ToNativeAwsV2(TestSetupUtils.setupAwsSdkV2(model, "kms")); + ToNativeAwsV2 underTest = new ToNativeAwsV2(TestSetupUtils.setupAwsSdkV2(model, "kms", dafnyVersion)); final Map actual = underTest.generate(); final Path expectedPath = Path.of("software/amazon/cryptography/services/kms/internaldafny/ToNative.java"); Path[] temp = new Path[1]; diff --git a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/library/ModelCodegenTest.java b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/library/ModelCodegenTest.java index ac2d029ba..52c9a5342 100644 --- a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/library/ModelCodegenTest.java +++ b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/library/ModelCodegenTest.java @@ -7,6 +7,8 @@ import org.junit.Before; import org.junit.Test; +import software.amazon.polymorph.smithydafny.DafnyVersion; +import software.amazon.polymorph.smithyjava.ForEachDafnyTest; import software.amazon.polymorph.smithyjava.ModelConstants; import software.amazon.polymorph.smithyjava.generator.awssdk.TestSetupUtils; import software.amazon.smithy.model.Model; @@ -15,14 +17,13 @@ import static software.amazon.polymorph.util.Tokenizer.tokenizeAndAssertEqual; -public class ModelCodegenTest { +public class ModelCodegenTest extends ForEachDafnyTest { protected ModelCodegen underTest; protected Model model; - @Before - public void setup() { + public ModelCodegenTest(DafnyVersion dafnyVersion) { model = TestSetupUtils.setupLocalModel(ModelConstants.CRYPTOGRAPHY_A_STRING_OPERATION); - underTest = new ModelCodegen(TestSetupUtils.setupLibrary(model, "aws.cryptography.test")); + underTest = new ModelCodegen(TestSetupUtils.setupLibrary(model, "aws.cryptography.test", dafnyVersion)); } @Test diff --git a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/nameresolver/DafnyTest.java b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/nameresolver/DafnyTest.java index da1991ebe..4606578a9 100644 --- a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/nameresolver/DafnyTest.java +++ b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/nameresolver/DafnyTest.java @@ -8,6 +8,10 @@ import org.junit.Before; import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import software.amazon.polymorph.smithydafny.DafnyVersion; +import software.amazon.polymorph.smithyjava.ForEachDafnyTest; import software.amazon.polymorph.smithyjava.ModelConstants; import software.amazon.polymorph.smithyjava.generator.CodegenSubject; import software.amazon.polymorph.smithyjava.generator.awssdk.TestSetupUtils; @@ -19,15 +23,17 @@ import software.amazon.smithy.model.shapes.ShapeId; import software.amazon.smithy.model.shapes.StructureShape; +import java.util.Arrays; +import java.util.Collection; + import static org.junit.Assert.assertEquals; import static software.amazon.polymorph.util.Tokenizer.tokenizeAndAssertEqual; -public class DafnyTest { +public class DafnyTest extends ForEachDafnyTest { Dafny underTest; protected Model model; - @Before - public void setup() { + public DafnyTest(DafnyVersion dafnyVersion) { String rawModel = """ namespace smithy.example service Example {} @@ -40,7 +46,7 @@ public void setup() { (builder, modelAssembler) -> modelAssembler .addUnparsedModel("test.smithy", rawModel)); ServiceShape serviceShape = ModelUtils.serviceFromNamespace(model, "smithy.example"); - underTest = new Dafny("Dafny.Smithy.Example", model, serviceShape, CodegenSubject.AwsSdkVersion.V2); + underTest = new Dafny("Dafny.Smithy.Example", model, serviceShape, CodegenSubject.AwsSdkVersion.V2, dafnyVersion); } @Test diff --git a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/util/Tokenizer.java b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/util/Tokenizer.java index 2573a240b..de00cd881 100644 --- a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/util/Tokenizer.java +++ b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/util/Tokenizer.java @@ -10,6 +10,7 @@ import software.amazon.polymorph.antlr.CSharpLexer; import java.util.List; +import java.util.Objects; import org.junit.Assert; @@ -33,6 +34,11 @@ public static record ParseToken(String text, int type) {} public static void tokenizeAndAssertEqual(String expected, String actual) { final List actualTokens = tokenize(actual); final List expectedTokens = tokenize(expected); - Assert.assertEquals(expectedTokens, actualTokens); + if (!Objects.equals(expectedTokens, actualTokens)) { + // If the tokens aren't equal, assert the original strings are equal + // knowing it is guaranteed to fail, + // just so that we get a much more readable diff in tooling. + Assert.assertEquals(expected, actual); + } } }