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


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


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


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


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


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


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


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


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


End TRANSL_FUNCTION.

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


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


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