aboutsummaryrefslogtreecommitdiffstats
path: root/backend
diff options
context:
space:
mode:
authorBernhard Schommer <bschommer@users.noreply.github.com>2017-05-03 11:18:32 +0200
committerGitHub <noreply@github.com>2017-05-03 11:18:32 +0200
commit7873af34a9520ee5a8a6f10faddf3255a4ff02b2 (patch)
tree74500c845c99b39ba91a5507656060dea60404ea /backend
parent25ea686abc4cce13aba92196dbeb284f727b6e0e (diff)
downloadcompcert-7873af34a9520ee5a8a6f10faddf3255a4ff02b2.tar.gz
compcert-7873af34a9520ee5a8a6f10faddf3255a4ff02b2.zip
Hybrid 64bit/32bit PowerPC port
This commit adds code generation for 64bit PowerPC architectures which execute 32bit applications. The main difference to the normal 32bit PowerPC port is that it uses the available 64bit instructions instead of using the runtime library functions. However pointers are still 32bit and the 32bit calling convention is used. In order to use this port the target architecture must be either in Server execution mode or if in Embedded execution mode the high order 32 bits of GPRs must be implemented in 32-bit mode. Furthermore the operating system must preserve the high order 32 bits of GPRs.
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-06-29 11:31:29 +0000