From 7c36befd9298363e517c5c945c9bbc693715dff8 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 13 Oct 2023 10:14:41 -0400 Subject: [PATCH 1/3] Add declare_ghost_state, mark llvm_declare_ghost_state as legacy command We want to be able to declare ghost state in all SAW language backends, so we now use a more general `declare_ghost_state` name for the command to reflect this. The old `llvm_declare_ghost_state` command is now a legacy command whose use is discouraged in favor of `declare_ghost_state`. This is one part of an eventual fix for #1929. --- doc/manual/manual.md | 2 +- doc/manual/manual.pdf | Bin 587289 -> 587278 bytes examples/ghost/ghost.saw | 2 +- intTests/test_ghost/test.saw | 2 +- intTests/test_ghost_branch_00/test.saw | 2 +- intTests/test_ghost_branch_01/test.saw | 2 +- intTests/test_ghost_branch_02/test.saw | 2 +- intTests/test_ghost_branch_03/test.saw | 2 +- intTests/test_ghost_types_00/test.saw | 2 +- src/SAWScript/Builtins.hs | 12 ++++++++++++ src/SAWScript/Crucible/LLVM/Builtins.hs | 9 --------- src/SAWScript/Interpreter.hs | 13 +++++++++---- 12 files changed, 29 insertions(+), 21 deletions(-) diff --git a/doc/manual/manual.md b/doc/manual/manual.md index 9fb91a2d73..b993b6b719 100644 --- a/doc/manual/manual.md +++ b/doc/manual/manual.md @@ -3541,7 +3541,7 @@ thought of as additional global state that is visible only to the verifier. Ghost state with a given name can be declared at the top level with the following function: -* `llvm_declare_ghost_state : String -> TopLevel Ghost` +* `declare_ghost_state : String -> TopLevel Ghost` Ghost state variables do not initially have any particluar type, and can store data of any type. Given an existing ghost variable the following diff --git a/doc/manual/manual.pdf b/doc/manual/manual.pdf index 80e0c8ad8c4b32a041ff75e6ade359f83307846c..67280f5b035144c8784710dcab0b6b0b7b589899 100644 GIT binary patch delta 8548 zcmbt(2Q*w=_jj~lh)xL6MQ@{b(R&{zqK+U%Hw+HHl6{ zbR%lCPoDNZ&-;J>>s{aXt#!{{zq{|=zkTjHd-mPuO!hig(mL1U2)tVSl4*Qtxh&i@ zd_G{w`d0GfTk4Pk`=Y~G0;uFMd+zQHyr)iAh{^6CltS6uoYd0Nqfi?60|%gDJG186 zGGkxg?pM^jjm3MI^Io~EZ0)e@)m^l$X8H0}{4aNTEVW)IfE^iPA*i;)6;3)Z{mJm! zuwXrwLNO3^wOpn4s!Dr75ISmOd?us~(-Z*gxZkk6h2#O>vURuA>lZVsSs5z#*^@ui zx0jjhN1F*SdI+q4pL51E(sg+88+sx5N7#E`ln0F0+?c(7+_YR;wGGkVnr*|_be)&+ zdjx#TwLje@l?*=I8urO?P8>;Ihocu_m z$;ynt4|iW!H3|h=Rc?>K61H9LgjYuqLka0zOWi$7r_F;5H=@2IeTn;$|ApC;qN;Ct zAlAZ<6QaWutbRw+H;zI-ZVnF-7YjU#_=1c`CnVadDz!In!~G0kPz)G;0x$AvkoISD zllsU^o0a4L96eO^YSt7;?iA+}YuJ079{Mmd)`UsQl`u=QR#RhAvqMKX`MF}ko898( zDvJ&$M$2N3Wh1;RWRTj1&NfM;tas({7^%QrDhkOGq%g%C3}cG$}L)bB6H$&D6xAxMIWro zxQ4APnALqUndE0-=^_+W_G(r`&zKWY|7GD3JK}W2m$0gYrs!i7H@zTEw;u9vGuC#j z!`E2R?%`nh!8eORyFAfLJm(276mEHtyyEcsL-sM!d z0h4@UsO32~&*i@Nv5z>o0a3*G0K6#jwQBhe@>0w2`|5Qi=h?j+mh5MiX2%T4>38b0 z-75phD%H_*lMjVbR2oRAuIfOr{Bm&`Dd&S;I5J zv(BX}G#+b|ihEj@QEQ|3GeB#&7sxG6J|{?}aOPC@{NO;%rW02``fYR*+I)Ail=}^M za>fkvazDqK&IDT|&1EM6YG5jg7)Y}J!EKipbc`E~qr}gZVka*IcugBT)t+cET1G(w z^NG(|l!)edkaAsLaViP#7C*T9T#q!pze(^erk&aAYqt7os0{JE_3G78*9OS1Y#s0Z zus7xI)%n0zX*Te?=*y4~lZ8C@-h3xb@MGl`oN5>nAi=Teit>~jmt0bE!Sv6M5c9c2tM#5&>CtS>AsuO2A4CK^J9?N1jqXo@ z(m=IjSKU8zJ`Q<6J%Z-w*N;#6{3wog3q(%+^poIsMX02S!o$V)C(3Oiw?m1EAH4m+ zE}d3vln!68MTI@1$jSB#rxY71$+AP19-Y3nQWBx3tbR z(IpuQ`m}mWqQg5z(@^DW!tvS^#~lZ!#UVLYDWA|J4oChS+Cu*{X?IuCAB~zsls=m# znC#853&_LLePU!$A?L5jB`c)7VpBFWhm&Dm6d%BEodN3S%>shY<0 z{-*ofKgB3SP=Jr(-uUjDU5lxYdeN8e9X2ovJZr~)!_7m3h>9_#V<+~yY~7n;y5j|l zR^er3dM5^X7&07=T{IQosG^t8_e@Pz$3&Nlu(K(FGx$i^Tkjqq8}<#H2DfC#6bu40 zRLhA*K49d5`tks?Y1y6)Rh8DY@&YXrLS4Jd_GhgMtU#21FKrnmv5rU3AhT(^-HL%e zlim}k&$RHD3Pzvi=63F5rRvAEEz2LrQ$H=Gu{NDNTDRSlseM}G4{4EWa`z2d(l>I< z@2B?-@_95&vG}05MkJ_e)Cvq&_Ufz85EO=53Osm~r&J}{bPeq_*Zbq%#*6ED2CLu5 z^Q!(D3+yev_q;Uc)d6qcm4edX zdZ(38KcP+oWFW_)cKY%sNxP+yF^OaRcrZFm`0i|jZwa-1QvAZDb$Fd3`!g}Am1f!P zysP3qS7iz-`O73nXJH{J4o@S$+hG_B%#dmg@$3Ls(p`=*8!$fE5Nk6&S8|r!J=B5A z&eJDfIuqleRD7nLHy+5L5sJHaK@-*=7Do>vtmHdIg!gW*auI}em>9U;yX`O3T-Z+^ z=`+*Ya4OhC*Cv^@Uiw@z&$U{GCc?o4#lvo@U?byPJVq!%L#cDEN%RS|aG#}-z$(HV zjpYFzmjuO=&P5ff>Z@%IjvFs<8^CapKVt_M-uW=dYCe?JeCh?NofzGpG3Wtvp^4tJ z4Sr0|G09!8;jS#vQ|Dk9L*6!C#^^2wV(*=Orj>$AoZ9meHa7>{iVM=U_Ig_O;A?%6 zd&>ge1HBHtv7qdp5PXct`**w>@D+o#`$wffLIoOaC%iQ`c32kV*Fv+GN*>~)NPvby z94B+^(g(Tb<6t4uyZwQ2eg(>P!Uhd57#X`iw+)~)>~t+hBaPMupyp_En*0afAcKXIVaBI!{UtZeQYbKJ#~pEWML-nO_Q(Bncb7(nWjKg#(fDfGCu51O8S*-*jjC84YtdBl}@ zsm|KI*{ZsipP{6K_3m-6uL(sep>#zV=?x{ktNbUIj(KL%`XV@uvR%piUR>Htv(1Po z-rIHW3D=Q13T^Ay)+XO55eX-74Ftk~hc5e&=i!J;ngt>%cR(9KZcL!G0lZ#j{%76K zjHf*^BLw;{rK>M+2{QtI=AQ|#+)=-$VQa?uM(KbwyvjX4NB8lt`k2(wAjJpe-tQx| z7-nq$tvO{rG}l5=Cw_jIieU!5vHwv41hi6)H-q<>lnmDLBC*oWZGo5trY=P+VXiPX8uGhv5Vbw5V zn~oIpaz7QFe{A!kCGQ?V;x^#x9UI3J2FpTJC=Fj`PR_?8qm>OqF?Ee3u}!}l=Gh9- zpc4S0<6~-U;Aim>_S|;DJJ$Qw6dqRCDXG$NG`)?`ilE3@kQ`itZhxX}>D+2#9<$1D zgnhYe#Ls3jp2kahM^(!uyqLhWFmH3UkW5G0mp-ndZ29AxrE?aNTHxy&*1OO5+_ph$ zem$990o=UyFnhKgk5}>2NW_VvAep1dn26RrM|2p;0|gAToc!t&TcHEqb?;gz(H`Sds{t*&8HniID z47IY%=i7aquz6!(ZY z&;OA;%idvp(|ZVT_fl7#ox?nh`my!#QrU4$yS8O#ykcU!{2)<7&pR59aA$Tt4SBE_SVCMJ3>N>*q&{GR zWQNp4Q%VjjEd~}76PMH!laf)B5SNnx%g9QoONdEJ-;|b9W>@^LCbl3^17{Cc_+54> z@ia$y0f6U=>nov+o5b6X{Fl=w`x{#hW`ef%re@X}H+UGu7s#II8mQqv!!mLah{LFe zH6$HI6Scx(m^9z78sJl_VEOLv%-=}*htIHgLdWfC1DDPNbPIrc5UyOBlVS)0J`9^>HTx zX&9}v6ImUMxz35$A9j@@V(_ii;`}CA-r&;)G;>f>9;&oAAV%9`^1+(O<{XjTk-7}L z=OGTI#Ld{j*CUp651GV-WRj1!Cnt7WnmPP*3#n8LcF4dhPcT_R3ijGuNoJqA9aF+c z0hse$M2XV=lE>IZK7h5U=yh@HFq-Niz(y-|N+|YjyZeoNh7ud6c&M^0gv&;B$%Z|b zjarlqO_PlrkqxhrjsBEH))1rLkRaF)r)$&YH`Q)9)#*OfVLR3JNU>cVJH@(4n!mu5 z?*tOvrV;O-2na_cG^mzCmrjdnjvj;oW%6MFOw!*`X5T?nWKJN8__KRLKn=Z>7XiXy zo%zG?MeTa^FuGUlDOpSK<;^)f)&>44Q6Om^$Mby63nU{R{Epi;(pNTlUW{kynp=k@ z`7szAc*zQPDH(@fCC(E5#Eo2{nhzebAMI)1BDnW@6l1of_b0f214wU*E0I1ZpEr<` zW-4$_x)~hxGCxE-(}DkDEuz#Fhx2;^Z4fWA+bO<7mV`_UBL+(fVn3{pn#q-03<_k_ z=q*+JZ&1QwO?`PY|1j7{IAg}@LYV6>UHG9bjD*Mhx72e5rYrrUfx&X)?%tk}7S z^+B zZ(@WuSQ~PJuD<m7B?h5*j~LH(H^qVQIY;vW zEl#9HOc)-reb%6Goq?0KMjg3#jH{DFMjrvlc6=c$r%(@#P&Zhp7gT{2sOY&?5sCf~ zaXwAUtPb7pKD?hxcx|@RABtz-M&`H}v|x{DZ##&c=3qH7YkoiM&^hb?W7}W6M6p0c zu}G4%z?ig1XtY3Qv`9XD$?6HU9 zw_{{y8kL7)Z2hel#oo?GoDr@q0h9X8J8kE&NTM&wvZ8SPYjIo9n(zHR8#mNMj9RE--#u znqtoJGPfEWksK^}2KiRHXD#ppfHOxt)svz(Zjy^IKJjS&Vblvlnw7pVGc3u`lT!Lx zb@?K!z>q~@>80W494CGD-L6kO1!gT;FG3!@*g;3FS$FxF|2e~q`vPNaMsrl?gK49`-Xj4H+i;}86oAg6Y`N-B{8XdGUVQJD z3r5}30UBJJT2qM)%-%8!9@yy^3^jslvxnP*t`tXILhZ9yqs6tNHJrFIMbb#^!}V3` zZDI;Dhm4v>#DzjUk9qH&!Lkd4(;s{WXi9_omNeH@zJ{Tz^$hh%7)&htjd2j|Nv($3 zZuPLPcmJvuELaYf9%`0uah6`vr&#`{Jxou#<(~Eu*;YGA;x?@-nDHP1r)MyGcW z_GIEx{6^4MffP!?6y;b%_T}f9$=Qt^ z%^&E$0HQ&}&0kcB_gY2al#lpYnSS&CFJ8afoY0Jlx8biW4}T~r&{xR{5jnN_*|_U_ z^sS2$uyWn(4o?pe89VX*K7*w7qzxANa-#WN`Dpp#7g)L07(ykg&`dGScI0u=#a!=4 zHKf^WA4Z)3BVR;DtrQ(A5HEDOIEuPNZE7nsdglIB=-btVI$=T`WCbHb^EvN0(ii%}$=2 zkMTvv*~#5koBrw;yi9p12J?na6X|i(2VQKH+f>QhjKBy7<^(QZD9X`!0&hkKG1HUGYi3DuZf_d^eg6R`s=Yf!l+>V;mD$6#8z^ZOUy`j z(J?V_4MF7jr#lZU6*QwJf=bb^n4+-~p#AF-Z04qK_OpfAW1IKP|A3Cj1`Xt2ce+^( zZpd^TPgUgRM2KW-%D@P+Q84&kb0>m0$LViDe}fEBx&i_EP1sZsRI$F$3e7(tP`ukz zGN<2>)iRWOR1}cwEuyV{p>8T zsPo^9{!kb-7BUmBJAaR~Pb3!kZFc>Lsggg6jcEg?qTEH7O95Ps;dO;ExHwUKgRy>d z!Y8Yyil6J;Dkf`76FD&w`7L`Zz|`7mTVFA_!$FwgcSFTE%-`FT+tgJ-o)=jhAvlnR zK@kU`D386VqP-Zkz36(qSa`i?Ue3YxzA`nylmhXLy+n2`Pai3Mi*JbNZwR~ScY%L4 zyjU*9F5ig(r#r^#p1lW)<=wmX3-sK1N9s3L42C~@#hrhp^rUr?W?3iWU3@(t;qAIG zh|PP)mrMWfK;`-t=cd6_cEcaqSOr?djUj`=Y{$OL=$TyO9$qMsxC?9mi;NYgb-K}G zkdVzNArAaY(_s*nO(;R?LNgHj{>k5Mely7%mGW##^xT7gKRsMtxCxRpZ&_#2$c>dw zbH34UkeMwcVPAF!|2<(2sU+>)-{PuDgu48$_+e{sW6Yo|+tV4m_io{UTWt{b*6e+- zZCb1}KVfEDpM`T zuLS)Q2&VgMe}8l$3M@WZy~*4rW)@}1WbJ%6qX_b!fo~IJ+|qjE^U(1?=%JdxkX~Cx zh~TN^&&u7~EA_*kC9|Mb`rx2`D@*V7t%w;~cH0ts=l8gXJ@ampX4OJu*gP(pnac|QtY5Ctkn^#sR@hTyNM zZ3)iC5ZAIYS5xO!Gu^JHpRB&FfFk=d6)zEclSF$HYI~FSdSB*M-}1ET?UIdj9Cq?! zX^Y?H09ulq9x_?2_jtF)>0)rG39o79gushU7{=4B8$4Ba{AK+5p?AlmRo&)%>vUEf zYr81*Ol$QXNl4zdf8RK*BKml0T;dS6={^;Qz&Swp?;14IP}AR$A7((+;t=UCJgc9bima-L7YK z=j(*ada^P7ae{S{-c-4KL!qVOP}hT0VM7+TYQfV`d5U1N?fo#}JQg=p&`c(bqV6-W zmx~Pbr||!@r;r_*PvQR=QWN@yB3Scezg9T$I@b8QwT#JR2OfskePy%VZ>ip;Pc@WS zd%bK!HJ-S4y=;el#=q0!L_Ijn+#eD`WiM=pNcccQx$)H2+=*&7y00x!lxY^;EaD8h zvOrRLG8qu;EekoTER~LNViRPWH6RBBEN9YLuog~Biweo~F&Q#`#3)hJjyDq42wQqI zq7q}6kdf?Eh6#rTx`u{6ql7IvT@p}<$w1UGzB*yIRDMyi^XpN@%@eyfv^^@vdC;Ro ze*)MNk;<5Q#mU3lTrn9FsiorBzACiT71WM^loSDKr`-L$T1E4jVRykz;NnRwecOCY zhShi}DYoyJ!s$K-Y)LBUzBp_t>q{KA592PN%xS4SBdYwUqL~*N*GnVFRv^h5P|<9a z8@C0vRA#-&k_rusmPRw7c5q(xoR%}k$hfx1n2h8t;SggQ!7W4M?k)9;7gWU-SakO> z7nPni5VaJ@#~ec9h5>`?QGLeOBkPQ>M?W*Z)o8eKIC}5Z!RRgWtm$(w*O|+5uuguk zl7}tHyMz7i%6P}GyS)qJC1N{~h{f?Gv7LfjQ%y8l^=CFyP1m$$&#Sy2fD=LvF76n5 zk{*FQY$=`E4wf4HxDwb7OB?(o655uJs;#z8&r%K^xxB>$MFGv{ zqG99mx7O}#45Ae#a-hu1Up`IjymGeaugr87p0)mlW*u!ZUDLn#E6{H2zGeBXN=J0m zSRX{ts?zF00|-FMEh-Js(qnNJf@T*+6l1IA<;InA=x?KX=7NTmqUhGqGP82MN*;9B zD9B7ur;-`%@rzOG-+{u~*fRBbuf4{}K?oC0n60H&{Yj{pDw delta 8553 zcmbVw1yr2Lwr+yEI{`w_;0_6%(70>x-~@tOqkn+l1a}QV5+FziYdkn1NFa>_YoL*I z(8is|%$Yee=iGDOz3;76wbxf)?Y(RNtLm@XRS8=x*;_2HUf-=pD_uYn7tKV`p>YCh zCdP^L{iGpqOFuG0Y@Sv~jN5m{h>g`?)Q>B^jGw2m>*gWLU2#7`7;xHhot93Q8o9N`VSMt7WIy$~s7?}hdEbXmRBa9!Uj*Pe#*ApN_a*5j?it~qe68N-s zE^?KIp{lzRh%CHYok`=TCoqVog$O-gp2s>!J0Glzz|gg>7%hDcucO4LO;0Tw`WVK7 zDEr3a9HyT{F9rUL+ng2$T4Fzv$Xw_uK$PYU`;D`lmgI8;G(_~K&D=Do^kG24^qfd+ zIO0f5`1Fp8)^?Tngg=XM}ABgxy*+paVf)zX9G5}%nS78 zp)KG#%KJUf1by7Bo>+%jqFX(l=|<;4i>-q-p1>GCw3qrSxoEk7w&k|-#iNYYT-Vhr z9;b4Z5Om!C^o|WQAPU-hCD{ik=sa;zf1(-|cHRW5DTfCHOW`w0A(dOSCCunsi5qi% zzKK!OXdO5CX$0FX2jrG%C}`#bc^bbD1qjrKbL~XGN)5kY(HY3H zx165s)2*DArR9rFiBJvp*0+sH4E}VwsaVCu4fqTBy`L+Ud-UyxHxJIQa|nXipVvwz zNL+ueezmA!vj7tb_@rP0APEW!%A;(iEaX@{vXB(LS{xY*;H}nuUz&?@nnF(%c3hi$ z=+Rfnhn{nggrTAMK5fdQN@b++>W-mg8}X{^=_Og0X}N-9J+n%mYTI|0^nyTZBcH>0 z^2E%71G=_H>2*dM_;O$1i1HO}g)h1zMi{iI6Ee1@qr0>=ggI}3i$&UMAF`amgcuqP z+thJ-@M%or`IjN=AgEsvjk6GfZ?z`VHtSCN#7ON{@My;-+an=RRmrg^f?7{T>!md<_!9aqk`B!54%XkQ@P)ur4nld`NDoa5fV%rP){2eo2S zv4&`RXT)#RSCy=pOuWZWk-3^<4L)Z|^5!H*g#=>7fz@=|-iy6&v_ided7m;k^fFLu zJ9O66Nk@(}YBnA`!ntJsnoLMCmrk6Q-k<B;%MSJThe(Nf>v2(W9(7JhM|P%QT+U}Zsb`<(1RRF1uP@Ac*fOYOpCLyfDcO;hSl zm{(I5Z4K{H8|s^-=2d8uyxN5AxG>G8w6Y=8qsV|{MK;Ak)iAs4RE8}#LS{6U@Q2l^ z)E$999Y1DoGhiz2`%QDbCR36jXWhU~w>Un`4bI2q1P{0hGwZ|8M$oCv7=fF4;mz5*gGaZwZUH4_ZSWybe zTjJWuI^ReHN!+Z}Fzv~7^V7l4{i8)*qfV=M3{SgtR~_WG*|%F3->s{~;W4hx7tt)t zW9{RRZZYRKr(r)+l)Il)$EKz^TgXi`$agn4ca5)5$k<tUwP zr1GH$ojG8=2B!Onv_m#Si_?kjPV9O3=_`a{+N!9s?hud`bIK7d5!5Fz7q2e&5_M`x z38h$79PXEJ#0(VcKe6EUZkuN;0iUw zFDpFpxh^XQ>n=R*-~KGnPFummp^c$pfn|B!Aqy}JR4?OB&atpIp>Mq5d|u;SR!UH+ z%+tI>8E+JS+K+J~Y}%Y%uT-)GImA7#U~u{~X( zek=gr#{3-GEM2w0z5OVT9}KoukOIG_*x&RmXl*`xjnnTn<{XhEyQu{aeJRIF_13(q zdgjB^t)6AajF3#*fHhjIeV-JLLW>h>Nab~e!=Mw<`~wCacYIr(F_P$H<#-$4JDrWA zX^x}+Hbr4z@@rR6R#{;5iFb{8yw*c?=6Mj1M5CQDesV>CfBbMuZCWL z?Nw=D9PU!WTREjCJN#2xE3E3)sL=D6(Ul*bh7zCv2~eH~UVRgcXi>dih`a%Fgo%GV zEk`?dtDV)QRP`yd;bc~z*2abLhJWvi>ppT(Z{aIT4ve-ouz75tyoq~GrSoc2(RSO) zU1!xURZ(zuzZF(1-^dq-ZEvLdhSM2P9{;hy$AWkF=j3UHl21F?Q3^qbuM|teGXtx+ z9Luy(mgQJ$f3d@_cCklUGL5|I&~+M`z8{^#5CsbjF@If+&u=CU#pIDTMpzUu&f-^<^cB$#me?+&xZyPNIm@FJr0mEUZ!X=zw4;-2p@By{6n6E2H( z*AKyK8sGnThCABi9M?g|8-Wf{;isV-5%#EYg>OWOE~XB>exRA{fbX+@XD8J>{dLLF zrAvRfvfo*9XV;z*!FDNMF}lN02>DAeutc@H(=vp8gJM>IaGul3&3zHx?CZk zyywa95`oXjyY9PmTvVeZ=>zw6%aZpo6xg=%!#?6||4F2!_OJbt-o;v^=C5FTS(8v!dB6~CxQ-_}U=?InCNagdreShopL0lgmo{J|b;S#eIu z$kUgfrcl9MLTs{Vg}=(3J>Gk2ee<}md8}@Iufl2RX9QE!(GT+&346;#jGN}Zs;-Zb z)!FxMNF~kHgBLPkI1yJ^jaU=djQ8``9!Uuh`tn0Lu^4puHyMR#g+hT6yp_?g3~9{V z0aAO20D8DW`33%$lEH>|#>H#T$bPhB_Bmo)*xCwBNkGg7>~uPw&tty7qoh#u zPP;W4Ita?_R6Yf*OmfxO)!2=@eV=D?{TeIL#&*@xFcHTVJk$s9_ZM*XTpu@G-jqp( zm@lx@ogU7=SSNQ1+~mW`-PD@gRLn>_5CEXv=fHoa zt-`E!2)yn(FfvJ2Eb>l%8(>O|_(&YceeW8iyhXXOXbj5&+CuTR?oGFbGdbdQqVwzJIrn^Id{l^4jH*X z2)4c!i<{&KjC(yfC$z2zvP5Y@+CHp(zL32WsvkawXP5a@4vjQQ{ukP9MZc{Ww-xiY zVl~PC!p7ak6c-i~70A?@#$o&iZ1SAOS;W;A5`82l4^j{lQ&f}}0Es9H2q`KGKLrUs zeIz6%F9CWab6@IzR58cnSGRL@@OHc}Dwvt%i^c`8&H8`faS5T`tKND1bs^L1Bp7~M zroA#x+UEkNy_z!Lc6|s#Z}{!`&Za=FOd#}S zHF5J9D@AM=8)y90+1XfBg-pA?EPPjQ1Nm#`D4@OYFff(BdWEj~B(OckVnXsTSK1Ue z<2mp!!|IWJEgCljuM&dg3?bTt+@*)$=0Y${A%t@fbV&$)D+D_bLVV$I2ipUOBW1DI zZD5&EEuftZ;zOf!-d^5JeTp`=;0v3wk?J;WJBbRJ$ffJG!B!RwRZ+L1I}l*PuN6R6 zg-9~izEMIz;%dR_E}xyy4e5(!1*a350Y)bIeOtCEYbkY=X6g$8nThLR3aaPK8P<}% zHpE0LUQ$n`wjNm^2>abC3wis+z+o@3t)sP8C^QiSqbv7D5omlXWPAv`+b?^^FYZp> z=H|d$O;-zRXjA1 zy0`-;)n6dLR4ewtiSocu@<8_!lo(C^H%g{5_np zJxq(Pt5|UwCdDaLY!A&1br&I+HTb^v zPG!oX`1Q@4(XL6m^HKF=t0C|wvcM^=E{3g#NEbZZutykY(DY7&*N{dwgj3eSjnAce z$rtR*27(=OXz#tUm>fkrQlDr&!bc5j@;20|ZhzF3tb~nn{WnnfX}dI1T838ag9VE06(zIztqLCOS5~C{`$E}4gXmTg#KGsCknulm7wj5?$ijdyi!A@*z3C}PW~<|TP%rj z&uQ-WVXzBEycq5Y;`#i9r`wvROP8m|bND%E;zGQWk-wg_GIbGt76@s@x?Q*&kcY_N z6D8F2$V^z(Oyu@VX#PyZ!VEeGoI|ri>lkr|XoZ9bfwR&ZOfcYqCg}7&Wf3@G?2Rkz zr_JkolsABB*2`wrPifXCYBoSP-^)AS&oJM|v$HJ2xWp{evjKiR01kT(j^y9F$G=Bb zvq$G95Y+^ZI=N=*yZMl)vO8VfM}MhnaM@6AS|L}CR*IL#rTsqv056Su$YsIg|GX{r> zRd!`Vge{c+p$Y5Vr#O5I3)dx9mF7J93#5fStlD>)xEPmx<6s!63;b8V|H3et;w#{3 zrCMA}f&6vkd zM#^+JbelnDi6vfbojBW3c-;Qoh(d0RSng|(lh_;otU}fsUkc(>rA7gjYbSo+(!wv| zbqOOGw1J!7)hDt`gjF0;Mp^S!9;bSdU+3XInu~a&vVUM1*Eu9r zXYtjxU^_fXxZHl_i!aBQCLly~C+Hi5rcAveTmP2T9nn0i480v0SA^V={nggXl*=o4 ztV6OJJ6ydZJ4pD*2gg5{Yh=ADZml1f*V9MXq{(pKM-HV0R@o*=Ch%~9!-qnv8|MT+&hNzRZvrp zrWMz|h1gcn7*mi_u)>Ro`SXwCsx9f>&X1d(xJJz5HB)+WuNn?kC7Ckc5*izZ!6x6E z7t&a7PN)&z;%!^mR6_Q|d?V&_W~zuqtGrZN$%nq3C&BPKD1*39rv^%=q}-|wO}{sb z=9>atO<``BaJ-INoZWOjku!SRgZv`^O20smq|N2(l!aQ#jk{Qa{$5qgf@)`a2=~=g zo@*&wwbP*7aB$l}WxuCpz@`+A*BqR}db8#~e+-L?Q(pE@xjgA)Xab$5xUwz$7C$%A zaH6VYj$gVl3L}^x$r>$H1pub~5PaBz{KymH{+*yxDX#!#Dl5T^=YO4x&b3sVwT$$& zq`9@UrnQuFwG5KAthp$b$Y{;#)0UneK$q%uIK3w$R1gx+5j`9n zCbdnzirfH)X6}XVdk5_uhVCEUTU=pSM4-z&!NeQT{UAq*U5*xkN5Q2X&z;mB-#Q$w z!(Eno9qR0n%a~cPhC>U0g4n0RpAh3oa~{6^_P+z6aZj~FZ~fbt+*3P$f34U?`@c6{ zp@Ko6=t$}b{t`>&&ZH24`Rd7e#3B9}6@u8vsGwI~wKK^H^#CdRjI0T_gTw_ThU~md zg>L6h5t_+Het;=MCC2IFmf1e?eD0dnqcXY&XXLf%m(*SN>@58*mwtPFY zE(555FtU4il~*cKO(a!3^_m}$w)iQwv&3ibL41Px49cg;Q&PEMa*I}y>e7?yp#~>V zgJX=qZ^W~DOxt<_gXC;?W>X@}oR~9B21}_tf%3obKcM{qx0^Fj_mfIaDq|c=}-JT=m+U>GOLZr)-yexaE zYEPHD4VJ>!P@=|*)KzQw0}|+E;^_Ueh1AU?{LW>uZ!vL`Uzk9h;!l;`+MU@)*`f69 z-k&4>b8vy*qMRtr@GfUFcT&kTnE?KVOVg*TFf4I9=vc!e0AW|*(Mg4g8-&|HHJ(0~ zcDY`wCvNIYJ%Yk&(u&CZ z*mhLs)1llRMl01ouQ@~bwLuw}?LgHey@XrED5aXf+(!m^Q)3x3P4ahD_2VJi8e5Am zZ7Ke@%IgNU)n@4rEn-^#;m^RVEB$vqeV9AjNa$~h>BE(esJ(4IFS3QNGWCVx-^Rvv z`b*6Z$t=%=4wPhlW;G)%$nTdLj>7M)!-wF+K`_)H1YZTiDWAm{xG(!nMZk@zLmZ~9 zq{W`Ih-F8Ue_67o8t|huP3amo+j8v_dpSU~)yucl&$tCLJ6TLbm%uT~av(hz_o5>iRRfG zE2Dk+agv!j9h|gMSFZD*`DUn>#~&=UAK#AI+h#ehp0pY*EGFP#!E^H7tT;hx8$O`l zEWVk>OK{zKxbGj#Zv=)H?mF2pTb7!@iKr6azpI4kOt&HV7JseT?qvd^M7nRAf2~d5 zpEav*=J7IK|1@lueWA-n?a24-_c24)(MB+H@J0S0cC9_j*L6pNxl=2(7~!b^&ZESn z(wvJHc4`;C*?DSl{~!;R)zMJDCp)j_vq$q?z016)cPG4eR_8|4u;86ci2}6?VYYjd zAGF?+=Ep3kw4{1-AT=lQOC(kNQg&DuvS)7D-^D`>2W!88Z%BEL(@`Vo{F;Erlt1;~ z>V;}z{tW=P6uGM3ecGV91eVEgz77H1NKM+uc0bdK^!_vOYSEk0G+CIm-TS(+5~2S# zHH70z^F04h66rUwTLM?^-4V7l?wgTS#kyJbkV^ln@4qMme=@E7?b^Sm(HdAc z{-8@MZuZo!&TEw|%|C8tByqJgYPA$!YwvN_l2z8y{mWT5+yqA9&twpU?Da^z{WF;k zZ=Z>}l8AmP@gGh*ZfF)k2;gw9A7G15EpW2FbnT8hWbZ!|+nIUe(Gh3dikb<8?h-08 z67PN6Q8Lwu9NP}5J;Dhw+e5Zjae$pp@~a&7)Lv`3xkyJ@as=hn9g)>+bwG~jIj%7;2X>#HPJFo*BTjI5>V{p>)?WfJBFLnzDaYZ_!=wODB?k(LGg1CM&nW!_%(w) z!FMM8TA4wq1M}3oCqpvDr;M)5~ zMt{PJUeweZn6G#D4#>1c($oAbHCsq`X`HszNpfOk{84L#RO}qz%p2KWa8)(58{+K9++zCLsmQ`}iJeKUlm5$L zS(<~o_x(W7+HGUrlJ;N{)28FNT@ctj&T_j14>yHa4L3COx2FJSM- z^Ax@4N?)Xvjb|!a(iyzaFC9-&l&8adK~XaPMp69Mqj&MYgS?}h&FCAHIO)xz8_RVa z9CWGIiOtcpem8HL&d#O24wd`4|HnsvG>%W}w0S)_8}8>$78c#vm8i}4{VJ8&;Rgl? z-Ioac$)Hzt`oc2u8e<88d*P+Gk5B*o<^Jy%#6Rzc*7S`w*uK`(x35CSnOo~P^uXVq zeyR~zt}9fo2%;TpsuOo6;yseWWiP32oBy1weOAH=ks!KGHi%7 z|9@ux7c20i?CYMIH`pkx8>QWwyV(v6ckt|7ZN0ob?W|mWLvGeicwXLCp59 jsonVerificationSummary Pretty -> prettyVerificationSummary ppOpts nenv in io $ writeFile f' $ formatSummary summary + +declare_ghost_state :: + String -> + TopLevel SV.Value +declare_ghost_state name = + do allocator <- getHandleAlloc + global <- liftIO (freshGlobalVar allocator (Text.pack name) knownRepr) + return (SV.VGhostVar global) diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index e7fa7c7892..9a7332b86e 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -43,7 +43,6 @@ module SAWScript.Crucible.LLVM.Builtins , llvm_spec_size , llvm_spec_solvers , llvm_ghost_value - , llvm_declare_ghost_state , llvm_equal , llvm_points_to , llvm_conditional_points_to @@ -2795,14 +2794,6 @@ llvm_equal (getAllLLVM -> val1) (getAllLLVM -> val2) = } Setup.addCondition (MS.SetupCond_Equal md val1 val2) -llvm_declare_ghost_state :: - String -> - TopLevel Value -llvm_declare_ghost_state name = - do allocator <- getHandleAlloc - global <- liftIO (Crucible.freshGlobalVar allocator (Text.pack name) knownRepr) - return (VGhostVar global) - llvm_ghost_value :: MS.GhostGlobal -> TypedTerm -> diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 9f4830e4a0..d28188b79c 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -3605,16 +3605,21 @@ primitives = Map.fromList ] -- Ghost state support - , prim "llvm_declare_ghost_state" + , prim "declare_ghost_state" "String -> TopLevel Ghost" - (pureVal llvm_declare_ghost_state) + (pureVal declare_ghost_state) Current [ "Allocates a unique ghost variable." ] + , prim "llvm_declare_ghost_state" + "String -> TopLevel Ghost" + (pureVal declare_ghost_state) + Current + [ "Legacy alternative name for `declare_ghost_state`." ] , prim "crucible_declare_ghost_state" "String -> TopLevel Ghost" - (pureVal llvm_declare_ghost_state) + (pureVal declare_ghost_state) Current - [ "Legacy alternative name for `llvm_declare_ghost_state`." ] + [ "Legacy alternative name for `declare_ghost_state`." ] , prim "llvm_ghost_value" "Ghost -> Term -> LLVMSetup ()" From 72428952c6b0f7a770a1249367aaab102e285a0d Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 13 Oct 2023 11:38:29 -0400 Subject: [PATCH 2/3] Support ghost values in all language backends MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This patch: * Factors out the machinery needed to track ghost state into the `SAWScript.Crucible.Common.Override` and `SAWScript.Builtins` modules. Nothing about ghost state is specific to any language backend, so it deserves to live in a non-LLVM–specific location. * Adds `jvm_ghost_value` and `mir_ghost_value` commands, which behave exactly like the LLVM backend's `llvm_ghost_value` command does, but for the JVM and MIR backends, respectively. * Adds a `test_mir_ghost` test case in SAWScript and the remote API to ensure that everything works as expected. Fixes #1929. --- CHANGES.md | 7 + .../src/Mir/Compositional/Builder.hs | 4 +- .../src/Mir/Compositional/Override.hs | 2 +- doc/manual/manual.md | 11 +- doc/manual/manual.pdf | Bin 587278 -> 587259 bytes intTests/test_mir_ghost/Makefile | 13 ++ intTests/test_mir_ghost/test.linked-mir.json | 1 + intTests/test_mir_ghost/test.rs | 9 ++ intTests/test_mir_ghost/test.saw | 28 ++++ intTests/test_mir_ghost/test.sh | 3 + saw-remote-api/CHANGELOG.md | 2 + saw-remote-api/python/CHANGELOG.md | 2 + .../saw/test-files/mir_ghost.linked-mir.json | 1 + .../python/tests/saw/test-files/mir_ghost.rs | 9 ++ .../python/tests/saw/test_mir_ghost.py | 53 +++++++ .../src/SAWServer/JVMCrucibleSetup.hs | 22 +-- saw-remote-api/src/SAWServer/JVMVerify.hs | 5 +- .../src/SAWServer/MIRCrucibleSetup.hs | 18 ++- saw-remote-api/src/SAWServer/MIRVerify.hs | 5 +- src/SAWScript/Builtins.hs | 23 +++- src/SAWScript/Crucible/Common/MethodSpec.hs | 31 ++++- src/SAWScript/Crucible/Common/Override.hs | 110 ++++++++++++++- src/SAWScript/Crucible/Common/Setup/Value.hs | 11 -- src/SAWScript/Crucible/JVM/Builtins.hs | 44 ++++-- src/SAWScript/Crucible/JVM/Override.hs | 98 +++++-------- src/SAWScript/Crucible/JVM/Setup/Value.hs | 2 - src/SAWScript/Crucible/LLVM/Builtins.hs | 13 +- src/SAWScript/Crucible/LLVM/MethodSpecIR.hs | 29 +--- src/SAWScript/Crucible/LLVM/Override.hs | 130 +----------------- src/SAWScript/Crucible/LLVM/Setup/Value.hs | 2 - src/SAWScript/Crucible/MIR/Builtins.hs | 44 ++++-- src/SAWScript/Crucible/MIR/Override.hs | 72 +++------- src/SAWScript/Crucible/MIR/Setup/Value.hs | 2 - src/SAWScript/Interpreter.hs | 14 ++ 34 files changed, 468 insertions(+), 352 deletions(-) create mode 100644 intTests/test_mir_ghost/Makefile create mode 100644 intTests/test_mir_ghost/test.linked-mir.json create mode 100644 intTests/test_mir_ghost/test.rs create mode 100644 intTests/test_mir_ghost/test.saw create mode 100755 intTests/test_mir_ghost/test.sh create mode 100644 saw-remote-api/python/tests/saw/test-files/mir_ghost.linked-mir.json create mode 100644 saw-remote-api/python/tests/saw/test-files/mir_ghost.rs create mode 100644 saw-remote-api/python/tests/saw/test_mir_ghost.py diff --git a/CHANGES.md b/CHANGES.md index dbf13e439f..d722ae64cb 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -17,6 +17,13 @@ generating LLVM setup scripts for Cryptol FFI functions with the `llvm_ffi_setup` command. For more information, see the [manual](https://github.com/GaloisInc/saw-script/blob/master/doc/manual/manual.md#verifying-cryptol-ffi-functions). +* Ghost state is now supported with the JVM and MIR language backends: + * The `llvm_declare_ghost_state` command is now deprecated in favor of the + new `declare_ghost_state` command, as nothing about this command is + LLVM-specific. + * Add `jvm_ghost_value` and `mir_ghost_value` commands in addition to the + existing `llvm_ghost_value` command. + # Version 1.0 -- 2023-06-26 ## New Features diff --git a/crucible-mir-comp/src/Mir/Compositional/Builder.hs b/crucible-mir-comp/src/Mir/Compositional/Builder.hs index 0e77b644b7..b8271368d6 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Builder.hs +++ b/crucible-mir-comp/src/Mir/Compositional/Builder.hs @@ -641,8 +641,8 @@ substMethodSpec sc sm ms = do MS.SetupCond_Equal loc <$> goSetupValue sv1 <*> goSetupValue sv2 goSetupCondition (MS.SetupCond_Pred loc tt) = MS.SetupCond_Pred loc <$> goTypedTerm tt - goSetupCondition (MS.SetupCond_Ghost b loc gg tt) = - MS.SetupCond_Ghost b loc gg <$> goTypedTerm tt + goSetupCondition (MS.SetupCond_Ghost loc gg tt) = + MS.SetupCond_Ghost loc gg <$> goTypedTerm tt goSetupSlice (MirSetupSliceRaw ref len) = MirSetupSliceRaw <$> goSetupValue ref <*> goSetupValue len diff --git a/crucible-mir-comp/src/Mir/Compositional/Override.hs b/crucible-mir-comp/src/Mir/Compositional/Override.hs index da5d4ce55e..ea63c2122f 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Override.hs +++ b/crucible-mir-comp/src/Mir/Compositional/Override.hs @@ -581,7 +581,7 @@ condTerm sc (MS.SetupCond_Pred md tt) = do sub <- use MS.termSub t' <- liftIO $ SAW.scInstantiateExt sc sub $ SAW.ttTerm tt return (md, t') -condTerm _ (MS.SetupCond_Ghost _ _ _ _) = do +condTerm _ (MS.SetupCond_Ghost _ _ _) = do error $ "learnCond: SetupCond_Ghost is not supported" diff --git a/doc/manual/manual.md b/doc/manual/manual.md index b993b6b719..b6e5beb656 100644 --- a/doc/manual/manual.md +++ b/doc/manual/manual.md @@ -3545,14 +3545,15 @@ with the following function: Ghost state variables do not initially have any particluar type, and can store data of any type. Given an existing ghost variable the following -function can be used to specify its value: +functions can be used to specify its value: * `llvm_ghost_value : Ghost -> Term -> LLVMSetup ()` +* `jvm_ghost_value : Ghost -> Term -> JVMSetup ()` +* `mir_ghost_value : Ghost -> Term -> MIRSetup ()` -Currently, this function can only be used for LLVM verification, though -that will likely be generalized in the future. It can be used in either -the pre state or the post state, to specify the value of ghost state -either before or after the execution of the function, respectively. +These can be used in either the pre state or the post state, to specify the +value of ghost state either before or after the execution of the function, +respectively. ## An Extended Example diff --git a/doc/manual/manual.pdf b/doc/manual/manual.pdf index 67280f5b035144c8784710dcab0b6b0b7b589899..67f1cbdc2db4c2a4e2ae61618dac5f03424dbeab 100644 GIT binary patch delta 10304 zcmcJU1ymf%*6)M62N_(0dvJG`1eYLzKyY_ybRf6{_h3PSgx~~b&>$IHgAGm~Xo3WL zB_i9`gK?Td)Myj?y0@1cGo2AGhFR4ghU{GK+M?%h~8Z2w%QpNnHIcKma^IF}dwPeD#>w-4w84g=VBX?C#3=1wUN3#~M{?2G7R$f1 zDh#Wdb)btlr~1(MvwUxq8?ihB9(1XQE@J6URN0$B9|k^4HRQ{X0@G)5M!g8l<^YI_ zY8iApU-8_C~G9f zokc}0%jawB-gR`k1qDc|w=PLyQ-~lAG)_>nCkxJQJjc^*$!;kz zROn1$WoQ0!X2T`Dk!7wPyyK*!bzTtXg6EacQ+v@MP|WdB;!QcvW{+rcej*@d-kEIA z6j8uNoKnBK$h=zm9Q@f~k#T0(9N5)(mPEBi*7@GvoZL*Rq45Y>?O}p8q~*2m_)$|9 zPoP@*$xMr)hixu+wF(hCWF=sgn-F(A zyn4*iBp-0+6%9)GSYKdTJpBmlngo0>8oW`;wKBf4!XFg(XdBRII9STX!3r#rDKEq` zV2cj~DOMvd@**4~AZ~0B;R`;oNQg&9tQ~ews3P!T6b)@A<5-G|vWQ0O&jR-^`H@== z(0tj_9>slV6&2U&N~amd5_2P*g2n4we(-*Hhzl#6v<Q^v)N0= zWXYBpYacRcKg?iOVhSyISvEzE8Z>EC;?w;z0ulwC%+MeZ}12bL|p_bCvsk`s+I)31>U+Mv7i8RCAFJEUb#5VwdYY z=^4|aFE@9UF1?v9gbNmjqgv zujJoM7wMKx6-hYf+%#1hmLw?i1_wE)Ng|a~I;-Urc%afB^~j6%3h61ft3Z(R%ZFN{ zo=8pj$$;8C9#Dxuw~5aMua@=C3_jRECH6^O&2;oiOn0i^2jX;E**f%48SRPs3wxls zMs9?DI7j_Rpp)qc7`+&ai2B?>xHho1GpMW6B*Ql^%59m^jY7Mf^F~EI?{YkqAqTlW zP?#2WoOf(JK9~x9R3;$lv56L%J3w1Oq}lSUGgPg&TLD77;U&8>uuriglga99-~Z+P z=iNGYU|HD82+RjAnrVTaZpGz_6w|$xS>F(T18t(Aqn0}aen7saU&2SV7NUYyUWd1& z^0U!3#8|KG^Y9f?AyIZ7YcC%@$QkQeuep+8d3iqHK1fPOE&hD@!%j}?WZMTwAJvZA z_yauA>}Nf)d^no2C}XHNK7nh|;x<~oRPVqQjb930qr_&yBS14dW_jOr9?E_#(dnCT zF>$xI6cw9727D!_!tjDZLhwLGJYVIzzfVR!g%c!&>rf+ve*xns(=2Y3QKz?KY&=7t ziKJLbSkKEj#^_47FGMb8*QdZsZuw@$9Uaq4ExmiocmBbLv)iRy%Bwz`1^we zmQU}>!dDP{`o~zoZ3+^w_1D{BgWWnqbn6kIh7HXEWzLj#-hl2moGFFTN}VRs0)o9z z(W*F)3cv{0wo`aX^D)1Ba`WgVs3Qf z1irPF;7(Z8B~NfQd(4s=tnM=KCW3h{RWBiASuR!~pTk4Rd2NNb+v1aj9!72I z8W6(UO@y82PJ|*L(rYNI(~KW8iD!_wSBg>|z%p}QC}d+VH4Q3%;;S*X*!Vh5t#h!h z^B6#zjK5_zG&P3Q)tWlC4tQFT^g@#xeWIX|xP#I?ayq3Jg1pu5$e-8JW`Rw6W^#hE zHv6|rK!H~nJ_I61*~}zm^rdaFsPJ#(2_JH;r+OZpIV-_@)Q#rw6ZT4lAg@I=@`Mbn z9j!~piQ`pr2K&i=w7iVnnow%UP9;y>R|4|!NO>xFsHOs&%MmfQY_8{Bk!2(cSWe~F zm@U5^n1JeOeF`hEk6wh3DfExrtDhc?j{@K4a3Q#~dVW-_a*zFBj@{(efktHEXCkzZM8o0rd8d{OOXDvU zm>RdL6d>!F2(H|I2${N2ztS9>*GP~1F|7Ml!iweUO|15tK7KCj7IcnyC5*yRqbuNB z&XaKM8Ld-JF=YE8O_l>^+8sX31-OOq70SR~#ckr~XW+rY#T}Z_0XO9>-JekzC-ex( z{xW@lw|S{WYksY;CK ziSZ89B`cnkz0p?$5GoaY2Z*9M8q6)FIms)>r4aZhz8oouSneu+i&+qwf<3A}$ptTz zBwX|o_M()(f<(1>cXD#6FPLnM$HMFha=0FA_1t z-!+tY+D_icX7^6kO1hn@cZyu@7?o$s?Pu7#@xq6S%+Gm}MjkNxQUi}3RDmq6Km;Lj z4>{tF4lx{EiEgN;R`DvO`5^@7syb7M!5i0Y@Ql(T|7(bW6igYT>%#J4bB9DH?1v*a zvPrgN{C(ovaTN3^7Q-(lsk~2~I*{s8kAPo@A9aP>S4}Rlx7&b!dQhc0LhqE)zvr&_ z+~~U`CLi!I|N0Pt5!l8+lvxKzua9)<*a|6#DP?wA%T=aT85c;CI?<}!y}XVE?nuLw z!-#J&%Lg}^lWC-V!>qZ9Yb4Vr)y{O+^>)3Pf{JLz!y&YkRbuLCSHX!2rAJ(J`p?Ka zSP8W~(M743#fH0Tv%77ACzqcsfAKjx`I=P_oz6FuiEQ{O)4c4Mr8qA2Nhf3$69c}- zsg}c7g}g>_yVsr0M!qXYAaHFD>oSsy=gCX^Nf+soO@vB!Ye>g%=%g>$GU zE;N2(gY&t8ia?)Uqug|(At3*3fs7h;Jm!DMO;SF1?rVZ!a`wq{b;$mXfz!2g5qf`mB^%#k%X6% zZDcmytjgAF1i6*)wWMro=rlCGpXeD|S;aL_*oOK_ zFKQy@S#?NyTqzjuC> z^MIx_l)WxGB|VcBqLlWlh`qnJ{{4GPycB^d*)BZPKX~T#*=^47Ac@hY8s!X~4iC}m zEyA>A#wW#a`J|Yy@2w`@BSc^{B0YmPv9ZY*JVr$BCAO3YWRG1xvq9azSvEBbQBb!s z?9Ycu+$`d7-(3)yjQFs=#TS?9>JXQb%3tcb({pv47GivkWN=mp19J`<>|gC!2#HgU z4ot)Q1_R+QPlp;(?To9_xtyqhU?~a7T+On`*vd>Cv~_p)fB}CJSqz_BX(QdJAm0NI2<|4tH0MAu0 zY3zCG)$5~JJW?!-tIyBDp6Qd%Mc$R_y<};CUp|*GtJ#YEQ5N*}V770sAr);sz=u&2 zGv>{iC$!%p0vEz$x^qf628&?uAG zO9j{6Y1_xh6fG}S+}_SX1pIbU#8g;{{O8{aRw;8SSfR&lU{Y{;SkcJwh9y(-gP?sa zL%H>2^DXY`^UcntBHsnH=2cC0It3Y=K$OGymPo}Rs{D@Fm3}_z5`)Z`6-?Dg|BpA0`-9=XR&#(zrzo$)6o# zAXUd{`79l)U39E_Ts0*~?Q>@^R8u*js=ZR$9*T!-s?J%vvC{|n2#S*#)RMA$JxqvV z?wN$sQA3XFd%+Qj?{mMb#}`|5Pp z(G)kT=Ww)O=n&7PeE0dyBu|G(&azqO$?5UZ(ZxofxQWy=Sk#X}DXE(6s)pEI>h9}K zWryzw{A32-U2=tZNme$>#|4;p&Wx^78Fi%b@zqtJvA{+02PYZjG1Tn#@8W!kHCUgbU8JHWs=NXH(q40jHh= zC)%crTBgGXX7OX6%4cnmZO=sN3F1;-0s4tEq)-Hz!J~!Ma-Wwk>I$o$+99kk>qK*l2l^o5l3V-k4hGBFUM1C8o{S_g|yZ{>1+z9~1aG3d^z!uaaR$LT~eG_@+R5ChW4um#O|^#0Y)0_4yLK=#$= zd!5&OFyLf?y&SZsxPq8Ij03{q-#Q?P8yQ@BRG%zjvq&74EYiBt>u9ZcAhhV`V`RNM z@!CBC1$*zs{TuPW544^9E=Yd;*P4!wdg*ENEe{UGU8}ce)_wLf9c#ARh>6Q@fpCs{9 z3S+s|PAt#Wt7Zg|vt7O=-JOhexbj%5|ab&G)X)(*a@^o z;k;^}zHKE06`y_M2);331l4HVAw3kKCd zrr{Pm63VD(!2v*F8pQnqSszl)gT-!1Tn!eeBasaEIufal!l@(Z4AH0qH9_>}P`_BB z?MFPTqd0?@&7obvA5f~HPIgh02QY%L)0OsUDamn3Mx>(3k47A#8mYUHe31^XEiJqA##c`f1z>~lTVb8`kkjEVYC zTOLqZ$pTJ*g?m}gJW3r|I)u57*t?r+4$mA)6rCs$Zg52YC_`W*9ZGV9GA|fSCyC3v z%9tBA>52;L77@lHU8Oe-8+JvZ=bl{^T@1-_#d7YUTnue@#XIQ9I3gAgi8?~3?jiEU zgntw1075d3FwJ_zJ3^cBxmJ46E*7GR7UW+iJ_^t4Qqtw8y^S0fet-tYrvy8=QaoZ7 z*^l#Wrf`Nz_&(_GJmp+c%gmjg8bsmA!qVw`?)yM%m9+!;kln0j<9Z^C(-q;MXCuk3 ziJ%6emx--o>=JhW13vQ0$`?azhGU3F2^~>C0<3uQxI_BtL_yaVcU^(U&b{pfhl(8( ze~BC>+9{2Qg+-S~{F@`Dfy3_M7no*0fBx#u1okXnU4bM_@wWHy4g@`Z$< zz(3S~6~-91diqtCIMo`cciTSetMuBhq!qLpxj@%d6vt?O6@p(Xmed5+V3V5!1o4qv(Rrc@?lvwRy-l+ybZ`I8J2fR;w7>#jX0!}OQv3+~hR z5&>Pqr4n37z^Z?E6aF_rU5V1&y>2~rqaFBB{%;?BoUX%3hZtJ6MU?uK=UORe(OD(0ei=>t_>USrq8lwDq;mA=7szBU5OC-mL`&f5G zZ5*w>TWa`{YQ5yrJMN87o>51t`=B8p#ro>J&-^?TIBY;m-MDb+cTf#CDuwR<>c~~$ z+>pQR!kC2lJy#@WAk5!NpN>xq&1aSCt&GiKIOdBp0`aIQ75B^9UJ)sf9G(z>1Q);yq1Bf{cTBcgojkr|KWm-SWR7r10zW`@hdqImt6m z5IXeX0<&5P{DBy}7FDoVkm2z?v|@RTz}-r3^HI+6UsQo9D&b&I&Thqo5=$zWx-^N{Vfj3^HT&GIKa@XN~dY-F58-S#4ThCc2 zRxDQBe)=lm;NO8U9w1jVDC{a9>wle$&{CQ%>yXxD{Rw>sj1qnL*DNALH zmw7_tOs)L&Vma9`;|ahC&2q;vMRZN<7hg(Y;)l9F^L7`rU{uF{aDU>qJg8a%~3 z=bvPh@b@P+AE>5Wf0=YE>-Bl$JrMj0Tg~5Y^wY_UL0ODE~47VpkGf7{3?FaUK`~7j}WzPS#Lj1zp3K^;hrn`5X_C{nj)%Mf;ghI zEKmY58|n!4q4tJY1yIoo%9$S2IdpT#qd9C73wFowZ*@q&=BoSYi+evj$CVbubxY&6 z_In0laDA8nbrVKlhCj>&^ShG3pnfgD15!AlDVW`rxCZLgLWix`9Q|(fopsBBRDbIt zSfmBX2Tr{h#SLe#dm(;_Pc0+d94>B$=63=Tk0P~@^WziD7ktgU4aez-^f{uI3_*Vg zE5#3`*L;eMNx&jsm?=*iK;UA8uK13OsVB%_O+e({h#xBZN9`{G{Pz2$V&;g3W$4f% zDIdCPfBL@@kUoUpjaeB}s(_h0iAfp$?=N3`;Kt#Ma0Q@T{R>@v)*fEFPjVTrP^$V) zt$khmIurwCoQ@xXIxlLE7fdR0-0x_e#X7XW06cLWkETN~1R0EfsAfrSV}TH7LC2vA z?(*c2Yp>7kk6I;H&jrNdiKPB>EQwHa1ubS~xmnq4p^76nzqF}g z?kTt#7ar4SL20(cJ%BuG*)G$>hJ{;S;LQ#&Q$wwM5w+mIdhUqO4C;`1p8${m%g_My z?E_BMji-^Ol}T#E?iI3JdY?)$TXpF&*nSzaIm7zukmr0zdG&fq?OSwlGT2t0ZkkjE zsx{~h9^rL@l=yq+v#l@o?)chz+5c=NE!s}8<99=B%~N?p|JZaRGi-XR_MUn@tE^F* z_Nr(De%;J@5-K=6O^g8{bm2!WNAD=cgWbYauw@F3u|yaz%?iFxu6c&c>7QH^ zV0Pac@Gs3xl>TmOCc%WroXA{@Nk=WA-=V)XUlV+{S^kC{u@QZWUOQHr^S_Cl<3{aS zn?Q|!!l{3Df7WwW{T_}flN316^>AA$kP};A={LY1hov6`NnHyMYej13E3;~Tf%7a# z5OllyMHux@k6-SMgJwDV0^5J#B}`g#f6;EuAFShY{iEtHmp_g_Iw;zBEnHG7Hr#TB zj|J}eF}uunAGtgL3afe#b_;{J(69V>kv8AtKgJo?bst##iil9~_8(yjQ6zE`%@XaB zfF1HVs+QSg$oud+hQ6!AY3jk9!)Uh<>J2*l6~5tOBOd=4cX}{{G0ImT=Y}@8;=+1R zTpRok2wSWqd;lCXNSd|%y4HY*c@%{!ku&r^Q)L}r)Y{d?fUTna7krJiamA50%}2PI zup2sCQCrah_2VvY3A19}0_?NtJK|?BkG9_=oRkhut(zQ^{Bim}rL2dnN6%{@Up=Vh zp?MuZ@N&fNzW^Hf3yG~y|L!z8oE>|x{*?QX4shv}%UIO9vuO~rkh_pO{0ED2X}M#6 z$6~{M&YnBHsFP(Hc;X9a%DPjh7=4zg8LaqR@mZo}a2<*>_>t&PTzB`@KxmCRPCKnU^nC}HnqYdle?!U6!d!VuZyD)p{Pt=|fZief>7Le%g zf4>pzC=`;0nj!zQ02B(DOII?~gRWe9vxa17@ZuthNWo@g{+2tDe=C-A4M`H1jrL%)B!khZiJ32ISgXdg1ntt0RZQR>yNo0z2CzG`wvCuN}74ggy8AUai>n1 zlkua=q3v8efs5f+Z8RU~vCVfoXZ;@pn;sqK%`o^@U+M2*TrhPH2pNw;YKbIa4j)4@ z+G-okLeV^Eiius0ts)b-8`rLucl!s{R%tv797HCMX|sM7`{cU=o`v-e6nI_*fITSM zt#Yrrf0C#8$}o2LSb3HyuGFqW`MfAyIX+{jZMohwK4Ukyl*x2m%M%A?*xg_7b$Rw= z%BSP$ta1X1bBFOPKfHb_e)cQ*S^ZA@>@Li1aK-l{my#77rIL}Gni}Civb^j-S-)@W z0S>1MrOV_CfFr?53qjIsGG*`>;99CO4ii}}-V@@r+NC_4{2`WApPPWU6EkmUI6zGR zbi8G%U!U_*UNUqX81Ni*7(AE@+Dx<=G7K3g_w4iL=v(J+dn2AO3)}6dS;OMmiMbX| zAUUU6H(8si*~unfZ^2EzBa4cQO}KhmHYTj7ydl+p+2dY;5W*%WgsJO_I`U-TK<;*owWS2!|Cy> z=)ex{PD%PhtgUrZ`jh+r>edMSlyVZQ;yw+4dXwZg@)oW&qdyJo9^Bt;FEepPR(@lB zVNFCuepz93;B+iH5L^DbgpJ-MVk@ybgZBJ%fR4Hp{qwa7{^cbwN&D^8R%UEl&-s*3 z5+LXexaCtHI*_`3ckvlE%@}lSHQtt90-UV8@sh~u^yM%XO4&7EqJEb%`2DVv`kl$( z$ieA&Ti!@uL-dR(-|0t5W1kchTP}q?=l81yxAq?nn2N2?-grrYf>vTwYC5}eSJAc} zUG$$ny4YIDUPTiE)Q{c)g3v_qyj7RGU1X`-2BN_29b~D?E252+%+A8g!e-&alCpxf$_@Xie(M zDH{0d16i9{M%puGuYTv*6ihT{{CPpig3h5JM4&ndHNEx>#jw@5D;TinH2x-TSZmz; z+(b?9in{vgH|tRHSEF6tI*!(W5QmdMG%irIwH%5+|QMx zaFmXS`!%Yqzq0ZN$0UhT+V2xp*VO(4;6F|Oe=NhXgF90D1=wpeH{sAbq#2zL62DhM UcYmN$Uz~nzX|-pjVD%CT5M$!X?){cQ0uB)bb_!R7$Ju~R2@)PEfmy(r=Cr4E0Zx+Y9D9Y z41N;RNBga>=|CF%7`=58YiVPeHoZn1QrF)j5c96@#EIRUX%b;! zZQih;m%#U-6;Ab3DxLBA2et9zY>0veqLYt91BfASqDvMf$>W<_pO(aH&?E8_YI?fss1(5UK1TldKkr@j#pwa?@!IV`n$SpTzDaO|DiJqSs{ zLt`?(M=a%8ZEoWy(oya6m}_!V-Oks3VLJ*oHwk&ujaBRX`-_3UPEvoK$p@)hDE5TL zmlTB?gC{(bV?+|i`n<70pT9R%RT)a zducKYvh{g8}~}J%Doez2-B>ag|xHdxpwCR zT+6g}i`LiQ15W4VpUg=KFL?B#sx?*w-ir);#J}PqrmV`i8SRp~3R?Q^*BG5g~>;zpt%|j-!f!$_`y`_Y(aq)-V0p&9Hs!_Qmv7pR2^eWL!?8Eum}81dj~=YD8DzzG!!P=V_ym z7QQxyhkpaV;Qp`t**Fnnz*`8OGOhFAwq&Nfjui*)lwqd)jwHT^xj{9m-vh?fB_)<4I_!mF$R3h-|$BS6Dv8|WJQNJZhCtA?ZoTr z0)Jm6?p}18Ma;374i07~E_?Rn7~a~Y$B8w(B3avL%;;q8_Yqk$lOG@f0A`5{?7sZ1 zLPyeqnSjZWv!kI;&reSVvu1p>GPqF_UTlsOTqZfS-Q3>kHcx&0nQn4F$h?h>b^M?& zg?JQfG!;0m7@#Rbjm}BYFKxLq_4CrSW-NmUU9j-Q&*e1|a+ZWZRpOZdigLY=Rkr?$ z{mY%QGpEbDz1*%$B<61*nyE_1(f8soOtdrK8h5{(Zj!3;ODqS;H~RYt3NTvD?#i^% zw7;9cTtf1UDYQ9y6t8ug4aT{dc1%Smk!tKk&@&yQ0wDdCN3P163Q|Pc} zJQMffAuiUu5Pk5((z|h9MCHjFi#`0s2D3dTCd5Oup8|-fGyqQMu7_@uA|(-sNJ1AW z*irUMPCrCFU&&k%q7c7otVmEkbA>KY`Ni+)!HfDGo3$V{8=CgjIJDrG<*_fL>3UWJ z@ar6QUJMZW@6ZMu$o9jS)!8W9;Vv*bE=>zrJ$uic_V8=qcECLXq?xE;_0x1uofXPA zN&2snO`UtZ=D(g+53`Errt;<&=vi62c~u= ztp$+>*O%pi^C$YUwelz<>{J@_lcK1%Xh{6!;{?TvTI{*-6G7nzM0(xr!~5JG&roD! z)B16B8MHaV5JK=`2z4Iu$guHG9I50NWO&%hxDxFLUpf4Ba`EK86X!Q5<%MHsL6=kT zrRc05oKf|YU2HZ9WhGXe zNT}90O3o$HLOYIK)IMFBQL{1RaPlya@9L8JG!lh+14z(}M?R>foUqD2eZ7qxv_P4{ zVZc+y9?>k;DL8ysnjdI_BC}DnC@-S8R2N?YJ}$GS`PCliM9OWlshN<84D1eB#1#${ zFl8d7fLPN!M91Le`RJs!84?YjGR;poSmZ9wCIKtT;-|gfkt@!f_Fa$OF6v+;q2 z*RGtk-ikQ-FUC>$1)v>Cq9dkc*S)Om`f^Tzg$LhtxVkJN=Yk7p4NE>ZMSd-4bQu5E zc4I?~``9X2@p#Aws-qWQ6lX7-J7>}q8!ga5(%)KgDDKiKedVRCk%@oH5d6#aGL(aGrDcg zz?`e1Q(387R<^jXvkkXC*GZCGo(S59T4qpS z69Na{&MU}GCW?O&5`PDRkV+mh z?@2QB&@6EXv}dsH`XM}sO>~xQJipz2O1j$TX19l8|6UEN?`ei_n#4`6dqt3@UqS*t za(q*+lqM4<5RRpozQsFw!=Xev{H^|R1n?dWkl@Ceg0xEE6ZbO(jk<;)o-0D4o2@UW z8!>jOdPK0`r%wGNzSbKKP*jtIhN&*Z?c9lc7bt+{ml}$OX1-hvY6<}d!7Xz{feofTYHll!f;V@PE)AHuu7|R6UP&44pnt}6hn7dIE=+c zgL$)Q8%#%Cd0w3T29)owey6ZOX+mF8AREIWn~de(t$UB4pf`&(4#H@v#Ntxv(p~`6 zbWkfStShN2t;SOlBU$hu^@uUP#q05aC0^;tf&`@?vI}+1Dv8!aAKWhVVMiHPZ^H4jjKF zF$T$8nk5OJZ)!%zLw0Fx1(XyP0kO5YIT7$QN7hCK*@pIW)3o$AYtKI_aBy8OBfFAf zqgyh_&!5AeTpouDf+b8dm}YezN&Lc{V*FK8d8VCwaTsvet2D8mflqx~`wKZd`aW2l zswNzEq|7#{TEs<_5#ry{+m%t|L2+2=}iD177K;+W5E6)p< z@kpfjzo7}|2E|3ZTH3EIrt0Q=R<0W-t&Sl_qB2B2-^R?H-?L^vzG$P^{My(5Xx%(PC2pO`uZvzljv$A*SmQms1giS+&zxQiqC8i}bz} zqOmhnmZ$NqUnyj0g%IErclTv0d!LIDeM+>A{62*~*sm3xW2v$>^fEEVjx7yMC&jWK zNW_O5-P}txv9H)|wHNQyPzt(udS%c3cAqSUH(wD_m zVr)z$qlD`tuK<3*5#NV|bsU{Qr!n!KXv|0G=JKSa_sfTgWYj6K`D9gEscc;AN0a+j zf{$`AgndczG9htOVqye*-UOMtarK`+&mQzMuMRq8Z_&E@ogngL03FX&B9`f|`}$^Q zM|W>;Y6wgPJKkry^{6X64%L^^wDsJpA#7V&IdpB2lTpe|N|dfqP|7Ug0-n$KZx+*7$ew;l4>MZ7XZ%_OJ3Vf-X>Cv!u}iH`JV1`@VzEc9 zKB>^C!V^j!#a8ir6rWifTlyxU2hSipp=TEAsI8?T=42pq@jX66&Gsm}vNmE}SF$H9 zxQ>Ke%AU%oIx?)A^D6tjK7aXO;V46d*C{*0IApL#k(vXZ9qKU}Eh^+cJbP!^Y_)xQ zBXwDxugh;Er(a96KcXXV1o`z)ms8HJQI^m$=k2v3HxB#}>6dQIkQrNnv=N_XdV$G2 zMN4Uo_(|(;?BqqR{MmNuTVvx6gHSREZAq7L50k0|LUOktsq^0HNc1G4JvTod7fBPc&At1e3 zE>IrvjxkiL_+ir8izc>K;S#(>K`75f@^^QYN`u_8U9xtD_qqo?&!{wx-FB=YAN6Ho zrX}HAgQL?F2|eUtN|J>l1RAeHw4n^;@iRQuh0^>ugH-Xd-9CxW-2f?XX?}Ii9j)u1_q83vf5zzQNDmHh@0PW|@TIq zHn6A85##54Ok)nUtWecxfj^^yz&8aW;(Ov>6~CZ@Z{{?z)VcN0eV&`DZ&SCLW|ZQi z(OZ#ktm6`Z?*+eA!>cif99B`%weHI2vi z8=APM@fPuo)Foxbq(sC-L_{UjMI@zF#YJVs#iV7#)x<@lq*SD2715VLeB8 zXOIhrYD7{>qEfKEk+T!`lBj|%7F}qasig=?nC_loQIEiik zNpvwC3B;7=E=#25_Z+%jqCuE-CBn(I+h87!35$BrBd&lraPuCYwZb)gR82-{UslZ8P5+sL-Vbn`c4d z=dRM{IuHmSP>2pp`-S<&H!D|It=$yVU%U*3l*@%e01`g-(x-O9Ld$%SxU+8Ye)ZIr zo|wLNyNttQ3VjD30-_Ki*@U0LID56)JS`rGQMwBV+tt*juEe|N@G|I#FGyh5TM4QRJ&Y$pt3zE_rTP$@} zv7#p{MW5%Gr~-~G%?%Pwv*W${7m;cTW4UmDYu}QLE|N|2H31|2@S)dlowdsUgyLp9Y8!jG=U@ZD)J4lXW2(D$*RH|LKycD$UoDGop~@!;GE`yMhk%bq z%UN92vf|nin3oti{tt$Fshrm=LpAkZjk!WvMZr-ADXdo{iSOux*#BtC{g&5_9a+r( z%M5?+o;J_`!feBbAW;y3jv{*V4CB<_W>S7{T1A=mUxrc4BWQvwG|nHIgfD=XqjX^c zE=aXvlIuLs1^VLOjaw3c`6l@E396=|4(DYZ$xa@_9P4nx9+9w~B3os%G zsQ8TjcOYE0b*#gStApGJ-Ck9o`pol7qz4O)5jhsJo-sQB>nReAWR;8r ziI=!amx#nNSfw&R5)G{~4fVcvSpEI$Dy6vu9&-Kud-lX)KuQZ9%CiGHUp1L4cZKyU zXwN$`cZHayMt!d8`Hn!0;n_Np)P}9H;fB}l?MDU(0Mw+c#6%xboT(%E;71M4 zU0S{ov-~o&u|oFiueN>8Z$0>y%sTE;UX&a*MD9H9^)~&php8|4CMBxXJ;D!Ks!-bM zFDIwlUuFK;I@m8ij#Q9qvJLC!l-_+Sz(q)dhKB}TFV5`h6MT{Y-i z@O#Lyr!k)ZX=VgUue!q)qT9%QIriZ9-Kok@X!Iw% zVPuz9bq~LDh~_Y!JlETBGROOM7Ka*%e^$>GUeg}krs}S@3y;c#w-n9dIl6$gUSKWZ zb&!LRNE3%#X^YD{G3ZdjGGn)Ns0Y^49S$-=0`GJ*E)$Ob>V|A#4)FTNR5sztjwbRg zL5FA^gjDM&!^PVr6FYj*I4ar@5>Qd-dnP4;WVFk%jH zne2XlL96vG=#Nh*%JNlc3=0+t&=Lt99a%V@^-Irz(zGt*0Da{k;9OY+%6bt-FA>@! z5mrj8;0UX5PODf)t3+z67;~!xNvk+-t0dx?X#JUZ!I@aMnMCI1c$)%w7{lQZ>+G9mD@VZ7OJ`s_a0Yy`G7jMGu1)&H8uj}w$0D9$oquD8lijl^+Z zrE%}og!lRaA*7;Sd2FOtSpMhacPkY*Ux7)5ssR#Y$Y?dL`*srMn9S+YktVmxy=s#hb4zvCb0Qt8% z>>*#3-%<(BJA^@`fjk}b|M&KPZ+=ZNA=-(twJ|naoTsal9wc;Qec5vCb+O({YU#Y! z7nTwvGp_>QKo3Bm+eD!ERb`h>^So#)gV3w^>b?Ni zE)CZnr)Dg%ZHoR)Dc3(20qZW2qa*35CjVrjy zNa~|){cB_4Y0OPBlrwUZK#d|l^JFDGAWJ%+Gd!RgK43ES3rY8jn2ye9YkbC@Zq?68 z^C~978u0J91sd$q(^@iz!5D<^xZ2&guR@0nQ-Z6K`p5FZCzaFdUgwF~4 zmh)*(v;){czjmir3-A{+MYOR!BGRo^IMYBe5KbF_cDmKrZ@xo&X!AqpUvJv!&92ZC z6lYDu-gJ;e$D6@%XbV61d3%p9Zl=TElKz1-k=lHIx~;Hep}Hbnfh~%E!J^~V;$_|L z^v@$%7X^Mj0K@ z2Moemvbg1*{UX9n$UC8H1ED`gZ>1Qyrt1EWHq`kLKz~zTA-3)ByO}5CHLpGHhH*Im z;Jdau+}CxaS3t5TPdZIcDugE!wEdioRppRqFdW7iwHvdSkPmvA=$hdQdt@G3^p^BdZ6+fzGQ# zu$(VES=0e%O3eHB_Vng6n*ZsIk*DYDCwU}iH=eEKYbpi~+pfRG94qR}( z_zXJnzd5?~LNl<$@tr6J!QbA-h(i7?CTBv@qcy?f1hjc`zOkx8AYuA>m+4_vjMO_v zt^vKY3;}W5@@E*|url!_C|&-@t1KSk^bg08jULyeUU`Oxqu9xp)wBDmLx6shZ(y5u zF;bLn>v35EK|qclQz1>N?h*5uLsjmdO1u~$OT}CBUz>7h0&Lr=ZGHw4i_N=#pAs{wF~GqCdc^)qKk0@z2?jtHF?SRlX6O z&eS0O8;i@T<0o59V;;pz1Rd1i*8`Roz}@}uMUSURhMa$|{cqv_aGWv=PyDf~E;u8t zN3u=5+Q&%+-mzCmWW=N2>USy zZ>G+;1NP5}4gvI*yKrDftacl!ZrXE!G2Z{~sMZGYaP1SDZ@l_G#e5Fzp0jM+Tj^Lx zZ)E8bCSUBRJ;4jgIq>;9MXAtmH9sYO4%l;>kM%`4L^K(?^=-U%lvWhzIA?52a+4iX z;XdxT@n3q?d7_HB?>5qKHIf!Wci)G3@@{YHvp<)-W;b8mBr;Oc4QlgsE1R$@vDx>{ zw+w^K`gqKlRCimq;W+2phh6x1d_Sz(w+pf1kTq)VzSq`4$>OqL7h}__X!N;TtnFRn zu}5uBbv%xaO!Po3f1?DDEQ@C(q)gPx`7BvbpUJhB|0YC^1Wb5v8Y-B>4e=rInK_Zq2+1Y!nKiEu`A7m*zdnV05=>x*88SbXHk#{3Z{v2`+UxROYjXOk z9D=L4TmDly4i~Xoe#o}y)8l@v1`aj#F%KfM6@2O&KTJXTGuy`0fov)2YiEKm{Sv5M z$dQ0}6|d}i&JPTfF~6-UlZtj=eBjU4IOkskVIjkY&lc=LprM+?MgzFB0PynO_ zuogJ36s;ehn&eR47G~w|91`-L6tL!i#-|jW>f1>7;hN1tv84F$cU7v&_0x}(aHXpp ztBV95Ou!np(xh7Db-)vj=+x=tGEvyqng&VYx6seR(Q(6`!a( zSE5rbr^@hQU$00UUa$k!BwxRPhyvEqzsJJ9wz=^s-m_3#6jltZZ0Cl?A}IJ-^CVdO zD%&lyV)w-?6j@Z5lCAusq#Ee!4pE*>_be8#ps}41(Wy!Mfq_=7?uKFKhM|kMG>LsI}a`xqWjM=+xi#I*2U_)b(yt6nGU?N2JKK$j=GHS>*6e7ivX| zm(Eqt2Edfuqn&3zhZ^LkGp!gmzRye_esDA!s7iAbTzb6Tz%tQlyrWyC*6?)lg+;}q zD*J}W$*<=8mQ|K_9zOF5vnu@tsmWL~ev`WxlF4n;3d1Vd2FUt^jw!!>m2gAHM7c?Y zP8DZE=mdcYzg87vgZpnqjeiIEoyiUIUkKZW*JnZWD5WcN7-V~T`G>_)@X_O{$_AgQ zAWAFwtjV+GhZah~URF1F2DT@ZGG3EGH)itBCrv#&%57q+a>}=-J=4mgxFH`3Hv#AWa5_&|OOl&LXZt z_X#_M&pVd?|AXuQvou659)b+(Rk=Rx^u1+OP;V^#uS?C} u32 { + unimplemented!("This should be overridden") +} + +pub fn example() -> u32 { + next(); + next(); + next() +} diff --git a/intTests/test_mir_ghost/test.saw b/intTests/test_mir_ghost/test.saw new file mode 100644 index 0000000000..01046b4bcc --- /dev/null +++ b/intTests/test_mir_ghost/test.saw @@ -0,0 +1,28 @@ +enable_experimental; + +let next_spec counter = do { + n <- mir_fresh_var "n" mir_u32; + mir_ghost_value counter n; + + mir_execute_func []; + + mir_ghost_value counter {{n+1}}; + mir_return (mir_term {{n}}); +}; + +let example_spec counter = do { + n <- mir_fresh_var "nm" mir_u32; + mir_precond {{n < 2}}; + mir_ghost_value counter n; + + mir_execute_func []; + + mir_ghost_value counter {{n+3}}; + mir_return (mir_term {{n+2}}); +}; + +counter <- declare_ghost_state "ctr"; +m <- mir_load_module "test.linked-mir.json"; + +next <- mir_unsafe_assume_spec m "test::next" (next_spec counter); +mir_verify m "test::example" [next] false (example_spec counter) z3; diff --git a/intTests/test_mir_ghost/test.sh b/intTests/test_mir_ghost/test.sh new file mode 100755 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test_mir_ghost/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw diff --git a/saw-remote-api/CHANGELOG.md b/saw-remote-api/CHANGELOG.md index 1316e3e6ba..8aafd8075b 100644 --- a/saw-remote-api/CHANGELOG.md +++ b/saw-remote-api/CHANGELOG.md @@ -35,6 +35,8 @@ * Add `"slice"` and `"slice range"` `setup value`s representing slices in MIR verification. Attempting to use these in LLVM or JVM verification will raise an error. +* The `SAW/create ghost variable` command and the associated + `ghost variable value` value are now supported with JVM and MIR verification. ## 1.0.0 -- 2023-06-26 diff --git a/saw-remote-api/python/CHANGELOG.md b/saw-remote-api/python/CHANGELOG.md index 4892e5c863..b2434fd8fc 100644 --- a/saw-remote-api/python/CHANGELOG.md +++ b/saw-remote-api/python/CHANGELOG.md @@ -38,6 +38,8 @@ variable. This function is currently only supported with LLVM and MIR verification, and using this function with JVM verification will raise an error. +* The `create_ghost_variable()` and `ghost_value()` functions are now supported + with JVM and MIR verification. ## 1.0.1 -- YYYY-MM-DD diff --git a/saw-remote-api/python/tests/saw/test-files/mir_ghost.linked-mir.json b/saw-remote-api/python/tests/saw/test-files/mir_ghost.linked-mir.json new file mode 100644 index 0000000000..f09a6a8147 --- /dev/null +++ b/saw-remote-api/python/tests/saw/test-files/mir_ghost.linked-mir.json @@ -0,0 +1 @@ +{"fns":[{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[],"terminator":{"args":[],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::ae5488df1dc4e585"},"kind":"Constant"},"kind":"Call","pos":"mir_ghost.rs:6:5: 6:11"}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"args":[],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}},"bb2"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::ae5488df1dc4e585"},"kind":"Constant"},"kind":"Call","pos":"mir_ghost.rs:7:5: 7:11"}},"blockid":"bb1"},{"block":{"data":[],"terminator":{"args":[],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"bb3"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::ae5488df1dc4e585"},"kind":"Constant"},"kind":"Call","pos":"mir_ghost.rs:8:5: 8:11"}},"blockid":"bb2"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"mir_ghost.rs:9:2: 9:2"}},"blockid":"bb3"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}]},"name":"mir_ghost/150ed446::example","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_22","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:24: 709:45 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"mir_ghost/150ed4465f8cb026::{{alloc}}[0]","kind":"static_ref"},"ty":"ty::Ref::c2a5dcbb98af2a61"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_5","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:24: 709:45 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_22","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:24: 709:45 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_5","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Ref::675b2a8049aad652"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:24: 709:45 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Move"},"ty":"ty::Ref::675b2a8049aad652","type":{"kind":"Pointer(Unsize)"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"mir_ghost.rs:2:20: 2:47","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"mir_ghost/150ed4465f8cb026::{{alloc}}[1]","kind":"static_ref"},"ty":"ty::Ref::c2a5dcbb98af2a61"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_16","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"mir_ghost.rs:2:20: 2:47","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_15","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"mir_ghost.rs:2:20: 2:47","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_16","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::675b2a8049aad652"}},"pos":"mir_ghost.rs:2:20: 2:47","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_15","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Move"},"ty":"ty::Ref::675b2a8049aad652","type":{"kind":"Pointer(Unsize)"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::d0bd7bf253977b90"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"mir_ghost/150ed4465f8cb026::{{alloc}}[2]","kind":"static_ref"},"ty":"ty::Ref::d0bd7bf253977b90"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_19","ty":"ty::Ref::d0bd7bf253977b90"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::d0bd7bf253977b90"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::d0bd7bf253977b90"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_19","ty":"ty::Ref::d0bd7bf253977b90"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::913e2ff5487f7787"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::d0bd7bf253977b90"}},"kind":"Move"},"ty":"ty::Ref::913e2ff5487f7787","type":{"kind":"Pointer(Unsize)"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Move"},{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_13","ty":"ty::Adt::ba5184b53bc36a4d"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::76afb566734aff77"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !mir_ghost.rs:2:5: 2:48"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_12","ty":"ty::Ref::bf4d6d337c623aee"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !mir_ghost.rs:2:5: 2:48","rhs":{"borrowkind":"Shared","kind":"Ref","refvar":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_13","ty":"ty::Adt::ba5184b53bc36a4d"}},"region":"unimplement"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::bf4d6d337c623aee"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_12","ty":"ty::Ref::bf4d6d337c623aee"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::bf4d6d337c623aee"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::Adt::613f1953a8669d14"}},"bb2"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::72bf0f6662028c6a"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !mir_ghost.rs:2:5: 2:48"}},"blockid":"bb1"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_9","ty":"ty::Array::6167cd8fdeb01e06"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !mir_ghost.rs:2:5: 2:48","rhs":{"akind":{"kind":"Array","ty":"ty::Adt::613f1953a8669d14"},"kind":"Aggregate","ops":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::Adt::613f1953a8669d14"}},"kind":"Move"}]}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_8","ty":"ty::Ref::41f3f8f95d02c3e9"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !mir_ghost.rs:2:5: 2:48","rhs":{"borrowkind":"Shared","kind":"Ref","refvar":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_9","ty":"ty::Array::6167cd8fdeb01e06"}},"region":"unimplement"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::41f3f8f95d02c3e9"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_8","ty":"ty::Ref::41f3f8f95d02c3e9"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::913e2ff5487f7787"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::41f3f8f95d02c3e9"}},"kind":"Move"},"ty":"ty::Ref::913e2ff5487f7787","type":{"kind":"Pointer(Unsize)"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Move"},{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Adt::ba5184b53bc36a4d"}},"bb3"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::76afb566734aff77"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !mir_ghost.rs:2:5: 2:48"}},"blockid":"bb2"},{"block":{"data":[],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Adt::ba5184b53bc36a4d"}},"kind":"Move"}],"cleanup":null,"destination":null,"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::906e67453a1bbab9"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:9: 57:73 !mir_ghost.rs:2:5: 2:48"}},"blockid":"bb3"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":true,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::Never::7199a9b06188843c"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Adt::ba5184b53bc36a4d"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_5","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::913e2ff5487f7787"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::41f3f8f95d02c3e9"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_8","ty":"ty::Ref::41f3f8f95d02c3e9"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_9","ty":"ty::Array::6167cd8fdeb01e06"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::Adt::613f1953a8669d14"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::bf4d6d337c623aee"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_12","ty":"ty::Ref::bf4d6d337c623aee"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_13","ty":"ty::Adt::ba5184b53bc36a4d"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_15","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_16","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::913e2ff5487f7787"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_19","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_22","ty":"ty::Ref::c2a5dcbb98af2a61"}]},"name":"mir_ghost/150ed446::next","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::bf4d6d337c623aee"}],"body":{"blocks":[{"block":{"data":[{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:328:23: 328:24 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::bf4d6d337c623aee"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::bf4d6d337c623aee"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:328:23: 328:24 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::bf4d6d337c623aee"}},"kind":"Copy"}}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:328:26: 328:33 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::FnPtr::07cd89921cc84271"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::FnPtr::07cd89921cc84271"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:328:26: 328:33 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","rhs":{"kind":"Cast","op":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::b30b83d63051810b"},"kind":"Constant"},"ty":"ty::FnPtr::07cd89921cc84271","type":{"kind":"Pointer(ReifyFnPointer)"}}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:42: 347:59 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::FnPtr::bd6bee7b1f95b7bf"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:57: 347:58 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::FnPtr::07cd89921cc84271"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::FnPtr::07cd89921cc84271"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:57: 347:58 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::FnPtr::07cd89921cc84271"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::FnPtr::07cd89921cc84271"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::FnPtr::bd6bee7b1f95b7bf"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::788a983faed72be6"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:42: 347:59 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35"}},"blockid":"bb0"},{"block":{"data":[{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:58: 347:59 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::FnPtr::07cd89921cc84271"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:68: 347:85 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::4e8e6a61a1ceb622"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:83: 347:84 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::bf4d6d337c623aee"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::bf4d6d337c623aee"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:83: 347:84 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::bf4d6d337c623aee"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::bf4d6d337c623aee"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::4e8e6a61a1ceb622"}},"bb2"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f532a620418c4246"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:68: 347:85 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35"}},"blockid":"bb1"},{"block":{"data":[{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:84: 347:85 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::bf4d6d337c623aee"}},{"kind":"Deinit","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:18: 347:87 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35"},{"kind":"Assign","lhs":{"data":[{"field":0,"kind":"Field","ty":"ty::Ref::4e8e6a61a1ceb622"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::613f1953a8669d14"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:18: 347:87 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::4e8e6a61a1ceb622"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[{"field":1,"kind":"Field","ty":"ty::FnPtr::bd6bee7b1f95b7bf"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::613f1953a8669d14"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:18: 347:87 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::FnPtr::bd6bee7b1f95b7bf"}},"kind":"Move"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:86: 347:87 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::4e8e6a61a1ceb622"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:86: 347:87 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::FnPtr::bd6bee7b1f95b7bf"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:328:33: 328:34 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::FnPtr::07cd89921cc84271"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:328:33: 328:34 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::bf4d6d337c623aee"}}],"terminator":{"kind":"Return","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:329:10: 329:10 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35"}},"blockid":"bb2"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::613f1953a8669d14"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::bf4d6d337c623aee"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::FnPtr::07cd89921cc84271"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::FnPtr::bd6bee7b1f95b7bf"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::FnPtr::07cd89921cc84271"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::4e8e6a61a1ceb622"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::bf4d6d337c623aee"}]},"name":"core/73237d41::fmt::{impl#3}::new_display::_inst47ac314b85a79c82[0]","return_ty":"ty::Adt::613f1953a8669d14","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::913e2ff5487f7787"}],"body":{"blocks":[{"block":{"data":[{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::bool"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:37","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::bool"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:24","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::usize"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:24","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::675b2a8049aad652"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::675b2a8049aad652"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:24","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::usize"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:24","rhs":{"kind":"Len","lv":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::675b2a8049aad652"}}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:23: 400:24","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::675b2a8049aad652"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:27: 400:37","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::usize"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:27: 400:37","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::913e2ff5487f7787"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:27: 400:37","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::usize"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:27: 400:37","rhs":{"kind":"Len","lv":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::913e2ff5487f7787"}}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:36: 400:37","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::bool"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:37","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::usize"}},"kind":"Move"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::usize"}},"kind":"Move"},"kind":"BinaryOp","op":{"kind":"Lt"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:36: 400:37","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::usize"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:36: 400:37","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::usize"}}],"terminator":{"discr":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::bool"}},"kind":"Move"},"discr_span":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:37","kind":"SwitchInt","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","switch_ty":"ty::bool","targets":["bb2","bb1"],"values":["0"]}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::bool"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"bool","size":1,"val":"1"},"ty":"ty::bool"},"kind":"Constant"}}}],"terminator":{"kind":"Goto","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","target":"bb3"}},"blockid":"bb1"},{"block":{"data":[{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:41: 400:70","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::bool"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:41: 400:53","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::usize"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:41: 400:53","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::675b2a8049aad652"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::675b2a8049aad652"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:41: 400:53","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::usize"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:41: 400:53","rhs":{"kind":"Len","lv":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::675b2a8049aad652"}}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:52: 400:53","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::675b2a8049aad652"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:56: 400:70","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::usize"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:56: 400:66","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::usize"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:56: 400:66","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::913e2ff5487f7787"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:56: 400:66","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::usize"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:56: 400:66","rhs":{"kind":"Len","lv":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::913e2ff5487f7787"}}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:65: 400:66","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::usize"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:56: 400:70","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::usize"}},"kind":"Move"},"R":{"data":{"rendered":{"kind":"usize","size":8,"val":"1"},"ty":"ty::usize"},"kind":"Constant"},"kind":"BinaryOp","op":{"kind":"Add"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:69: 400:70","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::usize"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::bool"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:41: 400:70","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::usize"}},"kind":"Move"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::usize"}},"kind":"Move"},"kind":"BinaryOp","op":{"kind":"Gt"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:69: 400:70","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::usize"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:69: 400:70","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::usize"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::bool"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::bool"}},"kind":"Move"}}}],"terminator":{"kind":"Goto","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","target":"bb3"}},"blockid":"bb2"},{"block":{"data":[{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:69: 400:70","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::bool"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:69: 400:70","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::bool"}}],"terminator":{"discr":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::bool"}},"kind":"Move"},"discr_span":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","kind":"SwitchInt","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","switch_ty":"ty::bool","targets":["bb6","bb4"],"values":["0"]}},"blockid":"bb3"},{"block":{"data":[{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:9: 57:73 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","slvar":{"is_zst":true,"mut":{"kind":"Not"},"name":"_15","ty":"ty::Never::7199a9b06188843c"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_16","ty":"ty::Adt::ba5184b53bc36a4d"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:20: 401:34","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::675b2a8049aad652"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:20: 401:34","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::c2a5dcbb98af2a61"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:20: 401:34","slvar":{"is_zst":false,"mut":{"kind":"Not"},"name":"_19","ty":"ty::Ref::c2a5dcbb98af2a61"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_27","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:20: 401:34","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"mir_ghost/150ed4465f8cb026::{{alloc}}[3]","kind":"static_ref"},"ty":"ty::Ref::c2a5dcbb98af2a61"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_19","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:20: 401:34","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_27","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:20: 401:34","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_19","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::675b2a8049aad652"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:20: 401:34","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Move"},"ty":"ty::Ref::675b2a8049aad652","type":{"kind":"Pointer(Unsize)"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:33: 401:34","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::c2a5dcbb98af2a61"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::d0bd7bf253977b90"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","slvar":{"is_zst":false,"mut":{"kind":"Not"},"name":"_22","ty":"ty::Ref::d0bd7bf253977b90"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_26","ty":"ty::Ref::d0bd7bf253977b90"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"mir_ghost/150ed4465f8cb026::{{alloc}}[2]","kind":"static_ref"},"ty":"ty::Ref::d0bd7bf253977b90"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_22","ty":"ty::Ref::d0bd7bf253977b90"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_26","ty":"ty::Ref::d0bd7bf253977b90"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::d0bd7bf253977b90"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_22","ty":"ty::Ref::d0bd7bf253977b90"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::913e2ff5487f7787"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::d0bd7bf253977b90"}},"kind":"Move"},"ty":"ty::Ref::913e2ff5487f7787","type":{"kind":"Pointer(Unsize)"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:71: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::d0bd7bf253977b90"}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Move"},{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_16","ty":"ty::Adt::ba5184b53bc36a4d"}},"bb5"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::76afb566734aff77"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35"}},"blockid":"bb4"},{"block":{"data":[{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:71: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:71: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::675b2a8049aad652"}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_16","ty":"ty::Adt::ba5184b53bc36a4d"}},"kind":"Move"}],"cleanup":null,"destination":null,"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::906e67453a1bbab9"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:9: 57:73 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35"}},"blockid":"bb5"},{"block":{"data":[{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:402:9: 402:10","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::bool"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:21: 403:27","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_23","ty":"ty::Ref::675b2a8049aad652"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_23","ty":"ty::Ref::675b2a8049aad652"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:21: 403:27","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Copy"}}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:34: 403:38","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_24","ty":"ty::Adt::45883e75bd5c5ca5"}},{"kind":"Deinit","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:34: 403:38"},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_24","ty":"ty::Adt::45883e75bd5c5ca5"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:34: 403:38","variant_index":0},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:40: 403:44","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_25","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_25","ty":"ty::Ref::913e2ff5487f7787"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:40: 403:44","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Copy"}}},{"kind":"Deinit","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:9: 403:46"},{"kind":"Assign","lhs":{"data":[{"field":0,"kind":"Field","ty":"ty::Ref::675b2a8049aad652"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::ba5184b53bc36a4d"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:9: 403:46","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_23","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[{"field":1,"kind":"Field","ty":"ty::Adt::45883e75bd5c5ca5"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::ba5184b53bc36a4d"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:9: 403:46","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_24","ty":"ty::Adt::45883e75bd5c5ca5"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[{"field":2,"kind":"Field","ty":"ty::Ref::913e2ff5487f7787"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::ba5184b53bc36a4d"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:9: 403:46","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_25","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Move"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:45: 403:46","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_25","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:45: 403:46","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_24","ty":"ty::Adt::45883e75bd5c5ca5"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:45: 403:46","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_23","ty":"ty::Ref::675b2a8049aad652"}}],"terminator":{"kind":"Return","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:404:6: 404:6"}},"blockid":"bb6"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::ba5184b53bc36a4d"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::913e2ff5487f7787"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::913e2ff5487f7787"},{"is_zst":true,"mut":{"kind":"Not"},"name":"_15","ty":"ty::Never::7199a9b06188843c"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_16","ty":"ty::Adt::ba5184b53bc36a4d"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_19","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::913e2ff5487f7787"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_22","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_23","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_24","ty":"ty::Adt::45883e75bd5c5ca5"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_25","ty":"ty::Ref::913e2ff5487f7787"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_26","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_27","ty":"ty::Ref::c2a5dcbb98af2a61"}]},"name":"core/73237d41::fmt::{impl#4}::new_v1::_instbd21306cbe4f0b9b[0]","return_ty":"ty::Adt::ba5184b53bc36a4d","spread_arg":null}],"adts":[{"kind":{"kind":"Struct"},"name":"core/73237d41::fmt::Arguments::_adtbd21306cbe4f0b9b[0]","orig_def_id":"core/73237d41::fmt::Arguments","orig_substs":["nonty::Lifetime"],"repr_transparent":false,"size":48,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"core/73237d41::fmt::Arguments::pieces","ty":"ty::Ref::675b2a8049aad652"},{"name":"core/73237d41::fmt::Arguments::fmt","ty":"ty::Adt::45883e75bd5c5ca5"},{"name":"core/73237d41::fmt::Arguments::args","ty":"ty::Ref::913e2ff5487f7787"}],"inhabited":true,"name":"core/73237d41::fmt::Arguments"}]},{"kind":{"kind":"Struct"},"name":"core/73237d41::fmt::ArgumentV1::_adtbd21306cbe4f0b9b[0]","orig_def_id":"core/73237d41::fmt::ArgumentV1","orig_substs":["nonty::Lifetime"],"repr_transparent":false,"size":16,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"core/73237d41::fmt::ArgumentV1::value","ty":"ty::Ref::4e8e6a61a1ceb622"},{"name":"core/73237d41::fmt::ArgumentV1::formatter","ty":"ty::FnPtr::bd6bee7b1f95b7bf"}],"inhabited":true,"name":"core/73237d41::fmt::ArgumentV1"}]},{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"core/73237d41::option::Option::_adta9d03177c2d4a99f[0]","orig_def_id":"core/73237d41::option::Option","orig_substs":["ty::Ref::5f3877d5405402c5"],"repr_transparent":false,"size":16,"variants":[{"ctor_kind":{"kind":"Const"},"discr":{"index":0,"kind":"Relative"},"discr_value":"0","fields":[],"inhabited":true,"name":"core/73237d41::option::Option::None"},{"ctor_kind":{"kind":"Fn"},"discr":{"index":1,"kind":"Relative"},"discr_value":"1","fields":[{"name":"core/73237d41::option::Option::Some::0","ty":"ty::Ref::5f3877d5405402c5"}],"inhabited":true,"name":"core/73237d41::option::Option::Some"}]},{"kind":{"kind":"Struct"},"name":"core/73237d41::fmt::Error::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::Error","orig_substs":[],"repr_transparent":false,"size":0,"variants":[{"ctor_kind":{"kind":"Const"},"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[],"inhabited":true,"name":"core/73237d41::fmt::Error"}]},{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"core/73237d41::result::Result::_adt0f6d5765b4e92fb6[0]","orig_def_id":"core/73237d41::result::Result","orig_substs":["ty::Tuple::e93222e871854c41","ty::Adt::8d47b311e48cbf8f"],"repr_transparent":false,"size":1,"variants":[{"ctor_kind":{"kind":"Fn"},"discr":{"index":0,"kind":"Relative"},"discr_value":"0","fields":[{"name":"core/73237d41::result::Result::Ok::0","ty":"ty::Tuple::e93222e871854c41"}],"inhabited":true,"name":"core/73237d41::result::Result::Ok"},{"ctor_kind":{"kind":"Fn"},"discr":{"index":1,"kind":"Relative"},"discr_value":"1","fields":[{"name":"core/73237d41::result::Result::Err::0","ty":"ty::Adt::8d47b311e48cbf8f"}],"inhabited":true,"name":"core/73237d41::result::Result::Err"}]},{"kind":{"kind":"Struct"},"name":"core/73237d41::fmt::rt::v1::Argument::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::Argument","orig_substs":[],"repr_transparent":false,"size":56,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"core/73237d41::fmt::rt::v1::Argument::position","ty":"ty::usize"},{"name":"core/73237d41::fmt::rt::v1::Argument::format","ty":"ty::Adt::ed8948c5d0b3a39f"}],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Argument"}]},{"kind":{"kind":"Struct"},"name":"core/73237d41::fmt::Formatter::_adtbd21306cbe4f0b9b[0]","orig_def_id":"core/73237d41::fmt::Formatter","orig_substs":["nonty::Lifetime"],"repr_transparent":false,"size":64,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"core/73237d41::fmt::Formatter::flags","ty":"ty::u32"},{"name":"core/73237d41::fmt::Formatter::fill","ty":"ty::char"},{"name":"core/73237d41::fmt::Formatter::align","ty":"ty::Adt::c4745d1cf6b33a46"},{"name":"core/73237d41::fmt::Formatter::width","ty":"ty::Adt::ba42a94c73933868"},{"name":"core/73237d41::fmt::Formatter::precision","ty":"ty::Adt::ba42a94c73933868"},{"name":"core/73237d41::fmt::Formatter::buf","ty":"ty::Ref::0cd866b4eb1c792b"}],"inhabited":true,"name":"core/73237d41::fmt::Formatter"}]},{"kind":{"kind":"Struct"},"name":"core/73237d41::fmt::rt::v1::FormatSpec::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::FormatSpec","orig_substs":[],"repr_transparent":false,"size":48,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"core/73237d41::fmt::rt::v1::FormatSpec::fill","ty":"ty::char"},{"name":"core/73237d41::fmt::rt::v1::FormatSpec::align","ty":"ty::Adt::c4745d1cf6b33a46"},{"name":"core/73237d41::fmt::rt::v1::FormatSpec::flags","ty":"ty::u32"},{"name":"core/73237d41::fmt::rt::v1::FormatSpec::precision","ty":"ty::Adt::389b970f3565f26b"},{"name":"core/73237d41::fmt::rt::v1::FormatSpec::width","ty":"ty::Adt::389b970f3565f26b"}],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::FormatSpec"}]},{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"core/73237d41::fmt::rt::v1::Alignment::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::Alignment","orig_substs":[],"repr_transparent":false,"size":1,"variants":[{"ctor_kind":{"kind":"Const"},"discr":{"index":0,"kind":"Relative"},"discr_value":"0","fields":[],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Alignment::Left"},{"ctor_kind":{"kind":"Const"},"discr":{"index":1,"kind":"Relative"},"discr_value":"1","fields":[],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Alignment::Right"},{"ctor_kind":{"kind":"Const"},"discr":{"index":2,"kind":"Relative"},"discr_value":"2","fields":[],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Alignment::Center"},{"ctor_kind":{"kind":"Const"},"discr":{"index":3,"kind":"Relative"},"discr_value":"3","fields":[],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Alignment::Unknown"}]},{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"core/73237d41::option::Option::_adtaffa7a8b1157c078[0]","orig_def_id":"core/73237d41::option::Option","orig_substs":["ty::usize"],"repr_transparent":false,"size":16,"variants":[{"ctor_kind":{"kind":"Const"},"discr":{"index":0,"kind":"Relative"},"discr_value":"0","fields":[],"inhabited":true,"name":"core/73237d41::option::Option::None"},{"ctor_kind":{"kind":"Fn"},"discr":{"index":1,"kind":"Relative"},"discr_value":"1","fields":[{"name":"core/73237d41::option::Option::Some::0","ty":"ty::usize"}],"inhabited":true,"name":"core/73237d41::option::Option::Some"}]},{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"core/73237d41::fmt::rt::v1::Count::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::Count","orig_substs":[],"repr_transparent":false,"size":16,"variants":[{"ctor_kind":{"kind":"Fn"},"discr":{"index":0,"kind":"Relative"},"discr_value":"0","fields":[{"name":"core/73237d41::fmt::rt::v1::Count::Is::0","ty":"ty::usize"}],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Count::Is"},{"ctor_kind":{"kind":"Fn"},"discr":{"index":1,"kind":"Relative"},"discr_value":"1","fields":[{"name":"core/73237d41::fmt::rt::v1::Count::Param::0","ty":"ty::usize"}],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Count::Param"},{"ctor_kind":{"kind":"Const"},"discr":{"index":2,"kind":"Relative"},"discr_value":"2","fields":[],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Count::Implied"}]}],"statics":[{"kind":"constant","mutable":false,"name":"mir_ghost/150ed4465f8cb026::{{alloc}}[0]","rendered":{"element_ty":"ty::Ref::fb1cfdc5725cd03b","elements":[{"kind":"str","val":[110,111,116,32,105,109,112,108,101,109,101,110,116,101,100,58,32]}],"kind":"array"},"ty":"ty::Array::e5bd840a2dafa04a"},{"kind":"constant","mutable":false,"name":"mir_ghost/150ed4465f8cb026::{{alloc}}[1]","rendered":{"element_ty":"ty::Ref::fb1cfdc5725cd03b","elements":[{"kind":"str","val":[84,104,105,115,32,115,104,111,117,108,100,32,98,101,32,111,118,101,114,114,105,100,100,101,110]}],"kind":"array"},"ty":"ty::Array::e5bd840a2dafa04a"},{"kind":"constant","mutable":false,"name":"mir_ghost/150ed4465f8cb026::{{alloc}}[2]","rendered":{"element_ty":"ty::Adt::613f1953a8669d14","elements":[],"kind":"array"},"ty":"ty::Array::0e1a52ee2b2d3e97"},{"kind":"constant","mutable":false,"name":"mir_ghost/150ed4465f8cb026::{{alloc}}[3]","rendered":{"element_ty":"ty::Ref::fb1cfdc5725cd03b","elements":[{"kind":"str","val":[105,110,118,97,108,105,100,32,97,114,103,115]}],"kind":"array"},"ty":"ty::Array::e5bd840a2dafa04a"}],"vtables":[],"traits":[{"items":[{"item_id":"core/73237d41::fmt::Write::write_str","kind":"Method","signature":{"abi":{"kind":"Rust"},"inputs":["ty::Ref::0cd866b4eb1c792b","ty::Ref::fb1cfdc5725cd03b"],"output":"ty::Adt::30ed5848b4f625b6"}},{"item_id":"core/73237d41::fmt::Write::write_char","kind":"Method","signature":{"abi":{"kind":"Rust"},"inputs":["ty::Ref::0cd866b4eb1c792b","ty::char"],"output":"ty::Adt::30ed5848b4f625b6"}},{"item_id":"core/73237d41::fmt::Write::write_fmt","kind":"Method","signature":{"abi":{"kind":"Rust"},"inputs":["ty::Ref::0cd866b4eb1c792b","ty::Adt::ba5184b53bc36a4d"],"output":"ty::Adt::30ed5848b4f625b6"}}],"name":"core/73237d41::fmt::Write::_trait3e5b0354795cc029[0]"}],"intrinsics":[{"inst":{"def_id":"mir_ghost/150ed446::example","kind":"Item","substs":[]},"name":"mir_ghost/150ed446::example"},{"inst":{"def_id":"mir_ghost/150ed446::next","kind":"Item","substs":[]},"name":"mir_ghost/150ed446::next"},{"inst":{"def_id":"core/73237d41::fmt::{impl#3}::new_display","kind":"Item","substs":["nonty::Lifetime","ty::Adt::ba5184b53bc36a4d"]},"name":"core/73237d41::fmt::{impl#3}::new_display::_inst47ac314b85a79c82[0]"},{"inst":{"def_id":"core/73237d41::fmt::{impl#4}::new_v1","kind":"Item","substs":["nonty::Lifetime"]},"name":"core/73237d41::fmt::{impl#4}::new_v1::_instbd21306cbe4f0b9b[0]"},{"inst":{"def_id":"core/73237d41::panicking::panic_fmt","kind":"Item","substs":[]},"name":"core/73237d41::panicking::panic_fmt"},{"inst":{"def_id":"core/73237d41::intrinsics::{extern#0}::transmute","kind":"Intrinsic","substs":["ty::Ref::bf4d6d337c623aee","ty::Ref::4e8e6a61a1ceb622"]},"name":"core/73237d41::intrinsics::{extern#0}::transmute::_inst79e1dbb43599bccf[0]"},{"inst":{"def_id":"core/73237d41::intrinsics::{extern#0}::transmute","kind":"Intrinsic","substs":["ty::FnPtr::07cd89921cc84271","ty::FnPtr::bd6bee7b1f95b7bf"]},"name":"core/73237d41::intrinsics::{extern#0}::transmute::_inst82602b44b15ef1cb[0]"},{"inst":{"def_id":"core/73237d41::fmt::{impl#7}::fmt","kind":"Item","substs":["nonty::Lifetime"]},"name":"core/73237d41::fmt::{impl#7}::fmt::_instbd21306cbe4f0b9b[0]"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::FnDef::ae5488df1dc4e585","ty":{"defid":"mir_ghost/150ed446::next","kind":"FnDef"}},{"name":"ty::Never::7199a9b06188843c","ty":{"kind":"Never"}},{"name":"ty::Adt::ba5184b53bc36a4d","ty":{"kind":"Adt","name":"core/73237d41::fmt::Arguments::_adtbd21306cbe4f0b9b[0]","orig_def_id":"core/73237d41::fmt::Arguments","substs":["nonty::Lifetime"]}},{"name":"ty::str","ty":{"kind":"Str"}},{"name":"ty::Ref::fb1cfdc5725cd03b","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::str"}},{"name":"ty::Slice::563a94fdd2fd2b33","ty":{"kind":"Slice","ty":"ty::Ref::fb1cfdc5725cd03b"}},{"name":"ty::Ref::675b2a8049aad652","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Slice::563a94fdd2fd2b33"}},{"name":"ty::usize","ty":{"kind":"Uint","uintkind":{"kind":"Usize"}}},{"name":"ty::Array::e5bd840a2dafa04a","ty":{"kind":"Array","size":{"rendered":{"kind":"usize","size":8,"val":"1"},"ty":"ty::usize"},"ty":"ty::Ref::fb1cfdc5725cd03b"}},{"name":"ty::Ref::c2a5dcbb98af2a61","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Array::e5bd840a2dafa04a"}},{"name":"ty::Adt::613f1953a8669d14","ty":{"kind":"Adt","name":"core/73237d41::fmt::ArgumentV1::_adtbd21306cbe4f0b9b[0]","orig_def_id":"core/73237d41::fmt::ArgumentV1","substs":["nonty::Lifetime"]}},{"name":"ty::Slice::818a2c6d5f962f99","ty":{"kind":"Slice","ty":"ty::Adt::613f1953a8669d14"}},{"name":"ty::Ref::913e2ff5487f7787","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Slice::818a2c6d5f962f99"}},{"name":"ty::Array::6167cd8fdeb01e06","ty":{"kind":"Array","size":{"rendered":{"kind":"usize","size":8,"val":"1"},"ty":"ty::usize"},"ty":"ty::Adt::613f1953a8669d14"}},{"name":"ty::Ref::41f3f8f95d02c3e9","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Array::6167cd8fdeb01e06"}},{"name":"ty::Ref::bf4d6d337c623aee","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Adt::ba5184b53bc36a4d"}},{"name":"ty::Array::0e1a52ee2b2d3e97","ty":{"kind":"Array","size":{"rendered":{"kind":"usize","size":8,"val":"0"},"ty":"ty::usize"},"ty":"ty::Adt::613f1953a8669d14"}},{"name":"ty::Ref::d0bd7bf253977b90","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Array::0e1a52ee2b2d3e97"}},{"name":"ty::FnDef::76afb566734aff77","ty":{"defid":"core/73237d41::fmt::{impl#4}::new_v1::_instbd21306cbe4f0b9b[0]","kind":"FnDef"}},{"name":"ty::FnDef::72bf0f6662028c6a","ty":{"defid":"core/73237d41::fmt::{impl#3}::new_display::_inst47ac314b85a79c82[0]","kind":"FnDef"}},{"name":"ty::FnDef::906e67453a1bbab9","ty":{"defid":"core/73237d41::panicking::panic_fmt","kind":"FnDef"}},{"name":"ty::Adt::afb4c9f4ce8cdadf","ty":{"kind":"Adt","name":"core/73237d41::fmt::rt::v1::Argument::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::Argument","substs":[]}},{"name":"ty::Slice::26b8a0a5e2b22aa9","ty":{"kind":"Slice","ty":"ty::Adt::afb4c9f4ce8cdadf"}},{"name":"ty::Ref::5f3877d5405402c5","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Slice::26b8a0a5e2b22aa9"}},{"name":"ty::Adt::45883e75bd5c5ca5","ty":{"kind":"Adt","name":"core/73237d41::option::Option::_adta9d03177c2d4a99f[0]","orig_def_id":"core/73237d41::option::Option","substs":["ty::Ref::5f3877d5405402c5"]}},{"name":"ty::Foreign::66d9923797cfc204","ty":{"kind":"Foreign"}},{"name":"ty::Ref::4e8e6a61a1ceb622","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Foreign::66d9923797cfc204"}},{"name":"ty::Adt::ad5a554022507816","ty":{"kind":"Adt","name":"core/73237d41::fmt::Formatter::_adtbd21306cbe4f0b9b[0]","orig_def_id":"core/73237d41::fmt::Formatter","substs":["nonty::Lifetime"]}},{"name":"ty::Ref::7984c7d8fa40d865","ty":{"kind":"Ref","mutability":{"kind":"Mut"},"ty":"ty::Adt::ad5a554022507816"}},{"name":"ty::Tuple::e93222e871854c41","ty":{"kind":"Tuple","tys":[]}},{"name":"ty::Adt::8d47b311e48cbf8f","ty":{"kind":"Adt","name":"core/73237d41::fmt::Error::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::Error","substs":[]}},{"name":"ty::Adt::30ed5848b4f625b6","ty":{"kind":"Adt","name":"core/73237d41::result::Result::_adt0f6d5765b4e92fb6[0]","orig_def_id":"core/73237d41::result::Result","substs":["ty::Tuple::e93222e871854c41","ty::Adt::8d47b311e48cbf8f"]}},{"name":"ty::FnPtr::bd6bee7b1f95b7bf","ty":{"kind":"FnPtr","signature":{"abi":{"kind":"Rust"},"inputs":["ty::Ref::4e8e6a61a1ceb622","ty::Ref::7984c7d8fa40d865"],"output":"ty::Adt::30ed5848b4f625b6"}}},{"name":"ty::FnPtr::07cd89921cc84271","ty":{"kind":"FnPtr","signature":{"abi":{"kind":"Rust"},"inputs":["ty::Ref::bf4d6d337c623aee","ty::Ref::7984c7d8fa40d865"],"output":"ty::Adt::30ed5848b4f625b6"}}},{"name":"ty::FnDef::b30b83d63051810b","ty":{"defid":"core/73237d41::fmt::{impl#7}::fmt::_instbd21306cbe4f0b9b[0]","kind":"FnDef"}},{"name":"ty::FnDef::788a983faed72be6","ty":{"defid":"core/73237d41::intrinsics::{extern#0}::transmute::_inst82602b44b15ef1cb[0]","kind":"FnDef"}},{"name":"ty::FnDef::f532a620418c4246","ty":{"defid":"core/73237d41::intrinsics::{extern#0}::transmute::_inst79e1dbb43599bccf[0]","kind":"FnDef"}},{"name":"ty::bool","ty":{"kind":"Bool"}},{"name":"ty::isize","ty":{"intkind":{"kind":"Isize"},"kind":"Int"}},{"name":"ty::Adt::ed8948c5d0b3a39f","ty":{"kind":"Adt","name":"core/73237d41::fmt::rt::v1::FormatSpec::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::FormatSpec","substs":[]}},{"name":"ty::char","ty":{"kind":"Char"}},{"name":"ty::Adt::c4745d1cf6b33a46","ty":{"kind":"Adt","name":"core/73237d41::fmt::rt::v1::Alignment::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::Alignment","substs":[]}},{"name":"ty::Adt::ba42a94c73933868","ty":{"kind":"Adt","name":"core/73237d41::option::Option::_adtaffa7a8b1157c078[0]","orig_def_id":"core/73237d41::option::Option","substs":["ty::usize"]}},{"name":"ty::Dynamic::08a22e65af9638be","ty":{"kind":"Dynamic","predicates":[{"kind":"Trait","substs":[],"trait":"core/73237d41::fmt::Write"}],"trait_id":"core/73237d41::fmt::Write::_trait3e5b0354795cc029[0]"}},{"name":"ty::Ref::0cd866b4eb1c792b","ty":{"kind":"Ref","mutability":{"kind":"Mut"},"ty":"ty::Dynamic::08a22e65af9638be"}},{"name":"ty::Adt::389b970f3565f26b","ty":{"kind":"Adt","name":"core/73237d41::fmt::rt::v1::Count::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::Count","substs":[]}}],"roots":["mir_ghost/150ed446::next","mir_ghost/150ed446::example"]} \ No newline at end of file diff --git a/saw-remote-api/python/tests/saw/test-files/mir_ghost.rs b/saw-remote-api/python/tests/saw/test-files/mir_ghost.rs new file mode 100644 index 0000000000..fafa13669c --- /dev/null +++ b/saw-remote-api/python/tests/saw/test-files/mir_ghost.rs @@ -0,0 +1,9 @@ +pub fn next() -> u32 { + unimplemented!("This should be overridden") +} + +pub fn example() -> u32 { + next(); + next(); + next() +} diff --git a/saw-remote-api/python/tests/saw/test_mir_ghost.py b/saw-remote-api/python/tests/saw/test_mir_ghost.py new file mode 100644 index 0000000000..3d4e388cad --- /dev/null +++ b/saw-remote-api/python/tests/saw/test_mir_ghost.py @@ -0,0 +1,53 @@ +import unittest +from pathlib import Path + +from saw_client import * +from saw_client.crucible import cry_f +from saw_client.mir import Contract, GhostVariable, u32 + + +class NextContract(Contract): + def __init__(self, counter: GhostVariable) -> None: + super().__init__() + self.counter = counter + + def specification(self) -> None: + n = self.fresh_var(u32, 'n') + self.ghost_value(self.counter, n) + + self.execute_func() + + self.ghost_value(self.counter, cry_f('{n} + 1')) + self.returns(n) + + +class ExampleContract(Contract): + def __init__(self, counter: GhostVariable) -> None: + super().__init__() + self.counter = counter + + def specification(self) -> None: + n = self.fresh_var(u32, 'n') + self.precondition_f('{n} < 2') + self.ghost_value(self.counter, n) + + self.execute_func() + self.ghost_value(self.counter, cry_f('{n} + 3')) + self.returns_f('{n} + 2') + + +class MIRGhostTest(unittest.TestCase): + def test_mir_ghost(self): + connect(reset_server=True) + if __name__ == "__main__": view(LogResults()) + json_name = str(Path('tests', 'saw', 'test-files', 'mir_ghost.linked-mir.json')) + mod = mir_load_module(json_name) + + counter = create_ghost_variable('ctr'); + next_ov = mir_assume(mod, 'mir_ghost::next', NextContract(counter)) + example_result = mir_verify(mod, 'mir_ghost::example', ExampleContract(counter), lemmas=[next_ov]) + self.assertIs(example_result.is_success(), True) + + +if __name__ == "__main__": + unittest.main() diff --git a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs index c601974f4a..8262e46c81 100644 --- a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs @@ -26,7 +26,7 @@ import qualified Data.Map as Map import qualified Cryptol.Parser.AST as P import Cryptol.Utils.Ident (mkIdent) import qualified Lang.Crucible.JVM as CJ -import SAWScript.Crucible.Common.MethodSpec as MS (SetupValue(..)) +import qualified SAWScript.Crucible.Common.MethodSpec as MS import SAWScript.Crucible.JVM.Builtins ( jvm_alloc_array, jvm_alloc_object, @@ -35,6 +35,7 @@ import SAWScript.Crucible.JVM.Builtins jvm_static_field_is, jvm_execute_func, jvm_fresh_var, + jvm_ghost_value, jvm_postcond, jvm_precond, jvm_return ) @@ -56,10 +57,11 @@ import SAWServer import SAWServer.Data.Contract ( PointsTo(PointsTo), PointsToBitfield, + GhostValue(GhostValue), Allocated(Allocated), ContractVar(ContractVar), - Contract(preVars, preConds, preAllocated, prePointsTos, prePointsToBitfields, - argumentVals, postVars, postConds, postAllocated, postPointsTos, postPointsToBitfields, + Contract(preVars, preConds, preAllocated, preGhostValues, prePointsTos, prePointsToBitfields, + argumentVals, postVars, postConds, postAllocated, postGhostValues, postPointsTos, postPointsToBitfields, returnVal) ) import SAWServer.Data.SetupValue () import SAWServer.CryptolExpression (CryptolModuleException(..), getTypedTermOfCExp) @@ -82,28 +84,29 @@ instance Doc.DescribedMethod StartJVMSetupParams OK where ] resultFieldDescription = [] -newtype ServerSetupVal = Val (SetupValue CJ.JVM) +newtype ServerSetupVal = Val (MS.SetupValue CJ.JVM) compileJVMContract :: (FilePath -> IO ByteString) -> BuiltinContext -> + Map ServerName MS.GhostGlobal -> CryptolEnv -> Contract JavaType (P.Expr P.PName) -> JVMSetupM () -compileJVMContract fileReader bic cenv0 c = +compileJVMContract fileReader bic ghostEnv cenv0 c = do allocsPre <- mapM setupAlloc (preAllocated c) (envPre, cenvPre) <- setupState allocsPre (Map.empty, cenv0) (preVars c) mapM_ (\p -> getTypedTerm cenvPre p >>= jvm_precond) (preConds c) mapM_ (setupPointsTo (envPre, cenvPre)) (prePointsTos c) mapM_ setupPointsToBitfields (prePointsToBitfields c) - --mapM_ (setupGhostValue ghostEnv cenvPre) (preGhostValues c) + mapM_ (setupGhostValue ghostEnv cenvPre) (preGhostValues c) traverse (getSetupVal (envPre, cenvPre)) (argumentVals c) >>= jvm_execute_func allocsPost <- mapM setupAlloc (postAllocated c) (envPost, cenvPost) <- setupState (allocsPre ++ allocsPost) (envPre, cenvPre) (postVars c) mapM_ (\p -> getTypedTerm cenvPost p >>= jvm_postcond) (postConds c) mapM_ (setupPointsTo (envPost, cenvPost)) (postPointsTos c) mapM_ setupPointsToBitfields (postPointsToBitfields c) - --mapM_ (setupGhostValue ghostEnv cenvPost) (postGhostValues c) + mapM_ (setupGhostValue ghostEnv cenvPost) (postGhostValues c) case returnVal c of Just v -> getSetupVal (envPost, cenvPost) v >>= jvm_return Nothing -> return () @@ -149,7 +152,10 @@ compileJVMContract fileReader bic cenv0 c = setupPointsToBitfields _ = JVMSetupM $ fail "Points-to-bitfield not supported in JVM API." - --setupGhostValue _ _ _ = fail "Ghost values not supported yet in JVM API." + setupGhostValue genv cenv (GhostValue serverName e) = + do g <- resolve genv serverName + t <- getTypedTerm cenv e + jvm_ghost_value g t resolve :: Map ServerName a -> ServerName -> JVMSetupM a resolve env name = diff --git a/saw-remote-api/src/SAWServer/JVMVerify.hs b/saw-remote-api/src/SAWServer/JVMVerify.hs index f7c97654ed..293d424e79 100644 --- a/saw-remote-api/src/SAWServer/JVMVerify.hs +++ b/saw-remote-api/src/SAWServer/JVMVerify.hs @@ -9,6 +9,7 @@ module SAWServer.JVMVerify import Prelude hiding (mod) import Control.Lens +import qualified Data.Map as Map import SAWScript.Crucible.JVM.Builtins ( jvm_unsafe_assume_spec, jvm_verify ) @@ -26,6 +27,7 @@ import SAWServer pushTask, dropTask, setServerVal, + getGhosts, getJVMClass, getJVMMethodSpecIR ) import SAWServer.CryptolExpression (getCryptolExpr) @@ -51,7 +53,8 @@ jvmVerifyAssume mode (VerifyParams className fun lemmaNames checkSat contract sc let bic = view sawBIC state cenv = rwCryptol (view sawTopLevelRW state) fileReader <- Argo.getFileReader - setup <- compileJVMContract fileReader bic cenv <$> traverse getCryptolExpr contract + ghostEnv <- Map.fromList <$> getGhosts + setup <- compileJVMContract fileReader bic ghostEnv cenv <$> traverse getCryptolExpr contract res <- case mode of VerifyContract -> do lemmas <- mapM getJVMMethodSpecIR lemmaNames diff --git a/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs b/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs index a1ce2f07d3..b6cf3555df 100644 --- a/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs @@ -31,6 +31,7 @@ import SAWScript.Crucible.MIR.Builtins mir_fresh_expanded_value, mir_fresh_var, mir_execute_func, + mir_ghost_value, mir_load_module, mir_points_to, mir_postcond, @@ -58,10 +59,11 @@ import SAWServer.CryptolExpression (CryptolModuleException(..), getTypedTermOfCE import SAWServer.Data.Contract ( PointsTo(PointsTo), PointsToBitfield, + GhostValue(GhostValue), Allocated(Allocated), ContractVar(ContractVar), - Contract(preVars, preConds, preAllocated, prePointsTos, prePointsToBitfields, - argumentVals, postVars, postConds, postAllocated, postPointsTos, postPointsToBitfields, + Contract(preVars, preConds, preAllocated, preGhostValues, prePointsTos, prePointsToBitfields, + argumentVals, postVars, postConds, postAllocated, postGhostValues, postPointsTos, postPointsToBitfields, returnVal) ) import SAWServer.Data.MIRType (JSONMIRType, mirType) import SAWServer.Exceptions ( notAtTopLevel ) @@ -74,24 +76,25 @@ newtype ServerSetupVal = Val (MS.SetupValue MIR) compileMIRContract :: (FilePath -> IO ByteString) -> BuiltinContext -> + Map ServerName MS.GhostGlobal -> CryptolEnv -> SAWEnv -> Contract JSONMIRType (P.Expr P.PName) -> MIRSetupM () -compileMIRContract fileReader bic cenv0 sawenv c = +compileMIRContract fileReader bic ghostEnv cenv0 sawenv c = do allocsPre <- mapM setupAlloc (preAllocated c) (envPre, cenvPre) <- setupState allocsPre (Map.empty, cenv0) (preVars c) mapM_ (\p -> getTypedTerm cenvPre p >>= mir_precond) (preConds c) mapM_ (setupPointsTo (envPre, cenvPre)) (prePointsTos c) mapM_ setupPointsToBitfields (prePointsToBitfields c) - --mapM_ (setupGhostValue ghostEnv cenvPre) (preGhostValues c) + mapM_ (setupGhostValue ghostEnv cenvPre) (preGhostValues c) traverse (getSetupVal (envPre, cenvPre)) (argumentVals c) >>= mir_execute_func allocsPost <- mapM setupAlloc (postAllocated c) (envPost, cenvPost) <- setupState (allocsPre ++ allocsPost) (envPre, cenvPre) (postVars c) mapM_ (\p -> getTypedTerm cenvPost p >>= mir_postcond) (postConds c) mapM_ (setupPointsTo (envPost, cenvPost)) (postPointsTos c) mapM_ setupPointsToBitfields (postPointsToBitfields c) - --mapM_ (setupGhostValue ghostEnv cenvPost) (postGhostValues c) + mapM_ (setupGhostValue ghostEnv cenvPost) (postGhostValues c) case returnVal c of Just v -> getSetupVal (envPost, cenvPost) v >>= mir_return Nothing -> return () @@ -136,7 +139,10 @@ compileMIRContract fileReader bic cenv0 sawenv c = setupPointsToBitfields _ = MIRSetupM $ fail "Points-to-bitfield not supported in the MIR API." - --setupGhostValue _ _ _ = fail "Ghost values not supported yet in the MIR API." + setupGhostValue genv cenv (GhostValue serverName e) = + do g <- resolve genv serverName + t <- getTypedTerm cenv e + mir_ghost_value g t resolve :: Map ServerName a -> ServerName -> MIRSetupM a resolve env name = diff --git a/saw-remote-api/src/SAWServer/MIRVerify.hs b/saw-remote-api/src/SAWServer/MIRVerify.hs index 5106396341..f3bf31e447 100644 --- a/saw-remote-api/src/SAWServer/MIRVerify.hs +++ b/saw-remote-api/src/SAWServer/MIRVerify.hs @@ -9,6 +9,7 @@ module SAWServer.MIRVerify import Prelude hiding (mod) import Control.Lens +import qualified Data.Map as Map import SAWScript.Crucible.MIR.Builtins ( mir_unsafe_assume_spec, mir_verify ) @@ -26,6 +27,7 @@ import SAWServer pushTask, dropTask, setServerVal, + getGhosts, getMIRModule, getMIRMethodSpecIR ) import SAWServer.CryptolExpression (getCryptolExpr) @@ -53,7 +55,8 @@ mirVerifyAssume mode (VerifyParams modName fun lemmaNames checkSat contract scri cenv = rwCryptol (view sawTopLevelRW state) sawenv = view sawEnv state fileReader <- Argo.getFileReader - setup <- compileMIRContract fileReader bic cenv sawenv <$> + ghostEnv <- Map.fromList <$> getGhosts + setup <- compileMIRContract fileReader bic ghostEnv cenv sawenv <$> traverse getCryptolExpr contract res <- case mode of VerifyContract -> do diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index bdc896c2c4..dc41073628 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -27,6 +27,7 @@ import Data.Functor import Control.Applicative import Data.Monoid #endif +import Control.Lens (view) import Control.Monad (foldM, forM, unless, when) import Control.Monad.Except (MonadError(..)) import Control.Monad.IO.Class (MonadIO(..)) @@ -135,7 +136,8 @@ import SAWScript.Value (ProofScript, printOutLnTop, AIGNetwork) import SAWScript.SolverCache import SAWScript.SolverVersions -import SAWScript.Crucible.Common.MethodSpec (ppTypedTermType) +import qualified SAWScript.Crucible.Common.MethodSpec as MS +import SAWScript.Crucible.Common.Setup.Type (addCondition, croTags) import SAWScript.Prover.Util(checkBooleanSchema) import SAWScript.Prover.SolverStats import qualified SAWScript.Prover.SBV as Prover @@ -161,7 +163,7 @@ definePrim name (TypedTerm (TypedTermSchema schema) rhs) = definePrim _name (TypedTerm tp _) = fail $ unlines [ "Expected term with Cryptol schema type, but got" - , show (ppTypedTermType tp) + , show (MS.ppTypedTermType tp) ] sbvUninterpreted :: String -> Term -> TopLevel Uninterp @@ -699,7 +701,7 @@ term_type tt = TypedTermSchema sch -> pure sch tp -> fail $ unlines [ "Term does not have a Cryptol type" - , show (ppTypedTermType tp) + , show (MS.ppTypedTermType tp) ] goal_eval :: [String] -> ProofScript () @@ -2477,3 +2479,18 @@ declare_ghost_state name = do allocator <- getHandleAlloc global <- liftIO (freshGlobalVar allocator (Text.pack name) knownRepr) return (SV.VGhostVar global) + +ghost_value :: + MS.GhostGlobal -> + TypedTerm -> + SV.CrucibleSetup ext () +ghost_value ghost val = + do loc <- SV.getW4Position "ghost_value" + tags <- view croTags + let md = MS.ConditionMetadata + { MS.conditionLoc = loc + , MS.conditionTags = tags + , MS.conditionType = "ghost value" + , MS.conditionContext = "" + } + addCondition (MS.SetupCond_Ghost md ghost val) diff --git a/src/SAWScript/Crucible/Common/MethodSpec.hs b/src/SAWScript/Crucible/Common/MethodSpec.hs index e8ce39d657..acba975084 100644 --- a/src/SAWScript/Crucible/Common/MethodSpec.hs +++ b/src/SAWScript/Crucible/Common/MethodSpec.hs @@ -13,8 +13,10 @@ Grow\", and is prevalent across the Crucible codebase. {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} @@ -22,6 +24,7 @@ Grow\", and is prevalent across the Crucible codebase. {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeFamilyDependencies #-} {-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -Wno-orphans #-} module SAWScript.Crucible.Common.MethodSpec ( AllocIndex(..) @@ -62,7 +65,6 @@ module SAWScript.Crucible.Common.MethodSpec , setupToTypedTerm , setupToTerm - , XGhostState , GhostValue , GhostType , GhostGlobal @@ -118,6 +120,7 @@ import Data.Set (Set) import Data.Time.Clock import Data.Void (absurd) +import Control.Monad (when) import Control.Monad.Trans.Maybe import Control.Monad.Trans (lift) import Control.Lens @@ -132,13 +135,17 @@ import Lang.Crucible.JVM (JVM) import qualified Lang.Crucible.Types as Crucible (IntrinsicType, EmptyCtx) import qualified Lang.Crucible.CFG.Common as Crucible (GlobalVar) +import qualified Lang.Crucible.Simulator.Intrinsics as Crucible import Mir.Intrinsics (MIR) +import qualified Cryptol.TypeCheck.Type as Cryptol (Schema) import qualified Cryptol.Utils.PP as Cryptol import Verifier.SAW.TypedTerm as SAWVerifier import Verifier.SAW.SharedTerm as SAWVerifier +import Verifier.SAW.Simulator.What4.ReturnTrip as SAWVerifier +import SAWScript.Crucible.Common (Sym, sawCoreState) import SAWScript.Crucible.Common.Setup.Value import SAWScript.Crucible.LLVM.Setup.Value (LLVM) import SAWScript.Crucible.JVM.Setup.Value () @@ -344,21 +351,33 @@ type GhostValue = "GhostValue" type GhostType = Crucible.IntrinsicType GhostValue Crucible.EmptyCtx type GhostGlobal = Crucible.GlobalVar GhostType +instance Crucible.IntrinsicClass Sym GhostValue where + type Intrinsic Sym GhostValue ctx = (Cryptol.Schema, Term) + muxIntrinsic sym _ _namerep _ctx prd (thnSch,thn) (elsSch,els) = + do when (thnSch /= elsSch) $ fail $ unlines $ + [ "Attempted to mux ghost variables of different types:" + , show (Cryptol.pp thnSch) + , show (Cryptol.pp elsSch) + ] + st <- sawCoreState sym + let sc = saw_ctx st + prd' <- toSC sym st prd + typ <- scTypeOf sc thn + res <- scIte sc typ prd' thn els + return (thnSch, res) + -------------------------------------------------------------------------------- -- *** StateSpec data SetupCondition ext where SetupCond_Equal :: ConditionMetadata -> SetupValue ext -> SetupValue ext -> SetupCondition ext SetupCond_Pred :: ConditionMetadata -> TypedTerm -> SetupCondition ext - SetupCond_Ghost :: XGhostState ext -> - ConditionMetadata -> + SetupCond_Ghost :: ConditionMetadata -> GhostGlobal -> TypedTerm -> SetupCondition ext -deriving instance ( SetupValueHas Show ext - , Show (XGhostState ext) - ) => Show (SetupCondition ext) +deriving instance SetupValueHas Show ext => Show (SetupCondition ext) -- | Verification state (either pre- or post-) specification data StateSpec ext = StateSpec diff --git a/src/SAWScript/Crucible/Common/Override.hs b/src/SAWScript/Crucible/Common/Override.hs index 48d31e1b66..fac57dcb20 100644 --- a/src/SAWScript/Crucible/Common/Override.hs +++ b/src/SAWScript/Crucible/Common/Override.hs @@ -65,11 +65,16 @@ module SAWScript.Crucible.Common.Override -- , assignmentToList , MetadataMap + -- + , learnGhost + , executeGhost + , instantiateExtMatchTerm + , matchTerm ) where import qualified Control.Exception as X import Control.Lens -import Control.Monad (foldM, unless) +import Control.Monad (foldM, unless, when) import Control.Monad.Trans.State hiding (get, put) import Control.Monad.State.Class (MonadState(..)) import Control.Monad.Error.Class (MonadError) @@ -82,6 +87,7 @@ import qualified Data.Map as Map import Data.Map (Map) import Data.Maybe (fromMaybe) import Data.Proxy (Proxy(..)) +import qualified Data.Set as Set import Data.Set (Set) import Data.Typeable (Typeable) import Data.Void @@ -92,10 +98,13 @@ import qualified Data.Parameterized.Context as Ctx import Data.Parameterized.Some (Some) import Data.Parameterized.TraversableFC (toListFC) +import Verifier.SAW.Prelude as SAWVerifier (scEq) import Verifier.SAW.SharedTerm as SAWVerifier import Verifier.SAW.TypedAST as SAWVerifier import Verifier.SAW.TypedTerm as SAWVerifier +import qualified Cryptol.Utils.PP as Cryptol (pp) + import qualified Lang.Crucible.Backend as Crucible import qualified Lang.Crucible.Backend.Online as Crucible import qualified Lang.Crucible.CFG.Core as Crucible (TypeRepr, GlobalVar) @@ -529,3 +538,102 @@ assignmentToList :: Ctx.Assignment (Crucible.RegEntry sym) ctx -> [Crucible.AnyValue sym] assignmentToList = toListFC (\(Crucible.RegEntry x y) -> Crucible.AnyValue x y) + +------------------------------------------------------------------------ + +learnGhost :: + SharedContext -> + MS.ConditionMetadata -> + PrePost -> + MS.GhostGlobal -> + TypedTerm -> + OverrideMatcher ext md () +learnGhost sc md prepost var (TypedTerm (TypedTermSchema schEx) tmEx) = + do (sch,tm) <- readGlobal var + when (sch /= schEx) $ fail $ unlines $ + [ "Ghost variable had the wrong type:" + , "- Expected: " ++ show (Cryptol.pp schEx) + , "- Actual: " ++ show (Cryptol.pp sch) + ] + instantiateExtMatchTerm sc md prepost tm tmEx +learnGhost _sc _md _prepost _var (TypedTerm tp _) + = fail $ unlines + [ "Ghost variable expected value has improper type" + , "expected Cryptol schema type, but got" + , show (MS.ppTypedTermType tp) + ] + +executeGhost :: + SharedContext -> + MS.ConditionMetadata -> + MS.GhostGlobal -> + TypedTerm -> + OverrideMatcher ext RW () +executeGhost sc _md var (TypedTerm (TypedTermSchema sch) tm) = + do s <- OM (use termSub) + tm' <- liftIO (scInstantiateExt sc s tm) + writeGlobal var (sch,tm') +executeGhost _sc _md _var (TypedTerm tp _) = + fail $ unlines + [ "executeGhost: improper value type" + , "expected Cryptol schema type, but got" + , show (MS.ppTypedTermType tp) + ] + +-- | NOTE: The two 'Term' arguments must have the same type. +instantiateExtMatchTerm :: + SharedContext {- ^ context for constructing SAW terms -} -> + MS.ConditionMetadata -> + PrePost -> + Term {- ^ exported concrete term -} -> + Term {- ^ expected specification term -} -> + OverrideMatcher ext md () +instantiateExtMatchTerm sc md prepost actual expected = do + sub <- OM (use termSub) + matchTerm sc md prepost actual =<< liftIO (scInstantiateExt sc sub expected) + +matchTerm :: + SharedContext {- ^ context for constructing SAW terms -} -> + MS.ConditionMetadata -> + PrePost -> + Term {- ^ exported concrete term -} -> + Term {- ^ expected specification term -} -> + OverrideMatcher ext md () + +matchTerm _ _ _ real expect | real == expect = return () +matchTerm sc md prepost real expect = + do let loc = MS.conditionLoc md + free <- OM (use osFree) + case unwrapTermF expect of + FTermF (ExtCns ec) + | Set.member (ecVarIndex ec) free -> + do assignTerm sc md prepost (ecVarIndex ec) real + + _ -> + do t <- liftIO $ scEq sc real expect + let msg = unlines $ + [ "Literal equality " ++ MS.stateCond prepost +-- , "Expected term: " ++ prettyTerm expect +-- , "Actual term: " ++ prettyTerm real + ] + addTermEq t md $ Crucible.SimError loc $ Crucible.AssertFailureSimError msg "" +-- where prettyTerm = show . ppTermDepth 20 + +assignTerm :: + SharedContext {- ^ context for constructing SAW terms -} -> + MS.ConditionMetadata -> + PrePost -> + VarIndex {- ^ external constant index -} -> + Term {- ^ value -} -> + OverrideMatcher ext md () + +assignTerm sc md prepost var val = + do mb <- OM (use (termSub . at var)) + case mb of + Nothing -> OM (termSub . at var ?= val) + Just old -> + matchTerm sc md prepost val old + +-- do t <- liftIO $ scEq sc old val +-- p <- liftIO $ resolveSAWPred cc t +-- addAssert p (Crucible.AssertFailureSimError ("literal equality " ++ MS.stateCond prepost)) diff --git a/src/SAWScript/Crucible/Common/Setup/Value.hs b/src/SAWScript/Crucible/Common/Setup/Value.hs index 505acce1c9..b9fa6ebcde 100644 --- a/src/SAWScript/Crucible/Common/Setup/Value.hs +++ b/src/SAWScript/Crucible/Common/Setup/Value.hs @@ -51,8 +51,6 @@ module SAWScript.Crucible.Common.Setup.Value , SetupValue(..) , SetupValueHas - , XGhostState - , ConditionMetadata(..) , MethodId @@ -185,15 +183,6 @@ deriving instance (SetupValueHas Show ext) => Show (SetupValue ext) -- deriving instance (SetupValueHas Eq ext) => Eq (SetupValue ext) -- deriving instance (SetupValueHas Ord ext) => Ord (SetupValue ext) --------------------------------------------------------------------------------- --- ** Ghost state - --- | This extension field controls whether ghost state is enabled for a --- particular language backend. At the moment, ghost state is only enabled for --- the LLVM backend, but we want to expand this to cover other language backends --- in the future. See . -type family XGhostState ext - -------------------------------------------------------------------------------- -- ** Pre- and post-conditions diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs index 77c5d99dd6..c4e9b3ae80 100644 --- a/src/SAWScript/Crucible/JVM/Builtins.hs +++ b/src/SAWScript/Crucible/JVM/Builtins.hs @@ -44,6 +44,7 @@ module SAWScript.Crucible.JVM.Builtins , jvm_alloc_object , jvm_alloc_array , jvm_setup_with_tag + , jvm_ghost_value ) where import Control.Lens @@ -70,7 +71,6 @@ import Data.Text (Text) import qualified Data.Text as Text import Data.Time.Clock (getCurrentTime, diffUTCTime) import qualified Data.Vector as V -import Data.Void (absurd) import Prettyprinter import System.IO @@ -112,6 +112,7 @@ import Verifier.SAW.TypedTerm import Verifier.SAW.Simulator.What4.ReturnTrip +import SAWScript.Builtins (ghost_value) import SAWScript.Exceptions import SAWScript.Panic import SAWScript.Proof @@ -415,7 +416,8 @@ verifyPrestate cc mspec globals0 = (env, globals1) <- runStateT (Map.traverseWithKey doAlloc preallocs) globals0' globals2 <- setupPrePointsTos mspec cc env (mspec ^. MS.csPreState . MS.csPointsTos) globals1 - cs <- setupPrestateConditions mspec cc env (mspec ^. MS.csPreState . MS.csConditions) + (globals3, cs) <- + setupPrestateConditions mspec cc env globals2 (mspec ^. MS.csPreState . MS.csConditions) args <- resolveArguments cc mspec env -- Check the type of the return setup value @@ -435,7 +437,7 @@ verifyPrestate cc mspec globals0 = ] (Nothing, _) -> return () - return (args, cs, env, globals2) + return (args, cs, env, globals3) -- | Check two Types for register compatibility. registerCompatible :: J.Type -> J.Type -> Bool @@ -540,32 +542,43 @@ setupPrePointsTos mspec cc env pts mem0 = foldM doPointsTo mem0 pts _ -> panic "setupPrePointsTo" ["invalid invariant", "jvm_modifies in pre-state"] --- | Collects boolean terms that should be assumed to be true. +-- | Sets up globals (ghost variable), and collects boolean terms +-- that should be assumed to be true. setupPrestateConditions :: MethodSpec -> JVMCrucibleContext -> Map AllocIndex JVMRefVal -> + Crucible.SymGlobalState Sym -> [SetupCondition] -> - IO [Crucible.LabeledPred Term AssumptionReason] + IO ( Crucible.SymGlobalState Sym, [Crucible.LabeledPred Term AssumptionReason] + ) setupPrestateConditions mspec cc env = aux [] where tyenv = MS.csAllocations mspec nameEnv = mspec ^. MS.csPreState . MS.csVarTypeNames - aux acc [] = return acc + aux acc globals [] = return (globals, acc) - aux acc (MS.SetupCond_Equal loc val1 val2 : xs) = + aux acc globals (MS.SetupCond_Equal loc val1 val2 : xs) = do val1' <- resolveSetupVal cc env tyenv nameEnv val1 val2' <- resolveSetupVal cc env tyenv nameEnv val2 t <- assertEqualVals cc val1' val2' let lp = Crucible.LabeledPred t (loc, "equality precondition") - aux (lp:acc) xs + aux (lp:acc) globals xs - aux acc (MS.SetupCond_Pred loc tm : xs) = + aux acc globals (MS.SetupCond_Pred loc tm : xs) = let lp = Crucible.LabeledPred (ttTerm tm) (loc, "precondition") in - aux (lp:acc) xs - - aux _ (MS.SetupCond_Ghost empty_ _ _ _ : _) = absurd empty_ + aux (lp:acc) globals xs + + aux acc globals (MS.SetupCond_Ghost _md var val : xs) = + case val of + TypedTerm (TypedTermSchema sch) tm -> + aux acc (Crucible.insertGlobal var (sch,tm) globals) xs + TypedTerm tp _ -> + fail $ unlines + [ "Setup term for global variable expected to have Cryptol schema type, but got" + , show (MS.ppTypedTermType tp) + ] -------------------------------------------------------------------------------- @@ -1421,6 +1434,13 @@ jvm_setup_with_tag :: jvm_setup_with_tag tag m = JVMSetupM (Setup.setupWithTag tag (runJVMSetupM m)) +jvm_ghost_value :: + MS.GhostGlobal -> + TypedTerm -> + JVMSetupM () +jvm_ghost_value ghost val = JVMSetupM $ + ghost_value ghost val + -------------------------------------------------------------------------------- -- | Sort a list of things and group them into equivalence classes. diff --git a/src/SAWScript/Crucible/JVM/Override.hs b/src/SAWScript/Crucible/JVM/Override.hs index 258249647c..680686ac8c 100644 --- a/src/SAWScript/Crucible/JVM/Override.hs +++ b/src/SAWScript/Crucible/JVM/Override.hs @@ -92,8 +92,6 @@ import Data.Parameterized.Some (Some(Some)) -- saw-core import Verifier.SAW.SharedTerm -import Verifier.SAW.Prelude (scEq) -import Verifier.SAW.TypedAST import Verifier.SAW.TypedTerm import Verifier.SAW.Simulator.What4.ReturnTrip (toSC) @@ -326,13 +324,13 @@ methodSpecHandler_prestate opts sc cc args cs = -- which involves writing values into memory, computing the return value, -- and computing postcondition predicates. methodSpecHandler_poststate :: - forall ret w. + forall ret. Options {- ^ output/verbosity options -} -> SharedContext {- ^ context for constructing SAW terms -} -> JVMCrucibleContext {- ^ context for interacting with Crucible -} -> Crucible.TypeRepr ret {- ^ type representation of function return value -} -> CrucibleMethodSpecIR {- ^ specification for current function override -} -> - OverrideMatcher CJ.JVM w (Crucible.RegValue Sym ret) + OverrideMatcher CJ.JVM RW (Crucible.RegValue Sym ret) methodSpecHandler_poststate opts sc cc retTy cs = do executeCond opts sc cc cs (cs ^. MS.csPostState) computeReturnValue opts cc sc cs retTy (cs ^. MS.csRetValue) @@ -350,10 +348,22 @@ learnCond opts sc cc cs prepost ss = do let loc = cs ^. MS.csLoc matchPointsTos opts sc cc cs prepost (ss ^. MS.csPointsTos) traverse_ (learnSetupCondition opts sc cc cs prepost) (ss ^. MS.csConditions) + assertTermEqualities sc cc enforceDisjointness cc loc ss enforceCompleteSubstitution loc ss +assertTermEqualities :: + SharedContext -> + JVMCrucibleContext -> + OverrideMatcher CJ.JVM md () +assertTermEqualities sc cc = do + let assertTermEquality (t, md, e) = do + p <- instantiateExtResolveSAWPred sc cc t + addAssert p md e + traverse_ assertTermEquality =<< OM (use termEqs) + + -- execute a pre/post condition executeCond :: Options -> @@ -361,7 +371,7 @@ executeCond :: JVMCrucibleContext -> CrucibleMethodSpecIR -> StateSpec -> - OverrideMatcher CJ.JVM w () + OverrideMatcher CJ.JVM RW () executeCond opts sc cc cs ss = do refreshTerms sc ss traverse_ (executeAllocation opts cc) (Map.assocs (ss ^. MS.csAllocs)) @@ -508,26 +518,6 @@ assignVar cc md var ref = ------------------------------------------------------------------------ - -assignTerm :: - SharedContext {- ^ context for constructing SAW terms -} -> - JVMCrucibleContext {- ^ context for interacting with Crucible -} -> - MS.ConditionMetadata -> - PrePost -> - VarIndex {- ^ external constant index -} -> - Term {- ^ value -} -> - OverrideMatcher CJ.JVM w () - -assignTerm sc cc md prepost var val = - do mb <- OM (use (termSub . at var)) - case mb of - Nothing -> OM (termSub . at var ?= val) - Just old -> - matchTerm sc cc md prepost val old - - ------------------------------------------------------------------------- - -- | Match the value of a function argument with a symbolic 'SetupValue'. matchArg :: Options {- ^ saw script print out opts -} -> @@ -547,7 +537,7 @@ matchArg opts sc cc cs prepost md actual expectedTy expected@(MS.SetupTerm expec = do sym <- Ov.getSymInterface failMsg <- mkStructuralMismatch opts cc sc cs actual expected expectedTy realTerm <- valueToSC sym md failMsg tval actual - matchTerm sc cc md prepost realTerm (ttTerm expectedTT) + matchTerm sc md prepost realTerm (ttTerm expectedTT) matchArg opts sc cc cs prepost md actual@(RVal ref) expectedTy setupval = case setupval of @@ -606,32 +596,6 @@ valueToSC _sym md failMsg _tval _val = ------------------------------------------------------------------------ --- | NOTE: The two 'Term' arguments must have the same type. -matchTerm :: - SharedContext {- ^ context for constructing SAW terms -} -> - JVMCrucibleContext {- ^ context for interacting with Crucible -} -> - MS.ConditionMetadata -> - PrePost -> - Term {- ^ exported concrete term -} -> - Term {- ^ expected specification term -} -> - OverrideMatcher CJ.JVM w () - -matchTerm _ _ _ _ real expect | real == expect = return () -matchTerm sc cc md prepost real expect = - do free <- OM (use osFree) - let loc = MS.conditionLoc md - case unwrapTermF expect of - FTermF (ExtCns ec) - | Set.member (ecVarIndex ec) free -> - do assignTerm sc cc md prepost (ecVarIndex ec) real - - _ -> - do t <- liftIO $ scEq sc real expect - p <- liftIO $ resolveBoolTerm (cc ^. jccSym) t - addAssert p md (Crucible.SimError loc (Crucible.AssertFailureSimError ("literal equality " ++ MS.stateCond prepost) "")) - ------------------------------------------------------------------------- - -- | Use the current state to learn about variable assignments based on -- preconditions for a procedure specification. learnSetupCondition :: @@ -642,9 +606,11 @@ learnSetupCondition :: PrePost -> SetupCondition -> OverrideMatcher CJ.JVM w () -learnSetupCondition opts sc cc spec prepost (MS.SetupCond_Equal md val1 val2) = learnEqual opts sc cc spec md prepost val1 val2 -learnSetupCondition _opts sc cc _ prepost (MS.SetupCond_Pred md tm) = learnPred sc cc md prepost (ttTerm tm) -learnSetupCondition _opts _ _ _ _ (MS.SetupCond_Ghost empty _ _ _) = absurd empty +learnSetupCondition opts sc cc spec prepost cond = + case cond of + MS.SetupCond_Equal md val1 val2 -> learnEqual opts sc cc spec md prepost val1 val2 + MS.SetupCond_Pred md tm -> learnPred sc cc md prepost (ttTerm tm) + MS.SetupCond_Ghost md var val -> learnGhost sc md prepost var val ------------------------------------------------------------------------ @@ -717,7 +683,7 @@ learnPointsTo opts sc cc spec prepost pt = ety_tm <- liftIO $ Cryptol.importType sc Cryptol.emptyEnv ety ts <- traverse load [0 .. fromInteger len - 1] realTerm <- liftIO $ scVector sc ety_tm ts - matchTerm sc cc md prepost realTerm (ttTerm tt) + matchTerm sc md prepost realTerm (ttTerm tt) -- If the right-hand-side is 'Nothing', this is indicates a "modifies" declaration, -- which should probably not appear in the pre-state section, and has no effect. @@ -761,6 +727,15 @@ learnPred sc cc md prepost t = let loc = MS.conditionLoc md addAssert p md (Crucible.SimError loc (Crucible.AssertFailureSimError (MS.stateCond prepost) "")) +instantiateExtResolveSAWPred :: + SharedContext -> + JVMCrucibleContext -> + Term -> + OverrideMatcher CJ.JVM md (W4.Pred Sym) +instantiateExtResolveSAWPred sc cc cond = do + sub <- OM (use termSub) + liftIO $ resolveSAWPred cc =<< scInstantiateExt sc sub cond + ------------------------------------------------------------------------ -- TODO: replace (W4.ProgramLoc, J.Type) by some allocation datatype @@ -800,10 +775,13 @@ executeSetupCondition :: JVMCrucibleContext -> CrucibleMethodSpecIR -> SetupCondition -> - OverrideMatcher CJ.JVM w () -executeSetupCondition opts sc cc spec (MS.SetupCond_Equal md val1 val2) = executeEqual opts sc cc spec md val1 val2 -executeSetupCondition _opts sc cc _ (MS.SetupCond_Pred md tm) = executePred sc cc md tm -executeSetupCondition _ _ _ _ (MS.SetupCond_Ghost empty _ _ _) = absurd empty + OverrideMatcher CJ.JVM RW () +executeSetupCondition opts sc cc spec = + \case + MS.SetupCond_Equal md val1 val2 -> + executeEqual opts sc cc spec md val1 val2 + MS.SetupCond_Pred md tm -> executePred sc cc md tm + MS.SetupCond_Ghost md var val -> executeGhost sc md var val ------------------------------------------------------------------------ diff --git a/src/SAWScript/Crucible/JVM/Setup/Value.hs b/src/SAWScript/Crucible/JVM/Setup/Value.hs index 8286704750..a69e29ec05 100644 --- a/src/SAWScript/Crucible/JVM/Setup/Value.hs +++ b/src/SAWScript/Crucible/JVM/Setup/Value.hs @@ -87,8 +87,6 @@ type instance MS.XSetupCast CJ.JVM = Void type instance MS.XSetupUnion CJ.JVM = Void type instance MS.XSetupGlobalInitializer CJ.JVM = Void -type instance MS.XGhostState CJ.JVM = Void - type JIdent = String -- FIXME(huffman): what to put here? type instance MS.TypeName CJ.JVM = JIdent diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index 9a7332b86e..625e0db955 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -188,6 +188,7 @@ import Verifier.SAW.TypedTerm -- saw-script import SAWScript.AST (Located(..)) +import SAWScript.Builtins (ghost_value) import SAWScript.Proof import SAWScript.Prover.SolverStats import SAWScript.Prover.Versions @@ -1205,7 +1206,7 @@ setupPrestateConditions mspec cc mem env = aux [] let lp = Crucible.LabeledPred (ttTerm tm) (md, "precondition") in aux (lp:acc) globals xs - aux acc globals (MS.SetupCond_Ghost () _md var val : xs) = + aux acc globals (MS.SetupCond_Ghost _md var val : xs) = case val of TypedTerm (TypedTermSchema sch) tm -> aux acc (Crucible.insertGlobal var (sch,tm) globals) xs @@ -2799,15 +2800,7 @@ llvm_ghost_value :: TypedTerm -> LLVMCrucibleSetupM () llvm_ghost_value ghost val = LLVMCrucibleSetupM $ - do loc <- getW4Position "llvm_ghost_value" - tags <- view Setup.croTags - let md = MS.ConditionMetadata - { MS.conditionLoc = loc - , MS.conditionTags = tags - , MS.conditionType = "ghost value" - , MS.conditionContext = "" - } - Setup.addCondition (MS.SetupCond_Ghost () md ghost val) + ghost_value ghost val llvm_spec_solvers :: SomeLLVM MS.ProvedSpec -> [String] llvm_spec_solvers (SomeLLVM ps) = diff --git a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs index 2ed66092e3..d64181171e 100644 --- a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs @@ -12,11 +12,9 @@ Stability : provisional {-# LANGUAGE DoAndIfThenElse #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE LambdaCase #-} -{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE PatternSynonyms #-} @@ -119,16 +117,12 @@ module SAWScript.Crucible.LLVM.MethodSpecIR ) where import Control.Lens -import Control.Monad (when) import Data.Functor.Compose (Compose(..)) import qualified Data.Map as Map import qualified Prettyprinter as PPL import qualified Text.LLVM.AST as L import qualified Text.LLVM.PP as L -import qualified Cryptol.TypeCheck.AST as Cryptol -import qualified Cryptol.Utils.PP as Cryptol (pp) - import Data.Parameterized.All (All(All)) import Data.Parameterized.Some (Some(Some)) import qualified Data.Parameterized.Map as MapF @@ -137,7 +131,7 @@ import What4.ProgramLoc (ProgramLoc) import qualified Lang.Crucible.Types as Crucible (SymbolRepr, knownSymbol) import qualified Lang.Crucible.Simulator.Intrinsics as Crucible - (IntrinsicClass(Intrinsic, muxIntrinsic), IntrinsicMuxFn(IntrinsicMuxFn)) + (IntrinsicMuxFn(IntrinsicMuxFn)) import SAWScript.Crucible.Common import qualified SAWScript.Crucible.Common.MethodSpec as MS @@ -146,9 +140,6 @@ import qualified SAWScript.Crucible.Common.Setup.Type as Setup import qualified SAWScript.Crucible.LLVM.CrucibleLLVM as CL import SAWScript.Crucible.LLVM.Setup.Value -import Verifier.SAW.Simulator.What4.ReturnTrip ( toSC, saw_ctx ) - -import Verifier.SAW.SharedTerm import Verifier.SAW.TypedTerm @@ -177,24 +168,6 @@ mutIso = isMut :: Lens' LLVMAllocSpec Bool isMut = allocSpecMut . mutIso --------------------------------------------------------------------------------- --- ** Ghost state - -instance Crucible.IntrinsicClass Sym MS.GhostValue where - type Intrinsic Sym MS.GhostValue ctx = (Cryptol.Schema, Term) - muxIntrinsic sym _ _namerep _ctx prd (thnSch,thn) (elsSch,els) = - do when (thnSch /= elsSch) $ fail $ unlines $ - [ "Attempted to mux ghost variables of different types:" - , show (Cryptol.pp thnSch) - , show (Cryptol.pp elsSch) - ] - st <- sawCoreState sym - let sc = saw_ctx st - prd' <- toSC sym st prd - typ <- scTypeOf sc thn - res <- scIte sc typ prd' thn els - return (thnSch, res) - -------------------------------------------------------------------------------- -- ** CrucibleContext diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index f28768f11b..44dc4f89e4 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -64,7 +64,7 @@ import Control.Lens.Getter import Control.Lens.Lens import Control.Lens.Setter import Control.Exception as X -import Control.Monad (filterM, foldM, forM, forM_, when, zipWithM) +import Control.Monad (filterM, foldM, forM, forM_, zipWithM) import Control.Monad.Except (runExcept) import Control.Monad.IO.Class (MonadIO(..)) import Data.Either (partitionEithers) @@ -87,7 +87,6 @@ import qualified Text.LLVM.AST as L import qualified Cryptol.TypeCheck.AST as Cryptol (Schema(..)) import qualified Cryptol.Eval.Type as Cryptol (TValue(..), evalType) -import qualified Cryptol.Utils.PP as Cryptol (pp) import qualified Lang.Crucible.Backend as Crucible import qualified Lang.Crucible.CFG.Core as Crucible (TypeRepr(UnitRepr)) @@ -117,9 +116,7 @@ import Data.Parameterized.NatRepr import Data.Parameterized.Some (Some(..)) import qualified Data.BitVector.Sized as BV -import Verifier.SAW.Prelude (scEq) import Verifier.SAW.SharedTerm -import Verifier.SAW.TypedAST import Verifier.SAW.Recognizer import Verifier.SAW.TypedTerm import Verifier.SAW.Simulator.What4.ReturnTrip (SAWCoreState(..), toSC, bindSAWTerm) @@ -1073,29 +1070,6 @@ assignVar cc md var val = ------------------------------------------------------------------------ - -assignTerm :: - SharedContext {- ^ context for constructing SAW terms -} -> - LLVMCrucibleContext arch {- ^ context for interacting with Crucible -} -> - MS.ConditionMetadata -> - PrePost -> - VarIndex {- ^ external constant index -} -> - Term {- ^ value -} -> - OverrideMatcher (LLVM arch) md () - -assignTerm sc cc md prepost var val = - do mb <- OM (use (termSub . at var)) - case mb of - Nothing -> OM (termSub . at var ?= val) - Just old -> - matchTerm sc cc md prepost val old - --- do t <- liftIO $ scEq sc old val --- p <- liftIO $ resolveSAWPred cc t --- addAssert p (Crucible.AssertFailureSimError ("literal equality " ++ MS.stateCond prepost)) - ------------------------------------------------------------------------- - diffMemTypes :: Crucible.HasPtrWidth wptr => Crucible.MemType -> @@ -1176,7 +1150,7 @@ matchArg opts sc cc cs prepost md actual expectedTy expected = , Right tval <- Cryptol.evalType mempty tyexpr -> do failMsg <- mkStructuralMismatch opts cc sc cs actual expected expectedTy realTerm <- valueToSC sym md failMsg tval actual - instantiateExtMatchTerm sc cc md prepost realTerm (ttTerm expectedTT) + instantiateExtMatchTerm sc md prepost realTerm (ttTerm expectedTT) -- match arrays point-wise (Crucible.LLVMValArray _ xs, Crucible.ArrayType _len y, SetupArray () zs) @@ -1346,50 +1320,6 @@ typeToSC sc t = do fields' <- V.toList <$> traverse (typeToSC sc . view Crucible.fieldVal) fields scTupleType sc fields' ------------------------------------------------------------------------- - --- | NOTE: The two 'Term' arguments must have the same type. -instantiateExtMatchTerm :: - SharedContext {- ^ context for constructing SAW terms -} -> - LLVMCrucibleContext arch {- ^ context for interacting with Crucible -} -> - MS.ConditionMetadata -> - PrePost -> - Term {- ^ exported concrete term -} -> - Term {- ^ expected specification term -} -> - OverrideMatcher (LLVM arch) md () -instantiateExtMatchTerm sc cc md prepost actual expected = do - sub <- OM (use termSub) - matchTerm sc cc md prepost actual =<< liftIO (scInstantiateExt sc sub expected) - -matchTerm :: - SharedContext {- ^ context for constructing SAW terms -} -> - LLVMCrucibleContext arch {- ^ context for interacting with Crucible -} -> - MS.ConditionMetadata -> - PrePost -> - Term {- ^ exported concrete term -} -> - Term {- ^ expected specification term -} -> - OverrideMatcher (LLVM arch) md () - -matchTerm _ _ _ _ real expect | real == expect = return () -matchTerm sc cc md prepost real expect = - do let loc = MS.conditionLoc md - free <- OM (use osFree) - case unwrapTermF expect of - FTermF (ExtCns ec) - | Set.member (ecVarIndex ec) free -> - do assignTerm sc cc md prepost (ecVarIndex ec) real - - _ -> - do t <- liftIO $ scEq sc real expect - let msg = unlines $ - [ "Literal equality " ++ MS.stateCond prepost --- , "Expected term: " ++ prettyTerm expect --- , "Actual term: " ++ prettyTerm real - ] - addTermEq t md $ Crucible.SimError loc $ Crucible.AssertFailureSimError msg "" --- where prettyTerm = show . ppTermDepth 20 - - ------------------------------------------------------------------------ -- | Use the current state to learn about variable assignments based on @@ -1405,36 +1335,10 @@ learnSetupCondition :: OverrideMatcher (LLVM arch) md () learnSetupCondition opts sc cc spec prepost cond = case cond of - MS.SetupCond_Equal md val1 val2 -> learnEqual opts sc cc spec md prepost val1 val2 - MS.SetupCond_Pred md tm -> learnPred sc cc md prepost (ttTerm tm) - MS.SetupCond_Ghost () md var val -> learnGhost sc cc md prepost var val - - ------------------------------------------------------------------------- + MS.SetupCond_Equal md val1 val2 -> learnEqual opts sc cc spec md prepost val1 val2 + MS.SetupCond_Pred md tm -> learnPred sc cc md prepost (ttTerm tm) + MS.SetupCond_Ghost md var val -> learnGhost sc md prepost var val --- TODO(lb): make this language-independent! -learnGhost :: - SharedContext -> - LLVMCrucibleContext arch -> - MS.ConditionMetadata -> - PrePost -> - MS.GhostGlobal -> - TypedTerm -> - OverrideMatcher (LLVM arch) md () -learnGhost sc cc md prepost var (TypedTerm (TypedTermSchema schEx) tmEx) = - do (sch,tm) <- readGlobal var - when (sch /= schEx) $ fail $ unlines $ - [ "Ghost variable had the wrong type:" - , "- Expected: " ++ show (Cryptol.pp schEx) - , "- Actual: " ++ show (Cryptol.pp sch) - ] - instantiateExtMatchTerm sc cc md prepost tm tmEx -learnGhost _sc _cc _md _prepost _var (TypedTerm tp _) - = fail $ unlines - [ "Ghost variable expected value has improper type" - , "expected Cryptol schema type, but got" - , show (MS.ppTypedTermType tp) - ] ------------------------------------------------------------------------ @@ -1553,7 +1457,7 @@ matchPointsToValue opts sc cc spec prepost md maybe_cond ptr val = off_tm -- src offset instantiated_expected_sz_tm -- length - instantiateExtMatchTerm sc cc md prepost arr_tm $ ttTerm expected_arr_tm + instantiateExtMatchTerm sc md prepost arr_tm $ ttTerm expected_arr_tm sz_tm <- liftIO $ toSC sym st sz expected_end_off_tm <- liftIO $ scBvAdd sc ptr_width_tm off_tm $ ttTerm expected_sz_tm @@ -1979,27 +1883,7 @@ executeSetupCondition opts sc cc spec = MS.SetupCond_Equal md val1 val2 -> executeEqual opts sc cc spec md val1 val2 MS.SetupCond_Pred md tm -> executePred sc cc md tm - MS.SetupCond_Ghost () md var val -> executeGhost sc md var val - ------------------------------------------------------------------------- - --- TODO(lb): make this language independent! -executeGhost :: - SharedContext -> - MS.ConditionMetadata -> - MS.GhostGlobal -> - TypedTerm -> - OverrideMatcher (LLVM arch) RW () -executeGhost sc _md var (TypedTerm (TypedTermSchema sch) tm) = - do s <- OM (use termSub) - tm' <- liftIO (scInstantiateExt sc s tm) - writeGlobal var (sch,tm') -executeGhost _sc _md _var (TypedTerm tp _) = - fail $ unlines - [ "executeGhost: improper value type" - , "expected Cryptol schema type, but got" - , show (MS.ppTypedTermType tp) - ] + MS.SetupCond_Ghost md var val -> executeGhost sc md var val ------------------------------------------------------------------------ diff --git a/src/SAWScript/Crucible/LLVM/Setup/Value.hs b/src/SAWScript/Crucible/LLVM/Setup/Value.hs index ac5baba510..9f301187f7 100644 --- a/src/SAWScript/Crucible/LLVM/Setup/Value.hs +++ b/src/SAWScript/Crucible/LLVM/Setup/Value.hs @@ -130,8 +130,6 @@ type instance Setup.XSetupUnion (LLVM _) = () type instance Setup.XSetupGlobal (LLVM _) = () type instance Setup.XSetupGlobalInitializer (LLVM _) = () -type instance Setup.XGhostState (LLVM _) = () - type instance Setup.TypeName (LLVM arch) = CL.Ident type instance Setup.ExtType (LLVM arch) = CL.MemType diff --git a/src/SAWScript/Crucible/MIR/Builtins.hs b/src/SAWScript/Crucible/MIR/Builtins.hs index 341e6dac0c..fdead987dd 100644 --- a/src/SAWScript/Crucible/MIR/Builtins.hs +++ b/src/SAWScript/Crucible/MIR/Builtins.hs @@ -18,6 +18,7 @@ module SAWScript.Crucible.MIR.Builtins , mir_fresh_cryptol_var , mir_fresh_expanded_value , mir_fresh_var + , mir_ghost_value , mir_load_module , mir_points_to , mir_postcond @@ -81,7 +82,6 @@ import Data.Text (Text) import Data.Time.Clock (diffUTCTime, getCurrentTime) import Data.Traversable (mapAccumL) import Data.Type.Equality (TestEquality(..)) -import Data.Void (absurd) import qualified Prettyprinter as PP import System.IO (stdout) @@ -116,6 +116,7 @@ import Verifier.SAW.SharedTerm import Verifier.SAW.Simulator.What4.ReturnTrip import Verifier.SAW.TypedTerm +import SAWScript.Builtins (ghost_value) import SAWScript.Crucible.Common import qualified SAWScript.Crucible.Common.MethodSpec as MS import SAWScript.Crucible.Common.Override @@ -395,6 +396,13 @@ mir_fresh_var name mty = Nothing -> X.throwM $ MIRFreshVarInvalidType mty Just cty -> Setup.freshVariable sc name cty +mir_ghost_value :: + MS.GhostGlobal -> + TypedTerm -> + MIRSetupM () +mir_ghost_value ghost val = MIRSetupM $ + ghost_value ghost val + -- | Load a MIR JSON file and return a handle to it. mir_load_module :: String -> TopLevel Mir.RustModule mir_load_module inputFile = do @@ -757,32 +765,43 @@ setupPrePointsTos :: setupPrePointsTos mspec cc env pts mem0 = foldM (doPointsTo mspec cc env) mem0 pts --- | Collects boolean terms that should be assumed to be true. +-- | Sets up globals (ghost variable), and collects boolean terms +-- that should be assumed to be true. setupPrestateConditions :: MethodSpec -> MIRCrucibleContext -> Map MS.AllocIndex (Some (MirPointer Sym)) -> + Crucible.SymGlobalState Sym -> [SetupCondition] -> - IO [Crucible.LabeledPred Term AssumptionReason] + IO ( Crucible.SymGlobalState Sym, [Crucible.LabeledPred Term AssumptionReason] + ) setupPrestateConditions mspec cc env = aux [] where tyenv = MS.csAllocations mspec nameEnv = mspec ^. MS.csPreState . MS.csVarTypeNames - aux acc [] = return acc + aux acc globals [] = return (globals, acc) - aux acc (MS.SetupCond_Equal loc val1 val2 : xs) = + aux acc globals (MS.SetupCond_Equal loc val1 val2 : xs) = do val1' <- resolveSetupVal cc env tyenv nameEnv val1 val2' <- resolveSetupVal cc env tyenv nameEnv val2 t <- assertEqualVals cc val1' val2' let lp = Crucible.LabeledPred t (loc, "equality precondition") - aux (lp:acc) xs + aux (lp:acc) globals xs - aux acc (MS.SetupCond_Pred loc tm : xs) = + aux acc globals (MS.SetupCond_Pred loc tm : xs) = let lp = Crucible.LabeledPred (ttTerm tm) (loc, "precondition") in - aux (lp:acc) xs - - aux _ (MS.SetupCond_Ghost empty_ _ _ _ : _) = absurd empty_ + aux (lp:acc) globals xs + + aux acc globals (MS.SetupCond_Ghost _md var val : xs) = + case val of + TypedTerm (TypedTermSchema sch) tm -> + aux acc (Crucible.insertGlobal var (sch,tm) globals) xs + TypedTerm tp _ -> + fail $ unlines + [ "Setup term for global variable expected to have Cryptol schema type, but got" + , show (MS.ppTypedTermType tp) + ] verifyObligations :: MIRCrucibleContext -> @@ -962,7 +981,8 @@ verifyPrestate cc mspec globals0 = globals0 globals2 <- setupPrePointsTos mspec cc env (mspec ^. MS.csPreState . MS.csPointsTos) globals1 - cs <- setupPrestateConditions mspec cc env (mspec ^. MS.csPreState . MS.csConditions) + (globals3, cs) <- + setupPrestateConditions mspec cc env globals2 (mspec ^. MS.csPreState . MS.csConditions) args <- resolveArguments cc mspec env -- Check the type of the return setup value @@ -983,7 +1003,7 @@ verifyPrestate cc mspec globals0 = ] (Nothing, _) -> return () - return (args, cs, env, globals2) + return (args, cs, env, globals3) -- | Simulate a MIR function with Crucible as part of a 'mir_verify' command, -- making sure to install any overrides that the user supplies. diff --git a/src/SAWScript/Crucible/MIR/Override.hs b/src/SAWScript/Crucible/MIR/Override.hs index bea3d78edf..11826af349 100644 --- a/src/SAWScript/Crucible/MIR/Override.hs +++ b/src/SAWScript/Crucible/MIR/Override.hs @@ -69,10 +69,8 @@ import qualified What4.Interface as W4 import qualified What4.LabeledPred as W4 import qualified What4.ProgramLoc as W4 -import Verifier.SAW.Prelude (scEq) import Verifier.SAW.SharedTerm import Verifier.SAW.Simulator.What4.ReturnTrip (saw_ctx, toSC) -import Verifier.SAW.TypedAST import Verifier.SAW.TypedTerm import SAWScript.Crucible.Common @@ -120,22 +118,6 @@ assignVar cc md var sref@(Some ref) = do p <- liftIO (equalRefsPred cc ref ref') addAssert p md (Crucible.SimError loc (Crucible.AssertFailureSimError "equality of aliased references" "")) -assignTerm :: - SharedContext {- ^ context for constructing SAW terms -} -> - MIRCrucibleContext {- ^ context for interacting with Crucible -} -> - MS.ConditionMetadata -> - MS.PrePost -> - VarIndex {- ^ external constant index -} -> - Term {- ^ value -} -> - OverrideMatcher MIR w () - -assignTerm sc cc md prepost var val = - do mb <- OM (use (termSub . at var)) - case mb of - Nothing -> OM (termSub . at var ?= val) - Just old -> - matchTerm sc cc md prepost val old - -- | When a specification is used as a composition override, this function -- checks that the postconditions of the specification fully specify (via -- @mir_points_to@ statements) the values of all local mutable allocations @@ -607,7 +589,7 @@ executeCond :: MIRCrucibleContext -> CrucibleMethodSpecIR -> StateSpec -> - OverrideMatcher MIR w () + OverrideMatcher MIR RW () executeCond opts sc cc cs ss = do refreshTerms sc ss F.traverse_ (executeAllocation opts cc) (Map.assocs (ss ^. MS.csAllocs)) @@ -654,10 +636,13 @@ executeSetupCondition :: MIRCrucibleContext -> CrucibleMethodSpecIR -> SetupCondition -> - OverrideMatcher MIR w () -executeSetupCondition opts sc cc spec (MS.SetupCond_Equal md val1 val2) = executeEqual opts sc cc spec md val1 val2 -executeSetupCondition _ sc cc _ (MS.SetupCond_Pred md tm) = executePred sc cc md tm -executeSetupCondition _ _ _ _ (MS.SetupCond_Ghost empty _ _ _) = absurd empty + OverrideMatcher MIR RW () +executeSetupCondition opts sc cc spec = + \case + MS.SetupCond_Equal md val1 val2 -> + executeEqual opts sc cc spec md val1 val2 + MS.SetupCond_Pred md tm -> executePred sc cc md tm + MS.SetupCond_Ghost md var val -> executeGhost sc md var val handleSingleOverrideBranch :: forall rtp args ret. Options {- ^ output/verbosity options -} -> @@ -1026,9 +1011,11 @@ learnSetupCondition :: MS.PrePost -> SetupCondition -> OverrideMatcher MIR w () -learnSetupCondition opts sc cc spec prepost (MS.SetupCond_Equal md val1 val2) = learnEqual opts sc cc spec md prepost val1 val2 -learnSetupCondition _opts sc cc _ prepost (MS.SetupCond_Pred md tm) = learnPred sc cc md prepost (ttTerm tm) -learnSetupCondition _opts _ _ _ _ (MS.SetupCond_Ghost empty _ _ _) = absurd empty +learnSetupCondition opts sc cc spec prepost cond = + case cond of + MS.SetupCond_Equal md val1 val2 -> learnEqual opts sc cc spec md prepost val1 val2 + MS.SetupCond_Pred md tm -> learnPred sc cc md prepost (ttTerm tm) + MS.SetupCond_Ghost md var val -> learnGhost sc md prepost var val -- | Match the value of a function argument with a symbolic 'SetupValue'. matchArg :: @@ -1049,7 +1036,7 @@ matchArg opts sc cc cs prepost md actual expectedTy expected@(MS.SetupTerm expec = do sym <- Ov.getSymInterface failMsg <- mkStructuralMismatch opts cc sc cs actual expected expectedTy realTerm <- valueToSC sym md failMsg tval actual - matchTerm sc cc md prepost realTerm (ttTerm expectedTT) + matchTerm sc md prepost realTerm (ttTerm expectedTT) matchArg opts sc cc cs prepost md actual expectedTy expected = mccWithBackend cc $ \bak -> do @@ -1272,33 +1259,6 @@ matchPointsTos opts sc cc spec prepost = go False [] setupSlice (MirSetupSliceRange arr _start _end) = setupVars arr -matchTerm :: - SharedContext {- ^ context for constructing SAW terms -} -> - MIRCrucibleContext {- ^ context for interacting with Crucible -} -> - MS.ConditionMetadata -> - MS.PrePost -> - Term {- ^ exported concrete term -} -> - Term {- ^ expected specification term -} -> - OverrideMatcher MIR md () - -matchTerm _ _ _ _ real expect | real == expect = return () -matchTerm sc cc md prepost real expect = - do let loc = MS.conditionLoc md - free <- OM (use osFree) - case unwrapTermF expect of - FTermF (ExtCns ec) - | Set.member (ecVarIndex ec) free -> - do assignTerm sc cc md prepost (ecVarIndex ec) real - - _ -> - do t <- liftIO $ scEq sc real expect - let msg = unlines $ - [ "Literal equality " ++ MS.stateCond prepost --- , "Expected term: " ++ prettyTerm expect --- , "Actual term: " ++ prettyTerm real - ] - addTermEq t md $ Crucible.SimError loc $ Crucible.AssertFailureSimError msg "" - -- | This function is responsible for implementing the \"override\" behavior -- of method specifications. The main work done in this function to manage -- the process of selecting between several possible different override @@ -1403,13 +1363,13 @@ methodSpecHandler opts sc cc mdMap css h = -- which involves writing values into memory, computing the return value, -- and computing postcondition predicates. methodSpecHandler_poststate :: - forall ret w. + forall ret. Options {- ^ output/verbosity options -} -> SharedContext {- ^ context for constructing SAW terms -} -> MIRCrucibleContext {- ^ context for interacting with Crucible -} -> Crucible.TypeRepr ret {- ^ type representation of function return value -} -> CrucibleMethodSpecIR {- ^ specification for current function override -} -> - OverrideMatcher MIR w (Crucible.RegValue Sym ret) + OverrideMatcher MIR RW (Crucible.RegValue Sym ret) methodSpecHandler_poststate opts sc cc retTy cs = do executeCond opts sc cc cs (cs ^. MS.csPostState) computeReturnValue opts cc sc cs retTy (cs ^. MS.csRetValue) diff --git a/src/SAWScript/Crucible/MIR/Setup/Value.hs b/src/SAWScript/Crucible/MIR/Setup/Value.hs index f764de1f17..bbdfbd85a9 100644 --- a/src/SAWScript/Crucible/MIR/Setup/Value.hs +++ b/src/SAWScript/Crucible/MIR/Setup/Value.hs @@ -81,8 +81,6 @@ type instance MS.XSetupCast MIR = Void type instance MS.XSetupUnion MIR = Void type instance MS.XSetupGlobalInitializer MIR = () -type instance MS.XGhostState MIR = Void - type instance MS.TypeName MIR = Text type instance MS.ExtType MIR = M.Ty diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index d28188b79c..34a021d769 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -3633,6 +3633,20 @@ primitives = Map.fromList Current [ "Legacy alternative name for `llvm_ghost_value`."] + , prim "jvm_ghost_value" + "Ghost -> Term -> JVMSetup ()" + (pureVal jvm_ghost_value) + Current + [ "Specifies the value of a ghost variable. This can be used" + , "in the pre- and post- conditions of a setup block."] + + , prim "mir_ghost_value" + "Ghost -> Term -> MIRSetup ()" + (pureVal mir_ghost_value) + Current + [ "Specifies the value of a ghost variable. This can be used" + , "in the pre- and post- conditions of a setup block."] + , prim "llvm_spec_solvers" "LLVMSpec -> [String]" (\_ _ -> toValue llvm_spec_solvers) Current From 3fa027c696c27edcb063f905185b6305d90b792a Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 13 Nov 2023 10:02:56 -0500 Subject: [PATCH 3/3] Make symbolic branching work with JVM/MIR ghost state This is not entirely straightforward to do for the JVM backend, as the `jvmSimContext` function (`crucible-jvm`'s API function for constructing a `SimContext`) does not support adding additional intrinsic types, including the intrinsic type needed to support SAW ghost state. For the time being, I have simply inlined the implementation of `jvmSimContext` as needed, and I have opened https://github.com/GaloisInc/crucible/issues/1128 as a reminder to generalize `jvmSimContext` upstream. --- .../test_mir_ghost_symbolic_branch/Makefile | 13 ++++++++++ .../test.linked-mir.json | 1 + .../test_mir_ghost_symbolic_branch/test.rs | 10 ++++++++ .../test_mir_ghost_symbolic_branch/test.saw | 24 +++++++++++++++++++ .../test_mir_ghost_symbolic_branch/test.sh | 3 +++ src/SAWScript/Crucible/JVM/Builtins.hs | 8 ++++++- src/SAWScript/Crucible/JVM/MethodSpecIR.hs | 16 +++++++++++++ src/SAWScript/Crucible/LLVM/MethodSpecIR.hs | 4 +++- src/SAWScript/Crucible/MIR/Builtins.hs | 2 +- src/SAWScript/Crucible/MIR/MethodSpecIR.hs | 20 ++++++++++++++++ src/SAWScript/Crucible/MIR/Override.hs | 8 +++---- .../Crucible/MIR/ResolveSetupValue.hs | 7 +++--- 12 files changed, 106 insertions(+), 10 deletions(-) create mode 100644 intTests/test_mir_ghost_symbolic_branch/Makefile create mode 100644 intTests/test_mir_ghost_symbolic_branch/test.linked-mir.json create mode 100644 intTests/test_mir_ghost_symbolic_branch/test.rs create mode 100644 intTests/test_mir_ghost_symbolic_branch/test.saw create mode 100755 intTests/test_mir_ghost_symbolic_branch/test.sh diff --git a/intTests/test_mir_ghost_symbolic_branch/Makefile b/intTests/test_mir_ghost_symbolic_branch/Makefile new file mode 100644 index 0000000000..bc6297ae15 --- /dev/null +++ b/intTests/test_mir_ghost_symbolic_branch/Makefile @@ -0,0 +1,13 @@ +all: test.linked-mir.json + +test.linked-mir.json: test.rs + saw-rustc $< + $(MAKE) remove-unused-build-artifacts + +.PHONY: remove-unused-build-artifacts +remove-unused-build-artifacts: + rm -f test libtest.mir libtest.rlib + +.PHONY: clean +clean: remove-unused-build-artifacts + rm -f test.linked-mir.json diff --git a/intTests/test_mir_ghost_symbolic_branch/test.linked-mir.json b/intTests/test_mir_ghost_symbolic_branch/test.linked-mir.json new file mode 100644 index 0000000000..deea148368 --- /dev/null +++ b/intTests/test_mir_ghost_symbolic_branch/test.linked-mir.json @@ -0,0 +1 @@ +{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::bool"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::bool"}},"pos":"test.rs:5:8: 5:9","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::bool"}},"kind":"Copy"}}}],"terminator":{"discr":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::bool"}},"kind":"Move"},"discr_span":"test.rs:5:8: 5:9 !test.rs:5:8: 5:9","kind":"SwitchInt","pos":"test.rs:5:8: 5:9 !test.rs:5:8: 5:9","switch_ty":"ty::bool","targets":["bb2","bb1"],"values":["0"]}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"args":[{"data":{"rendered":{"kind":"uint","size":4,"val":"27"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}},"bb3"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::140cf1f14525dfe1"},"kind":"Constant"},"kind":"Call","pos":"test.rs:6:9: 6:14"}},"blockid":"bb1"},{"block":{"data":[],"terminator":{"args":[{"data":{"rendered":{"kind":"uint","size":4,"val":"42"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}},"bb3"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::140cf1f14525dfe1"},"kind":"Constant"},"kind":"Call","pos":"test.rs:8:9: 8:14"}},"blockid":"bb2"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:10:2: 10:2"}},"blockid":"bb3"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::bool"}]},"name":"test/2c9d3c4c::g","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}],"body":{"blocks":[{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:2:21: 2:21"}},"blockid":"bb0"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}]},"name":"test/2c9d3c4c::f","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null}],"adts":[],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/2c9d3c4c::g","kind":"Item","substs":[]},"name":"test/2c9d3c4c::g"},{"inst":{"def_id":"test/2c9d3c4c::f","kind":"Item","substs":[]},"name":"test/2c9d3c4c::f"}],"tys":[{"name":"ty::bool","ty":{"kind":"Bool"}},{"name":"ty::Tuple::e93222e871854c41","ty":{"kind":"Tuple","tys":[]}},{"name":"ty::FnDef::140cf1f14525dfe1","ty":{"defid":"test/2c9d3c4c::f","kind":"FnDef"}},{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}}],"roots":["test/2c9d3c4c::f","test/2c9d3c4c::g"]} \ No newline at end of file diff --git a/intTests/test_mir_ghost_symbolic_branch/test.rs b/intTests/test_mir_ghost_symbolic_branch/test.rs new file mode 100644 index 0000000000..6a3d06e7fd --- /dev/null +++ b/intTests/test_mir_ghost_symbolic_branch/test.rs @@ -0,0 +1,10 @@ +// Meant to be overridden +pub fn f(_x: u32) {} + +pub fn g(b: bool) { + if b { + f(27) + } else { + f(42) + } +} diff --git a/intTests/test_mir_ghost_symbolic_branch/test.saw b/intTests/test_mir_ghost_symbolic_branch/test.saw new file mode 100644 index 0000000000..e35b0652cc --- /dev/null +++ b/intTests/test_mir_ghost_symbolic_branch/test.saw @@ -0,0 +1,24 @@ +enable_experimental; + +m <- mir_load_module "test.linked-mir.json"; + +g <- declare_ghost_state "g"; + +let f_spec = do { + x <- mir_fresh_var "x" mir_u32; + + mir_execute_func [mir_term x]; + + mir_ghost_value g x; +}; + +let g_spec = do { + b <- mir_fresh_var "b" mir_bool; + + mir_execute_func [mir_term b]; + + mir_ghost_value g ({{ if b then 27 else 42 : [32] }}); +}; + +f_ov <- mir_unsafe_assume_spec m "test::f" f_spec; +mir_verify m "test::g" [f_ov] false g_spec z3; diff --git a/intTests/test_mir_ghost_symbolic_branch/test.sh b/intTests/test_mir_ghost_symbolic_branch/test.sh new file mode 100755 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test_mir_ghost_symbolic_branch/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs index c4e9b3ae80..f2a55d93b4 100644 --- a/src/SAWScript/Crucible/JVM/Builtins.hs +++ b/src/SAWScript/Crucible/JVM/Builtins.hs @@ -673,7 +673,13 @@ verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals _checkSat m regmap <- prepareArgs (Crucible.handleArgTypes h) (map snd args) res <- do let feats = pfs - let simctx = CJ.jvmSimContext bak halloc stdout jc verbosity SAWCruciblePersonality + -- TODO: Use crucible-jvm's jvmSimContext here (instead of manually + -- calling mkDelayedBindings/initSimContext), once + -- https://github.com/GaloisInc/crucible/issues/1128 has been fixed + -- upstream. + let bindings = CJ.mkDelayedBindings jc verbosity + let simctx = Crucible.initSimContext bak intrinsics halloc stdout + bindings CJ.jvmExtensionImpl SAWCruciblePersonality let simSt = Crucible.InitialState simctx globals Crucible.defaultAbortHandler (Crucible.handleReturnType h) let fnCall = Crucible.regValue <$> Crucible.callFnVal (Crucible.HandleFnVal h) regmap let overrideSim = diff --git a/src/SAWScript/Crucible/JVM/MethodSpecIR.hs b/src/SAWScript/Crucible/JVM/MethodSpecIR.hs index bc9e40a9f6..1e3cd413f8 100644 --- a/src/SAWScript/Crucible/JVM/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/JVM/MethodSpecIR.hs @@ -53,9 +53,13 @@ module SAWScript.Crucible.JVM.MethodSpecIR , initialDefCrucibleMethodSpecIR , initialCrucibleSetupState + + , intrinsics ) where import Control.Lens +import qualified Data.Parameterized.Map as MapF +import Data.Parameterized.SymbolRepr (SymbolRepr, knownSymbol) import qualified Prettyprinter as PPL -- what4 @@ -63,6 +67,8 @@ import What4.ProgramLoc (ProgramLoc) -- crucible-jvm import qualified Lang.Crucible.JVM as CJ +import qualified Lang.Crucible.Simulator.Intrinsics as CS + (IntrinsicMuxFn(IntrinsicMuxFn)) import qualified Lang.JVM.Codebase as CB -- jvm-parser @@ -184,6 +190,16 @@ initialCrucibleSetupState cc (cls, method) loc = (J.className cls) method loc +-------------------------------------------------------------------------------- + +-- | The default JVM intrinsics extended with the 'MS.GhostValue' intrinsic, +-- which powers ghost state. +intrinsics :: MapF.MapF SymbolRepr (CS.IntrinsicMuxFn Sym) +intrinsics = + MapF.insert + (knownSymbol :: SymbolRepr MS.GhostValue) + CS.IntrinsicMuxFn + CJ.jvmIntrinsicTypes -------------------------------------------------------------------------------- diff --git a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs index d64181171e..f627d36508 100644 --- a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs @@ -222,8 +222,10 @@ instance PPL.Pretty (LLVMPointsToValue arch) where MS.ppTypedTerm arr PPL.<+> PPL.pretty "[" PPL.<+> MS.ppTypedTerm sz PPL.<+> PPL.pretty "]" -------------------------------------------------------------------------------- --- ** ??? +-- ** SAW LLVM intrinsics +-- | The default LLVM intrinsics extended with the 'MS.GhostValue' intrinsic, +-- which powers ghost state. intrinsics :: MapF.MapF Crucible.SymbolRepr (Crucible.IntrinsicMuxFn Sym) intrinsics = MapF.insert diff --git a/src/SAWScript/Crucible/MIR/Builtins.hs b/src/SAWScript/Crucible/MIR/Builtins.hs index fdead987dd..c81a39546d 100644 --- a/src/SAWScript/Crucible/MIR/Builtins.hs +++ b/src/SAWScript/Crucible/MIR/Builtins.hs @@ -1260,7 +1260,7 @@ setupCrucibleContext rm = (Crucible.UseCFG cfg (Crucible.postdomInfo cfg))) $ Map.elems cfgMap let simctx0 = Crucible.initSimContext bak - Mir.mirIntrinsicTypes halloc stdout + intrinsics halloc stdout bindings Mir.mirExtImpl SAWCruciblePersonality let globals0 = Crucible.emptyGlobals diff --git a/src/SAWScript/Crucible/MIR/MethodSpecIR.hs b/src/SAWScript/Crucible/MIR/MethodSpecIR.hs index b66b3cc02a..c52292ea43 100644 --- a/src/SAWScript/Crucible/MIR/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/MIR/MethodSpecIR.hs @@ -17,6 +17,7 @@ module SAWScript.Crucible.MIR.MethodSpecIR , mccSymGlobalState , mccStaticInitializerMap , mccHandleAllocator + , mccIntrinsicTypes , mccWithBackend , mccSym @@ -53,13 +54,20 @@ module SAWScript.Crucible.MIR.MethodSpecIR -- * Initial CrucibleSetupMethodSpec , initialDefCrucibleMethodSpecIR , initialCrucibleSetupState + + -- * Intrinsics + , intrinsics ) where import Control.Lens (Getter, Iso', Lens', (^.), iso, to) +import qualified Data.Parameterized.Map as MapF +import Data.Parameterized.SymbolRepr (SymbolRepr, knownSymbol) import qualified Prettyprinter as PP import Lang.Crucible.FunctionHandle (HandleAllocator) import Lang.Crucible.Simulator (SimContext(..)) +import Lang.Crucible.Simulator.Intrinsics + (IntrinsicMuxFn(IntrinsicMuxFn), IntrinsicTypes) import Mir.Generator import Mir.Intrinsics import qualified Mir.Mir as M @@ -73,6 +81,9 @@ import SAWScript.Crucible.MIR.Setup.Value mccHandleAllocator :: Getter MIRCrucibleContext HandleAllocator mccHandleAllocator = mccSimContext . to simHandleAllocator +mccIntrinsicTypes :: Getter MIRCrucibleContext (IntrinsicTypes Sym) +mccIntrinsicTypes = mccSimContext . to ctxIntrinsicTypes + mccWithBackend :: MIRCrucibleContext -> (forall solver. OnlineSolver solver => Backend solver -> a) -> @@ -127,3 +138,12 @@ initialCrucibleSetupState cc fn loc = (cc ^. mccRustModule ^. rmCS) fn loc + +-- | The default MIR intrinsics extended with the 'MS.GhostValue' intrinsic, +-- which powers ghost state. +intrinsics :: MapF.MapF SymbolRepr (IntrinsicMuxFn Sym) +intrinsics = + MapF.insert + (knownSymbol :: SymbolRepr MS.GhostValue) + IntrinsicMuxFn + mirIntrinsicTypes diff --git a/src/SAWScript/Crucible/MIR/Override.hs b/src/SAWScript/Crucible/MIR/Override.hs index 11826af349..0cee024cc5 100644 --- a/src/SAWScript/Crucible/MIR/Override.hs +++ b/src/SAWScript/Crucible/MIR/Override.hs @@ -980,10 +980,12 @@ learnPointsTo opts sc cc spec prepost (MirPointsTo md reference referents) = ] let innerShp = tyToShapeEq col referenceInnerMirTy referenceInnerTpr referentVal <- firstPointsToReferent referents - v <- liftIO $ Mir.readMirRefIO bak globals Mir.mirIntrinsicTypes + v <- liftIO $ Mir.readMirRefIO bak globals iTypes referenceInnerTpr referenceVal matchArg opts sc cc spec prepost md (MIRVal innerShp v) referenceInnerMirTy referentVal + where + iTypes = cc ^. mccIntrinsicTypes -- | Process a "mir_precond" statement from the precondition -- section of the CrucibleSetup block. @@ -1173,6 +1175,7 @@ matchArg opts sc cc cs prepost md actual expectedTy expected = where colState = cc ^. mccRustModule . Mir.rmCS col = colState ^. Mir.collection + iTypes = cc ^. mccIntrinsicTypes tyenv = MS.csAllocations cs nameEnv = MS.csTypeNames cs @@ -1181,9 +1184,6 @@ matchArg opts sc cc cs prepost md actual expectedTy expected = mkStructuralMismatch opts cc sc cs actual expected expectedTy notEq = notEqual prepost opts loc cc sc cs expected actual - iTypes :: Crucible.IntrinsicTypes Sym - iTypes = Mir.mirIntrinsicTypes - -- | For each points-to statement read the memory value through the -- given pointer (lhs) and match the value against the given pattern -- (rhs). Statements are processed in dependency order: a points-to diff --git a/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs b/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs index 1426e62f02..4727199da3 100644 --- a/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs @@ -422,7 +422,7 @@ resolveSetupVal mcc env tyenv nameEnv val = where cs = mcc ^. mccRustModule . Mir.rmCS col = cs ^. Mir.collection - iTypes = Mir.mirIntrinsicTypes + iTypes = mcc ^. mccIntrinsicTypes usizeBvLit :: Sym -> Int -> IO (W4.SymBV Sym Mir.SizeBits) usizeBvLit sym = W4.bvLit sym W4.knownNat . BV.mkBV W4.knownNat . toInteger @@ -967,7 +967,7 @@ doAlloc cc globals (Some ma) = do let col = cc ^. mccRustModule ^. Mir.rmCS ^. Mir.collection let halloc = cc^.mccHandleAllocator let sym = backendGetSym bak - let iTypes = Mir.mirIntrinsicTypes + let iTypes = cc^.mccIntrinsicTypes Some tpr <- pure $ Mir.tyToRepr col (ma^.maMirType) -- Create an uninitialized `MirVector_PartialVector` of length 1 and @@ -1026,8 +1026,9 @@ doPointsTo mspec cc env globals (MirPointsTo _ reference referents) = , "Reference type: " ++ show referenceInnerTy , "Referent type: " ++ show (shapeType referentShp) ] - Mir.writeMirRefIO bak globals Mir.mirIntrinsicTypes referenceVal referentVal + Mir.writeMirRefIO bak globals iTypes referenceVal referentVal where + iTypes = cc ^. mccIntrinsicTypes tyenv = MS.csAllocations mspec nameEnv = mspec ^. MS.csPreState . MS.csVarTypeNames