diff options
Diffstat (limited to 'backend')
-rw-r--r-- | backend/Allocation.v | 134 | ||||
-rw-r--r-- | backend/Allocproof.v | 338 | ||||
-rw-r--r-- | backend/Asmgenproof0.v | 6 | ||||
-rw-r--r-- | backend/Bounds.v | 22 | ||||
-rw-r--r-- | backend/CSEproof.v | 4 | ||||
-rw-r--r-- | backend/Cminor.v | 2 | ||||
-rw-r--r-- | backend/Constpropproof.v | 20 | ||||
-rw-r--r-- | backend/Conventions.v | 8 | ||||
-rw-r--r-- | backend/Deadcodeproof.v | 2 | ||||
-rw-r--r-- | backend/Inliningproof.v | 2 | ||||
-rw-r--r-- | backend/Inliningspec.v | 10 | ||||
-rw-r--r-- | backend/Lineartyping.v | 2 | ||||
-rw-r--r-- | backend/Locations.v | 4 | ||||
-rw-r--r-- | backend/PrintAsmaux.ml | 1 | ||||
-rw-r--r-- | backend/RTLtyping.v | 2 | ||||
-rw-r--r-- | backend/Regalloc.ml | 40 | ||||
-rw-r--r-- | backend/SelectDiv.vp | 12 | ||||
-rw-r--r-- | backend/SelectDivproof.v | 50 | ||||
-rw-r--r-- | backend/Selection.v | 4 | ||||
-rw-r--r-- | backend/Selectionproof.v | 63 | ||||
-rw-r--r-- | backend/SplitLong.vp | 4 | ||||
-rw-r--r-- | backend/SplitLongproof.v | 20 | ||||
-rw-r--r-- | backend/Stackingproof.v | 152 | ||||
-rw-r--r-- | backend/Tailcallproof.v | 4 | ||||
-rw-r--r-- | backend/Unusedglobproof.v | 96 | ||||
-rw-r--r-- | backend/ValueAnalysis.v | 16 | ||||
-rw-r--r-- | backend/ValueDomain.v | 35 |
27 files changed, 711 insertions, 342 deletions
diff --git a/backend/Allocation.v b/backend/Allocation.v index f561ef4e..3dd4cb09 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -39,7 +39,12 @@ Require Import Op Registers RTL Locations Conventions RTLtyping LTL. maching between an RTL instruction and an LTL basic block. *) -Definition move := (loc * loc)%type. +Inductive move: Type := + | MV (src dst: loc) + | MVmakelong (src1 src2 dst: mreg) + | MVlowlong (src dst: mreg) + | MVhighlong (src dst: mreg). + Definition moves := list move. Inductive block_shape: Type := @@ -110,18 +115,22 @@ Definition classify_operation {A: Type} (op: operation) (args: list A) : operati end. (** Extract the move instructions at the beginning of block [b]. - Return the list of moves and the suffix of [b] after the moves. *) + Return the list of moves and the suffix of [b] after the moves. + Two versions are provided: [extract_moves], which extracts only + "true" moves, and [extract_moves_ext], which also extracts + the [makelong], [lowlong] and [highlong] operations over 64-bit integers. +*) Fixpoint extract_moves (accu: moves) (b: bblock) {struct b} : moves * bblock := match b with | Lgetstack sl ofs ty dst :: b' => - extract_moves ((S sl ofs ty, R dst) :: accu) b' + extract_moves (MV (S sl ofs ty) (R dst) :: accu) b' | Lsetstack src sl ofs ty :: b' => - extract_moves ((R src, S sl ofs ty) :: accu) b' + extract_moves (MV (R src) (S sl ofs ty) :: accu) b' | Lop op args res :: b' => match is_move_operation op args with | Some arg => - extract_moves ((R arg, R res) :: accu) b' + extract_moves (MV (R arg) (R res) :: accu) b' | None => (List.rev accu, b) end @@ -129,6 +138,29 @@ Fixpoint extract_moves (accu: moves) (b: bblock) {struct b} : moves * bblock := (List.rev accu, b) end. +Fixpoint extract_moves_ext (accu: moves) (b: bblock) {struct b} : moves * bblock := + match b with + | Lgetstack sl ofs ty dst :: b' => + extract_moves_ext (MV (S sl ofs ty) (R dst) :: accu) b' + | Lsetstack src sl ofs ty :: b' => + extract_moves_ext (MV (R src) (S sl ofs ty) :: accu) b' + | Lop op args res :: b' => + match classify_operation op args with + | operation_Omove arg => + extract_moves_ext (MV (R arg) (R res) :: accu) b' + | operation_Omakelong arg1 arg2 => + extract_moves_ext (MVmakelong arg1 arg2 res :: accu) b' + | operation_Olowlong arg => + extract_moves_ext (MVlowlong arg res :: accu) b' + | operation_Ohighlong arg => + extract_moves_ext (MVhighlong arg res :: accu) b' + | operation_other _ _ => + (List.rev accu, b) + end + | _ => + (List.rev accu, b) + end. + Definition check_succ (s: node) (b: LTL.bblock) : bool := match b with | Lbranch s' :: _ => peq s s' @@ -251,17 +283,17 @@ Definition pair_instr_block | _ => None end | Icall sg ros args res s => - let (mv1, b1) := extract_moves nil b in + let (mv1, b1) := extract_moves_ext nil b in match b1 with | Lcall sg' ros' :: b2 => - let (mv2, b3) := extract_moves nil b2 in + let (mv2, b3) := extract_moves_ext nil b2 in assertion (signature_eq sg sg'); assertion (check_succ s b3); Some(BScall sg ros args res mv1 ros' mv2 s) | _ => None end | Itailcall sg ros args => - let (mv1, b1) := extract_moves nil b in + let (mv1, b1) := extract_moves_ext nil b in match b1 with | Ltailcall sg' ros' :: b2 => assertion (signature_eq sg sg'); @@ -297,7 +329,7 @@ Definition pair_instr_block | _ => None end | Ireturn arg => - let (mv1, b1) := extract_moves nil b in + let (mv1, b1) := extract_moves_ext nil b in match b1 with | Lreturn :: b2 => Some(BSreturn arg mv1) | _ => None @@ -319,7 +351,7 @@ Definition pair_codes (f1: RTL.function) (f2: LTL.function) : PTree.t block_shap Definition pair_entrypoints (f1: RTL.function) (f2: LTL.function) : option moves := do b <- (LTL.fn_code f2)!(LTL.fn_entrypoint f2); - let (mv, b1) := extract_moves nil b in + let (mv, b1) := extract_moves_ext nil b in assertion (check_succ (RTL.fn_entrypoint f1) b1); Some mv. @@ -602,6 +634,55 @@ Definition subst_loc (l1 l2: loc) (e: eqs) : option eqs := (EqSet2.elements_between (select_loc_l l1) (select_loc_h l1) (eqs2 e)) (Some e). +(** [subst_loc_part l1 l2 k e] simulates the effect of assigning + [l2] to the [k] part of [l1] on [e]. + All equations of the form [r = l1 [k]] are replaced by [r = l2 [Full]]. + Return [None] if [e] contains an equation of the form [r = l] with [l] + partially overlapping [l1], or an equation of the form [r = l1] with + a kind different from [k1]. +*) + +Definition subst_loc_part (l1: loc) (l2: loc) (k: equation_kind) (e: eqs) : option eqs := + EqSet2.fold + (fun q opte => + match opte with + | None => None + | Some e => + if Loc.eq l1 (eloc q) then + if IndexedEqKind.eq (ekind q) k + then Some (add_equation (Eq Full (ereg q) l2) (remove_equation q e)) + else None + else + None + end) + (EqSet2.elements_between (select_loc_l l1) (select_loc_h l1) (eqs2 e)) + (Some e). + +(** [subst_loc_pair l1 l2 l2'] simulates the effect of assigning + [makelong l2 l2'] to [l1]. All equations of the form [r = l1 [Full]] + are replaced by the two equations [r = l2 [High], r = l2' [Low]]. + Return [None] if [e] contains an equation of the form [r = l] with [l] + partially overlapping [l1], or an equation of the form [r = l1] with + a kind different from [Full]. *) + +Definition subst_loc_pair (l1 l2 l2': loc) (e: eqs) : option eqs := + EqSet2.fold + (fun q opte => + match opte with + | None => None + | Some e => + if Loc.eq l1 (eloc q) then + if IndexedEqKind.eq (ekind q) Full + then Some (add_equation (Eq High (ereg q) l2) + (add_equation (Eq Low (ereg q) l2') + (remove_equation q e))) + else None + else + None + end) + (EqSet2.elements_between (select_loc_l l1) (select_loc_h l1) (eqs2 e)) + (Some e). + (** [loc_type_compat env l e] checks that for all equations [r = l] in [e], the type [env r] of [r] is compatible with the type of [l]. *) @@ -616,6 +697,14 @@ Definition loc_type_compat (env: regenv) (l: loc) (e: eqs) : bool := (fun q => subtype (sel_type (ekind q) (env (ereg q))) (Loc.type l)) (select_loc_l l) (select_loc_h l) (eqs2 e). +(** [long_type_compat env l e] checks that for all equations [r = l] in [e]. + then type [env r] of [r] is compatible with the type [Tlong]. *) + +Definition long_type_compat (env: regenv) (l: loc) (e: eqs) : bool := + EqSet2.for_all_between + (fun q => subtype (env (ereg q)) Tlong) + (select_loc_l l) (select_loc_h l) (eqs2 e). + (** [add_equations [r1...rN] [m1...mN] e] adds to [e] the [N] equations [ri = R mi [Full]]. Return [None] if the two lists have different lengths. *) @@ -637,9 +726,8 @@ Function add_equations_args (rl: list reg) (tyl: list typ) (ll: list (rpair loc) | r1 :: rl, ty :: tyl, One l1 :: ll => add_equations_args rl tyl ll (add_equation (Eq Full r1 l1) e) | r1 :: rl, Tlong :: tyl, Twolong l1 l2 :: ll => - if Archi.splitlong then - add_equations_args rl tyl ll (add_equation (Eq Low r1 l2) (add_equation (Eq High r1 l1) e)) - else None + if Archi.ptr64 then None else + add_equations_args rl tyl ll (add_equation (Eq Low r1 l2) (add_equation (Eq High r1 l1) e)) | _, _, _ => None end. @@ -651,9 +739,8 @@ Function add_equations_res (r: reg) (oty: option typ) (p: rpair mreg) (e: eqs) : | One mr, _ => Some (add_equation (Eq Full r (R mr)) e) | Twolong mr1 mr2, Some Tlong => - if Archi.splitlong then - Some (add_equation (Eq Low r (R mr2)) (add_equation (Eq High r (R mr1)) e)) - else None + if Archi.ptr64 then None else + Some (add_equation (Eq Low r (R mr2)) (add_equation (Eq High r (R mr1)) e)) | _, _ => None end. @@ -857,11 +944,24 @@ Definition well_typed_move (env: regenv) (dst: loc) (e: eqs) : bool := Fixpoint track_moves (env: regenv) (mv: moves) (e: eqs) : option eqs := match mv with | nil => Some e - | (src, dst) :: mv => + | 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); subst_loc dst src e1 + | MVmakelong src1 src2 dst :: mv => + assertion (negb Archi.ptr64); + do e1 <- track_moves env mv e; + assertion (long_type_compat env (R dst) e1); + subst_loc_pair (R dst) (R src1) (R src2) e1 + | MVlowlong src dst :: mv => + assertion (negb Archi.ptr64); + do e1 <- track_moves env mv e; + subst_loc_part (R dst) (R src) Low e1 + | MVhighlong src dst :: mv => + assertion (negb Archi.ptr64); + do e1 <- track_moves env mv e; + subst_loc_part (R dst) (R src) High e1 end. (** [transfer_use_def args res args' res' undefs e] returns the set diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 888945ec..3b2ecd35 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -34,10 +34,13 @@ Qed. Definition expand_move (m: move) : instruction := match m with - | (R src, R dst) => Lop Omove (src::nil) dst - | (S sl ofs ty, R dst) => Lgetstack sl ofs ty dst - | (R src, S sl ofs ty) => Lsetstack src sl ofs ty - | (S _ _ _, S _ _ _) => Lreturn (**r should never happen *) + | MV (R src) (R dst) => Lop Omove (src::nil) dst + | MV (S sl ofs ty) (R dst) => Lgetstack sl ofs ty dst + | MV (R src) (S sl ofs ty) => Lsetstack src sl ofs ty + | MV (S _ _ _) (S _ _ _) => Lreturn (**r should never happen *) + | MVmakelong src1 src2 dst => Lop Omakelong (src1::src2::nil) dst + | MVlowlong src dst => Lop Olowlong (src::nil) dst + | MVhighlong src dst => Lop Ohighlong (src::nil) dst end. Definition expand_moves (mv: moves) (k: bblock) : bblock := @@ -45,7 +48,7 @@ Definition expand_moves (mv: moves) (k: bblock) : bblock := Definition wf_move (m: move) : Prop := match m with - | (S _ _ _, S _ _ _) => False + | MV (S _ _ _) (S _ _ _) => False | _ => True end. @@ -64,17 +67,20 @@ Inductive expand_block_shape: block_shape -> RTL.instruction -> LTL.bblock -> Pr (Iop Omove (src :: nil) dst s) (expand_moves mv (Lbranch s :: k)) | ebs_makelong: forall src1 src2 dst mv s k, - wf_moves mv -> Archi.splitlong = true -> + wf_moves mv -> + Archi.splitlong = true -> expand_block_shape (BSmakelong src1 src2 dst mv s) (Iop Omakelong (src1 :: src2 :: nil) dst s) (expand_moves mv (Lbranch s :: k)) | ebs_lowlong: forall src dst mv s k, - wf_moves mv -> Archi.splitlong = true -> + wf_moves mv -> + Archi.splitlong = true -> expand_block_shape (BSlowlong src dst mv s) (Iop Olowlong (src :: nil) dst s) (expand_moves mv (Lbranch s :: k)) | ebs_highlong: forall src dst mv s k, - wf_moves mv -> Archi.splitlong = true -> + wf_moves mv -> + Archi.splitlong = true -> expand_block_shape (BShighlong src dst mv s) (Iop Ohighlong (src :: nil) dst s) (expand_moves mv (Lbranch s :: k)) @@ -97,7 +103,8 @@ Inductive expand_block_shape: block_shape -> RTL.instruction -> LTL.bblock -> Pr (Lload chunk addr args' dst' :: expand_moves mv2 (Lbranch s :: k))) | ebs_load2: forall addr addr2 args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s k, wf_moves mv1 -> wf_moves mv2 -> wf_moves mv3 -> - Archi.splitlong = true -> offset_addressing addr 4 = Some addr2 -> + Archi.splitlong = true -> + offset_addressing addr 4 = Some addr2 -> expand_block_shape (BSload2 addr addr2 args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s) (Iload Mint64 addr args dst s) (expand_moves mv1 @@ -107,7 +114,7 @@ Inductive expand_block_shape: block_shape -> RTL.instruction -> LTL.bblock -> Pr expand_moves mv3 (Lbranch s :: k)))) | ebs_load2_1: forall addr args dst mv1 args' dst' mv2 s k, wf_moves mv1 -> wf_moves mv2 -> - Archi.splitlong = true -> + Archi.splitlong = true -> expand_block_shape (BSload2_1 addr args dst mv1 args' dst' mv2 s) (Iload Mint64 addr args dst s) (expand_moves mv1 @@ -115,7 +122,8 @@ Inductive expand_block_shape: block_shape -> RTL.instruction -> LTL.bblock -> Pr expand_moves mv2 (Lbranch s :: k))) | ebs_load2_2: forall addr addr2 args dst mv1 args' dst' mv2 s k, wf_moves mv1 -> wf_moves mv2 -> - Archi.splitlong = true -> offset_addressing addr 4 = Some addr2 -> + Archi.splitlong = true -> + offset_addressing addr 4 = Some addr2 -> expand_block_shape (BSload2_2 addr addr2 args dst mv1 args' dst' mv2 s) (Iload Mint64 addr args dst s) (expand_moves mv1 @@ -134,7 +142,8 @@ Inductive expand_block_shape: block_shape -> RTL.instruction -> LTL.bblock -> Pr (Lstore chunk addr args' src' :: Lbranch s :: k)) | ebs_store2: forall addr addr2 args src mv1 args1' src1' mv2 args2' src2' s k, wf_moves mv1 -> wf_moves mv2 -> - Archi.splitlong = true -> offset_addressing addr 4 = Some addr2 -> + Archi.splitlong = true -> + offset_addressing addr 4 = Some addr2 -> expand_block_shape (BSstore2 addr addr2 args src mv1 args1' src1' mv2 args2' src2' s) (Istore Mint64 addr args src s) (expand_moves mv1 @@ -184,7 +193,7 @@ Ltac MonadInv := | [ H: match negb (proj_sumbool ?x) with true => _ | false => None end = Some _ |- _ ] => destruct x; [discriminate|simpl in H; MonadInv] | [ H: match negb ?x with true => _ | false => None end = Some _ |- _ ] => - destruct x; [discriminate|simpl in H; MonadInv] + destruct x as [] eqn:? ; [discriminate|simpl in H; MonadInv] | [ H: match ?x with true => _ | false => None end = Some _ |- _ ] => destruct x as [] eqn:? ; [MonadInv|discriminate] | [ H: match ?x with (_, _) => _ end = Some _ |- _ ] => @@ -233,7 +242,45 @@ Proof. + (* reg-stack move *) exploit IHb; eauto. constructor; auto. exact I. rewrite expand_moves_cons; auto. } - intros. exploit IND; eauto. constructor. + intros. exploit IND; eauto. constructor. +Qed. + +Lemma extract_moves_ext_sound: + forall b mv b', + extract_moves_ext nil b = (mv, b') -> + wf_moves mv /\ b = expand_moves mv b'. +Proof. + assert (BASE: + forall accu b, + wf_moves accu -> + wf_moves (List.rev accu) /\ expand_moves (List.rev accu) b = expand_moves (List.rev accu) b). + { 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', + 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). + + destruct (classify_operation op args). + * (* reg-reg move *) + exploit IHb; eauto. constructor; auto. exact I. rewrite expand_moves_cons; auto. + * (* makelong *) + exploit IHb; eauto. constructor; auto. exact I. rewrite expand_moves_cons; auto. + * (* lowlong *) + exploit IHb; eauto. constructor; auto. exact I. rewrite expand_moves_cons; auto. + * (* highlong *) + exploit IHb; eauto. constructor; auto. exact I. rewrite expand_moves_cons; auto. + * (* default *) + inv H; apply BASE; auto. + + (* stack-reg move *) + exploit IHb; eauto. constructor; auto. exact I. rewrite expand_moves_cons; auto. + + (* reg-stack move *) + exploit IHb; eauto. constructor; auto. exact I. rewrite expand_moves_cons; auto. + } + intros. exploit IND; eauto. constructor. Qed. Lemma check_succ_sound: @@ -248,6 +295,8 @@ 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: check_succ _ _ = true |- _ ] => try (discriminate H); destruct (check_succ_sound _ _ H); clear H; subst; UseParsingLemmas @@ -261,7 +310,7 @@ Proof. assert (OP: forall op args res s b bsh, 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. + unfold pair_Iop_block; intros. MonadInv. destruct b0. MonadInv; UseParsingLemmas. destruct i; MonadInv; UseParsingLemmas. eapply ebs_op; eauto. @@ -290,8 +339,8 @@ Proof. destruct (chunk_eq m Mint64 && Archi.splitlong) eqn:A; MonadInv; UseParsingLemmas. destruct b as [ | [] b]; MonadInv; UseParsingLemmas. InvBooleans. subst m. eapply ebs_load2; eauto. - InvBooleans. subst m. - destruct (eq_addressing a addr). + InvBooleans. subst m. + destruct (eq_addressing a addr). inv H; inv H2. eapply ebs_load2_1; eauto. destruct (option_eq eq_addressing (offset_addressing a 4) (Some addr)). inv H; inv H2. eapply ebs_load2_2; eauto. @@ -418,20 +467,28 @@ Proof. intros until e'. functional induction (add_equations_args rl tyl ll e); intros. - inv H; auto. - eapply add_equation_satisf; eauto. +- discriminate. - eapply add_equation_satisf. eapply add_equation_satisf. eauto. - congruence. -- congruence. Qed. -Lemma val_longofwords_eq: +Lemma val_longofwords_eq_1: forall v, - Val.has_type v Tlong -> Archi.splitlong = true -> + Val.has_type v Tlong -> Archi.ptr64 = false -> Val.longofwords (Val.hiword v) (Val.loword v) = v. Proof. intros. red in H. destruct v; try contradiction. - reflexivity. - simpl. rewrite Int64.ofwords_recompose. auto. -- rewrite Archi.splitlong_ptr32 in H by auto. congruence. +- congruence. +Qed. + +Lemma val_longofwords_eq_2: + forall v, + Val.has_type v Tlong -> Archi.splitlong = true -> + Val.longofwords (Val.hiword v) (Val.loword v) = v. +Proof. + intros. apply Archi.splitlong_ptr32 in H0. apply val_longofwords_eq_1; assumption. Qed. Lemma add_equations_args_lessdef: @@ -445,14 +502,14 @@ Proof. - inv H; auto. - destruct H1. constructor; auto. eapply add_equation_lessdef with (q := Eq Full r1 l1). eapply add_equations_args_satisf; eauto. +- discriminate. - destruct H1. constructor; auto. - rewrite <- (val_longofwords_eq (rs#r1)) by auto. apply Val.longofwords_lessdef. + rewrite <- (val_longofwords_eq_1 (rs#r1)) by auto. apply Val.longofwords_lessdef. eapply add_equation_lessdef with (q := Eq High r1 l1). eapply add_equation_satisf. eapply add_equations_args_satisf; eauto. eapply add_equation_lessdef with (q := Eq Low r1 l2). eapply add_equations_args_satisf; eauto. - discriminate. -- discriminate. Qed. Lemma add_equation_ros_satisf: @@ -676,7 +733,7 @@ Lemma parallel_assignment_satisf_2: Proof. intros. functional inversion H. - (* One location *) - subst. simpl in H2. InvBooleans. simpl. + subst. simpl in H2. InvBooleans. simpl. apply parallel_assignment_satisf with Full; auto. unfold reg_loc_unconstrained. rewrite H1, H4. auto. - (* Two 32-bit halves *) @@ -686,10 +743,10 @@ Proof. 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. 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 by auto. rewrite Locmap.gss. apply Val.hiword_lessdef; auto. assert (EqSet.In q e'). unfold e', remove_equation; simpl; ESD.fsetdec. rewrite Regmap.gso. rewrite ! Locmap.gso. auto. @@ -737,7 +794,7 @@ Proof. { apply ESP.fold_rec; unfold Q; intros. - auto. - - simpl. red in H2. rewrite H2 in H4. ESD.fsetdec. + - simpl. red in H2. rewrite H2 in H4. ESD.fsetdec. } destruct (ESP.In_dec q elt). left. split. apply IN_ELT. auto. apply H. auto. @@ -878,7 +935,7 @@ Lemma partial_fold_ind: f x a' = Some a'' -> P s' a' -> P s'' a'') -> P s final. Proof. - intros. + intros. set (g := fun q opte => match opte with Some e => f q e | None => None end) in *. set (Q := fun s1 opte => match opte with None => True | Some e => P s1 e end). change (Q s (Some final)). @@ -909,7 +966,7 @@ Proof. simpl. rewrite ESF.add_iff, ESF.remove_iff. apply H1 in H4; destruct H4. subst x; rewrite e; auto. - apply H3 in H2; destruct H2. split. congruence. + apply H3 in H2; destruct H2. split. congruence. destruct (OrderedEquation.eq_dec x {| ekind := ekind q; ereg := ereg q; eloc := l2 |}); auto. subst x; auto. } @@ -999,6 +1056,171 @@ Proof. rewrite Locmap.gso; auto. Qed. +Lemma in_subst_loc_part: + forall l1 l2 k q (e e': eqs), + EqSet.In q e -> + subst_loc_part l1 l2 k e = Some e' -> + (eloc q = l1 /\ ekind q = k /\ EqSet.In (Eq Full (ereg q) l2) e') \/ (Loc.diff l1 (eloc q) /\ EqSet.In q e'). +Proof. + unfold subst_loc_part; intros l1 l2 k q e0 e0' IN SUBST. + set (elt := EqSet2.elements_between (select_loc_l l1) (select_loc_h l1) (eqs2 e0)) in *. + set (f := fun q0 e => + if Loc.eq l1 (eloc q0) then + if IndexedEqKind.eq (ekind q0) k then + Some (add_equation + {| ekind := Full; ereg := ereg q0; eloc := l2 |} + (remove_equation q0 e)) + else None else None). + set (P := fun e1 e2 => EqSet2.In q e1 -> eloc q = l1 /\ ekind q = k /\ EqSet.In (Eq Full (ereg q) l2) e2). + assert (A: P elt e0'). + { eapply partial_fold_ind with (f := f) (s := elt) (final := e0'). eexact SUBST. + - unfold P; intros. ESD2.fsetdec. + - unfold P, f; intros. destruct (Loc.eq l1 (eloc x)); try discriminate. + destruct (IndexedEqKind.eq (ekind x) k); inversion H2; subst a''; clear H2. + simpl. rewrite ESF.add_iff, ESF.remove_iff. + apply H1 in H4; destruct H4. + subst x; rewrite e, <- e1; auto. + apply H3 in H2; destruct H2 as (X & Y & Z). split; auto. split; auto. + destruct (OrderedEquation.eq_dec x {| ekind := Full; ereg := ereg q; eloc := l2 |}); auto. + subst x; auto. + } + set (Q := fun e1 e2 => ~EqSet2.In q e1 -> EqSet.In q e2). + assert (B: Q elt e0'). + { eapply partial_fold_ind with (f := f) (s := elt) (final := e0'). eexact SUBST. + - unfold Q; intros. auto. + - unfold Q, f; intros. destruct (Loc.eq l1 (eloc x)); try congruence. + destruct (IndexedEqKind.eq (ekind x) k); inversion H2; subst a''; clear H2. + simpl. rewrite ESF.add_iff, ESF.remove_iff. + red in H1. rewrite H1 in H4. intuition auto. } + destruct (ESP2.In_dec q elt). + left. apply A; auto. + right. split; auto. + rewrite <- select_loc_charact. + destruct (select_loc_l l1 q) eqn: LL; auto. + destruct (select_loc_h l1 q) eqn: LH; auto. + elim n. eapply EqSet2.elements_between_iff. + exact (select_loc_l_monotone l1). + exact (select_loc_h_monotone l1). + split. apply eqs_same; auto. auto. +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' -> + 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 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' -> + 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 Locmap.gso; auto. +Qed. + +Lemma in_subst_loc_pair: + forall l1 l2 l2' q (e e': eqs), + EqSet.In q e -> + subst_loc_pair l1 l2 l2' e = Some e' -> + (eloc q = l1 /\ ekind q = Full /\ EqSet.In (Eq High (ereg q) l2) e' /\ EqSet.In (Eq Low (ereg q) l2') e') + \/ (Loc.diff l1 (eloc q) /\ EqSet.In q e'). +Proof. + unfold subst_loc_pair; intros l1 l2 l2' q e0 e0' IN SUBST. + set (elt := EqSet2.elements_between (select_loc_l l1) (select_loc_h l1) (eqs2 e0)) in *. + set (f := fun q0 e => + if Loc.eq l1 (eloc q0) then + if IndexedEqKind.eq (ekind q0) Full then + Some (add_equation {| ekind := High; ereg := ereg q0; eloc := l2 |} + (add_equation {| ekind := Low; ereg := ereg q0; eloc := l2' |} + (remove_equation q0 e))) + else None else None). + set (P := fun e1 e2 => EqSet2.In q e1 -> eloc q = l1 /\ ekind q = Full + /\ EqSet.In (Eq High (ereg q) l2) e2 + /\ EqSet.In (Eq Low (ereg q) l2') e2). + assert (A: P elt e0'). + { eapply partial_fold_ind with (f := f) (s := elt) (final := e0'). eexact SUBST. + - unfold P; intros. ESD2.fsetdec. + - unfold P, f; intros. destruct (Loc.eq l1 (eloc x)); try discriminate. + destruct (IndexedEqKind.eq (ekind x) Full); inversion H2; subst a''; clear H2. + simpl. rewrite ! ESF.add_iff, ! ESF.remove_iff. + apply H1 in H4; destruct H4. + subst x. rewrite e, e1. intuition auto. + apply H3 in H2; destruct H2 as (U & V & W & X). + destruct (OrderedEquation.eq_dec x {| ekind := High; ereg := ereg q; eloc := l2 |}). + subst x. intuition auto. + destruct (OrderedEquation.eq_dec x {| ekind := Low; ereg := ereg q; eloc := l2' |}). + subst x. intuition auto. + intuition auto. } + set (Q := fun e1 e2 => ~EqSet2.In q e1 -> EqSet.In q e2). + assert (B: Q elt e0'). + { eapply partial_fold_ind with (f := f) (s := elt) (final := e0'). eexact SUBST. + - unfold Q; intros. auto. + - unfold Q, f; intros. destruct (Loc.eq l1 (eloc x)); try congruence. + destruct (IndexedEqKind.eq (ekind x) Full); inversion H2; subst a''; clear H2. + simpl. rewrite ! ESF.add_iff, ! ESF.remove_iff. + red in H1. rewrite H1 in H4. intuition auto. } + destruct (ESP2.In_dec q elt). + left. apply A; auto. + right. split; auto. + rewrite <- select_loc_charact. + destruct (select_loc_l l1 q) eqn: LL; auto. + destruct (select_loc_h l1 q) eqn: LH; auto. + elim n. eapply EqSet2.elements_between_iff. + exact (select_loc_l_monotone l1). + exact (select_loc_h_monotone l1). + split. apply eqs_same; auto. auto. +Qed. + +Lemma long_type_compat_charact: + forall env l e q, + long_type_compat env l e = true -> + EqSet.In q e -> + subtype (env (ereg q)) Tlong = true \/ Loc.diff l (eloc q). +Proof. + unfold long_type_compat; intros. + rewrite EqSet2.for_all_between_iff in H. + destruct (select_loc_l l q) eqn: LL. + destruct (select_loc_h l q) eqn: LH. + left; apply H; auto. apply eqs_same; auto. + right. apply select_loc_charact. auto. + right. apply select_loc_charact. auto. + intros; subst; auto. + exact (select_loc_l_monotone l). + exact (select_loc_h_monotone l). +Qed. + +Lemma subst_loc_pair_satisf_makelong: + forall env src1 src2 dst rs ls e e', + subst_loc_pair (R dst) (R src1) (R src2) e = Some e' -> + long_type_compat env (R dst) e = true -> + wt_regset env rs -> + satisf rs ls e' -> + Archi.ptr64 = false -> + satisf rs (Locmap.set (R dst) (Val.longofwords (ls (R src1)) (ls (R src2))) ls) e. +Proof. + intros; red; intros. + exploit in_subst_loc_pair; eauto. intros [[A [B [C D]]] | [A B]]. +- rewrite A, B. apply H2 in C. apply H2 in D. + 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)). + apply Val.longofwords_lessdef. exact C. exact D. + eapply Val.has_subtype; eauto. + assumption. +- rewrite Locmap.gso; auto. +Qed. + Lemma can_undef_sound: forall e ml q, can_undef ml e = true -> EqSet.In q e -> Loc.notin (eloc q) (map R ml). @@ -1086,7 +1308,7 @@ Lemma add_equations_res_lessdef: Proof. intros. functional inversion H; simpl. - subst. eapply add_equation_lessdef with (q := Eq Full r (R mr)); eauto. -- subst. rewrite <- (val_longofwords_eq rs#r) by auto. +- subst. rewrite <- (val_longofwords_eq_1 rs#r) by auto. apply Val.longofwords_lessdef. eapply add_equation_lessdef with (q := Eq High r (R mr1)). eapply add_equation_satisf. eauto. @@ -1109,7 +1331,7 @@ Lemma return_regs_agree_callee_save: Proof. intros; red; intros. unfold return_regs. red in H. destruct l. - rewrite H; auto. + rewrite H; auto. destruct sl; auto || congruence. Qed. @@ -1163,7 +1385,7 @@ Proof. exploit no_caller_saves_sound; eauto. intros. red in H5. rewrite <- H5; auto. - (* Two 32-bit halves *) - subst. rewrite <- H9 in *. simpl in *. + subst. rewrite <- H9 in *. simpl in *. set (e' := remove_equation {| ekind := Low; ereg := res; eloc := R mr2 |} (remove_equation {| ekind := High; ereg := res; eloc := R mr1 |} e)) in *. InvBooleans. @@ -1260,7 +1482,7 @@ Qed. Lemma return_regs_arg_values: forall sg ls1 ls2, tailcall_is_possible sg = true -> - map (fun p => Locmap.getpair p (return_regs ls1 ls2)) (loc_arguments sg) + map (fun p => Locmap.getpair p (return_regs ls1 ls2)) (loc_arguments sg) = map (fun p => Locmap.getpair p ls2) (loc_arguments sg). Proof. intros. @@ -1268,7 +1490,7 @@ Proof. apply list_map_exten; intros. apply Locmap.getpair_exten; intros. assert (In l (regs_of_rpairs (loc_arguments sg))) by (eapply in_regs_of_rpairs; eauto). - exploit loc_arguments_acceptable_2; eauto. exploit H; eauto. + exploit loc_arguments_acceptable_2; eauto. exploit H; eauto. destruct l; simpl; intros; try contradiction. rewrite H4; auto. Qed. @@ -1291,7 +1513,7 @@ Lemma loadv_int64_split: /\ Val.lessdef (Val.hiword v) v1 /\ Val.lessdef (Val.loword v) v2. Proof. - intros. apply Archi.splitlong_ptr32 in H0. + intros. apply Archi.splitlong_ptr32 in H0. exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & A & B & C). exists v1, v2. split; auto. split; auto. inv C; auto. destruct v1, v2; simpl; auto. @@ -1324,9 +1546,8 @@ Proof. exploit add_equation_lessdef. eauto. simpl; intros LD1. exploit add_equation_lessdef. eapply add_equation_satisf. eauto. simpl; intros LD2. exists (Val.longofwords (ls x0) (ls x1)); split; auto with barg. - rewrite <- (val_longofwords_eq rs#x). apply Val.longofwords_lessdef; auto. + rewrite <- (val_longofwords_eq_2 rs#x); auto. apply Val.longofwords_lessdef; auto. rewrite <- e0; apply WT. - assumption. - econstructor; eauto with barg. - econstructor; eauto with barg. - econstructor; eauto with barg. @@ -1534,7 +1755,7 @@ Proof. monadInv Heqr. destruct (check_entrypoints_aux f tf env x) as [y|] eqn:?; try discriminate. unfold check_entrypoints_aux, pair_entrypoints in Heqo0. MonadInv. - exploit extract_moves_sound; eauto. intros [A B]. subst b. + 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. Qed. @@ -1639,7 +1860,8 @@ Opaque destroyed_by_op. - unfold expand_moves; simpl. inv H. exists ls; split. apply star_refl. auto. (* step *) - assert (wf_moves mv) by (inv H0; auto). - destruct a as (src, dst); unfold expand_moves; simpl; MonadInv. + destruct a; unfold expand_moves; simpl; MonadInv. ++ (* loc-loc move *) destruct src as [rsrc | ssrc]; destruct dst as [rdst | sdst]. * (* reg-reg *) exploit IHmv; eauto. eapply subst_loc_undef_satisf; eauto. @@ -1655,6 +1877,18 @@ Opaque destroyed_by_op. econstructor. auto. auto. * (* stack->stack *) inv H0. simpl in H6. contradiction. ++ (* makelong *) + exploit IHmv; eauto. eapply subst_loc_pair_satisf_makelong; eauto. + intros [ls' [A B]]. exists ls'; split; auto. eapply star_left; eauto. + econstructor. simpl; eauto. reflexivity. traceEq. ++ (* lowlong *) + exploit IHmv; eauto. eapply subst_loc_part_satisf_lowlong; eauto. + intros [ls' [A B]]. exists ls'; split; auto. eapply star_left; eauto. + econstructor. simpl; eauto. reflexivity. traceEq. ++ (* highlong *) + exploit IHmv; eauto. eapply subst_loc_part_satisf_highlong; eauto. + intros [ls' [A B]]. exists ls'; split; auto. eapply star_left; eauto. + econstructor. simpl; eauto. reflexivity. traceEq. Qed. (** The simulation relation *) @@ -1749,7 +1983,7 @@ Proof. assert (B: In (env r) (type_of_addressing addr)). { rewrite <- H5. apply in_map; auto. } assert (C: env r = Tint). - { apply A in B. rewrite B. unfold Tptr. rewrite Archi.splitlong_ptr32 by auto. auto. } + { apply A in B. rewrite B. unfold Tptr. rewrite Archi.splitlong_ptr32 by auto. auto. } red; intros; subst r. rewrite C in H8; discriminate. Qed. @@ -2195,7 +2429,7 @@ Proof. with (Locmap.getpair (map_rpair R (loc_result (RTL.fn_sig f))) ls1). eapply add_equations_res_lessdef; eauto. rewrite H13. apply WTRS. - generalize (loc_result_caller_save (RTL.fn_sig f)). + generalize (loc_result_caller_save (RTL.fn_sig f)). destruct (loc_result (RTL.fn_sig f)); simpl. intros A; rewrite A; auto. intros [A B]; rewrite A, B; auto. @@ -2228,15 +2462,15 @@ Proof. econstructor; split. apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved with (ge1 := ge); eauto. apply senv_preserved. - econstructor; eauto. + econstructor; eauto. simpl. destruct (loc_result (ef_sig ef)) eqn:RES; simpl. rewrite Locmap.gss; auto. - generalize (loc_result_pair (ef_sig ef)); rewrite RES; intros (A & B & C & D & E). + 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. - rewrite val_longofwords_eq by auto. auto. + rewrite Locmap.gss. rewrite Locmap.gso by (red; auto). rewrite Locmap.gss. + rewrite val_longofwords_eq_1 by auto. auto. red; intros. rewrite (AG l H0). - symmetry; apply Locmap.gpo. + symmetry; apply Locmap.gpo. assert (X: forall r, is_callee_save r = false -> Loc.diff l (R r)). { intros. destruct l; simpl in *. congruence. auto. } generalize (loc_result_caller_save (ef_sig ef)). destruct (loc_result (ef_sig ef)); simpl; intuition auto. @@ -2276,18 +2510,18 @@ Lemma final_states_simulation: forall st1 st2 r, match_states st1 st2 -> RTL.final_state st1 r -> LTL.final_state st2 r. Proof. - intros. inv H0. inv H. inv STACKS. + intros. inv H0. inv H. inv STACKS. econstructor. rewrite <- (loc_result_exten sg). inv RES; auto. - rewrite H; auto. + rewrite H; auto. Qed. - + Lemma wt_prog: wt_program prog. Proof. - red; intros. - exploit list_forall2_in_left. eexact (proj1 TRANSF). eauto. + 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. +- monadInv H2. unfold transf_function in EQ. destruct (type_function f) as [env|] eqn:TF; try discriminate. econstructor. eapply type_function_correct; eauto. diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index 2c7994e9..53ecf73a 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -338,7 +338,7 @@ Proof. - exploit extcall_arg_match; eauto. intros (v' & A & B). exists v'; split; auto. constructor; auto. - exploit extcall_arg_match. eauto. eauto. eexact H2. intros (v1 & A1 & B1). exploit extcall_arg_match. eauto. eauto. eexact H3. intros (v2 & A2 & B2). - exists (Val.longofwords v1 v2); split. constructor; auto. apply Val.longofwords_lessdef; auto. + exists (Val.longofwords v1 v2); split. constructor; auto. apply Val.longofwords_lessdef; auto. Qed. Lemma extcall_args_match: @@ -871,13 +871,13 @@ Inductive match_stack: list Mach.stackframe -> Prop := Lemma parent_sp_def: forall s, match_stack s -> parent_sp s <> Vundef. Proof. - induction 1; simpl. + induction 1; simpl. unfold Vnullptr; destruct Archi.ptr64; congruence. auto. Qed. Lemma parent_ra_def: forall s, match_stack s -> parent_ra s <> Vundef. -Proof. +Proof. induction 1; simpl. unfold Vnullptr; destruct Archi.ptr64; congruence. inv H0. congruence. diff --git a/backend/Bounds.v b/backend/Bounds.v index 8a383380..93a4b504 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -190,7 +190,7 @@ Remark fold_left_ensures: (forall a, P (f a b0)) -> forall l a, In b0 l -> P (fold_left f l a). Proof. - induction l; simpl; intros. contradiction. + induction l; simpl; intros. contradiction. destruct H1. subst a. apply fold_left_preserves; auto. apply IHl; auto. Qed. @@ -199,7 +199,7 @@ Definition only_callee_saves (u: RegSet.t) : Prop := Lemma record_reg_only: forall u r, only_callee_saves u -> only_callee_saves (record_reg u r). Proof. - unfold only_callee_saves, record_reg; intros. + unfold only_callee_saves, record_reg; intros. destruct (is_callee_save r) eqn:CS; auto. destruct (mreg_eq r r0). congruence. apply H; eapply RegSet.add_3; eauto. Qed. @@ -214,11 +214,11 @@ Proof. intros. destruct i; simpl; auto using record_reg_only, record_regs_only. Qed. -Lemma record_regs_of_function_only: +Lemma record_regs_of_function_only: only_callee_saves record_regs_of_function. Proof. intros. unfold record_regs_of_function. - apply fold_left_preserves. apply record_regs_of_instr_only. + apply fold_left_preserves. apply record_regs_of_instr_only. red; intros. eelim RegSet.empty_1; eauto. Qed. @@ -248,7 +248,7 @@ Next Obligation. apply record_regs_of_function_only. apply RegSet.elements_2. apply InA_alt. exists r; auto. Qed. - + (** We now show the correctness of the inferred bounds. *) Lemma record_reg_incr: forall u r r', RegSet.In r' u -> RegSet.In r' (record_reg u r). @@ -268,7 +268,7 @@ Qed. Lemma record_regs_ok: forall r rl u, In r rl -> is_callee_save r = true -> RegSet.In r (record_regs u rl). Proof. - intros. unfold record_regs. eapply fold_left_ensures; eauto using record_reg_incr, record_reg_ok. + intros. unfold record_regs. eapply fold_left_ensures; eauto using record_reg_incr, record_reg_ok. Qed. Lemma record_regs_of_instr_incr: forall r' u i, RegSet.In r' u -> RegSet.In r' (record_regs_of_instr u i). @@ -291,7 +291,7 @@ Proof. destruct H; auto using record_regs_incr, record_regs_ok. Qed. -Lemma record_regs_of_function_ok: +Lemma record_regs_of_function_ok: forall r i, In i f.(fn_code) -> defined_by_instr r i -> is_callee_save r = true -> RegSet.In r record_regs_of_function. Proof. intros. unfold record_regs_of_function. @@ -373,9 +373,9 @@ Lemma mreg_is_within_bounds: forall r, defined_by_instr r i -> mreg_within_bounds function_bounds r. Proof. - intros. unfold mreg_within_bounds. intros. + intros. unfold mreg_within_bounds. intros. exploit record_regs_of_function_ok; eauto. intros. - apply RegSet.elements_1 in H2. rewrite InA_alt in H2. destruct H2 as (r' & A & B). + apply RegSet.elements_1 in H2. rewrite InA_alt in H2. destruct H2 as (r' & A & B). subst r'; auto. Qed. @@ -447,9 +447,9 @@ Proof. Local Opaque mreg_type. induction l as [ | r l]; intros; simpl. - omega. -- eapply Zle_trans. 2: apply IHl. +- eapply Zle_trans. 2: apply IHl. generalize (AST.typesize_pos (mreg_type r)); intros. - apply Zle_trans with (align ofs (AST.typesize (mreg_type r))). + apply Zle_trans with (align ofs (AST.typesize (mreg_type r))). apply align_le; auto. omega. Qed. diff --git a/backend/CSEproof.v b/backend/CSEproof.v index bf152e82..8516e384 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -661,12 +661,12 @@ Proof with (try discriminate). } inv H2. + inv H3. exploit eval_addressing_Ainstack_inv; eauto. intros [E1 E2]. - simpl in E2; rewrite Ptrofs.add_zero_l in E2. subst a. + simpl in E2; rewrite Ptrofs.add_zero_l in E2. subst a. apply eq_holds_strict. econstructor. rewrite eval_addressing_Ainstack. simpl. rewrite Ptrofs.add_zero_l. eauto. apply LD; auto. + inv H4. exploit eval_addressing_Ainstack_inv; eauto. intros [E1 E2]. - simpl in E2; rewrite Ptrofs.add_zero_l in E2. subst a. + simpl in E2; rewrite Ptrofs.add_zero_l in E2. subst a. apply eq_holds_lessdef with v; auto. econstructor. rewrite eval_addressing_Ainstack. simpl. rewrite Ptrofs.add_zero_l. eauto. apply LD; auto. diff --git a/backend/Cminor.v b/backend/Cminor.v index e238140b..11941da3 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -61,7 +61,7 @@ Inductive unary_operation : Type := | Ointofsingle: unary_operation (**r signed integer to float32 *) | Ointuofsingle: unary_operation (**r unsigned integer to float32 *) | Osingleofint: unary_operation (**r float32 to signed integer *) - | Osingleofintu: unary_operation (**r float32 to unsigned integer *) + | Osingleofintu: unary_operation (**r float32 to unsigned integer *) | Onegl: unary_operation (**r long integer opposite *) | Onotl: unary_operation (**r long bitwise complement *) | Ointoflong: unary_operation (**r long to int *) diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index fd9cfaa5..b14c4be0 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -55,7 +55,7 @@ Lemma functions_translated: Genv.find_funct ge v = Some f -> exists cunit, Genv.find_funct tge v = Some (transf_fundef (romem_for cunit) f) /\ linkorder cunit prog. Proof. - intros. exploit (Genv.find_funct_match TRANSL); eauto. + intros. exploit (Genv.find_funct_match TRANSL); eauto. intros (cu & tf & A & B & C). subst tf. exists cu; auto. Qed. @@ -64,7 +64,7 @@ Lemma function_ptr_translated: Genv.find_funct_ptr ge b = Some f -> exists cunit, Genv.find_funct_ptr tge b = Some (transf_fundef (romem_for cunit) f) /\ linkorder cunit prog. Proof. - intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto. + intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto. intros (cu & tf & A & B & C). subst tf. exists cu; auto. Qed. @@ -92,7 +92,7 @@ Lemma transf_ros_correct: ematch bc rs ae -> find_function ge ros rs = Some f -> regs_lessdef rs rs' -> - exists cunit, + exists cunit, find_function tge (transf_ros ae ros) rs' = Some (transf_fundef (romem_for cunit) f) /\ linkorder cunit prog. Proof. @@ -100,7 +100,7 @@ Proof. - (* function pointer *) generalize (EM r); fold (areg ae r); intro VM. generalize (RLD r); intro LD. assert (DEFAULT: - exists cunit, + exists cunit, find_function tge (inl _ r) rs' = Some (transf_fundef (romem_for cunit) f) /\ linkorder cunit prog). { @@ -131,7 +131,7 @@ Lemma const_for_result_correct: Proof. intros. exploit ConstpropOpproof.const_for_result_correct; eauto. intros (v' & A & B). exists v'; split. - rewrite <- A; apply eval_operation_preserved. exact symbols_preserved. + rewrite <- A; apply eval_operation_preserved. exact symbols_preserved. auto. Qed. @@ -163,10 +163,10 @@ Proof. try apply match_pc_base. eapply match_pc_cond; eauto. intros b' DYNAMIC. assert (b = b'). - { eapply resolve_branch_sound; eauto. - rewrite <- DYNAMIC. apply eval_static_condition_sound with bc. + { eapply resolve_branch_sound; eauto. + rewrite <- DYNAMIC. apply eval_static_condition_sound with bc. apply aregs_sound; auto. } - subst b'. apply IHn. + subst b'. apply IHn. Qed. Lemma match_successor: @@ -326,7 +326,7 @@ Lemma match_states_succ: match_states O (State s f sp pc rs m) (State s' (transf_function (romem_for cu) f) sp pc rs' m'). Proof. - intros. apply match_states_intro; auto. constructor. + intros. apply match_states_intro; auto. constructor. Qed. Lemma transf_instr_at: @@ -506,7 +506,7 @@ Opaque builtin_strength_reduction. - (* Icond, skipped over *) rewrite H1 in H; inv H. - right; exists n; split. omega. split. auto. + right; exists n; split. omega. split. auto. econstructor; eauto. - (* Ijumptable *) diff --git a/backend/Conventions.v b/backend/Conventions.v index 64a83a58..bdc4c8b6 100644 --- a/backend/Conventions.v +++ b/backend/Conventions.v @@ -33,7 +33,7 @@ Proof. exploit H; eauto. destruct p; simpl in *; intuition congruence. apply IHpl; auto. Qed. - + (** ** Location of function parameters *) (** A function finds the values of its parameter in the same locations @@ -65,7 +65,7 @@ Proof. inv A. auto. unfold loc_parameters. generalize (loc_arguments sg). induction l as [ | p l]; simpl; intros. auto. - rewrite map_app. f_equal; auto. destruct p; auto. + rewrite map_app. f_equal; auto. destruct p; auto. Qed. (** * Tail calls *) @@ -90,8 +90,8 @@ Definition tailcall_is_possible (sg: signature) : bool := Lemma tailcall_is_possible_correct: forall s, tailcall_is_possible s = true -> tailcall_possible s. Proof. - unfold tailcall_is_possible; intros. rewrite forallb_forall in H. - red; intros. apply H in H0. destruct l; [auto|discriminate]. + unfold tailcall_is_possible; intros. rewrite forallb_forall in H. + red; intros. apply H in H0. destruct l; [auto|discriminate]. Qed. Lemma zero_size_arguments_tailcall_possible: diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index fa402e9f..3f0c5a4c 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -1101,7 +1101,7 @@ Proof. exists (Callstate nil tf nil m0); split. econstructor; eauto. eapply (Genv.init_mem_match TRANSF); eauto. - replace (prog_main tprog) with (prog_main prog). + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto. symmetry; eapply match_program_main; eauto. rewrite <- H3. eapply sig_function_translated; eauto. diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index d5d7e033..bc991f0f 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -400,7 +400,7 @@ Proof. simpl in H0. unfold ge, fundef in H0. rewrite A in H0. rewrite <- Genv.find_funct_ptr_iff in B. congruence. -Qed. +Qed. (** Translation of builtin arguments. *) diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v index 331f8b06..dfd96333 100644 --- a/backend/Inliningspec.v +++ b/backend/Inliningspec.v @@ -52,9 +52,9 @@ Proof. P dm fenv -> P (fold_left (fun x idg => PTree.set (fst idg) (snd idg) x) l dm) (fold_left add_globdef l fenv)). - { induction l; simpl; intros. + { induction l; simpl; intros. - auto. - - apply IHl. apply ADD; auto. + - apply IHl. apply ADD; auto. } intros. apply REC. red; intros. rewrite PTree.gempty in H; discriminate. Qed. @@ -63,8 +63,8 @@ Lemma fenv_compat_linkorder: forall cunit prog fenv, linkorder cunit prog -> fenv_compat cunit fenv -> fenv_compat prog fenv. Proof. - intros; red; intros. apply H0 in H1. - destruct (prog_defmap_linkorder _ _ _ _ H H1) as (gd' & P & Q). + intros; red; intros. apply H0 in H1. + destruct (prog_defmap_linkorder _ _ _ _ H H1) as (gd' & P & Q). inv Q. inv H3. auto. Qed. @@ -702,7 +702,7 @@ Lemma tr_function_linkorder: tr_function cunit f f' -> tr_function prog f f'. Proof. - intros. inv H0. econstructor; eauto. eapply fenv_compat_linkorder; eauto. + intros. inv H0. econstructor; eauto. eapply fenv_compat_linkorder; eauto. Qed. Lemma transf_function_spec: diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index e13ffb40..30cc0d91 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -164,7 +164,7 @@ 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 & C & D & E) F. +- 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. diff --git a/backend/Locations.v b/backend/Locations.v index 52abfc46..ca148761 100644 --- a/backend/Locations.v +++ b/backend/Locations.v @@ -403,7 +403,7 @@ Module Locmap. (forall l, In l (regs_of_rpair p) -> ls2 l = ls1 l) -> getpair p ls2 = getpair p ls1. Proof. - intros. destruct p; simpl. + intros. destruct p; simpl. apply H; simpl; auto. f_equal; apply H; simpl; auto. Qed. @@ -412,7 +412,7 @@ Module Locmap. forall p v m l, forall_rpair (fun r => Loc.diff l (R r)) p -> setpair p v m l = m l. Proof. - intros; destruct p; simpl in *. + intros; destruct p; simpl in *. - apply gso. apply Loc.diff_sym; auto. - destruct H. rewrite ! gso by (apply Loc.diff_sym; auto). auto. Qed. diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 09630e29..c8f8ea82 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -72,6 +72,7 @@ let elf_label oc lbl = let float64_literals : (int * int64) list ref = ref [] let float32_literals : (int * int32) list ref = ref [] +let int64_literals : (int * int64) list ref = ref [] let jumptables : (int * label list) list ref = ref [] let reset_constants () = diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index f9f01d49..9992ab79 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -693,7 +693,7 @@ Proof. rewrite A; simpl; rewrite C; simpl. rewrite H2; rewrite dec_eq_true. replace (tailcall_is_possible sig) with true; auto. - symmetry. unfold tailcall_is_possible. apply forallb_forall. + symmetry. unfold tailcall_is_possible. apply forallb_forall. intros. apply H3 in H4. destruct x; intuition auto. - (* builtin *) exploit type_builtin_args_complete; eauto. instantiate (1 := args). intros [e1 [A B]]. diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml index cfaf422d..c14852f4 100644 --- a/backend/Regalloc.ml +++ b/backend/Regalloc.ml @@ -605,6 +605,17 @@ let add_interfs_destroyed g live mregs = (fun mr -> VSet.iter (IRC.add_interf g (L (R mr))) live) mregs +let add_interfs_caller_save g live = + VSet.iter + (fun v -> + let tv = typeof v in + List.iter + (fun mr -> + if not (is_callee_save mr && subtype tv (callee_save_type mr)) + then IRC.add_interf g (L (R mr)) v) + all_mregs) + live + let add_interfs_live g live v = VSet.iter (fun v' -> IRC.add_interf g v v') live @@ -622,7 +633,14 @@ let add_interfs_instr g instr live = match instr with | Xmove(src, dst) | Xspill(src, dst) | Xreload(src, dst) -> IRC.add_pref g src dst; - add_interfs_move g src dst live + add_interfs_move g src dst live; + (* Reloads from incoming slots can occur when some 64-bit + parameters are split and passed as two 32-bit stack locations. *) + begin match src with + | L(Locations.S(Incoming, _, _)) -> + add_interfs_def g (vmreg temp_for_parent_frame) live + | _ -> () + end | Xparmove(srcs, dsts, itmp, ftmp) -> List.iter2 (IRC.add_pref g) srcs dsts; (* Interferences with live across *) @@ -636,20 +654,10 @@ let add_interfs_instr g instr live = add_interfs_list g ftmp srcs; add_interfs_list g ftmp dsts; (* Take into account destroyed reg when accessing Incoming param *) if List.exists (function (L(Locations.S(Incoming, _, _))) -> true | _ -> false) srcs - then add_interfs_list g (vmreg temp_for_parent_frame) dsts; - (* Take into account destroyed reg when initializing Outgoing - arguments of type Tsingle *) - if List.exists - (function (L(Locations.S(Outgoing, _, Tsingle))) -> true | _ -> false) dsts - then - List.iter - (fun mr -> - add_interfs_list g (vmreg mr) srcs; - IRC.add_interf g (vmreg mr) ftmp) - (destroyed_by_setstack Tsingle) - | Xop(Ofloatofsingle, arg1::_, res) when Configuration.arch = "powerpc" -> - add_interfs_def g res live; - IRC.add_pref g arg1 res + then begin + add_interfs_list g (vmreg temp_for_parent_frame) dsts; + add_interfs_live g across (vmreg temp_for_parent_frame) + end | Xop(op, args, res) -> begin match is_two_address op args with | None -> @@ -672,7 +680,7 @@ let add_interfs_instr g instr live = begin match vos with | Coq_inl v -> List.iter (fun r -> IRC.add_interf g (vmreg r) v) destroyed_at_indirect_call | _ -> () end; - add_interfs_destroyed g (vset_removelist res live) destroyed_at_call + add_interfs_caller_save g (vset_removelist res live) | Xtailcall(sg, Coq_inl v, args) -> List.iter (fun r -> IRC.add_interf g (vmreg r) v) (int_callee_save_regs @ destroyed_at_indirect_call) | Xtailcall(sg, Coq_inr id, args) -> diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp index 96b07e28..d91797c5 100644 --- a/backend/SelectDiv.vp +++ b/backend/SelectDiv.vp @@ -123,7 +123,7 @@ Definition divuimm (e1: expr) (n2: int) := end end. -Definition divu (e1: expr) (e2: expr) := +Definition divu (e1: expr) (e2: expr) := match is_intconst e2, is_intconst e1 with | Some n2, Some n1 => if Int.eq n2 Int.zero @@ -149,7 +149,7 @@ Definition moduimm (e1: expr) (n2: int) := end end. -Definition modu (e1: expr) (e2: expr) := +Definition modu (e1: expr) (e2: expr) := match is_intconst e2, is_intconst e1 with | Some n2, Some n1 => if Int.eq n2 Int.zero @@ -169,7 +169,7 @@ Definition divs_mul (p: Z) (m: Z) := Definition divsimm (e1: expr) (n2: int) := match Int.is_power2 n2 with - | Some l => + | Some l => if Int.ltu l (Int.repr 31) then shrximm e1 l else divs_base e1 (Eop (Ointconst n2) Enil) @@ -183,7 +183,7 @@ Definition divsimm (e1: expr) (n2: int) := end end. -Definition divs (e1: expr) (e2: expr) := +Definition divs (e1: expr) (e2: expr) := match is_intconst e2, is_intconst e1 with | Some n2, Some n1 => if Int.eq n2 Int.zero @@ -209,7 +209,7 @@ Definition modsimm (e1: expr) (n2: int) := end end. -Definition mods (e1: expr) (e2: expr) := +Definition mods (e1: expr) (e2: expr) := match is_intconst e2, is_intconst e1 with | Some n2, Some n1 => if Int.eq n2 Int.zero @@ -266,7 +266,7 @@ Definition modlu (e1 e2: expr) := end. Definition divls_mull (p: Z) (m: Z) := - let e2 := + let e2 := mullhs (Eletvar O) (Int64.repr m) in let e3 := if zlt m Int64.half_modulus then e2 else addl e2 (Eletvar O) in diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v index 5704b32b..fe5bfe28 100644 --- a/backend/SelectDivproof.v +++ b/backend/SelectDivproof.v @@ -184,7 +184,7 @@ Proof with (try discriminate). destruct (find_div_mul_params Int.wordsize (Int.half_modulus - Int.half_modulus mod d - 1) d 32) as [[p m] | ]... - generalize (p - 32). intro p1. + generalize (p - 32). intro p1. destruct (zlt 0 d)... destruct (zlt (two_p (32 + p1)) (m * d))... destruct (zle (m * d) (two_p (32 + p1) + two_p (p1 + 1)))... @@ -192,7 +192,7 @@ Proof with (try discriminate). destruct (zlt m Int.modulus)... destruct (zle 0 p1)... destruct (zlt p1 32)... - intros EQ; inv EQ. + intros EQ; inv EQ. split. auto. split. auto. intros. replace (32 + p') with (31 + (p' + 1)) by omega. apply Zquot_mul; try omega. @@ -331,7 +331,7 @@ Proof with (try discriminate). destruct (find_div_mul_params Int64.wordsize (Int64.half_modulus - Int64.half_modulus mod d - 1) d 64) as [[p m] | ]... - generalize (p - 64). intro p1. + generalize (p - 64). intro p1. destruct (zlt 0 d)... destruct (zlt (two_p (64 + p1)) (m * d))... destruct (zle (m * d) (two_p (64 + p1) + two_p (p1 + 1)))... @@ -339,7 +339,7 @@ Proof with (try discriminate). destruct (zlt m Int64.modulus)... destruct (zle 0 p1)... destruct (zlt p1 64)... - intros EQ; inv EQ. + intros EQ; inv EQ. split. auto. split. auto. intros. replace (64 + p') with (63 + (p' + 1)) by omega. apply Zquot_mul; try omega. @@ -746,7 +746,7 @@ Proof. unfold modl_from_divl; intros. exploit eval_mullimm; eauto. instantiate (1 := n). intros (v1 & A1 & B1). assert (A0: eval_expr ge sp e m le (Eletvar O) (Vlong x)) by (constructor; auto). - exploit eval_subl; auto. eexact A0. eexact A1. + exploit eval_subl ; auto ; try apply HELPERS. exact A0. exact A1. intros (v2 & A2 & B2). simpl in B1; inv B1. simpl in B2; inv B2. exact A2. Qed. @@ -784,11 +784,11 @@ Proof. + destruct (Int64.is_power2' n2) as [l|] eqn:POW. * exploit Val.divlu_pow2; eauto. intros EQ; subst z. apply eval_shrluimm; auto. * destruct (Compopts.optim_for_size tt). eapply eval_divlu_base; eauto. - destruct (divlu_mul_params (Int64.unsigned n2)) as [[p M]|] eqn:PARAMS. + destruct (divlu_mul_params (Int64.unsigned n2)) as [[p M]|] eqn:PARAMS. ** destruct x; simpl in H1; try discriminate. destruct (Int64.eq n2 Int64.zero); inv H1. - econstructor; split; eauto. econstructor. eauto. eapply eval_divlu_mull; eauto. -** eapply eval_divlu_base; eauto. + econstructor; split; eauto. econstructor. eauto. eapply eval_divlu_mull; eauto. +** eapply eval_divlu_base; eauto. - eapply eval_divlu_base; eauto. Qed. @@ -809,15 +809,15 @@ Proof. + destruct (Int64.is_power2 n2) as [l|] eqn:POW. * exploit Val.modlu_pow2; eauto. intros EQ; subst z. eapply eval_andl; eauto. apply eval_longconst. * destruct (Compopts.optim_for_size tt). eapply eval_modlu_base; eauto. - destruct (divlu_mul_params (Int64.unsigned n2)) as [[p M]|] eqn:PARAMS. + destruct (divlu_mul_params (Int64.unsigned n2)) as [[p M]|] eqn:PARAMS. ** destruct x; simpl in H1; try discriminate. destruct (Int64.eq n2 Int64.zero) eqn:Z; inv H1. - rewrite Int64.modu_divu. + rewrite Int64.modu_divu. econstructor; split; eauto. econstructor. eauto. - eapply eval_modl_from_divl; eauto. + eapply eval_modl_from_divl; eauto. eapply eval_divlu_mull; eauto. - red; intros; subst n2; discriminate Z. -** eapply eval_modlu_base; eauto. + red; intros; subst n2; discriminate Z. +** eapply eval_modlu_base; eauto. - eapply eval_modlu_base; eauto. Qed. @@ -831,16 +831,16 @@ Proof. assert (A0: eval_expr ge sp e m le (Eletvar O) (Vlong x)). { constructor; auto. } exploit eval_mullhs. eauto. eexact A0. instantiate (1 := Int64.repr M). intros (v1 & A1 & B1). - exploit eval_addl; auto. eexact A1. eexact A0. intros (v2 & A2 & B2). + exploit eval_addl; auto; try apply HELPERS. eexact A1. eexact A0. intros (v2 & A2 & B2). exploit eval_shrluimm. eauto. eexact A0. instantiate (1 := Int.repr 63). intros (v3 & A3 & B3). set (a4 := if zlt M Int64.half_modulus then mullhs (Eletvar 0) (Int64.repr M) else addl (mullhs (Eletvar 0) (Int64.repr M)) (Eletvar 0)). set (v4 := if zlt M Int64.half_modulus then v1 else v2). - assert (A4: eval_expr ge sp e m le a4 v4). + assert (A4: eval_expr ge sp e m le a4 v4). { unfold a4, v4; destruct (zlt M Int64.half_modulus); auto. } exploit eval_shrlimm. eauto. eexact A4. instantiate (1 := Int.repr p). intros (v5 & A5 & B5). - exploit eval_addl; auto. eexact A5. eexact A3. intros (v6 & A6 & B6). + exploit eval_addl; auto; try apply HELPERS. eexact A5. eexact A3. intros (v6 & A6 & B6). assert (RANGE: forall x, 0 <= x < 64 -> Int.ltu (Int.repr x) Int64.iwordsize' = true). { intros. unfold Int.ltu. rewrite Int.unsigned_repr. rewrite zlt_true by tauto. auto. assert (64 < Int.max_unsigned) by (compute; auto). omega. } @@ -850,11 +850,11 @@ Proof. destruct (zlt M Int64.half_modulus). - exploit (divls_mul_shift_1 x); eauto. intros [A B]. simpl in B5; rewrite RANGE in B5 by auto; inv B5. - simpl in B6; inv B6. + simpl in B6; inv B6. rewrite B; exact A6. - exploit (divls_mul_shift_2 x); eauto. intros [A B]. simpl in B5; rewrite RANGE in B5 by auto; inv B5. - simpl in B6; inv B6. + simpl in B6; inv B6. rewrite B; exact A6. Qed. @@ -870,7 +870,7 @@ Proof. - assert (y = Vlong n2) by (eapply is_longconst_sound; eauto). subst y. destruct (is_longconst a) as [n1|] eqn:N1. + assert (x = Vlong n1) by (eapply is_longconst_sound; eauto). subst x. - simpl in H1. + simpl in H1. destruct (Int64.eq n2 Int64.zero || Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone); inv H1. econstructor; split. apply eval_longconst. constructor. @@ -879,7 +879,7 @@ Proof. ** exploit Val.divls_pow2; eauto. intros EQ. eapply eval_shrxlimm; eauto. ** eapply eval_divls_base; eauto. * destruct (Compopts.optim_for_size tt). eapply eval_divls_base; eauto. - destruct (divls_mul_params (Int64.signed n2)) as [[p M]|] eqn:PARAMS. + destruct (divls_mul_params (Int64.signed n2)) as [[p M]|] eqn:PARAMS. ** destruct x; simpl in H1; try discriminate. destruct (Int64.eq n2 Int64.zero || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone); inv H1. @@ -901,7 +901,7 @@ Proof. - assert (y = Vlong n2) by (eapply is_longconst_sound; eauto). subst y. destruct (is_longconst a) as [n1|] eqn:N1. + assert (x = Vlong n1) by (eapply is_longconst_sound; eauto). subst x. - simpl in H1. + simpl in H1. destruct (Int64.eq n2 Int64.zero || Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone); inv H1. econstructor; split. apply eval_longconst. constructor. @@ -917,19 +917,19 @@ Proof. assert (A: eval_expr ge sp e m le' (Eletvar O) (Vlong i)) by (constructor; auto). exploit eval_shrxlimm; eauto. intros (v1 & A1 & B1). inv B1. econstructor; split. - econstructor. eauto. eapply eval_modl_from_divl. eexact A1. reflexivity. + econstructor. eauto. eapply eval_modl_from_divl. eexact A1. reflexivity. rewrite Int64.mods_divs. auto. **eapply eval_modls_base; eauto. * destruct (Compopts.optim_for_size tt). eapply eval_modls_base; eauto. - destruct (divls_mul_params (Int64.signed n2)) as [[p M]|] eqn:PARAMS. + destruct (divls_mul_params (Int64.signed n2)) as [[p M]|] eqn:PARAMS. ** destruct x; simpl in H1; try discriminate. destruct (Int64.eq n2 Int64.zero || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone); inv H1. econstructor; split; eauto. econstructor. eauto. - rewrite Int64.mods_divs. + rewrite Int64.mods_divs. eapply eval_modl_from_divl; auto. eapply eval_divls_mull; eauto. -** eapply eval_modls_base; eauto. +** eapply eval_modls_base; eauto. - eapply eval_modls_base; eauto. Qed. diff --git a/backend/Selection.v b/backend/Selection.v index abda1d95..f278ed0b 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -339,7 +339,7 @@ Definition sel_fundef (dm: PTree.t globdef) (hf: helper_functions) (f: Cminor.fu (** We build a partial mapping from global identifiers to their definitions, restricting ourselves to the globals we are interested in, namely the external function declarations that are marked as runtime library - helpers. + helpers. This ensures that the mapping remains small and that [lookup_helper] below is efficient. *) @@ -350,7 +350,7 @@ Definition globdef_of_interest (gd: globdef) : bool := end. Definition record_globdefs (defmap: PTree.t globdef) : PTree.t globdef := - PTree.fold + PTree.fold (fun m id gd => if globdef_of_interest gd then PTree.set id gd m else m) defmap (PTree.empty globdef). diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 90e50338..ebc64c6f 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -34,14 +34,14 @@ Definition match_prog (p: Cminor.program) (tp: CminorSel.program) := Lemma record_globdefs_sound: forall dm id gd, (record_globdefs dm)!id = Some gd -> dm!id = Some gd. Proof. - intros. + intros. set (f := fun m id gd => if globdef_of_interest gd then PTree.set id gd m else m) in *. set (P := fun m m' => m'!id = Some gd -> m!id = Some gd). assert (X: P dm (PTree.fold f dm (PTree.empty _))). { apply PTree_Properties.fold_rec. - unfold P; intros. rewrite <- H0; auto. - red. rewrite ! PTree.gempty. auto. - - unfold P; intros. rewrite PTree.gsspec. unfold f in H3. + - unfold P; intros. rewrite PTree.gsspec. unfold f in H3. destruct (globdef_of_interest v). + rewrite PTree.gsspec in H3. destruct (peq id k); auto. + apply H2 in H3. destruct (peq id k). congruence. auto. } @@ -91,7 +91,7 @@ Qed. Theorem transf_program_match: forall p tp, sel_program p = OK tp -> match_prog p tp. Proof. - intros. monadInv H. + intros. monadInv H. eapply match_transform_partial_program_contextual. eexact EQ0. intros. exists x; split; auto. apply get_helpers_correct; auto. Qed. @@ -100,10 +100,10 @@ Lemma helper_functions_declared_linkorder: forall (p p': Cminor.program) hf, helper_functions_declared p hf -> linkorder p p' -> helper_functions_declared p' hf. Proof. - intros. + intros. assert (X: forall id name sg, helper_declared p id name sg -> helper_declared p' id name sg). { unfold helper_declared; intros. - destruct (prog_defmap_linkorder _ _ _ _ H0 H1) as (gd & P & Q). + destruct (prog_defmap_linkorder _ _ _ _ H0 H1) as (gd & P & Q). inv Q. inv H3. auto. } red in H. decompose [Logic.and] H; clear H. red; auto 20. Qed. @@ -139,7 +139,7 @@ Lemma functions_translated: exists cu tf, Genv.find_funct tge v' = Some tf /\ match_fundef cu f tf /\ linkorder cu prog. Proof. intros. inv H0. - eapply Genv.find_funct_match; eauto. + eapply Genv.find_funct_match; eauto. discriminate. Qed. @@ -159,11 +159,11 @@ Lemma helper_functions_preserved: forall hf, helper_functions_declared prog hf -> helper_functions_declared tprog hf. Proof. assert (X: forall id name sg, helper_declared prog id name sg -> helper_declared tprog id name sg). - { unfold helper_declared; intros. + { unfold helper_declared; intros. generalize (match_program_defmap _ _ _ _ _ TRANSF id). unfold Cminor.fundef; rewrite H; intros R; inv R. inv H2. destruct H4 as (cu & A & B). monadInv B. auto. } - unfold helper_functions_declared; intros. decompose [Logic.and] H; clear H. auto 20. + unfold helper_functions_declared; intros. decompose [Logic.and] H; clear H. auto 20. Qed. Section CMCONSTR. @@ -354,13 +354,13 @@ Proof. exploit expr_is_addrof_ident_correct; eauto. intros EQ; subst a. inv H0. inv H3. unfold Genv.symbol_address in *. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; try discriminate. - rewrite Genv.find_funct_find_funct_ptr in H1. + rewrite Genv.find_funct_find_funct_ptr in H1. assert (DFL: exists b1, Genv.find_symbol ge id = Some b1 /\ Vptr b Ptrofs.zero = Vptr b1 Ptrofs.zero) by (exists b; auto). unfold globdef; destruct (prog_defmap unit)!id as [[[f|ef] |gv] |] eqn:G; auto. destruct (ef_inline ef) eqn:INLINE; auto. destruct (prog_defmap_linkorder _ _ _ _ H G) as (gd & P & Q). - inv Q. inv H2. -- apply Genv.find_def_symbol in P. destruct P as (b' & X & Y). fold ge in X, Y. + inv Q. inv H2. +- apply Genv.find_def_symbol in P. destruct P as (b' & X & Y). fold ge in X, Y. rewrite <- Genv.find_funct_ptr_iff in Y. congruence. - simpl in INLINE. discriminate. Qed. @@ -459,6 +459,17 @@ Qed. End SEL_SWITCH. +Section SEL_SWITH_INT. + +Variable cunit: Cminor.program. +Variable hf: helper_functions. +Hypothesis LINK: linkorder cunit prog. +Hypothesis HF: helper_functions_declared cunit hf. + +Let HF': helper_functions_declared tprog hf. +Proof. + apply helper_functions_preserved. eapply helper_functions_declared_linkorder; eauto. +Qed. Lemma sel_switch_int_correct: forall dfl cases arg sp e m i t le, validate_switch Int.modulus dfl cases t = true -> @@ -517,7 +528,7 @@ Proof. rewrite Int64.unsigned_repr. destruct (zlt (Int64.unsigned n0) n); auto. unfold Int64.max_unsigned; omega. - intros until n; intros EVAL R RANGE. - exploit eval_subl; auto. eexact EVAL. apply eval_longconst with (n := Int64.repr n). + exploit eval_subl; auto; try apply HF'. eexact EVAL. apply eval_longconst with (n := Int64.repr n). intros (vb & A & B). inv R. simpl in B. inv B. econstructor; split; eauto. replace ((Int64.unsigned n0 - n) mod Int64.modulus) @@ -535,6 +546,8 @@ Proof. - apply Int64.unsigned_range. Qed. +End SEL_SWITH_INT. + (** Compatibility of evaluation functions with the "less defined than" relation. *) Ltac TrivialExists := @@ -561,7 +574,7 @@ Lemma eval_binop_lessdef: Proof. intros until m'; intros EV LD1 LD2 ME. assert (exists v', eval_binop op v1' v2' m = Some v' /\ Val.lessdef v v'). - { inv LD1. inv LD2. exists v; auto. + { inv LD1. inv LD2. exists v; auto. destruct op; destruct v1'; simpl in *; inv EV; TrivialExists. destruct op; simpl in *; inv EV; TrivialExists. } assert (CMPU: forall c, @@ -648,7 +661,7 @@ Proof. exists (Vint i); split; auto. econstructor. constructor. auto. exists (Vfloat f); split; auto. econstructor. constructor. auto. exists (Vsingle f); split; auto. econstructor. constructor. auto. - exists (Vlong i); split; auto. apply eval_longconst. + exists (Vlong i); split; auto. apply eval_longconst. unfold Genv.symbol_address; rewrite <- symbols_preserved; fold (Genv.symbol_address tge i i0). apply eval_addrsymbol. apply eval_addrstack. (* Eunop *) @@ -808,7 +821,7 @@ Remark call_cont_commut: Proof. induction 1; simpl; auto; red; intros. - constructor. -- eapply match_cont_call with (hf := hf); eauto. +- eapply match_cont_call with (hf := hf); eauto. Qed. Remark match_is_call_cont: @@ -816,7 +829,7 @@ Remark match_is_call_cont: Proof. destruct 1; intros; try contradiction; red; intros. - constructor. -- eapply match_cont_call with (hf := hf); eauto. +- eapply match_cont_call with (hf := hf); eauto. Qed. Remark match_call_cont_cont: @@ -920,7 +933,7 @@ Proof. econstructor; eauto. econstructor; eauto. eapply sig_function_translated; eauto. eapply match_callstate with (cunit := cunit'); eauto. - red; intros. eapply match_cont_call with (cunit := cunit) (hf := hf); eauto. + red; intros. eapply match_cont_call with (cunit := cunit) (hf := hf); eauto. + (* direct *) intros [b [U V]]. exploit sel_exprlist_correct; eauto. intros [vargs' [C D]]. @@ -930,7 +943,7 @@ Proof. subst vf. econstructor; eauto. rewrite symbols_preserved; eauto. eapply sig_function_translated; eauto. eapply match_callstate with (cunit := cunit'); eauto. - red; intros; eapply match_cont_call with (cunit := cunit) (hf := hf); eauto. + red; intros; eapply match_cont_call with (cunit := cunit) (hf := hf); eauto. + (* turned into Sbuiltin *) intros EQ. subst fd. exploit sel_builtin_args_correct; eauto. intros [vargs' [C D]]. @@ -943,7 +956,7 @@ Proof. exploit sel_exprlist_correct; eauto. intros [vargs' [C D]]. exploit functions_translated; eauto. intros (cunit' & fd' & E & F & G). left; econstructor; split. - exploit classify_call_correct. eexact LINK. eauto. eauto. + exploit classify_call_correct. eexact LINK. eauto. eauto. destruct (classify_call (prog_defmap cunit)) as [ | id | ef]; intros. econstructor; eauto. econstructor; eauto. eapply sig_function_translated; eauto. destruct H2 as [b [U V]]. subst vf. inv B. @@ -1021,7 +1034,7 @@ Proof. econstructor; eauto. econstructor; eauto. - (* internal function *) - destruct TF as (hf & HF & TF). specialize (MC cunit hf). + destruct TF as (hf & HF & TF). specialize (MC cunit hf). monadInv TF. generalize EQ; intros TF; monadInv TF. exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. intros [m2' [A B]]. @@ -1029,7 +1042,7 @@ Proof. econstructor; simpl; eauto. econstructor; simpl; eauto. apply set_locals_lessdef. apply set_params_lessdef; auto. - (* external call *) - destruct TF as (hf & HF & TF). + destruct TF as (hf & HF & TF). monadInv TF. exploit external_call_mem_extends; eauto. intros [vres' [m2 [A [B [C D]]]]]. @@ -1043,7 +1056,7 @@ Proof. econstructor. eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved. econstructor; eauto. - (* return *) - apply match_call_cont_cont in MC. destruct MC as (cunit0 & hf0 & MC). + apply match_call_cont_cont in MC. destruct MC as (cunit0 & hf0 & MC). inv MC. left; econstructor; split. econstructor. @@ -1073,7 +1086,7 @@ Lemma sel_final_states: match_states S R -> Cminor.final_state S r -> final_state R r. Proof. intros. inv H0. inv H. - apply match_call_cont_cont in MC. destruct MC as (cunit0 & hf0 & MC). + apply match_call_cont_cont in MC. destruct MC as (cunit0 & hf0 & MC). inv MC. inv LD. constructor. Qed. @@ -1081,7 +1094,7 @@ Theorem transf_program_correct: forward_simulation (Cminor.semantics prog) (CminorSel.semantics tprog). Proof. apply forward_simulation_opt with (match_states := match_states) (measure := measure). - apply senv_preserved. + apply senv_preserved. apply sel_initial_states; auto. apply sel_final_states; auto. apply sel_step_correct; auto. @@ -1101,5 +1114,5 @@ Local Transparent Linker_fundef. - discriminate. - destruct e; inv H2. econstructor; eauto. - destruct e; inv H2. econstructor; eauto. -- destruct (external_function_eq e e0); inv H2. econstructor; eauto. +- destruct (external_function_eq e e0); inv H2. econstructor; eauto. Qed. diff --git a/backend/SplitLong.vp b/backend/SplitLong.vp index cbf7fa30..de954482 100644 --- a/backend/SplitLong.vp +++ b/backend/SplitLong.vp @@ -130,7 +130,7 @@ Definition negl (e: expr) := Definition notl (e: expr) := splitlong e (fun h l => makelong (notint h) (notint l)). -Definition longoffloat (arg: expr) := +Definition longoffloat (arg: expr) := Eexternal i64_dtos sig_f_l (arg ::: Enil). Definition longuoffloat (arg: expr) := Eexternal i64_dtou sig_f_l (arg ::: Enil). @@ -138,7 +138,7 @@ Definition floatoflong (arg: expr) := Eexternal i64_stod sig_l_f (arg ::: Enil). Definition floatoflongu (arg: expr) := Eexternal i64_utod sig_l_f (arg ::: Enil). -Definition longofsingle (arg: expr) := +Definition longofsingle (arg: expr) := longoffloat (floatofsingle arg). Definition longuofsingle (arg: expr) := longuoffloat (floatofsingle arg). diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v index 3b1eaa6b..fd1fdebd 100644 --- a/backend/SplitLongproof.v +++ b/backend/SplitLongproof.v @@ -96,7 +96,7 @@ Lemma eval_helper: Proof. intros. red in H0. apply Genv.find_def_symbol in H0. destruct H0 as (b & P & Q). - rewrite <- Genv.find_funct_ptr_iff in Q. + rewrite <- Genv.find_funct_ptr_iff in Q. econstructor; eauto. Qed. @@ -363,7 +363,7 @@ Qed. Theorem eval_longofint: unary_constructor_sound longofint Val.longofint. Proof. red; intros. unfold longofint. destruct (longofint_match a). -- InvEval. econstructor; split. apply eval_longconst. auto. +- InvEval. econstructor; split. apply eval_longconst. auto. - exploit (eval_shrimm ge sp e m (Int.repr 31) (x :: le) (Eletvar 0)). EvalOp. intros [v1 [A B]]. econstructor; split. EvalOp. @@ -725,7 +725,7 @@ Qed. Theorem eval_addl: Archi.ptr64 = false -> binary_constructor_sound addl Val.addl. Proof. - unfold addl; red; intros. + unfold addl; red; intros. set (default := Ebuiltin (EF_builtin "__builtin_addl" sig_ll_l) (a ::: b ::: Enil)). assert (DEFAULT: exists v, eval_expr ge sp e m le default v /\ Val.lessdef (Val.addl x y) v). @@ -806,7 +806,7 @@ Proof. exists v; split; auto. destruct x; simpl; auto. erewrite Int64.mul_pow2' by eauto. - simpl in B. erewrite Int64.is_power2'_range in B by eauto. + simpl in B. erewrite Int64.is_power2'_range in B by eauto. exact B. apply eval_mull_base; auto. apply eval_longconst. Qed. @@ -828,18 +828,18 @@ Proof. - apply eval_mull_base; auto. Qed. -Theorem eval_mullhu: +Theorem eval_mullhu: forall n, unary_constructor_sound (fun a => mullhu a n) (fun v => Val.mullhu v (Vlong n)). Proof. - unfold mullhu; intros; red; intros. econstructor; split; eauto. - eapply eval_helper_2; eauto. apply eval_longconst. DeclHelper; eauto. UseHelper. + unfold mullhu; intros; red; intros. econstructor; split; eauto. + eapply eval_helper_2; eauto. apply eval_longconst. DeclHelper; eauto. UseHelper. Qed. -Theorem eval_mullhs: +Theorem eval_mullhs: forall n, unary_constructor_sound (fun a => mullhs a n) (fun v => Val.mullhs v (Vlong n)). Proof. - unfold mullhs; intros; red; intros. econstructor; split; eauto. - eapply eval_helper_2; eauto. apply eval_longconst. DeclHelper; eauto. UseHelper. + unfold mullhs; intros; red; intros. econstructor; split; eauto. + eapply eval_helper_2; eauto. apply eval_longconst. DeclHelper; eauto. UseHelper. Qed. Theorem eval_shrxlimm: diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index d8d916de..b885d22c 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -147,7 +147,7 @@ Lemma contains_get_stack: m |= contains (chunk_of_type ty) sp ofs spec -> exists v, load_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr ofs) = Some v /\ spec v. Proof. - intros. unfold load_stack. + intros. unfold load_stack. replace (Val.offset_ptr (Vptr sp Ptrofs.zero) (Ptrofs.repr ofs)) with (Vptr sp (Ptrofs.repr ofs)). eapply loadv_rule; eauto. simpl. rewrite Ptrofs.add_zero_l; auto. @@ -169,7 +169,7 @@ Lemma contains_set_stack: store_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr ofs) v = Some m' /\ m' |= contains (chunk_of_type ty) sp ofs spec ** P. Proof. - intros. unfold store_stack. + intros. unfold store_stack. replace (Val.offset_ptr (Vptr sp Ptrofs.zero) (Ptrofs.repr ofs)) with (Vptr sp (Ptrofs.repr ofs)). eapply storev_rule; eauto. simpl. rewrite Ptrofs.add_zero_l; auto. @@ -195,11 +195,11 @@ Program Definition contains_locations (j: meminj) (sp: block) (pos bound: Z) (sl b = sp /\ pos <= ofs < pos + 4 * bound |}. Next Obligation. - intuition auto. + intuition auto. - red; intros. eapply Mem.perm_unchanged_on; eauto. simpl; auto. - exploit H4; eauto. intros (v & A & B). exists v; split; auto. eapply Mem.load_unchanged_on; eauto. - simpl; intros. rewrite size_type_chunk, typesize_typesize in H8. + simpl; intros. rewrite size_type_chunk, typesize_typesize in H8. split; auto. omega. Qed. Next Obligation. @@ -214,9 +214,9 @@ Remark valid_access_location: Mem.valid_access m (chunk_of_type ty) sp (pos + 4 * ofs) p. Proof. intros; split. -- red; intros. apply Mem.perm_implies with Freeable; auto with mem. +- red; intros. apply Mem.perm_implies with Freeable; auto with mem. apply H0. rewrite size_type_chunk, typesize_typesize in H4. omega. -- rewrite align_type_chunk. apply Z.divide_add_r. +- rewrite align_type_chunk. apply Z.divide_add_r. apply Zdivide_trans with 8; auto. exists (8 / (4 * typealign ty)); destruct ty; reflexivity. apply Z.mul_divide_mono_l. auto. @@ -246,20 +246,20 @@ Lemma set_location: /\ m' |= contains_locations j sp pos bound sl (Locmap.set (S sl ofs ty) v ls) ** P. Proof. intros. destruct H as (A & B & C). destruct A as (D & E & F & G & H). - edestruct Mem.valid_access_store as [m' STORE]. - eapply valid_access_location; eauto. + edestruct Mem.valid_access_store as [m' STORE]. + eapply valid_access_location; eauto. assert (PERM: Mem.range_perm m' sp pos (pos + 4 * bound) Cur Freeable). { red; intros; eauto with mem. } exists m'; split. - unfold store_stack; simpl. rewrite Ptrofs.add_zero_l, Ptrofs.unsigned_repr; eauto. unfold Ptrofs.max_unsigned. generalize (typesize_pos ty). omega. - simpl. intuition auto. -+ unfold Locmap.set. ++ unfold Locmap.set. destruct (Loc.eq (S sl ofs ty) (S sl ofs0 ty0)); [|destruct (Loc.diff_dec (S sl ofs ty) (S sl ofs0 ty0))]. * (* same location *) inv e. rename ofs0 into ofs. rename ty0 into ty. exists (Val.load_result (chunk_of_type ty) v'); split. - eapply Mem.load_store_similar_2; eauto. omega. + eapply Mem.load_store_similar_2; eauto. omega. apply Val.load_result_inject; auto. * (* different locations *) exploit H; eauto. intros (v0 & X & Y). exists v0; split; auto. @@ -267,11 +267,11 @@ Proof. destruct d. congruence. right. rewrite ! size_type_chunk, ! typesize_typesize. omega. * (* overlapping locations *) destruct (Mem.valid_access_load m' (chunk_of_type ty0) sp (pos + 4 * ofs0)) as [v'' LOAD]. - apply Mem.valid_access_implies with Writable; auto with mem. + apply Mem.valid_access_implies with Writable; auto with mem. eapply valid_access_location; eauto. exists v''; auto. -+ apply (m_invar P) with m; auto. - eapply Mem.store_unchanged_on; eauto. ++ apply (m_invar P) with m; auto. + eapply Mem.store_unchanged_on; eauto. intros i; rewrite size_type_chunk, typesize_typesize. intros; red; intros. eelim C; eauto. simpl. split; auto. omega. Qed. @@ -284,7 +284,7 @@ Lemma initial_locations: m |= contains_locations j sp pos bound sl ls ** P. Proof. intros. destruct H as (A & B & C). destruct A as (D & E & F). split. -- simpl; intuition auto. red; intros; eauto with mem. +- simpl; intuition auto. red; intros; eauto with mem. destruct (Mem.valid_access_load m (chunk_of_type ty) sp (pos + 4 * ofs)) as [v LOAD]. eapply valid_access_location; eauto. red; intros; eauto with mem. @@ -389,7 +389,7 @@ Lemma frame_get_local: Proof. unfold frame_contents, frame_contents_1; intros. unfold slot_valid in H1; InvBooleans. apply mconj_proj1 in H. apply sep_proj1 in H. apply sep_proj1 in H. - eapply get_location; eauto. + eapply get_location; eauto. Qed. Lemma frame_get_outgoing: @@ -402,7 +402,7 @@ Lemma frame_get_outgoing: Proof. unfold frame_contents, frame_contents_1; intros. unfold slot_valid in H1; InvBooleans. apply mconj_proj1 in H. apply sep_proj1 in H. apply sep_pick2 in H. - eapply get_location; eauto. + eapply get_location; eauto. Qed. Lemma frame_get_parent: @@ -437,9 +437,9 @@ Lemma frame_set_local: /\ m' |= frame_contents j sp (Locmap.set (S Local ofs ty) v ls) ls0 parent retaddr ** P. Proof. intros. unfold frame_contents in H. - exploit mconj_proj1; eauto. unfold frame_contents_1. + exploit mconj_proj1; eauto. unfold frame_contents_1. rewrite ! sep_assoc; intros SEP. - unfold slot_valid in H1; InvBooleans. simpl in H0. + unfold slot_valid in H1; InvBooleans. simpl in H0. exploit set_location; eauto. intros (m' & A & B). exists m'; split; auto. assert (forall i k p, Mem.perm m sp i k p -> Mem.perm m' sp i k p). @@ -463,8 +463,8 @@ Lemma frame_set_outgoing: Proof. intros. unfold frame_contents in H. exploit mconj_proj1; eauto. unfold frame_contents_1. - rewrite ! sep_assoc, sep_swap. intros SEP. - unfold slot_valid in H1; InvBooleans. simpl in H0. + rewrite ! sep_assoc, sep_swap. intros SEP. + unfold slot_valid in H1; InvBooleans. simpl in H0. exploit set_location; eauto. intros (m' & A & B). exists m'; split; auto. assert (forall i k p, Mem.perm m sp i k p -> Mem.perm m' sp i k p). @@ -510,7 +510,7 @@ Proof. Local Opaque sepconj. induction rl; simpl; intros. - auto. -- apply frame_set_reg; auto. +- apply frame_set_reg; auto. Qed. Corollary frame_set_regpair: @@ -626,7 +626,7 @@ Lemma agree_regs_set_pair: Proof. intros. destruct p; simpl. - apply agree_regs_set_reg; auto. -- apply agree_regs_set_reg. apply agree_regs_set_reg; auto. +- apply agree_regs_set_reg. apply agree_regs_set_reg; auto. apply Val.hiword_inject; auto. apply Val.loword_inject; auto. Qed. @@ -728,7 +728,7 @@ Proof. apply agree_locs_set_reg; auto. apply caller_save_reg_within_bounds; auto. destruct H0. apply agree_locs_set_reg; auto. apply agree_locs_set_reg; auto. - apply caller_save_reg_within_bounds; auto. apply caller_save_reg_within_bounds; auto. + apply caller_save_reg_within_bounds; auto. apply caller_save_reg_within_bounds; auto. Qed. Lemma agree_locs_set_res: @@ -770,8 +770,8 @@ Lemma agree_locs_undef_locs: existsb is_callee_save regs = false -> agree_locs (LTL.undef_regs regs ls) ls0. Proof. - intros. eapply agree_locs_undef_locs_1; eauto. - intros. destruct (is_callee_save r) eqn:CS; auto. + intros. eapply agree_locs_undef_locs_1; eauto. + intros. destruct (is_callee_save r) eqn:CS; auto. assert (existsb is_callee_save regs = true). { apply existsb_exists. exists r; auto. } congruence. @@ -831,7 +831,7 @@ Lemma agree_callee_save_set_result: agree_callee_save ls1 ls2 -> agree_callee_save (Locmap.setpair (loc_result sg) v ls1) ls2. Proof. - intros; red; intros. rewrite Locmap.gpo. apply H; auto. + intros; red; intros. rewrite Locmap.gpo. apply H; auto. assert (X: forall r, is_callee_save r = false -> Loc.diff l (R r)). { intros. destruct l; auto. simpl; congruence. } generalize (loc_result_caller_save sg). destruct (loc_result sg); simpl; intuition auto. @@ -845,7 +845,7 @@ Definition no_callee_saves (l: list mreg) : Prop := Remark destroyed_by_op_caller_save: forall op, no_callee_saves (destroyed_by_op op). Proof. - unfold no_callee_saves; destruct op; reflexivity. + unfold no_callee_saves; destruct op; (reflexivity || destruct c; reflexivity). Qed. Remark destroyed_by_load_caller_save: @@ -950,10 +950,10 @@ Lemma save_callee_save_rec_correct: Proof. Local Opaque mreg_type. induction l as [ | r l]; simpl; intros until P; intros CS SEP AG. -- exists rs, m. +- exists rs, m. split. apply star_refl. split. rewrite sep_pure; split; auto. eapply sep_drop; eauto. - split. auto. + split. auto. auto. - set (ty := mreg_type r) in *. set (sz := AST.typesize ty) in *. @@ -971,17 +971,17 @@ Local Opaque mreg_type. apply range_contains in SEP; auto. exploit (contains_set_stack (fun v' => Val.inject j (ls (R r)) v') (rs r)). eexact SEP. - apply load_result_inject; auto. apply wt_ls. + apply load_result_inject; auto. apply wt_ls. clear SEP; intros (m1 & STORE & SEP). set (rs1 := undef_regs (destroyed_by_setstack ty) rs). assert (AG1: agree_regs j ls rs1). { red; intros. unfold rs1. destruct (In_dec mreg_eq r0 (destroyed_by_setstack ty)). erewrite ls_temp_undef by eauto. auto. rewrite undef_regs_other by auto. apply AG. } - rewrite sep_swap in SEP. + rewrite sep_swap in SEP. exploit (IHl (pos1 + sz) rs1 m1); eauto. intros (rs2 & m2 & A & B & C & D). - exists rs2, m2. + exists rs2, m2. split. eapply star_left; eauto. constructor. exact STORE. auto. traceEq. split. rewrite sep_assoc, sep_swap. exact B. split. intros. apply C. unfold store_stack in STORE; simpl in STORE. eapply Mem.perm_store_1; eauto. @@ -1042,16 +1042,16 @@ Proof. intros until P; intros SEP TY AGCS AG; intros ls1 rs1. exploit (save_callee_save_rec_correct j cs fb sp ls1). - intros. unfold ls1. apply LTL_undef_regs_same. eapply destroyed_by_setstack_function_entry; eauto. -- intros. unfold ls1. apply undef_regs_type. apply TY. +- intros. unfold ls1. apply undef_regs_type. apply TY. - exact b.(used_callee_save_prop). - eexact SEP. - instantiate (1 := rs1). apply agree_regs_undef_regs. apply agree_regs_call_regs. auto. - clear SEP. intros (rs' & m' & EXEC & SEP & PERMS & AG'). - exists rs', m'. + exists rs', m'. split. eexact EXEC. split. rewrite (contains_callee_saves_exten j sp ls0 ls1). exact SEP. intros. apply b.(used_callee_save_prop) in H. - unfold ls1. rewrite LTL_undef_regs_others. unfold call_regs. + unfold ls1. rewrite LTL_undef_regs_others. unfold call_regs. apply AGCS; auto. red; intros. assert (existsb is_callee_save destroyed_at_function_entry = false) @@ -1095,14 +1095,14 @@ Proof. unfold fn_stacksize, fn_link_ofs, fn_retaddr_ofs. (* Stack layout info *) Local Opaque b fe. - generalize (frame_env_range b) (frame_env_aligned b). replace (make_env b) with fe by auto. simpl. + generalize (frame_env_range b) (frame_env_aligned b). replace (make_env b) with fe by auto. simpl. intros LAYOUT1 LAYOUT2. (* Allocation step *) destruct (Mem.alloc m1' 0 (fe_size fe)) as [m2' sp'] eqn:ALLOC'. exploit alloc_parallel_rule_2. - eexact SEP. eexact ALLOC. eexact ALLOC'. + eexact SEP. eexact ALLOC. eexact ALLOC'. instantiate (1 := fe_stack_data fe). tauto. - reflexivity. + reflexivity. instantiate (1 := fe_stack_data fe + bound_stack_data b). rewrite Z.max_comm. reflexivity. generalize (bound_stack_data_pos b) size_no_overflow; omega. tauto. @@ -1139,23 +1139,23 @@ Local Opaque b fe. clear SEP; intros (rs2 & m5' & SAVE_CS & SEP & PERMS & AGREGS'). rewrite sep_swap5 in SEP. (* Materializing the Local and Outgoing locations *) - exploit (initial_locations j'). eexact SEP. tauto. - instantiate (1 := Local). instantiate (1 := ls1). + exploit (initial_locations j'). eexact SEP. tauto. + instantiate (1 := Local). instantiate (1 := ls1). intros; rewrite LS1. rewrite LTL_undef_regs_slot. reflexivity. clear SEP; intros SEP. rewrite sep_swap in SEP. - exploit (initial_locations j'). eexact SEP. tauto. - instantiate (1 := Outgoing). instantiate (1 := ls1). + exploit (initial_locations j'). eexact SEP. tauto. + instantiate (1 := Outgoing). instantiate (1 := ls1). intros; rewrite LS1. rewrite LTL_undef_regs_slot. reflexivity. clear SEP; intros SEP. rewrite sep_swap in SEP. (* Now we frame this *) assert (SEPFINAL: m5' |= frame_contents j' sp' ls1 ls0 parent ra ** minjection j' m2 ** globalenv_inject ge j' ** P). { eapply frame_mconj. eexact SEPCONJ. - rewrite chunk_of_Tptr in SEP. + rewrite chunk_of_Tptr in SEP. unfold frame_contents_1; rewrite ! sep_assoc. exact SEP. assert (forall ofs k p, Mem.perm m2' sp' ofs k p -> Mem.perm m5' sp' ofs k p). - { intros. apply PERMS. + { intros. apply PERMS. unfold store_stack in STORE_PARENT, STORE_RETADDR. simpl in STORE_PARENT, STORE_RETADDR. eauto using Mem.perm_store_1. } @@ -1172,7 +1172,7 @@ Local Opaque b fe. split. eexact SAVE_CS. split. exact AGREGS'. split. rewrite LS1. apply agree_locs_undef_locs; [|reflexivity]. - constructor; intros. unfold call_regs. apply AGCS. + constructor; intros. unfold call_regs. apply AGCS. unfold mreg_within_bounds in H; tauto. unfold call_regs. apply AGCS. auto. split. exact SEPFINAL. @@ -1229,13 +1229,13 @@ Local Opaque mreg_type. eauto. intros (rs' & A & B & C & D). exists rs'. - split. eapply star_step; eauto. + split. eapply star_step; eauto. econstructor. exact LOAD. traceEq. split. intros. - destruct (In_dec mreg_eq r0 l). auto. + destruct (In_dec mreg_eq r0 l). auto. assert (r = r0) by tauto. subst r0. rewrite C by auto. rewrite Regmap.gss. exact SPEC. - split. intros. + split. intros. rewrite C by tauto. apply Regmap.gso. intuition auto. exact D. Qed. @@ -1256,8 +1256,8 @@ Lemma restore_callee_save_correct: is_callee_save r = false -> rs' r = rs r). Proof. intros. - unfold frame_contents, frame_contents_1 in H. - apply mconj_proj1 in H. rewrite ! sep_assoc in H. apply sep_pick5 in H. + unfold frame_contents, frame_contents_1 in H. + apply mconj_proj1 in H. rewrite ! sep_assoc in H. apply sep_pick5 in H. exploit restore_callee_save_rec_correct; eauto. intros; unfold mreg_within_bounds; auto. intros (rs' & A & B & C & D). @@ -1304,7 +1304,7 @@ Proof. (* Reloading the callee-save registers *) exploit restore_callee_save_correct. eexact SEP. - instantiate (1 := rs). + instantiate (1 := rs). red; intros. destruct AGL. rewrite <- agree_unused_reg0 by auto. apply AGR. intros (rs' & LOAD_CS & CS & NCS). (* Reloading the back link and return address *) @@ -1320,7 +1320,7 @@ Proof. split. assumption. split. assumption. split. eassumption. - split. red; unfold return_regs; intros. + split. red; unfold return_regs; intros. destruct (is_callee_save r) eqn:C. apply CS; auto. rewrite NCS by auto. apply AGR. @@ -1418,7 +1418,7 @@ Lemma match_stacks_type_sp: Val.has_type (parent_sp cs') Tptr. Proof. induction 1; unfold parent_sp. apply Val.Vnullptr_has_type. apply Val.Vptr_has_type. -Qed. +Qed. Lemma match_stacks_type_retaddr: forall j cs cs' sg, @@ -1504,7 +1504,7 @@ Lemma is_tail_save_callee_save: is_tail k (save_callee_save_rec l ofs k). Proof. induction l; intros; simpl. auto with coqlib. - constructor; auto. + constructor; auto. Qed. Lemma is_tail_restore_callee_save: @@ -1512,7 +1512,7 @@ Lemma is_tail_restore_callee_save: is_tail k (restore_callee_save_rec l ofs k). Proof. induction l; intros; simpl. auto with coqlib. - constructor; auto. + constructor; auto. Qed. Lemma is_tail_transl_instr: @@ -1541,7 +1541,7 @@ Lemma is_tail_transf_function: is_tail (transl_code (make_env (function_bounds f)) c) (fn_code tf). Proof. intros. rewrite (unfold_transf_function _ _ H). simpl. - unfold transl_body, save_callee_save. + unfold transl_body, save_callee_save. eapply is_tail_trans. 2: apply is_tail_save_callee_save. apply is_tail_transl_code; auto. Qed. @@ -1636,7 +1636,7 @@ Proof. + elim (H1 _ H). + simpl in SEP. unfold parent_sp. assert (slot_valid f Outgoing pos ty = true). - { destruct H0. unfold slot_valid, proj_sumbool. + { destruct H0. unfold slot_valid, proj_sumbool. rewrite zle_true by omega. rewrite pred_dec_true by auto. reflexivity. } assert (slot_within_bounds (function_bounds f) Outgoing pos ty) by eauto. exploit frame_get_outgoing; eauto. intros (v & A & B). @@ -1651,10 +1651,10 @@ Lemma transl_external_argument_2: Proof. intros. destruct p as [l | l1 l2]. - destruct (transl_external_argument l) as (v & A & B). eapply in_regs_of_rpairs; eauto; simpl; auto. - exists v; split; auto. constructor; auto. + exists v; split; auto. constructor; auto. - destruct (transl_external_argument l1) as (v1 & A1 & B1). eapply in_regs_of_rpairs; eauto; simpl; auto. destruct (transl_external_argument l2) as (v2 & A2 & B2). eapply in_regs_of_rpairs; eauto; simpl; auto. - exists (Val.longofwords v1 v2); split. + exists (Val.longofwords v1 v2); split. constructor; auto. apply Val.longofwords_inject; auto. Qed. @@ -1724,7 +1724,7 @@ Local Opaque fe. - assert (loc_valid f x = true) by auto. destruct x as [r | [] ofs ty]; try discriminate. + exists (rs r); auto with barg. - + exploit frame_get_local; eauto. intros (v & A & B). + + exploit frame_get_local; eauto. intros (v & A & B). exists v; split; auto. constructor; auto. - econstructor; eauto with barg. - econstructor; eauto with barg. @@ -1734,12 +1734,12 @@ Local Opaque fe. apply sep_proj2 in SEP. apply sep_proj1 in SEP. exploit loadv_parallel_rule; eauto. instantiate (1 := Val.offset_ptr (Vptr sp' Ptrofs.zero) ofs'). simpl. rewrite ! Ptrofs.add_zero_l. econstructor; eauto. - intros (v' & A & B). exists v'; split; auto. constructor; auto. + intros (v' & A & B). exists v'; split; auto. constructor; auto. - econstructor; split; eauto with barg. unfold Val.offset_ptr. rewrite ! Ptrofs.add_zero_l. econstructor; eauto. - apply sep_proj2 in SEP. apply sep_proj1 in SEP. exploit loadv_parallel_rule; eauto. intros (v' & A & B). exists v'; auto with barg. -- econstructor; split; eauto with barg. +- econstructor; split; eauto with barg. - destruct IHeval_builtin_arg1 as (v1 & A1 & B1); auto using in_or_app. destruct IHeval_builtin_arg2 as (v2 & A2 & B2); auto using in_or_app. exists (Val.longofwords v1 v2); split; auto with barg. @@ -1776,7 +1776,7 @@ End BUILTIN_ARGUMENTS. >> Matching between source and target states is defined by [match_states] below. It implies: -- Satisfaction of the separation logic assertions that describe the contents +- Satisfaction of the separation logic assertions that describe the contents of memory. This is a separating conjunction of facts about: -- the current stack frame -- the frames in the call stack @@ -1864,7 +1864,7 @@ Proof. eapply slot_outgoing_argument_valid; eauto. intros (v & A & B). econstructor; split. - apply plus_one. eapply exec_Mgetparam; eauto. + apply plus_one. eapply exec_Mgetparam; eauto. rewrite (unfold_transf_function _ _ TRANSL). unfold fn_link_ofs. eapply frame_get_parent. eexact SEP. econstructor; eauto with coqlib. econstructor; eauto. @@ -1901,7 +1901,7 @@ Proof. apply plus_one. destruct sl; try discriminate. econstructor. eexact STORE. eauto. econstructor. eexact STORE. eauto. - econstructor. eauto. eauto. eauto. + econstructor. eauto. eauto. eauto. apply agree_regs_set_slot. apply agree_regs_undef_regs. auto. apply agree_locs_set_slot. apply agree_locs_undef_locs. auto. apply destroyed_by_setstack_caller_save. auto. eauto. eauto with coqlib. eauto. @@ -1923,7 +1923,7 @@ Proof. apply agree_regs_set_reg; auto. rewrite transl_destroyed_by_op. apply agree_regs_undef_regs; 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. + apply frame_set_reg. apply frame_undef_regs. exact SEP. - (* Lload *) assert (exists a', @@ -1935,7 +1935,7 @@ Proof. destruct H1 as [a' [A B]]. exploit loadv_parallel_rule. apply sep_proj2 in SEP. apply sep_proj2 in SEP. apply sep_proj1 in SEP. eexact SEP. - eauto. eauto. + eauto. eauto. intros [v' [C D]]. econstructor; split. apply plus_one. econstructor. @@ -1943,7 +1943,7 @@ 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. - apply agree_locs_set_reg. apply agree_locs_undef_locs. auto. apply destroyed_by_load_caller_save. auto. + apply agree_locs_set_reg. apply agree_locs_undef_locs. auto. apply destroyed_by_load_caller_save. auto. - (* Lstore *) assert (exists a', @@ -1954,14 +1954,14 @@ Proof. eapply agree_reglist; eauto. destruct H1 as [a' [A B]]. rewrite sep_swap3 in SEP. - exploit storev_parallel_rule. eexact SEP. eauto. eauto. apply AGREGS. + exploit storev_parallel_rule. eexact SEP. eauto. eauto. apply AGREGS. clear SEP; intros (m1' & C & SEP). rewrite sep_swap3 in SEP. econstructor; split. apply plus_one. econstructor. instantiate (1 := a'). rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved. eexact C. eauto. - econstructor. eauto. eauto. eauto. + econstructor. eauto. eauto. eauto. rewrite transl_destroyed_by_store. apply agree_regs_undef_regs; auto. apply agree_locs_undef_locs. auto. apply destroyed_by_store_caller_save. auto. eauto with coqlib. @@ -2018,7 +2018,7 @@ Proof. eapply match_stacks_change_meminj; eauto. apply agree_regs_set_res; auto. apply agree_regs_undef_regs; auto. eapply agree_regs_inject_incr; eauto. 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. + 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. exact SEP. @@ -2042,7 +2042,7 @@ Proof. econstructor. eauto. eauto. eauto. apply agree_regs_undef_regs; auto. apply agree_locs_undef_locs. auto. apply destroyed_by_cond_caller_save. - auto. + auto. eapply find_label_tail; eauto. apply frame_undef_regs; auto. @@ -2081,7 +2081,7 @@ Proof. revert TRANSL. unfold transf_fundef, transf_partial_fundef. destruct (transf_function f) as [tfn|] eqn:TRANSL; simpl; try congruence. intros EQ; inversion EQ; clear EQ; subst tf. - rewrite sep_comm, sep_assoc in SEP. + rewrite sep_comm, sep_assoc in SEP. exploit function_prologue_correct; eauto. red; intros; eapply wt_callstate_wt_regs; eauto. eapply match_stacks_type_sp; eauto. @@ -2111,16 +2111,16 @@ Proof. eapply match_stacks_change_meminj; eauto. apply agree_regs_set_pair. apply agree_regs_inject_incr with j; auto. auto. apply agree_callee_save_set_result; auto. - apply stack_contents_change_meminj with j; auto. + apply stack_contents_change_meminj with j; auto. rewrite sep_comm, sep_assoc; auto. - (* return *) - inv STACKS. simpl in AGLOCS. simpl in SEP. rewrite sep_assoc in SEP. + inv STACKS. simpl in AGLOCS. simpl in SEP. rewrite sep_assoc in SEP. econstructor; split. apply plus_one. apply exec_return. econstructor; eauto. apply agree_locs_return with rs0; auto. - apply frame_contents_exten with rs0 (parent_locset s); auto. + apply frame_contents_exten with rs0 (parent_locset s); auto. Qed. Lemma transf_initial_states: diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index 1dcdfb64..06e314f3 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -577,7 +577,7 @@ Proof. econstructor; eauto. apply (Genv.init_mem_transf TRANSL). auto. replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto. - symmetry; eapply match_program_main; eauto. + symmetry; eapply match_program_main; eauto. rewrite <- H3. apply sig_preserved. constructor. constructor. constructor. apply Mem.extends_refl. Qed. @@ -597,7 +597,7 @@ Theorem transf_program_correct: forward_simulation (RTL.semantics prog) (RTL.semantics tprog). Proof. eapply forward_simulation_opt with (measure := measure); eauto. - apply senv_preserved. + apply senv_preserved. eexact transf_initial_states. eexact transf_final_states. exact transf_step_correct. diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v index c79ae4fd..db03d0b3 100644 --- a/backend/Unusedglobproof.v +++ b/backend/Unusedglobproof.v @@ -315,11 +315,11 @@ Corollary used_globals_valid: valid_used_set p u. Proof. intros. constructor. -- intros. eapply used_globals_sound; eauto. +- intros. eapply used_globals_sound; eauto. - eapply used_globals_incl; eauto. apply seen_main_initial_workset. - intros. eapply used_globals_incl; eauto. apply seen_public_initial_workset; auto. - intros. apply ISF.for_all_iff in H0. -+ red in H0. apply H0 in H1. unfold global_defined in H1. ++ red in H0. apply H0 in H1. unfold global_defined in H1. destruct pm!id as [g|] eqn:E. * left. change id with (fst (id,g)). apply in_map. apply in_prog_defmap; auto. * InvBooleans; auto. @@ -394,7 +394,7 @@ Lemma filter_globdefs_map: Proof. intros. unfold PTree_Properties.of_list. fold prog_map. unfold PTree.elt. fold add_def. destruct (IS.mem id u) eqn:MEM. -- erewrite filter_globdefs_map_2. rewrite List.rev_involutive. reflexivity. +- erewrite filter_globdefs_map_2. rewrite List.rev_involutive. reflexivity. auto. auto. - apply filter_globdefs_map_1. auto. apply PTree.gempty. Qed. @@ -419,7 +419,7 @@ Proof. - constructor. - destruct (IS.mem id1 u) eqn:MEM; auto. rewrite filter_globdefs_nil, map_app. simpl. - apply list_norepet_append; auto. + apply list_norepet_append; auto. constructor. simpl; tauto. constructor. red; simpl; intros. destruct H0; try tauto. subst y. apply filter_globdefs_domain in H. rewrite ISF.remove_iff in H. intuition. @@ -433,11 +433,11 @@ Proof. unfold transform_program; intros p tp TR. set (pm := prog_defmap p) in *. destruct (used_globals p pm) as [u|] eqn:U; try discriminate. destruct (IS.for_all (global_defined p pm) u) eqn:DEF; inv TR. - exists u; split. + exists u; split. apply used_globals_valid; auto. constructor; simpl; auto. intros. unfold prog_defmap; simpl. apply filter_globdefs_map. - apply filter_globdefs_unique_names. + apply filter_globdefs_unique_names. Qed. (** * Semantic preservation *) @@ -480,7 +480,7 @@ Lemma transform_find_symbol_1: forall id b, Genv.find_symbol ge id = Some b -> kept id -> exists b', Genv.find_symbol tge id = Some b'. Proof. - intros. + intros. assert (A: exists g, (prog_defmap p)!id = Some g). { apply prog_defmap_dom. eapply Genv.find_symbol_inversion; eauto. } destruct A as (g & P). @@ -493,13 +493,13 @@ Lemma transform_find_symbol_2: forall id b, Genv.find_symbol tge id = Some b -> kept id /\ exists b', Genv.find_symbol ge id = Some b'. Proof. - intros. + intros. assert (A: exists g, (prog_defmap tp)!id = Some g). { apply prog_defmap_dom. eapply Genv.find_symbol_inversion; eauto. } destruct A as (g & P). - erewrite match_prog_def in P by eauto. + erewrite match_prog_def in P by eauto. destruct (IS.mem id used) eqn:U; try discriminate. - split. apply IS.mem_2; auto. + split. apply IS.mem_2; auto. apply Genv.find_symbol_exists with g. apply in_prog_defmap. auto. Qed. @@ -564,7 +564,7 @@ Proof. auto. - exploit transform_find_symbol_1; eauto. intros (b' & F). exists b'; split; auto. eapply init_meminj_eq; eauto. -- exploit transform_find_symbol_2; eauto. intros (K & b & F). +- exploit transform_find_symbol_2; eauto. intros (K & b & F). exists b; split; auto. eapply init_meminj_eq; eauto. - exploit init_meminj_invert; eauto. intros (A & id & B & C). assert (kept id) by (eapply transform_find_symbol_2; eauto). @@ -573,7 +573,7 @@ Proof. assert ((prog_defmap tp)!id = Some gd). { erewrite match_prog_def by eauto. rewrite IS.mem_1 by auto. auto. } rewrite Genv.find_def_symbol in H3. destruct H3 as (b1 & P & Q). - fold tge in P. replace b' with b1 by congruence. split; auto. split; auto. + fold tge in P. replace b' with b1 by congruence. split; auto. split; auto. intros. eapply kept_closed; eauto. - exploit init_meminj_invert; eauto. intros (A & id & B & C). assert ((prog_defmap tp)!id = Some gd). @@ -616,7 +616,7 @@ Proof. rewrite <- Genv.find_var_info_iff in A. rewrite A; auto. destruct (Genv.find_var_info tge b2) as [gv|] eqn:V2; auto. rewrite Genv.find_var_info_iff in V2. - exploit defs_rev_inject; eauto. intros (A & B). + exploit defs_rev_inject; eauto. intros (A & B). rewrite <- Genv.find_var_info_iff in A. congruence. Qed. @@ -805,15 +805,15 @@ Proof. - exploit Genv.find_funct_inv; eauto. intros (b & R). rewrite R in H0. rewrite Genv.find_funct_find_funct_ptr in H0. specialize (H1 r). rewrite R in H1. inv H1. - rewrite Genv.find_funct_ptr_iff in H0. + rewrite Genv.find_funct_ptr_iff in H0. exploit defs_inject; eauto. intros (A & B & C). - rewrite <- Genv.find_funct_ptr_iff in A. + rewrite <- Genv.find_funct_ptr_iff in A. rewrite B; auto. - destruct (Genv.find_symbol ge id) as [b|] eqn:FS; try discriminate. exploit symbols_inject_2; eauto. intros (tb & P & Q). rewrite P. - rewrite Genv.find_funct_ptr_iff in H0. + rewrite Genv.find_funct_ptr_iff in H0. exploit defs_inject; eauto. intros (A & B & C). - rewrite <- Genv.find_funct_ptr_iff in A. + rewrite <- Genv.find_funct_ptr_iff in A. auto. Qed. @@ -1057,7 +1057,7 @@ Proof. { induction l as [ | [id1 g1] l]; simpl; intros. - auto. - apply IHl. unfold Genv.add_global, P; simpl. intros LT. apply Plt_succ_inv in LT. destruct LT. - + rewrite PTree.gso. apply H; auto. apply Plt_ne; auto. + + rewrite PTree.gso. apply H; auto. apply Plt_ne; auto. + rewrite H0. rewrite PTree.gss. exists g1; auto. } apply H. red; simpl; intros. exfalso; xomega. Qed. @@ -1074,14 +1074,14 @@ Lemma init_meminj_invert_strong: /\ Genv.find_def tge b' = Some gd /\ (forall i, ref_def gd i -> kept i). Proof. - intros. exploit init_meminj_invert; eauto. intros (A & id & B & C). + intros. exploit init_meminj_invert; eauto. intros (A & id & B & C). assert (exists gd, (prog_defmap p)!id = Some gd). { apply prog_defmap_dom. eapply Genv.find_symbol_inversion; eauto. } destruct H0 as [gd DM]. rewrite Genv.find_def_symbol in DM. destruct DM as (b'' & P & Q). fold ge in P. rewrite P in B; inv B. fold ge in Q. exploit defs_inject. apply init_meminj_preserves_globals. - eauto. eauto. intros (X & _ & Y). - split. auto. exists id, gd; auto. + eauto. eauto. intros (X & _ & Y). + split. auto. exists id, gd; auto. Qed. Section INIT_MEM. @@ -1098,11 +1098,11 @@ Proof. induction il as [ | i1 il]; simpl; intros. - constructor. - apply list_forall2_app. -+ destruct i1; simpl; try (apply inj_bytes_inject). ++ destruct i1; simpl; try (apply inj_bytes_inject). induction (Z.to_nat z); simpl; constructor. constructor. auto. destruct (Genv.find_symbol ge i) as [b|] eqn:FS. assert (kept i). { apply H. red. exists i0; auto with coqlib. } - exploit symbols_inject_2. apply init_meminj_preserves_globals. eauto. eauto. + exploit symbols_inject_2. apply init_meminj_preserves_globals. eauto. eauto. intros (b' & A & B). rewrite A. apply inj_value_inject. econstructor; eauto. symmetry; apply Ptrofs.add_zero. destruct (Genv.find_symbol tge i) as [b'|] eqn:FS'. @@ -1123,7 +1123,7 @@ Proof. - inv H. rewrite inj_S in H1. destruct (zeq i p0). + congruence. + apply IHn with (p0 + 1); auto. omega. omega. -Qed. +Qed. Lemma init_mem_inj_1: Mem.mem_inj init_meminj m tm. @@ -1138,9 +1138,9 @@ Proof. apply Mem.perm_cur. auto. + intros (P2 & Q2 & R2 & S2) (P1 & Q1 & R1 & S1). apply Q1 in H0. destruct H0. subst. - apply Mem.perm_cur. eapply Mem.perm_implies; eauto. + apply Mem.perm_cur. eapply Mem.perm_implies; eauto. apply P2. omega. -- exploit init_meminj_invert; eauto. intros (A & id & B & C). +- exploit init_meminj_invert; eauto. intros (A & id & B & C). subst delta. apply Zdivide_0. - exploit init_meminj_invert_strong; eauto. intros (A & id & gd & B & C & D & E & F). exploit (Genv.init_mem_characterization_gen p); eauto. @@ -1157,9 +1157,9 @@ Local Transparent Mem.loadbytes. generalize (S2 NO). unfold Mem.loadbytes. destruct Mem.range_perm_dec; intros E2; inv E2. rewrite Zplus_0_r. apply Mem_getN_forall2 with (p := 0) (n := nat_of_Z (init_data_list_size (gvar_init v))). - rewrite H3, H4. apply bytes_of_init_inject. auto. - omega. - rewrite nat_of_Z_eq by (apply init_data_list_size_pos). omega. + rewrite H3, H4. apply bytes_of_init_inject. auto. + omega. + rewrite nat_of_Z_eq by (apply init_data_list_size_pos). omega. Qed. Lemma init_mem_inj_2: @@ -1168,9 +1168,9 @@ Proof. constructor; intros. - apply init_mem_inj_1. - destruct (init_meminj b) as [[b' delta]|] eqn:INJ; auto. - elim H. exploit init_meminj_invert; eauto. intros (A & id & B & C). + elim H. exploit init_meminj_invert; eauto. intros (A & id & B & C). eapply Genv.find_symbol_not_fresh; eauto. -- exploit init_meminj_invert; eauto. intros (A & id & B & C). +- exploit init_meminj_invert; eauto. intros (A & id & B & C). eapply Genv.find_symbol_not_fresh; eauto. - red; intros. exploit init_meminj_invert. eexact H0. intros (A1 & id1 & B1 & C1). @@ -1187,7 +1187,7 @@ Proof. left; apply Mem.perm_cur; auto. + intros (P2 & Q2 & R2 & S2) (P1 & Q1 & R1 & S1). apply Q2 in H0. destruct H0. subst. - left. apply Mem.perm_cur. eapply Mem.perm_implies; eauto. + left. apply Mem.perm_cur. eapply Mem.perm_implies; eauto. apply P1. omega. Qed. @@ -1198,7 +1198,7 @@ Lemma init_mem_exists: exists tm, Genv.init_mem tp = Some tm. Proof. intros. apply Genv.init_mem_exists. - intros. + intros. assert (P: (prog_defmap tp)!id = Some (Gvar v)). { eapply prog_defmap_norepet; eauto. eapply match_prog_unique; eauto. } rewrite (match_prog_def _ _ _ TRANSF) in P. destruct (IS.mem id used) eqn:U; try discriminate. @@ -1206,7 +1206,7 @@ Proof. split. auto. intros. exploit FV; eauto. intros (b & FS). apply transform_find_symbol_1 with b; auto. - apply kept_closed with id (Gvar v). + apply kept_closed with id (Gvar v). apply IS.mem_2; auto. auto. red. red. exists o; auto. Qed. @@ -1218,9 +1218,9 @@ Proof. intros. exploit init_mem_exists; eauto. intros [tm INIT]. exists init_meminj, tm. - split. auto. - split. eapply init_mem_inj_2; eauto. - apply init_meminj_preserves_globals. + split. auto. + split. eapply init_mem_inj_2; eauto. + apply init_meminj_preserves_globals. Qed. Lemma transf_initial_states: @@ -1228,7 +1228,7 @@ Lemma transf_initial_states: Proof. intros. inv H. exploit init_mem_inject; eauto. intros (j & tm & A & B & C). exploit symbols_inject_2. eauto. eapply kept_main. eexact H1. intros (tb & P & Q). - rewrite Genv.find_funct_ptr_iff in H2. + rewrite Genv.find_funct_ptr_iff in H2. exploit defs_inject. eauto. eexact Q. exact H2. intros (R & S & T). rewrite <- Genv.find_funct_ptr_iff in R. @@ -1286,15 +1286,15 @@ Local Transparent Linker_def Linker_fundef Linker_varinit Linker_vardef Linker_u destruct (link_varinit init1 init2) as [init|] eqn:LI... destruct (eqb ro1 ro2) eqn:RO... destruct (eqb vo1 vo2) eqn:VO... - simpl. + simpl. destruct info1, info2. assert (EITHER: init = init1 \/ init = init2). - { revert LI. unfold link_varinit. + { revert LI. unfold link_varinit. destruct (classify_init init1), (classify_init init2); intro EQ; inv EQ; auto. destruct (zeq sz (Z.max sz0 0 + 0)); inv H0; auto. destruct (zeq sz (init_data_list_size il)); inv H0; auto. destruct (zeq sz (init_data_list_size il)); inv H0; auto. } - apply eqb_prop in RO. apply eqb_prop in VO. + apply eqb_prop in RO. apply eqb_prop in VO. intro EQ; inv EQ. destruct EITHER; subst init; auto. Qed. @@ -1339,7 +1339,7 @@ Proof. + (* common definition *) exploit Y; eauto. intros (PUB1 & PUB2 & _). exploit link_def_either; eauto. intros [EQ|EQ]; subst gd. -* left. eapply used_closed. eexact V1. eapply used_public. eexact V1. eauto. eauto. auto. +* left. eapply used_closed. eexact V1. eapply used_public. eexact V1. eauto. eauto. auto. * right. eapply used_closed. eexact V2. eapply used_public. eexact V2. eauto. eauto. auto. + (* left definition *) inv H0. destruct (ISP.In_dec id used1). @@ -1358,7 +1358,7 @@ Proof. + (* no definition *) auto. - simpl. rewrite ISF.union_iff; left; eapply used_main; eauto. -- simpl. intros id. rewrite in_app_iff, ISF.union_iff. +- simpl. intros id. rewrite in_app_iff, ISF.union_iff. intros [A|A]; [left|right]; eapply used_public; eauto. - intros. rewrite ISF.union_iff in H. destruct (ident_eq id (prog_main p1)). @@ -1387,16 +1387,16 @@ Theorem link_match_program: Proof. intros. destruct H0 as (used1 & A1 & B1). destruct H1 as (used2 & A2 & B2). destruct (link_prog_inv _ _ _ H) as (U & V & W). - econstructor; split. + econstructor; split. - apply link_prog_succeeds. + rewrite (match_prog_main _ _ _ B1), (match_prog_main _ _ _ B2). auto. -+ intros. ++ intros. rewrite (match_prog_def _ _ _ B1) in H0. rewrite (match_prog_def _ _ _ B2) in H1. destruct (IS.mem id used1) eqn:U1; try discriminate. destruct (IS.mem id used2) eqn:U2; try discriminate. edestruct V as (X & Y & gd & Z); eauto. - split. rewrite (match_prog_public _ _ _ B1); auto. + split. rewrite (match_prog_public _ _ _ B1); auto. split. rewrite (match_prog_public _ _ _ B2); auto. congruence. - exists (IS.union used1 used2); split. @@ -1411,7 +1411,7 @@ Proof. destruct (prog_defmap p1)!id as [gd1|] eqn:GD1; destruct (prog_defmap p2)!id as [gd2|] eqn:GD2. - (* both defined *) - exploit V; eauto. intros (PUB1 & PUB2 & _). + exploit V; eauto. intros (PUB1 & PUB2 & _). assert (EQ1: IS.mem id used1 = true) by (apply IS.mem_1; eapply used_public; eauto). assert (EQ2: IS.mem id used2 = true) by (apply IS.mem_1; eapply used_public; eauto). rewrite EQ1, EQ2; auto. @@ -1428,7 +1428,7 @@ Proof. - (* none defined *) destruct (IS.mem id used1), (IS.mem id used2); auto. } -* intros. apply PTree.elements_keys_norepet. +* intros. apply PTree.elements_keys_norepet. Qed. Instance TransfSelectionLink : TransfLink match_prog := link_match_program. diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index c89f8435..17a518cd 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -1468,7 +1468,7 @@ End SOUNDNESS. (** ** Extension to separate compilation *) -(** Following Kang et al, POPL 2016, we now extend the results above +(** Following Kang et al, POPL 2016, we now extend the results above to the case where only one compilation unit is analyzed, and not the whole program. *) @@ -1485,14 +1485,14 @@ Inductive sound_state: state -> Prop := Theorem sound_step: forall st t st', RTL.step ge st t st' -> sound_state st -> sound_state st'. Proof. - intros. inv H0. constructor; intros. eapply sound_step_base; eauto. + intros. inv H0. constructor; intros. eapply sound_step_base; eauto. Qed. Remark sound_state_inv: forall st cunit, sound_state st -> linkorder cunit prog -> sound_state_base cunit ge st. Proof. - intros. inv H. eauto. + intros. inv H. eauto. Qed. End LINKING. @@ -1700,7 +1700,7 @@ Proof. rewrite PTree.gsspec in H2. destruct (peq id id1). inv H2. rewrite PTree.gss in H3. discriminate. assert (Plt b (Genv.genv_next g)) by (eapply Genv.genv_symb_range; eauto). - rewrite PTree.gso in H3 by (apply Plt_ne; auto). + rewrite PTree.gso in H3 by (apply Plt_ne; auto). assert (Mem.valid_block m b) by (red; rewrite <- H; auto). assert (b <> b1) by (apply Mem.valid_not_valid_diff with m; eauto with mem). apply bmatch_inv with m. @@ -1729,7 +1729,7 @@ Proof. intros. eapply Mem.loadbytes_drop; eauto. right; right; right. unfold Genv.perm_globvar. rewrite H4, H5. constructor. + assert (Plt b (Genv.genv_next g)) by (eapply Genv.genv_symb_range; eauto). - rewrite PTree.gso in H3 by (apply Plt_ne; auto). + rewrite PTree.gso in H3 by (apply Plt_ne; auto). assert (Mem.valid_block m b) by (red; rewrite <- H; auto). assert (b <> b1) by (apply Mem.valid_not_valid_diff with m; eauto with mem). apply bmatch_inv with m3. @@ -1773,14 +1773,14 @@ Lemma alloc_global_consistent: Proof. intros; red; intros. destruct idg as [id1 [f1 | v1]]; simpl in *. - rewrite PTree.grspec in H0. destruct (PTree.elt_eq id id1); try discriminate. - rewrite PTree.gso by auto. apply H; auto. + rewrite PTree.gso by auto. apply H; auto. - destruct (gvar_readonly v1 && negb (gvar_volatile v1) && definitive_initializer (gvar_init v1)) eqn:RO. + InvBooleans. rewrite negb_true_iff in H4. rewrite PTree.gsspec in *. destruct (peq id id1). * inv H0. exists v1; auto. * apply H; auto. + rewrite PTree.grspec in H0. destruct (PTree.elt_eq id id1); try discriminate. - rewrite PTree.gso by auto. apply H; auto. + rewrite PTree.gso by auto. apply H; auto. Qed. Lemma romem_for_consistent: @@ -1802,7 +1802,7 @@ Proof. exploit (romem_for_consistent cunit); eauto. intros (v & DM & RO & VO & DEFN & AB). destruct (prog_defmap_linkorder _ _ _ _ H DM) as (gd & P & Q). assert (gd = Gvar v). - { inv Q. inv H2. simpl in *. f_equal. f_equal. + { inv Q. inv H2. simpl in *. f_equal. f_equal. destruct info1, info2; auto. inv H3; auto; discriminate. } subst gd. exists v; auto. diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 4b782286..f905ffa2 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -425,7 +425,7 @@ Proof. cmatch (Val.cmpu_bool valid c (Vptr b1 ofs1) (Vptr b2 ofs2)) (Maybe (Ptrofs.cmpu c ofs1 ofs2))). { - intros. subst b2. simpl. destruct Archi.ptr64. + intros. subst b2. simpl. destruct Archi.ptr64. constructor. rewrite dec_eq_true. destruct ((valid b1 (Ptrofs.unsigned ofs1) || valid b1 (Ptrofs.unsigned ofs1 - 1)) && @@ -1492,7 +1492,7 @@ Proof. - apply vmatch_uns. red; intros. rewrite Int.bits_rol by auto. generalize (Int.unsigned_range n); intros. rewrite Zmod_small by omega. - apply H1. omega. omega. + apply H1. omega. omega. - destruct (zlt n0 Int.zwordsize); auto with va. apply vmatch_sgn. red; intros. rewrite ! Int.bits_rol by omega. generalize (Int.unsigned_range n); intros. @@ -1732,7 +1732,7 @@ Proof. destruct (Int.ltu i0 Int64.iwordsize'); constructor. } unfold shift_long. destruct y; auto. destruct (Int.ltu n Int64.iwordsize') eqn:LT; auto. - destruct x; auto. + destruct x; auto. inv H; inv H0. rewrite LT. constructor. Qed. @@ -1966,6 +1966,19 @@ Proof. rewrite LTU; auto with va. Qed. +Definition rolml (x: aval) (amount: int) (mask: int64) := + andl (roll x (I amount)) (L mask). + +Lemma rolml_sound: + forall v x amount mask, + vmatch v x -> vmatch (Val.rolml v amount mask) (rolml x amount mask). +Proof. + intros. + replace (Val.rolml v amount mask) with (Val.andl (Val.roll v (Vint amount)) (Vlong mask)). + apply andl_sound. apply roll_sound. auto. constructor. constructor. + destruct v; auto. +Qed. + (** Pointer operations *) Definition offset_ptr (v: aval) (n: ptrofs) := @@ -2101,7 +2114,7 @@ Proof. apply Z.min_case; auto with va. Qed. -Definition longofint (v: aval) := +Definition longofint (v: aval) := match v with | I i => L (Int64.repr (Int.signed i)) | _ => ntop1 v @@ -2113,7 +2126,7 @@ Proof. unfold Val.longofint, longofint; intros; inv H; auto with va. Qed. -Definition longofintu (v: aval) := +Definition longofintu (v: aval) := match v with | I i => L (Int64.repr (Int.unsigned i)) | _ => ntop1 v @@ -2637,7 +2650,7 @@ Proof. assert (IP: forall i b ofs, cmatch (Val.cmpu_bool valid c (Vint i) (Vptr b ofs)) (cmp_different_blocks c)). { - intros. simpl. destruct Archi.ptr64. + intros. simpl. destruct Archi.ptr64. apply cmp_different_blocks_none. destruct (Int.eq i Int.zero && (valid b (Ptrofs.unsigned ofs) || valid b (Ptrofs.unsigned ofs - 1))). apply cmp_different_blocks_sound. apply cmp_different_blocks_none. @@ -2645,7 +2658,7 @@ Proof. assert (PI: forall i b ofs, cmatch (Val.cmpu_bool valid c (Vptr b ofs) (Vint i)) (cmp_different_blocks c)). { - intros. simpl. destruct Archi.ptr64. + intros. simpl. destruct Archi.ptr64. apply cmp_different_blocks_none. destruct (Int.eq i Int.zero && (valid b (Ptrofs.unsigned ofs) || valid b (Ptrofs.unsigned ofs - 1))). apply cmp_different_blocks_sound. apply cmp_different_blocks_none. @@ -2942,7 +2955,7 @@ Proof with (auto using provenance_monotone with va). - destruct (zlt n2 16); constructor... - destruct ptr64... - destruct ptr64... -- destruct ptr64... +- destruct ptr64... - destruct ptr64... - destruct ptr64... - destruct ptr64... @@ -3511,7 +3524,7 @@ Proof. - unfold ablock_load_anywhere; intros; congruence. - assert (A: forall i, ZTree.get i (ab_contents ab1) = ZTree.get i (ab_contents ab2)). { - intros. exploit ZTree.beq_sound; eauto. instantiate (1 := i). + intros. exploit ZTree.beq_sound; eauto. instantiate (1 := i). destruct (ab_contents ab1)##i, (ab_contents ab2)##i; intros; try contradiction. InvBooleans; subst; auto. auto. } @@ -3569,7 +3582,7 @@ Proof. { exploit smatch_lub_l; eauto. instantiate (1 := ab_summary y). intros [SUMM _]. eapply vnormalize_cast; eauto. } exploit BM2; eauto. - unfold ablock_load; simpl. rewrite ZTree.gcombine by auto. + unfold ablock_load; simpl. rewrite ZTree.gcombine by auto. unfold combine_acontents; destruct (ab_contents x)##ofs as [[chunkx avx]|], (ab_contents y)##ofs as [[chunky avy]|]; auto. destruct (chunk_eq chunkx chunky); auto. subst chunky. @@ -3588,7 +3601,7 @@ Proof. { exploit smatch_lub_r; eauto. instantiate (1 := ab_summary x). intros [SUMM _]. eapply vnormalize_cast; eauto. } exploit BM2; eauto. - unfold ablock_load; simpl. rewrite ZTree.gcombine by auto. + unfold ablock_load; simpl. rewrite ZTree.gcombine by auto. unfold combine_acontents; destruct (ab_contents x)##ofs as [[chunkx avx]|], (ab_contents y)##ofs as [[chunky avy]|]; auto. destruct (chunk_eq chunkx chunky); auto. subst chunky. |