alive2 icon indicating copy to clipboard operation
alive2 copied to clipboard

Encode the basic refinement of escaped local blocks

Open aqjune opened this issue 3 years ago • 7 comments

This patch checks the bytes of local blocks escaped via fn calls (resolves #435 ).

This check is done when the local block ids are known to be constants (which is common). Otherwise, it fallbacks into the original checking.

The beginning point for reading the diff of this PR would be Pointer::fninputRefined. If the pointer bids are constant and local, it now calls Pointer::encodeLocalPtrRefinement which is a new member function.

Among Pointer::encodeLocalPtrRefinement's arguments, readsbytes is:

  • if true, compare the blocks’ bytes as well as all other block attributes (which is implemented in Memory::blockRefined)
    • Note that, previously, Memory::blockRefined was receiving one non-local block id; in this PR, bid_other optional argument is added. If it is some(bid_other), refinement of two local blocks bid and bid_other is encoded.
    • Memory::blockRefined again calls refinement between bytes, which can be pointer bytes. It calls Pointer::refined, and Pointer::refined’s block_refined is still commentized, so recursive pointer refinement call does not happen.
  • if false, compare block attributes except bytes (Memory::blockPropertiesRefined).

The byval encoding is updated to check the contents as well. It follows the encoding of the cav paper.

aqjune avatar Oct 10 '21 13:10 aqjune

Unfortunately, alive-tv/calls/call.{src,tgt}.ll is failing for some reason. :/ Also, alive-tv/bugs/pr10067.srctgt.ll is raising some weird message (regarding approximation).

I'll look into these issues tomorrow. My room isn't provided internet access, and my tethering has a daily quota. :(

aqjune avatar Oct 10 '21 13:10 aqjune

Ready to be reviewed.

aqjune avatar Oct 17 '21 08:10 aqjune

The updated unit tests succeed, but I'll run LLVM unit tests and see how it goes (not sure I'll be back today).

aqjune avatar Feb 05 '22 06:02 aqjune

Four new failures appear, and the reasons are as follows:

Transforms/DeadStoreElimination/captures-before-call.ll Transforms/DeadStoreElimination/captures-before-load.ll -> They fail due to https://github.com/AliveToolkit/alive2/issues/650

Transforms/MemCpyOpt/callslot.ll -> This fails because the pointer refinement defined in CAV isn't sufficient! :( Pointers of different offsets must be allowed.

define void @dest_is_gep_nounwind_call() {
%0:
  %dest = alloca i64 16, align 1
  %src = alloca i64 8, align 1
  %src.i8 = bitcast * %src to *
  %dest.i8 = gep * %dest, 16 x i64 0, 1 x i64 8
  call void @accept_ptr(* %src.i8)
  memcpy * %dest.i8 align 1, * %src.i8 align 1, i64 8
  ret void
}
=>
define void @dest_is_gep_nounwind_call() {
%0:
  %dest = alloca i64 16, align 1
  %src = alloca i64 8, align 1
  %dest.i8 = gep * %dest, 16 x i64 0, 1 x i64 8
  %dest.i81 = bitcast * %dest.i8 to *
  %dest.i812 = bitcast * %dest.i81 to *
  call void @accept_ptr(* %dest.i812)
  ret void
}
Transformation doesn't verify!
ERROR: Source is more defined than target

Transforms/LICM/promote-capture.ll -> I think this is a bug in Alive2. A phi node is not successfully getting a value from the operand, or the counter example is not being correctly printed.

  %if:
    %c.inc = add i32 %c.inc2, 1
    br label %latch
  
  %latch:
    %c.inc1 = phi i32 [ %c.inc, %if ], [ %c.inc2, %loop ]

CEx:

    >> Jump to %if
  i32 %c.inc = #x00000001 (1)
    >> Jump to %latch
  i32 %c.inc1 = #x00000000 (0)

aqjune avatar Feb 06 '22 07:02 aqjune

For the first two failures, I added tests/alive-tv/calls/writeonly-local.srctgt.ll to this PR that must succeed after the issue is fixed.

aqjune avatar Feb 06 '22 07:02 aqjune

Updated the description to explain from which function reading the diff would start.

aqjune avatar Feb 26 '22 05:02 aqjune

These tests have invalid transformations involving escaped local blocks, but Alive2 doesn't detect the problems even with this PR:

  • alive-tv/bugs/pr1014.srctgt.ll
  • alive-tv/bugs/pr23599.srctgt.ll

yotann avatar Apr 29 '22 21:04 yotann