From f5cf0f4669a7d48fcd30b24dc494b9c021a6a53a Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 11 Jan 2024 15:59:26 -0800 Subject: [PATCH 1/2] feat: optional tests --- .github/workflows/ci_test_vector_net.yml | 2 ++ TestVectors/dafny/DDBEncryption/src/Index.dfy | 8 ++++++-- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci_test_vector_net.yml b/.github/workflows/ci_test_vector_net.yml index 22c2522ba..bd4965951 100644 --- a/.github/workflows/ci_test_vector_net.yml +++ b/.github/workflows/ci_test_vector_net.yml @@ -58,5 +58,7 @@ jobs: - name: Test TestVectors working-directory: ./TestVectors/runtimes/net run: | + cp ../java/decrypt_java.json ../java/decrypt_dotnet.json . + dotnet run cp ../java/*.json . dotnet run diff --git a/TestVectors/dafny/DDBEncryption/src/Index.dfy b/TestVectors/dafny/DDBEncryption/src/Index.dfy index 8a67f6039..262c04b58 100644 --- a/TestVectors/dafny/DDBEncryption/src/Index.dfy +++ b/TestVectors/dafny/DDBEncryption/src/Index.dfy @@ -17,8 +17,12 @@ module WrappedDDBEncryptionMain { method AddJson(prev : TestVectorConfig, file : string) returns (output : Result) { - var configBv :- expect FileIO.ReadBytesFromFile(file); - var configBytes := BvToBytes(configBv); + var configBv := FileIO.ReadBytesFromFile(file); + if configBv.Failure? { + print "Failed to open ", file, " continuing anyway.\n"; + return Success(MakeEmptyTestVector()); + } + var configBytes := BvToBytes(configBv.value); var json :- expect API.Deserialize(configBytes); output := ParseTestVector(json, prev); if output.Failure? { From 8f0e6b482cbe0a0716575ae6088268d1ade17f32 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 11 Jan 2024 16:07:24 -0800 Subject: [PATCH 2/2] m --- TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index c5e2b2cb1..7a6c67301 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -91,6 +91,10 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { var _ :- expect WriteManifest.Write("encrypt.json"); var _ :- expect EncryptManifest.Encrypt("encrypt.json", "decrypt.json", "java", "3.2"); var _ :- expect DecryptManifest.Decrypt("decrypt.json"); + if |globalRecords| + |tableEncryptionConfigs| + |queries| == 0 { + print "\nRunning no tests\n"; + return; + } Validate(); StringOrdering(); BasicIoTest();