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

Conversation

robin-aws
Copy link
Contributor

@robin-aws robin-aws commented Jun 26, 2024

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.
  • 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.
  • Raised the visibility of a few things in the main crate to pub so that the dafny_tests integration test crate can see them - open to feedback here on whether it's reasonable or we should find a better solution.
    • Not necessary any more, see edit to the bullet about the wrapped client.

Not ready to merge yet because this relies on a newer Dafny feature branch commit, which I'll tackle in a separate PR first since it will be noisy to update all the patch files.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

@robin-aws robin-aws requested a review from ajewellamz June 26, 2024 16:31
robin-aws added 21 commits June 26, 2024 09:57
…thy-lang/smithy-dafny into robin-aws/dafny-tests-on-rust

# Conflicts:
#	TestModels/SimpleTypes/SimpleBoolean/codegen-patches/rust/dafny-4.5.0.patch
#	TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/dafny_impl/src/implementation_from_dafny.rs
#	TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/client.rs
#	TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/conversions/get_boolean.rs
#	TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/src/implementation_from_dafny.rs
#	TestModels/SimpleTypes/SimpleTimestamp/runtimes/rust/dafny_impl/src/implementation_from_dafny.rs
#	TestModels/dafny-dependencies/StandardLibrary/codegen-patches/rust/dafny-4.5.0.patch
#	codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/CodegenEngine.java
@robin-aws robin-aws marked this pull request as ready for review July 10, 2024 22:24
@robin-aws robin-aws requested a review from a team as a code owner July 10, 2024 22:24
@robin-aws robin-aws requested a review from andrewbanchich July 10, 2024 22:25
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The error handling code in here is all over the map, please help me use some cleaner idioms :) I can't use ? in general since r#_Wrappers_Compile::Result is not a Rust Result, but perhaps we can use Result.map_err somehow?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Did the best I could with this. :)

@robin-aws robin-aws merged commit 81dd77f into main-1.x Jul 12, 2024
68 checks passed
@robin-aws robin-aws deleted the robin-aws/dafny-tests-on-rust branch July 12, 2024 20:58
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Support Dafny tests for benerated test models
2 participants