From 94382ebfade36f9ab1fda28630385d7827e4310f Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Thu, 5 May 2022 07:17:16 -0700 Subject: [PATCH 1/8] added alloc_sum_array_test example to arrays.c --- heapster-saw/examples/arrays.bc | Bin 12064 -> 12160 bytes heapster-saw/examples/arrays.c | 12 ++++++++++++ heapster-saw/examples/arrays.saw | 4 ++++ 3 files changed, 16 insertions(+) diff --git a/heapster-saw/examples/arrays.bc b/heapster-saw/examples/arrays.bc index 99b83c8c5ed0ca4931d42bf1c1345626e844fa93..711e36b39df8c2796290e18aaa83b2181ef60a03 100644 GIT binary patch literal 12160 zcmbt)4OAP~nf4uxq!B`YU>pl0#0dXHj%^UKjdA=p0_@<1v?7U9lDG#63k+EdLc;vm z{?ZW=7UrW_*>zpANzY1-yGu827uRmXw)wu506WwrDM{Uw^}0SHc2nv&S(>IYOPMu%HARR)LCA0Agk*{gL_?~-cF zn~qaH#R`cmS13H2Uj3CV+Bb76l5>*y0NT6Wq8m+QVzASb(ea4^$1 zQLXVsbd*tJl|k9;okS{Nko$T4Bvm?!_;kdF80#w_{| z4Ea|>%6C2bx9z%Vd;S%he$Jx57Ri4jq@00A_I%Q-d&{mLv*>0*x+}bX%#c45QeHIZ zW}p(vh&gnhtpqb^SjEh!qO4HOUoSWW_p^uhpHG?km(>%!d{)tzryBUjp(2@tRa{` z=Fv~5DslR|n&<<={!ZRs8uU9g417-ynSxJ+Mk(R-aQ;{X`u@4EdwZ(8B#POBOv$%3GF#OH`QVpxjKDa<9O>T(>E@t!A(&$QO&oANzd_3!?x#1~yqE~nrM0v>?C%LMrM2G9 zCgw2Y5BZ%O;}#Mym5|>v1bv5+LSiV92+|w-<7q(MCMX|fwv5s|pbly<0oZ6ajC_;d ziSv~l_M5_tzdM^h<t<$g)`(libV4hnlpRAKq4X;(12M#l#`oP9T?15`Ormi#iarM{8{O*4aU_zv(e*XgDjLe z3-k3X{H~Mnx`|m`V-B^ozoN`HK3FbTfP1K2@h(xnuTg!(tJW#X^~Y#pSxPIV7SvnF+`Nqv1@HE&g|(@f-F z1G6^dkJkKQ~rpVMh$4mB|wn*f!}MjnmEX#?mmowp@W zZ5Qva1EbXXT|@q!AvuW59ZgKP&EKK*cLe>pZ#<^{ zfT%yTs%`{S*E#hptGWffV2wa#Xti${bXPt4t5MyJ+5DT7zEN9KHd686i{8ys*5&bz z*!*4HO!rVt^+y3Uj)49dfhP?4K-JGudi-ER{=8lKc%QdyYJBrZ#a0-QJ7ZgJRBY~t z+ws8*a_FhQ3%&=OfRS+xdG=h_sBVQ-zqYD=Z(0_4%c8$Ay9BKB8hk)i?&cBi*7M#x z-+0+z#ipt8Eu)c5ljG3GEmKwJ+rf5iOuN8pqz6Fo7npySzKX5rSL9~6%vJ0%&)~6R zZ&n61M#q*CbNO=t!%N-v--;hzwkpHSv{^GBTBq==Vc+I5cdp)&MaW~753^4+xZKTc zt(9GNS7Y*~q5i-=c2{d-TOy}xZF#K7t%bbehHm?QXG??I;)E-^x5eJNkL`@L z&z6)FnTlX)gxs|yC8l+FZ!Rh|uPUx?u6Nm8J;jySZkw~gRb0`wf4{xeQQh3y@OWEW zi@O-Q;x2x~zV}Oy)fTxOe^-3K?J90=-P>}&(NOH}aTnKh^f(*fr@6JGbbVb%QByq8 z(gxokTp$Cw)Y8z}{I|B3XzM_-u|z7>+JRPg^S;&w2McA~2loH1O{RAdX9;^4`~6#M zZeCYb8Xvu)rn)+Z-PP6HDj=b*L+DO=PXLcQyWs+dsW-4`ne58C-hgG9?8)`LfnCdF z|FQmZj>*BpQ*i@afCJenlg&~(&SzXv(4{Tw6uQvsrVdG|mC`a~icD!(dNC&=;Vld& z%`_5;sfMn-l-o^~;>+PmFzJ~fR8 zq|Zd9>#{`i(l946QN(1W9w%hVO&m^-$VnD$;2VBI6%#j>#=9LCBFwblHlU(L$cx4* zs-d^QO(y}TLc$7f-c?KfRHcmQ$^BCDTD$JGfAeYkJ@_|DIsVPFYS{Z=ZL3XwlVe(= zQb^1PRX2mG4zSdWOZ{Ja{d=!}`~9z-dG5PY7Y5hfYH2+&_UACGm|&Nbmj1YOiTUih zZ=U^8O>fa+y#40-@0&NmotcpD0Qak){Y<&b2%O3staT1mYz1l@sn|3<-utfZVoW4~ z0FXCh=d{1!em8K{v~ij|Pw+XlAN-0C*fxf=Gu{mZAlijN5EEzgk? zikqN$GvS}yF~T@(x^n}(dNSPKxR@#kQ147VAllB-ju&=|pXH+nPXDVf! zkzCKVtF>n1WtQ;mM@JZCZcZ~x!lRWlv|ll>UQ2AfWd9-`{{kx(^vk*|ZsoDD>dL^b z)22m~BYV|UC3(J5J}#XIXu|ywif6UjuY7=#=T*3DpGNg#+H1|Rk1)j4!pUURpjJm@ zy`DE`KY>Rhe})VF7r3a`Nq5Xj4-qmht#l@<`qlgR=tpo#Rdooe;wY|BA-^7_NswaK zN&6!66j5xHMRKRKIXlOosh?_OkwJ@HCsa6bOcNfowCDUULe7aV_$Y2CzCH0fcv}Q- zOA7x;kq%DNo9h*|-yy_ECViCYs%E_nzMTC=0ST`e=fqI%9c(2}Q(ZyeV;{Xkk*VyQ zMN+bsdcMSXQkg^e`*>(SQ_G9Uv?!44tzSi32~n_`p%UYL>xhJCOUj5wOk0%w2F#M? z5ZesjFA~AcNfF$f3=WxyQ8YPdc~cBuo>#3UREdC#r^TEard&Ae>|cu;pBVAG05^3> z+|X4y>_XgV@&(+m0|IU$Hw4^xn`5~72I6L;mEM@b%~CUeHI5raF853lH|$2ljizOh zxc@HPhy~na{nfbP>i-JdNW{!vfgA4G1a1cA05>eo{Emq@ZnQ9OH7VR=<)`7susDgE z9e|sGpCoW|VR;fa^{%^dQ=P)ig&S$Ok?c<4h5&BXr~o%75jRgHaWiHH-0+z!z~W3A zY{W6xtVxH>nT4?NNK&x5CvN%y4~xWA_vD)u@GQXO4t)L;5{B1?gs~AOK9B`WaO&Yt2pJ}5 z*c-k|NWR8ryBM51zMX)BGuwf>#7cx<{zph%CJj*6n=4@1F)kJV9I5L~dl0GXHK3)3 ztx)b-6eutQNvufmCqjyxwlShDWl!>CrGkI57wV24*+zIfJ?4?Y&Fv#w!87#k9V0A* ze5Xy33k`FN-10-k3u5%Oc-UD&j>GTg;baXwi{WHKjHHyrNu9kBG-whlCEC6cSjkmx zAx4@E?G_*6qz)5s$~KlZYh!T9wZ-6~IR500dB$OtzCB>b`69KrRMQ-kf-8SPMrkCr z7<%>wr7%?w`?fYs+7ws0n7>lx4tnwwB=~zylw0nYtTLLl0HEh1VLe$Xn=ZA;Ml;H% z!P$O3hEjg(TLOlDjL1m%t-**E@By4JDksaN4C%GmI(~o!<`60zoS%*lT1uqtF`5!H zN%!_976_!fw+q@k5kRB>qCg};Msl+iX0QpNVUd0jpyTvv0x|%mxr)PtIK+;N zL8JEufKHB}YnTQmiMg#)iqAl)f&2yhlUY#-kUU{|NASKTC57+t9uashodD>Pz1E>f z5>4izd!vcxpbybCNT%RjwiDEMY)ra(wAkG9>pA=3tSWqM3xR)2uLE2 zda1dV-l!n}J>Qr#kiJB~TBTsE!BLL}v!a6{wBjc@ zP;M7=I(ROyDOZc*@E}V+icx6z(#zD+fGA;9syBG3b3N91K*OBIH4s?fuy->nA!UYs zV0G0^C}Eoj6HcQz@gNHV@{~&VC=#zoA&k<^D3pzviipOFx-~HWEhak=PY?`yJuS8^ z&~+d+0B1Yy>7VaU*of3eBUc}6aJAJ5@qv_o-YV1bqSIjCuH#fJd?`WXD}0RNdd{O3It(!br zOz^pKpX6tdPR)H?qpNLyTVrDq19Xi>Qj?AW;Ki2!1Hg;k8o+?3AP_M+S4*v?zQ<-b z0_*kGk)s;kN-nMt6_^~X{22`{0HfX`ipoe_rop0;mA9IpA9RL8cFeFWwA0S3$!zpYJm|z|e0|vPb1|OG(N#A)79oA`uo3@W7ck4?Gd)fz?BiGllcCxv3AF;TBZA~2=p z@8XC={6OqU`b}MG(Vx)r!y?q_3;4u&F3AK5EQREqsKerF|9(MyEx^ai;aDxbf}D?s zEB4%iiqwJ^PBb@CJ|SRIEKQlQJgNI@srTaRN6Bg@5Oy3-lGRPPP*n6Hp3azHs;33% zzZkWdfT#22zfa(4;E5{0Q!>)f1T1u3l&1dWKt7}dJ>#BPaI~xhJ>%*%!GvdY_R&J{ zKvsx~Y)=H;^a>UT?8`=Q>T?+&C#lRqsAB`JRBY6TG@0XBq{cNSKs`|77zxUtQpuX- zaKA(b)Ct4;7#CaTfGnICLs^&&q$qzv=7rTnW)TD@jwodhusrC1lejvqwak&9xUXIideQQdmt{LW3g@ii3B|Wb=Gl>Y zljO;vz8ykrb2t{;%#&>_lWcT)AMrt42-c~0c!T$;vOWT6?=84Ryxm-`?M3-9m*R&qH?2{pIVvhG0G&|Z_6!4a`Qgv9b)~l zDGDC6{GT7u^nwR9IyoX2^ICut9C`d2&F1;-nR%Mc;55EkLwqM2yZCDCOx+b#=zz{dA zi~sy5$fX4%{TNc{qkkBV)dExx%Zj*R)!l@rYQans&0Q@=j0v}Y0U329YXheh7wMXNv zNm*iwhg3YoLnw_6HZTrr42r|vIkd#5%qGjhS^96_ZyGc?3)Z6vtBn%GrZaF*+!~0 zTTuT(h@4)R_4q=Y1wu{JK4;NZX3(q>{whn=fM&Ho`$VvS6%Bbj9)sFZHsJy76E~`> zf(;8QIN`1O>FalUs}dDRj+jwh41xL?4I^jI@GPuKfW-5}%V9Y=(5^)xo9i<`-eeFX z5UMHAy#MIqo`*2>(3p=3P#QqF0Z~3__#@QA#p7=REbbJGYp3C`u5^7; z`*;sbdJm-I1hmilfRjJ5IhFB1s<|nvto_))3o;$T4r{-A(b2h6|;M&H=;ymMS z2ge{2byb1yDbmD(iN`URNS+db4t}))LgUkvp&w!dcKTF?3`z{G0972Txd{m}OMMAG z9%S{7EecQqux$~aV~i~hft-pRb~eE`3)i?D?33dhKLEwzb1Z0F*otngYjX$+*Inmm zPG9F7nuIv)5PK}L6~j9i z_R*Qc3l04?E_2`Vd$xk1vvEUD?P+|TmWBPM_%z1$!u}nnaXLPYGZlF;6`JCPj!`Ud z8zGU1DcaRNDJ{FR3xQJcUvN=>ghj!U{yVN^$I`WIEQI+g7D+T0t@w@Z80q?tc`9bwQOO5c6(gQ-k@Ra>WpN=gm0?^+3yPo`A@aQ^YXY3B8a7MFR%DqE4ain;mcgAd6GXLOrCnZtEA3uf zl|{#em9`ZEjzFDNsg<@zT>;fRg4KL%0b`hf51R4Y)r4iGF}^`8*0b;(!eM8zM&uid z;QP==VqB8TI$<%KC@(nyFCiv%kS}0TUMYpmY+`R|Y1=C-xrE?LT}OkvqgJSge`-a( zBgl~4+v5edX`Zm}P+Tr}nXnREOq2=#gC$DaDv12+g~(-2S|cJXdLk4GR{|F-nAJNpgz={T-B5KLHZ7OOg8hY7IrNxhoK}sS}v^21wrNVeivJ=pfVL?k-*|C-kM^8Zva{2e*ixk7( zGLfAM1rbMrABvv27%a>9c1+p4BYX+3#bw3QVhBaRVF1p-ee%qAh|K3P4$`|$^fkZ8 z44gjtFK04;y1w8` zXMw*!8fa8_R};^dt%0)81`bd@ocLa%d_Lr(3c}bs$h~C#{g99EgG&|OOO)RT`HLa1 z0#595BEK5)@gJPO3@6r?$p3P@9y{b=`-%L0kiQ7-op53tBawd)^3hMAP2!j(@;#6b zLrePM#C8(-UxR$C_v>(`_v^)Y{UOLtum4{mAHV+`oax^Wx8y6(KnMK7+?~d`OYJ|v z#zRX>=l&u`{k|dxr0tNA{*M@S$-87CwhxxNO>JSM!gi^Y5WxFvEGM?|P187ONsv3A zb&U6-rP#lFb(fXG8*AU3RNU(=Epx2*eYzXf77$3j~1Rfdq2NW=e?eYWp)_v$>(D<1z3x@k+$ literal 12064 zcmcgyeOOaxmVa;V&AlOnBtX^p38@kWtjvn13t?2!-Gg8O-QDqm?$8>6mHJ9;;3zk+0N=KHaKAfhq_|dP`x-=yrMQIFs!#drD&N_oigzDZA1J& zQWd)fjCYvt2$nw*-g}fkI|c0?;R!LqZ^iQZ48CQM`Tp|b1Ms*!FcviA?0kGUbKv++ zz1PEptRX#5tWAuQ59yDO)V!!CjP-cEI zf3-sOB2nciNdt89I`or&;~Uri02d{a3^Q$|$0cK+C&=}g1KlC+;8dV080a~{_3!~V zAE@F3-f+MR>2`nL5Z4z9R0&*fyZ@kyJ7nb|rg2}v$73eRXBxK^epXy?X)NnwU*Y>M z(~PU&qODF7vPnvfb^T*a}|!;Oc%yX7p21S;(`lfS?7vP7oZVJ2#C%= zpP7>cu1^&>Xbx0Kfu4GJaPiI66AfOFn1^^Cq|Qr5WQh2kp|Rlgz^z?^BGzK)IkdZfQ|OR%C`qZ+^^KK zemy>a*u@6B1C{D~G`Yk8u4Pk%Qiw^C+8SSBY?LMM&iyVx?!*hoO&OO7< z^IVT!PRqi00f5y(D|g7rd1u&P!&A=gb834DcSz5 z?D3#VUq@E`Zak=NXW|2fu@WM&#$D@!6eD3qzGjI1rFU$EsFDJ5o3s9>>=6aArX*12 zj!nHcxATPJhlJ=;h1NxapDZ=7L`q3Q)ZyK;^A ztY}hXr8PftH2vtNA+67S@}?oZ6b^#T#l4U(i49)h9V7QcaKH){q;I)?@3#q=Jk&ps#XV7JOz9C1eB{(Nv6qJQ=5U>GGw<5Obpk^+Tj`P)_hEK zpX#;OByFXprVw-!0Nf@hF3I8aYfM4(ACrPhJ#M- z;dX9AJ0Ob(do<8D>MQwdUi(>0`yUbQRe^4r8Z*s} znLxkbdC6sZtJpN@1N+9lAGB|rvTq!fpJyg4BX$eu+{i>3bb6z|`aE47p3uD65fJwT z+@jyx&hSlTERhR{D21AD${a&%@lCSVm%rrM! z@CjAeW^Ay8?VFDItEU|+6BBU;dV0Cu(T1JZf;wD*!iQuVQd|IL{4uH!2V7h*?_zfk z`YqEF)nWSNqW#FB{X$p~ea}`n zH@gfp_d^&!eO`6gzvUHw{=kG~*uHUkV)L2k#;FOI;mqf45nl5p z=j}t9ybO0mJ-@;?eDvtMwIRK^WpjB&&6C067e-wxxg9H3XS~dH#WL0Prnd#=_tKt; zJB`=pYwxMu!Qa>F_H^v;s_k*P+ftdHKCnY`2?Jjqtr{hqoW4oQ-*?O?G z)8%%%`aGr0W%qiZiL!kzueZ^iu=tF;UY*>=^Id0ahfJJmNPR`*(v zm9_S|_KBUX9-9bHzPZ!Y^&o#RJ`TRTqEsjqc(W{BTV5eRuC%hEv|@D`7Vl_wd11Jo zvOUfFTUtw9qF83%-{o!X@_Nc@aajAsR(F}B)8%d3@80JryW7?Lt$X&AiU~nl8JK+P zwWsCJ69pml|JzU50gt<^qpP{|Kuc?xr_WQ?=i825Ejg?Msc|J!3j;gQ<>`2^tF?uPGM)qb{)D4TUpPc1u3P-~PdJE@~`JI|A)+qgH#dD%fi?&YfuX+y4*-tObtHq_TRldxby0C>&dQ> z*bX^+`x7UppMV^kZ+-+m70*VQYPT7D6?bTlIBMSlE+=f?I5W}zvFTi#m;%i$F1RB5 zfTim$JGKAn0N0|MLkFY#SBLgmI0kjW^PRvW0kronFbx)dx#`Wv{nf|7dC^-!{>|XX zf)ls~E}oEK_|0Xul^`iWUchW4--I9Xxj@KD_+5V2RIq`qWwIdM3|7n4(d7{u-L1`# z|MBq&&2=L9`wePBSs4w1$vE%JzUIp_zIk%_JY6X~|DC!R*Cts`KTZtOgihYOs#r?oeb(DLs3fNjmG;wMf!OL9(P8Ni3-gQ zgKLH(LZ?-wqK1toqU!gZdiTHKmH1!qpl`rKSIO4RvcOg+*jh2w)CX7b)vNGWXzF2T z%1ZH->|pnGip-FyVVg^M3@T>Th%88tf^@oqsex{dcNLLHnCf21K*n?yG9|Wh7YSxV z9iJsc$Zk^6?BH|E#LD&Sr;UaoT8(YzvJuffBSoRqZYXtHLucd5%kmtAEDAE)v(-e{ z;n-;;uQ1R?$#a0=wGzC@G!7}qi~@Q%HR1yyt5<>aFY-W|n7YJHVqcjnpoLCrErreP zC{8wKprE;RHW(|L%UZ2~PsGLjjHH7f`Ev1pEN%uEE!0?qo5mDw=ph4t6K-nbxEYG$ zM%XCh#(7c3jqQhk8=}2Hv?<*9-_-DyIBtB+tUf=98(O7B+%UgnsP`7*hLLfT{YT@* z+Vn@@M#*r01a7R4C2>>d1%&7+*rDw5IBo>MP2I=>ZfetUQ=h_(194NnF_gf~&IR0j z|7P5j-wUM@xcPoMZgwx=2C=v27~;kU2)HkW8`radn}`xI^8NyBsHQkV4+yM(==Ga#M94WyH{=5B4(O_&iUWLpzE{GGaat}XIx^yG4) zti1Bnck1-&wwdp&Iox1T?lwN7dNei~J;zdHc*nrj-f5?wrpUS5`-`k?kti6$O}drA z;@ZQ*1HWRwB#sZQMP!vqUu9FhoKX`(Tlw{NM@kusi?Xqh?amuuG0^UGJ|G)_ViO}Y ziG)|NhgYG+nUF2izoS`!MgHKnYcQ<1SsFWwX2~fR!Uvco<+9&VM3b-g*$CK$5*sut z4iyoiL~S?y7K{-M#z^_*@1fKN6_p3lV;~iN&KtpiM6&>5EodUV+hMDhV5J9g)nvxU zGXT101{B0WrUoeCl75{Nn)W(i?@K1E@=Hm99q+UgC>enB?R1Vw9zuDuqnC!(ZpYU4 z8gEc!Z!7|BbXrR&3QW>zM(+80XiW#`?8va~^DI!2)6AO#lvRtPH8POThoV$Dp<#W| zzPze=ZY6~JH+1`SgRD~+x;;Or^9l$!_3;ly1VA>Bl3wX-N}@jFr70L&ofHxi5R5KX1hM(w*yRpdObK@hbGGn|y67`a=o*w?S`{NFIN;Jcoa zG4vWDBk8+_qej37?1Q3)tYA6P?{s#a!U7i%Dg^F7On_NnyW^&c;ZiOxiUl0$F7B-H z2CAqGqF^*>kd%35*s67C4}!ig06Ld=rUkGNq%af5k&X2O=JL=|v<4A0XulfRyHl(lY&1AOJ1PCp(4d}Vrz+#5JNh5+aXjg<6yWI;doTv3MS;qiZ$eGZ zvMIn#Df3Gpb6Vp=_s}WETRL2W79!seO6oWR)duq|V_40H)dutHA(L=OT`{m2Gw94d zXNM6$H8X$&1F3L<1!HtZXnDT?=B9--oeTBS+YH3{y6@0H2F=q*jl$ID41(Ydo9ulM zMG3t)W<#5*i{WhMaUxJ^(pL$bDhmcwXL7zk$g5KBXl%OM6g*KdyY0q(-&LHwKcMz&OmY{FuS{%@s0XjQtI&ND{ zB11l;q~=Z@?CDvP1;T&8FPG}UB9?P^!TXXZ@In1j)FrOP33Zp@Knp^?)k#WtKxAJe za7(&gpxrG>*j-)1 zRda3OCe`3Q*1;?~!iwP|deQ(cxdv5$i>tsDP=VhjRNyi4EL9W%wOnx3e&1FyQlz;? zIs3^2xdY@mp2>spRAxu(cG44rV zp7{(O1aHL3=>{o5*WhqDq%dhn=nJbNucl?H{zQXup0@sATw2W7ZiN9lW$)S-FfgCM zK(X2h_70DTDgSv3E;eXBeNm0&vyRCuD4r7%h+6Hjf&W8jIW zb2Omwt2I!@i%1);QG#XoDgvPGkc@!Q8ki{{AkMo&z`LFXM;*UhJRz?^GMBmQmbzaK z@8Y~`K$!#SwvJAqTaB)+mPQDtHH!N^3;TbsS$S{z{-X_8ldu6x5;g!J@MD!Vs`+j) zIKwd~`xD1cjN5EW?sH8Lu9I-jsVH8FaRE5ry%b5Yck7avl>kg;xRJb*3W(((Oh^TN zp9FLACd12T)%2s}#2(`n8ocJ~t5nn?K7W&qNX8KuU&?phws81Q^7#`AKE(mnnTBZ1LTHgK|3A6DPY1*UZV7WY`5(txj?O zlM+xR`5YNlUjkGn@Dx>FgiMLwi3Vtm27u^A`u|EzP6AJLYu2Uk6qizoh(ieA_^vwb z1h8ghh>%IFer6n;tyK+h99&cKd=ieb6ycbSaQwR%1R17tz$cwuV}LT(uwq1kXH)dQ z$`UKI7RPa1iv5y0^hjZ}a(nssA!29Z5CP0EI}@4Vb}VvI&w_3&+Y1&AHek0kbs7qf zgUPcl!J(Cy@mK+cUlw46!MnvVj%SMpd0-Us<>CpMg;XxH{gxQF!8;k_Ig|8Zo*@YA zik8mu&WeXpyzjev2EUt*Z3t{d*8;YA!*pyZV4GLBiJ7f{Z6JE$*r-hO&N!y;=m(;= z*WzC?v3hE}TUqO>t5gdtyovnt~dr$bA36(ib-`cWtQ zQ^G+Y2jmc6JE61~@dP3%TG>|#g#6%a>yTgoF@oi->hC$(Gbm4;Ow`NN+bGBD4nZxw zK1eyp`BIIfaQ25?xdS|S&x=g)1<;cXHq|B=OJ(-VVm}(!k;GA0cCVdQV`lQW@$L`N zlnS!rOh(k!iXoZtjHQ&S;1fi-Y=5U9g$(U{|821Ou&1>t1MU4=cy;F_HppWsaMBH# zJ+MLvrP}tOtW>gs{sxP}mcJT_w*qD!oL@qz9{4r9)yXQF?Cw$x9!um{pnU!S%y(zj z1IjWGWv@v9lOVd%?o5b{B$cW=^Dkv1EuoQKi?%jF1f;0kgM1)6k3)qC#l~yp9`u=U zwT039GS%QZv$2OWp&tO-!~mTy^Ur{|CDhiJxfl5$?LxIJH2}Sww1WD~^*4k1WB|D9 zO6!5tZIRtTTxvu0k%N9eb3B_Q2}d)Zgq~!w${=Z+8*c)4;KMZuQ^m?SAuxchlp3Hp zxk#+vI0D)y!ubi-r9Pp3@~G?L9JSeTbzFdPDjE~_kbiGgZ>Hp<}$VEy7*8CDqsxy zK6sbV#cyHx%sWk4sE_bDs!{a1|Ae1T(!VZQ@Z$}BT!KXEiwS;jOxXvqeo(yGK3Hnk zunq0XZyR^xe?>(8n&$m?S_!iUzE2blk8^O`fUD#oQVBn1{O2bEuYi?Hs{z=Agk6&V zo-_Wt2S`W({>~aL_luT60+d-{-rT0w_V9RWB+9omlN5wqXZm=brnsVI<#~(d1{Ioi z#dNUBTF`O~r(^4t+2hA5NBRls)fB2=(ywJ}TTulUaimjNK#xj4fe#F$TP7*k z{DcBtl=WR^%So>`L?dwpr?KGG%C%_bWd*!EgPy<{_XK(wixXLj9Kh093u5WCW?T=* zYjFU!gEU66{#I`WJy2GHG*228h>B`C7vcje4J4+ZR%s*`U6Y}5juZayQ+fX9O;0(9 zv~@7@tUwNDslLHW8MO0heze?t&P9}jXM=hEUzrS0CaX>JxW{Ovh@vUUl@Y(sF5*f( zu#R8BE+5BkF}zD~B{>eBhTF!fbt#_YKXAc+ARQ~flWf(sYYyLORPIWIoi@#ZQ;LV3 z_5`XEVW(F1>LTO*QUQCNIOc^2hMflP*7tYz>)T-r{|6VAg9GvwC-?c3wgdUgqJ91) z?sGVOpU-YOkFlgAdyxsw>rm*<Zm#d&d4NIO-%UTl}aqlLN-*bM29$WKaPNRPKU-`V?7#{B0y#_e~f( zfU0gYb_P+%h9wc*bItzzX@jbo+-X-=}=ELwkzpHV7i_C^SjV&GN z=b?u$&=23V&(zj9A0|a{J}l`v;7qK%$1;fI_Q|{p_Com#^d+2u9zG+Vfoh5zZK4iC zK@cLMr!@16l-;luj>DmAE;!BSGOC2Kr@n!F9p^ooa?kN^Xa9iPn2bMOu;;_7EwT-r zuV8^I2#I9;(WUEK;JoLm5GZy$IqNVEgYNl16P$NEo%6=Sor^xz#q3|Ixi!Uk=g`tv@eEbB6}jiK5{O*S+2OQ1;}f80-Btmla^Ojy3&=UD zTLxxmHG1jag?%ZHDobUL`fWyT01jAIo!sh5Y*iJfqzzV?l1706T$unvY1Km!<<{XS zAWgYM_Lc*N1u$M0Fbc*%x2KX|Ji9ds#s%Km#KS;HF#r_5!DhyYYQSe6rnip_b{yj# zKYrw;lbJuSdg9;S&}qi4nsbuot%&9wlJ%Z73qG=5jAX5ZN^o`agutgfQlZr^A0V@= zdHykp{=KSRIw2{KWwwj&NZiL+L(b2njK9&J;LX0wQ@K;2Z&Fy5v_i!P;WvjK5pZ1S zj84PN!o3r2EVT!2yzm#t8H`sYKZEpbaQ^~sP#O6h{G{Gv8q4GL0o?e#5HFMgaQ=WF zp??kO?1W68kgG}v`4Z9?v?_ob>m|!)K;OuvF`k=|CeH;q)(6uo*GraP0rDjvv%`(w z;gfO;$nhVSzYRCGmz3KR?YKaO{U_!3fIJuSpqm8G#z}b_$kCqk!;Nc}lG(A|_0%;cr z(m&)krgEu7{2R(bb|L(|5b9e<$$_7*#sT7|rZk_ImIU|rRYMv7H>zGs6}(*w|0UJg zx^|zddB3N(TqrGHUs{#?@2!OaV?e&~=E>dkIxV{}A^96o+M9(5Hm1!hEs3$M#;?v% aj(JqXLmvr7DvOe7`0uE%&J(w5(e*!&x**a3 diff --git a/heapster-saw/examples/arrays.c b/heapster-saw/examples/arrays.c index ceabdf0267..ac510c31bb 100644 --- a/heapster-saw/examples/arrays.c +++ b/heapster-saw/examples/arrays.c @@ -122,3 +122,15 @@ uint64_t even_odd_sums_diff(const uint64_t *arr, size_t len) { } return sum; } + +uint64_t alloc_sum_array_test (void) { + uint64_t X[8]; + X[0] = 0; X[1] = 1; X[2] = 2; X[3] = 3; + X[4] = 4; X[5] = 5; X[6] = 6; X[7] = 7; + /* + for (uint64_t i = 0; i < 16; ++i) { + X[i] = i; + } + */ + return sum_inc_ptr (X, 8); +} diff --git a/heapster-saw/examples/arrays.saw b/heapster-saw/examples/arrays.saw index ee86907ea8..c7d23e1462 100644 --- a/heapster-saw/examples/arrays.saw +++ b/heapster-saw/examples/arrays.saw @@ -62,4 +62,8 @@ heapster_typecheck_fun env "even_odd_sums_diff" "(l:bv 64). arg0:array(W,0,<2*l,*8,fieldsh(int64<>)), arg1:eq(llvmword(2*l)) -o \ \ arg0:array(W,0,<2*l,*8,fieldsh(int64<>)), arg1:true, ret:int64<>"; +heapster_set_debug_level env 2; +heapster_typecheck_fun env "alloc_sum_array_test" "(). empty -o ret:int64<>"; +heapster_set_debug_level env 0; + heapster_export_coq env "arrays_gen.v"; From c2882a5bf06680ebdc24a9150cc01403fad2af9d Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Thu, 5 May 2022 15:21:53 -0700 Subject: [PATCH 2/8] whoops, called the wrong array sum function in alloc_sum_array_test --- heapster-saw/examples/arrays.bc | Bin 12160 -> 12160 bytes heapster-saw/examples/arrays.c | 2 +- 2 files changed, 1 insertion(+), 1 deletion(-) diff --git a/heapster-saw/examples/arrays.bc b/heapster-saw/examples/arrays.bc index 711e36b39df8c2796290e18aaa83b2181ef60a03..7b734c75380dea34af2ab065baa2d718a4f4ab18 100644 GIT binary patch delta 86 zcmZpOZ;0o;cR-w*0SH8ZIAtQQG2@Gkj^3<{UYmPa`BfMjH_z3a$*8o&j-f%2nVG@S mAYezrEJF=Hr Date: Thu, 5 May 2022 15:22:57 -0700 Subject: [PATCH 3/8] cleaned up the code for proveVarLLVMArray, eliminating some bugs and infinite loops --- .../src/Verifier/SAW/Heapster/Implication.hs | 319 ++++++++++-------- .../src/Verifier/SAW/Heapster/Permissions.hs | 120 +++++-- 2 files changed, 271 insertions(+), 168 deletions(-) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs index 3501935e4c..64b2831749 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs @@ -58,6 +58,7 @@ import Lang.Crucible.LLVM.MemModel import Lang.Crucible.CFG.Core import Lang.Crucible.FunctionHandle import Verifier.SAW.Term.Functor (Ident) +import Lang.Crucible.LLVM.Bytes import Data.Binding.Hobbits import Verifier.SAW.Heapster.CruUtil @@ -779,15 +780,14 @@ data SimplImpl ps_in ps_out where -- translation to give a default value to the cells of the output array -- permission: -- - -- > x:[l2]memblock(rw,off1, -o x:[2]memblock(rw,off1, x:[l2]memblock(rw,off1, -o x:[l2]memblock(rw,off1, * x:[l]array(rw,off, - ExprVar (LLVMPointerType w) -> - LLVMBlockPerm w -> - LLVMArrayPerm w -> - SimplImpl (RNil :> LLVMPointerType w) (RNil :> LLVMPointerType w :> LLVMPointerType w) + (1 <= w, KnownNat w) => ExprVar (LLVMPointerType w) -> + LLVMBlockPerm w -> LLVMArrayPerm w -> + SimplImpl (RNil :> LLVMPointerType w) + (RNil :> LLVMPointerType w :> LLVMPointerType w) -- | Convert an array of byte-sized cells to a field of the same size with -- @true@ contents: @@ -6519,7 +6519,7 @@ proveVarLLVMFieldH2 x (Perm_LLVMArray ap) off mb_fp llvmArrayBorrows = [] } , Just fp <- llvmArrayToField sz sub_ap = mbVarsM sub_ap >>>= \mb_sub_ap -> - proveVarLLVMArray x True [Perm_LLVMArray ap] mb_sub_ap >>> + proveVarLLVMArray x [Perm_LLVMArray ap] mb_sub_ap >>> implSimplM Proxy (SImpl_LLVMArrayToField x sub_ap sz) >>> proveVarLLVMFieldH x (Perm_LLVMField fp) off mb_fp @@ -6544,6 +6544,9 @@ proveVarLLVMFieldH2 x p _ mb_fp = -- * Proving LLVM Array Permissions ---------------------------------------------------------------------- +-- FIXME: look over this stuff and make sure there isn't something useful in +-- here before removing it... +{- -- | Search for a permission that _could_ prove a block at an offset in the -- given range findSomeBlock :: forall w. (1 <= w, KnownNat w) => @@ -6654,42 +6657,7 @@ borrowedLLVMArrayForArray lhs rhs = = chopBorrows ((bs_lhs!!bi):bs_skip) (deleteNth bi bs_lhs) bs_rhs | otherwise = bs_skip ++ bs_lhs - --- | TODO: hide the bool parameter -solveForArray :: - (1 <= w, KnownNat w, NuMatchingAny1 r) => - Bool -> - [AtomicPerm (LLVMPointerType w)] -> - Mb vars (LLVMArrayPerm w) -> - ImplM vars s r ps ps () -solveForArray should_fail ps mb_ap = - getPSubst >>>= \psubst -> - case partialSubst psubst mb_ap of - Just _ap -> return () - Nothing - | should_fail -> - implFailM "goo goo" - | otherwise -> - solveForArrayH ps psubst mb_ap - -solveForArrayH :: - (1 <= w, KnownNat w, NuMatchingAny1 r) => - [AtomicPerm (LLVMPointerType w)] -> - PartialSubst vars -> - Mb vars (LLVMArrayPerm w) -> - ImplM vars s r ps ps () -solveForArrayH ps psubst mb_ap - | Nothing <- partialSubst psubst $ mbLLVMArrayLifetime mb_ap - , Just l:_ <- atomicPermLifetime <$> ps = - tryUnifyVars l (mbLLVMArrayLifetime mb_ap) >>> - solveForArray False ps mb_ap -solveForArrayH ps psubst mb_ap - | Nothing <- partialSubst psubst $ mbLLVMArrayRW mb_ap - , Just l:_ <- atomicPermModality <$> ps = - tryUnifyVars l (mbLLVMArrayRW mb_ap) >>> - solveForArray False ps mb_ap -solveForArrayH ps _ mb_ap = - solveForArray True ps mb_ap +-} -- | Prove an LLVM array permission @ap@ from permissions @x:(p1 * ... *pn)@ on @@ -6698,144 +6666,219 @@ solveForArrayH ps _ mb_ap = -- named permissions in the @pi@s. proveVarLLVMArray :: (1 <= w, KnownNat w, NuMatchingAny1 r) => ExprVar (LLVMPointerType w) -> - Bool -> [AtomicPerm (LLVMPointerType w)] -> Mb vars (LLVMArrayPerm w) -> + [AtomicPerm (LLVMPointerType w)] -> Mb vars (LLVMArrayPerm w) -> ImplM vars s r (ps :> LLVMPointerType w) (ps :> LLVMPointerType w) () -proveVarLLVMArray x first_p ps mb_ap = +proveVarLLVMArray x ps mb_ap = implTraceM (\i -> pretty "proveVarLLVMArray:" <+> permPretty i x <> colon <> align (sep [PP.group (permPretty i (ValPerm_Conj ps)), pretty "-o", PP.group (permPretty i mb_ap)])) >>> getPSubst >>>= \psubst -> - proveVarLLVMArrayH x first_p psubst ps mb_ap + proveVarLLVMArrayH x psubst ps mb_ap +-- | The main implementation of 'proveVarLLVMArray'. At a high level, the +-- algorithm chooses one of the ways that an array permission can be proved, +-- which are: +-- +-- 1. From an array permission with the same offset and length; +-- +-- 2. By borrowing or copying a portion of a larger array permission; +-- +-- 3. By constructing a fully borrowed array using 'SImpl_LLVMArrayBorrowed'; or +-- +-- 4. By eliminating a @memblock@ permission with array shape. +-- +-- +-- To determine which case to use, the algorithm searches for a permission +-- currently held on the left that is either an array permission with exactly +-- the required offset and length or that includes them in its range, or is a +-- block permission that that includes the required offset and length in its +-- range. Currently, there are no rules for changing the stride of an array, so +-- arrays with different strides are not considered. If no such permission is +-- found on the left, then a fully borrowed array permission is created, where +-- the borrows are calculated to either line up with the ranges of permissions +-- we already hold on the left, so they can be returned, or to be in the desired +-- output permission, so we do not have to return them. +-- +-- In all of these cases, an array permission with the required offset and +-- length is either found on the left or created, and all cases then reduce to +-- case 1. At this point, the algorithm equalizes the borrows, meaning that it +-- returns any borrows on the left that are not on the right (where the right is +-- the desired output permission) and borrows any borrows on the right that are +-- not on the left. It then adjusts the read/write and lifetime modalities and +-- coerces the cell permissions if necessary. These steps are performed by the +-- helper function 'proveVarLLVMArray_FromArray'. proveVarLLVMArrayH :: (1 <= w, KnownNat w, NuMatchingAny1 r) => ExprVar (LLVMPointerType w) -> - Bool -> PartialSubst vars -> [AtomicPerm (LLVMPointerType w)] -> + PartialSubst vars -> [AtomicPerm (LLVMPointerType w)] -> Mb vars (LLVMArrayPerm w) -> ImplM vars s r (ps :> LLVMPointerType w) (ps :> LLVMPointerType w) () -- Special case: if the length is 0, prove an empty array -proveVarLLVMArrayH x _ psubst ps mb_ap +proveVarLLVMArrayH x psubst ps mb_ap | Just len <- partialSubst psubst $ mbLLVMArrayLen mb_ap , bvIsZero len = recombinePerm x (ValPerm_Conj ps) >>> partialSubstForceM mb_ap "proveVarLLVMArray: incomplete psubst" >>>= \ap -> implLLVMArrayEmpty x ap --- Special case: if we already have a single array permission that covers the --- RHS, then just use (a subset of) that -proveVarLLVMArrayH x _p psubst ps mb_ap +-- If we have a single array permission that covers the RHS, then we are in case +-- 1 or 2, so either use that or borrow or copy a portion of it and proceed to +-- proveVarLLVMArray_FromArray +proveVarLLVMArrayH x psubst ps mb_ap | Just off <- partialSubst psubst $ mbLLVMArrayOffset mb_ap , Just len <- partialSubst psubst $ mbLLVMArrayLen mb_ap , Just lenBytes <- partialSubst psubst $ mbLLVMArrayLenBytes mb_ap - , Just i <- findIndex (containsRHS off lenBytes) ps + , stride <- mbLLVMArrayStride mb_ap + , Just i <- findIndex (suitableAP off lenBytes stride) ps , Perm_LLVMArray ap_lhs <- ps!!i = - implGetConjM x ps i >>>= \ps' -> - recombinePerm x (ValPerm_Conj ps') >>> + implVerbTraceM (\info -> pretty "proveVarLLVMArrayH case 1: using" <+> + permPretty info ap_lhs) >>> + implGetConjM x ps i >>>= \ps' -> + recombinePerm x (ValPerm_Conj ps') >>> - partialSubstForceM (mbLLVMArrayBorrows mb_ap) - "proveVarLLVMArrayH: incomplete array borrows" >>>= \bs -> + partialSubstForceM (mbLLVMArrayBorrows mb_ap) + "proveVarLLVMArrayH: incomplete array borrows" >>>= \bs -> - if bvEq off (llvmArrayOffset ap_lhs) && bvEq len (llvmArrayLen ap_lhs) then - proveVarLLVMArray_FromArray2 x ap_lhs len bs mb_ap >>>= \_ -> - return () - else - implLLVMArrayGet x ap_lhs off len >>>= \ap_lhs' -> - recombinePerm x (ValPerm_LLVMArray ap_lhs') >>> - proveVarLLVMArray_FromArray2 x (llvmMakeSubArray ap_lhs off len) len bs mb_ap >>>= \_ -> - return () + if bvEq off (llvmArrayOffset ap_lhs) && bvEq len (llvmArrayLen ap_lhs) then + proveVarLLVMArray_FromArray x ap_lhs len bs mb_ap >>>= \_ -> + return () + else + implLLVMArrayGet x ap_lhs off len >>>= \ap_lhs' -> + recombinePerm x (ValPerm_LLVMArray ap_lhs') >>> + proveVarLLVMArray_FromArray x (llvmMakeSubArray ap_lhs off len) len bs mb_ap >>>= \_ -> + return () where - containsRHS :: + -- Test if an atomic permission is a "suitable" array permission for the + -- given offset, length, and stride, meaning that it has the required + -- stride, could contain the offset and length, and does not have all of the + -- offset and length borrowed + suitableAP :: (1 <= w, KnownNat w) => - PermExpr (BVType w) -> PermExpr (BVType w) -> AtomicPerm (LLVMPointerType w) -> Bool - containsRHS off len p = - case p of - Perm_LLVMArray ap -> - -- Return `True` if this permission *could* cover the desired off/len - all bvPropCouldHold $ - bvPropRangeSubset (BVRange off len) $ - BVRange (llvmArrayOffset ap) (llvmArrayLengthBytes ap) - _ -> False - --- Check if there's a block with array shape and eliminate it. This new array --- could then be used in the case above, so recurse. -proveVarLLVMArrayH x p psubst ps mb_ap - | Just i <- findIndex arrayBlock ps - , Perm_LLVMBlock bp <- ps !! i - , Just ap <- llvmBlockPermToArray bp = - implExtractSwapConjM x ps i >>> - implElimLLVMBlock x bp >>> - implSwapInsertConjM x (Perm_LLVMArray ap) (deleteNth i ps) i >>> - proveVarLLVMArrayH x p psubst (replaceNth i (Perm_LLVMArray ap) ps) mb_ap - where - arrayBlock (Perm_LLVMBlock bp) - | PExpr_ArrayShape {} <- llvmBlockShape bp = True - arrayBlock _ = False - -proveVarLLVMArrayH x p psubst ps mb_ap - | Just i <- findIndex seqFieldBlock ps = + PermExpr (BVType w) -> PermExpr (BVType w) -> Bytes -> + AtomicPerm (LLVMPointerType w) -> Bool + suitableAP off len stride (Perm_LLVMArray ap) = + -- Test that the strides are equal + llvmArrayStride ap == stride && + -- Make sure the range [off,len) is not fully borrowed + not (llvmArrayRangeIsBorrowed ap (BVRange off len)) && + -- Test if this permission *could* cover the desired off/len + all bvPropCouldHold (bvPropRangeSubset (BVRange off len) + (llvmArrayAbsOffsets ap)) + suitableAP _ _ _ _ = False + +-- Check if there is a block that contains the required offset and length, in +-- which case eliminate it +proveVarLLVMArrayH x psubst ps mb_ap + | Just rng <- partialSubst psubst $ mbLLVMArrayRange mb_ap + , Just i <- findIndex (\p -> isLLVMBlockPerm p && + llvmAtomicPermCouldContainRange rng p) ps = + implVerbTraceM (\info -> pretty "proveVarLLVMArrayH case 2: eliminating" <+> + permPretty info (ps!!i)) >>> implElimAppendIthLLVMBlock x ps i >>>= \ps' -> - proveVarLLVMArrayH x p psubst ps' mb_ap - where - seqFieldBlock (Perm_LLVMBlock bp) - | Just flds <- matchLLVMFieldShapeSeq (llvmBlockShape bp) = length flds > 1 - seqFieldBlock _ = False - --- Otherwise, try and build a completely borrowed array that references existing --- permissions that cover the range of mb_ap, and recurse (hitting the special --- case above). -proveVarLLVMArrayH x first_p psubst ps mb_ap - | Nothing <- partialSubst psubst mb_ap = - solveForArray False ps mb_ap >>> - getPSubst >>>= \psubst' -> - proveVarLLVMArrayH x first_p psubst' ps mb_ap - -proveVarLLVMArrayH x first_p psubst ps mb_ap + proveVarLLVMArray x ps' mb_ap + +-- The following step needs the modalities of mb_ap to be determined, so we do +-- that by finding an arbitrary permission on the left that overlaps with a +-- non-borrowed portion of mb_ap and using it to instantiate the modalities +proveVarLLVMArrayH x psubst ps mb_ap + | Just off <- partialSubst psubst $ mbLLVMArrayOffset mb_ap + , Just lenBytes <- partialSubst psubst $ mbLLVMArrayLenBytes mb_ap + , not (isJust $ partialSubst psubst $ mbLLVMArrayRW mb_ap) || + not (isJust $ partialSubst psubst $ mbLLVMArrayLifetime mb_ap) + , Just p <- find (llvmAtomicPermCouldOverlapRange (BVRange off lenBytes)) ps + , Just rw <- atomicPermModality p + , Just l <- atomicPermLifetime p = + implVerbTraceM (\_ -> pretty "proveVarLLVMArrayH case 3 (unifying vars)") >>> + tryUnifyVars rw (mbLLVMArrayRW mb_ap) >>> + tryUnifyVars l (mbLLVMArrayLifetime mb_ap) >>> + proveVarLLVMArray x ps mb_ap + +-- Otherwise, try and build a completely borrowed array whose borrows are made +-- up of either borrows in the desired output permission mb_ap or are ranges on +-- permissions that we already hold on the left +proveVarLLVMArrayH x psubst ps mb_ap | Just ap <- partialSubst psubst mb_ap - -- NOTE: borrowedLLVMArrayForArray only returns a single possible covering, though - -- there may be multiple. It may be necessary to modify this to return a list, but - -- we'd like to avoid the blowup in branches (see `borrowedLLVMArrayForArray`) - , Just (ps', borrowed) <- borrowedLLVMArrayForArray ps ap - , Just bp_lhs <- findSomeBlock ps' (llvmArrayAbsOffsets ap) = - let bp = bp_lhs { llvmBlockShape = llvmArrayCellShape ap } in - mbVarsM bp >>>= \mb_bp -> - proveVarLLVMBlock x ps mb_bp >>> - implLLVMArrayBorrowed x bp borrowed >>> - recombinePerm x (ValPerm_Conj1 (Perm_LLVMBlock bp)) >>> - -- The recursive call should now hit the case above - proveVarLLVMArrayH x first_p psubst [Perm_LLVMArray borrowed] mb_ap - -proveVarLLVMArrayH x _ _ ps mb_ap = - -- TODO: Review this note? - -- Because we told implGetLLVMPermForOffset to eliminate block perms, there - -- should be no other cases that will work here, so fail + , len <- llvmArrayLen ap + , lhs_cells@(lhs_cell_rng:_) <- mapMaybe (permCells ap) ps + , rhs_cells <- map llvmArrayBorrowCells (llvmArrayBorrows ap) + , Just cells <- gatherCoveringRanges (llvmArrayCells ap) (lhs_cells ++ + rhs_cells) + , bs <- map cellRangeToBorrow cells + , ap_borrowed <- ap { llvmArrayBorrows = bs } + , cell_bp <- blockForCell ap (bvRangeOffset lhs_cell_rng) = + implVerbTraceM (\i -> hang 2 $ + sep [pretty "proveVarLLVMArrayH case 4", + pretty "cell ranges = " <> permPretty i cells, + pretty "bp = " <> permPretty i cell_bp]) >>> + mbVarsM cell_bp >>>= \mb_cell_bp -> + proveVarLLVMBlock x ps mb_cell_bp >>> + implLLVMArrayBorrowed x cell_bp ap_borrowed >>> + recombinePerm x (ValPerm_Conj1 (Perm_LLVMBlock cell_bp)) >>> + proveVarLLVMArray_FromArray x ap_borrowed len (llvmArrayBorrows ap) mb_ap >>>= \_ -> + return () + where + -- Comupte the range of array cells in ap that an atomic permission + -- corresponds to, if any, as long as it is not wholly borrowed + permCells :: (1 <= w, KnownNat w) => LLVMArrayPerm w -> + AtomicPerm (LLVMPointerType w) -> Maybe (BVRange w) + permCells ap p = permOffsets p >>= llvmArrayAbsOffsetsToCells ap + + -- Compute the range of offsets in an atomic permission, if any, using the + -- whole range of an array permission iff it is not fully borrowed + permOffsets :: (1 <= w, KnownNat w) => AtomicPerm (LLVMPointerType w) -> + Maybe (BVRange w) + permOffsets (Perm_LLVMArray ap) | llvmArrayIsBorrowed ap = Nothing + permOffsets (Perm_LLVMArray ap) = Just $ llvmArrayRange ap + permOffsets p = llvmAtomicPermRange p + + -- Convert a range to a borrow + cellRangeToBorrow :: (1 <= w, KnownNat w) => BVRange w -> LLVMArrayBorrow w + cellRangeToBorrow (BVRange cell (bvMatchConstInt -> Just 1)) = + FieldBorrow cell + cellRangeToBorrow rng = RangeBorrow rng + + -- Create a block permission for a cell in an array + blockForCell :: (1 <= w, KnownNat w) => LLVMArrayPerm w -> + PermExpr (BVType w) -> LLVMBlockPerm w + blockForCell ap cell = + LLVMBlockPerm { llvmBlockRW = llvmArrayRW ap, + llvmBlockLifetime = llvmArrayLifetime ap, + llvmBlockOffset = llvmArrayCellToAbsOffset ap cell, + llvmBlockLen = bvInt (toInteger $ llvmArrayStride ap), + llvmBlockShape = llvmArrayCellShape ap } + +-- If we get here, then there is no covering of the offsets needed for mb_ap, so +-- there is no possible way we could prove mb_ap, and thus we fail +proveVarLLVMArrayH x _ ps mb_ap = implFailVarM "proveVarLLVMArrayH" x (ValPerm_Conj ps) (mbValPerm_LLVMArray mb_ap) + -- | Prove an array permission @mb_ap@ with borrows set to the supplied list and -- length set to that of @ap_lhs@ using the array permission @ap_lhs@ on top of -- the stack, assuming that @ap_lhs@ has the same offset and stride as @ap@. -- Return the resulting array permission that was proved. -proveVarLLVMArray_FromArray2 :: +proveVarLLVMArray_FromArray :: (1 <= w, KnownNat w, NuMatchingAny1 r) => ExprVar (LLVMPointerType w) -> LLVMArrayPerm w -> PermExpr (BVType w) -> [LLVMArrayBorrow w] -> Mb vars (LLVMArrayPerm w) -> ImplM vars s r (ps :> LLVMPointerType w) (ps :> LLVMPointerType w) (LLVMArrayPerm w) -proveVarLLVMArray_FromArray2 x ap_lhs len bs mb_ap = +proveVarLLVMArray_FromArray x ap_lhs len bs mb_ap = implTraceM (\info -> - pretty "proveVarLLVMArray_FromArray2:" <+> + pretty "proveVarLLVMArray_FromArray:" <+> permPretty info x <> colon <> align (sep [permPretty info (ValPerm_LLVMArray ap_lhs), pretty "-o", PP.group (permPretty info mb_ap)])) >>> - proveVarLLVMArray_FromArray2H x ap_lhs len bs mb_ap + proveVarLLVMArray_FromArrayH x ap_lhs len bs mb_ap --- | The implementation of 'proveVarLLVMArray_FromArray2' -proveVarLLVMArray_FromArray2H :: +-- | The implementation of 'proveVarLLVMArray_FromArray' +proveVarLLVMArray_FromArrayH :: (1 <= w, KnownNat w, NuMatchingAny1 r) => ExprVar (LLVMPointerType w) -> LLVMArrayPerm w -> PermExpr (BVType w) -> [LLVMArrayBorrow w] -> Mb vars (LLVMArrayPerm w) -> @@ -6847,12 +6890,12 @@ proveVarLLVMArray_FromArray2H :: -- FIXME: when an array ap_ret is being borrowed from ap_lhs, this code requires -- all of it to be returned, with no borrows, even though it could be that ap -- allows some of ap_ret to be borrowed -proveVarLLVMArray_FromArray2H x ap_lhs len bs mb_ap +proveVarLLVMArray_FromArrayH x ap_lhs len bs mb_ap | Just b <- find (flip notElem bs) (llvmArrayBorrows ap_lhs) = -- Find a borrow on the rhs that overlaps b and subtract the overlapped part -- Prove the rest of ap with b borrowed - proveVarLLVMArray_FromArray2 x ap_lhs len (b:bs) mb_ap >>>= \ap' -> + proveVarLLVMArray_FromArray x ap_lhs len (b:bs) mb_ap >>>= \ap' -> -- Prove the borrowed perm let p = permForLLVMArrayBorrow ap' b in @@ -6868,11 +6911,11 @@ proveVarLLVMArray_FromArray2H x ap_lhs len bs mb_ap -- If there is a borrow in ap that is not in ap_lhs, borrow it from ap_lhs. Note -- the assymmetry with the previous case: we only add borrows if we definitely -- have to, but we remove borrows if we might have to. -proveVarLLVMArray_FromArray2H x ap_lhs len bs mb_ap +proveVarLLVMArray_FromArrayH x ap_lhs len bs mb_ap | Just b <- find (flip notElem (llvmArrayBorrows ap_lhs)) bs = -- Prove the rest of ap without b borrowed - proveVarLLVMArray_FromArray2 x ap_lhs len (delete b bs) mb_ap >>>= \ap' -> + proveVarLLVMArray_FromArray x ap_lhs len (delete b bs) mb_ap >>>= \ap' -> -- Borrow the permission if that is possible; this will fail if ap has a -- borrow that is not actually in its range. Note that the borrow is always @@ -6885,7 +6928,7 @@ proveVarLLVMArray_FromArray2H x ap_lhs len bs mb_ap -- If we get here then ap_lhs and ap have the same borrows, offset, length, and -- stride, so equalize their modalities, prove the shape of mb_ap from that of -- ap_lhs, rearrange their borrows, and we are done -proveVarLLVMArray_FromArray2H x ap_lhs _ bs mb_ap = +proveVarLLVMArray_FromArrayH x ap_lhs _ bs mb_ap = -- Coerce the rw modality of ap_lhs to that of mb_ap, if possibe equalizeRWs x (\rw -> ValPerm_LLVMArray $ ap_lhs { llvmArrayRW = rw }) (llvmArrayRW ap_lhs) (mbLLVMArrayRW mb_ap) @@ -8075,7 +8118,7 @@ proveVarAtomicImpl x ps mb_p = case mbMatch mb_p of [nuMP| Perm_LLVMField mb_fp |] -> partialSubstForceM (mbLLVMFieldOffset mb_fp) "proveVarPtrPerms" >>>= \off -> proveVarLLVMField x ps off mb_fp - [nuMP| Perm_LLVMArray mb_ap |] -> proveVarLLVMArray x True ps mb_ap + [nuMP| Perm_LLVMArray mb_ap |] -> proveVarLLVMArray x ps mb_ap [nuMP| Perm_LLVMBlock mb_bp |] -> proveVarLLVMBlock x ps mb_bp [nuMP| Perm_LLVMFree mb_e |] -> diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs index c537d85a8e..9d9a159569 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs @@ -2659,6 +2659,11 @@ mbLLVMArrayLen = mbMapCl $(mkClosed [| llvmArrayLen |]) mbLLVMArrayLenBytes :: (1 <= w, KnownNat w) => Mb ctx (LLVMArrayPerm w) -> Mb ctx (PermExpr (BVType w)) mbLLVMArrayLenBytes = mbMapCl $(mkClosed [| llvmArrayLengthBytes |]) +-- | Get the range of offsets of an array permission in binding +mbLLVMArrayRange :: (1 <= w, KnownNat w) => Mb ctx (LLVMArrayPerm w) -> + Mb ctx (BVRange w) +mbLLVMArrayRange = mbMapCl $(mkClosed [| llvmArrayRange |]) + -- | Get the stride of an array permission in binding mbLLVMArrayStride :: Mb ctx (LLVMArrayPerm w) -> Bytes mbLLVMArrayStride = mbLift . mbMapCl $(mkClosed [| llvmArrayStride |]) @@ -4957,6 +4962,15 @@ llvmArrayCellsToOffsets :: (1 <= w, KnownNat w) => LLVMArrayPerm w -> llvmArrayCellsToOffsets ap (BVRange cell num_cells) = BVRange (llvmArrayCellToOffset ap cell) (llvmArrayCellToOffset ap num_cells) +-- | Convert a range of absolute byte offsets to a range of cell numbers in an +-- array permission, if possible +llvmArrayAbsOffsetsToCells :: (1 <= w, KnownNat w) => LLVMArrayPerm w -> + BVRange w -> Maybe (BVRange w) +llvmArrayAbsOffsetsToCells ap rng + | Just cell <- matchLLVMArrayCell ap (bvRangeOffset rng) = + Just $ BVRange cell (bvDiv (bvRangeLength rng) (llvmArrayStride ap)) +llvmArrayAbsOffsetsToCells _ _ = Nothing + -- | Return the clopen range @[0,len)@ of the cells of an array permission llvmArrayCells :: (1 <= w, KnownNat w) => LLVMArrayPerm w -> BVRange w llvmArrayCells ap = BVRange (bvInt 0) (llvmArrayLen ap) @@ -5031,18 +5045,27 @@ permToLLVMArrayBorrow ap p = _ -> Nothing +-- | Get the range of offsets spanned by a borrow relative to the start of an +-- array permission llvmArrayBorrowRange :: (1 <= w, KnownNat w) => LLVMArrayPerm w -> LLVMArrayBorrow w -> BVRange w llvmArrayBorrowRange ap borrow = llvmArrayCellsToOffsets ap (llvmArrayBorrowCells borrow) +-- | Get the "absolute" range of offsets spanned by a borrow relative to the +-- pointer with this array permission llvmArrayAbsBorrowRange :: (1 <= w, KnownNat w) => - LLVMArrayPerm w -> LLVMArrayBorrow w -> BVRange w + LLVMArrayPerm w -> LLVMArrayBorrow w -> BVRange w llvmArrayAbsBorrowRange ap borrow = range { bvRangeOffset = bvAdd (llvmArrayOffset ap) (bvRangeOffset range) } where range = llvmArrayCellsToOffsets ap (llvmArrayBorrowCells borrow) +-- | Get the absolute offset at which an array borrow starts +llvmArrayBorrowAbsOffset :: (1 <= w, KnownNat w) => LLVMArrayPerm w -> + LLVMArrayBorrow w -> PermExpr (BVType w) +llvmArrayBorrowAbsOffset ap b = bvRangeOffset $ llvmArrayAbsBorrowRange ap b + -- | Add a borrow to an 'LLVMArrayPerm' llvmArrayAddBorrow :: LLVMArrayBorrow w -> LLVMArrayPerm w -> LLVMArrayPerm w llvmArrayAddBorrow b ap = ap { llvmArrayBorrows = b : llvmArrayBorrows ap } @@ -5119,6 +5142,8 @@ llvmArrayBorrowCells :: (KnownNat w, 1 <= w) => LLVMArrayBorrow w -> BVRange w llvmArrayBorrowCells (FieldBorrow idx) = bvRangeOfIndex idx llvmArrayBorrowCells (RangeBorrow r) = r +-- FIXME: delete? not used, and should be implementable via bvRangeDelete +{- -- | Given a borrow @borrow@ and range (of borrowed indices) @rng@, -- delete @rng@ from @borrow@, and return the borrows that describe -- the remaining borrowed cells. @@ -5139,27 +5164,43 @@ llvmArrayBorrowRangeDelete borrow rng = , bvEq (bvRangeLength new_range) (bvInt 1) = Just $ FieldBorrow idx | otherwise = error "llvmArrayBorrowRangeDelete: found non unit new_range for FieldBorrow" +-} --- | Return whether or not the borrows in @ap@ cover the range of cells [0, len). Specifically, --- if the borrowed cells (as ranges) can be arranged in as a sequence of non-overlapping but contiguous --- ranges (in the sense of @bvCouldEqual@) that extends at least as far as @len@ (in the sense of @bvLeq@) -llvmArrayIsBorrowed :: - (HasCallStack, 1 <= w, KnownNat w) => - LLVMArrayPerm w -> - Bool +-- | Take in a range @rng@ and a list of ranges @rngs@ and try to find a +-- sequence of non-overlapping but contiguous ranges in @rngs@ that covers the +-- desired range @rng@ +gatherCoveringRanges :: (1 <= w, KnownNat w) => BVRange w -> [BVRange w] -> + Maybe [BVRange w] +gatherCoveringRanges rng _ | bvIsZero (bvRangeLength rng) = Just [] +gatherCoveringRanges rng rngs + | off <- bvRangeOffset rng + , Just i <- findIndex (bvEq off . bvRangeOffset) rngs + , rng' <- rngs!!i = + -- If rng' covers all of rng, then we are done + if bvRangeSubset rng rng' then Just [rng'] else + (rng' :) <$> + gatherCoveringRanges (bvRangeSuffix (bvAdd off (bvRangeLength rng')) rng) + (deleteNth i rngs) +gatherCoveringRanges _ _ = Nothing + +-- | Test if the borrows in @ap@ cover a given range of offsets. That is, test +-- if the ranges of the borrows in @ap@ can be arranged as a sequence of +-- non-overlapping but contiguous ranges that extends at least as far as @len@ +-- (in the sense of @bvLeq@). +llvmArrayRangeIsBorrowed :: (HasCallStack, 1 <= w, KnownNat w) => + LLVMArrayPerm w -> BVRange w -> Bool +llvmArrayRangeIsBorrowed ap rng = + isJust $ gatherCoveringRanges rng $ + map (llvmArrayBorrowAbsOffsets ap) (llvmArrayBorrows ap) + +-- | Test whether the borrows in @ap@ cover the range of cells @[0, len)@. That +-- is, test if the ranges of the borrows in @ap@ can be arranged as a sequence +-- of non-overlapping but contiguous ranges that extends at least as far as +-- @len@ (in the sense of @bvLeq@) +llvmArrayIsBorrowed :: (HasCallStack, 1 <= w, KnownNat w) => LLVMArrayPerm w -> + Bool llvmArrayIsBorrowed ap = - go (bvInt 0) (llvmArrayBorrowCells <$> llvmArrayBorrows ap) - where - end = bvRangeEnd (llvmArrayCells ap) - - go off borrows - | bvLeq end off - = True - | Just i <- findIndex (permForOff off) borrows - = go (bvAdd off (bvRangeLength (borrows!!i))) (deleteNth i borrows) - go _ _ = False - - permForOff o b = bvCouldEqual o (bvRangeOffset b) + llvmArrayRangeIsBorrowed ap (llvmArrayAbsOffsets ap) -- | Test if a byte offset @o@ statically aligns with a statically-known offset -- into some array cell, i.e., whether @@ -5367,23 +5408,42 @@ llvmPermContainsOffsetBool :: (1 <= w, KnownNat w) => PermExpr (BVType w) -> llvmPermContainsOffsetBool off p = maybe False snd $ llvmPermContainsOffset off p --- | Test if an atomic LLVM permission contains (in the sense of 'bvPropHolds') --- all offsets in a given range -llvmAtomicPermContainsRange :: (1 <= w, KnownNat w) => BVRange w -> - AtomicPerm (LLVMPointerType w) -> Bool -llvmAtomicPermContainsRange rng (Perm_LLVMArray ap) +-- | Build the propositions stating that an atomic LLVM permission contains all +-- offsets in a given range +llvmAtomicPermContainsRangeProps :: (1 <= w, KnownNat w) => BVRange w -> + AtomicPerm (LLVMPointerType w) -> + Maybe [BVProp w] +llvmAtomicPermContainsRangeProps rng (Perm_LLVMArray ap) | Just ix1 <- matchLLVMArrayIndex ap (bvRangeOffset rng) , Just ix2 <- matchLLVMArrayIndex ap (bvRangeEnd rng) , props <- llvmArrayBorrowInArray ap (RangeBorrow $ BVRange (llvmArrayIndexCell ix1) (llvmArrayIndexCell ix2)) = + Just props +llvmAtomicPermContainsRangeProps rng (Perm_LLVMField fp) = + Just $ bvPropRangeSubset rng (llvmFieldRange fp) +llvmAtomicPermContainsRangeProps rng (Perm_LLVMBlock bp) = + Just $ bvPropRangeSubset rng (llvmBlockRange bp) +llvmAtomicPermContainsRangeProps _ _ = Nothing + +-- | Test if an atomic LLVM permission contains (in the sense of 'bvPropHolds') +-- all offsets in a given range +llvmAtomicPermContainsRange :: (1 <= w, KnownNat w) => BVRange w -> + AtomicPerm (LLVMPointerType w) -> Bool +llvmAtomicPermContainsRange rng p + | Just props <- llvmAtomicPermContainsRangeProps rng p = all bvPropHolds props -llvmAtomicPermContainsRange rng (Perm_LLVMField fp) = - bvRangeSubset rng (llvmFieldRange fp) -llvmAtomicPermContainsRange rng (Perm_LLVMBlock bp) = - bvRangeSubset rng (llvmBlockRange bp) llvmAtomicPermContainsRange _ _ = False +-- | Test if an atomic LLVM permission could contain (in the sense of +-- 'bvPropCouldHold') all offsets in a given range +llvmAtomicPermCouldContainRange :: (1 <= w, KnownNat w) => BVRange w -> + AtomicPerm (LLVMPointerType w) -> Bool +llvmAtomicPermCouldContainRange rng p + | Just props <- llvmAtomicPermContainsRangeProps rng p = + all bvPropCouldHold props +llvmAtomicPermCouldContainRange _ _ = False + -- | Test if an atomic LLVM permission has a range that overlaps with (in the -- sense of 'bvPropHolds') the offsets in a given range llvmAtomicPermOverlapsRange :: (1 <= w, KnownNat w) => BVRange w -> @@ -5437,7 +5497,7 @@ llvmArrayToBlocks _ = Nothing llvmArrayBorrowOffsets :: (1 <= w, KnownNat w) => LLVMArrayPerm w -> LLVMArrayBorrow w -> BVRange w llvmArrayBorrowOffsets ap (FieldBorrow ix) = - bvRangeOfIndex $ llvmArrayCellToOffset ap ix + BVRange (llvmArrayCellToOffset ap ix) (bvInt $ toInteger $ llvmArrayStride ap) llvmArrayBorrowOffsets ap (RangeBorrow r) = llvmArrayCellsToOffsets ap r -- | Get the range of byte offsets represented by an array borrow relative to From 84e55ff09f0ac00140b8ff777fab95905d1eefcf Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Thu, 5 May 2022 16:49:47 -0700 Subject: [PATCH 4/8] fixed gatherCoveringRanges to find coverings that start before the beginning of the supplied range; fixed llvmMakeSubArray to correctly offset the borrows in the array it returns --- heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs index 9d9a159569..e86d937293 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs @@ -5129,7 +5129,7 @@ llvmArrayBorrowsPermuteTo ap bs = -- | Add a cell offset to an 'LLVMArrayBorrow', meaning we change the borrow to -- be relative to an array with that many more cells added to the front cellOffsetLLVMArrayBorrow :: (1 <= w, KnownNat w) => PermExpr (BVType w) -> - LLVMArrayBorrow w -> LLVMArrayBorrow w + LLVMArrayBorrow w -> LLVMArrayBorrow w cellOffsetLLVMArrayBorrow off (FieldBorrow ix) = FieldBorrow (bvAdd ix off) cellOffsetLLVMArrayBorrow off (RangeBorrow rng) = @@ -5173,13 +5173,12 @@ gatherCoveringRanges :: (1 <= w, KnownNat w) => BVRange w -> [BVRange w] -> Maybe [BVRange w] gatherCoveringRanges rng _ | bvIsZero (bvRangeLength rng) = Just [] gatherCoveringRanges rng rngs - | off <- bvRangeOffset rng - , Just i <- findIndex (bvEq off . bvRangeOffset) rngs + | Just i <- findIndex (bvInRange (bvRangeOffset rng)) rngs , rng' <- rngs!!i = -- If rng' covers all of rng, then we are done if bvRangeSubset rng rng' then Just [rng'] else (rng' :) <$> - gatherCoveringRanges (bvRangeSuffix (bvAdd off (bvRangeLength rng')) rng) + gatherCoveringRanges (bvRangeSuffix (bvRangeEnd rng') rng) (deleteNth i rngs) gatherCoveringRanges _ _ = Nothing @@ -5369,6 +5368,7 @@ llvmMakeSubArray ap off len , cell_rng <- BVRange cell len = ap { llvmArrayOffset = off, llvmArrayLen = len, llvmArrayBorrows = + map (cellOffsetLLVMArrayBorrow (bvNegate cell)) $ filter (not . all bvPropHolds . llvmArrayBorrowsDisjoint (RangeBorrow cell_rng)) $ llvmArrayBorrows ap } From 58f0e4bddb64009fe2ec9d4e668bb4769e5adca4 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Thu, 5 May 2022 16:50:36 -0700 Subject: [PATCH 5/8] removed debug statements from arrays.saw --- heapster-saw/examples/arrays.saw | 2 -- 1 file changed, 2 deletions(-) diff --git a/heapster-saw/examples/arrays.saw b/heapster-saw/examples/arrays.saw index c7d23e1462..4a9bb1d0cf 100644 --- a/heapster-saw/examples/arrays.saw +++ b/heapster-saw/examples/arrays.saw @@ -62,8 +62,6 @@ heapster_typecheck_fun env "even_odd_sums_diff" "(l:bv 64). arg0:array(W,0,<2*l,*8,fieldsh(int64<>)), arg1:eq(llvmword(2*l)) -o \ \ arg0:array(W,0,<2*l,*8,fieldsh(int64<>)), arg1:true, ret:int64<>"; -heapster_set_debug_level env 2; heapster_typecheck_fun env "alloc_sum_array_test" "(). empty -o ret:int64<>"; -heapster_set_debug_level env 0; heapster_export_coq env "arrays_gen.v"; From b4f0704cc9ca4f8532026a855d6e62701a267b59 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Thu, 5 May 2022 16:51:24 -0700 Subject: [PATCH 6/8] changed the Sum data type to have a repr(u64) attribute --- heapster-saw/examples/rust_data.bc | Bin 277472 -> 277360 bytes heapster-saw/examples/rust_data.rs | 2 +- 2 files changed, 1 insertion(+), 1 deletion(-) diff --git a/heapster-saw/examples/rust_data.bc b/heapster-saw/examples/rust_data.bc index 80a74acce427992ed8480b2cdbf9da44135af51a..6c66093e95ceda75aea28e2758ca1be5a4ce2744 100644 GIT binary patch delta 59313 zcmce;30PCt)-Zfd5;75z0AZd^Aj}|P5KvGPq6mT(sq+{pB2I|bc}l{JVvTGRtV4rE ztJbzSqqUjeh8T5GR)2aT_U z9lr`K?&|H#F}OtVnzY&CJ^c9Q>GSaYn=g3K^rH_w_2#MwseLx~JTAs6!!>r2!fKyu zI)ULOvRBeN$D`U@Nz%|nBlGsRiQflYS44HlBdh39r)wkIHLi{HA@z#E)wP4j@3gM( zRk;229G51In?%f6sau!CAiBR5X%-0;$@ItN)H2e9*YjWKb-SEcd(ofSY4lQk_d+top zN$hbCfvTd|nCfm9Tt&`t9K1PK(iGchWWJY`J2*9ev_x$F($Yhs@eo;g2$eQrCG@0t zAHhiJh4}Q{=UZLcDx6=+1dSCg?Q+3Oz38so^|sg$HK{LkdnNkBVtuE&QOzl!5cDq~QN|K|t>H03VcuR1+#?p?}@iMb6__YHy*|y_i zg17mmIt2xi=*z*zwgI%X7R;J;STsC$^sE#r93l$_bFlM+L`NN#%*b*|t*onBW}S z5;Z4#y|_imdQX{M8S?&s;@YTs1*tx#>CsJ=iovIIqR1OsbQAR*wZ#PTbTN^Q^ub4C zBK34P^cBNjsd4L+J3d!hc?!q#TJsOApjoHcoGP-sskUiYZ&{*b-EK&nCFTE22=41x ztD5+&gy5$n{&V<_nYRo1Pi2CioA{MN{!1Z$jhfOWJyV$^SSDl5F|s)2MLg6RCK=I* zSv)fE+tn6&o$F&Y|EgY4(zHd|c$5n$Ua0x^2*J-;f~TehFu^JvYaccKg^=H&XORj@ zB1MsABN;1Zc}1Wcvq+a-jn~nK#Th2D1M;&JlS;G}k@SjQrD1dNMk@{X30Qx?;M3%m-$TDw97Hf*OV6hKtC|DDTo3y2j z;27JhF>|;1R+z2yDOhaG>E2zjpw8AKts<}u-f@g!=YbI%iCt*5#wwmTRj$F}<7l_e z2{Q?qRf%jx@HwwGForbE%iVZN{yqIVinf)B(lFDsluh*$Mxl8(GL zsoaQ8PY$f~`#Iru?MPTj6P)MNCRa-&8s-O#hzt$)17=``n6t#*qwSt~sl7+iJ@cdX zp&6~_@w)T&H7bjlz+`)HdRDF7V)^E6b4)s{rAPMi30mv`T!oZYG&G8~WJiJXs>hu> zaR18M=q9?G$w_s}txB}4Q^l4U*$xf7mFL(~nt6-Pv!@i&SDxohDO6ao!_u2-(o1B! z!HL|{G6IEjK<6&8By#h#kGHj>?+F4OA21+^;KV1GV!J6svwe*D_V{euxbXa@80Qk5+3t;2l9auLHdj-? zC7`kX)-EvPPSb*7nRQE2X0bLmvI*YvB9j&_F?xmmf(FF7jH;v!Db0zlkBI~)TuOJ- z{R8J*6*Cz8b~El$sd1}}F=r6^(d$C3U6IRR=g|tkCdHuo{~nJ7kBrwD%MBJaMRbdA z*_lGR&FsDC&;$Y%4qTxEk75X4;`~81J}4e`?Xc`ZaE&8dc5zUQ6{gI8P$=fKIfqK* zym+F$Jk=sKE<1iq%vEp}by~*mkHl;uAC%(Y2aLc%P1OesTA}9X2l)eGQk~2D)i4Q@ zS=C4FtT>P(4LuKN z5*L?9GBi&W8;M|G`t=pTli7OQm`O{&By7FWx`dK5~Zh`_(COMpKMcp*)s!nsRtLiyae-F^IUB*ydW-!kE}58c`4LHLh$0yl2P3 zdv;c#Vz`4x(s{*8acCND?N=e(CN}>viL~djDmXx3hy%Z(Py7%)X4ofaxi7(^>REj}mEa{IcxdGRNO~>vuJ7Oi_1uS2 z!AmM$$JdX|iW>Sv2vDVoom(`{cPm`dHLf)fJHc-# zUE4KeWNpXE5L-iiCqtarnGA-6=zNNELyGHz3Q?Qf6@o6rH!wo{0xy$&)h;gXI>RGF z6E{xck(3>`L^37Yp+zfk-&{gQ^%dFWX^g;V&5pF(fM|^_jS(UAP*fFFh3p#Q`Anyoc;5gxd1_Q4e=ydA`mw1o^gfu!F(-<$8gNTaxMwgP7l3LkpI5P3Q$x)i41gL7-6b>!S= zm4O?`+$w9wkjDSCG*{ACx3RV>?Dx{=+=sxP z6@b!8?7h(a=zdIqN*gn%ToHMl9@RwmBS`{JrQkjvz6#{}>u}CJN)(tx^EQng@%W)z zJRx%sb5^^{w~0A_#?dSr7?TObHiJc~kS=ZzX2vC#lnh@VlItYZa1w=|HewhJQ#;Sf zmw?n6zKVko4C83=4eU$|8{5Fk1j<$Q$+20A688J)`oj1U*~eg2i{(2)YQ6s0%y?dE z$%cK{;vkJtOSJont5|`;{lyqNP`kfa#t9T2DAt+>Y7aE(%wVr3&B`AwBsgt;erk?# z#39F6VX`KD7Bix0JvPoiv?X@}rkm=}>UDJYG$8lrZks0!42EuogGz2*S~1fBx1OR? zI^e>Yx)g^L!AxB$jLg)1;Gn^#=+Ybv5{7P;gJuFlm%dGd0pCL|vL_SRh>JXU$1|p+ z*N+%bBD)bn_w?D!IJMOhlVJ^8!7wT%SB@7OnJbe{fO!N;G-rUGHg`MG0PqW>BsN~; zsWJ%++czz?BiFlqS~>`%ME20VxLj=h(-gZy7kTqwq<(sS7Tp)*kzFQ+BwGb~33ygy zi-rezDC?}#fo5ImF#?h|A>)+*z-Vgk}lNy*z6Fpde% z68zUD2bIL{Ah@sfte%NKV}cj(h!C`b6QgK3476nN??W~x6+F}lCf+x))@cg|N^s1A z&}^%*peK+rV1(8YiyGOJ<1AJ-isrGe z4lC&hqTNcI6@nstWoT)l8!Gd4L8mSK!@3g~PuX(g7JVCV=$#eup`T|Am(ShGP6TDVcx1ND{!{2N>)3Ci8Vh z7AV1*xHRzI^=%5t_6q@MAMrU_7%W7BkZ3DNjv?-8F954ZT#yuQJrp&JRjImMM`V3% zR11~ZH)Th+wFWMh!6lH4P zvjXN9Z?nAF5tO~n@@Pj;$u{2>?Z*;H>&)Sy9`oue;3yh? zRH_VA+~qCigQ*q-fw(8PZU+b`rk2dOpj z?;H6qrGh#3Q#^`eM~3D*X}yk0U_xow`;t~S(vM}#DfL!VSIhyi4BFTME=Lv!(PE#2 z!6NC?{SY%o|2EP}wQp{0T+FrhxnLF7!73U)wk*L0-gf-=1$Jh;n(Oq(=G-Bcw?K$VkBb^XU)H3&mmB_m8m!nk(kgC2KBVM;CUv_*iwxY%9iCjR z0%6B(CIx7 zx(e5pR@bWrmwE{1M!UJ)PuEq5Iv}uj6~-=CwTw%K*Sj(#mpwd~~L?5CoSRyP~ zl~u4hjdf zV7NX@^0R75t8(1wONCIe`MANMX>!lFPp>(+oBO>UY2~vtz52rF!?Mr8!Vk;72(5EG z3>jwAPsPUkfTYJfjl~w|YJ`2gO|Nu@uqNitzfP60iNg|WJWonQS%Thf z_!xA6crx>4w1S<3G2&<=zGK(uoko8LDI)3fZiFhJnlU@I%kr?!s^P9oZP`*afTes1W7r+^oiExkJO(KRfkaU2sZ^mS9o%wKizj|-tX7TlK# z`pjnhYLRn$WW9dR5cljAnmqT)Fo+d3MCaJBq}R@VtH_bzy1HP(YH244F*TL=8Nu7$niGZ6$uY6m}_Q$Wc>0i94y~WNFo@fxOAT zG-ptg!m6``QS&`CB*+dH5|~L;WOKmC0;ha1iT^+*h&Lv9$EiY>9!U~B(X&kN-Tebf zFk~a4TS9v7eI@^;mT~5wrZeLG(ErdC1BW!T{#|rZ*5V#4em&nn;yw5}H(_yJSMXg| zu%g)`3B6;zI`l~mTI1=4>rhs5fZ27rYbTC&C;3l;ve6_0kU*tgoh#d2mni60Q^Vup zny6}U=$fE-9Val$YmV)s3bJDbjTGouH4zqXWn^cn!2q_vSrbnin6+1mg2oX}T`dw> zPFM#W%zEOa0!fD_=cRsIjS`*axH&#balI;cYcL4Fs?u9sZdW*$KtmykG5ZZl^dq3l zl4eaG2I^Lxw>$%kL++B19lEU+jUFwt`H$O+c8~VTy5 z;ZvLF%m2spt)%d!MOshn-4Ev;*`F1%vM7LzzXvew!2G`lSWIEa`g;JA%$NK zioXXiNqNoR11zI3sQ(_oB-h-(2UtO2DC`H|*jG>{NfyVwzdNY0l!bQKxzW|kImn3! z5P~z@LkOM&hJ%{Y$ZOll>@ncK$sVC=V~#uiC*x(O-bXz}ap{u!a1e zDCTx#6iUj6L#NBDC5(?H<$9hI5YsL?#%&DUQ%iQ#(4#>@6gYTT1!l5z*rk3x@~>&8L{EYM*c;|B4dABMrnA2w>ukVNw|Zp9AH z5VCz0in-LJxHie1+ge?o8eG7aKS*(ggPn#}=SO1aHY(pu?-~)AMmo{x$kCP%3zwxh zLr3dDg)20;WH=fVnHU7~jgU{`t~K!9Y6lNY-E$cKwGZ@pjQ^&>?yVZhgZ+i@Y(|O; z#KPfPSKsxaOVP6-{S@mB>}rXv18N>>!NI7#e5+8QjnUoe^hbpZorOD-I{n#1pl8v( z=9D@WsrG3@7XU(UHllf;;j?IISXhskWhkt9^z+Cbdg@R zqX=z^_O>X@8ANLJJ-3FoL}&CS%F8^)xrwrfKbyQz(NI60j#BH+g298VzcmR!z*$Bb zM%}QN7f{DgKl5rzng6Ir>Y>8bM8!rE6?~xLc^4I>q0`a9Va~iBla*-3pwTjdl4*jK zk77Ss26v>1dU8rD#-mT*j+AK$qan#3X@(ITQl{~=S?ycUGZ|q{N>ri=5nbHohZe@T znv+IaB6IloexeQPkh_@dG+xKMv3T!#v`Fs4q0Cg0l%Gj0OUjd6_9VG1B~NnM>6g<` zh0N95Bu|+A%VM-pE;c7+NiJO$IvKcdqohgBHte{7R>)krCTYU*j_8TpokI$eq&pbd z$B4}-LBhfx4MONWKrUpFVg%Yt8_@!IPKuFSe3of(ZXHgF5f&eaGUe_Tqy)*ex25T} zokxZ+0vUY#1v1+jDE}ajgVIRs+>YKPNAgX2JWv}}#0hORkSSmtRGG)PNu zM^b4ba+4}ma0(|Y$SP+o>4ZbMf|+X8GIqftvYN|TYtLG?qG07dDDDb^)j8|h&4zX4 zh$6F(4np=l{ORF99XhS@s8afnT>79~cqcos0Zrr?&mcY7avcDf_{(g!N*Ska^qX%J zPxU$Iyx)ZEMuw?6WCHTAQ!01`XOSJ|Pr+Gs@P8%y^<+n^LrZqG$VQlqES$g(9y9Wx zkN+@>|1^o;MsUfa$146hE$vQIM1f`DI9=A|;k|9L{~dYIKfqo@mXTV9i4%-0-ztk^A9_XD7c7T8q%>i12Dxv`dbhq{Cc#>{g0+Htn%Ao*gc&(#q)&(| zSgA9ezZyK-cZS}tA){YFc~6(z5Lrr(sv~Gj z(kK#r*Qd2WkUZQ?F||&dpSQv<0?5w7ByrdGQF2#cuT6}H7E#MGP5m^aOA5CF#V0#$ z3M)eT-fr(pAMQ;eYb`W%)G+g|0&B^4+rC7Oqum*B!gCZ(qJ2>#Z-`jPeN1&>$cy|>wty~BW3 zpP}>>Iu_ae$SQy~!b~txFh%kfx(cj``@meuqwnYrdN@W8gM%t~WBrnA!IVovJ zyLI-o?E3hR=W=IAx1dQ0Ey=5tbxi^5g24*g7HC_FUD`EZZ!Qlsu5B3K)XaFRM{^QF znA-Om+7pj=*^N81%KR5K>l^fpXHWbOCUiA+_QwTC;Ogc?g`4H};BDv-kJk9GNdF_u zTdrpfMe)p`O!6lk9du+jI*277y8qMA&8Du@VA|Z-4LJPjT`QB|5Rzw!}O?%>%?t?$gpriC5@DP5D zldFh^=9ferGs=CS!glxpD|g>5rTMWjJdaPuUa4m=G${-pyCdr-&c`Evx2(kN=f}C@ zgqe|-O*9+ha4lvo)G+^>L+LxnI z?&M|o74+L=Z`=cUO!1&iKa1j~e24Rq{nUBlyfIp4MwQ`V4i=|2Bg{TEFCgHQIOhje z*BZ-F<^tb3=Q^mB*bo6GbBTh#)(}r5E5>?`k^RuRiyOx)sv}s#unPuqhv}3d} zpP(btL-7ab$LV8eW9m@E3~#&u&79$gd!tn|oW(o0naxo%opvl?s~MB9Wa;36=2x*h z#(fG*qNi!Iuk1u8W_VgY_l={EYc^JQkG7&GfT#9|&CFLc+Np1j@KY~as*J7}76}bo z=>NjSmR8m%6oLnIOwGbDf*Ql{{Bh4SbTMl&EDHu0)F7ePjtbg1ai0Lg_!y=(0W$29 z_w3V{zXDtUC8P$`nBqXzz$xNk7?uPBG-^<&jJtoFIp8r1n}snkIP;?}8gGAM^FF!| z#|QvpQ)4o<_=c;~VwpRJ#lb)im2+o%2ohltPG2h17qn>BW0=&mK7a$22ToWFQzHEm zkxB|k&H9k#H$Eap9&6$r9$`yq7%=d~X`B^C!(@FS4}23b$pDa2fFdCQi85|!Hp`_A zh_vlX|F0czFpXnIfa;|`%Js7j4=f#1!bBiVJs8J;)yL2Gu&TbSau*85uRtf4`pCp%FsvPB_YiyRD$Dsg$O<-F z2IFu61;4&A(xY*;0q#g*)fg%4wQlot-blR6T4na`vn{9GcI&+{DbPal0UHd|rT(T6 zy@e6@MJEAcaDlo!Rh82AVR|Lpk-#!?Bj)lq4-(p7m>vcQc)DLm3^*T-5$BmvSo@|GN^wj89k!BEI@t4Y}hL2a4v6i{{T+gwLqv#B_y z2SmN{-E${ySQ{7P&4xir?{QM^r;dE1oCxg07OUX_T(IVq=)j4EJ`7WjXyl_e+gk9`$Z3Vo`_E}u4$#=U zwsv%fdIqL!0(epj2vTLYoQQX9Hph6drVPe_Wzd4Uh$}g7u>M+LBk-Q5Mq5|-&@|s5 z{fcOnY$m2ucC$f=u60#5_fHz8aH8;#2w^+8k5Lxe0kdy`K>}W|G*BttSE;DS^u~Uy zCXdW>j%8x`5dhVreOu=FEl~zxQgT0l8|~#XYCP8U}EZS3IG!zP4Hja6oN#nd{iBPyABY`V3uwSY_`I0?8HtY z9mC4IgeKcbY33haQs`y<(BEEd!af*gll)QGZT|3Is|B=8U1(txHtSK=!<;QRrURdg zk=qKCD&ssIH<=GAhttz#_xFt8>~?YgS|31J6o2r5W{@Hrqu8NF0jDY z!`|nvg$UP2P1BwALnY zKj86$XC$6S3`(v3mF_x$g{jBGNUx|n!w(w=qeW}21I?OY|N4<`b9J;|J?tp>nm(l8 z$edrX1RYu{3OEXD^b`5|7N=w#(E1W45b%NvXwCS(GW!X71{1PCz54C+4VS@tby0uW z=_|ozEhu=MD4+vY-vd~B1!uD~!?64>f;;enYeb9IiTs6b7#0TNAeW|O`mpL#ZW|qw z^^@uP9WE24sA`=kkoE@lw@ZdFflM!o11?f& z2a1!FNU0X7vdzID`eU17V`XL!!3`1=%1li8%{KuOZU_TYcjGZB?fU6)q6`qxRDkUx zsaoNHgB%P4BbC7exWM{uIxIGGqG85>VS1wcY1AgD1C$>)xnbM}D*`wQf5xO;&cq;_@yNBRwuKrUr1G2e@>Xhi;O4-8uY zh1>4EHtL_A<~rle~o&rPSjekF3(h zqOsZ5fjI+VU1u03mj_uW<7RD0b~$Q^VXfpXHAp57TT0VgH=@niqJTvpQZnlFEbljF zPeeHoTHlXQqu)1j7jy+CJOWuPh6z2(Z+SRsxpX9GAn37-T7lffHxpCyqL5{djsF^0 zVNkyn_If5kzDoXij@kqdKJ(o1;oRM5Y>tg;6bDn2JJ7Sh_^%SGvPQwKb}e91`~%0! zlI2_A4}8EE^`g0TwvBs`(LcNPOWyH^9w3!nkXVVfS6PY&R!^LKk zXqXaQeXkVHeQNDiZ-rriK?dVprZ;WpIL%f_5c=ayjoM!mi2QQ>0@`54&j8*l_p)8e ziZWQMAI-o2DltEc)VU&@jke_asp>%h{j}|mxK_hDOfLnWLg^)y7avaGdNzXXtb)NF zQEmAo`9t*>a76v~;@*~z>7a{LSnW}a5y!_3t+K|jSN#Zd-TRzo*okC$BHO2+5<}r( zk7hKS_th%V+`M77*n1de-$e|pF0FiX@qnNWoz3%^tM$e(AYKhm;ew6*VxAfQCHMnK z4tnKq|{1nZ{_U1AD%rG_7 zlob0WA9mn9bBjqxP+${S4XXP&JR{L`cE-_4n|mzOk;ZK4nO`}_Srj-<1bHe zYX?XWwG4pa0z<63oou#C1?x)4dukMrp1Zr%uk&5d$1TZuA@4$(J>TkQgmsC2gx)wY z&X5ntKmpYhPEx>EjC;6B2r6+f(z6u}c3%y{RQ~U1#V>81+*AN1eN_+Wqllof1V9>L zkboCl;A>M>6=hF`#bJjq_<#!(&hcLfBJ%fq{SxN!w`T0dCSaHzz+@C8DS*qbtjtu$ zfGyI{djzoMyqymeVWdQRL9f21<^5)Y>M^PDQ)cS)fRu#lS$@>d=Avd;9-s&qhYJXu zv+hYY6mIyjp7(n1iK3kh*&QQtoO(4<3J_^iHxeHGB>`inStw*z;#jVnriSx0iritl(ODBK&b#)x|gRE zEW>Y!IpT!|K38 zuQeUH{D#bq)j%q60vE6_@a|-{N<$vyV2k2!U7N-OwvDS-6QWpi(ee+%&1kF06akI)aj zLzc~jd8>#C7^*F{QW;@aAc1O}C(xCR)~d(AE%}?&ULCN%3(ww>%dBs=Q&{>#&bZr1oQBM! zpH>&WOlSV^uB?yVZPWo|KUv?uz1=~l0^b|ZZ}~R>nht@ZAJT`N;pX!|Lj5wd1OGlT zIWh>kS1_Ldp5X%TqdQw6U-ho=e~$=@1IT_NH4r124~M-=>EO1@#5cW^nqt%w_vOro zy^viU5XqnwN+jMSqR}Ryh)q7U?A0h`lh3fCSu`^&w{dQwZ z)=2XXRHd~EFhW*d4v2cpb<3pX2g$5l50sEAzy*x8eElJ-6Ft+40_yEBUI?sCNr&{z zeoa5iG-ohndG`vGXV&PvS-+y-&7%4GAk03aiwO`PY;eHC``PQjGegdX0VY5NanSF* zpKV{7WBJgk?Gq+GSyinEVw(FAlX267Bc!Way-3>NMUYM|uhuoP86DaTZWoAwzum*s z@CZg-fMukWHe4FAREwT%7O7}OIHv6)rYm_~_q~E+O@F8Ru=Jyu zzB+phgRXQRYdik-rR*Hk$lySz6=4bcHj`J5YIkU1-Pn0hCS_H6U`qHIlMJqkuPlXXDSs_qSV7A1BNf->&LWn~pBoQdhd!}pTU{lXv<+(e%sn}BMlA^SPw70$euWQgkLN@o3} z#JGcz5!nPT1C2b?m(&|SE}egSZJ@NO?t;n=WeVu3iJSXxQh@|KV;A4lny@Rh3bB2&06?5%L&v}YNJwv z-z$fZEQ4uqf#EzI%DZdmY}14`_GvL;GMn zZ+Pt`SO|orrq&|0&iTe6`$FapUU{JCy?pc_)k94WYj}*cuqe~|8${W(T8Ffgm{dgU`Yk87{c6LF&iwPABC~& zct+iK7?#nOLYL%AzuW5#pWvpZNDqaMe+C!kj6=a&Z6<%td{=)(7YNZb3yfI}E0Pqd zsRS~rG7A48l9w>h{uw5w0KZI$P)0eDvloocYb>z*WEkxs zaQsOmcP5**WE$QbN?a6v+r8<7gc0vjxbHpY@+6d0W;?ZS$D+&UyKKcHwSZ}HUsnCL z2hbNu0nvkgo6$L$c~6~*VU7JZW63dIr~Kc@P$sg^IRzbSu*qItpZ^e2&RT|^l=-SE zaxvw;?hT_{=gCzL&6;=3V}092wV=fUQ-jYV02N$h+@8tYBLf*!1DP^vkTif%O*|!j z7qp`rElAEj`NnPsUClgD18@z!lsG?%5AC3@q^k`UFieV_AjN)cdpf~?gbtO1EBgjh zb~_I0*}049NvxNkGk~ZkBpoOZr$_0~$Zc~~%}y8(LTm3czvc*f6nPli&kJlbI&^5x zKp5yJ8LM-l+JbLr>Iz9;az>QRZeqQKCBZ}XYJuO-?~H;@P*X7WUM)bTM z-2_uXbkvWbLNi2Hrv&vOcxK$Oo3lGutIe?5eiV=T<~vOED;LY}NAZ@AKf!$-L;1C) zFU5XKhtbE%24VJZ`cXVz#jI2!>+R$1vRA*81p5uUq8GIw)%JPzI^e0ZA5ThWi+cHe zMBCw~x@wLwyVZ!2LUcLvB=$Zg?LH*}5rY~%3bt7Gm(4fZKBvhX(z^cVdEuk!GYaAS z@{fL``fg{g)Gvlq0@#v)bl?KC!_6Wrp6lO*z}mfR2T+x<-b z84TBfqwO`*rBPD{>T^!gX*zJ&y)v{pGgr@A&SI$N!6<_QCUd8P8#=*rKARLRK@F07aq1v* zdDC(kcDf(isZ%U|HU6x|)P31@PCj(pu|wXD<3=E`2QT;B4ZSE92|lq2D0LNLhx-zL zpkyNbi^poLob*Pf3&i*PX~(3`P|_zhs$>CMeH+GmWU%Fr&*i?AfaX{~G{dIlWK9}E zVDtNlR(X=SxM`IPYw1UO+J_cK<1cDV-503@R<)5uxhTH(lW)Rj$i zT*9zWOC$Q^kTdPgE%eQys6cwBnLZ;1EB0c`S>GG4kC@JL5*lQf%bMB`?5``NtIcUMLWV{HiIPBI3*Wvj7NOW~0ru86kx4YDX#G?y|&5_jJ>8d0D?et%c z)Np{QdaDHvRxwC_v@b2)d<6}vjTUR92}zAs!WYc{8y@w?yzp7*$7A|lQolNGFhUBykwnFQPB2S0XeprJRoE{2)xq0xk zqIcO>r=tR~vzYy8w)zS~+-`K@A6ITjp}X6&bvX-Vw__Z_iEIs)&dE)zJ0TLPmvo?+ z-{_s1hRwGoWPctWA_F<5Ni^EcjF40%MzEPFXz&?#yckVC(+KZ=XXnBD*0Yn`9(g-f zhI4(37Zz9)>h0A-i&JFgsm*G3FU9RPEej*(A#BxI|{{k`;ME_-- z3f>2t+W_yU&V{>G{I=l4_rk`!5*!b=radmiOI%^oW|g_dXzj)%|9}MNXW+$0GS45v z&B~ASIAf8dUW;_!jzhv0o3eo}Gy#%cU@@sjc$wuS+!`faU`oU&IY(IR#n5MD3mdH% z9!w^dt;}+(bY~o4)D+5bP-8V(bzx4~dmc2d_ouO3hqi@Lf8-kj3d!AK6Rg0;U>tfg z{N+I2@F|sMX7R*Y3nXd?!ppZd;qIQmV$URfKt4?J>7I1j3>O|^9+pQ6(WVA({1rOU zkR-V&rOW=T8m-2DzxXRgMypUuK=D~Dw^9P0!5(90%bSt^MFLMji5JC+56WD5N3;B1 z-}&gQxN5^}&?YV|F4jB>j7lZP)>{iI-R&g_HJKE0;ms{1(rw_!ASZIXvrKwpv zSnO;=Gpf2c6C8rDabiII#FLEJ-~?gYp|elkIMI&ThY)%%x!NUIc9+gD=pO48Y^{eK z#qo878e_a)E{ysUWRZI&Uo3!L^p8>H zr65K*=@wO&y;XmJR+CCqEjE3c?qS`mch~**LN>lQO|BlDjYXxZPlGh%xAF>vKJg)V z3tul@u|Yzo&G%z8ThiNx$b`IxFQaqybF8k`@STL38A5eF9b7S)GcB7>yglye#P}C3 zy2?OnFZ=e;VB$H{^8bGt%#rjvf5)B;Z7sT_#TMTyDJYxW&@cAWI(`0p!;GcK^D8tjc%zBuqBka?jwEiMMV{>~$?pG%KkBDd>y z>DY~PVcjm>p{Of(#W#(j6=CR`E6(^Nbhs&n*0~wkT#3c^p=no~t#da+Qw1*H6{#b6 z+~=5FT7@=T83UlVuf+2bLufMNb`Uk0V+38b#kDB*>NNX)1jtry?j``8y6VUc37LA$ z8DqPjPeOOEPO*D=-s@J_`88@{H}AL2ZqXJoZbYFp=OlXX+5p<`9Y}S}nU=3bJFkgt zV!Xa;RI>9e*x_upa;th&xX_raMAxoG<5@^}orrE0ZR8okMnZJkZK1pob1sYpSPxq$ zw+u5>;Re>vme@+xJu(&u*}8?P`kWWSJh+jX(dwhMX#Vve7GVmYM|NM&!+rK0=Vizy zO=S)u_690kgg3St1nhYirQFw?kTJDGMCVrxc<0Zo1IcdZ5gk!L;w|QN_(5 zi+fYKY*{RCeFsPjL;t=R0vVL>Uv4U*;?^i5Da=qy4`_Ss-&~Vex4#HJV;pxiTjpd( zgCbA59G!h77XqgcLbh&UT2eF3A=u{;n7ID_RgbQCTJ9-)6U$@`Xi2Tp?E{sem(AOx z3=?Cq*15{9%DB(ecUFcomX0OGt{2LFyhSwU!M;yt@bH&7|H|~lowF5cyA{Ep3g-Bd zT^2Dj#sOrNQ08WoJv5sEBZe7|&w=aoVKl7_XRpy%fKkO@D{U5xty1!kPpeuP>Be zAwz_6;9x_5AtW{FC|Ec?>EDUc1ii$wOSMnoX!b1^YepuM)xu*}owQVrk2pUFd_IHONKr`9-NwGB%RA`H2%&65|MB$s=BkGD@@5+-0XDQq1*_yT<-4psTX%7 zJ9@s1t--WeXj#ipf67QHj*XB&kapVr3EqXe@BR!!-?!MQDChqn<@}%7E;Kp+tU5CV zIR7vUdtK1*xq7OwnW?JT>Xtkp>#}v z$B^(VS!s5D);8cEs=Qd*zsLIKOtrZ9j`9Kk@}4- z5Js{K$tWd{ctlPmXfR?_66(pcT%+15EhmdW5qHCdsSWA#>+9y%*Jmoz8kEYpXzks> zs+M|-+?f%}a_)V*w$jVxv7v11`=jlh?%bKQvDs;c!{p-PCMQ>pwGGGSf~C!c;;FZ$ zH(E?dyj5(mt=z)lmPK)*121v(<^+csj{k17kkrIr7Qb||F+7<1%K~gFGY8TWUho2k z7BzhNtZF!E$QYJFnEtb4Yew1A-*9f3jzMEMY%lGrF^fj%YMFIHHf9llrhgxWFG1VB zUm&E!pR^$d#2-ym|E@u{#-*gzSp_4l5fphlI%M=WkIVbwqsiG~4kvRH`q4PwnT({= zl|oRz%g3zAOlY$kn9^>vuyvRNsA;7a*OV$%EjuFTfuh6GoCx%7t7=f`!l>8z>Of(P zR375<{j%p4hN(x*EaRal7_knbec`C-oFk0kG57C`IU_EoQWiEXZvUD)7m(^+8XppW z1_+=OykA%X10A}vzROJ1Ka8Qn9CYOeTmOd4=v?*WtAoBzS5t9~*BjTO1Y-5B=%ZDz z8dZWItF{p&h6XD%tu4lX15`lY3w0wlk9>U`Eo5J(1^Vb2;QZ>rzo^IG^eguyVtK`H z!2Z?fLfZ^-=0z(MaNnJ8vQ09|u`#mdM+3b|J$vm5qMM9cdE4Ni{ z70a_%=HPE>T^<_>q7~2GgYqp3LC^Wf_@lQ2v%_576$JQaG|$b?l6IlN26rN&-HYYb zRp*Uv-^BzUI8QbXJ!?-InzXD{%($@G3=g*>Gw|nB1|H!WQzh|Wj#R3y4W5v{>tSWrbi$gGa`^d+?-R(F>NT6b@>Fj(#6)B=0B&Njg z>vuoVdp|kG%7czIHBp)Vd5YljFWI#L8Z844XZ2D#5(Fzf!l;D;z#Z0pP#SZ-3fC~8 zYax@k>-Xp-=&PTkR!W<1pllZ|E`dPI!x#qQF?#lsFMb|5JuZfDyzjAxT`po<*7UF` zEw*?50XA2N?mb?VKoSk)E&!(=3)U1{2=Y74nQm4WAlGWJG8)ph=Bu%shs^4X4a#b9 zmbtWimN1{#Xo^)-Oz0dY z`F%pScg~$)RPpp_mtj@iQKGb;{k!fY9Y*}&5wmB0xbw@K?zI7OX=+kA88^Q<#tu#( zV4pl_*-9l!cwR_@?Yi;YhaomRu|)WbXqs^b8ur445m5b2Hd4L_V0e)av@ed3MOTU} zu`KvHZikdFgPdPJ=!f~F39~baS$*X5mpt6{e_A`}C>s5I7>az#L&UFxoSUX@;8C?& z3aO1Su`a+MHC6Nv(dbvp(c@o7{BJ-XF}3lrSo=)W`f9j?Y~jEVP>@;+d z{@`kd`B|Zaey@|TCr>*v;_YCZ3o7OYapRG?92NaOfYzRXPX0dE^pSwF{)oa~qJw|H z53bSqKiqI5dho{_yb2}#Nhnq}XX-UjV~`P#DuF6VVM}8oi@X(cHDjcgAnz@d z&?h|{Bi-l@b9`#+Uyc)r>H=_7(z%sJ)AF~{@vr_fd7tL}Ka!X6`~OH@(f=EHdzSvc zk*ApR`hO(v_tF1cdT~tLt?WZHJi?ED?BktjRH1@F0dRZNb^@A@AE}}FxPCG%=c8#_ z%N*KJsJvE;DywJWAA;mz?gRn-=z%`d?v#DO#2xU4vTvFA61-?D8?aAh;r{%&Hc?;| z!6u(}tgMuU&!ZlX;%5x(^W;R?BsTe^td5N*xb55W7_^q=ex?Y>@f#-#C^+HTzni`vk*>UAmu3gnnQD#a%n77&5XJRtq8P_ zy~Gl`CV>i@7Ca-wn)o(AE~jBJ%*pD>`L*l^7X6Y7Tw_l5Zm8rUUov1T6vXyWTq~Q# zb@gS-ZgTN+_`b3o=C~iuDErnNueBL7HF!zOadA6IzzQ+h03!+cgok^phBxT00|~t4 zmYA;)eyXPb$e#EaqH5BzAH<9eU2gdFw{{pK68w6j>p#bRz06=q;bvRm5qN2t%nG-~ zeaa?U;c4vM&~|}EmXy_6;lot>g_*2YVao_`P9ie+Oq#PX>uYua5d^KFdt|>vKk8ua zo%l$`>doLF<4FfOVXk*eW{tRg!>nfYBpR*Uv#KPab(x57m`S=dYtpT4xywEAc@{h7 z2QZmkq{$p)My3kQ-lpZ_hQ;Lf5* z##dLM12LVV`ILcw;-@Tj>JLug#2Jbr_+M)>e^j*!8)NN(vlJnPYH>&HlcCPpx9xLM z=&3vtQT*&`mqJCB(<}(krE&_}ZG-TH`6Bk>A9%22s7XxGKKGWn^9`Am5D7LjDHiv$ zMz&&O25$yljyT9)uHR6*l-}8+z5M zoyx65z1k{@%+N&8zf&fa32bp0ID;fx+{>;Tg0Sm_(7%7W%+eMg3NXrvxTA3Bi!n8% zJ}SvJiQz(F*%&)~aGBH&=L@3g@AZ9D);bZ7Dl4?Zou|}GJjlQaI&z9?@AiIHbSdV$ zpX!YADL%#a!U1F&ncNYYAZ!fbk@*aJg(WD=xkC9fGUZ-d_JdQrV8}&C-7=JXMCQ?DbL{b}WEnFX z1P6b06@hEYRyyDbKI#QeeT#J7<(~G?NppbAxg&T|JRHPLW`4>}=VV*bQ%R@&>!)Rp z9q`p80>N0k9|GBej(?88%7lQDm#L_qU$)W{caf7FPVYlc^z_jeZdy%v8FYs}jcoe( ztUsOxe_8oVO8r(4^Jk2n6g>ZSRgAIFM)9qUQ}zNylgT`dW&iTTgE-GT91oCgGPO+L zh1+qCNKCiJvLG+qn_E&%en2WX91aHO;doP+XGns&GPlmuGEV1MeS8$^A}-WL z>Q`$%y}8OhKQ8>T8ZyHZd4QQ7BAjUUZiHGNtp(p#GGa}+x?m>T})>!(q`%M z_7I%3at|At-)DZi4oBYC72Vku$#^X0&S5c{MZJo%vz(3l?TEPvRq6|M?-9V}BH_Lm zzr+vKEVlck^W33QGuAfNdo54v%4~gbH@v+p+y@^*JY5>DkS>&}XTm8rb$SHJS{32$ z4v~q<+{(_n;tnjTO*^==?0Z*y7_E3$8R3R|L_ZkQw#59QxmAm+L0rCh3ADb_92wA< z<>Vx;eYD<|#>Iqt2TfxzEQ9Nfp69a7?`mc{)GK+}VXWUDm#N(F(D^y%j4rFh!gNmc z9KJIyuj7R*Kk(Uy91%h>D7eQ;QWfDq6K#(W_qS(EipwA%NcYe&2iF`@X+_UZ2P3kaPCg zXU}`B&-$#jE2jnOl-(RvhkYGyuXD5%%{{NuFQ}aMNT>FuUk>*k;N0lNA>q$VT6A8j z>{$1ceI&QnmD)ivwIL)c=>o~F(PS+&*;|^dD1)X8qv>2Aox-G`a=T17HW+S3z|Cq` zxY+_Xr!l(laxD*Do{8b*fXuY$rJH2O0AhMdZ!V%Y2f$5!15bsOL^&%G5aVA2UZ*sJCzK9+)@<^%#*mZDavHU@>R810H(C#$Q;ra&)7 zMWs5c<=*paRgdVy9;CtteMT8k=YdBh_d!zG#~IH4D8m-|&f4F0(hP$$J2FJBkYOu* z=!L2@&Att_P80I&U7++-Jk^Q!5wJ5R; z`;{;K6#He~Zq;JHq|_I6$J}G20p6Fl*ex>2nr;B~eclTzHt>eZL^1pWrS83o4E)1- ziB1mBrkmgePTxPwDnL}dOXX~35#jk6Tme`iD7%qN_5+pGhot!-5A9}GxyuiEBP)=0 zrpd-c^Lt8m!%pCJc^xt4?J{ZYlAw0d0OVlC0@C5L2Z-dX>6-SOnoJEqJ{ej$>`skBb!v5{*#g!C z6;|ugcZE||P_VO~7K}zZ^`IBvPMFX{EHhFrVFRYN|}V zm`CM3g)x{PSFZxpJW22tZv#QY*1Bw+`(pc0bQ2cR`}B0i25uRQ4HS9EVwg%!Y$2LbxbY`iwQ2nIkH z9RMI)-gO3*!_#zB9asViFzpf^R)*@ka3h`;Wcqf6hjYo(K4`Qa%*oThOWWj%$-F*D zI<)f#O74vkb!qzmYHa-I1J(2c?#`MIbm{m&_C)xAoPJ$9zz{g;ZJO^%ekjtZS7hFqD=gmg^rDQORfS#1{vebH=qYgwLiTKa{UE=(VgEvY{UATj9-90xn;$5RlKyBw2S6~rKk~>} z?~%Ckp6FORK;Zv);=H5g`4Vp}K%fkFTXu7QATOmIAQ%=A-L&tNV|hD3kg)p6z4_jT z)swUUfqcymmX+!A1TXJt0fG&+HC1-YLn>G*DP58p%6grC7Hb=lb-V;_viZ?RwroD0eOhkFfw`oDxpgDJkS+i z3_#;iIvFBEpV=x|eHO5^WuRlW3j0~nfs@G+47!oyGGsGU^<+NqDIBeQpMthRq2i~1 zi(qj(W|JY%8wB=$CgTTUAF7Y0WMT(C!GY8S(n#p;wndp(8$GL zfC^<9wsZyQMlD5G!Eq4yIkndx$H|z@4;c{o3(($V&|=*_Ssd;r=~rqO2l7^qg7jWS z4I50U5n)}3EEr{EQ1zX)EcP(YNvN=PhmGYc%{3=ma}{l^o>?X}MFsplxiv#`4EdVh zmwhzX((Fu4y1i}b8Msbx8@de)3{KT8K8k?~a{Zm3DE$S+{+mQaeDTnL;=BajN!wi_ z5$PX-^u!-w-!9f$wb(aNgdnr-2PdVcJx)#P(Ws6OWrk&TsA(_qMFp9}81-`Rz|2T# z2Hih>+s`iCwT<|#I050Z)I35$%nKffo54n@6q%#h4* zvNjYsA`YnxMGmGd^Lu}*7oycmzpXg^Y$kaeiu~cZ{Xk@kxltr&APTc>-rw7BPSeHH zj#A@Eb-=LtPS(MeBg%oup0{`2QEO5&5P5ZJ~d^ zm|Pf)+>NRJ5ZP$2%u)q_ia~ddE@8-Cchky*a@s{D#5)XG=w(jbT1va7G@c9(L$Zvm zsrL#?9&%(NtEF#cduFwfVH%l8A(rHF;;dbV$wa<-b~cvNM0hDjeBZmyNRaITJs0^k;$TW_|JYBszYerEoP+Z*`_D(v@2$O{eE5O<- zOeqU)X*R1JZ9Ltoe%?{rd`ZA<$yI1p++pBPH+ED)lyrY!CU!Cc9TgknzUA37M4;_9 zpSyPEt82=j)do+hHm?jB#Ic{>@S~J>*VrCDL1~6*%?Q|qSKVd<5*&JW{ITUVqGl*v zk0G*88Y9~t!nndVQ4Q2}ViSR^GWHuq+@N#%6UAStw*R%g)k<6Jw*#I9C_uf5f(6N= zAC6e)@+{wXh|1MXq&Q&IG2JJv7i4;r1=j@IR34Zoc<5{njLUdHwY4OqqyEPDvxM9- z9hT|X+P@3rnR$SlUl`kUDTVw@W zjP=MlRu?JBB#{a+K_H@KJBUmPZy55$%4Z~C7+{CxByAXSn5cYMPY2=G&ej^s7^PLH zE_OEuGc|yPARlIBzE!R^23w>V2hc}bHK32O{$J+^&v;cA5GDKskiQK>DUuXd>+RzJxYAykgkmb=)~|&tjQ4tyHyo^Js=j3JaAeby z`?_$u2C@?d0AyG0*(k@s@nZqDi{S?A>VeFjW(rdDu~@rl>y%<&H?YWXBgy;W$d0lH zi0ud@@sfQ}^H@J#x0uK6?gc{uQ1*pTtA=G0V_<>y8zO1oFaXR~Q6uRwk}v`V_Ez?P zlEdHcJER4m$V7l5BR_i-!bhvB_nz}Y08^L9BRS6eQyU?d=CQw(Kra3oV85*L#t5(h zP!o8HYz%o8iTtHdF(s`SXKUunQmLu$XK>x#ab2YczhPqUH`H9`k&z>jtT36vM*zQpOe3G2tMcXflN?&`)EbMM2f7yi0?zV*~~sKKX%R&mj_57qHzE%TdVDQu5`^7jC>b8LU8` z)214<2`bq%m5dmLyxA6IMxp)~eMMBG09k!h**Xe^B8wf}b?n5KK~#FffFiI{HZ+<) zUgAMUjX_?+p`UlO_4l7%wX9jEt{U6Mr@uA#0q&(kv4Yf(LH+?;lXq+51m)v#Os%Q} z`kyPdv2vXylYuO9P|1N*eP9eW?rA#fe~ym9b;evS zrC45@zNv;OaaBM!3~%p-C!~5Tvd)P7D%qO*1DHbEzmejU4ZjPtzrRZH;QE!g76E!n z%b@rw#V>n&){I&;EbhYQU3q*kG%MqEJ?u2KV7_R0ER5IPr~UNc%?*+gSJfb)Az-hv zEs1r42CxonbSUwCyYZn2qa_{^{=`g(HYwBjQUrd{OA!y{lguP+>g+ZLUJf6 zB6H#2zvdyj{s7EW*L%oY!j$-W%qVdStq%8@o z8_<)$q7^e_;CR%ZR|tA8*%*Z+=GshTg&mo=kz?c00FaE{k4KkGRm+B(gB+F=A}el# zh-=C13CIO3Biv|IhFeyWUD3!%`sx7eV=W>TXjOqcS-44EK_<%v}E zM$%OyiLQv~H1Np-c(Gy!VTIvL#;fkO(T z!x~&!HD67BnS#6r!IsZTWhLu7OJz{px&)qV@=HqSrOfn2`jcRgDrzO;=^(u}uiL$E zVU){YRrm>31rC{_Kw?YZGtZK3@rfcoN7atbQp!pNvc%cnlAQ`PoL>K~Kz)VR!dLW{ zinE&O4odpR0PI~wCdVKPaeC9fGmecb0;sT)&^epsG008&5#y|c`%>~HtB?ZyOqu<% z4it0N@+&*rN5j>uu56A$Ty}BX4T~fAS=kW5RAdAn6Hf&Ru9?WDqI9D+_BWGoPy>CO zn~Fw(q0%l6&fn&y)|B42$%1*mfja_ZAHDhCmS$t$q8WxTb!y!j2XAT@cHsCB-Y0Hb zN!tg_)b8(J#UWsMlcqR8yOl(58gk0e>3jGxiIc!mXq$B_i6y4?ZUIz$hoW0=Ypz}` z@Kh;;zBBTx3_U)e_IWm0L4xe@{71SwXgcFvik*FfVd^HV9X2%|EiOr&1<#c_160frDNR5~eWr=~5905e6vEy=7jyS+2y)t$-Yzh9qNk zy!d&Zyc+*5TNp{Q`P0;hG+Cw?xV^9%W|>!njH{Mj$m}L5h|}r2>xzA(gzq;D105tG z_gTSMX`SY^Z_S@xi&(xJJ=+;kh2M2 z=Qpw>9$5@388KexOaCU(F@d<=uS9OeV?~^qk#(kj}yzH#a#C|&R1Uq!ZbY!PB zxmPAmN4a<`$S*b^zr3XKOKC-Dblw=SK!kV#2$N;8JOQ2_f}8xwaPy=O+?3m{OE{lo z82a6`gnYpKYfr+i^lJhRQ;mfI zyw4H;fG|_!@+$WNr*KGhu^>DaHp8|p=)_DE0dzQ`KMSm~GSYVzaufrdRxK(YWCe;( z@C@h$t*k^+;iXT|Y^Qq)xRXX}(GO~ot%0GSvPwPBClYd9iRT>DEufFM;579E2tA>> zQYCI42pF-E>{9ive3Tz0U`kv;tZDJ_?dcK*OX92Jq;L*$@p`u^c+=o60oewLV07(d zJG-?|P<_8Fn7NSGp^=drbCAv8SxE(NvbKV58?bP;(Mi>BI#VKLlpLqoFt(2XOTC8e zS^dSUVUfT-(=PvG-$RY-3J@@s1bk=GHxa4$6^DchP{h$()DNYS0drAs#`~)8zYIyT z1mA&?l#rRUU8n9@hHcg{DqT8L)!)-so@mr8dO8qHaV}K#pSa67`JE(R=>yc0SY03n zs3R^G-PG^R%eV}ae;CDpK3i1Kw4}~aumW7D(x@rF%0y^(xZkP}sWtUir65DncCj@1 zol{1>(tii!LkR}z2*0G}H-ikTXHe$`b82y38_zlW>`U9MYgJGjPqsLhWvg#G_vYTdo(f;+rA8c}G|Aq43t4wzMxwe&?324EO=ey;0e0(VDrV6MY_t z-VdUP=^RlPTFZfRWR*Je5FhcY4hauK2N@?LC*k@y9@DO}4oF7*W3N!%LHu%qcggnfHT#*mL1W8GkIscVMuBAM)5Ei@UmUN zmMasv^DC3h9U;|LhT~@fYZCco0g@V2T>lN6kj}vJzgn2QZa%Vfk24=|65#po2XTg` zwCDn2FAJ$Ki#wCAwZ#_;xf;VQkwHoLNyvV)ILm^6UIqC=)X&i0+4=zWEDV(xb99Qy@`b3ssauGj?7^GShMALXLF+He zJNIlSxwQ~kW&~TU&h)66q{5!X2A9;(@3rFF{28fFqkJ_r++{YUz*)zW>O) zIMumldtfqG)NK`>W!B#OtT%6OsdXq76wQ7EL9r!duS>m2Ihs@KXjPS*?wK#?74#B5 zo%G<%I72k2j^E+;@Ltp%{2pdx$fnAyRwJ*<6Ul<)lfpV7q-Gwx`OFZ_ee_XkA4r`b zn+1t8y(-Tn3u;ap)EPkHq6crH4AH`ZE}gUP4T-1AQfSWID=#GruADTiGlay-2XDq3 zqV)2P#2MoEqP~ziUY1U??q2z0vf$oHqdFr?qS{T2!seip=m}$BsT?vDuR{@L3epA0NIzrBJ<*y`e$csvx0ne z{dCV235yPYC<#$@TNE4$YKz7VXF%;|HC|}2ryNS`SJ^E^5PZtD&J{`=`S4AgA=*`- z*SW+qpu{#8cu?Z{rsEk;h-rLIWQ%?N4{j-;;hA4 zP~z!{bD_jb_kL93boD0t`*=9}j)%Vkf5-SgXSRbPDJn~VAqibMu`~sQM zlsIX|GFa~<0?8kE!_BV<^98atOM3Vw-cWwHjyeT~@`}pt)<3&I_I-h@%=kSjeNqJ1 z9(cnJp>k%18pJ0~AvfV2^Www()`zrsFQ(YrEE(sq^|_`k^+az8XxVj5OX?k!qybh> z93){j8N?+HcqnSr{~mTRxxGmCLmmrFjmn1Yx8k4y+at}(X3(eZBH6t>-%86A!5h~p z^qXb^$>$-gU)?uy5Ei0-<@;6|r3l_n>j_U~76M6nHrxG@`#!J=N%eU}Co)P||F)m# zhUQfrQgSo9H_w@C1CLwa@jb`-XVtb@tF6{UGjO`#u$K+gtGGH5HdnOn0jhs?!WI|r zS^-ZLU2xssI1gdiW}Z`mShZcKke`rBt+K3kH%u? zCg=2an9xYSYy@(UYIXnA!~IA|QjccZ$UWqo84gF9wwx!K8PNV!O-s%@s@K1wja(sN znv5nUo_IhiGLV(IQFP)r4@5aD(rJrEi)2{^u-1^<^eq9qM%Bmnr>*BBkPOLLcXK*1 zVBk^cx|>sb^JZl`Kyj0-c|{&h=b!B-LG%$m|LhxET=kf$lu83!XPF7hCYePa&7;e$ z{8m97G(b)lqB$1gJd!zNLEF)mRBbuAe}50(skVr>56H(AvC+Lkd85hbd80OF6R^^tE0(g z(qxBdvWYZ1Z(2A@NY=W{l@#Rw(>jS9%|RLFy$%inxUvXIdU4Nz<*K?HNZ(R2A{PxY z4=iIJRonOC4%I&LCg0?u8OWDdb`! zRy+wf`*pe4QcI7KZ#ce6zE%IQ*f;QZ zK&BMG&JRic6?A|wjO(&E8}&NOJkdsu${m1dH8L_GrtFB=B1R8nvs=IMOS7Wu5(s1&Y(vFpQ|JF?$8DR3u++rlv&QyxaHILmx<l93!KR@i4YzKPiy`zm@Wr}BXktfA<8nbc9k~V6eEmq7P>+BDvk*I z!K|#2NH}_2Tr@swJ9m0u_BA((2#er5l1D0{T7@idgCA*Jh0c(TDcFGQU5(Clc+D(X zgTy>ldh#l=VGVLe^`v$U3bA;6$V}%7?7}hQo!Ext#7H=t31r@n$dpKn(V;(kUvDjf zL#;f>sWm9r<4-f_3wfFH26>6#%7gzd%T1ISq;xIn(__X?o3qB2Y}ki_kHbFPU!k*J z6ZWC@OLE9zg6uqUcfG$VYCsyR{y#dMCp?U$LOU#ehU-d@z3Hg(;w)h2;T4=l ziE|qw;ah@M8o-3E2f;BBUiYWvw;{FbQOYNk2;G39 z2P+}2K>%;={^om2w{uKgvf1zh^#dou9DNP=0mu67NC+DMtRglvf}S0yY6C~Hp%JQ< zfvXc(&cpUV7Ubauw21?Kc#lD(i#_`%L~6|N4anOA zi=CSEQX)B>HzP~IjWVT~G%3M{?sIZei3V#f!TeGW5HwQAtWt2LY==e9l%hd_=T_4A z6{+i(PvnNYT<=Hih-k@?q&B$$JKD6(m4RE)7hW2Vs?CNWnHDwRwoRFZ+x|8r7z~ij zj+-ukU5?iwMv-5)qT!yu$IQw$eoLOA2ntdvUD}u&d!Z%;CI%W;L8cbOE3gVr--ae? zK|zjbXK3@sZOA<%!k=L7su{xZNbVwza4UIO0un(%%!=8rO07h2@>7YRp)t2T0AzNG z<&_SJpdKWGQx${uX2F019R7xu*60DWM$U@MEUi(R{6y`Z(_@r+luXwTBIArHH|B)9 zC$X9UXZJywpR#s%3WO+dIxid1-E3%f1LS#DIeniAzsW0eYnxYfZ~oOLZ*sH@b=R_# z$@4N);Y-IT2ols6q@bD&tq7xzjyY4fn({*U*P4W@4^o4#e55BdbT87d9gXf-C_Q(e zex_|{Y9K^}dLXAc=EAeUhg zTG3wGKgyAf!NgtpdvnaH%p$Ym%2cG=E-=(-MYSQjP_Z71mCv!NVamzlUC7m-ooz^w z^0h|ToJe+~19=XhAJu z6f{9Wx9>p%u{@DH-GkiFHe$XP_=Ij`=w4XfRfmLKGUr&iz#cV`N9y;YZbAzG(~-hL z|9|X75`8ADuR*dW<#BrukFSxn$Ai~C!C-1@f!QU0e0WgJCxUN9U9MJICW(;VNPc5` zzG&zb|G@z7j}itF@-0q%c^J^pSDG0~1$Cc&C^h5BqvctRA8SJ{8xzqEk^8@V?j$P?XESJzvolf<(rJ5F|f@ zt$+|Dkp>WgM7mPqYUHhRSYl@xQbe4-L6)N8TNwhmRZ+En;Wv!rp3sYge}g1op`ZB; zY)Qo={~KTdx*at&&g!MeUb##zOqgmwX=_%UXlv%iI4~`{3<%f$XCRX-w`pcWzMomyk~3@AMHmPn+ku>r=I39hD+`Tw85~L_rVL7=cb~!wJGa07lYLB=i94+C9;E^wI#H&icP>s#1f*`@PzlijV`S2e0Dr zhYjT70o1MC)8YLA*e0!^DdJfZGxg)}fTqZ_08a;zVJ(lyzeDlXO_vRH*r1W}0=oHh ziZMv4ze6$Zi`Xzc<3$kLPnZm{gxcB01jI?nmv)r;?9#!7Bts6NIZn!_H8jek{zs7) zA>NZLe2`G|I|#r^^3x#{trs-|WRn;0yNV2`L^E;oD6*##g-&8UFG|?BhDSdVp|zqk z8z2Zo>O#SE5UEA9M5R6dQKZhqAX3lwwXBv7_TU8%HwYS-WRJX$RNj4m#0u6~ghWsp8f>T?ff|$X=<+P>CNy#zPS0h=8$ZOZQRTRIz8 zXyQsezjbQEG&ysjQ&3NmS%b`B87DO;i2vImp&{lI-;;<2yymYviSi*1rRqCdQg#xY zbj!i}3PJY~`n$z1b0^cKe(g^<*m$2(vQ5_P_&f+b5>syJtI`diY^JWvqw*C{taSMiRIq zeLZksrnGK0i9dzrK}j1=p-vIPi2iBRjhnse5xHE8EIuw{j7Q+VQ$}DKo&&z5q}%Vy zHvEgl#o%jDe;Q>&F(c0)=MK>+{S531hp+cIQ-K`o2XfdjHljfbtA)u$Z7gxr`%_0Y z+3kDXwd=cMCiNKs_5kR27QnIlq!CL?_1o?1{GHy)_C{=TfVd;Ndn%NyJ%?rqxiIFU z`B`*-A4!VpIv4V29rBrZdhX@_r9zRSb7%n_f~)E}tK(1#39&qfjG!nt{x^#PohCSs zx^<{80q2oJ@T=w?XWN2FRUmm2^xYZ=K_ohzc3pVD?XM?5@!=Bf1Ry2nk*!x}G6*=Y zy=s^6%DykxZro1Y+EgF)dEiWzliBs?E3ssGJr%hiUM&mT9PJ{I@`S}8p8~pOq z%2kd<`iGTjhq9?;-UT%IUwvT+VJ;#<#8(1O>H_)Llf~MSExU9hArE-at!fh#!fG z&Lvo$eS$5>;_;)7m~6D3(hQSa; z$Bzcx($XyGyi_1JWYIS_K*f|mQ&z*Yht||6aoQ(&=07eBap_+#zAB*3Vt?BNa&$a z#wp?c>DVO#qZtj$I}63aFsr2*e5oJ#n_Ia zPr-r_YGS5>fG5=d&+TW2v*0jMJq)xkDMpg}s4L+&qBu(^#

KkRQnH!PLv(G_7%_UA->tgAyiuZ|p2 zqvhxT3Au}kx#b)V`TYkZseF4E`5`;)GNPGE722spBi<%F}D0V*_v+G_sANI0BVME(%jpox`}9->KTz=&wy#kUUybGV78M0`cV9Kmq| zxtLvyOQ`Kdv^9qM-N*~_C|#D<7C-)kmF9P78u{=u>f1$?p5ZusVF?-V2=yA48MIwA zFA9R-fI|Rn_|bYgIX!8(M_UMS3J)8M;h}!-aEawa;B3k$vs2JV;~8{}Sf{UB9X@}Z zs?<%l`HmPJnOzXLdOX(pdz{U~PU~GuwC)_07LS3TZj}|jj?c*f9;yI? z`2<8D(2i0-=653#pMXqQLM}dmfqSl!_Y0cI&G2m)C!8wb-_*+#R+)!b70D}OrCh(3 zaf0bBUyB>mLY3lF5r4XfZO$|HJ4lL$@%9Hx2=Ty+5$WMIU;-kyzS5y0BjypX##v* zLl^P4%4e1qWkDB7!sPZ4ISU+ahviVda|x{E@*AX}1x;(uq7t(3`_DA>FWMoO-qzHY z|Ej4)C;$6RUGXn8wUzJe|3Xs>v`t-^{u=#(2mU99-*a-J71?IAY?+iZp5OHbD55$; zp8~T3f;X9W3@JaZ4qo{!OK<#A1?47ZU@74b2v~_}@0CPMW)JiQDbTKGL zJx?38>i2u~?SIzPudc4$5o+*}3o@Dh8wzW$EUEkr>;=W-{cmU(=+Y5yQB23Lw{Ou1 zdh;Dbe=H`)-+_i%Ow8Y-NVo~lf=I8o$W-%|2T{L=)vAp2{{Ws&Wn_uwa{L1t*seVR zdb;N$GId^fhx|+~{*K0W>DGpDdLvwF3&_NEKqkC`fAUl09GoWR0*HAG0p{5ZnCH)b zAjy9{XX~|3ao>L-_g@gU^R{z78EG+1UOgb}OkL!rQ!=>;{GlitI3cpd=!&nOWY#>^ z`GHZv#L7HEdSN`0dR?6|AJwa+pf=6yZwVcd(TO0A0=G{*g@;)LWT

5xL7nHhOm_5M^WNbM1>q5j zSHX#nAfofXhbN5qu&73>Ac2;qXrS_c!RBT1wuo`;_XYI(<;2+#Pqlnw?%nx?q-%7W zd9s2aBRqgK8Dc|=KTomF2oL{M#IiU?RC&8JwjK#?n6dhA9C@7E z>EZoKrr#Zpr+#8SE9o$w%}sdaWZj0S6|@V4-X?f;#3Thb#v)FRIAJtAE#Fb_Qdv7c z)1Y7ibqoM~gF1YwV~_fQvc@w3vY`C3PA{)H`{@~FNtV1KA;e`;N~xf~i0GN(h17Y% z)R#Rl&!LM(Vo{K9OmV)0c+C+A2cHFO8L&wSWB1GkuS5X!p~1lqSMn!E==gngwKwIi8Qk5OWLc?GX0OYk@iz0K$R#ePb2Z zC>Stw*9Zv+;=9;5im?`WJ;*8VEjq7Ho|bqp=Kh_eT4EP2#3CdcEn&)qJRp^p*iOuJ zj%&DXN-Je$3waII{*e3`PQYV)}^Xn7U?F&p6wQd@nRg0 zjKEFL3Wxx|Q-8f3;OBYK3cCZ!+-ilR!P9e$HC)O`g*7%u1?03f-Ui#?OdCApqf1xf zW{bxm7m{I%BWV;Hdh&vK`@ssLg;6Q#J@aMVSNfX~t{o2J!YLMHA0InXmp(h}9VDTa zl(;HKsY-Dq##`+qhLGu!I`_<-eEVJ!!=nPmzxlA0GS<{sO^MjSK=TfD(hv?ts>x4w zcpBZ0EJu=1dz{|2{O9?L;DiFVLY9ZE^aiko2@B1-=^V&Qz6?9rYGMD%J1OLWJzh#9 zliR{Zt71yXLI>;w<=NzbyYpz^aB{%`+X<$AwGj;nFh=C11D;2}Vm^{2Nbu(lQFciY z?Q?W#C~e*liKRXSEO7rVC4B&SFTsvFK1|{tKNBZMTu3AMTaP3ajyMo=*ODiWc)1Z9 z`Kc+GhMF;lDC{KH2`AEYmcFFb2}|(zKE&D?=fdDnI^%rJ834q~1$V=(C1k7%9z=`l zg2Q-h9MwlISRqpPPn!kNQI~FdbJ(gS<$wu^a>d!y^zjpA9)mdXz!f_gwZU9%teqTU z(G|OCG70XA-7Q-WJM(#=fMf#*B68NS-5|VAQMJJ$M&(l%)2MKHA|# zcDmt6x?i~Ak(1)Sy!kqiH)kF_N~}|WnicsX=@6%nOcs+C3No*{T&sOH)HdsI0*&<% z(h-~BN{FD$&0Q1dgFQ_o+&witnCx)JKD=KGZ*C?x-0@22sRR%BX4#6HH~y7x`cv=k z|H?PNrtxanZ|+-p^Rf1ujh?tG@+5zF;sK(T!ymSUs4eth9Ig*cO%EZ%y|87M#*_n@ zkKW{y*D*p2>4z&nU9(6VR1|7cI2#pEbwMKt@=>Zc6~MCmr$8lLIekuQ4SDJ0Af3yDgKt%Vg1 zAHbhBj=6k6wS_#C;_*%&G5WOQ{vA!EynKQAYGXDBqWIxd(@%0gK!f2f?tv9Fb4#bT zh6K=I5su%-MQaznsiw1>5JTu_gDND=ZAPRM88F;b7;S@!V;8!e(^Sz?+;OldV zf3kbAaOe@(SK$P}pKmZKor&NXd}Sfo;*Y~AJ@PCpAX|ZnGjs^$T+)9r5|9$$3QU}j zD3bsA0tx@2M3ipVQ6f^;6FW=VTs}EACL6k&B$Ou{vPq(1Om|1?a>~`*N%VW+{w^FE z-^~`+Jt@1H-;0-)NsavqW0}KGlIDRBD~4x*UTq_DdSRd5U-nvD`oi*7LWo2Y_R1cm zZZoJ!m<=zejTxY?zX9Q-Xy)G7Y2}$;pQb!Jg&M@V>R-t9UU(4|lLK&9%Ujf>z`|H% z8W?L8?VWjKMF9Q`SI;631F##!QZNd{{pio(f!IU8XeU_Ve=KoLC^$;8192#7sjLgc z8&J1a7aDBenV)|g#EjYv8#M<)qVGPn?HBgJlRW;;CbrVc>RCmh2*a%>C87F)OJxAqnnzh%l zg14LVBtA+T4-gD;7*3xpd9!_9W@Wh)t=t*&i~gQFGX(EzjyT?jXhQ;l^8Sn#*-5e> z2+M_$TGMy(v!TRAg=Bj44r~0LPYnCvc^OdU5fg3MMi9X2X(dsYNcp$-)tRvND-=`!1SI$9uo#x zLvX6gFZ`31j2sECL`y7ZFB+Hxts`E}|KSDsy&tyEICC|Lzw0hMhOEn~XD*kYxGJj1 z6GPc%HCRt;c<#^JC+CA`JWwqx4-nF357XG*-qtTBRSZDp+EqCS4YI8N$ zoOV?I;hE4i`avmw!192E)x4q;LRsHH4nDd>di` zW*@Z^v$FEo06ZCGXa+MBxW*y`AfZmd4#3J^y&4+mLNwJGCaNFlT=<-hUKjY)B$|EV zYDHu2)#v`w1#Cy5YS1KrWvy+nb=@w3!Qe}aUXE8DKMd!-wiMIB zK-SB#VK?P2~m*4 z+s*tHKCiakA-@J=JCMAEA=r8*w6CuldwSoJou$Iz_aT62a~?qM1xt1!gE4H#0r19J zveVIE+*DdJE8jr&{1g2zB{HD)(?b!IzO?(?Ag5kwZ14dL$BAy{2QVxAX#}u4GZ-$! zW?e#xLa~MYH)MO ztT%Ci96W2!P*2B983%gQtL}^kU1*;B*WoYf2A{Yp)qm~l@bT9h@se8lb!``UoA5-H zFoO=lVsuR}TylUHaiX#^6epoR3#<1Gl$ z2%8G-%#d=gNmnc(iw9u`bd78pgl&66j|3DL^we}hLH3O(8r~+6Dl*WJk5s*GYZ?-M zJW=<$P2=_(XHz>+Ie7tj_PH~oF8fxA#(x8r{RZysa+(2jZT}X7zVOytb-=ImEqwvZ z%mRjEV#bE}d)1fpAB@ErP$r#M936N?W7tr>dG9Rv0X$M$A?m~A)d$1xWf?N$8jj93b76kR`5{T?jc_FT|71IULX8LJv~A=fO@<_ z;zNwXerQ}CJ2@(g9E5*|gE8wgMw@Ho?qF;>>$(5a;EbohMgfK>jESekHAQqIXJ>11@O6DlIcYer2)?w*PW=oX7_uFxzxtre==z3kc4+S&TZ zgqJ}N>B<=>z({y9J^?PzmCW2;EuVQe%bSA zaK|9LeT-L4UEpSc*X-ByWU$QZ&;8#Ita^Wr9g#)KQdX=13Ckeam_RRP_@A3Lk><>( zsdZl<85W{Hq$9sACwSG=oBeah?>fz|dhPCx4$8ZpV0l&3r3ot*^ww-K;7tC@0&7Lc zFvC>|iBmYOuTkc_dGr5>NBct^}(C+ExOC7^UT^#;4vPTapgte^=w}0Zv7eh0ifM)zK2%1s;<8%L} z!55qABeg4qI{zZO)_fSAy`*LNMfm!=%RTziJUXou8O*RHomPtJ0rD2=Y%SL4(ZYE>7A{OS@qtE|h*`U$AoyVJs5b?FzvYKo-~76{O|4ZFYsxqrk2p**;*U z#;%a3>B5{*tX)Am8k>=)qp&Ww#quzT9E~X-3~t(?MlyUf?rmEL8XWsCMxyoUs3}0$ z2ey?bWZP(*)DMM!cPR#(#Xt*yLz$#Qq!6UENN%CXHs)qi@P4xA;Nm#S8IywHrCR-6 zs*5~cce!Tb7Ldp>_)E|i)njmXsskF0#d*BU^jph_<75cBcW^BBL;J|jV{y+;{1EmK z#KfL{EGwuDcJ4h6uM)Qr?)WUzE^yfax>00v`V1oX#^DjDg7|&*Q3Jx@ga%Bqm`)oI z&bC`F#B2is3~;7Ssx<@i+MTd1(%<7a2o()wNSp$26wdteDiO z!_)agVn;4UVF}dcc@&;VG0E#Dm67A|Myvxt$@F4KOEg}iQ$hQTBu&C@5GfKH(-?3L zld+sUorEP28}idTC7;~!ZF^ya$*cKJ8d_0mJFSSBj7MPL^uSkDuvU7cudov38|&9E3fH7^u!bq{!eDZ>6B$yDGFpckD|08Vzm z!=;|IDquNk?fNlU?9YD#tqax}mZZk7gPb2lFNK`bJP+`Y>j4iK-IN%XiTt3nZx1=0 zmh*3)gR?K2q&!6tx(%$Ks4T41nL7>6pm&=~<0S^e<{<*6hY>j&gD3q@7b5<@P>8|g zX)NC1-}#t64R20kE>fkZl*Vf?6UL3{zeg@x1|iP`LadA#M@~=0a-BzD`Mykqarksb z=S-kI4`?Zns`RhrGl63RZg3nAP+{dF8oEwU#(9)xlXqD_w__zwd4G;1j0<)#?8)hK zJ8!E$WkIX>a9cW*z1^MOzR%uP)6}xa`~I+_s`Md8$M6*ijTwwU1zPoO{=lB}2t-jf z&41nX0!YLN=^KhDXPSQx0lZN<1KwaD+AMwH4EsVP`@)tV*%u7x3ygw&Awa-c+A5HUS#!jJRH*8osPqOp;v*L z*~1t*2Cki_3_GxG=#-%Y8?X~!8r1MWWpn~|__sJhf@uoA4fbz@IO=)G;2aRN1PPIR zn;d^B7wQDypSCO?U)x9A-Kkb3ap5Hp8d{JS1n%R&cFo41&Z)mY(z?I>&lX=NN`@6U zw?FQ8^pW;)zoTkjzj)GfHtu5?#SJw$B-F3rN9+BZ#BDY>WOfO439}{r!H;&$l4d^H zI~#khiN0(=Y;Pg&HE$|J#Ayy5FDma1a4s86d^=s&zb4D(U~8Vdu`r*EoQur{zIrGO zpQs7jBAa_r3DN}>**5l&roM>ea8}DLBzCNU#EjRlu}4sv?*k44n@8PJ&<&4E&KI8%lmp#IAo{5G-#bBj#d@|CM6wNW#N#^)vE1 z2`_O3KWm0>0sJ_%z*yMWlEhc7|YPRrBzDz}Cs86zpu){+5b; zOOxTmZ5MFl-lqFtnU3 zS%6u-?E-9Ou!RDhyXhA3*JUOt}^W3=g8B?O> zzs-$5FeUBH``m;FQ%W8R@@B4AR1MP4n|(>qxWh0nF*l}_Z=IKoER9G+JO=HaCKfBE zg2!MW}R^*h+CUZ#7ywJJ3qfm{*L-=R{elZ{@8+S&3;@ipO~+=;+)M zE76C%4e0LNDl3I<{w8!LsnJSikiP{zPinPNTjwj$m3d<8BDegl==o5&ma z$I!JUjW(R;`Nz?+j8>Zr#ru2}TFxM`ZKRQysX@0hQJ`&-mzb$VIoT-6Rum*=PNSFE zD9u(HA!h2(vm8`n%ZU;*=g^H@RAsB2D`x6ZVLocKWfqE=i)d#)YPD6Qie^@b3P^J=9*%t||nWreP6gAo>^~}yozpt@(IGs-dZzR_?vG~pquEu zHIsuceUpKr+*+(`m^^%XKT2~`jIdz}@V-N+#7(xyhFOXqRiP?3*(MuiIaVG)jc&># zHq1(V@EB@!W87?+BD}W-iQQ#hw#;hWRD%NDlX}}S#rXV56y@GBz?NBu57eSG_oU&r za6a(aQ>esUlwiwjz=uzxDtGll+YDwC&aOj^?y3@7W($6F7PY#|_S!N^oOvFJJ&KOn zGFvgJM}Z!Zmu#6beBuI%@~C)X%k03aizv+_>6tB4j(@#~N<0*;w#;t4v!cHpa|Hi(6;*kvhuJa5@P+HB(KBg=9djJt`vJ9j7Ok*j zRQTXeNbJSgYsb{!dq1H-FAfZ$T3mh;MR`e&*)gYa<4u(26?xu{sl(qlp%Smi3wBJ# zIo#5Os=SJB*fI6E{1$5TO8WoWI@_S8vNMi*o^w9b&g>GcoklA+?Ch7Dq>zw6xZ(Ya zGrU@MrqgDoJG+4pTE|XHzqGMqn+HKe6pXvB_ln4dj8z0=v$};VSex0gTXii>E#l?X zKoLVki1^a0MQFC)%J%D-|D2iMZ|0mi=b1C-nMlTA_{$VgzgIhzjA2lxh&I)?kc@XA zI8B7qip69cfr)A2NKIKz#!=|GPdurS)nruQ!F?j7;(9WULsNvvsiDmrPQs}fqNK)m za5xQro*`;#D4D|utjr|3Ri=5RO%hvtYQ%~{UjJpBFv@uWrG=P(LQ z^F&H3+{0lEI_8O-7XKNCi+~S_l2);g!zH-#kf>>q{T#;OpAU)FgkBC;;AoTxrivpR zK7(6P;xIW|ID7%KQQ|R0S~*m`phk&gDwH^U1=0eMO%qq!6|dtKm(76LkJCV*hrs0A|4@hgTp4;y+|a%d7Hy#+WeTv zLU4@3qcr%KC_>>Rhplw%F;N9?WST=CtzRNqdpyeF2lVt(qOC}6jKdT3($zdA}E)&`AT;;HxPAwC~UbxO-2VGw#s@?w$9s23%IMHU~ zH+2}Ge~c3$+xLbJ&(f!H;>Zqbb$E_?&p#oa?82Qo?4r|8h?MQu>9Cu&t`IqUlSzlY zbp9DpvYmm{x71 z3deLP)2`P<$_Y*AaFC9@CUQ=ET8CF@{TfknYP}1IeT8hH^snXnBF@8+B}Vk$2+v89)!GLE{`Mhn708OdGTT%M`?cpc=DWOJSw#R zAV_(&@A5cKm4hJX`QGDklKLA#$qVo0ahi@af|?ip1&*9M$6o?1=ZONu20|wYo0E7~s$AD+q+4JBi3GO%GIVN_2 zr^MW9z%C|T0I4L>X25QC{Q}4(zB2~wWo_M{lwgkm``F!XP)kz!3>ai}J>b=rhGYX? zVqHBTl!k^3_!+y|1CG-0H3Rmu{$B8uI{#`wnZ4)*snj`Uz(Ll35#-XylmV}@*hNrE z%~1nhWBxu+OT&*07-Hjnpe?IiHsI&11cdT#BefP}0JlwnU*OlZ?`~LA0`pdh2dj|&2o`%yu)Y!7JtQoHADj~z{wpnbI zV#?FRk2AkofwH75w>#5fvkMk$dPYr_P5k>x;sKe{hp6&Zu!!SGp|!9W4?&I_XwX_YB_NQj?KcnPs+H)7@EaTaA#lOPuedZ*8%fZ8dIt zWtGK}m04X=Y2GDn4^Uo{nO^O7Sp>J)U7cAi)L6vhPZHOL@H5!9rONKkbXlv?tE$}9 z=0t3lcqBkmlQOF-Ef%{y)0$;TP*jV_FJSvX$#b|*HCe6xuHF1S6-0SPU8kZ>lCK4zvJWI&YIW6U)q&7I>R@< zeU$w^-!U?keQ}rFMv*ErZ1YAJdW-E&;9eyK8Uo^#(y&JV5`$Ivdb<*ty>h)Bx0;uH zhAi?cE%dEz@{5@8W0&Ajl3=xwbGt2A@Yu*%t>*ng2_J|AkLAK!l<@A4O z7xE;pAT@9B{k#qE`6TbXRMxn<+>+Eh>65&zfL6_LxG45b3nm>NizDh3PUXgZE)wf< z<9-)~O}X(vxxyyF#F}+Vw6t0uAX7}M2y#YhkvH1w95N$G;&GewoG$S&>x2zD&-M<_ z(+c5Zwbvbm*M)k|bNFwk?!R@mCavRz6t6q9eY~J-b28T3XACIFWKN0IS>NM5ZQ?F^ z!qc7NCR8)m&)XZ0PCEsPX*H{vvVEKwqdu}r&uSgTMskkSe~p&?yPC7Y#8xK>SIRjH z%$x*jtV{ZIs}S0lXBC<#^yPrDvilikJ~ZphEf z2P@h&o+pg7Ii;Q;~959W%5!ZfGgf+hXlfiFKm!a~FwC zW@TM#X}rORcx2_t5t5XUEr@)CB?3_ zUHMYcJbp*PAmAy@HKMM=<_oH|wU#za&G2T@qmM5z&SKYV)fHz&^V2sZ)_X#@=p+PB zEEb^?T7t$4;HsIKbDA6Tl&>pjNo9o=6~xbFg*NFD=dweaB-Sh3A~F<_3C4@y%*$1| zP8ov>GW8iHMyrKq$E}bFz~^p(@4%-_h|WdZGcycq6gI>G4GVKgf`ApMn?08wZHkXf zXj3``MxD-NF1~4Cg{JA!=kh~~{H+rJ<-VxBZAy<4gH34L5`LxCd8xvt)IBakB1mXs zJcze0k-gQ#yDJku79mNfgI9t|xvV)lzWvNH?vQwu(nB>QzFFx}G-Q|=RXih5$}kVx zWSv)w!YfVUajnCn1tqh>ZIUak7$Q@^=?ZHh(g-}*630809-a7+Q%U9ysVJ+}T+rF1 zE1k=VF4C1pyfqY^AL5Nh4SfUY2RWb*9o;o;?pg1JUF+H*1;J0F?zp7bvZ%Wr5^F-n ze5c94I`E!r2~{9%duQAsc9^u%Z(!wpaN<-IW69SdmM9L?`a@W*QAmy8kd&ABf7Ml3YsRW#2%q-YuyXs5L`shv;jJg=vC-BWnAkm8;vp>pA4!mG2=!z}TD&vo!H z#p{B?y9J~3?%R>VHygcIBN^q0j@h|K)d@Sk_E_5dzDo)4lBRn+mmQs?7eD9|SYbCxJr061irU)Oyr$QKBJk`rkq+KyxN88@ zsB=Z1v3z7YS4;YUJY1#oma6v-l^14~b5@8rIoXBpW^(#Mq{<4yVh*|yIM7)yC9H>v zrH~_3c}9tAitQYu&)LT|Xzf7n7;p(W&VY~#@0$d-WP-;A!7paPZ{UwwL5ECu2mWXi zbPz&-IV=)9lnZ`o6V%9s9daS+NRFICyXSjp>}cw)O{sKYu3c@lG_}Mo@Q^giKD3^{ zRC}Q$FcD|tSjAi6xlSL*Cxt8Fb4qxwJ6Ap}Jl{P{!F^MmdvsKKSd-ha(mbi5jNieI z0S962t&pdnkDLc^EUt*ll#oR)C@Y0eSVg_<+{4VxXT(bl`JRx5!ja^%b}I<1Z3Qb- zWa2KgxBuh}ccGiZ5dg`~bAceZ8UD?zIKY>6$1XC!w@6_(F#!7mxY!S8L`&%^ zDJQ(aEl~09wz~op$_mhcjf15^Jz#MN_~W+3(@dNH1=8!LT9DS^d9U8HImPP*MMg~P zttjq@1ixvqU?FOEfed9fkD;tc608UJ1T(I* ziP}T+PeAEFg+y>$?sUD<>zdBvcD?Yz`Hyg1S(m7^Prvz}$?iP?=uhtYsNy1IejR2K zwzca#TT(pkNIb9Cd)`){lgj0Z3!le|CbUuW*wMg|=3Ed3ztO^J6rhP61jcgr1*BdQ^urtBF|~xqo9V$9pOcV_=94@Xd93-kK)~+99s412cp`zO2HhYGlwzzr#Lv*B7P5|Er=jDZn zwAJ$p;FG8djp+1oPN0@n=+2_YVpvgJ2@%Fre!LTxMP+Xl(4D$Hl8xd5< ziW2!#z!R(BT`990ant%bA;fid|Dtw!->AP1oj>(hogUek3ss4O@dT@RZ0{seOVU_{MpG>MS zQ;Tb|oN|1d1MAwtIikWffDFpDKu)$Oe~nq+yK$AaFb9`(g_)U!Z_~6)16qa@W|{S? z%L`Yu6;96TVvbZbxs?!Fc2dK*4tBmD$iSEnfsD7i0F1Co#TecSc3?HSmFq3BdZU%U z$O!#GDoC_J9Pb>VcRwBJ-%{>+&9I}h?R2rxDsaNr>BrEFx2ReB3UgGPwSiDvQ(c%9Xq5xSsR1fYrG2T~J0jm*zBNxO(kjzg(c*&m^t=#LL1Oxb z!PFTlLFTe^@!oJ()RD9<sj!Pm zk=?5Zq6?RL_2UR=*Am#fjh;GUx~#D+RwDD+=31~fe~00`*zB8E>njbl=E)+bU$HCS znpd%}N72l;H5rggn8UeNIYSCpXB1{-azMe6fuGpD;ro$mqwSkxr`wlrW#w)QDp4D7 zD3cCml!6-^0XH}huYu_DDVF%)h+BC99P$|5bR%fmYY!L zwtmx#G*+}>Qwtb6mq)CK0^uYj7&WyJcGwBI#*8KDnQ?)v(M!NIPEdiXw+9`D6J4a% z;^;Ui(E-odv;3t{Nbg%(Kxq{qtz+9=N2D60N!KB?CAM7$r%z0}QD8@D|AHfkrBlR1 z;_6bSe0jyu_MB*G`y?pU@*_&zS6V^W-gjww{*)KO!7I105_dptJ%DJt2`tT;@MAGm zJnQ_A;G>}#I-mJ@l{vZo@VP)2Jij1hjl_S&(1^53r?ARaC><(`te2eQFKx>;?t5E0 z4A^t|(6{aEDE9AW!Jh`4r6Kd&HwbPf2_I$(@0tajkb=52Hb;6MpG@LCkqK@QLQA?| zpi7=fU%kGU2HozKuaIl%kw>0=Cf=>G;?%qq9O3OKBg^hsF^vu zieg3%o6C)JX;3x%q#Cm)1{xc6!FS-IdBfuB>ajEIKPRShtHxlJy3_Tr2z|8qXa45= zau7HxCgMp`z%=T6aOP>$71vbTY2aVYE8{ccoVcqBO!4Dj3UT3waq8YKK`nS7$HfS+ zcGo26OcFej;oGVt%)ON1B~>hudNp*T>x$ za$Fx<3OwnC)-s0!ufS*(GsX}%w7D@BZVk$zu(E?0dXX7h9XGVf#~&(YVy3(SyuQHM z0it`+{Gtxq&-?~Tesq=CH2QWz6k@g62Yt(3Dsu_@7PCvh;34Y+2{x>zJR@k(=%ewM z4xfuflCgd)KmH=vzz6BF!yicU6a+)6tDetFd9kT>KGc0U#6PTn&t^u>x7=w(*1Bbs ziMv$fz3KhKGOJ7$gR4I`hDD{ccJ@|-Ky`6LOkHCvt_)LT(D{F|%swkPZnrp>A`xm0b1q)KjE;x-3>1a6pww=%on`u6vs_UyJR;=5-Dvj1Kswm z5jcK@SA6gaSO0iSd-)kY9z(og5?`qIYN>aE@x#4JT)#m1k>25XrP8BBb}}>R@APfy zm0njYEhaP+Mz8x?!3*dgw2m$HP@Y)p6BsX-?G3j~mr$3Jk4yJ#36k05K+fC7LMeZ* zgVA(EzpT{45z~wW>kgsbF3tQ(7;!Du>rXd*A5MOuB1(<}rB_2M+m)tU>8viEoTmwrpVY*R`S>t>Wo^s+ZC8Hv9rwMzU;NwEi zI|^Iv!!E(YE}Mr*La4pr_EWeu^L{r$DbD#_%UK6)fA1C%uFrpw(T*(=Jna(vPP@Uu zp1)x(02pez1P_t~L79}oa69a~M!Mw%TrhGmbE4q+Za6_E!~=wtN{1Z@mI)o6(!fZL z8L6UeqE}8Oa>pG(d~|52w>vHVc7oqV*?v_jqi5imBG?>c- zg7p2ZOY1AvrJy7*m{#QgK4B>y9UDk5x|SEeF!d=tIf-+{Jnps(eJqos1Ab2Ec)Shb zhq(t}AtVVcvyXMSkmf;q0#OTucFT}gFVziGE!>tM1}douwim!sC=V!Muc!PU%ULiV zr%s7?8Wvd_{DguZZp@K_8GL{AUQtLc)K5kXvww{uzhbg5y6xXe~JG{uzhS zg5y6xm@GK#{~3qbg5y6x5VXXS9QxsS)!1%Q7MVIEjD4J6@d(v>Q>e;rpz2loZWGU6 zje5#5eRus0sRHUTC~?(=b7Z*6d>2BdOMcHH=Pl?9>Nt2}O8NEfg+Eq7ZET?HI+fKb zSz)G{vr@%bt}e_%?>h`&;jn_vaUxKh!<%T&s9B@6xZi+g0}9wVkecWMA1A2xLfEsa zybvhJa$yd+Q#c!n{$2`HoK^cEO*N?P6_a+Xe*=oyFMZWs(5?R8PNb4RF8}>Rs$PiW zgj@_0frb=M94guzZ8zs_Es|K5j<&Zwm9qCevBX>9SLqw2ug9l{sVNY$h zAYo*XwN7vW5WOfkhZK=P_DL`SE*`%wZo!TPbMse}b5<9j>%-jzg+sLZIo0||etf{m z%E8D9uv}BPv3H{zN$xZSUELIHvQS{#Ws}oQ!PgZR(Lp8EGp9pWhYhk#RCsklke|jp zyL|5odQh%($QI%NKV>S8?)-^gSByf{6SU}nT_8H1y0nGcrlJ&JJ;_@8k1wrXl7;&8`% zV>=SzJ}MIvo^E?_%&zxb54V*_MO2U>qOvAMJed^fpu!z+FwUNhxNgz~%lD$p;r_2E z(I7$BV}h({B_`;&n~^9sh)XN5N?wH&u|a%`{*tNG&T;O@W`sZAqQW52(5$_i(DLE_ zJc|~^MbuD~5EE!^Q6q0u30e)9EsC@9Nkj+X&Z0QRWoMZe1V01FtdU&ID?O2c2#02t~ z!?4{YQ$Dwl^@w1bi?qowHV4hWiOhiTrir#aaZwUlHe!JFDr_-ucnjJMz^3lgCtFVE z!@L-qZII}Tti4F1^c3`XLAg{EGXDU&tni}!AfX{$wKZZA8adJftPqP)ni4VUn~GpG zKEePF=u-IP&G)L}fqx8U%#HUB1i+~S{5mQ}-{!;kRV#Md3 zML|k<)_w3II9Nc75Drd3Zjs*&fp-WL`pR~IU9)ls^kv86VpOeqF=PY!iNE=BzU?#aIi%C3s?eK!)aa}#0O2LdVRD-Wnmx@rG&9g4vR5jnEAf61LOlJ) z6T%k1eCz3qE|`Q+O($2gvVIy@hZd@apo62WyX)vd>{wCk{0n;YYkV{+;d(3e;xujN z(C-EoH^#slPUvH5`-s(?iEMq?#Gi**M6ck3G)B-Eb{fUL4q5Om*A{LoQzI zg11`Zxe8u`{P7NWtNg?&nxy0QB$&>BC3*K;C%bnJ4&BHDuo`%UU>5vN_b^Ypz?+1> z&~Fqz5#c(%0~#KKu!>$>W1@Q&x?u^bV|Bc}cP5>CF25C`fD#;%9fil0tL3e zU3X5*!!JY-Z=4M}JjvlLF!+CetDnSs1XNN&+=z7Xex~~mV%T?sdtPC_(xg=aQ(b}| zdv;ituXnF42A@u|Y z^h=`9t_xE@%SR_aQyK9?6QY9T=*p0hC2vT_Ko8t&J0|AvW;{uWfr-$I+?b1CCir#$ z+}0_FgDJtwWV6ou3FKE@AedWTn>mxJM*m!d^S- zLV?2^64BLx8l;{WF2&P;#@H(Th*G^bxC$P@z(@>x(NGu*Bv2dAO|*x3tY*T0-N$2% zz}HgDoW%tDcbV|6QFzOYJNsP_Z$*Ni4J>X_schI=k&3jZuD6;{s| zR=od*FRY*s-x{3I<6sQdctzmOAh(`bovd)B5x+T^0&f6{3RedfvJ8m}_M|sAB+gZa z`jwSj2wZS6GS#g@OUa6fTMUAzSvqAgIYeq-MY=3j`H+;AnV(Cwn^mNNu#xlP%X}1W zYWE#MguR+n)!&&dRWTRqZ6f2n@hD^3O7a1^F)e_cfjHBB8J=fQ z$n!hMPwz)nBh(SgoIi zt@p$UO51V_+33n-xJmM&HaD&lq?Lxz7&p_;W5Msx*rtlDWB*O0U+>74*=H zX3zGJ%-U|XK+AUDv4X2*O(l|L$A;KkAg-GC#Su~y!;pLa3$%Tss^1z=oyQLdF-@^a6r_8|xrEc8;j zaK5i_IvisCDwXL=t|^KMLS{K1z=6sGpWBWsw<8GuSE+nZ_bWRZ&afip_K_JpDOxER zW03|tBi>S9Nt#+G4xgR)JlMq0ThO$8G0v|9%2d@+-PMYzCx9%@P(_7f&G z++k=rR?I@d=AkM_f-u1X1wU{B^5**H`i}|13`b*} z@W^D?5N{V<1dyn4rQPECgCOx&pWd6b+3>`HaN%QC;o@Tb)(`UG9AOY97g*@UlUQsw zv<~nz!y*MgZ~<+##d*q4!Hn7X7I0Y9xX>*qe>Re@5{GDQ2>yI{M%xLA4S&X%XY!fA zFQ`}x58#3m&&M9-+(p_|L6a3<5+-9ewr=r#JxXvBOby(MqT%tmBPxz7z5-SEK+;CB z@NAXsLo1>HplC=2hJ03Wt^OO!lt0~v~ws46>FL!}XFbq^b~;5t_4^8A@ZoI7B{f|Fwf@b05b zxhvsvjXnZCXtE^xs+cW=$=t&LZ7IoP@;xT9iGpZ=>b1Tti-K3Q4I*S%8$iBADE1Tb z8MaeVN{*wZ8g!RQuM@;R2Yh1U6vrsFE7$?7Qt*=$fUS7Tnc$Di;g~239*f9k-4f3P z8sIbx2^WYg^5A2#6%OLyTY3?!c*DFs!ZbFa#eosi28aOX*a6J7@(A=KCs3n~fNvcD zxEvlC$Afa?f+tLQLV)(myM-j*Nu&SkQyRUzANnirTF?)J-M#1?{~EBC0JLr0XyF+I ziF=uMnH3~qgdhvD#24tz&+UDip|w1MSc&iHRZPLvna#TS=!?}s48k3Ct`1V124;uD zW)v^tGhI#`?@OSdpT0I+b5Cvu&K|>l z3Vz@M&N6OPDSrWf>1GTTvEl!HTD%T4_=?r2ASZYZ+bbIJZ)S5oEdR#qW;1x(xu9Y& zq&=LSRZxROf^1p^+L^VivEST;s{6GWa2=z2xI<%5_#OJq=o^q2WxKP+^rquZFeUHsmYgUr7n0QD2(fwNybzCdz~qoxSyKTo+0otD4-6Ou^ugf zXW=c0hU-fZk6?v@AGp9Ff?Vz@1SDbT<^>kPA>2->gg~yg2QSd4l}s8Le?%KV5D-|f zNG*^hX9K-Y10-Z9ie3Yp9uq%y+Z=ZQ1l(Uh*Q0#kwa!#|e71A< zG&#_g-A~SIJ#~6FlFkji8aeQ_?@%>BuI>l4CiYoQuY06O0 zKsQs}8Dr+#S@|;D(&!Cp5GO4%+;{iE14}HCcoV^9(=c-GH!0!rq2dt;M~(|IHQkF9MKB& z{t1hHhU2yOQAp(nmSRB*PvC;M^L?b1{qI02WSTyLTTTZV%F+1zkxrR!5=2j32*k*$ zo_%vb_z3OJ4|Hk{APC?^ixJVNK3QZXc#b;q9R{RS5$fh1xzL4cMb;#apB146Q|zN? z?Wg7r$TYObEfMn4ZYQ^k zVuJV>Rx#f05^7>-WF7J@bPUaW>-CECz_uf8)JITI0yNf##W{ZeWD+|Dr4%}7jPOj> z{S0ubRqr%Rc6|Xyynw|%(xZ+(qM-8V2RZ57WbZtveW1RS12A0Rj7?XP^AEv6QhZA< z0?t#{w+5HK4tf7tvQ?Dkbx^BETZ3P~xzwwQ3BL6C#L7az1~#arkzyI2H}B!ihn%H? zm0oSMIDa;B$bi=j;rC8I-U5L1cop(q^q>h-H2`XcRSJIKf&`GVdcAT69L~YF^de3G z{~9a44ynCgD=_K%*}F0)gZ%=SoQA{#IQOT0ejRXy9luuqTTVL%?f?M*V||bpo-*=B z{$&B{^{PqJ=NM&EEMUFIC;nn1z759%6b0~b0ig@lJy6aSs6GwvY3mnikMB+s8$EjyTEunVlQ6lY!`@;%& zP$4gWEHAC2#NR z2FDwysTrB^Z)WsM#Y+-bN&Qri_1%5p<$p7yFVi*uZbt1<&zYAXj`pYZ#P{CSPzd?= zqg6Bb++U_6;G8{zrQ^z;w=Z+5fmo0Ltpb{@nsd+0;Ko{z5>^&1fWg*F#5csc8sGrS$*#$z~0Vw74ZYSqwS^JEq_vT%hiCAD?0@eJ$4B%O5{3WQe^wj;PSng|YLEn6V6i;g&ttQLdc#h4w(h8V0FWj%z+gx@hTIVFc{nks7ZN{mNzT7Lnf;t4 z?w^i=f4kNqKaQd|1v0e9QOc$OjlK+cfiTj?((g4hT=5JbsGmh#_@UKw{59tHoY?MK z}#*LY5}sJ>~CG!?s^>3 zN=U!sp8@22=-c|?y!#}|CJW@%uXa4}!{^fmWP;op009LefD4Soc(RgQ^SUlxMn}TG z6n#%TpzC$YhIO7JPV`Y`Nrn%6R1>G5$wq>KmpZ_xA%C%C%_p z`+*}RV88uX*nC?p8Pzv0rd`VKsz(TnwXyTdEvUdzns(^(pP_^A2Wsxw5bPd{q9fbQ z_VbFhuW`}hA2Uo1^i1x@?}6{n>!8#(!eX!OwTz63-3PWeyPNXv;n&WU*#;;FssI!d z(Op)qdT>WWfNe~L(4e)@2KKjp$r#Ra=+eMl`+~*Q2iMIYEIiKcgWQri#^z7hI}Y|@ z3M}PH%dLTq55a-UVWro#w@h7iFmn#%M}U*V1Gqp8*S;M1cHwgdLHXl*dKFg)KYI@C zbSC)WJ+dWn6mI)Po^rBevpD3X6`}V8SbUmCJd1W1j82vWId_6oq1UES$uX*hA@y>PrReVx zM@=UX8~ZA;2i~?~E^h~lR`)PXQ?%cPeKQG^4B!NS!v*Ei^tm!oz9UQw;p{#gUpl9* z<_u>OrZ-`=mwetQ^>Se+=&2g-g&)wcRx)c#wqECT5#kjvB&S!g@nn1OAL9hpFSN}2 zSxxX#*o1s4!1dy7xm`~Qo4_Uy!D=twOF!%Dhh0QnNX$rSMeNdGvIT{eI%-N`cs#cs zyPw-KN8Ay<7N=uH$`%xIbj&Igp zgsECT3eUcDG3oY`mf=sYb-Dc=R>Yjj)OPexNCAbOs?qwiF7{#e>n1HeLx~q6#a74Z zW;cRZ-jBkIQs#)Z!7#&yRSI)To3vjd`=)6TA-e-^DaUJcrF(7*|8)Jo2z5J1ON&=6 z@nE29IkOH`Zxw4e%bA4Q8y@ru?Vaz^G6lETL>vTXT4r+WWGyGpm_1r-iGpMr3C4yi z)-RC4V+VNSb6D+*!P^6vLsikQQ@HO<_A1jDm|=EPh-143D(t@l;NKj9P4o;{x-)_2 zR&vNeK%Mm}^TFFgn9DN&_3eJ@c`}WCvui0qwDwcaiX;3dlIxZUmKF$v3k>M{rLM*} z7{SZIO$i|&hYP&_(U0Nq1tWC6EJy>RNcFxRmC^$HVzq0#V)|@ z8V#M>=dkxwgOKU~v)r-@K9ShQS9bs@)jeowQZDUsHRdh>OM!6FXUpt+2@zfTHAqwL zNdAhplrLm}H<1-$r{`cM-I0cRPem9w=NZ~cDXd~Uz^17hT{gdsnG>>6$2Lc@4gI-olCyH{Yn5*B$nz%gJv4XwB8KQ~)V5vBklaSMw+EAE zWVb`CfmwyD=j|Ct1yp-4%ywnv2}0cy-D%-jZC}u41BG1w7nxCSFlU?KE$&}E#!Kh_ zpzZ7&+1rrhflxWH2N$3n6>a;-cpF|Hfpux=MQps92g}@cG@N~HoSInromreEAn-dR z$^r{jV9-wXN7aCL1*`ySxWLSFA4C#`AArvfgnO)O5RO`9_0s~`7Ee+C(l36vZB#9j zfnRTQUm`W~-RT~e6hjfC`WgL@5819)Nm2%}s{4YYHaw4P&!5I%7~z=SROV=Nfb`1a zBHd20=1verB=*Ded>?y-d8M2v2Q!yjFo7tpC)?g39%_jpFo4urRzVb-K5~o9;;;ya z%H0>3CvU_h?OkX1@<~6mFZQ#~og_#jCa+f#$ulPmE`MglB`(2gFMX5VKcEO|15tbo zfPE2d`6T9uYG8YEKfEJ8X4_mRNmDH~QFzHH zlnc37&=kFhL&mX#>{asBa^iSDu2ZMm{$YBoCA9sxK6KQri@ZmYW+1N@E$`GNlX#+# zt8E9Iy{v4R`SHi~p4DC=;_$1y94MK>-1I<8lmp)G3#9q-xLeYvAk8H`Yna@H4=c`9aJ8mv@ zsP4lc%`py34&nP1j%NPL*a67pfV}$xK|MIecE3WBL_c{ezaN~j21E*ZxckD1>FlTV zURrMvaqLyrgWG56=a?KQJVMu6fPwX|ex2rapL{}+MqE|`JX~PD$v+K#Viij=j6gy! z?~@jOrW<0m77*XfL6tPyM7{^BZ=z zQh{xJrNbGOIyXFZZq1^%7rg8H@!SD#ht0K#+3xOFRI}#O0Fu4=DF2iXS@z&dQi57O zn`K4cBU5z{gO!1Pu8u$(s>AT&*FJrVX?WMyJ|x;%>%}$xc9tL_?0!P;9`az2S5Qao zAk=(_AKLiT%9Nobiv78YkvGg2N6+HBi|XaX%QcO2ozGX3c6^p>EF~>Hu?PNl2p=Ny za57^vQD#?6Ity`lkrvzcAwHbYADgjh^vqstKF()*v7v5kzaCEQqiaUZ|91QNng(m& zu-Rvct9>fkQS04@te44{{v`c343eA6s7BJGteVB(k&98|5tCOBj{$DGPpn+TpX$FScUrE``-4KP zrc=J`{A?}dQr((pRl{mJUZ1&+lx-6cyRDUN-$qN9b~rV%N6AF;kvELTts)l7SxmCk zp8G|&fZW}_$PN^-E0$>4>Z7RTO9fVC6R6TK8i|ibFdEmQgySPv`@qQ1-*us=?zlrA zliwYW2_15haCw8PJ^yRJ}2U>EpsRez;72Md=zv%4InJ{OC$kAFik zUzywuip36;oLw^82tKn;PWApZz^y8Z z7qo9#p>2`LMLVK6MQ)SYuH_b!&6Vq}-bHs$%6Rv#!oitr%Jn(&HI;L#XD#E_r*s<8 zjm9vfuIB~)8Q``jis#ycW8F!Gd}9iYTAfG1 z^-)OF#6}|;_~?2)m;4i*Y;<{*f@pXo{`X}+l-VR6hGTDp-Ln9m?pO->{eDIY*S+cnUtEs5I9-keElJ%luf0ijDSJZ0H@@2D$ zTy>jwl@F_i)lj4$!6|m2pmT+zTgRp2B(0mlntCB)^aUr<55dZ&fp~wtGeItomSmwpA z%?u{4{dH1Oy>UL6CXb74QfD?V(js8eEkKzcBaxP((Ce}&dFOn#lo zs@Fa+#c>V3&a?>X(EL_qfGG1hQD_dy8~DCNZc~dbO-~$)WlKW4#brms9z<=e;~9@6 zh&t=6sNRWP4aClRtePiG%{jfDIhD_Sl5e8F|gbsKwlbJ8_GUAh^#~V z&IT{>cPT2^zqw%?YpLaTo;7<{%EBtyVmX&XrpdKubwo_6_Be1$UVT|0qQ*F}+NIoT zUv~4mI0Vkh=ITnM$n=2gk^8v{c-^b)_H1Piz|Y|ILY> zi1qCNvJ=U^b!IS+qJ(e9N3}gor)z=$w_WkP2)h^w{{5Xx7n!S)87AMTGMw-PJ?MyM z{sofI_ds+-HVjn*I{U3}Xunt=yF%gI6YGgfry_e|z3ZOtWa!zJ2xSA>eBOghM+I#u z3>iXq+v3X>EoRuF*z+QX$D3hN16NRX>KH!n5oFanXwLcZ0R8Ft1mEf54Eayn!5^W1 zfoO_p)n=4V4{RNEKQE)yEvR+WLF9H}rb|DfKWkNU3v9VjT&{YnHZdy6oZN;!`Ysk)&(80t*vH~c{QAf- zkRf;3&cCEQ70H3a4%^P(GP1s!tmphUL8_U64qowQPeDOv{I>otB&0WHy1QV4^3w>dYXop`fdi z*|1HNLZa^<&Ox152e9eHN0xo^lyomMwvsHT520U*uv_Qjw%eaKh8qiEOh*{ZDDm0| z4ej+bt3A%t^Bb}R?OZ*-f1~gBXQTwF7_PTf`BZa|?jzoKC7m01IB}htaoiGl8||F= zU~S(~;9*T|gCebl|HkguT6A4IWoa!m&|5I`oWG;%P{V|0TNw<)x)Ui^Y&J4d4Br{ZrbfbkbDR?BUZN^K24dC3F;>7Ox5IaTj)!)QkSI6=d40?WGpypNsajr zoRY2s^+anFODUT#Vx4K7 z`(RY zKo(hYV~I$7ZA85!X`?<@YKWE9z05`TZoK0U*zFasmQHx2=fE2MYB-@jMET|cHk0!| zd2d>-#M*Z0x9CgrVm~85(pL&a|0@mH2G!JNZ}7GKKJoP-ifY9WQJG;S!vke>xVeIH zSNZcS#TT`zM!|1n=K+bE5=HLOv}`&Un#kd)I^50{}@zxL|C&|5dt1kj7H6iZx7A+knpWWDZYU#S_+Xz`Cx zqv+jgnW8*bDkglY#H|=BQ(&&f;-V40SeTi?~QB!eC^t}Hm603IQ!u&0VC!?S%hqAeTf9<614p%l-WGST;YY%M@ zK|3)7IsX^>}Bbe;Z z=c6(A@~{wH6{ziApr)BRYArHuEhY^0i-px#ocE+|dvUpQ^B;cir|@%7y4sl~OI1I? z_36+fZEbW{a+>C@{8MgYh|a(wqd0wRjR7slYFLfXtoQ&y4@#A%t4Y3&1wmCV-DTQi z^h5feW%lKcU%_NTlvM)d0-s>j6A#d-pM%JY=$D_1$<1iZeP1vn<9$c?r_o36FV|qw zf#?;Gb>hJ>oPW~>m->rvhsPN0&0^bOVX`+ zm3{qLv+kVm>1&O+v$*!93 zyMjrN=a+pNLlm;qq;j0qPaNTfjio@-z6|K_koTh^hGH$+|0s}ES^vNlU3wJjn>6Rk z3o?j~ViB~HCCF(jgu|5gCUQ%5Bxf(|I2c>^l^#X@7Q)(#H>CYmg9%8HCn3+r@gC1_ z_dDzh%V8e)u&x@-V?OEipU4?hizJUmBK|`@YW*V+dHiALaeu}}KHY<+U}uBPO(FGQ z7ue{!kmS!*$n?kP{|V?lcGB2*qFIfO{5i_CdfDJ`Fs4RZayEnjy$qUNtM#DP$H@MP zFZ|oks3(3<@6LSUI&c1|5fGxo$7Xi>%Ct>mWn+y!H@6a@m6}OH5DLi&$_&b|c3sMi zl9ex&Z@R?A?xM~*&=FL)z?X0hlQrO)@zVs{S7<}-BV$wX-O2R#iW zc_#21D0;7`H=~qip=2t0|C!Y3;*@o=7Rx*nsOe_?cXZ~NmqvdzW(aF#eG>ei)x~p~ zigdV5zv#T4Ti*jtLM>Oy1+AC=x*=+;y4BvJhIOtRZpvp|C@X%&4r1usoxcaVfpT9* zhTlg{AEXZP6)ye7EYcQ?hUPeDubuOXHE~7`+p8x)oGQY@0+jw-;8;BE*bbm8Vr*us z{X|RZN}7Y#KlcizQPiG>|8siJQ0n(d0rhUZQ--OKFR$m+acduN?Yjk;wA(8DER^p>6mzj|yo~-++Bog* zc-bZ&A2C%FsBd{ZQ7mo>AyKlWG%b^n`u`U=IQY*09S6)s zPyZJjynN$-qXQ2%>0LI)ii{TO>$dGoqnkJaimK~no2*Dz#_7be9c=P#P!<4A7V1Ag z@CwY0G98}7Z6=mCP$VSKaXN0Yp{kh}`K0lkD8e%%$=92*$R;%$MkicJMM+CvU zVu|TJ7wQ+_#kBHA32P$+Pn>3c{Mvc>Rt_0u(^qUjG1w;ijtXSt7Rile=fr1#XwE+o zUHQevFMEh)a|Z3|C3+2~hib}}{Ei9bQQ1-f3Dev%p@58Ggnw5i5|G2-wy^uQNI-^^ zbqUBTZ@$V?w8T?FLsX5G7=NnuRIO3%4@JD62jeesWi4y7;mSXy7te z5gAWDEmMog+Y?^JJeSaq-tqK~3+LmD!UcH9?L`-|P@w8x8SMj1%qD1&1=9^9rd!FuA*l zXH=%d*8Hn8hOpk<3}HI~hwaG=W!L^{klfiguU$Kp!6^5uE2EqM4V>V_A_ zWx8F0cy0w*Q@zKvEAzRakQ)3cki(CP)Y4^EsIXCr3_bBQFO;H}xcj+L_O;KyS3viYqqETgO zn;wku$i3nMEqE&5LX@DiZut7RO!s+EjFc*9Y*$E!&j&5%X8p*ABO@$gip{+FhrghH zX%!@+&1{;*{hXw0e>F+&&^h-qg-P3ZSsj2!??XWeE0@U1-V&4d+2*7CBh{+1(T?OG za%$N-j^s3Fea-5f>aA3>);Aoo{TQ`LqR;Hdp3WRf+Z@&7dOyW#VnZD1@7tmu9IY##h zeZTj0Tk7k-wHf8p1B+cm197>V+!Zla)EdrL;wgBx9oWmMBE_$`U#Kd(;7t0DKCpZI z`pB_bsB^*qzIyJ7Txks}A(+)Z?v=^-YHq#wtbHKVjkp~s-s~9$eIYij`jYo>Pf#}8 zg}i_pw)r48g&P@7{#y2iD>*h$z4T$wdSgJjp9{Qbb%l~YFk)%~yeFN;-VG&Tt{pRV z1a#WUsxp%+`7WNQ2~*1CZsd@j{nXN~|9-zcz5ms@#oJ|Jex#=Y&z=V!dSGHMICI&4 za+>Tab0#ihR2z?`bqR=HW%QRpi2}=$^YYuFK+_Kb5`jM-H-n z;_G$*H*yQggdU``^)adC_NTHz9%KNos*WyXz6 z*4End6Aa8ZQTMeWsC2UTOQwInNRS^9cv%jbOA?>OHp4T@$)T>u#Voyx%luY_w>VRB z=ILnS<$%1|i7AUYWQqe4cUO&nY_HaOyjD#6yzFMcu$6L=i}Bmh(eve;cri!qF-+0G z<+@y}AoIE*fk3tV=Kf&z6KBJuF6;)&_Ekc*bwgG{baTxzetBs3VQKO%T$h-@5V3xj zja_0Im!2V)yFobS@8nrG)L-=5g1|8GJn@!kfLdUDa3Bj-h+JIYY+?jM66t|#yD(Pn zw{OU74-|rvw~+%L$hF_Nk7J`(e3P+wi+2PC!m1!lo)v;|E!B=nj986^AilJl1%K8w3c^x(Y`%tr5t3+ z55Fwhzx4;h+}3GIG6!@3+xYP9Z12=URqQ6c!4m!u#epwgEpymCM5V_z>!n#V_!thg z-#vuI5C2|tvD;!{&iqpMrrpwXHhWE=W~$-V%Xf#atFJMEBVh|)70`v1L%#6@G2u@l z5+T#-jYfA1AqrYm}Y3T@B+QWdB?wSpyu{+n0 z{yvocp2Gazlm3pn(pqZSw8>3OlNL~kXDU!z?_bd0U(nxeRZQhEv=WgKt$YTp zMD687Yf8oM)fSeIy1^&ILrY99gZh$qe+vQnWX&M53w5rIv7vinr^pmHK4Vs#@s7ATq2c z8c(ru7Xe{ME0lDuFu7BOFX%fP-|V3k-s?~ya)%0E(}%%+WOz?Bj+!Dbx{!1+@-S~% z0x<{hM;+H?)N#Fq92BGBq4_tR_lSgnA~1`lnx8fYK$0;A;{-qKedAhwRI6cJy8Kha zxcu!7onf5x_eI|L^fx5g7Y+CDa9U)ZGt(IQ|2z=OHnE3E__6uNwtEH^8wW%L@=uRY z(3AC23c2fxZ0y5+Y`Jd7260RPcCBPdv3f3B6)@y;xdaGZEuEkTyt+2DlEB`f@qmkD*zcj(|*e>4_4=($It?cmzZ9c)_5FaC!e zEPP+n*1;(O+77M=KqI6V_I#1s6bm9f=B2o@;2edsIw8hx^DM;=QHo?e-zNcF@Ty$p zRq91c?LZlrN~Ivfh14_YjdL{qTZmmRO15-0F*5dOR`i<6HoWIFBli z?A{)&7H<=HyQBU4{L zsIPhWzfoU*sL#)zsqehDK2RX5`=gL{gMr=v)IH0#=iKM__|-h=Ts>$Do@I&yY>#6JMTXK{lH$yk}-750v@U7zq2b4 z1?a2=$|2(7`@aX9s1tS80%_O}BgpdssFW(*^FeuB8Gqu_!~t_YOQ z^~U{e>B7loa2q~kq6FCuyZkr?@?W|55PIxp!z9`Gas!_@fX}p2$v7fM1wR%ut|byLpWC4?}^d zh@^+1ZlI-Y2}Avy?hXiF!ONFzQVf#t=W|Ykt?Ac_0g8xH-v7Nf`2${IXGcmSiElV^ z_D>n-ZwU^+^m@mqQmJ{ww9~RK&wUNSZ8~gSJt&aZWuNsvY#63fMh{EQJxwEd;V1y5 zkQ3p6Fg!hhG=!rF`zMEbn`AUjJ?AVoo1y{F``40oARg&A5IM5z=fATjQwJiiF0D}H z$~6PgX=GL5t>>r%R!NMCj)Gc*^+?iS1^met5#{hAKlpbcm9s;be4XZuKhHdNgfYIl5RN*?ky{Q$dd4Fmw%A#pWO;KYLG|q zuqcleFLWO+;rlKZlTi`K!n@-fo*paQ)i#HvNfaDIy&=fgcn6#__Gh+`H4(^??cQ(h zw`6YwvX8_W;marK^%CS%zpCoLI_!mTM*ZK!>QOjCreI+DY9<)L zvFx0a_RA6Wy36Kcu0aC%oWhbzrbBldkV_u$Kpn6_`|DI2-j-OEC2avUoEHlO>@)e5kj31IEkp|^-+D0Ex<^u=lV zbT`z{_B3TEvThTaRt`mPku97M!q_>sm*wD!n@i=1ejq(5ocNYRISlz?`7?5D7?Nax zJzM)1E7FD%Td>0!%nbFw0R&IbrotIaTGh!c-h+ueCy!l1gS1Z`d+!#3=sB~ zEU+@t;gMAg_%fGw&P!dKYfYh0T-zF`AT)Kn@fTL8?X| zk(X#`%_E}(gY|4ZZ!cJnV0T{#y?s(NITjeQU!B?nV|6?N5qL)arxaBqId<6O=m z-^dqWi<}F#NY(h3Fb-Oieei-80yA}~G>YZQIkOpRk&k;*3bh1iP5t{T7mP$Ei2CHy zBr#-J6bcYSZ#ckB84)?VoE5;XCZ&LnhkKyX0vUvNwI>H||Q?RH$DQ z!6?{o_qvb+fDHwxVI!y}@~`I3G)TNMcB8uoOhH!cTi-!&6(pnIyAzk;E}5AV^{LZbLk`d;*TGRh7d0 zE9~rS+%~!kQk_)^9gxxuVchPs=y-X6eN3%9L#~ZME{WohlVz98gFTbL>{y`cDF%cM zz)@)EO`%iDOE|>iYgH+9QJs3ZwTCit{EQL_$R0trU#WXB*iR`9 zrQ6c{6cciiYMX$A^Iq=F=YacLnPAY}LE8)2()vfd1cQURrU!4W7nQoJ2JuY5`YPHs zSHrCb@4#mF@|tX#V65`@u}B|*M9f(Hzr8=SqglVB#sAyWogPt(f8TYYqa1Q-JmNav zy+2e7W67m3mI>dCfPHFz$T|f%w?-?FpT?sUYxRWV@Pr>Pd zv1o)9$YCjAlJ%`d<0i6bB60&y$+n5846j&C22MgQw)iNVWH0yt^IQ|mmJBi16lODc zmPbTB30b3JLMEZZdJ2{|88#UW_680MQEpo9$)fC&W}~rSz)e7Iv(a#Hp{WbijF9)7 zs3xNk7Qc)hs(^k+QAPsS-og;QCC*b&hPC4Lgk9{7?tEAoECbk}+T}vNoPvtb7Sekv znh4{vek!`phd3g+KI5o`)~N1RFb(-+!O_nMW^nW~pCA&zC!AcGM7Ct=?-VRe@qrqn zDX?y3wW0}h-8RhccJDAOd~J(@F9eeUUE zd;D#&pR;Or2f3ytj4PhqAkRF^GL6XX1U4jLGBg6<{$!mD_2u0gvT}e}kkiZ@z(2~6 zQ_t(RC!5s#1At?O<5H>4q#-domUYQ(9H4P-SQ$hGsKgEp5sz5pA?}2gE!BG|TFoe{ z0Gw4SUTU;hSy_qXe4mIr(Gu3x?<(c7NRQ#M`zVi%184Jfax@M^#h*!I99nGJitU#t z9@Uyg5~ibQa7!Pbj(QJKd{(plzFiJ*j!k+asfe`j@OB0EElx6l%~$L3aPStqoW=Lk z;5xrrWY7Ktb)2$m(5zM&g7l3?{ZKi{j7Q#p0@xjoTs+V8JAQ@4D}kBX=iExs1IDtu z_Y1JS?=J1uTc~GPE7>ijhWb5)XZzyc_#1hta2`_#VbsTJ5etY3w)*HnH zJd2@k@A8EwcJ@+Acy13w60NoA)gWG)+;K4#L5xwnr)BC%>pYRAM?D!o1Bu2C^x@?9 zVAlk6`9dyAwfZ%EXr?4vpkb^SIaZZnTm5={=u+mj3!v`QSp7umW*~7d-;qbh7+$l_1aV$q`Rka--AoY!V9Vy5GjG?A zm2s|kWee)e!vhLI%BF^)_^6}AHv!rBG+TVk&DJwvUe?%J{#q8fzwPB5&Y5@0u@xLY zAVn@(%NaO;WF#O@^pGeMkO0ShK~5x~9`3TfW6W|EL=+^g>W8Gw#)hT!yHem(t5pxi zk~I5PLq(^*(An7%v2%bYYP!4mtL@Ma+qn+9hP@hl`X6D^O- zF5wP|gR`>rgqk!94Fy;q*)t2AwiV=Wvyig@Fv(5)@2;lVTHN<@ma?5gF8@gq%L6E|1E;wa7xZ7?msllpB5!y0p3GEZxHywJjv#!8?A5INL;}@-IG&%3gT?rv=nbiMZWzOq*e9GD|v5*Ef zQ%gk3F2R`8zV2BC%7EQa4@D(34fU&P&WJQoCyjwa$cp-@HzX9Fe_CpvbG-`4>A{e5 zMYir{uiotaYXFrnfoW`?v|D9bDtF>^KqVZb#<+v=iji~wXy#WB3QCrwGc-TqY;QEV z;9R(JUW5F#mLiiu$EU2%3KQGK0)NPrGF4rWdRDGW<<6Q;Aql<|lF&4?Pw<0`(I)CS z>nT2tfh0^$>aw?S)dgqGN`Kf^mqiR+zsNS+9NU|Hat#NF7i!1S@n~w_9tFyv@4-tP zqhLsDR*awf*#rLjLDWP#hu?+va^Reb%IztLgE*RFyyGxIU(QD^yszWga-GskZq7#o zqmSyJjMeaF zTZNpiKzF|x#2S|N!T@ac6=4;Y@#hM39{lw@h1UB^8W*5zbnIfO2`nAC{KHN}{MYE; z(1HHIzovhV{wMSohaIwvw<-MR^xw)v{Z0D13Xd?Lc99uNe>3q|hz4W@hWQmf$cQn? zo@x&wQJM9{rxo@&r=qm$tNCaJEO(g@#!!Ccu$UCnrxtY|PePFvVoW{voz5xwdHt2v` zoq0LRnzPy2wlVdjcY!Fd-%B8->OsaN6EsJ|X%8tWHS>m$k|fFW3S00lRo+kKrk>_$ zcu-jLAY-x#n%B~)a8D?lD47j~)jpL!r*dmf8*7ZAaKnR)DJE!PVV90IXZ42CGbL%X z>YkOqrgE>IHqn?s>6Ql>Q%%s~@=m4uLg56-Vp?_2%6F;Ud#6n`rcn6xgN$h==yOe{ z!u_G}49QMfv$#?(jr;PnrN$Bpb022NOi)$}Q#eZ-HB)L90;S_6`)SqUN~1JxXswmT z3Q7weX2hDHWrf_1R1bl|(yV5Dm)Sj z%OpS3s{JZ^q;YF%9W)M5IObu-3=_1m(4ZsH6QHourPB!!oJ)zpGj7K;`)WWnm# zcynWKcJhv{9al%Pd!2daQBznP{nAeQ7l=l@&wd{Zi*DxJ&mQvYmu=~|=&o!4)AyB# zIU?75Xd@$v(mC@ulC`;{1=xPS4brw#TwlYNc+ih$(9#~n6@ zsd}8~MDnB>I4VD1Lkr@Rq$1D>L|oBFm(4d15&O?Uv95ZUG229XTtnkC!`a1U^DjO9 z-aaSIlR(L0u4s6e5tWxelfuy*^TnWEm7~+R*B|)64p+I#hpn77ch5t9MbQZ=%@1ZB z7fx(|*IJC=SXZs>wfp##O<^y5mQb7DYzga;@LHqKCFer&8Q1}Eph%u;?ENGQnq9#G z(LrWwccszflCzT3182tlMDi^w6XzB@LDS(3|b5X9rJTz|(t&>YiR8u}hKAYE9i!jXhq!mj)xs zx?s((ba|6v`iR*U(u*w+w`10vqAuobch-pYz#xKUlg0NUA}Tv22hxw)`6J8^m-^rpgwUEFO4 z?JG8SrhOe1Pi`*g&7Q4rf~P4$c5(N^7oVQ6&p9?>GxShmj3cbCP_$F_a%#pd@m_oJ zX_Y;$dPEgWr7_mnoTr>LyHQ1R$z124_^cI)v5=dCH3)& zsUYutwPgDw&{+hav#5FSi;4q}GAXR-x*Al07gPgSN;QBes@ix`)y4{nv8eZLDT*ERb zmwN_^X=t%owAe9PY%;CRhZ1K4#au0ulRR5 z_mA~o@83I7hyJ~f`lNqPvj5Zmff22I8S2L8#ZAJ-lPr@Pjww$c(|2kncb1_ZSxX=% z%^*XAg>fe%V8S=~td;ICIxg@H{u69tlIIy=sn0;ih`?Br!`f`v?sS@D>a5%iR<#DX zgvY=w;)>;lAnx6H!!iGDU_C53a9X7DB|hFim?_v}zzp}^q@Sf{08T8C0oSw7WnE1= zze?a{qXb>L>9c$4VLQztXe@{Ht{p6UFv%`QN3wLW8IT%?0(t>i%{XKRmcv?p6=g>q z%}mw@7yg_LK~j@!dQS1VA_JVPC+EA_HcWq1kAIMrDF3CX{{5y_GsK4LC3FZG<@x zJ$7M5H0W)7$hYE$bEg;F_7Lf@oE2Uwudtj?&2*}|Gi{l|!oqC61NP129UGRm!jS7y z@JrYt1Mom(;V^t<<{~H2vq)UkO|IpHg42x-<2*#bA)9(V1G+G&ixBx}96d zh++VZe+UjcY|YUh02Y3I2-8dHo@xcdGmx4TLanuN$#(bzOEDoon`?fh>35z<_T*sd z_`T0FpVH6rb#7~{=C;>kA(I9CdSl8knmp@1Z~W9oeE=GtHVzYWj_?MV!B4_zGI-YJ zZ96$#f9Mf*M6_Wetac5xSSW`Y#VgDdHDI&lNsKgn`O>B1p)A! zy|8EMc_Z~@p!}8zbgX(Q>A42kdpgYwR$TX>=43upC~7%pTQBK#0ag~bJJtleu304z zl)*-o_>=TC=p1-V`mIIZyLF7mfxQXbnc1UEKr$T`@zT`!Byb(rD}N-ibtuf}%`r>; zmvB z53*(hqRBkSz71#!MG>(_&9UuTL--|H6p=4r>+B*DAsG(!F>zf34QV)vh0CHww z!{W`E%$7L*GukD2e3YvQ5Tu&?) zN{W+KMT7O)W3uKiJ7q^?8&R5Zr=F3fjcAgE95P7+vF9CXzPEfAB!|$0tPW(vCL|P= z89IQrHZYn=9Z^*TBM*N0h$1LXayFrbv@Q-9hc|(=7G6ZSn~_^L$Xhp46lbKzPhIw< zVZY?Dd`#_9b6W%1bfG;v$mq?eFKQyIHzS)^ZTpL)Gw!#we~15Ce;QbdchgO?=$oO zK@NO@dT9UmBxoDRv}=ghHY74F-nrg@2_RC81?Ch-CT#8V76@sd|Wtb_=_CFEQ9s{OS$k!(kH+%{9`^zCR+aKkE^ z1th&h{>fRNpXbxkW+g2>k@Ru7Tr;P`qQJlz9FwI zg{UIU=4$&q^;MUp>vBAd`YccUc+AnT7QH)9Rin!*U|tbIo% ze#+VrX^@A(?-kiq9Q)GM@^40-wNKqN8@TE%= z4*hCanuThedzdaX3l{YbhjDH-@{~uZXIMI_2aIihlDrFzZs(ilcA@?jtz~K;hPP=T ztNE8pPj3^O-N>s)_^?ag#fh)8MDfM?r86L?_O`53LdxCM8fpQd8HC8(-Kd*=ZlUpm zU*UCd-_`?r;q}5Yy~|#$=I=wh(Lqlz;l@j%fH?XWEBXsUv*%Mn?~%eiXsF(icssJ4 zkGqlgdyq|MJH1mm^0Ym_He=Jyaa0}~cX&IM$1sivW$f><<;X?QiCV{#6>ZdRE=P90 zv-TDo$Q@B-8I=>CUZXSFn(SzGw2C9aSrJ8TDfSC>g4R#vXuTn0NuOg|Bd;KNdy%_w z8(@)fkZ=0{K!CcvNEq&YV}OlYzl%|PWYy|PD0TmIkIe9S*tSOmCv@^KxPk98xaUcv z`#$9A$Ar3BQo!gk@1z1_?y>-Yy}OQ=@JDgRyX+M0w0H&!kPGU5ef)+~yJ!wulC=+2 zQA%xKbu2*Ru%TRGvx`?UF`8c-L^jBR96N}d_!YOZxKi6=@-Ykrx$tncxz`2taW;uZ}#i}AH zFLAmtMb+81KkRE|hJ!N|WdQFEI0tR!cqCg!LS2VA_aGSFqY1!@JA4|4kLVSb!a;|S z);q%)^l3PJtjW^*K{`?8@KYx(eoUhw1SWY*)BOJkE_o?f{$R+pIqe4#(uLU}!|Y0Y=ilaST^KuKp6)aTpw~ zHKge<>gv6~b@cKew*JO{I9S__=iU$04VM2AmK9dPlT1XEqy$*-gl&?{&=XNHw(F8sue&nTs z1R`*^GY1h>Wa><@)*W(elApdtb6n(4YiR0FBb*E_ZQYzfwk^q!K|KDSAS*YJjALk$ zVR{lsG{3<27v$zKGz-f|lfjiJoWq1|Y$9tak%J3lR|36YncGYdv-z~?oxMI4v+FA% zPKMEH5nTYr-vxy>GHYfzVu|O$*J2`X`vK_1;Pfj8~YX&gYTBa~|FmDAN$R-j{4FcgB zl2Q#Y>14928jXc!-c_S9c)d9p^$qiN&o?L$Jt6#4ND8Q&=u>EYpa=kfgA6AyY5yM0 z7MOf3f_!y>=dknE& zO*j3J}BYzvW+`^-A~Pf00%qJc}H>JHQcQ0ZfBTt3$pdxDL%0 zC|5J6dB|+c7;7Kc(&V+FhK3~T5|SFf{PE8<&c#N@l`2tL7P)i@MUpX>kj20IRw6D< zA@jZi>2VE_T}Iw~&FpuB^I6{Ylw1?s;zYJy2A0lfrJi_8TiKMGXmsnZWbYkhO6tFZ z3$lTwe}_iGN56XH8UTP4$^{vN2rxLBmqR`&VKk_yHkSP^in&q~=5X?W!$}EeQWLGq?~&^~UhzoNHDqD3Wy8RH&eRX;NHQ6F z1BF4RqK!9De`mm{myLs*WYnrBnUv_SRof}Xzi`}AE;2Yl{kMuA48vle_+xTP~OBC z!JQP{$QOS@@isul&T)oNADk?qG_c_;?euG6+kgg&wGVZvf5VwVVQtY5)s3ISY)Cl+ zvSamfxNJFh8(GzWBHaG2$}>!?#P@f&jDk$(?mc}|z~)=on9-oYIlbrtEk+>KDj~LytvEuIw_!<(Z$na^Pgn2o z+em6&?*3PA3^Jc>^;f?`O?Mb>09Ld~)}5?i2EghdsW-=){Bj2b@sq@%35iiN8PSAR zpcCX~6IzcdDpT%)P1r%l479sNq}wetogaT3xqAh{O= z5F=MmaoF=A8?0WZJft)atH(9bb4U%gwtCE^0DT?8@9*pZoZUW;+t|PGWSc!8-mF2M zC~*aWXnDFW`Z@FgT4q8|0_HDP#A5wMes}=9bxP%L56~23D{dOci)C?c8A^H8R;LAp z>Ply>!dNX}k(oaskztE%YfAn_WX(^gZx`{>EHrcBQF84kNM$P>u!}!G22$%lL;)=2 z=Fx`wxxHwjOMA!=D;+>QT9Cc@eIi^~5*?XQqT23Z(0ojEcorGgf_gcLwj~z^ubqH( z(IV&bvCBsHQe7}e<-QgGr`v``mT*|P07&IxaD0GS9#oq&kmzOP#UnHy7HZsM)C)CK zmOe(a^s@Y*GczR688z*UZK=94PNL_}QdorwbJfeG##bf0alF~Zoaq(L9?(hKWC%D3 zQ*!KbdNqj3)%3C@f3s(;J!UWAFxMVfpl#WSr9w}gO#Q=|)idhXZguBI%dcKG=Yn!R zT9^JU3-Z4~hTWlSIVjM$JtP!nR^_E#ZsMg&qzP^R`X(%^PJ_2Q1~AlxaUEyYDp|m5 z&pz*YA-U~ejhC&*oS~ht%TpF{vmv1rPiVqs!PRoClIJLh8>{dhn4v;fNyu~1ijI;+ z&yfRw{FN_|gfu)y!tO8W$)5*l>!E|vS=)<4VQxebYDdVm1#!879P7!YLDDMk0?ez{HabxE-P+)>x|Z%*A>b?xrXQO{tFi@4&YR^FAslB3Ix@ZNM> zcad+vhfqO^-=N{3W8Z#*V%xv1dJ7yJetZk5DJw|yJ5ZA=$liA-3VwuV{m6wk$U^&8 zcT#@^JQrKu!~Ry0tM4KAn~Io!U_PQhpn>heJs4B>cY7>{B;bFi<}8FAd_K6IjK z(7q&dNG|t4v*#P>Dw&Ypr7~gFhN0^&ZsIsYd!_f!+;%q#&}nmh4DnuVl20QnpdB{E zVfc^VN{nzQ{^JIG1dwVYY|*z>!wYfICKT?+n2SERDvGU>D5|RqdbOITm}m)-bqZhd zQ6qud(6p;gFo!&2V{0PfVJ`oV4Lyta3?}U?44mKz3Fcv{o2}sC{sL9TH_q%qYq*|) zdN>*G{n1$+$z2}q%h$|BBUrQ>D@pS7CRz4kHNV!fAs3$~hf=Af=^|NKf*93>S37}Ob z08&b2)K7~x&~{Id*Cu$3r;hsG#bAGBF5W3UG})jn@ixeT3YaI}%P+|XQ|v_6n_`KF z?j6tecYOcq9rE53Pt|+#TMvSausov{Ve$BG$;B;k)ZmrFT2zz2SL+cH;rgVtzp|w99@j_oFP(XJ0-pYf^R2Yq z`8F@{l?$XF%Apps!Zrc1#tg3=+CNq=);b>Us)&FKz$S2rO!W{2V~RfXj-PvOgKZ7{R6w0}Y|StmovB1)lN0Ei}gx?{H;SdFu+RZ8%7E zxSwhzrIeLIa4eNW%ZQ&9&OmWwuNC%jl7ICZwuWzeSi4gks^@N_cF;F zf49OL0Wni--H~a1YmEnE#aqI)!ESnxB9Zj8!9wi%kVM*G2SKNFizU-uQy4doUH=`C z+hAwm3w;-9Qk}WjfWts$`CR#7x8mA>s{RUc(gycv^BFv~!3oF|!u)Kdb8P>l@qWAE zo`x^J7Lp~l*c2A`3R^r04ACv{VN)A(5cE&zsd#-}$DU3U;+=3V{wc(foj$sf3MJx@ z8ao_?dJqeH97S)qfGaSp+HSbuFIwss_6Uru*G&tbJU0?k4`%<{&!DAVN zMppWOHAWs0uDIzR%uc-mXWQCgl1jaFvd|GPH-s+R!?CN9D~Yiac7cY)PS~4G^QV(o zC+xsgC^t)`L1y|S-wDsBtysm9_fB|$Q?WzJ(6*hqJe&@0n8?NmG9-99q@R?MVi9)M z|0;Lx;1+TW^1{=k2EtfG?*0uqlLTjMjTNP2sWV<-%4Csh45b-utRU|^v30?7>17Bu zQnJDYi||%4Ip~7(U}z-Ik$??uOTIB#&J2AWFF#j$ktm!X<84##e@9 z&W6;i%eQb(*jlC^i6&3nu!6cmex$HtkTVv#V;9p_lU6I%r=09_#~#{BzIVr-Hijo$ zIc%zzx_s3OE~B_we@W@Sc{wK5UGW?`8n&^duq$@u7e^+K6@_)ky>+rHc4X&ozFA3b zb;T~B-ajOjEJo5?aiVEpxo4)^7w*BIp6^$Uz5$#I@P@Z<@)O%qZYd)?Tdn2NZa5zX zLDLPx)uP(FEquuHZrF~^U>8h0u&bfriDlvG{+TVicaXjwubA!u} z;pr#CNgq$#lWkIT^D8pP6R!di-+MxvwX1Ia9Q<#zSxckI|CKhc(2O}uo0nJLe5Y$O zxd(8%0J5$J4)MV!9F$>A)`qYaH%?AJIS`UaZDI`RA{&PI7KZpA-lrWo-;%MS#0$?e zhxKOH>7t;4>$1PI<}&C;aQl#LUeHHoZC&-k;V{l`lIb`nlo80}HV?+R*t>mN`jJX+ z><~nY!yO|kxML*0vbabFS2W~^_OQPY1{YcQ=&u(o+oA=RKrDib)tKb&PPce{PMr53 zMn25UP4>aPz3wS*8uwu*jiTGuz_Ieqd@fvM#;lT5CN@Djg~leVi43iDO($v}Ad=?N zA+LOJ0Zhb_o_K=gZ|;7&Ohpu}1wg^!_ohwwG>^szif>rV1m{b8Sz~xZOz43pL&oD{&>JN<#y((;n~90o8mT8 zl^Zgq_|BrA#rcttu?^scO7*UINQ)i63&MT`2o)cKNM=#I`l=Rg^0uCH+Iu~3>Ipb* zW%MRExk`UBgdJZkAe>%!2*t^r2d=UM;61~NNMQhW`v0Qc$-S_vs5NMmWjAz_w|Qb= z(lNUfD#Lg?3(G0`^dQ;R3lDI^G*6v9))?--xgn69nN5BEGBe5eA4Sar=@oa@D18q> zfw*Vyt$|Cn|6=n^QkY1aqRSDz+HG8um<%s8naKg5{yRt}tl0W;Rz_<>|C`g#UV-1~yyTmyNkB7?w$)X_afnJiGLAXEtdM^lf zH`43@-}~Q6-4hFcB{so09Q{!_IT&w3-9Ea}`$Jth1*bsNXxg+{d$;HOuRrzZJM_U* zvi@WW+v?6j<+~()<2@QybW$XLwkI~T=osa?%$ICA^`~=R)E$Y@l8nTlmg|`)EdCXPQat;FP z)nl9^Qxe0zIH%W#k${hem|8QqgtKf1O<7d-F-g{VPa`o}9CjM)&wNl2uDz%|GYPi- z)sF$;Y3lS4qV9_={j!8!)rBXv<%@bM?YcV#igM+wx7+fQd%n!caV!3FPwdY|``;yT z-`AXQz7JWBxLoB&(xo3B$Q!S7gR7nnBdTwa#EAaFIKpdJ5+fDzCiVSrSQhki}ez1#`aQ1Soppzad~2_Z|?m5%`_OGk}@S0;&Uk{1n3fe{g`;C%lvIiL`N zc0lT#EP<1T#_NoS#`J92@#2dzOXOCe^y3? z;HgNWUFgt(8tX6sBy>oyur-sbUJCSHUD=4B<1qW_A;#;bO};f!?>8F(T@;zxpJ7qc++I<0m8qA^ zxeJr%<&2M(3jMC~>20NRxmE9ynnvi+D-Mr4H$5Y9QhW(5CE`$QJrQagJ*AFbsHL^l zs}}D!qoer?%=k#Sa3>q)a`M9YlrxF=k~k)2;KVl0%AT)wyi00$8`qOoDsQ5$Bd(}_ zYi=%T^j8sOC>CbH==ypXuZGcmwr4wU#C=Fp+MG`nuV;IZ@faqZfrPREXXA0xDS?0~ zVQz0RS}l?Q&Y#}Wp!B7a=K(bZW-^Hla5f7_2$HW1peZTdCCT+5(JNG8k}%!4BRP*G zM*5LpSo(tu2*Uy(h10*uxDQS6UdtqA${aZ$r-{P9dULt*hwyVr6D*DQtbQ+OL;)LX zLh5UxVTpeT$gRnI0!v(E*sSit>gSj<)nsvw#Ue)>p(DRiM{4#)$`Wiweeh;_oI&(Lup-1gG8c&%mVZju8 zY0h=0T<1f827j&@{Kqx1(Qm#^om+3fOKWNCy1DZ)XIBEBI2tNpT{j#eI>H_bbQrxK zWdw9ojtK|z(b%QJW2YL7m}LQugou$$ge|5kYg*#_j_aV(jC}_Hb^2_{q}Fw?LYlOK z#+Gu~#jrIgvwW8%*1IlV`Hb)fVJGy0hzDVNI^{uy#=W$2Q>geMh9=ROOZ6WZ-4<2g zZSCm7m&Z+kx9JT7W(w+AYWn7PF75;8z-^I;wMgMsJRt|xm_~7{R2%RCheo~L?Q&Wh zOyz(V#(klRw@pFMXcb0W*t>;tmbqmXlOYNEvqR#zgsO2iUn}IS7Spwo1cO!2_DHQ76qc|wU~x{?XO{J?kzqZm&v`<{2U$+# zv|@d>sU1I@PF9##U6&r($*Ri={k)FeIL!o{r?_0jhM_NUD>x$sw zh@Q~8Ut9`H#LePV?{SriO<>A>U=tsQ-y@aq-b1;|T`e8Wy|p;5rNXPR1EX_c^z6Va z7qixZiG*d=YrRR&t1cau>xLoxqi|08n!s`mrpr|fo$gl`u|m6CJxz6tVNnI!O!#Oi z85V&ZF?vptBVa|mOKK@_Qg>k{ERalS?TwwLs9MMRiU>$IQ5iY<5M30vWQ$k0^Q{N(Rfh{^N@FaZO_3%HgsVtVp zS#;iq@59Sm*bEm4i&-(WT*n2X|F|Zx-u==-#|5IS_hdzP?=Y;t4dt&m1D<~i7}nu* zSck!|PCPJ_y73t6Ko8E|) z3vphS)|3m30Xl4sy`*L;BbeUr^Oze6pAny-SRjR^vG_`llc60}Wi?w(!{}y11jrBG^v_Pm>B+N5(>lE^i?9=t_%bCb(Ft9mD_X-;77J}2@Kk|FlZkJ zQ3mk04*`vXFE`fd7(i3OWrm&H8mU{oNJ+zO;%C3?NHBd}$j4;8f2HlA67s z@$`#;0X%{vCy`AHLMq1%!#r%rI}CT6o&XtX3rQY0#X!>gPl7eLM%byvtVNbdKujym@C1n$@9pH zXdDFA68q8MN&AHajm9ZhJ(TPnjU645dkkJ5PjO>n@X@GM$I{)T2?i^)yHQ1&N8{BD zo^IW{vrfjjiR&pGKmaZ`&=z-&!TD_I=eLT8bPBd35o00J>ua)jEbi3-YQkI=3HOIG z7@}4q^`)_Rji42V$6@ey!9_7a3_LkBa1 zCZi4=vCfT1vc_WxbW}AS7*zX+GuP*WcjzxZKe+0tt&?e`aGCsS-oQ!rFcTHDQdw2r zq*mW#%67WfZdUMA$zdXJ1%xxMfcg+WuXHIDl=)^*UUmHp)j!Q>H7lny=)3E4oWbd- zfQW5i$;Q{TcZ4TPB4`>g$fJ3dPEH+B#Nf%)q)Aj$gc{v^_~}Eg>aM*AZ7Jjis8`y9^gCI4NBRPTH}RyuF12 z$*`%|1{bTzjHy`Ub)77!$n)LAhif*$uSyYDFv-%-)ywI%rK-dnScE*SW*Ie&9GZ$9 ztbI=0+5x6#Q`$TBg+eLgX8MdYPsP6IH)1^vAHqr&`Nb03kfv$aum^y|IsoQ6fYLZy zVIT^vmvQwBPIL!TzvD?_CBtC=Uz#8T%i4+VZY^Ym4A|4huAO0LfBhW*V!(G8xEn_U zHRn!V4mD@>IKoEmC%S{0Od)33$PdQGxzgpV^z5ArUfJSCF!6)ruEm2Bn5Iid(XaIN7UthaaacLY%2w2A{ii-$2kd()rq zGe0-c(vqnA0dT~sjG#v6AuAIb;^kZw=-+oZ1AEb19{CDdf60wPC?x06H)Jucw0?gs zyswRsfOfIunn89~aETLwsRs0IBJ32BQm~ z9oIdxI_>GYr>hf8CB8I6;)%-VGqKZu1~*cqa1tw=qX6M0Ocq>k;?>I(O3us*X^dU~ zV+YjH()qJ(*{G-69*rMT56P*y`TZc&9Kf#%42qiI+Y>E^+Wu|wb)nc;u4~)lkdqC% z#~~-{ef`qO`PsOSO`=||@iCs!JD| z_FPti>_8>5y@WpxTMGC3_sjHsz>>qk0;ak?3n+G+n(9VuB?IQ+K}=rkJ9BWEDfnz{ z!5MdfX2DLAM3KkI*!>?8@*(ekj*vbncsR~}PL`$MrCbOAw-8AY5s%kCf81Bu)38uwP@<=yvKR6LsJFgp5?{8m>PWc zd0zaEtZ6ZvcXU*R7Z}@3M{?b)5UJss_ zFGpX`5D55*`8jA=La;zND?b;VPKXhR=H=(3EiaQ(oH^+Z8C$t@#3>#Is-r(xe7w z366qKXt1*O82Sq1yhg^VhpJhR{cI`vtDP_(q*Aj;2t zElgQfP=WSj3hekr1&7h~%wW5e)dfe<)`c;4FUkv!p<|0O?TWuFs6rnXmD)v}EI5IF zUR-6z`mvxI-C5dTSMj{y6e`JjZI{LWP@qCYjsUDH5XfuLqihsxFY*@1Ytd>2im_Mq z6Ufh^4+@lN-!xPp*Pz$AsMNk9Mj*d{n)6VVeN?7EUWe8fpay&KB7yueI$VHW+w+$Q z5dhy)HVRtw};(Z*#c*rE7Kf&4mpxg5nf@Q(}R-=m7GB9!SMs}{%`P-77)b*Qfs z$bUqoD^Zn$__jdah#JL9HP3X-=BycRQww2#Qhqj<#$KoGs z<<023ttiGZs>N3R5S{q~WjaQ^ww1S_H``FDV=-4Ke~dOMQI(^}L@0lPwrxiZj;xR@ zq5K&-wHv*5te7K|zd$SZAc2#-NGN}a*6c&UPEp?o<*(4s`%#P&Un7+Nj&>eEnNIvV zq5L(veE^j@slF4+-=eZFQI%8FEus89+H?>#IH`UX%Kt>y4x-miP0xgKIWGAM2|Oy^ z3FSFh^A!sAP<{}~b8*X8St!OsZf7UY$9E2)Opg~acJe}e?iecds9$U+UyienqbiU3 zt#{;%8aE7blp_AFRGwE_!rfF)sk6YVj|5`OlysXxGj)=H04kaK2uN*EaqA`XTT&U6$ z6j>=DhzJYbP7=g!^3>A4fAjtS^LzLnzWHCwq7{SiK|iqw;Y2I$gGc>D7ED=I+z*o% ziCe%zD;|KWmxy05xvjA^#1kJ7RS3Ol#abA?OfJ*2AU&VhG_j zD~6!C+E#}W!u?apMB!1B}Z^dSK=NeJP=oeOOfzE40 z6Z@8|cnt1bBf1!QX2o_m6eflkUS-3MShGK|Nakach-iNVc{n6Cq%B=@CuCFB5Fcp(1w8l*fB=5g!r2_ zyb2e_h@M~?v*92_#)y$%8n_TDCz#Q1wQ9EOi#oeYVQ`!>7|4{sB9VuxYF5x6u? z{E5D08|tt;PSiy6^Bj&sLxgCFWiN1e3r^l4dScMZ;cXbdLySa^ox=$1oQTaRN(u=a zPQZf+A}5)1IGlurN#ag2y~g1bod1mYlkiOrr=f9*s7aCEa5w|n6w#7`zvFNgYCk7> zQgkDSa}X=VHhcG!!+{var96pAnY2r^tl|v%{ z`|c7oIdYK0FX6;pq9sS`I9!6+yF^b8HgmWP9W%s8?mNaI(uo;jkv;EoxS4LbM`YR5 z&EXc>dylwf&sh$)(LJ-oFM9?!+)gje5>+-0a#%x;-Y1$|c9X-Mbl^VG<;WO^yXk}b z#E=6x&0&xpo+B1laE8Nu^z_`<+e>CS+)qEABW{;zj>7}=(H!x+LI#H_4b2nPmH!oo zwRB*fXfD$-hjsMHJkec|=j>Qd4@QaM%3o#25Ir3wmdyAU?bt~F86|S2W3?TR(p?M0 zo#|U+$0i!Mut5Bo5t|*Gsj)!R%zVL)Ewp)&Xqh3|j>qVxM?}vw|H6*#^wUSg$i%np z*g@Ylh$SmjW5*Np6NAWEeQkC;Mei*Uca}r9;~A63XJrp5`r&r) z=lXW>I87UOfSMaU%;OA=y=_{qxh25kEbXrWJvYCN$2t0-28`Uk9v-7Kx)UsUKAp!! zdSn;KdFER@KBOP-0(V|yjK{}xVHf!G@~3$;=z-m!<^^YX{E~)ugO(RDcwC}4_kf<~ zdtSh0dN&A0p2;F0#zujIr66b(a5MXCZvf;1hoN zvmev~-_HfCVGsTWT0z-c0`6o>2S6`~ZWM4gd!m3*;HwcZ$UacPQrNdkz5E(0oL|18i$8_zOd=0;+7j7SuxXSs{S6tmZIig`rUa>)6y`&=Jj%}h9o$8pw?%AXCz`=u6xkzUGduYns71j# z5nI^!d!QBN9})2wJKX|$k)ut-b{1^`qbU5oh#jo16#|xGU$=-S*u_?mi+yKBJjEtk z!Cj13L_EWWj)A|}d`(1+?QH|K*nCsOZZ^~gT5)h(#9p?w9rWVJT@lZ*o^~*b@xF+C z>`^;dO5(o|v7a@+4{}N9ISDVZ_d38`Qucy`m)VCM;4g`+mN0OIojwj~iHVnRfE_vs zT1hZd!mF(7BiDUB3LILzwLfL!W$OTz2y>=|&E#&3{t zg!OiUztmGBq0WXhP)mb*BphX1x?)9c#38&bN9`LUZos)2yJ?n{$n|gQEOKn5Cb@YuVWY~moJ(+obd4;zs!y)+z%CAnTOs|krov!q>DmkT6R>~d%A6M;k$tkH$xjGi!>6M-96ni60j7ur6 zuK4C?|0sQ2;+C! diff --git a/heapster-saw/examples/rust_data.rs b/heapster-saw/examples/rust_data.rs index f50c96ef50..cb021bba12 100644 --- a/heapster-saw/examples/rust_data.rs +++ b/heapster-saw/examples/rust_data.rs @@ -179,7 +179,7 @@ pub fn extract_from_result_infallible <'a> (r:&'a Result) -> u64 /* Sum of two types; yes, this is like Result, but defined locally so we can * make an impl block on it */ #[derive(Clone, Debug, PartialEq)] -#[repr(C)] +#[repr(C,u64)] pub enum Sum { Left (X), Right (Y) From 9d86918e0d2d08c51f85d628c6aedf8ef87c4eb5 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Fri, 6 May 2022 13:28:14 -0700 Subject: [PATCH 7/8] changed proveVarLLVMArray_FromArray to actuall add and remove the borrows it computes as it computes them; fixed case 4 of proveVarLLVMArrayH so that it only uses the unborrowed ranges for permissions on the LHS --- .../src/Verifier/SAW/Heapster/Implication.hs | 86 +++++++++---------- 1 file changed, 42 insertions(+), 44 deletions(-) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs index 64b2831749..b4a18de8d8 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs @@ -5089,7 +5089,7 @@ implLLVMArrayReturn :: implLLVMArrayReturn x ap ret_ap = implSimplM Proxy (SImpl_LLVMArrayReturn x ap ret_ap) >>> pure (llvmArrayRemBorrow (llvmSubArrayBorrow ap ret_ap) $ - llvmArrayAddArrayBorrows ap ret_ap) + llvmArrayAddArrayBorrows ap ret_ap) -- | Add a borrow to an LLVM array permission by borrowing its corresponding -- permission, failing if that is not possible because the borrow is not in @@ -6743,13 +6743,11 @@ proveVarLLVMArrayH x psubst ps mb_ap "proveVarLLVMArrayH: incomplete array borrows" >>>= \bs -> if bvEq off (llvmArrayOffset ap_lhs) && bvEq len (llvmArrayLen ap_lhs) then - proveVarLLVMArray_FromArray x ap_lhs len bs mb_ap >>>= \_ -> - return () + proveVarLLVMArray_FromArray x ap_lhs len bs mb_ap else implLLVMArrayGet x ap_lhs off len >>>= \ap_lhs' -> recombinePerm x (ValPerm_LLVMArray ap_lhs') >>> - proveVarLLVMArray_FromArray x (llvmMakeSubArray ap_lhs off len) len bs mb_ap >>>= \_ -> - return () + proveVarLLVMArray_FromArray x (llvmMakeSubArray ap_lhs off len) len bs mb_ap where -- Test if an atomic permission is a "suitable" array permission for the -- given offset, length, and stride, meaning that it has the required @@ -6802,7 +6800,7 @@ proveVarLLVMArrayH x psubst ps mb_ap proveVarLLVMArrayH x psubst ps mb_ap | Just ap <- partialSubst psubst mb_ap , len <- llvmArrayLen ap - , lhs_cells@(lhs_cell_rng:_) <- mapMaybe (permCells ap) ps + , lhs_cells@(lhs_cell_rng:_) <- concatMap (permCells ap) ps , rhs_cells <- map llvmArrayBorrowCells (llvmArrayBorrows ap) , Just cells <- gatherCoveringRanges (llvmArrayCells ap) (lhs_cells ++ rhs_cells) @@ -6817,22 +6815,22 @@ proveVarLLVMArrayH x psubst ps mb_ap proveVarLLVMBlock x ps mb_cell_bp >>> implLLVMArrayBorrowed x cell_bp ap_borrowed >>> recombinePerm x (ValPerm_Conj1 (Perm_LLVMBlock cell_bp)) >>> - proveVarLLVMArray_FromArray x ap_borrowed len (llvmArrayBorrows ap) mb_ap >>>= \_ -> - return () + proveVarLLVMArray_FromArray x ap_borrowed len (llvmArrayBorrows ap) mb_ap where -- Comupte the range of array cells in ap that an atomic permission -- corresponds to, if any, as long as it is not wholly borrowed permCells :: (1 <= w, KnownNat w) => LLVMArrayPerm w -> - AtomicPerm (LLVMPointerType w) -> Maybe (BVRange w) - permCells ap p = permOffsets p >>= llvmArrayAbsOffsetsToCells ap + AtomicPerm (LLVMPointerType w) -> [BVRange w] + permCells ap p = mapMaybe (llvmArrayAbsOffsetsToCells ap) (permOffsets p) -- Compute the range of offsets in an atomic permission, if any, using the -- whole range of an array permission iff it is not fully borrowed permOffsets :: (1 <= w, KnownNat w) => AtomicPerm (LLVMPointerType w) -> - Maybe (BVRange w) - permOffsets (Perm_LLVMArray ap) | llvmArrayIsBorrowed ap = Nothing - permOffsets (Perm_LLVMArray ap) = Just $ llvmArrayRange ap - permOffsets p = llvmAtomicPermRange p + [BVRange w] + permOffsets (Perm_LLVMArray ap) = + bvRangesDelete (llvmArrayRange ap) $ + map (llvmArrayAbsBorrowRange ap) (llvmArrayBorrows ap) + permOffsets p = maybeToList $ llvmAtomicPermRange p -- Convert a range to a borrow cellRangeToBorrow :: (1 <= w, KnownNat w) => BVRange w -> LLVMArrayBorrow w @@ -6857,16 +6855,14 @@ proveVarLLVMArrayH x _ ps mb_ap = (mbValPerm_LLVMArray mb_ap) --- | Prove an array permission @mb_ap@ with borrows set to the supplied list and --- length set to that of @ap_lhs@ using the array permission @ap_lhs@ on top of --- the stack, assuming that @ap_lhs@ has the same offset and stride as @ap@. --- Return the resulting array permission that was proved. +-- | Prove an array permission @mb_ap@ using the array permission @ap_lhs@ on +-- top of the stack, assuming that @ap_lhs@ has the same offset and stride as +-- @ap@ and that @ap@ has length and borrows given by the supplied arguments. proveVarLLVMArray_FromArray :: (1 <= w, KnownNat w, NuMatchingAny1 r) => ExprVar (LLVMPointerType w) -> LLVMArrayPerm w -> PermExpr (BVType w) -> [LLVMArrayBorrow w] -> Mb vars (LLVMArrayPerm w) -> - ImplM vars s r (ps :> LLVMPointerType w) (ps :> LLVMPointerType w) - (LLVMArrayPerm w) + ImplM vars s r (ps :> LLVMPointerType w) (ps :> LLVMPointerType w) () proveVarLLVMArray_FromArray x ap_lhs len bs mb_ap = implTraceM (\info -> @@ -6874,7 +6870,8 @@ proveVarLLVMArray_FromArray x ap_lhs len bs mb_ap = permPretty info x <> colon <> align (sep [permPretty info (ValPerm_LLVMArray ap_lhs), pretty "-o", - PP.group (permPretty info mb_ap)])) >>> + PP.group (permPretty info mb_ap), + pretty "bs = " <> permPretty info bs])) >>> proveVarLLVMArray_FromArrayH x ap_lhs len bs mb_ap -- | The implementation of 'proveVarLLVMArray_FromArray' @@ -6882,8 +6879,7 @@ proveVarLLVMArray_FromArrayH :: (1 <= w, KnownNat w, NuMatchingAny1 r) => ExprVar (LLVMPointerType w) -> LLVMArrayPerm w -> PermExpr (BVType w) -> [LLVMArrayBorrow w] -> Mb vars (LLVMArrayPerm w) -> - ImplM vars s r (ps :> LLVMPointerType w) (ps :> LLVMPointerType w) - (LLVMArrayPerm w) + ImplM vars s r (ps :> LLVMPointerType w) (ps :> LLVMPointerType w) () -- If there is a borrow in ap_lhs that is not in ap, return it to ap_lhs -- @@ -6892,21 +6888,25 @@ proveVarLLVMArray_FromArrayH :: -- allows some of ap_ret to be borrowed proveVarLLVMArray_FromArrayH x ap_lhs len bs mb_ap | Just b <- find (flip notElem bs) (llvmArrayBorrows ap_lhs) = - -- Find a borrow on the rhs that overlaps b and subtract the overlapped part - - -- Prove the rest of ap with b borrowed - proveVarLLVMArray_FromArray x ap_lhs len (b:bs) mb_ap >>>= \ap' -> -- Prove the borrowed perm - let p = permForLLVMArrayBorrow ap' b in + let p = permForLLVMArrayBorrow ap_lhs b in mbVarsM p >>>= \mb_p -> - implTraceM (\info -> pretty "Proving borrowed permission..." <+> permPretty info (ap', b) <+> permPretty info p) >>> + implTraceM (\info -> + hang 2 $ + sep [pretty "Proving borrowed permission...", + permPretty info p, + pretty "For borrow:" <+> permPretty info b, + pretty "From array:" <+> permPretty info ap_lhs]) >>> proveVarImplInt x mb_p >>> - implSwapM x (ValPerm_Conj1 $ Perm_LLVMArray ap') x p >>> + implSwapM x (ValPerm_Conj1 $ Perm_LLVMArray ap_lhs) x p >>> + + -- Return the borrowed perm to ap_lhs to get ap + implLLVMArrayReturnBorrow x ap_lhs b >>> - -- Return the borrowed perm to ap' to get ap - implLLVMArrayReturnBorrow x ap' b >>> - return (ap' { llvmArrayBorrows = bs }) + -- Continue proving mb_ap with the updated ap_lhs + let ap_lhs' = llvmArrayRemBorrow b ap_lhs in + proveVarLLVMArray_FromArray x ap_lhs' len bs mb_ap -- If there is a borrow in ap that is not in ap_lhs, borrow it from ap_lhs. Note -- the assymmetry with the previous case: we only add borrows if we definitely @@ -6914,16 +6914,15 @@ proveVarLLVMArray_FromArrayH x ap_lhs len bs mb_ap proveVarLLVMArray_FromArrayH x ap_lhs len bs mb_ap | Just b <- find (flip notElem (llvmArrayBorrows ap_lhs)) bs = - -- Prove the rest of ap without b borrowed - proveVarLLVMArray_FromArray x ap_lhs len (delete b bs) mb_ap >>>= \ap' -> - -- Borrow the permission if that is possible; this will fail if ap has a - -- borrow that is not actually in its range. Note that the borrow is always - -- added to the front of the list of borrows, so we need to rearrange. - implLLVMArrayBorrowBorrow x ap' b >>>= \p -> + -- borrow that is not actually in its range + implLLVMArrayBorrowBorrow x ap_lhs b >>>= \p -> recombinePerm x p >>> - implLLVMArrayRearrange x (llvmArrayAddBorrow b ap') bs >>> - return (ap' { llvmArrayBorrows = bs }) + + -- Continue proving mb_ap with the updated ap_lhs + let ap_lhs' = llvmArrayAddBorrow b ap_lhs in + proveVarLLVMArray_FromArray x ap_lhs' len bs mb_ap + -- If we get here then ap_lhs and ap have the same borrows, offset, length, and -- stride, so equalize their modalities, prove the shape of mb_ap from that of @@ -6961,8 +6960,7 @@ proveVarLLVMArray_FromArrayH x ap_lhs _ bs mb_ap = return (ap_lhs'' { llvmArrayCellShape = sh })) >>>= \ap_lhs''' -> -- Finally, rearrange the borrows of ap_lhs to match bs - implLLVMArrayRearrange x ap_lhs''' bs >>> - return (ap_lhs''' { llvmArrayBorrows = bs }) + implLLVMArrayRearrange x ap_lhs''' bs ---------------------------------------------------------------------- @@ -9103,7 +9101,7 @@ checkVarImpl ps act = 0 /= permImplSucceeds (evalState st (toClosed 0)) emptyPermEnv emptyPPInfo "checkVarImpl" - (DebugLevel 1) + (DebugLevel 2) NameMap.empty Nothing LittleEndian From b7f6308caf3683a2e1757b0075a4532fa761c894 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Fri, 6 May 2022 15:58:36 -0700 Subject: [PATCH 8/8] changed some comments to address feedback from Matt Y --- .../src/Verifier/SAW/Heapster/Implication.hs | 48 +++++++++++-------- 1 file changed, 29 insertions(+), 19 deletions(-) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs index b4a18de8d8..b7a82cb4e0 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs @@ -780,8 +780,8 @@ data SimplImpl ps_in ps_out where -- translation to give a default value to the cells of the output array -- permission: -- - -- > x:[l2]memblock(rw,off1, -o x:[l2]memblock(rw,off1, x:[l2]memblock(rw,off1,stride,sh) + -- > -o x:[l2]memblock(rw,off1,stride,sh) -- > * x:[l]array(rw,off, ExprVar (LLVMPointerType w) -> @@ -6690,8 +6690,10 @@ proveVarLLVMArray x ps mb_ap = -- -- 4. By eliminating a @memblock@ permission with array shape. -- +-- NOTE: these "ways" do *not* line up with the cases of the function, labeled +-- as "case 1", "case 2", etc. outputs in the code below. -- --- To determine which case to use, the algorithm searches for a permission +-- To determine which way to use, the algorithm searches for a permission -- currently held on the left that is either an array permission with exactly -- the required offset and length or that includes them in its range, or is a -- block permission that that includes the required offset and length in its @@ -6702,9 +6704,9 @@ proveVarLLVMArray x ps mb_ap = -- we already hold on the left, so they can be returned, or to be in the desired -- output permission, so we do not have to return them. -- --- In all of these cases, an array permission with the required offset and --- length is either found on the left or created, and all cases then reduce to --- case 1. At this point, the algorithm equalizes the borrows, meaning that it +-- In all of these ways, an array permission with the required offset and +-- length is either found on the left or created, and all ways then reduce to +-- way 1. At this point, the algorithm equalizes the borrows, meaning that it -- returns any borrows on the left that are not on the right (where the right is -- the desired output permission) and borrows any borrows on the right that are -- not on the left. It then adjusts the read/write and lifetime modalities and @@ -6724,9 +6726,9 @@ proveVarLLVMArrayH x psubst ps mb_ap partialSubstForceM mb_ap "proveVarLLVMArray: incomplete psubst" >>>= \ap -> implLLVMArrayEmpty x ap --- If we have a single array permission that covers the RHS, then we are in case --- 1 or 2, so either use that or borrow or copy a portion of it and proceed to --- proveVarLLVMArray_FromArray +-- If we have a single array permission that covers the RHS, then we are using +-- way 1 or 2, so either use that or borrow or copy a portion of it and proceed +-- to proveVarLLVMArray_FromArray proveVarLLVMArrayH x psubst ps mb_ap | Just off <- partialSubst psubst $ mbLLVMArrayOffset mb_ap , Just len <- partialSubst psubst $ mbLLVMArrayLen mb_ap @@ -6768,7 +6770,10 @@ proveVarLLVMArrayH x psubst ps mb_ap suitableAP _ _ _ _ = False -- Check if there is a block that contains the required offset and length, in --- which case eliminate it +-- which case eliminate it, allowing us to either satisfy way 4 (eliminate a +-- memblock to an array), or to generate a set of permissions that can contain +-- array and/or pointer permissions that can be used to satisfy one of ways 1-3 +-- when we recurse proveVarLLVMArrayH x psubst ps mb_ap | Just rng <- partialSubst psubst $ mbLLVMArrayRange mb_ap , Just i <- findIndex (\p -> isLLVMBlockPerm p && @@ -6778,9 +6783,10 @@ proveVarLLVMArrayH x psubst ps mb_ap implElimAppendIthLLVMBlock x ps i >>>= \ps' -> proveVarLLVMArray x ps' mb_ap --- The following step needs the modalities of mb_ap to be determined, so we do --- that by finding an arbitrary permission on the left that overlaps with a --- non-borrowed portion of mb_ap and using it to instantiate the modalities +-- This case prepares us to hit case 4 below, which needs the modalities of +-- mb_ap to be determined; this is done by finding an arbitrary permission on +-- the left that overlaps with a non-borrowed portion of mb_ap and using it to +-- instantiate the modalities proveVarLLVMArrayH x psubst ps mb_ap | Just off <- partialSubst psubst $ mbLLVMArrayOffset mb_ap , Just lenBytes <- partialSubst psubst $ mbLLVMArrayLenBytes mb_ap @@ -6794,9 +6800,10 @@ proveVarLLVMArrayH x psubst ps mb_ap tryUnifyVars l (mbLLVMArrayLifetime mb_ap) >>> proveVarLLVMArray x ps mb_ap --- Otherwise, try and build a completely borrowed array whose borrows are made --- up of either borrows in the desired output permission mb_ap or are ranges on --- permissions that we already hold on the left +-- If none of the above match, try and build a completely borrowed array whose +-- borrows are made up of either borrows in the desired output permission mb_ap +-- or are ranges on permissions that we already hold on the left, which is way 3 +-- for building an array permission proveVarLLVMArrayH x psubst ps mb_ap | Just ap <- partialSubst psubst mb_ap , len <- llvmArrayLen ap @@ -6883,9 +6890,12 @@ proveVarLLVMArray_FromArrayH :: -- If there is a borrow in ap_lhs that is not in ap, return it to ap_lhs -- --- FIXME: when an array ap_ret is being borrowed from ap_lhs, this code requires --- all of it to be returned, with no borrows, even though it could be that ap --- allows some of ap_ret to be borrowed +-- FIXME: when an array is returned to ap_lhs, this code requires all of it to +-- be returned, with no borrows, even though it could be that some portion of +-- that borrow is borrowed in mb_ap. E.g., if ap_lhs has the range [0,8) +-- borrowed while mb_ap only needs to have [2,3) borrowed, this code will first +-- return all of [0,8) and then borrow [2,3), while the array return rule allows +-- all of [0,8) except [2,3) to be returned as one step. proveVarLLVMArray_FromArrayH x ap_lhs len bs mb_ap | Just b <- find (flip notElem bs) (llvmArrayBorrows ap_lhs) =