AliveToolkit / alive2

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

Missing support for memory(argmem) with escaped ptrs through ptr2int #969

Open regehr opened 7 months ago

regehr commented 7 months ago

I was debugging a issue found by arm-tv and it boils down alive-tv not being happy about this input. I can't figure out what's going on. the problem depends on the (unused) argument %0 being there.

@X = external global i32

define i32 @test2(ptr %0) {
  %2 = load i32, ptr @X, align 4
  ret i32 %2
}
regehr@john-home:~/reduce$ ~/alive2-regehr/build/alive-tv reduced.ll 

----------------------------------------
@X = global 4 bytes, align 4

define i32 @test2(ptr %#0) {
#1:
  %#2 = load i32, ptr @X, align 4
  ret i32 %#2
}
=>
@X = global 4 bytes, align 4

define i32 @test2(ptr nocapture noread nowrite %#0) nofree willreturn memory(globals: read, errno: read, other: read) {
#1:
  %#2 = load i32, ptr @X, align 4
  ret i32 %#2
}
Transformation doesn't verify!

ERROR: Source is more defined than target

Example:
ptr %#0 = pointer(non-local, block_id=1, offset=0)

Source:
i32 %#2 = poison

SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >   size: 0 align: 4    alloc type: 0   alive: false    address: 0
Contents:
else: poison

Block 1 >   size: 4 align: 4    alloc type: 0   alive: true address: 8
Contents:
else: poison

Block 2 >   size: 0 align: 1    alloc type: 0   alive: true address: 8
Contents:
else: poison

Target:
i32 %#2 = UB triggered!

Summary:
  0 correct transformations
  1 incorrect transformations
  0 failed-to-prove transformations
  0 Alive2 errors
regehr@john-home:~/reduce$ 

cc @tanmaytirpankar

nunoplopes commented 7 months ago

this requires rewriting the support for memory(argmem). The implementation is semantic, but LangRef uses a "based-on" definition. The full implementation is non-trivial due to ptr2int/int2ptr round-trips (ptr2int must escape the pointer I guess), but we can start with a simple data-flow propagation only.

regehr commented 7 months ago

I see... so this is about the attribute inference pass. makes sense. as a short-term workaround, should we maybe drop some of the inferred attributes that we get back from -O2 on code lifted from ARM assembly? that would be easy and sound.

nunoplopes commented 7 months ago

Ah, right, because you're running -O2 on the lifted code. Dropping all the attributes should be fine (or just make them equal to the source). I should be able to fix this within a few days. Just need to sleep today 😅

nunoplopes commented 7 months ago

Ok, partial implementation in. Should be good enough for your use cases. Doesn't take escape pointers into account.

regehr commented 7 months ago

awesome, thanks!