Skip to content

possible bug in initializes semantics #1202

@regehr

Description

@regehr

here's a function:

define void @f(ptr %0, ptr %1) {
  %3 = load i64, ptr %1, align 4
  store i64 %3, ptr %0, align 4
  ret void
}

opt infers that %0 initializes 8 bytes of storage. this is fine by my reading of langref (the fact that %1 might alias some or all of the initialized storage is OK, according to the text)

but Alive is not happy about the aliasing case:

~$ ~/alive2-regehr/build/alive-tv foo.ll

----------------------------------------
define void @f(ptr %#0, ptr %#1) {
#2:
  %#3 = load i64, ptr %#1, align 4
  store i64 %#3, ptr %#0, align 4
  ret void
}
=>
define void @f(ptr nocapture noread initializes((0, 8)) %#0, ptr nocapture nowrite %#1) nofree willreturn memory(argmem: readwrite) {
#2:
  %#3 = load i64, ptr nocapture nowrite %#1, align 4
  store i64 %#3, ptr nocapture noread initializes((0, 8)) %#0, align 4
  ret void
}
Transformation doesn't verify!

ERROR: Source is more defined than target

Example:
ptr %#0 = pointer(non-local, block_id=1, offset=0, attrs=8) / Address=#x04
ptr %#1 = pointer(non-local, block_id=1, offset=0, attrs=8) / Address=#x04

Source:
i64 %#3 = poison

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

Target:
i64 %#3 = UB triggered!


Summary:
  0 correct transformations
  1 incorrect transformations
  0 failed-to-prove transformations
  0 Alive2 errors
~$ 

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions