From 2ae43be7b9d4118335c9d2cef6e098f9b9f807fe Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 9 Feb 2006 14:55:48 +0000 Subject: Initial import of compcert git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/RTLtyping.v | 1277 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1277 insertions(+) create mode 100644 backend/RTLtyping.v (limited to 'backend/RTLtyping.v') diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v new file mode 100644 index 00000000..d15dbb88 --- /dev/null +++ b/backend/RTLtyping.v @@ -0,0 +1,1277 @@ +(** Typing rules and a type inference algorithm for RTL. *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Op. +Require Import Registers. +Require Import RTL. +Require Import union_find. + +(** * The type system *) + +(** Like Cminor and all intermediate languages, RTL can be equipped with + a simple type system that statically guarantees that operations + and addressing modes are applied to the right number of arguments + and that the arguments are of the correct types. The type algebra + is trivial, consisting of the two types [Tint] (for integers and pointers) + and [Tfloat] (for floats). + + Additionally, we impose that each pseudo-register has the same type + throughout the function. This requirement helps with register allocation, + enabling each pseudo-register to be mapped to a single hardware register + or stack location of the correct type. + + + The typing judgement for instructions is of the form [wt_instr f env instr], + where [f] is the current function (used to type-check [Ireturn] + instructions) and [env] is a typing environment associating types to + pseudo-registers. Since pseudo-registers have unique types throughout + the function, the typing environment does not change during type-checking + of individual instructions. One point to note is that we have two + polymorphic operators, [Omove] and [Oundef], which can work both + over integers and floats. +*) + +Definition regenv := reg -> typ. + +Section WT_INSTR. + +Variable env: regenv. +Variable funct: function. + +Inductive wt_instr : instruction -> Prop := + | wt_Inop: + forall s, + wt_instr (Inop s) + | wt_Iopmove: + forall r1 r s, + env r1 = env r -> + wt_instr (Iop Omove (r1 :: nil) r s) + | wt_Iopundef: + forall r s, + wt_instr (Iop Oundef nil r s) + | wt_Iop: + forall op args res s, + op <> Omove -> op <> Oundef -> + (List.map env args, env res) = type_of_operation op -> + wt_instr (Iop op args res s) + | wt_Iload: + forall chunk addr args dst s, + List.map env args = type_of_addressing addr -> + env dst = type_of_chunk chunk -> + wt_instr (Iload chunk addr args dst s) + | wt_Istore: + forall chunk addr args src s, + List.map env args = type_of_addressing addr -> + env src = type_of_chunk chunk -> + wt_instr (Istore chunk addr args src s) + | wt_Icall: + forall sig ros args res s, + match ros with inl r => env r = Tint | inr s => True end -> + List.map env args = sig.(sig_args) -> + env res = match sig.(sig_res) with None => Tint | Some ty => ty end -> + wt_instr (Icall sig ros args res s) + | wt_Icond: + forall cond args s1 s2, + List.map env args = type_of_condition cond -> + wt_instr (Icond cond args s1 s2) + | wt_Ireturn: + forall optres, + option_map env optres = funct.(fn_sig).(sig_res) -> + wt_instr (Ireturn optres). + +End WT_INSTR. + +(** A function [f] is well-typed w.r.t. a typing environment [env], + written [wt_function env f], if all instructions are well-typed, + parameters agree in types with the function signature, and + names of parameters are pairwise distinct. *) + +Record wt_function (env: regenv) (f: function) : Prop := + mk_wt_function { + wt_params: + List.map env f.(fn_params) = f.(fn_sig).(sig_args); + wt_norepet: + list_norepet f.(fn_params); + wt_instrs: + forall pc instr, f.(fn_code)!pc = Some instr -> wt_instr env f instr + }. + +(** * Type inference *) + +(** There are several ways to ensure that RTL code is well-typed and + to obtain the typing environment (type assignment for pseudo-registers) + needed for register allocation. One is to start with well-typed Cminor + code and show type preservation for RTL generation and RTL optimizations. + Another is to start with untyped RTL and run a type inference algorithm + that reconstructs the typing environment, determining the type of + each pseudo-register from its uses in the code. We follow the second + approach. + + The algorithm and its correctness proof in this section were + contributed by Damien Doligez. *) + +(** ** Type inference algorithm *) + +Set Implicit Arguments. + +(** Type inference for RTL is similar to that for simply-typed + lambda-calculus: we use type variables to represent the types + of registers that have not yet been determined to be [Tint] or [Tfloat] + based on their uses. We need exactly one type variable per pseudo-register, + therefore type variables can be conveniently equated with registers. + The type of a register during inference is therefore either + [tTy t] (with [t = Tint] or [t = Tfloat]) for a known type, + or [tReg r] to mean ``the same type as that of register [r]''. *) + +Inductive myT : Set := + | tTy : typ -> myT + | tReg : reg -> myT. + +(** The algorithm proceeds by unification of the currently inferred + type for a pseudo-register with the type dictated by its uses. + Unification builds on a ``union-find'' data structure representing + equivalence classes of types (see module [Union_find]). +*) + +Module myreg. + Definition T := myT. + Definition eq : forall (x y : T), {x=y}+{x<>y}. + Proof. + destruct x; destruct y; auto; + try (apply right; discriminate); try (apply left; discriminate). + destruct t; destruct t0; + try (apply right; congruence); try (apply left; congruence). + elim (peq r r0); intros. + rewrite a; apply left; apply refl_equal. + apply right; congruence. + Defined. +End myreg. + +Module mymap. + Definition elt := myreg.T. + Definition encode (t : myreg.T) : positive := + match t with + | tTy Tint => xH + | tTy Tfloat => xI xH + | tReg r => xO r + end. + Definition decode (p : positive) : elt := + match p with + | xH => tTy Tint + | xI _ => tTy Tfloat + | xO r => tReg r + end. + + Lemma encode_decode : forall x : myreg.T, decode (encode x) = x. + Proof. + destruct x; try destruct t; simpl; auto. + Qed. + + Lemma encode_injective : + forall (x y : myreg.T), encode x = encode y -> x = y. + Proof. + intros. + unfold encode in H. destruct x; destruct y; try congruence; + try destruct t; try destruct t0; congruence. + Qed. + + Definition T := PTree.t positive. + Definition empty := PTree.empty positive. + Definition get (adr : elt) (t : T) := + option_map decode (PTree.get (encode adr) t). + Definition add (adr dat : elt) (t : T) := + PTree.set (encode adr) (encode dat) t. + + Theorem get_empty : forall (x : elt), get x empty = None. + Proof. + intro. + unfold get. unfold empty. + rewrite PTree.gempty. + simpl; auto. + Qed. + Theorem get_add_1 : + forall (x y : elt) (m : T), get x (add x y m) = Some y. + Proof. + intros. + unfold add. unfold get. + rewrite PTree.gss. + simpl; rewrite encode_decode; auto. + Qed. + Theorem get_add_2 : + forall (x y z : elt) (m : T), z <> x -> get z (add x y m) = get z m. + Proof. + intros. + unfold get. unfold add. + rewrite PTree.gso; auto. + intro. apply H. apply encode_injective. auto. + Qed. +End mymap. + +Module Uf := Unionfind (myreg) (mymap). + +Definition error := Uf.identify Uf.empty (tTy Tint) (tTy Tfloat). + +Fixpoint fold2 (A B : Set) (f : Uf.T -> A -> B -> Uf.T) + (init : Uf.T) (la : list A) (lb : list B) {struct la} + : Uf.T := + match la, lb with + | ha::ta, hb::tb => fold2 f (f init ha hb) ta tb + | nil, nil => init + | _, _ => error + end. + +Definition option_fold2 (A B : Set) (f : Uf.T -> A -> B -> Uf.T) + (init : Uf.T) (oa : option A) (ob : option B) + : Uf.T := + match oa, ob with + | Some a, Some b => f init a b + | None, None => init + | _, _ => error + end. + +Definition teq (ty1 ty2 : typ) : bool := + match ty1, ty2 with + | Tint, Tint => true + | Tfloat, Tfloat => true + | _, _ => false + end. + +Definition type_rtl_arg (u : Uf.T) (r : reg) (t : typ) := + Uf.identify u (tReg r) (tTy t). + +Definition type_rtl_ros (u : Uf.T) (ros : reg+ident) := + match ros with + | inl r => Uf.identify u (tReg r) (tTy Tint) + | inr s => u + end. + +Definition type_of_sig_res (sig : signature) := + match sig.(sig_res) with None => Tint | Some ty => ty end. + +(** This is the core type inference function. The [u] argument is + the current substitution / equivalence classes between types. + An updated set of equivalence classes, reflecting unifications + possibly performed during the type-checking of [i], is returned. + Note that [type_rtl_instr] never fails explicitly. However, + in case of type error (e.g. applying the [Oadd] integer operation + to float registers), the equivalence relation returned will + put [tTy Tint] and [tTy Tfloat] in the same equivalence class. + This fact will propagate through type inference for other instructions, + and be detected at the end of type inference, indicating a typing failure. +*) + +Definition type_rtl_instr (rtyp : option typ) + (u : Uf.T) (_ : positive) (i : instruction) := + match i with + | Inop _ => u + | Iop Omove (r1 :: nil) r0 _ => Uf.identify u (tReg r0) (tReg r1) + | Iop Omove _ _ _ => error + | Iop Oundef nil _ _ => u + | Iop Oundef _ _ _ => error + | Iop op args r0 _ => + let (argtyp, restyp) := type_of_operation op in + let u1 := type_rtl_arg u r0 restyp in + fold2 type_rtl_arg u1 args argtyp + | Iload chunk addr args r0 _ => + let u1 := type_rtl_arg u r0 (type_of_chunk chunk) in + fold2 type_rtl_arg u1 args (type_of_addressing addr) + | Istore chunk addr args r0 _ => + let u1 := type_rtl_arg u r0 (type_of_chunk chunk) in + fold2 type_rtl_arg u1 args (type_of_addressing addr) + | Icall sign ros args r0 _ => + let u1 := type_rtl_ros u ros in + let u2 := type_rtl_arg u1 r0 (type_of_sig_res sign) in + fold2 type_rtl_arg u2 args sign.(sig_args) + | Icond cond args _ _ => + fold2 type_rtl_arg u args (type_of_condition cond) + | Ireturn o => option_fold2 type_rtl_arg u o rtyp + end. + +Definition mk_env (u : Uf.T) (r : reg) := + if myreg.eq (Uf.repr u (tReg r)) (Uf.repr u (tTy Tfloat)) + then Tfloat + else Tint. + +Fixpoint member (x : reg) (l : list reg) {struct l} : bool := + match l with + | nil => false + | y :: rest => if peq x y then true else member x rest + end. + +Fixpoint repet (l : list reg) : bool := + match l with + | nil => false + | x :: rest => member x rest || repet rest + end. + +Definition type_rtl_function (f : function) := + let u1 := PTree.fold (type_rtl_instr f.(fn_sig).(sig_res)) + f.(fn_code) Uf.empty in + let u2 := fold2 type_rtl_arg u1 f.(fn_params) f.(fn_sig).(sig_args) in + if repet f.(fn_params) then + None + else + if myreg.eq (Uf.repr u2 (tTy Tint)) (Uf.repr u2 (tTy Tfloat)) + then None + else Some (mk_env u2). + +Unset Implicit Arguments. + +(** ** Correctness proof for type inference *) + +(** General properties of the type equivalence relation. *) + +Definition consistent (u : Uf.T) := + Uf.repr u (tTy Tint) <> Uf.repr u (tTy Tfloat). + +Lemma consistent_not_eq : forall (u : Uf.T) (A : Type) (x y : A), + consistent u -> + (if myreg.eq (Uf.repr u (tTy Tint)) (Uf.repr u (tTy Tfloat)) then x else y) + = y. + Proof. + intros. + unfold consistent in H. + destruct (myreg.eq (Uf.repr u (tTy Tint)) (Uf.repr u (tTy Tfloat))); + congruence. + Qed. + +Lemma equal_eq : forall (t : myT) (A : Type) (x y : A), + (if myreg.eq t t then x else y) = x. + Proof. + intros. + destruct (myreg.eq t t); congruence. + Qed. + +Lemma error_inconsistent : forall (A : Prop), consistent error -> A. + Proof. + intros. + absurd (consistent error); auto. + intro. + unfold error in H. unfold consistent in H. + rewrite Uf.sameclass_identify_1 in H. + congruence. + Qed. + +Lemma teq_correct : forall (t1 t2 : typ), teq t1 t2 = true -> t1 = t2. + Proof. + intros; destruct t1; destruct t2; try simpl in H; congruence. + Qed. + +Definition included (u1 u2 : Uf.T) : Prop := + forall (e1 e2: myT), + Uf.repr u1 e1 = Uf.repr u1 e2 -> Uf.repr u2 e1 = Uf.repr u2 e2. + +Lemma included_refl : + forall (e : Uf.T), included e e. + Proof. + unfold included. auto. + Qed. + +Lemma included_trans : + forall (e1 e2 e3 : Uf.T), + included e3 e2 -> included e2 e1 -> included e3 e1. + Proof. + unfold included. auto. + Qed. + +Lemma included_consistent : + forall (u1 u2 : Uf.T), + included u1 u2 -> consistent u2 -> consistent u1. + Proof. + unfold consistent. unfold included. + intros. + intro. apply H0. apply H. + auto. + Qed. + +Lemma included_identify : + forall (u : Uf.T) (t1 t2 : myT), included u (Uf.identify u t1 t2). + Proof. + unfold included. + intros. + apply Uf.sameclass_identify_2; auto. + Qed. + +Lemma type_arg_correct_1 : + forall (u : Uf.T) (r : reg) (t : typ), + consistent (type_rtl_arg u r t) + -> Uf.repr (type_rtl_arg u r t) (tReg r) + = Uf.repr (type_rtl_arg u r t) (tTy t). + Proof. + intros. + unfold type_rtl_arg. + rewrite Uf.sameclass_identify_1. + auto. + Qed. + +Lemma type_arg_correct : + forall (u : Uf.T) (r : reg) (t : typ), + consistent (type_rtl_arg u r t) -> mk_env (type_rtl_arg u r t) r = t. + Proof. + intros. + unfold mk_env. + rewrite type_arg_correct_1. + destruct t. + apply consistent_not_eq; auto. + destruct (myreg.eq (Uf.repr (type_rtl_arg u r Tfloat) (tTy Tfloat))); + congruence. + auto. + Qed. + +Lemma type_arg_included : + forall (u : Uf.T) (r : reg) (t : typ), included u (type_rtl_arg u r t). + Proof. + intros. + unfold type_rtl_arg. + apply included_identify. + Qed. + +Lemma type_arg_extends : + forall (u : Uf.T) (r : reg) (t : typ), + consistent (type_rtl_arg u r t) -> consistent u. + Proof. + intros. + apply included_consistent with (u2 := type_rtl_arg u r t). + apply type_arg_included. + auto. + Qed. + +Lemma type_args_included : + forall (l1 : list reg) (l2 : list typ) (u : Uf.T), + consistent (fold2 type_rtl_arg u l1 l2) + -> included u (fold2 type_rtl_arg u l1 l2). + Proof. + induction l1; intros; destruct l2. + simpl in H; simpl; apply included_refl. + simpl in H. apply error_inconsistent. auto. + simpl in H. apply error_inconsistent. auto. + simpl. + simpl in H. + apply included_trans with (e2 := type_rtl_arg u a t). + apply type_arg_included. + apply IHl1. + auto. + Qed. + +Lemma type_args_extends : + forall (l1 : list reg) (l2 : list typ) (u : Uf.T), + consistent (fold2 type_rtl_arg u l1 l2) -> consistent u. + Proof. + intros. + apply (included_consistent _ _ (type_args_included l1 l2 u H)). + auto. + Qed. + +Lemma type_args_correct : + forall (l1 : list reg) (l2 : list typ) (u : Uf.T), + consistent (fold2 type_rtl_arg u l1 l2) + -> map (mk_env (fold2 type_rtl_arg u l1 l2)) l1 = l2. + Proof. + induction l1. + intros. + destruct l2. + unfold map; simpl; auto. + simpl in H; apply error_inconsistent; auto. + intros. + destruct l2. + simpl in H; apply error_inconsistent; auto. + simpl. + simpl in H. + rewrite (IHl1 l2 (type_rtl_arg u a t) H). + unfold mk_env. + destruct t. + rewrite (type_args_included _ _ _ H (tReg a) (tTy Tint)). + rewrite consistent_not_eq; auto. + apply type_arg_correct_1. + apply type_args_extends with (l1 := l1) (l2 := l2); auto. + rewrite (type_args_included _ _ _ H (tReg a) (tTy Tfloat)). + rewrite equal_eq; auto. + apply type_arg_correct_1. + apply type_args_extends with (l1 := l1) (l2 := l2); auto. + Qed. + +(** Correctness of [wt_params]. *) + +Lemma type_rtl_function_params : + forall (f: function) (env: regenv), + type_rtl_function f = Some env + -> List.map env f.(fn_params) = f.(fn_sig).(sig_args). + Proof. + destruct f; unfold type_rtl_function; simpl. + destruct (repet fn_params); simpl; intros; try congruence. + pose (u := PTree.fold (type_rtl_instr (sig_res fn_sig)) fn_code Uf.empty). + fold u in H. + cut (consistent (fold2 type_rtl_arg u fn_params (sig_args fn_sig))). + intro. + pose (R := Uf.repr (fold2 type_rtl_arg u fn_params (sig_args fn_sig))). + fold R in H. + destruct (myreg.eq (R (tTy Tint)) (R (tTy Tfloat))). + congruence. + injection H. + intro. + rewrite <- H1. + apply type_args_correct. + auto. + intro. + rewrite H0 in H. + rewrite equal_eq in H. + congruence. + Qed. + +(** Correctness of [wt_norepet]. *) + +Lemma member_correct : + forall (l : list reg) (a : reg), member a l = false -> ~In a l. + Proof. + induction l; simpl; intros; try tauto. + destruct (peq a0 a); simpl; try congruence. + intro. destruct H0; try congruence. + generalize H0; apply IHl; auto. + Qed. + +Lemma repet_correct : + forall (l : list reg), repet l = false -> list_norepet l. + Proof. + induction l; simpl; intros. + exact (list_norepet_nil reg). + elim (orb_false_elim (member a l) (repet l) H); intros. + apply list_norepet_cons. + apply member_correct; auto. + apply IHl; auto. + Qed. + +Lemma type_rtl_function_norepet : + forall (f: function) (env: regenv), + type_rtl_function f = Some env + -> list_norepet f.(fn_params). + Proof. + destruct f; unfold type_rtl_function; simpl. + intros. cut (repet fn_params = false). + intro. apply repet_correct. auto. + destruct (repet fn_params); congruence. + Qed. + +(** Correctness of [wt_instrs]. *) + +Lemma step1 : + forall (f : function) (env : regenv), + type_rtl_function f = Some env + -> exists u2 : Uf.T, + included (PTree.fold (type_rtl_instr f.(fn_sig).(sig_res)) + f.(fn_code) Uf.empty) + u2 + /\ env = mk_env u2 + /\ consistent u2. + Proof. + intros f env. + pose (u1 := (PTree.fold (type_rtl_instr f.(fn_sig).(sig_res)) + f.(fn_code) Uf.empty)). + fold u1. + unfold type_rtl_function. + intros. + destruct (repet f.(fn_params)). + congruence. + fold u1 in H. + pose (u2 := (fold2 type_rtl_arg u1 f.(fn_params) f.(fn_sig).(sig_args))). + fold u2 in H. + exists u2. + caseEq (myreg.eq (Uf.repr u2 (tTy Tint)) (Uf.repr u2 (tTy Tfloat))). + intros. + rewrite e in H. + rewrite equal_eq in H. + congruence. + intros. + rewrite consistent_not_eq in H. + apply conj. + unfold u2. + apply type_args_included. + auto. + apply conj; auto. + congruence. + auto. + Qed. + +Lemma let_fold_args_res : + forall (u : Uf.T) (l : list reg) (r : reg) (e : list typ * typ), + (let (argtyp, restyp) := e in + fold2 type_rtl_arg (type_rtl_arg u r restyp) l argtyp) + = fold2 type_rtl_arg (type_rtl_arg u r (snd e)) l (fst e). + Proof. + intros. rewrite (surjective_pairing e). simpl. auto. + Qed. + +Lemma type_args_res_included : + forall (l1 : list reg) (l2 : list typ) (u : Uf.T) (r : reg) (t : typ), + consistent (fold2 type_rtl_arg (type_rtl_arg u r t) l1 l2) + -> included u (fold2 type_rtl_arg (type_rtl_arg u r t) l1 l2). + Proof. + intros. + apply included_trans with (e2 := type_rtl_arg u r t). + apply type_arg_included. + apply type_args_included; auto. + Qed. + +Lemma type_args_res_ros_included : + forall (l1 : list reg) (l2 : list typ) (u : Uf.T) (r : reg) (t : typ) + (ros : reg+ident), + consistent (fold2 type_rtl_arg (type_rtl_arg (type_rtl_ros u ros) r t) l1 l2) + -> included u (fold2 type_rtl_arg (type_rtl_arg (type_rtl_ros u ros) r t) l1 l2). +Proof. + intros. + apply included_trans with (e2 := type_rtl_ros u ros). + unfold type_rtl_ros; destruct ros. + apply included_identify. + apply included_refl. + apply type_args_res_included; auto. +Qed. + +Lemma type_instr_included : + forall (p : positive) (i : instruction) (u : Uf.T) (res_ty : option typ), + consistent (type_rtl_instr res_ty u p i) + -> included u (type_rtl_instr res_ty u p i). + Proof. + intros. + destruct i; simpl; simpl in H; try apply type_args_res_included; auto. + apply included_refl; auto. + destruct o; simpl; simpl in H; try apply type_args_res_included; auto. + destruct l; simpl; simpl in H; auto. + apply error_inconsistent; auto. + destruct l; simpl; simpl in H; auto. + apply included_identify. + apply error_inconsistent; auto. + destruct l; simpl; simpl in H; auto. + apply included_refl. + apply error_inconsistent; auto. + apply type_args_res_ros_included; auto. + apply type_args_included; auto. + destruct res_ty; destruct o; simpl; simpl in H; + try (apply error_inconsistent; auto; fail). + apply type_arg_included. + apply included_refl. + Qed. + +Lemma type_instrs_extends : + forall (l : list (positive * instruction)) (u : Uf.T) (res_ty : option typ), + consistent + (fold_left (fun v p => type_rtl_instr res_ty v (fst p) (snd p)) l u) + -> consistent u. +Proof. + induction l; simpl; intros. + auto. + apply included_consistent + with (u2 := (type_rtl_instr res_ty u (fst a) (snd a))). + apply type_instr_included. + apply IHl with (res_ty := res_ty); auto. + apply IHl with (res_ty := res_ty); auto. +Qed. + +Lemma type_instrs_included : + forall (l : list (positive * instruction)) (u : Uf.T) (res_ty : option typ), + consistent + (fold_left (fun v p => type_rtl_instr res_ty v (fst p) (snd p)) l u) + -> included u + (fold_left (fun v p => type_rtl_instr res_ty v (fst p) (snd p)) l u). + Proof. + induction l; simpl; intros. + apply included_refl; auto. + apply included_trans with (e2 := (type_rtl_instr res_ty u (fst a) (snd a))). + apply type_instr_included. + apply type_instrs_extends with (res_ty := res_ty) (l := l); auto. + apply IHl; auto. + Qed. + +Lemma step2 : + forall (res_ty : option typ) (c : code) (u0 : Uf.T), + consistent (PTree.fold (type_rtl_instr res_ty) c u0) -> + forall (pc : positive) (i : instruction), + c!pc = Some i + -> exists u : Uf.T, + consistent (type_rtl_instr res_ty u pc i) + /\ included (type_rtl_instr res_ty u pc i) + (PTree.fold (type_rtl_instr res_ty) c u0). + Proof. + intros. + rewrite PTree.fold_spec. + rewrite PTree.fold_spec in H. + pose (H1 := PTree.elements_correct _ _ H0). + generalize H. clear H. + generalize u0. clear u0. + generalize H1. clear H1. + induction (PTree.elements c). + intros. + absurd (In (pc, i) nil). + apply in_nil. + auto. + intros. + simpl in H. + elim H1. + intro. + rewrite H2 in H. + simpl in H. + rewrite H2. simpl. + exists u0. + apply conj. + apply type_instrs_extends with (res_ty := res_ty) (l := l). + auto. + apply type_instrs_included. + auto. + intro. + simpl. + apply IHl. + auto. + auto. + Qed. + +Definition mapped (u : Uf.T) (r : reg) := + Uf.repr u (tReg r) = Uf.repr u (tTy Tfloat) + \/ Uf.repr u (tReg r) = Uf.repr u (tTy Tint). + +Definition definite (u : Uf.T) (i : instruction) := + match i with + | Inop _ => True + | Iop Omove (r1 :: nil) r0 _ => Uf.repr u (tReg r1) = Uf.repr u (tReg r0) + | Iop Oundef _ _ _ => True + | Iop _ args r0 _ => + mapped u r0 /\ forall r : reg, In r args -> mapped u r + | Iload _ _ args r0 _ => + mapped u r0 /\ forall r : reg, In r args -> mapped u r + | Istore _ _ args r0 _ => + mapped u r0 /\ forall r : reg, In r args -> mapped u r + | Icall _ ros args r0 _ => + match ros with inl r => mapped u r | _ => True end + /\ mapped u r0 /\ forall r : reg, In r args -> mapped u r + | Icond _ args _ _ => + forall r : reg, In r args -> mapped u r + | Ireturn None => True + | Ireturn (Some r) => mapped u r + end. + +Lemma type_arg_complete : + forall (u : Uf.T) (r : reg) (t : typ), + mapped (type_rtl_arg u r t) r. +Proof. + intros. + unfold type_rtl_arg. + unfold mapped. + destruct t. + right; apply Uf.sameclass_identify_1. + left; apply Uf.sameclass_identify_1. +Qed. + +Lemma type_arg_mapped : + forall (u : Uf.T) (r r0 : reg) (t : typ), + mapped u r0 -> mapped (type_rtl_arg u r t) r0. +Proof. + unfold mapped. + unfold type_rtl_arg. + intros. + elim H; intros. + left; apply Uf.sameclass_identify_2; auto. + right; apply Uf.sameclass_identify_2; auto. +Qed. + +Lemma type_args_mapped : + forall (lr : list reg) (lt : list typ) (u : Uf.T) (r : reg), + consistent (fold2 type_rtl_arg u lr lt) -> + mapped u r -> + mapped (fold2 type_rtl_arg u lr lt) r. +Proof. + induction lr; simpl; intros. + destruct lt; simpl; auto; try (apply error_inconsistent; auto; fail). + destruct lt; simpl; auto; try (apply error_inconsistent; auto; fail). + apply IHlr. + auto. + apply type_arg_mapped; auto. +Qed. + +Lemma type_args_complete : + forall (lr : list reg) (lt : list typ) (u : Uf.T), + consistent (fold2 type_rtl_arg u lr lt) + -> forall r, (In r lr -> mapped (fold2 type_rtl_arg u lr lt) r). +Proof. + induction lr; simpl; intros. + destruct lt; simpl; try tauto. + destruct lt; simpl. + apply error_inconsistent; auto. + elim H0; intros. + rewrite H1. + rewrite H1 in H. + apply type_args_mapped; auto. + apply type_arg_complete. + apply IHlr; auto. +Qed. + +Lemma type_res_complete : + forall (u : Uf.T) (lr : list reg) (lt : list typ) (r : reg) (t : typ), + consistent (fold2 type_rtl_arg (type_rtl_arg u r t) lr lt) + -> mapped (fold2 type_rtl_arg (type_rtl_arg u r t) lr lt) r. +Proof. + intros. + apply type_args_mapped; auto. + apply type_arg_complete. +Qed. + +Lemma type_args_res_complete : + forall (u : Uf.T) (lr : list reg) (lt : list typ) (r : reg) (t : typ), + consistent (fold2 type_rtl_arg (type_rtl_arg u r t) lr lt) + -> mapped (fold2 type_rtl_arg (type_rtl_arg u r t) lr lt) r + /\ forall rr, (In rr lr -> mapped (fold2 type_rtl_arg (type_rtl_arg u r t) + lr lt) + rr). +Proof. + intros. + apply conj. + apply type_res_complete; auto. + apply type_args_complete; auto. +Qed. + +Lemma type_ros_complete : + forall (u : Uf.T) (lr : list reg) (lt : list typ) (r r1 : reg) (t : typ), + consistent (fold2 type_rtl_arg (type_rtl_arg + (type_rtl_ros u (inl ident r1)) r t) lr lt) + -> + mapped (fold2 type_rtl_arg (type_rtl_arg + (type_rtl_ros u (inl ident r1)) r t) lr lt) r1. +Proof. + intros. + apply type_args_mapped; auto. + apply type_arg_mapped. + unfold type_rtl_ros. + unfold mapped. + right. + apply Uf.sameclass_identify_1; auto. +Qed. + +Lemma type_res_correct : + forall (u : Uf.T) (lr : list reg) (lt : list typ) (r : reg) (t : typ), + consistent (fold2 type_rtl_arg (type_rtl_arg u r t) lr lt) + -> mk_env (fold2 type_rtl_arg (type_rtl_arg u r t) lr lt) r = t. +Proof. + intros. + unfold mk_env. + rewrite (type_args_included _ _ _ H (tReg r) (tTy t)). + destruct t. + apply consistent_not_eq; auto. + apply equal_eq; auto. + unfold type_rtl_arg; apply Uf.sameclass_identify_1; auto. +Qed. + +Lemma type_ros_correct : + forall (u : Uf.T) (lr : list reg) (lt : list typ) (r r1 : reg) (t : typ), + consistent (fold2 type_rtl_arg (type_rtl_arg + (type_rtl_ros u (inl ident r1)) r t) lr lt) + -> + mk_env (fold2 type_rtl_arg (type_rtl_arg + (type_rtl_ros u (inl ident r1)) r t) lr lt) r1 + = Tint. +Proof. + intros. + unfold mk_env. + rewrite (type_args_included _ _ _ H (tReg r1) (tTy Tint)). + apply consistent_not_eq; auto. + rewrite (type_arg_included (type_rtl_ros u (inl ident r1)) r t (tReg r1) (tTy Tint)). + auto. + simpl. + apply Uf.sameclass_identify_1; auto. +Qed. + +Lemma step3 : + forall (u : Uf.T) (f : function) (c : code) (i : instruction) (pc : positive), + c!pc = Some i -> + consistent (type_rtl_instr f.(fn_sig).(sig_res) u pc i) + -> wt_instr (mk_env (type_rtl_instr f.(fn_sig).(sig_res) u pc i)) f i + /\ definite (type_rtl_instr f.(fn_sig).(sig_res) u pc i) i. + Proof. + Opaque type_rtl_arg. + intros. + destruct i; simpl in H0; simpl. + (* Inop *) + apply conj; auto. apply wt_Inop. + (* Iop *) + destruct o; + try (apply conj; [ + apply wt_Iop; try congruence; simpl; + rewrite (type_args_correct _ _ _ H0); + rewrite (type_res_correct _ _ _ _ _ H0); + auto + |apply (type_args_res_complete _ _ _ _ _ H0)]). + (* Omove *) + destruct l; [apply error_inconsistent; auto | idtac]. + destruct l; [idtac | apply error_inconsistent; auto]. + apply conj. + apply wt_Iopmove. + simpl. + unfold mk_env. + rewrite Uf.sameclass_identify_1. + congruence. + simpl. + rewrite Uf.sameclass_identify_1; congruence. + (* Oundef *) + destruct l; [idtac | apply error_inconsistent; auto]. + apply conj. apply wt_Iopundef. + unfold definite. auto. + (* Iload *) + apply conj. + apply wt_Iload. + rewrite (type_args_correct _ _ _ H0); auto. + rewrite (type_res_correct _ _ _ _ _ H0); auto. + simpl; apply (type_args_res_complete _ _ _ _ _ H0). + (* IStore *) + apply conj. + apply wt_Istore. + rewrite (type_args_correct _ _ _ H0); auto. + rewrite (type_res_correct _ _ _ _ _ H0); auto. + simpl; apply (type_args_res_complete _ _ _ _ _ H0). + (* Icall *) + apply conj. + apply wt_Icall. + destruct s0; auto. apply type_ros_correct. auto. + apply type_args_correct. auto. + fold (type_of_sig_res s). apply type_res_correct. auto. + destruct s0. + apply conj. + apply type_ros_complete. auto. + apply type_args_res_complete. auto. + apply conj; auto. + apply type_args_res_complete. auto. + (* Icond *) + apply conj. + apply wt_Icond. + apply (type_args_correct _ _ _ H0). + simpl; apply (type_args_complete _ _ _ H0). + (* Ireturn *) + destruct o; simpl. + apply conj. + apply wt_Ireturn. + destruct f.(fn_sig).(sig_res); simpl; simpl in H0. + rewrite type_arg_correct; auto. + apply error_inconsistent; auto. + destruct f.(fn_sig).(sig_res); simpl; simpl in H0. + apply type_arg_complete. + apply error_inconsistent; auto. + apply conj; auto. apply wt_Ireturn. + destruct f.(fn_sig).(sig_res); simpl; simpl in H0. + apply error_inconsistent; auto. + congruence. + Transparent type_rtl_arg. + Qed. + +Lemma mapped_included_consistent : + forall (u1 u2 : Uf.T) (r : reg), + mapped u1 r -> + included u1 u2 -> + consistent u2 -> + mk_env u2 r = mk_env u1 r. +Proof. + intros. + unfold mk_env. + unfold mapped in H. + elim H; intros; rewrite H2; rewrite (H0 _ _ H2). + rewrite equal_eq; rewrite equal_eq; auto. + rewrite (consistent_not_eq u2). + rewrite (consistent_not_eq u1). + auto. + apply included_consistent with (u2 := u2). + auto. + auto. + auto. +Qed. + +Lemma mapped_list_included : + forall (u1 u2 : Uf.T) (lr : list reg), + (forall r, In r lr -> mapped u1 r) -> + included u1 u2 -> + consistent u2 -> + map (mk_env u2) lr = map (mk_env u1) lr. +Proof. + induction lr; simpl; intros. + auto. + rewrite (mapped_included_consistent u1 u2 a). + rewrite IHlr; auto. + apply (H a); intros. + left; auto. + auto. + auto. +Qed. + +Lemma included_mapped : + forall (u1 u2 : Uf.T) (r : reg), + included u1 u2 -> + mapped u1 r -> + mapped u2 r. +Proof. + unfold mapped. + intros. + elim H0; intros. + left; rewrite (H _ _ H1); auto. + right; rewrite (H _ _ H1); auto. +Qed. + +Lemma included_mapped_forall : + forall (u1 u2 : Uf.T) (r : reg) (l : list reg), + included u1 u2 -> + mapped u1 r /\ (forall r, In r l -> mapped u1 r) -> + mapped u2 r /\ (forall r, In r l -> mapped u2 r). +Proof. + intros. + elim H0; intros. + apply conj. + apply (included_mapped _ _ r H); auto. + intros. + apply (included_mapped _ _ r0 H). + apply H2; auto. +Qed. + +Lemma definite_included : + forall (u1 u2 : Uf.T) (i : instruction), + included u1 u2 -> definite u1 i -> definite u2 i. +Proof. + unfold definite. + intros. + destruct i; try apply (included_mapped_forall _ _ _ _ H H0); auto. + destruct o; try apply (included_mapped_forall _ _ _ _ H H0); auto. + destruct l; auto. + apply (included_mapped_forall _ _ _ _ H H0). + destruct l; auto. + apply (included_mapped_forall _ _ _ _ H H0). + destruct s0; auto. + elim H0; intros. + apply conj. + apply (included_mapped _ _ _ H H1). + apply (included_mapped_forall _ _ _ _ H H2). + elim H0; intros. + apply conj; auto. + apply (included_mapped_forall _ _ _ _ H H2). + intros. + apply (included_mapped _ _ _ H (H0 r H1)). + destruct o; auto. + apply (included_mapped _ _ _ H H0). +Qed. + +Lemma step4 : + forall (f : function) (u1 u3 : Uf.T) (i : instruction), + included u3 u1 -> + wt_instr (mk_env u3) f i -> + definite u3 i -> + consistent u1 -> + wt_instr (mk_env u1) f i. + Proof. + intros f u1 u3 i H1 H H0 X. + destruct H; try simpl in H0; try (elim H0; intros). + apply wt_Inop. + apply wt_Iopmove. unfold mk_env. rewrite (H1 _ _ H0). auto. + apply wt_Iopundef. + apply wt_Iop; auto. + destruct op; try congruence; simpl; simpl in H3; + simpl in H0; elim H0; intros; rewrite (mapped_included_consistent _ _ _ H4 H1 X); + rewrite (mapped_list_included _ _ _ H5 H1); auto. + apply wt_Iload. + rewrite (mapped_list_included _ _ _ H4 H1); auto. + rewrite (mapped_included_consistent _ _ _ H3 H1 X). auto. + apply wt_Istore. + rewrite (mapped_list_included _ _ _ H4 H1); auto. + rewrite (mapped_included_consistent _ _ _ H3 H1 X). auto. + elim H5; intros; destruct ros; apply wt_Icall. + rewrite (mapped_included_consistent _ _ _ H4 H1 X); auto. + rewrite (mapped_list_included _ _ _ H7 H1); auto. + rewrite (mapped_included_consistent _ _ _ H6 H1 X); auto. + auto. + rewrite (mapped_list_included _ _ _ H7 H1); auto. + rewrite (mapped_included_consistent _ _ _ H6 H1 X); auto. + apply wt_Icond. rewrite (mapped_list_included _ _ _ H0 H1); auto. + apply wt_Ireturn. + destruct optres; destruct f.(fn_sig).(sig_res); + simpl in H; simpl; try congruence. + rewrite (mapped_included_consistent _ _ _ H0 H1 X); auto. + Qed. + +Lemma type_rtl_function_instrs : + forall (f: function) (env: regenv), + type_rtl_function f = Some env + -> forall pc i, f.(fn_code)!pc = Some i -> wt_instr env f i. + Proof. + intros. + elim (step1 _ _ H). + intros. + elim H1. + intros. + elim H3. + intros. + rewrite H4. + elim (step2 _ _ _ (included_consistent _ _ H2 H5) _ _ H0). + intros. + elim H6. intros. + elim (step3 x0 f _ _ _ H0); auto. intros. + apply (step4 f _ _ i H2); auto. + apply (step4 _ _ _ _ H8 H9 H10). + apply (included_consistent _ _ H2); auto. + apply (definite_included _ _ _ H8 H10); auto. + Qed. + +(** Combining the sub-proofs. *) + +Theorem type_rtl_function_correct: + forall (f: function) (env: regenv), + type_rtl_function f = Some env -> wt_function env f. + Proof. + intros. + exact (mk_wt_function env f (type_rtl_function_params f _ H) + (type_rtl_function_norepet f _ H) + (type_rtl_function_instrs f _ H)). + Qed. + +Definition wt_program (p: program) : Prop := + forall i f, In (i, f) (prog_funct p) -> type_rtl_function f <> None. + +(** * Type preservation during evaluation *) + +(** The type system for RTL is not sound in that it does not guarantee + progress: well-typed instructions such as [Icall] can fail because + of run-time type tests (such as the equality between calle and caller's + signatures). However, the type system guarantees a type preservation + property: if the execution does not fail because of a failed run-time + test, the result values and register states match the static + typing assumptions. This preservation property will be useful + later for the proof of semantic equivalence between [Machabstr] and [Mach]. + Even though we do not need it for [RTL], we show preservation for [RTL] + here, as a warm-up exercise and because some of the lemmas will be + useful later. *) + +Require Import Globalenvs. +Require Import Values. +Require Import Mem. +Require Import Integers. + +Definition wt_regset (env: regenv) (rs: regset) : Prop := + forall r, Val.has_type (rs#r) (env r). + +Lemma wt_regset_assign: + forall env rs v r, + wt_regset env rs -> + Val.has_type v (env r) -> + wt_regset env (rs#r <- v). +Proof. + intros; red; intros. + rewrite Regmap.gsspec. + case (peq r0 r); intro. + subst r0. assumption. + apply H. +Qed. + +Lemma wt_regset_list: + forall env rs, + wt_regset env rs -> + forall rl, Val.has_type_list (rs##rl) (List.map env rl). +Proof. + induction rl; simpl. + auto. + split. apply H. apply IHrl. +Qed. + +Lemma wt_init_regs: + forall env rl args, + Val.has_type_list args (List.map env rl) -> + wt_regset env (init_regs args rl). +Proof. + induction rl; destruct args; simpl; intuition. + red; intros. rewrite Regmap.gi. simpl; auto. + apply wt_regset_assign; auto. +Qed. + +Section SUBJECT_REDUCTION. + +Variable p: program. + +Hypothesis wt_p: wt_program p. + +Let ge := Genv.globalenv p. + +Definition exec_instr_subject_reduction + (c: code) (sp: val) + (pc: node) (rs: regset) (m: mem) + (pc': node) (rs': regset) (m': mem) : Prop := + forall env f + (CODE: c = fn_code f) + (WT_FN: wt_function env f) + (WT_RS: wt_regset env rs), + wt_regset env rs'. + +Definition exec_function_subject_reduction + (f: function) (args: list val) (m: mem) (res: val) (m': mem) : Prop := + forall env, + wt_function env f -> + Val.has_type_list args f.(fn_sig).(sig_args) -> + Val.has_type res + (match f.(fn_sig).(sig_res) with None => Tint | Some ty => ty end). + +Lemma subject_reduction: + forall f args m res m', + exec_function ge f args m res m' -> + exec_function_subject_reduction f args m res m'. +Proof. + apply (exec_function_ind_3 ge + exec_instr_subject_reduction + exec_instr_subject_reduction + exec_function_subject_reduction); + intros; red; intros; + try (rewrite CODE in H; + generalize (wt_instrs env _ WT_FN pc _ H); + intro WT_INSTR; + inversion WT_INSTR). + + assumption. + + apply wt_regset_assign. auto. + subst op. subst args. simpl in H0. injection H0; intro. + subst v. rewrite <- H2. apply WT_RS. + + apply wt_regset_assign. auto. + subst op; subst args; simpl in H0. injection H0; intro; subst v. + simpl; auto. + + apply wt_regset_assign. auto. + replace (env res) with (snd (type_of_operation op)). + apply type_of_operation_sound with function ge rs##args sp; auto. + rewrite <- H7. reflexivity. + + apply wt_regset_assign. auto. rewrite H8. + eapply type_of_chunk_correct; eauto. + + assumption. + + apply wt_regset_assign. auto. rewrite H11. rewrite H1. + assert (type_rtl_function f <> None). + destruct ros; simpl in H0. + pattern f. apply Genv.find_funct_prop with function p (rs#r). + exact wt_p. exact H0. + caseEq (Genv.find_symbol ge i); intros; rewrite H12 in H0. + pattern f. apply Genv.find_funct_ptr_prop with function p b. + exact wt_p. exact H0. + discriminate. + assert (exists env1, wt_function env1 f). + caseEq (type_rtl_function f); intros; try congruence. + exists t. apply type_rtl_function_correct; auto. + elim H13; intros env1 WT_FN1. + eapply H3. eexact WT_FN1. rewrite <- H1. rewrite <- H10. + apply wt_regset_list; auto. + + assumption. + assumption. + assumption. + eauto. + eauto. + + assert (WT_INIT: wt_regset env (init_regs args (fn_params f))). + apply wt_init_regs. rewrite (wt_params env f H4). assumption. + generalize (H1 env f (refl_equal (fn_code f)) H4 WT_INIT). + intro WT_RS. + generalize (wt_instrs env _ H4 pc _ H2). + intro WT_INSTR; inversion WT_INSTR. + destruct or; simpl in H3; simpl in H7; rewrite <- H7. + rewrite H3. apply WT_RS. + rewrite H3. simpl; auto. +Qed. + +End SUBJECT_REDUCTION. -- cgit