From 44ee820af72f19dde79745bace46b3544fd52388 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 18 Oct 2024 16:40:34 -0700 Subject: [PATCH 01/12] Start with model --- examples/tutorial/model/weather.smithy | 136 +++++++++++++++++++++++++ examples/tutorial/smithy-build.json | 10 ++ 2 files changed, 146 insertions(+) create mode 100644 examples/tutorial/model/weather.smithy create mode 100644 examples/tutorial/smithy-build.json diff --git a/examples/tutorial/model/weather.smithy b/examples/tutorial/model/weather.smithy new file mode 100644 index 000000000..df1cf637e --- /dev/null +++ b/examples/tutorial/model/weather.smithy @@ -0,0 +1,136 @@ +$version: "2" + +namespace example.weather + +/// Provides weather forecasts. +@paginated(inputToken: "nextToken", outputToken: "nextToken", pageSize: "pageSize") +service Weather { + version: "2006-03-01" + resources: [ + City + ] + operations: [ + GetCurrentTime + ] +} + +resource City { + identifiers: { cityId: CityId } + properties: { coordinates: CityCoordinates } + read: GetCity + list: ListCities + resources: [ + Forecast + ] +} + +resource Forecast { + identifiers: { cityId: CityId } + properties: { chanceOfRain: Float } + read: GetForecast +} + +// "pattern" is a trait. +@pattern("^[A-Za-z0-9 ]+$") +string CityId + +@readonly +operation GetCity { + input := for City { + // "cityId" provides the identifier for the resource and + // has to be marked as required. + @required + $cityId + } + + output := for City { + // "required" is used on output to indicate if the service + // will always provide a value for the member. + @required + @notProperty + name: String + + @required + $coordinates + } + + errors: [ + NoSuchResource + ] +} + +// This structure is nested within GetCityOutput. +structure CityCoordinates { + @required + latitude: Float + + @required + longitude: Float +} + +// "error" is a trait that is used to specialize +// a structure as an error. +@error("client") +structure NoSuchResource { + @required + resourceType: String +} + +// The paginated trait indicates that the operation may +// return truncated results. +@readonly +@paginated(items: "items") +operation ListCities { + input := { + nextToken: String + pageSize: Integer + } + + output := { + nextToken: String + + @required + items: CitySummaries + } +} + +// CitySummaries is a list of CitySummary structures. +list CitySummaries { + member: CitySummary +} + +// CitySummary contains a reference to a City. +@references([ + { + resource: City + } +]) +structure CitySummary { + @required + cityId: CityId + + @required + name: String +} + +@readonly +operation GetCurrentTime { + output := { + @required + time: Timestamp + } +} + +@readonly +operation GetForecast { + input := for Forecast { + // "cityId" provides the only identifier for the resource since + // a Forecast doesn't have its own. + @required + $cityId + } + + output := for Forecast { + $chanceOfRain + } +} diff --git a/examples/tutorial/smithy-build.json b/examples/tutorial/smithy-build.json new file mode 100644 index 000000000..942839164 --- /dev/null +++ b/examples/tutorial/smithy-build.json @@ -0,0 +1,10 @@ +{ + "version": "1.0", + "sources": ["model"], + "maven": { + "dependencies": [ + ], + "repositories": [ + ] + } +} \ No newline at end of file From 058f566b35526662bf6f737b2d8bf1f1eb20786a Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Mon, 3 Mar 2025 10:30:12 -0800 Subject: [PATCH 02/12] Add --enforce-determinism everywhere --- SmithyDafnyMakefile.mk | 5 +++++ TestModels/dafny-dependencies/StandardLibrary/Makefile | 3 ++- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/SmithyDafnyMakefile.mk b/SmithyDafnyMakefile.mk index ea3a25405..54431b26a 100644 --- a/SmithyDafnyMakefile.mk +++ b/SmithyDafnyMakefile.mk @@ -90,6 +90,7 @@ verify:DAFNY_OPTIONS=--allow-warnings verify: find . -name '*.dfy' | xargs -n 1 -P $(DAFNY_PROCESSES) -I % dafny verify \ --cores $(Z3_PROCESSES) \ + --enforce-determinism \ --unicode-char false \ --function-syntax 3 \ --log-format csv \ @@ -106,6 +107,7 @@ verify_single:DAFNY_OPTIONS=--allow-warnings verify_single: dafny verify \ --cores $(CORES) \ + --enforce-determinism \ --unicode-char false \ --function-syntax 3 \ --log-format text \ @@ -122,6 +124,7 @@ verify_service: @: $(if ${SERVICE},,$(error You must pass the SERVICE to generate for)); dafny verify \ --cores $(CORES) \ + --enforce-determinism \ --unicode-char false \ --function-syntax 3 \ --log-format text \ @@ -201,6 +204,7 @@ transpile_implementation: --stdin \ --no-verify \ --cores:$(CORES) \ + --enforce-determinism \ --optimize-erasable-datatype-wrapper:false \ --unicode-char:false \ --function-syntax:3 \ @@ -241,6 +245,7 @@ transpile_test: --stdin \ --no-verify \ --cores:$(CORES) \ + --enforce-determinism \ --optimize-erasable-datatype-wrapper:false \ --unicode-char:false \ --function-syntax:3 \ diff --git a/TestModels/dafny-dependencies/StandardLibrary/Makefile b/TestModels/dafny-dependencies/StandardLibrary/Makefile index f3984ba7f..6f0eac325 100644 --- a/TestModels/dafny-dependencies/StandardLibrary/Makefile +++ b/TestModels/dafny-dependencies/StandardLibrary/Makefile @@ -103,6 +103,7 @@ transpile_implementation: --stdin \ --no-verify \ --cores:$(CORES) \ + --enforce-determinism \ --optimize-erasable-datatype-wrapper:false \ --unicode-char:false \ --function-syntax:3 \ @@ -138,7 +139,7 @@ dafny_benerate: DAFNY_RUST_OUTPUT_RS_DTR=\ dafny_benerate: DAFNY_RUST_IMPL=\ runtimes/rust/src/implementation_from_dafny.rs dafny_benerate: - $(DAFNY) translate rs src/Index.dfy --emit-uncompilable-code --no-verify --optimize-erasable-datatype-wrapper false --include-runtime --compile-suffix true --unicode-char false --function-syntax 3 --allow-warnings --output $(DAFNY_RUST_OUTPUT) + $(DAFNY) translate rs src/Index.dfy --emit-uncompilable-code --no-verify --enforce-determinism --optimize-erasable-datatype-wrapper false --include-runtime --compile-suffix true --unicode-char false --function-syntax 3 --allow-warnings --output $(DAFNY_RUST_OUTPUT) rustfmt $(DAFNY_RUST_OUTPUT_RS) # echo "Diffs remaining till code generation works:" # diff -u $(DAFNY_RUST_OUTPUT_RS) $(DAFNY_RUST_IMPL) | wc -l From fa7904d25b35c16581d39e38376941b008d223a6 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Mon, 3 Mar 2025 10:45:09 -0800 Subject: [PATCH 03/12] One more --- .../DafnyStandardLibraries-smithy-dafny-subset.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/TestModels/dafny-dependencies/StandardLibrary/DafnyStandardLibraries-smithy-dafny-subset.toml b/TestModels/dafny-dependencies/StandardLibrary/DafnyStandardLibraries-smithy-dafny-subset.toml index b3ea6e4ac..3cc98bcb7 100644 --- a/TestModels/dafny-dependencies/StandardLibrary/DafnyStandardLibraries-smithy-dafny-subset.toml +++ b/TestModels/dafny-dependencies/StandardLibrary/DafnyStandardLibraries-smithy-dafny-subset.toml @@ -18,7 +18,7 @@ includes = [ # Options that help support more values of consuming context options # (mostly turning on any more restrictive verification) track-print-effects = true -enforce-determinism = false +enforce-determinism = true reads-clauses-on-methods = true # Options that differ from Dafny's From 5c0d8ddfc31976e79d3499ac9d3d81bcb46aadf4 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 4 Mar 2025 09:37:09 -0800 Subject: [PATCH 04/12] Update dafny submodule --- TestModels/dafny-dependencies/dafny | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/TestModels/dafny-dependencies/dafny b/TestModels/dafny-dependencies/dafny index 70831a833..f98f30c82 160000 --- a/TestModels/dafny-dependencies/dafny +++ b/TestModels/dafny-dependencies/dafny @@ -1 +1 @@ -Subproject commit 70831a8332ccbca883ac54b273db26d98cc06e48 +Subproject commit f98f30c825d0245cacebf4a2f35ad59e518b5b10 From 0dee6d04c7f0ead0ce322029e4507c5e08550bc4 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 4 Mar 2025 10:51:01 -0800 Subject: [PATCH 05/12] Switch to more focused dafny branch --- TestModels/dafny-dependencies/dafny | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/TestModels/dafny-dependencies/dafny b/TestModels/dafny-dependencies/dafny index f98f30c82..d12aa376e 160000 --- a/TestModels/dafny-dependencies/dafny +++ b/TestModels/dafny-dependencies/dafny @@ -1 +1 @@ -Subproject commit f98f30c825d0245cacebf4a2f35ad59e518b5b10 +Subproject commit d12aa376e62d2e0a940c4de687c64625862b8206 From 62fa28570bacbc490b50f77d069c98ec9e0797fe Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 20 May 2025 14:31:42 -0700 Subject: [PATCH 06/12] Accidental add --- examples/tutorial/model/weather.smithy | 136 ------------------------- examples/tutorial/smithy-build.json | 10 -- 2 files changed, 146 deletions(-) delete mode 100644 examples/tutorial/model/weather.smithy delete mode 100644 examples/tutorial/smithy-build.json diff --git a/examples/tutorial/model/weather.smithy b/examples/tutorial/model/weather.smithy deleted file mode 100644 index df1cf637e..000000000 --- a/examples/tutorial/model/weather.smithy +++ /dev/null @@ -1,136 +0,0 @@ -$version: "2" - -namespace example.weather - -/// Provides weather forecasts. -@paginated(inputToken: "nextToken", outputToken: "nextToken", pageSize: "pageSize") -service Weather { - version: "2006-03-01" - resources: [ - City - ] - operations: [ - GetCurrentTime - ] -} - -resource City { - identifiers: { cityId: CityId } - properties: { coordinates: CityCoordinates } - read: GetCity - list: ListCities - resources: [ - Forecast - ] -} - -resource Forecast { - identifiers: { cityId: CityId } - properties: { chanceOfRain: Float } - read: GetForecast -} - -// "pattern" is a trait. -@pattern("^[A-Za-z0-9 ]+$") -string CityId - -@readonly -operation GetCity { - input := for City { - // "cityId" provides the identifier for the resource and - // has to be marked as required. - @required - $cityId - } - - output := for City { - // "required" is used on output to indicate if the service - // will always provide a value for the member. - @required - @notProperty - name: String - - @required - $coordinates - } - - errors: [ - NoSuchResource - ] -} - -// This structure is nested within GetCityOutput. -structure CityCoordinates { - @required - latitude: Float - - @required - longitude: Float -} - -// "error" is a trait that is used to specialize -// a structure as an error. -@error("client") -structure NoSuchResource { - @required - resourceType: String -} - -// The paginated trait indicates that the operation may -// return truncated results. -@readonly -@paginated(items: "items") -operation ListCities { - input := { - nextToken: String - pageSize: Integer - } - - output := { - nextToken: String - - @required - items: CitySummaries - } -} - -// CitySummaries is a list of CitySummary structures. -list CitySummaries { - member: CitySummary -} - -// CitySummary contains a reference to a City. -@references([ - { - resource: City - } -]) -structure CitySummary { - @required - cityId: CityId - - @required - name: String -} - -@readonly -operation GetCurrentTime { - output := { - @required - time: Timestamp - } -} - -@readonly -operation GetForecast { - input := for Forecast { - // "cityId" provides the only identifier for the resource since - // a Forecast doesn't have its own. - @required - $cityId - } - - output := for Forecast { - $chanceOfRain - } -} diff --git a/examples/tutorial/smithy-build.json b/examples/tutorial/smithy-build.json deleted file mode 100644 index 942839164..000000000 --- a/examples/tutorial/smithy-build.json +++ /dev/null @@ -1,10 +0,0 @@ -{ - "version": "1.0", - "sources": ["model"], - "maven": { - "dependencies": [ - ], - "repositories": [ - ] - } -} \ No newline at end of file From 2a557cbc349aedb33dd625594134d4224eb5ff4a Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 20 May 2025 17:45:02 -0700 Subject: [PATCH 07/12] Add is-dafny-at-least command --- .../software/amazon/polymorph/CodegenCli.java | 65 ++++++++++++++----- .../amazon/polymorph/CodegenEngine.java | 2 +- 2 files changed, 50 insertions(+), 17 deletions(-) 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 fe7498610..7aa9d8608 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 @@ -39,13 +39,16 @@ public class CodegenCli { private enum Command { GENERATE, PATCH_AFTER_TRANSPILE, + IS_DAFNY_AT_LEAST, } private static final Map optionsForCommand = Map.of( Command.GENERATE, getCliOptionsForBuild(), Command.PATCH_AFTER_TRANSPILE, - getCliOptionsForPatchAfterTranspile() + getCliOptionsForPatchAfterTranspile(), + Command.IS_DAFNY_AT_LEAST, + getCliOptionsForCheckDafnyVersion() ); public static void main(String[] args) { @@ -165,6 +168,7 @@ public static void main(String[] args) { switch (cliArguments.command) { case GENERATE -> engine.run(); case PATCH_AFTER_TRANSPILE -> engine.patchAfterTranspiling(); + // IS_DAFNY_AT_LEAST is handled in CodegenCli.parse() instead } } @@ -454,7 +458,22 @@ private static Options getCliOptionsForPatchAfterTranspile() { ); } - private static void printHelpMessage() { + private static Options getCliOptionsForCheckDafnyVersion() { + return new Options() + .addOption( + Option.builder("h").longOpt("help").desc("print help message").build() + ) + .addOption( + Option + .builder() + .longOpt("dafny-version") + .desc("Minimum Dafny version to check for") + .hasArg() + .build() + ); + } + + private static void printHelpMessage() { new HelpFormatter() .printHelp( "smithy-dafny-codegen-cli [generate]", @@ -465,6 +484,11 @@ private static void printHelpMessage() { "smithy-dafny-codegen-cli patch-after-transpile", getCliOptionsForPatchAfterTranspile() ); + new HelpFormatter() + .printHelp( + "smithy-dafny-codegen-cli is-dafny-at-least", + getCliOptionsForCheckDafnyVersion() + ); } private record CliArguments( @@ -525,6 +549,26 @@ static Optional parse(String[] args) throws ParseException { return Optional.empty(); } + DafnyVersion dafnyVersion = null; + String dafnyVersionStr = commandLine.getOptionValue("dafny-version"); + if (dafnyVersionStr != null) { + try { + dafnyVersion = DafnyVersion.parse(dafnyVersionStr.trim()); + } catch (IllegalArgumentException ex) { + LOGGER.error("Could not parse --dafny-version: {}", dafnyVersionStr); + throw ex; + } + } + + // This command doesn't need a model/codegen engine/etc. + if (command == Command.IS_DAFNY_AT_LEAST) { + if (CodegenEngine.getDafnyVersionFromDafny().compareTo(dafnyVersion) >= 0) { + System.exit(0); + } else { + System.exit(1); + } + } + Path libraryRoot = Paths.get(commandLine.getOptionValue("library-root")); final Path modelPath = Path.of(commandLine.getOptionValue('m')); @@ -591,25 +635,14 @@ static Optional parse(String[] args) throws ParseException { Optional javaAwsSdkVersion = Optional.empty(); if (commandLine.hasOption("java-aws-sdk-version")) { - final String versionStr = commandLine + final String sdkVersionStr = commandLine .getOptionValue("java-aws-sdk-version") .trim() .toUpperCase(); try { - javaAwsSdkVersion = Optional.of(AwsSdkVersion.valueOf(versionStr)); - } catch (IllegalArgumentException ex) { - LOGGER.error("Unknown Java AWS SDK version {}", versionStr); - throw ex; - } - } - - DafnyVersion dafnyVersion = null; - String versionStr = commandLine.getOptionValue("dafny-version"); - if (versionStr != null) { - try { - dafnyVersion = DafnyVersion.parse(versionStr.trim()); + javaAwsSdkVersion = Optional.of(AwsSdkVersion.valueOf(sdkVersionStr)); } catch (IllegalArgumentException ex) { - LOGGER.error("Could not parse --dafny-version: {}", versionStr); + LOGGER.error("Unknown Java AWS SDK version {}", sdkVersionStr); throw ex; } } 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 7136e4594..74c902cab 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 @@ -1305,7 +1305,7 @@ public CodegenEngine build() { // If the version has not been released yet, // downgrade it. Otherwise, the system will not find runtime libraries // with the same version. - // The better fix for this is for Dafny to pre-release + // The better fix for this is for Dafny to pre-release runtimes as well. if (dafnyVersion.compareTo(MAX_DAFNY_VERSION) > 0) { LOGGER.warn( "Dafny version {} appears to be unreleased, downgrading to {} to ensure runtimes are available", From a91f26957da309179353c029d07f23a9bf402af3 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 20 May 2025 20:33:27 -0700 Subject: [PATCH 08/12] =?UTF-8?q?Only=20include=20`=E2=80=94enforce-determ?= =?UTF-8?q?inism`=20on=20newer=20Dafnies?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- SmithyDafnyMakefile.mk | 16 +++++++--- codegen/build.gradle.kts | 4 +-- .../software/amazon/polymorph/CodegenCli.java | 31 +++++++++++++------ 3 files changed, 34 insertions(+), 17 deletions(-) diff --git a/SmithyDafnyMakefile.mk b/SmithyDafnyMakefile.mk index 54431b26a..ab81358b5 100644 --- a/SmithyDafnyMakefile.mk +++ b/SmithyDafnyMakefile.mk @@ -80,6 +80,8 @@ ENABLE_EXTERN_PROCESSING?= # ensures DAFNY_PROCESSES(cpus) * Z3_PROCESSES(cpus) <= cpus # {} +ENFORCE_DETERMINISM_OPTION := $(shell cd $(CODEGEN_CLI_ROOT); \ + ./../gradlew run -q --args="if-dafny-at-least --dafny-version 4.8 --text --enforce-determinism") # Verify the entire project verify:Z3_PROCESSES=$(shell echo $$(( $(CORES) >= 3 ? 2 : 1 ))) @@ -90,7 +92,7 @@ verify:DAFNY_OPTIONS=--allow-warnings verify: find . -name '*.dfy' | xargs -n 1 -P $(DAFNY_PROCESSES) -I % dafny verify \ --cores $(Z3_PROCESSES) \ - --enforce-determinism \ + $(ENFORCE_DETERMINISM_OPTION) \ --unicode-char false \ --function-syntax 3 \ --log-format csv \ @@ -107,7 +109,7 @@ verify_single:DAFNY_OPTIONS=--allow-warnings verify_single: dafny verify \ --cores $(CORES) \ - --enforce-determinism \ + $(ENFORCE_DETERMINISM_OPTION) \ --unicode-char false \ --function-syntax 3 \ --log-format text \ @@ -124,7 +126,7 @@ verify_service: @: $(if ${SERVICE},,$(error You must pass the SERVICE to generate for)); dafny verify \ --cores $(CORES) \ - --enforce-determinism \ + $(ENFORCE_DETERMINISM_OPTION) \ --unicode-char false \ --function-syntax 3 \ --log-format text \ @@ -204,7 +206,7 @@ transpile_implementation: --stdin \ --no-verify \ --cores:$(CORES) \ - --enforce-determinism \ + $(ENFORCE_DETERMINISM_OPTION) \ --optimize-erasable-datatype-wrapper:false \ --unicode-char:false \ --function-syntax:3 \ @@ -245,7 +247,7 @@ transpile_test: --stdin \ --no-verify \ --cores:$(CORES) \ - --enforce-determinism \ + $(ENFORCE_DETERMINISM_OPTION) \ --optimize-erasable-datatype-wrapper:false \ --unicode-char:false \ --function-syntax:3 \ @@ -269,6 +271,10 @@ transpile_dependencies_test: $(if $(strip $(STD_LIBRARY)), $(MAKE) -C $(PROJECT_ROOT)/$(STD_LIBRARY) transpile_test_$(LANG), ) $(patsubst %, $(MAKE) -C $(PROJECT_ROOT)/% transpile_test_$(LANG);, $(PROJECT_DEPENDENCIES)) +needs_enforce_determinism: + cd $(CODEGEN_CLI_ROOT); \ + ./../gradlew run --args="is-dafny-at-least --dafny-version 4.9"; + ########################## Code-Gen targets mvn_local_deploy_polymorph_dependencies: diff --git a/codegen/build.gradle.kts b/codegen/build.gradle.kts index 24bd35a7a..c6ca57f62 100644 --- a/codegen/build.gradle.kts +++ b/codegen/build.gradle.kts @@ -58,8 +58,8 @@ subprojects { */ when (subproject.name) { - "smithy-dafny-codegen-test" -> println("Skipping publish for smithy-dafny-codegen-test") - "smithy-python-codegen" -> println("Skipping publish for smithy-python-codegen") + "smithy-dafny-codegen-test" -> logger.info("Skipping publish for smithy-dafny-codegen-test") + "smithy-python-codegen" -> logger.info("Skipping publish for smithy-python-codegen") else -> { if (subproject.name == "smithy-dafny-codegen-cli") { apply(plugin = "application") 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 7aa9d8608..1669a18fc 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 @@ -39,7 +39,7 @@ public class CodegenCli { private enum Command { GENERATE, PATCH_AFTER_TRANSPILE, - IS_DAFNY_AT_LEAST, + IF_DAFNY_AT_LEAST, } private static final Map optionsForCommand = Map.of( @@ -47,8 +47,8 @@ private enum Command { getCliOptionsForBuild(), Command.PATCH_AFTER_TRANSPILE, getCliOptionsForPatchAfterTranspile(), - Command.IS_DAFNY_AT_LEAST, - getCliOptionsForCheckDafnyVersion() + Command.IF_DAFNY_AT_LEAST, + getCliOptionsForIfDafnyAtLeast() ); public static void main(String[] args) { @@ -168,7 +168,7 @@ public static void main(String[] args) { switch (cliArguments.command) { case GENERATE -> engine.run(); case PATCH_AFTER_TRANSPILE -> engine.patchAfterTranspiling(); - // IS_DAFNY_AT_LEAST is handled in CodegenCli.parse() instead + // IF_DAFNY_AT_LEAST is handled in CodegenCli.parse() instead } } @@ -458,7 +458,7 @@ private static Options getCliOptionsForPatchAfterTranspile() { ); } - private static Options getCliOptionsForCheckDafnyVersion() { + private static Options getCliOptionsForIfDafnyAtLeast() { return new Options() .addOption( Option.builder("h").longOpt("help").desc("print help message").build() @@ -469,6 +469,16 @@ private static Options getCliOptionsForCheckDafnyVersion() { .longOpt("dafny-version") .desc("Minimum Dafny version to check for") .hasArg() + .required() + .build() + ) + .addOption( + Option + .builder() + .longOpt("text") + .desc("Text to output if the Dafny version passes the check") + .hasArg() + .required() .build() ); } @@ -487,7 +497,7 @@ private static void printHelpMessage() { new HelpFormatter() .printHelp( "smithy-dafny-codegen-cli is-dafny-at-least", - getCliOptionsForCheckDafnyVersion() + getCliOptionsForIfDafnyAtLeast() ); } @@ -521,6 +531,7 @@ private record CliArguments( * @return parsed arguments, or {@code Optional.empty()} if help should be printed * @throws ParseException if command line arguments are invalid */ + @SuppressWarnings("security:S4507") // Suppressing log injection warning for makefile echo-like command static Optional parse(String[] args) throws ParseException { final DefaultParser parser = new DefaultParser(); final String commandString = args.length > 0 && !args[0].startsWith("-") @@ -561,12 +572,12 @@ static Optional parse(String[] args) throws ParseException { } // This command doesn't need a model/codegen engine/etc. - if (command == Command.IS_DAFNY_AT_LEAST) { + if (command == Command.IF_DAFNY_AT_LEAST) { + String text = commandLine.getOptionValue("text"); if (CodegenEngine.getDafnyVersionFromDafny().compareTo(dafnyVersion) >= 0) { - System.exit(0); - } else { - System.exit(1); + System.out.println(text); } + System.exit(0); } Path libraryRoot = Paths.get(commandLine.getOptionValue("library-root")); From 30644a584460a86d8b41e1a28a569fdd280a8774 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 20 May 2025 20:35:24 -0700 Subject: [PATCH 09/12] Formatting --- .../src/main/java/software/amazon/polymorph/CodegenCli.java | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) 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 1669a18fc..fdc3a1486 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 @@ -483,7 +483,7 @@ private static Options getCliOptionsForIfDafnyAtLeast() { ); } - private static void printHelpMessage() { + private static void printHelpMessage() { new HelpFormatter() .printHelp( "smithy-dafny-codegen-cli [generate]", @@ -574,7 +574,9 @@ static Optional parse(String[] args) throws ParseException { // This command doesn't need a model/codegen engine/etc. if (command == Command.IF_DAFNY_AT_LEAST) { String text = commandLine.getOptionValue("text"); - if (CodegenEngine.getDafnyVersionFromDafny().compareTo(dafnyVersion) >= 0) { + if ( + CodegenEngine.getDafnyVersionFromDafny().compareTo(dafnyVersion) >= 0 + ) { System.out.println(text); } System.exit(0); From faed7f1aa89557db94e499f45ed8590266dd8c38 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 21 May 2025 07:31:21 -0700 Subject: [PATCH 10/12] Rust 1.82 --- .github/workflows/test_models_rust_tests.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/test_models_rust_tests.yml b/.github/workflows/test_models_rust_tests.yml index 2ad943133..524acb437 100644 --- a/.github/workflows/test_models_rust_tests.yml +++ b/.github/workflows/test_models_rust_tests.yml @@ -59,7 +59,7 @@ jobs: - name: Set up Rust uses: actions-rust-lang/setup-rust-toolchain@v1 with: - toolchain: "1.81.0" + toolchain: "1.82.0" rustflags: "" components: rustfmt From bef5cdf324383da886db8eccabbe1b6c922a0cdf Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 21 May 2025 10:57:53 -0700 Subject: [PATCH 11/12] Typos --- SmithyDafnyMakefile.mk | 4 ---- .../src/main/java/software/amazon/polymorph/CodegenCli.java | 2 +- 2 files changed, 1 insertion(+), 5 deletions(-) diff --git a/SmithyDafnyMakefile.mk b/SmithyDafnyMakefile.mk index ab81358b5..1dde2776f 100644 --- a/SmithyDafnyMakefile.mk +++ b/SmithyDafnyMakefile.mk @@ -271,10 +271,6 @@ transpile_dependencies_test: $(if $(strip $(STD_LIBRARY)), $(MAKE) -C $(PROJECT_ROOT)/$(STD_LIBRARY) transpile_test_$(LANG), ) $(patsubst %, $(MAKE) -C $(PROJECT_ROOT)/% transpile_test_$(LANG);, $(PROJECT_DEPENDENCIES)) -needs_enforce_determinism: - cd $(CODEGEN_CLI_ROOT); \ - ./../gradlew run --args="is-dafny-at-least --dafny-version 4.9"; - ########################## Code-Gen targets mvn_local_deploy_polymorph_dependencies: 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 fdc3a1486..f91ead976 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 @@ -496,7 +496,7 @@ private static void printHelpMessage() { ); new HelpFormatter() .printHelp( - "smithy-dafny-codegen-cli is-dafny-at-least", + "smithy-dafny-codegen-cli fs-dafny-at-least", getCliOptionsForIfDafnyAtLeast() ); } From a9d57f9215b8f60d57f307e2f6fc230589f823cf Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 21 May 2025 11:05:36 -0700 Subject: [PATCH 12/12] Update codegen/smithy-dafny-codegen-cli/src/main/java/software/amazon/polymorph/CodegenCli.java Co-authored-by: Rishav karanjit --- .../src/main/java/software/amazon/polymorph/CodegenCli.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 f91ead976..b0368f882 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 @@ -496,7 +496,7 @@ private static void printHelpMessage() { ); new HelpFormatter() .printHelp( - "smithy-dafny-codegen-cli fs-dafny-at-least", + "smithy-dafny-codegen-cli if-dafny-at-least", getCliOptionsForIfDafnyAtLeast() ); }