From 8dd48da9d0ceb5c2ec4f6b773d3e2cb16f7b31bc Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Mon, 12 Aug 2024 14:25:10 -0700 Subject: [PATCH] wip --- SmithyDafnyMakefile.mk | 78 ++++++++++++++++++- TestModels/Aggregate/Makefile | 14 ++++ TestModels/SimpleTypes/SimpleBlob/Makefile | 14 ++++ .../SimpleTypes/SimpleBlob/src/Index.dfy | 2 +- .../SimpleBlob/src/WrappedSimpleBlobImpl.dfy | 2 +- TestModels/SimpleTypes/SimpleBoolean/Makefile | 14 ++++ .../SimpleTypes/SimpleBoolean/src/Index.dfy | 2 +- .../src/WrappedSimpleBooleanImpl.dfy | 2 +- TestModels/SimpleTypes/SimpleDouble/Makefile | 14 ++++ .../SimpleTypes/SimpleDouble/src/Index.dfy | 2 +- .../SimpleDouble/src/WrappedIndex.dfy | 3 +- TestModels/SimpleTypes/SimpleEnum/Makefile | 14 ++++ .../smithydafny/DafnyApiCodegen.java | 5 +- 13 files changed, 157 insertions(+), 9 deletions(-) diff --git a/SmithyDafnyMakefile.mk b/SmithyDafnyMakefile.mk index e89779fe8..1a96d54d9 100644 --- a/SmithyDafnyMakefile.mk +++ b/SmithyDafnyMakefile.mk @@ -56,6 +56,14 @@ SMITHY_MODEL_ROOT := $(LIBRARY_ROOT)/Model CODEGEN_CLI_ROOT := $(SMITHY_DAFNY_ROOT)/codegen/smithy-dafny-codegen-cli GRADLEW := $(SMITHY_DAFNY_ROOT)/codegen/gradlew +# On macOS, sed requires an extra parameter of "" +OS := $(shell uname) +ifeq ($(OS), Darwin) + SED_PARAMETER := "" +else + SED_PARAMETER := +endif + ########################## Dafny targets # TODO: This target will not work for projects that use `replaceable` @@ -151,6 +159,74 @@ clean-dafny-report: # Dafny helper targets +_no_extern_pre_transpile: _no_extern_pre_transpile_dependencies _sed_index_file_remove_extern _sed_types_file_remove_extern _sed_wrapped_types_file_remove_extern +_no_extern_post_transpile: _no_extern_post_transpile_dependencies _sed_types_file_add_extern _sed_index_file_add_extern _sed_wrapped_types_file_add_extern + +_no_extern_pre_transpile_dependencies: + $(patsubst %, $(MAKE) -C $(PROJECT_ROOT)/% _no_extern_pre_transpile;, $(PROJECT_DEPENDENCIES)) + +_no_extern_post_transpile_dependencies: + $(patsubst %, $(MAKE) -C $(PROJECT_ROOT)/% _no_extern_post_transpile;, $(PROJECT_DEPENDENCIES)) + +_sed_types_file_remove_extern: + $(MAKE) _sed_file SED_FILE_PATH=$(TYPES_FILE_PATH) SED_BEFORE_STRING=$(TYPES_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(TYPES_FILE_WITHOUT_EXTERN_STRING) + +_sed_index_file_remove_extern: + $(MAKE) _sed_file SED_FILE_PATH=$(INDEX_FILE_PATH) SED_BEFORE_STRING=$(INDEX_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(INDEX_FILE_WITHOUT_EXTERN_STRING) + +_sed_wrapped_types_file_remove_extern: + $(if $(strip $(WRAPPED_INDEX_FILE_PATH)), $(MAKE) _sed_file SED_FILE_PATH=$(WRAPPED_INDEX_FILE_PATH) SED_BEFORE_STRING=$(WRAPPED_INDEX_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING), ) + +_sed_types_file_add_extern: + $(MAKE) _sed_file SED_FILE_PATH=$(TYPES_FILE_PATH) SED_BEFORE_STRING=$(TYPES_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(TYPES_FILE_WITH_EXTERN_STRING) + +_sed_index_file_add_extern: + $(MAKE) _sed_file SED_FILE_PATH=$(INDEX_FILE_PATH) SED_BEFORE_STRING=$(INDEX_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(INDEX_FILE_WITH_EXTERN_STRING) + +_sed_wrapped_types_file_add_extern: + $(if $(strip $(WRAPPED_INDEX_FILE_PATH)), $(MAKE) _sed_file SED_FILE_PATH=$(WRAPPED_INDEX_FILE_PATH) SED_BEFORE_STRING=$(WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(WRAPPED_INDEX_FILE_WITH_EXTERN_STRING), ) + +_sed_file: + @{ \ + : "If the AFTER string is already present and the BEFORE string is not," ; \ + : "then exit success," ; \ + : "because the expected result is already present." ; \ + if grep -q '$(SED_AFTER_STRING)' $(SED_FILE_PATH) && ! grep -q '$(SED_BEFORE_STRING)' $(SED_FILE_PATH); then \ + echo "String has already been replaced in $(SED_FILE_PATH)"; \ + exit 0; \ + fi; \ + \ + : "If neither the AFTER nor BEFORE strings are present," ; \ + : "then exit failure," ; \ + : "because the sed will fail as the BEFORE string is not present." ; \ + if ! grep -q '$(SED_BEFORE_STRING)' $(SED_FILE_PATH); then \ + echo "Error: Could not find string to replace in $(SED_FILE_PATH)"; \ + exit 1; \ + fi; \ + \ + : "If both the AFTER and BEFORE strings are present," ; \ + : "then exit failure," ; \ + : "because the sed will produce unintended results (2 after strings)." ; \ + if grep -q '$(SED_AFTER_STRING)' $(SED_FILE_PATH) && grep -q '$(SED_BEFORE_STRING)' $(SED_FILE_PATH); then \ + echo "Error: Could not find string to replace in $(SED_FILE_PATH)"; \ + exit 1; \ + fi; \ + \ + : "Perform sed" ; \ + echo "Replacing in $(SED_FILE_PATH)"; \ + sed -i $(SED_PARAMETER) 's/$(SED_BEFORE_STRING)/$(SED_AFTER_STRING)/g' $(SED_FILE_PATH); \ + \ + : "If the BEFORE string is still present or the AFTER string is not present," ; \ + : "then exit failure," ; \ + : "because the sed did not succeed." ; \ + if grep -q '$(SED_BEFORE_STRING)' $(SED_FILE_PATH) || ! grep -q '$(SED_AFTER_STRING)' $(SED_FILE_PATH); then \ + echo "Error: No replacements made in $(SED_FILE_PATH)"; \ + exit 1; \ + else \ + echo "Replacement successful in $(SED_FILE_PATH)"; \ + fi; \ + } + # Transpile the entire project's impl # For each index file listed in the project Makefile's PROJECT_INDEX variable, # append a `-library:TestModels/$(PROJECT_INDEX) to the transpiliation target @@ -605,7 +681,7 @@ clean: _clean ########################## Python targets # Python MUST transpile dependencies first to generate .dtr files -transpile_python: | transpile_dependencies_python transpile_implementation_python transpile_test_python +transpile_python: | _no_extern_pre_transpile transpile_dependencies_python transpile_implementation_python transpile_test_python _no_extern_post_transpile transpile_implementation_python: TARGET=py transpile_implementation_python: OUT=runtimes/python/dafny_src diff --git a/TestModels/Aggregate/Makefile b/TestModels/Aggregate/Makefile index 7099d5b4f..d38ac982b 100644 --- a/TestModels/Aggregate/Makefile +++ b/TestModels/Aggregate/Makefile @@ -20,6 +20,20 @@ SMITHY_DEPS=dafny-dependencies/Model/traits.smithy # This project has no dependencies # DEPENDENT-MODELS:= +# Constants for languages that drop extern names (Python, Go) + +TYPES_FILE_PATH=Model/SimpleTypesBooleanTypes.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.boolean.internaldafny.types\" } SimpleTypesBooleanTypes" +TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleTypesBooleanTypes" + +INDEX_FILE_PATH=src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.boolean.internaldafny\" } SimpleBoolean refines AbstractSimpleTypesBooleanService {" +INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleBoolean refines AbstractSimpleTypesBooleanService {" + +WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleBooleanImpl.dfy +WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.boolean.internaldafny.wrapped\"} WrappedSimpleTypesBooleanService refines WrappedAbstractSimpleTypesBooleanService {" +WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleTypesBooleanService refines WrappedAbstractSimpleTypesBooleanService {" + # Python PYTHON_MODULE_NAME=simple_aggregate diff --git a/TestModels/SimpleTypes/SimpleBlob/Makefile b/TestModels/SimpleTypes/SimpleBlob/Makefile index db107c4cf..2ad67da48 100644 --- a/TestModels/SimpleTypes/SimpleBlob/Makefile +++ b/TestModels/SimpleTypes/SimpleBlob/Makefile @@ -16,6 +16,20 @@ SERVICE_DEPS_SimpleBlob := SMITHY_DEPS=dafny-dependencies/Model/traits.smithy +# Constants for languages that drop extern names (Python, Go) + +TYPES_FILE_PATH=Model/SimpleTypesBlobTypes.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.blob.internaldafny.types\" } SimpleTypesBlobTypes" +TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleTypesBlobTypes" + +INDEX_FILE_PATH=src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.blob.internaldafny\" } SimpleBlob refines AbstractSimpleTypesBlobService {" +INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleBlob refines AbstractSimpleTypesBlobService {" + +WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleBlobImpl.dfy +WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.blob.internaldafny.wrapped\"} WrappedSimpleTypesBlobService refines WrappedAbstractSimpleTypesBlobService {" +WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleTypesBlobService refines WrappedAbstractSimpleTypesBlobService {" + # Python PYTHON_MODULE_NAME=simple_types_blob diff --git a/TestModels/SimpleTypes/SimpleBlob/src/Index.dfy b/TestModels/SimpleTypes/SimpleBlob/src/Index.dfy index a6c5571bc..ec82dd2e4 100644 --- a/TestModels/SimpleTypes/SimpleBlob/src/Index.dfy +++ b/TestModels/SimpleTypes/SimpleBlob/src/Index.dfy @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 include "SimpleBlobImpl.dfy" -module SimpleBlob refines AbstractSimpleTypesBlobService { +module {:extern "simple.types.blob.internaldafny" } SimpleBlob refines AbstractSimpleTypesBlobService { import Operations = SimpleBlobImpl function method DefaultSimpleBlobConfig(): SimpleBlobConfig { diff --git a/TestModels/SimpleTypes/SimpleBlob/src/WrappedSimpleBlobImpl.dfy b/TestModels/SimpleTypes/SimpleBlob/src/WrappedSimpleBlobImpl.dfy index 09f928d75..1b26fc838 100644 --- a/TestModels/SimpleTypes/SimpleBlob/src/WrappedSimpleBlobImpl.dfy +++ b/TestModels/SimpleTypes/SimpleBlob/src/WrappedSimpleBlobImpl.dfy @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 include "../Model/SimpleTypesBlobTypesWrapped.dfy" -module WrappedSimpleTypesBlobService refines WrappedAbstractSimpleTypesBlobService { +module {:extern "simple.types.blob.internaldafny.wrapped"} WrappedSimpleTypesBlobService refines WrappedAbstractSimpleTypesBlobService { import WrappedService = SimpleBlob function method WrappedDefaultSimpleBlobConfig(): SimpleBlobConfig { SimpleBlobConfig diff --git a/TestModels/SimpleTypes/SimpleBoolean/Makefile b/TestModels/SimpleTypes/SimpleBoolean/Makefile index 70f8a24a1..9fc796501 100644 --- a/TestModels/SimpleTypes/SimpleBoolean/Makefile +++ b/TestModels/SimpleTypes/SimpleBoolean/Makefile @@ -16,6 +16,20 @@ SERVICE_DEPS_SimpleBoolean := SMITHY_DEPS=dafny-dependencies/Model/traits.smithy +# Constants for languages that drop extern names (Python, Go) + +TYPES_FILE_PATH=Model/SimpleTypesBooleanTypes.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.boolean.internaldafny.types\" } SimpleTypesBooleanTypes" +TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleTypesBooleanTypes" + +INDEX_FILE_PATH=src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.boolean.internaldafny\" } SimpleBoolean refines AbstractSimpleTypesBooleanService {" +INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleBoolean refines AbstractSimpleTypesBooleanService {" + +WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleBooleanImpl.dfy +WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.boolean.internaldafny.wrapped\"} WrappedSimpleTypesBooleanService refines WrappedAbstractSimpleTypesBooleanService {" +WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleTypesBooleanService refines WrappedAbstractSimpleTypesBooleanService {" + # Python PYTHON_MODULE_NAME=simple_types_boolean diff --git a/TestModels/SimpleTypes/SimpleBoolean/src/Index.dfy b/TestModels/SimpleTypes/SimpleBoolean/src/Index.dfy index 3d7dbf35c..0c068e575 100644 --- a/TestModels/SimpleTypes/SimpleBoolean/src/Index.dfy +++ b/TestModels/SimpleTypes/SimpleBoolean/src/Index.dfy @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 include "SimpleBooleanImpl.dfy" -module SimpleBoolean refines AbstractSimpleTypesBooleanService { +module {:extern "simple.types.boolean.internaldafny" } SimpleBoolean refines AbstractSimpleTypesBooleanService { import Operations = SimpleBooleanImpl function method DefaultSimpleBooleanConfig(): SimpleBooleanConfig { diff --git a/TestModels/SimpleTypes/SimpleBoolean/src/WrappedSimpleBooleanImpl.dfy b/TestModels/SimpleTypes/SimpleBoolean/src/WrappedSimpleBooleanImpl.dfy index cf2385fab..d4ef79631 100644 --- a/TestModels/SimpleTypes/SimpleBoolean/src/WrappedSimpleBooleanImpl.dfy +++ b/TestModels/SimpleTypes/SimpleBoolean/src/WrappedSimpleBooleanImpl.dfy @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 include "../Model/SimpleTypesBooleanTypesWrapped.dfy" -module WrappedSimpleTypesBooleanService refines WrappedAbstractSimpleTypesBooleanService { +module {:extern "simple.types.boolean.internaldafny.wrapped"} WrappedSimpleTypesBooleanService refines WrappedAbstractSimpleTypesBooleanService { import WrappedService = SimpleBoolean function method WrappedDefaultSimpleBooleanConfig(): SimpleBooleanConfig { SimpleBooleanConfig diff --git a/TestModels/SimpleTypes/SimpleDouble/Makefile b/TestModels/SimpleTypes/SimpleDouble/Makefile index d3d05f51c..fe6e85286 100644 --- a/TestModels/SimpleTypes/SimpleDouble/Makefile +++ b/TestModels/SimpleTypes/SimpleDouble/Makefile @@ -24,6 +24,20 @@ transpile_net_dependencies: format_net: pushd runtimes/net && dotnet format && popd +# Constants for languages that drop extern names (Python, Go) + +TYPES_FILE_PATH=Model/SimpleTypesSmithyDoubleTypes.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.smithydouble.internaldafny.types\" } SimpleTypesSmithyDoubleTypes" +TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleTypesSmithyDoubleTypes" + +INDEX_FILE_PATH=src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.smithydouble.internaldafny\" } SimpleDouble refines AbstractSimpleTypesSmithyDoubleService {" +INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleDouble refines AbstractSimpleTypesSmithyDoubleService {" + +WRAPPED_INDEX_FILE_PATH=src/WrappedIndex.dfy +WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.smithydouble.internaldafny.wrapped\"} WrappedSimpleTypesDouble refines WrappedAbstractSimpleTypesSmithyDoubleService" +WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleTypesDouble refines WrappedAbstractSimpleTypesSmithyDoubleService" + # Python PYTHON_MODULE_NAME=simple_types_smithydouble diff --git a/TestModels/SimpleTypes/SimpleDouble/src/Index.dfy b/TestModels/SimpleTypes/SimpleDouble/src/Index.dfy index 1f311eea9..b7a48b6b6 100644 --- a/TestModels/SimpleTypes/SimpleDouble/src/Index.dfy +++ b/TestModels/SimpleTypes/SimpleDouble/src/Index.dfy @@ -4,7 +4,7 @@ include "../Model/SimpleTypesSmithyDoubleTypes.dfy" include "./SimpleSmithyDoubleOperations.dfy" -module SimpleDouble refines AbstractSimpleTypesSmithyDoubleService { +module {:extern "simple.types.smithydouble.internaldafny" } SimpleDouble refines AbstractSimpleTypesSmithyDoubleService { import Operations = SimpleSmithyDoubleOperations function method DefaultSimpleDoubleConfig(): SimpleDoubleConfig { diff --git a/TestModels/SimpleTypes/SimpleDouble/src/WrappedIndex.dfy b/TestModels/SimpleTypes/SimpleDouble/src/WrappedIndex.dfy index 8c3667084..c94b00039 100644 --- a/TestModels/SimpleTypes/SimpleDouble/src/WrappedIndex.dfy +++ b/TestModels/SimpleTypes/SimpleDouble/src/WrappedIndex.dfy @@ -3,8 +3,7 @@ include "../Model/SimpleTypesSmithyDoubleTypesWrapped.dfy" -module - WrappedSimpleTypesDouble refines WrappedAbstractSimpleTypesSmithyDoubleService +module {:extern "simple.types.smithydouble.internaldafny.wrapped"} WrappedSimpleTypesDouble refines WrappedAbstractSimpleTypesSmithyDoubleService { import WrappedService = SimpleDouble diff --git a/TestModels/SimpleTypes/SimpleEnum/Makefile b/TestModels/SimpleTypes/SimpleEnum/Makefile index d900accf8..3a10fec82 100644 --- a/TestModels/SimpleTypes/SimpleEnum/Makefile +++ b/TestModels/SimpleTypes/SimpleEnum/Makefile @@ -19,6 +19,20 @@ SMITHY_DEPS=dafny-dependencies/Model/traits.smithy # This project has no dependencies # DEPENDENT-MODELS:= +# Constants for languages that drop extern names (Python, Go) + +TYPES_FILE_PATH=Model/SimpleTypesEnumTypes.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.enum.internaldafny.types\" } SimpleTypesEnumTypes" +TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleTypesEnumTypes" + +INDEX_FILE_PATH=src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.enum.internaldafny\" } SimpleEnum refines AbstractSimpleTypesEnumService {" +INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleEnum refines AbstractSimpleTypesEnumService {" + +WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleEnumImpl.dfy +WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.types.enum.internaldafny.wrapped\"} WrappedSimpleTypesEnumService refines WrappedAbstractSimpleTypesEnumService {" +WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleTypesEnumService refines WrappedAbstractSimpleTypesEnumService {" + # Python PYTHON_MODULE_NAME=simple_types_smithyenum diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java index 09b2126c0..e05350ca1 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java @@ -129,7 +129,10 @@ public Map generate() { namespace ); final TokenTree typesModuleHeader = Token.of( - "module %s".formatted( + "module {:extern \"%s\" } %s".formatted( + DafnyNameResolverHelpers.dafnyExternNamespaceForShapeId( + serviceShape.getId() + ), typesModuleName ) );