chore: support sync rust (#760)

smithy-lang · Jan 22, 2025 · ce73393 · ce73393
1 parent 6475c2e
commit ce73393
Show file tree

Hide file tree

Showing 82 changed files with 1,133 additions and 626 deletions.
diff --git a/.github/workflows/pull.yml b/.github/workflows/pull.yml
@@ -53,7 +53,7 @@ jobs:
         # Rust code generation is under development and depends on pending changes to the
         # Dafny Rust code generation, so we test on a specific unreleased commit instead.
         dafny-version:
-          - 5f2330113320f2af0476473fd267b5b547f94cba
+          - d07403b6d6606257e1b5aada4d0156901f4a17de
     uses: ./.github/workflows/test_models_rust_tests.yml
     with:
       dafny: ${{ matrix.dafny-version }}

diff --git a/SmithyDafnyMakefile.mk b/SmithyDafnyMakefile.mk
@@ -193,6 +193,7 @@ transpile_implementation: SRC_INDEX_TRANSPILE=$(if $(SRC_INDEX),$(SRC_INDEX),src
 # Also the expectation is that verification happens in the `verify` target
 # `find` looks for `Index.dfy` files in either V1 or V2-styled project directories (single vs. multiple model files).
 transpile_implementation:
+	dafny --version
 	find ./dafny/**/$(SRC_INDEX_TRANSPILE)/ ./$(SRC_INDEX_TRANSPILE)/ -name 'Index.dfy' | sed -e 's/^/include "/' -e 's/$$/"/' | dafny \
 	translate $(TARGET) \
 		--stdin \
@@ -231,6 +232,7 @@ _transpile_test_all: TRANSPILE_DEPENDENCIES=$(if ${DIR_STRUCTURE_V2}, $(patsubst
 _transpile_test_all: transpile_test
 
 transpile_test:
+	dafny --version
 	find ./dafny/**/$(TEST_INDEX_TRANSPILE) ./$(TEST_INDEX_TRANSPILE) -name "*.dfy" -name '*.dfy' | sed -e 's/^/include "/' -e 's/$$/"/' | dafny \
 		translate $(TARGET) \
 		--stdin \
@@ -609,7 +611,7 @@ transpile_implementation_rust: SRC_INDEX=$(RUST_SRC_INDEX)
 transpile_implementation_rust: TEST_INDEX=$(RUST_TEST_INDEX)
 # The Dafny Rust code generator is not complete yet,
 # so we want to emit code even if there are unsupported features in the input.
-transpile_implementation_rust: DAFNY_OPTIONS=--emit-uncompilable-code --allow-warnings --compile-suffix --rust-module-name implementation_from_dafny
+transpile_implementation_rust: DAFNY_OPTIONS=--emit-uncompilable-code --allow-warnings --compile-suffix --rust-module-name implementation_from_dafny --rust-sync
 # The Dafny Rust code generator only supports a single crate for everything,
 # so we inline all dependencies by not passing `-library` to Dafny.
 transpile_implementation_rust: TRANSPILE_DEPENDENCIES=
@@ -629,14 +631,15 @@ _mv_implementation_rust:
 # Pre-process the Dafny-generated Rust code to remove them.
 	sed -i -e 's/[[:space:]]*$$//' runtimes/rust/src/implementation_from_dafny.rs 
 	rm -f runtimes/rust/src/implementation_from_dafny.rs-e
-	rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs
+#	rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs
 	rm -rf implementation_from_dafny-rust
 
 build_rust:
 	cd runtimes/rust; \
 	cargo build
 
 test_rust:
+	rustc --version
 	cd runtimes/rust; \
 	cargo test --release -- --nocapture
 
@@ -776,7 +779,7 @@ local_transpile_impl_rust_single: TARGET=rs
 local_transpile_impl_rust_single: OUT=implementation_from_dafny
 local_transpile_impl_rust_single: SRC_INDEX=$(RUST_SRC_INDEX)
 local_transpile_impl_rust_single: TEST_INDEX=$(RUST_TEST_INDEX)
-local_transpile_impl_rust_single: DAFNY_OPTIONS=--emit-uncompilable-code --allow-warnings --compile-suffix
+local_transpile_impl_rust_single: DAFNY_OPTIONS=--emit-uncompilable-code --allow-warnings --compile-suffix --rust-sync
 local_transpile_impl_rust_single: TRANSPILE_DEPENDENCIES=
 local_transpile_impl_rust_single: STD_LIBRARY=
 local_transpile_impl_rust_single: SRC_INDEX_TRANSPILE=$(if $(SRC_INDEX),$(SRC_INDEX),src)

diff --git a/TestModels/.gitignore b/TestModels/.gitignore
@@ -50,6 +50,9 @@
 **/src/types.rs
 **/src/types
 **/target
+**/src/validation.rs
+**/src/wrapped
+**/src/wrapped.rs
 
 # .NET Artifacts
 **/bin

diff --git a/TestModels/Aggregate/runtimes/rust/Cargo.toml b/TestModels/Aggregate/runtimes/rust/Cargo.toml
@@ -12,7 +12,7 @@ wrapped-client = []
 aws-smithy-runtime = {version = "1.6.0", features = ["client"] }
 aws-smithy-runtime-api = {version = "1.7.0", features = ["client"] }
 aws-smithy-types = "1.2.0"
-dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust"}
+dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]}
 
 [dev-dependencies]
 simple_aggregate = { path = ".", features = ["wrapped-client"] }

diff --git a/TestModels/CallingAWSSDKFromLocalService/runtimes/rust/Cargo.toml b/TestModels/CallingAWSSDKFromLocalService/runtimes/rust/Cargo.toml
@@ -13,7 +13,7 @@ aws-config = "1.5.8"
 aws-smithy-runtime = {version = "1.7.1", features=["client"]}
 aws-smithy-runtime-api = {version = "1.7.2", features=["client"]}
 aws-smithy-types = "1.2.4"
-dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust"}
+dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]}
 aws-sdk-dynamodb = "1.50.0"
 aws-sdk-kms = "1.47.0"
 

diff --git a/TestModels/CallingAWSSDKFromLocalService/runtimes/rust/src/ddb.rs b/TestModels/CallingAWSSDKFromLocalService/runtimes/rust/src/ddb.rs
@@ -17,10 +17,10 @@ static DAFNY_TOKIO_RUNTIME: LazyLock<tokio::runtime::Runtime> = LazyLock::new(||
 
 #[allow(non_snake_case)]
 impl crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::_default {
-  pub fn DynamoDBClient() -> ::std::rc::Rc<
+    pub fn DynamoDBClient() -> ::dafny_runtime::Rc<
   crate::r#_Wrappers_Compile::Result<
     ::dafny_runtime::Object<dyn crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::IDynamoDBClient>,
-    ::std::rc::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::Error>
+    ::dafny_runtime::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::Error>
     >
     >{
         let shared_config = match tokio::runtime::Handle::try_current() {
@@ -36,7 +36,7 @@ impl crate::r#software::amazon::cryptography::services::dynamodb::internaldafny:
         let inner = aws_sdk_dynamodb::Client::new(&shared_config);
         let client = crate::deps::com_amazonaws_dynamodb::client::Client { inner };
         let dafny_client = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(client));
-        std::rc::Rc::new(crate::r#_Wrappers_Compile::Result::Success {
+        dafny_runtime::Rc::new(crate::r#_Wrappers_Compile::Result::Success {
             value: dafny_client,
         })
     }

diff --git a/TestModels/CallingAWSSDKFromLocalService/runtimes/rust/src/kms.rs b/TestModels/CallingAWSSDKFromLocalService/runtimes/rust/src/kms.rs
@@ -17,7 +17,7 @@ static DAFNY_TOKIO_RUNTIME: LazyLock<tokio::runtime::Runtime> = LazyLock::new(||
 
 impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_default {
     #[allow(non_snake_case)]
-    pub fn KMSClient() -> ::std::rc::Rc<crate::r#_Wrappers_Compile::Result<::dafny_runtime::Object<dyn crate::software::amazon::cryptography::services::kms::internaldafny::types::IKMSClient>, ::std::rc::Rc<crate::software::amazon::cryptography::services::kms::internaldafny::types::Error>>>{
+    pub fn KMSClient() -> ::dafny_runtime::Rc<crate::r#_Wrappers_Compile::Result<::dafny_runtime::Object<dyn crate::software::amazon::cryptography::services::kms::internaldafny::types::IKMSClient>, ::dafny_runtime::Rc<crate::software::amazon::cryptography::services::kms::internaldafny::types::Error>>>{
         let shared_config = match tokio::runtime::Handle::try_current() {
             Ok(curr) => tokio::task::block_in_place(|| {
                 curr.block_on(async {
@@ -32,7 +32,7 @@ impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_def
         let inner = aws_sdk_kms::Client::new(&shared_config);
         let client = crate::deps::com_amazonaws_kms::client::Client { inner };
         let dafny_client = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(client));
-        std::rc::Rc::new(crate::r#_Wrappers_Compile::Result::Success {
+        dafny_runtime::Rc::new(crate::r#_Wrappers_Compile::Result::Success {
             value: dafny_client,
         })
     }

diff --git a/TestModels/CallingAWSSDKFromLocalService/runtimes/rust/src/lib.rs b/TestModels/CallingAWSSDKFromLocalService/runtimes/rust/src/lib.rs
@@ -1,9 +1,9 @@
 #![allow(
-  deprecated,
-  non_upper_case_globals,
-  unused,
-  non_snake_case,
-  non_camel_case_types
+    deprecated,
+    non_upper_case_globals,
+    unused,
+    non_snake_case,
+    non_camel_case_types
 )]
 
 pub mod client;
@@ -14,10 +14,10 @@ pub mod error;
 pub(crate) mod implementation_from_dafny;
 /// All operations that this crate can perform.
 pub mod operation;
-pub mod validation;
 mod standard_library_conversions;
 mod standard_library_externs;
 pub mod types;
+pub mod validation;
 pub mod wrapped;
 pub(crate) use crate::implementation_from_dafny::r#_Wrappers_Compile;
 pub(crate) use crate::implementation_from_dafny::simple;
@@ -30,4 +30,4 @@ pub use crate::deps::com_amazonaws_kms;
 pub mod ddb;
 pub mod kms;
 
-pub(crate) use crate::implementation_from_dafny::software;
+pub(crate) use crate::implementation_from_dafny::software;
diff --git a/TestModels/Constraints/runtimes/rust/Cargo.toml b/TestModels/Constraints/runtimes/rust/Cargo.toml
@@ -12,7 +12,7 @@ wrapped-client = []
 aws-smithy-runtime = {version = "1.7.1", features=["client"]}
 aws-smithy-runtime-api = {version = "1.7.2", features=["client"]}
 aws-smithy-types = "1.2.4"
-dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust"}
+dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]}
 
 [dependencies.tokio]
 version = "1.26.0"

diff --git a/TestModels/Constructor/runtimes/rust/Cargo.toml b/TestModels/Constructor/runtimes/rust/Cargo.toml
@@ -11,7 +11,7 @@ wrapped-client = []
 [dependencies]
 aws-smithy-runtime-api = {version = "1.7.0", features = ["client"] }
 aws-smithy-types = "1.2.0"
-dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust"}
+dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]}
 
 [dev-dependencies]
 constructor = { path = ".", features = ["wrapped-client"] }

diff --git a/TestModels/Dependencies/runtimes/rust/Cargo.toml b/TestModels/Dependencies/runtimes/rust/Cargo.toml
@@ -11,7 +11,7 @@ wrapped-client = []
 [dependencies]
 aws-smithy-runtime-api = {version = "1.7.0", features = ["client"] }
 aws-smithy-types = "1.2.0"
-dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust"}
+dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]}
 
 [dev-dependencies]
 dependencies = { path = ".", features = ["wrapped-client"] }

diff --git a/TestModels/Documentation/runtimes/rust/Cargo.toml b/TestModels/Documentation/runtimes/rust/Cargo.toml
@@ -10,7 +10,7 @@ wrapped-client = []
 aws-smithy-runtime = {version = "1.6.0", features = ["client"] }
 aws-smithy-runtime-api = {version = "1.7.0", features = ["client"] }
 aws-smithy-types = "1.2.0"
-dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust"}
+dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]}
 
 [dev-dependencies]
 documentation = { path = ".", features = ["wrapped-client"] }

diff --git a/TestModels/Errors/runtimes/rust/Cargo.toml b/TestModels/Errors/runtimes/rust/Cargo.toml
@@ -12,7 +12,7 @@ wrapped-client = []
 aws-smithy-runtime = {version = "1.7.1", features=["client"]}
 aws-smithy-runtime-api = {version = "1.7.2", features=["client"]}
 aws-smithy-types = "1.2.4"
-dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust"}
+dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]}
 
 [dependencies.tokio]
 version = "1.26.0"

diff --git a/TestModels/Extendable/runtimes/rust/Cargo.toml b/TestModels/Extendable/runtimes/rust/Cargo.toml
@@ -12,7 +12,7 @@ wrapped-client = []
 aws-smithy-runtime = {version = "1.7.1", features=["client"]}
 aws-smithy-runtime-api = {version = "1.7.2", features=["client"]}
 aws-smithy-types = "1.2.4"
-dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust"}
+dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]}
 
 [dependencies.tokio]
 version = "1.26.0"

diff --git a/TestModels/Extendable/runtimes/rust/src/factory.rs b/TestModels/Extendable/runtimes/rust/src/factory.rs
@@ -12,7 +12,7 @@ use crate::simple::extendable::resources::internaldafny::types::GetExtendableRes
 use crate::simple::extendable::resources::internaldafny::types::GetExtendableResourceErrorsInput;
 use crate::simple::extendable::resources::internaldafny::types::GetExtendableResourceErrorsOutput;
 use crate::simple::extendable::resources::internaldafny::types::IExtendableResource;
-use std::rc::Rc;
+use ::dafny_runtime::Rc;
 
 pub mod simple {
     pub mod extendable {
@@ -30,8 +30,8 @@ pub struct NativeResource {
     pub inner: Box<dyn IExtendableResource>,
 }
 
-impl dafny_runtime::UpcastObject<dyn std::any::Any> for NativeResource {
-    dafny_runtime::UpcastObjectFn!(dyn std::any::Any);
+impl dafny_runtime::UpcastObject<::dafny_runtime::DynAny> for NativeResource {
+    dafny_runtime::UpcastObjectFn!(::dafny_runtime::DynAny);
 }
 
 impl IExtendableResource for NativeResource {

diff --git a/TestModels/Extendable/runtimes/rust/src/lib.rs b/TestModels/Extendable/runtimes/rust/src/lib.rs
@@ -11,15 +11,15 @@ pub mod conversions;
 pub mod deps;
 /// Common errors and error handling utilities.
 pub mod error;
+pub mod factory;
 pub(crate) mod implementation_from_dafny;
 /// All operations that this crate can perform.
 pub mod operation;
-pub mod validation;
 mod standard_library_conversions;
 mod standard_library_externs;
 pub mod types;
+pub mod validation;
 pub mod wrapped;
-pub mod factory;
 pub(crate) use crate::implementation_from_dafny::_SimpleExtendableResourcesTest_Compile;
 pub(crate) use crate::implementation_from_dafny::_WrappedTest_Compile;
 pub(crate) use crate::implementation_from_dafny::_Wrappers_Compile;

diff --git a/TestModels/LanguageSpecificLogic/runtimes/rust/Cargo.toml b/TestModels/LanguageSpecificLogic/runtimes/rust/Cargo.toml
@@ -12,7 +12,7 @@ wrapped-client = []
 aws-smithy-runtime = {version = "1.6.0", features = ["client"] }
 aws-smithy-runtime-api = {version = "1.7.0", features = ["client"] }
 aws-smithy-types = "1.2.0"
-dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust"}
+dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]}
 
 [dev-dependencies]
 language_specific_logic = { path = ".", features = ["wrapped-client"] }

diff --git a/TestModels/LocalService/runtimes/rust/Cargo.toml b/TestModels/LocalService/runtimes/rust/Cargo.toml
@@ -12,7 +12,7 @@ wrapped-client = []
 aws-smithy-runtime = {version = "1.6.0", features = ["client"] }
 aws-smithy-runtime-api = {version = "1.7.0", features = ["client"] }
 aws-smithy-types = "1.2.0"
-dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust"}
+dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]}
 
 [dev-dependencies]
 local_service = { path = ".", features = ["wrapped-client"] }

diff --git a/TestModels/MultipleModels/runtimes/rust/Cargo.toml b/TestModels/MultipleModels/runtimes/rust/Cargo.toml
@@ -11,7 +11,7 @@ wrapped-client = []
 [dependencies]
 aws-smithy-runtime-api = {version = "1.7.0", features = ["client"] }
 aws-smithy-types = "1.2.0"
-dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust"}
+dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]}
 
 [dev-dependencies]
 multiple_models = { path = ".", features = ["wrapped-client"] }

diff --git a/TestModels/OrphanedShapes/runtimes/rust/Cargo.toml b/TestModels/OrphanedShapes/runtimes/rust/Cargo.toml
@@ -12,7 +12,7 @@ wrapped-client = []
 aws-smithy-runtime = {version = "1.6.0", features = ["client"] }
 aws-smithy-runtime-api = {version = "1.7.0", features = ["client"] }
 aws-smithy-types = "1.2.0"
-dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust"}
+dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]}
 
 [dev-dependencies]
 simple_orphaned = { path = ".", features = ["wrapped-client"] }

diff --git a/TestModels/OrphanedShapes/runtimes/rust/src/extern_definitions.rs b/TestModels/OrphanedShapes/runtimes/rust/src/extern_definitions.rs
@@ -3,8 +3,8 @@
 
 use crate::r#_Wrappers_Compile::Result;
 use dafny_runtime::rcmut;
+use dafny_runtime::Rc;
 use std::cell::UnsafeCell;
-use std::rc::Rc;
 
 pub mod internal_ExternDefinitions_Compile {
 
@@ -14,6 +14,7 @@ pub mod internal_ExternDefinitions_Compile {
     use crate::simple::orphaned::internaldafny::types as internaldafny_types;
     use crate::simple::orphaned::internaldafny::types::*;
     use crate::types::*;
+    use dafny_runtime::Rc;
 
     impl _default {
         pub fn InitializeOrphanedStructure(
@@ -37,7 +38,7 @@ pub mod internal_ExternDefinitions_Compile {
         {
             let native_resource_ref =
                 crate::conversions::orphaned_resource::from_dafny(dafny_resource.clone());
-            let native_resource = native_resource_ref.inner.borrow();
+            let native_resource = native_resource_ref.inner.lock().unwrap();
             let native_output = native_resource.orphaned_resource_operation(
                 crate::operation::orphaned_resource_operation::OrphanedResourceOperationInput {
                     some_string: std::option::Option::Some(
@@ -52,7 +53,7 @@ pub mod internal_ExternDefinitions_Compile {
                     native_output.unwrap(),
                 );
 
-            ::std::rc::Rc::new(Result::<
+            Rc::new(Result::<
                 Rc<internaldafny_types::OrphanedResourceOperationOutput>,
                 Rc<Error>,
             >::Success {

diff --git a/TestModels/Positional/runtimes/rust/Cargo.toml b/TestModels/Positional/runtimes/rust/Cargo.toml
@@ -12,7 +12,7 @@ wrapped-client = []
 aws-smithy-runtime = {version = "1.6.0", features = ["client"] }
 aws-smithy-runtime-api = {version = "1.7.0", features = ["client"] }
 aws-smithy-types = "1.2.0"
-dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust"}
+dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]}
 
 [dev-dependencies]
 positional = { path = ".", features = ["wrapped-client"] }

diff --git a/TestModels/Refinement/runtimes/rust/Cargo.toml b/TestModels/Refinement/runtimes/rust/Cargo.toml
@@ -9,7 +9,7 @@ edition = "2021"
 aws-smithy-runtime = {version = "1.6.0", features = ["client"] }
 aws-smithy-runtime-api = {version = "1.7.0", features = ["client"] }
 aws-smithy-types = "1.2.0"
-dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust"}
+dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]}
 
 [dev-dependencies.tokio]
 version = "1.26.0"

diff --git a/TestModels/Resource/runtimes/rust/Cargo.toml b/TestModels/Resource/runtimes/rust/Cargo.toml
@@ -12,7 +12,7 @@ wrapped-client = []
 aws-smithy-runtime = {version = "1.6.0", features = ["client"] }
 aws-smithy-runtime-api = {version = "1.7.0", features = ["client"] }
 aws-smithy-types = "1.2.0"
-dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust"}
+dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust", features = ["sync"]}
 
 [dev-dependencies]
 simple_resources = { path = ".", features = ["wrapped-client"] }

diff --git a/TestModels/Resource/runtimes/rust/src/lib.rs b/TestModels/Resource/runtimes/rust/src/lib.rs
@@ -14,10 +14,10 @@ pub mod error;
 pub(crate) mod implementation_from_dafny;
 /// All operations that this crate can perform.
 pub mod operation;
-pub mod validation;
 mod standard_library_conversions;
 mod standard_library_externs;
 pub mod types;
+pub mod validation;
 pub mod wrapped;
 pub(crate) use crate::implementation_from_dafny::r#_Wrappers_Compile;
 pub(crate) use crate::implementation_from_dafny::simple;