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

Encode the basic refinement of escaped local blocks #753

Open
wants to merge 8 commits into
base: master
Choose a base branch
from

Conversation

aqjune
Copy link
Member

@aqjune aqjune commented Oct 10, 2021

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
Copy link
Member Author

aqjune commented Oct 10, 2021

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. :(

@@ -1890,7 +1891,23 @@ expr Memory::blockValRefined(const Memory &other, unsigned bid, bool local,
return val.refined(val2);
}

expr Memory::blockPropertiesRefined(const Pointer &src, const Pointer &tgt)
const {
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The code below is moved from Memory::blockRefined below

@@ -1890,7 +1891,23 @@ expr Memory::blockValRefined(const Memory &other, unsigned bid, bool local,
return val.refined(val2);
Copy link
Member Author

@aqjune aqjune Oct 10, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If pointer bytes are stored inside an alloca, this will call Pointer::refined.
Pointer::refined is unchanged in this PR, so this is fine.

@aqjune aqjune changed the title [WIP] Encode the basic refinement of escaped local blocks Encode the basic refinement of escaped local blocks Oct 17, 2021
@aqjune
Copy link
Member Author

aqjune commented Oct 17, 2021

Ready to be reviewed.

@aqjune
Copy link
Member Author

aqjune commented Feb 5, 2022

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
Copy link
Member Author

aqjune commented Feb 6, 2022

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 #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
Copy link
Member Author

aqjune commented Feb 6, 2022

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
Copy link
Member Author

aqjune commented Feb 26, 2022

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

@yotann
Copy link

yotann commented Apr 29, 2022

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

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

Successfully merging this pull request may close these issues.

Comparison of bytes of allocas given to function arguments
2 participants