Skip to content

writeonly fns cannot read memory, but fninputRefined violates it #650

@aqjune

Description

@aqjune

Consider this function:

define void @f(i8* %p) {
  %call = call i8* @g1(i8* %p)
  call void @g2(i8* %call)
  ret void
}

declare i8* @g1(i8*)
declare void @g2(i8*) writeonly

Running alive-tv with an identity input raises ERROR: Source is more defined than target, and the reason is pretty interesting.

When encoding the refinement of g2's inputs, Pointer::fninputRefined is called. fninputRefined is checking isBlockAlive().implies(other.isBlockAlive()), but this isn't well-defined because g2 is a writeonly function.
State::addFnCall is filling the source's input memory with just an initial memory.

Should Pointer::fninputRefined take an additional flag which doesn't check liveness? Pointer::fninputRefined already has is_byval_arg flag.

Metadata

Metadata

Assignees

No one assigned

    Labels

    memoryMemory Model

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions