inbounds관련 load-store 예제 수정

aqjune commented 8 years ago

기존의 최적화는 제대로 검산이 될 수 없는 예제라 판정되어서, 검산이 될 수 있는 예제로 수정했습니다.

jeehoonkang commented 8 years ago

"제대로 검산이 될 수 없는 예제라 판정" 이게 옳음에도 불구하고 우리가 검산할 수 없는건가요? 아니면 틀린 최적화인가요?

aqjune commented 8 years ago

저는 틀린 최적화라고 생각했습니다. 이 예제는 아래와 같이 최적화 됩니다.

<source>
%p = getelementptr inbounds %struct.ST, %struct.ST* %s, i64 1, i32 2, i32 1, i64 5, i64 13
%q = getelementptr %struct.ST, %struct.ST* %s, i64 1, i32 2, i32 1, i64 5, i64 13
store i32 3, i32* %p
 %z = load i32, i32* %q
ret %z
----
<target>
%p = getelementptr inbounds %struct.ST, %struct.ST* %s, i64 1, i32 2, i32 1, i64 5, i64 13
%q = getelementptr %struct.ST, %struct.ST* %s, i64 1, i32 2, i32 1, i64 5, i64 13
store i32 3, i32* %p
%z = load i32, i32 *%q
ret 3

%z의 user에서 %z를 3으로 바꾸는 근거는, 해당 InstCombine 최적화에서 %p와 %q가 같은 주소라고 판단하기 때문입니다.

문제가 되는 이유는 아래와 같습니다. 먼저, %z를 3으로 바꾸기 위해서는 %z >= 3 이 필요 합니다. %z >= 3을 만들기 위해 store 문장에서 (load %p) >= 3와 load 문장에서 %z >= (load %q) 를 transitivity로 묶어야 하는데, 두 식을 이어주는 load %q >= load %p 를 만들기 위해서는 %q >= %p 가 필요합니다. 그런데 이 예제에서는 %p는 undef(더 정확히는 poison)가 될 수 있지만 %q는 undef가 되지 않기 때문에 %q >= %p가 성립할 수 없습니다.

aqjune commented 8 years ago

위 최적화는 확인해 보니 옳은 것이고(이유는 store에서 어짜피 UB가 생길 것이기 때문), 다만 증명을 어떻게 할지를 몰랐었는데 지훈이형께서 방향을 제시해 주셨습니다 일단 이 PR이 merge 되기 위해서, 제가 문제가 되었다고 생각되었던 최적화 예제 파일도 추가를 했습니다.

aqjune commented 8 years ago

이 예제 관련해서 생각하던 것이 있는데, 내일 오전 중에 간단히 질문드리고자 합니다.

aqjune commented 8 years ago

이전에 지훈이형이 이야기하셨던 것이, invariant에 load ty %ptr >= %x가 있을 때 이것의 의미가 제대로 정의되어 있지 않고, 정의를 해야 한다면 아래와 같이 두 가지 중 하나를 하면 좋겠다고 하셨습니다. (1) (%ptr로 메모리 접근이 성공) && (%ptr을 로드한 값 >= %x) (2) (%ptr로 메모리 접근이 성공) -> (%ptr을 로드한 값 >= %x)

이에 대한 제 생각은, 우리는 은연중에 (1)를 load ty %ptr >= %x의 정의로 사용해 오고 있었던 것 같고, 따라서 (1)을 계속 사용하면 좋을 것 같다는 것입니다.

(1)을 정의로 생각했던 이유는 아래와 같습니다.

(2)를 택할 경우 transitivity rule이 문제가 될 수 있습니다. %x >= load ty %ptr 이고 load ty %ptr >= %y일 때 transitivity를 적용한 %x >= %y는 의미가 "%ptr이 load에 성공했을 때 %x >= %y이다"가 되어야 하는데, 이는 지금 transitivity의 정의와 맞지 않습니다.
만약 (2)를 택하게 된다면, noalias를 계산하거나 하는 곳에서 "%ptr로 메모리 접근이 성공함"이라는 별도의 invariant를 활용하고 있었어야 합니다. (마치 %ptr alloca invariant 처럼..)
IR의 %x = load ty %ptr의 post condition이 "%ptr로 메모리 접근이 성공함"이라는 invariant도 생성을 해 주어야 했다고 생각합니다. (그리고 "메모리 접근 성공" invariant는 사실 이 순간에 만들어 주지 않으면 다른 때 만들어줄 때가 별로 없을 것 같습니다..)

후에 여유 있으실 때 답글 주셔요..!

aqjune commented 8 years ago

이 주제에 대해서 다음주중에 정리를 한 다음 다시 revisit하도록 하겠습니다.

aqjune commented 8 years ago

inbounds를 없애는 방향과 추가하는 방향 둘 다 검증할 수 있도록 inference rule들을 추가를 했습니다. (https://github.com/snu-sf/llvmberry/pull/329) 329 PR이 merge될 때 이것도 merge하도록 하겠습니다.

aqjune commented 8 years ago

Inbounds를 없애는 것은 확인을 받았으므로 이 테스트케이스는 머지하도록 하겠습니다.

오타 정정합니다. 없애는 것 -> 추가하는 것

snu-sf / crellvm-tests

inbounds관련 load-store 예제 수정 #59