Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore: add new externs for file append and cpu time #1126

Merged
merged 11 commits into from
Dec 16, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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
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"
lucasmcdonald3 marked this conversation as resolved.
Show resolved Hide resolved
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 {
lucasmcdonald3 marked this conversation as resolved.
Show resolved Hide resolved
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)
ajewellamz marked this conversation as resolved.
Show resolved Hide resolved

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())
ajewellamz marked this conversation as resolved.
Show resolved Hide resolved
}

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)
ajewellamz marked this conversation as resolved.
Show resolved Hide resolved
syscall.Getrusage(syscall.RUSAGE_SELF, usage)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The doc says this can return an error, and next line then can cause panic.

return (usage.Utime.Nano() + usage.Stime.Nano()) / 1000000
}
Loading
Loading