From d63f36a5b6c60dd95ba5a806337b45727ea8fda0 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Thu, 9 Jun 2022 11:15:42 -0400 Subject: [PATCH] Fix #1684 by bringing in GaloisInc/crucible#998 Now that the `crucible-llvm` memory model can reason about struct padding with `lax-loads-and-stores` enabled, bumping the `crucible` submodule to bring in that change fixes #1684 as a consequence. I have also added a regression test. --- deps/crucible | 2 +- deps/macaw | 2 +- intTests/test1684/Makefile | 11 +++++++++++ intTests/test1684/test.bc | Bin 0 -> 2960 bytes intTests/test1684/test.c | 12 ++++++++++++ intTests/test1684/test.saw | 13 +++++++++++++ intTests/test1684/test.sh | 3 +++ 7 files changed, 41 insertions(+), 2 deletions(-) create mode 100644 intTests/test1684/Makefile create mode 100644 intTests/test1684/test.bc create mode 100644 intTests/test1684/test.c create mode 100644 intTests/test1684/test.saw create mode 100644 intTests/test1684/test.sh diff --git a/deps/crucible b/deps/crucible index 9946c88689..95677b97a0 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 9946c8868959350152a1b1c2fda4424e2b2a5a80 +Subproject commit 95677b97a0fc37a45733f900da162f1d917bc4c9 diff --git a/deps/macaw b/deps/macaw index 6a4f406c68..2791b1050f 160000 --- a/deps/macaw +++ b/deps/macaw @@ -1 +1 @@ -Subproject commit 6a4f406c680dc0438799ef5c95c94311e07e722a +Subproject commit 2791b1050f348922a27192d8a73ee538fed57629 diff --git a/intTests/test1684/Makefile b/intTests/test1684/Makefile new file mode 100644 index 0000000000..f7abdbe50b --- /dev/null +++ b/intTests/test1684/Makefile @@ -0,0 +1,11 @@ +CC = clang +CFLAGS = -g -emit-llvm -frecord-command-line -O0 + +all: test.bc + +test.bc: test.c + $(CC) $(CFLAGS) -c $< -o $@ + +.PHONY: clean +clean: + rm -f test.bc diff --git a/intTests/test1684/test.bc b/intTests/test1684/test.bc new file mode 100644 index 0000000000000000000000000000000000000000..7ba1a7072b3810a6c8dade31743407a3b870d05c GIT binary patch literal 2960 zcma(TZERE5^}amE_W{nc30X#F|3&^Wdgt{z?P$EL;CScLZCZ<;E&b15s zv1!`1?mhQ>+;h+8eeSSk@4i%lP$@#lp%S)z|A)WnKls&^*EaM@-4xLDDum9LAhe-G zj{u+-VB&b~>GoO00i~v)`3#j*Z7*f2bc%Nzl4gHN$C(WsNlinAnW=nreM851mw!fI z+gUD8Xxh(|xMrD46}=<3Vb<}klZs6> z7m~2tOHQUL%DcxWHYAhX8le`6iaCy|YjcBgYu(w2AWrm2cmc^B?l{U%qAcA&|^_K=Ep$;4tnTd7e3Yn zd$}nsM^iZFp+!k<^2q)S4xzlBo44z3QT(i4yQ=4A;@Vr2WnbvI+i~rJjhl{Zfr~^2 zkEZ1yV#Ji}_sF0#8kIwS95diCL}Vy_ev(_Y>lTo1Wsfa?d#e+Xd@cR7WCW~l=it2CK8pK zdgPb~M?G|m!2z2bOyevu6)r6vU(|Dp|Lb^K4w-SJ5S%x`g{VCC-(#}4tX+_FD|&8; z(t$~z{)aK+V;R|BDTg5-DLIlU#2*sjp#vAOD9Ax@4epwQ(5)dJqPnuo-HPiVuuGFV zbUaI2JhUZ4OQ0kri-tmK43HN&2B}PATiFe2>zY*dd6rwV>sI1rpJ%iS)Yf@h8HD;4 zpf(-2yaEDf>)H~F&g;PI>FXS1Fi+_gG7x;-93{wpn>=Q~(nVN_JrSXBkxh;;IQF~% z<}(Z_sPCcjHY$vsK%*RhS|k0j>4dF=C$NrK{It}PNi<1v01^r5yoir`5~5#@&D+-B zpHn`{U|83996>lH;9v%eJRU~spdSYcdqOMq0*ibg+#Ez(4g{a#oNDF zkB}=)2uhd@y0oflV|Qv|UEM1;6xK6AL$bz@C`XsT-=71&k&(EWWv;)1Y8|(lleviw z32Fq3>40h#sUKVQZ?MR5H>X+bPeou^x8t*sMuYd$&w&2fyuV_mWzy2MY9 zMrA)QSLHXd4^!;2p!Nysdu!}k58J4j(cXm?)N7~hx_;r5<&%VE&f0v1Zuun9lB6y9 zwTe+2KIXxDNZa8(5~&ow4UZb|=+jbA8l2ncv}G!%`khzyAC`mu zL_hN^H)t2H>!#avx1samy2T}^bnRa# zU4Lb-dCI!?T*8v?+4ij?Pp@W_F)Ly^cu3K5& zJin~H3kGymS*8-LR}$69oO#09oX@pfyWTvT10P%RT~`9|4%u)30(e-i`qK^ep-ug0 z3CdS}Ur^uY)&J;WeH!+jzykW^lJd_>>`D*&RIn~D6kfPBs$jYO&$2ju9o_Sj-RFU???H+ zQa23IpI%rjK_Ryo+T}EPMuy#{py(V4g-o3z&hW6?7ZOcfcITkiHvmu^bPo-gM0><2 zI)h$+$mI2fUWcQii72RVGVgW{*?j~2s5>ZnM|^y}unT_1-C;-A7Yf(&oe_JmpMRss z?Q}cB1N;GB|Hv~+#ObjI`$TWdZ3>G)(~#F;8X6iMHr5L!hu3E+>NXDWM)$BcWF#!! z*dKH|M}jV+b7Xkf?sFN3ygoN?d`;kuPQK_BZyYJ^98OfroDfd%s#>O`{sdnESpA&} z;Zq2frUe!l(`}_11_`u~lQcI~i90^oHa9i>x@mL6rN(zJecW48 zS4+@$ukQJ9@70FQjaR2Gf7JUHe*2K!d3jJgQ2V0ze)aZLxr1O;#|8&Ch_%jF#TTo$ zr_nE=?>EAA8`i@&G6GM|VSn1%3T-iEZJx`WSmkcO7qOkR`>I}BtkV~E-?Om~dZ7H( zE2Ih34|>=q#N^L3#Wx1$TP`Fl=b)+R)=Z)W8Z4C~|2^zHLT>`xq-bw}mkW7d*1R&C z>fM(*0$bG1E802!XvR#P7s#{L@37nL(Lx5iKIc%_PW42Pz zAs6J|7>32S%R@kYQ(x%+I2ao9yTx6ezP@K?!amVE;B&ip(K8YZjS+HVLtm&UKz7ds zfa7q$n|a8Lpf~=Y^q^}b zm}uuwH0VsIqM!{SU>#i5xDbXE6y)1fS!9;>m)TCXS6`%fOoXN`Qac43U6y`!sC1F5=vL9#D{7wcnZaisAO;1r98HM2RBc4&NEB^{UmAQwo zs6Qkh&3t9WgiDDsjmlE-Jqjsi$Xz6VKT>2!nhPVqBSfxkU^O*K^ns#CMaT^j+W{%3 z&l-qZ*l0hKhj}rvOW|*5`?tn?;3t<8Hj1Sv_Jb`39;}Zyme}lFa zX(VQZMj)XxJ7ELk$6%WpAlT+7ct2_MT`tGKE|(jgfS|khs(f3Me&@f-ve@tB%)bCJ CqrQLu literal 0 HcmV?d00001 diff --git a/intTests/test1684/test.c b/intTests/test1684/test.c new file mode 100644 index 0000000000..178b8d1682 --- /dev/null +++ b/intTests/test1684/test.c @@ -0,0 +1,12 @@ +#include + +struct a { + uint16_t x; + uint32_t y; +}; + +struct b { + struct a aa; +}; + +void f(struct b *bb) {} diff --git a/intTests/test1684/test.saw b/intTests/test1684/test.saw new file mode 100644 index 0000000000..c0fb026915 --- /dev/null +++ b/intTests/test1684/test.saw @@ -0,0 +1,13 @@ +enable_experimental; +enable_lax_loads_and_stores; + +let f_spec = do { + aa <- llvm_fresh_var "aa" (llvm_alias "struct.a"); + bb <- llvm_alloc (llvm_alias "struct.b"); + llvm_points_to (llvm_field bb "aa") (llvm_term aa); + + llvm_execute_func [bb]; +}; + +m <- llvm_load_module "test.bc"; +llvm_verify m "f" [] false f_spec (w4_unint_yices []); diff --git a/intTests/test1684/test.sh b/intTests/test1684/test.sh new file mode 100644 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test1684/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw