From c6ca304bf5af934e464caf0bf1cf9a44650d0839 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 13 Oct 2023 11:38:29 -0400 Subject: [PATCH] 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 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 557010 -> 556945 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 | 128 +----------------- 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 | 16 ++- 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..e7c72acbfc 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 languaage 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 b74bc4c0f4..5f0358ec82 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Builder.hs +++ b/crucible-mir-comp/src/Mir/Compositional/Builder.hs @@ -640,8 +640,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 goTypedTerm tt = do term' <- goTerm $ SAW.ttTerm tt diff --git a/crucible-mir-comp/src/Mir/Compositional/Override.hs b/crucible-mir-comp/src/Mir/Compositional/Override.hs index 73e8623d2e..45c1abec2e 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Override.hs +++ b/crucible-mir-comp/src/Mir/Compositional/Override.hs @@ -571,7 +571,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 c9af375cbb..6e78015c58 100644 --- a/doc/manual/manual.md +++ b/doc/manual/manual.md @@ -3142,14 +3142,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 cea4608664367c8e3ddfc0a35b21343de6c1c0a0..96431a316220b33f36a4afd5e9cce04018337e5c 100644 GIT binary patch delta 7267 zcmc)NbyOAYx&UxCn{JSlZj{fvlcfNDackVsw{(0AL-dWE(&&0dd%slhX$Te&HHEU29s1lPt3R4J@Aa~9KtQs4| ztyGi0%&-{VPr#X)h>B3`lfqcvvyKt7_UGCUZAx(*-(>pkTu@?TPal5mzsWM5_|XAI z{eps94*WbStGCda(ISbmf_>SDDJe zLl!$-n?u`Oh&|7miL%*glij#UfM!VMYv*0U3PrA>pWA9qblpzkE`Ci$fwwM7KE0n? zHNHbdRKxkg%Wd3MPzhqHc5Bw6U$nP;LoNMSHDR)+dDC}u(x)i*e4(Yzv;+7~StETo z!xLNju#Qq5%R<4zw7L0ei|w<#+x3u)UcAb(@q3;xUQuZfP0?Gvfdl6SmJjcXcRi^h zw(wqsywGf6xyJBH`A~A(){-YUDHa+aaRMIt`m>(XIXZwx!nN2NUi&G0rYmcvbZgrX zm}T$yf&ij1Zv(mIQSwv{MOBYFbnU^f&l8UG-Y>;pY}Li;BDFM;ORm7 zbt#FllX(V19(7DfjRa-To~16s1=E#vWLyd!vqU+;%bbJ+cb+UPJj~Rnaifqos!nOI z1r}9JztSR;ot$l++}_$P02D5Re{mk)-`sVVBR*f!mN7;ZqpIrtOtdg;GSv}A8j_{hOfSU9_#u8j%Lo8n6(@{Y6)s5z0?%x&V@!-M2c z**Rlb2a@&EMnD|%LN`kgt4>R*v4n?oT2YNLu*6uHHBMRb(MgO-cT9XIX!KE5trerH zwUsZDBQ(p_S0zsMmyhyD&vi;p+%*_ZV#hY`GGs{(RgHp;t&L6anOAP>QW(8++0CER z@mJs{;9-Md&@fi9S7BF$rbZ>4ZOod)_3#=JAE$z z3>J>jamBR=bHyVkeW_dRtcT^e{biZQZHyaBSY! zxrhvWJkU4rEL?0K>sjw1i+Dng7CfDdvVh|Os#_v~d+lxLM?l)lmdRO_8xTwbC^2dZ zIMSj~c?l`=5dliHO8u))HjNy^F70qNFxOm%c82IJh6uy4BZa}*mVQQg9Pw(BG*5kY znjf?j$!szpX9=g77t~@I{`re?gN#vaUrSiy$l6Fo-g){4*4H!JEGRRQ&zZ<>pET;u>@-@E}#auDD1(i*$LBg11Kpswt@c_>LEYU8bte{7$mA zo=*^;YGmg&t2HHdF9;btA!M5{1DD~+o)e|T)had5UE>1!?tJmAvv!4*YE4@O#K0!(hLV1%g%9Ftp{qS|u?N(g zh^s2jkChBEsYwESAC}Ak)!7NEYq+xUKrjR zNkYGzJ(Hs(33Gip_DQ4jwvdGo)x5EVD7_xGFJbR!gq!7kV>Oq@5vJq$f@M59Qr|;P zVybv!&OA&haV>KzRzc*i3RKs-f(^_&d(CEps<{JsTaeP|sp{?DLTF5B?nyqa}!EnVVsN`7Ld49>E)y_e^TafXCFP+aJ zSSKe!rxQO<)?dM8_p2?Rh_=bM3lxK90e)5Ayy}Q?p(v&G)0nzLujW**bQR=U#@tf{ ziP39s`PPnTL~bqbNXW9T8G8${%TFp&LmdMB!ubKwlUq}Ox0BXGr#y8B$yJckN8!&C z6Mj{Vp$5ym%wxym`3T#+gk`$?u0n#D2``&vX^MwWznq3&*{54S$cb|yyj6M!N7?-Z z>d6;xkf52ao6vN+v-aW&-HPQ#@I+4;|KVMEMTkoYi#V6_l^?hf9X*rWf2~SkN{qH# zUbgWeE{lT$WS^-NG7ywWi?(D4xgiXeAL^wQd1MtB$X)I)v4ZNG@JzaFf|p^ekDWm- zJ+*;;{f2K7aWwC{Ie;B=Xz^~hyC^#4wwT+&Dl#bopfi+aQicTnOK?{R&wKkN7j*pzX6&}@~gDu*Cz57Jlb^@Ut_P&6;pZ$q;cBp@l zqD*?46m8SD<_=}y1gZHm{V2!%Z#EIBoSFTflfF>e-ldKP0!^kbh-?*%6st0&ZDBja zILtHBA_+k`5ucwOOp^@FcmEizJU0m&Fj}1Fu3~S`Y+p(XS~eX6aGg58N$u#Cf_FMIPGh%@u%T^uj)A#pTm7h z1=ehJ(DWE1zE&}w@6w}NE4->z4!<#NWc5V=8*nk0?84 z`kmAEO((gS4=V0r;>i;B5w%B(lg6&Bm_wu^ErI-jz&=4^tH-oXC0`A`4oM9qtnKO8 z4YjF<#ed_5aq3Za7kCc?E^bbcqUI8n9-vc;M#SQjO-$aZB{({5agD(l`nvXG#^y1LYi_Vc1bxXm0Y^ z*aj1dYehlLA$}FKy-p@yuPy4AZF9Vs1@8pUekZ{TiUL()oCR|Hz32qgl6yt68vSfo zLMAf9QAPR=LHm&l2vLRv$B**DQ2l_({p$ykixUA*hiOUn3k}mO^T-eRhp|a2(}v5# zB9=y&DiBc{uR`?5HlNw%4z40ySCFiWEYdFPaF_gLyjxYT^LHnyGBXNKi5w#deYf%) zSnU~1%uA8-WD;1s{&})j*r@PufAiI7A2;RkiYg|Xkk#GiZ@p*`n=v3Z#rbjf>D6kz(Im{jCcj7AXKN_rj&A^22lQz4A}>89hDgf-Qb`nRk0L6;m8#XIr(p~2H;{%HJu$K9@{QgIK5 z7(6lz>5A#Wk5e}-N#d?OwgaEO7Q5o0eAfoWY4K$&5r=5(8h*C*ew=Uu0moIEo0$dp zf{Ya35TX_culgaH26rAIWnPxlHl*VGXg;kJ68uUM;1|0h$!NzD;^)fH)j;FUpn6u;d%0I9la&8Es_zq z=9|9mn~tj}sL?g+b5{t>!o!K9*hrp>?}#nLGXGjxKA!EveB#@)_ z;R_{OEyL7rziUYR%#y!2^caGTAb{f0gU%6LP&_Hn1B4~?W{e$_&%?LfZn?Gv`d~a> zydzD|mPY)u6{L;($Yz>U?&5&mjWV{)T@u8NqC|#^xKR(b`PO34peRhkdEKZ=+q`Q* z5-94~@cV8wJHJmsiXxW|=iZ}CZ}ap438JVP!zK2p=iB_xEW7bb*!ywegA)Kp;SQOM zjrfaJtto8o1{9xZ2&%Oqh7MZYs#J^fv8fI>Zc&Ix<({wzX0(-5aZpkj^+X#&*bPqv z2$Xu+>@&G!77gQ{ulh4!yu+m5wLjD>FGMpg0n zVZz|5c&s&DK?zG0RZextnEu;o0&NpHXWmCH*agcNf9u}tqm((H;X1Ldgoe&G+i8~$@LdG4Bnb_hSt->dVT6P&hA21_4-0?Ws*XiBAC6!5TTTYzU zt$MXMlPH|oFcUZWomR72+*1@tI!tAcHoaBH2WJR{-N-Q?S76O$!JXD}VNP^G-1rK% z$E5h-z?BmdA?<<30`Ox1!Q(ei&6dFxdC{3lVyGI)-8%*P!FamQ;Dgtiok3Hdrati$ zO>m~QG|@ou6gY{JAiC{OB4s%-lkjxe{yX@Z!r;uST^OjkKFZu9_bQVjT#dFcMaC*W zEHmo&anX zA2%r|I&K_~YR}Pu8 zein+RVZlf1*5<={}3`5Txc3LTQynhdWN5*I|fd!YUQpyu+Ye&>GY z%}q#CG6zsCOrqwpS^vNr^p3!E^SzASy@V4`>E)bf{X{t=HXE(#t?Hi+68HVP7!TLZyr+X-3pvne z0~=cV&qfIx0KityAwkgKUNKT@-XxwWTS;vF!MWb5#j1t8Abe#_8Gdn&cD}q#!hFZ2^WDgjVFmA-SrsdBn2MfX0++$#L1ejnb=t#&Vn& z9l9fPC#sFrAn`VPw``GRWe0oS=b_tW;1}%zwRryUoy-Esexj{cfo04jt#XoB5hy%{ zS2k`8TCzl^l(m=d-Ot55Nd`NxYrzQk4jPCCbj<&yB&Vm=rffB+p3cvoP5)JvYoP%I zLyJ<4L5Mv9^A36+!rjFO5HrbuHm_mqnh#2(%E2ok|ADpp$YsgGYtNJ=>-_U=L{>9PJCt*$9D@Dqp;KO!eD8Ne8Md@ZDy;;ah5QZh_wFA(ABk~x z{{6pf8;)F_WS_mRgBCb)!*?c?m&BwTS3e|$>XR7%EvPCQCh%^coPvJ;7w=r(x#Bxc za?i<}Jw+nV^l6RjP5u>7Z^Aj>Z&B1~0{;h{NhZzug)=K;=tlBC>6h0;HLW)O9r60- ziNeF=9q|(3-z?yWag#?#gJ6+)JFL)4YI-T-s^uTD)~jo~s7l zrI^8h|7nnh^sqDrtljqCANa;%IJ^XWf+1&-S9{{$R!DS7A28E32p>h z9dwd}LyJJbNQq#ln_wGNEy3jCz1g5tH$vAA##+MD#hcI3&6L2rRsGzab=P;~a#AMd zR#QmL9?3j-)Q+3(o$)F=r`_t_r;EH#Sp&YRu;2Q;{z1P_zt2)ikZwad8cb$E@rU=J z9!kQ(*Pi?2F9*EKn0k5pc>56EzIdcSAFuB}*w75y+pC)YC%(!@gHr)-m;(jqjOv7x z0Va;}#7_9Y$b^%siM+Bcyw;~Peh`*gmCssS!IYaHyO7O!_qQ*aNhKzw0JWwgny+J-ncU;N@Q zy|UXAt;UA9Ot&=sHAI_0;_X~hL?)KEtJ}q=Nba+|h=jGdPJ#0*p~4=PRzv~JTM=M4 zGLkkcNlXoh3H9f^U}}g_&_U+6T~2n3DQalSc>o_BI=5mt zDby6};5!80Gw2NYp8$u*LuqQy88rII!BlJIy2g5{cR}yQV4n9zpVZI;1NtY)w=#CW zNC|nsHhh*&FmZc+3zYKg;tt7a{-nTEGClnrI|cU$73Sj ze!QqJHSSfq+fqPZ!DWDUF%wH5GN>sCmlO%p0Zv%0sUJUHf^Ii{JJ z#ET~K9~%PWw}DqebDYM@kjw_dXVhON%yL%IPoc3p^87POO}_Pnm206BEXMof7W8M2 z1Y_43LeGqmvq3nqlhN^|-(oy(9)o(Vc@yGiUN*AuIg`9+IZelqT>9(<402zYA_tjr zn)tYkdTh3XwGZoU+JbD%ht{J7H1QHvO=)EDajLV#8!+Pt*_HE^w+EY7RdA64;WUv2`gY zO>z?b>-jO=R?p+y>c_B!q1^#F3-MnV_6-zp^IdR6epz)4YGV^|s&B zqWgSgp600e!>L`P;Bw&pPLHzM^H>r=p!*>@k9MKob|nv>EYVZlEz%h_PCL3ndkz~X zyfMG|6Rqm|G5IiZqTcqXp@pgBxNm9;h@8+BK1pgCo__l#@K=|ki$=HLrEjG;=koR5 z!0J*lu;ktfnJdG!w-nq8y>!DMX=jxrLKH*sQ~=ok zamwqLy!&+jKSch|%YHAhUE1Cy)eG2hTE7O_wmp+Y6aaY41j3RK0!~h)$I1l%1xJtl Ap8x;= delta 7339 zcmcK7byQUCx&UxW8l<~nK)SmnhX$ovB?N&1MnYl(BApV0(kUI1(nG^YC?O)<(%o_K z^ZU;E&bjBV`_H}WH}9Tj&-=W4X3gH~SvyXQ*T_(&`e=>1-ecU|?@CsB7ba2J@Z@g;KGYN5hubFD$V!-=a_Ef*R$&52U zXrZnv2ETl2J0CMd{dv%(`a5)S5%d0P8OMW*NkeJvYdV)&=534vRC0wL zf6pgiI-|Q-JUBjvk;mHvT>=+xBBZFkeO0tBc(fJ#Jm+2Crs=Hqy&qNVQX$1oXT_YM zRgM?;&M~q&(VWKTkwb`LzV1i2#ay?$A2vFNPchLCL{mG`vh9>CcvP*|ar#J3(4Tr) z$-n|5QK*1VRS^$K?MiA@J0IKnPS}mlfT~=Xvg$eU#r%hHKlm)^jFU#wamOc1UMCPA zR}PNyDw6nUkbyO%V!V1aC21Nx+(+-v7~#gozXf*~vF)6H(ukP$D3vhE;HMtQc}2=D zT{R7^Rq~$yd7(W_*qp2utW3T5xU_U*0_K>ofIb4CRF6Kux0?CP;FCpLD6R9udr4|7 zWNJ1Q6~_jQ)FJeoq@6M<;`LmICD%S7@xl_T0X&vPoHCS2Er6l2$S57umy$RUzK)X7 zH68_j{;og-Js*CPaUnWJUudbEJ>kE+!ki^mf9GVEFY;S;=9OJ zd&33$)K)!@WVGmqAs1&ZOGo=az-YEcSLik+*CMU!e#}(b)cfy|b?ItMoYmX3wLT6m zg-Ym3%lPv-xgL3SSssu_u0*owKAZbvZ$(j3h1+qn*mN75AI2+F7=##kXJFh|jCLCX zNfPdTOTZ*!tn6*v=7T7`r`jCnd0Y7S4K*i&jJ4Q?+D;Ey35dI~XgOKC)l{p@<{HmF zWi;K}N!zqo7oRID%zV_gW;60u$Qau5IWo+f(3OQr&)&?QH26$qTD_lRlw|kAv+9vv z<0?kUs5Fd#&Wv$$Oxm^M#WP^2Y)Pd7ARXAsZrU3}IsQ=}`F6_FqHP|WYe$}c+CD*v zrsXhA%t~rc&NKB<3F&%*iM47W9!ADk9ZJHMfr(3)W<&_3=m*8Jgw_BuNJ2_D)Jbhm51m zvYx6MMO>j3&g41$Fdp;W$qvF0_k4gZS|1|y5KU6mZfFJhgrPl72RS7@J@5R}mX0#A zi0Gky2A{FFAmfeyH0(sN(@6#b46o|(Y!=6@cZxN14Wt*<7r^pAkVwRQ9LZyM@l-G3 zkdjNzQ(QbD;QxqnhBPF%Ng<#{r?s^gI?2pTS)exT`HI9xN-dutdt~1?-j`-dI;=6k z_o(kN6I;Mp&dk%rDZyy*xuwUud@K4WWn>z%yTwg+Q_9S^q%d}zm-$WgZ}!9G<=;nv*T&T`33gZ$hFky{3;La<3g z&o3vNrd{mC?Y0LTe4vO`gJncQhZKx+)njcVkGAKVmz}vm`Iw;qR0c9opTx;MnVUGF zBiUqW2_rZ-WhuoWpz&aZQ~@IO`>X_sW97OGc7 zeKAa}e%xjJV9zPQzkc)uN~A#261V-F zQPbD3;a(+IBm)UkIs)C4_fQKOuLY&3>25rG&Ik^?W6uL)3$&FC$vz^Z@- zo11LZkM*KrqAT!k=RfCFe#W!zrerO+`*iw-^l60UMdDUbE|k!*4TK5LdZHqiO!r3CbUc#*h^5!nDUxCqO#WMm;N{cIF2`CKMNw9yIdCr@)$D@5By*U)4PVIci})duHouPuJmlxnE${aUzB>8O8}b2H_zFJn5c8GBvzc)j?^?#z z=jj-}Xxj;37Q?k>#*o z4-~To2Aff9jUwl9nfiosNG7T>45~HW3~v*B;Cn1V*V#O$pf>wA($;ykB9_9pVN%-f zJGGOfF?b1;A7)M`J=Uf8Frjo?1kZ<;UewXeoHKhgrkppD7ZD0v;&I{Sol40`Al$vI zwzf?Gh6g<~dcz1hVoHI)H0+L{sASsi_o2wPCst&k=%03ERauqFNe8L8d*AlWl0J}F z$y9_$?l^~E6SoLS*Ru_Xreb@`v*LVXJB%(pH>pz&?=`4QP}OwcJBv{buuQ`x?;bSa zaDouWgu3y3i5bd!fH_)!&#c1@Us0=K`VFTGuzhtpA7FaelKy-tYERHL{1qrDXGqe3 z?)lSbmEiyzEE@Po)R&@F_4;aPQ4>9Z4GAhrEwXEJ_)we5nNr6%Q;E%om39wsXcOaL zV^vfnsHL;Jtt6W{r?Tya_SUjKlzfFYgSa9?Jl$7OS35(Dfrz-E105WiEhm}2m4%}U zsJIhGloqdj(L~(RVAd=b)7j@9zkuK%UiKJ3yja*QpSaK;I2T5|`YhR+q5p=j(1AR+ zrqV$^xHjE9nuhkck0*JP_(aU4Gzc5}Jp1ugBX?UHIYRf_VP{$kRrI*riTWvg$cD-t=e}DK)Twd{df;yR^iL9rG5xQ;Q1j1O zw{z%jUApF!BKhiO?jQQ$9yUUK=X;rYUjZ#qKMD) zYp-}MRZ8%1t2GkFr8TEIaWzaf#>cxw$&u!tnql5%>|^*pZ&ZVm?J0cX20aNJ1BqQSJun-9Wn=_wELI{X#NE@Bpfapa{&~8k6ByP#W(-MttYB1mD8?83T1dQVusDNo7iVMmZt zv2bKxkz?hMgD7(4bxUR&S^u`Swe8}1iFB>C+s5=SzO<#G zcr#jdH3`s@D{mFf!1GEZvJNIATy-mUBCgjfl_&*Ppwgi6O7w{i38VY4erHT-WK-CR zGp0DQIE>x}lZyfVY7+Oy0_$|p>fOd z*hD4qK1+Jpt=!`oM*p4{TLI~nI3AtG4QQQ#p45V~F9IVWcp5(L_vzqIDPo|{Y|+R% z-HebQ{rYa$z6+)x;4SXo>h*2WJkpbUw)S^G%T8y|y`Sm(^lPxv@z%@2yI&geNL0d) zXsCk}(T8S)Y%RNLVg1G538U>gY`f# z83~fq%gh{B^weMYfqv#8p2)$lT`{R(HxNuJytb3WSfikh-XD2~?|5PSu9zU^gG<*D zcB3?C>)!S{PvG639n(3GH+rkp+=Ok=No9nyX(bKwcE#k^m2ISCmd5%pFO(Ko4Z$Dk zyw`vUn-?$(EP>#acj7f*)z6De2R1?O?{uPiVaCq$O9g(|!_DZ#@d7u~KkC+K)sg^C zPWksl_sC}9J_LaSO|WZMOa>rat`_O)oUCaKVy3yWq(+$6ro9XePFAe1D`$4olma{mZ~pSl&6sTQ4p(p>;ve2(9V z-B)+1xca^d6dYA$S^+eV-E{ipK^RGY2EgyA%F@*skNgdA87o%t=jDGd|COt6h8&z2 z3SN_KBbp-(QKR6nE)32l`W;vVAsJT4qj3-xDrOM{ZoFppWC(PAdo>2Ae5>tVwtvfF z8MQ<4BA}n;-Kp&U6io`wp_L3*z?(`;vQ8o+Y=jjcUK+q|gjHfCT#EcnDB&i7O_a62 zI5V=^iD@@w!eA0-6#Q`|b8*ILe$M}E+jSmr3BEl^@M*7YUv`>=v4r055k2Wd7Q+mk z=c5VCC9spkXPak93mS!>n`vldygq~=o2h6twx=}X8qRYx)TK1zmrJqkb|^F?u&l|_ z=DGo2_|IwRK>gd*`|lC4Lgf^eEd7z0pRd)u?o}+{HNWxPqbt<(6U!Ib4vHME!N}!H zX34x#@(qrKGJ$2T85_&hM!^i?>5e;^Mg!1)*Es#{v!$BbFO7r+Zpp~Pff0gAv=FjCKL@CYdE%7bsqEXgmyx6)2QG6 zH!IU&+PP_|N#KK};cmXq&#EQBH>-+JurrCrl5M_g^;aVuDr% za|@^!|MXMhg_z57zU~m-<(-+|2En@FWG;h0SK?xQ)}uMp|q969&n|}1nB*;*xb+U z7Lyp43rIA<3J{8zc3m;_-UYNSh<4zQ3d(v*!L@lQvj9m5`_GKqZ-Cf}O#_PI0+m@P zHH3KQQ+Q;5YbtbiJGx>f6l0IzuAGKl_WW58uqx(-n*;0j@Mlp+-*l2|kefqrOpdHb zRC)d^vcjb2n~KSm2N84kzaYk@~o>C!`RIh6R8-INRuc8u<=@v-ltE zv!5WXDZSX;Gf2670tj50hUr#WR{l3#y3=vwU4Qs!V1_b;^M@ZPqYEuxc>UOi)O`s> z4-fPTe=@nr`O5zt@b{Cy;^x$i_~f&{cyRsnzmD7|bf44vqQx>Z9NXpSHZma3iBU#V z^Dlv;VJ_*02Ycn*$G;Jn5ttzwDOYc7tLE3z^5w+kp7}d~d!~%YWu-!Yk-Pu5vLeS= z))`qNx;3jtn}5*XDtqE0{%<-zmDX-F=QlPhn3;U(@-00j`gw>zruH9m!SGaf|`t^F2jlTv5 zLO2B1xe~SLqTaMdeG#l#NmNRi(t{-~Z0Gr1)d*cY9b#B*exL3b`KmEpM4~edW*bAF?KHsl8 z?o{gM4Wg|#+yZXug|Qp>^J79(DX_u}vRT=yxC*t5;aLOC{9zRIn<>Z?^m?WFS>B-W?uuO-`C$b4-Z;&?#_;vVKE}%cyY%xuJ=IZDCpA3i1Ql`f4=MICI zA7w^-$;1G2fvT22*1R+!`j4huxsC5^wB5tSQXR71?Jk^n; zOF;Bpf#@Vl2`Q_@tLwxMGhZ~Xq&{h9pG=LS@uEPT`>Q+v|ELdA0i*qW=k(pWOc;L@ zh)4()Pp5tZ`nLu2>0na`^-jBa1IFpLU1&sTe_so#YmUku#jl zz7M=#SWUSX91b=E zCG10W{)*vKyGWfeinr+Qde+$}kl1S!v(Y1O!z^3Q>G&yN*?AG2A0-f>y*coVhvOVD zo}nloSzdc-BMM8q%5lCD+3)Aw9Ppxx6))fDQB-~8Z*IuF%#<`Y7HynRa#dIUzW)tp zTS-Zb8x~@BvxnKpdx(Cc=czG2f__sO{~0$>T*BiXh{)Uw5iLS&@8Wmludke(V>n2_ z+OEo+*U37rTAUTFQo5>U_l8-0mcIj&?L8X2f#v1YO|zIsP?$q>N6HRSnQO|3d8sgt z?IzFHgR4SO70>MC?VMSunR_OO@{R;$XJHk1zIo)m?lJPd+*;0ZsJ)xrs)p-5;ssXu z(!n?A@p`1IkYMwkB%DTKsY(S*E~n;CJv!MQ-`hr6wk@ z@ATbHdcb78SN=y9wQ$8RU3iS9YZFZb_&`^Q!x`7c>5RmfzfZ_xGqQdX?~OO6R!+pMA;2 zc;z$!f2h=yK(fW>IOEOUvnLXou5;}^tF3cj))Vf?Ubw$*W|_?E>$9Sk{mS(dM#`%P2i&c6>6?mZD+S zKmaTC!*l?yJnptyJW+D@m976%=fD*Lsw7Egd%X;NtDq_ z(mJ@uB(kJ6`BsQDAF7Wv{Z=R{ga99IErz19KtU5q3?b5jKNmx_TcAk`y{qs%@V_+( z&Tzn~0o8MXZu-yezzaotfl?}ze2>Ti?&yW;vOwF6u~?mbb}FmstNj1r@&Ca^JviTa iU8ZM8WNv%j(D$S|Im7G$OnPiVAyI4)NJ(26`@aAZ>=_yW diff --git a/intTests/test_mir_ghost/Makefile b/intTests/test_mir_ghost/Makefile new file mode 100644 index 0000000000..bc6297ae15 --- /dev/null +++ b/intTests/test_mir_ghost/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/test.linked-mir.json b/intTests/test_mir_ghost/test.linked-mir.json new file mode 100644 index 0000000000..238971f5f7 --- /dev/null +++ b/intTests/test_mir_ghost/test.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::53e788cd45991c87"},"kind":"Constant"},"kind":"Call","pos":"test.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::53e788cd45991c87"},"kind":"Constant"},"kind":"Call","pos":"test.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::53e788cd45991c87"},"kind":"Constant"},"kind":"Call","pos":"test.rs:8:5: 8:11"}},"blockid":"bb2"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.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":"test/9f9d7d4c::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 !test.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/9f9d7d4c190de41a::{{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 !test.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 !test.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 !test.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":"test.rs:2:20: 2:47","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/9f9d7d4c190de41a::{{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":"test.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":"test.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":"test.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 !test.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/9f9d7d4c190de41a::{{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 !test.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 !test.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 !test.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 !test.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 !test.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 !test.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 !test.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 !test.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 !test.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 !test.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 !test.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 !test.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 !test.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":"test/9f9d7d4c::next","return_ty":"ty::u32","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":"test/9f9d7d4c190de41a::{{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":"test/9f9d7d4c190de41a::{{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},{"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}],"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":{"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":{"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::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":{"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::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":{"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::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":"test/9f9d7d4c190de41a::{{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":"test/9f9d7d4c190de41a::{{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":"test/9f9d7d4c190de41a::{{alloc}}[2]","rendered":{"element_ty":"ty::Adt::613f1953a8669d14","elements":[],"kind":"array"},"ty":"ty::Array::0e1a52ee2b2d3e97"},{"kind":"constant","mutable":false,"name":"test/9f9d7d4c190de41a::{{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":"test/9f9d7d4c::example","kind":"Item","substs":[]},"name":"test/9f9d7d4c::example"},{"inst":{"def_id":"test/9f9d7d4c::next","kind":"Item","substs":[]},"name":"test/9f9d7d4c::next"},{"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::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::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::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]"},{"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]"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::FnDef::53e788cd45991c87","ty":{"defid":"test/9f9d7d4c::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::bool","ty":{"kind":"Bool"}},{"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::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::isize","ty":{"intkind":{"kind":"Isize"},"kind":"Int"}},{"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":["test/9f9d7d4c::next","test/9f9d7d4c::example"]} \ No newline at end of file diff --git a/intTests/test_mir_ghost/test.rs b/intTests/test_mir_ghost/test.rs new file mode 100644 index 0000000000..fafa13669c --- /dev/null +++ b/intTests/test_mir_ghost/test.rs @@ -0,0 +1,9 @@ +pub fn next() -> 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 17f8f73d2e..19046d21dd 100644 --- a/saw-remote-api/CHANGELOG.md +++ b/saw-remote-api/CHANGELOG.md @@ -27,6 +27,8 @@ * The API for `"struct"` `setup value`s now has a `"MIR ADT"` field. For MIR verification, this field is required. For LLVM and JVM verification, this field must be `null`, or else an error will be raised. +* 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 bb6f462977..e91b9249fc 100644 --- a/saw-remote-api/python/CHANGELOG.md +++ b/saw-remote-api/python/CHANGELOG.md @@ -30,6 +30,8 @@ * Add a `proclaim_f` function. This behaves like the `proclaim` function, except that it takes a `cry_f`-style format string as an argument. That is, `proclaim_f(...)` is equivalent to `proclaim(cry_f(...))`. +* 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 7f051c5fe0..f8176fce2b 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 e2b5942741..152911fa71 100644 --- a/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs @@ -30,6 +30,7 @@ import SAWScript.Crucible.MIR.Builtins mir_alloc_mut, mir_fresh_var, mir_execute_func, + mir_ghost_value, mir_load_module, mir_points_to, mir_postcond, @@ -55,10 +56,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 ) @@ -71,24 +73,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 () @@ -133,7 +136,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 ed3e3d92ff..98782f6196 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.Except (MonadError(..)) import Control.Monad.State import qualified Control.Exception as Ex @@ -132,7 +133,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 @@ -158,7 +160,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 @@ -696,7 +698,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 () @@ -2474,3 +2476,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 3f78ae8d85..f856318673 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(..) @@ -61,7 +64,6 @@ module SAWScript.Crucible.Common.MethodSpec , setupToTypedTerm , setupToTerm - , XGhostState , GhostValue , GhostType , GhostGlobal @@ -117,6 +119,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 @@ -131,13 +134,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 () @@ -323,21 +330,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 b96b9b2ad8..b9ecb027a9 100644 --- a/src/SAWScript/Crucible/Common/Setup/Value.hs +++ b/src/SAWScript/Crucible/Common/Setup/Value.hs @@ -50,8 +50,6 @@ module SAWScript.Crucible.Common.Setup.Value , SetupValue(..) , SetupValueHas - , XGhostState - , ConditionMetadata(..) , MethodId @@ -176,15 +174,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 a3920359f6..001bfb0b78 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 @@ -67,7 +68,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 @@ -109,6 +109,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 @@ -412,7 +413,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 @@ -432,7 +434,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 @@ -537,32 +539,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) + ] -------------------------------------------------------------------------------- @@ -1418,6 +1431,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 c6a82d9353..33aaf9063d 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 @@ -605,32 +595,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 :: @@ -641,9 +605,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 ------------------------------------------------------------------------ @@ -716,7 +682,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. @@ -760,6 +726,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 @@ -799,10 +774,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 edf3c80581..7c77b15e1f 100644 --- a/src/SAWScript/Crucible/JVM/Setup/Value.hs +++ b/src/SAWScript/Crucible/JVM/Setup/Value.hs @@ -86,8 +86,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 0977cb7570..3f109de81c 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -184,6 +184,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 @@ -1201,7 +1202,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 @@ -2795,15 +2796,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 6f532e0f45..860d1e36db 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -86,7 +86,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)) @@ -116,9 +115,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) @@ -1071,29 +1068,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 -> @@ -1174,7 +1148,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) @@ -1342,50 +1316,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 @@ -1401,36 +1331,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) - ] ------------------------------------------------------------------------ @@ -1549,7 +1453,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 @@ -1975,27 +1879,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 de4b0ff143..5102861f10 100644 --- a/src/SAWScript/Crucible/LLVM/Setup/Value.hs +++ b/src/SAWScript/Crucible/LLVM/Setup/Value.hs @@ -129,8 +129,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 5a157f1865..694c3a4358 100644 --- a/src/SAWScript/Crucible/MIR/Builtins.hs +++ b/src/SAWScript/Crucible/MIR/Builtins.hs @@ -16,6 +16,7 @@ module SAWScript.Crucible.MIR.Builtins , mir_execute_func , mir_find_adt , mir_fresh_var + , mir_ghost_value , mir_load_module , mir_points_to , mir_postcond @@ -75,7 +76,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) @@ -110,6 +110,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 @@ -226,6 +227,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 @@ -576,32 +584,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 -> @@ -781,7 +800,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 @@ -802,7 +822,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 bdc16e255b..117a828f83 100644 --- a/src/SAWScript/Crucible/MIR/Override.hs +++ b/src/SAWScript/Crucible/MIR/Override.hs @@ -62,10 +62,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 @@ -113,22 +111,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 - computeReturnValue :: Options {- ^ saw script debug and print options -} -> MIRCrucibleContext {- ^ context of the crucible simulation -} -> @@ -222,7 +204,7 @@ executeCond :: MIRCrucibleContext -> CrucibleMethodSpecIR -> StateSpec -> - OverrideMatcher MIR w () + OverrideMatcher MIR RW () executeCond opts sc cc cs ss = do refreshTerms sc ss traverse_ (executeAllocation opts cc) (Map.assocs (ss ^. MS.csAllocs)) @@ -275,10 +257,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 -} -> @@ -624,9 +609,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 :: @@ -647,7 +634,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 @@ -812,33 +799,6 @@ matchPointsTos opts sc cc spec prepost = go False [] MS.SetupUnion empty _ _ -> absurd empty MS.SetupNull empty -> absurd empty -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 @@ -943,13 +903,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 dc173f5d97..bb1f486a3d 100644 --- a/src/SAWScript/Crucible/MIR/Setup/Value.hs +++ b/src/SAWScript/Crucible/MIR/Setup/Value.hs @@ -77,8 +77,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 7360ca5f39..4e1816abd6 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -3623,9 +3623,23 @@ primitives = Map.fromList , prim "crucible_ghost_value" "Ghost -> Term -> LLVMSetup ()" (pureVal llvm_ghost_value) - Current + Deprecated [ "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