From da064137717c14bc154d30fda9f700b748066819 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 26 Oct 2022 14:35:00 -0400
Subject: [PATCH] Add test case for movt semantics

This requires bumping the `asl-translator` submodule to bring the changes from
GaloisInc/asl-translator#47, which are necessary for the test case to work.
---
 deps/asl-translator                           |   2 +-
 macaw-aarch32-symbolic/tests/pass/Makefile    |   6 +++++
 macaw-aarch32-symbolic/tests/pass/movt.c      |  21 ++++++++++++++++++
 .../tests/pass/movt.opt.exe                   | Bin 0 -> 1044 bytes
 .../tests/pass/movt.unopt.exe                 | Bin 0 -> 1092 bytes
 5 files changed, 28 insertions(+), 1 deletion(-)
 create mode 100644 macaw-aarch32-symbolic/tests/pass/movt.c
 create mode 100755 macaw-aarch32-symbolic/tests/pass/movt.opt.exe
 create mode 100755 macaw-aarch32-symbolic/tests/pass/movt.unopt.exe

diff --git a/deps/asl-translator b/deps/asl-translator
index 4a7eb74d..94fcf64d 160000
--- a/deps/asl-translator
+++ b/deps/asl-translator
@@ -1 +1 @@
-Subproject commit 4a7eb74dada86f5296654e0daeecc21ae4e94504
+Subproject commit 94fcf64dc94dfa246afd34d600cc668be717a280
diff --git a/macaw-aarch32-symbolic/tests/pass/Makefile b/macaw-aarch32-symbolic/tests/pass/Makefile
index a4cbe59e..0b53e90c 100644
--- a/macaw-aarch32-symbolic/tests/pass/Makefile
+++ b/macaw-aarch32-symbolic/tests/pass/Makefile
@@ -17,3 +17,9 @@ all: $(unopt) $(opt)
 # conditionally performs a bunch of other operations instead
 test-conditional-return.opt.exe: test-conditional-return.c
 	$(CC) $(CFLAGS) -O1 $< -o $@
+
+# We need to pass -mcpu=cortex-a7 here
+movt.unopt.exe: movt.c
+	$(CC) $(CFLAGS) -mcpu=cortex-a7 -O0 $< -o $@
+movt.opt.exe: movt.c
+	$(CC) $(CFLAGS) -mcpu=cortex-a7 -O2 $< -o $@
diff --git a/macaw-aarch32-symbolic/tests/pass/movt.c b/macaw-aarch32-symbolic/tests/pass/movt.c
new file mode 100644
index 00000000..5f6797c3
--- /dev/null
+++ b/macaw-aarch32-symbolic/tests/pass/movt.c
@@ -0,0 +1,21 @@
+// A test case which ensures that the `movt` instruction works as expected.
+int __attribute__((noinline)) test_movt(void) {
+  int ret = 0;
+  // After the movt instruction, the value of r0 should be 0x10000, which
+  // should suffice to make the `movne %0 #1` instruction fire and set the
+  // value of ret (i.e., %0) to 1.
+  __asm__(
+  "movw      r6, #0x0;"
+  "movt      r6, #0x1;"
+  "cmp       r6, #0x0;"
+  "movne     %0, #1;"
+  : "=r"(ret) /* Outputs */
+  : /* Inputs */
+  : "r6", "r7" /* Clobbered registers */
+  );
+  return ret;
+}
+
+void _start() {
+  test_movt();
+}
diff --git a/macaw-aarch32-symbolic/tests/pass/movt.opt.exe b/macaw-aarch32-symbolic/tests/pass/movt.opt.exe
new file mode 100755
index 0000000000000000000000000000000000000000..27700aa85dc485f3e40ea7d593196aceeb86a694
GIT binary patch
literal 1044
zcma)5&ubGw82x59X;Qt^TG3W5Q6jX}jEO|j7KDZvd(bKh?RC4`EE+ILNoGYo=+S?`
zKfphuAVR^DcfnpI2<pv)SL=J5of@_mAG~?r`{tY3`L(Z`_wFdA#KMsUq5F)sN_EgU
zlC4TXT=eB77x$0qS*hdzEt!pzN;1&5F%?uv5i!X;`S6=*L5^VpnJJJpGoTBu-`|vW
z<<suV-}(1<|I{vB{8{_xHCDguOX-Jf%TR5v4MnzwO5UB`mk;0P53heE*Bg!1!op?{
zbxl-Q(N$e8RifBcUfn3`a#dFrM|r7ppMK~EZBa`Iv$d_JOq|Ho^J>zW&djJY>a2TC
z&8j(P-np!n)HUZemv#)?E8!-(cjS49|KP?u8~2%{a+J%+ufse-JDwLX2Y&!1rl2QN
zem3Q~5#AxsavJqlQvH>bUrG73lyAawJr|&yPddG4M(;?`7tad@18-pbzVW=oh27Rs
z9QPof<ieJ3FbGaeI4~Y3648Sf9peX3(;w**8+Cgo)Q`K74x;wcR;k?*ZNle9^iHqS
z3A+gDk2bV#OurpOm=Y`eKb%Kd4&<rw?)YYlpasv4&>(M??~`Y+2Q7dWwvO+Jb>*ak
z|HRcKrm&B^1>yniLSnc`-n0hF8iG3ha+a9@xel(I-{t=@364L=Wej?NoQ0k56cXcg
MZ&0^ki=ejdFYBCrTmS$7

literal 0
HcmV?d00001

diff --git a/macaw-aarch32-symbolic/tests/pass/movt.unopt.exe b/macaw-aarch32-symbolic/tests/pass/movt.unopt.exe
new file mode 100755
index 0000000000000000000000000000000000000000..0a30d93f35de3bfa10d0040a61e9f924aa48d22a
GIT binary patch
literal 1092
zcma)5O=}ZT6uoaIA5-fh){3@;5+p*cW}Ik5DhdrXR<QA-*t&B%(-};_B$B*{ZglI$
zU4KAax~d3b5eoeY{RuW9&>}(w!G%IRcam4*bmN6P=bdxUd-LYLH?Q&wH-!+SLZc~S
z_5;r>Frwq3Q8Y_Q(or)g9@Kk&b_y~8oY6oO6alUUDS(1f7<01DdA}n)z@dmiNg&xX
zisV<%-&vxCN9zxNB|kh^|M+{~d+U7p`7Zi-%Si7T@87hJZWmf)HQNbmxI-({7Av!D
zqUE-*n#Wm7SQ8zcnmfk!?bepDxjWgtutT@fdlAh2*6n_!{bZY7Z|=^|&0S4SExC<~
zY$RvQtZAh)jeuodUbIXrYi7>&bjopG9N%$EB&IQpURlml>_|Lkh#_qxGAd4pllmz!
zCdReN*l95>&TBXLQw|09hC}b;#sSy<@#;Y*{z^JJ)SKDUBJ{m$V5sKvfsKP3qPI>0
zd^p6%LYzN@&z$={0{@v%Jrm+HAwC=8d2rs(H6X7?<?1tOu2RY&+ji@9yDpuYwCz6g
zE8f94s6g*)zUN3x0wd|yrOgWwne`WC>9{~y>tRuiDpl#5k1Gw+ZIqsP>5@mL^q)&I
zSF7c+U%?=^STG$aYbCdVC9%W*iwW4`NbV}1-5M~3RKfR_!$k7=@O|bUYyj^eRVW|d
zBlcPS0{=tjl&N3i`gJ5O&{I{q1o5&WK=yDj4&Iz13rOAv@0;Jt|JM+5@In?b=`J)C
SYQ19+27RC4D<~6C`ThXEZjRpo

literal 0
HcmV?d00001