AliveToolkit / alive2

Automatic verification of LLVM optimizations
MIT License
719 stars 93 forks source link

target-side padding for non-byte-sized loads/stores #1019

Closed regehr closed 3 weeks ago

regehr commented 4 months ago

Nuno and I have talked about this but I'd like to drop an issue here as a reminder.

this function:

define i8 @f(ptr %p) {
  %x = load i1, ptr %p, align 4
  %y = zext i1 %x to i8
  ret i8 %y
}

is quite properly lowered by the AArch64 backend to:

f:
        ldrb    w0, [x0]
        ret

but now it looks like there's been a refinement failure since Alive thinks this load can return values other than 0,1.

if I knew which loads and stores on the ARM side corresponded to LLVM-side loads and stores of i1, I could patch up the load side and insert the corresponding checking on the store side. but I don't, and I can't think of a different way to support this.

as far as I know, for practical purposes, i1 is the only case that actually matters

regehr commented 4 months ago

well, I didn't really want to do this, but now I'm tagging each LLVM instruction with a debug location and then using that to track where each ARM instruction comes from, in order to support patching up this sort of thing. this is working fine so far.

there are other use cases for this mapping, such as finding call site attributes, that I can't solve any other way that I can think of.

nunoplopes commented 3 weeks ago

This requires changes to the memory model. The justification for correctness is in Langref:

When loading a value of a type like i20 with a size that is not an integral number of bytes, the result is undefined if the value was not originally written using a store of the same type

Just making the memory bitwise poison isn't sufficient, we need to remember the stored type and poison the result if different.

nunoplopes commented 3 weeks ago

This is a bit complex feature. If you have time, please fire up your tests and let me know if there are false positives. I'm running the LLVM test suite right now to check for regressions as well.

regehr commented 3 weeks ago

awesome!

this version passes all of my tests -- doing some stress testing with arm-tv now.