Library Globalenvs

Global environments are a component of the dynamic semantics of all languages involved in the compiler. A global environment maps symbol names (names of functions and of global variables) to the corresponding memory addresses. It also maps memory addresses of functions to the corresponding function descriptions.

Global environments, along with the initial memory state at the beginning of program execution, are built from the program of interest, as follows:

A distinct memory address is assigned to each function of the program. These function addresses use negative numbers to distinguish them from addresses of memory blocks. The associations of function name to function address and function address to function description are recorded in the global environment.
For each global variable, a memory block is allocated and associated to the name of the variable.

These operations reflect (at a high level of abstraction) what takes place during program linking and program loading in a real operating system.





Require Import Coqlib.

Require Import Errors.

Require Import Maps.

Require Import AST.

Require Import Integers.

Require Import Values.

Require Import Mem.




Set Implicit Arguments.




Module Type GENV.

Types and operations





  Variable t: Type -> Type.

The type of global environments. The parameter F is the type of function descriptions.





  Variable globalenv: forall (F V: Type), program F V -> t F.

Return the global environment for the given program.





  Variable init_mem: forall (F V: Type), program F V -> mem.

Return the initial memory state for the given program.





  Variable find_funct_ptr: forall (F: Type), t F -> block -> option F.

Return the function description associated with the given address, if any.





  Variable find_funct: forall (F: Type), t F -> val -> option F.

Same as find_funct_ptr but the function address is given as a value, which must be a pointer with offset 0.





  Variable find_symbol: forall (F: Type), t F -> ident -> option block.

Return the address of the given global symbol, if any.

Properties of the operations.





  Hypothesis find_funct_inv:

    forall (F: Type) (ge: t F) (v: val) (f: F),

    find_funct ge v = Some f -> exists b, v = Vptr b Int.zero.

  Hypothesis find_funct_find_funct_ptr:

    forall (F: Type) (ge: t F) (b: block),

    find_funct ge (Vptr b Int.zero) = find_funct_ptr ge b.




  Hypothesis find_symbol_exists:

    forall (F V: Type) (p: program F V)

           (id: ident) (init: list init_data) (v: V),

    In (id, init, v) (prog_vars p) ->

    exists b, find_symbol (globalenv p) id = Some b.

  Hypothesis find_funct_ptr_exists:

    forall (F V: Type) (p: program F V) (id: ident) (f: F),

    list_norepet (prog_funct_names p) ->

    list_disjoint (prog_funct_names p) (prog_var_names p) ->

    In (id, f) (prog_funct p) ->

    exists b, find_symbol (globalenv p) id = Some b

           /\ find_funct_ptr (globalenv p) b = Some f.




  Hypothesis find_funct_ptr_inversion:

    forall (F V: Type) (P: F -> Prop) (p: program F V) (b: block) (f: F),

    find_funct_ptr (globalenv p) b = Some f ->

    exists id, In (id, f) (prog_funct p).

  Hypothesis find_funct_inversion:

    forall (F V: Type) (P: F -> Prop) (p: program F V) (v: val) (f: F),

    find_funct (globalenv p) v = Some f ->

    exists id, In (id, f) (prog_funct p).

  Hypothesis find_funct_ptr_symbol_inversion:

    forall (F V: Type) (p: program F V) (id: ident) (b: block) (f: F),

    find_symbol (globalenv p) id = Some b ->

    find_funct_ptr (globalenv p) b = Some f ->

    In (id, f) p.(prog_funct).




  Hypothesis find_funct_ptr_prop:

    forall (F V: Type) (P: F -> Prop) (p: program F V) (b: block) (f: F),

    (forall id f, In (id, f) (prog_funct p) -> P f) ->

    find_funct_ptr (globalenv p) b = Some f ->

    P f.

  Hypothesis find_funct_prop:

    forall (F V: Type) (P: F -> Prop) (p: program F V) (v: val) (f: F),

    (forall id f, In (id, f) (prog_funct p) -> P f) ->

    find_funct (globalenv p) v = Some f ->

    P f.




  Hypothesis initmem_nullptr:

    forall (F V: Type) (p: program F V),

    let m := init_mem p in

    valid_block m nullptr /\

    m.(blocks) nullptr = empty_block 0 0.

  Hypothesis initmem_inject_neutral:

    forall (F V: Type) (p: program F V),

    mem_inject_neutral (init_mem p).

  Hypothesis find_funct_ptr_negative:

    forall (F V: Type) (p: program F V) (b: block) (f: F),

    find_funct_ptr (globalenv p) b = Some f -> b < 0.

  Hypothesis find_symbol_not_fresh:

    forall (F V: Type) (p: program F V) (id: ident) (b: block),

    find_symbol (globalenv p) id = Some b -> b < nextblock (init_mem p).

  Hypothesis find_symbol_not_nullptr:

    forall (F V: Type) (p: program F V) (id: ident) (b: block),

    find_symbol (globalenv p) id = Some b -> b <> nullptr.

  Hypothesis global_addresses_distinct:

    forall (F V: Type) (p: program F V) id1 id2 b1 b2,

    id1<>id2 ->

    find_symbol (globalenv p) id1 = Some b1 ->

    find_symbol (globalenv p) id2 = Some b2 ->

    b1<>b2.

Commutation properties between program transformations and operations over global environments.





  Hypothesis find_funct_ptr_transf:

    forall (A B V: Type) (transf: A -> B) (p: program A V),

    forall (b: block) (f: A),

    find_funct_ptr (globalenv p) b = Some f ->

    find_funct_ptr (globalenv (transform_program transf p)) b = Some (transf f).

  Hypothesis find_funct_transf:

    forall (A B V: Type) (transf: A -> B) (p: program A V),

    forall (v: val) (f: A),

    find_funct (globalenv p) v = Some f ->

    find_funct (globalenv (transform_program transf p)) v = Some (transf f).

  Hypothesis find_symbol_transf:

    forall (A B V: Type) (transf: A -> B) (p: program A V),

    forall (s: ident),

    find_symbol (globalenv (transform_program transf p)) s =

    find_symbol (globalenv p) s.

  Hypothesis init_mem_transf:

    forall (A B V: Type) (transf: A -> B) (p: program A V),

    init_mem (transform_program transf p) = init_mem p.

  Hypothesis find_funct_ptr_rev_transf:

    forall (A B V: Type) (transf: A -> B) (p: program A V),

    forall (b : block) (tf : B),

    find_funct_ptr (globalenv (transform_program transf p)) b = Some tf ->

    exists f : A, find_funct_ptr (globalenv p) b = Some f /\ transf f = tf.

  Hypothesis find_funct_rev_transf:

    forall (A B V: Type) (transf: A -> B) (p: program A V),

    forall (v : val) (tf : B),

    find_funct (globalenv (transform_program transf p)) v = Some tf ->

    exists f : A, find_funct (globalenv p) v = Some f /\ transf f = tf.

Commutation properties between partial program transformations and operations over global environments.





  Hypothesis find_funct_ptr_transf_partial:

    forall (A B V: Type) (transf: A -> res B) (p: program A V) (p': program B V),

    transform_partial_program transf p = OK p' ->

    forall (b: block) (f: A),

    find_funct_ptr (globalenv p) b = Some f ->

    exists f',

    find_funct_ptr (globalenv p') b = Some f' /\ transf f = OK f'.

  Hypothesis find_funct_transf_partial:

    forall (A B V: Type) (transf: A -> res B) (p: program A V) (p': program B V),

    transform_partial_program transf p = OK p' ->

    forall (v: val) (f: A),

    find_funct (globalenv p) v = Some f ->

    exists f',

    find_funct (globalenv p') v = Some f' /\ transf f = OK f'.

  Hypothesis find_symbol_transf_partial:

    forall (A B V: Type) (transf: A -> res B) (p: program A V) (p': program B V),

    transform_partial_program transf p = OK p' ->

    forall (s: ident),

    find_symbol (globalenv p') s = find_symbol (globalenv p) s.

  Hypothesis init_mem_transf_partial:

    forall (A B V: Type) (transf: A -> res B) (p: program A V) (p': program B V),

    transform_partial_program transf p = OK p' ->

    init_mem p' = init_mem p.

  Hypothesis find_funct_ptr_rev_transf_partial:

    forall (A B V: Type) (transf: A -> res B) (p: program A V) (p': program B V),

    transform_partial_program transf p = OK p' ->

    forall (b : block) (tf : B),

    find_funct_ptr (globalenv p') b = Some tf ->

    exists f : A,

      find_funct_ptr (globalenv p) b = Some f /\ transf f = OK tf.

  Hypothesis find_funct_rev_transf_partial:

    forall (A B V: Type) (transf: A -> res B) (p: program A V) (p': program B V),

    transform_partial_program transf p = OK p' ->

    forall (v : val) (tf : B),

    find_funct (globalenv p') v = Some tf ->

    exists f : A,

      find_funct (globalenv p) v = Some f /\ transf f = OK tf.




  Hypothesis find_funct_ptr_transf_partial2:

    forall (A B V W: Type) (transf_fun: A -> res B) (transf_var: V -> res W)

           (p: program A V) (p': program B W),

    transform_partial_program2 transf_fun transf_var p = OK p' ->

    forall (b: block) (f: A),

    find_funct_ptr (globalenv p) b = Some f ->

    exists f',

    find_funct_ptr (globalenv p') b = Some f' /\ transf_fun f = OK f'.

  Hypothesis find_funct_transf_partial2:

    forall (A B V W: Type) (transf_fun: A -> res B) (transf_var: V -> res W)

           (p: program A V) (p': program B W),

    transform_partial_program2 transf_fun transf_var p = OK p' ->

    forall (v: val) (f: A),

    find_funct (globalenv p) v = Some f ->

    exists f',

    find_funct (globalenv p') v = Some f' /\ transf_fun f = OK f'.

  Hypothesis find_symbol_transf_partial2:

    forall (A B V W: Type) (transf_fun: A -> res B) (transf_var: V -> res W)

           (p: program A V) (p': program B W),

    transform_partial_program2 transf_fun transf_var p = OK p' ->

    forall (s: ident),

    find_symbol (globalenv p') s = find_symbol (globalenv p) s.

  Hypothesis init_mem_transf_partial2:

    forall (A B V W: Type) (transf_fun: A -> res B) (transf_var: V -> res W)

           (p: program A V) (p': program B W),

    transform_partial_program2 transf_fun transf_var p = OK p' ->

    init_mem p' = init_mem p.

  Hypothesis find_funct_ptr_rev_transf_partial2:

    forall (A B V W: Type) (transf_fun: A -> res B) (transf_var: V -> res W)

           (p: program A V) (p': program B W),

    transform_partial_program2 transf_fun transf_var p = OK p' ->

    forall (b : block) (tf : B),

    find_funct_ptr (globalenv p') b = Some tf ->

    exists f : A,

      find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf.

  Hypothesis find_funct_rev_transf_partial2:

    forall (A B V W: Type) (transf_fun: A -> res B) (transf_var: V -> res W)

           (p: program A V) (p': program B W),

    transform_partial_program2 transf_fun transf_var p = OK p' ->

    forall (v : val) (tf : B),

    find_funct (globalenv p') v = Some tf ->

    exists f : A,

      find_funct (globalenv p) v = Some f /\ transf_fun f = OK tf.

Commutation properties between matching between programs and operations over global environments.





  Hypothesis find_funct_ptr_match:

    forall (A B V W: Type) (match_fun: A -> B -> Prop)

           (match_var: V -> W -> Prop) (p: program A V) (p': program B W),

    match_program match_fun match_var p p' ->

    forall (b : block) (f : A),

    find_funct_ptr (globalenv p) b = Some f ->

    exists tf : B,

    find_funct_ptr (globalenv p') b = Some tf /\ match_fun f tf.

  Hypothesis find_funct_ptr_rev_match:

    forall (A B V W: Type) (match_fun: A -> B -> Prop)

           (match_var: V -> W -> Prop) (p: program A V) (p': program B W),

    match_program match_fun match_var p p' ->

    forall (b : block) (tf : B),

    find_funct_ptr (globalenv p') b = Some tf ->

    exists f : A,

    find_funct_ptr (globalenv p) b = Some f /\ match_fun f tf.

  Hypothesis find_funct_match:

    forall (A B V W: Type) (match_fun: A -> B -> Prop)

           (match_var: V -> W -> Prop) (p: program A V) (p': program B W),

    match_program match_fun match_var p p' ->

    forall (v : val) (f : A),

    find_funct (globalenv p) v = Some f ->

    exists tf : B, find_funct (globalenv p') v = Some tf /\ match_fun f tf.

  Hypothesis find_funct_rev_match:

    forall (A B V W: Type) (match_fun: A -> B -> Prop)

           (match_var: V -> W -> Prop) (p: program A V) (p': program B W),

    match_program match_fun match_var p p' ->

    forall (v : val) (tf : B),

    find_funct (globalenv p') v = Some tf ->

    exists f : A, find_funct (globalenv p) v = Some f /\ match_fun f tf.

  Hypothesis find_symbol_match:

    forall (A B V W: Type) (match_fun: A -> B -> Prop)

           (match_var: V -> W -> Prop) (p: program A V) (p': program B W),

    match_program match_fun match_var p p' ->

    forall (s : ident),

    find_symbol (globalenv p') s = find_symbol (globalenv p) s.

  Hypothesis init_mem_match:

    forall (A B V W: Type) (match_fun: A -> B -> Prop)

           (match_var: V -> W -> Prop) (p: program A V) (p': program B W),

    match_program match_fun match_var p p' ->

    init_mem p' = init_mem p.




End GENV.

The rest of this library is a straightforward implementation of the module signature above.





Module Genv: GENV.




Section GENV.




Variable F: Type. 

Variable V: Type. 

Record genv : Type := mkgenv {

  functions: ZMap.t (option F);       nextfunction: Z;

  symbols: PTree.t block                }.




Definition t := genv.




Definition add_funct (name_fun: (ident * F)) (g: genv) : genv :=

  let b := g.(nextfunction) in

  mkgenv (ZMap.set b (Some (snd name_fun)) g.(functions))

         (Zpred b)

         (PTree.set (fst name_fun) b g.(symbols)).




Definition add_symbol (name: ident) (b: block) (g: genv) : genv :=

  mkgenv g.(functions)

         g.(nextfunction)

         (PTree.set name b g.(symbols)).




Definition find_funct_ptr (g: genv) (b: block) : option F :=

  ZMap.get b g.(functions).




Definition find_funct (g: genv) (v: val) : option F :=

  match v with

  | Vptr b ofs =>

      if Int.eq ofs Int.zero then find_funct_ptr g b else None

  | _ =>

      None

  end.




Definition find_symbol (g: genv) (symb: ident) : option block :=

  PTree.get symb g.(symbols).




Lemma find_funct_inv:

  forall (ge: t) (v: val) (f: F),

  find_funct ge v = Some f -> exists b, v = Vptr b Int.zero.






Lemma find_funct_find_funct_ptr:

  forall (ge: t) (b: block),

  find_funct ge (Vptr b Int.zero) = find_funct_ptr ge b.






Definition empty : genv :=

  mkgenv (ZMap.init None) (-1) (PTree.empty block).




Definition add_functs (init: genv) (fns: list (ident * F)) : genv :=

  List.fold_right add_funct init fns.




Definition add_globals 

       (init: genv * mem) (vars: list (ident * list init_data * V))

       : genv * mem :=

  List.fold_right

    (fun (id_init: ident * list init_data * V) (g_st: genv * mem) =>

       match id_init, g_st with

       | ((id, init), info), (g, st) =>

           let (st', b) := Mem.alloc_init_data st init in

           (add_symbol id b g, st')

       end)

    init vars.




Definition globalenv_initmem (p: program F V) : (genv * mem) :=

  add_globals

    (add_functs empty p.(prog_funct), Mem.empty)

    p.(prog_vars).




Definition globalenv (p: program F V) : genv :=

  fst (globalenv_initmem p).

Definition init_mem  (p: program F V) : mem :=

  snd (globalenv_initmem p).




Lemma functions_globalenv:

  forall (p: program F V),

  functions (globalenv p) = functions (add_functs empty p.(prog_funct)).






Lemma initmem_nullptr:

  forall (p: program F V),

  let m := init_mem p in

  valid_block m nullptr /\

  m.(blocks) nullptr = mkblock 0 0 (fun y => Undef).






Lemma initmem_inject_neutral:

  forall (p: program F V),

  mem_inject_neutral (init_mem p).






Remark nextfunction_add_functs_neg:

  forall fns, nextfunction (add_functs empty fns) < 0.






Theorem find_funct_ptr_negative:

  forall (p: program F V) (b: block) (f: F),

  find_funct_ptr (globalenv p) b = Some f -> b < 0.






Remark find_symbol_add_functs_negative:

  forall (fns: list (ident * F)) s b,

  (symbols (add_functs empty fns)) ! s = Some b -> b < 0.






Remark find_symbol_add_symbols_not_fresh:

  forall fns vars g m s b,

  add_globals (add_functs empty fns, Mem.empty) vars = (g, m) ->

  (symbols g)!s = Some b ->

  b < nextblock m.






Theorem find_symbol_not_fresh:

  forall (p: program F V) (id: ident) (b: block),

  find_symbol (globalenv p) id = Some b -> b < nextblock (init_mem p).






Lemma find_symbol_exists:

  forall (p: program F V)

         (id: ident) (init: list init_data) (v: V),

  In (id, init, v) (prog_vars p) ->

  exists b, find_symbol (globalenv p) id = Some b.






Remark find_symbol_above_nextfunction:

  forall (id: ident) (b: block) (fns: list (ident * F)),

  let g := add_functs empty fns in

  PTree.get id g.(symbols) = Some b ->

  b > g.(nextfunction).






Remark find_symbol_add_globals:

  forall (id: ident) (ge_m: t * mem) (vars: list (ident * list init_data * V)),

  ~In id (map (fun x: ident * list init_data * V => fst(fst x)) vars) ->

  find_symbol (fst (add_globals ge_m vars)) id =

  find_symbol (fst ge_m) id.






Lemma find_funct_ptr_exists:

  forall (p: program F V) (id: ident) (f: F),

  list_norepet (prog_funct_names p) ->

  list_disjoint (prog_funct_names p) (prog_var_names p) ->

  In (id, f) (prog_funct p) ->

  exists b, find_symbol (globalenv p) id = Some b

         /\ find_funct_ptr (globalenv p) b = Some f.






Lemma find_funct_ptr_inversion:

  forall (P: F -> Prop) (p: program F V) (b: block) (f: F),

  find_funct_ptr (globalenv p) b = Some f ->

  exists id, In (id, f) (prog_funct p).






Lemma find_funct_ptr_prop:

  forall (P: F -> Prop) (p: program F V) (b: block) (f: F),

  (forall id f, In (id, f) (prog_funct p) -> P f) ->

  find_funct_ptr (globalenv p) b = Some f ->

  P f.






Lemma find_funct_inversion:

  forall (P: F -> Prop) (p: program F V) (v: val) (f: F),

  find_funct (globalenv p) v = Some f ->

  exists id, In (id, f) (prog_funct p).






Lemma find_funct_prop:

  forall (P: F -> Prop) (p: program F V) (v: val) (f: F),

  (forall id f, In (id, f) (prog_funct p) -> P f) ->

  find_funct (globalenv p) v = Some f ->

  P f.






Lemma find_funct_ptr_symbol_inversion:

  forall (p: program F V) (id: ident) (b: block) (f: F),

  find_symbol (globalenv p) id = Some b ->

  find_funct_ptr (globalenv p) b = Some f ->

  In (id, f) p.(prog_funct).






Theorem find_symbol_not_nullptr:

  forall (p: program F V) (id: ident) (b: block),

  find_symbol (globalenv p) id = Some b -> b <> nullptr.






Theorem global_addresses_distinct:

  forall (p: program F V) id1 id2 b1 b2,

  id1<>id2 ->

  find_symbol (globalenv p) id1 = Some b1 ->

  find_symbol (globalenv p) id2 = Some b2 ->

  b1<>b2.






End GENV.




Section MATCH_PROGRAM.




Variable A B V W: Type.

Variable match_fun: A -> B -> Prop.

Variable match_var: V -> W -> Prop.

Variable p: program A V.

Variable p': program B W.

Hypothesis match_prog:

  match_program match_fun match_var p p'.




Lemma add_functs_match:

  forall (fns: list (ident * A)) (tfns: list (ident * B)),

  list_forall2 (match_funct_entry match_fun) fns tfns ->

  let r := add_functs (empty A) fns in

  let tr := add_functs (empty B) tfns in

  nextfunction tr = nextfunction r /\

  symbols tr = symbols r /\

  forall (b: block) (f: A),

  ZMap.get b (functions r) = Some f ->

  exists tf, ZMap.get b (functions tr) = Some tf /\ match_fun f tf.






Lemma add_functs_rev_match:

  forall (fns: list (ident * A)) (tfns: list (ident * B)),

  list_forall2 (match_funct_entry match_fun) fns tfns ->

  let r := add_functs (empty A) fns in

  let tr := add_functs (empty B) tfns in

  nextfunction tr = nextfunction r /\

  symbols tr = symbols r /\

  forall (b: block) (tf: B),

  ZMap.get b (functions tr) = Some tf ->

  exists f, ZMap.get b (functions r) = Some f /\ match_fun f tf.






Lemma mem_add_globals_match:

  forall (g1: genv A) (g2: genv B) (m: mem) 

         (vars: list (ident * list init_data * V))

         (tvars: list (ident * list init_data * W)),

  list_forall2 (match_var_entry match_var) vars tvars ->

  snd (add_globals (g1, m) vars) = snd (add_globals (g2, m) tvars).






Lemma symbols_add_globals_match:

  forall (g1: genv A) (g2: genv B) (m: mem),

  symbols g1 = symbols g2 ->

  forall (vars: list (ident * list init_data * V))

         (tvars: list (ident * list init_data * W)),

  list_forall2 (match_var_entry match_var) vars tvars ->

  symbols (fst (add_globals (g1, m) vars)) =

  symbols (fst (add_globals (g2, m) tvars)).






Theorem find_funct_ptr_match:

  forall (b: block) (f: A),

  find_funct_ptr (globalenv p) b = Some f ->

  exists tf, find_funct_ptr (globalenv p') b = Some tf /\ match_fun f tf.






Theorem find_funct_ptr_rev_match:

  forall (b: block) (tf: B),

  find_funct_ptr (globalenv p') b = Some tf ->

  exists f, find_funct_ptr (globalenv p) b = Some f /\ match_fun f tf.






Theorem find_funct_match:

  forall (v: val) (f: A),

  find_funct (globalenv p) v = Some f ->

  exists tf, find_funct (globalenv p') v = Some tf /\ match_fun f tf.






Theorem find_funct_rev_match:

  forall (v: val) (tf: B),

  find_funct (globalenv p') v = Some tf ->

  exists f, find_funct (globalenv p) v = Some f /\ match_fun f tf.






Lemma symbols_init_match:

  symbols (globalenv p') = symbols (globalenv p).






Theorem find_symbol_match:

  forall (s: ident),

  find_symbol (globalenv p') s = find_symbol (globalenv p) s.






Theorem init_mem_match:

  init_mem p' = init_mem p.






End MATCH_PROGRAM.




Section TRANSF_PROGRAM_PARTIAL2.




Variable A B V W: Type.

Variable transf_fun: A -> res B.

Variable transf_var: V -> res W.

Variable p: program A V.

Variable p': program B W.

Hypothesis transf_OK:

  transform_partial_program2 transf_fun transf_var p = OK p'.




Remark prog_match:

  match_program

    (fun fd tfd => transf_fun fd = OK tfd)

    (fun info tinfo => transf_var info = OK tinfo)

    p p'.






Theorem find_funct_ptr_transf_partial2:

  forall (b: block) (f: A),

  find_funct_ptr (globalenv p) b = Some f ->

  exists f',

  find_funct_ptr (globalenv p') b = Some f' /\ transf_fun f = OK f'.






Theorem find_funct_ptr_rev_transf_partial2:

  forall (b: block) (tf: B),

  find_funct_ptr (globalenv p') b = Some tf ->

  exists f, find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf.






Theorem find_funct_transf_partial2:

  forall (v: val) (f: A),

  find_funct (globalenv p) v = Some f ->

  exists f',

  find_funct (globalenv p') v = Some f' /\ transf_fun f = OK f'.






Theorem find_funct_rev_transf_partial2:

  forall (v: val) (tf: B),

  find_funct (globalenv p') v = Some tf ->

  exists f, find_funct (globalenv p) v = Some f /\ transf_fun f = OK tf.






Theorem find_symbol_transf_partial2:

  forall (s: ident),

  find_symbol (globalenv p') s = find_symbol (globalenv p) s.






Theorem init_mem_transf_partial2:

  init_mem p' = init_mem p.






End TRANSF_PROGRAM_PARTIAL2.




Section TRANSF_PROGRAM_PARTIAL.




Variable A B V: Type.

Variable transf: A -> res B.

Variable p: program A V.

Variable p': program B V.

Hypothesis transf_OK: transform_partial_program transf p = OK p'.




Remark transf2_OK:

  transform_partial_program2 transf (fun x => OK x) p = OK p'.






Theorem find_funct_ptr_transf_partial:

  forall (b: block) (f: A),

  find_funct_ptr (globalenv p) b = Some f ->

  exists f',

  find_funct_ptr (globalenv p') b = Some f' /\ transf f = OK f'.






Theorem find_funct_ptr_rev_transf_partial:

  forall (b: block) (tf: B),

  find_funct_ptr (globalenv p') b = Some tf ->

  exists f, find_funct_ptr (globalenv p) b = Some f /\ transf f = OK tf.






Theorem find_funct_transf_partial:

  forall (v: val) (f: A),

  find_funct (globalenv p) v = Some f ->

  exists f',

  find_funct (globalenv p') v = Some f' /\ transf f = OK f'.






Theorem find_funct_rev_transf_partial:

  forall (v: val) (tf: B),

  find_funct (globalenv p') v = Some tf ->

  exists f, find_funct (globalenv p) v = Some f /\ transf f = OK tf.






Theorem find_symbol_transf_partial:

  forall (s: ident),

  find_symbol (globalenv p') s = find_symbol (globalenv p) s.






Theorem init_mem_transf_partial:

  init_mem p' = init_mem p.






End TRANSF_PROGRAM_PARTIAL.




Section TRANSF_PROGRAM.




Variable A B V: Type.

Variable transf: A -> B.

Variable p: program A V.

Let tp := transform_program transf p.




Remark transf_OK:

  transform_partial_program (fun x => OK (transf x)) p = OK tp.






Theorem find_funct_ptr_transf:

  forall (b: block) (f: A),

  find_funct_ptr (globalenv p) b = Some f ->

  find_funct_ptr (globalenv tp) b = Some (transf f).






Theorem find_funct_ptr_rev_transf:

  forall (b: block) (tf: B),

  find_funct_ptr (globalenv tp) b = Some tf ->

  exists f, find_funct_ptr (globalenv p) b = Some f /\ transf f = tf.






Theorem find_funct_transf:

  forall (v: val) (f: A),

  find_funct (globalenv p) v = Some f ->

  find_funct (globalenv tp) v = Some (transf f).






Theorem find_funct_rev_transf:

  forall (v: val) (tf: B),

  find_funct (globalenv tp) v = Some tf ->

  exists f, find_funct (globalenv p) v = Some f /\ transf f = tf.






Theorem find_symbol_transf:

  forall (s: ident),

  find_symbol (globalenv tp) s = find_symbol (globalenv p) s.






Theorem init_mem_transf:

  init_mem tp = init_mem p.






End TRANSF_PROGRAM.




End Genv.