summaryrefslogtreecommitdiff
path: root/backend/Stackingtyping.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Stackingtyping.v')
-rw-r--r--backend/Stackingtyping.v250
1 files changed, 0 insertions, 250 deletions
diff --git a/backend/Stackingtyping.v b/backend/Stackingtyping.v
deleted file mode 100644
index 2324cd5..0000000
--- a/backend/Stackingtyping.v
+++ /dev/null
@@ -1,250 +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. *)
-(* *)
-(* *********************************************************************)
-
-(** Type preservation for the [Stacking] pass. *)
-
-Require Import Coqlib.
-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.
- apply wt_restore_callee_save_int. apply wt_restore_callee_save_float. auto.
-Qed.
-
-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).
-Proof.
- intros.
- generalize (instr_is_within_bounds f instr H H0); intro BND.
- destruct instr; unfold transl_instr; inv H0; simpl in BND.
- (* getstack *)
- destruct BND.
- destruct s; simpl in *; apply wt_instrs_cons; auto;
- constructor; auto.
- (* setstack *)
- destruct s.
- apply wt_instrs_cons; auto. apply wt_Msetstack. auto.
- auto.
- apply wt_instrs_cons; auto. apply wt_Msetstack. auto.
- (* op, move *)
- simpl. apply wt_instrs_cons. constructor; auto. auto.
- (* op, others *)
- apply wt_instrs_cons; auto.
- constructor.
- destruct o; simpl; congruence.
- rewrite H6. symmetry. apply type_shift_stack_operation.
- (* load *)
- apply wt_instrs_cons; auto.
- constructor; auto.
- rewrite H4. destruct a; reflexivity.
- (* store *)
- apply wt_instrs_cons; auto.
- constructor; auto.
- rewrite H4. destruct a; reflexivity.
- (* call *)
- apply wt_instrs_cons; auto.
- constructor; auto.
- (* tailcall *)
- apply wt_restore_callee_save. apply wt_instrs_cons; auto.
- constructor; auto.
- destruct s0; auto. rewrite H5; auto.
- (* builtin *)
- apply wt_instrs_cons; auto.
- constructor; auto.
- (* annot *)
- apply wt_instrs_cons; auto.
- constructor; auto.
- (* label *)
- apply wt_instrs_cons; auto.
- constructor.
- (* goto *)
- apply wt_instrs_cons; auto.
- constructor; auto.
- (* cond *)
- apply wt_instrs_cons; auto.
- constructor; auto.
- (* jumptable *)
- apply wt_instrs_cons; auto.
- constructor; auto.
- (* return *)
- apply wt_restore_callee_save. apply wt_instrs_cons. constructor. auto.
-Qed.
-
-End TRANSL_FUNCTION.
-
-Lemma wt_transf_function:
- forall f tf,
- transf_function f = OK tf ->
- Lineartyping.wt_function f ->
- wt_function tf.
-Proof.
- intros.
- exploit unfold_transf_function; eauto. intro EQ.
- set (b := function_bounds f) in *.
- set (fe := make_env b) in *.
- constructor.
- change (wt_instrs (fn_code tf)).
- rewrite EQ; simpl; unfold transl_body.
- unfold fe, b; apply wt_save_callee_save; auto.
- unfold transl_code. apply wt_fold_right.
- intros. eapply wt_transl_instr; eauto.
- red; intros. elim H1.
- rewrite EQ; unfold fn_stacksize.
- generalize (size_pos f).
- generalize (size_no_overflow _ _ H).
- unfold fe, b. 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 i f H H1).
- intros [f0 [IN TRANSF]].
- apply wt_transf_fundef with f0; auto.
- eapply H0; eauto.
-Qed.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-07 21:04:50 +0000