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

[robin-aws]

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: #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.

[texastony]

Blocking on resolving if consuming packages (MPL, DB-ESDK) can use TestNG & JUint simultaneously.

[texastony]

Issue-ish: The DB-ESDK is already using TestNG as it's test platform.
As is the MPL-Java.

Our Options:

1. Figure out if TestNG & JUnit can co-exist in the same Gradle project (maybe a as different targets?)
2. Have Smithy-Dafny use TestNG
3. Have DB-ESDK use JUnit
4. Something else?

[robin-aws]

Ah interesting I wasn't aware. I only went with JUnit as a fairly arbitrary default, so I'll just switch to TestNG to avoid unnecessary complexity.

[texastony]

If the Scope of Smoke Test does not include "consuming" libraries, this issue can be resolved.

[robin-aws]

The primary focus is definitely testing smithy-dafny itself since that's where it's the most valuable, and given it can't support @references I don't see it being useful for a lot of library operations. But it's very easy to switch to TestNG to avoid the potential incompatibility down the road so I'm happy to do it.

[texastony]

Suggested change

	* ModelCodegen generates tests for the content of the Subject's Model package.
	* ModelTestCodegen generates tests for the content of the Subject's Model package.

[texastony]

Question: It has been a while since I looked at this,
but how does memberShape.getTarget handle indirect references?

Like a reference to a Keyring?

I recall I had to write a bunch of defrencing logic to handle that.

[robin-aws]

Ah great question. You're talking about how to handle @references shapes in other words.

In practical terms smokeTests isn't going to be able to handle that, because resources aren't expressible as a simple Node literal. You need at least a sequence of calls: one call to say Create***Keyring to create a reference, and then another call to bind that as input to another call. I can imagine having a more beefed-up version of specifying a test that supports sequences, but it gets a lot more complicated real fast, and at that point I think you're better off writing a Dafny test instead so you're using a proper language.

But this does make me realize that I should raise an explicit error if the shape has @references on it, in case someone tries to misuse this by accident.

[texastony]

This is a good answer, but it raises another question.

Can you, with documentation only, state what the scope of Smoke Test is?

It sounds like it is for Testing Smithy-Dafny ONLY, at least today.
As compared to testing Smithy-Dafny's MPL or DB-ESDK generated artifacts.
(Because those would need @references support.)

This a very reasonable (and valuable!) scope,
but we need to tell people.

[robin-aws]

Ah I had it in my todos to consider adding something under designs for this, but I think the easiest place is to add a case under https://github.com/smithy-lang/smithy-dafny/tree/main-1.x/TestModels#testing-patterns, so I'll do that.

I'm also going to note more visibility that the way we have mapped shapes to Dafny types makes it impossible to implement smokeTests for Dafny, which is fine but not obvious.

[texastony]

designs is buried from users, as is Testing-Patterns.

The output-java-test argument you added only supports Smoke-Tests, correct?

That is GREAT spot to tell users this is for internal testing only.

Adding some comments to the implementations should inform any Smithy-Dafny contributors.

And this really is only for internal testing,
as @references is a prominent Smithy-Dafny feature.

[robin-aws]

The output-java-test argument you added only supports Smoke-Tests, correct?

At the moment yes, but there are other Smithy traits that could generate tests in the future (existing ones like those in https://smithy.io/2.0/additional-specs/http-protocol-compliance-tests.html or future ones we might invent ourselves) and they wouldn't necessarily be internal-only, so it feels a little wrong to give a warning there.

I think it would be better to create a direct warning on the use of smokeTests outside of the test models. There might be a clean way to do that based on metadata suppressions, let me experiment.

[texastony]

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.

[texastony]

Suggested change

	The `Contraints` test model currently tries to force Dafny code to compile to invalid input
	by using `assume {:axiom}` statements to lie to the verifier.
	This is technically relying on undefined behavior and hence not guaranteed to keep working,
	and cannot force Dafny to not provide `@required` values to boot.
	They should be refactored to use `smokeTests` instead once language support is complete.
	The `Contraints` test model currently (2024/05/10) tries to force Dafny code to compile to invalid input
	by using `assume {:axiom}` statements to lie to the verifier.
	This is technically relying on undefined behavior and hence not guaranteed to keep working,
	and cannot force Dafny to not provide `@required` values to boot.
	They should be refactored to use `smokeTests` instead once language support is complete.

[texastony]

Blocking: TODO logic has continually bitten us in the ass (see .NET constraints issue).

Can you just scope this class down?

i.e: Call it what it does right now?

Suggested change

	* This is not yet complete, especially since there are existing
	* models out there misusing the trait.
	* For now, we're only validating that smokeTests.params values
	* never try to bind a node value to a reference shape,
	* since there's no way to express a reference as a literal node value.
	*/
	public class ReferenceTraitValidator extends AbstractValidator {
	* For now, we're only validating that smokeTests.params values
	* never try to bind a node value to a reference shape,
	* since there's no way to express a reference as a literal node value.
	* We could expand this to a proper {@code ReferenceTraitValidator} in the future.
	*/
	public class ReferenceTraitNotInSmokeTestValidator extends AbstractValidator {

[robin-aws]

I think this is fair. It's not really customer-facing since having more validation error show up later with the validation event id of "ReferenceTrait" is reasonable. But I can see that the previous name gives implementors a false sense of confidence.

We do have #315 to track the gap.

[robin-aws]

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.