feat: Optionally generate (mostly) complete projects (#390)

*Description of changes:*

Adds a new `--generate` option that accepts a "generation aspect" argument, and can be specified multiple times. The available aspects are:

* `project-files` - files like `build.gradle.kts` or `Service.csproj`
* `client-constructors` - externally defined [wrapped] client constructors, and similar top-level Dafny module boilerplate (open to a better name for this one)
* `impl-stubs` - stubbed out Dafny concrete operations modules and tests.

These options make it much quicker to create new libraries, especially new TestModels. The last option is intended to be used once to get started on files that do have to be manually edited, but the other two can be left on more permanently.

I set up a templated file mechanism for all these kinds of assets, since they are mostly static content with just a few pieces that depend on the service name/sdkID and other parameters. It uses [the shared `AbstractCodeWriter` templating mechanism](https://smithy.io/2.0/guides/building-codegen/generating-code.html) from the core Smithy implementation.

Also used this to generate the missing files to make `Timestamp` work for .NET (it doesn't work yet for Java because of some apparent confusion over `Date` vs. `Instant`)

.github/workflows/test_models_net_tests.yml

@@ -45,7 +45,7 @@ jobs:
             TestModels/SimpleTypes/SimpleLong,
             # TestModels/SimpleTypes/SimpleShort,
             TestModels/SimpleTypes/SimpleString,
-            # TestModels/SimpleTypes/SimpleTimestamp,
+            TestModels/SimpleTypes/SimpleTimestamp,
             TestModels/Union,
             TestModels/aws-sdks/ddb,
             TestModels/aws-sdks/glue,
@@ -99,10 +99,6 @@ jobs:
         # https://github.com/actions/setup-dotnet/blob/main/.github/csc.json
         run: echo "::remove-matcher owner=csc::"
 
-      - name: Download Dependencies
-        working-directory: ./${{ matrix.library }}
-        run: make setup_net
-
       - name: Setup Java 17 for codegen
         uses: actions/setup-java@v3
         with:
@@ -116,6 +112,10 @@ jobs:
           make polymorph_dafny DAFNY_VERSION_OPTION="--dafny-version $DAFNY_VERSION"
           make polymorph_dotnet DAFNY_VERSION_OPTION="--dafny-version $DAFNY_VERSION"
 
+      - name: Download Dependencies
+        working-directory: ./${{ matrix.library }}
+        run: make setup_net
+
       - name: Compile ${{ matrix.library }} implementation
         shell: bash
         working-directory: ./${{ matrix.library }}

.prettierignore

@@ -0,0 +1,5 @@
+# Codegen templates (often not parsable)
+codegen/smithy-dafny-codegen/src/main/resources/templates/**/*.*
+
+# Build folders (faster to ignore tons of irrelevant files)
+**/runtimes/rust/target/debug/**/*.*

SmithyDafnyMakefile.mk

@@ -292,6 +292,7 @@ _polymorph_wrapped:
 	--dafny-version $(DAFNY_VERSION) \
 	--library-root $(LIBRARY_ROOT) \
 	--properties-file $(LIBRARY_ROOT)/project.properties \
+	$(INPUT_DAFNY) \
 	$(OUTPUT_DAFNY_WRAPPED) \
 	$(OUTPUT_DOTNET_WRAPPED) \
 	$(OUTPUT_JAVA_WRAPPED) \
@@ -368,6 +369,8 @@ polymorph_dotnet:
 
 _polymorph_dotnet: OUTPUT_DOTNET=\
     $(if $(DIR_STRUCTURE_V2), --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/$(SERVICE)/, --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/)
+_polymorph_dotnet: INPUT_DAFNY=\
+		--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy
 _polymorph_dotnet: _polymorph
 
 # Generates java code for all namespaces in this project
@@ -384,6 +387,8 @@ polymorph_java:
 
 _polymorph_java: OUTPUT_JAVA=--output-java $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated
 _polymorph_java: OUTPUT_JAVA_TEST=--output-java-test $(LIBRARY_ROOT)/runtimes/java/src/test/smithy-generated
+_polymorph_java: INPUT_DAFNY=\
+	--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy
 _polymorph_java: _polymorph
 
 # Dependency for formatting generating Java code

TestModels/SharedMakefile.mk

@@ -55,12 +55,16 @@ _polymorph_dafny: _polymorph_wrapped
 
 _polymorph_java: OUTPUT_JAVA=--output-java $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated
 _polymorph_java: OUTPUT_JAVA_TEST=--output-java-test $(LIBRARY_ROOT)/runtimes/java/src/test/smithy-generated
+_polymorph_java: INPUT_DAFNY=\
+		--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy
 _polymorph_java: _polymorph
 _polymorph_java: OUTPUT_JAVA_WRAPPED=--output-java $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated
 _polymorph_java: _polymorph_wrapped
 
 _polymorph_dotnet: OUTPUT_DOTNET=\
     $(if $(DIR_STRUCTURE_V2), --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/$(SERVICE)/, --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/)
+_polymorph_dotnet: INPUT_DAFNY=\
+		--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy
 _polymorph_dotnet: _polymorph
 _polymorph_dotnet: OUTPUT_DOTNET_WRAPPED=\
     $(if $(DIR_STRUCTURE_V2), --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/Wrapped/$(SERVICE)/, --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/Wrapped)

TestModels/SimpleTypes/SimpleTimestamp/Makefile

@@ -7,6 +7,17 @@ include ../../SharedMakefile.mk
 
 NAMESPACE=simple.types.timestamp
 
+PROJECT_SERVICES := \
+	SimpleTypesTimestamp
+
+SERVICE_NAMESPACE_SimpleTypesTimestamp=simple.types.timestamp
+
+SERVICE_DEPS_SimpleTypesTimestamp :=
+
+SMITHY_DEPS=dafny-dependencies/Model/traits.smithy
+
 # This project has no dependencies 
 # DEPENDENT-MODELS:= 
 
+
+POLYMORPH_OPTIONS=--generate client-constructors,project-files

TestModels/SimpleTypes/SimpleTimestamp/src/SimpleTimestampImpl.dfy

@@ -0,0 +1,24 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+// Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
+include "../Model/SimpleTypesTimestampTypes.dfy"
+module SimpleTypesTimestampImpl refines AbstractSimpleTypesTimestampOperations {
+  datatype Config = Config
+  type InternalConfig = Config
+  predicate ValidInternalConfig?(config: InternalConfig)
+  {true}
+  function ModifiesInternalConfig(config: InternalConfig): set<object>
+  {{}}
+  predicate GetTimestampEnsuresPublicly(input: GetTimestampInput , output: Result<GetTimestampOutput, Error>)
+  {true}
+
+
+
+  method GetTimestamp ( config: InternalConfig , input: GetTimestampInput )
+    returns (output: Result<GetTimestampOutput, Error>)
+
+  {
+    var res := GetTimestampOutput(value := input.value);
+    return Success(res);
+  }
+}

TestModels/SimpleTypes/SimpleTimestamp/test/SimpleTimestampImplTest.dfy

@@ -0,0 +1,27 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+include "../src/Index.dfy"
+
+module SimpleTimestampImplTest {
+
+    import SimpleTimestamp
+    import opened SimpleTypesTimestampTypes
+    import opened Wrappers
+
+    method {:test} TestClient(){
+        var client :- expect SimpleTimestamp.SimpleTimestamp();
+
+        TestGetTimestamp(client);
+    }
+
+    method TestGetTimestamp(client: ISimpleTypesTimestampClient)
+      requires client.ValidState()
+      modifies client.Modifies
+      ensures client.ValidState()
+    {
+        var dafnyTimestamp := "2024-06-11T12:34:56";
+        var ret :- expect client.GetTimestamp(SimpleTimestamp.Types.GetTimestampInput(value:= Some(dafnyTimestamp)));
+        expect ret.value == Some(dafnyTimestamp);
+        print ret;
+    }
+}

TestModels/SimpleTypes/SimpleTimestamp/test/WrappedSimpleTimestampTest.dfy

@@ -0,0 +1,15 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+include "../src/WrappedSimpleTypesTimestampImpl.dfy"
+include "SimpleTimestampImplTest.dfy"
+
+module WrappedSimpleTypesTimestampTest {
+    import WrappedSimpleTypesTimestampService
+    import SimpleTimestampImplTest
+    import opened Wrappers
+    method{:test} GetString() {
+        var client :- expect WrappedSimpleTypesTimestampService.WrappedSimpleTimestamp();
+
+        SimpleTimestampImplTest.TestGetTimestamp(client);
+    }
+}

TestModels/aws-sdks/glue/Makefile

@@ -21,7 +21,6 @@ AWS_SDK_CMD=--aws-sdk
 # This project has no dependencies
 # DEPENDENT-MODELS:=
 
-
 # There is no wrapped target for aws-sdk types
 _polymorph_wrapped: ;
 _polymorph_wrapped_dafny: ;

TestModels/aws-sdks/lakeformation/Makefile

@@ -21,6 +21,7 @@ AWS_SDK_CMD=--aws-sdk
 # This project has no dependencies
 # DEPENDENT-MODELS:=
 
+POLYMORPH_OPTIONS=--generate project-files --generate client-constructors
 
 # There is no wrapped target for aws-sdk types
 _polymorph_wrapped: ;

codegen/smithy-dafny-codegen-cli/src/main/java/software/amazon/polymorph/CodegenCli.java

@@ -6,10 +6,12 @@
 import java.nio.file.Path;
 import java.nio.file.Paths;
 import java.util.Arrays;
+import java.util.Collections;
 import java.util.HashMap;
 import java.util.List;
 import java.util.Map;
 import java.util.Optional;
+import java.util.Set;
 import java.util.stream.Collectors;
 import org.apache.commons.cli.CommandLine;
 import org.apache.commons.cli.DefaultParser;
@@ -114,7 +116,8 @@ public static void main(String[] args) {
       .withAwsSdkStyle(cliArguments.awsSdkStyle)
       .withLocalServiceTest(cliArguments.localServiceTest)
       .withDafnyVersion(cliArguments.dafnyVersion)
-      .withUpdatePatchFiles(cliArguments.updatePatchFiles);
+      .withUpdatePatchFiles(cliArguments.updatePatchFiles)
+      .withGenerationAspects(cliArguments.generationAspects);
     cliArguments.propertiesFile.ifPresent(engineBuilder::withPropertiesFile);
     cliArguments.javaAwsSdkVersion.ifPresent(
       engineBuilder::withJavaAwsSdkVersion
@@ -275,6 +278,18 @@ private static Options getCliOptions() {
             "<optional> update patch files in <patch-files-dir> instead of applying them"
           )
           .build()
+      )
+      .addOption(
+        Option
+          .builder()
+          .longOpt("generate")
+          .desc(
+            "<optional> optional aspects to generate. Available aspects:\n" +
+            CodegenEngine.GenerationAspect.helpText()
+          )
+          .hasArgs()
+          .valueSeparator(',')
+          .build()
       );
   }
 
@@ -299,7 +314,8 @@ private record CliArguments(
     boolean awsSdkStyle,
     boolean localServiceTest,
     Optional<Path> patchFilesDir,
-    boolean updatePatchFiles
+    boolean updatePatchFiles,
+    Set<CodegenEngine.GenerationAspect> generationAspects
   ) {
     /**
      * @param args arguments to parse
@@ -384,11 +400,9 @@ static Optional<CliArguments> parse(String[] args) throws ParseException {
         .ofNullable(commandLine.getOptionValue("properties-file"))
         .map(Paths::get);
 
-      Optional<Path> includeDafnyFile = Optional.empty();
-      if (outputDafnyDir.isPresent()) {
-        includeDafnyFile =
-          Optional.of(Paths.get(commandLine.getOptionValue("include-dafny")));
-      }
+      Optional<Path> includeDafnyFile = Optional
+        .ofNullable(commandLine.getOptionValue("include-dafny"))
+        .map(Paths::get);
 
       Optional<Path> patchFilesDir = Optional
         .ofNullable(commandLine.getOptionValue("patch-files-dir"))
@@ -397,6 +411,14 @@ static Optional<CliArguments> parse(String[] args) throws ParseException {
         "update-patch-files"
       );
 
+      final String[] generationAspectOptions = Optional
+        .ofNullable(commandLine.getOptionValues("generate"))
+        .orElse(new String[0]);
+      final Set<CodegenEngine.GenerationAspect> generationAspects = Arrays
+        .stream(generationAspectOptions)
+        .map(CodegenEngine.GenerationAspect::fromOption)
+        .collect(Collectors.toSet());
+
       return Optional.of(
         new CliArguments(
           libraryRoot,
@@ -415,7 +437,8 @@ static Optional<CliArguments> parse(String[] args) throws ParseException {
           awsSdkStyle,
           localServiceTest,
           patchFilesDir,
-          updatePatchFiles
+          updatePatchFiles,
+          generationAspects
         )
       );
     }