Skip to content

Commit 81dd77f

Browse files
robin-awsrobin-aws
authored
feat: Support Dafny tests on test models for Rust (#460)
*Issue #, if available:* Resolves #458 *Description of changes:* Supports compiling the common Dafny tests in a test model for Rust. This involved having to change some properties of how we lay out the Rust crates: * ~Removed the `dafny_impl` sub-crate and moved `implementation_from_dafny.rs` into the main `src` directory - hence replacing `::simple_boolean_dafny` with `crate::implementation_from_dafny` everywhere. I originally had this separated to better divide Dafny-generated code from Smithy-generated code, but it made implementing externs hard/impossible, and Dafny tests make use of "wrapped services" which are essentially testing-only extern shims.~ * This turned out to be unnecessary, because it is reasonable to patch in additional `use ::simple_boolean_dafny::*;` and `use simple_boolean::*;` imports into the compiled tests. This is equivalent to the `pub use dafny_standard_library::implementation_from_dafny::*;` import the Makefile is adding, and will be replaced by a Dafny feature named something like `--rust-module-name` as some other other supported languages already have. * Added ~`tests/tests_from_dafny/_wrapped.rs`~ `wrapped::client::Client` with the implementation of the "wrapped service", which is implementing the Dafny-client interface using the Rust idiomatic client. * Since this is only used for testing, but implements a Dafny extern that is only defined by Dafny test code, I guarded this with a `wrapped-client` feature which the Dafny-compiled integration test enables, as per rust-lang/cargo#2911 (comment) * ~Removed `async` from the client interfaces - we'd originally kept these for better forwards-compatibility, but AFAICT it's impossible to implement the synchronous Dafny-generated trait methods with async methods. This just means that in the future we'll eventually have to provide separate async clients, but that's happened with the AWS SDKs frequently as well.~ * Worked around this by instantiating a `current_thread` Tokio `Runtime` as per https://tokio.rs/tokio/topics/bridging instead.
1 parent 10e908e commit 81dd77f

File tree

22 files changed

+1627
-1261
lines changed

22 files changed

+1627
-1261
lines changed

‎SmithyDafnyMakefile.mk

+18-8
Original file line numberDiff line numberDiff line change
@@ -242,6 +242,7 @@ transpile_test:
242242
-functionSyntax:3 \
243243
-useRuntimeLib \
244244
-out $(OUT) \
245+
$(DAFNY_OPTIONS) \
245246
$(if $(strip $(STD_LIBRARY)) , -library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \
246247
$(TRANSPILE_DEPENDENCIES) \
247248

@@ -251,6 +252,10 @@ transpile_dependencies:
251252
$(if $(strip $(STD_LIBRARY)), $(MAKE) -C $(PROJECT_ROOT)/$(STD_LIBRARY) transpile_implementation_$(LANG), )
252253
$(patsubst %, $(MAKE) -C $(PROJECT_ROOT)/% transpile_implementation_$(LANG);, $(PROJECT_DEPENDENCIES))
253254

255+
transpile_dependencies_test:
256+
$(if $(strip $(STD_LIBRARY)), $(MAKE) -C $(PROJECT_ROOT)/$(STD_LIBRARY) transpile_test_$(LANG), )
257+
$(patsubst %, $(MAKE) -C $(PROJECT_ROOT)/% transpile_test_$(LANG);, $(PROJECT_DEPENDENCIES))
258+
254259
########################## Code-Gen targets
255260

256261
# The OUTPUT variables are created this way
@@ -296,6 +301,7 @@ _polymorph_wrapped:
296301
$(OUTPUT_DAFNY_WRAPPED) \
297302
$(OUTPUT_DOTNET_WRAPPED) \
298303
$(OUTPUT_JAVA_WRAPPED) \
304+
$(OUTPUT_RUST_WRAPPED) \
299305
--model $(if $(DIR_STRUCTURE_V2),$(LIBRARY_ROOT)/dafny/$(SERVICE)/Model,$(LIBRARY_ROOT)/Model) \
300306
--dependent-model $(PROJECT_ROOT)/$(SMITHY_DEPS) \
301307
$(patsubst %, --dependent-model $(PROJECT_ROOT)/%/Model, $($(service_deps_var))) \
@@ -510,10 +516,11 @@ test_java:
510516

511517
########################## Rust targets
512518

513-
# TODO: Dafny test transpilation needs manual patching to work too,
514-
# which isn't a high priority at this stage,
515-
# so don't include transpile_test_rust for now.
516-
transpile_rust: | transpile_implementation_rust transpile_dependencies_rust
519+
# Note that transpile_dependencies_test_rust is necessary
520+
# only because we are patching test code in the StandardLibrary,
521+
# so we don't transpile that code then the recursive call to polymorph_rust
522+
# on the StandardLibrary will fail because the patch does not apply.
523+
transpile_rust: | transpile_implementation_rust transpile_test_rust transpile_dependencies_rust transpile_dependencies_test_rust
517524

518525
transpile_implementation_rust: TARGET=rs
519526
transpile_implementation_rust: OUT=implementation_from_dafny
@@ -535,6 +542,9 @@ transpile_test_rust: _transpile_test_all _mv_test_rust
535542
transpile_dependencies_rust: LANG=rust
536543
transpile_dependencies_rust: transpile_dependencies
537544

545+
transpile_dependencies_test_rust: LANG=rust
546+
transpile_dependencies_test_rust: transpile_dependencies_test
547+
538548
_mv_implementation_rust:
539549
rm -rf runtimes/rust/dafny_impl/src
540550
mkdir -p runtimes/rust/dafny_impl/src
@@ -544,10 +554,10 @@ _mv_implementation_rust:
544554
rustfmt runtimes/rust/dafny_impl/src/implementation_from_dafny.rs
545555
rm -rf implementation_from_dafny-rust
546556
_mv_test_rust:
547-
rm -rf runtimes/rust/dafny_impl/tests
548-
mkdir -p runtimes/rust/dafny_impl/tests
549-
mv tests_from_dafny-rust/src/tests_from_dafny.rs runtimes/rust/dafny_impl/tests/tests_from_dafny.rs
550-
rustfmt runtimes/rust/dafny_impl/tests/tests_from_dafny.rs
557+
rm -f runtimes/rust/tests/tests_from_dafny/mod.rs
558+
mkdir -p runtimes/rust/tests/tests_from_dafny
559+
mv tests_from_dafny-rust/src/tests_from_dafny.rs runtimes/rust/tests/tests_from_dafny/mod.rs
560+
rustfmt runtimes/rust/tests/tests_from_dafny/mod.rs
551561
rm -rf tests_from_dafny-rust
552562

553563
build_rust:

‎TestModels/SharedMakefile.mk

+9
Original file line numberDiff line numberDiff line change
@@ -69,3 +69,12 @@ _polymorph_dotnet: _polymorph
6969
_polymorph_dotnet: OUTPUT_DOTNET_WRAPPED=\
7070
$(if $(DIR_STRUCTURE_V2), --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/Wrapped/$(SERVICE)/, --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/Wrapped)
7171
_polymorph_dotnet: _polymorph_wrapped
72+
73+
_polymorph_rust: OUTPUT_RUST=--output-rust $(LIBRARY_ROOT)/runtimes/rust
74+
_polymorph_rust: INPUT_DAFNY=\
75+
--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy
76+
_polymorph_rust: _polymorph
77+
# TODO: This doesn't yet work for Rust because we are patching transpiled code,
78+
# so this target will complain about "patch does not apply" because it was already applied.
79+
# _polymorph_rust: OUTPUT_RUST_WRAPPED=--output-rust $(LIBRARY_ROOT)/runtimes/rust
80+
# _polymorph_rust: _polymorph_wrapped

‎TestModels/SimpleTypes/SimpleBoolean/codegen-patches/rust/dafny-4.5.0.patch

+162-4
Original file line numberDiff line numberDiff line change
@@ -62,14 +62,54 @@ index 00000000..299b0baa
6262
+}
6363
diff --git b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions.rs a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions.rs
6464
new file mode 100644
65-
index 00000000..c1acac7b
65+
index 00000000..86f87891
6666
--- /dev/null
6767
+++ a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions.rs
68-
@@ -0,0 +1,4 @@
68+
@@ -0,0 +1,6 @@
6969
+// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT.
7070
+pub mod get_boolean;
7171
+
7272
+pub mod simple_boolean_config;
73+
+
74+
+pub(crate) mod error;
75+
\ No newline at end of file
76+
diff --git b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions/error.rs a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions/error.rs
77+
new file mode 100644
78+
index 00000000..d6fd32b7
79+
--- /dev/null
80+
+++ a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions/error.rs
81+
@@ -0,0 +1,30 @@
82+
+/// Wraps up an arbitrary Rust Error value as a Dafny Error
83+
+pub fn to_opaque_error<E: std::error::Error + 'static>(value: E) ->
84+
+ ::std::rc::Rc<::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error>
85+
+{
86+
+ let error_obj: ::dafny_runtime::Object<dyn::std::any::Any> =
87+
+ ::dafny_runtime::Object(Some(::std::rc::Rc::new(
88+
+ ::std::cell::UnsafeCell::new(value),
89+
+ )));
90+
+ ::std::rc::Rc::new(
91+
+ ::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error::Opaque {
92+
+ obj: error_obj,
93+
+ },
94+
+ )
95+
+}
96+
+
97+
+/// Wraps up an arbitrary Rust Error value as a Dafny Result<T, Error>.Failure
98+
+pub fn to_opaque_error_result<T: dafny_runtime::DafnyType, E: std::error::Error + 'static>(value: E) ->
99+
+ ::std::rc::Rc<
100+
+ dafny_standard_library::implementation_from_dafny::_Wrappers_Compile::Result<
101+
+ T,
102+
+ ::std::rc::Rc<::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error>
103+
+ >
104+
+ >
105+
+{
106+
+ ::std::rc::Rc::new(
107+
+ dafny_standard_library::implementation_from_dafny::_Wrappers_Compile::Result::Failure {
108+
+ error: to_opaque_error(value)
109+
+ }
110+
+ )
111+
+}
112+
\ No newline at end of file
73113
diff --git b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions/get_boolean.rs a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions/get_boolean.rs
74114
new file mode 100644
75115
index 00000000..065d3ad3
@@ -287,10 +327,10 @@ index 00000000..4d66eb2e
287327
\ No newline at end of file
288328
diff --git b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/lib.rs a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/lib.rs
289329
new file mode 100644
290-
index 00000000..1d16c191
330+
index 00000000..53977d7d
291331
--- /dev/null
292332
+++ a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/lib.rs
293-
@@ -0,0 +1,17 @@
333+
@@ -0,0 +1,20 @@
294334
+#![allow(deprecated)]
295335
+
296336
+// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT.
@@ -306,6 +346,9 @@ index 00000000..1d16c191
306346
+
307347
+mod conversions;
308348
+
349+
+#[cfg(feature = "wrapped-client")]
350+
+pub mod wrapped;
351+
+
309352
+pub use client::Client;
310353
+pub use types::simple_boolean_config::SimpleBooleanConfig;
311354
diff --git b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/operation.rs a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/operation.rs
@@ -719,3 +762,118 @@ index 00000000..6bf027f6
719762
+ ::std::result::Result::Ok(SimpleBooleanConfig {})
720763
+ }
721764
+}
765+
diff --git b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/wrapped.rs a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/wrapped.rs
766+
new file mode 100644
767+
index 00000000..39355176
768+
--- /dev/null
769+
+++ a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/wrapped.rs
770+
@@ -0,0 +1 @@
771+
+pub mod client;
772+
\ No newline at end of file
773+
diff --git b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/wrapped/client.rs a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/wrapped/client.rs
774+
new file mode 100644
775+
index 00000000..49c75f76
776+
--- /dev/null
777+
+++ a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/wrapped/client.rs
778+
@@ -0,0 +1,88 @@
779+
+use tokio::runtime::Runtime;
780+
+
781+
+pub struct Client {
782+
+ wrapped: crate::client::Client,
783+
+
784+
+ /// A `current_thread` runtime for executing operations on the
785+
+ /// asynchronous client in a blocking manner.
786+
+ rt: Runtime
787+
+}
788+
+
789+
+impl dafny_runtime::UpcastObject<dyn ::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::ISimpleTypesBooleanClient> for Client {
790+
+ ::dafny_runtime::UpcastObjectFn!(dyn ::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::ISimpleTypesBooleanClient);
791+
+}
792+
+
793+
+impl dafny_runtime::UpcastObject<dyn std::any::Any> for Client {
794+
+ ::dafny_runtime::UpcastObjectFn!(dyn ::std::any::Any);
795+
+}
796+
+
797+
+impl Client {
798+
+ pub fn from_conf(config: &::std::rc::Rc<
799+
+ ::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::SimpleBooleanConfig,
800+
+ >) ->
801+
+::std::rc::Rc<::simple_boolean_dafny::r#_Wrappers_Compile::Result<
802+
+ ::dafny_runtime::Object<dyn ::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::ISimpleTypesBooleanClient>,
803+
+ ::std::rc::Rc<::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error>
804+
+>> {
805+
+ let rt_result = tokio::runtime::Builder::new_current_thread()
806+
+ .enable_all()
807+
+ .build();
808+
+ let rt = match rt_result {
809+
+ Ok(x) => x,
810+
+ Err(error) => return crate::conversions::error::to_opaque_error_result(error),
811+
+ };
812+
+ let result = crate::client::Client::from_conf(
813+
+ crate::conversions::simple_boolean_config::_simple_boolean_config::from_dafny(
814+
+ config.clone(),
815+
+ ),
816+
+ );
817+
+ match result {
818+
+ Ok(client) => {
819+
+ let wrap = crate::wrapped::client::Client {
820+
+ wrapped: client,
821+
+ rt
822+
+ };
823+
+ std::rc::Rc::new(
824+
+ ::simple_boolean_dafny::_Wrappers_Compile::Result::Success {
825+
+ value: ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(wrap))
826+
+ }
827+
+ )
828+
+ },
829+
+ Err(error) => crate::conversions::error::to_opaque_error_result(error)
830+
+ }
831+
+ }
832+
+}
833+
+
834+
+impl ::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::ISimpleTypesBooleanClient
835+
+ for Client
836+
+{
837+
+ fn GetBoolean(
838+
+ &mut self,
839+
+ input: &std::rc::Rc<
840+
+ ::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::GetBooleanInput,
841+
+ >,
842+
+ ) -> std::rc::Rc<
843+
+ ::simple_boolean_dafny::r#_Wrappers_Compile::Result<
844+
+ std::rc::Rc<
845+
+ ::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::GetBooleanOutput,
846+
+ >,
847+
+ std::rc::Rc<::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error>,
848+
+ >,
849+
+ >{
850+
+ let inner_input =
851+
+ crate::conversions::get_boolean::_get_boolean_input::from_dafny(input.clone());
852+
+ let result = self.rt.block_on(crate::operation::get_boolean::GetBoolean::send(&self.wrapped, inner_input));
853+
+ match result {
854+
+ Err(error) => ::std::rc::Rc::new(
855+
+ ::simple_boolean_dafny::_Wrappers_Compile::Result::Failure {
856+
+ error: crate::conversions::get_boolean::to_dafny_error(error),
857+
+ },
858+
+ ),
859+
+ Ok(client) => ::std::rc::Rc::new(
860+
+ ::simple_boolean_dafny::_Wrappers_Compile::Result::Success {
861+
+ value: crate::conversions::get_boolean::_get_boolean_output::to_dafny(client),
862+
+ },
863+
+ ),
864+
+ }
865+
+ }
866+
+}
867+
diff --git b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/tests/tests_from_dafny/mod.rs a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/tests/tests_from_dafny/mod.rs
868+
index ce6d90a2..7f1ba031 100644
869+
--- b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/tests/tests_from_dafny/mod.rs
870+
+++ a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/tests/tests_from_dafny/mod.rs
871+
@@ -1,5 +1,8 @@
872+
#![allow(warnings, unconditional_panic)]
873+
#![allow(nonstandard_style)]
874+
+use ::simple_boolean_dafny::*;
875+
+use simple_boolean::*;
876+
+mod _wrapped;
877+
878+
pub mod r#_simple_dtypes_dboolean_dinternaldafny_dwrapped {
879+
pub struct _default {}

‎TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/Cargo.toml

+8-2
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,9 @@ edition = "2021"
55

66
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
77

8+
[features]
9+
wrapped-client = []
10+
811
[dependencies]
912
aws-smithy-runtime = {version = "1.6.0", features = ["client"] }
1013
aws-smithy-runtime-api = {version = "1.7.0", features = ["client"] }
@@ -13,6 +16,9 @@ dafny_runtime = { path = "../../../../dafny-dependencies/dafny_runtime_rust"}
1316
dafny_standard_library = { path = "../../../../dafny-dependencies/StandardLibrary/runtimes/rust"}
1417
simple_boolean_dafny = { path = "./dafny_impl"}
1518

16-
[dev-dependencies.tokio]
19+
[dev-dependencies]
20+
simple_boolean = { path = ".", features = ["wrapped-client"] }
21+
22+
[dependencies.tokio]
1723
version = "1.26.0"
18-
features = ["full"]
24+
features = ["full"]

‎TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/dafny_impl/Cargo.toml

+1-1
Original file line numberDiff line numberDiff line change
@@ -10,4 +10,4 @@ dafny_runtime = { path = "../../../../../dafny-dependencies/dafny_runtime_rust"}
1010
dafny_standard_library = { path = "../../../../../dafny-dependencies/StandardLibrary/runtimes/rust"}
1111

1212
[lib]
13-
path = "src/implementation_from_dafny.rs"
13+
path = "src/implementation_from_dafny.rs"

‎TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions.rs

+2
Original file line numberDiff line numberDiff line change
@@ -2,3 +2,5 @@
22
pub mod get_boolean;
33

44
pub mod simple_boolean_config;
5+
6+
pub(crate) mod error;

‎TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions/error.rs

+30
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
/// Wraps up an arbitrary Rust Error value as a Dafny Error
2+
pub fn to_opaque_error<E: std::error::Error + 'static>(value: E) ->
3+
::std::rc::Rc<::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error>
4+
{
5+
let error_obj: ::dafny_runtime::Object<dyn::std::any::Any> =
6+
::dafny_runtime::Object(Some(::std::rc::Rc::new(
7+
::std::cell::UnsafeCell::new(value),
8+
)));
9+
::std::rc::Rc::new(
10+
::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error::Opaque {
11+
obj: error_obj,
12+
},
13+
)
14+
}
15+
16+
/// Wraps up an arbitrary Rust Error value as a Dafny Result<T, Error>.Failure
17+
pub fn to_opaque_error_result<T: dafny_runtime::DafnyType, E: std::error::Error + 'static>(value: E) ->
18+
::std::rc::Rc<
19+
dafny_standard_library::implementation_from_dafny::_Wrappers_Compile::Result<
20+
T,
21+
::std::rc::Rc<::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error>
22+
>
23+
>
24+
{
25+
::std::rc::Rc::new(
26+
dafny_standard_library::implementation_from_dafny::_Wrappers_Compile::Result::Failure {
27+
error: to_opaque_error(value)
28+
}
29+
)
30+
}

‎TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/lib.rs

+3
Original file line numberDiff line numberDiff line change
@@ -13,5 +13,8 @@ pub mod operation;
1313

1414
mod conversions;
1515

16+
#[cfg(feature = "wrapped-client")]
17+
pub mod wrapped;
18+
1619
pub use client::Client;
1720
pub use types::simple_boolean_config::SimpleBooleanConfig;

‎TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/wrapped.rs

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
pub mod client;

0 commit comments

Comments
 (0)