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

vexing value mismatch from arm-tv, in addresses of stack memory #1153

Closed
regehr opened this issue Jan 3, 2025 · 1 comment
Closed

vexing value mismatch from arm-tv, in addresses of stack memory #1153

regehr opened this issue Jan 3, 2025 · 1 comment

Comments

@regehr
Copy link
Contributor

regehr commented Jan 3, 2025

Is there something we can do about this sort of issue?

src is:

define ptr @f() {
  %1 = alloca i32, align 4
  %2 = getelementptr i8, ptr %1, i32 -2
  ret ptr %2
}

tgt is:

define nonnull ptr @f() {
arm_tv_entry:
  %stack17 = alloca i8, i64 1280, align 16
  %0 = getelementptr inbounds nuw i8, ptr %stack17, i64 1024
  %1 = ptrtoint ptr %0 to i64
  %a6_2 = add i64 %1, -6
  %2 = inttoptr i64 %a6_2 to ptr
  ret ptr %2
}

pretty clearly this is a faithful translation, as far as arm-tv is concerned, but I get a value mismatch out of it. not sure what the fix here would be.

----------------------------------------
define ptr @f() {
#0:
  %#1 = alloca i64 4, align 4
  %#2 = gep ptr %#1, 1 x i32 4294967294
  ret ptr %#2
}
=>
define ptr @f() nonnull asm {
arm_tv_entry:
  %stack17 = alloca i64 1 x i64 1280, align 16
  %#0 = gep inbounds nuw ptr %stack17, 1 x i64 1024
  %#1 = ptrtoint ptr %#0 to i64
  %a6_2 = add i64 %#1, -6
  %#2 = int2ptr i64 %a6_2 to ptr
  ret ptr %#2
}
Transformation doesn't verify!

ERROR: Value mismatch

Example:

Source:
ptr %#1 = pointer(local, block_id=0, offset=0) / Address=#x8000000000000000
ptr %#2 = pointer(local, block_id=0, offset=-2) / Address=#x7ffffffffffffffe

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

LOCAL BLOCKS:
Block 2 >	size: 4	align: 4	alloc type: 1	alive: true	address: 9223372036854775808

Target:
ptr %stack17 = pointer(local, block_id=0, offset=0) / Address=#x8000000000000000
ptr %#0 = pointer(local, block_id=0, offset=1024) / Address=#x8000000000000400
i64 %#1 = #x8000000000000400 (9223372036854776832, -9223372036854774784)
i64 %a6_2 = #x80000000000003fa (9223372036854776826, -9223372036854774790)
ptr %#2 = phy-ptr(addr=9223372036854776826) / Address=#x80000000000003fa

TARGET MEMORY STATE
===================
LOCAL BLOCKS:
Block 2 >	size: 1280	align: 16	alloc type: 1	alive: true	address: 9223372036854775808
Source value: pointer(local, block_id=0, offset=-2) / Address=#x7ffffffffffffffe
Target value: phy-ptr(addr=9223372036854776826) / Address=#x80000000000003fa

done comparing functions
Summary:
  0 correct transformations
  1 incorrect transformations
  0 failed-to-prove transformations
  0 Alive2 errors
@regehr
Copy link
Contributor Author

regehr commented Jan 3, 2025

(removing nonnull from tgt doesn't help. I mean it doesn't seem like it would, but I double checked)

# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant