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.

0 files changed, 0 insertions, 0 deletions