diff options
Diffstat (limited to 'ia32')
-rw-r--r-- | ia32/Asm.v | 18 | ||||
-rw-r--r-- | ia32/Asmgen.v | 6 | ||||
-rw-r--r-- | ia32/Asmgenproof.v | 4 | ||||
-rw-r--r-- | ia32/Asmgenproof1.v | 14 | ||||
-rw-r--r-- | ia32/Machregs.v | 9 | ||||
-rw-r--r-- | ia32/Op.v | 21 | ||||
-rw-r--r-- | ia32/PrintAsm.ml | 12 | ||||
-rw-r--r-- | ia32/standard/Conventions1.v | 7 |
8 files changed, 51 insertions, 40 deletions
@@ -115,8 +115,6 @@ Inductive instruction: Type := | Pmov_ra (rd: ireg) (id: ident) | Pmov_rm (rd: ireg) (a: addrmode) | Pmov_mr (a: addrmode) (rs: ireg) - | Pmovd_fr (rd: freg) (r1: ireg) (**r [movd] (32-bit int) *) - | Pmovd_rf (rd: ireg) (rd: freg) | Pmovsd_ff (rd: freg) (r1: freg) (**r [movsd] (single 64-bit float) *) | Pmovsd_fi (rd: freg) (n: float) (**r (pseudo-instruction) *) | Pmovsd_fm (rd: freg) (a: addrmode) @@ -129,16 +127,16 @@ Inductive instruction: Type := (** Moves with conversion *) | Pmovb_mr (a: addrmode) (rs: ireg) (**r [mov] (8-bit int) *) | Pmovw_mr (a: addrmode) (rs: ireg) (**r [mov] (16-bit int) *) - | Pmovzb_rr (rd: ireg) (rs: ireg) (**r [movzb] (8-bit zero-extension) *) + | Pmovzb_rr (rd: ireg) (rs: ireg) (**r [movzb] (8-bit zero-extension) *) | Pmovzb_rm (rd: ireg) (a: addrmode) - | Pmovsb_rr (rd: ireg) (rs: ireg) (**r [movsb] (8-bit sign-extension) *) + | Pmovsb_rr (rd: ireg) (rs: ireg) (**r [movsb] (8-bit sign-extension) *) | Pmovsb_rm (rd: ireg) (a: addrmode) - | Pmovzw_rr (rd: ireg) (rs: ireg) (**r [movzw] (16-bit zero-extension) *) + | Pmovzw_rr (rd: ireg) (rs: ireg) (**r [movzw] (16-bit zero-extension) *) | Pmovzw_rm (rd: ireg) (a: addrmode) - | Pmovsw_rr (rd: ireg) (rs: ireg) (**r [movsw] (16-bit sign-extension) *) + | Pmovsw_rr (rd: ireg) (rs: ireg) (**r [movsw] (16-bit sign-extension) *) | Pmovsw_rm (rd: ireg) (a: addrmode) | Pcvtss2sd_fm (rd: freg) (a: addrmode) (**r [cvtss2sd] (single float load) *) - | Pcvtsd2ss_ff (rd: freg) (r1: freg) (**r pseudo (single conversion) *) + | Pcvtsd2ss_ff (rd: freg) (r1: freg) (**r conversion to single (pseudo) *) | Pcvtsd2ss_mf (a: addrmode) (r1: freg) (**r [cvtsd2ss] (single float store *) | Pcvttsd2si_rf (rd: ireg) (r1: freg) (**r double to signed int *) | Pcvtsi2sd_fr (rd: freg) (r1: ireg) (**r signed int to double *) @@ -185,7 +183,7 @@ Inductive instruction: Type := | Pjmp_s (symb: ident) | Pjmp_r (r: ireg) | Pjcc (c: testcond)(l: label) - | Pjcc2 (c1 c2: testcond)(l: label) + | Pjcc2 (c1 c2: testcond)(l: label) (**r pseudo *) | Pjmptbl (r: ireg) (tbl: list label) (**r pseudo *) | Pcall_s (symb: ident) | Pcall_r (r: ireg) @@ -481,10 +479,6 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome exec_load Mint32 m a rs rd | Pmov_mr a r1 => exec_store Mint32 m a rs r1 nil - | Pmovd_fr rd r1 => - Next (nextinstr (rs#rd <- (rs r1))) m - | Pmovd_rf rd r1 => - Next (nextinstr (rs#rd <- (rs r1))) m | Pmovsd_ff rd r1 => Next (nextinstr (rs#rd <- (rs r1))) m | Pmovsd_fi rd n => diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v index 78f7d6e5..4543ac9b 100644 --- a/ia32/Asmgen.v +++ b/ia32/Asmgen.v @@ -103,6 +103,9 @@ Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) := | ST0 => OK (Pfld_m (Addrmode (Some base) None (inl _ ofs)) :: k) | _ => Error (msg "Asmgen.loadind") end + | Tsingle => + do r <- freg_of dst; + OK (Pcvtss2sd_fm r (Addrmode (Some base) None (inl _ ofs)) :: k) | Tlong => Error (msg "Asmgen.loadind") end. @@ -118,6 +121,9 @@ Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) := | ST0 => OK (Pfstp_m (Addrmode (Some base) None (inl _ ofs)) :: k) | _ => Error (msg "Asmgen.loadind") end + | Tsingle => + do r <- freg_of src; + OK (Pcvtsd2ss_mf (Addrmode (Some base) None (inl _ ofs)) r :: k) | Tlong => Error (msg "Asmgen.storeind") end. diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index ca0fd182..f6eefbde 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -172,6 +172,7 @@ Proof. TailNoLabel. destruct (preg_of dst); TailNoLabel. discriminate. + TailNoLabel. Qed. Remark storeind_label: @@ -183,6 +184,7 @@ Proof. TailNoLabel. destruct (preg_of src); TailNoLabel. discriminate. + TailNoLabel. Qed. Remark mk_setcc_base_label: @@ -506,6 +508,8 @@ Proof. exists rs'; split. eauto. split. eapply agree_undef_regs; eauto. simpl; intros. rewrite Q; auto with asmgen. +Local Transparent destroyed_by_setstack. + destruct ty; simpl; intuition congruence. - (* Mgetparam *) assert (f0 = f) by congruence; subst f0. diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index 303337ed..00b706cb 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -341,6 +341,12 @@ Proof. intuition Simplifs. (* long *) inv H. + (* single *) + monadInv H. + rewrite (freg_of_eq _ _ EQ). econstructor. + split. apply exec_straight_one. simpl. unfold exec_load. rewrite H1. rewrite H0. + eauto. auto. + intuition Simplifs. Qed. Lemma storeind_correct: @@ -349,7 +355,7 @@ Lemma storeind_correct: Mem.storev (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) (rs#(preg_of src)) = Some m' -> exists rs', exec_straight ge fn c rs m k rs' m' - /\ forall r, data_preg r = true -> r <> ST0 -> rs'#r = rs#r. + /\ forall r, data_preg r = true -> preg_notin r (destroyed_by_setstack ty) -> rs'#r = rs#r. Proof. unfold storeind; intros. set (addr := Addrmode (Some base) None (inl (ident * int) ofs)) in *. @@ -372,6 +378,12 @@ Proof. intros. simpl. Simplifs. (* long *) inv H. + (* single *) + monadInv H. + rewrite (freg_of_eq _ _ EQ) in H0. econstructor. + split. apply exec_straight_one. simpl. unfold exec_store. rewrite H1. rewrite H0. + simpl. eauto. auto. + intros. destruct H2. Simplifs. Qed. (** Translation of addressing modes *) diff --git a/ia32/Machregs.v b/ia32/Machregs.v index 31ea8eea..528e9ed0 100644 --- a/ia32/Machregs.v +++ b/ia32/Machregs.v @@ -124,6 +124,13 @@ Definition destroyed_by_builtin (ef: external_function): list mreg := Definition destroyed_at_function_entry: list mreg := DX :: FP0 :: nil. (* must include destroyed_by_op Omove *) +Definition destroyed_by_setstack (ty: typ): list mreg := + match ty with + | Tfloat => FP0 :: nil + | Tsingle => X7 :: FP0 :: nil + | _ => nil + end. + Definition temp_for_parent_frame: mreg := DX. @@ -164,7 +171,7 @@ Definition mregs_for_builtin (ef: external_function): list (option mreg) * list Global Opaque destroyed_by_op destroyed_by_load destroyed_by_store destroyed_by_cond destroyed_by_jumptable destroyed_by_builtin - destroyed_at_function_entry temp_for_parent_frame + destroyed_by_setstack destroyed_at_function_entry temp_for_parent_frame mregs_for_operation mregs_for_builtin. (** Two-address operations. Return [true] if the first argument and @@ -295,7 +295,7 @@ Definition type_of_operation (op: operation) : list typ * typ := match op with | Omove => (nil, Tint) (* treated specially *) | Ointconst _ => (nil, Tint) - | Ofloatconst _ => (nil, Tfloat) + | Ofloatconst f => (nil, if Float.is_single_dec f then Tsingle else Tfloat) | Oindirectsymbol _ => (nil, Tint) | Ocast8signed => (Tint :: nil, Tint) | Ocast8unsigned => (Tint :: nil, Tint) @@ -331,7 +331,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Osubf => (Tfloat :: Tfloat :: nil, Tfloat) | Omulf => (Tfloat :: Tfloat :: nil, Tfloat) | Odivf => (Tfloat :: Tfloat :: nil, Tfloat) - | Osingleoffloat => (Tfloat :: nil, Tfloat) + | Osingleoffloat => (Tfloat :: nil, Tsingle) | Ointoffloat => (Tfloat :: nil, Tint) | Ofloatofint => (Tint :: nil, Tfloat) | Omakelong => (Tint :: Tint :: nil, Tlong) @@ -377,7 +377,7 @@ Proof with (try exact I). destruct op; simpl in H0; FuncInv; subst; simpl. congruence. exact I. - exact I. + destruct (Float.is_single_dec f); auto. unfold symbol_address; destruct (Genv.find_symbol genv i)... destruct v0... destruct v0... @@ -416,7 +416,7 @@ Proof with (try exact I). destruct v0; destruct v1... destruct v0; destruct v1... destruct v0; destruct v1... - destruct v0... + destruct v0... apply Float.singleoffloat_is_single. destruct v0; simpl in H0; inv H0. destruct (Float.intoffloat f); inv H2... destruct v0; simpl in H0; inv H0... destruct v0; destruct v1... @@ -425,19 +425,6 @@ Proof with (try exact I). destruct (eval_condition c vl m); simpl... destruct b... Qed. -Lemma type_of_chunk_correct: - forall chunk m addr v, - Mem.loadv chunk m addr = Some v -> - Val.has_type v (type_of_chunk chunk). -Proof. - intro chunk. - assert (forall v, Val.has_type (Val.load_result chunk v) (type_of_chunk chunk)). - destruct v; destruct chunk; exact I. - intros until v. unfold Mem.loadv. - destruct addr; intros; try discriminate. - eapply Mem.load_type; eauto. -Qed. - End SOUNDNESS. (** * Manipulating and transforming operations *) diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 5ee4d010..88205155 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -281,7 +281,7 @@ let print_annot_val oc txt args res = | [IR src], [IR dst] -> if dst <> src then fprintf oc " movl %a, %a\n" ireg src ireg dst | [FR src], [FR dst] -> - if dst <> src then fprintf oc " movsd %a, %a\n" freg src freg dst + if dst <> src then fprintf oc " movapd %a, %a\n" freg src freg dst | _, _ -> assert false (* Handling of memcpy *) @@ -442,7 +442,7 @@ let print_builtin_inline oc name args res = | "__builtin_fabs", [FR a1], [FR res] -> need_masks := true; if a1 <> res then - fprintf oc " movsd %a, %a\n" freg a1 freg res; + fprintf oc " movapd %a, %a\n" freg a1 freg res; fprintf oc " andpd %a, %a\n" raw_symbol "__absd_mask" freg res | "__builtin_fsqrt", [FR a1], [FR res] -> fprintf oc " sqrtsd %a, %a\n" freg a1 freg res @@ -452,7 +452,7 @@ let print_builtin_inline oc name args res = else if res = a2 then fprintf oc " maxsd %a, %a\n" freg a1 freg res else begin - fprintf oc " movsd %a, %a\n" freg a1 freg res; + fprintf oc " movapd %a, %a\n" freg a1 freg res; fprintf oc " maxsd %a, %a\n" freg a2 freg res end | "__builtin_fmin", [FR a1; FR a2], [FR res] -> @@ -461,7 +461,7 @@ let print_builtin_inline oc name args res = else if res = a2 then fprintf oc " minsd %a, %a\n" freg a1 freg res else begin - fprintf oc " movsd %a, %a\n" freg a1 freg res; + fprintf oc " movapd %a, %a\n" freg a1 freg res; fprintf oc " minsd %a, %a\n" freg a2 freg res end (* 64-bit integer arithmetic *) @@ -531,10 +531,6 @@ let print_instruction oc = function fprintf oc " movl %a, %a\n" addressing a ireg rd | Pmov_mr(a, r1) -> fprintf oc " movl %a, %a\n" ireg r1 addressing a - | Pmovd_fr(rd, r1) -> - fprintf oc " movd %a, %a\n" ireg r1 freg rd - | Pmovd_rf(rd, r1) -> - fprintf oc " movd %a, %a\n" freg r1 ireg rd | Pmovsd_ff(rd, r1) -> fprintf oc " movapd %a, %a\n" freg r1 freg rd | Pmovsd_fi(rd, n) -> diff --git a/ia32/standard/Conventions1.v b/ia32/standard/Conventions1.v index cae20f6e..e097e855 100644 --- a/ia32/standard/Conventions1.v +++ b/ia32/standard/Conventions1.v @@ -220,7 +220,7 @@ Definition loc_result (s: signature) : list mreg := match s.(sig_res) with | None => AX :: nil | Some Tint => AX :: nil - | Some Tfloat => FP0 :: nil + | Some (Tfloat | Tsingle) => FP0 :: nil | Some Tlong => DX :: AX :: nil end. @@ -261,6 +261,7 @@ Fixpoint loc_arguments_rec | nil => nil | Tint :: tys => S Outgoing ofs Tint :: loc_arguments_rec tys (ofs + 1) | Tfloat :: tys => S Outgoing ofs Tfloat :: loc_arguments_rec tys (ofs + 2) + | Tsingle :: tys => S Outgoing ofs Tsingle :: loc_arguments_rec tys (ofs + 1) | Tlong :: tys => S Outgoing (ofs + 1) Tint :: S Outgoing ofs Tint :: loc_arguments_rec tys (ofs + 2) end. @@ -314,6 +315,9 @@ Proof. destruct H. subst l; split; [omega|congruence]. exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega. +- destruct H. subst l. split. omega. congruence. + exploit IHtyl; eauto. + destruct l; auto. destruct sl; auto. intuition omega. Qed. Lemma loc_arguments_acceptable: @@ -362,6 +366,7 @@ Proof. destruct H. inv H. simpl typesize. apply Zle_trans with (ofs + 2). omega. apply size_arguments_rec_above. auto. + destruct H. inv H. apply size_arguments_rec_above. auto. Qed. |