Pointer arithmetic *(--p) fails verification

[ttaubert]

Suppose we have this somewhat nonsensical function:

uint8_t test(uint8_t* a) {
    uint8_t* pa = a + 1;
    return *(pa - 1);
}

And here's some SAW code to test it:

llvm_verify m "test" [] do {
    llvm_ptr "a" (llvm_array 1 (llvm_int 8));
    a <- llvm_var "*a" (llvm_array 1 (llvm_int 8));
    llvm_return {{ a @ 0 }};
    llvm_verify_tactic abc;
};

This yields Successfully verified @test. If you change the function to the following though you get a user error:

uint8_t test(uint8_t* a) {
    uint8_t* pa = a + 1;
    return *(--pa);
}

Simulation error: Invalid load address (Prelude.bvAdd
                        64
                        lss__alloc0
                        (Prelude.bvNat 64 4294967296))
  at #0:@test:%0.0:9
All paths yielded errors!
--------------------------------------------------------------------------------
Error reason        : Invalid load address (Prelude.bvAdd
                        64
                        lss__alloc0
                        (Prelude.bvNat 64 4294967296))
Error path state    :
Path #0:@test:%0.0:9
Stack frame
  Allocations:
    StackAlloc lss__alloc2 Prelude.bvNat
                             64
                             8
    StackAlloc lss__alloc1 Prelude.bvNat
                             64
                             8
  Writes:
    *lss__alloc2 := Prelude.bvAdd
                      64
                      lss__alloc0
                      (Prelude.bvNat 64 4294967296)
    *lss__alloc2 := Prelude.bvAdd 64
                      lss__alloc0
                      (Prelude.bvNat 64 1)
    *lss__alloc1 := lss__alloc0
    *lss__alloc0 := *(%a)
Base memory
  Allocations:
    HeapAlloc lss__alloc0 Prelude.bvNat
                            64
                            1
  Writes:

--------------------------------------------------------------------------------
All paths yielded errors!
--------------------------------------------------------------------------------
Error reason        : Invalid load address (Prelude.bvAdd
                        64
                        lss__alloc0
                        (Prelude.bvNat 64 4294967296))
Error path state    :
Path #0:@test:%0.0:9
Stack frame
  Allocations:
    StackAlloc lss__alloc2 Prelude.bvNat
                             64
                             8
    StackAlloc lss__alloc1 Prelude.bvNat
                             64
                             8
  Writes:
    *lss__alloc2 := Prelude.bvAdd
                      64
                      lss__alloc0
                      (Prelude.bvNat 64 4294967296)
    *lss__alloc2 := Prelude.bvAdd 64
                      lss__alloc0
                      (Prelude.bvNat 64 1)
    *lss__alloc1 := lss__alloc0
    *lss__alloc0 := *(%a)
Base memory
  Allocations:
    HeapAlloc lss__alloc0 Prelude.bvNat
                            64
                            1
  Writes:

--------------------------------------------------------------------------------
saw: user error (simulator did not return value when expected)

[ttaubert]

It looks like decrementing the pointer with --pa just doesn't work, you can fix the code by doing pa -= 1; return *pa; if we wanted to keep the behavior modifying the pointer.

[atomb]

This is a subtle bug! The difference in the generated LLVM code is twofold:

• The latter version stores the result of the pointer decrement, which I think is irrelevant.
• The latter version uses a 32-bit -1 constant in the getelementptr instruction whereas the former uses a 64-bit -1 constant. We currently assume 64-bit addresses.

I expect that the 32-bit -1 isn't being sign-extended, so it gets treated as a large positive value instead of a negative value.