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 diff --git a/SmithyDafnyMakefile.mk b/SmithyDafnyMakefile.mk index 621558c01..d5014bcaf 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,6 +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_OPTION) \ --unicode-char false \ --function-syntax 3 \ --log-format csv \ @@ -106,6 +109,7 @@ verify_single:DAFNY_OPTIONS=--allow-warnings verify_single: dafny verify \ --cores $(CORES) \ + $(ENFORCE_DETERMINISM_OPTION) \ --unicode-char false \ --function-syntax 3 \ --log-format text \ @@ -122,6 +126,7 @@ verify_service: @: $(if ${SERVICE},,$(error You must pass the SERVICE to generate for)); dafny verify \ --cores $(CORES) \ + $(ENFORCE_DETERMINISM_OPTION) \ --unicode-char false \ --function-syntax 3 \ --log-format text \ @@ -201,6 +206,7 @@ transpile_implementation: --stdin \ --no-verify \ --cores:$(CORES) \ + $(ENFORCE_DETERMINISM_OPTION) \ --optimize-erasable-datatype-wrapper:false \ --unicode-char:false \ --function-syntax:3 \ @@ -241,6 +247,7 @@ transpile_test: --stdin \ --no-verify \ --cores:$(CORES) \ + $(ENFORCE_DETERMINISM_OPTION) \ --optimize-erasable-datatype-wrapper:false \ --unicode-char:false \ --function-syntax:3 \ 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 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 diff --git a/TestModels/dafny-dependencies/dafny b/TestModels/dafny-dependencies/dafny index 70831a833..d12aa376e 160000 --- a/TestModels/dafny-dependencies/dafny +++ b/TestModels/dafny-dependencies/dafny @@ -1 +1 @@ -Subproject commit 70831a8332ccbca883ac54b273db26d98cc06e48 +Subproject commit d12aa376e62d2e0a940c4de687c64625862b8206 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 fe7498610..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 @@ -39,13 +39,16 @@ public class CodegenCli { private enum Command { GENERATE, PATCH_AFTER_TRANSPILE, + IF_DAFNY_AT_LEAST, } private static final Map optionsForCommand = Map.of( Command.GENERATE, getCliOptionsForBuild(), Command.PATCH_AFTER_TRANSPILE, - getCliOptionsForPatchAfterTranspile() + getCliOptionsForPatchAfterTranspile(), + Command.IF_DAFNY_AT_LEAST, + getCliOptionsForIfDafnyAtLeast() ); 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(); + // IF_DAFNY_AT_LEAST is handled in CodegenCli.parse() instead } } @@ -454,6 +458,31 @@ private static Options getCliOptionsForPatchAfterTranspile() { ); } + private static Options getCliOptionsForIfDafnyAtLeast() { + 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() + .required() + .build() + ) + .addOption( + Option + .builder() + .longOpt("text") + .desc("Text to output if the Dafny version passes the check") + .hasArg() + .required() + .build() + ); + } + private static void printHelpMessage() { new HelpFormatter() .printHelp( @@ -465,6 +494,11 @@ private static void printHelpMessage() { "smithy-dafny-codegen-cli patch-after-transpile", getCliOptionsForPatchAfterTranspile() ); + new HelpFormatter() + .printHelp( + "smithy-dafny-codegen-cli if-dafny-at-least", + getCliOptionsForIfDafnyAtLeast() + ); } private record CliArguments( @@ -497,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("-") @@ -525,6 +560,28 @@ 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.IF_DAFNY_AT_LEAST) { + String text = commandLine.getOptionValue("text"); + if ( + CodegenEngine.getDafnyVersionFromDafny().compareTo(dafnyVersion) >= 0 + ) { + System.out.println(text); + } + System.exit(0); + } + Path libraryRoot = Paths.get(commandLine.getOptionValue("library-root")); final Path modelPath = Path.of(commandLine.getOptionValue('m')); @@ -591,25 +648,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",