Require Import FSets.
Require Archi.
Require Import Coqlib.
Require Import Ordered.
Require Import Errors.
Require Import Maps.
Require Import Lattice.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Op.
Require Import Registers.
Require Import RTL.
Require Import RTLtyping.
Require Import Kildall.
Require Import Locations.
Require Import Conventions.
Require Import LTL.
Require Import Allocation.
Require Import Annotations.

Soundness of structural checks

Definition expand_move (sd: loc * loc) : instruction :=
  match sd with
  | (R src, R dst) => Lop Omove (src::nil) dst
  | (S sl ofs ty, R dst) => Lgetstack sl ofs ty dst
  | (R src, S sl ofs ty) => Lsetstack src sl ofs ty
  | (S _ _ _, S _ _ _) => Lreturn (* should never happen *)
  end.

Definition expand_moves (mv: moves) (k: bblock) : bblock :=
  List.map expand_move mv ++ k.

Definition wf_move (sd: loc * loc) : Prop :=
  match sd with
  | (S _ _ _, S _ _ _) => False
  | _ => True
  end.

Definition wf_moves (mv: moves) : Prop :=
  forall sd, In sd mv -> wf_move sd.

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 ->
      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 ->
      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 ->
      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 alpha chunk addr args dst mv1 args' dst' mv2 s k,
      wf_moves mv1 -> wf_moves mv2 ->
      expand_block_shape (BSload alpha chunk addr args dst mv1 args' dst' mv2 s)
                         (Iload alpha chunk addr args dst s)
                         (expand_moves mv1
                           (Lload alpha chunk addr args' dst' :: expand_moves mv2 (Lbranch s :: k)))
  | ebs_load2: forall alpha alpha2 addr addr2 args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s k,
      wf_moves mv1 -> wf_moves mv2 -> wf_moves mv3 ->
      offset_addressing addr (Int.repr 4) = Some addr2 ->
      offset_annotation alpha (Int.repr 4) = alpha2 ->
      (forall depth varname base bound, In (ABlocal depth varname (base, bound)) (snd alpha) -> Int.unsigned base < Int.max_unsigned - 4 /\ Int.unsigned bound < Int.max_unsigned - 4) ->
      (forall id base bound, In (ABglobal id (base, bound)) (snd alpha) -> Int.unsigned base < Int.max_unsigned - 4 /\ Int.unsigned bound < Int.max_unsigned - 4) ->
      expand_block_shape (BSload2 alpha alpha2 addr addr2 args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s)
                         (Iload alpha Mint64 addr args dst s)
                         (expand_moves mv1
                           (Lload alpha Mint32 addr args1' dst1' ::
                           expand_moves mv2
                             (Lload alpha2 Mint32 addr2 args2' dst2' ::
                              expand_moves mv3 (Lbranch s :: k))))
  | ebs_load2_1: forall alpha addr args dst mv1 args' dst' mv2 s k,
      wf_moves mv1 -> wf_moves mv2 ->
      expand_block_shape (BSload2_1 alpha addr args dst mv1 args' dst' mv2 s)
                         (Iload alpha Mint64 addr args dst s)
                         (expand_moves mv1
                           (Lload alpha Mint32 addr args' dst' ::
                            expand_moves mv2 (Lbranch s :: k)))
  | ebs_load2_2: forall alpha alpha2 addr addr2 args dst mv1 args' dst' mv2 s k,
      wf_moves mv1 -> wf_moves mv2 ->
      offset_addressing addr (Int.repr 4) = Some addr2 ->
      offset_annotation alpha (Int.repr 4) = alpha2 ->
      (forall depth varname base bound, In (ABlocal depth varname (base, bound)) (snd alpha) -> Int.unsigned base < Int.max_unsigned - 4 /\ Int.unsigned bound < Int.max_unsigned - 4) ->
      (forall id base bound, In (ABglobal id (base, bound)) (snd alpha) -> Int.unsigned base < Int.max_unsigned - 4 /\ Int.unsigned bound < Int.max_unsigned - 4) ->
      expand_block_shape (BSload2_2 alpha alpha2 addr addr2 args dst mv1 args' dst' mv2 s)
                         (Iload alpha Mint64 addr args dst s)
                         (expand_moves mv1
                           (Lload alpha2 Mint32 addr2 args' dst' ::
                            expand_moves mv2 (Lbranch s :: k)))
  | ebs_load_dead: forall alpha chunk addr args dst mv s k,
      wf_moves mv ->
      expand_block_shape (BSloaddead alpha chunk addr args dst mv s)
                         (Iload alpha chunk addr args dst s)
                         (expand_moves mv (Lbranch s :: k))
  | ebs_store: forall alpha chunk addr args src mv1 args' src' s k,
      wf_moves mv1 ->
      expand_block_shape (BSstore alpha chunk addr args src mv1 args' src' s)
                         (Istore alpha chunk addr args src s)
                         (expand_moves mv1
                           (Lstore alpha chunk addr args' src' :: Lbranch s :: k))
  | ebs_store2: forall alpha alpha2 addr addr2 args src mv1 args1' src1' mv2 args2' src2' s k,
      wf_moves mv1 -> wf_moves mv2 ->
      offset_addressing addr (Int.repr 4) = Some addr2 ->
      offset_annotation alpha (Int.repr 4) = alpha2 ->
      (forall depth varname base bound, In (ABlocal depth varname (base, bound)) (snd alpha) -> Int.unsigned base < Int.max_unsigned - 4 /\ Int.unsigned bound < Int.max_unsigned - 4) ->
      (forall id base bound, In (ABglobal id (base, bound)) (snd alpha) -> Int.unsigned base < Int.max_unsigned - 4 /\ Int.unsigned bound < Int.max_unsigned - 4) ->
      expand_block_shape (BSstore2 alpha alpha2 addr addr2 args src mv1 args1' src1' mv2 args2' src2' s)
                         (Istore alpha Mint64 addr args src s)
                         (expand_moves mv1
                           (Lstore alpha Mint32 addr args1' src1' ::
                            expand_moves mv2
                             (Lstore alpha2 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,
      wf_moves mv ->
      expand_block_shape (BScond cond args mv args' s1 s2)
                         (Icond cond args s1 s2)
                         (expand_moves mv (Lcond cond args' s1 s2 :: 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; [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.

Lemma extract_moves_sound:
  forall b mv b',
  extract_moves nil b = (mv, b') ->
  wf_moves mv /\ b = expand_moves mv b'.

Lemma check_succ_sound:
  forall s b, check_succ s b = true -> exists k, b = Lbranch s :: k.

Ltac UseParsingLemmas :=
  match goal with
  | [ H: extract_moves nil _ = (_, _) |- _ ] =>
      destruct (extract_moves_sound _ _ _ H); clear H; subst; UseParsingLemmas
  | [ H: check_succ _ _ = true |- _ ] =>
      try discriminate;
      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.

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.

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.


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.

Lemma satisf_incr:
  forall rs ls (e1 e2: eqs),
  satisf rs ls e2 -> EqSet.Subset e1 e2 -> satisf rs ls e1.

Lemma satisf_undef_reg:
  forall rs ls e r,
  satisf rs ls e ->
  satisf (rs#r <- Vundef) ls e.

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)).

Lemma add_equation_satisf:
  forall rs ls q e,
  satisf rs ls (add_equation q e) -> satisf rs ls e.

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.

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).

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.

Lemma val_longofwords_eq:
  forall v,
  Val.has_type v Tlong ->
  Val.longofwords (Val.hiword v) (Val.loword v) = v.

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) (decode_longs tyl (map ls ll)).

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.

Lemma remove_equation_satisf:
  forall rs ls q e,
  satisf rs ls e -> satisf rs ls (remove_equation q e).

Lemma remove_equation_res_satisf:
  forall rs ls r oty ll e e',
  remove_equations_res r oty ll e = Some e' ->
  satisf rs ls e -> satisf rs ls e'.

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.

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.

Remark select_reg_charact:
  forall r q, select_reg_l r q = true /\ select_reg_h r q = true <-> ereg q = r.

Lemma reg_unconstrained_sound:
  forall r e q,
  reg_unconstrained r e = true ->
  EqSet.In q e ->
  ereg q <> r.

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.

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.

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.

Remark select_loc_charact:
  forall l q,
  select_loc_l l q = false \/ select_loc_h l q = false <-> Loc.diff l (eloc q).

Lemma loc_unconstrained_sound:
  forall l e q,
  loc_unconstrained l e = true ->
  EqSet.In q e ->
  Loc.diff l (eloc q).

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.

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).

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.

Lemma parallel_assignment_satisf_2:
  forall rs ls res mres' oty e e' v v',
  let res' := map R mres' in
  remove_equations_res res oty res' e = Some e' ->
  satisf rs ls e' ->
  reg_unconstrained res e' = true ->
  forallb (fun l => loc_unconstrained l e') res' = true ->
  Val.lessdef v v' ->
  satisf (rs#res <- v) (Locmap.setlist res' (encode_long oty v') ls) e.

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).

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.

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).

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.

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.

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.

Module ESF2 := FSetFacts.Facts(EqSet2).
Module ESP2 := FSetProperties.Properties(EqSet2).
Module ESD2 := FSetDecide.Decide(EqSet2).

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').

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).

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.

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').

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.

Lemma can_undef_sound:
  forall e ml q,
  can_undef ml e = true -> EqSet.In q e -> Loc.notin (eloc q) (map R ml).

Lemma undef_regs_outside:
  forall ml ls l,
  Loc.notin l (map R ml) -> undef_regs ml ls l = ls l.

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.

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).

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.

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).

Lemma add_equations_res_lessdef:
  forall r oty ll e e' rs ls,
  add_equations_res r oty ll e = Some e' ->
  satisf rs ls e' ->
  Val.lessdef_list (encode_long oty rs#r) (map ls ll).

Definition callee_save_loc (l: loc) :=
  match l with
  | R r => ~(In r destroyed_at_call)
  | S sl ofs ty => sl <> Outgoing
  end.

Definition agree_callee_save (ls1 ls2: locset) : Prop :=
  forall l, callee_save_loc l -> ls1 l = ls2 l.

Lemma return_regs_agree_callee_save:
  forall caller callee,
  agree_callee_save caller (return_regs caller callee).

Lemma no_caller_saves_sound:
  forall e q,
  no_caller_saves e = true ->
  EqSet.In q e ->
  callee_save_loc (eloc q).

Lemma function_return_satisf:
  forall rs ls_before ls_after res res' sg e e' v,
  res' = map R (loc_result sg) ->
  remove_equations_res res (sig_res sg) res' e = Some e' ->
  satisf rs ls_before e' ->
  forallb (fun l => reg_loc_unconstrained res l e') res' = true ->
  no_caller_saves e' = true ->
  Val.lessdef_list (encode_long (sig_res sg) v) (map ls_after res') ->
  agree_callee_save ls_before ls_after ->
  satisf (rs#res <- v) ls_after e.

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.

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).

Lemma val_hiword_longofwords:
  forall v1 v2, Val.lessdef (Val.hiword (Val.longofwords v1 v2)) v1.

Lemma val_loword_longofwords:
  forall v1 v2, Val.lessdef (Val.loword (Val.longofwords v1 v2)) v2.

Lemma compat_entry_satisf:
  forall rl tyl ll e,
  compat_entry rl tyl ll e = true ->
  forall vl ls,
  Val.lessdef_list vl (decode_longs tyl (map ls ll)) ->
  satisf (init_regs vl rl) ls e.

Lemma call_regs_param_values:
  forall sg ls,
  map (call_regs ls) (loc_parameters sg) = map ls (loc_arguments sg).

Lemma return_regs_arg_values:
  forall sg ls1 ls2,
  tailcall_is_possible sg = true ->
  map (return_regs ls1 ls2) (loc_arguments sg) = map ls2 (loc_arguments sg).

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.

Lemma loadv_int64_split:
  forall m a v,
  Mem.loadv Mint64 m a = Some v ->
  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.

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.

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'.

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.

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'.

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.

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'.

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'.

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.

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.

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'.


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) (sig_args (RTL.fn_sig 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.

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.

Semantic preservation

Section PRESERVATION.

Variable prog: RTL.program.
Variable tprog: LTL.program.
Hypothesis TRANSF: transf_program prog = OK 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.

Lemma public_preserved:
  forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s.

Lemma varinfo_preserved:
  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.

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_fundef _ 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_fundef _ TRANSF).

Lemma sig_function_translated:
  forall f tf,
  transf_fundef f = OK tf ->
  LTL.funsig tf = RTL.funsig f.

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.

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.

Lemma exec_moves_safe:
  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_safe tge (Block s f sp (expand_moves mv bb) ls m)
                    E0 (Block s f sp bb ls' m)
  /\ satisf rs ls' e.


Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> signature -> Prop :=
  | match_stackframes_nil: forall sg,
      sg.(sig_res) = Some 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_list (encode_long (sig_res sg) v) (map ls1 (map R (loc_result sg))) ->
           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 (decode_longs (sig_args (funsig tf)) (map 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_list (encode_long (sig_res sg) res) (map ls (map R (loc_result sg))))
        (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').

Inductive match_stackframes': list RTL.stackframe -> list LTL.stackframe -> signature -> Prop :=
  | match_stackframes_nil': forall sg,
      sg.(sig_res) = Some 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_list (encode_long (sig_res sg) v) (map ls1 (map R (loc_result sg))) ->
           Val.has_type v (env res) ->
           agree_callee_save ls ls1 ->
           exists ls2,
           star LTL.step_safe 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 (decode_longs (sig_args (funsig tf)) (map 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_list (encode_long (sig_res sg) res) (map ls (map R (loc_result sg))))
        (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'.

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'.

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 env f alpha addr args dst s r,
  wt_instr f env (Iload alpha Mint64 addr args dst s) ->
  In r args -> r <> dst.


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'.

Lemma initial_states_simulation:
  forall st1, RTL.initial_state prog st1 ->
  exists st2, LTL.initial_state tprog st2 /\ match_states st1 st2.

Lemma final_states_simulation:
  forall st1 st2 r,
  match_states st1 st2 -> RTL.final_state st1 r -> LTL.final_state st2 r.

Lemma wt_prog: wt_program prog.

Theorem transf_program_correct:
  forward_simulation (RTL.semantics prog) (LTL.semantics tprog).

Lemma match_stackframes_implies_same_sp':
  forall s ts sig,
    match_stackframes' s ts sig ->
    List.map (fun s => match s with | RTL.Stackframe _ _ sp _ _ => sp end) s = List.map (fun s => match s with Stackframe _ sp _ _ => sp end) ts.

Lemma initial_states_simulation':
  forall st1, RTL.initial_state prog st1 ->
  exists st2, LTL.initial_state tprog st2 /\ match_states' st1 st2.

Lemma final_states_simulation':
  forall st1 st2 r,
  match_states' st1 st2 -> RTL.final_state st1 r -> LTL.final_state st2 r.

Lemma annot_sem_offset:
  forall find_symbol sps alpha a ofs,
  annot_sem find_symbol sps alpha a ->
  (forall depth varname base bound, In (ABlocal depth varname (base, bound)) alpha -> Int.unsigned base < Int.max_unsigned - Int.unsigned ofs /\ Int.unsigned bound < Int.max_unsigned - Int.unsigned ofs) ->
  (forall id base bound, In (ABglobal id (base, bound)) alpha -> Int.unsigned base < Int.max_unsigned - Int.unsigned ofs /\ Int.unsigned bound < Int.max_unsigned - Int.unsigned ofs) ->
  annot_sem find_symbol sps (map (fun x => offset_ablock x ofs) alpha) (Val.add a (Vint ofs)).
  
Lemma step_simulation':
  forall S1 t S2, RTL.step_safe ge S1 t S2 -> wt_state S1 ->
  forall S1', match_states' S1 S1' ->
  exists S2', plus LTL.step_safe tge S1' t S2' /\ match_states' S2 S2'.


Theorem transf_program_safe_correct:
  forward_simulation (RTL.semantics_safe prog) (LTL.semantics_safe tprog).
  
End PRESERVATION.