Skip to content

Commit

Permalink
[ConstraintElimination] Rewrite tests to reduce verification complexity.
Browse files Browse the repository at this point in the history 
This patch reduces the bitwidth of types certain tests operate and gets
rid of a number of @use(i1) calls and xor's the conditions together
instead, which eliminates all timeouts when verifying the tests.
See AliveToolkit/alive2#744 for more details.
  • Loading branch information
@fhahn
fhahn committed Aug 26, 2021
1 parent 55bdb14 commit 0bcfd4c
Show file tree
Hide file tree
Showing 10 changed files with 878 additions and 960 deletions.
177 changes: 81 additions & 96 deletions llvm/test/Transforms/ConstraintElimination/and.ll
View file
Expand Up @@ -3,145 +3,130 @@

declare void @use(i1)

define i32 @test_and_ule(i32 %x, i32 %y, i32 %z, i32 %a) {
define i1 @test_and_ule(i4 %x, i4 %y, i4 %z, i4 %a) {
; CHECK-LABEL: @test_and_ule(
; CHECK-NEXT: entry:
; CHECK-NEXT: [[C_1:%.*]] = icmp ule i32 [[X:%.*]], [[Y:%.*]]
; CHECK-NEXT: [[C_2:%.*]] = icmp ule i32 [[Y]], [[Z:%.*]]
; CHECK-NEXT: [[C_1:%.*]] = icmp ule i4 [[X:%.*]], [[Y:%.*]]
; CHECK-NEXT: [[C_2:%.*]] = icmp ule i4 [[Y]], [[Z:%.*]]
; CHECK-NEXT: [[AND:%.*]] = and i1 [[C_1]], [[C_2]]
; CHECK-NEXT: br i1 [[AND]], label [[BB1:%.*]], label [[EXIT:%.*]]
; CHECK: bb1:
; CHECK-NEXT: [[T_1:%.*]] = icmp ule i32 [[X]], [[Z]]
; CHECK-NEXT: call void @use(i1 true)
; CHECK-NEXT: [[T_2:%.*]] = icmp ule i32 [[X]], [[Y]]
; CHECK-NEXT: call void @use(i1 true)
; CHECK-NEXT: [[T_3:%.*]] = icmp ule i32 [[Y]], [[Z]]
; CHECK-NEXT: call void @use(i1 true)
; CHECK-NEXT: [[C_3:%.*]] = icmp ule i32 [[X]], [[A:%.*]]
; CHECK-NEXT: call void @use(i1 [[C_3]])
; CHECK-NEXT: ret i32 10
; CHECK-NEXT: [[T_1:%.*]] = icmp ule i4 [[X]], [[Z]]
; CHECK-NEXT: [[T_2:%.*]] = icmp ule i4 [[X]], [[Y]]
; CHECK-NEXT: [[R_1:%.*]] = xor i1 true, true
; CHECK-NEXT: [[T_3:%.*]] = icmp ule i4 [[Y]], [[Z]]
; CHECK-NEXT: [[R_2:%.*]] = xor i1 [[R_1]], true
; CHECK-NEXT: [[C_3:%.*]] = icmp ule i4 [[X]], [[A:%.*]]
; CHECK-NEXT: [[R_3:%.*]] = xor i1 [[R_2]], [[C_3]]
; CHECK-NEXT: ret i1 [[R_3]]
; CHECK: exit:
; CHECK-NEXT: [[C_4:%.*]] = icmp ule i32 [[X]], [[Z]]
; CHECK-NEXT: call void @use(i1 [[C_4]])
; CHECK-NEXT: [[C_5:%.*]] = icmp ule i32 [[X]], [[A]]
; CHECK-NEXT: call void @use(i1 [[C_5]])
; CHECK-NEXT: [[C_6:%.*]] = icmp ule i32 [[X]], [[Y]]
; CHECK-NEXT: call void @use(i1 [[C_6]])
; CHECK-NEXT: [[C_7:%.*]] = icmp ule i32 [[Y]], [[Z]]
; CHECK-NEXT: call void @use(i1 [[C_7]])
; CHECK-NEXT: ret i32 20
; CHECK-NEXT: [[C_4:%.*]] = icmp ule i4 [[X]], [[Z]]
; CHECK-NEXT: [[C_5:%.*]] = icmp ule i4 [[X]], [[A]]
; CHECK-NEXT: [[R_4:%.*]] = xor i1 [[C_4]], [[C_5]]
; CHECK-NEXT: [[C_6:%.*]] = icmp ule i4 [[X]], [[Y]]
; CHECK-NEXT: [[R_5:%.*]] = xor i1 [[R_4]], [[C_6]]
; CHECK-NEXT: [[C_7:%.*]] = icmp ule i4 [[Y]], [[Z]]
; CHECK-NEXT: [[R_6:%.*]] = xor i1 [[R_5]], [[C_7]]
; CHECK-NEXT: ret i1 [[R_6]]
;
entry:
%c.1 = icmp ule i32 %x, %y
%c.2 = icmp ule i32 %y, %z
%c.1 = icmp ule i4 %x, %y
%c.2 = icmp ule i4 %y, %z
%and = and i1 %c.1, %c.2
br i1 %and, label %bb1, label %exit

bb1:
%t.1 = icmp ule i32 %x, %z
call void @use(i1 %t.1)
%t.1 = icmp ule i4 %x, %z
%t.2 = icmp ule i4 %x, %y
%r.1 = xor i1 %t.1, %t.2

%t.2 = icmp ule i32 %x, %y
call void @use(i1 %t.2)
%t.3 = icmp ule i4 %y, %z
%r.2 = xor i1 %r.1, %t.3

%t.3 = icmp ule i32 %y, %z
call void @use(i1 %t.3)

%c.3 = icmp ule i4 %x, %a
%r.3 = xor i1 %r.2, %c.3

%c.3 = icmp ule i32 %x, %a
call void @use(i1 %c.3)

ret i32 10
ret i1 %r.3

exit:
%c.4 = icmp ule i32 %x, %z
call void @use(i1 %c.4)

%c.5 = icmp ule i32 %x, %a
call void @use(i1 %c.5)
%c.4 = icmp ule i4 %x, %z
%c.5 = icmp ule i4 %x, %a
%r.4 = xor i1 %c.4, %c.5

%c.6 = icmp ule i32 %x, %y
call void @use(i1 %c.6)
%c.6 = icmp ule i4 %x, %y
%r.5 = xor i1 %r.4, %c.6

%c.7 = icmp ule i32 %y, %z
call void @use(i1 %c.7)
%c.7 = icmp ule i4 %y, %z
%r.6 = xor i1 %r.5, %c.7

ret i32 20
ret i1 %r.6
}

; The result of test_and_ule and test_and_select_ule should be same
define i32 @test_and_select_ule(i32 %x, i32 %y, i32 %z, i32 %a) {
define i1 @test_and_select_ule(i4 %x, i4 %y, i4 %z, i4 %a) {
; CHECK-LABEL: @test_and_select_ule(
; CHECK-NEXT: entry:
; CHECK-NEXT: [[C_1:%.*]] = icmp ule i32 [[X:%.*]], [[Y:%.*]]
; CHECK-NEXT: [[C_2:%.*]] = icmp ule i32 [[Y]], [[Z:%.*]]
; CHECK-NEXT: [[C_1:%.*]] = icmp ule i4 [[X:%.*]], [[Y:%.*]]
; CHECK-NEXT: [[C_2:%.*]] = icmp ule i4 [[Y]], [[Z:%.*]]
; CHECK-NEXT: [[AND:%.*]] = select i1 [[C_1]], i1 [[C_2]], i1 false
; CHECK-NEXT: br i1 [[AND]], label [[BB1:%.*]], label [[EXIT:%.*]]
; CHECK: bb1:
; CHECK-NEXT: [[T_1:%.*]] = icmp ule i32 [[X]], [[Z]]
; CHECK-NEXT: call void @use(i1 true)
; CHECK-NEXT: [[T_2:%.*]] = icmp ule i32 [[X]], [[Y]]
; CHECK-NEXT: call void @use(i1 true)
; CHECK-NEXT: [[T_3:%.*]] = icmp ule i32 [[Y]], [[Z]]
; CHECK-NEXT: call void @use(i1 true)
; CHECK-NEXT: [[C_3:%.*]] = icmp ule i32 [[X]], [[A:%.*]]
; CHECK-NEXT: call void @use(i1 [[C_3]])
; CHECK-NEXT: ret i32 10
; CHECK-NEXT: [[T_1:%.*]] = icmp ule i4 [[X]], [[Z]]
; CHECK-NEXT: [[T_2:%.*]] = icmp ule i4 [[X]], [[Y]]
; CHECK-NEXT: [[R_1:%.*]] = xor i1 true, true
; CHECK-NEXT: [[T_3:%.*]] = icmp ule i4 [[Y]], [[Z]]
; CHECK-NEXT: [[R_2:%.*]] = xor i1 [[R_1]], true
; CHECK-NEXT: [[C_3:%.*]] = icmp ule i4 [[X]], [[A:%.*]]
; CHECK-NEXT: [[R_3:%.*]] = xor i1 [[R_2]], [[C_3]]
; CHECK-NEXT: ret i1 [[R_3]]
; CHECK: exit:
; CHECK-NEXT: [[C_4:%.*]] = icmp ule i32 [[X]], [[Z]]
; CHECK-NEXT: call void @use(i1 [[C_4]])
; CHECK-NEXT: [[C_5:%.*]] = icmp ule i32 [[X]], [[A]]
; CHECK-NEXT: call void @use(i1 [[C_5]])
; CHECK-NEXT: [[C_6:%.*]] = icmp ule i32 [[X]], [[Y]]
; CHECK-NEXT: call void @use(i1 [[C_6]])
; CHECK-NEXT: [[C_7:%.*]] = icmp ule i32 [[Y]], [[Z]]
; CHECK-NEXT: call void @use(i1 [[C_7]])
; CHECK-NEXT: ret i32 20
; CHECK-NEXT: [[C_4:%.*]] = icmp ule i4 [[X]], [[Z]]
; CHECK-NEXT: [[C_5:%.*]] = icmp ule i4 [[X]], [[A]]
; CHECK-NEXT: [[R_4:%.*]] = xor i1 [[C_4]], [[C_5]]
; CHECK-NEXT: [[C_6:%.*]] = icmp ule i4 [[X]], [[Y]]
; CHECK-NEXT: [[R_5:%.*]] = xor i1 [[R_4]], [[C_6]]
; CHECK-NEXT: [[C_7:%.*]] = icmp ule i4 [[Y]], [[Z]]
; CHECK-NEXT: [[R_6:%.*]] = xor i1 [[R_5]], [[C_7]]
; CHECK-NEXT: ret i1 [[R_6]]
;
entry:
%c.1 = icmp ule i32 %x, %y
%c.2 = icmp ule i32 %y, %z
%c.1 = icmp ule i4 %x, %y
%c.2 = icmp ule i4 %y, %z
%and = select i1 %c.1, i1 %c.2, i1 false
br i1 %and, label %bb1, label %exit

bb1:
%t.1 = icmp ule i32 %x, %z
call void @use(i1 %t.1)

%t.2 = icmp ule i32 %x, %y
call void @use(i1 %t.2)

%t.3 = icmp ule i32 %y, %z
call void @use(i1 %t.3)
%t.1 = icmp ule i4 %x, %z
%t.2 = icmp ule i4 %x, %y
%r.1 = xor i1 %t.1, %t.2

%t.3 = icmp ule i4 %y, %z
%r.2 = xor i1 %r.1, %t.3

%c.3 = icmp ule i32 %x, %a
call void @use(i1 %c.3)

ret i32 10
%c.3 = icmp ule i4 %x, %a
%r.3 = xor i1 %r.2, %c.3
ret i1 %r.3

exit:
%c.4 = icmp ule i32 %x, %z
call void @use(i1 %c.4)

%c.5 = icmp ule i32 %x, %a
call void @use(i1 %c.5)

%c.6 = icmp ule i32 %x, %y
call void @use(i1 %c.6)
%c.4 = icmp ule i4 %x, %z
%c.5 = icmp ule i4 %x, %a
%r.4 = xor i1 %c.4, %c.5

%c.7 = icmp ule i32 %y, %z
call void @use(i1 %c.7)
%c.6 = icmp ule i4 %x, %y
%r.5 = xor i1 %r.4, %c.6

ret i32 20
%c.7 = icmp ule i4 %y, %z
%r.6 = xor i1 %r.5, %c.7
ret i1 %r.6
}

define i4 @and_compare_undef(i16 %N, i16 %step) {
define i4 @and_compare_undef(i4 %N, i4 %step) {
; CHECK-LABEL: @and_compare_undef(
; CHECK-NEXT: step.check:
; CHECK-NEXT: [[STEP_POS:%.*]] = icmp uge i16 [[STEP:%.*]], 0
; CHECK-NEXT: [[B1:%.*]] = add i16 undef, -1
; CHECK-NEXT: [[STEP_ULT_N:%.*]] = icmp ult i16 [[B1]], [[N:%.*]]
; CHECK-NEXT: [[STEP_POS:%.*]] = icmp uge i4 [[STEP:%.*]], 0
; CHECK-NEXT: [[B1:%.*]] = add i4 undef, -1
; CHECK-NEXT: [[STEP_ULT_N:%.*]] = icmp ult i4 [[B1]], [[N:%.*]]
; CHECK-NEXT: [[AND_STEP:%.*]] = and i1 [[STEP_POS]], [[STEP_ULT_N]]
; CHECK-NEXT: br i1 [[AND_STEP]], label [[PTR_CHECK:%.*]], label [[EXIT:%.*]]
; CHECK: ptr.check:
Expand All @@ -150,9 +135,9 @@ define i4 @and_compare_undef(i16 %N, i16 %step) {
; CHECK-NEXT: ret i4 3
;
step.check:
%step.pos = icmp uge i16 %step, 0
%B1 = add i16 undef, -1
%step.ult.N = icmp ult i16 %B1, %N
%step.pos = icmp uge i4 %step, 0
%B1 = add i4 undef, -1
%step.ult.N = icmp ult i4 %B1, %N
%and.step = and i1 %step.pos, %step.ult.N
br i1 %and.step, label %ptr.check, label %exit

Expand Down
41 changes: 17 additions & 24 deletions llvm/test/Transforms/ConstraintElimination/decompose-with-temporary-indices.ll
View file
Expand Up @@ -4,7 +4,7 @@
declare void @use(i1)


define void @test_uge_temporary_indices_decompose(i8 %start, i8 %n, i8 %idx) {
define i1 @test_uge_temporary_indices_decompose(i8 %start, i8 %n, i8 %idx) {
; CHECK-LABEL: @test_uge_temporary_indices_decompose(
; CHECK-NEXT: entry:
; CHECK-NEXT: [[CMP_PRE:%.*]] = icmp ult i8 [[IDX:%.*]], [[N:%.*]]
Expand All @@ -14,24 +14,22 @@ define void @test_uge_temporary_indices_decompose(i8 %start, i8 %n, i8 %idx) {
; CHECK-NEXT: br i1 [[CMP_PRE]], label [[IF_THEN:%.*]], label [[IF_END:%.*]]
; CHECK: if.then:
; CHECK-NEXT: [[T_0:%.*]] = icmp ult i8 [[START_ADD_IDX]], [[START_ADD_N]]
; CHECK-NEXT: call void @use(i1 true)
; CHECK-NEXT: [[F_0:%.*]] = icmp uge i8 [[START_ADD_IDX]], [[START_ADD_N]]
; CHECK-NEXT: call void @use(i1 false)
; CHECK-NEXT: [[R_1:%.*]] = xor i1 true, false
; CHECK-NEXT: [[C_1:%.*]] = icmp ult i8 [[START_ADD_1]], [[START_ADD_N]]
; CHECK-NEXT: call void @use(i1 [[C_1]])
; CHECK-NEXT: [[R_2:%.*]] = xor i1 [[R_1]], [[C_1]]
; CHECK-NEXT: [[C_2:%.*]] = icmp ult i8 [[START_ADD_IDX]], [[START_ADD_1]]
; CHECK-NEXT: call void @use(i1 [[C_2]])
; CHECK-NEXT: ret void
; CHECK-NEXT: [[R_3:%.*]] = xor i1 [[R_2]], [[C_2]]
; CHECK-NEXT: ret i1 [[R_3]]
; CHECK: if.end:
; CHECK-NEXT: [[F_1:%.*]] = icmp ult i8 [[START_ADD_IDX]], [[START_ADD_N]]
; CHECK-NEXT: call void @use(i1 false)
; CHECK-NEXT: [[T_1:%.*]] = icmp uge i8 [[START_ADD_IDX]], [[START_ADD_N]]
; CHECK-NEXT: call void @use(i1 true)
; CHECK-NEXT: [[R_4:%.*]] = xor i1 false, true
; CHECK-NEXT: [[C_3:%.*]] = icmp ult i8 [[START_ADD_1]], [[START_ADD_N]]
; CHECK-NEXT: call void @use(i1 [[C_3]])
; CHECK-NEXT: [[R_5:%.*]] = xor i1 [[R_4]], [[C_3]]
; CHECK-NEXT: [[C_4:%.*]] = icmp ult i8 [[START_ADD_IDX]], [[START_ADD_1]]
; CHECK-NEXT: call void @use(i1 [[C_4]])
; CHECK-NEXT: ret void
; CHECK-NEXT: [[R_6:%.*]] = xor i1 [[R_5]], [[C_4]]
; CHECK-NEXT: ret i1 [[R_6]]
;
entry:
%cmp.pre = icmp ult i8 %idx, %n
Expand All @@ -42,32 +40,27 @@ entry:

if.then: ; preds = %entry
%t.0 = icmp ult i8 %start.add.idx, %start.add.n
call void @use(i1 %t.0)

%f.0 = icmp uge i8 %start.add.idx, %start.add.n
call void @use(i1 %f.0)
%r.1 = xor i1 %t.0, %f.0

%c.1 = icmp ult i8 %start.add.1, %start.add.n
call void @use(i1 %c.1)
%r.2 = xor i1 %r.1, %c.1

%c.2 = icmp ult i8 %start.add.idx, %start.add.1
call void @use(i1 %c.2)

ret void
%r.3 = xor i1 %r.2, %c.2
ret i1 %r.3


if.end: ; preds = %entry
%f.1 = icmp ult i8 %start.add.idx, %start.add.n
call void @use(i1 %f.1)

%t.1 = icmp uge i8 %start.add.idx, %start.add.n
call void @use(i1 %t.1)
%r.4 = xor i1 %f.1, %t.1

%c.3 = icmp ult i8 %start.add.1, %start.add.n
call void @use(i1 %c.3)
%r.5 = xor i1 %r.4, %c.3

%c.4 = icmp ult i8 %start.add.idx, %start.add.1
call void @use(i1 %c.4)
%r.6 = xor i1 %r.5, %c.4

ret void
ret i1 %r.6
}

0 comments on commit 0bcfd4c

Please sign in to comment.