alive2
alive2 copied to clipboard
Encode the basic refinement of escaped local blocks
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 issome(bid_other)
, refinement of two local blocksbid
andbid_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.
- Note that, previously, Memory::blockRefined was receiving one non-local block id; in this PR,
- 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.
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. :(
Ready to be reviewed.
The updated unit tests succeed, but I'll run LLVM unit tests and see how it goes (not sure I'll be back today).
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)
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.
Updated the description to explain from which function reading the diff would start.
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