Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Fix false positive on icmp ptr with samesign flag #1151

Merged
merged 5 commits into from
Jan 5, 2025

Conversation

dtcxzyw
Copy link
Contributor

@dtcxzyw dtcxzyw commented Jan 3, 2025

Pointers should be interpreted as integral before extracting the sign bit.

Alive2: https://alive2.llvm.org/ce/z/GnWJ9H

----------------------------------------
define i1 @src(ptr %a, ptr %b) {
#0:
  %pa = ptrtoint ptr %a to i8
  %pb = ptrtoint ptr %b to i8
  %sub = sub i8 %pb, %pa
  %gep = gep ptr %a, 1 x i8 %sub
  %cmp = icmp samesign eq ptr %gep, null
  ret i1 %cmp
}
=>
define i1 @tgt(ptr %a, ptr %b) {
#0:
  %cmp = icmp samesign eq ptr %b, null
  ret i1 %cmp
}
Transformation doesn't verify!

ERROR: Target is more poisonous than source

Example:
ptr %a = null
ptr %b = pointer(non-local, block_id=2, offset=0) / Address=#x01

Source:
i8 %pa = #x00 (0)
i8 %pb = #x01 (1)
i8 %sub = #x01 (1)
ptr %gep = pointer(non-local, block_id=0, offset=1) / Address=#x01
i1 %cmp = #x0 (0)

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

Target:
i1 %cmp = poison
Source value: #x0 (0)
Target value: poison

@dtcxzyw dtcxzyw marked this pull request as draft January 3, 2025 12:08
@dtcxzyw dtcxzyw marked this pull request as ready for review January 3, 2025 12:13
@dtcxzyw dtcxzyw marked this pull request as draft January 3, 2025 12:17
@dtcxzyw dtcxzyw marked this pull request as ready for review January 3, 2025 12:23
@nunoplopes nunoplopes merged commit da0d731 into AliveToolkit:master Jan 5, 2025
15 checks passed
# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants