Derived rules and proof automation for C light
Andrew W. Appel · Cambridge University Press eBooks · 2014
F or 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 π τ v 1 v 2 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 , v 1 is a pointer to a struct of type τ, and the heaplet contains exactly v 1 + δ v 2 , (value v 2 at address v 1 + δ with permission-share π), where v 2 : τ 2 .