diff options
Diffstat (limited to 'ia32')
| -rw-r--r-- | ia32/Machregs.v | 30 | ||||
| -rw-r--r-- | ia32/Machregsaux.ml | 31 | ||||
| -rw-r--r-- | ia32/Machregsaux.mli | 1 | ||||
| -rw-r--r-- | ia32/Op.v | 70 | ||||
| -rw-r--r-- | ia32/PrintOp.ml | 12 | ||||
| -rw-r--r-- | ia32/TargetPrinter.ml | 8 |
6 files changed, 89 insertions, 63 deletions
diff --git a/ia32/Machregs.v b/ia32/Machregs.v index a9f2b6c4..65e27599 100644 --- a/ia32/Machregs.v +++ b/ia32/Machregs.v @@ -69,6 +69,25 @@ End IndexedMreg. Definition is_stack_reg (r: mreg) : bool := match r with FP0 => true | _ => false end. +(** ** Names of registers *) + +Local Open Scope string_scope. + +Definition register_names := + ("EAX", AX) :: ("EBX", BX) :: ("ECX", CX) :: ("EDX", DX) :: + ("ESI", SI) :: ("EDI", DI) :: ("EBP", BP) :: + ("XMM0", X0) :: ("XMM1", X1) :: ("XMM2", X2) :: ("XMM3", X3) :: + ("XMM4", X4) :: ("XMM5", X5) :: ("XMM6", X6) :: ("XMM7", X7) :: + ("ST0", FP0) :: 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 := @@ -100,7 +119,15 @@ Definition destroyed_by_cond (cond: condition): list mreg := Definition destroyed_by_jumptable: list mreg := nil. -Local Open Scope string_scope. +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 builtin_write16_reversed := ident_of_string "__builtin_write16_reversed". Definition builtin_write32_reversed := ident_of_string "__builtin_write32_reversed". @@ -115,6 +142,7 @@ Definition destroyed_by_builtin (ef: external_function): list mreg := if ident_eq id builtin_write16_reversed || ident_eq id builtin_write32_reversed then CX :: DX :: nil else nil + | EF_inline_asm txt sg clob => destroyed_by_clobber clob | _ => nil end. diff --git a/ia32/Machregsaux.ml b/ia32/Machregsaux.ml index 5e98b58b..6485e752 100644 --- a/ia32/Machregsaux.ml +++ b/ia32/Machregsaux.ml @@ -12,38 +12,25 @@ (** Auxiliary functions on machine registers *) +open Camlcoq open Machregs -let register_names = [ - ("EAX", AX); ("EBX", BX); ("ECX", CX); ("EDX", DX); - ("ESI", SI); ("EDI", DI); ("EBP", BP); - ("XMM0", X0); ("XMM1", X1); ("XMM2", X2); ("XMM3", X3); - ("XMM4", X4); ("XMM5", X5); ("XMM6", X6); ("XMM7", X7); - ("ST0", FP0) -] +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 = [] 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/ia32/Machregsaux.mli b/ia32/Machregsaux.mli index f0feec96..d4877a62 100644 --- a/ia32/Machregsaux.mli +++ b/ia32/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 @@ -755,30 +755,30 @@ 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 _ (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; inv H2; simpl in H0; inv H0; auto. @@ -789,7 +789,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. @@ -798,32 +798,32 @@ 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. - 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 H5; simpl; auto. - apply Values.val_add_inject; auto. apply Values.val_add_inject; auto. inv H3; 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. 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. + 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 -> + 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. @@ -959,7 +959,7 @@ Proof. apply weak_valid_pointer_extends; auto. apply weak_valid_pointer_no_overflow_extends. 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: @@ -969,10 +969,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. @@ -991,10 +991,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. @@ -1018,7 +1018,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. @@ -1027,7 +1027,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. @@ -1041,11 +1041,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. @@ -1055,12 +1055,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/ia32/PrintOp.ml b/ia32/PrintOp.ml index fb9a7cc5..1f7f4a65 100644 --- a/ia32/PrintOp.ml +++ b/ia32/PrintOp.ml @@ -38,6 +38,10 @@ let print_condition reg pp = function fprintf pp "%a %sf %a" reg r1 (comparison_name c) reg r2 | (Cnotcompf c, [r1;r2]) -> fprintf pp "%a not(%sf) %a" reg r1 (comparison_name c) reg r2 + | (Ccompfs c, [r1;r2]) -> + fprintf pp "%a %sfs %a" reg r1 (comparison_name c) reg r2 + | (Cnotcompfs c, [r1;r2]) -> + fprintf pp "%a not(%sfs) %a" reg r1 (comparison_name c) reg r2 | (Cmaskzero n, [r1]) -> fprintf pp "%a & 0x%lx == 0" reg r1 (camlint_of_coqint n) | (Cmasknotzero n, [r1]) -> @@ -100,10 +104,18 @@ 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 | Ofloatofint, [r1] -> fprintf pp "floatofint(%a)" reg r1 + | Ointofsingle, [r1] -> fprintf pp "intofsingle(%a)" reg r1 + | Osingleofint, [r1] -> fprintf pp "singleofint(%a)" reg r1 | Omakelong, [r1;r2] -> fprintf pp "makelong(%a,%a)" reg r1 reg r2 | Olowlong, [r1] -> fprintf pp "lowlong(%a)" reg r1 | Ohighlong, [r1] -> fprintf pp "highlong(%a)" reg r1 diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index ca07a172..a53a8fbd 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -323,7 +323,7 @@ module Target(System: SYSTEM):TARGET = (* Emit .file / .loc debugging directives *) let print_file_line oc file line = - PrintAnnot.print_file_line oc comment file line + print_file_line oc comment file line let print_location oc loc = if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc) @@ -345,12 +345,12 @@ 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 "%esp" oc txt targs args + print_annot_stmt preg "%esp" oc txt targs args end let print_annot_val oc txt args res = fprintf oc "%s annotation: " comment; - PrintAnnot.print_annot_val preg oc txt args; + print_annot_val preg oc txt args; match args, res with | [IR src], [IR dst] -> if dst <> src then fprintf oc " movl %a, %a\n" ireg src ireg dst @@ -873,7 +873,7 @@ module Target(System: SYSTEM):TARGET = print_annot_val oc (extern_atom txt) args res | 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 |