From f7ee74051d8d7c199f34b9fda8dc8b1f8c8bfca8 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Thu, 23 Jun 2022 14:48:56 -0700 Subject: [PATCH 1/2] bump crucible, llvm-pretty and llvm-pretty-bc-parser submodules --- deps/crucible | 2 +- deps/llvm-pretty | 2 +- deps/llvm-pretty-bc-parser | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/deps/crucible b/deps/crucible index e826210639..7523723451 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit e826210639edaf608687041136443f056c25e596 +Subproject commit 7523723451e22d1e843a40037b6131f07b6717ec diff --git a/deps/llvm-pretty b/deps/llvm-pretty index 34c95e77fb..64d43d9375 160000 --- a/deps/llvm-pretty +++ b/deps/llvm-pretty @@ -1 +1 @@ -Subproject commit 34c95e77fb9fdc584c23208f81f6072cb0e05c3f +Subproject commit 64d43d9375a819dc2a2df99fb98df24f049dcfaa diff --git a/deps/llvm-pretty-bc-parser b/deps/llvm-pretty-bc-parser index 1bad3e43c7..cbcf0954c2 160000 --- a/deps/llvm-pretty-bc-parser +++ b/deps/llvm-pretty-bc-parser @@ -1 +1 @@ -Subproject commit 1bad3e43c7444e363ef4c3d9f954bc04b01b1795 +Subproject commit cbcf0954c23da0018df3cc6aae77290ae2efe53b From 26f24781372b7ff6ea906a10c3ee87ee9c414fcd Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 24 Jun 2022 08:23:01 -0400 Subject: [PATCH 2/2] Fix #1691 by bringing in GaloisInc/crucible#1004 Now that the `crucible-llvm` memory model has a fix for GaloisInc/crucible#1004, bumping the `crucible` submodule to bring in that change fixes #1691 as a consequence. I have also added a regression test. --- deps/crucible | 2 +- intTests/test1691/Makefile | 11 +++++++++++ intTests/test1691/test.bc | Bin 0 -> 2820 bytes intTests/test1691/test.c | 8 ++++++++ intTests/test1691/test.saw | 17 +++++++++++++++++ intTests/test1691/test.sh | 3 +++ 6 files changed, 40 insertions(+), 1 deletion(-) create mode 100644 intTests/test1691/Makefile create mode 100644 intTests/test1691/test.bc create mode 100644 intTests/test1691/test.c create mode 100644 intTests/test1691/test.saw create mode 100755 intTests/test1691/test.sh diff --git a/deps/crucible b/deps/crucible index 7523723451..4bf2ab8696 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 7523723451e22d1e843a40037b6131f07b6717ec +Subproject commit 4bf2ab8696856e5190dc8a053281fe70c8fe9126 diff --git a/intTests/test1691/Makefile b/intTests/test1691/Makefile new file mode 100644 index 0000000000..f7abdbe50b --- /dev/null +++ b/intTests/test1691/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/test1691/test.bc b/intTests/test1691/test.bc new file mode 100644 index 0000000000000000000000000000000000000000..6757815299456bc26e2b5b62ca9db51a74d1a391 GIT binary patch literal 2820 zcmaJ@Z%kX)6~B*Xd>vw*9k3dcJik0c5?N^+KTJjd!v>fpq@^ol)s$+TVq*+u0b~0a zY@BSfvD@b)Ze+4Z^`?9&zjMxgZnaL{|BeQsVuVn)QrP|S8z1z(`mgJ+ZS4woP_U*~BJ}ej zgtivx5fJnObR4M~Z<&)Fm8;G57pRzWPqCtclb!1ht6wT=y|A@4rZ#Kp6xvrx%&qZu z&y2pRtxQU&TP_s!%qgyFc&n2>lZ1&Y8VWzkx=1&=v#DE92fE9!*Lr$rlepJhg`H6mTFy+Cyo6mr)L-J+%1Zq)9W_$>`X*=Yohdlp1l*%E!x=Whz@p< zsK6sB$%hnTQu4SY&>0L$eh&^A@F*fO6u&URZrHg+#H~%Rv!H5%U7Tc>Cv?*h_WAMn zNIMR==n;cN6uRhB2FaV20!gX%rsU^ws2L*$P3!JYl-`-rj$sbo;-IiI1iwk5(E6K$21*oyQ*n;iA1)uqa4Aa1HL72k15t52&uKu(u){0J}WF zq0^JJ#YJ1vbQqK*CDD)%jRE2!g&>qEY%86mc5Q}B?@h9sc5W?FdM~Y8q;@UXN&)Iy zz}h%)c?|^6uFYiz{h9->r>9tmV2Sw zMsdB`uDXo1;ZoF+>)idVBanMR987g}JV~ku0^CoyTXyz=UUz>=_cMyTAvwKn(=LDg zt!P~?Yspxf0FbYz8`rFsII!8ohb7>t6aaf5hoO*DkvCV>%)?1$y_5M;sG7Rd!mX`r zUs%!I2LswGESYH2_2|x6wk~0<&t)5LPSww4!N#{IAQ*S|{^Vu&ylTU%5>xZ@K;O-M?h(AXu5KX~Ei% zvo^%74dC^>^}A@4N2m{S%Ez_y*0{1_i_hH7S49%z;~%%B)rOwNYIE!Pr2f4i|95KE z5PawIQW5eyMgIYZ$u%_SH2Flwkl$}=8*&T}I^BNJ)NXg2?05G86;C<`227$oU=$s` zevjYO@AkhAM@17+P+ePJ?HI7T`}h&3PwXFZ^VPxu_!$olcMrS$!_|CS!0zkie^}UU zb9N8+@kiagL(f(M4wv0`LhKJYO~azkG|=B|8WH@+tDMh9Q;iZ>1wX59`{r3edSNLi&o)niBlT=iXz za2vo&mOZouALN*R=p^`w{uUjtebEZr%s;SDpomO5ntT7 zCxw0kb-xX++gbwO$pAb%$2}=)6O={9T0fs1+hAwmtJp%yeM7G+kr%U^eisL8zC zaH+(Ts1}e6jmr^-7DUuzi%^~D+>S~3+k+aQqvLmx3WzpLUiVDP(`j3|9(ALK^~gLo ziR!{HmCoDF&yTkt#4B3a%oS?KpDG&6@Vd%c;&iRTX_K#(O?|>vDT~nY?b>qLVG7l3 zli8Bf8ETtSCUkq?ocv7Xzu|L2e+7eTm3&xoTFvY_g^JsHm1nJ=BR+b+BKoPP5vBRr z80Bf1D3>?O)#Y+jK?EFMd@FGCnLuQ$Ts~QR?)zF)(cGa$+0r9OUL*gI8bwKJCPrnZ z5-naOhh#H(Jbxrh)5KLTj}V!d8Fgh0T>+>H%?V%twd2r9 zBb4mN2?K3A^m6F?pc8o_OWL!2GAHuS+OvH^0f=wV?!uX8u_u(QEA|&o{1|K_@d4XB rWTlrB)`6bxz5_i@C^?_AP{qNz+7q=0jUERnvEiVx&plkIFLLHTq-c?$ literal 0 HcmV?d00001 diff --git a/intTests/test1691/test.c b/intTests/test1691/test.c new file mode 100644 index 0000000000..9e5a88524a --- /dev/null +++ b/intTests/test1691/test.c @@ -0,0 +1,8 @@ +struct s { + unsigned x:1; + unsigned y:1; +}; + +int f(const struct s *ss) { + return ss->x == ss->y; +} diff --git a/intTests/test1691/test.saw b/intTests/test1691/test.saw new file mode 100644 index 0000000000..c6781b6e0f --- /dev/null +++ b/intTests/test1691/test.saw @@ -0,0 +1,17 @@ +enable_experimental; +enable_lax_loads_and_stores; + +let f_spec = do { + ss <- llvm_alloc_readonly (llvm_alias "struct.s"); + x <- llvm_fresh_var "x" (llvm_int 1); + y <- llvm_fresh_var "y" (llvm_int 1); + llvm_points_to_bitfield ss "x" (llvm_term x); + llvm_points_to_bitfield ss "y" (llvm_term y); + + llvm_execute_func [ss]; + + llvm_return (llvm_term {{ if x == y then 1 else 0 : [32] }}); +}; + +m <- llvm_load_module "test.bc"; +ov <- llvm_verify m "f" [] false f_spec (w4_unint_yices []); diff --git a/intTests/test1691/test.sh b/intTests/test1691/test.sh new file mode 100755 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test1691/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw