Name
Abstract | ||
|---|---|---|
Systems code often requires fine-grained control over memory layout and pointers, expressed using low-level (e.g., bitwise) operations on pointer values. Since these operations go beyond what basic pointer arithmetic in C allows, they are performed with the help of integer-pointer casts. Prior work has explored increasingly realistic memory object models for C that account for the desired semantics of integer-pointer casts while also being sound w.r.t. compiler optimisations, culminating in PNVI-ae-udi, the preferred memory object model in ongoing discussions within the ISO WG14 C standards committee. However, its complexity makes it an unappealing target for verification, and no tools currently exist to verify C programs under PNVI-ae-udi. In this paper, we introduce VIP, a newmemory object model aimed at supporting C verification. VIP sidesteps the complexities of PNVI-ae-udi with a simple but effective idea: a new construct that lets programmers express the intended provenances of integer-pointer casts explicitly. At the same time, we prove VIP compatible with PNVI-ae-udi, thus enabling verification on top of VIP to benefit from PNVI-ae-udi's validation with respect to practice. In particular, we build a verification tool, RefinedC-VIP, for verifying programs under VIP semantics. As the name suggests, RefinedC-VIP extends the recently developed RefinedC tool, which is automated yet also produces foundational proofs in Coq. We evaluate RefinedC-VIP on a range of systems-code idioms, and validate VIP's expressiveness via an implementation in the Cerberus C semantics. |
Year | DOI | Venue |
|---|---|---|
2022 | 10.1145/3498681 | PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL |
Keywords | DocType | Volume |
C programming language, memory model, pointer provenance, separation logic, proof automation, Iris, Coq | Journal | 6 |
Issue | Citations | PageRank |
POPL | 0 | 0.34 |
References | Authors | |
0 | 6 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Rodolphe Lepigre | 1 | 0 | 0.34 |
| Michael Sammler | 2 | 3 | 2.10 |
| Kayvan Memarian | 3 | 0 | 0.34 |
| Robbert Krebbers | 4 | 0 | 1.01 |
| Derek Dreyer | 5 | 0 | 0.34 |
| Peter Sewell | 6 | 0 | 0.34 |