A source is more defined than target error

[aqjune]

The input (reduced by @Dongjoo-Kim):

declare i32* @g()

define void @f(i32** %p1, i32* %p2, i32** %p3, i32*) {
entry:
  load i32*, i32** %p1, align 8
  %cond1 = icmp eq i32* undef, %p2
  br i1 %cond1, label %if.then, label %exit
exit:
  ret void

if.then:
  %.1 = load i32, i32* %p2, align 8
  %cond2 = icmp eq i32 %.1, 0
  br i1 %cond2, label %if.then2, label %if.end2
if.then2:
  call i32* @g()
  br label %if.end2
if.end2:
  %i = load i32*, i32** %p3, align 8
  ret void
}

The example is pretty long; I guess it is related to quantification of undef vars. I'll reduce this more when I have time.

[aqjune]

Command: alive-tv <src> <src>

[aqjune]

Interestingly, the error disappeared after rebuilding Alive2 using the latest LLVM and Z3. Previously https://github.com/llvm/llvm-project/commit/5e31e226b5b2b682607a6578ff5adb33daf4fe39 and https://github.com/z3prover/z3/commit/c49d39af81a2a05a7cdb450175aed7a0c2ce72a9 were being used. This might be a sign of use after free in somewhere, but it isn't reproducible anymore using this example

[nunoplopes]

I can still reproduce this with latest LLVM & Z3 on ubuntu.

[aqjune]

Another pair that raises Mismatch in memory which might be relevant (reduced by @Dongjoo-Kim)

declare i8* @g()

define void @f(i8* noundef %p0) {
entry:
  %ptr = call i8* @g()
  store i8 undef, i8* %p0, align 1
  %cmp = icmp eq i8* %ptr, null
  br i1 %cmp, label %cleanup, label %if.end

if.end:
  %p2 = bitcast i8* %ptr to i8**
  load i8*, i8** %p2, align 1
  br label %cleanup

cleanup:
  ret void
}

This example is slightly shorter.

[aqjune]

Reduced further:

declare void @g()
@p = global i64 0

define void @f(i1 noundef %cond, i8** noundef %ptr) {
entry:
  call void @g()
  store i64 undef, i64* @p, align 8
  br i1 %cond, label %cleanup, label %if.end

if.end:
  load i8*, i8** %ptr, align 8
  br label %cleanup

cleanup:
  ret void
}

[aqjune]

The undef was constrained by a precondition that is introduced in POR (Memory::load). Since POR enforces upperbound of bid in src and tgt differently, this caused a behavior mismatch. A suggested fix: https://github.com/AliveToolkit/alive2/pull/659

[nunoplopes]

Last example repros again with a high timeout (30s).

[nunoplopes]

The bug is in the POR in loads() here:

https://github.com/AliveToolkit/alive2/blob/6eb3840ccfbc4ca8b02842c237325929490d143e/ir/memory.cpp#L1789