From 53b5ef0c8f2b5c14d0eeac38c409a3350c15a305 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Thu, 9 Mar 2023 10:06:17 -0500
Subject: [PATCH] Add test case for #1788

The fix for #1828 also addresses many of the symptoms of #1788, so let's add
a test case to ensure that those symptoms remain cured.
---
 intTests/test1788/Makefile |  17 +++++++++++++++++
 intTests/test1788/test.bc  | Bin 0 -> 2788 bytes
 intTests/test1788/test.c   |   5 +++++
 intTests/test1788/test.saw |  13 +++++++++++++
 intTests/test1788/test.sh  |   3 +++
 5 files changed, 38 insertions(+)
 create mode 100644 intTests/test1788/Makefile
 create mode 100644 intTests/test1788/test.bc
 create mode 100644 intTests/test1788/test.c
 create mode 100644 intTests/test1788/test.saw
 create mode 100755 intTests/test1788/test.sh

diff --git a/intTests/test1788/Makefile b/intTests/test1788/Makefile
new file mode 100644
index 0000000000..1a3bb3f6a4
--- /dev/null
+++ b/intTests/test1788/Makefile
@@ -0,0 +1,17 @@
+CC = clang
+CFLAGS = -g -frecord-command-line -O0
+
+all: test.bc test.exe
+
+test.bc: test.c
+	$(CC) $(CFLAGS) -c -emit-llvm $< -o $@
+
+test.o: test.c
+	$(CC) $(CFLAGS) -c $< -o $@
+
+test.exe: test.o
+	$(CC) $(CFLAGS) $< -o $@
+
+.PHONY: clean
+clean:
+	rm -f test.bc test.exe
diff --git a/intTests/test1788/test.bc b/intTests/test1788/test.bc
new file mode 100644
index 0000000000000000000000000000000000000000..8d2870d93b7a92c94964b81896792265dac28789
GIT binary patch
literal 2788
zcma)8ZA@F&89tY5I1ZR=^P$8f*UoiFBCCz@#U#YUumPqmS(yS^wPji-Y>dHfz}UY2
z!pWv<?C!d$H#u3PdQyIvHa}AB4_Trp+o}mLV-#5tjiQKA6oDW#tCEbZS(R?py7$;k
z_G8nub9KJnbKdv7U(Y$W(>i_cNG(F82%!N5zyDj`|J~5H|8f09MW5J10ZpesC{%(_
zMTrhUhjv26vHJ5J3$o*7DpSh^Dxo+~DzDSZ-X0KDFO_s&sOU_nOtogY`qgq%XR_Nn
zr>pO(mQt#Y3nhaK@~gF+_2ne@A!X`Js9(^(kZwFX_4;{kZUN-J#UTX8A=5tj4sP&G
zS<Sx731~JFlj+*(o@A;bk?2uzg3Q({L+7f*nAoYP>Z?MiPmRzofN#&-!KYtAp}c5^
zp5_!uUj&b*CBGU+ZPHm6Jsy#wUhLOnzl-*F<1^hbmYOqCB#omkS`ejXm*maj0Ltsw
zWxIBf;udt8Egd@-(=1L_KG3nZW11BkI~&u$DiY*4l#%>ME~F)|O9GjZh!pVRs2-0a
zvWMc9C)q8#b_HoSC)s%rHOa0_vul%@*%<qrJsIl8VHX|JOGKcHKBJd>St*>Bnr})0
z4oBNDV$iJS-el$N8BHFf5ebzmI`#pjc`igAj!4bDQq+YbE;=g5KAYsv;Ax^N99m>w
z)v>Gpi#;O+%s5<d&X2%^h&2A+eX_c)SrN6HI(CiHf=ajkLz(1wR`RN)AUGr~g|h|!
zLm*tV?+O-p$q%N%Sxex$ZN!0BH`m$4m=+wnHmOBtr)i6ewq$7$grp@wUkHsJ;vz*M
zlo@QRoTv6~i<Nh$*=@UaGgf&wt68D;F54=>)r&B-X~E=8*nswKuQBLdEm%D}!$Jh}
zly)Tx&etwcyyUe><9aM!ftKhK<_ibeq_7-EpC`a_R!$P?o2a^-3Zf?fh~toJ1P3(}
zwoXV_RCADM{It}PjW>&u4+06{yn@fV;(}L-F5AlQFO@yYVraKH97Z_GV}BM493DkV
zzZd%oV?r!$fPmX@Ad5rocr?vGOQuU@TOx+U^l><{RQ6cJQ56mq84Ih|RM;=#-8zN4
zCvo_T*>pJv8WJT*k)smz$*NvTCX!j9w4>@hvU8vAKxi;V2xU-B+Ki&EswbV=aqyLS
znRUXiPwdmjtI<`k_vf(QBp2Dab#|zhYD-$piCn5vgdD*_#;4dq%10{ZiO4i5I>FPB
z5$q6OTG$rflc(DjtZgZ}Egwk%IL^rNc(>#Qlz8b-MDlV{UA~HWm}b^_rH5B;Y%|-v
zOp|I(a}OY>)6CknL;PEo58{?3Ys+=I^@Dh8g0|$hYeP1C#)Xd(*x{oh$rP^*hx9n~
zv=qdKMX6sd`P7gv(s(9z=<zo5c#ZknH1m+B2NobZCfR(UUA41|MSR=K?xw9R3)YrQ
zp}m<iU$mN&wB=&X2#0<-VYx$FrgDluxFzo?$?uH^0BSZVpq2tzsqWTyl#h|}uf5D>
zn%QVqu5-*ou!7TTR%f)c9opM~yqI=%4KiKxDWx4!_nD`x$1cS!`QH6s8v=P3!I4Z~
z&y%#0ctHDxcG1p0&}r_?XnstQ`y;Q@Y}?CTdoym%=PXm!HgL$7v#py}OA@BJ)bGo|
zQYj4jK>h-VGqKk<RLsL^=6)~p8DBqhyF<IVzH511a}N~guCq+V+pfp=By#4IwI!cx
zy*bmekOLcA^WE2da1YtA4;*+(s{44Jd1zBUT7&de-shF~IpycQj7P<6@C-~pTPyq1
z8nfBUJmszHD}@_wn<{8-fBDWIb7lzERL;0;J(jl~OInYC)l1fIpm7eNVaO@Jwwtpi
z6?HrOrf#l2mO6j_qpqw<KiJx6>ik(+_g;kiGc~V|{Pgl_2?{ucK!d~R8XI*Q{eojG
z5HNO)IfA23Pe3qs+a0Ifo?+;P)6S6*qhJpk1c%@44H(^?z-z!N7>R(!qh_;X#O@j9
zLQcQn9`kUGd;@%j!@+@|ClGApy25t<5cl2UYL{~$ILsaQ42?abgdHxszh7`ioyMTx
zH;%Xmj3XnVQ9~nd9B_M#McIa7&M@S6I>!8i2FKXwsNFMY7;$@?oZ$q|862F!IqD7=
z2p?CpiZhHAM*|L2FBka<q^Osp#tBplv&K8M{4H>nsudb2v+boSIpS$PC#pVF#7`b-
zQl!r3Rf;B=l#(6P?`m%TZSyYE)uwl@{-&?wU_F_>bK~f*j@>ZrYPvCX?bm%j!RJoe
z9oJ3^$Ln7d-rI8^T|Gc%b!SeWt`O=SuL>{jIgml`1McBzMHS`nMuy?aIpxh*+W;0*
z)|RE*#1=abFJcFQ`<6~q%+sBRH*Cx&y^#LOO#%YtC%w!QqVh+o;vIwYt(W7LO8_dm
zEgNqIfTeTfAH&We^gZZnWF3cKYvJmW9dT=R{~e*f@CaFew(pgNbe}eP9EPZi<=)8h
z6dDbV1PXC*dmJOdL8mcdZtibBOq?Bz7=}GT2ns}A2n<3N7=qAv8eF7nGWGvIjDc~l
zQ)qDY_dnwadIa~d$2rJ>j0i%%yqtR<4Xfi+J5ssP8YOm=+9<?dL7?;JEUI(a5Ig;D
z*_7!-rKlu|?>r&~gS!j&Et=|($NA+hxu`}P)v=E+=@cdC)Gl>RqMmB1LblZG6ji05
z`2jED<Yh0N{3kp^xi6qmZjlEmudb!%DOAc2Dat$7(b_}@3?|l*EnXL&P@9oF363Sc
z{ejFzlcRkcLS$fKRQnQWQbuT`IN^uu0QA-LMLpS1o(=dNEa=z+J)xa~N($-8dXh|_
z?1owc)c}>eA<u+9TL;qfXNZiSt&<*%_zLYW(n!n+jr4>rKLi6PKLp(f4RjO8oWz^J
ereSbkxM9!<X!ARZ0RB4gUdO*<UxXH6L;nJ;bC1se

literal 0
HcmV?d00001

diff --git a/intTests/test1788/test.c b/intTests/test1788/test.c
new file mode 100644
index 0000000000..4bdebf77ed
--- /dev/null
+++ b/intTests/test1788/test.c
@@ -0,0 +1,5 @@
+#include <stdint.h>
+
+uint32_t mult(uint32_t x) {
+  return x * 0x85EBCA77U;
+}
diff --git a/intTests/test1788/test.saw b/intTests/test1788/test.saw
new file mode 100644
index 0000000000..ceb9626201
--- /dev/null
+++ b/intTests/test1788/test.saw
@@ -0,0 +1,13 @@
+// This test case ensures that ABC can prove that a C implementation of the
+// `mult` function is equivalent to a direct Cryptol implementation of the
+// same function.
+
+let
+{{
+cryptol_mult : [32] -> [32]
+cryptol_mult x = x * 0x85EBCA77
+}};
+
+m <- llvm_load_module "test.bc";
+llvm_mult <- llvm_extract m "mult";
+prove abc {{ \x -> llvm_mult x == cryptol_mult x }};
diff --git a/intTests/test1788/test.sh b/intTests/test1788/test.sh
new file mode 100755
index 0000000000..2315cc233c
--- /dev/null
+++ b/intTests/test1788/test.sh
@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw