From f5da5188171962d13b9f3eac04845dd19d0aa931 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 22 Apr 2020 08:08:21 +0200 Subject: automated writing Compiler.v --- Makefile | 2 +- backend/Allocationproof.v | 2619 +++++++++++++++++++++++++++++++++++++++++++++ backend/Allocproof.v | 2619 --------------------------------------------- backend/Tunneling.v | 2 +- backend/Tunnelingproof.v | 2 +- driver/Compiler.vexpand | 119 +- tools/compiler_expand.ml | 87 +- 7 files changed, 2709 insertions(+), 2741 deletions(-) create mode 100644 backend/Allocationproof.v delete mode 100644 backend/Allocproof.v diff --git a/Makefile b/Makefile index 2f9ab029..ba8add27 100644 --- a/Makefile +++ b/Makefile @@ -100,7 +100,7 @@ BACKEND=\ ForwardMoves.v ForwardMovesproof.v \ FirstNop.v FirstNopproof.v \ Allnontrap.v Allnontrapproof.v \ - Allocation.v Allocproof.v \ + Allocation.v Allocationproof.v \ Tunneling.v Tunnelingproof.v \ Linear.v Lineartyping.v \ Linearize.v Linearizeproof.v \ diff --git a/backend/Allocationproof.v b/backend/Allocationproof.v new file mode 100644 index 00000000..3c7df58a --- /dev/null +++ b/backend/Allocationproof.v @@ -0,0 +1,2619 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Correctness proof for the [Allocation] pass (validated translation from + RTL to LTL). *) + +Require Import FunInd. +Require Import FSets. +Require Import Coqlib Ordered Maps Errors Integers Floats. +Require Import AST Linking Lattice Kildall. +Require Import Values Memory Globalenvs Events Smallstep. +Require Archi. +Require Import Op Registers RTL Locations Conventions RTLtyping LTL. +Require Import Allocation. + +Definition match_prog (p: RTL.program) (tp: LTL.program) := + match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. + +Lemma transf_program_match: + forall p tp, transf_program p = OK tp -> match_prog p tp. +Proof. + intros. eapply match_transform_partial_program; eauto. +Qed. + +(** * Soundness of structural checks *) + +Definition expand_move (m: move) : instruction := + match m with + | 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 := + List.map expand_move mv ++ k. + +Definition wf_move (m: move) : Prop := + match m with + | MV (S _ _ _) (S _ _ _) => False + | _ => True + end. + +Definition wf_moves (mv: moves) : Prop := + List.Forall wf_move mv. + +Inductive expand_block_shape: block_shape -> RTL.instruction -> LTL.bblock -> Prop := + | ebs_nop: forall mv s k, + wf_moves mv -> + expand_block_shape (BSnop mv s) + (Inop s) + (expand_moves mv (Lbranch s :: k)) + | ebs_move: forall src dst mv s k, + wf_moves mv -> + expand_block_shape (BSmove src dst mv s) + (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 -> + 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 -> + 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 -> + expand_block_shape (BShighlong src dst mv s) + (Iop Ohighlong (src :: nil) dst s) + (expand_moves mv (Lbranch s :: k)) + | ebs_op: forall op args res mv1 args' res' mv2 s k, + wf_moves mv1 -> wf_moves mv2 -> + expand_block_shape (BSop op args res mv1 args' res' mv2 s) + (Iop op args res s) + (expand_moves mv1 + (Lop op args' res' :: expand_moves mv2 (Lbranch s :: k))) + | ebs_op_dead: forall op args res mv s k, + wf_moves mv -> + expand_block_shape (BSopdead op args res mv s) + (Iop op args res s) + (expand_moves mv (Lbranch s :: k)) + | ebs_load: forall trap chunk addr args dst mv1 args' dst' mv2 s k, + wf_moves mv1 -> wf_moves mv2 -> + expand_block_shape (BSload trap chunk addr args dst mv1 args' dst' mv2 s) + (Iload trap chunk addr args dst s) + (expand_moves mv1 + (Lload trap 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 -> + expand_block_shape (BSload2 addr addr2 args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s) + (Iload TRAP Mint64 addr args dst s) + (expand_moves mv1 + (Lload TRAP Mint32 addr args1' dst1' :: + expand_moves mv2 + (Lload TRAP Mint32 addr2 args2' dst2' :: + 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 -> + expand_block_shape (BSload2_1 addr args dst mv1 args' dst' mv2 s) + (Iload TRAP Mint64 addr args dst s) + (expand_moves mv1 + (Lload TRAP Mint32 addr args' dst' :: + 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 -> + expand_block_shape (BSload2_2 addr addr2 args dst mv1 args' dst' mv2 s) + (Iload TRAP Mint64 addr args dst s) + (expand_moves mv1 + (Lload TRAP Mint32 addr2 args' dst' :: + expand_moves mv2 (Lbranch s :: k))) + | ebs_load_dead: forall trap chunk addr args dst mv s k, + wf_moves mv -> + expand_block_shape (BSloaddead chunk addr args dst mv s) + (Iload trap chunk addr args dst s) + (expand_moves mv (Lbranch s :: k)) + | ebs_store: forall chunk addr args src mv1 args' src' s k, + wf_moves mv1 -> + expand_block_shape (BSstore chunk addr args src mv1 args' src' s) + (Istore chunk addr args src s) + (expand_moves mv1 + (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 -> + expand_block_shape (BSstore2 addr addr2 args src mv1 args1' src1' mv2 args2' src2' s) + (Istore Mint64 addr args src s) + (expand_moves mv1 + (Lstore Mint32 addr args1' src1' :: + expand_moves mv2 + (Lstore Mint32 addr2 args2' src2' :: + Lbranch s :: k))) + | ebs_call: forall sg ros args res mv1 ros' mv2 s k, + wf_moves mv1 -> wf_moves mv2 -> + expand_block_shape (BScall sg ros args res mv1 ros' mv2 s) + (Icall sg ros args res s) + (expand_moves mv1 + (Lcall sg ros' :: expand_moves mv2 (Lbranch s :: k))) + | ebs_tailcall: forall sg ros args mv ros' k, + wf_moves mv -> + expand_block_shape (BStailcall sg ros args mv ros') + (Itailcall sg ros args) + (expand_moves mv (Ltailcall sg ros' :: k)) + | ebs_builtin: forall ef args res mv1 args' res' mv2 s k, + wf_moves mv1 -> wf_moves mv2 -> + expand_block_shape (BSbuiltin ef args res mv1 args' res' mv2 s) + (Ibuiltin ef args res s) + (expand_moves mv1 + (Lbuiltin ef args' res' :: expand_moves mv2 (Lbranch s :: k))) + | ebs_cond: forall cond args mv args' s1 s2 k i i', + wf_moves mv -> + expand_block_shape (BScond cond args mv args' s1 s2) + (Icond cond args s1 s2 i) + (expand_moves mv (Lcond cond args' s1 s2 i' :: k)) + | ebs_jumptable: forall arg mv arg' tbl k, + wf_moves mv -> + expand_block_shape (BSjumptable arg mv arg' tbl) + (Ijumptable arg tbl) + (expand_moves mv (Ljumptable arg' tbl :: k)) + | ebs_return: forall optarg mv k, + wf_moves mv -> + expand_block_shape (BSreturn optarg mv) + (Ireturn optarg) + (expand_moves mv (Lreturn :: k)). + +Ltac MonadInv := + match goal with + | [ H: match ?x with Some _ => _ | None => None end = Some _ |- _ ] => + destruct x as [] eqn:? ; [MonadInv|discriminate] + | [ H: match ?x with left _ => _ | right _ => None end = Some _ |- _ ] => + destruct x; [MonadInv|discriminate] + | [ 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 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 _ |- _ ] => + destruct x as [] eqn:? ; MonadInv + | [ H: Some _ = Some _ |- _ ] => + inv H; MonadInv + | [ H: None = Some _ |- _ ] => + discriminate + | _ => + idtac + end. + +Remark expand_moves_cons: + forall m accu b, + expand_moves (rev (m :: accu)) b = expand_moves (rev accu) (expand_move m :: b). +Proof. + unfold expand_moves; intros. simpl. rewrite map_app. rewrite app_ass. auto. +Qed. + +Lemma extract_moves_sound: + forall b mv b', + extract_moves 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 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 (is_move_operation op args) as [arg|] eqn:E. + exploit is_move_operation_correct; eauto. intros [A B]; subst. + (* reg-reg move *) + exploit IHb; eauto. constructor; auto. exact I. rewrite expand_moves_cons; auto. + inv H; apply BASE; auto. + + (* 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 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: + forall s b, check_succ s b = true -> exists k, b = Lbranch s :: k. +Proof. + intros. destruct b; simpl in H; try discriminate. + destruct i; try discriminate. + destruct (peq s s0); simpl in H; inv H. exists b; auto. +Qed. + +Ltac UseParsingLemmas := + match goal with + | [ H: extract_moves nil _ = (_, _) |- _ ] => + destruct (extract_moves_sound _ _ _ H); clear H; subst; UseParsingLemmas + | [ H: extract_moves_ext nil _ = (_, _) |- _ ] => + destruct (extract_moves_ext_sound _ _ _ H); clear H; subst; UseParsingLemmas + | [ H: check_succ _ _ = true |- _ ] => + try (discriminate H); + destruct (check_succ_sound _ _ H); clear H; subst; UseParsingLemmas + | _ => idtac + end. + +Lemma pair_instr_block_sound: + forall i b bsh, + pair_instr_block i b = Some bsh -> expand_block_shape bsh i b. +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. + MonadInv; UseParsingLemmas. + destruct i; MonadInv; UseParsingLemmas. + eapply ebs_op; eauto. + inv H0. eapply ebs_op_dead; eauto. } + + intros; destruct i; simpl in H; MonadInv; UseParsingLemmas. +- (* nop *) + econstructor; eauto. +- (* op *) + destruct (classify_operation o l). ++ (* move *) + MonadInv; UseParsingLemmas. econstructor; eauto. ++ (* makelong *) + destruct Archi.splitlong eqn:SL; eauto. + MonadInv; UseParsingLemmas. econstructor; eauto. ++ (* lowlong *) + destruct Archi.splitlong eqn:SL; eauto. + MonadInv; UseParsingLemmas. econstructor; eauto. ++ (* highlong *) + destruct Archi.splitlong eqn:SL; eauto. + MonadInv; UseParsingLemmas. econstructor; eauto. ++ (* other ops *) + eauto. +- (* load *) + destruct b0 as [ | [] b0]; MonadInv; UseParsingLemmas. + 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). + 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. + discriminate. + eapply ebs_load; eauto. + inv H. eapply ebs_load_dead; eauto. +- (* store *) + destruct b0; MonadInv. destruct i; MonadInv; UseParsingLemmas. + destruct (chunk_eq m Mint64 && Archi.splitlong) eqn:A; MonadInv; UseParsingLemmas. + destruct b as [ | [] b]; MonadInv; UseParsingLemmas. + InvBooleans. subst m. eapply ebs_store2; eauto. + eapply ebs_store; eauto. +- (* call *) + destruct b0 as [|[] ]; MonadInv; UseParsingLemmas. econstructor; eauto. +- (* tailcall *) + destruct b0 as [|[] ]; MonadInv; UseParsingLemmas. econstructor; eauto. +- (* builtin *) + destruct b1 as [|[] ]; MonadInv; UseParsingLemmas. econstructor; eauto. +- (* cond *) + destruct b0 as [|[]]; MonadInv; UseParsingLemmas. econstructor; eauto. +- (* jumptable *) + destruct b0 as [|[]]; MonadInv; UseParsingLemmas. econstructor; eauto. +- (* return *) + destruct b0 as [|[]]; MonadInv; UseParsingLemmas. econstructor; eauto. +Qed. + +Lemma matching_instr_block: + forall f1 f2 pc bsh i, + (pair_codes f1 f2)!pc = Some bsh -> + (RTL.fn_code f1)!pc = Some i -> + exists b, (LTL.fn_code f2)!pc = Some b /\ expand_block_shape bsh i b. +Proof. + intros. unfold pair_codes in H. rewrite PTree.gcombine in H; auto. rewrite H0 in H. + destruct (LTL.fn_code f2)!pc as [b|]. + exists b; split; auto. apply pair_instr_block_sound; auto. + discriminate. +Qed. + +(** * Properties of equations *) + +Module ESF := FSetFacts.Facts(EqSet). +Module ESP := FSetProperties.Properties(EqSet). +Module ESD := FSetDecide.Decide(EqSet). + +Definition sel_val (k: equation_kind) (v: val) : val := + match k with + | Full => v + | Low => Val.loword v + | High => Val.hiword v + end. + +(** A set of equations [e] is satisfied in a RTL pseudoreg state [rs] + and an LTL location state [ls] if, for every equation [r = l [k]] in [e], + [sel_val k (rs#r)] (the [k] fragment of [r]'s value in the RTL code) + is less defined than [ls l] (the value of [l] in the LTL code). *) + +Definition satisf (rs: regset) (ls: locset) (e: eqs) : Prop := + forall q, EqSet.In q e -> Val.lessdef (sel_val (ekind q) rs#(ereg q)) (ls (eloc q)). + +Lemma empty_eqs_satisf: + forall rs ls, satisf rs ls empty_eqs. +Proof. + unfold empty_eqs; intros; red; intros. ESD.fsetdec. +Qed. + +Lemma satisf_incr: + forall rs ls (e1 e2: eqs), + satisf rs ls e2 -> EqSet.Subset e1 e2 -> satisf rs ls e1. +Proof. + unfold satisf; intros. apply H. ESD.fsetdec. +Qed. + +Lemma satisf_undef_reg: + forall rs ls e r, + satisf rs ls e -> + satisf (rs#r <- Vundef) ls e. +Proof. + intros; red; intros. rewrite Regmap.gsspec. destruct (peq (ereg q) r); auto. + destruct (ekind q); simpl; auto. +Qed. + +Lemma add_equation_lessdef: + forall rs ls q e, + satisf rs ls (add_equation q e) -> Val.lessdef (sel_val (ekind q) rs#(ereg q)) (ls (eloc q)). +Proof. + intros. apply H. unfold add_equation. simpl. apply EqSet.add_1. auto. +Qed. + +Lemma add_equation_satisf: + forall rs ls q e, + satisf rs ls (add_equation q e) -> satisf rs ls e. +Proof. + intros. eapply satisf_incr; eauto. unfold add_equation. simpl. ESD.fsetdec. +Qed. + +Lemma add_equations_satisf: + forall rs ls rl ml e e', + add_equations rl ml e = Some e' -> + satisf rs ls e' -> satisf rs ls e. +Proof. + induction rl; destruct ml; simpl; intros; MonadInv. + auto. + eapply add_equation_satisf; eauto. +Qed. + +Lemma add_equations_lessdef: + forall rs ls rl ml e e', + add_equations rl ml e = Some e' -> + satisf rs ls e' -> + Val.lessdef_list (rs##rl) (reglist ls ml). +Proof. + induction rl; destruct ml; simpl; intros; MonadInv. + constructor. + constructor; eauto. + apply add_equation_lessdef with (e := e) (q := Eq Full a (R m)). + eapply add_equations_satisf; eauto. +Qed. + +Lemma add_equations_args_satisf: + forall rs ls rl tyl ll e e', + add_equations_args rl tyl ll e = Some e' -> + satisf rs ls e' -> satisf rs ls e. +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. +Qed. + +Lemma val_longofwords_eq_1: + forall v, + 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. +- 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: + forall rs ls rl tyl ll e e', + add_equations_args rl tyl ll e = Some e' -> + satisf rs ls e' -> + Val.has_type_list (rs##rl) tyl -> + Val.lessdef_list (rs##rl) (map (fun p => Locmap.getpair p ls) ll). +Proof. + intros until e'. functional induction (add_equations_args rl tyl ll e); simpl; intros. +- 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_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. +Qed. + +Lemma add_equation_ros_satisf: + forall rs ls ros mos e e', + add_equation_ros ros mos e = Some e' -> + satisf rs ls e' -> satisf rs ls e. +Proof. + unfold add_equation_ros; intros. destruct ros; destruct mos; MonadInv. + eapply add_equation_satisf; eauto. + auto. +Qed. + +Lemma remove_equation_satisf: + forall rs ls q e, + satisf rs ls e -> satisf rs ls (remove_equation q e). +Proof. + intros. eapply satisf_incr; eauto. unfold remove_equation; simpl. ESD.fsetdec. +Qed. + +Lemma remove_equation_res_satisf: + forall rs ls r l e e', + remove_equations_res r l e = Some e' -> + satisf rs ls e -> satisf rs ls e'. +Proof. + intros. functional inversion H. + apply remove_equation_satisf; auto. + apply remove_equation_satisf. apply remove_equation_satisf; auto. +Qed. + +Remark select_reg_l_monotone: + forall r q1 q2, + OrderedEquation.eq q1 q2 \/ OrderedEquation.lt q1 q2 -> + select_reg_l r q1 = true -> select_reg_l r q2 = true. +Proof. + unfold select_reg_l; intros. destruct H. + red in H. congruence. + rewrite Pos.leb_le in *. red in H. destruct H as [A | [A B]]. + red in A. zify; omega. + rewrite <- A; auto. +Qed. + +Remark select_reg_h_monotone: + forall r q1 q2, + OrderedEquation.eq q1 q2 \/ OrderedEquation.lt q2 q1 -> + select_reg_h r q1 = true -> select_reg_h r q2 = true. +Proof. + unfold select_reg_h; intros. destruct H. + red in H. congruence. + rewrite Pos.leb_le in *. red in H. destruct H as [A | [A B]]. + red in A. zify; omega. + rewrite A; auto. +Qed. + +Remark select_reg_charact: + forall r q, select_reg_l r q = true /\ select_reg_h r q = true <-> ereg q = r. +Proof. + unfold select_reg_l, select_reg_h; intros; split. + rewrite ! Pos.leb_le. unfold reg; zify; omega. + intros. rewrite H. rewrite ! Pos.leb_refl; auto. +Qed. + +Lemma reg_unconstrained_sound: + forall r e q, + reg_unconstrained r e = true -> + EqSet.In q e -> + ereg q <> r. +Proof. + unfold reg_unconstrained; intros. red; intros. + apply select_reg_charact in H1. + assert (EqSet.mem_between (select_reg_l r) (select_reg_h r) e = true). + { + apply EqSet.mem_between_2 with q; auto. + exact (select_reg_l_monotone r). + exact (select_reg_h_monotone r). + tauto. + tauto. + } + rewrite H2 in H; discriminate. +Qed. + +Lemma reg_unconstrained_satisf: + forall r e rs ls v, + reg_unconstrained r e = true -> + satisf rs ls e -> + satisf (rs#r <- v) ls e. +Proof. + red; intros. rewrite PMap.gso. auto. eapply reg_unconstrained_sound; eauto. +Qed. + +Remark select_loc_l_monotone: + forall l q1 q2, + OrderedEquation'.eq q1 q2 \/ OrderedEquation'.lt q1 q2 -> + select_loc_l l q1 = true -> select_loc_l l q2 = true. +Proof. + unfold select_loc_l; intros. set (lb := OrderedLoc.diff_low_bound l) in *. + destruct H. + red in H. subst q2; auto. + assert (eloc q1 = eloc q2 \/ OrderedLoc.lt (eloc q1) (eloc q2)). + red in H. tauto. + destruct H1. rewrite <- H1; auto. + destruct (OrderedLoc.compare (eloc q2) lb); auto. + assert (OrderedLoc.lt (eloc q1) lb) by (eapply OrderedLoc.lt_trans; eauto). + destruct (OrderedLoc.compare (eloc q1) lb). + auto. + eelim OrderedLoc.lt_not_eq; eauto. + eelim OrderedLoc.lt_not_eq. eapply OrderedLoc.lt_trans. eexact l1. eexact H2. red; auto. +Qed. + +Remark select_loc_h_monotone: + forall l q1 q2, + OrderedEquation'.eq q1 q2 \/ OrderedEquation'.lt q2 q1 -> + select_loc_h l q1 = true -> select_loc_h l q2 = true. +Proof. + unfold select_loc_h; intros. set (lb := OrderedLoc.diff_high_bound l) in *. + destruct H. + red in H. subst q2; auto. + assert (eloc q2 = eloc q1 \/ OrderedLoc.lt (eloc q2) (eloc q1)). + red in H. tauto. + destruct H1. rewrite H1; auto. + destruct (OrderedLoc.compare (eloc q2) lb); auto. + assert (OrderedLoc.lt lb (eloc q1)) by (eapply OrderedLoc.lt_trans; eauto). + destruct (OrderedLoc.compare (eloc q1) lb). + eelim OrderedLoc.lt_not_eq. eapply OrderedLoc.lt_trans. eexact l1. eexact H2. red; auto. + eelim OrderedLoc.lt_not_eq. eexact H2. apply OrderedLoc.eq_sym; auto. + auto. +Qed. + +Remark select_loc_charact: + forall l q, + select_loc_l l q = false \/ select_loc_h l q = false <-> Loc.diff l (eloc q). +Proof. + unfold select_loc_l, select_loc_h; intros; split; intros. + apply OrderedLoc.outside_interval_diff. + destruct H. + left. destruct (OrderedLoc.compare (eloc q) (OrderedLoc.diff_low_bound l)); assumption || discriminate. + right. destruct (OrderedLoc.compare (eloc q) (OrderedLoc.diff_high_bound l)); assumption || discriminate. + exploit OrderedLoc.diff_outside_interval. eauto. + intros [A | A]. + left. destruct (OrderedLoc.compare (eloc q) (OrderedLoc.diff_low_bound l)). + auto. + eelim OrderedLoc.lt_not_eq; eauto. + eelim OrderedLoc.lt_not_eq. eapply OrderedLoc.lt_trans; eauto. red; auto. + right. destruct (OrderedLoc.compare (eloc q) (OrderedLoc.diff_high_bound l)). + eelim OrderedLoc.lt_not_eq. eapply OrderedLoc.lt_trans; eauto. red; auto. + eelim OrderedLoc.lt_not_eq; eauto. apply OrderedLoc.eq_sym; auto. + auto. +Qed. + +Lemma loc_unconstrained_sound: + forall l e q, + loc_unconstrained l e = true -> + EqSet.In q e -> + Loc.diff l (eloc q). +Proof. + unfold loc_unconstrained; intros. + destruct (select_loc_l l q) eqn:SL. + destruct (select_loc_h l q) eqn:SH. + assert (EqSet2.mem_between (select_loc_l l) (select_loc_h l) (eqs2 e) = true). + { + apply EqSet2.mem_between_2 with q; auto. + exact (select_loc_l_monotone l). + exact (select_loc_h_monotone l). + apply eqs_same. auto. + } + rewrite H1 in H; discriminate. + apply select_loc_charact; auto. + apply select_loc_charact; auto. +Qed. + +Lemma loc_unconstrained_satisf: + forall rs ls k r mr e v, + let l := R mr in + satisf rs ls (remove_equation (Eq k r l) e) -> + loc_unconstrained (R mr) (remove_equation (Eq k r l) e) = true -> + Val.lessdef (sel_val k rs#r) v -> + satisf rs (Locmap.set l v ls) e. +Proof. + intros; red; intros. + destruct (OrderedEquation.eq_dec q (Eq k r l)). + subst q; simpl. unfold l; rewrite Locmap.gss. auto. + assert (EqSet.In q (remove_equation (Eq k r l) e)). + simpl. ESD.fsetdec. + rewrite Locmap.gso. apply H; auto. eapply loc_unconstrained_sound; eauto. +Qed. + +Lemma reg_loc_unconstrained_sound: + forall r l e q, + reg_loc_unconstrained r l e = true -> + EqSet.In q e -> + ereg q <> r /\ Loc.diff l (eloc q). +Proof. + intros. destruct (andb_prop _ _ H). + split. eapply reg_unconstrained_sound; eauto. eapply loc_unconstrained_sound; eauto. +Qed. + +Lemma parallel_assignment_satisf: + forall k r mr e rs ls v v', + let l := R mr in + Val.lessdef (sel_val k v) v' -> + reg_loc_unconstrained r (R mr) (remove_equation (Eq k r l) e) = true -> + satisf rs ls (remove_equation (Eq k r l) e) -> + satisf (rs#r <- v) (Locmap.set l v' ls) e. +Proof. + intros; red; intros. + destruct (OrderedEquation.eq_dec q (Eq k r l)). + subst q; simpl. unfold l; rewrite Regmap.gss; rewrite Locmap.gss; auto. + assert (EqSet.In q (remove_equation {| ekind := k; ereg := r; eloc := l |} e)). + simpl. ESD.fsetdec. + exploit reg_loc_unconstrained_sound; eauto. intros [A B]. + rewrite Regmap.gso; auto. rewrite Locmap.gso; auto. +Qed. + +Lemma parallel_assignment_satisf_2: + forall rs ls res res' e e' v v', + remove_equations_res res res' e = Some e' -> + satisf rs ls e' -> + reg_unconstrained res e' = true -> + forallb (fun l => loc_unconstrained l e') (map R (regs_of_rpair res')) = true -> + Val.lessdef v v' -> + satisf (rs#res <- v) (Locmap.setpair res' v' ls) e. +Proof. + intros. functional inversion H. +- (* One location *) + subst. simpl in H2. InvBooleans. simpl. + apply parallel_assignment_satisf with Full; auto. + unfold reg_loc_unconstrained. rewrite H1, H4. auto. +- (* Two 32-bit halves *) + subst. + set (e' := remove_equation {| ekind := Low; ereg := res; eloc := R mr2 |} + (remove_equation {| ekind := High; ereg := res; eloc := R mr1 |} e)) in *. + simpl in H2. InvBooleans. simpl. + red; intros. + destruct (OrderedEquation.eq_dec q (Eq Low res (R mr2))). + subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gss. + 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. + apply Val.hiword_lessdef; auto. + assert (EqSet.In q e'). unfold e', remove_equation; simpl; ESD.fsetdec. + rewrite Regmap.gso. rewrite ! Locmap.gso. auto. + eapply loc_unconstrained_sound; eauto. + eapply loc_unconstrained_sound; eauto. + eapply reg_unconstrained_sound; eauto. +Qed. + +Remark in_elements_between_1: + forall r1 s q, + EqSet.In q (EqSet.elements_between (select_reg_l r1) (select_reg_h r1) s) <-> EqSet.In q s /\ ereg q = r1. +Proof. + intros. rewrite EqSet.elements_between_iff, select_reg_charact. tauto. + exact (select_reg_l_monotone r1). exact (select_reg_h_monotone r1). +Qed. + +Lemma in_subst_reg: + forall r1 r2 q (e: eqs), + EqSet.In q e -> + ereg q = r1 /\ EqSet.In (Eq (ekind q) r2 (eloc q)) (subst_reg r1 r2 e) + \/ ereg q <> r1 /\ EqSet.In q (subst_reg r1 r2 e). +Proof. + intros r1 r2 q e0 IN0. unfold subst_reg. + set (f := fun (q: EqSet.elt) e => add_equation (Eq (ekind q) r2 (eloc q)) (remove_equation q e)). + generalize (in_elements_between_1 r1 e0). + set (elt := EqSet.elements_between (select_reg_l r1) (select_reg_h r1) e0). + intros IN_ELT. + set (P := fun e1 e2 => + EqSet.In q e1 -> + EqSet.In (Eq (ekind q) r2 (eloc q)) e2). + assert (P elt (EqSet.fold f elt e0)). + { + apply ESP.fold_rec; unfold P; intros. + - ESD.fsetdec. + - simpl. red in H1. apply H1 in H3. destruct H3. + + subst x. ESD.fsetdec. + + rewrite ESF.add_iff. rewrite ESF.remove_iff. + destruct (OrderedEquation.eq_dec x {| ekind := ekind q; ereg := r2; eloc := eloc q |}); auto. + left. subst x; auto. + } + set (Q := fun e1 e2 => + ~EqSet.In q e1 -> + EqSet.In q e2). + assert (Q elt (EqSet.fold f elt e0)). + { + apply ESP.fold_rec; unfold Q; intros. + - auto. + - 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. + right. split. red; intros. elim n. rewrite IN_ELT. auto. apply H0. auto. +Qed. + +Lemma subst_reg_satisf: + forall src dst rs ls e, + satisf rs ls (subst_reg dst src e) -> + satisf (rs#dst <- (rs#src)) ls e. +Proof. + intros; red; intros. + destruct (in_subst_reg dst src q e H0) as [[A B] | [A B]]. + subst dst. rewrite Regmap.gss. exploit H; eauto. + rewrite Regmap.gso; auto. +Qed. + +Lemma in_subst_reg_kind: + forall r1 k1 r2 k2 q (e: eqs), + EqSet.In q e -> + (ereg q, ekind q) = (r1, k1) /\ EqSet.In (Eq k2 r2 (eloc q)) (subst_reg_kind r1 k1 r2 k2 e) + \/ EqSet.In q (subst_reg_kind r1 k1 r2 k2 e). +Proof. + intros r1 k1 r2 k2 q e0 IN0. unfold subst_reg. + set (f := fun (q: EqSet.elt) e => + if IndexedEqKind.eq (ekind q) k1 + then add_equation (Eq k2 r2 (eloc q)) (remove_equation q e) + else e). + generalize (in_elements_between_1 r1 e0). + set (elt := EqSet.elements_between (select_reg_l r1) (select_reg_h r1) e0). + intros IN_ELT. + set (P := fun e1 e2 => + EqSet.In q e1 -> ekind q = k1 -> + EqSet.In (Eq k2 r2 (eloc q)) e2). + assert (P elt (EqSet.fold f elt e0)). + { + intros; apply ESP.fold_rec; unfold P; intros. + - ESD.fsetdec. + - simpl. red in H1. apply H1 in H3. destruct H3. + + subst x. unfold f. destruct (IndexedEqKind.eq (ekind q) k1). + simpl. ESD.fsetdec. contradiction. + + unfold f. destruct (IndexedEqKind.eq (ekind x) k1). + simpl. rewrite ESF.add_iff. rewrite ESF.remove_iff. + destruct (OrderedEquation.eq_dec x {| ekind := k2; ereg := r2; eloc := eloc q |}); auto. + left. subst x; auto. + auto. + } + set (Q := fun e1 e2 => + ~EqSet.In q e1 \/ ekind q <> k1 -> + EqSet.In q e2). + assert (Q elt (EqSet.fold f elt e0)). + { + apply ESP.fold_rec; unfold Q; intros. + - auto. + - unfold f. red in H2. rewrite H2 in H4. + destruct (IndexedEqKind.eq (ekind x) k1). + simpl. rewrite ESF.add_iff. rewrite ESF.remove_iff. + right. split. apply H3. tauto. intuition congruence. + apply H3. intuition auto. + } + destruct (ESP.In_dec q elt). + destruct (IndexedEqKind.eq (ekind q) k1). + left. split. f_equal. apply IN_ELT. auto. auto. apply H. auto. auto. + right. apply H0. auto. + right. apply H0. auto. +Qed. + +Lemma subst_reg_kind_satisf_makelong: + forall src1 src2 dst rs ls e, + let e1 := subst_reg_kind dst High src1 Full e in + let e2 := subst_reg_kind dst Low src2 Full e1 in + reg_unconstrained dst e2 = true -> + satisf rs ls e2 -> + satisf (rs#dst <- (Val.longofwords rs#src1 rs#src2)) ls e. +Proof. + intros; red; intros. + destruct (in_subst_reg_kind dst High src1 Full q e H1) as [[A B] | B]; fold e1 in B. + destruct (in_subst_reg_kind dst Low src2 Full _ e1 B) as [[C D] | D]; fold e2 in D. + simpl in C; simpl in D. inv C. + inversion A. rewrite H3; rewrite H4. rewrite Regmap.gss. + apply Val.lessdef_trans with (rs#src1). + simpl. destruct (rs#src1); simpl; auto. destruct (rs#src2); simpl; auto. + rewrite Int64.hi_ofwords. auto. + exploit H0. eexact D. simpl. auto. + destruct (in_subst_reg_kind dst Low src2 Full q e1 B) as [[C D] | D]; fold e2 in D. + inversion C. rewrite H3; rewrite H4. rewrite Regmap.gss. + apply Val.lessdef_trans with (rs#src2). + simpl. destruct (rs#src1); simpl; auto. destruct (rs#src2); simpl; auto. + rewrite Int64.lo_ofwords. auto. + exploit H0. eexact D. simpl. auto. + rewrite Regmap.gso. apply H0; auto. eapply reg_unconstrained_sound; eauto. +Qed. + +Lemma subst_reg_kind_satisf_lowlong: + forall src dst rs ls e, + let e1 := subst_reg_kind dst Full src Low e in + reg_unconstrained dst e1 = true -> + satisf rs ls e1 -> + satisf (rs#dst <- (Val.loword rs#src)) ls e. +Proof. + intros; red; intros. + destruct (in_subst_reg_kind dst Full src Low q e H1) as [[A B] | B]; fold e1 in B. + inversion A. rewrite H3; rewrite H4. simpl. rewrite Regmap.gss. + exploit H0. eexact B. simpl. auto. + rewrite Regmap.gso. apply H0; auto. eapply reg_unconstrained_sound; eauto. +Qed. + +Lemma subst_reg_kind_satisf_highlong: + forall src dst rs ls e, + let e1 := subst_reg_kind dst Full src High e in + reg_unconstrained dst e1 = true -> + satisf rs ls e1 -> + satisf (rs#dst <- (Val.hiword rs#src)) ls e. +Proof. + intros; red; intros. + destruct (in_subst_reg_kind dst Full src High q e H1) as [[A B] | B]; fold e1 in B. + inversion A. rewrite H3; rewrite H4. simpl. rewrite Regmap.gss. + exploit H0. eexact B. simpl. auto. + rewrite Regmap.gso. apply H0; auto. eapply reg_unconstrained_sound; eauto. +Qed. + +Module ESF2 := FSetFacts.Facts(EqSet2). +Module ESP2 := FSetProperties.Properties(EqSet2). +Module ESD2 := FSetDecide.Decide(EqSet2). + +Lemma partial_fold_ind: + forall (A: Type) (P: EqSet2.t -> A -> Prop) f init final s, + EqSet2.fold + (fun q opte => + match opte with + | None => None + | Some e => f q e + end) + s (Some init) = Some final -> + (forall s', EqSet2.Empty s' -> P s' init) -> + (forall x a' a'' s' s'', + EqSet2.In x s -> ~EqSet2.In x s' -> ESP2.Add x s' s'' -> + f x a' = Some a'' -> P s' a' -> P s'' a'') -> + P s final. +Proof. + 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)). + rewrite <- H. apply ESP2.fold_rec; unfold Q, g; intros. + - auto. + - destruct a as [e|]; auto. destruct (f x e) as [e'|] eqn:F; auto. eapply H1; eauto. +Qed. + +Lemma in_subst_loc: + forall l1 l2 q (e e': eqs), + EqSet.In q e -> + subst_loc l1 l2 e = Some e' -> + (eloc q = l1 /\ EqSet.In (Eq (ekind q) (ereg q) l2) e') \/ (Loc.diff l1 (eloc q) /\ EqSet.In q e'). +Proof. + unfold subst_loc; intros l1 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 + Some (add_equation + {| ekind := ekind q0; ereg := ereg q0; eloc := l2 |} + (remove_equation q0 e)) + else None). + set (P := fun e1 e2 => EqSet2.In q e1 -> eloc q = l1 /\ EqSet.In (Eq (ekind q) (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)); inversion H2; subst a''; clear H2. + 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. + destruct (OrderedEquation.eq_dec x {| ekind := ekind q; 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)); 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 loc_type_compat_charact: + forall env l e q, + loc_type_compat env l e = true -> + EqSet.In q e -> + subtype (sel_type (ekind q) (env (ereg q))) (Loc.type l) = true \/ Loc.diff l (eloc q). +Proof. + unfold loc_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 well_typed_move_charact: + forall env l e k r rs, + well_typed_move env l e = true -> + EqSet.In (Eq k r l) e -> + wt_regset env rs -> + match l with + | R mr => True + | S sl ofs ty => Val.has_type (sel_val k rs#r) ty + end. +Proof. + unfold well_typed_move; intros. + destruct l as [mr | sl ofs ty]. + auto. + exploit loc_type_compat_charact; eauto. intros [A | A]. + simpl in A. eapply Val.has_subtype; eauto. + generalize (H1 r). destruct k; simpl; intros. + auto. + destruct (rs#r); exact I. + destruct (rs#r); exact I. + eelim Loc.diff_not_eq. eexact A. auto. +Qed. + +Remark val_lessdef_normalize: + forall v v' ty, + Val.has_type v ty -> Val.lessdef v v' -> + Val.lessdef v (Val.load_result (chunk_of_type ty) v'). +Proof. + intros. inv H0. rewrite Val.load_result_same; auto. auto. +Qed. + +Lemma subst_loc_satisf: + forall env src dst rs ls e e', + subst_loc dst src e = Some e' -> + well_typed_move env dst e = true -> + wt_regset env rs -> + satisf rs ls e' -> + satisf rs (Locmap.set dst (ls src) ls) e. +Proof. + intros; red; intros. + exploit in_subst_loc; eauto. intros [[A B] | [A B]]. + subst dst. rewrite Locmap.gss. + destruct q as [k r l]; simpl in *. + exploit well_typed_move_charact; eauto. + destruct l as [mr | sl ofs ty]; intros. + apply (H2 _ B). + apply val_lessdef_normalize; auto. apply (H2 _ B). + 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). +Proof. + induction ml; simpl; intros. + tauto. + InvBooleans. split. + apply Loc.diff_sym. eapply loc_unconstrained_sound; eauto. + eauto. +Qed. + +Lemma undef_regs_outside: + forall ml ls l, + Loc.notin l (map R ml) -> undef_regs ml ls l = ls l. +Proof. + induction ml; simpl; intros. auto. + rewrite Locmap.gso. apply IHml. tauto. apply Loc.diff_sym. tauto. +Qed. + +Lemma can_undef_satisf: + forall ml e rs ls, + can_undef ml e = true -> + satisf rs ls e -> + satisf rs (undef_regs ml ls) e. +Proof. + intros; red; intros. rewrite undef_regs_outside. eauto. + eapply can_undef_sound; eauto. +Qed. + +Lemma can_undef_except_sound: + forall lx e ml q, + can_undef_except lx ml e = true -> EqSet.In q e -> Loc.diff (eloc q) lx -> Loc.notin (eloc q) (map R ml). +Proof. + induction ml; simpl; intros. + tauto. + InvBooleans. split. + destruct (orb_true_elim _ _ H2). + apply proj_sumbool_true in e0. congruence. + apply Loc.diff_sym. eapply loc_unconstrained_sound; eauto. + eapply IHml; eauto. +Qed. + +Lemma subst_loc_undef_satisf: + forall env src dst rs ls ml e e', + subst_loc dst src e = Some e' -> + well_typed_move env dst e = true -> + can_undef_except dst ml e = true -> + wt_regset env rs -> + satisf rs ls e' -> + satisf rs (Locmap.set dst (ls src) (undef_regs ml ls)) e. +Proof. + intros; red; intros. + exploit in_subst_loc; eauto. intros [[A B] | [A B]]. + subst dst. rewrite Locmap.gss. + destruct q as [k r l]; simpl in *. + exploit well_typed_move_charact; eauto. + destruct l as [mr | sl ofs ty]; intros. + apply (H3 _ B). + apply val_lessdef_normalize; auto. apply (H3 _ B). + rewrite Locmap.gso; auto. rewrite undef_regs_outside. eauto. + eapply can_undef_except_sound; eauto. apply Loc.diff_sym; auto. +Qed. + +Lemma transfer_use_def_satisf: + forall args res args' res' und e e' rs ls, + transfer_use_def args res args' res' und e = Some e' -> + satisf rs ls e' -> + Val.lessdef_list rs##args (reglist ls args') /\ + (forall v v', Val.lessdef v v' -> + satisf (rs#res <- v) (Locmap.set (R res') v' (undef_regs und ls)) e). +Proof. + unfold transfer_use_def; intros. MonadInv. + split. eapply add_equations_lessdef; eauto. + intros. eapply parallel_assignment_satisf; eauto. assumption. + eapply can_undef_satisf; eauto. + eapply add_equations_satisf; eauto. +Qed. + +Lemma add_equations_res_lessdef: + forall r ty l e e' rs ls, + add_equations_res r ty l e = Some e' -> + satisf rs ls e' -> + Val.has_type rs#r ty -> + Val.lessdef rs#r (Locmap.getpair (map_rpair R l) ls). +Proof. + intros. functional inversion H; simpl. +- subst. eapply add_equation_lessdef with (q := Eq Full r (R mr)); eauto. +- 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. + eapply add_equation_lessdef with (q := Eq Low r (R mr2)). + eauto. +Qed. + +Lemma return_regs_agree_callee_save: + forall caller callee, + agree_callee_save caller (return_regs caller callee). +Proof. + intros; red; intros. unfold return_regs. red in H. + destruct l. + rewrite H; auto. + destruct sl; auto || congruence. +Qed. + +Lemma no_caller_saves_sound: + forall e q, + no_caller_saves e = true -> + EqSet.In q e -> + callee_save_loc (eloc q). +Proof. + unfold no_caller_saves, callee_save_loc; intros. + exploit EqSet.for_all_2; eauto. + hnf. intros. simpl in H1. rewrite H1. auto. + lazy beta. destruct (eloc q). auto. destruct sl; congruence. +Qed. + +Lemma val_hiword_longofwords: + forall v1 v2, Val.lessdef (Val.hiword (Val.longofwords v1 v2)) v1. +Proof. + intros. destruct v1; simpl; auto. destruct v2; auto. unfold Val.hiword. + rewrite Int64.hi_ofwords. auto. +Qed. + +Lemma val_loword_longofwords: + forall v1 v2, Val.lessdef (Val.loword (Val.longofwords v1 v2)) v2. +Proof. + intros. destruct v1; simpl; auto. destruct v2; auto. unfold Val.loword. + rewrite Int64.lo_ofwords. auto. +Qed. + +Lemma function_return_satisf: + forall rs ls_before ls_after res res' sg e e' v, + res' = loc_result sg -> + remove_equations_res res res' e = Some e' -> + satisf rs ls_before e' -> + forallb (fun l => reg_loc_unconstrained res l e') (map R (regs_of_rpair res')) = true -> + no_caller_saves e' = true -> + Val.lessdef v (Locmap.getpair (map_rpair R res') ls_after) -> + agree_callee_save ls_before ls_after -> + satisf (rs#res <- v) ls_after e. +Proof. + intros; red; intros. + functional inversion H0. +- (* One register *) + subst. rewrite <- H8 in *. simpl in *. InvBooleans. + set (e' := remove_equation {| ekind := Full; ereg := res; eloc := R mr |} e) in *. + destruct (OrderedEquation.eq_dec q (Eq Full res (R mr))). + subst q; simpl. rewrite Regmap.gss; auto. + assert (EqSet.In q e'). unfold e', remove_equation; simpl. ESD.fsetdec. + exploit reg_loc_unconstrained_sound; eauto. intros [A B]. + rewrite Regmap.gso; auto. + exploit no_caller_saves_sound; eauto. intros. + red in H5. rewrite <- H5; auto. +- (* Two 32-bit halves *) + 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. + destruct (OrderedEquation.eq_dec q (Eq Low res (R mr2))). + subst q; simpl. rewrite Regmap.gss. + eapply Val.lessdef_trans. apply Val.loword_lessdef. eauto. apply val_loword_longofwords. + destruct (OrderedEquation.eq_dec q (Eq High res (R mr1))). + subst q; simpl. rewrite Regmap.gss. + eapply Val.lessdef_trans. apply Val.hiword_lessdef. eauto. apply val_hiword_longofwords. + assert (EqSet.In q e'). unfold e', remove_equation; simpl; ESD.fsetdec. + exploit reg_loc_unconstrained_sound. eexact H. eauto. intros [A B]. + exploit reg_loc_unconstrained_sound. eexact H2. eauto. intros [C D]. + rewrite Regmap.gso; auto. + exploit no_caller_saves_sound; eauto. intros. + red in H5. rewrite <- H5; auto. +Qed. + +Lemma compat_left_sound: + forall r l e q, + compat_left r l e = true -> EqSet.In q e -> ereg q = r -> ekind q = Full /\ eloc q = l. +Proof. + unfold compat_left; intros. + rewrite EqSet.for_all_between_iff in H. + apply select_reg_charact in H1. destruct H1. + exploit H; eauto. intros. + destruct (ekind q); try discriminate. + destruct (Loc.eq l (eloc q)); try discriminate. + auto. + intros. subst x2. auto. + exact (select_reg_l_monotone r). + exact (select_reg_h_monotone r). +Qed. + +Lemma compat_left2_sound: + forall r l1 l2 e q, + compat_left2 r l1 l2 e = true -> EqSet.In q e -> ereg q = r -> + (ekind q = High /\ eloc q = l1) \/ (ekind q = Low /\ eloc q = l2). +Proof. + unfold compat_left2; intros. + rewrite EqSet.for_all_between_iff in H. + apply select_reg_charact in H1. destruct H1. + exploit H; eauto. intros. + destruct (ekind q); try discriminate. + InvBooleans. auto. + InvBooleans. auto. + intros. subst x2. auto. + exact (select_reg_l_monotone r). + exact (select_reg_h_monotone r). +Qed. + +Lemma compat_entry_satisf: + forall rl ll e, + compat_entry rl ll e = true -> + forall vl ls, + Val.lessdef_list vl (map (fun p => Locmap.getpair p ls) ll) -> + satisf (init_regs vl rl) ls e. +Proof. + intros until e. functional induction (compat_entry rl ll e); intros. +- (* no params *) + simpl. red; intros. rewrite Regmap.gi. destruct (ekind q); simpl; auto. +- (* a param in a single location *) + InvBooleans. simpl in H0. inv H0. simpl. + red; intros. rewrite Regmap.gsspec. destruct (peq (ereg q) r1). + exploit compat_left_sound; eauto. intros [A B]. rewrite A; rewrite B; auto. + eapply IHb; eauto. +- (* a param split across two locations *) + InvBooleans. simpl in H0. inv H0. simpl. + red; intros. rewrite Regmap.gsspec. destruct (peq (ereg q) r1). + exploit compat_left2_sound; eauto. + intros [[A B] | [A B]]; rewrite A; rewrite B; simpl. + apply Val.lessdef_trans with (Val.hiword (Val.longofwords (ls l1) (ls l2))). + apply Val.hiword_lessdef; auto. apply val_hiword_longofwords. + apply Val.lessdef_trans with (Val.loword (Val.longofwords (ls l1) (ls l2))). + apply Val.loword_lessdef; auto. apply val_loword_longofwords. + eapply IHb; eauto. +- (* error case *) + discriminate. +Qed. + +Lemma call_regs_param_values: + forall sg ls, + map (fun p => Locmap.getpair p (call_regs ls)) (loc_parameters sg) + = map (fun p => Locmap.getpair p ls) (loc_arguments sg). +Proof. + intros. unfold loc_parameters. rewrite list_map_compose. + apply list_map_exten; intros. symmetry. + assert (A: forall l, loc_argument_acceptable l -> call_regs ls (parameter_of_argument l) = ls l). + { destruct l as [r | [] ofs ty]; simpl; auto; contradiction. } + exploit loc_arguments_acceptable; eauto. destruct x; simpl; intros. +- auto. +- destruct H0; f_equal; auto. +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 ls2) (loc_arguments sg). +Proof. + intros. + apply tailcall_is_possible_correct in H. + 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. + destruct l; simpl; intros; try contradiction. rewrite H4; auto. +Qed. + +Lemma find_function_tailcall: + forall tge ros ls1 ls2, + ros_compatible_tailcall ros = true -> + find_function tge ros (return_regs ls1 ls2) = find_function tge ros ls2. +Proof. + unfold ros_compatible_tailcall, find_function; intros. + destruct ros as [r|id]; auto. + unfold return_regs. destruct (is_callee_save r). discriminate. auto. +Qed. + +Lemma loadv_int64_split: + forall m a v, + Mem.loadv Mint64 m a = Some v -> Archi.splitlong = true -> + exists v1 v2, + Mem.loadv Mint32 m a = Some (if Archi.big_endian then v1 else v2) + /\ Mem.loadv Mint32 m (Val.add a (Vint (Int.repr 4))) = Some (if Archi.big_endian then v2 else v1) + /\ Val.lessdef (Val.hiword v) v1 + /\ Val.lessdef (Val.loword v) v2. +Proof. + 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. + rewrite Int64.hi_ofwords, Int64.lo_ofwords; auto. +Qed. + +Lemma add_equations_builtin_arg_satisf: + forall env rs ls arg arg' e e', + add_equations_builtin_arg env arg arg' e = Some e' -> + satisf rs ls e' -> satisf rs ls e. +Proof. + induction arg; destruct arg'; simpl; intros; MonadInv; eauto. + eapply add_equation_satisf; eauto. + destruct arg'1; MonadInv. destruct arg'2; MonadInv. eauto using add_equation_satisf. +Qed. + +Lemma add_equations_builtin_arg_lessdef: + forall env (ge: RTL.genv) sp rs ls m arg v, + eval_builtin_arg ge (fun r => rs#r) sp m arg v -> + forall e e' arg', + add_equations_builtin_arg env arg arg' e = Some e' -> + satisf rs ls e' -> + wt_regset env rs -> + exists v', eval_builtin_arg ge ls sp m arg' v' /\ Val.lessdef v v'. +Proof. + induction 1; simpl; intros e e' arg' AE SAT WT; destruct arg'; MonadInv. +- exploit add_equation_lessdef; eauto. simpl; intros. + exists (ls x0); auto with barg. +- destruct arg'1; MonadInv. destruct arg'2; MonadInv. + 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_2 rs#x); auto. apply Val.longofwords_lessdef; auto. + rewrite <- e0; apply WT. +- econstructor; eauto with barg. +- econstructor; eauto with barg. +- econstructor; eauto with barg. +- econstructor; eauto with barg. +- econstructor; eauto with barg. +- econstructor; eauto with barg. +- econstructor; eauto with barg. +- econstructor; eauto with barg. +- exploit IHeval_builtin_arg1; eauto. eapply add_equations_builtin_arg_satisf; eauto. + intros (v1 & A & B). + exploit IHeval_builtin_arg2; eauto. intros (v2 & C & D). + exists (Val.longofwords v1 v2); split; auto with barg. apply Val.longofwords_lessdef; auto. +- exploit IHeval_builtin_arg1; eauto. eapply add_equations_builtin_arg_satisf; eauto. + intros (v1' & A & B). + exploit IHeval_builtin_arg2; eauto. intros (v2' & C & D). + econstructor; split. eauto with barg. + destruct Archi.ptr64; auto using Val.add_lessdef, Val.addl_lessdef. +Qed. + +Lemma add_equations_builtin_args_satisf: + forall env rs ls arg arg' e e', + add_equations_builtin_args env arg arg' e = Some e' -> + satisf rs ls e' -> satisf rs ls e. +Proof. + induction arg; destruct arg'; simpl; intros; MonadInv; eauto using add_equations_builtin_arg_satisf. +Qed. + +Lemma add_equations_builtin_args_lessdef: + forall env (ge: RTL.genv) sp rs ls m tm arg vl, + eval_builtin_args ge (fun r => rs#r) sp m arg vl -> + forall arg' e e', + add_equations_builtin_args env arg arg' e = Some e' -> + satisf rs ls e' -> + wt_regset env rs -> + Mem.extends m tm -> + exists vl', eval_builtin_args ge ls sp tm arg' vl' /\ Val.lessdef_list vl vl'. +Proof. + induction 1; simpl; intros; destruct arg'; MonadInv. +- exists (@nil val); split; constructor. +- exploit IHlist_forall2; eauto. intros (vl' & A & B). + exploit add_equations_builtin_arg_lessdef; eauto. + eapply add_equations_builtin_args_satisf; eauto. intros (v1' & C & D). + exploit (@eval_builtin_arg_lessdef _ ge ls ls); eauto. intros (v1'' & E & F). + exists (v1'' :: vl'); split; constructor; auto. eapply Val.lessdef_trans; eauto. +Qed. + +Lemma add_equations_debug_args_satisf: + forall env rs ls arg arg' e e', + add_equations_debug_args env arg arg' e = Some e' -> + satisf rs ls e' -> satisf rs ls e. +Proof. + induction arg; destruct arg'; simpl; intros; MonadInv; auto. + destruct (add_equations_builtin_arg env a b e) as [e1|] eqn:A; + eauto using add_equations_builtin_arg_satisf. +Qed. + +Lemma add_equations_debug_args_eval: + forall env (ge: RTL.genv) sp rs ls m tm arg vl, + eval_builtin_args ge (fun r => rs#r) sp m arg vl -> + forall arg' e e', + add_equations_debug_args env arg arg' e = Some e' -> + satisf rs ls e' -> + wt_regset env rs -> + Mem.extends m tm -> + exists vl', eval_builtin_args ge ls sp tm arg' vl'. +Proof. + induction 1; simpl; intros; destruct arg'; MonadInv. +- exists (@nil val); constructor. +- exists (@nil val); constructor. +- destruct (add_equations_builtin_arg env a1 b e) as [e1|] eqn:A. ++ exploit IHlist_forall2; eauto. intros (vl' & B). + exploit add_equations_builtin_arg_lessdef; eauto. + eapply add_equations_debug_args_satisf; eauto. intros (v1' & C & D). + exploit (@eval_builtin_arg_lessdef _ ge ls ls); eauto. intros (v1'' & E & F). + exists (v1'' :: vl'); constructor; auto. ++ eauto. +Qed. + +Lemma add_equations_builtin_eval: + forall ef env args args' e1 e2 m1 m1' rs ls (ge: RTL.genv) sp vargs t vres m2, + wt_regset env rs -> + match ef with + | EF_debug _ _ _ => add_equations_debug_args env args args' e1 + | _ => add_equations_builtin_args env args args' e1 + end = Some e2 -> + Mem.extends m1 m1' -> + satisf rs ls e2 -> + eval_builtin_args ge (fun r => rs # r) sp m1 args vargs -> + external_call ef ge vargs m1 t vres m2 -> + satisf rs ls e1 /\ + exists vargs' vres' m2', + eval_builtin_args ge ls sp m1' args' vargs' + /\ external_call ef ge vargs' m1' t vres' m2' + /\ Val.lessdef vres vres' + /\ Mem.extends m2 m2'. +Proof. + intros. + assert (DEFAULT: add_equations_builtin_args env args args' e1 = Some e2 -> + satisf rs ls e1 /\ + exists vargs' vres' m2', + eval_builtin_args ge ls sp m1' args' vargs' + /\ external_call ef ge vargs' m1' t vres' m2' + /\ Val.lessdef vres vres' + /\ Mem.extends m2 m2'). + { + intros. split. eapply add_equations_builtin_args_satisf; eauto. + exploit add_equations_builtin_args_lessdef; eauto. + intros (vargs' & A & B). + exploit external_call_mem_extends; eauto. + intros (vres' & m2' & C & D & E & F). + exists vargs', vres', m2'; auto. + } + destruct ef; auto. + split. eapply add_equations_debug_args_satisf; eauto. + exploit add_equations_debug_args_eval; eauto. + intros (vargs' & A). + simpl in H4; inv H4. + exists vargs', Vundef, m1'. intuition auto. simpl. constructor. +Qed. + +Lemma parallel_set_builtin_res_satisf: + forall env res res' e0 e1 rs ls v v', + remove_equations_builtin_res env res res' e0 = Some e1 -> + forallb (fun r => reg_unconstrained r e1) (params_of_builtin_res res) = true -> + forallb (fun mr => loc_unconstrained (R mr) e1) (params_of_builtin_res res') = true -> + satisf rs ls e1 -> + Val.lessdef v v' -> + satisf (regmap_setres res v rs) (Locmap.setres res' v' ls) e0. +Proof. + intros. rewrite forallb_forall in *. + destruct res, res'; simpl in *; inv H. +- apply parallel_assignment_satisf with (k := Full); auto. + unfold reg_loc_unconstrained. rewrite H0 by auto. rewrite H1 by auto. auto. +- destruct res'1; try discriminate. destruct res'2; try discriminate. + rename x0 into hi; rename x1 into lo. MonadInv. destruct (mreg_eq hi lo); inv H5. + set (e' := remove_equation {| ekind := High; ereg := x; eloc := R hi |} e0) in *. + set (e'' := remove_equation {| ekind := Low; ereg := x; eloc := R lo |} e') in *. + simpl in *. red; intros. + destruct (OrderedEquation.eq_dec q (Eq Low x (R lo))). + subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gss. apply Val.loword_lessdef; auto. + destruct (OrderedEquation.eq_dec q (Eq High x (R hi))). + subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gso by (red; auto). + rewrite Locmap.gss. apply Val.hiword_lessdef; auto. + assert (EqSet.In q e''). + { unfold e'', e', remove_equation; simpl; ESD.fsetdec. } + rewrite Regmap.gso. rewrite ! Locmap.gso. auto. + eapply loc_unconstrained_sound; eauto. + eapply loc_unconstrained_sound; eauto. + eapply reg_unconstrained_sound; eauto. +- auto. +Qed. + +(** * Properties of the dataflow analysis *) + +Lemma analyze_successors: + forall f env bsh an pc bs s e, + analyze f env bsh = Some an -> + bsh!pc = Some bs -> + In s (successors_block_shape bs) -> + an!!pc = OK e -> + exists e', transfer f env bsh s an!!s = OK e' /\ EqSet.Subset e' e. +Proof. + unfold analyze; intros. exploit DS.fixpoint_allnodes_solution; eauto. + rewrite H2. unfold DS.L.ge. destruct (transfer f env bsh s an#s); intros. + exists e0; auto. + contradiction. +Qed. + +Lemma satisf_successors: + forall f env bsh an pc bs s e rs ls, + analyze f env bsh = Some an -> + bsh!pc = Some bs -> + In s (successors_block_shape bs) -> + an!!pc = OK e -> + satisf rs ls e -> + exists e', transfer f env bsh s an!!s = OK e' /\ satisf rs ls e'. +Proof. + intros. exploit analyze_successors; eauto. intros [e' [A B]]. + exists e'; split; auto. eapply satisf_incr; eauto. +Qed. + +(** Inversion on [transf_function] *) + +Inductive transf_function_spec (f: RTL.function) (tf: LTL.function) : Prop := + | transf_function_spec_intro: + forall env an mv k e1 e2, + wt_function f env -> + analyze f env (pair_codes f tf) = Some an -> + (LTL.fn_code tf)!(LTL.fn_entrypoint tf) = Some(expand_moves mv (Lbranch (RTL.fn_entrypoint f) :: k)) -> + wf_moves mv -> + transfer f env (pair_codes f tf) (RTL.fn_entrypoint f) an!!(RTL.fn_entrypoint f) = OK e1 -> + track_moves env mv e1 = Some e2 -> + compat_entry (RTL.fn_params f) (loc_parameters (fn_sig tf)) e2 = true -> + can_undef destroyed_at_function_entry e2 = true -> + RTL.fn_stacksize f = LTL.fn_stacksize tf -> + RTL.fn_sig f = LTL.fn_sig tf -> + transf_function_spec f tf. + +Lemma transf_function_inv: + forall f tf, + transf_function f = OK tf -> + transf_function_spec f tf. +Proof. + unfold transf_function; intros. + destruct (type_function f) as [env|] eqn:TY; try discriminate. + destruct (regalloc f); try discriminate. + destruct (check_function f f0 env) as [] eqn:?; inv H. + unfold check_function in Heqr. + destruct (analyze f env (pair_codes f tf)) as [an|] eqn:?; try discriminate. + monadInv Heqr. + destruct (check_entrypoints_aux f tf env x) as [y|] eqn:?; try discriminate. + unfold check_entrypoints_aux, pair_entrypoints in Heqo0. MonadInv. + 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. + +Lemma invert_code: + forall f env tf pc i opte e, + wt_function f env -> + (RTL.fn_code f)!pc = Some i -> + transfer f env (pair_codes f tf) pc opte = OK e -> + exists eafter, exists bsh, exists bb, + opte = OK eafter /\ + (pair_codes f tf)!pc = Some bsh /\ + (LTL.fn_code tf)!pc = Some bb /\ + expand_block_shape bsh i bb /\ + transfer_aux f env bsh eafter = Some e /\ + wt_instr f env i. +Proof. + intros. destruct opte as [eafter|]; simpl in H1; try discriminate. exists eafter. + destruct (pair_codes f tf)!pc as [bsh|] eqn:?; try discriminate. exists bsh. + exploit matching_instr_block; eauto. intros [bb [A B]]. + destruct (transfer_aux f env bsh eafter) as [e1|] eqn:?; inv H1. + exists bb. exploit wt_instr_at; eauto. + tauto. +Qed. + +(** * Semantic preservation *) + +Section PRESERVATION. + +Variable prog: RTL.program. +Variable tprog: LTL.program. +Hypothesis TRANSF: match_prog prog tprog. + +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +Lemma symbols_preserved: + forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. +Proof (Genv.find_symbol_match TRANSF). + +Lemma senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_match TRANSF). + +Lemma functions_translated: + forall (v: val) (f: RTL.fundef), + Genv.find_funct ge v = Some f -> + exists tf, + Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf. +Proof (Genv.find_funct_transf_partial TRANSF). + +Lemma function_ptr_translated: + forall (b: block) (f: RTL.fundef), + Genv.find_funct_ptr ge b = Some f -> + exists tf, + Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf. +Proof (Genv.find_funct_ptr_transf_partial TRANSF). + +Lemma sig_function_translated: + forall f tf, + transf_fundef f = OK tf -> + LTL.funsig tf = RTL.funsig f. +Proof. + intros; destruct f; monadInv H. + destruct (transf_function_inv _ _ EQ). simpl; auto. + auto. +Qed. + +Lemma find_function_translated: + forall ros rs fd ros' e e' ls, + RTL.find_function ge ros rs = Some fd -> + add_equation_ros ros ros' e = Some e' -> + satisf rs ls e' -> + exists tfd, + LTL.find_function tge ros' ls = Some tfd /\ transf_fundef fd = OK tfd. +Proof. + unfold RTL.find_function, LTL.find_function; intros. + destruct ros as [r|id]; destruct ros' as [r'|id']; simpl in H0; MonadInv. + (* two regs *) + exploit add_equation_lessdef; eauto. intros LD. inv LD. + eapply functions_translated; eauto. + rewrite <- H2 in H. simpl in H. congruence. + (* two symbols *) + rewrite symbols_preserved. rewrite Heqo. + eapply function_ptr_translated; eauto. +Qed. + +Lemma exec_moves: + forall mv env rs s f sp bb m e e' ls, + track_moves env mv e = Some e' -> + wf_moves mv -> + satisf rs ls e' -> + wt_regset env rs -> + exists ls', + star step tge (Block s f sp (expand_moves mv bb) ls m) + E0 (Block s f sp bb ls' m) + /\ satisf rs ls' e. +Proof. +Opaque destroyed_by_op. + induction mv; simpl; intros. + (* base *) +- unfold expand_moves; simpl. inv H. exists ls; split. apply star_refl. auto. + (* step *) +- assert (wf_moves mv) by (inv H0; auto). + destruct a; unfold expand_moves; simpl; MonadInv. ++ (* loc-loc move *) + destruct src as [rsrc | ssrc]; destruct dst as [rdst | sdst]. +* (* reg-reg *) + exploit IHmv; eauto. eapply subst_loc_undef_satisf; eauto. + intros [ls' [A B]]. exists ls'; split; auto. eapply star_left; eauto. + econstructor. simpl. eauto. auto. auto. +* (* reg->stack *) + exploit IHmv; eauto. eapply subst_loc_undef_satisf; eauto. + intros [ls' [A B]]. exists ls'; split; auto. eapply star_left; eauto. + econstructor. simpl. eauto. auto. +* (* stack->reg *) + simpl in Heqb. exploit IHmv; eauto. eapply subst_loc_undef_satisf; eauto. + intros [ls' [A B]]. exists ls'; split; auto. eapply star_left; eauto. + 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 *) + +Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> signature -> Prop := + | match_stackframes_nil: forall sg, + sg.(sig_res) = Tint -> + match_stackframes nil nil sg + | match_stackframes_cons: + forall res f sp pc rs s tf bb ls ts sg an e env + (STACKS: match_stackframes s ts (fn_sig tf)) + (FUN: transf_function f = OK tf) + (ANL: analyze f env (pair_codes f tf) = Some an) + (EQ: transfer f env (pair_codes f tf) pc an!!pc = OK e) + (WTF: wt_function f env) + (WTRS: wt_regset env rs) + (WTRES: env res = proj_sig_res sg) + (STEPS: forall v ls1 m, + Val.lessdef v (Locmap.getpair (map_rpair R (loc_result sg)) ls1) -> + Val.has_type v (env res) -> + agree_callee_save ls ls1 -> + exists ls2, + star LTL.step tge (Block ts tf sp bb ls1 m) + E0 (State ts tf sp pc ls2 m) + /\ satisf (rs#res <- v) ls2 e), + match_stackframes + (RTL.Stackframe res f sp pc rs :: s) + (LTL.Stackframe tf sp ls bb :: ts) + sg. + +Inductive match_states: RTL.state -> LTL.state -> Prop := + | match_states_intro: + forall s f sp pc rs m ts tf ls m' an e env + (STACKS: match_stackframes s ts (fn_sig tf)) + (FUN: transf_function f = OK tf) + (ANL: analyze f env (pair_codes f tf) = Some an) + (EQ: transfer f env (pair_codes f tf) pc an!!pc = OK e) + (SAT: satisf rs ls e) + (MEM: Mem.extends m m') + (WTF: wt_function f env) + (WTRS: wt_regset env rs), + match_states (RTL.State s f sp pc rs m) + (LTL.State ts tf sp pc ls m') + | match_states_call: + forall s f args m ts tf ls m' + (STACKS: match_stackframes s ts (funsig tf)) + (FUN: transf_fundef f = OK tf) + (ARGS: Val.lessdef_list args (map (fun p => Locmap.getpair p ls) (loc_arguments (funsig tf)))) + (AG: agree_callee_save (parent_locset ts) ls) + (MEM: Mem.extends m m') + (WTARGS: Val.has_type_list args (sig_args (funsig tf))), + match_states (RTL.Callstate s f args m) + (LTL.Callstate ts tf ls m') + | match_states_return: + forall s res m ts ls m' sg + (STACKS: match_stackframes s ts sg) + (RES: Val.lessdef res (Locmap.getpair (map_rpair R (loc_result sg)) ls)) + (AG: agree_callee_save (parent_locset ts) ls) + (MEM: Mem.extends m m') + (WTRES: Val.has_type res (proj_sig_res sg)), + match_states (RTL.Returnstate s res m) + (LTL.Returnstate ts ls m'). + +Lemma match_stackframes_change_sig: + forall s ts sg sg', + match_stackframes s ts sg -> + sg'.(sig_res) = sg.(sig_res) -> + match_stackframes s ts sg'. +Proof. + intros. inv H. + constructor. congruence. + econstructor; eauto. + unfold proj_sig_res in *. rewrite H0; auto. + intros. rewrite (loc_result_exten sg' sg) in H by auto. eauto. +Qed. + +Ltac UseShape := + match goal with + | [ WT: wt_function _ _, CODE: (RTL.fn_code _)!_ = Some _, EQ: transfer _ _ _ _ _ = OK _ |- _ ] => + destruct (invert_code _ _ _ _ _ _ _ WT CODE EQ) as (eafter & bsh & bb & AFTER & BSH & TCODE & EBS & TR & WTI); + inv EBS; unfold transfer_aux in TR; MonadInv + end. + +Remark addressing_not_long: + forall trap env f addr args dst s r, + wt_instr f env (Iload trap Mint64 addr args dst s) -> Archi.splitlong = true -> + In r args -> r <> dst. +Proof. + intros. inv H. + assert (A: forall ty, In ty (type_of_addressing addr) -> ty = Tptr). + { intros. destruct addr; simpl in H; intuition. } + 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. } + red; intros; subst r. rewrite C in H9; discriminate. +Qed. + +(** The proof of semantic preservation is a simulation argument of the + "plus" kind. *) + +Lemma step_simulation: + forall S1 t S2, RTL.step ge S1 t S2 -> wt_state S1 -> + forall S1', match_states S1 S1' -> + exists S2', plus LTL.step tge S1' t S2' /\ match_states S2 S2'. +Proof. + induction 1; intros WT S1' MS; inv MS; try UseShape. + +(* nop *) +- exploit exec_moves; eauto. intros [ls1 [X Y]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_right. eexact X. econstructor; eauto. + eauto. traceEq. + exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. + econstructor; eauto. + +(* op move *) +- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'. + simpl in H0. inv H0. + exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_right. eexact X. econstructor; eauto. + eauto. traceEq. + exploit satisf_successors; eauto. simpl; eauto. eapply subst_reg_satisf; eauto. + intros [enext [U V]]. + econstructor; eauto. + +(* op makelong *) +- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'. + simpl in H0. inv H0. + exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_right. eexact X. econstructor; eauto. + eauto. traceEq. + exploit satisf_successors; eauto. simpl; eauto. + eapply subst_reg_kind_satisf_makelong. eauto. eauto. + intros [enext [U V]]. + econstructor; eauto. + +(* op lowlong *) +- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'. + simpl in H0. inv H0. + exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_right. eexact X. econstructor; eauto. + eauto. traceEq. + exploit satisf_successors; eauto. simpl; eauto. + eapply subst_reg_kind_satisf_lowlong. eauto. eauto. + intros [enext [U V]]. + econstructor; eauto. + +(* op highlong *) +- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'. + simpl in H0. inv H0. + exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_right. eexact X. econstructor; eauto. + eauto. traceEq. + exploit satisf_successors; eauto. simpl; eauto. + eapply subst_reg_kind_satisf_highlong. eauto. eauto. + intros [enext [U V]]. + econstructor; eauto. + +(* op regular *) +- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'. + exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. + exploit transfer_use_def_satisf; eauto. intros [X Y]. + exploit eval_operation_lessdef; eauto. intros [v' [F G]]. + exploit (exec_moves mv2); eauto. intros [ls2 [A2 B2]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_trans. eexact A1. + eapply star_left. econstructor. instantiate (1 := v'). rewrite <- F. + apply eval_operation_preserved. exact symbols_preserved. + eauto. eapply star_right. eexact A2. constructor. + eauto. eauto. eauto. traceEq. + exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. + econstructor; eauto. + +(* op dead *) +- exploit exec_moves; eauto. intros [ls1 [X Y]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_right. eexact X. econstructor; eauto. + eauto. traceEq. + exploit satisf_successors. eauto. eauto. simpl; eauto. eauto. + eapply reg_unconstrained_satisf; eauto. + intros [enext [U V]]. + econstructor; eauto. + eapply wt_exec_Iop; eauto. + +(* load regular TRAP *) +- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. + exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. + exploit transfer_use_def_satisf; eauto. intros [X Y]. + exploit eval_addressing_lessdef; eauto. intros [a' [F G]]. + exploit Mem.loadv_extends; eauto. intros [v' [P Q]]. + exploit (exec_moves mv2); eauto. intros [ls2 [A2 B2]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_trans. eexact A1. + eapply star_left. econstructor. instantiate (1 := a'). rewrite <- F. + apply eval_addressing_preserved. exact symbols_preserved. eauto. eauto. + eapply star_right. eexact A2. constructor. + eauto. eauto. eauto. traceEq. + exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. + econstructor; eauto. + +(* load pair *) +- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. + exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2). + set (v2' := if Archi.big_endian then v2 else v1) in *. + set (v1' := if Archi.big_endian then v1 else v2) in *. + exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. + assert (LD1: Val.lessdef_list rs##args (reglist ls1 args1')). + { eapply add_equations_lessdef; eauto. } + exploit eval_addressing_lessdef. eexact LD1. eauto. intros [a1' [F1 G1]]. + exploit Mem.loadv_extends. eauto. eexact LOAD1. eexact G1. intros (v1'' & LOAD1' & LD2). + set (ls2 := Locmap.set (R dst1') v1'' (undef_regs (destroyed_by_load Mint32 addr) ls1)). + assert (SAT2: satisf (rs#dst <- v) ls2 e2). + { eapply loc_unconstrained_satisf. eapply can_undef_satisf; eauto. + eapply reg_unconstrained_satisf. eauto. + eapply add_equations_satisf; eauto. assumption. + rewrite Regmap.gss. + apply Val.lessdef_trans with v1'; unfold sel_val; unfold kind_first_word; unfold v1'; destruct Archi.big_endian; auto. + } + exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]]. + assert (LD3: Val.lessdef_list rs##args (reglist ls3 args2')). + { replace (rs##args) with ((rs#dst<-v)##args). + eapply add_equations_lessdef; eauto. + apply list_map_exten; intros. rewrite Regmap.gso; auto. + eapply addressing_not_long; eauto. + } + exploit eval_addressing_lessdef. eexact LD3. + eapply eval_offset_addressing; eauto; apply Archi.splitlong_ptr32; auto. + intros [a2' [F2 G2]]. + assert (LOADX: exists v2'', Mem.loadv Mint32 m' a2' = Some v2'' /\ Val.lessdef v2' v2''). + { discriminate || (eapply Mem.loadv_extends; [eauto|eexact LOAD2|eexact G2]). } + destruct LOADX as (v2'' & LOAD2' & LD4). + set (ls4 := Locmap.set (R dst2') v2'' (undef_regs (destroyed_by_load Mint32 addr2) ls3)). + assert (SAT4: satisf (rs#dst <- v) ls4 e0). + { eapply loc_unconstrained_satisf. eapply can_undef_satisf; eauto. + eapply add_equations_satisf; eauto. assumption. + rewrite Regmap.gss. + apply Val.lessdef_trans with v2'; unfold sel_val; unfold kind_second_word; unfold v2'; destruct Archi.big_endian; auto. + } + exploit (exec_moves mv3); eauto. intros [ls5 [A5 B5]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_trans. eexact A1. + eapply star_left. econstructor. + instantiate (1 := a1'). rewrite <- F1. apply eval_addressing_preserved. exact symbols_preserved. + eexact LOAD1'. instantiate (1 := ls2); auto. + eapply star_trans. eexact A3. + eapply star_left. econstructor. + instantiate (1 := a2'). rewrite <- F2. apply eval_addressing_preserved. exact symbols_preserved. + eexact LOAD2'. instantiate (1 := ls4); auto. + eapply star_right. eexact A5. + constructor. + eauto. eauto. eauto. eauto. eauto. traceEq. + exploit satisf_successors; eauto. simpl; eauto. intros [enext [W Z]]. + econstructor; eauto. + +(* load first word of a pair *) +- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. + exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2). + set (v2' := if Archi.big_endian then v2 else v1) in *. + set (v1' := if Archi.big_endian then v1 else v2) in *. + exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. + assert (LD1: Val.lessdef_list rs##args (reglist ls1 args')). + { eapply add_equations_lessdef; eauto. } + exploit eval_addressing_lessdef. eexact LD1. eauto. intros [a1' [F1 G1]]. + exploit Mem.loadv_extends. eauto. eexact LOAD1. eexact G1. intros (v1'' & LOAD1' & LD2). + set (ls2 := Locmap.set (R dst') v1'' (undef_regs (destroyed_by_load Mint32 addr) ls1)). + assert (SAT2: satisf (rs#dst <- v) ls2 e0). + { eapply parallel_assignment_satisf; eauto. + apply Val.lessdef_trans with v1'; + unfold sel_val; unfold kind_first_word; unfold v1'; destruct Archi.big_endian; auto. + eapply can_undef_satisf. eauto. eapply add_equations_satisf; eauto. + } + exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_trans. eexact A1. + eapply star_left. econstructor. + instantiate (1 := a1'). rewrite <- F1. apply eval_addressing_preserved. exact symbols_preserved. + eexact LOAD1'. instantiate (1 := ls2); auto. + eapply star_right. eexact A3. + constructor. + eauto. eauto. eauto. traceEq. + exploit satisf_successors; eauto. simpl; eauto. intros [enext [W Z]]. + econstructor; eauto. + +(* load second word of a pair *) +- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. + exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2). + set (v2' := if Archi.big_endian then v2 else v1) in *. + set (v1' := if Archi.big_endian then v1 else v2) in *. + exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. + assert (LD1: Val.lessdef_list rs##args (reglist ls1 args')). + { eapply add_equations_lessdef; eauto. } + exploit eval_addressing_lessdef. eexact LD1. + eapply eval_offset_addressing; eauto; apply Archi.splitlong_ptr32; auto. + intros [a1' [F1 G1]]. + assert (LOADX: exists v2'', Mem.loadv Mint32 m' a1' = Some v2'' /\ Val.lessdef v2' v2''). + { discriminate || (eapply Mem.loadv_extends; [eauto|eexact LOAD2|eexact G1]). } + destruct LOADX as (v2'' & LOAD2' & LD2). + set (ls2 := Locmap.set (R dst') v2'' (undef_regs (destroyed_by_load Mint32 addr2) ls1)). + assert (SAT2: satisf (rs#dst <- v) ls2 e0). + { eapply parallel_assignment_satisf; eauto. + apply Val.lessdef_trans with v2'; unfold sel_val; unfold kind_second_word; unfold v2'; destruct Archi.big_endian; auto. + eapply can_undef_satisf. eauto. eapply add_equations_satisf; eauto. + } + exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_trans. eexact A1. + eapply star_left. econstructor. + instantiate (1 := a1'). rewrite <- F1. apply eval_addressing_preserved. exact symbols_preserved. + eexact LOAD2'. instantiate (1 := ls2); auto. + eapply star_right. eexact A3. + constructor. + eauto. eauto. eauto. traceEq. + exploit satisf_successors; eauto. simpl; eauto. intros [enext [W Z]]. + econstructor; eauto. + +(* load dead *) +- exploit exec_moves; eauto. intros [ls1 [X Y]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_right. eexact X. econstructor; eauto. + eauto. traceEq. + exploit satisf_successors. eauto. eauto. simpl; eauto. eauto. + eapply reg_unconstrained_satisf; eauto. + intros [enext [U V]]. + econstructor; eauto. + eapply wt_exec_Iload; eauto. + +- (* load notrap1 *) + generalize (wt_exec_Iload_notrap _ _ _ _ _ _ _ _ WTI WTRS). + intro WTRS'. + exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. + exploit transfer_use_def_satisf; eauto. intros [X Y]. + exploit eval_addressing_lessdef_none; eauto. intro Haddr. + exploit (exec_moves mv2); eauto. intros [ls2 [A2 B2]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_trans. eexact A1. + eapply star_left. eapply exec_Lload_notrap1. rewrite <- Haddr. + apply eval_addressing_preserved. exact symbols_preserved. eauto. + + eapply star_right. eexact A2. constructor. + eauto. eauto. eauto. traceEq. + exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. + econstructor; eauto. + +(* load notrap1 dead *) +- exploit exec_moves; eauto. intros [ls1 [X Y]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_right. eexact X. econstructor; eauto. + eauto. traceEq. + exploit satisf_successors. eauto. eauto. simpl; eauto. eauto. + eapply reg_unconstrained_satisf; eauto. + intros [enext [U V]]. + econstructor; eauto. + eapply wt_exec_Iload_notrap; eauto. + +(* load regular notrap2 *) +- generalize (wt_exec_Iload_notrap _ _ _ _ _ _ _ _ WTI WTRS). + intro WTRS'. + exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. + exploit transfer_use_def_satisf; eauto. intros [X Y]. + exploit eval_addressing_lessdef; eauto. intros [a' [F G]]. + destruct (Mem.loadv chunk m' a') as [v' |] eqn:Hload. + { exploit (exec_moves mv2 env (rs # dst <- Vundef)); eauto. intros [ls2 [A2 B2]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_trans. eexact A1. + eapply star_left. econstructor. instantiate (1 := a'). rewrite <- F. + apply eval_addressing_preserved. exact symbols_preserved. eauto. eauto. + eapply star_right. eexact A2. constructor. + eauto. eauto. eauto. traceEq. + exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. + econstructor; eauto. + } + { exploit (exec_moves mv2 env (rs # dst <- Vundef)); eauto. intros [ls2 [A2 B2]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_trans. eexact A1. + eapply star_left. eapply exec_Lload_notrap2. rewrite <- F. + apply eval_addressing_preserved. exact symbols_preserved. assumption. + eauto. + eapply star_right. eexact A2. constructor. + eauto. eauto. eauto. traceEq. + exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. + econstructor; eauto. + } + +- (* load notrap2 dead *) + exploit exec_moves; eauto. intros [ls1 [X Y]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_right. eexact X. econstructor; eauto. + eauto. traceEq. + exploit satisf_successors. eauto. eauto. simpl; eauto. eauto. + eapply reg_unconstrained_satisf; eauto. + intros [enext [U V]]. + econstructor; eauto. + eapply wt_exec_Iload_notrap; eauto. + +(* store *) +- exploit exec_moves; eauto. intros [ls1 [X Y]]. + exploit add_equations_lessdef; eauto. intros LD. simpl in LD. inv LD. + exploit eval_addressing_lessdef; eauto. intros [a' [F G]]. + exploit Mem.storev_extends; eauto. intros [m'' [P Q]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_trans. eexact X. + eapply star_two. econstructor. instantiate (1 := a'). rewrite <- F. + apply eval_addressing_preserved. exact symbols_preserved. eauto. eauto. + constructor. eauto. eauto. traceEq. + exploit satisf_successors; eauto. simpl; eauto. + eapply can_undef_satisf; eauto. eapply add_equations_satisf; eauto. intros [enext [U V]]. + econstructor; eauto. + +(* store 2 *) +- assert (SF: Archi.ptr64 = false) by (apply Archi.splitlong_ptr32; auto). + exploit Mem.storev_int64_split; eauto. + replace (if Archi.big_endian then Val.hiword rs#src else Val.loword rs#src) + with (sel_val kind_first_word rs#src) + by (unfold kind_first_word; destruct Archi.big_endian; reflexivity). + replace (if Archi.big_endian then Val.loword rs#src else Val.hiword rs#src) + with (sel_val kind_second_word rs#src) + by (unfold kind_second_word; destruct Archi.big_endian; reflexivity). + intros [m1 [STORE1 STORE2]]. + exploit (exec_moves mv1); eauto. intros [ls1 [X Y]]. + exploit add_equations_lessdef. eexact Heqo1. eexact Y. intros LD1. + exploit add_equation_lessdef. eapply add_equations_satisf. eexact Heqo1. eexact Y. + simpl. intros LD2. + set (ls2 := undef_regs (destroyed_by_store Mint32 addr) ls1). + assert (SAT2: satisf rs ls2 e1). + eapply can_undef_satisf. eauto. + eapply add_equation_satisf. eapply add_equations_satisf; eauto. + exploit eval_addressing_lessdef. eexact LD1. eauto. intros [a1' [F1 G1]]. + assert (F1': eval_addressing tge sp addr (reglist ls1 args1') = Some a1'). + rewrite <- F1. apply eval_addressing_preserved. exact symbols_preserved. + exploit Mem.storev_extends. eauto. eexact STORE1. eexact G1. eauto. + intros [m1' [STORE1' EXT1]]. + exploit (exec_moves mv2); eauto. intros [ls3 [U V]]. + exploit add_equations_lessdef. eexact Heqo. eexact V. intros LD3. + exploit add_equation_lessdef. eapply add_equations_satisf. eexact Heqo. eexact V. + simpl. intros LD4. + exploit eval_addressing_lessdef. eexact LD3. eauto. intros [a2' [F2 G2]]. + assert (F2': eval_addressing tge sp addr (reglist ls3 args2') = Some a2'). + rewrite <- F2. apply eval_addressing_preserved. exact symbols_preserved. + exploit (eval_offset_addressing tge); eauto. intros F2''. + assert (STOREX: exists m2', Mem.storev Mint32 m1' (Val.add a2' (Vint (Int.repr 4))) (ls3 (R src2')) = Some m2' /\ Mem.extends m' m2'). + { try discriminate; + (eapply Mem.storev_extends; + [eexact EXT1 | eexact STORE2 | apply Val.add_lessdef; [eexact G2|eauto] | eauto]). } + destruct STOREX as [m2' [STORE2' EXT2]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_trans. eexact X. + eapply star_left. + econstructor. eexact F1'. eexact STORE1'. instantiate (1 := ls2). auto. + eapply star_trans. eexact U. + eapply star_two. + eapply exec_Lstore with (m' := m2'). eexact F2''. discriminate||exact STORE2'. eauto. + constructor. eauto. eauto. eauto. eauto. traceEq. + exploit satisf_successors; eauto. simpl; eauto. + eapply can_undef_satisf. eauto. + eapply add_equation_satisf. eapply add_equations_satisf; eauto. + intros [enext [P Q]]. + econstructor; eauto. + +(* call *) +- set (sg := RTL.funsig fd) in *. + set (args' := loc_arguments sg) in *. + set (res' := loc_result sg) in *. + exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. + exploit find_function_translated. eauto. eauto. eapply add_equations_args_satisf; eauto. + intros [tfd [E F]]. + assert (SIG: funsig tfd = sg). eapply sig_function_translated; eauto. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_right. eexact A1. econstructor; eauto. + eauto. traceEq. + exploit analyze_successors; eauto. simpl. left; eauto. intros [enext [U V]]. + econstructor; eauto. + econstructor; eauto. + inv WTI. congruence. + intros. exploit (exec_moves mv2). eauto. eauto. + eapply function_return_satisf with (v := v) (ls_before := ls1) (ls_after := ls0); eauto. + eapply add_equation_ros_satisf; eauto. + eapply add_equations_args_satisf; eauto. + congruence. + apply wt_regset_assign; auto. + intros [ls2 [A2 B2]]. + exists ls2; split. + eapply star_right. eexact A2. constructor. traceEq. + apply satisf_incr with eafter; auto. + rewrite SIG. eapply add_equations_args_lessdef; eauto. + inv WTI. rewrite <- H7. apply wt_regset_list; auto. + simpl. red; auto. + inv WTI. rewrite SIG. rewrite <- H7. apply wt_regset_list; auto. + +(* tailcall *) +- set (sg := RTL.funsig fd) in *. + set (args' := loc_arguments sg) in *. + exploit Mem.free_parallel_extends; eauto. intros [m'' [P Q]]. + exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. + exploit find_function_translated. eauto. eauto. eapply add_equations_args_satisf; eauto. + intros [tfd [E F]]. + assert (SIG: funsig tfd = sg). eapply sig_function_translated; eauto. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_right. eexact A1. econstructor; eauto. + rewrite <- E. apply find_function_tailcall; auto. + replace (fn_stacksize tf) with (RTL.fn_stacksize f); eauto. + destruct (transf_function_inv _ _ FUN); auto. + eauto. traceEq. + econstructor; eauto. + eapply match_stackframes_change_sig; eauto. rewrite SIG. rewrite e0. decEq. + destruct (transf_function_inv _ _ FUN); auto. + rewrite SIG. rewrite return_regs_arg_values; auto. eapply add_equations_args_lessdef; eauto. + inv WTI. rewrite <- H6. apply wt_regset_list; auto. + apply return_regs_agree_callee_save. + rewrite SIG. inv WTI. rewrite <- H6. apply wt_regset_list; auto. + +(* builtin *) +- exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. + exploit add_equations_builtin_eval; eauto. + intros (C & vargs' & vres' & m'' & D & E & F & G). + assert (WTRS': wt_regset env (regmap_setres res vres rs)) by (eapply wt_exec_Ibuiltin; eauto). + set (ls2 := Locmap.setres res' vres' (undef_regs (destroyed_by_builtin ef) ls1)). + assert (satisf (regmap_setres res vres rs) ls2 e0). + { eapply parallel_set_builtin_res_satisf; eauto. + eapply can_undef_satisf; eauto. } + exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_trans. eexact A1. + eapply star_left. econstructor. + eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved. apply senv_preserved. eauto. + instantiate (1 := ls2); auto. + eapply star_right. eexact A3. + econstructor. + reflexivity. reflexivity. reflexivity. traceEq. + exploit satisf_successors; eauto. simpl; eauto. + intros [enext [U V]]. + econstructor; eauto. + +(* cond *) +- exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_right. eexact A1. + econstructor. eapply eval_condition_lessdef; eauto. eapply add_equations_lessdef; eauto. + eauto. eauto. eauto. traceEq. + exploit satisf_successors; eauto. + instantiate (1 := if b then ifso else ifnot). simpl. destruct b; auto. + eapply can_undef_satisf. eauto. eapply add_equations_satisf; eauto. + intros [enext [U V]]. + econstructor; eauto. + +(* jumptable *) +- exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. + assert (Val.lessdef (Vint n) (ls1 (R arg'))). + rewrite <- H0. eapply add_equation_lessdef with (q := Eq Full arg (R arg')); eauto. + inv H2. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_right. eexact A1. + econstructor. eauto. eauto. eauto. eauto. traceEq. + exploit satisf_successors; eauto. + instantiate (1 := pc'). simpl. eapply list_nth_z_in; eauto. + eapply can_undef_satisf. eauto. eapply add_equation_satisf; eauto. + intros [enext [U V]]. + econstructor; eauto. + +(* return *) +- destruct (transf_function_inv _ _ FUN). + exploit Mem.free_parallel_extends; eauto. rewrite H10. intros [m'' [P Q]]. + inv WTI; MonadInv. ++ (* without an argument *) + exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_right. eexact A1. + econstructor. eauto. eauto. traceEq. + simpl. econstructor; eauto. + apply return_regs_agree_callee_save. + constructor. ++ (* with an argument *) + exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_right. eexact A1. + econstructor. eauto. eauto. traceEq. + simpl. econstructor; eauto. rewrite <- H11. + replace (Locmap.getpair (map_rpair R (loc_result (RTL.fn_sig f))) + (return_regs (parent_locset ts) ls1)) + with (Locmap.getpair (map_rpair R (loc_result (RTL.fn_sig f))) ls1). + eapply add_equations_res_lessdef; eauto. + rewrite <- H14. apply WTRS. + 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. + apply return_regs_agree_callee_save. + rewrite <- H11, <- H14. apply WTRS. + +(* internal function *) +- monadInv FUN. simpl in *. + destruct (transf_function_inv _ _ EQ). + exploit Mem.alloc_extends; eauto. apply Z.le_refl. rewrite H8; apply Z.le_refl. + intros [m'' [U V]]. + assert (WTRS: wt_regset env (init_regs args (fn_params f))). + { apply wt_init_regs. inv H0. rewrite wt_params. rewrite H9. auto. } + exploit (exec_moves mv). eauto. eauto. + eapply can_undef_satisf; eauto. eapply compat_entry_satisf; eauto. + rewrite call_regs_param_values. eexact ARGS. + exact WTRS. + intros [ls1 [A B]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_left. econstructor; eauto. + eapply star_right. eexact A. + econstructor; eauto. + eauto. eauto. traceEq. + econstructor; eauto. + +(* external function *) +- exploit external_call_mem_extends; eauto. intros [v' [m'' [F [G [J K]]]]]. + simpl in FUN; inv FUN. + econstructor; split. + apply plus_one. econstructor; eauto. + eapply external_call_symbols_preserved with (ge1 := ge); eauto. apply senv_preserved. + 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). + assert (WTRES': Val.has_type v' Tlong). + { rewrite <- B. eapply external_call_well_typed; eauto. } + 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). + rewrite locmap_get_set_loc_result_callee_save by auto. + unfold undef_caller_save_regs. destruct l; simpl in H0. + rewrite H0; auto. + destruct sl; auto; congruence. + eapply external_call_well_typed; eauto. + +(* return *) +- inv STACKS. + exploit STEPS; eauto. rewrite WTRES0; auto. intros [ls2 [A B]]. + econstructor; split. + eapply plus_left. constructor. eexact A. traceEq. + econstructor; eauto. + apply wt_regset_assign; auto. rewrite WTRES0; auto. +Qed. + +Lemma initial_states_simulation: + forall st1, RTL.initial_state prog st1 -> + exists st2, LTL.initial_state tprog st2 /\ match_states st1 st2. +Proof. + intros. inv H. + exploit function_ptr_translated; eauto. intros [tf [FIND TR]]. + exploit sig_function_translated; eauto. intros SIG. + exists (LTL.Callstate nil tf (Locmap.init Vundef) m0); split. + econstructor; eauto. + eapply (Genv.init_mem_transf_partial TRANSF); eauto. + rewrite symbols_preserved. + rewrite (match_program_main TRANSF). auto. + congruence. + constructor; auto. + constructor. rewrite SIG; rewrite H3; auto. + rewrite SIG, H3, loc_arguments_main. auto. + red; auto. + apply Mem.extends_refl. + rewrite SIG, H3. constructor. +Qed. + +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. + econstructor. rewrite <- (loc_result_exten sg). inv RES; auto. + rewrite H; auto. +Qed. + +Lemma wt_prog: wt_program prog. +Proof. + red; intros. + exploit list_forall2_in_left. eexact (proj1 TRANSF). eauto. + intros ([i' gd] & A & B & C). simpl in *; subst i'. + inv C. destruct f; simpl in *. +- monadInv H2. + unfold transf_function in EQ. + destruct (type_function f) as [env|] eqn:TF; try discriminate. + econstructor. eapply type_function_correct; eauto. +- constructor. +Qed. + +Theorem transf_program_correct: + forward_simulation (RTL.semantics prog) (LTL.semantics tprog). +Proof. + set (ms := fun s s' => wt_state s /\ match_states s s'). + eapply forward_simulation_plus with (match_states := ms). +- apply senv_preserved. +- intros. exploit initial_states_simulation; eauto. intros [st2 [A B]]. + exists st2; split; auto. split; auto. + apply wt_initial_state with (p := prog); auto. exact wt_prog. +- intros. destruct H. eapply final_states_simulation; eauto. +- intros. destruct H0. + exploit step_simulation; eauto. intros [s2' [A B]]. + exists s2'; split. exact A. split. + eapply subject_reduction; eauto. eexact wt_prog. eexact H. + auto. +Qed. + +End PRESERVATION. diff --git a/backend/Allocproof.v b/backend/Allocproof.v deleted file mode 100644 index 3c7df58a..00000000 --- a/backend/Allocproof.v +++ /dev/null @@ -1,2619 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Correctness proof for the [Allocation] pass (validated translation from - RTL to LTL). *) - -Require Import FunInd. -Require Import FSets. -Require Import Coqlib Ordered Maps Errors Integers Floats. -Require Import AST Linking Lattice Kildall. -Require Import Values Memory Globalenvs Events Smallstep. -Require Archi. -Require Import Op Registers RTL Locations Conventions RTLtyping LTL. -Require Import Allocation. - -Definition match_prog (p: RTL.program) (tp: LTL.program) := - match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. - -Lemma transf_program_match: - forall p tp, transf_program p = OK tp -> match_prog p tp. -Proof. - intros. eapply match_transform_partial_program; eauto. -Qed. - -(** * Soundness of structural checks *) - -Definition expand_move (m: move) : instruction := - match m with - | 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 := - List.map expand_move mv ++ k. - -Definition wf_move (m: move) : Prop := - match m with - | MV (S _ _ _) (S _ _ _) => False - | _ => True - end. - -Definition wf_moves (mv: moves) : Prop := - List.Forall wf_move mv. - -Inductive expand_block_shape: block_shape -> RTL.instruction -> LTL.bblock -> Prop := - | ebs_nop: forall mv s k, - wf_moves mv -> - expand_block_shape (BSnop mv s) - (Inop s) - (expand_moves mv (Lbranch s :: k)) - | ebs_move: forall src dst mv s k, - wf_moves mv -> - expand_block_shape (BSmove src dst mv s) - (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 -> - 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 -> - 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 -> - expand_block_shape (BShighlong src dst mv s) - (Iop Ohighlong (src :: nil) dst s) - (expand_moves mv (Lbranch s :: k)) - | ebs_op: forall op args res mv1 args' res' mv2 s k, - wf_moves mv1 -> wf_moves mv2 -> - expand_block_shape (BSop op args res mv1 args' res' mv2 s) - (Iop op args res s) - (expand_moves mv1 - (Lop op args' res' :: expand_moves mv2 (Lbranch s :: k))) - | ebs_op_dead: forall op args res mv s k, - wf_moves mv -> - expand_block_shape (BSopdead op args res mv s) - (Iop op args res s) - (expand_moves mv (Lbranch s :: k)) - | ebs_load: forall trap chunk addr args dst mv1 args' dst' mv2 s k, - wf_moves mv1 -> wf_moves mv2 -> - expand_block_shape (BSload trap chunk addr args dst mv1 args' dst' mv2 s) - (Iload trap chunk addr args dst s) - (expand_moves mv1 - (Lload trap 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 -> - expand_block_shape (BSload2 addr addr2 args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s) - (Iload TRAP Mint64 addr args dst s) - (expand_moves mv1 - (Lload TRAP Mint32 addr args1' dst1' :: - expand_moves mv2 - (Lload TRAP Mint32 addr2 args2' dst2' :: - 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 -> - expand_block_shape (BSload2_1 addr args dst mv1 args' dst' mv2 s) - (Iload TRAP Mint64 addr args dst s) - (expand_moves mv1 - (Lload TRAP Mint32 addr args' dst' :: - 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 -> - expand_block_shape (BSload2_2 addr addr2 args dst mv1 args' dst' mv2 s) - (Iload TRAP Mint64 addr args dst s) - (expand_moves mv1 - (Lload TRAP Mint32 addr2 args' dst' :: - expand_moves mv2 (Lbranch s :: k))) - | ebs_load_dead: forall trap chunk addr args dst mv s k, - wf_moves mv -> - expand_block_shape (BSloaddead chunk addr args dst mv s) - (Iload trap chunk addr args dst s) - (expand_moves mv (Lbranch s :: k)) - | ebs_store: forall chunk addr args src mv1 args' src' s k, - wf_moves mv1 -> - expand_block_shape (BSstore chunk addr args src mv1 args' src' s) - (Istore chunk addr args src s) - (expand_moves mv1 - (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 -> - expand_block_shape (BSstore2 addr addr2 args src mv1 args1' src1' mv2 args2' src2' s) - (Istore Mint64 addr args src s) - (expand_moves mv1 - (Lstore Mint32 addr args1' src1' :: - expand_moves mv2 - (Lstore Mint32 addr2 args2' src2' :: - Lbranch s :: k))) - | ebs_call: forall sg ros args res mv1 ros' mv2 s k, - wf_moves mv1 -> wf_moves mv2 -> - expand_block_shape (BScall sg ros args res mv1 ros' mv2 s) - (Icall sg ros args res s) - (expand_moves mv1 - (Lcall sg ros' :: expand_moves mv2 (Lbranch s :: k))) - | ebs_tailcall: forall sg ros args mv ros' k, - wf_moves mv -> - expand_block_shape (BStailcall sg ros args mv ros') - (Itailcall sg ros args) - (expand_moves mv (Ltailcall sg ros' :: k)) - | ebs_builtin: forall ef args res mv1 args' res' mv2 s k, - wf_moves mv1 -> wf_moves mv2 -> - expand_block_shape (BSbuiltin ef args res mv1 args' res' mv2 s) - (Ibuiltin ef args res s) - (expand_moves mv1 - (Lbuiltin ef args' res' :: expand_moves mv2 (Lbranch s :: k))) - | ebs_cond: forall cond args mv args' s1 s2 k i i', - wf_moves mv -> - expand_block_shape (BScond cond args mv args' s1 s2) - (Icond cond args s1 s2 i) - (expand_moves mv (Lcond cond args' s1 s2 i' :: k)) - | ebs_jumptable: forall arg mv arg' tbl k, - wf_moves mv -> - expand_block_shape (BSjumptable arg mv arg' tbl) - (Ijumptable arg tbl) - (expand_moves mv (Ljumptable arg' tbl :: k)) - | ebs_return: forall optarg mv k, - wf_moves mv -> - expand_block_shape (BSreturn optarg mv) - (Ireturn optarg) - (expand_moves mv (Lreturn :: k)). - -Ltac MonadInv := - match goal with - | [ H: match ?x with Some _ => _ | None => None end = Some _ |- _ ] => - destruct x as [] eqn:? ; [MonadInv|discriminate] - | [ H: match ?x with left _ => _ | right _ => None end = Some _ |- _ ] => - destruct x; [MonadInv|discriminate] - | [ 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 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 _ |- _ ] => - destruct x as [] eqn:? ; MonadInv - | [ H: Some _ = Some _ |- _ ] => - inv H; MonadInv - | [ H: None = Some _ |- _ ] => - discriminate - | _ => - idtac - end. - -Remark expand_moves_cons: - forall m accu b, - expand_moves (rev (m :: accu)) b = expand_moves (rev accu) (expand_move m :: b). -Proof. - unfold expand_moves; intros. simpl. rewrite map_app. rewrite app_ass. auto. -Qed. - -Lemma extract_moves_sound: - forall b mv b', - extract_moves 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 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 (is_move_operation op args) as [arg|] eqn:E. - exploit is_move_operation_correct; eauto. intros [A B]; subst. - (* reg-reg move *) - exploit IHb; eauto. constructor; auto. exact I. rewrite expand_moves_cons; auto. - inv H; apply BASE; auto. - + (* 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 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: - forall s b, check_succ s b = true -> exists k, b = Lbranch s :: k. -Proof. - intros. destruct b; simpl in H; try discriminate. - destruct i; try discriminate. - destruct (peq s s0); simpl in H; inv H. exists b; auto. -Qed. - -Ltac UseParsingLemmas := - match goal with - | [ H: extract_moves nil _ = (_, _) |- _ ] => - destruct (extract_moves_sound _ _ _ H); clear H; subst; UseParsingLemmas - | [ H: extract_moves_ext nil _ = (_, _) |- _ ] => - destruct (extract_moves_ext_sound _ _ _ H); clear H; subst; UseParsingLemmas - | [ H: check_succ _ _ = true |- _ ] => - try (discriminate H); - destruct (check_succ_sound _ _ H); clear H; subst; UseParsingLemmas - | _ => idtac - end. - -Lemma pair_instr_block_sound: - forall i b bsh, - pair_instr_block i b = Some bsh -> expand_block_shape bsh i b. -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. - MonadInv; UseParsingLemmas. - destruct i; MonadInv; UseParsingLemmas. - eapply ebs_op; eauto. - inv H0. eapply ebs_op_dead; eauto. } - - intros; destruct i; simpl in H; MonadInv; UseParsingLemmas. -- (* nop *) - econstructor; eauto. -- (* op *) - destruct (classify_operation o l). -+ (* move *) - MonadInv; UseParsingLemmas. econstructor; eauto. -+ (* makelong *) - destruct Archi.splitlong eqn:SL; eauto. - MonadInv; UseParsingLemmas. econstructor; eauto. -+ (* lowlong *) - destruct Archi.splitlong eqn:SL; eauto. - MonadInv; UseParsingLemmas. econstructor; eauto. -+ (* highlong *) - destruct Archi.splitlong eqn:SL; eauto. - MonadInv; UseParsingLemmas. econstructor; eauto. -+ (* other ops *) - eauto. -- (* load *) - destruct b0 as [ | [] b0]; MonadInv; UseParsingLemmas. - 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). - 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. - discriminate. - eapply ebs_load; eauto. - inv H. eapply ebs_load_dead; eauto. -- (* store *) - destruct b0; MonadInv. destruct i; MonadInv; UseParsingLemmas. - destruct (chunk_eq m Mint64 && Archi.splitlong) eqn:A; MonadInv; UseParsingLemmas. - destruct b as [ | [] b]; MonadInv; UseParsingLemmas. - InvBooleans. subst m. eapply ebs_store2; eauto. - eapply ebs_store; eauto. -- (* call *) - destruct b0 as [|[] ]; MonadInv; UseParsingLemmas. econstructor; eauto. -- (* tailcall *) - destruct b0 as [|[] ]; MonadInv; UseParsingLemmas. econstructor; eauto. -- (* builtin *) - destruct b1 as [|[] ]; MonadInv; UseParsingLemmas. econstructor; eauto. -- (* cond *) - destruct b0 as [|[]]; MonadInv; UseParsingLemmas. econstructor; eauto. -- (* jumptable *) - destruct b0 as [|[]]; MonadInv; UseParsingLemmas. econstructor; eauto. -- (* return *) - destruct b0 as [|[]]; MonadInv; UseParsingLemmas. econstructor; eauto. -Qed. - -Lemma matching_instr_block: - forall f1 f2 pc bsh i, - (pair_codes f1 f2)!pc = Some bsh -> - (RTL.fn_code f1)!pc = Some i -> - exists b, (LTL.fn_code f2)!pc = Some b /\ expand_block_shape bsh i b. -Proof. - intros. unfold pair_codes in H. rewrite PTree.gcombine in H; auto. rewrite H0 in H. - destruct (LTL.fn_code f2)!pc as [b|]. - exists b; split; auto. apply pair_instr_block_sound; auto. - discriminate. -Qed. - -(** * Properties of equations *) - -Module ESF := FSetFacts.Facts(EqSet). -Module ESP := FSetProperties.Properties(EqSet). -Module ESD := FSetDecide.Decide(EqSet). - -Definition sel_val (k: equation_kind) (v: val) : val := - match k with - | Full => v - | Low => Val.loword v - | High => Val.hiword v - end. - -(** A set of equations [e] is satisfied in a RTL pseudoreg state [rs] - and an LTL location state [ls] if, for every equation [r = l [k]] in [e], - [sel_val k (rs#r)] (the [k] fragment of [r]'s value in the RTL code) - is less defined than [ls l] (the value of [l] in the LTL code). *) - -Definition satisf (rs: regset) (ls: locset) (e: eqs) : Prop := - forall q, EqSet.In q e -> Val.lessdef (sel_val (ekind q) rs#(ereg q)) (ls (eloc q)). - -Lemma empty_eqs_satisf: - forall rs ls, satisf rs ls empty_eqs. -Proof. - unfold empty_eqs; intros; red; intros. ESD.fsetdec. -Qed. - -Lemma satisf_incr: - forall rs ls (e1 e2: eqs), - satisf rs ls e2 -> EqSet.Subset e1 e2 -> satisf rs ls e1. -Proof. - unfold satisf; intros. apply H. ESD.fsetdec. -Qed. - -Lemma satisf_undef_reg: - forall rs ls e r, - satisf rs ls e -> - satisf (rs#r <- Vundef) ls e. -Proof. - intros; red; intros. rewrite Regmap.gsspec. destruct (peq (ereg q) r); auto. - destruct (ekind q); simpl; auto. -Qed. - -Lemma add_equation_lessdef: - forall rs ls q e, - satisf rs ls (add_equation q e) -> Val.lessdef (sel_val (ekind q) rs#(ereg q)) (ls (eloc q)). -Proof. - intros. apply H. unfold add_equation. simpl. apply EqSet.add_1. auto. -Qed. - -Lemma add_equation_satisf: - forall rs ls q e, - satisf rs ls (add_equation q e) -> satisf rs ls e. -Proof. - intros. eapply satisf_incr; eauto. unfold add_equation. simpl. ESD.fsetdec. -Qed. - -Lemma add_equations_satisf: - forall rs ls rl ml e e', - add_equations rl ml e = Some e' -> - satisf rs ls e' -> satisf rs ls e. -Proof. - induction rl; destruct ml; simpl; intros; MonadInv. - auto. - eapply add_equation_satisf; eauto. -Qed. - -Lemma add_equations_lessdef: - forall rs ls rl ml e e', - add_equations rl ml e = Some e' -> - satisf rs ls e' -> - Val.lessdef_list (rs##rl) (reglist ls ml). -Proof. - induction rl; destruct ml; simpl; intros; MonadInv. - constructor. - constructor; eauto. - apply add_equation_lessdef with (e := e) (q := Eq Full a (R m)). - eapply add_equations_satisf; eauto. -Qed. - -Lemma add_equations_args_satisf: - forall rs ls rl tyl ll e e', - add_equations_args rl tyl ll e = Some e' -> - satisf rs ls e' -> satisf rs ls e. -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. -Qed. - -Lemma val_longofwords_eq_1: - forall v, - 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. -- 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: - forall rs ls rl tyl ll e e', - add_equations_args rl tyl ll e = Some e' -> - satisf rs ls e' -> - Val.has_type_list (rs##rl) tyl -> - Val.lessdef_list (rs##rl) (map (fun p => Locmap.getpair p ls) ll). -Proof. - intros until e'. functional induction (add_equations_args rl tyl ll e); simpl; intros. -- 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_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. -Qed. - -Lemma add_equation_ros_satisf: - forall rs ls ros mos e e', - add_equation_ros ros mos e = Some e' -> - satisf rs ls e' -> satisf rs ls e. -Proof. - unfold add_equation_ros; intros. destruct ros; destruct mos; MonadInv. - eapply add_equation_satisf; eauto. - auto. -Qed. - -Lemma remove_equation_satisf: - forall rs ls q e, - satisf rs ls e -> satisf rs ls (remove_equation q e). -Proof. - intros. eapply satisf_incr; eauto. unfold remove_equation; simpl. ESD.fsetdec. -Qed. - -Lemma remove_equation_res_satisf: - forall rs ls r l e e', - remove_equations_res r l e = Some e' -> - satisf rs ls e -> satisf rs ls e'. -Proof. - intros. functional inversion H. - apply remove_equation_satisf; auto. - apply remove_equation_satisf. apply remove_equation_satisf; auto. -Qed. - -Remark select_reg_l_monotone: - forall r q1 q2, - OrderedEquation.eq q1 q2 \/ OrderedEquation.lt q1 q2 -> - select_reg_l r q1 = true -> select_reg_l r q2 = true. -Proof. - unfold select_reg_l; intros. destruct H. - red in H. congruence. - rewrite Pos.leb_le in *. red in H. destruct H as [A | [A B]]. - red in A. zify; omega. - rewrite <- A; auto. -Qed. - -Remark select_reg_h_monotone: - forall r q1 q2, - OrderedEquation.eq q1 q2 \/ OrderedEquation.lt q2 q1 -> - select_reg_h r q1 = true -> select_reg_h r q2 = true. -Proof. - unfold select_reg_h; intros. destruct H. - red in H. congruence. - rewrite Pos.leb_le in *. red in H. destruct H as [A | [A B]]. - red in A. zify; omega. - rewrite A; auto. -Qed. - -Remark select_reg_charact: - forall r q, select_reg_l r q = true /\ select_reg_h r q = true <-> ereg q = r. -Proof. - unfold select_reg_l, select_reg_h; intros; split. - rewrite ! Pos.leb_le. unfold reg; zify; omega. - intros. rewrite H. rewrite ! Pos.leb_refl; auto. -Qed. - -Lemma reg_unconstrained_sound: - forall r e q, - reg_unconstrained r e = true -> - EqSet.In q e -> - ereg q <> r. -Proof. - unfold reg_unconstrained; intros. red; intros. - apply select_reg_charact in H1. - assert (EqSet.mem_between (select_reg_l r) (select_reg_h r) e = true). - { - apply EqSet.mem_between_2 with q; auto. - exact (select_reg_l_monotone r). - exact (select_reg_h_monotone r). - tauto. - tauto. - } - rewrite H2 in H; discriminate. -Qed. - -Lemma reg_unconstrained_satisf: - forall r e rs ls v, - reg_unconstrained r e = true -> - satisf rs ls e -> - satisf (rs#r <- v) ls e. -Proof. - red; intros. rewrite PMap.gso. auto. eapply reg_unconstrained_sound; eauto. -Qed. - -Remark select_loc_l_monotone: - forall l q1 q2, - OrderedEquation'.eq q1 q2 \/ OrderedEquation'.lt q1 q2 -> - select_loc_l l q1 = true -> select_loc_l l q2 = true. -Proof. - unfold select_loc_l; intros. set (lb := OrderedLoc.diff_low_bound l) in *. - destruct H. - red in H. subst q2; auto. - assert (eloc q1 = eloc q2 \/ OrderedLoc.lt (eloc q1) (eloc q2)). - red in H. tauto. - destruct H1. rewrite <- H1; auto. - destruct (OrderedLoc.compare (eloc q2) lb); auto. - assert (OrderedLoc.lt (eloc q1) lb) by (eapply OrderedLoc.lt_trans; eauto). - destruct (OrderedLoc.compare (eloc q1) lb). - auto. - eelim OrderedLoc.lt_not_eq; eauto. - eelim OrderedLoc.lt_not_eq. eapply OrderedLoc.lt_trans. eexact l1. eexact H2. red; auto. -Qed. - -Remark select_loc_h_monotone: - forall l q1 q2, - OrderedEquation'.eq q1 q2 \/ OrderedEquation'.lt q2 q1 -> - select_loc_h l q1 = true -> select_loc_h l q2 = true. -Proof. - unfold select_loc_h; intros. set (lb := OrderedLoc.diff_high_bound l) in *. - destruct H. - red in H. subst q2; auto. - assert (eloc q2 = eloc q1 \/ OrderedLoc.lt (eloc q2) (eloc q1)). - red in H. tauto. - destruct H1. rewrite H1; auto. - destruct (OrderedLoc.compare (eloc q2) lb); auto. - assert (OrderedLoc.lt lb (eloc q1)) by (eapply OrderedLoc.lt_trans; eauto). - destruct (OrderedLoc.compare (eloc q1) lb). - eelim OrderedLoc.lt_not_eq. eapply OrderedLoc.lt_trans. eexact l1. eexact H2. red; auto. - eelim OrderedLoc.lt_not_eq. eexact H2. apply OrderedLoc.eq_sym; auto. - auto. -Qed. - -Remark select_loc_charact: - forall l q, - select_loc_l l q = false \/ select_loc_h l q = false <-> Loc.diff l (eloc q). -Proof. - unfold select_loc_l, select_loc_h; intros; split; intros. - apply OrderedLoc.outside_interval_diff. - destruct H. - left. destruct (OrderedLoc.compare (eloc q) (OrderedLoc.diff_low_bound l)); assumption || discriminate. - right. destruct (OrderedLoc.compare (eloc q) (OrderedLoc.diff_high_bound l)); assumption || discriminate. - exploit OrderedLoc.diff_outside_interval. eauto. - intros [A | A]. - left. destruct (OrderedLoc.compare (eloc q) (OrderedLoc.diff_low_bound l)). - auto. - eelim OrderedLoc.lt_not_eq; eauto. - eelim OrderedLoc.lt_not_eq. eapply OrderedLoc.lt_trans; eauto. red; auto. - right. destruct (OrderedLoc.compare (eloc q) (OrderedLoc.diff_high_bound l)). - eelim OrderedLoc.lt_not_eq. eapply OrderedLoc.lt_trans; eauto. red; auto. - eelim OrderedLoc.lt_not_eq; eauto. apply OrderedLoc.eq_sym; auto. - auto. -Qed. - -Lemma loc_unconstrained_sound: - forall l e q, - loc_unconstrained l e = true -> - EqSet.In q e -> - Loc.diff l (eloc q). -Proof. - unfold loc_unconstrained; intros. - destruct (select_loc_l l q) eqn:SL. - destruct (select_loc_h l q) eqn:SH. - assert (EqSet2.mem_between (select_loc_l l) (select_loc_h l) (eqs2 e) = true). - { - apply EqSet2.mem_between_2 with q; auto. - exact (select_loc_l_monotone l). - exact (select_loc_h_monotone l). - apply eqs_same. auto. - } - rewrite H1 in H; discriminate. - apply select_loc_charact; auto. - apply select_loc_charact; auto. -Qed. - -Lemma loc_unconstrained_satisf: - forall rs ls k r mr e v, - let l := R mr in - satisf rs ls (remove_equation (Eq k r l) e) -> - loc_unconstrained (R mr) (remove_equation (Eq k r l) e) = true -> - Val.lessdef (sel_val k rs#r) v -> - satisf rs (Locmap.set l v ls) e. -Proof. - intros; red; intros. - destruct (OrderedEquation.eq_dec q (Eq k r l)). - subst q; simpl. unfold l; rewrite Locmap.gss. auto. - assert (EqSet.In q (remove_equation (Eq k r l) e)). - simpl. ESD.fsetdec. - rewrite Locmap.gso. apply H; auto. eapply loc_unconstrained_sound; eauto. -Qed. - -Lemma reg_loc_unconstrained_sound: - forall r l e q, - reg_loc_unconstrained r l e = true -> - EqSet.In q e -> - ereg q <> r /\ Loc.diff l (eloc q). -Proof. - intros. destruct (andb_prop _ _ H). - split. eapply reg_unconstrained_sound; eauto. eapply loc_unconstrained_sound; eauto. -Qed. - -Lemma parallel_assignment_satisf: - forall k r mr e rs ls v v', - let l := R mr in - Val.lessdef (sel_val k v) v' -> - reg_loc_unconstrained r (R mr) (remove_equation (Eq k r l) e) = true -> - satisf rs ls (remove_equation (Eq k r l) e) -> - satisf (rs#r <- v) (Locmap.set l v' ls) e. -Proof. - intros; red; intros. - destruct (OrderedEquation.eq_dec q (Eq k r l)). - subst q; simpl. unfold l; rewrite Regmap.gss; rewrite Locmap.gss; auto. - assert (EqSet.In q (remove_equation {| ekind := k; ereg := r; eloc := l |} e)). - simpl. ESD.fsetdec. - exploit reg_loc_unconstrained_sound; eauto. intros [A B]. - rewrite Regmap.gso; auto. rewrite Locmap.gso; auto. -Qed. - -Lemma parallel_assignment_satisf_2: - forall rs ls res res' e e' v v', - remove_equations_res res res' e = Some e' -> - satisf rs ls e' -> - reg_unconstrained res e' = true -> - forallb (fun l => loc_unconstrained l e') (map R (regs_of_rpair res')) = true -> - Val.lessdef v v' -> - satisf (rs#res <- v) (Locmap.setpair res' v' ls) e. -Proof. - intros. functional inversion H. -- (* One location *) - subst. simpl in H2. InvBooleans. simpl. - apply parallel_assignment_satisf with Full; auto. - unfold reg_loc_unconstrained. rewrite H1, H4. auto. -- (* Two 32-bit halves *) - subst. - set (e' := remove_equation {| ekind := Low; ereg := res; eloc := R mr2 |} - (remove_equation {| ekind := High; ereg := res; eloc := R mr1 |} e)) in *. - simpl in H2. InvBooleans. simpl. - red; intros. - destruct (OrderedEquation.eq_dec q (Eq Low res (R mr2))). - subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gss. - 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. - apply Val.hiword_lessdef; auto. - assert (EqSet.In q e'). unfold e', remove_equation; simpl; ESD.fsetdec. - rewrite Regmap.gso. rewrite ! Locmap.gso. auto. - eapply loc_unconstrained_sound; eauto. - eapply loc_unconstrained_sound; eauto. - eapply reg_unconstrained_sound; eauto. -Qed. - -Remark in_elements_between_1: - forall r1 s q, - EqSet.In q (EqSet.elements_between (select_reg_l r1) (select_reg_h r1) s) <-> EqSet.In q s /\ ereg q = r1. -Proof. - intros. rewrite EqSet.elements_between_iff, select_reg_charact. tauto. - exact (select_reg_l_monotone r1). exact (select_reg_h_monotone r1). -Qed. - -Lemma in_subst_reg: - forall r1 r2 q (e: eqs), - EqSet.In q e -> - ereg q = r1 /\ EqSet.In (Eq (ekind q) r2 (eloc q)) (subst_reg r1 r2 e) - \/ ereg q <> r1 /\ EqSet.In q (subst_reg r1 r2 e). -Proof. - intros r1 r2 q e0 IN0. unfold subst_reg. - set (f := fun (q: EqSet.elt) e => add_equation (Eq (ekind q) r2 (eloc q)) (remove_equation q e)). - generalize (in_elements_between_1 r1 e0). - set (elt := EqSet.elements_between (select_reg_l r1) (select_reg_h r1) e0). - intros IN_ELT. - set (P := fun e1 e2 => - EqSet.In q e1 -> - EqSet.In (Eq (ekind q) r2 (eloc q)) e2). - assert (P elt (EqSet.fold f elt e0)). - { - apply ESP.fold_rec; unfold P; intros. - - ESD.fsetdec. - - simpl. red in H1. apply H1 in H3. destruct H3. - + subst x. ESD.fsetdec. - + rewrite ESF.add_iff. rewrite ESF.remove_iff. - destruct (OrderedEquation.eq_dec x {| ekind := ekind q; ereg := r2; eloc := eloc q |}); auto. - left. subst x; auto. - } - set (Q := fun e1 e2 => - ~EqSet.In q e1 -> - EqSet.In q e2). - assert (Q elt (EqSet.fold f elt e0)). - { - apply ESP.fold_rec; unfold Q; intros. - - auto. - - 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. - right. split. red; intros. elim n. rewrite IN_ELT. auto. apply H0. auto. -Qed. - -Lemma subst_reg_satisf: - forall src dst rs ls e, - satisf rs ls (subst_reg dst src e) -> - satisf (rs#dst <- (rs#src)) ls e. -Proof. - intros; red; intros. - destruct (in_subst_reg dst src q e H0) as [[A B] | [A B]]. - subst dst. rewrite Regmap.gss. exploit H; eauto. - rewrite Regmap.gso; auto. -Qed. - -Lemma in_subst_reg_kind: - forall r1 k1 r2 k2 q (e: eqs), - EqSet.In q e -> - (ereg q, ekind q) = (r1, k1) /\ EqSet.In (Eq k2 r2 (eloc q)) (subst_reg_kind r1 k1 r2 k2 e) - \/ EqSet.In q (subst_reg_kind r1 k1 r2 k2 e). -Proof. - intros r1 k1 r2 k2 q e0 IN0. unfold subst_reg. - set (f := fun (q: EqSet.elt) e => - if IndexedEqKind.eq (ekind q) k1 - then add_equation (Eq k2 r2 (eloc q)) (remove_equation q e) - else e). - generalize (in_elements_between_1 r1 e0). - set (elt := EqSet.elements_between (select_reg_l r1) (select_reg_h r1) e0). - intros IN_ELT. - set (P := fun e1 e2 => - EqSet.In q e1 -> ekind q = k1 -> - EqSet.In (Eq k2 r2 (eloc q)) e2). - assert (P elt (EqSet.fold f elt e0)). - { - intros; apply ESP.fold_rec; unfold P; intros. - - ESD.fsetdec. - - simpl. red in H1. apply H1 in H3. destruct H3. - + subst x. unfold f. destruct (IndexedEqKind.eq (ekind q) k1). - simpl. ESD.fsetdec. contradiction. - + unfold f. destruct (IndexedEqKind.eq (ekind x) k1). - simpl. rewrite ESF.add_iff. rewrite ESF.remove_iff. - destruct (OrderedEquation.eq_dec x {| ekind := k2; ereg := r2; eloc := eloc q |}); auto. - left. subst x; auto. - auto. - } - set (Q := fun e1 e2 => - ~EqSet.In q e1 \/ ekind q <> k1 -> - EqSet.In q e2). - assert (Q elt (EqSet.fold f elt e0)). - { - apply ESP.fold_rec; unfold Q; intros. - - auto. - - unfold f. red in H2. rewrite H2 in H4. - destruct (IndexedEqKind.eq (ekind x) k1). - simpl. rewrite ESF.add_iff. rewrite ESF.remove_iff. - right. split. apply H3. tauto. intuition congruence. - apply H3. intuition auto. - } - destruct (ESP.In_dec q elt). - destruct (IndexedEqKind.eq (ekind q) k1). - left. split. f_equal. apply IN_ELT. auto. auto. apply H. auto. auto. - right. apply H0. auto. - right. apply H0. auto. -Qed. - -Lemma subst_reg_kind_satisf_makelong: - forall src1 src2 dst rs ls e, - let e1 := subst_reg_kind dst High src1 Full e in - let e2 := subst_reg_kind dst Low src2 Full e1 in - reg_unconstrained dst e2 = true -> - satisf rs ls e2 -> - satisf (rs#dst <- (Val.longofwords rs#src1 rs#src2)) ls e. -Proof. - intros; red; intros. - destruct (in_subst_reg_kind dst High src1 Full q e H1) as [[A B] | B]; fold e1 in B. - destruct (in_subst_reg_kind dst Low src2 Full _ e1 B) as [[C D] | D]; fold e2 in D. - simpl in C; simpl in D. inv C. - inversion A. rewrite H3; rewrite H4. rewrite Regmap.gss. - apply Val.lessdef_trans with (rs#src1). - simpl. destruct (rs#src1); simpl; auto. destruct (rs#src2); simpl; auto. - rewrite Int64.hi_ofwords. auto. - exploit H0. eexact D. simpl. auto. - destruct (in_subst_reg_kind dst Low src2 Full q e1 B) as [[C D] | D]; fold e2 in D. - inversion C. rewrite H3; rewrite H4. rewrite Regmap.gss. - apply Val.lessdef_trans with (rs#src2). - simpl. destruct (rs#src1); simpl; auto. destruct (rs#src2); simpl; auto. - rewrite Int64.lo_ofwords. auto. - exploit H0. eexact D. simpl. auto. - rewrite Regmap.gso. apply H0; auto. eapply reg_unconstrained_sound; eauto. -Qed. - -Lemma subst_reg_kind_satisf_lowlong: - forall src dst rs ls e, - let e1 := subst_reg_kind dst Full src Low e in - reg_unconstrained dst e1 = true -> - satisf rs ls e1 -> - satisf (rs#dst <- (Val.loword rs#src)) ls e. -Proof. - intros; red; intros. - destruct (in_subst_reg_kind dst Full src Low q e H1) as [[A B] | B]; fold e1 in B. - inversion A. rewrite H3; rewrite H4. simpl. rewrite Regmap.gss. - exploit H0. eexact B. simpl. auto. - rewrite Regmap.gso. apply H0; auto. eapply reg_unconstrained_sound; eauto. -Qed. - -Lemma subst_reg_kind_satisf_highlong: - forall src dst rs ls e, - let e1 := subst_reg_kind dst Full src High e in - reg_unconstrained dst e1 = true -> - satisf rs ls e1 -> - satisf (rs#dst <- (Val.hiword rs#src)) ls e. -Proof. - intros; red; intros. - destruct (in_subst_reg_kind dst Full src High q e H1) as [[A B] | B]; fold e1 in B. - inversion A. rewrite H3; rewrite H4. simpl. rewrite Regmap.gss. - exploit H0. eexact B. simpl. auto. - rewrite Regmap.gso. apply H0; auto. eapply reg_unconstrained_sound; eauto. -Qed. - -Module ESF2 := FSetFacts.Facts(EqSet2). -Module ESP2 := FSetProperties.Properties(EqSet2). -Module ESD2 := FSetDecide.Decide(EqSet2). - -Lemma partial_fold_ind: - forall (A: Type) (P: EqSet2.t -> A -> Prop) f init final s, - EqSet2.fold - (fun q opte => - match opte with - | None => None - | Some e => f q e - end) - s (Some init) = Some final -> - (forall s', EqSet2.Empty s' -> P s' init) -> - (forall x a' a'' s' s'', - EqSet2.In x s -> ~EqSet2.In x s' -> ESP2.Add x s' s'' -> - f x a' = Some a'' -> P s' a' -> P s'' a'') -> - P s final. -Proof. - 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)). - rewrite <- H. apply ESP2.fold_rec; unfold Q, g; intros. - - auto. - - destruct a as [e|]; auto. destruct (f x e) as [e'|] eqn:F; auto. eapply H1; eauto. -Qed. - -Lemma in_subst_loc: - forall l1 l2 q (e e': eqs), - EqSet.In q e -> - subst_loc l1 l2 e = Some e' -> - (eloc q = l1 /\ EqSet.In (Eq (ekind q) (ereg q) l2) e') \/ (Loc.diff l1 (eloc q) /\ EqSet.In q e'). -Proof. - unfold subst_loc; intros l1 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 - Some (add_equation - {| ekind := ekind q0; ereg := ereg q0; eloc := l2 |} - (remove_equation q0 e)) - else None). - set (P := fun e1 e2 => EqSet2.In q e1 -> eloc q = l1 /\ EqSet.In (Eq (ekind q) (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)); inversion H2; subst a''; clear H2. - 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. - destruct (OrderedEquation.eq_dec x {| ekind := ekind q; 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)); 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 loc_type_compat_charact: - forall env l e q, - loc_type_compat env l e = true -> - EqSet.In q e -> - subtype (sel_type (ekind q) (env (ereg q))) (Loc.type l) = true \/ Loc.diff l (eloc q). -Proof. - unfold loc_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 well_typed_move_charact: - forall env l e k r rs, - well_typed_move env l e = true -> - EqSet.In (Eq k r l) e -> - wt_regset env rs -> - match l with - | R mr => True - | S sl ofs ty => Val.has_type (sel_val k rs#r) ty - end. -Proof. - unfold well_typed_move; intros. - destruct l as [mr | sl ofs ty]. - auto. - exploit loc_type_compat_charact; eauto. intros [A | A]. - simpl in A. eapply Val.has_subtype; eauto. - generalize (H1 r). destruct k; simpl; intros. - auto. - destruct (rs#r); exact I. - destruct (rs#r); exact I. - eelim Loc.diff_not_eq. eexact A. auto. -Qed. - -Remark val_lessdef_normalize: - forall v v' ty, - Val.has_type v ty -> Val.lessdef v v' -> - Val.lessdef v (Val.load_result (chunk_of_type ty) v'). -Proof. - intros. inv H0. rewrite Val.load_result_same; auto. auto. -Qed. - -Lemma subst_loc_satisf: - forall env src dst rs ls e e', - subst_loc dst src e = Some e' -> - well_typed_move env dst e = true -> - wt_regset env rs -> - satisf rs ls e' -> - satisf rs (Locmap.set dst (ls src) ls) e. -Proof. - intros; red; intros. - exploit in_subst_loc; eauto. intros [[A B] | [A B]]. - subst dst. rewrite Locmap.gss. - destruct q as [k r l]; simpl in *. - exploit well_typed_move_charact; eauto. - destruct l as [mr | sl ofs ty]; intros. - apply (H2 _ B). - apply val_lessdef_normalize; auto. apply (H2 _ B). - 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). -Proof. - induction ml; simpl; intros. - tauto. - InvBooleans. split. - apply Loc.diff_sym. eapply loc_unconstrained_sound; eauto. - eauto. -Qed. - -Lemma undef_regs_outside: - forall ml ls l, - Loc.notin l (map R ml) -> undef_regs ml ls l = ls l. -Proof. - induction ml; simpl; intros. auto. - rewrite Locmap.gso. apply IHml. tauto. apply Loc.diff_sym. tauto. -Qed. - -Lemma can_undef_satisf: - forall ml e rs ls, - can_undef ml e = true -> - satisf rs ls e -> - satisf rs (undef_regs ml ls) e. -Proof. - intros; red; intros. rewrite undef_regs_outside. eauto. - eapply can_undef_sound; eauto. -Qed. - -Lemma can_undef_except_sound: - forall lx e ml q, - can_undef_except lx ml e = true -> EqSet.In q e -> Loc.diff (eloc q) lx -> Loc.notin (eloc q) (map R ml). -Proof. - induction ml; simpl; intros. - tauto. - InvBooleans. split. - destruct (orb_true_elim _ _ H2). - apply proj_sumbool_true in e0. congruence. - apply Loc.diff_sym. eapply loc_unconstrained_sound; eauto. - eapply IHml; eauto. -Qed. - -Lemma subst_loc_undef_satisf: - forall env src dst rs ls ml e e', - subst_loc dst src e = Some e' -> - well_typed_move env dst e = true -> - can_undef_except dst ml e = true -> - wt_regset env rs -> - satisf rs ls e' -> - satisf rs (Locmap.set dst (ls src) (undef_regs ml ls)) e. -Proof. - intros; red; intros. - exploit in_subst_loc; eauto. intros [[A B] | [A B]]. - subst dst. rewrite Locmap.gss. - destruct q as [k r l]; simpl in *. - exploit well_typed_move_charact; eauto. - destruct l as [mr | sl ofs ty]; intros. - apply (H3 _ B). - apply val_lessdef_normalize; auto. apply (H3 _ B). - rewrite Locmap.gso; auto. rewrite undef_regs_outside. eauto. - eapply can_undef_except_sound; eauto. apply Loc.diff_sym; auto. -Qed. - -Lemma transfer_use_def_satisf: - forall args res args' res' und e e' rs ls, - transfer_use_def args res args' res' und e = Some e' -> - satisf rs ls e' -> - Val.lessdef_list rs##args (reglist ls args') /\ - (forall v v', Val.lessdef v v' -> - satisf (rs#res <- v) (Locmap.set (R res') v' (undef_regs und ls)) e). -Proof. - unfold transfer_use_def; intros. MonadInv. - split. eapply add_equations_lessdef; eauto. - intros. eapply parallel_assignment_satisf; eauto. assumption. - eapply can_undef_satisf; eauto. - eapply add_equations_satisf; eauto. -Qed. - -Lemma add_equations_res_lessdef: - forall r ty l e e' rs ls, - add_equations_res r ty l e = Some e' -> - satisf rs ls e' -> - Val.has_type rs#r ty -> - Val.lessdef rs#r (Locmap.getpair (map_rpair R l) ls). -Proof. - intros. functional inversion H; simpl. -- subst. eapply add_equation_lessdef with (q := Eq Full r (R mr)); eauto. -- 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. - eapply add_equation_lessdef with (q := Eq Low r (R mr2)). - eauto. -Qed. - -Lemma return_regs_agree_callee_save: - forall caller callee, - agree_callee_save caller (return_regs caller callee). -Proof. - intros; red; intros. unfold return_regs. red in H. - destruct l. - rewrite H; auto. - destruct sl; auto || congruence. -Qed. - -Lemma no_caller_saves_sound: - forall e q, - no_caller_saves e = true -> - EqSet.In q e -> - callee_save_loc (eloc q). -Proof. - unfold no_caller_saves, callee_save_loc; intros. - exploit EqSet.for_all_2; eauto. - hnf. intros. simpl in H1. rewrite H1. auto. - lazy beta. destruct (eloc q). auto. destruct sl; congruence. -Qed. - -Lemma val_hiword_longofwords: - forall v1 v2, Val.lessdef (Val.hiword (Val.longofwords v1 v2)) v1. -Proof. - intros. destruct v1; simpl; auto. destruct v2; auto. unfold Val.hiword. - rewrite Int64.hi_ofwords. auto. -Qed. - -Lemma val_loword_longofwords: - forall v1 v2, Val.lessdef (Val.loword (Val.longofwords v1 v2)) v2. -Proof. - intros. destruct v1; simpl; auto. destruct v2; auto. unfold Val.loword. - rewrite Int64.lo_ofwords. auto. -Qed. - -Lemma function_return_satisf: - forall rs ls_before ls_after res res' sg e e' v, - res' = loc_result sg -> - remove_equations_res res res' e = Some e' -> - satisf rs ls_before e' -> - forallb (fun l => reg_loc_unconstrained res l e') (map R (regs_of_rpair res')) = true -> - no_caller_saves e' = true -> - Val.lessdef v (Locmap.getpair (map_rpair R res') ls_after) -> - agree_callee_save ls_before ls_after -> - satisf (rs#res <- v) ls_after e. -Proof. - intros; red; intros. - functional inversion H0. -- (* One register *) - subst. rewrite <- H8 in *. simpl in *. InvBooleans. - set (e' := remove_equation {| ekind := Full; ereg := res; eloc := R mr |} e) in *. - destruct (OrderedEquation.eq_dec q (Eq Full res (R mr))). - subst q; simpl. rewrite Regmap.gss; auto. - assert (EqSet.In q e'). unfold e', remove_equation; simpl. ESD.fsetdec. - exploit reg_loc_unconstrained_sound; eauto. intros [A B]. - rewrite Regmap.gso; auto. - exploit no_caller_saves_sound; eauto. intros. - red in H5. rewrite <- H5; auto. -- (* Two 32-bit halves *) - 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. - destruct (OrderedEquation.eq_dec q (Eq Low res (R mr2))). - subst q; simpl. rewrite Regmap.gss. - eapply Val.lessdef_trans. apply Val.loword_lessdef. eauto. apply val_loword_longofwords. - destruct (OrderedEquation.eq_dec q (Eq High res (R mr1))). - subst q; simpl. rewrite Regmap.gss. - eapply Val.lessdef_trans. apply Val.hiword_lessdef. eauto. apply val_hiword_longofwords. - assert (EqSet.In q e'). unfold e', remove_equation; simpl; ESD.fsetdec. - exploit reg_loc_unconstrained_sound. eexact H. eauto. intros [A B]. - exploit reg_loc_unconstrained_sound. eexact H2. eauto. intros [C D]. - rewrite Regmap.gso; auto. - exploit no_caller_saves_sound; eauto. intros. - red in H5. rewrite <- H5; auto. -Qed. - -Lemma compat_left_sound: - forall r l e q, - compat_left r l e = true -> EqSet.In q e -> ereg q = r -> ekind q = Full /\ eloc q = l. -Proof. - unfold compat_left; intros. - rewrite EqSet.for_all_between_iff in H. - apply select_reg_charact in H1. destruct H1. - exploit H; eauto. intros. - destruct (ekind q); try discriminate. - destruct (Loc.eq l (eloc q)); try discriminate. - auto. - intros. subst x2. auto. - exact (select_reg_l_monotone r). - exact (select_reg_h_monotone r). -Qed. - -Lemma compat_left2_sound: - forall r l1 l2 e q, - compat_left2 r l1 l2 e = true -> EqSet.In q e -> ereg q = r -> - (ekind q = High /\ eloc q = l1) \/ (ekind q = Low /\ eloc q = l2). -Proof. - unfold compat_left2; intros. - rewrite EqSet.for_all_between_iff in H. - apply select_reg_charact in H1. destruct H1. - exploit H; eauto. intros. - destruct (ekind q); try discriminate. - InvBooleans. auto. - InvBooleans. auto. - intros. subst x2. auto. - exact (select_reg_l_monotone r). - exact (select_reg_h_monotone r). -Qed. - -Lemma compat_entry_satisf: - forall rl ll e, - compat_entry rl ll e = true -> - forall vl ls, - Val.lessdef_list vl (map (fun p => Locmap.getpair p ls) ll) -> - satisf (init_regs vl rl) ls e. -Proof. - intros until e. functional induction (compat_entry rl ll e); intros. -- (* no params *) - simpl. red; intros. rewrite Regmap.gi. destruct (ekind q); simpl; auto. -- (* a param in a single location *) - InvBooleans. simpl in H0. inv H0. simpl. - red; intros. rewrite Regmap.gsspec. destruct (peq (ereg q) r1). - exploit compat_left_sound; eauto. intros [A B]. rewrite A; rewrite B; auto. - eapply IHb; eauto. -- (* a param split across two locations *) - InvBooleans. simpl in H0. inv H0. simpl. - red; intros. rewrite Regmap.gsspec. destruct (peq (ereg q) r1). - exploit compat_left2_sound; eauto. - intros [[A B] | [A B]]; rewrite A; rewrite B; simpl. - apply Val.lessdef_trans with (Val.hiword (Val.longofwords (ls l1) (ls l2))). - apply Val.hiword_lessdef; auto. apply val_hiword_longofwords. - apply Val.lessdef_trans with (Val.loword (Val.longofwords (ls l1) (ls l2))). - apply Val.loword_lessdef; auto. apply val_loword_longofwords. - eapply IHb; eauto. -- (* error case *) - discriminate. -Qed. - -Lemma call_regs_param_values: - forall sg ls, - map (fun p => Locmap.getpair p (call_regs ls)) (loc_parameters sg) - = map (fun p => Locmap.getpair p ls) (loc_arguments sg). -Proof. - intros. unfold loc_parameters. rewrite list_map_compose. - apply list_map_exten; intros. symmetry. - assert (A: forall l, loc_argument_acceptable l -> call_regs ls (parameter_of_argument l) = ls l). - { destruct l as [r | [] ofs ty]; simpl; auto; contradiction. } - exploit loc_arguments_acceptable; eauto. destruct x; simpl; intros. -- auto. -- destruct H0; f_equal; auto. -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 ls2) (loc_arguments sg). -Proof. - intros. - apply tailcall_is_possible_correct in H. - 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. - destruct l; simpl; intros; try contradiction. rewrite H4; auto. -Qed. - -Lemma find_function_tailcall: - forall tge ros ls1 ls2, - ros_compatible_tailcall ros = true -> - find_function tge ros (return_regs ls1 ls2) = find_function tge ros ls2. -Proof. - unfold ros_compatible_tailcall, find_function; intros. - destruct ros as [r|id]; auto. - unfold return_regs. destruct (is_callee_save r). discriminate. auto. -Qed. - -Lemma loadv_int64_split: - forall m a v, - Mem.loadv Mint64 m a = Some v -> Archi.splitlong = true -> - exists v1 v2, - Mem.loadv Mint32 m a = Some (if Archi.big_endian then v1 else v2) - /\ Mem.loadv Mint32 m (Val.add a (Vint (Int.repr 4))) = Some (if Archi.big_endian then v2 else v1) - /\ Val.lessdef (Val.hiword v) v1 - /\ Val.lessdef (Val.loword v) v2. -Proof. - 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. - rewrite Int64.hi_ofwords, Int64.lo_ofwords; auto. -Qed. - -Lemma add_equations_builtin_arg_satisf: - forall env rs ls arg arg' e e', - add_equations_builtin_arg env arg arg' e = Some e' -> - satisf rs ls e' -> satisf rs ls e. -Proof. - induction arg; destruct arg'; simpl; intros; MonadInv; eauto. - eapply add_equation_satisf; eauto. - destruct arg'1; MonadInv. destruct arg'2; MonadInv. eauto using add_equation_satisf. -Qed. - -Lemma add_equations_builtin_arg_lessdef: - forall env (ge: RTL.genv) sp rs ls m arg v, - eval_builtin_arg ge (fun r => rs#r) sp m arg v -> - forall e e' arg', - add_equations_builtin_arg env arg arg' e = Some e' -> - satisf rs ls e' -> - wt_regset env rs -> - exists v', eval_builtin_arg ge ls sp m arg' v' /\ Val.lessdef v v'. -Proof. - induction 1; simpl; intros e e' arg' AE SAT WT; destruct arg'; MonadInv. -- exploit add_equation_lessdef; eauto. simpl; intros. - exists (ls x0); auto with barg. -- destruct arg'1; MonadInv. destruct arg'2; MonadInv. - 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_2 rs#x); auto. apply Val.longofwords_lessdef; auto. - rewrite <- e0; apply WT. -- econstructor; eauto with barg. -- econstructor; eauto with barg. -- econstructor; eauto with barg. -- econstructor; eauto with barg. -- econstructor; eauto with barg. -- econstructor; eauto with barg. -- econstructor; eauto with barg. -- econstructor; eauto with barg. -- exploit IHeval_builtin_arg1; eauto. eapply add_equations_builtin_arg_satisf; eauto. - intros (v1 & A & B). - exploit IHeval_builtin_arg2; eauto. intros (v2 & C & D). - exists (Val.longofwords v1 v2); split; auto with barg. apply Val.longofwords_lessdef; auto. -- exploit IHeval_builtin_arg1; eauto. eapply add_equations_builtin_arg_satisf; eauto. - intros (v1' & A & B). - exploit IHeval_builtin_arg2; eauto. intros (v2' & C & D). - econstructor; split. eauto with barg. - destruct Archi.ptr64; auto using Val.add_lessdef, Val.addl_lessdef. -Qed. - -Lemma add_equations_builtin_args_satisf: - forall env rs ls arg arg' e e', - add_equations_builtin_args env arg arg' e = Some e' -> - satisf rs ls e' -> satisf rs ls e. -Proof. - induction arg; destruct arg'; simpl; intros; MonadInv; eauto using add_equations_builtin_arg_satisf. -Qed. - -Lemma add_equations_builtin_args_lessdef: - forall env (ge: RTL.genv) sp rs ls m tm arg vl, - eval_builtin_args ge (fun r => rs#r) sp m arg vl -> - forall arg' e e', - add_equations_builtin_args env arg arg' e = Some e' -> - satisf rs ls e' -> - wt_regset env rs -> - Mem.extends m tm -> - exists vl', eval_builtin_args ge ls sp tm arg' vl' /\ Val.lessdef_list vl vl'. -Proof. - induction 1; simpl; intros; destruct arg'; MonadInv. -- exists (@nil val); split; constructor. -- exploit IHlist_forall2; eauto. intros (vl' & A & B). - exploit add_equations_builtin_arg_lessdef; eauto. - eapply add_equations_builtin_args_satisf; eauto. intros (v1' & C & D). - exploit (@eval_builtin_arg_lessdef _ ge ls ls); eauto. intros (v1'' & E & F). - exists (v1'' :: vl'); split; constructor; auto. eapply Val.lessdef_trans; eauto. -Qed. - -Lemma add_equations_debug_args_satisf: - forall env rs ls arg arg' e e', - add_equations_debug_args env arg arg' e = Some e' -> - satisf rs ls e' -> satisf rs ls e. -Proof. - induction arg; destruct arg'; simpl; intros; MonadInv; auto. - destruct (add_equations_builtin_arg env a b e) as [e1|] eqn:A; - eauto using add_equations_builtin_arg_satisf. -Qed. - -Lemma add_equations_debug_args_eval: - forall env (ge: RTL.genv) sp rs ls m tm arg vl, - eval_builtin_args ge (fun r => rs#r) sp m arg vl -> - forall arg' e e', - add_equations_debug_args env arg arg' e = Some e' -> - satisf rs ls e' -> - wt_regset env rs -> - Mem.extends m tm -> - exists vl', eval_builtin_args ge ls sp tm arg' vl'. -Proof. - induction 1; simpl; intros; destruct arg'; MonadInv. -- exists (@nil val); constructor. -- exists (@nil val); constructor. -- destruct (add_equations_builtin_arg env a1 b e) as [e1|] eqn:A. -+ exploit IHlist_forall2; eauto. intros (vl' & B). - exploit add_equations_builtin_arg_lessdef; eauto. - eapply add_equations_debug_args_satisf; eauto. intros (v1' & C & D). - exploit (@eval_builtin_arg_lessdef _ ge ls ls); eauto. intros (v1'' & E & F). - exists (v1'' :: vl'); constructor; auto. -+ eauto. -Qed. - -Lemma add_equations_builtin_eval: - forall ef env args args' e1 e2 m1 m1' rs ls (ge: RTL.genv) sp vargs t vres m2, - wt_regset env rs -> - match ef with - | EF_debug _ _ _ => add_equations_debug_args env args args' e1 - | _ => add_equations_builtin_args env args args' e1 - end = Some e2 -> - Mem.extends m1 m1' -> - satisf rs ls e2 -> - eval_builtin_args ge (fun r => rs # r) sp m1 args vargs -> - external_call ef ge vargs m1 t vres m2 -> - satisf rs ls e1 /\ - exists vargs' vres' m2', - eval_builtin_args ge ls sp m1' args' vargs' - /\ external_call ef ge vargs' m1' t vres' m2' - /\ Val.lessdef vres vres' - /\ Mem.extends m2 m2'. -Proof. - intros. - assert (DEFAULT: add_equations_builtin_args env args args' e1 = Some e2 -> - satisf rs ls e1 /\ - exists vargs' vres' m2', - eval_builtin_args ge ls sp m1' args' vargs' - /\ external_call ef ge vargs' m1' t vres' m2' - /\ Val.lessdef vres vres' - /\ Mem.extends m2 m2'). - { - intros. split. eapply add_equations_builtin_args_satisf; eauto. - exploit add_equations_builtin_args_lessdef; eauto. - intros (vargs' & A & B). - exploit external_call_mem_extends; eauto. - intros (vres' & m2' & C & D & E & F). - exists vargs', vres', m2'; auto. - } - destruct ef; auto. - split. eapply add_equations_debug_args_satisf; eauto. - exploit add_equations_debug_args_eval; eauto. - intros (vargs' & A). - simpl in H4; inv H4. - exists vargs', Vundef, m1'. intuition auto. simpl. constructor. -Qed. - -Lemma parallel_set_builtin_res_satisf: - forall env res res' e0 e1 rs ls v v', - remove_equations_builtin_res env res res' e0 = Some e1 -> - forallb (fun r => reg_unconstrained r e1) (params_of_builtin_res res) = true -> - forallb (fun mr => loc_unconstrained (R mr) e1) (params_of_builtin_res res') = true -> - satisf rs ls e1 -> - Val.lessdef v v' -> - satisf (regmap_setres res v rs) (Locmap.setres res' v' ls) e0. -Proof. - intros. rewrite forallb_forall in *. - destruct res, res'; simpl in *; inv H. -- apply parallel_assignment_satisf with (k := Full); auto. - unfold reg_loc_unconstrained. rewrite H0 by auto. rewrite H1 by auto. auto. -- destruct res'1; try discriminate. destruct res'2; try discriminate. - rename x0 into hi; rename x1 into lo. MonadInv. destruct (mreg_eq hi lo); inv H5. - set (e' := remove_equation {| ekind := High; ereg := x; eloc := R hi |} e0) in *. - set (e'' := remove_equation {| ekind := Low; ereg := x; eloc := R lo |} e') in *. - simpl in *. red; intros. - destruct (OrderedEquation.eq_dec q (Eq Low x (R lo))). - subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gss. apply Val.loword_lessdef; auto. - destruct (OrderedEquation.eq_dec q (Eq High x (R hi))). - subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gso by (red; auto). - rewrite Locmap.gss. apply Val.hiword_lessdef; auto. - assert (EqSet.In q e''). - { unfold e'', e', remove_equation; simpl; ESD.fsetdec. } - rewrite Regmap.gso. rewrite ! Locmap.gso. auto. - eapply loc_unconstrained_sound; eauto. - eapply loc_unconstrained_sound; eauto. - eapply reg_unconstrained_sound; eauto. -- auto. -Qed. - -(** * Properties of the dataflow analysis *) - -Lemma analyze_successors: - forall f env bsh an pc bs s e, - analyze f env bsh = Some an -> - bsh!pc = Some bs -> - In s (successors_block_shape bs) -> - an!!pc = OK e -> - exists e', transfer f env bsh s an!!s = OK e' /\ EqSet.Subset e' e. -Proof. - unfold analyze; intros. exploit DS.fixpoint_allnodes_solution; eauto. - rewrite H2. unfold DS.L.ge. destruct (transfer f env bsh s an#s); intros. - exists e0; auto. - contradiction. -Qed. - -Lemma satisf_successors: - forall f env bsh an pc bs s e rs ls, - analyze f env bsh = Some an -> - bsh!pc = Some bs -> - In s (successors_block_shape bs) -> - an!!pc = OK e -> - satisf rs ls e -> - exists e', transfer f env bsh s an!!s = OK e' /\ satisf rs ls e'. -Proof. - intros. exploit analyze_successors; eauto. intros [e' [A B]]. - exists e'; split; auto. eapply satisf_incr; eauto. -Qed. - -(** Inversion on [transf_function] *) - -Inductive transf_function_spec (f: RTL.function) (tf: LTL.function) : Prop := - | transf_function_spec_intro: - forall env an mv k e1 e2, - wt_function f env -> - analyze f env (pair_codes f tf) = Some an -> - (LTL.fn_code tf)!(LTL.fn_entrypoint tf) = Some(expand_moves mv (Lbranch (RTL.fn_entrypoint f) :: k)) -> - wf_moves mv -> - transfer f env (pair_codes f tf) (RTL.fn_entrypoint f) an!!(RTL.fn_entrypoint f) = OK e1 -> - track_moves env mv e1 = Some e2 -> - compat_entry (RTL.fn_params f) (loc_parameters (fn_sig tf)) e2 = true -> - can_undef destroyed_at_function_entry e2 = true -> - RTL.fn_stacksize f = LTL.fn_stacksize tf -> - RTL.fn_sig f = LTL.fn_sig tf -> - transf_function_spec f tf. - -Lemma transf_function_inv: - forall f tf, - transf_function f = OK tf -> - transf_function_spec f tf. -Proof. - unfold transf_function; intros. - destruct (type_function f) as [env|] eqn:TY; try discriminate. - destruct (regalloc f); try discriminate. - destruct (check_function f f0 env) as [] eqn:?; inv H. - unfold check_function in Heqr. - destruct (analyze f env (pair_codes f tf)) as [an|] eqn:?; try discriminate. - monadInv Heqr. - destruct (check_entrypoints_aux f tf env x) as [y|] eqn:?; try discriminate. - unfold check_entrypoints_aux, pair_entrypoints in Heqo0. MonadInv. - 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. - -Lemma invert_code: - forall f env tf pc i opte e, - wt_function f env -> - (RTL.fn_code f)!pc = Some i -> - transfer f env (pair_codes f tf) pc opte = OK e -> - exists eafter, exists bsh, exists bb, - opte = OK eafter /\ - (pair_codes f tf)!pc = Some bsh /\ - (LTL.fn_code tf)!pc = Some bb /\ - expand_block_shape bsh i bb /\ - transfer_aux f env bsh eafter = Some e /\ - wt_instr f env i. -Proof. - intros. destruct opte as [eafter|]; simpl in H1; try discriminate. exists eafter. - destruct (pair_codes f tf)!pc as [bsh|] eqn:?; try discriminate. exists bsh. - exploit matching_instr_block; eauto. intros [bb [A B]]. - destruct (transfer_aux f env bsh eafter) as [e1|] eqn:?; inv H1. - exists bb. exploit wt_instr_at; eauto. - tauto. -Qed. - -(** * Semantic preservation *) - -Section PRESERVATION. - -Variable prog: RTL.program. -Variable tprog: LTL.program. -Hypothesis TRANSF: match_prog prog tprog. - -Let ge := Genv.globalenv prog. -Let tge := Genv.globalenv tprog. - -Lemma symbols_preserved: - forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof (Genv.find_symbol_match TRANSF). - -Lemma senv_preserved: - Senv.equiv ge tge. -Proof (Genv.senv_match TRANSF). - -Lemma functions_translated: - forall (v: val) (f: RTL.fundef), - Genv.find_funct ge v = Some f -> - exists tf, - Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf. -Proof (Genv.find_funct_transf_partial TRANSF). - -Lemma function_ptr_translated: - forall (b: block) (f: RTL.fundef), - Genv.find_funct_ptr ge b = Some f -> - exists tf, - Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf. -Proof (Genv.find_funct_ptr_transf_partial TRANSF). - -Lemma sig_function_translated: - forall f tf, - transf_fundef f = OK tf -> - LTL.funsig tf = RTL.funsig f. -Proof. - intros; destruct f; monadInv H. - destruct (transf_function_inv _ _ EQ). simpl; auto. - auto. -Qed. - -Lemma find_function_translated: - forall ros rs fd ros' e e' ls, - RTL.find_function ge ros rs = Some fd -> - add_equation_ros ros ros' e = Some e' -> - satisf rs ls e' -> - exists tfd, - LTL.find_function tge ros' ls = Some tfd /\ transf_fundef fd = OK tfd. -Proof. - unfold RTL.find_function, LTL.find_function; intros. - destruct ros as [r|id]; destruct ros' as [r'|id']; simpl in H0; MonadInv. - (* two regs *) - exploit add_equation_lessdef; eauto. intros LD. inv LD. - eapply functions_translated; eauto. - rewrite <- H2 in H. simpl in H. congruence. - (* two symbols *) - rewrite symbols_preserved. rewrite Heqo. - eapply function_ptr_translated; eauto. -Qed. - -Lemma exec_moves: - forall mv env rs s f sp bb m e e' ls, - track_moves env mv e = Some e' -> - wf_moves mv -> - satisf rs ls e' -> - wt_regset env rs -> - exists ls', - star step tge (Block s f sp (expand_moves mv bb) ls m) - E0 (Block s f sp bb ls' m) - /\ satisf rs ls' e. -Proof. -Opaque destroyed_by_op. - induction mv; simpl; intros. - (* base *) -- unfold expand_moves; simpl. inv H. exists ls; split. apply star_refl. auto. - (* step *) -- assert (wf_moves mv) by (inv H0; auto). - destruct a; unfold expand_moves; simpl; MonadInv. -+ (* loc-loc move *) - destruct src as [rsrc | ssrc]; destruct dst as [rdst | sdst]. -* (* reg-reg *) - exploit IHmv; eauto. eapply subst_loc_undef_satisf; eauto. - intros [ls' [A B]]. exists ls'; split; auto. eapply star_left; eauto. - econstructor. simpl. eauto. auto. auto. -* (* reg->stack *) - exploit IHmv; eauto. eapply subst_loc_undef_satisf; eauto. - intros [ls' [A B]]. exists ls'; split; auto. eapply star_left; eauto. - econstructor. simpl. eauto. auto. -* (* stack->reg *) - simpl in Heqb. exploit IHmv; eauto. eapply subst_loc_undef_satisf; eauto. - intros [ls' [A B]]. exists ls'; split; auto. eapply star_left; eauto. - 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 *) - -Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> signature -> Prop := - | match_stackframes_nil: forall sg, - sg.(sig_res) = Tint -> - match_stackframes nil nil sg - | match_stackframes_cons: - forall res f sp pc rs s tf bb ls ts sg an e env - (STACKS: match_stackframes s ts (fn_sig tf)) - (FUN: transf_function f = OK tf) - (ANL: analyze f env (pair_codes f tf) = Some an) - (EQ: transfer f env (pair_codes f tf) pc an!!pc = OK e) - (WTF: wt_function f env) - (WTRS: wt_regset env rs) - (WTRES: env res = proj_sig_res sg) - (STEPS: forall v ls1 m, - Val.lessdef v (Locmap.getpair (map_rpair R (loc_result sg)) ls1) -> - Val.has_type v (env res) -> - agree_callee_save ls ls1 -> - exists ls2, - star LTL.step tge (Block ts tf sp bb ls1 m) - E0 (State ts tf sp pc ls2 m) - /\ satisf (rs#res <- v) ls2 e), - match_stackframes - (RTL.Stackframe res f sp pc rs :: s) - (LTL.Stackframe tf sp ls bb :: ts) - sg. - -Inductive match_states: RTL.state -> LTL.state -> Prop := - | match_states_intro: - forall s f sp pc rs m ts tf ls m' an e env - (STACKS: match_stackframes s ts (fn_sig tf)) - (FUN: transf_function f = OK tf) - (ANL: analyze f env (pair_codes f tf) = Some an) - (EQ: transfer f env (pair_codes f tf) pc an!!pc = OK e) - (SAT: satisf rs ls e) - (MEM: Mem.extends m m') - (WTF: wt_function f env) - (WTRS: wt_regset env rs), - match_states (RTL.State s f sp pc rs m) - (LTL.State ts tf sp pc ls m') - | match_states_call: - forall s f args m ts tf ls m' - (STACKS: match_stackframes s ts (funsig tf)) - (FUN: transf_fundef f = OK tf) - (ARGS: Val.lessdef_list args (map (fun p => Locmap.getpair p ls) (loc_arguments (funsig tf)))) - (AG: agree_callee_save (parent_locset ts) ls) - (MEM: Mem.extends m m') - (WTARGS: Val.has_type_list args (sig_args (funsig tf))), - match_states (RTL.Callstate s f args m) - (LTL.Callstate ts tf ls m') - | match_states_return: - forall s res m ts ls m' sg - (STACKS: match_stackframes s ts sg) - (RES: Val.lessdef res (Locmap.getpair (map_rpair R (loc_result sg)) ls)) - (AG: agree_callee_save (parent_locset ts) ls) - (MEM: Mem.extends m m') - (WTRES: Val.has_type res (proj_sig_res sg)), - match_states (RTL.Returnstate s res m) - (LTL.Returnstate ts ls m'). - -Lemma match_stackframes_change_sig: - forall s ts sg sg', - match_stackframes s ts sg -> - sg'.(sig_res) = sg.(sig_res) -> - match_stackframes s ts sg'. -Proof. - intros. inv H. - constructor. congruence. - econstructor; eauto. - unfold proj_sig_res in *. rewrite H0; auto. - intros. rewrite (loc_result_exten sg' sg) in H by auto. eauto. -Qed. - -Ltac UseShape := - match goal with - | [ WT: wt_function _ _, CODE: (RTL.fn_code _)!_ = Some _, EQ: transfer _ _ _ _ _ = OK _ |- _ ] => - destruct (invert_code _ _ _ _ _ _ _ WT CODE EQ) as (eafter & bsh & bb & AFTER & BSH & TCODE & EBS & TR & WTI); - inv EBS; unfold transfer_aux in TR; MonadInv - end. - -Remark addressing_not_long: - forall trap env f addr args dst s r, - wt_instr f env (Iload trap Mint64 addr args dst s) -> Archi.splitlong = true -> - In r args -> r <> dst. -Proof. - intros. inv H. - assert (A: forall ty, In ty (type_of_addressing addr) -> ty = Tptr). - { intros. destruct addr; simpl in H; intuition. } - 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. } - red; intros; subst r. rewrite C in H9; discriminate. -Qed. - -(** The proof of semantic preservation is a simulation argument of the - "plus" kind. *) - -Lemma step_simulation: - forall S1 t S2, RTL.step ge S1 t S2 -> wt_state S1 -> - forall S1', match_states S1 S1' -> - exists S2', plus LTL.step tge S1' t S2' /\ match_states S2 S2'. -Proof. - induction 1; intros WT S1' MS; inv MS; try UseShape. - -(* nop *) -- exploit exec_moves; eauto. intros [ls1 [X Y]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_right. eexact X. econstructor; eauto. - eauto. traceEq. - exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. - econstructor; eauto. - -(* op move *) -- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'. - simpl in H0. inv H0. - exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_right. eexact X. econstructor; eauto. - eauto. traceEq. - exploit satisf_successors; eauto. simpl; eauto. eapply subst_reg_satisf; eauto. - intros [enext [U V]]. - econstructor; eauto. - -(* op makelong *) -- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'. - simpl in H0. inv H0. - exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_right. eexact X. econstructor; eauto. - eauto. traceEq. - exploit satisf_successors; eauto. simpl; eauto. - eapply subst_reg_kind_satisf_makelong. eauto. eauto. - intros [enext [U V]]. - econstructor; eauto. - -(* op lowlong *) -- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'. - simpl in H0. inv H0. - exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_right. eexact X. econstructor; eauto. - eauto. traceEq. - exploit satisf_successors; eauto. simpl; eauto. - eapply subst_reg_kind_satisf_lowlong. eauto. eauto. - intros [enext [U V]]. - econstructor; eauto. - -(* op highlong *) -- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'. - simpl in H0. inv H0. - exploit (exec_moves mv); eauto. intros [ls1 [X Y]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_right. eexact X. econstructor; eauto. - eauto. traceEq. - exploit satisf_successors; eauto. simpl; eauto. - eapply subst_reg_kind_satisf_highlong. eauto. eauto. - intros [enext [U V]]. - econstructor; eauto. - -(* op regular *) -- generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'. - exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. - exploit transfer_use_def_satisf; eauto. intros [X Y]. - exploit eval_operation_lessdef; eauto. intros [v' [F G]]. - exploit (exec_moves mv2); eauto. intros [ls2 [A2 B2]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_trans. eexact A1. - eapply star_left. econstructor. instantiate (1 := v'). rewrite <- F. - apply eval_operation_preserved. exact symbols_preserved. - eauto. eapply star_right. eexact A2. constructor. - eauto. eauto. eauto. traceEq. - exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. - econstructor; eauto. - -(* op dead *) -- exploit exec_moves; eauto. intros [ls1 [X Y]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_right. eexact X. econstructor; eauto. - eauto. traceEq. - exploit satisf_successors. eauto. eauto. simpl; eauto. eauto. - eapply reg_unconstrained_satisf; eauto. - intros [enext [U V]]. - econstructor; eauto. - eapply wt_exec_Iop; eauto. - -(* load regular TRAP *) -- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. - exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. - exploit transfer_use_def_satisf; eauto. intros [X Y]. - exploit eval_addressing_lessdef; eauto. intros [a' [F G]]. - exploit Mem.loadv_extends; eauto. intros [v' [P Q]]. - exploit (exec_moves mv2); eauto. intros [ls2 [A2 B2]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_trans. eexact A1. - eapply star_left. econstructor. instantiate (1 := a'). rewrite <- F. - apply eval_addressing_preserved. exact symbols_preserved. eauto. eauto. - eapply star_right. eexact A2. constructor. - eauto. eauto. eauto. traceEq. - exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. - econstructor; eauto. - -(* load pair *) -- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. - exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2). - set (v2' := if Archi.big_endian then v2 else v1) in *. - set (v1' := if Archi.big_endian then v1 else v2) in *. - exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. - assert (LD1: Val.lessdef_list rs##args (reglist ls1 args1')). - { eapply add_equations_lessdef; eauto. } - exploit eval_addressing_lessdef. eexact LD1. eauto. intros [a1' [F1 G1]]. - exploit Mem.loadv_extends. eauto. eexact LOAD1. eexact G1. intros (v1'' & LOAD1' & LD2). - set (ls2 := Locmap.set (R dst1') v1'' (undef_regs (destroyed_by_load Mint32 addr) ls1)). - assert (SAT2: satisf (rs#dst <- v) ls2 e2). - { eapply loc_unconstrained_satisf. eapply can_undef_satisf; eauto. - eapply reg_unconstrained_satisf. eauto. - eapply add_equations_satisf; eauto. assumption. - rewrite Regmap.gss. - apply Val.lessdef_trans with v1'; unfold sel_val; unfold kind_first_word; unfold v1'; destruct Archi.big_endian; auto. - } - exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]]. - assert (LD3: Val.lessdef_list rs##args (reglist ls3 args2')). - { replace (rs##args) with ((rs#dst<-v)##args). - eapply add_equations_lessdef; eauto. - apply list_map_exten; intros. rewrite Regmap.gso; auto. - eapply addressing_not_long; eauto. - } - exploit eval_addressing_lessdef. eexact LD3. - eapply eval_offset_addressing; eauto; apply Archi.splitlong_ptr32; auto. - intros [a2' [F2 G2]]. - assert (LOADX: exists v2'', Mem.loadv Mint32 m' a2' = Some v2'' /\ Val.lessdef v2' v2''). - { discriminate || (eapply Mem.loadv_extends; [eauto|eexact LOAD2|eexact G2]). } - destruct LOADX as (v2'' & LOAD2' & LD4). - set (ls4 := Locmap.set (R dst2') v2'' (undef_regs (destroyed_by_load Mint32 addr2) ls3)). - assert (SAT4: satisf (rs#dst <- v) ls4 e0). - { eapply loc_unconstrained_satisf. eapply can_undef_satisf; eauto. - eapply add_equations_satisf; eauto. assumption. - rewrite Regmap.gss. - apply Val.lessdef_trans with v2'; unfold sel_val; unfold kind_second_word; unfold v2'; destruct Archi.big_endian; auto. - } - exploit (exec_moves mv3); eauto. intros [ls5 [A5 B5]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_trans. eexact A1. - eapply star_left. econstructor. - instantiate (1 := a1'). rewrite <- F1. apply eval_addressing_preserved. exact symbols_preserved. - eexact LOAD1'. instantiate (1 := ls2); auto. - eapply star_trans. eexact A3. - eapply star_left. econstructor. - instantiate (1 := a2'). rewrite <- F2. apply eval_addressing_preserved. exact symbols_preserved. - eexact LOAD2'. instantiate (1 := ls4); auto. - eapply star_right. eexact A5. - constructor. - eauto. eauto. eauto. eauto. eauto. traceEq. - exploit satisf_successors; eauto. simpl; eauto. intros [enext [W Z]]. - econstructor; eauto. - -(* load first word of a pair *) -- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. - exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2). - set (v2' := if Archi.big_endian then v2 else v1) in *. - set (v1' := if Archi.big_endian then v1 else v2) in *. - exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. - assert (LD1: Val.lessdef_list rs##args (reglist ls1 args')). - { eapply add_equations_lessdef; eauto. } - exploit eval_addressing_lessdef. eexact LD1. eauto. intros [a1' [F1 G1]]. - exploit Mem.loadv_extends. eauto. eexact LOAD1. eexact G1. intros (v1'' & LOAD1' & LD2). - set (ls2 := Locmap.set (R dst') v1'' (undef_regs (destroyed_by_load Mint32 addr) ls1)). - assert (SAT2: satisf (rs#dst <- v) ls2 e0). - { eapply parallel_assignment_satisf; eauto. - apply Val.lessdef_trans with v1'; - unfold sel_val; unfold kind_first_word; unfold v1'; destruct Archi.big_endian; auto. - eapply can_undef_satisf. eauto. eapply add_equations_satisf; eauto. - } - exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_trans. eexact A1. - eapply star_left. econstructor. - instantiate (1 := a1'). rewrite <- F1. apply eval_addressing_preserved. exact symbols_preserved. - eexact LOAD1'. instantiate (1 := ls2); auto. - eapply star_right. eexact A3. - constructor. - eauto. eauto. eauto. traceEq. - exploit satisf_successors; eauto. simpl; eauto. intros [enext [W Z]]. - econstructor; eauto. - -(* load second word of a pair *) -- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. - exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2). - set (v2' := if Archi.big_endian then v2 else v1) in *. - set (v1' := if Archi.big_endian then v1 else v2) in *. - exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. - assert (LD1: Val.lessdef_list rs##args (reglist ls1 args')). - { eapply add_equations_lessdef; eauto. } - exploit eval_addressing_lessdef. eexact LD1. - eapply eval_offset_addressing; eauto; apply Archi.splitlong_ptr32; auto. - intros [a1' [F1 G1]]. - assert (LOADX: exists v2'', Mem.loadv Mint32 m' a1' = Some v2'' /\ Val.lessdef v2' v2''). - { discriminate || (eapply Mem.loadv_extends; [eauto|eexact LOAD2|eexact G1]). } - destruct LOADX as (v2'' & LOAD2' & LD2). - set (ls2 := Locmap.set (R dst') v2'' (undef_regs (destroyed_by_load Mint32 addr2) ls1)). - assert (SAT2: satisf (rs#dst <- v) ls2 e0). - { eapply parallel_assignment_satisf; eauto. - apply Val.lessdef_trans with v2'; unfold sel_val; unfold kind_second_word; unfold v2'; destruct Archi.big_endian; auto. - eapply can_undef_satisf. eauto. eapply add_equations_satisf; eauto. - } - exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_trans. eexact A1. - eapply star_left. econstructor. - instantiate (1 := a1'). rewrite <- F1. apply eval_addressing_preserved. exact symbols_preserved. - eexact LOAD2'. instantiate (1 := ls2); auto. - eapply star_right. eexact A3. - constructor. - eauto. eauto. eauto. traceEq. - exploit satisf_successors; eauto. simpl; eauto. intros [enext [W Z]]. - econstructor; eauto. - -(* load dead *) -- exploit exec_moves; eauto. intros [ls1 [X Y]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_right. eexact X. econstructor; eauto. - eauto. traceEq. - exploit satisf_successors. eauto. eauto. simpl; eauto. eauto. - eapply reg_unconstrained_satisf; eauto. - intros [enext [U V]]. - econstructor; eauto. - eapply wt_exec_Iload; eauto. - -- (* load notrap1 *) - generalize (wt_exec_Iload_notrap _ _ _ _ _ _ _ _ WTI WTRS). - intro WTRS'. - exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. - exploit transfer_use_def_satisf; eauto. intros [X Y]. - exploit eval_addressing_lessdef_none; eauto. intro Haddr. - exploit (exec_moves mv2); eauto. intros [ls2 [A2 B2]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_trans. eexact A1. - eapply star_left. eapply exec_Lload_notrap1. rewrite <- Haddr. - apply eval_addressing_preserved. exact symbols_preserved. eauto. - - eapply star_right. eexact A2. constructor. - eauto. eauto. eauto. traceEq. - exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. - econstructor; eauto. - -(* load notrap1 dead *) -- exploit exec_moves; eauto. intros [ls1 [X Y]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_right. eexact X. econstructor; eauto. - eauto. traceEq. - exploit satisf_successors. eauto. eauto. simpl; eauto. eauto. - eapply reg_unconstrained_satisf; eauto. - intros [enext [U V]]. - econstructor; eauto. - eapply wt_exec_Iload_notrap; eauto. - -(* load regular notrap2 *) -- generalize (wt_exec_Iload_notrap _ _ _ _ _ _ _ _ WTI WTRS). - intro WTRS'. - exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. - exploit transfer_use_def_satisf; eauto. intros [X Y]. - exploit eval_addressing_lessdef; eauto. intros [a' [F G]]. - destruct (Mem.loadv chunk m' a') as [v' |] eqn:Hload. - { exploit (exec_moves mv2 env (rs # dst <- Vundef)); eauto. intros [ls2 [A2 B2]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_trans. eexact A1. - eapply star_left. econstructor. instantiate (1 := a'). rewrite <- F. - apply eval_addressing_preserved. exact symbols_preserved. eauto. eauto. - eapply star_right. eexact A2. constructor. - eauto. eauto. eauto. traceEq. - exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. - econstructor; eauto. - } - { exploit (exec_moves mv2 env (rs # dst <- Vundef)); eauto. intros [ls2 [A2 B2]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_trans. eexact A1. - eapply star_left. eapply exec_Lload_notrap2. rewrite <- F. - apply eval_addressing_preserved. exact symbols_preserved. assumption. - eauto. - eapply star_right. eexact A2. constructor. - eauto. eauto. eauto. traceEq. - exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. - econstructor; eauto. - } - -- (* load notrap2 dead *) - exploit exec_moves; eauto. intros [ls1 [X Y]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_right. eexact X. econstructor; eauto. - eauto. traceEq. - exploit satisf_successors. eauto. eauto. simpl; eauto. eauto. - eapply reg_unconstrained_satisf; eauto. - intros [enext [U V]]. - econstructor; eauto. - eapply wt_exec_Iload_notrap; eauto. - -(* store *) -- exploit exec_moves; eauto. intros [ls1 [X Y]]. - exploit add_equations_lessdef; eauto. intros LD. simpl in LD. inv LD. - exploit eval_addressing_lessdef; eauto. intros [a' [F G]]. - exploit Mem.storev_extends; eauto. intros [m'' [P Q]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_trans. eexact X. - eapply star_two. econstructor. instantiate (1 := a'). rewrite <- F. - apply eval_addressing_preserved. exact symbols_preserved. eauto. eauto. - constructor. eauto. eauto. traceEq. - exploit satisf_successors; eauto. simpl; eauto. - eapply can_undef_satisf; eauto. eapply add_equations_satisf; eauto. intros [enext [U V]]. - econstructor; eauto. - -(* store 2 *) -- assert (SF: Archi.ptr64 = false) by (apply Archi.splitlong_ptr32; auto). - exploit Mem.storev_int64_split; eauto. - replace (if Archi.big_endian then Val.hiword rs#src else Val.loword rs#src) - with (sel_val kind_first_word rs#src) - by (unfold kind_first_word; destruct Archi.big_endian; reflexivity). - replace (if Archi.big_endian then Val.loword rs#src else Val.hiword rs#src) - with (sel_val kind_second_word rs#src) - by (unfold kind_second_word; destruct Archi.big_endian; reflexivity). - intros [m1 [STORE1 STORE2]]. - exploit (exec_moves mv1); eauto. intros [ls1 [X Y]]. - exploit add_equations_lessdef. eexact Heqo1. eexact Y. intros LD1. - exploit add_equation_lessdef. eapply add_equations_satisf. eexact Heqo1. eexact Y. - simpl. intros LD2. - set (ls2 := undef_regs (destroyed_by_store Mint32 addr) ls1). - assert (SAT2: satisf rs ls2 e1). - eapply can_undef_satisf. eauto. - eapply add_equation_satisf. eapply add_equations_satisf; eauto. - exploit eval_addressing_lessdef. eexact LD1. eauto. intros [a1' [F1 G1]]. - assert (F1': eval_addressing tge sp addr (reglist ls1 args1') = Some a1'). - rewrite <- F1. apply eval_addressing_preserved. exact symbols_preserved. - exploit Mem.storev_extends. eauto. eexact STORE1. eexact G1. eauto. - intros [m1' [STORE1' EXT1]]. - exploit (exec_moves mv2); eauto. intros [ls3 [U V]]. - exploit add_equations_lessdef. eexact Heqo. eexact V. intros LD3. - exploit add_equation_lessdef. eapply add_equations_satisf. eexact Heqo. eexact V. - simpl. intros LD4. - exploit eval_addressing_lessdef. eexact LD3. eauto. intros [a2' [F2 G2]]. - assert (F2': eval_addressing tge sp addr (reglist ls3 args2') = Some a2'). - rewrite <- F2. apply eval_addressing_preserved. exact symbols_preserved. - exploit (eval_offset_addressing tge); eauto. intros F2''. - assert (STOREX: exists m2', Mem.storev Mint32 m1' (Val.add a2' (Vint (Int.repr 4))) (ls3 (R src2')) = Some m2' /\ Mem.extends m' m2'). - { try discriminate; - (eapply Mem.storev_extends; - [eexact EXT1 | eexact STORE2 | apply Val.add_lessdef; [eexact G2|eauto] | eauto]). } - destruct STOREX as [m2' [STORE2' EXT2]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_trans. eexact X. - eapply star_left. - econstructor. eexact F1'. eexact STORE1'. instantiate (1 := ls2). auto. - eapply star_trans. eexact U. - eapply star_two. - eapply exec_Lstore with (m' := m2'). eexact F2''. discriminate||exact STORE2'. eauto. - constructor. eauto. eauto. eauto. eauto. traceEq. - exploit satisf_successors; eauto. simpl; eauto. - eapply can_undef_satisf. eauto. - eapply add_equation_satisf. eapply add_equations_satisf; eauto. - intros [enext [P Q]]. - econstructor; eauto. - -(* call *) -- set (sg := RTL.funsig fd) in *. - set (args' := loc_arguments sg) in *. - set (res' := loc_result sg) in *. - exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. - exploit find_function_translated. eauto. eauto. eapply add_equations_args_satisf; eauto. - intros [tfd [E F]]. - assert (SIG: funsig tfd = sg). eapply sig_function_translated; eauto. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_right. eexact A1. econstructor; eauto. - eauto. traceEq. - exploit analyze_successors; eauto. simpl. left; eauto. intros [enext [U V]]. - econstructor; eauto. - econstructor; eauto. - inv WTI. congruence. - intros. exploit (exec_moves mv2). eauto. eauto. - eapply function_return_satisf with (v := v) (ls_before := ls1) (ls_after := ls0); eauto. - eapply add_equation_ros_satisf; eauto. - eapply add_equations_args_satisf; eauto. - congruence. - apply wt_regset_assign; auto. - intros [ls2 [A2 B2]]. - exists ls2; split. - eapply star_right. eexact A2. constructor. traceEq. - apply satisf_incr with eafter; auto. - rewrite SIG. eapply add_equations_args_lessdef; eauto. - inv WTI. rewrite <- H7. apply wt_regset_list; auto. - simpl. red; auto. - inv WTI. rewrite SIG. rewrite <- H7. apply wt_regset_list; auto. - -(* tailcall *) -- set (sg := RTL.funsig fd) in *. - set (args' := loc_arguments sg) in *. - exploit Mem.free_parallel_extends; eauto. intros [m'' [P Q]]. - exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. - exploit find_function_translated. eauto. eauto. eapply add_equations_args_satisf; eauto. - intros [tfd [E F]]. - assert (SIG: funsig tfd = sg). eapply sig_function_translated; eauto. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_right. eexact A1. econstructor; eauto. - rewrite <- E. apply find_function_tailcall; auto. - replace (fn_stacksize tf) with (RTL.fn_stacksize f); eauto. - destruct (transf_function_inv _ _ FUN); auto. - eauto. traceEq. - econstructor; eauto. - eapply match_stackframes_change_sig; eauto. rewrite SIG. rewrite e0. decEq. - destruct (transf_function_inv _ _ FUN); auto. - rewrite SIG. rewrite return_regs_arg_values; auto. eapply add_equations_args_lessdef; eauto. - inv WTI. rewrite <- H6. apply wt_regset_list; auto. - apply return_regs_agree_callee_save. - rewrite SIG. inv WTI. rewrite <- H6. apply wt_regset_list; auto. - -(* builtin *) -- exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. - exploit add_equations_builtin_eval; eauto. - intros (C & vargs' & vres' & m'' & D & E & F & G). - assert (WTRS': wt_regset env (regmap_setres res vres rs)) by (eapply wt_exec_Ibuiltin; eauto). - set (ls2 := Locmap.setres res' vres' (undef_regs (destroyed_by_builtin ef) ls1)). - assert (satisf (regmap_setres res vres rs) ls2 e0). - { eapply parallel_set_builtin_res_satisf; eauto. - eapply can_undef_satisf; eauto. } - exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_trans. eexact A1. - eapply star_left. econstructor. - eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. - eapply external_call_symbols_preserved. apply senv_preserved. eauto. - instantiate (1 := ls2); auto. - eapply star_right. eexact A3. - econstructor. - reflexivity. reflexivity. reflexivity. traceEq. - exploit satisf_successors; eauto. simpl; eauto. - intros [enext [U V]]. - econstructor; eauto. - -(* cond *) -- exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_right. eexact A1. - econstructor. eapply eval_condition_lessdef; eauto. eapply add_equations_lessdef; eauto. - eauto. eauto. eauto. traceEq. - exploit satisf_successors; eauto. - instantiate (1 := if b then ifso else ifnot). simpl. destruct b; auto. - eapply can_undef_satisf. eauto. eapply add_equations_satisf; eauto. - intros [enext [U V]]. - econstructor; eauto. - -(* jumptable *) -- exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. - assert (Val.lessdef (Vint n) (ls1 (R arg'))). - rewrite <- H0. eapply add_equation_lessdef with (q := Eq Full arg (R arg')); eauto. - inv H2. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_right. eexact A1. - econstructor. eauto. eauto. eauto. eauto. traceEq. - exploit satisf_successors; eauto. - instantiate (1 := pc'). simpl. eapply list_nth_z_in; eauto. - eapply can_undef_satisf. eauto. eapply add_equation_satisf; eauto. - intros [enext [U V]]. - econstructor; eauto. - -(* return *) -- destruct (transf_function_inv _ _ FUN). - exploit Mem.free_parallel_extends; eauto. rewrite H10. intros [m'' [P Q]]. - inv WTI; MonadInv. -+ (* without an argument *) - exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_right. eexact A1. - econstructor. eauto. eauto. traceEq. - simpl. econstructor; eauto. - apply return_regs_agree_callee_save. - constructor. -+ (* with an argument *) - exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_right. eexact A1. - econstructor. eauto. eauto. traceEq. - simpl. econstructor; eauto. rewrite <- H11. - replace (Locmap.getpair (map_rpair R (loc_result (RTL.fn_sig f))) - (return_regs (parent_locset ts) ls1)) - with (Locmap.getpair (map_rpair R (loc_result (RTL.fn_sig f))) ls1). - eapply add_equations_res_lessdef; eauto. - rewrite <- H14. apply WTRS. - 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. - apply return_regs_agree_callee_save. - rewrite <- H11, <- H14. apply WTRS. - -(* internal function *) -- monadInv FUN. simpl in *. - destruct (transf_function_inv _ _ EQ). - exploit Mem.alloc_extends; eauto. apply Z.le_refl. rewrite H8; apply Z.le_refl. - intros [m'' [U V]]. - assert (WTRS: wt_regset env (init_regs args (fn_params f))). - { apply wt_init_regs. inv H0. rewrite wt_params. rewrite H9. auto. } - exploit (exec_moves mv). eauto. eauto. - eapply can_undef_satisf; eauto. eapply compat_entry_satisf; eauto. - rewrite call_regs_param_values. eexact ARGS. - exact WTRS. - intros [ls1 [A B]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_left. econstructor; eauto. - eapply star_right. eexact A. - econstructor; eauto. - eauto. eauto. traceEq. - econstructor; eauto. - -(* external function *) -- exploit external_call_mem_extends; eauto. intros [v' [m'' [F [G [J K]]]]]. - simpl in FUN; inv FUN. - econstructor; split. - apply plus_one. econstructor; eauto. - eapply external_call_symbols_preserved with (ge1 := ge); eauto. apply senv_preserved. - 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). - assert (WTRES': Val.has_type v' Tlong). - { rewrite <- B. eapply external_call_well_typed; eauto. } - 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). - rewrite locmap_get_set_loc_result_callee_save by auto. - unfold undef_caller_save_regs. destruct l; simpl in H0. - rewrite H0; auto. - destruct sl; auto; congruence. - eapply external_call_well_typed; eauto. - -(* return *) -- inv STACKS. - exploit STEPS; eauto. rewrite WTRES0; auto. intros [ls2 [A B]]. - econstructor; split. - eapply plus_left. constructor. eexact A. traceEq. - econstructor; eauto. - apply wt_regset_assign; auto. rewrite WTRES0; auto. -Qed. - -Lemma initial_states_simulation: - forall st1, RTL.initial_state prog st1 -> - exists st2, LTL.initial_state tprog st2 /\ match_states st1 st2. -Proof. - intros. inv H. - exploit function_ptr_translated; eauto. intros [tf [FIND TR]]. - exploit sig_function_translated; eauto. intros SIG. - exists (LTL.Callstate nil tf (Locmap.init Vundef) m0); split. - econstructor; eauto. - eapply (Genv.init_mem_transf_partial TRANSF); eauto. - rewrite symbols_preserved. - rewrite (match_program_main TRANSF). auto. - congruence. - constructor; auto. - constructor. rewrite SIG; rewrite H3; auto. - rewrite SIG, H3, loc_arguments_main. auto. - red; auto. - apply Mem.extends_refl. - rewrite SIG, H3. constructor. -Qed. - -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. - econstructor. rewrite <- (loc_result_exten sg). inv RES; auto. - rewrite H; auto. -Qed. - -Lemma wt_prog: wt_program prog. -Proof. - red; intros. - exploit list_forall2_in_left. eexact (proj1 TRANSF). eauto. - intros ([i' gd] & A & B & C). simpl in *; subst i'. - inv C. destruct f; simpl in *. -- monadInv H2. - unfold transf_function in EQ. - destruct (type_function f) as [env|] eqn:TF; try discriminate. - econstructor. eapply type_function_correct; eauto. -- constructor. -Qed. - -Theorem transf_program_correct: - forward_simulation (RTL.semantics prog) (LTL.semantics tprog). -Proof. - set (ms := fun s s' => wt_state s /\ match_states s s'). - eapply forward_simulation_plus with (match_states := ms). -- apply senv_preserved. -- intros. exploit initial_states_simulation; eauto. intros [st2 [A B]]. - exists st2; split; auto. split; auto. - apply wt_initial_state with (p := prog); auto. exact wt_prog. -- intros. destruct H. eapply final_states_simulation; eauto. -- intros. destruct H0. - exploit step_simulation; eauto. intros [s2' [A B]]. - exists s2'; split. exact A. split. - eapply subject_reduction; eauto. eexact wt_prog. eexact H. - auto. -Qed. - -End PRESERVATION. diff --git a/backend/Tunneling.v b/backend/Tunneling.v index a4c4a195..78458582 100644 --- a/backend/Tunneling.v +++ b/backend/Tunneling.v @@ -101,5 +101,5 @@ Definition tunnel_function (f: LTL.function) : LTL.function := Definition tunnel_fundef (f: LTL.fundef) : LTL.fundef := transf_fundef tunnel_function f. -Definition tunnel_program (p: LTL.program) : LTL.program := +Definition transf_program (p: LTL.program) : LTL.program := transform_program tunnel_fundef p. diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index d3b8a9f0..cdf6c800 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -22,7 +22,7 @@ Definition match_prog (p tp: program) := match_program (fun ctx f tf => tf = tunnel_fundef f) eq p tp. Lemma transf_program_match: - forall p, match_prog p (tunnel_program p). + forall p, match_prog p (transf_program p). Proof. intros. eapply match_transform_program; eauto. Qed. diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand index c044d9ef..17b504b7 100644 --- a/driver/Compiler.vexpand +++ b/driver/Compiler.vexpand @@ -36,12 +36,6 @@ Require Cminorgen. Require Selection. Require RTLgen. EXPAND_RTL_REQUIRE -Require Allocation. -Require Tunneling. -Require Linearize. -Require CleanupLabels. -Require Debugvar. -Require Stacking. Require Asmgen. (** Proofs of semantic preservation. *) Require SimplExprproof. @@ -51,12 +45,6 @@ Require Cminorgenproof. Require Selectionproof. Require RTLgenproof. EXPAND_RTL_REQUIRE_PROOF -Require Allocproof. -Require Tunnelingproof. -Require Linearizeproof. -Require CleanupLabelsproof. -Require Debugvarproof. -Require Stackingproof. Require Import Asmgenproof. (** Command-line flags. *) Require Import Compopts. @@ -109,16 +97,8 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := OK f @@ print (print_RTL 0) EXPAND_RTL_TRANSF_PROGRAM - @@@ time "Register allocation" Allocation.transf_program - @@ print print_LTL - @@ time "Branch tunneling" Tunneling.tunnel_program - @@@ time "CFG linearization" Linearize.transf_program - @@ time "Label cleanup" CleanupLabels.transf_program - @@@ partial_if Compopts.debug (time "Debugging info for local variables" Debugvar.transf_program) - @@@ time "Mach generation" Stacking.transf_program - @@ print print_Mach @@@ time "Total Mach->Asm generation" Asmgen.transf_program. - + Definition transf_cminor_program (p: Cminor.program) : res Asm.program := OK p @@ print print_Cminor @@ -209,12 +189,6 @@ Definition CompCert's_passes := ::: mkpass Selectionproof.match_prog ::: mkpass RTLgenproof.match_prog EXPAND_RTL_MKPASS - ::: mkpass Allocproof.match_prog - ::: mkpass Tunnelingproof.match_prog - ::: mkpass Linearizeproof.match_prog - ::: mkpass CleanupLabelsproof.match_prog - ::: mkpass (match_if Compopts.debug Debugvarproof.match_prog) - ::: mkpass Stackingproof.match_prog ::: mkpass Asmgenproof.match_prog ::: pass_nil _. @@ -244,30 +218,7 @@ Proof. destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. simpl in T. - set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. - destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. - set (p8bis := total_if profile_arcs Profiling.transf_program p8) in *. - set (p8ter := total_if branch_probabilities ProfilingExploit.transf_program p8bis) in *. - set (p9 := total_if Compopts.optim_move_loop_invariants FirstNop.transf_program p8ter) in *. - set (p9bis := Renumber.transf_program p9) in *. - destruct (partial_if optim_duplicate Duplicate.transf_program p9bis) as [p10|e] eqn:P10; simpl in T; try discriminate. - set (p11 := Renumber.transf_program p10) in *. - set (p12 := total_if optim_constprop Constprop.transf_program p11) in *. - destruct (partial_if optim_move_loop_invariants LICM.transf_program p12) as [p12bis|e] eqn:P12bis; simpl in T; try discriminate. - set (p12ter :=(total_if optim_move_loop_invariants Renumber.transf_program p12bis)) in *. - destruct (partial_if optim_CSE CSE.transf_program p12ter) as [p13|e] eqn:P13; simpl in T; try discriminate. - set (p13bis := total_if optim_CSE2 CSE2.transf_program p13) in *. - destruct (partial_if optim_CSE3 CSE3.transf_program p13bis) as [p13ter|e] eqn:P13ter; simpl in T; try discriminate. - set (p13quater := total_if optim_forward_moves ForwardMoves.transf_program p13ter) in *. - destruct (partial_if optim_redundancy Deadcode.transf_program p13quater) as [p14|e] eqn:P14; simpl in T; try discriminate. - set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. - destruct (Unusedglob.transf_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. - destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate. - set (p17 := Tunneling.tunnel_program p16) in *. - destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; simpl in T; try discriminate. - set (p19 := CleanupLabels.transf_program p18) in *. - destruct (partial_if debug Debugvar.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate. - destruct (Stacking.transf_program p20) as [p21|e] eqn:P21; simpl in T; try discriminate. +EXPAND_RTL_PROOF unfold match_prog; simpl. exists p1; split. apply SimplExprproof.transf_program_match; auto. exists p2; split. apply SimplLocalsproof.match_transf_program; auto. @@ -275,30 +226,7 @@ Proof. exists p4; split. apply Cminorgenproof.transf_program_match; auto. exists p5; split. apply Selectionproof.transf_program_match; auto. exists p6; split. apply RTLgenproof.transf_program_match; auto. - exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match. - exists p8; split. apply Inliningproof.transf_program_match; auto. - exists p8bis; split. apply total_if_match. apply Profilingproof.transf_program_match; auto. - exists p8ter; split. apply total_if_match. apply ProfilingExploitproof.transf_program_match; auto. - exists p9; split. apply total_if_match. apply FirstNopproof.transf_program_match. - exists p9bis; split. apply Renumberproof.transf_program_match. - exists p10; split. eapply partial_if_match; eauto. apply Duplicateproof.transf_program_match; auto. - exists p11; split. apply Renumberproof.transf_program_match. - exists p12; split. apply total_if_match. apply Constpropproof.transf_program_match. - exists p12bis; split. eapply partial_if_match; eauto. apply LICMproof.transf_program_match. - exists p12ter; split. apply total_if_match; eauto. apply Renumberproof.transf_program_match. - exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. - exists p13bis; split. apply total_if_match. apply CSE2proof.transf_program_match. - exists p13ter; split. eapply partial_if_match; eauto. apply CSE3proof.transf_program_match. - exists p13quater; split. eapply total_if_match; eauto. apply ForwardMovesproof.transf_program_match. - exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. - exists p14bis; split. eapply total_if_match; eauto. apply Allnontrapproof.transf_program_match. - exists p15; split. apply Unusedglobproof.transf_program_match; auto. - exists p16; split. apply Allocproof.transf_program_match; auto. - exists p17; split. apply Tunnelingproof.transf_program_match. - exists p18; split. apply Linearizeproof.transf_program_match; auto. - exists p19; split. apply CleanupLabelsproof.transf_program_match; auto. - exists p20; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match. - exists p21; split. apply Stackingproof.transf_program_match; auto. +EXPAND_RTL_PROOF2 exists tp; split. apply Asmgenproof.transf_program_match; auto. reflexivity. Qed. @@ -350,7 +278,9 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p31)). + assert (F: forward_simulation (Cstrategy.semantics p) +EXPAND_ASM_SEMANTICS + ). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -364,42 +294,9 @@ Ltac DestructM := eapply Selectionproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply RTLgenproof.transf_program_correct; eassumption. +EXPAND_RTL_FORWARD_SIMULATIONS eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Tailcallproof.transf_program_correct. - eapply compose_forward_simulations. - eapply Inliningproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Profilingproof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact ProfilingExploitproof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact FirstNopproof.transf_program_correct. - eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Duplicateproof.transf_program_correct. - eapply compose_forward_simulations. - eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. - eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact LICMproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Renumberproof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact CSEproof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact CSE2proof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact CSE3proof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact ForwardMovesproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Allnontrapproof.transf_program_correct. - eapply compose_forward_simulations. - eapply Unusedglobproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply Allocproof.transf_program_correct; eassumption. + eapply Allocationproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Tunnelingproof.transf_program_correct; eassumption. eapply compose_forward_simulations. diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml index 1ef233e7..1555d75b 100644 --- a/tools/compiler_expand.ml +++ b/tools/compiler_expand.ml @@ -1,4 +1,5 @@ type is_partial = TOTAL | PARTIAL;; +type print_result = Noprint | Print of string;; type when_triggered = Always | Option of string;; let rtl_passes = @@ -23,21 +24,38 @@ TOTAL, (Option "all_loads_nontrap"), None, "Allnontrap"; PARTIAL, Always, (Some "Unused globals"), "Unusedglob" |];; +let post_rtl_passes = +[| + PARTIAL, Always, (Some "Register allocation"), "Allocation", (Print "LTL"); + TOTAL, Always, (Some "Branch tunneling"), "Tunneling", Noprint; + PARTIAL, Always, (Some "CFG linearization"), "Linearize", Noprint; + TOTAL, Always, (Some "Label cleanup"), "CleanupLabels", Noprint; + PARTIAL, (Option "debug"), (Some "Debugging info for local variables"), "Debugvar", Noprint; + PARTIAL, Always, (Some "Mach generation"), "Stacking", (Print "Mach") +|];; + +let all_passes = + Array.concat + [Array.mapi + (fun i (a,b,c,d) -> (a,b,c,d, Print (Printf.sprintf "RTL %d" (i+1)))) + rtl_passes; + post_rtl_passes];; + let totality = function TOTAL -> "total" | PARTIAL -> "partial";; let print_rtl_require oc = - Array.iter (fun (partial, trigger, time_label, pass_name) -> + Array.iter (fun (partial, trigger, time_label, pass_name, printing) -> Printf.fprintf oc "Require %s.\n" pass_name) - rtl_passes;; + all_passes;; let print_rtl_require_proof oc = - Array.iter (fun (partial, trigger, time_label, pass_name) -> + Array.iter (fun (partial, trigger, time_label, pass_name, printing) -> Printf.fprintf oc "Require %sproof.\n" pass_name) - rtl_passes;; + all_passes;; let print_rtl_transf oc = Array.iteri - (fun i (partial, trigger, time_label, pass_name) -> + (fun i (partial, trigger, time_label, pass_name, printing) -> output_string oc (match partial with | TOTAL -> " @@ " | PARTIAL -> " @@@ "); @@ -51,17 +69,61 @@ let print_rtl_transf oc = | Some s -> Printf.fprintf oc "time \"%s\" " s); Printf.fprintf oc "%s.transf_program)\n" pass_name; - Printf.fprintf oc " @@ print (print_RTL %d)\n" (succ i) - ) rtl_passes;; + (match printing with + | Noprint -> () + | Print s -> + Printf.fprintf oc " @@ print (print_%s)\n" s) + ) all_passes;; let print_rtl_mkpass oc = - Array.iter (fun (partial, trigger, time_label, pass_name) -> + Array.iter (fun (partial, trigger, time_label, pass_name, printing) -> output_string oc " ::: mkpass ("; (match trigger with | Always -> () | Option s -> Printf.fprintf oc "match_if Compopts.%s " s); Printf.fprintf oc "%sproof.match_prog)\n" pass_name) + all_passes;; + +let print_if kind oc = function + | Always -> () + | Option s -> Printf.fprintf oc "%s_if %s " kind s;; + +let numbering_base = 7 + +let print_rtl_proof oc = + Array.iteri (fun i (partial, trigger, time_label, pass_name, printing) -> + let j = i+numbering_base in + match partial with + | TOTAL -> + Printf.fprintf oc "set (p%d := %a%s.transf_program p%d) in *.\n" + j (print_if "total") trigger pass_name (pred j) + | PARTIAL -> + Printf.fprintf oc "destruct (%a%s.transf_program p%d) as [p%d|e] eqn:P%d; simpl in T; try discriminate.\n" + (print_if "partial") trigger pass_name (pred j) j j) + all_passes;; + +let print_rtl_proof2 oc = + Array.iteri (fun i (partial, trigger, time_label, pass_name, printing) -> + let j = i+numbering_base in + Printf.fprintf oc " exists p%d; split. " j; + (match trigger with + | Always -> () + | Option _ -> + (match partial with + | TOTAL -> output_string oc "apply total_if_match. " + | PARTIAL -> output_string oc "eapply partial_if_match; eauto. ")); + Printf.fprintf oc "apply %sproof.transf_program_match; auto.\n" pass_name) + all_passes;; + +let print_rtl_forward_simulations oc = + Array.iter (fun (partial, trigger, time_label, pass_name) -> + output_string oc " eapply compose_forward_simulations.\n "; + (match trigger with + | Always -> () + | Option s -> output_string oc "eapply match_if_simulation. eassumption. "); + Printf.fprintf oc "eapply %sproof.transf_program_correct; eassumption." pass_name + ) rtl_passes;; if (Array.length Sys.argv)<>3 @@ -81,6 +143,15 @@ let filename_in = Sys.argv.(1) and filename_out = Sys.argv.(2) in print_rtl_require_proof oc | "EXPAND_RTL_MKPASS" -> print_rtl_mkpass oc + | "EXPAND_RTL_PROOF" -> + print_rtl_proof oc + | "EXPAND_RTL_PROOF2" -> + print_rtl_proof2 oc + | "EXPAND_ASM_SEMANTICS" -> + Printf.fprintf oc " (Asm.semantics p%d)\n" + ((Array.length all_passes) + 7) + | "EXPAND_RTL_FORWARD_SIMULATIONS" -> + print_rtl_forward_simulations oc | line -> (output_string oc line; output_char oc '\n') done -- cgit