A failure due to an issue related with escaped local block

[aqjune]

This is a srctgt reduced from ph7:

define i32 @src(i8* %dummy, i8** %pCur1) {
entry:
  %retval = alloca i32, align 4
  %i = load i8*, i8** %pCur1, align 8
  %call16 = call i8* @f(i8* %i)
  call void @g(i8* %call16)
  ret i32 0
}

define i32 @tgt(i8* %dummy, i8** %pCur1) {
entry:
  %i = load i8*, i8** %pCur1, align 8
  %call16 = call i8* @f(i8* %i)
  call void @g(i8* %call16)
  ret i32 0
}

declare i8* @f(i8*)
declare void @g(i8*)

It fails because Alive2 finds a case when @f in src returns a local block.

I think this is related with is_initial_memblock, because -smt-verbose shows that %i looks like this:

%i = ((_ extract 11 0)
  (ite (= #b001 ((_ extract 10 8) %pCur1))
       (select init_mem_1 ((_ extract 7 3) %pCur1))
       (select init_mem_2 ((_ extract 7 3) %pCur1))))

[aqjune]

Just a second, is using equality here correct?

https://github.com/AliveToolkit/alive2/blob/a15bfb4bab6475a6e5b17449d1ed1ce8dc30d8c7/ir/state.cpp#L730

Local block map should be used instead, I guess.

[nunoplopes]

The equality there is ok. This is just to make fn calls in the source equal. That's sufficient to cover LLVM's optimizations AFAICT. The bug is elsewhere. But there's a bug, I agree :)

[aqjune]

Oh, sorry. Yes, it was relating src - src. https://github.com/AliveToolkit/alive2/blob/a15bfb4bab6475a6e5b17449d1ed1ce8dc30d8c7/ir/state.cpp#L751 This is relating src-tgt, and I guess this might be the place to fix.

[nunoplopes]

Ok, so the issue is that we overwrite the local memory of tgt. The encoding needs to copy only non-local and sync the local blocks.

The 2nd issue is that the alloca is considered escaped because Alive2 is too conservative in its analysis.

[aqjune]

Another related test that uses clang-tv (written by @regehr):

char *a() {
   char *b = __builtin_alloca(1);
   return a();
}

[aqjune]

Another example from redis:

define void @src() {
  %c = alloca ptr, align 8
  store ptr %c, ptr %c, align 8
  %call = call ptr @a()
  %l = load i32, ptr %call, align 4
  ret void
}

define void @tgt() {
  %call = call ptr @a()
  %l = load i32, ptr %call, align 4
  ret void
}

declare ptr @a()

Output message:

Transformation doesn't verify!

ERROR: Source is more defined than target

Source:
...
* %call = pointer(local, block_id=4, offset=0)
...
Target:
* %call = pointer(non-local, block_id=4, offset=0)

call @a in tgt cannot return a local pointer, but the counter example shows it is returning it (well, the message is saying it's non-local, but it cannot be)

[nunoplopes]

Another one from gcc bench:

declare ptr @f(ptr)
declare void @g(ptr)

define void @src(ptr %dummy, ptr %operands) {
  %src = alloca ptr, i32 0, align 8
  %ptr = load ptr, ptr %operands, align 8
  %call = call ptr @f(ptr %ptr)
  call void @g(ptr %call)
  ret void
}

define void @tgt(ptr %dummy, ptr %operands) {
  %ptr = load ptr, ptr %operands, align 8
  %call = call ptr @f(ptr %ptr)
  call void @g(ptr %call)
  ret void
}

[nunoplopes]

Another from gcc:

%struct.ix86_address = type { ptr, ptr, ptr, i64, i32 }

@__FUNCTION__.aligned_operand = external constant [8 x i8]

declare void @fancy_abort(ptr)

define i32 @aligned_operand(ptr %op) {
entry:
  %parts = alloca %struct.ix86_address, i32 0, align 8
  %0 = load ptr, ptr %op, align 8
  %call16 = call i32 @ix86_decompose_address(ptr %0)
  br i1 false, label %if.end19, label %if.then18

if.then18:
  call void @fancy_abort(ptr @__FUNCTION__.aligned_operand)
  unreachable

if.end19:
  %tobool20 = icmp ne ptr %0, null
  br i1 %tobool20, label %if.then21, label %if.then21

if.then21:
  br label %if.then21

if.then21:
  ret i32 0
}

declare i32 @ix86_decompose_address(ptr)

Need to fix this quickly.

[nunoplopes]

Last two examples fixed. The redis one is different, there's a store to unescaped memory. Our current abstraction is too coarse.

[nunoplopes]

Another example:

define ptr @src(ptr %n0) {
   %n2 = alloca ptr, i32 0, align 8
   %n3 = alloca i64, align 8
   store ptr %n3, ptr %n0, align 8
   %n5 = call ptr @fn()
   store ptr %n5, ptr %n0, align 8
   %n6 = load ptr, ptr %n0, align 8
   store ptr null, ptr %n5, align 8
   ret ptr null
}

define ptr @tgt(ptr %n0) {
   %n3 = alloca i64, align 8
   store ptr %n3, ptr %n0, align 8
   %n5 = call ptr @fn()
   store ptr %n5, ptr %n0, align 8
   %n6 = load ptr, ptr %n0, align 8
   store ptr null, ptr %n5, align 8
   ret ptr null
}

declare ptr @fn()

This one requires synthesizing a synchronization map. Src program returns block 9, while tgt doesn't even have block 9 because one the allocas was removed. Block 9 in src <=> block 8 in tgt.