fix(.NET): validate that MemoryStream instances are backed by an array #311
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
texastony
approved these changes
Feb 1, 2024
robin-aws
added a commit
to aws/aws-cryptographic-material-providers-library
that referenced
this pull request
Feb 13, 2024
robin-aws
added a commit
to aws/aws-cryptographic-material-providers-library
that referenced
this pull request
Mar 1, 2024
#195) Applies several fixes/improvements in order to work with newer Dafny versions. * Adds `smithy-dafny` as a submodule so that we can lock down the exact commit used to generate code, and use the tool in CI. * Updates the shared makefile with similar improvements to smithy-dafny's (hook up `--library-root` and `--patch-files-dir`, generate dependencies first) * Regenerates the checked-in code using a newer `smithy-dafny` to abstract away from the changes in Java TypeDescriptors when constructing datatypes in Dafny 4.3. This includes adding some helper methods to Dafny code for the benefit of Java external code, in the same style as smithy-lang/smithy-dafny#301 did. * Also updated various `__default` classes to use the above to avoid constructing Dafny datatypes directly. * Regenerating means that the effect of smithy-lang/smithy-dafny#311 on C# code shows up too. * Introduced `InternalResult<T, R>` to replace some internal-only uses of Dafny's compiled `Result` type, to avoid even more Dafny helper methods. * Leverage the `smithy-dafny` `<library-root>/codegen-patches[/<service>]` feature to extract out manual patch files. * This allows building with a newer version of Dafny to work despite having to regenerate code differently, in some cases by providing different patch files for different version ranges. * Cheated slightly by using this to conditionally remove an instance of `{:vcs_split_on_every_assert}` on `AwsKmsKeyring.OnDecrypt'` that is necessary on Dafny 4.2 but makes things work on Dafny 4.4 (which was not the intention of the patching feature, but also solves this problem much more cheaply than having to refactor the code to work in both versions :) * Add regenerating code to CI, either to verify that it matches what's checked in, or to pick up the necessary changes to work with newer Dafny versions. Manually verified the CI passes on the source branch with the latest Dafny nightly prerelease: https://github.com/aws/aws-cryptographic-material-providers-library/actions/runs/8039889665 Note that CI will now reject making further manual edits to generated files without capturing those edits in patch files. The error message will suggest how to update the patch files accordingly. See also https://github.com/smithy-lang/smithy-dafny/tree/main-1.x/TestModels/CodegenPatches
lucasmcdonald3
pushed a commit
to aws/aws-cryptographic-material-providers-library
that referenced
this pull request
Jun 4, 2024
#195) Applies several fixes/improvements in order to work with newer Dafny versions. * Adds `smithy-dafny` as a submodule so that we can lock down the exact commit used to generate code, and use the tool in CI. * Updates the shared makefile with similar improvements to smithy-dafny's (hook up `--library-root` and `--patch-files-dir`, generate dependencies first) * Regenerates the checked-in code using a newer `smithy-dafny` to abstract away from the changes in Java TypeDescriptors when constructing datatypes in Dafny 4.3. This includes adding some helper methods to Dafny code for the benefit of Java external code, in the same style as smithy-lang/smithy-dafny#301 did. * Also updated various `__default` classes to use the above to avoid constructing Dafny datatypes directly. * Regenerating means that the effect of smithy-lang/smithy-dafny#311 on C# code shows up too. * Introduced `InternalResult<T, R>` to replace some internal-only uses of Dafny's compiled `Result` type, to avoid even more Dafny helper methods. * Leverage the `smithy-dafny` `<library-root>/codegen-patches[/<service>]` feature to extract out manual patch files. * This allows building with a newer version of Dafny to work despite having to regenerate code differently, in some cases by providing different patch files for different version ranges. * Cheated slightly by using this to conditionally remove an instance of `{:vcs_split_on_every_assert}` on `AwsKmsKeyring.OnDecrypt'` that is necessary on Dafny 4.2 but makes things work on Dafny 4.4 (which was not the intention of the patching feature, but also solves this problem much more cheaply than having to refactor the code to work in both versions :) * Add regenerating code to CI, either to verify that it matches what's checked in, or to pick up the necessary changes to work with newer Dafny versions. Manually verified the CI passes on the source branch with the latest Dafny nightly prerelease: https://github.com/aws/aws-cryptographic-material-providers-library/actions/runs/8039889665 Note that CI will now reject making further manual edits to generated files without capturing those edits in patch files. The error message will suggest how to update the patch files accordingly. See also https://github.com/smithy-lang/smithy-dafny/tree/main-1.x/TestModels/CodegenPatches
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Issue #, if available: n/a
Description of changes: See aws/aws-encryption-sdk-dafny#633 for more info. This PR addresses the issue in the codegen library itself, so the manual edit won't be lost.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.