From 21b61d2997ee1347768276b11913eba7498ec1a4 Mon Sep 17 00:00:00 2001 From: Herman Venter Date: Fri, 5 Feb 2021 13:31:20 -0800 Subject: [PATCH 1/7] Do not infer thin pointer path types --- checker/src/block_visitor.rs | 33 +++++++++++++++++---------------- checker/src/call_visitor.rs | 14 ++++++++------ checker/src/path.rs | 14 +++++++++++--- 3 files changed, 36 insertions(+), 25 deletions(-) diff --git a/checker/src/block_visitor.rs b/checker/src/block_visitor.rs index 0c97d530..af14a0e2 100644 --- a/checker/src/block_visitor.rs +++ b/checker/src/block_visitor.rs @@ -1639,7 +1639,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E> .starts_with_slice_pointer(source_type.kind()) { // Need to upgrade the thin pointer to a fat pointer - let target_thin_pointer_path = + let (target_thin_pointer_path, _) = Path::get_path_to_thin_pointer_at_offset_0( self.bv.tcx, &self.bv.current_environment, @@ -1647,7 +1647,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E> ty, ) .expect("there to be such path because ty starts with it"); - let source_thin_pointer_path = + let (source_thin_pointer_path, thin_ptr_type) = Path::get_path_to_thin_pointer_at_offset_0( self.bv.tcx, &self.bv.current_environment, @@ -1657,10 +1657,6 @@ impl<'block, 'analysis, 'compilation, 'tcx, E> .expect( "there to be such a path because source_type can cast to target type", ); - let thin_ptr_type = self.bv.type_visitor.get_path_rustc_type( - &source_thin_pointer_path, - self.bv.current_span, - ); let target_type = type_visitor::get_target_type(thin_ptr_type); self.bv.copy_or_move_elements( target_thin_pointer_path.clone(), @@ -2935,16 +2931,14 @@ impl<'block, 'analysis, 'compilation, 'tcx, E> let selector = self.visit_projection_elem(ty, elem); match elem { mir::ProjectionElem::Deref => { - if let Some(thin_pointer_path) = Path::get_path_to_thin_pointer_at_offset_0( - self.bv.tcx, - &self.bv.current_environment, - &result, - ty, - ) { - let thin_ptr_type = self - .bv - .type_visitor - .get_path_rustc_type(&thin_pointer_path, self.bv.current_span); + if let Some((thin_pointer_path, thin_ptr_type)) = + Path::get_path_to_thin_pointer_at_offset_0( + self.bv.tcx, + &self.bv.current_environment, + &result, + ty, + ) + { ty = type_visitor::get_target_type(thin_ptr_type); let deref_path = Path::new_deref(thin_pointer_path, ExpressionType::from(ty.kind())); @@ -2960,6 +2954,13 @@ impl<'block, 'analysis, 'compilation, 'tcx, E> } mir::ProjectionElem::Field(_, field_ty) => { if let Some(prev) = prev_result { + //todo: Actually, field 0 of fat pointer path does not have to mean + //the thin pointer. It looks like we might have to unroll the qualifier + //if the field type is not an actual raw pointer. Perhaps only well known + //types behave like fat pointers. Perhaps also, we might be better off to + // normalize fields into (typed) offsets. At any rate, the code below is wrong. + // Make some test cases. + // The previous selector was a deref of a fat pointer, which in MIR seems // to be any struct that has a field 0 that is a thin or fat pointer. // When such a path is used as is, or as the qualifier of an index or slice diff --git a/checker/src/call_visitor.rs b/checker/src/call_visitor.rs index b7fb3f0c..138bdc43 100644 --- a/checker/src/call_visitor.rs +++ b/checker/src/call_visitor.rs @@ -1131,13 +1131,13 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E> let target_type = ExpressionType::from( type_visitor::get_target_type(self.actual_argument_types[0]).kind(), ); - let source_thin_pointer_path = Path::get_path_to_thin_pointer_at_offset_0( + let (source_thin_pointer_path, _) = Path::get_path_to_thin_pointer_at_offset_0( self.block_visitor.bv.tcx, &self.block_visitor.bv.current_environment, &source_pointer_path, source_pointer_rustc_type, ) - .unwrap_or(source_pointer_path); + .unwrap_or((source_pointer_path, source_pointer_rustc_type)); let source_path = Path::new_deref(source_thin_pointer_path, target_type) .canonicalize(&self.block_visitor.bv.current_environment); trace!("MiraiAddTag: tagging {:?} with {:?}", tag, source_path); @@ -1219,13 +1219,13 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E> let target_type = ExpressionType::from( type_visitor::get_target_type(self.actual_argument_types[0]).kind(), ); - let source_thin_pointer_path = Path::get_path_to_thin_pointer_at_offset_0( + let (source_thin_pointer_path, _) = Path::get_path_to_thin_pointer_at_offset_0( self.block_visitor.bv.tcx, &self.block_visitor.bv.current_environment, &source_pointer_path, source_pointer_rustc_type, ) - .unwrap_or(source_pointer_path); + .unwrap_or((source_pointer_path, source_pointer_rustc_type)); let source_path = Path::new_deref(source_thin_pointer_path, target_type) .canonicalize(&self.block_visitor.bv.current_environment); trace!( @@ -2056,7 +2056,8 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E> &source_path, source_rustc_type, ) - .unwrap_or(source_path); + .unwrap_or((source_path, target_rustc_type)) + .0; } else if type_visitor::is_thin_pointer(&source_rustc_type.kind()) { target_path = Path::get_path_to_thin_pointer_at_offset_0( self.block_visitor.bv.tcx, @@ -2064,7 +2065,8 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E> &target_path, target_rustc_type, ) - .unwrap_or(target_path); + .unwrap_or((target_path, source_rustc_type)) + .0; } fn add_leaf_fields_for<'a>( diff --git a/checker/src/path.rs b/checker/src/path.rs index 2e8c804c..52cf9166 100644 --- a/checker/src/path.rs +++ b/checker/src/path.rs @@ -373,7 +373,7 @@ impl Path { environment: &Environment, path: &Rc, path_rustc_type: Ty<'tcx>, - ) -> Option> { + ) -> Option<(Rc, Ty<'tcx>)> { trace!( "get_path_to_thin_pointer_at_offset_0 {:?} {:?}", path, @@ -382,12 +382,20 @@ impl Path { match path_rustc_type.kind() { TyKind::Ref(..) | TyKind::RawPtr(..) => { if type_visitor::is_slice_pointer(path_rustc_type.kind()) { - Some(Path::new_field(path.clone(), 0)) + let elem_t = type_visitor::get_element_type(path_rustc_type); + let ft = tcx.mk_ptr(rustc_middle::ty::TypeAndMut { + ty: elem_t, + mutbl: rustc_hir::Mutability::Not, + }); + Some((Path::new_field(path.clone(), 0), ft)) } else { - Some(path.clone()) + Some((path.clone(), path_rustc_type)) } } TyKind::Adt(def, substs) => { + if def.is_enum() { + return None; + } let path0 = Path::new_field(path.clone(), 0); for v in def.variants.iter() { if let Some(field0) = v.fields.get(0) { From d04aa0c8048d9518e086a0f1a2b9a9d1093a15ff Mon Sep 17 00:00:00 2001 From: Herman Venter Date: Tue, 9 Feb 2021 13:57:46 -0800 Subject: [PATCH 2/7] Keep derefs from places in paths --- binaries/summary_store.tar | Bin 1267200 -> 1268224 bytes checker/src/block_visitor.rs | 46 +++++++++++++--------- checker/src/body_visitor.rs | 21 +++++----- checker/src/call_visitor.rs | 40 +++++++++++-------- checker/src/callbacks.rs | 37 ++++++------------ checker/src/path.rs | 74 ++++------------------------------- checker/src/type_visitor.rs | 8 +++- 7 files changed, 87 insertions(+), 139 deletions(-) diff --git a/binaries/summary_store.tar b/binaries/summary_store.tar index db4dfa3b7107ab115d2bd80cff6cbbdc0aa09f97..a72c4ee50276c78186a4fb28a02851cbbab4fd8f 100644 GIT binary patch delta 4082 zcmeHKYfw{16wVDv?&aRV-rS{-T7*O+4-J@L2(c=n6#+Fq==kik0&1xag22@G18C7Y zK8i*;?bK16+S1Nohx)qJ>KJM}`lDJ}i`709wYD=VN?JhBYPy$zO&p&^X8NN$bM9<* zzw@0vCuh&@7FF4c_SnnTYRo2UoOwWk&SZ{{PcX}L@s3R8%-s~VhVq)SS`*^#PWhEk zJ>soqtIljOncLMZW}vPjCBhL=6A2&^C?XYFyNNDIwT)n#UWCMVkyc$WD>El2Z$^`alF1zB zg-9st!K9U1s zQ&QBjNV zY8vuash*)j-gXAFt`gXA1f@`qZ3i+-G>>a2pxqD`a%y-!>k^4;3nbT!5dJL+g{ZHP zsmo^DLvgQvP_sxC%zjken#Q_z5Ub$S@UxyEln-$6!M4ONj-nKXnY`&j8q+5GUDVW~ zvs5?w)}6jQ0rwN7Tyal2xXU5AZ#sLj4D5&>3Z|o+4Qfv#t<*C??AJ)}Ol0ik)R4DX zZS>4`{xpD^=O;kM{!TU0Gr`U^$__Q>HnmM8d{hJ-m0r~#ZyqY1zJpSg=*X?BrEd52 z_5ymX`43Vg`Fb|+_Z!aPOq=4ce0h;frh;L~e1FlX;Sc?v48HZJJCi};hRYnEw`zO{ zFOCn<{8&e)8zNd**8ng#Xl&F~D2^0*!P*851J9-5C`Xc2eczG_HPNad38IxwG~cot z{(5M^#hBz1P`q9qCPrM-Frfj|LH%n?lUBZdqD-a)onD9%XRv~T>JE#w&6+`!I6Xi( zmO-12amQF!KE&n;Ft7_`A|czQq!Y5zTbPz+P|X(_yTI1IG;kK77|58ZN``amH3Px) zDH;cSfJP1Biv>>9EfV(n(Z8NQ{5sQ8C;q%tC|7pXqPXS_VbE4Op*kgtZJ7zj^*B`C zk_uP!I1Ub1ks_0{gwnx88`d#XdyXk7i<)@~0(xT;ylf*mv$GfZ`~$nxi@?IhjUF{B z|Bgk1Wq3_yO%im>$ojO>hRM^aJREZ-30k<_+lM3GKsXRuX*Z|)ArEYwf!O=UioqGE zV+@OfpIdO`$4efB(HW=(dmkU7(msT!@%xIfrDL}xdSJiw@ga(dAc(7#SB4Z8-z@PU zN+Wy_brOQ-!YbdlfA&^8LX3&T$7y=V@XuS>)=HrI9BVYd~xsgnz`rm<~)bLF#Sp)l+>RtvQWSSj}#1Nuee&#o_2g~FD;*x*}z z)ZWzxCfKmS-*qTC&A$D1oC!8mqR7XF2X`x6cr13NbL~(woV-FRLU=}8_B@_P-KXw8 z#Pfe+%#qPY5g;9@ob(}04f=k#-$TMD)+Ayb<-grrma}BU&dNuI`yTuw<9!eQkxqH= zOy_z;DTIFXd)s3o*`~zukvNuW0{u6Na4H)3G@K0;wPgDY-JsC|U&1M%=qrT+PFk>y zZ2X||RIG!<6x>%Y<<|=_f9CymVE-8Jo&V;o3#&JN7~RA{{tp}$%TjQYf_-(gYdc#l z&z8jib&JK&vp?p!*}2)VnT68}X1!W;_aN0tkFNHsXM3#4=WcZYY{v~7OnmuR?ERXz PS}c~1=eS6X!*12z`IZJ> delta 3097 zcmds3dr(wm6u)=b$K~F;es{kQ>87YlfGmn~m&XE{3g%nESK8Fbv=oS@2xx^eBZ7~} zK>=IiXoiw$)1)-`>S}2NqfX{%i9ImX(x%Br8Ez^=yRTq%MXZjcqM_nLMN7r4(^D}3tK(bkU~4_D<1Uhkpw37ed^$6Yi%qv`rwvJtz&oC^Ux-JE%tG6M6)BXp6s5Fon zSXh`g`W@bBW%HRps5MEwAOTAT2-&LfD?f~)9ajbhK<^~t=O~;hLqa{Wv}!gLn?&C; zQCBwy9V)qEfSe+IPeWt!nk?Qq4FZp#u@I8O5-)#NfOYTVp-^xPX}eMwTPXyn)=uZ0 zMKqRNcP!yB;xr0?%SVyo_{P}{KCV3^s9mD>=XY6-VBYyErGpxilxYWAf%u ze?ErBa@^&e!}GWnCRDZ7p&waC<*Y{vCMOR+@vrzibQ22u82r08%l)16EITA2X#^-= z2ysx|fMoZV0?8*4_89E@1QD{{7Q;Q(_P@a(O43xYA82=@UkX$e>)PCEwuo^m2sPX!9r`~ly?ejlsvu<*NwTC$vZ>)a!-?S^#PCiZa9%UTu?HcsT-z7M{b3Rz zshM5`_dSH#Ful1$-6<^5^i};EO^!dV|Ih(qlz)S^La?l!jY`S6N{9CIrwynS4FH{j4i&UB@>TC2p=Z+Kt&E-WeEEG z)>7VShyB?&zWcr^_1&#AtWa)W=9}*&<`E>_J`Yib}Ci)Y^a}yP*Xv?ws2SJ9)*`f%dJI9(l!B5SIB?|jE{OX8!62gi* zS2M|cizZ!@&ICZ>ue@xaO;TEmW)zeTA;UYjMRh?W*w^-k(U{rrZju72^{8KmBIRZE ze{?I?&J65&6zyrm+?)^eg=0t@*ky@RtA>$m7UtB`hwMSu<_&%riNhYEHM$R$;5lB5 z2p7XiKksf&ojQ`3S>J~AOMfaaBxiNbx0AVZ!X7i%?)@OAP6pMTl#fBWGinTfvp>{~ zCxbONnp+Do8wU1CBm*i>2^_fAnPiZb(`r+2RI7!4ktD(MRNR|DY&|=k@!#dlzwYK8 ze@}p%dV!Qzin3ZTk(|@=zm4B@nBSnuU^%# eX?=)f&`%{-%cqf!O}{NVCbF$-SJ~;rrT-g&y$^W+ diff --git a/checker/src/block_visitor.rs b/checker/src/block_visitor.rs index af14a0e2..5120aa8e 100644 --- a/checker/src/block_visitor.rs +++ b/checker/src/block_visitor.rs @@ -124,7 +124,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E> /// Write the RHS Rvalue to the LHS Place. #[logfn_inputs(TRACE)] fn visit_assign(&mut self, place: &mir::Place<'tcx>, rvalue: &mir::Rvalue<'tcx>) { - let mut path = self.visit_place_defer_refinement(place); + let mut path = self.visit_lh_place(place); match &path.value { PathEnum::PhantomData => { // No need to track this data @@ -147,7 +147,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E> place: &mir::Place<'tcx>, variant_index: rustc_target::abi::VariantIdx, ) { - let target_path = Path::new_discriminant(self.visit_place(place)); + let target_path = Path::new_discriminant(self.visit_rh_place(place)); let ty = self .bv .type_visitor @@ -453,8 +453,8 @@ impl<'block, 'analysis, 'compilation, 'tcx, E> .clone(); let func_to_call = Rc::new(func_const.clone().into()); let destination = Some((*place, target)); - let path = self.visit_place(place); - let val = self.bv.lookup_path_and_refine_result(path.clone(), ty); + let path = self.visit_rh_place(place); + let ref_to_path_value = AbstractValue::make_reference(path); let mut call_visitor = CallVisitor::new( self, destructor.did, @@ -463,7 +463,10 @@ impl<'block, 'analysis, 'compilation, 'tcx, E> self.bv.current_environment.clone(), func_const, ); - call_visitor.actual_args = vec![(path, val)]; + call_visitor.actual_args = vec![( + Path::new_computed(ref_to_path_value.clone()), + ref_to_path_value, + )]; call_visitor.actual_argument_types = actual_argument_types; call_visitor.cleanup = unwind; call_visitor.destination = destination; @@ -1396,7 +1399,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E> /// with place. #[logfn_inputs(TRACE)] fn visit_used_copy(&mut self, target_path: Rc, place: &mir::Place<'tcx>) { - let rpath = self.visit_place(place); + let rpath = self.visit_rh_place(place); let rtype = self .bv .type_visitor @@ -1410,7 +1413,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E> /// with place, and also remove the (path', value) pair from the environment. #[logfn_inputs(TRACE)] fn visit_used_move(&mut self, target_path: Rc, place: &mir::Place<'tcx>) { - let rpath = self.visit_place(place); + let rpath = self.visit_rh_place(place); let rtype = self .bv .type_visitor @@ -1441,7 +1444,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E> .bv .type_visitor .get_path_rustc_type(&path, self.bv.current_span); - let value_path = self.visit_place_defer_refinement(place); + let value_path = self.visit_lh_place(place); let value = match &value_path.value { PathEnum::QualifiedPath { qualifier, @@ -1563,7 +1566,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E> // With more optimization the len instruction becomes a constant. self.visit_constant(None, &len) } else { - let mut value_path = self.visit_place_defer_refinement(place); + let mut value_path = self.visit_lh_place(place); if let PathEnum::QualifiedPath { qualifier, selector, @@ -1626,7 +1629,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E> return; } }; - let source_path = self.visit_place(place); + let source_path = self.visit_rh_place(place); let source_type = self.get_operand_rustc_type(operand); if let PointerCast::Unsize = pointer_cast { // Unsize a pointer/reference value, e.g., `&[T; n]` to`&[T]`. @@ -1694,7 +1697,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E> .visit_operand(operand) .cast(ExpressionType::from(ty.kind())); if let mir::Operand::Move(place) = operand { - let source_path = self.visit_place(place); + let source_path = self.visit_rh_place(place); self.bv.current_environment.value_map = self.bv.current_environment.value_map.remove(&source_path); } @@ -1862,7 +1865,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E> /// Read the discriminant of an enum and assign to path. #[logfn_inputs(TRACE)] fn visit_discriminant(&mut self, path: Rc, place: &mir::Place<'tcx>) { - let discriminant_path = Path::new_discriminant(self.visit_place(place)); + let discriminant_path = Path::new_discriminant(self.visit_rh_place(place)); let discriminant_value = self .bv .lookup_path_and_refine_result(discriminant_path, self.bv.tcx.types.u128); @@ -1923,7 +1926,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E> #[logfn_inputs(TRACE)] fn get_operand_path(&mut self, operand: &mir::Operand<'tcx>) -> Rc { match operand { - mir::Operand::Copy(place) | mir::Operand::Move(place) => self.visit_place(place), + mir::Operand::Copy(place) | mir::Operand::Move(place) => self.visit_rh_place(place), mir::Operand::Constant(..) => Path::new_computed(self.visit_operand(operand)), } } @@ -1965,7 +1968,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E> /// by construction during build, but also checked by the MIR type checker. #[logfn_inputs(TRACE)] fn visit_copy(&mut self, place: &mir::Place<'tcx>) -> Rc { - let path = self.visit_place(place); + let path = self.visit_rh_place(place); let rust_place_type = self .bv .type_visitor @@ -1980,7 +1983,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E> /// `Copy` may be converted to `Move` to enable "last-use" optimizations. #[logfn_inputs(TRACE)] fn visit_move(&mut self, place: &mir::Place<'tcx>) -> Rc { - let path = self.visit_place(place); + let path = self.visit_rh_place(place); let rust_place_type = self .bv .type_visitor @@ -2773,7 +2776,7 @@ impl<'block, 'analysis, 'compilation, 'tcx, E> /// Returns a normalized Path instance that is the essentially the same as the Place instance, but which /// can be serialized and used as a cache key. Also caches the place type with the path as key. #[logfn_inputs(TRACE)] - pub fn visit_place(&mut self, place: &mir::Place<'tcx>) -> Rc { + pub fn visit_rh_place(&mut self, place: &mir::Place<'tcx>) -> Rc { let place_path = self.get_path_for_place(place); let mut path = place_path.canonicalize(&self.bv.current_environment); match &place_path.value { @@ -2839,13 +2842,13 @@ impl<'block, 'analysis, 'compilation, 'tcx, E> path } - /// Returns a Path instance that is the essentially the same as the Place instance, but which + /// Returns a Path instance that is essentially the same as the Place instance, but which /// can be serialized and used as a cache key. Also caches the place type with the path as key. /// The path is not normalized so deref selectors are left in place until it is determined if /// the fat pointer is being dereferenced to get at its target value, or dereferenced to make /// a copy of it. #[logfn_inputs(TRACE)] - pub fn visit_place_defer_refinement(&mut self, place: &mir::Place<'tcx>) -> Rc { + pub fn visit_lh_place(&mut self, place: &mir::Place<'tcx>) -> Rc { self.get_path_for_place(place) } @@ -2946,7 +2949,12 @@ impl<'block, 'analysis, 'compilation, 'tcx, E> .type_visitor .path_ty_cache .insert(deref_path.clone(), ty); - prev_result = Some(result); + let fat_pointer_target_type = type_visitor::get_target_type(ty); + let fat_pointer_path = Path::new_deref( + result, + ExpressionType::from(fat_pointer_target_type.kind()), + ); + prev_result = Some(fat_pointer_path); result = deref_path; continue; } diff --git a/checker/src/body_visitor.rs b/checker/src/body_visitor.rs index d64a6deb..6c7e4d92 100644 --- a/checker/src/body_visitor.rs +++ b/checker/src/body_visitor.rs @@ -1174,7 +1174,7 @@ impl<'analysis, 'compilation, 'tcx, E> BodyVisitor<'analysis, 'compilation, 'tcx // drop the assignment of the length field continue; } - _ => assume_unreachable!("something went wrong here"), + _ => assume_unreachable!("something went wrong here: {:?}", tpath), } } } @@ -2003,15 +2003,6 @@ impl<'analysis, 'compilation, 'tcx, E> BodyVisitor<'analysis, 'compilation, 'tcx // be saddled with removing it. This case corresponds to no_children being true. if val_type == ExpressionType::NonPrimitive || val_type == ExpressionType::Function { // First look at paths that are rooted in rpath. - // Remove an explicit deref from source_path to make it a valid root. - let source_path = match &source_path.value { - PathEnum::QualifiedPath { - qualifier, - selector, - .. - } if **selector == PathSelector::Deref => qualifier.clone(), - _ => source_path, - }; let value_map = self.current_environment.value_map.clone(); for (path, value) in value_map .iter() @@ -2511,8 +2502,14 @@ impl<'analysis, 'compilation, 'tcx, E> BodyVisitor<'analysis, 'compilation, 'tcx ) -> (Rc, Rc) { precondition!(!root_rustc_type.is_scalar()); - let tag_field_path = - Path::new_tag_field(qualifier.clone()).canonicalize(&self.current_environment); + let target_type = type_visitor::get_target_type(root_rustc_type); + let tag_field_path = if target_type != root_rustc_type { + let target_type = ExpressionType::from(target_type.kind()); + Path::new_tag_field(Path::new_deref(qualifier.clone(), target_type)) + .canonicalize(&self.current_environment) + } else { + Path::new_tag_field(qualifier.clone()).canonicalize(&self.current_environment) + }; let mut tag_field_value = self.lookup_path_and_refine_result( tag_field_path.clone(), self.type_visitor.dummy_untagged_value_type, diff --git a/checker/src/call_visitor.rs b/checker/src/call_visitor.rs index 138bdc43..b78726dd 100644 --- a/checker/src/call_visitor.rs +++ b/checker/src/call_visitor.rs @@ -338,7 +338,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E> .bv .type_visitor .get_rustc_place_type(place, self.block_visitor.bv.current_span); - let target_path = self.block_visitor.visit_place(place); + let target_path = self.block_visitor.visit_rh_place(place); if !summary.is_computed { self.deal_with_missing_summary(); // Now just do a deep copy and carry on. @@ -450,7 +450,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E> } KnownNames::MiraiResult => { if let Some((place, _)) = &self.destination { - let target_path = self.block_visitor.visit_place(place); + let target_path = self.block_visitor.visit_rh_place(place); let target_rustc_type = self .block_visitor .bv @@ -547,7 +547,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E> let result = self.try_to_inline_special_function(); if !result.is_bottom() { if let Some((place, _)) = &self.destination { - let target_path = self.block_visitor.visit_place(place); + let target_path = self.block_visitor.visit_rh_place(place); self.block_visitor .bv .current_environment @@ -1014,7 +1014,15 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E> let mut argument_map = self.callee_generic_argument_map.clone(); if closure_ty.is_closure() { if self.callee_known_name != KnownNames::StdSyncOnceCallOnce { - actual_args.insert(0, self.actual_args[0].clone()); + let closure_path = self.actual_args[0].0.clone(); + let closure_reference = AbstractValue::make_reference(closure_path); + actual_args.insert( + 0, + ( + Path::get_as_path(closure_reference.clone()), + closure_reference, + ), + ); actual_argument_types.insert(0, closure_ref_ty); } //todo: could this be a generator? @@ -1092,7 +1100,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E> #[logfn_inputs(TRACE)] fn handle_abstract_value(&mut self) { if let Some((place, target)) = &self.destination { - let path = self.block_visitor.visit_place(place); + let path = self.block_visitor.visit_rh_place(place); let expression_type = self .block_visitor .bv @@ -1338,7 +1346,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E> // Return the abstract result and update exit conditions. let destination = &self.destination; if let Some((place, _)) = destination { - let target_path = self.block_visitor.visit_place(place); + let target_path = self.block_visitor.visit_rh_place(place); self.block_visitor.bv.current_environment.update_value_at( target_path.clone(), result.unwrap_or_else(|| { @@ -1378,7 +1386,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E> let source_path = Path::new_model_field(qualifier, field_name) .canonicalize(&self.block_visitor.bv.current_environment); - let target_path = self.block_visitor.visit_place(place); + let target_path = self.block_visitor.visit_rh_place(place); if self .block_visitor .bv @@ -1655,7 +1663,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E> } } } - let target_path = self.block_visitor.visit_place(place); + let target_path = self.block_visitor.visit_rh_place(place); self.block_visitor .bv .current_environment @@ -1797,7 +1805,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E> KnownNames::StdIntrinsicsMulWithOverflow => mir::BinOp::Mul, _ => assume_unreachable!(), }; - let target_path = self.block_visitor.visit_place(target_place); + let target_path = self.block_visitor.visit_rh_place(target_place); let path0 = Path::new_field(target_path.clone(), 0); let path1 = Path::new_field(target_path.clone(), 1); let target_type = self @@ -1880,7 +1888,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E> .canonicalize(&self.block_visitor.bv.current_environment); let source_path = &Path::get_as_path(self.actual_args[1].1.clone()); if let Some((place, _)) = &self.destination { - let target_path = self.block_visitor.visit_place(place); + let target_path = self.block_visitor.visit_rh_place(place); let root_rustc_type = self .block_visitor .bv @@ -1920,7 +1928,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E> return Rc::new((ty_and_layout.layout.size.bytes() as u128).into()); } } - let path = self.block_visitor.visit_place( + let path = self.block_visitor.visit_rh_place( &self .destination .expect("std::intrinsics::size_of should have a destination") @@ -1953,7 +1961,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E> return Rc::new((ty_and_layout.layout.align.abi.bytes() as u128).into()); } // todo: need an expression that resolves to the value size once the value is known (typically after call site refinement). - let path = self.block_visitor.visit_place( + let path = self.block_visitor.visit_rh_place( &self .destination .expect("std::intrinsics::min_align_of_val should have a destination") @@ -2013,7 +2021,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E> } } // todo: need an expression that resolves to the value size once the value is known (typically after call site refinement). - let path = self.block_visitor.visit_place( + let path = self.block_visitor.visit_rh_place( &self .destination .expect("std::intrinsics::size_of_value should have a destination") @@ -2042,7 +2050,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E> .expect("rustc type error") .expect_ty(); if let Some((place, _)) = &self.destination { - let mut target_path = self.block_visitor.visit_place(place); + let mut target_path = self.block_visitor.visit_rh_place(place); let target_rustc_type = self .block_visitor .bv @@ -2527,7 +2535,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E> let destination = self.destination; if let Some((place, _)) = &destination { // Assign function result to place - let target_path = self.block_visitor.visit_place(place); + let target_path = self.block_visitor.visit_rh_place(place); let result_path = &Some(target_path.clone()); let return_value_path = Path::new_result(); @@ -2613,7 +2621,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E> pub fn add_post_condition_to_exit_conditions(&mut self, function_summary: &Summary) { let destination = self.destination; if let Some((place, target)) = &destination { - let target_path = self.block_visitor.visit_place(place); + let target_path = self.block_visitor.visit_rh_place(place); let result_path = &Some(target_path); let mut exit_condition = self .block_visitor diff --git a/checker/src/callbacks.rs b/checker/src/callbacks.rs index 374b9260..70d0bfa0 100644 --- a/checker/src/callbacks.rs +++ b/checker/src/callbacks.rs @@ -139,33 +139,20 @@ impl MiraiCallbacks { } fn is_excluded(file_name: &str) -> bool { - file_name.contains("common/logger/src") - || file_name.contains("config/src") - || file_name.contains("config/management/src") + file_name.contains("config/src") + || file_name.contains("config/management/src") || file_name.contains("config/management/operational/src") || file_name.contains("config/management/genesis/src") - || file_name.contains("language/bytecode-verifier/src") - || file_name.contains("language/compiler/src") - || file_name.contains("language/compiler/ir-to-bytecode/src") - || file_name.contains("language/compiler/ir-to-bytecode/syntax/src") - || file_name.contains("language/diem-tools/diem-events-fetcher/src") - || file_name.contains("language/diem-vm/src") - || file_name.contains("language/move-lang/src") - || file_name.contains("language/move-model/src") - || file_name.contains("language/move-prover/src") // compiler panic - || file_name.contains("language/move-prover/bytecode/src") - || file_name.contains("language/move-prover/abigen/src") - || file_name.contains("language/move-prover/docgen/src") - || file_name.contains("language/move-prover/spec-lang/src") // compiler panic - || file_name.contains("language/move-vm/test-utils/src") - || file_name.contains("language/stdlib/src") - || file_name.contains("language/tools/move-cli/src") - || file_name.contains("language/tools/move-coverage/src") - || file_name.contains("language/libra-tools/transaction-replay/src") - || file_name.contains("language/vm/src") - || file_name.contains("secure/push-metrics/src") - || file_name.contains("state-synchronizer/src") // Z3 encoding error - || file_name.contains("storage/diemdb/src") + || file_name.contains("consensus/safety-rules/src") + || file_name.contains("crypto/crypto/src") + || file_name.contains("language/move-lang/src") // too slow + || file_name.contains("language/move-model/src") // too slow + || file_name.contains("language/move-prover/bytecode/src") // too slow + || file_name.contains("language/vm/src") // too slow + || file_name.contains("network/network-address/src") + || file_name.contains("secure/storage/vault/src") + || file_name.contains("state-synchronizer/src") // Z3 encoding error + || file_name.contains("types/src") // too slow } /// Analyze the crate currently being compiled, using the information given in compiler and tcx. diff --git a/checker/src/path.rs b/checker/src/path.rs index 52cf9166..112b0a21 100644 --- a/checker/src/path.rs +++ b/checker/src/path.rs @@ -92,7 +92,7 @@ impl Path { /// When splitting paths while doing weak updates, it is important to not refine paths because /// they are already canonical and because doing so can lead to recursive loops as refined paths /// re-introduce joined paths that have been split earlier. - /// A split path, however, can be serve as the qualifier of a newly constructed qualified path + /// A split path, however, can serve as the qualifier of a newly constructed qualified path /// and the qualified path might not be canonical. This routine tries to remove the two sources of /// de-canonicalization that are currently know. Essentially: when a path that binds to a value /// that is a reference is implicitly dereferenced by the selector, the canonical path will @@ -103,7 +103,7 @@ impl Path { /// If the function returns a re-canonicalized path, which is used as the qualifier of a newly /// constructed qualified path, the caller of this function should check if the selector of the /// qualified path is `PathSelector::Deref`. If so, the deref selector should also be removed. - #[logfn_inputs(DEBUG)] + #[logfn_inputs(TRACE)] pub fn try_to_dereference(path: &Rc, environment: &Environment) -> Option> { if let PathEnum::Computed { value } = &path.value { if let Expression::Reference(path) = &value.expression { @@ -639,17 +639,6 @@ impl Path { #[logfn_inputs(TRACE)] pub fn new_discriminant(enum_path: Rc) -> Rc { let selector = Rc::new(PathSelector::Discriminant); - if let PathEnum::QualifiedPath { - qualifier: base_qualifier, - selector: base_selector, - .. - } = &enum_path.value - { - if *base_selector.as_ref() == PathSelector::Deref { - // no need for an explicit deref in a qualifier - return Path::new_qualified(base_qualifier.clone(), selector); - } - } Self::new_qualified(enum_path, selector) } @@ -657,17 +646,6 @@ impl Path { #[logfn_inputs(TRACE)] pub fn new_field(qualifier: Rc, field_index: usize) -> Rc { let selector = Rc::new(PathSelector::Field(field_index)); - if let PathEnum::QualifiedPath { - qualifier: base_qualifier, - selector: base_selector, - .. - } = &qualifier.value - { - if *base_selector.as_ref() == PathSelector::Deref { - // no need for an explicit deref in a qualifier - return Path::new_qualified(base_qualifier.clone(), selector); - } - } Self::new_qualified(qualifier, selector) } @@ -685,17 +663,6 @@ impl Path { #[logfn_inputs(TRACE)] pub fn new_index(collection_path: Rc, index_value: Rc) -> Rc { let selector = Rc::new(PathSelector::Index(index_value)); - if let PathEnum::QualifiedPath { - qualifier: base_qualifier, - selector: base_selector, - .. - } = &collection_path.value - { - if *base_selector.as_ref() == PathSelector::Deref { - // no need for an explicit deref in a qualifier - return Path::new_qualified(base_qualifier.clone(), selector); - } - } Self::new_qualified(collection_path, selector) } @@ -761,17 +728,6 @@ impl Path { #[logfn_inputs(TRACE)] pub fn new_length(array_path: Rc) -> Rc { let selector = Rc::new(PathSelector::Field(1)); - if let PathEnum::QualifiedPath { - qualifier: base_qualifier, - selector: base_selector, - .. - } = &array_path.value - { - if *base_selector.as_ref() == PathSelector::Deref { - // no need for an explicit deref in a qualifier - return Path::new_qualified(base_qualifier.clone(), selector); - } - } Self::new_qualified(array_path, selector) } @@ -986,18 +942,6 @@ impl PathRefinement for Rc { } = &self.value { let canonical_qualifier = qualifier.canonicalize(environment); - // (*p).q is equivalent to p.q, etc. - if let PathEnum::QualifiedPath { - qualifier: base_qualifier, - selector: base_selector, - .. - } = &canonical_qualifier.value - { - if *base_selector.as_ref() == PathSelector::Deref { - // no need for an explicit deref in a qualifier - return Path::new_qualified(base_qualifier.clone(), selector.clone()); - } - } // If the canonical qualifier binds to a special value, we may need to deconstruct that // value before constructing the qualified path. let qualifier_as_value = @@ -1014,18 +958,13 @@ impl PathRefinement for Rc { // address of the parameter, which is the same in the pre and post state, // but is it true in other cases? Expression::InitialParameterValue { path, .. } => { - if let PathEnum::QualifiedPath { - qualifier, - selector: qs, - .. - } = &path.value - { + if let PathEnum::QualifiedPath { selector: qs, .. } = &path.value { if *qs.as_ref() == PathSelector::Deref { - // old(q.deref).s => old(q.s) + // old(q.deref).s => old(q.deref.s) return Path::new_computed( AbstractValue::make_initial_parameter_value( ExpressionType::ThinPointer, - Path::new_qualified(qualifier.clone(), selector.clone()), + Path::new_qualified(path.clone(), selector.clone()), ), ); } @@ -1045,6 +984,9 @@ impl PathRefinement for Rc { return Path::new_qualified(p.clone(), selector.clone()) .canonicalize(environment); } + Expression::Variable { path, .. } => { + return Path::new_qualified(path.clone(), selector.clone()); + } _ => {} } } diff --git a/checker/src/type_visitor.rs b/checker/src/type_visitor.rs index 127f0966..05d44b5b 100644 --- a/checker/src/type_visitor.rs +++ b/checker/src/type_visitor.rs @@ -76,14 +76,20 @@ impl<'analysis, 'compilation, 'tcx> TypeVisitor<'tcx> { path: &Rc, first_state: &mut Environment, ) { + let mut is_ref = false; if let TyKind::Ref(_, t, _) = path_ty.kind() { + is_ref = true; path_ty = t; } match path_ty.kind() { TyKind::Closure(_, substs) => { for (i, ty) in substs.as_closure().upvar_tys().enumerate() { let var_type: ExpressionType = ty.kind().into(); - let closure_field_path = Path::new_field(path.clone(), i); + let mut qualifier = path.clone(); + if is_ref { + qualifier = Path::new_deref(path.clone(), ExpressionType::NonPrimitive) + } + let closure_field_path = Path::new_field(qualifier, i); self.path_ty_cache.insert(closure_field_path.clone(), ty); let closure_field_val = AbstractValue::make_typed_unknown(var_type, closure_field_path.clone()); From 47447a7e169d85add10dcca4da4b84e3f6fb3357 Mon Sep 17 00:00:00 2001 From: Herman Venter Date: Wed, 10 Feb 2021 18:26:56 -0800 Subject: [PATCH 3/7] Fix min_align_of_val --- checker/src/call_visitor.rs | 2 +- checker/tests/run-pass/vec_dealloc.rs | 23 +++++++++++++++++++++++ 2 files changed, 24 insertions(+), 1 deletion(-) create mode 100644 checker/tests/run-pass/vec_dealloc.rs diff --git a/checker/src/call_visitor.rs b/checker/src/call_visitor.rs index b78726dd..6f214824 100644 --- a/checker/src/call_visitor.rs +++ b/checker/src/call_visitor.rs @@ -1956,7 +1956,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E> fn handle_min_align_of_val(&mut self) -> Rc { let param_env = self.block_visitor.bv.tcx.param_env(self.callee_def_id); checked_assume!(self.actual_argument_types.len() == 1); - let t = self.actual_argument_types[0]; + let t = type_visitor::get_target_type(self.actual_argument_types[0]); if let Ok(ty_and_layout) = self.block_visitor.bv.tcx.layout_of(param_env.and(t)) { return Rc::new((ty_and_layout.layout.align.abi.bytes() as u128).into()); } diff --git a/checker/tests/run-pass/vec_dealloc.rs b/checker/tests/run-pass/vec_dealloc.rs new file mode 100644 index 00000000..f90f2c7a --- /dev/null +++ b/checker/tests/run-pass/vec_dealloc.rs @@ -0,0 +1,23 @@ +// Copyright (c) Facebook, Inc. and its affiliates. +// +// This source code is licensed under the MIT license found in the +// LICENSE file in the root directory of this source tree. +// + +// A test that checks layout consistency for vec alloc/dealloc + +fn might_be_none(i: u8) -> Option { + if i > 0 { + Some(i) + } else { + None + } +} + +pub fn encode_key(i: u8) -> std::io::Result> { + Ok(vec![ + might_be_none(i).ok_or(std::io::ErrorKind::InvalidInput)? + ]) +} + +pub fn main() {} From 89a73281a698bd3cc29624805ccc2158573c7271 Mon Sep 17 00:00:00 2001 From: Herman Venter Date: Thu, 11 Feb 2021 12:52:07 -0800 Subject: [PATCH 4/7] Tweak replace_root to deal with more kinds of roots --- binaries/summary_store.tar | Bin 1268224 -> 1278976 bytes checker/src/abstract_value.rs | 66 +++++++++++++++++--- checker/src/callbacks.rs | 10 ++- checker/src/path.rs | 59 +++-------------- standard_contracts/src/foreign_contracts.rs | 5 ++ 5 files changed, 76 insertions(+), 64 deletions(-) diff --git a/binaries/summary_store.tar b/binaries/summary_store.tar index a72c4ee50276c78186a4fb28a02851cbbab4fd8f..cc00dffa73dcfb72e105e6a73316f543eefa3484 100644 GIT binary patch delta 15528 zcmd6O2UrzH_x_!|7w+!t-MzbesWytDh>Bp>L{Vd}DE0=Zs7UXKN>QVts9+l#mK3AL z*rJXlCK3}niW*}Qqk^$lE+9xO{LkKNOY(jB`z853Pk0_;-ZN*;%z4k5GqbZx`p(|z zv-@PvlbZT8Y1+J{tB-H<<}I6OT$?Wnwi)|5LRsi_ON$mQo4#t%W}xaVn>20W>+0Lg z$JbZw-oh8UxA66Crg8OAyH7_pvycsfUj}})@T-GgRb~sn`cIGziwseiR8>_}!B5)W zS%NJKzZ?~8@$CzCWnovhSOn2L`IjEj#A zjU4~lNN9WrSyqJCkl9yoXWD+V?JtO4y@q?s+;R8s=He7IPD5H=#mxvV#GUaw57s}% z5g@BeP8H&6gs;K|k_Ij8iEsS2;z%@(oGiqVv~fAkL-~htztEds#iu_nUos1zWn8TzZBZ;@7r`@j0$rTW{rjto-8Nz*n@eAW4c< zDQW&3e`Rr*u5HhHGVFc-)h*ddoj*N+_;ZFgOfE?`xRO(ca7Q6z-1vb*8_mFR;88>C zjCw!8ELr;)=-Ka5v<*k2@#Owv94&fW^Sgn^gPyDEHpzG7Ymix$xU=$=&!;R-g@%@D zL)@guF(jBZnaIK?I9RvEY0o8MHu5IwYUC#};?vw;@35se&;*r056g%)t1tYHKZG-;oM2|RqRe2tFRvs9`P%# zM_e5F7N|BsPjHQw+4vi=g8+ zIy(%&fv$c}dPmkB0-guJFSt z=gE&@#P%0DFJ?<~P^ij>1LUq87MLZA~*oG}@iza{_os|t{+)Hzur`26cWKTNsDWtqH|C439FC3qw$wA=w z0{TPK|K#{fQ@?TFhWmWeC&Tebm^yjhkar|mFdf_}=$AIId_rOQ^lJbaQsKq>vyQ=Q z3UDF{C4C$4iCDTEUkVI`YMQGmjmh%{d{6wvW@Q{s0HL=ktVbsIhoQ_r1%L?-^O}R3JnP#8yFdt`h59-H`Rleb3M4aO}t0pEKn!e zUHQ3m>To`n5r3A<@33VFC`=`>lf{lr2(b9tKf?}0gMX*$=g)ki?m9qKdTEl7GX5(@bZTY7HX zS-qNoVH%Pj1PRz?6s*4=cWhaLhoLYsYZO0>{Z_v^0G3=Bxjl*>&e~;{%~thEuRwkz zElJ>?B9}aN`2x07hr(52#FVCiag*Y_hcyk12n!seF2rj=eEWB#-^fEFtemU&U?9RCShb_Ip0BU&jmh5UYC?oZ;f%i^e&NafDu zj`l$0uL!D!`hzA?)Q3Oz$Kv&J4Zp~{7nDlBANh9-hr9P}X2d}#oRlZ=LF|72JKbQF zhLcgrd;)f?eRC@w4a`+1LCL%wF(>oAaL9g>*Be4Qd=fv;$c2Q=uVfzwq6li9&G%*b zRaN^Mu$9ar)IWk4pRzt=?Rd$JuFBzkc}3?V9%Uvgzx(bG7hLK96Z(1+|4|+8W?s-@Y@P);>NKB(bVGM;Y(t_MgB^Wdz=tAT z>Dab)tT^qgiuWjU!mC)x1 zZy?48{0e)!HJO@Q+l-Q{F;P{Zh@Q`t2yRTsgl`ca$;YM^}OxDRH{h&@})s0~> z>R|R%{}Vp}2`y`^<=BeVC^A4@i+SUv+H}oDe!QM@Ee0LmPK4bo2 zY@Umv=tsVW$%w1zdiOKc@hIxqRCQeLa0A*i0dH)kI<~Yyt@BpgpoNP2wDa$1#h$0+ zQs^Wre~cp?a1{N5q{ryv(CWNc52*VSg)g?`}e992|j4(gTtL~JkC<*6+>4phIw&Z!Q5k3ynBg? z8y9-IS@D^rDjx9ecRFmY4f^+p!Gv^SJLhGP(|HC5>b%^bMO@tTgGx!$^))3z{1`~-~Wq8iDJ9X@!RVg7?9VBJiJImR}Em17ZUTvty zihCv{o&q)op_o{Wrj|-pPbz(4sKCm&+bK(cl^yN8=W?8U+OICt@t9-*oN8zh0?p|zJIg0D2(MZHx1c~Cp z2nu=VDoEtPMT4Hcd)=^DC$5;se8yJdW+)&|E#4g#3B759JBD)#yPW@~5J-AX`Bs9n z4TawHZ*6p}m5+cp60?c#hQjGdUO)^l#nfwqOM0O=jUy?#XfV;cf>4jq?cIE5#?q~V z9rcm~FGhFWcEUyCyI!y(K9>zPG)58XGP)A?#v9)d?zB^d_3Qf8d_!2_079;9vso8$ z36J7vU1#A5tg9~zn^^{>Ue$$n8SK)hYd$t_gh>#yt6)#xuPIDN+|`EbL$G-h^pahK z6-Y=4w%x^+4MOo2PJQc09`ur{P*aDGm#?h_BpOj1xsoi@r;R*>?-k|D{Okj;`_*}s zWwF*QqmX4Dh=7s@f&L0D>?M8tx2WY_QX6mK7Kb0y#BRjqTokvvt1u6lzC3Vdi3Mud zv7w29fe9^|k#+loZi~{7*pXs4VFfCIP16u-r*B*nHS(W{e)^dZj3PGGb{dVAYfA=9l73u zUyL3KqsR1y(TnH7=>1^yHNypgt{f)x)tXinh1ue=1`r9(GSyJuCM3GI(4D03)>-FD zcZ?E7Xhj=uc>`N1ezm>CZKGxU3#ZpgFmMqmEm*((WlP>5k&*_H{yQhP$7YwGo%} z09^W^(1zg-nMWV6;uh;w{9QrTdsaMYgNntbDS2wv#?vo0saabMKU$(@Z9F}=8M2m} zHcY8w4M6Fi|iNA8+9>ZG2I1L)=bx zI@+R0hyE-yVz^1^rG?o19QavqS$F{JcZXr9%2y%*zU=6VLcx>a@4J8Kqb~JC*gu0e z$R=8NRhWUedONp&sjl@zBHe%jFzuS~KH^r4-*VL=q##^@xJR2d-FQRk=uJ@4rI-d@ zB(ke$MI&LV_hjeEPBD&>9On9;9HEs1O(6l|C8!?>iIEAV;gG;!O~u$=c2XM;X>I?^dvs} z#35vQckvvTzG?bsiy{r|A;Lk^)Na~!Y+eg~SM(IK5x4I8ncdjD4JFg;-r`!s=Qkc7 zsq&HxtE9+ZG|@hN#o35kz4q8#Y~BKDSNz4*i0c|(-ra%;V0*fdBmS#FJScL6p!72au zt$1FDilfg&w^VnSM7k|htghoPY#RPETdDmTO|q^i;yO)gNNY!mV-5V~KHV3ym8QNZ zanj4x){tIF5zW=vZ#Bwui0?1-)-mz14TY@udv#EJBfgW8tO16nw6?W;aalu{Y}R_Q zhK}ofdWZ&>{t5xuzDc~J<=YfKePt;ljlZ*|_vRc%n}j4Y^Fx?~6?q`L_=w?JtW7^z=_+0mJ2Yym#NC zL^oU#FKPMhE+ZP^(q||IN{Pk&4~xVfv|PjM{jkbX3IUev=(6j;2`8?))LEq}g#?-* zSF>)bLM85?^BY1K6NGd~*ba-3g63T<``H$T$CsgF|3~6wT@0P3kX%orBk5T#p44r0 zIagwZO)3Ch{c&77D|CJ=p5z$6)Lgb~Gnz~vJQi2!MAPgOt=LMb8%mk19=9Pf-D%M? z@vf6{&28RvVBPx_>yuuy-kTu~mEu28$fe&VS;}Nf9pS=9+}fIoi_m0pwyv>=o#N%> z1O84X`|BAmv#YvIn2WCfTIXrJ!p@(z_T!hxj;yM0Ji)F!+hEaa(R4543GSQv&-AK2 z4e@CVL`60*9%J8Gv5T`<^=oLnj4N_BPFFjrPqCkiCeo&n@i^PK_2V%XO9pS_6|UB> z^S^QE;KHHt&q^dA#4nONT!W;ca&?+HZIaNP3&xHyIQ^fDH4SN5O02+mD`=Z65J9r5lB4mUpG zT58d+>TSG&+oD^SR0Iy256dRB8Ui%Nc9FgfG{65pB zOns4SLE=Uecruk-h&DcCtM0yg&Vo+G7$0)SYuBic%?KI~#~RJ-&Hl$*;;#XH6=(b! ze^}7`AU=eq0)u&#K*8#G;}&+_@x~KWAsLWhJjAjaVn$eyOCq2l!{T%Cw`eN8lW2_A z8VBb4TxUyDQEGFzmqueq&PrQ1Iw!^0Rf`whY+k^Y`XeTlUYu(5)7n4W^1&(~X7Vdy zrfAR@>idpym@O?lEVGFEMDXYIZ^@AI`)h3`bxDT7<-c(R&&DA+#$OQk)v_61;*uvQ zmG)a?yvy*pxp!l6DT7iqt|aRtqcaU!YP`U3Yge!F#pWbl*6dJW+LGg3-LLH&hGzbJKD3)r_%#Vy`1m)~Lhn>Ls(pRicCF>f=HEHG!V{_wM za{Y&w7ffo}pOI|{KRxoS4K@d(G>sd{lcj2;y#kLz_r5lIBR=D+Bf;1_4cawny`qnrSE=r>!I#0x;QPS$waOM57S#5E@v?ncc6^+QH2f=@>eb0_jb_i~Ul@h| z^C1r(8Wna-ghy?B1&ngVP}q+~t@W`?w7A$<$SvOc2(JFFGHLWjv+*qAQcJzzX#5M{ zou$Tei2GnuQ6DSLex%}MJC}G{ad?G_O+%yMndKVjcdImhhq#JKm!4qrb-*4^jOP*8 zaC5{&t9|V=)qbNM-QX36YX9m3e2=8&8{MdXhSBbA!)yN^!kh7@@x|dozuW_Lt&qu} zevPF9#H~DXwT%@!`KmZ#@{TfW20y5|iF5{Wc|w+*>Uah{(M&pv*f|yNw#E5O2Kl&! zl+Qk&lJf|sLP%0tN~zp~Gr!iw=3`7cMXjX0Na*zJ>nCj42h236R(jH*i{wKqT1%sJ zc$n9+NO-x$q)(%P?WB2n_IRhxK0wJS+GdQ@1<`Ffafgn=GsAN3Ei076f23mCpXd7d zrsMYEFlHKAI7kX(S8tim$dJx3X7B{aEpWt_OJ&r%$+zD4YyD?O znzwAxtkt_P)|nHW(|_CJ;5fD8Q#~Hav?f*A(oh-@FTvxs|IPa|*^*Pt3_p#=iEQ^{ zVae`;LgJAqr7@U4;y0cx?aZ{BLANAJ&9rQO%uUKxvLd~=TxzMM*(b#WEj4;bwcj=r zwg23MHt)1;H-luvV!Qw525i*_v!wQVL2pVivL#QM_j{=`H#@S<#OH$KPP;9ZK4WmM z7!tyklrufwr&UX(>x^>iT2^(Kd81eBYC45=^;kc-LdPuHC&AX(# z3`>))E(Zd7(ZX|*tB#!am0hWiUTpHe`QG!d_&)Pboae$r_Qov4Bbb>>k4qyAJM!9G zRe?qhX-eeH(h%W}&8539CEjH1aA~k`ME0q~BSA?CY3fbT2x$nLd&cXUszq{6NF#)1 zm)sA$(I;CPY*_xIW7gzOn~BmM`sLgijjYsLhs+VrI@#N$zk&d6yn9kVLJ*ldwU+Z`i8@dtXhk0lL3H za<9Kc@~l5)xl`fuBjDdGQvJF#lC4q4`IH5v1LB)RUEPgGF|#zLIC65EG@K7Bevqd& zYm_+RyImT_e*N^uGK>DU8`4N))Z=r*UNl1htSQS@pZaj6Dx@hlrLIUAf6?_ATlSEd z-BhEoAu*YXD}8WF+OHFuH{2J-mR4u_&Q{;T_sdk;)AIY$5r!4p(@G#Pi;_liBKtob z_j~_E!e;;XMahLf%`Dl8BbeF5jgcepV(jREBbnKn+N9{FWKTY0qwtiOZznrqepjPNUpUuqXB;v~-cy|y zS?#KIvb48ykq3*){Er$s0Hd2LwQ74#D zgT=B2AHX*yEXQQdQ6Ka>ctGn>*^B->LjGK0GrN8V_j+sr-LOus1vi#@aUr7ZgO%m_ z-QA2GnYRqXp#PIF%(28l3a_#sQwxqcb2Pf}sNk_<$@W2#I|)jYJF*w2Us{i&m^oxq znjFOre%Sp1jsxVDF2}KL13Zu71ZEChl`fyOWhdM3b;2E)*(7=vblg5<`a|4?Ng?}Y z$?K&6=KI-rAQPdn4G#?q37a+sD&&AawJTQ-ZyBH0`DPNd+F+?4L7 zazmZ)RCnuV_->z>ou$z@tF^ryZS;lAX_dl)WVqtyY+n_eIW*6tEQHU6sQeeaAM#hd z&r<99|Id9Pe1B~5Vcd_&(%6Q!BHQ;W^_HHKb>vBf?9SiG9op(e6Up1Bc#`&y<+_61 z{r4W>{?I`m>f6H7gA^9ab=l6$9bT0a*Ryhe;lYAq+g@nFi&WLFs%1kyJuABjUj+sA zdEFRuMs7e>m&@*K+JfLC78Bm*z=U_u(bg}t)OYu)*4Fc~yLc(K`5+ts6JX&ry>-r3 z+uMGU-8lcfE8rX5k<2{W?mM}+4ks?}nZ=fRGFkIT&PKiC(r2;*{rU&_4#VcxEOUWC znP}u=`Ad-&=gY#|mZPD6IVkhqCMsfhR_>||uY9zS4`I=h=(>svy>nmgq2t!q+)de% z$IN`%wnV>wT?7XdPJ*!Vr9iUky0B$V%z}aHNvXX%Y%T%3^0O9yx_Z?fbpZ}oK!O``wbdp) z9b;5_>DW|+FXg3c~heip?C;0Un3-t?Zt9qvUZ51BPm@K zcj4+IX~l~sScL1mlmKB)ddWF>alvE{Rw;BVR-CDOH$`W|H+!c-1NSVR%%E)Q+gouI zlvx+o&jjXry(&@j)e?11B*lxMSC>%b-$JAf5IHEDxHXpS`S8t)C+5TEH%J5TnawZR zIJVK?M7E8PFg+Bm)I_3Bmm&%ejq^2Pf?6Ch%yJ_uZ7z{OTZy=$&8t?j)=L?{j@oa3 z2In%_WK*P)%YFN;77kc3Og8n8Qi9==t-;>#F;X(%ebLGU#AVdW?S$D~J9vnBaNnxTA#jWcFwVXJ1{Vz&G| zlb!P-!j0*qRAr$pdnsovyf@&+(D@%LCL`VRy{P+_tOQ$20COx6DASiu8Vc?&dsPc^Ue|&aWN@)Eh#m|y z6#Yvm!7nKpvWR4ihEH0<>6-IOJFPe<`0z;h6EbG;F!=kA_Qdx`c%*Ldqw=m6=j~M* zvt>UsLl@JSpOq6jcI2AX55VJ}XqCbAnURj|X1x3_@vi=B?}jcOHhjd$QGr3hqsNSe zKTwcu3eOo_l-<{poM=b6Ru z!VdJR5p$W+7bogfxY)r+ZXxl)hgTBgzp z_VHL|3H7gnN{R2f_W7KBG>jRxgl^HBy4xtpooC7L1*-m4?kxIU?yR7jYnbrAq!zjU rhTSE9q?ev@F*RwTzOBmfX|%Mz>5V@^Zqck+^A~?bOi_TT%J%;OnH*)} delta 14854 zcmd5@cUTqIwm*9~z@9y4=A4;BwSWahL=i05qJoMo_JWE9QLxex5tL%ZhJX;a8WoJW zVlT05HO874dyk2+VejPt7HqsV=R`F3-J6%E_m9i>jefti*IKjJZ>?Qs&z!UwUDLL7 z$;vQz`_}hq(71}XPoqYSeKb`X<%C#=ZboPh`q1L*+qiyti`67lv0)=$AKxlI4ZVGQ zRP%;DVD9TvAC$aR^C`$W9a$r|IJm6f(!!<6Y~ZpjK-L)P0^XIBmAxo~ztsG6(FViC zGtq|J`<3ahl3x*yj=QXoBosz7pOGXyY0rib5&=klP9jLmSH8X^5`}5p>E2ROfu3>@ zM7rTQ39xPF710(KZ=jC~NnaXwjpWg+XQUzBQ%bs-6`0>zn;VEVyGgppBzeBu3KE8f zYg|+}j?DfA$w$<)lq8V@qiPqEIB2RvmpSTc(3X2sC%pMw zlWZ~q4W~pejNm;qYg0)IsL(fx(1h0P%?CJiZti>=7tcl`H1KB~H#XEOTBE_V?kh4H zSv=VUN5{vF^fY_Lp<%;A;={*&xUnt0s0jVdzAW7r=dS$qCtO^DhJ#Bj4Y^5b+F1P3 z?r%v=y6`R8L+3jPLusWKB!K1n;aVIvMJEK|Qf=q0$Az=H_v*|1gfR9(FHGV{6YZ)W z$#CeTE1gs%*;DKzbR%6Ha4eY!!bYmlfxh(=TxqXbLICc`Jq;rL(FmGfOX!aqMeO>T z3;={YgaNM2MvED^co7<@1}v!o$0f#j#Yc`B?-ij&9%2+uAj@q8uZU5R!Es|lhK>1f zi~5xF5Q5mo4z@Ruo0!!H7vDi6z?s$( zRjjJ!&X(@3CnV9j2H`y&KMhP;2y_f&Eh+#X_W#l|1$u_FfgZvz4%b+eUxy4rBdNh( z7(~u=zu5%}a3mDq>HdOoertiJIsQU-eo~JG1!NpF&`AM;H?7oK2;iqbj++W3f^1WO z;7jvCR(aj?w-a&kOf*WRNT*UXc4TZ=NT^r1O3;AXLTCC*9r#D~7aY+?H)$Ly#F#x; zDxpqUzymK_qC+FWk@la6`LkQzfu+tCo9N!DAElsGCZJTy2mD#3xGPJ)An{iujAuTc@v;b9SBkz>8W z!b76t!b0UgOF_LFjcFq|>N-Y3!Gm5%XlQL!QjHIdj|~|+Dk{?34C$g!L4v74Z88%{ zfyh4!R~eSO=`!Rf7g?!MYcyyi%WfbX)>Z$%v-Ke)TJ0GLqo>yDwEWpNTT01P;E8H8pq0-0DQ<*|M-m-0q4;c!mOO`McAM{Gt@*Y)WXR?GDda=0A%(?hw zFbeOb(HQBzJ1`p!+%D8&8}kJY3*WhqdWcK89Mm(M>fc~*8huBq%A{3-kDy$CJHQ%Z zDJoC%Xx3wkaR1Yzs*1v?e@9(Mezh)mBq?@4;cW1J;afL8#x&vvF{J|*?g$BpKRI=M z7h;+Lc=lakJmSN8H|u4=y89}wQ@_;}3(k0;;xQ|K@*<|0pf5cV5)nVS!|gm`nguxP zv5S3-5xyjU1vE8Ut$87{TC zh{9pjFtgW|mAn$B=#|lJ^6hY`wL>{MW0-$|=%uA#Sc_#%6Bz#F>{sQ&BP>Mu`kshV zI~u`uI_V(L*~gz;x(ckBy z>OUBH$;qPMx{9hF&bbK|{9{$KeY)ci3vO3k#m{aX7cKq{xq&~is~oZozgUhU%|vYq zlxondR=QejaZO!oTWPsR_TLqeZN9w>Ddg)&1@PZSKW&m4XuvDUJqMcu0 zsKLPQ>Ss`76&?|3;b_Q~nVX1dHi~4q9d#3cBg4br)tDoh)0YslHa+IrChA{ZXU|r3 z){R11O-1K#EZDQFihq;(HnQM#-2n5?mc4nR#vI99d#D_)yj^*R#s4=wRsSy+p4~`H zOQF4HZ{1wPpUIkXoS5{RiCsCB8n4Cp7mfTlIZH0CJnBErXsfZ$@ zm}{_(h|2mI9Seb$kn$pmP>U!*OTpl?iwFi=%Z|Fvyx8EaqV_L}u_WjpUmzn~5=EkjWnIw(iy$jXu-^V$VN3y#yOy#eQ>>Lw!ovB!v)7AvPos+UIxo*%N{ zjgwXEvLqHNO}$HpsVZ(%cz(6nD=VC)%SQZ&uLm?GrfSfhl&({dv^f6ZI9#f^kD`Gl zJ9;foUxV$Lq1(hu1D||R38tidC<^wdMta&=?8tterwbME%h>^uKvz2R3D-^1(#-z) z8We2)6HE`iZN4^y-4oLYBJp~w$kAV{tJMjKolLLfhPwb?@QKukM0Fg z7DqnJ2a490S5%Z*QTMf^S1+%c^6?`qsf zy!IR;MGF82U)0Uuc)wl;?~|g1fS+F0&E)tgx?W4nm;$zEv`{ye;}2i%w)!KX#|;n) zU;JZaE-CsN#b_L9$VHuzeSb@r>nM6WsWAwbJV&uTG#UflcUP=IGb)G*O>Zh1=Hbx^kfP2g7NW?04pB_0DY|ofy~U4;Nl`}>%Qn{%n{q;&Z`4{+ z)Ctt=>0TevjtQQk8^?z#wXT@OtVvz58OQH&XfoP@C)88%8f_Yw3E*b8kN6t#+PQby znD55+HxR$zgqbORJBeu(xV57pO~GwtUvUZ&##UMe)52==-9T()yBmwska(eFs3$H7 zL~&+nCvAlp{_C}(!hl*qE4Uwd;RuB4QEVLbOP8wBDnWW%x~q>^gWYc-Zc-Gdem@Ta zUSE~-8uJIQpmXUnrhEQ9uW@E#je*|rume~Ey~m-W#svq*H>l6D=R#b3t&H>6%`L27 zh?s%+^f?JID3<~~kB5qLk+9!^jwGhFC{8UYHSR^BVmjhuGk)quN<2WV_HfZz%m3gq zrZOq14Y>1Yv4WO=)*|?K3yz8eER9PKI&H@04$wC#(snvztSGTTabhGvZp6_2B_aT-lEdac0lCG(gdMmh*x`W?T3OLfrIvE}5} zWlyukR`yEeotuxtMx<&vudynxvh?YD4Dz1Qu@*{shZDBLNQpZd%aXT=j#{3RqKB&G z8AnY&L)C2BDc0b$U7hbXrcY}Fe!NTcV~j!q~85nO8+4$Gfd|SZD45gB~>HwCSyJ zp~dgJyOIs-a0L8{6UJOxtIh@S=7ROPCpNZB1E6Bd4jmJ7wYX{5Q?M`Lqi9~X=tiq_ zGSp#PPK&aF*Lgb)2Ugp&#sy-iH7&dg)t+|@s(py7{EyG5R^bD;@#cEvk8M8CffThs zaja>vSeN4++1WQ19Q6#a^t(MxA*Odg10N9|PEYxW4s7oW@hlSh-LT%P5)=;vneIwP zwy9K|Jo?71UZsxecy{fzxDfG6Zf$p0hjToe@>X1ggetxT6U-PU6K^Eju`kNRsjvjS zUY=?eZ#^t6Lj2y=16vc*8n6oIq^}Y0e|Sp`b#TNpgH~FMghQEU4w&x(a|hZc*|DS6 z5{$9-t=|Qky-ImVe25!1;~gQixK6zc8={}{GO)~quxl~@To zrsN$1(lb%~I7^vl1;ILAr5~hgfhhUtF$%u58x$hg@f+eyYwC(*7fUm^`<%I1_fb~H zS*DS*U&TWpOMqM)H!?gpcvOS>^jdwXR!)9J9dpf=x*@Xsa{n(aD)dykWY6?o5Jqc!&7;oyM5;qRA1VkBGa~~-kX+zVlmC}vYk~6znUz&!rywWs_RxK0l zsH-nj@Z^T7&}q)tB(so#a5mCrUOJ`wNa;{xP~xZT>JGcwHE0|QY^r8zz14NdH{6iD zY6h9&=Y>?BK}_oa=Y1h9LHsXusvRY!^=KS@ItEhIzoj$_iD3nPU*eJ=lweNL=`&F7 zo%=}&gB0nt!np+x55nB-kH#f1|F)91gj*{=yFn&$*y&2rdTaW$wNitD!RI95PeVgr zN9x44*p}j=?i|N4pP>@$932)-wYT8I!&E#?nl_J^@}WH>Ov*xn_shtd#IzA50M*OB z0IKyPfHi(#{omfH1SGKKBY^;|{)cfDsb5Q=e$Z%$U3-31#|sv$4Oj7{ereAvcufRg ze&a?@*xYRZ`<78s9^$vB7#Epu!)`}Q`G^m=H|(&wKtRT0C0HPKY#6sfT>#?Qrg2gQ zt+6pZ5oE?192*v4DJ7IDb(r_P9UHPt+G52w%IjarV(}scEchd7iR;xhBA!*4B30B1 zOXH^v!KGIF(fDx;7S~NWA%A{uPh4v3hT_MU50yHsW3FVXh=;yy)C_X7gC+Kq3LrOv zp~vUu=Hme}o|==>Ioxq2DX9Z}tg=_Cq!limxsyeTUjg}c)c+V1)_@4#Cj>pEvzrBn)IX)mP%oFH`Vvy~LTMTt;_=7>XH zOTSt1^SAWNQTa(^t;?kQR{WOZ=Ps$lB(g?U`Uh70%4&zxEZD9xoz=UsbBcbfR;oYi+!9=B=ztQF)SWP-q9e<5)IV^-mG2~lLKd`a;ti>? z4K3_saHC-J*=wNTpEyr4la7!4wvs2;P!iqgr@w~pS8#0);U>}L{`xCgGCt}J-7D)I z>EhPve8g;OMscW2C3^t7z2`Y$r?|fQ?=O`eS(A>hDs_{@mLE zeId)%mjE|#=aHaLr9CL@;LGejh-^FPkBL8=-2V(e^Fb5db5@PE`3>7KhmQKYTHTRI zH~hkYk|t<0RVfhKf%WXF-(sWGY&0_%X!9s9)x|9~b;)MzTHY*nLaZIqg<$yj}e z4KD1S)c`2#%A`K}FdNo=v5XPx{)n8l{d9_y|3%S63rEjet`DWl!hs|A+4_sxQ5Tzk zYk@9v^cVSo#)^Z9389IU%g~!}%+TY0WIv$S8T$RWQDJ>X4gku^)Z5VubM+f=#aFdl z--{05r3=P+zDIU6Dhm`&jE=icegYzDX6vJ^_$P~-!n>6el+5yS^^sQO(YuyQaB+9U zB{Rnb`c_uX+LDr9phdRo+h`>Zt2ZXn6O^h)#fEv&?hEv;G--#vF80c)I-g8O$#laG z{d7|3ll+*ZgIX23X@}m04%(?7LF!Yq&lxBjW9NUO`91G(YlZ$XP@H#UT^f_MJ}Th znsh^d8UOlgZ*}cRp}{v{@;j1rJIag#ZUKtvm&KWp=WRgG)9XElSulmlcl1~JhOYv0 zaq%gX%1ZC(_gYDPbFX)Vqq#dMB~_!bq1T!#6=)k9gUpH^=vVT1+njMNf!!2(=$PJ} zK|{Mw6q5>{~;)sdR;-;WB1-*CatmsdToJ;R;?I z;GAwoG0uQ?))^3QMtv&)s(YH$fN)c3i;9M;c>38)U$alQN`^vy-|tu35Yu&(!ox&arh`4lc@N|Dk?ty>mEq6iu0?fxLvcL<-~Lo@I*JmImCZc z;Y9&4-2&Xdrr{UFC!TEYYw_Q>mg;}J$IvSld!;tm%e8v0eZ)O$h1Aaw%zyCtLS9a^ zb=F^9+1{?M2VOs%R#x^zwMl*atjPTTVrS~rIl<9?sUjEhMMd|Tf--g4;wX?X@8we{^Z;}?TD$6OJmLY z7)~Kxd~plj@~GI@SH-Wt+&YDrp!4iuKf`In_iZtI7*GfJU=UD;EB)NO6FJVM(fomi z<2WuS=QonVrPBC8h7^8S%a`yX<1m-X-V8GAK>WM4M~C8)Z@5Wpcd%ieR;;mp{!w_t z!=+AAX;`+`P=zIj8b;gVWU{_1(C{st)Yj02rV(Q)Gi)bi+-J|iwiZez{dIvy4UMW! z#&DA;n`jt=-OAGEk?GLs+Q|k78-hZEo8Y2T+~j8TL<8GObZ=EyOXo~6By;3v&w8o2 zxDVHKGCg_ArW#FMZm7xvryGzJ?s0tIU5Mx)dosq*4yi5Qu#G-^%IAlq|0ASEjeQ$7 z`2ucz`Y7-8Zx>PPFQ`hURSSVnZq?8hyj6U6W_Em}^YlVXY8 zzwLR`%?3YPF}r&5cwF>`o7!3Jxycbbv%H;#lbmQ1Q}8`5dd_`0Rimj$mtBXDw*6oz z;Ba=u2PwD|Td}6!7#dsAA*Yq2Go2CY&E#ZFi>? z#KnWTY136|Rn94JZcUHBGq^DN!XQ~Gc_-qg0LlL4Bu{0_CM&(QG;1eG{p=!Z@%LDt z{ui{1XHJ!FgixnzlsMo$=4(SgVV0fCjz2_H_|*_3d>edg9~lff#yA@Ft6_ljcJIAy zvJ>e||8pKQ4K~rL%o{ z`KnfYJK@GVTwIasmae{uj**Oh?2(=PGlv&C?R^Iv4rS|J83t>a-$L0*`xy@*E&ncQ z>3=aeBXYaAkq9mwUI&CcknL%I4>^!nJFc8gB0*T)B0S+C_aznlc6xrS8CnGOwz>0n zu^$U})CO~x4(S^|7J7MtaP;x-V?Gux2O+*TxPCN@{d9`z$o{xf#`Bw`Gw|4{j+~$u z>fQPlP5@CSZiWYK^^H$dBv6WZzuPa zu+Ok6*Ma8AY?q@v4x3vjSXE|)dfm29d){mJc~tk16+5FnbX5-1`?J8|vI$Oc`50Sb zy2s66-ABq7kp0}f-{ce1BW{L995#N~$Po!)A!CBs$v7EyBYfSF_04U}DO|pc_}kqo zg%Q(JuzeRH7s7#T_NmUqWCDCAO1_5pr!Pz4(~W0_oX8k)Gac@dPO4xfwInr)&Qj z$VtscZRS2z-fX~5ubw+Y^9r`TxBL}m@6Ib*teIi6*!t5BAlmPw7gP2X2ajdHZw?T7zK3S zRoRZdS})hd0zYdUX~reedK=^w_^0}(%SazCoL=4__t7~nyK|BB+b^y`x&d0SN$!RZMpa5AXTa~1P4XFh@-1ivDZyjhF@&sW|==GiaDz^W&5_uqiiMjW4gugKHtQJ&-&vt zqpEaBbE5-``axbHDE%&-a)Q+UP(JU^Q0M)zS~_H*oXgcJeM$DD zRYr)uDowQkCygVV##*P7O%$q#L^`T6*ES z&WU!PWFWZGGwms}k0r0b$E6C^{r~U*1-j|AT%UG#R4U?(XKM@0T0LINJ#osN9*0OT zxbK?Raxd}V%q6FB$sle{1NFHm+D~c3{NBiRTH?5Pjy*1}#m$~Wvsc+VmZ!?Fb+&S! z!?O|x_JD-kW0!Bsi?s|4AAL>@cKZ7nnDcj1Al1V!ebp#6c$80lGwtEo~+NAoQ4AXR!_e2>~9tz*YC)ZbYi)dHXk+{T(o7)GzBc{vR8f&rW2FfKX z64Z4JQU_h{xiq8>U!7LTR%}^XW2LheKiz|7Lu8nRR8eM1YD;hCy+;uKE5fU7HMfr? zK%8=@$qX`rn>)X&G6L^PYh(QfaA4EADrtHmteadwO7T?4rGBt7Ru)%H?DLfL<1#d2 zJdCGnxk>{n-c+jKe&0G-AUzM`#c-V7isN_UPD{r;ZS?i-` z;q0Uq7nrFQ#Oc=X{kp-~=*(8fE4OsY8h6uR;O@gCPlh@xzxcFAp8s%V)V2od0y8Pv z3vaA{$yFvIVV2`vFL>h1&`9t}LRZC``h9JHCx`h;HK9Xr&hqz7X=>Aun@UZ*W?SWf zWC@o^D^g_%?|n#s@BL!9Otz0IA@Dt4P)+#0U_4;Yg~~|8kFEXHKGKHE)X=K=iai~b z3unI_nrF0uy<{f6y-4ZI-$ggzBV0GIX#TZghlDrN55XI21|}70a=zlkVizkJh~T5a zaG=&h^)xYGabfODm1+n-TK-iCY#B0Xk31zxY&^8*bNu`nmu1eI>t&@fyPv20Xd~Xd zwkIAx|AouUQWF}oOR2~1uTbXM;O*?{YDiX7Mkg!JC2BTV@J!bJcNDsfIa^ugbm2C) zj`t^tTo%2yM@htiHBX!-;{grbtBf}WPF&J~Nlv0>C_l{^!d)M(L; zECscceaccC-5WjzSOUmxzp@0o*=^iU1^_y|Ul~B!t}cs&L}fum@4X`Xv#0|~q7~ok zH}A{1cpjI{Ob3<8R)iHE9*m2(a(%N|@)6}*D`oqWLw$k39_4$GOtsn{!fbe1Y4YE} zBDS#DH=FKTtFxo?3zc9V<);rKCJ%_~U7_NPa6-q5w;=j#=6YQ@Y9;n;*5NHKddJP{ zuRbR3o55G4-CsjB)w`{H$B8vNPi=;at8xA2sf%L_<*PBnJ>?;XuWfO&2Qng=#|fpg zo`K0b^hqZj|LI{*-c!(T9`)ZZ7}?x+N=qy8S;;pCaB()569m6+fS&~!+p@}>v8ff= zIMH|)mt5ld=g?*Oyemt!Hm=nwxog(DKzJL=bDeF;wK{A9%>+?U^k!k%R-Q`B6X{5?1JyK>zWD=!#Ok< z869a>Wn&-_UDiK=$CMm+Jq3F9)Y`?^8=t?zXOM8v3vn@q k_limits::MAX_EXPRESSION_SIZE { if expression_size < u64::MAX { trace!("expression {:?}", expression); - info!("expression abstracted"); + debug!("expression abstracted"); } // If the expression gets too large, refining it gets expensive and composing it // into other expressions leads to exponential growth. We therefore need to abstract @@ -484,6 +484,7 @@ pub trait AbstractValueTrait: Sized { fresh: usize, ) -> Self; fn refine_with(&self, path_condition: &Self, depth: usize) -> Self; + fn replace_embedded_path_root(&self, old_root: &Rc, new_root: Rc) -> Self; fn transmute(&self, target_type: ExpressionType) -> Self; fn try_resolve_as_byte_array(&self, _environment: &Environment) -> Option>; fn try_resolve_as_ref_to_str(&self, environment: &Environment) -> Option>; @@ -965,7 +966,7 @@ impl AbstractValueTrait for Rc { if let Some(trimmed) = self .trim_prefix_conjuncts(k_limits::MAX_EXPRESSION_SIZE - other.expression_size) { - info!("and expression prefix trimmed"); + debug!("and expression prefix trimmed"); trimmed_self = trimmed; } else { return other; @@ -1538,7 +1539,7 @@ impl AbstractValueTrait for Rc { .expression_size .saturating_add(consequent.expression_size); if condition_plus_consequent < k_limits::MAX_EXPRESSION_SIZE - 1 { - info!("alternate abstracted"); + debug!("alternate abstracted"); alternate = AbstractValue::make_from(alternate.expression.clone(), u64::MAX); expression_size = condition_plus_consequent + 1; } else { @@ -1546,7 +1547,7 @@ impl AbstractValueTrait for Rc { .expression_size .saturating_add(alternate.expression_size); if condition_plus_alternate < k_limits::MAX_EXPRESSION_SIZE - 1 { - info!("consequent abstracted"); + debug!("consequent abstracted"); consequent = AbstractValue::make_from(consequent.expression.clone(), u64::MAX); expression_size = condition_plus_alternate + 1; } else { @@ -1554,7 +1555,7 @@ impl AbstractValueTrait for Rc { .expression_size .saturating_add(alternate.expression_size); if consequent_plus_alternate < k_limits::MAX_EXPRESSION_SIZE - 1 { - info!("condition abstracted"); + debug!("condition abstracted"); condition = AbstractValue::make_from(condition.expression.clone(), u64::MAX); expression_size = consequent_plus_alternate + 1; @@ -4562,7 +4563,7 @@ impl AbstractValueTrait for Rc { //do not use false path conditions to refine things checked_precondition!(path_condition.as_bool_if_known().is_none()); if depth >= k_limits::MAX_REFINE_DEPTH { - info!("max refine depth exceeded during refine_with"); + debug!("max refine depth exceeded during refine_with"); //todo: perhaps this should go away. // right now it deals with the situation where some large expressions have sizes // that are not accurately tracked. These really should get fixed. @@ -4863,6 +4864,55 @@ impl AbstractValueTrait for Rc { } } + /// Given a left-hand expression that occurs in a Path that is in a root position, look for an embedded + /// path that is rooted in old_root and replace the path with one that is rooted in new_root. + #[logfn_inputs(TRACE)] + fn replace_embedded_path_root( + &self, + old_root: &Rc, + new_root: Rc, + ) -> Rc { + match &self.expression { + Expression::ConditionalExpression { + condition, + consequent, + alternate, + } => { + let replaced_consequent = + consequent.replace_embedded_path_root(old_root, new_root.clone()); + let replaced_alternate = alternate.replace_embedded_path_root(old_root, new_root); + condition.conditional_expression(replaced_consequent, replaced_alternate) + } + Expression::InitialParameterValue { path, var_type } => { + AbstractValue::make_initial_parameter_value( + var_type.clone(), + path.replace_root(old_root, new_root), + ) + } + Expression::Reference(path) => { + AbstractValue::make_reference(path.replace_root(old_root, new_root)) + } + Expression::Variable { path, var_type } => AbstractValue::make_typed_unknown( + var_type.clone(), + path.replace_root(old_root, new_root), + ), + Expression::WidenedJoin { path, operand } => { + operand.widen(&path.replace_root(old_root, new_root)) + } + _ => { + if self.is_top() || self.is_bottom() { + return self.clone(); + } + unimplemented!( + "replacing embedded path root of {:?}, old_root {:?}, new_root {:?}", + self, + old_root, + new_root + ); + } + } + } + /// A cast that re-interprets existing bits rather than doing conversions. /// When the source type and target types differ in length, bits are truncated /// or zero filled as appropriate. diff --git a/checker/src/callbacks.rs b/checker/src/callbacks.rs index 70d0bfa0..a4e5d445 100644 --- a/checker/src/callbacks.rs +++ b/checker/src/callbacks.rs @@ -139,15 +139,13 @@ impl MiraiCallbacks { } fn is_excluded(file_name: &str) -> bool { - file_name.contains("config/src") - || file_name.contains("config/management/src") - || file_name.contains("config/management/operational/src") - || file_name.contains("config/management/genesis/src") - || file_name.contains("consensus/safety-rules/src") + file_name.contains("consensus/safety-rules/src") || file_name.contains("crypto/crypto/src") + || file_name.contains("language/bytecode-verifier/src") // too slow || file_name.contains("language/move-lang/src") // too slow || file_name.contains("language/move-model/src") // too slow - || file_name.contains("language/move-prover/bytecode/src") // too slow + || file_name.contains("language/move-prover/bytecode/src") // too slow + || file_name.contains("language/tools/move-coverage/src") // too slow || file_name.contains("language/vm/src") // too slow || file_name.contains("network/network-address/src") || file_name.contains("secure/storage/vault/src") diff --git a/checker/src/path.rs b/checker/src/path.rs index 112b0a21..291732cf 100644 --- a/checker/src/path.rs +++ b/checker/src/path.rs @@ -1053,59 +1053,18 @@ impl PathRefinement for Rc { return new_root; } match &self.value { - PathEnum::Computed { value } => match &value.expression { - Expression::InitialParameterValue { path, .. } => { - path.replace_root(old_root, new_root) - } - Expression::Reference(path) => Path::new_computed(AbstractValue::make_reference( - path.replace_root(old_root, new_root), - )), - Expression::Variable { path, var_type } => { - Path::new_computed(AbstractValue::make_typed_unknown( - var_type.clone(), - path.replace_root(old_root, new_root), - )) - } - _ => { - if value.is_top() || value.is_bottom() { - return self.clone(); - } - unimplemented!( - "replacing root of {:?}, old_root {:?}, new_root {:?}", - self, - old_root, - new_root - ); - } - }, + PathEnum::Computed { value } => { + Path::new_computed(value.replace_embedded_path_root(old_root, new_root)) + } PathEnum::Offset { value } => { if let Expression::Offset { left, right } = &value.expression { - match &left.expression { - Expression::InitialParameterValue { path, var_type } - | Expression::Variable { path, var_type } => { - let replaced_left = AbstractValue::make_typed_unknown( - var_type.clone(), - path.replace_root(old_root, new_root), - ); - let replaced_offset = replaced_left.offset(right.clone()); - return Path::get_as_path(replaced_offset); - } - Expression::Reference(path) => { - let replaced_left = AbstractValue::make_reference( - path.replace_root(old_root, new_root), - ); - let replaced_offset = replaced_left.offset(right.clone()); - return Path::get_as_path(replaced_offset); - } - _ => {} - } + let replaced_left = left.replace_embedded_path_root(old_root, new_root); + Path::get_as_path(replaced_left.offset(right.clone())) + } else { + assume_unreachable!( + "PathEnum::Offset has value that is not Expression::Offset" + ); } - unimplemented!( - "replacing root of {:?}, old_root {:?}, new_root {:?}", - self, - old_root, - new_root - ); } PathEnum::QualifiedPath { qualifier, diff --git a/standard_contracts/src/foreign_contracts.rs b/standard_contracts/src/foreign_contracts.rs index 89dade1d..0f9876df 100644 --- a/standard_contracts/src/foreign_contracts.rs +++ b/standard_contracts/src/foreign_contracts.rs @@ -3774,6 +3774,10 @@ pub mod std { _self } } + + default_contract!(read); + default_contract!(read_to_string); + default_contract!(write); } pub mod io { @@ -3884,6 +3888,7 @@ pub mod std { } default_contract!(_join); + default_contract!(to_str); } pub mod implement_std_path_PathBuf { From 01f4f62865f3504bd7e09dc2e29acf491ce4a16a Mon Sep 17 00:00:00 2001 From: Herman Venter Date: Thu, 11 Feb 2021 15:57:07 -0800 Subject: [PATCH 5/7] Specialize opaque closures when adding closure fields --- checker/src/body_visitor.rs | 4 +++- checker/src/callbacks.rs | 5 +---- checker/src/type_visitor.rs | 7 +++++-- 3 files changed, 9 insertions(+), 7 deletions(-) diff --git a/checker/src/body_visitor.rs b/checker/src/body_visitor.rs index 6c7e4d92..6e32a129 100644 --- a/checker/src/body_visitor.rs +++ b/checker/src/body_visitor.rs @@ -1166,7 +1166,9 @@ impl<'analysis, 'compilation, 'tcx, E> BodyVisitor<'analysis, 'compilation, 'tcx } = &tpath.value { match selector.as_ref() { - PathSelector::Field(0) | PathSelector::UnionField { .. } => { + PathSelector::Field(0) + | PathSelector::Slice(..) + | PathSelector::UnionField { .. } => { // assign the pointer field of the slice pointer to the unqualified target tpath = qualifier.clone(); } diff --git a/checker/src/callbacks.rs b/checker/src/callbacks.rs index a4e5d445..2b0f755d 100644 --- a/checker/src/callbacks.rs +++ b/checker/src/callbacks.rs @@ -139,16 +139,13 @@ impl MiraiCallbacks { } fn is_excluded(file_name: &str) -> bool { - file_name.contains("consensus/safety-rules/src") - || file_name.contains("crypto/crypto/src") + file_name.contains("config/management/src") // too slow || file_name.contains("language/bytecode-verifier/src") // too slow || file_name.contains("language/move-lang/src") // too slow || file_name.contains("language/move-model/src") // too slow || file_name.contains("language/move-prover/bytecode/src") // too slow || file_name.contains("language/tools/move-coverage/src") // too slow || file_name.contains("language/vm/src") // too slow - || file_name.contains("network/network-address/src") - || file_name.contains("secure/storage/vault/src") || file_name.contains("state-synchronizer/src") // Z3 encoding error || file_name.contains("types/src") // too slow } diff --git a/checker/src/type_visitor.rs b/checker/src/type_visitor.rs index 05d44b5b..bbaddb3c 100644 --- a/checker/src/type_visitor.rs +++ b/checker/src/type_visitor.rs @@ -98,8 +98,11 @@ impl<'analysis, 'compilation, 'tcx> TypeVisitor<'tcx> { .insert_mut(closure_field_path, closure_field_val); } } - TyKind::Opaque(def_id, ..) => { - self.add_any_closure_fields_for(self.tcx.type_of(*def_id), path, first_state); + TyKind::Opaque(def_id, substs) => { + let map = self.get_generic_arguments_map(*def_id, substs, &[]); + let path_ty = + self.specialize_generic_argument_type(self.tcx.type_of(*def_id), &map); + self.add_any_closure_fields_for(path_ty, path, first_state); } TyKind::FnDef(..) | TyKind::FnPtr(..) => {} _ => { From 8e0fe645d64656a7a7256566010bec68b3085660 Mon Sep 17 00:00:00 2001 From: Herman Venter Date: Fri, 12 Feb 2021 12:03:41 -0800 Subject: [PATCH 6/7] Add transmute expression --- Cargo.lock | 22 ++++++++-------------- annotations/Cargo.toml | 2 +- annotations/README.md | 2 ++ annotations/src/lib.rs | 1 + binaries/summary_store.tar | Bin 1278976 -> 1278976 bytes checker/src/abstract_value.rs | 28 ++++++++++++++++++++++++---- checker/src/call_visitor.rs | 14 ++++++++++++++ checker/src/callbacks.rs | 7 +++---- checker/src/expression.rs | 28 +++++++++++++++++++--------- checker/src/z3_solver.rs | 16 +++++++++++++++- checker/tests/run-pass/to_bits.rs | 14 ++++++++++++++ rebuild_std.sh | 11 ++++------- 12 files changed, 105 insertions(+), 40 deletions(-) create mode 100644 checker/tests/run-pass/to_bits.rs diff --git a/Cargo.lock b/Cargo.lock index 8328b3c1..71fbf82f 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -200,7 +200,7 @@ checksum = "1d34cfa13a63ae058bfa601fe9e313bbdb3746427c1459185464ce0fcf62e1e8" dependencies = [ "cfg-if", "libc", - "redox_syscall 0.2.4", + "redox_syscall", "winapi", ] @@ -364,7 +364,7 @@ dependencies = [ [[package]] name = "mirai-annotations" -version = "1.10.1" +version = "1.11.0" [[package]] name = "mirai-standard-contracts" @@ -392,14 +392,14 @@ dependencies = [ [[package]] name = "parking_lot_core" -version = "0.8.2" +version = "0.8.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9ccb628cad4f84851442432c60ad8e1f607e29752d0bf072cbd0baf28aa34272" +checksum = "fa7a782938e745763fe6907fc6ba86946d72f49fe7e21de074e08128a99fb018" dependencies = [ "cfg-if", "instant", "libc", - "redox_syscall 0.1.57", + "redox_syscall", "smallvec", "winapi", ] @@ -421,9 +421,9 @@ dependencies = [ [[package]] name = "quote" -version = "1.0.8" +version = "1.0.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "991431c3519a3f36861882da93630ce66b52918dcf1b8e2fd66b397fc96f28df" +checksum = "c3d0b9745dc2debf507c8422de05d7226cc1f0644216dfdfead988f9b1ab32a7" dependencies = [ "proc-macro2", ] @@ -468,12 +468,6 @@ dependencies = [ "rand_core", ] -[[package]] -name = "redox_syscall" -version = "0.1.57" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "41cc0f7e4d5d4544e8861606a285bb08d3e70712ccc7d2b84d7c0ccfaf4b05ce" - [[package]] name = "redox_syscall" version = "0.2.4" @@ -658,7 +652,7 @@ dependencies = [ "cfg-if", "libc", "rand", - "redox_syscall 0.2.4", + "redox_syscall", "remove_dir_all", "winapi", ] diff --git a/annotations/Cargo.toml b/annotations/Cargo.toml index f98220fd..1b192538 100644 --- a/annotations/Cargo.toml +++ b/annotations/Cargo.toml @@ -1,7 +1,7 @@ [package] name = "mirai-annotations" -version = "1.10.1" +version = "1.11.0" authors = ["Herman Venter "] description = "Macros that provide source code annotations for MIRAI" repository = "https://github.com/facebookexperimental/MIRAI" diff --git a/annotations/README.md b/annotations/README.md index c6d55729..ceb42ca3 100644 --- a/annotations/README.md +++ b/annotations/README.md @@ -37,7 +37,9 @@ Additionally we also have: This crate also provides macros for describing and constraining abstract state that only has meaning to MIRAI. These are: * abstract_value! +* add_tag! * get_model_field! +* has_tag! * result! * set_model_field! diff --git a/annotations/src/lib.rs b/annotations/src/lib.rs index dcbe705e..c22ecfab 100644 --- a/annotations/src/lib.rs +++ b/annotations/src/lib.rs @@ -64,6 +64,7 @@ pub enum TagPropagation { Sub, SubComponent, SubOverflows, + Transmute, UninterpretedCall, } diff --git a/binaries/summary_store.tar b/binaries/summary_store.tar index cc00dffa73dcfb72e105e6a73316f543eefa3484..73a4475d46f1e97308dbb0b02a8cb247f34b257d 100644 GIT binary patch delta 28110 zcmchA2UrwI^Y<&+g6)_}puN|MR`i= ztD_F9K>fqs(nCkR$5Uyi5Rtnv(W~yY7j#q~(ITNvbKBqj(PS0b#6fDdJ}jZ{XusOfaG}TeDhJzw6Q>73Cb5@ zZ@9Zyv|Oj^7htcqHG$Btjq5Z3_$6@zB^GcPxdM6$n8h!ER{3p675j zv6%un>qV>~#6OX14>H|p4ae7ujG)m5&LJe7SGN+PP8e6BAIt;J17wCTI$7!IgJQtV zlj1_2!@qe&;Ji`f%vzYWY4|RfuuvhHS0pUe1e9ES; zi_1j;xOSs{1BXCz7UH~WStrj>X2fftWRupaydq?8c1IUR%P?;3fgYM_KF@VDNU&-OiYQa>on49r>5Ysk6@dc3?Xf9}hC^#&( zHyks&KSQ(z!2idBQT8TP$xyxZ1Qhz`z<*FAuG18XOK=d0yU5i^P?J7ihMgBhty$?( z^mac(u!Lrpc%9F;CK}L_E{Q^_3$U!-e#=2*X}X|!3xPlm!7s!PF!u(YxmI5lJ*Y0` ze_j_&5ECC?#~*;BcW?_9jv+Zz1Y`SLVW?a~Tg}?^92yphETGL@ekwiiUh)zm3q^Hc z(_J2=GX^oI>4BUc-C z6p8FvYT@}C&-NALjOuq$_}+z&#Pu8q=N^g<{H~(Po~)tsAB&cYiR`(tVUS$HxAH}& zl0b$~2i})(5TRM~yS2d1+Y&oAb}|!)c`eegO*5=1yu?UY!Ijq>e5n7$)dwm{G=0NM z2>xyy2fa(NXXn1*>L5HuY?d;5YC%SAF$wBYK4`q0aryxx;LFyT_jT1+j#ms%ur7TO zHPWD!FIiS3@PKa)q!}GlhMnSfvHBkLobUhxkbV&D{9Q%ggD&|jIwB@^FB>}rE*grt z94q2Pnjy3zc!EjOXj9lyfiP{?E(8`v;^r&@iO+p!!-NV1`MnPTP-G--$#Qh*-LMhl zi*Xq0EfTZK8_MOt{=PWnXf6PyvDlsE{dmRk1Ryc5zW6YCkFQm8@Y$wHbEZc4AM?;3n4iYkWZj>0s;6B>fO{|7-l$eYD zu^Uoe!6i!El$CvW!R!yHkHlAXgvyBi!jpz*eEz{{S}MavR#An%77d-L5EqLH-wSV) zFw#uSWiwP!*N1S~Ozf(+87&+5!=A44c9r;s=B+*lVt@0FUZ)4 zd86Bs1bw9q?%v-;<~t{s?KF+NNtV_VwDuAROrYR8=>vz`i)a0=+R8CSLuYjqwk4)PkLDu(>aLi$_(XmV*HuEoiHO z;(+QxOpHD=w+B2)60fWVs2CV~`sOh4WRlpNV37zBDV$#u^28+%Aa5cb9z`iypH@at z_J&HKN=NK4o_F;4VM`Y=vUOnhcs~00KRKBI-^TM`c$;1y4ha*)^;mCr58o$)V?4pQ zuu!ucbryID#4)jnBOtjY$t|e1X0>|&i4%F@_I);-U`*k<jxOh}tUoS%K3VwZtEc;vF$D~ZwQ0JW31%ir2HNe%6 z6vNzO;wQfg`}euimeM&<~-0OE6 z%q^;1Cd667_G{wRRn)*LqF3G!+fd34_jWj;E`oLfk~u@@J2bh{a4UN!BAF)Hf@cx$ z61iJLI>L-1zU3eG-%DiJI1gyl#ls9b7W0{aEal={czqv3*rS-AG_#H0b^`f5o-Nl? zc!y!D3$yQW^(oJtavO|-u#J??#yC)xayvD|yLV^a>r@Bc=T*l{`|Jrz?(?dn_DMD~ zY}_8qgtyDSLgWK32avgyhh8MhN(Jp32?R#4%AK-AbGff?i-B-_B(C*tJlcH)ue;&v3-DB1Th&dS>}+YvRv`Yj(;xBaFoKYzyA= zY_sQThBH)-ZAZJ!lNdR3=<|W!jcGOZ{5yL4hw8_2;?*UqSQztFTvlB;4+%*>LcU;U zSfg*>-hIRWn;0GUk(P_d0Tl86R!b3#my_Ho-6QYtCx%ct5p;}g-2l2MNUrg2y{}p_ z1al}+%7f&nsJX^7uNk?1Io=>)J6lu`$c*kWP?4j;sNx?%1qZYO?ru(fck4 z6Mb5Di-pIgWcKeWsvMFvbU|%$5{33AJimvch5mR=H7Sy;1ufR|GhE=BuFv799furR zmFRJdXEp<04Ubf>RnvAd%y`?Jr=l~niA=qOn*(VIYY*}se7@WIzZeM%7;R6oIU%|_ z^V-FV5=DF&aW^<=nogp<120i{w%PWI65IJQA}cCjApOyS>{y-HlK(*TR(hp8mVEO_ z=--jaWN_!U1f%*`ZPiZSn7&Z9HMXZ$G$eBkTfwL$PnfEiKMG=W1SZQcOn7Y!M=CIwzv#09YI$%Hia(r2Jwly@9R%V* zLq-l7mRKnhaf<7e3>Q2|?mYU6^M!3-*NP{Yn!dOS<9ULth0*f}^37ghrw&ZiU3E{< z6iVLWWU00%8Bs-iH0b>s=@_!Ki?DqsnD`Z+5M?~ao^{!a+)_o2+>HE38}b-Ml&w@g zgR}sW%dh;L9E+eZfR89^`XBUS2z4MXkna!Wfr+lLJ&;G^-MbgBfb7f@h6Ub9hnUVB z+{B03_6^`j1;PNMp-xb%3(sLVd!sRos6fat`a(fL1%jK)Gda``BDr0i`Qw+LhUj3@ z5;g?!amnmpzy1u>3Tg!N>)f;^?$Hd@2SXQg3g5{&_@uo~_DL`=o807xw~iXpm8W`t zNZt&qx{_Sd5qmTB4#>KZY}%<<_V#Tv)J51yK*o+7o)qU^DQ%cpSC$8dcy1{%Xh9Ck zUFm@6?C@)UK|%gjDJIQXb%Vx9~)Rb|=0Iee` zH&7mcdQ{y9Wex>DOvVF7|3MyW{@+TM0EXrWb^98G-f$0YgLpcB;R}zb_`@1 z___n-2~LS*@9H-2+92{XMNAuS*bO{Klh*Jdm7gXizQq^0FqPZSs-yG_0r?p0$)_=| zu4)bO@6u+r43(SUM+a{UfkK9@;*sv;f7aSERF;kOH&L(0ku(tURHPar$CBJm^qwx; zhQqe8+EJk0y=%C!WD7&U$K2yMhnIc4n)IG5yDIFgoy7ADsM_@UaX3u;E+*ek+ljN9 zY=Eme+p@esLUHZ2^1^rEP$jGJZtC7;aWgsxHLTiE9T+sgPcop*Pl|a zO0pQL1&o->fkN5!v3rR6GHQhL@$8(x3@0fM=kmIye$HL3lj=N=lOkfI5nmW88x*J- zkJ`I)YOJ6^2A_TPwJp8K@LIv53{EdvzuU6}^~d#ELvjjP6TW6}k(fG_W@Ss3l?l5* zo?K}K$Dg4FfL8}fP|PPut%>XNGRbOpNLS7MW8k%@`W@193E3PWAMa+%P(NW8ft9XB z+t!fWVqTIvD;I=oIlPDr-<#tZf)%8%p)lqrT^<)W|8hHYgG+UbsVL27j1J zxWsnkqZ%UEoXf|FS?dh1p#-5EAKPvq>w?QVt{c!`d7%#)fQ#zF>s_*1i{uo7<+^g8 zCzQP;$oe4p?vpS`AP{7&8dw{=%SdC|WIfqkT*+TG^o?!gM>SFwY;s0PnB9p{X9dff zsSu=`U?yPcXS;S`xL;q@W z2NqQztnx8d!kZ$JJzrNeHk&sSCwPQF9Oc#^VQ>P(UQ>JWS_V-szSB(h&-8tNo$ zBp^n>syQ5vM8?fa_o2aCjNoxvN`O;2*RjOZS-X9iB5qANG@#~afVU)f3!b89tlzJc#h6KeZMjUQ^-)u3Ap=?Q%^a3T2X>}3%d%S=!?_@`XP!Np^b8jf*|cZ zug3khatZzFeRZ&2lvuWsrat4yUPT9GdySs(jXaNtm7>EPVLPHspbw(B6>eJSiKh&e z9i7DcYlfzvl2F{0i|MC2EQO&GioGaHB-Ba$0*@sWcVT5u&)|O{R7!Qwk6KEyb=qMR zkD~^-c~dpugA-*8%N;qm(EiP&2O5ma9q{=cX87ntsUgXOV<6rwxfl*RWE8i(v?U~J zKGZR${Pk53#}+n^r8A7FkyS-UBP*oGyd~e23xh%g0tMt*p!RgEih3&gFSs@Ims->_ zMEo<<>@4iCr)qeg^Q$+ z=t0@BO+?3*En=kDek9DCW;|zj^@~vrm1f%BAJ48K0w{iiYJzuttf8VwS3ZR=0ih$s zUfriQOb#f(9fJjM$JjzcXU=?C`}7uV$IcRVv__1Vx0C+hcaOL5k|dT;rL4zEYe zs%j6hnrL@dN+v;_drfe}PSYJb%_L9kG#QSR3dx)mSr8ji~3q5&(r)A~IoPd2LKS(W@=fViEEu)r>DRbd?Yr<`>?@T&e<9=(} z%Zm!HDux=_LHOr6v%c=$Lm*Hye$ov7ZA0z*FDKWV^$S1v6$n4dP9hncadQv~!QjY7 zz!nFJz4J@R_Qc|Hm;4*JDYT#A))aQJ*EjHiOw);D{hI*&#Qd*U~kUgu!{{WuUKIyZqE+$iWI1j>+qUS)4fiT}YJp%#;a3P#%So_aAaC89Godqd;?_ZhVnaEjz=FRnb zfD@XYIHA#2dLxnI79kyqOm;KO)=-o~DPT|{UsE5k#}+zgAT_1x*p7YvHkfuzq9#{W zh2Fz8`-W4ECDc%5_#HG%7%G609I8GHn5Z>YdpqQStq5FGsfKWGA|ID8mrk9=Q1v(H zHN=54K968)Dm74#6_sW?$^dO)G^UEw{b1W9uKCoE+6@|^l}u6cG^!VLpUf2zJs+7I zf)$gg&TO~#&-9E#S(rBftPRv&Fn2YMc=1zsiF9Y1MzC`V70*g!9-l2D%SH%$31C$Y zWkttNrCL=vRU^uy)%EC|GpX$A;!H11XB>IMhTenW6>zx*WeG_LXH?kQoMkvK8MK&d z8g*=8htEjc5T%>CAv~>6)Nx(?<7hY|O8+|>OiAZ8~Ha=Ivsw(d`J8!$tRj=|zDjP&{4lqCyXn?rHyQ95RT*88b;5V41| zMDoX%BO|b%hY13P!tuYT7I17orGoc72jLvwd>r`frH1RZ5r=LazX*kUsc4o^&@s}C zPS{7O4RsVf8o&OdAuf%sVMxz9MCDey2U3nx>m-C%WLO=rzsTDde=qe7?6^pc)*Fph zoQ^z)ohcm0ZP#l!SdPBLAxmC64mpIQOWUt>z;YB{iZu@2J)X2ORLVdoUh5%~_ zVl;Sz)ioyEUg5B%+MBo@!ww!UfQHv7e<1R?BI4scGZF&xaSE-UW}EaMyo#w|DoY5s zKAE7i3#e^XMMNVz9#p=YEMF%K?=27rA+wz{l%{V`&#S7CbMn`>sO=JT>&~4Nv_jZh z&{Nm^lrnzZV)Len33Pl+#j>rb)%}(`+ zr);3pOT2s1>8TbnE!vJHkthR~`!nS}aO){Q<^AE;P673v;dxCzoLp7q^Ux;D9Lq3w zfM_`~hm2=D{*Oan1Ef8thOzdvSX17Rc6>o?s46-dA~$T%a{A6|>UvdGumJCSM;()( z56joIMvH|Jf?!=6KFAS!Hy@3D_-{81Mg#_o#lcBR! zRl$Nv4^bgQDT?3GC>)Q;NIdEIAmj(RE_@3^n~58N%nFUuHwa~X@kqli9*JGt%?~w! z96w|MB{qm#_PCq(^Fd27L$?YH+pW3x4AJrPOJ-DLu(U_DptB9KV=)U2@jU>`Y|t2% zu=&HhIPkLNQC<3UXGgeei{e<0kp>Oj8A1cde~H&Do9lA+5Ho7-SJNNsqPtZ^OCwX~ zb(fRn9>T~dW@YZPNjiq^?}VbOs*r=fW&_kxitJA8>Vr~*QGzBg)*d;-l$MBD?J=)$ zk_HKr(N$aouHGme;ypOGBpgOO5Wr3kv{erQI+V6K5?#Q&Q}JRN;TsvAd@tT8eUSj+ zo_L>F@0M2^wQdd1Jn@Q0A02LeU1Ny>j}o}UYft0^L9vK}Ev>ow(9<)mub}Ce!Ar+r z=Y_a07OcxuB%&F(%v)FXpbcWSYnX#(!-N+#X_Yr3t2__N5?fquMV7r3MnyB|@9d5` z(4+lO+iIhaI-)=+VSczb3E@4^HWrBu%HdydVi1k*v&Hm4?vU6Mv4`MjWMY;znug2p z8wX6;x1NYyW1^4mug(6hOa${oc}FyD7hnU$p?Jlw$J})5;TT?`0c`4p*wb$m^Rn#) zoU%s?@Vm;9C=&XIX`>l)fJ9yBa6^vmjm8OQB#H;SaITk#4Z#m z7=_eeH3}ivF#_SKa0FuasfqGc+09_i2poj;iZcxB7DDhyl%^+8ic?8<(Gjc%V#cCT z(6xY{CMSKmB!dg1@H#;+{De9+fes#BjQ~T)cNukB-)cOnQYT@b;3CTG$>;<=>pr~U zIt0x_Jy;V@&ps3h`SVZ=O9;JfdIQ2UP#8<-;CuHp!{G|@Oys7gQpYXtY(ocxeenL= zLNpBSW%8buHS_5_aG8$}PINF(=bom9qxlT)orNf%(t%OTmJ{I+kcHZ@wYi*{84icD zP%KNRb9M9++J8aSW2#0LCNIL7U8Jy2tUw@w;McMtbb}>mPIdg0c>$hAE6__R;lA1_ z1wL=WyPNu6H(7jZAk5i}7wUS#u46;TgYy=AAxKX+(rUgJ?AgMFN#f?G@)w}q%7qhR zPfGJ;Fk~xYw~Yv!UTq%2^{re75ZBL#bp+RKh&zC4_4ryT%-x1MvbEGYlaovvY)76| zU+T^IR6BzX*oDSa2P-Br(P|ofk)r$VqZ{D37RN+MnZyi?i&Z4Pu!~L9BeQs)jSNs|(1FMHf0!Pnqb07)`o+!h;6(^`yfuYe^F5I9gEnlSJ&FDCRjgDd7 zLuLv*%eg!{_?4cHcbMYv4wJSD%wPn!&vA*1EH7cuNwRdCu&;K{I(UqRvuYkP=va&ecb-~@H;S}h>z|q_uPr2pBAC^Rc*b7IJf#*7rONWbhxT2H~>35 zMqV<){6#ZwNGnI7tkF+x{BVB!7M~2Veki#ehmQsN;bVd09}s?%(L^GH?Qc1#(3W0j z2jOFZe)w1bGnhincl^w5*n)n7=k9(2sQ(ewgGKK+F~aV)!x$)hhu9-!>c*+~*Vy4P zZ_-EP07>sTUgWVt@=0$)@<(I?Meq46BcKC{sI93HghGebkG-6?SsO-rzIU_XzHTNUGTW=kH_sQQ>g}88%vmV zo%SltfP8~-FxObZZc!3tF1PE0NG|cyb5Mi7bvTJ8U}^ZQk~9bV5Pl+`cr)AtKFKBe zw?Z_O{jRBPF$|bDMlCUiMGF4PgDG0~5DFC>FJYd&Jq^N?5^nK6cEywT@Ioo+%i1<$ zmzOb}qLN&#GOk45acL*$a1%*-RaJ1_+oZN6S%ya6C|`-!0P*;)$fP&MHGy=KIO)wr zvQr^WcohkK5Tn?4qAC&e?{N%bW5kXlbdfy|j#xp3CmUC_f>lEh*bl3Jb%CC(CWmQY{w*DMHg zk+4VTGLQGENn~lJFhLt)^TtR`>H98{h^hjlA!d%;aFPyeD0xs-6&%JB8%bu#h(3MW zW`NX3!j4m7;da4mNcNGin-A2PZ7Jp$mIQo)=O=Lmi#8k}RGt!=<4(XuJN+b0A%`zQ zgJNHA#S7pBK?5l0B~dSGBdG!TaS}1q@#W;v!~-qr;jM-QfiusP<;$OB*-pEi28F&7 zUl!kKGxpSkfVPtMETQGv-05(nt%QrpGfeN-qFeY$psM(2h@S0crqg#iNUD6q!a=+( zK(azcIQ-i!1A@XNgY-tD8g6%r@giaXUPQz=D%--{D2WJ~g>$$NwcN(8gw$|e;@y`^ z3-LN(0JF$*RQf`6Z;6dw8)cB*(;ZF4Wl%6)(i*?)%ju!iaaXSDigrfhqOlR$BJF5+ zdG8T)ij;W3*9Zxhw#13XiWn-pKB4Y*zN5lH8|%)SAaQ_ik(_Q~y;tKxxq)bMXrrtaSaq}dt_3lLsSV`gUtIU&d$8~3(6LH|5!3VuP!%K=8 zf)!lN;M|g~l_~L&6YlF8ThNg?lIx;hZlOj3hVjkF4+dGnu7g1SnRJDue~oRxc%$UT zuPXuTwUPh`Y9wn8J61`e;oAy{jPAKYVrZZ($?{f9!FrLTp02cHJ1%XwkS&Fz!&03b z-Ef!Wwl@*5Kk5W6FO{tLQ8P5gYg@PcN`4UC5)K;7+!o0DSJsv;`zT4JD%q`}3khkg zjcm=dC5U{tMmVG!!@RSHu?8}{q>l75duiYg>!I(~mkxF!a{juonGWhHy=7QgJt!ii z9hh%c_Fgm{zu=fLPD(9Wia(IBW1Q5EA%}qXWMh2wYq7KsB(;{MFdXE3Ycm}Kri4Jo zbqN7WyGzZ%wXaBj2E{o_jVS48C!+DX;%qu&rnIJhuxfPG<}B7JBw*zkDL(zZCo|FM z#RVY{LCB0*-ph#Pp^w()`~JDjMTs0|pe4AMg%9 zw_!}rWY$pz!V&}7BNoCVQdt}xeIYdVg-4BLAxjI*$+8~8;aWQ;?Zty2dy7m(V>{aa ze(m&pPuZ=x#H&1MHl2J?=1|!kej%=E=-vggh0SCMH*Y&IW{uLCmE2LGfr+-pDsb?| z|EJhzY(xi8#;#Q`&|7A_#$EQ0kNpU;EKE3BtG?hWZgoJYv5Lm(JN=eY8gF^3X3DY~ zkL*XjT`wG~)#oF{<}P`H_4U7KyqM4-{|k-hM)=9A#zkJTY4H!fkY!th&MJLEb6c0~6GG!>x95XNZmy=?}&#H(x`<#GY+N z3p>jX>6=s0G90RU!;rC9p0}0_RY9N_tS0Er-Q?|R6FVoj`Ga0ONZx?Kn8^<47s>K` zHXzDwbhwj8zC9vL885(Z$729(A=Ou9Pd6Vf_hy;2=Kr8YG&W(Z-X-vN=Elg+)Fv9- zD;LsB7sv-xHBZtIZo8t6)5^v29L|m_OXc;!x>(r)mL@8iL3Ebfqyl^z8ke85CVE@H z-cK((B=7s%RcnZsc~<-Ab4TT?rEDw+zbNlQ7hRAmEbvDvSD4ae|H_5G<^I}bHGSZj zynStXkN$NYef#!G`=act$*=K?vWj)Rhyfz=?(~5u#kDHv4T@8gSfc0SmTxBC`D859K#c9K{j3S;JcxbI#ZDZNq;G@m&{Z+fMP%U z7faiz$BpheOL1LAOt5I|2(HT%-zw?(nFY*7ge-fWbrD(WXV7{o^L3|5wUplAy;70= z+lq9SviAAYZmSg?%!tna__l!Y2Nn5xdl{}@Yng0=!~A9VW2*+8rZJyR!0$+Uz`i4j zUcYNtWe_xU#Bs$JGvbufp)GXe-wOH{oL3_=vR!?TENy1cdAjzkwyUbbN4}|%g_w+dNtQ+$OrOCRGRaO=3sV197{R5l z3QHQ^DaLVQ_@_AQtIz$YP}d|Dx~1--56hK(D#M{|h2GV^!?E(m&}9On!1-jUxj~ni z%)7qH#%gbPQA4Re2Cppoi%-lg5qhtwvbYA3KI)qomex};8-F$(m51<;a)^>y_!l%( z_QXFshbZe455^z352G6>Lw?8=n=vdI!d!pC<+*cN3AA$8D*xX#UNbtE3O0?E%$Dl^ z=DK>h&lwOmRWhe;|C`IE)G-QPH~XJRvF*AmUXWnKXFz@Kpawfx~S_%KKr z{zJPme4X~fy&*qwxy#OiMQ|}$$sGIrXWwYs*k|t_1K{AWpXjnOG#CMEM=0ZdsOzZw z^D$U7O355W{_h&|!F)8NjZr@SUtB-&nIE|*;rsl>PWsjqr4bY9{?mq^X#YR=y8qwx zX}$cP1MC~In!{MJjO6H8#W|Be;skBlBjrS_s6TUvp&(Rb2Du-}0iZ&tCXVDBZ zjhQzY5hK5N_oW*gQGP{O36oLilE&lPl{F#yy~0tKyf7&xUGtpsc}=S8_Vf*8*$jhp z-K*I}HIWE*w8V*Yy+Z6{Iwkr!LW6e%bgAexz4Gs-opZfM9V1J_4Q8e@UpUM(R=0+W z_mwNZQ}T;*VdY%QpT7P`=~PqpWM;2avMj=24t~2?1WDeiCbaiwWpg$UuWS%nH1L=Y zS?XwzJ_j;4;*A!zb&7>)s`Bs5V%ydN6xJ#Sh`x;@vulxr#P8$CC_2MH1*U}If~f`I zQd@QVJ6Tr3RwsM-w$ipjivFKdtcGYb_-Zs*)KL}c!PLqAeNSoz(UvOx#hd?@)w0qr ztyF<(Vrs%=L)xp6%IAlmnA`$4fxYJp>zu`W;p~&8R&rZwU5qL z4LZLr;~`mg+o0D1-D@5bjnq9VyR`(A~H1M}pGqb9>joKXH zmx=`fWBkt*5*wtLSw-gD`;`1X-({VS|m@9v9l&QsOr_8>p2P{w6_g zt9JdKKtk$Zr2>Z8sx?GO=WYsEW~*jyMOoBUo5K+oHM7->|7L2$KX|K!;m)p$xuy3; zK4!SxV7wE4m*HDoHM2F6VOQDO9rd)bm>fzt2Y8Qx=XP5C12tIxy!u-G_-{r({?Y4y zrosBRwFz~GRt{LdpS>EN(`LOkuZRQl2;1$M7O{Vl5VTu~zd7Zgu0`zdo1$W*nYJ8u zsB9B{X6nN~`ubj-RZ8K@ZY2rPmvHDjewv_+V=j$4N4}3USQw6P%HuEkS*xAkm7lsR z{lrmyg&9j#(F&dov?%=)U6%0&aI!2vMUrK#l2fq4Kk!13yQ*hmK(tp9&P|>bOXs<& zBPtJo%A@s1Pxvb(T8w_HyJUCuzHG+K0Hue14l-hku)U2->k{lH%xt!VaDK^(}ly;AqGT9&afSHvr*VI b%;_~+-I=KHA7pFXg#FL1(ZccSZ=(MP_cn5e delta 28104 zcmchA2UHZ<^7jlhGu?M)n4|6F`U;q^nBdBW*AVMi7bj=Ad zwOKK)8FbAGnDZLIfTDi4XQsQs^VU`PpYNUH8@g^)-KyWMTQ_!Z^2|=jGdrcuQ#5pM z(6Dh+Yj=;vjhi+QST|0OG>Y0O6wVd$B~6+%ZOD}v>Pwn7H?2g2hJ6GGn+F(&*p&O)(6KPPRzh@?)F#-dD8lmNa$!n{s2fYTPX1{H@m)lAVBbY#!&2v5*l>=a`mqG{l<;gF8_|_#d($@R zsg63T0@eK4*Ec%qeV$4?g^C&&6S9=B?{we(qD-MqbKBqj(WDpKL_vO$aX46y5xu8( z4HV^yh|g{(_UfvfH=H*wq;R|nf<}nygW(8~HS3Chy1z3+?Z^_wQLe!{wpThfWie@Q zIK8L@w#H%E{&Bp=1s2nIkVGpT`Z2tAFt-9VqS?9iI%;_Z>g<-ddi0Z+EMZCYw>$P0WP}#^dF3g%>hJpl* z1)_nGqX&Vot;B}a;GW{#2R>(rnzMxUcRu%q@JycI+xBib9L*FpWjQ{!sWBXEfF~@g zNf;kr6c9zy*Y4<*=f&s3XReh=B#bMS$$G?S{Yg^kI?U z(Td_S-Umn9`cQA9s2*#fZ!{#qq>Umcmauc#oNOrI2{MYD-BqtFvOfsVbLmsoeejIo zC=gd~6f<-L#HS-Jtb(Q$rZYWW18+8QW)Z0dJ(oet&3s*3MyAw*1)FgK)Q(q`+wvEl zG&0qC`$puu4}!)`nee%HO6&vi+eBTfsE=!WRj#Osn2>~)B}3p|9xT;_L>jX9it6jZ zk}tmT&4WW=U<1e-#YHx;d3VcH2-wGa``Kc4TUfSF@3#{(CkF#Sia00risPOkXKL_*&CjViG+LSL}s8lr^TV*pxEAU&)_W#(Ha2%AB%;i z)qqTLLh@co}G8v5_6qDf++ ze(O0S;qYDTK}HhEp;E9rgzu~=XIZZvCA=H6S zZ#alhkMQm9aOk$cVU1(V1R~#xG^}fvZ`~I$5>{~OEe9XkW9T!oqC}H-yhMS?^&IF^ zf&+W)JFX7m`F{V?j2?4HttBQwUBagfFMoSCMxYH_r^3TGm*W+~GptKrL>VX7xImT` z3q0Yw18GJFm*SZCU95ftJ!9m7FCZ-w<^HasA3>Ltiw=p2{#}>&!+Aq7H^rJO8}t{n zBzVHQBzz^s=8!{*?N~P1ar3_zD%(fMWS@iQQ6z4n+^%9ZjHkq0>fbSN zr5#+L#7$V)6%X$^g9{R0))6WL`U_7QLij-4l9tM_kyTWouSG+rDa7~0#6m)O3&xm< zxyj58w_I1aXeM^o+l>68U$jF}0#8952&s)B^fMQ;y#<{)_N8~lvRqx++jThKi^lKH ztR-fvBVyM-F`$Rn5=Z^E;XlT2m(;b5AlOQLy1EEN+lmcI;^E;Aui>?`*b3&<6SEzU z5N>txVW@TBT|Mo<#;ml7mJgNtA5PkT~%5*&Rr6=5exY?7f7k*h`N;@x|Vusm_uF7v7RnBWj;#Eb(F4#4sGF;@+LEOO0xwA2 zh07WGuHwJYa5S#~Om#);1hA}8Ry z;1SB_$mi4A--OAbe01(UwDB1{59OmX$RVXBv<(wCWaD@5yP(;yDvam2mREEEzEt3d zgupY5X_hdi8*f!Y#?nO$m20`7H#Th2v9;^Yv%Qp>Z-vzE92?c{tMC+AdQIT19a%FQ zP!ig@huEpw4fk}^ZeQ}}v1M}}YtqXzScd_TSJ3>+HFAwo=6n_h%@ zLoi#LAv{~G@@P6k=Yc~3C6~XQ{7M} zftNrWIUqIx;#-j14&sD9YuzArGB2FDwIjut!nKL%lZjm*Eg3gm`((aNYHe8J!B9Ci z<4v80>ex(Ec(zk?Mh!YLMclbM4U_y;{K4?U?WW*5U7T6HcG1wPS>iuQBE-mJ3s^72 z&|XX9t@RT>e#=m~0l?qiV4;p}%|f27@$qfh@XtctcbmMVuMEKwMyK;^&hwYAfWzr5 zo4w)tFgJ#)4zyV$wqYAL+Le_qyOg(>jhMpxJs3L2_+rd*Kho*%gY99*w=i7kh8Q!wt28A8wq+&Rxq`RvU(G z;78+HttJg(4B^_?*lS~BhENB5HgZ)H$GTierRQv{enydHJuFHj-@OsEX)6%af`Wg< ztzhXkaY%LJxJ9n`K1pOha{3Fb_w(LFCR^mf>-{(s*Y4-NNtkl(B}3(U>(~o!3v_G= z2Y5Eco+qv0$N`QGWxTz+2d_=r;??Zi`IIRfJ%TX~ILKpMr_3;%k+6jA2RS{+*mUaf ziejdRv`J04QDiTBo*0DpyL<&kqXs3!fX!r1ipaN`I|ue1!sDdw?1?aXk=zrchsE4h z@wssB=bKAA;|RYJj^RDTet+ z#Ls>g_a7%uOKy!@N4|R~XzM2s)P`Ik)e>5qVArFSr$oR0q@gdK5*tv&_3WmHps*OP z0p4HY`;KM9gV(@2pYxKq_4-Poj%{x~$0pmd-}oT;Zl|D~c6Oi)CtE>4fw<@II?S!A zEW4*aft)Mi)m7BMDxz0j6WdVAB$uxDQD;Fr0m+;pM30QG)ZaAC9vx>~vV~T~d`OJ$ zPp80)V%~GdL}50=#znyWWK5hC0Net`m*RF5dH-;BT|6ys&+JFk1nUocUY%Tf{5XjFz-OY7p)1W9 zLLDgmz#&Zd5NjVo>yI23#G}W@YlHj~W=rVC#WE4yV59{@a{5vpmwV{6*yOm>a`00KUol{o*Tu$72_%sWWzKKh#i{=3#=|{+~jX?1I z`^WG2f0Orp|4z$AGKAXj zMvVv3YYLLxB_M*=NUnpGlH>-x(zM4jb-eNEJWlKG%x1XifJDV_7?%|qywI`6sYrHr zj0kwv?3s@D7SAiY>GRZ)EIlU-&<1wob!^M>I;0cik0)zDaszDDEH!!WcftE11ryy( z*JQy{Q*!C=Dyp22HFQBOGKE4>>*P+TpD+L~sZt_Hb7;PvAK#V@&2@moc3R+=jXi43 zjnO=>8MM*xK+PN;GmhcKd*(b9nfg8HrI+wK}2)TH)3?a*oLsNImzw7 zW)4!vfKdyc5cWL&AVlg2%oM|Lo$4eUs=#p8HYE(qJvj-5`Qt?{sFToNARabi%&<|h zm8Kz|Ht*jL=R8U7Fxv8wV>H;c!KIArHUH4;rK6K@(4v}g5O!goIsMB zTrGNhu09k6^7&-shMuJip$ zv~(unk1Y(<3TlM#i`-tH3pO)U9}HdO349+X0nOFPJ`3Sxvp+}7(NROY@YJ*>3;V&U zE+jYO*kLxn1Y})FcFw5?YF@J(bryCMkORhyj*DtgY0l8|ID-Ea?K=&Zysu6+A&JsPQH+hGWtq2))69r@3D2yA#hm!2p zKe5x~qz!C~=KP}WIIO8bmOc~)G1Gc8$evCj+9if;R-K&2EQV#&nF*iBcVC1Zf*1$i z`ctjIDVFS04F{QBG5X3dvYaA9cN8y%R%1zPC`;ytiEYiF|HDwZ-K_J4g)2dxgd_PR z=G9fLA)18!{fwb6J5JQwh?DZxF)kfoP}owQ?ko&i;hUOyhEiQmQK$5A^X z`&c*VoJ^kmT}3~R+5@MOrik)3-*pKM5Oxwk+yp#mXV2q2AbcKP9Rn*C;K>I$pXBa7 zh17Z4gP~eL!h8-C>iyQ!t|*#OBV33_=lo@Oj`C$qk>M~=3fjfUW&y6|>~%sf+0 zAz03rOXmlO>XIM72!jOzLHeqpwZOZSG^S0~lVRdY0jr^}Z6iOc(NW8QdngXGJ2CpK zV0lv&f(ggD3W;U(=9&Y~kc_oVE1(8<(G2T>ys@Bztv^y6>A|hQfse z4#s>OjO$MD+IIZ?{UE$PK{jHA)0!{p4>>1E6BuxkAL$0vZ2gX*a&>q!=NpMYxN=DXtRw&M9&;NhDlI+(*y3MBX>3dZXb!o(uZWOQdrL_BUYLSV}nWC7XbqzGJitBATUhqQ(k#r$mH zPt$8Akf|eR_0E5F3*Hrz?BTlN(eYX^;z48p0M#A7c|7N zq`L{U@IEQ~?H-_ zA5q-$winpgFjTf{5>6JycR(efxa$_(C7VNFq=aJc$P#-m4`>2UB@}m8C3^7=XXqiN z{B?$Es9XJG644->GQh)|ssUwAlrb!KuChz6#>R{;xCWRAXvPRngJNHcaU`k^J~x7#u1PC?L-QwWkND zsOO^p1-FL&YEHdCgyhf{DQvf=YJsAWN&&BWXcx(+7z`b{Lr*V+(HeIP+yK|18Hd;0eMoJS=GS+0Y6n>h~{7 zan{}{cqXBHJ5#f&+Cr=*x`8_-lc1HE%OBvN3By5?(h3Jnsv{+XA)XXFnMOSt-Ry*? zCSmw?Ye<~R1iX4tB;4hrik#WgbsmZphJlSSh4=KlsmiUCa^-0*gtx{GxU(h2t`@0B z51ze5L$Ov!@xoFzttj?V5Ah^VVWAVqXvGV7dYbI#1neutL5SthVn%@VjOw_@w3y?q z33t4HFzK|X{Vm$di|Sof3^lR^hh1titLw0C0)d)|lcw;*m)i5cf?RLbFZ|$_AN(jg ziR4J%M(a>021k|vTO26%vM+IG{2UV)5khgJ^O>}R3!or`i$ruZ$Mh2FE9{0BBW~R= zuIUPiEgSfu2cA%{wF?eD{rutTcsx?p>`HMf3A?vubzyQ>s->O-`GsZ7M^msmPblh! z7jK$S{vvmL<4!GLL?|_oRTon-vNSV{iejJ7%!_#j^TW7)MZAa}n@SsWqb5}ub|P)f zjZk`C&#Jc^ZUq{@DiID7{$Q?iqY#OB7aE2c>~#$FhT%-neJIC3oE;b48v=)LDV+FrwW$dl9zun&Ak7}< z*$Z05a#o-SpF3`NI@29bXS9`Gi>0_F$P%~rV;N>^D9)x7Ff5j@$=vaqKb<|4np$;i zJD(J8pxxuBDOFXWk8sVN(NrS|^=IK;6EsTLLjZ5GDHj+rS!=BJX2_Vl3*eqixxxL( zd|tL{Ij|E$)nA?05QC`IF0eJ38mh;N>h)^T8MKAbm@LA3c-vAq_o>5IFML8PnWFeV zsGblug)1VaJH3yC6;r5AY_sl(D9l0Wm^Tot4b)yRe>Ki{gQoHl;g61eg50UpAXeh} z>(2Md(ga~o0j$cVtmr}0sFqcpsu4#69$uw$XHrY6i!+@ymkH#gfk)QDYvAS@)TJKj zd3Z*Jt<7GB=Ox1ybFNXtdu?utw2mk})Nb&+LebK}7bR#kBjxR(c7>QFS}BkE5_`iI zqT7(Ogc{D`;c6UWg%)AfAQ<7HZUIFH@kApli>n3&+5FW8Ex-)^ki3-gf)~pv3eGOo zGH55fo7Vpcl-LM&HC(yZ3a&2@O&2_SPp2)TzE%|}4Kek!$qagFHZ``Y z?ZpN)9l4eYlc2aZE4$-B>m}#`%44V#EU2eOAV18xPK@r{n}Wz(oaA&_7EMT8c@3?_ z5)q69u4 zL(yE!0Il~@?I3&?XNknTLBwGk=e-1hBjM-`syQ6lOR3-!&p~`ye|tOl?50NRwGl&V z)D=U~ZmJ(k*c83AoF2S~QXA?hdNh9hM?-uHdGMK@b%0u1?G~7Dlv*bt{z=<+4eZbJ zHtus7&>Xg(r^f1yMxD_i0~}1fao%>nf|KRg3moFa{=s`@K>h_T@`yXFYn+Bx`53#L zi`t=)c_D;qDDXyrH3Tynyus=UlWs3@*ixA{uZ+e4-dg}}SEv9W^0^|SzRQ>65R{Ln z(E4Ha;f8rbm>Q1%sBKk6L?e5jWYB?pzfRb@k3b-Vw06=SG<}VFSyhEh zdon$pes`PNCP7Hmnno*xeFWWg?oTM?*DY^aUAqe%o>Bu?Z~n?^RtDFfQiEAS!lOVF z81jsot|y>cOYkgWBvw}+(q2+F(D5I7BVf`Pt+MG6_*DvF zM`cCPci&Q1tExiZVKjR_Qb#1nv5WV6v{)D}2+{daCP(bOe6+D1u^599j=?CHEAfTR zhKSpNy*usrW%y!}BH8x7R*)jX>0ckSV=vA+1Xf}^RIow3O4An(i;?~wfQIncc%hu` zNutuKLZTsV{Q1Wwx|a-{uBr+aReFR98A{Q<$@!_cQ%2xX#|I%lSX-a>aMq`XpFn1X z#_JtIJ`HYo;~0;?G4A1q8bh`pvVb=>h+FqO`1_C9C<`-mt-z3D&AnoXlt$wMD>7Kx zBXj6vgX~z$W-ZMg3CnCy5=$7@WM~d}+487%)O1OKLR%EYa;(2_zKkKbLjFH^(XzQN zXAe={V&X^ob6r$eRkSoR`=_fvkncT(5q+7Zxz8qP5~*xW)!zHUJbol;eBF#TpE_&eGe~M;WdvwKOhh9s~GXVf(G!m6>@^$0f>Sv zt-1P;Cv}%V(=mgWj=|0gabGJ)j3~)QGjN%=uI!;N;x=p~?Hu3IDsMzqc_@@cD4L%n zOaBq}?Z@Ds8;1Ppv3{s+wed$CP>_^3JL<@B=-mx%W1&bYgeG`y&=22ci|mFPKx}u! zo`R$GYvNv@KX4g-;eaXo-W{>aOjN(AyU!10B3Rgi55-fna-PGz9(d8O2mMt4zMFUn zSJ>1OvB%$NyUlt5p0)QA;5U^cPy`I@#U(VV){Mp{u)Y28oHGIq0=wQ^GZ9HEL`5*H zHy$_iE!}9@@mQMbgQQi*->+Z1EBW3_*e{a7Kfb-xmmU_0mR1}8ZZT+*6n*;pG(u^@ zNI?f!H5U1R)hI5j6U#lC7(@Ihe1M?$rfZFW?qD<;`Lcu?i$-Qa{Aheop~v)%>zgUK z^&)ZW6(k}xSS2C^+Y^uioD&ecRZZ9pA6pLd5^x^UEA}~mv<8HXL38v3Do>JL6CJ{O zAaWc^gf0dAP#N6F^%R^-#A^k;@IrfG79BFSia92)7~lF|`fkVimJ?A`8;Q#)v!|eA zQsUsKj+PL-0Ci(6tl`%q1M(N3NR}{5U0Mfvr=nggVaeQ9#ter$$kULAo=PbTT1TUO z!v1)RE(48%`)Pcn`L?IpLj8sK;6#T4Wu_UBiWV}wcQa66r4ys=18htWtzyjIr}2E?W9fqGl;jUYW?Xi0o2?ApTRNkY`f#2(aJxpYEA z@4Vd|Mr=jw&Jpn@bCoMx-O4opK^W~z0rzc)Ie^l>H|*fv4CZe`9oS0xKa0+w4RTPc zsxS8TUVb&04%~r~stuKzMqj0scu2H`!XD7?p{tpYO`!JRYQ%tf}p-3AA;WScNryK5biB&|iy`U@piy=A&Q zeH=l{&ZCT~s^Id%n@h+{M%e7>yb`2$xtTE9oPDzdAE!p+<5cXD9c;PFc|(-O-p_^4 zcM-e8OqHF>ABB@%v;g1jMtDcHkb{PpdR_AY_7-a6R-4Zf#x??V5#qL7KfJjc0SQHX zhaXmQqX!riqb_U{XVwA}m{iQCcAuqY$@KGL)V`|DYl!kWc6;d757EJ@s^IYRe~P?h z#97K$ROtfhZLHaX}1oa z3&h}a0nA_uH9zv>`sELyws_=@5rE5Q`iR&AWlAiW(*nmk=8gM| z93bu!$BUkaJayOG5dRt3K=CJj4iay@${O6t@C6`!Uo3vO?KZu!437*tir(X2|Ix@o zW?sr7OZEw41_}fO*vyx>)4^X+wN46|RJZ$-BtVA3db&)*-F6`EwyR8~8fa}S;TCoW ztnO`x`Nk4NKZXZWK@afTB3>L}rkY6tkVstNs^xW+(t zUXIAc`$>bC{Um3JJtR9zD3H}-RpL)z*d;-?dXhL6vOhYT42L)MB;3JD`EyTS=v80B z9-+&;ulwPzcccjiYZGiMnv1UCUL%Jq{pfo#4A z9o(Xd!OP#l0#_*LDN$$oN@_rUltc`5+Hmq{+n8HV@J7R6K|P)+y$yemRno!B8;aUU z+OT+s`gbpcz_yb1Ea63LyC68!R>I}v@@Dp5>E?bCs46@fqW_4=3G`imNtI7nIE1$a zN><2-502Y=LvSz2Ful>}>rXlsa@JGNy& z!WaoR#-9|g=nB`z@F}52YUxa9k;sc|N_id)D-$K`&H+Kq4fzD$5+&T7m}KW?bD;lN zPAS!3!#WF`m1FS=WE{@Q56AMLEpq zFPHbyPm}n_iRkG0WpqTgvOwMwSzEgFvm}|SWVVJbBBTRs zWH)SL^2m>W3P*Hhm~*=sYarE2>PRoMmj?Z7HQHOlg)Y+JPJ~mf-i_$s?$X#>Ub%YnT5ZNuzkGLjv~4omHc&HhZy7Apt8-Nk!m(UuL4y ziwi;_oRCT3{6wir$Ba>y!lf)(9Ako3f`lR$Sq;4<`ci)=ekGOCTjxrb8|ggN7|(GL z`r-)56UN0e;1!t50_f8VrBEd(Xbi<_OJdv<&n5JwJyH>=uZ7r~H0C0FKP)|~C;WeK z@hE}A6N8kakvZe@S%ozOAC_8Fpl#nP?ZUL86oM6%Sa_P2rT8kIJ@N{)kGMcZcRVX4 z8p@6o+14XVKL|&KXfJO)m1$sJEtv{tG?yvha4VUZ-t<+P|Jyl5W1Kb5U@KXMSN~l{ zF)fo;M;Qc53}lZngv@s#;ILFS0C&Dn8pp!pMzV2{qTOU^H{ocl9VxqUCs?{grlPSO z?SH>^dSNTs?fFDri>r<4`13M{%Hi+}X;nk_DUf9}m9=*^n#Guvs5L9TgF*w7ZH-mn z;En%JvB%hm4y26Tt6-qF%=pg+veNzEZ&Xso{DZz-kmwN}+k z+3rg@e~};73&&~o`AD(3OP*nU1J4^TCUn933(j*r{P<<#VlSD2*QDiS=@#L5ty19? zxgGttO5WlZFx3$1ndh3(fu?d~R;hLkxF^c%LUIkcH50?yujyLR$?o#5W-`lO>tf0G z9>NK1b+*vv23dnP36QgsIjwjbUNSw^6fqjxqz8LX;2xNy)(394lh=cOQ6l}ZSY`J$ z#E8M8y3)c<@&kHzDq4n9RUa5J4$Je_vZ*Q<6vNd7-Knd*T`j`v#gkE+)9{t-@Yl!?e-~OV{9G0(^vgx$L@xZT@YjBN zn%?(9-oBPRx_MFV_wTQ@@5pAsJN%BUVqH(7?bl;p=zV<^SE`^lI7;!x5&g8p% zgQ+dxVnh6~ila6vdzd>_p+7>c99X~bq#-`6%D)b>>57Lx^o``1ia3b7p}=7>Q{e!L zz3g8sEmsd5-F=qgs)`7H@@hJ`FH?N4q~}*mkV#H^4J1qa3|dcPzU-7@uJi`)m5Qam ztw?7nYhM8Ev0CA8Mu^qpON8_)o8g%@F`Dy}wL(&uW98&cB zUBfDaprON$D!!T#Z6?{Arz37E=wFCljqJuOt9fKeQ-e;^wePfDRyBh~cNDXJVv6R! z9d&@@EQKvSxkz!o2636b*Msg{sz5&rPK|86^W(Z?Nrb`l8H^z*b}Dm7zNs*R3*Qu$ zG<;Ny=Q{C!;;gTJ?PrC$CNc1~^%?r0T-m=e99l2*q4oogl|O?nYwWx~mMp1l(0L~F zrfWw95az#_>;@8iP$EC9|XY?_A@Y zm-&OZiIO>S`**Hc%4-Giw&~Axq1n6EoJDWn8<+@SWjmz_ESsie;QUv$l6_bI>`Imi zI~dGz0ym@-Wn|C2ITP-GL`A?~=*COSC4NMs1x%ZMIyK4G*) zDB0~Y+=DDL$~7>V1$pH}Jt(@SvZ8yoQ=VqV*8gece^mD~Q~uA(m@uNZhbq@8iR^(Z z8bGfY<$!;)TN`q_nvaQtj)VRqn9Sa+y$&uze%`di$~q(bKt1$7xZ)<)RzcY?W$&Nb z)oj&uPq;tgKSD0%uWx2>K3>V3`Tftf(fW9{dy|K-f7E~IqVJV|fi(%rsGsUGd1c@M znTbl~9P;05Tpl<+2j(OxpZ*)yf5gnsLX;@2zuJYqJymJMWV-)p!+&W1KaaZq-}Pyu z{MI66xfOA4J3X{@y85~<|y%w`X_~>Zt}v+De0PLlrL*ilky&3BTHu( z%+2KZq zZ&@uX{g0I@NKL?8dn?+jp~~l{a}}NPBW2hyt+B{ZRnbHZv3bR^y>xI>m0#sH=bHZK zE^26t7Al7(vf0V+uHdzzL27sAyGUsXct$iYO(mw|;#4-3*QXk~e3Xj)M!1G(jPFm%mWu*Ce_{o(iY)g=%)eshylUfc1AASK3w5ul}{2 zRQu>`)u6n6DmSw9jzP~wy4O4=8>zch4r>i~lj_|6_Dw_AN9tN8#K_#GEg`^K&5WwG zZPc|9ey3OE~j%wanw_mJeoc8NxBoeg>kJRsN_Z<}whQQPA}o7+nK2B)i9 zS>bOIOvbEctwX&GpgIG)aaS>kHY4s1)VEqeRwEFSi zjDGy1*Z)F;_1mE3%b}$M*6(Mp#>cejZ);b?fq8@+d&VR7PZEN6DlNduL2XWW$=a=D zq#0ihI#jj^KQr~=AANnVPb;PHb*GYqeiv}+JbIF#jGIoPKa!uK3^ID-oAUT$e%5Ly zcZkh`mAVnDR7Nx!h} zw3E(rSBF>b0F`^|&z>~;8h@*~X+;yYP))e~IpZr`GeFIJ^_7n9ptdt0nr?63ALa$B znWc(PkopMz5q8r4w~j{f~4QXsM|6zgDG|C9)r{t z`iJ^-_F(m5A(rtOuAVBS4-Qq=z?qR|Bn^qBt6UuRj8Y$Gm@&Au>7voM gX(Bcab9#+ccOokMr`Q@bYOMbcuF=AY>hGfe2l)?jy8r+H diff --git a/checker/src/abstract_value.rs b/checker/src/abstract_value.rs index 90529b34..3e8ac613 100644 --- a/checker/src/abstract_value.rs +++ b/checker/src/abstract_value.rs @@ -2614,6 +2614,7 @@ impl AbstractValueTrait for Rc { match &self.expression { Expression::Cast { operand, .. } | Expression::TaggedExpression { operand, .. } + | Expression::Transmute { operand, .. } | Expression::UnknownTagCheck { operand, .. } => { operand.might_benefit_from_refinement() } @@ -3991,7 +3992,8 @@ impl AbstractValueTrait for Rc { | Expression::IntrinsicBitVectorUnary { operand, .. } | Expression::IntrinsicFloatingPointUnary { operand, .. } | Expression::LogicalNot { operand, .. } - | Expression::Neg { operand, .. } => { + | Expression::Neg { operand, .. } + | Expression::Transmute { operand, .. } => { operand.get_cached_tags().propagate_through(exp_tag_prop) } @@ -4062,6 +4064,7 @@ impl AbstractValueTrait for Rc { | Expression::Neg { operand } | Expression::LogicalNot { operand } | Expression::TaggedExpression { operand, .. } + | Expression::Transmute { operand, .. } | Expression::UnknownTagCheck { operand, .. } => { operand.get_widened_subexpression(path) } @@ -4436,6 +4439,12 @@ impl AbstractValueTrait for Rc { Expression::TaggedExpression { operand, tag } => operand .refine_parameters_and_paths(args, result, pre_env, post_env, fresh) .add_tag(*tag), + Expression::Transmute { + operand, + target_type, + } => operand + .refine_parameters_and_paths(args, result, pre_env, post_env, fresh) + .transmute(target_type.clone()), Expression::UninterpretedCall { callee, arguments, @@ -4822,6 +4831,12 @@ impl AbstractValueTrait for Rc { Expression::TaggedExpression { operand, tag } => { operand.refine_with(path_condition, depth + 1).add_tag(*tag) } + Expression::Transmute { + operand, + target_type, + } => operand + .refine_with(path_condition, depth + 1) + .transmute(target_type.clone()), Expression::UninterpretedCall { callee, arguments, @@ -4920,15 +4935,19 @@ impl AbstractValueTrait for Rc { fn transmute(&self, target_type: ExpressionType) -> Rc { if let Expression::CompileTimeConstant(c) = &self.expression { Rc::new(c.transmute(target_type).into()) - } else if target_type.is_integer() { + } else if target_type.is_integer() && self.expression.infer_type().is_integer() { self.unsigned_modulo(target_type.bit_length()) .cast(target_type) } else if target_type == ExpressionType::Bool { self.unsigned_modulo(target_type.bit_length()) .not_equals(Rc::new(ConstantDomain::U128(0).into())) } else { - // todo: add an expression case that will delay transmutation until the operand refines to a constant - AbstractValue::make_typed_unknown(target_type, Path::get_as_path(self.clone())) + AbstractValue::make_typed_unary(self.clone(), target_type, |operand, target_type| { + Expression::Transmute { + operand, + target_type, + } + }) } } @@ -5088,6 +5107,7 @@ impl AbstractValueTrait for Rc { | Expression::Neg { operand } | Expression::LogicalNot { operand } | Expression::TaggedExpression { operand, .. } + | Expression::Transmute { operand, .. } | Expression::UnknownTagCheck { operand, .. } => operand.uses(variables), Expression::CompileTimeConstant(..) => false, Expression::ConditionalExpression { diff --git a/checker/src/call_visitor.rs b/checker/src/call_visitor.rs index 6f214824..c6b4d8c0 100644 --- a/checker/src/call_visitor.rs +++ b/checker/src/call_visitor.rs @@ -2119,6 +2119,20 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E> ); self.copy_field_bits(source_fields, target_fields); } + (TyKind::Float(..), TyKind::Uint(..)) + | (TyKind::Float(..), TyKind::Int(..)) + | (TyKind::Uint(..), TyKind::Float(..)) + | (TyKind::Int(..), TyKind::Float(..)) => { + let val = self + .block_visitor + .bv + .lookup_path_and_refine_result(source_path, source_rustc_type); + let target_expression_type = ExpressionType::from(target_rustc_type.kind()); + self.block_visitor + .bv + .current_environment + .update_value_at(target_path, val.transmute(target_expression_type)); + } _ => { self.block_visitor.bv.copy_or_move_elements( target_path, diff --git a/checker/src/callbacks.rs b/checker/src/callbacks.rs index 2b0f755d..8f06fa40 100644 --- a/checker/src/callbacks.rs +++ b/checker/src/callbacks.rs @@ -141,12 +141,11 @@ impl MiraiCallbacks { fn is_excluded(file_name: &str) -> bool { file_name.contains("config/management/src") // too slow || file_name.contains("language/bytecode-verifier/src") // too slow - || file_name.contains("language/move-lang/src") // too slow + || file_name.contains("language/move-lang/src") // probably does not terminate || file_name.contains("language/move-model/src") // too slow - || file_name.contains("language/move-prover/bytecode/src") // too slow - || file_name.contains("language/tools/move-coverage/src") // too slow + || file_name.contains("language/move-prover/bytecode/src") // too slow + || file_name.contains("language/tools/move-coverage/src") /* probably does not terminate */ || file_name.contains("language/vm/src") // too slow - || file_name.contains("state-synchronizer/src") // Z3 encoding error || file_name.contains("types/src") // too slow } diff --git a/checker/src/expression.rs b/checker/src/expression.rs index 69a0c5f6..a0362d24 100644 --- a/checker/src/expression.rs +++ b/checker/src/expression.rs @@ -363,6 +363,12 @@ pub enum Expression { tag: Tag, }, + /// An expression that interprets the bits of operand as being a value of the target type + Transmute { + operand: Rc, + target_type: ExpressionType, + }, + /// An expression that represents the result of calling an unknown function. /// Typically this will be a trait method, function parameter, or an intrinsic/foreign function. /// In the case of a trait method or a function parameter, the caller might be able to refine @@ -591,6 +597,10 @@ impl Debug for Expression { Expression::TaggedExpression { operand, tag } => { f.write_fmt(format_args!("{:?} tagged with {:?}", operand, tag)) } + Expression::Transmute { + operand, + target_type, + } => f.write_fmt(format_args!("transmute({:?}, {:?})", operand, target_type)), Expression::UninterpretedCall { callee, arguments, @@ -667,9 +677,8 @@ impl Expression { | Expression::Cast { operand, .. } | Expression::IntrinsicBitVectorUnary { operand, .. } | Expression::IntrinsicFloatingPointUnary { operand, .. } - | Expression::TaggedExpression { operand, .. } => { - operand.expression.contains_local_variable() - } + | Expression::TaggedExpression { operand, .. } + | Expression::Transmute { operand, .. } => operand.expression.contains_local_variable(), Expression::Bottom => true, Expression::CompileTimeConstant(..) => false, @@ -767,9 +776,8 @@ impl Expression { | Expression::Cast { operand, .. } | Expression::IntrinsicBitVectorUnary { operand, .. } | Expression::IntrinsicFloatingPointUnary { operand, .. } - | Expression::TaggedExpression { operand, .. } => { - operand.expression.contains_parameter() - } + | Expression::TaggedExpression { operand, .. } + | Expression::Transmute { operand, .. } => operand.expression.contains_parameter(), Expression::Bottom => true, Expression::CompileTimeConstant(..) => false, @@ -864,9 +872,8 @@ impl Expression { | Expression::Cast { operand, .. } | Expression::IntrinsicBitVectorUnary { operand, .. } | Expression::IntrinsicFloatingPointUnary { operand, .. } - | Expression::TaggedExpression { operand, .. } => { - operand.expression.contains_widened_join() - } + | Expression::TaggedExpression { operand, .. } + | Expression::Transmute { operand, .. } => operand.expression.contains_widened_join(), Expression::Bottom => false, Expression::CompileTimeConstant(..) => false, @@ -981,6 +988,7 @@ impl Expression { Expression::SubOverflows { .. } => Some(TagPropagation::SubOverflows), Expression::Switch { .. } => None, Expression::TaggedExpression { .. } => None, + Expression::Transmute { .. } => Some(TagPropagation::Transmute), Expression::UninterpretedCall { .. } => Some(TagPropagation::UninterpretedCall), Expression::UnknownModelField { .. } => None, Expression::UnknownTagCheck { .. } => None, @@ -1122,6 +1130,7 @@ impl Expression { Expression::SubOverflows { .. } => Bool, Expression::Switch { default, .. } => default.expression.infer_type(), Expression::TaggedExpression { operand, .. } => operand.expression.infer_type(), + Expression::Transmute { target_type, .. } => target_type.clone(), Expression::UninterpretedCall { result_type, .. } => result_type.clone(), Expression::UnknownModelField { default, .. } => default.expression.infer_type(), Expression::UnknownTagCheck { .. } => Bool, @@ -1212,6 +1221,7 @@ impl Expression { | Expression::Neg { operand } | Expression::LogicalNot { operand } | Expression::TaggedExpression { operand, .. } + | Expression::Transmute { operand, .. } | Expression::UnknownTagCheck { operand, .. } => { operand.expression.record_heap_blocks_and_strings(result); } diff --git a/checker/src/z3_solver.rs b/checker/src/z3_solver.rs index 087bff01..66ed5c12 100644 --- a/checker/src/z3_solver.rs +++ b/checker/src/z3_solver.rs @@ -808,7 +808,10 @@ impl Z3Solver { | Expression::IntrinsicBitVectorUnary { operand, .. } | Expression::IntrinsicFloatingPointUnary { operand, .. } | Expression::LogicalNot { operand, .. } - | Expression::Neg { operand, .. } => self.general_has_tag(&operand.expression, tag), + | Expression::Neg { operand, .. } + | Expression::Transmute { operand, .. } => { + self.general_has_tag(&operand.expression, tag) + } Expression::UninterpretedCall { callee, arguments, .. @@ -1071,6 +1074,17 @@ impl Z3Solver { Expression::TaggedExpression { operand, .. } => { self.get_as_numeric_z3_ast(&operand.expression) } + Expression::Transmute { target_type, .. } => unsafe { + if target_type.is_floating_point_number() { + let sort = self.get_sort_for(target_type); + ( + true, + z3_sys::Z3_mk_fresh_const(self.z3_context, self.empty_str, sort), + ) + } else { + self.numeric_fresh_const() + } + }, Expression::Top | Expression::Bottom => self.numeric_fresh_const(), Expression::UninterpretedCall { result_type: var_type, diff --git a/checker/tests/run-pass/to_bits.rs b/checker/tests/run-pass/to_bits.rs new file mode 100644 index 00000000..2109c715 --- /dev/null +++ b/checker/tests/run-pass/to_bits.rs @@ -0,0 +1,14 @@ +// Copyright (c) Facebook, Inc. and its affiliates. +// +// This source code is licensed under the MIT license found in the +// LICENSE file in the root directory of this source tree. + +// A test for transmutation of floating point numbers to integers + +use mirai_annotations::*; + +pub fn t1() { + verify!((12.5f64).to_bits() == 0x4029000000000000); +} + +pub fn main() {} diff --git a/rebuild_std.sh b/rebuild_std.sh index 88a7623c..bb441951 100755 --- a/rebuild_std.sh +++ b/rebuild_std.sh @@ -9,16 +9,13 @@ # Exit immediately if a command exits with a non-zero status. set -e -# start clean -cargo clean - -#install mirai into cargo (use --debug because it is quicker to build and build is currently the long pole) -cargo uninstall -q mirai || true -cargo install --debug --path ./checker +cargo build # build the mirai-standard-contracts crate touch standard_contracts/src/lib.rs -RUSTFLAGS="-Z force-overflow-checks=off" RUSTC_WRAPPER=mirai RUST_BACKTRACE=1 MIRAI_LOG=warn MIRAI_START_FRESH=true MIRAI_SHARE_PERSISTENT_STORE=true MIRAI_FLAGS="--diag=paranoid" cargo build --lib -p mirai-standard-contracts +RUSTFLAGS="-Z force-overflow-checks=off" cargo build --lib -p mirai-standard-contracts +touch standard_contracts/src/lib.rs +RUSTFLAGS="-Z force-overflow-checks=off" RUSTC_WRAPPER=target/debug/mirai RUST_BACKTRACE=1 MIRAI_LOG=warn MIRAI_START_FRESH=true MIRAI_SHARE_PERSISTENT_STORE=true MIRAI_FlAGS="--diag=paranoid" cargo build --lib -p mirai-standard-contracts # collect the summary store into a tar file cd target/debug/deps From 571238648bbb2afd0f6c9202bb7627acdb6c1623 Mon Sep 17 00:00:00 2001 From: Herman Venter Date: Tue, 19 Jan 2021 11:12:10 -0800 Subject: [PATCH 7/7] Adapt to nightly 2021-02-12 --- .travis.yml | 2 +- checker/src/body_visitor.rs | 19 ++++++++++++++----- checker/src/call_visitor.rs | 5 ++--- checker/src/expression.rs | 31 +++++++++++++++---------------- checker/src/lib.rs | 1 - checker/src/utils.rs | 31 +++++++++++++++---------------- checker/src/z3_solver.rs | 3 +-- rust-toolchain | 2 +- setup.sh | 2 ++ 9 files changed, 51 insertions(+), 45 deletions(-) diff --git a/.travis.yml b/.travis.yml index ca5c28e3..fe3621c3 100644 --- a/.travis.yml +++ b/.travis.yml @@ -4,7 +4,7 @@ os: # - windows language: rust rust: -- nightly-2021-01-01 +- nightly-2021-02-09 before_install: - if [ ${TRAVIS_OS_NAME} == "osx" ]; then curl -L https://github.com/mozilla/grcov/releases/download/v0.5.9/grcov-osx-x86_64.tar.bz2 | tar jxf -; fi diff --git a/checker/src/body_visitor.rs b/checker/src/body_visitor.rs index 6e32a129..b3e700dc 100644 --- a/checker/src/body_visitor.rs +++ b/checker/src/body_visitor.rs @@ -29,7 +29,7 @@ use rpds::HashTrieMap; use rustc_errors::DiagnosticBuilder; use rustc_hir::def_id::DefId; use rustc_middle::mir; -use rustc_middle::ty::{Ty, TyCtxt, TyKind}; +use rustc_middle::ty::{Ty, TyCtxt, TyKind, UintTy}; use std::collections::{HashMap, HashSet}; use std::convert::TryFrom; use std::fmt::{Debug, Formatter, Result}; @@ -93,7 +93,9 @@ impl<'analysis, 'compilation, 'tcx, E> BodyVisitor<'analysis, 'compilation, 'tcx .summary_cache .get_summary_key_for(def_id) .clone(); - let mir = crate_visitor.tcx.optimized_mir(def_id); + let id = rustc_middle::ty::WithOptConstParam::unknown(def_id); + let def = rustc_middle::ty::InstanceDef::Item(id); + let mir = crate_visitor.tcx.instance_mir(def); let tcx = crate_visitor.tcx; BodyVisitor { cv: crate_visitor, @@ -161,8 +163,8 @@ impl<'analysis, 'compilation, 'tcx, E> BodyVisitor<'analysis, 'compilation, 'tcx function_constant_args: &[(Rc, Rc)], parameter_types: &[Ty<'tcx>], ) -> Summary { - if cfg!(DEBUG) { - let mut stdout = std::io::stdout(); + if !cfg!(DEBUG) { + let mut stdout = std::io::sink(); stdout.write_fmt(format_args!("{:?}", self.def_id)).unwrap(); rustc_mir::util::write_mir_pretty(self.tcx, Some(self.def_id), &mut stdout).unwrap(); info!("{:?}", stdout.flush()); @@ -783,6 +785,13 @@ impl<'analysis, 'compilation, 'tcx, E> BodyVisitor<'analysis, 'compilation, 'tcx #[logfn_inputs(TRACE)] fn promote_constants(&mut self) -> Environment { let mut environment = Environment::default(); + if matches!( + self.tcx.def_kind(self.def_id), + rustc_hir::def::DefKind::Variant + ) { + return environment; + } + trace!("def_id {:?}", self.tcx.def_kind(self.def_id)); let saved_mir = self.mir; for (ordinal, constant_mir) in self.tcx.promoted_mir(self.def_id).iter().enumerate() { self.mir = constant_mir; @@ -2057,7 +2066,7 @@ impl<'analysis, 'compilation, 'tcx, E> BodyVisitor<'analysis, 'compilation, 'tcx // The value is a string literal. See if the target will treat it as &[u8]. if let TyKind::Ref(_, ty, _) = root_rustc_type.kind() { if let TyKind::Slice(elem_ty) = ty.kind() { - if let TyKind::Uint(rustc_ast::ast::UintTy::U8) = elem_ty.kind() { + if let TyKind::Uint(UintTy::U8) = elem_ty.kind() { self.expand_aliased_string_literals_if_appropriate( &target_path, &value, diff --git a/checker/src/call_visitor.rs b/checker/src/call_visitor.rs index c6b4d8c0..d8a8d88b 100644 --- a/checker/src/call_visitor.rs +++ b/checker/src/call_visitor.rs @@ -5,11 +5,10 @@ use log_derive::*; use mirai_annotations::*; -use rustc_ast::ast; use rustc_hir::def_id::DefId; use rustc_middle::mir; use rustc_middle::ty::subst::{GenericArg, GenericArgKind, SubstsRef}; -use rustc_middle::ty::{AdtDef, Ty, TyCtxt, TyKind}; +use rustc_middle::ty::{AdtDef, Ty, TyCtxt, TyKind, UintTy}; use std::collections::HashMap; use std::fmt::{Debug, Formatter, Result}; use std::rc::Rc; @@ -2807,7 +2806,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx, E> let tag_propagation_set_rustc_const; match tag_substs_ref[0].unpack() { GenericArgKind::Const(rustc_const) - if *rustc_const.ty.kind() == TyKind::Uint(ast::UintTy::U128) => + if *rustc_const.ty.kind() == TyKind::Uint(UintTy::U128) => { tag_propagation_set_rustc_const = rustc_const } diff --git a/checker/src/expression.rs b/checker/src/expression.rs index a0362d24..242a4b93 100644 --- a/checker/src/expression.rs +++ b/checker/src/expression.rs @@ -12,8 +12,7 @@ use crate::type_visitor; use log_derive::*; use mirai_annotations::*; -use rustc_ast::ast; -use rustc_middle::ty::{Ty, TyCtxt, TyKind}; +use rustc_middle::ty::{FloatTy, IntTy, Ty, TyCtxt, TyKind, UintTy}; use serde::{Deserialize, Serialize}; use std::collections::HashSet; use std::fmt::{Debug, Formatter, Result}; @@ -1351,20 +1350,20 @@ impl<'a> From<&TyKind<'a>> for ExpressionType { match ty_kind { TyKind::Bool => ExpressionType::Bool, TyKind::Char => ExpressionType::Char, - TyKind::Int(ast::IntTy::Isize) => ExpressionType::Isize, - TyKind::Int(ast::IntTy::I8) => ExpressionType::I8, - TyKind::Int(ast::IntTy::I16) => ExpressionType::I16, - TyKind::Int(ast::IntTy::I32) => ExpressionType::I32, - TyKind::Int(ast::IntTy::I64) => ExpressionType::I64, - TyKind::Int(ast::IntTy::I128) => ExpressionType::I128, - TyKind::Uint(ast::UintTy::Usize) => ExpressionType::Usize, - TyKind::Uint(ast::UintTy::U8) => ExpressionType::U8, - TyKind::Uint(ast::UintTy::U16) => ExpressionType::U16, - TyKind::Uint(ast::UintTy::U32) => ExpressionType::U32, - TyKind::Uint(ast::UintTy::U64) => ExpressionType::U64, - TyKind::Uint(ast::UintTy::U128) => ExpressionType::U128, - TyKind::Float(ast::FloatTy::F32) => ExpressionType::F32, - TyKind::Float(ast::FloatTy::F64) => ExpressionType::F64, + TyKind::Int(IntTy::Isize) => ExpressionType::Isize, + TyKind::Int(IntTy::I8) => ExpressionType::I8, + TyKind::Int(IntTy::I16) => ExpressionType::I16, + TyKind::Int(IntTy::I32) => ExpressionType::I32, + TyKind::Int(IntTy::I64) => ExpressionType::I64, + TyKind::Int(IntTy::I128) => ExpressionType::I128, + TyKind::Uint(UintTy::Usize) => ExpressionType::Usize, + TyKind::Uint(UintTy::U8) => ExpressionType::U8, + TyKind::Uint(UintTy::U16) => ExpressionType::U16, + TyKind::Uint(UintTy::U32) => ExpressionType::U32, + TyKind::Uint(UintTy::U64) => ExpressionType::U64, + TyKind::Uint(UintTy::U128) => ExpressionType::U128, + TyKind::Float(FloatTy::F32) => ExpressionType::F32, + TyKind::Float(FloatTy::F64) => ExpressionType::F64, TyKind::Dynamic(..) | TyKind::Foreign(..) | TyKind::FnDef(..) diff --git a/checker/src/lib.rs b/checker/src/lib.rs index 02bf1103..13aa1fad 100644 --- a/checker/src/lib.rs +++ b/checker/src/lib.rs @@ -16,7 +16,6 @@ #![feature(box_patterns)] #![feature(box_syntax)] #![feature(core_intrinsics)] -#![feature(vec_remove_item)] extern crate rustc_ast; extern crate rustc_data_structures; diff --git a/checker/src/utils.rs b/checker/src/utils.rs index 3b14e0ba..4a6e14bd 100644 --- a/checker/src/utils.rs +++ b/checker/src/utils.rs @@ -13,7 +13,7 @@ use rustc_hir::{ItemKind, Node}; use rustc_middle::ty; use rustc_middle::ty::print::{FmtPrinter, Printer}; use rustc_middle::ty::subst::{GenericArgKind, SubstsRef}; -use rustc_middle::ty::{DefIdTree, ProjectionTy, Ty, TyCtxt, TyKind}; +use rustc_middle::ty::{DefIdTree, FloatTy, IntTy, ProjectionTy, Ty, TyCtxt, TyKind, UintTy}; use std::rc::Rc; /// Returns the location of the rust system binaries that are associated with this build of Mirai. @@ -97,35 +97,34 @@ pub fn argument_types_key_str<'tcx>( /// generic trait methods). fn append_mangled_type<'tcx>(str: &mut String, ty: Ty<'tcx>, tcx: TyCtxt<'tcx>) { trace!("append_mangled_type {:?} to {}", ty.kind(), str); - use rustc_ast::ast; use TyKind::*; match ty.kind() { Bool => str.push_str("bool"), Char => str.push_str("char"), Int(int_ty) => { str.push_str(match int_ty { - ast::IntTy::Isize => "isize", - ast::IntTy::I8 => "i8", - ast::IntTy::I16 => "i16", - ast::IntTy::I32 => "i32", - ast::IntTy::I64 => "i64", - ast::IntTy::I128 => "i128", + IntTy::Isize => "isize", + IntTy::I8 => "i8", + IntTy::I16 => "i16", + IntTy::I32 => "i32", + IntTy::I64 => "i64", + IntTy::I128 => "i128", }); } Uint(uint_ty) => { str.push_str(match uint_ty { - ast::UintTy::Usize => "usize", - ast::UintTy::U8 => "u8", - ast::UintTy::U16 => "u16", - ast::UintTy::U32 => "u32", - ast::UintTy::U64 => "u64", - ast::UintTy::U128 => "u128", + UintTy::Usize => "usize", + UintTy::U8 => "u8", + UintTy::U16 => "u16", + UintTy::U32 => "u32", + UintTy::U64 => "u64", + UintTy::U128 => "u128", }); } Float(float_ty) => { str.push_str(match float_ty { - ast::FloatTy::F32 => "f32", - ast::FloatTy::F64 => "f64", + FloatTy::F32 => "f32", + FloatTy::F64 => "f64", }); } Adt(def, subs) => { diff --git a/checker/src/z3_solver.rs b/checker/src/z3_solver.rs index 66ed5c12..dd7e5844 100644 --- a/checker/src/z3_solver.rs +++ b/checker/src/z3_solver.rs @@ -816,8 +816,7 @@ impl Z3Solver { Expression::UninterpretedCall { callee, arguments, .. } => { - let mut checks = Vec::new(); - checks.push(self.general_has_tag(&callee.expression, tag)); + let mut checks = vec![self.general_has_tag(&callee.expression, tag)]; for argument in arguments { checks.push(self.general_has_tag(&argument.expression, tag)); } diff --git a/rust-toolchain b/rust-toolchain index a2b82fb1..e500a60d 100644 --- a/rust-toolchain +++ b/rust-toolchain @@ -1 +1 @@ -nightly-2021-01-01 +nightly-2021-02-12 diff --git a/setup.sh b/setup.sh index b80e9ff3..7f996976 100755 --- a/setup.sh +++ b/setup.sh @@ -19,3 +19,5 @@ rustup "+$TOOLCHAIN" component add rustc-dev rustup "+$TOOLCHAIN" component add llvm-tools-preview # install audit cargo "+$TOOLCHAIN" install cargo-audit +# override tool chain +rustup override set $TOOLCHAIN