From 355b4abcee015c3fae9ac5653c25259e104a886c Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Aug 2007 07:27:50 +0000 Subject: Fusion des modifications faites sur les branches "tailcalls" et "smallstep". En particulier: - Semantiques small-step depuis RTL jusqu'a PPC - Cminor independant du processeur - Ajout passes Selection et Reload - Ajout des langages intermediaires CminorSel et LTLin correspondants - Ajout des tailcalls depuis Cminor jusqu'a PPC git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Events.v | 117 ++++++++++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 109 insertions(+), 8 deletions(-) (limited to 'common/Events.v') diff --git a/common/Events.v b/common/Events.v index a0559fd0..e1a4729a 100644 --- a/common/Events.v +++ b/common/Events.v @@ -1,4 +1,4 @@ -(** Representation of (traces of) observable events. *) +(** Representation of observable events and execution traces. *) Require Import Coqlib. Require Import AST. @@ -6,23 +6,77 @@ Require Import Integers. Require Import Floats. Require Import Values. +(** The observable behaviour of programs is stated in terms of + input/output events, which can also be thought of as system calls + to the operating system. An event is generated each time an + external function (see module AST) is invoked. The event records + the name of the external function, the arguments to the function + invocation provided by the program, and the return value provided by + the outside world (e.g. the operating system). Arguments and values + are either integers or floating-point numbers. We currently do not + allow pointers to be exchanged between the program and the outside + world. *) + Inductive eventval: Set := | EVint: int -> eventval | EVfloat: float -> eventval. -Parameter trace: Set. -Parameter E0: trace. -Parameter Eextcall: ident -> list eventval -> eventval -> trace. -Parameter Eapp: trace -> trace -> trace. +Record event : Set := mkevent { + ev_name: ident; + ev_args: list eventval; + ev_res: eventval +}. + +(** The dynamic semantics for programs collect traces of events. + Traces are of two kinds: finite (type [trace]) + or infinite (type [traceinf]). *) + +Definition trace := list event. + +Definition E0 : trace := nil. + +Definition Eextcall + (name: ident) (args: list eventval) (res: eventval) : trace := + mkevent name args res :: nil. + +Definition Eapp (t1 t2: trace) : trace := t1 ++ t2. + +CoInductive traceinf : Set := + | Econsinf: event -> traceinf -> traceinf. + +Fixpoint Eappinf (t: trace) (T: traceinf) {struct t} : traceinf := + match t with + | nil => T + | ev :: t' => Econsinf ev (Eappinf t' T) + end. + +(** Concatenation of traces is written [**] in the finite case + or [***] in the infinite case. *) Infix "**" := Eapp (at level 60, right associativity). +Infix "***" := Eappinf (at level 60, right associativity). -Axiom E0_left: forall t, E0 ** t = t. -Axiom E0_right: forall t, t ** E0 = t. -Axiom Eapp_assoc: forall t1 t2 t3, (t1 ** t2) ** t3 = t1 ** (t2 ** t3). +Lemma E0_left: forall t, E0 ** t = t. +Proof. auto. Qed. + +Lemma E0_right: forall t, t ** E0 = t. +Proof. intros. unfold E0, Eapp. rewrite <- app_nil_end. auto. Qed. + +Lemma Eapp_assoc: forall t1 t2 t3, (t1 ** t2) ** t3 = t1 ** (t2 ** t3). +Proof. intros. unfold Eapp, trace. apply app_ass. Qed. + +Lemma Eappinf_assoc: forall t1 t2 T, (t1 ** t2) *** T = t1 *** (t2 *** T). +Proof. + induction t1; intros; simpl. auto. decEq; auto. +Qed. Hint Rewrite E0_left E0_right Eapp_assoc: trace_rewrite. +Opaque trace E0 Eextcall Eapp. + +(** The following [traceEq] tactic proves equalities between traces + or infinite traces. *) + Ltac substTraceHyp := match goal with | [ H: (@eq trace ?x ?y) |- _ ] => @@ -40,6 +94,11 @@ Ltac decomposeTraceEq := Ltac traceEq := repeat substTraceHyp; autorewrite with trace_rewrite; decomposeTraceEq. +(** The predicate [event_match ef vargs t vres] expresses that + the event [t] is generated when invoking external function [ef] + with arguments [vargs], and obtaining [vres] as a return value + from the operating system. *) + Inductive eventval_match: eventval -> typ -> val -> Prop := | ev_match_int: forall i, eventval_match (EVint i) Tint (Vint i) @@ -63,6 +122,10 @@ Inductive event_match: eventval_match eres (proj_sig_res ef.(ef_sig)) vres -> event_match ef vargs (Eextcall ef.(ef_id) eargs eres) vres. +(** The following section shows that [event_match] is stable under + relocation of pointer values, as performed by memory injections + (see module [Mem]). *) + Require Import Mem. Section EVENT_MATCH_INJECT. @@ -101,3 +164,41 @@ Proof. Qed. End EVENT_MATCH_INJECT. + +(** The following section shows that [event_match] is stable under + replacement of [Vundef] values by more defined values. *) + +Section EVENT_MATCH_LESSDEF. + +Remark eventval_match_lessdef: + forall ev ty v1, eventval_match ev ty v1 -> + forall v2, Val.lessdef v1 v2 -> + eventval_match ev ty v2. +Proof. + induction 1; intros; inv H; constructor. +Qed. + +Remark eventval_list_match_moredef: + forall evl tyl vl1, eventval_list_match evl tyl vl1 -> + forall vl2, Val.lessdef_list vl1 vl2 -> + eventval_list_match evl tyl vl2. +Proof. + induction 1; intros. + inversion H; constructor. + inversion H1; constructor. + eapply eventval_match_lessdef; eauto. + eauto. +Qed. + +Lemma event_match_lessdef: + forall ef args1 t res1 args2, + event_match ef args1 t res1 -> + Val.lessdef_list args1 args2 -> + exists res2, event_match ef args2 t res2 /\ Val.lessdef res1 res2. +Proof. + intros. inversion H; subst. exists res1; split. + constructor. eapply eventval_list_match_moredef; eauto. auto. + auto. +Qed. + +End EVENT_MATCH_LESSDEF. -- cgit