Book contents
- Frontmatter
- Dedication
- Contents
- Road map
- Acknowledgments
- 1 Introduction
- I Generic separation logic
- II Higher order separation logic
- III Separation logic for CompCert
- 22 Verifiable C
- 23 Expressions, values, and assertions
- 24 The VST separation logic for C light
- 25 Typechecking for Verifiable C
- 26 Derived rules and proof automation for C light
- 27 Proof of a program
- 28 More C programs
- 29 Dependently typed C programs
- 30 Concurrent separation logic
- IV Operational semantics of CompCert
- V Higher-order semantic models
- VI Semantic model and soundness of Verifiable C
- VII Applications
- Bibliography
- Index
26 - Derived rules and proof automation for C light
from III - Separation logic for CompCert
Published online by Cambridge University Press: 05 August 2014
- Frontmatter
- Dedication
- Contents
- Road map
- Acknowledgments
- 1 Introduction
- I Generic separation logic
- II Higher order separation logic
- III Separation logic for CompCert
- 22 Verifiable C
- 23 Expressions, values, and assertions
- 24 The VST separation logic for C light
- 25 Typechecking for Verifiable C
- 26 Derived rules and proof automation for C light
- 27 Proof of a program
- 28 More C programs
- 29 Dependently typed C programs
- 30 Concurrent separation logic
- IV Operational semantics of CompCert
- V Higher-order semantic models
- VI Semantic model and soundness of Verifiable C
- VII Applications
- Bibliography
- Index
Summary
For convenient application of the VST program logic for C light, we have synthetic or derived rules: lemmas built from common combinations of the primitive inference rules for C light. We also have proof automation: programs that look at proof goals and choose which rules to apply.
For example, consider the C-language statements x:=e→f; and e1→f := e2; where x is a variable, f is the name of a structure field, and e, e1, e2 are expressions. The first command is a load field statement, and the second is a store field. Proofs about these statements could be done using the general semax-load and semax-store rules—along with the mapsto operator—but these require a lot of reasoning about field l-values. It's best to define a synthetic field_mapsto predicate that can be used as if it were a primitive:
Definition field-mapsto (sh:share)(t1:type)(fld:ident)(v1 v2: val): mpred.
We do not show the definition here (see floyd/field_mapsto.v) but basically field_mapsto π τ v1v2 is a predicate meaning: τ is a struct type whose field f of type τ2 has address-offset δ from the base address of the struct; the size/signedness of f is ch, v1 is a pointer to a struct of type τ, and the heaplet contains exactly v1 + δ v2, (value v2 at address v1 + δ with permission-share π), where v2: τ2.
- Type
- Chapter
- Information
- Program Logics for Certified Compilers , pp. 184 - 194Publisher: Cambridge University PressPrint publication year: 2014