Skip to content

Commit

Permalink
Enable full SDK test models in Rust (#584)
Browse files Browse the repository at this point in the history
Enables the KMS and DDB test models in Rust, mainly by hooking up union support for SDK wrappers as well, plus some miscellaneous bug fixes and some special cases where I've given up on inferring the smithy-rs logic for now.

Both test models needed an extern to implement client creation externs, which I borrowed from https://github.com/aws/aws-database-encryption-sdk-dynamodb/tree/ajewell/rust/releases/rust/db_esdk/src

Also added top-level make <lang> Makefile targets for fully generating and building all code for a given language!
  • Loading branch information
robin-aws authored Oct 2, 2024
1 parent 55c68f4 commit eb6ea03
Show file tree
Hide file tree
Showing 82 changed files with 677 additions and 469 deletions.
10 changes: 9 additions & 1 deletion SmithyDafnyMakefile.mk
Original file line number Diff line number Diff line change
Expand Up @@ -450,6 +450,8 @@ _polymorph_rust: $(if $(RUST_BENERATED), , _polymorph)

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

net: polymorph_dafny transpile_net polymorph_net test_net

transpile_net: $(if $(ENABLE_EXTERN_PROCESSING), _with_extern_pre_transpile, )
transpile_net: | transpile_implementation_net transpile_test_net transpile_dependencies_net
transpile_net: $(if $(ENABLE_EXTERN_PROCESSING), _with_extern_post_transpile, )
Expand Down Expand Up @@ -499,6 +501,8 @@ format_net-check:

########################## Java targets

java: polymorph_dafny transpile_java polymorph_java build_java test_java

build_java: transpile_java mvn_local_deploy_dependencies
$(GRADLEW) -p runtimes/java build

Expand Down Expand Up @@ -553,6 +557,8 @@ test_java:

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

rust: polymorph_dafny transpile_rust polymorph_rust test_rust

# The Dafny Rust code generator only supports a single crate for everything,
# so (among other consequences) we compile src and test code together.
transpile_rust: | transpile_implementation_rust transpile_dependencies_rust
Expand Down Expand Up @@ -583,7 +589,7 @@ _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

rustfmt runtimes/rust/src/implementation_from_dafny.rs
rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs
rm -rf implementation_from_dafny-rust

patch_after_transpile_rust:
Expand Down Expand Up @@ -632,6 +638,8 @@ clean: _clean

########################## Python targets

net: polymorph_dafny transpile_python polymorph_python test_python

# Python MUST transpile dependencies first to generate .dtr files
transpile_python: $(if $(ENABLE_EXTERN_PROCESSING), _no_extern_pre_transpile, )
transpile_python: | transpile_dependencies_python transpile_implementation_python transpile_test_python
Expand Down
11 changes: 5 additions & 6 deletions TestModels/aws-sdks/ddb-lite/runtimes/rust/src/client.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,8 @@
use std::sync::LazyLock;
use crate::conversions;

struct Client {
inner: aws_sdk_dynamodb::Client
pub struct Client {
pub inner: aws_sdk_dynamodb::Client
}

/// A runtime for executing operations on the asynchronous client in a blocking manner.
Expand All @@ -27,7 +27,7 @@ impl dafny_runtime::UpcastObject<dyn crate::r#software::amazon::cryptography::se

impl crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::IDynamoDBClient
for Client {
fn BatchExecuteStatement(&mut self, input: &std::rc::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchExecuteStatementInput>)
fn BatchExecuteStatement(&mut self, input: &std::rc::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchExecuteStatementInput>)
-> std::rc::Rc<crate::r#_Wrappers_Compile::Result<
std::rc::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchExecuteStatementOutput>,
std::rc::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::Error>
Expand Down Expand Up @@ -206,9 +206,8 @@ impl crate::r#software::amazon::cryptography::services::dynamodb::internaldafny:
crate::standard_library_conversions::result_to_dafny(&native_result,
conversions::update_item::_update_item_response::to_dafny,
conversions::update_item::to_dafny_error)
} }

#[allow(non_snake_case)]
}
} #[allow(non_snake_case)]
impl crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::_default {
pub fn DynamoDBClient() -> ::std::rc::Rc<
crate::r#_Wrappers_Compile::Result<
Expand Down
Original file line number Diff line number Diff line change
@@ -1,110 +1,129 @@
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0
// Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT.

#[allow(dead_code)]
pub fn to_dafny(
value: &aws_sdk_dynamodb::types::AttributeValue,
) -> ::std::rc::Rc<crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue>{
::std::rc::Rc::new(
match value {
aws_sdk_dynamodb::types::AttributeValue::B(x) =>
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::B {
B: crate::standard_library_conversions::blob_to_dafny(x)
},
aws_sdk_dynamodb::types::AttributeValue::Bool(x) =>
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::BOOL {
BOOL: *x
},
aws_sdk_dynamodb::types::AttributeValue::Bs(x) =>
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::BS {
BS: dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, crate::standard_library_conversions::blob_to_dafny)
},
aws_sdk_dynamodb::types::AttributeValue::L(x) =>
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::L {
L: dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x, to_dafny)
},
aws_sdk_dynamodb::types::AttributeValue::M(x) =>
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::M {
M: dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x,
|s| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&s),
to_dafny)
},
aws_sdk_dynamodb::types::AttributeValue::N(x) =>
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::N {
N: dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&x)
},
aws_sdk_dynamodb::types::AttributeValue::Ns(x) =>
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::NS {
NS: dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x,
|s| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(s))
},
aws_sdk_dynamodb::types::AttributeValue::Null(x) =>
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::NULL {
NULL: *x
},
) -> ::std::rc::Rc<
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue,
> {
::std::rc::Rc::new(match value {
aws_sdk_dynamodb::types::AttributeValue::S(x) =>
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::S {
S: dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&x)
},
aws_sdk_dynamodb::types::AttributeValue::Ss(x) =>
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::SS {
SS: dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x,
|s| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(s))
},
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::S {
S: dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&x),
},
aws_sdk_dynamodb::types::AttributeValue::N(x) =>
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::N {
N: dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&x),
},
aws_sdk_dynamodb::types::AttributeValue::B(x) =>
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::B {
B: crate::standard_library_conversions::blob_to_dafny(&x),
},
aws_sdk_dynamodb::types::AttributeValue::Ss(x) =>
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::SS {
SS: ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&x,
|e| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&e),
)
,
},
aws_sdk_dynamodb::types::AttributeValue::Ns(x) =>
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::NS {
NS: ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&x,
|e| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&e),
)
,
},
aws_sdk_dynamodb::types::AttributeValue::Bs(x) =>
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::BS {
BS: ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&x,
|e| crate::standard_library_conversions::blob_to_dafny(&e),
)
,
},
aws_sdk_dynamodb::types::AttributeValue::M(x) =>
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::M {
M: ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(&x.clone(),
|k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k),
|v| crate::conversions::attribute_value::to_dafny(&v)
,
)
,
},
aws_sdk_dynamodb::types::AttributeValue::L(x) =>
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::L {
L: ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&x,
|e| crate::conversions::attribute_value::to_dafny(&e)
,
)
,
},
aws_sdk_dynamodb::types::AttributeValue::Null(x) =>
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::NULL {
NULL: x.clone(),
},
aws_sdk_dynamodb::types::AttributeValue::Bool(x) =>
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::BOOL {
BOOL: x.clone(),
},
_ => panic!("Unknown union variant: {:?}", value),
}
)
})
}

#[allow(dead_code)]
pub fn from_dafny(
dafny_value: ::std::rc::Rc<
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue,
>,
) -> aws_sdk_dynamodb::types::AttributeValue {
match &*dafny_value {
crate::software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::S { S } =>
aws_sdk_dynamodb::types::AttributeValue::S(
dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(S)
),
crate::software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::N { N } =>
aws_sdk_dynamodb::types::AttributeValue::N(
dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(N)
),
crate::software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::B { B } =>
aws_sdk_dynamodb::types::AttributeValue::B(
crate::standard_library_conversions::blob_from_dafny(B.clone())
),
crate::software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::SS { SS } =>
aws_sdk_dynamodb::types::AttributeValue::Ss(
dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(SS,
dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string)
),
crate::software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::NS { NS } =>
aws_sdk_dynamodb::types::AttributeValue::Ss(
dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(NS,
dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string)
),
crate::software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::BS { BS } =>
aws_sdk_dynamodb::types::AttributeValue::Bs(
dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(BS,
|b| crate::standard_library_conversions::blob_from_dafny(b.clone()))
),
crate::software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::M { M } =>
aws_sdk_dynamodb::types::AttributeValue::M(
dafny_runtime::dafny_runtime_conversions::dafny_map_to_hashmap(M,
dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string,
|v| from_dafny(v.clone()))
),
crate::software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::L { L } =>
aws_sdk_dynamodb::types::AttributeValue::L(
dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(L,
|v| from_dafny(v.clone()))
),
crate::software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::NULL { NULL } =>
aws_sdk_dynamodb::types::AttributeValue::Null(*NULL),
crate::software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::BOOL { BOOL } =>
aws_sdk_dynamodb::types::AttributeValue::Bool(*BOOL),
}
match &::std::rc::Rc::unwrap_or_clone(dafny_value) {
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::S {
S: x @ _,
} => aws_sdk_dynamodb::types::AttributeValue::S(dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(x)),
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::N {
N: x @ _,
} => aws_sdk_dynamodb::types::AttributeValue::N(dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(x)),
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::B {
B: x @ _,
} => aws_sdk_dynamodb::types::AttributeValue::B(crate::standard_library_conversions::blob_from_dafny(x.clone())),
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::SS {
SS: x @ _,
} => aws_sdk_dynamodb::types::AttributeValue::Ss(::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(x,
|e| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(e),
)
),
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::NS {
NS: x @ _,
} => aws_sdk_dynamodb::types::AttributeValue::Ns(::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(x,
|e| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(e),
)
),
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::BS {
BS: x @ _,
} => aws_sdk_dynamodb::types::AttributeValue::Bs(::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(x,
|e| crate::standard_library_conversions::blob_from_dafny(e.clone()),
)
),
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::M {
M: x @ _,
} => aws_sdk_dynamodb::types::AttributeValue::M(::dafny_runtime::dafny_runtime_conversions::dafny_map_to_hashmap(&x,
|k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(k),
|v| crate::conversions::attribute_value::from_dafny(v.clone())
,
)
),
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::L {
L: x @ _,
} => aws_sdk_dynamodb::types::AttributeValue::L(::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(x,
|e| crate::conversions::attribute_value::from_dafny(e.clone())
,
)
),
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::NULL {
NULL: x @ _,
} => aws_sdk_dynamodb::types::AttributeValue::Null(x .clone()),
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::BOOL {
BOOL: x @ _,
} => aws_sdk_dynamodb::types::AttributeValue::Bool(x .clone()),
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ pub fn to_dafny(
::std::rc::Rc::new(
crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValueUpdate::AttributeValueUpdate {
Value: ::std::rc::Rc::new(match &value.value {
Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::attribute_value::to_dafny(x) },
Some(x) => crate::_Wrappers_Compile::Option::Some { value: crate::conversions::attribute_value::to_dafny(&x) },
None => crate::_Wrappers_Compile::Option::None { }
})
,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ pub fn to_dafny(
>{
::std::rc::Rc::new(crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchExecuteStatementInput::BatchExecuteStatementInput {
Statements: ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&value.statements.clone().unwrap(),
|e| crate::conversions::batch_statement_request::to_dafny(e)
|e| crate::conversions::batch_statement_request::to_dafny(&e)
,
)
,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ pub fn to_dafny(
Responses: ::std::rc::Rc::new(match &value.responses {
Some(x) => crate::r#_Wrappers_Compile::Option::Some { value :
::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x,
|e| crate::conversions::batch_statement_response::to_dafny(e)
|e| crate::conversions::batch_statement_response::to_dafny(&e)
,
)
},
Expand All @@ -21,7 +21,7 @@ pub fn to_dafny(
ConsumedCapacity: ::std::rc::Rc::new(match &value.consumed_capacity {
Some(x) => crate::r#_Wrappers_Compile::Option::Some { value :
::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x,
|e| crate::conversions::consumed_capacity::to_dafny(e)
|e| crate::conversions::consumed_capacity::to_dafny(&e)
,
)
},
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ pub fn to_dafny(
::std::rc::Rc::new(crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::types::BatchGetItemInput::BatchGetItemInput {
RequestItems: ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(&value.request_items.clone().unwrap(),
|k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k),
|v| crate::conversions::keys_and_attributes::to_dafny(v)
|v| crate::conversions::keys_and_attributes::to_dafny(&v)
,
)
,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ pub fn to_dafny(
|v| ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&v,
|e| ::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(&e.clone(),
|k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k),
|v| crate::conversions::attribute_value::to_dafny(v)
|v| crate::conversions::attribute_value::to_dafny(&v)
,
)
,
Expand All @@ -32,7 +32,7 @@ pub fn to_dafny(
Some(x) => crate::r#_Wrappers_Compile::Option::Some { value :
::dafny_runtime::dafny_runtime_conversions::hashmap_to_dafny_map(x,
|k| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&k),
|v| crate::conversions::keys_and_attributes::to_dafny(v)
|v| crate::conversions::keys_and_attributes::to_dafny(&v)
,
)
},
Expand All @@ -42,7 +42,7 @@ pub fn to_dafny(
ConsumedCapacity: ::std::rc::Rc::new(match &value.consumed_capacity {
Some(x) => crate::r#_Wrappers_Compile::Option::Some { value :
::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x,
|e| crate::conversions::consumed_capacity::to_dafny(e)
|e| crate::conversions::consumed_capacity::to_dafny(&e)
,
)
},
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ pub fn to_dafny(
Parameters: ::std::rc::Rc::new(match &value.parameters {
Some(x) => crate::r#_Wrappers_Compile::Option::Some { value :
::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(x,
|e| crate::conversions::attribute_value::to_dafny(e)
|e| crate::conversions::attribute_value::to_dafny(&e)
,
)
},
Expand Down
Loading

0 comments on commit eb6ea03

Please sign in to comment.