search

smithy-lang / smithy-dafny

Apache License 2.0
7 stars 8 forks source link

feat: Add support for smithy.test#smokeTests for Java #355

Closed robin-aws closed 1 month ago

robin-aws commented 1 month ago

Issue #, if available:

Fixes #298

Description of changes:

This trait is ideal for filling a testing gap in our TestModels. Because our strategy for mapping Smithy shapes to Dafny types enforces constraints statically, it's not possible to express invalid input without lying to Dafny through axioms that aren't actually true, or in some cases (such as @required) not possible at all. smokeTests instances generate tests that specify inputs at the Smithy level using document types (i.e. more or less JSON valued arguments to the trait), which generate target language tests using the customer-facing interfaces such as builders to create input, and can therefore express invalid input as well.

The key new component in the implementation is the ModeledShapeValue.shapeValue method, which creates a code block in Java expressing the given Shape value. Similar logic already appears in other smithy code generators, although mostly for HTTP Protocol Compliance Tests instead. I mainly imitated the structure of smithy-python's logic, but was also inspired by smithy-typescript and smithy-rs.

Because this feature introduces a new category of generated code (Smithy-generated tests) this PR also adds an --output-java-test option with SmithyDafnyMakefile.mk support. We will likely need to add a similar parameter for the other languages. It may make more sense to migrate to smithy-build.json first though: https://github.com/smithy-lang/smithy-dafny/issues/356.

It also adds ./gradlew test as an additional step for make test_java, since running the Java @Tests is distinct from executing the transpiled dafny test program.

Finally, it also improves the CLI interface to print out validation events even if there are only warnings. Besides providing previously hidden but useful information in general, this provides a way to warn against using smokeTests outside of test models - since it doesn't/can't support @reference shapes it's not terribly useful as a testing method for local services themselves.

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 commented 1 month ago

I left a blocking comment that is not really blocking,

but I do wish we would not put in a Reference Trait Validator

that we know only validates a particular condition...

That is asking any user to look up what it does,

rather than telling them in the name that it is limited.

I actually made a commit to do this and thought I pushed before merging, but the push failed without my noticing. :P I've queued it up for my next PR though.