From bac2a0854ea51217690bc6f225da62053ed7ac06 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 11 Mar 2016 08:48:31 +0100 Subject: Removed unused parameter from is_small/rel_data. The ofs parameter is no longer used. Adopted the proofs and ml code using it. Bug 18394 --- cfrontend/C2C.ml | 6 +++--- powerpc/Asm.v | 6 +++--- powerpc/Asmexpand.ml | 8 ++++---- powerpc/Asmgen.v | 17 ++++++++--------- powerpc/Asmgenproof.v | 8 ++++---- powerpc/Asmgenproof1.v | 9 ++++----- 6 files changed, 26 insertions(+), 28 deletions(-) diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index c3e07995..d29bb295 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -76,13 +76,13 @@ let atom_sections a = with Not_found -> [] -let atom_is_small_data a _ = +let atom_is_small_data a = try (Hashtbl.find decl_atom a).a_access = Sections.Access_near with Not_found -> false -let atom_is_rel_data a _ = +let atom_is_rel_data a = try (Hashtbl.find decl_atom a).a_access = Sections.Access_far with Not_found -> @@ -478,7 +478,7 @@ let checkFunctionType env tres targs = l end end - + let rec convertTyp env t = match t with | C.TVoid _ -> Tvoid diff --git a/powerpc/Asm.v b/powerpc/Asm.v index a9b60fbd..81f81040 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -477,15 +477,15 @@ Axiom low_high_half: register pointing to the base of the small data area containing symbol [symb]. We leave this transformation up to the linker. *) -Parameter symbol_is_small_data: ident -> int -> bool. +Parameter symbol_is_small_data: ident -> bool. Parameter small_data_area_offset: genv -> ident -> int -> val. Axiom small_data_area_addressing: forall id ofs, - symbol_is_small_data id ofs = true -> + symbol_is_small_data id = true -> small_data_area_offset ge id ofs = Genv.symbol_address ge id ofs. -Parameter symbol_is_rel_data: ident -> int -> bool. +Parameter symbol_is_rel_data: ident -> bool. (** Armed with the [low_half] and [high_half] functions, we can define the evaluation of a symbolic constant. diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index a6795030..917d4466 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -211,9 +211,9 @@ let expand_builtin_vload chunk args res = expand_builtin_vload_common chunk GPR11 (Cint _0) res end | [BA_addrglobal(id, ofs)] -> - if symbol_is_small_data id ofs then + if symbol_is_small_data id then expand_builtin_vload_common chunk GPR0 (Csymbol_sda(id, ofs)) res - else if symbol_is_rel_data id ofs then begin + else if symbol_is_rel_data id then begin emit (Paddis(GPR11, GPR0, Csymbol_rel_high(id, ofs))); expand_builtin_vload_common chunk GPR11 (Csymbol_rel_low(id, ofs)) res end else begin @@ -268,9 +268,9 @@ let expand_builtin_vstore chunk args = expand_builtin_vstore_common chunk tmp (Cint _0) src end | [BA_addrglobal(id, ofs); src] -> - if symbol_is_small_data id ofs then + if symbol_is_small_data id then expand_builtin_vstore_common chunk GPR0 (Csymbol_sda(id, ofs)) src - else if symbol_is_rel_data id ofs then begin + else if symbol_is_rel_data id then begin let tmp = temp_for_vstore src in emit (Paddis(tmp, GPR0, Csymbol_rel_high(id, ofs))); expand_builtin_vstore_common chunk tmp (Csymbol_rel_low(id, ofs)) src diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 4ad5e2f9..f961ad73 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -331,9 +331,9 @@ Definition transl_op do r <- freg_of res; OK (Plfis r f :: k) | Oaddrsymbol s ofs, nil => do r <- ireg_of res; - OK (if symbol_is_small_data s ofs then + OK (if symbol_is_small_data s then Paddi r GPR0 (Csymbol_sda s ofs) :: k - else if symbol_is_rel_data s ofs then + else if symbol_is_rel_data s then Paddis r GPR0 (Csymbol_rel_high s ofs) :: Paddi r r (Csymbol_rel_low s ofs) :: k else @@ -352,10 +352,10 @@ Definition transl_op do r1 <- ireg_of a1; do r <- ireg_of res; OK (addimm r r1 n k) | Oaddsymbol s ofs, a1 :: nil => do r1 <- ireg_of a1; do r <- ireg_of res; - OK (if symbol_is_small_data s ofs then + OK (if symbol_is_small_data s then Paddi GPR0 GPR0 (Csymbol_sda s ofs) :: Padd r r1 GPR0 :: k - else if symbol_is_rel_data s ofs then + else if symbol_is_rel_data s then Pmr GPR0 r1 :: Paddis r GPR0 (Csymbol_rel_high s ofs) :: Paddi r r (Csymbol_rel_low s ofs) :: @@ -536,9 +536,9 @@ Definition transl_memory_access do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (mk2 r1 r2 :: k) | Aglobal symb ofs, nil => - OK (if symbol_is_small_data symb ofs then + OK (if symbol_is_small_data symb then mk1 (Csymbol_sda symb ofs) GPR0 :: k - else if symbol_is_rel_data symb ofs then + else if symbol_is_rel_data symb then Paddis temp GPR0 (Csymbol_rel_high symb ofs) :: Paddi temp temp (Csymbol_rel_low symb ofs) :: mk1 (Cint Int.zero) temp :: k @@ -547,10 +547,10 @@ Definition transl_memory_access mk1 (Csymbol_low symb ofs) temp :: k) | Abased symb ofs, a1 :: nil => do r1 <- ireg_of a1; - OK (if symbol_is_small_data symb ofs then + OK (if symbol_is_small_data symb then Paddi GPR0 GPR0 (Csymbol_sda symb ofs) :: mk2 r1 GPR0 :: k - else if symbol_is_rel_data symb ofs then + else if symbol_is_rel_data symb then Pmr GPR0 r1 :: Paddis temp GPR0 (Csymbol_rel_high symb ofs) :: Paddi temp temp (Csymbol_rel_low symb ofs) :: @@ -736,4 +736,3 @@ Definition transf_fundef (f: Mach.fundef) : res Asm.fundef := Definition transf_program (p: Mach.program) : res Asm.program := transform_partial_program transf_fundef p. - diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 4e59b297..47b69d6a 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -254,8 +254,8 @@ Proof. Opaque Int.eq. unfold transl_op; intros; destruct op; TailNoLabel. destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel. - destruct (symbol_is_small_data i i0). TailNoLabel. destruct (symbol_is_rel_data i i0); TailNoLabel. - destruct (symbol_is_small_data i i0). TailNoLabel. destruct (symbol_is_rel_data i i0); TailNoLabel. + destruct (symbol_is_small_data i). TailNoLabel. destruct (symbol_is_rel_data i); TailNoLabel. + destruct (symbol_is_small_data i). TailNoLabel. destruct (symbol_is_rel_data i); TailNoLabel. destruct (Int.eq (high_s i) Int.zero); TailNoLabel; eapply tail_nolabel_trans; TailNoLabel. destruct (Int.eq (high_s i) Int.zero); TailNoLabel; eapply tail_nolabel_trans; TailNoLabel. eapply transl_cond_op_label; eauto. @@ -271,8 +271,8 @@ Remark transl_memory_access_label: Proof. unfold transl_memory_access; intros; destruct addr; TailNoLabel. destruct (Int.eq (high_s i) Int.zero); TailNoLabel. - destruct (symbol_is_small_data i i0). TailNoLabel. destruct (symbol_is_rel_data i i0); TailNoLabel. - destruct (symbol_is_small_data i i0). TailNoLabel. destruct (symbol_is_rel_data i i0); TailNoLabel. + destruct (symbol_is_small_data i). TailNoLabel. destruct (symbol_is_rel_data i); TailNoLabel. + destruct (symbol_is_small_data i). TailNoLabel. destruct (symbol_is_rel_data i); TailNoLabel. destruct (Int.eq (high_s i) Int.zero); TailNoLabel. Qed. diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index aa2645f3..70698736 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -844,7 +844,7 @@ Opaque Int.eq. exists rs'. auto with asmgen. (* Oaddrsymbol *) set (v' := Genv.symbol_address ge i i0). - destruct (symbol_is_small_data i i0) eqn:SD; [ | destruct (symbol_is_rel_data i i0) ]. + destruct (symbol_is_small_data i) eqn:SD; [ | destruct (symbol_is_rel_data i) ]. (* small data *) Opaque Val.add. econstructor; split. apply exec_straight_one; simpl; reflexivity. @@ -867,7 +867,7 @@ Opaque Val.add. destruct (addimm_correct x0 x i k rs m) as [rs' [A [B C]]]; eauto with asmgen. exists rs'; auto with asmgen. (* Oaddsymbol *) - destruct (symbol_is_small_data i i0) eqn:SD; [ | destruct (symbol_is_rel_data i i0) ]. + destruct (symbol_is_small_data i) eqn:SD; [ | destruct (symbol_is_rel_data i) ]. (* small data *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. split. Simpl. rewrite (Val.add_commut (rs x)). f_equal. @@ -1020,7 +1020,7 @@ Transparent Val.add. (* Aindexed2 *) apply MK2; auto. (* Aglobal *) - destruct (symbol_is_small_data i i0) eqn:SISD; [ | destruct (symbol_is_rel_data i i0) ]; inv TR. + destruct (symbol_is_small_data i) eqn:SISD; [ | destruct (symbol_is_rel_data i) ]; inv TR. (* Aglobal from small data *) apply MK1. unfold const_low. rewrite small_data_area_addressing by auto. apply add_zero_symbol_address. @@ -1048,7 +1048,7 @@ Transparent Val.add. exists rs'; split. apply exec_straight_step with rs1 m; auto. eexact EX'. auto. (* Abased *) - destruct (symbol_is_small_data i i0) eqn:SISD; [ | destruct (symbol_is_rel_data i i0) ]. + destruct (symbol_is_small_data i) eqn:SISD; [ | destruct (symbol_is_rel_data i) ]. (* Abased from small data *) set (rs1 := nextinstr (rs#GPR0 <- (Genv.symbol_address ge i i0))). exploit (MK2 x GPR0 rs1 k). @@ -1232,4 +1232,3 @@ Local Transparent destroyed_by_store. Qed. End CONSTRUCTORS. - -- cgit