From 070babeff47562a72d6a58dd70fc7ac1bcbf205c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 15 Jun 2020 19:20:15 +0200 Subject: SimplExpr: better translation of casts in a "for effects" context This is useful for statements such as `(void) expr;` where we would prefer not to explicitly compute intermediate values of type `void` and store them in Clight temporary variables. See issue #361 for a real-world occurrence of this phenomenon. --- cfrontend/SimplExpr.v | 11 ++- cfrontend/SimplExprproof.v | 165 +++++++++++++++++++++++---------------------- cfrontend/SimplExprspec.v | 126 +++++++++++++++++++--------------- 3 files changed, 166 insertions(+), 136 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index 7cdff468..1398317d 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -226,6 +226,8 @@ Definition sd_seqbool_val (tmp: ident) (ty: type) := SDbase type_bool ty tmp. Definition sd_seqbool_set (ty: type) (sd: set_destination) := let tmp := sd_temp sd in SDcons type_bool ty tmp sd. +Definition sd_cast_set (ty: type) (sd: set_destination) := + let tmp := sd_temp sd in SDcons ty ty tmp sd. Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement * expr) := match a with @@ -268,8 +270,13 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement do (sl2, a2) <- transl_expr For_val r2; ret (finish dst (sl1 ++ sl2) (Ebinop op a1 a2 ty)) | Csyntax.Ecast r1 ty => - do (sl1, a1) <- transl_expr For_val r1; - ret (finish dst sl1 (Ecast a1 ty)) + match dst with + | For_val | For_set _ => + do (sl1, a1) <- transl_expr For_val r1; + ret (finish dst sl1 (Ecast a1 ty)) + | For_effects => + transl_expr For_effects r1 + end | Csyntax.Eseqand r1 r2 ty => do (sl1, a1) <- transl_expr For_val r1; match dst with diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index ee1df409..9a3f32ec 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -145,18 +145,18 @@ 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 discriminate; auto. - rewrite H0; auto. simpl; auto. - rewrite H0; auto. simpl; auto. - destruct H1; congruence. - destruct (andb_prop _ _ H6). inv H1. +- rewrite H0; auto. simpl; auto. +- rewrite H0; auto. simpl; auto. +- destruct H1; congruence. +- destruct (andb_prop _ _ H6). inv H1. rewrite H0; eauto. simpl; auto. unfold chunk_for_volatile_type in H9. destruct (type_is_volatile (Csyntax.typeof e1)); simpl in H8; congruence. - rewrite H0; auto. simpl; auto. - rewrite H0; auto. simpl; auto. - destruct (andb_prop _ _ H7). rewrite H0; auto. rewrite H2; auto. simpl; auto. - rewrite H0; auto. simpl; auto. - destruct (andb_prop _ _ H6). rewrite H0; auto. +- rewrite H0; auto. simpl; auto. +- rewrite H0; auto. simpl; auto. +- destruct (andb_prop _ _ H7). rewrite H0; auto. rewrite H2; auto. simpl; auto. +- rewrite H0; auto. simpl; auto. +- destruct (andb_prop _ _ H6). rewrite H0; auto. Qed. Lemma tr_simple_expr_nil: @@ -234,11 +234,11 @@ Proof. Opaque makeif. intros e m. apply (eval_simple_rvalue_lvalue_ind ge e m); intros until tmps; intros TR; inv TR. -(* value *) +- (* value *) auto. - auto. - exists a0; auto. -(* rvalof *) +- auto. +- exists a0; auto. +- (* rvalof *) inv H7; try congruence. exploit H0; eauto. intros [A [B C]]. subst sl1; simpl. @@ -248,53 +248,55 @@ Opaque makeif. exploit deref_loc_translated; eauto. unfold chunk_for_volatile_type; rewrite H2. tauto. destruct dst; auto. econstructor. split. simpl; eauto. auto. -(* addrof *) +- (* addrof *) exploit H0; eauto. intros [A [B C]]. subst sl1; simpl. assert (eval_expr tge e le m (Eaddrof' a1 ty) (Vptr b ofs)) by (apply eval_Eaddrof'; auto). assert (typeof (Eaddrof' a1 ty) = ty) by (apply typeof_Eaddrof'). destruct dst; auto. simpl; econstructor; eauto. -(* unop *) +- (* unop *) exploit H0; eauto. intros [A [B C]]. subst sl1; simpl. assert (eval_expr tge e le m (Eunop op a1 ty) v). econstructor; eauto. congruence. destruct dst; auto. simpl; econstructor; eauto. -(* binop *) +- (* binop *) exploit H0; eauto. intros [A [B C]]. exploit H2; eauto. intros [D [E F]]. subst sl1 sl2; simpl. assert (eval_expr tge e le m (Ebinop op a1 a2 ty) v). econstructor; eauto. rewrite comp_env_preserved; congruence. destruct dst; auto. simpl; econstructor; eauto. -(* cast *) +- (* cast effects *) + exploit H0; eauto. +- (* cast val *) exploit H0; eauto. intros [A [B C]]. subst sl1; simpl. assert (eval_expr tge e le m (Ecast a1 ty) v). econstructor; eauto. congruence. destruct dst; auto. simpl; econstructor; eauto. -(* sizeof *) +- (* sizeof *) rewrite <- comp_env_preserved. destruct dst. split; auto. split; auto. constructor. auto. exists (Esizeof ty1 ty). split. auto. split. auto. constructor. -(* alignof *) +- (* alignof *) rewrite <- comp_env_preserved. destruct dst. split; auto. split; auto. constructor. auto. exists (Ealignof ty1 ty). split. auto. split. auto. constructor. -(* var local *) +- (* var local *) split; auto. split; auto. apply eval_Evar_local; auto. -(* var global *) +- (* var global *) split; auto. split; auto. apply eval_Evar_global; auto. rewrite symbols_preserved; auto. -(* deref *) +- (* deref *) exploit H0; eauto. intros [A [B C]]. subst sl1. split; auto. split. rewrite typeof_Ederef'; auto. apply eval_Ederef'; auto. -(* field struct *) +- (* field struct *) rewrite <- comp_env_preserved in *. exploit H0; eauto. intros [A [B C]]. subst sl1. split; auto. split; auto. rewrite B in H1. eapply eval_Efield_struct; eauto. -(* field union *) +- (* field union *) rewrite <- comp_env_preserved in *. exploit H0; eauto. intros [A [B C]]. subst sl1. split; auto. split; auto. rewrite B in H1. eapply eval_Efield_union; eauto. @@ -408,43 +410,43 @@ Ltac UNCHANGED := (*generalize compat_dest_change; intro CDC.*) apply leftcontext_leftcontextlist_ind; intros. -(* base *) +- (* base *) TR. rewrite <- app_nil_end; auto. red; auto. intros. rewrite <- app_nil_end; auto. -(* deref *) +- (* deref *) inv H1. exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. subst sl1; rewrite app_ass; eauto. auto. intros. rewrite <- app_ass. econstructor; eauto. -(* field *) +- (* field *) inv H1. exploit H0. eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. subst sl1; rewrite app_ass; eauto. auto. intros. rewrite <- app_ass. econstructor; eauto. -(* rvalof *) +- (* rvalof *) inv H1. exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. subst sl1; rewrite app_ass; eauto. red; eauto. intros. rewrite <- app_ass; econstructor; eauto. exploit typeof_context; eauto. congruence. -(* addrof *) +- (* addrof *) inv H1. exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. subst sl1; rewrite app_ass; eauto. auto. intros. rewrite <- app_ass. econstructor; eauto. -(* unop *) +- (* unop *) inv H1. exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. subst sl1; rewrite app_ass; eauto. auto. intros. rewrite <- app_ass. econstructor; eauto. -(* binop left *) +- (* binop left *) inv H1. exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. subst sl1. rewrite app_ass. eauto. red; auto. intros. rewrite <- app_ass. econstructor; eauto. eapply tr_expr_invariant; eauto. UNCHANGED. -(* binop right *) +- (* binop right *) inv H2. assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl. exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. @@ -452,14 +454,19 @@ Ltac UNCHANGED := red; auto. intros. rewrite <- app_ass. change (sl3 ++ sl2') with (nil ++ sl3 ++ sl2'). rewrite app_ass. econstructor; eauto. eapply tr_expr_invariant; eauto. UNCHANGED. -(* cast *) +- (* cast *) inv H1. ++ (* for effects *) exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. - TR. subst sl1; rewrite app_ass; eauto. auto. + TR. eauto. auto. + intros. econstructor; eauto. ++ (* generic *) + exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. + TR. subst sl1. rewrite app_ass. eauto. auto. intros. rewrite <- app_ass. econstructor; eauto. -(* seqand *) +- (* seqand *) inv H1. - (* for val *) ++ (* for val *) exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. rewrite Q. rewrite app_ass. eauto. @@ -467,15 +474,15 @@ Ltac UNCHANGED := intros. rewrite <- app_ass. econstructor. apply S; auto. eapply tr_expr_invariant; eauto. UNCHANGED. auto. auto. auto. auto. - (* for effects *) ++ (* for effects *) exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. rewrite Q. rewrite app_ass. eauto. red; auto. intros. rewrite <- app_ass. econstructor. apply S; auto. eapply tr_expr_invariant; eauto. UNCHANGED. - auto. auto. auto. auto. - (* for set *) + auto. auto. auto. ++ (* for set *) exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. rewrite Q. rewrite app_ass. eauto. @@ -483,9 +490,9 @@ Ltac UNCHANGED := intros. rewrite <- app_ass. econstructor. apply S; auto. eapply tr_expr_invariant; eauto. UNCHANGED. auto. auto. auto. auto. -(* seqor *) +- (* seqor *) inv H1. - (* for val *) ++ (* for val *) exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. rewrite Q. rewrite app_ass. eauto. @@ -493,15 +500,15 @@ Ltac UNCHANGED := intros. rewrite <- app_ass. econstructor. apply S; auto. eapply tr_expr_invariant; eauto. UNCHANGED. auto. auto. auto. auto. - (* for effects *) ++ (* for effects *) exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. rewrite Q. rewrite app_ass. eauto. red; auto. intros. rewrite <- app_ass. econstructor. apply S; auto. eapply tr_expr_invariant; eauto. UNCHANGED. - auto. auto. auto. auto. - (* for set *) + auto. auto. auto. ++ (* for set *) exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. rewrite Q. rewrite app_ass. eauto. @@ -509,9 +516,9 @@ Ltac UNCHANGED := intros. rewrite <- app_ass. econstructor. apply S; auto. eapply tr_expr_invariant; eauto. UNCHANGED. auto. auto. auto. auto. -(* condition *) +- (* condition *) inv H1. - (* for val *) ++ (* for val *) exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. rewrite Q. rewrite app_ass. eauto. @@ -520,7 +527,7 @@ Ltac UNCHANGED := eapply tr_expr_invariant; eauto. UNCHANGED. eapply tr_expr_invariant; eauto. UNCHANGED. auto. auto. auto. auto. auto. auto. - (* for effects *) ++ (* for effects *) exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. rewrite Q. rewrite app_ass. eauto. @@ -529,7 +536,7 @@ Ltac UNCHANGED := eapply tr_expr_invariant; eauto. UNCHANGED. eapply tr_expr_invariant; eauto. UNCHANGED. auto. auto. auto. auto. auto. - (* for set *) ++ (* for set *) exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. rewrite Q. rewrite app_ass. eauto. @@ -538,16 +545,16 @@ Ltac UNCHANGED := eapply tr_expr_invariant; eauto. UNCHANGED. eapply tr_expr_invariant; eauto. UNCHANGED. auto. auto. auto. auto. auto. auto. -(* assign left *) +- (* assign left *) inv H1. - (* for effects *) ++ (* for effects *) exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. subst sl1. rewrite app_ass. eauto. red; auto. intros. rewrite <- app_ass. econstructor. apply S; auto. eapply tr_expr_invariant; eauto. UNCHANGED. auto. auto. auto. - (* for val *) ++ (* for val *) exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. subst sl1. rewrite app_ass. eauto. red; auto. @@ -556,9 +563,9 @@ Ltac UNCHANGED := auto. auto. auto. auto. auto. auto. eapply typeof_context; eauto. auto. -(* assign right *) +- (* assign right *) inv H2. - (* for effects *) ++ (* for effects *) assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl. exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. subst sl2. rewrite app_ass. eauto. @@ -567,7 +574,7 @@ Ltac UNCHANGED := econstructor. eapply tr_expr_invariant; eauto. UNCHANGED. apply S; auto. auto. auto. auto. - (* for val *) ++ (* for val *) assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl. exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. subst sl2. rewrite app_ass. eauto. @@ -577,9 +584,9 @@ Ltac UNCHANGED := eapply tr_expr_invariant; eauto. UNCHANGED. apply S; auto. auto. auto. auto. auto. auto. auto. auto. eapply typeof_context; eauto. -(* assignop left *) +- (* assignop left *) inv H1. - (* for effects *) ++ (* for effects *) exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. subst sl1. rewrite app_ass. eauto. red; auto. @@ -587,7 +594,7 @@ Ltac UNCHANGED := eapply tr_expr_invariant; eauto. UNCHANGED. symmetry; eapply typeof_context; eauto. eauto. auto. auto. auto. auto. auto. auto. - (* for val *) ++ (* for val *) exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. subst sl1. rewrite app_ass. eauto. red; auto. @@ -595,9 +602,9 @@ Ltac UNCHANGED := eapply tr_expr_invariant; eauto. UNCHANGED. eauto. auto. auto. auto. auto. auto. auto. auto. auto. auto. auto. eapply typeof_context; eauto. -(* assignop right *) +- (* assignop right *) inv H2. - (* for effects *) ++ (* for effects *) assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl. exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. subst sl2. rewrite app_ass. eauto. @@ -605,7 +612,7 @@ Ltac UNCHANGED := intros. rewrite <- app_ass. change (sl0 ++ sl2') with (nil ++ sl0 ++ sl2'). rewrite app_ass. econstructor. eapply tr_expr_invariant; eauto. UNCHANGED. apply S; auto. auto. eauto. auto. auto. auto. auto. auto. auto. - (* for val *) ++ (* for val *) assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl. exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. subst sl2. rewrite app_ass. eauto. @@ -613,35 +620,35 @@ Ltac UNCHANGED := intros. rewrite <- app_ass. change (sl0 ++ sl2') with (nil ++ sl0 ++ sl2'). rewrite app_ass. econstructor. eapply tr_expr_invariant; eauto. UNCHANGED. apply S; auto. eauto. auto. auto. auto. auto. auto. auto. auto. auto. auto. auto. auto. -(* postincr *) +- (* postincr *) inv H1. - (* for effects *) ++ (* for effects *) exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. rewrite Q; rewrite app_ass; eauto. red; auto. intros. rewrite <- app_ass. econstructor; eauto. symmetry; eapply typeof_context; eauto. - (* for val *) ++ (* for val *) exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. rewrite Q; rewrite app_ass; eauto. red; auto. intros. rewrite <- app_ass. econstructor; eauto. eapply typeof_context; eauto. -(* call left *) +- (* call left *) inv H1. - (* for effects *) ++ (* for effects *) exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. rewrite Q; rewrite app_ass; eauto. red; auto. intros. rewrite <- app_ass. econstructor. apply S; auto. eapply tr_exprlist_invariant; eauto. UNCHANGED. auto. auto. auto. - (* for val *) ++ (* for val *) exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. rewrite Q; rewrite app_ass; eauto. red; auto. intros. rewrite <- app_ass. econstructor. auto. apply S; auto. eapply tr_exprlist_invariant; eauto. UNCHANGED. auto. auto. auto. auto. -(* call right *) +- (* call right *) inv H2. - (* for effects *) ++ (* for effects *) assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl. exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. rewrite Q; rewrite app_ass; eauto. @@ -650,7 +657,7 @@ Ltac UNCHANGED := intros. rewrite <- app_ass. change (sl3++sl2') with (nil ++ sl3 ++ sl2'). rewrite app_ass. econstructor. eapply tr_expr_invariant; eauto. UNCHANGED. apply S; auto. auto. auto. auto. - (* for val *) ++ (* for val *) assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl. exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. rewrite Q; rewrite app_ass; eauto. @@ -660,42 +667,42 @@ Ltac UNCHANGED := auto. eapply tr_expr_invariant; eauto. UNCHANGED. apply S; auto. auto. auto. auto. auto. -(* builtin *) +- (* builtin *) inv H1. - (* for effects *) ++ (* for effects *) exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. rewrite Q; rewrite app_ass; eauto. red; auto. intros. rewrite <- app_ass. change (sl3++sl2') with (nil ++ sl3 ++ sl2'). rewrite app_ass. econstructor. apply S; auto. auto. - (* for val *) ++ (* for val *) exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. rewrite Q; rewrite app_ass; eauto. red; auto. intros. rewrite <- app_ass. change (sl3++sl2') with (nil ++ sl3 ++ sl2'). rewrite app_ass. econstructor. auto. apply S; auto. auto. auto. -(* comma *) +- (* comma *) inv H1. exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. rewrite Q; rewrite app_ass; eauto. red; auto. intros. rewrite <- app_ass. econstructor. apply S; auto. eapply tr_expr_invariant; eauto. UNCHANGED. auto. auto. auto. -(* paren *) +- (* paren *) inv H1. - (* for val *) ++ (* for val *) exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. rewrite Q. eauto. red; auto. intros. econstructor; eauto. - (* for effects *) ++ (* for effects *) exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. rewrite Q. eauto. auto. intros. econstructor; eauto. - (* for set *) ++ (* for set *) exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. rewrite Q. eauto. auto. intros. econstructor; eauto. -(* cons left *) +- (* cons left *) inv H1. exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. TR. subst sl1. rewrite app_ass. eauto. @@ -703,7 +710,7 @@ Ltac UNCHANGED := intros. rewrite <- app_ass. econstructor. apply S; auto. eapply tr_exprlist_invariant; eauto. UNCHANGED. auto. auto. auto. -(* cons right *) +- (* cons right *) inv H2. assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl. exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [R S]]]]]]]]. diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v index e7d57a1c..98425311 100644 --- a/cfrontend/SimplExprspec.v +++ b/cfrontend/SimplExprspec.v @@ -108,7 +108,12 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement -> tr_expr le dst (Csyntax.Ebinop op e1 e2 ty) (sl1 ++ sl2 ++ final dst (Ebinop op a1 a2 ty)) (Ebinop op a1 a2 ty) tmp - | tr_cast: forall le dst e1 ty sl1 a1 tmp, + | tr_cast_effects: forall le e1 ty sl1 a1 any tmp, + tr_expr le For_effects e1 sl1 a1 tmp -> + tr_expr le For_effects (Csyntax.Ecast e1 ty) + sl1 + any tmp + | tr_cast_val: forall le dst e1 ty sl1 a1 tmp, tr_expr le For_val e1 sl1 a1 tmp -> tr_expr le dst (Csyntax.Ecast e1 ty) (sl1 ++ final dst (Ecast a1 ty)) @@ -767,58 +772,69 @@ Lemma transl_meets_spec: exists tmps, (forall le, tr_exprlist le rl sl al tmps) /\ contained tmps g g'). Proof. apply expr_exprlist_ind; simpl add_dest; intros. -(* val *) +- (* val *) simpl in H. destruct v; monadInv H; exists (@nil ident); split; auto with gensym. Opaque makeif. - intros. destruct dst; simpl in *; inv H2. ++ intros. destruct dst; simpl in *; inv H2. constructor. auto. intros; constructor. constructor. constructor. auto. intros; constructor. - intros. destruct dst; simpl in *; inv H2. ++ intros. destruct dst; simpl in *; inv H2. constructor. auto. intros; constructor. constructor. constructor. auto. intros; constructor. - intros. destruct dst; simpl in *; inv H2. ++ intros. destruct dst; simpl in *; inv H2. constructor. auto. intros; constructor. constructor. constructor. auto. intros; constructor. - intros. destruct dst; simpl in *; inv H2. ++ intros. destruct dst; simpl in *; inv H2. constructor. auto. intros; constructor. constructor. constructor. auto. intros; constructor. -(* var *) +- (* var *) monadInv H; econstructor; split; auto with gensym. UseFinish. constructor. -(* field *) +- (* field *) monadInv H0. exploit H; eauto. auto. intros [tmp [A B]]. UseFinish. econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto. -(* valof *) +- (* valof *) monadInv H0. exploit H; eauto. intros [tmp1 [A B]]. exploit transl_valof_meets_spec; eauto. intros [tmp2 [Csyntax D]]. UseFinish. exists (tmp1 ++ tmp2); split. intros; apply tr_expr_add_dest. econstructor; eauto with gensym. eauto with gensym. -(* deref *) +- (* deref *) monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish. econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto. -(* addrof *) +- (* addrof *) monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish. econstructor; split; eauto. intros; apply tr_expr_add_dest. econstructor; eauto. -(* unop *) +- (* unop *) monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish. econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto. -(* binop *) +- (* binop *) monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. exploit H0; eauto. intros [tmp2 [Csyntax D]]. UseFinish. exists (tmp1 ++ tmp2); split. intros; apply tr_expr_add_dest. econstructor; eauto with gensym. eauto with gensym. -(* cast *) - monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish. - econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto. -(* seqand *) +- (* cast *) + destruct dst. ++ (* for value *) + monadInv H0. exploit H; eauto. intros [tmp [A B]]. + econstructor; split; eauto. intros; apply tr_expr_add_dest. + rewrite (app_nil_end sl). + apply tr_cast_val with (dst := For_val); auto. ++ (* for effects *) + exploit H; eauto. intros [tmp [A B]]. + econstructor; split; eauto. intros; eapply tr_cast_effects; eauto. ++ (* for set *) + monadInv H0. exploit H; eauto. intros [tmp [A B]]. + econstructor; split; eauto. intros; apply tr_expr_add_dest. + apply tr_cast_val with (dst := For_set sd); auto. +- (* seqand *) monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. destruct dst; monadInv EQ0. - (* for value *) ++ (* for value *) exploit H0; eauto with gensym. intros [tmp2 [C D]]. simpl add_dest in *. exists (x0 :: tmp1 ++ tmp2); split. @@ -826,23 +842,23 @@ Opaque makeif. apply list_disjoint_cons_r; eauto with gensym. apply contained_cons. eauto with gensym. apply contained_app; eauto with gensym. - (* for effects *) ++ (* for effects *) exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]]. simpl add_dest in *. exists (tmp1 ++ tmp2); split. intros; eapply tr_seqand_effects; eauto with gensym. apply contained_app; eauto with gensym. - (* for set *) ++ (* for set *) exploit H0; eauto with gensym. intros [tmp2 [C D]]. simpl add_dest in *. exists (tmp1 ++ tmp2); split. intros; eapply tr_seqand_set; eauto with gensym. apply list_disjoint_cons_r; eauto with gensym. apply contained_app; eauto with gensym. -(* seqor *) +- (* seqor *) monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. destruct dst; monadInv EQ0. - (* for value *) ++ (* for value *) exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]]. simpl add_dest in *. exists (x0 :: tmp1 ++ tmp2); split. @@ -850,23 +866,23 @@ Opaque makeif. apply list_disjoint_cons_r; eauto with gensym. apply contained_cons. eauto with gensym. apply contained_app; eauto with gensym. - (* for effects *) ++ (* for effects *) exploit H0; eauto with gensym. intros [tmp2 [C D]]. simpl add_dest in *. exists (tmp1 ++ tmp2); split. intros; eapply tr_seqor_effects; eauto with gensym. apply contained_app; eauto with gensym. - (* for set *) ++ (* for set *) exploit H0; eauto with gensym. intros [tmp2 [C D]]. simpl add_dest in *. exists (tmp1 ++ tmp2); split. intros; eapply tr_seqor_set; eauto with gensym. apply list_disjoint_cons_r; eauto with gensym. apply contained_app; eauto with gensym. -(* condition *) +- (* condition *) monadInv H2. exploit H; eauto. intros [tmp1 [A B]]. destruct dst; monadInv EQ0. - (* for value *) ++ (* for value *) exploit H0; eauto with gensym. intros [tmp2 [C D]]. exploit H1; eauto with gensym. intros [tmp3 [E F]]. simpl add_dest in *. @@ -877,14 +893,14 @@ Opaque makeif. apply contained_cons. eauto with gensym. apply contained_app. eauto with gensym. apply contained_app; eauto with gensym. - (* for effects *) ++ (* for effects *) exploit H0; eauto. intros [tmp2 [Csyntax D]]. exploit H1; eauto. intros [tmp3 [E F]]. simpl add_dest in *. exists (tmp1 ++ tmp2 ++ tmp3); split. intros; eapply tr_condition_effects; eauto with gensym. apply contained_app; eauto with gensym. - (* for test *) ++ (* for test *) exploit H0; eauto with gensym. intros [tmp2 [C D]]. exploit H1; eauto 10 with gensym. intros [tmp3 [E F]]. simpl add_dest in *. @@ -895,69 +911,69 @@ Opaque makeif. apply contained_cons; eauto with gensym. apply contained_app; eauto with gensym. apply contained_app; eauto with gensym. -(* sizeof *) +- (* sizeof *) monadInv H. UseFinish. exists (@nil ident); split; auto with gensym. constructor. -(* alignof *) +- (* alignof *) monadInv H. UseFinish. exists (@nil ident); split; auto with gensym. constructor. -(* assign *) +- (* 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 *. - (* for value *) ++ (* for value *) exists (x1 :: 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. - (* for effects *) ++ (* for effects *) exists (tmp1 ++ tmp2); split. econstructor; eauto with gensym. apply contained_app; eauto with gensym. - (* for set *) ++ (* for set *) exists (x1 :: 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. apply contained_app; eauto with gensym. -(* assignop *) +- (* assignop *) 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 *. - (* for value *) ++ (* 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. - (* for effects *) ++ (* for effects *) exists (tmp1 ++ tmp2 ++ tmp3); split. econstructor; eauto with gensym. apply contained_app; eauto with gensym. - (* for set *) ++ (* for set *) exists (x2 :: 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. -(* postincr *) +- (* postincr *) monadInv H0. exploit H; eauto. intros [tmp1 [A B]]. destruct dst; monadInv EQ0; simpl add_dest in *. - (* for value *) ++ (* for value *) exists (x0 :: tmp1); split. econstructor; eauto with gensym. apply contained_cons; eauto with gensym. - (* for effects *) ++ (* for effects *) exploit transl_valof_meets_spec; eauto. intros [tmp2 [Csyntax D]]. exists (tmp1 ++ tmp2); split. econstructor; eauto with gensym. eauto with gensym. - (* for set *) ++ (* for set *) repeat rewrite app_ass; simpl. exists (x0 :: tmp1); split. econstructor; eauto with gensym. apply contained_cons; eauto with gensym. -(* comma *) +- (* comma *) monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]]. exists (tmp1 ++ tmp2); split. @@ -967,46 +983,46 @@ Opaque makeif. simpl. eapply incl_tran. 2: apply add_dest_incl. auto with gensym. destruct dst; simpl; auto with gensym. apply contained_app; eauto with gensym. -(* call *) +- (* call *) monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. exploit H0; eauto. intros [tmp2 [Csyntax D]]. destruct dst; monadInv EQ2; simpl add_dest in *. - (* for value *) ++ (* for value *) exists (x1 :: tmp1 ++ tmp2); split. econstructor; eauto with gensym. congruence. apply contained_cons. eauto with gensym. apply contained_app; eauto with gensym. - (* for effects *) ++ (* for effects *) exists (tmp1 ++ tmp2); split. econstructor; eauto with gensym. apply contained_app; eauto with gensym. - (* for set *) ++ (* for set *) exists (x1 :: tmp1 ++ tmp2); split. repeat rewrite app_ass. econstructor; eauto with gensym. congruence. apply contained_cons. eauto with gensym. apply contained_app; eauto with gensym. -(* builtin *) +- (* builtin *) monadInv H0. exploit H; eauto. intros [tmp1 [A B]]. destruct dst; monadInv EQ0; simpl add_dest in *. - (* for value *) ++ (* for value *) exists (x0 :: tmp1); split. econstructor; eauto with gensym. congruence. apply contained_cons; eauto with gensym. - (* for effects *) ++ (* for effects *) exists tmp1; split. econstructor; eauto with gensym. auto. - (* for set *) ++ (* for set *) exists (x0 :: tmp1); split. repeat rewrite app_ass. econstructor; eauto with gensym. congruence. apply contained_cons; eauto with gensym. -(* loc *) +- (* loc *) monadInv H. -(* paren *) +- (* paren *) monadInv H0. -(* nil *) +- (* nil *) monadInv H; exists (@nil ident); split; auto with gensym. constructor. -(* cons *) +- (* cons *) monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. exploit H0; eauto. intros [tmp2 [Csyntax D]]. exists (tmp1 ++ tmp2); split. -- cgit