summaryrefslogtreecommitdiff
path: root/backend
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2010-03-11 12:22:26 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2010-03-11 12:22:26 +0000
commit7c55573d4a6dd0f643295d52c391d33f7593064a (patch)
tree06a4d8f3d732335dc954c5ff03b31333a991e145 /backend
parent261103b5bfd89335d028bf800af3f0a1ab1b70e5 (diff)
Restored the big-step semantics for Cminor
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1287 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend')
-rw-r--r--backend/Cminor.v250
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.
-
-***************************************************)
-
-