From 93b89122000e42ac57abc39734fdf05d3a89e83c Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 15 Jul 2011 08:26:16 +0000
Subject: Merge of branch new-semantics: revised and strengthened top-level
 statements of semantic preservation.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1683 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 ia32/Asm.v         | 67 ++++++++++++++++++++++++++++++++++++++++++++++++++++--
 ia32/Asmgenproof.v |  7 +++---
 2 files changed, 68 insertions(+), 6 deletions(-)

(limited to 'ia32')

diff --git a/ia32/Asm.v b/ia32/Asm.v
index f3809c4..ebb22a6 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -788,6 +788,69 @@ Inductive final_state: state -> int -> Prop :=
       rs#EAX = Vint r ->
       final_state (State rs m) r.
       
-Definition exec_program (p: program) (beh: program_behavior) : Prop :=
-  program_behaves step (initial_state p) final_state (Genv.globalenv p) beh.
+Definition semantics (p: program) :=
+  Semantics step (initial_state p) final_state (Genv.globalenv p).
 
+(** Determinacy of the [Asm] semantics. *)
+
+Remark extcall_arguments_determ:
+  forall rs m sg args1 args2,
+  extcall_arguments rs m sg args1 -> extcall_arguments rs m sg args2 -> args1 = args2.
+Proof.
+  intros until m.
+  assert (forall ll vl1, list_forall2 (extcall_arg rs m) ll vl1 ->
+          forall vl2, list_forall2 (extcall_arg rs m) ll vl2 -> vl1 = vl2).
+    induction 1; intros vl2 EA; inv EA.
+    auto.
+    f_equal; auto. 
+    inv H; inv H3; congruence.
+  intros. red in H0; red in H1. eauto. 
+Qed.
+
+Remark annot_arguments_determ:
+  forall rs m params args1 args2,
+  annot_arguments rs m params args1 -> annot_arguments rs m params args2 -> args1 = args2.
+Proof.
+  unfold annot_arguments. intros. revert params args1 H args2 H0. 
+  induction 1; intros. 
+  inv H0; auto.
+  inv H1. decEq; eauto. inv H; inv H4. auto. congruence. 
+Qed.
+
+Lemma semantics_determinate: forall p, determinate (semantics p).
+Proof.
+Ltac Equalities :=
+  match goal with
+  | [ H1: ?a = ?b, H2: ?a = ?c |- _ ] =>
+      rewrite H1 in H2; inv H2; Equalities
+  | _ => idtac
+  end.
+  intros; constructor; simpl; intros.
+(* determ *)
+  inv H; inv H0; Equalities.
+  split. constructor. auto.
+  discriminate.
+  discriminate.
+  inv H11. 
+  exploit external_call_determ. eexact H4. eexact H11. intros [A B].
+  split. auto. intros. destruct B; auto. subst. auto.
+  inv H12.
+  assert (vargs0 = vargs) by (eapply annot_arguments_determ; eauto). subst vargs0.
+  exploit external_call_determ. eexact H5. eexact H13. intros [A B].
+  split. auto. intros. destruct B; auto. subst. auto.
+  assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0.
+  exploit external_call_determ. eexact H3. eexact H8. intros [A B].
+  split. auto. intros. destruct B; auto. subst. auto.
+(* trace length *)
+  inv H; simpl.
+  omega.
+  eapply external_call_trace_length; eauto.
+  eapply external_call_trace_length; eauto.
+  eapply external_call_trace_length; eauto.
+(* initial states *)
+  inv H; inv H0. f_equal. congruence.
+(* final no step *)
+  inv H. unfold Vzero in H0. red; intros; red; intros. inv H; congruence.
+(* final states *)
+  inv H; inv H0. congruence.
+Qed.
diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v
index a9b9f3b..d049737 100644
--- a/ia32/Asmgenproof.v
+++ b/ia32/Asmgenproof.v
@@ -1294,11 +1294,10 @@ Proof.
 Qed.
 
 Theorem transf_program_correct:
-  forall (beh: program_behavior), not_wrong beh ->
-  Machsem.exec_program prog beh -> Asm.exec_program tprog beh.
+  forward_simulation (Machsem.semantics prog) (Asm.semantics tprog).
 Proof.
-  unfold Machsem.exec_program, Asm.exec_program; intros.
-  eapply simulation_star_preservation with (measure := measure); eauto.
+  eapply forward_simulation_star with (measure := measure).
+  eexact symbols_preserved.
   eexact transf_initial_states.
   eexact transf_final_states.
   exact transf_instr_correct. 
-- 
cgit v1.2.3