diff --git a/AwsCryptographicMaterialProviders/runtimes/rust/src/dafny_libraries.rs b/AwsCryptographicMaterialProviders/runtimes/rust/src/dafny_libraries.rs index a5e7f437f..b83589c14 100644 --- a/AwsCryptographicMaterialProviders/runtimes/rust/src/dafny_libraries.rs +++ b/AwsCryptographicMaterialProviders/runtimes/rust/src/dafny_libraries.rs @@ -83,7 +83,13 @@ pub mod DafnyLibraries { use std::io::Write; use std::path::Path; - pub fn INTERNAL_ReadBytesFromFile( + // Attempts to read all bytes from the file at {@code path}, and returns a tuple of the following values: + // isError : true iff an exception was thrown during path string conversion or when reading the file + // bytesRead : the sequence of bytes read from the file, or an empty sequence if {@code isError} is true + // errorMsg : the error message of the thrown exception if {@code isError} is true, or an empty equence otherwise + // We return these values individually because Result is not defined in the runtime but + // instead in library code. It is the responsibility of library code to construct an equivalent Result value. + pub(crate) fn INTERNAL_ReadBytesFromFile( file: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, ) -> ( bool, @@ -122,28 +128,62 @@ pub mod DafnyLibraries { } } + // Get the current dirctory for use in error messages fn curr_dir() -> String { let path = std::env::current_dir(); match path { Ok(path) => format!("{}", path.display()), - Err(_) => "unknown".to_string(), + Err(_) => "Error while getting the path of current directory".to_string(), } } - pub fn INTERNAL_WriteBytesToFile( + // Attempts to append bytes to the file at path, creating nonexistent parent + // See SendBytesToFile for details + pub(crate) fn INTERNAL_AppendBytesToFile( path: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, bytes: &::dafny_runtime::Sequence, ) -> ( bool, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ) { + SendBytesToFile(path, bytes, true) + } + + // Attempts to write bytes to the file at path, creating nonexistent parent + // See SendBytesToFile for details + pub(crate) fn INTERNAL_WriteBytesToFile( + path: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + bytes: &::dafny_runtime::Sequence, + ) -> ( + bool, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ) { + SendBytesToFile(path, bytes, false) + } + + // Attempts to write bytes to the file at path, creating nonexistent parent + // directories as necessary, and returns a tuple of the following values: + // isError : true iff an exception was thrown during path string conversion or when writing to the file + // errorMsg : the error message of the thrown exception if {@code isError} is true, or an empty sequence otherwise + // We return these values individually because {@code Result} is not defined in the runtime but + // instead in library code. It is the responsibility of library code to construct an equivalent Result value. + // if append is false, the file is truncated, otherwise we append to the existing file. + fn SendBytesToFile( + path: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + bytes: &::dafny_runtime::Sequence, + append: bool, + ) -> ( + bool, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, ) { let file_name = dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(path); let path = Path::new(&file_name); let maybe_file = std::fs::OpenOptions::new() + .append(append) .write(true) .create(true) - .truncate(true) + .truncate(!append) .open(path); let mut file = match maybe_file { Err(why) => { diff --git a/AwsCryptographicMaterialProviders/runtimes/rust/src/rsa.rs b/AwsCryptographicMaterialProviders/runtimes/rust/src/rsa.rs index 9bb76d9cc..650d72a2b 100644 --- a/AwsCryptographicMaterialProviders/runtimes/rust/src/rsa.rs +++ b/AwsCryptographicMaterialProviders/runtimes/rust/src/rsa.rs @@ -12,8 +12,8 @@ pub mod RSAEncryption { use crate::_Wrappers_Compile as Wrappers; use crate::software::amazon::cryptography::primitives::internaldafny::types::RSAPaddingMode; use crate::*; - use ::std::rc::Rc; use aws_lc_rs::encoding::{AsDer, Pkcs8V1Der, PublicKeyX509Der}; + use std::rc::Rc; use aws_lc_rs::rsa::KeySize; use aws_lc_rs::rsa::OaepAlgorithm; diff --git a/AwsCryptographicMaterialProviders/runtimes/rust/src/storm_tracker.rs b/AwsCryptographicMaterialProviders/runtimes/rust/src/storm_tracker.rs index 7c0b59a7a..9ca4461ca 100644 --- a/AwsCryptographicMaterialProviders/runtimes/rust/src/storm_tracker.rs +++ b/AwsCryptographicMaterialProviders/runtimes/rust/src/storm_tracker.rs @@ -25,8 +25,8 @@ pub mod internal_StormTrackingCMC { } } - impl ::dafny_runtime::UpcastObject for StormTrackingCMC { - ::dafny_runtime::UpcastObjectFn!(dyn::std::any::Any); + impl ::dafny_runtime::UpcastObject for StormTrackingCMC { + ::dafny_runtime::UpcastObjectFn!(dyn ::std::any::Any); } impl ::dafny_runtime::UpcastObject diff --git a/AwsCryptographicMaterialProviders/runtimes/rust/src/time.rs b/AwsCryptographicMaterialProviders/runtimes/rust/src/time.rs index cb170033f..3182c8020 100644 --- a/AwsCryptographicMaterialProviders/runtimes/rust/src/time.rs +++ b/AwsCryptographicMaterialProviders/runtimes/rust/src/time.rs @@ -6,6 +6,7 @@ #![deny(clippy::all)] use crate::*; +use std::convert::TryFrom; use std::time::SystemTime; impl crate::Time::_default { @@ -26,6 +27,13 @@ impl crate::Time::_default { } } + #[allow(non_snake_case)] + #[allow(dead_code)] + pub fn GetProcessCpuTimeMillis() -> i64 { + i64::try_from(cpu_time::ProcessTime::now().as_duration().as_millis()) + .expect("CPU millisecond didn't fit in an i64") + } + #[allow(non_snake_case)] pub fn GetCurrentTimeStamp() -> ::std::rc::Rc< _Wrappers_Compile::Result< diff --git a/AwsCryptographicMaterialProviders/runtimes/rust/src/timer.rs b/AwsCryptographicMaterialProviders/runtimes/rust/src/timer.rs index 970620d32..a751af3c1 100644 --- a/AwsCryptographicMaterialProviders/runtimes/rust/src/timer.rs +++ b/AwsCryptographicMaterialProviders/runtimes/rust/src/timer.rs @@ -2,26 +2,31 @@ // SPDX-License-Identifier: Apache-2.0 pub struct ResourceTracker { - count : usize, - total : usize, - time : std::time::SystemTime, - cpu : cpu_time::ProcessTime, + count: usize, + total: usize, + time: std::time::SystemTime, + cpu: cpu_time::ProcessTime, } impl ResourceTracker { pub fn new() -> Self { - Self { - count : get_counter(), - total : get_total(), - time : std::time::SystemTime::now(), - cpu : cpu_time::ProcessTime::now(), - } + Self { + count: get_counter(), + total: get_total(), + time: std::time::SystemTime::now(), + cpu: cpu_time::ProcessTime::now(), + } } pub fn report(&self) { - let time = self.time.elapsed().unwrap().as_secs_f64(); - let cpu = self.cpu.elapsed().as_secs_f64(); - println!("Allocation Count : {}, Total : {}, CPU Time : {}, Clock Time : {}", - get_counter()-self.count, get_total()-self.total, cpu, time); + let time = self.time.elapsed().unwrap().as_secs_f64(); + let cpu = self.cpu.elapsed().as_secs_f64(); + println!( + "Allocation Count : {}, Total : {}, CPU Time : {}, Clock Time : {}", + get_counter() - self.count, + get_total() - self.total, + cpu, + time + ); } } @@ -31,32 +36,28 @@ static mut TOTAL: usize = 0; fn add_to_counter(inc: usize) { // SAFETY: There are no other threads which could be accessing `COUNTER`. unsafe { - COUNTER += 1; + COUNTER += 1; TOTAL += inc; } } fn get_counter() -> usize { // SAFETY: There are no other threads which could be accessing `COUNTER`. - unsafe { - COUNTER - } + unsafe { COUNTER } } fn get_total() -> usize { // SAFETY: There are no other threads which could be accessing `COUNTER`. - unsafe { - TOTAL - } + unsafe { TOTAL } } -use std::alloc::{GlobalAlloc, System, Layout}; +use std::alloc::{GlobalAlloc, Layout, System}; struct MyAllocator; unsafe impl GlobalAlloc for MyAllocator { unsafe fn alloc(&self, layout: Layout) -> *mut u8 { - add_to_counter(layout.size()); + add_to_counter(layout.size()); System.alloc(layout) } diff --git a/AwsCryptographyPrimitives/runtimes/rust/Cargo.toml b/AwsCryptographyPrimitives/runtimes/rust/Cargo.toml index f554c5665..669018fa9 100644 --- a/AwsCryptographyPrimitives/runtimes/rust/Cargo.toml +++ b/AwsCryptographyPrimitives/runtimes/rust/Cargo.toml @@ -13,6 +13,7 @@ aws-lc-sys = "0.22.0" aws-smithy-runtime-api = "1.7.3" aws-smithy-types = "1.2.9" chrono = "0.4.38" +cpu-time = "1.0.0" dafny_runtime = { path = "../../../smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust"} dashmap = "6.1.0" pem = "3.0.4" diff --git a/ComAmazonawsDynamodb/runtimes/rust/Cargo.toml b/ComAmazonawsDynamodb/runtimes/rust/Cargo.toml index 0531c245b..927d50f43 100644 --- a/ComAmazonawsDynamodb/runtimes/rust/Cargo.toml +++ b/ComAmazonawsDynamodb/runtimes/rust/Cargo.toml @@ -12,6 +12,7 @@ aws-sdk-dynamodb = "1.53.0" aws-smithy-runtime-api = "1.7.3" aws-smithy-types = "1.2.9" chrono = "0.4.38" +cpu-time = "1.0.0" dafny_runtime = { path = "../../../smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust"} dashmap = "6.1.0" tokio = {version = "1.41.1", features = ["full"] } diff --git a/ComAmazonawsKms/runtimes/rust/Cargo.toml b/ComAmazonawsKms/runtimes/rust/Cargo.toml index c6ee65034..37cb028d0 100644 --- a/ComAmazonawsKms/runtimes/rust/Cargo.toml +++ b/ComAmazonawsKms/runtimes/rust/Cargo.toml @@ -12,6 +12,7 @@ aws-sdk-kms = "1.50.0" aws-smithy-runtime-api = "1.7.3" aws-smithy-types = "1.2.9" chrono = "0.4.38" +cpu-time = "1.0.0" dafny_runtime = { path = "../../../smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust"} dashmap = "6.1.0" tokio = {version = "1.41.1", features = ["full"] } diff --git a/StandardLibrary/Makefile b/StandardLibrary/Makefile index dcdb70bd9..e29e5db2e 100644 --- a/StandardLibrary/Makefile +++ b/StandardLibrary/Makefile @@ -24,6 +24,7 @@ PYTHON_MODULE_NAME=smithy_dafny_standard_library RUST_OTHER_FILES := \ runtimes/rust/src/concurrent_call.rs \ + runtimes/rust/src/dafny_libraries.rs \ runtimes/rust/src/sets.rs \ runtimes/rust/src/time.rs \ runtimes/rust/src/uuid.rs diff --git a/StandardLibrary/runtimes/go/ImplementationFromDafny-go/FileIO/externs.go b/StandardLibrary/runtimes/go/ImplementationFromDafny-go/FileIO/externs.go index f136630c8..f93bcf4d9 100644 --- a/StandardLibrary/runtimes/go/ImplementationFromDafny-go/FileIO/externs.go +++ b/StandardLibrary/runtimes/go/ImplementationFromDafny-go/FileIO/externs.go @@ -14,7 +14,18 @@ var m_DafnyLibraries struct { } func (_static CompanionStruct_Default___) INTERNAL_ReadBytesFromFile(path _dafny.Sequence) (isError bool, bytesRead _dafny.Sequence, errorMsg _dafny.Sequence) { - p := _dafny.SequenceVerbatimString(path, false) + p := func() string { + var s string + for i := _dafny.Iterate(path); ; { + val, notEndOfSequence := i() + if notEndOfSequence { + s = s + string(val.(_dafny.Char)) + } else { + return s + } + } + }() + dat, err := ioutil.ReadFile(p) if err != nil { errAsSequence := _dafny.UnicodeSeqOfUtf8Bytes(err.Error()) @@ -25,11 +36,20 @@ func (_static CompanionStruct_Default___) INTERNAL_ReadBytesFromFile(path _dafny } func (_static CompanionStruct_Default___) INTERNAL_WriteBytesToFile(path _dafny.Sequence, bytes _dafny.Sequence) (isError bool, errorMsg _dafny.Sequence) { - p := _dafny.SequenceVerbatimString(path, false) + p := func() string { + var s string + for i := _dafny.Iterate(path); ; { + val, notEndOfSequence := i() + if notEndOfSequence { + s = s + string(val.(_dafny.Char)) + } else { + return s + } + } + }() // Create directories os.MkdirAll(filepath.Dir(p), os.ModePerm) - bytesArray := _dafny.ToByteArray(bytes) err := ioutil.WriteFile(p, bytesArray, 0644) if err != nil { @@ -38,3 +58,37 @@ func (_static CompanionStruct_Default___) INTERNAL_WriteBytesToFile(path _dafny. } return false, _dafny.EmptySeq } + +func (_static CompanionStruct_Default___) INTERNAL_AppendBytesToFile(path _dafny.Sequence, bytes _dafny.Sequence) (isError bool, errorMsg _dafny.Sequence) { + p := func() string { + var s string + for i := _dafny.Iterate(path); ; { + val, notEndOfSequence := i() + if notEndOfSequence { + s = s + string(val.(_dafny.Char)) + } else { + return s + } + } + }() + + // Create directories + os.MkdirAll(filepath.Dir(p), os.ModePerm) + + bytesArray := _dafny.ToByteArray(bytes) + + f, err := os.OpenFile(p, os.O_APPEND|os.O_CREATE|os.O_WRONLY, 0644) + if err != nil { + return true, _dafny.UnicodeSeqOfUtf8Bytes(err.Error()) + } + + if _, err := f.Write(bytesArray); err != nil { + return true, _dafny.UnicodeSeqOfUtf8Bytes(err.Error()) + } + + if err := f.Close(); err != nil { + return true, _dafny.UnicodeSeqOfUtf8Bytes(err.Error()) + } + + return false, _dafny.EmptySeq +} diff --git a/StandardLibrary/runtimes/go/ImplementationFromDafny-go/Time_/externs.go b/StandardLibrary/runtimes/go/ImplementationFromDafny-go/Time_/externs.go index bf1f25e21..7d4867f43 100644 --- a/StandardLibrary/runtimes/go/ImplementationFromDafny-go/Time_/externs.go +++ b/StandardLibrary/runtimes/go/ImplementationFromDafny-go/Time_/externs.go @@ -1,16 +1,30 @@ package _Time import ( + "syscall" "time" "github.com/dafny-lang/DafnyRuntimeGo/v4/dafny" "github.com/dafny-lang/DafnyStandardLibGo/Wrappers" ) +var m__Time = CompanionStruct_Default___{} + +func (CompanionStruct_Default___) CurrentRelativeTimeMilli() int64 { + return CurrentRelativeTimeMilli() +} + +func (CompanionStruct_Default___) CurrentRelativeTime() int64 { + return CurrentRelativeTime() +} func CurrentRelativeTime() int64 { return int64(time.Now().Second()) } +func (CompanionStruct_Default___) GetCurrentTimeStamp() Wrappers.Result { + return GetCurrentTimeStamp() +} + func GetCurrentTimeStamp() Wrappers.Result { return Wrappers.Companion_Result_.Create_Success_(dafny.SeqOfChars([]dafny.Char(time.Now().Format("2006-01-02T15:04:05.000000Z"))...)) } @@ -18,3 +32,13 @@ func GetCurrentTimeStamp() Wrappers.Result { func CurrentRelativeTimeMilli() int64 { return time.Now().UnixMilli() } + +func (CompanionStruct_Default___) GetProcessCpuTimeMillis() int64 { + return GetProcessCpuTimeMillis() +} + +func GetProcessCpuTimeMillis() int64 { + usage := new(syscall.Rusage) + syscall.Getrusage(syscall.RUSAGE_SELF, usage) + return (usage.Utime.Nano() + usage.Stime.Nano()) / 1000000 +} diff --git a/StandardLibrary/runtimes/java/src/main/java/DafnyLibraries/FileIO.java b/StandardLibrary/runtimes/java/src/main/java/DafnyLibraries/FileIO.java index a7418f5c0..945c64ddd 100644 --- a/StandardLibrary/runtimes/java/src/main/java/DafnyLibraries/FileIO.java +++ b/StandardLibrary/runtimes/java/src/main/java/DafnyLibraries/FileIO.java @@ -102,6 +102,54 @@ > INTERNAL_WriteBytesToFile( } } + /** + * Attempts to append {@code bytes} to the file at {@code path}, creating nonexistent parent + * directories as necessary, and returns a tuple of the following values: + * + *
+ *
{@code isError} + *
true iff an exception was thrown during path string conversion or when writing to the + * file + *
{@code errorMsg} + *
the error message of the thrown exception if {@code isError} is true, or an empty + * sequence otherwise + *
+ * + *

We return these values individually because {@code Result} is not defined in the runtime but + * instead in library code. It is the responsibility of library code to construct an equivalent + * {@code Result} value. + */ + public static Tuple2< + Boolean, + DafnySequence + > INTERNAL_AppendBytesToFile( + DafnySequence path, + DafnySequence bytes + ) { + try { + final Path pathObj = dafnyStringToPath(path); + createParentDirs(pathObj); + + // It's safe to cast `bytes` to `DafnySequence` since the cast value is immediately + // consumed + @SuppressWarnings("unchecked") + final byte[] byteArr = DafnySequence.toByteArray( + (DafnySequence) bytes + ); + + java.io.OutputStream out = Files.newOutputStream( + pathObj, + java.nio.file.StandardOpenOption.CREATE, + java.nio.file.StandardOpenOption.APPEND + ); + out.write(byteArr); + out.close(); + return Tuple2.create(false, DafnySequence.empty(TypeDescriptor.CHAR)); + } catch (Exception ex) { + return Tuple2.create(true, stackTraceToDafnyString(ex)); + } + } + /** Returns a Path constructed from the given Dafny string. */ private static final Path dafnyStringToPath( final DafnySequence path diff --git a/StandardLibrary/runtimes/java/src/main/java/Time/__default.java b/StandardLibrary/runtimes/java/src/main/java/Time/__default.java index dc5c8b30d..cce43f8e6 100644 --- a/StandardLibrary/runtimes/java/src/main/java/Time/__default.java +++ b/StandardLibrary/runtimes/java/src/main/java/Time/__default.java @@ -1,7 +1,9 @@ package Time; import Wrappers_Compile.Result; +import com.sun.management.OperatingSystemMXBean; import dafny.DafnySequence; +import java.lang.management.ManagementFactory; import java.text.DateFormat; import java.text.SimpleDateFormat; import java.util.Date; @@ -17,6 +19,12 @@ public static Long CurrentRelativeTimeMilli() { return System.currentTimeMillis(); } + public static Long GetProcessCpuTimeMillis() { + OperatingSystemMXBean bean = + (com.sun.management.OperatingSystemMXBean) ManagementFactory.getOperatingSystemMXBean(); + return new Long(bean.getProcessCpuTime() / 1000000); + } + public static Result< DafnySequence, DafnySequence diff --git a/StandardLibrary/runtimes/net/Extern/FileIO.cs b/StandardLibrary/runtimes/net/Extern/FileIO.cs new file mode 100644 index 000000000..614fd71dc --- /dev/null +++ b/StandardLibrary/runtimes/net/Extern/FileIO.cs @@ -0,0 +1,147 @@ +/******************************************************************************* +* Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ + +namespace DafnyLibraries +{ + using System; + using System.IO; + + using Dafny; + + public class FileIO + { + ///

+ /// Attempts to read all bytes from the file at the given path, and outputs the following values: + /// + /// + /// isError + /// + /// true iff an exception was thrown during path string conversion or when reading the file + /// + /// + /// + /// bytesRead + /// + /// the sequence of bytes read from the file, or an empty sequence if isError is true + /// + /// + /// + /// errorMsg + /// + /// the error message of the thrown exception if isError is true, or an empty sequence otherwise + /// + /// + /// + /// + /// We output these values individually because Result is not defined in the runtime but instead in library code. + /// It is the responsibility of library code to construct an equivalent Result value. + /// + public static void INTERNAL_ReadBytesFromFile(ISequence path, out bool isError, out ISequence bytesRead, + out ISequence errorMsg) + { + isError = true; + bytesRead = Sequence.Empty; + errorMsg = Sequence.Empty; + try + { + bytesRead = Helpers.SeqFromArray(File.ReadAllBytes(path?.ToString())); + isError = false; + } + catch (Exception e) + { + errorMsg = Helpers.SeqFromArray(e.ToString().ToCharArray()); + } + } + + /// + /// Attempts to write all given bytes to the file at the given path, creating nonexistent parent directories as necessary, + /// and outputs the following values: + /// + /// + /// isError + /// + /// true iff an exception was thrown during path string conversion or when writing to the file + /// + /// + /// + /// errorMsg + /// + /// the error message of the thrown exception if isError is true, or an empty sequence otherwise + /// + /// + /// + /// + /// We output these values individually because Result is not defined in the runtime but instead in library code. + /// It is the responsibility of library code to construct an equivalent Result value. + /// + public static void INTERNAL_WriteBytesToFile(ISequence path, ISequence bytes, out bool isError, out ISequence errorMsg) + { + isError = true; + errorMsg = Sequence.Empty; + try + { + string pathStr = path?.ToString(); + CreateParentDirs(pathStr); + File.WriteAllBytes(pathStr, bytes.CloneAsArray()); + isError = false; + } + catch (Exception e) + { + errorMsg = Helpers.SeqFromArray(e.ToString().ToCharArray()); + } + } + + /// + /// Attempts to append all given bytes to the file at the given path, creating nonexistent parent directories as necessary, + /// and outputs the following values: + /// + /// + /// isError + /// + /// true iff an exception was thrown during path string conversion or when writing to the file + /// + /// + /// + /// errorMsg + /// + /// the error message of the thrown exception if isError is true, or an empty sequence otherwise + /// + /// + /// + /// + /// We output these values individually because Result is not defined in the runtime but instead in library code. + /// It is the responsibility of library code to construct an equivalent Result value. + /// + public static void INTERNAL_AppendBytesToFile(ISequence path, ISequence bytes, out bool isError, out ISequence errorMsg) + { + isError = true; + errorMsg = Sequence.Empty; + try + { + string pathStr = path?.ToString(); + CreateParentDirs(pathStr); + using (var stream = new FileStream(pathStr, FileMode.Append)) + { + var myBytes = bytes.CloneAsArray(); + stream.Write(myBytes, 0, myBytes.Length); + } + isError = false; + } + catch (Exception e) + { + errorMsg = Helpers.SeqFromArray(e.ToString().ToCharArray()); + } + } + + /// + /// Creates the nonexistent parent directory(-ies) of the given path. + /// + private static void CreateParentDirs(string path) + { + string parentDir = Path.GetDirectoryName(Path.GetFullPath(path)); + Directory.CreateDirectory(parentDir); + } + } +} diff --git a/StandardLibrary/runtimes/net/Extern/Time.cs b/StandardLibrary/runtimes/net/Extern/Time.cs index 611cd27a5..f51ff66e8 100644 --- a/StandardLibrary/runtimes/net/Extern/Time.cs +++ b/StandardLibrary/runtimes/net/Extern/Time.cs @@ -3,6 +3,7 @@ using System; using System.Numerics; +using System.Diagnostics; using Microsoft.VisualBasic; using Wrappers_Compile; using ibyteseq = Dafny.ISequence; @@ -27,6 +28,11 @@ public static long CurrentRelativeTimeMilli() return (long)timespan.TotalMilliseconds; } + public static long GetProcessCpuTimeMillis() + { + return (long)Process.GetCurrentProcess().TotalProcessorTime.TotalMilliseconds; + } + public static _IResult GetCurrentTimeStamp() { var utcTime = DateTime.UtcNow; diff --git a/StandardLibrary/runtimes/net/STD.csproj b/StandardLibrary/runtimes/net/STD.csproj index 22a34f9c3..bb01d7630 100644 --- a/StandardLibrary/runtimes/net/STD.csproj +++ b/StandardLibrary/runtimes/net/STD.csproj @@ -64,9 +64,6 @@ - - FileIO.cs - diff --git a/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/extern/DafnyLibraries.py b/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/extern/DafnyLibraries.py index 3edd73b2f..d20779c51 100644 --- a/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/extern/DafnyLibraries.py +++ b/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/extern/DafnyLibraries.py @@ -110,6 +110,22 @@ def INTERNAL_WriteBytesToFile(path, contents): exc_str = traceback.format_exc() exc_seq = _dafny.Seq(exc_str) return (True, exc_seq) + + @staticmethod + def INTERNAL_AppendBytesToFile(path, contents): + path_str = path.VerbatimString(False) + contents_bytes = bytes(contents) + + try: + pathlib.Path(path_str).parent.mkdir(parents=True, exist_ok=True) + + with open(path_str, mode="ab") as file: + contents = file.write(contents_bytes) + return (False, _dafny.Seq()) + except: + exc_str = traceback.format_exc() + exc_seq = _dafny.Seq(exc_str) + return (True, exc_seq) @staticmethod def INTERNAL_ReadBytesFromFile(path): diff --git a/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/extern/Time.py b/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/extern/Time.py index 60d3d701e..bbdc7acb9 100644 --- a/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/extern/Time.py +++ b/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/extern/Time.py @@ -1,4 +1,5 @@ import datetime +import os import pytz import _dafny @@ -13,6 +14,10 @@ def CurrentRelativeTimeMilli(): def CurrentRelativeTime(): return round(datetime.datetime.now(tz = pytz.UTC).timestamp()) + def GetProcessCpuTimeMillis(): + t = os.times() + return round((t.user + t.system) * 1000) + def GetCurrentTimeStamp(): try: d = datetime.datetime.now(tz = pytz.UTC).strftime("%Y-%m-%dT%H:%M:%S.%fZ") diff --git a/StandardLibrary/runtimes/rust/Cargo.toml b/StandardLibrary/runtimes/rust/Cargo.toml index 4e2380d2a..776c79775 100644 --- a/StandardLibrary/runtimes/rust/Cargo.toml +++ b/StandardLibrary/runtimes/rust/Cargo.toml @@ -8,6 +8,7 @@ rust-version = "1.80.0" [dependencies] chrono = "0.4.38" +cpu-time = "1.0.0" dafny_runtime = { path = "../../../smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust"} dashmap = "6.1.0" uuid = { version = "1.11.0", features = ["v4"] } diff --git a/StandardLibrary/runtimes/rust/copy_externs.sh b/StandardLibrary/runtimes/rust/copy_externs.sh index eb901a4aa..546d95dac 100755 --- a/StandardLibrary/runtimes/rust/copy_externs.sh +++ b/StandardLibrary/runtimes/rust/copy_externs.sh @@ -5,6 +5,9 @@ cd $( dirname ${BASH_SOURCE[0]} ) SRC=../../../AwsCryptographicMaterialProviders/runtimes/rust/src/ cp $SRC/concurrent_call.rs src +# we have a separate copy of dafny_libraries, becuase +# it must not include MutableMap +# cp $SRC/dafny_libraries.rs src cp $SRC/sets.rs src cp $SRC/time.rs src cp $SRC/uuid.rs src diff --git a/StandardLibrary/runtimes/rust/src/dafny_libraries.rs b/StandardLibrary/runtimes/rust/src/dafny_libraries.rs new file mode 100644 index 000000000..604f70b89 --- /dev/null +++ b/StandardLibrary/runtimes/rust/src/dafny_libraries.rs @@ -0,0 +1,144 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +#![deny(warnings, unconditional_panic)] +#![deny(nonstandard_style)] +#![deny(clippy::all)] + +#[allow(non_snake_case)] +pub mod DafnyLibraries { + pub mod FileIO { + use std::fs::File; + use std::io::Read; + use std::io::Write; + use std::path::Path; + + // Attempts to read all bytes from the file at {@code path}, and returns a tuple of the following values: + // isError : true iff an exception was thrown during path string conversion or when reading the file + // bytesRead : the sequence of bytes read from the file, or an empty sequence if {@code isError} is true + // errorMsg : the error message of the thrown exception if {@code isError} is true, or an empty equence otherwise + // We return these values individually because Result is not defined in the runtime but + // instead in library code. It is the responsibility of library code to construct an equivalent Result value. + pub(crate) fn INTERNAL_ReadBytesFromFile( + file: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ) -> ( + bool, + ::dafny_runtime::Sequence, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ) { + let file_name = dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(file); + let path = Path::new(&file_name); + + let mut file = match File::open(path) { + Err(why) => { + let err_msg = format!( + "couldn't open {} for reading 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, dafny_runtime::Sequence::default(), err_msg); + } + Ok(file) => file, + }; + + let mut result = Vec::new(); + match file.read_to_end(&mut result) { + Err(why) => { + let err_msg = format!("couldn't read from {}: {}", path.display(), why); + let err_msg = dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&err_msg); + (true, dafny_runtime::Sequence::default(), err_msg) + } + Ok(_) => ( + false, + dafny_runtime::Sequence::from_array_owned(result), + dafny_runtime::Sequence::default(), + ), + } + } + + // Get the current dirctory for use in error messages + fn curr_dir() -> String { + let path = std::env::current_dir(); + match path { + Ok(path) => format!("{}", path.display()), + Err(_) => "Error while getting the path of current directory".to_string(), + } + } + + // Attempts to append bytes to the file at path, creating nonexistent parent + // See SendBytesToFile for details + pub(crate) fn INTERNAL_AppendBytesToFile( + path: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + bytes: &::dafny_runtime::Sequence, + ) -> ( + bool, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ) { + SendBytesToFile(path, bytes, true) + } + + // Attempts to write bytes to the file at path, creating nonexistent parent + // See SendBytesToFile for details + pub(crate) fn INTERNAL_WriteBytesToFile( + path: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + bytes: &::dafny_runtime::Sequence, + ) -> ( + bool, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ) { + SendBytesToFile(path, bytes, false) + } + + // Attempts to write bytes to the file at path, creating nonexistent parent + // directories as necessary, and returns a tuple of the following values: + // isError : true iff an exception was thrown during path string conversion or when writing to the file + // errorMsg : the error message of the thrown exception if {@code isError} is true, or an empty sequence otherwise + // We return these values individually because {@code Result} is not defined in the runtime but + // instead in library code. It is the responsibility of library code to construct an equivalent Result value. + // if append is false, the file is truncated, otherwise we append to the existing file. + fn SendBytesToFile( + path: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + bytes: &::dafny_runtime::Sequence, + append: bool, + ) -> ( + bool, + ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, + ) { + let file_name = dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(path); + let path = Path::new(&file_name); + + let maybe_file = std::fs::OpenOptions::new() + .append(append) + .write(true) + .create(true) + .truncate(!append) + .open(path); + let mut file = match maybe_file { + Err(why) => { + let err_msg = format!( + "couldn't open {} for writing 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); + } + Ok(file) => file, + }; + + let bytes = bytes.to_array(); + match file.write_all(&bytes) { + Err(why) => { + let err_msg = + format!("couldn't write all bytes to {}: {}", path.display(), why); + let err_msg = dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&err_msg); + (true, err_msg) + } + Ok(_) => (false, dafny_runtime::Sequence::default()), + } + } + } +} diff --git a/StandardLibrary/runtimes/rust/src/lib.rs b/StandardLibrary/runtimes/rust/src/lib.rs index ea7ad0578..66fa543d3 100644 --- a/StandardLibrary/runtimes/rust/src/lib.rs +++ b/StandardLibrary/runtimes/rust/src/lib.rs @@ -11,10 +11,11 @@ pub(crate) use crate::implementation_from_dafny::r#_Wrappers_Compile; pub(crate) mod sets; pub(crate) mod time; pub(crate) mod uuid; +pub(crate) mod dafny_libraries; pub(crate) use crate::implementation_from_dafny::UTF8; pub(crate) mod concurrent_call; -//pub(crate) mod dafny_libraries; pub(crate) use crate::implementation_from_dafny::ConcurrentCall; pub(crate) use crate::implementation_from_dafny::Time; pub(crate) use crate::implementation_from_dafny::UUID; +pub(crate) use crate::dafny_libraries::DafnyLibraries; diff --git a/StandardLibrary/src/Time.dfy b/StandardLibrary/src/Time.dfy index 0fe098038..178c4592a 100644 --- a/StandardLibrary/src/Time.dfy +++ b/StandardLibrary/src/Time.dfy @@ -36,11 +36,19 @@ module {:extern "Time"} Time { // be negative. ensures res >= 0 + // Returns the number of milliseconds of CPU used by the current process so far. + // Time is represented as signed over unsigned because java does not do unsigned + // values - net can do both so we are able to change the representation to signed. + method {:extern "GetProcessCpuTimeMillis"} GetProcessCpuTimeMillis() returns (res: int64) + // We are able to make this claim because it does not make sense for time to + // be negative. + ensures res >= 0 + // Returns a timestamp for the current time in ISO8601 format in UTC // to microsecond precision (e.g. “YYYY-MM-DDTHH:mm:ss.ssssssZ“) method {:extern "GetCurrentTimeStamp"} GetCurrentTimeStamp() returns (res: Result) - function method FormatMilli(diff : nat) : string + function method FormatMilli(diff : uint64) : string { var whole := String.Base10Int2String((diff / 1000) as int); var frac := String.Base10Int2String((diff % 1000) as int); @@ -57,9 +65,76 @@ module {:extern "Time"} Time { requires end >= 0 { if start <= end then - FormatMilli(end as nat - start as nat) + FormatMilli((end - start) as uint64) else - "-" + FormatMilli(start as nat - end as nat) + "-" + FormatMilli((start - end) as uint64) + } + + datatype AbsoluteTime = AbsoluteTime( + ClockTime : uint64, + CpuTime : uint64 + ) + datatype RelativeTime = RelativeTime( + ClockTime : uint64, + CpuTime : uint64 + ) + method GetAbsoluteTime() returns (output : AbsoluteTime) + { + var ClockTime := GetCurrentMilli(); + var CpuTime := GetProcessCpuTimeMillis(); + return AbsoluteTime ( + ClockTime := ClockTime as uint64, + CpuTime := CpuTime as uint64 + ); + } + + method PrintTimeSince(start : AbsoluteTime) + { + var t := TimeSince(start); + PrintTime(t); + } + + method PrintTimeSinceShort(start : AbsoluteTime) + { + var t := TimeSince(start); + PrintTimeShort(t); + } + + method PrintTimeSinceShortChained(start : AbsoluteTime) returns (x : AbsoluteTime) + { + var end := GetAbsoluteTime(); + PrintTimeShort(TimeDiff(start, end)); + return end; + } + + function method TimeDiff(start : AbsoluteTime, end : AbsoluteTime) : RelativeTime + { + if start.ClockTime <= end.ClockTime && start.CpuTime <= end.CpuTime then + RelativeTime ( + ClockTime := end.ClockTime - start.ClockTime, + CpuTime := end.CpuTime - start.CpuTime + ) + else + RelativeTime ( + ClockTime := 0, + CpuTime := 0 + ) + } + + method TimeSince(start : AbsoluteTime) returns (output : RelativeTime) + { + var end := GetAbsoluteTime(); + output := TimeDiff(start, end); + } + + method PrintTime(time : RelativeTime) + { + print "Clock Time : ", FormatMilli(time.ClockTime), " CPU Time : ", FormatMilli(time.CpuTime), "\n"; + } + + method PrintTimeShort(time : RelativeTime) + { + print "CPU:", FormatMilli(time.CpuTime), " "; } // The next two functions are for the benefit of the extern implementation to call, diff --git a/StandardLibrary/test/TestComputeSetToOrderedSequenceUInt8Less.dfy b/StandardLibrary/test/TestComputeSetToOrderedSequenceUInt8Less.dfy index 7e509c637..15818ef33 100644 --- a/StandardLibrary/test/TestComputeSetToOrderedSequenceUInt8Less.dfy +++ b/StandardLibrary/test/TestComputeSetToOrderedSequenceUInt8Less.dfy @@ -3,6 +3,7 @@ include "../src/StandardLibrary.dfy" include "../src/Sets.dfy" +include "../src/Time.dfy" // Just to make sure we don't conflict with dafny-lang/libraries' Sets.dfy include "../../libraries/src/Collections/Sets/Sets.dfy" @@ -17,6 +18,7 @@ module TestComputeSetToOrderedSequenceUInt8Less { import opened StandardLibrary import opened UInt = StandardLibrary.UInt import opened SortedSets + import Time predicate method UInt8Greater(x : uint8, y : uint8) { y < x @@ -82,12 +84,15 @@ module TestComputeSetToOrderedSequenceUInt8Less { } method {:test} TestSetToOrderedSequenceManyItems() { + var time := Time.GetAbsoluteTime(); var a := set x:uint16 | 0 <= x < 0xFFFF :: UInt16ToSeq(x); + time := Time.PrintTimeSinceShortChained(time); var output := ComputeSetToOrderedSequence(a, UInt8Less); var output2 := ComputeSetToOrderedSequence2(a, UInt8Less); var expected : seq> := seq(0xFFFF, i requires 0 <= i < 0xFFFF => UInt16ToSeq(i as uint16)); expect output == expected; expect output2 == expected; + Time.PrintTimeSinceShort(time); } } diff --git a/StandardLibrary/test/TestString.dfy b/StandardLibrary/test/TestString.dfy index 8833c3198..600ab3609 100644 --- a/StandardLibrary/test/TestString.dfy +++ b/StandardLibrary/test/TestString.dfy @@ -4,10 +4,12 @@ include "../src/StandardLibrary.dfy" include "../src/String.dfy" include "../../libraries/src/Wrappers.dfy" +include "../../libraries/src/FileIO/FileIO.dfy" module TestStrings { import StandardLibrary.String import opened Wrappers + import opened FileIO method {:test} TestHasSubStringPositive() { @@ -32,4 +34,17 @@ module TestStrings { actual := String.HasSubString("large", "larger"); expect actual == None, "Needle larger than haystack"; } -} + + method {:test} TestFileIO() + { + var x :- expect WriteBytesToFile("MyFile", [1,2,3,4,5]); + x :- expect AppendBytesToFile("MyFile", [6,7,8,9,10]); + x :- expect AppendBytesToFile("MyFile", [11,12,13,14,15]); + var y :- expect ReadBytesFromFile("MyFile"); + expect y == [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15]; + x :- expect WriteBytesToFile("MyFile", [1,2,3,4,5]); + y :- expect ReadBytesFromFile("MyFile"); + expect y == [1,2,3,4,5]; + } + +} \ No newline at end of file diff --git a/libraries b/libraries index 7af1ae1b9..c71deb6e5 160000 --- a/libraries +++ b/libraries @@ -1 +1 @@ -Subproject commit 7af1ae1b99aa893616db42c0ddeb5af6827b1524 +Subproject commit c71deb6e537856d3ae946649ed49c4979f3c06ac diff --git a/smithy-dafny b/smithy-dafny index 99d3dd9d1..5b66889c6 160000 --- a/smithy-dafny +++ b/smithy-dafny @@ -1 +1 @@ -Subproject commit 99d3dd9d1902b54e0cb1f659379c8db43aec29b9 +Subproject commit 5b66889c630658f963ebed04c4a4c33d2047f845