summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-05-19 07:57:29 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-05-19 07:57:29 +0000
commit0d27eae0b07c7c46cb7d4e6d7b0b1145dbdab0c3 (patch)
tree7fdacd8abd518194cc5b05f1aa614c646e635805
parenta3f1744823d6dbeaf400812de86263fb615bbbba (diff)
Issue with simplification of nested ?: expressions of different types.
(Ill-typed Clight/Cminor/RTL code was generated due to incorrect reuse of destination temporary.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2257 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r--cfrontend/SimplExpr.v60
-rw-r--r--cfrontend/SimplExprproof.v20
-rw-r--r--cfrontend/SimplExprspec.v134
-rw-r--r--test/regression/seqops.c6
4 files changed, 135 insertions, 85 deletions
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v
index 98dad93..8e6bc9f 100644
--- a/cfrontend/SimplExpr.v
+++ b/cfrontend/SimplExpr.v
@@ -187,26 +187,37 @@ Definition make_assign (l r: expr) : statement :=
assignment. In this case, [a] is meaningless.
*)
+Inductive set_destination : Type :=
+ | SDbase (ty: type) (tmp: ident)
+ | SDcons (ty: type) (tmp: ident) (sd: set_destination).
+
Inductive destination : Type :=
| For_val
| For_effects
- | For_set (tyl: list type) (tmp: ident).
+ | For_set (sd: set_destination).
Definition dummy_expr := Econst_int Int.zero type_int32s.
-Fixpoint do_set (tmp: ident) (tyl: list type) (a: expr) : list statement :=
- match tyl with
- | nil => nil
- | ty1 :: tys => Sset tmp (Ecast a ty1) :: do_set tmp tys (Etempvar tmp ty1)
+Fixpoint do_set (sd: set_destination) (a: expr) : list statement :=
+ match sd with
+ | SDbase ty tmp => Sset tmp (Ecast a ty) :: nil
+ | SDcons ty tmp sd' => Sset tmp (Ecast a ty) :: do_set sd' (Etempvar tmp ty)
end.
Definition finish (dst: destination) (sl: list statement) (a: expr) :=
match dst with
| For_val => (sl, a)
| For_effects => (sl, a)
- | For_set tyl tmp => (sl ++ do_set tmp tyl a, a)
+ | For_set sd => (sl ++ do_set sd a, a)
end.
+Definition sd_temp (sd: set_destination) :=
+ match sd with SDbase _ tmp => tmp | SDcons _ tmp _ => tmp end.
+Definition sd_seqbool_val (tmp: ident) (ty: type) :=
+ SDcons type_bool tmp (SDbase ty tmp).
+Definition sd_seqbool_set (ty: type) (sd: set_destination) :=
+ let tmp := sd_temp sd in SDcons type_bool tmp (SDcons ty tmp sd).
+
Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement * expr) :=
match a with
| Csyntax.Eloc b ofs ty =>
@@ -253,17 +264,17 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
match dst with
| For_val =>
do t <- gensym ty;
- do (sl2, a2) <- transl_expr (For_set (type_bool :: ty :: nil) t) r2;
+ do (sl2, a2) <- transl_expr (For_set (sd_seqbool_val t ty)) r2;
ret (sl1 ++
makeif a1 (makeseq sl2) (Sset t (Econst_int Int.zero ty)) :: nil,
Etempvar t ty)
| For_effects =>
do (sl2, a2) <- transl_expr For_effects r2;
ret (sl1 ++ makeif a1 (makeseq sl2) Sskip :: nil, dummy_expr)
- | For_set tyl t =>
- do (sl2, a2) <- transl_expr (For_set (type_bool :: ty :: tyl) t) r2;
+ | For_set sd =>
+ do (sl2, a2) <- transl_expr (For_set (sd_seqbool_set ty sd)) r2;
ret (sl1 ++
- makeif a1 (makeseq sl2) (makeseq (do_set t tyl (Econst_int Int.zero ty))) :: nil,
+ makeif a1 (makeseq sl2) (makeseq (do_set sd (Econst_int Int.zero ty))) :: nil,
dummy_expr)
end
| Csyntax.Eseqor r1 r2 ty =>
@@ -271,17 +282,17 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
match dst with
| For_val =>
do t <- gensym ty;
- do (sl2, a2) <- transl_expr (For_set (type_bool :: ty :: nil) t) r2;
+ do (sl2, a2) <- transl_expr (For_set (sd_seqbool_val t ty)) r2;
ret (sl1 ++
makeif a1 (Sset t (Econst_int Int.one ty)) (makeseq sl2) :: nil,
Etempvar t ty)
| For_effects =>
do (sl2, a2) <- transl_expr For_effects r2;
ret (sl1 ++ makeif a1 Sskip (makeseq sl2) :: nil, dummy_expr)
- | For_set tyl t =>
- do (sl2, a2) <- transl_expr (For_set (type_bool :: ty :: tyl) t) r2;
+ | For_set sd =>
+ do (sl2, a2) <- transl_expr (For_set (sd_seqbool_set ty sd)) r2;
ret (sl1 ++
- makeif a1 (makeseq (do_set t tyl (Econst_int Int.one ty))) (makeseq sl2) :: nil,
+ makeif a1 (makeseq (do_set sd (Econst_int Int.one ty))) (makeseq sl2) :: nil,
dummy_expr)
end
| Csyntax.Econdition r1 r2 r3 ty =>
@@ -289,8 +300,8 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
match dst with
| For_val =>
do t <- gensym ty;
- do (sl2, a2) <- transl_expr (For_set (ty::nil) t) r2;
- do (sl3, a3) <- transl_expr (For_set (ty::nil) t) r3;
+ do (sl2, a2) <- transl_expr (For_set (SDbase ty t)) r2;
+ do (sl3, a3) <- transl_expr (For_set (SDbase ty t)) r3;
ret (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil,
Etempvar t ty)
| For_effects =>
@@ -298,9 +309,10 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
do (sl3, a3) <- transl_expr For_effects r3;
ret (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil,
dummy_expr)
- | For_set tyl t =>
- do (sl2, a2) <- transl_expr (For_set (ty::tyl) t) r2;
- do (sl3, a3) <- transl_expr (For_set (ty::tyl) t) r3;
+ | For_set sd =>
+ do t <- gensym ty;
+ do (sl2, a2) <- transl_expr (For_set (SDcons ty t sd)) r2;
+ do (sl3, a3) <- transl_expr (For_set (SDcons ty t sd)) r3;
ret (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil,
dummy_expr)
end
@@ -310,7 +322,7 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
let ty1 := Csyntax.typeof l1 in
let ty2 := Csyntax.typeof r2 in
match dst with
- | For_val | For_set _ _ =>
+ | For_val | For_set _ =>
do t <- gensym ty2;
ret (finish dst
(sl1 ++ sl2 ++ Sset t a2 :: make_assign a1 (Etempvar t ty2) :: nil)
@@ -325,7 +337,7 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
do (sl2, a2) <- transl_expr For_val r2;
do (sl3, a3) <- transl_valof ty1 a1;
match dst with
- | For_val | For_set _ _ =>
+ | For_val | For_set _ =>
do t <- gensym tyres;
ret (finish dst
(sl1 ++ sl2 ++ sl3 ++
@@ -340,7 +352,7 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
let ty1 := Csyntax.typeof l1 in
do (sl1, a1) <- transl_expr For_val l1;
match dst with
- | For_val | For_set _ _ =>
+ | For_val | For_set _ =>
do t <- gensym ty1;
ret (finish dst
(sl1 ++ make_set t a1 ::
@@ -359,7 +371,7 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
do (sl1, a1) <- transl_expr For_val r1;
do (sl2, al2) <- transl_exprlist rl2;
match dst with
- | For_val | For_set _ _ =>
+ | For_val | For_set _ =>
do t <- gensym ty;
ret (finish dst (sl1 ++ sl2 ++ Scall (Some t) a1 al2 :: nil)
(Etempvar t ty))
@@ -369,7 +381,7 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
| Csyntax.Ebuiltin ef tyargs rl ty =>
do (sl, al) <- transl_exprlist rl;
match dst with
- | For_val | For_set _ _ =>
+ | For_val | For_set _ =>
do t <- gensym ty;
ret (finish dst (sl ++ Sbuiltin (Some t) ef tyargs al :: nil)
(Etempvar t ty))
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
index 150ed76..a2b8e61 100644
--- a/cfrontend/SimplExprproof.v
+++ b/cfrontend/SimplExprproof.v
@@ -192,8 +192,8 @@ Lemma tr_simple:
match dst with
| For_val => sl = nil /\ Csyntax.typeof r = typeof a /\ eval_expr tge e le m a v
| For_effects => sl = nil
- | For_set tyl t =>
- exists b, sl = do_set t tyl b
+ | For_set sd =>
+ exists b, sl = do_set sd b
/\ Csyntax.typeof r = typeof b
/\ eval_expr tge e le m b v
end)
@@ -277,8 +277,8 @@ Lemma tr_simple_rvalue:
match dst with
| For_val => sl = nil /\ Csyntax.typeof r = typeof a /\ eval_expr tge e le m a v
| For_effects => sl = nil
- | For_set tyl t =>
- exists b, sl = do_set t tyl b
+ | For_set sd =>
+ exists b, sl = do_set sd b
/\ Csyntax.typeof r = typeof b
/\ eval_expr tge e le m b v
end.
@@ -1063,9 +1063,9 @@ Proof.
Qed.
Lemma nolabel_do_set:
- forall tmp tyl a, nolabel_list (do_set tmp tyl a).
+ forall sd a, nolabel_list (do_set sd a).
Proof.
- induction tyl; intros; simpl; split; auto; red; auto.
+ induction sd; intros; simpl; split; auto; red; auto.
Qed.
Lemma nolabel_final:
@@ -1418,8 +1418,9 @@ Proof.
apply push_seq. reflexivity. reflexivity.
rewrite <- Kseqlist_app.
eapply match_exprstates; eauto.
- apply S. apply tr_paren_set with (a1 := dummy_expr); auto. econstructor; eauto.
- apply tr_expr_monotone with tmp2; eauto. auto. auto.
+ apply S. apply tr_paren_set with (a1 := dummy_expr) (t := sd_temp sd); auto.
+ apply tr_paren_set with (a1 := a2) (t := sd_temp sd).
+ apply tr_expr_monotone with tmp2; eauto. auto. auto. auto.
(* seqand false *)
exploit tr_top_leftcontext; eauto. clear H9.
intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [R S]]]]]]]].
@@ -1527,7 +1528,8 @@ Proof.
apply push_seq. reflexivity. reflexivity.
rewrite <- Kseqlist_app.
eapply match_exprstates; eauto.
- apply S. apply tr_paren_set with (a1 := dummy_expr); auto. econstructor; eauto.
+ apply S. apply tr_paren_set with (a1 := dummy_expr) (t := sd_temp sd); auto.
+ apply tr_paren_set with (a1 := a2) (t := sd_temp sd); auto.
apply tr_expr_monotone with tmp2; eauto. auto. auto.
(* condition *)
exploit tr_top_leftcontext; eauto. clear H9.
diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v
index 1e7a84c..d063c4e 100644
--- a/cfrontend/SimplExprspec.v
+++ b/cfrontend/SimplExprspec.v
@@ -46,7 +46,7 @@ Definition final (dst: destination) (a: expr) : list statement :=
match dst with
| For_val => nil
| For_effects => nil
- | For_set tyl t => do_set t tyl a
+ | For_set sd => do_set sd a
end.
Inductive tr_rvalof: type -> expr -> list statement -> expr -> list ident -> Prop :=
@@ -78,13 +78,13 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement ->
eval_expr tge e le' m a v) ->
tr_expr le For_val (Csyntax.Eval v ty)
nil a tmp
- | tr_val_set: forall le tyl t v ty a any tmp,
+ | tr_val_set: forall le sd v ty a any tmp,
typeof a = ty ->
(forall tge e le' m,
(forall id, In id tmp -> le'!id = le!id) ->
eval_expr tge e le' m a v) ->
- tr_expr le (For_set tyl t) (Csyntax.Eval v ty)
- (do_set t tyl a) any tmp
+ tr_expr le (For_set sd) (Csyntax.Eval v ty)
+ (do_set sd a) any tmp
| tr_sizeof: forall le dst ty' ty tmp,
tr_expr le dst (Csyntax.Esizeof ty' ty)
(final dst (Esizeof ty' ty))
@@ -124,7 +124,7 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement ->
(Ecast a1 ty) tmp
| tr_seqand_val: forall le e1 e2 ty sl1 a1 tmp1 t sl2 a2 tmp2 tmp,
tr_expr le For_val e1 sl1 a1 tmp1 ->
- tr_expr le (For_set (type_bool :: ty :: nil) t) e2 sl2 a2 tmp2 ->
+ tr_expr le (For_set (sd_seqbool_val t ty)) e2 sl2 a2 tmp2 ->
list_disjoint tmp1 tmp2 ->
incl tmp1 tmp -> incl tmp2 tmp -> In t tmp ->
tr_expr le For_val (Csyntax.Eseqand e1 e2 ty)
@@ -139,18 +139,18 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement ->
tr_expr le For_effects (Csyntax.Eseqand e1 e2 ty)
(sl1 ++ makeif a1 (makeseq sl2) Sskip :: nil)
any tmp
- | tr_seqand_set: forall le tyl t e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 any tmp,
+ | tr_seqand_set: forall le sd e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 any tmp,
tr_expr le For_val e1 sl1 a1 tmp1 ->
- tr_expr le (For_set (type_bool :: ty :: tyl) t) e2 sl2 a2 tmp2 ->
+ tr_expr le (For_set (sd_seqbool_set ty sd)) e2 sl2 a2 tmp2 ->
list_disjoint tmp1 tmp2 ->
- incl tmp1 tmp -> incl tmp2 tmp -> In t tmp ->
- tr_expr le (For_set tyl t) (Csyntax.Eseqand e1 e2 ty)
+ incl tmp1 tmp -> incl tmp2 tmp -> In (sd_temp sd) tmp ->
+ tr_expr le (For_set sd) (Csyntax.Eseqand e1 e2 ty)
(sl1 ++ makeif a1 (makeseq sl2)
- (makeseq (do_set t tyl (Econst_int Int.zero ty))) :: nil)
+ (makeseq (do_set sd (Econst_int Int.zero ty))) :: nil)
any tmp
| tr_seqor_val: forall le e1 e2 ty sl1 a1 tmp1 t sl2 a2 tmp2 tmp,
tr_expr le For_val e1 sl1 a1 tmp1 ->
- tr_expr le (For_set (type_bool :: ty :: nil) t) e2 sl2 a2 tmp2 ->
+ tr_expr le (For_set (sd_seqbool_val t ty)) e2 sl2 a2 tmp2 ->
list_disjoint tmp1 tmp2 ->
incl tmp1 tmp -> incl tmp2 tmp -> In t tmp ->
tr_expr le For_val (Csyntax.Eseqor e1 e2 ty)
@@ -165,19 +165,19 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement ->
tr_expr le For_effects (Csyntax.Eseqor e1 e2 ty)
(sl1 ++ makeif a1 Sskip (makeseq sl2) :: nil)
any tmp
- | tr_seqor_set: forall le tyl t e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 any tmp,
+ | tr_seqor_set: forall le sd e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 any tmp,
tr_expr le For_val e1 sl1 a1 tmp1 ->
- tr_expr le (For_set (type_bool :: ty :: tyl) t) e2 sl2 a2 tmp2 ->
+ tr_expr le (For_set (sd_seqbool_set ty sd)) e2 sl2 a2 tmp2 ->
list_disjoint tmp1 tmp2 ->
- incl tmp1 tmp -> incl tmp2 tmp -> In t tmp ->
- tr_expr le (For_set tyl t) (Csyntax.Eseqor e1 e2 ty)
- (sl1 ++ makeif a1 (makeseq (do_set t tyl (Econst_int Int.one ty)))
+ incl tmp1 tmp -> incl tmp2 tmp -> In (sd_temp sd) tmp ->
+ tr_expr le (For_set sd) (Csyntax.Eseqor e1 e2 ty)
+ (sl1 ++ makeif a1 (makeseq (do_set sd (Econst_int Int.one ty)))
(makeseq sl2) :: nil)
any tmp
| tr_condition_val: forall le e1 e2 e3 ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 t tmp,
tr_expr le For_val e1 sl1 a1 tmp1 ->
- tr_expr le (For_set (ty::nil) t) e2 sl2 a2 tmp2 ->
- tr_expr le (For_set (ty::nil) t) e3 sl3 a3 tmp3 ->
+ tr_expr le (For_set (SDbase ty t)) e2 sl2 a2 tmp2 ->
+ tr_expr le (For_set (SDbase ty t)) e3 sl3 a3 tmp3 ->
list_disjoint tmp1 tmp2 ->
list_disjoint tmp1 tmp3 ->
incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp -> In t tmp ->
@@ -194,14 +194,14 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement ->
tr_expr le For_effects (Csyntax.Econdition e1 e2 e3 ty)
(sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil)
any tmp
- | tr_condition_set: forall le tyl t e1 e2 e3 ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 any tmp,
+ | tr_condition_set: forall le sd t e1 e2 e3 ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 any tmp,
tr_expr le For_val e1 sl1 a1 tmp1 ->
- tr_expr le (For_set (ty::tyl) t) e2 sl2 a2 tmp2 ->
- tr_expr le (For_set (ty::tyl) t) e3 sl3 a3 tmp3 ->
+ tr_expr le (For_set (SDcons ty t sd)) e2 sl2 a2 tmp2 ->
+ tr_expr le (For_set (SDcons ty t sd)) e3 sl3 a3 tmp3 ->
list_disjoint tmp1 tmp2 ->
list_disjoint tmp1 tmp3 ->
incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp -> In t tmp ->
- tr_expr le (For_set tyl t) (Csyntax.Econdition e1 e2 e3 ty)
+ 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,
@@ -305,7 +305,7 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement ->
(sl ++ Sbuiltin (Some t) ef tyargs al :: final dst (Etempvar t ty))
(Etempvar t ty) tmp
| tr_paren_val: forall le e1 ty sl1 a1 t tmp,
- tr_expr le (For_set (ty :: nil) t) e1 sl1 a1 tmp ->
+ tr_expr le (For_set (SDbase ty t)) e1 sl1 a1 tmp ->
In t tmp ->
tr_expr le For_val (Csyntax.Eparen e1 ty)
sl1
@@ -313,10 +313,10 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement ->
| tr_paren_effects: forall le e1 ty sl1 a1 tmp any,
tr_expr le For_effects e1 sl1 a1 tmp ->
tr_expr le For_effects (Csyntax.Eparen e1 ty) sl1 any tmp
- | tr_paren_set: forall le tyl t e1 ty sl1 a1 tmp any,
- tr_expr le (For_set (ty::tyl) t) e1 sl1 a1 tmp ->
+ | tr_paren_set: forall le t sd e1 ty sl1 a1 tmp any,
+ tr_expr le (For_set (SDcons ty t sd)) e1 sl1 a1 tmp ->
In t tmp ->
- tr_expr le (For_set tyl t) (Csyntax.Eparen e1 ty) sl1 any tmp
+ tr_expr le (For_set sd) (Csyntax.Eparen e1 ty) sl1 any tmp
with tr_exprlist: temp_env -> Csyntax.exprlist -> list statement -> list expr -> list ident -> Prop :=
| tr_nil: forall le tmp,
@@ -646,7 +646,7 @@ Qed.
Definition dest_below (dst: destination) (g: generator) : Prop :=
match dst with
- | For_set tyl tmp => Plt tmp g.(gen_next)
+ | For_set sd => Plt (sd_temp sd) g.(gen_next)
| _ => True
end.
@@ -656,20 +656,37 @@ Proof. intros; simpl; auto. Qed.
Remark dest_for_effect_below: forall g, dest_below For_effects g.
Proof. intros; simpl; auto. Qed.
-Lemma dest_below_notin:
- forall tyl tmp g1 g2 l,
- dest_below (For_set tyl tmp) g1 -> contained l g1 g2 -> ~In tmp l.
+Lemma dest_for_set_seqbool_val:
+ forall tmp ty g1 g2,
+ within tmp g1 g2 -> dest_below (For_set (sd_seqbool_val tmp ty)) g2.
+Proof.
+ intros. destruct H. simpl. auto.
+Qed.
+
+Lemma dest_for_set_seqbool_set:
+ forall sd ty g, dest_below (For_set sd) g -> dest_below (For_set (sd_seqbool_set ty sd)) g.
+Proof.
+ intros. assumption.
+Qed.
+
+Lemma dest_for_set_condition_val:
+ forall tmp ty g1 g2, within tmp g1 g2 -> dest_below (For_set (SDbase ty tmp)) g2.
Proof.
- simpl; intros. red in H0. red; intros. destruct (H0 _ H1).
- elim (Plt_strict tmp). apply Plt_Ple_trans with (gen_next g1); auto.
+ intros. destruct H. simpl. auto.
Qed.
-Lemma within_dest_below:
- forall tyl tmp g1 g2,
- within tmp g1 g2 -> dest_below (For_set tyl tmp) g2.
+Lemma dest_for_set_condition_set:
+ forall sd tmp ty g1 g2, dest_below (For_set sd) g2 -> within tmp g1 g2 -> dest_below (For_set (SDcons ty tmp sd)) g2.
Proof.
- intros; simpl. destruct H. tauto.
-Qed.
+ intros. destruct H0. simpl. auto.
+Qed.
+
+Lemma sd_temp_notin:
+ forall sd g1 g2 l, dest_below (For_set sd) g1 -> contained l g1 g2 -> ~In (sd_temp sd) l.
+Proof.
+ intros. simpl in H. red; intros. exploit H0; eauto. intros [A B].
+ elim (Plt_strict (sd_temp sd)). apply Plt_Ple_trans with (gen_next g1); auto.
+Qed.
Lemma dest_below_le:
forall dst g1 g2,
@@ -680,9 +697,12 @@ Qed.
Hint Resolve gensym_within within_widen contained_widen
contained_cons contained_app contained_disjoint
- contained_notin contained_nil dest_below_notin
+ contained_notin contained_nil
+ dest_for_set_seqbool_val dest_for_set_seqbool_set
+ dest_for_set_condition_val dest_for_set_condition_set
+ sd_temp_notin dest_below_le
incl_refl incl_tl incl_app incl_appl incl_appr incl_same_head
- in_eq in_cons within_dest_below dest_below_le
+ in_eq in_cons
Ple_trans Ple_refl: gensym.
Hint Resolve dest_for_val_below dest_for_effect_below.
@@ -711,16 +731,24 @@ Ltac UseFinish :=
repeat rewrite app_ass
end.
+(*
+Fixpoint add_set_dest (sd: set_destination) (tmps: list ident) :=
+ match sd with
+ | SDbase ty tmp => tmp :: tmps
+ | SDcons ty tmp sd' => tmp :: add_set_dest sd' tmps
+ end.
+*)
+
Definition add_dest (dst: destination) (tmps: list ident) :=
match dst with
- | For_set tyl t => t :: tmps
+ | For_set sd => sd_temp sd :: tmps
| _ => tmps
end.
Lemma add_dest_incl:
forall dst tmps, incl tmps (add_dest dst tmps).
Proof.
- intros. destruct dst; simpl; auto with coqlib.
+ intros. destruct dst; simpl; eauto with coqlib.
Qed.
Lemma tr_expr_add_dest:
@@ -805,7 +833,7 @@ Opaque makeif.
monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
destruct dst; monadInv EQ0.
(* for value *)
- exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
+ exploit H0; eauto with gensym. intros [tmp2 [C D]].
simpl add_dest in *.
exists (x0 :: tmp1 ++ tmp2); split.
intros; eapply tr_seqand_val; eauto with gensym.
@@ -819,7 +847,7 @@ Opaque makeif.
intros; eapply tr_seqand_effects; eauto with gensym.
apply contained_app; eauto with gensym.
(* for set *)
- exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
+ 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.
@@ -834,16 +862,16 @@ Opaque makeif.
exists (x0 :: tmp1 ++ tmp2); split.
intros; eapply tr_seqor_val; eauto with gensym.
apply list_disjoint_cons_r; eauto with gensym.
- apply contained_cons. eauto with gensym.
+ apply contained_cons. eauto with gensym.
apply contained_app; eauto with gensym.
(* for effects *)
- exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
+ 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 *)
- exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
+ 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.
@@ -853,7 +881,7 @@ Opaque makeif.
monadInv H2. exploit H; eauto. intros [tmp1 [A B]].
destruct dst; monadInv EQ0.
(* for value *)
- exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
+ exploit H0; eauto with gensym. intros [tmp2 [C D]].
exploit H1; eauto with gensym. intros [tmp3 [E F]].
simpl add_dest in *.
exists (x0 :: tmp1 ++ tmp2 ++ tmp3); split.
@@ -871,13 +899,15 @@ Opaque makeif.
intros; eapply tr_condition_effects; eauto with gensym.
apply contained_app; eauto with gensym.
(* for test *)
- exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
- exploit H1; eauto with gensym. intros [tmp3 [E F]].
+ exploit H0; eauto with gensym. intros [tmp2 [C D]].
+ exploit H1; eauto 10 with gensym. intros [tmp3 [E F]].
simpl add_dest in *.
- exists (tmp1 ++ tmp2 ++ tmp3); split.
+ exists (x0 :: tmp1 ++ tmp2 ++ tmp3); split.
intros; eapply tr_condition_set; eauto with gensym.
apply list_disjoint_cons_r; eauto with gensym.
apply list_disjoint_cons_r; eauto with gensym.
+ apply contained_cons; eauto with gensym.
+ apply contained_app; eauto with gensym.
apply contained_app; eauto with gensym.
(* sizeof *)
monadInv H. UseFinish.
@@ -901,7 +931,7 @@ Opaque makeif.
(* for set *)
exists (x1 :: tmp1 ++ tmp2); split.
repeat rewrite app_ass. simpl.
- intros. eapply tr_assign_val with (dst := For_set tyl tmp); eauto with gensym.
+ 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 *)
@@ -921,7 +951,7 @@ Opaque makeif.
(* for set *)
exists (x2 :: tmp1 ++ tmp2 ++ tmp3); split.
repeat rewrite app_ass. simpl.
- intros. eapply tr_assignop_val with (dst := For_set tyl tmp); eauto with gensym.
+ 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 *)
diff --git a/test/regression/seqops.c b/test/regression/seqops.c
index c9ee549..0e31090 100644
--- a/test/regression/seqops.c
+++ b/test/regression/seqops.c
@@ -85,3 +85,9 @@ int mixed4l(int x, int y, int z, int u) { return ((f(x) && f(y)) || f(z)) && f(u
int mixed4r(int x, int y, int z, int u) { return f(x) && (f(y) || (f(z) && f(u))); }
int mixed4b(int x, int y, int z, int u) { return (f(x) && f(y)) || (f(z) && f(u)); }
+
+/* This caused a RTL type error in CompCert 1.11 and 1.12 */
+double cond2(int x)
+{
+ return x == 0 ? 3.1415 : (x > 0 ? 1 : -1);
+}