Skip to content

Commit

Permalink
feat: Support externs in rust without patch files (#521)
Browse files Browse the repository at this point in the history
Dafny's `feat-rust` branch currently assumes all code is going into one crate. There are two options for adding additional Rust code that is manually-written (or generated from other sources :):

1. Pass the files as additional input files to `dafny`.
2. Post-process the output from `dafny` to declare the extra modules.

#1 is cleaner, but requires that the Rust source files are not nested under folders to implicitly declare their ancestor modules. Since the design for Rust support so far has lots of these nested files, and we are hoping to eventually reuse the `smithy-rs` logic which generates such files, we're opting for #2 for now (although we do now use #1 for the StandardLibrary as a special case).

Our approach so far has been to use patch files to add these extra declarations, but maintaining the patch files has been very painful in development, and we don't want to force `smithy-dafny` consumers to use them to create functional Rust libraries. Therefore this change adds automation to add the extra declarations.

Since the extra declarations depend on the Smithy model, this is done in Java logic rather than Makefile or scripting. I've added an additional `patch-after-transpiling` command to the CLI, retroactively interpreting the existing single command as `generate`. The apache commons CLI library doesn't support this directly but it's pretty simple to handle subcommands ourselves.

Also deleted all patch files for Rust. 🎉  Now test models can indicate they are benerated with `RUST_BENERATED=1` instead, which will make `make polymorph_rust` a no-op. Also fixed up the test models to work with the common set of declarations: some test models were missing their copy of `standard_library_conversions.rs`, and `Constructor` deviated from the config naming convention.
  • Loading branch information
robin-aws authored Aug 19, 2024
1 parent 9b1bf1d commit c2acbe8
Show file tree
Hide file tree
Showing 68 changed files with 2,508 additions and 24,757 deletions.
45 changes: 33 additions & 12 deletions SmithyDafnyMakefile.mk
Original file line number Diff line number Diff line change
Expand Up @@ -202,6 +202,7 @@ transpile_implementation:
-useRuntimeLib \
-out $(OUT) \
$(DAFNY_OPTIONS) \
$(DAFNY_OTHER_FILES) \
$(if $(strip $(STD_LIBRARY)) , -library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \
$(TRANSPILE_DEPENDENCIES)

Expand Down Expand Up @@ -243,6 +244,7 @@ transpile_test:
-useRuntimeLib \
-out $(OUT) \
$(DAFNY_OPTIONS) \
$(DAFNY_OTHER_FILES) \
$(if $(strip $(STD_LIBRARY)) , -library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \
$(TRANSPILE_DEPENDENCIES) \

Expand Down Expand Up @@ -417,7 +419,10 @@ polymorph_rust:
done

_polymorph_rust: OUTPUT_RUST=--output-rust $(LIBRARY_ROOT)/runtimes/rust
_polymorph_rust: _polymorph
# For several TestModels we've just manually written the code generation target,
# So we just want to ensure we can transpile and pass the tests in CI.
# For those, make polymorph_rust should just be a no-op.
_polymorph_rust: $(if $(RUST_BENERATED), , _polymorph)

########################## .NET targets

Expand Down Expand Up @@ -533,26 +538,42 @@ transpile_implementation_rust: TRANSPILE_DEPENDENCIES=
transpile_implementation_rust: STD_LIBRARY=
transpile_implementation_rust: SRC_INDEX_TRANSPILE=$(if $(SRC_INDEX),$(SRC_INDEX),src)
transpile_implementation_rust: TEST_INDEX_TRANSPILE=$(if $(TEST_INDEX),$(TEST_INDEX),test)
transpile_implementation_rust: $(if $(TRANSPILE_TESTS_IN_RUST), transpile_test, transpile_implementation) _mv_implementation_rust
transpile_implementation_rust: DAFNY_OTHER_FILES=$(RUST_OTHER_FILES)
transpile_implementation_rust: $(if $(TRANSPILE_TESTS_IN_RUST), transpile_test, transpile_implementation) _mv_implementation_rust patch_after_transpile_rust

transpile_dependencies_rust: LANG=rust
transpile_dependencies_rust: transpile_dependencies

_mv_implementation_rust: RUST_EXTERN_MODULE_DECLARATIONS=$(if $(AWS_SDK_CMD), \
mod client; \
mod conversions; \
mod standard_library_conversions;, )
_mv_implementation_rust:
mkdir -p runtimes/rust/src
# Dafny-generated code assumes its output will be the main library file,
# so we need to splice in module declarations for any extern code.
$(if $(AWS_SDK_CMD), \
python3 -c "import sys; data = sys.stdin.buffer.read(); sys.stdout.buffer.write(data.replace(b'\npub mod', b'\n$(RUST_EXTERN_MODULE_DECLARATIONS)\n\npub mod', 1) if b'\npub mod' in data else data)" \
< implementation_from_dafny-rust/src/implementation_from_dafny.rs > runtimes/rust/src/implementation_from_dafny.rs, \
mv implementation_from_dafny-rust/src/implementation_from_dafny.rs runtimes/rust/src/implementation_from_dafny.rs)
mv implementation_from_dafny-rust/src/implementation_from_dafny.rs runtimes/rust/src/implementation_from_dafny.rs
rustfmt runtimes/rust/src/implementation_from_dafny.rs
rm -rf implementation_from_dafny-rust

patch_after_transpile_rust:
set -e; for service in $(PROJECT_SERVICES) ; do \
export service_deps_var=SERVICE_DEPS_$${service} ; \
export namespace_var=SERVICE_NAMESPACE_$${service} ; \
export SERVICE=$${service} ; \
$(MAKE) _patch_after_transpile_rust ; \
done

_patch_after_transpile_rust: OUTPUT_RUST=--output-rust $(LIBRARY_ROOT)/runtimes/rust
_patch_after_transpile_rust:
cd $(CODEGEN_CLI_ROOT); \
./../gradlew run --args="\
patch-after-transpile \
--dafny-version $(DAFNY_VERSION) \
--library-root $(LIBRARY_ROOT) \
$(OUTPUT_RUST) \
--model $(if $(DIR_STRUCTURE_V2), $(LIBRARY_ROOT)/dafny/$(SERVICE)/Model, $(SMITHY_MODEL_ROOT)) \
--dependent-model $(PROJECT_ROOT)/$(SMITHY_DEPS) \
$(patsubst %, --dependent-model $(PROJECT_ROOT)/%/Model, $($(service_deps_var))) \
--namespace $($(namespace_var)) \
$(AWS_SDK_CMD) \
$(POLYMORPH_OPTIONS) \
";

build_rust:
cd runtimes/rust; \
cargo build
Expand Down
2 changes: 2 additions & 0 deletions TestModels/Aggregate/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,8 @@

CORES=2

RUST_BENERATED=1

include ../SharedMakefile.mk

PROJECT_SERVICES := \
Expand Down
Loading

0 comments on commit c2acbe8

Please sign in to comment.