Skip to content
New issue

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

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

Already on GitHub? Sign in to your account

malloc returning different pointers in src and tgt #1136

Open
regehr opened this issue Dec 7, 2024 · 0 comments
Open

malloc returning different pointers in src and tgt #1136

regehr opened this issue Dec 7, 2024 · 0 comments

Comments

@regehr
Copy link
Contributor

regehr commented Dec 7, 2024

this one is sort of wild, I'm getting a value mismatch from arm-tv on this function, but in the counterexample it looks like Alive is saying that malloc returns different values in src and tgt. so I don't understand what's going on, but it seems like it has to behave the same on both sides, right?

declare ptr @malloc(i64)

define i1 @f(ptr %0) {
  %2 = call nonnull ptr @malloc(i64 16)
  %3 = icmp eq ptr %2, %0
  ret i1 %3
}

this gets lowered to something that seems sensible:

_f:                                     ; @f
	stp	x20, x19, [sp, #-32]!           ; 16-byte Folded Spill
	stp	x29, x30, [sp, #16]             ; 16-byte Folded Spill
	.cfi_def_cfa_offset 32
	.cfi_offset w30, -8
	.cfi_offset w29, -16
	.cfi_offset w19, -24
	.cfi_offset w20, -32
	mov	x19, x0
	mov	w0, #16                         ; =0x10
	bl	_malloc
	ldp	x29, x30, [sp, #16]             ; 16-byte Folded Reload
	cmp	x0, x19
	cset	w0, eq
	ldp	x20, x19, [sp], #32             ; 16-byte Folded Reload
	ret

and lifted to:

declare void @llvm.assert(i1)

define i1 @f(ptr %0) local_unnamed_addr {
arm_tv_entry:
  %stack = tail call align 16 dereferenceable(1280) ptr @myalloc(i64 1280, i64 16)
  %1 = getelementptr inbounds nuw i8, ptr %stack, i64 1024
  %2 = ptrtoint ptr %1 to i64
  %3 = getelementptr inbounds nuw i8, ptr %stack, i64 1008
  %a3_8 = add i64 %2, -16
  %4 = tail call dereferenceable_or_null(16) ptr @malloc(i64 16)
  %a8_6.not = icmp eq ptr %4, %0
  %5 = inttoptr i64 %a3_8 to ptr
  %6 = getelementptr i8, ptr %5, i64 8
  tail call void @llvm.memset.p0.i64(ptr noundef nonnull align 16 dereferenceable(16) %3, i8 0, i64 16, i1 false)
  %a10_7 = load i64, ptr %6, align 8
  tail call void @llvm.assert(i1 true)
  %a11_3 = icmp eq i64 %a10_7, 0
  tail call void @llvm.assert(i1 %a11_3)
  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 @myfree(ptr nonnull %stack)
  ret i1 %a8_6.not
}

; 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

; Function Attrs: mustprogress nofree nounwind willreturn allockind("alloc,uninitialized") allocsize(0) memory(inaccessiblemem: readwrite)
declare noalias noundef ptr @malloc(i64 noundef) local_unnamed_addr #2

; Function Attrs: nocallback nofree nounwind willreturn memory(argmem: write)
declare void @llvm.memset.p0.i64(ptr nocapture writeonly, i8, i64, i1 immarg) #3

attributes #0 = { mustprogress willreturn allockind("alloc") allocsize(0) "alloc-family"="arm-tv-alloc" }
attributes #1 = { mustprogress willreturn allockind("free") "alloc-family"="arm-tv-alloc" }
attributes #2 = { mustprogress nofree nounwind willreturn allockind("alloc,uninitialized") allocsize(0) memory(inaccessiblemem: readwrite) "alloc-family"="malloc" }
attributes #3 = { nocallback nofree nounwind willreturn memory(argmem: write) }

notice that if we ignore the clutter, src and tgt are performing identical computations!
anyway, in the CEX that I'm getting, malloc returns non-null in src and null in tgt, causing the value mismatch.

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

No branches or pull requests

1 participant