diff options
Diffstat (limited to 'powerpc')
| -rw-r--r-- | powerpc/Machregs.v | 42 | ||||
| -rw-r--r-- | powerpc/Machregsaux.ml | 43 | ||||
| -rw-r--r-- | powerpc/Machregsaux.mli | 1 | ||||
| -rw-r--r-- | powerpc/Op.v | 70 | ||||
| -rw-r--r-- | powerpc/PrintOp.ml | 8 | ||||
| -rw-r--r-- | powerpc/TargetPrinter.ml | 12 |
6 files changed, 100 insertions, 76 deletions
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index f7ed7793..3b7cbb76 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -10,6 +10,7 @@ (* *) (* *********************************************************************) +Require Import String. Require Import Coqlib. Require Import Maps. Require Import AST. @@ -97,6 +98,36 @@ End IndexedMreg. Definition is_stack_reg (r: mreg) : bool := false. +(** ** Names of registers *) + +Local Open Scope string_scope. + +Definition register_names := + ("R3", R3) :: ("R4", R4) :: ("R5", R5) :: ("R6", R6) :: + ("R7", R7) :: ("R8", R8) :: ("R9", R9) :: ("R10", R10) :: + ("R11", R11) :: ("R12", R12) :: + ("R14", R14) :: ("R15", R15) :: ("R16", R16) :: + ("R17", R17) :: ("R18", R18) :: ("R19", R19) :: ("R20", R20) :: + ("R21", R21) :: ("R22", R22) :: ("R23", R23) :: ("R24", R24) :: + ("R25", R25) :: ("R26", R26) :: ("R27", R27) :: ("R28", R28) :: + ("R29", R29) :: ("R30", R30) :: ("R31", R31) :: + ("F0", F0) :: ("F1", F1) :: ("F2", F2) :: ("F3", F3) :: ("F4", F4) :: + ("F5", F5) :: ("F6", F6) :: ("F7", F7) :: ("F8", F8) :: + ("F9", F9) :: ("F10", F10) :: ("F11", F11) :: ("F12", F12) :: + ("F13", F13) :: ("F14", F14) :: ("F15", F15) :: + ("F16", F16) :: ("F17", F17) :: ("F18", F18) :: ("F19", F19) :: + ("F20", F20) :: ("F21", F21) :: ("F22", F22) :: ("F23", F23) :: + ("F24", F24) :: ("F25", F25) :: ("F26", F26) :: ("F27", F27) :: + ("F28", F28) :: ("F29", F29) :: ("F30", F30) :: ("F31", F31) :: nil. + +Definition register_by_name (s: string) : option mreg := + let fix assoc (l: list (string * mreg)) : option mreg := + match l with + | nil => None + | (s1, r1) :: l' => if string_dec s s1 then Some r1 else assoc l' + end + in assoc register_names. + (** ** Destroyed registers, preferred registers *) Definition destroyed_by_op (op: operation): list mreg := @@ -119,6 +150,16 @@ Definition destroyed_by_cond (cond: condition): list mreg := Definition destroyed_by_jumptable: list mreg := R12 :: nil. +Fixpoint destroyed_by_clobber (cl: list string): list mreg := + match cl with + | nil => nil + | c1 :: cl => + match register_by_name c1 with + | Some r => r :: destroyed_by_clobber cl + | None => destroyed_by_clobber cl + end + end. + Definition destroyed_by_builtin (ef: external_function): list mreg := match ef with | EF_builtin _ _ => F13 :: nil @@ -128,6 +169,7 @@ Definition destroyed_by_builtin (ef: external_function): list mreg := | EF_vstore_global Mint64 _ _ => R10 :: R11 :: R12 :: nil | EF_vstore_global _ _ _ => R11 :: R12 :: nil | EF_memcpy _ _ => R11 :: R12 :: F13 :: nil + | EF_inline_asm txt sg clob => destroyed_by_clobber clob | _ => nil end. diff --git a/powerpc/Machregsaux.ml b/powerpc/Machregsaux.ml index ba111089..8c3017ff 100644 --- a/powerpc/Machregsaux.ml +++ b/powerpc/Machregsaux.ml @@ -12,49 +12,24 @@ (** Auxiliary functions on machine registers *) +open Camlcoq open Machregs -let register_names = [ - ("R3", R3); ("R4", R4); ("R5", R5); ("R6", R6); - ("R7", R7); ("R8", R8); ("R9", R9); ("R10", R10); - ("R11", R11); ("R12", R12); - ("R14", R14); ("R15", R15); ("R16", R16); - ("R17", R17); ("R18", R18); ("R19", R19); ("R20", R20); - ("R21", R21); ("R22", R22); ("R23", R23); ("R24", R24); - ("R25", R25); ("R26", R26); ("R27", R27); ("R28", R28); - ("R29", R29); ("R30", R30); ("R31", R31); - ("F0", F0); ("F1", F1); ("F2", F2); ("F3", F3); ("F4", F4); - ("F5", F5); ("F6", F6); ("F7", F7); ("F8", F8); - ("F9", F9); ("F10", F10); ("F11", F11); ("F12", F12); - ("F13", F13); ("F14", F14); ("F15", F15); - ("F16", F16); ("F17", F17); ("F18", F18); ("F19", F19); - ("F20", F20); ("F21", F21); ("F22", F22); ("F23", F23); - ("F24", F24); ("F25", F25); ("F26", F26); ("F27", F27); - ("F28", F28); ("F29", F29); ("F30", F30); ("F31", F31) -] +let register_names : (mreg, string) Hashtbl.t = Hashtbl.create 31 + +let _ = + List.iter + (fun (s, r) -> Hashtbl.add register_names r (camlstring_of_coqstring s)) + Machregs.register_names let scratch_register_names = [ "R0" ] let name_of_register r = - let rec rev_assoc = function - | [] -> None - | (a, b) :: rem -> if b = r then Some a else rev_assoc rem - in rev_assoc register_names + try Some (Hashtbl.find register_names r) with Not_found -> None let register_by_name s = - try - Some(List.assoc (String.uppercase s) register_names) - with Not_found -> - None + Machregs.register_by_name (coqstring_of_camlstring (String.uppercase s)) let can_reserve_register r = List.mem r Conventions1.int_callee_save_regs || List.mem r Conventions1.float_callee_save_regs - -let mregs_of_clobber idl = - List.fold_left - (fun l c -> - match register_by_name (Camlcoq.extern_atom c) with - | Some r -> r :: l - | None -> l) - [] idl diff --git a/powerpc/Machregsaux.mli b/powerpc/Machregsaux.mli index f0feec96..d4877a62 100644 --- a/powerpc/Machregsaux.mli +++ b/powerpc/Machregsaux.mli @@ -16,4 +16,3 @@ val name_of_register: Machregs.mreg -> string option val register_by_name: string -> Machregs.mreg option val scratch_register_names: string list val can_reserve_register: Machregs.mreg -> bool -val mregs_of_clobber: Camlcoq.atom list -> Machregs.mreg list diff --git a/powerpc/Op.v b/powerpc/Op.v index 4c1168cd..3ff08791 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -677,32 +677,32 @@ Hypothesis valid_different_pointers_inj: Ltac InvInject := match goal with - | [ H: val_inject _ (Vint _) _ |- _ ] => + | [ H: Val.inject _ (Vint _) _ |- _ ] => inv H; InvInject - | [ H: val_inject _ (Vfloat _) _ |- _ ] => + | [ H: Val.inject _ (Vfloat _) _ |- _ ] => inv H; InvInject - | [ H: val_inject _ (Vsingle _) _ |- _ ] => + | [ H: Val.inject _ (Vsingle _) _ |- _ ] => inv H; InvInject - | [ H: val_inject _ (Vptr _ _) _ |- _ ] => + | [ H: Val.inject _ (Vptr _ _) _ |- _ ] => inv H; InvInject - | [ H: val_list_inject _ nil _ |- _ ] => + | [ H: Val.inject_list _ nil _ |- _ ] => inv H; InvInject - | [ H: val_list_inject _ (_ :: _) _ |- _ ] => + | [ H: Val.inject_list _ (_ :: _) _ |- _ ] => inv H; InvInject | _ => idtac end. Lemma eval_condition_inj: forall cond vl1 vl2 b, - val_list_inject f vl1 vl2 -> + Val.inject_list f vl1 vl2 -> eval_condition cond vl1 m1 = Some b -> eval_condition cond vl2 m2 = Some b. Proof. intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto. inv H3; inv H2; simpl in H0; inv H0; auto. - eauto 3 using val_cmpu_bool_inject, Mem.valid_pointer_implies. + eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. inv H3; simpl in H0; inv H0; auto. - eauto 3 using val_cmpu_bool_inject, Mem.valid_pointer_implies. + eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. inv H3; inv H2; simpl in H0; inv H0; auto. inv H3; inv H2; simpl in H0; inv H0; auto. inv H3; try discriminate; auto. @@ -711,7 +711,7 @@ Qed. Ltac TrivialExists := match goal with - | [ |- exists v2, Some ?v1 = Some v2 /\ val_inject _ _ v2 ] => + | [ |- exists v2, Some ?v1 = Some v2 /\ Val.inject _ _ v2 ] => exists v1; split; auto | _ => idtac end. @@ -720,20 +720,20 @@ 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 -> + Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> + Val.inject f sp1 sp2 -> + Val.inject_list f vl1 vl2 -> 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. + exists v2, eval_operation ge2 sp2 op vl2 m2 = Some v2 /\ Val.inject f v1 v2. Proof. 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. + 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 GL; simpl; 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. @@ -797,16 +797,16 @@ 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 -> + Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> + Val.inject f sp1 sp2 -> + Val.inject_list f vl1 vl2 -> eval_addressing ge1 sp1 addr vl1 = Some v1 -> - exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ val_inject f v1 v2. + exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ Val.inject f v1 v2. Proof. intros. destruct addr; simpl in H2; simpl; FuncInv; InvInject; TrivialExists; - auto using Values.val_add_inject. + auto using Values.Val.add_inject. apply H; simpl; auto. - apply Values.val_add_inject; auto. apply H; simpl; auto. + apply Values.Val.add_inject; auto. apply H; simpl; auto. Qed. End EVAL_COMPAT. @@ -872,7 +872,7 @@ Proof. apply weak_valid_pointer_extends; auto. apply weak_valid_pointer_no_overflow_extends; auto. apply valid_different_pointers_extends; auto. - rewrite <- val_list_inject_lessdef. eauto. auto. + rewrite <- val_inject_list_lessdef. eauto. auto. Qed. Lemma eval_operation_lessdef: @@ -882,10 +882,10 @@ Lemma eval_operation_lessdef: eval_operation genv sp op vl1 m1 = Some v1 -> exists v2, eval_operation genv sp op vl2 m2 = Some v2 /\ Val.lessdef v1 v2. Proof. - intros. rewrite val_list_inject_lessdef in H. + intros. rewrite val_inject_list_lessdef in H. assert (exists v2 : val, eval_operation genv sp op vl2 m2 = Some v2 - /\ val_inject (fun b => Some(b, 0)) v1 v2). + /\ Val.inject (fun b => Some(b, 0)) v1 v2). eapply eval_operation_inj with (m1 := m1) (sp1 := sp). apply valid_pointer_extends; auto. apply weak_valid_pointer_extends; auto. @@ -903,10 +903,10 @@ Lemma eval_addressing_lessdef: eval_addressing genv sp addr vl1 = Some v1 -> exists v2, eval_addressing genv sp addr vl2 = Some v2 /\ Val.lessdef v1 v2. Proof. - intros. rewrite val_list_inject_lessdef in H. + intros. rewrite val_inject_list_lessdef in H. assert (exists v2 : val, eval_addressing genv sp addr vl2 = Some v2 - /\ val_inject (fun b => Some(b, 0)) v1 v2). + /\ Val.inject (fun b => Some(b, 0)) v1 v2). eapply eval_addressing_inj with (sp1 := sp). intros. rewrite <- val_inject_lessdef; auto. rewrite <- val_inject_lessdef; auto. @@ -930,7 +930,7 @@ Variable delta: Z. Hypothesis sp_inj: f sp1 = Some(sp2, delta). Remark symbol_address_inject: - forall id ofs, val_inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs). + forall id ofs, Val.inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs). Proof. intros. unfold Genv.symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto. exploit (proj1 globals); eauto. intros. @@ -939,7 +939,7 @@ Qed. Lemma eval_condition_inject: forall cond vl1 vl2 b m1 m2, - val_list_inject f vl1 vl2 -> + Val.inject_list f vl1 vl2 -> Mem.inject f m1 m2 -> eval_condition cond vl1 m1 = Some b -> eval_condition cond vl2 m2 = Some b. @@ -953,11 +953,11 @@ Qed. Lemma eval_addressing_inject: forall addr vl1 vl2 v1, - val_list_inject f vl1 vl2 -> + Val.inject_list f vl1 vl2 -> eval_addressing genv (Vptr sp1 Int.zero) addr vl1 = Some v1 -> exists v2, eval_addressing genv (Vptr sp2 Int.zero) (shift_stack_addressing (Int.repr delta) addr) vl2 = Some v2 - /\ val_inject f v1 v2. + /\ Val.inject f v1 v2. Proof. intros. rewrite eval_shift_stack_addressing. simpl. @@ -967,12 +967,12 @@ Qed. Lemma eval_operation_inject: forall op vl1 vl2 v1 m1 m2, - val_list_inject f vl1 vl2 -> + Val.inject_list f vl1 vl2 -> Mem.inject f m1 m2 -> eval_operation genv (Vptr sp1 Int.zero) op vl1 m1 = Some v1 -> exists v2, eval_operation genv (Vptr sp2 Int.zero) (shift_stack_operation (Int.repr delta) op) vl2 m2 = Some v2 - /\ val_inject f v1 v2. + /\ Val.inject f v1 v2. Proof. intros. rewrite eval_shift_stack_operation. simpl. diff --git a/powerpc/PrintOp.ml b/powerpc/PrintOp.ml index 664280f9..b0213014 100644 --- a/powerpc/PrintOp.ml +++ b/powerpc/PrintOp.ml @@ -49,6 +49,7 @@ let print_operation reg pp = function | Omove, [r1] -> reg pp r1 | Ointconst n, [] -> fprintf pp "%ld" (camlint_of_coqint n) | Ofloatconst n, [] -> fprintf pp "%F" (camlfloat_of_coqfloat n) + | Osingleconst n, [] -> fprintf pp "%Ff" (camlfloat_of_coqfloat32 n) | Oaddrsymbol(id, ofs), [] -> fprintf pp "\"%s\" + %ld" (extern_atom id) (camlint_of_coqint ofs) | Oaddrstack ofs, [] -> @@ -95,7 +96,14 @@ let print_operation reg pp = function | Osubf, [r1;r2] -> fprintf pp "%a -f %a" reg r1 reg r2 | Omulf, [r1;r2] -> fprintf pp "%a *f %a" reg r1 reg r2 | Odivf, [r1;r2] -> fprintf pp "%a /f %a" reg r1 reg r2 + | Onegfs, [r1] -> fprintf pp "negfs(%a)" reg r1 + | Oabsfs, [r1] -> fprintf pp "absfs(%a)" reg r1 + | Oaddfs, [r1;r2] -> fprintf pp "%a +fs %a" reg r1 reg r2 + | Osubfs, [r1;r2] -> fprintf pp "%a -fs %a" reg r1 reg r2 + | Omulfs, [r1;r2] -> fprintf pp "%a *fs %a" reg r1 reg r2 + | Odivfs, [r1;r2] -> fprintf pp "%a /fs %a" reg r1 reg r2 | Osingleoffloat, [r1] -> fprintf pp "singleoffloat(%a)" reg r1 + | Ofloatofsingle, [r1] -> fprintf pp "floatofsingle(%a)" reg r1 | Ointoffloat, [r1] -> fprintf pp "intoffloat(%a)" reg r1 | Ofloatofwords, [r1;r2] -> fprintf pp "floatofwords(%a,%a)" reg r1 reg r2 | Omakelong, [r1;r2] -> fprintf pp "makelong(%a,%a)" reg r1 reg r2 diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index b05b29c0..3789d62e 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -132,7 +132,7 @@ module Linux_System : SYSTEM = let print_file_line oc file line = - PrintAnnot.print_file_line oc comment file line + print_file_line oc comment file line (* Emit .cfi directives *) let cfi_startproc = cfi_startproc @@ -203,7 +203,7 @@ module Diab_System : SYSTEM = | Section_debug_abbrev -> ".debug_abbrev,,n" let print_file_line oc file line = - PrintAnnot.print_file_line_d2 oc comment file line + print_file_line_d2 oc comment file line (* Emit .cfi directives *) let cfi_startproc oc = () @@ -240,10 +240,10 @@ module Diab_System : SYSTEM = end_addr := label_end; fprintf oc "%a:\n" label label_end; fprintf oc " .text\n"; - PrintAnnot.StringSet.iter (fun file -> + StringSet.iter (fun file -> let label = new_label () in Hashtbl.add filenum file label; - fprintf oc ".L%d: .d2filenum \"%s\"\n" label file) !PrintAnnot.all_files; + fprintf oc ".L%d: .d2filenum \"%s\"\n" label file) !all_files; fprintf oc " .d2_line_end\n" end @@ -331,7 +331,7 @@ module Target (System : SYSTEM):TARGET = (int_of_string (Str.matched_group 2 txt)) end else begin fprintf oc "%s annotation: " comment; - PrintAnnot.print_annot_stmt preg_annot "R1" oc txt targs args + print_annot_stmt preg_annot "R1" oc txt targs args end (* Determine if the displacement of a conditional branch fits the short form *) @@ -652,7 +652,7 @@ module Target (System : SYSTEM):TARGET = begin match ef with | EF_inline_asm(txt, sg, clob) -> fprintf oc "%s begin inline assembly\n\t" comment; - PrintAnnot.print_inline_asm preg oc (extern_atom txt) sg args res; + print_inline_asm preg oc (extern_atom txt) sg args res; fprintf oc "%s end inline assembly\n" comment | _ -> assert false |