From 5c84fd4adbcd8a63cc29fb0286cb46f18abde55c Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 29 Apr 2013 17:11:47 +0000 Subject: Expand 64-bit integer comparisons into 32-bit integer comparisons. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2218 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Cminor.v | 4 +- backend/CminorSel.v | 75 +++++++++---- backend/RTLgen.v | 41 ++++--- backend/RTLgenaux.ml | 17 ++- backend/RTLgenproof.v | 160 ++++++++++++++++++++++----- backend/RTLgenspec.v | 91 +++++++++++----- backend/SelectLong.vp | 46 +++++--- backend/SelectLongproof.v | 273 ++++++++++++++++++++++++++++------------------ backend/Selection.v | 16 +-- backend/Selectionproof.v | 32 +++--- 10 files changed, 506 insertions(+), 249 deletions(-) (limited to 'backend') diff --git a/backend/Cminor.v b/backend/Cminor.v index 3963e76..6b36b4d 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -309,8 +309,8 @@ Definition eval_binop | Ocmp c => Some (Val.cmp c arg1 arg2) | Ocmpu c => Some (Val.cmpu (Mem.valid_pointer m) c arg1 arg2) | Ocmpf c => Some (Val.cmpf c arg1 arg2) - | Ocmpl c => Some (Val.cmpl c arg1 arg2) - | Ocmplu c => Some (Val.cmplu c arg1 arg2) + | Ocmpl c => Val.cmpl c arg1 arg2 + | Ocmplu c => Val.cmplu c arg1 arg2 end. (** Evaluation of an expression: [eval_expr ge sp e m a v] diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 3538dda..c80f424 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -40,7 +40,7 @@ Inductive expr : Type := | Evar : ident -> expr | Eop : operation -> exprlist -> expr | Eload : memory_chunk -> addressing -> exprlist -> expr - | Econdition : condition -> exprlist -> expr -> expr -> expr + | Econdition : condexpr -> expr -> expr -> expr | Elet : expr -> expr -> expr | Eletvar : nat -> expr | Ebuiltin : external_function -> exprlist -> expr @@ -48,7 +48,12 @@ Inductive expr : Type := with exprlist : Type := | Enil: exprlist - | Econs: expr -> exprlist -> exprlist. + | Econs: expr -> exprlist -> exprlist + +with condexpr : Type := + | CEcond : condition -> exprlist -> condexpr + | CEcondition : condexpr -> condexpr -> condexpr -> condexpr + | CElet: expr -> condexpr -> condexpr. Infix ":::" := Econs (at level 60, right associativity) : cminorsel_scope. @@ -65,7 +70,7 @@ Inductive stmt : Type := | Stailcall: signature -> expr + ident -> exprlist -> stmt | Sbuiltin : option ident -> external_function -> exprlist -> stmt | Sseq: stmt -> stmt -> stmt - | Sifthenelse: condition -> exprlist -> stmt -> stmt -> stmt + | Sifthenelse: condexpr -> stmt -> stmt -> stmt | Sloop: stmt -> stmt | Sblock: stmt -> stmt | Sexit: nat -> stmt @@ -161,11 +166,10 @@ Inductive eval_expr: letenv -> expr -> val -> Prop := eval_addressing ge sp addr vl = Some vaddr -> Mem.loadv chunk m vaddr = Some v -> eval_expr le (Eload chunk addr al) v - | eval_Econdition: forall le cond al b c vl vb v, - eval_exprlist le al vl -> - eval_condition cond vl m = Some vb -> - eval_expr le (if vb then b else c) v -> - eval_expr le (Econdition cond al b c) v + | eval_Econdition: forall le a b c va v, + eval_condexpr le a va -> + eval_expr le (if va then b else c) v -> + eval_expr le (Econdition a b c) v | eval_Elet: forall le a b v1 v2, eval_expr le a v1 -> eval_expr (v1 :: le) b v2 -> @@ -190,10 +194,25 @@ with eval_exprlist: letenv -> exprlist -> list val -> Prop := eval_exprlist le Enil nil | eval_Econs: forall le a1 al v1 vl, eval_expr le a1 v1 -> eval_exprlist le al vl -> - eval_exprlist le (Econs a1 al) (v1 :: vl). + eval_exprlist le (Econs a1 al) (v1 :: vl) + +with eval_condexpr: letenv -> condexpr -> bool -> Prop := + | eval_CEcond: forall le cond al vl vb, + eval_exprlist le al vl -> + eval_condition cond vl m = Some vb -> + eval_condexpr le (CEcond cond al) vb + | eval_CEcondition: forall le a b c va v, + eval_condexpr le a va -> + eval_condexpr le (if va then b else c) v -> + eval_condexpr le (CEcondition a b c) v + | eval_CElet: forall le a b v1 v2, + eval_expr le a v1 -> + eval_condexpr (v1 :: le) b v2 -> + eval_condexpr le (CElet a b) v2. -Scheme eval_expr_ind2 := Minimality for eval_expr Sort Prop - with eval_exprlist_ind2 := Minimality for eval_exprlist Sort Prop. +Scheme eval_expr_ind3 := Minimality for eval_expr Sort Prop + with eval_exprlist_ind3 := Minimality for eval_exprlist Sort Prop + with eval_condexpr_ind3 := Minimality for eval_condexpr Sort Prop. Inductive eval_expr_or_symbol: letenv -> expr + ident -> val -> Prop := | eval_eos_e: forall le e v, @@ -232,7 +251,7 @@ Fixpoint find_label (lbl: label) (s: stmt) (k: cont) | Some sk => Some sk | None => find_label lbl s2 k end - | Sifthenelse cond al s1 s2 => + | Sifthenelse c s1 s2 => match find_label lbl s1 k with | Some sk => Some sk | None => find_label lbl s2 k @@ -302,10 +321,9 @@ Inductive step: state -> trace -> state -> Prop := step (State f (Sseq s1 s2) k sp e m) E0 (State f s1 (Kseq s2 k) sp e m) - | step_ifthenelse: forall f cond al s1 s2 k sp e m vl b, - eval_exprlist sp e m nil al vl -> - eval_condition cond vl m = Some b -> - step (State f (Sifthenelse cond al s1 s2) k sp e m) + | step_ifthenelse: forall f c s1 s2 k sp e m b, + eval_condexpr sp e m nil c b -> + step (State f (Sifthenelse c s1 s2) k sp e m) E0 (State f (if b then s1 else s2) k sp e m) | step_loop: forall f s k sp e m, @@ -382,7 +400,7 @@ Inductive final_state: state -> int -> Prop := Definition semantics (p: program) := Semantics step (initial_state p) final_state (Genv.globalenv p). -Hint Constructors eval_expr eval_exprlist: evalexpr. +Hint Constructors eval_expr eval_exprlist eval_condexpr: evalexpr. (** * Lifting of let-bound variables *) @@ -396,8 +414,8 @@ Fixpoint lift_expr (p: nat) (a: expr) {struct a}: expr := | Evar id => Evar id | Eop op bl => Eop op (lift_exprlist p bl) | Eload chunk addr bl => Eload chunk addr (lift_exprlist p bl) - | Econdition cond al b c => - Econdition cond (lift_exprlist p al) (lift_expr p b) (lift_expr p c) + | Econdition a b c => + Econdition (lift_condexpr p a) (lift_expr p b) (lift_expr p c) | Elet b c => Elet (lift_expr p b) (lift_expr (S p) c) | Eletvar n => if le_gt_dec p n then Eletvar (S n) else Eletvar n @@ -409,6 +427,13 @@ with lift_exprlist (p: nat) (a: exprlist) {struct a}: exprlist := match a with | Enil => Enil | Econs b cl => Econs (lift_expr p b) (lift_exprlist p cl) + end + +with lift_condexpr (p: nat) (a: condexpr) {struct a}: condexpr := + match a with + | CEcond c al => CEcond c (lift_exprlist p al) + | CEcondition a b c => CEcondition (lift_condexpr p a) (lift_condexpr p b) (lift_condexpr p c) + | CElet a b => CElet (lift_expr p a) (lift_condexpr (S p) b) end. Definition lift (a: expr): expr := lift_expr O a. @@ -458,22 +483,28 @@ Lemma eval_lift_expr: eval_expr ge sp e m le' (lift_expr p a) v. Proof. intros until w. - apply (eval_expr_ind2 ge sp e m + apply (eval_expr_ind3 ge sp e m (fun le a v => forall p le', insert_lenv le p w le' -> eval_expr ge sp e m le' (lift_expr p a) v) (fun le al vl => forall p le', insert_lenv le p w le' -> - eval_exprlist ge sp e m le' (lift_exprlist p al) vl)); + eval_exprlist ge sp e m le' (lift_exprlist p al) vl) + (fun le a b => + forall p le', insert_lenv le p w le' -> + eval_condexpr ge sp e m le' (lift_condexpr p a) b)); simpl; intros; eauto with evalexpr. - eapply eval_Econdition; eauto. destruct vb; eauto. + eapply eval_Econdition; eauto. destruct va; eauto. eapply eval_Elet. eauto. apply H2. apply insert_lenv_S; auto. case (le_gt_dec p n); intro. apply eval_Eletvar. eapply insert_lenv_lookup2; eauto. apply eval_Eletvar. eapply insert_lenv_lookup1; eauto. + + eapply eval_CEcondition; eauto. destruct va; eauto. + eapply eval_CElet; eauto. apply H2. constructor; auto. Qed. Lemma eval_lift: diff --git a/backend/RTLgen.v b/backend/RTLgen.v index f5e34e4..193702e 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -401,12 +401,10 @@ Fixpoint transl_expr (map: mapping) (a: expr) (rd: reg) (nd: node) do rl <- alloc_regs map al; do no <- add_instr (Iload chunk addr rl rd nd); transl_exprlist map al rl no - | Econdition cond al b c => - do rl <- alloc_regs map al; + | Econdition a b c => do nfalse <- transl_expr map c rd nd; do ntrue <- transl_expr map b rd nd; - do nt <- add_instr (Icond cond rl ntrue nfalse); - transl_exprlist map al rl nt + transl_condexpr map a ntrue nfalse | Elet b c => do r <- new_reg; do nc <- transl_expr (add_letvar map r) c rd nd; @@ -435,6 +433,26 @@ with transl_exprlist (map: mapping) (al: exprlist) (rl: list reg) (nd: node) do no <- transl_exprlist map bs rs nd; transl_expr map b r no | _, _ => error (Errors.msg "RTLgen.transl_exprlist") + end + +(** Translation of a conditional expression. Branches to [ntrue] or + to [nfalse] depending on the truth value of the expression. *) + +with transl_condexpr (map: mapping) (a: condexpr) (ntrue nfalse: node) + {struct a} : mon node := + match a with + | CEcond c al => + do rl <- alloc_regs map al; + do nt <- add_instr (Icond c rl ntrue nfalse); + transl_exprlist map al rl nt + | CEcondition a b c => + do nc <- transl_condexpr map c ntrue nfalse; + do nb <- transl_condexpr map b ntrue nfalse; + transl_condexpr map a nb nc + | CElet b c => + do r <- new_reg; + do nc <- transl_condexpr (add_letvar map r) c ntrue nfalse; + transl_expr map b r nc end. (** Auxiliary for branch prediction. When compiling an if/then/else @@ -445,7 +463,7 @@ with transl_exprlist (map: mapping) (al: exprlist) (rl: list reg) (nd: node) no impact on program correctness. We delegate the choice to an external heuristic (written in OCaml), declared below. *) -Parameter more_likely: condition -> stmt -> stmt -> bool. +Parameter more_likely: condexpr -> stmt -> stmt -> bool. (** Auxiliary for translating [Sswitch] statements. *) @@ -545,18 +563,15 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) | Sseq s1 s2 => do ns <- transl_stmt map s2 nd nexits ngoto nret rret; transl_stmt map s1 ns nexits ngoto nret rret - | Sifthenelse cond al strue sfalse => - do rl <- alloc_regs map al; - if more_likely cond strue sfalse then + | Sifthenelse c strue sfalse => + if more_likely c strue sfalse then do nfalse <- transl_stmt map sfalse nd nexits ngoto nret rret; do ntrue <- transl_stmt map strue nd nexits ngoto nret rret; - do nt <- add_instr (Icond cond rl ntrue nfalse); - transl_exprlist map al rl nt + transl_condexpr map c ntrue nfalse else do ntrue <- transl_stmt map strue nd nexits ngoto nret rret; do nfalse <- transl_stmt map sfalse nd nexits ngoto nret rret; - do nt <- add_instr (Icond cond rl ntrue nfalse); - transl_exprlist map al rl nt + transl_condexpr map c ntrue nfalse | Sloop sbody => do n1 <- reserve_instr; do n2 <- transl_stmt map sbody n1 nexits ngoto nret rret; @@ -611,7 +626,7 @@ Fixpoint reserve_labels (s: stmt) (ms: labelmap * state) {struct s} : labelmap * state := match s with | Sseq s1 s2 => reserve_labels s1 (reserve_labels s2 ms) - | Sifthenelse cond al s1 s2 => reserve_labels s1 (reserve_labels s2 ms) + | Sifthenelse c s1 s2 => reserve_labels s1 (reserve_labels s2 ms) | Sloop s1 => reserve_labels s1 ms | Sblock s1 => reserve_labels s1 ms | Slabel lbl s1 => alloc_label lbl (reserve_labels s1 ms) diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml index 150de5a..7590102 100644 --- a/backend/RTLgenaux.ml +++ b/backend/RTLgenaux.ml @@ -30,8 +30,8 @@ let rec size_expr = function | Evar id -> 0 | Eop(op, args) -> 1 + size_exprs args | Eload(chunk, addr, args) -> 1 + size_exprs args - | Econdition(cond, args, e1, e2) -> - 1 + size_exprs args + max (size_expr e1) (size_expr e2) + | Econdition(ce, e1, e2) -> + 1 + size_condexpr ce + max (size_expr e1) (size_expr e2) | Elet(e1, e2) -> size_expr e1 + size_expr e2 | Eletvar n -> 0 | Ebuiltin(ef, el) -> 2 + size_exprs el @@ -41,6 +41,13 @@ and size_exprs = function | Enil -> 0 | Econs(e1, el) -> size_expr e1 + size_exprs el +and size_condexpr = function + | CEcond(c, args) -> size_exprs args + | CEcondition(c1, c2, c3) -> + 1 + size_condexpr c1 + size_condexpr c2 + size_condexpr c3 + | CElet(a, c) -> + size_expr a + size_condexpr c + let rec length_exprs = function | Enil -> 0 | Econs(e1, el) -> 1 + length_exprs el @@ -59,8 +66,8 @@ let rec size_stmt = function 3 + size_eos eos + size_exprs args + length_exprs args | Sbuiltin(optid, ef, args) -> 1 + size_exprs args | Sseq(s1, s2) -> size_stmt s1 + size_stmt s2 - | Sifthenelse(cond, args, s1, s2) -> - 1 + size_exprs args + max (size_stmt s1) (size_stmt s2) + | Sifthenelse(ce, s1, s2) -> + size_condexpr ce + max (size_stmt s1) (size_stmt s2) | Sloop s -> 1 + 4 * size_stmt s | Sblock s -> size_stmt s | Sexit n -> 1 @@ -70,7 +77,7 @@ let rec size_stmt = function | Slabel(lbl, s) -> size_stmt s | Sgoto lbl -> 1 -let more_likely (c: Op.condition) (ifso: stmt) (ifnot: stmt) = +let more_likely (c: condexpr) (ifso: stmt) (ifnot: stmt) = size_stmt ifso > size_stmt ifnot (* Compiling a switch table into a decision tree *) diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index c3cae28..51f1f27 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -546,6 +546,19 @@ Definition transl_exprlist_prop /\ (forall r, In r pr -> rs'#r = rs#r) /\ Mem.extends m tm'. +Definition transl_condexpr_prop + (le: letenv) (a: condexpr) (v: bool) : Prop := + forall tm cs f map pr ns ntrue nfalse rs + (MWF: map_wf map) + (TE: tr_condition f.(fn_code) map pr a ns ntrue nfalse) + (ME: match_env map e le rs) + (EXT: Mem.extends m tm), + exists rs', exists tm', + plus step tge (State cs f sp ns rs tm) E0 (State cs f sp (if v then ntrue else nfalse) rs' tm') + /\ match_env map e le rs' + /\ (forall r, In r pr -> rs'#r = rs#r) + /\ Mem.extends m tm'. + (** The correctness of the translation is a huge induction over the Cminor evaluation derivation for the source program. To keep the proof manageable, we put each case of the proof in a separate @@ -639,25 +652,22 @@ Proof. Qed. Lemma transl_expr_Econdition_correct: - forall (le : letenv) (cond : condition) (al: exprlist) (ifso ifnot : expr) - (vl: list val) (vcond : bool) (v : val), - eval_exprlist ge sp e m le al vl -> - transl_exprlist_prop le al vl -> - eval_condition cond vl m = Some vcond -> - eval_expr ge sp e m le (if vcond then ifso else ifnot) v -> - transl_expr_prop le (if vcond then ifso else ifnot) v -> - transl_expr_prop le (Econdition cond al ifso ifnot) v. + forall (le : letenv) (a: condexpr) (ifso ifnot : expr) + (va : bool) (v : val), + eval_condexpr ge sp e m le a va -> + transl_condexpr_prop le a va -> + eval_expr ge sp e m le (if va then ifso else ifnot) v -> + transl_expr_prop le (if va then ifso else ifnot) v -> + transl_expr_prop le (Econdition a ifso ifnot) v. Proof. - intros; red; intros; inv TE. inv H14. - exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [RES1 [OTHER1 EXT1]]]]]]. - assert (tr_expr f.(fn_code) map pr (if vcond then ifso else ifnot) (if vcond then ntrue else nfalse) nd rd dst). - destruct vcond; auto. - exploit H3; eauto. intros [rs2 [tm2 [EX2 [ME2 [RES2 [OTHER2 EXT2]]]]]]. + intros; red; intros; inv TE. + exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [OTHER1 EXT1]]]]]. + assert (tr_expr f.(fn_code) map pr (if va then ifso else ifnot) (if va then ntrue else nfalse) nd rd dst). + destruct va; auto. + exploit H2; eauto. intros [rs2 [tm2 [EX2 [ME2 [RES2 [OTHER2 EXT2]]]]]]. exists rs2; exists tm2. (* Exec *) - split. eapply star_trans. eexact EX1. - eapply star_left. eapply exec_Icond. eauto. eapply eval_condition_lessdef; eauto. reflexivity. - eexact EX2. reflexivity. traceEq. + split. eapply star_trans. apply plus_star. eexact EX1. eexact EX2. traceEq. (* Match-env *) split. assumption. (* Result value *) @@ -829,14 +839,85 @@ Proof. auto. Qed. +Lemma transl_condexpr_CEcond_correct: + forall le cond al vl vb, + eval_exprlist ge sp e m le al vl -> + transl_exprlist_prop le al vl -> + eval_condition cond vl m = Some vb -> + transl_condexpr_prop le (CEcond cond al) vb. +Proof. + intros; red; intros. inv TE. + exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [RES1 [OTHER1 EXT1]]]]]]. + exists rs1; exists tm1. +(* Exec *) + split. eapply plus_right. eexact EX1. eapply exec_Icond. eauto. + eapply eval_condition_lessdef; eauto. auto. traceEq. +(* Match-env *) + split. assumption. +(* Other regs *) + split. assumption. +(* Mem *) + auto. +Qed. + +Lemma transl_condexpr_CEcondition_correct: + forall le a b c va v, + eval_condexpr ge sp e m le a va -> + transl_condexpr_prop le a va -> + eval_condexpr ge sp e m le (if va then b else c) v -> + transl_condexpr_prop le (if va then b else c) v -> + transl_condexpr_prop le (CEcondition a b c) v. +Proof. + intros; red; intros. inv TE. + exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [OTHER1 EXT1]]]]]. + assert (tr_condition (fn_code f) map pr (if va then b else c) (if va then n2 else n3) ntrue nfalse). + destruct va; auto. + exploit H2; eauto. intros [rs2 [tm2 [EX2 [ME2 [OTHER2 EXT2]]]]]. + exists rs2; exists tm2. +(* Exec *) + split. eapply plus_trans. eexact EX1. eexact EX2. traceEq. +(* Match-env *) + split. assumption. +(* Other regs *) + split. intros. rewrite OTHER2; auto. +(* Mem *) + auto. +Qed. + +Lemma transl_condexpr_CElet_correct: + forall le a b v1 v2, + eval_expr ge sp e m le a v1 -> + transl_expr_prop le a v1 -> + eval_condexpr ge sp e m (v1 :: le) b v2 -> + transl_condexpr_prop (v1 :: le) b v2 -> + transl_condexpr_prop le (CElet a b) v2. +Proof. + intros; red; intros. inv TE. + exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [RES1 [OTHER1 EXT1]]]]]]. + assert (map_wf (add_letvar map r)). + eapply add_letvar_wf; eauto. + exploit H2; eauto. eapply match_env_bind_letvar; eauto. + intros [rs2 [tm2 [EX2 [ME3 [OTHER2 EXT2]]]]]. + exists rs2; exists tm2. +(* Exec *) + split. eapply star_plus_trans. eexact EX1. eexact EX2. traceEq. +(* Match-env *) + split. eapply match_env_unbind_letvar; eauto. +(* Other regs *) + split. intros. rewrite OTHER2; auto. +(* Mem *) + auto. +Qed. + Theorem transl_expr_correct: forall le a v, eval_expr ge sp e m le a v -> transl_expr_prop le a v. Proof - (eval_expr_ind2 ge sp e m + (eval_expr_ind3 ge sp e m transl_expr_prop transl_exprlist_prop + transl_condexpr_prop transl_expr_Evar_correct transl_expr_Eop_correct transl_expr_Eload_correct @@ -846,16 +927,20 @@ Proof transl_expr_Ebuiltin_correct transl_expr_Eexternal_correct transl_exprlist_Enil_correct - transl_exprlist_Econs_correct). + transl_exprlist_Econs_correct + transl_condexpr_CEcond_correct + transl_condexpr_CEcondition_correct + transl_condexpr_CElet_correct). Theorem transl_exprlist_correct: forall le a v, eval_exprlist ge sp e m le a v -> transl_exprlist_prop le a v. Proof - (eval_exprlist_ind2 ge sp e m + (eval_exprlist_ind3 ge sp e m transl_expr_prop transl_exprlist_prop + transl_condexpr_prop transl_expr_Evar_correct transl_expr_Eop_correct transl_expr_Eload_correct @@ -865,7 +950,33 @@ Proof transl_expr_Ebuiltin_correct transl_expr_Eexternal_correct transl_exprlist_Enil_correct - transl_exprlist_Econs_correct). + transl_exprlist_Econs_correct + transl_condexpr_CEcond_correct + transl_condexpr_CEcondition_correct + transl_condexpr_CElet_correct). + +Theorem transl_condexpr_correct: + forall le a v, + eval_condexpr ge sp e m le a v -> + transl_condexpr_prop le a v. +Proof + (eval_condexpr_ind3 ge sp e m + transl_expr_prop + transl_exprlist_prop + transl_condexpr_prop + transl_expr_Evar_correct + transl_expr_Eop_correct + transl_expr_Eload_correct + transl_expr_Econdition_correct + transl_expr_Elet_correct + transl_expr_Eletvar_correct + transl_expr_Ebuiltin_correct + transl_expr_Eexternal_correct + transl_exprlist_Enil_correct + transl_exprlist_Econs_correct + transl_condexpr_CEcond_correct + transl_condexpr_CEcondition_correct + transl_condexpr_CElet_correct). End CORRECTNESS_EXPR. @@ -877,7 +988,7 @@ Fixpoint size_stmt (s: stmt) : nat := match s with | Sskip => 0 | Sseq s1 s2 => (size_stmt s1 + size_stmt s2 + 1) - | Sifthenelse cond el s1 s2 => (size_stmt s1 + size_stmt s2 + 1) + | Sifthenelse c s1 s2 => (size_stmt s1 + size_stmt s2 + 1) | Sloop s1 => (size_stmt s1 + 1) | Sblock s1 => (size_stmt s1 + 1) | Sexit n => 0 @@ -1206,11 +1317,10 @@ Proof. econstructor; eauto. econstructor; eauto. (* ifthenelse *) - inv TS. inv H13. - exploit transl_exprlist_correct; eauto. intros [rs' [tm' [A [B [C [D E]]]]]]. + inv TS. + exploit transl_condexpr_correct; eauto. intros [rs' [tm' [A [B [C D]]]]]. econstructor; split. - left. eapply plus_right. eexact A. eapply exec_Icond; eauto. - eapply eval_condition_lessdef; eauto. traceEq. + left. eexact A. destruct b; econstructor; eauto. (* loop *) diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index d8d5dc8..c82c051 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -703,11 +703,11 @@ Inductive tr_expr (c: code): c!n1 = Some (Iload chunk addr rl rd nd) -> reg_map_ok map rd dst -> ~In rd pr -> tr_expr c map pr (Eload chunk addr al) ns nd rd dst - | tr_Econdition: forall map pr cond bl ifso ifnot ns nd rd ntrue nfalse dst, - tr_condition c map pr cond bl ns ntrue nfalse -> + | tr_Econdition: forall map pr a ifso ifnot ns nd rd ntrue nfalse dst, + tr_condition c map pr a ns ntrue nfalse -> tr_expr c map pr ifso ntrue nd rd dst -> tr_expr c map pr ifnot nfalse nd rd dst -> - tr_expr c map pr (Econdition cond bl ifso ifnot) ns nd rd dst + tr_expr c map pr (Econdition a ifso ifnot) ns nd rd dst | tr_Elet: forall map pr b1 b2 ns nd rd n1 r dst, ~reg_in_map map r -> tr_expr c map pr b1 ns n1 r None -> @@ -730,17 +730,27 @@ Inductive tr_expr (c: code): tr_expr c map pr (Eexternal id sg al) ns nd rd dst -(** [tr_condition c map pr cond al ns ntrue nfalse rd] holds if the graph [c], +(** [tr_condition c map pr a ns ntrue nfalse rd] holds if the graph [c], starting at node [ns], contains instructions that compute the truth - value of the Cminor conditional expression [cond] and terminate + value of the Cminor conditional expression [a] and terminate on node [ntrue] if the condition holds and on node [nfalse] otherwise. *) with tr_condition (c: code): - mapping -> list reg -> condition -> exprlist -> node -> node -> node -> Prop := + mapping -> list reg -> condexpr -> node -> node -> node -> Prop := | tr_CEcond: forall map pr cond bl ns ntrue nfalse n1 rl, tr_exprlist c map pr bl ns n1 rl -> c!n1 = Some (Icond cond rl ntrue nfalse) -> - tr_condition c map pr cond bl ns ntrue nfalse + tr_condition c map pr (CEcond cond bl) ns ntrue nfalse + | tr_CEcondition: forall map pr a1 a2 a3 ns ntrue nfalse n2 n3, + tr_condition c map pr a1 ns n2 n3 -> + tr_condition c map pr a2 n2 ntrue nfalse -> + tr_condition c map pr a3 n3 ntrue nfalse -> + tr_condition c map pr (CEcondition a1 a2 a3) ns ntrue nfalse + | tr_CElet: forall map pr a b ns ntrue nfalse r n1, + ~reg_in_map map r -> + tr_expr c map pr a ns n1 r None -> + tr_condition c (add_letvar map r) pr b n1 ntrue nfalse -> + tr_condition c map pr (CElet a b) ns ntrue nfalse (** [tr_exprlist c map pr exprs ns nd rds] holds if the graph [c], between nodes [ns] and [nd], contains instructions that compute the values @@ -840,11 +850,11 @@ Inductive tr_stmt (c: code) (map: mapping): tr_stmt c map s2 n nd nexits ngoto nret rret -> tr_stmt c map s1 ns n nexits ngoto nret rret -> tr_stmt c map (Sseq s1 s2) ns nd nexits ngoto nret rret - | tr_Sifthenelse: forall cond al strue sfalse ns nd nexits ngoto nret rret ntrue nfalse, + | tr_Sifthenelse: forall a strue sfalse ns nd nexits ngoto nret rret ntrue nfalse, tr_stmt c map strue ntrue nd nexits ngoto nret rret -> tr_stmt c map sfalse nfalse nd nexits ngoto nret rret -> - tr_condition c map nil cond al ns ntrue nfalse -> - tr_stmt c map (Sifthenelse cond al strue sfalse) ns nd nexits ngoto nret rret + tr_condition c map nil a ns ntrue nfalse -> + tr_stmt c map (Sifthenelse a strue sfalse) ns nd nexits ngoto nret rret | tr_Sloop: forall sbody ns nd nexits ngoto nret rret nloop nend, tr_stmt c map sbody nloop nend nexits ngoto nret rret -> c!ns = Some(Inop nloop) -> @@ -914,9 +924,9 @@ Lemma tr_expr_incr: tr_expr s2.(st_code) map pr a ns nd rd dst with tr_condition_incr: forall s1 s2, state_incr s1 s2 -> - forall map pr cond al ns ntrue nfalse, - tr_condition s1.(st_code) map pr cond al ns ntrue nfalse -> - tr_condition s2.(st_code) map pr cond al ns ntrue nfalse + forall map pr a ns ntrue nfalse, + tr_condition s1.(st_code) map pr a ns ntrue nfalse -> + tr_condition s2.(st_code) map pr a ns ntrue nfalse with tr_exprlist_incr: forall s1 s2, state_incr s1 s2 -> forall map pr al ns nd rl, @@ -962,7 +972,14 @@ with transl_exprlist_charact: (OK: target_regs_ok map pr al rl) (VALID1: regs_valid pr s) (VALID2: regs_valid rl s), - tr_exprlist s'.(st_code) map pr al ns nd rl. + tr_exprlist s'.(st_code) map pr al ns nd rl + +with transl_condexpr_charact: + forall a map ntrue nfalse s ns s' pr INCR + (TR: transl_condexpr map a ntrue nfalse s = OK ns s' INCR) + (WF: map_valid map s) + (VALID: regs_valid pr s), + tr_condition s'.(st_code) map pr a ns ntrue nfalse. Proof. induction a; intros; try (monadInv TR); saturateTrans. @@ -981,12 +998,12 @@ Proof. eapply transl_exprlist_charact; eauto with rtlg. (* Econdition *) inv OK. - econstructor; eauto with rtlg. - econstructor; eauto with rtlg. eapply transl_exprlist_charact; eauto with rtlg. - apply tr_expr_incr with s2; auto. - eapply transl_expr_charact; eauto 2 with rtlg. constructor; auto. + econstructor. + eauto with rtlg. apply tr_expr_incr with s1; auto. eapply transl_expr_charact; eauto 2 with rtlg. constructor; auto. + apply tr_expr_incr with s0; auto. + eapply transl_expr_charact; eauto 2 with rtlg. constructor; auto. (* Elet *) inv OK. econstructor. eapply new_reg_not_in_map; eauto with rtlg. @@ -1031,6 +1048,22 @@ Proof. eapply transl_exprlist_charact; eauto with rtlg. apply regs_valid_cons. apply VALID2. auto with coqlib. auto. red; intros; apply VALID2; auto with coqlib. + +(* Conditional expressions *) + induction a; intros; try (monadInv TR); saturateTrans. + + (* CEcond *) + econstructor; eauto with rtlg. eapply transl_exprlist_charact; eauto with rtlg. + (* CEcondition *) + econstructor; eauto with rtlg. + apply tr_condition_incr with s1; eauto with rtlg. + apply tr_condition_incr with s0; eauto with rtlg. + (* CElet *) + econstructor; eauto with rtlg. + eapply transl_expr_charact; eauto with rtlg. + apply tr_condition_incr with s1; eauto with rtlg. + eapply transl_condexpr_charact; eauto with rtlg. + apply add_letvar_valid; eauto with rtlg. Qed. (** A variant of [transl_expr_charact], for use when the destination @@ -1056,10 +1089,10 @@ Proof. eapply transl_exprlist_charact; eauto with rtlg. (* Econdition *) econstructor; eauto with rtlg. - econstructor; eauto with rtlg. eapply transl_exprlist_charact; eauto with rtlg. - apply tr_expr_incr with s2; auto. - eapply IHa1; eauto 2 with rtlg. + eapply transl_condexpr_charact; eauto with rtlg. apply tr_expr_incr with s1; auto. + eapply IHa1; eauto 2 with rtlg. + apply tr_expr_incr with s0; auto. eapply IHa2; eauto 2 with rtlg. (* Elet *) econstructor. eapply new_reg_not_in_map; eauto with rtlg. @@ -1227,21 +1260,19 @@ Proof. eapply IHstmt2; eauto with rtlg. eapply IHstmt1; eauto with rtlg. (* Sifthenelse *) - destruct (more_likely c stmt1 stmt2); monadInv EQ0. + destruct (more_likely c stmt1 stmt2); monadInv TR. econstructor. - apply tr_stmt_incr with s2; auto. + apply tr_stmt_incr with s1; auto. eapply IHstmt1; eauto with rtlg. - apply tr_stmt_incr with s1; auto. + apply tr_stmt_incr with s0; auto. eapply IHstmt2; eauto with rtlg. - econstructor; eauto with rtlg. - eapply transl_exprlist_charact; eauto with rtlg. + eapply transl_condexpr_charact; eauto with rtlg. econstructor. - apply tr_stmt_incr with s1; auto. + apply tr_stmt_incr with s0; auto. eapply IHstmt1; eauto with rtlg. - apply tr_stmt_incr with s2; auto. + apply tr_stmt_incr with s1; auto. eapply IHstmt2; eauto with rtlg. - econstructor; eauto with rtlg. - eapply transl_exprlist_charact; eauto with rtlg. + eapply transl_condexpr_charact; eauto with rtlg. (* Sloop *) econstructor. apply tr_stmt_incr with s1; auto. diff --git a/backend/SelectLong.vp b/backend/SelectLong.vp index 8eb32c3..aad9d60 100644 --- a/backend/SelectLong.vp +++ b/backend/SelectLong.vp @@ -41,9 +41,7 @@ Record helper_functions : Type := mk_helper_functions { i64_umod: ident; (**r unsigned remainder *) i64_shl: ident; (**r shift left *) i64_shr: ident; (**r shift right unsigned *) - i64_sar: ident; (**r shift right signed *) - i64_scmp: ident; (**r signed comparison *) - i64_ucmp: ident (**r unsigned comparison *) + i64_sar: ident (**r shift right signed *) }. Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong). @@ -51,7 +49,6 @@ Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat). Definition sig_f_l := mksignature (Tfloat :: nil) (Some Tlong). Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) (Some Tlong). Definition sig_li_l := mksignature (Tlong :: Tint :: nil) (Some Tlong). -Definition sig_ll_i := mksignature (Tlong :: Tlong :: nil) (Some Tint). Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong). Section SELECT. @@ -291,6 +288,12 @@ Definition cmpl_eq_zero (e: expr) := Definition cmpl_ne_zero (e: expr) := splitlong e (fun h l => comp Cne (or h l) (Eop (Ointconst Int.zero) Enil)). +Definition cmplu_gen (ch cl: comparison) (e1 e2: expr) := + splitlong2 e1 e2 (fun h1 l1 h2 l2 => + Econdition (CEcond (Ccomp Ceq) (h1:::h2:::Enil)) + (Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil)) + (Eop (Ocmp (Ccompu ch)) (h1:::h2:::Enil))). + Definition cmplu (c: comparison) (e1 e2: expr) := match c with | Ceq => @@ -301,15 +304,23 @@ Definition cmplu (c: comparison) (e1 e2: expr) := if is_longconst_zero e2 then cmpl_ne_zero e1 else cmpl_ne_zero (xorl e1 e2) - | _ => - comp c (Eexternal hf.(i64_ucmp) sig_ll_i (e1 ::: e2 ::: Enil)) - (Eop (Ointconst Int.zero) Enil) + | Clt => + cmplu_gen Clt Clt e1 e2 + | Cle => + cmplu_gen Clt Cle e1 e2 + | Cgt => + cmplu_gen Cgt Cgt e1 e2 + | Cge => + cmplu_gen Cgt Cge e1 e2 end. +Definition cmpl_gen (ch cl: comparison) (e1 e2: expr) := + splitlong2 e1 e2 (fun h1 l1 h2 l2 => + Econdition (CEcond (Ccomp Ceq) (h1:::h2:::Enil)) + (Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil)) + (Eop (Ocmp (Ccomp ch)) (h1:::h2:::Enil))). + Definition cmpl (c: comparison) (e1 e2: expr) := - let default := - comp c (Eexternal hf.(i64_scmp) sig_ll_i (e1 ::: e2 ::: Enil)) - (Eop (Ointconst Int.zero) Enil) in match c with | Ceq => if is_longconst_zero e2 @@ -322,13 +333,15 @@ Definition cmpl (c: comparison) (e1 e2: expr) := | Clt => if is_longconst_zero e2 then comp Clt (highlong e1) (Eop (Ointconst Int.zero) Enil) - else default + else cmpl_gen Clt Clt e1 e2 + | Cle => + cmpl_gen Clt Cle e1 e2 + | Cgt => + cmpl_gen Cgt Cgt e1 e2 | Cge => if is_longconst_zero e2 then comp Cge (highlong e1) (Eop (Ointconst Int.zero) Enil) - else default - | _ => - default + else cmpl_gen Cgt Cge e1 e2 end. End SELECT. @@ -359,10 +372,7 @@ Definition get_helpers (ge: Cminor.genv): res helper_functions := do i64_shl <- get_helper ge "__i64_shl" sig_li_l ; do i64_shr <- get_helper ge "__i64_shr" sig_li_l ; do i64_sar <- get_helper ge "__i64_sar" sig_li_l ; - do i64_scmp <- get_helper ge "__i64_scmp" sig_ll_i ; - do i64_ucmp <- get_helper ge "__i64_ucmp" sig_ll_i ; OK (mk_helper_functions i64_dtos i64_dtou i64_stod i64_utod i64_neg i64_add i64_sub i64_mul i64_sdiv i64_udiv i64_smod i64_umod - i64_shl i64_shr i64_sar - i64_scmp i64_ucmp). + i64_shl i64_shr i64_sar). diff --git a/backend/SelectLongproof.v b/backend/SelectLongproof.v index aca05bf..3eeeeb5 100644 --- a/backend/SelectLongproof.v +++ b/backend/SelectLongproof.v @@ -61,11 +61,7 @@ Definition i64_helpers_correct (hf: helper_functions) : Prop := /\(forall x y z, Val.modlu x y = Some z -> helper_implements hf.(i64_umod) sig_ll_l (x::y::nil) z) /\(forall x y, helper_implements hf.(i64_shl) sig_li_l (x::y::nil) (Val.shll x y)) /\(forall x y, helper_implements hf.(i64_shr) sig_li_l (x::y::nil) (Val.shrlu x y)) - /\(forall x y, helper_implements hf.(i64_sar) sig_li_l (x::y::nil) (Val.shrl x y)) - /\(forall c x y, exists z, helper_implements hf.(i64_scmp) sig_ll_i (x::y::nil) z - /\ Val.cmpl c x y = Val.cmp c z Vzero) - /\(forall c x y, exists z, helper_implements hf.(i64_ucmp) sig_ll_i (x::y::nil) z - /\ Val.cmplu c x y = Val.cmp c z Vzero). + /\(forall x y, helper_implements hf.(i64_sar) sig_li_l (x::y::nil) (Val.shrl x y)). End HELPERS. @@ -180,6 +176,22 @@ Proof. destruct v; try (rewrite UNDEF; auto). erewrite B; simpl; eauto. rewrite Int64.ofwords_recompose. auto. Qed. +Lemma eval_splitlong_strict: + forall le a f va v, + eval_expr ge sp e m le a (Vlong va) -> + (forall le a1 a2, + eval_expr ge sp e m le a1 (Vint (Int64.hiword va)) -> + eval_expr ge sp e m le a2 (Vint (Int64.loword va)) -> + eval_expr ge sp e m le (f a1 a2) v) -> + eval_expr ge sp e m le (splitlong a f) v. +Proof. + intros until v. + unfold splitlong. case (splitlong_match a); intros. +- InvEval. destruct v1; simpl in H; try discriminate. destruct v0; inv H. + apply H0. rewrite Int64.hi_ofwords; auto. rewrite Int64.lo_ofwords; auto. +- EvalOp. apply H0; EvalOp. +Qed. + Lemma eval_splitlong2: forall le a b f va vb sem, (forall le a1 a2 b1 b2 x1 x2 y1 y2, @@ -198,7 +210,7 @@ Lemma eval_splitlong2: exists v, eval_expr ge sp e m le (splitlong2 a b f) v /\ Val.lessdef (sem va vb) v. Proof. intros until sem; intros EXEC UNDEF. - unfold splitlong2. case (splitlong2_match a); intros. + unfold splitlong2. case (splitlong2_match a b); intros. - InvEval. subst va vb. exploit (EXEC le h1 l1 h2 l2); eauto. intros [v [A B]]. exists v; split; auto. @@ -240,6 +252,35 @@ Proof. erewrite B; simpl; eauto. rewrite ! Int64.ofwords_recompose; auto. Qed. +Lemma eval_splitlong2_strict: + forall le a b f va vb v, + eval_expr ge sp e m le a (Vlong va) -> + eval_expr ge sp e m le b (Vlong vb) -> + (forall le a1 a2 b1 b2, + eval_expr ge sp e m le a1 (Vint (Int64.hiword va)) -> + eval_expr ge sp e m le a2 (Vint (Int64.loword va)) -> + eval_expr ge sp e m le b1 (Vint (Int64.hiword vb)) -> + eval_expr ge sp e m le b2 (Vint (Int64.loword vb)) -> + eval_expr ge sp e m le (f a1 a2 b1 b2) v) -> + eval_expr ge sp e m le (splitlong2 a b f) v. +Proof. + assert (INV: forall v1 v2 n, + Val.longofwords v1 v2 = Vlong n -> v1 = Vint(Int64.hiword n) /\ v2 = Vint(Int64.loword n)). + { + intros. destruct v1; simpl in H; try discriminate. destruct v2; inv H. + rewrite Int64.hi_ofwords; rewrite Int64.lo_ofwords; auto. + } + intros until v. + unfold splitlong2. case (splitlong2_match a b); intros. +- InvEval. exploit INV. eexact H. intros [EQ1 EQ2]. exploit INV. eexact H0. intros [EQ3 EQ4]. + subst. auto. +- InvEval. exploit INV; eauto. intros [EQ1 EQ2]. subst. + econstructor. eauto. apply H1; EvalOp. +- InvEval. exploit INV; eauto. intros [EQ1 EQ2]. subst. + econstructor. eauto. apply H1; EvalOp. +- EvalOp. apply H1; EvalOp. +Qed. + Lemma is_longconst_sound: forall le a x n, is_longconst a = Some n -> @@ -891,35 +932,49 @@ Proof. Qed. Lemma eval_cmpl_eq_zero: - unary_constructor_sound cmpl_eq_zero (fun v => Val.cmpl Ceq v (Vlong Int64.zero)). + forall le a x, + eval_expr ge sp e m le a (Vlong x) -> + eval_expr ge sp e m le (cmpl_eq_zero a) (Val.of_bool (Int64.eq x Int64.zero)). Proof. - red; intros. unfold cmpl_eq_zero. - apply eval_splitlong with (sem := fun x => Val.cmpl Ceq x (Vlong Int64.zero)); auto. -- intros. - exploit eval_or. eexact H0. eexact H1. intros [v1 [A1 B1]]. + intros. unfold cmpl_eq_zero. + eapply eval_splitlong_strict; eauto. intros. + exploit eval_or. eexact H0. eexact H1. intros [v1 [A1 B1]]. simpl in B1; inv B1. exploit eval_comp. eexact A1. instantiate (2 := Eop (Ointconst Int.zero) Enil). EvalOp. - instantiate (1 := Ceq). intros [v2 [A2 B2]]. - exists v2; split. auto. intros; subst. - simpl in B1; inv B1. unfold Val.cmp in B2; simpl in B2. - unfold Val.cmpl; simpl. rewrite decompose_cmpl_eq_zero. - destruct (Int.eq (Int.or p q)); inv B2; auto. -- destruct x; auto. + instantiate (1 := Ceq). intros [v2 [A2 B2]]. + unfold Val.cmp in B2; simpl in B2. + rewrite <- decompose_cmpl_eq_zero in B2. + rewrite Int64.ofwords_recompose in B2. + destruct (Int64.eq x Int64.zero); inv B2; auto. Qed. Lemma eval_cmpl_ne_zero: - unary_constructor_sound cmpl_ne_zero (fun v => Val.cmpl Cne v (Vlong Int64.zero)). + forall le a x, + eval_expr ge sp e m le a (Vlong x) -> + eval_expr ge sp e m le (cmpl_ne_zero a) (Val.of_bool (negb (Int64.eq x Int64.zero))). Proof. - red; intros. unfold cmpl_eq_zero. - apply eval_splitlong with (sem := fun x => Val.cmpl Cne x (Vlong Int64.zero)); auto. -- intros. - exploit eval_or. eexact H0. eexact H1. intros [v1 [A1 B1]]. + intros. unfold cmpl_ne_zero. + eapply eval_splitlong_strict; eauto. intros. + exploit eval_or. eexact H0. eexact H1. intros [v1 [A1 B1]]. simpl in B1; inv B1. exploit eval_comp. eexact A1. instantiate (2 := Eop (Ointconst Int.zero) Enil). EvalOp. - instantiate (1 := Cne). intros [v2 [A2 B2]]. - exists v2; split. auto. intros; subst. - simpl in B1; inv B1. unfold Val.cmp in B2; simpl in B2. - unfold Val.cmpl; simpl. rewrite decompose_cmpl_eq_zero. - destruct (Int.eq (Int.or p q)); inv B2; auto. -- destruct x; auto. + instantiate (1 := Cne). intros [v2 [A2 B2]]. + unfold Val.cmp in B2; simpl in B2. + rewrite <- decompose_cmpl_eq_zero in B2. + rewrite Int64.ofwords_recompose in B2. + destruct (negb (Int64.eq x Int64.zero)); inv B2; auto. +Qed. + +Lemma eval_cmplu_gen: + forall ch cl a b le x y, + eval_expr ge sp e m le a (Vlong x) -> + eval_expr ge sp e m le b (Vlong y) -> + eval_expr ge sp e m le (cmplu_gen ch cl a b) + (Val.of_bool (if Int.eq (Int64.hiword x) (Int64.hiword y) + then Int.cmpu cl (Int64.loword x) (Int64.loword y) + else Int.cmpu ch (Int64.hiword x) (Int64.hiword y))). +Proof. + intros. unfold cmplu_gen. eapply eval_splitlong2_strict; eauto. intros. + econstructor. econstructor. EvalOp. simpl. eauto. + destruct (Int.eq (Int64.hiword x) (Int64.hiword y)); EvalOp. Qed. Remark int64_eq_xor: @@ -933,44 +988,57 @@ Proof. auto. Qed. -Theorem eval_cmplu: forall c, binary_constructor_sound (cmplu hf c) (Val.cmplu c). +Theorem eval_cmplu: + forall c le a x b y v, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.cmplu c x y = Some v -> + eval_expr ge sp e m le (cmplu c a b) v. Proof. - intros; red; intros. unfold cmplu. - set (default := comp c (Eexternal (i64_ucmp hf) sig_ll_i (a ::: b ::: Enil)) - (Eop (Ointconst Int.zero) Enil)). - assert (DEFAULT: - exists v, eval_expr ge sp e m le default v /\ Val.lessdef (Val.cmplu c x y) v). - { - assert (HELP: exists z, helper_implements ge hf.(i64_ucmp) sig_ll_i (x::y::nil) z - /\ Val.cmplu c x y = Val.cmp c z Vzero) - by UseHelper. - destruct HELP as [z [A B]]. - exploit eval_comp. eapply eval_helper_2. eexact H. eexact H0. eauto. - instantiate (2 := Eop (Ointconst Int.zero) Enil). EvalOp. - instantiate (1 := c). fold Vzero. intros [v [C D]]. - econstructor; split; eauto. congruence. - } - destruct c; auto. + intros. unfold Val.cmplu in H1. + destruct x; simpl in H1; try discriminate. destruct y; inv H1. + rename i into x. rename i0 into y. + destruct c; simpl. - (* Ceq *) destruct (is_longconst_zero b) eqn:LC. -+ exploit is_longconst_zero_sound; eauto. intros EQ; subst; clear H0. ++ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0. apply eval_cmpl_eq_zero; auto. -+ exploit eval_xorl. eexact H. eexact H0. intros [v [A B]]. - exploit eval_cmpl_eq_zero. eexact A. intros [v' [C D]]. - exists v'; split; auto. - eapply Val.lessdef_trans; [idtac|eexact D]. - destruct x; auto. destruct y; auto. simpl in B; inv B. - unfold Val.cmplu, Val.cmpl; simpl. rewrite int64_eq_xor; auto. ++ exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B. inv B. + rewrite int64_eq_xor. apply eval_cmpl_eq_zero; auto. - (* Cne *) destruct (is_longconst_zero b) eqn:LC. -+ exploit is_longconst_zero_sound; eauto. intros EQ; subst; clear H0. ++ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0. apply eval_cmpl_ne_zero; auto. -+ exploit eval_xorl. eexact H. eexact H0. intros [v [A B]]. - exploit eval_cmpl_ne_zero. eexact A. intros [v' [C D]]. - exists v'; split; auto. - eapply Val.lessdef_trans; [idtac|eexact D]. - destruct x; auto. destruct y; auto. simpl in B; inv B. - unfold Val.cmplu, Val.cmpl; simpl. rewrite int64_eq_xor; auto. ++ exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B. inv B. + rewrite int64_eq_xor. apply eval_cmpl_ne_zero; auto. +- (* Clt *) + exploit (eval_cmplu_gen Clt Clt). eexact H. eexact H0. simpl. + rewrite <- Int64.decompose_ltu. rewrite ! Int64.ofwords_recompose. auto. +- (* Cle *) + exploit (eval_cmplu_gen Clt Cle). eexact H. eexact H0. intros. + rewrite <- (Int64.ofwords_recompose x). rewrite <- (Int64.ofwords_recompose y). + rewrite Int64.decompose_leu. auto. +- (* Cgt *) + exploit (eval_cmplu_gen Cgt Cgt). eexact H. eexact H0. simpl. + rewrite Int.eq_sym. rewrite <- Int64.decompose_ltu. rewrite ! Int64.ofwords_recompose. auto. +- (* Cge *) + exploit (eval_cmplu_gen Cgt Cge). eexact H. eexact H0. intros. + rewrite <- (Int64.ofwords_recompose x). rewrite <- (Int64.ofwords_recompose y). + rewrite Int64.decompose_leu. rewrite Int.eq_sym. auto. +Qed. + +Lemma eval_cmpl_gen: + forall ch cl a b le x y, + eval_expr ge sp e m le a (Vlong x) -> + eval_expr ge sp e m le b (Vlong y) -> + eval_expr ge sp e m le (cmpl_gen ch cl a b) + (Val.of_bool (if Int.eq (Int64.hiword x) (Int64.hiword y) + then Int.cmpu cl (Int64.loword x) (Int64.loword y) + else Int.cmp ch (Int64.hiword x) (Int64.hiword y))). +Proof. + intros. unfold cmpl_gen. eapply eval_splitlong2_strict; eauto. intros. + econstructor. econstructor. EvalOp. simpl. eauto. + destruct (Int.eq (Int64.hiword x) (Int64.hiword y)); EvalOp. Qed. Remark decompose_cmpl_lt_zero: @@ -991,72 +1059,61 @@ Proof. vm_compute. intuition congruence. Qed. -Theorem eval_cmpl: forall c, binary_constructor_sound (cmpl hf c) (Val.cmpl c). +Theorem eval_cmpl: + forall c le a x b y v, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.cmpl c x y = Some v -> + eval_expr ge sp e m le (cmpl c a b) v. Proof. - intros; red; intros. unfold cmpl. - set (default := comp c (Eexternal (i64_scmp hf) sig_ll_i (a ::: b ::: Enil)) - (Eop (Ointconst Int.zero) Enil)). - assert (DEFAULT: - exists v, eval_expr ge sp e m le default v /\ Val.lessdef (Val.cmpl c x y) v). - { - assert (HELP: exists z, helper_implements ge hf.(i64_scmp) sig_ll_i (x::y::nil) z - /\ Val.cmpl c x y = Val.cmp c z Vzero) - by UseHelper. - destruct HELP as [z [A B]]. - exploit eval_comp. eapply eval_helper_2. eexact H. eexact H0. eauto. - instantiate (2 := Eop (Ointconst Int.zero) Enil). EvalOp. - instantiate (1 := c). fold Vzero. intros [v [C D]]. - econstructor; split; eauto. congruence. - } - destruct c; auto. + intros. unfold Val.cmpl in H1. + destruct x; simpl in H1; try discriminate. destruct y; inv H1. + rename i into x. rename i0 into y. + destruct c; simpl. - (* Ceq *) destruct (is_longconst_zero b) eqn:LC. -+ exploit is_longconst_zero_sound; eauto. intros EQ; subst; clear H0. ++ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0. apply eval_cmpl_eq_zero; auto. -+ exploit eval_xorl. eexact H. eexact H0. intros [v [A B]]. - exploit eval_cmpl_eq_zero. eexact A. intros [v' [C D]]. - exists v'; split; auto. - eapply Val.lessdef_trans; [idtac|eexact D]. - destruct x; auto. destruct y; auto. simpl in B; inv B. - unfold Val.cmpl; simpl. rewrite int64_eq_xor; auto. ++ exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B; inv B. + rewrite int64_eq_xor. apply eval_cmpl_eq_zero; auto. - (* Cne *) destruct (is_longconst_zero b) eqn:LC. -+ exploit is_longconst_zero_sound; eauto. intros EQ; subst; clear H0. ++ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0. apply eval_cmpl_ne_zero; auto. -+ exploit eval_xorl. eexact H. eexact H0. intros [v [A B]]. - exploit eval_cmpl_ne_zero. eexact A. intros [v' [C D]]. - exists v'; split; auto. - eapply Val.lessdef_trans; [idtac|eexact D]. - destruct x; auto. destruct y; auto. simpl in B; inv B. - unfold Val.cmpl; simpl. rewrite int64_eq_xor; auto. ++ exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B; inv B. + rewrite int64_eq_xor. apply eval_cmpl_ne_zero; auto. - (* Clt *) destruct (is_longconst_zero b) eqn:LC. -+ exploit is_longconst_zero_sound; eauto. intros EQ; subst; clear H0. - exploit eval_highlong. eexact H. intros [v1 [A1 B1]]. ++ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0. + exploit eval_highlong. eexact H. intros [v1 [A1 B1]]. simpl in B1. inv B1. exploit eval_comp. eexact A1. instantiate (2 := Eop (Ointconst Int.zero) Enil). EvalOp. instantiate (1 := Clt). intros [v2 [A2 B2]]. - econstructor; split. eauto. - destruct x; simpl in *; auto. inv B1. - unfold Val.cmp, Val.cmp_bool, Val.of_optbool, Int.cmp in B2. - unfold Val.cmpl, Val.cmpl_bool, Val.of_optbool, Int64.cmp. - rewrite <- (Int64.ofwords_recompose i). rewrite decompose_cmpl_lt_zero. - auto. -+ apply DEFAULT. + unfold Val.cmp in B2. simpl in B2. + rewrite <- (Int64.ofwords_recompose x). rewrite decompose_cmpl_lt_zero. + destruct (Int.lt (Int64.hiword x) Int.zero); inv B2; auto. ++ exploit (eval_cmpl_gen Clt Clt). eexact H. eexact H0. simpl. + rewrite <- Int64.decompose_lt. rewrite ! Int64.ofwords_recompose. auto. +- (* Cle *) + exploit (eval_cmpl_gen Clt Cle). eexact H. eexact H0. intros. + rewrite <- (Int64.ofwords_recompose x). rewrite <- (Int64.ofwords_recompose y). + rewrite Int64.decompose_le. auto. +- (* Cgt *) + exploit (eval_cmpl_gen Cgt Cgt). eexact H. eexact H0. simpl. + rewrite Int.eq_sym. rewrite <- Int64.decompose_lt. rewrite ! Int64.ofwords_recompose. auto. - (* Cge *) destruct (is_longconst_zero b) eqn:LC. -+ exploit is_longconst_zero_sound; eauto. intros EQ; subst; clear H0. - exploit eval_highlong. eexact H. intros [v1 [A1 B1]]. ++ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0. + exploit eval_highlong. eexact H. intros [v1 [A1 B1]]. simpl in B1; inv B1. exploit eval_comp. eexact A1. instantiate (2 := Eop (Ointconst Int.zero) Enil). EvalOp. instantiate (1 := Cge). intros [v2 [A2 B2]]. - econstructor; split. eauto. - destruct x; simpl in *; auto. inv B1. - unfold Val.cmp, Val.cmp_bool, Val.of_optbool, Int.cmp in B2. - unfold Val.cmpl, Val.cmpl_bool, Val.of_optbool, Int64.cmp. - rewrite <- (Int64.ofwords_recompose i). rewrite decompose_cmpl_lt_zero. - auto. -+ apply DEFAULT. + unfold Val.cmp in B2; simpl in B2. + rewrite <- (Int64.ofwords_recompose x). rewrite decompose_cmpl_lt_zero. + destruct (negb (Int.lt (Int64.hiword x) Int.zero)); inv B2; auto. ++ exploit (eval_cmpl_gen Cgt Cge). eexact H. eexact H0. intros. + rewrite <- (Int64.ofwords_recompose x). rewrite <- (Int64.ofwords_recompose y). + rewrite Int64.decompose_le. rewrite Int.eq_sym. auto. Qed. End CMCONSTR. diff --git a/backend/Selection.v b/backend/Selection.v index 7964feb..edc63cd 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -37,10 +37,12 @@ Open Local Scope cminorsel_scope. (** Conversion of conditions *) -Function condition_of_expr (e: expr) : condition * exprlist := +Function condexpr_of_expr (e: expr) : condexpr := match e with - | Eop (Ocmp c) el => (c, el) - | _ => (Ccompuimm Cne Int.zero, e ::: Enil) + | Eop (Ocmp c) el => CEcond c el + | Econdition a b c => CEcondition a (condexpr_of_expr b) (condexpr_of_expr c) + | Elet a b => CElet a (condexpr_of_expr b) + | _ => CEcond (Ccompuimm Cne Int.zero) (e ::: Enil) end. (** Conversion of loads and stores *) @@ -133,8 +135,8 @@ Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr := | Cminor.Ocmp c => comp c arg1 arg2 | Cminor.Ocmpu c => compu c arg1 arg2 | Cminor.Ocmpf c => compf c arg1 arg2 - | Cminor.Ocmpl c => cmpl hf c arg1 arg2 - | Cminor.Ocmplu c => cmplu hf c arg1 arg2 + | Cminor.Ocmpl c => cmpl c arg1 arg2 + | Cminor.Ocmplu c => cmplu c arg1 arg2 end. (** Conversion from Cminor expression to Cminorsel expressions *) @@ -205,8 +207,8 @@ Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : stmt := end | Cminor.Sseq s1 s2 => Sseq (sel_stmt ge s1) (sel_stmt ge s2) | Cminor.Sifthenelse e ifso ifnot => - let (cond, args) := condition_of_expr (sel_expr e) in - Sifthenelse cond args (sel_stmt ge ifso) (sel_stmt ge ifnot) + Sifthenelse (condexpr_of_expr (sel_expr e)) + (sel_stmt ge ifso) (sel_stmt ge ifnot) | Cminor.Sloop body => Sloop (sel_stmt ge body) | Cminor.Sblock body => Sblock (sel_stmt ge body) | Cminor.Sexit n => Sexit n diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 525a29d..93a5c51 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -117,8 +117,6 @@ Proof. repeat (match goal with [ H: _ /\ _ |- _ /\ _ ] => destruct H; split end); intros; try (eapply helper_implements_preserved; eauto); try (eapply builtin_implements_preserved; eauto). - exploit H14; eauto. intros [z [A B]]. exists z; split; eauto. eapply helper_implements_preserved; eauto. - exploit H15; eauto. intros [z [A B]]. exists z; split; eauto. eapply helper_implements_preserved; eauto. Qed. Section CMCONSTR. @@ -127,22 +125,22 @@ Variable sp: val. Variable e: env. Variable m: mem. -Lemma eval_condition_of_expr: - forall le a v b, +Lemma eval_condexpr_of_expr: + forall a le v b, eval_expr tge sp e m le a v -> Val.bool_of_val v b -> - match condition_of_expr a with (cond, args) => - exists vl, - eval_exprlist tge sp e m le args vl /\ - eval_condition cond vl m = Some b - end. + eval_condexpr tge sp e m le (condexpr_of_expr a) b. Proof. - intros until a. functional induction (condition_of_expr a); intros. + intros until a. functional induction (condexpr_of_expr a); intros. (* compare *) - inv H. exists vl; split; auto. + inv H. econstructor; eauto. simpl in H6. inv H6. apply Val.bool_of_val_of_optbool. auto. +(* condition *) + inv H. econstructor; eauto. destruct va; eauto. +(* let *) + inv H. econstructor; eauto. (* default *) - exists (v :: nil); split. constructor. auto. constructor. + econstructor. constructor. eauto. constructor. simpl. inv H0. auto. auto. Qed. @@ -248,8 +246,8 @@ Proof. apply eval_comp; auto. apply eval_compu; auto. apply eval_compf; auto. - apply eval_cmpl; auto. - apply eval_cmplu; auto. + exists v; split; auto. eapply eval_cmpl; eauto. + exists v; split; auto. eapply eval_cmplu; eauto. Qed. End CMCONSTR. @@ -495,7 +493,6 @@ Proof. destruct (find_label lbl (sel_stmt hf ge s1) (Kseq (sel_stmt hf ge s2) k')) as [[sy ky] | ]; intuition. apply IHs2; auto. (* ifthenelse *) - destruct (condition_of_expr (sel_expr hf e)) as [cond args]. simpl. exploit (IHs1 k); eauto. destruct (Cminor.find_label lbl s1 k) as [[sx kx] | ]; destruct (find_label lbl (sel_stmt hf ge s1) k') as [[sy ky] | ]; @@ -594,11 +591,8 @@ Proof. (* Sifthenelse *) exploit sel_expr_correct; eauto. intros [v' [A B]]. assert (Val.bool_of_val v' b). inv B. auto. inv H0. - exploit eval_condition_of_expr; eauto. - destruct (condition_of_expr (sel_expr hf a)) as [cond args]. - intros [vl' [C D]]. left; exists (State (sel_function hf ge f) (if b then sel_stmt hf ge s1 else sel_stmt hf ge s2) k' sp e' m'); split. - econstructor; eauto. + econstructor; eauto. eapply eval_condexpr_of_expr; eauto. constructor; auto. destruct b; auto. (* Sloop *) left; econstructor; split. constructor. constructor; auto. constructor; auto. -- cgit v1.2.3