|
|
|
|
|
|
|
|
|
|
|
|
| |
CompCert currently uses `Instance` in so-called "refine" mode, where
Coq drops automatically in proof mode if some members of the instance
are missing.
This mode is soon going to be turned off by default, see
https://github.com/coq/coq/pull/9270.
In order to make CompCert robust against this change, this commit
replaces those occurrences of `Instance` that use "refine" mode
with `Program Instance`.
|
|
This framework follows "approach A" from the paper "Lightweight Verification of Separate Compilation" by Kang, Kim, Hur, Dreyer and Vafeiadis, POPL 2016.
Syntactic linking (of compilation units and their syntactic elements) is modeled by a type class with two components:
- a partial binary operation "link" that returns the syntactic element corresponding to the act of linking together its two arguments. It may fail if the two arguments cannot be linked, e.g. are incompatible definitions of the same name.
- a partial order "linkorder x y" that holds if "x" is a sub-unit of a whole program or bigger unit "y", or in other words, if "y" can be obtained by linking "x" with other units.
Instances of this type class are provided for the type AST.program and its syntactic elements (globvar, globdef, etc).
The "match_program" predicate that provides a relational characterization of compiler passes / program transformations is extended to account for context-dependent transformations and separate compilation: the transformation of a function definition can depend on the compilation unit it occurs in (this is the context), and this compilation unit "ctx" is characterized as any unit that is in the "linkorder ctx prog" relation with the whole source program "prog".
Under mild hypotheses, we show that "match_program" commutes with linking: if a1 matches b1, a2 matches b2, and a1 and a2 link together producing a, then b1 and b2 link together, producing a b that matches a.
Finally, we extend binary linking to linking of a nonempty list of compilation units; commutation with "match_program" still holds.
|