Restored the big-step semantics for Cminor

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1287 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 125 insertions, 125 deletions

diff --git a/backend/Cminor.v b/backend/Cminor.v
index 094bef7..f2f03c5 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -536,9 +536,11 @@ Definition exec_program (p: program) (beh: program_behavior) : Prop :=
 
 (** * Alternate operational semantics (big-step) *)
 
-(** In big-step style, just like expressions evaluate to values, 
-    statements evaluate to``outcomes'' indicating how execution should
-    proceed afterwards. *)
+(** We now define another semantics for Cminor without [goto] that follows
+  the ``big-step'' style of semantics, also known as natural semantics.
+  In this style, just like expressions evaluate to values, 
+  statements evaluate to``outcomes'' indicating how execution should
+  proceed afterwards. *)
 
 Inductive outcome: Type :=
   | Out_normal: outcome                (**r continue in sequence *)
@@ -570,10 +572,6 @@ Definition outcome_free_mem
   | _ => Mem.free m sp 0 sz = Some m'
   end.
 
-(***** REVISE - PROBLEMS WITH free *)
-
-(******************************
-
 Section NATURALSEM.
 
 Variable ge: genv.
@@ -591,7 +589,7 @@ Inductive eval_funcall:
       forall m f vargs m1 sp e t e2 m2 out vres m3,
       Mem.alloc m 0 f.(fn_stackspace) = (m1, sp) ->
       set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e ->
-      exec_stmt (Vptr sp Int.zero) e m1 f.(fn_body) t e2 m2 out ->
+      exec_stmt f (Vptr sp Int.zero) e m1 f.(fn_body) t e2 m2 out ->
       outcome_result_value out f.(fn_sig).(sig_res) vres ->
       outcome_free_mem out m2 sp f.(fn_stackspace) m3 ->
       eval_funcall m (Internal f) vargs t m3 vres
@@ -600,7 +598,7 @@ Inductive eval_funcall:
       external_call ef args m t res m' ->
       eval_funcall m (External ef) args t m' res
 
-(** Execution of a statement: [exec_stmt ge sp e m s t e' m' out]
+(** Execution of a statement: [exec_stmt ge f sp e m s t e' m' out]
   means that statement [s] executes with outcome [out].
   [e] is the initial environment and [m] is the initial memory state.
   [e'] is the final environment, reflecting variable assignments performed
@@ -609,89 +607,103 @@ Inductive eval_funcall:
   the execution.  The other parameters are as in [eval_expr]. *)
 
 with exec_stmt:
-         val ->
+         function -> val ->
          env -> mem -> stmt -> trace ->
          env -> mem -> outcome -> Prop :=
   | exec_Sskip:
-      forall sp e m,
-      exec_stmt sp e m Sskip E0 e m Out_normal
+      forall f sp e m,
+      exec_stmt f sp e m Sskip E0 e m Out_normal
   | exec_Sassign:
-      forall sp e m id a v,
+      forall f sp e m id a v,
       eval_expr ge sp e m a v ->
-      exec_stmt sp e m (Sassign id a) E0 (PTree.set id v e) m Out_normal
+      exec_stmt f sp e m (Sassign id a) E0 (PTree.set id v e) m Out_normal
   | exec_Sstore:
-      forall sp e m chunk addr a vaddr v m',
+      forall f sp e m chunk addr a vaddr v m',
       eval_expr ge sp e m addr vaddr ->
       eval_expr ge sp e m a v ->
       Mem.storev chunk m vaddr v = Some m' ->
-      exec_stmt sp e m (Sstore chunk addr a) E0 e m' Out_normal
+      exec_stmt f sp e m (Sstore chunk addr a) E0 e m' Out_normal
   | exec_Scall:
-      forall sp e m optid sig a bl vf vargs f t m' vres e',
+      forall f sp e m optid sig a bl vf vargs fd t m' vres e',
       eval_expr ge sp e m a vf ->
       eval_exprlist ge sp e m bl vargs ->
-      Genv.find_funct ge vf = Some f ->
-      funsig f = sig ->
-      eval_funcall m f vargs t m' vres ->
+      Genv.find_funct ge vf = Some fd ->
+      funsig fd = sig ->
+      eval_funcall m fd vargs t m' vres ->
       e' = set_optvar optid vres e ->
-      exec_stmt sp e m (Scall optid sig a bl) t e' m' Out_normal
+      exec_stmt f sp e m (Scall optid sig a bl) t e' m' Out_normal
   | exec_Sifthenelse:
-      forall sp e m a s1 s2 v b t e' m' out,
+      forall f sp e m a s1 s2 v b t e' m' out,
       eval_expr ge sp e m a v ->
       Val.bool_of_val v b ->
-      exec_stmt sp e m (if b then s1 else s2) t e' m' out ->
-      exec_stmt sp e m (Sifthenelse a s1 s2) t e' m' out
+      exec_stmt f sp e m (if b then s1 else s2) t e' m' out ->
+      exec_stmt f sp e m (Sifthenelse a s1 s2) t e' m' out
   | exec_Sseq_continue:
-      forall sp e m t s1 t1 e1 m1 s2 t2 e2 m2 out,
-      exec_stmt sp e m s1 t1 e1 m1 Out_normal ->
-      exec_stmt sp e1 m1 s2 t2 e2 m2 out ->
+      forall f sp e m t s1 t1 e1 m1 s2 t2 e2 m2 out,
+      exec_stmt f sp e m s1 t1 e1 m1 Out_normal ->
+      exec_stmt f sp e1 m1 s2 t2 e2 m2 out ->
       t = t1 ** t2 ->
-      exec_stmt sp e m (Sseq s1 s2) t e2 m2 out
+      exec_stmt f sp e m (Sseq s1 s2) t e2 m2 out
   | exec_Sseq_stop:
-      forall sp e m t s1 s2 e1 m1 out,
-      exec_stmt sp e m s1 t e1 m1 out ->
+      forall f sp e m t s1 s2 e1 m1 out,
+      exec_stmt f sp e m s1 t e1 m1 out ->
       out <> Out_normal ->
-      exec_stmt sp e m (Sseq s1 s2) t e1 m1 out
+      exec_stmt f sp e m (Sseq s1 s2) t e1 m1 out
   | exec_Sloop_loop:
-      forall sp e m s t t1 e1 m1 t2 e2 m2 out,
-      exec_stmt sp e m s t1 e1 m1 Out_normal ->
-      exec_stmt sp e1 m1 (Sloop s) t2 e2 m2 out ->
+      forall f sp e m s t t1 e1 m1 t2 e2 m2 out,
+      exec_stmt f sp e m s t1 e1 m1 Out_normal ->
+      exec_stmt f sp e1 m1 (Sloop s) t2 e2 m2 out ->
       t = t1 ** t2 ->
-      exec_stmt sp e m (Sloop s) t e2 m2 out
+      exec_stmt f sp e m (Sloop s) t e2 m2 out
   | exec_Sloop_stop:
-      forall sp e m t s e1 m1 out,
-      exec_stmt sp e m s t e1 m1 out ->
+      forall f sp e m t s e1 m1 out,
+      exec_stmt f sp e m s t e1 m1 out ->
       out <> Out_normal ->
-      exec_stmt sp e m (Sloop s) t e1 m1 out
+      exec_stmt f sp e m (Sloop s) t e1 m1 out
   | exec_Sblock:
-      forall sp e m s t e1 m1 out,
-      exec_stmt sp e m s t e1 m1 out ->
-      exec_stmt sp e m (Sblock s) t e1 m1 (outcome_block out)
+      forall f sp e m s t e1 m1 out,
+      exec_stmt f sp e m s t e1 m1 out ->
+      exec_stmt f sp e m (Sblock s) t e1 m1 (outcome_block out)
   | exec_Sexit:
-      forall sp e m n,
-      exec_stmt sp e m (Sexit n) E0 e m (Out_exit n)
+      forall f sp e m n,
+      exec_stmt f sp e m (Sexit n) E0 e m (Out_exit n)
   | exec_Sswitch:
-      forall sp e m a cases default n,
+      forall f sp e m a cases default n,
       eval_expr ge sp e m a (Vint n) ->
-      exec_stmt sp e m (Sswitch a cases default)
+      exec_stmt f sp e m (Sswitch a cases default)
                 E0 e m (Out_exit (switch_target n default cases))
   | exec_Sreturn_none:
-      forall sp e m,
-      exec_stmt sp e m (Sreturn None) E0 e m (Out_return None)
+      forall f sp e m,
+      exec_stmt f sp e m (Sreturn None) E0 e m (Out_return None)
   | exec_Sreturn_some:
-      forall sp e m a v,
+      forall f sp e m a v,
       eval_expr ge sp e m a v ->
-      exec_stmt sp e m (Sreturn (Some a)) E0 e m (Out_return (Some v))
+      exec_stmt f sp e m (Sreturn (Some a)) E0 e m (Out_return (Some v))
   | exec_Stailcall:
-      forall sp e m sig a bl vf vargs f t m' vres,
+      forall f sp e m sig a bl vf vargs fd t m' m'' vres,
       eval_expr ge (Vptr sp Int.zero) e m a vf ->
       eval_exprlist ge (Vptr sp Int.zero) e m bl vargs ->
-      Genv.find_funct ge vf = Some f ->
-      funsig f = sig ->
-      eval_funcall (Mem.free m sp) f vargs t m' vres ->
-      exec_stmt (Vptr sp Int.zero) e m (Stailcall sig a bl) t e m' (Out_tailcall_return vres).
+      Genv.find_funct ge vf = Some fd ->
+      funsig fd = sig ->
+      Mem.free m sp 0 f.(fn_stackspace) = Some m' ->
+      eval_funcall m' fd vargs t m'' vres ->
+      exec_stmt f (Vptr sp Int.zero) e m (Stailcall sig a bl) t e m'' (Out_tailcall_return vres).
 
 Scheme eval_funcall_ind2 := Minimality for eval_funcall Sort Prop
   with exec_stmt_ind2 := Minimality for exec_stmt Sort Prop.
+Combined Scheme eval_funcall_exec_stmt_ind2 
+  from eval_funcall_ind2, exec_stmt_ind2.
+
+(*
+Definition eval_funcall_exec_stmt_ind2 
+  (P1: mem -> fundef -> list val -> trace -> mem -> val -> Prop)
+  (P2: val -> env -> mem -> stmt -> trace ->
+              env -> mem -> outcome -> Prop) :=
+  fun a b c d e f g h i j k l m n o p q =>
+  conj
+    (eval_funcall_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q)
+    (exec_stmt_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q).
+*)
 
 (** Coinductive semantics for divergence.
   [evalinf_funcall ge m f args t]
@@ -706,7 +718,7 @@ CoInductive evalinf_funcall:
       forall m f vargs m1 sp e t,
       Mem.alloc m 0 f.(fn_stackspace) = (m1, sp) ->
       set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e ->
-      execinf_stmt (Vptr sp Int.zero) e m1 f.(fn_body) t ->
+      execinf_stmt f (Vptr sp Int.zero) e m1 f.(fn_body) t ->
       evalinf_funcall m (Internal f) vargs t
 
 (** [execinf_stmt ge sp e m s t] means that statement [s] diverges.
@@ -714,53 +726,54 @@ CoInductive evalinf_funcall:
   and [t] the trace of observable events performed during the execution. *)
 
 with execinf_stmt:
-         val -> env -> mem -> stmt -> traceinf -> Prop :=
+         function -> val -> env -> mem -> stmt -> traceinf -> Prop :=
   | execinf_Scall:
-      forall sp e m optid sig a bl vf vargs f t,
+      forall f sp e m optid sig a bl vf vargs fd t,
       eval_expr ge sp e m a vf ->
       eval_exprlist ge sp e m bl vargs ->
-      Genv.find_funct ge vf = Some f ->
-      funsig f = sig ->
-      evalinf_funcall m f vargs t ->
-      execinf_stmt sp e m (Scall optid sig a bl) t
+      Genv.find_funct ge vf = Some fd ->
+      funsig fd = sig ->
+      evalinf_funcall m fd vargs t ->
+      execinf_stmt f sp e m (Scall optid sig a bl) t
   | execinf_Sifthenelse:
-      forall sp e m a s1 s2 v b t,
+      forall f sp e m a s1 s2 v b t,
       eval_expr ge sp e m a v ->
       Val.bool_of_val v b ->
-      execinf_stmt sp e m (if b then s1 else s2) t ->
-      execinf_stmt sp e m (Sifthenelse a s1 s2) t
+      execinf_stmt f sp e m (if b then s1 else s2) t ->
+      execinf_stmt f sp e m (Sifthenelse a s1 s2) t
   | execinf_Sseq_1:
-      forall sp e m t s1 s2,
-      execinf_stmt sp e m s1 t ->
-      execinf_stmt sp e m (Sseq s1 s2) t
+      forall f sp e m t s1 s2,
+      execinf_stmt f sp e m s1 t ->
+      execinf_stmt f sp e m (Sseq s1 s2) t
   | execinf_Sseq_2:
-      forall sp e m t s1 t1 e1 m1 s2 t2,
-      exec_stmt sp e m s1 t1 e1 m1 Out_normal ->
-      execinf_stmt sp e1 m1 s2 t2 ->
+      forall f sp e m t s1 t1 e1 m1 s2 t2,
+      exec_stmt f sp e m s1 t1 e1 m1 Out_normal ->
+      execinf_stmt f sp e1 m1 s2 t2 ->
       t = t1 *** t2 ->
-      execinf_stmt sp e m (Sseq s1 s2) t
+      execinf_stmt f sp e m (Sseq s1 s2) t
   | execinf_Sloop_body:
-      forall sp e m s t,
-      execinf_stmt sp e m s t ->
-      execinf_stmt sp e m (Sloop s) t
+      forall f sp e m s t,
+      execinf_stmt f sp e m s t ->
+      execinf_stmt f sp e m (Sloop s) t
   | execinf_Sloop_loop:
-      forall sp e m s t t1 e1 m1 t2,
-      exec_stmt sp e m s t1 e1 m1 Out_normal ->
-      execinf_stmt sp e1 m1 (Sloop s) t2 ->
+      forall f sp e m s t t1 e1 m1 t2,
+      exec_stmt f sp e m s t1 e1 m1 Out_normal ->
+      execinf_stmt f sp e1 m1 (Sloop s) t2 ->
       t = t1 *** t2 ->
-      execinf_stmt sp e m (Sloop s) t
+      execinf_stmt f sp e m (Sloop s) t
   | execinf_Sblock:
-      forall sp e m s t,
-      execinf_stmt sp e m s t ->
-      execinf_stmt sp e m (Sblock s) t
+      forall f sp e m s t,
+      execinf_stmt f sp e m s t ->
+      execinf_stmt f sp e m (Sblock s) t
   | execinf_Stailcall:
-      forall sp e m sig a bl vf vargs f t,
+      forall f sp e m sig a bl vf vargs fd m' t,
       eval_expr ge (Vptr sp Int.zero) e m a vf ->
       eval_exprlist ge (Vptr sp Int.zero) e m bl vargs ->
-      Genv.find_funct ge vf = Some f ->
-      funsig f = sig ->
-      evalinf_funcall (Mem.free m sp) f vargs t ->
-      execinf_stmt (Vptr sp Int.zero) e m (Stailcall sig a bl) t.
+      Genv.find_funct ge vf = Some fd ->
+      funsig fd = sig ->
+      Mem.free m sp 0 f.(fn_stackspace) = Some m' ->
+      evalinf_funcall m' fd vargs t ->
+      execinf_stmt f (Vptr sp Int.zero) e m (Stailcall sig a bl) t.
 
 End NATURALSEM.
 
@@ -795,15 +808,6 @@ Section BIGSTEP_TO_TRANSITION.
 Variable prog: program.
 Let ge := Genv.globalenv prog.
 
-Definition eval_funcall_exec_stmt_ind2 
-  (P1: mem -> fundef -> list val -> trace -> mem -> val -> Prop)
-  (P2: val -> env -> mem -> stmt -> trace ->
-              env -> mem -> outcome -> Prop) :=
-  fun a b c d e f g h i j k l m n o p q =>
-  conj
-    (eval_funcall_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q)
-    (exec_stmt_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q).
-
 Inductive outcome_state_match
         (sp: val) (e: env) (m: mem) (f: function) (k: cont):
         outcome -> state -> Prop :=
@@ -850,9 +854,9 @@ Lemma eval_funcall_exec_stmt_steps:
    is_call_cont k ->
    star step ge (Callstate fd args k m)
               t (Returnstate res k m'))
-/\(forall sp e m s t e' m' out,
-   exec_stmt ge sp e m s t e' m' out ->
-   forall f k,
+/\(forall f sp e m s t e' m' out,
+   exec_stmt ge f sp e m s t e' m' out ->
+   forall k,
    exists S,
    star step ge (State f s k sp e m) t S
    /\ outcome_state_match sp e' m' f k out S).
@@ -860,7 +864,7 @@ Proof.
   apply eval_funcall_exec_stmt_ind2; intros.
 
 (* funcall internal *)
-  destruct (H2 f k) as [S [A B]].
+  destruct (H2 k) as [S [A B]].
   assert (call_cont k = k) by (apply call_cont_is_call_cont; auto).
   eapply star_left. econstructor; eauto. 
   eapply star_trans. eexact A.
@@ -868,22 +872,22 @@ Proof.
   (* Out normal *)
   assert (f.(fn_sig).(sig_res) = None /\ vres = Vundef).
     destruct f.(fn_sig).(sig_res). contradiction. auto.
-  destruct H6. subst vres.
+  destruct H7. subst vres.
   apply star_one. apply step_skip_call; auto. 
   (* Out_return None *)
   assert (f.(fn_sig).(sig_res) = None /\ vres = Vundef).
     destruct f.(fn_sig).(sig_res). contradiction. auto.
-  destruct H7. subst vres.
+  destruct H8. subst vres.
   replace k with (call_cont k') by congruence.
   apply star_one. apply step_return_0; auto.
   (* Out_return Some *)
   assert (f.(fn_sig).(sig_res) <> None /\ vres = v).
     destruct f.(fn_sig).(sig_res). split; congruence. contradiction.
-  destruct H8. subst vres.
+  destruct H9. subst vres.
   replace k with (call_cont k') by congruence.
   apply star_one. eapply step_return_1; eauto.
   (* Out_tailcall_return *)
-  subst vres. rewrite H5. apply star_refl.
+  subst vres. red in H4. subst m3. rewrite H6. apply star_refl.
 
   reflexivity. traceEq.
 
@@ -913,7 +917,7 @@ Proof.
   subst e'. constructor.
 
 (* ifthenelse *)
-  destruct (H2 f k) as [S [A B]].
+  destruct (H2 k) as [S [A B]].
   exists S; split.
   apply star_left with E0 (State f (if b then s1 else s2) k sp e m) t.
   econstructor; eauto. exact A.
@@ -921,8 +925,8 @@ Proof.
   auto.
 
 (* seq continue *)
-  destruct (H0 f (Kseq s2 k)) as [S1 [A1 B1]].
-  destruct (H2 f k) as [S2 [A2 B2]].
+  destruct (H0 (Kseq s2 k)) as [S1 [A1 B1]].
+  destruct (H2 k) as [S2 [A2 B2]].
   inv B1.
   exists S2; split.
   eapply star_left. constructor. 
@@ -932,7 +936,7 @@ Proof.
   auto.
 
 (* seq stop *)
-  destruct (H0 f (Kseq s2 k)) as [S1 [A1 B1]].
+  destruct (H0 (Kseq s2 k)) as [S1 [A1 B1]].
   set (S2 :=
     match out with
     | Out_exit n => State f (Sexit n) k sp e1 m1
@@ -946,8 +950,8 @@ Proof.
   unfold S2; inv B1; congruence || simpl; constructor; auto.
 
 (* loop loop *)
-  destruct (H0 f (Kseq (Sloop s) k)) as [S1 [A1 B1]].
-  destruct (H2 f k) as [S2 [A2 B2]].
+  destruct (H0 (Kseq (Sloop s) k)) as [S1 [A1 B1]].
+  destruct (H2 k) as [S2 [A2 B2]].
   inv B1.
   exists S2; split.
   eapply star_left. constructor. 
@@ -957,7 +961,7 @@ Proof.
   auto.
 
 (* loop stop *)
-  destruct (H0 f (Kseq (Sloop s) k)) as [S1 [A1 B1]].
+  destruct (H0 (Kseq (Sloop s) k)) as [S1 [A1 B1]].
   set (S2 :=
     match out with
     | Out_exit n => State f (Sexit n) k sp e1 m1
@@ -971,7 +975,7 @@ Proof.
   unfold S2; inv B1; congruence || simpl; constructor; auto.
 
 (* block *)
-  destruct (H0 f (Kblock k)) as [S1 [A1 B1]].
+  destruct (H0 (Kblock k)) as [S1 [A1 B1]].
   set (S2 :=
     match out with
     | Out_normal => State f Sskip k sp e1 m1
@@ -1005,8 +1009,8 @@ Proof.
 (* tailcall *)
   econstructor; split.
   eapply star_left. econstructor; eauto.  
-  apply H4. apply is_call_cont_call_cont. traceEq.
-  constructor. 
+  apply H5. apply is_call_cont_call_cont. traceEq.
+  econstructor. 
 Qed.
 
 Lemma eval_funcall_steps:
@@ -1019,9 +1023,9 @@ Lemma eval_funcall_steps:
 Proof (proj1 eval_funcall_exec_stmt_steps).
 
 Lemma exec_stmt_steps:
-   forall sp e m s t e' m' out,
-   exec_stmt ge sp e m s t e' m' out ->
-   forall f k,
+   forall f sp e m s t e' m' out,
+   exec_stmt ge f sp e m s t e' m' out ->
+   forall k,
    exists S,
    star step ge (State f s k sp e m) t S
    /\ outcome_state_match sp e' m' f k out S.
@@ -1034,7 +1038,7 @@ Lemma evalinf_funcall_forever:
 Proof.
   cofix CIH_FUN.
   assert (forall sp e m s T f k,
-          execinf_stmt ge sp e m s T ->
+          execinf_stmt ge f sp e m s T ->
           forever_plus step ge (State f s k sp e m) T).
   cofix CIH_STMT.
   intros. inv H.
@@ -1055,7 +1059,7 @@ Proof.
   apply CIH_STMT. eauto. traceEq.
 
 (* seq 2 *)
-  destruct (exec_stmt_steps _ _ _ _ _ _ _ _ H0 f (Kseq s2 k))
+  destruct (exec_stmt_steps _ _ _ _ _ _ _ _ _ H0 (Kseq s2 k))
   as [S [A B]]. inv B.
   eapply forever_plus_intro.
   eapply plus_left. constructor.
@@ -1069,7 +1073,7 @@ Proof.
   apply CIH_STMT. eauto. traceEq.
 
 (* loop loop *)
-  destruct (exec_stmt_steps _ _ _ _ _ _ _ _ H0 f (Kseq (Sloop s0) k))
+  destruct (exec_stmt_steps _ _ _ _ _ _ _ _ _ H0 (Kseq (Sloop s0) k))
   as [S [A B]]. inv B.
   eapply forever_plus_intro.
   eapply plus_left. constructor.
@@ -1100,7 +1104,7 @@ Theorem bigstep_program_terminates_exec:
 Proof.
   intros. inv H.
   econstructor.
-  econstructor. eauto. eauto. auto. 
+  econstructor; eauto. 
   apply eval_funcall_steps. eauto. red; auto. 
   econstructor.
 Qed.
@@ -1117,14 +1121,10 @@ Proof.
     eapply evalinf_funcall_forever; eauto. 
   destruct (forever_silent_or_reactive _ _ _ _ _ _ H)
   as [A | [t [s' [T' [B [C D]]]]]]. 
-  left. econstructor. econstructor. eauto. eauto. auto. auto.
+  left. econstructor. econstructor; eauto. auto.
   right. exists t. split.
   econstructor. econstructor; eauto. eauto. auto.  
   subst T. rewrite <- (E0_right t) at 1. apply traceinf_prefix_app. constructor.
 Qed.
 
 End BIGSTEP_TO_TRANSITION.
-
-***************************************************)
-
-