From e57315d524658bcde314785bcf30780f2361e359 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 22 Mar 2013 10:10:13 +0000 Subject: RTLtyping: now performed entirely in Coq, no need for an external Caml oracle + a validator. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2157 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/RTLtyping.v | 914 +++++++++++++++++++++++++++++++++++++----------- backend/RTLtypingaux.ml | 170 --------- 2 files changed, 713 insertions(+), 371 deletions(-) delete mode 100644 backend/RTLtypingaux.ml (limited to 'backend') diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index f8dbfe4..a1f9518 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -12,6 +12,7 @@ (** Typing rules and a type inference algorithm for RTL. *) +Require Import Recdef. Require Import Coqlib. Require Import Errors. Require Import Maps. @@ -160,266 +161,777 @@ Definition wt_program (p: program): Prop := (** * 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. +Section INFERENCE. - We delegate the task of determining the type of each pseudo-register - to an external ``oracle'': a function written in Caml and not - proved correct. We verify the returned type environment using - the following Coq code, which we will prove correct. *) +Local Open Scope error_monad_scope. -Parameter infer_type_environment: - function -> list (node * instruction) -> option regenv. +Variable f: function. -(** ** Algorithm to check the correctness of a type environment *) +(** The type inference engine operates over a state that has two components: +- [te_typ]: a partial map from pseudoregisters to types, for + pseudoregs whose types are already determined from their uses; +- [te_eqs]: a list of pairs [(r1,r2)] of pseudoregisters, indicating that + [r1] and [r2] must have the same type because they are involved in a move + [r1 := r2] or [r2 := r1], but this type is not yet determined. +*) -Section TYPECHECKING. +Record typenv : Type := Typenv { + te_typ: PTree.t typ; (**r mapping reg -> known type *) + te_eqs: list (reg * reg) (**r pairs of regs that must have same type *) +}. -Variable funct: function. -Variable env: regenv. +(** Determine that [r] must have type [ty]. *) -Definition check_reg (r: reg) (ty: typ): bool := - if typ_eq (env r) ty then true else false. +Definition type_reg (e: typenv) (r: reg) (ty: typ) : res typenv := + match e.(te_typ)!r with + | None => OK {| te_typ := PTree.set r ty e.(te_typ); te_eqs := e.(te_eqs) |} + | Some ty' => if typ_eq ty ty' then OK e else Error (MSG "bad type for variable " :: POS r :: nil) + end. -Fixpoint check_regs (rl: list reg) (tyl: list typ) {struct rl}: bool := +Fixpoint type_regs (e: typenv) (rl: list reg) (tyl: list typ) {struct rl}: res typenv := match rl, tyl with - | nil, nil => true - | r1::rs, ty::tys => check_reg r1 ty && check_regs rs tys - | _, _ => false + | nil, nil => OK e + | r1::rs, ty1::tys => do e1 <- type_reg e r1 ty1; type_regs e1 rs tys + | _, _ => Error (msg "arity mismatch") + end. + +Definition type_ros (e: typenv) (ros: reg + ident) : res typenv := + match ros with + | inl r => type_reg e r Tint + | inr s => OK e + end. + +(** Determine that [r1] and [r2] must have the same type. If none of + [r1] and [r2] has known type, just record an equality constraint. + The boolean result is [true] if one of the types of [r1] and [r2] + was previously unknown and could be determined because the other type is + known. Otherwise, [te_typ] does not change and [false] is returned. *) + +Function type_move (e: typenv) (r1 r2: reg) : res (bool * typenv) := + match e.(te_typ)!r1, e.(te_typ)!r2 with + | None, None => + OK (false, {| te_typ := e.(te_typ); te_eqs := (r1, r2) :: e.(te_eqs) |}) + | Some ty1, None => + OK (true, {| te_typ := PTree.set r2 ty1 e.(te_typ); te_eqs := e.(te_eqs) |}) + | None, Some ty2 => + OK (true, {| te_typ := PTree.set r1 ty2 e.(te_typ); te_eqs := e.(te_eqs) |}) + | Some ty1, Some ty2 => + if typ_eq ty1 ty2 + then OK (false, e) + else Error(MSG "ill-typed move between " :: POS r1 :: MSG " and " :: POS r2 :: nil) + end. + +(** Checking the validity of successor nodes. *) + +Definition check_successor (s: node): res unit := + match f.(fn_code)!s with + | None => Error (MSG "bad successor " :: POS s :: nil) + | Some i => OK tt + end. + +Fixpoint check_successors (sl: list node): res unit := + match sl with + | nil => OK tt + | s1 :: sl' => do x <- check_successor s1; check_successors sl' end. -Definition check_op (op: operation) (args: list reg) (res: reg): bool := - let (targs, tres) := type_of_operation op in - check_regs args targs && check_reg res tres. +Definition is_move (op: operation) : bool := + match op with Omove => true | _ => false end. -Definition check_successor (s: node) : bool := - match funct.(fn_code)!s with None => false | Some i => true end. +(** First pass: check structural constraints and process all type constraints + of the form [typeof(r) = ty] arising from the RTL instructions. + Simultaneously, record equations [typeof(r1) = typeof(r2)] arising + from move instructions that cannot be immediately resolved. *) -Definition check_instr (i: instruction) : bool := +Definition type_instr (e: typenv) (i: instruction) : res typenv := match i with | Inop s => - check_successor s - | Iop Omove (arg::nil) res s => - if typ_eq (env arg) (env res) - then check_successor s - else false - | Iop Omove args res s => - false + do x <- check_successor s; OK e | Iop op args res s => - check_op op args res && check_successor s + do x <- check_successor s; + if is_move op then + match args with + | arg :: nil => do (changed, e') <- type_move e arg res; OK e' + | _ => Error (msg "ill-formed move") + end + else + (let (targs, tres) := type_of_operation op in + do e1 <- type_regs e args targs; type_reg e1 res tres) | Iload chunk addr args dst s => - check_regs args (type_of_addressing addr) - && check_reg dst (type_of_chunk chunk) - && check_successor s + do x <- check_successor s; + do e1 <- type_regs e args (type_of_addressing addr); + type_reg e1 dst (type_of_chunk chunk) | Istore chunk addr args src s => - check_regs args (type_of_addressing addr) - && check_reg src (type_of_chunk chunk) - && check_successor s + do x <- check_successor s; + do e1 <- type_regs e args (type_of_addressing addr); + type_reg e1 src (type_of_chunk chunk) | Icall sig ros args res s => - match ros with inl r => check_reg r Tint | inr s => true end - && check_regs args sig.(sig_args) - && check_reg res (proj_sig_res sig) - && check_successor s + do x <- check_successor s; + do e1 <- type_ros e ros; + do e2 <- type_regs e1 args sig.(sig_args); + type_reg e2 res (proj_sig_res sig) | Itailcall sig ros args => - match ros with inl r => check_reg r Tint | inr s => true end - && check_regs args sig.(sig_args) - && opt_typ_eq sig.(sig_res) funct.(fn_sig).(sig_res) - && tailcall_is_possible sig + do e1 <- type_ros e ros; + do e2 <- type_regs e1 args sig.(sig_args); + if opt_typ_eq sig.(sig_res) f.(fn_sig).(sig_res) then + if tailcall_is_possible sig + then OK e2 + else Error(msg "tailcall not possible") + else Error(msg "bad return type in tailcall") | Ibuiltin ef args res s => - check_regs args (ef_sig ef).(sig_args) - && check_reg res (proj_sig_res (ef_sig ef)) - && (if ef_reloads ef then arity_ok (ef_sig ef).(sig_args) else true) - && check_successor s + let sig := ef_sig ef in + do x <- check_successor s; + do e1 <- type_regs e args sig.(sig_args); + do e2 <- type_reg e1 res (proj_sig_res sig); + if (negb (ef_reloads ef)) || arity_ok sig.(sig_args) + then OK e2 + else Error(msg "cannot reload builtin") | Icond cond args s1 s2 => - check_regs args (type_of_condition cond) - && check_successor s1 - && check_successor s2 + do x1 <- check_successor s1; + do x2 <- check_successor s2; + type_regs e args (type_of_condition cond) | Ijumptable arg tbl => - check_reg arg Tint - && List.forallb check_successor tbl - && zle (list_length_z tbl * 4) Int.max_unsigned + do x <- check_successors tbl; + do e1 <- type_reg e arg Tint; + if zle (list_length_z tbl * 4) Int.max_unsigned then OK e1 else Error(msg "jumptable too big") | Ireturn optres => - match optres, funct.(fn_sig).(sig_res) with - | None, None => true - | Some r, Some t => check_reg r t - | _, _ => false + match optres, f.(fn_sig).(sig_res) with + | None, None => OK e + | Some r, Some t => type_reg e r t + | _, _ => Error(msg "bad return") end end. -Definition check_params_norepet (params: list reg): bool := - if list_norepet_dec Reg.eq params then true else false. +Definition type_code (e: typenv): res typenv := + PTree.fold + (fun re pc i => + match re with + | Error _ => re + | OK e => + match type_instr e i with + | Error msg => Error(MSG "At PC " :: POS pc :: MSG ": " :: msg) + | OK e' => OK e' + end + end) + f.(fn_code) (OK e). + +(** Second pass: iteratively process the remaining equality constraints + arising out of "move" instructions *) -Fixpoint check_instrs (instrs: list (node * instruction)) : bool := - match instrs with - | nil => true - | (pc, i) :: rem => check_instr i && check_instrs rem +Definition equations := list (reg * reg). + +Fixpoint solve_rec (e: typenv) (changed: bool) (q: equations) : res (typenv * bool) := + match q with + | nil => + OK (e, changed) + | (r1, r2) :: q' => + do (changed1, e1) <- type_move e r1 r2; solve_rec e1 (changed || changed1) q' end. -(** ** Correctness of the type-checking algorithm *) +Lemma type_move_length: + forall e r1 r2 changed e', + type_move e r1 r2 = OK (changed, e') -> + if changed + then List.length e'.(te_eqs) = List.length e.(te_eqs) + else (List.length e'.(te_eqs) <= S (List.length e.(te_eqs)))%nat. +Proof. + intros. functional inversion H; subst; simpl; omega. +Qed. + +Lemma solve_rec_length: + forall q e changed e' changed', + solve_rec e changed q = OK (e', changed') -> + (List.length e'.(te_eqs) <= List.length e.(te_eqs) + List.length q)%nat. +Proof. + induction q; simpl; intros. +- inv H. omega. +- destruct a as [r1 r2]. monadInv H. + assert (length (te_eqs x0) <= S (length (te_eqs e)))%nat. + { + exploit type_move_length; eauto. destruct x; omega. + } + exploit IHq; eauto. + omega. +Qed. -Ltac elimAndb := - match goal with - | [ H: _ && _ = true |- _ ] => - elim (andb_prop _ _ H); clear H; intros; elimAndb - | _ => - idtac +Lemma solve_rec_shorter: + forall q e e', + solve_rec e false q = OK (e', true) -> + (List.length e'.(te_eqs) < List.length e.(te_eqs) + List.length q)%nat. +Proof. + induction q; simpl; intros. +- discriminate. +- destruct a as [r1 r2]; monadInv H. + exploit type_move_length; eauto. destruct x; intros. + exploit solve_rec_length; eauto. omega. + exploit IHq; eauto. omega. +Qed. + +Definition length_typenv (e: typenv) := length e.(te_eqs). + +Function solve_equations (e: typenv) {measure length_typenv e} : res typenv := + match solve_rec {| te_typ := e.(te_typ); te_eqs := nil |} false e.(te_eqs) with + | OK (e', false) => OK e (**r no progress made: terminate *) + | OK (e', true) => solve_equations e' (**r at least one type changed: iterate *) + | Error msg => Error msg end. +Proof. + intros. exploit solve_rec_shorter; eauto. +Qed. + +(** The final type assignment aribtrarily gives type [Tint] to the + pseudoregs that are still unconstrained at the end of type inference. *) + +Definition make_regenv (e: typenv) : regenv := + fun r => match e.(te_typ)!r with Some ty => ty | None => Tint end. + +Definition check_params_norepet (params: list reg): res unit := + if list_norepet_dec Reg.eq params then OK tt else Error(msg "duplicate parameters"). -Lemma check_reg_correct: - forall r ty, check_reg r ty = true -> env r = ty. +Definition type_function : res regenv := + do e1 <- type_code {| te_typ := PTree.empty typ; te_eqs := nil |}; + do e2 <- type_regs e1 f.(fn_params) f.(fn_sig).(sig_args); + do e3 <- solve_equations e2; + do x1 <- check_params_norepet f.(fn_params); + do x2 <- check_successor f.(fn_entrypoint); + OK (make_regenv e3). + +(** ** Soundness proof *) + +(** What it means for a final type assignment [te] to satisfy the constraints + collected so far in the [e] state. *) + +Definition satisf (te: regenv) (e: typenv) : Prop := + (forall r ty, e.(te_typ)!r = Some ty -> te r = ty) + /\ (forall r1 r2, In (r1, r2) e.(te_eqs) -> te r1 = te r2). + +Remark type_reg_incr: + forall e r ty e' te, type_reg e r ty = OK e' -> satisf te e' -> satisf te e. +Proof. + unfold type_reg; intros; destruct (e.(te_typ)!r) eqn:E. + destruct (typ_eq ty t); inv H. auto. + inv H. destruct H0 as [A B]. split; intros. + apply A. simpl. rewrite PTree.gso; auto. congruence. + apply B. simpl; auto. +Qed. + +Hint Resolve type_reg_incr: ty. + +Remark type_regs_incr: + forall rl tyl e e' te, type_regs e rl tyl = OK e' -> satisf te e' -> satisf te e. Proof. - unfold check_reg; intros. - destruct (typ_eq (env r) ty). auto. discriminate. + induction rl; simpl; intros; destruct tyl; try discriminate. + inv H; eauto with ty. + monadInv H. eauto with ty. Qed. -Lemma check_regs_correct: - forall rl tyl, check_regs rl tyl = true -> List.map env rl = tyl. +Hint Resolve type_regs_incr: ty. + +Remark type_ros_incr: + forall e ros e' te, type_ros e ros = OK e' -> satisf te e' -> satisf te e. +Proof. + unfold type_ros; intros. destruct ros. eauto with ty. inv H; auto with ty. +Qed. + +Hint Resolve type_ros_incr: ty. + +Remark type_move_incr: + forall e r1 r2 changed e' te, + type_move e r1 r2 = OK (changed, e') -> + satisf te e' -> satisf te e. Proof. - induction rl; destruct tyl; simpl; intros. - auto. discriminate. discriminate. - elimAndb. - rewrite (check_reg_correct _ _ H). rewrite (IHrl tyl H0). auto. + intros. destruct H0 as [A B]. functional inversion H; subst; simpl in *. +- split; auto. +- split; intros. apply A. rewrite PTree.gso; auto. congruence. auto. +- split; intros. apply A. rewrite PTree.gso; auto. congruence. auto. +- split; auto. Qed. -Lemma check_op_correct: - forall op args res, - check_op op args res = true -> - (List.map env args, env res) = type_of_operation op. +Hint Resolve type_move_incr: ty. + +Lemma type_reg_sound: + forall e r ty e' te, type_reg e r ty = OK e' -> satisf te e' -> te r = ty. Proof. - unfold check_op; intros. - destruct (type_of_operation op) as [targs tres]. - elimAndb. - rewrite (check_regs_correct _ _ H). - rewrite (check_reg_correct _ _ H0). + unfold type_reg; intros. destruct H0 as [A B]. + destruct (e.(te_typ)!r) as [t|] eqn:E. + destruct (typ_eq ty t); inv H. apply A; auto. + inv H. apply A. simpl. apply PTree.gss. +Qed. + +Lemma type_regs_sound: + forall rl tyl e e' te, type_regs e rl tyl = OK e' -> satisf te e' -> map te rl = tyl. +Proof. + induction rl; simpl; intros; destruct tyl; try discriminate. +- auto. +- monadInv H. f_equal; eauto. eapply type_reg_sound. eauto. eauto with ty. +Qed. + +Lemma type_ros_sound: + forall e ros e' te, type_ros e ros = OK e' -> satisf te e' -> + match ros with inl r => te r = Tint | inr s => True end. +Proof. + unfold type_ros; intros. destruct ros. + eapply type_reg_sound; eauto. auto. Qed. -Lemma check_successor_correct: - forall s, - check_successor s = true -> valid_successor funct s. -Proof. - intro; unfold check_successor, valid_successor. - destruct (fn_code funct)!s; intro. - exists i; auto. - discriminate. -Qed. - -Lemma check_instr_correct: - forall i, check_instr i = true -> wt_instr env funct i. -Proof. - unfold check_instr; intros; destruct i; elimAndb. - (* nop *) - constructor. apply check_successor_correct; auto. - (* op *) - destruct o; elimAndb; - try (apply wt_Iop; [ congruence - | apply check_op_correct; auto - | apply check_successor_correct; auto ]). - destruct l; try discriminate. destruct l; try discriminate. - destruct (typ_eq (env r0) (env r)); try discriminate. - apply wt_Iopmove; auto. apply check_successor_correct; auto. - (* load *) - constructor. apply check_regs_correct; auto. apply check_reg_correct; auto. - apply check_successor_correct; auto. - (* store *) - constructor. apply check_regs_correct; auto. apply check_reg_correct; auto. - apply check_successor_correct; auto. - (* call *) +Lemma type_move_sound: + forall e r1 r2 changed e' te, + type_move e r1 r2 = OK (changed, e') -> satisf te e' -> te r1 = te r2. +Proof. + intros. destruct H0 as [A B]. functional inversion H; subst; simpl in *. +- apply B; auto. +- rewrite (A r1 ty1). rewrite (A r2 ty1). auto. + apply PTree.gss. rewrite PTree.gso; auto. congruence. +- rewrite (A r1 ty2). rewrite (A r2 ty2). auto. + rewrite PTree.gso; auto. congruence. apply PTree.gss. +- erewrite ! A; eauto. +Qed. + +Lemma check_successor_sound: + forall s x, check_successor s = OK x -> valid_successor f s. +Proof. + unfold check_successor, valid_successor; intros. + destruct (fn_code f)!s; inv H. exists i; auto. +Qed. + +Hint Resolve check_successor_sound: ty. + +Lemma check_successors_sound: + forall sl x, check_successors sl = OK x -> forall s, In s sl -> valid_successor f s. +Proof. + induction sl; simpl; intros. + contradiction. + monadInv H. destruct H0. subst a; eauto with ty. eauto. +Qed. + +Lemma type_instr_incr: + forall e i e' te, + type_instr e i = OK e' -> satisf te e' -> satisf te e. +Proof. + intros; destruct i; try (monadInv H); eauto with ty. +- (* op *) + destruct (is_move o) eqn:ISMOVE. + destruct l; try discriminate. destruct l; monadInv EQ0. eauto with ty. + destruct (type_of_operation o) as [targs tres] eqn:TYOP. monadInv EQ0. eauto with ty. +- (* tailcall *) + destruct (opt_typ_eq (sig_res s) (sig_res (fn_sig f))); try discriminate. + destruct (tailcall_is_possible s) eqn:TCIP; inv EQ2. + eauto with ty. +- (* builtin *) + destruct (negb (ef_reloads e0) || arity_ok (sig_args (ef_sig e0))) eqn:E; inv EQ3. + eauto with ty. +- (* jumptable *) + destruct (zle (list_length_z l * 4) Int.max_unsigned); inv EQ2. + eauto with ty. +- (* return *) + simpl in H. destruct o as [r|] eqn: RET; destruct (sig_res (fn_sig f)) as [t|] eqn: RES; try discriminate. + eauto with ty. + inv H; auto with ty. +Qed. + +Lemma type_instr_sound: + forall e i e' te, + type_instr e i = OK e' -> satisf te e' -> wt_instr te f i. +Proof. + intros; destruct i; try (monadInv H); simpl. +- (* nop *) + constructor; eauto with ty. +- (* op *) + destruct (is_move o) eqn:ISMOVE. + (* move *) + + assert (o = Omove) by (unfold is_move in ISMOVE; destruct o; congruence). + subst o. + destruct l; try discriminate. destruct l; monadInv EQ0. + constructor. eapply type_move_sound; eauto. eauto with ty. + + destruct (type_of_operation o) as [targs tres] eqn:TYOP. monadInv EQ0. + apply wt_Iop. + unfold is_move in ISMOVE; destruct o; congruence. + rewrite TYOP. f_equal. eapply type_regs_sound; eauto with ty. eapply type_reg_sound; eauto. + eauto with ty. +- (* load *) constructor. - destruct s0; auto. apply check_reg_correct; auto. - apply check_regs_correct; auto. - apply check_reg_correct; auto. - apply check_successor_correct; auto. - (* tailcall *) + eapply type_regs_sound; eauto with ty. eapply type_reg_sound; eauto. + eauto with ty. +- (* store *) constructor. - destruct s0; auto. apply check_reg_correct; auto. - eapply proj_sumbool_true; eauto. - apply check_regs_correct; auto. - apply tailcall_is_possible_correct; auto. - (* builtin *) + eapply type_regs_sound; eauto with ty. eapply type_reg_sound; eauto. + eauto with ty. +- (* call *) + constructor. + eapply type_ros_sound; eauto with ty. + eapply type_regs_sound; eauto with ty. + eapply type_reg_sound; eauto. + eauto with ty. +- (* tailcall *) + destruct (opt_typ_eq (sig_res s) (sig_res (fn_sig f))); try discriminate. + destruct (tailcall_is_possible s) eqn:TCIP; inv EQ2. constructor. - apply check_regs_correct; auto. - apply check_reg_correct; auto. + eapply type_ros_sound; eauto with ty. auto. - destruct (ef_reloads e); auto. - apply check_successor_correct; auto. - (* cond *) - constructor. apply check_regs_correct; auto. - apply check_successor_correct; auto. - apply check_successor_correct; auto. - (* jumptable *) - constructor. apply check_reg_correct; auto. - rewrite List.forallb_forall in H1. intros. apply check_successor_correct; auto. - eapply proj_sumbool_true. eauto. - (* return *) - constructor. - destruct o; simpl; destruct funct.(fn_sig).(sig_res); try discriminate. - rewrite (check_reg_correct _ _ H); auto. + eapply type_regs_sound; eauto with ty. + apply tailcall_is_possible_correct; auto. +- (* builtin *) + destruct (negb (ef_reloads e0) || arity_ok (sig_args (ef_sig e0))) eqn:E; inv EQ3. + constructor. + eapply type_regs_sound; eauto with ty. + eapply type_reg_sound; eauto. + destruct (ef_reloads e0); auto. + eauto with ty. +- (* cond *) + constructor. + eapply type_regs_sound; eauto with ty. + eauto with ty. + eauto with ty. +- (* jumptable *) + destruct (zle (list_length_z l * 4) Int.max_unsigned); inv EQ2. + constructor. + eapply type_reg_sound; eauto. + eapply check_successors_sound; eauto. auto. +- (* return *) + simpl in H. destruct o as [r|] eqn: RET; destruct (sig_res (fn_sig f)) as [t|] eqn: RES; try discriminate. + constructor. simpl. rewrite RES. f_equal. eapply type_reg_sound; eauto. + inv H. constructor. rewrite RES; auto. Qed. -Lemma check_instrs_correct: - forall instrs, - check_instrs instrs = true -> - forall pc i, In (pc, i) instrs -> wt_instr env funct i. +Lemma type_code_sound: + forall e e' te, + type_code e = OK e' -> + forall pc i, f.(fn_code)!pc = Some i -> satisf te e' -> wt_instr te f i. Proof. - induction instrs; simpl; intros. - elim H0. - destruct a as [pc' i']. elimAndb. - elim H0; intro. - inversion H2; subst pc' i'. apply check_instr_correct; auto. - eauto. + intros e0 e1 te TCODE. + set (P := fun c opte => + match opte with + | Error _ => True + | OK e' => forall pc i, c!pc = Some i -> satisf te e' -> wt_instr te f i + end). + assert (P f.(fn_code) (OK e1)). + { + rewrite <- TCODE. unfold type_code. apply PTree_Properties.fold_rec; unfold P; intros. + - (* extensionality *) + destruct a; auto. intros. rewrite <- H in H1. eapply H0; eauto. + - (* base case *) + rewrite PTree.gempty in H; discriminate. + - (* inductive case *) + destruct a as [e|?]; auto. + destruct (type_instr e v) as [e'|?] eqn:TYINSTR; auto. + intros. rewrite PTree.gsspec in H2. destruct (peq pc k). + inv H2. eapply type_instr_sound; eauto. + eapply H1; eauto. eapply type_instr_incr; eauto. + } + intros; eapply H; eauto. Qed. -End TYPECHECKING. +Lemma solve_rec_incr: + forall te q e changed e' changed', + solve_rec e changed q = OK (e', changed') -> satisf te e' -> satisf te e. +Proof. + induction q; simpl; intros. +- inv H; auto. +- destruct a as [r1 r2]; monadInv H. eauto with ty. +Qed. -(** ** The type inference function **) +Lemma solve_rec_sound: + forall r1 r2 te q e changed e' changed', + solve_rec e changed q = OK (e', changed') -> satisf te e' -> In (r1, r2) q -> te r1 = te r2. +Proof. + induction q; simpl; intros. +- contradiction. +- destruct a as [r3 r4]; monadInv H. destruct H1 as [A|A]. + inv A. eapply type_move_sound; eauto. eapply solve_rec_incr; eauto. + eapply IHq; eauto. +Qed. -Open Scope string_scope. +Lemma solve_rec_false: + forall q e changed e', + solve_rec e changed q = OK (e', false) -> changed = false. +Proof. + induction q; simpl; intros. +- inv H; auto. +- destruct a as [r1 r2]; monadInv H. exploit IHq; eauto. rewrite orb_false_iff. tauto. +Qed. -Definition type_function (f: function): res regenv := - let instrs := PTree.elements f.(fn_code) in - match infer_type_environment f instrs with - | None => Error (msg "RTL type inference error") - | Some env => - if check_regs env f.(fn_params) f.(fn_sig).(sig_args) - && check_params_norepet f.(fn_params) - && check_instrs f env instrs - && check_successor f f.(fn_entrypoint) - then OK env - else Error (msg "RTL type checking error") - end. +Lemma solve_rec_solved: + forall r1 r2 q e changed e', + solve_rec e changed q = OK (e', false) -> + In (r1, r2) q -> make_regenv e r1 = make_regenv e r2. +Proof. + induction q; simpl; intros. +- contradiction. +- destruct a as [r3 r4]; monadInv H. + assert (x = false). + { exploit solve_rec_false; eauto. rewrite orb_false_iff. tauto. } + subst x. functional inversion EQ. + + destruct H0 as [A|A]. + inv A. unfold make_regenv. rewrite H1; rewrite H2; auto. + subst x0. exploit IHq; eauto. + + destruct H0 as [A|A]. + inv A. unfold make_regenv. rewrite H1; rewrite H2; auto. + subst x0. exploit IHq; eauto. +Qed. -Lemma type_function_correct: - forall f env, - type_function f = OK env -> - wt_function f env. -Proof. - unfold type_function; intros until env. - set (instrs := PTree.elements f.(fn_code)). - case (infer_type_environment f instrs). - intro env'. - caseEq (check_regs env' f.(fn_params) f.(fn_sig).(sig_args)); intro; simpl; try congruence. - caseEq (check_params_norepet f.(fn_params)); intro; simpl; try congruence. - caseEq (check_instrs f env' instrs); intro; simpl; try congruence. - caseEq (check_successor f (fn_entrypoint f)); intro; simpl; try congruence. - intro EQ; inversion EQ; subst env'. - constructor. - apply check_regs_correct; auto. - unfold check_params_norepet in H0. - destruct (list_norepet_dec Reg.eq (fn_params f)). auto. discriminate. - intros. eapply check_instrs_correct. eauto. - unfold instrs. apply PTree.elements_correct. eauto. - apply check_successor_correct. auto. +Lemma solve_equations_incr: + forall te e e', solve_equations e = OK e' -> satisf te e' -> satisf te e. +Proof. + intros te e0; functional induction (solve_equations e0); intros. +- inv H. auto. +- exploit solve_rec_incr; eauto. intros [A B]. split; intros. + apply A; auto. + eapply solve_rec_sound; eauto. +- discriminate. +Qed. + +Lemma solve_equations_sound: + forall e e', solve_equations e = OK e' -> satisf (make_regenv e') e'. +Proof. + intros e0; functional induction (solve_equations e0); intros. +- inv H. split; intros. + unfold make_regenv; rewrite H; auto. + exploit solve_rec_solved; eauto. +- eauto. +- discriminate. +Qed. + +Theorem type_function_correct: + forall env, type_function = OK env -> wt_function f env. +Proof. + unfold type_function; intros. monadInv H. + exploit solve_equations_sound; eauto. intros SAT1. + exploit solve_equations_incr; eauto. intros SAT0. + exploit type_regs_incr; eauto. intros SAT. + constructor. +- (* type of parameters *) + eapply type_regs_sound; eauto. +- (* parameters are unique *) + unfold check_params_norepet in EQ2. + destruct (list_norepet_dec Reg.eq (fn_params f)); inv EQ2; auto. +- (* instructions are well typed *) + intros; eapply type_code_sound; eauto. +- (* entry point is valid *) + eauto with ty. +Qed. + +(** ** Completeness proof *) + +Lemma type_reg_complete: + forall te e r ty, + satisf te e -> te r = ty -> exists e', type_reg e r ty = OK e' /\ satisf te e'. +Proof. + intros. unfold type_reg. + destruct ((te_typ e)!r) as [ty'|] eqn: E. + exists e; split; auto. replace ty' with ty. apply dec_eq_true. + exploit (proj1 H); eauto. congruence. + econstructor; split. reflexivity. + destruct H as [A B]; split; simpl; intros; auto. + rewrite PTree.gsspec in H. destruct (peq r0 r); auto. congruence. +Qed. + +Lemma type_regs_complete: + forall te rl tyl e, + satisf te e -> map te rl = tyl -> exists e', type_regs e rl tyl = OK e' /\ satisf te e'. +Proof. + induction rl; simpl; intros; subst tyl. + exists e; auto. + destruct (type_reg_complete te e a (te a)) as [e1 [A B]]; auto. + exploit IHrl; eauto. intros [e' [C D]]. + exists e'; split; auto. rewrite A; simpl; rewrite C; auto. +Qed. + +Lemma type_ros_complete: + forall te ros e, + satisf te e -> + match ros with inl r => te r = Tint | inr s => True end -> + exists e', type_ros e ros = OK e' /\ satisf te e'. +Proof. + intros; destruct ros; simpl. + eapply type_reg_complete; eauto. + exists e; auto. +Qed. + +Lemma type_move_complete: + forall te r1 r2 e, + satisf te e -> + te r1 = te r2 -> + exists changed e', type_move e r1 r2 = OK (changed, e') /\ satisf te e'. +Proof. + intros. functional induction (type_move e r1 r2). +- econstructor; econstructor; split; eauto. + destruct H as [A B]; split; simpl; intros; auto. + destruct H; auto. congruence. +- econstructor; econstructor; split; eauto. + destruct H as [A B]; split; simpl; intros; auto. + rewrite PTree.gsspec in H. destruct (peq r r2); auto. + subst. exploit A; eauto. congruence. +- econstructor; econstructor; split; eauto. + destruct H as [A B]; split; simpl; intros; auto. + rewrite PTree.gsspec in H. destruct (peq r r1); auto. + subst. exploit A; eauto. congruence. +- econstructor; econstructor; split; eauto. +- destruct H as [A B]. apply A in e0. apply A in e1. congruence. +Qed. + +Lemma check_successor_complete: + forall s, valid_successor f s -> check_successor s = OK tt. +Proof. + unfold valid_successor, check_successor; intros. + destruct H as [i EQ]; rewrite EQ; auto. +Qed. + +Lemma type_instr_complete: + forall te e i, + satisf te e -> + wt_instr te f i -> + exists e', type_instr e i = OK e' /\ satisf te e'. +Proof. + induction 2; simpl. +- (* nop *) + econstructor; split. rewrite check_successor_complete; simpl; eauto. auto. +- (* move *) + exploit type_move_complete; eauto. intros (changed & e' & A & B). + exists e'; split. rewrite check_successor_complete by auto; simpl. rewrite A; auto. auto. +- (* other op *) + destruct (type_of_operation op) as [targ tres]. injection H1; clear H1; intros. + exploit type_regs_complete. eauto. eauto. intros [e1 [A B]]. + exploit type_reg_complete. eexact B. eauto. intros [e2 [C D]]. + exists e2; split; auto. + rewrite check_successor_complete by auto; simpl. + replace (is_move op) with false. rewrite A; simpl; rewrite C; auto. + destruct op; reflexivity || congruence. +- (* load *) + exploit type_regs_complete. eauto. eauto. intros [e1 [A B]]. + exploit type_reg_complete. eexact B. eauto. intros [e2 [C D]]. + exists e2; split; auto. + rewrite check_successor_complete by auto; simpl. + rewrite A; simpl; rewrite C; auto. +- (* store *) + exploit type_regs_complete. eauto. eauto. intros [e1 [A B]]. + exploit type_reg_complete. eexact B. eauto. intros [e2 [C D]]. + exists e2; split; auto. + rewrite check_successor_complete by auto; simpl. + rewrite A; simpl; rewrite C; auto. +- (* call *) + exploit type_ros_complete. eauto. eauto. intros [e1 [A B]]. + exploit type_regs_complete. eauto. eauto. intros [e2 [C D]]. + exploit type_reg_complete. eexact D. eauto. intros [e3 [E F]]. + exists e3; split; auto. + rewrite check_successor_complete by auto; simpl. + rewrite A; simpl; rewrite C; simpl; rewrite E; auto. +- (* tailcall *) + exploit type_ros_complete. eauto. eauto. intros [e1 [A B]]. + exploit type_regs_complete. eauto. eauto. intros [e2 [C D]]. + exists e2; split; auto. + rewrite A; simpl; rewrite C; simpl. + rewrite H1; rewrite dec_eq_true. + replace (tailcall_is_possible sig) with true; auto. + revert H3. unfold tailcall_possible, tailcall_is_possible. generalize (loc_arguments sig). + induction l; simpl; intros. auto. + exploit (H3 a); auto. intros. destruct a; try contradiction. apply IHl. + intros; apply H3; auto. +- (* builtin *) + exploit type_regs_complete. eauto. eauto. intros [e1 [A B]]. + exploit type_reg_complete. eexact B. eauto. intros [e2 [C D]]. + exists e2; split; auto. + rewrite check_successor_complete by auto; simpl. + rewrite A; simpl; rewrite C; simpl. + destruct H2; rewrite H2. + rewrite orb_true_r. auto. + auto. +- (* cond *) + exploit type_regs_complete. eauto. eauto. intros [e1 [A B]]. + exists e1; split; auto. + rewrite check_successor_complete by auto; simpl. + rewrite check_successor_complete by auto; simpl. + auto. +- (* jumptbl *) + exploit type_reg_complete. eauto. eauto. intros [e1 [A B]]. + exists e1; split; auto. + replace (check_successors tbl) with (OK tt). simpl. + rewrite A; simpl. apply zle_true; auto. + revert H1. generalize tbl. induction tbl0; simpl; intros. auto. + rewrite check_successor_complete by auto; simpl. + apply IHtbl0; intros; auto. +- (* return *) + rewrite <- H0. destruct optres; simpl. + apply type_reg_complete; auto. + exists e; auto. +Qed. + +Lemma type_code_complete: + forall te e, + (forall pc instr, f.(fn_code)!pc = Some instr -> wt_instr te f instr) -> + satisf te e -> + exists e', type_code e = OK e' /\ satisf te e'. +Proof. + intros te e0 WTC SAT0. + set (P := fun c res => + (forall pc i, c!pc = Some i -> wt_instr te f i) -> + exists e', res = OK e' /\ satisf te e'). + assert (P f.(fn_code) (type_code e0)). + { + unfold type_code. apply PTree_Properties.fold_rec; unfold P; intros. + - apply H0. intros. apply H1 with pc. rewrite <- H; auto. + - exists e0; auto. + - destruct H1 as [e [A B]]. + intros. apply H2 with pc. rewrite PTree.gso; auto. congruence. + subst a. + destruct (type_instr_complete te e v) as [e' [C D]]. + auto. apply H2 with k. apply PTree.gss. + exists e'; split; auto. rewrite C; auto. + } + apply H; auto. +Qed. + +Lemma solve_rec_complete: + forall te q e changed, + satisf te e -> + (forall r1 r2, In (r1, r2) q -> te r1 = te r2) -> + exists e' changed', solve_rec e changed q = OK(e', changed') /\ satisf te e'. +Proof. + induction q; simpl; intros. +- exists e; exists changed; auto. +- destruct a as [r3 r4]. + exploit type_move_complete. eauto. apply H0. left; eauto. + intros (changed1 & e1 & A & B). + destruct (IHq e1 (changed || changed1)) as (e2 & changed2 & C & D); auto. + exists e2; exists changed2; split; auto. rewrite A; simpl; rewrite C; auto. +Qed. + +Lemma solve_equations_complete: + forall te e, + satisf te e -> + exists e', solve_equations e = OK e' /\ satisf te e'. +Proof. + intros te e0. functional induction (solve_equations e0); intros. +- exists e; auto. +- destruct (solve_rec_complete te (te_eqs e) {| te_typ := te_typ e; te_eqs := nil |} false) + as (e1 & changed1 & A & B). + destruct H; split; intros. apply H; auto. contradiction. + exact (proj2 H). + rewrite e0 in A. inv A. auto. +- destruct (solve_rec_complete te (te_eqs e) {| te_typ := te_typ e; te_eqs := nil |} false) + as (e1 & changed1 & A & B). + destruct H; split; intros. apply H; auto. contradiction. + exact (proj2 H). congruence. Qed. +Theorem type_function_complete: + forall te, wt_function f te -> exists te, type_function = OK te. +Proof. + intros. destruct H. + destruct (type_code_complete te {| te_typ := PTree.empty typ; te_eqs := nil |}) as (e1 & A & B). + auto. split; simpl; intros. rewrite PTree.gempty in H; congruence. contradiction. + destruct (type_regs_complete te f.(fn_params) f.(fn_sig).(sig_args) e1) as (e2 & C & D); auto. + destruct (solve_equations_complete te e2) as (e3 & E & F); auto. + exists (make_regenv e3); unfold type_function. + rewrite A; simpl. rewrite C; simpl. rewrite E; simpl. + unfold check_params_norepet. rewrite pred_dec_true; auto. simpl. + rewrite check_successor_complete by auto. auto. +Qed. + +End INFERENCE. + (** * Type preservation during evaluation *) (** The type system for RTL is not sound in that it does not guarantee diff --git a/backend/RTLtypingaux.ml b/backend/RTLtypingaux.ml deleted file mode 100644 index 5935605..0000000 --- a/backend/RTLtypingaux.ml +++ /dev/null @@ -1,170 +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 inference for RTL *) - -open Datatypes -open Camlcoq -open Maps -open AST -open Memdata -open Op -open Registers -open RTL -open PrintAST - -exception Type_error of string - -let env = ref (PTree.empty : typ PTree.t) - -let set_type r ty = - match PTree.get r !env with - | None -> env := PTree.set r ty !env - | Some ty' -> if ty <> ty' then raise (Type_error "type mismatch") - -let rec set_types rl tyl = - match rl, tyl with - | [], [] -> () - | r1 :: rs, ty1 :: tys -> set_type r1 ty1; set_types rs tys - | _, _ -> raise (Type_error "arity mismatch") - -(* First pass: process constraints of the form typeof(r) = ty *) - -let type_instr retty (pc, i) = - match i with - | Inop(_) -> - () - | Iop(Omove, _, _, _) -> - () - | Iop(op, args, res, _) -> - if two_address_op op && List.length args >= 1 && List.hd args <> res - then raise (Type_error "two-address constraint violation"); - let (targs, tres) = type_of_operation op in - set_types args targs; set_type res tres - | Iload(chunk, addr, args, dst, _) -> - set_types args (type_of_addressing addr); - set_type dst (type_of_chunk chunk) - | Istore(chunk, addr, args, src, _) -> - set_types args (type_of_addressing addr); - set_type src (type_of_chunk chunk) - | Icall(sg, ros, args, res, _) -> - begin try - begin match ros with - | Coq_inl r -> set_type r Tint - | Coq_inr _ -> () - end; - set_types args sg.sig_args; - set_type res (match sg.sig_res with None -> Tint | Some ty -> ty) - with Type_error msg -> - let name = - match ros with - | Coq_inl _ -> "" - | Coq_inr id -> extern_atom id in - raise(Type_error (Printf.sprintf "type mismatch in Icall(%s): %s" - name msg)) - end - | Itailcall(sg, ros, args) -> - begin try - begin match ros with - | Coq_inl r -> set_type r Tint - | Coq_inr _ -> () - end; - set_types args sg.sig_args; - if sg.sig_res <> retty then - raise (Type_error "mismatch on return type") - with Type_error msg -> - let name = - match ros with - | Coq_inl _ -> "" - | Coq_inr id -> extern_atom id in - raise(Type_error (Printf.sprintf "type mismatch in Itailcall(%s): %s" - name msg)) - end - | Ibuiltin(ef, args, res, _) -> - begin try - let sg = ef_sig ef in - set_types args sg.sig_args; - set_type res (match sg.sig_res with None -> Tint | Some ty -> ty); - if ef_reloads ef && not (Conventions.arity_ok sg.sig_args) then - raise(Type_error "wrong arity") - with Type_error msg -> - raise(Type_error (Printf.sprintf "type mismatch in Ibuiltin(%s): %s" - (name_of_external ef) msg)) - end - | Icond(cond, args, _, _) -> - set_types args (type_of_condition cond) - | Ijumptable(arg, _) -> - set_type arg Tint - | Ireturn(optres) -> - begin match optres, retty with - | None, None -> () - | Some r, Some ty -> set_type r ty - | _, _ -> raise (Type_error "type mismatch in Ireturn") - end - -let type_pass1 retty instrs = - List.iter (type_instr retty) instrs - -(* Second pass: extract move constraints typeof(r1) = typeof(r2) - and solve them iteratively *) - -let rec extract_moves = function - | [] -> [] - | (pc, i) :: rem -> - match i with - | Iop(Omove, [r1], r2, _) -> - (r1, r2) :: extract_moves rem - | Iop(Omove, _, _, _) -> - raise (Type_error "wrong Omove") - | _ -> - extract_moves rem - -let changed = ref false - -let rec solve_moves = function - | [] -> [] - | (r1, r2) :: rem -> - match (PTree.get r1 !env, PTree.get r2 !env) with - | Some ty1, Some ty2 -> - if ty1 = ty2 - then (changed := true; solve_moves rem) - else raise (Type_error "type mismatch in Omove") - | Some ty1, None -> - env := PTree.set r2 ty1 !env; changed := true; solve_moves rem - | None, Some ty2 -> - env := PTree.set r1 ty2 !env; changed := true; solve_moves rem - | None, None -> - (r1, r2) :: solve_moves rem - -let rec iter_solve_moves mvs = - changed := false; - let mvs' = solve_moves mvs in - if !changed then iter_solve_moves mvs' - -let type_pass2 instrs = - iter_solve_moves (extract_moves instrs) - -let typeof e r = - match PTree.get r e with Some ty -> ty | None -> Tint - -let infer_type_environment f instrs = - try - env := PTree.empty; - set_types f.fn_params f.fn_sig.sig_args; - type_pass1 f.fn_sig.sig_res instrs; - type_pass2 instrs; - let e = !env in - env := PTree.empty; - Some(typeof e) - with Type_error msg -> - Printf.eprintf "Error during RTL type inference: %s\n" msg; - None -- cgit v1.2.3