From ce4951549999f403446415c135ad1403a16a15c3 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 12 Nov 2012 13:42:22 +0000 Subject: Globalenvs: allocate one-byte block with permissions Nonempty for each function definition, so that comparisons between function pointers are correctly defined. AST, Globalenvs, and many other files: represent programs as a list of (function or variable) definitions instead of two lists, one for functions and the other for variables. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2067 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/CMparser.mly | 37 +++++++++++++++-------------------- backend/CMtypecheck.ml | 11 ++++++----- backend/Constprop.v | 20 +++++++++++-------- backend/Constpropproof.v | 29 +++++++++++++++------------ backend/Inlining.v | 18 +++++++---------- backend/Inliningproof.v | 12 +++++++----- backend/Inliningspec.v | 51 +++++++++++++++--------------------------------- backend/LTLintyping.v | 2 +- backend/LTLtyping.v | 2 +- backend/Lineartyping.v | 2 +- backend/Machtyping.v | 2 +- backend/PrintCminor.ml | 23 ++++++++++------------ backend/PrintLTLin.ml | 10 +++++----- backend/PrintMach.ml | 10 +++++----- backend/PrintRTL.ml | 10 +++++----- backend/RTLtyping.v | 2 +- backend/Stackingproof.v | 9 +++++---- backend/Unusedglob.ml | 25 ++++++++++++------------ 18 files changed, 127 insertions(+), 148 deletions(-) (limited to 'backend') 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 "@[extern @[\"%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 "@["; - List.iter (print_var p) prog.prog_vars; - fprintf p "@]@["; - List.iter (print_fundef p) prog.prog_funct; + fprintf p "@["; + 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 *) -- cgit v1.2.3