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. --- powerpc/Unusedglob1.ml | 67 -------------------------------------------------- 1 file changed, 67 deletions(-) delete mode 100644 powerpc/Unusedglob1.ml (limited to 'powerpc') diff --git a/powerpc/Unusedglob1.ml b/powerpc/Unusedglob1.ml deleted file mode 100644 index 2d3efe39..00000000 --- a/powerpc/Unusedglob1.ml +++ /dev/null @@ -1,67 +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 a PowerPC Asm instruction *) - -open Datatypes -open AST -open Asm - -let referenced_constant = function - | Cint n -> [] - | Csymbol_low(s, ofs) -> [s] - | Csymbol_high(s, ofs) -> [s] - | Csymbol_sda(s, ofs) -> [s] - | Csymbol_rel_low(s, ofs) -> [s] - | Csymbol_rel_high(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 - | Pbl(s, _) -> [s] - | Pbs(s, _) -> [s] - | Paddi(_, _, c) - | Paddic(_, _, c) - | Paddis(_, _, c) - | Pandi_(_, _, c) - | Pandis_(_, _, c) - | Pcmplwi(_, c) - | Pcmpwi(_, c) - | Plbz(_, c, _) - | Plfd(_, c, _) - | Plfd_a(_, c, _) - | Plfs(_, c, _) - | Plha(_, c, _) - | Plhz(_, c, _) - | Plwz(_, c, _) - | Plwz_a(_, c, _) - | Pmulli(_, _, c) - | Pori(_, _, c) - | Poris(_, _, c) - | Pstb(_, c, _) - | Pstfd(_, c, _) - | Pstfd_a(_, c, _) - | Pstfs(_, c, _) - | Psth(_, c, _) - | Pstw(_, c, _) - | Pstw_a(_, c, _) - | Psubfic(_, _, c) - | Pxori(_, _, c) - | Pxoris(_, _, c) -> referenced_constant c - | Pbuiltin(ef, _, _) -> referenced_builtin ef - | _ -> [] - -let code_of_function f = f.fn_code -- cgit From 0b78a7b471eecd1ab983bbc48dfe8b39a0985d47 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 5 Nov 2014 15:32:52 +0100 Subject: Update PowerPC port. --- powerpc/Asmgenproof.v | 16 +++++++++++---- powerpc/Op.v | 56 +++++++++++++++++++++++++++++++++++---------------- 2 files changed, 51 insertions(+), 21 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 9adf44dc..c7439c3d 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -49,6 +49,14 @@ Proof. exact TRANSF. Qed. +Lemma public_preserved: + forall id, Genv.public_symbol tge id = Genv.public_symbol ge id. +Proof. + intros. unfold ge, tge. + apply Genv.public_symbol_transf_partial with transf_fundef. + exact TRANSF. +Qed. + Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof. @@ -755,7 +763,7 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen. eapply exec_step_builtin. eauto. eauto. eapply find_instr_tail; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eauto. econstructor; eauto. Simpl. rewrite set_pregs_other_2. rewrite undef_regs_other_2. rewrite <- H0. simpl. econstructor; eauto. @@ -777,7 +785,7 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen. eapply exec_step_annot. eauto. eauto. eapply find_instr_tail; eauto. eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_states_intro with (ep := false); eauto with coqlib. unfold nextinstr. rewrite Pregmap.gss. rewrite <- H1; simpl. econstructor; eauto. @@ -960,7 +968,7 @@ Local Transparent destroyed_by_jumptable. left; econstructor; split. apply plus_one. eapply exec_step_external; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. unfold loc_external_result. apply agree_set_other; auto. apply agree_set_mregs; auto. @@ -1005,7 +1013,7 @@ Theorem transf_program_correct: forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog). Proof. eapply forward_simulation_star with (measure := measure). - eexact symbols_preserved. + eexact public_preserved. eexact transf_initial_states. eexact transf_final_states. exact step_simulation. diff --git a/powerpc/Op.v b/powerpc/Op.v index dbec2755..3d5b1fc5 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -581,6 +581,22 @@ Proof. destruct c; simpl; auto; discriminate. Qed. +(** Global variables mentioned in an operation or addressing mode *) + +Definition globals_operation (op: operation) : list ident := + match op with + | Oaddrsymbol s ofs => s :: nil + | Oaddsymbol s ofs => s :: nil + | _ => nil + end. + +Definition globals_addressing (addr: addressing) : list ident := + match addr with + | Aglobal s n => s :: nil + | Abased s n => s :: nil + | _ => nil + end. + (** * Invariance and compatibility properties. *) (** [eval_operation] and [eval_addressing] depend on a global environment @@ -622,14 +638,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. @@ -704,18 +717,22 @@ Ltac TrivialExists := 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. - inv H; simpl; econstructor; eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + intros until v1; intros GL; intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists. + apply GL; simpl; auto. + apply Values.val_add_inject; auto. inv H4; simpl; auto. inv H4; simpl; auto. apply Values.val_add_inject; auto. apply Values.val_add_inject; auto. - apply Values.val_add_inject; auto. + apply Values.val_add_inject; auto. apply GL; simpl; auto. inv H4; inv H2; simpl; auto. econstructor; eauto. rewrite Int.sub_add_l. auto. destruct (eq_block b1 b0); auto. subst. rewrite H1 in H0. inv H0. rewrite dec_eq_true. @@ -777,13 +794,18 @@ Qed. 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; auto using Values.val_add_inject. + apply H; simpl; auto. + apply Values.val_add_inject; auto. apply H; simpl; auto. Qed. End EVAL_COMPAT. @@ -864,11 +886,11 @@ 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; auto. apply valid_different_pointers_extends; auto. + intros. rewrite <- val_inject_lessdef; auto. rewrite <- val_inject_lessdef; auto. eauto. auto. destruct H2 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto. @@ -939,7 +961,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: @@ -954,11 +976,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. -- cgit From c1daedb244d1f7586c12749642b0d78ae910e60a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 17 Dec 2014 11:33:23 +0100 Subject: Clean up support for common symbols. Uninitialized "const" symbols can be common. --- powerpc/PrintAsm.ml | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) (limited to 'powerpc') diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 587dfccf..760ed275 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -105,13 +105,14 @@ module Linux_System = let name_of_section = function | Section_text -> ".text" - | Section_data i -> if i then ".data" else "COMM" + | Section_data i -> + if i then ".data" else "COMM" | Section_small_data i -> - if i - then ".section .sdata,\"aw\",@progbits" - else ".section .sbss,\"aw\",@progbits" - | Section_const -> ".rodata" - | Section_small_const -> ".section .sdata2,\"a\",@progbits" + if i then ".section .sdata,\"aw\",@progbits" else "COMM" + | Section_const i -> + if i then ".rodata" else "COMM" + | Section_small_const i -> + if i then ".section .sdata2,\"a\",@progbits" else "COMM" | Section_string -> ".rodata" | Section_literal -> ".section .rodata.cst8,\"aM\",@progbits,8" | Section_jumptable -> ".text" @@ -197,10 +198,10 @@ module Diab_System = let name_of_section = function | Section_text -> ".text" - | Section_data i -> if i then ".data" else ".bss" + | Section_data i -> if i then ".data" else "COMM" | Section_small_data i -> if i then ".sdata" else ".sbss" - | Section_const -> ".text" - | Section_small_const -> ".sdata2" + | Section_const _ -> ".text" + | Section_small_const _ -> ".sdata2" | Section_string -> ".text" | Section_literal -> ".text" | Section_jumptable -> ".text" -- cgit