From 2e60608058fe61bd1365c9f66037cba4abccd03f Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Sun, 3 Dec 2023 17:29:51 -0500 Subject: [PATCH] Properly extend path condition for `llvm_conditional_points_to` This leverages the newly introduced `withConditionalPred` function (see the parent commit) to make `llvm_conditional_points_to cond ptr val` properly extend the path condition with `cond` before matching `val` against the value that `ptr` points to. Fixes #1945. --- intTests/test1945/Makefile | 11 ++++++++++ intTests/test1945/test.bc | Bin 0 -> 2760 bytes intTests/test1945/test.c | 3 +++ intTests/test1945/test.saw | 17 ++++++++++++++++ intTests/test1945/test.sh | 3 +++ src/SAWScript/Crucible/LLVM/Override.hs | 26 ++++++++++++++++++------ 6 files changed, 54 insertions(+), 6 deletions(-) create mode 100644 intTests/test1945/Makefile create mode 100644 intTests/test1945/test.bc create mode 100644 intTests/test1945/test.c create mode 100644 intTests/test1945/test.saw create mode 100755 intTests/test1945/test.sh diff --git a/intTests/test1945/Makefile b/intTests/test1945/Makefile new file mode 100644 index 0000000000..ebf9cc47cc --- /dev/null +++ b/intTests/test1945/Makefile @@ -0,0 +1,11 @@ +CC = clang +CFLAGS = -g -frecord-command-line -O0 + +all: test.bc + +test.bc: test.c + $(CC) $(CFLAGS) -c -emit-llvm $< -o $@ + +.PHONY: clean +clean: + rm -f test.bc diff --git a/intTests/test1945/test.bc b/intTests/test1945/test.bc new file mode 100644 index 0000000000000000000000000000000000000000..f30cc928b26f7b5ec2788b1760845c32a16205c3 GIT binary patch literal 2760 zcma)8eM}q46(3{AV}ec1Un-kbMk=Iwj)es5-*9djF&a)b^bgxqqv>br0M*?0A;**8nhvF#$zY2^s@6(Lko zq(#8cYtV6`@>)|?a#pG|*(OD!^5X|&6&lIU+^q6+QS)R;^Qh8PZk4INchJ;4-WFQa zR<<1CCzMT-Mc%CJ!*a^eI!=8oGBuB?PU=o3jhAOGT%#7VVD}1z5CPnDOjb;}Taosg zRntoCaUd1nkdNI+I-9*0s4DMBV})qCvQamIn$1e5?B>Zo*otThoIR&Ps2%nnZLNI% zH8fEO73;*5Toy_4AwM7Xi{o)V8p6XmJcJe!>Qxc7rd6+}OIOq6eJ#0~F3qROdkM`( zlV)vGvyvcpMQUV4vcWiCo5Djf9A{xWAMtYoGCbUfSZ~yIbm=bm?MRlba`(z?xID()7lXXim(g_)wCM=u334v?o&JQ>A&9KqH!k zCe8gcxtlJ{rOAba=8GmUrC}{9e0fe>+bNFB@k2>m+sO_1@nt7xndXOdf;cqIhm*pB z%X6F^$%b#@K^rarsEFjBrx|O#QbyMW*JK^ZjrunQNy^yI+~eiX7NxQN2dGb zkC5WAl6b}vW_hz_VO|Zn@zDng%ebRCaYNS8Fd=Tp#U}t#@5=B{8y^B}g~S7KK1A^q zxiTW3B(`WpkXCH(5qlkkS-Gg*0Gw&n3oeb1zGA<_*_R!*S#kXxu6|T(&+U~DIPtrF zTql4P*RcXtLQXuO!voI`fZ0Ko?~?KTDn1OkpH7^5vPV4GB>p)^QAh z+{s5(d^E*Z+2iJcDOIbHepybG#Py}I>!UaNkjRWEAQkilK;8$RlN`yEHa zZLw{Nv*kMPK=vWnVeqq!9}EEihbV-`0ApcI8|4_6R}_a$ZB%7q;@Y(bEh(kWTW>Tq zzn9ehGE09@Bt69@DrzPttIkA9qD&-O?J@ZKdKp7_$QA7FiFo>=QA10gC)UdZqY*=! z%X29Z>;@jW#PswSBCep<-4_QwsE>HUfl$;C2u9C?orpoOX0+8<7>|jejqW;=kM=NL zuhCUkQ|B`KT(vfn$yejE{=gjzMq`wx2R=v*FyTm`FGv|{s_AN4Z;TZtjn&4ML08yE z{cwM}g>lEask1>}-z&|a$L|VvMFPW2$5{u}&I~X;9cNGP4`PE+m%E4YgfnL3_#^4SF4f`(WyD7ad%y|03UcINUw--Xx_XL6rrGJyA^d3sj z^ai4OVIQ@BV3fXZf8_QcR4E&$M_75KOlBNm%RvH0I^GsJ${-=a!v>8)i0%+cn&})} zGiJ{0sg~uAXq#DH`V-PYnijuxbQ8*6I|>)F+n^`+Kg zEBX!GKU(mifZT4OUS6x&b`qa=Kp84_ zgkn^D-a$N@VH0>rSGXnOJRn@Ck;}Ym@;kjB) zli7V>iykNug4-40T>TBsejP3caYKr$hl?Va5su15A>;>sSkhDv&jWf3`mrI@~S-bupyV0Q#6RGxljkMKm@!8A(a*u_! z7-?^v*XH)nF1NYX>$7!ry)+pMMgrYI#!CsfjYBNI`!)9zU5s<0Mx^{j;dexJ9=)Mt z=Tk*WF{R=faHEuAk!&U_I%R4To6)Dj2_W_~;T#hkan2nnh%l>xL2co;3awJ8cjk%` z)q!HWd`q5VkE~G$Ip1-%D<|PGGM5#(lM6GVGMR*ShY%%`wvK!SuQc}rh~iH`zLQgx zi(^uhGE48W?~9ORQTUATX8%YsC#0m%`YD9OFftL!W25Mb@XQq&11pZh=#Y3yC*)ID z1HXKQoVNoPbe+(JCUC*-xFA3i;yDam4_&~>E2FRGK~-2UaG|}L7dSZnHLBXz0mKS( y0vGhMQ!s$`4)`YMz_*AX3-}Rgy4vgRuJ$r;6@;1nOXww#LZ1I&X}|7;ZRo!ROp4I} literal 0 HcmV?d00001 diff --git a/intTests/test1945/test.c b/intTests/test1945/test.c new file mode 100644 index 0000000000..32ff9ad7fa --- /dev/null +++ b/intTests/test1945/test.c @@ -0,0 +1,3 @@ +#include + +void test(uint8_t *x) {} diff --git a/intTests/test1945/test.saw b/intTests/test1945/test.saw new file mode 100644 index 0000000000..2475cf87d8 --- /dev/null +++ b/intTests/test1945/test.saw @@ -0,0 +1,17 @@ +// Test a use of `llvm_conditional_points_to` where the value that the pointer +// points to will fail to match against the right-hand side value unless the +// condition is properly incorporated into the path condition. This serves as +// a regression test for https://github.com/GaloisInc/saw-script/issues/1945. + +let test_spec = do { + p <- llvm_alloc (llvm_int 8); + x <- llvm_fresh_var "x" (llvm_int 8); + llvm_points_to p (llvm_term x); + + llvm_execute_func [p]; + + llvm_conditional_points_to {{ x == 1 }} p (llvm_term {{ 1 : [8] }}); +}; + +m <- llvm_load_module "test.bc"; +llvm_verify m "test" [] false test_spec z3; diff --git a/intTests/test1945/test.sh b/intTests/test1945/test.sh new file mode 100755 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test1945/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index 1a0d1ed882..8174385b8a 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -1410,14 +1410,28 @@ matchPointsToValue opts sc cc spec prepost md maybe_cond ptr val = let badLoadSummary = summarizeBadLoad cc memTy prepost ptr case res of Crucible.NoErr pred_ res_val -> do - pred_' <- case maybe_cond of - Just cond -> do - cond' <- instantiateExtResolveSAWPred sc cc (ttTerm cond) - liftIO $ W4.impliesPred sym cond' pred_ - Nothing -> return pred_ + -- If dealing with an `llvm_conditional_points_to` statement, + -- convert the condition to a `Pred`. If dealing with an + -- ordinary `llvm_points_to` statement, this condition will + -- simply be `True`. + cond' <- case maybe_cond of + Just cond -> + instantiateExtResolveSAWPred sc cc (ttTerm cond) + Nothing -> + pure $ W4.truePred sym + -- Next, construct an implication involving the condition and + -- assert it. + pred_' <- liftIO $ W4.impliesPred sym cond' pred_ addAssert pred_' md $ Crucible.SimError loc $ Crucible.AssertFailureSimError (show $ PP.vcat badLoadSummary) "" - pure Nothing <* matchArg opts sc cc spec prepost md res_val memTy val' + + -- Finally, match the value that the pointer points to against + -- the right-hand side value in the points_to statement. Make + -- sure to execute this match with an extended path condition + -- that takes the condition above into account. See also + -- Note [oeConditionalPred] in SAWScript.Crucible.Common.Override. + withConditionalPred cond' $ + pure Nothing <* matchArg opts sc cc spec prepost md res_val memTy val' _ -> do pure $ Just $ describeConcreteMemoryLoadFailure mem badLoadSummary ptr