From 25b9b003178002360d666919f2e49e7f5f4a36e2 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Feb 2012 19:14:14 +0000 Subject: Merge of the "volatile" branch: - native treatment of volatile accesses in CompCert C's semantics - translation of volatile accesses to built-ins in SimplExpr - native treatment of struct assignment and passing struct parameter by value - only passing struct result by value remains emulated - in cparser, remove emulations that are no longer used - added C99's type _Bool and used it to express || and && more efficiently. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1814 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/SimplExprspec.v | 103 ++++++++++++++++++++++++++++++++++------------ 1 file changed, 76 insertions(+), 27 deletions(-) (limited to 'cfrontend/SimplExprspec.v') diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v index 1224ea9d..b3efd7f7 100644 --- a/cfrontend/SimplExprspec.v +++ b/cfrontend/SimplExprspec.v @@ -48,6 +48,14 @@ Definition final (dst: destination) (a: expr) : list statement := | For_test tyl s1 s2 => makeif (fold_left Ecast tyl a) s1 s2 :: nil end. +Inductive tr_rvalof: type -> expr -> list statement -> expr -> list ident -> Prop := + | tr_rvalof_nonvol: forall ty a tmp, + type_is_volatile ty = false -> + tr_rvalof ty a nil a tmp + | tr_rvalof_vol: forall ty a t tmp, + type_is_volatile ty = true -> In t tmp -> + tr_rvalof ty a (Svolread t a :: nil) (Etempvar t ty) tmp. + Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr -> list ident -> Prop := | tr_var: forall le dst id ty tmp, tr_expr le dst (C.Evar id ty) @@ -80,11 +88,13 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - tr_expr le dst (C.Esizeof ty' ty) (final dst (Esizeof ty' ty)) (Esizeof ty' ty) tmp - | tr_valof: forall le dst e1 ty tmp sl1 a1, - tr_expr le For_val e1 sl1 a1 tmp -> + | tr_valof: forall le dst e1 ty tmp sl1 a1 tmp1 sl2 a2 tmp2, + tr_expr le For_val e1 sl1 a1 tmp1 -> + tr_rvalof (C.typeof e1) a1 sl2 a2 tmp2 -> + list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp -> tr_expr le dst (C.Evalof e1 ty) - (sl1 ++ final dst a1) - a1 tmp + (sl1 ++ sl2 ++ final dst a2) + a2 tmp | tr_addrof: forall le dst e1 ty tmp sl1 a1, tr_expr le For_val e1 sl1 a1 tmp -> tr_expr le dst (C.Eaddrof e1 ty) @@ -153,38 +163,45 @@ Inductive tr_expr: temp_env -> destination -> C.expr -> list statement -> expr - Sassign a1 (Etempvar t ty2) :: final dst (Ecast (Etempvar t ty2) ty1)) (Ecast (Etempvar t ty2) ty1) tmp - | tr_assignop_effects: forall le op e1 e2 tyres ty sl1 a1 tmp1 sl2 a2 tmp2 any tmp, + | tr_assignop_effects: forall le op e1 e2 tyres ty ty1 sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 any tmp, tr_expr le For_val e1 sl1 a1 tmp1 -> tr_expr le For_val e2 sl2 a2 tmp2 -> - list_disjoint tmp1 tmp2 -> - incl tmp1 tmp -> incl tmp2 tmp -> + ty1 = C.typeof e1 -> + tr_rvalof ty1 a1 sl3 a3 tmp3 -> + list_disjoint tmp1 tmp2 -> list_disjoint tmp1 tmp3 -> list_disjoint tmp2 tmp3 -> + incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp -> tr_expr le For_effects (C.Eassignop op e1 e2 tyres ty) - (sl1 ++ sl2 ++ Sassign a1 (Ebinop op a1 a2 tyres) :: nil) + (sl1 ++ sl2 ++ sl3 ++ Sassign a1 (Ebinop op a3 a2 tyres) :: nil) any tmp - | tr_assignop_val: forall le dst op e1 e2 tyres ty sl1 a1 tmp1 sl2 a2 tmp2 t tmp ty1, + | tr_assignop_val: forall le dst op e1 e2 tyres ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 t tmp ty1, tr_expr le For_val e1 sl1 a1 tmp1 -> tr_expr le For_val e2 sl2 a2 tmp2 -> - list_disjoint tmp1 tmp2 -> - incl tmp1 tmp -> incl tmp2 tmp -> - In t tmp -> ~In t tmp1 -> ~In t tmp2 -> + tr_rvalof ty1 a1 sl3 a3 tmp3 -> + list_disjoint tmp1 tmp2 -> list_disjoint tmp1 tmp3 -> list_disjoint tmp2 tmp3 -> + incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp -> + In t tmp -> ~In t tmp1 -> ~In t tmp2 -> ~In t tmp3 -> ty1 = C.typeof e1 -> tr_expr le dst (C.Eassignop op e1 e2 tyres ty) - (sl1 ++ sl2 ++ - Sset t (Ebinop op a1 a2 tyres) :: + (sl1 ++ sl2 ++ sl3 ++ + Sset t (Ebinop op a3 a2 tyres) :: Sassign a1 (Etempvar t tyres) :: final dst (Ecast (Etempvar t tyres) ty1)) (Ecast (Etempvar t tyres) ty1) tmp - | tr_postincr_effects: forall le id e1 ty sl1 a1 tmp any, - tr_expr le For_val e1 sl1 a1 tmp -> + | tr_postincr_effects: forall le id e1 ty ty1 sl1 a1 tmp1 sl2 a2 tmp2 any tmp, + tr_expr le For_val e1 sl1 a1 tmp1 -> + tr_rvalof ty1 a1 sl2 a2 tmp2 -> + ty1 = C.typeof e1 -> + incl tmp1 tmp -> incl tmp2 tmp -> + list_disjoint tmp1 tmp2 -> tr_expr le For_effects (C.Epostincr id e1 ty) - (sl1 ++ Sassign a1 (transl_incrdecr id a1 (C.typeof e1)) :: nil) + (sl1 ++ sl2 ++ Sassign a1 (transl_incrdecr id a2 ty1) :: nil) any tmp | tr_postincr_val: forall le dst id e1 ty sl1 a1 tmp1 t ty1 tmp, tr_expr le For_val e1 sl1 a1 tmp1 -> incl tmp1 tmp -> In t tmp -> ~In t tmp1 -> ty1 = C.typeof e1 -> tr_expr le dst (C.Epostincr id e1 ty) - (sl1 ++ Sset t a1 :: + (sl1 ++ make_set t a1 :: Sassign a1 (transl_incrdecr id (Etempvar t ty1) ty1) :: final dst (Etempvar t ty1)) (Etempvar t ty1) tmp @@ -253,6 +270,13 @@ Proof. induction 1; intros; econstructor; eauto. Qed. +Lemma tr_rvalof_monotone: + forall ty a sl b tmps, tr_rvalof ty a sl b tmps -> + forall tmps', incl tmps tmps' -> tr_rvalof ty a sl b tmps'. +Proof. + induction 1; intros; econstructor; unfold incl in *; eauto. +Qed. + Lemma tr_expr_monotone: forall le dst r sl a tmps, tr_expr le dst r sl a tmps -> forall tmps', incl tmps tmps' -> tr_expr le dst r sl a tmps' @@ -260,6 +284,7 @@ with tr_exprlist_monotone: forall le rl sl al tmps, tr_exprlist le rl sl al tmps -> forall tmps', incl tmps tmps' -> tr_exprlist le rl sl al tmps'. Proof. + specialize tr_rvalof_monotone. intros RVALOF. induction 1; intros; econstructor; unfold incl in *; eauto. induction 1; intros; econstructor; unfold incl in *; eauto. Qed. @@ -572,6 +597,25 @@ Ltac UseFinish := repeat rewrite app_ass end. +Lemma transl_valof_meets_spec: + forall ty a g sl b g' I, + transl_valof ty a g = Res (sl, b) g' I -> + exists tmps, tr_rvalof ty a sl b tmps /\ contained tmps g g'. +Proof. + unfold transl_valof; intros. + destruct (type_is_volatile ty) as []_eqn; monadInv H. + exists (x :: nil); split; eauto with gensym. econstructor; eauto with coqlib. + exists (@nil ident); split; eauto with gensym. constructor; auto. +(* + destruct (access_mode ty) as []_eqn. + destruct (Csem.type_is_volatile ty) as []_eqn; monadInv H. + exists (x :: nil); split; eauto with gensym. econstructor; eauto with coqlib. + exists (@nil ident); split; eauto with gensym. constructor; auto. + monadInv H. exists (@nil ident); split; eauto with gensym. constructor; auto. + monadInv H. exists (@nil ident); split; eauto with gensym. constructor; auto. +*) +Qed. + Scheme expr_ind2 := Induction for C.expr Sort Prop with exprlist_ind2 := Induction for C.exprlist Sort Prop. Combined Scheme expr_exprlist_ind from expr_ind2, exprlist_ind2. @@ -603,9 +647,11 @@ Opaque makeif. monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish. econstructor; split; eauto. constructor; auto. (* valof *) - monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish. - econstructor; split. - econstructor; eauto. eauto with gensym. + monadInv H0. exploit H; eauto. intros [tmp1 [A B]]. + exploit transl_valof_meets_spec; eauto. intros [tmp2 [C D]]. UseFinish. + exists (tmp1 ++ tmp2); split. + econstructor; eauto with gensym. + eauto with gensym. (* deref *) monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish. econstructor; split; eauto. constructor; auto. @@ -668,18 +714,19 @@ Opaque makeif. (* assignop *) monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. exploit H0; eauto. intros [tmp2 [C D]]. - destruct dst; monadInv EQ2. + exploit transl_valof_meets_spec; eauto. intros [tmp3 [E F]]. + destruct dst; monadInv EQ3. (* for value *) - exists (x1 :: tmp1 ++ tmp2); split. + exists (x2 :: tmp1 ++ tmp2 ++ tmp3); split. intros. eapply tr_assignop_val with (dst := For_val); eauto with gensym. apply contained_cons. eauto with gensym. apply contained_app; eauto with gensym. (* for effects *) - exists (tmp1 ++ tmp2); split. + exists (tmp1 ++ tmp2 ++ tmp3); split. econstructor; eauto with gensym. apply contained_app; eauto with gensym. (* for test *) - exists (x1 :: tmp1 ++ tmp2); split. + exists (x2 :: tmp1 ++ tmp2 ++ tmp3); split. repeat rewrite app_ass. simpl. intros. eapply tr_assignop_val with (dst := For_test tyl s1 s2); eauto with gensym. apply contained_cons. eauto with gensym. @@ -692,8 +739,10 @@ Opaque makeif. econstructor; eauto with gensym. apply contained_cons; eauto with gensym. (* for effects *) - exists tmp1; split. - econstructor; eauto with gensym. auto. + exploit transl_valof_meets_spec; eauto. intros [tmp2 [C D]]. + exists (tmp1 ++ tmp2); split. + econstructor; eauto with gensym. + eauto with gensym. (* for test *) repeat rewrite app_ass; simpl. exists (x0 :: tmp1); split. -- cgit