snu-sf/CompCert

Update the final theorem for Part II

Closed this issue · 5 comments

jeehoonkang commented
  • Part I's final theorem says: if c1 and c2 are compiled by CompCert into a1 and a2, a1+a2 refines c1+c2.
  • Part II generalizes the result. Now CompCert can perform arbitrary number of intra-RTL optimizations. For this, we updated (and will update) correctness theorem for each intra-RTL optimization.
  • The last step is:
    • define the "new" CompCert
    • define the compilation relation for the new CompCert
    • state the final theorem for the new CompCert
    • prove it.

We have to do the last step. I guess this is mainly plumbing existing things. @kim-yoonseung , let's discuss how to design it; and then you will implement and prove it :-)

jeehoonkang commented

compiled cprog asmprog =

c2rtl cprog rtl
optimized rtl ortl
rtl2asm ortl asmprog

rtl1 rtl2
ortl1 rtl2
ortl1 ortl2

induciton on (H:optimized rtl1 ortl1)

jeehoonkang commented

exists (asmprog:Asm.program)
(_:backward_simulation (Csem.semantics cprog) (Asm.semantics asmprog)),
Tree.reduce (link_program Language_Asm) asmtree = Some asmprog.

forward simulation from Cstrategy to Asm
backward simulation from Csem to Asm

Csem - Cstrategy - Clight - ...

foo(e1, e2)

kim-yoonseung commented

#5 의 pull request에서 받은 코멘트에 대한 수정과, Csem에서부터 backward simulation으로 Asm까지 가는 증명을 완료했습니다.

jeehoonkang commented

I code-reviewed; please see the comments.

Jeehoon