From a9a07e3b672711f74bde27bd72b518631e3a29b4 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 19 May 2019 11:24:03 +0200 Subject: If-conversion optimization for Cminor Add an experimental pass that converts some if/then/else statements into "select" built-ins, which in turn can be compiled down to branchless instruction sequences if the target architecture supports them. The statements that are converted are of the form if (cond) { x = a1; } else { x = a2; } if (cond) { x = a1; } if (cond) { /*skip*/; } else { x = a2; } where a1, a2 are "safe" expressions, containing no operations that can fail at run-time, such as memory loads or integer divisions. To support the optimization, I added a type inference and type checking pass for Cminor, in backend/Cminortyping.v. The inferred type information is used to determine the type at which the "select" built-in operates, and to prove semantic preservation. --- Makefile | 4 +- backend/Cminortyping.v | 701 +++++++++++++++++++++++++++++++++++++++++++++++++ backend/Ifconv.v | 129 +++++++++ backend/Ifconvproof.v | 590 +++++++++++++++++++++++++++++++++++++++++ driver/Compiler.v | 12 +- 5 files changed, 1433 insertions(+), 3 deletions(-) create mode 100644 backend/Cminortyping.v create mode 100644 backend/Ifconv.v create mode 100644 backend/Ifconvproof.v diff --git a/Makefile b/Makefile index 8ab6b5b0..9390c8ee 100644 --- a/Makefile +++ b/Makefile @@ -67,7 +67,9 @@ COMMON=Errors.v AST.v Linking.v \ # Back-end modules (in backend/, $(ARCH)/) BACKEND=\ - Cminor.v Op.v CminorSel.v \ + Cminor.v Cminortyping.v \ + Ifconv.v Ifconvproof.v \ + Op.v CminorSel.v \ SelectOp.v SelectDiv.v SplitLong.v SelectLong.v Selection.v \ SelectOpproof.v SelectDivproof.v SplitLongproof.v \ SelectLongproof.v Selectionproof.v \ diff --git a/backend/Cminortyping.v b/backend/Cminortyping.v new file mode 100644 index 00000000..14c80f07 --- /dev/null +++ b/backend/Cminortyping.v @@ -0,0 +1,701 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, Collège de France and Inria Paris *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +Require Import Coqlib Maps Errors. +Require Import AST Integers Floats Values Memory Globalenvs Events Smallstep. +Require Import Cminor. +Require Import Unityping. + +Local Open Scope string_scope. +Local Open Scope error_monad_scope. + +Definition type_constant (c: constant) : typ := + match c with + | Ointconst _ => Tint + | Ofloatconst _ => Tfloat + | Osingleconst _ => Tsingle + | Olongconst _ => Tlong + | Oaddrsymbol _ _ => Tptr + | Oaddrstack _ => Tptr + end. + +Definition type_unop (op: unary_operation) : typ * typ := + match op with + | Ocast8unsigned | Ocast8signed | Ocast16unsigned | Ocast16signed + | Onegint | Onotint => (Tint, Tint) + | Onegf | Oabsf => (Tfloat, Tfloat) + | Onegfs | Oabsfs => (Tsingle, Tsingle) + | Osingleoffloat => (Tfloat, Tsingle) + | Ofloatofsingle => (Tsingle, Tfloat) + | Ointoffloat | Ointuoffloat => (Tfloat, Tint) + | Ofloatofint | Ofloatofintu => (Tint, Tfloat) + | Ointofsingle | Ointuofsingle => (Tsingle, Tint) + | Osingleofint | Osingleofintu => (Tint, Tsingle) + | Onegl | Onotl => (Tlong, Tlong) + | Ointoflong => (Tlong, Tint) + | Olongofint | Olongofintu => (Tint, Tlong) + | Olongoffloat | Olonguoffloat => (Tfloat, Tlong) + | Ofloatoflong | Ofloatoflongu => (Tlong, Tfloat) + | Olongofsingle | Olonguofsingle => (Tsingle, Tlong) + | Osingleoflong | Osingleoflongu => (Tlong, Tsingle) + end. + +Definition type_binop (op: binary_operation) : typ * typ * typ := + match op with + | Oadd | Osub | Omul | Odiv | Odivu | Omod | Omodu + | Oand | Oor | Oxor | Oshl | Oshr | Oshru => (Tint, Tint, Tint) + | Oaddf | Osubf | Omulf | Odivf => (Tfloat, Tfloat, Tfloat) + | Oaddfs| Osubfs| Omulfs| Odivfs => (Tsingle, Tsingle, Tsingle) + | Oaddl | Osubl | Omull | Odivl | Odivlu | Omodl | Omodlu + | Oandl | Oorl | Oxorl => (Tlong, Tlong, Tlong) + | Oshll | Oshrl | Oshrlu => (Tlong, Tint, Tlong) + | Ocmp _ | Ocmpu _ => (Tint, Tint, Tint) + | Ocmpf _ => (Tfloat, Tfloat, Tint) + | Ocmpfs _ => (Tsingle, Tsingle, Tint) + | Ocmpl _ | Ocmplu _ => (Tlong, Tlong, Tint) + end. + +Module RTLtypes <: TYPE_ALGEBRA. + +Definition t := typ. +Definition eq := typ_eq. +Definition default := Tint. + +End RTLtypes. + +Module S := UniSolver(RTLtypes). + +Definition expect (e: S.typenv) (t1 t2: typ) : res S.typenv := + if typ_eq t1 t2 then OK e else Error (msg "type mismatch"). + +Fixpoint type_expr (e: S.typenv) (a: expr) (t: typ) : res S.typenv := + match a with + | Evar id => S.set e id t + | Econst c => expect e (type_constant c) t + | Eunop op a1 => + let '(targ1, tres) := type_unop op in + do e1 <- type_expr e a1 targ1; + expect e1 tres t + | Ebinop op a1 a2 => + let '(targ1, targ2, tres) := type_binop op in + do e1 <- type_expr e a1 targ1; + do e2 <- type_expr e1 a2 targ2; + expect e2 tres t + | Eload chunk a1 => + do e1 <- type_expr e a1 Tptr; + expect e1 (type_of_chunk chunk) t + end. + +Fixpoint type_exprlist (e: S.typenv) (al: list expr) (tl: list typ) : res S.typenv := + match al, tl with + | nil, nil => OK e + | a :: al, t :: tl => do e1 <- type_expr e a t; type_exprlist e1 al tl + | _, _ => Error (msg "arity mismatch") + end. + +Definition type_assign (e: S.typenv) (id: ident) (a: expr) : res S.typenv := + match a with + | Evar id' => + do (changed, e1) <- S.move e id id'; OK e1 + | Econst c => + S.set e id (type_constant c) + | Eunop op a1 => + let '(targ1, tres) := type_unop op in + do e1 <- type_expr e a1 targ1; + S.set e1 id tres + | Ebinop op a1 a2 => + let '(targ1, targ2, tres) := type_binop op in + do e1 <- type_expr e a1 targ1; + do e2 <- type_expr e1 a2 targ2; + S.set e2 id tres + | Eload chunk a1 => + do e1 <- type_expr e a1 Tptr; + S.set e1 id (type_of_chunk chunk) + end. + +Definition opt_set (e: S.typenv) (optid: option ident) (optty: option typ) : res S.typenv := + match optid, optty with + | None, _ => OK e + | Some id, Some ty => S.set e id ty + | _, _ => Error (msg "inconsistent call") + end. + +Fixpoint type_stmt (tret: option typ) (e: S.typenv) (s: stmt) : res S.typenv := + match s with + | Sskip => OK e + | Sassign id a => type_assign e id a + | Sstore chunk a1 a2 => + do e1 <- type_expr e a1 Tptr; type_expr e1 a2 (type_of_chunk chunk) + | Scall optid sg fn args => + do e1 <- type_expr e fn Tptr; + do e2 <- type_exprlist e1 args sg.(sig_args); + opt_set e2 optid sg.(sig_res) + | Stailcall sg fn args => + assertion (opt_typ_eq sg.(sig_res) tret); + do e1 <- type_expr e fn Tptr; + type_exprlist e1 args sg.(sig_args) + | Sbuiltin optid ef args => + let sg := ef_sig ef in + do e1 <- type_exprlist e args sg.(sig_args); + opt_set e1 optid sg.(sig_res) + | Sseq s1 s2 => + do e1 <- type_stmt tret e s1; type_stmt tret e1 s2 + | Sifthenelse a s1 s2 => + do e1 <- type_expr e a Tint; + do e2 <- type_stmt tret e1 s1; + type_stmt tret e2 s2 + | Sloop s1 => + type_stmt tret e s1 + | Sblock s1 => + type_stmt tret e s1 + | Sexit n => + OK e + | Sswitch sz a tbl dfl => + type_expr e a (if sz then Tlong else Tint) + | Sreturn opta => + match tret, opta with + | None, None => OK e + | Some t, Some a => type_expr e a t + | _, _ => Error (msg "inconsistent return") + end + | Slabel lbl s1 => + type_stmt tret e s1 + | Sgoto lbl => + OK e + end. + +Definition typenv := ident -> typ. + +Definition type_function (f: function) : res typenv := + do e1 <- S.set_list S.initial f.(fn_params) f.(fn_sig).(sig_args); + do e2 <- type_stmt f.(fn_sig).(sig_res) e1 f.(fn_body); + S.solve e2. + +(** Relational specification of the type system *) + +Section SPEC. + +Variable env: ident -> typ. +Variable tret: option typ. + +Inductive wt_expr: expr -> typ -> Prop := + | wt_Evar: forall id, + wt_expr (Evar id) (env id) + | wt_Econst: forall c, + wt_expr (Econst c) (type_constant c) + | wt_Eunop: forall op a1 targ1 tres, + type_unop op = (targ1, tres) -> + wt_expr a1 targ1 -> + wt_expr (Eunop op a1) tres + | wt_Ebinop: forall op a1 a2 targ1 targ2 tres, + type_binop op = (targ1, targ2, tres) -> + wt_expr a1 targ1 -> wt_expr a2 targ2 -> + wt_expr (Ebinop op a1 a2) tres + | wt_Eload: forall chunk a1, + wt_expr a1 Tptr -> + wt_expr (Eload chunk a1) (type_of_chunk chunk). + +Definition wt_opt_assign (optid: option ident) (optty: option typ) : Prop := + match optid with Some id => optty = Some (env id) | _ => True end. + +Inductive wt_stmt: stmt -> Prop := + | wt_Sskip: + wt_stmt Sskip + | wt_Sassign: forall id a, + wt_expr a (env id) -> + wt_stmt (Sassign id a) + | wt_Sstore: forall chunk a1 a2, + wt_expr a1 Tptr -> wt_expr a2 (type_of_chunk chunk) -> + wt_stmt (Sstore chunk a1 a2) + | wt_Scall: forall optid sg a1 al, + wt_expr a1 Tptr -> list_forall2 wt_expr al sg.(sig_args) -> + wt_opt_assign optid sg.(sig_res) -> + wt_stmt (Scall optid sg a1 al) + | wt_Stailcall: forall sg a1 al, + wt_expr a1 Tptr -> list_forall2 wt_expr al sg.(sig_args) -> + sg.(sig_res) = tret -> + wt_stmt (Stailcall sg a1 al) + | wt_Sbuiltin: forall optid ef al, + list_forall2 wt_expr al (ef_sig ef).(sig_args) -> + wt_opt_assign optid (ef_sig ef).(sig_res) -> + wt_stmt (Sbuiltin optid ef al) + | wt_Sseq: forall s1 s2, + wt_stmt s1 -> wt_stmt s2 -> + wt_stmt (Sseq s1 s2) + | wt_Sifthenelse: forall a s1 s2, + wt_expr a Tint -> wt_stmt s1 -> wt_stmt s2 -> + wt_stmt (Sifthenelse a s1 s2) + | wt_Sloop: forall s1, + wt_stmt s1 -> + wt_stmt (Sloop s1) + | wt_Sblock: forall s1, + wt_stmt s1 -> + wt_stmt (Sblock s1) + | wt_Sexit: forall n, + wt_stmt (Sexit n) + | wt_Sswitch: forall (sz: bool) a tbl dfl, + wt_expr a (if sz then Tlong else Tint) -> + wt_stmt (Sswitch sz a tbl dfl) + | wt_Sreturn_none: + tret = None -> + wt_stmt (Sreturn None) + | wt_Sreturn_some: forall a t, + tret = Some t -> wt_expr a t -> + wt_stmt (Sreturn (Some a)) + | wt_Slabel: forall lbl s1, + wt_stmt s1 -> + wt_stmt (Slabel lbl s1) + | wt_Sgoto: forall lbl, + wt_stmt (Sgoto lbl). + +End SPEC. + +Inductive wt_function (env: typenv) (f: function) : Prop := + wt_function_intro: + type_function f = OK env -> (**r to ensure uniqueness of [env] *) + List.map env f.(fn_params) = f.(fn_sig).(sig_args) -> + wt_stmt env f.(fn_sig).(sig_res) f.(fn_body) -> + wt_function env f. + +Inductive wt_fundef: fundef -> Prop := + | wt_fundef_internal: forall env f, + wt_function env f -> + wt_fundef (Internal f) + | wt_fundef_external: forall ef, + wt_fundef (External ef). + +Definition wt_program (p: program): Prop := + forall i f, In (i, Gfun f) (prog_defs p) -> wt_fundef f. + +(** Soundness of type inference *) + +Lemma expect_incr: forall te e t1 t2 e', + expect e t1 t2 = OK e' -> S.satisf te e' -> S.satisf te e. +Proof. + unfold expect; intros. destruct (typ_eq t1 t2); inv H; auto. +Qed. +Hint Resolve expect_incr: ty. + +Lemma expect_sound: forall e t1 t2 e', + expect e t1 t2 = OK e' -> t1 = t2. +Proof. + unfold expect; intros. destruct (typ_eq t1 t2); inv H; auto. +Qed. + +Lemma type_expr_incr: forall te a t e e', + type_expr e a t = OK e' -> S.satisf te e' -> S.satisf te e. +Proof. + induction a; simpl; intros until e'; intros T SAT; try (monadInv T); eauto with ty. +- destruct (type_unop u) as [targ1 tres]; monadInv T; eauto with ty. +- destruct (type_binop b) as [[targ1 targ2] tres]; monadInv T; eauto with ty. +Qed. +Hint Resolve type_expr_incr: ty. + +Lemma type_expr_sound: forall te a t e e', + type_expr e a t = OK e' -> S.satisf te e' -> wt_expr te a t. +Proof. + induction a; simpl; intros until e'; intros T SAT; try (monadInv T). +- erewrite <- S.set_sound by eauto. constructor. +- erewrite <- expect_sound by eauto. constructor. +- destruct (type_unop u) as [targ1 tres] eqn:TU; monadInv T. + erewrite <- expect_sound by eauto. econstructor; eauto with ty. +- destruct (type_binop b) as [[targ1 targ2] tres] eqn:TB; monadInv T. + erewrite <- expect_sound by eauto. econstructor; eauto with ty. +- erewrite <- expect_sound by eauto. econstructor; eauto with ty. +Qed. + +Lemma type_exprlist_incr: forall te al tl e e', + type_exprlist e al tl = OK e' -> S.satisf te e' -> S.satisf te e. +Proof. + induction al; destruct tl; simpl; intros until e'; intros T SAT; monadInv T; eauto with ty. +Qed. +Hint Resolve type_exprlist_incr: ty. + +Lemma type_exprlist_sound: forall te al tl e e', + type_exprlist e al tl = OK e' -> S.satisf te e' -> list_forall2 (wt_expr te) al tl. +Proof. + induction al; destruct tl; simpl; intros until e'; intros T SAT; monadInv T. +- constructor. +- constructor; eauto using type_expr_sound with ty. +Qed. + +Lemma type_assign_incr: forall te id a e e', + type_assign e id a = OK e' -> S.satisf te e' -> S.satisf te e. +Proof. + induction a; simpl; intros until e'; intros T SAT; try (monadInv T); eauto with ty. +- destruct (type_unop u) as [targ1 tres]; monadInv T; eauto with ty. +- destruct (type_binop b) as [[targ1 targ2] tres]; monadInv T; eauto with ty. +Qed. +Hint Resolve type_assign_incr: ty. + +Lemma type_assign_sound: forall te id a e e', + type_assign e id a = OK e' -> S.satisf te e' -> wt_expr te a (te id). +Proof. + induction a; simpl; intros until e'; intros T SAT; try (monadInv T). +- erewrite S.move_sound by eauto. constructor. +- erewrite S.set_sound by eauto. constructor. +- destruct (type_unop u) as [targ1 tres] eqn:TU; monadInv T. + erewrite S.set_sound by eauto. econstructor; eauto using type_expr_sound with ty. +- destruct (type_binop b) as [[targ1 targ2] tres] eqn:TB; monadInv T. + erewrite S.set_sound by eauto. econstructor; eauto using type_expr_sound with ty. +- erewrite S.set_sound by eauto. econstructor; eauto using type_expr_sound with ty. +Qed. + +Lemma opt_set_incr: forall te optid optty e e', + opt_set e optid optty = OK e' -> S.satisf te e' -> S.satisf te e. +Proof. + unfold opt_set; intros. destruct optid, optty; try (monadInv H); eauto with ty. +Qed. +Hint Resolve opt_set_incr: ty. + +Lemma opt_set_sound: forall te optid optty e e', + opt_set e optid optty = OK e' -> S.satisf te e' -> wt_opt_assign te optid optty. +Proof. + unfold opt_set; intros; red. destruct optid; [destruct optty |]; try (monadInv H). +- erewrite S.set_sound by eauto. auto. +- auto. +Qed. + +Lemma type_stmt_incr: forall te tret s e e', + type_stmt tret e s = OK e' -> S.satisf te e' -> S.satisf te e. +Proof. + induction s; simpl; intros e1 e2 T SAT; try (monadInv T); eauto with ty. +- destruct tret, o; try (monadInv T); eauto with ty. +Qed. +Hint Resolve type_stmt_incr: ty. + +Lemma type_stmt_sound: forall te tret s e e', + type_stmt tret e s = OK e' -> S.satisf te e' -> wt_stmt te tret s. +Proof. + induction s; simpl; intros e1 e2 T SAT; try (monadInv T). +- constructor. +- constructor; eauto using type_assign_sound. +- constructor; eauto using type_expr_sound with ty. +- constructor; eauto using type_expr_sound, type_exprlist_sound, opt_set_sound with ty. +- constructor; eauto using type_expr_sound, type_exprlist_sound with ty. +- constructor; eauto using type_exprlist_sound, opt_set_sound with ty. +- constructor; eauto with ty. +- constructor; eauto using type_expr_sound with ty. +- constructor; eauto. +- constructor; eauto. +- constructor. +- constructor; eauto using type_expr_sound with ty. +- destruct tret, o; try (monadInv T); econstructor; eauto using type_expr_sound with ty. +- constructor; eauto. +- constructor. +Qed. + +Theorem type_function_sound: forall f env, + type_function f = OK env -> wt_function env f. +Proof. + intros. generalize H; unfold type_function; intros T; monadInv T. + assert (S.satisf env x0) by (apply S.solve_sound; auto). + constructor; eauto using S.set_list_sound, type_stmt_sound with ty. +Qed. + +(** Semantic soundness *) + +Definition wt_env (env: typenv) (e: Cminor.env) : Prop := + forall id v, e!id = Some v -> Val.has_type v (env id). + +Definition def_env (f: function) (e: Cminor.env) : Prop := + forall id, In id f.(fn_params) \/ In id f.(fn_vars) -> exists v, e!id = Some v. + +Inductive wt_cont_call: cont -> option typ -> Prop := + | wt_cont_Kstop: + wt_cont_call Kstop (Some Tint) + | wt_cont_Kcall: forall optid f sp e k tret env + (WT_FN: wt_function env f) + (WT_CONT: wt_cont env f.(fn_sig).(sig_res) k) + (WT_ENV: wt_env env e) + (DEF_ENV: def_env f e) + (WT_DEST: wt_opt_assign env optid tret), + wt_cont_call (Kcall optid f sp e k) tret + +with wt_cont: typenv -> option typ -> cont -> Prop := + | wt_cont_Kseq: forall env tret s k, + wt_stmt env tret s -> + wt_cont env tret k -> + wt_cont env tret (Kseq s k) + | wt_cont_Kblock: forall env tret k, + wt_cont env tret k -> + wt_cont env tret (Kblock k) + | wt_cont_other: forall env tret k, + wt_cont_call k tret -> + wt_cont env tret k. + +Inductive wt_state: state -> Prop := + | wt_normal_state: forall f s k sp e m env + (WT_FN: wt_function env f) + (WT_STMT: wt_stmt env f.(fn_sig).(sig_res) s) + (WT_CONT: wt_cont env f.(fn_sig).(sig_res) k) + (WT_ENV: wt_env env e) + (DEF_ENV: def_env f e), + wt_state (State f s k sp e m) + | wt_call_state: forall f args k m + (WT_FD: wt_fundef f) + (WT_ARGS: Val.has_type_list args (funsig f).(sig_args)) + (WT_CONT: wt_cont_call k (funsig f).(sig_res)), + wt_state (Callstate f args k m) + | wt_return_state: forall v k m tret + (WT_RES: Val.has_type v (match tret with None => Tint | Some t => t end)) + (WT_CONT: wt_cont_call k tret), + wt_state (Returnstate v k m). + +Lemma wt_is_call_cont: + forall env tret k, wt_cont env tret k -> is_call_cont k -> wt_cont_call k tret. +Proof. + destruct 1; intros ICC; contradiction || auto. +Qed. + +Lemma call_cont_wt: + forall env tret k, wt_cont env tret k -> wt_cont_call (call_cont k) tret. +Proof. + induction 1; simpl; auto. inversion H; subst; auto. +Qed. + +Lemma wt_env_assign: forall env id e v, + wt_env env e -> Val.has_type v (env id) -> wt_env env (PTree.set id v e). +Proof. + intros; red; intros. rewrite PTree.gsspec in H1; destruct (peq id0 id). +- congruence. +- auto. +Qed. + +Lemma def_env_assign: forall f e id v, + def_env f e -> def_env f (PTree.set id v e). +Proof. + intros; red; intros i IN. rewrite PTree.gsspec. destruct (peq i id). + exists v; auto. + auto. +Qed. + +Lemma wt_env_set_params: forall env il vl, + Val.has_type_list vl (map env il) -> wt_env env (set_params vl il). +Proof. + induction il as [ | i il]; destruct vl as [ | vl]; simpl; intros; try contradiction. +- red; intros. rewrite PTree.gempty in H0; discriminate. +- destruct H. apply wt_env_assign; auto. +Qed. + +Lemma def_set_params: forall id il vl, + In id il -> exists v, PTree.get id (set_params vl il) = Some v. +Proof. + induction il as [ | i il]; simpl; intros. +- contradiction. +- destruct vl as [ | v vl]; rewrite PTree.gsspec; destruct (peq id i). + econstructor; eauto. + apply IHil; intuition congruence. + econstructor; eauto. + apply IHil; intuition congruence. +Qed. + +Lemma wt_env_set_locals: forall env il e, + wt_env env e -> wt_env env (set_locals il e). +Proof. + induction il as [ | i il]; simpl; intros. +- auto. +- apply wt_env_assign; auto. exact I. +Qed. + +Lemma def_set_locals: forall id il e, + (exists v, PTree.get id e = Some v) \/ In id il -> + exists v, PTree.get id (set_locals il e) = Some v. +Proof. + induction il as [ | i il]; simpl; intros. +- tauto. +- rewrite PTree.gsspec; destruct (peq id i). + econstructor; eauto. + apply IHil; intuition congruence. +Qed. + +Lemma wt_find_label: forall env tret lbl s k, + wt_stmt env tret s -> wt_cont env tret k -> + match find_label lbl s k with + | Some (s', k') => wt_stmt env tret s' /\ wt_cont env tret k' + | None => True + end. +Proof. + induction s; intros k WS WK; simpl; auto. +- inv WS. assert (wt_cont env tret (Kseq s2 k)) by (constructor; auto). + specialize (IHs1 _ H1 H). destruct (find_label lbl s1 (Kseq s2 k)). + auto. apply IHs2; auto. +- inv WS. specialize (IHs1 _ H3 WK). destruct (find_label lbl s1 k). + auto. apply IHs2; auto. +- inversion WS; subst. apply IHs; auto. constructor; auto. +- inv WS. apply IHs; auto. constructor; auto. +- inv WS. destruct (ident_eq lbl l). auto. apply IHs; auto. +Qed. + +Section SUBJECT_REDUCTION. + +Variable p: program. + +Hypothesis wt_p: wt_program p. + +Let ge := Genv.globalenv p. + +Ltac VHT := + match goal with + | [ |- Val.has_type (if Archi.ptr64 then _ else _) _] => unfold Val.has_type; destruct Archi.ptr64 eqn:?; VHT + | [ |- Val.has_type (match ?v with _ => _ end) _] => destruct v; VHT + | [ |- Val.has_type (Vptr _ _) Tptr ] => apply Val.Vptr_has_type + | [ |- Val.has_type _ _ ] => exact I + | [ |- Val.has_type (?f _ _ _ _ _) _ ] => unfold f; VHT + | [ |- Val.has_type (?f _ _ _ _) _ ] => unfold f; VHT + | [ |- Val.has_type (?f _ _) _ ] => unfold f; VHT + | [ |- Val.has_type (?f _ _ _) _ ] => unfold f; VHT + | [ |- Val.has_type (?f _) _ ] => unfold f; VHT + | [ |- True ] => exact I + | [ |- ?x = ?x ] => reflexivity + | _ => idtac + end. + +Ltac VHT' := + match goal with + | [ H: None = Some _ |- _ ] => discriminate + | [ H: Some _ = Some _ |- _ ] => inv H; VHT + | [ H: match ?x with _ => _ end = Some _ |- _ ] => destruct x; VHT' + | [ H: ?f _ _ _ _ = Some _ |- _ ] => unfold f in H; VHT' + | [ H: ?f _ _ _ = Some _ |- _ ] => unfold f in H; VHT' + | [ H: ?f _ _ = Some _ |- _ ] => unfold f in H; VHT' + | [ H: ?f _ = Some _ |- _ ] => unfold f in H; VHT' + | _ => idtac + end. + +Lemma type_constant_sound: forall sp cst v, + eval_constant ge sp cst = Some v -> + Val.has_type v (type_constant cst). +Proof. + intros until v; intros EV. destruct cst; simpl in *; inv EV; VHT. +Qed. + +Lemma type_unop_sound: forall op v1 v, + eval_unop op v1 = Some v -> Val.has_type v (snd (type_unop op)). +Proof. + unfold eval_unop; intros op v1 v EV; destruct op; simpl; VHT'. +Qed. + +Lemma type_binop_sound: forall op v1 v2 m v, + eval_binop op v1 v2 m = Some v -> Val.has_type v (snd (type_binop op)). +Proof. + unfold eval_binop; intros op v1 v2 m v EV; destruct op; simpl; VHT'; + destruct (eq_block b b0); VHT. +Qed. + +Lemma wt_eval_expr: forall env sp e m a v, + eval_expr ge sp e m a v -> + forall t, + wt_expr env a t -> + wt_env env e -> + Val.has_type v t. +Proof. + induction 1; intros t WT ENV. +- inv WT. apply ENV; auto. +- inv WT. eapply type_constant_sound; eauto. +- inv WT. replace t with (snd (type_unop op)) by (rewrite H3; auto). eapply type_unop_sound; eauto. +- inv WT. replace t with (snd (type_binop op)) by (rewrite H5; auto). eapply type_binop_sound; eauto. +- inv WT. destruct vaddr; try discriminate. eapply Mem.load_type; eauto. +Qed. + +Lemma wt_eval_exprlist: forall env sp e m al vl, + eval_exprlist ge sp e m al vl -> + forall tl, + list_forall2 (wt_expr env) al tl -> + wt_env env e -> + Val.has_type_list vl tl. +Proof. + induction 1; intros tl WT ENV; inv WT; simpl. +- auto. +- split. eapply wt_eval_expr; eauto. eauto. +Qed. + +Lemma wt_find_funct: forall v fd, + Genv.find_funct ge v = Some fd -> wt_fundef fd. +Proof. + intros. eapply Genv.find_funct_prop; eauto. +Qed. + +Lemma subject_reduction: + forall st1 t st2, step ge st1 t st2 -> + forall (WT: wt_state st1), wt_state st2. +Proof. + destruct 1; intros; inv WT. +- inv WT_CONT. econstructor; eauto. inv H. +- inv WT_CONT. econstructor; eauto. inv H. +- econstructor; eauto using wt_is_call_cont. exact I. +- inv WT_STMT. econstructor; eauto using wt_Sskip. + apply wt_env_assign; auto. eapply wt_eval_expr; eauto. + apply def_env_assign; auto. +- econstructor; eauto using wt_Sskip. +- inv WT_STMT. econstructor; eauto. + eapply wt_find_funct; eauto. + eapply wt_eval_exprlist; eauto. + econstructor; eauto. +- inv WT_STMT. econstructor; eauto. + eapply wt_find_funct; eauto. + eapply wt_eval_exprlist; eauto. + rewrite H8; eapply call_cont_wt; eauto. +- inv WT_STMT. exploit external_call_well_typed; eauto. intros TRES. + econstructor; eauto using wt_Sskip. + unfold proj_sig_res in TRES; red in H5. + destruct optid. rewrite H5 in TRES. apply wt_env_assign; auto. assumption. + destruct optid. apply def_env_assign; auto. assumption. +- inv WT_STMT. econstructor; eauto. econstructor; eauto. +- inv WT_STMT. destruct b; econstructor; eauto. +- inv WT_STMT. econstructor; eauto. econstructor; eauto. constructor; auto. +- inv WT_STMT. econstructor; eauto. econstructor; eauto. +- inv WT_CONT. econstructor; eauto. inv H. +- inv WT_CONT. econstructor; eauto using wt_Sskip. inv H. +- inv WT_CONT. econstructor; eauto using wt_Sexit. inv H. +- econstructor; eauto using wt_Sexit. +- inv WT_STMT. econstructor; eauto using call_cont_wt. rewrite H0; exact I. +- inv WT_STMT. econstructor; eauto using call_cont_wt. + rewrite H2. eapply wt_eval_expr; eauto. +- inv WT_STMT. econstructor; eauto. +- inversion WT_FN; subst. + assert (WT_CK: wt_cont env (sig_res (fn_sig f)) (call_cont k)). + { constructor. eapply call_cont_wt; eauto. } + generalize (wt_find_label _ _ lbl _ _ H2 WT_CK). + rewrite H. intros [WT_STMT' WT_CONT']. econstructor; eauto. +- inv WT_FD. inversion H1; subst. econstructor; eauto. + constructor; auto. + apply wt_env_set_locals. apply wt_env_set_params. rewrite H2; auto. + red; intros. apply def_set_locals. destruct H4; auto. left; apply def_set_params; auto. +- exploit external_call_well_typed; eauto. unfold proj_sig_res. simpl in *. intros. + econstructor; eauto. +- inv WT_CONT. econstructor; eauto using wt_Sskip. + red in WT_DEST. + destruct optid. rewrite WT_DEST in WT_RES. apply wt_env_assign; auto. assumption. + destruct optid. apply def_env_assign; auto. assumption. +Qed. + +Lemma subject_reduction_star: + forall st1 t st2, star step ge st1 t st2 -> + forall (WT: wt_state st1), wt_state st2. +Proof. + induction 1; eauto using subject_reduction. +Qed. + + +Lemma wt_initial_state: + forall S, initial_state p S -> wt_state S. +Proof. + intros. inv H. constructor. eapply Genv.find_funct_ptr_prop; eauto. + rewrite H3; constructor. + rewrite H3; constructor. +Qed. + +End SUBJECT_REDUCTION. diff --git a/backend/Ifconv.v b/backend/Ifconv.v new file mode 100644 index 00000000..0c9c5b5c --- /dev/null +++ b/backend/Ifconv.v @@ -0,0 +1,129 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, Collège de France and Inria Paris *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +Require Import Coqlib Maps Errors. +Require Import AST Events Cminor. +Require Import Cminortyping. + +Definition tyenv := ident -> typ. +Definition known_idents := PTree.t unit. + +Definition is_known (ki: known_idents) (id: ident) := + match ki!id with Some _ => true | None => false end. + +Definition safe_unop (op: unary_operation) : bool := + match op with + | Ointoffloat | Ointuoffloat | Ofloatofint | Ofloatofintu => false + | Ointofsingle | Ointuofsingle | Osingleofint | Osingleofintu => false + | Olongoffloat | Olonguoffloat | Ofloatoflong | Ofloatoflongu => false + | Olongofsingle | Olonguofsingle | Osingleoflong | Osingleoflongu => false + | _ => true + end. + +Definition safe_binop (op: binary_operation) : bool := + match op with + | Odiv | Odivu | Omod | Omodu => false + | Odivl | Odivlu | Omodl | Omodlu => false + | Ocmpl _ | Ocmplu _ => false + | _ => true + end. + +Fixpoint safe_expr (ki: known_idents) (a: expr) : bool := + match a with + | Evar v => is_known ki v + | Econst c => true + | Eunop op e1 => safe_unop op && safe_expr ki e1 + | Ebinop op e1 e2 => safe_binop op && safe_expr ki e1 && safe_expr ki e2 + | Eload chunk e => false + end. + +Definition Sselection (id: ident) (ty: typ) (cond ifso ifnot: expr) : stmt := + Sbuiltin (Some id) (EF_select ty) (cond :: ifso :: ifnot :: nil). + +Inductive stmt_class : Type := + | SCskip + | SCassign (id: ident) (a: expr) + | SCother. + +Function classify_stmt (s: stmt) : stmt_class := + match s with + | Sskip => SCskip + | Sassign id a => SCassign id a + | Sseq Sskip s => classify_stmt s + | Sseq s Sskip => classify_stmt s + | _ => SCother + end. + +Definition if_conversion_base + (ki: known_idents) (env: tyenv) + (cond: expr) (id: ident) (ifso ifnot: expr) : option stmt := + if is_known ki id && safe_expr ki ifso && safe_expr ki ifnot + then Some (Sselection id (env id) cond ifso ifnot) + else None. + +Definition if_conversion + (ki: known_idents) (env: tyenv) + (cond: expr) (ifso ifnot: stmt) : option stmt := + match classify_stmt ifso, classify_stmt ifnot with + | SCskip, SCassign id a => + if_conversion_base ki env cond id (Evar id) a + | SCassign id a, SCskip => + if_conversion_base ki env cond id a (Evar id) + | SCassign id1 a1, SCassign id2 a2 => + if ident_eq id1 id2 then if_conversion_base ki env cond id1 a1 a2 else None + | _, _ => None + end. + +Fixpoint transf_stmt (ki: known_idents) (env: tyenv) (s: stmt) : stmt := + match s with + | Sskip => s + | Sassign _ _ => s + | Sstore _ _ _ => s + | Scall _ _ _ _ => s + | Stailcall _ _ _ => s + | Sbuiltin _ _ _ => s + | Sseq s1 s2 => Sseq (transf_stmt ki env s1) (transf_stmt ki env s2) + | Sifthenelse e s1 s2 => + match if_conversion ki env e s1 s2 with + | Some s => s + | None => Sifthenelse e (transf_stmt ki env s1) (transf_stmt ki env s2) + end + | Sloop s1 => Sloop (transf_stmt ki env s1) + | Sblock s1 => Sblock (transf_stmt ki env s1) + | Sexit _ => s + | Sswitch _ _ _ _ => s + | Sreturn _ => s + | Slabel lbl s1 => Slabel lbl (transf_stmt ki env s1) + | Sgoto _ => s + end. + +Definition known_id (f: function) : known_idents := + let add (ki: known_idents) (id: ident) := PTree.set id tt ki in + List.fold_left add f.(fn_vars) + (List.fold_left add f.(fn_params) (PTree.empty unit)). + +Local Open Scope error_monad_scope. + +Definition transf_function (f: function) : res function := + let ki := known_id f in + do env <- type_function f; + OK (mkfunction f.(fn_sig) f.(fn_params) f.(fn_vars) f.(fn_stackspace) + (transf_stmt ki env f.(fn_body))). + +Definition transf_fundef (fd: fundef) : res fundef := + transf_partial_fundef transf_function fd. + +Definition transf_program (p: program) : res program := + transform_partial_program transf_fundef p. diff --git a/backend/Ifconvproof.v b/backend/Ifconvproof.v new file mode 100644 index 00000000..9e14ce2f --- /dev/null +++ b/backend/Ifconvproof.v @@ -0,0 +1,590 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, Collège de France and Inria Paris *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +Require Import Recdef Coqlib Maps Errors. +Require Import AST Linking. +Require Import Values Memory Events Globalenvs Smallstep. +Require Import Cminor Cminortyping Ifconv. + +Definition match_prog (prog tprog: program) := + match_program (fun cu f tf => transf_fundef f = OK tf) eq prog tprog. + +Lemma transf_program_match: + forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog. +Proof. + intros. apply match_transform_partial_program; auto. +Qed. + +Lemma known_id_sound_1: + forall f id x, (known_id f)!id = Some x -> In id f.(fn_params) \/ In id f.(fn_vars). +Proof. + unfold known_id. + set (add := fun (ki: known_idents) (id: ident) => PTree.set id tt ki). + intros. + assert (REC: forall l ki, (fold_left add l ki)!id = Some x -> In id l \/ ki!id = Some x). + { induction l as [ | i l ]; simpl; intros. + - auto. + - apply IHl in H0. destruct H0; auto. unfold add in H0; rewrite PTree.gsspec in H0. + destruct (peq id i); auto. } + apply REC in H. destruct H; auto. apply REC in H. destruct H; auto. + rewrite PTree.gempty in H; discriminate. +Qed. + +Lemma known_id_sound_2: + forall f id, is_known (known_id f) id = true -> In id f.(fn_params) \/ In id f.(fn_vars). +Proof. + unfold is_known; intros. destruct (known_id f)!id eqn:E; try discriminate. + eapply known_id_sound_1; eauto. +Qed. + +Lemma eval_safe_expr: + forall ge f sp e m a, + def_env f e -> + safe_expr (known_id f) a = true -> + exists v, eval_expr ge sp e m a v. +Proof. + induction a; simpl; intros. + - apply known_id_sound_2 in H0. + destruct (H i H0) as [v E]. + exists v; constructor; auto. + - destruct (eval_constant ge sp c) as [v|] eqn:E. + exists v; constructor; auto. + destruct c; discriminate. + - InvBooleans. destruct IHa as [v1 E1]; auto. + destruct (eval_unop u v1) as [v|] eqn:E. + exists v; econstructor; eauto. + destruct u; discriminate. + - InvBooleans. + destruct IHa1 as [v1 E1]; auto. + destruct IHa2 as [v2 E2]; auto. + destruct (eval_binop b v1 v2 m) as [v|] eqn:E. + exists v; econstructor; eauto. + destruct b; discriminate. + - discriminate. +Qed. + +Lemma step_selection: + forall ge f id ty cond a1 a2 k sp e m v0 b v1 v2, + eval_expr ge sp e m cond v0 -> Val.bool_of_val v0 b -> + eval_expr ge sp e m a1 v1 -> + eval_expr ge sp e m a2 v2 -> + Val.has_type v1 ty -> Val.has_type v2 ty -> + step ge (State f (Sselection id ty cond a1 a2) k sp e m) + E0 (State f Sskip k sp (PTree.set id (if b then v1 else v2) e) m). +Proof. + unfold Sselection; intros. + eapply step_builtin with (optid := Some id). + eauto 6 using eval_Enil, eval_Econs. + replace (if b then v1 else v2) with (Val.select (Some b) v1 v2 ty). + constructor; auto. + destruct b; apply Val.normalize_idem; auto. +Qed. + +Section PRESERVATION. + +Variable prog: program. +Variable tprog: program. +Hypothesis TRANSL: match_prog prog tprog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +Lemma wt_prog : wt_program prog. +Proof. + red; intros. + destruct TRANSL as [A _]. + exploit list_forall2_in_left; eauto. + intros ((i' & gd') & B & (C & D)). simpl in *. inv D. + destruct f; monadInv H2. +- monadInv EQ. econstructor; apply type_function_sound; eauto. +- constructor. +Qed. + +Lemma symbols_preserved: + forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. +Proof (Genv.find_symbol_match TRANSL). + +Lemma senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_match TRANSL). + +Lemma function_ptr_translated: + forall b f, + Genv.find_funct_ptr ge b = Some f -> + exists tf, + Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf. +Proof + (Genv.find_funct_ptr_transf_partial TRANSL). + +Lemma functions_translated: + forall v f, + Genv.find_funct ge v = Some f -> + exists tf, + Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf. +Proof + (Genv.find_funct_transf_partial TRANSL). + +Lemma sig_transf_function: + forall f tf, + transf_fundef f = OK tf -> + funsig tf = funsig f. +Proof. + unfold transf_fundef, transf_partial_fundef; intros. destruct f. +- monadInv H. monadInv EQ. auto. +- inv H. auto. +Qed. + +Lemma stackspace_transf_function: + forall f tf, + transf_function f = OK tf -> + tf.(fn_stackspace) = f.(fn_stackspace). +Proof. + intros. monadInv H. auto. +Qed. + +Lemma eval_expr_preserved: + forall sp e m a v, eval_expr ge sp e m a v -> eval_expr tge sp e m a v. +Proof. + induction 1; econstructor; eauto. + destruct cst; auto. + simpl in *. unfold Genv.symbol_address in *. rewrite symbols_preserved. auto. +Qed. + +Lemma eval_exprlist_preserved: + forall sp e m al vl, eval_exprlist ge sp e m al vl -> eval_exprlist tge sp e m al vl. +Proof. + induction 1; econstructor; eauto using eval_expr_preserved. +Qed. + +(* +Lemma classify_stmt_sound: + forall f sp e m s, + match classify_stmt s with + | SCskip => + forall k, star step ge (State f s k sp e m) E0 (State f Sskip k sp e m) + | SCassign id a => + forall k v, + eval_expr ge sp e m a v -> + star step ge (State f s k sp e m) E0 (State f Sskip k sp (PTree.set id v e) m) + | SCother => True + end. +Proof. + intros until s; functional induction (classify_stmt s). + - intros; apply star_refl. + - intros; apply star_one; constructor; auto. + - assert (A: forall k, star step ge (State f (Sseq Sskip s0) k sp e m) + E0 (State f s0 k sp e m)). + { intros. eapply star_two; constructor. } + destruct (classify_stmt s0); auto; + intros; (eapply star_trans; [apply A| auto | reflexivity]). + - destruct (classify_stmt s0); auto. + + intros. eapply star_left. constructor. eapply star_right. + apply IHs0. constructor. eauto. eauto. + + intros. eapply star_left. constructor. eapply star_right. + apply IHs0. eauto. constructor. eauto. eauto. + - auto. +Qed. +*) + +Lemma classify_stmt_sound_1: + forall f sp e m s k, + classify_stmt s = SCskip -> + star step ge (State f s k sp e m) E0 (State f Sskip k sp e m). +Proof. + intros until s; functional induction (classify_stmt s); intros; try discriminate. + - apply star_refl. + - eapply star_trans; eauto. eapply star_two. constructor. constructor. + traceEq. traceEq. + - eapply star_left. constructor. + eapply star_right. eauto. constructor. + traceEq. traceEq. +Qed. + +Lemma classify_stmt_sound_2: + forall f sp e m a id v, + eval_expr ge sp e m a v -> + forall s k, + classify_stmt s = SCassign id a -> + star step ge (State f s k sp e m) E0 (State f Sskip k sp (PTree.set id v e) m). +Proof. + intros until s; functional induction (classify_stmt s); intros; try discriminate. + - inv H0. apply star_one. constructor; auto. + - eapply star_trans; eauto. eapply star_two. constructor. constructor. + traceEq. traceEq. + - eapply star_left. constructor. + eapply star_right. eauto. constructor. + traceEq. traceEq. +Qed. + +Lemma classify_stmt_wt_2: + forall env tyret id a s, + classify_stmt s = SCassign id a -> + wt_stmt env tyret s -> + wt_expr env a (env id). +Proof. + intros until s; functional induction (classify_stmt s); intros CL WT; + try discriminate. +- inv CL; inv WT; auto. +- inv WT; eauto. +- inv WT; eauto. +Qed. + +Lemma if_conversion_sound: + forall f env cond ifso ifnot s vb b k f' k' sp e m, + if_conversion (known_id f) env cond ifso ifnot = Some s -> + def_env f e -> wt_env env e -> + wt_stmt env f.(fn_sig).(sig_res) ifso -> + wt_stmt env f.(fn_sig).(sig_res) ifnot -> + eval_expr ge sp e m cond vb -> Val.bool_of_val vb b -> + let s0 := if b then ifso else ifnot in + exists e1, + step tge (State f' s k' sp e m) E0 (State f' Sskip k' sp e1 m) + /\ star step ge (State f s0 k sp e m) E0 (State f Sskip k sp e1 m). +Proof. + unfold if_conversion; intros until m; intros IFC DE WTE WT1 WT2 EVC BOV. + set (s0 := if b then ifso else ifnot). set (ki := known_id f) in *. + destruct (classify_stmt ifso) eqn:IFSO; try discriminate; + destruct (classify_stmt ifnot) eqn:IFNOT; try discriminate; + unfold if_conversion_base in IFC. + - destruct (is_known ki id && safe_expr ki (Evar id) && safe_expr ki a) eqn:B; inv IFC. + InvBooleans. + destruct (eval_safe_expr ge f sp e m (Evar id)) as (v1 & EV1); auto. + destruct (eval_safe_expr ge f sp e m a) as (v2 & EV2); auto. + assert (Val.has_type v1 (env id)). + { eapply wt_eval_expr; eauto using wt_prog. constructor. } + assert (Val.has_type v2 (env id)). + { eapply wt_eval_expr; eauto using wt_prog. eapply classify_stmt_wt_2; eauto. } + econstructor; split. + eapply step_selection; eauto using eval_expr_preserved. + unfold s0; destruct b. + rewrite PTree.gsident by (inv EV1; auto). apply classify_stmt_sound_1; auto. + eapply classify_stmt_sound_2; eauto. + - destruct (is_known ki id && safe_expr ki a && safe_expr ki (Evar id)) eqn:B; inv IFC. + InvBooleans. + destruct (eval_safe_expr ge f sp e m a) as (v1 & EV1); auto. + destruct (eval_safe_expr ge f sp e m (Evar id)) as (v2 & EV2); auto. + assert (Val.has_type v1 (env id)). + { eapply wt_eval_expr; eauto using wt_prog. eapply classify_stmt_wt_2; eauto. } + assert (Val.has_type v2 (env id)). + { eapply wt_eval_expr; eauto using wt_prog. constructor. } + econstructor; split. + eapply step_selection; eauto using eval_expr_preserved. + unfold s0; destruct b. + eapply classify_stmt_sound_2; eauto. + rewrite PTree.gsident by (inv EV2; auto). apply classify_stmt_sound_1; auto. + - destruct (ident_eq id id0); try discriminate. subst id0. + destruct (is_known ki id && safe_expr ki a && safe_expr ki a0) eqn:B; inv IFC. + InvBooleans. + destruct (eval_safe_expr ge f sp e m a) as (v1 & EV1); auto. + destruct (eval_safe_expr ge f sp e m a0) as (v2 & EV2); auto. + assert (Val.has_type v1 (env id)). + { eapply wt_eval_expr; eauto using wt_prog. eapply classify_stmt_wt_2; eauto. } + assert (Val.has_type v2 (env id)). + { eapply wt_eval_expr; eauto using wt_prog. eapply classify_stmt_wt_2; eauto. } + econstructor; split. + eapply step_selection; eauto using eval_expr_preserved. + unfold s0; destruct b; eapply classify_stmt_sound_2; eauto. +Qed. + +Inductive match_cont: known_idents -> typenv -> cont -> cont -> Prop := + | match_cont_seq: forall ki env s k k', + match_cont ki env k k' -> + match_cont ki env (Kseq s k) (Kseq (transf_stmt ki env s) k') + | match_cont_block: forall ki env k k', + match_cont ki env k k' -> + match_cont ki env (Kblock k) (Kblock k') + | match_cont_call: forall ki env k k', + match_call_cont k k' -> + match_cont ki env k k' + +with match_call_cont: cont -> cont -> Prop := + | match_call_cont_stop: + match_call_cont Kstop Kstop + | match_call_cont_base: forall optid f sp e k f' k' env + (WT_FN: type_function f = OK env) + (TR_FN: transf_function f = OK f') + (CONT: match_cont (known_id f) env k k'), + match_call_cont (Kcall optid f sp e k) + (Kcall optid f' sp e k'). + +Inductive match_states: state -> state -> Prop := + | match_states_gen: forall f s k sp e m f' s' env k' + (WT_FN: type_function f = OK env) + (TR_FN: transf_function f = OK f') + (TR_STMT: transf_stmt (known_id f) env s = s') + (CONT: match_cont (known_id f) env k k'), + match_states (State f s k sp e m) + (State f' s' k' sp e m) + | match_states_call: forall f args k m f' k' + (TR_FN: transf_fundef f = OK f') + (CONT: match_call_cont k k'), + match_states (Callstate f args k m) + (Callstate f' args k' m) + | match_states_return: forall v k m k' + (CONT: match_call_cont k k'), + match_states (Returnstate v k m) + (Returnstate v k' m). + +Lemma match_cont_is_call_cont: + forall ki env k k', + match_cont ki env k k' -> is_call_cont k -> is_call_cont k' /\ match_call_cont k k'. +Proof. + destruct 1; intros; try contradiction. split; auto. inv H; exact I. +Qed. + +Lemma match_cont_call_cont: + forall ki env k k', + match_cont ki env k k' -> match_call_cont (call_cont k) (call_cont k'). +Proof. + induction 1; auto. inversion H; subst; auto. +Qed. + +Definition nolabel (s: stmt) : Prop := + forall lbl k, find_label lbl s k = None. + +Lemma classify_stmt_nolabel: + forall s, classify_stmt s <> SCother -> nolabel s. +Proof. + intros s. functional induction (classify_stmt s); intros. +- red; auto. +- red; auto. +- apply IHs0 in H. red; intros; simpl. apply H. +- apply IHs0 in H. red; intros; simpl. rewrite H; auto. +- congruence. +Qed. + +Lemma if_conversion_base_nolabel: forall ki env a id a1 a2 s, + if_conversion_base ki env a id a1 a2 = Some s -> + nolabel s. +Proof. + unfold if_conversion_base; intros. + destruct (is_known ki id && safe_expr ki a1 && safe_expr ki a2); inv H. + red; auto. +Qed. + +Lemma if_conversion_nolabel: forall ki env a s1 s2 s, + if_conversion ki env a s1 s2 = Some s -> + nolabel s1 /\ nolabel s2 /\ nolabel s. +Proof. + unfold if_conversion; intros. + Ltac conclude := + split; [apply classify_stmt_nolabel;congruence + |split; [apply classify_stmt_nolabel;congruence + |eapply if_conversion_base_nolabel; eauto]]. + destruct (classify_stmt s1) eqn:C1; try discriminate; + destruct (classify_stmt s2) eqn:C2; try discriminate. + conclude. + conclude. + destruct (ident_eq id id0). conclude. discriminate. +Qed. + +Lemma transf_find_label: forall lbl ki env s k k', + match_cont ki env k k' -> + match find_label lbl s k with + | Some (s1, k1) => + exists k1', find_label lbl (transf_stmt ki env s) k' = Some (transf_stmt ki env s1, k1') + /\ match_cont ki env k1 k1' + | None => find_label lbl (transf_stmt ki env s) k' = None + end. +Proof. + induction s; intros k k' MC; simpl; auto. +- exploit (IHs1 (Kseq s2 k)). econstructor; eauto. + destruct (find_label lbl s1 (Kseq s2 k)) as [[sx kx]|]. + + intros (kx' & A & B); rewrite A. exists kx'; auto. + + intros A; rewrite A. apply IHs2; auto. +- destruct (if_conversion ki env e s1 s2) as [s|] eqn:IFC. + + apply if_conversion_nolabel in IFC. destruct IFC as (L1 & L2 & L3). + rewrite L1, L2. apply L3. + + simpl. exploit (IHs1 k); eauto. destruct (find_label lbl s1 k) as [[sx kx]|]. + * intros (kx' & A & B). rewrite A. exists kx'; auto. + * intros A; rewrite A. apply IHs2; auto. +- apply IHs. constructor; auto. +- apply IHs. constructor; auto. +- destruct (ident_eq lbl l). + + exists k'; auto. + + apply IHs; auto. +Qed. + +Lemma simulation: + forall S1 t S2, step ge S1 t S2 -> wt_state S1 -> + forall R1, match_states S1 R1 -> + exists S3 R2, star step ge S2 E0 S3 /\ step tge R1 t R2 /\ match_states S3 R2. +Proof. + assert (DFL: forall R1 t R2 S2, + step tge R1 t R2 -> match_states S2 R2 -> + exists S3 R2, star step ge S2 E0 S3 /\ step tge R1 t R2 /\ match_states S3 R2). + { intros. exists S2, R2; split. apply star_refl. auto. } + destruct 1; intros WT R1 MS; inv MS. +- (* skip Kseq *) + inv CONT; simpl. eapply DFL. + constructor. + econstructor; eauto. + inv H. +- (* skip Kblock *) + inv CONT; simpl. eapply DFL. + constructor. + econstructor; eauto. + inv H. +- (* skip return *) + exploit match_cont_is_call_cont; eauto. intros [A B]. + eapply DFL. + eapply step_skip_call; eauto. erewrite stackspace_transf_function; eauto. + econstructor; eauto. +- (* assign *) + eapply DFL. + econstructor. eapply eval_expr_preserved; eauto. + econstructor; eauto. +- (* store *) + eapply DFL. + econstructor; eauto using eval_expr_preserved. + econstructor; eauto. +- (* call *) + exploit functions_translated; eauto using eval_expr_preserved. + intros (tf & A & B). + eapply DFL. + econstructor; eauto using eval_expr_preserved, eval_exprlist_preserved. + apply sig_transf_function; auto. + econstructor; eauto. econstructor; eauto. +- (* tailcall *) + exploit functions_translated; eauto using eval_expr_preserved. + intros (tf & A & B). + eapply DFL. + econstructor; eauto using eval_expr_preserved, eval_exprlist_preserved. + apply sig_transf_function; auto. + erewrite stackspace_transf_function; eauto. + econstructor; eauto using match_cont_call_cont. +- (* builtin *) + eapply DFL. + econstructor. eapply eval_exprlist_preserved; eauto. + eapply external_call_symbols_preserved. eexact senv_preserved. eauto. + econstructor; eauto. +- (* seq *) + simpl. eapply DFL. + econstructor. + econstructor; eauto. econstructor; eauto. +- (* ifthenelse *) + simpl. destruct (if_conversion (known_id f) env a s1 s2) as [s|] eqn:IFC. + + inv WT. assert (env0 = env) by (inv WT_FN; inv WT_FN0; congruence); subst env0. + inv WT_STMT. + exploit if_conversion_sound; eauto. + set (s0 := if b then s1 else s2). + intros (e1 & A & B). + econstructor; econstructor. split. eexact B. split. eexact A. + econstructor; eauto. + + eapply DFL. + econstructor; eauto using eval_expr_preserved. + econstructor; eauto. destruct b; auto. +- (* loop *) + eapply DFL. + simpl; econstructor. + econstructor; eauto. econstructor; eauto. +- (* block *) + eapply DFL. + simpl; econstructor. + econstructor; eauto. econstructor; eauto. +- (* exit seq *) + inv CONT. eapply DFL. + econstructor; eauto. + econstructor; eauto. + inv H. +- (* exit block *) + inv CONT. eapply DFL. + econstructor; eauto. + econstructor; eauto. + inv H. +- (* exit block *) + inv CONT. eapply DFL. + econstructor; eauto. + econstructor; eauto. + inv H. +- (* switch *) + eapply DFL. + econstructor; eauto using eval_expr_preserved. + econstructor; eauto. +- (* return none *) + eapply DFL. + econstructor. erewrite stackspace_transf_function; eauto. + econstructor; eauto using match_cont_call_cont. +- (* return some *) + eapply DFL. + econstructor. eapply eval_expr_preserved; eauto. erewrite stackspace_transf_function; eauto. + econstructor; eauto using match_cont_call_cont. +- (* label *) + eapply DFL. + simpl; econstructor. + econstructor; eauto. +- (* goto *) + exploit (transf_find_label lbl (known_id f) env (fn_body f)). + apply match_cont_call. eapply match_cont_call_cont. eauto. + rewrite H. intros (k'' & A & B). + replace (transf_stmt (known_id f) env (fn_body f)) with (fn_body f') in A + by (monadInv TR_FN; simpl; congruence). + eapply DFL. + econstructor; eauto. + econstructor; eauto. +- (* internal function *) + monadInv TR_FN. generalize EQ; intros EQ'; monadInv EQ'. + eapply DFL. + econstructor; simpl; eauto. + econstructor; simpl; eauto. constructor; auto. +- (* external function *) + monadInv TR_FN. eapply DFL. + econstructor. eapply external_call_symbols_preserved. eexact senv_preserved. eauto. + econstructor; eauto. +- (* return *) + inv CONT. eapply DFL. + econstructor. + econstructor; eauto. +Qed. + +Lemma initial_states_simulation: + forall S, initial_state prog S -> exists R, initial_state tprog R /\ match_states S R. +Proof. + intros; inv H. + exploit function_ptr_translated; eauto. intros (tf & FIND & TR). + exploit sig_transf_function; eauto. intros SG. + econstructor; split. + econstructor. eapply (Genv.init_mem_transf_partial TRANSL); eauto. + rewrite symbols_preserved, (match_program_main TRANSL); eauto. + eauto. + congruence. + constructor; auto. constructor. +Qed. + +Lemma final_states_simulation: + forall S R r, + match_states S R -> final_state S r -> final_state R r. +Proof. + intros. inv H0. inv H. inv CONT. constructor. +Qed. + +Theorem transf_program_correct: + forward_simulation (semantics prog) (semantics tprog). +Proof. + set (ms := fun S R => wt_state S /\ match_states S R). + eapply forward_simulation_determ_one with (match_states := ms). +- apply Cminor.semantics_determinate. +- apply senv_preserved. +- intros. exploit initial_states_simulation; eauto. intros [R [A B]]. + exists R; split; auto. split; auto. + apply wt_initial_state with (p := prog); auto. exact wt_prog. +- intros. destruct H. eapply final_states_simulation; eauto. +- intros. destruct H0. + exploit simulation; eauto. intros (s1'' & s2' & A & B & C). + exists s1'', s2'. intuition auto. split; auto. + eapply subject_reduction_star with (st1 := s1). eexact wt_prog. + econstructor; eauto. auto. +Qed. + +End PRESERVATION. diff --git a/driver/Compiler.v b/driver/Compiler.v index 75247f71..48404b46 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -33,6 +33,7 @@ Require SimplExpr. Require SimplLocals. Require Cshmgen. Require Cminorgen. +Require Ifconv. Require Selection. Require RTLgen. Require Tailcall. @@ -54,6 +55,7 @@ Require SimplExprproof. Require SimplLocalsproof. Require Cshmgenproof. Require Cminorgenproof. +Require Ifconvproof. Require Selectionproof. Require RTLgenproof. Require Tailcallproof. @@ -149,6 +151,7 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := Definition transf_cminor_program (p: Cminor.program) : res Asm.program := OK p @@ print print_Cminor + @@@ time "If-conversion" Ifconv.transf_program @@@ time "Instruction selection" Selection.sel_program @@@ time "RTL generation" RTLgen.transl_program @@@ transf_rtl_program. @@ -233,6 +236,7 @@ Definition CompCert's_passes := ::: mkpass SimplLocalsproof.match_prog ::: mkpass Cshmgenproof.match_prog ::: mkpass Cminorgenproof.match_prog + ::: mkpass Ifconvproof.match_prog ::: mkpass Selectionproof.match_prog ::: mkpass RTLgenproof.match_prog ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog) @@ -275,7 +279,8 @@ Proof. destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; simpl in T; try discriminate. destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; simpl in T; try discriminate. unfold transf_cminor_program, time in T. rewrite ! compose_print_identity in T. simpl in T. - destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. + destruct (Ifconv.transf_program p4) as [p41|e] eqn:P41; simpl in T; try discriminate. + destruct (Selection.sel_program p41) as [p5|e] eqn:P5; simpl in T; try discriminate. destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. simpl in T. set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. @@ -297,6 +302,7 @@ Proof. exists p2; split. apply SimplLocalsproof.match_transf_program; auto. exists p3; split. apply Cshmgenproof.transf_program_match; auto. exists p4; split. apply Cminorgenproof.transf_program_match; auto. + exists p41; split. apply Ifconvproof.transf_program_match; auto. exists p5; split. apply Selectionproof.transf_program_match; auto. exists p6; split. apply RTLgenproof.transf_program_match; auto. exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match. @@ -364,7 +370,7 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p21)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p22)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -374,6 +380,8 @@ Ltac DestructM := eapply Cshmgenproof.transl_program_correct; eassumption. eapply compose_forward_simulations. eapply Cminorgenproof.transl_program_correct; eassumption. + eapply compose_forward_simulations. + eapply Ifconvproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Selectionproof.transf_program_correct; eassumption. eapply compose_forward_simulations. -- cgit