diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-03-06 09:59:32 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-03-06 09:59:32 +0100 |
commit | be2315351761e4fc0430b91ac791d66eec0e0cd7 (patch) | |
tree | d59874899157972a09c3141401912a720bb00f31 /test/cminor/marksweep.cmp | |
parent | fe55fe4397636e331fdbe7c2581b00e35bbec734 (diff) | |
download | compcert-be2315351761e4fc0430b91ac791d66eec0e0cd7.tar.gz compcert-be2315351761e4fc0430b91ac791d66eec0e0cd7.zip |
Globalenvs: adapt to new linking framework, and revise.
The commutation lemmas between program transformations and Genv operations now take separate compilation into account. For example:
Theorem find_funct_ptr_match:
forall b f,
find_funct_ptr (globalenv p) b = Some f ->
exists cunit tf,
find_funct_ptr (globalenv tp) b = Some tf
/\ match_fundef cunit f tf
/\ linkorder cunit ctx.
Note how "f" and "tf" are related wrt a compilation unit "cunit" which is not necessarily "ctx" (the context for the whole program), but can be a sub-unit of the this whole program.
The other changes in Globalenvs are a long-overdue refactoring and cleanup:
- Introduce Senv.equiv (extensional equivalence between two Senv.t) to collect (in one place) the invariance properties relevant to external functions (preservation of names, of public names, and of volatile blocks).
- Revise internal representation of Genv.t: one map ident -> globdef F V instead of two maps ident -> F and ident -> globvar V.
- More precise characterization of initial memory states: "Genv.init_mem_characterization" uniquely characterizes every byte (memval) of the representation of an initialized global variable.
- Necessary and sufficient conditions for the initial memory state to exist.
- Revised proofs about init_mem, especially init_mem_inject.
- Removed some Genv lemmas that were unused.
Diffstat (limited to 'test/cminor/marksweep.cmp')
0 files changed, 0 insertions, 0 deletions