A Concrete Memory Model for CompCert

被引：14

作者：

Besson, Frederic ^{[1
]}

Blazy, Sandrine ^{[2
]}

Wilke, Pierre ^{[2
]}

机构：

[1] INRIA, Rennes, France

[2] Univ Rennes 1, IRISA, Rennes, France

来源：

INTERACTIVE THEOREM PROVING | 2015年 / 9236卷

关键词：

FORMAL VERIFICATION;

D O I：

10.1007/978-3-319-22102-1_5

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Semantics preserving compilation of low-level C programs is challenging because their semantics is implementation defined according to the C standard. This paper presents the proof of an enhanced and more concrete memory model for the CompCert C compiler which assigns a definite meaning to more C programs. In our new formally verified memory model, pointers are still abstract but are nonetheless mapped to concrete 32-bit integers. Hence, the memory is finite and it is possible to reason about the binary encoding of pointers. We prove that the existing memory model is an abstraction of our more concrete model thus validating formally the soundness of CompCert's abstract semantics of pointers. We also show how to adapt the front-end of CompCert thus demonstrating that it should be feasible to port the whole compiler to our novel memory model.

引用

页码：67 / 83

页数：17

共 22 条

[11]

Jourdan Jacques-Henri, 2015, POPL

[12]

Kang J., 2015, PLDI

[13]

Krebbers Robbert, 2014, Interactive Theorem Proving. 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014. Proceedings: LNCS 8558, P543, DOI 10.1007/978-3-319-08970-6_36

[14]

Krebbers R, 2014, POPL

[15]

Krebbers R, 2013, LECT NOTES COMPUT SC, V8307, P50, DOI 10.1007/978-3-319-03545-1_4

[16] Formal verification of a C-like memory model and its uses for verifying program transformations [J].