AliveToolkit / alive2

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

issue with returned arguments in asm memory mode #1014

Closed regehr closed 5 months ago

regehr commented 5 months ago

while working through the SPEC benchmarks I'm running into functions where arguments have the returned attribute, like this:

define ptr @src(ptr returned %this) {
  ret ptr %this
}

define ptr @tgt(ptr returned %this) {
  ret ptr %this
}

but then I'm getting:

regehr@john-home:~/alive2-regehr/build$ ./alive-tv --tgt-is-asm reduced.ll

----------------------------------------
define ptr @src(ptr returned %this) {
#0:
  ret ptr returned %this
}
=>
define ptr @tgt(ptr returned %this) asm {
#0:
  ret ptr returned %this
}
Transformation doesn't verify!

ERROR: Source is more defined than target

Example:
ptr returned %this = poison

Source:

SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >   size: 0 align: 1    alloc type: 0   alive: false    address: 0
Block 1 >   size: 9 align: 1    alloc type: 0   alive: true address: 8

Target:

regehr@john-home:~/alive2-regehr/build$ 
nunoplopes commented 5 months ago

funny. only repros in asm mode with poison input.

regehr commented 5 months ago

but if you add readnone then it triggers without poison/undef. on the other hand, this is on the tgt side, which gives me a workaround-- I can strip off that attribute from lifted code. should I just do that?

; ModuleID = 'reduced.bc'
target datalayout = "e-m:o-i64:64-i128:128-n32:64-S128"
target triple = "arm64-apple-macosx14.0.0"

; Function Attrs: strictfp
define ptr @src(ptr returned %this) #0 {
entry:
  ret ptr %this
}

define ptr @tgt(ptr readnone returned %this) local_unnamed_addr #0 {
entry:
  ret ptr %this
}

attributes #0 = { strictfp }
nunoplopes commented 5 months ago

Interesting. I'll try to debug it tonight. But stripping attributes is not ideal. Leaving them is good so get better coverage.

regehr commented 5 months ago

but note it's only on the tgt side that I have to remove the attribute -- no coverage lost

(sorry I did not notice that before mentioning this issue in the first place, I had not realized the subtlety that with poison inputs disabled it seems to require 2 attributes + asm mode to trigger this)