From 67b42929219585bd5e9a69c91bcdb4010dbb8df6 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 13 Oct 2023 11:38:29 -0400 Subject: [PATCH] Draft: Support ghost values in all language backends Still TODO: * Once the MIR backend supports overrides, the MIR backend needs to call the `executeGhost` function from `executeCond`, similarly to how the LLVM and JVM backends do currently. * Add a MIR test case demonstrating that it works. 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 557027 -> 556972 bytes saw-remote-api/CHANGELOG.md | 2 + saw-remote-api/python/CHANGELOG.md | 2 + .../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 | 111 ++++++++++++++- src/SAWScript/Crucible/Common/Setup/Value.hs | 11 -- src/SAWScript/Crucible/JVM/Builtins.hs | 44 ++++-- src/SAWScript/Crucible/JVM/Override.hs | 97 ++++++------- 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 | 127 +----------------- src/SAWScript/Crucible/LLVM/Setup/Value.hs | 2 - src/SAWScript/Crucible/MIR/Builtins.hs | 44 ++++-- src/SAWScript/Crucible/MIR/Override.hs | 55 +------- src/SAWScript/Crucible/MIR/Setup/Value.hs | 2 - src/SAWScript/Interpreter.hs | 16 ++- 26 files changed, 342 insertions(+), 343 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index dbf13e439f..e7c72acbfc 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -17,6 +17,13 @@ generating LLVM setup scripts for Cryptol FFI functions with the `llvm_ffi_setup` command. For more information, see the [manual](https://github.com/GaloisInc/saw-script/blob/master/doc/manual/manual.md#verifying-cryptol-ffi-functions). +* Ghost state is now supported with the JVM and MIR languaage backends: + * The `llvm_declare_ghost_state` command is now deprecated in favor of the + new `declare_ghost_state` command, as nothing about this command is + LLVM-specific. + * Add `jvm_ghost_value` and `mir_ghost_value` commands in addition to the + existing `llvm_ghost_value` command. + # Version 1.0 -- 2023-06-26 ## New Features diff --git a/crucible-mir-comp/src/Mir/Compositional/Builder.hs b/crucible-mir-comp/src/Mir/Compositional/Builder.hs index c8effab421..b87d665b82 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Builder.hs +++ b/crucible-mir-comp/src/Mir/Compositional/Builder.hs @@ -649,8 +649,8 @@ substMethodSpec sc sm ms = do MS.SetupCond_Equal loc <$> goSetupValue sv1 <*> goSetupValue sv2 goSetupCondition (MS.SetupCond_Pred loc tt) = MS.SetupCond_Pred loc <$> goTypedTerm tt - goSetupCondition (MS.SetupCond_Ghost b loc gg tt) = - MS.SetupCond_Ghost b loc gg <$> goTypedTerm tt + goSetupCondition (MS.SetupCond_Ghost loc gg tt) = + MS.SetupCond_Ghost loc gg <$> goTypedTerm tt goTypedTerm tt = do term' <- goTerm $ SAW.ttTerm tt diff --git a/crucible-mir-comp/src/Mir/Compositional/Override.hs b/crucible-mir-comp/src/Mir/Compositional/Override.hs index 73e8623d2e..45c1abec2e 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Override.hs +++ b/crucible-mir-comp/src/Mir/Compositional/Override.hs @@ -571,7 +571,7 @@ condTerm sc (MS.SetupCond_Pred md tt) = do sub <- use MS.termSub t' <- liftIO $ SAW.scInstantiateExt sc sub $ SAW.ttTerm tt return (md, t') -condTerm _ (MS.SetupCond_Ghost _ _ _ _) = do +condTerm _ (MS.SetupCond_Ghost _ _ _) = do error $ "learnCond: SetupCond_Ghost is not supported" diff --git a/doc/manual/manual.md b/doc/manual/manual.md index 2c1d2e4689..bb5973bdd7 100644 --- a/doc/manual/manual.md +++ b/doc/manual/manual.md @@ -3144,14 +3144,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 65fcc6cb8bc45ba00a3e1e69c615a124f825a7ce..c1aa536cab0a491f5f25b48051d079b8264e1bad 100644 GIT binary patch delta 12155 zcmc(kWmH{Fv!HQzcXxLV?u6jMgS)#PbmI^#1Um$G2_D=nSg_#k7F-f6*pU0K@80?D z+*$K;*0XBw>aMmQ)w`;D@4Qe~zEB5;LpQ*HVxR>eZpSdpz@Gm5k1O&xLAfUR|U?Hkjs{Fax(WxI} zs;7v%%3(#atLI67>$kjn-Bsgv_6NtL@%QuE${xz|Xi3X{PE8?57-++jhU3iVNOR%n z5{hNRr2yCq7HOU7Q!(ntBnQIn3O={3xm)4jK6x|W( zl8*4_NNdD>0QdZ>d9)#@)_a9X}SA{%`hveegCD1FB)o%Pm8Ns^)<<@EI6v( z>sj^T0dOBYf*sY~^)QU)!XX|j?C0YVecsMc(}CBu&_vT-xzN6Q(!EbX%i?bQ5sTp<0GAK7ow{PFG5zsKGFsRY{IC-tbp{q`P&UU7NfaJUB2@{+6a zS1Q_5efcRV#^%8`NAsayxwI!p-)#+}z1qm+Mn;gJUj}1@&a4twFer#Y&Y4x`l5H{_ z-RfOuLQ0O_nQG&}ub#DQHC1dhdnV~ZbT<~Ad4<_B(H5wbo)bJvto?B`yBz8ef#Dz~ zks2WT!BAt#KTxr>hQVqHk@_V@+g;^qWjhQ-{KrU0dMwlD*n4cL!6H7)LxP0InCoQx zjMRrg=4yVNjNyb2L@Jia)1=@#NzK68$Ej%v^@eQI;**faQ#?%EJl!@5Z-2E#?@k(- zlCl)7u3mcjLnmvcigoE@b@I~{eYQ=BbR-p1LRal?%)~LWrle@+<+6qO;rt|T1X9+& za%ZWYOpA=nJG5T?Nm+kuOdD0diQ1%f{=q^aK4me|zUI|qJM5J}o zH#x#Z6krdm>S8}BuSkQx-s-IKXgIM3hu9$i`L!$q2+jHDAn?CUmRB>a{6+PCYdJzk zDjN9KnbN?cav7*7jOulQPdeQ{{2prYvgQ@81Q#5e$VQdQ{^{%``&%wmR4y;C{I9n+pr9Ue(DDpKuI(@PUg&Qa!=; zq+lZ{BkR1e4$6_>)DJ;KbQr#(5=f>~O_E2t(n^wVxw*Fdu(U@+D!ddmCc}Pcd0tGJ zLw7idp+*JzkP@3Bm#$FvLmr6KFNuw1SH5oeya~E1D4}#8e9}I{;&I&hp6`)hzl$v# z8C*P!8NBS(W-k((p@z=V^2s8~+%?c4npU}n@lT7r;u-+S+f3SyNAL!+n`)u?;=6Rg3X8{O(<8wVoy zs6k<31@+ZVx=ODFW>lF+7oFEY;-A|j|cHN1g(%llQ zGn(OOS`q~zNL&w0iU^BH%|9DmtaVbsYHL}J4Jn1mEUYo>yMgl`bN2=P$){PLa9!a( z4)!^NFFOcuVfpFv(*mb@U{we&%CRr`(~S#}<|DA&ZmC3G{HE&$F%%1pMF5VDCF-~& zx*^L{ejEC&%mF=5f!xyA+qc)w-_u&4Tu;}{p}=zLdGriEjK3J&a2V?DWS?biE{lZT zfaLr@a%8S3DG;q2W3@pZ+En;!O4X^94E4;DLb|FVMH%XZuiSz;V?N1a9<4`m|l~fx_Hyfa`T^N5P+-i7@EXJ9^W15X6 z>&vciyXMLh$0kkZ*&$X}LMPzCn#q9UxvG92RGiq)>xN!BWfrg^Dw(OR6cNV7l;i*) z-S)$)Q||TT4`}o}n75Ak6T3ZuUq|_=?Zno`!B~gF8<*s0Cg!%Bp2TFJ(FfRB-g<+0 zjCE+dK=%M{#s-%iKL~+ z5lYxcCyI=>!P7EJ{Ju_^HVfQ;ew+d~B$w_4EvUubvZ7jgJ(?GDvu(Q*9MARA)PdYR zyiiq`UbZVah8_8k(qqYw=QHQ$wl8x#n!HBLU)`~XfkZ~ zqU@{9c?6{Yk7>0mNyLZ7AAmE&ECmJ+Is)RI0z)N0t?RMSJvM0NW}A4h4w`2CT2VGr zCXgm6P$fA@{fEwd#mz&dBe$&htaVMT%UE|9d0H1N{u45m0wahN51?bz@^36dP*Y)e zfeKJXVP2X_TK_V=(^(ST@iY%dnrB2Ta3J$W)-3Q^Dx`sFV+=5P*e5zOKUd{mms(-TKaV82X0#!Xa$`eUaY3sW8z#UB$B*B6Tq(c9`m zlfjPTaf}&K1ur(O=vjM)S49vd#aH?d5W0dIi=u zhWhqzbb~|fUq*Q~_!u$Gy%L~#r7SEo0=xJi0kvzH1-%HNE`-5@bfv-I!*cP1lBFJ)fKw7Xm))l8b|B&h zXKF0@`xJ$DikPMzCp1!_e07;{3MevZAPR3UW%_ZD>dMQyk2=ZQoJOCARxZg)a6kaz zMz7n?HUIqE8)->WzrLAIr55Ct`4=&NwsQ$XqBVMB>p9rt4OYL+K^iZ_T{yeKy4~zx ze+uvhPU-PcX6-K*c+PB2Bn$PZ1LSCqCe zA)jt2ISOYd>kiRmI-ReM>YByEo}-o6tGe6US9=!t1`?b$0(=#3@6-oK%NC2e8@smd*?>uldJz& z1uRxI%^uK~+YFjq8#lT0w`lVd`ZW&OFv;AiJ;3I9!dAWDppZlyE1f16}1U2ZFknD>RLBX5UFv4&yKbQr`_KT2zNLGLw(R+H=XC zh%#&~WF70G2UjRa8p>Wk#^$3y4fr{ltE9d=ypGMC(O;DBe1mfY2b(VN9B23?8I|8 zLVqJqZwb*>p?nmcY_2a8wR6p#a^Z{?x$j_`asW7<*roXza!SjK4GI;XhW#yg(vPC4 z;lX|6e$t;J#LMZ%hs#VCF|$V;&I(yhbDSt5i_Ksw^oxjv>Cfq|d;IVsWBh#_Ic8r( zT`J34UbK5e#QBY8FbB8yAZFVe0 z;N!h1)Yjyrdo#hOePqW)T*oucq+qqrOb=6RsPM_ALBNJS(v^~NDT%TJ;1PS9h`hYi zCODVI+^3!_5_3yFa93zmgOt~4cE0>+K@v#pH?oT5J(C<@iGGvpa-4;cY>ETUw?Cj{ zxKubmu-fH-QO2_rs{uEyVKy~&=kqA#m<uc&+X z>2Rss(za@H@2_lvfCCx6yJ&O@9de~~piPe@fM@q2MWJWAi9VJI1Ea-h@D#uZ&SG7B zb2#5T<9ALazB8$hma_GG=M!%=bkpFs%eeVuy6ECxL2`39>DyA0NSE_pGgKyVl}-G< zQfCByLBWduj)NC}ftd;`l8M+W%8eMzWIId!{m-q~q*y1s^E!44t?F<&b@(Dncg4h2 z>9(Ye{cn!RJr+AO{v_iwy;2rHcTeI>oX+SoHnm1sZ-e1>;6Tv25U1C7O*T}VYPM(? zIE^Hmarp&UiukHhG6%wIK8R))DkG~6^H3!&6#;UNc)mV8SQ8;4!hlT*$KjTpUdwXY z>QKd)^g#O;Om(2|m#7u^w#AKu{$OE=QY^`GD;|P8HP2wxvX@(aVYD0o`T0Uh_}$yY z59QTjkOirjIQkUhVxP?ui#jy%r&#*9@FMC7tvp=DEXpZebp@?@a~K5P8f03Gwvlqt zh#-u2Y3{K16l*wX&*UUZ3_W_oSf*FK)9`S3jAH$sBjPxI-m9k+Op7ypa4Gq>B|~}z zv~)&s{+Fv56+zOLt{@uVcxCxI?`oZ5Lhdt>^Lsq&dRbSZSOMlzyyt_RaOnRmyO&K~5x0ztZh1ak{rMnWrTCTp!ZgkAWszcEnd%echy@1{i*EoQGoesjG{{*47)_9xDc z_Po4(M!-}`%jbX?O*PhL@JL_>lV~~bXz=cRBD7@jVg5zC$eaRH=C9g4rclqW(%CR! z-T~p{oV!KKkn1<90MEK9Kyz8HxfmV-V?jkXksB<&&5bFx#!%qirgD&DHStGrI0u(0 zGFvkYuASZ4$s%e%WNpFZ z!efLhCVF*ySNBP0gi3LPlJoTS2+NqrdHVCfNP@<{j-c$k^H`H0&amyQ$--N}}? zwO7~aVZJOjYb&SSxPL2GJH!mX`Thz9N~=Gx_yBzumTvH^<;45Yewkhai;JeP@%&){ z=ZH@r=*o3%{+3dv@laPZtx}usHbtpYT=BDhJ42njP}a2wt*>z(q-Q2BjCobLZXU3! z3ek%k`dBOngvuS^r)@5Iq=ugQweDDsHfN7ePv}r8A$2XW4wDnuD(N&I>b@(C3O}B^ zYcWWFx{DL7z+!Bd@)2t$CFG*Qb<{tYu&Fsvm-HkEwdWlyu(A3ijb6j!3cY!1t}C}R zs)Aqz*XVC=U@v07C0k|j;sYUtmbxa{r|Cfap)-2}%*0*L9z`K3)?~wsL_QI3Pyeo@ zw~TD@{Q2@pnQXNh3;P)cW@}jNt!~4BI_gkqKHX!Cs&bjOtVQTzKA;q+^c1PD#H-+6 z@>9l5vVzDFD5O?;=1rjKNX)n!CQ_2re`YI@s^f|JTA`+uyRy%D_;w($wgors#h zD9WDz%38Jz!&+8Yz3WBlD22QNi-}{lsy`^K z5$0<{P6-uy$hKXJ!(Yb65HP1W_0V6J0Rm(U-E!Gvm^bq_C)oiucK#VCiGH|GpPsgR zE{3+)50Ekk-rG99zX=+RJxC+$wDd)OpF=Y`V?Kx(l<-*oA$T$#G#pgJXdDt-=NfyR3PiixBUzpfQ6~Bj#SZwDenNER6sKoCfzny$}#R;(a zvqp2;K_UFzYo2+3M$0o5TtLDl64*E)Bk>!u1B&cQi?#F&ecHCZF@aLAFB(>f>HhWd zc>9CZjO3IfvK$fSi`b_lNlTJHsXl?1p8V#Jb8LeFoY9pDv9 zg|rA{Q|7Rg@#OD#6XKqledm_fpI|PnG}%(?MVFI5MgDmoulF4D)-1?{D0vp?eCMg# zTf@q=`SoaUix15MaWjQw20HcLsgVg{1$CQj4ejO|e-xuw!H@s1sr)QvSYvAC=C>58f zlfTh`)|-+T*yJfkILazSncCB_#!A9HBk|U_zD_rKYeZY^8CKUq0<@R3u^fpBEJ#Nr zVrl58&@AXLFeTzDGtTMikUtleO_iXPdy>P%&U#&77ayBa!T)42Wv+-ZrE6Su5>9f~ zTrg6MK#lw~c$5|vTU&|KO7zg4Wn?+09g+y$4?`>HrB2QzC8fUiWw%E)MU_lYfyOn_ ztjY6;XDqGKF|LR znkhWOKF(V>5A0#JRZE-CA>V{_$-_Z};B%xxG3d%Tq^8?sq^agOtk$Hp=|i;IFw!Dk zMXs&7)zB08C>dUq2`7=LpM82V7I|=1OZ~WM+`e^s4zwtCZ4Kymp6w0{EG2UQVhNr{DqJtL&V6(QK;7dHz&Kmzb9e(y<5LB8dAree-Lh)eYhYf5ax zqd)WV*KYMZSI51(xcwsKAaPoK`rtsr{OQ`-WaPq*pKo2p$K&y|^EQ*g+tML5NbXv` zFm_CJ0~qej5Nk(#*Gzw#JCwM;ZU+M%y@~rJK6BT|zR@QAFM9cp!gXfM;8O#J+JWaWgc)@^$r3GYFP+ zVet)n-?{{7oruX8o2CgeI2+eZaLI-V1+GS^eWm>QLo{jCMp}e4$|>50#ggbN5Xsz_uI)KJAz)TW8=ayHLuyMM!fvbkB#hZ*dbMA^p!6Xqb6-3NrnEn5~wSQ;87` zQ~cQ@U1k|dctvR;A}wIS-u;VThubw~J~pNPMBWE8hwj{DXx*Lb3mb1JOAiB{b^xvb zP`0>n$FE;|rCS4+OIMzq-RYReJKccZq;BcKj79i;;3tABziO36rrfLTDTG@A*Z5O9c83QpnJsk}$MQCy3y3eDnxoQ1=Zf@@G0vN}?+|DL9 za#uIMG$X4H!uGLKxig=jUOx4#7A&-ncS}a@3VELe%jEc34J`=Gj)_%n{44wQC zXUa9F$R8@?FLu1r!)zWng_Mvl2uljW%kuk%P!gF`WC^$Mb39V2ejUrv^aqet&m97n zA;ZNJ^$xJ1afT*rU|W^`(fd5K#@Iw>#Vw%gefj+HF}Y9x3+*^ z=S_S6g*0`$e}0_F2bZ(h_es$bcIW3{Qk*H-8VPZoviP1k+|ZGODJ{{CPQ?hqJgz%0 z59B(0YzgUAjg_y>Nz~*G1+K#l_nyCQ#`#VRD)UyR*^lwj`g0QtSzD@A&W#LH$k7h@ zb&m|xO8v3rC5dmbap%`zz$h~A{=C%F;!t95$$n(SOY%Op#bMCgC~uv=u#N}$))&XZ zO2dkCeqMT0NY4N@#O64MfncMuDngRizyMWFjLM)NYW%Wd{)$U?!qmV6M|V=;KA(}6 zW7CJx!l7hDp`lfFolZ|;C_{e7iAvr=Zfn-xb%AmpNlquu^!IJkDekgPZNijO?vJL> zsSg!G*4c&Bq`k|A2E3tOe9oB^D?P#_*ZmLtca+Me@E`tOMBzp?cf-62?5n`N3jC`e zG&gr6HWa{f^MbeqAg<;}6#uBr$>vBAs2Z|-a<{g(2ldpPWaP&JVO(_%;mUJR~cx=23KkgW6W;hp^ z<=mIR`>*q7XLA(`x3?zk_S!WI$4@5Rf}MKk4yI1s3z_Rmot-AfcJ%3pzs#W7!sTj- zfV3VBJ%mv+_{wnYT9SE5v~G;~euPD&OjBORkg8hrrhbe?UAg-DqK+uCj#A)=UsYj<}=KQ*p!4${3M_CW?*o^li zIMWsNtREH(qqem~w8W-|iZG0pIPjG+r0@cpEbQYJC@VPG6-Bk57=(JTDQXxT>x#_L zkKcl_uqnLyx36cVZBcT>;eoRJJEcP z(r{VXz@GaZz2U^~-NzAqMgc;Fn2KHoISj0@yJEBXJ1njE{~ZHdg8RT=ip>_bR|_-W zqrZq$x-%q_O0pD}L2 z2H zog;0$Q_+(3#6x3I{Zgu*OE;m*`e_7qnbNCu)OI@%ag%D1IHNxg!sUiU0ugjW!a)Au zR9$4;#K%wsF>^zr2MVo8_-D#K%a8Nfm%QU0XO(!VWoHWLc-zVOXsj%A&G)6$_k50m z?q@%oa@ZkP@Y{4~UNZvaUdMD;4>O7}wayxV9>EBDNBMc)r=XoEt=Aod!K!)g^TKUx z1Yco>UK!z4OCiuBzX+GvTjJMW;%7nX7)4%->)q=djqb~NViWe{3Wd=}9c?8H^Ja?{ zgh1J^1p4F$fO)O`a8!HkK(IDjWLZ(DuGk#CRxL2PTO@{2q^`Kmy-qE#K3f#4QHU2< z6ulOI-HBKK~lEV0QD8!W1!Bgv$O)0bZ+K#~-!t zV18Ty25(XR)gJk;LZ;=eK7cQ&;G6FEa{X}m{y(SxM>)d9+C0LKmZXPCMbe^C?-X>$ z#QClH=L4neLgT>f@096tSsy4;Q8~CJ)~GuZnlu(TC}u&6hIHT z!j!)fdVx>#nNiJ2*=|m4pxKG$ylh@z5z|0(`3m#$$opa==sWPh{Bm0Q*qpnJ`miZL zrf~Rk>+YKr2rg<1>DvWmFZUf$LO(JHxpb2+3z`sD^Y2E5TEN!i;41moUTwKbZ$ri0 zQdK;VpsaVF;=U%MDE0&%93RK`-Vo@(Gs#1#M=n16?ma ztGxP|!r?JM;Ic)V`DyxKvfuV-l1}or1iVyKB0LGda)%%g zPb4b9f%&O7hA3ru4Bm1dh6lH0j2{^Ely@pg;$65RzI0+6*-3f+-Oe3+{4jPMNU(70 zp4bW1#`|v=6gGG^|BILw{G$1)H%jgm69y%(?5!sKAFv$g1nBRrRx2My0SD$JI$w>l zr#G^qIYz4boYyKFoOSd`6Zml^w`tF?U;aatyR(qXUa|HB z`@<`1|8V;D-3P*1D}Ui)7tZ+4I2$Y{X-|K7?R)YH&0Nx|vD%>tARtcKj7QhJli>`o z1JB+Ifs%UQ#Od2E0s!?vx%q$MJbobz?r9dd*_bjyJ3D?6Yx}Rr5Glk(xZfL~2Zh?p z{=JL7T;d>;dtC$drfyzXFZB=W3!||fx`=7ukqbZutU#SP-Z(|F*Wx$zdbc2nXubf$ zHWJo^Cy`>cgg3oGASlEwEV4*iS3L1h3#?xv7>t{ASuo8e5350^B8UfDFsmU-^+vv4$poA6q!~E5a-%-+Be95QJ`@KH=#5!D%Lk(z)Y|QTF!mgNhf)r z|39#b>kArr<JBRsi(4!vJaeRh31RWMhr6c2C~c> zpMR(Hn+Wwu3iyrtKiC|$(U!lYMqHBr?fLJ-bZVZEACMmyfe5S5aDJ>!{RacRXuxab z|HK;Z0iW6N`y=2Qk=t!sgzsk2 z&#>eIOw|~1w$OoExU@bVJq!#$yizNkQR8KXof|U4HUAXPDer?`3H)bJa?5IjZ|W0R z#1JuMJPBRf{BhVXzKHo6HOWHzUEvb?-ngQPNA9@7sP-}c%}2Pi-ahR=a9{rVAHvaV zQbH{nT6%%D-kUu80*Shmo7|%RCnpisMm0Fsd}$ZyXvN?%;xz(zjgk%jGO3Jv{KB(7 zq%*EFZYq|_;Fmjy`fcGKbPA1=81^UQn=cG%LgyqcRQ?CXP5*&>C{mTvf#mkb#eI4_r{cb+z{x#E9)5zMgJ zBI#@K(tuufJ!n=ld@x7Dh)2GPgBf{c6nZVTK(F;8jDZ>Hx4MhJ`ROL;Vv5SS#X#u5=K8Z2<0{Yw4gFhe~a+oR@{A!Kq2+67!&>QEpU)66vGGyS90ebl@|Es ztpwN;bvI6x)rb4Lf`)$SLAVJT=Tx$C5mYXaZZUf5o(v>*fBQkZs|weahK#?#`) zftu#r27O*eRy^oPK6=<7EQE0|EIOcaR42MrNyn*{e0%pWdtNmX8UGQoB(f8z;hsG2xwEv0n}9$2_kFVMN_m!);^rt3l4!6<0P0ta~gF z{fLEdDR@pgh{_!-6(!Cc?ZO*o7KfwByOzI&cq#JOWENocXp73t2a&2w)FvH#G#6sO z{P7L3?j`_jXDFQM3W&U9^|u=g5xg`_Kg-XRND0e#M6)mow`Nk1ao|s>%}+s-b74x5 z!6qMk+i-%h(^?*fxf8DSBPvupo+3$zit;ewDV}9}_iM2QL!kC%uOGBA}NuKuq6ZX7e0zN*}_& zNf|r;hwpxzL!Wed_v5o~2SR5qvBmNuH^Yl5nbz9*HR|K4#XIJ&UxoJY?xrqxgUVHQtKFJj+mDJ&avyOKunK^SDgoQ1H)o=q>(z70;7R1{vXwmRD7eqNd znqY*bE=j=_~6mK`~avHT3$oi03<48 O9)1*hdO0
Y@nJA0G> delta 12200 zcmbuE1yCN{(x7n-PH?y2?(XjH4#C}RaF^f?!7Y#%cXto&4k5S&hp>F#{r`LS-rcRO z+O22KRL^uzpP4$+r{{coBi(x=4GaZufZ&dXVCPI0d8P&qbafKehtLAHj99KPU@w21 zhS;gbLsCaTLnD~_a$SWm*ij>UrlCa;+$=8$j{r)98#z>-n!0>bao|2#lY*61Cl8fb zGd9i9noNvPDKoO)V)bz?`smTCOo6L@32JlNhZ3z4Er&?^htmVYZvktDen>+1Hjs1n z9ghM2?pMG{dZxC8N!p0HyL-K=Zn$%nLX4rk))q8yTxHq3NnH}W(=-r`%(#}_2p8VS z-utRsDiSZDM3+rNIZ2Ux*uUcY&!j%UpO9){Z6tc-oKq}AOW zNsl4;tSVkBwJu3ZXqg!l4L>K&<{oi7L_zg%-~%Kd8~39;`XmpEAX$i7d^j=d{QAVP zKv&6S=pWd783?F2g|eoJZ~Krp)ZQ3Zgz!~fR0Nz2iFOwINV$92#=>v*{-Q>XBo8ygjWo>%R7upB99-8EGUovSoxgI3#UTOJ()UD%a5aV6Vjx| zbN|d?+=3=lD<#k)G8Kbf8+Mxrkqz2A&m$b@!^;SgWcsu}IlR2cN3Uys+ttZq!5=Gp z5>)juZRK0QnuhdT65^9$E-!$K;~c2a)*)9Zy55FRhNxHjB9g(yR_q-PwMz0_a0+yI zoVzMmT-?&+c4ehl5Qn}XYK}6DI>w;TdMSN^HDxR`XZ(p694li@G|NEn2z~O2j-Bp4 zS54oRf<2KCgC%Q(s)XzEGOyIf@v*1`_-e)1E4u>uIL<>vCH&n@;Pfu9_UtMCLuR3> z>LXryN^x^0L$wcLwOHeFbE9?-z^sVY!?;};sm6*K)x(LisTL(E25-xb#hJ2M$C9IX zy2>}YXxn=Al(H$aNfuGRjnSlj5osnJm$DqL=ds9j`Pvps~f6CeTZIO zuxwb0C2)|WCaphPN{5SwAO@B`!SY9?__-wyzkw8pfEOw*6`T^wfE+ty)Q;YGes^hs z%bz6ra<{?9ADU_3d+SElLu*buyrP#q<6&dOAD7B|ek7YDs<^x!?L(2ezDC6AVAQur zUm9zRtlj4nH>~4jI?m#V#CkB$N_`z-&0a?Z&!2qPlLs`1FjikHM!>I8`0?(xu=qMx zi>YPq*O9~#Qj0S}P%a)#ZxplB6_@X zg3de3fIJ}v-5^+4+mUM$&SVP3BuThy^(4ubyEF5sl>;1n-j#?6F@_`aixT2IiX$at zB@*tal$aEW4C&fgNg!Oew5m!#{O$Vh;jZS(2N;qn2&;SwcD6@u7*KG3go(e5#%}3rmrKAM0_J|@z5+VWC)Dd`+ zE~|T-mOFW~sSECTK6&R<;cDoG>2_K`Eq%ShW_`$BOsMN$$%?Lgeql8LA-&y#>OfTlHCwq8T8!g`{Xmc$@cKm ze|&+!0VG_&EP1nuP|?cOd6kemuK6X;Utm%`dZ&gT^Tnc||E}NOpgY`Cb5VoyL^B^i zLn_XZlQae&gG|j`n)0uyIPJ_^|6E+>bVh~+C7S~3)m1zY;PPi}wXHr3IHv2PBQ!}* zJ7!pLh79gimbbOe_Mqo48^;Yh>xd6{#*U>40L~5SO5$h3zQ2Z(K!rpTf=7+*w9$|; ze9B1l5}y6x9TjV(!s)82+L>KP$q2UI){FzTiHd0zHM+6#B9jv;Lob*lG^4|BJq1xF zjZzkgp%`?XHMV&&s%=?Z_w`RdPnIf%O|t)&;y86{>H#u**TYdiu2KGG?opxk!f>0? zH{c{AFaletf*XIqFbR{O>=bXso?4H|yC+E%q?_2oOv;6q{mL;XkMZY@mEMR z5JKKtr_@r@AZ2-Mk6~>~v!HT@F2T*o0$pP@mj0ADTTL`=E+EXi1_htqa;xJgz_qcR zaf|6HPu`q5(Yxg{qB|Ard9r~6yv)gw!%&EH^JCD3@dLV;Z^8I>kIrWP*SyRP8@Eg3 zufOUK26KLN4W<<^j}kcfF-bJw{9Zn?lqs*XqijTItTTRDTbqTk>cK}KuVjEGYj@Sc z@w2=6ArFy4G*&ZeyT;!hKU3y#4>U)n*Y_AuHHffotBLn@Es7o!RCkFkzj;OZ-)`aEC=j6Mk5pvd6wZ_#U;*QRIX5tBZ z%g||sEWSO;BCm&ux&Hg36oXsm;yHGUqsZ=X=#|)P@X!=B3*;ZAFKP0O0|0bslqnB3 zw(D%g3lhmu2WYG{c3NWFn)js0yFB6dkNy7Tl?+rOQmf-LgqP+)8jY37SP?Cs;2j2w zk}0oJ+ia9a9yBx^7-Ydcq`oLll=yvf!yiIX#z6VF|0q{Ah^nDM^RVhCG0$}J{$+XH z=ZmoP{wMPqalEjo#vg#4Q@Uvi1O|9ex@#`%S+B%H=AZDg+x) z&s`;U#Y6X4Dv=bwGHIk#ESI=_jhFRf26&D z_L$}3!8;98G`%u6Vzw_D8g0?TgOe3-RVN?Ro>Cgwvr0rjpbm}rvxL14(4eUh&>ljL zd1?sB_krrycN|4bnHcV^c+H;dAWN23z6~cSjIU>+$mkFY*iMp>+!9Ws13e0@YoKVT+$K>LnKl5$t>fW|3_&3lV`mHT4>f~=7R@PY>MP8rP-=(?&>ox`Bx%GJ z;s=0}a?YFr8UYEXwZnm~&yVDmDcdw&;iug926mIevWzFX(6Gmv{Y*EPG+5AmH)Q^W zeQx?rH3UZbbQ%N}BnvZ7dO1lzcN6b7DC8l!y$ zY^CRm6ak8D9D5?WM^4k*rfUIvl4VD_AT|tjG%r8@J>u}rt^*olSKAlnaKu*TnZ5x@ z^8)>Ep4i=naJVH&Lh+@)E4FsA8M`+}2eEGl?=P1CUGTOAxUIt_?DX$!t-y$Qn)v9h zPkp2Yghb3CaEv%$*RyT>XULJ%>;IzLX!l&`zQ z`b+OceeV8w?EoRKN!Jng+Mv9@DqW7o;u7np%j5Vh7j^-5-@yqt!3>oIPTT;Q7}}7f zb0;K%5n#8C8sYz4(b+n&TvOn}Pp;br$RB=aVp zVPqJ*GTaEZ_<2ZamGR=GK@gm5-F+=i*vKnm^*c+fLHp#K-F?66ClNy;pHuvRP5Ux9 zfn0eC1dDwtnM!diIjqP-O!h;Dq@%bHzqu7l%dtDIc0mGrGj0GZYShOEy5H6e){yr; zFfFc4eovT0BmH}-As|h|T20=t<^=wATO+IUh>|ENV|#pySMOtSC`C}SUo#WK1+aKp zBAud7v7J*pm9b#U?wJCTME;gP@40A;zUjf!I)u@U<_cGT+w%+Cy|L-J<^Y-%F4*Y| zs-Kie1!DENW6NlP0QwhnY{_lj2qKT5C|ISY!5)#m;q_C+J@6oQa~B{R4%yZLTTJdR zC0lILC)$IdX53v%kfLhLxd6@!LEsBT8#jTAbHXJ?^Y?owTp0HlZ9`PbqW^bL}bhFyzCZcGxw3?&k+^ z`~)msnb4q5gg)YlVc-=MlOyHZjc0h-7hds|ZoW<4UJUg3+Bz3JZCD-2^N?Fb%=7&1 z7On-4*xmiD#^?6)_bqZ;ko920@<> z&VCbBnq*0v=_t7&Jr~K<$k&D192_uR3rf=aorD>Pi`k`$*f8>vQ}S%+6=Q+y&Jss`DI1$IPh>Ylv zuB!?d&)Y~$pe=8dH_|15XU+pt-2Ro4pa)XW-nyPOo5q}Ie+l?4iG@PyY`}$+>pk<> z*YlZ3`|1&lkZ{4ln7jfeNEysccoOkDf0Ej@`Hxu#uNVnhd260TCViLrcXd*&-~8zSgS; zitx)u$f=ePo68mFW0g#W|`j!_j47BM~WBP_|@6 z9M05CQZK$GR6gRZcX2n(-$EG>oZi#`V!8QhaOONk=-feLRTzZEs5Wo@Vc;QJ1Nnlo zpLo%5Hz-k8UBd|HM=GQnG8a5iPtAA~1kYf7aiBFq5Xh~z{MEf)R;l&jj$~sCu=Z5QDl1m4?om!)FWX#I`2eUkPCWDP8SA z&EHc^8FKQW#p3}?d27o3(UJ6BcO$Dlho66VIwBv|eVEVsF>|6qxqNGotty7JqIgd6 z;}eEU1V*0QelH!Gc^k(OJM)|9@rM}FLgoyu= zvVdaWj{*!Y?A}UzQRNK96F6yG;75z^1u&3gmNY_|!QmMp7<&gTGMPW5+8bTC)m|0V z6`XN=f}~Y_XVKLZjQAP)cFEX_1^Ox)9I>6e;t3xX*UomTN#9ESmGs;}4%~}cPa7le z*qb{NgVJ=bzxSIBIR{d$74^EE;C{v2B14`Fu@bLRRxB-vyPyS_vWea=;Kd<90lnwv zi>@n{2ygz;tvT&1^-XiAU0u%;1~%?@XTdLCc$k_6Ka4+MP&i&;4c>W%bn>BPhVbRK zXYkILY%#^o zmTIeeiUh;Qg*2F>zVz!5U3q7DiS`mr%OB#+g-tuwQAGf9Algy2H#VK2@Pfi`$zU3 ze*{)KHfAKJ3MwHYskwLmjF(IQdmpysE;O?>Ez1H#V+I4n}Bu`|6 zd+otmizg5_RzxB30|T;0hLT`#hn6D?rZ#J?=~13wDi$=1wWaoe@ALv*Q}$7O5yKWc zC)2Oh*EzT-H(K_2WQ+#rs233xYXY zvkV2pugl!hl^Xdmn*d!5J9@)6-0ug*$l3T9&DIacxnFD9)?U(~-F zGl&WW))v>MP75_VqG5Twz&pHO=y=EfiKmji;KCPz!<0r$Cohpa;PR>`fe_7=jr6iVmh1OXD1+a;StbFnBCEsx*1Y+);Ukn{uBnQU z35NT7Jc_4UqRI@Gxl&>}^pyflru0eHaf^e?z`x$wu02;hSIa=GajK(_zgqmW`=?6q zm^thl*5CU}H=niR%rfvfDkNZ+nZ8TCNrMTQeUXz2LVX<vNyTL1pN(3XRP}1q*E+-Q)J*KU--Oug*{Q6j+JAcw!9iD}Gk7Yb5 zNGi1$5-4ECL)+P-`^l+*O%utbG6KcvBU_#~k7~HQ1}= zt<%2v265%ym`D5B=eMW?%+u!$vqwIxu*X~r`7!?CX8=3|*8k-1Y@!*X2x9*u1RH1i zj29#gpuOgRDTV64_5IiI<(Isgnqxh4Qd~G}8WmJ3^r!>a`q} zLb+;sVbJ(2&#ueDl9@{w->3Fj=%HPk)0|@)K=Z7&6^j-wTt?EB6g$)l#vWFNFrcnNV&sb zf#RDl@vFQjviP1v4NZ(Zq#St0${*FwJAP(JezgpLE94QzLq08F6{>+)@}@MWl|B@ZIMB5)^V_39HvWT+OykjS-Z{S#_SyVaI|&`aPdowP#bjJsZS<=0`5aW+ZXYY z&OPUZNQW2(CSMX}t+m-Y9?#AIqdk{TkAqSaPV)HO`%kXs_G|ob z3;{vnh12^zi1Tly&K&l)UY@rxI}0raMs{g?9-jMr7fV+gM^{C+pFGQDStYb|`GX7h zkTxZ^jw}smg!z57I*_SlyNY+|RQ=epj3AlFjZA-!lp@LX+HSE1xzZT|%75OFhFZlv zZ**NbD{}ag7oZ+A>u`FVkUQsLhA^*i4JKh~Mo(&MgAlJ1V`qA<*dU-sQO%aoW4=$~ zG=<{SYxiSiF*R-)VEh{Die%|RU;f;ng^_{pZMwJ9gLB18X}_J*>43uNWXd#%W0tn9 zSKQt|R6sU)miP2)a#N-dkf~xLOmq9(eqM!nOS9!W{PD4EPxhrWp6~R#rY#)b`kASX zqR}8@l#|3M!BgMYKj)@i4VxYKTn0+qczGyH;lp0SkqPtc55CltkCEXyd)TOaL7oMNpSMoXa*WaEr_KQ64JdXMZh^+lO2zovb zbQZR$?J3C+aG)aqFtQLmsHeJ8AMC-!I@0jp9@mvlOxoMHd3f+6&K_HSA6_Urh*xsK zo9y{GAx6q$F$lEbXW)@Z!$bwEBxqbZ7=Ig_JMCzL@32c~2_^|Lhr&*=E|+w|A{a7< z`ZVzkHO|<<3545AjdKRg$sDECg%rzU+X&GtwY8jqA)4V0csyrA?(J)EQhh=FsT~VX zk#mNAA#Z$zHjU(KHTAZ3*}=o;h%}-nmI~51w)B1sZC9Ogx!7Z!jvXiHehyBmCZq;d zf}&CCTc?Z;dDDO1wtqp2wLn_3BgYwEwIj~yNAOl0gp2?9KAMd`Xd4vU8E-^ov$)83 zn#xFm&IcF(yxukpSGHjHPc@I{b*K%2v_tZU#c4JZ4J5vaaV%KoOnOynUj(9ua8BZ2 zuzTCd(O3$TRjdXkRV!;*Yl90{@afogJw_LB8q1r={D2VQpOcb(F6o~<|$B>_iQ;z`S1Udcnj ztjXY+sHzpq+#*uk-c^0Q_fKM? z-wRB0R5xsWAv7~9D+f!uh$$S=Kg4EpQ@AihRTg#@7G_Bf2{93N5pi}FQ86B7PLcNu zW^r+G9!W__K@$G|tBC;ule~q)XE!Snb~YaNzxT5#S9C@w-_!f6&by_pKW)z^-g(1w zH~dOvhmUUgb2olIn!l-1sTtBxRcKUVBO^(o&qbrYdKHk#{O(JUMq{G2iA4~FqqaMt zio!A7ktqE2r}OZqNwvVdVPoD~yT?MM;rFHI?f}O+ZAe=agYKp5(~`|irn?68i3n&A zDpoIGstqA$f=eIq5rnSUYx8bJirh`a*(13OmAxad454R&Zx=xb!tm&IScdf7aXMBA zUlZk>_r zGrkr3$?h!i;aoq1OOg%N4ZnVoJ7LJ1eGdpK!$&lsi7jK)&@-l6KfZsO!}$BTZxKkB zM5lq-m!#`qzL#)B{mCqKD3c{yr2?x;Q7NoU$XE=U|*se_SynokdBkw z1q$Mi%E$K4u!UJfSM8HSip$V58<2xq!M#fE$5F0Qg=NF#J!LwRkFm)Dt&dPS z;c{t-G9V)My2S~lPP(mxB5g@LI%zX#>u)4+AB$^)*{_iP?Nam05W=js$h%EZX|_Uz z=e--jChP3`L*vqBxYkX$HvtSsb{-|0Cl^DQ5uU!}$FuKR)~tthaBeuw@Sn`-H%@RA z$Op63>5`_|RTb$BG2j*Hl+JLB>B7!%(7;XK5pfe#Sb|o?{mNFHNqL^+ExTjqS_qVX zMj$RTJY+_2CNrXCKl?;bD>KT^{^0rN>%+aTbS62YMvp#j={+vm;Gax1j$iMDhTE%5 zkiLbvgZ|m$K;@h7$1=>C3G8X80SMnzWE1h(Sco7n#0kzcE51jC8%Ae%2Z}#Jt>Qj{ z%dGhSt@W>_s-rXg5`BQXdzQ=eO9aDyeAJ+^_H;TII5MCS>;+mg#+U_U^eFXhmskav zmZ!Y9SQna1xmu=^cp?_O)~MD}97$rn1oI06ul<+@=#_4@# zgG5zA>CW!}9WovU)nBGpXeQ;M1?b_jIJC9Zia`YGF3O`Kl(4D)5`gzxwMNc5aoAzN ztKv(|f4TohJ%8D1=!1u*JXhQkcVlmT{L9flJ(`pY!hqKp2LAVpEa*v{iv$PA3OyOk zxZAS`WU4+*{z5h;moH=g9<%hbM?VAh#sr)`R04#P)}yKoGj0O?EfmlI;Vt&)Iw`Q7 z33>ad$yNzrbT?&o6zQ%R3)v}Hj|&a9ul07nHUQ7oZ+CNl&dTol1Rvm#i`{-Z`R$Pq z1ot~Z?OqOVbLRvmJ0WaF%sIhK1;<1k-8g|W2A@P)W8=(eZPV(9oLqvpTxWD4-S241 zVha)$xy-Pf*#mw20CjhQH)=Pmu6t}-VB zWpIjrA21C{J&ahE{yu7+ao5OFfE-=XcXdQ(EB#OE54tRQ*^>UEUID~fG9ADwIK{SP zf_u24Ny1~sQS@moXO;^wd$2r|ln)HH6Cd^~Cpmiz8tNB9+~LRRy>tsV zI1=E5=CyZ>o4PR*abyD8oXRQF_D}3l?5aHF=b8hy-L;IQ2pa#LHD|D;`^=MP`kIRa z5?>g%&;Leq{Os(;e?z;g`9-&xh+(vv*D=!}(;?MW&gDO;%F(;BPIYakEg=SS5==5i zJrrb(cs?2=>4j~y=~!=kYrsm;#95u}(UY^6^E=@z*O;r$a#(PyD%IQlFAmmSHpk@N z9o@at_7B$XB`7zQ)6X(fx|--EW&Nr^e{1jbI5z6G>b9cQM9~{@cFGj%!X@l=XQ6UuY%#fEx^U2bCb4+zB(j*E#YkH&pFXFbAgD2zXu(IO9XX-X>cQ9BvT`26w#- zRy>eYLHkMnflI*g+snnk)r3PU^R1DBMEd!xzdeoEfhwR4u1Yqx(Bpj+ z-i#UU0_kMfR>Ba)^e-ez*5Px~bJBf7W13az$DA94Zp&EM@8td$#<>xmDc>ojke^oooJ@q*5An*Ej>O*E&Hdr>$epJi6Zas|SpkC!NySaJ(JF*=Z zeTq?@6#qqO4PVkzz7S@2uiNl{P`1oBxas^(nCs3lBjg6*-xvUP6Hb5M{!8`m2-GQI zH02flA!dpS!q`Il4?5igiI#tPFGav-fZzFVA{irC_R(h`%`wCN?BmZs@rd4Bq4D`# z_G{yxiyY&d!wuR6FWTE~KxoJXW~lA$SZ)R|Ks+%PunUX>!E=h)eYOv(1|c=|BQL|Z z8*?qY`81>4^}h$kh;3$qpdzOa@%`}J@MYWn+(?Jp{QRNy6>kf1ESHE*@QnQ*TM(AE zdHuk+wyFH!h&R^43jb~Y@i51YYJ zllhL!-+V5KLfVR+uGOg5VAEDAi)tX>B|l;)tS@&KQU~v^6Y`XH!)otmAVx(lMiiUYh%l3>s!K6@V}#xVKHkVYhl&W z*1o>+XY@So^OGvAOy{jL(yyj?9~qB#eSG&xNKv# zj(-gPWvoqbJ`?PmPyy@RA6jPHz9z({5s*%($h{`q5K=oh1QBaav_(jT3ACV~Y?JZ_4_`v%^|3wR zD%T0AT05Q=75Y z%`}t*OFn1FY+yHEQuwtU)X!R2w%u__VlS>E;%8FjFK*Twu*2ymZchpk_Q{#N4H2AC ze=<(|E8Mad{@F~lqZcz*^z`5k%F&oIni)?aK5S~-Zbr?wj}WRkKjP5f^qpn3s1Q|X z6i0zFzTsn#Dhz5EG%81`zwbL)D%3>dx7n1U z*6fNIxT{NRJIit9wT`(uOL67(N9#B%ak-G#4ni8Z>%i$>Npp3`7+i^S=|>x0$!jTK zUu*F%A#I3icg)AZNt<5ja+#9G59)0=tHXpCW{tcJsnv;GuaZ>*g7Uu@=d-|*+YlRI zm`nJKY^f$@bIUmJ`Ni>8Xz(V$t5q6y$-6kO6GaH79bM$7e+jZi38fVD@}NHMh*cw!T#E(a>q8_G zZ!Wb#yep=9Io=fp)hNRI5rzCM@MJ>XUL1E|2(rH!YPTg+Kez0M zNv8;8p~xF2hyI6AZfgt{_B4@+FFN=`52m~dS3i1SS?>Kl?3s&VdiQgW8)kWLYwh(i zZ-|u%rGymNeK0c&wWO97bLB_@6{LKSaHNhGLn9ngY&b>UYpsYyF^f?D5fLnya#awE zGU!XaDF%!Z#WM{B{9H1{8J``vCla^y&bo5lid~Fm-!t+Mx3$RXXrk4vn%!s0k6k=w ze_VnsYNSFc1q5_$=eEnbF{<6IFB7B+8wC{%9uuwXrPY9T9$oyo`M3D-0LzQ};S6Vw z*b2v3mRAh32_yEQLLpqUl{gm70N>cge0;OLJAh^Lc?@R_u!=Ph5**shkJ}qvWv-*L z?7y-8IoN$OBpoPKYdL;Son~80I4H|dTclk~XpDJM4;gD}&3RU&oqB{j7(8)6y=Xcm zRr_Ilh+5Ma7jJNv&bCO~^S}{PuI5*qX=7@e3Vj0vS2Ty_qGWAH^a{16COrONA+3Iq zHlTE1gDF=b9XFJirOTfexu)c!3;)FY@9F2i79hR<3EM&R$C|l%^id zex> zL!~Zp@_N*~V2Jx&y}+4vK6Zq23Hu3Ry)Akis4M#Y{{#I0yZDEP0FFt&SG~Q_Kl9i= zZzv9d<^c#64(6_IE*2*Ce@Tv}HVCe6CN6GXE*6#u92~4{T&xI`lu!~%k_i6;^6w=3 diff --git a/saw-remote-api/CHANGELOG.md b/saw-remote-api/CHANGELOG.md index a7e3531764..fc378f9f76 100644 --- a/saw-remote-api/CHANGELOG.md +++ b/saw-remote-api/CHANGELOG.md @@ -25,6 +25,8 @@ * The API for `"struct"` `setup value`s now has a `"MIR ADT"` field. For MIR verification, this field is required. For LLVM and JVM verification, this field must be `null`, or else an error will be raised. +* The `SAW/create ghost variable` command and the associated + `ghost variable value` value are now supported with JVM and MIR verification. ## 1.0.0 -- 2023-06-26 diff --git a/saw-remote-api/python/CHANGELOG.md b/saw-remote-api/python/CHANGELOG.md index 6a25dcc327..f5970d01a5 100644 --- a/saw-remote-api/python/CHANGELOG.md +++ b/saw-remote-api/python/CHANGELOG.md @@ -29,6 +29,8 @@ * Add a `proclaim_f` function. This behaves like the `proclaim` function, except that it takes a `cry_f`-style format string as an argument. That is, `proclaim_f(...)` is equivalent to `proclaim(cry_f(...))`. +* The `create_ghost_variable()` and `ghost_value()` functions are now supported + with JVM and MIR verification. ## 1.0.1 -- YYYY-MM-DD diff --git a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs index 7f051c5fe0..f8176fce2b 100644 --- a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs @@ -26,7 +26,7 @@ import qualified Data.Map as Map import qualified Cryptol.Parser.AST as P import Cryptol.Utils.Ident (mkIdent) import qualified Lang.Crucible.JVM as CJ -import SAWScript.Crucible.Common.MethodSpec as MS (SetupValue(..)) +import qualified SAWScript.Crucible.Common.MethodSpec as MS import SAWScript.Crucible.JVM.Builtins ( jvm_alloc_array, jvm_alloc_object, @@ -35,6 +35,7 @@ import SAWScript.Crucible.JVM.Builtins jvm_static_field_is, jvm_execute_func, jvm_fresh_var, + jvm_ghost_value, jvm_postcond, jvm_precond, jvm_return ) @@ -56,10 +57,11 @@ import SAWServer import SAWServer.Data.Contract ( PointsTo(PointsTo), PointsToBitfield, + GhostValue(GhostValue), Allocated(Allocated), ContractVar(ContractVar), - Contract(preVars, preConds, preAllocated, prePointsTos, prePointsToBitfields, - argumentVals, postVars, postConds, postAllocated, postPointsTos, postPointsToBitfields, + Contract(preVars, preConds, preAllocated, preGhostValues, prePointsTos, prePointsToBitfields, + argumentVals, postVars, postConds, postAllocated, postGhostValues, postPointsTos, postPointsToBitfields, returnVal) ) import SAWServer.Data.SetupValue () import SAWServer.CryptolExpression (CryptolModuleException(..), getTypedTermOfCExp) @@ -82,28 +84,29 @@ instance Doc.DescribedMethod StartJVMSetupParams OK where ] resultFieldDescription = [] -newtype ServerSetupVal = Val (SetupValue CJ.JVM) +newtype ServerSetupVal = Val (MS.SetupValue CJ.JVM) compileJVMContract :: (FilePath -> IO ByteString) -> BuiltinContext -> + Map ServerName MS.GhostGlobal -> CryptolEnv -> Contract JavaType (P.Expr P.PName) -> JVMSetupM () -compileJVMContract fileReader bic cenv0 c = +compileJVMContract fileReader bic ghostEnv cenv0 c = do allocsPre <- mapM setupAlloc (preAllocated c) (envPre, cenvPre) <- setupState allocsPre (Map.empty, cenv0) (preVars c) mapM_ (\p -> getTypedTerm cenvPre p >>= jvm_precond) (preConds c) mapM_ (setupPointsTo (envPre, cenvPre)) (prePointsTos c) mapM_ setupPointsToBitfields (prePointsToBitfields c) - --mapM_ (setupGhostValue ghostEnv cenvPre) (preGhostValues c) + mapM_ (setupGhostValue ghostEnv cenvPre) (preGhostValues c) traverse (getSetupVal (envPre, cenvPre)) (argumentVals c) >>= jvm_execute_func allocsPost <- mapM setupAlloc (postAllocated c) (envPost, cenvPost) <- setupState (allocsPre ++ allocsPost) (envPre, cenvPre) (postVars c) mapM_ (\p -> getTypedTerm cenvPost p >>= jvm_postcond) (postConds c) mapM_ (setupPointsTo (envPost, cenvPost)) (postPointsTos c) mapM_ setupPointsToBitfields (postPointsToBitfields c) - --mapM_ (setupGhostValue ghostEnv cenvPost) (postGhostValues c) + mapM_ (setupGhostValue ghostEnv cenvPost) (postGhostValues c) case returnVal c of Just v -> getSetupVal (envPost, cenvPost) v >>= jvm_return Nothing -> return () @@ -149,7 +152,10 @@ compileJVMContract fileReader bic cenv0 c = setupPointsToBitfields _ = JVMSetupM $ fail "Points-to-bitfield not supported in JVM API." - --setupGhostValue _ _ _ = fail "Ghost values not supported yet in JVM API." + setupGhostValue genv cenv (GhostValue serverName e) = + do g <- resolve genv serverName + t <- getTypedTerm cenv e + jvm_ghost_value g t resolve :: Map ServerName a -> ServerName -> JVMSetupM a resolve env name = diff --git a/saw-remote-api/src/SAWServer/JVMVerify.hs b/saw-remote-api/src/SAWServer/JVMVerify.hs index f7c97654ed..293d424e79 100644 --- a/saw-remote-api/src/SAWServer/JVMVerify.hs +++ b/saw-remote-api/src/SAWServer/JVMVerify.hs @@ -9,6 +9,7 @@ module SAWServer.JVMVerify import Prelude hiding (mod) import Control.Lens +import qualified Data.Map as Map import SAWScript.Crucible.JVM.Builtins ( jvm_unsafe_assume_spec, jvm_verify ) @@ -26,6 +27,7 @@ import SAWServer pushTask, dropTask, setServerVal, + getGhosts, getJVMClass, getJVMMethodSpecIR ) import SAWServer.CryptolExpression (getCryptolExpr) @@ -51,7 +53,8 @@ jvmVerifyAssume mode (VerifyParams className fun lemmaNames checkSat contract sc let bic = view sawBIC state cenv = rwCryptol (view sawTopLevelRW state) fileReader <- Argo.getFileReader - setup <- compileJVMContract fileReader bic cenv <$> traverse getCryptolExpr contract + ghostEnv <- Map.fromList <$> getGhosts + setup <- compileJVMContract fileReader bic ghostEnv cenv <$> traverse getCryptolExpr contract res <- case mode of VerifyContract -> do lemmas <- mapM getJVMMethodSpecIR lemmaNames diff --git a/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs b/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs index e2b5942741..152911fa71 100644 --- a/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs @@ -30,6 +30,7 @@ import SAWScript.Crucible.MIR.Builtins mir_alloc_mut, mir_fresh_var, mir_execute_func, + mir_ghost_value, mir_load_module, mir_points_to, mir_postcond, @@ -55,10 +56,11 @@ import SAWServer.CryptolExpression (CryptolModuleException(..), getTypedTermOfCE import SAWServer.Data.Contract ( PointsTo(PointsTo), PointsToBitfield, + GhostValue(GhostValue), Allocated(Allocated), ContractVar(ContractVar), - Contract(preVars, preConds, preAllocated, prePointsTos, prePointsToBitfields, - argumentVals, postVars, postConds, postAllocated, postPointsTos, postPointsToBitfields, + Contract(preVars, preConds, preAllocated, preGhostValues, prePointsTos, prePointsToBitfields, + argumentVals, postVars, postConds, postAllocated, postGhostValues, postPointsTos, postPointsToBitfields, returnVal) ) import SAWServer.Data.MIRType (JSONMIRType, mirType) import SAWServer.Exceptions ( notAtTopLevel ) @@ -71,24 +73,25 @@ newtype ServerSetupVal = Val (MS.SetupValue MIR) compileMIRContract :: (FilePath -> IO ByteString) -> BuiltinContext -> + Map ServerName MS.GhostGlobal -> CryptolEnv -> SAWEnv -> Contract JSONMIRType (P.Expr P.PName) -> MIRSetupM () -compileMIRContract fileReader bic cenv0 sawenv c = +compileMIRContract fileReader bic ghostEnv cenv0 sawenv c = do allocsPre <- mapM setupAlloc (preAllocated c) (envPre, cenvPre) <- setupState allocsPre (Map.empty, cenv0) (preVars c) mapM_ (\p -> getTypedTerm cenvPre p >>= mir_precond) (preConds c) mapM_ (setupPointsTo (envPre, cenvPre)) (prePointsTos c) mapM_ setupPointsToBitfields (prePointsToBitfields c) - --mapM_ (setupGhostValue ghostEnv cenvPre) (preGhostValues c) + mapM_ (setupGhostValue ghostEnv cenvPre) (preGhostValues c) traverse (getSetupVal (envPre, cenvPre)) (argumentVals c) >>= mir_execute_func allocsPost <- mapM setupAlloc (postAllocated c) (envPost, cenvPost) <- setupState (allocsPre ++ allocsPost) (envPre, cenvPre) (postVars c) mapM_ (\p -> getTypedTerm cenvPost p >>= mir_postcond) (postConds c) mapM_ (setupPointsTo (envPost, cenvPost)) (postPointsTos c) mapM_ setupPointsToBitfields (postPointsToBitfields c) - --mapM_ (setupGhostValue ghostEnv cenvPost) (postGhostValues c) + mapM_ (setupGhostValue ghostEnv cenvPost) (postGhostValues c) case returnVal c of Just v -> getSetupVal (envPost, cenvPost) v >>= mir_return Nothing -> return () @@ -133,7 +136,10 @@ compileMIRContract fileReader bic cenv0 sawenv c = setupPointsToBitfields _ = MIRSetupM $ fail "Points-to-bitfield not supported in the MIR API." - --setupGhostValue _ _ _ = fail "Ghost values not supported yet in the MIR API." + setupGhostValue genv cenv (GhostValue serverName e) = + do g <- resolve genv serverName + t <- getTypedTerm cenv e + mir_ghost_value g t resolve :: Map ServerName a -> ServerName -> MIRSetupM a resolve env name = diff --git a/saw-remote-api/src/SAWServer/MIRVerify.hs b/saw-remote-api/src/SAWServer/MIRVerify.hs index 09261a2f8c..9728001b74 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_verify ) @@ -26,6 +27,7 @@ import SAWServer pushTask, dropTask, setServerVal, + getGhosts, getMIRModule, getMIRMethodSpecIR ) import SAWServer.CryptolExpression (getCryptolExpr) @@ -53,7 +55,8 @@ mirVerifyAssume mode (VerifyParams modName fun lemmaNames checkSat contract scri cenv = rwCryptol (view sawTopLevelRW state) sawenv = view sawEnv state fileReader <- Argo.getFileReader - setup <- compileMIRContract fileReader bic cenv sawenv <$> + ghostEnv <- Map.fromList <$> getGhosts + setup <- compileMIRContract fileReader bic ghostEnv cenv sawenv <$> traverse getCryptolExpr contract res <- case mode of VerifyContract -> do diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index ed3e3d92ff..98782f6196 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -27,6 +27,7 @@ import Data.Functor import Control.Applicative import Data.Monoid #endif +import Control.Lens (view) import Control.Monad.Except (MonadError(..)) import Control.Monad.State import qualified Control.Exception as Ex @@ -132,7 +133,8 @@ import SAWScript.Value (ProofScript, printOutLnTop, AIGNetwork) import SAWScript.SolverCache import SAWScript.SolverVersions -import SAWScript.Crucible.Common.MethodSpec (ppTypedTermType) +import qualified SAWScript.Crucible.Common.MethodSpec as MS +import SAWScript.Crucible.Common.Setup.Type (addCondition, croTags) import SAWScript.Prover.Util(checkBooleanSchema) import SAWScript.Prover.SolverStats import qualified SAWScript.Prover.SBV as Prover @@ -158,7 +160,7 @@ definePrim name (TypedTerm (TypedTermSchema schema) rhs) = definePrim _name (TypedTerm tp _) = fail $ unlines [ "Expected term with Cryptol schema type, but got" - , show (ppTypedTermType tp) + , show (MS.ppTypedTermType tp) ] sbvUninterpreted :: String -> Term -> TopLevel Uninterp @@ -696,7 +698,7 @@ term_type tt = TypedTermSchema sch -> pure sch tp -> fail $ unlines [ "Term does not have a Cryptol type" - , show (ppTypedTermType tp) + , show (MS.ppTypedTermType tp) ] goal_eval :: [String] -> ProofScript () @@ -2474,3 +2476,18 @@ declare_ghost_state name = do allocator <- getHandleAlloc global <- liftIO (freshGlobalVar allocator (Text.pack name) knownRepr) return (SV.VGhostVar global) + +ghost_value :: + MS.GhostGlobal -> + TypedTerm -> + SV.CrucibleSetup ext () +ghost_value ghost val = + do loc <- SV.getW4Position "ghost_value" + tags <- view croTags + let md = MS.ConditionMetadata + { MS.conditionLoc = loc + , MS.conditionTags = tags + , MS.conditionType = "ghost value" + , MS.conditionContext = "" + } + addCondition (MS.SetupCond_Ghost md ghost val) diff --git a/src/SAWScript/Crucible/Common/MethodSpec.hs b/src/SAWScript/Crucible/Common/MethodSpec.hs index 3f78ae8d85..f856318673 100644 --- a/src/SAWScript/Crucible/Common/MethodSpec.hs +++ b/src/SAWScript/Crucible/Common/MethodSpec.hs @@ -13,8 +13,10 @@ Grow\", and is prevalent across the Crucible codebase. {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} @@ -22,6 +24,7 @@ Grow\", and is prevalent across the Crucible codebase. {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeFamilyDependencies #-} {-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -Wno-orphans #-} module SAWScript.Crucible.Common.MethodSpec ( AllocIndex(..) @@ -61,7 +64,6 @@ module SAWScript.Crucible.Common.MethodSpec , setupToTypedTerm , setupToTerm - , XGhostState , GhostValue , GhostType , GhostGlobal @@ -117,6 +119,7 @@ import Data.Set (Set) import Data.Time.Clock import Data.Void (absurd) +import Control.Monad (when) import Control.Monad.Trans.Maybe import Control.Monad.Trans (lift) import Control.Lens @@ -131,13 +134,17 @@ import Lang.Crucible.JVM (JVM) import qualified Lang.Crucible.Types as Crucible (IntrinsicType, EmptyCtx) import qualified Lang.Crucible.CFG.Common as Crucible (GlobalVar) +import qualified Lang.Crucible.Simulator.Intrinsics as Crucible import Mir.Intrinsics (MIR) +import qualified Cryptol.TypeCheck.Type as Cryptol (Schema) import qualified Cryptol.Utils.PP as Cryptol import Verifier.SAW.TypedTerm as SAWVerifier import Verifier.SAW.SharedTerm as SAWVerifier +import Verifier.SAW.Simulator.What4.ReturnTrip as SAWVerifier +import SAWScript.Crucible.Common (Sym, sawCoreState) import SAWScript.Crucible.Common.Setup.Value import SAWScript.Crucible.LLVM.Setup.Value (LLVM) import SAWScript.Crucible.JVM.Setup.Value () @@ -323,21 +330,33 @@ type GhostValue = "GhostValue" type GhostType = Crucible.IntrinsicType GhostValue Crucible.EmptyCtx type GhostGlobal = Crucible.GlobalVar GhostType +instance Crucible.IntrinsicClass Sym GhostValue where + type Intrinsic Sym GhostValue ctx = (Cryptol.Schema, Term) + muxIntrinsic sym _ _namerep _ctx prd (thnSch,thn) (elsSch,els) = + do when (thnSch /= elsSch) $ fail $ unlines $ + [ "Attempted to mux ghost variables of different types:" + , show (Cryptol.pp thnSch) + , show (Cryptol.pp elsSch) + ] + st <- sawCoreState sym + let sc = saw_ctx st + prd' <- toSC sym st prd + typ <- scTypeOf sc thn + res <- scIte sc typ prd' thn els + return (thnSch, res) + -------------------------------------------------------------------------------- -- *** StateSpec data SetupCondition ext where SetupCond_Equal :: ConditionMetadata -> SetupValue ext -> SetupValue ext -> SetupCondition ext SetupCond_Pred :: ConditionMetadata -> TypedTerm -> SetupCondition ext - SetupCond_Ghost :: XGhostState ext -> - ConditionMetadata -> + SetupCond_Ghost :: ConditionMetadata -> GhostGlobal -> TypedTerm -> SetupCondition ext -deriving instance ( SetupValueHas Show ext - , Show (XGhostState ext) - ) => Show (SetupCondition ext) +deriving instance SetupValueHas Show ext => Show (SetupCondition ext) -- | Verification state (either pre- or post-) specification data StateSpec ext = StateSpec diff --git a/src/SAWScript/Crucible/Common/Override.hs b/src/SAWScript/Crucible/Common/Override.hs index 6e01203e38..84d1e48890 100644 --- a/src/SAWScript/Crucible/Common/Override.hs +++ b/src/SAWScript/Crucible/Common/Override.hs @@ -55,11 +55,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 (unless) +import Control.Monad (unless, when) import Control.Monad.Trans.State hiding (get, put) import Control.Monad.State.Class (MonadState(..)) import Control.Monad.Error.Class (MonadError) @@ -70,6 +75,7 @@ import Control.Monad.Trans.Class import Control.Monad.IO.Class import qualified Data.Map as Map import Data.Map (Map) +import qualified Data.Set as Set import Data.Set (Set) import Data.Typeable (Typeable) import Data.Void @@ -80,9 +86,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.CFG.Core as Crucible (TypeRepr, GlobalVar) import qualified Lang.Crucible.Simulator.GlobalState as Crucible import qualified Lang.Crucible.Simulator.RegMap as Crucible @@ -404,3 +414,102 @@ assignmentToList :: Ctx.Assignment (Crucible.RegEntry sym) ctx -> [Crucible.AnyValue sym] assignmentToList = toListFC (\(Crucible.RegEntry x y) -> Crucible.AnyValue x y) + +------------------------------------------------------------------------ + +learnGhost :: + SharedContext -> + MS.ConditionMetadata -> + PrePost -> + MS.GhostGlobal -> + TypedTerm -> + OverrideMatcher ext md () +learnGhost sc md prepost var (TypedTerm (TypedTermSchema schEx) tmEx) = + do (sch,tm) <- readGlobal var + when (sch /= schEx) $ fail $ unlines $ + [ "Ghost variable had the wrong type:" + , "- Expected: " ++ show (Cryptol.pp schEx) + , "- Actual: " ++ show (Cryptol.pp sch) + ] + instantiateExtMatchTerm sc md prepost tm tmEx +learnGhost _sc _md _prepost _var (TypedTerm tp _) + = fail $ unlines + [ "Ghost variable expected value has improper type" + , "expected Cryptol schema type, but got" + , show (MS.ppTypedTermType tp) + ] + +executeGhost :: + SharedContext -> + MS.ConditionMetadata -> + MS.GhostGlobal -> + TypedTerm -> + OverrideMatcher ext RW () +executeGhost sc _md var (TypedTerm (TypedTermSchema sch) tm) = + do s <- OM (use termSub) + tm' <- liftIO (scInstantiateExt sc s tm) + writeGlobal var (sch,tm') +executeGhost _sc _md _var (TypedTerm tp _) = + fail $ unlines + [ "executeGhost: improper value type" + , "expected Cryptol schema type, but got" + , show (MS.ppTypedTermType tp) + ] + +-- | NOTE: The two 'Term' arguments must have the same type. +instantiateExtMatchTerm :: + SharedContext {- ^ context for constructing SAW terms -} -> + MS.ConditionMetadata -> + PrePost -> + Term {- ^ exported concrete term -} -> + Term {- ^ expected specification term -} -> + OverrideMatcher ext md () +instantiateExtMatchTerm sc md prepost actual expected = do + sub <- OM (use termSub) + matchTerm sc md prepost actual =<< liftIO (scInstantiateExt sc sub expected) + +matchTerm :: + SharedContext {- ^ context for constructing SAW terms -} -> + MS.ConditionMetadata -> + PrePost -> + Term {- ^ exported concrete term -} -> + Term {- ^ expected specification term -} -> + OverrideMatcher ext md () + +matchTerm _ _ _ real expect | real == expect = return () +matchTerm sc md prepost real expect = + do let loc = MS.conditionLoc md + free <- OM (use osFree) + case unwrapTermF expect of + FTermF (ExtCns ec) + | Set.member (ecVarIndex ec) free -> + do assignTerm sc md prepost (ecVarIndex ec) real + + _ -> + do t <- liftIO $ scEq sc real expect + let msg = unlines $ + [ "Literal equality " ++ MS.stateCond prepost +-- , "Expected term: " ++ prettyTerm expect +-- , "Actual term: " ++ prettyTerm real + ] + addTermEq t md $ Crucible.SimError loc $ Crucible.AssertFailureSimError msg "" +-- where prettyTerm = show . ppTermDepth 20 + +assignTerm :: + SharedContext {- ^ context for constructing SAW terms -} -> + MS.ConditionMetadata -> + PrePost -> + VarIndex {- ^ external constant index -} -> + Term {- ^ value -} -> + OverrideMatcher ext md () + +assignTerm sc md prepost var val = + do mb <- OM (use (termSub . at var)) + case mb of + Nothing -> OM (termSub . at var ?= val) + Just old -> + matchTerm sc md prepost val old + +-- do t <- liftIO $ scEq sc old val +-- p <- liftIO $ resolveSAWPred cc t +-- addAssert p (Crucible.AssertFailureSimError ("literal equality " ++ MS.stateCond prepost)) diff --git a/src/SAWScript/Crucible/Common/Setup/Value.hs b/src/SAWScript/Crucible/Common/Setup/Value.hs index b96b9b2ad8..b9ecb027a9 100644 --- a/src/SAWScript/Crucible/Common/Setup/Value.hs +++ b/src/SAWScript/Crucible/Common/Setup/Value.hs @@ -50,8 +50,6 @@ module SAWScript.Crucible.Common.Setup.Value , SetupValue(..) , SetupValueHas - , XGhostState - , ConditionMetadata(..) , MethodId @@ -176,15 +174,6 @@ deriving instance (SetupValueHas Show ext) => Show (SetupValue ext) -- deriving instance (SetupValueHas Eq ext) => Eq (SetupValue ext) -- deriving instance (SetupValueHas Ord ext) => Ord (SetupValue ext) --------------------------------------------------------------------------------- --- ** Ghost state - --- | This extension field controls whether ghost state is enabled for a --- particular language backend. At the moment, ghost state is only enabled for --- the LLVM backend, but we want to expand this to cover other language backends --- in the future. See . -type family XGhostState ext - -------------------------------------------------------------------------------- -- ** Pre- and post-conditions diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs index a3920359f6..001bfb0b78 100644 --- a/src/SAWScript/Crucible/JVM/Builtins.hs +++ b/src/SAWScript/Crucible/JVM/Builtins.hs @@ -44,6 +44,7 @@ module SAWScript.Crucible.JVM.Builtins , jvm_alloc_object , jvm_alloc_array , jvm_setup_with_tag + , jvm_ghost_value ) where import Control.Lens @@ -67,7 +68,6 @@ import Data.Text (Text) import qualified Data.Text as Text import Data.Time.Clock (getCurrentTime, diffUTCTime) import qualified Data.Vector as V -import Data.Void (absurd) import Prettyprinter import System.IO @@ -109,6 +109,7 @@ import Verifier.SAW.TypedTerm import Verifier.SAW.Simulator.What4.ReturnTrip +import SAWScript.Builtins (ghost_value) import SAWScript.Exceptions import SAWScript.Panic import SAWScript.Proof @@ -412,7 +413,8 @@ verifyPrestate cc mspec globals0 = (env, globals1) <- runStateT (Map.traverseWithKey doAlloc preallocs) globals0' globals2 <- setupPrePointsTos mspec cc env (mspec ^. MS.csPreState . MS.csPointsTos) globals1 - cs <- setupPrestateConditions mspec cc env (mspec ^. MS.csPreState . MS.csConditions) + (globals3, cs) <- + setupPrestateConditions mspec cc env globals2 (mspec ^. MS.csPreState . MS.csConditions) args <- resolveArguments cc mspec env -- Check the type of the return setup value @@ -432,7 +434,7 @@ verifyPrestate cc mspec globals0 = ] (Nothing, _) -> return () - return (args, cs, env, globals2) + return (args, cs, env, globals3) -- | Check two Types for register compatibility. registerCompatible :: J.Type -> J.Type -> Bool @@ -537,32 +539,43 @@ setupPrePointsTos mspec cc env pts mem0 = foldM doPointsTo mem0 pts _ -> panic "setupPrePointsTo" ["invalid invariant", "jvm_modifies in pre-state"] --- | Collects boolean terms that should be assumed to be true. +-- | Sets up globals (ghost variable), and collects boolean terms +-- that should be assumed to be true. setupPrestateConditions :: MethodSpec -> JVMCrucibleContext -> Map AllocIndex JVMRefVal -> + Crucible.SymGlobalState Sym -> [SetupCondition] -> - IO [Crucible.LabeledPred Term AssumptionReason] + IO ( Crucible.SymGlobalState Sym, [Crucible.LabeledPred Term AssumptionReason] + ) setupPrestateConditions mspec cc env = aux [] where tyenv = MS.csAllocations mspec nameEnv = mspec ^. MS.csPreState . MS.csVarTypeNames - aux acc [] = return acc + aux acc globals [] = return (globals, acc) - aux acc (MS.SetupCond_Equal loc val1 val2 : xs) = + aux acc globals (MS.SetupCond_Equal loc val1 val2 : xs) = do val1' <- resolveSetupVal cc env tyenv nameEnv val1 val2' <- resolveSetupVal cc env tyenv nameEnv val2 t <- assertEqualVals cc val1' val2' let lp = Crucible.LabeledPred t (loc, "equality precondition") - aux (lp:acc) xs + aux (lp:acc) globals xs - aux acc (MS.SetupCond_Pred loc tm : xs) = + aux acc globals (MS.SetupCond_Pred loc tm : xs) = let lp = Crucible.LabeledPred (ttTerm tm) (loc, "precondition") in - aux (lp:acc) xs - - aux _ (MS.SetupCond_Ghost empty_ _ _ _ : _) = absurd empty_ + aux (lp:acc) globals xs + + aux acc globals (MS.SetupCond_Ghost _md var val : xs) = + case val of + TypedTerm (TypedTermSchema sch) tm -> + aux acc (Crucible.insertGlobal var (sch,tm) globals) xs + TypedTerm tp _ -> + fail $ unlines + [ "Setup term for global variable expected to have Cryptol schema type, but got" + , show (MS.ppTypedTermType tp) + ] -------------------------------------------------------------------------------- @@ -1418,6 +1431,13 @@ jvm_setup_with_tag :: jvm_setup_with_tag tag m = JVMSetupM (Setup.setupWithTag tag (runJVMSetupM m)) +jvm_ghost_value :: + MS.GhostGlobal -> + TypedTerm -> + JVMSetupM () +jvm_ghost_value ghost val = JVMSetupM $ + ghost_value ghost val + -------------------------------------------------------------------------------- -- | Sort a list of things and group them into equivalence classes. diff --git a/src/SAWScript/Crucible/JVM/Override.hs b/src/SAWScript/Crucible/JVM/Override.hs index 5ba395b742..5751adbef8 100644 --- a/src/SAWScript/Crucible/JVM/Override.hs +++ b/src/SAWScript/Crucible/JVM/Override.hs @@ -92,7 +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 @@ -326,13 +325,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 +349,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 +372,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)) @@ -523,26 +534,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 -} -> @@ -562,7 +553,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 @@ -620,32 +611,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 :: @@ -656,9 +621,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 ------------------------------------------------------------------------ @@ -731,7 +698,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. @@ -775,6 +742,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 @@ -814,10 +790,13 @@ executeSetupCondition :: JVMCrucibleContext -> CrucibleMethodSpecIR -> SetupCondition -> - OverrideMatcher CJ.JVM w () -executeSetupCondition opts sc cc spec (MS.SetupCond_Equal md val1 val2) = executeEqual opts sc cc spec md val1 val2 -executeSetupCondition _opts sc cc _ (MS.SetupCond_Pred md tm) = executePred sc cc md tm -executeSetupCondition _ _ _ _ (MS.SetupCond_Ghost empty _ _ _) = absurd empty + OverrideMatcher CJ.JVM RW () +executeSetupCondition opts sc cc spec = + \case + MS.SetupCond_Equal md val1 val2 -> + executeEqual opts sc cc spec md val1 val2 + MS.SetupCond_Pred md tm -> executePred sc cc md tm + MS.SetupCond_Ghost md var val -> executeGhost sc md var val ------------------------------------------------------------------------ diff --git a/src/SAWScript/Crucible/JVM/Setup/Value.hs b/src/SAWScript/Crucible/JVM/Setup/Value.hs index edf3c80581..7c77b15e1f 100644 --- a/src/SAWScript/Crucible/JVM/Setup/Value.hs +++ b/src/SAWScript/Crucible/JVM/Setup/Value.hs @@ -86,8 +86,6 @@ type instance MS.XSetupCast CJ.JVM = Void type instance MS.XSetupUnion CJ.JVM = Void type instance MS.XSetupGlobalInitializer CJ.JVM = Void -type instance MS.XGhostState CJ.JVM = Void - type JIdent = String -- FIXME(huffman): what to put here? type instance MS.TypeName CJ.JVM = JIdent diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index 0977cb7570..3f109de81c 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -184,6 +184,7 @@ import Verifier.SAW.TypedTerm -- saw-script import SAWScript.AST (Located(..)) +import SAWScript.Builtins (ghost_value) import SAWScript.Proof import SAWScript.Prover.SolverStats import SAWScript.Prover.Versions @@ -1201,7 +1202,7 @@ setupPrestateConditions mspec cc mem env = aux [] let lp = Crucible.LabeledPred (ttTerm tm) (md, "precondition") in aux (lp:acc) globals xs - aux acc globals (MS.SetupCond_Ghost () _md var val : xs) = + aux acc globals (MS.SetupCond_Ghost _md var val : xs) = case val of TypedTerm (TypedTermSchema sch) tm -> aux acc (Crucible.insertGlobal var (sch,tm) globals) xs @@ -2795,15 +2796,7 @@ llvm_ghost_value :: TypedTerm -> LLVMCrucibleSetupM () llvm_ghost_value ghost val = LLVMCrucibleSetupM $ - do loc <- getW4Position "llvm_ghost_value" - tags <- view Setup.croTags - let md = MS.ConditionMetadata - { MS.conditionLoc = loc - , MS.conditionTags = tags - , MS.conditionType = "ghost value" - , MS.conditionContext = "" - } - Setup.addCondition (MS.SetupCond_Ghost () md ghost val) + ghost_value ghost val llvm_spec_solvers :: SomeLLVM MS.ProvedSpec -> [String] llvm_spec_solvers (SomeLLVM ps) = diff --git a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs index 2ed66092e3..d64181171e 100644 --- a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs @@ -12,11 +12,9 @@ Stability : provisional {-# LANGUAGE DoAndIfThenElse #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE LambdaCase #-} -{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE PatternSynonyms #-} @@ -119,16 +117,12 @@ module SAWScript.Crucible.LLVM.MethodSpecIR ) where import Control.Lens -import Control.Monad (when) import Data.Functor.Compose (Compose(..)) import qualified Data.Map as Map import qualified Prettyprinter as PPL import qualified Text.LLVM.AST as L import qualified Text.LLVM.PP as L -import qualified Cryptol.TypeCheck.AST as Cryptol -import qualified Cryptol.Utils.PP as Cryptol (pp) - import Data.Parameterized.All (All(All)) import Data.Parameterized.Some (Some(Some)) import qualified Data.Parameterized.Map as MapF @@ -137,7 +131,7 @@ import What4.ProgramLoc (ProgramLoc) import qualified Lang.Crucible.Types as Crucible (SymbolRepr, knownSymbol) import qualified Lang.Crucible.Simulator.Intrinsics as Crucible - (IntrinsicClass(Intrinsic, muxIntrinsic), IntrinsicMuxFn(IntrinsicMuxFn)) + (IntrinsicMuxFn(IntrinsicMuxFn)) import SAWScript.Crucible.Common import qualified SAWScript.Crucible.Common.MethodSpec as MS @@ -146,9 +140,6 @@ import qualified SAWScript.Crucible.Common.Setup.Type as Setup import qualified SAWScript.Crucible.LLVM.CrucibleLLVM as CL import SAWScript.Crucible.LLVM.Setup.Value -import Verifier.SAW.Simulator.What4.ReturnTrip ( toSC, saw_ctx ) - -import Verifier.SAW.SharedTerm import Verifier.SAW.TypedTerm @@ -177,24 +168,6 @@ mutIso = isMut :: Lens' LLVMAllocSpec Bool isMut = allocSpecMut . mutIso --------------------------------------------------------------------------------- --- ** Ghost state - -instance Crucible.IntrinsicClass Sym MS.GhostValue where - type Intrinsic Sym MS.GhostValue ctx = (Cryptol.Schema, Term) - muxIntrinsic sym _ _namerep _ctx prd (thnSch,thn) (elsSch,els) = - do when (thnSch /= elsSch) $ fail $ unlines $ - [ "Attempted to mux ghost variables of different types:" - , show (Cryptol.pp thnSch) - , show (Cryptol.pp elsSch) - ] - st <- sawCoreState sym - let sc = saw_ctx st - prd' <- toSC sym st prd - typ <- scTypeOf sc thn - res <- scIte sc typ prd' thn els - return (thnSch, res) - -------------------------------------------------------------------------------- -- ** CrucibleContext diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index f9b258952e..ab79d52c21 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -89,7 +89,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.Backend.Online as Crucible @@ -120,7 +119,6 @@ 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 @@ -1180,29 +1178,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 -> @@ -1283,7 +1258,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) @@ -1451,50 +1426,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 @@ -1510,36 +1441,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) - ] ------------------------------------------------------------------------ @@ -1658,7 +1563,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 @@ -2084,27 +1989,7 @@ executeSetupCondition opts sc cc spec = MS.SetupCond_Equal md val1 val2 -> executeEqual opts sc cc spec md val1 val2 MS.SetupCond_Pred md tm -> executePred sc cc md tm - MS.SetupCond_Ghost () md var val -> executeGhost sc md var val - ------------------------------------------------------------------------- - --- TODO(lb): make this language independent! -executeGhost :: - SharedContext -> - MS.ConditionMetadata -> - MS.GhostGlobal -> - TypedTerm -> - OverrideMatcher (LLVM arch) RW () -executeGhost sc _md var (TypedTerm (TypedTermSchema sch) tm) = - do s <- OM (use termSub) - tm' <- liftIO (scInstantiateExt sc s tm) - writeGlobal var (sch,tm') -executeGhost _sc _md _var (TypedTerm tp _) = - fail $ unlines - [ "executeGhost: improper value type" - , "expected Cryptol schema type, but got" - , show (MS.ppTypedTermType tp) - ] + MS.SetupCond_Ghost md var val -> executeGhost sc md var val ------------------------------------------------------------------------ diff --git a/src/SAWScript/Crucible/LLVM/Setup/Value.hs b/src/SAWScript/Crucible/LLVM/Setup/Value.hs index de4b0ff143..5102861f10 100644 --- a/src/SAWScript/Crucible/LLVM/Setup/Value.hs +++ b/src/SAWScript/Crucible/LLVM/Setup/Value.hs @@ -129,8 +129,6 @@ type instance Setup.XSetupUnion (LLVM _) = () type instance Setup.XSetupGlobal (LLVM _) = () type instance Setup.XSetupGlobalInitializer (LLVM _) = () -type instance Setup.XGhostState (LLVM _) = () - type instance Setup.TypeName (LLVM arch) = CL.Ident type instance Setup.ExtType (LLVM arch) = CL.MemType diff --git a/src/SAWScript/Crucible/MIR/Builtins.hs b/src/SAWScript/Crucible/MIR/Builtins.hs index 3c4f0774f6..f87195709d 100644 --- a/src/SAWScript/Crucible/MIR/Builtins.hs +++ b/src/SAWScript/Crucible/MIR/Builtins.hs @@ -16,6 +16,7 @@ module SAWScript.Crucible.MIR.Builtins , mir_execute_func , mir_find_adt , mir_fresh_var + , mir_ghost_value , mir_load_module , mir_points_to , mir_postcond @@ -73,7 +74,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) @@ -108,6 +108,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 @@ -214,6 +215,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 @@ -585,32 +593,43 @@ setupPrePointsTos mspec cc env pts mem0 = foldM doPointsTo mem0 pts ] Mir.writeMirRefIO bak globals Mir.mirIntrinsicTypes referenceVal referentVal --- | 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 -> @@ -788,7 +807,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 @@ -809,7 +829,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 a6f9931a16..0e3c2996a3 100644 --- a/src/SAWScript/Crucible/MIR/Override.hs +++ b/src/SAWScript/Crucible/MIR/Override.hs @@ -49,10 +49,8 @@ import qualified What4.Expr as W4 import qualified What4.Interface 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 @@ -100,22 +98,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 - decodeMIRVal :: Mir.Collection -> Mir.Ty -> Crucible.AnyValue Sym -> Maybe MIRVal decodeMIRVal col ty (Crucible.AnyValue repr rv) | Some shp <- tyToShape col ty @@ -292,9 +274,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 :: @@ -315,7 +299,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 @@ -480,33 +464,6 @@ matchPointsTos opts sc cc spec prepost = go False [] MS.SetupUnion empty _ _ -> absurd empty MS.SetupNull empty -> absurd empty -matchTerm :: - SharedContext {- ^ context for constructing SAW terms -} -> - MIRCrucibleContext {- ^ context for interacting with Crucible -} -> - MS.ConditionMetadata -> - MS.PrePost -> - Term {- ^ exported concrete term -} -> - Term {- ^ expected specification term -} -> - OverrideMatcher MIR md () - -matchTerm _ _ _ _ real expect | real == expect = return () -matchTerm sc cc md prepost real expect = - do let loc = MS.conditionLoc md - free <- OM (use osFree) - case unwrapTermF expect of - FTermF (ExtCns ec) - | Set.member (ecVarIndex ec) free -> - do assignTerm sc cc md prepost (ecVarIndex ec) real - - _ -> - do t <- liftIO $ scEq sc real expect - let msg = unlines $ - [ "Literal equality " ++ MS.stateCond prepost --- , "Expected term: " ++ prettyTerm expect --- , "Actual term: " ++ prettyTerm real - ] - addTermEq t md $ Crucible.SimError loc $ Crucible.AssertFailureSimError msg "" - -- | Try to translate the spec\'s 'SetupValue' into a 'MIRVal', pretty-print -- the 'MIRVal'. mkStructuralMismatch :: diff --git a/src/SAWScript/Crucible/MIR/Setup/Value.hs b/src/SAWScript/Crucible/MIR/Setup/Value.hs index 5c592abefb..a8d155f8c3 100644 --- a/src/SAWScript/Crucible/MIR/Setup/Value.hs +++ b/src/SAWScript/Crucible/MIR/Setup/Value.hs @@ -76,8 +76,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 db255e9eeb..0a9c8c39d1 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -3623,9 +3623,23 @@ primitives = Map.fromList , prim "crucible_ghost_value" "Ghost -> Term -> LLVMSetup ()" (pureVal llvm_ghost_value) - Current + Deprecated [ "Legacy alternative name for `llvm_ghost_value`."] + , prim "jvm_ghost_value" + "Ghost -> Term -> JVMSetup ()" + (pureVal jvm_ghost_value) + Current + [ "Specifies the value of a ghost variable. This can be used" + , "in the pre- and post- conditions of a setup block."] + + , prim "mir_ghost_value" + "Ghost -> Term -> MIRSetup ()" + (pureVal mir_ghost_value) + Current + [ "Specifies the value of a ghost variable. This can be used" + , "in the pre- and post- conditions of a setup block."] + , prim "llvm_spec_solvers" "LLVMSpec -> [String]" (\_ _ -> toValue llvm_spec_solvers) Current