From 10941819e09e2f9090e7fe39301a0b9026a0eba0 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 5 Nov 2014 14:36:14 +0100 Subject: Verification of the Unusedglob pass (removal of unreferenced static global definitions). Assorted changes to ia32/Op.v. PowerPC and ARM need updating. --- ia32/Op.v | 65 ++++++++++++++++++++++++++++++++++++----------------- ia32/Unusedglob1.ml | 46 ------------------------------------- 2 files changed, 44 insertions(+), 67 deletions(-) delete mode 100644 ia32/Unusedglob1.ml (limited to 'ia32') diff --git a/ia32/Op.v b/ia32/Op.v index 14e4cbb1..846d094f 100644 --- a/ia32/Op.v +++ b/ia32/Op.v @@ -659,6 +659,23 @@ Proof. destruct c; simpl; try congruence. reflexivity. Qed. +(** Global variables mentioned in an operation or addressing mode *) + +Definition globals_addressing (addr: addressing) : list ident := + match addr with + | Aglobal s n => s :: nil + | Abased s n => s :: nil + | Abasedscaled sc s n => s :: nil + | _ => nil + end. + +Definition globals_operation (op: operation) : list ident := + match op with + | Oindirectsymbol s => s :: nil + | Olea addr => globals_addressing addr + | _ => nil + end. + (** * Invariance and compatibility properties. *) (** [eval_operation] and [eval_addressing] depend on a global environment @@ -699,14 +716,11 @@ End GENV_TRANSF. Section EVAL_COMPAT. -Variable F V: Type. -Variable genv: Genv.t F V. +Variable F1 F2 V1 V2: Type. +Variable ge1: Genv.t F1 V1. +Variable ge2: Genv.t F2 V2. Variable f: meminj. -Hypothesis symbol_address_inj: - forall id ofs, - val_inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs). - Variable m1: mem. Variable m2: mem. @@ -781,29 +795,37 @@ Ltac TrivialExists := Lemma eval_addressing_inj: forall addr sp1 vl1 sp2 vl2 v1, + (forall id ofs, + In id (globals_addressing addr) -> + val_inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> val_inject f sp1 sp2 -> val_list_inject f vl1 vl2 -> - eval_addressing genv sp1 addr vl1 = Some v1 -> - exists v2, eval_addressing genv sp2 addr vl2 = Some v2 /\ val_inject f v1 v2. + eval_addressing ge1 sp1 addr vl1 = Some v1 -> + exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ val_inject f v1 v2. Proof. - intros. destruct addr; simpl in H1; simpl; FuncInv; InvInject; TrivialExists. + intros. destruct addr; simpl in H2; simpl; FuncInv; InvInject; TrivialExists. apply Values.val_add_inject; auto. apply Values.val_add_inject; auto. apply Values.val_add_inject; auto. - apply Values.val_add_inject; auto. inv H4; simpl; auto. - apply Values.val_add_inject; auto. apply Values.val_add_inject; auto. inv H2; simpl; auto. - apply Values.val_add_inject; auto. - apply Values.val_add_inject; auto. inv H4; simpl; auto. + apply Values.val_add_inject; auto. inv H5; simpl; auto. + apply Values.val_add_inject; auto. apply Values.val_add_inject; auto. inv H3; simpl; auto. + apply H; simpl; auto. + apply Values.val_add_inject; auto. apply H; simpl; auto. + apply Values.val_add_inject; auto. apply H; simpl; auto. inv H5; simpl; auto. apply Values.val_add_inject; auto. Qed. Lemma eval_operation_inj: forall op sp1 vl1 sp2 vl2 v1, + (forall id ofs, + In id (globals_operation op) -> + val_inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> val_inject f sp1 sp2 -> val_list_inject f vl1 vl2 -> - eval_operation genv sp1 op vl1 m1 = Some v1 -> - exists v2, eval_operation genv sp2 op vl2 m2 = Some v2 /\ val_inject f v1 v2. + eval_operation ge1 sp1 op vl1 m1 = Some v1 -> + exists v2, eval_operation ge2 sp2 op vl2 m2 = Some v2 /\ val_inject f v1 v2. Proof. - intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists. + intros until v1; intros GL; intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists. + apply GL; simpl; auto. inv H4; simpl; auto. inv H4; simpl; auto. inv H4; simpl; auto. @@ -951,13 +973,14 @@ Proof. eval_operation genv sp op vl2 m2 = Some v2 /\ val_inject (fun b => Some(b, 0)) v1 v2). eapply eval_operation_inj with (m1 := m1) (sp1 := sp). - intros. rewrite <- val_inject_lessdef; auto. apply valid_pointer_extends; auto. apply weak_valid_pointer_extends; auto. apply weak_valid_pointer_no_overflow_extends. apply valid_different_pointers_extends; auto. - rewrite <- val_inject_lessdef; auto. - eauto. auto. + intros. apply val_inject_lessdef. auto. + apply val_inject_lessdef; auto. + eauto. + auto. destruct H2 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto. Qed. @@ -1026,7 +1049,7 @@ Proof. intros. rewrite eval_shift_stack_addressing. simpl. eapply eval_addressing_inj with (sp1 := Vptr sp1 Int.zero); eauto. - exact symbol_address_inject. + intros. apply symbol_address_inject. Qed. Lemma eval_operation_inject: @@ -1041,11 +1064,11 @@ Proof. intros. rewrite eval_shift_stack_operation. simpl. eapply eval_operation_inj with (sp1 := Vptr sp1 Int.zero) (m1 := m1); eauto. - exact symbol_address_inject. intros; eapply Mem.valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto. intros; eapply Mem.different_pointers_inject; eauto. + intros. apply symbol_address_inject. Qed. End EVAL_INJECT. diff --git a/ia32/Unusedglob1.ml b/ia32/Unusedglob1.ml deleted file mode 100644 index eb0298bb..00000000 --- a/ia32/Unusedglob1.ml +++ /dev/null @@ -1,46 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(* Identifiers referenced from an IA32 Asm instruction *) - -open Datatypes -open AST -open Asm - -let referenced_addr (Addrmode(base, ofs, const)) = - match const with - | Coq_inl n -> [] - | Coq_inr(s, ofs) -> [s] - -let referenced_builtin ef = - match ef with - | EF_vload_global(chunk, id, ofs) -> [id] - | EF_vstore_global(chunk, id, ofs) -> [id] - | _ -> [] - -let referenced_instr = function - | Pmov_rm (_, a) | Pmov_mr (a, _) - | Pmov_rm_a (_, a) | Pmov_mr_a (a, _) - | Pmovsd_fm (_, a) | Pmovsd_mf(a, _) - | Pmovss_fm (_, a) | Pmovss_mf(a, _) - | Pfldl_m a | Pflds_m a | Pfstpl_m a | Pfstps_m a - | Pmovb_mr (a, _) | Pmovw_mr (a, _) - | Pmovzb_rm (_, a) | Pmovsb_rm (_, a) - | Pmovzw_rm (_, a) | Pmovsw_rm (_, a) - | Plea (_, a) -> referenced_addr a - | Pjmp_s(s, _) -> [s] - | Pcall_s(s, _) -> [s] - | Pbuiltin(ef, args, res) -> referenced_builtin ef - | _ -> [] - -let code_of_function f = f.fn_code - -- cgit