From 65cc3738e7436e46f70c0508638a71fbb49c50a8 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 25 Feb 2012 10:42:34 +0000 Subject: Translate CompCert C's "a ? b : c" to the equivalent simple Clight expr if b and c are simple. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1826 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cstrategy.v | 173 +++++++++++++++++++++++++++------------------ cfrontend/SimplExpr.v | 33 +++++---- cfrontend/SimplExprproof.v | 56 +++++++++++---- cfrontend/SimplExprspec.v | 33 ++++++++- 4 files changed, 197 insertions(+), 98 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index e088c26..4bb550f 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -44,30 +44,30 @@ Variable ge: genv. (** Simple expressions are defined as follows. *) -Fixpoint simple (a: expr) : Prop := +Fixpoint simple (a: expr) : bool := match a with - | Eloc _ _ _ => True - | Evar _ _ => True + | Eloc _ _ _ => true + | Evar _ _ => true | Ederef r _ => simple r | Efield r _ _ => simple r - | Eval _ _ => True - | Evalof l _ => simple l /\ type_is_volatile (typeof l) = false + | Eval _ _ => true + | Evalof l _ => simple l && negb(type_is_volatile (typeof l)) | Eaddrof l _ => simple l | Eunop _ r1 _ => simple r1 - | Ebinop _ r1 r2 _ => simple r1 /\ simple r2 + | Ebinop _ r1 r2 _ => simple r1 && simple r2 | Ecast r1 _ => simple r1 - | Econdition _ _ _ _ => False - | Esizeof _ _ => True - | Eassign _ _ _ => False - | Eassignop _ _ _ _ _ => False - | Epostincr _ _ _ => False - | Ecomma _ _ _ => False - | Ecall _ _ _ => False - | Eparen _ _ => False + | Econdition r1 r2 r3 _ => simple r1 && simple r2 && simple r3 + | Esizeof _ _ => true + | Eassign _ _ _ => false + | Eassignop _ _ _ _ _ => false + | Epostincr _ _ _ => false + | Ecomma _ _ _ => false + | Ecall _ _ _ => false + | Eparen _ _ => false end. -Fixpoint simplelist (rl: exprlist) : Prop := - match rl with Enil => True | Econs r rl' => simple r /\ simplelist rl' end. +Fixpoint simplelist (rl: exprlist) : bool := + match rl with Enil => true | Econs r rl' => simple r && simplelist rl' end. (** Simple expressions have interesting properties: their evaluations always terminate, are deterministic, and preserve the memory state. @@ -125,6 +125,13 @@ with eval_simple_rvalue: expr -> val -> Prop := eval_simple_rvalue r1 v1 -> sem_cast v1 (typeof r1) ty = Some v -> eval_simple_rvalue (Ecast r1 ty) v + | esr_condition: forall r1 r2 r3 ty v1 b v2 v, + simple r2 = true -> simple r3 = true -> + eval_simple_rvalue r1 v1 -> + bool_val v1 (typeof r1) = Some b -> + eval_simple_rvalue (if b then r2 else r3) v2 -> + sem_cast v2 (typeof (if b then r2 else r3)) ty = Some v -> + eval_simple_rvalue (Econdition r1 r2 r3 ty) v | esr_sizeof: forall ty1 ty, eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ty1))). @@ -161,7 +168,7 @@ Inductive leftcontext: kind -> kind -> (expr -> expr) -> Prop := | lctx_binop_left: forall k C op e2 ty, leftcontext k RV C -> leftcontext k RV (fun x => Ebinop op (C x) e2 ty) | lctx_binop_right: forall k C op e1 ty, - simple e1 -> leftcontext k RV C -> + simple e1 = true -> leftcontext k RV C -> leftcontext k RV (fun x => Ebinop op e1 (C x) ty) | lctx_cast: forall k C ty, leftcontext k RV C -> leftcontext k RV (fun x => Ecast (C x) ty) @@ -170,19 +177,19 @@ Inductive leftcontext: kind -> kind -> (expr -> expr) -> Prop := | lctx_assign_left: forall k C e2 ty, leftcontext k LV C -> leftcontext k RV (fun x => Eassign (C x) e2 ty) | lctx_assign_right: forall k C e1 ty, - simple e1 -> leftcontext k RV C -> + simple e1 = true -> leftcontext k RV C -> leftcontext k RV (fun x => Eassign e1 (C x) ty) | lctx_assignop_left: forall k C op e2 tyres ty, leftcontext k LV C -> leftcontext k RV (fun x => Eassignop op (C x) e2 tyres ty) | lctx_assignop_right: forall k C op e1 tyres ty, - simple e1 -> leftcontext k RV C -> + simple e1 = true -> leftcontext k RV C -> leftcontext k RV (fun x => Eassignop op e1 (C x) tyres ty) | lctx_postincr: forall k C id ty, leftcontext k LV C -> leftcontext k RV (fun x => Epostincr id (C x) ty) | lctx_call_left: forall k C el ty, leftcontext k RV C -> leftcontext k RV (fun x => Ecall (C x) el ty) | lctx_call_right: forall k C e1 ty, - simple e1 -> leftcontextlist k C -> + simple e1 = true -> leftcontextlist k C -> leftcontext k RV (fun x => Ecall e1 (C x) ty) | lctx_comma: forall k C e2 ty, leftcontext k RV C -> leftcontext k RV (fun x => Ecomma (C x) e2 ty) @@ -193,7 +200,7 @@ with leftcontextlist: kind -> (expr -> exprlist) -> Prop := | lctx_list_head: forall k C el, leftcontext k RV C -> leftcontextlist k (fun x => Econs (C x) el) | lctx_list_tail: forall k C e1, - simple e1 -> leftcontextlist k C -> + simple e1 = true -> leftcontextlist k C -> leftcontextlist k (fun x => Econs e1 (C x)). Lemma leftcontext_context: @@ -231,6 +238,7 @@ Inductive estep: state -> trace -> state -> Prop := t (ExprState f (C (Eval v ty)) k e m) | step_condition: forall f C r1 r2 r3 ty k e m v b, + simple r2 = false \/ simple r3 = false -> leftcontext RV RV C -> eval_simple_rvalue e m r1 v -> bool_val v (typeof r1) = Some b -> @@ -670,6 +678,12 @@ Ltac FinishL := apply star_one; left; apply step_lred; eauto; simpl; try (econst FinishR. (* cast *) Steps H0 (fun x => C(Ecast x ty)). FinishR. +(* condition *) + Steps H2 (fun x => C(Econdition x r2 r3 ty)). + eapply star_left with (s2 := ExprState f (C (Eparen (if b then r2 else r3) ty)) k e m). + left; apply step_rred; eauto. constructor; auto. + Steps H5 (fun x => C(Eparen x ty)). + FinishR. auto. (* sizeof *) FinishR. (* loc *) @@ -720,7 +734,7 @@ Qed. Lemma simple_can_eval: forall a from C, - simple a -> context from RV C -> safe (ExprState f (C a) k e m) -> + simple a = true -> context from RV C -> safe (ExprState f (C a) k e m) -> match from with | LV => exists b, exists ofs, eval_simple_lvalue e m a b ofs | RV => exists v, eval_simple_rvalue e m a v @@ -742,7 +756,7 @@ Ltac StepR REC C' a := induction a; intros from C S CTX SAFE; generalize (safe_expr_kind _ _ _ _ _ _ _ CTX SAFE); intro K; subst; - simpl in S; try contradiction; simpl. + simpl in S; try discriminate; simpl. (* val *) exists v; constructor. (* var *) @@ -756,7 +770,8 @@ Ltac StepR REC C' a := destruct TY as [delta OFS]. exists b; exists (Int.add ofs (Int.repr delta)); econstructor; eauto. exists b; exists ofs; econstructor; eauto. (* valof *) - destruct S. StepL IHa (fun x => C(Evalof x ty)) a. + destruct (andb_prop _ _ S) as [S1 S2]. clear S. rewrite negb_true_iff in S2. + StepL IHa (fun x => C(Evalof x ty)) a. exploit safe_inv. eexact SAFE0. eauto. simpl. intros [TY [t [v LOAD]]]. assert (t = E0). inv LOAD; auto. congruence. subst t. exists v; econstructor; eauto. congruence. @@ -772,7 +787,7 @@ Ltac StepR REC C' a := exploit safe_inv. eexact SAFE0. eauto. simpl. intros [v' EQ]. exists v'; econstructor; eauto. (* binop *) - destruct S. + destruct (andb_prop _ _ S) as [S1 S2]; clear S. StepR IHa1 (fun x => C(Ebinop op x a2 ty)) a1. StepR IHa2 (fun x => C(Ebinop op (Eval v (typeof a1)) x ty)) a2. exploit safe_inv. eexact SAFE1. eauto. simpl. intros [v' EQ]. @@ -781,6 +796,23 @@ Ltac StepR REC C' a := StepR IHa (fun x => C(Ecast x ty)) a. exploit safe_inv. eexact SAFE0. eauto. simpl. intros [v' CAST]. exists v'; econstructor; eauto. +(* condition *) + destruct (andb_prop _ _ S) as [S' S3]. destruct (andb_prop _ _ S') as [S1 S2]. clear S S'. + StepR IHa1 (fun x => C(Econdition x a2 a3 ty)) a1. + exploit safe_inv. eexact SAFE0. eauto. simpl. intros [b BV]. + set (a' := if b then a2 else a3). + assert (SAFE1: safe (ExprState f (C (Eparen a' ty)) k e m)). + eapply safe_steps. eexact SAFE0. apply star_one. left; apply step_rred; auto. + unfold a'; constructor; auto. + assert (EV': exists v, eval_simple_rvalue e m a' v). + unfold a'; destruct b. + eapply (IHa2 RV (fun x => C(Eparen x ty))); eauto. + eapply (IHa3 RV (fun x => C(Eparen x ty))); eauto. + destruct EV' as [v1 E1]. + exploit safe_inv. eapply (eval_simple_rvalue_safe (fun x => C(Eparen x ty))). + eexact E1. eauto. auto. eauto. + simpl. intros [v2 CAST]. + exists v2. econstructor; eauto. (* sizeof *) econstructor; econstructor. (* loc *) @@ -789,7 +821,7 @@ Qed. Lemma simple_can_eval_rval: forall r C, - simple r -> context RV RV C -> safe (ExprState f (C r) k e m) -> + simple r = true -> context RV RV C -> safe (ExprState f (C r) k e m) -> exists v, eval_simple_rvalue e m r v /\ safe (ExprState f (C (Eval v (typeof r))) k e m). Proof. @@ -799,7 +831,7 @@ Qed. Lemma simple_can_eval_lval: forall l C, - simple l -> context LV RV C -> safe (ExprState f (C l) k e m) -> + simple l = true -> context LV RV C -> safe (ExprState f (C l) k e m) -> exists b, exists ofs, eval_simple_lvalue e m l b ofs /\ safe (ExprState f (C (Eloc b ofs (typeof l))) k e m). Proof. @@ -916,14 +948,14 @@ Qed. Lemma simple_list_can_eval: forall rl C, - simplelist rl -> + simplelist rl = true -> contextlist' C -> safe (ExprState f (C rl) k e m) -> exists vl, eval_simple_list' rl vl. Proof. induction rl; intros. econstructor; constructor. - simpl in H; destruct H. + simpl in H. destruct (andb_prop _ _ H). exploit (simple_can_eval r1 RV (fun x => C(Econs x rl))); eauto. intros [v1 EV1]. exploit (IHrl (fun x => C(Econs (Eval v1 (typeof r1)) x))); eauto. @@ -952,14 +984,14 @@ Variable m: mem. Definition simple_side_effect (r: expr) : Prop := match r with - | Evalof l _ => simple l /\ type_is_volatile (typeof l) = true - | Econdition r1 r2 r3 _ => simple r1 - | Eassign l1 r2 _ => simple l1 /\ simple r2 - | Eassignop _ l1 r2 _ _ => simple l1 /\ simple r2 - | Epostincr _ l1 _ => simple l1 - | Ecomma r1 r2 _ => simple r1 - | Ecall r1 rl _ => simple r1 /\ simplelist rl - | Eparen r1 _ => simple r1 + | Evalof l _ => simple l = true /\ type_is_volatile (typeof l) = true + | Econdition r1 r2 r3 _ => simple r1 = true /\ (simple r2 = false \/ simple r3 = false) + | Eassign l1 r2 _ => simple l1 = true /\ simple r2 = true + | Eassignop _ l1 r2 _ _ => simple l1 = true /\ simple r2 = true + | Epostincr _ l1 _ => simple l1 = true + | Ecomma r1 r2 _ => simple r1 = true + | Ecall r1 rl _ => simple r1 = true /\ simplelist rl = true + | Eparen r1 _ => simple r1 = true | _ => False end. @@ -972,11 +1004,11 @@ Hint Constructors leftcontext leftcontextlist. Lemma decompose_expr: (forall a from C, context from RV C -> safe (ExprState f (C a) k e m) -> - simple a + simple a = true \/ exists C', exists a', a = C' a' /\ simple_side_effect a' /\ leftcontext RV from C') /\(forall rl C, contextlist' C -> safe (ExprState f (C rl) k e m) -> - simplelist rl + simplelist rl = true \/ exists C', exists a', rl = C' a' /\ simple_side_effect a' /\ leftcontextlist RV C'). Proof. apply expr_expr_list_ind; intros; simpl; auto. @@ -995,7 +1027,7 @@ Ltac Base := (* rvalof *) Kind. Rec H LV C (fun x => Evalof x ty). destruct (type_is_volatile (typeof l)) as []_eqn. - Base. auto. + Base. rewrite H2; auto. (* deref *) Kind. Rec H RV C (fun x => Ederef x ty). (* addrof *) @@ -1003,11 +1035,14 @@ Ltac Base := (* unop *) Kind. Rec H RV C (fun x => Eunop op x ty). (* binop *) - Kind. Rec H RV C (fun x => Ebinop op x r2 ty). Rec H0 RV C (fun x => Ebinop op r1 x ty). + Kind. Rec H RV C (fun x => Ebinop op x r2 ty). rewrite H3. + Rec H0 RV C (fun x => Ebinop op r1 x ty). (* cast *) Kind. Rec H RV C (fun x => Ecast x ty). (* condition *) - Kind. Rec H RV C (fun x => Econdition x r2 r3 ty). Base. + Kind. Rec H RV C (fun x => Econdition x r2 r3 ty). rewrite H4; simpl. + destruct (simple r2 && simple r3) as []_eqn. auto. + rewrite andb_false_iff in Heqb. Base. (* assign *) Kind. Rec H LV C (fun x => Eassign x r ty). Rec H0 RV C (fun x => Eassign l x ty). Base. (* assignop *) @@ -1028,8 +1063,8 @@ Ltac Base := destruct (H RV (fun x => C (Econs x rl))) as [A | [C' [a' [A [B D]]]]]. eapply contextlist'_head; eauto. auto. destruct (H0 (fun x => C (Econs r1 x))) as [A' | [C' [a' [A' [B D]]]]]. - eapply contextlist'_tail; eauto. auto. - auto. + eapply contextlist'_tail; eauto. auto. + rewrite A; rewrite A'; auto. right; exists (fun x => Econs r1 (C' x)); exists a'. rewrite A'; eauto. right; exists (fun x => Econs (C' x) rl); exists a'. rewrite A; eauto. Qed. @@ -1037,7 +1072,7 @@ Qed. Lemma decompose_topexpr: forall a, safe (ExprState f a k e m) -> - simple a + simple a = true \/ exists C, exists a', a = C a' /\ simple_side_effect a' /\ leftcontext RV RV C. Proof. intros. eapply (proj1 decompose_expr). apply ctx_top. auto. @@ -1178,6 +1213,7 @@ Proof. exploit safe_inv. eexact S1. eauto. simpl. intros [A [t [v B]]]. econstructor; econstructor; eapply step_rvalof_volatile; eauto. congruence. (* condition *) + destruct Q. exploit (simple_can_eval_rval f k e m b1 (fun x => C(Econdition x b2 b3 ty))); eauto. intros [v1 [E1 S1]]. exploit safe_inv. eexact S1. eauto. simpl. intros [b BV]. @@ -1541,6 +1577,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop := eval_expr e m RV a t m' a' -> eval_expr e m RV (Ecast a ty) t m' (Ecast a' ty) | eval_condition: forall e m a1 a2 a3 ty t1 m' a1' v1 t2 m'' a' v' b v, + simple a2 = false \/ simple a3 = false -> eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> bool_val v1 (typeof a1) = Some b -> eval_expr e m' RV (if b then a2 else a3) t2 m'' a' -> eval_simple_rvalue ge e m'' a' v' -> @@ -1774,7 +1811,8 @@ CoInductive evalinf_expr: env -> mem -> kind -> expr -> traceinf -> Prop := | evalinf_condition: forall e m a1 a2 a3 ty t1, evalinf_expr e m RV a1 t1 -> evalinf_expr e m RV (Econdition a1 a2 a3 ty) t1 - | evalinf_condition_true: forall e m a1 a2 a3 ty t1 m' a1' v1 t2 b, + | evalinf_condition_2: forall e m a1 a2 a3 ty t1 m' a1' v1 t2 b, + simple a2 = false \/ simple a3 = false -> eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> bool_val v1 (typeof a1) = Some b -> evalinf_expr e m' RV (if b then a2 else a3) t2 -> @@ -1973,17 +2011,18 @@ Qed. Lemma exprlist_app_leftcontext: forall rl1 rl2, - simplelist rl1 -> leftcontextlist RV (fun x => exprlist_app rl1 (Econs x rl2)). + simplelist rl1 = true -> leftcontextlist RV (fun x => exprlist_app rl1 (Econs x rl2)). Proof. induction rl1; simpl; intros. apply lctx_list_head. constructor. - destruct H. apply lctx_list_tail. auto. auto. + destruct (andb_prop _ _ H). apply lctx_list_tail. auto. auto. Qed. Lemma exprlist_app_simple: - forall rl1 rl2, simplelist rl1 -> simplelist rl2 -> simplelist (exprlist_app rl1 rl2). + forall rl1 rl2, + simplelist (exprlist_app rl1 rl2) = simplelist rl1 && simplelist rl2. Proof. - induction rl1; simpl; intros. auto. destruct H; auto. + induction rl1; intros; simpl. auto. rewrite IHrl1. apply andb_assoc. Qed. Lemma bigstep_to_steps: @@ -1994,12 +2033,12 @@ Lemma bigstep_to_steps: /\(forall e m K a t m' a', eval_expr e m K a t m' a' -> forall C f k, leftcontext K RV C -> - simple a' /\ typeof a' = typeof a /\ + simple a' = true /\ typeof a' = typeof a /\ star step ge (ExprState f (C a) k e m) t (ExprState f (C a') k e m')) /\(forall e m al t m' al', eval_exprlist e m al t m' al' -> - forall a1 al2 ty C f k, leftcontext RV RV C -> simple a1 -> simplelist al2 -> - simplelist al' /\ + forall a1 al2 ty C f k, leftcontext RV RV C -> simple a1 = true -> simplelist al2 = true -> + simplelist al' = true /\ star step ge (ExprState f (C (Ecall a1 (exprlist_app al2 al) ty)) k e m) t (ExprState f (C (Ecall a1 (exprlist_app al2 al') ty)) k e m')) /\(forall e m s t m' out, @@ -2033,7 +2072,7 @@ Proof. (* valof *) exploit (H1 (fun x => C(Evalof x ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. - simpl; intuition; eauto. congruence. + simpl; intuition; eauto. rewrite A; rewrite B; rewrite H; auto. (* valof volatile *) exploit (H1 (fun x => C(Evalof x ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. @@ -2064,11 +2103,11 @@ Proof. eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. simpl; intuition; eauto. (* condition *) - exploit (H0 (fun x => C(Econdition x a2 a3 ty))). + exploit (H1 (fun x => C(Econdition x a2 a3 ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. - exploit (H4 (fun x => C(Eparen x ty))). + exploit (H5 (fun x => C(Eparen x ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [E [F G]]. - simpl; intuition. + simpl. split; auto. split; auto. eapply star_trans. eexact D. eapply star_left. left; eapply step_condition; eauto. rewrite B; eauto. eapply star_right. eexact G. left; eapply step_paren; eauto. congruence. @@ -2115,7 +2154,7 @@ Proof. (* call *) exploit (H0 (fun x => C(Ecall x rargs ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. - exploit (H2 rf' Enil ty C); eauto. red; auto. intros [E F]. + exploit (H2 rf' Enil ty C); eauto. intros [E F]. simpl; intuition. eapply star_trans. eexact D. eapply star_trans. eexact F. @@ -2130,10 +2169,9 @@ Proof. eapply leftcontext_compose; eauto. repeat constructor. auto. apply exprlist_app_leftcontext; auto. intros [A [B D]]. exploit (H2 a0 (exprlist_app al2 (Econs a1' Enil))); eauto. - apply exprlist_app_simple; auto. simpl. auto. + rewrite exprlist_app_simple. simpl. rewrite H5; rewrite A; auto. repeat rewrite exprlist_app_assoc. simpl. intros [E F]. - simpl; intuition. eapply star_trans; eauto. @@ -2398,15 +2436,15 @@ Lemma eval_expr_to_steps: forall e m K a t m' a', eval_expr e m K a t m' a' -> forall C f k, leftcontext K RV C -> - simple a' /\ typeof a' = typeof a /\ + simple a' = true /\ typeof a' = typeof a /\ star step ge (ExprState f (C a) k e m) t (ExprState f (C a') k e m'). Proof (proj1 (proj2 bigstep_to_steps)). Lemma eval_exprlist_to_steps: forall e m al t m' al', eval_exprlist e m al t m' al' -> - forall a1 al2 ty C f k, leftcontext RV RV C -> simple a1 -> simplelist al2 -> - simplelist al' /\ + forall a1 al2 ty C f k, leftcontext RV RV C -> simple a1 = true -> simplelist al2 = true -> + simplelist al' = true /\ star step ge (ExprState f (C (Ecall a1 (exprlist_app al2 al) ty)) k e m) t (ExprState f (C (Ecall a1 (exprlist_app al2 al') ty)) k e m'). Proof (proj1 (proj2 (proj2 bigstep_to_steps))). @@ -2495,7 +2533,7 @@ Proof. assert (COEL: forall e m a t C f k a1 al ty, evalinf_exprlist e m a t -> - leftcontext RV RV C -> simple a1 -> simplelist al -> + leftcontext RV RV C -> simple a1 = true -> simplelist al = true -> forever_N step lt ge (esizelist a) (ExprState f (C (Ecall a1 (exprlist_app al a) ty)) k e m) t). cofix COEL. @@ -2516,7 +2554,8 @@ Proof. change (Econs a1' al0) with (exprlist_app (Econs a1' Enil) al0). rewrite <- exprlist_app_assoc. eapply COEL. eauto. auto. auto. - apply exprlist_app_simple. auto. simpl; auto. traceEq. + rewrite exprlist_app_simple. simpl. rewrite H2; rewrite P; auto. + auto. intros. inv H. (* field *) @@ -2559,7 +2598,7 @@ Proof. eapply COE with (C := fun x => C(Econdition x a2 a3 ty)). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* condition *) - destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Econdition x a2 a3 ty)) f k) + destruct (eval_expr_to_steps _ _ _ _ _ _ _ H2 (fun x => C(Econdition x a2 a3 ty)) f k) as [P [Q R]]. eapply leftcontext_compose; eauto. repeat constructor. eapply forever_N_plus. eapply plus_right. eexact R. @@ -2613,7 +2652,7 @@ Proof. as [P [Q R]]. eapply leftcontext_compose; eauto. repeat constructor. eapply forever_N_star with (a2 := (esizelist a2)). eexact R. simpl; omega. - eapply COEL with (al := Enil). eauto. auto. auto. red; auto. traceEq. + eapply COEL with (al := Enil). eauto. auto. auto. auto. traceEq. (* call *) destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Ecall x rargs ty)) f k) as [P [Q R]]. diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index 1dae78c..7b37692 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -21,6 +21,7 @@ Require Import Values. Require Import AST. Require Import Csyntax. Require Import Csem. +Require Cstrategy. Require Import Clight. Module C := Csyntax. @@ -231,19 +232,25 @@ Fixpoint transl_expr (dst: destination) (a: C.expr) : mon (list statement * expr do (sl1, a1) <- transl_expr For_val r1; ret (finish dst sl1 (Ecast a1 ty)) | C.Econdition r1 r2 r3 ty => - do (sl1, a1) <- transl_expr For_val r1; - do (sl2, a2) <- transl_expr (cast_destination ty dst) r2; - do (sl3, a3) <- transl_expr (cast_destination ty dst) r3; - match dst with - | For_val => - do t <- gensym ty; - ret (sl1 ++ makeif a1 (Ssequence (makeseq sl2) (Sset t (Ecast a2 ty))) - (Ssequence (makeseq sl3) (Sset t (Ecast a3 ty))) :: nil, - Etempvar t ty) - | For_effects | For_test _ _ _ => - ret (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil, - dummy_expr) - end + if Cstrategy.simple r2 && Cstrategy.simple r3 then ( + do (sl1, a1) <- transl_expr For_val r1; + do (sl2, a2) <- transl_expr For_val r2; + do (sl3, a3) <- transl_expr For_val r3; + ret (finish dst sl1 (Econdition a1 a2 a3 ty)) + ) else ( + do (sl1, a1) <- transl_expr For_val r1; + do (sl2, a2) <- transl_expr (cast_destination ty dst) r2; + do (sl3, a3) <- transl_expr (cast_destination ty dst) r3; + match dst with + | For_val => + do t <- gensym ty; + ret (sl1 ++ makeif a1 (Ssequence (makeseq sl2) (Sset t (Ecast a2 ty))) + (Ssequence (makeseq sl3) (Sset t (Ecast a3 ty))) :: nil, + Etempvar t ty) + | For_effects | For_test _ _ _ => + ret (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil, + dummy_expr) + end) | C.Eassign l1 r2 ty => do (sl1, a1) <- transl_expr For_val l1; do (sl2, a2) <- transl_expr For_val r2; diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 4df5f03..a88e4c3 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -110,32 +110,38 @@ Qed. Lemma tr_simple_nil: (forall le dst r sl a tmps, tr_expr le dst r sl a tmps -> - dst = For_val \/ dst = For_effects -> simple r -> sl = nil) + dst = For_val \/ dst = For_effects -> simple r = true -> sl = nil) /\(forall le rl sl al tmps, tr_exprlist le rl sl al tmps -> - simplelist rl -> sl = nil). + simplelist rl = true -> sl = nil). Proof. assert (A: forall dst a, dst = For_val \/ dst = For_effects -> final dst a = nil). intros. destruct H; subst dst; auto. - apply tr_expr_exprlist; intros; simpl in *; try contradiction; auto. + apply tr_expr_exprlist; intros; simpl in *; try discriminate; auto. rewrite H0; auto. simpl; auto. rewrite H0; auto. simpl; auto. destruct H1; congruence. - destruct H6. inv H1; try congruence. rewrite H0; auto. simpl; auto. + destruct (andb_prop _ _ H6). inv H1. rewrite H0; auto. simpl; auto. + rewrite H9 in H8; discriminate. rewrite H0; auto. simpl; auto. - destruct H7. rewrite H0; auto. rewrite H2; auto. simpl; auto. rewrite H0; auto. simpl; auto. - destruct H6. rewrite H0; auto. + destruct (andb_prop _ _ H7). rewrite H0; auto. rewrite H2; auto. simpl; auto. + rewrite H0; auto. simpl; auto. + destruct (andb_prop _ _ H13). destruct (andb_prop _ _ H14). + rewrite H2; auto. simpl; auto. + destruct (andb_prop _ _ H14). destruct (andb_prop _ _ H15). intuition congruence. + destruct (andb_prop _ _ H13). destruct (andb_prop _ _ H14). intuition congruence. + destruct (andb_prop _ _ H6). rewrite H0; auto. Qed. Lemma tr_simple_expr_nil: forall le dst r sl a tmps, tr_expr le dst r sl a tmps -> - dst = For_val \/ dst = For_effects -> simple r -> sl = nil. + dst = For_val \/ dst = For_effects -> simple r = true -> sl = nil. Proof (proj1 tr_simple_nil). Lemma tr_simple_exprlist_nil: forall le rl sl al tmps, tr_exprlist le rl sl al tmps -> - simplelist rl -> sl = nil. + simplelist rl = true -> sl = nil. Proof (proj2 tr_simple_nil). (** Evaluation of simple expressions and of their translation *) @@ -222,6 +228,16 @@ Opaque makeif. subst sl1; simpl. assert (eval_expr tge e le m (Ecast a1 ty) v). econstructor; eauto. congruence. destruct dst; auto. simpl; econstructor; eauto. +(* condition *) + exploit H2; eauto. intros [A [B C]]. subst sl1. + assert (tr_expr le For_val (if b then r2 else r3) (if b then sl2 else sl3) (if b then a2 else a3) (if b then tmp2 else tmp3)). + destruct b; auto. + exploit H5; eauto. intros [D [E F]]. + assert (eval_expr tge e le m (Econdition a1 a2 a3 ty) v). + econstructor; eauto. congruence. rewrite <- E. auto. + destruct dst; auto. simpl; econstructor; eauto. + intuition congruence. + intuition congruence. (* sizeof *) destruct dst. split; auto. split; auto. constructor. @@ -445,12 +461,20 @@ Ltac UNCHANGED := intros. rewrite <- app_ass. econstructor; eauto. (* condition *) inv H1. + (* simple *) + exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. subst sl1. rewrite app_ass. eauto. + red; auto. + intros. rewrite <- app_ass. econstructor. auto. auto. eauto. + eapply tr_expr_invariant; eauto. UNCHANGED. + eapply tr_expr_invariant; eauto. UNCHANGED. + auto. auto. auto. auto. auto. (* for val *) exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. TR. rewrite Q. rewrite app_ass. eauto. red; auto. - intros. rewrite <- app_ass. econstructor. apply S; auto. + intros. rewrite <- app_ass. econstructor. auto. apply S; auto. eapply tr_expr_invariant; eauto. UNCHANGED. eapply tr_expr_invariant; eauto. UNCHANGED. auto. auto. auto. auto. auto. auto. auto. @@ -459,7 +483,7 @@ Ltac UNCHANGED := TR. rewrite Q. rewrite app_ass. eauto. red; auto. - intros. rewrite <- app_ass. econstructor. auto. apply S; auto. + intros. rewrite <- app_ass. econstructor. auto. auto. apply S; auto. eapply tr_expr_invariant; eauto. UNCHANGED. eapply tr_expr_invariant; eauto. UNCHANGED. auto. auto. auto. auto. auto. @@ -1065,8 +1089,8 @@ Proof. rewrite (makeseq_nolabel sl2); auto. rewrite (makeseq_nolabel sl3); auto. apply makeif_nolabel; NoLabelTac. - rewrite (makeseq_nolabel sl2). auto. apply H3. apply nolabel_dest_cast; auto. - rewrite (makeseq_nolabel sl3). auto. apply H5. apply nolabel_dest_cast; auto. + rewrite (makeseq_nolabel sl2). auto. apply H4. apply nolabel_dest_cast; auto. + rewrite (makeseq_nolabel sl3). auto. apply H6. apply nolabel_dest_cast; auto. eapply tr_rvalof_nolabel; eauto. eapply tr_rvalof_nolabel; eauto. eapply tr_rvalof_nolabel; eauto. @@ -1341,10 +1365,12 @@ Proof. apply S. apply tr_val_gen. auto. intros. constructor. rewrite H5; auto. apply PTree.gss. intros. apply PTree.gso. red; intros; subst; elim H5; auto. auto. -(* condition true *) - exploit tr_top_leftcontext; eauto. clear H9. +(* condition *) + exploit tr_top_leftcontext; eauto. clear H10. intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]]. - inv P. inv H2. + inv P. inv H3. + (* simple *) + intuition congruence. (* for value *) exploit tr_simple_rvalue; eauto. intros [SL [TY EV]]. subst sl0; simpl Kseqlist. destruct b. diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v index b3efd7f..647e048 100644 --- a/cfrontend/SimplExprspec.v +++ b/cfrontend/SimplExprspec.v @@ -21,6 +21,7 @@ Require Import Values. Require Import Memory. Require Import AST. Require Import Csyntax. +Require Cstrategy. Require Import Clight. Require Import SimplExpr. @@ -117,7 +118,19 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - tr_expr le dst (C.Ecast e1 ty) (sl1 ++ final dst (Ecast a1 ty)) (Ecast a1 ty) tmp + | tr_condition_simple: forall le dst e1 e2 e3 ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 tmp, + Cstrategy.simple e2 = true -> Cstrategy.simple e3 = true -> + tr_expr le For_val e1 sl1 a1 tmp1 -> + tr_expr le For_val e2 sl2 a2 tmp2 -> + tr_expr le For_val e3 sl3 a3 tmp3 -> + list_disjoint tmp1 tmp2 -> + list_disjoint tmp1 tmp3 -> + incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp -> + tr_expr le dst (C.Econdition e1 e2 e3 ty) + (sl1 ++ final dst (Econdition a1 a2 a3 ty)) + (Econdition a1 a2 a3 ty) tmp | tr_condition_val: forall le e1 e2 e3 ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 t tmp, + Cstrategy.simple e2 = false \/ Cstrategy.simple e3 = false -> tr_expr le For_val e1 sl1 a1 tmp1 -> tr_expr le For_val e2 sl2 a2 tmp2 -> tr_expr le For_val e3 sl3 a3 tmp3 -> @@ -131,6 +144,7 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - (Ssequence (makeseq sl3) (Sset t (Ecast a3 ty))) :: nil) (Etempvar t ty) tmp | tr_condition_effects: forall le dst e1 e2 e3 ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 any tmp, + Cstrategy.simple e2 = false \/ Cstrategy.simple e3 = false -> dst <> For_val -> tr_expr le For_val e1 sl1 a1 tmp1 -> tr_expr le (cast_destination ty dst) e2 sl2 a2 tmp2 -> @@ -671,23 +685,36 @@ Opaque makeif. monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish. econstructor; split; eauto. constructor; auto. (* condition *) + simpl in H2. + destruct (Cstrategy.simple r2 && Cstrategy.simple r3) as []_eqn. + (* simple *) + monadInv H2. exploit H; eauto. intros [tmp1 [A B]]. + exploit H0; eauto. intros [tmp2 [C D]]. + exploit H1; eauto. intros [tmp3 [E F]]. + UseFinish. destruct (andb_prop _ _ Heqb). + exists (tmp1 ++ tmp2 ++ tmp3); split. + intros; eapply tr_condition_simple; eauto with gensym. + apply contained_app. eauto with gensym. + apply contained_app; eauto with gensym. + (* not simple *) monadInv H2. exploit H; eauto. intros [tmp1 [A B]]. exploit H0; eauto. intros [tmp2 [C D]]. exploit H1; eauto. intros [tmp3 [E F]]. + rewrite andb_false_iff in Heqb. destruct dst; monadInv EQ3. (* for value *) exists (x2 :: tmp1 ++ tmp2 ++ tmp3); split. - econstructor; eauto with gensym. + intros; eapply tr_condition_val; eauto with gensym. apply contained_cons. eauto with gensym. apply contained_app. eauto with gensym. apply contained_app; eauto with gensym. (* for effects *) exists (tmp1 ++ tmp2 ++ tmp3); split. - econstructor; eauto with gensym. congruence. + intros; eapply tr_condition_effects; eauto with gensym. congruence. apply contained_app; eauto with gensym. (* for test *) exists (tmp1 ++ tmp2 ++ tmp3); split. - econstructor; eauto with gensym. congruence. + intros; eapply tr_condition_effects; eauto with gensym. congruence. apply contained_app; eauto with gensym. (* sizeof *) monadInv H. UseFinish. -- cgit v1.2.3