Skip to content

Commit 1a90c5c

Browse files
ajewellamzajewellamz
committed
m
1 parent 7ff1bbe commit 1a90c5c

File tree

3 files changed

+4209
-4126
lines changed

3 files changed

+4209
-4126
lines changed

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

Lines changed: 63 additions & 68 deletions
Original file line numberDiff line numberDiff line change
@@ -56,6 +56,9 @@ pub use ::std::cell::UnsafeCell;
5656
pub struct UnsafeCell<T: ?Sized> {
5757
data: ::std::cell::UnsafeCell<T>, // UnsafeCell for interior mutability
5858
}
59+
// SAFETY: UnsafeCell is not possibly sync normally.
60+
// However, we use it only for raw pointers, and fields and access to read and write
61+
// to fields will be subject to mutexes in any cases.
5962
#[cfg(feature = "sync")]
6063
unsafe impl<T: ?Sized> Sync for UnsafeCell<T> where T: Send {}
6164
#[cfg(feature = "sync")]
@@ -740,10 +743,10 @@ where
740743
values: Rc<Vec<T>>,
741744
},
742745
ConcatSequence {
743-
left: Rc<UnsafeCell<Sequence<T>>>,
744-
right: Rc<UnsafeCell<Sequence<T>>>,
746+
left: Rc<RefCell<Sequence<T>>>,
747+
right: Rc<RefCell<Sequence<T>>>,
745748
length: SizeT,
746-
boxed: Rc<RefCell<Option<Rc<Vec<T>>>>>,
749+
cache: Rc<RefCell<Option<Rc<Vec<T>>>>>,
747750
},
748751
}
749752

@@ -800,12 +803,12 @@ where
800803
values: Rc::new(values),
801804
}
802805
}
803-
pub fn new_concat_sequence(left: &Sequence<T>, right: &Sequence<T>) -> Sequence<T> {
806+
pub(crate) fn new_concat_sequence(left: &Sequence<T>, right: &Sequence<T>) -> Sequence<T> {
804807
Sequence::ConcatSequence {
805-
left: Rc::new(UnsafeCell::new(left.clone())),
806-
right: Rc::new(UnsafeCell::new(right.clone())),
808+
left: Rc::new(RefCell::new(left.clone())),
809+
right: Rc::new(RefCell::new(right.clone())),
807810
length: left.cardinality_usize() + right.cardinality_usize(),
808-
boxed: Rc::new(RefCell::new(None)),
811+
cache: Rc::new(RefCell::new(None)),
809812
}
810813
}
811814
pub fn to_array(&self) -> Rc<Vec<T>> {
@@ -818,40 +821,49 @@ where
818821
}
819822
Sequence::ConcatSequence {
820823
length,
821-
boxed,
824+
cache,
822825
left,
823826
right,
824827
} => {
825828
#[cfg(feature = "sync")]
826-
let into_boxed = boxed.as_ref();
827-
#[cfg(feature = "sync")]
828-
let into_boxed_borrowed = into_boxed;
829-
#[cfg(feature = "sync")]
830-
let mut guard = into_boxed_borrowed.lock().unwrap();
831-
#[cfg(feature = "sync")]
832-
let borrowed: Option<&Rc<Vec<T>>> = guard.as_ref();
829+
{
830+
let guard = cache.as_ref().lock().unwrap();
831+
let cache_borrow: Option<&Rc<Vec<T>>> = guard.as_ref();
832+
if let Some(cache) = cache_borrow {
833+
return Rc::clone(cache);
834+
}
835+
}
833836

834837
#[cfg(not(feature = "sync"))]
835-
let into_boxed = boxed.as_ref().clone();
836-
#[cfg(not(feature = "sync"))]
837-
let into_boxed_borrowed = into_boxed.borrow();
838-
#[cfg(not(feature = "sync"))]
839-
let borrowed: Option<&Rc<Vec<T>>> = into_boxed_borrowed.as_ref();
840-
if let Some(cache) = borrowed.as_ref() {
841-
return Rc::clone(cache);
838+
{
839+
let cache_opened = cache.as_ref().clone();
840+
let cache_opened_borrowed = cache_opened.borrow();
841+
let cache_borrow: Option<&Rc<Vec<T>>> = cache_opened_borrowed.as_ref();
842+
if let Some(cache) = cache_borrow {
843+
return Rc::clone(cache);
844+
}
842845
}
843846
// Let's create an array of size length and fill it up recursively
844847
// We don't materialize nested arrays because most of the time they are forgotten
845848
let mut array: Vec<T> = Vec::with_capacity(*length);
846-
Sequence::<T>::append_recursive_safe(&mut array, &borrowed, left, right);
849+
Sequence::<T>::append_recursive_safe(&mut array, &None, left, right);
847850
let result = Rc::new(array);
848-
let mutable_left: *mut Sequence<T> = left.get();
849-
let mutable_right: *mut Sequence<T> = right.get();
850-
// safety: Once the array is computed, left and right won't ever be read again.
851-
unsafe { *mutable_left = seq!() };
852-
unsafe { *mutable_right = seq!() };
853851
#[cfg(not(feature = "sync"))]
854-
let mut guard = boxed.borrow_mut();
852+
{
853+
*left.borrow_mut() = seq!();
854+
*right.borrow_mut() = seq!();
855+
}
856+
#[cfg(feature = "sync")]
857+
{
858+
let mut left_guard = left.as_ref().lock().unwrap();
859+
let mut right_guard = right.as_ref().lock().unwrap();
860+
*left_guard = seq!();
861+
*right_guard = seq!();
862+
}
863+
#[cfg(not(feature = "sync"))]
864+
let mut guard = cache.borrow_mut();
865+
#[cfg(feature = "sync")]
866+
let mut guard = cache.as_ref().lock().unwrap();
855867
*guard = Some(result.clone());
856868
result
857869
}
@@ -860,19 +872,28 @@ where
860872

861873
pub fn append_recursive_safe(
862874
array: &mut Vec<T>,
863-
borrowed: &Option<&Rc<Vec<T>>>,
864-
left: &Rc<UnsafeCell<Sequence<T>>>,
865-
right: &Rc<UnsafeCell<Sequence<T>>>,
875+
cache_borrow: &Option<&Rc<Vec<T>>>,
876+
left: &Rc<RefCell<Sequence<T>>>,
877+
right: &Rc<RefCell<Sequence<T>>>,
866878
) {
867-
if let Some(values) = borrowed.as_ref() {
879+
if let Some(values) = cache_borrow.as_ref() {
868880
for value in values.iter() {
869881
array.push(value.clone());
870882
}
871883
return;
872884
}
873-
// safety: When a concat is initialized, the left and right are well defined
874-
Sequence::<T>::append_recursive(array, unsafe { &mut *left.get() });
875-
Sequence::<T>::append_recursive(array, unsafe { &mut *right.get() });
885+
#[cfg(not(feature = "sync"))]
886+
{
887+
Sequence::<T>::append_recursive(array, &left.as_ref().borrow());
888+
Sequence::<T>::append_recursive(array, &right.as_ref().borrow());
889+
}
890+
#[cfg(feature = "sync")]
891+
{
892+
let left_guard = left.as_ref().lock().unwrap();
893+
let right_guard = right.as_ref().lock().unwrap();
894+
Sequence::<T>::append_recursive(array, &left_guard);
895+
Sequence::<T>::append_recursive(array, &right_guard);
896+
}
876897
}
877898

878899
pub fn append_recursive(array: &mut Vec<T>, this: &Sequence<T>) {
@@ -885,7 +906,7 @@ where
885906
}
886907
}
887908
Sequence::ConcatSequence {
888-
boxed, left, right, ..
909+
cache: boxed, left, right, ..
889910
} =>
890911
// Let's create an array of size length and fill it up recursively
891912
{
@@ -904,20 +925,11 @@ where
904925
let into_boxed_borrowed = into_boxed.borrow();
905926
#[cfg(not(feature = "sync"))]
906927
let borrowed: Option<&Rc<Vec<T>>> = into_boxed_borrowed.as_ref();
907-
if let Some(values) = borrowed.as_ref() {
908-
for value in values.iter() {
909-
array.push(value.clone());
910-
}
911-
return;
912-
}
913-
// safety: When a concat is initialized, the left and right are well defined
914-
Sequence::<T>::append_recursive(array, unsafe { &mut *left.get() });
915-
Sequence::<T>::append_recursive(array, unsafe { &mut *right.get() });
928+
Self::append_recursive_safe(array, &borrowed, left, right);
916929
}
917930
}
918931
}
919-
/// Returns the cardinality of this [`Sequence<T>`].
920-
// The cardinality returns the length of the sequence
932+
/// Returns the cardinality or length of this [`Sequence<T>`].
921933
pub fn cardinality_usize(&self) -> SizeT {
922934
match self {
923935
Sequence::ArraySequence { values, .. } =>
@@ -1917,14 +1929,6 @@ pub fn dafny_rational_to_int(r: &BigRational) -> BigInt {
19171929
euclidian_division(r.numer().clone(), r.denom().clone())
19181930
}
19191931

1920-
pub fn nullable_referential_equality<T: ?Sized>(left: Option<Rc<T>>, right: Option<Rc<T>>) -> bool {
1921-
match (left, right) {
1922-
(Some(l), Some(r)) => Rc::ptr_eq(&l, &r),
1923-
(None, None) => true,
1924-
_ => false,
1925-
}
1926-
}
1927-
19281932
pub fn euclidian_division<A: Signed + Zero + One + Clone + PartialEq>(a: A, b: A) -> A {
19291933
if !a.is_negative() {
19301934
if !b.is_negative() {
@@ -2131,16 +2135,6 @@ impl<T: DafnyPrint> Display for DafnyPrintWrapper<&T> {
21312135
}
21322136
}
21332137

2134-
// from gazebo
2135-
#[inline]
2136-
pub unsafe fn transmute_unchecked<A, B>(x: A) -> B {
2137-
assert_eq!(std::mem::size_of::<A>(), std::mem::size_of::<B>());
2138-
debug_assert_eq!(0, (&x as *const A).align_offset(std::mem::align_of::<B>()));
2139-
let b = std::ptr::read(&x as *const A as *const B);
2140-
std::mem::forget(x);
2141-
b
2142-
}
2143-
21442138
pub trait DafnyPrint {
21452139
fn fmt_print(&self, f: &mut Formatter<'_>, in_seq: bool) -> std::fmt::Result;
21462140

@@ -3237,7 +3231,6 @@ macro_rules! cast_any_object {
32373231
};
32383232
}
32393233

3240-
32413234
// When initializing an uninitialized field for the first time,
32423235
// we ensure we don't drop the previous content
32433236
// This is problematic if the same field is overwritten multiple times
@@ -3665,7 +3658,9 @@ pub struct AllocationTracker {
36653658
}
36663659

36673660
#[cfg(feature = "sync")]
3668-
pub fn allocate_object_track<T: 'static + Sync + Send>(allocation_tracker: &mut AllocationTracker) -> Object<T> {
3661+
pub fn allocate_object_track<T: 'static + Sync + Send>(
3662+
allocation_tracker: &mut AllocationTracker,
3663+
) -> Object<T> {
36693664
let res = allocate_object::<T>();
36703665
allocation_tracker
36713666
.allocations

0 commit comments

Comments
 (0)