diff options
Diffstat (limited to 'common/Globalenvs.v')
-rw-r--r-- | common/Globalenvs.v | 380 |
1 files changed, 222 insertions, 158 deletions
diff --git a/common/Globalenvs.v b/common/Globalenvs.v index 036fd8f6..ccb7b03e 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -35,10 +35,10 @@ Module Type GENV. (** The type of global environments. The parameter [F] is the type of function descriptions. *) - Variable globalenv: forall (F: Set), program F -> t F. + Variable globalenv: forall (F V: Set), program F V -> t F. (** Return the global environment for the given program. *) - Variable init_mem: forall (F: Set), program F -> mem. + Variable init_mem: forall (F V: Set), program F V -> mem. (** Return the initial memory state for the given program. *) Variable find_funct_ptr: forall (F: Set), t F -> block -> option F. @@ -61,83 +61,110 @@ Module Type GENV. forall (F: Set) (ge: t F) (b: block), find_funct ge (Vptr b Int.zero) = find_funct_ptr ge b. Hypothesis find_funct_ptr_prop: - forall (F: Set) (P: F -> Prop) (p: program F) (b: block) (f: F), + forall (F V: Set) (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: Set) (P: F -> Prop) (p: program F) (v: val) (f: F), + forall (F V: Set) (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 find_funct_ptr_symbol_inversion: - forall (F: Set) (p: program F) (id: ident) (b: block) (f: F), + forall (F V: Set) (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 initmem_nullptr: - forall (F: Set) (p: program F), + forall (F V: Set) (p: program F V), let m := init_mem p in valid_block m nullptr /\ m.(blocks) nullptr = empty_block 0 0. Hypothesis initmem_block_init: - forall (F: Set) (p: program F) (b: block), + forall (F V: Set) (p: program F V) (b: block), exists id, (init_mem p).(blocks) b = block_init_data id. Hypothesis find_funct_ptr_inv: - forall (F: Set) (p: program F) (b: block) (f: F), + forall (F V: Set) (p: program F V) (b: block) (f: F), find_funct_ptr (globalenv p) b = Some f -> b < 0. Hypothesis find_symbol_inv: - forall (F: Set) (p: program F) (id: ident) (b: block), + forall (F V: Set) (p: program F V) (id: ident) (b: block), find_symbol (globalenv p) id = Some b -> b < nextblock (init_mem p). (** Commutation properties between program transformations and operations over global environments. *) Hypothesis find_funct_ptr_transf: - forall (A B: Set) (transf: A -> B) (p: program A) (b: block) (f: A), + forall (A B V: Set) (transf: A -> B) (p: program A V) (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: Set) (transf: A -> B) (p: program A) (v: val) (f: A), + forall (A B V: Set) (transf: A -> B) (p: program A V) (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: Set) (transf: A -> B) (p: program A) (s: ident), + forall (A B V: Set) (transf: A -> B) (p: program A V) (s: ident), find_symbol (globalenv (transform_program transf p)) s = find_symbol (globalenv p) s. Hypothesis init_mem_transf: - forall (A B: Set) (transf: A -> B) (p: program A), + forall (A B V: Set) (transf: A -> B) (p: program A V), init_mem (transform_program transf p) = init_mem p. (** Commutation properties between partial program transformations and operations over global environments. *) Hypothesis find_funct_ptr_transf_partial: - forall (A B: Set) (transf: A -> option B) - (p: program A) (p': program B), + forall (A B V: Set) (transf: A -> option B) + (p: program A V) (p': program B V), transform_partial_program transf p = Some p' -> forall (b: block) (f: A), find_funct_ptr (globalenv p) b = Some f -> find_funct_ptr (globalenv p') b = transf f /\ transf f <> None. Hypothesis find_funct_transf_partial: - forall (A B: Set) (transf: A -> option B) - (p: program A) (p': program B), + forall (A B V: Set) (transf: A -> option B) + (p: program A V) (p': program B V), transform_partial_program transf p = Some p' -> forall (v: val) (f: A), find_funct (globalenv p) v = Some f -> find_funct (globalenv p') v = transf f /\ transf f <> None. Hypothesis find_symbol_transf_partial: - forall (A B: Set) (transf: A -> option B) - (p: program A) (p': program B), + forall (A B V: Set) (transf: A -> option B) + (p: program A V) (p': program B V), transform_partial_program transf p = Some p' -> forall (s: ident), find_symbol (globalenv p') s = find_symbol (globalenv p) s. Hypothesis init_mem_transf_partial: - forall (A B: Set) (transf: A -> option B) - (p: program A) (p': program B), + forall (A B V: Set) (transf: A -> option B) + (p: program A V) (p': program B V), transform_partial_program transf p = Some p' -> init_mem p' = init_mem p. + + Hypothesis find_funct_ptr_transf_partial2: + forall (A B V W: Set) (transf_fun: A -> option B) (transf_var: V -> option W) + (p: program A V) (p': program B W), + transform_partial_program2 transf_fun transf_var p = Some p' -> + forall (b: block) (f: A), + find_funct_ptr (globalenv p) b = Some f -> + find_funct_ptr (globalenv p') b = transf_fun f /\ transf_fun f <> None. + Hypothesis find_funct_transf_partial2: + forall (A B V W: Set) (transf_fun: A -> option B) (transf_var: V -> option W) + (p: program A V) (p': program B W), + transform_partial_program2 transf_fun transf_var p = Some p' -> + forall (v: val) (f: A), + find_funct (globalenv p) v = Some f -> + find_funct (globalenv p') v = transf_fun f /\ transf_fun f <> None. + Hypothesis find_symbol_transf_partial2: + forall (A B V W: Set) (transf_fun: A -> option B) (transf_var: V -> option W) + (p: program A V) (p': program B W), + transform_partial_program2 transf_fun transf_var p = Some p' -> + forall (s: ident), + find_symbol (globalenv p') s = find_symbol (globalenv p) s. + Hypothesis init_mem_transf_partial2: + forall (A B V W: Set) (transf_fun: A -> option B) (transf_var: V -> option W) + (p: program A V) (p': program B W), + transform_partial_program2 transf_fun transf_var p = Some p' -> + init_mem p' = init_mem p. + End GENV. (** The rest of this library is a straightforward implementation of @@ -147,17 +174,18 @@ Module Genv: GENV. Section GENV. -Variable funct: Set. (* The type of functions *) +Variable F: Set. (* The type of functions *) +Variable V: Set. (* The type of information over variables *) Record genv : Set := mkgenv { - functions: ZMap.t (option funct); (* mapping function ptr -> function *) + functions: ZMap.t (option F); (* mapping function ptr -> function *) nextfunction: Z; symbols: PTree.t block (* mapping symbol -> block *) }. Definition t := genv. -Definition add_funct (name_fun: (ident * funct)) (g: genv) : 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) @@ -168,10 +196,10 @@ Definition add_symbol (name: ident) (b: block) (g: genv) : genv := g.(nextfunction) (PTree.set name b g.(symbols)). -Definition find_funct_ptr (g: genv) (b: block) : option funct := +Definition find_funct_ptr (g: genv) (b: block) : option F := ZMap.get b g.(functions). -Definition find_funct (g: genv) (v: val) : option funct := +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 @@ -183,7 +211,7 @@ Definition find_symbol (g: genv) (symb: ident) : option block := PTree.get symb g.(symbols). Lemma find_funct_inv: - forall (ge: t) (v: val) (f: funct), + forall (ge: t) (v: val) (f: F), find_funct ge v = Some f -> exists b, v = Vptr b Int.zero. Proof. intros until f. unfold find_funct. destruct v; try (intros; discriminate). @@ -207,38 +235,40 @@ Qed. Definition empty : genv := mkgenv (ZMap.init None) (-1) (PTree.empty block). -Definition add_functs (init: genv) (fns: list (ident * funct)) : genv := +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)) : genv * mem := + (init: genv * mem) (vars: list (ident * list init_data * V)) + : genv * mem := List.fold_right - (fun (id_init: ident * list init_data) (g_st: genv * mem) => - let (id, init) := id_init in - let (g, st) := g_st in - let (st', b) := Mem.alloc_init_data st init in - (add_symbol id b g, st')) + (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 funct) : (genv * mem) := +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 funct) : genv := +Definition globalenv (p: program F V) : genv := fst (globalenv_initmem p). -Definition init_mem (p: program funct) : mem := +Definition init_mem (p: program F V) : mem := snd (globalenv_initmem p). Lemma functions_globalenv: - forall (p: program funct), + forall (p: program F V), functions (globalenv p) = functions (add_functs empty p.(prog_funct)). Proof. assert (forall init vars, functions (fst (add_globals init vars)) = functions (fst init)). induction vars; simpl. reflexivity. - destruct a. destruct (add_globals init vars). + destruct a as [[id1 init1] info1]. destruct (add_globals init vars). simpl. exact IHvars. unfold add_globals; simpl. @@ -247,34 +277,28 @@ Proof. Qed. Lemma initmem_nullptr: - forall (p: program funct), + forall (p: program F V), let m := init_mem p in valid_block m nullptr /\ m.(blocks) nullptr = mkblock 0 0 (fun y => Undef) (undef_undef_outside 0 0). Proof. - assert - (forall init, - let m1 := snd init in - 0 < m1.(nextblock) -> - m1.(blocks) nullptr = mkblock 0 0 (fun y => Undef) (undef_undef_outside 0 0) -> - forall vars, - let m2 := snd (add_globals init vars) in - 0 < m2.(nextblock) /\ - m2.(blocks) nullptr = mkblock 0 0 (fun y => Undef) (undef_undef_outside 0 0)). + pose (P := fun m => valid_block m nullptr /\ + m.(blocks) nullptr = mkblock 0 0 (fun y => Undef) (undef_undef_outside 0 0)). + assert (forall init, P (snd init) -> forall vars, P (snd (add_globals init vars))). induction vars; simpl; intros. - tauto. - destruct a. - caseEq (add_globals init vars). intros g m2 EQ. - rewrite EQ in IHvars. simpl in IHvars. elim IHvars; intros. - simpl. split. omega. - rewrite update_o. auto. apply sym_not_equal. apply Zlt_not_eq. exact H1. - - intro. unfold init_mem. unfold globalenv_initmem. - unfold valid_block. apply H. simpl. omega. reflexivity. + auto. + destruct a as [[id1 in1] inf1]. + destruct (add_globals init vars) as [g st]. + simpl in *. destruct IHvars. split. + red; simpl. red in H0. omega. + simpl. rewrite update_o. auto. unfold block. red in H0. omega. + + intro. unfold init_mem, globalenv_initmem. apply H. + red; simpl. split. compute. auto. reflexivity. Qed. Lemma initmem_block_init: - forall (p: program funct) (b: block), + forall (p: program F V) (b: block), exists id, (init_mem p).(blocks) b = block_init_data id. Proof. assert (forall g0 vars g1 m b, @@ -283,11 +307,12 @@ Proof. induction vars; simpl. intros. inversion H. unfold Mem.empty; simpl. exists (@nil init_data). symmetry. apply Mem.block_init_data_empty. - destruct a. caseEq (add_globals (g0, Mem.empty) vars). intros g1 m1 EQ. + destruct a as [[id1 init1] info1]. + caseEq (add_globals (g0, Mem.empty) vars). intros g1 m1 EQ. intros g m b EQ1. injection EQ1; intros EQ2 EQ3; clear EQ1. rewrite <- EQ2; simpl. unfold update. case (zeq b (nextblock m1)); intro. - exists l; auto. + exists init1; auto. eauto. intros. caseEq (globalenv_initmem p). intros g m EQ. unfold init_mem; rewrite EQ; simpl. @@ -301,7 +326,7 @@ Proof. Qed. Theorem find_funct_ptr_inv: - forall (p: program funct) (b: block) (f: funct), + forall (p: program F V) (b: block) (f: F), find_funct_ptr (globalenv p) b = Some f -> b < 0. Proof. intros until f. @@ -316,7 +341,7 @@ Proof. Qed. Theorem find_symbol_inv: - forall (p: program funct) (id: ident) (b: block), + forall (p: program F V) (id: ident) (b: block), find_symbol (globalenv p) id = Some b -> b < nextblock (init_mem p). Proof. assert (forall fns s b, @@ -333,9 +358,10 @@ Proof. induction vars; simpl; intros until b. intros. inversion H0. subst g m. simpl. generalize (H fns s b H1). omega. - destruct a. caseEq (add_globals (add_functs empty fns, Mem.empty) vars). + destruct a as [[id1 init1] info1]. + caseEq (add_globals (add_functs empty fns, Mem.empty) vars). intros g1 m1 ADG EQ. inversion EQ; subst g m; clear EQ. - unfold add_symbol; simpl. rewrite PTree.gsspec. case (peq s i); intro. + unfold add_symbol; simpl. rewrite PTree.gsspec. case (peq s id1); intro. intro EQ; inversion EQ. omega. intro. generalize (IHvars _ _ _ _ ADG H0). omega. intros until b. unfold find_symbol, globalenv, init_mem, globalenv_initmem; simpl. @@ -348,7 +374,7 @@ End GENV. (* Invariants on functions *) Lemma find_funct_ptr_prop: - forall (F: Set) (P: F -> Prop) (p: program F) (b: block) (f: F), + forall (F V: Set) (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. @@ -364,7 +390,7 @@ Proof. Qed. Lemma find_funct_prop: - forall (F: Set) (P: F -> Prop) (p: program F) (v: val) (f: F), + forall (F V: Set) (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. @@ -376,7 +402,7 @@ Proof. Qed. Lemma find_funct_ptr_symbol_inversion: - forall (F: Set) (p: program F) (id: ident) (b: block) (f: F), + forall (F V: Set) (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). @@ -407,15 +433,15 @@ Proof. generalize (H _ H0). fold g. unfold block. omega. assert (forall g0 m0, b < 0 -> forall vars g m, - @add_globals F (g0, m0) vars = (g, m) -> + @add_globals F V (g0, m0) vars = (g, m) -> PTree.get id g.(symbols) = Some b -> PTree.get id g0.(symbols) = Some b). induction vars; simpl. intros. inversion H2. auto. - destruct a. caseEq (add_globals (g0, m0) vars). + destruct a as [[id1 init1] info1]. caseEq (add_globals (g0, m0) vars). intros g1 m1 EQ g m EQ1. injection EQ1; simpl; clear EQ1. unfold add_symbol; intros A B. rewrite <- B. simpl. - rewrite PTree.gsspec. case (peq id i); intros. + rewrite PTree.gsspec. case (peq id id1); intros. assert (b > 0). injection H2; intros. rewrite <- H3. apply nextblock_pos. omegaContradiction. eauto. @@ -430,24 +456,26 @@ Qed. (* Global environments and program transformations. *) -Section TRANSF_PROGRAM_PARTIAL. +Section TRANSF_PROGRAM_PARTIAL2. -Variable A B: Set. -Variable transf: A -> option B. -Variable p: program A. -Variable p': program B. -Hypothesis transf_OK: transform_partial_program transf p = Some p'. +Variable A B V W: Set. +Variable transf_fun: A -> option B. +Variable transf_var: V -> option W. +Variable p: program A V. +Variable p': program B W. +Hypothesis transf_OK: + transform_partial_program2 transf_fun transf_var p = Some p'. Lemma add_functs_transf: forall (fns: list (ident * A)) (tfns: list (ident * B)), - transf_partial_program transf fns = Some tfns -> + map_partial transf_fun fns = Some 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 -> - ZMap.get b (functions tr) = transf f /\ transf f <> None. + ZMap.get b (functions tr) = transf_fun f /\ transf_fun f <> None. Proof. induction fns; simpl. @@ -455,8 +483,8 @@ Proof. simpl. split. reflexivity. split. reflexivity. intros b f; repeat (rewrite ZMap.gi). intros; discriminate. - intro tfns. destruct a. caseEq (transf a). intros a' TA. - caseEq (transf_partial_program transf fns). intros l TPP EQ. + intro tfns. destruct a. caseEq (transf_fun a). intros a' TA. + caseEq (map_partial transf_fun fns). intros l TPP EQ. injection EQ; intro; subst tfns. clear EQ. simpl. generalize (IHfns l TPP). @@ -476,32 +504,49 @@ Proof. Qed. Lemma mem_add_globals_transf: - forall (g1: genv A) (g2: genv B) (m: mem) (vars: list (ident * list init_data)), - snd (add_globals (g1, m) vars) = snd (add_globals (g2, m) vars). + forall (g1: genv A) (g2: genv B) (m: mem) + (vars: list (ident * list init_data * V)) + (tvars: list (ident * list init_data * W)), + map_partial transf_var vars = Some tvars -> + snd (add_globals (g1, m) vars) = snd (add_globals (g2, m) tvars). Proof. induction vars; simpl. - reflexivity. - destruct a. destruct (add_globals (g1, m) vars). - destruct (add_globals (g2, m) vars). - simpl in IHvars. subst m1. reflexivity. -Qed. + intros. inversion H. reflexivity. + intro. destruct a as [[id1 init1] info1]. + caseEq (transf_var info1); try congruence. + intros tinfo1 EQ1. + caseEq (map_partial transf_var vars); try congruence. + intros tvars' EQ2 EQ3. + inversion EQ3. simpl. + generalize (IHvars _ EQ2). + destruct (add_globals (g1, m) vars). + destruct (add_globals (g2, m) tvars'). + simpl. intro. subst m1. auto. +Qed. Lemma symbols_add_globals_transf: forall (g1: genv A) (g2: genv B) (m: mem), symbols g1 = symbols g2 -> - forall (vars: list (ident * list init_data)), + forall (vars: list (ident * list init_data * V)) + (tvars: list (ident * list init_data * W)), + map_partial transf_var vars = Some tvars -> symbols (fst (add_globals (g1, m) vars)) = - symbols (fst (add_globals (g2, m) vars)). + symbols (fst (add_globals (g2, m) tvars)). Proof. induction vars; simpl. - assumption. - generalize (mem_add_globals_transf g1 g2 m vars); intro. - destruct a. destruct (add_globals (g1, m) vars). - destruct (add_globals (g2, m) vars). - simpl. simpl in IHvars. simpl in H0. - rewrite H0; rewrite IHvars. reflexivity. + intros. inversion H0. assumption. + intro. destruct a as [[id1 init1] info1]. + caseEq (transf_var info1); try congruence. intros tinfo1 EQ1. + caseEq (map_partial transf_var vars); try congruence. + intros tvars' EQ2 EQ3. inversion EQ3; simpl. + generalize (IHvars _ EQ2). + generalize (mem_add_globals_transf g1 g2 m vars EQ2). + destruct (add_globals (g1, m) vars). + destruct (add_globals (g2, m) tvars'). + simpl. intros. congruence. Qed. +(* Lemma prog_funct_transf_OK: transf_partial_program transf p.(prog_funct) = Some p'.(prog_funct). Proof. @@ -510,94 +555,118 @@ Proof. injection transf_OK0; intros; subst p'. reflexivity. discriminate. Qed. +*) -Theorem find_funct_ptr_transf_partial: +Theorem find_funct_ptr_transf_partial2: forall (b: block) (f: A), find_funct_ptr (globalenv p) b = Some f -> - find_funct_ptr (globalenv p') b = transf f /\ transf f <> None. + find_funct_ptr (globalenv p') b = transf_fun f /\ transf_fun f <> None. Proof. - intros until f. - generalize (add_functs_transf p.(prog_funct) prog_funct_transf_OK). - intros [X [Y Z]]. - unfold find_funct_ptr. - repeat (rewrite functions_globalenv). - apply Z. + intros until f. functional inversion transf_OK. + destruct (add_functs_transf _ H0) as [P [Q R]]. + unfold find_funct_ptr. repeat rewrite functions_globalenv. simpl. + auto. Qed. -Theorem find_funct_transf_partial: +Theorem find_funct_transf_partial2: forall (v: val) (f: A), find_funct (globalenv p) v = Some f -> - find_funct (globalenv p') v = transf f /\ transf f <> None. + find_funct (globalenv p') v = transf_fun f /\ transf_fun f <> None. Proof. intros until f. unfold find_funct. case v; try (intros; discriminate). intros b ofs. case (Int.eq ofs Int.zero); try (intros; discriminate). - apply find_funct_ptr_transf_partial. + apply find_funct_ptr_transf_partial2. Qed. -Lemma symbols_init_transf: +Lemma symbols_init_transf2: symbols (globalenv p') = symbols (globalenv p). Proof. unfold globalenv. unfold globalenv_initmem. - generalize (add_functs_transf p.(prog_funct) prog_funct_transf_OK). - intros [X [Y Z]]. - generalize transf_OK. - unfold transform_partial_program. - case (transf_partial_program transf (prog_funct p)). - intros. injection transf_OK0; intro; subst p'; simpl. - symmetry. apply symbols_add_globals_transf. - symmetry. exact Y. - intros; discriminate. + functional inversion transf_OK. + destruct (add_functs_transf _ H0) as [P [Q R]]. + simpl. symmetry. apply symbols_add_globals_transf. auto. auto. Qed. -Theorem find_symbol_transf_partial: +Theorem find_symbol_transf_partial2: forall (s: ident), find_symbol (globalenv p') s = find_symbol (globalenv p) s. Proof. intros. unfold find_symbol. - rewrite symbols_init_transf. auto. + rewrite symbols_init_transf2. auto. Qed. -Theorem init_mem_transf_partial: +Theorem init_mem_transf_partial2: init_mem p' = init_mem p. Proof. unfold init_mem. unfold globalenv_initmem. - generalize transf_OK. - unfold transform_partial_program. - case (transf_partial_program transf (prog_funct p)). - intros. injection transf_OK0; intro; subst p'; simpl. - symmetry. apply mem_add_globals_transf. - intros; discriminate. + functional inversion transf_OK. + simpl. symmetry. apply mem_add_globals_transf. auto. Qed. -End TRANSF_PROGRAM_PARTIAL. +End TRANSF_PROGRAM_PARTIAL2. -Section TRANSF_PROGRAM. -Variable A B: Set. -Variable transf: A -> B. -Variable p: program A. -Let tp := transform_program transf p. +Section TRANSF_PROGRAM_PARTIAL. -Definition transf_partial (x: A) : option B := Some (transf x). +Variable A B V: Set. +Variable transf: A -> option B. +Variable p: program A V. +Variable p': program B V. +Hypothesis transf_OK: transform_partial_program transf p = Some p'. -Lemma transf_program_transf_partial_program: - forall (fns: list (ident * A)), - transf_partial_program transf_partial fns = - Some (transf_program transf fns). +Remark transf2_OK: + transform_partial_program2 transf (fun x => Some x) p = Some p'. Proof. - induction fns; simpl. - reflexivity. - destruct a. rewrite IHfns. reflexivity. + rewrite <- transf_OK. unfold transform_partial_program2, transform_partial_program. + destruct (map_partial transf (prog_funct p)); auto. + rewrite map_partial_identity; auto. +Qed. + +Theorem find_funct_ptr_transf_partial: + forall (b: block) (f: A), + find_funct_ptr (globalenv p) b = Some f -> + find_funct_ptr (globalenv p') b = transf f /\ transf f <> None. +Proof. + exact (@find_funct_ptr_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). Qed. -Lemma transform_program_transform_partial_program: - transform_partial_program transf_partial p = Some tp. +Theorem find_funct_transf_partial: + forall (v: val) (f: A), + find_funct (globalenv p) v = Some f -> + find_funct (globalenv p') v = transf f /\ transf f <> None. Proof. - unfold tp. unfold transform_partial_program, transform_program. - rewrite transf_program_transf_partial_program. - reflexivity. + exact (@find_funct_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). +Qed. + +Theorem find_symbol_transf_partial: + forall (s: ident), + find_symbol (globalenv p') s = find_symbol (globalenv p) s. +Proof. + exact (@find_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). +Qed. + +Theorem init_mem_transf_partial: + init_mem p' = init_mem p. +Proof. + exact (@init_mem_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). +Qed. + +End TRANSF_PROGRAM_PARTIAL. + +Section TRANSF_PROGRAM. + +Variable A B V: Set. +Variable transf: A -> B. +Variable p: program A V. +Let tp := transform_program transf p. + +Remark transf_OK: + transform_partial_program (fun x => Some (transf x)) p = Some tp. +Proof. + unfold tp, transform_program, transform_partial_program. + rewrite map_partial_total. reflexivity. Qed. Theorem find_funct_ptr_transf: @@ -605,10 +674,9 @@ Theorem find_funct_ptr_transf: find_funct_ptr (globalenv p) b = Some f -> find_funct_ptr (globalenv tp) b = Some (transf f). Proof. - intros. - generalize (find_funct_ptr_transf_partial transf_partial p - transform_program_transform_partial_program). - intros. elim (H0 b f H). intros. exact H1. + intros. + destruct (@find_funct_ptr_transf_partial _ _ _ _ _ _ transf_OK _ _ H) + as [X Y]. auto. Qed. Theorem find_funct_transf: @@ -616,26 +684,22 @@ Theorem find_funct_transf: find_funct (globalenv p) v = Some f -> find_funct (globalenv tp) v = Some (transf f). Proof. - intros. - generalize (find_funct_transf_partial transf_partial p - transform_program_transform_partial_program). - intros. elim (H0 v f H). intros. exact H1. + intros. + destruct (@find_funct_transf_partial _ _ _ _ _ _ transf_OK _ _ H) + as [X Y]. auto. Qed. Theorem find_symbol_transf: forall (s: ident), find_symbol (globalenv tp) s = find_symbol (globalenv p) s. Proof. - intros. - apply find_symbol_transf_partial with transf_partial. - apply transform_program_transform_partial_program. + exact (@find_symbol_transf_partial _ _ _ _ _ _ transf_OK). Qed. Theorem init_mem_transf: init_mem tp = init_mem p. Proof. - apply init_mem_transf_partial with transf_partial. - apply transform_program_transform_partial_program. + exact (@init_mem_transf_partial _ _ _ _ _ _ transf_OK). Qed. End TRANSF_PROGRAM. |