sed

aws · Nov 4, 2024 · d8a408e · d8a408e
1 parent 6d453b3
commit d8a408e
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 12 deletions.
diff --git a/.github/workflows/library_interop_test_vectors.yml b/.github/workflows/library_interop_test_vectors.yml
@@ -80,7 +80,6 @@ jobs:
             # This works because `node` is installed by default on GHA runners
             CORES=$(node -e 'console.log(os.cpus().length)')
             make build_java CORES=$CORES
-            make write_correct_main_java
 
         - name: Build ${{ matrix.library }} implementation in .NET
           if: matrix.language == 'net'
@@ -90,7 +89,6 @@ jobs:
             # This works because `node` is installed by default on GHA runners
             CORES=$(node -e 'console.log(os.cpus().length)')
             make transpile_net
-            make write_correct_main_net
             
         - name: Setup gradle
           if: matrix.language == 'java'
@@ -162,13 +160,13 @@ jobs:
 
       # Set up runtimes
       - name: Setup .NET Core SDK ${{ matrix.dotnet-version }}
-        if: matrix.decrypting_language == 'net'
+        if: matrix.language == 'net'
         uses: actions/setup-dotnet@v3
         with:
           dotnet-version: ${{ matrix.dotnet-version }}
 
       - name: Setup Java 17
-        if: matrix.decrypting_language == 'java'
+        if: matrix.language == 'java'
         uses: actions/setup-java@v3
         with:
           distribution: "corretto"
@@ -196,7 +194,6 @@ jobs:
           # This works because `node` is installed by default on GHA runners
           CORES=$(node -e 'console.log(os.cpus().length)')
           make build_java CORES=$CORES
-          make write_correct_main_java
 
       - name: Build ${{ matrix.library }} implementation in .NET
         if: matrix.language == 'net'
@@ -206,8 +203,7 @@ jobs:
           # This works because `node` is installed by default on GHA runners
           CORES=$(node -e 'console.log(os.cpus().length)')
           make transpile_net
-          make write_correct_main_net
-          
+
       - name: Download Encrypt Manifest Artifact
         uses: actions/download-artifact@v4
         with:

diff --git a/TestVectors/Makefile b/TestVectors/Makefile
@@ -38,7 +38,7 @@ PROJECT_INDEX := \
 	mpl/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Index.dfy \
 	mpl/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Index.dfy \
 	mpl/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/Index.dfy \
-	mpl/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/Index.dfy \
+	mpl/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/LibraryIndex.dfy \
 	AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy \
 
 STD_LIBRARY=mpl/StandardLibrary
@@ -59,11 +59,22 @@ SERVICE_DEPS_TestVectors := \
 format_net:
 	pushd runtimes/net && dotnet format && popd
 
-write_correct_main_java:
-	sed -i "" "s/dafny.Helpers.withHaltHandling(() -> { WrappedMaterialProvidersMain_Compile.__default.__Main(dafny.Helpers.FromMainArguments(args)); } );/dafny.Helpers.withHaltHandling(() -> { WrappedESDKMain_Compile.__default.Main2(dafny.Helpers.FromMainArguments(args)); } );/g" runtimes/java/src/main/dafny-generated/ImplementationFromDafny.java
+IMPLEMENTATION_FROM_DAFNY_TV_JAVA_FILE=runtimes/java/src/main/dafny-generated/ImplementationFromDafny.java
+IMPLEMENTATION_FROM_DAFNY_TV_JAVA_MPL_MAIN="dafny.Helpers.withHaltHandling(() -> { WrappedMaterialProvidersMain_Compile.__default.__Main(dafny.Helpers.FromMainArguments(args)); } );"
+IMPLEMENTATION_FROM_DAFNY_TV_JAVA_ESDK_MAIN="dafny.Helpers.withHaltHandling(() -> { WrappedESDKMain_Compile.__default.Main2(dafny.Helpers.FromMainArguments(args)); } );"
 
-write_correct_main_net:
-	sed -i "" "s/Dafny.Helpers.WithHaltHandling(() => WrappedMaterialProvidersMain_Compile.__default._Main(Dafny.Sequence<Dafny.ISequence<char>>.FromMainArguments(args)));/Dafny.Helpers.WithHaltHandling(() => WrappedESDKMain_Compile.__default.Main2(Dafny.Sequence<Dafny.ISequence<char>>.FromMainArguments(args)));/g" runtimes/net/ImplementationFromDafny.cs
+IMPLEMENTATION_FROM_DAFNY_TV_NET_FILE=runtimes/net/ImplementationFromDafny.cs
+IMPLEMENTATION_FROM_DAFNY_TV_NET_MPL_MAIN="Dafny.Helpers.WithHaltHandling(() => WrappedMaterialProvidersMain_Compile.__default._Main(Dafny.Sequence<Dafny.ISequence<char>>.FromMainArguments(args)));"
+IMPLEMENTATION_FROM_DAFNY_TV_NET_ESDK_MAIN="Dafny.Helpers.WithHaltHandling(() => WrappedESDKMain_Compile.__default.Main2(Dafny.Sequence<Dafny.ISequence<char>>.FromMainArguments(args)));"
+
+transpile_implementation_java: _replace_main_method_name_java
+transpile_implementation_net: _replace_main_method_name_net
+
+_replace_main_method_name_java:
+	$(MAKE) _sed_file SED_FILE_PATH=$(IMPLEMENTATION_FROM_DAFNY_TV_JAVA_FILE) SED_BEFORE_STRING=$(IMPLEMENTATION_FROM_DAFNY_TV_JAVA_MPL_MAIN) SED_AFTER_STRING=$(IMPLEMENTATION_FROM_DAFNY_TV_JAVA_ESDK_MAIN)
+
+_replace_main_method_name_net:
+	$(MAKE) _sed_file SED_FILE_PATH=$(IMPLEMENTATION_FROM_DAFNY_TV_NET_FILE) SED_BEFORE_STRING=$(IMPLEMENTATION_FROM_DAFNY_TV_NET_MPL_MAIN) SED_AFTER_STRING=$(IMPLEMENTATION_FROM_DAFNY_TV_NET_ESDK_MAIN)
 
 
 # Commands to generate and test test vectors