Module Stackingtyping

Type preservation for the Stacking pass.

Require Import Coqlib.
Require Import Maps.
Require Import Errors.
Require Import Integers.
Require Import Ast.
Require Import Op.
Require Import Locations.
Require Import Conventions.
Require Import Linear.
Require Import Lineartyping.
Require Import Mach.
Require Import Machtyping.
Require Import Bounds.
Require Import Stacklayout.
Require Import Stacking.
Require Import Stackingproof.

We show that the Mach code generated by the Stacking pass is well-typed if the original LTLin code is.

Definition wt_instrs (k: Mach.code) : Prop :=
  forall i, In i k -> wt_instr i.

Lemma wt_instrs_cons:
  forall i k,
  wt_instr i -> wt_instrs k -> wt_instrs (i :: k).

Proof.

unfold wt_instrs; intros. elim H1; intro.
subst i0; auto. auto.
Qed.

Section TRANSL_FUNCTION.

Variable f: Linear.function.
Let fe := make_env (function_bounds f).
Variable tf: Mach.function.
Hypothesis TRANSF_F: transf_function f = OK tf.

Lemma wt_fold_right:
  forall (A: Type) (f: A -> code -> code) (k: code) (l: list A),
  (forall x k', In x l -> wt_instrs k' -> wt_instrs (f x k')) ->
  wt_instrs k ->
  wt_instrs (List.fold_right f k l).

Proof.

  induction l; intros; simpl.
  auto.
  apply H. apply in_eq. apply IHl.
  intros. apply H. auto with coqlib. auto.
  auto.
Qed.

Lemma wt_save_callee_save_int:
  forall k,
  wt_instrs k ->
  wt_instrs (save_callee_save_int fe k).

Proof.

  intros. unfold save_callee_save_int, save_callee_save_regs.
  apply wt_fold_right; auto.
  intros. unfold save_callee_save_reg.
  case (zlt (index_int_callee_save x) (fe_num_int_callee_save fe)); intro.
  apply wt_instrs_cons; auto.
  apply wt_Msetstack. apply int_callee_save_type; auto.
  auto.
Qed.

Lemma wt_save_callee_save_float:
  forall k,
  wt_instrs k ->
  wt_instrs (save_callee_save_float fe k).

Proof.

  intros. unfold save_callee_save_float, save_callee_save_regs.
  apply wt_fold_right; auto.
  intros. unfold save_callee_save_reg.
  case (zlt (index_float_callee_save x) (fe_num_float_callee_save fe)); intro.
  apply wt_instrs_cons; auto.
  apply wt_Msetstack. apply float_callee_save_type; auto.
  auto.
Qed.

Lemma wt_restore_callee_save_int:
  forall k,
  wt_instrs k ->
  wt_instrs (restore_callee_save_int fe k).

Proof.

  intros. unfold restore_callee_save_int, restore_callee_save_regs.
  apply wt_fold_right; auto.
  intros. unfold restore_callee_save_reg.
  case (zlt (index_int_callee_save x) (fe_num_int_callee_save fe)); intro.
  apply wt_instrs_cons; auto.
  constructor. apply int_callee_save_type; auto.
  auto.
Qed.

Lemma wt_restore_callee_save_float:
  forall k,
  wt_instrs k ->
  wt_instrs (restore_callee_save_float fe k).

Proof.

  intros. unfold restore_callee_save_float, restore_callee_save_regs.
  apply wt_fold_right; auto.
  intros. unfold restore_callee_save_reg.
  case (zlt (index_float_callee_save x) (fe_num_float_callee_save fe)); intro.
  apply wt_instrs_cons; auto.
  constructor. apply float_callee_save_type; auto.
  auto.
Qed.

Lemma wt_save_callee_save:
forall k,
wt_instrs k -> wt_instrs (save_callee_save fe k).

Proof.

intros. unfold save_callee_save.
apply wt_save_callee_save_int. apply wt_save_callee_save_float. auto.
Qed.

Lemma wt_restore_callee_save:
forall k,
wt_instrs k -> wt_instrs (restore_callee_save fe k).

Proof.

intros. unfold restore_callee_save.
auto using wt_restore_callee_save_int, wt_restore_callee_save_float.
Qed.

Lemma wt_transl_instr:
  forall shift instr k,
  In instr f.(Linear.fn_code) ->
  Lineartyping.wt_instr f instr ->
  wt_instrs k ->
  wt_instrs (transl_instr fe shift instr k).

Proof.

  intros.
  generalize (instr_is_within_bounds f instr H H0); intro BND.
  destruct instr; unfold transl_instr; inv H0; simpl in BND;
    try solve [apply wt_instrs_cons; auto; constructor; auto].
  destruct BND.
  destruct s; simpl in *; apply wt_instrs_cons; auto;
  constructor; auto.
  destruct s.
  apply wt_instrs_cons; auto. apply wt_Msetstack. auto.
  auto.
  apply wt_instrs_cons; auto. apply wt_Msetstack. auto.
  apply wt_instrs_cons; auto.
  constructor.
  destruct o; simpl; congruence.
  rewrite H6. symmetry. apply type_shift_stack_operation.
  apply wt_instrs_cons; auto.
  constructor; auto.
  rewrite H4. destruct a; reflexivity.
  apply wt_instrs_cons; auto.
  constructor; auto.
  rewrite H4. destruct a; reflexivity.
  apply wt_restore_callee_save. apply wt_instrs_cons. constructor. auto.
Qed.

End TRANSL_FUNCTION.

Lemma unsigned_nneg:
forall i, 0 <= Int.unsigned i.

Proof.

exact (fun i => proj1 (Int.unsigned_range i)). Qed.

Lemma align_size_16_div:
forall sz, (Mem.align_size sz | 16).

Proof.

intro. unfold Mem.align_size.
repeat destruct zlt; by apply Zmod_divide.
Qed.

Lemma wt_transf_function:
  forall f tf,
  transf_function f = OK tf ->
  Lineartyping.wt_function f ->
  wt_function tf.

Proof.

  intros.
  generalize H; unfold transf_function, Int.lt.
  case zle; try done; intros LT.
  case zle; try done; intros LT' _.
  assert (EQ := unfold_transf_function f tf H).
  assert (FRMPOS : 0 <= fn_framesize tf) .
    by subst tf; eapply Zle_trans, align_framesize_le;
      pose proof (size_pos f); omega.
  assert (STKPOS : 0 <= fn_paddedstacksize tf).
    subst. unfold fn_paddedstacksize, align_stacksize.
    pose proof (align_le (Int.unsigned (Linear.fn_stacksize f) + fe_retaddrsize)
                         (Mem.align_size (Int.unsigned (Linear.fn_stacksize f)))
                         (Mem.align_size_pos _)).
    pose proof (Int.unsigned_range (Linear.fn_stacksize f)). omega.
  assert (DIV16: (16 | fn_paddedstacksize tf + fn_framesize tf +
                       fe_retaddrsize)).
    subst tf; unfold fn_framesize, fn_paddedstacksize in *.
    set (ssz := align_stacksize (Int.unsigned (Linear.fn_stacksize f))
      fe_retaddrsize); set (rsz := fe_retaddrsize);
        set (fsz := fe_size (make_env (function_bounds f))).
    unfold align_framesize.
    replace (ssz + (align (ssz + rsz + fsz) 16 - ssz - rsz) + rsz) with
      (align (ssz + rsz + fsz) 16); [|omega].
    by apply align_divides.
  constructor; try done.
  - change (wt_instrs (fn_code tf)).
    rewrite EQ; simpl; unfold transl_body.
    apply wt_save_callee_save; auto.
    unfold transl_code. apply wt_fold_right; try done.
    intros; eapply wt_transl_instr; eauto.
  - subst tf; unfold fn_paddedstacksize, fn_stacksize, align_stacksize.
    pose proof (align_le (Int.unsigned (Linear.fn_stacksize f) + fe_retaddrsize)
                         (Mem.align_size (Int.unsigned (Linear.fn_stacksize f)))
                         (Mem.align_size_pos _)); omega.
  - split.
      pose proof (Int.unsigned_range (fn_stacksize tf)).
      unfold fe_retaddrsize. omega.
    subst tf. unfold fn_framesize, fn_paddedstacksize in *.
    unfold Int.min_signed in LT. omega.
  - pose proof (Zdivide_trans _ _ _ (align_size_16_div
      (Int.unsigned (fn_stacksize tf))) DIV16) as ASD.
    assert (STRA: (Mem.align_size (Int.unsigned (fn_stacksize tf)) |
                  fn_paddedstacksize tf + fe_retaddrsize)).
      rewrite EQ; unfold fn_paddedstacksize, fn_stacksize, align_stacksize.
      rewrite Zplus_minus_l. apply align_divides, Mem.align_size_pos.
    replace (fn_framesize tf) with (fn_paddedstacksize tf + fn_framesize tf +
      fe_retaddrsize - (fn_paddedstacksize tf + fe_retaddrsize)); [|omega].
    eby eapply (Zdivide_minus_l _ _ _ ASD STRA).
  - by apply Zmod_divide.
  - subst. simpl. unfold Int.min_signed in LT'. omega.
Qed.

Lemma wt_transf_fundef:
  forall f tf,
  Lineartyping.wt_fundef f ->
  transf_fundef f = OK tf ->
  wt_fundef tf.

Proof.

  intros f tf WT. inversion WT; subst.
  simpl; intros; inversion H. constructor.
  unfold transf_fundef, transf_partial_fundef.
  caseEq (transf_function f0); simpl; try congruence.
  intros tfn TRANSF EQ. inversion EQ; subst tf.
  constructor; eapply wt_transf_function; eauto.
Qed.

Lemma program_typing_preserved:
  forall (p: Linear.program) (tp: Mach.program),
  transf_program p = OK tp ->
  Lineartyping.wt_program p ->
  Machtyping.wt_program tp.

Proof.

  intros; red; intros.
  generalize (transform_partial_program_function transf_fundef p id f H H1).
  intros [f0 [IN TRANSF]].
  apply wt_transf_fundef with f0; auto.
  eapply H0; eauto.
Qed.