diff --git a/Makefile b/Makefile index e96cb5e3ce..769840062b 100644 --- a/Makefile +++ b/Makefile @@ -86,7 +86,8 @@ BACKEND=\ CSEdomain.v CombineOp.v CSE.v CombineOpproof.v CSEproof.v \ NeedDomain.v NeedOp.v Deadcode.v Deadcodeproof.v \ Unusedglob.v Unusedglobproof.v \ - Machregs.v Locations.v Conventions1.v Conventions.v LTL.v \ + Machregs.v Locations.v Conventions1.v Conventions.v \ + LTL.v LTLtyping.v \ Allocation.v Allocproof.v \ Tunneling.v Tunnelingproof.v \ Linear.v Lineartyping.v \ diff --git a/arm/Asm.v b/arm/Asm.v index 85eb94c18e..1b32bd1a3e 100644 --- a/arm/Asm.v +++ b/arm/Asm.v @@ -323,11 +323,11 @@ Definition set_pair (p: rpair preg) (v: val) (rs: regset) : regset := (** Assigning the result of a builtin *) -Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset := +Definition set_res (res: builtin_res preg) (v: val) (rs: regset) : regset := match res with | BR r => rs#r <- v | BR_none => rs - | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs) + | BR_splitlong hi lo => rs #hi <- (Val.hiword v) #lo <- (Val.loword v) end. Section RELSEM. diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml index 04b4152d04..3054b2d0be 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -188,7 +188,7 @@ let expand_builtin_vload_common chunk base ofs res = emit (Pldrsh (res, base, SOimm ofs)) | Mint32, BR(IR res) -> emit (Pldr (res, base, SOimm ofs)) - | Mint64, BR_splitlong(BR(IR res1), BR(IR res2)) -> + | Mint64, BR_splitlong(IR res1, IR res2) -> let ofs_hi = if Archi.big_endian then ofs else Int.add ofs _4 in let ofs_lo = if Archi.big_endian then Int.add ofs _4 else ofs in if base <> res2 then begin @@ -351,7 +351,7 @@ let expand_builtin_inline name args res = emit (Pfsqrt (res,a1)) (* 64-bit integer arithmetic *) | "__builtin_negl", [BA_splitlong(BA(IR ah), BA(IR al))], - BR_splitlong(BR(IR rh), BR(IR rl)) -> + BR_splitlong(IR rh, IR rl) -> expand_int64_arith (rl = ah ) rl (fun rl -> emit (Prsbs (rl,al,SOimm _0)); (* No "rsc" instruction in Thumb2. Emulate based on @@ -365,20 +365,20 @@ let expand_builtin_inline name args res = end) | "__builtin_addl", [BA_splitlong(BA(IR ah), BA(IR al)); BA_splitlong(BA(IR bh), BA(IR bl))], - BR_splitlong(BR(IR rh), BR(IR rl)) -> + BR_splitlong(IR rh, IR rl) -> expand_int64_arith (rl = ah || rl = bh) rl (fun rl -> emit (Padds (rl,al,SOreg bl)); emit (Padc (rh,ah,SOreg bh))) | "__builtin_subl", [BA_splitlong(BA(IR ah), BA(IR al)); BA_splitlong(BA(IR bh), BA(IR bl))], - BR_splitlong(BR(IR rh), BR(IR rl)) -> + BR_splitlong(IR rh, IR rl) -> expand_int64_arith (rl = ah || rl = bh) rl (fun rl -> emit (Psubs (rl,al,SOreg bl)); emit (Psbc (rh,ah,SOreg bh))) | "__builtin_mull", [BA(IR a); BA(IR b)], - BR_splitlong(BR(IR rh), BR(IR rl)) -> + BR_splitlong(IR rh, IR rl) -> emit (Pumull (rl,rh,a,b)) (* Memory accesses *) | "__builtin_read16_reversed", [BA(IR a1)], BR(IR res) -> diff --git a/arm/Conventions1.v b/arm/Conventions1.v index c5277e8dca..71ece2d6d5 100644 --- a/arm/Conventions1.v +++ b/arm/Conventions1.v @@ -16,6 +16,7 @@ Require Import Coqlib. Require Import Decidableplus. Require Import AST. +Require Import Values. Require Import Events. Require Import Locations. Require Archi. @@ -122,6 +123,17 @@ Proof. intros. unfold proj_sig_res, loc_result. destruct (sig_res sig) as [[]|]; destruct Archi.big_endian; auto. Qed. +Lemma loc_result_has_type: + forall res sig, + Val.has_type res (proj_sig_res sig) -> + Val.has_type_rpair res (loc_result sig) Val.loword Val.hiword mreg_type. +Proof. + intros. unfold Val.has_type_rpair, loc_result, proj_sig_res in *. + destruct sig; simpl. destruct sig_res; simpl in H. + destruct t, res, Archi.big_endian; simpl; auto. + destruct res; simpl; auto. +Qed. + (** The result locations are caller-save registers *) Lemma loc_result_caller_save: diff --git a/arm/Op.v b/arm/Op.v index 60c214d082..b22dc688a0 100644 --- a/arm/Op.v +++ b/arm/Op.v @@ -557,6 +557,17 @@ Proof. intros; discriminate. Qed. +Lemma is_not_move_operation: + forall (F V A: Type) (genv: Genv.t F V) (sp: val) + (op: operation) (f: A -> val) (args: list A) (m: mem) (v: val), + eval_operation genv sp op (map f args) m = Some v -> + is_move_operation op args = None -> + op <> Omove. +Proof. + intros. destruct (eq_operation op Omove); auto. + subst. destruct args; try destruct args; simpl in *; congruence. +Qed. + (** [negate_condition cond] returns a condition that is logically equivalent to the negation of [cond]. *) diff --git a/backend/Allocation.v b/backend/Allocation.v index cf62295dde..c8cbc87d65 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -16,7 +16,7 @@ Require Import FSets FSetAVLplus. Require Import Coqlib Ordered Maps Errors Integers Floats. Require Import AST Lattice Kildall Memdata. Require Archi. -Require Import Op Registers RTL Locations Conventions RTLtyping LTL. +Require Import Op Registers RTL Locations Conventions RTLtyping LTL LTLtyping. (** The validation algorithm used here is described in "Validating register allocation and spilling", @@ -847,8 +847,10 @@ Definition remove_equations_builtin_res (env: regenv) (res: builtin_res reg) (res': builtin_res mreg) (e: eqs) : option eqs := match res, res' with | BR r, BR r' => Some (remove_equation (Eq Full r (R r')) e) - | BR r, BR_splitlong (BR rhi) (BR rlo) => + | BR r, BR_splitlong rhi rlo => assertion (typ_eq (env r) Tlong); + assertion (subtype Tint (mreg_type rhi)); + assertion (subtype Tint (mreg_type rlo)); if mreg_eq rhi rlo then None else Some (remove_equation (Eq Low r (R rlo)) (remove_equation (Eq High r (R rhi)) e)) @@ -932,12 +934,6 @@ Definition destroyed_by_move (src dst: loc) := | _, _ => destroyed_by_op Omove end. -Definition well_typed_move (env: regenv) (dst: loc) (e: eqs) : bool := - match dst with - | R r => true - | S sl ofs ty => loc_type_compat env dst e - end. - (** Simulate the effect of a sequence of moves [mv] on a set of equations [e]. The set [e] is the equations that must hold after the sequence of moves. Return the set of equations that @@ -950,7 +946,7 @@ Fixpoint track_moves (env: regenv) (mv: moves) (e: eqs) : option eqs := | MV src dst :: mv => do e1 <- track_moves env mv e; assertion (can_undef_except dst (destroyed_by_move src dst)) e1; - assertion (well_typed_move env dst e1); + assertion (loc_type_compat env dst e1); subst_loc dst src e1 | MVmakelong src1 src2 dst :: mv => assertion (negb Archi.ptr64); @@ -1359,7 +1355,11 @@ Definition transf_function (f: RTL.function) : res LTL.function := | OK env => match regalloc f with | Error m => Error m - | OK tf => do x <- check_function f tf env; OK tf + | OK tf => + if wt_function tf then + do x <- check_function f tf env; OK tf + else + Error (msg "Ill-typed LTL code") end end. diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 4b75e34d4e..de48a33e11 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -18,6 +18,7 @@ Require Import Coqlib Ordered Maps Errors Integers Floats. Require Import AST Linking Lattice Kildall. Require Import Values Memory Globalenvs Events Smallstep. Require Archi. +Require Import LTLtyping. Require Import Op Registers RTL Locations Conventions RTLtyping LTL. Require Import Allocation. @@ -214,7 +215,8 @@ Proof. Qed. Lemma extract_moves_sound: - forall b mv b', + forall f b mv b', + wt_bblock f b = true -> extract_moves nil b = (mv, b') -> wf_moves mv /\ b = expand_moves mv b'. Proof. @@ -225,18 +227,19 @@ Proof. { intros; split; auto. unfold wf_moves in *; rewrite Forall_forall in *. intros. apply H. rewrite <- in_rev in H0; auto. } - assert (IND: forall b accu mv b', + assert (IND: forall f b accu mv b', + wt_bblock f b = true -> extract_moves accu b = (mv, b') -> wf_moves accu -> wf_moves mv /\ expand_moves (List.rev accu) b = expand_moves mv b'). { induction b; simpl; intros. - - inv H. auto. - - destruct a; try (inv H; apply BASE; auto; fail). + - inv H0. auto. + - destruct a; try (inv H0; apply BASE; auto; fail); simpl in H; InvBooleans. + destruct (is_move_operation op args) as [arg|] eqn:E. exploit is_move_operation_correct; eauto. intros [A B]; subst. (* reg-reg move *) exploit IHb; eauto. constructor; auto. exact I. rewrite expand_moves_cons; auto. - inv H; apply BASE; auto. + inv H0; apply BASE; auto. + (* stack-reg move *) exploit IHb; eauto. constructor; auto. exact I. rewrite expand_moves_cons; auto. + (* reg-stack move *) @@ -246,7 +249,8 @@ Proof. Qed. Lemma extract_moves_ext_sound: - forall b mv b', + forall f b mv b', + wt_bblock f b = true -> extract_moves_ext nil b = (mv, b') -> wf_moves mv /\ b = expand_moves mv b'. Proof. @@ -257,13 +261,14 @@ Proof. { intros; split; auto. unfold wf_moves in *; rewrite Forall_forall in *. intros. apply H. rewrite <- in_rev in H0; auto. } - assert (IND: forall b accu mv b', + assert (IND: forall f b accu mv b', + wt_bblock f b = true -> extract_moves_ext accu b = (mv, b') -> wf_moves accu -> wf_moves mv /\ expand_moves (List.rev accu) b = expand_moves mv b'). { induction b; simpl; intros. - - inv H. auto. - - destruct a; try (inv H; apply BASE; auto; fail). + - inv H0. auto. + - destruct a; try (inv H0; apply BASE; auto; fail); simpl in H; InvBooleans. + destruct (classify_operation op args). * (* reg-reg move *) exploit IHb; eauto. constructor; auto. exact I. rewrite expand_moves_cons; auto. @@ -274,7 +279,7 @@ Proof. * (* highlong *) exploit IHb; eauto. constructor; auto. exact I. rewrite expand_moves_cons; auto. * (* default *) - inv H; apply BASE; auto. + inv H0; apply BASE; auto. + (* stack-reg move *) exploit IHb; eauto. constructor; auto. exact I. rewrite expand_moves_cons; auto. + (* reg-stack move *) @@ -291,12 +296,36 @@ Proof. destruct (peq s s0); simpl in H; inv H. exists b; auto. Qed. +Lemma wt_bblock_expand_moves_head: + forall f m i b, + wt_bblock f (expand_moves m (i :: b)) = true -> LTLtyping.wt_instr f i = true. +Proof. + intros. unfold expand_moves, wt_bblock in H. + rewrite forallb_app in H; InvBooleans. + simpl in H1; InvBooleans. auto. +Qed. + +Lemma wt_bblock_expand_moves_cons: + forall f m i b, + wt_bblock f (expand_moves m (i :: b)) = true -> wt_bblock f b = true. +Proof. + induction b; intros; auto. + simpl. unfold expand_moves, wt_bblock in H. + rewrite forallb_app in H; InvBooleans. + simpl in H1; InvBooleans. unfold wt_bblock. + rewrite H1, H3; auto. +Qed. + Ltac UseParsingLemmas := match goal with - | [ H: extract_moves nil _ = (_, _) |- _ ] => - destruct (extract_moves_sound _ _ _ H); clear H; subst; UseParsingLemmas - | [ H: extract_moves_ext nil _ = (_, _) |- _ ] => - destruct (extract_moves_ext_sound _ _ _ H); clear H; subst; UseParsingLemmas + | [ H: extract_moves nil ?b = (_, _), WT: wt_bblock _ ?b = true |- _ ] => + destruct (extract_moves_sound _ _ _ _ WT H); clear H; subst; UseParsingLemmas + | [ H: extract_moves nil ?b = (_, _), WT: wt_bblock _ (expand_moves _ (_ :: ?b)) = true |- _ ] => + apply wt_bblock_expand_moves_cons in WT; UseParsingLemmas + | [ H: extract_moves_ext nil ?b = (_, _), WT: wt_bblock _ ?b = true |- _ ] => + destruct (extract_moves_ext_sound _ _ _ _ WT H); clear H; subst; UseParsingLemmas + | [ H: extract_moves_ext nil ?b = (_, _), WT: wt_bblock _ (expand_moves _ (_ :: ?b)) = true |- _ ] => + apply wt_bblock_expand_moves_cons in WT; UseParsingLemmas | [ H: check_succ _ _ = true |- _ ] => try (discriminate H); destruct (check_succ_sound _ _ H); clear H; subst; UseParsingLemmas @@ -304,19 +333,21 @@ Ltac UseParsingLemmas := end. Lemma pair_instr_block_sound: - forall i b bsh, + forall i f b bsh, + wt_bblock f b = true -> pair_instr_block i b = Some bsh -> expand_block_shape bsh i b. Proof. - assert (OP: forall op args res s b bsh, + assert (OP: forall op args res s f b bsh, + wt_bblock f b = true -> pair_Iop_block op args res s b = Some bsh -> expand_block_shape bsh (Iop op args res s) b). { unfold pair_Iop_block; intros. MonadInv. destruct b0. MonadInv; UseParsingLemmas. destruct i; MonadInv; UseParsingLemmas. eapply ebs_op; eauto. - inv H0. eapply ebs_op_dead; eauto. } + inv H1. eapply ebs_op_dead; eauto. } - intros; destruct i; simpl in H; MonadInv; UseParsingLemmas. + intros i f b bsh WT; intros; destruct i; simpl in H; MonadInv; UseParsingLemmas. - (* nop *) econstructor; eauto. - (* op *) @@ -371,11 +402,14 @@ Lemma matching_instr_block: forall f1 f2 pc bsh i, (pair_codes f1 f2)!pc = Some bsh -> (RTL.fn_code f1)!pc = Some i -> + LTLtyping.wt_function f2 = true -> exists b, (LTL.fn_code f2)!pc = Some b /\ expand_block_shape bsh i b. Proof. intros. unfold pair_codes in H. rewrite PTree.gcombine in H; auto. rewrite H0 in H. - destruct (LTL.fn_code f2)!pc as [b|]. - exists b; split; auto. apply pair_instr_block_sound; auto. + destruct (LTL.fn_code f2)!pc as [b|] eqn:B. + exists b; split; auto. + eapply wt_function_wt_bblock in H1; eauto. + eapply pair_instr_block_sound; eauto. discriminate. Qed. @@ -685,11 +719,12 @@ Lemma loc_unconstrained_satisf: satisf rs ls (remove_equation (Eq k r l) e) -> loc_unconstrained (R mr) (remove_equation (Eq k r l) e) = true -> Val.lessdef (sel_val k rs#r) v -> + Val.has_type v (mreg_type mr) -> satisf rs (Locmap.set l v ls) e. Proof. intros; red; intros. destruct (OrderedEquation.eq_dec q (Eq k r l)). - subst q; simpl. unfold l; rewrite Locmap.gss. auto. + subst q; simpl. unfold l; rewrite Locmap.gss. rewrite Val.load_result_same; auto. assert (EqSet.In q (remove_equation (Eq k r l) e)). simpl. ESD.fsetdec. rewrite Locmap.gso. apply H; auto. eapply loc_unconstrained_sound; eauto. @@ -709,13 +744,14 @@ Lemma parallel_assignment_satisf: forall k r mr e rs ls v v', let l := R mr in Val.lessdef (sel_val k v) v' -> + Val.has_type v' (mreg_type mr) -> reg_loc_unconstrained r (R mr) (remove_equation (Eq k r l) e) = true -> satisf rs ls (remove_equation (Eq k r l) e) -> satisf (rs#r <- v) (Locmap.set l v' ls) e. Proof. intros; red; intros. destruct (OrderedEquation.eq_dec q (Eq k r l)). - subst q; simpl. unfold l; rewrite Regmap.gss; rewrite Locmap.gss; auto. + subst q; simpl. unfold l; rewrite Regmap.gss; rewrite Locmap.gss, Val.load_result_same; auto. assert (EqSet.In q (remove_equation {| ekind := k; ereg := r; eloc := l |} e)). simpl. ESD.fsetdec. exploit reg_loc_unconstrained_sound; eauto. intros [A B]. @@ -729,24 +765,25 @@ Lemma parallel_assignment_satisf_2: reg_unconstrained res e' = true -> forallb (fun l => loc_unconstrained l e') (map R (regs_of_rpair res')) = true -> Val.lessdef v v' -> + Val.has_type_rpair v' res' Val.loword Val.hiword mreg_type -> satisf (rs#res <- v) (Locmap.setpair res' v' ls) e. Proof. intros. functional inversion H. - (* One location *) subst. simpl in H2. InvBooleans. simpl. apply parallel_assignment_satisf with Full; auto. - unfold reg_loc_unconstrained. rewrite H1, H4. auto. + unfold reg_loc_unconstrained. rewrite H1, H5. auto. - (* Two 32-bit halves *) - subst. + subst. destruct H4. set (e' := remove_equation {| ekind := Low; ereg := res; eloc := R mr2 |} (remove_equation {| ekind := High; ereg := res; eloc := R mr1 |} e)) in *. simpl in H2. InvBooleans. simpl. red; intros. destruct (OrderedEquation.eq_dec q (Eq Low res (R mr2))). - subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gss. + subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gss, Val.load_result_same by auto. apply Val.loword_lessdef; auto. destruct (OrderedEquation.eq_dec q (Eq High res (R mr1))). - subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gso by auto. rewrite Locmap.gss. + subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gso, Locmap.gss, Val.load_result_same by auto. apply Val.hiword_lessdef; auto. assert (EqSet.In q e'). unfold e', remove_equation; simpl; ESD.fsetdec. rewrite Regmap.gso. rewrite ! Locmap.gso. auto. @@ -1007,19 +1044,14 @@ Proof. exact (select_loc_h_monotone l). Qed. -Lemma well_typed_move_charact: +Lemma loc_type_compat_well_typed: forall env l e k r rs, - well_typed_move env l e = true -> + loc_type_compat env l e = true -> EqSet.In (Eq k r l) e -> wt_regset env rs -> - match l with - | R mr => True - | S sl ofs ty => Val.has_type (sel_val k rs#r) ty - end. + Val.has_type (sel_val k rs#r) (Loc.type l). Proof. - unfold well_typed_move; intros. - destruct l as [mr | sl ofs ty]. - auto. + intros. exploit loc_type_compat_charact; eauto. intros [A | A]. simpl in A. eapply Val.has_subtype; eauto. generalize (H1 r). destruct k; simpl; intros. @@ -1040,8 +1072,9 @@ Qed. Lemma subst_loc_satisf: forall env src dst rs ls e e', subst_loc dst src e = Some e' -> - well_typed_move env dst e = true -> + loc_type_compat env dst e = true -> wt_regset env rs -> + Val.has_type (ls src) (Loc.type dst) -> satisf rs ls e' -> satisf rs (Locmap.set dst (ls src) ls) e. Proof. @@ -1049,10 +1082,8 @@ Proof. exploit in_subst_loc; eauto. intros [[A B] | [A B]]. subst dst. rewrite Locmap.gss. destruct q as [k r l]; simpl in *. - exploit well_typed_move_charact; eauto. - destruct l as [mr | sl ofs ty]; intros. - apply (H2 _ B). - apply val_lessdef_normalize; auto. apply (H2 _ B). + exploit loc_type_compat_well_typed; eauto. + intro. rewrite Val.load_result_same by auto. apply (H3 _ B). rewrite Locmap.gso; auto. Qed. @@ -1107,24 +1138,28 @@ Qed. Lemma subst_loc_part_satisf_lowlong: forall src dst rs ls e e', subst_loc_part (R dst) (R src) Low e = Some e' -> + Val.has_type (Val.loword (ls (R src))) (mreg_type dst) -> satisf rs ls e' -> satisf rs (Locmap.set (R dst) (Val.loword (ls (R src))) ls) e. Proof. intros; red; intros. exploit in_subst_loc_part; eauto. intros [[A [B C]] | [A B]]. - rewrite A, B. apply H0 in C. rewrite Locmap.gss. apply Val.loword_lessdef. exact C. + rewrite A, B. apply H1 in C. rewrite Locmap.gss, Val.load_result_same by auto. + apply Val.loword_lessdef. exact C. rewrite Locmap.gso; auto. Qed. Lemma subst_loc_part_satisf_highlong: forall src dst rs ls e e', subst_loc_part (R dst) (R src) High e = Some e' -> + Val.has_type (Val.hiword (ls (R src))) (mreg_type dst) -> satisf rs ls e' -> satisf rs (Locmap.set (R dst) (Val.hiword (ls (R src))) ls) e. Proof. intros; red; intros. exploit in_subst_loc_part; eauto. intros [[A [B C]] | [A B]]. - rewrite A, B. apply H0 in C. rewrite Locmap.gss. apply Val.hiword_lessdef. exact C. + rewrite A, B. apply H1 in C. rewrite Locmap.gss, Val.load_result_same by auto. + apply Val.hiword_lessdef. exact C. rewrite Locmap.gso; auto. Qed. @@ -1206,6 +1241,7 @@ Lemma subst_loc_pair_satisf_makelong: wt_regset env rs -> satisf rs ls e' -> Archi.ptr64 = false -> + Val.has_type (Val.longofwords (ls (R src1)) (ls (R src2))) (mreg_type dst) -> satisf rs (Locmap.set (R dst) (Val.longofwords (ls (R src1)) (ls (R src2))) ls) e. Proof. intros; red; intros. @@ -1214,7 +1250,8 @@ Proof. assert (subtype (env (ereg q)) Tlong = true). { exploit long_type_compat_charact; eauto. intros [P|P]; auto. eelim Loc.diff_not_eq; eauto. } - rewrite Locmap.gss. simpl. rewrite <- (val_longofwords_eq_1 rs#(ereg q)). + rewrite Locmap.gss, Val.load_result_same by auto. + simpl. rewrite <- (val_longofwords_eq_1 rs#(ereg q)). apply Val.longofwords_lessdef. exact C. exact D. eapply Val.has_subtype; eauto. assumption. @@ -1266,7 +1303,7 @@ Qed. Lemma subst_loc_undef_satisf: forall env src dst rs ls ml e e', subst_loc dst src e = Some e' -> - well_typed_move env dst e = true -> + loc_type_compat env dst e = true -> can_undef_except dst ml e = true -> wt_regset env rs -> satisf rs ls e' -> @@ -1276,9 +1313,7 @@ Proof. exploit in_subst_loc; eauto. intros [[A B] | [A B]]. subst dst. rewrite Locmap.gss. destruct q as [k r l]; simpl in *. - exploit well_typed_move_charact; eauto. - destruct l as [mr | sl ofs ty]; intros. - apply (H3 _ B). + exploit loc_type_compat_well_typed; eauto. intros. apply val_lessdef_normalize; auto. apply (H3 _ B). rewrite Locmap.gso; auto. rewrite undef_regs_outside. eauto. eapply can_undef_except_sound; eauto. apply Loc.diff_sym; auto. @@ -1289,7 +1324,7 @@ Lemma transfer_use_def_satisf: transfer_use_def args res args' res' und e = Some e' -> satisf rs ls e' -> Val.lessdef_list rs##args (reglist ls args') /\ - (forall v v', Val.lessdef v v' -> + (forall v v', Val.lessdef v v' -> Val.has_type v' (mreg_type res') -> satisf (rs#res <- v) (Locmap.set (R res') v' (undef_regs und ls)) e). Proof. unfold transfer_use_def; intros. MonadInv. @@ -1675,22 +1710,28 @@ Lemma parallel_set_builtin_res_satisf: forallb (fun mr => loc_unconstrained (R mr) e1) (params_of_builtin_res res') = true -> satisf rs ls e1 -> Val.lessdef v v' -> + Val.has_type_builtin_res v' res' Val.loword Val.hiword mreg_type -> satisf (regmap_setres res v rs) (Locmap.setres res' v' ls) e0. Proof. intros. rewrite forallb_forall in *. destruct res, res'; simpl in *; inv H. - apply parallel_assignment_satisf with (k := Full); auto. unfold reg_loc_unconstrained. rewrite H0 by auto. rewrite H1 by auto. auto. -- destruct res'1; try discriminate. destruct res'2; try discriminate. - rename x0 into hi; rename x1 into lo. MonadInv. destruct (mreg_eq hi lo); inv H5. - set (e' := remove_equation {| ekind := High; ereg := x; eloc := R hi |} e0) in *. +- set (e' := remove_equation {| ekind := High; ereg := x; eloc := R hi |} e0) in *. set (e'' := remove_equation {| ekind := Low; ereg := x; eloc := R lo |} e') in *. - simpl in *. red; intros. + red; intros. + assert (subtype Tint (mreg_type hi) = true /\ + subtype Tint (mreg_type lo) = true /\ + lo <> hi /\ e'' = e1). + { destruct (typ_eq (env x) Tlong), (mreg_eq hi lo), (mreg_type hi), (mreg_type lo); + try inversion H6; auto. } + decompose [and] H4. decompose [and] H5; subst. destruct (OrderedEquation.eq_dec q (Eq Low x (R lo))). - subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gss. apply Val.loword_lessdef; auto. + subst q; simpl. rewrite Regmap.gss. + rewrite Locmap.gss, Val.load_result_same; auto. apply Val.loword_lessdef; auto. destruct (OrderedEquation.eq_dec q (Eq High x (R hi))). subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gso by (red; auto). - rewrite Locmap.gss. apply Val.hiword_lessdef; auto. + rewrite Locmap.gss, Val.load_result_same; auto. apply Val.hiword_lessdef; auto. assert (EqSet.In q e''). { unfold e'', e', remove_equation; simpl; ESD.fsetdec. } rewrite Regmap.gso. rewrite ! Locmap.gso. auto. @@ -1754,12 +1795,14 @@ Proof. unfold transf_function; intros. destruct (type_function f) as [env|] eqn:TY; try discriminate. destruct (regalloc f); try discriminate. + destruct (LTLtyping.wt_function f0) eqn:WT; try discriminate. destruct (check_function f f0 env) as [] eqn:?; inv H. unfold check_function in Heqr. destruct (analyze f env (pair_codes f tf)) as [an|] eqn:?; try discriminate. monadInv Heqr. destruct (check_entrypoints_aux f tf env x) as [y|] eqn:?; try discriminate. unfold check_entrypoints_aux, pair_entrypoints in Heqo0. MonadInv. + eapply wt_function_wt_bblock in WT; eauto. exploit extract_moves_ext_sound; eauto. intros [A B]. subst b. exploit check_succ_sound; eauto. intros [k EQ1]. subst b0. econstructor; eauto. eapply type_function_correct; eauto. congruence. @@ -1768,6 +1811,7 @@ Qed. Lemma invert_code: forall f env tf pc i opte e, wt_function f env -> + LTLtyping.wt_function tf = true -> (RTL.fn_code f)!pc = Some i -> transfer f env (pair_codes f tf) pc opte = OK e -> exists eafter, exists bsh, exists bb, @@ -1778,10 +1822,10 @@ Lemma invert_code: transfer_aux f env bsh eafter = Some e /\ wt_instr f env i. Proof. - intros. destruct opte as [eafter|]; simpl in H1; try discriminate. exists eafter. + intros. destruct opte as [eafter|]; simpl in H2; try discriminate. exists eafter. destruct (pair_codes f tf)!pc as [bsh|] eqn:?; try discriminate. exists bsh. exploit matching_instr_block; eauto. intros [bb [A B]]. - destruct (transfer_aux f env bsh eafter) as [e1|] eqn:?; inv H1. + destruct (transfer_aux f env bsh eafter) as [e1|] eqn:?; inv H2. exists bb. exploit wt_instr_at; eauto. tauto. Qed. @@ -1854,44 +1898,75 @@ Lemma exec_moves: wf_moves mv -> satisf rs ls e' -> wt_regset env rs -> + LTLtyping.wt_locset ls /\ LTLtyping.wt_bblock f (expand_moves mv bb) = true -> exists ls', - star step tge (Block s f sp (expand_moves mv bb) ls m) - E0 (Block s f sp bb ls' m) + star step tge (Block s f sp (expand_moves mv bb) ls m) + E0 (Block s f sp bb ls' m) + /\ LTLtyping.wt_locset ls' /\ satisf rs ls' e. Proof. Opaque destroyed_by_op. induction mv; simpl; intros. (* base *) -- unfold expand_moves; simpl. inv H. exists ls; split. apply star_refl. auto. +- unfold expand_moves; simpl. inv H. exists ls; split. apply star_refl. tauto. (* step *) - assert (wf_moves mv) by (inv H0; auto). destruct a; unfold expand_moves; simpl; MonadInv. + (* loc-loc move *) - destruct src as [rsrc | ssrc]; destruct dst as [rdst | sdst]. + destruct H3. destruct src as [rsrc | ssrc]; destruct dst as [rdst | sdst]. * (* reg-reg *) exploit IHmv; eauto. eapply subst_loc_undef_satisf; eauto. + InvBooleans. split; eauto. apply wt_setreg. + apply Val.has_subtype with (ty1 := mreg_type rsrc); auto. apply H3. + apply wt_undef_regs. auto. intros [ls' [A B]]. exists ls'; split; auto. eapply star_left; eauto. econstructor. simpl. eauto. auto. auto. * (* reg->stack *) exploit IHmv; eauto. eapply subst_loc_undef_satisf; eauto. + InvBooleans. split; eauto. apply wt_setstack, wt_undef_regs. auto. intros [ls' [A B]]. exists ls'; split; auto. eapply star_left; eauto. econstructor. simpl. eauto. auto. * (* stack->reg *) simpl in Heqb. exploit IHmv; eauto. eapply subst_loc_undef_satisf; eauto. + InvBooleans. split; eauto. apply wt_setreg, wt_undef_regs. auto. + apply Val.has_subtype with (ty1 := ty); auto. simpl in H6. InvBooleans; auto. + apply H3. auto. intros [ls' [A B]]. exists ls'; split; auto. eapply star_left; eauto. econstructor. auto. auto. * (* stack->stack *) - inv H0. simpl in H6. contradiction. + inv H0. simpl in H8. contradiction. + (* makelong *) + assert (HT: Val.has_type (Val.longofwords (ls (R src1)) (ls (R src2))) (mreg_type dst)). + { + destruct H3; InvBooleans. simpl in H6. + destruct (mreg_type dst) eqn:T; simpl; auto; inversion H6. + destruct (ls (R src1)), (ls (R src2)); simpl; auto. + destruct (ls (R src1)), (ls (R src2)); simpl; auto. + } exploit IHmv; eauto. eapply subst_loc_pair_satisf_makelong; eauto. + destruct H3; InvBooleans. split; eauto using wt_setreg. intros [ls' [A B]]. exists ls'; split; auto. eapply star_left; eauto. econstructor. simpl; eauto. reflexivity. traceEq. + (* lowlong *) + assert (HT: Val.has_type (Val.loword (ls (R src))) (mreg_type dst)). + { + destruct H3. simpl in H5. InvBooleans. + destruct (mreg_type dst) eqn:T; simpl; auto; inversion H6; + destruct (ls (R src)); simpl; auto. + } exploit IHmv; eauto. eapply subst_loc_part_satisf_lowlong; eauto. + destruct H3; InvBooleans. split; eauto using wt_setreg. intros [ls' [A B]]. exists ls'; split; auto. eapply star_left; eauto. econstructor. simpl; eauto. reflexivity. traceEq. + (* highlong *) + assert (HT: Val.has_type (Val.hiword (ls (R src))) (mreg_type dst)). + { + destruct H3. simpl in H5. InvBooleans. + destruct (mreg_type dst) eqn:T; simpl; auto; inversion H6; + destruct (ls (R src)); simpl; auto. + } exploit IHmv; eauto. eapply subst_loc_part_satisf_highlong; eauto. + destruct H3; InvBooleans. split; eauto using wt_setreg. intros [ls' [A B]]. exists ls'; split; auto. eapply star_left; eauto. econstructor. simpl; eauto. reflexivity. traceEq. Qed. @@ -1915,6 +1990,7 @@ Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> signa Val.lessdef v (Locmap.getpair (map_rpair R (loc_result sg)) ls1) -> Val.has_type v (env res) -> agree_callee_save ls ls1 -> + wt_locset ls1 -> exists ls2, star LTL.step tge (Block ts tf sp bb ls1 m) E0 (State ts tf sp pc ls2 m) @@ -1972,11 +2048,25 @@ Qed. Ltac UseShape := match goal with - | [ WT: wt_function _ _, CODE: (RTL.fn_code _)!_ = Some _, EQ: transfer _ _ _ _ _ = OK _ |- _ ] => - destruct (invert_code _ _ _ _ _ _ _ WT CODE EQ) as (eafter & bsh & bb & AFTER & BSH & TCODE & EBS & TR & WTI); + | [ WT: wt_function _ _, + WTTF: LTLtyping.wt_function _ = true, + CODE: (RTL.fn_code _)!_ = Some _, + EQ: transfer _ _ _ _ _ = OK _ |- _ ] => + destruct (invert_code _ _ _ _ _ _ _ WT WTTF CODE EQ) as (eafter & bsh & bb & AFTER & BSH & TCODE & EBS & TR & WTI); inv EBS; unfold transfer_aux in TR; MonadInv end. +Ltac WellTypedBlock := + match goal with + | [ T: (fn_code ?tf) ! _ = Some _ |- wt_bblock _ _ = true ] => + apply wt_function_wt_bblock in T; try eassumption; + unfold wt_bblock, expand_moves in *; try eassumption; WellTypedBlock + | [ T: forallb (LTLtyping.wt_instr _) (_ ++ _) = true |- forallb _ _ = true ] => + rewrite forallb_app in T; simpl in T; + InvBooleans; try eassumption; WellTypedBlock + | _ => idtac + end. + Remark addressing_not_long: forall env f addr args dst s r, wt_instr f env (Iload Mint64 addr args dst s) -> Archi.splitlong = true -> @@ -1992,41 +2082,107 @@ Proof. red; intros; subst r. rewrite C in H8; discriminate. Qed. +Lemma wt_transf_function: + forall (f: RTL.function) (tf: LTL.function), + transf_function f = OK tf -> + LTLtyping.wt_function tf = true. +Proof. + intros. unfold transf_function in H. + destruct (type_function f); try congruence. + destruct (regalloc f); try congruence. + destruct (LTLtyping.wt_function f0) eqn:WT; try congruence. + monadInv H; auto. +Qed. + +Lemma wt_transf_fundef: + forall (fd: RTL.fundef) (tfd: LTL.fundef), + transf_fundef fd = OK tfd -> + LTLtyping.wt_fundef tfd. +Proof. + intros. + destruct fd, tfd; simpl in *; auto; try congruence. + monadInv H. simpl; eauto using wt_transf_function. +Qed. + +Lemma wt_prog: wt_program prog. +Proof. + red; intros. + exploit list_forall2_in_left. eexact (proj1 TRANSF). eauto. + intros ([i' gd] & A & B & C). simpl in *; subst i'. + inv C. destruct f; simpl in *. +- monadInv H2. + unfold transf_function in EQ. + destruct (type_function f) as [env|] eqn:TF; try discriminate. + econstructor. eapply type_function_correct; eauto. +- constructor. +Qed. + +Corollary wt_tprog: LTLtyping.wt_program tprog. +Proof. + generalize wt_prog; unfold wt_program; intros. + unfold LTLtyping.wt_program; intros. + unfold match_prog, match_program, match_program_gen in TRANSF. + decompose [and] TRANSF. + exploit list_forall2_in_right; eauto. + intros ([i' gd] & A & B & C). + inversion C. eapply wt_transf_fundef. eauto. +Qed. + +Lemma star_step_type_preservation: + forall S1 t S2, + LTLtyping.wt_state S1 -> + star LTL.step tge S1 t S2 -> + LTLtyping.wt_state S2. +Proof. + intros. induction H0; auto. + apply IHstar. eapply LTLtyping.step_type_preservation; eauto. + eapply wt_tprog. +Qed. + (** The proof of semantic preservation is a simulation argument of the "plus" kind. *) Lemma step_simulation: forall S1 t S2, RTL.step ge S1 t S2 -> wt_state S1 -> - forall S1', match_states S1 S1' -> - exists S2', plus LTL.step tge S1' t S2' /\ match_states S2 S2'. + forall S1', match_states S1 S1' -> LTLtyping.wt_state S1' -> + exists S2', plus LTL.step tge S1' t S2' /\ LTLtyping.wt_state S2' /\ match_states S2 S2'. Proof. - induction 1; intros WT S1' MS; inv MS; try UseShape. + induction 1; intros WT S1' MS WT'; inv MS; + try assert (WTTF: LTLtyping.wt_function tf = true) by (inversion WT'; auto); + inversion WT'; subst; + try UseShape. (* nop *) -- exploit exec_moves; eauto. intros [ls1 [X Y]]. +- exploit exec_moves; eauto. + split; eauto using LTLtyping.wt_function_wt_bblock. + intros [ls1 [X [Y Z]]]. econstructor; split. eapply plus_left. econstructor; eauto. eapply star_right. eexact X. econstructor; eauto. eauto. traceEq. exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. - econstructor; eauto. + split; econstructor; eauto. (* op move *) - generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'. simpl in H0. inv H0. - exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. + exploit (exec_moves mv); eauto. + split; eauto using LTLtyping.wt_function_wt_bblock. + intros [ls1 [X [Y Z]]]. econstructor; split. eapply plus_left. econstructor; eauto. eapply star_right. eexact X. econstructor; eauto. eauto. traceEq. exploit satisf_successors; eauto. simpl; eauto. eapply subst_reg_satisf; eauto. intros [enext [U V]]. - econstructor; eauto. + split; econstructor; eauto. (* op makelong *) - generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'. simpl in H0. inv H0. - exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. + exploit (exec_moves mv); eauto. + split; eauto using LTLtyping.wt_function_wt_bblock. + intros [ls1 [X [Y Z]]]. econstructor; split. eapply plus_left. econstructor; eauto. eapply star_right. eexact X. econstructor; eauto. @@ -2034,12 +2190,14 @@ Proof. exploit satisf_successors; eauto. simpl; eauto. eapply subst_reg_kind_satisf_makelong. eauto. eauto. intros [enext [U V]]. - econstructor; eauto. + split; econstructor; eauto. (* op lowlong *) - generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'. simpl in H0. inv H0. - exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. + exploit (exec_moves mv); eauto. + split; eauto using LTLtyping.wt_function_wt_bblock. + intros [ls1 [X [Y Z]]]. econstructor; split. eapply plus_left. econstructor; eauto. eapply star_right. eexact X. econstructor; eauto. @@ -2047,12 +2205,14 @@ Proof. exploit satisf_successors; eauto. simpl; eauto. eapply subst_reg_kind_satisf_lowlong. eauto. eauto. intros [enext [U V]]. - econstructor; eauto. + split; econstructor; eauto. (* op highlong *) - generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'. simpl in H0. inv H0. - exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. + exploit (exec_moves mv); eauto. + split; eauto using LTLtyping.wt_function_wt_bblock. + intros [ls1 [X [Y Z]]]. econstructor; split. eapply plus_left. econstructor; eauto. eapply star_right. eexact X. econstructor; eauto. @@ -2060,14 +2220,31 @@ Proof. exploit satisf_successors; eauto. simpl; eauto. eapply subst_reg_kind_satisf_highlong. eauto. eauto. intros [enext [U V]]. - econstructor; eauto. + split; econstructor; eauto. (* op regular *) - generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'. - exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. + exploit (exec_moves mv1); eauto. + split; eauto using LTLtyping.wt_function_wt_bblock. + intros [ls1 [A1 [B1 C1]]]. exploit transfer_use_def_satisf; eauto. intros [X Y]. exploit eval_operation_lessdef; eauto. intros [v' [F G]]. - exploit (exec_moves mv2); eauto. intros [ls2 [A2 B2]]. + assert (RES_TYPE: Val.has_type v' (mreg_type res')). + { + generalize (LTLtyping.wt_function_wt_bblock tf pc _ WTTF TCODE); intro WTBB. + apply wt_bblock_expand_moves_head in WTBB. + simpl in WTBB. + destruct (is_move_operation op args') eqn:MOVE. + - apply is_move_operation_correct in MOVE. destruct MOVE; subst. simpl in *. + inversion F. eapply Val.has_subtype; eauto. apply B1. + - apply Val.has_subtype with (ty1 := snd (type_of_operation op)). + destruct (type_of_operation op); simpl; auto. + generalize (is_not_move_operation _ _ _ _ _ F MOVE); intros. + eapply type_of_operation_sound; eauto. + } + exploit (exec_moves mv2); eauto. + split. apply wt_setreg; auto. apply wt_undef_regs; auto. WellTypedBlock. + intros [ls2 [A2 [B2 C2]]]. econstructor; split. eapply plus_left. econstructor; eauto. eapply star_trans. eexact A1. @@ -2075,11 +2252,14 @@ Proof. apply eval_operation_preserved. exact symbols_preserved. eauto. eapply star_right. eexact A2. constructor. eauto. eauto. eauto. traceEq. - exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. - econstructor; eauto. + exploit satisf_successors; eauto. simpl; eauto. + intros [enext [U V]]. + split; econstructor; eauto. (* op dead *) -- exploit exec_moves; eauto. intros [ls1 [X Y]]. +- exploit exec_moves; eauto. + split; eauto using LTLtyping.wt_function_wt_bblock. + intros [ls1 [X [Y Z]]]. econstructor; split. eapply plus_left. econstructor; eauto. eapply star_right. eexact X. econstructor; eauto. @@ -2087,16 +2267,29 @@ Proof. exploit satisf_successors. eauto. eauto. simpl; eauto. eauto. eapply reg_unconstrained_satisf; eauto. intros [enext [U V]]. - econstructor; eauto. + split; econstructor; eauto. eapply wt_exec_Iop; eauto. (* load regular *) - generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. - exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. + exploit (exec_moves mv1); eauto. + split; eauto using LTLtyping.wt_function_wt_bblock. + intros [ls1 [A1 [B1 C1]]]. exploit transfer_use_def_satisf; eauto. intros [X Y]. exploit eval_addressing_lessdef; eauto. intros [a' [F G]]. exploit Mem.loadv_extends; eauto. intros [v' [P Q]]. - exploit (exec_moves mv2); eauto. intros [ls2 [A2 B2]]. + assert (DST_TYPE: Val.has_type v' (mreg_type dst')). + { + generalize (LTLtyping.wt_function_wt_bblock tf pc _ WTTF TCODE); intro WTBB. + apply wt_bblock_expand_moves_head in WTBB. + simpl in WTBB. + eapply Val.has_subtype; eauto. + unfold Mem.loadv in P; destruct a'; try inversion P. + eapply Mem.load_type; eauto. + } + exploit (exec_moves mv2); eauto. + split. apply wt_setreg; auto using wt_undef_regs. WellTypedBlock. + intros [ls2 [A2 [B2 C2]]]. econstructor; split. eapply plus_left. econstructor; eauto. eapply star_trans. eexact A1. @@ -2105,18 +2298,28 @@ Proof. eapply star_right. eexact A2. constructor. eauto. eauto. eauto. traceEq. exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. - econstructor; eauto. + split; econstructor; eauto. (* load pair *) - generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2). set (v2' := if Archi.big_endian then v2 else v1) in *. set (v1' := if Archi.big_endian then v1 else v2) in *. - exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. + exploit (exec_moves mv1); eauto. + split; eauto using LTLtyping.wt_function_wt_bblock. + intros [ls1 [A1 [B1 C1]]]. assert (LD1: Val.lessdef_list rs##args (reglist ls1 args1')). { eapply add_equations_lessdef; eauto. } exploit eval_addressing_lessdef. eexact LD1. eauto. intros [a1' [F1 G1]]. exploit Mem.loadv_extends. eauto. eexact LOAD1. eexact G1. intros (v1'' & LOAD1' & LD2). + assert (DST_TYPE1: Val.has_type v1'' (mreg_type dst1')). + { + generalize (LTLtyping.wt_function_wt_bblock tf pc _ WTTF TCODE); intro WTBB. + apply wt_bblock_expand_moves_head in WTBB. + unfold Mem.loadv in LOAD1'; destruct a1'; inversion LOAD1'. + eapply Val.has_subtype; eauto. + eapply Mem.load_type; eauto. + } set (ls2 := Locmap.set (R dst1') v1'' (undef_regs (destroyed_by_load Mint32 addr) ls1)). assert (SAT2: satisf (rs#dst <- v) ls2 e2). { eapply loc_unconstrained_satisf. eapply can_undef_satisf; eauto. @@ -2124,8 +2327,11 @@ Proof. eapply add_equations_satisf; eauto. assumption. rewrite Regmap.gss. apply Val.lessdef_trans with v1'; unfold sel_val; unfold kind_first_word; unfold v1'; destruct Archi.big_endian; auto. + auto. } - exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]]. + exploit (exec_moves mv2); eauto. + split. apply wt_setreg; auto using wt_undef_regs. WellTypedBlock. + intros [ls3 [A3 [B3 C3]]]. assert (LD3: Val.lessdef_list rs##args (reglist ls3 args2')). { replace (rs##args) with ((rs#dst<-v)##args). eapply add_equations_lessdef; eauto. @@ -2138,21 +2344,34 @@ Proof. assert (LOADX: exists v2'', Mem.loadv Mint32 m' a2' = Some v2'' /\ Val.lessdef v2' v2''). { discriminate || (eapply Mem.loadv_extends; [eauto|eexact LOAD2|eexact G2]). } destruct LOADX as (v2'' & LOAD2' & LD4). + assert (DST_TYPE2: Val.has_type v2'' (mreg_type dst2')). + { + generalize (LTLtyping.wt_function_wt_bblock tf pc _ WTTF TCODE); intro WTBB. + apply wt_bblock_expand_moves_cons in WTBB. + apply wt_bblock_expand_moves_head in WTBB. + unfold Mem.loadv in LOAD2'; destruct a2'; inversion LOAD2'. + eapply Val.has_subtype; eauto. + eapply Mem.load_type; eauto. + } set (ls4 := Locmap.set (R dst2') v2'' (undef_regs (destroyed_by_load Mint32 addr2) ls3)). assert (SAT4: satisf (rs#dst <- v) ls4 e0). { eapply loc_unconstrained_satisf. eapply can_undef_satisf; eauto. eapply add_equations_satisf; eauto. assumption. rewrite Regmap.gss. apply Val.lessdef_trans with v2'; unfold sel_val; unfold kind_second_word; unfold v2'; destruct Archi.big_endian; auto. + auto. } - exploit (exec_moves mv3); eauto. intros [ls5 [A5 B5]]. + exploit (exec_moves mv3); eauto. + split. apply wt_setreg; auto using wt_undef_regs. WellTypedBlock. + intros [ls5 [A5 [B5 C5]]]. econstructor; split. eapply plus_left. econstructor; eauto. eapply star_trans. eexact A1. eapply star_left. econstructor. instantiate (1 := a1'). rewrite <- F1. apply eval_addressing_preserved. exact symbols_preserved. eexact LOAD1'. instantiate (1 := ls2); auto. - eapply star_trans. eexact A3. + eapply star_trans. + eexact A3. eapply star_left. econstructor. instantiate (1 := a2'). rewrite <- F2. apply eval_addressing_preserved. exact symbols_preserved. eexact LOAD2'. instantiate (1 := ls4); auto. @@ -2160,18 +2379,30 @@ Proof. constructor. eauto. eauto. eauto. eauto. eauto. traceEq. exploit satisf_successors; eauto. simpl; eauto. intros [enext [W Z]]. - econstructor; eauto. + split; econstructor; eauto. (* load first word of a pair *) - generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2). set (v2' := if Archi.big_endian then v2 else v1) in *. set (v1' := if Archi.big_endian then v1 else v2) in *. - exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. + exploit (exec_moves mv1); eauto. + split. auto. apply wt_function_wt_bblock in TCODE; eauto. + intros [ls1 [A1 [B1 C1]]]. assert (LD1: Val.lessdef_list rs##args (reglist ls1 args')). { eapply add_equations_lessdef; eauto. } exploit eval_addressing_lessdef. eexact LD1. eauto. intros [a1' [F1 G1]]. exploit Mem.loadv_extends. eauto. eexact LOAD1. eexact G1. intros (v1'' & LOAD1' & LD2). + assert (DST_TYPE: Val.has_type v1'' (mreg_type dst')). + { + generalize (LTLtyping.wt_function_wt_bblock tf pc _ WTTF TCODE); intro WTBB. + apply wt_bblock_expand_moves_head in WTBB. simpl in WTBB. + unfold Mem.loadv in LOAD1'; destruct a1'; try inversion LOAD1'. + apply Mem.load_type in LOAD1'. + destruct (mreg_type dst'); auto; try congruence. + apply Val.has_subtype with (ty1 := Tint); auto. + apply Val.has_subtype with (ty1 := Tint); auto. + } set (ls2 := Locmap.set (R dst') v1'' (undef_regs (destroyed_by_load Mint32 addr) ls1)). assert (SAT2: satisf (rs#dst <- v) ls2 e0). { eapply parallel_assignment_satisf; eauto. @@ -2179,7 +2410,9 @@ Proof. unfold sel_val; unfold kind_first_word; unfold v1'; destruct Archi.big_endian; auto. eapply can_undef_satisf. eauto. eapply add_equations_satisf; eauto. } - exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]]. + exploit (exec_moves mv2); eauto. + split. apply wt_setreg, wt_undef_regs; auto. WellTypedBlock. + intros [ls3 [A3 [B3 C3]]]. econstructor; split. eapply plus_left. econstructor; eauto. eapply star_trans. eexact A1. @@ -2190,14 +2423,16 @@ Proof. constructor. eauto. eauto. eauto. traceEq. exploit satisf_successors; eauto. simpl; eauto. intros [enext [W Z]]. - econstructor; eauto. + split; econstructor; eauto. (* load second word of a pair *) - generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2). set (v2' := if Archi.big_endian then v2 else v1) in *. set (v1' := if Archi.big_endian then v1 else v2) in *. - exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. + exploit (exec_moves mv1); eauto. + split. auto. apply wt_function_wt_bblock in TCODE; eauto. + intros [ls1 [A1 [B1 C1]]]. assert (LD1: Val.lessdef_list rs##args (reglist ls1 args')). { eapply add_equations_lessdef; eauto. } exploit eval_addressing_lessdef. eexact LD1. @@ -2206,13 +2441,25 @@ Proof. assert (LOADX: exists v2'', Mem.loadv Mint32 m' a1' = Some v2'' /\ Val.lessdef v2' v2''). { discriminate || (eapply Mem.loadv_extends; [eauto|eexact LOAD2|eexact G1]). } destruct LOADX as (v2'' & LOAD2' & LD2). + assert (DST_TYPE: Val.has_type v2'' (mreg_type dst')). + { + generalize (LTLtyping.wt_function_wt_bblock tf pc _ WTTF TCODE); intro WTBB. + apply wt_bblock_expand_moves_head in WTBB. simpl in WTBB. + unfold Mem.loadv in LOAD2'; destruct a1'; try inversion LOAD2'. + apply Mem.load_type in LOAD2'. + destruct (mreg_type dst'); auto; try congruence. + apply Val.has_subtype with (ty1 := Tint); auto. + apply Val.has_subtype with (ty1 := Tint); auto. + } set (ls2 := Locmap.set (R dst') v2'' (undef_regs (destroyed_by_load Mint32 addr2) ls1)). assert (SAT2: satisf (rs#dst <- v) ls2 e0). { eapply parallel_assignment_satisf; eauto. apply Val.lessdef_trans with v2'; unfold sel_val; unfold kind_second_word; unfold v2'; destruct Archi.big_endian; auto. eapply can_undef_satisf. eauto. eapply add_equations_satisf; eauto. } - exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]]. + exploit (exec_moves mv2); eauto. + split. apply wt_setreg, wt_undef_regs; auto. WellTypedBlock. + intros [ls3 [A3 [B3 C3]]]. econstructor; split. eapply plus_left. econstructor; eauto. eapply star_trans. eexact A1. @@ -2223,10 +2470,12 @@ Proof. constructor. eauto. eauto. eauto. traceEq. exploit satisf_successors; eauto. simpl; eauto. intros [enext [W Z]]. - econstructor; eauto. + split; econstructor; eauto. (* load dead *) -- exploit exec_moves; eauto. intros [ls1 [X Y]]. +- exploit exec_moves; eauto. + split; auto. apply wt_function_wt_bblock in TCODE; eauto. + intros [ls1 [X [Y Z]]]. econstructor; split. eapply plus_left. econstructor; eauto. eapply star_right. eexact X. econstructor; eauto. @@ -2234,11 +2483,14 @@ Proof. exploit satisf_successors. eauto. eauto. simpl; eauto. eauto. eapply reg_unconstrained_satisf; eauto. intros [enext [U V]]. - econstructor; eauto. + split; econstructor; eauto. eapply wt_exec_Iload; eauto. (* store *) -- exploit exec_moves; eauto. intros [ls1 [X Y]]. +- exploit exec_moves; eauto. + split; auto. + eapply wt_function_wt_bblock; eauto. + intros [ls1 [X [Y Z]]]. exploit add_equations_lessdef; eauto. intros LD. simpl in LD. inv LD. exploit eval_addressing_lessdef; eauto. intros [a' [F G]]. exploit Mem.storev_extends; eauto. intros [m'' [P Q]]. @@ -2250,7 +2502,7 @@ Proof. constructor. eauto. eauto. traceEq. exploit satisf_successors; eauto. simpl; eauto. eapply can_undef_satisf; eauto. eapply add_equations_satisf; eauto. intros [enext [U V]]. - econstructor; eauto. + split; econstructor; eauto using wt_undef_regs. (* store 2 *) - assert (SF: Archi.ptr64 = false) by (apply Archi.splitlong_ptr32; auto). @@ -2262,7 +2514,10 @@ Proof. with (sel_val kind_second_word rs#src) by (unfold kind_second_word; destruct Archi.big_endian; reflexivity). intros [m1 [STORE1 STORE2]]. - exploit (exec_moves mv1); eauto. intros [ls1 [X Y]]. + exploit (exec_moves mv1); eauto. + split; auto. + eapply wt_function_wt_bblock; eauto. + intros [ls1 [X [Z Y]]]. exploit add_equations_lessdef. eexact Heqo1. eexact Y. intros LD1. exploit add_equation_lessdef. eapply add_equations_satisf. eexact Heqo1. eexact Y. simpl. intros LD2. @@ -2275,7 +2530,9 @@ Proof. rewrite <- F1. apply eval_addressing_preserved. exact symbols_preserved. exploit Mem.storev_extends. eauto. eexact STORE1. eexact G1. eauto. intros [m1' [STORE1' EXT1]]. - exploit (exec_moves mv2); eauto. intros [ls3 [U V]]. + exploit (exec_moves mv2); eauto. + split; try apply wt_undef_regs; auto. WellTypedBlock. + intros [ls3 [U [W V]]]. exploit add_equations_lessdef. eexact Heqo. eexact V. intros LD3. exploit add_equation_lessdef. eapply add_equations_satisf. eexact Heqo. eexact V. simpl. intros LD4. @@ -2301,13 +2558,16 @@ Proof. eapply can_undef_satisf. eauto. eapply add_equation_satisf. eapply add_equations_satisf; eauto. intros [enext [P Q]]. - econstructor; eauto. + split; econstructor; eauto using wt_undef_regs. (* call *) - set (sg := RTL.funsig fd) in *. set (args' := loc_arguments sg) in *. set (res' := loc_result sg) in *. - exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. + exploit (exec_moves mv1); eauto. + split; auto. + eapply wt_function_wt_bblock; eauto. + intros [ls1 [A1 [B1 C1]]]. exploit find_function_translated. eauto. eauto. eapply add_equations_args_satisf; eauto. intros [tfd [E F]]. assert (SIG: funsig tfd = sg). eapply sig_function_translated; eauto. @@ -2316,6 +2576,8 @@ Proof. eapply star_right. eexact A1. econstructor; eauto. eauto. traceEq. exploit analyze_successors; eauto. simpl. left; eauto. intros [enext [U V]]. + split. apply wt_call_state; auto. constructor; auto. WellTypedBlock. + eauto using wt_transf_fundef. econstructor; eauto. econstructor; eauto. inv WTI. congruence. @@ -2325,7 +2587,8 @@ Proof. eapply add_equations_args_satisf; eauto. congruence. apply wt_regset_assign; auto. - intros [ls2 [A2 B2]]. + split; auto. WellTypedBlock. + intros [ls2 [A2 [B2 C2]]]. exists ls2; split. eapply star_right. eexact A2. constructor. traceEq. apply satisf_incr with eafter; auto. @@ -2338,7 +2601,10 @@ Proof. - set (sg := RTL.funsig fd) in *. set (args' := loc_arguments sg) in *. exploit Mem.free_parallel_extends; eauto. intros [m'' [P Q]]. - exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. + exploit (exec_moves mv); eauto. + split; auto. + eapply wt_function_wt_bblock; eauto. + intros [ls1 [A1 [B1 C1]]]. exploit find_function_translated. eauto. eauto. eapply add_equations_args_satisf; eauto. intros [tfd [E F]]. assert (SIG: funsig tfd = sg). eapply sig_function_translated; eauto. @@ -2349,6 +2615,9 @@ Proof. replace (fn_stacksize tf) with (RTL.fn_stacksize f); eauto. destruct (transf_function_inv _ _ FUN); auto. eauto. traceEq. + split. + constructor. auto. eapply wt_transf_fundef; eauto. + auto using wt_return_regs, wt_parent_locset. econstructor; eauto. eapply match_stackframes_change_sig; eauto. rewrite SIG. rewrite e0. decEq. destruct (transf_function_inv _ _ FUN); auto. @@ -2358,15 +2627,35 @@ Proof. rewrite SIG. inv WTI. rewrite <- H6. apply wt_regset_list; auto. (* builtin *) -- exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. +- exploit (exec_moves mv1); eauto. + split; auto. + eapply wt_function_wt_bblock; eauto. + intros [ls1 [A1 [B1 C1]]]. exploit add_equations_builtin_eval; eauto. intros (C & vargs' & vres' & m'' & D & E & F & G). assert (WTRS': wt_regset env (regmap_setres res vres rs)) by (eapply wt_exec_Ibuiltin; eauto). + assert (WTBR: wt_builtin_res (proj_sig_res (ef_sig ef)) res' = true). + { + apply wt_function_wt_bblock in TCODE; auto. + unfold wt_bblock, expand_moves in *. rewrite forallb_app in TCODE. + simpl in TCODE. InvBooleans. auto. + } + exploit external_call_well_typed; eauto; intros. set (ls2 := Locmap.setres res' vres' (undef_regs (destroyed_by_builtin ef) ls1)). assert (satisf (regmap_setres res vres rs) ls2 e0). { eapply parallel_set_builtin_res_satisf; eauto. - eapply can_undef_satisf; eauto. } - exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]]. + eapply can_undef_satisf; eauto. + unfold Val.has_type_builtin_res; unfold wt_builtin_res in WTBR. + destruct res'; try eapply Val.has_subtype; eauto. + InvBooleans. split. + eapply Val.has_subtype; eauto. destruct vres'; simpl; eauto. + eapply Val.has_subtype; eauto. destruct vres'; simpl; eauto. + } + exploit (exec_moves mv2); eauto. + split; auto. + apply wt_setres with (ty := proj_sig_res (ef_sig ef)); auto. + apply wt_undef_regs; auto. WellTypedBlock. + intros [ls3 [A3 [B3 C3]]]. econstructor; split. eapply plus_left. econstructor; eauto. eapply star_trans. eexact A1. @@ -2379,10 +2668,13 @@ Proof. reflexivity. reflexivity. reflexivity. traceEq. exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. - econstructor; eauto. + split; econstructor; eauto. (* cond *) -- exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. +- exploit (exec_moves mv); eauto. + split; auto. + eapply wt_function_wt_bblock; eauto. + intros [ls1 [A1 [B1 C1]]]. econstructor; split. eapply plus_left. econstructor; eauto. eapply star_right. eexact A1. @@ -2392,10 +2684,13 @@ Proof. instantiate (1 := if b then ifso else ifnot). simpl. destruct b; auto. eapply can_undef_satisf. eauto. eapply add_equations_satisf; eauto. intros [enext [U V]]. - econstructor; eauto. + split; econstructor; eauto using wt_undef_regs. (* jumptable *) -- exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. +- exploit (exec_moves mv); eauto. + split; auto. + eapply wt_function_wt_bblock; eauto. + intros [ls1 [A1 [B1 C1]]]. assert (Val.lessdef (Vint n) (ls1 (R arg'))). rewrite <- H0. eapply add_equation_lessdef with (q := Eq Full arg (R arg')); eauto. inv H2. @@ -2407,28 +2702,38 @@ Proof. instantiate (1 := pc'). simpl. eapply list_nth_z_in; eauto. eapply can_undef_satisf. eauto. eapply add_equation_satisf; eauto. intros [enext [U V]]. - econstructor; eauto. + split; econstructor; eauto using wt_undef_regs. (* return *) - destruct (transf_function_inv _ _ FUN). exploit Mem.free_parallel_extends; eauto. rewrite H10. intros [m'' [P Q]]. inv WTI; MonadInv. + (* without an argument *) - exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. + exploit (exec_moves mv); eauto. + split; auto. + eapply wt_function_wt_bblock; eauto. + intros [ls1 [A1 [B1 C1]]]. econstructor; split. eapply plus_left. econstructor; eauto. eapply star_right. eexact A1. econstructor. eauto. eauto. traceEq. - simpl. econstructor; eauto. + simpl. split. econstructor; eauto. + auto using wt_return_regs, wt_parent_locset. + econstructor; eauto. apply return_regs_agree_callee_save. constructor. + (* with an argument *) - exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. + exploit (exec_moves mv); eauto. + split; auto. + eapply wt_function_wt_bblock; eauto. + intros [ls1 [A1 [B1 C1]]]. econstructor; split. eapply plus_left. econstructor; eauto. eapply star_right. eexact A1. econstructor. eauto. eauto. traceEq. - simpl. econstructor; eauto. rewrite <- H11. + simpl. split. econstructor; eauto. + auto using wt_return_regs, wt_parent_locset. + econstructor; eauto. rewrite <- H11. replace (Locmap.getpair (map_rpair R (loc_result (RTL.fn_sig f))) (return_regs (parent_locset ts) ls1)) with (Locmap.getpair (map_rpair R (loc_result (RTL.fn_sig f))) ls1). @@ -2452,14 +2757,16 @@ Proof. eapply can_undef_satisf; eauto. eapply compat_entry_satisf; eauto. rewrite call_regs_param_values. eexact ARGS. exact WTRS. - intros [ls1 [A B]]. + split. apply wt_undef_regs, wt_call_regs. auto. + eapply wt_function_wt_bblock; eauto. + intros [ls1 [A [B C]]]. econstructor; split. eapply plus_left. econstructor; eauto. eapply star_left. econstructor; eauto. eapply star_right. eexact A. econstructor; eauto. eauto. eauto. traceEq. - econstructor; eauto. + split; econstructor; eauto. (* external function *) - exploit external_call_mem_extends; eauto. intros [v' [m'' [F [G [J K]]]]]. @@ -2467,13 +2774,29 @@ Proof. econstructor; split. apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved with (ge1 := ge); eauto. apply senv_preserved. + exploit external_call_well_typed; eauto; intro WTRES. + split. econstructor; eauto. + apply wt_setpair; auto. + econstructor; eauto. simpl. destruct (loc_result (ef_sig ef)) eqn:RES; simpl. rewrite Locmap.gss; auto. + generalize (loc_result_type (ef_sig ef)); intro SUBTYP. + rewrite RES in SUBTYP; simpl in SUBTYP. + exploit Val.has_subtype; eauto; intros. + rewrite Val.load_result_same; auto. + generalize (loc_result_pair (ef_sig ef)); rewrite RES; intros (A & B & C & D & E). exploit external_call_well_typed; eauto. unfold proj_sig_res; rewrite B. intros WTRES'. rewrite Locmap.gss. rewrite Locmap.gso by (red; auto). rewrite Locmap.gss. + + generalize (loc_result_type (ef_sig ef)); intro SUBTYP. + rewrite RES in SUBTYP; simpl in SUBTYP. + rewrite !Val.load_result_same. rewrite val_longofwords_eq_1 by auto. auto. + eapply Val.has_subtype; eauto. destruct v'; simpl; auto. + eapply Val.has_subtype; eauto. destruct v'; simpl; auto. + red; intros. rewrite (AG l H0). symmetry; apply Locmap.gpo. assert (X: forall r, is_callee_save r = false -> Loc.diff l (R r)). @@ -2486,6 +2809,9 @@ Proof. exploit STEPS; eauto. rewrite WTRES0; auto. intros [ls2 [A B]]. econstructor; split. eapply plus_left. constructor. eexact A. traceEq. + split. + apply star_step_type_preservation in A; eauto. + inversion WTSTK. econstructor; eauto. econstructor; eauto. apply wt_regset_assign; auto. rewrite WTRES0; auto. Qed. @@ -2520,30 +2846,19 @@ Proof. rewrite H; auto. Qed. -Lemma wt_prog: wt_program prog. -Proof. - red; intros. - exploit list_forall2_in_left. eexact (proj1 TRANSF). eauto. - intros ([i' gd] & A & B & C). simpl in *; subst i'. - inv C. destruct f; simpl in *. -- monadInv H2. - unfold transf_function in EQ. - destruct (type_function f) as [env|] eqn:TF; try discriminate. - econstructor. eapply type_function_correct; eauto. -- constructor. -Qed. - Theorem transf_program_correct: forward_simulation (RTL.semantics prog) (LTL.semantics tprog). Proof. - set (ms := fun s s' => wt_state s /\ match_states s s'). + set (ms := fun s s' => wt_state s /\ LTLtyping.wt_state s' /\ match_states s s'). eapply forward_simulation_plus with (match_states := ms). - apply senv_preserved. - intros. exploit initial_states_simulation; eauto. intros [st2 [A B]]. exists st2; split; auto. split; auto. apply wt_initial_state with (p := prog); auto. exact wt_prog. -- intros. destruct H. eapply final_states_simulation; eauto. -- intros. destruct H0. + split; auto. + apply LTLtyping.wt_initial_state with (prog := tprog); auto. exact wt_tprog. +- intros. destruct H as [H1 [H2 H3]]. eapply final_states_simulation; eauto. +- intros. destruct H0 as [H1 [H2 H3]]. exploit step_simulation; eauto. intros [s2' [A B]]. exists s2'; split. exact A. split. eapply subject_reduction; eauto. eexact wt_prog. eexact H. diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index f6f03868ce..12839f8c4b 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -416,9 +416,12 @@ Proof. - eapply agree_set_mreg; eauto. rewrite Pregmap.gss. auto. intros. apply Pregmap.gso; auto. - auto. -- apply IHres2. apply IHres1. auto. - apply Val.hiword_lessdef; auto. - apply Val.loword_lessdef; auto. +- apply agree_set_mreg with (rs := rs # (preg_of hi) <- (Val.hiword v')). + apply agree_set_mreg with (rs := rs). + auto. rewrite Pregmap.gss; auto using Val.hiword_lessdef. + intros. apply Pregmap.gso; auto. + rewrite Pregmap.gss. auto using Val.loword_lessdef. + intros. apply Pregmap.gso; auto. Qed. Lemma set_res_other: @@ -429,7 +432,9 @@ Proof. induction res; simpl; intros. - apply Pregmap.gso. red; intros; subst r. rewrite preg_of_data in H; discriminate. - auto. -- rewrite IHres2, IHres1; auto. +- rewrite !Pregmap.gso; auto. + red; intros; subst r. rewrite preg_of_data in H; discriminate. + red; intros; subst r. rewrite preg_of_data in H; discriminate. Qed. (** * Correspondence between Mach code and Asm code *) diff --git a/backend/Debugvar.v b/backend/Debugvar.v index 1f36103017..0cb33a8860 100644 --- a/backend/Debugvar.v +++ b/backend/Debugvar.v @@ -111,11 +111,11 @@ Fixpoint arg_no_overlap (a: builtin_arg loc) (l: loc) : bool := Definition kill (l: loc) (s: avail) : avail := List.filter (fun vi => arg_no_overlap (proj1_sig (snd vi)) l) s. -Fixpoint kill_res (r: builtin_res mreg) (s: avail) : avail := +Definition kill_res (r: builtin_res mreg) (s: avail) : avail := match r with | BR r => kill (R r) s | BR_none => s - | BR_splitlong hi lo => kill_res hi (kill_res lo s) + | BR_splitlong hi lo => kill (R hi) (kill (R lo) s) end. (** Likewise when a function call takes place. *) diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v new file mode 100644 index 0000000000..501c7dbb7a --- /dev/null +++ b/backend/LTLtyping.v @@ -0,0 +1,405 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Type-checking LTL code, adapted with tiny changes from [Lineartyping]. *) + +Require Import Coqlib. +Require Import AST. +Require Import Integers. +Require Import Values. +Require Import Globalenvs. +Require Import Memory. +Require Import Events. +Require Import Op. +Require Import Machregs. +Require Import Locations. +Require Import Conventions. +Require Import LTL. + +(** The rules are presented as boolean-valued functions so that we + get an executable type-checker for free. *) + +Section WT_INSTR. + +Variable funct: function. + +Definition slot_valid (sl: slot) (ofs: Z) (ty: typ): bool := + match sl with + | Local => zle 0 ofs + | Outgoing => zle 0 ofs + | Incoming => In_dec Loc.eq (S Incoming ofs ty) (regs_of_rpairs (loc_parameters funct.(fn_sig))) + end + && Zdivide_dec (typealign ty) ofs (typealign_pos ty). + +Definition slot_writable (sl: slot) : bool := + match sl with + | Local => true + | Outgoing => true + | Incoming => false + end. + +Definition loc_valid (l: loc) : bool := + match l with + | R r => true + | S Local ofs ty => slot_valid Local ofs ty + | S _ _ _ => false + end. + +Definition wt_builtin_res (ty: typ) (res: builtin_res mreg) : bool := + match res with + | BR r => subtype ty (mreg_type r) + | BR_none => true + | BR_splitlong hi lo => subtype Tint (mreg_type hi) && subtype Tint (mreg_type lo) + end. + +Definition wt_instr (i: instruction) : bool := + match i with + | Lgetstack sl ofs ty r => + subtype ty (mreg_type r) && slot_valid sl ofs ty + | Lsetstack r sl ofs ty => + slot_valid sl ofs ty && slot_writable sl + | Lop op args res => + match is_move_operation op args with + | Some arg => + subtype (mreg_type arg) (mreg_type res) + | None => + let (targs, tres) := type_of_operation op in + subtype tres (mreg_type res) + end + | Lload chunk addr args dst => + subtype (type_of_chunk chunk) (mreg_type dst) + | Ltailcall sg ros => + zeq (size_arguments sg) 0 + | Lbuiltin ef args res => + wt_builtin_res (proj_sig_res (ef_sig ef)) res + && forallb loc_valid (params_of_builtin_args args) + | _ => + true + end. + +End WT_INSTR. + +Definition wt_bblock (f: function) (b: bblock) : bool := + forallb (wt_instr f) b. + +Definition wt_function (f: function) : bool := + let bs := map snd (Maps.PTree.elements f.(fn_code)) in + forallb (wt_bblock f) bs. + +Lemma wt_function_wt_bblock: + forall f pc b, + wt_function f = true -> + Maps.PTree.get pc (fn_code f) = Some b -> + wt_bblock f b = true. +Proof. + intros. apply Maps.PTree.elements_correct in H0. + unfold wt_function, wt_bblock in *. eapply forallb_forall in H; eauto. + change b with (snd (pc, b)). apply in_map; auto. +Qed. + +(** Typing the run-time state. *) + +Definition wt_locset (ls: locset) : Prop := + forall l, Val.has_type (ls l) (Loc.type l). + +Lemma wt_setreg: + forall ls r v, + Val.has_type v (mreg_type r) -> wt_locset ls -> wt_locset (Locmap.set (R r) v ls). +Proof. + intros; red; intros. + unfold Locmap.set. + destruct (Loc.eq (R r) l). + subst l. rewrite Val.load_result_same; auto. + destruct (Loc.diff_dec (R r) l). auto. red. auto. +Qed. + +Lemma wt_setstack: + forall ls sl ofs ty v, + wt_locset ls -> wt_locset (Locmap.set (S sl ofs ty) v ls). +Proof. + intros; red; intros. + unfold Locmap.set. + destruct (Loc.eq (S sl ofs ty) l). + subst l. simpl. + generalize (Val.load_result_type (chunk_of_type ty) v). + replace (type_of_chunk (chunk_of_type ty)) with ty. auto. + destruct ty; reflexivity. + destruct (Loc.diff_dec (S sl ofs ty) l). auto. red. auto. +Qed. + +Lemma wt_undef_regs: + forall rs ls, wt_locset ls -> wt_locset (undef_regs rs ls). +Proof. + induction rs; simpl; intros. auto. apply wt_setreg; auto. red; auto. +Qed. + +Lemma wt_call_regs: + forall ls, wt_locset ls -> wt_locset (call_regs ls). +Proof. + intros; red; intros. unfold call_regs. destruct l. auto. + destruct sl. + red; auto. + change (Loc.type (S Incoming pos ty)) with (Loc.type (S Outgoing pos ty)). auto. + red; auto. +Qed. + +Lemma wt_return_regs: + forall caller callee, + wt_locset caller -> wt_locset callee -> wt_locset (return_regs caller callee). +Proof. + intros; red; intros. + unfold return_regs. destruct l; auto. destruct (is_callee_save r); auto. +Qed. + +Lemma wt_init: + wt_locset (Locmap.init Vundef). +Proof. + red; intros. unfold Locmap.init. red; auto. +Qed. + +Lemma wt_setpair: + forall sg v rs, + Val.has_type v (proj_sig_res sg) -> + wt_locset rs -> + wt_locset (Locmap.setpair (loc_result sg) v rs). +Proof. + intros. generalize (loc_result_pair sg) (loc_result_type sg). + destruct (loc_result sg); simpl Locmap.setpair. +- intros. apply wt_setreg; auto. eapply Val.has_subtype; eauto. +- intros A B. decompose [and] A. + apply wt_setreg. eapply Val.has_subtype; eauto. destruct v; exact I. + apply wt_setreg. eapply Val.has_subtype; eauto. destruct v; exact I. + auto. +Qed. + +Lemma wt_setres: + forall res ty v rs, + wt_builtin_res ty res = true -> + Val.has_type v ty -> + wt_locset rs -> + wt_locset (Locmap.setres res v rs). +Proof. + induction res; simpl; intros. +- apply wt_setreg; auto. eapply Val.has_subtype; eauto. +- auto. +- InvBooleans. + apply wt_setreg; auto. apply Val.has_subtype with (ty1 := Tint); auto. + destruct v; exact I. + apply wt_setreg; auto. apply Val.has_subtype with (ty1 := Tint); auto. + destruct v; exact I. +Qed. + +(** Soundness of the type system *) + +Definition wt_fundef (fd: fundef) := + match fd with + | Internal f => wt_function f = true + | External ef => True + end. + +Definition wt_program (prog: program): Prop := + forall i fd, In (i, Gfun fd) prog.(prog_defs) -> wt_fundef fd. + +Inductive wt_callstack: list stackframe -> Prop := + | wt_callstack_nil: + wt_callstack nil + | wt_callstack_cons: forall f sp rs b s + (WTSTK: wt_callstack s) + (WTF: wt_function f = true) + (WTB: wt_bblock f b = true) + (WTLS: wt_locset rs), + wt_callstack (Stackframe f sp rs b :: s). + +Lemma wt_parent_locset: + forall s, wt_callstack s -> wt_locset (parent_locset s). +Proof. + induction 1; simpl. +- apply wt_init. +- auto. +Qed. + +Inductive wt_state: state -> Prop := + | wt_branch_state: forall s f sp n rs m + (WTSTK: wt_callstack s ) + (WTF: wt_function f = true) + (WTLS: wt_locset rs), + wt_state (State s f sp n rs m) + | wt_regular_state: forall s f sp b rs m + (WTSTK: wt_callstack s ) + (WTF: wt_function f = true) + (WTB: wt_bblock f b = true) + (WTLS: wt_locset rs), + wt_state (Block s f sp b rs m) + | wt_call_state: forall s fd rs m + (WTSTK: wt_callstack s) + (WTFD: wt_fundef fd) + (WTLS: wt_locset rs), + wt_state (Callstate s fd rs m) + | wt_return_state: forall s rs m + (WTSTK: wt_callstack s) + (WTLS: wt_locset rs), + wt_state (Returnstate s rs m). + +(** Preservation of state typing by transitions *) + +Section SOUNDNESS. + +Variable prog: program. +Let ge := Genv.globalenv prog. + +Hypothesis wt_prog: wt_program prog. + +Lemma wt_find_function: + forall ros rs f, find_function ge ros rs = Some f -> wt_fundef f. +Proof. + intros. + assert (X: exists i, In (i, Gfun f) prog.(prog_defs)). + { + destruct ros as [r | s]; simpl in H. + eapply Genv.find_funct_inversion; eauto. + destruct (Genv.find_symbol ge s) as [b|]; try discriminate. + eapply Genv.find_funct_ptr_inversion; eauto. + } + destruct X as [i IN]. eapply wt_prog; eauto. +Qed. + +Theorem step_type_preservation: + forall S1 t S2, step ge S1 t S2 -> wt_state S1 -> wt_state S2. +Proof. +Local Opaque mreg_type. + induction 1; intros WTS; inv WTS. +- (* startblock *) + econstructor; eauto. + apply Maps.PTree.elements_correct in H. + unfold wt_function in WTF. eapply forallb_forall in WTF; eauto. + change bb with (snd (pc, bb)). apply in_map; auto. +- (* op *) + simpl in *. destruct (is_move_operation op args) as [src | ] eqn:ISMOVE. + + (* move *) + InvBooleans. exploit is_move_operation_correct; eauto. intros [EQ1 EQ2]; subst. + simpl in H. inv H. + econstructor; eauto. apply wt_setreg. eapply Val.has_subtype; eauto. apply WTLS. + apply wt_undef_regs; auto. + + (* other ops *) + destruct (type_of_operation op) as [ty_args ty_res] eqn:TYOP. InvBooleans. + econstructor; eauto. + apply wt_setreg; auto. eapply Val.has_subtype; eauto. + change ty_res with (snd (ty_args, ty_res)). rewrite <- TYOP. eapply type_of_operation_sound; eauto. + red; intros; subst op. simpl in ISMOVE. + destruct args; try discriminate. destruct args; discriminate. + apply wt_undef_regs; auto. +- (* load *) + simpl in *; InvBooleans. + econstructor; eauto. + apply wt_setreg. eapply Val.has_subtype; eauto. + destruct a; simpl in H0; try discriminate. eapply Mem.load_type; eauto. + apply wt_undef_regs; auto. +- (* getstack *) + simpl in *; InvBooleans. + econstructor; eauto. + eapply wt_setreg; eauto. eapply Val.has_subtype; eauto. apply WTLS. + apply wt_undef_regs; auto. +- (* setstack *) + simpl in *; InvBooleans. + econstructor; eauto. + apply wt_setstack. apply wt_undef_regs; auto. +- (* store *) + simpl in *; InvBooleans. + econstructor. eauto. eauto. eauto. + apply wt_undef_regs; auto. +- (* call *) + simpl in *; InvBooleans. + econstructor; eauto. econstructor; eauto. + eapply wt_find_function; eauto. +- (* tailcall *) + simpl in *; InvBooleans. + econstructor; eauto. + eapply wt_find_function; eauto. + apply wt_return_regs; auto. apply wt_parent_locset; auto. +- (* builtin *) + simpl in *; InvBooleans. + econstructor; eauto. + eapply wt_setres; eauto. eapply external_call_well_typed; eauto. + apply wt_undef_regs; auto. +- (* branch *) + simpl in *. econstructor; eauto. +- (* cond branch *) + simpl in *. econstructor; auto; apply wt_undef_regs; auto. +- (* jumptable *) + simpl in *. econstructor; auto; apply wt_undef_regs; auto. +- (* return *) + simpl in *. InvBooleans. + econstructor; eauto. + apply wt_return_regs; auto. apply wt_parent_locset; auto. +- (* internal function *) + simpl in WTFD. + econstructor. eauto. eauto. eauto. + apply wt_undef_regs. apply wt_call_regs. auto. +- (* external function *) + econstructor. auto. apply wt_setpair; auto. + eapply external_call_well_typed; eauto. +- (* return *) + inv WTSTK. econstructor; eauto. +Qed. + +Theorem wt_initial_state: + forall S, initial_state prog S -> wt_state S. +Proof. + induction 1. econstructor. constructor. + unfold ge0 in H1. exploit Genv.find_funct_ptr_inversion; eauto. + intros [id IN]. eapply wt_prog; eauto. + apply wt_init. +Qed. + +End SOUNDNESS. + +(** Properties of well-typed states that are used in [Allocproof]. *) + +Lemma wt_state_getstack: + forall s f sp sl ofs ty rd c rs m, + wt_state (Block s f sp (Lgetstack sl ofs ty rd :: c) rs m) -> + slot_valid f sl ofs ty = true. +Proof. + intros. inv H. simpl in WTB; InvBooleans. auto. +Qed. + +Lemma wt_state_setstack: + forall s f sp sl ofs ty r c rs m, + wt_state (Block s f sp (Lsetstack r sl ofs ty :: c) rs m) -> + slot_valid f sl ofs ty = true /\ slot_writable sl = true. +Proof. + intros. inv H. simpl in WTB; InvBooleans. intuition. +Qed. + +Lemma wt_state_tailcall: + forall s f sp sg ros c rs m, + wt_state (Block s f sp (Ltailcall sg ros :: c) rs m) -> + size_arguments sg = 0. +Proof. + intros. inv H. simpl in WTB; InvBooleans. auto. +Qed. + +Lemma wt_state_builtin: + forall s f sp ef args res c rs m, + wt_state (Block s f sp (Lbuiltin ef args res :: c) rs m) -> + forallb (loc_valid f) (params_of_builtin_args args) = true. +Proof. + intros. inv H. simpl in WTB; InvBooleans. auto. +Qed. + +Lemma wt_callstate_wt_regs: + forall s f rs m, + wt_state (Callstate s f rs m) -> + forall r, Val.has_type (rs (R r)) (mreg_type r). +Proof. + intros. inv H. apply WTLS. +Qed. diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 30cc0d9194..1a31a6efb0 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -55,11 +55,11 @@ Definition loc_valid (l: loc) : bool := | S _ _ _ => false end. -Fixpoint wt_builtin_res (ty: typ) (res: builtin_res mreg) : bool := +Definition wt_builtin_res (ty: typ) (res: builtin_res mreg) : bool := match res with | BR r => subtype ty (mreg_type r) | BR_none => true - | BR_splitlong hi lo => wt_builtin_res Tint hi && wt_builtin_res Tint lo + | BR_splitlong hi lo => subtype Tint (mreg_type hi) && subtype Tint (mreg_type lo) end. Definition wt_instr (i: instruction) : bool := @@ -107,7 +107,7 @@ Proof. intros; red; intros. unfold Locmap.set. destruct (Loc.eq (R r) l). - subst l; auto. + subst l; rewrite Val.load_result_same; auto. destruct (Loc.diff_dec (R r) l). auto. red. auto. Qed. @@ -180,8 +180,11 @@ Proof. induction res; simpl; intros. - apply wt_setreg; auto. eapply Val.has_subtype; eauto. - auto. -- InvBooleans. eapply IHres2; eauto. destruct v; exact I. - eapply IHres1; eauto. destruct v; exact I. +- InvBooleans. + apply wt_setreg; auto. apply Val.has_subtype with (ty1 := Tint); auto. + destruct v; exact I. + apply wt_setreg; auto. apply Val.has_subtype with (ty1 := Tint); auto. + destruct v; exact I. Qed. Lemma wt_find_label: diff --git a/backend/Locations.v b/backend/Locations.v index c437df5dd6..8e0b3349a4 100644 --- a/backend/Locations.v +++ b/backend/Locations.v @@ -331,26 +331,25 @@ Module Locmap. Definition set (l: loc) (v: val) (m: t) : t := fun (p: loc) => if Loc.eq l p then - match l with R r => v | S sl ofs ty => Val.load_result (chunk_of_type ty) v end + Val.load_result (chunk_of_type (Loc.type l)) v else if Loc.diff_dec l p then m p else Vundef. Lemma gss: forall l v m, - (set l v m) l = - match l with R r => v | S sl ofs ty => Val.load_result (chunk_of_type ty) v end. + (set l v m) l = Val.load_result (chunk_of_type (Loc.type l)) v. Proof. intros. unfold set. apply dec_eq_true. Qed. - Lemma gss_reg: forall r v m, (set (R r) v m) (R r) = v. + Lemma gss_reg: forall r v m, Val.has_type v (mreg_type r) -> (set (R r) v m) (R r) = v. Proof. - intros. unfold set. rewrite dec_eq_true. auto. + intros. unfold set. rewrite dec_eq_true, Val.load_result_same; auto. Qed. Lemma gss_typed: forall l v m, Val.has_type v (Loc.type l) -> (set l v m) l = v. Proof. - intros. rewrite gss. destruct l. auto. apply Val.load_result_same; auto. + intros. rewrite gss. apply Val.load_result_same; auto. Qed. Lemma gso: forall l v m p, Loc.diff l p -> (set l v m) p = m p. @@ -377,10 +376,10 @@ Module Locmap. Lemma gus: forall ll l m, In l ll -> (undef ll m) l = Vundef. Proof. assert (P: forall ll l m, m l = Vundef -> (undef ll m) l = Vundef). - induction ll; simpl; intros. auto. apply IHll. + { induction ll; simpl; intros. auto. apply IHll. unfold set. destruct (Loc.eq a l). - destruct a. auto. destruct ty; reflexivity. - destruct (Loc.diff_dec a l); auto. + apply Val.load_result_same; auto. simpl; auto. + destruct (Loc.diff_dec a l); auto. } induction ll; simpl; intros. contradiction. destruct H. apply P. subst a. apply gss_typed. exact I. auto. @@ -417,12 +416,12 @@ Module Locmap. - destruct H. rewrite ! gso by (apply Loc.diff_sym; auto). auto. Qed. - Fixpoint setres (res: builtin_res mreg) (v: val) (m: t) : t := + Definition setres (res: builtin_res mreg) (v: val) (m: t) : t := match res with | BR r => set (R r) v m | BR_none => m | BR_splitlong hi lo => - setres lo (Val.loword v) (setres hi (Val.hiword v) m) + set (R lo) (Val.loword v) (set (R hi) (Val.hiword v) m) end. End Locmap. diff --git a/backend/Mach.v b/backend/Mach.v index 839a25bd45..e11a5a4f50 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -162,11 +162,11 @@ Definition set_pair (p: rpair mreg) (v: val) (rs: regset) : regset := | Twolong rhi rlo => rs#rhi <- (Val.hiword v) #rlo <- (Val.loword v) end. -Fixpoint set_res (res: builtin_res mreg) (v: val) (rs: regset) : regset := +Definition set_res (res: builtin_res mreg) (v: val) (rs: regset) : regset := match res with | BR r => Regmap.set r v rs | BR_none => rs - | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs) + | BR_splitlong hi lo => Regmap.set lo (Val.loword v) (Regmap.set hi (Val.hiword v) rs) end. Definition is_label (lbl: label) (instr: instruction) : bool := diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index df3445ea6a..8c18fc9a6b 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -243,7 +243,7 @@ let print_asm_argument print_preg oc modifier = function let builtin_arg_of_res = function | BR r -> BA r - | BR_splitlong(BR hi, BR lo) -> BA_splitlong(BA hi, BA lo) + | BR_splitlong(hi, lo) -> BA_splitlong(BA hi, BA lo) | _ -> assert false let re_asm_param_1 = Str.regexp "%%\\|%[QR]?[0-9]+" diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml index d4d7362d81..05cea84999 100644 --- a/backend/Regalloc.ml +++ b/backend/Regalloc.ml @@ -174,7 +174,7 @@ let convert_builtin_res tyenv = function | BR r -> let ty = tyenv r in if Archi.splitlong && ty = Tlong - then BR_splitlong(BR(V(r, Tint)), BR(V(twin_reg r, Tint))) + then BR_splitlong(V(r, Tint), V(twin_reg r, Tint)) else BR(V(r, ty)) | BR_none -> BR_none | BR_splitlong _ -> assert false @@ -201,15 +201,20 @@ let rec constrain_builtin_args al cl = let (al', cl2) = constrain_builtin_args al cl1 in (a' :: al', cl2) -let rec constrain_builtin_res a cl = - match a, cl with - | BR x, None :: cl' -> (a, cl') - | BR x, Some mr :: cl' -> (BR (L(R mr)), cl') - | BR_splitlong(hi, lo), _ -> - let (hi', cl1) = constrain_builtin_res hi cl in - let (lo', cl2) = constrain_builtin_res lo cl1 in - (BR_splitlong(hi', lo'), cl2) - | _, _ -> (a, cl) +let constrain_builtin_res_var x cl = + match cl with + | None :: cl' -> (BR x, cl') + | Some mr :: cl' -> (BR (L(R mr)), cl') + | _ -> (BR x, cl) + +let constrain_builtin_res a cl = + match a with + | BR x -> constrain_builtin_res_var x cl + | BR_splitlong(hi, lo) -> + let (hi', cl1) = constrain_builtin_res_var hi cl in + let (lo', cl2) = constrain_builtin_res_var lo cl1 in + (BR_splitlong(hi, lo), cl2) + | _ -> (a, cl) (* Return the XTL basic block corresponding to the given RTL instruction. Move and parallel move instructions are introduced to honor calling @@ -346,11 +351,11 @@ let rec vset_addarg a after = let vset_addargs al after = List.fold_right vset_addarg al after -let rec vset_removeres r after = +let vset_removeres r after = match r with | BR v -> VSet.remove v after | BR_none -> after - | BR_splitlong(hi, lo) -> vset_removeres hi (vset_removeres lo after) + | BR_splitlong(hi, lo) -> VSet.remove hi (VSet.remove lo after) let live_before instr after = match instr with @@ -883,15 +888,15 @@ let save_var tospill eqs v = (t, [Xspill(t, v)], add v t (kill v eqs)) end -let rec save_res tospill eqs = function +let save_res tospill eqs = function | BR v -> let (t, c1, eqs1) = save_var tospill eqs v in (BR t, c1, eqs1) | BR_none -> (BR_none, [], eqs) | BR_splitlong(hi, lo) -> - let (hi', c1, eqs1) = save_res tospill eqs hi in - let (lo', c2, eqs2) = save_res tospill eqs1 lo in + let (hi', c1, eqs1) = save_var tospill eqs hi in + let (lo', c2, eqs2) = save_var tospill eqs1 lo in (BR_splitlong(hi', lo'), c1 @ c2, eqs2) (* Trimming equations when we have too many or when they are too old. diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index f7570f571f..66721046ee 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -18,7 +18,7 @@ Require Import Coqlib Errors. Require Import Integers AST Linking. Require Import Values Memory Separation Events Globalenvs Smallstep. Require Import LTL Op Locations Linear Mach. -Require Import Bounds Conventions Stacklayout Lineartyping. +Require Import Bounds Conventions Conventions1 Stacklayout Lineartyping. Require Import Stacking. Local Open Scope sep_scope. @@ -610,11 +610,12 @@ Lemma agree_regs_set_reg: forall j ls rs r v v', agree_regs j ls rs -> Val.inject j v v' -> + Val.has_type v (mreg_type r) -> agree_regs j (Locmap.set (R r) v ls) (Regmap.set r v' rs). Proof. intros; red; intros. unfold Regmap.set. destruct (RegEq.eq r0 r). subst r0. - rewrite Locmap.gss; auto. + rewrite Locmap.gss, Val.load_result_same; auto. rewrite Locmap.gso; auto. red. auto. Qed. @@ -622,11 +623,12 @@ Lemma agree_regs_set_pair: forall j p v v' ls rs, agree_regs j ls rs -> Val.inject j v v' -> + Val.has_type_rpair v p Val.loword Val.hiword mreg_type -> agree_regs j (Locmap.setpair p v ls) (set_pair p v' rs). Proof. - intros. destruct p; simpl. + intros. destruct p; try destruct H1; simpl. - apply agree_regs_set_reg; auto. -- apply agree_regs_set_reg. apply agree_regs_set_reg; auto. +- apply agree_regs_set_reg; auto. apply agree_regs_set_reg; auto. apply Val.hiword_inject; auto. apply Val.loword_inject; auto. Qed. @@ -634,12 +636,13 @@ Lemma agree_regs_set_res: forall j res v v' ls rs, agree_regs j ls rs -> Val.inject j v v' -> + Val.has_type_builtin_res v res Val.loword Val.hiword mreg_type -> agree_regs j (Locmap.setres res v ls) (set_res res v' rs). Proof. - induction res; simpl; intros. + destruct res eqn:RES; simpl; intros. - apply agree_regs_set_reg; auto. - auto. -- apply IHres2. apply IHres1. auto. +- repeat apply agree_regs_set_reg; try tauto. apply Val.hiword_inject; auto. apply Val.loword_inject; auto. Qed. @@ -664,6 +667,7 @@ Proof. induction rl; simpl; intros. auto. apply agree_regs_set_reg; auto. + simpl; auto. Qed. (** Preservation under assignment of stack slot *) @@ -740,7 +744,7 @@ Proof. induction res; simpl; intros. - eapply agree_locs_set_reg; eauto. - auto. -- apply IHres2; auto using in_or_app. +- repeat eapply agree_locs_set_reg; eauto. Qed. Lemma agree_locs_undef_regs: @@ -994,7 +998,8 @@ Remark LTL_undef_regs_same: forall r rl ls, In r rl -> LTL.undef_regs rl ls (R r) = Vundef. Proof. induction rl; simpl; intros. contradiction. - unfold Locmap.set. destruct (Loc.eq (R a) (R r)). auto. + unfold Locmap.set. destruct (Loc.eq (R a) (R r)). + rewrite Val.load_result_same; simpl; auto. destruct (Loc.diff_dec (R a) (R r)); auto. apply IHrl. intuition congruence. Qed. @@ -1019,7 +1024,8 @@ Remark undef_regs_type: Proof. induction rl; simpl; intros. - auto. -- unfold Locmap.set. destruct (Loc.eq (R a) l). red; auto. +- unfold Locmap.set. destruct (Loc.eq (R a) l). + rewrite Val.load_result_same; simpl; auto. destruct (Loc.diff_dec (R a) l); auto. red; auto. Qed. @@ -1855,6 +1861,8 @@ Proof. apply plus_one. apply exec_Mgetstack. exact A. econstructor; eauto with coqlib. apply agree_regs_set_reg; auto. + inversion WTS; subst. simpl in WTC; InvBooleans. + apply Val.has_subtype with (ty1 := ty); auto. apply WTRS. apply agree_locs_set_reg; auto. + (* Lgetstack, incoming *) unfold slot_valid in SV. InvBooleans. @@ -1872,8 +1880,10 @@ Proof. rewrite (unfold_transf_function _ _ TRANSL). unfold fn_link_ofs. eapply frame_get_parent. eexact SEP. econstructor; eauto with coqlib. econstructor; eauto. - apply agree_regs_set_reg. apply agree_regs_set_reg. auto. auto. + apply agree_regs_set_reg. apply agree_regs_set_reg. auto. auto. simpl; auto. erewrite agree_incoming by eauto. exact B. + inversion WTS; subst. simpl in WTC; InvBooleans. + apply Val.has_subtype with (ty1 := ty); auto. apply WTRS. apply agree_locs_set_reg; auto. apply agree_locs_undef_locs; auto. + (* Lgetstack, outgoing *) exploit frame_get_outgoing; eauto. intros (v & A & B). @@ -1881,6 +1891,8 @@ Proof. apply plus_one. apply exec_Mgetstack. exact A. econstructor; eauto with coqlib. apply agree_regs_set_reg; auto. + inversion WTS; subst. simpl in WTC; InvBooleans. + apply Val.has_subtype with (ty1 := ty); auto. apply WTRS. apply agree_locs_set_reg; auto. - (* Lsetstack *) @@ -1926,6 +1938,16 @@ Proof. econstructor; eauto with coqlib. apply agree_regs_set_reg; auto. rewrite transl_destroyed_by_op. apply agree_regs_undef_regs; auto. + inversion WTS; subst. simpl in WTC; InvBooleans. + destruct (is_move_operation op args) eqn:MOVE. + apply is_move_operation_correct in MOVE; destruct MOVE. subst. + simpl in H; inv H. + apply Val.has_subtype with (ty1 := mreg_type m0); auto. apply WTRS. + generalize (is_not_move_operation ge _ _ args m H MOVE); intros. + assert (subtype (snd (type_of_operation op)) (mreg_type res) = true). + { rewrite <- H0. destruct (type_of_operation op); reflexivity. } + assert (Val.has_type v (snd (type_of_operation op))) by eauto using type_of_operation_sound. + apply Val.has_subtype with (ty1 := snd (type_of_operation op)); auto. apply agree_locs_set_reg; auto. apply agree_locs_undef_locs. auto. apply destroyed_by_op_caller_save. apply frame_set_reg. apply frame_undef_regs. exact SEP. @@ -1947,6 +1969,10 @@ Proof. eexact C. eauto. econstructor; eauto with coqlib. apply agree_regs_set_reg. rewrite transl_destroyed_by_load. apply agree_regs_undef_regs; auto. auto. + inversion WTS; subst. simpl in WTC; InvBooleans. + destruct a'; try inversion C. apply Mem.load_type in H4. + apply Val.has_subtype with (ty1 := type_of_chunk chunk); auto. + destruct D; auto. simpl; auto. apply agree_locs_set_reg. apply agree_locs_undef_locs. auto. apply destroyed_by_load_caller_save. auto. - (* Lstore *) @@ -2020,7 +2046,16 @@ Proof. eapply external_call_symbols_preserved; eauto. apply senv_preserved. eapply match_states_intro with (j := j'); eauto with coqlib. eapply match_stacks_change_meminj; eauto. - apply agree_regs_set_res; auto. apply agree_regs_undef_regs; auto. eapply agree_regs_inject_incr; eauto. + eapply agree_regs_set_res; eauto. apply agree_regs_undef_regs; auto. eapply agree_regs_inject_incr; eauto. + inversion WTS; subst. simpl in WTC; InvBooleans. + unfold wt_builtin_res in H3. + unfold Val.has_type_builtin_res. + apply external_call_well_typed in H0. + destruct res; auto. + eapply Val.has_subtype; eauto. + InvBooleans; split. + eapply Val.has_subtype; eauto. destruct vres; auto; constructor. + eapply Val.has_subtype; eauto. destruct vres; auto; constructor. apply agree_locs_set_res; auto. apply agree_locs_undef_regs; auto. apply frame_set_res. apply frame_undef_regs. apply frame_contents_incr with j; auto. rewrite sep_swap2. apply stack_contents_change_meminj with j; auto. rewrite sep_swap2. @@ -2114,6 +2149,8 @@ Proof. eapply match_states_return with (j := j'). eapply match_stacks_change_meminj; eauto. apply agree_regs_set_pair. apply agree_regs_inject_incr with j; auto. auto. + apply external_call_well_typed in H0. + apply loc_result_has_type; auto. apply agree_callee_save_set_result; auto. apply stack_contents_change_meminj with j; auto. rewrite sep_comm, sep_assoc; auto. diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index c6644cebb1..2dc1d78c93 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -271,7 +271,7 @@ Lemma locmap_set_undef_lessdef: locmap_lessdef ls1 ls2 -> locmap_lessdef (Locmap.set l Vundef ls1) ls2. Proof. intros; red; intros l'. unfold Locmap.set. destruct (Loc.eq l l'). -- destruct l; auto. destruct ty; auto. +- subst. destruct (Loc.type l'); auto. - destruct (Loc.diff_dec l l'); auto. Qed. diff --git a/backend/XTL.ml b/backend/XTL.ml index f10efeedbc..d39b38b8fd 100644 --- a/backend/XTL.ml +++ b/backend/XTL.ml @@ -142,10 +142,10 @@ let rec type_builtin_args al tyl = | a :: al, ty :: tyl -> type_builtin_arg a ty; type_builtin_args al tyl | _, _ -> raise Type_error -let rec type_builtin_res a ty = +let type_builtin_res a ty = match a with | BR v -> set_var_type v ty - | BR_splitlong(a1, a2) -> type_builtin_res a1 Tint; type_builtin_res a2 Tint + | BR_splitlong(a1, a2) -> set_var_type a1 Tint; set_var_type a2 Tint | _ -> () let type_instr = function diff --git a/common/AST.v b/common/AST.v index a072ef2934..d4ea7e4f31 100644 --- a/common/AST.v +++ b/common/AST.v @@ -633,7 +633,7 @@ Inductive builtin_arg (A: Type) : Type := Inductive builtin_res (A: Type) : Type := | BR (x: A) | BR_none - | BR_splitlong (hi lo: builtin_res A). + | BR_splitlong (hi lo: A). Fixpoint globals_of_builtin_arg (A: Type) (a: builtin_arg A) : list ident := match a with @@ -658,11 +658,11 @@ Fixpoint params_of_builtin_arg (A: Type) (a: builtin_arg A) : list A := Definition params_of_builtin_args (A: Type) (al: list (builtin_arg A)) : list A := List.fold_right (fun a l => params_of_builtin_arg a ++ l) nil al. -Fixpoint params_of_builtin_res (A: Type) (a: builtin_res A) : list A := +Definition params_of_builtin_res (A: Type) (a: builtin_res A) : list A := match a with | BR x => x :: nil | BR_none => nil - | BR_splitlong hi lo => params_of_builtin_res hi ++ params_of_builtin_res lo + | BR_splitlong hi lo => hi :: lo :: nil end. Fixpoint map_builtin_arg (A B: Type) (f: A -> B) (a: builtin_arg A) : builtin_arg B := @@ -682,12 +682,11 @@ Fixpoint map_builtin_arg (A B: Type) (f: A -> B) (a: builtin_arg A) : builtin_ar BA_addptr (map_builtin_arg f a1) (map_builtin_arg f a2) end. -Fixpoint map_builtin_res (A B: Type) (f: A -> B) (a: builtin_res A) : builtin_res B := +Definition map_builtin_res (A B: Type) (f: A -> B) (a: builtin_res A) : builtin_res B := match a with | BR x => BR (f x) | BR_none => BR_none - | BR_splitlong hi lo => - BR_splitlong (map_builtin_res f hi) (map_builtin_res f lo) + | BR_splitlong hi lo => BR_splitlong (f hi) (f lo) end. (** Which kinds of builtin arguments are supported by which external function. *) diff --git a/common/PrintAST.ml b/common/PrintAST.ml index ac7d22766f..8cd0f2a080 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -80,10 +80,8 @@ let rec print_builtin_args px oc = function | a1 :: al -> fprintf oc "%a, %a" (print_builtin_arg px) a1 (print_builtin_args px) al -let rec print_builtin_res px oc = function +let print_builtin_res px oc = function | BR x -> px oc x | BR_none -> fprintf oc "_" - | BR_splitlong(hi, lo) -> - fprintf oc "splitlong(%a, %a)" - (print_builtin_res px) hi (print_builtin_res px) lo + | BR_splitlong(hi, lo) -> fprintf oc "splitlong(%a, %a)" px hi px lo diff --git a/common/Values.v b/common/Values.v index 802d827b44..58a43885da 100644 --- a/common/Values.v +++ b/common/Values.v @@ -89,6 +89,19 @@ Definition has_type (v: val) (t: typ) : Prop := | _, _ => False end. +Definition has_type_rpair {A} (v: val) (p: rpair A) (lof hif: val -> val) (tf: A -> typ) : Prop := + match p with + | One r => has_type v (tf r) + | Twolong hi lo => has_type (lof v) (tf lo) /\ has_type (hif v) (tf hi) + end. + +Definition has_type_builtin_res {A} (v: val) (r: builtin_res A) (lof hif: val -> val) (tf: A -> typ) : Prop := + match r with + | BR_none => True + | BR r => has_type v (tf r) + | BR_splitlong hi lo => has_type (lof v) (tf lo) /\ has_type (hif v) (tf hi) + end. + Fixpoint has_type_list (vl: list val) (tl: list typ) {struct vl} : Prop := match vl, tl with | nil, nil => True @@ -132,6 +145,35 @@ Proof. simpl in *. InvBooleans. destruct H0. split; auto. eapply has_subtype; eauto. Qed. +Definition has_type_b (v: val) (t: typ) : bool := + match v, t with + | Vundef, _ => true + | Vint _, Tint => true + | Vlong _, Tlong => true + | Vfloat _, Tfloat => true + | Vsingle _, Tsingle => true + | Vptr _ _, Tint => negb Archi.ptr64 + | Vptr _ _, Tlong => Archi.ptr64 + | (Vint _ | Vsingle _), Tany32 => true + | Vptr _ _, Tany32 => negb Archi.ptr64 + | _, Tany64 => true + | _, _ => false + end. + +Program Definition has_type_dec (v: val) (t: typ) : {has_type v t} + {~ has_type v t} := + match has_type_b v t with + | true => left _ + | false => right _ + end. +Next Obligation. + destruct v, t; simpl in *; auto; try congruence; destruct Archi.ptr64; auto. +Qed. +Next Obligation. + destruct v, t; simpl in *; auto; try congruence. + apply eq_sym, negb_false_iff in Heq_anonymous. congruence. + apply eq_sym, negb_false_iff in Heq_anonymous. congruence. +Qed. + (** Truth values. Non-zero integers are treated as [True]. The integer 0 (also used to represent the null pointer) is [False]. Other values are neither true nor false. *) diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 746a610b7b..c2277b8af3 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -454,11 +454,11 @@ Definition set_pair (p: rpair preg) (v: val) (rs: regset) : regset := (** Assigning the result of a builtin *) -Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset := +Definition set_res (res: builtin_res preg) (v: val) (rs: regset) : regset := match res with | BR r => rs#r <- v | BR_none => rs - | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs) + | BR_splitlong hi lo => rs #hi <- (Val.hiword v) #lo <- (Val.loword v) end. Section RELSEM. diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index deab77033e..80a535e916 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -275,7 +275,7 @@ let expand_builtin_vload_1 chunk addr res = (fun r c -> emit (Pld(res, c, r))) (fun r1 r2 -> emit (Pldx(res, r1, r2))) addr GPR11 - | Mint64, BR_splitlong(BR(IR hi), BR(IR lo)) -> + | Mint64, BR_splitlong(IR hi, IR lo) -> expand_volatile_access (fun r c -> match offset_constant c _4 with @@ -517,24 +517,24 @@ let expand_builtin_inline name args res = emit (Pcfi_adjust _m8) (* 64-bit integer arithmetic *) | "__builtin_negl", [BA_splitlong(BA(IR ah), BA(IR al))], - BR_splitlong(BR(IR rh), BR(IR rl)) -> + BR_splitlong(IR rh, IR rl) -> expand_int64_arith (rl = ah) rl (fun rl -> emit (Psubfic(rl, al, Cint _0)); emit (Psubfze(rh, ah))) | "__builtin_addl", [BA_splitlong(BA(IR ah), BA(IR al)); BA_splitlong(BA(IR bh), BA(IR bl))], - BR_splitlong(BR(IR rh), BR(IR rl)) -> + BR_splitlong(IR rh, IR rl) -> expand_int64_arith (rl = ah || rl = bh) rl (fun rl -> emit (Paddc(rl, al, bl)); emit (Padde(rh, ah, bh))) | "__builtin_subl", [BA_splitlong(BA(IR ah), BA(IR al)); BA_splitlong(BA(IR bh), BA(IR bl))], - BR_splitlong(BR(IR rh), BR(IR rl)) -> + BR_splitlong(IR rh, IR rl) -> expand_int64_arith (rl = ah || rl = bh) rl (fun rl -> emit (Psubfc(rl, bl, al)); emit (Psubfe(rh, bh, ah))) | "__builtin_mull", [BA(IR a); BA(IR b)], - BR_splitlong(BR(IR rh), BR(IR rl)) -> + BR_splitlong(IR rh, IR rl) -> expand_int64_arith (rl = a || rl = b) rl (fun rl -> emit (Pmullw(rl, a, b)); emit (Pmulhwu(rh, a, b))) diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v index 1de55c1af8..bf2f541bbd 100644 --- a/powerpc/Conventions1.v +++ b/powerpc/Conventions1.v @@ -16,6 +16,7 @@ Require Import Coqlib. Require Import Decidableplus. Require Import AST. +Require Import Values. Require Import Events. Require Import Locations. Require Archi. @@ -144,6 +145,22 @@ Proof. destruct Archi.ptr64 eqn:?; destruct (sig_res sig) as [[]|]; destruct Archi.ppc64; simpl; auto. Qed. +Lemma loc_result_has_type: + forall res sig, + Val.has_type res (proj_sig_res sig) -> + Val.has_type_rpair res (loc_result sig) Val.loword Val.hiword mreg_type. +Proof. + intros. unfold Val.has_type_rpair, loc_result, proj_sig_res in *. +Local Transparent Archi.ptr64. + assert (P: Archi.ptr64 = false) by (unfold Archi.ptr64; auto). + destruct sig; simpl. destruct sig_res; simpl in H. + destruct t, res; simpl; auto; + simpl; try rewrite P; auto; + destruct Archi.ppc64 eqn:Q; simpl; try rewrite Q; auto. + destruct res; simpl; auto; destruct Archi.ppc64; auto. +Qed. +Local Opaque Archi.ptr64. + (** The result locations are caller-save registers *) Lemma loc_result_caller_save: diff --git a/powerpc/Op.v b/powerpc/Op.v index e6f942c1fd..d3bd30ac9e 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -602,6 +602,17 @@ Proof. intros; discriminate. Qed. +Lemma is_not_move_operation: + forall (F V A: Type) (genv: Genv.t F V) (sp: val) + (op: operation) (f: A -> val) (args: list A) (m: mem) (v: val), + eval_operation genv sp op (map f args) m = Some v -> + is_move_operation op args = None -> + op <> Omove. +Proof. + intros. destruct (eq_operation op Omove); auto. + subst. destruct args; try destruct args; simpl in *; congruence. +Qed. + (** [negate_condition cond] returns a condition that is logically equivalent to the negation of [cond]. *) diff --git a/riscV/Asm.v b/riscV/Asm.v index 4cd3b1fd0f..db7bddadf5 100644 --- a/riscV/Asm.v +++ b/riscV/Asm.v @@ -483,11 +483,11 @@ Fixpoint set_regs (rl: list preg) (vl: list val) (rs: regset) : regset := (** Assigning the result of a builtin *) -Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset := +Definition set_res (res: builtin_res preg) (v: val) (rs: regset) : regset := match res with | BR r => rs#r <- v | BR_none => rs - | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs) + | BR_splitlong hi lo => rs #hi <- (Val.hiword v) #lo <- (Val.loword v) end. Section RELSEM. diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml index d42f4d134c..164f11e7b8 100644 --- a/riscV/Asmexpand.ml +++ b/riscV/Asmexpand.ml @@ -224,7 +224,7 @@ let expand_builtin_vload_common chunk base ofs res = emit (Plw (res, base, Ofsimm ofs)) | Mint64, BR(IR res) -> emit (Pld (res, base, Ofsimm ofs)) - | Mint64, BR_splitlong(BR(IR res1), BR(IR res2)) -> + | Mint64, BR_splitlong(IR res1, IR res2) -> let ofs' = Ptrofs.add ofs _4 in if base <> res2 then begin emit (Plw (res2, base, Ofsimm ofs)); @@ -414,7 +414,7 @@ let expand_builtin_inline name args res = | "__builtin_bswap64", [BA(IR a1)], BR(IR res) -> expand_bswap64 res a1 | "__builtin_bswap64", [BA_splitlong(BA(IR ah), BA(IR al))], - BR_splitlong(BR(IR rh), BR(IR rl)) -> + BR_splitlong(IR rh, IR rl) -> assert (ah = X6 && al = X5 && rh = X5 && rl = X6); expand_bswap32 X5 X5; expand_bswap32 X6 X6 @@ -437,7 +437,7 @@ let expand_builtin_inline name args res = emit (Pfmaxd(res, a1, a2)) (* 64-bit integer arithmetic for a 32-bit platform *) | "__builtin_negl", [BA_splitlong(BA(IR ah), BA(IR al))], - BR_splitlong(BR(IR rh), BR(IR rl)) -> + BR_splitlong(IR rh, IR rl) -> expand_int64_arith (rl = ah) rl (fun rl -> emit (Psltuw (X1, X0, X al)); @@ -446,7 +446,7 @@ let expand_builtin_inline name args res = emit (Psubw (rh, X rh, X X1))) | "__builtin_addl", [BA_splitlong(BA(IR ah), BA(IR al)); BA_splitlong(BA(IR bh), BA(IR bl))], - BR_splitlong(BR(IR rh), BR(IR rl)) -> + BR_splitlong(IR rh, IR rl) -> expand_int64_arith (rl = bl || rl = ah || rl = bh) rl (fun rl -> emit (Paddw (rl, X al, X bl)); @@ -455,7 +455,7 @@ let expand_builtin_inline name args res = emit (Paddw (rh, X rh, X X1))) | "__builtin_subl", [BA_splitlong(BA(IR ah), BA(IR al)); BA_splitlong(BA(IR bh), BA(IR bl))], - BR_splitlong(BR(IR rh), BR(IR rl)) -> + BR_splitlong(IR rh, IR rl) -> expand_int64_arith (rl = ah || rl = bh) rl (fun rl -> emit (Psltuw (X1, X al, X bl)); @@ -463,7 +463,7 @@ let expand_builtin_inline name args res = emit (Psubw (rh, X ah, X bh)); emit (Psubw (rh, X rh, X X1))) | "__builtin_mull", [BA(IR a); BA(IR b)], - BR_splitlong(BR(IR rh), BR(IR rl)) -> + BR_splitlong(IR rh, IR rl) -> expand_int64_arith (rl = a || rl = b) rl (fun rl -> emit (Pmulw (rl, X a, X b)); diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v index df7ddfd20d..8f5d8f6ca6 100644 --- a/riscV/Conventions1.v +++ b/riscV/Conventions1.v @@ -19,7 +19,7 @@ machine registers and stack slots. *) Require Import Coqlib Decidableplus. -Require Import AST Machregs Locations. +Require Import AST Values Machregs Locations. (** * Classification of machine registers *) @@ -132,6 +132,17 @@ Proof. destruct (sig_res sig) as [[]|]; auto; destruct Archi.ptr64; auto. Qed. +Lemma loc_result_has_type: + forall res sig, + Val.has_type res (proj_sig_res sig) -> + Val.has_type_rpair res (loc_result sig) Val.loword Val.hiword mreg_type. +Proof. + intros. unfold Val.has_type_rpair, loc_result, proj_sig_res in *. + destruct sig; simpl. destruct sig_res; simpl in H. + destruct t, res; simpl; auto; destruct Archi.ptr64 eqn:P; simpl; try rewrite P; auto. + destruct res; simpl; auto; destruct Archi.ptr64; auto. +Qed. + (** The result locations are caller-save registers *) Lemma loc_result_caller_save: diff --git a/riscV/Op.v b/riscV/Op.v index bb04f78641..7c401cec01 100644 --- a/riscV/Op.v +++ b/riscV/Op.v @@ -691,6 +691,17 @@ Proof. intros; discriminate. Qed. +Lemma is_not_move_operation: + forall (F V A: Type) (genv: Genv.t F V) (sp: val) + (op: operation) (f: A -> val) (args: list A) (m: mem) (v: val), + eval_operation genv sp op (map f args) m = Some v -> + is_move_operation op args = None -> + op <> Omove. +Proof. + intros. destruct (eq_operation op Omove); auto. + subst. destruct args; try destruct args; simpl in *; congruence. +Qed. + (** [negate_condition cond] returns a condition that is logically equivalent to the negation of [cond]. *) diff --git a/x86/Asm.v b/x86/Asm.v index 8b873e48ac..c0a7076c2d 100644 --- a/x86/Asm.v +++ b/x86/Asm.v @@ -333,11 +333,11 @@ Definition set_pair (p: rpair preg) (v: val) (rs: regset) : regset := (** Assigning the result of a builtin *) -Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset := +Definition set_res (res: builtin_res preg) (v: val) (rs: regset) : regset := match res with | BR r => rs#r <- v | BR_none => rs - | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs) + | BR_splitlong hi lo => rs #hi <- (Val.hiword v) #lo <- (Val.loword v) end. Section RELSEM. diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml index 1b71616549..4097f59afe 100644 --- a/x86/Asmexpand.ml +++ b/x86/Asmexpand.ml @@ -173,7 +173,7 @@ let expand_builtin_vload_common chunk addr res = emit (Pmovl_rm (res,addr)) | Mint64, BR(IR res) -> emit (Pmovq_rm (res,addr)) - | Mint64, BR_splitlong(BR(IR res1), BR(IR res2)) -> + | Mint64, BR_splitlong(IR res1, IR res2) -> let addr' = offset_addressing addr _4z in if not (Asmgen.addressing_mentions addr res2) then begin emit (Pmovl_rm (res2,addr)); @@ -323,7 +323,7 @@ let expand_builtin_inline name args res = emit (Pmov_rr (res,a1)); emit (Pbswap64 res) | "__builtin_bswap64", [BA_splitlong(BA(IR ah), BA(IR al))], - BR_splitlong(BR(IR rh), BR(IR rl)) -> + BR_splitlong(IR rh, IR rl) -> assert (ah = RAX && al = RDX && rh = RDX && rl = RAX); emit (Pbswap32 RAX); emit (Pbswap32 RDX) @@ -411,25 +411,25 @@ let expand_builtin_inline name args res = (fun r1 r2 r3 -> Pfnmsub231(r1, r2, r3)) (* 64-bit integer arithmetic *) | "__builtin_negl", [BA_splitlong(BA(IR ah), BA(IR al))], - BR_splitlong(BR(IR rh), BR(IR rl)) -> + BR_splitlong(IR rh, IR rl) -> assert (ah = RDX && al = RAX && rh = RDX && rl = RAX); emit (Pnegl RAX); emit (Padcl_ri (RDX,_0)); emit (Pnegl RDX) | "__builtin_addl", [BA_splitlong(BA(IR ah), BA(IR al)); BA_splitlong(BA(IR bh), BA(IR bl))], - BR_splitlong(BR(IR rh), BR(IR rl)) -> + BR_splitlong(IR rh, IR rl) -> assert (ah = RDX && al = RAX && bh = RCX && bl = RBX && rh = RDX && rl = RAX); emit (Paddl_rr (RAX,RBX)); emit (Padcl_rr (RDX,RCX)) | "__builtin_subl", [BA_splitlong(BA(IR ah), BA(IR al)); BA_splitlong(BA(IR bh), BA(IR bl))], - BR_splitlong(BR(IR rh), BR(IR rl)) -> + BR_splitlong(IR rh, IR rl) -> assert (ah = RDX && al = RAX && bh = RCX && bl = RBX && rh = RDX && rl = RAX); emit (Psubl_rr (RAX,RBX)); emit (Psbbl_rr (RDX,RCX)) | "__builtin_mull", [BA(IR a); BA(IR b)], - BR_splitlong(BR(IR rh), BR(IR rl)) -> + BR_splitlong(IR rh, IR rl) -> assert (a = RAX && b = RDX && rh = RDX && rl = RAX); emit (Pmull_r RDX) (* Memory accesses *) diff --git a/x86/Conventions1.v b/x86/Conventions1.v index 646c4afb31..2f4b4da5fc 100644 --- a/x86/Conventions1.v +++ b/x86/Conventions1.v @@ -14,7 +14,7 @@ machine registers and stack slots. *) Require Import Coqlib Decidableplus. -Require Import AST Machregs Locations. +Require Import AST Values Machregs Locations. (** * Classification of machine registers *) @@ -130,6 +130,17 @@ Proof. destruct Archi.ptr64; destruct (sig_res sig) as [[]|]; auto. Qed. +Lemma loc_result_has_type: + forall res sig, + Val.has_type res (proj_sig_res sig) -> + Val.has_type_rpair res (loc_result sig) Val.loword Val.hiword mreg_type. +Proof. + intros. unfold Val.has_type_rpair, loc_result, proj_sig_res in *. + destruct sig; simpl. destruct sig_res; simpl in H. + destruct t, res; simpl; auto; destruct Archi.ptr64 eqn:P; simpl; try rewrite P; auto. + destruct res; simpl; auto; destruct Archi.ptr64 eqn:P; simpl; try rewrite P; auto. +Qed. + (** The result locations are caller-save registers *) Lemma loc_result_caller_save: diff --git a/x86/Op.v b/x86/Op.v index 02b0457493..b37e37d739 100644 --- a/x86/Op.v +++ b/x86/Op.v @@ -746,6 +746,17 @@ Proof. intros; discriminate. Qed. +Lemma is_not_move_operation: + forall (F V A: Type) (genv: Genv.t F V) (sp: val) + (op: operation) (f: A -> val) (args: list A) (m: mem) (v: val), + eval_operation genv sp op (map f args) m = Some v -> + is_move_operation op args = None -> + op <> Omove. +Proof. + intros. destruct (eq_operation op Omove); auto. + subst. destruct args; try destruct args; simpl in *; congruence. +Qed. + (** [negate_condition cond] returns a condition that is logically equivalent to the negation of [cond]. *)