chore(dafny): add timing support

AwsCryptographicMaterialProviders/runtimes/rust/src/dafny_libraries.rs

@@ -180,6 +180,19 @@ pub mod DafnyLibraries {
             let file_name = dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(path);
             let path = Path::new(&file_name);
 
+            if let Some(parent) = path.parent() {
+                if let Err(why) = std::fs::create_dir_all(parent) {
+                    let err_msg = format!(
+                        "couldn't create directory {} from {}: {}",
+                        path.display(),
+                        curr_dir(),
+                        why
+                    );
+                    let err_msg = dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&err_msg);
+                    return (true, err_msg);
+                }
+            }
+
             let maybe_file = std::fs::OpenOptions::new()
                 .append(append)
                 .write(true)

StandardLibrary/src/Time.dfy

@@ -5,13 +5,17 @@ include "./StandardLibrary.dfy"
 include "./UInt.dfy"
 include "./String.dfy"
 include "./OsLang.dfy"
+include "./UTF8.dfy"
+include "../../libraries/src/FileIO/FileIO.dfy"
 
 module {:extern "Time"} Time {
   import opened StandardLibrary
   import opened Wrappers
   import opened UInt = StandardLibrary.UInt
   import StandardLibrary.String
   import OsLang
+  import UTF8
+  import FileIO
 
   // Time is non-deterministic.
   // In this way it is similar to random number.
@@ -134,9 +138,22 @@ module {:extern "Time"} Time {
     print "Clock Time : ", FormatMilli(time.ClockTime), " CPU Time : ", FormatMilli(time.CpuTime), "\n";
   }
 
-  method PrintTimeLong(time : RelativeTime, tag : string)
+  method PrintTimeSinceLong(start : AbsoluteTime, tag : string, file : Option<string> :=  None)
   {
-    print tag, " ", OsLang.GetOsLong(), " ", OsLang.GetLanguageLong(), " Clock Time : ", FormatMilli(time.ClockTime), " CPU Time : ", FormatMilli(time.CpuTime), "\n";
+    var t := TimeSince(start);
+    PrintTimeLong(t, tag, file);
+  }
+
+  method PrintTimeLong(time : RelativeTime, tag : string, file : Option<string> :=  None)
+  {
+    var val := tag + " " + OsLang.GetOsShort() + " " + OsLang.GetLanguageShort() + " " + FormatMilli(time.ClockTime) + " " + FormatMilli(time.CpuTime) + "\n";
+    print val;
+    if file.Some? {
+      var utf8_val := UTF8.Encode(val);
+      if utf8_val.Success? {
+        var _ := FileIO.AppendBytesToFile(file.value, utf8_val.value);
+      }
+    }
   }
 
   method PrintTimeShort(time : RelativeTime)

TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestManifests.dfy

@@ -26,6 +26,15 @@ module {:options "-functionSyntax:4"} TestManifests {
   import MplManifestOptions
   import CompleteVectors
   import Time
+  import OsLang
+
+  function LogFileName() : string
+  {
+    if OsLang.GetOsShort() == "Windows" && OsLang.GetLanguageShort() == "Dotnet" then
+      "..\\..\\PerfLog.txt"
+    else
+      "../../PerfLog.txt"
+  }
 
   method StartEncrypt(op: MplManifestOptions.ManifestOptions)
     returns (output: Result<(), string>)
@@ -60,6 +69,7 @@ module {:options "-functionSyntax:4"} TestManifests {
 
     var decryptableTests: seq<(TestVectors.EncryptTest, Types.EncryptionMaterials)> := [];
 
+    var time := Time.GetAbsoluteTime();
     for i := 0 to |tests|
       invariant forall t <- tests :: t.cmm.ValidState()
     {
@@ -72,6 +82,8 @@ module {:options "-functionSyntax:4"} TestManifests {
         hasFailure := true;
       }
     }
+    var elapsed :=Time.TimeSince(time);
+    Time.PrintTimeLong(elapsed, "TestEncrypts", Some(LogFileName()));
 
     print "\n=================== Completed ", |tests|, " Encrypt Tests =================== \n\n";
 
@@ -106,6 +118,7 @@ module {:options "-functionSyntax:4"} TestManifests {
 
     var hasFailure := false;
 
+    var time := Time.GetAbsoluteTime();
     for i := 0 to |tests|
       invariant forall t <- tests :: t.cmm.ValidState()
     {
@@ -114,6 +127,8 @@ module {:options "-functionSyntax:4"} TestManifests {
         hasFailure := true;
       }
     }
+    var elapsed := Time.TimeSince(time);
+    Time.PrintTimeLong(elapsed, "TestDecrypts", Some(LogFileName()));
     print "\n=================== Completed ", |tests|, " Decrypt Tests =================== \n\n";
 
     expect !hasFailure;