From f7693b3d897b90fd3bc2533be002dc0bdcd9f6c2 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 6 Oct 2012 15:46:47 +0000 Subject: Merge of branch seq-and-or. See Changelog for details. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2059 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cstrategy.v | 203 +++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 158 insertions(+), 45 deletions(-) (limited to 'cfrontend/Cstrategy.v') diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index 13cffb58..5be17edc 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -56,7 +56,9 @@ Fixpoint simple (a: expr) : bool := | Eunop _ r1 _ => simple r1 | Ebinop _ r1 r2 _ => simple r1 && simple r2 | Ecast r1 _ => simple r1 - | Econdition r1 r2 r3 _ => simple r1 && simple r2 && simple r3 + | Eseqand _ _ _ => false + | Eseqor _ _ _ => false + | Econdition _ _ _ _ => false | Esizeof _ _ => true | Ealignof _ _ => true | Eassign _ _ _ => false @@ -64,6 +66,7 @@ Fixpoint simple (a: expr) : bool := | Epostincr _ _ _ => false | Ecomma _ _ _ => false | Ecall _ _ _ => false + | Ebuiltin _ _ _ _ => false | Eparen _ _ => false end. @@ -126,13 +129,6 @@ 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))) | esr_alignof: forall ty1 ty, @@ -175,6 +171,10 @@ Inductive leftcontext: kind -> kind -> (expr -> expr) -> Prop := 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) + | lctx_seqand: forall k C r2 ty, + leftcontext k RV C -> leftcontext k RV (fun x => Eseqand (C x) r2 ty) + | lctx_seqor: forall k C r2 ty, + leftcontext k RV C -> leftcontext k RV (fun x => Eseqor (C x) r2 ty) | lctx_condition: forall k C r2 r3 ty, leftcontext k RV C -> leftcontext k RV (fun x => Econdition (C x) r2 r3 ty) | lctx_assign_left: forall k C e2 ty, @@ -194,6 +194,9 @@ Inductive leftcontext: kind -> kind -> (expr -> expr) -> Prop := | lctx_call_right: forall k C e1 ty, simple e1 = true -> leftcontextlist k C -> leftcontext k RV (fun x => Ecall e1 (C x) ty) + | lctx_builtin: forall k C ef tyargs ty, + leftcontextlist k C -> + leftcontext k RV (fun x => Ebuiltin ef tyargs (C x) ty) | lctx_comma: forall k C e2 ty, leftcontext k RV C -> leftcontext k RV (fun x => Ecomma (C x) e2 ty) | lctx_paren: forall k C ty, @@ -240,8 +243,33 @@ Inductive estep: state -> trace -> state -> Prop := estep (ExprState f (C (Evalof l ty)) k e m) t (ExprState f (C (Eval v ty)) k e m) + | step_seqand_true: forall f C r1 r2 ty k e m v, + leftcontext RV RV C -> + eval_simple_rvalue e m r1 v -> + bool_val v (typeof r1) = Some true -> + estep (ExprState f (C (Eseqand r1 r2 ty)) k e m) + E0 (ExprState f (C (Eparen (Eparen r2 type_bool) ty)) k e m) + | step_seqand_false: forall f C r1 r2 ty k e m v, + leftcontext RV RV C -> + eval_simple_rvalue e m r1 v -> + bool_val v (typeof r1) = Some false -> + estep (ExprState f (C (Eseqand r1 r2 ty)) k e m) + E0 (ExprState f (C (Eval (Vint Int.zero) ty)) k e m) + + | step_seqor_true: forall f C r1 r2 ty k e m v, + leftcontext RV RV C -> + eval_simple_rvalue e m r1 v -> + bool_val v (typeof r1) = Some true -> + estep (ExprState f (C (Eseqor r1 r2 ty)) k e m) + E0 (ExprState f (C (Eval (Vint Int.one) ty)) k e m) + | step_seqor_false: forall f C r1 r2 ty k e m v, + leftcontext RV RV C -> + eval_simple_rvalue e m r1 v -> + bool_val v (typeof r1) = Some false -> + estep (ExprState f (C (Eseqor r1 r2 ty)) k e m) + E0 (ExprState f (C (Eparen (Eparen r2 type_bool) 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 -> @@ -338,7 +366,14 @@ Inductive estep: state -> trace -> state -> Prop := Genv.find_funct ge vf = Some fd -> type_of_fundef fd = Tfunction targs tres -> estep (ExprState f (C (Ecall rf rargs ty)) k e m) - E0 (Callstate fd vargs (Kcall f e C ty k) m). + E0 (Callstate fd vargs (Kcall f e C ty k) m) + + | step_builtin: forall f C ef tyargs rargs ty k e m vargs t vres m', + leftcontext RV RV C -> + eval_simple_list e m rargs tyargs vargs -> + external_call ef ge vargs m t vres m' -> + estep (ExprState f (C (Ebuiltin ef tyargs rargs ty)) k e m) + t (ExprState f (C (Eval vres ty)) k e m'). Definition step (S: state) (t: trace) (S': state) : Prop := estep S t S' \/ sstep ge S t S'. @@ -503,6 +538,10 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := exists v, sem_binary_operation op v1 ty1 v2 ty2 m = Some v | Ecast (Eval v1 ty1) ty => exists v, sem_cast v1 ty1 ty = Some v + | Eseqand (Eval v1 ty1) r2 ty => + exists b, bool_val v1 ty1 = Some b + | Eseqor (Eval v1 ty1) r2 ty => + exists b, bool_val v1 ty1 = Some b | Econdition (Eval v1 ty1) r1 r2 ty => exists b, bool_val v1 ty1 = Some b | Eassign (Eloc b ofs ty1) (Eval v2 ty2) ty => @@ -527,6 +566,11 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := /\ Genv.find_funct ge vf = Some fd /\ cast_arguments rargs tyargs vl /\ type_of_fundef fd = Tfunction tyargs tyres + | Ebuiltin ef tyargs rargs ty => + exprlist_all_values rargs -> + exists vargs, exists t, exists vres, exists m', + cast_arguments rargs tyargs vargs + /\ external_call ef ge vargs m t vres m' | _ => True end. @@ -549,11 +593,14 @@ Proof. exists v; auto. exists v; auto. exists v; auto. + exists true; auto. exists false; auto. + exists true; auto. exists false; auto. exists b; auto. exists v; exists m'; exists t; auto. exists t; exists v1; auto. exists t; exists v1; auto. exists v; auto. + intros. exists vargs; exists t; exists vres; exists m'; auto. Qed. Lemma callred_invert: @@ -591,12 +638,15 @@ Proof. destruct (C a); auto; contradiction. destruct (C a); auto; contradiction. destruct (C a); auto; contradiction. + destruct (C a); auto; contradiction. + destruct (C a); auto; contradiction. destruct e1; auto; destruct (C a); auto; contradiction. destruct (C a); auto; contradiction. destruct e1; auto; destruct (C a); auto; contradiction. destruct (C a); auto; contradiction. destruct (C a); auto; contradiction. destruct e1; auto. intros. elim (H0 a m); auto. + intros. elim (H0 a m); auto. destruct (C a); auto; contradiction. destruct (C a); auto; contradiction. red; intros. destruct (C a); auto. @@ -681,12 +731,6 @@ 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. (* alignof *) @@ -801,23 +845,6 @@ 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. (* alignof *) @@ -898,9 +925,12 @@ Proof. Qed. Inductive contextlist' : (exprlist -> expr) -> Prop := - | contextlist'_intro: forall r1 rl0 ty C, + | contextlist'_call: forall r1 rl0 ty C, + context RV RV C -> + contextlist' (fun rl => C (Ecall r1 (exprlist_app rl0 rl) ty)) + | contextlist'_builtin: forall ef tyargs rl0 ty C, context RV RV C -> - contextlist' (fun rl => C (Ecall r1 (exprlist_app rl0 rl) ty)). + contextlist' (fun rl => C (Ebuiltin ef tyargs (exprlist_app rl0 rl) ty)). Lemma exprlist_app_context: forall rl1 rl2, @@ -921,6 +951,10 @@ Proof. assert (context RV RV C'). constructor. apply exprlist_app_context. change (context RV RV (fun x => C0 (C' x))). eapply context_compose; eauto. + set (C' := fun x => Ebuiltin ef tyargs (exprlist_app rl0 (Econs x rl)) ty). + assert (context RV RV C'). constructor. apply exprlist_app_context. + change (context RV RV (fun x => C0 (C' x))). + eapply context_compose; eauto. Qed. Lemma contextlist'_tail: @@ -933,6 +967,10 @@ Proof. with (fun x => C0 (Ecall r0 (exprlist_app (exprlist_app rl0 (Econs r1 Enil)) x) ty)). constructor. auto. apply extensionality; intros. f_equal. f_equal. apply exprlist_app_assoc. + replace (fun x => C0 (Ebuiltin ef tyargs (exprlist_app rl0 (Econs r1 x)) ty)) + with (fun x => C0 (Ebuiltin ef tyargs (exprlist_app (exprlist_app rl0 (Econs r1 Enil)) x) ty)). + constructor. auto. + apply extensionality; intros. f_equal. f_equal. apply exprlist_app_assoc. Qed. Hint Resolve contextlist'_head contextlist'_tail. @@ -992,12 +1030,15 @@ Variable m: mem. Definition simple_side_effect (r: expr) : Prop := match r with | Evalof l _ => simple l = true /\ type_is_volatile (typeof l) = true - | Econdition r1 r2 r3 _ => simple r1 = true /\ (simple r2 = false \/ simple r3 = false) + | Eseqand r1 r2 _ => simple r1 = true + | Eseqor r1 r2 _ => simple r1 = true + | Econdition r1 r2 r3 _ => simple r1 = true | 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 + | Ebuiltin ef tyargs rl _ => simplelist rl = true | Eparen r1 _ => simple r1 = true | _ => False end. @@ -1046,10 +1087,12 @@ Ltac Base := Rec H0 RV C (fun x => Ebinop op r1 x ty). (* cast *) Kind. Rec H RV C (fun x => Ecast x ty). +(* seqand *) + Kind. Rec H RV C (fun x => Eseqand x r2 ty). Base. +(* seqor *) + Kind. Rec H RV C (fun x => Eseqor x r2 ty). Base. (* condition *) - 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. + Kind. Rec H RV C (fun x => Econdition x r2 r3 ty). 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 *) @@ -1061,9 +1104,15 @@ Ltac Base := (* call *) Kind. Rec H RV C (fun x => Ecall x rargs ty). destruct (H0 (fun x => C (Ecall r1 x ty))) as [A | [C' [a' [D [A B]]]]]. - eapply contextlist'_intro with (C := C) (rl0 := Enil). auto. auto. + eapply contextlist'_call with (C := C) (rl0 := Enil). auto. auto. Base. right; exists (fun x => Ecall r1 (C' x) ty); exists a'. rewrite D; simpl; auto. +(* builtin *) + Kind. + destruct (H (fun x => C (Ebuiltin ef tyargs x ty))) as [A | [C' [a' [D [A B]]]]]. + eapply contextlist'_builtin with (C := C) (rl0 := Enil). auto. auto. + Base. + right; exists (fun x => Ebuiltin ef tyargs (C' x) ty); exists a'. rewrite D; simpl; auto. (* rparen *) Kind. Rec H RV C (fun x => (Eparen x ty)). Base. (* cons *) @@ -1102,6 +1151,22 @@ Proof. eapply plus_right. eapply eval_simple_lvalue_steps with (C := fun x => C(Evalof x (typeof l))); eauto. left. apply step_rred; eauto. econstructor; eauto. auto. +(* seqand true *) + eapply plus_right. + eapply eval_simple_rvalue_steps with (C := fun x => C(Eseqand x r2 ty)); eauto. + left. apply step_rred; eauto. apply red_seqand_true; auto. traceEq. +(* seqand false *) + eapply plus_right. + eapply eval_simple_rvalue_steps with (C := fun x => C(Eseqand x r2 ty)); eauto. + left. apply step_rred; eauto. apply red_seqand_false; auto. traceEq. +(* seqor true *) + eapply plus_right. + eapply eval_simple_rvalue_steps with (C := fun x => C(Eseqor x r2 ty)); eauto. + left. apply step_rred; eauto. apply red_seqor_true; auto. traceEq. +(* seqor false *) + eapply plus_right. + eapply eval_simple_rvalue_steps with (C := fun x => C(Eseqor x r2 ty)); eauto. + left. apply step_rred; eauto. apply red_seqor_false; auto. traceEq. (* condition *) eapply plus_right. eapply eval_simple_rvalue_steps with (C := fun x => C(Econdition x r2 r3 ty)); eauto. @@ -1196,9 +1261,16 @@ Proof. eapply eval_simple_rvalue_steps with (C := fun x => C(Ecall x rargs ty)); eauto. eapply plus_right. eapply eval_simple_list_steps with (C := fun x => C(Ecall (Eval vf (typeof rf)) x ty)); eauto. - eapply contextlist'_intro with (rl0 := Enil); auto. + eapply contextlist'_call with (rl0 := Enil); auto. left; apply Csem.step_call; eauto. econstructor; eauto. traceEq. auto. +(* builtin *) + exploit eval_simple_list_implies; eauto. intros [vl' [A B]]. + eapply plus_right. + eapply eval_simple_list_steps with (C := fun x => C(Ebuiltin ef tyargs x ty)); eauto. + eapply contextlist'_builtin with (rl0 := Enil); auto. + left; apply Csem.step_rred; eauto. econstructor; eauto. + traceEq. Qed. Lemma can_estep: @@ -1219,8 +1291,21 @@ Proof. intros [b1 [ofs [E1 S1]]]. exploit safe_inv. eexact S1. eauto. simpl. intros [A [t [v B]]]. econstructor; econstructor; eapply step_rvalof_volatile; eauto. congruence. +(* seqand *) + exploit (simple_can_eval_rval f k e m b1 (fun x => C(Eseqand x b2 ty))); eauto. + intros [v1 [E1 S1]]. + exploit safe_inv. eexact S1. eauto. simpl. intros [b BV]. + destruct b. + econstructor; econstructor; eapply step_seqand_true; eauto. + econstructor; econstructor; eapply step_seqand_false; eauto. +(* seqor *) + exploit (simple_can_eval_rval f k e m b1 (fun x => C(Eseqor x b2 ty))); eauto. + intros [v1 [E1 S1]]. + exploit safe_inv. eexact S1. eauto. simpl. intros [b BV]. + destruct b. + econstructor; econstructor; eapply step_seqor_true; eauto. + econstructor; econstructor; eapply step_seqor_false; eauto. (* 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]. @@ -1276,7 +1361,7 @@ Proof. exploit (simple_can_eval_rval f k e m b (fun x => C(Ecall x rargs ty))); eauto. intros [vf [E1 S1]]. pose (C' := fun x => C(Ecall (Eval vf (typeof b)) x ty)). - assert (contextlist' C'). unfold C'; eapply contextlist'_intro with (rl0 := Enil); auto. + assert (contextlist' C'). unfold C'; eapply contextlist'_call with (rl0 := Enil); auto. exploit (simple_list_can_eval f k e m rargs C'); eauto. intros [vl E2]. exploit safe_inv. 2: eapply leftcontext_context; eexact R. @@ -1285,6 +1370,18 @@ Proof. simpl. intros X. exploit X. eapply rval_list_all_values. intros [tyargs [tyres [fd [vargs [P [Q [U V]]]]]]]. econstructor; econstructor; eapply step_call; eauto. eapply can_eval_simple_list; eauto. +(* builtin *) + pose (C' := fun x => C(Ebuiltin ef tyargs x ty)). + assert (contextlist' C'). unfold C'; eapply contextlist'_builtin with (rl0 := Enil); auto. + exploit (simple_list_can_eval f k e m rargs C'); eauto. + intros [vl E]. + exploit safe_inv. 2: eapply leftcontext_context; eexact R. + eapply safe_steps. eexact H. + apply (eval_simple_list_steps f k e m rargs vl E C'); auto. + simpl. intros X. exploit X. eapply rval_list_all_values. + intros [vargs [t [vres [m' [U V]]]]]. + econstructor; econstructor; eapply step_builtin; eauto. + eapply can_eval_simple_list; eauto. (* paren *) exploit (simple_can_eval_rval f k e m b (fun x => C(Eparen x ty))); eauto. intros [v1 [E1 S1]]. @@ -1448,6 +1545,11 @@ Proof. rewrite Heqo; rewrite Heqo0; auto. econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto. rewrite Heqo; auto. + (* builtin *) + exploit external_call_trace_length; eauto. destruct t1; simpl; intros. + exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. + econstructor; econstructor. left; eapply step_builtin; eauto. + omegaContradiction. (* external calls *) inv H1. exploit external_call_trace_length; eauto. destruct t1; simpl; intros. @@ -1474,6 +1576,9 @@ Proof. tauto. (* postincr stuck *) exploit deref_loc_trace; eauto. destruct t; auto. destruct t; tauto. + (* builtins *) + exploit external_call_trace_length; eauto. + destruct t; simpl; auto. destruct t; simpl; auto. intros; omegaContradiction. (* external calls *) exploit external_call_trace_length; eauto. destruct t; simpl; auto. destruct t; simpl; auto. intros; omegaContradiction. @@ -1502,6 +1607,8 @@ Qed. (** * A big-step semantics implementing the reduction strategy. *) +(** TODO: update with seqand / seqor *) + Section BIGSTEP. Variable ge: genv. @@ -2488,6 +2595,8 @@ Fixpoint esize (a: expr) : nat := | Eunop _ r1 _ => S(esize r1) | Ebinop _ r1 r2 _ => S(esize r1 + esize r2)%nat | Ecast r1 _ => S(esize r1) + | Eseqand r1 r2 _ => S(esize r1) + | Eseqor r1 r2 _ => S(esize r1) | Econdition r1 _ _ _ => S(esize r1) | Esizeof _ _ => 1%nat | Ealignof _ _ => 1%nat @@ -2496,6 +2605,7 @@ Fixpoint esize (a: expr) : nat := | Epostincr _ l1 _ => S(esize l1) | Ecomma r1 r2 _ => S(esize r1 + esize r2)%nat | Ecall r1 rl2 _ => S(esize r1 + esizelist rl2)%nat + | Ebuiltin ef tyargs rl _ => S(esizelist rl) | Eparen r1 _ => S(esize r1) end @@ -2518,8 +2628,11 @@ with leftcontextlist_size: (esize e1 < esize e2)%nat -> (esizelist (C e1) < esizelist (C e2))%nat. Proof. - induction 1; intros; simpl; auto with arith. exploit leftcontextlist_size; eauto. auto with arith. - induction 1; intros; simpl; auto with arith. exploit leftcontext_size; eauto. auto with arith. + induction 1; intros; simpl; auto with arith. + exploit leftcontextlist_size; eauto. auto with arith. + exploit leftcontextlist_size; eauto. auto with arith. + induction 1; intros; simpl; auto with arith. + exploit leftcontext_size; eauto. auto with arith. Qed. Lemma evalinf_funcall_steps: -- cgit