possible intresting issue with physical pointers

[regehr]

happily, I can now verify the AArch64 backend's translation of this kind of function:

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

however, a roundtrip through integer causes it to fail validation:

define ptr @f() {
  %1 = alloca i32, align 4
  %2 = ptrtoint ptr %1 to i64
  %3 = inttoptr i64 %2 to ptr
  ret ptr %3
}

the generated ARM is the same in both cases:

f:                         
	sub	sp, sp, #16
	add	x0, sp, #12
	add	sp, sp, #16
	ret

of course the lifted code is the same in both cases:

define nonnull ptr @f() local_unnamed_addr {
arm_tv_entry:
  %stack = tail call align 16 dereferenceable(1280) ptr @myalloc(i64 1280, i64 16)
  %0 = getelementptr inbounds i8, ptr %stack, i64 1024
  %1 = ptrtoint ptr %0 to i64
  %a5_1 = add i64 %1, -4
  tail call void @myfree(ptr nonnull %stack)
  %2 = inttoptr i64 %a5_1 to ptr
  ret ptr %2
}

; Function Attrs: mustprogress willreturn allockind("alloc") allocsize(0)
declare nonnull ptr @myalloc(i64, i64 allocalign) local_unnamed_addr #0

; Function Attrs: mustprogress willreturn allockind("free")
declare void @myfree(ptr allocptr) local_unnamed_addr #1

attributes #0 = { mustprogress willreturn allockind("alloc") allocsize(0) "alloc-family"="arm-tv-alloc" }
attributes #1 = { mustprogress willreturn allockind("free") "alloc-family"="arm-tv-alloc" }

here's the failing output:

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

----------------------------------------
define ptr @f() {
#0:
  %#1 = alloca i64 4, align 4
  %#2 = ptrtoint ptr %#1 to i64
  %#3 = int2ptr i64 %#2 to ptr
  ret ptr %#3
}
=>
declare ptr @myalloc(i64, allocalign i64) nonnull willreturn alloc-family(arm-tv-alloc) allockind(alloc) allocsize(0)
declare void @myfree(allocptr ptr) willreturn alloc-family(arm-tv-alloc) allockind(free)

define ptr @f() nonnull asm {
arm_tv_entry:
  %stack = tail call ptr @myalloc(i64 1280, allocalign i64 16) dereferenceable(1280) nonnull align(16) willreturn alloc-family(arm-tv-alloc) allockind(alloc) allocsize(0)
  %#0 = gep inbounds ptr %stack, 1 x i64 1024
  %#1 = ptrtoint ptr %#0 to i64
  %a5_1 = add i64 %#1, -4
  tail call void @myfree(nonnull allocptr ptr %stack) willreturn alloc-family(arm-tv-alloc) allockind(free)
  %#2 = int2ptr i64 %a5_1 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
i64 %#2 = #x8000000000000000 (9223372036854775808, -9223372036854775808)
ptr %#3 = phy-ptr(addr=9223372036854775808) / Address=#x8000000000000000

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

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

Target:
ptr %stack = 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 %a5_1 = #x80000000000003fc (9223372036854776828, -9223372036854774788)
Function @myfree returned
ptr %#2 = phy-ptr(addr=9223372036854776828) / Address=#x80000000000003fc

TARGET MEMORY STATE
===================
LOCAL BLOCKS:
Block 2 >	size: 1280	align: 16	alloc type: 2	alive: false	address: 9223372036854775808
Block 3 >	size: 0	align: 576460752303423488	alloc type: 0	alive: false	address: 8646911284551352320
Source value: phy-ptr(addr=9223372036854775808) / Address=#x8000000000000000
Target value: phy-ptr(addr=9223372036854776828) / Address=#x80000000000003fc

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

[regehr]

I wonder if this issue is related? I can't verify the lowering of this one either:

define void @f() {
  %1 = alloca i32, align 4
  call void @test1(ptr %1)
  ret void
}

declare void @test1(ptr)

the lifted code I end up with is:

define void @f() local_unnamed_addr {
arm_tv_entry:
  %stack = tail call align 16 dereferenceable(1280) ptr @myalloc(i64 1280, i64 16)
  %0 = getelementptr inbounds i8, ptr %stack, i64 1024
  %1 = ptrtoint ptr %0 to i64
  %2 = getelementptr inbounds i8, ptr %stack, i64 1008
  store i64 0, ptr %2, align 16
  %a5_1 = add i64 %1, -4
  %3 = inttoptr i64 %a5_1 to ptr
  tail call void @test1(ptr nonnull %3)
  tail call void @myfree(ptr nonnull %stack)
  ret void
}

; Function Attrs: mustprogress willreturn allockind("alloc") allocsize(0)
declare nonnull ptr @myalloc(i64, i64 allocalign) local_unnamed_addr #0

; Function Attrs: mustprogress willreturn allockind("free")
declare void @myfree(ptr allocptr) local_unnamed_addr #1

declare void @test1(ptr) local_unnamed_addr

attributes #0 = { mustprogress willreturn allockind("alloc") allocsize(0) "alloc-family"="arm-tv-alloc" }
attributes #1 = { mustprogress willreturn allockind("free") "alloc-family"="arm-tv-alloc" }

[regehr]

ok, sorry to pile on the examples, but here's one more, and this one is really stopping me from verifying interesting programs.

the src/tgt pair below does not verify in assembly mode. however, it does verify if I remove the ptr2int/int2ptr round trip, replace it with a GEP, and invoke alive-tv without assembly mode, but disabling poison and undef inputs.

src is:

define <4 x i32> @f(<4 x i32> %a) {
  %c = shufflevector <4 x i32> %a, <4 x i32> <i32 5, i32 6, i32 7, i32 8>, <4 x i32> <i32 0, i32 1, i32 6, i32 7>
  ret <4 x i32> %c
}

tgt is:

%0 = type { i8, i8, i8, i8, i8, i8, i8, i8, i8, i8, i8, i8, i8, i8, i8, i8 }

@.LCPI0_0 = constant %0 { i8 0, i8 0, i8 0, i8 0, i8 0, i8 0, i8 0, i8 0, i8 7, i8 0, i8 0, i8 0, i8 8, i8 0, i8 0, i8 0 }, align 16

declare void @llvm.assert(i1)

define <4 x i32> @f(<4 x i32> %0) local_unnamed_addr {
arm_tv_entry:
  %a8_2 = load i64, ptr inttoptr (i64 add (i64 ptrtoint (ptr @.LCPI0_0 to i64), i64 8) to ptr), align 8
  %1 = bitcast <4 x i32> %0 to <2 x i64>
  %a8_4 = insertelement <2 x i64> %1, i64 %a8_2, i64 1
  tail call void @llvm.assert(i1 true)
  tail call void @llvm.assert(i1 true)
  tail call void @llvm.assert(i1 true)
  tail call void @llvm.assert(i1 true)
  tail call void @llvm.assert(i1 true)
  tail call void @llvm.assert(i1 true)
  tail call void @llvm.assert(i1 true)
  tail call void @llvm.assert(i1 true)
  tail call void @llvm.assert(i1 true)
  tail call void @llvm.assert(i1 true)
  tail call void @llvm.assert(i1 true)
  %2 = bitcast <2 x i64> %a8_4 to <4 x i32>
  ret <4 x i32> %2
}