From 8583a6de535d32adfa8099b296df9a16bf0ac455 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 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 587257 -> 587241 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 | 14 ++ 34 files changed, 467 insertions(+), 351 deletions(-) create mode 100644 intTests/test_mir_ghost/Makefile create mode 100644 intTests/test_mir_ghost/test.linked-mir.json create mode 100644 intTests/test_mir_ghost/test.rs create mode 100644 intTests/test_mir_ghost/test.saw create mode 100755 intTests/test_mir_ghost/test.sh create mode 100644 saw-remote-api/python/tests/saw/test-files/mir_ghost.linked-mir.json create mode 100644 saw-remote-api/python/tests/saw/test-files/mir_ghost.rs create mode 100644 saw-remote-api/python/tests/saw/test_mir_ghost.py diff --git a/CHANGES.md b/CHANGES.md index dbf13e439f..d722ae64cb 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -17,6 +17,13 @@ generating LLVM setup scripts for Cryptol FFI functions with the `llvm_ffi_setup` command. For more information, see the [manual](https://github.com/GaloisInc/saw-script/blob/master/doc/manual/manual.md#verifying-cryptol-ffi-functions). +* Ghost state is now supported with the JVM and MIR language backends: + * The `llvm_declare_ghost_state` command is now deprecated in favor of the + new `declare_ghost_state` command, as nothing about this command is + LLVM-specific. + * Add `jvm_ghost_value` and `mir_ghost_value` commands in addition to the + existing `llvm_ghost_value` command. + # Version 1.0 -- 2023-06-26 ## New Features diff --git a/crucible-mir-comp/src/Mir/Compositional/Builder.hs b/crucible-mir-comp/src/Mir/Compositional/Builder.hs index 0e77b644b7..b8271368d6 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Builder.hs +++ b/crucible-mir-comp/src/Mir/Compositional/Builder.hs @@ -641,8 +641,8 @@ substMethodSpec sc sm ms = do MS.SetupCond_Equal loc <$> goSetupValue sv1 <*> goSetupValue sv2 goSetupCondition (MS.SetupCond_Pred loc tt) = MS.SetupCond_Pred loc <$> goTypedTerm tt - goSetupCondition (MS.SetupCond_Ghost b loc gg tt) = - MS.SetupCond_Ghost b loc gg <$> goTypedTerm tt + goSetupCondition (MS.SetupCond_Ghost loc gg tt) = + MS.SetupCond_Ghost loc gg <$> goTypedTerm tt goSetupSlice (MirSetupSliceRaw ref len) = MirSetupSliceRaw <$> goSetupValue ref <*> goSetupValue len diff --git a/crucible-mir-comp/src/Mir/Compositional/Override.hs b/crucible-mir-comp/src/Mir/Compositional/Override.hs index da5d4ce55e..ea63c2122f 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Override.hs +++ b/crucible-mir-comp/src/Mir/Compositional/Override.hs @@ -581,7 +581,7 @@ condTerm sc (MS.SetupCond_Pred md tt) = do sub <- use MS.termSub t' <- liftIO $ SAW.scInstantiateExt sc sub $ SAW.ttTerm tt return (md, t') -condTerm _ (MS.SetupCond_Ghost _ _ _ _) = do +condTerm _ (MS.SetupCond_Ghost _ _ _) = do error $ "learnCond: SetupCond_Ghost is not supported" diff --git a/doc/manual/manual.md b/doc/manual/manual.md index 8769e575d3..79ec0b8deb 100644 --- a/doc/manual/manual.md +++ b/doc/manual/manual.md @@ -3544,14 +3544,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 853622bf380bbb8e5fd864beb239981ef82c8e66..4f4626e54c36d9ae88d8ee96733ebb1ce0e6c26a 100644 GIT binary patch delta 10280 zcmchbbyytB_O64wyF-BBo?!+L?vMaMf({T!(7~O?A-E(!aDoMg5ZpaTu;4yOfZznz zOZGndY&qw5@BQcA=k2cN>#wS-XP#P9YfWElGj44&`UN3;Mhw{kh(4Ta)xXvg`ziT` zpgNG3V;7DjW$2A@oS)^Bb)hd;zr zjiiFNZd`AJzZ__eP&=DY&EqeFAv^^u*MX1Qe%x}xl4rDnNIMfMPfM$u~%(&eYs285g@=<+8?ggi{<3VrFH0&o&# zmosXisPYV$xj5BYH{5~0z<^2cGkXBSn_%6uC0MNE0g>BQ=6A1ZeQ~asmsJh z?SzG)1vBLprA;jkK3?J~^$X(IR6>Zo)nl|Aae~uFRMm}H7s>i=GPSB+rg&O)DRsHJ zvMup!94vFE7TizP-W#jMlDr&1zD3 zppqxgChO#!EYm`kixIK?mb{jE2yr)d=GUmT=Ev)2&S>25AH53MwIIgTdqeqjD74|k zrPJu0_yeBw>^?C!^K(oS4WM~T-|Mqp-;I2l*^4VP{60~qhF;aGy@fO!EbnZ|f-F28 z_9$-(xf0}gK7>OA#I-dde8FcX(NV~VJt8W6KqInsw-lLA?9o9t)NEVkn? zSyLoO8vFGd_mf!Unf)_g<&RUM`h3&Nb?dkcqVV(F85kED=U_pF-xTM(j+vZqMO&$` z%)S0XGf5Qu_}~k@qEc+YaGAZTwgVN;>$6Drb588eVw>2PuZWxCBav32_^fsd{JI}+ zUTf=XI$k+t>Ui7CHf#e?-8npg(~V-f(?vTT+N+yF(WjfGgW0cUOSma}XO~4#u?sYx zb&jY%EHH*W$-9}z(^`&8$%MZ4Gz8O%uYd9J}`$tQ1|7BfrhP8z*!VNZw? z8Z3Ct|MMAYGl6C@V59ePBq;Q272!(n%4VOIW{o8Oj4%&0sRM<6BlUx#O8UiU0%Iz2 zr8k6r=rH}ze6%m2{ZT$h+-V)nKdqO(kVvi0u*F}wt3$SpcFjd_RrWe8=l08}1{_}fenothIN6FPS$cOeCItE&4VE?4;N8$y1Sba9sXX$NV zU4j5RLshu>$__7o77Y@0%i+_-{RgQdt*d2MlB}=JW*Ym*7-&UJ7e8;N)_-gG+}2IA z=`i{LPdLS}Q;Hu)O$ucM701ncB}~*p-JPa1q_BD}^DRn5GCYW4a?>dNSd&=lN3Le~ zn7zKE6;xPc96)v#9}mFu@$mT(5I7ftA4fO8mQS15h_Pmf zKo?B46up|BdWg}QXqAOrKvk2bfaAn5NHwf$h$-=Q=w|)pH)seN0YjVSfQ2B98!ym@ zAw7OIO`JvfuID2qoJI+}YeR{A!$hqjBb$TsY^rs?4%k0rgWW`DW51SC!r|*moU!%L z7FSSQb%t>dzhqZL1{G&;>3(NR>K?A8i!WBu#m9Kt^#DyavcH*raoj=r{V4_D7yQ71c_RLKJ_*P1FKe z=_wc^o}~!V?Z;jts$phd5J6UEf53^1yxCOid}Rs;qm(r7nsKXk1cL15lY z-{Otk#MdM1d@*0!9iE9!aZMfOqPqU#sf#_{hLlP!A?sp}BIPt5O6prP#H~8F_vit% z1~4x_z78VnbVni-kWiPdlx8h{_%}SAnC(220x#Cdvn;TMmBa)^!83Q&k@@Pkk;*N7 z6)nIa+PA1%7F~lEZ58DPHub&EW~5#1an)|2?ZLQxPdcSF^GpQ!N=hkB%jw^T7<5ji z`n+H7*~q2vzQS-L5IRUZ+QF#>5=7zar^?PzRZ1}>3<5N*B_nBUTnS&M;h zynU!Z(s5x8TvKzi6OLOhT~2rUJ$NdA{5o;3NW85%QuJGXY<18)U~f>6bh~^V{DoBKx5{~zQQN>W27a!CeKw>U0LjlSJ9@d!;@n4 ziq_FsraOvODbd)JweDo&i3d|5lYU;SNh3|yIHmL` z1b))QoRJ6n7&b7X8`|+@yrL%pZ3JgZn&XJRYu63%q`Yj;>oy&UAq9-qbLjc{CaGq? zi4703eu{Y1edXJ9;PWK{!y`Plpj(F4o95y4qexNzydLIE`+Q2}RTm{Ik4>T*-v#3a@B{%B}6epCJX31h((25;hTn<5Z zWC02RB)6Caed{c7bWhv^%y~%4#1p?MpK7f>-*RR4$)+C-Y@??x7EyV3uKqDYv8vK-X47t$NZ?yy@>Q8G`Loh)@}Bbr~4*%T z`2J?dKs=^*HHuA^%s_>$e()&MU}|IMAsp=b%9>2oMT=z2ungHhU^Q7bELtc$mf9^t zl3wT2w13pt8keb#BB=X$we&=_E+F%&jKrt8v;NhAl}?~g!{YM<18gm*aHq>FMQ1{~ zjsRq@$|AM4XD&wtAIlh$vKqMc;Cy^i+1z?znJPs{5O4rq4_cZQ8Xf11py)f+B4o1Q zV8V-U4dfQCYzpQp1ZhR^mDm*X_KEhW9wI~b>fwVFWe@{;MS79>(%~~KM1Tibkx-3U z+RBO)w?R(Jq=w@Tg@f>M?ifAEgo}I@n$Y+IMM6c8)EKWM0oywaR94W$OL>_hGll0a z-OtpD0%Hsw%bqW@9%fU2v|x&hr2#QhVo9k&l+cqr2|Xz}&)87{FuyPql|5lED(3FZ zYCwJSJajDFu*5GhGA{)0ARb6~vG?&=5Idn{QPBYRMy~Mr7b^;s1U)XstwAdaIRUqc zcKNux4-e?_{5dMZ;uDkE+T`E;Y9j8Rt$qK!#a;=u%UjM8YwsDle07-C-HTr`G_z9P5L4iC=(n0W%!M-(OFpshMOdU@GFo_Hv{~{b=2iw2nkvI)|Ws znbSiIq>@N=w}nIH^QKj&tD0zu9iAk{5*k}nrf zh@(SUI={ggXxk1eyF!9uKBdhqM>IMMzs6+cNSk4n0o2F+M4G%o?cWauW{&oufW5jH z_SMfV8w1?X&i&!c{(U_Af-TdVZ@f)Hsf$J}M?Vi24$jxSMfD{NheA*KBqYiz&bI@}$7_-CA{-~OvBedUs*c%S z&;Us;!wNajqP}XTElUWQ(W#CNy2HmGdWF?PYaNjF{z&aRZ~KFw3!bNUcSA#|8_Q(s zV^o$b(H}MXCp5A6pD$g^%+#c%SNq)A7QVQ8);tkIj;35J;-^Cv95AakgWj|J6-3z{ z1W3L4dau)K_j+wjuor!{<(3c=2XH8G1itT)Mh^BZJgSTnvY00ch!d(`>asCc+XK&g zxapa1jlH$e7ATn3 zy(EnqmmNtfv1K(?DV`KWPO;yOy*nCda_GKZNeUy7whDK<1wHJ(oM{g$ZrC-+RgIq7 zddHKfingjsk1IFmFxQe-=ihi*ZBRIY-r^H>i-j+YHjMew&fLk_@g>yumr64BMnnmf zCPKPDk?+r68uk7}tCc1~Kkh^l;1fs^o0h6iegu)#1A?ge=1c= zM&u89O!;~2{+waYc$xZ{-YRF)=gJ^eN=V#YXiRK4yPf>J5qHTb5^pvtKijxj9Q?@v zBPl!aYThy$6FJ`&1N1RC1J@5QO8kU$F^WwqB1b@lYyu4{sBqiJ4v1G?4=Gn8_S{wei1MX?oN_A%+UdtIs`DBbUs9c7tak&J0FU6AmojJ2PY5>VL2df z2|75XHfjTu-BHS+==RH8K?7$82rc|8L6dPumASRswP8hGU9G&7XmEV$5JniyUfUY| zRVjh}S(|Mg9$x!&tx=v2MnX=CFbFH5p7%LtK%b{hLfA?LJME^C5{&XUVmfKuF^AzeO`(0{Iw~7g73kV5&Gt8UF+BS(7OR`AJ*JMz z)(r<56WyB0WenxVzx#^4XS3W`eV$0srE@SgQ2uL;1lui=u@9ZyFv{A+EK`K0@fwQK zQGV3ty8X28H3Z z$HGZFAJ(nrtEB!B(0d1^?beo7E>A`!1uc@($+A ziWYtSR|EVhe<@+y`M(>N)p+NNeXMfVs$*B#`!ThTbF2i41b;QR{re~M{^BZLw_I?ftoD!+_A@E2I)d&!vmQX+x~c4oeuK;G^dKTj;ej zkxd9!1wc~M?mCSi0wvo)Wm)P~Yl%5)_k}$8ZABptbirmYYSVGGN6ncnboRdgC4{Dy zh3EZJVOVyZG|8cjFuc7^q;u*Pzt978+D;;O%=>V6$K_dOZVH&<4FVsKE?#&M13BVM z&6$mqbO#)T=fLaNwQrxW`D-BNAuD0LC1hoOs+9FV80$(01)mIXtW9jku9jLU?78pn zVisG!%ssOPucCRffdj~u_}-ebc0UczCYELk(ZJ68W&AOx$CuDslZa183S(F4bWvc! z-$np=gaZj#ff{IexJoo{g;`ym{>U1aEDVgli7!1;8oTP;@8*d3>umoqy(uf59#&8= zi(>grw!4Sye?C83#Pq2b1=8U=vRz3;pX6UZ_D6~>r@QCxm@DXkt(yz5sT+fC*dUi` zJhKE{3|HW9i>IWEQVhi@33jQV6%QUZL9z)_t)Qs!s~%2kU2qbKH^1TOY20OcEZ!kr zftWm($|Q0tb?q#1{!`qIRZ;EQQPko!ujOlAH{$4a2M7WSoH#8+07g30?os!E3{Gee z@@tFpm+hSgaOyB>+dR#Nq|EJT_d3KXP~Uq!&}MatfeVQ$#d846(H9ulaM}2IfFMRM z-@NjZcLGy+{z_%-0j;>7L*F%hj^H1pB1DYa-0xw~`0EG<(Wn?3hj{O1vc?_DYm3Rs z8J3>K%g1KI{{%=)&bT2jmv@xAr-n$7sSoc?;ri{*K~Jt#(K#$8%My!Y^TznKxjRnZ z3qLbH6^i2DnNgGgRZvt@WZ#1@^PcHK{_c@c@KWR-7+cr1fD9!5_;6+*Gf+hJ<_*)u zme}Ek@fRm20?ZbV97us)!cgml_j*4qC$A|EZL#|Xm@e|}sCbrz=_4ExpPZs553PLi z+l#zsQs6~{{y#~mBhlC<%ww*1DIMis;9p1?;_CY+rCam;1)%h~D8(boJ9^x&3N@(- zYv9E$?!MADz(T{v*Xhc$H1r{pvKq?Xzu0yx1P$wR+)O&#scs~m|IYn|kp0Qn{rp$= zEd0*yOP8MW!$~96_$6^7c_nXa)7qWi`0hO5JK)Pvn7DTOlj$M`V9XfsRd&3BDBhmy ziJo?K%j&u(GTr^$?*`1EnOli};gn_92B;Qx(*4|Bk0da97co8LW}3ml~$LjUjX8%Q4E3cQ~f5zOP(V4ozfrq^AcfmxcdpW#@7qy?PxK- zazNL99xsjnFBX#S1FVEwi3MVHeMET^hp{_&`ATJ81$JU5O9kS06XueDi3-%o4q;uq z`$SNIFu#{P10dTu4%+zJR?xV%sZFEU`485i@K=$Y{yPb5^E%wR-O5v+^FeS~mYLE5 zzQIt3I)os2WXr#{k>#GjNGbsVFr1)HR=|mI>#oZ<9Nd6X3&$PoG^|5ATNr=S?vZ?a zcW5KJ$|veyaKJ1YxN(4J)WPA7Bkhi455Q@fLScK0@xcaG3`sA(o!W)!xcnOBw^UkM-Xj19z%TsSHDtOgF~oMmvP|f6T&cnnLjVg|=Ox z$h$ue5~KSL!=x8ed6O=MfQzBkz5bGCxAx~T=~6|v`g6>-{+&f{!foqiqrEe+*{@p$g)zsYpsvGDWob1U}uFPivh1%@V^ z$L<1KNgD}2GCftyihsiFuY~vxnH@vxABI2+q07r2ovy!N;oa>k>(=djk5n~i>u$=& z!MjVx^dqoY_E(|zUO&fl}?>teTdsp!Dkk(n}Pab)_{G^liZ{P+7@7Rn+ z4S%Pb#$br!zfzn{)xc+BpHR4_K@B-1xo1KL@XbTRIEG?sB!^JI$TALySr2vkd7VHG0qx0F6=Ggt^tKag15Z?**|(9oE^h zxTxPS9LpU&X8AsJdEgZHRm|S|&`(Ky7x@fG7Mj^-`!n*Ri9+|(wQ#aHk@V9EOjXCQes zv%ljjX)W$dMt7pYf0AV1ElHT7%+rcF{(bzr!M|wH>ihMm|HOwZp(>>cNV(E}l%!6( zln|R1YOd{MJhk@g?v}c~)d;G1Ghb&WHzv1yr-G;<=e-rplp&hdg#hy(WVcKiP?JX4 zzHu;PrW!%|n+3jq@P7K<{H=MDFHk8$<1D-xw(mXh?V_k4;R%bs8e%%KForYXCcreJ znDxtverpHtpX4l&$rlB3x9}25vxKN&r;`iwIh$^Fjl9Vw`l~UxrB*_tzwpldNAI0& zQyjAJsmR}15m{**_IXKScE|hvlI2d!DEub+zXJSe?{V0V2O?kcqTDYDov)y81&T#{ zq49;?&QQk#(l#kw|k+>7=1ABnm!2rRQUuLBaT!kU3b+AEjESEXc0)YV-!~4qxfFjg^;8DJ1DtRl_ z^26pge9b7eyFHL4e~-q)`9|0<8aCY-+kCyjSY3C;8PbKWlDN`MAC>OA=NU2zk+DPgTU^fsO3l787rKGH2Fb zadtRxa@fsjtU#2QoNcTkYiFBZE5BLYb)BIb033Go{bHtUUpqFDODZ+wWSk za;Vp+LECG#vD<^Ug2Fxf?i#YlwI|Y3+?8!uZEY2~>ZEXM*7VYQvySH_W|UbF(;Z(l z4-lexM5kKq5b482NB2lZ_9%Z1QX+SB*vIIvusBX5&lBg3t=UD=ca;xNGs_+E<A?mO65&y7AMVYghBD)@#jAV2h23Dv~!v#$c- z#5E~}RNc$U>IV-!6miHTnOgfM3B!Q36L2ID7`6tU4!4Iq^r*z$ppQSJ>4A~R9QD(d z`78LQmp)Xs0B*m;XxA8_Z$H$OGA>HdaUh$Vqbn^Jpgnc5P;oMzJbDKjkMW%geyw$4_1##4ew|VUGV5v^C1EEb{cf^%q;!$is-G43A^2u(e z6a8`aySb;Uoyzq4aFS%s#=AAk6~MKOc`Ks4ck+bkhNqQG9~{4>oNBsl!GGg4V79Hz zf76QFJGpCaF}ye3kTB@II#&tG9K1dRqDve5c4mAkU3lK#%s_1x)KPnd|?qUXYLi>eAJ>X^rV#R-0%1=d#5IGji!syi`!Z6r0C0=j%N@U?rPKC$k+Yamr}Q zMM`ceU#cN0n#Z%Rj>leo9DUAMC1(-UK^Y8MvFe)GEV?%e zqaK29QM)qF^znh2{U_JYTCvpZzWTt7th;7ERvk+CM^)+lBv1R2Qm{-tDT-83{v8G4 z1iHN{1RTb!LYBQJ>PY4w&q4d`dPVQkvQU2};NDiJnj%eY{J%Qf$WVW#La}UszoyLl zjp{yQwn;*eL*eMuzyACGGh@~vC&4idf~{dRc5SM4f0lW0g!@-pZPM<@F>nmg;QLf5 z8cKFRXw+^^e*c~eYkyhH`@xDl(P687pEx;z#6w@1>#%czL&g<(perVf?r+ZjA0sKg my;Wa?q6<^vQf>bZ!S498deX=VIvpk$%#X>;EUPYu`M&_Q;NrRf delta 10296 zcmb7~2UHZxw)X`j=Zs`TGDwCYI75&e1q74~5>%pO1e%-&6eMTK8ANg(h5?nFk<3U& zGC1T9&pr3N@7{Oby6>&kz5Cby+O?~Cb*)`hy?S$-^=z9pAO!6*de|l~XzN${{WEXY zSqgk&c&qDU&E`6%YtJPz@t3?f?><{@AHns9pC_|+PhkR-hP5x;l@d+`FrJJ#o*b@( zM{|k@I)>b29mOp&cWKGG3z?EcMNAGom&1fIkmHfmPojjR$3!NHGBDu>B zjT@kyb^K9(GH)ihp(ffB%Nv!?SwL-G`{kk7G_%Hz4aS2&mN*dOWV8B%0g&b_u-Bwb z`%=1v4su)~AoFB=dAZ396iek9ZFjIH*Ga<%hr#h#HBuBTYbqc5H{mE`;9Y}KM~f_? z%^H1;B73L@dK&h{eV?N>PuyKxpQ28#5(aAeV7!qDJtsCSPwBTr=!n}MQbDk8HjMom zj8(XT{a?F$3@Wp!rI782(b%t!8Ds9vts^-3H2AG|(4F9%5h8kgb?wm37zsj$Fc2R<&mKjxQSRvN5ZAa#~s9ZIOAQ zqT5ZCmYbmwu%*pC?ODHXl%B+~x4;J|e85};21u}_hw68WluO-XQ+jpNujZ3}9nZGf z?qeGywdyy&{qA!*CuKA%#y{`WeNd^m%==N`+b7%$c0%%s)T@zBu?zpj@6Js++_(#; zt$i6V_$+CM*R}cDr7ixUOF-%B6zOK=NkZk&TZlu}9a2Z30Mg^o@Rygg-P3iztaR26 znAe@GT9)*b5VBYA8j_{SP8KS3fO?=JhlVAGevlEg*6J$QCe$b1=AhL&di`qZBF`aa zJ&rlP+*Vtlwcg`LfhV?`&bT#qFiAr@? zLuFhQbSLjR9=^SsoSA5WCzkI492sic{w>ioDOE#O>`AROsclhQr>B~g2YpU(dYJtq zfpZ1js-Km6UV#Kb%*Nu~)kA6@0#28|?N!kc*&U-JM!mIugwivS-kB(CcgIdnZoM9V zdztI)3E}8QGg-hGjcjLSuwl1gS&HPUUVI)~#U+rwb%z0sr1e2>`t(FG;A6=kl8V`r zvzcd2oIC9^G5qUj@bk;llm7H+59L&jgK<}8Ych77%<3)<_hb`O4{!RbtYXmns3_}V z4YA&50os#(V_+X85G5KLS)aJU_T3$hZa*w*N>Ntd)!1;3_VRK~3NY50QkEe4d=&4c17BZc0&YJ3bonF7uYQ5!V(P;^fv_@Ez3gz(P%POmh!AV%4bSC)7$iTgRPC(Y^o&GNFLY>|&J$>)vJ3o1QCzC9(f_9wL8o=ZPZUiD~ zNWS)xHHe$QZIe}hc@wJEmFPPGuS=s|N6^4l zd~j>5wqJe2_ui)V*_Y^pGbk{Vw<7G|H0(?oivJ`t0=>XdPTt7=%)>z>xApydi zTkz`GQ2wQ05nTbh!QM}U$?ezgInAngdy`^b7S~-Pz1>x-G$kI0rqFkX(YsyT`))gh>-`1?CZ+@)hE_^cXpHspkl{}F+DSL@IohtrD# z5|Sy6=$cgOOnw00cOj56n{asO$xke?_*W!2m@?QRt@~eDy;ZYtB)=2p)IqXCFw;|( zKH!Sc7(e<&&ZDQTud@1WM?;N;Z_q|l18Yc=Z+eqe1eHPvW-N0~AuQ3;4t$tr#el{n zPWTM&vlp1|Grfz(Ss&y_aeZNPx!@gPa0#Nspaji3{|EtI2UJumO6R%r$tRp`G(1d? zEjtmBtFjiIjipX$Kem(qe6B~yOq)Wb@r#X~?BY9C+Q0UA zVyIimt~WhP9&=c*BdBhSpJHPQd88w#J+F6{@GRQ^ilezPzfXZrw1t%gNsp zo2s|=Y}M{yER9!V2e`Rz+oA+V^zrt)>07m>Y`pW2zN@l#>W9q+BgKoQ;Yxcz<{>*|iBx5|3a>WWE9vY~99_n(R$_4Mrn2fkW`ZLE1X~mj4f6fbhf~(Ch zr|XgCa_R)|08^X3VNc_AtCWKV5k*}!zyW1Ly5quo$15@D&Yh=Am2M4zz5(#Ykp3pc zeJ@UTI`#QVPviu*uf+q?JGDti*j;=x;hWT^AlwsLQggk>n6xMHq}_7 zNCyMT8-e6hR|2_bx4($lmEzne!<^0&4PW=nNi{ zj7iIBH*ZlWi|q`NBqi5nY;8+LVaobJ_308pK~Q6xFJ)5(8<^s!&vU^0X_|kgI6UsHZ7%HqRny4)ccY zGE-q(ZI}hnP?n<#GTyo6cq`mSSSQ!HSC}gi$tn?l*SkyYK3;BjI#V=2rwd`UE4ORS zby2dC&&#VRtSPEVmpR4A58QI@Mehv4ndpk))Y=MMo8Ww^@K%%?W9?^Wpi$ z0Y8Y2QuU=942v$Fp&u7<1@C+%Ry|LEn-UzO`C&gha%PETja)yt!v=j2rvs&wluNO1 zJrGCd4?5S2<40{MMZ^F*)MmU8=>^NE>a5IAM3OaAy|hGKD@r#h`Q7TvPtvUHmrKab zxTuJxR8rJSgwgqN2%oQrZYuqZ>NAlW>`A(ts`6hd@n?rVhux6zwNzZn>*^ci(8$LC z1&XQ=_>m0rgj_y5MQWgTQ)4qK=>|F}7d=ZhY(Meeym# zLQ_HySI`+|mBhvx$E~7t{c+gtaY&qazeCzXojymD83vuBt=vXV7{IcWy_YMWB4=%( z{w3Xfg%h#J{eg>M;fFO+5*WCyHw|~ivQgsKv(Hf*$4Kh1`ib#V+-metzV(Lsdyrkg zA6th8wNrF_Ds&Oy*eusBqUs|thBjw^oc>D@+tvyJODje2kFOkw4watvvi%uZlM@QXUD>1w(d zH!HiA2;dNDa&pOPhJ1+7OzW4a{-$ywqf~iL70ojzF_Tys9$oe!vAA;W+6M@BSzVf# zq-1|n;jZaM(J12{w5gqUI1XvV#5*r`%fi!L-^`x#rmP7Wd`(NqnAb_^NE`ZHWzL&K zGtokRKM+0`OgLi4lO@E(1A9yr`uJwNFiOFgU@P_c-9i%=4;+oWcPr+KiwY@%Qv%(u zA5xiX$w*PT*DmMLHsfIxboBrkGVUlLg3qyLVc#dw`umh4G7V%`2VciVnlmTeQT<@h z=R&}Z9nsiLMM~CND*NF_O4HF@y&?B6vAR3b)5=ZQ_;jNf!8qK3<`^R`PqkUeV08wX zp=$_QkI*%J5f&Vl&}r{`db_PFWKY(gYL9wzRzQoiF|j{?2vCbMag~PxLa!ey)9Xxn ze<`4lA{Nt`iV0E~6=fAyX6PQ#Rwui{<(WZYJfTL+qnO(*Kf zXfHB4Dw|r!{)vkhH}{CU7`ld~>Sr@542!^chW1p7xadLY5CKSm9Fto@wwc1j&SE6K zXF1>~6P@3a7$+@yQb-67;C9DLQ;V)`Yn$2cV_508$=IZJ^g8Ly23fYhlnq_FciGc3 zGc&SteN~00%h&!f%>kw${X9rROv%i7w+g>ydHK-3NfHFfii;Jml7?gzy3{$l9HEZF zH@|ebNkd~Lt;D2FAF?+ztcUe-632g=Vk9S{K$~2{E$JKzLyX7*nT~ej>BETxTOZwM z7YM5S-(F3D7VZ2`85Kyue#gFb8B8$=QX!skj4jKnD2q4Q=>BI1zIqLdvBDv>DTtoW zllmhjsf7H9lS4~Urm6JP5$}#zC(Sq}UPz<7X#5k3zGYGZhN}J3!t9bIQRO;pAc&%< z8Rsx$;o#n>IA$(zujkM`_uJh>nl_O6gvc#n4? z8*Jc+^Thzp9%aOM;%VC*yt*~exD^H)*?032lZImmfOQs0_AN%=(s`{0NZqRqwR^Ta zI0y&r0o2R=cA%gJLsi`~}?rVRo+Lq%h&mLM8`;6NP!yu>xux3j~Re{LS{uGD4o zFA{6T4kZ)4r>atc#Zt<IuNs(}`3rFt_)<8};=en}mTP8}?2xq5epK6sy`WG$cGx!lqydVY z0z?t){UcLkP#9@2L^MwTPw{P_N(yah%rvKQo;VLyKShj0mq#ov*S%0QR~*G3)rJ%EvC>c?*olNbRZmeX0BFln zs^zi7)`Eo!gDlG}VI&hDX+qJ2sjbkv;Lq(sV(++qu4fsY@BSWk=ct1G(9ASVJgJ}G zAF7!i$jtj9~2gql^c)?rb1?p@1ikMYAEPTvc% zD{8%U?0h_H#}}?{Z>%jGev?zOxi9+Na12P^ zqph1Av#4N#g(Nq?_T9Fa*F^5&lIeV1_ZN%o4A;Sz*%?Ui@`dKP<{XD44ZlH(ns@5^ zCl99tKI$lDKu(mxNOenCgCnRANu{I&5qUWqal$&Bp+Uymv@#dZuDy%5=5u}8_Db8D zo8PvX?m;fv4vLbU?-`u8Eg1426J0tE>381eMUe6KP$XFZ68h$B`WB*-=6sVDkHpMb z#VmyD&3WoAq&&yjz~{?@`G9YY zK_dce6YM)M$Cz^=F;{|yeHyI;JSRcg;2L}Mqw4#|?du(j?LJdmCS{%#3w8el$cZnf zJA<0T?o?jt8y|M?xBI~;^r1&rs^zd(_Hg!?Ft75K0G>vqx^Sr9aM|}~IazpZ+c)Ci zT3xlD7 zmk#88|I3^gh@&RIaK@s_hA(y+5XmBWuY^m*ejEQi|3`O^1!aN+W312GDs|Bf%=;L+WlXLDbV%hS8l>yciVLM z6(}GW6ymk=`w_!HuQ=rP)I5>VTF3{Q%OZnIyo1Zq50~ygTo$Ta;;vklbX;P0w7_a` z!S-|^W?HtI>&1|Uvq~d4yn>3n!q&Y4lT&(lS`lkBw(xdl3||as_0Bg{10<=>X<$KSu?>8%f25Va$tvZ3g_nC--x*

8ck}K9QuRbveudfueomj|_9wAHj8{ah69Ldae9Jo=M{` z@78*yTdUF^-J>wPY<(;X>9Rx4|8+-56z)PRL=iuC9i z%jJ;iT%tes;<%)kiRDg(maa-sye3r2(E46*%iB8;$dhI2?x@XV3Pb!wr|LEIC4TW@7(ZpA@Qy)F$QKP%4{Eu~8 z+eK+9Y4DfQNnVYUnI)pYtAT6)uN^9XC>>&U^$T?ujGgb2@s!yQQ>Ey@DzH)4rD(i%uP_(! z+9`dvkvgxl8uZUAHh))LGU{pwa>87^#eO5dmm2H01;>ANqOCa7J&N$CRpCqT5*W;ZH(ZO#$C?#XI`Kh zOLhZzHuXm<@{Lp);vL!M+kZ{}HBy0I>J^hyE6t5xzitQWzPF7Jn97`m%0e*7oU5>! z;9CuPSvBqJYO3vOM!IU!^y+&?)s(Z<3{utPE!A{ytEn%XF|g%;1qd7i5+M(YVFg85 zfnv#15Gon4ml<8pGP=EuI~9xpn6+`&Q{!%TYk_9(OHME0Pi}>@~COumK>m;gD8WBVsf^_yrqHH;7#zQX+-!9MT~O zwnrnf^4|c~FT7^ucwv^jT{`L(_mZqI^(`s&tq3PA878||V-KLt@2z}=>n-VkdMj)X z7~4CSWEsS-KNl>wvpKh7DzFDZU_k!;rC}Pw*%}3ecVYb~cj*8%5#*HI4M#g$`!L}g zoUeaLY0jrRxHpZpi9tXnd!$)8u= zXPod{xyJRb>+~mY93P1EKT8bYe+1>|>*P6Uk;7kGJqU zrds(NnE^NXUk6X?1Iku+6HAk1!zs2&_sCmhNp5`i#{v9tF`Uxyjo34oOEOaN;XMYn zFOa#o3uyu>m`VD!9&+iy_&2F`09v6f7$_FMYx!=jo zfevxT>?I!SVz^0U3z;X|uIe0+*m&!qlmjGknSN=F*Js;Q9Zk&VkvGW1y#mhOqi9zu z|I0b?i)rdkVn0u+fl$?pTlc6`9s}zrgMYeERxN#PjrV3dQeFH1ocRO>pY>sQtP6jp%~RXe#7I{NRI3Xd&w6+`d&KX2!0%YB#Dy zXb7GeDMjwdo@XyhBYke%8r>-DV!JZe3j8KmOQfY(* zZ7loYDUpKYR_wRRpTdI_6@dhE_Ad3H)G7&~e|M>MZC=yxJg6|m3BEbVJ7C64D>3!B z_i^BH`WK-DYxZyINvZr#g#vBR2kxffijdo}53A?=(fV)U>>+!?EB1;02BFk*;KjjP zG8S9G7bQ0Bm0upGM~WTwXi#-DlD=8*lw$Fe+f`rJ6qg)piryP_+x;;+fE&!u6dNZ{ zJ>M#TQZLskBF&7PS7}agVnFrPYotNvlQG;A$BeTFw>IZ%TJk20%# zBq=xaa&!YVG5-YMPa;=s;3sIWicl)WHo1f;-;=c7_>ij`rup~Kzp435>ZN-!Y>7h* zL9G+0d7gPJwdpy!m%pgek>Jm9rMaKE)Dq`wP1$?xPvh$%2~PaC@_$wU{;F}SwEQwH z4i5lhDZ`fdZ$z&xgc03KQ(*W!uDT`B+HFd*LZh-IrLw|Jvi#SKYK0+YnQ%sBcF9{G z(zSQvA)Qk(9rklNFmpO|emb~qIt~N$H&dWO27WLE$fP4iN-L^piMU)=c7-3a$8HkN zeWvR@qq5mS^e!M6oCMZxcT+p zv=Lqa9*`Pq=CDW;B~kkB#(Aas7ZMqtxA_R_UV^4}F^srHGn}R_7`7&ybLZn6xTc(I zOoD~StCw|Je%YT*dN%e~zNhD&a}G6G#3inCZ2Vej!Bo2744uDcbS`deYoI94Mvt)W z(J)E_#b{7$43E<|*1VlhVkc^tNxar(2ye#(P|g!cnna#6ZI)_+;cs`&HTt!s!Y_8t zGyAo*!m)QsXSAP%x8J{Z?n*)sA&ZDA=t_U?r_8(7yLoOjA7Tqz7k73icuaT{_jHeW zJoTn=l6ozE%>wT7ZsCT+R8dt)A#5YVJ!UFP1Y`E(S0V7^7$-^7WTDV7mk_;cdFgfl zl)-(|rALRTiA#)gV#lK7aZ)9+Dy=y@$n3>~e@$=ho=!GA1F6>-*BrKQG9lOzUwZ{7 z<}J!wYdf_^!fOr%?<6uIzDgMpJoTsHVH(pp`(5-^z@L8xKfw%zG(7w1fnm9d36YX1 zztlIfib$M_pTUKHb*dM|t~ulu1*C{;4(S~DWXfBw2N2n^@UK-3lpV_vi3XE1T=1_K zL{=UWmaC#~J=iQ)4Q8X@Ut1i+!1wjR3;bZe@>Y%%XfGKLQ?>}BS9z;JI&@D+AIvCA zA8+U#F4jVR`w-5atojQVDbSA4h{U)(K7TDTo;{5r#Gbs>DpCfXt=9v5rOTbkL*e*9 z-qIhGQ52+RhJ78%3aTH<3j8?qylG$ywS!swYlkf+X&(5+e;_VpAa}Skg`AvtcX@T* z=*|~of=X(1e-v{y8r|s58gq4Ii<}$~XulY9+197IInM5>NENvDyg*L=6mXG*8hOIt z{MYJp&2;Q>e)4n8)a(Gn-DHIvx>0+03vE2h+)FHGY#Tbj~hd@zt#IY#Ig`)3} zfs*fay3*w^Dq<&^)qm$3tN&qxl^{p=k0FyNBid6IF?-XL%TG^HkMlC2mSRye8!z$_ zpi<(yb9Rof1^Chvw?<*(oS+3HMq(GNQ-b>XUaDSfp7dscccGl$()@e!)+W~!EQxc3e&LLm0P z=Ow&v)$}~oWdC7hUd@E u32 { + unimplemented!("This should be overridden") +} + +pub fn example() -> u32 { + next(); + next(); + next() +} diff --git a/intTests/test_mir_ghost/test.saw b/intTests/test_mir_ghost/test.saw new file mode 100644 index 0000000000..01046b4bcc --- /dev/null +++ b/intTests/test_mir_ghost/test.saw @@ -0,0 +1,28 @@ +enable_experimental; + +let next_spec counter = do { + n <- mir_fresh_var "n" mir_u32; + mir_ghost_value counter n; + + mir_execute_func []; + + mir_ghost_value counter {{n+1}}; + mir_return (mir_term {{n}}); +}; + +let example_spec counter = do { + n <- mir_fresh_var "nm" mir_u32; + mir_precond {{n < 2}}; + mir_ghost_value counter n; + + mir_execute_func []; + + mir_ghost_value counter {{n+3}}; + mir_return (mir_term {{n+2}}); +}; + +counter <- declare_ghost_state "ctr"; +m <- mir_load_module "test.linked-mir.json"; + +next <- mir_unsafe_assume_spec m "test::next" (next_spec counter); +mir_verify m "test::example" [next] false (example_spec counter) z3; diff --git a/intTests/test_mir_ghost/test.sh b/intTests/test_mir_ghost/test.sh new file mode 100755 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test_mir_ghost/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw diff --git a/saw-remote-api/CHANGELOG.md b/saw-remote-api/CHANGELOG.md index 1316e3e6ba..8aafd8075b 100644 --- a/saw-remote-api/CHANGELOG.md +++ b/saw-remote-api/CHANGELOG.md @@ -35,6 +35,8 @@ * Add `"slice"` and `"slice range"` `setup value`s representing slices in MIR verification. Attempting to use these in LLVM or JVM verification will raise an error. +* The `SAW/create ghost variable` command and the associated + `ghost variable value` value are now supported with JVM and MIR verification. ## 1.0.0 -- 2023-06-26 diff --git a/saw-remote-api/python/CHANGELOG.md b/saw-remote-api/python/CHANGELOG.md index 4892e5c863..b2434fd8fc 100644 --- a/saw-remote-api/python/CHANGELOG.md +++ b/saw-remote-api/python/CHANGELOG.md @@ -38,6 +38,8 @@ variable. This function is currently only supported with LLVM and MIR verification, and using this function with JVM verification will raise an error. +* The `create_ghost_variable()` and `ghost_value()` functions are now supported + with JVM and MIR verification. ## 1.0.1 -- YYYY-MM-DD diff --git a/saw-remote-api/python/tests/saw/test-files/mir_ghost.linked-mir.json b/saw-remote-api/python/tests/saw/test-files/mir_ghost.linked-mir.json new file mode 100644 index 0000000000..f09a6a8147 --- /dev/null +++ b/saw-remote-api/python/tests/saw/test-files/mir_ghost.linked-mir.json @@ -0,0 +1 @@ +{"fns":[{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[],"terminator":{"args":[],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::ae5488df1dc4e585"},"kind":"Constant"},"kind":"Call","pos":"mir_ghost.rs:6:5: 6:11"}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"args":[],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}},"bb2"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::ae5488df1dc4e585"},"kind":"Constant"},"kind":"Call","pos":"mir_ghost.rs:7:5: 7:11"}},"blockid":"bb1"},{"block":{"data":[],"terminator":{"args":[],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"bb3"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::ae5488df1dc4e585"},"kind":"Constant"},"kind":"Call","pos":"mir_ghost.rs:8:5: 8:11"}},"blockid":"bb2"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"mir_ghost.rs:9:2: 9:2"}},"blockid":"bb3"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}]},"name":"mir_ghost/150ed446::example","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_22","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:24: 709:45 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"mir_ghost/150ed4465f8cb026::{{alloc}}[0]","kind":"static_ref"},"ty":"ty::Ref::c2a5dcbb98af2a61"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_5","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:24: 709:45 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_22","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:24: 709:45 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_5","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Ref::675b2a8049aad652"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:24: 709:45 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Move"},"ty":"ty::Ref::675b2a8049aad652","type":{"kind":"Pointer(Unsize)"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"mir_ghost.rs:2:20: 2:47","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"mir_ghost/150ed4465f8cb026::{{alloc}}[1]","kind":"static_ref"},"ty":"ty::Ref::c2a5dcbb98af2a61"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_16","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"mir_ghost.rs:2:20: 2:47","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_15","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"mir_ghost.rs:2:20: 2:47","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_16","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::675b2a8049aad652"}},"pos":"mir_ghost.rs:2:20: 2:47","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_15","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Move"},"ty":"ty::Ref::675b2a8049aad652","type":{"kind":"Pointer(Unsize)"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::d0bd7bf253977b90"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"mir_ghost/150ed4465f8cb026::{{alloc}}[2]","kind":"static_ref"},"ty":"ty::Ref::d0bd7bf253977b90"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_19","ty":"ty::Ref::d0bd7bf253977b90"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::d0bd7bf253977b90"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::d0bd7bf253977b90"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_19","ty":"ty::Ref::d0bd7bf253977b90"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::913e2ff5487f7787"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::d0bd7bf253977b90"}},"kind":"Move"},"ty":"ty::Ref::913e2ff5487f7787","type":{"kind":"Pointer(Unsize)"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Move"},{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_13","ty":"ty::Adt::ba5184b53bc36a4d"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::76afb566734aff77"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !mir_ghost.rs:2:5: 2:48"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_12","ty":"ty::Ref::bf4d6d337c623aee"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !mir_ghost.rs:2:5: 2:48","rhs":{"borrowkind":"Shared","kind":"Ref","refvar":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_13","ty":"ty::Adt::ba5184b53bc36a4d"}},"region":"unimplement"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::bf4d6d337c623aee"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_12","ty":"ty::Ref::bf4d6d337c623aee"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::bf4d6d337c623aee"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::Adt::613f1953a8669d14"}},"bb2"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::72bf0f6662028c6a"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/macros/mod.rs:709:47: 709:77 !mir_ghost.rs:2:5: 2:48"}},"blockid":"bb1"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_9","ty":"ty::Array::6167cd8fdeb01e06"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !mir_ghost.rs:2:5: 2:48","rhs":{"akind":{"kind":"Array","ty":"ty::Adt::613f1953a8669d14"},"kind":"Aggregate","ops":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::Adt::613f1953a8669d14"}},"kind":"Move"}]}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_8","ty":"ty::Ref::41f3f8f95d02c3e9"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !mir_ghost.rs:2:5: 2:48","rhs":{"borrowkind":"Shared","kind":"Ref","refvar":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_9","ty":"ty::Array::6167cd8fdeb01e06"}},"region":"unimplement"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::41f3f8f95d02c3e9"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_8","ty":"ty::Ref::41f3f8f95d02c3e9"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::913e2ff5487f7787"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !mir_ghost.rs:2:5: 2:48","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::41f3f8f95d02c3e9"}},"kind":"Move"},"ty":"ty::Ref::913e2ff5487f7787","type":{"kind":"Pointer(Unsize)"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Move"},{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Adt::ba5184b53bc36a4d"}},"bb3"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::76afb566734aff77"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !mir_ghost.rs:2:5: 2:48"}},"blockid":"bb2"},{"block":{"data":[],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Adt::ba5184b53bc36a4d"}},"kind":"Move"}],"cleanup":null,"destination":null,"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::906e67453a1bbab9"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:9: 57:73 !mir_ghost.rs:2:5: 2:48"}},"blockid":"bb3"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":true,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::Never::7199a9b06188843c"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Adt::ba5184b53bc36a4d"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_5","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::913e2ff5487f7787"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::41f3f8f95d02c3e9"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_8","ty":"ty::Ref::41f3f8f95d02c3e9"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_9","ty":"ty::Array::6167cd8fdeb01e06"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::Adt::613f1953a8669d14"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::bf4d6d337c623aee"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_12","ty":"ty::Ref::bf4d6d337c623aee"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_13","ty":"ty::Adt::ba5184b53bc36a4d"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_15","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_16","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::913e2ff5487f7787"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_19","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_22","ty":"ty::Ref::c2a5dcbb98af2a61"}]},"name":"mir_ghost/150ed446::next","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::bf4d6d337c623aee"}],"body":{"blocks":[{"block":{"data":[{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:328:23: 328:24 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::bf4d6d337c623aee"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::bf4d6d337c623aee"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:328:23: 328:24 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::bf4d6d337c623aee"}},"kind":"Copy"}}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:328:26: 328:33 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::FnPtr::07cd89921cc84271"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::FnPtr::07cd89921cc84271"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:328:26: 328:33 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","rhs":{"kind":"Cast","op":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::b30b83d63051810b"},"kind":"Constant"},"ty":"ty::FnPtr::07cd89921cc84271","type":{"kind":"Pointer(ReifyFnPointer)"}}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:42: 347:59 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::FnPtr::bd6bee7b1f95b7bf"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:57: 347:58 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::FnPtr::07cd89921cc84271"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::FnPtr::07cd89921cc84271"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:57: 347:58 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::FnPtr::07cd89921cc84271"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::FnPtr::07cd89921cc84271"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::FnPtr::bd6bee7b1f95b7bf"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::788a983faed72be6"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:42: 347:59 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35"}},"blockid":"bb0"},{"block":{"data":[{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:58: 347:59 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::FnPtr::07cd89921cc84271"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:68: 347:85 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::4e8e6a61a1ceb622"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:83: 347:84 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::bf4d6d337c623aee"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::bf4d6d337c623aee"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:83: 347:84 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::bf4d6d337c623aee"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::bf4d6d337c623aee"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::4e8e6a61a1ceb622"}},"bb2"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f532a620418c4246"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:68: 347:85 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35"}},"blockid":"bb1"},{"block":{"data":[{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:84: 347:85 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::bf4d6d337c623aee"}},{"kind":"Deinit","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:18: 347:87 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35"},{"kind":"Assign","lhs":{"data":[{"field":0,"kind":"Field","ty":"ty::Ref::4e8e6a61a1ceb622"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::613f1953a8669d14"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:18: 347:87 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::4e8e6a61a1ceb622"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[{"field":1,"kind":"Field","ty":"ty::FnPtr::bd6bee7b1f95b7bf"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::613f1953a8669d14"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:18: 347:87 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::FnPtr::bd6bee7b1f95b7bf"}},"kind":"Move"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:86: 347:87 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::4e8e6a61a1ceb622"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:347:86: 347:87 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::FnPtr::bd6bee7b1f95b7bf"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:328:33: 328:34 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::FnPtr::07cd89921cc84271"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:328:33: 328:34 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::bf4d6d337c623aee"}}],"terminator":{"kind":"Return","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:329:10: 329:10 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:350:5: 350:35"}},"blockid":"bb2"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::613f1953a8669d14"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::bf4d6d337c623aee"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::FnPtr::07cd89921cc84271"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::FnPtr::bd6bee7b1f95b7bf"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::FnPtr::07cd89921cc84271"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::4e8e6a61a1ceb622"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::bf4d6d337c623aee"}]},"name":"core/73237d41::fmt::{impl#3}::new_display::_inst47ac314b85a79c82[0]","return_ty":"ty::Adt::613f1953a8669d14","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::913e2ff5487f7787"}],"body":{"blocks":[{"block":{"data":[{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::bool"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:37","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::bool"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:24","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::usize"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:24","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::675b2a8049aad652"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::675b2a8049aad652"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:24","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::usize"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:24","rhs":{"kind":"Len","lv":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::675b2a8049aad652"}}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:23: 400:24","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::675b2a8049aad652"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:27: 400:37","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::usize"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:27: 400:37","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::913e2ff5487f7787"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:27: 400:37","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::usize"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:27: 400:37","rhs":{"kind":"Len","lv":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::913e2ff5487f7787"}}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:36: 400:37","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::bool"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:37","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::usize"}},"kind":"Move"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::usize"}},"kind":"Move"},"kind":"BinaryOp","op":{"kind":"Lt"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:36: 400:37","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::usize"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:36: 400:37","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::usize"}}],"terminator":{"discr":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::bool"}},"kind":"Move"},"discr_span":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:37","kind":"SwitchInt","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","switch_ty":"ty::bool","targets":["bb2","bb1"],"values":["0"]}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::bool"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"bool","size":1,"val":"1"},"ty":"ty::bool"},"kind":"Constant"}}}],"terminator":{"kind":"Goto","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","target":"bb3"}},"blockid":"bb1"},{"block":{"data":[{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:41: 400:70","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::bool"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:41: 400:53","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::usize"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:41: 400:53","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::675b2a8049aad652"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::675b2a8049aad652"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:41: 400:53","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::usize"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:41: 400:53","rhs":{"kind":"Len","lv":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::675b2a8049aad652"}}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:52: 400:53","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::675b2a8049aad652"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:56: 400:70","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::usize"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:56: 400:66","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::usize"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:56: 400:66","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::913e2ff5487f7787"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:56: 400:66","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::usize"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:56: 400:66","rhs":{"kind":"Len","lv":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::913e2ff5487f7787"}}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:65: 400:66","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::usize"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:56: 400:70","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::usize"}},"kind":"Move"},"R":{"data":{"rendered":{"kind":"usize","size":8,"val":"1"},"ty":"ty::usize"},"kind":"Constant"},"kind":"BinaryOp","op":{"kind":"Add"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:69: 400:70","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::usize"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::bool"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:41: 400:70","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::usize"}},"kind":"Move"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::usize"}},"kind":"Move"},"kind":"BinaryOp","op":{"kind":"Gt"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:69: 400:70","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::usize"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:69: 400:70","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::usize"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::bool"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::bool"}},"kind":"Move"}}}],"terminator":{"kind":"Goto","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","target":"bb3"}},"blockid":"bb2"},{"block":{"data":[{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:69: 400:70","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::bool"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:69: 400:70","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::bool"}}],"terminator":{"discr":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::bool"}},"kind":"Move"},"discr_span":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","kind":"SwitchInt","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:400:12: 400:70","switch_ty":"ty::bool","targets":["bb6","bb4"],"values":["0"]}},"blockid":"bb3"},{"block":{"data":[{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:9: 57:73 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","slvar":{"is_zst":true,"mut":{"kind":"Not"},"name":"_15","ty":"ty::Never::7199a9b06188843c"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_16","ty":"ty::Adt::ba5184b53bc36a4d"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:20: 401:34","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::675b2a8049aad652"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:20: 401:34","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::c2a5dcbb98af2a61"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:20: 401:34","slvar":{"is_zst":false,"mut":{"kind":"Not"},"name":"_19","ty":"ty::Ref::c2a5dcbb98af2a61"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_27","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:20: 401:34","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"mir_ghost/150ed4465f8cb026::{{alloc}}[3]","kind":"static_ref"},"ty":"ty::Ref::c2a5dcbb98af2a61"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_19","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:20: 401:34","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_27","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::c2a5dcbb98af2a61"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:20: 401:34","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_19","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::675b2a8049aad652"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:20: 401:34","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::c2a5dcbb98af2a61"}},"kind":"Move"},"ty":"ty::Ref::675b2a8049aad652","type":{"kind":"Pointer(Unsize)"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:33: 401:34","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::c2a5dcbb98af2a61"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::d0bd7bf253977b90"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","slvar":{"is_zst":false,"mut":{"kind":"Not"},"name":"_22","ty":"ty::Ref::d0bd7bf253977b90"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_26","ty":"ty::Ref::d0bd7bf253977b90"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"mir_ghost/150ed4465f8cb026::{{alloc}}[2]","kind":"static_ref"},"ty":"ty::Ref::d0bd7bf253977b90"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_22","ty":"ty::Ref::d0bd7bf253977b90"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_26","ty":"ty::Ref::d0bd7bf253977b90"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::d0bd7bf253977b90"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_22","ty":"ty::Ref::d0bd7bf253977b90"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::913e2ff5487f7787"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","rhs":{"kind":"Cast","op":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::d0bd7bf253977b90"}},"kind":"Move"},"ty":"ty::Ref::913e2ff5487f7787","type":{"kind":"Pointer(Unsize)"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:71: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::d0bd7bf253977b90"}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Move"},{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_16","ty":"ty::Adt::ba5184b53bc36a4d"}},"bb5"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::76afb566734aff77"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:38: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35"}},"blockid":"bb4"},{"block":{"data":[{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:71: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:71: 57:72 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::675b2a8049aad652"}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_16","ty":"ty::Adt::ba5184b53bc36a4d"}},"kind":"Move"}],"cleanup":null,"destination":null,"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::906e67453a1bbab9"},"kind":"Constant"},"kind":"Call","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/panic.rs:57:9: 57:73 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:401:13: 401:35"}},"blockid":"bb5"},{"block":{"data":[{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:402:9: 402:10","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::bool"}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:21: 403:27","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_23","ty":"ty::Ref::675b2a8049aad652"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_23","ty":"ty::Ref::675b2a8049aad652"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:21: 403:27","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Copy"}}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:34: 403:38","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_24","ty":"ty::Adt::45883e75bd5c5ca5"}},{"kind":"Deinit","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:34: 403:38"},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_24","ty":"ty::Adt::45883e75bd5c5ca5"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:34: 403:38","variant_index":0},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:40: 403:44","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_25","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_25","ty":"ty::Ref::913e2ff5487f7787"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:40: 403:44","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Copy"}}},{"kind":"Deinit","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:9: 403:46"},{"kind":"Assign","lhs":{"data":[{"field":0,"kind":"Field","ty":"ty::Ref::675b2a8049aad652"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::ba5184b53bc36a4d"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:9: 403:46","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_23","ty":"ty::Ref::675b2a8049aad652"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[{"field":1,"kind":"Field","ty":"ty::Adt::45883e75bd5c5ca5"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::ba5184b53bc36a4d"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:9: 403:46","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_24","ty":"ty::Adt::45883e75bd5c5ca5"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[{"field":2,"kind":"Field","ty":"ty::Ref::913e2ff5487f7787"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::ba5184b53bc36a4d"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:9: 403:46","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_25","ty":"ty::Ref::913e2ff5487f7787"}},"kind":"Move"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:45: 403:46","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_25","ty":"ty::Ref::913e2ff5487f7787"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:45: 403:46","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_24","ty":"ty::Adt::45883e75bd5c5ca5"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:403:45: 403:46","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_23","ty":"ty::Ref::675b2a8049aad652"}}],"terminator":{"kind":"Return","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/fmt/mod.rs:404:6: 404:6"}},"blockid":"bb6"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::ba5184b53bc36a4d"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::913e2ff5487f7787"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Ref::913e2ff5487f7787"},{"is_zst":true,"mut":{"kind":"Not"},"name":"_15","ty":"ty::Never::7199a9b06188843c"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_16","ty":"ty::Adt::ba5184b53bc36a4d"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_19","ty":"ty::Ref::c2a5dcbb98af2a61"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Ref::913e2ff5487f7787"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_22","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_23","ty":"ty::Ref::675b2a8049aad652"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_24","ty":"ty::Adt::45883e75bd5c5ca5"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_25","ty":"ty::Ref::913e2ff5487f7787"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_26","ty":"ty::Ref::d0bd7bf253977b90"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_27","ty":"ty::Ref::c2a5dcbb98af2a61"}]},"name":"core/73237d41::fmt::{impl#4}::new_v1::_instbd21306cbe4f0b9b[0]","return_ty":"ty::Adt::ba5184b53bc36a4d","spread_arg":null}],"adts":[{"kind":{"kind":"Struct"},"name":"core/73237d41::fmt::Arguments::_adtbd21306cbe4f0b9b[0]","orig_def_id":"core/73237d41::fmt::Arguments","orig_substs":["nonty::Lifetime"],"repr_transparent":false,"size":48,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"core/73237d41::fmt::Arguments::pieces","ty":"ty::Ref::675b2a8049aad652"},{"name":"core/73237d41::fmt::Arguments::fmt","ty":"ty::Adt::45883e75bd5c5ca5"},{"name":"core/73237d41::fmt::Arguments::args","ty":"ty::Ref::913e2ff5487f7787"}],"inhabited":true,"name":"core/73237d41::fmt::Arguments"}]},{"kind":{"kind":"Struct"},"name":"core/73237d41::fmt::ArgumentV1::_adtbd21306cbe4f0b9b[0]","orig_def_id":"core/73237d41::fmt::ArgumentV1","orig_substs":["nonty::Lifetime"],"repr_transparent":false,"size":16,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"core/73237d41::fmt::ArgumentV1::value","ty":"ty::Ref::4e8e6a61a1ceb622"},{"name":"core/73237d41::fmt::ArgumentV1::formatter","ty":"ty::FnPtr::bd6bee7b1f95b7bf"}],"inhabited":true,"name":"core/73237d41::fmt::ArgumentV1"}]},{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"core/73237d41::option::Option::_adta9d03177c2d4a99f[0]","orig_def_id":"core/73237d41::option::Option","orig_substs":["ty::Ref::5f3877d5405402c5"],"repr_transparent":false,"size":16,"variants":[{"ctor_kind":{"kind":"Const"},"discr":{"index":0,"kind":"Relative"},"discr_value":"0","fields":[],"inhabited":true,"name":"core/73237d41::option::Option::None"},{"ctor_kind":{"kind":"Fn"},"discr":{"index":1,"kind":"Relative"},"discr_value":"1","fields":[{"name":"core/73237d41::option::Option::Some::0","ty":"ty::Ref::5f3877d5405402c5"}],"inhabited":true,"name":"core/73237d41::option::Option::Some"}]},{"kind":{"kind":"Struct"},"name":"core/73237d41::fmt::Error::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::Error","orig_substs":[],"repr_transparent":false,"size":0,"variants":[{"ctor_kind":{"kind":"Const"},"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[],"inhabited":true,"name":"core/73237d41::fmt::Error"}]},{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"core/73237d41::result::Result::_adt0f6d5765b4e92fb6[0]","orig_def_id":"core/73237d41::result::Result","orig_substs":["ty::Tuple::e93222e871854c41","ty::Adt::8d47b311e48cbf8f"],"repr_transparent":false,"size":1,"variants":[{"ctor_kind":{"kind":"Fn"},"discr":{"index":0,"kind":"Relative"},"discr_value":"0","fields":[{"name":"core/73237d41::result::Result::Ok::0","ty":"ty::Tuple::e93222e871854c41"}],"inhabited":true,"name":"core/73237d41::result::Result::Ok"},{"ctor_kind":{"kind":"Fn"},"discr":{"index":1,"kind":"Relative"},"discr_value":"1","fields":[{"name":"core/73237d41::result::Result::Err::0","ty":"ty::Adt::8d47b311e48cbf8f"}],"inhabited":true,"name":"core/73237d41::result::Result::Err"}]},{"kind":{"kind":"Struct"},"name":"core/73237d41::fmt::rt::v1::Argument::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::Argument","orig_substs":[],"repr_transparent":false,"size":56,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"core/73237d41::fmt::rt::v1::Argument::position","ty":"ty::usize"},{"name":"core/73237d41::fmt::rt::v1::Argument::format","ty":"ty::Adt::ed8948c5d0b3a39f"}],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Argument"}]},{"kind":{"kind":"Struct"},"name":"core/73237d41::fmt::Formatter::_adtbd21306cbe4f0b9b[0]","orig_def_id":"core/73237d41::fmt::Formatter","orig_substs":["nonty::Lifetime"],"repr_transparent":false,"size":64,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"core/73237d41::fmt::Formatter::flags","ty":"ty::u32"},{"name":"core/73237d41::fmt::Formatter::fill","ty":"ty::char"},{"name":"core/73237d41::fmt::Formatter::align","ty":"ty::Adt::c4745d1cf6b33a46"},{"name":"core/73237d41::fmt::Formatter::width","ty":"ty::Adt::ba42a94c73933868"},{"name":"core/73237d41::fmt::Formatter::precision","ty":"ty::Adt::ba42a94c73933868"},{"name":"core/73237d41::fmt::Formatter::buf","ty":"ty::Ref::0cd866b4eb1c792b"}],"inhabited":true,"name":"core/73237d41::fmt::Formatter"}]},{"kind":{"kind":"Struct"},"name":"core/73237d41::fmt::rt::v1::FormatSpec::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::FormatSpec","orig_substs":[],"repr_transparent":false,"size":48,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"core/73237d41::fmt::rt::v1::FormatSpec::fill","ty":"ty::char"},{"name":"core/73237d41::fmt::rt::v1::FormatSpec::align","ty":"ty::Adt::c4745d1cf6b33a46"},{"name":"core/73237d41::fmt::rt::v1::FormatSpec::flags","ty":"ty::u32"},{"name":"core/73237d41::fmt::rt::v1::FormatSpec::precision","ty":"ty::Adt::389b970f3565f26b"},{"name":"core/73237d41::fmt::rt::v1::FormatSpec::width","ty":"ty::Adt::389b970f3565f26b"}],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::FormatSpec"}]},{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"core/73237d41::fmt::rt::v1::Alignment::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::Alignment","orig_substs":[],"repr_transparent":false,"size":1,"variants":[{"ctor_kind":{"kind":"Const"},"discr":{"index":0,"kind":"Relative"},"discr_value":"0","fields":[],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Alignment::Left"},{"ctor_kind":{"kind":"Const"},"discr":{"index":1,"kind":"Relative"},"discr_value":"1","fields":[],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Alignment::Right"},{"ctor_kind":{"kind":"Const"},"discr":{"index":2,"kind":"Relative"},"discr_value":"2","fields":[],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Alignment::Center"},{"ctor_kind":{"kind":"Const"},"discr":{"index":3,"kind":"Relative"},"discr_value":"3","fields":[],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Alignment::Unknown"}]},{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"core/73237d41::option::Option::_adtaffa7a8b1157c078[0]","orig_def_id":"core/73237d41::option::Option","orig_substs":["ty::usize"],"repr_transparent":false,"size":16,"variants":[{"ctor_kind":{"kind":"Const"},"discr":{"index":0,"kind":"Relative"},"discr_value":"0","fields":[],"inhabited":true,"name":"core/73237d41::option::Option::None"},{"ctor_kind":{"kind":"Fn"},"discr":{"index":1,"kind":"Relative"},"discr_value":"1","fields":[{"name":"core/73237d41::option::Option::Some::0","ty":"ty::usize"}],"inhabited":true,"name":"core/73237d41::option::Option::Some"}]},{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"core/73237d41::fmt::rt::v1::Count::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::Count","orig_substs":[],"repr_transparent":false,"size":16,"variants":[{"ctor_kind":{"kind":"Fn"},"discr":{"index":0,"kind":"Relative"},"discr_value":"0","fields":[{"name":"core/73237d41::fmt::rt::v1::Count::Is::0","ty":"ty::usize"}],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Count::Is"},{"ctor_kind":{"kind":"Fn"},"discr":{"index":1,"kind":"Relative"},"discr_value":"1","fields":[{"name":"core/73237d41::fmt::rt::v1::Count::Param::0","ty":"ty::usize"}],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Count::Param"},{"ctor_kind":{"kind":"Const"},"discr":{"index":2,"kind":"Relative"},"discr_value":"2","fields":[],"inhabited":true,"name":"core/73237d41::fmt::rt::v1::Count::Implied"}]}],"statics":[{"kind":"constant","mutable":false,"name":"mir_ghost/150ed4465f8cb026::{{alloc}}[0]","rendered":{"element_ty":"ty::Ref::fb1cfdc5725cd03b","elements":[{"kind":"str","val":[110,111,116,32,105,109,112,108,101,109,101,110,116,101,100,58,32]}],"kind":"array"},"ty":"ty::Array::e5bd840a2dafa04a"},{"kind":"constant","mutable":false,"name":"mir_ghost/150ed4465f8cb026::{{alloc}}[1]","rendered":{"element_ty":"ty::Ref::fb1cfdc5725cd03b","elements":[{"kind":"str","val":[84,104,105,115,32,115,104,111,117,108,100,32,98,101,32,111,118,101,114,114,105,100,100,101,110]}],"kind":"array"},"ty":"ty::Array::e5bd840a2dafa04a"},{"kind":"constant","mutable":false,"name":"mir_ghost/150ed4465f8cb026::{{alloc}}[2]","rendered":{"element_ty":"ty::Adt::613f1953a8669d14","elements":[],"kind":"array"},"ty":"ty::Array::0e1a52ee2b2d3e97"},{"kind":"constant","mutable":false,"name":"mir_ghost/150ed4465f8cb026::{{alloc}}[3]","rendered":{"element_ty":"ty::Ref::fb1cfdc5725cd03b","elements":[{"kind":"str","val":[105,110,118,97,108,105,100,32,97,114,103,115]}],"kind":"array"},"ty":"ty::Array::e5bd840a2dafa04a"}],"vtables":[],"traits":[{"items":[{"item_id":"core/73237d41::fmt::Write::write_str","kind":"Method","signature":{"abi":{"kind":"Rust"},"inputs":["ty::Ref::0cd866b4eb1c792b","ty::Ref::fb1cfdc5725cd03b"],"output":"ty::Adt::30ed5848b4f625b6"}},{"item_id":"core/73237d41::fmt::Write::write_char","kind":"Method","signature":{"abi":{"kind":"Rust"},"inputs":["ty::Ref::0cd866b4eb1c792b","ty::char"],"output":"ty::Adt::30ed5848b4f625b6"}},{"item_id":"core/73237d41::fmt::Write::write_fmt","kind":"Method","signature":{"abi":{"kind":"Rust"},"inputs":["ty::Ref::0cd866b4eb1c792b","ty::Adt::ba5184b53bc36a4d"],"output":"ty::Adt::30ed5848b4f625b6"}}],"name":"core/73237d41::fmt::Write::_trait3e5b0354795cc029[0]"}],"intrinsics":[{"inst":{"def_id":"mir_ghost/150ed446::example","kind":"Item","substs":[]},"name":"mir_ghost/150ed446::example"},{"inst":{"def_id":"mir_ghost/150ed446::next","kind":"Item","substs":[]},"name":"mir_ghost/150ed446::next"},{"inst":{"def_id":"core/73237d41::fmt::{impl#3}::new_display","kind":"Item","substs":["nonty::Lifetime","ty::Adt::ba5184b53bc36a4d"]},"name":"core/73237d41::fmt::{impl#3}::new_display::_inst47ac314b85a79c82[0]"},{"inst":{"def_id":"core/73237d41::fmt::{impl#4}::new_v1","kind":"Item","substs":["nonty::Lifetime"]},"name":"core/73237d41::fmt::{impl#4}::new_v1::_instbd21306cbe4f0b9b[0]"},{"inst":{"def_id":"core/73237d41::panicking::panic_fmt","kind":"Item","substs":[]},"name":"core/73237d41::panicking::panic_fmt"},{"inst":{"def_id":"core/73237d41::intrinsics::{extern#0}::transmute","kind":"Intrinsic","substs":["ty::Ref::bf4d6d337c623aee","ty::Ref::4e8e6a61a1ceb622"]},"name":"core/73237d41::intrinsics::{extern#0}::transmute::_inst79e1dbb43599bccf[0]"},{"inst":{"def_id":"core/73237d41::intrinsics::{extern#0}::transmute","kind":"Intrinsic","substs":["ty::FnPtr::07cd89921cc84271","ty::FnPtr::bd6bee7b1f95b7bf"]},"name":"core/73237d41::intrinsics::{extern#0}::transmute::_inst82602b44b15ef1cb[0]"},{"inst":{"def_id":"core/73237d41::fmt::{impl#7}::fmt","kind":"Item","substs":["nonty::Lifetime"]},"name":"core/73237d41::fmt::{impl#7}::fmt::_instbd21306cbe4f0b9b[0]"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::FnDef::ae5488df1dc4e585","ty":{"defid":"mir_ghost/150ed446::next","kind":"FnDef"}},{"name":"ty::Never::7199a9b06188843c","ty":{"kind":"Never"}},{"name":"ty::Adt::ba5184b53bc36a4d","ty":{"kind":"Adt","name":"core/73237d41::fmt::Arguments::_adtbd21306cbe4f0b9b[0]","orig_def_id":"core/73237d41::fmt::Arguments","substs":["nonty::Lifetime"]}},{"name":"ty::str","ty":{"kind":"Str"}},{"name":"ty::Ref::fb1cfdc5725cd03b","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::str"}},{"name":"ty::Slice::563a94fdd2fd2b33","ty":{"kind":"Slice","ty":"ty::Ref::fb1cfdc5725cd03b"}},{"name":"ty::Ref::675b2a8049aad652","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Slice::563a94fdd2fd2b33"}},{"name":"ty::usize","ty":{"kind":"Uint","uintkind":{"kind":"Usize"}}},{"name":"ty::Array::e5bd840a2dafa04a","ty":{"kind":"Array","size":{"rendered":{"kind":"usize","size":8,"val":"1"},"ty":"ty::usize"},"ty":"ty::Ref::fb1cfdc5725cd03b"}},{"name":"ty::Ref::c2a5dcbb98af2a61","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Array::e5bd840a2dafa04a"}},{"name":"ty::Adt::613f1953a8669d14","ty":{"kind":"Adt","name":"core/73237d41::fmt::ArgumentV1::_adtbd21306cbe4f0b9b[0]","orig_def_id":"core/73237d41::fmt::ArgumentV1","substs":["nonty::Lifetime"]}},{"name":"ty::Slice::818a2c6d5f962f99","ty":{"kind":"Slice","ty":"ty::Adt::613f1953a8669d14"}},{"name":"ty::Ref::913e2ff5487f7787","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Slice::818a2c6d5f962f99"}},{"name":"ty::Array::6167cd8fdeb01e06","ty":{"kind":"Array","size":{"rendered":{"kind":"usize","size":8,"val":"1"},"ty":"ty::usize"},"ty":"ty::Adt::613f1953a8669d14"}},{"name":"ty::Ref::41f3f8f95d02c3e9","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Array::6167cd8fdeb01e06"}},{"name":"ty::Ref::bf4d6d337c623aee","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Adt::ba5184b53bc36a4d"}},{"name":"ty::Array::0e1a52ee2b2d3e97","ty":{"kind":"Array","size":{"rendered":{"kind":"usize","size":8,"val":"0"},"ty":"ty::usize"},"ty":"ty::Adt::613f1953a8669d14"}},{"name":"ty::Ref::d0bd7bf253977b90","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Array::0e1a52ee2b2d3e97"}},{"name":"ty::FnDef::76afb566734aff77","ty":{"defid":"core/73237d41::fmt::{impl#4}::new_v1::_instbd21306cbe4f0b9b[0]","kind":"FnDef"}},{"name":"ty::FnDef::72bf0f6662028c6a","ty":{"defid":"core/73237d41::fmt::{impl#3}::new_display::_inst47ac314b85a79c82[0]","kind":"FnDef"}},{"name":"ty::FnDef::906e67453a1bbab9","ty":{"defid":"core/73237d41::panicking::panic_fmt","kind":"FnDef"}},{"name":"ty::Adt::afb4c9f4ce8cdadf","ty":{"kind":"Adt","name":"core/73237d41::fmt::rt::v1::Argument::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::Argument","substs":[]}},{"name":"ty::Slice::26b8a0a5e2b22aa9","ty":{"kind":"Slice","ty":"ty::Adt::afb4c9f4ce8cdadf"}},{"name":"ty::Ref::5f3877d5405402c5","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Slice::26b8a0a5e2b22aa9"}},{"name":"ty::Adt::45883e75bd5c5ca5","ty":{"kind":"Adt","name":"core/73237d41::option::Option::_adta9d03177c2d4a99f[0]","orig_def_id":"core/73237d41::option::Option","substs":["ty::Ref::5f3877d5405402c5"]}},{"name":"ty::Foreign::66d9923797cfc204","ty":{"kind":"Foreign"}},{"name":"ty::Ref::4e8e6a61a1ceb622","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Foreign::66d9923797cfc204"}},{"name":"ty::Adt::ad5a554022507816","ty":{"kind":"Adt","name":"core/73237d41::fmt::Formatter::_adtbd21306cbe4f0b9b[0]","orig_def_id":"core/73237d41::fmt::Formatter","substs":["nonty::Lifetime"]}},{"name":"ty::Ref::7984c7d8fa40d865","ty":{"kind":"Ref","mutability":{"kind":"Mut"},"ty":"ty::Adt::ad5a554022507816"}},{"name":"ty::Tuple::e93222e871854c41","ty":{"kind":"Tuple","tys":[]}},{"name":"ty::Adt::8d47b311e48cbf8f","ty":{"kind":"Adt","name":"core/73237d41::fmt::Error::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::Error","substs":[]}},{"name":"ty::Adt::30ed5848b4f625b6","ty":{"kind":"Adt","name":"core/73237d41::result::Result::_adt0f6d5765b4e92fb6[0]","orig_def_id":"core/73237d41::result::Result","substs":["ty::Tuple::e93222e871854c41","ty::Adt::8d47b311e48cbf8f"]}},{"name":"ty::FnPtr::bd6bee7b1f95b7bf","ty":{"kind":"FnPtr","signature":{"abi":{"kind":"Rust"},"inputs":["ty::Ref::4e8e6a61a1ceb622","ty::Ref::7984c7d8fa40d865"],"output":"ty::Adt::30ed5848b4f625b6"}}},{"name":"ty::FnPtr::07cd89921cc84271","ty":{"kind":"FnPtr","signature":{"abi":{"kind":"Rust"},"inputs":["ty::Ref::bf4d6d337c623aee","ty::Ref::7984c7d8fa40d865"],"output":"ty::Adt::30ed5848b4f625b6"}}},{"name":"ty::FnDef::b30b83d63051810b","ty":{"defid":"core/73237d41::fmt::{impl#7}::fmt::_instbd21306cbe4f0b9b[0]","kind":"FnDef"}},{"name":"ty::FnDef::788a983faed72be6","ty":{"defid":"core/73237d41::intrinsics::{extern#0}::transmute::_inst82602b44b15ef1cb[0]","kind":"FnDef"}},{"name":"ty::FnDef::f532a620418c4246","ty":{"defid":"core/73237d41::intrinsics::{extern#0}::transmute::_inst79e1dbb43599bccf[0]","kind":"FnDef"}},{"name":"ty::bool","ty":{"kind":"Bool"}},{"name":"ty::isize","ty":{"intkind":{"kind":"Isize"},"kind":"Int"}},{"name":"ty::Adt::ed8948c5d0b3a39f","ty":{"kind":"Adt","name":"core/73237d41::fmt::rt::v1::FormatSpec::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::FormatSpec","substs":[]}},{"name":"ty::char","ty":{"kind":"Char"}},{"name":"ty::Adt::c4745d1cf6b33a46","ty":{"kind":"Adt","name":"core/73237d41::fmt::rt::v1::Alignment::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::Alignment","substs":[]}},{"name":"ty::Adt::ba42a94c73933868","ty":{"kind":"Adt","name":"core/73237d41::option::Option::_adtaffa7a8b1157c078[0]","orig_def_id":"core/73237d41::option::Option","substs":["ty::usize"]}},{"name":"ty::Dynamic::08a22e65af9638be","ty":{"kind":"Dynamic","predicates":[{"kind":"Trait","substs":[],"trait":"core/73237d41::fmt::Write"}],"trait_id":"core/73237d41::fmt::Write::_trait3e5b0354795cc029[0]"}},{"name":"ty::Ref::0cd866b4eb1c792b","ty":{"kind":"Ref","mutability":{"kind":"Mut"},"ty":"ty::Dynamic::08a22e65af9638be"}},{"name":"ty::Adt::389b970f3565f26b","ty":{"kind":"Adt","name":"core/73237d41::fmt::rt::v1::Count::_adtb7803c2264daf0ec[0]","orig_def_id":"core/73237d41::fmt::rt::v1::Count","substs":[]}}],"roots":["mir_ghost/150ed446::next","mir_ghost/150ed446::example"]} \ No newline at end of file diff --git a/saw-remote-api/python/tests/saw/test-files/mir_ghost.rs b/saw-remote-api/python/tests/saw/test-files/mir_ghost.rs new file mode 100644 index 0000000000..fafa13669c --- /dev/null +++ b/saw-remote-api/python/tests/saw/test-files/mir_ghost.rs @@ -0,0 +1,9 @@ +pub fn next() -> u32 { + unimplemented!("This should be overridden") +} + +pub fn example() -> u32 { + next(); + next(); + next() +} diff --git a/saw-remote-api/python/tests/saw/test_mir_ghost.py b/saw-remote-api/python/tests/saw/test_mir_ghost.py new file mode 100644 index 0000000000..3d4e388cad --- /dev/null +++ b/saw-remote-api/python/tests/saw/test_mir_ghost.py @@ -0,0 +1,53 @@ +import unittest +from pathlib import Path + +from saw_client import * +from saw_client.crucible import cry_f +from saw_client.mir import Contract, GhostVariable, u32 + + +class NextContract(Contract): + def __init__(self, counter: GhostVariable) -> None: + super().__init__() + self.counter = counter + + def specification(self) -> None: + n = self.fresh_var(u32, 'n') + self.ghost_value(self.counter, n) + + self.execute_func() + + self.ghost_value(self.counter, cry_f('{n} + 1')) + self.returns(n) + + +class ExampleContract(Contract): + def __init__(self, counter: GhostVariable) -> None: + super().__init__() + self.counter = counter + + def specification(self) -> None: + n = self.fresh_var(u32, 'n') + self.precondition_f('{n} < 2') + self.ghost_value(self.counter, n) + + self.execute_func() + self.ghost_value(self.counter, cry_f('{n} + 3')) + self.returns_f('{n} + 2') + + +class MIRGhostTest(unittest.TestCase): + def test_mir_ghost(self): + connect(reset_server=True) + if __name__ == "__main__": view(LogResults()) + json_name = str(Path('tests', 'saw', 'test-files', 'mir_ghost.linked-mir.json')) + mod = mir_load_module(json_name) + + counter = create_ghost_variable('ctr'); + next_ov = mir_assume(mod, 'mir_ghost::next', NextContract(counter)) + example_result = mir_verify(mod, 'mir_ghost::example', ExampleContract(counter), lemmas=[next_ov]) + self.assertIs(example_result.is_success(), True) + + +if __name__ == "__main__": + unittest.main() diff --git a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs index c601974f4a..8262e46c81 100644 --- a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs @@ -26,7 +26,7 @@ import qualified Data.Map as Map import qualified Cryptol.Parser.AST as P import Cryptol.Utils.Ident (mkIdent) import qualified Lang.Crucible.JVM as CJ -import SAWScript.Crucible.Common.MethodSpec as MS (SetupValue(..)) +import qualified SAWScript.Crucible.Common.MethodSpec as MS import SAWScript.Crucible.JVM.Builtins ( jvm_alloc_array, jvm_alloc_object, @@ -35,6 +35,7 @@ import SAWScript.Crucible.JVM.Builtins jvm_static_field_is, jvm_execute_func, jvm_fresh_var, + jvm_ghost_value, jvm_postcond, jvm_precond, jvm_return ) @@ -56,10 +57,11 @@ import SAWServer import SAWServer.Data.Contract ( PointsTo(PointsTo), PointsToBitfield, + GhostValue(GhostValue), Allocated(Allocated), ContractVar(ContractVar), - Contract(preVars, preConds, preAllocated, prePointsTos, prePointsToBitfields, - argumentVals, postVars, postConds, postAllocated, postPointsTos, postPointsToBitfields, + Contract(preVars, preConds, preAllocated, preGhostValues, prePointsTos, prePointsToBitfields, + argumentVals, postVars, postConds, postAllocated, postGhostValues, postPointsTos, postPointsToBitfields, returnVal) ) import SAWServer.Data.SetupValue () import SAWServer.CryptolExpression (CryptolModuleException(..), getTypedTermOfCExp) @@ -82,28 +84,29 @@ instance Doc.DescribedMethod StartJVMSetupParams OK where ] resultFieldDescription = [] -newtype ServerSetupVal = Val (SetupValue CJ.JVM) +newtype ServerSetupVal = Val (MS.SetupValue CJ.JVM) compileJVMContract :: (FilePath -> IO ByteString) -> BuiltinContext -> + Map ServerName MS.GhostGlobal -> CryptolEnv -> Contract JavaType (P.Expr P.PName) -> JVMSetupM () -compileJVMContract fileReader bic cenv0 c = +compileJVMContract fileReader bic ghostEnv cenv0 c = do allocsPre <- mapM setupAlloc (preAllocated c) (envPre, cenvPre) <- setupState allocsPre (Map.empty, cenv0) (preVars c) mapM_ (\p -> getTypedTerm cenvPre p >>= jvm_precond) (preConds c) mapM_ (setupPointsTo (envPre, cenvPre)) (prePointsTos c) mapM_ setupPointsToBitfields (prePointsToBitfields c) - --mapM_ (setupGhostValue ghostEnv cenvPre) (preGhostValues c) + mapM_ (setupGhostValue ghostEnv cenvPre) (preGhostValues c) traverse (getSetupVal (envPre, cenvPre)) (argumentVals c) >>= jvm_execute_func allocsPost <- mapM setupAlloc (postAllocated c) (envPost, cenvPost) <- setupState (allocsPre ++ allocsPost) (envPre, cenvPre) (postVars c) mapM_ (\p -> getTypedTerm cenvPost p >>= jvm_postcond) (postConds c) mapM_ (setupPointsTo (envPost, cenvPost)) (postPointsTos c) mapM_ setupPointsToBitfields (postPointsToBitfields c) - --mapM_ (setupGhostValue ghostEnv cenvPost) (postGhostValues c) + mapM_ (setupGhostValue ghostEnv cenvPost) (postGhostValues c) case returnVal c of Just v -> getSetupVal (envPost, cenvPost) v >>= jvm_return Nothing -> return () @@ -149,7 +152,10 @@ compileJVMContract fileReader bic cenv0 c = setupPointsToBitfields _ = JVMSetupM $ fail "Points-to-bitfield not supported in JVM API." - --setupGhostValue _ _ _ = fail "Ghost values not supported yet in JVM API." + setupGhostValue genv cenv (GhostValue serverName e) = + do g <- resolve genv serverName + t <- getTypedTerm cenv e + jvm_ghost_value g t resolve :: Map ServerName a -> ServerName -> JVMSetupM a resolve env name = diff --git a/saw-remote-api/src/SAWServer/JVMVerify.hs b/saw-remote-api/src/SAWServer/JVMVerify.hs index f7c97654ed..293d424e79 100644 --- a/saw-remote-api/src/SAWServer/JVMVerify.hs +++ b/saw-remote-api/src/SAWServer/JVMVerify.hs @@ -9,6 +9,7 @@ module SAWServer.JVMVerify import Prelude hiding (mod) import Control.Lens +import qualified Data.Map as Map import SAWScript.Crucible.JVM.Builtins ( jvm_unsafe_assume_spec, jvm_verify ) @@ -26,6 +27,7 @@ import SAWServer pushTask, dropTask, setServerVal, + getGhosts, getJVMClass, getJVMMethodSpecIR ) import SAWServer.CryptolExpression (getCryptolExpr) @@ -51,7 +53,8 @@ jvmVerifyAssume mode (VerifyParams className fun lemmaNames checkSat contract sc let bic = view sawBIC state cenv = rwCryptol (view sawTopLevelRW state) fileReader <- Argo.getFileReader - setup <- compileJVMContract fileReader bic cenv <$> traverse getCryptolExpr contract + ghostEnv <- Map.fromList <$> getGhosts + setup <- compileJVMContract fileReader bic ghostEnv cenv <$> traverse getCryptolExpr contract res <- case mode of VerifyContract -> do lemmas <- mapM getJVMMethodSpecIR lemmaNames diff --git a/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs b/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs index a1ce2f07d3..b6cf3555df 100644 --- a/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs @@ -31,6 +31,7 @@ import SAWScript.Crucible.MIR.Builtins mir_fresh_expanded_value, mir_fresh_var, mir_execute_func, + mir_ghost_value, mir_load_module, mir_points_to, mir_postcond, @@ -58,10 +59,11 @@ import SAWServer.CryptolExpression (CryptolModuleException(..), getTypedTermOfCE import SAWServer.Data.Contract ( PointsTo(PointsTo), PointsToBitfield, + GhostValue(GhostValue), Allocated(Allocated), ContractVar(ContractVar), - Contract(preVars, preConds, preAllocated, prePointsTos, prePointsToBitfields, - argumentVals, postVars, postConds, postAllocated, postPointsTos, postPointsToBitfields, + Contract(preVars, preConds, preAllocated, preGhostValues, prePointsTos, prePointsToBitfields, + argumentVals, postVars, postConds, postAllocated, postGhostValues, postPointsTos, postPointsToBitfields, returnVal) ) import SAWServer.Data.MIRType (JSONMIRType, mirType) import SAWServer.Exceptions ( notAtTopLevel ) @@ -74,24 +76,25 @@ newtype ServerSetupVal = Val (MS.SetupValue MIR) compileMIRContract :: (FilePath -> IO ByteString) -> BuiltinContext -> + Map ServerName MS.GhostGlobal -> CryptolEnv -> SAWEnv -> Contract JSONMIRType (P.Expr P.PName) -> MIRSetupM () -compileMIRContract fileReader bic cenv0 sawenv c = +compileMIRContract fileReader bic ghostEnv cenv0 sawenv c = do allocsPre <- mapM setupAlloc (preAllocated c) (envPre, cenvPre) <- setupState allocsPre (Map.empty, cenv0) (preVars c) mapM_ (\p -> getTypedTerm cenvPre p >>= mir_precond) (preConds c) mapM_ (setupPointsTo (envPre, cenvPre)) (prePointsTos c) mapM_ setupPointsToBitfields (prePointsToBitfields c) - --mapM_ (setupGhostValue ghostEnv cenvPre) (preGhostValues c) + mapM_ (setupGhostValue ghostEnv cenvPre) (preGhostValues c) traverse (getSetupVal (envPre, cenvPre)) (argumentVals c) >>= mir_execute_func allocsPost <- mapM setupAlloc (postAllocated c) (envPost, cenvPost) <- setupState (allocsPre ++ allocsPost) (envPre, cenvPre) (postVars c) mapM_ (\p -> getTypedTerm cenvPost p >>= mir_postcond) (postConds c) mapM_ (setupPointsTo (envPost, cenvPost)) (postPointsTos c) mapM_ setupPointsToBitfields (postPointsToBitfields c) - --mapM_ (setupGhostValue ghostEnv cenvPost) (postGhostValues c) + mapM_ (setupGhostValue ghostEnv cenvPost) (postGhostValues c) case returnVal c of Just v -> getSetupVal (envPost, cenvPost) v >>= mir_return Nothing -> return () @@ -136,7 +139,10 @@ compileMIRContract fileReader bic cenv0 sawenv c = setupPointsToBitfields _ = MIRSetupM $ fail "Points-to-bitfield not supported in the MIR API." - --setupGhostValue _ _ _ = fail "Ghost values not supported yet in the MIR API." + setupGhostValue genv cenv (GhostValue serverName e) = + do g <- resolve genv serverName + t <- getTypedTerm cenv e + mir_ghost_value g t resolve :: Map ServerName a -> ServerName -> MIRSetupM a resolve env name = diff --git a/saw-remote-api/src/SAWServer/MIRVerify.hs b/saw-remote-api/src/SAWServer/MIRVerify.hs index 5106396341..f3bf31e447 100644 --- a/saw-remote-api/src/SAWServer/MIRVerify.hs +++ b/saw-remote-api/src/SAWServer/MIRVerify.hs @@ -9,6 +9,7 @@ module SAWServer.MIRVerify import Prelude hiding (mod) import Control.Lens +import qualified Data.Map as Map import SAWScript.Crucible.MIR.Builtins ( mir_unsafe_assume_spec, mir_verify ) @@ -26,6 +27,7 @@ import SAWServer pushTask, dropTask, setServerVal, + getGhosts, getMIRModule, getMIRMethodSpecIR ) import SAWServer.CryptolExpression (getCryptolExpr) @@ -53,7 +55,8 @@ mirVerifyAssume mode (VerifyParams modName fun lemmaNames checkSat contract scri cenv = rwCryptol (view sawTopLevelRW state) sawenv = view sawEnv state fileReader <- Argo.getFileReader - setup <- compileMIRContract fileReader bic cenv sawenv <$> + ghostEnv <- Map.fromList <$> getGhosts + setup <- compileMIRContract fileReader bic ghostEnv cenv sawenv <$> traverse getCryptolExpr contract res <- case mode of VerifyContract -> do diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index 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 e8ce39d657..acba975084 100644 --- a/src/SAWScript/Crucible/Common/MethodSpec.hs +++ b/src/SAWScript/Crucible/Common/MethodSpec.hs @@ -13,8 +13,10 @@ Grow\", and is prevalent across the Crucible codebase. {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} @@ -22,6 +24,7 @@ Grow\", and is prevalent across the Crucible codebase. {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeFamilyDependencies #-} {-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -Wno-orphans #-} module SAWScript.Crucible.Common.MethodSpec ( AllocIndex(..) @@ -62,7 +65,6 @@ module SAWScript.Crucible.Common.MethodSpec , setupToTypedTerm , setupToTerm - , XGhostState , GhostValue , GhostType , GhostGlobal @@ -118,6 +120,7 @@ import Data.Set (Set) import Data.Time.Clock import Data.Void (absurd) +import Control.Monad (when) import Control.Monad.Trans.Maybe import Control.Monad.Trans (lift) import Control.Lens @@ -132,13 +135,17 @@ import Lang.Crucible.JVM (JVM) import qualified Lang.Crucible.Types as Crucible (IntrinsicType, EmptyCtx) import qualified Lang.Crucible.CFG.Common as Crucible (GlobalVar) +import qualified Lang.Crucible.Simulator.Intrinsics as Crucible import Mir.Intrinsics (MIR) +import qualified Cryptol.TypeCheck.Type as Cryptol (Schema) import qualified Cryptol.Utils.PP as Cryptol import Verifier.SAW.TypedTerm as SAWVerifier import Verifier.SAW.SharedTerm as SAWVerifier +import Verifier.SAW.Simulator.What4.ReturnTrip as SAWVerifier +import SAWScript.Crucible.Common (Sym, sawCoreState) import SAWScript.Crucible.Common.Setup.Value import SAWScript.Crucible.LLVM.Setup.Value (LLVM) import SAWScript.Crucible.JVM.Setup.Value () @@ -344,21 +351,33 @@ type GhostValue = "GhostValue" type GhostType = Crucible.IntrinsicType GhostValue Crucible.EmptyCtx type GhostGlobal = Crucible.GlobalVar GhostType +instance Crucible.IntrinsicClass Sym GhostValue where + type Intrinsic Sym GhostValue ctx = (Cryptol.Schema, Term) + muxIntrinsic sym _ _namerep _ctx prd (thnSch,thn) (elsSch,els) = + do when (thnSch /= elsSch) $ fail $ unlines $ + [ "Attempted to mux ghost variables of different types:" + , show (Cryptol.pp thnSch) + , show (Cryptol.pp elsSch) + ] + st <- sawCoreState sym + let sc = saw_ctx st + prd' <- toSC sym st prd + typ <- scTypeOf sc thn + res <- scIte sc typ prd' thn els + return (thnSch, res) + -------------------------------------------------------------------------------- -- *** StateSpec data SetupCondition ext where SetupCond_Equal :: ConditionMetadata -> SetupValue ext -> SetupValue ext -> SetupCondition ext SetupCond_Pred :: ConditionMetadata -> TypedTerm -> SetupCondition ext - SetupCond_Ghost :: XGhostState ext -> - ConditionMetadata -> + SetupCond_Ghost :: ConditionMetadata -> GhostGlobal -> TypedTerm -> SetupCondition ext -deriving instance ( SetupValueHas Show ext - , Show (XGhostState ext) - ) => Show (SetupCondition ext) +deriving instance SetupValueHas Show ext => Show (SetupCondition ext) -- | Verification state (either pre- or post-) specification data StateSpec ext = StateSpec diff --git a/src/SAWScript/Crucible/Common/Override.hs b/src/SAWScript/Crucible/Common/Override.hs index 48d31e1b66..fac57dcb20 100644 --- a/src/SAWScript/Crucible/Common/Override.hs +++ b/src/SAWScript/Crucible/Common/Override.hs @@ -65,11 +65,16 @@ module SAWScript.Crucible.Common.Override -- , assignmentToList , MetadataMap + -- + , learnGhost + , executeGhost + , instantiateExtMatchTerm + , matchTerm ) where import qualified Control.Exception as X import Control.Lens -import Control.Monad (foldM, unless) +import Control.Monad (foldM, unless, when) import Control.Monad.Trans.State hiding (get, put) import Control.Monad.State.Class (MonadState(..)) import Control.Monad.Error.Class (MonadError) @@ -82,6 +87,7 @@ import qualified Data.Map as Map import Data.Map (Map) import Data.Maybe (fromMaybe) import Data.Proxy (Proxy(..)) +import qualified Data.Set as Set import Data.Set (Set) import Data.Typeable (Typeable) import Data.Void @@ -92,10 +98,13 @@ import qualified Data.Parameterized.Context as Ctx import Data.Parameterized.Some (Some) import Data.Parameterized.TraversableFC (toListFC) +import Verifier.SAW.Prelude as SAWVerifier (scEq) import Verifier.SAW.SharedTerm as SAWVerifier import Verifier.SAW.TypedAST as SAWVerifier import Verifier.SAW.TypedTerm as SAWVerifier +import qualified Cryptol.Utils.PP as Cryptol (pp) + import qualified Lang.Crucible.Backend as Crucible import qualified Lang.Crucible.Backend.Online as Crucible import qualified Lang.Crucible.CFG.Core as Crucible (TypeRepr, GlobalVar) @@ -529,3 +538,102 @@ assignmentToList :: Ctx.Assignment (Crucible.RegEntry sym) ctx -> [Crucible.AnyValue sym] assignmentToList = toListFC (\(Crucible.RegEntry x y) -> Crucible.AnyValue x y) + +------------------------------------------------------------------------ + +learnGhost :: + SharedContext -> + MS.ConditionMetadata -> + PrePost -> + MS.GhostGlobal -> + TypedTerm -> + OverrideMatcher ext md () +learnGhost sc md prepost var (TypedTerm (TypedTermSchema schEx) tmEx) = + do (sch,tm) <- readGlobal var + when (sch /= schEx) $ fail $ unlines $ + [ "Ghost variable had the wrong type:" + , "- Expected: " ++ show (Cryptol.pp schEx) + , "- Actual: " ++ show (Cryptol.pp sch) + ] + instantiateExtMatchTerm sc md prepost tm tmEx +learnGhost _sc _md _prepost _var (TypedTerm tp _) + = fail $ unlines + [ "Ghost variable expected value has improper type" + , "expected Cryptol schema type, but got" + , show (MS.ppTypedTermType tp) + ] + +executeGhost :: + SharedContext -> + MS.ConditionMetadata -> + MS.GhostGlobal -> + TypedTerm -> + OverrideMatcher ext RW () +executeGhost sc _md var (TypedTerm (TypedTermSchema sch) tm) = + do s <- OM (use termSub) + tm' <- liftIO (scInstantiateExt sc s tm) + writeGlobal var (sch,tm') +executeGhost _sc _md _var (TypedTerm tp _) = + fail $ unlines + [ "executeGhost: improper value type" + , "expected Cryptol schema type, but got" + , show (MS.ppTypedTermType tp) + ] + +-- | NOTE: The two 'Term' arguments must have the same type. +instantiateExtMatchTerm :: + SharedContext {- ^ context for constructing SAW terms -} -> + MS.ConditionMetadata -> + PrePost -> + Term {- ^ exported concrete term -} -> + Term {- ^ expected specification term -} -> + OverrideMatcher ext md () +instantiateExtMatchTerm sc md prepost actual expected = do + sub <- OM (use termSub) + matchTerm sc md prepost actual =<< liftIO (scInstantiateExt sc sub expected) + +matchTerm :: + SharedContext {- ^ context for constructing SAW terms -} -> + MS.ConditionMetadata -> + PrePost -> + Term {- ^ exported concrete term -} -> + Term {- ^ expected specification term -} -> + OverrideMatcher ext md () + +matchTerm _ _ _ real expect | real == expect = return () +matchTerm sc md prepost real expect = + do let loc = MS.conditionLoc md + free <- OM (use osFree) + case unwrapTermF expect of + FTermF (ExtCns ec) + | Set.member (ecVarIndex ec) free -> + do assignTerm sc md prepost (ecVarIndex ec) real + + _ -> + do t <- liftIO $ scEq sc real expect + let msg = unlines $ + [ "Literal equality " ++ MS.stateCond prepost +-- , "Expected term: " ++ prettyTerm expect +-- , "Actual term: " ++ prettyTerm real + ] + addTermEq t md $ Crucible.SimError loc $ Crucible.AssertFailureSimError msg "" +-- where prettyTerm = show . ppTermDepth 20 + +assignTerm :: + SharedContext {- ^ context for constructing SAW terms -} -> + MS.ConditionMetadata -> + PrePost -> + VarIndex {- ^ external constant index -} -> + Term {- ^ value -} -> + OverrideMatcher ext md () + +assignTerm sc md prepost var val = + do mb <- OM (use (termSub . at var)) + case mb of + Nothing -> OM (termSub . at var ?= val) + Just old -> + matchTerm sc md prepost val old + +-- do t <- liftIO $ scEq sc old val +-- p <- liftIO $ resolveSAWPred cc t +-- addAssert p (Crucible.AssertFailureSimError ("literal equality " ++ MS.stateCond prepost)) diff --git a/src/SAWScript/Crucible/Common/Setup/Value.hs b/src/SAWScript/Crucible/Common/Setup/Value.hs index 505acce1c9..b9fa6ebcde 100644 --- a/src/SAWScript/Crucible/Common/Setup/Value.hs +++ b/src/SAWScript/Crucible/Common/Setup/Value.hs @@ -51,8 +51,6 @@ module SAWScript.Crucible.Common.Setup.Value , SetupValue(..) , SetupValueHas - , XGhostState - , ConditionMetadata(..) , MethodId @@ -185,15 +183,6 @@ deriving instance (SetupValueHas Show ext) => Show (SetupValue ext) -- deriving instance (SetupValueHas Eq ext) => Eq (SetupValue ext) -- deriving instance (SetupValueHas Ord ext) => Ord (SetupValue ext) --------------------------------------------------------------------------------- --- ** Ghost state - --- | This extension field controls whether ghost state is enabled for a --- particular language backend. At the moment, ghost state is only enabled for --- the LLVM backend, but we want to expand this to cover other language backends --- in the future. See . -type family XGhostState ext - -------------------------------------------------------------------------------- -- ** Pre- and post-conditions diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs index 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 258249647c..680686ac8c 100644 --- a/src/SAWScript/Crucible/JVM/Override.hs +++ b/src/SAWScript/Crucible/JVM/Override.hs @@ -92,8 +92,6 @@ import Data.Parameterized.Some (Some(Some)) -- saw-core import Verifier.SAW.SharedTerm -import Verifier.SAW.Prelude (scEq) -import Verifier.SAW.TypedAST import Verifier.SAW.TypedTerm import Verifier.SAW.Simulator.What4.ReturnTrip (toSC) @@ -326,13 +324,13 @@ methodSpecHandler_prestate opts sc cc args cs = -- which involves writing values into memory, computing the return value, -- and computing postcondition predicates. methodSpecHandler_poststate :: - forall ret w. + forall ret. Options {- ^ output/verbosity options -} -> SharedContext {- ^ context for constructing SAW terms -} -> JVMCrucibleContext {- ^ context for interacting with Crucible -} -> Crucible.TypeRepr ret {- ^ type representation of function return value -} -> CrucibleMethodSpecIR {- ^ specification for current function override -} -> - OverrideMatcher CJ.JVM w (Crucible.RegValue Sym ret) + OverrideMatcher CJ.JVM RW (Crucible.RegValue Sym ret) methodSpecHandler_poststate opts sc cc retTy cs = do executeCond opts sc cc cs (cs ^. MS.csPostState) computeReturnValue opts cc sc cs retTy (cs ^. MS.csRetValue) @@ -350,10 +348,22 @@ learnCond opts sc cc cs prepost ss = do let loc = cs ^. MS.csLoc matchPointsTos opts sc cc cs prepost (ss ^. MS.csPointsTos) traverse_ (learnSetupCondition opts sc cc cs prepost) (ss ^. MS.csConditions) + assertTermEqualities sc cc enforceDisjointness cc loc ss enforceCompleteSubstitution loc ss +assertTermEqualities :: + SharedContext -> + JVMCrucibleContext -> + OverrideMatcher CJ.JVM md () +assertTermEqualities sc cc = do + let assertTermEquality (t, md, e) = do + p <- instantiateExtResolveSAWPred sc cc t + addAssert p md e + traverse_ assertTermEquality =<< OM (use termEqs) + + -- execute a pre/post condition executeCond :: Options -> @@ -361,7 +371,7 @@ executeCond :: JVMCrucibleContext -> CrucibleMethodSpecIR -> StateSpec -> - OverrideMatcher CJ.JVM w () + OverrideMatcher CJ.JVM RW () executeCond opts sc cc cs ss = do refreshTerms sc ss traverse_ (executeAllocation opts cc) (Map.assocs (ss ^. MS.csAllocs)) @@ -508,26 +518,6 @@ assignVar cc md var ref = ------------------------------------------------------------------------ - -assignTerm :: - SharedContext {- ^ context for constructing SAW terms -} -> - JVMCrucibleContext {- ^ context for interacting with Crucible -} -> - MS.ConditionMetadata -> - PrePost -> - VarIndex {- ^ external constant index -} -> - Term {- ^ value -} -> - OverrideMatcher CJ.JVM w () - -assignTerm sc cc md prepost var val = - do mb <- OM (use (termSub . at var)) - case mb of - Nothing -> OM (termSub . at var ?= val) - Just old -> - matchTerm sc cc md prepost val old - - ------------------------------------------------------------------------- - -- | Match the value of a function argument with a symbolic 'SetupValue'. matchArg :: Options {- ^ saw script print out opts -} -> @@ -547,7 +537,7 @@ matchArg opts sc cc cs prepost md actual expectedTy expected@(MS.SetupTerm expec = do sym <- Ov.getSymInterface failMsg <- mkStructuralMismatch opts cc sc cs actual expected expectedTy realTerm <- valueToSC sym md failMsg tval actual - matchTerm sc cc md prepost realTerm (ttTerm expectedTT) + matchTerm sc md prepost realTerm (ttTerm expectedTT) matchArg opts sc cc cs prepost md actual@(RVal ref) expectedTy setupval = case setupval of @@ -606,32 +596,6 @@ valueToSC _sym md failMsg _tval _val = ------------------------------------------------------------------------ --- | NOTE: The two 'Term' arguments must have the same type. -matchTerm :: - SharedContext {- ^ context for constructing SAW terms -} -> - JVMCrucibleContext {- ^ context for interacting with Crucible -} -> - MS.ConditionMetadata -> - PrePost -> - Term {- ^ exported concrete term -} -> - Term {- ^ expected specification term -} -> - OverrideMatcher CJ.JVM w () - -matchTerm _ _ _ _ real expect | real == expect = return () -matchTerm sc cc md prepost real expect = - do free <- OM (use osFree) - let loc = MS.conditionLoc md - case unwrapTermF expect of - FTermF (ExtCns ec) - | Set.member (ecVarIndex ec) free -> - do assignTerm sc cc md prepost (ecVarIndex ec) real - - _ -> - do t <- liftIO $ scEq sc real expect - p <- liftIO $ resolveBoolTerm (cc ^. jccSym) t - addAssert p md (Crucible.SimError loc (Crucible.AssertFailureSimError ("literal equality " ++ MS.stateCond prepost) "")) - ------------------------------------------------------------------------- - -- | Use the current state to learn about variable assignments based on -- preconditions for a procedure specification. learnSetupCondition :: @@ -642,9 +606,11 @@ learnSetupCondition :: PrePost -> SetupCondition -> OverrideMatcher CJ.JVM w () -learnSetupCondition opts sc cc spec prepost (MS.SetupCond_Equal md val1 val2) = learnEqual opts sc cc spec md prepost val1 val2 -learnSetupCondition _opts sc cc _ prepost (MS.SetupCond_Pred md tm) = learnPred sc cc md prepost (ttTerm tm) -learnSetupCondition _opts _ _ _ _ (MS.SetupCond_Ghost empty _ _ _) = absurd empty +learnSetupCondition opts sc cc spec prepost cond = + case cond of + MS.SetupCond_Equal md val1 val2 -> learnEqual opts sc cc spec md prepost val1 val2 + MS.SetupCond_Pred md tm -> learnPred sc cc md prepost (ttTerm tm) + MS.SetupCond_Ghost md var val -> learnGhost sc md prepost var val ------------------------------------------------------------------------ @@ -717,7 +683,7 @@ learnPointsTo opts sc cc spec prepost pt = ety_tm <- liftIO $ Cryptol.importType sc Cryptol.emptyEnv ety ts <- traverse load [0 .. fromInteger len - 1] realTerm <- liftIO $ scVector sc ety_tm ts - matchTerm sc cc md prepost realTerm (ttTerm tt) + matchTerm sc md prepost realTerm (ttTerm tt) -- If the right-hand-side is 'Nothing', this is indicates a "modifies" declaration, -- which should probably not appear in the pre-state section, and has no effect. @@ -761,6 +727,15 @@ learnPred sc cc md prepost t = let loc = MS.conditionLoc md addAssert p md (Crucible.SimError loc (Crucible.AssertFailureSimError (MS.stateCond prepost) "")) +instantiateExtResolveSAWPred :: + SharedContext -> + JVMCrucibleContext -> + Term -> + OverrideMatcher CJ.JVM md (W4.Pred Sym) +instantiateExtResolveSAWPred sc cc cond = do + sub <- OM (use termSub) + liftIO $ resolveSAWPred cc =<< scInstantiateExt sc sub cond + ------------------------------------------------------------------------ -- TODO: replace (W4.ProgramLoc, J.Type) by some allocation datatype @@ -800,10 +775,13 @@ executeSetupCondition :: JVMCrucibleContext -> CrucibleMethodSpecIR -> SetupCondition -> - OverrideMatcher CJ.JVM w () -executeSetupCondition opts sc cc spec (MS.SetupCond_Equal md val1 val2) = executeEqual opts sc cc spec md val1 val2 -executeSetupCondition _opts sc cc _ (MS.SetupCond_Pred md tm) = executePred sc cc md tm -executeSetupCondition _ _ _ _ (MS.SetupCond_Ghost empty _ _ _) = absurd empty + OverrideMatcher CJ.JVM RW () +executeSetupCondition opts sc cc spec = + \case + MS.SetupCond_Equal md val1 val2 -> + executeEqual opts sc cc spec md val1 val2 + MS.SetupCond_Pred md tm -> executePred sc cc md tm + MS.SetupCond_Ghost md var val -> executeGhost sc md var val ------------------------------------------------------------------------ diff --git a/src/SAWScript/Crucible/JVM/Setup/Value.hs b/src/SAWScript/Crucible/JVM/Setup/Value.hs index 8286704750..a69e29ec05 100644 --- a/src/SAWScript/Crucible/JVM/Setup/Value.hs +++ b/src/SAWScript/Crucible/JVM/Setup/Value.hs @@ -87,8 +87,6 @@ type instance MS.XSetupCast CJ.JVM = Void type instance MS.XSetupUnion CJ.JVM = Void type instance MS.XSetupGlobalInitializer CJ.JVM = Void -type instance MS.XGhostState CJ.JVM = Void - type JIdent = String -- FIXME(huffman): what to put here? type instance MS.TypeName CJ.JVM = JIdent diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index 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 619e9f8f52..1803a59f3a 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) @@ -1072,29 +1069,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 -> @@ -1175,7 +1149,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) @@ -1345,50 +1319,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 @@ -1404,36 +1334,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) - ] ------------------------------------------------------------------------ @@ -1552,7 +1456,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 @@ -1978,27 +1882,7 @@ executeSetupCondition opts sc cc spec = MS.SetupCond_Equal md val1 val2 -> executeEqual opts sc cc spec md val1 val2 MS.SetupCond_Pred md tm -> executePred sc cc md tm - MS.SetupCond_Ghost () md var val -> executeGhost sc md var val - ------------------------------------------------------------------------- - --- TODO(lb): make this language independent! -executeGhost :: - SharedContext -> - MS.ConditionMetadata -> - MS.GhostGlobal -> - TypedTerm -> - OverrideMatcher (LLVM arch) RW () -executeGhost sc _md var (TypedTerm (TypedTermSchema sch) tm) = - do s <- OM (use termSub) - tm' <- liftIO (scInstantiateExt sc s tm) - writeGlobal var (sch,tm') -executeGhost _sc _md _var (TypedTerm tp _) = - fail $ unlines - [ "executeGhost: improper value type" - , "expected Cryptol schema type, but got" - , show (MS.ppTypedTermType tp) - ] + MS.SetupCond_Ghost md var val -> executeGhost sc md var val ------------------------------------------------------------------------ diff --git a/src/SAWScript/Crucible/LLVM/Setup/Value.hs b/src/SAWScript/Crucible/LLVM/Setup/Value.hs index ac5baba510..9f301187f7 100644 --- a/src/SAWScript/Crucible/LLVM/Setup/Value.hs +++ b/src/SAWScript/Crucible/LLVM/Setup/Value.hs @@ -130,8 +130,6 @@ type instance Setup.XSetupUnion (LLVM _) = () type instance Setup.XSetupGlobal (LLVM _) = () type instance Setup.XSetupGlobalInitializer (LLVM _) = () -type instance Setup.XGhostState (LLVM _) = () - type instance Setup.TypeName (LLVM arch) = CL.Ident type instance Setup.ExtType (LLVM arch) = CL.MemType diff --git a/src/SAWScript/Crucible/MIR/Builtins.hs b/src/SAWScript/Crucible/MIR/Builtins.hs index 0c7a75a175..9d1593cc62 100644 --- a/src/SAWScript/Crucible/MIR/Builtins.hs +++ b/src/SAWScript/Crucible/MIR/Builtins.hs @@ -17,6 +17,7 @@ module SAWScript.Crucible.MIR.Builtins , mir_find_adt , mir_fresh_expanded_value , mir_fresh_var + , mir_ghost_value , mir_load_module , mir_points_to , mir_postcond @@ -80,7 +81,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) @@ -115,6 +115,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 @@ -345,6 +346,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 @@ -707,32 +715,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 -> @@ -912,7 +931,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 @@ -933,7 +953,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 608e27d4c8..2d38c4783a 100644 --- a/src/SAWScript/Crucible/MIR/Override.hs +++ b/src/SAWScript/Crucible/MIR/Override.hs @@ -69,10 +69,8 @@ import qualified What4.Interface as W4 import qualified What4.LabeledPred as W4 import qualified What4.ProgramLoc as W4 -import Verifier.SAW.Prelude (scEq) import Verifier.SAW.SharedTerm import Verifier.SAW.Simulator.What4.ReturnTrip (saw_ctx, toSC) -import Verifier.SAW.TypedAST import Verifier.SAW.TypedTerm import SAWScript.Crucible.Common @@ -120,22 +118,6 @@ assignVar cc md var sref@(Some ref) = do p <- liftIO (equalRefsPred cc ref ref') addAssert p md (Crucible.SimError loc (Crucible.AssertFailureSimError "equality of aliased references" "")) -assignTerm :: - SharedContext {- ^ context for constructing SAW terms -} -> - MIRCrucibleContext {- ^ context for interacting with Crucible -} -> - MS.ConditionMetadata -> - MS.PrePost -> - VarIndex {- ^ external constant index -} -> - Term {- ^ value -} -> - OverrideMatcher MIR w () - -assignTerm sc cc md prepost var val = - do mb <- OM (use (termSub . at var)) - case mb of - Nothing -> OM (termSub . at var ?= val) - Just old -> - matchTerm sc cc md prepost val old - -- | When a specification is used as a composition override, this function -- checks that the postconditions of the specification fully specify (via -- @mir_points_to@ statements) the values of all local mutable allocations @@ -600,7 +582,7 @@ executeCond :: MIRCrucibleContext -> CrucibleMethodSpecIR -> StateSpec -> - OverrideMatcher MIR w () + OverrideMatcher MIR RW () executeCond opts sc cc cs ss = do refreshTerms sc ss F.traverse_ (executeAllocation opts cc) (Map.assocs (ss ^. MS.csAllocs)) @@ -650,10 +632,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 -} -> @@ -1011,9 +996,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 :: @@ -1034,7 +1021,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 @@ -1257,33 +1244,6 @@ matchPointsTos opts sc cc spec prepost = go False [] setupSlice (MirSetupSliceRange arr _start _end) = setupVars arr -matchTerm :: - SharedContext {- ^ context for constructing SAW terms -} -> - MIRCrucibleContext {- ^ context for interacting with Crucible -} -> - MS.ConditionMetadata -> - MS.PrePost -> - Term {- ^ exported concrete term -} -> - Term {- ^ expected specification term -} -> - OverrideMatcher MIR md () - -matchTerm _ _ _ _ real expect | real == expect = return () -matchTerm sc cc md prepost real expect = - do let loc = MS.conditionLoc md - free <- OM (use osFree) - case unwrapTermF expect of - FTermF (ExtCns ec) - | Set.member (ecVarIndex ec) free -> - do assignTerm sc cc md prepost (ecVarIndex ec) real - - _ -> - do t <- liftIO $ scEq sc real expect - let msg = unlines $ - [ "Literal equality " ++ MS.stateCond prepost --- , "Expected term: " ++ prettyTerm expect --- , "Actual term: " ++ prettyTerm real - ] - addTermEq t md $ Crucible.SimError loc $ Crucible.AssertFailureSimError msg "" - -- | This function is responsible for implementing the \"override\" behavior -- of method specifications. The main work done in this function to manage -- the process of selecting between several possible different override @@ -1388,13 +1348,13 @@ methodSpecHandler opts sc cc mdMap css h = -- which involves writing values into memory, computing the return value, -- and computing postcondition predicates. methodSpecHandler_poststate :: - forall ret w. + forall ret. Options {- ^ output/verbosity options -} -> SharedContext {- ^ context for constructing SAW terms -} -> MIRCrucibleContext {- ^ context for interacting with Crucible -} -> Crucible.TypeRepr ret {- ^ type representation of function return value -} -> CrucibleMethodSpecIR {- ^ specification for current function override -} -> - OverrideMatcher MIR w (Crucible.RegValue Sym ret) + OverrideMatcher MIR RW (Crucible.RegValue Sym ret) methodSpecHandler_poststate opts sc cc retTy cs = do executeCond opts sc cc cs (cs ^. MS.csPostState) computeReturnValue opts cc sc cs retTy (cs ^. MS.csRetValue) diff --git a/src/SAWScript/Crucible/MIR/Setup/Value.hs b/src/SAWScript/Crucible/MIR/Setup/Value.hs index f764de1f17..bbdfbd85a9 100644 --- a/src/SAWScript/Crucible/MIR/Setup/Value.hs +++ b/src/SAWScript/Crucible/MIR/Setup/Value.hs @@ -81,8 +81,6 @@ type instance MS.XSetupCast MIR = Void type instance MS.XSetupUnion MIR = Void type instance MS.XSetupGlobalInitializer MIR = () -type instance MS.XGhostState MIR = Void - type instance MS.TypeName MIR = Text type instance MS.ExtType MIR = M.Ty diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index eb566842b2..c48d5ade18 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -3633,6 +3633,20 @@ primitives = Map.fromList Current [ "Legacy alternative name for `llvm_ghost_value`."] + , prim "jvm_ghost_value" + "Ghost -> Term -> JVMSetup ()" + (pureVal jvm_ghost_value) + Current + [ "Specifies the value of a ghost variable. This can be used" + , "in the pre- and post- conditions of a setup block."] + + , prim "mir_ghost_value" + "Ghost -> Term -> MIRSetup ()" + (pureVal mir_ghost_value) + Current + [ "Specifies the value of a ghost variable. This can be used" + , "in the pre- and post- conditions of a setup block."] + , prim "llvm_spec_solvers" "LLVMSpec -> [String]" (\_ _ -> toValue llvm_spec_solvers) Current