From 0642f4cd0e210b2e197b0a59c4a6eeb11a45b33f Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 25 May 2021 11:04:04 -0400 Subject: [PATCH] Add enable_lax_pointer_ordering Fixes #1308. --- CHANGES.md | 4 +++ intTests/test1308/Makefile | 11 ++++++++ intTests/test1308/test.bc | Bin 0 -> 6368 bytes intTests/test1308/test.c | 10 ++++++++ intTests/test1308/test.saw | 29 ++++++++++++++++++++++ intTests/test1308/test.sh | 3 +++ saw-remote-api/docs/SAW.rst | 2 +- saw-remote-api/docs/old-Saw.rst | 1 + saw-remote-api/src/SAWServer.hs | 1 + saw-remote-api/src/SAWServer/SetOption.hs | 5 ++++ src/SAWScript/Crucible/LLVM/Builtins.hs | 6 ++++- src/SAWScript/Interpreter.hs | 11 ++++++++ src/SAWScript/Value.hs | 1 + 13 files changed, 82 insertions(+), 2 deletions(-) create mode 100644 intTests/test1308/Makefile create mode 100644 intTests/test1308/test.bc create mode 100644 intTests/test1308/test.c create mode 100644 intTests/test1308/test.saw create mode 100644 intTests/test1308/test.sh diff --git a/CHANGES.md b/CHANGES.md index 16cd1ea2e6..dc66312aec 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -20,6 +20,10 @@ Several improvements have been made to JVM verification: "current" status, so that `enable_experimental` is no longer necessary for JVM verification. +A new `enable_lax_pointer_ordering` function exists, which relaxes the +restrictions that Crucible imposes on comparisons between pointers from +different allocation blocks. + # Version 0.8 ## New Features diff --git a/intTests/test1308/Makefile b/intTests/test1308/Makefile new file mode 100644 index 0000000000..06a530f11d --- /dev/null +++ b/intTests/test1308/Makefile @@ -0,0 +1,11 @@ +CC = clang +CFLAGS = -g -emit-llvm -frecord-command-line -O2 + +all: test.bc + +test.bc: test.c + $(CC) $(CFLAGS) -c $< -o $@ + +.PHONY: clean +clean: + rm -f test.bc diff --git a/intTests/test1308/test.bc b/intTests/test1308/test.bc new file mode 100644 index 0000000000000000000000000000000000000000..5359a4d625c6f7c8de9ca23fbb716454a1d2457f GIT binary patch literal 6368 zcma)A4^&%Kn!k@1@*WUgLZLJ)N%~SM#~?3|b-$a0 zR(F82FXz7d?)QE7-tYI_-~H};snmyOwr3%fj1X!NaT_1n|8~p6e;Ii+t(LDLK&BKS z^cg7Al9VV3+SyPjXWnt$gy2D;L{oZ#aEtCqrgId6XB&9QuB6HnX_an?CaZ*&?n%{D zdaJD$m3dWbJVO%QiKM0p`dk*P-|c1JB{Y?8=_b`CU*VC^lgHVM6EN;E79k1LnhkUc z+cYT1+%W8h+jV!)m$jzGJCx>j*GRV61pzIWWT21HuQ>V2>c@}2pTUpHbX+nw#G(=C zj%uX{{RHaVOZm6Ifs0rq5ra}_vOzYZQ_Kftmz;{Ia{aVcF%wi=b;>R~Wz)Ru%BbQB zJO|TnC>8Tg#dKIU8%&>8$`%MYveQ(z-(y3xt=iK^Q=LYS%}n;w9*5CWEcIB8pryjH zh*N$eC_@q1yiztDluaYWj8cBpskp3Dpq^f;M@8|_(eLRqlf6EVP3m#Lm}b(>d%9`L zh9;G=s7Y~|V5gy1Fg+TSeE^bR`mLD5;Q90{_7MA1g6N)JPjNNX!{O0jgkrPD8lW6^ z2e~>YpVrE62IYWaK`FcFlwUR}?gGKxtsbj&weCj6l{wkfpll+T{#8&mKL_a2Cke%L zKpt@_rU(vzd-?#B)zbsf@Oi8})eA0_{IxSToQjA^_Hi(MR;QSOfS6n{^wk`H*SK95~R^_yLtyr&;665?Bd^jkcG1{4vU;)9@U0o({ev=ujX zFqDGdE~Soy$>Ms_9`^M4sN#B8x0yO(bZv)Ft8lXq;_Sl)N5Zah zLw^R|JqY~6dnMDWm3mWjL}os?SAILWJm4zkJ)LH<8=`cEI%0O&t)BjW+7eY2TDkHlBJ&OlPdo9v#ZcA+}XYKlam>F9+poI7AY#?`Uv&6p3CFwjjj9 zGv10klJd%bxh~blv>-mt|}sT$Cz zh=B~;;T*){MW~BtUUqR#){;f+^y*98V?&iZ)z?ee{hgv4Nc@?E`HE+XM3sujs2o;f|HR*!ycq|@R)UYBde(H z+sQC&5AQihdpf1D4eNJq`FxT2e3toBn7PG~4HK{(f-)c>+^?EsmlOL-__0r4I-xK1 z$L<%#N>1uaykz;wu>zR%>w)r*$nwyb=pBp4TJN!0T@EwVYxFoE4+K0pA3P@h9Era) zF!Mgh{LGPeK)tCC+G#k9YoltCuBI*YgAO+wKktt|=Z%YNi4pEPVt05N(X$@Kbb zYrgV{aRd}k#WtE!J~Jx+K7sSzq*A_U64nj6N+!q3L;9T%kgp>Z^ZIfxG{=U1{ftoT0+OuK}+&N0yZUGJawR!jb3L!_c-LbW?z}(T+ zTwt>|b~qdbRUM68ZO!ctdqK6S@vx=+5Y+a=&8@8kc2keq-e|K}9R-$lM;&yv7vKR3 zi@1`;R#W>Sw!7J8w{*0#h1^#7ske1CbhSIW3fY=nj}&y-Z3V5ChJx1C?lyHH7kiHN zDu`Rdn2oJnP0a;%M^jUC%T}}9(%*d0(b@sycD36rhuWK)SeUn}$7E|^_r+(bYHsK{ z#6H;G(y=7zX*8Q`2XWuOnz6ysUJ&zw^on(zUOM-WwF9a=+=GQ8I-G)TDCG;Wy_3D|x{>+40k))g9&b$X?+wgX z*y9fYH-;zv4G&ECYRhU4!y~GZu}=jAI*H`b;rf1y z^ifVt3K4;RnTAo#sa;7Md~iNwQn`!s(9N$$N!_F zqtDuG-)cU1aH&tDslkHj+0oW+v359M&#;($k6GHRt<9{yK)-o2TUV*m)c{$mI@(N@ zc1*XetsNcKtrmNCbEBif20U#7JedOa<;Mk`oP2E4r~U}?4;eTlLbVcsG6lhlXUkeb zR`U+`Iz4YJn=lT-Nf)X-LzdMmqlEmdAv}krZn%B3SR=jDgNXH*jrGVBhP|T%&q}2x1GXFc1Kh;_JftI#6`^#uNYo;F zrjaL+nQbz0CbUhWDfDybXs+N9QNDdj(%r)bsfcDi=#EW|G6`|Bq z5WIB~uF=4LC_`FGDZYvI&&2eHM5$FTlSo?34mc5DWCj$`QJ9E>iE}gKjz}= z?2xo8v%&o)SlYYpTL}UHuYrI#B>h3GABNNjdYI`X%w!@rNNJ$a0(*Nv4Up)f*cv9* zIN(Ceud(~T{f_%-GzM&DP{3tm{t4^HV|tkBG=x@^D;d=yyvB2~BPN*0|D83KyB)L# z+CUi6rI(VuR_rYs%JTh zuD^!eUzwsCZ({vQ6s?YqEkn_b$Hn0O$`sx7A=a-%(S4Ei%TUyO%(p5<{l`wMLQ!pI ze&I3{eR%ldsuX>61nXC#=ufQ2mZ9kPH{`EM(aWc?ekF?f2OnOBqI`BKc7H{R&Svk# z`jsfEKGLuZMK93Lu1eA0sIYz|iuRham!aswt|wNdD8Ku_Dio#Df3+M%w_U^TuT0VH zH?e*tiar$`UxuP*kFQ&mqHlbN^(#@dWvpNsik^9HYE_CxpS!XmMUAJlpgYMj2p@pX zRAajEZDO~GL4wgRCw_%Zn+7$4|C$1>sobSwAq&M$gtrS5G1n5lZ=Ze(?2sox3w#35 z0-VO+I6#VD5@eBZoDkaXoc<%8N6wD7!#MEH2??Kl0q1E*YABVDrQ;s8Y10`$m zfsypID6u341V{1(d{_onukWo8%CmeB!myf@gvipuJU>p>N zEWJbUX95oUap$`Pn$*yGm{3MS9>*_s=oFL#0>qrpGWb$Gn_BN1X4gLdc+^&>+ax>7 zk3>!-rR|+F464Voha=}w4?JH`J?L8N+ZWyI)y3^Ev(U!2d zT}eG*8B`B$0?C=ksncsgvd{EhM%t2N1KA*{GwtcblGj6@LV zXipr=Nxd(X+RXkk^fN6;n8%}g&w}KgO|7Lf$|X1xAi?l&f&|0)uRCyVg9O9*CIRR8 z9XRH*<@W8>NNSL8@p zh)@CWEA1$neIeN`LBqZONl1gMvqm}49)=no?(tInS6rl6i>Y%z({a#b#HqnHignV6**rv@I%LN57JsA`vBZW*rR~Uq8D=B0SA88*8&)?Nq2v z +#include + +const size_t LEN = 42; + +void zip_with_add(uint64_t c[LEN], const uint64_t a[LEN], const uint64_t b[LEN]) { + for (size_t i = 0; i < LEN; i++) { + c[i] = a[i] + b[i]; + } +} diff --git a/intTests/test1308/test.saw b/intTests/test1308/test.saw new file mode 100644 index 0000000000..63825d11e8 --- /dev/null +++ b/intTests/test1308/test.saw @@ -0,0 +1,29 @@ +enable_lax_pointer_ordering; + +let alloc_init_readonly ty v = do { + p <- llvm_alloc_readonly ty; + llvm_points_to p v; + return p; +}; + +let ptr_to_fresh_readonly n ty = do { + x <- llvm_fresh_var n ty; + p <- alloc_init_readonly ty (llvm_term x); + return (x, p); +}; + +let LEN = 42; + +let zip_with_add_spec = do { + let array_ty = llvm_array LEN (llvm_int 64); + c_ptr <- llvm_alloc array_ty; + (a, a_ptr) <- ptr_to_fresh_readonly "a" array_ty; + (b, b_ptr) <- ptr_to_fresh_readonly "b" array_ty; + + llvm_execute_func [c_ptr, a_ptr, b_ptr]; + + llvm_points_to c_ptr (llvm_term {{ zipWith`{LEN} (+) a b }}); +}; + +mod <- llvm_load_module "test.bc"; +llvm_verify mod "zip_with_add" [] false zip_with_add_spec z3; diff --git a/intTests/test1308/test.sh b/intTests/test1308/test.sh new file mode 100644 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test1308/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw diff --git a/saw-remote-api/docs/SAW.rst b/saw-remote-api/docs/SAW.rst index 6c22b4ec1b..9501fcef43 100644 --- a/saw-remote-api/docs/SAW.rst +++ b/saw-remote-api/docs/SAW.rst @@ -402,7 +402,7 @@ Parameter fields ``option`` - The option to set and its accompanying value (i.e., true or false); one of the following:``lax arithmetic``, ``SMT array memory model``, or ``What4 hash consing`` + The option to set and its accompanying value (i.e., true or false); one of the following:``lax arithmetic``, ``lax pointer ordering``, ``SMT array memory model``, or ``What4 hash consing`` diff --git a/saw-remote-api/docs/old-Saw.rst b/saw-remote-api/docs/old-Saw.rst index f42adb5fe6..c055fc3b76 100644 --- a/saw-remote-api/docs/old-Saw.rst +++ b/saw-remote-api/docs/old-Saw.rst @@ -165,6 +165,7 @@ Setting Options - ``option``: The name of the option to set. This is one of: * ``lax arithmetic`` + * ``lax pointer ordering`` * ``SMT array memory model`` * ``What4 hash consing`` diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs index 870f442562..47b75dfffd 100644 --- a/saw-remote-api/src/SAWServer.hs +++ b/saw-remote-api/src/SAWServer.hs @@ -218,6 +218,7 @@ initialState readFileFn = , rwProfilingFile = Nothing , rwCrucibleAssertThenAssume = False , rwLaxArith = False + , rwLaxPointerOrdering = False , rwWhat4HashConsing = False , rwWhat4HashConsingX86 = False , rwStackBaseAlign = defaultStackBaseAlign diff --git a/saw-remote-api/src/SAWServer/SetOption.hs b/saw-remote-api/src/SAWServer/SetOption.hs index 0d6b62a3b3..b57f0a61be 100644 --- a/saw-remote-api/src/SAWServer/SetOption.hs +++ b/saw-remote-api/src/SAWServer/SetOption.hs @@ -31,6 +31,8 @@ setOption opt = case opt of EnableLaxArithmetic enabled -> updateRW rw { rwLaxArith = enabled } + EnableLaxPointerOrdering enabled -> + updateRW rw { rwLaxPointerOrdering = enabled } EnableSMTArrayMemoryModel enabled -> undefined updateRW rw { rwSMTArrayMemoryModel = enabled } EnableWhat4HashConsing enabled -> undefined @@ -39,6 +41,7 @@ setOption opt = data SetOptionParams = EnableLaxArithmetic Bool + | EnableLaxPointerOrdering Bool | EnableSMTArrayMemoryModel Bool | EnableWhat4HashConsing Bool @@ -46,6 +49,7 @@ parseOption :: Object -> String -> Parser SetOptionParams parseOption o name = case name of "lax arithmetic" -> EnableLaxArithmetic <$> o .: "value" + "lax pointer ordering" -> EnableLaxPointerOrdering <$> o .: "value" "SMT array memory model" -> EnableSMTArrayMemoryModel <$> o .: "value" "What4 hash consing" -> EnableWhat4HashConsing <$> o .: "value" _ -> empty @@ -60,6 +64,7 @@ instance Doc.DescribedMethod SetOptionParams OK where [ ("option", Doc.Paragraph [Doc.Text "The option to set and its accompanying value (i.e., true or false); one of the following:" , Doc.Literal "lax arithmetic", Doc.Text ", " + , Doc.Literal "lax pointer ordering", Doc.Text ", " , Doc.Literal "SMT array memory model", Doc.Text ", or " , Doc.Literal "What4 hash consing" ]) diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index 576e8f003c..25a76c0196 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -1341,6 +1341,7 @@ setupLLVMCrucibleContext pathSat lm action = smt_array_memory_model_enabled <- gets rwSMTArrayMemoryModel crucible_assert_then_assume_enabled <- gets rwCrucibleAssertThenAssume what4HashConsing <- gets rwWhat4HashConsing + laxPointerOrdering <- gets rwLaxPointerOrdering Crucible.llvmPtrWidth ctx $ \wptr -> Crucible.withPtrWidth wptr $ do let ?lc = ctx^.Crucible.llvmTypeCtx @@ -1377,8 +1378,11 @@ setupLLVMCrucibleContext pathSat lm action = crucible_assert_then_assume_enabled let bindings = Crucible.fnBindingsFromList [] + let memOpts = Crucible.defaultMemOptions + { Crucible.laxPointerOrdering = laxPointerOrdering + } let simctx = Crucible.initSimContext sym intrinsics halloc stdout - bindings (Crucible.llvmExtensionImpl Crucible.defaultMemOptions) + bindings (Crucible.llvmExtensionImpl memOpts) Common.SAWCruciblePersonality mem <- Crucible.populateConstGlobals sym (Crucible.globalInitMap mtrans) =<< Crucible.initializeMemoryConstGlobals sym ctx llvm_mod diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index eff7fee17b..a59d362992 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -475,6 +475,7 @@ buildTopLevelEnv proxy opts = , rwCrucibleAssertThenAssume = False , rwProfilingFile = Nothing , rwLaxArith = False + , rwLaxPointerOrdering = False , rwWhat4HashConsing = False , rwWhat4HashConsingX86 = False , rwPreservedRegs = [] @@ -543,6 +544,11 @@ enable_lax_arithmetic = do rw <- getTopLevelRW putTopLevelRW rw { rwLaxArith = True } +enable_lax_pointer_ordering :: TopLevel () +enable_lax_pointer_ordering = do + rw <- getTopLevelRW + putTopLevelRW rw { rwLaxPointerOrdering = True } + enable_what4_hash_consing :: TopLevel () enable_what4_hash_consing = do rw <- getTopLevelRW @@ -764,6 +770,11 @@ primitives = Map.fromList Current [ "Enable lax rules for arithmetic overflow in Crucible." ] + , prim "enable_lax_pointer_ordering" "TopLevel ()" + (pureVal enable_lax_pointer_ordering) + Current + [ "Enable lax rules for pointer ordering comparisons in Crucible." ] + , prim "enable_what4_hash_consing" "TopLevel ()" (pureVal enable_what4_hash_consing) Current diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index 4a8e6f3d8b..7d30838782 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -409,6 +409,7 @@ data TopLevelRW = , rwCrucibleAssertThenAssume :: Bool , rwProfilingFile :: Maybe FilePath , rwLaxArith :: Bool + , rwLaxPointerOrdering :: Bool -- FIXME: These might be better split into "simulator hash-consing" and "tactic hash-consing" , rwWhat4HashConsing :: Bool