From 71a8a9586078c0132aa326a8c7968d38fe25a78d Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 18 Aug 2014 12:34:43 +0000 Subject: powerpc/Asm: simplify the modeling of Csymbol_low and Csymbol_high. powerpc/Asmgen*: simplify the code generated for far-data relative accesses, so that the only occurrences of Csymbol_rel_{low,high} are in the pattern Paddis(r, GPR0, Csymbol_rel_high...); Paddi(r, r, Csymbol_rel_low...) checklink/Check.ml: check the pattern above. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2569 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- checklink/Check.ml | 28 +++++++--- powerpc/Asm.v | 26 +++------ powerpc/Asmexpand.ml | 32 ++++++++--- powerpc/Asmgen.v | 36 +++++++------ powerpc/Asmgenproof.v | 10 ++-- powerpc/Asmgenproof1.v | 127 ++++++++++++++++++++------------------------ powerpc/extractionMachdep.v | 4 +- 7 files changed, 139 insertions(+), 124 deletions(-) diff --git a/checklink/Check.ml b/checklink/Check.ml index 7eb3ea3..cc53f4e 100644 --- a/checklink/Check.ml +++ b/checklink/Check.ml @@ -415,13 +415,12 @@ let match_csts (cc: constant) (ec: int32): checker = fun ffw -> end | Csymbol_sda (ident, i) -> (* sda should be handled separately in places it occurs *) - fatal "Unhandled Csymbol_sda, please report." + ERR("Incorrect reference to near-data symbol " + ^ Hashtbl.find ffw.sf.ident_to_name ident) | Csymbol_rel_low (ident, i) | Csymbol_rel_high (ident, i) -> - (* not checked yet *) - OK((ff_ef ^%= - (add_log (WARNING("Cannot check access to far-data symbol " ^ - Hashtbl.find ffw.sf.ident_to_name ident)))) - ffw) + (* should be handled separately in places it occurs *) + ERR("Incorrect reference to far-data symbol " + ^ Hashtbl.find ffw.sf.ident_to_name ident) let match_z_int32 (cz: Z.t) (ei: int32) = let cz = z_int32 cz in @@ -738,6 +737,23 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end + | Paddis(rd, r1, Csymbol_rel_high(id, ofs)) -> + begin match cs with + | Paddi(rd', r1', Csymbol_rel_low(id', ofs')) :: cs + when id' = id && ofs' = ofs -> + begin match ecode with + | ADDIS(rD, rA, simm) :: ADDI(rD', rA', simm') :: es -> + OK(fw) + >>= match_iregs rd rD + >>= match_iregs r1' rA' + >>= match_iregs rd' rD' + >>= check_sda id ofs rA + Int32.(add (shift_left (of_int simm) 16) (exts simm')) + >>= compare_code cs es (Int32.add 8l pc) + | _ -> error + end + | _ -> error + end | Paddis(rd, r1, cst) -> begin match ecode with | ADDIS(rD, rA, simm) :: es -> diff --git a/powerpc/Asm.v b/powerpc/Asm.v index ab52ca5..fc8c2d9 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -429,8 +429,8 @@ Variable ge: genv. symbolic references [symbol + offset] and splits their actual values into two 16-bit halves. *) -Parameter low_half: val -> val. -Parameter high_half: val -> val. +Parameter low_half: genv -> ident -> int -> val. +Parameter high_half: genv -> ident -> int -> val. (** The fundamental property of these operations is that, when applied to the address of a symbol, their results can be recombined by @@ -438,18 +438,8 @@ Parameter high_half: val -> val. Axiom low_high_half: forall id ofs, - Val.add (low_half (Genv.symbol_address ge id ofs)) (high_half (Genv.symbol_address ge id ofs)) - = Genv.symbol_address ge id ofs. - -(** The other axioms we take is that the results of - the [low_half] and [high_half] functions are of type [Tint], - i.e. either integers, pointers or undefined values. *) - -Axiom low_half_type: - forall v, Val.has_type (low_half v) Tint. -Axiom high_half_type: - forall v, Val.has_type (high_half v) Tint. - + Val.add (high_half ge id ofs) (low_half ge id ofs) = Genv.symbol_address ge id ofs. + (** We also axiomatize the small data area. For simplicity, we claim that small data symbols can be accessed by absolute 16-bit offsets, that is, relative to [GPR0]. In reality, the linker @@ -479,10 +469,10 @@ Parameter symbol_is_rel_data: ident -> int -> bool. Definition const_low (c: constant) := match c with | Cint n => Vint n - | Csymbol_low id ofs => low_half (Genv.symbol_address ge id ofs) + | Csymbol_low id ofs => low_half ge id ofs | Csymbol_high id ofs => Vundef | Csymbol_sda id ofs => small_data_area_offset ge id ofs - | Csymbol_rel_low id ofs => low_half (Genv.symbol_address ge id ofs) + | Csymbol_rel_low id ofs => low_half ge id ofs | Csymbol_rel_high id ofs => Vundef end. @@ -490,10 +480,10 @@ Definition const_high (c: constant) := match c with | Cint n => Vint (Int.shl n (Int.repr 16)) | Csymbol_low id ofs => Vundef - | Csymbol_high id ofs => high_half (Genv.symbol_address ge id ofs) + | Csymbol_high id ofs => high_half ge id ofs | Csymbol_sda id ofs => Vundef | Csymbol_rel_low id ofs => Vundef - | Csymbol_rel_high id ofs => high_half (Genv.symbol_address ge id ofs) + | Csymbol_rel_high id ofs => high_half ge id ofs end. (** The semantics is purely small-step and defined as a function diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 07cc50b..bec4daa 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -212,6 +212,11 @@ let expand_builtin_vload_sda chunk id ofs args res = assert false end +let expand_builtin_vload_rel chunk id ofs args res = + emit (Paddis(GPR11, GPR0, Csymbol_rel_high(id, ofs))); + emit (Paddi(GPR11, GPR11, Csymbol_rel_low(id, ofs))); + expand_builtin_vload chunk [IR GPR11] res + let expand_builtin_vstore_common chunk base offset src = match chunk, src with | (Mint8signed | Mint8unsigned), IR src -> @@ -264,11 +269,20 @@ let expand_builtin_vstore_sda chunk id ofs args = expand_builtin_vstore_common chunk GPR0 (Csymbol_sda(id, ofs)) src | [IR src1; IR src2] when chunk = Mint64 -> emit (Pstw(src1, Csymbol_sda(id, ofs), GPR0)); + let ofs = Int.add ofs _4 in emit (Pstw(src2, Csymbol_sda(id, ofs), GPR0)) | _ -> assert false end +let expand_builtin_vstore_rel chunk id ofs args = + let tmp = + if not (List.mem (IR GPR12) args) then GPR12 else + if not (List.mem (IR GPR11) args) then GPR11 else GPR10 in + emit (Paddis(tmp, GPR0, Csymbol_rel_high(id, ofs))); + emit (Paddi(tmp, tmp, Csymbol_rel_low(id, ofs))); + expand_builtin_vstore chunk (IR tmp :: args) + (* Handling of varargs *) let current_function_stacksize = ref 0l @@ -492,13 +506,19 @@ let expand_instruction instr = | EF_vstore chunk -> expand_builtin_vstore chunk args | EF_vload_global(chunk, id, ofs) -> - if symbol_is_small_data id ofs - then expand_builtin_vload_sda chunk id ofs args res - else expand_builtin_vload_global chunk id ofs args res + if symbol_is_small_data id ofs then + expand_builtin_vload_sda chunk id ofs args res + else if symbol_is_rel_data id ofs then + expand_builtin_vload_rel chunk id ofs args res + else + expand_builtin_vload_global chunk id ofs args res | EF_vstore_global(chunk, id, ofs) -> - if symbol_is_small_data id ofs - then expand_builtin_vstore_sda chunk id ofs args - else expand_builtin_vstore_global chunk id ofs args + if symbol_is_small_data id ofs then + expand_builtin_vstore_sda chunk id ofs args + else if symbol_is_rel_data id ofs then + expand_builtin_vstore_rel chunk id ofs args + else + expand_builtin_vstore_global chunk id ofs args | EF_memcpy(sz, al) -> expand_builtin_memcpy (Z.to_int sz) (Z.to_int al) args | EF_annot_val(txt, targ) -> diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 5c4ffde..2bd69d9 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -314,11 +314,6 @@ Definition transl_cond_op (** Translation of the arithmetic operation [r <- op(args)]. The corresponding instructions are prepended to [k]. *) -Definition csymbol_high (s: ident) (ofs: int) (rel: bool) := - if rel then Csymbol_rel_high s ofs else Csymbol_high s ofs. -Definition csymbol_low (s: ident) (ofs: int) (rel: bool) := - if rel then Csymbol_rel_low s ofs else Csymbol_low s ofs. - Definition transl_op (op: operation) (args: list mreg) (res: mreg) (k: code) := match op, args with @@ -338,10 +333,12 @@ Definition transl_op do r <- ireg_of res; OK (if symbol_is_small_data s ofs then Paddi r GPR0 (Csymbol_sda s ofs) :: k + else if symbol_is_rel_data s ofs then + Paddis r GPR0 (Csymbol_rel_high s ofs) :: + Paddi r r (Csymbol_rel_low s ofs) :: k else - let rel := symbol_is_rel_data s ofs in - Paddis r GPR0 (csymbol_high s ofs rel) :: - Paddi r r (csymbol_low s ofs rel) :: k) + Paddis r GPR0 (Csymbol_high s ofs) :: + Paddi r r (Csymbol_low s ofs) :: k) | Oaddrstack n, nil => do r <- ireg_of res; OK (addimm r GPR1 n k) | Ocast8signed, a1 :: nil => @@ -359,9 +356,10 @@ Definition transl_op Paddi GPR0 GPR0 (Csymbol_sda s ofs) :: Padd r r1 GPR0 :: k else if symbol_is_rel_data s ofs then - Paddis GPR0 GPR0 (Csymbol_rel_high s ofs) :: - Padd r r1 GPR0 :: - Paddi r r (Csymbol_rel_low s ofs) :: k + Pmr GPR0 r1 :: + Paddis r GPR0 (Csymbol_rel_high s ofs) :: + Paddi r r (Csymbol_rel_low s ofs) :: + Padd r r GPR0 :: k else Paddis r r1 (Csymbol_high s ofs) :: Paddi r r (Csymbol_low s ofs) :: k) @@ -531,19 +529,23 @@ Definition transl_memory_access | Aglobal symb ofs, nil => OK (if symbol_is_small_data symb ofs then mk1 (Csymbol_sda symb ofs) GPR0 :: k + else if symbol_is_rel_data symb ofs then + Paddis temp GPR0 (Csymbol_rel_high symb ofs) :: + Paddi temp temp (Csymbol_rel_low symb ofs) :: + mk1 (Cint Int.zero) temp :: k else - let rel := symbol_is_rel_data symb ofs in - Paddis temp GPR0 (csymbol_high symb ofs rel) :: - mk1 (csymbol_low symb ofs rel) temp :: k) + Paddis temp GPR0 (Csymbol_high symb ofs) :: + 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 Paddi GPR0 GPR0 (Csymbol_sda symb ofs) :: mk2 r1 GPR0 :: k else if symbol_is_rel_data symb ofs then - Paddis GPR0 GPR0 (Csymbol_rel_high symb ofs) :: - Padd temp r1 GPR0 :: - mk1 (Csymbol_rel_low symb ofs) temp :: k + Pmr GPR0 r1 :: + Paddis temp GPR0 (Csymbol_rel_high symb ofs) :: + Paddi temp temp (Csymbol_rel_low symb ofs) :: + mk2 temp GPR0 :: k else Paddis temp r1 (Csymbol_high symb ofs) :: mk1 (Csymbol_low symb ofs) temp :: k) diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 2b52fe0..9adf44d 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -246,9 +246,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_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 i0). TailNoLabel. destruct (symbol_is_rel_data i i0); 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. @@ -264,9 +263,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_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 i0). TailNoLabel. destruct (symbol_is_rel_data i i0); TailNoLabel. destruct (Int.eq (high_s i) Int.zero); TailNoLabel. Qed. diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index e1ab9a1..cb94c55 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -31,17 +31,6 @@ Require Import Asmgenproof0. (** * Properties of low half/high half decomposition *) -Lemma high_half_zero: - forall v, Val.add (high_half v) Vzero = high_half v. -Proof. - intros. generalize (high_half_type v). - rewrite Val.add_commut. - case (high_half v); simpl; intros; try contradiction. - auto. - rewrite Int.add_commut; rewrite Int.add_zero; auto. - rewrite Int.add_zero; auto. -Qed. - Lemma low_high_u: forall n, Int.or (Int.shl (high_u n) (Int.repr 16)) (low_u n) = n. Proof. @@ -111,20 +100,12 @@ Proof. simpl. rewrite Int.add_zero; auto. Qed. -Lemma csymbol_high_low: +Lemma low_high_half_zero: forall (ge: genv) id ofs, - Val.add (high_half (Genv.symbol_address ge id ofs)) (low_half (Genv.symbol_address ge id ofs)) - = Genv.symbol_address ge id ofs. + Val.add (Val.add Vzero (high_half ge id ofs)) (low_half ge id ofs) = + Genv.symbol_address ge id ofs. Proof. - intros. rewrite Val.add_commut. apply low_high_half. -Qed. - -Lemma csymbol_high_low_2: - forall (ge: genv) id ofs rel, - Val.add (const_high ge (csymbol_high id ofs rel)) - (const_low ge (csymbol_low id ofs rel)) = Genv.symbol_address ge id ofs. -Proof. - intros. destruct rel; apply csymbol_high_low. + intros. rewrite Val.add_assoc. rewrite low_high_half. apply add_zero_symbol_address. Qed. (** Useful properties of the GPR0 registers. *) @@ -863,16 +844,21 @@ 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_small_data i i0) eqn:SD; [ | destruct (symbol_is_rel_data i i0) ]. (* small data *) Opaque Val.add. econstructor; split. apply exec_straight_one; simpl; reflexivity. split. Simpl. rewrite small_data_area_addressing by auto. apply add_zero_symbol_address. intros; Simpl. - (* not small data *) + (* relative data *) + econstructor; split. eapply exec_straight_two; simpl; reflexivity. + split. Simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen. Simpl. + apply low_high_half_zero. + intros; Simpl. + (* absolute data *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. split. Simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. Simpl. - rewrite Val.add_assoc. rewrite csymbol_high_low_2. apply add_zero_symbol_address. + apply low_high_half_zero. intros; Simpl. (* Oaddrstack *) destruct (addimm_correct x GPR1 i k rs m) as [rs' [EX [RES OTH]]]; eauto with asmgen. @@ -881,24 +867,24 @@ 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_small_data i i0) eqn:SD; [ | destruct (symbol_is_rel_data i i0) ]. (* small data *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. split. Simpl. rewrite (Val.add_commut (rs x)). f_equal. rewrite small_data_area_addressing by auto. apply add_zero_symbol_address. intros; Simpl. - destruct (symbol_is_rel_data i i0). (* relative data *) - econstructor; split. eapply exec_straight_three; simpl; reflexivity. - split. Simpl. rewrite gpr_or_zero_zero. rewrite gpr_or_zero_not_zero by (eauto with asmgen). - Simpl. rewrite Val.add_assoc. rewrite (Val.add_commut (rs x)). f_equal. - rewrite Val.add_assoc. rewrite csymbol_high_low. apply add_zero_symbol_address. - intros; Simpl. + econstructor; split. eapply exec_straight_trans. + eapply exec_straight_two; simpl; reflexivity. + eapply exec_straight_two; simpl; reflexivity. + split. assert (GPR0 <> x0) by (apply sym_not_equal; eauto with asmgen). + Simpl. rewrite ! gpr_or_zero_zero. rewrite ! gpr_or_zero_not_zero by eauto with asmgen. Simpl. + rewrite low_high_half_zero. auto. + intros; Simpl. (* absolute data *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. split. Simpl. rewrite ! gpr_or_zero_not_zero by (eauto with asmgen). Simpl. - rewrite Val.add_assoc. rewrite (Val.add_commut (rs x)). f_equal. - apply csymbol_high_low. + rewrite Val.add_assoc. rewrite (Val.add_commut (rs x)). rewrite low_high_half. auto. intros; Simpl. (* Osubimm *) case (Int.eq (high_s i) Int.zero). @@ -1022,27 +1008,35 @@ Transparent Val.add. (* Aindexed2 *) apply MK2; auto. (* Aglobal *) - destruct (symbol_is_small_data i i0) eqn:SISD; inv TR. + destruct (symbol_is_small_data i i0) eqn:SISD; [ | destruct (symbol_is_rel_data i i0) ]; inv TR. (* Aglobal from small data *) apply MK1. unfold const_low. rewrite small_data_area_addressing by auto. apply add_zero_symbol_address. auto. - (* Aglobal general case *) - set (rel := symbol_is_rel_data i i0). - set (rs1 := nextinstr (rs#temp <- (const_high ge (csymbol_high i i0 rel)))). - exploit (MK1 (csymbol_low i i0 rel) temp rs1 k). - simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. - unfold rs1. Simpl. apply csymbol_high_low_2. - intros; unfold rs1; Simpl. + (* Aglobal from relative data *) + set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))). + set (rs2 := nextinstr (rs1#temp <- (Genv.symbol_address ge i i0))). + exploit (MK1 (Cint Int.zero) temp rs2). + simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen. + unfold rs2. Simpl. rewrite Val.add_commut. apply add_zero_symbol_address. + intros; unfold rs2, rs1; Simpl. intros [rs' [EX' AG']]. - exists rs'. split. apply exec_straight_step with rs1 m. - unfold exec_instr. rewrite gpr_or_zero_zero. - rewrite Val.add_commut. unfold const_high, csymbol_high. - destruct rel; rewrite high_half_zero; reflexivity. - reflexivity. - assumption. assumption. + exists rs'; split. apply exec_straight_step with rs1 m; auto. + apply exec_straight_step with rs2 m; auto. simpl. unfold rs2. + rewrite gpr_or_zero_not_zero by eauto with asmgen. f_equal. f_equal. f_equal. + unfold rs1; Simpl. apply low_high_half_zero. + eexact EX'. auto. + (* Aglobal from absolute data *) + set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))). + exploit (MK1 (Csymbol_low i i0) temp rs1). + simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen. + unfold rs1. Simpl. apply low_high_half_zero. + intros; unfold rs1; Simpl. + intros [rs' [EX' AG']]. + 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_small_data i i0) eqn:SISD; [ | destruct (symbol_is_rel_data i i0) ]. (* Abased from small data *) set (rs1 := nextinstr (rs#GPR0 <- (Genv.symbol_address ge i i0))). exploit (MK2 x GPR0 rs1 k). @@ -1055,30 +1049,25 @@ Transparent Val.add. apply add_zero_symbol_address. reflexivity. assumption. assumption. - destruct (symbol_is_rel_data i i0). - (* Abased relative *) - set (rs1 := nextinstr (rs#GPR0 <- (const_high ge (Csymbol_rel_high i i0)))). - set (rs2 := nextinstr (rs1#temp <- (Val.add (rs x) (const_high ge (Csymbol_rel_high i i0))))). - exploit (MK1 (Csymbol_rel_low i i0) temp rs2 k). - simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. - unfold rs2. Simpl. rewrite Val.add_assoc. simpl. rewrite csymbol_high_low. - apply Val.add_commut. - intros. unfold rs2; Simpl. unfold rs1; Simpl. + (* Abased from relative data *) + set (rs1 := nextinstr (rs#GPR0 <- (rs#x))). + set (rs2 := nextinstr (rs1#temp <- (Val.add Vzero (high_half ge i i0)))). + set (rs3 := nextinstr (rs2#temp <- (Genv.symbol_address ge i i0))). + exploit (MK2 temp GPR0 rs3). + f_equal. unfold rs3; Simpl. unfold rs3, rs2, rs1; Simpl. + intros. unfold rs3, rs2, rs1; Simpl. intros [rs' [EX' AG']]. - exists rs'. split. apply exec_straight_step with rs1 m. - unfold exec_instr. rewrite gpr_or_zero_zero. - rewrite (Val.add_commut Vzero). unfold const_high. rewrite high_half_zero. auto. - reflexivity. - apply exec_straight_step with rs2 m. - simpl. unfold rs2, rs1. Simpl. - reflexivity. - assumption. assumption. + exists rs'. split. eapply exec_straight_trans with (rs2 := rs3) (m2 := m). + apply exec_straight_three with rs1 m rs2 m; auto. + simpl. unfold rs3. f_equal. f_equal. f_equal. rewrite gpr_or_zero_not_zero by auto. + unfold rs2; Simpl. apply low_high_half_zero. + eexact EX'. auto. (* Abased absolute *) - set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (const_high ge (Csymbol_high i i0))))). + set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (high_half ge i i0)))). exploit (MK1 (Csymbol_low i i0) temp rs1 k). simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. unfold rs1. Simpl. - rewrite Val.add_assoc. simpl. rewrite csymbol_high_low. apply Val.add_commut. + rewrite Val.add_assoc. rewrite low_high_half. apply Val.add_commut. intros; unfold rs1; Simpl. intros [rs' [EX' AG']]. exists rs'. split. apply exec_straight_step with rs1 m. diff --git a/powerpc/extractionMachdep.v b/powerpc/extractionMachdep.v index 352d3b5..b448e3d 100644 --- a/powerpc/extractionMachdep.v +++ b/powerpc/extractionMachdep.v @@ -13,8 +13,8 @@ (* Additional extraction directives specific to the PowerPC port *) (* Asm *) -Extract Constant Asm.low_half => "fun _ -> assert false". -Extract Constant Asm.high_half => "fun _ -> assert false". +Extract Constant Asm.low_half => "fun _ _ _ -> assert false". +Extract Constant Asm.high_half => "fun _ _ _ -> assert false". Extract Constant Asm.symbol_is_small_data => "C2C.atom_is_small_data". Extract Constant Asm.small_data_area_offset => "fun _ _ _ -> assert false". Extract Constant Asm.symbol_is_rel_data => "C2C.atom_is_rel_data". -- cgit v1.2.3