feat: add constraint checking for dotnet #336

ajewellamz · 2024-04-10T01:40:37Z

Description of changes:

This ONLY addresses constraint checking for dotnet

pull/257 will address rejecting any types, traits or constraints that we do not or cannot handle properly.

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

seebees · 2024-04-10T19:57:34Z

TestModels/Constraints/test/Helpers.dfy

is this all just formatting?

No, I completely re-did the helpers, into something that actually helped.

seebees · 2024-04-10T19:58:44Z

TestModels/Constraints/Model/Constraints.smithy

-@uniqueItems
-list MyUniqueList {
-  member: String
-}
+// we don't do uniqueItems yet
+// @uniqueItems
+// list MyUniqueList {
+//   member: String
+// }


We don't support them in .Net. We also don't have any code in Java?
Do we add an error if someone tries to do this?

That's a different topic.
pull/257 is responsible for "we don't support that" errors.

seebees · 2024-04-10T20:03:11Z

TestModels/Constraints/test/SimpleConstraintsImplTest.dfy

+      // This client is NOT wrapped
+      // Therefore, it does not do any constraint testing


I think we want to add this above or something. The point here, is that by not wrapping these things we are relying on Dafny verification. And the fact that this succeeds may imply a soundness bug in the callers code. As opposed to just "well, we don't check it" :)

Going further, given the extensive testing on the wrapped side, does this test serve any value? would it be better to do nothing here and explain that this is all verified by Dafny and so testing is not useful?

Yes, this test shows that the unwrapped client behaves as expected.
It's not especially interesting, I'll admit, but it seems a reasonable thing to test.

seebees · 2024-04-10T20:05:36Z

TestModels/Constraints/test/WrappedSimpleConstraintsTest.dfy

+    ensures client.ValidState()
+  {
+    var input := GetValidInput();
+    input := input.(StringLessThanOrEqualToTen := Some(ForceStringLessThanOrEqualToTen("this string is really way too long")));


Given the conversations about how strings are complicated would it be better to not support this at all?

That's a different topic.
pull/257 is responsible for "we don't support that" errors.
This PR makes dotnet behave the same as Java.

seebees · 2024-04-10T20:07:51Z

...afny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/TypeConversionCodegen.java

@@ -251,6 +259,100 @@ public TypeConverter generateBooleanConverter(final BooleanShape booleanShape) {
        return buildConverterFromMethodBodies(booleanShape, fromDafnyBody, toDafnyBody);
    }

+    public String generateStringConstraints(final Shape shape, final String value) {


Again is it better to not support strings at all? Given dafny unicode false support?

Again, that's a different topic.
pull/257 is responsible for "we don't support that" errors.
This PR makes dotnet behave the same as Java.
I suppose that part pf pull/257 might be to rip these out, since the smithy file will have to remove any length constraints on strings.

texastony · 2024-04-10T20:46:20Z

TestModels/Constraints/test/WrappedSimpleConstraintsTest.dfy

+    var input := GetValidInput();
+    input := input.(OneToTen := Some(ForceOneToTen(1000)));
+    var ret := client.GetConstraints(input := input);
+    expect ret.Failure?;


Nit/Issue: I keep running into tests where we just expect ret.Failure? and do not validate what caused the failure or what the failure was.

These tests sometimes mask bugs.
As an example, there is a test that asserts that if no Branch Key ID exists,
the Keystore's Get* methods for that Branch Key ID will fail.

And the Keystore does fail!
But with a bizarre KMS Exception that no customer could use to realize they were asking for a non-existance Branch Key ID.

Is it possible to bulk replace ret.Failure? here with something like ret.Failure? AND ret.Failure == IllegalInputException?

I agree completely, but unfortunately, the error is an Opaque error that came from an exception, and there's no way (as far as I know) to get the actual exception type or the error text out of an Opaque error.
Further, things will likely be different between Java and Dotnet, even if we could get at that stuff; since the errors are generated from custom native code.

I just logged in to write the same thing.
Which is a pretty severe limitation of this Test Model approach we have endorsed.

@seebees And @robin-aws for awareness.

Not that we are going to take any action to resolve this, but we should bear in mind that our limited error expressions mixed with our wrapping test strategy ensures we can never assert the exception type.

lucasmcdonald3 · 2024-04-10T22:48:18Z

TestModels/Constraints/test/Helpers.dfy

+
+  function method ForceLessThanTen(value : int) : LessThanTen
+  {
+    assume {:axiom} ValidInt32(value);


We might want to loop in @robin-aws.
He pushed back on testing failure cases for SimpleConstraints using assume statements.
(I am on board with what you've done)

texastony · 2024-04-11T19:12:43Z

...afny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/TypeConversionCodegen.java

        final TokenTree fromDafnyBody = Token.of("return value;");
-        final TokenTree toDafnyBody = Token.of("return value;");
+        final TokenTree toDafnyBody = Token.of(constraints + "return value;");


Blocking: Are we not putting these into the validate method?
It appears we pushing these constraint checks into the Type Conversion Methods,
which definitely would solve the problem.

But I thought the plan was to put them in structure's validate method,
and then ensure validate is always called in the toDafnyBody methods.

@ajewellamz and @texastony chatted on a call.
My dreams of a useful and complete Validate method are punted to another day.
But @ajewellamz in this PR or a very fast follow will ensure that Validate is called in the to Dafny methods for all structures.

I think I am going to leave this PR blocked until that is done,
but if @ajewellamz tells me that he really wants to do it another PR,
I will yield.

texastony

Most Groovy.
Thank you @ajewellamz

texastony · 2024-04-12T00:07:15Z

...afny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/TypeConversionCodegen.java

+        String validate = "value.Validate();";
+        if (AwsSdkNameResolverHelpers.isInAwsSdkNamespace(structureShape.getId())) {
+            validate = "";
+        }


feat: add constraint checking for dotnet

d635327

ajewellamz requested a review from a team as a code owner April 10, 2024 01:40

ajewellamz added 4 commits April 9, 2024 21:50

m

f30210d

m

318478f

cleanup

dbd302f

cleanup

c2a811b

seebees reviewed Apr 10, 2024

View reviewed changes

texastony reviewed Apr 10, 2024

View reviewed changes

lucasmcdonald3 reviewed Apr 10, 2024

View reviewed changes

texastony approved these changes Apr 11, 2024

View reviewed changes

texastony requested changes Apr 11, 2024

View reviewed changes

ajewellamz added 3 commits April 11, 2024 16:37

call validate

ce2d493

fix

4062888

noAwsSdk

6ec244c

texastony approved these changes Apr 12, 2024

View reviewed changes

ajewellamz merged commit e631c8f into main-1.x Apr 12, 2024
125 checks passed

ajewellamz deleted the ajewell/constraints branch April 12, 2024 11:19

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: add constraint checking for dotnet #336

feat: add constraint checking for dotnet #336

ajewellamz commented Apr 10, 2024

seebees Apr 10, 2024

ajewellamz Apr 10, 2024

seebees Apr 10, 2024

ajewellamz Apr 10, 2024

seebees Apr 10, 2024

seebees Apr 10, 2024

ajewellamz Apr 10, 2024

seebees Apr 10, 2024

ajewellamz Apr 10, 2024

seebees Apr 10, 2024

ajewellamz Apr 10, 2024

texastony Apr 10, 2024

ajewellamz Apr 10, 2024

texastony Apr 11, 2024

lucasmcdonald3 Apr 10, 2024 •

edited

Loading

texastony Apr 11, 2024

texastony Apr 11, 2024

texastony left a comment

texastony Apr 12, 2024

		// This client is NOT wrapped
		// Therefore, it does not do any constraint testing

feat: add constraint checking for dotnet #336

feat: add constraint checking for dotnet #336

Conversation

ajewellamz commented Apr 10, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

lucasmcdonald3 Apr 10, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

texastony left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

lucasmcdonald3 Apr 10, 2024 •

edited

Loading