search

snu-sf-class / swpp202401

Principles and Practices of Software Development Main Repository
14 stars 4 forks source link

[Project] There seems to be a problem with the Alive2 patch regarding some intrinsic functions #166

Open choco-bear opened 5 months ago

choco-bear commented 5 months ago

안녕하세요, 다름이 아니라 패치와 관련하여 버그로 의심되는 현상을 또 발견하여 문의드립니다. [1]에서는 source의 %#1 = call i32 @decr_i32(i32 %a)의 리턴값이 없다는 출력이 있으며, [2]에서는 @incr_i64 함수가 UB를 발생시켰다고 하는데, 이는 아마 intrinsic function의 인자로 poison이 전달되는 경우를 처리하지 못해서 발생하는 것으로 보입니다. Intrinsic function의 인자로 poison이 전달되었을 때 리턴값이 poison인 것이 아닌 UB를 발생시키는 것이 의도된 동작인가요? 감사합니다.

[1]

TEST test/if2ternary/check3.ll

----------------------------------------
declare i32 @decr_i32(i32)
declare i32 @incr_i32(i32)

define i32 @iftest(i1 %cond, i32 %a) {
#0:
  br i1 %cond, label %if.true, label %if.false

if.false:
  %#1 = call i32 @decr_i32(i32 %a)
  br label %next

if.true:
  %#2 = call i32 @incr_i32(i32 %a)
  br label %next

next:
  %ret = phi i32 [ %#2, %if.true ], [ %#1, %if.false ]
  ret i32 %ret
}
=>
declare i32 @incr_i32(i32)
declare i32 @decr_i32(i32)

define i32 @iftest(i1 %cond, i32 %a) {
#0:
  %#1 = call i32 @incr_i32(i32 %a)
  %#2 = call i32 @decr_i32(i32 %a)
  %#3 = select i1 %cond, i32 %#1, i32 %#2
  ret i32 %#3
}
Transformation doesn't verify!

ERROR: Source is more defined than target

Example:
i1 %cond = #x0 (0)
i32 %a = poison

Source:
  >> Jump to %if.false
i32 %#1 = function did not return!

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

Target:
i32 %#1 = function did not return!

Summary:
  0 correct transformations
  1 incorrect transformations
  0 failed-to-prove transformations
  0 Alive2 errors

[2]

TEST test/arithmetic/check1.ll

----------------------------------------
define i32 @add(i64 %a) {
entry:
  %b = trunc i64 %a to i32
  %add10 = add nsw i32 %b, 1
  %add11 = add nsw i32 %add10, 4294967295
  %add12 = add nsw i32 %add11, 4
  %add13 = add nsw i32 %add12, 4294967292
  %add14 = add nsw i32 %add13, 3
  %add15 = add nsw i32 %add14, 4294967293
  %add16 = add nsw i32 %add15, 5
  %add17 = add nsw i32 %add16, 4294967291
  %add18 = add nsw i32 %add17, 2
  %add19 = add nsw i32 %add18, 4294967294
  %sub19 = sub nsw i32 %add19, 1
  %sub20 = sub nsw i32 %sub19, 4294967295
  %sub21 = sub nsw i32 %sub20, 4
  %sub22 = sub nsw i32 %sub21, 4294967292
  %sub23 = sub nsw i32 %sub22, 3
  %sub24 = sub nsw i32 %sub23, 4294967293
  %sub25 = sub nsw i32 %sub24, 5
  %sub26 = sub nsw i32 %sub25, 4294967291
  %sub27 = sub nsw i32 %sub26, 2
  %sub28 = sub nsw i32 %sub27, 4294967294
  ret i32 %sub28
}
=>
declare i64 @incr_i64(i64)
declare i64 @decr_i64(i64)
declare i32 @incr_i32(i32)
declare i32 @decr_i32(i32)

define i32 @add(i64 %a) {
entry:
  %#0 = call i64 @incr_i64(i64 %a)
  %#1 = call i64 @decr_i64(i64 %#0)
  %#2 = call i64 @incr_i64(i64 %#1)
  %#3 = call i64 @incr_i64(i64 %#2)
  %#4 = call i64 @incr_i64(i64 %#3)
  %#5 = call i64 @incr_i64(i64 %#4)
  %#6 = call i64 @decr_i64(i64 %#5)
  %#7 = call i64 @decr_i64(i64 %#6)
  %#8 = call i64 @decr_i64(i64 %#7)
  %#9 = call i64 @decr_i64(i64 %#8)
  %#10 = call i64 @incr_i64(i64 %#9)
  %#11 = call i64 @incr_i64(i64 %#10)
  %#12 = call i64 @incr_i64(i64 %#11)
  %#13 = call i64 @decr_i64(i64 %#12)
  %#14 = call i64 @decr_i64(i64 %#13)
  %#15 = call i64 @decr_i64(i64 %#14)
  %add6 = add nsw i64 %#15, 5
  %add7 = add nsw i64 %add6, -5
  %#16 = call i64 @incr_i64(i64 %add7)
  %#17 = call i64 @incr_i64(i64 %#16)
  %#18 = call i64 @decr_i64(i64 %#17)
  %#19 = call i64 @decr_i64(i64 %#18)
  %#20 = call i64 @decr_i64(i64 %#19)
  %#21 = call i64 @incr_i64(i64 %#20)
  %#22 = call i64 @decr_i64(i64 %#21)
  %#23 = call i64 @decr_i64(i64 %#22)
  %#24 = call i64 @decr_i64(i64 %#23)
  %#25 = call i64 @decr_i64(i64 %#24)
  %#26 = call i64 @incr_i64(i64 %#25)
  %#27 = call i64 @incr_i64(i64 %#26)
  %#28 = call i64 @incr_i64(i64 %#27)
  %#29 = call i64 @incr_i64(i64 %#28)
  %#30 = call i64 @decr_i64(i64 %#29)
  %#31 = call i64 @decr_i64(i64 %#30)
  %#32 = call i64 @decr_i64(i64 %#31)
  %#33 = call i64 @incr_i64(i64 %#32)
  %#34 = call i64 @incr_i64(i64 %#33)
  %#35 = call i64 @incr_i64(i64 %#34)
  %sub15 = sub nsw i64 %#35, 5
  %sub16 = sub nsw i64 %sub15, -5
  %#36 = call i64 @decr_i64(i64 %sub16)
  %#37 = call i64 @decr_i64(i64 %#36)
  %#38 = call i64 @incr_i64(i64 %#37)
  %#39 = call i64 @incr_i64(i64 %#38)
  %b = trunc i64 %a to i32
  %#40 = call i32 @incr_i32(i32 %b)
  %#41 = call i32 @decr_i32(i32 %#40)
  %#42 = call i32 @incr_i32(i32 %#41)
  %#43 = call i32 @incr_i32(i32 %#42)
  %#44 = call i32 @incr_i32(i32 %#43)
  %#45 = call i32 @incr_i32(i32 %#44)
  %#46 = call i32 @decr_i32(i32 %#45)
  %#47 = call i32 @decr_i32(i32 %#46)
  %#48 = call i32 @decr_i32(i32 %#47)
  %#49 = call i32 @decr_i32(i32 %#48)
  %#50 = call i32 @incr_i32(i32 %#49)
  %#51 = call i32 @incr_i32(i32 %#50)
  %#52 = call i32 @incr_i32(i32 %#51)
  %#53 = call i32 @decr_i32(i32 %#52)
  %#54 = call i32 @decr_i32(i32 %#53)
  %#55 = call i32 @decr_i32(i32 %#54)
  %add16 = add nsw i32 %#55, 5
  %add17 = add nsw i32 %add16, 4294967291
  %#56 = call i32 @incr_i32(i32 %add17)
  %#57 = call i32 @incr_i32(i32 %#56)
  %#58 = call i32 @decr_i32(i32 %#57)
  %#59 = call i32 @decr_i32(i32 %#58)
  %#60 = call i32 @decr_i32(i32 %#59)
  %#61 = call i32 @incr_i32(i32 %#60)
  %#62 = call i32 @decr_i32(i32 %#61)
  %#63 = call i32 @decr_i32(i32 %#62)
  %#64 = call i32 @decr_i32(i32 %#63)
  %#65 = call i32 @decr_i32(i32 %#64)
  %#66 = call i32 @incr_i32(i32 %#65)
  %#67 = call i32 @incr_i32(i32 %#66)
  %#68 = call i32 @incr_i32(i32 %#67)
  %#69 = call i32 @incr_i32(i32 %#68)
  %#70 = call i32 @decr_i32(i32 %#69)
  %#71 = call i32 @decr_i32(i32 %#70)
  %#72 = call i32 @decr_i32(i32 %#71)
  %#73 = call i32 @incr_i32(i32 %#72)
  %#74 = call i32 @incr_i32(i32 %#73)
  %#75 = call i32 @incr_i32(i32 %#74)
  %sub25 = sub nsw i32 %#75, 5
  %sub26 = sub nsw i32 %sub25, 4294967291
  %#76 = call i32 @decr_i32(i32 %sub26)
  %#77 = call i32 @decr_i32(i32 %#76)
  %#78 = call i32 @incr_i32(i32 %#77)
  %#79 = call i32 @incr_i32(i32 %#78)
  ret i32 %#79
}
Transformation doesn't verify!

ERROR: Source is more defined than target

Example:
i64 %a = poison

Source:
i32 %b = poison
i32 %add10 = poison
i32 %add11 = poison
i32 %add12 = poison
i32 %add13 = poison
i32 %add14 = poison
i32 %add15 = poison
i32 %add16 = poison
i32 %add17 = poison
i32 %add18 = poison
i32 %add19 = poison
i32 %sub19 = poison
i32 %sub20 = poison
i32 %sub21 = poison
i32 %sub22 = poison
i32 %sub23 = poison
i32 %sub24 = poison
i32 %sub25 = poison
i32 %sub26 = poison
i32 %sub27 = poison
i32 %sub28 = poison

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

Target:
Function @incr_i64 triggered UB

Summary:
  0 correct transformations
  1 incorrect transformations
  0 failed-to-prove transformations
  0 Alive2 errors
strikef commented 5 months ago

네, poison을 어떤 식으로든 값을 그대로 넘기지 않고 연산에 사용하면 UB가 발생하는 것이 맞습니다.

choco-bear commented 5 months ago

네, poison을 어떤 식으로든 값을 그대로 넘기지 않고 연산에 사용하면 UB가 발생하는 것이 맞습니다.

답변 감사합니다!

serverrepairman commented 5 months ago

@strikef 그런데 그럴 경우 %a가 poison일 때

%add = add i32 %a, 1

는 poison이고

%add = call i32 @incr_i32(i32 %a)

는 UB를 발생시킨다면

단지 1을 더하는 instruction조차 @incr_i32으로 변경할 수 없는 것 아닌가요? 이 경우 @incr_i32를 사용할 수 있는 경우가 있나요?