diff options
38 files changed, 1301 insertions, 1637 deletions
@@ -7,6 +7,9 @@ Improvements in confidence: top of the Flocq library. Language semantics: +- Comparison between function pointers is now correctly defined + in the semantics of CompCert C (it was previously undefined behavior, + by mistake). - The "&&" and "||" operators are now primitive in CompCert C and are given explicit semantic rules, instead of being expressed in terms of "_ ? _ : _" as in previous CompCert releases. @@ -28,6 +31,9 @@ Internal simplifications: - Clight: removed dependencies on CompCert C syntax and semantics. - Cminor: suppressed the "Oboolval" and "Onotbool" operators, which can be expressed in terms of "Ocmpu" at no performance costs. +- All languages: programs are now presented as a list of global definitions + (of functions or variables) instead of two lists, one for functions + and the other for variables. Other changes: - For compatibility with other C compilers, output files are now generated diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index ec1e836..60d0fa4 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -698,13 +698,6 @@ let print_function oc name fn = fprintf oc " .type %a, %%function\n" print_symb name; fprintf oc " .size %a, . - %a\n" print_symb name print_symb name -let print_fundef oc (name, defn) = - match defn with - | Internal code -> - print_function oc name code - | External ef -> - () - (* Data *) let print_init oc = function @@ -734,7 +727,7 @@ let print_init_data oc name id = else List.iter (print_init oc) id -let print_var oc (name, v) = +let print_var oc name v = match v.gvar_init with | [] -> () | _ -> @@ -756,8 +749,14 @@ let print_var oc (name, v) = fprintf oc " .type %a, %%object\n" print_symb name; fprintf oc " .size %a, . - %a\n" print_symb name print_symb name +let print_globdef oc (name, gdef) = + | Gfun(Internal f) -> print_function oc name f + | Gfun(External ef) -> () + | Gvar v -> print_var oc name v + let print_program oc p = (* fprintf oc " .fpu vfp\n"; *) List.iter (print_var oc) p.prog_vars; - List.iter (print_fundef oc) p.prog_funct + List.iter (print_globdef oc) p.prog_defs + diff --git a/backend/CMparser.mly b/backend/CMparser.mly index aec0a5e..a62bd74 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -307,10 +307,9 @@ let mkmatch expr cases = /* Programs */ prog: - global_declarations proc_list EOF - { { prog_funct = List.rev $2; - prog_main = intern_string "main"; - prog_vars = List.rev $1; } } + global_declarations EOF + { { prog_defs = List.rev $1; + prog_main = intern_string "main" } } ; global_declarations: @@ -319,12 +318,14 @@ global_declarations: ; global_declaration: - VAR STRINGLIT LBRACKET INTLIT RBRACKET /* old style */ - { ($2, {gvar_info = (); gvar_init = [Init_space(z_of_camlint $4)]; - gvar_readonly = false; gvar_volatile = false}) } + proc + { $1 } + | VAR STRINGLIT LBRACKET INTLIT RBRACKET /* old style */ + { ($2, Gvar{gvar_info = (); gvar_init = [Init_space(z_of_camlint $4)]; + gvar_readonly = false; gvar_volatile = false}) } | VAR STRINGLIT is_readonly is_volatile LBRACE init_data_list RBRACE - { ($2, {gvar_info = (); gvar_init = List.rev $6; - gvar_readonly = $3; gvar_volatile = $4; } ) } + { ($2, Gvar{gvar_info = (); gvar_init = List.rev $6; + gvar_readonly = $3; gvar_volatile = $4; } ) } ; is_readonly: @@ -359,12 +360,6 @@ init_data: | INTLIT LPAREN STRINGLIT RPAREN { Init_addrof ($3, coqint_of_camlint $1) } ; - -proc_list: - /* empty */ { [] } - | proc_list proc { $2 :: $1 } -; - /* Procedures */ proc: @@ -378,13 +373,13 @@ proc: temporaries := []; temp_counter := 0; ($1, - Internal { fn_sig = $6; - fn_params = List.rev $3; - fn_vars = List.rev (tmp @ $9); - fn_stackspace = $8; - fn_body = $10 }) } + Gfun(Internal { fn_sig = $6; + fn_params = List.rev $3; + fn_vars = List.rev (tmp @ $9); + fn_stackspace = $8; + fn_body = $10 })) } | EXTERN STRINGLIT COLON signature - { ($2, External(EF_external($2,$4))) } + { ($2, Gfun(External(EF_external($2,$4)))) } ; signature: diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml index 4070785..408e9ec 100644 --- a/backend/CMtypecheck.ml +++ b/backend/CMtypecheck.ml @@ -349,10 +349,11 @@ let type_function id f = with Error s -> raise (Error (sprintf "In function %s:\n%s" (extern_atom id) s)) -let type_fundef (id, fd) = - match fd with - | Internal f -> type_function id f - | External ef -> () +let type_globdef (id, gd) = + match gd with + | Gfun(Internal f) -> type_function id f + | Gfun(External ef) -> () + | Gvar v -> () let type_program p = - List.iter type_fundef p.prog_funct; p + List.iter type_globdef p.prog_defs; p diff --git a/backend/Constprop.v b/backend/Constprop.v index 104aa3b..fc242e1 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -368,17 +368,21 @@ Definition transf_function (gapp: global_approx) (f: function) : function := Definition transf_fundef (gapp: global_approx) (fd: fundef) : fundef := AST.transf_fundef (transf_function gapp) fd. -Fixpoint make_global_approx (gapp: global_approx) (vars: list (ident * globvar unit)) : global_approx := - match vars with +Fixpoint make_global_approx (gapp: global_approx) (gdl: list (ident * globdef fundef unit)): global_approx := + match gdl with | nil => gapp - | (id, gv) :: vars' => + | (id, gl) :: gdl' => let gapp1 := - if gv.(gvar_readonly) && negb gv.(gvar_volatile) - then PTree.set id gv.(gvar_init) gapp - else PTree.remove id gapp in - make_global_approx gapp1 vars' + match gl with + | Gfun f => PTree.remove id gapp + | Gvar gv => + if gv.(gvar_readonly) && negb gv.(gvar_volatile) + then PTree.set id gv.(gvar_init) gapp + else PTree.remove id gapp + end in + make_global_approx gapp1 gdl' end. Definition transf_program (p: program) : program := - let gapp := make_global_approx (PTree.empty _) p.(prog_vars) in + let gapp := make_global_approx (PTree.empty _) p.(prog_defs) in transform_program (transf_fundef gapp) p. diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index 8228493..f14e87a 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -37,7 +37,7 @@ Variable prog: program. Let tprog := transf_program prog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. -Let gapp := make_global_approx (PTree.empty _) prog.(prog_vars). +Let gapp := make_global_approx (PTree.empty _) prog.(prog_defs). (** * Correctness of the static analysis *) @@ -279,31 +279,34 @@ Definition global_approx_charact (g: genv) (ga: global_approx) : Prop := Genv.find_var_info g b = Some (mkglobvar tt il true false). Lemma make_global_approx_correct: - forall vl g ga, + forall gdl g ga, global_approx_charact g ga -> - global_approx_charact (Genv.add_variables g vl) (make_global_approx ga vl). + global_approx_charact (Genv.add_globals g gdl) (make_global_approx ga gdl). Proof. - induction vl; simpl; intros. + induction gdl; simpl; intros. auto. - destruct a as [id gv]. apply IHvl. + destruct a as [id gd]. apply IHgdl. red; intros. - assert (EITHER: id0 = id /\ gv = mkglobvar tt il true false + assert (EITHER: id0 = id /\ gd = Gvar(mkglobvar tt il true false) \/ id0 <> id /\ ga!id0 = Some il). - destruct (gvar_readonly gv && negb (gvar_volatile gv)) as []_eqn. + destruct gd. + rewrite PTree.grspec in H0. destruct (PTree.elt_eq id0 id); [discriminate|auto]. + destruct (gvar_readonly v && negb (gvar_volatile v)) as []_eqn. rewrite PTree.gsspec in H0. destruct (peq id0 id). inv H0. left. split; auto. - destruct gv; simpl in *. + destruct v; simpl in *. destruct gvar_readonly; try discriminate. destruct gvar_volatile; try discriminate. destruct gvar_info. auto. - right; auto. - rewrite PTree.grspec in H0. destruct (PTree.elt_eq id0 id); try discriminate. - right; auto. - unfold Genv.add_variable, Genv.find_symbol, Genv.find_var_info in *; + auto. + rewrite PTree.grspec in H0. destruct (PTree.elt_eq id0 id); [discriminate|auto]. + + unfold Genv.add_global, Genv.find_symbol, Genv.find_var_info in *; simpl in *. destruct EITHER as [[A B] | [A B]]. subst id0. rewrite PTree.gss in H1. inv H1. rewrite ZMap.gss. auto. - rewrite PTree.gso in H1; auto. rewrite ZMap.gso. eapply H. eauto. auto. + rewrite PTree.gso in H1; auto. destruct gd. eapply H; eauto. + rewrite ZMap.gso. eapply H; eauto. exploit Genv.genv_symb_range; eauto. unfold ZIndexed.t. omega. Qed. diff --git a/backend/Inlining.v b/backend/Inlining.v index 406447b..3ddfe9a 100644 --- a/backend/Inlining.v +++ b/backend/Inlining.v @@ -28,7 +28,7 @@ Ltac xomega := unfold Plt, Ple in *; zify; omega. (** ** Environment of inlinable functions *) (** We maintain a mapping from function names to their definitions. - In this mapping, we only include functions that are eligible for + In this mapping, we only include internal functions that are eligible for inlining, as determined by the external heuristic [should_inline]. *) @@ -38,22 +38,18 @@ Definition size_fenv (fenv: funenv) := PTree_Properties.cardinal fenv. Parameter should_inline: ident -> function -> bool. -Definition add_fundef (fenv: funenv) (idf: ident * fundef) : funenv := - match idf with - | (id, External ef) => - PTree.remove id fenv - | (id, Internal f) => +Definition add_globdef (fenv: funenv) (idg: ident * globdef fundef unit) : funenv := + match idg with + | (id, Gfun (Internal f)) => if should_inline id f then PTree.set id f fenv else PTree.remove id fenv + | (id, _) => + PTree.remove id fenv end. -Definition remove_vardef (fenv: funenv) (idv: ident * globvar unit) : funenv := - PTree.remove (fst idv) fenv. - Definition funenv_program (p: program) : funenv := - List.fold_left remove_vardef p.(prog_vars) - (List.fold_left add_fundef p.(prog_funct) (PTree.empty function)). + List.fold_left add_globdef p.(prog_defs) (PTree.empty function). (** Resources used by a function. *) diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index 9ca351a..8de8487 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -358,7 +358,8 @@ Inductive match_globalenvs (F: meminj) (bound: Z): Prop := (DOMAIN: forall b, b < bound -> F b = Some(b, 0)) (IMAGE: forall b1 b2 delta, F b1 = Some(b2, delta) -> b2 < bound -> b1 = b2) (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> b < bound) - (INFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound). + (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> b < bound) + (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound). Lemma find_function_agree: forall ros rs fd F ctx rs' bound, @@ -374,9 +375,9 @@ Proof. exploit Genv.find_funct_inv; eauto. intros [b EQ]. assert (A: val_inject F rs#r rs'#(sreg ctx r)). eapply agree_val_reg; eauto. rewrite EQ in A; inv A. - inv H1. rewrite DOMAIN in H5. inv H5. auto. - rewrite EQ in H; rewrite Genv.find_funct_find_funct_ptr in H. - exploit Genv.find_funct_ptr_negative. unfold ge in H; eexact H. omega. + inv H1. rewrite DOMAIN in H5. inv H5. auto. + apply FUNCTIONS with fd. + rewrite EQ in H; rewrite Genv.find_funct_find_funct_ptr in H. auto. rewrite H2. eapply functions_translated; eauto. (* symbol *) rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try discriminate. @@ -1219,7 +1220,8 @@ Proof. apply Mem.nextblock_pos. unfold Mem.flat_inj. apply zlt_true; auto. unfold Mem.flat_inj in H. destruct (zlt b1 (Mem.nextblock m0)); congruence. - eapply Genv.find_symbol_not_fresh; eauto. + eapply Genv.find_symbol_not_fresh; eauto. + eapply Genv.find_funct_ptr_not_fresh; eauto. eapply Genv.find_var_info_not_fresh; eauto. omega. eapply Genv.initmem_inject; eauto. diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v index ec72290..84bcdcd 100644 --- a/backend/Inliningspec.v +++ b/backend/Inliningspec.v @@ -35,43 +35,30 @@ Definition fenv_compat (ge: genv) (fenv: funenv) : Prop := fenv!id = Some f -> Genv.find_symbol ge id = Some b -> Genv.find_funct_ptr ge b = Some (Internal f). -Remark add_fundef_compat: - forall ge fenv idf, +Remark add_globdef_compat: + forall ge fenv idg, fenv_compat ge fenv -> - fenv_compat (Genv.add_function ge idf) (Inlining.add_fundef fenv idf). + fenv_compat (Genv.add_global ge idg) (Inlining.add_globdef fenv idg). Proof. - intros. destruct idf as [id fd]. red; simpl; intros. + intros. destruct idg as [id gd]. red; simpl; intros. unfold Genv.find_symbol in H1; simpl in H1. unfold Genv.find_funct_ptr; simpl. rewrite PTree.gsspec in H1. destruct (peq id0 id). (* same *) - subst id0. inv H1. rewrite ZMap.gss. - destruct fd. destruct (should_inline id f0). - rewrite PTree.gss in H0. inv H0; auto. + subst id0. inv H1. destruct gd. destruct f0. + destruct (should_inline id f0). + rewrite PTree.gss in H0. rewrite ZMap.gss. inv H0; auto. + rewrite PTree.grs in H0; discriminate. rewrite PTree.grs in H0; discriminate. rewrite PTree.grs in H0; discriminate. (* different *) - rewrite ZMap.gso. eapply H; eauto. - destruct fd. destruct (should_inline id f0). + destruct gd. rewrite ZMap.gso. eapply H; eauto. + destruct f0. destruct (should_inline id f0). rewrite PTree.gso in H0; auto. rewrite PTree.gro in H0; auto. rewrite PTree.gro in H0; auto. - exploit Genv.genv_symb_range; eauto. intros [A B]. unfold ZIndexed.t; omega. -Qed. - -Remark remove_vardef_compat: - forall ge fenv idv, - fenv_compat ge fenv -> - fenv_compat (Genv.add_variable ge idv) (Inlining.remove_vardef fenv idv). -Proof. - intros. destruct idv as [id vi]. red; simpl; intros. - unfold Genv.find_symbol in H1; simpl in H1. - unfold Genv.find_funct_ptr; simpl. - unfold remove_vardef in H0; simpl in H0. - rewrite PTree.gsspec in H1. rewrite PTree.grspec in H0. - unfold PTree.elt_eq in H0. destruct (peq id0 id). - discriminate. - eapply H; eauto. + exploit Genv.genv_symb_range; eauto. intros [A B]. unfold ZIndexed.t; omega. + rewrite PTree.gro in H0; auto. eapply H; eauto. Qed. Lemma funenv_program_compat: @@ -79,17 +66,11 @@ Lemma funenv_program_compat: Proof. intros. unfold Genv.globalenv, funenv_program. - assert (forall funs ge fenv, - fenv_compat ge fenv -> - fenv_compat (Genv.add_functions ge funs) (fold_left add_fundef funs fenv)). - unfold Genv.add_functions. induction funs; simpl; intros. - auto. apply IHfuns. apply add_fundef_compat; auto. - assert (forall vars ge fenv, + assert (forall gl ge fenv, fenv_compat ge fenv -> - fenv_compat (Genv.add_variables ge vars) (fold_left remove_vardef vars fenv)). - unfold Genv.add_variables. induction vars; simpl; intros. - auto. apply IHvars. apply remove_vardef_compat; auto. - apply H0. apply H. red; intros. rewrite PTree.gempty in H1; discriminate. + fenv_compat (Genv.add_globals ge gl) (fold_left add_globdef gl fenv)). + induction gl; simpl; intros. auto. apply IHgl. apply add_globdef_compat; auto. + apply H. red; intros. rewrite PTree.gempty in H0; discriminate. Qed. (** ** Soundness of the computed bounds over function resources *) diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v index 1a20f73..e9cc2df 100644 --- a/backend/LTLintyping.v +++ b/backend/LTLintyping.v @@ -122,4 +122,4 @@ Inductive wt_fundef: fundef -> Prop := wt_fundef (Internal f). Definition wt_program (p: program): Prop := - forall i f, In (i, f) (prog_funct p) -> wt_fundef f. + forall i f, In (i, Gfun f) (prog_defs p) -> wt_fundef f. diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v index 40a584f..2e627e9 100644 --- a/backend/LTLtyping.v +++ b/backend/LTLtyping.v @@ -142,4 +142,4 @@ Inductive wt_fundef: fundef -> Prop := wt_fundef (Internal f). Definition wt_program (p: program): Prop := - forall i f, In (i, f) (prog_funct p) -> wt_fundef f. + forall i f, In (i, Gfun f) (prog_defs p) -> wt_fundef f. diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 3930da3..da73b00 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -133,7 +133,7 @@ Inductive wt_fundef: fundef -> Prop := wt_fundef (Internal f). Definition wt_program (p: program) : Prop := - forall i f, In (i, f) (prog_funct p) -> wt_fundef f. + forall i f, In (i, Gfun f) (prog_defs p) -> wt_fundef f. (** Typing the run-time state. These definitions are used in [Stackingproof]. *) diff --git a/backend/Machtyping.v b/backend/Machtyping.v index 2d8c83d..b9d8009 100644 --- a/backend/Machtyping.v +++ b/backend/Machtyping.v @@ -111,4 +111,4 @@ Inductive wt_fundef: fundef -> Prop := wt_fundef (Internal f). Definition wt_program (p: program) : Prop := - forall i f, In (i, f) (prog_funct p) -> wt_fundef f. + forall i f, In (i, Gfun f) (prog_defs p) -> wt_fundef f. diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index 858ef21..8e49303 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -273,13 +273,6 @@ let print_extfun p id ef = fprintf p "@[<v 0>extern @[<hov 2>\"%s\":@ %a@]@ " (extern_atom id) print_sig (ef_sig ef) -let print_fundef p (id, fd) = - match fd with - | External ef -> - print_extfun p id ef - | Internal f -> - print_function p id f - let print_init_data p = function | Init_int8 i -> fprintf p "int8 %ld" (camlint_of_coqint i) | Init_int16 i -> fprintf p "int16 %ld" (camlint_of_coqint i) @@ -306,14 +299,18 @@ let print_globvar p gv = print_init_data_list p gv.gvar_init; fprintf p "}" -let print_var p (id, gv) = - fprintf p "var \"%s\" %a\n" (extern_atom id) print_globvar gv +let print_globdef p (id, gd) = + match gd with + | Gfun(External ef) -> + print_extfun p id ef + | Gfun(Internal f) -> + print_function p id f + | Gvar gv -> + fprintf p "var \"%s\" %a\n" (extern_atom id) print_globvar gv let print_program p prog = - fprintf p "@[<v>"; - List.iter (print_var p) prog.prog_vars; - fprintf p "@]@[<v 0>"; - List.iter (print_fundef p) prog.prog_funct; + fprintf p "@[<v 0>"; + List.iter (print_globdef p) prog.prog_defs; fprintf p "@]@." let destination : string option ref = ref None diff --git a/backend/PrintLTLin.ml b/backend/PrintLTLin.ml index bb360eb..4dc311c 100644 --- a/backend/PrintLTLin.ml +++ b/backend/PrintLTLin.ml @@ -95,13 +95,13 @@ let print_function pp id f = List.iter (print_instruction pp) f.fn_code; fprintf pp "@;<0 -2>}@]@." -let print_fundef pp (id, fd) = - match fd with - | Internal f -> print_function pp id f - | External _ -> () +let print_globdef pp (id, gd) = + match gd with + | Gfun(Internal f) -> print_function pp id f + | _ -> () let print_program pp prog = - List.iter (print_fundef pp) prog.prog_funct + List.iter (print_globdef pp) prog.prog_defs let destination : string option ref = ref None diff --git a/backend/PrintMach.ml b/backend/PrintMach.ml index 03977a6..dfbc66e 100644 --- a/backend/PrintMach.ml +++ b/backend/PrintMach.ml @@ -102,13 +102,13 @@ let print_function pp id f = List.iter (print_instruction pp) f.fn_code; fprintf pp "@;<0 -2>}@]@." -let print_fundef pp (id, fd) = - match fd with - | Internal f -> print_function pp id f - | External _ -> () +let print_globdef pp (id, gd) = + match gd with + | Gfun(Internal f) -> print_function pp id f + | _ -> () let print_program pp prog = - List.iter (print_fundef pp) prog.prog_funct + List.iter (print_globdef pp) prog.prog_defs let destination : string option ref = ref None diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml index 4fc8f56..4cd3871 100644 --- a/backend/PrintRTL.ml +++ b/backend/PrintRTL.ml @@ -103,13 +103,13 @@ let print_function pp id f = List.iter (print_instruction pp) instrs; fprintf pp "@;<0 -2>}@]@." -let print_fundef pp (id, fd) = - match fd with - | Internal f -> print_function pp id f - | External _ -> () +let print_globdef pp (id, gd) = + match gd with + | Gfun(Internal f) -> print_function pp id f + | _ -> () let print_program pp (prog: RTL.program) = - List.iter (print_fundef pp) prog.prog_funct + List.iter (print_globdef pp) prog.prog_defs let print_if optdest prog = match !optdest with diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index 65506c8..a14e944 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -158,7 +158,7 @@ Inductive wt_fundef: fundef -> Prop := wt_fundef (Internal f). Definition wt_program (p: program): Prop := - forall i f, In (i, f) (prog_funct p) -> wt_fundef f. + forall i f, In (i, Gfun f) (prog_defs p) -> wt_fundef f. (** * Type inference *) diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 1cfb738..1d87ad3 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -1734,7 +1734,8 @@ Inductive match_globalenvs (j: meminj) (bound: Z) : Prop := (DOMAIN: forall b, b < bound -> j b = Some(b, 0)) (IMAGE: forall b1 b2 delta, j b1 = Some(b2, delta) -> b2 < bound -> b1 = b2) (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> b < bound) - (INFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound). + (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> b < bound) + (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound). Inductive match_stacks (j: meminj) (m m': mem): list Linear.stackframe -> list stackframe -> signature -> Z -> Z -> Prop := @@ -2170,9 +2171,8 @@ Proof. exploit function_ptr_translated; eauto. intros [tf [A B]]. exists b; exists tf; split; auto. simpl. generalize (AG m0). rewrite EQ. intro INJ. inv INJ. - exploit Genv.find_funct_ptr_negative. unfold ge in FF; eexact FF. intros. - inv MG. rewrite (DOMAIN b) in H2. inv H2. auto. omega. - revert FF. case_eq (Genv.find_symbol ge i); intros; try discriminate. + inv MG. rewrite DOMAIN in H2. inv H2. simpl. auto. eapply FUNCTIONS; eauto. + destruct (Genv.find_symbol ge i) as [b|]_eqn; try discriminate. exploit function_ptr_translated; eauto. intros [tf [A B]]. exists b; exists tf; split; auto. simpl. rewrite symbols_preserved. auto. @@ -2742,6 +2742,7 @@ Proof. intros. unfold Mem.flat_inj. apply zlt_true; auto. unfold Mem.flat_inj; intros. destruct (zlt b1 (Mem.nextblock m0)); congruence. intros. change (Mem.valid_block m0 b0). eapply Genv.find_symbol_not_fresh; eauto. + intros. change (Mem.valid_block m0 b0). eapply Genv.find_funct_ptr_not_fresh; eauto. intros. change (Mem.valid_block m0 b0). eapply Genv.find_var_info_not_fresh; eauto. rewrite H3. red; intros. contradiction. eapply Genv.find_funct_ptr_prop. eexact wt_prog. diff --git a/backend/Unusedglob.ml b/backend/Unusedglob.ml index 4139678..1a88ee9 100644 --- a/backend/Unusedglob.ml +++ b/backend/Unusedglob.ml @@ -28,10 +28,6 @@ let add_referenced_instr rf i = let referenced_function f = List.fold_left add_referenced_instr IdentSet.empty (code_of_function f) -let referenced_fundef = function - | Internal f -> referenced_function f - | External ef -> IdentSet.empty - (* The set of globals referenced from a variable definition (initialization) *) let add_referenced_init_data rf = function @@ -43,10 +39,15 @@ let referenced_globvar gv = (* The map global |-> set of globals it references *) +let referenced_globdef gd = + match gd with + | Gfun(Internal f) -> referenced_function f + | Gfun(External ef) -> IdentSet.empty + | Gvar gv -> referenced_globvar gv + let use_map p = - List.fold_left (fun m (id, gv) -> PTree.set id (referenced_globvar gv) m) - (List.fold_left (fun m (id, fd) -> PTree.set id (referenced_fundef fd) m) - PTree.empty p.prog_funct) p.prog_vars + List.fold_left (fun m (id, gd) -> PTree.set id (referenced_globdef gd) m) + PTree.empty p.prog_defs (* Worklist algorithm computing the set of used globals *) @@ -66,9 +67,8 @@ let add_nonstatic wrk id = if C2C.atom_is_static id then wrk else id :: wrk let initial_worklist p = - List.fold_left (fun wrk (id, gv) -> add_nonstatic wrk id) - (List.fold_left (fun wrk (id, fd) -> add_nonstatic wrk id) - [] p.prog_funct) p.prog_vars + List.fold_left (fun wrk (id, gd) -> add_nonstatic wrk id) + [] p.prog_defs (* Eliminate unused definitions *) @@ -80,9 +80,8 @@ let rec filter used = function else filter used rem let filter_prog used p = - { prog_funct = filter used p.prog_funct; - prog_main = p.prog_main; - prog_vars = filter used p.prog_vars } + { prog_defs = filter used p.prog_defs; + prog_main = p.prog_main } (* Entry point *) diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index c659b86..2cdcc03 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -137,8 +137,8 @@ let global_for_string s id = :: !init in add_char '\000'; for i = String.length s - 1 downto 0 do add_char s.[i] done; - (id, {gvar_info = typeStringLiteral s; gvar_init = !init; - gvar_readonly = true; gvar_volatile = false}) + (id, Gvar {gvar_info = typeStringLiteral s; gvar_init = !init; + gvar_readonly = true; gvar_volatile = false}) let globals_for_strings globs = Hashtbl.fold @@ -155,7 +155,7 @@ let register_special_external name ef targs tres = let declare_special_externals k = Hashtbl.fold - (fun name fd k -> (intern_string name, fd) :: k) + (fun name fd k -> (intern_string name, Gfun fd) :: k) special_externals_table k (** ** Handling of stubs for variadic functions *) @@ -709,8 +709,8 @@ let convertFundef env fd = a_sections = Sections.for_function env id' fd.fd_ret; a_small_data = false; a_inline = fd.fd_inline }; - (id', Internal {fn_return = ret; fn_params = params; - fn_vars = vars; fn_body = body'}) + (id', Gfun(Internal {fn_return = ret; fn_params = params; + fn_vars = vars; fn_body = body'})) (** External function declaration *) @@ -727,7 +727,7 @@ let convertFundecl env (sto, id, ty, optinit) = if List.mem_assoc id.name builtins.functions then EF_builtin(id', sg) else EF_external(id', sg) in - (id', External(ef, args, res)) + (id', Gfun(External(ef, args, res))) (** Initializers *) @@ -788,8 +788,8 @@ let convertGlobvar env (sto, id, ty, optinit) = a_inline = false }; let volatile = List.mem C.AVolatile attr in let readonly = List.mem C.AConst attr && not volatile in - (id', {gvar_info = ty'; gvar_init = init'; - gvar_readonly = readonly; gvar_volatile = volatile}) + (id', Gvar {gvar_info = ty'; gvar_init = init'; + gvar_readonly = readonly; gvar_volatile = volatile}) (** Sanity checks on composite declarations. *) @@ -803,13 +803,12 @@ let checkComposite env si id attr flds = in List.iter checkField flds (** Convert a list of global declarations. - Result is a pair [(funs, vars)] where [funs] are - the function definitions (internal and external) - and [vars] the variable declarations. *) + Result is a list of CompCert C global declarations (functions + + variables). *) -let rec convertGlobdecls env funs vars gl = +let rec convertGlobdecls env res gl = match gl with - | [] -> (List.rev funs, List.rev vars) + | [] -> List.rev res | g :: gl' -> updateLoc g.gloc; match g.gdesc with @@ -819,29 +818,29 @@ let rec convertGlobdecls env funs vars gl = Other types become variable declarations. *) begin match Cutil.unroll env ty with | TFun(_, Some _, false, _) -> - convertGlobdecls env (convertFundecl env d :: funs) vars gl' + convertGlobdecls env (convertFundecl env d :: res) gl' | TFun(_, None, false, _) -> error "function declaration without prototype"; - convertGlobdecls env funs vars gl' + convertGlobdecls env res gl' | TFun(_, _, true, _) -> - convertGlobdecls env funs vars gl' + convertGlobdecls env res gl' | _ -> - convertGlobdecls env funs (convertGlobvar env d :: vars) gl' + convertGlobdecls env (convertGlobvar env d :: res) gl' end | C.Gfundef fd -> - convertGlobdecls env (convertFundef env fd :: funs) vars gl' + convertGlobdecls env (convertFundef env fd :: res) gl' | C.Gcompositedecl _ | C.Gtypedef _ | C.Genumdef _ -> (* typedefs are unrolled, structs are expanded inline, and enum tags are folded. So we just skip their declarations. *) - convertGlobdecls env funs vars gl' + convertGlobdecls env res gl' | C.Gcompositedef(su, id, attr, flds) -> (* sanity checks on fields *) checkComposite env su id attr flds; - convertGlobdecls env funs vars gl' + convertGlobdecls env res gl' | C.Gpragma s -> if not (!process_pragma_hook s) then warning ("'#pragma " ^ s ^ "' directive ignored"); - convertGlobdecls env funs vars gl' + convertGlobdecls env res gl' (** Build environment of typedefs and structs *) @@ -921,14 +920,12 @@ let convertProgram p = Hashtbl.clear special_externals_table; let p = Builtins.declarations() @ p in try - let (funs1, vars1) = - convertGlobdecls (translEnv Env.empty p) [] [] (cleanupGlobals p) in - let funs2 = declare_special_externals funs1 in - let vars2 = globals_for_strings vars1 in + let gl1 = convertGlobdecls (translEnv Env.empty p) [] (cleanupGlobals p) in + let gl2 = declare_special_externals gl1 in + let gl3 = globals_for_strings gl2 in if !numErrors > 0 then None - else Some { AST.prog_funct = funs2; - AST.prog_vars = vars2; + else Some { AST.prog_defs = gl3; AST.prog_main = intern_string "main" } with Env.Error msg -> error (Env.error_message msg); None diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index 2c02813..a47efb2 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -565,19 +565,19 @@ Definition build_compilenv (fn_variables f) (globenv, 0). -Definition assign_global_variable - (ce: compilenv) (info: ident * globvar var_kind) : compilenv := - match info with - | (id, mkglobvar vk _ _ _) => - PMap.set id (match vk with Vscalar chunk => Var_global_scalar chunk - | Varray _ _ => Var_global_array - end) - ce - end. +Definition assign_global_def + (ce: compilenv) (gdef: ident * globdef Csharpminor.fundef var_kind) : compilenv := + let (id, gd) := gdef in + let kind := + match gd with + | Gvar (mkglobvar (Vscalar chunk) _ _ _) => Var_global_scalar chunk + | Gvar (mkglobvar (Varray _ _) _ _ _) => Var_global_array + | Gfun f => Var_global_array + end in + PMap.set id kind ce. Definition build_global_compilenv (p: Csharpminor.program) : compilenv := - List.fold_left assign_global_variable - p.(prog_vars) (PMap.init Var_global_array). + List.fold_left assign_global_def p.(prog_defs) (PMap.init Var_global_array). (** * Translation of functions *) diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 0fa9ac0..42f54b3 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -109,23 +109,28 @@ Lemma global_compilenv_charact: Proof. assert (A: forall ge, global_compilenv_match (PMap.init Var_global_array) ge). intros; red; intros. rewrite PMap.gi. auto. - assert (B: forall ce ge v, + assert (B: forall ce ge idg, global_compilenv_match ce ge -> - global_compilenv_match (assign_global_variable ce v) - (Genv.add_variable ge v)). - intros; red; intros. destruct v as [id1 [info1 init1 ro1 vo1]]. - unfold assign_global_variable, Genv.find_symbol, Genv.find_var_info; simpl. - rewrite PMap.gsspec. destruct (peq id id1). subst id. + global_compilenv_match (assign_global_def ce idg) + (Genv.add_global ge idg)). + intros; red; intros. unfold assign_global_def. + destruct idg as [id1 gd]. rewrite PMap.gsspec. destruct (peq id id1). + (* same var *) + subst id1. destruct gd as [f | [info1 init1 ro1 vo1]]. auto. destruct info1; auto. - rewrite PTree.gss. intros. inv H0. rewrite ZMap.gss in H1. inv H1. auto. - generalize (H id). destruct (ce!!id); auto. - rewrite PTree.gso; auto. intros. rewrite ZMap.gso in H2. eapply H0; eauto. + unfold Genv.find_symbol, Genv.find_var_info. simpl; intros. + rewrite PTree.gss in H0. inv H0. rewrite ZMap.gss in H1. inv H1; auto. + (* different var *) + generalize (H id). unfold Genv.find_symbol, Genv.find_var_info. simpl. intros. + destruct (ce!!id); auto. intros. + rewrite PTree.gso in H1; auto. + destruct gd as [f|v]. eauto. rewrite ZMap.gso in H2. eauto. exploit Genv.genv_symb_range; eauto. unfold block, ZIndexed.t; omega. - assert (C: forall vl ce ge, + assert (C: forall gl ce ge, global_compilenv_match ce ge -> - global_compilenv_match (fold_left assign_global_variable vl ce) - (Genv.add_variables ge vl)). - induction vl; simpl; intros. auto. apply IHvl. apply B. auto. + global_compilenv_match (fold_left assign_global_def gl ce) + (Genv.add_globals ge gl)). + induction gl; simpl; intros. auto. apply IHgl. apply B. auto. unfold gce, build_global_compilenv, ge, Genv.globalenv. apply C. apply A. @@ -680,7 +685,8 @@ Inductive match_globalenvs (f: meminj) (bound: Z): Prop := (DOMAIN: forall b, b < bound -> f b = Some(b, 0)) (IMAGE: forall b1 b2 delta, f b1 = Some(b2, delta) -> b2 < bound -> b1 = b2) (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> b < bound) - (INFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound). + (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> b < bound) + (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound). (** Matching of call stacks imply: - matching of environments for each of the frames @@ -1132,7 +1138,7 @@ Remark inj_preserves_globals: Proof. intros. inv H. split. intros. apply DOMAIN. eapply SYMBOLS. eauto. - split. intros. apply DOMAIN. eapply INFOS. eauto. + split. intros. apply DOMAIN. eapply VARINFOS. eauto. intros. symmetry. eapply IMAGE; eauto. Qed. @@ -2822,16 +2828,15 @@ Inductive match_states: Csharpminor.state -> Cminor.state -> Prop := Remark val_inject_function_pointer: forall bound v fd f tv, - Genv.find_funct tge v = Some fd -> + Genv.find_funct ge v = Some fd -> match_globalenvs f bound -> val_inject f v tv -> tv = v. Proof. intros. exploit Genv.find_funct_inv; eauto. intros [b EQ]. subst v. - rewrite Genv.find_funct_find_funct_ptr in H. - assert (b < 0). unfold tge in H. eapply Genv.find_funct_ptr_negative; eauto. - assert (f b = Some(b, 0)). inv H0. apply DOMAIN. omega. - inv H1. rewrite H3 in H6; inv H6. reflexivity. + rewrite Genv.find_funct_find_funct_ptr in H. + assert (f b = Some(b, 0)). inv H0. apply DOMAIN. eapply FUNCTIONS; eauto. + inv H1. rewrite H2 in H5; inv H5. reflexivity. Qed. Lemma match_call_cont: @@ -3426,6 +3431,7 @@ Proof. intros. unfold Mem.flat_inj in H0. destruct (zlt b1 (Mem.nextblock m)); congruence. intros. eapply Genv.find_symbol_not_fresh; eauto. + intros. eapply Genv.find_funct_ptr_not_fresh; eauto. intros. eapply Genv.find_var_info_not_fresh; eauto. Qed. diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index c5e9b8d..a459297 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -546,8 +546,16 @@ with transl_lbl_stmt (tyret: type) (nbrk ncnt: nat) Definition prefix_var_name (id: ident) : errmsg := MSG "In local variable " :: CTX id :: MSG ": " :: nil. -Definition transl_vars (l: list (ident * type)) := - AST.map_partial prefix_var_name var_kind_of_type l. +Fixpoint transl_vars (l: list (ident * type)) : res (list (ident * var_kind)) := + match l with + | nil => OK nil + | (id, ty) :: l' => + match var_kind_of_type ty with + | Error msg => Error (MSG "In local variable " :: CTX id :: MSG ": " :: msg) + | OK vk => + do tl' <- transl_vars l'; OK ((id, vk) :: tl') + end + end. Definition transl_function (f: Clight.function) : res function := do tparams <- transl_vars (Clight.fn_params f); diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 9f73467..2f319d0 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -214,39 +214,15 @@ Qed. (** * Properties of the translation functions *) -Lemma map_partial_names: - forall (A B: Type) (f: A -> res B) - (l: list (ident * A)) (tl: list (ident * B)), - map_partial prefix_var_name f l = OK tl -> - List.map (@fst ident B) tl = List.map (@fst ident A) l. -Proof. - induction l; simpl. - intros. inversion H. reflexivity. - intro tl. destruct a as [id x]. destruct (f x); try congruence. - caseEq (map_partial prefix_var_name f l); simpl; intros; try congruence. - inv H0. simpl. decEq. auto. -Qed. - -Lemma map_partial_append: - forall (A B: Type) (f: A -> res B) - (l1 l2: list (ident * A)) (tl1 tl2: list (ident * B)), - map_partial prefix_var_name f l1 = OK tl1 -> - map_partial prefix_var_name f l2 = OK tl2 -> - map_partial prefix_var_name f (l1 ++ l2) = OK (tl1 ++ tl2). -Proof. - induction l1; intros until tl2; simpl. - intros. inversion H. simpl; auto. - destruct a as [id x]. destruct (f x); try congruence. - caseEq (map_partial prefix_var_name f l1); simpl; intros; try congruence. - inv H0. rewrite (IHl1 _ _ _ H H1). auto. -Qed. - Lemma transl_vars_names: forall vars tvars, transl_vars vars = OK tvars -> List.map variable_name tvars = var_names vars. Proof. - exact (map_partial_names _ _ var_kind_of_type). + induction vars; simpl; intros. + monadInv H. auto. + destruct a as [id ty]. destruct (var_kind_of_type ty); monadInv H. + simpl. decEq; auto. Qed. Lemma transl_names_norepet: @@ -268,7 +244,10 @@ Lemma transl_vars_append: transl_vars l1 = OK tl1 -> transl_vars l2 = OK tl2 -> transl_vars (l1 ++ l2) = OK (tl1 ++ tl2). Proof. - exact (map_partial_append _ _ var_kind_of_type). + induction l1; simpl; intros. + inv H. auto. + destruct a as [id ty]. destruct (var_kind_of_type ty); monadInv H. + erewrite IHl1; eauto. simpl. auto. Qed. Lemma transl_fn_variables: diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index 7b9f3d3..0e8b494 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -249,7 +249,7 @@ let print_function p id f = print_stmt p f.fn_body; fprintf p "@;<0 -2>}@]@ @ " -let print_fundef p (id, fd) = +let print_fundef p id fd = match fd with | External(EF_external(_,_), args, res) -> fprintf p "extern %s;@ @ " @@ -259,6 +259,11 @@ let print_fundef p (id, fd) = | Internal f -> print_function p id f +let print_globdef p (id, gd) = + match gd with + | Gfun f -> print_fundef p id f + | Gvar v -> print_globvar p id v (* from PrintCsyntax *) + (* Collect struct and union types *) let rec collect_expr e = @@ -307,17 +312,14 @@ let collect_function f = List.iter (fun (id, ty) -> collect_type ty) f.fn_temps; collect_stmt f.fn_body -let collect_fundef (id, fd) = - match fd with - | External(_, args, res) -> collect_type_list args; collect_type res - | Internal f -> collect_function f - -let collect_globvar (id, v) = - collect_type v.gvar_info +let collect_globdef (id, gd) = + match gd with + | Gfun(External(_, args, res)) -> collect_type_list args; collect_type res + | Gfun(Internal f) -> collect_function f + | Gvar v -> collect_type v.gvar_info let collect_program p = - List.iter collect_globvar p.prog_vars; - List.iter collect_fundef p.prog_funct + List.iter collect_globdef p.prog_defs let declare_struct_or_union p (name, fld) = fprintf p "%s;@ @ " name @@ -338,8 +340,7 @@ let print_program p prog = fprintf p "@[<v 0>"; StructUnionSet.iter (declare_struct_or_union p) !struct_unions; StructUnionSet.iter (print_struct_or_union p) !struct_unions; - List.iter (print_globvar p) prog.prog_vars; - List.iter (print_fundef p) prog.prog_funct; + List.iter (print_globdef p) prog.prog_defs; fprintf p "@]@." let destination : string option ref = ref None diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 5490321..7858545 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -372,7 +372,7 @@ let print_function p id f = print_stmt p f.fn_body; fprintf p "@;<0 -2>}@]@ @ " -let print_fundef p (id, fd) = +let print_fundef p id fd = match fd with | External(EF_external(_,_), args, res) -> fprintf p "extern %s;@ @ " @@ -414,7 +414,7 @@ let print_init p = function let re_string_literal = Str.regexp "__stringlit_[0-9]+" -let print_globvar p (id, v) = +let print_globvar p id v = let name1 = extern_atom id in let name2 = if v.gvar_readonly then "const " ^ name1 else name1 in let name3 = if v.gvar_volatile then "volatile " ^ name2 else name2 in @@ -439,6 +439,11 @@ let print_globvar p (id, v) = end; fprintf p ";@]@ @ " +let print_globdef p (id, gd) = + match gd with + | Gfun f -> print_fundef p id f + | Gvar v -> print_globvar p id v + (* Collect struct and union types *) let rec collect_type = function @@ -519,17 +524,14 @@ let collect_function f = List.iter (fun (id, ty) -> collect_type ty) f.fn_vars; collect_stmt f.fn_body -let collect_fundef (id, fd) = - match fd with - | External(_, args, res) -> collect_type_list args; collect_type res - | Internal f -> collect_function f - -let collect_globvar (id, v) = - collect_type v.gvar_info +let collect_globdef (id, gd) = + match gd with + | Gfun(External(_, args, res)) -> collect_type_list args; collect_type res + | Gfun(Internal f) -> collect_function f + | Gvar v -> collect_type v.gvar_info let collect_program p = - List.iter collect_globvar p.prog_vars; - List.iter collect_fundef p.prog_funct + List.iter collect_globdef p.prog_defs let declare_struct_or_union p (name, fld) = fprintf p "%s;@ @ " name @@ -550,8 +552,7 @@ let print_program p prog = fprintf p "@[<v 0>"; StructUnionSet.iter (declare_struct_or_union p) !struct_unions; StructUnionSet.iter (print_struct_or_union p) !struct_unions; - List.iter (print_globvar p) prog.prog_vars; - List.iter (print_fundef p) prog.prog_funct; + List.iter (print_globdef p) prog.prog_defs; fprintf p "@]@." let destination : string option ref = ref None diff --git a/common/AST.v b/common/AST.v index 6425cb0..ccc9dbf 100644 --- a/common/AST.v +++ b/common/AST.v @@ -118,44 +118,29 @@ Record globvar (V: Type) : Type := mkglobvar { }. (** Whole programs consist of: -- a collection of function definitions (name and description); -- the name of the ``main'' function that serves as entry point in the program; -- a collection of global variable declarations (name and information). +- a collection of global definitions (name and description); +- the name of the ``main'' function that serves as entry point in the program. +A global definition is either a global function or a global variable. The type of function descriptions and that of additional information for variables vary among the various intermediate languages and are taken as parameters to the [program] type. The other parts of whole programs are common to all languages. *) -Record program (F V: Type) : Type := mkprogram { - prog_funct: list (ident * F); - prog_main: ident; - prog_vars: list (ident * globvar V) -}. +Inductive globdef (F V: Type) : Type := + | Gfun (f: F) + | Gvar (v: globvar V). -Definition funct_names (F: Type) (fl: list (ident * F)) : list ident := - map (@fst ident F) fl. +Implicit Arguments Gfun [F V]. +Implicit Arguments Gvar [F V]. -Lemma funct_names_app : forall (F: Type) (fl1 fl2 : list (ident * F)), - funct_names (fl1 ++ fl2) = funct_names fl1 ++ funct_names fl2. -Proof. - intros; unfold funct_names; apply list_append_map. -Qed. - -Definition var_names (V: Type) (vl: list (ident * globvar V)) : list ident := - map (@fst ident (globvar V)) vl. - -Lemma var_names_app : forall (V: Type) (vl1 vl2 : list (ident * globvar V)), - var_names (vl1 ++ vl2) = var_names vl1 ++ funct_names vl2. -Proof. - intros; unfold var_names; apply list_append_map. -Qed. - -Definition prog_funct_names (F V: Type) (p: program F V) : list ident := - funct_names p.(prog_funct). +Record program (F V: Type) : Type := mkprogram { + prog_defs: list (ident * globdef F V); + prog_main: ident +}. -Definition prog_var_names (F V: Type) (p: program F V) : list ident := - var_names p.(prog_vars). +Definition prog_defs_names (F V: Type) (p: program F V) : list ident := + List.map fst p.(prog_defs). (** * Generic transformations over programs *) @@ -168,253 +153,195 @@ Section TRANSF_PROGRAM. Variable A B V: Type. Variable transf: A -> B. -Definition transf_program (l: list (ident * A)) : list (ident * B) := - List.map (fun id_fn => (fst id_fn, transf (snd id_fn))) l. +Definition transform_program_globdef (idg: ident * globdef A V) : ident * globdef B V := + match idg with + | (id, Gfun f) => (id, Gfun (transf f)) + | (id, Gvar v) => (id, Gvar v) + end. Definition transform_program (p: program A V) : program B V := mkprogram - (transf_program p.(prog_funct)) - p.(prog_main) - p.(prog_vars). + (List.map transform_program_globdef p.(prog_defs)) + p.(prog_main). Lemma transform_program_function: forall p i tf, - In (i, tf) (transform_program p).(prog_funct) -> - exists f, In (i, f) p.(prog_funct) /\ transf f = tf. + In (i, Gfun tf) (transform_program p).(prog_defs) -> + exists f, In (i, Gfun f) p.(prog_defs) /\ transf f = tf. Proof. - simpl. unfold transf_program. intros. + simpl. unfold transform_program. intros. exploit list_in_map_inv; eauto. - intros [[i' f] [EQ IN]]. simpl in EQ. inversion EQ; subst. - exists f; split; auto. + intros [[i' gd] [EQ IN]]. simpl in EQ. destruct gd; inv EQ. + exists f; auto. Qed. End TRANSF_PROGRAM. -(** The following is a variant of [transform_program] where the - code transformation function can fail and therefore returns an - option type. *) +(** The following is a more general presentation of [transform_program] where + global variable information can be transformed, in addition to function + definitions. Moreover, the transformation functions can fail and + return an error message. *) Open Local Scope error_monad_scope. Open Local Scope string_scope. -Section MAP_PARTIAL. +Section TRANSF_PROGRAM_GEN. -Variable A B C: Type. -Variable prefix_errmsg: A -> errmsg. -Variable f: B -> res C. +Variables A B V W: Type. +Variable transf_fun: A -> res B. +Variable transf_var: V -> res W. + +Definition transf_globvar (g: globvar V) : res (globvar W) := + do info' <- transf_var g.(gvar_info); + OK (mkglobvar info' g.(gvar_init) g.(gvar_readonly) g.(gvar_volatile)). -Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) := +Fixpoint transf_globdefs (l: list (ident * globdef A V)) : res (list (ident * globdef B W)) := match l with | nil => OK nil - | (a, b) :: rem => - match f b with - | Error msg => Error (prefix_errmsg a ++ msg)%list - | OK c => - do rem' <- map_partial rem; - OK ((a, c) :: rem') + | (id, Gfun f) :: l' => + match transf_fun f with + | Error msg => Error (MSG "In function " :: CTX id :: MSG ": " :: msg) + | OK tf => + do tl' <- transf_globdefs l'; OK ((id, Gfun tf) :: tl') + end + | (id, Gvar v) :: l' => + match transf_globvar v with + | Error msg => Error (MSG "In variable " :: CTX id :: MSG ": " :: msg) + | OK tv => + do tl' <- transf_globdefs l'; OK ((id, Gvar tv) :: tl') end end. -Remark In_map_partial: - forall l l' a c, - map_partial l = OK l' -> - In (a, c) l' -> - exists b, In (a, b) l /\ f b = OK c. -Proof. - induction l; simpl. - intros. inv H. elim H0. - intros until c. destruct a as [a1 b1]. - caseEq (f b1); try congruence. - intro c1; intros. monadInv H0. - elim H1; intro. inv H0. exists b1; auto. - exploit IHl; eauto. intros [b [P Q]]. exists b; auto. -Qed. +Definition transform_partial_program2 (p: program A V) : res (program B W) := + do gl' <- transf_globdefs p.(prog_defs); OK(mkprogram gl' p.(prog_main)). -Remark map_partial_forall2: - forall l l', - map_partial l = OK l' -> - list_forall2 - (fun (a_b: A * B) (a_c: A * C) => - fst a_b = fst a_c /\ f (snd a_b) = OK (snd a_c)) - l l'. +Lemma transform_partial_program2_function: + forall p tp i tf, + transform_partial_program2 p = OK tp -> + In (i, Gfun tf) tp.(prog_defs) -> + exists f, In (i, Gfun f) p.(prog_defs) /\ transf_fun f = OK tf. Proof. - induction l; simpl. - intros. inv H. constructor. - intro l'. destruct a as [a b]. - caseEq (f b). 2: congruence. intro c; intros. monadInv H0. - constructor. simpl. auto. auto. + intros. monadInv H. simpl in H0. + revert x EQ H0. induction (prog_defs p); simpl; intros. + inv EQ. contradiction. + destruct a as [id [f|v]]. + destruct (transf_fun f) as [tf1|msg]_eqn; monadInv EQ. + simpl in H0; destruct H0. inv H. exists f; auto. + exploit IHl; eauto. intros [f' [P Q]]; exists f'; auto. + destruct (transf_globvar v) as [tv1|msg]_eqn; monadInv EQ. + simpl in H0; destruct H0. inv H. + exploit IHl; eauto. intros [f' [P Q]]; exists f'; auto. Qed. -End MAP_PARTIAL. - -Remark map_partial_total: - forall (A B C: Type) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)), - map_partial prefix (fun b => OK (f b)) l = - OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l). +Lemma transform_partial_program2_variable: + forall p tp i tv, + transform_partial_program2 p = OK tp -> + In (i, Gvar tv) tp.(prog_defs) -> + exists v, + In (i, Gvar(mkglobvar v tv.(gvar_init) tv.(gvar_readonly) tv.(gvar_volatile))) p.(prog_defs) + /\ transf_var v = OK tv.(gvar_info). Proof. - induction l; simpl. - auto. - destruct a as [a1 b1]. rewrite IHl. reflexivity. + intros. monadInv H. simpl in H0. + revert x EQ H0. induction (prog_defs p); simpl; intros. + inv EQ. contradiction. + destruct a as [id [f|v]]. + destruct (transf_fun f) as [tf1|msg]_eqn; monadInv EQ. + simpl in H0; destruct H0. inv H. + exploit IHl; eauto. intros [v' [P Q]]; exists v'; auto. + destruct (transf_globvar v) as [tv1|msg]_eqn; monadInv EQ. + simpl in H0; destruct H0. inv H. + monadInv Heqr. simpl. exists (gvar_info v). split. left. destruct v; auto. auto. + exploit IHl; eauto. intros [v' [P Q]]; exists v'; auto. Qed. -Remark map_partial_identity: - forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)), - map_partial prefix (fun b => OK b) l = OK l. +Lemma transform_partial_program2_main: + forall p tp, + transform_partial_program2 p = OK tp -> + tp.(prog_main) = p.(prog_main). Proof. - induction l; simpl. - auto. - destruct a as [a1 b1]. rewrite IHl. reflexivity. + intros. monadInv H. reflexivity. Qed. -Section TRANSF_PARTIAL_PROGRAM. +(** Additionally, we can also "augment" the program with new global definitions + and a different "main" function. *) -Variable A B V: Type. -Variable transf_partial: A -> res B. - -Definition prefix_name (id: ident) : errmsg := - MSG "In function " :: CTX id :: MSG ": " :: nil. +Section AUGMENT. -Definition transform_partial_program (p: program A V) : res (program B V) := - do fl <- map_partial prefix_name transf_partial p.(prog_funct); - OK (mkprogram fl p.(prog_main) p.(prog_vars)). +Variable new_globs: list(ident * globdef B W). +Variable new_main: ident. -Lemma transform_partial_program_function: - forall p tp i tf, - transform_partial_program p = OK tp -> - In (i, tf) tp.(prog_funct) -> - exists f, In (i, f) p.(prog_funct) /\ transf_partial f = OK tf. -Proof. - intros. monadInv H. simpl in H0. - eapply In_map_partial; eauto. -Qed. +Definition transform_partial_augment_program (p: program A V) : res (program B W) := + do gl' <- transf_globdefs p.(prog_defs); + OK(mkprogram (gl' ++ new_globs) new_main). -Lemma transform_partial_program_main: +Lemma transform_partial_augment_program_main: forall p tp, - transform_partial_program p = OK tp -> - tp.(prog_main) = p.(prog_main). + transform_partial_augment_program p = OK tp -> + tp.(prog_main) = new_main. Proof. intros. monadInv H. reflexivity. Qed. -Lemma transform_partial_program_vars: - forall p tp, - transform_partial_program p = OK tp -> - tp.(prog_vars) = p.(prog_vars). +End AUGMENT. + +Remark transform_partial_program2_augment: + forall p, + transform_partial_program2 p = + transform_partial_augment_program nil p.(prog_main) p. Proof. - intros. monadInv H. reflexivity. + unfold transform_partial_program2, transform_partial_augment_program; intros. + destruct (transf_globdefs (prog_defs p)); auto. + simpl. f_equal. f_equal. rewrite <- app_nil_end. auto. Qed. -End TRANSF_PARTIAL_PROGRAM. +End TRANSF_PROGRAM_GEN. -(** The following is a variant of [transform_program_partial] where - both the program functions and the additional variable information - are transformed by functions that can fail. *) +(** The following is a special case of [transform_partial_program2], + where only function definitions are transformed, but not variable definitions. *) -Section TRANSF_PARTIAL_PROGRAM2. - -Variable A B V W: Type. -Variable transf_partial_function: A -> res B. -Variable transf_partial_variable: V -> res W. - -Definition transf_globvar (g: globvar V) : res (globvar W) := - do info' <- transf_partial_variable g.(gvar_info); - OK (mkglobvar info' g.(gvar_init) g.(gvar_readonly) g.(gvar_volatile)). - -Definition transform_partial_program2 (p: program A V) : res (program B W) := - do fl <- map_partial prefix_name transf_partial_function p.(prog_funct); - do vl <- map_partial prefix_name transf_globvar p.(prog_vars); - OK (mkprogram fl p.(prog_main) vl). +Section TRANSF_PARTIAL_PROGRAM. -Lemma transform_partial_program2_function: - forall p tp i tf, - transform_partial_program2 p = OK tp -> - In (i, tf) tp.(prog_funct) -> - exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf. -Proof. - intros. monadInv H. - eapply In_map_partial; eauto. -Qed. +Variable A B V: Type. +Variable transf_partial: A -> res B. -Lemma transform_partial_program2_variable: - forall p tp i tg, - transform_partial_program2 p = OK tp -> - In (i, tg) tp.(prog_vars) -> - exists v, - In (i, mkglobvar v tg.(gvar_init) tg.(gvar_readonly) tg.(gvar_volatile)) p.(prog_vars) - /\ transf_partial_variable v = OK tg.(gvar_info). -Proof. - intros. monadInv H. exploit In_map_partial; eauto. intros [g [P Q]]. - monadInv Q. simpl in *. exists (gvar_info g); split. destruct g; auto. auto. - Qed. +Definition transform_partial_program (p: program A V) : res (program B V) := + transform_partial_program2 transf_partial (fun v => OK v) p. -Lemma transform_partial_program2_main: +Lemma transform_partial_program_main: forall p tp, - transform_partial_program2 p = OK tp -> + transform_partial_program p = OK tp -> tp.(prog_main) = p.(prog_main). Proof. - intros. monadInv H. reflexivity. + apply transform_partial_program2_main. Qed. -End TRANSF_PARTIAL_PROGRAM2. - -(** The following is a variant of [transform_partial_program2] where the - where the set of functions and global data is augmented, and - the main function is potentially changed. *) - -Section TRANSF_PARTIAL_AUGMENT_PROGRAM. - -Variable A B V W: Type. -Variable transf_partial_function: A -> res B. -Variable transf_partial_variable: V -> res W. - -Variable new_functs : list (ident * B). -Variable new_vars : list (ident * globvar W). -Variable new_main : ident. - -Definition transform_partial_augment_program (p: program A V) : res (program B W) := - do fl <- map_partial prefix_name transf_partial_function p.(prog_funct); - do vl <- map_partial prefix_name (transf_globvar transf_partial_variable) p.(prog_vars); - OK (mkprogram (fl ++ new_functs) new_main (vl ++ new_vars)). - -Lemma transform_partial_augment_program_function: +Lemma transform_partial_program_function: forall p tp i tf, - transform_partial_augment_program p = OK tp -> - In (i, tf) tp.(prog_funct) -> - (exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf) - \/ In (i,tf) new_functs. -Proof. - intros. monadInv H. simpl in H0. - rewrite in_app in H0. destruct H0. - left. eapply In_map_partial; eauto. - right. auto. -Qed. - -Lemma transform_partial_augment_program_main: - forall p tp, - transform_partial_augment_program p = OK tp -> - tp.(prog_main) = new_main. + transform_partial_program p = OK tp -> + In (i, Gfun tf) tp.(prog_defs) -> + exists f, In (i, Gfun f) p.(prog_defs) /\ transf_partial f = OK tf. Proof. - intros. monadInv H. reflexivity. + apply transform_partial_program2_function. Qed. +End TRANSF_PARTIAL_PROGRAM. -Lemma transform_partial_augment_program_variable: - forall p tp i tg, - transform_partial_augment_program p = OK tp -> - In (i, tg) tp.(prog_vars) -> - (exists v, In (i, mkglobvar v tg.(gvar_init) tg.(gvar_readonly) tg.(gvar_volatile)) p.(prog_vars) /\ transf_partial_variable v = OK tg.(gvar_info)) - \/ In (i,tg) new_vars. +Lemma transform_program_partial_program: + forall (A B V: Type) (transf: A -> B) (p: program A V), + transform_partial_program (fun f => OK(transf f)) p = OK(transform_program transf p). Proof. - intros. monadInv H. - simpl in H0. rewrite in_app in H0. inversion H0. - left. exploit In_map_partial; eauto. intros [g [P Q]]. - monadInv Q. simpl in *. exists (gvar_info g); split. destruct g; auto. auto. - right. auto. + intros. + unfold transform_partial_program, transform_partial_program2, transform_program; intros. + replace (transf_globdefs (fun f => OK (transf f)) (fun v => OK v) p.(prog_defs)) + with (OK (map (transform_program_globdef transf) p.(prog_defs))). + auto. + induction (prog_defs p); simpl. + auto. + destruct a as [id [f|v]]; rewrite <- IHl. + auto. + destruct v; auto. Qed. -End TRANSF_PARTIAL_AUGMENT_PROGRAM. - - (** The following is a relational presentation of [transform_partial_augment_preogram]. Given relations between function definitions and between variable information, it defines a relation @@ -429,61 +356,50 @@ Variable A B V W: Type. Variable match_fundef: A -> B -> Prop. Variable match_varinfo: V -> W -> Prop. -Inductive match_funct_entry: ident * A -> ident * B -> Prop := - | match_funct_entry_intro: forall id fn1 fn2, - match_fundef fn1 fn2 -> - match_funct_entry (id, fn1) (id, fn2). - -Inductive match_var_entry: ident * globvar V -> ident * globvar W -> Prop := - | match_var_entry_intro: forall id info1 info2 init ro vo, +Inductive match_globdef: ident * globdef A V -> ident * globdef B W -> Prop := + | match_glob_fun: forall id f1 f2, + match_fundef f1 f2 -> + match_globdef (id, Gfun f1) (id, Gfun f2) + | match_glob_var: forall id init ro vo info1 info2, match_varinfo info1 info2 -> - match_var_entry (id, mkglobvar info1 init ro vo) - (id, mkglobvar info2 init ro vo). + match_globdef (id, Gvar (mkglobvar info1 init ro vo)) (id, Gvar (mkglobvar info2 init ro vo)). -Definition match_program (new_functs : list (ident * B)) - (new_vars : list (ident * globvar W)) +Definition match_program (new_globs : list (ident * globdef B W)) (new_main : ident) (p1: program A V) (p2: program B W) : Prop := - (exists tfuncts, list_forall2 match_funct_entry p1.(prog_funct) tfuncts /\ - (p2.(prog_funct) = tfuncts ++ new_functs)) /\ - (exists tvars, list_forall2 match_var_entry p1.(prog_vars) tvars /\ - (p2.(prog_vars) = tvars ++ new_vars)) /\ + (exists tglob, list_forall2 match_globdef p1.(prog_defs) tglob /\ + p2.(prog_defs) = tglob ++ new_globs) /\ p2.(prog_main) = new_main. End MATCH_PROGRAM. -Remark transform_partial_augment_program_match: +Lemma transform_partial_augment_program_match: forall (A B V W: Type) - (transf_partial_function: A -> res B) - (transf_partial_variable : V -> res W) + (transf_fun: A -> res B) + (transf_var: V -> res W) (p: program A V) - (new_functs : list (ident * B)) - (new_vars : list (ident * globvar W)) + (new_globs : list (ident * globdef B W)) (new_main : ident) (tp: program B W), - transform_partial_augment_program transf_partial_function transf_partial_variable new_functs new_vars new_main p = OK tp -> + transform_partial_augment_program transf_fun transf_var new_globs new_main p = OK tp -> match_program - (fun fd tfd => transf_partial_function fd = OK tfd) - (fun info tinfo => transf_partial_variable info = OK tinfo) - new_functs new_vars new_main + (fun fd tfd => transf_fun fd = OK tfd) + (fun info tinfo => transf_var info = OK tinfo) + new_globs new_main p tp. Proof. - intros. unfold transform_partial_augment_program in H. monadInv H. split. - exists x. split. - apply list_forall2_imply with - (fun (ab: ident * A) (ac: ident * B) => - fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)). - eapply map_partial_forall2. eauto. - intros. destruct v1; destruct v2; simpl in *. - destruct H1; subst. constructor. auto. - auto. - split. exists x0. split. - apply list_forall2_imply with - (fun (ab: ident * globvar V) (ac: ident * globvar W) => - fst ab = fst ac /\ transf_globvar transf_partial_variable (snd ab) = OK (snd ac)). - eapply map_partial_forall2. eauto. - intros. destruct v1; destruct v2; simpl in *. destruct H1; subst. - monadInv H2. destruct g; simpl in *. constructor. auto. auto. auto. + unfold transform_partial_augment_program; intros. monadInv H. + red; simpl. split; auto. exists x; split; auto. + revert x EQ. generalize (prog_defs p). induction l; simpl; intros. + monadInv EQ. constructor. + destruct a as [id [f|v]]. + (* function *) + destruct (transf_fun f) as [tf|?]_eqn; monadInv EQ. + constructor; auto. constructor; auto. + (* variable *) + unfold transf_globvar in EQ. + destruct (transf_var (gvar_info v)) as [tinfo|?]_eqn; simpl in EQ; monadInv EQ. + constructor; auto. destruct v; simpl in *. constructor; auto. Qed. (** * External functions *) diff --git a/common/Globalenvs.v b/common/Globalenvs.v index ba038f8..8565ae6 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -69,13 +69,13 @@ Record t: Type := mkgenv { genv_symb: PTree.t block; (**r mapping symbol -> block *) genv_funs: ZMap.t (option F); (**r mapping function pointer -> definition *) genv_vars: ZMap.t (option (globvar V)); (**r mapping variable pointer -> info *) - genv_nextfun: block; (**r next function pointer *) - genv_nextvar: block; (**r next variable pointer *) - genv_nextfun_neg: genv_nextfun < 0; - genv_nextvar_pos: genv_nextvar > 0; - genv_symb_range: forall id b, PTree.get id genv_symb = Some b -> b <> 0 /\ genv_nextfun < b /\ b < genv_nextvar; - genv_funs_range: forall b f, ZMap.get b genv_funs = Some f -> genv_nextfun < b < 0; - genv_vars_range: forall b v, ZMap.get b genv_vars = Some v -> 0 < b < genv_nextvar; + genv_next: block; (**r next symbol pointer *) + genv_next_pos: genv_next > 0; + genv_symb_range: forall id b, PTree.get id genv_symb = Some b -> 0 < b < genv_next; + genv_funs_range: forall b f, ZMap.get b genv_funs = Some f -> 0 < b < genv_next; + genv_vars_range: forall b v, ZMap.get b genv_vars = Some v -> 0 < b < genv_next; + genv_funs_vars: forall b1 b2 f v, + ZMap.get b1 genv_funs = Some f -> ZMap.get b2 genv_vars = Some v -> b1 <> b2; genv_vars_inj: forall id1 id2 b, PTree.get id1 genv_symb = Some b -> PTree.get id2 genv_symb = Some b -> id1 = id2 }. @@ -117,69 +117,53 @@ Definition find_var_info (ge: t) (b: block) : option (globvar V) := (** ** Constructing the global environment *) -Program Definition add_function (ge: t) (idf: ident * F) : t := +Program Definition add_global (ge: t) (idg: ident * globdef F V) : t := @mkgenv - (PTree.set idf#1 ge.(genv_nextfun) ge.(genv_symb)) - (ZMap.set ge.(genv_nextfun) (Some idf#2) ge.(genv_funs)) - ge.(genv_vars) - (ge.(genv_nextfun) - 1) - ge.(genv_nextvar) + (PTree.set idg#1 ge.(genv_next) ge.(genv_symb)) + (match idg#2 with + | Gfun f => ZMap.set ge.(genv_next) (Some f) ge.(genv_funs) + | Gvar v => ge.(genv_funs) + end) + (match idg#2 with + | Gfun f => ge.(genv_vars) + | Gvar v => ZMap.set ge.(genv_next) (Some v) ge.(genv_vars) + end) + (ge.(genv_next) + 1) _ _ _ _ _ _. Next Obligation. destruct ge; simpl; omega. Qed. Next Obligation. - destruct ge; auto. -Qed. -Next Obligation. destruct ge; simpl in *. rewrite PTree.gsspec in H. destruct (peq id i). inv H. unfold block; omega. exploit genv_symb_range0; eauto. unfold block; omega. Qed. Next Obligation. - destruct ge; simpl in *. rewrite ZMap.gsspec in H. - destruct (ZIndexed.eq b genv_nextfun0). subst; omega. + destruct ge; simpl in *. + destruct g. + rewrite ZMap.gsspec in H. + destruct (ZIndexed.eq b genv_next0). subst; omega. + exploit genv_funs_range0; eauto. omega. exploit genv_funs_range0; eauto. omega. -Qed. -Next Obligation. - destruct ge; eauto. Qed. Next Obligation. destruct ge; simpl in *. - rewrite PTree.gsspec in H. rewrite PTree.gsspec in H0. - destruct (peq id1 i); destruct (peq id2 i). - congruence. - exploit genv_symb_range0; eauto. intros [A B]. inv H. omegaContradiction. - exploit genv_symb_range0; eauto. intros [A B]. inv H0. omegaContradiction. - eauto. -Qed. - -Program Definition add_variable (ge: t) (idv: ident * globvar V) : t := - @mkgenv - (PTree.set idv#1 ge.(genv_nextvar) ge.(genv_symb)) - ge.(genv_funs) - (ZMap.set ge.(genv_nextvar) (Some idv#2) ge.(genv_vars)) - ge.(genv_nextfun) - (ge.(genv_nextvar) + 1) - _ _ _ _ _ _. -Next Obligation. - destruct ge; auto. -Qed. -Next Obligation. - destruct ge; simpl; omega. -Qed. -Next Obligation. - destruct ge; simpl in *. - rewrite PTree.gsspec in H. destruct (peq id i). inv H. unfold block; omega. - exploit genv_symb_range0; eauto. unfold block; omega. -Qed. -Next Obligation. - destruct ge; eauto. + destruct g. + exploit genv_vars_range0; eauto. omega. + rewrite ZMap.gsspec in H. + destruct (ZIndexed.eq b genv_next0). subst; omega. + exploit genv_vars_range0; eauto. omega. Qed. Next Obligation. - destruct ge; simpl in *. rewrite ZMap.gsspec in H. - destruct (ZIndexed.eq b genv_nextvar0). subst; omega. - exploit genv_vars_range0; eauto. omega. + destruct ge; simpl in *. destruct g. + rewrite ZMap.gsspec in H. + destruct (ZIndexed.eq b1 genv_next0). inv H. + exploit genv_vars_range0; eauto. unfold ZIndexed.t; omega. + eauto. + rewrite ZMap.gsspec in H0. + destruct (ZIndexed.eq b2 genv_next0). inv H. + exploit genv_funs_range0; eauto. unfold ZIndexed.t; omega. + eauto. Qed. Next Obligation. destruct ge; simpl in *. @@ -191,16 +175,26 @@ Next Obligation. eauto. Qed. +Definition add_globals (ge: t) (gl: list (ident * globdef F V)) : t := + List.fold_left add_global gl ge. + +Lemma add_globals_app: + forall gl2 gl1 ge, + add_globals ge (gl1 ++ gl2) = add_globals (add_globals ge gl1) gl2. +Proof. + induction gl1; simpl; intros. auto. rewrite IHgl1; auto. +Qed. + Program Definition empty_genv : t := - @mkgenv (PTree.empty block) (ZMap.init None) (ZMap.init None) (-1) 1 _ _ _ _ _ _. + @mkgenv (PTree.empty block) (ZMap.init None) (ZMap.init None) 1 _ _ _ _ _ _. Next Obligation. omega. Qed. Next Obligation. - omega. + rewrite PTree.gempty in H. discriminate. Qed. Next Obligation. - rewrite PTree.gempty in H. discriminate. + rewrite ZMap.gi in H. discriminate. Qed. Next Obligation. rewrite ZMap.gi in H. discriminate. @@ -212,27 +206,54 @@ Next Obligation. rewrite PTree.gempty in H. discriminate. Qed. -Definition add_functions (ge: t) (fl: list (ident * F)) : t := - List.fold_left add_function fl ge. +Definition globalenv (p: program F V) := + add_globals empty_genv p.(prog_defs). -Lemma add_functions_app : forall ge fl1 fl2, - add_functions ge (fl1 ++ fl2) = add_functions (add_functions ge fl1) fl2. -Proof. - intros. unfold add_functions. rewrite fold_left_app. auto. -Qed. +(** Proof principles *) +Section GLOBALENV_PRINCIPLES. -Definition add_variables (ge: t) (vl: list (ident * globvar V)) : t := - List.fold_left add_variable vl ge. +Variable P: t -> Prop. -Lemma add_variables_app : forall ge vl1 vl2 , - add_variables ge (vl1 ++ vl2) = add_variables (add_variables ge vl1) vl2. -Proof. - intros. unfold add_variables. rewrite fold_left_app. auto. +Lemma add_globals_preserves: + forall gl ge, + (forall ge id g, P ge -> In (id, g) gl -> P (add_global ge (id, g))) -> + P ge -> P (add_globals ge gl). +Proof. + induction gl; simpl; intros. + auto. + destruct a. apply IHgl; auto. Qed. -Definition globalenv (p: program F V) := - add_variables (add_functions empty_genv p.(prog_funct)) p.(prog_vars). +Lemma add_globals_ensures: + forall id g gl ge, + (forall ge id g, P ge -> In (id, g) gl -> P (add_global ge (id, g))) -> + (forall ge, P (add_global ge (id, g))) -> + In (id, g) gl -> P (add_globals ge gl). +Proof. + induction gl; simpl; intros. + contradiction. + destruct H1. subst a. apply add_globals_preserves; auto. + apply IHgl; auto. +Qed. + +Lemma add_globals_norepet_ensures: + forall id g gl ge, + (forall ge id1 g1, P ge -> In (id1, g1) gl -> id1 <> id -> P (add_global ge (id1, g1))) -> + (forall ge, P (add_global ge (id, g))) -> + In (id, g) gl -> list_norepet (map fst gl) -> P (add_globals ge gl). +Proof. + induction gl; simpl; intros. + contradiction. + inv H2. + destruct H1. subst a. simpl in H5. + apply add_globals_preserves; auto. + intros. apply H. auto. auto. red; intros; subst id0. elim H5. + change id with (fst (id, g0)). apply List.in_map; auto. + apply IHgl; auto. +Qed. + +End GLOBALENV_PRINCIPLES. (** ** Properties of the operations over global environments *) @@ -254,298 +275,132 @@ Proof. Qed. Theorem find_symbol_exists: - forall p id gv, - In (id, gv) (prog_vars p) -> + forall p id g, + In (id, g) (prog_defs p) -> exists b, find_symbol (globalenv p) id = Some b. Proof. - intros until gv. - assert (forall vl ge, - (exists b, find_symbol ge id = Some b) -> - exists b, find_symbol (add_variables ge vl) id = Some b). - unfold find_symbol; induction vl; simpl; intros. auto. apply IHvl. - simpl. rewrite PTree.gsspec. fold ident. destruct (peq id a#1). - exists (genv_nextvar ge); auto. auto. - - assert (forall vl ge, In (id, gv) vl -> - exists b, find_symbol (add_variables ge vl) id = Some b). - unfold find_symbol; induction vl; simpl; intros. contradiction. - destruct H0. apply H. subst; unfold find_symbol; simpl. - rewrite PTree.gss. exists (genv_nextvar ge); auto. - eauto. + intros. unfold globalenv. eapply add_globals_ensures; eauto. +(* preserves *) + intros. unfold find_symbol; simpl. rewrite PTree.gsspec. destruct (peq id id0). + econstructor; eauto. + auto. +(* ensures *) + intros. unfold find_symbol; simpl. rewrite PTree.gss. econstructor; eauto. +Qed. - intros. unfold globalenv; eauto. +Theorem find_funct_ptr_exists: + forall p id f, + list_norepet (prog_defs_names p) -> + In (id, Gfun f) (prog_defs p) -> + exists b, + find_symbol (globalenv p) id = Some b + /\ find_funct_ptr (globalenv p) b = Some f. +Proof. + intros; unfold globalenv. eapply add_globals_norepet_ensures; eauto. +(* preserves *) + intros. unfold find_symbol, find_funct_ptr in *; simpl. + destruct H1 as [b [A B]]. exists b; split. + rewrite PTree.gso; auto. + destruct g1 as [f1 | v1]. rewrite ZMap.gso. auto. + exploit genv_funs_range; eauto. unfold ZIndexed.t; omega. + auto. +(* ensures *) + intros. unfold find_symbol, find_funct_ptr in *; simpl. + exists (genv_next ge); split. apply PTree.gss. apply ZMap.gss. Qed. Theorem find_var_exists: - forall p id gv, - list_norepet (prog_var_names p) -> - In (id, gv) (prog_vars p) -> + forall p id v, + list_norepet (prog_defs_names p) -> + In (id, Gvar v) (prog_defs p) -> exists b, find_symbol (globalenv p) id = Some b - /\ find_var_info (globalenv p) b = Some gv. -Proof. - intros until gv. - assert (forall vl ge, - ~In id (var_names vl) -> - (exists b, find_symbol ge id = Some b /\ find_var_info ge b = Some gv) -> - (exists b, find_symbol (add_variables ge vl) id = Some b - /\ find_var_info (add_variables ge vl) b = Some gv)). - induction vl; simpl; intros. - auto. - apply IHvl. tauto. destruct a as [id1 gv1]. destruct H0 as [b [P Q]]. - unfold add_variable, find_symbol, find_var_info; simpl. - exists b; split. rewrite PTree.gso. auto. intuition. - rewrite ZMap.gso. auto. exploit genv_vars_range; eauto. - unfold ZIndexed.t; omega. - - unfold globalenv, prog_var_names. - generalize (prog_vars p) (add_functions empty_genv (prog_funct p)). - induction l; simpl; intros. - contradiction. - destruct a as [id1 gv1]; simpl in *. inv H0. - destruct H1. inv H0. - apply H; auto. - exists (genv_nextvar t0); split. - unfold find_symbol, add_variable; simpl. apply PTree.gss. - unfold find_var_info, add_variable; simpl. apply ZMap.gss. - apply IHl; auto. -Qed. - -Remark add_variables_inversion : forall vs e x b, - find_symbol (add_variables e vs) x = Some b -> - In x (var_names vs) \/ find_symbol e x = Some b. -Proof. - induction vs; intros. - simpl in H. intuition. - simpl in H. destruct (IHvs _ _ _ H). - left. simpl. intuition. - destruct a as [y ?]. - unfold add_variable, find_symbol in H0. simpl in H0. - rewrite PTree.gsspec in H0. destruct (peq x y); subst; simpl; intuition. -Qed. - -Remark add_functions_inversion : forall fs e x b, - find_symbol (add_functions e fs) x = Some b -> - In x (funct_names fs) \/ find_symbol e x = Some b. -Proof. - induction fs; intros. - simpl in H. intuition. - simpl in H. destruct (IHfs _ _ _ H). - left. simpl. intuition. - destruct a as [y ?]. - unfold add_variable, find_symbol in H0. simpl in H0. - rewrite PTree.gsspec in H0. destruct (peq x y); subst; simpl; intuition. + /\ find_var_info (globalenv p) b = Some v. +Proof. + intros; unfold globalenv. eapply add_globals_norepet_ensures; eauto. +(* preserves *) + intros. unfold find_symbol, find_var_info in *; simpl. + destruct H1 as [b [A B]]. exists b; split. + rewrite PTree.gso; auto. + destruct g1 as [f1 | v1]. auto. rewrite ZMap.gso. auto. + exploit genv_vars_range; eauto. unfold ZIndexed.t; omega. +(* ensures *) + intros. unfold find_symbol, find_var_info in *; simpl. + exists (genv_next ge); split. apply PTree.gss. apply ZMap.gss. Qed. Lemma find_symbol_inversion : forall p x b, find_symbol (globalenv p) x = Some b -> - In x (prog_var_names p ++ prog_funct_names p). -Proof. - unfold prog_var_names, prog_funct_names, globalenv. - intros. - apply in_app. - apply add_variables_inversion in H. intuition. - apply add_functions_inversion in H0. inversion H0. intuition. - unfold find_symbol in H. - rewrite PTree.gempty in H. inversion H. -Qed. - - -Remark add_functions_same_symb: - forall id fl ge, - ~In id (funct_names fl) -> - find_symbol (add_functions ge fl) id = find_symbol ge id. -Proof. - induction fl; simpl; intros. auto. - rewrite IHfl. unfold find_symbol; simpl. apply PTree.gso. intuition. intuition. -Qed. - -Remark add_functions_same_address: - forall b fl ge, - b > ge.(genv_nextfun) -> - find_funct_ptr (add_functions ge fl) b = find_funct_ptr ge b. -Proof. - induction fl; simpl; intros. auto. - rewrite IHfl. unfold find_funct_ptr; simpl. apply ZMap.gso. - red; intros; subst b; omegaContradiction. - simpl. omega. -Qed. - -Remark add_variables_same_symb: - forall id vl ge, - ~In id (var_names vl) -> - find_symbol (add_variables ge vl) id = find_symbol ge id. + In x (prog_defs_names p). Proof. - induction vl; simpl; intros. auto. - rewrite IHvl. unfold find_symbol; simpl. apply PTree.gso. intuition. intuition. -Qed. - -Remark add_variables_same_address: - forall b vl ge, - b < ge.(genv_nextvar) -> - find_var_info (add_variables ge vl) b = find_var_info ge b. -Proof. - induction vl; simpl; intros. auto. - rewrite IHvl. unfold find_var_info; simpl. apply ZMap.gso. - red; intros; subst b; omegaContradiction. - simpl. omega. -Qed. - -Remark add_variables_same_funs: - forall b vl ge, find_funct_ptr (add_variables ge vl) b = find_funct_ptr ge b. -Proof. - induction vl; simpl; intros. auto. rewrite IHvl. auto. + intros until b; unfold globalenv. eapply add_globals_preserves. +(* preserves *) + unfold find_symbol; simpl; intros. rewrite PTree.gsspec in H1. + destruct (peq x id). subst x. change id with (fst (id, g)). apply List.in_map; auto. + auto. +(* base *) + unfold find_symbol; simpl; intros. rewrite PTree.gempty in H. discriminate. Qed. -Remark add_functions_nextvar: - forall fl ge, genv_nextvar (add_functions ge fl) = genv_nextvar ge. +Theorem find_funct_ptr_inversion: + forall p b f, + find_funct_ptr (globalenv p) b = Some f -> + exists id, In (id, Gfun f) (prog_defs p). Proof. - induction fl; simpl; intros. auto. rewrite IHfl. auto. + intros until f. unfold globalenv. apply add_globals_preserves. +(* preserves *) + unfold find_funct_ptr; simpl; intros. destruct g; auto. + rewrite ZMap.gsspec in H1. destruct (ZIndexed.eq b (genv_next ge)). + inv H1. exists id; auto. + auto. +(* base *) + unfold find_funct_ptr; simpl; intros. rewrite ZMap.gi in H. discriminate. Qed. -Remark add_variables_nextvar: - forall vl ge, genv_nextvar (add_variables ge vl) = genv_nextvar ge + Z_of_nat(List.length vl). +Theorem find_funct_inversion: + forall p v f, + find_funct (globalenv p) v = Some f -> + exists id, In (id, Gfun f) (prog_defs p). Proof. - induction vl; intros. - simpl. unfold block; omega. - simpl length; rewrite inj_S; simpl. rewrite IHvl. simpl. unfold block; omega. -Qed. - -Theorem find_funct_ptr_exists: - forall p id 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. -Proof. - intros until f. - - assert (forall fl ge, In (id, f) fl -> list_norepet (funct_names fl) -> - exists b, find_symbol (add_functions ge fl) id = Some b - /\ find_funct_ptr (add_functions ge fl) b = Some f). - induction fl; simpl; intros. contradiction. inv H0. - destruct H. subst a. exists (genv_nextfun ge); split. - rewrite add_functions_same_symb; auto. unfold find_symbol; simpl. apply PTree.gss. - rewrite add_functions_same_address. unfold find_funct_ptr; simpl. apply ZMap.gss. - simpl; omega. - apply IHfl; auto. - - intros. exploit (H p.(prog_funct) empty_genv); eauto. intros [b [A B]]. - unfold globalenv; exists b; split. - rewrite add_variables_same_symb. auto. eapply list_disjoint_notin; eauto. - unfold prog_funct_names. change id with (fst (id, f)). apply in_map; auto. - rewrite add_variables_same_funs. auto. + intros. exploit find_funct_inv; eauto. intros [b EQ]. subst v. + rewrite find_funct_find_funct_ptr in H. + eapply find_funct_ptr_inversion; eauto. Qed. Theorem find_funct_ptr_prop: forall (P: F -> Prop) p b f, - (forall id f, In (id, f) (prog_funct p) -> P f) -> + (forall id f, In (id, Gfun f) (prog_defs p) -> P f) -> find_funct_ptr (globalenv p) b = Some f -> P f. Proof. - intros until f. intros PROP. - assert (forall fl ge, - List.incl fl (prog_funct p) -> - match find_funct_ptr ge b with None => True | Some f => P f end -> - match find_funct_ptr (add_functions ge fl) b with None => True | Some f => P f end). - induction fl; simpl; intros. auto. - apply IHfl. eauto with coqlib. unfold find_funct_ptr; simpl. - destruct a as [id' f']; simpl. - rewrite ZMap.gsspec. destruct (ZIndexed.eq b (genv_nextfun ge)). - apply PROP with id'. apply H. auto with coqlib. - assumption. - - unfold globalenv. rewrite add_variables_same_funs. intro. - exploit (H p.(prog_funct) empty_genv). auto with coqlib. - unfold find_funct_ptr; simpl. rewrite ZMap.gi. auto. - rewrite H0. auto. + intros. exploit find_funct_ptr_inversion; eauto. intros [id IN]. eauto. Qed. Theorem find_funct_prop: forall (P: F -> Prop) p v f, - (forall id f, In (id, f) (prog_funct p) -> P f) -> + (forall id f, In (id, Gfun f) (prog_defs p) -> P f) -> find_funct (globalenv p) v = Some f -> P f. Proof. - intros. exploit find_funct_inv; eauto. intros [b EQ]. subst v. - rewrite find_funct_find_funct_ptr in H0. - eapply find_funct_ptr_prop; eauto. -Qed. - -Theorem find_funct_ptr_inversion: - forall p b f, - find_funct_ptr (globalenv p) b = Some f -> - exists id, In (id, f) (prog_funct p). -Proof. - intros. pattern f. apply find_funct_ptr_prop with p b; auto. - intros. exists id; auto. -Qed. - -Theorem find_funct_inversion: - forall p v f, - find_funct (globalenv p) v = Some f -> - exists id, In (id, f) (prog_funct p). -Proof. - intros. pattern f. apply find_funct_prop with p v; auto. - intros. exists id; auto. -Qed. - -Theorem find_funct_ptr_negative: - forall p b f, - find_funct_ptr (globalenv p) b = Some f -> b < 0. -Proof. - unfold find_funct_ptr. intros. destruct (globalenv p). simpl in H. - exploit genv_funs_range0; eauto. omega. -Qed. - -Theorem find_var_info_positive: - forall p b v, - find_var_info (globalenv p) b = Some v -> b > 0. -Proof. - unfold find_var_info. intros. destruct (globalenv p). simpl in H. - exploit genv_vars_range0; eauto. omega. -Qed. - -Remark add_variables_symb_neg: - forall id b vl ge, - find_symbol (add_variables ge vl) id = Some b -> b < 0 -> - find_symbol ge id = Some b. -Proof. - induction vl; simpl; intros. auto. - exploit IHvl; eauto. unfold find_symbol; simpl. rewrite PTree.gsspec. - fold ident. destruct (peq id (a#1)); auto. intros. inv H1. - generalize (genv_nextvar_pos ge). intros. omegaContradiction. + intros. exploit find_funct_inversion; eauto. intros [id IN]. eauto. Qed. Theorem find_funct_ptr_symbol_inversion: forall p id b f, find_symbol (globalenv p) id = Some b -> find_funct_ptr (globalenv p) b = Some f -> - In (id, f) p.(prog_funct). -Proof. - intros until f. - - assert (forall fl ge, - find_symbol (add_functions ge fl) id = Some b -> - find_funct_ptr (add_functions ge fl) b = Some f -> - In (id, f) fl \/ (find_symbol ge id = Some b /\ find_funct_ptr ge b = Some f)). - induction fl; simpl; intros. + In (id, Gfun f) p.(prog_defs). +Proof. + intros until f. unfold globalenv, find_symbol, find_funct_ptr. apply add_globals_preserves. +(* preserves *) + intros. simpl in *. rewrite PTree.gsspec in H1. destruct (peq id id0). + inv H1. destruct g as [f1|v1]. rewrite ZMap.gss in H2. inv H2. auto. + exploit genv_funs_range; eauto. intros. omegaContradiction. + destruct g as [f1|v1]. rewrite ZMap.gso in H2. auto. + exploit genv_symb_range; eauto. unfold ZIndexed.t; omega. auto. - exploit IHfl; eauto. intros [A | [A B]]. auto. - destruct a as [id' f']. - unfold find_symbol in A; simpl in A. - unfold find_funct_ptr in B; simpl in B. - rewrite PTree.gsspec in A. destruct (peq id id'). inv A. - rewrite ZMap.gss in B. inv B. auto. - rewrite ZMap.gso in B. right; auto. - exploit genv_symb_range; eauto. unfold block, ZIndexed.t; omega. - - intros. assert (b < 0) by (eapply find_funct_ptr_negative; eauto). - unfold globalenv in *. rewrite add_variables_same_funs in H1. - exploit (H (prog_funct p) empty_genv). - eapply add_variables_symb_neg; eauto. auto. - intuition. unfold find_symbol in H3; simpl in H3. rewrite PTree.gempty in H3. discriminate. +(* initial *) + intros. simpl in *. rewrite PTree.gempty in H. discriminate. Qed. Theorem find_symbol_not_nullptr: @@ -553,7 +408,7 @@ Theorem find_symbol_not_nullptr: find_symbol (globalenv p) id = Some b -> b <> Mem.nullptr. Proof. intros until b. unfold find_symbol. destruct (globalenv p); simpl. - intros. exploit genv_symb_range0; eauto. intuition. + intros. exploit genv_symb_range0; eauto. unfold Mem.nullptr, block. omega. Qed. Theorem global_addresses_distinct: @@ -599,6 +454,16 @@ Proof. congruence. Qed. +Remark genv_next_add_globals: + forall gl ge, + genv_next (add_globals ge gl) = genv_next ge + Z_of_nat (length gl). +Proof. + induction gl; intros. + simpl. unfold block; omega. + simpl add_globals; simpl length; rewrite inj_S. + rewrite IHgl. simpl. unfold block; omega. +Qed. + (** * Construction of the initial memory state *) Section INITMEM. @@ -622,6 +487,18 @@ Proof. destruct i; simpl; try omega. generalize (Zle_max_r z 0). omega. Qed. +Function store_zeros (m: mem) (b: block) (p: Z) (n: Z) {wf (Zwf 0) n}: option mem := + if zle n 0 then Some m else + let n' := n - 1 in + match Mem.store Mint8unsigned m b p Vzero with + | Some m' => store_zeros m' b (p + 1) n' + | None => None + end. +Proof. + intros. red. omega. + apply Zwf_well_founded. +Qed. + Definition store_init_data (m: mem) (b: block) (p: Z) (id: init_data) : option mem := match id with | Init_int8 n => Mem.store Mint8unsigned m b p (Vint n) @@ -648,18 +525,6 @@ Fixpoint store_init_data_list (m: mem) (b: block) (p: Z) (idl: list init_data) end end. -Function store_zeros (m: mem) (b: block) (n: Z) {wf (Zwf 0) n}: option mem := - if zle n 0 then Some m else - let n' := n - 1 in - match Mem.store Mint8unsigned m b n' Vzero with - | Some m' => store_zeros m' b n' - | None => None - end. -Proof. - intros. red. omega. - apply Zwf_well_founded. -Qed. - Fixpoint init_data_list_size (il: list init_data) {struct il} : Z := match il with | nil => 0 @@ -671,37 +536,54 @@ Definition perm_globvar (gv: globvar V) : permission := else if gv.(gvar_readonly) then Readable else Writable. -Definition alloc_variable (m: mem) (idv: ident * globvar V) : option mem := - let init := idv#2.(gvar_init) in - let sz := init_data_list_size init in - let (m1, b) := Mem.alloc m 0 sz in - match store_zeros m1 b sz with - | None => None - | Some m2 => - match store_init_data_list m2 b 0 init with +Definition alloc_global (m: mem) (idg: ident * globdef F V): option mem := + match idg with + | (id, Gfun f) => + let (m1, b) := Mem.alloc m 0 1 in + Mem.drop_perm m1 b 0 1 Nonempty + | (id, Gvar v) => + let init := v.(gvar_init) in + let sz := init_data_list_size init in + let (m1, b) := Mem.alloc m 0 sz in + match store_zeros m1 b 0 sz with | None => None - | Some m3 => Mem.drop_perm m3 b 0 sz (perm_globvar idv#2) + | Some m2 => + match store_init_data_list m2 b 0 init with + | None => None + | Some m3 => Mem.drop_perm m3 b 0 sz (perm_globvar v) + end end end. -Fixpoint alloc_variables (m: mem) (vl: list (ident * globvar V)) - {struct vl} : option mem := - match vl with +Fixpoint alloc_globals (m: mem) (gl: list (ident * globdef F V)) + {struct gl} : option mem := + match gl with | nil => Some m - | v :: vl' => - match alloc_variable m v with + | g :: gl' => + match alloc_global m g with | None => None - | Some m' => alloc_variables m' vl' + | Some m' => alloc_globals m' gl' end end. -Lemma alloc_variables_app : forall vl1 vl2 m m1, - alloc_variables m vl1 = Some m1 -> - alloc_variables m1 vl2 = alloc_variables m (vl1 ++ vl2). +Lemma alloc_globals_app : forall gl1 gl2 m m1, + alloc_globals m gl1 = Some m1 -> + alloc_globals m1 gl2 = alloc_globals m (gl1 ++ gl2). +Proof. + induction gl1. + simpl. intros. inversion H; subst. auto. + simpl. intros. destruct (alloc_global m a); eauto. inversion H. +Qed. + +(** Next-block properties *) + +Remark store_zeros_nextblock: + forall m b p n m', store_zeros m b p n = Some m' -> Mem.nextblock m' = Mem.nextblock m. Proof. - induction vl1. - simpl. intros. inversion H; subst. auto. - simpl. intros. destruct (alloc_variable m a); eauto. inversion H. + intros until n. functional induction (store_zeros m b p n); intros. + inv H; auto. + rewrite IHo; eauto with mem. + congruence. Qed. Remark store_init_data_list_nextblock: @@ -714,71 +596,52 @@ Proof. caseEq (store_init_data m b p a); try congruence. intros. transitivity (Mem.nextblock m0). eauto. destruct a; simpl in H; try (eapply Mem.nextblock_store; eauto; fail). - congruence. - destruct (find_symbol ge i); try congruence. eapply Mem.nextblock_store; eauto. -Qed. - -Remark store_zeros_nextblock: - forall m b n m', store_zeros m b n = Some m' -> Mem.nextblock m' = Mem.nextblock m. -Proof. - intros until n. functional induction (store_zeros m b n); intros. - inv H; auto. - rewrite IHo; eauto with mem. congruence. + destruct (find_symbol ge i); try congruence. eapply Mem.nextblock_store; eauto. Qed. -Remark alloc_variable_nextblock: - forall v m m', - alloc_variable m v = Some m' -> +Remark alloc_global_nextblock: + forall g m m', + alloc_global m g = Some m' -> Mem.nextblock m' = Zsucc(Mem.nextblock m). Proof. - unfold alloc_variable. - intros until m'. - set (init := gvar_init v#2). - set (sz := init_data_list_size init). - caseEq (Mem.alloc m 0 sz). intros m1 b ALLOC. - caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ. - caseEq (store_init_data_list m2 b 0 init); try congruence. intros m3 STORE. - caseEq (Mem.drop_perm m3 b 0 sz (perm_globvar v#2)); try congruence. intros m4 DROP REC. - inv REC; subst. - rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). - rewrite (store_init_data_list_nextblock _ _ _ _ STORE). - rewrite (store_zeros_nextblock _ _ _ STZ). - rewrite (Mem.nextblock_alloc _ _ _ _ _ ALLOC). - auto. -Qed. - - -Remark alloc_variables_nextblock: - forall vl m m', - alloc_variables m vl = Some m' -> - Mem.nextblock m' = Mem.nextblock m + Z_of_nat(List.length vl). -Proof. - induction vl. + unfold alloc_global. intros. + destruct g as [id [f|v]]. + (* function *) + destruct (Mem.alloc m 0 1) as [m1 b]_eqn. + erewrite Mem.nextblock_drop; eauto. erewrite Mem.nextblock_alloc; eauto. + (* variable *) + set (init := gvar_init v) in *. + set (sz := init_data_list_size init) in *. + destruct (Mem.alloc m 0 sz) as [m1 b]_eqn. + destruct (store_zeros m1 b 0 sz) as [m2|]_eqn; try discriminate. + destruct (store_init_data_list m2 b 0 init) as [m3|]_eqn; try discriminate. + erewrite Mem.nextblock_drop; eauto. + erewrite store_init_data_list_nextblock; eauto. + erewrite store_zeros_nextblock; eauto. + erewrite Mem.nextblock_alloc; eauto. +Qed. + +Remark alloc_globals_nextblock: + forall gl m m', + alloc_globals m gl = Some m' -> + Mem.nextblock m' = Mem.nextblock m + Z_of_nat(List.length gl). +Proof. + induction gl. simpl; intros. inv H; unfold block; omega. - simpl length; rewrite inj_S; simpl. intros m m'. - unfold alloc_variable. - set (init := gvar_init a#2). - set (sz := init_data_list_size init). - caseEq (Mem.alloc m 0 sz). intros m1 b ALLOC. - caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ. - caseEq (store_init_data_list m2 b 0 init); try congruence. intros m3 STORE. - caseEq (Mem.drop_perm m3 b 0 sz (perm_globvar a#2)); try congruence. intros m4 DROP REC. - rewrite (IHvl _ _ REC). - rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). - rewrite (store_init_data_list_nextblock _ _ _ _ STORE). - rewrite (store_zeros_nextblock _ _ _ STZ). - rewrite (Mem.nextblock_alloc _ _ _ _ _ ALLOC). - unfold block in *; omega. + simpl length; rewrite inj_S; simpl; intros. + destruct (alloc_global m a) as [m1|]_eqn; try discriminate. + erewrite IHgl; eauto. erewrite alloc_global_nextblock; eauto. unfold block; omega. Qed. +(** Permissions *) Remark store_zeros_perm: - forall k prm b' q m b n m', - store_zeros m b n = Some m' -> + forall k prm b' q m b p n m', + store_zeros m b p n = Some m' -> (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm). Proof. - intros until n. functional induction (store_zeros m b n); intros. + intros until n. functional induction (store_zeros m b p n); intros. inv H; tauto. destruct (IHo _ H); intros. split; eauto with mem. congruence. @@ -793,56 +656,74 @@ Proof. intros. inv H. tauto. caseEq (store_init_data m b p a); try congruence. intros. rewrite <- (IHidl _ _ _ _ H0). - destruct a; simpl in H; split; eauto with mem. - inv H; auto. inv H; auto. - destruct (find_symbol ge i); try congruence. eauto with mem. - destruct (find_symbol ge i); try congruence. eauto with mem. + assert (forall chunk v, + Mem.store chunk m b p v = Some m0 -> + (Mem.perm m b' q k prm <-> Mem.perm m0 b' q k prm)). + intros; split; eauto with mem. + destruct a; simpl in H; eauto. + inv H; tauto. + destruct (find_symbol ge i). eauto. discriminate. Qed. -Remark alloc_variables_perm: - forall k prm b' q vl m m', - alloc_variables m vl = Some m' -> +Remark alloc_global_perm: + forall k prm b' q idg m m', + alloc_global m idg = Some m' -> Mem.valid_block m b' -> (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm). Proof. - induction vl. - simpl; intros. inv H. tauto. - intros until m'. simpl. unfold alloc_variable. - set (init := gvar_init a#2). - set (sz := init_data_list_size init). - caseEq (Mem.alloc m 0 sz). intros m1 b ALLOC. - caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ. - caseEq (store_init_data_list m2 b 0 init); try congruence. intros m3 STORE. - caseEq (Mem.drop_perm m3 b 0 sz (perm_globvar a#2)); try congruence. intros m4 DROP REC VALID. + intros. destruct idg as [id [f|v]]; simpl in H. + (* function *) + destruct (Mem.alloc m 0 1) as [m1 b]_eqn. + assert (b' <> b). apply Mem.valid_not_valid_diff with m; eauto with mem. + split; intros. + eapply Mem.perm_drop_3; eauto. eapply Mem.perm_alloc_1; eauto. + eapply Mem.perm_alloc_4; eauto. eapply Mem.perm_drop_4; eauto. + (* variable *) + set (init := gvar_init v) in *. + set (sz := init_data_list_size init) in *. + destruct (Mem.alloc m 0 sz) as [m1 b]_eqn. + destruct (store_zeros m1 b 0 sz) as [m2|]_eqn; try discriminate. + destruct (store_init_data_list m2 b 0 init) as [m3|]_eqn; try discriminate. assert (b' <> b). apply Mem.valid_not_valid_diff with m; eauto with mem. - assert (VALID': Mem.valid_block m4 b'). - unfold Mem.valid_block. rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). - rewrite (store_init_data_list_nextblock _ _ _ _ STORE). - rewrite (store_zeros_nextblock _ _ _ STZ). - change (Mem.valid_block m1 b'). eauto with mem. - rewrite <- (IHvl _ _ REC VALID'). split; intros. eapply Mem.perm_drop_3; eauto. - rewrite <- store_init_data_list_perm; [idtac|eauto]. - rewrite <- store_zeros_perm; [idtac|eauto]. - eauto with mem. - assert (Mem.perm m1 b' q k prm). - rewrite store_zeros_perm; [idtac|eauto]. - rewrite store_init_data_list_perm; [idtac|eauto]. - eapply Mem.perm_drop_4; eauto. - exploit Mem.perm_alloc_inv; eauto. rewrite zeq_false; auto. + erewrite <- store_init_data_list_perm; [idtac|eauto]. + erewrite <- store_zeros_perm; [idtac|eauto]. + eapply Mem.perm_alloc_1; eauto. + eapply Mem.perm_alloc_4; eauto. + erewrite store_zeros_perm; [idtac|eauto]. + erewrite store_init_data_list_perm; [idtac|eauto]. + eapply Mem.perm_drop_4; eauto. +Qed. + +Remark alloc_globals_perm: + forall k prm b' q gl m m', + alloc_globals m gl = Some m' -> + Mem.valid_block m b' -> + (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm). +Proof. + induction gl. + simpl; intros. inv H. tauto. + simpl; intros. destruct (alloc_global m a) as [m1|]_eqn; try discriminate. + erewrite alloc_global_perm; eauto. eapply IHgl; eauto. + unfold Mem.valid_block in *. erewrite alloc_global_nextblock; eauto. omega. Qed. +(** Data preservation properties *) + Remark store_zeros_outside: - forall m b n m', - store_zeros m b n = Some m' -> - forall chunk b' p, - b' <> b -> Mem.load chunk m' b' p = Mem.load chunk m b' p. + forall m b p n m', + store_zeros m b p n = Some m' -> + forall chunk b' p', + b' <> b \/ p' + size_chunk chunk <= p \/ p + n <= p' -> + Mem.load chunk m' b' p' = Mem.load chunk m b' p'. Proof. - intros until n. functional induction (store_zeros m b n); intros. + intros until n. functional induction (store_zeros m b p n); intros. inv H; auto. - rewrite IHo; auto. eapply Mem.load_store_other; eauto. - inv H. + transitivity (Mem.load chunk m' b' p'). + apply IHo. auto. unfold block in *; omega. + eapply Mem.load_store_other; eauto. simpl. unfold block in *; omega. + discriminate. Qed. Remark store_init_data_list_outside: @@ -854,12 +735,12 @@ Remark store_init_data_list_outside: Proof. induction il; simpl. intros; congruence. - intros until m'. caseEq (store_init_data m b p a); try congruence. - intros m1 A B chunk b' q C. transitivity (Mem.load chunk m1 b' q). + intros. destruct (store_init_data m b p a) as [m1|]_eqn; try congruence. + transitivity (Mem.load chunk m1 b' q). eapply IHil; eauto. generalize (init_data_size_pos a). intuition omega. - destruct a; simpl in A; + destruct a; simpl in Heqo; try (eapply Mem.load_store_other; eauto; intuition; fail). - congruence. + inv Heqo. auto. destruct (find_symbol ge i); try congruence. eapply Mem.load_store_other; eauto; intuition. Qed. @@ -904,10 +785,9 @@ Proof. induction il; simpl. auto. - intros until m'. caseEq (store_init_data m b p a); try congruence. - intros m1 B C. + intros. destruct (store_init_data m b p a) as [m1|]_eqn; try congruence. exploit IHil; eauto. intro D. - destruct a; simpl in B; intuition. + destruct a; simpl in Heqo; intuition. eapply (A Mint8unsigned (Vint i)); eauto. eapply (A Mint16unsigned (Vint i)); eauto. eapply (A Mint32 (Vint i)); eauto. @@ -917,36 +797,49 @@ Proof. eapply (A Mint32 (Vptr b0 i0)); eauto. Qed. -Remark load_alloc_variables: - forall chunk b p vl m m', - alloc_variables m vl = Some m' -> +Remark load_alloc_global: + forall chunk b p id g m m', + alloc_global m (id, g) = Some m' -> Mem.valid_block m b -> Mem.load chunk m' b p = Mem.load chunk m b p. Proof. - induction vl; simpl; intros until m'. - congruence. - unfold alloc_variable. - set (init := gvar_init a#2). - set (sz := init_data_list_size init). - caseEq (Mem.alloc m 0 sz). intros m1 b1 ALLOC. - caseEq (store_zeros m1 b1 sz); try congruence. intros m2 STZ. - caseEq (store_init_data_list m2 b1 0 init); try congruence. intros m3 STORE. - caseEq (Mem.drop_perm m3 b1 0 sz (perm_globvar a#2)); try congruence. intros m4 DROP REC VALID. - assert (b <> b1). apply Mem.valid_not_valid_diff with m; eauto with mem. - transitivity (Mem.load chunk m4 b p). - apply IHvl; auto. red. - rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). - rewrite (store_init_data_list_nextblock _ _ _ _ STORE). - rewrite (store_zeros_nextblock _ _ _ STZ). - change (Mem.valid_block m1 b). eauto with mem. - transitivity (Mem.load chunk m3 b p). + intros. destruct g as [f|v]; simpl in H. + (* function *) + destruct (Mem.alloc m 0 1) as [m1 b']_eqn. + assert (b <> b'). apply Mem.valid_not_valid_diff with m; eauto with mem. + transitivity (Mem.load chunk m1 b p). eapply Mem.load_drop; eauto. + eapply Mem.load_alloc_unchanged; eauto. + (* variable *) + set (init := gvar_init v) in *. + set (sz := init_data_list_size init) in *. + destruct (Mem.alloc m 0 sz) as [m1 b']_eqn. + destruct (store_zeros m1 b' 0 sz) as [m2|]_eqn; try discriminate. + destruct (store_init_data_list m2 b' 0 init) as [m3|]_eqn; try discriminate. + assert (b <> b'). apply Mem.valid_not_valid_diff with m; eauto with mem. + transitivity (Mem.load chunk m3 b p). + eapply Mem.load_drop; eauto. transitivity (Mem.load chunk m2 b p). - eapply store_init_data_list_outside; eauto. + eapply store_init_data_list_outside; eauto. transitivity (Mem.load chunk m1 b p). eapply store_zeros_outside; eauto. eapply Mem.load_alloc_unchanged; eauto. -Qed. +Qed. + +Remark load_alloc_globals: + forall chunk b p gl m m', + alloc_globals m gl = Some m' -> + Mem.valid_block m b -> + Mem.load chunk m' b p = Mem.load chunk m b p. +Proof. + induction gl; simpl; intros. + congruence. + destruct (alloc_global m a) as [m''|]_eqn; try discriminate. + transitivity (Mem.load chunk m'' b p). + apply IHgl; auto. unfold Mem.valid_block in *. + erewrite alloc_global_nextblock; eauto. omega. + destruct a as [id g]. eapply load_alloc_global; eauto. +Qed. Remark load_store_init_data_invariant: forall m m' b, @@ -967,114 +860,147 @@ Definition variables_initialized (g: t) (m: mem) := 0 <= ofs < init_data_list_size gv.(gvar_init) /\ perm_order (perm_globvar gv) p) /\ (gv.(gvar_volatile) = false -> load_store_init_data m b 0 gv.(gvar_init)). -Lemma alloc_variable_initialized: - forall g m id v m', - genv_nextvar g = Mem.nextblock m -> - alloc_variable m (id, v) = Some m' -> - variables_initialized g m -> - variables_initialized (add_variable g (id, v)) m' - /\ genv_nextvar (add_variable g (id,v)) = Mem.nextblock m'. -Proof. - intros. revert H0. unfold alloc_variable. simpl. - set (il := gvar_init v). - set (sz := init_data_list_size il). - caseEq (Mem.alloc m 0 sz). intros m1 b1 ALLOC. - caseEq (store_zeros m1 b1 sz); try congruence. intros m2 ZEROS. - caseEq (store_init_data_list m2 b1 0 il); try congruence. intros m3 INIT DROP. - exploit Mem.nextblock_alloc; eauto. intros NB1. - assert (Mem.nextblock m' = Mem.nextblock m1). - rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). - rewrite (store_init_data_list_nextblock _ _ _ _ INIT). - eapply store_zeros_nextblock; eauto. - exploit Mem.alloc_result; eauto. intro RES. - split. - (* var-init *) - red; intros. revert H2. - unfold add_variable, find_var_info; simpl. - rewrite H; rewrite <- RES. - rewrite ZMap.gsspec. destruct (ZIndexed.eq b b1); intros VI. - (* new var *) - injection VI; intro EQ. subst b gv. clear VI. - fold il. fold sz. - split. red; intros. eapply Mem.perm_drop_1; eauto. - split. intros. - assert (0 <= ofs < sz). - eapply Mem.perm_alloc_3; eauto. - rewrite store_zeros_perm; [idtac|eauto]. - rewrite store_init_data_list_perm; [idtac|eauto]. - eapply Mem.perm_drop_4; eauto. - split; auto. eapply Mem.perm_drop_2; eauto. +Definition functions_initialized (g: t) (m: mem) := + forall b fd, + find_funct_ptr g b = Some fd -> + Mem.perm m b 0 Cur Nonempty + /\ (forall ofs k p, Mem.perm m b ofs k p -> ofs = 0 /\ perm_order Nonempty p). + +Lemma alloc_global_initialized: + forall ge m id g m', + genv_next ge = Mem.nextblock m -> + alloc_global m (id, g) = Some m' -> + variables_initialized ge m -> + functions_initialized ge m -> + variables_initialized (add_global ge (id, g)) m' + /\ functions_initialized (add_global ge (id, g)) m' + /\ genv_next (add_global ge (id, g)) = Mem.nextblock m'. +Proof. intros. - apply load_store_init_data_invariant with m3. - intros. eapply Mem.load_drop; eauto. right; right; right. - unfold perm_globvar. destruct (gvar_volatile v); try discriminate. - destruct (gvar_readonly v); auto with mem. + exploit alloc_global_nextblock; eauto. intros NB. split. +(* variables-initialized *) + destruct g as [f|v]. +(* function *) + red; intros. unfold find_var_info in H3. simpl in H3. + exploit H1; eauto. intros [A [B C]]. + assert (D: Mem.valid_block m b). + red. exploit genv_vars_range; eauto. rewrite H; omega. + split. red; intros. erewrite <- alloc_global_perm; eauto. + split. intros. eapply B. erewrite alloc_global_perm; eauto. + intros. apply load_store_init_data_invariant with m; auto. + intros. eapply load_alloc_global; eauto. +(* variable *) + red; intros. unfold find_var_info in H3. simpl in H3. rewrite ZMap.gsspec in H3. + destruct (ZIndexed.eq b (genv_next ge0)). + (* same *) + inv H3. simpl in H0. + set (init := gvar_init gv) in *. + set (sz := init_data_list_size init) in *. + destruct (Mem.alloc m 0 sz) as [m1 b']_eqn. + destruct (store_zeros m1 b' 0 sz) as [m2|]_eqn; try discriminate. + destruct (store_init_data_list m2 b' 0 init) as [m3|]_eqn; try discriminate. + exploit Mem.alloc_result; eauto. intro RES. + replace (genv_next ge0) with b' by congruence. + split. red; intros. eapply Mem.perm_drop_1; eauto. + split. intros. + assert (0 <= ofs < sz). + eapply Mem.perm_alloc_3; eauto. + erewrite store_zeros_perm; [idtac|eauto]. + erewrite store_init_data_list_perm; [idtac|eauto]. + eapply Mem.perm_drop_4; eauto. + split. auto. eapply Mem.perm_drop_2; eauto. + intros. apply load_store_init_data_invariant with m3. + intros. eapply Mem.load_drop; eauto. + right; right; right. unfold perm_globvar. rewrite H3. + destruct (gvar_readonly gv); auto with mem. eapply store_init_data_list_charact; eauto. - (* older vars *) + (* older var *) exploit H1; eauto. intros [A [B C]]. - split. red; intros. eapply Mem.perm_drop_3; eauto. - rewrite <- store_init_data_list_perm; [idtac|eauto]. - rewrite <- store_zeros_perm; [idtac|eauto]. - eapply Mem.perm_alloc_1; eauto. - split. intros. eapply B. - eapply Mem.perm_alloc_4; eauto. - rewrite store_zeros_perm; [idtac|eauto]. - rewrite store_init_data_list_perm; [idtac|eauto]. - eapply Mem.perm_drop_4; eauto. - intros. apply load_store_init_data_invariant with m; auto. - intros. transitivity (Mem.load chunk m3 b ofs). - eapply Mem.load_drop; eauto. - transitivity (Mem.load chunk m2 b ofs). - eapply store_init_data_list_outside; eauto. - transitivity (Mem.load chunk m1 b ofs). - eapply store_zeros_outside; eauto. - eapply Mem.load_alloc_unchanged; eauto. - red. exploit genv_vars_range; eauto. rewrite <- H. omega. - rewrite H0; rewrite NB1; rewrite H; auto. -Qed. - -Lemma alloc_variables_initialized: - forall vl g m m', - genv_nextvar g = Mem.nextblock m -> - alloc_variables m vl = Some m' -> - variables_initialized g m -> - variables_initialized (add_variables g vl) m'. -Proof. - induction vl; simpl; intros. + assert (D: Mem.valid_block m b). + red. exploit genv_vars_range; eauto. rewrite H; omega. + split. red; intros. erewrite <- alloc_global_perm; eauto. + split. intros. eapply B. erewrite alloc_global_perm; eauto. + intros. apply load_store_init_data_invariant with m; auto. + intros. eapply load_alloc_global; eauto. +(* functions-initialized *) + split. destruct g as [f|v]. +(* function *) + red; intros. unfold find_funct_ptr in H3. simpl in H3. rewrite ZMap.gsspec in H3. + destruct (ZIndexed.eq b (genv_next ge0)). + (* same *) + inv H3. simpl in H0. + destruct (Mem.alloc m 0 1) as [m1 b']_eqn. + exploit Mem.alloc_result; eauto. intro RES. + replace (genv_next ge0) with b' by congruence. + split. eapply Mem.perm_drop_1; eauto. omega. + intros. + assert (0 <= ofs < 1). + eapply Mem.perm_alloc_3; eauto. + eapply Mem.perm_drop_4; eauto. + split. omega. eapply Mem.perm_drop_2; eauto. + (* older function *) + exploit H2; eauto. intros [A B]. + assert (D: Mem.valid_block m b). + red. exploit genv_funs_range; eauto. rewrite H; omega. + split. erewrite <- alloc_global_perm; eauto. + intros. eapply B. erewrite alloc_global_perm; eauto. +(* variables *) + red; intros. unfold find_funct_ptr in H3. simpl in H3. + exploit H2; eauto. intros [A B]. + assert (D: Mem.valid_block m b). + red. exploit genv_funs_range; eauto. rewrite H; omega. + split. erewrite <- alloc_global_perm; eauto. + intros. eapply B. erewrite alloc_global_perm; eauto. +(* nextblock *) + rewrite NB. simpl. rewrite H. unfold block; omega. +Qed. + +Lemma alloc_globals_initialized: + forall gl ge m m', + genv_next ge = Mem.nextblock m -> + alloc_globals m gl = Some m' -> + variables_initialized ge m -> + functions_initialized ge m -> + variables_initialized (add_globals ge gl) m' /\ functions_initialized (add_globals ge gl) m'. +Proof. + induction gl; simpl; intros. inv H0; auto. - destruct (alloc_variable m a) as [m1|]_eqn; try discriminate. - destruct a as [id gv]. - exploit alloc_variable_initialized; eauto. intros [P Q]. - eapply IHvl; eauto. + destruct a as [id g]. destruct (alloc_global m (id, g)) as [m1|]_eqn; try discriminate. + exploit alloc_global_initialized; eauto. intros [P [Q R]]. + eapply IHgl; eauto. Qed. End INITMEM. Definition init_mem (p: program F V) := - alloc_variables (globalenv p) Mem.empty p.(prog_vars). + alloc_globals (globalenv p) Mem.empty p.(prog_defs). + +Lemma init_mem_genv_next: forall p m, + init_mem p = Some m -> + genv_next (globalenv p) = Mem.nextblock m. +Proof. + unfold init_mem; intros. + exploit alloc_globals_nextblock; eauto. rewrite Mem.nextblock_empty. intro. + generalize (genv_next_add_globals (prog_defs p) empty_genv). + fold (globalenv p). simpl genv_next. intros. congruence. +Qed. Theorem find_symbol_not_fresh: forall p id b m, init_mem p = Some m -> find_symbol (globalenv p) id = Some b -> Mem.valid_block m b. Proof. - unfold init_mem; intros. - exploit alloc_variables_nextblock; eauto. rewrite Mem.nextblock_empty. intro. - exploit genv_symb_range; eauto. intros. - generalize (add_variables_nextvar (prog_vars p) (add_functions empty_genv (prog_funct p))). - rewrite add_functions_nextvar. simpl genv_nextvar. intro. - red. rewrite H1. rewrite <- H3. intuition. + intros. red. erewrite <- init_mem_genv_next; eauto. + exploit genv_symb_range; eauto. omega. Qed. -Lemma init_mem_genv_vars : forall p m, - init_mem p = Some m -> - genv_nextvar (globalenv p) = Mem.nextblock m. +Theorem find_funct_ptr_not_fresh: + forall p b f m, + init_mem p = Some m -> + find_funct_ptr (globalenv p) b = Some f -> Mem.valid_block m b. Proof. - clear. unfold globalenv, init_mem. intros. - exploit alloc_variables_nextblock; eauto. - simpl (Mem.nextblock Mem.empty). - rewrite add_variables_nextvar. rewrite add_functions_nextvar. - simpl (genv_nextvar empty_genv). auto. + intros. red. erewrite <- init_mem_genv_next; eauto. + exploit genv_funs_range; eauto. omega. Qed. Theorem find_var_info_not_fresh: @@ -1082,12 +1008,8 @@ Theorem find_var_info_not_fresh: init_mem p = Some m -> find_var_info (globalenv p) b = Some gv -> Mem.valid_block m b. Proof. - unfold init_mem; intros. - exploit alloc_variables_nextblock; eauto. rewrite Mem.nextblock_empty. intro. - exploit genv_vars_range; eauto. intros. - generalize (add_variables_nextvar (prog_vars p) (add_functions empty_genv (prog_funct p))). - rewrite add_functions_nextvar. simpl genv_nextvar. intro. - red. rewrite H1. rewrite <- H3. intuition. + intros. red. erewrite <- init_mem_genv_next; eauto. + exploit genv_vars_range; eauto. omega. Qed. Theorem init_mem_characterization: @@ -1099,10 +1021,23 @@ Theorem init_mem_characterization: 0 <= ofs < init_data_list_size gv.(gvar_init) /\ perm_order (perm_globvar gv) p) /\ (gv.(gvar_volatile) = false -> load_store_init_data (globalenv p) m b 0 gv.(gvar_init)). Proof. - intros. eapply alloc_variables_initialized; eauto. - rewrite add_functions_nextvar; auto. - red; intros. exploit genv_vars_range; eauto. rewrite add_functions_nextvar. - simpl. intros. omegaContradiction. + intros. eapply alloc_globals_initialized; eauto. + rewrite Mem.nextblock_empty. auto. + red; intros. exploit genv_vars_range; eauto. simpl. intros. omegaContradiction. + red; intros. exploit genv_funs_range; eauto. simpl. intros. omegaContradiction. +Qed. + +Theorem init_mem_characterization_2: + forall p b fd m, + find_funct_ptr (globalenv p) b = Some fd -> + init_mem p = Some m -> + Mem.perm m b 0 Cur Nonempty + /\ (forall ofs k p, Mem.perm m b ofs k p -> ofs = 0 /\ perm_order Nonempty p). +Proof. + intros. unfold init_mem in H0. eapply alloc_globals_initialized; eauto. + rewrite Mem.nextblock_empty. auto. + red; intros. exploit genv_vars_range; eauto. simpl. intros. omegaContradiction. + red; intros. exploit genv_funs_range; eauto. simpl. intros. omegaContradiction. Qed. (** ** Compatibility with memory injections *) @@ -1113,6 +1048,19 @@ Variable ge: t. Variable thr: block. Hypothesis symb_inject: forall id b, find_symbol ge id = Some b -> b < thr. +Lemma store_zeros_neutral: + forall m b p n m', + Mem.inject_neutral thr m -> + b < thr -> + store_zeros m b p n = Some m' -> + Mem.inject_neutral thr m'. +Proof. + intros until n. functional induction (store_zeros m b p n); intros. + inv H1; auto. + apply IHo; auto. eapply Mem.store_inject_neutral; eauto. constructor. + inv H1. +Qed. + Lemma store_init_data_neutral: forall m b p id m', Mem.inject_neutral thr m -> @@ -1122,7 +1070,7 @@ Lemma store_init_data_neutral: Proof. intros. destruct id; simpl in H1; try (eapply Mem.store_inject_neutral; eauto; fail). - inv H1; auto. + congruence. revert H1. caseEq (find_symbol ge i); try congruence. intros b' FS ST. eapply Mem.store_inject_neutral; eauto. econstructor. unfold Mem.flat_inj. apply zlt_true; eauto. @@ -1143,54 +1091,46 @@ Proof. eapply IHidl. eapply store_init_data_neutral; eauto. auto. eauto. Qed. -Lemma store_zeros_neutral: - forall m b n m', - Mem.inject_neutral thr m -> - b < thr -> - store_zeros m b n = Some m' -> - Mem.inject_neutral thr m'. -Proof. - intros until n. functional induction (store_zeros m b n); intros. - inv H1; auto. - apply IHo; auto. eapply Mem.store_inject_neutral; eauto. constructor. - inv H1. -Qed. - -Lemma alloc_variable_neutral: - forall id m m', - alloc_variable ge m id = Some m' -> +Lemma alloc_global_neutral: + forall idg m m', + alloc_global ge m idg = Some m' -> Mem.inject_neutral thr m -> Mem.nextblock m < thr -> Mem.inject_neutral thr m'. Proof. - intros until m'. unfold alloc_variable. - set (init := gvar_init id#2). - set (sz := init_data_list_size init). - caseEq (Mem.alloc m 0 sz); try congruence. intros m1 b ALLOC. - caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ. - caseEq (store_init_data_list ge m2 b 0 init); try congruence. - intros m3 STORE DROP NEUTRAL NEXT. - assert (b < thr). rewrite (Mem.alloc_result _ _ _ _ _ ALLOC). auto. + intros. destruct idg as [id [f|v]]; simpl in H. + (* function *) + destruct (Mem.alloc m 0 1) as [m1 b]_eqn. + assert (b < thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto. + eapply Mem.drop_inject_neutral; eauto. + eapply Mem.alloc_inject_neutral; eauto. + (* variable *) + set (init := gvar_init v) in *. + set (sz := init_data_list_size init) in *. + destruct (Mem.alloc m 0 sz) as [m1 b]_eqn. + destruct (store_zeros m1 b 0 sz) as [m2|]_eqn; try discriminate. + destruct (store_init_data_list ge m2 b 0 init) as [m3|]_eqn; try discriminate. + assert (b < thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto. eapply Mem.drop_inject_neutral; eauto. eapply store_init_data_list_neutral with (m := m2) (b := b); eauto. eapply store_zeros_neutral with (m := m1); eauto. eapply Mem.alloc_inject_neutral; eauto. Qed. -Lemma alloc_variables_neutral: - forall idl m m', - alloc_variables ge m idl = Some m' -> +Lemma alloc_globals_neutral: + forall gl m m', + alloc_globals ge m gl = Some m' -> Mem.inject_neutral thr m -> Mem.nextblock m' <= thr -> Mem.inject_neutral thr m'. Proof. - induction idl; simpl. + induction gl; simpl. intros. congruence. - intros until m'. caseEq (alloc_variable ge m a); try congruence. intros. - assert (Mem.nextblock m' = Mem.nextblock m + Z_of_nat(length (a :: idl))). - eapply alloc_variables_nextblock with ge. simpl. rewrite H. auto. + intros until m'. caseEq (alloc_global ge m a); try congruence. intros. + assert (Mem.nextblock m' = Mem.nextblock m + Z_of_nat(length (a :: gl))). + eapply alloc_globals_nextblock with ge. simpl. rewrite H. auto. simpl length in H3. rewrite inj_S in H3. - exploit alloc_variable_neutral; eauto. unfold block in *; omega. + exploit alloc_global_neutral; eauto. unfold block in *; omega. Qed. End INITMEM_INJ. @@ -1202,7 +1142,7 @@ Theorem initmem_inject: Proof. unfold init_mem; intros. apply Mem.neutral_inject. - eapply alloc_variables_neutral; eauto. + eapply alloc_globals_neutral; eauto. intros. exploit find_symbol_not_fresh; eauto. apply Mem.empty_inject_neutral. omega. @@ -1213,6 +1153,22 @@ Section INITMEM_AUGMENT_INJ. Variable ge: t. Variable thr: block. +Lemma store_zeros_augment: + forall m1 m2 b p n m2', + Mem.inject (Mem.flat_inj thr) m1 m2 -> + b >= thr -> + store_zeros m2 b p n = Some m2' -> + Mem.inject (Mem.flat_inj thr) m1 m2'. +Proof. + intros until n. functional induction (store_zeros m2 b p n); intros. + inv H1; auto. + apply IHo; auto. exploit Mem.store_outside_inject; eauto. simpl. + intros. exfalso. unfold Mem.flat_inj in H2. destruct (zlt b' thr). + inversion H2; subst; omega. + discriminate. + inv H1. +Qed. + Lemma store_init_data_augment: forall m1 m2 b p id m2', Mem.inject (Mem.flat_inj thr) m1 m2 -> @@ -1228,7 +1184,7 @@ Proof. intros. unfold Mem.flat_inj in H0. destruct (zlt b' thr); inversion H0; subst. omega. destruct id; simpl in ST; try (eapply P; eauto; fail). - inv ST; auto. + congruence. revert ST. caseEq (find_symbol ge i); try congruence. intros; eapply P; eauto. Qed. @@ -1246,59 +1202,49 @@ Proof. eapply IHidl. eapply store_init_data_augment; eauto. auto. eauto. Qed. -Lemma store_zeros_augment: - forall m1 m2 b n m2', - Mem.inject (Mem.flat_inj thr) m1 m2 -> - b >= thr -> - store_zeros m2 b n = Some m2' -> - Mem.inject (Mem.flat_inj thr) m1 m2'. -Proof. - intros until n. functional induction (store_zeros m2 b n); intros. - inv H1; auto. - apply IHo; auto. exploit Mem.store_outside_inject; eauto. simpl. - intros. exfalso. unfold Mem.flat_inj in H2. destruct (zlt b' thr). - inversion H2; subst; omega. - discriminate. - inv H1. -Qed. - -Lemma alloc_variable_augment: - forall id m1 m2 m2', - alloc_variable ge m2 id = Some m2' -> +Lemma alloc_global_augment: + forall idg m1 m2 m2', + alloc_global ge m2 idg = Some m2' -> Mem.inject (Mem.flat_inj thr) m1 m2 -> Mem.nextblock m2 >= thr -> Mem.inject (Mem.flat_inj thr) m1 m2'. Proof. - intros until m2'. unfold alloc_variable. - set (sz := init_data_list_size (gvar_init id#2)). - caseEq (Mem.alloc m2 0 sz); try congruence. intros m3 b ALLOC. - caseEq (store_zeros m3 b sz); try congruence. intros m4 STZ. - caseEq (store_init_data_list ge m4 b 0 (gvar_init id#2)); try congruence. - intros m5 STORE DROP INJ NEXT. - assert (b >= thr). - pose proof (Mem.fresh_block_alloc _ _ _ _ _ ALLOC). - unfold Mem.valid_block in H. unfold block in *; omega. - eapply Mem.drop_outside_inject. 2: eauto. - eapply store_init_data_list_augment. 2: eauto. 2: eauto. - eapply store_zeros_augment. 2: eauto. 2: eauto. - eapply Mem.alloc_right_inject; eauto. - intros. unfold Mem.flat_inj in H0. destruct (zlt b' thr); inversion H0. + intros. destruct idg as [id [f|v]]; simpl in H. + (* function *) + destruct (Mem.alloc m2 0 1) as [m3 b]_eqn. + assert (b >= thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto. + eapply Mem.drop_outside_inject. 2: eauto. + eapply Mem.alloc_right_inject; eauto. + intros. unfold Mem.flat_inj in H3. destruct (zlt b' thr); inversion H3. + subst; exfalso; omega. + (* variable *) + set (init := gvar_init v) in *. + set (sz := init_data_list_size init) in *. + destruct (Mem.alloc m2 0 sz) as [m3 b]_eqn. + destruct (store_zeros m3 b 0 sz) as [m4|]_eqn; try discriminate. + destruct (store_init_data_list ge m4 b 0 init) as [m5|]_eqn; try discriminate. + assert (b >= thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto. + eapply Mem.drop_outside_inject. 2: eauto. + eapply store_init_data_list_augment. 3: eauto. 2: eauto. + eapply store_zeros_augment. 3: eauto. 2: eauto. + eapply Mem.alloc_right_inject; eauto. + intros. unfold Mem.flat_inj in H3. destruct (zlt b' thr); inversion H3. subst; exfalso; omega. Qed. -Lemma alloc_variables_augment: - forall idl m1 m2 m2', - alloc_variables ge m2 idl = Some m2' -> +Lemma alloc_globals_augment: + forall gl m1 m2 m2', + alloc_globals ge m2 gl = Some m2' -> Mem.inject (Mem.flat_inj thr) m1 m2 -> Mem.nextblock m2 >= thr -> Mem.inject (Mem.flat_inj thr) m1 m2'. Proof. - induction idl; simpl. + induction gl; simpl. intros. congruence. - intros until m2'. caseEq (alloc_variable ge m2 a); try congruence. intros. - eapply IHidl with (m2 := m); eauto. - eapply alloc_variable_augment; eauto. - rewrite (alloc_variable_nextblock _ _ _ H). + intros until m2'. caseEq (alloc_global ge m2 a); try congruence. intros. + eapply IHgl with (m2 := m); eauto. + eapply alloc_global_augment; eauto. + rewrite (alloc_global_nextblock _ _ _ H). unfold block in *; omega. Qed. @@ -1321,216 +1267,156 @@ Inductive match_globvar: globvar V -> globvar W -> Prop := match_varinfo info1 info2 -> match_globvar (mkglobvar info1 init ro vo) (mkglobvar info2 init ro vo). -Record match_genvs (new_functs : list (ident * B)) (new_vars : list (ident * globvar W)) +Record match_genvs (new_globs : list (ident * globdef B W)) (ge1: t A V) (ge2: t B W): Prop := { - mge_nextfun: genv_nextfun ge2 = genv_nextfun ge1 - Z_of_nat(length new_functs); - mge_nextvar: genv_nextvar ge2 = genv_nextvar ge1 + Z_of_nat(length new_vars); - mge_symb: forall id, ~ In id ((funct_names new_functs) ++ (var_names new_vars)) -> + mge_next: + genv_next ge2 = genv_next ge1 + Z_of_nat(length new_globs); + mge_symb: + forall id, ~ In id (map fst new_globs) -> PTree.get id (genv_symb ge2) = PTree.get id (genv_symb ge1); mge_funs: forall b f, ZMap.get b (genv_funs ge1) = Some f -> exists tf, ZMap.get b (genv_funs ge2) = Some tf /\ match_fun f tf; mge_rev_funs: forall b tf, ZMap.get b (genv_funs ge2) = Some tf -> - if zlt (genv_nextfun ge1) b then + if zlt b (genv_next ge1) then exists f, ZMap.get b (genv_funs ge1) = Some f /\ match_fun f tf else - In tf (map (@snd ident B) new_functs); + In (Gfun tf) (map snd new_globs); mge_vars: forall b v, ZMap.get b (genv_vars ge1) = Some v -> exists tv, ZMap.get b (genv_vars ge2) = Some tv /\ match_globvar v tv; mge_rev_vars: forall b tv, ZMap.get b (genv_vars ge2) = Some tv -> - if zlt b (genv_nextvar ge1) then + if zlt b (genv_next ge1) then exists v, ZMap.get b (genv_vars ge1) = Some v /\ match_globvar v tv else - In tv (map (@snd ident (globvar W)) new_vars) + In (Gvar tv) (map snd new_globs) }. -Lemma add_function_match: - forall ge1 ge2 id f1 f2, - match_genvs nil nil ge1 ge2 -> - match_fun f1 f2 -> - match_genvs nil nil (add_function ge1 (id, f1)) (add_function ge2 (id, f2)). +Lemma add_global_match: + forall ge1 ge2 idg1 idg2, + match_genvs nil ge1 ge2 -> + match_globdef match_fun match_varinfo idg1 idg2 -> + match_genvs nil (add_global ge1 idg1) (add_global ge2 idg2). Proof. intros. destruct H. - simpl in mge_nextfun0. rewrite Zminus_0_r in mge_nextfun0. - simpl in mge_nextvar0. rewrite Zplus_0_r in mge_nextvar0. - constructor; simpl. - rewrite Zminus_0_r. congruence. + simpl in mge_next0. rewrite Zplus_0_r in mge_next0. + inv H0. +(* two functions *) + constructor; simpl. rewrite Zplus_0_r. congruence. - intros. rewrite mge_nextfun0. - repeat rewrite PTree.gsspec. destruct (peq id0 id); auto. - rewrite mge_nextfun0. intros. rewrite ZMap.gsspec in H. rewrite ZMap.gsspec. - destruct (ZIndexed.eq b (genv_nextfun ge1)). + intros. rewrite mge_next0. + repeat rewrite PTree.gsspec. destruct (peq id0 id); auto. + rewrite mge_next0. intros. rewrite ZMap.gsspec in H0. rewrite ZMap.gsspec. + destruct (ZIndexed.eq b (genv_next ge1)). exists f2; split; congruence. eauto. - rewrite mge_nextfun0. intros. rewrite ZMap.gsspec in H. rewrite ZMap.gsspec. - destruct (ZIndexed.eq b (genv_nextfun ge1)). - subst b. destruct (zlt (genv_nextfun ge1 - 1) (genv_nextfun ge1)). - exists f1; split; congruence. omega. - pose proof (mge_rev_funs0 b tf H). - destruct (zlt (genv_nextfun ge1) b); - destruct (zlt (genv_nextfun ge1 - 1) b). auto. omega. exfalso; omega. intuition. - auto. - auto. -Qed. - -Lemma add_functions_match: - forall fl1 fl2, list_forall2 (match_funct_entry match_fun) fl1 fl2 -> - forall ge1 ge2, match_genvs nil nil ge1 ge2 -> - match_genvs nil nil (add_functions ge1 fl1) (add_functions ge2 fl2). -Proof. - induction 1; intros; simpl. - auto. - destruct a1 as [id1 f1]; destruct b1 as [id2 f2]. - destruct H. subst. apply IHlist_forall2. apply add_function_match; auto. -Qed. - -Lemma add_function_augment_match: - forall new_functs new_vars ge1 ge2 id f2, - match_genvs new_functs new_vars ge1 ge2 -> - match_genvs (new_functs++((id,f2)::nil)) new_vars ge1 (add_function ge2 (id, f2)). -Proof. - intros. destruct H. constructor; simpl. - rewrite mge_nextfun0. rewrite app_length. - simpl. rewrite inj_plus. rewrite inj_S. rewrite inj_0. unfold block; omega. (* painful! *) - auto. - intros. unfold funct_names in H. rewrite map_app in H. rewrite in_app in H. rewrite in_app in H. simpl in H. - destruct (peq id id0). subst. intuition. rewrite PTree.gso. - apply mge_symb0. intro. apply H. rewrite in_app in H0. inversion H0; intuition. intuition. - intros. rewrite ZMap.gso. auto. - rewrite mge_nextfun0. pose proof (genv_funs_range ge1 b H). intro; subst; omega. - intros. rewrite ZMap.gsspec in H. - destruct (ZIndexed.eq b (genv_nextfun ge2)). - destruct (zlt (genv_nextfun ge1) b). - exfalso. rewrite mge_nextfun0 in e. unfold block; omega. - rewrite map_app. rewrite in_app. simpl. inversion H; intuition. - pose proof (mge_rev_funs0 b tf H). - destruct (zlt (genv_nextfun ge1) b). - auto. - rewrite map_app. rewrite in_app. intuition. - auto. - auto. -Qed. - - -Lemma add_functions_augment_match: - forall fl new_functs new_vars ge1 ge2, - match_genvs new_functs new_vars ge1 ge2 -> - match_genvs (new_functs++fl) new_vars ge1 (add_functions ge2 fl). -Proof. - induction fl; simpl. - intros. rewrite app_nil_r. auto. - intros. replace (new_functs ++ a :: fl) with ((new_functs ++ (a::nil)) ++ fl) - by (rewrite app_ass; auto). - apply IHfl. destruct a. apply add_function_augment_match. auto. -Qed. - - -Lemma add_variable_match: - forall new_functs ge1 ge2 id v1 v2, - match_genvs new_functs nil ge1 ge2 -> - match_globvar v1 v2 -> - match_genvs new_functs nil (add_variable ge1 (id, v1)) (add_variable ge2 (id, v2)). -Proof. - intros. destruct H. - simpl in mge_nextvar0. rewrite Zplus_0_r in mge_nextvar0. - constructor; simpl. - auto. - rewrite Zplus_0_r. rewrite mge_nextvar0. auto. - intros. rewrite mge_nextvar0. - repeat rewrite PTree.gsspec. destruct (peq id0 id); auto. - auto. - auto. - rewrite mge_nextvar0. intros. rewrite ZMap.gsspec in H. rewrite ZMap.gsspec. - destruct (ZIndexed.eq b (genv_nextvar ge1)). - exists v2; split; congruence. - eauto. - rewrite mge_nextvar0. intros. rewrite ZMap.gsspec in H. rewrite ZMap.gsspec. - destruct (ZIndexed.eq b (genv_nextvar ge1)). - subst b. inversion H; subst. - destruct (zlt (genv_nextvar ge1) (genv_nextvar ge1 + 1)). - exists v1; split; congruence. omega. - pose proof (mge_rev_vars0 _ _ H). - destruct (zlt b (genv_nextvar ge1)); - destruct (zlt b (genv_nextvar ge1 + 1)). auto. omega. exfalso; omega. intuition. + rewrite mge_next0. intros. rewrite ZMap.gsspec in H0. rewrite ZMap.gsspec. + destruct (ZIndexed.eq b (genv_next ge1)). + subst b. rewrite zlt_true. exists f1; split; congruence. omega. + pose proof (mge_rev_funs0 b tf H0). + destruct (zlt b (genv_next ge1)). rewrite zlt_true. auto. omega. + contradiction. + eauto. + intros. + pose proof (mge_rev_vars0 b tv H0). + destruct (zlt b (genv_next ge1)). rewrite zlt_true. auto. omega. + contradiction. +(* two variables *) + constructor; simpl. + rewrite Zplus_0_r. congruence. + intros. rewrite mge_next0. + repeat rewrite PTree.gsspec. destruct (peq id0 id); auto. + eauto. + intros. + pose proof (mge_rev_funs0 b tf H0). + destruct (zlt b (genv_next ge1)). rewrite zlt_true. auto. omega. + contradiction. + rewrite mge_next0. intros. rewrite ZMap.gsspec in H0. rewrite ZMap.gsspec. + destruct (ZIndexed.eq b (genv_next ge1)). + econstructor; split. eauto. inv H0. constructor; auto. + eauto. + rewrite mge_next0. intros. rewrite ZMap.gsspec in H0. rewrite ZMap.gsspec. + destruct (ZIndexed.eq b (genv_next ge1)). + subst b. rewrite zlt_true. + econstructor; split. eauto. inv H0. constructor; auto. + omega. + pose proof (mge_rev_vars0 b tv H0). + destruct (zlt b (genv_next ge1)). rewrite zlt_true. auto. omega. + contradiction. Qed. -Lemma add_variables_match: - forall vl1 vl2, list_forall2 (match_var_entry match_varinfo) vl1 vl2 -> - forall new_functs ge1 ge2, match_genvs new_functs nil ge1 ge2 -> - match_genvs new_functs nil (add_variables ge1 vl1) (add_variables ge2 vl2). +Lemma add_globals_match: + forall gl1 gl2, list_forall2 (match_globdef match_fun match_varinfo) gl1 gl2 -> + forall ge1 ge2, match_genvs nil ge1 ge2 -> + match_genvs nil (add_globals ge1 gl1) (add_globals ge2 gl2). Proof. induction 1; intros; simpl. auto. - inv H. apply IHlist_forall2. apply add_variable_match; auto. constructor; auto. + apply IHlist_forall2. apply add_global_match; auto. Qed. - -Lemma add_variable_augment_match: - forall ge1 new_functs new_vars ge2 id v2, - match_genvs new_functs new_vars ge1 ge2 -> - match_genvs new_functs (new_vars++((id,v2)::nil)) ge1 (add_variable ge2 (id, v2)). +Lemma add_global_augment_match: + forall new_globs ge1 ge2 idg, + match_genvs new_globs ge1 ge2 -> + match_genvs (new_globs ++ (idg :: nil)) ge1 (add_global ge2 idg). Proof. intros. destruct H. constructor; simpl. - auto. - rewrite mge_nextvar0. rewrite app_length. - simpl. rewrite inj_plus. rewrite inj_S. rewrite inj_0. unfold block; omega. (* painful! *) - intros. unfold funct_names, var_names in H. rewrite map_app in H. rewrite in_app in H. rewrite in_app in H. simpl in H. - destruct (peq id id0). subst. intuition. rewrite PTree.gso. - apply mge_symb0. intro. apply H. rewrite in_app in H0. inversion H0; intuition. intuition. - auto. - auto. - intros. rewrite ZMap.gso. auto. - rewrite mge_nextvar0. pose proof (genv_vars_range ge1 b H). intro; subst; omega. - intros. rewrite ZMap.gsspec in H. - destruct (ZIndexed.eq b (genv_nextvar ge2)). - destruct (zlt b (genv_nextvar ge1)). - exfalso. rewrite mge_nextvar0 in e. unfold block; omega. - rewrite map_app. rewrite in_app. simpl. inversion H; intuition. - pose proof (mge_rev_vars0 b tv H). - destruct (zlt b (genv_nextvar ge1)). - auto. - rewrite map_app. rewrite in_app. intuition. - -Qed. - -Lemma add_variables_augment_match: - forall vl ge1 new_functs new_vars ge2, - match_genvs new_functs new_vars ge1 ge2 -> - match_genvs new_functs (new_vars++vl) ge1 (add_variables ge2 vl). -Proof. - induction vl; simpl. + rewrite mge_next0. rewrite app_length. + simpl. rewrite inj_plus. change (Z_of_nat 1) with 1. unfold block; omega. + intros. rewrite map_app in H. rewrite in_app in H. simpl in H. + destruct (peq id idg#1). subst. intuition. rewrite PTree.gso. + apply mge_symb0. intuition. auto. + intros. destruct idg as [id1 [f1|v1]]; simpl; eauto. + rewrite ZMap.gso. eauto. exploit genv_funs_range; eauto. rewrite mge_next0. unfold ZIndexed.t; omega. + intros. rewrite map_app. destruct idg as [id1 [f1|v1]]; simpl in H. + rewrite ZMap.gsspec in H. destruct (ZIndexed.eq b (genv_next ge2)). + rewrite zlt_false. rewrite in_app. simpl; right; left. congruence. + subst b. rewrite mge_next0. omega. + exploit mge_rev_funs0; eauto. destruct (zlt b (genv_next ge1)); auto. + rewrite in_app. tauto. + exploit mge_rev_funs0; eauto. destruct (zlt b (genv_next ge1)); auto. + rewrite in_app. tauto. + intros. destruct idg as [id1 [f1|v1]]; simpl; eauto. + rewrite ZMap.gso. eauto. exploit genv_vars_range; eauto. rewrite mge_next0. unfold ZIndexed.t; omega. + intros. rewrite map_app. destruct idg as [id1 [f1|v1]]; simpl in H. + exploit mge_rev_vars0; eauto. destruct (zlt b (genv_next ge1)); auto. + rewrite in_app. tauto. + rewrite ZMap.gsspec in H. destruct (ZIndexed.eq b (genv_next ge2)). + rewrite zlt_false. rewrite in_app. simpl; right; left. congruence. + subst b. rewrite mge_next0. omega. + exploit mge_rev_vars0; eauto. destruct (zlt b (genv_next ge1)); auto. + rewrite in_app. tauto. +Qed. + +Lemma add_globals_augment_match: + forall gl new_globs ge1 ge2, + match_genvs new_globs ge1 ge2 -> + match_genvs (new_globs ++ gl) ge1 (add_globals ge2 gl). +Proof. + induction gl; simpl. intros. rewrite app_nil_r. auto. - intros. replace (new_vars ++ a :: vl) with ((new_vars ++ (a::nil)) ++ vl) - by (rewrite app_ass; auto). - apply IHvl. destruct a. apply add_variable_augment_match. auto. + intros. change (a :: gl) with ((a :: nil) ++ gl). rewrite <- app_ass. + apply IHgl. apply add_global_augment_match. auto. Qed. -Variable new_functs : list (ident * B). -Variable new_vars : list (ident * globvar W). +Variable new_globs : list (ident * globdef B W). Variable new_main : ident. Variable p: program A V. Variable p': program B W. Hypothesis progmatch: - match_program match_fun match_varinfo new_functs new_vars new_main p p'. + match_program match_fun match_varinfo new_globs new_main p p'. Lemma globalenvs_match: - match_genvs new_functs new_vars (globalenv p) (globalenv p'). -Proof. - unfold globalenv. destruct progmatch. clear progmatch. - destruct H as [tfuncts [P1 P2]]. destruct H0. clear H0. destruct H as [tvars [Q1 Q2]]. - rewrite P2. rewrite Q2. clear P2 Q2. - rewrite add_variables_app. - rewrite add_functions_app. - pattern new_vars at 1. replace new_vars with (nil++new_vars) by auto. - apply add_variables_augment_match. - apply add_variables_match; auto. - pattern new_functs at 1. replace new_functs with (nil++new_functs) by auto. - apply add_functions_augment_match. - apply add_functions_match; auto. + match_genvs new_globs (globalenv p) (globalenv p'). +Proof. + unfold globalenv. destruct progmatch as [[tglob [P Q]] R]. + rewrite Q. rewrite add_globals_app. + change new_globs with (nil ++ new_globs) at 1. + apply add_globals_augment_match. + apply add_globals_match; auto. constructor; simpl; auto; intros; rewrite ZMap.gi in H; congruence. Qed. @@ -1544,10 +1430,10 @@ Proof (mge_funs globalenvs_match). Theorem find_funct_ptr_rev_match: forall (b : block) (tf : B), find_funct_ptr (globalenv p') b = Some tf -> - if zlt (genv_nextfun (globalenv p)) b then + if zlt b (genv_next (globalenv p)) then exists f, find_funct_ptr (globalenv p) b = Some f /\ match_fun f tf else - In tf (map (@snd ident B) new_functs). + In (Gfun tf) (map snd new_globs). Proof (mge_rev_funs globalenvs_match). Theorem find_funct_match: @@ -1565,13 +1451,13 @@ 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) - \/ (In tf (map (@snd ident B) new_functs)). + \/ (In (Gfun tf) (map snd new_globs)). Proof. intros. exploit find_funct_inv; eauto. intros [b EQ]. subst v. rewrite find_funct_find_funct_ptr in H. rewrite find_funct_find_funct_ptr. apply find_funct_ptr_rev_match in H. - destruct (zlt (genv_nextfun (globalenv p)) b); intuition. + destruct (zlt b (genv_next (globalenv p))); auto. Qed. Theorem find_var_info_match: @@ -1584,23 +1470,23 @@ Proof (mge_vars globalenvs_match). Theorem find_var_info_rev_match: forall (b : block) (tv : globvar W), find_var_info (globalenv p') b = Some tv -> - if zlt b (genv_nextvar (globalenv p)) then + if zlt b (genv_next (globalenv p)) then exists v, find_var_info (globalenv p) b = Some v /\ match_globvar v tv else - In tv (map (@snd ident (globvar W)) new_vars). + In (Gvar tv) (map snd new_globs). Proof (mge_rev_vars globalenvs_match). Theorem find_symbol_match: forall (s : ident), - ~In s (funct_names new_functs ++ var_names new_vars) -> + ~In s (map fst new_globs) -> find_symbol (globalenv p') s = find_symbol (globalenv p) s. Proof. intros. destruct globalenvs_match. unfold find_symbol. auto. Qed. Hypothesis new_ids_fresh : - (forall s', find_symbol (globalenv p) s' <> None -> - ~In s' (funct_names new_functs ++ var_names new_vars)). + forall s', find_symbol (globalenv p) s' <> None -> + ~In s' (map fst new_globs). Lemma store_init_data_list_match: forall idl m b ofs m', @@ -1611,46 +1497,43 @@ Proof. auto. assert (forall m', store_init_data (globalenv p) m b ofs a = Some m' -> store_init_data (globalenv p') m b ofs a = Some m'). - destruct a; simpl; auto. rewrite find_symbol_match. auto. - inversion H. case_eq (find_symbol (globalenv p) i). - intros. apply new_ids_fresh. intro. rewrite H0 in H2; inversion H2. - intro. rewrite H0 in H1. inversion H1. + destruct a; simpl; auto. rewrite find_symbol_match. auto. + simpl in H. destruct (find_symbol (globalenv p) i) as [b'|]_eqn; try discriminate. + apply new_ids_fresh. congruence. case_eq (store_init_data (globalenv p) m b ofs a); intros. rewrite H1 in H. pose proof (H0 _ H1). rewrite H2. auto. rewrite H1 in H. inversion H. Qed. -Lemma alloc_variables_match: - forall vl1 vl2, list_forall2 (match_var_entry match_varinfo) vl1 vl2 -> +Lemma alloc_globals_match: + forall gl1 gl2, list_forall2 (match_globdef match_fun match_varinfo) gl1 gl2 -> forall m m', - alloc_variables (globalenv p) m vl1 = Some m' -> - alloc_variables (globalenv p') m vl2 = Some m'. + alloc_globals (globalenv p) m gl1 = Some m' -> + alloc_globals (globalenv p') m gl2 = Some m'. Proof. - induction 1; intros until m'; simpl. + induction 1; simpl; intros. auto. - inv H. - unfold alloc_variable; simpl. - destruct (Mem.alloc m 0 (init_data_list_size init)). - destruct (store_zeros m0 b (init_data_list_size init)); auto. - case_eq (store_init_data_list (globalenv p) m1 b 0 init); intros m2 P. - rewrite (store_init_data_list_match _ _ _ _ P). - change (perm_globvar (mkglobvar info2 init ro vo)) - with (perm_globvar (mkglobvar info1 init ro vo)). - destruct (Mem.drop_perm m2 b 0 (init_data_list_size init) - (perm_globvar (mkglobvar info1 init ro vo))); auto. - inversion P. + destruct (alloc_global (globalenv p) m a1) as [m1|]_eqn; try discriminate. + assert (alloc_global (globalenv p') m b1 = Some m1). + inv H; simpl in *. + auto. + set (sz := init_data_list_size init) in *. + destruct (Mem.alloc m 0 sz) as [m2 b]_eqn. + destruct (store_zeros m2 b 0 sz) as [m3|]_eqn; try discriminate. + destruct (store_init_data_list (globalenv p) m3 b 0 init) as [m4|]_eqn; try discriminate. + erewrite store_init_data_list_match; eauto. + rewrite H2. eauto. Qed. Theorem init_mem_match: forall m, init_mem p = Some m -> - init_mem p' = alloc_variables (globalenv p') m new_vars. + init_mem p' = alloc_globals (globalenv p') m new_globs. Proof. - unfold init_mem. destruct progmatch. destruct H0. destruct H0 as [tvars [P1 P2]]. - rewrite P2. - intros. - erewrite <- alloc_variables_app; eauto. - eapply alloc_variables_match; eauto. + unfold init_mem; intros. + destruct progmatch as [[tglob [P Q]] R]. + rewrite Q. erewrite <- alloc_globals_app; eauto. + eapply alloc_globals_match; eauto. Qed. End MATCH_PROGRAMS. @@ -1661,21 +1544,20 @@ Variable A B V W: Type. Variable transf_fun: A -> res B. Variable transf_var: V -> res W. -Variable new_functs : list (ident * B). -Variable new_vars : list (ident * globvar W). +Variable new_globs : list (ident * globdef B W). Variable new_main : ident. Variable p: program A V. Variable p': program B W. Hypothesis transf_OK: - transform_partial_augment_program transf_fun transf_var new_functs new_vars new_main p = OK p'. + transform_partial_augment_program transf_fun transf_var new_globs new_main p = OK p'. Remark prog_match: match_program (fun fd tfd => transf_fun fd = OK tfd) (fun info tinfo => transf_var info = OK tinfo) - new_functs new_vars new_main + new_globs new_main p p'. Proof. apply transform_partial_augment_program_match; auto. @@ -1692,51 +1574,39 @@ Proof. intros [tf [X Y]]. exists tf; auto. Qed. - - -(* This may not yet be in the ideal form for easy use .*) Theorem find_new_funct_ptr_exists: - list_norepet (prog_funct_names p ++ funct_names new_functs) -> - list_disjoint (prog_funct_names p ++ funct_names new_functs) (prog_var_names p ++ var_names new_vars) -> - forall id f, In (id, f) new_functs -> + list_norepet (List.map fst new_globs) -> + forall id f, In (id, Gfun f) new_globs -> exists b, find_symbol (globalenv p') id = Some b /\ find_funct_ptr (globalenv p') b = Some f. Proof. - intros. - destruct p. - unfold transform_partial_augment_program in transf_OK. - monadInv transf_OK. rename x into prog_funct'. rename x0 into prog_vars'. simpl in *. - assert (funct_names prog_funct = funct_names prog_funct'). - clear - EQ. generalize dependent prog_funct'. induction prog_funct; intros. - simpl in EQ. inversion EQ; subst; auto. - simpl in EQ. destruct a. destruct (transf_fun a); try discriminate. monadInv EQ. - simpl; f_equal; auto. - assert (var_names prog_vars = var_names prog_vars'). - clear - EQ1. generalize dependent prog_vars'. induction prog_vars; intros. - simpl in EQ1. inversion EQ1; subst; auto. - simpl in EQ1. destruct a. destruct (transf_globvar transf_var g); try discriminate. monadInv EQ1. - simpl; f_equal; auto. - apply find_funct_ptr_exists. - unfold prog_funct_names in *; simpl in *. - rewrite funct_names_app. rewrite <- H2. auto. - unfold prog_funct_names, prog_var_names in *; simpl in *. - rewrite funct_names_app. rewrite var_names_app. rewrite <- H2. rewrite <- H3. auto. - simpl. intuition. + intros. destruct prog_match as [[tglob [P Q]] R]. + unfold globalenv. rewrite Q. rewrite add_globals_app. + eapply add_globals_norepet_ensures; eauto. +(* preserves *) + intros. unfold find_symbol, find_funct_ptr in *; simpl. + destruct H1 as [b [X Y]]. exists b; split. + rewrite PTree.gso; auto. + destruct g1 as [f1 | v1]. rewrite ZMap.gso. auto. + exploit genv_funs_range; eauto. unfold ZIndexed.t; omega. + auto. +(* ensures *) + intros. unfold find_symbol, find_funct_ptr in *; simpl. + exists (genv_next ge); split. apply PTree.gss. apply ZMap.gss. Qed. Theorem find_funct_ptr_rev_transf_augment: forall (b: block) (tf: B), find_funct_ptr (globalenv p') b = Some tf -> - if (zlt (genv_nextfun (globalenv p)) b) then + if zlt b (genv_next (globalenv p)) then (exists f, find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf) else - In tf (map (@snd ident B) new_functs). + In (Gfun tf) (map snd new_globs). Proof. intros. - exploit find_funct_ptr_rev_match;eauto. eexact prog_match; eauto. auto. + exploit find_funct_ptr_rev_match; eauto. eexact prog_match; eauto. auto. Qed. - Theorem find_funct_transf_augment: forall (v: val) (f: A), find_funct (globalenv p) v = Some f -> @@ -1744,15 +1614,14 @@ Theorem find_funct_transf_augment: find_funct (globalenv p') v = Some f' /\ transf_fun f = OK f'. Proof. intros. - exploit find_funct_match. eexact prog_match. eauto. - intros [tf [X Y]]. exists tf; auto. + exploit find_funct_match. eexact prog_match. eauto. auto. Qed. Theorem find_funct_rev_transf_augment: 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) \/ - In tf (map (@snd ident B) new_functs). + In (Gfun tf) (map snd new_globs). Proof. intros. exploit find_funct_rev_match. eexact prog_match. eauto. auto. @@ -1765,65 +1634,49 @@ Theorem find_var_info_transf_augment: find_var_info (globalenv p') b = Some v' /\ transf_globvar transf_var v = OK v'. Proof. intros. - exploit find_var_info_match. eexact prog_match. eauto. - intros [tv [X Y]]. exists tv; split; auto. inv Y. unfold transf_globvar; simpl. + exploit find_var_info_match. eexact prog_match. eauto. intros [tv [X Y]]. + exists tv; split; auto. inv Y. unfold transf_globvar; simpl. rewrite H0; simpl. auto. Qed. Theorem find_new_var_exists: - forall id gv, - list_norepet (var_names new_vars) -> - In (id, gv) new_vars -> - exists b, find_symbol (globalenv p') id = Some b /\ find_var_info (globalenv p') b = Some gv. -Proof. - intros. - assert (P: forall b vars (ge: t B W), - ~In id (var_names vars) -> - find_symbol ge id = Some b - /\ find_var_info ge b = Some gv -> - find_symbol (add_variables ge vars) id = Some b - /\ find_var_info (add_variables ge vars) b = Some gv). - induction vars; simpl; intros. auto. apply IHvars. tauto. - destruct a as [id1 gv1]; unfold add_variable, find_symbol, find_var_info; simpl in *. - destruct H2; split. rewrite PTree.gso. auto. intuition. - rewrite ZMap.gso. auto. exploit genv_vars_range; eauto. unfold ZIndexed.t; omega. - - assert (Q: forall vars (ge: t B W), - list_norepet (var_names vars) -> - In (id, gv) vars -> - exists b, find_symbol (add_variables ge vars) id = Some b - /\ find_var_info (add_variables ge vars) b = Some gv). - induction vars; simpl; intros. - contradiction. - destruct a as [id1 gv1]; simpl in *. inv H1. destruct H2. inv H1. - exists (genv_nextvar ge). apply P; auto. - unfold add_variable, find_symbol, find_var_info; simpl in *. - split. apply PTree.gss. apply ZMap.gss. - apply IHvars; auto. - - unfold transform_partial_augment_program in transf_OK. - monadInv transf_OK. rename x into prog_funct'. rename x0 into prog_vars'. simpl in *. - unfold globalenv; simpl. repeat rewrite add_variables_app. apply Q; auto. + list_norepet (List.map fst new_globs) -> + forall id gv, In (id, Gvar gv) new_globs -> + exists b, find_symbol (globalenv p') id = Some b + /\ find_var_info (globalenv p') b = Some gv. +Proof. + intros. destruct prog_match as [[tglob [P Q]] R]. + unfold globalenv. rewrite Q. rewrite add_globals_app. + eapply add_globals_norepet_ensures; eauto. +(* preserves *) + intros. unfold find_symbol, find_var_info in *; simpl. + destruct H1 as [b [X Y]]. exists b; split. + rewrite PTree.gso; auto. + destruct g1 as [f1 | v1]. auto. rewrite ZMap.gso. auto. + exploit genv_vars_range; eauto. unfold ZIndexed.t; omega. +(* ensures *) + intros. unfold find_symbol, find_var_info in *; simpl. + exists (genv_next ge); split. apply PTree.gss. apply ZMap.gss. Qed. Theorem find_var_info_rev_transf_augment: forall (b: block) (v': globvar W), find_var_info (globalenv p') b = Some v' -> - if zlt b (genv_nextvar (globalenv p)) then + if zlt b (genv_next (globalenv p)) then (exists v, find_var_info (globalenv p) b = Some v /\ transf_globvar transf_var v = OK v') else - (In v' (map (@snd ident (globvar W)) new_vars)). + (In (Gvar v') (map snd new_globs)). Proof. intros. exploit find_var_info_rev_match. eexact prog_match. eauto. - destruct (zlt b (genv_nextvar (globalenv p))); auto. + destruct (zlt b (genv_next (globalenv p))); auto. intros [v [X Y]]. exists v; split; auto. inv Y. unfold transf_globvar; simpl. rewrite H0; simpl. auto. Qed. Theorem find_symbol_transf_augment: forall (s: ident), - ~ In s (funct_names new_functs ++ var_names new_vars) -> + ~ In s (map fst new_globs) -> find_symbol (globalenv p') s = find_symbol (globalenv p) s. Proof. intros. eapply find_symbol_match. eexact prog_match. auto. @@ -1831,16 +1684,16 @@ Qed. Theorem init_mem_transf_augment: (forall s', find_symbol (globalenv p) s' <> None -> - ~ In s' (funct_names new_functs ++ var_names new_vars)) -> + ~ In s' (map fst new_globs)) -> forall m, init_mem p = Some m -> - init_mem p' = alloc_variables (globalenv p') m new_vars. + init_mem p' = alloc_globals (globalenv p') m new_globs. Proof. intros. eapply init_mem_match. eexact prog_match. auto. auto. Qed. Theorem init_mem_inject_transf_augment: (forall s', find_symbol (globalenv p) s' <> None -> - ~ In s' (funct_names new_functs ++ var_names new_vars)) -> + ~ In s' (map fst new_globs)) -> forall m, init_mem p = Some m -> forall m', init_mem p' = Some m' -> Mem.inject (Mem.flat_inj (Mem.nextblock m)) m m'. @@ -1848,10 +1701,9 @@ Proof. intros. pose proof (initmem_inject p H0). erewrite init_mem_transf_augment in H1; eauto. - eapply alloc_variables_augment; eauto. omega. + eapply alloc_globals_augment; eauto. omega. Qed. - End TRANSF_PROGRAM_AUGMENT. Section TRANSF_PROGRAM_PARTIAL2. @@ -1865,13 +1717,9 @@ Hypothesis transf_OK: transform_partial_program2 transf_fun transf_var p = OK p'. Remark transf_augment_OK: - transform_partial_augment_program transf_fun transf_var nil nil p.(prog_main) p = OK p'. + transform_partial_augment_program transf_fun transf_var nil p.(prog_main) p = OK p'. Proof. - rewrite <- transf_OK. - unfold transform_partial_augment_program, transform_partial_program2. - destruct (map_partial prefix_name transf_fun (prog_funct p)); auto. simpl. - destruct (map_partial prefix_name (transf_globvar transf_var) (prog_vars p)); simpl. - repeat rewrite app_nil_r. auto. auto. + rewrite <- transf_OK. apply symmetry. apply transform_partial_program2_augment. Qed. Theorem find_funct_ptr_transf_partial2: @@ -1880,7 +1728,7 @@ Theorem find_funct_ptr_transf_partial2: exists f', find_funct_ptr (globalenv p') b = Some f' /\ transf_fun f = OK f'. Proof. - exact (@find_funct_ptr_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK). + exact (@find_funct_ptr_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK). Qed. Theorem find_funct_ptr_rev_transf_partial2: @@ -1888,9 +1736,9 @@ Theorem find_funct_ptr_rev_transf_partial2: find_funct_ptr (globalenv p') b = Some tf -> exists f, find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf. Proof. - pose proof (@find_funct_ptr_rev_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK). + pose proof (@find_funct_ptr_rev_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK). intros. pose proof (H b tf H0). - destruct (zlt (genv_nextfun (globalenv p)) b). auto. inversion H1. + destruct (zlt b (genv_next (globalenv p))). auto. contradiction. Qed. Theorem find_funct_transf_partial2: @@ -1899,7 +1747,7 @@ Theorem find_funct_transf_partial2: exists f', find_funct (globalenv p') v = Some f' /\ transf_fun f = OK f'. Proof. - exact (@find_funct_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK). + exact (@find_funct_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK). Qed. Theorem find_funct_rev_transf_partial2: @@ -1907,9 +1755,9 @@ Theorem find_funct_rev_transf_partial2: find_funct (globalenv p') v = Some tf -> exists f, find_funct (globalenv p) v = Some f /\ transf_fun f = OK tf. Proof. - pose proof (@find_funct_rev_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK). + pose proof (@find_funct_rev_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK). intros. pose proof (H v tf H0). - destruct H1. auto. inversion H1. + destruct H1. auto. contradiction. Qed. Theorem find_var_info_transf_partial2: @@ -1918,7 +1766,7 @@ Theorem find_var_info_transf_partial2: exists v', find_var_info (globalenv p') b = Some v' /\ transf_globvar transf_var v = OK v'. Proof. - exact (@find_var_info_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK). + exact (@find_var_info_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK). Qed. Theorem find_var_info_rev_transf_partial2: @@ -1927,23 +1775,23 @@ Theorem find_var_info_rev_transf_partial2: exists v, find_var_info (globalenv p) b = Some v /\ transf_globvar transf_var v = OK v'. Proof. - pose proof (@find_var_info_rev_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK). + pose proof (@find_var_info_rev_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK). intros. pose proof (H b v' H0). - destruct (zlt b (genv_nextvar (globalenv p))). auto. inversion H1. + destruct (zlt b (genv_next (globalenv p))). auto. contradiction. Qed. Theorem find_symbol_transf_partial2: forall (s: ident), find_symbol (globalenv p') s = find_symbol (globalenv p) s. Proof. - pose proof (@find_symbol_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK). + pose proof (@find_symbol_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK). auto. Qed. Theorem init_mem_transf_partial2: forall m, init_mem p = Some m -> init_mem p' = Some m. Proof. - pose proof (@init_mem_transf_augment _ _ _ _ _ _ _ _ _ _ _ transf_augment_OK). + pose proof (@init_mem_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK). intros. simpl in H. apply H; auto. Qed. @@ -1957,24 +1805,13 @@ 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'. -Proof. - rewrite <- transf_OK. - unfold transform_partial_program2, transform_partial_program. - destruct (map_partial prefix_name transf (prog_funct p)); auto. - simpl. replace (transf_globvar (fun (x : V) => OK x)) with (fun (v: globvar V) => OK v). - rewrite map_partial_identity; auto. - apply extensionality; intros. destruct x; auto. -Qed. - 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'. Proof. - exact (@find_funct_ptr_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). + exact (@find_funct_ptr_transf_partial2 _ _ _ _ _ _ _ _ transf_OK). Qed. Theorem find_funct_ptr_rev_transf_partial: @@ -1982,7 +1819,7 @@ Theorem find_funct_ptr_rev_transf_partial: find_funct_ptr (globalenv p') b = Some tf -> exists f, find_funct_ptr (globalenv p) b = Some f /\ transf f = OK tf. Proof. - exact (@find_funct_ptr_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). + exact (@find_funct_ptr_rev_transf_partial2 _ _ _ _ _ _ _ _ transf_OK). Qed. Theorem find_funct_transf_partial: @@ -1991,7 +1828,7 @@ Theorem find_funct_transf_partial: exists f', find_funct (globalenv p') v = Some f' /\ transf f = OK f'. Proof. - exact (@find_funct_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). + exact (@find_funct_transf_partial2 _ _ _ _ _ _ _ _ transf_OK). Qed. Theorem find_funct_rev_transf_partial: @@ -1999,14 +1836,14 @@ Theorem find_funct_rev_transf_partial: find_funct (globalenv p') v = Some tf -> exists f, find_funct (globalenv p) v = Some f /\ transf f = OK tf. Proof. - exact (@find_funct_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). + exact (@find_funct_rev_transf_partial2 _ _ _ _ _ _ _ _ transf_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). + exact (@find_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf_OK). Qed. Theorem find_var_info_transf_partial: @@ -2014,10 +1851,10 @@ Theorem find_var_info_transf_partial: find_var_info (globalenv p') b = find_var_info (globalenv p) b. Proof. intros. case_eq (find_var_info (globalenv p) b); intros. - exploit find_var_info_transf_partial2. eexact transf2_OK. eauto. + exploit find_var_info_transf_partial2. eexact transf_OK. eauto. intros [v' [P Q]]. monadInv Q. rewrite P. inv EQ. destruct g; auto. case_eq (find_var_info (globalenv p') b); intros. - exploit find_var_info_rev_transf_partial2. eexact transf2_OK. eauto. + exploit find_var_info_rev_transf_partial2. eexact transf_OK. eauto. intros [v' [P Q]]. monadInv Q. inv EQ. congruence. auto. Qed. @@ -2025,7 +1862,7 @@ Qed. Theorem init_mem_transf_partial: forall m, init_mem p = Some m -> init_mem p' = Some m. Proof. - exact (@init_mem_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). + exact (@init_mem_transf_partial2 _ _ _ _ _ _ _ _ transf_OK). Qed. End TRANSF_PROGRAM_PARTIAL. @@ -2040,8 +1877,7 @@ Let tp := transform_program transf p. Remark transf_OK: transform_partial_program (fun x => OK (transf x)) p = OK tp. Proof. - unfold tp, transform_program, transform_partial_program. - rewrite map_partial_total. reflexivity. + unfold tp. apply transform_program_partial_program. Qed. Theorem find_funct_ptr_transf: diff --git a/driver/Compiler.v b/driver/Compiler.v index 6fbfacd..e6e8cc2 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -184,91 +184,6 @@ Proof. intros; unfold print. destruct (printer prog); auto. Qed. -Lemma map_partial_compose: - forall (X A B C: Type) - (ctx: X -> errmsg) - (f1: A -> res B) (f2: B -> res C) - (pa: list (X * A)) (pc: list (X * C)), - map_partial ctx (fun f => f1 f @@@ f2) pa = OK pc -> - { pb | map_partial ctx f1 pa = OK pb /\ map_partial ctx f2 pb = OK pc }. -Proof. - induction pa; simpl. - intros. inv H. econstructor; eauto. - intro pc. destruct a as [x a]. - destruct (f1 a) as [] _eqn; simpl; try congruence. - destruct (f2 b) as [] _eqn; simpl; try congruence. - destruct (map_partial ctx (fun f => f1 f @@@ f2) pa) as [] _eqn; simpl; try congruence. - intros. inv H. - destruct (IHpa l) as [pb [P Q]]; auto. - rewrite P; simpl. - econstructor; split. eauto. simpl. rewrite Heqr0. rewrite Q. auto. -Qed. - -Lemma transform_partial_program_compose: - forall (A B C V: Type) - (f1: A -> res B) (f2: B -> res C) - (pa: program A V) (pc: program C V), - transform_partial_program (fun f => f1 f @@@ f2) pa = OK pc -> - { pb | transform_partial_program f1 pa = OK pb /\ - transform_partial_program f2 pb = OK pc }. -Proof. - intros. unfold transform_partial_program in H. - destruct (map_partial prefix_name (fun f : A => f1 f @@@ f2) (prog_funct pa)) as [] _eqn; - simpl in H; inv H. - destruct (map_partial_compose _ _ _ _ _ _ _ _ _ Heqr) as [xb [P Q]]. - exists (mkprogram xb (prog_main pa) (prog_vars pa)); split. - unfold transform_partial_program. rewrite P; auto. - unfold transform_partial_program. simpl. rewrite Q; auto. -Qed. - -Lemma transform_program_partial_program: - forall (A B V: Type) (f: A -> B) (p: program A V) (tp: program B V), - transform_partial_program (fun x => OK (f x)) p = OK tp -> - transform_program f p = tp. -Proof. - intros until tp. unfold transform_partial_program. - rewrite map_partial_total. simpl. intros. inv H. auto. -Qed. - -Lemma transform_program_compose: - forall (A B C V: Type) - (f1: A -> res B) (f2: B -> C) - (pa: program A V) (pc: program C V), - transform_partial_program (fun f => f1 f @@ f2) pa = OK pc -> - { pb | transform_partial_program f1 pa = OK pb /\ - transform_program f2 pb = pc }. -Proof. - intros. - replace (fun f : A => f1 f @@ f2) - with (fun f : A => f1 f @@@ (fun x => OK (f2 x))) in H. - destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [pb [X Y]]. - exists pb; split. auto. - apply transform_program_partial_program. auto. - apply extensionality; intro. destruct(f1 x); auto. -Qed. - -Lemma transform_partial_program_identity: - forall (A V: Type) (pa pb: program A V), - transform_partial_program (@OK A) pa = OK pb -> - pa = pb. -Proof. - intros until pb. unfold transform_partial_program. - replace (@OK A) with (fun b => @OK A b). - rewrite map_partial_identity. simpl. destruct pa; simpl; congruence. - apply extensionality; auto. -Qed. - -Lemma transform_program_print_identity: - forall (A V: Type) (p: program A V) (f: A -> unit), - transform_program (print f) p = p. -Proof. - intros until f. unfold transform_program, transf_program. - destruct p; simpl; f_equal. - transitivity (map (fun x => x) prog_funct). - apply list_map_exten; intros. destruct x; simpl. rewrite print_identity. auto. - apply list_map_identity. -Qed. - Lemma compose_print_identity: forall (A: Type) (x: res A) (f: A -> unit), x @@ print f = x. @@ -290,18 +205,6 @@ Qed. These results establish the correctness of the whole compiler! *) -Ltac TransfProgInv := - match goal with - | [ H: transform_partial_program (fun f => _ @@@ _) _ = OK _ |- _ ] => - let p := fresh "p" in let X := fresh "X" in let P := fresh "P" in - destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [p [X P]]; - clear H - | [ H: transform_partial_program (fun f => _ @@ _) _ = OK _ |- _ ] => - let p := fresh "p" in let X := fresh "X" in let P := fresh "P" in - destruct (transform_program_compose _ _ _ _ _ _ _ _ H) as [p [X P]]; - clear H - end. - Theorem transf_rtl_program_correct: forall p tp, transf_rtl_program p = OK tp -> diff --git a/driver/Interp.ml b/driver/Interp.ml index fc0526a..9031042 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -87,9 +87,11 @@ let print_event p = function let name_of_fundef prog fd = let rec find_name = function | [] -> "<unknown function>" - | (id, fd') :: rem -> + | (id, Gfun fd') :: rem -> if fd = fd' then extern_atom id else find_name rem - in find_name prog.prog_funct + | (id, Gvar v) :: rem -> + find_name rem + in find_name prog.prog_defs let name_of_function prog fn = name_of_fundef prog (Internal fn) @@ -468,11 +470,13 @@ let rec explore p prog ge time ss = (* Massaging the source program *) let unvolatile prog = - let unvolatile_globvar (id, gv) = - (id, if gv.gvar_volatile - then {gv with gvar_readonly = false; gvar_volatile = false} - else gv) in - {prog with prog_vars = List.map unvolatile_globvar prog.prog_vars} + let unvolatile_globdef = function + | (id, Gvar gv) -> + (id, Gvar(if gv.gvar_volatile + then {gv with gvar_readonly = false; gvar_volatile = false} + else gv)) + | idfd -> idfd in + {prog with prog_defs = List.map unvolatile_globdef prog.prog_defs} let change_main_function p old_main old_main_ty = let old_main = Evalof(Evar(old_main, old_main_ty), old_main_ty) in @@ -483,24 +487,29 @@ let change_main_function p old_main old_main_ty = let new_main_fn = { fn_return = type_int32s; fn_params = []; fn_vars = []; fn_body = body } in let new_main_id = intern_string "___main" in - { p with - prog_main = new_main_id; - prog_funct = (new_main_id, Internal new_main_fn) :: p.prog_funct } + { prog_main = new_main_id; + prog_defs = (new_main_id, Gfun(Internal new_main_fn)) :: p.prog_defs } + +let rec find_main_function name = function + | [] -> None + | (id, Gfun fd) :: gdl -> if id = name then Some fd else find_main_function name gdl + | (id, Gvar v) :: gdl -> find_main_function name gdl let fixup_main p = - try - match type_of_fundef (List.assoc p.prog_main p.prog_funct) with - | Tfunction(Tnil, Tint(I32, Signed, _)) -> - Some p - | Tfunction(Tcons(Tint _, Tcons(Tpointer(Tpointer(Tint(I8,_,_),_),_), Tnil)), - Tint _) as ty -> - Some (change_main_function p p.prog_main ty) - | _ -> - fprintf err_formatter "ERROR: wrong type for main() function"; - None - with Not_found -> - fprintf err_formatter "ERROR: no main() function"; - None + match find_main_function p.prog_main p.prog_defs with + | None -> + fprintf err_formatter "ERROR: no main() function"; + None + | Some main_fd -> + match type_of_fundef main_fd with + | Tfunction(Tnil, Tint(I32, Signed, _)) -> + Some p + | Tfunction(Tcons(Tint _, Tcons(Tpointer(Tpointer(Tint(I8,_,_),_),_), Tnil)), + Tint _) as ty -> + Some (change_main_function p p.prog_main ty) + | _ -> + fprintf err_formatter "ERROR: wrong type for main() function"; + None (* Execution of a whole program *) diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index a36adb1..08bd2f5 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -767,11 +767,6 @@ let print_function oc name code = jumptables := [] end -let print_fundef oc (name, defn) = - match defn with - | Internal code -> print_function oc name code - | External ef -> () - let print_init oc = function | Init_int8 n -> fprintf oc " .byte %ld\n" (camlint_of_coqint n) @@ -802,7 +797,7 @@ let print_init_data oc name id = else List.iter (print_init oc) id -let print_var oc (name, v) = +let print_var oc name v = match v.gvar_init with | [] -> () | _ -> @@ -826,11 +821,16 @@ let print_var oc (name, v) = fprintf oc " .size %a, . - %a\n" symbol name symbol name end +let print_globdef oc (name, gdef) = + match gdef with + | Gfun(Internal code) -> print_function oc name code + | Gfun(External ef) -> () + | Gvar v -> print_var oc name v + let print_program oc p = need_masks := false; indirect_symbols := StringSet.empty; - List.iter (print_var oc) p.prog_vars; - List.iter (print_fundef oc) p.prog_funct; + List.iter (print_globdef oc) p.prog_defs; if !need_masks then begin section oc Section_const; (* not Section_literal because not 8-bytes *) print_align oc 16; diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index ac9a5da..5bfd3ee 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -881,7 +881,7 @@ let function_needs_stub name = (* Generation of whole programs *) -let print_fundef oc (name, defn) = +let print_fundef oc name defn = match defn with | Internal code -> print_function oc name code @@ -890,13 +890,12 @@ let print_fundef oc (name, defn) = | External _ -> () -let record_extfun (name, defn) = - match defn with - | Internal _ -> () - | External (EF_external _ | EF_malloc | EF_free) -> +let record_extfun (name, gd) = + match gd with + | Gfun(External (EF_external _ | EF_malloc | EF_free)) -> if function_needs_stub name then stubbed_functions := IdentSet.add name !stubbed_functions - | External _ -> () + | _ -> () let print_init oc = function | Init_int8 n -> @@ -930,7 +929,7 @@ let print_init_data oc name id = else List.iter (print_init oc) id -let print_var oc (name, v) = +let print_var oc name v = match v.gvar_init with | [] -> () | _ -> @@ -963,9 +962,13 @@ let print_var oc (name, v) = (1 lsl align) end +let print_globdef oc (name, gdef) = + match gdef with + | Gfun f -> print_fundef oc name f + | Gvar v -> print_var oc name v + let print_program oc p = stubbed_functions := IdentSet.empty; - List.iter record_extfun p.prog_funct; - List.iter (print_var oc) p.prog_vars; - List.iter (print_fundef oc) p.prog_funct + List.iter record_extfun p.prog_defs; + List.iter (print_globdef oc) p.prog_defs diff --git a/test/regression/Makefile b/test/regression/Makefile index a649f88..e8fb236 100644 --- a/test/regression/Makefile +++ b/test/regression/Makefile @@ -9,7 +9,7 @@ LIBS=$(LIBMATH) TESTS=attribs1 bitfields1 bitfields2 bitfields3 bitfields4 \ bitfields5 bitfields6 bitfields7 \ - expr1 expr6 initializers volatile1 volatile2 volatile3 \ + expr1 expr6 funptr2 initializers volatile1 volatile2 volatile3 \ funct3 expr5 struct7 struct8 struct11 casts1 casts2 char1 \ sizeof1 sizeof2 packedstruct1 packedstruct2 \ instrsel bool compar diff --git a/test/regression/Results/funptr2 b/test/regression/Results/funptr2 new file mode 100644 index 0000000..f364c59 --- /dev/null +++ b/test/regression/Results/funptr2 @@ -0,0 +1,3 @@ +f == f is 1 +f == g is 0 +f + 1 == f is 0 diff --git a/test/regression/Results/initializers b/test/regression/Results/initializers index d3fc91a..7474148 100644 --- a/test/regression/Results/initializers +++ b/test/regression/Results/initializers @@ -1,3 +1,4 @@ +x0 = 0 x1 = 'x' x2 = 12345 x3 = 3.14159 diff --git a/test/regression/funptr2.c b/test/regression/funptr2.c new file mode 100644 index 0000000..5c31dd2 --- /dev/null +++ b/test/regression/funptr2.c @@ -0,0 +1,14 @@ +/* Comparisons of pointers to functions */ + +#include <stdio.h> + +int f(void) { return 0; } +int g(void) { return 1; } + +int main(void) { + printf ("f == f is %d\n", &f == &f); + printf ("f == g is %d\n", &f == &g); + /* The following is undefined behavior */ + printf ("f + 1 == f is %d\n", ((char *) &f) + 1 == (char *) &f); + return 0; +} diff --git a/test/regression/initializers.c b/test/regression/initializers.c index f831c67..d0a35f3 100644 --- a/test/regression/initializers.c +++ b/test/regression/initializers.c @@ -1,5 +1,7 @@ #include <stdio.h> +int x0; + char x1 = 'x'; int x2 = 12345; @@ -67,6 +69,7 @@ int main() { int i; + printf("x0 = %d\n", x0); printf("x1 = '%c'\n", x1); printf("x2 = %d\n", x2); printf("x3 = %.5f\n", x3); |