Skip to content

Commit

Permalink
chore: add new externs for file append and cpu time (#1126)
Browse files Browse the repository at this point in the history
* chore: add new externs for file append and cpu time
  • Loading branch information
ajewellamz authored Dec 16, 2024
1 parent ce65262 commit 382edfd
Show file tree
Hide file tree
Showing 27 changed files with 645 additions and 43 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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<u8>,
) -> (
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<u8>,
) -> (
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<u8>,
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) => {
Expand Down
2 changes: 1 addition & 1 deletion AwsCryptographicMaterialProviders/runtimes/rust/src/rsa.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -25,8 +25,8 @@ pub mod internal_StormTrackingCMC {
}
}

impl ::dafny_runtime::UpcastObject<dyn::std::any::Any> for StormTrackingCMC {
::dafny_runtime::UpcastObjectFn!(dyn::std::any::Any);
impl ::dafny_runtime::UpcastObject<dyn ::std::any::Any> for StormTrackingCMC {
::dafny_runtime::UpcastObjectFn!(dyn ::std::any::Any);
}

impl ::dafny_runtime::UpcastObject<dyn software::amazon::cryptography::materialproviders::internaldafny::types::ICryptographicMaterialsCache>
Expand Down
8 changes: 8 additions & 0 deletions AwsCryptographicMaterialProviders/runtimes/rust/src/time.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@
#![deny(clippy::all)]

use crate::*;
use std::convert::TryFrom;
use std::time::SystemTime;

impl crate::Time::_default {
Expand All @@ -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<
Expand Down
47 changes: 24 additions & 23 deletions AwsCryptographicMaterialProviders/runtimes/rust/src/timer.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
);
}
}

Expand All @@ -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)
}

Expand Down
1 change: 1 addition & 0 deletions AwsCryptographyPrimitives/runtimes/rust/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
1 change: 1 addition & 0 deletions ComAmazonawsDynamodb/runtimes/rust/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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"] }
Expand Down
1 change: 1 addition & 0 deletions ComAmazonawsKms/runtimes/rust/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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"] }
Expand Down
1 change: 1 addition & 0 deletions StandardLibrary/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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())
Expand All @@ -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 {
Expand All @@ -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
}
Original file line number Diff line number Diff line change
@@ -1,20 +1,44 @@
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"))...))
}

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
}
Loading

0 comments on commit 382edfd

Please sign in to comment.