Skip to content

feat: Misc Rust runtime improvements #5769

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.

Sign up for GitHub

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

Merged
merged 4 commits into from
Sep 17, 2024
Merged

feat: Misc Rust runtime improvements #5769

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
310c10f
feat(rust): make Object conversions more lenient
alex-chew Sep 13, 2024
b203ca4
ensure all proc macros use $crate hygiene
alex-chew Sep 16, 2024
bf1a89e
add a couple more $crate
alex-chew Sep 16, 2024
129874c
Merge branch 'master' into alexchew/misc-rust-runtime-improvements
alex-chew Sep 17, 2024
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
100 changes: 52 additions & 48 deletions Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,15 +8,19 @@ pub use once_cell::unsync::Lazy;
use std::{
any::Any,
borrow::Borrow,
boxed::Box,
cell::{RefCell, UnsafeCell},
clone::Clone,
cmp::Ordering,
collections::{HashMap, HashSet},
convert::From,
fmt::{Debug, Display, Formatter},
hash::{Hash, Hasher},
ptr::NonNull,
mem,
ops::{Add, Deref, Div, Mul, Neg, Rem, Sub},
ops::{Add, Deref, Div, Fn, Mul, Neg, Rem, Sub},
rc::{Rc, Weak},
vec::Vec,
};

pub use system::*;
Expand Down Expand Up @@ -71,11 +75,11 @@ pub mod dafny_runtime_conversions {
pub type DafnyArray2<T> = crate::Object<crate::Array2<T>>;
pub type DafnyArray3<T> = crate::Object<crate::Array3<T>>;
// Conversion to and from Dafny reference-counted classes. All these methods take ownership of the class.
pub unsafe fn dafny_class_to_struct<T: Clone>(ptr: DafnyClass<T>) -> T {
pub fn dafny_class_to_struct<T: Clone>(ptr: DafnyClass<T>) -> T {
let t: &T = crate::rd!(ptr);
t.clone()
}
pub unsafe fn dafny_class_to_boxed_struct<T: Clone>(ptr: DafnyClass<T>) -> Box<T> {
pub fn dafny_class_to_boxed_struct<T: Clone>(ptr: DafnyClass<T>) -> Box<T> {
Box::new(dafny_class_to_struct(ptr))
}
pub unsafe fn dafny_class_to_rc_struct<T: Clone + ?Sized>(ptr: DafnyClass<T>) -> ::std::rc::Rc<T> {
Expand All @@ -87,7 +91,7 @@ pub mod dafny_runtime_conversions {
pub fn boxed_struct_to_dafny_class<T>(t: Box<T>) -> DafnyClass<T> {
struct_to_dafny_class(*t)
}
pub unsafe fn rc_struct_to_dafny_class<T>(t: ::std::rc::Rc<T>) -> DafnyClass<T> {
pub unsafe fn rc_struct_to_dafny_class<T: ?Sized>(t: ::std::rc::Rc<T>) -> DafnyClass<T> {
crate::Object::from_rc(t)
}
// Conversions to and from Dafny arrays. They all take ownership
Expand Down Expand Up @@ -590,14 +594,14 @@ impl DafnyInt {
macro_rules! impl_dafnyint_from {
() => {};
($type:ident) => {
impl From<$type> for DafnyInt {
impl $crate::From<$type> for $crate::DafnyInt {
fn from(n: $type) -> Self {
DafnyInt {
data: Rc::new(n.into()),
$crate::DafnyInt {
data: $crate::Rc::new(n.into()),
}
}
}
impl DafnyUsize for $type {
impl $crate::DafnyUsize for $type {
fn into_usize(self) -> usize {
self as usize
}
Expand Down Expand Up @@ -1986,8 +1990,8 @@ impl<A: DafnyPrint> DafnyPrint for LazyFieldWrapper<A> {
// Convert the DafnyPrint above into a macro so that we can create it for functions of any input arity
macro_rules! dafny_print_function {
($($n:tt)*) => {
impl <B, $($n),*> DafnyPrint for Rc<dyn Fn($($n),*) -> B> {
fn fmt_print(&self, f: &mut Formatter<'_>, _in_seq: bool) -> std::fmt::Result {
impl <B, $($n),*> $crate::DafnyPrint for $crate::Rc<dyn $crate::Fn($($n),*) -> B> {
fn fmt_print(&self, f: &mut ::std::fmt::Formatter<'_>, _in_seq: bool) -> ::std::fmt::Result {
write!(f, "<function>")
}
}
Expand Down Expand Up @@ -2060,9 +2064,9 @@ impl<T> DafnyPrint for *const T {

macro_rules! impl_print_display {
($name:ty) => {
impl DafnyPrint for $name {
fn fmt_print(&self, f: &mut Formatter<'_>, _in_seq: bool) -> std::fmt::Result {
std::fmt::Display::fmt(&self, f)
impl $crate::DafnyPrint for $name {
fn fmt_print(&self, f: &mut ::std::fmt::Formatter<'_>, _in_seq: bool) -> ::std::fmt::Result {
::std::fmt::Display::fmt(&self, f)
}
}
};
Expand Down Expand Up @@ -2407,12 +2411,12 @@ pub fn string_utf16_of(s: &str) -> DafnyStringUTF16 {

macro_rules! impl_tuple_print {
($($items:ident)*) => {
impl <$($items,)*> DafnyPrint for ($($items,)*)
impl <$($items,)*> $crate::DafnyPrint for ($($items,)*)
where
$($items: DafnyPrint,)*
$($items: $crate::DafnyPrint,)*
{
#[allow(unused_assignments)]
fn fmt_print(&self, f: &mut Formatter<'_>, _in_seq: bool) -> std::fmt::Result {
fn fmt_print(&self, f: &mut ::std::fmt::Formatter<'_>, _in_seq: bool) -> ::std::fmt::Result {
#[allow(non_snake_case)]
let ($($items,)*) = self;

Expand Down Expand Up @@ -2527,8 +2531,8 @@ macro_rules! int {
macro_rules! ARRAY_GETTER_LENGTH0 {
() => {
#[inline]
pub fn length0(&self) -> DafnyInt {
DafnyInt::from(self.length0_usize())
pub fn length0(&self) -> $crate::DafnyInt {
$crate::DafnyInt::from(self.length0_usize())
}
#[inline]
pub fn length0_usize(&self) -> usize {
Expand All @@ -2539,7 +2543,7 @@ macro_rules! ARRAY_GETTER_LENGTH0 {
macro_rules! ARRAY_GETTER_LENGTH {
($field: ident, $field_usize: ident) => {
#[inline]
pub fn $field(&self) -> DafnyInt {
pub fn $field(&self) -> $crate::DafnyInt {
$crate::DafnyInt::from(self.$field_usize())
}
#[inline]
Expand All @@ -2553,14 +2557,14 @@ macro_rules! ARRAY_GETTER_LENGTH {
#[macro_export]
macro_rules! array {
($($x:expr), *) => {
array::from_native(Box::new([$($x), *]))
$crate::array::from_native($crate::Box::new([$($x), *]))
}
}

macro_rules! ARRAY_INIT {
{$length: ident, $inner: expr} => {
$crate::array::initialize_box_usize($length, {
Rc::new(move |_| { $inner })
$crate::Rc::new(move |_| { $inner })
})
}
}
Expand All @@ -2575,10 +2579,10 @@ macro_rules! ARRAY_INIT_INNER {
// Box<[Box<[Box<[T]>]>]>
macro_rules! ARRAY_DATA_TYPE {
($length:ident) => {
Box<[T]>
$crate::Box<[T]>
};
($length:ident, $($rest_length:ident),+) => {
Box<[ARRAY_DATA_TYPE!($($rest_length),+)]>
$crate::Box<[ARRAY_DATA_TYPE!($($rest_length),+)]>
};
}

Expand All @@ -2602,18 +2606,18 @@ macro_rules! ARRAY_METHODS {
pub fn placebos_box_usize(
$length0: usize,
$($length: usize),+
) -> Box<$ArrayType<$crate::MaybeUninit<T>>> {
Box::new($ArrayType {
) -> $crate::Box<$ArrayType<$crate::MaybeUninit<T>>> {
$crate::Box::new($ArrayType {
$($length: $length),+,
data: INIT_ARRAY_DATA!($ArrayType, $length0, $($length),+),
})
}

pub fn placebos_usize(
$length0: usize,
$($length: usize),+
) -> Ptr<$ArrayType<$crate::MaybeUninit<T>>> {
Ptr::from_box(Self::placebos_box_usize(
) -> $crate::Ptr<$ArrayType<$crate::MaybeUninit<T>>> {
$crate::Ptr::from_box(Self::placebos_box_usize(
$length0,
$($length),+
))
Expand All @@ -2633,19 +2637,19 @@ macro_rules! ARRAY_METHODS {
pub fn placebos(
$length0: &$crate::DafnyInt,
$($length: &$crate::DafnyInt),+
) -> Ptr<$ArrayType<$crate::MaybeUninit<T>>> {
) -> $crate::Ptr<$ArrayType<$crate::MaybeUninit<T>>> {
Self::placebos_usize(
$length0.as_usize(),
$($length.as_usize()),+
)
}

// Once all the elements have been initialized, transform the signature of the pointer
pub fn construct(p: Ptr<$ArrayType<$crate::MaybeUninit<T>>>) -> Ptr<$ArrayType<T>> {
pub fn construct(p: $crate::Ptr<$ArrayType<$crate::MaybeUninit<T>>>) -> $crate::Ptr<$ArrayType<T>> {
unsafe { std::mem::transmute(p) }
}
// Once all the elements have been initialized, transform the signature of the pointer
pub fn construct_object(p: $crate::Object<$ArrayType<MaybeUninit<T>>>) -> Object<$ArrayType<T>> {
pub fn construct_object(p: $crate::Object<$ArrayType<$crate::MaybeUninit<T>>>) -> $crate::Object<$ArrayType<T>> {
unsafe { std::mem::transmute(p) }
}
};
Expand All @@ -2672,15 +2676,15 @@ macro_rules! ARRAY_TO_VEC_LOOP {
};
(@inner $self: ident, $outerTmp: ident, $data: expr $(, $rest_length_usize: ident)*) => {
{
let mut tmp = Vec::new();
let mut tmp = $crate::Vec::new();
ARRAY_TO_VEC_LOOP!(@for $self, tmp, $data $(, $rest_length_usize)*);
$outerTmp.push(tmp);
}
};

($self: ident, $data: expr $(, $rest_length_usize: ident)*) => {
{
let mut tmp = Vec::new();
let mut tmp = $crate::Vec::new();
ARRAY_TO_VEC_LOOP!(@for $self, tmp, $data $(, $rest_length_usize)*);
tmp
}
Expand All @@ -2689,10 +2693,10 @@ macro_rules! ARRAY_TO_VEC_LOOP {

macro_rules! ARRAY_TO_VEC_TYPE {
($length0: ident) => {
Vec<T>
$crate::Vec<T>
};
($length0: ident $(, $res_length: ident)*) => {
Vec<ARRAY_TO_VEC_TYPE!($($res_length), *)>
$crate::Vec<ARRAY_TO_VEC_TYPE!($($res_length), *)>
}
}

Expand Down Expand Up @@ -2747,7 +2751,7 @@ macro_rules! ARRAY_DEF {
$(($length, $length_usize)), +
}
}
impl<T: Clone> $ArrayType<T> {
impl<T: $crate::Clone> $ArrayType<T> {
ARRAY_TO_VEC_WRAPPER!{
$(($length, $length_usize)), +
}
Expand All @@ -2757,12 +2761,12 @@ macro_rules! ARRAY_DEF {

// Array2 to Array16

ARRAY_DEF!{Array2,
ARRAY_DEF!{Array2,
(length0, length0_usize),
(length1, length1_usize)
}

ARRAY_DEF!{Array3,
ARRAY_DEF!{Array3,
(length0, length0_usize),
(length1, length1_usize),
(length2, length2_usize)
Expand Down Expand Up @@ -3107,15 +3111,15 @@ macro_rules! is_object {
#[macro_export]
macro_rules! cast_any {
($raw:expr) => {
$crate::Upcast::<dyn Any>::upcast($crate::read!($raw))
$crate::Upcast::<dyn $crate::Any>::upcast($crate::read!($raw))
};
}
// cast_any_object is meant to be used on references only, to convert any references (classes or traits)*
// to an Any reference trait
#[macro_export]
macro_rules! cast_any_object {
($obj:expr) => {
$crate::UpcastObject::<dyn Any>::upcast($crate::md!($obj))
$crate::UpcastObject::<dyn $crate::Any>::upcast($crate::md!($obj))
};
}

Expand Down Expand Up @@ -3551,7 +3555,7 @@ macro_rules! rd {
#[macro_export]
macro_rules! refcount {
($x:expr) => {
Rc::strong_count(unsafe { rcmut::as_rc($x.0.as_ref().unwrap()) })
$crate::Rc::strong_count(unsafe { $crate::rcmut::as_rc($x.0.as_ref().unwrap()) })
};
}

Expand Down Expand Up @@ -3835,10 +3839,10 @@ macro_rules! UpcastDef {
$crate::UpcastFn!($B);
}
};

($A:ty, $B:ty, $($C: ty),*) => {
UpcastDef!($A, $B);
UpcastDef!($A, $($C),*);
$crate::UpcastDef!($A, $B);
$crate::UpcastDef!($A, $($C),*);
}
}

Expand All @@ -3849,10 +3853,10 @@ macro_rules! UpcastDefObject {
$crate::UpcastObjectFn!($B);
}
};

($A:ty, $B:ty, $($C: ty),*) => {
UpcastDefObject!($A, $B);
UpcastDefObject!($A, $($C),*);
$crate::UpcastDefObject!($A, $B);
$crate::UpcastDefObject!($A, $($C),*);
}
}

Expand Down