diff options
Diffstat (limited to 'cfrontend/SimplExprspec.v')
| -rw-r--r-- | cfrontend/SimplExprspec.v | 161 |
1 files changed, 102 insertions, 59 deletions
diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v index 98425311..b689bdeb 100644 --- a/cfrontend/SimplExprspec.v +++ b/cfrontend/SimplExprspec.v @@ -18,6 +18,8 @@ Require Import Ctypes Cop Csyntax Clight SimplExpr. Section SPEC. +Variable ce: composite_env. + Local Open Scope gensym_monad_scope. (** * Relational specification of the translation. *) @@ -40,13 +42,28 @@ Definition final (dst: destination) (a: expr) : list statement := | For_set sd => do_set sd a end. +Definition tr_is_bitfield_access (l: expr) (bf: bitfield) : Prop := + match l with + | Efield r f _ => + exists co ofs, + match typeof r with + | Tstruct id _ => + ce!id = Some co /\ field_offset ce f (co_members co) = OK (ofs, bf) + | Tunion id _ => + ce!id = Some co /\ union_field_offset ce f (co_members co) = OK (ofs, bf) + | _ => False + end + | _ => bf = Full + 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, + | tr_rvalof_vol: forall ty a t bf tmp, type_is_volatile ty = true -> In t tmp -> - tr_rvalof ty a (make_set t a :: nil) (Etempvar t ty) tmp. + tr_is_bitfield_access a bf -> + tr_rvalof ty a (make_set bf t a :: nil) (Etempvar t ty) tmp. Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement -> expr -> list ident -> Prop := | tr_var: forall le dst id ty tmp, @@ -200,15 +217,16 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement -> tr_expr le (For_set sd) (Csyntax.Econdition e1 e2 e3 ty) (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil) any tmp - | tr_assign_effects: forall le e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 any tmp, + | tr_assign_effects: forall le e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 bf 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 -> + tr_is_bitfield_access a1 bf -> tr_expr le For_effects (Csyntax.Eassign e1 e2 ty) - (sl1 ++ sl2 ++ make_assign a1 a2 :: nil) + (sl1 ++ sl2 ++ make_assign bf a1 a2 :: nil) any tmp - | tr_assign_val: forall le dst e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 t tmp ty1 ty2, + | tr_assign_val: forall le dst e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 t tmp ty1 ty2 bf, tr_expr le For_val e1 sl1 a1 tmp1 -> tr_expr le For_val e2 sl2 a2 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp -> @@ -216,23 +234,25 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement -> In t tmp -> ~In t tmp1 -> ~In t tmp2 -> ty1 = Csyntax.typeof e1 -> ty2 = Csyntax.typeof e2 -> + tr_is_bitfield_access a1 bf -> tr_expr le dst (Csyntax.Eassign e1 e2 ty) (sl1 ++ sl2 ++ Sset t (Ecast a2 ty1) :: - make_assign a1 (Etempvar t ty1) :: - final dst (Etempvar t ty1)) - (Etempvar t ty1) tmp - | tr_assignop_effects: forall le op e1 e2 tyres ty ty1 sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 any tmp, + make_assign bf a1 (Etempvar t ty1) :: + final dst (make_assign_value bf (Etempvar t ty1))) + (make_assign_value bf (Etempvar t ty1)) tmp + | tr_assignop_effects: forall le op e1 e2 tyres ty ty1 sl1 a1 tmp1 sl2 a2 tmp2 bf sl3 a3 tmp3 any tmp, tr_expr le For_val e1 sl1 a1 tmp1 -> tr_expr le For_val e2 sl2 a2 tmp2 -> ty1 = Csyntax.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_is_bitfield_access a1 bf -> tr_expr le For_effects (Csyntax.Eassignop op e1 e2 tyres ty) - (sl1 ++ sl2 ++ sl3 ++ make_assign a1 (Ebinop op a3 a2 tyres) :: nil) + (sl1 ++ sl2 ++ sl3 ++ make_assign bf 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 sl3 a3 tmp3 t tmp ty1, + | tr_assignop_val: forall le dst op e1 e2 tyres ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 t bf tmp ty1, tr_expr le For_val e1 sl1 a1 tmp1 -> tr_expr le For_val e2 sl2 a2 tmp2 -> tr_rvalof ty1 a1 sl3 a3 tmp3 -> @@ -240,28 +260,31 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement -> incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp -> In t tmp -> ~In t tmp1 -> ~In t tmp2 -> ~In t tmp3 -> ty1 = Csyntax.typeof e1 -> + tr_is_bitfield_access a1 bf -> tr_expr le dst (Csyntax.Eassignop op e1 e2 tyres ty) (sl1 ++ sl2 ++ sl3 ++ Sset t (Ecast (Ebinop op a3 a2 tyres) ty1) :: - make_assign a1 (Etempvar t ty1) :: - final dst (Etempvar t ty1)) - (Etempvar t ty1) tmp - | tr_postincr_effects: forall le id e1 ty ty1 sl1 a1 tmp1 sl2 a2 tmp2 any tmp, + make_assign bf a1 (Etempvar t ty1) :: + final dst (make_assign_value bf (Etempvar t ty1))) + (make_assign_value bf (Etempvar t ty1)) tmp + | tr_postincr_effects: forall le id e1 ty ty1 sl1 a1 tmp1 sl2 a2 tmp2 bf any tmp, tr_expr le For_val e1 sl1 a1 tmp1 -> tr_rvalof ty1 a1 sl2 a2 tmp2 -> ty1 = Csyntax.typeof e1 -> incl tmp1 tmp -> incl tmp2 tmp -> list_disjoint tmp1 tmp2 -> + tr_is_bitfield_access a1 bf -> tr_expr le For_effects (Csyntax.Epostincr id e1 ty) - (sl1 ++ sl2 ++ make_assign a1 (transl_incrdecr id a2 ty1) :: nil) + (sl1 ++ sl2 ++ make_assign bf 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_postincr_val: forall le dst id e1 ty sl1 a1 tmp1 bf t ty1 tmp, tr_expr le For_val e1 sl1 a1 tmp1 -> incl tmp1 tmp -> In t tmp -> ~In t tmp1 -> ty1 = Csyntax.typeof e1 -> + tr_is_bitfield_access a1 bf -> tr_expr le dst (Csyntax.Epostincr id e1 ty) - (sl1 ++ make_set t a1 :: - make_assign a1 (transl_incrdecr id (Etempvar t ty1) ty1) :: + (sl1 ++ make_set bf t a1 :: + make_assign bf a1 (transl_incrdecr id (Etempvar t ty1) ty1) :: final dst (Etempvar t ty1)) (Etempvar t ty1) tmp | tr_comma: forall le dst e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 tmp, @@ -746,14 +769,31 @@ Proof. intros. apply tr_expr_monotone with tmps; auto. apply add_dest_incl. Qed. +Lemma is_bitfield_access_meets_spec: forall l g bf g' I, + is_bitfield_access ce l g = Res bf g' I -> + tr_is_bitfield_access l bf. +Proof. + unfold is_bitfield_access; intros; red. destruct l; try (monadInv H; auto). + assert (AUX: forall fn id, + is_bitfield_access_aux ce fn id i g = Res bf g' I -> + exists co ofs, + ce!id = Some co /\ fn ce i (co_members co) = OK (ofs, bf)). + { unfold is_bitfield_access_aux; intros. + destruct ce!id as [co|]; try discriminate. + destruct (fn ce i (co_members co)) as [[ofs1 bf1]|] eqn:FN; inv H0. + exists co, ofs1; auto. } + destruct (typeof l); try discriminate; apply AUX; auto. +Qed. + Lemma transl_valof_meets_spec: forall ty a g sl b g' I, - transl_valof ty a g = Res (sl, b) g' I -> + transl_valof ce 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) eqn:?; monadInv H. - exists (x :: nil); split; eauto with gensym. econstructor; eauto with coqlib. + exists (x :: nil); split; eauto with gensym. + econstructor; eauto using is_bitfield_access_meets_spec with coqlib. exists (@nil ident); split; eauto with gensym. constructor; auto. Qed. @@ -763,12 +803,12 @@ Combined Scheme expr_exprlist_ind from expr_ind2, exprlist_ind2. Lemma transl_meets_spec: (forall r dst g sl a g' I, - transl_expr dst r g = Res (sl, a) g' I -> + transl_expr ce dst r g = Res (sl, a) g' I -> dest_below dst g -> exists tmps, (forall le, tr_expr le dst r sl a (add_dest dst tmps)) /\ contained tmps g g') /\ (forall rl g sl al g' I, - transl_exprlist rl g = Res (sl, al) g' I -> + transl_exprlist ce rl g = Res (sl, al) g' I -> exists tmps, (forall le, tr_exprlist le rl sl al tmps) /\ contained tmps g g'). Proof. apply expr_exprlist_ind; simpl add_dest; intros. @@ -920,9 +960,10 @@ Opaque makeif. - (* assign *) monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. exploit H0; eauto. intros [tmp2 [Csyntax D]]. - destruct dst; monadInv EQ2; simpl add_dest in *. + apply is_bitfield_access_meets_spec in EQ0. + destruct dst; monadInv EQ3; simpl add_dest in *. + (* for value *) - exists (x1 :: tmp1 ++ tmp2); split. + exists (x2 :: tmp1 ++ tmp2); split. intros. eapply tr_assign_val with (dst := For_val); eauto with gensym. apply contained_cons. eauto with gensym. apply contained_app; eauto with gensym. @@ -931,7 +972,7 @@ Opaque makeif. econstructor; eauto with gensym. apply contained_app; eauto with gensym. + (* for set *) - exists (x1 :: tmp1 ++ tmp2); split. + exists (x2 :: tmp1 ++ tmp2); split. repeat rewrite app_ass. simpl. intros. eapply tr_assign_val with (dst := For_set sd); eauto with gensym. apply contained_cons. eauto with gensym. @@ -940,37 +981,39 @@ Opaque makeif. monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. exploit H0; eauto. intros [tmp2 [Csyntax D]]. exploit transl_valof_meets_spec; eauto. intros [tmp3 [E F]]. - destruct dst; monadInv EQ3; simpl add_dest in *. + apply is_bitfield_access_meets_spec in EQ2. + destruct dst; monadInv EQ4; simpl add_dest in *. + (* for value *) - 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. + exists (x3 :: tmp1 ++ tmp2 ++ tmp3); split. + intros. eapply tr_assignop_val with (dst := For_val); eauto 6 with gensym. + apply contained_cons. eauto 6 with gensym. + apply contained_app; eauto 6 with gensym. + (* for effects *) exists (tmp1 ++ tmp2 ++ tmp3); split. econstructor; eauto with gensym. apply contained_app; eauto with gensym. + (* for set *) - exists (x2 :: tmp1 ++ tmp2 ++ tmp3); split. + exists (x3 :: tmp1 ++ tmp2 ++ tmp3); split. repeat rewrite app_ass. simpl. - intros. eapply tr_assignop_val with (dst := For_set sd); eauto with gensym. - apply contained_cons. eauto with gensym. - apply contained_app; eauto with gensym. + intros. eapply tr_assignop_val with (dst := For_set sd); eauto 6 with gensym. + apply contained_cons. eauto 6 with gensym. + apply contained_app; eauto 6 with gensym. - (* postincr *) monadInv H0. exploit H; eauto. intros [tmp1 [A B]]. - destruct dst; monadInv EQ0; simpl add_dest in *. + apply is_bitfield_access_meets_spec in EQ1. + destruct dst; monadInv EQ2; simpl add_dest in *. + (* for value *) - exists (x0 :: tmp1); split. + exists (x1 :: tmp1); split. econstructor; eauto with gensym. apply contained_cons; eauto with gensym. + (* for effects *) - exploit transl_valof_meets_spec; eauto. intros [tmp2 [Csyntax D]]. + exploit transl_valof_meets_spec; eauto. intros [tmp2 [C D]]. exists (tmp1 ++ tmp2); split. econstructor; eauto with gensym. eauto with gensym. + (* for set *) repeat rewrite app_ass; simpl. - exists (x0 :: tmp1); split. + exists (x1 :: tmp1); split. econstructor; eauto with gensym. apply contained_cons; eauto with gensym. - (* comma *) @@ -1032,7 +1075,7 @@ Qed. Lemma transl_expr_meets_spec: forall r dst g sl a g' I, - transl_expr dst r g = Res (sl, a) g' I -> + transl_expr ce dst r g = Res (sl, a) g' I -> dest_below dst g -> exists tmps, forall ge e le m, tr_top ge e le m dst r sl a tmps. Proof. @@ -1042,7 +1085,7 @@ Qed. Lemma transl_expression_meets_spec: forall r g s a g' I, - transl_expression r g = Res (s, a) g' I -> + transl_expression ce r g = Res (s, a) g' I -> tr_expression r s a. Proof. intros. monadInv H. exploit transl_expr_meets_spec; eauto. @@ -1051,7 +1094,7 @@ Qed. Lemma transl_expr_stmt_meets_spec: forall r g s g' I, - transl_expr_stmt r g = Res s g' I -> + transl_expr_stmt ce r g = Res s g' I -> tr_expr_stmt r s. Proof. intros. monadInv H. exploit transl_expr_meets_spec; eauto. @@ -1060,7 +1103,7 @@ Qed. Lemma transl_if_meets_spec: forall r s1 s2 g s g' I, - transl_if r s1 s2 g = Res s g' I -> + transl_if ce r s1 s2 g = Res s g' I -> tr_if r s1 s2 s. Proof. intros. monadInv H. exploit transl_expr_meets_spec; eauto. @@ -1068,9 +1111,9 @@ Proof. Qed. Lemma transl_stmt_meets_spec: - forall s g ts g' I, transl_stmt s g = Res ts g' I -> tr_stmt s ts + forall s g ts g' I, transl_stmt ce s g = Res ts g' I -> tr_stmt s ts with transl_lblstmt_meets_spec: - forall s g ts g' I, transl_lblstmt s g = Res ts g' I -> tr_lblstmts s ts. + forall s g ts g' I, transl_lblstmt ce s g = Res ts g' I -> tr_lblstmts s ts. Proof. generalize transl_expression_meets_spec transl_expr_stmt_meets_spec transl_if_meets_spec; intros T1 T2 T3. Opaque transl_expression transl_expr_stmt. @@ -1099,32 +1142,32 @@ Inductive tr_function: Csyntax.function -> Clight.function -> Prop := fn_vars tf = Csyntax.fn_vars f -> tr_function f tf. -Inductive tr_fundef: Csyntax.fundef -> Clight.fundef -> Prop := - | tr_internal: forall f tf, - tr_function f tf -> - tr_fundef (Internal f) (Internal tf) - | tr_external: forall ef targs tres cconv, - tr_fundef (External ef targs tres cconv) (External ef targs tres cconv). - Lemma transl_function_spec: forall f tf, - transl_function f = OK tf -> + transl_function ce f = OK tf -> tr_function f tf. Proof. unfold transl_function; intros. - destruct (transl_stmt (Csyntax.fn_body f) (initial_generator tt)) eqn:T; inv H. + destruct (transl_stmt ce (Csyntax.fn_body f) (initial_generator tt)) eqn:T; inv H. constructor; auto. simpl. eapply transl_stmt_meets_spec; eauto. Qed. +End SPEC. + +Inductive tr_fundef (p: Csyntax.program): Csyntax.fundef -> Clight.fundef -> Prop := + | tr_internal: forall f tf, + tr_function p.(prog_comp_env) f tf -> + tr_fundef p (Internal f) (Internal tf) + | tr_external: forall ef targs tres cconv, + tr_fundef p (External ef targs tres cconv) (External ef targs tres cconv). + Lemma transl_fundef_spec: - forall fd tfd, - transl_fundef fd = OK tfd -> - tr_fundef fd tfd. + forall p fd tfd, + transl_fundef p.(prog_comp_env) fd = OK tfd -> + tr_fundef p fd tfd. Proof. unfold transl_fundef; intros. destruct fd; Errors.monadInv H. + constructor. eapply transl_function_spec; eauto. + constructor. Qed. - -End SPEC. |