@@ -6,7 +6,6 @@ pub use mem::MaybeUninit;
66use num:: { bigint:: ParseBigIntError , Integer , Num , One , Signed } ;
77pub use once_cell:: unsync:: Lazy ;
88use std:: {
9- any:: Any ,
109 borrow:: Borrow ,
1110 boxed:: Box ,
1211 clone:: Clone ,
@@ -41,6 +40,15 @@ pub use num::ToPrimitive;
4140pub use num:: Zero ;
4241pub use std:: convert:: Into ;
4342
43+ pub use :: std:: any:: Any ;
44+ pub use :: std:: marker:: Send ;
45+ pub use :: std:: marker:: Sync ;
46+
47+ #[ cfg( not( feature = "sync" ) ) ]
48+ pub type DynAny = dyn Any ;
49+ #[ cfg( feature = "sync" ) ]
50+ pub type DynAny = dyn Any + Send + Sync ;
51+
4452#[ cfg( not( feature = "sync" ) ) ]
4553pub use :: std:: cell:: UnsafeCell ;
4654
@@ -812,10 +820,10 @@ where
812820 #[ cfg( feature = "sync" ) ]
813821 let into_boxed_borrowed = into_boxed;
814822 #[ cfg( feature = "sync" ) ]
815- let guard = into_boxed_borrowed. lock ( ) . unwrap ( ) ;
823+ let mut guard = into_boxed_borrowed. lock ( ) . unwrap ( ) ;
816824 #[ cfg( feature = "sync" ) ]
817825 let borrowed: Option < & Rc < Vec < T > > > = guard. as_ref ( ) ;
818-
826+
819827 #[ cfg( not( feature = "sync" ) ) ]
820828 let into_boxed = boxed. as_ref ( ) . clone ( ) ;
821829 #[ cfg( not( feature = "sync" ) ) ]
@@ -828,19 +836,38 @@ where
828836 // Let's create an array of size length and fill it up recursively
829837 // We don't materialize nested arrays because most of the time they are forgotten
830838 let mut array: Vec < T > = Vec :: with_capacity ( * length) ;
831- Sequence :: < T > :: append_recursive ( & mut array, self ) ;
839+ Sequence :: < T > :: append_recursive_safe ( & mut array, & borrowed , left , right ) ;
832840 let result = Rc :: new ( array) ;
833841 let mutable_left: * mut Sequence < T > = left. get ( ) ;
834842 let mutable_right: * mut Sequence < T > = right. get ( ) ;
835843 // safety: Once the array is computed, left and right won't ever be read again.
836844 unsafe { * mutable_left = seq ! ( ) } ;
837845 unsafe { * mutable_right = seq ! ( ) } ;
838- Self :: write_cache ( boxed, result. clone ( ) ) ;
846+ #[ cfg( not( feature = "sync" ) ) ]
847+ let mut guard = boxed. borrow_mut ( ) ;
848+ * guard = Some ( result. clone ( ) ) ;
839849 result
840850 }
841851 }
842852 }
843853
854+ pub fn append_recursive_safe (
855+ array : & mut Vec < T > ,
856+ borrowed : & Option < & Rc < Vec < T > > > ,
857+ left : & Rc < UnsafeCell < Sequence < T > > > ,
858+ right : & Rc < UnsafeCell < Sequence < T > > > ,
859+ ) {
860+ if let Some ( values) = borrowed. as_ref ( ) {
861+ for value in values. iter ( ) {
862+ array. push ( value. clone ( ) ) ;
863+ }
864+ return ;
865+ }
866+ // safety: When a concat is initialized, the left and right are well defined
867+ Sequence :: < T > :: append_recursive ( array, unsafe { & mut * left. get ( ) } ) ;
868+ Sequence :: < T > :: append_recursive ( array, unsafe { & mut * right. get ( ) } ) ;
869+ }
870+
844871 pub fn append_recursive ( array : & mut Vec < T > , this : & Sequence < T > ) {
845872 match this {
846873 Sequence :: ArraySequence { values, .. } =>
@@ -863,7 +890,7 @@ where
863890 let guard = into_boxed_borrowed. lock ( ) . unwrap ( ) ;
864891 #[ cfg( feature = "sync" ) ]
865892 let borrowed: Option < & Rc < Vec < T > > > = guard. as_ref ( ) ;
866-
893+
867894 #[ cfg( not( feature = "sync" ) ) ]
868895 let into_boxed = boxed. as_ref ( ) . clone ( ) ;
869896 #[ cfg( not( feature = "sync" ) ) ]
@@ -940,28 +967,6 @@ where
940967 }
941968}
942969
943- #[ cfg( feature = "sync" ) ]
944- impl < T > Sequence < T >
945- where
946- T : DafnyType ,
947- {
948- fn write_cache ( boxed : & Rc < RefCell < Option < Rc < Vec < T > > > > > , array : Rc < Vec < T > > ) {
949- let mut cache = boxed. lock ( ) . unwrap ( ) ;
950- * cache = Some ( array. clone ( ) ) ;
951- }
952- }
953-
954- #[ cfg( not( feature = "sync" ) ) ]
955- impl < T > Sequence < T >
956- where
957- T : DafnyType ,
958- {
959- fn write_cache ( boxed : & Rc < RefCell < Option < Rc < Vec < T > > > > > , array : Rc < Vec < T > > ) {
960- let mut cache = boxed. borrow_mut ( ) ;
961- * cache = Some ( array. clone ( ) ) ;
962- }
963- }
964-
965970pub struct SequenceIter < T : Clone > {
966971 array : Rc < Vec < T > > ,
967972 index : SizeT ,
@@ -2178,7 +2183,7 @@ impl DafnyPrint for () {
21782183 }
21792184}
21802185
2181- #[ derive( Clone ) ]
2186+ #[ derive( Clone , Copy ) ]
21822187pub struct DafnyCharUTF16 ( pub u16 ) ;
21832188pub type DafnyStringUTF16 = Sequence < DafnyCharUTF16 > ;
21842189
@@ -2254,7 +2259,7 @@ impl Sub<DafnyCharUTF16> for DafnyCharUTF16 {
22542259 }
22552260}
22562261
2257- #[ derive( Clone ) ]
2262+ #[ derive( Clone , Copy ) ]
22582263pub struct DafnyChar ( pub char ) ;
22592264pub type DafnyString = Sequence < DafnyChar > ;
22602265
@@ -3200,18 +3205,19 @@ macro_rules! is_object {
32003205#[ macro_export]
32013206macro_rules! cast_any {
32023207 ( $raw: expr) => {
3203- $crate:: Upcast :: <dyn :: std :: any :: Any >:: upcast( $crate:: read!( $raw) )
3208+ $crate:: Upcast :: <$crate :: DynAny >:: upcast( $crate:: read!( $raw) )
32043209 } ;
32053210}
32063211// cast_any_object is meant to be used on references only, to convert any references (classes or traits)*
32073212// to an Any reference trait
32083213#[ macro_export]
32093214macro_rules! cast_any_object {
32103215 ( $obj: expr) => {
3211- $crate:: UpcastObject :: <dyn :: std :: any :: Any >:: upcast( $crate:: md!( $obj) )
3216+ $crate:: UpcastObject :: <$crate :: DynAny >:: upcast( $crate:: md!( $obj) )
32123217 } ;
32133218}
32143219
3220+
32153221// When initializing an uninitialized field for the first time,
32163222// we ensure we don't drop the previous content
32173223// This is problematic if the same field is overwritten multiple times
@@ -3354,12 +3360,12 @@ impl<T: ?Sized> Ptr<T> {
33543360 }
33553361}
33563362
3357- impl < T : ?Sized + ' static + Upcast < dyn Any > > Ptr < T > {
3363+ impl < T : ?Sized + ' static + Upcast < DynAny > > Ptr < T > {
33583364 pub fn is_instance_of < U : ' static > ( self ) -> bool {
33593365 if self . is_null ( ) {
33603366 false
33613367 } else {
3362- read ! ( Upcast :: <dyn Any >:: upcast( read!( self ) ) )
3368+ read ! ( Upcast :: <DynAny >:: upcast( read!( self ) ) )
33633369 . downcast_ref :: < U > ( )
33643370 . is_some ( )
33653371 }
@@ -3490,10 +3496,10 @@ impl<T: ?Sized> Object<T> {
34903496 self . 0 . is_none ( )
34913497 }
34923498}
3493- impl < T : ?Sized + ' static + UpcastObject < dyn Any > > Object < T > {
3499+ impl < T : ?Sized + ' static + UpcastObject < DynAny > > Object < T > {
34943500 pub fn is_instance_of < U : ' static > ( self ) -> bool {
34953501 // safety: Dafny won't call this function unless it can guarantee the object is still allocated
3496- rd ! ( UpcastObject :: <dyn Any >:: upcast( rd!( self ) ) )
3502+ rd ! ( UpcastObject :: <DynAny >:: upcast( rd!( self ) ) )
34973503 . downcast_ref :: < U > ( )
34983504 . is_some ( )
34993505 }
@@ -3517,14 +3523,14 @@ impl<T: ?Sized> Default for Object<T> {
35173523 }
35183524}
35193525
3520- impl < T : ?Sized + UpcastObject < dyn Any > > Debug for Object < T > {
3526+ impl < T : ?Sized + UpcastObject < DynAny > > Debug for Object < T > {
35213527 fn fmt ( & self , f : & mut Formatter ) -> std:: fmt:: Result {
35223528 self . fmt_print ( f, false )
35233529 }
35243530}
3525- impl < T : ?Sized + UpcastObject < dyn Any > > DafnyPrint for Object < T > {
3531+ impl < T : ?Sized + UpcastObject < DynAny > > DafnyPrint for Object < T > {
35263532 fn fmt_print ( & self , f : & mut Formatter < ' _ > , _in_seq : bool ) -> std:: fmt:: Result {
3527- let obj_any = UpcastObject :: < dyn Any > :: upcast ( self . as_ref ( ) ) ;
3533+ let obj_any = UpcastObject :: < DynAny > :: upcast ( self . as_ref ( ) ) ;
35283534 let option_string = obj_any. as_ref ( ) . downcast_ref :: < String > ( ) ;
35293535 match option_string {
35303536 Some ( s) => write ! ( f, "{}" , s) ,
@@ -3538,11 +3544,10 @@ impl<T: DafnyType> DafnyPrint for Object<[T]> {
35383544 write ! ( f, "<object>" )
35393545 }
35403546}
3541-
3542- impl UpcastObject < dyn Any > for String {
3543- fn upcast ( & self ) -> Object < dyn Any > {
3547+ impl UpcastObject < DynAny > for String {
3548+ fn upcast ( & self ) -> Object < DynAny > {
35443549 // SAFETY: RC was just created
3545- unsafe { Object :: from_rc ( Rc :: new ( self . clone ( ) ) as Rc < dyn Any > ) }
3550+ unsafe { Object :: from_rc ( Rc :: new ( self . clone ( ) ) as Rc < DynAny > ) }
35463551 }
35473552}
35483553
@@ -3630,9 +3635,18 @@ pub fn allocate_object<T>() -> Object<T> {
36303635}
36313636
36323637pub struct AllocationTracker {
3633- allocations : Vec < Weak < dyn Any > > ,
3638+ allocations : Vec < Weak < DynAny > > ,
36343639}
36353640
3641+ #[ cfg( feature = "sync" ) ]
3642+ pub fn allocate_object_track < T : ' static + Sync + Send > ( allocation_tracker : & mut AllocationTracker ) -> Object < T > {
3643+ let res = allocate_object :: < T > ( ) ;
3644+ allocation_tracker
3645+ . allocations
3646+ . push ( Rc :: < UnsafeCell < T > > :: downgrade ( & res. 0 . clone ( ) . unwrap ( ) ) ) ;
3647+ res
3648+ }
3649+ #[ cfg( not( feature = "sync" ) ) ]
36363650pub fn allocate_object_track < T : ' static > ( allocation_tracker : & mut AllocationTracker ) -> Object < T > {
36373651 let res = allocate_object :: < T > ( ) ;
36383652 allocation_tracker
@@ -3778,31 +3792,17 @@ macro_rules! refcount {
37783792}
37793793
37803794pub mod object {
3781- use std:: any:: Any ;
3782-
3783- #[ cfg( not( feature = "sync" ) ) ]
3784- pub fn downcast < T : ' static > ( _self : crate :: Object < dyn Any > ) -> crate :: Object < T > {
3785- unsafe {
3786- crate :: Object ( Some ( crate :: rcmut:: downcast :: < T > ( _self. 0 . unwrap ( ) ) . unwrap ( ) ) )
3787- // Use unwrap_unchecked?
3788- }
3789- }
3795+ use crate :: { Any , DynAny } ;
37903796
3791- #[ cfg( feature = "sync" ) ]
3792- pub fn downcast < T : ' static + Send + Sync > (
3793- _self : crate :: Object < dyn Any + Send + Sync > ,
3794- ) -> crate :: Object < T > {
3795- unsafe {
3796- crate :: Object ( Some ( crate :: rcmut:: downcast :: < T > ( _self. 0 . unwrap ( ) ) . unwrap ( ) ) )
3797- // Use unwrap_unchecked?
3798- }
3797+ pub fn downcast < T : ' static > ( _self : crate :: Object < DynAny > ) -> crate :: Object < T > {
3798+ super :: cast_object!( _self, T )
37993799 }
38003800
38013801 pub fn new < T > ( val : T ) -> crate :: Object < T > {
38023802 crate :: Object ( Some ( crate :: rcmut:: new ( val) ) )
38033803 }
38043804 #[ inline]
3805- pub fn is < T : ' static + :: std :: any :: Any > ( _self : crate :: Object < dyn Any > ) -> bool {
3805+ pub fn is < T : ' static + Any > ( _self : crate :: Object < DynAny > ) -> bool {
38063806 is_object ! ( _self, T )
38073807 }
38083808}
@@ -3875,16 +3875,16 @@ pub mod rcmut {
38753875
38763876 #[ cfg( feature = "sync" ) ]
38773877 pub unsafe fn downcast < T : ' static + Send + Sync > (
3878- this : RcMut < dyn :: std :: any :: Any + Send + Sync > ,
3878+ this : RcMut < crate :: DynAny > ,
38793879 ) -> Option < RcMut < T > > {
3880- let t: Rc < dyn :: std :: any :: Any + Send + Sync > = to_rc ( this) ;
3880+ let t: Rc < crate :: DynAny > = to_rc ( this) ;
38813881 let t: Rc < T > = Rc :: downcast :: < T > ( t) . ok ( ) ?;
38823882 mem:: transmute ( t)
38833883 }
38843884
38853885 #[ cfg( not( feature = "sync" ) ) ]
3886- pub unsafe fn downcast < T : ' static > ( this : RcMut < dyn :: std :: any :: Any > ) -> Option < RcMut < T > > {
3887- let t: Rc < dyn :: std :: any :: Any > = to_rc ( this) ;
3886+ pub unsafe fn downcast < T : ' static > ( this : RcMut < crate :: DynAny > ) -> Option < RcMut < T > > {
3887+ let t: Rc < crate :: DynAny > = to_rc ( this) ;
38883888 let t: Rc < T > = Rc :: downcast :: < T > ( t) . ok ( ) ?;
38893889 mem:: transmute ( t)
38903890 }
0 commit comments