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

Missing support for memory(argmem) with escaped ptrs through ptr2int #969

Open
regehr opened this issue Nov 18, 2023 · 5 comments
Open

Missing support for memory(argmem) with escaped ptrs through ptr2int #969

regehr opened this issue Nov 18, 2023 · 5 comments
Labels
memory Memory Model

Comments

@regehr
Copy link
Contributor

regehr commented Nov 18, 2023

I was debugging a issue found by arm-tv and it boils down alive-tv not being happy about this input. I can't figure out what's going on. the problem depends on the (unused) argument %0 being there.

@X = external global i32

define i32 @test2(ptr %0) {
  %2 = load i32, ptr @X, align 4
  ret i32 %2
}
regehr@john-home:~/reduce$ ~/alive2-regehr/build/alive-tv reduced.ll 

----------------------------------------
@X = global 4 bytes, align 4

define i32 @test2(ptr %#0) {
#1:
  %#2 = load i32, ptr @X, align 4
  ret i32 %#2
}
=>
@X = global 4 bytes, align 4

define i32 @test2(ptr nocapture noread nowrite %#0) nofree willreturn memory(globals: read, errno: read, other: read) {
#1:
  %#2 = load i32, ptr @X, align 4
  ret i32 %#2
}
Transformation doesn't verify!

ERROR: Source is more defined than target

Example:
ptr %#0 = pointer(non-local, block_id=1, offset=0)

Source:
i32 %#2 = poison

SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >	size: 0	align: 4	alloc type: 0	alive: false	address: 0
Contents:
else: poison

Block 1 >	size: 4	align: 4	alloc type: 0	alive: true	address: 8
Contents:
else: poison

Block 2 >	size: 0	align: 1	alloc type: 0	alive: true	address: 8
Contents:
else: poison


Target:
i32 %#2 = UB triggered!


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

cc @tanmaytirpankar

@nunoplopes
Copy link
Member

this requires rewriting the support for memory(argmem). The implementation is semantic, but LangRef uses a "based-on" definition.
The full implementation is non-trivial due to ptr2int/int2ptr round-trips (ptr2int must escape the pointer I guess), but we can start with a simple data-flow propagation only.

@regehr
Copy link
Contributor Author

regehr commented Nov 19, 2023

I see... so this is about the attribute inference pass. makes sense. as a short-term workaround, should we maybe drop some of the inferred attributes that we get back from -O2 on code lifted from ARM assembly? that would be easy and sound.

@nunoplopes
Copy link
Member

Ah, right, because you're running -O2 on the lifted code.
Dropping all the attributes should be fine (or just make them equal to the source).
I should be able to fix this within a few days. Just need to sleep today 😅

nunoplopes added a commit that referenced this issue Nov 21, 2023
This implementation doesn't take escaped pointers through ptr2int into account
#969
@nunoplopes
Copy link
Member

Ok, partial implementation in. Should be good enough for your use cases. Doesn't take escape pointers into account.

@nunoplopes nunoplopes added the memory Memory Model label Nov 21, 2023
@nunoplopes nunoplopes changed the title unexpected UB Missing support for memory(argmem) with escaped ptrs through ptr2int Nov 21, 2023
@regehr
Copy link
Contributor Author

regehr commented Nov 21, 2023

awesome, thanks!

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

No branches or pull requests

2 participants