Skip to content

Commit

Permalink
feat: Misc Rust runtime improvements (#5769)
Browse files Browse the repository at this point in the history
### Description
This PR makes the following improvements to the Rust runtime to make it
easier to use:

* Remove `unsafe` from some `Object` conversions where we've determined
it's not needed
* Allow `rc_struct_to_dafny_class` to be used for unsized types
* Use `$crate` hygiene in all proc macros (and fully-qualifying some
symbols), both to avoid potential name conflicts with consuming code,
and also consuming code don't need to manually bring symbols into scope

### How has this been tested?
<!-- Tests can be added to
`Source/IntegrationTests/TestFiles/LitTests/LitTest/` or to
`Source/*.Test/…` and run with `dotnet test` -->
This PR relies on existing tests; no new API features or symbols were
added.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
  • Loading branch information
alex-chew authored Sep 17, 2024
1 parent cc73a34 commit fcdb143
Showing 1 changed file with 52 additions and 48 deletions.
100 changes: 52 additions & 48 deletions Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs
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

0 comments on commit fcdb143

Please sign in to comment.