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

1 files changed, 230 insertions, 59 deletions

diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
index 2372d02..4df5f03 100644
--- a/cfrontend/SimplExprproof.v
+++ b/cfrontend/SimplExprproof.v
@@ -68,6 +68,12 @@ Lemma varinfo_preserved:
 Proof
   (Genv.find_var_info_transf_partial transl_fundef _ TRANSL).
 
+Lemma block_is_volatile_preserved:
+  forall b, block_is_volatile tge b = block_is_volatile ge b.
+Proof.
+  intros. unfold block_is_volatile. rewrite varinfo_preserved. auto.
+Qed.
+
 Lemma type_of_fundef_preserved:
   forall f tf, transl_fundef f = OK tf ->
   type_of_fundef tf = C.type_of_fundef f.
@@ -114,7 +120,7 @@ Proof.
   rewrite H0; auto. simpl; auto.
   rewrite H0; auto. simpl; auto.
   destruct H1; congruence.
-  rewrite H0; auto. simpl; auto.
+  destruct H6. inv H1; try congruence. rewrite H0; auto. simpl; auto.
   rewrite H0; auto. simpl; auto.
   rewrite H0; auto. simpl; auto.
   destruct H7. rewrite H0; auto. rewrite H2; auto. simpl; auto.
@@ -134,6 +140,31 @@ Proof (proj2 tr_simple_nil).
 
 (** Evaluation of simple expressions and of their translation *)
 
+Remark deref_loc_preserved:
+  forall ty m b ofs t v,
+  deref_loc ge ty m b ofs t v -> deref_loc tge ty m b ofs t v.
+Proof.
+  intros. inv H. 
+  eapply deref_loc_value; eauto.
+  eapply deref_loc_volatile; eauto.
+  eapply volatile_load_preserved with (ge1 := ge); auto.
+  exact symbols_preserved. exact block_is_volatile_preserved.
+  eapply deref_loc_reference; eauto.
+  eapply deref_loc_copy; eauto.
+Qed.
+
+Remark assign_loc_preserved:
+  forall ty m b ofs v t m',
+  assign_loc ge ty m b ofs v t m' -> assign_loc tge ty m b ofs v t m'.
+Proof.
+  intros. inv H. 
+  eapply assign_loc_value; eauto.
+  eapply assign_loc_volatile; eauto.
+  eapply volatile_store_preserved with (ge1 := ge); auto.
+  exact symbols_preserved. exact block_is_volatile_preserved.
+  eapply assign_loc_copy; eauto.
+Qed.
+
 Lemma tr_simple:
  forall e m,
  (forall r v,
@@ -163,9 +194,11 @@ Opaque makeif.
   auto.
   exists a0; auto.
 (* rvalof *)
+  inv H7; try congruence. 
   exploit H0; eauto. intros [A [B C]].
   subst sl1; simpl.
-  assert (eval_expr tge e le m a v). eapply eval_Elvalue. eauto. congruence.
+  assert (eval_expr tge e le m a v).
+    eapply eval_Elvalue. eauto. congruence. rewrite <- B. eapply deref_loc_preserved; eauto. 
   destruct dst; auto.
   econstructor. split. simpl; eauto. auto. 
 (* addrof *)
@@ -346,9 +379,9 @@ Ltac TR :=
 Ltac NOTIN :=
   match goal with
   | [ H1: In ?x ?l, H2: list_disjoint ?l _ |- ~In ?x _ ] =>
-        red; intro; elim (H2 x x); auto
+        red; intro; elim (H2 x x); auto; fail
   | [ H1: In ?x ?l, H2: list_disjoint _ ?l |- ~In ?x _ ] =>
-        red; intro; elim (H2 x x); auto
+        red; intro; elim (H2 x x); auto; fail
   end.
 
 Ltac UNCHANGED :=
@@ -377,8 +410,9 @@ Ltac UNCHANGED :=
 (* rvalof *)
   inv H1.
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
-  TR. subst sl1; rewrite app_ass; eauto. auto. 
-  intros. rewrite <- app_ass; econstructor; eauto.
+  TR. subst sl1; rewrite app_ass; eauto. red; eauto. 
+  intros. rewrite <- app_ass; econstructor; eauto. 
+  exploit typeof_context; eauto. congruence.
 (* addrof *)
   inv H1. 
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
@@ -475,15 +509,16 @@ Ltac UNCHANGED :=
   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.
+  eapply tr_expr_invariant; eauto. UNCHANGED. 
+  symmetry; eapply typeof_context; eauto. eauto.  
+  auto. auto. auto. auto. auto. auto.
   (* for val *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [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. auto. auto. auto.
+  eapply tr_expr_invariant; eauto. UNCHANGED. 
+  eauto. auto. auto. auto. auto. auto. auto. auto. auto. auto. auto. 
   eapply typeof_context; eauto.
 (* assignop right *)
   inv H2.
@@ -492,25 +527,24 @@ Ltac UNCHANGED :=
   exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
   TR. subst sl2. rewrite app_ass. eauto. 
   red; auto.
-  intros. rewrite <- app_ass. change (sl3 ++ sl2') with (nil ++ sl3 ++ sl2'). rewrite app_ass. econstructor. 
+  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. auto. auto.
+  apply S; auto. auto. eauto. auto. auto. auto. auto. auto. auto. 
   (* 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 [U [R S]]]]]]]]].
   TR. subst sl2. rewrite app_ass. eauto. 
   red; auto. 
-  intros. rewrite <- app_ass. change (sl3 ++ sl2') with (nil ++ sl3 ++ sl2'). rewrite app_ass. econstructor. 
+  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. auto. auto. auto. auto. auto. auto. 
+  apply S; auto. eauto. auto. auto. auto. auto. auto. auto. auto. auto. auto. auto. auto. 
 (* postincr *)
   inv H1.
   (* for effects *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
   TR. rewrite Q; rewrite app_ass; eauto. red; auto. 
-  intros. replace (C.typeof (C e)) with (C.typeof (C e')). rewrite <- app_ass.
-  econstructor; eauto. 
-  eapply typeof_context; eauto.
+  intros. rewrite <- app_ass. econstructor; eauto. 
+  symmetry; eapply typeof_context; eauto. 
   (* for val *)
   exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
   TR. rewrite Q; rewrite app_ass; eauto. red; auto. 
@@ -706,7 +740,20 @@ Proof.
   apply star_one. eapply step_ifthenelse; eauto. 
 Qed.
 
-(** Matching between continuations *)
+Lemma step_make_set:
+  forall id a ty m b ofs t v e le f k,
+  deref_loc ge ty m b ofs t v ->
+  eval_lvalue tge e le m a b ofs ->
+  typeof a = ty ->
+  step tge (State f (make_set id a) k e le m)
+         t (State f Sskip k e (PTree.set id v le) m).
+Proof.
+  intros. exploit deref_loc_preserved; eauto. rewrite <- H1. intros DEREF.
+  unfold make_set. destruct (type_is_volatile (typeof a)) as []_eqn.
+  econstructor; eauto.
+  assert (t = E0). inv H; congruence. subst t.
+  constructor. eapply eval_Elvalue; eauto.
+Qed. 
 
 Fixpoint Kseqlist (sl: list statement) (k: cont) :=
   match sl with
@@ -721,6 +768,40 @@ Proof.
   induction sl1; simpl; congruence.
 Qed.
 
+(*
+Axiom only_scalar_types_volatile:
+  forall ty, type_is_volatile ty = true -> exists chunk, access_mode ty = By_value chunk.
+*)
+
+Lemma step_tr_rvalof:
+  forall ty m b ofs t v e le a sl a' tmp f k,
+  deref_loc ge ty m b ofs t v ->
+  eval_lvalue tge e le m a b ofs ->
+  tr_rvalof ty a sl a' tmp ->
+  typeof a = ty ->
+  exists le',
+    star step tge (State f Sskip (Kseqlist sl k) e le m)
+               t (State f Sskip k e le' m)
+  /\ eval_expr tge e le' m a' v
+  /\ typeof a' = typeof a
+  /\ forall x, ~In x tmp -> le'!x = le!x.
+Proof.
+  intros. inv H1. 
+  (* non volatile *)
+  assert (t = E0). inv H; auto. congruence. subst t.  
+  exists le; intuition. apply star_refl.
+  eapply eval_Elvalue; eauto. eapply deref_loc_preserved; eauto.
+  (* volatile *)
+  exists (PTree.set t0 v le); intuition.
+  simpl. eapply star_two. econstructor. eapply step_vol_read; eauto. 
+  eapply deref_loc_preserved; eauto. traceEq.
+  constructor. apply PTree.gss.
+  apply PTree.gso. congruence. 
+Qed.
+
+(** Matching between continuations *)
+
+
 Inductive match_cont : Csem.cont -> cont -> Prop :=
   | match_Kstop:
       match_cont Csem.Kstop Kstop
@@ -853,7 +934,9 @@ Inductive match_states: Csem.state -> state -> Prop :=
   | match_returnstates: forall res k m tk,
       match_cont k tk ->
       match_states (Csem.Returnstate res k m)
-                   (Returnstate res tk m).
+                   (Returnstate res tk m)
+  | match_stuckstate: forall S,
+      match_states Csem.Stuckstate S.
 
 Lemma push_seq:
   forall f sl k e le m,
@@ -931,6 +1014,12 @@ Proof.
   red; simpl; intros. rewrite H; auto.
 Qed.
 
+Lemma tr_rvalof_nolabel:
+  forall ty a sl a' tmp, tr_rvalof ty a sl a' tmp -> nolabel_list sl.
+Proof.
+  destruct 1; simpl; intuition. red; simpl; auto.
+Qed.
+
 Definition nolabel_dest (dst: destination) : Prop :=
   match dst with
   | For_val => True
@@ -970,13 +1059,18 @@ Lemma tr_find_label_expr:
 /\(forall le rl sl al tmps, tr_exprlist le rl sl al tmps -> nolabel_list sl).
 Proof.
   apply tr_expr_exprlist; intros; NoLabelTac.
-  destruct H1. apply makeif_nolabel; auto. 
+  destruct H1. apply makeif_nolabel; auto.
+  eapply tr_rvalof_nolabel; eauto.
   apply makeif_nolabel; NoLabelTac.
   rewrite (makeseq_nolabel sl2); auto.
   rewrite (makeseq_nolabel sl3); auto.
   apply makeif_nolabel; NoLabelTac.
   rewrite (makeseq_nolabel sl2). auto. apply H3. apply nolabel_dest_cast; auto. 
   rewrite (makeseq_nolabel sl3). auto. apply H5. apply nolabel_dest_cast; auto.
+  eapply tr_rvalof_nolabel; eauto.
+  eapply tr_rvalof_nolabel; eauto.
+  eapply tr_rvalof_nolabel; eauto.
+  unfold make_set. destruct (type_is_volatile (typeof a1)); auto.
   apply nolabel_dest_cast; auto.
 Qed.
 
@@ -1234,7 +1328,19 @@ Proof.
   exploit tr_simple_rvalue; eauto. destruct dest.
   intros [A [B C]]. subst sl. apply tr_top_val_val; auto.
   intros A. subst sl. apply tr_top_base. constructor. 
-  intros [b [A [B C]]]. subst sl. apply tr_top_val_test; auto. 
+  intros [b [A [B C]]]. subst sl. apply tr_top_val_test; auto.
+(* rval volatile *)
+  exploit tr_top_leftcontext; eauto. clear H11.
+  intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]].
+  inv P. inv H2. inv H7; try congruence. 
+  exploit tr_simple_lvalue; eauto. intros [SL [TY EV]]. subst sl0; simpl.
+  econstructor; split.
+  left. eapply plus_two. constructor. eapply step_vol_read; eauto. 
+  rewrite <- TY. eapply deref_loc_preserved; eauto. congruence. auto.
+  econstructor; eauto. change (final dst' (Etempvar t0 (C.typeof l)) ++ sl2) with (nil ++ (final dst' (Etempvar t0 (C.typeof l)) ++ sl2)).
+  apply S. apply tr_val_gen. auto. intros. constructor. rewrite H5; auto. apply PTree.gss.
+  intros. apply PTree.gso. red; intros; subst; elim H5; auto. 
+  auto.
 (* condition true *)
   exploit tr_top_leftcontext; eauto. clear H9. 
   intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]].
@@ -1297,14 +1403,14 @@ Proof.
   left. eapply plus_left. constructor.
   apply star_one. econstructor; eauto.
   rewrite <- TY1; rewrite <- TY2; eauto.
-  rewrite <- TY1; eauto.
+  rewrite <- TY1. eapply assign_loc_preserved; eauto.
   traceEq.
   econstructor. auto. change sl2 with (nil ++ sl2). apply S.
   constructor. auto. auto. auto.
   (* for value *)
   exploit tr_simple_rvalue; eauto. intros [SL2 [TY2 EV2]].
   exploit tr_simple_lvalue. eauto.
-    eapply tr_expr_invariant with (le' := PTree.set t v le). eauto. 
+    eapply tr_expr_invariant with (le' := PTree.set t0 v le). eauto. 
     intros. apply PTree.gso. intuition congruence.
   intros [SL1 [TY1 EV1]].
   subst; simpl Kseqlist.
@@ -1314,7 +1420,7 @@ Proof.
   eapply star_left. constructor.
   apply star_one. econstructor; eauto. constructor. apply PTree.gss.
   simpl. rewrite <- TY1; eauto.
-  rewrite <- TY1; eauto.
+  rewrite <- TY1. eapply assign_loc_preserved; eauto.
   reflexivity. reflexivity. traceEq.
   econstructor. auto. apply S.
   apply tr_val_gen. auto. intros. econstructor; eauto. constructor. 
@@ -1322,62 +1428,100 @@ Proof.
   intros. apply PTree.gso. intuition congruence.
   auto. auto.
 (* assignop *)
-  exploit tr_top_leftcontext; eauto. clear H14. 
+  exploit tr_top_leftcontext; eauto. clear H15. 
   intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]].
   inv P. inv H6.
   (* for effects *)
-  exploit tr_simple_rvalue; eauto. intros [SL2 [TY2 EV2]].
   exploit tr_simple_lvalue; eauto. intros [SL1 [TY1 EV1]].
-  subst; simpl Kseqlist.
+  exploit step_tr_rvalof; eauto. intros [le' [EXEC [EV3 [TY3 INV]]]].
+  exploit tr_simple_lvalue. eauto. eapply tr_expr_invariant with (le := le) (le' := le'). eauto. 
+  intros. apply INV. NOTIN. intros [? [? EV1']].
+  exploit tr_simple_rvalue. eauto. eapply tr_expr_invariant with (le := le) (le' := le'). eauto. 
+  intros. apply INV. NOTIN. simpl. intros [SL2 [TY2 EV2]].
+  subst; simpl Kseqlist. 
   econstructor; split.
-  left. eapply plus_left. constructor.
-  apply star_one. econstructor; eauto.
-    econstructor; eauto. eapply eval_Elvalue; eauto. rewrite <- TY1; eauto. 
-    rewrite <- TY1; rewrite <- TY2; eauto.
+  left. eapply star_plus_trans. rewrite app_ass. rewrite Kseqlist_app. eexact EXEC.
+  eapply plus_two. simpl. econstructor. econstructor. eexact EV1'. 
+    econstructor. eexact EV3. eexact EV2. 
+    rewrite TY3; rewrite <- TY1; rewrite <- TY2; eauto.
     rewrite <- TY1; eauto.
-    rewrite <- TY1; eauto.
-  traceEq.
+    rewrite <- TY1. eapply assign_loc_preserved; eauto.
+  reflexivity. traceEq.
   econstructor. auto. change sl2 with (nil ++ sl2). apply S.
   constructor. auto. auto. auto.
   (* for value *)
-  exploit tr_simple_rvalue; eauto. intros [SL2 [TY2 EV2]].
   exploit tr_simple_lvalue; eauto. intros [SL1 [TY1 EV1]].
-  exploit tr_simple_lvalue. eauto.
-    eapply tr_expr_invariant with (le' := PTree.set t v3 le). eauto. 
-    intros. apply PTree.gso. intuition congruence.
-  intros [SL3 [TY3 EV3]]. 
+  exploit step_tr_rvalof; eauto. intros [le' [EXEC [EV3 [TY3 INV]]]].
+  exploit tr_simple_lvalue. eauto. eapply tr_expr_invariant with (le := le) (le' := le'). eauto. 
+  intros. apply INV. NOTIN. intros [? [? EV1']].
+  exploit tr_simple_rvalue. eauto. eapply tr_expr_invariant with (le := le) (le' := le'). eauto. 
+  intros. apply INV. NOTIN. simpl. intros [SL2 [TY2 EV2]].
+  exploit tr_simple_lvalue. eauto. 
+    eapply tr_expr_invariant with (le := le) (le' := PTree.set t v3 le'). eauto. 
+    intros. rewrite PTree.gso. apply INV. NOTIN. intuition congruence.
+  intros [? [? EV1'']].
   subst; simpl Kseqlist.
   econstructor; split.
-  left. eapply plus_left. constructor. 
-  eapply star_left. constructor.
-    econstructor. eapply eval_Elvalue; eauto. rewrite <- TY1; eauto. eauto.
-    rewrite <- TY1; rewrite <- TY2. eauto. 
-  eapply star_left. constructor.
-  apply star_one. econstructor. eauto. constructor. apply PTree.gss. 
-    rewrite <- TY1. eauto. rewrite <- TY1. eauto.
-  reflexivity. reflexivity. traceEq.
+  left. rewrite app_ass. rewrite Kseqlist_app. 
+  eapply star_plus_trans. eexact EXEC.
+  simpl. eapply plus_four. econstructor. econstructor.
+    econstructor. eexact EV3. eexact EV2. 
+    rewrite TY3; rewrite <- TY1; rewrite <- TY2. eauto.
+  econstructor. econstructor.
+    eexact EV1''. constructor. apply PTree.gss. 
+    simpl. rewrite <- TY1; eauto.
+    rewrite <- TY1. eapply assign_loc_preserved; eauto. 
+  reflexivity. traceEq.
   econstructor. auto. apply S.
   apply tr_val_gen. auto. intros. econstructor; eauto. constructor. 
-  rewrite H6; auto. apply PTree.gss. 
-  intros. apply PTree.gso. intuition congruence.
+  rewrite H10; auto. apply PTree.gss. 
+  intros. rewrite PTree.gso. apply INV. 
+  red; intros; elim H10; auto. 
+  intuition congruence.
   auto. auto.
+(* assignop stuck *)
+  exploit tr_top_leftcontext; eauto. clear H12. 
+  intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]].
+  inv P. inv H4.
+  (* for effects *)
+  exploit tr_simple_lvalue; eauto. intros [SL1 [TY1 EV1]].
+  exploit tr_simple_rvalue; eauto. intros [SL2 [TY2 EV2]].
+  exploit step_tr_rvalof; eauto. intros [le' [EXEC [EV3 [TY3 INV]]]].
+  subst; simpl Kseqlist. 
+  econstructor; split.
+  right; split. rewrite app_ass. rewrite Kseqlist_app. eexact EXEC. 
+  simpl. omega.
+  constructor.
+  (* for value *)
+  exploit tr_simple_lvalue; eauto. intros [SL1 [TY1 EV1]].
+  exploit tr_simple_rvalue; eauto. intros [SL2 [TY2 EV2]].
+  exploit step_tr_rvalof; eauto. intros [le' [EXEC [EV3 [TY3 INV]]]].
+  subst; simpl Kseqlist. 
+  econstructor; split.
+  right; split. rewrite app_ass. rewrite Kseqlist_app. eexact EXEC. 
+  simpl. omega.
+  constructor.
 (* postincr *)
-  exploit tr_top_leftcontext; eauto. clear H13. 
+  exploit tr_top_leftcontext; eauto. clear H14. 
   intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]].
   inv P. inv H5.
   (* for effects *)
   exploit tr_simple_lvalue; eauto. intros [SL1 [TY1 EV1]].
-  assert (EV2: eval_expr tge e le m a1 v1). eapply eval_Elvalue; eauto. rewrite <- TY1; auto.
+  exploit step_tr_rvalof; eauto. intros [le' [EXEC [EV3 [TY3 INV]]]].
+  exploit tr_simple_lvalue. eauto. eapply tr_expr_invariant with (le := le) (le' := le'). eauto. 
+  intros. apply INV. NOTIN. intros [? [? EV1']].
   subst; simpl Kseqlist.
   econstructor; split.
-  left. eapply plus_two. constructor.
+  left. rewrite app_ass; rewrite Kseqlist_app. 
+  eapply star_plus_trans. eexact EXEC. 
+  eapply plus_two. simpl. constructor.
   econstructor; eauto.
   unfold transl_incrdecr. destruct id; simpl in H2. 
-  econstructor. eauto. constructor. simpl. rewrite <- TY1. eauto.
-  econstructor. eauto. constructor. simpl. rewrite <- TY1. eauto.
+  econstructor. eauto. constructor. simpl. rewrite TY3; rewrite <- TY1. eauto.
+  econstructor. eauto. constructor. simpl. rewrite TY3; rewrite <- TY1. eauto.
   rewrite <- TY1. instantiate (1 := v3). destruct id; auto. 
-  rewrite <- TY1. eauto. 
-  traceEq.
+  rewrite <- TY1. eapply assign_loc_preserved; eauto. 
+  reflexivity. traceEq.
   econstructor. auto. change sl2 with (nil ++ sl2). apply S.
   constructor. auto. auto. auto.
   (* for value *)
@@ -1388,21 +1532,40 @@ Proof.
   intros [SL2 [TY2 EV2]].
   subst; simpl Kseqlist.
   econstructor; split.
-  left. eapply plus_four. constructor. 
-  constructor. eapply eval_Elvalue; eauto. rewrite <- TY1; eauto.
+  left. eapply plus_four. constructor.
+  eapply step_make_set; eauto. 
   constructor.
   econstructor. eauto. 
   unfold transl_incrdecr. destruct id; simpl in H2. 
   econstructor. constructor. apply PTree.gss. constructor. simpl. eauto.
   econstructor. constructor. apply PTree.gss. constructor. simpl. eauto.
   rewrite <- TY1. instantiate (1 := v3). destruct id; auto. 
-  rewrite <- TY1. eauto. 
+  rewrite <- TY1. eapply assign_loc_preserved; eauto. 
   traceEq.
   econstructor. auto. apply S.
   apply tr_val_gen. auto. intros. econstructor; eauto.
   rewrite H5; auto. apply PTree.gss. 
   intros. apply PTree.gso. intuition congruence.
   auto. auto.
+(* postincr stuck *)
+  exploit tr_top_leftcontext; eauto. clear H11. 
+  intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]].
+  inv P. inv H3.
+  (* for effects *)
+  exploit tr_simple_lvalue; eauto. intros [SL1 [TY1 EV1]].
+  exploit step_tr_rvalof; eauto. intros [le' [EXEC [EV3 [TY3 INV]]]].
+  subst. simpl Kseqlist. 
+  econstructor; split.
+  right; split. rewrite app_ass; rewrite Kseqlist_app. eexact EXEC.
+  simpl; omega.
+  constructor.
+  (* for value *)
+  exploit tr_simple_lvalue; eauto. intros [SL1 [TY1 EV1]].
+  subst. simpl Kseqlist. 
+  econstructor; split.
+  left. eapply plus_two. constructor. eapply step_make_set; eauto. 
+  traceEq.
+  constructor.
 (* comma *)
   exploit tr_top_leftcontext; eauto. clear H9. 
   intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]].
@@ -1510,6 +1673,14 @@ Proof.
   inv H0. exists a0; auto.
 Qed.
 
+Lemma bind_parameters_preserved:
+  forall e m params args m',
+  bind_parameters ge e m params args m' ->
+  bind_parameters tge e m params args m'.
+Proof.
+  induction 1; econstructor; eauto. eapply assign_loc_preserved; eauto.
+Qed.
+
 Lemma sstep_simulation:
   forall S1 t S2, Csem.sstep ge S1 t S2 ->
   forall S1' (MS: match_states S1 S1'),
@@ -1766,7 +1937,7 @@ Proof.
   left; apply plus_one. eapply step_internal_function. 
   rewrite C; rewrite D; auto.
   rewrite C; rewrite D; eauto.
-  rewrite C; eauto.
+  rewrite C. eapply bind_parameters_preserved; eauto.
   constructor; auto. 
 
 (* external function *)