aarch32-symbolic: Setting up an ABI-compatible stack

[langston-barrett]

Like #433 + #437, but for AArch32. Towards #430. Based on #438. Needs to be integrated into the test suite for validation.

[langston-barrett]

As can be seen in CI, all variants (un/optimized, lazy/eager memory model) of the movt test fail with the new stack setup code:

        tests/pass/movt.opt.exe:                      FAIL (0.08s)
          Testing test_movt at 0x100b8 (0.02s)
            Failed to prove goal: tests/pass/movt.opt.exe:0x100cc: error: in test_movt
            Error during memory load
            CallStack (from HasCallStack):
              error, called at src/Data/Macaw/Symbolic/Testing.hs:396:33 in macaw-symbolic-0.0.1-inplace:Data.Macaw.Symbolic.Testing
          
          Use -p '/Lazy memory model.True assertions.tests\/pass\/movt.opt.exe/' to rerun this test only.

Of course, they do so with the completely generic Error during memory load message 🙃 More investigation needed!

[langston-barrett]

Here's the source and the disassembly:

// movt.c
// 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();
}

On movt.unopt.exe, the failure is at 0x100ec, i.e., pop {r6, r7, fp}

armv7l-linux-musleabi-objdump -d -j.text movt.unopt.exe

000100b8 <test_movt>:
   100b8:       e92d08c0        push    {r6, r7, fp}
   100bc:       e28db008        add     fp, sp, #8
   100c0:       e24dd00c        sub     sp, sp, #12
   100c4:       e3a03000        mov     r3, #0
   100c8:       e50b3010        str     r3, [fp, #-16]
   100cc:       e3006000        movw    r6, #0
   100d0:       e3406001        movt    r6, #1
   100d4:       e3560000        cmp     r6, #0
   100d8:       13a03001        movne   r3, #1
   100dc:       e50b3010        str     r3, [fp, #-16]
   100e0:       e51b3010        ldr     r3, [fp, #-16]
   100e4:       e1a00003        mov     r0, r3
   100e8:       e24bd008        sub     sp, fp, #8
   100ec:       e8bd08c0        pop     {r6, r7, fp}
   100f0:       e12fff1e        bx      lr

000100f4 <_start>:
   100f4:       e92d4800        push    {fp, lr}
   100f8:       e28db004        add     fp, sp, #4
   100fc:       ebffffed        bl      100b8 <test_movt>
   10100:       e320f000        nop     {0}
   10104:       e8bd8800        pop     {fp, pc}

On movt.opt.exe, the failure is at 0x100cc, i.e., pop {r6, r7}:

armv7l-linux-musleabi-objdump -d -j.text movt.opt.exe

000100b8 <test_movt>:
   100b8:       e92d00c0        push    {r6, r7}
   100bc:       e3006000        movw    r6, #0
   100c0:       e3406001        movt    r6, #1
   100c4:       e3560000        cmp     r6, #0
   100c8:       13a00001        movne   r0, #1
   100cc:       e8bd00c0        pop     {r6, r7}
   100d0:       e12fff1e        bx      lr

000100d4 <_start>:
   100d4:       e12fff1e        bx      lr

For what it's worth, test_conditional_return also has pushes and pops.

[langston-barrett]

A simpler version of this test also fails:

int __attribute__((noinline)) test_noop(void) {
  __asm__(
  "nop;"
  : /* Outputs */
  : /* Inputs */
  : "r6", "r7" /* Clobbered registers */
  );
  return 0;
}

int main() {
  return test_noop();
}

000105b4 <test_noop>:
   105b4:       e92d00c0        push    {r6, r7}
   105b8:       e320f000        nop     {0}
   105bc:       e3a00000        mov     r0, #0
   105c0:       e8bd00c0        pop     {r6, r7}
   105c4:       e12fff1e        bx      lr

Failed to prove goal: tests/pass/noop.opt.exe:0x105c0: error: in test_noop

[langston-barrett]

@RyanGlScott points out that the generated Macaw CFG has a read_mem _R13_0 (bvle4) statement, which doesn't make much sense in context. This function should only be reading from negative offsets from the stack pointer (i.e., inside its own stack frame). @RyanGlScott speculates that this is an instance of #266 (comment)

0x100b8:
  ;  _R13 = stack_frame + 0
  # 0x100b8 0x100b8: STMDB_A1(xxxxxxxx.xxxxxxxx.00x0xxxx.xxxx1001) Rn 13, W 1, cond 14, register_list 192
  # 0x100b8: STMDB_A1(xxxxxxxx.xxxxxxxx.00x0xxxx.xxxx1001) Rn 13, W 1, cond 14, register_list 192
  r88 := (bv_add _R13_0 (0xfffffff8 :: [32]))
  r96 := (bv_add _R13_0 (0xfffffffc :: [32]))
  write_mem r88 _R6_0
  write_mem r96 _R7_0

  <snip>

  # 0x100cc: LDM_A1(xxxxxxxx.xxxxxxxx.10x1xxxx.xxxx1000) Rn 13, W 1, cond 14, register_list 192
  r136 := (bv_add _R13_0 (0xfffffffc :: [32]))
  r138 := read_mem _R13_0 (bvle4)
  r146 := read_mem r88 (bvle4)
  r147 := read_mem r136 (bvle4)

[langston-barrett]

After fixing an off-by-one error (the stack pointer was initially set to one past the end of the stack, instead of at the end), I now see:

macaw-aarch32-symbolic tests
  Binary Tests
    Default memory model
      True assertions
        tests/pass/noop.opt.exe: FAIL (0.83s)
          Testing test_noop at 0x105b4 (0.15s)
            tests/Main.hs:249:
            AssertionResult
            expected: SimulationResult Unsat
             but got: SimulationResult Sat

          Use -p '/noop/&&/Default memory model.True assertions.tests\/pass\/noop.opt.exe/' to rerun this test only.
    Lazy memory model
      True assertions
        tests/pass/noop.opt.exe: FAIL (0.48s)
          Testing test_noop at 0x105b4 (0.02s)
            tests/Main.hs:249:
            AssertionResult
            expected: SimulationResult Unsat
             but got: SimulationResult Sat

I think what was happening is that the read from r13 was previously reading at the end of the stack allocation, at offset 0x1000.... With the fix, the stack pointer gets aligned to something of the form 0xffff..0, and I believe that the read is now at that offset. This means that it's reading uninitialized bytes (instead of the read failing). I'm not quite sure why that would result in Sat here - seems like the return value should still just be concretely 1.

[langston-barrett]

Fascinating: it appears that CI passes. No idea why I might be getting Sat locally in that case.

[RyanGlScott]

Wild. I don't suppose it's due to your local copy not rebuilding things thoroughly?

For what it's worth, the macaw-aarch32-symbolic tests also pass when I try them locally.