Skip to content

Commit 2c9c322

Browse files
ajewellamzajewellamz
committed
m
1 parent a3b9837 commit 2c9c322

File tree

2 files changed

+66
-30
lines changed
  • releases/rust/db_esdk/dafny_runtime_rust/src

2 files changed

+66
-30
lines changed

‎releases/rust/db_esdk/dafny_runtime_rust/src/lib.rs‎

Lines changed: 22 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -79,17 +79,16 @@ impl<T: ?Sized> UnsafeCell<T> {
7979
// An atomic box is just a RefCell in Rust
8080
pub type SizeT = usize;
8181

82+
#[cfg(not(feature = "sync"))]
83+
pub trait DafnyType: Clone + DafnyPrint + 'static {}
8284
#[cfg(feature = "sync")]
8385
pub trait DafnyType: Clone + DafnyPrint + Send + Sync + 'static {}
8486

8587
#[cfg(not(feature = "sync"))]
86-
pub trait DafnyType: Clone + DafnyPrint + 'static {}
87-
88+
impl<T> DafnyType for T where T: Clone + DafnyPrint + 'static {}
8889
#[cfg(feature = "sync")]
8990
impl<T> DafnyType for T where T: Clone + DafnyPrint + Send + Sync + 'static {}
9091

91-
#[cfg(not(feature = "sync"))]
92-
impl<T> DafnyType for T where T: Clone + DafnyPrint + 'static {}
9392
pub trait DafnyTypeEq: DafnyType + Hash + Eq {}
9493

9594
impl<T> DafnyTypeEq for T where T: DafnyType + Hash + Eq {}
@@ -2070,6 +2069,18 @@ impl<A: DafnyPrint> DafnyPrint for LazyFieldWrapper<A> {
20702069
}
20712070
}
20722071

2072+
#[cfg(feature = "sync")]
2073+
// Convert the DafnyPrint above into a macro so that we can create it for functions of any input arity
2074+
macro_rules! dafny_print_function {
2075+
($($n:tt)*) => {
2076+
impl <B, $($n),*> $crate::DafnyPrint for $crate::Rc<dyn ::std::ops::Fn($($n),*) -> B + Send + Sync> {
2077+
fn fmt_print(&self, f: &mut ::std::fmt::Formatter<'_>, _in_seq: bool) -> ::std::fmt::Result {
2078+
write!(f, "<function>")
2079+
}
2080+
}
2081+
}
2082+
}
2083+
#[cfg(not(feature = "sync"))]
20732084
// Convert the DafnyPrint above into a macro so that we can create it for functions of any input arity
20742085
macro_rules! dafny_print_function {
20752086
($($n:tt)*) => {
@@ -2080,6 +2091,7 @@ macro_rules! dafny_print_function {
20802091
}
20812092
}
20822093
}
2094+
20832095
// Now create a loop like impl_tuple_print_loop so that we can create functions up to size 32
20842096
macro_rules! dafny_print_function_loop {
20852097
($first:ident $($rest:ident)*) => {
@@ -3340,6 +3352,12 @@ macro_rules! update_field_mut_if_uninit {
33403352
// This Ptr has the same run-time space as *mut
33413353
pub struct Ptr<T: ?Sized>(pub Option<NonNull<UnsafeCell<T>>>);
33423354

3355+
#[cfg(feature = "sync")]
3356+
unsafe impl<T: ?Sized> Send for Ptr<T> {}
3357+
3358+
#[cfg(feature = "sync")]
3359+
unsafe impl<T: ?Sized> Sync for Ptr<T> {}
3360+
33433361
impl<T: ?Sized> Ptr<T> {
33443362
pub fn null() -> Self {
33453363
Ptr(None)

‎releases/rust/db_esdk/dafny_runtime_rust/src/tests/mod.rs‎

Lines changed: 44 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -47,18 +47,24 @@ mod tests {
4747
#[cfg(not(feature = "sync"))]
4848
assert!(boxed.as_ref().clone().borrow().as_ref().is_none());
4949
#[cfg(feature = "sync")]
50-
assert!(boxed.as_ref().clone().borrow().lock().unwrap().as_ref().is_none());
50+
assert!(boxed.as_ref().lock().unwrap().as_ref().is_none());
5151
}
5252
_ => panic!("This should never happen"),
5353
}
5454
let value = concat.get_usize(0);
5555
assert_eq!(value, 1);
5656
match &concat {
5757
crate::Sequence::ConcatSequence { boxed, .. } => {
58+
#[cfg(not(feature = "sync"))]
5859
assert_eq!(
5960
*boxed.as_ref().clone().borrow().as_ref().unwrap().as_ref(),
6061
vec![1, 2, 3, 4, 5, 6]
6162
);
63+
#[cfg(feature = "sync")]
64+
assert_eq!(
65+
*boxed.as_ref().lock().unwrap().as_ref().unwrap().as_ref(),
66+
vec![1, 2, 3, 4, 5, 6]
67+
);
6268
}
6369
_ => panic!("This should never happen"),
6470
}
@@ -443,11 +449,11 @@ mod tests {
443449
}
444450
}
445451

446-
impl <T: DafnyType> Upcast<dyn Any> for ClassWrapper<T> {
447-
UpcastFn!(dyn Any);
452+
impl <T: DafnyType> Upcast<crate::DynAny> for ClassWrapper<T> {
453+
UpcastFn!(crate::DynAny);
448454
}
449-
impl <T: DafnyType> UpcastObject<dyn Any> for ClassWrapper<T> {
450-
UpcastObjectFn!(dyn Any);
455+
impl <T: DafnyType> UpcastObject<crate::DynAny> for ClassWrapper<T> {
456+
UpcastObjectFn!(crate::DynAny);
451457
}
452458

453459
#[test]
@@ -549,19 +555,19 @@ mod tests {
549555
#[test]
550556
fn test_coercion_immutable() {
551557
let o = ClassWrapper::<i32>::constructor(1);
552-
let a: Ptr<dyn Any> = Upcast::<dyn Any>::upcast(read!(o));
558+
let a: Ptr<crate::DynAny> = Upcast::<crate::DynAny>::upcast(read!(o));
553559
assert_eq!(cast!(a, ClassWrapper<i32>), o);
554560
let seq_o = seq![o];
555-
let seq_a = Sequence::<Ptr<ClassWrapper<i32>>>::coerce(upcast::<ClassWrapper<i32>, dyn Any>())(seq_o);
561+
let seq_a = Sequence::<Ptr<ClassWrapper<i32>>>::coerce(upcast::<ClassWrapper<i32>, crate::DynAny>())(seq_o);
556562
assert_eq!(cast!(seq_a.get_usize(0), ClassWrapper<i32>), o);
557563
let set_o = set! {o};
558-
let set_a = Set::<Ptr<ClassWrapper<i32>>>::coerce(upcast::<ClassWrapper<i32>, dyn Any>())(set_o);
564+
let set_a = Set::<Ptr<ClassWrapper<i32>>>::coerce(upcast::<ClassWrapper<i32>, crate::DynAny>())(set_o);
559565
assert_eq!(cast!(set_a.peek(), ClassWrapper<i32>), o);
560566
let multiset_o = multiset! {o, o};
561-
let multiset_a = Multiset::<Ptr<ClassWrapper<i32>>>::coerce(upcast::<ClassWrapper<i32>, dyn Any>())(multiset_o);
567+
let multiset_a = Multiset::<Ptr<ClassWrapper<i32>>>::coerce(upcast::<ClassWrapper<i32>, crate::DynAny>())(multiset_o);
562568
assert_eq!(cast!(multiset_a.peek(), ClassWrapper<i32>), o);
563569
let map_o = map![1 => o, 2 => o];
564-
let map_a = Map::<i32, Ptr<ClassWrapper<i32>>>::coerce(upcast::<ClassWrapper<i32>, dyn Any>())(map_o);
570+
let map_a = Map::<i32, Ptr<ClassWrapper<i32>>>::coerce(upcast::<ClassWrapper<i32>, crate::DynAny>())(map_o);
565571
assert_eq!(cast!(map_a.get(&1), ClassWrapper<i32>), o);
566572
deallocate(o);
567573
}
@@ -594,7 +600,7 @@ mod tests {
594600

595601
#[test]
596602
fn test_function_wrappers() {
597-
let f: Rc<dyn Fn(i32) -> i32> = Rc::new(|i: i32| i + 1);
603+
let f: Rc<dyn Fn(i32) -> i32 + Send + Sync> = Rc::new(|i: i32| i + 1);
598604
let g = f.clone();
599605
let _h = seq![g];
600606
}
@@ -688,10 +694,22 @@ mod tests {
688694
let count_inner = count.clone();
689695
multiset!{1, 1, 5, 7, 8}
690696
.iter().for_each(move |_i: u32| {
691-
let c: i32 = *count_inner.as_ref().borrow();
692-
*count_inner.borrow_mut() = c + 1;
697+
#[cfg(not(feature = "sync"))]
698+
{
699+
let c: i32 = *count_inner.as_ref().borrow();
700+
*count_inner.borrow_mut() = c + 1;
701+
}
702+
#[cfg(feature = "sync")]
703+
{
704+
let mut guard = count_inner.as_ref().lock().unwrap();
705+
let c: i32 = *guard;
706+
*guard = c + 1;
707+
}
693708
});
709+
#[cfg(not(feature = "sync"))]
694710
assert_eq!(*count.as_ref().borrow(), 5);
711+
#[cfg(feature = "sync")]
712+
assert_eq!(*count.as_ref().lock().unwrap(), 5);
695713

696714
let m = map![1 => 4, 3 => 6, 5 => 8];
697715
let m2 = m.clone();
@@ -748,7 +766,7 @@ mod tests {
748766
assert_eq!(sum, 55);
749767
}
750768

751-
trait SuperTrait: Upcast<dyn Any> + UpcastObject<dyn Any> {
769+
trait SuperTrait: Upcast<crate::DynAny> + UpcastObject<crate::DynAny> {
752770
}
753771

754772
trait NodeRcMutTrait: SuperTrait + Upcast<dyn SuperTrait> + UpcastObject<dyn SuperTrait>{
@@ -767,11 +785,11 @@ mod tests {
767785
}
768786
}
769787
impl SuperTrait for NodeRcMut {}
770-
impl UpcastObject<dyn Any> for NodeRcMut {
771-
UpcastObjectFn!(dyn Any);
788+
impl UpcastObject<crate::DynAny> for NodeRcMut {
789+
UpcastObjectFn!(crate::DynAny);
772790
}
773-
impl Upcast<dyn Any> for NodeRcMut {
774-
UpcastFn!(dyn Any);
791+
impl Upcast<crate::DynAny> for NodeRcMut {
792+
UpcastFn!(crate::DynAny);
775793
}
776794
impl UpcastObject<dyn NodeRcMutTrait> for NodeRcMut {
777795
UpcastObjectFn!(dyn NodeRcMutTrait);
@@ -798,7 +816,7 @@ mod tests {
798816
assert_eq!(x.as_ref().next.as_ref().val, int!(42));
799817
md!(rd!(x).next).next = Object(None);
800818
assert_eq!(refcount!(x), 1);
801-
let y: Object<dyn Any> = upcast_object::<_, _>()(x.clone());
819+
let y: Object<crate::DynAny> = upcast_object::<_, _>()(x.clone());
802820
assert_eq!(refcount!(x), 2);
803821
let z: Object<dyn NodeRcMutTrait> = upcast_object::<_, _>()(x.clone());
804822
assert_eq!(refcount!(x), 3);
@@ -834,7 +852,7 @@ mod tests {
834852
}
835853
assert_eq!(refcount!(x), previous_count);
836854

837-
let objects: Set<Object<dyn ::std::any::Any>> = crate::set!{y.clone(), cast_any_object!(x.clone())};
855+
let objects: Set<Object<crate::DynAny>> = crate::set!{y.clone(), cast_any_object!(x.clone())};
838856
assert_eq!(objects.cardinality_usize(), 1);
839857
test_dafny_type(a.clone());
840858
}
@@ -850,8 +868,8 @@ mod tests {
850868
}
851869
}
852870
impl NodeRcMutTrait for NodeRawMut {}
853-
UpcastDefObject!(NodeRawMut, dyn NodeRcMutTrait, dyn SuperTrait, dyn Any);
854-
UpcastDef!(NodeRawMut, dyn NodeRcMutTrait, dyn SuperTrait, dyn Any);
871+
UpcastDefObject!(NodeRawMut, dyn NodeRcMutTrait, dyn SuperTrait, crate::DynAny);
872+
UpcastDef!(NodeRawMut, dyn NodeRcMutTrait, dyn SuperTrait, crate::DynAny);
855873

856874
impl SuperTrait for NodeRawMut {}
857875

@@ -863,7 +881,7 @@ mod tests {
863881
modify!(x.clone()).next = x.clone();
864882
assert_eq!(read!(read!(x.clone()).next.clone()).val, int!(42));
865883
modify!(read!(x.clone()).next.clone()).next = Ptr::null();
866-
let y: Ptr<dyn Any> = upcast::<_, _>()(x);
884+
let y: Ptr<crate::DynAny> = upcast::<_, _>()(x);
867885
assert!(y.is_instance_of::<NodeRawMut>());
868886
assert!(!y.is_instance_of::<NodeRcMut>());
869887
let z: Ptr<dyn NodeRcMutTrait> = upcast::<_, _>()(x);
@@ -907,13 +925,13 @@ mod tests {
907925
pub message: String,
908926
}
909927

910-
crate::UpcastDefObject!(InternalOpaqueError, dyn Any);
928+
crate::UpcastDefObject!(InternalOpaqueError, crate::DynAny);
911929

912930
#[test]
913931
fn test_native_string_upcast() {
914932
let s = InternalOpaqueError { message: "Hello, World!".to_string() };
915933
let o: Object<InternalOpaqueError> = Object::new(s);
916-
let n: Object<dyn ::std::any::Any> = upcast_object::<InternalOpaqueError, dyn ::std::any::Any>()(o);
934+
let n: Object<crate::DynAny> = upcast_object::<InternalOpaqueError, crate::DynAny>()(o);
917935
let x = cast_object!(n, InternalOpaqueError);
918936
let s2 = crate::dafny_runtime_conversions::object::dafny_class_to_struct(x);
919937
assert_eq!(s2.message, "Hello, World!");
@@ -923,7 +941,7 @@ mod tests {
923941
fn test_native_string_upcast_raw() {
924942
let message = "Hello, World!".to_string();
925943
let object = Object::new(message.clone());
926-
let object_any: Object<dyn Any> = UpcastObject::<dyn Any>::upcast(object.as_ref());
944+
let object_any: Object<crate::DynAny> = UpcastObject::<crate::DynAny>::upcast(object.as_ref());
927945
let resulting_message = format!("{:?}", object_any);
928946
assert_eq!(resulting_message, message);
929947
}

0 commit comments

Comments
 (0)