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

@@ -1 +1 @@
-Subproject commit 4a7eb74dada86f5296654e0daeecc21ae4e94504
+Subproject commit 94fcf64dc94dfa246afd34d600cc668be717a280

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 $@

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();
+}