From 74dd92af155dfcac2e3139628670e24bf8d8e72d Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sat, 16 May 2026 11:33:14 -0700 Subject: [PATCH 1/5] PO: proof obligations for command injection --- chb/api/XXPredicate.py | 31 +++++++- chb/app/FnProofObligations.py | 31 ++++++-- chb/app/FnXPODictionary.py | 32 +++++++- chb/app/XPOPredicate.py | 135 ++++++++++++++++++++++++++++------ 4 files changed, 198 insertions(+), 31 deletions(-) diff --git a/chb/api/XXPredicate.py b/chb/api/XXPredicate.py index 6fcdfe1b..77536b7f 100644 --- a/chb/api/XXPredicate.py +++ b/chb/api/XXPredicate.py @@ -26,7 +26,7 @@ # ------------------------------------------------------------------------------ -from typing import List, TYPE_CHECKING +from typing import List, Optional, TYPE_CHECKING from chb.api.InterfaceDictionaryRecord import ( InterfaceDictionaryRecord, apiregistry) @@ -925,6 +925,35 @@ def __str__(self) -> str: return "tainted(" + str(self.term) + ")" +@apiregistry.register_tag("tfs", XXPredicate) +class XXPTrustedOsCmdFmtString(XXPredicate): + + def __init__( + self, ixd: "InterfaceDictionary", ixval: IndexedTableValue) -> None: + XXPredicate.__init__(self, ixd, ixval) + + @property + def is_xp_trusted_os_cmd_string(self) -> bool: + return True + + @property + def fmt(self) -> "BTerm": + return self.id.bterm(self.args[0]) + + @property + def fmtkind(self) -> str: + return self.tags[1] + + @property + def optlen(self) -> Optional["BTerm"]: + if self.args[1] == -1: + return None + return self.id.bterm(self.args[1]) + + def __str__(self) -> str: + return "trusted-os-cmd-fmt-string(" + str(self.fmt) + ", " + self.fmtkind + ", " + str(self.optlen) + ")" + + @apiregistry.register_tag("v", XXPredicate) class XXPValidMem(XXPredicate): """Term points to valid memory diff --git a/chb/app/FnProofObligations.py b/chb/app/FnProofObligations.py index 18189360..5cd8a204 100644 --- a/chb/app/FnProofObligations.py +++ b/chb/app/FnProofObligations.py @@ -47,13 +47,20 @@ "o": "open", "dis": "safe", "del": "delegated", + "local": "delegated-local", "v": "violation" } class POStatus: - def __init__(self, tag: str) -> None: - self._tag = tag + def __init__(self, xpod: "FnXPODictionary", node: ET.Element) -> None: + self.node = node + self._xpod = xpod + self._tag = self.node.get("s", "none") + + @property + def xpod(self) -> "FnXPODictionary": + return self._xpod @property def tag(self) -> str: @@ -71,11 +78,20 @@ def is_discharged(self) -> bool: def is_delegated(self) -> bool: return self.tag == "del" + @property + def is_delegated_local(self) -> bool: + return self.tag == "local" + @property def is_violated(self) -> bool: return self.tag == "v" + def get_iaddr(self) -> str: + return self.node.get("iaddr", "?") + def __str__(self) -> str: + if self.is_delegated_local: + return "delegated-local: " + self.get_iaddr() return po_status_strings.get(self.tag, "?") @@ -173,11 +189,12 @@ def proofobligations(self) -> Dict[str, List[ProofObligation]]: self._store[iaddr] = [] for xxpo in xloc.findall("po"): xpo = self.xpod.read_xml_xpo_predicate(xxpo) - statustag = xxpo.get("s", "o") - status = POStatus(statustag) - msg = xxpo.get("m", "none") - po = ProofObligation(iaddr, xpo, status, msg) - self._store[iaddr].append(po) + xstatus = xxpo.find("status") + if xstatus is not None: + status = POStatus(self.xpod, xstatus) + msg = xxpo.get("m", "none") + po = ProofObligation(iaddr, xpo, status, msg) + self._store[iaddr].append(po) return self._store def open_proofobligations(self) -> Dict[str, List[ProofObligation]]: diff --git a/chb/app/FnXPODictionary.py b/chb/app/FnXPODictionary.py index a035dbfb..2ebdb709 100644 --- a/chb/app/FnXPODictionary.py +++ b/chb/app/FnXPODictionary.py @@ -28,9 +28,9 @@ import xml.etree.ElementTree as ET -from typing import List, TYPE_CHECKING +from typing import List, Optional, TYPE_CHECKING -from chb.app.FnXPODictionaryRecord import xporegistry +from chb.app.FnXPODictionaryRecord import xporegistry, FnXPODictionaryRecord from chb.app.XPOPredicate import XPOPredicate import chb.util.IndexedTable as IT @@ -41,6 +41,28 @@ from chb.app.Function import Function from chb.bctypes.BCDictionary import BCDictionary from chb.invariants.FnXprDictionary import FnXprDictionary + from chb.invariants.XXpr import XXpr + + +class XPOFormatArgument(FnXPODictionaryRecord): + + def __init__(self, xpod: "FnXPODictionary", ixval: IT.IndexedTableValue) -> None: + FnXPODictionaryRecord.__init__(self, xpod, ixval) + + @property + def argument(self) -> "XXpr": + return self.xd.xpr(self.args[0]) + + @property + def converter(self) -> str: + return self.tags[0] + + @property + def fieldwidth(self) -> Optional[int]: + return None if self.tags[1] == "other" else int(self.tags[1]) + + def __str__(self) -> str: + return "(" + self.converter + ", " + str(self.argument) + ")" class FnXPODictionary: @@ -50,8 +72,10 @@ def __init__( fn: "Function", xnode: ET.Element) -> None: self._fn = fn + self.format_arg_table = IT.IndexedTable("format-arg-table") self.xpo_predicate_table = IT.IndexedTable("xpo-predicate-table") self.tables: List[IT.IndexedTable] = [ + self.format_arg_table, self.xpo_predicate_table ] self.initialize(xnode) @@ -82,6 +106,10 @@ def xpo_predicate(self, ix: int) -> XPOPredicate: raise UF.CHBError( "Illegal xpo predicate index value: " + str(ix)) + def format_arg(self, ix: int) -> XPOFormatArgument: + return XPOFormatArgument(self, self.format_arg_table.retrieve(ix)) + + # ------------------------------------- initialize dictionary from file --- def read_xml_xpo_predicate(self, xnode: ET.Element) -> XPOPredicate: diff --git a/chb/app/XPOPredicate.py b/chb/app/XPOPredicate.py index 189a8bb0..fa1b7998 100644 --- a/chb/app/XPOPredicate.py +++ b/chb/app/XPOPredicate.py @@ -26,7 +26,7 @@ # ------------------------------------------------------------------------------ """Predicate over expressions in a function context.""" -from typing import List, TYPE_CHECKING +from typing import List, Optional, TYPE_CHECKING from chb.app.FnXPODictionaryRecord import ( FnXPODictionaryRecord, xporegistry) @@ -37,7 +37,7 @@ if TYPE_CHECKING: from chb.api.BTerm import BTerm - from chb.app.FnXPODictionary import FnXPODictionary + from chb.app.FnXPODictionary import FnXPODictionary, XPOFormatArgument from chb.bctypes.BCTyp import BCTyp from chb.invariants.XXpr import XXpr @@ -171,7 +171,7 @@ def is_xpo_validmem(self) -> bool: @property def is_xpo_disjunction(self) -> bool: return False - + @xporegistry.register_tag("ab", XPOPredicate) class XPOAllocationBase(XPOPredicate): @@ -380,7 +380,7 @@ class XPOFunctionPointer(XPOPredicate): def __init__( self, xpod: "FnXPODictionary", ixval: IndexedTableValue) -> None: XPOPredicate.__init__(self, xpod, ixval) - + @property def is_xpo_function_pointer(self) -> bool: return True @@ -458,7 +458,7 @@ def __str__(self) -> str: + str(self.size) + ")") - + @xporegistry.register_tag("ifs", XPOPredicate) class XPOInputFormatString(XPOPredicate): """Expression points to a format string for input (scanf). @@ -531,8 +531,8 @@ def size(self) -> "XXpr": def __str__(self) -> str: return "new-memory(" + str(self.pointer) + ", " + str(self.size) + ")" - - + + @xporegistry.register_tag("sa", XPOPredicate) class XPOStackAddress(XPOPredicate): """Expression is a stack address. @@ -542,7 +542,7 @@ class XPOStackAddress(XPOPredicate): def __init__( self, xpod: "FnXPODictionary", ixval: IndexedTableValue) -> None: - XPOPredicate.__init__(self, xpod, ixval) + XPOPredicate.__init__(self, xpod, ixval) @property def is_xpo_stack_address(self) -> bool: @@ -565,7 +565,7 @@ class XPOHeapAddress(XPOPredicate): def __init__( self, xpod: "FnXPODictionary", ixval: IndexedTableValue) -> None: - XPOPredicate.__init__(self, xpod, ixval) + XPOPredicate.__init__(self, xpod, ixval) @property def is_xpo_heap_address(self) -> bool: @@ -577,7 +577,7 @@ def expr(self) -> "XXpr": def __str__(self) -> str: return "heap-address(" + str(self.expr) + ")" - + @xporegistry.register_tag("ga", XPOPredicate) class XPOGlobalAddress(XPOPredicate): @@ -588,7 +588,7 @@ class XPOGlobalAddress(XPOPredicate): def __init__( self, xpod: "FnXPODictionary", ixval: IndexedTableValue) -> None: - XPOPredicate.__init__(self, xpod, ixval) + XPOPredicate.__init__(self, xpod, ixval) @property def is_xpo_global_address(self) -> bool: @@ -600,7 +600,7 @@ def expr(self) -> "XXpr": def __str__(self) -> str: return "global-address(" + str(self.expr) + ")" - + @xporegistry.register_tag("no", XPOPredicate) class XPONoOverlap(XPOPredicate): @@ -629,7 +629,7 @@ def pointer2(self) -> "XXpr": def __str__(self) -> str: return ( "no-overlap(" + str(self.pointer1) + ", " + str(self.pointer2) + ")") - + @xporegistry.register_tag("nn", XPOPredicate) class XPONotNull(XPOPredicate): @@ -652,7 +652,7 @@ def pointer(self) -> "XXpr": def __str__(self) -> str: return "not-null(" + str(self.pointer) + ")" - + @xporegistry.register_tag("nu", XPOPredicate) class XPONull(XPOPredicate): @@ -675,7 +675,7 @@ def pointer(self) -> "XXpr": def __str__(self) -> str: return "null(" + str(self.pointer) + ")" - + @xporegistry.register_tag("nz", XPOPredicate) class XPONotZero(XPOPredicate): @@ -698,7 +698,7 @@ def expr(self) -> "XXpr": def __str__(self) -> str: return "not-zero(" + str(self.expr) + ")" - + @xporegistry.register_tag("nng", XPOPredicate) class XPONonNegative(XPOPredicate): @@ -721,8 +721,8 @@ def expr(self) -> "XXpr": def __str__(self) -> str: return "non-negative(" + str(self.expr) + ")" - - + + @xporegistry.register_tag("nt", XPOPredicate) class XPONullTerminated(XPOPredicate): """Pointer points to null-terminated string. @@ -767,7 +767,7 @@ def pointer(self) -> "XXpr": def __str__(self) -> str: return "output-format-string(" + str(self.pointer) + ")" - + @xporegistry.register_tag("pos", XPOPredicate) class XPOPositive(XPOPredicate): @@ -901,6 +901,101 @@ def __str__(self) -> str: return "tainted(" + str(self.expr) + ")" +@xporegistry.register_tag("ts", XPOPredicate) +class XPOTrustedString(XPOPredicate): + """Expression is trusted. + + args[0]: index of expression in xprdictionary + """ + + def __init__( + self, xpod: "FnXPODictionary", ixval: IndexedTableValue) -> None: + XPOPredicate.__init__(self, xpod, ixval) + + @property + def is_xpo_trusted_string(self) -> bool: + return True + + @property + def expr(self) -> "XXpr": + return self.xd.xpr(self.args[0]) + + def __str__(self) -> str: + return "trusted-string(" + str(self.expr) + ")" + + +@xporegistry.register_tag("tc", XPOPredicate) +class XPOTrustedOsCmdString(XPOPredicate): + """Expression is trusted os command string + + args[0]: index of expression in xprdictionary + """ + + def __init__( + self, xpod: "FnXPODictionary", ixval: IndexedTableValue) -> None: + XPOPredicate.__init__(self, xpod, ixval) + + @property + def is_xpo_trusted_os_cmd_string(self) -> bool: + return True + + @property + def expr(self) -> "XXpr": + return self.xd.xpr(self.args[0]) + + def __str__(self) -> str: + return "trusted-os-cmd-string(" + str(self.expr) + ")" + + +@xporegistry.register_tag("tfs", XPOPredicate) +class XPOTrustedOsCmdFmtString(XPOPredicate): + """Expression is trusted os command format string + + args[0]: index of expression in xprdictionary + """ + + def __init__( + self, xpod: "FnXPODictionary", ixval: IndexedTableValue) -> None: + XPOPredicate.__init__(self, xpod, ixval) + + @property + def is_xpo_trusted_os_cmd_fmt_string(self) -> bool: + return True + + @property + def expr(self) -> "XXpr": + return self.xd.xpr(self.args[0]) + + @property + def kind(self) -> str: + if self.tags[1] == "f": + return "FMT_ARGS" + else: + return "VA_LIST" + + @property + def optlen(self) -> Optional["XXpr"]: + if self.args[1] == -1: + return None + return self.xd.xpr(self.args[1]) + + @property + def format_arguments(self) -> List["XPOFormatArgument"]: + return [self.xpod.format_arg(i) for i in self.args[2:]] + + def __str__(self) -> str: + return ( + "trusted-os-cmd-fmt-string(" + + str(self.expr) + + ", " + + self.kind + + ", " + + (str(self.optlen) if self.optlen is not None else "_") + + ", " + + ", ".join(str(fmtarg) for fmtarg in self.format_arguments) + + ")") + + @xporegistry.register_tag("v", XPOPredicate) class XPOValidMem(XPOPredicate): """Expression points to valid memory. @@ -922,5 +1017,3 @@ def expr(self) -> "XXpr": def __str__(self) -> str: return "validmem(" + str(self.expr) + ")" - - From e3ca6683ca1defaf4dc014d29ca8b5d1abfb4498 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sat, 16 May 2026 11:36:06 -0700 Subject: [PATCH 2/5] SUMMARIES: update summaries --- chb/summaries/bchsummaries.jar | Bin 3330191 -> 3330443 bytes 1 file changed, 0 insertions(+), 0 deletions(-) diff --git a/chb/summaries/bchsummaries.jar b/chb/summaries/bchsummaries.jar index 887d1243f1fe4afc7a4a652a463e9837372dd9fd..26ca2467066dc85fe760f56329fd4d996a3eb939 100644 GIT binary patch delta 20198 zcmY*h2VBi<`>%7_JKB4n(L9GXl@N}mnIwBeRLUL|MHC5j87)c?NkmaeR(6@$dlivQ zr2qGKPS5i`|M&ChbKKW`?R8)Gea`b{?7A$SR(M%jHF!8%MoUUTK|yL~YI&xr2OA$r zq7;#IiinjWVyB2?Qbe*TBDoZie2PdRMWmP_Qc4jir-)QiM5-wwwG@$hibx|xq?sb> zl_Kh$BGO6`X{U&EQbf8bBE1xmeu~H-MP!&FGD;B{r-)2aM5ZYsv!f#O@m}mrspVCB zz0A8Fv*)CiQ|uHAlZ3dK`H}PDXE-dL8+CL{!^Q_L8vPg5PdPPm{DJJp3woWED>Dl% zpx4aiVH&(V$C*t(U}IHW_m(#;woCtA=6EZ&nqrvGgb}yI0Y; zR-4`TlFt26p5NcJJUN{4e&kB|RsM@Nl{?;xFl-In-uJLq*V>KWeT;&265bYUl3o<` zEwlXbmy+8r3{1v8_%@^F@2SP{aiO~l-zvz5eYk6$yzugp2kl*}=UyLmZDITB1=>}` zcjSJnp4?r3_4l_KXV!9$KBiphrSC&uWL%P!^K;pHuPSh7@Zra*gC>t|DNqz@RL-(6 zT$)wyVca}0a)RZ+Q@hK@`yMiDkY691plH%{L-XG3^;;u+Dkq1A7%vFCH)*Jnw{l>1 z?2!w%2YCEk@FYv7GtVXMVzINA&-`I2cHw_FA6zf>=gG}7kM37|dO9^=_nw$_>$hgV z@(ShHCf_f;Ffha8`JSma?3?z4h34hyXX)pZ4T(5-%}ph@&(zU@((byqk^^~P^IjFt z`JP~QOuw7emMdS-i5)DUsuE(e@Y#r63edVcdcEN5Hq>4a`Xc^!v{;1{NuuYZrYO< zRU-T_^JPh^`-7BY%4Zt(ydAl%@A!4?!!^gM)~|b1u`jA1iW^zv_Nn75dvSHrn;Nsd z@k4&SU3FR*7e8{kO-HzjQV^##_eVsZTOm=AuPQQaW;x5|f8l@k!tX7>dWZa^G$$1;M4(QmbeQj*B_M*#SgXgTMmOd3a_0aC?{ipaT&)Jj_ zGA~CXLN|3(iPBVEhhjn7g6Wo=!mZzno>6A@_1Z}@9&XQ!yZ$mgKjBDjkT5W{*B`&* z!*3d$QPsPiE#u5}v(23=+)@9`I3m7w#LkYOgeHNP=O4KPUm`}dE{~R*C-+h3WXZ_f%b2{DAyxU^SqL$4+;gNhLbpEM7zoMi%_b$Hl_Q~31KaCYRcRI9hH{88HhV%3D zt6wI6HyurBT5#w`#~*!{k9YPPE=rzave|3a&j%CxcC&+r%PZu3_>s7bEhVL`NCO^O z*;kD+x9~7$DwhV-TbfY0uZ3DdK->c}jsBeaDQibQ*vB8Ty*0ky(Bt29E8nR2T`11> zk$ri#>)QmM{OlL6ZyEIpz5A#t`bn?rB`w8kwm6NMowa4Hqan*Tc7o_=)5Rv!CtIRl z?yHtxZxcJov2hwlyU&|s-kAJuh1D~C)K_Jl_PLmIVc4;YE*H-XJp4;(+_4o`j*Uz3 zyAe~CT~j(TF=76VyS-gECQec9%!!&)G++DEkHqX9i#7yrbRVScKdX1PuA`rabe4;1 zT;SFM&z6O19%(U21NI9PSg{7KM=RChWv{#+=rsJMhUJ>6WoPYT*_8{rlm^_9l}maf zeM5f7?#O=j$}1o@f0gr@8p?TYoLf)x3{I+z7K~fux5;A3 zwh5dzEQF*s=s5I}u%{A?^w|1;u^Xu=|+y

O5YOXA0r9Y0Y9&~J| zV9uv3xr~DeeRG}l4C{Ms)s;H*d2C?tr<^y*w5p}$o7;_#*UCED^xPDG>yMfy<@sFC zyH`ipWyQY>n|sTSc=IyF?jC!3%zFjB>#tv$MU?p6&@kQ;x$0%Dp8tTG;{r2=x184b zu_#vd{HsB;PtF}wI6f^Tws`ovUhfX&bS*S6G8+B5;$S)Wq zQx`GhZ~4vZu3k=)FN{!4TK8V5_eZl;*Mif3j~`sdAE&jdLv_Yk*ML#$8XE0G9PDSs zw_iNFqAj}a$b7AR*2C@9?UK*BhlH&gdin*oCfBi7xZ|atF&Z%&pS>_T@G7_=*=(ry z!2`3l&EKrvmFdy&Lu$yR-3hY~OJ93(D?Qbtwo2!(waktPzwa`gV+T7NmJR#(kt^r9 zxcwI|>Rnvu8qVV{#`B9;+sC^f>+jNU$8o#oQrESp?s|M^l;!5$`)j;baV%#PL|*Zz zT=uxedCdLU?+$7wzMiAqT=#Rs`qUfW4aRtJxTXc zcY8HHD{?wd=JSO|qh3s_xxU|6^yg>&Qs*J@vM=4f#g$Kb%Rc>ntzW>8kvXIMT!-CO z8L2v?wOd=QFgxOB#Mb#sbl$xD9Ccuh@S#KWyoxS=M?d{~&C?}YyPbwV`78Xb%+%s? zxsKpTsKrN$Qd0jrx8G4-g}G%F$Irqdmz{#b6i8c{(wr9-DhXp7<~_s-`e35qsrk^f ztmEHp2EP|6vDkHe*P7fIsUZ_Sd(7n>7Ngf6uKU%wacJ3?u(ApAbC-9F7&!lR-Lor& zTTdn&==-p6&Q@prn%YpIkLBE5{@W|Oy}Pn&r+)krH}qoi_)jr(AWL%|DOi5}VCb=9 zb$r@xANiDyZ56LPPcBcmT%Jv~)!~m19E=`Q?_`qg{;!B-_Zdzz zhkLD#nf|op6txyzOE4HP>{p_D*~Q6MMh`mo`TTf}NM`Qz3nNLpW4z3R&J*7%$5sFO zkhtSj*5Xm4$0tSZch0SUBy+)cX=#Z=LVj-C^3#Kh&VBy5Q)BAK114&dDjRo2=jy)= zkyZ=e=P>%<^`e}W@(=Fo)LaYeoV#}4)VTON0;O7)JFA5wswUK}O)0+ZVg5%u%YE0{ zZ`XRSej2Nun4wt|ctd}O#Z)bgh{$f+uNU3D-`N!=E36e*o?FFlciXgE*4cT$0KF7m z!Gi?2F`R`H~W3Ju}(zR)bo=&Om~kAJ5=ORJH*YqM)$^$y68Wcd}iqr!KNp-?=I-_idpPsD%yD> z_0MASk9zUFHVZmG?uvE^cA2Ukbw6p6QLBUHW@ny7g4bd5rUqBVjmo|^j#gYAxiWR= zwgcy9?EU>y<=RaDaZ5%{p8jr)(Uya{8-k`>ed6zFKD%vSdqwx}uDE^akJq$s&0uGT z{P4=m3Ux9!-5AhUc2$15{v4;*uh$!Ucy7wL`HAH^SH{=7{- z=lr^Oubl%eo^wqSChV^sX7s3h-KTy*%Z{ddwr*dvf8%_O`(_&r4kUjPeNgwimu#@* z{XiMcr;n9s!Sy=7v2upI_i}=S_mUigxhxCtLn1 zZO)XLVEACqMM}P3tMyIVXZ^Ktv|Qe*Jwa;sR4vUHcKI9l8m(7~OgAras?+G+vGn&m z?#70Gwwdg#$X)5}PsTfNPF)LVR0-UqaO`KV`-|oujy)zCn$twsRb#bK+JCh@-x1Rm8Fj}fJ zuv&C5d+cS|KY?TS3{=ezp10xlv4;(f8CA+Z2hLJ9t*lb6?viSW9&_0>x%;m5io%W( z?-75cnLZS^$)v9~ymTn2` z^1M>oHPPIZyekBX)GxzQJz;a@xf7>iL$r*Y4!m7B)Y~VkHFUqd{^lFEe|Lr)%c_pJ zA8s-7RVHivQKM>!sdmxt~m0#cH!~77E#y>|7UM*+{*dnP%tR7FeN-;aZ%Cm zleI7RpZm=o#8QGt0KYM*_*_Y5GPh}(Ly*%mHo>F4r z(feNW#rNN3Up+2lOK+{!@d#Q{b^Uj$U&yR(>Btv-_VoXHp(Dhgz2Aiqp+Eb{B#7MI z2QRw+_P9!o-GgksFNv-lsfqoiMZ-S`ZY1n}@*s)Rby9b&*{i32pM6mCNYvE(uh=eX?fn{4Lml{P!$OX453^)4&dSH2Z`epPD@TOm_4d)~){$B(1m z^gbbN6`XhOMS@jSk9x znIw?4N*KQWQkK>LOU<+UBiR8;zzf5FM>s z#UJQ(P5IYZpY5tgqAd8&A2uhQ*1dlyeoW}7%xJ?aLn~dB4OA~xj=SVJXVhM6d5;;P zR@v9a@9xjZn6$ySul9-6YQLiotvs_e^Iei{=m{Oxo(0nq&K?;!bK@t=B=yb@+nW8S zu+^`eF!^q~Hu-HX@-Ih`Jo;}ZO)3(V^EMA_ouy4sc z_g6VC=YRE1X$~le9g?tg`T1lWzZbi-ODsl|%s;!^r!_-w$b)756{`l_c+~4pyG3#E z)HK6e9U>Xt$B%#J*$3PVJ8HYawVoT87-$D zJ-Vv0a^0m<3tnASnRoEnyI=R7=d5u`DJt1e-*v1@JWTW41|@W{q@<)xN%Ne!F%@jI z>P0at1Ts|tn=Rvxvk$M|FRq@1g>m!#cM+}|J3Q`%i;7ocJ?qTK2Nf0%hE3deAUF5Q z*Bkx69_l}H*80Quh8ATfZ(f|RV!#N;@z-A5GBQ%KN>VrVIyL`$>z;#8hlQ1-KR*2J z+xnzir?o^MtKR3AC)m_i1pQ(Og%{ZgEBzOW;+FYWzrOvcrm|B0-hj^uzF}OqOZMZ- zZr(0$opJQ9{++5tt~+b4uG#Z!Th^Y+mlIAWWshIz6ZPRn<-(Mc2eS^H-`=Y{W#7#Y zzIzr<-=Fk%?zr~6g{=*W_r#_x&2oTRSO1^mL(V&T%_cuic)Hx$AqGn$0;hUh@*4!|8CE z)M-BaqDz$Sakm&{@AmtfKTo_dL+~iRt!BB8M)7U82U>o;ix+#_2s}TZHD$&4J}T({ zsO+;TC-iWa_j!XGWuaVd-2Cp*aF zjqekcu}9)>xZVmn;`MEXZ0%2ylV_WA%Y4_jWqFwLxX_N)3pM0YDZpv(0uXahN!$fTeg{y`Gz-X z`>R=L z9i;p~EAxbs%A1LG*X55NKlMjGwaI3jdQ)_!+td%qZmXhs7AtmM6z*~lwlcWcFKuki z^XqYKK`Wf%+LRgtcb3eYeEw^@*_Yg)UWeYTa(k|CHor4W?auC|NrN<&+8@k0aNN&& zX@BmP=0OE{hWiZW`lx#ASngIEd8T36>B~3bn(}?o=}`_42lubl1Y> zeZHd7O{X&JuYX^owD49!zl`n-rQ*d7K1RhCzm9Q=SDXBq&PB8q4;&FTk~95Lkn-YD ze*=o5pM8D*VVuRAWfk2H9|Pv+MitFecyf99?AS+o?%Peivh*X)oC(|Zde-f~iHdax zdFEe!KbHD>zJA!-7i9fs@ROrs#&nEczuG11p6Rp8^xOK+Ra2Ug$CK$+4wj!@|!9aGSjRjTMSm@A>bOE2m<=#J z33RE-!9s)fED>l>@&h$8kiyAm@``b_vWN8_22(h`C8B}Ukd}eTv|_e}3EiuJkz2O_Vy!FJqX zK~MTyXp`GEfs^!girfY#Y@$Qkz%gt$eccAJUyAwiA~l?`ms~s zE4`CEa*%#jpK=rB=fYC8 zn--MTEYQ!+17GReWS0j+ELtcg5AHC0K*yL*l}Gf4`3!hUzWD+hbKJwj|2HN}N&Ww% zD|%r;;V+PM#+Uwy`jLEybbU)r`QWnn9cdRJDm&UO$fOq}vRz znDh(r@qi{2!a=^OR8$B%rB+gNp}>gcp+O%C1%52*MJ`1GANEx(OA67l)S-+b0iS(T z*OFpan)hVg%OaS-H^|-t@y2)h7@yKDlSHPggQ{{F+p$oU~j3wl$r)iI*6k8L63KSmK5!0sYh4$ z!ITrjEXivaR^q;6Q3|c3{K=~n2{1m$lAZ)YKz=D|<2zjfP`ZmW_6vrvOGjIh!)TCQ zJn>H?SM5iboI)*W@*8s%cR)twoM4dpNR1OGiSq>A({Qwj!p_K;^ zm~V9M0FqUI204`owCK=uOC>5zg7t1?u)dH+mLbn~%&{bsIhMK-zcgTnHF_RBDuYE) zv6j>k17$o9B7_U$Y34ydmoB!XT@Dt8bm5>t$YwA5uVVV;0wF7K1qGDD&P$1w6qpF| zvT~5etfqVAi1^ABMEo3r;dn?OK=Yk^2r4dGPsPlq?gn~yNML1(D_;0N!>y^jl$7p& zTdY(8IaEON=bIsV1vsTv2%K02*>s{pFpTZ8-I6wLvos`yGxjQEe^_9`zPr+}AhV+|x$YSGAB9!xk5lGRlwWpTkLMKY zELG_*P}slf!K)qw+{=QVem(jallG^Xj2+DKIY-sUkYr_z^!FHwteFN>L50m%EvZ=! zJ+b?Wr93SzL`;uVAx%WhJre4g5Nn%Uz-6n!uH*)pSA)*wHk@+{Mz5@fet|7i3Mi}g z9(}Bafl?2t&vBHC;bU5O9B`{=RKt80yv#lU;_5d&{vLM%cK>N(?AD{|4T4_T`|V}u z_z5Ub)ow}Z?GVs@0s>SzsG&rlLyk4@&Am^SB>03Vtf+y*n`mzhL=OK!?`sf^+rR#s zM!~hntZ9ENsrI*}F1;G z%Ue;boRuNf*TKhQ6|JaT!Ak!>N3!-wU}vk4;3RyzRGos)p+1n1a*}f0g>81DrWKiL zf{Y1`*upmqm5LUz>yc;kb*!jju$2})*0z$T+4T@KSl@~XW^X#AXQe>Jo1ymUdXN|! z(c^mb#4BWR3ffhfTamiCRZnZkJcU|(MF&nH+Wk0m=nDL$*dTCVE$5MY1Juj2rGy4# z&pHPydS(x!A2+~%4@vPfHdFdg&}sOQ??PKnBUI^bbeH+8^&sOjfXnx%$!FlP$v)6_ z3o=@Kp5HnHtriTVjx&M*>~Vf#L-ff1ENtKnvts5GWAW)_h6`l)|7JcZDTDu4hs*rw z^jWl7>kv{p2W9$!K!nuyf{GQC$?+J6-^x zV~iCAN5h-q3QD|ycHJ0D1sC9i(s+7x0Zu4fNW6<6lwHyzW7S20fHi74N#8`_Ubu*C zUY9_fKw(`@BJWEm0jm^RbqTS`TiZkO@Di}zt|zt2Fm!b~jbc7mWzY`h^IRr9#V0#( zs})6WLCW}Cf#F6(QCA@T_jV?#eyjmG^z#aM7v_`aRZvacO-WZFGqi}#dEyn)E*-W6jS z(Ct7}!mAr#*?yl( zFVH5VTkyWsYsq3NvygowS(Gx1S3QeQ%;L*i$&TA?EN-?+775Jaa2r+JhRs{vNr0+% z0E~YxS&U*9quV8moy@}X1GCVf7k4n+8PTp5{F~Q;8MI6C?-=}>^|V7mQN=7yePRUY zP||WYNGZMkz~JD?LS=oGIxk6bOC_5*<|uR`ye1eeYR3Vixz* zB%IaMtmVk|85F2hm*94&K_!{HNZ3`+kgz!#62v3Vz;BJF1n1W?u$b9PvhaD1#gN{T z#ad>;)sif(F$)E4M!CVPciIx5srEno<6eOOWgP~rovi~sN?!>0$_I3q@;(It(S=$%UX6!sGBJki9Ob{Sh6)2Wvzw8N(2l^)5y5;!Pavb2_35I223 zecIrtOCw(4DEne*O`0oh3~1de)Em#*noe!u8PnZYXtkqw)>N@Ts6~y1j#}jW8qx+j zP{?as?k+e{?rXttR#6{ndyR&b>_Sd&&=4-UTGKlhYeQPh5^B({Hy~NyL3MA?M%4OS zlVd+?Gdk{$t-f!uHQa~H-@}kZZ);_Wc?*4K478@`0HF@$`dTYeEd#nZ$eKd>2=&Q0 z1ghw?g6_;v61L);DD}6d%frF)R}fg1Fk8EW=}ar6T@A6ONf)>}WY#9=%QhWpO%1a^ zKBo=Ak{(C7ZBTwyIJLFGW#cAdS4L<-qu;>?$0u3S{fX8bO3($LA zmVQR`W#2I_EpVQl?5)--vMjWz|%wpO6^@1d|t4BS@1)21u$5#@_<)cqb~Ox+@D z63iBAQ+PXCW$H2*^^I#tdzsaPmDc2-534`6!|g6f)+F7Rqesz+@WHlM_8K($14PEI zrq~Y~$*)U`Jdte^zd^fxXROIYC^VrR-=M3+WO+cHSwFzo z;NJhzQoN_!A{H8aIxgNSt49P{JBKeL552s7)`|+K4{>LJRBsN`{@_75)<@79d*}cOo^N zf754$_h zQ?ikzU(*pf=|3PbP$A<#u%S_%X8nOnKWf;Jh6aLkm#Sp#W4a8=zZ*Z6tXc$`*RDHw^6|JjfQhv1SgZ3VCqpVhbJE zmVu0mkiDUX0ENqdc79L~ZMuw5$TAo~r(}d9*vm)u@Zie|`>?K!Vl*7ax)VyJvclo4 zvEkWDV4@)h?JFnH06C!_yF0>$%p&0LVPBAQRdQf0KLxC(3yo>94W!A*12l1}jU?aQ zJyax$&X;K1mxLXP0!;;8WSvZ*WY&Fft zC;Ql1*vzz$CS`cyMQXN+a5&p|z1Vg7G*bnPqta|>!+J2TRuS^q4I5D^gE)rSs<3|U zW^z&m!Gf%wY&fvhMj@*U@(-v&e%5vyI;6m{qz|r;Agu<~zwaPpHJClNz(#WLE>(kw z{9UlPz(!wk`rKv^4;IoVH6*7-u?-3K*x;2*9qKRNOX=#u0QSxOJ;Bv2!?`W10Rpdb zGS>j-8;4<0i;WH?YQQ4tN~+L+yIECCjI~Kw6Zu?y+=dD)`C8OoZKF&PnlNidt+)f| zQGSh$93Ak23CA_T^+E&P))e}(hn`0im_z5OKKvQn3)byx?5UA8y}Ivq{dV>SM2~J>+QJg!96s5w%je##|7Kgky zeeVq?&%8-CTEaoBEw?C2ODJM@w}=hIJj0wPFSMZLoQKq{h3xKr%J@K!hR%Yii?qRN z_;Ya&(W1m>HVSk|8$Mk8njUH+eSWsu;L^jfrblj0S~N)q*mFLLt<)u_1g<>o)PVy} zchD6bB+AE6|6?RWcDmT|{6Z6Sh5oF!-)X-tg3{jElWs@dF^AabL9vH_8Mo`wI6b(5 zE5)G?LvhsXV^)dMoUC0O8yap2D>U_i{6&T)+W=Xt{Wu2FUyg$Nps%Fq!^0Vhcpy;V zaLK0^D1I>epOvV$fp8$(T?MmDywHdi7=Uw(Du*&vIA*kcDiB)?fOtcLz8Jtk6EGYz z3`ZFX`>+q_a_FiK2WdVLUH^z7@Pdq}$xs-`?rX|nTCX0t86g6ymJ+I!MnZS?EGv#A zv{#ue4=!~X!I|oIfX2f0lZ*kK=0ux}0i`}1YF2=}DhnsH4->ffX^dhD6aLU1Ey#= zyL>s!;D%=tGnn2skRxeM!DcYfWH5)RRSb{J@pa4$Ovd^3AY=>%^L8_ES~G<7&4qp} zso^x)92Mv652dY9KxfR+jCuugBsr>RA#`QW8OfoLR?Huv7D53_ek>Uag{D+$fovEQ zN)Ig13$BdsiE@`7vS7R=gc?rd&?Xn56-|nOP$NfJQ~@|^+9bMa2^$Vf=KMSExwG@9 zbLiAGjv*ylp^}p+yNi#q8-bEaG)`cg5(}1!ymVxO~jsx7 zz^&GDnEugISsS>}V?`>R&?)0E9A5!%IN3w+wxbkok8ahknnM$+0KEbzJNGz;PF5qD z^bwq_93Vu$mV6x0V8)+B*thV^X`chaaj{;U1UlLE9C`Zb0Mb9FIR6g2GUVlmki?$j zNc#9{N1-zwaX3srv!x4jV8C}r@YcO1=_r9$!Nti5YRzhu|bAXif{mQJMFh zVA6vd9Qtz|4p=)332H3>edHY)Ab=4CEvTA1NRIsireGdWivSJT^)ZwFf$X>^9LX${ zEQIETPsIkCkbAYGrugNwRS53#&yfJkEvo-B4t}>~hY6!^ABgDxg6S>8SQ{}5n+px- zXdf8%{;jx4=n?J}?rf(vanTt|hVhww!EMP04(({?n9~PlG&~9r%j*+e?~6EkeHFJ! z^M9{Le0IN|;u_MSlmL`uwlf$s{TAnxK3#D}4ZZtIf1Kf!Drqh`V9uln7o?Run=)L4 zqu4<*T&6tDDBTfS>$rkENuDdY+y%M<@wNgbxFWe)l}LIJk}L6?jS_R_V=z=9Q#WBS z>xMeTx}mkr>&2Bstl14>O|-M!0eq{+WzyE1qTB(zZAdxpD2sX%EKH#x64Q+SC)1#AbXq+fi_${dcv&2_*}^?Q+zvf@Ps}&wlvWb zP3o`%_usp-EL~u>WS!`jC!!iCAn$(gML}N(>%%pmmJvwRihgkMWoNqD4;`}871qDS zd$M&KuJ%LvLp6JMNOt3z(j_MZWD7v7sUB3`9|5`2k4x>ITyxU*f>IZKxYXv2Yq2OA zh_POvjTr>{2XalAv4hVl8Af-#Frl6ECsS{sKl^qNmuXXmWSWZMVWT&AsE2ULDVVEI zu9u?Gg2Y~3_WU6DJ{ibu7g4HD>Urf;!vna$@7{D4gn+km4t3~tZ zwJ)Zl=J{Ou6blQ)7wvHaVN}>6E-hOK9Ww?(NZ3-U83=-(2~36ruso9~co2ddl>$#P z=Sle>oL9l?xXie0B(Y0#Fzm8SC;P$3k4dj7~P7LgRpY?4#mEKIA9jCeO3^3UiCwg zjyr;co~*1+Y6(J;r~c(KXTA>AcfnD!W+AOd1_Qaao1%l!fc02B$!$DHnkP#w!C>vj z=KVW7%TOWOPK)Q|)GHphk;6d z3{TPl`j6%*klA?X5H*e`zMj&o@o>c8Bk0zuvYW*sBR)87_a3q;}^c~o(QcMrjpYnVGzqPosuTOrh6GYs^`LW zk0-%(R+&7>JBsCGq|3xDNNuKe3pS%{R!#=9{H@{?u%>3LSTWm}EJJ^C7pjuU6tHjF zPC-+ILs`{%v>l)9WonuRhH6KV!v3s5)f6}#hu+j0%9@T=Wp@g7%M2oo ze^673GvJez4Lr%qisuZ7+I>!veUvyu=*-eed`88CCg1#u2*lf_JUCH*2# zGCM}jM4vlzmA22sVHA0jp3H>M`j-DV0mbCVHoC{7{&$hQekagTie|xvX^-gCEV#Ss z=|6&>;jOsi3H-_%gWlFB5=gA)6ch=k&3MI=+((Z^f?NJ;#6(G`mpvQ8f3`7MJdADk zzDFgz-QwAFHheL)ozBn3ThfRQQlEo-4E@s6IJ8_Hv}ny7IAQE}R0i`5@wbI5$MkSq zi5U2W&K`4>qTrm>Qhdq7@wh0kJuOY^qcHQN$@1xd3}2txz9CVi=R)6VIWnFLWwe#} z%tN^`t(gmb1C{xbd(WRPIR7mW*=tnzl1i&p<||0v$At61;FmfD&O-?`_M+T*$oOx) z`I2M0dmbeFX_Helpi+8#GS}rBO1{L{9Sw%#4f&GpeJdJQ`(>tlN%@<`z(oQ}3W|aK z308b&Sj59q3?e!lH(zn(bjN^oE+(K@c)E!PJ|aBOsq&y$K`e4Q-hr;fBHJpR_>!^w zog-h7Jm!Oko{%qTwJYXB&P-=2n-BFGT=@U=NjXxB19x{f@{SXZWFPF$X9g);jN(A8 z?9C@TFX*EXkJZV6|5C|NKs=~E4WgCtaP*R)e93k5Wjunx_2)AW#QNm00KQ!q(BnwF zY${O#K&+-fIxkn%=Q!$O?tv&Jx=R^+}2 zz|ygj#YSe)7RsQDSjJ%t(2Q&s12}fPgva=~cqU6*jEF6mB-w6cwhv8~EIKCfWyolW zkgv31248By{HVFn^CVxuO2je392+Dikg<7^|VJbYXeGLCR9X(`LcAs5Van< z6u1*&|Fc&RgT0)k2+HO84A_KTFNIjSc*(+f85X_^{v~i_pBA?MZx6OTuJ-nSrXLNbt;7fK%!k3R!_8b7C5w1i5^3x|E3?`)~!) zZFhPPX#4_z99IJLVgsKvxA2X~Yy*^>yAs@nW-v0W|COpiHyF&0En-Y_(ntW(=q&1& z07cGc_t2LoAj%qfVgdM)D;%ECPJ}0R?%K zU5aAY3w5$9Y!ztbTGXvbmJY6EE)fb8l#T+?OGWTw6(x%q{gLU5Q^D+$I%%dsgR)fk zaAt2>vRi0L+cv`UhU>6>M~f=*&^YcSVTzx{KspR01i`tsa^z@Wi?kj9_f#``4n|@n zsNkus41HJ!fh&zA*fEEpm(O}YPMI(`!R&5RTQW1XH7DL?^yhEuLGEGBAdg|+wX&ta zBwGtgPXmFW4b`O~K6r@2ryiBtKxStsWcEo1(M>L6l8CL$x1~dlwt95C5XpOy*_vf5 z5&kzF?*kc5;(cQY>C6q-e<%3IXG+AGis#)b2Fi9}OxB~h`9cNyvH=2PjHH`F5wJCI4Kn}zzU z3F9Pch=W)M9Q-8OdkZdi>RW){HlAS@%;HXvq{>kSxGmy;B-vZxg`?9Xiaq|zSEJDk zq#;rwXJ(7N79HCPQ?jFNscN3BDb*GsmaHsj);mrTF#q|s%H+Bi6*__e2gFN~Ff9wR zk{3vD>f(X(Gz%8iFZ_?NbNNVJzid#+E|w@YX*-h9dy%asJzfL9=Q4Z#m_65{DAq0p zSX{^781TpyjFSGWjVqaGjbPia5_{W*HYS0xjiB}SH9cu&x(!xcNc;aXROrNZ$X~w= z%+xph>lAs~nu`dwFyIfFjQ$)l*be$-S(2R2`ipv8xEWUA9`J)DHuU_D=A8R?L7$v(}bMlJLMz zQ2*R7p%z!>-< zldL0Itw;Y&N@d!X3$-pE{}&=p&vU_8rbd#2J|_?xad#h>2NqQ)8F_e=%VQL*XQ=#H zf`)%RB95a9)p(*--Sa`v>l}k4u2mP-*^81zT|O@4(wD{U#fW~T!1J5}gs%Vf9?+x$ zuwQtCG7B&(bl#FACTkb&m0I`ymDP*FcQFxqB!QqBIh-Ycq3unx*J~v?0HK@g?P@m`qq{{ys^c*bs;9C&Q@EBV%h0a zWg(c4dq=MdG3E^ZK(qOLwqs-%Q*beqdmu;4i*e0NP_&~01v~s&lz}EG zQ(g(8|2-JabuEFQPwHYSeVSVW%|>W4`$O4>dfCx+P3W8IjQZ@g7veqj$YC$U>l@O7 zy*Ts+8PcJ>h@7k`#z@ez0B-rqN$x3&DjUJy(}rQ9AgsiCG#%8 z?2D}IXpW_w3A2wcy-Fbg^?~;b0eJnnw;d%7fDYw{QLkkOfNVK{(b|OG z902wtU-3SE@K^>Ne+;3>GE9w!MG{?`%HWWFlL#P{~>H1iI6N3m)RlTE5YFK zAtvn8dNlsXAnlz_W)+au7%66(9SLFUDujHMKeO$akwN_XFv-kts{-OVb4YLmp-?^y z<0eGek@-@__)-`@|FF;i|GCSP!)WpFh9m3YJbHQ<18h`0Lor)a#ZB9^Ak?yrS;;W$FPHHT{YO1Rgy0OQvwxi{%>Hq(<3oQmyqDU|td4aDj?p8(zPy%cgn=&P8z5AlkN zo;rtA8xeq$%-;D@x_<%>q;6$oT!YWJgEXlI*`O=O=v^gB6Tf-qvyWHX(fum;4*!uDM%_C2sEdN@(DKgJQc)eQj$ZXB#FKXX z?92a{#62lAP;_bdN2O2KgoffTXJ!M=jyWy%iz#CYz9)+6fpfhK;)!|wQq4)D;W$*=YAFyOYYcC>4TeQ%OGgXDMlNv>zm z94G#&5kj!r%Zi&Q;I0SVR`o)gl;mjrwT)RJyJanYww%d({B@dLsGKCm16pN zxJL=Uu|JQPKH}KZUmJTJdcYulw6!MB=N~E|QAR?wBeTXG|hyl{nL$@w6UgV8yyPn`$oO1>*Nydor49kNRYO4d!}9XrNFP zW8afOm3F=H3whAqi?gTB`Tt;@2NrwvLVGG&V2__=ZHHU+uL7j7+@5&L?5!y5Drl}I z*wcrVP=81U5GsIx3b=BWsib7mz6Q5=uB8dr;1=!%dm5IG0MuWDW~~|Y?i%iwGq#Xj s6DFExL`hBPBx*bCnRGLzwkBZ3=aEh`s!y?q!kUGSa<_`@@t;2YA76zB{r~^~ delta 19365 zcmZ9z30%zI_di}U?TOO9uQOBAw9F79m7-GGtXZ=ZMJZ$}R47|Tlw&EaB72sK&|(iQ zvJ>JRSrW<;%K!PA@p*sWzyJI3nD@&)_uR9ebI-l6S6d2hN^i}(DXkLV!L3N1}IE6JOkqbDuelec4n$@sf0Q)R7yH zn%g%^>xJIDde`w+Z+rcR^ws=lYfaQYw%%M)x*#Ry+8Dj!t$*?hhO5S9aE4ljR%IPE z>V9Wl864kyv}NI$=~1Qc<*yd(y`*HAXZ|64_o>wi%{x1fJ@20SB(FHTy<+P7`3qAQ z_UWs?YE*hju&`RY-=&l~2ReR%q+yq9h9HfyTfe|QeNH>Y){ZSStu{;Lj+j*+2*Ug48l z)-65h(J*n8QSz}ll^WdUrPB^2X};YZxVw7t@Xw+xi*#b=6&=cAEw&9;xG=VDxb>Ll zAH6h6H%EGFdWG0W8#gG#f4sXijHBN?EM(NO!Ao*m1(`2SB{t+9OLpqhC!~Ab`s=R6 zS;hS`FJ>qh9JHA9E6cF)l-kf%#cO>x+}QW!>i05r|H~HDGR6CJ2M(HN7ctsV$Mem` z#7k)!X)cfM&XX~dJ!_ddYvD1~-+laLgHn6{ak;oo*>S;<$E6P+*QwiQH{FTfAh;b; zk?}d&E_nmd}hgn-<+<7s%W=8qs~3lQrX)O|E(*fwxdgE`)b1AF8v)}cGxV=^74=2otnSd zVn%hiquzA?_R?L3g&#fFC#GeL_>`gPH>n||;{B9S^H#6eFFhxb!M)~#|| z$#MHpG_r8$gk43^gM1Hm)^h#0R_$Jw>eX#_bZ_1r{$_2~DX!fQ$4A{}uhv>t+uh8b z`g^M7*`zyd`CD@;$|sf%J6H5ypjRWIL$Nd0{JY+l#*Xm-4*qLRZZ_cMbhKKZE- ze9@`7YErSys{7T?s+#6KTorWOIlzaubrrv<{B!>gE5Juyp{+GNNRNOv3^VO}G zp+<#If6BHyu4}96qZ zLk}N6F(c~ZgS}t(v@V)jP`dPZ;u@v<=hmIxm#Afv?O0yNZ(pGGP5OAshpBgGtZ>tG z*Kp_EoOjsCEi%IT{57R99Tm^qI}~gc+WK%zO`bIr2G*@B9`SJcnAauWyXDBOk8}0IhS=R6Hs5B`PRp75JFjjwbej{RA!r+5>29bHw?-tqRNJL| z%)NMiX1rhJB8!qMwYx8C%Qzdhc8{6azxP%^wUo)BU|I8PK9lVy=SA55`aH7IWtq-X z;o|;p1{}OBW%V*?)oj)C6YYP#pJk$yVfApp)RXd$@0^)4v&8zLQ83qZ&j1_MJXKZDH&Cb)!pL z{#hKC>(n~>!O9p5rZK zJA0Ft&V9S+=IMH$eQA9|?l|?Uc=pI~_uZ2HwYFg-f{Wb>ebifimcV~6Oh zuxneC);RyeOgGh|IUarEr{-PQUf^6C(q+`3x$EGb*{2V0JkP#)oIR&Cdr|LLw#LP~($8C>7LSb83Nu-H)-3GYd6ut9k>1>} zqa}~_KC0iof%kL%x0N-;&nEBno3Qb6LD#sg<34PjIQ8U@rayP)r?oA;tWp%bBD;6f z)u_}@t=lVm-hR<$@@&-`lLTAjSuc}kw)AwHP^oN(hnaph)iw7M=UIPhcxBcnp2@F4 zs>7cIm#lN=w(m+7aI(EPyKk&0qSp=XvF}1es^$3s>!g&|p3FR6-#^!K?8)i#9{-q` zs66v~`=yJrcfR+_Og22{F?mPH-uJrffp@fOGjxA-HbvbS_RYC+ea4t_&F{-^Own!m zw#nYDqcXq1(W}f-DJDQ+tM1+luTGW4uX3)KTy;C*Owci{N_(T7j!$#VI~1ns&5d}! z`ohce3m@D*bF?v|uJr4frJOPk>vhdCIgQW1w9h{K&jszH_xIkH>IpeAf7zXtavtL~ z&I-?ryBZZ#*7r_LZK>O)AZGPb;D!z6+5HC$W)iT z8TSVc)c)qVYo1RptEF~ZFgxeKj-h|TWjL+u*QdD~(hqOk+?rbEm!a^uwrbopr5`qH zBUd-aJ{COf{+O_*HFHJ4gsF+)haIvjn`N%M#U474Rv%yI=-gsfbmhyBy#ZIBO&)Gg z6}Hv=`OpD{p0Y#!@m^ZIIF;MlHSFR2(ud3M--#MFX8IuBJi~&j1#^a5nlF8FFD@u- z%2D;2;K1GLu|XZfLsgxOq&^AP-W@&EeOyQitH!!LK51Xp%`J5zvynqmQZy!w4?mEo zVRLY_jO;9pqJ)J5;vdca64a+Ud)2_0Z`%)E?R`G0WrAbfkUqWcG5NAShb|e`v|jOR z)5?)|zZAHra8==iJD+y<4zpQj*;~ZD;_7|q6>Goq0^<|rzmG+TO0OkE&GB6YQI*8uxC_lY-t~J#UVR zV)aYajXeeCU!AMH1-q&?%-OMzRqcN@#X;xn?o$OP-M^G9N!$J7d&256$B|FRXM_%k z92Dtk`tqfG)>ZQu=bNUSmzGA;;}4gQHfTP+>9dpnuZ6nH?+oskm>sPeqUxzKv1SFQ zpL{`tTaAUI!6Ktb*TJq=<#N-@UGL0U-m0;x)_?l)9~Fc0uD0BfwoSd!@=amg&x9hQ zIO)}OE!$sLt9qp!@w{l~_IxXA^HG;6Zi>DgtY^Q5uS#3%cVn36-utDWw-&nIf3qZB zho5^np8HeD#$0iAWCU?@)aG}Nz3VAuHFVzeFNWJr|B>G47dSFy-l{=|Tnh*6SYy%| z7Hit;5dLeSWm@&BiDuWv7bS^GswXGX00l}2lU)5J?bk7GN=pZ%(MVQ9wX z-`{3R#R}?obVoQ>tbP9WV)Vfl_1dE)k9WrXu=(-%n^Ldp;~M$)cFm`25?c3O`JiIz zvUGI6rM+D~J^D;7DH#1KLPthQs$H2r2btQ?<6NO~S!A2p10K^fQ@oai5p@>|Rmv8t znh%Mm>=IKmy0z6@Cq66Y%DJjVff|PPg0^K|F0ScsgAUusZr^_I*U!Mx%oXA1rkRb~ zy4C+~L3Z=Sfer=@Lqof^-!8Jkey!mhMIXX@9L~-v>mGL9a((8Ho~(!rty16hT1$V) z+q93ETQbroTtU-@j(k~D_Tv1aqXtR(1rJ0Y zPOh3h>j?WLAlr_-UAcJ}*c#x$>ew^g&-*096vqsGVNPpU$W#en!) zeuhT1dAfgF^oltfp1geZzV^rU0sriubX9pDEAaOek)DOs4FlQQpW7G2$=^%1uT$>6 z<+_`5>cg$^g)2STNp`1ag-;BMNsn5-Ye#sbk&|9lcxTG;#zh>U$=0gq2&Rb0>8;?LN>M!+PGha*M-}z=@CV&V5odf2m7i zPX3_iNpS-be+~QbfzST3P-lmZyB^5y}h31BIqK}0d#h*kT z=o%~LKSKmsBa@JpneYesr`2}9i5=(^SYngM4d*5vF4t&=5*Xa zUrXL3I!wjUw2f{#=SOjX^xmO@P#SM8~6qtd$x5M2k5+Y z)tA{ns##O?!@^i4TxE4$%%lee?>R}+r+rmT(=D8M>y*{mL&L0jk1XD|?#)$v|IFKH zU`ylGld31&Hf>D0)z)EmEY@bi(`vu|x?#h7H-reUjl5~qGTBEq)jRFb%(L!ux@WjW zj#Mpq5OI9sA^oz>z0!I&^?UR89E)FBA$PodbUapLUs(<#%OM4yJA z5AE90utTLb;?aO%N2S7i*xM2_ZBn`2qRm|8XT`0NZ6VJ+2G!pgJ!b38ZC5+5OqiBv zcg1F$$5V%s!lUNL2ToVsu*uzfUi{#`7J7T0ZmsCtQqt9PyXn=w&Ng1%je;7pwHGPW z-@-Kh`01tu&w_r7mn3%gQ_b-`X|(UT*`ljY6&J}oA3HL3?+sC&V}ONTlhc+-zg{*j zdFQ{{e#twfYkqs*T(3!a`((uHVL28vpUW<~Jizszt|@)*zuZ;5(WGn2G{;BLson-( zbH});C&n%;oPS!{;dfBV#-U?W&9$=eoTJ(?vvd5&Ka=(57;PDT^r=DkeZ39zVn=uX z-Uz$ObfcH5`AH4kn_b&}t4LMfi(B)4KxLDROWV{b3nISEU$6Tqq^Iwf;!DD3DQ*Xp ztcu-Op1mGV^!X11!#kaNUHH3RI+m4R-0c^;(Yc`JT3C>BlhKjKlXf+DZs{+obkR$= z7&ln4=l99=m2IhWLREtIA3R-ryH_gs;#0eps2Tb{rWH)C>6!PV=iA(+J{#+&-x<98 z=TFb?@yxb!uB7#rHMX5{$+oj0AkYFo4t`wxc=%c3XN4ahKWqF1WdVUU+a@r#M)a!4 zW(f0-4MqoS@Uz9wuFU9w{oFbkY+BQ3bE=(QS^iStN3Fj1*Q!kZ_gtz#`%;7xrLE{| ziqM_)(42;*3f-kMXicinjrG-%YA|H03e0Gxz)X`2(}aBXdRsG^^~O}2?0d{)sKeGw znW7o^U3)Wfy)M+I(`iC`>BH2T21-O$TZNwNr$fw0`n0(^C2tklN}r@NTfwbnI2r90 zYLV(Tz=FtSn~-N5P#hEZZ!@nTC8aC%-~ZNA(l((7t9umP-Uhjfz0AmZw3z|fr3?Ae zBWX&y&`o+hWitmOaH<(qIhbow)HE}B(poE2rB~a9 zdeTPJyInX^I+@&eKMy%{a%GoI#!9KRmjO^E&Y12;zF*w~IlJz~Ee0K>)No&v!45c~r zkb&0jW*p(cj>s~jk6B>7@V6|u;#i9Y-NORc9E>j9 zH={)-h3b@$BeZ9gKBkj75b(fLGm5XW(4o*Op&FUxf@s@wa?TZUO|y_p|JN}7|Kru= zl^IpPf<1C_g?!e&H*_->=6?Q;)bbFb(lkB~l8>i77_oz^FlV<@!okM8_pgxou8K4Sj7UJPXlM98T zSjBxPw-BNPgwU-*p#dweAH6F?M)j)E)&iuW*M5*2NK5uZAOmf4TC@gvUcX;x%}R&8 z_CxqAeR3-TrG7@tSWjY-(?#MOsxJa3cTzuq`Dh+ZIe?hj$TufvYXs2Q1K?X}L#>#V z9!u5-g`?R|MCOz}z+8`Zez8%b{DVSWwvvN6lc5Im_#i}aA=zROD|DpBQlSBb6$?eu z4z#xz!Q)IXBoEFZh?VS43l4$%SUQfOv?+Dr!Jg-1PKIMZAMvP4p@-qP8b3-r423bMo6I)FuC;Vi(08 zg}J9u^-;uOLMX`{6M9K2k^eD}m!^zkfS!+}N6fP+nv9O)*}R12Fwd6d5```w7m8T( zWB=tkgned}IW1TXk;~7aNJO7N3JGcJ2?+OKE!{gIbY-`$H>bTxz?fTwm~bnB>4h}C z1XQ1GqI~ALCWYRV2rVdJl~Bg;-&RgeN=o~`#Z*dut2tf3!G(r=0jq$Ms5FM#X+(uk zgVvuE+OwZznp0hp(1;Q;z^L^kthZg06_T5>4$6pW}wO{Y+f9r6$`*N{Ad z(^zd>Xin1mL0w!6)}2PRn^uHaH~`5no`zM!4$`~R*kwi^CfhS`U4L492E;6>{0ux| zyt5Q>`Qr?El|rK{<&;_q+{W{asm38hIc1m*t)|E_I4170Ig|D36n({9j_S%lz3nRf zEJGS7)9`Z0cKen&HOOHL+f^=B_$f-fFUACdh8hBirWG{hCm56*ULHSSz+Ik5Vy*8NcGSBahq#L-s^!}gtFZH2|S3uAz zz=8=&T{5|fEnx6iB+fVsZ3@ANl`x*RU4>G&CenkeLSJ^$WDD9i#lle1JB+^uM<`FD z=xdPg%M3bw4g2D!)Ab=X>(ZeEA5xe=s# z13^3>%7Vs3V>0>%7~hPhtQ(j;wuD-4AZ89MwVi*fqxLJ#8ZX?-8?X{p8Sr%HP zTn8ox_CeMhEcnSZ4YTU7Yt75EpoDygKlB|c@s_XleN_M7Vl=IQYU+?(cZw|N{Q;~M zHypxxto>1pfIe(tM$z@)-+6?x>Y?QR6V!qy`|c?VYCnwyt_@%yi7chFg4FYl+;i9>fjLqEHS8FVo?m&-{YB5#9Ole%9 z+l{b;$u$dRx6&ZXJ7^B3+@L9Uu%PLt1qHU4s?(`Euy$zOU&r*^VGPj-L)-x|u`=VE zK#YBt@uxc3-m{RW%}r29{{fSj`qVld3|knS&yN^?s*~zn@NsV@x4W>n+Dl5l3tyT3 zL$~e<9avufQ2ISIojUh`WZ5bi1TzE0*UVrP>#g{yN$mhif2VEtkbMsKg?6k5Z4&Ib z`@k-JOVW=)r-m8OJIRdV0}NKYX9ijn_yB7re~`=&X0Rf08i#$qWvDmJCKb!eHYU$zUTh2=9~(>Y2glE@m)_ zW&Kq`fBItp`+k#P6f%Qv-y}2dnZbkal7Z+62IW5_gO$u+PdBqhi>jYMr1ovzB3CTBP|L()E*Nu(fC! zGx#Dap<^u1k)wmp!RDTvgxK5XSXd@6nYMp{0VzmkmSZ5jf@Zw{k&DbkkdlPFTni{V zDoe1&v|vWBkAznSGxJkC(4@!AOtXrFvgu0NUEKK+AKeyqizdSi|b9X%w{q@k^duf94ou@xKBdPCaRiaoK^NQ`1YSCn9>Ix`Z! z77k{AH{+111;>~+zeaA_Sa9giM3EugeJvERgDg3;$O=UJG@(8T-++&&4Tomh0zL8# zh}^QH-EV|G?1Lf>RS)3k?rZ~%jSd{j8-!J7zarEpv_X`*LA0n1qO5eJvu#M%{!a9# z4eR_}IHb0Xr%z#TQ6}cQaj4OruScie3hmgp-8m%OW~oU(-$ImYo*a7N#nC2@cVKbM zheOxKa7-xqosB9LyaS6Of2w>3(v1O>@B>}(;?s7TH0V70X$OMgd=42*73q?ehph(fWI(D>5W${@-X@wOPxb9E z-R;Hns~sC$^)e29=D=q`9~pA79I_iC(x<98jtoT%1=I46An<%Oyd=xhqQ3DQ1=^$y zcd$F4_0R;0{(|0nK_W+yC=f^9KnA>YEk$;qQ@N9bWgL+SJ?el()i!Ww#0DNN0fvYa zi2n)v9&QHrEgS=yYzbByK4Go>R_f?Re_Oi7PJ`|-keVIz`4haSl1YxAg?{W#`m0UO zXW;<$$ld>?s!8@*qy&-JxqCQtb}z?>rZmAv+fA$5D?o>ei zI)z@W?joApiNmVS5%~QmJbkVcX7V{suRF1^{VE~rF1T0o3@z#s`mx5AQgs*1x2B9k zruH!QiE@-0p9Roj@K+e@R5_$dhtpr2g=IWF;O0aIKD&aGnG5Hg{tDI?&Qt4G>{eqd z#Zj+KOPoMy>NnuI)*y)Ut+Xln5=WW#e1j+pu1Ta$dW~xJjX}!0j%09#-)+9bmNRZ4 ze5Z4@D25r`YY?Y|CY}3^czV}F?cdSswB6^B^g|d$&JPlW{D4u69x?&z&2D)jPDDN0 z*nztGi8(#^gU(gQCn?ZATZICOHpQAqfCK_&&o2-3=)lE zo#JHXh!C{A%r~NOtTh61k`@K9AKG&1vmInQCJj_0Aw8BBjb=Lx7Jx2hwwNiBO1tF;0=lSA`R-65!teNzFejv=#n^^f@DQ{>}7rsZ4_6XHp+@bY@x=MzijWqp8gE@gype6Zx>FPNm;Uuy-GM2vg7eg>^ZZ!OcZL;Km~|mITvcqgMU3f0WnTEu)Y@$}-?PUlG_k3%MkW;_6V2B5b-Unr40{OT>6tPtKO=#7ecj%?1c|l!Km8 zMKqXgx(Op@LkU(94PZxa=F+Au2n5X%l&8xoQ1MDCy-*Q(vlgY3pfCKtGDGZaJ^CsQ zw;k*YDR%GTQiCrpXxiELRX^QpZb zB1~gHmu!l-=G0+;c#crT!h{2~Q5D{JaOkgG?W$Pdc8mM`+xtqQ?FrH};q-{};VVRIkXBB`0+l z`sh_Ax(z6F4P3ih9ZIpTb4mXO*OZEf!`g2cP{~a$vxlpbwg&9jeM{_0UApW9t(R*6 z!M08uznV0yo~uaSi=k8v;H=g4^h^WX7u?}e)jJfj!I~gIOo)6<0l8P_9 zyF~}WfA~rVbdblNyP4?Hp}x8Z+7~@yYim)zKM2Svx>zds0|iPgjcC6vXs?&zQMNRX zOFhiocQ%jNsr6}eIBYUO4`fH6P1O^5vUe!(B*F7PXQ)yqGyhGI`su^3!JHT;l%4m!UO=A_sPaIZxu`8;02QO9t`iMHCvB4aP9ZwZRw-!Kw%~ zY#FbOp~=;uJjUE+6x)U><6t6UZmZD5nrpR=& zk(6kPWSl-q4ArE680cmX(lmn%GTt=Z48h~*!xL}om1dAx%U>+BCY7?$$(or%=BTmc zYz`MFPlU>Uw{>|cGKZ{QlXx^M2qykv4)--o;YnQEt&6CbWC6*IXYeRxu*iaTSpYpO z7{q6yaC%>gz$3fXI2%(uAD9{wjBjf3CO(jQUC(Wh~4pX`3(@-uXc3enn z@nr8<#G@mN;UV#^`kf0#f*2mTrdaBbfCol1mx=>Pi?%L9>ZTaO{F`{-c4Qez4}@%= zdWEud5tuBESnA-xbL&>|{w;S3G{F+4Sd#!z*eK1%6L|{c!VoF71gq?IJo+uHoI=)UmIuNwUj3lJ_6`? zDh2RS0Dq+Mn7th_%g5TNZ9JOMjnmIhK14m6PS)1YJ|#npqd{jgdHp0NIA9I3KS^v| z4SHw|>67>JC?^Y)tgx@M@9h&yp)YBR69qtjl+PpkP;_Z;exlUeU_d$hLE#>VX=%t@%;m#NfF zwpg2Wnu2UmVqMFqWPr$+F4@9FdF2R5cNnaX9h5h$ASXL)K*1Ma*oh)j+HVJSZ(n30 zLYvy{L_%pPGPXykF1^g7v@1MgT5t@Bu*V)Un_S~D#mt&?!U6iifb?(w^*%=^60#%e zkxxu9TPOt8y$zHj6a})MH}dGm9i9=*i^DQg5tc>X<1t->COy}+lBL}HP;t5lDi+@7 z(S-*{NO3bz22|GO$J8W(yM{IYHzkG)fNIO1@g!YN0!FL@&l#=#SjsI-;EiUDcqu6) zQLlK4v|u2L^7dCu7V44PIe6j9KoI}*hN%r>Sp(lPd8b7_4k8h2bvwm7h{mwpKEXvn zFpJo0-42l3trMZ|XJyKqN;Jr45J0Zq|7OveK?sGWpW=YgrK}%7cnSnoM-TlN1d~@t zSu(An9!(hxX_Z;DWw2;GYaE+e2BSktk|Wz8cs`P+I6T?yikAO2b&f0_Wzu&eDdbv8cEJb3pu-F+OIq{=Egjzpg68sRsuKh%wXvkcA2*ktdxcWXRJL98x9o<2UtoPwp|Rgejwc#j!5bqBo<4T?1xy&((=;?0(YE7 zSi&I`>@4zT&vUe-grR7waaLEQ2bf|v46~%SPL`(BEsfyjxB&aM3yp9=VTy5Qp6Zk{ z(y|X7bb(tBd(mANG*>r#NZ%EHd*o*+Y14I7P&D?qf}VPSB?$s8b*aG>QN|wk*NUnm z;O^rSBm|p>^Hpiy2q@Qg5|m?_Ue_Q9Y$pd1u8n{QGlS^W2-rJy8dhREFFwLf z7zqwDmeHb-K%23W%J5|WUL%eIBQh8T$GEJsr02>A$f)&@D|{4GiCzyb=1_BAlBFWW zGNN7{1w!LD(u+~>GjEF}Q>zUrd>W=EdB7HvQ!FK0;8qXN)Y)pubesD0!~C>zKQI|REPhAv77Gf=^p&(S^~_>i!u^W_L3u z6>re8DI-U3#PHd365%qvMMGKX7pT!2F&|fLDe0umV$dgg_&}248pN9%VtbVj6zsif zNx4E)x;h^S?tWby#ahfg$Uydin~3{cP(Ex7xK`DP<5YYS=ua0IkZgk`88uq|y;m{y z1@)*Vad2o7c9cF8>c_eC0h9J&Ch;xIcvJ{9s9aK0+MvJ-}6e;A?yWo+-0QYLIpS00X}=b;5xB z0}yg})szq*3S{l>rltVV7*l zD@k~DjfWxB^~E&tQNaX}J?pFyEt&u=HBCruGNS(p18lZnco>slBJlONR+7T!$+J?Y z4U5t7WKM)2C00~25mhf&K)n+|p|33kPJ;F4*ir5z)RMUaNP0dL>6wJybk9Hr$%q1i z5cYEhQ$i3dxnwAPia;E{2!gruhA{$ouRVpV#tm7W^c`}N? z#nCim3Z6V)Ms_p8eG~dTe8$L5_Op_-cJHQuWTQVLp$6GaMWZVl2w!yK0%grqoc!*M z6PrYrZcl}Z$`h<4r$UWsXk(*;tf)l=ZEVOi5GkHanbQz|e$(mEG}NcJv&m>WJgyyL z#k3t}l3T&u)4^SCo)sB~SsBpVp)k@*2J|N!TrD`bxSoM@QH``BtA$o3wDKF=xoifk zXb?@?XTbTdmRLznjO{ZJKpo4-G#J&JyTXcGR^p0h=yW)lfCN$DqV?EzXAg3dzz zFeBqgw)8QOlY_AK$F2Iq(pZpzkP|1FxZhkE3h5e8!oJMq=1q)P{ZBI?XheE*A&*y? z70oKQ(vu|o(z!79ymOR37Y9@OO3-Gyg->&_YHbyn&cnV?bot-NlcTlsK;7V~Sf#($ z7Y_hp&AKLu*{#>nTYd0CsT~jo>ug>C*8qXcl>go`j)dUAq5& z2I|io4e`qGAuSEZRM=B!){JD<838}HhC|kh=ZrL7Y`GS!Vy@Fd=Y#V6f2<_O!<<&| z-*p<;*XDzNL8}$@DB-~No5A}1_HT51EPxjF@5QpA9brcEK3GvgJN)^40Zclv!-}Fl zVI)3*42b}#Xr+}Z=mhKWC6Un(jZQhd2^PclO_qEn ziwr4aG3vq!8$R=Pz?9xC2Fr3gKC}NAGm5B^#}ZI95b|jj2O+z13Cy%$AQdlxq*omH z%q@lvDa7EWX82$l7K6LUlTNfPMl_b)&zVn_E+C`x5>jX^g%mYzWWN;Lzq<1oUz^b0 zrQo;PlP@_KzE}$40v}Rc2Ajr?;Y+q-TrbK|+%h=0$(PT(u+iA*4=eMS*Dv>%fvT=Q zeOV@QR~{L_ms%FOcu9EFLdmP63Cl6NFn|^98z5?aMB2hLipqsHcUVmQ5%$So)9GK0D zW(H%W>nSP@(mad9Mx(Suveaf31|BgI?4(s9Tjji1a9R?&ICSAMiQ-MG!0IN>&8tL{ zSn=`XwHil;&k3||HTtO=bKSLB52ALNd%joAX21bi6X9Y!U4Y2^6-UWF)`5+ z#kvwf;?MzVNrLPT4)XiaqbdZ~$h82UI3@u%ALnb*=CvT`c#4F{2-;g~aq3YhmrQG~ zLvwTgJS8ThCz!VmGf_1XwCqcKWxBWy3twH8;HqASY~uG$!u8+~St|k0UXP88-5?p* zH}cW-t;edLyy=h;R{1!Bvwh^0Q(2`px`{h?N&}N z-1ZoV?8Ci$e0X53MaCrROV%5aLZAPjfGoAvq;1(E1&ZB>g!7Z3LmSa{xyW17CrfKR zW&_kDt4*M}RN*gZ<|ZJ1#hc(%lofv9J_z*#r=A^+T9rhCTu!s`nq(M=62Sz7+1DuAHqXtn+9y&&str)BuOwn7B zLtR7u71@zB&RH^u+RpSF+klqqLeblRrZz${7bVozzC#G#{)sfW;^Iq1pdp@jioe>oHEevi&wX8 zhvPm@u%`6A*7{_!1IsNZQQ!{r`Llu~i{K0yI?K!)n=DzWoPoi|Da;^%C78yz)|>#; z#HY;=CTseC7XHqFiO$ZENFD~qivYQ}CzzPX?%}PYI zIIBK0;7O|(1r3S63u4J$-6;D zJw*Z*+voglgyxrR3`Ca@fqhA950=JfkjEZ0^R~MsxT(EJ|I$53trdI3Ha8)Kz0l^w zUdg;Ts>bhyT=>IOF)bv=K-Sbe$+S3TdiH{F>wXEuJxk=m+EOghK`{;e|Aj2b_WRJk ztL5lN7S0UYkN*cUIvX77PDn_Arz30F$^T5h%Z4&>rzAlp_UpubAlia9Y1S@Ey@WE_n#i*hb0PgLka^Q%Ws7b0rUJdz+Xf z^kwNhluV1Q4$|<)Qwc=uv;2G%=CjQb725MfLs$!6{AW71#ae+z7eK_K7Dg#Jig2Ry?Ph3bQe+VmDnAh_zpRbuLJ@?q>y=FP z7C{()7Wp5S*>vRWa0%1kAgK>sZY` zttOz`{RO(zdk_pe+u&P4`I2R zv4EzU2u!Hw5InFPAeNRHl^lay_yEU_5U+1H~gi_+cjonUU8KAUF>a(4@hF0TK%348p0QVgw`VJOWd7 z4HL_%PA0<`|5+36n#JF78&X$1QUWGU)6L=5v4+sBB;FlUn5;~;x|tbkg^ z35+Gj6s;3@+ruW|37qj9CrHdB*7p!5SPLf8)f1v%_R?u$!1ARIEh;<>-l7J8e1zoX2+hjKtP6ZaMt0& z@ZZ8ykS{+%Kz-K&Wb6tpU?D#HMdV))EMd!vUcwL<&APopOlW5;&~W79vt?q%#5m+z z0%d=m1~K=zzx4knsw(-M0sL!%m?DQhm55}hc$l3IJ?^pZtLU&+Ahmo+)SLzQq{>d6 zn$C!fSix(l^9-&Q4y+SU)p~(8ZK?+OIi;}AKkF&JR5XHZvOz$O8wEJMl|qh?jRIP| zNuWpl!#X+r>i2Cf0e=d6AxC z#j*bxbjA&ICE|$&Ot5;7(}(kj5swl91)qeR{ujW0-ARhO0J3$b>EZ>{rwe6_kebw7 zhc-=k5wR*wV=kg~yHP>87tuGlT|~B53UJDG249m(C^oc;Tq~hMOf_Q;E!tIyJyVPZ)0C(D@aF%%u^vY}|ml~|U@tl%tu-AsaqPiNKoLyg&&Lxot zvLN^pPLW+71*Gx`#ie~MD(Ud7n*fI=@Uo7 zI*~uSag7bVi?`9E>^c$inf&!S1Wv^|Qmco$F3B{x9_k8GD2Exhr_q~wv`O=~lVt Date: Fri, 22 May 2026 21:53:14 -0700 Subject: [PATCH 3/5] ASTI: separate register rdefs from other variables' rdefs --- chb/app/Function.py | 2 +- chb/app/Instruction.py | 11 +++++++++-- chb/arm/ARMInstruction.py | 4 ++-- chb/cmdline/astcmds.py | 2 +- 4 files changed, 13 insertions(+), 6 deletions(-) diff --git a/chb/app/Function.py b/chb/app/Function.py index d64991bc..6d7c8899 100644 --- a/chb/app/Function.py +++ b/chb/app/Function.py @@ -531,7 +531,7 @@ def rdef_location_partition(self) -> Dict[str, List[List[str]]]: result: Dict[str, List[List[str]]] = {} for (iaddr, instr) in self.instructions.items(): - irdefs = instr.rdef_locations() + irdefs = instr.rdef_register_locations() for (reg, rdeflist) in irdefs.items(): result.setdefault(reg, []) for rrlist in result[reg]: diff --git a/chb/app/Instruction.py b/chb/app/Instruction.py index 03f96660..14642dd6 100644 --- a/chb/app/Instruction.py +++ b/chb/app/Instruction.py @@ -341,8 +341,15 @@ def ast_switch_condition_prov( Optional[AST.ASTExpr], Optional[AST.ASTExpr]]: raise UF.CHBError("ast-switch-condition-prov not defined") - def rdef_locations(self) -> Dict[str, List[str]]: - """Returns for each register, which locations must be combined.""" + def rdef_register_locations(self) -> Dict[str, List[str]]: + """Returns for each register, which locations must be combined. + + Note that there may be rdefs (reaching definitions) for other + variables. In particular, stack variables that get initialized + as part of a function side effect create a definition for that + variable, which may be retrieved via a reaching definition later. + Those variables are not returned by this method. + """ return {} diff --git a/chb/arm/ARMInstruction.py b/chb/arm/ARMInstruction.py index ec27b6bc..d135d690 100644 --- a/chb/arm/ARMInstruction.py +++ b/chb/arm/ARMInstruction.py @@ -412,11 +412,11 @@ def lhs_variables( def rhs_expressions(self, filter: Callable[[XXpr], bool]) -> List[XXpr]: return [x for x in self.opcode.rhs(self.xdata) if filter(x)] - def rdef_locations(self) -> Dict[str, List[str]]: + def rdef_register_locations(self) -> Dict[str, List[str]]: result: Dict[str, List[str]] = {} for rdef in self.xdata.reachingdefs: - if rdef is not None: + if rdef is not None and rdef.variable.is_register_variable: rdefvar = str(rdef.variable) rdeflocs = sorted([str(s) for s in rdef.valid_deflocations]) result[rdefvar] = rdeflocs diff --git a/chb/cmdline/astcmds.py b/chb/cmdline/astcmds.py index d61e8337..df4a1292 100644 --- a/chb/cmdline/astcmds.py +++ b/chb/cmdline/astcmds.py @@ -468,7 +468,7 @@ def print_reachingdefs( dotpaths: List[Tuple[DotRdefPath, str, str]] = [] regspill = register + "_spill" for (iaddr, instr) in f.instructions.items(): - if register in instr.rdef_locations(): + if register in instr.rdef_register_locations(): register_o = app.bdictionary.register_by_name(register) cblock = f.containing_block(iaddr) rdefs = instr.reaching_definitions(register) From 016b9666ff6094a6c385397bf668f3f09c1c481e Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Fri, 22 May 2026 22:44:31 -0700 Subject: [PATCH 4/5] AST: silence warning about side effect reaching defs --- chb/astinterface/ASTIProvenance.py | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/chb/astinterface/ASTIProvenance.py b/chb/astinterface/ASTIProvenance.py index a092cd5c..29a20a56 100644 --- a/chb/astinterface/ASTIProvenance.py +++ b/chb/astinterface/ASTIProvenance.py @@ -453,7 +453,15 @@ def resolve_reaching_defs(self) -> None: v, str(instr.tgt), addr) self.add_reaching_definition(xid, instrid) else: - chklogger.logger.warning( + # Calls may have side effects, which will + # also produce reaching definitions. These + # are currently not included in the + # ASTCall data type, but probably should + # be added at some point. For now this + # warning is changed into an INFO msg until + # side effects are properly incorporated + # in the AST representation. + chklogger.logger.info( "Lhs variable names don't match: %s vs %s" + " to %s for reaching def address %s", str(instr.lhs), v, str(instr.tgt), addr) From da6f3b764a11e872069dd4064e290b0352192104 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sat, 23 May 2026 22:19:03 -0700 Subject: [PATCH 5/5] CMD: always reset when analyzing --- chb/cmdline/commandutil.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/chb/cmdline/commandutil.py b/chb/cmdline/commandutil.py index 7b509351..4cdf7761 100644 --- a/chb/cmdline/commandutil.py +++ b/chb/cmdline/commandutil.py @@ -475,6 +475,8 @@ def analyzecmd(args: argparse.Namespace) -> NoReturn: + ". Version found: " + chbversion) + doreset = True + try: userhints = prepare_executable( path,