x86-symbolic: Setting up a SysV-compatible stack

[langston-barrett]

Towards #430 and #434.

[langston-barrett]

Ok, I finally got this to the point where I can run the SysV stack setup code in the macaw-x86-symbolic test suite. Tests are now failing mysteriously:

        tests/fail/constant.unopt.exe:      FAIL
          Testing test_constant
            You have encountered a bug in Crucible's implementation.
            *** Please create an issue at https://github.com/GaloisInc/crucible/issues

            %< ---------------------------------------------------
              Revision:  e86140641260b00f64fdbd51d73d48d766c55bdf
              Branch:    HEAD
              Location:  writeMemWithAllocationCheck
              Message:   Expected succesful byte load when updating SMT array
                         but got an error instead
            CallStack (from HasCallStack):
              panic, called at src/Lang/Crucible/Panic.hs:11:9 in crucible-0.7.0.99-inplace:Lang.Crucible.Panic
              panic, called at src/Lang/Crucible/LLVM/MemModel/Generic.hs:1333:23 in crucible-llvm-0.6.0.99-inplace:Lang.Crucible.LLVM.MemModel.Generic
            %< ---------------------------------------------------

          Use -p '/Lazy memory model.False assertions.tests\/fail\/constant.unopt.exe/' to rerun this test only.

https://github.com/GaloisInc/crucible/blob/62359553c204abd18c4d98fcff74b750a2a15232/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs#L1333-L1336

[langston-barrett]

Ok, it's actually kind of non-trivial to see why this is failing. I modified ?recordLLVMAnnotation to print out the memory error explanations as the safety assertions are made, the last one for each test-case is something like this, so I think this is the one that's failing:

Unexpected argument type:
While selecting the low bits of a bitvector
  bitvectorType 8
Performing store at type: i512
  Via pointer: (2, 0xffff8:[64])
In memory state:
  Base memory
    Allocations:
      StackAlloc 2 0x100000:[64] Mutable 1-byte-aligned stack_alloc
      GlobalAlloc 1 0xffffffffffffffff:[64] Mutable 1-byte-aligned Global memory for macaw-symbolic
    Writes:
      Indexed chunk:
        1 |->   *(1, 0x0:[64]) := cglobalMemoryBytes@0:a
        2 |->   *(2, 0x0:[64]) := cstack_array@76:a

It makes sense that this would fail, because it's performing a 512-bit store at a stack offset that definitely doesn't have enough room for that. As for why it's doing a 512-bit store there... 🤷

[langston-barrett]

As for why it's doing a 512-bit store there... 🤷

It's because I wrote Bytes.toBytes 64 when I meant Bytes.toBytes 8 when describing the size of the return address that gets written to the stack. Fixed! Still seems wrong for the memory model to panic, I would expect for an assertion to fail with a reasonable message.