aboutsummaryrefslogtreecommitdiffstats
path: root/backend
diff options
context:
space:
mode:
Diffstat (limited to 'backend')
-rw-r--r--backend/Allocation.v134
-rw-r--r--backend/Allocproof.v338
-rw-r--r--backend/Asmgenproof0.v6
-rw-r--r--backend/Bounds.v22
-rw-r--r--backend/CSEproof.v4
-rw-r--r--backend/Cminor.v2
-rw-r--r--backend/Constpropproof.v20
-rw-r--r--backend/Conventions.v8
-rw-r--r--backend/Deadcodeproof.v2
-rw-r--r--backend/Inliningproof.v2
-rw-r--r--backend/Inliningspec.v10
-rw-r--r--backend/Lineartyping.v2
-rw-r--r--backend/Locations.v4
-rw-r--r--backend/PrintAsmaux.ml1
-rw-r--r--backend/RTLtyping.v2
-rw-r--r--backend/Regalloc.ml40
-rw-r--r--backend/SelectDiv.vp12
-rw-r--r--backend/SelectDivproof.v50
-rw-r--r--backend/Selection.v4
-rw-r--r--backend/Selectionproof.v63
-rw-r--r--backend/SplitLong.vp4
-rw-r--r--backend/SplitLongproof.v20
-rw-r--r--backend/Stackingproof.v152
-rw-r--r--backend/Tailcallproof.v4
-rw-r--r--backend/Unusedglobproof.v96
-rw-r--r--backend/ValueAnalysis.v16
-rw-r--r--backend/ValueDomain.v35
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.
generated by cgit (git 2.34.1) at 2024-07-01 14:35:14 +0000