[Assignment 5] Alive2 makes ERROR: Timeout

[jeongdaun]

Assignment 5에서 작성하는 pass를 통해 변환한 코드를 alive2의 alive-tv를 통해 원래 코드와 비교하였을때, check3.ll ~ check6.ll의 경우에 ERROR: Timeout이 발생하였습니다. 나머지 check들과 직접 만든 mycheck들은 정상적으로 동등성 검사가 완료되었습니다. 두 파일이 동등하거나 동등하지 않다는 결과가 아니라, Timeout이 발생하여 원인이 뭔지 파악이 힘들어 Issue를 작성하게 되었습니다.

아래는 check3.ll ~ check6.ll을 변환한 파일과 기존 파일을 alive-tv를 통해 비교한 결과입니다.

check3.ll

----------------------------------------
declare void @f(i32, i32)

define i32 @main(i32 %x, i32 %y) {
#0:
  %b = mul i32 %x, %y
  %a = add i32 %x, %y
  %cond = icmp eq i32 %a, %b
  br i1 %cond, label %bb_true, label %bb_false

bb_false:
  call void @f(i32 %a, i32 %b)
  br label %bb_exit

bb_true:
  call void @f(i32 %a, i32 %b)
  br label %bb_exit

bb_exit:
  call void @f(i32 %a, i32 %b)
  ret i32 %b
}
=>
declare void @f(i32, i32)

define i32 @main(i32 %x, i32 %y) {
#0:
  %b = mul i32 %x, %y
  %a = add i32 %x, %y
  %cond = icmp eq i32 %a, %b
  br i1 %cond, label %bb_true, label %bb_false

bb_false:
  call void @f(i32 %a, i32 %b)
  br label %bb_exit

bb_true:
  call void @f(i32 %b, i32 %b)
  br label %bb_exit

bb_exit:
  call void @f(i32 %a, i32 %b)
  ret i32 %b
}
ERROR: Timeout

Summary:
  0 correct transformations
  0 incorrect transformations
  1 failed-to-prove transformations
  0 Alive2 errors

check4.ll

----------------------------------------
declare void @f(i32, i32)

define i32 @main(i32 %x, i32 %y) {
#0:
  %a = add i32 %x, %y
  %b = mul i32 %x, %y
  %cond = icmp eq i32 %a, %b
  br i1 %cond, label %bb_true, label %bb_false

bb_false:
  call void @f(i32 %a, i32 %b)
  br label %bb_exit

bb_true:
  call void @f(i32 %a, i32 %b)
  br label %bb_exit

bb_exit:
  call void @f(i32 %a, i32 %b)
  ret i32 %b
}
=>
declare void @f(i32, i32)

define i32 @main(i32 %x, i32 %y) {
#0:
  %a = add i32 %x, %y
  %b = mul i32 %x, %y
  %cond = icmp eq i32 %a, %b
  br i1 %cond, label %bb_true, label %bb_false

bb_false:
  call void @f(i32 %a, i32 %b)
  br label %bb_exit

bb_true:
  call void @f(i32 %a, i32 %a)
  br label %bb_exit

bb_exit:
  call void @f(i32 %a, i32 %b)
  ret i32 %b
}
ERROR: Timeout

Summary:
  0 correct transformations
  0 incorrect transformations
  1 failed-to-prove transformations
  0 Alive2 errors

check5.ll

----------------------------------------
declare void @f(i32, i32)

define i32 @main(i32 %x, i32 %y, i32 %b) {
#0:
  %a = add i32 %x, %y
  %cond = icmp eq i32 %a, %b
  br i1 %cond, label %bb_true, label %bb_false

bb_false:
  call void @f(i32 %a, i32 %b)
  br label %bb_exit

bb_true:
  call void @f(i32 %a, i32 %b)
  br label %bb_exit

bb_exit:
  call void @f(i32 %a, i32 %b)
  ret i32 %b
}
=>
declare void @f(i32, i32)

define i32 @main(i32 %x, i32 %y, i32 %b) {
#0:
  %a = add i32 %x, %y
  %cond = icmp eq i32 %a, %b
  br i1 %cond, label %bb_true, label %bb_false

bb_false:
  call void @f(i32 %a, i32 %b)
  br label %bb_exit

bb_true:
  call void @f(i32 %b, i32 %b)
  br label %bb_exit

bb_exit:
  call void @f(i32 %a, i32 %b)
  ret i32 %b
}
ERROR: Timeout

Summary:
  0 correct transformations
  0 incorrect transformations
  1 failed-to-prove transformations
  0 Alive2 errors

check6.ll

----------------------------------------
declare void @f(i32, i32)

define i32 @main(i32 %x, i32 %y, i32 %b) {
#0:
  %a = add i32 %x, %y
  %cond = icmp eq i32 %b, %a
  br i1 %cond, label %bb_true, label %bb_false

bb_false:
  call void @f(i32 %a, i32 %b)
  br label %bb_exit

bb_true:
  call void @f(i32 %a, i32 %b)
  br label %bb_exit

bb_exit:
  call void @f(i32 %a, i32 %b)
  ret i32 %b
}
=>
declare void @f(i32, i32)

define i32 @main(i32 %x, i32 %y, i32 %b) {
#0:
  %a = add i32 %x, %y
  %cond = icmp eq i32 %b, %a
  br i1 %cond, label %bb_true, label %bb_false

bb_false:
  call void @f(i32 %a, i32 %b)
  br label %bb_exit

bb_true:
  call void @f(i32 %b, i32 %b)
  br label %bb_exit

bb_exit:
  call void @f(i32 %a, i32 %b)
  ret i32 %b
}
ERROR: Timeout

Summary:
  0 correct transformations
  0 incorrect transformations
  1 failed-to-prove transformations
  0 Alive2 errors

[strikef]

alive-tv에서 탐색해야 하는 범위가 저희 예상보다 많이 넓어서 발생하는 문제 같습니다. 탐색 범위를 줄이는 방향으로 테스트케이스 수정이 있을 예정입니다. 우선은 다른 테스트케이스가 통과하는지만 확인해주세요.

[strikef]

리포지토리에 수정된 테스트 파일들을 업데이트하였습니다.

다른 테스트와 비교해보았을 때, %a 와 %b가 각각 add와 mul의 결과라는 점이 alive-tv에 부하를 많이 가한 것으로 보입니다. alive-tv가 최적화 검산을 위해 사용하는 툴인 SMT solver는 휴리스틱을 이용해 쿼리의 많은 부분을 알아서 생략하고 최소한의 체크만으로 동등성을 확인이 가능한데, add와 mul로 인해 이 휴리스틱이 무력화되어 모든 경우의 수를 대입하며 계산하게 되어 타임아웃이 발생한 것입니다. 테스트의 로직을 바꾸지는 않고, 대신 자료형의 크기를 줄여서 탐색해야 할 경우의 수를 줄여 타임아웃이 발생하지 않도록 조치했습니다.