Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: Support Dafny tests on test models for Rust #460

Merged
merged 55 commits into from
Jul 12, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
55 commits
Select commit Hold shift + click to select a range
2ffb98d
Progress
robin-aws Jun 25, 2024
0710246
Progress
robin-aws Jun 25, 2024
323a1e5
Update package layout, most of the wrapped client impl
robin-aws Jun 25, 2024
644af7c
Successfully run and panicking!
robin-aws Jun 25, 2024
3f28cf7
tests passing
robin-aws Jun 26, 2024
e3ce7ea
Makefile updates
robin-aws Jun 26, 2024
ff1fcd6
Better tests file layout
robin-aws Jun 26, 2024
aa7f02e
Don’t let polymorph delete implementation_from_dafny.rs
robin-aws Jun 26, 2024
0d1f49a
Formatting
robin-aws Jun 26, 2024
3fccf32
Update commit
robin-aws Jul 9, 2024
6de828d
update copy of runtime
robin-aws Jul 9, 2024
9aec1d1
Don’t patch stdlib implementation_from_dafny.rs any more
robin-aws Jul 9, 2024
8911f81
Stop patching implementation_from_dafny.rs
robin-aws Jul 9, 2024
ac34eff
Fix SimpleBoolean
robin-aws Jul 9, 2024
9a99345
Much simpler Boolean fix
robin-aws Jul 9, 2024
3b7da6c
Add UpcastObject<Any> for Unhandled
robin-aws Jul 9, 2024
59aaed2
Replace most uses of UpcastTo
robin-aws Jul 9, 2024
3449728
Fix the rest
robin-aws Jul 9, 2024
af7138d
Don’t check in implementation_from_dafny.rs any more
robin-aws Jul 9, 2024
40b4d93
Missing sealed_unhandled.rs change
robin-aws Jul 9, 2024
bcbbbdc
Ignore implementation_from_dafny.rs
robin-aws Jul 9, 2024
636b83b
Tweak ignore
robin-aws Jul 9, 2024
1740711
UpcastObject impl for SimpleResourceWrapper
robin-aws Jul 9, 2024
1521617
Update patch files
robin-aws Jul 9, 2024
c902dcd
Formatting
robin-aws Jul 9, 2024
ec0e074
Merge branch 'robin-aws/use-tip-of-dafny-feat-rust' of github.com:smi…
robin-aws Jul 9, 2024
92649e1
Don’t check in implementation_from_dafny.rs any more
robin-aws Jul 9, 2024
63f9c3b
Mostly fix things up post-merge
robin-aws Jul 9, 2024
a3eee3f
Fix file layout
robin-aws Jul 9, 2024
536f73a
Merge branch 'main-1.x' of github.com:smithy-lang/smithy-dafny into r…
robin-aws Jul 9, 2024
b8ab362
update patch file
robin-aws Jul 10, 2024
42ab115
Add tests_from_dafny.rs so we can patch
robin-aws Jul 10, 2024
d880bde
Remove wrong file
robin-aws Jul 10, 2024
a8f1580
Patch test files as well for now
robin-aws Jul 10, 2024
fc033db
Undo dafny_impl change
robin-aws Jul 10, 2024
c4d3b28
Update patch
robin-aws Jul 10, 2024
1833dbb
Makefile fixes
robin-aws Jul 10, 2024
7c490e1
update patch
robin-aws Jul 10, 2024
08c8af8
Formatting
robin-aws Jul 10, 2024
dbf1849
Fix StandardLibrary
robin-aws Jul 10, 2024
9d7f307
remove tokio
robin-aws Jul 10, 2024
dc638a4
update patch
robin-aws Jul 10, 2024
7f0fde8
Unused import
robin-aws Jul 10, 2024
6e6635b
stdlib Makefile fix
robin-aws Jul 10, 2024
44bd953
Makefile comment
robin-aws Jul 10, 2024
ad467d0
Fix issue with stdlib patch not applying
robin-aws Jul 10, 2024
a815731
Partial change to put async back
robin-aws Jul 11, 2024
5ef3220
Working but messy as hell
robin-aws Jul 11, 2024
222c264
Update patch file
robin-aws Jul 11, 2024
7c06d32
Moved wrapped client into src, guarded by wrapped-client feature
robin-aws Jul 12, 2024
5a1e67d
Cleanup
robin-aws Jul 12, 2024
e729474
Update patch file
robin-aws Jul 12, 2024
af0663b
Clean up wrapped client code
robin-aws Jul 12, 2024
6bccce8
update patch files
robin-aws Jul 12, 2024
69ba357
Fix patch
robin-aws Jul 12, 2024
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 18 additions & 8 deletions SmithyDafnyMakefile.mk
Original file line number Diff line number Diff line change
Expand Up @@ -242,6 +242,7 @@ transpile_test:
-functionSyntax:3 \
-useRuntimeLib \
-out $(OUT) \
$(DAFNY_OPTIONS) \
$(if $(strip $(STD_LIBRARY)) , -library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \
$(TRANSPILE_DEPENDENCIES) \

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

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))

########################## Code-Gen targets

# The OUTPUT variables are created this way
Expand Down Expand Up @@ -296,6 +301,7 @@ _polymorph_wrapped:
$(OUTPUT_DAFNY_WRAPPED) \
$(OUTPUT_DOTNET_WRAPPED) \
$(OUTPUT_JAVA_WRAPPED) \
$(OUTPUT_RUST_WRAPPED) \
--model $(if $(DIR_STRUCTURE_V2),$(LIBRARY_ROOT)/dafny/$(SERVICE)/Model,$(LIBRARY_ROOT)/Model) \
--dependent-model $(PROJECT_ROOT)/$(SMITHY_DEPS) \
$(patsubst %, --dependent-model $(PROJECT_ROOT)/%/Model, $($(service_deps_var))) \
Expand Down Expand Up @@ -510,10 +516,11 @@ test_java:

########################## Rust targets

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

transpile_implementation_rust: TARGET=rs
transpile_implementation_rust: OUT=implementation_from_dafny
Expand All @@ -535,6 +542,9 @@ transpile_test_rust: _transpile_test_all _mv_test_rust
transpile_dependencies_rust: LANG=rust
transpile_dependencies_rust: transpile_dependencies

transpile_dependencies_test_rust: LANG=rust
transpile_dependencies_test_rust: transpile_dependencies_test

_mv_implementation_rust:
rm -rf runtimes/rust/dafny_impl/src
mkdir -p runtimes/rust/dafny_impl/src
Expand All @@ -544,10 +554,10 @@ _mv_implementation_rust:
rustfmt runtimes/rust/dafny_impl/src/implementation_from_dafny.rs
rm -rf implementation_from_dafny-rust
_mv_test_rust:
rm -rf runtimes/rust/dafny_impl/tests
mkdir -p runtimes/rust/dafny_impl/tests
mv tests_from_dafny-rust/src/tests_from_dafny.rs runtimes/rust/dafny_impl/tests/tests_from_dafny.rs
rustfmt runtimes/rust/dafny_impl/tests/tests_from_dafny.rs
rm -f runtimes/rust/tests/tests_from_dafny/mod.rs
mkdir -p runtimes/rust/tests/tests_from_dafny
mv tests_from_dafny-rust/src/tests_from_dafny.rs runtimes/rust/tests/tests_from_dafny/mod.rs
rustfmt runtimes/rust/tests/tests_from_dafny/mod.rs
rm -rf tests_from_dafny-rust

build_rust:
Expand Down
9 changes: 9 additions & 0 deletions TestModels/SharedMakefile.mk
Original file line number Diff line number Diff line change
Expand Up @@ -69,3 +69,12 @@ _polymorph_dotnet: _polymorph
_polymorph_dotnet: OUTPUT_DOTNET_WRAPPED=\
$(if $(DIR_STRUCTURE_V2), --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/Wrapped/$(SERVICE)/, --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/Wrapped)
_polymorph_dotnet: _polymorph_wrapped

_polymorph_rust: OUTPUT_RUST=--output-rust $(LIBRARY_ROOT)/runtimes/rust
_polymorph_rust: INPUT_DAFNY=\
--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy
_polymorph_rust: _polymorph
# TODO: This doesn't yet work for Rust because we are patching transpiled code,
# so this target will complain about "patch does not apply" because it was already applied.
# _polymorph_rust: OUTPUT_RUST_WRAPPED=--output-rust $(LIBRARY_ROOT)/runtimes/rust
# _polymorph_rust: _polymorph_wrapped
Original file line number Diff line number Diff line change
Expand Up @@ -62,14 +62,54 @@ index 00000000..299b0baa
+}
diff --git b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions.rs a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions.rs
new file mode 100644
index 00000000..c1acac7b
index 00000000..86f87891
--- /dev/null
+++ a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions.rs
@@ -0,0 +1,4 @@
@@ -0,0 +1,6 @@
+// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT.
+pub mod get_boolean;
+
+pub mod simple_boolean_config;
+
+pub(crate) mod error;
\ No newline at end of file
diff --git b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions/error.rs a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions/error.rs
new file mode 100644
index 00000000..d6fd32b7
--- /dev/null
+++ a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions/error.rs
@@ -0,0 +1,30 @@
+/// Wraps up an arbitrary Rust Error value as a Dafny Error
+pub fn to_opaque_error<E: std::error::Error + 'static>(value: E) ->
+ ::std::rc::Rc<::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error>
+{
+ let error_obj: ::dafny_runtime::Object<dyn::std::any::Any> =
+ ::dafny_runtime::Object(Some(::std::rc::Rc::new(
+ ::std::cell::UnsafeCell::new(value),
+ )));
+ ::std::rc::Rc::new(
+ ::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error::Opaque {
+ obj: error_obj,
+ },
+ )
+}
+
+/// Wraps up an arbitrary Rust Error value as a Dafny Result<T, Error>.Failure
+pub fn to_opaque_error_result<T: dafny_runtime::DafnyType, E: std::error::Error + 'static>(value: E) ->
+ ::std::rc::Rc<
+ dafny_standard_library::implementation_from_dafny::_Wrappers_Compile::Result<
+ T,
+ ::std::rc::Rc<::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error>
+ >
+ >
+{
+ ::std::rc::Rc::new(
+ dafny_standard_library::implementation_from_dafny::_Wrappers_Compile::Result::Failure {
+ error: to_opaque_error(value)
+ }
+ )
+}
\ No newline at end of file
diff --git b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions/get_boolean.rs a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions/get_boolean.rs
new file mode 100644
index 00000000..065d3ad3
Expand Down Expand Up @@ -287,10 +327,10 @@ index 00000000..4d66eb2e
\ No newline at end of file
diff --git b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/lib.rs a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/lib.rs
new file mode 100644
index 00000000..1d16c191
index 00000000..53977d7d
--- /dev/null
+++ a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/lib.rs
@@ -0,0 +1,17 @@
@@ -0,0 +1,20 @@
+#![allow(deprecated)]
+
+// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT.
Expand All @@ -306,6 +346,9 @@ index 00000000..1d16c191
+
+mod conversions;
+
+#[cfg(feature = "wrapped-client")]
+pub mod wrapped;
+
+pub use client::Client;
+pub use types::simple_boolean_config::SimpleBooleanConfig;
diff --git b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/operation.rs a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/operation.rs
Expand Down Expand Up @@ -719,3 +762,118 @@ index 00000000..6bf027f6
+ ::std::result::Result::Ok(SimpleBooleanConfig {})
+ }
+}
diff --git b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/wrapped.rs a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/wrapped.rs
new file mode 100644
index 00000000..39355176
--- /dev/null
+++ a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/wrapped.rs
@@ -0,0 +1 @@
+pub mod client;
\ No newline at end of file
diff --git b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/wrapped/client.rs a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/wrapped/client.rs
new file mode 100644
index 00000000..49c75f76
--- /dev/null
+++ a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/wrapped/client.rs
@@ -0,0 +1,88 @@
+use tokio::runtime::Runtime;
+
+pub struct Client {
+ wrapped: crate::client::Client,
+
+ /// A `current_thread` runtime for executing operations on the
+ /// asynchronous client in a blocking manner.
+ rt: Runtime
+}
+
+impl dafny_runtime::UpcastObject<dyn ::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::ISimpleTypesBooleanClient> for Client {
+ ::dafny_runtime::UpcastObjectFn!(dyn ::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::ISimpleTypesBooleanClient);
+}
+
+impl dafny_runtime::UpcastObject<dyn std::any::Any> for Client {
+ ::dafny_runtime::UpcastObjectFn!(dyn ::std::any::Any);
+}
+
+impl Client {
+ pub fn from_conf(config: &::std::rc::Rc<
+ ::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::SimpleBooleanConfig,
+ >) ->
+::std::rc::Rc<::simple_boolean_dafny::r#_Wrappers_Compile::Result<
+ ::dafny_runtime::Object<dyn ::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::ISimpleTypesBooleanClient>,
+ ::std::rc::Rc<::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error>
+>> {
+ let rt_result = tokio::runtime::Builder::new_current_thread()
+ .enable_all()
+ .build();
+ let rt = match rt_result {
+ Ok(x) => x,
+ Err(error) => return crate::conversions::error::to_opaque_error_result(error),
+ };
+ let result = crate::client::Client::from_conf(
+ crate::conversions::simple_boolean_config::_simple_boolean_config::from_dafny(
+ config.clone(),
+ ),
+ );
+ match result {
+ Ok(client) => {
+ let wrap = crate::wrapped::client::Client {
+ wrapped: client,
+ rt
+ };
+ std::rc::Rc::new(
+ ::simple_boolean_dafny::_Wrappers_Compile::Result::Success {
+ value: ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(wrap))
+ }
+ )
+ },
+ Err(error) => crate::conversions::error::to_opaque_error_result(error)
+ }
+ }
+}
+
+impl ::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::ISimpleTypesBooleanClient
+ for Client
+{
+ fn GetBoolean(
+ &mut self,
+ input: &std::rc::Rc<
+ ::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::GetBooleanInput,
+ >,
+ ) -> std::rc::Rc<
+ ::simple_boolean_dafny::r#_Wrappers_Compile::Result<
+ std::rc::Rc<
+ ::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::GetBooleanOutput,
+ >,
+ std::rc::Rc<::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error>,
+ >,
+ >{
+ let inner_input =
+ crate::conversions::get_boolean::_get_boolean_input::from_dafny(input.clone());
+ let result = self.rt.block_on(crate::operation::get_boolean::GetBoolean::send(&self.wrapped, inner_input));
+ match result {
+ Err(error) => ::std::rc::Rc::new(
+ ::simple_boolean_dafny::_Wrappers_Compile::Result::Failure {
+ error: crate::conversions::get_boolean::to_dafny_error(error),
+ },
+ ),
+ Ok(client) => ::std::rc::Rc::new(
+ ::simple_boolean_dafny::_Wrappers_Compile::Result::Success {
+ value: crate::conversions::get_boolean::_get_boolean_output::to_dafny(client),
+ },
+ ),
+ }
+ }
+}
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
index ce6d90a2..7f1ba031 100644
--- b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/tests/tests_from_dafny/mod.rs
+++ a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/tests/tests_from_dafny/mod.rs
@@ -1,5 +1,8 @@
#![allow(warnings, unconditional_panic)]
#![allow(nonstandard_style)]
+use ::simple_boolean_dafny::*;
+use simple_boolean::*;
+mod _wrapped;

pub mod r#_simple_dtypes_dboolean_dinternaldafny_dwrapped {
pub struct _default {}
10 changes: 8 additions & 2 deletions TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,9 @@ edition = "2021"

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

[features]
wrapped-client = []

[dependencies]
aws-smithy-runtime = {version = "1.6.0", features = ["client"] }
aws-smithy-runtime-api = {version = "1.7.0", features = ["client"] }
Expand All @@ -13,6 +16,9 @@ dafny_runtime = { path = "../../../../dafny-dependencies/dafny_runtime_rust"}
dafny_standard_library = { path = "../../../../dafny-dependencies/StandardLibrary/runtimes/rust"}
simple_boolean_dafny = { path = "./dafny_impl"}

[dev-dependencies.tokio]
[dev-dependencies]
simple_boolean = { path = ".", features = ["wrapped-client"] }

[dependencies.tokio]
version = "1.26.0"
features = ["full"]
features = ["full"]
Original file line number Diff line number Diff line change
Expand Up @@ -10,4 +10,4 @@ dafny_runtime = { path = "../../../../../dafny-dependencies/dafny_runtime_rust"}
dafny_standard_library = { path = "../../../../../dafny-dependencies/StandardLibrary/runtimes/rust"}

[lib]
path = "src/implementation_from_dafny.rs"
path = "src/implementation_from_dafny.rs"
Original file line number Diff line number Diff line change
Expand Up @@ -2,3 +2,5 @@
pub mod get_boolean;

pub mod simple_boolean_config;

pub(crate) mod error;
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
/// Wraps up an arbitrary Rust Error value as a Dafny Error
pub fn to_opaque_error<E: std::error::Error + 'static>(value: E) ->
::std::rc::Rc<::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error>
{
let error_obj: ::dafny_runtime::Object<dyn::std::any::Any> =
::dafny_runtime::Object(Some(::std::rc::Rc::new(
::std::cell::UnsafeCell::new(value),
)));
::std::rc::Rc::new(
::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error::Opaque {
obj: error_obj,
},
)
}

/// Wraps up an arbitrary Rust Error value as a Dafny Result<T, Error>.Failure
pub fn to_opaque_error_result<T: dafny_runtime::DafnyType, E: std::error::Error + 'static>(value: E) ->
::std::rc::Rc<
dafny_standard_library::implementation_from_dafny::_Wrappers_Compile::Result<
T,
::std::rc::Rc<::simple_boolean_dafny::r#_simple_dtypes_dboolean_dinternaldafny_dtypes::Error>
>
>
{
::std::rc::Rc::new(
dafny_standard_library::implementation_from_dafny::_Wrappers_Compile::Result::Failure {
error: to_opaque_error(value)
}
)
}
Original file line number Diff line number Diff line change
Expand Up @@ -13,5 +13,8 @@ pub mod operation;

mod conversions;

#[cfg(feature = "wrapped-client")]
pub mod wrapped;

pub use client::Client;
pub use types::simple_boolean_config::SimpleBooleanConfig;
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
pub mod client;
Loading
Loading