From 4c415e13544fe65ac16e4518b3c52a553aaf6043 Mon Sep 17 00:00:00 2001 From: Andrei Stefanescu Date: Fri, 11 Nov 2022 23:02:21 +0000 Subject: [PATCH 1/4] Find SMT array write of a fixed size. --- deps/crucible | 2 +- src/SAWScript/Crucible/LLVM/Override.hs | 25 ++++++++++++++++++++++++- 2 files changed, 25 insertions(+), 2 deletions(-) diff --git a/deps/crucible b/deps/crucible index 0515e64ab5..98428da33b 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 0515e64ab5c39036c6577e06bbe4272d39de5656 +Subproject commit 98428da33b1840e7adb37a74470d9a9246c3c03b diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index d193f73864..67104ba974 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -124,6 +124,7 @@ import Verifier.SAW.SharedTerm import Verifier.SAW.TypedAST import Verifier.SAW.Recognizer import Verifier.SAW.TypedTerm +import Verifier.SAW.Simulator.TermModel import Verifier.SAW.Simulator.What4.ReturnTrip (SAWCoreState(..), toSC, bindSAWTerm) import SAWScript.Crucible.Common @@ -1684,7 +1685,29 @@ matchPointsToValue opts sc cc spec prepost md maybe_cond ptr val = return Nothing - _ -> return $ Just errMsg + _ -> + do sub <- OM (use termSub) + modmap <- liftIO $ scGetModuleMap sc + instantiated_expected_sz_tm <- liftIO $ scInstantiateExt sc sub $ ttTerm expected_sz_tm + normalized_expected_sz_tm <- liftIO $ + normalizeSharedTerm sc modmap mempty mempty mempty instantiated_expected_sz_tm + case asUnsignedConcreteBv normalized_expected_sz_tm of + Just sz_nat -> + do sz_bv <- liftIO $ + W4.bvLit sym Crucible.PtrWidth $ BV.mkBV Crucible.PtrWidth $ fromIntegral sz_nat + maybe_matching_array <- liftIO $ + Crucible.asMemMatchingArrayStore sym Crucible.PtrWidth ptr sz_bv (Crucible.memImplHeap mem) + case maybe_matching_array of + Just (ok, arr) -> + do addAssert ok md $ Crucible.SimError loc $ Crucible.GenericSimError $ show errMsg + st <- liftIO (sawCoreState sym) + arr_tm <- liftIO $ toSC sym st arr + instantiateExtMatchTerm sc cc md prepost arr_tm $ ttTerm expected_arr_tm + return Nothing + + _ -> return $ Just errMsg + + _ -> return $ Just errMsg -- | Like 'matchPointsToValue', but specifically geared towards the needs -- of fields within bitfields. In particular, this performs all of the From b9651e35dc743b3a9fe1edfb071431702961c57f Mon Sep 17 00:00:00 2001 From: Andrei Stefanescu Date: Wed, 22 Feb 2023 14:52:19 +0000 Subject: [PATCH 2/4] Load SMT array with concrete size. --- src/SAWScript/Crucible/LLVM/Override.hs | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index 67104ba974..d8e8e7fc04 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -1697,17 +1697,22 @@ matchPointsToValue opts sc cc spec prepost md maybe_cond ptr val = W4.bvLit sym Crucible.PtrWidth $ BV.mkBV Crucible.PtrWidth $ fromIntegral sz_nat maybe_matching_array <- liftIO $ Crucible.asMemMatchingArrayStore sym Crucible.PtrWidth ptr sz_bv (Crucible.memImplHeap mem) - case maybe_matching_array of - Just (ok, arr) -> + res <- case maybe_matching_array of + Just (ok, arr) -> return $ Right (ok, arr) + Nothing -> liftIO $ Crucible.loadArrayConcreteSizeRaw sym mem ptr sz_nat alignment + + case res of + Right (ok, arr) -> do addAssert ok md $ Crucible.SimError loc $ Crucible.GenericSimError $ show errMsg st <- liftIO (sawCoreState sym) arr_tm <- liftIO $ toSC sym st arr instantiateExtMatchTerm sc cc md prepost arr_tm $ ttTerm expected_arr_tm return Nothing - _ -> return $ Just errMsg + Left{} -> return $ Just errMsg + + Nothing -> return $ Just errMsg - _ -> return $ Just errMsg -- | Like 'matchPointsToValue', but specifically geared towards the needs -- of fields within bitfields. In particular, this performs all of the From 94a7226ac41f4fa70e3884d19c9c3f6298ff8f19 Mon Sep 17 00:00:00 2001 From: Andrei Stefanescu Date: Wed, 22 Feb 2023 13:54:57 +0000 Subject: [PATCH 3/4] Add test. --- .../Makefile | 11 +++ .../test_smt_array_load_concrete_size/Mix.cry | 8 +++ .../test_smt_array_load_concrete_size/test.bc | Bin 0 -> 3452 bytes .../test_smt_array_load_concrete_size/test.c | 13 ++++ .../test.saw | 66 ++++++++++++++++++ .../test_smt_array_load_concrete_size/test.sh | 6 ++ 6 files changed, 104 insertions(+) create mode 100644 intTests/test_smt_array_load_concrete_size/Makefile create mode 100644 intTests/test_smt_array_load_concrete_size/Mix.cry create mode 100644 intTests/test_smt_array_load_concrete_size/test.bc create mode 100644 intTests/test_smt_array_load_concrete_size/test.c create mode 100644 intTests/test_smt_array_load_concrete_size/test.saw create mode 100755 intTests/test_smt_array_load_concrete_size/test.sh diff --git a/intTests/test_smt_array_load_concrete_size/Makefile b/intTests/test_smt_array_load_concrete_size/Makefile new file mode 100644 index 0000000000..dffb75bb76 --- /dev/null +++ b/intTests/test_smt_array_load_concrete_size/Makefile @@ -0,0 +1,11 @@ +CC = clang +CFLAGS = -g -emit-llvm -frecord-command-line -O1 + +all: test.bc + +test.bc: test.c + $(CC) $(CFLAGS) -c $< -o $@ + +.PHONY: clean +clean: + rm -f test.bc diff --git a/intTests/test_smt_array_load_concrete_size/Mix.cry b/intTests/test_smt_array_load_concrete_size/Mix.cry new file mode 100644 index 0000000000..2b51da1e58 --- /dev/null +++ b/intTests/test_smt_array_load_concrete_size/Mix.cry @@ -0,0 +1,8 @@ +module Mix where + +import Array + +type ByteArray = Array[64][8] + +mix : {l} (width l <= 64) => ByteArray -> [64] -> [l][8] -> ByteArray +mix block n data = arrayCopy block n (arrayRangeUpdate (arrayConstant 0) 0 data) 0 `(l) diff --git a/intTests/test_smt_array_load_concrete_size/test.bc b/intTests/test_smt_array_load_concrete_size/test.bc new file mode 100644 index 0000000000000000000000000000000000000000..6e209292979a6f91f64ad330f4305d67ab11afeb GIT binary patch literal 3452 zcma)94NP0t6~2#W{G4FymxQ)wp;OW7GqzdDGg8{rbe4$A_m#`kI>`@v1p07U>)DFdIBlvj%T!3~*xD zKnW}rmWjg#u~865+NhDV$S0|+_U4rKI>ErfHK%R?=~gE-GkWbB=*eo9CbiR14GPMr z;grau#4w!llAr-|yyS6%IG7ekl49c(F~m?2D}@wjT6=S{^2U@l58AMX$_2eRNKL_S4jHPc|~q^5LyQLkD2U&m8o$V`nGDBeqc-#~>&#juwQ z3Sy&I45XNQJ*4osSRXiOw2Mj#+5Dk2jHJ0T#Tgo-?LhZZ9& z6$H)RSh$UXE07Y6L3nj@lbUr1ETOwiWU1y%tT97Ag=FAG*evpCv5^&d85Oxeg$-gD zy~}Af31xw+%oDrUY&uvhOlmiymG5#o@DxZ0_;s5C7O?FuV%8^hix74Wf~FJTc5pD< zCJv%RBp`-mU=Qerpv8va3hNgUdmU?A;B+^quxEuNIaVyzgu1W%L=r5LFHeb{fty zva!k&dn7i%-!p(i3CufAT2=e$Lr%?(GWS^0fOhPEDN9=Jm0Qv=0NEg51rT$AddV9L z2E<5#+j?tWdM8c6xXDl>h=MTlX)4H2{Yc3NsKMeIGfNu)QydjaQ^QuOKdFEblk?Iw zfr57)WT?@3>0N<}(A040U{U%Tn&Jg&r(W)Bk01QkbaJaohKdP}lU^nes&7@Q%OnC2 zrN$!rfw|`e1TNigQfp7l+VKj3gc?X%DR51?6s_LYo*dt@|LGZteT+B6_ZVW^(Iq(a zV~{t<1kJT&O>Y&^lCYcOx$)K_qJpVG`5IE*p%otqiUxVBZW@D7)613@x5akl$(C7r z%Q)GR9~}<`sN(>nHZc&OA^~!ER17ep8j^n_saR%}epb1%sn~QV8t7~Ii3@t|v{Tp1 zp0ZqxS?29cm&xXSY@mkkm4n(5LF@+Dt03>h za4K4JcT;h9N%7CDVuK}nW+ydJ0rJIh(W$wv*IbKguREphChbkL_NG*Eypl6d*v$#j zGLfr;OFtX4yhBoE% z2JPY$&Z!%a>`~p~l4f;Tdz;YpsyfUW`%~v)mb_!{eMdNPWRx0Bb+mt!RN@HeUeH~4 zYS#6*cD+pCl9ktMH=WXFPsGgmoF!v#fq;BA-MnhIB!J9~|8XmLDvp3XkULN}Qqisz zTCtH;+;S*BWUHrc*mSGQj}?}+H^G25wIvg4xg6US&zZ;VP5E5&m8quL9QfFrZ@WAQ zrH`Wqi*-Z&*BQkIr@XTSa8}-8mA4q>#}0*`R;;iJAU|A^{%uLI>QLNctKZvj;u2R_ zeryA(t6qBzO0-_PuHW6uyk@y-Z@EG?O~jh=omb)Y!C5FNkv4H8Kp_-n5PA_X#_QS` zdqS?>!kgNd>gf2HGjAVC(*}2Qy{Yxpr2eO)%qPUm;}f>($A5=Ho?xifRp%Y(_tZK4 zZrUww&4#h_qA&P%X zaQ2RhfIN)d&cL~x`7&WSA8VO_&lmLe{TfB(o6pBA=O8J`mUOHc5;U2^CC|wqG!OF* zi4B*tVkwlA8>~-)ogc6Wodn*Vr)QHLN0X;uiE=b0?%Z4XI?Hp14qN4te%~lyrTA<< zzpHP^?Wr3zH+DB3#1AqwYCPs2f;R*p1w(GwXdHsUU+cw_x%>Y)7YYYF!CG&3_x&S7 z{-E!e-{WR5W-zb8)Ez2G@#>)%B>x2_46GuU>Pi3wn3qfjs%G?hPbfAO|Cj6@H#qwlB+Pviemk5(ZBNr0ykpfJNCWhs-fkAn_D~xUN0tqH6PDEkc>e zY^-@c*0K~Eiq_lcx^NL5k+>jf%e+2NqpdRW3%oXx7 zS=`piO01A5&<2?j-=v`T#L+bV{3$jMocao^wv!Va&NsaK0CfD_&<-8*I-%o+XRJF7 z9XCinv;(>wI^JKz0L*FV584ABrXQ^F3{m(T?JezeX_`pKn z1Do;x9kBTgOhb<2np@lN>30RfwE@;=E)BlMgGGV6=UDBqvv0^#N~`+?AmI9<29zo? HRtD`quJDB( literal 0 HcmV?d00001 diff --git a/intTests/test_smt_array_load_concrete_size/test.c b/intTests/test_smt_array_load_concrete_size/test.c new file mode 100644 index 0000000000..14e059ae58 --- /dev/null +++ b/intTests/test_smt_array_load_concrete_size/test.c @@ -0,0 +1,13 @@ +#include +#include + +int mix(uint8_t block[128], uint32_t n, uint8_t *data, size_t len) { + size_t left = 128 - n; + + if (len < left) { + memcpy(block + n, data, len); + } else { + memcpy(block + n, data, left); + } + return 1; +} diff --git a/intTests/test_smt_array_load_concrete_size/test.saw b/intTests/test_smt_array_load_concrete_size/test.saw new file mode 100644 index 0000000000..1cf9dc6343 --- /dev/null +++ b/intTests/test_smt_array_load_concrete_size/test.saw @@ -0,0 +1,66 @@ +enable_experimental; + +import "Mix.cry"; +let arrayRangeEq = parse_core "arrayRangeEq 64 (Vec 8 Bool)"; + +m <- llvm_load_module "test.bc"; + +let i8 = llvm_int 8; +let i32 = llvm_int 32; + +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 mix_spec len res_block_len range_eq_len = do { + block <- llvm_fresh_cryptol_var "block" {| ByteArray |}; + block_ptr <- llvm_symbolic_alloc false 1 {{ 128:[64] }}; + llvm_points_to_array_prefix block_ptr block {{ 128:[64] }}; + + (data, data_ptr) <- ptr_to_fresh_readonly "data" (llvm_array len i8); + + n <- llvm_fresh_var "n" i32; + llvm_precond({{ n < 128 }}); + + llvm_execute_func [block_ptr, (llvm_term n), data_ptr, (llvm_term {{ `len : [64] }})]; + + let res = {{ mix block (0 # n) data }}; + res_block <- llvm_fresh_cryptol_var "res_block" {| ByteArray |}; + llvm_points_to_array_prefix block_ptr res_block {{ `res_block_len:[64] }}; + llvm_postcond {{ arrayRangeEq res_block 0 res 0 `range_eq_len }}; + + llvm_return (llvm_term {{ 1 : [32]}}); +}; + +llvm_verify m "mix" + [] + true + (mix_spec 1 128 128) + (do { + w4_unint_z3 []; + }); + +llvm_verify m "mix" + [] + true + (mix_spec 1 0 0) + (do { + w4_unint_z3 []; + }); + +fails (llvm_verify m "mix" + [] + true + (mix_spec 1 129 0) + (do { + w4_unint_z3 []; + })); + diff --git a/intTests/test_smt_array_load_concrete_size/test.sh b/intTests/test_smt_array_load_concrete_size/test.sh new file mode 100755 index 0000000000..d5f2c8ea02 --- /dev/null +++ b/intTests/test_smt_array_load_concrete_size/test.sh @@ -0,0 +1,6 @@ +#!/usr/bin/env bash + +set -e + +$SAW test.saw + From 45be7c40ab4bc7835b918be52ff070765ca104df Mon Sep 17 00:00:00 2001 From: Andrei Date: Wed, 28 Jun 2023 01:58:27 +0000 Subject: [PATCH 4/4] Add noSatisfyingWriteFreshConstant option. --- src/SAWScript/Crucible/LLVM/Builtins.hs | 1 + src/SAWScript/Crucible/LLVM/X86.hs | 1 + 2 files changed, 2 insertions(+) diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index 3ddc66f29b..652117dea8 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -1741,6 +1741,7 @@ setupLLVMCrucibleContext pathSat lm action = let ?memOpts = Crucible.defaultMemOptions { Crucible.laxPointerOrdering = laxPointerOrdering , Crucible.laxLoadsAndStores = laxLoadsAndStores + , Crucible.noSatisfyingWriteFreshConstant = False } let ?intrinsicsOpts = Crucible.defaultIntrinsicsOptions let ?recordLLVMAnnotation = \_ _ _ -> return () diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 8cadba3856..ed32b0dc4e 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -371,6 +371,7 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec let ?ptrWidth = knownNat @64 let ?memOpts = C.LLVM.defaultMemOptions { C.LLVM.laxLoadsAndStores = laxLoadsAndStores + , C.LLVM.noSatisfyingWriteFreshConstant = False } let ?recordLLVMAnnotation = \_ _ _ -> return () sc <- getSharedContext