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/Cexec.v | 115 +++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 114 insertions(+), 1 deletion(-) (limited to 'cfrontend/Cexec.v') diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 5427ac6..9391d8e 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -778,6 +778,24 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := | None => incontext (fun x => Ecast x ty) (step_expr RV r1 m) end + | RV, Eseqand r1 r2 ty => + match is_val r1 with + | Some(v1, ty1) => + do b <- bool_val v1 ty1; + if b then topred (Rred (Eparen (Eparen r2 type_bool) ty) m E0) + else topred (Rred (Eval (Vint Int.zero) ty) m E0) + | None => + incontext (fun x => Eseqand x r2 ty) (step_expr RV r1 m) + end + | RV, Eseqor r1 r2 ty => + match is_val r1 with + | Some(v1, ty1) => + do b <- bool_val v1 ty1; + if b then topred (Rred (Eval (Vint Int.one) ty) m E0) + else topred (Rred (Eparen (Eparen r2 type_bool) ty) m E0) + | None => + incontext (fun x => Eseqor x r2 ty) (step_expr RV r1 m) + end | RV, Econdition r1 r2 r3 ty => match is_val r1 with | Some(v1, ty1) => @@ -859,6 +877,17 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := incontext2 (fun x => Ecall x rargs ty) (step_expr RV r1 m) (fun x => Ecall r1 x ty) (step_exprlist rargs m) end + | RV, Ebuiltin ef tyargs rargs ty => + match is_val_list rargs with + | Some vtl => + do vargs <- sem_cast_arguments vtl tyargs; + match do_external ef w vargs m with + | None => stuck + | Some(w',t,v,m') => topred (Rred (Eval v ty) m' t) + end + | _ => + incontext (fun x => Ebuiltin ef tyargs x ty) (step_exprlist rargs m) + end | _, _ => stuck end @@ -949,6 +978,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 => @@ -971,6 +1004,12 @@ 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', exists w', + cast_arguments rargs tyargs vargs + /\ external_call ef ge vargs m t vres m' + /\ possible_trace w t w' | _ => True end. @@ -993,11 +1032,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; exists w'; auto. exists t; exists v1; exists w'; auto. exists t; exists v1; exists w'; auto. exists v; auto. + intros; exists vargs; exists t; exists vres; exists m'; exists w'; auto. Qed. Lemma callred_invert: @@ -1035,12 +1077,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. @@ -1224,6 +1269,20 @@ Proof. destruct H5. destruct k1; intuition congruence. destruct k2; intuition congruence. Qed. +Lemma incontext_list_ok: + forall ef tyargs al ty m res, + list_reducts_ok al m res -> + is_val_list al = None -> + reducts_ok RV (Ebuiltin ef tyargs al ty) m + (incontext (fun x => Ebuiltin ef tyargs x ty) res). +Proof. + unfold reducts_ok, incontext; intros. destruct H. split; intros. + exploit list_in_map_inv; eauto. intros [[C1 rd1] [P Q]]. inv P. + exploit H; eauto. intros [a'' [k'' [U [V W]]]]. + exists a''; exists k''. split. eauto. rewrite V; auto. + destruct res; simpl in H2. elim H1; auto. congruence. +Qed. + Lemma incontext2_list_ok: forall a1 a2 ty m res1 res2, reducts_ok RV a1 m res1 -> @@ -1357,6 +1416,22 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; apply topred_ok; auto. split. apply red_cast; auto. exists w; constructor. (* depth *) eapply incontext_ok; eauto. +(* seqand *) + destruct (is_val a1) as [[v ty'] | ]_eqn. rewrite (is_val_inv _ _ _ Heqo). + (* top *) + destruct (bool_val v ty') as [v'|]_eqn... destruct v'. + apply topred_ok; auto. split. eapply red_seqand_true; eauto. exists w; constructor. + apply topred_ok; auto. split. eapply red_seqand_false; eauto. exists w; constructor. + (* depth *) + eapply incontext_ok; eauto. +(* seqor *) + destruct (is_val a1) as [[v ty'] | ]_eqn. rewrite (is_val_inv _ _ _ Heqo). + (* top *) + destruct (bool_val v ty') as [v'|]_eqn... destruct v'. + apply topred_ok; auto. split. eapply red_seqor_true; eauto. exists w; constructor. + apply topred_ok; auto. split. eapply red_seqor_false; eauto. exists w; constructor. + (* depth *) + eapply incontext_ok; eauto. (* condition *) destruct (is_val a1) as [[v ty'] | ]_eqn. rewrite (is_val_inv _ _ _ Heqo). (* top *) @@ -1430,7 +1505,26 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv. congruence. (* depth *) eapply incontext2_list_ok; eauto. - eapply incontext2_list_ok; eauto. + eapply incontext2_list_ok; eauto. +(* builtin *) + destruct (is_val_list rargs) as [vtl | ]_eqn. + exploit is_val_list_all_values; eauto. intros ALLVAL. + (* top *) + destruct (sem_cast_arguments vtl tyargs) as [vargs|]_eqn... + destruct (do_external ef w vargs m) as [[[[? ?] v] m'] | ]_eqn... + exploit do_ef_external_sound; eauto. intros [EC PT]. + apply topred_ok; auto. red. split; auto. eapply red_builtin; eauto. + eapply sem_cast_arguments_sound; eauto. + exists w0; auto. + apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv. + assert (x = vargs). + exploit sem_cast_arguments_complete; eauto. intros [vtl' [A B]]. congruence. + subst x. exploit do_ef_external_complete; eauto. congruence. + apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv. + exploit sem_cast_arguments_complete; eauto. intros [vtl' [A B]]. congruence. + (* depth *) + eapply incontext_list_ok; eauto. + (* loc *) split; intros. tauto. simpl; congruence. (* paren *) @@ -1495,6 +1589,12 @@ Proof. inv H0. rewrite H; auto. (* cast *) inv H0. rewrite H; auto. +(* seqand *) + inv H0. rewrite H; auto. + inv H0. rewrite H; auto. +(* seqor *) + inv H0. rewrite H; auto. + inv H0. rewrite H; auto. (* condition *) inv H0. rewrite H; auto. (* sizeof *) @@ -1511,6 +1611,10 @@ Proof. inv H0. rewrite dec_eq_true; auto. (* paren *) inv H0. rewrite H; auto. +(* builtin *) + exploit sem_cast_arguments_complete; eauto. intros [vtl [A B]]. + exploit do_ef_external_complete; eauto. intros C. + rewrite A. rewrite B. rewrite C. auto. Qed. Lemma callred_topred: @@ -1631,6 +1735,12 @@ Proof. (* cast *) eapply reducts_incl_trans with (C' := fun x => Ecast x ty); eauto. destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. +(* seqand *) + eapply reducts_incl_trans with (C' := fun x => Eseqand x r2 ty); eauto. + destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. +(* seqor *) + eapply reducts_incl_trans with (C' := fun x => Eseqor x r2 ty); eauto. + destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. (* condition *) eapply reducts_incl_trans with (C' := fun x => Econdition x r2 r3 ty); eauto. destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. @@ -1658,6 +1768,9 @@ Proof. eapply reducts_incl_trans with (C' := fun x => Ecall e1 x ty). apply step_exprlist_context. auto. destruct (is_val e1) as [[v1 ty1]|]_eqn; eauto. destruct (is_val_list (C a)) as [vl|]_eqn; eauto. +(* builtin *) + eapply reducts_incl_trans with (C' := fun x => Ebuiltin ef tyargs x ty). apply step_exprlist_context. auto. + destruct (is_val_list (C a)) as [vl|]_eqn; eauto. (* comma *) eapply reducts_incl_trans with (C' := fun x => Ecomma x e2 ty); eauto. destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. -- cgit v1.2.3