source: C-semantics/Events.ma @ 366

Last change on this file since 366 was 175, checked in by campbell, 9 years ago

Add cost labels, with the semantics that the label is added to the
event trace.

File size: 9.2 KB
Line 
1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*                                                                     *)
7(*  Copyright Institut National de Recherche en Informatique et en     *)
8(*  Automatique.  All rights reserved.  This file is distributed       *)
9(*  under the terms of the GNU General Public License as published by  *)
10(*  the Free Software Foundation, either version 2 of the License, or  *)
11(*  (at your option) any later version.  This file is also distributed *)
12(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
13(*                                                                     *)
14(* *********************************************************************)
15
16(* * Representation of observable events and execution traces. *)
17(*
18Require Import Coqlib.
19*)
20include "AST.ma".
21include "Integers.ma".
22include "Floats.ma".
23include "Values.ma".
24include "datatypes/list.ma".
25include "extralib.ma".
26include "CostLabel.ma".
27
28(* * The observable behaviour of programs is stated in terms of
29  input/output events, which can also be thought of as system calls
30  to the operating system.  An event is generated each time an
31  external function (see module AST) is invoked.  The event records
32  the name of the external function, the arguments to the function
33  invocation provided by the program, and the return value provided by
34  the outside world (e.g. the operating system).  Arguments and values
35  are either integers or floating-point numbers.  We currently do not
36  allow pointers to be exchanged between the program and the outside
37  world. *)
38
39ninductive eventval: Type :=
40  | EVint: int -> eventval
41  | EVfloat: float -> eventval.
42
43ninductive event : Type ≝
44  | EVcost: costlabel → event
45  | EVextcall: ∀ev_name: ident. ∀ev_args: list eventval. ∀ev_res: eventval. event.
46
47(* * The dynamic semantics for programs collect traces of events.
48  Traces are of two kinds: finite (type [trace]) or infinite (type [traceinf]). *)
49
50ndefinition trace := list event.
51
52ndefinition E0 : trace := nil ?.
53
54ndefinition Echarge : costlabel → trace ≝
55λlabel. EVcost label :: (nil ?).
56
57ndefinition Eextcall : ident → list eventval → eventval → trace ≝
58             λname: ident. λargs: list eventval. λres: eventval.
59  EVextcall name args res :: (nil ?).
60
61ndefinition Eapp : trace → trace → trace ≝ λt1,t2. t1 @ t2.
62
63ncoinductive traceinf : Type :=
64  | Econsinf: event -> traceinf -> traceinf.
65
66nlet rec Eappinf (t: trace) (T: traceinf) on t : traceinf :=
67  match t with
68  [ nil => T
69  | cons ev t' => Econsinf ev (Eappinf t' T)
70  ].
71
72(* * Concatenation of traces is written [**] in the finite case
73  or [***] in the infinite case. *)
74
75notation "hvbox(l1 break ⧺ l2)"
76  right associative with precedence 47
77  for @{'doubleplus $l1 $l2 }.
78
79notation "hvbox(l1 break ⧻ l2)"
80  right associative with precedence 47
81  for @{'tripleplus $l1 $l2 }.
82
83interpretation "trace concatenation" 'doubleplus l1 l2 = (Eapp l1 l2).
84interpretation "infinite trace concatenation" 'tripleplus l1 l2 = (Eappinf l1 l2).
85(*
86Infix "**" := Eapp (at level 60, right associativity).
87Infix "***" := Eappinf (at level 60, right associativity).
88*)
89nlemma E0_left: ∀t. E0 ⧺ t = t.
90//; nqed.
91
92nlemma E0_right: ∀t. t ⧺ E0 = t.
93napply append_nil; nqed.
94
95nlemma Eapp_assoc: ∀t1,t2,t3. (t1 ⧺ t2) ⧺ t3 = t1 ⧺ (t2 ⧺ t3).
96napply associative_append; nqed.
97
98nlemma Eapp_E0_inv: ∀t1,t2. t1 ⧺ t2 = E0 → t1 = E0 ∧ t2 = E0.
99napply nil_append_nil_both; nqed.
100 
101nlemma E0_left_inf: ∀T. E0 ⧻ T = T.
102//; nqed.
103
104nlemma Eappinf_assoc: ∀t1,t2,T. (t1 ⧺ t2) ⧻ T = t1 ⧻ (t2 ⧻ T).
105#t1; nelim t1; #t2 T; nnormalize; //; nqed.
106
107(*
108Hint Rewrite E0_left E0_right Eapp_assoc
109             E0_left_inf Eappinf_assoc: trace_rewrite.
110
111Opaque trace E0 Eextcall Eapp Eappinf.
112
113(** The following [traceEq] tactic proves equalities between traces
114  or infinite traces. *)
115
116Ltac substTraceHyp :=
117  match goal with
118  | [ H: (@eq trace ?x ?y) |- _ ] =>
119       subst x || clear H
120  end.
121
122Ltac decomposeTraceEq :=
123  match goal with
124  | [ |- (_ ** _) = (_ ** _) ] =>
125      apply (f_equal2 Eapp); auto; decomposeTraceEq
126  | _ =>
127      auto
128  end.
129
130Ltac traceEq :=
131  repeat substTraceHyp; autorewrite with trace_rewrite; decomposeTraceEq.
132*)
133(* * The predicate [event_match ef vargs t vres] expresses that
134  the event [t] is generated when invoking external function [ef]
135  with arguments [vargs], and obtaining [vres] as a return value
136  from the operating system. *)
137
138ninductive eventval_match: eventval -> typ -> val -> Prop :=
139  | ev_match_int:
140      ∀i. eventval_match (EVint i) Tint (Vint i)
141  | ev_match_float:
142      ∀f. eventval_match (EVfloat f) Tfloat (Vfloat f).
143
144ninductive eventval_list_match: list eventval -> list typ -> list val -> Prop :=
145  | evl_match_nil:
146      eventval_list_match (nil ?) (nil ?) (nil ?)
147  | evl_match_cons:
148      ∀ev1,evl,ty1,tyl,v1,vl.
149      eventval_match ev1 ty1 v1 ->
150      eventval_list_match evl tyl vl ->
151      eventval_list_match (ev1::evl) (ty1::tyl) (v1::vl).
152
153ninductive event_match:
154         external_function -> list val -> trace -> val -> Prop :=
155  event_match_intro:
156    ∀ef,vargs,vres,eargs,eres.
157    eventval_list_match eargs (sig_args (ef_sig ef)) vargs ->
158    eventval_match eres (proj_sig_res (ef_sig ef)) vres ->
159    event_match ef vargs (Eextcall (ef_id ef) eargs eres) vres.
160(*
161(** The following section shows that [event_match] is stable under
162  relocation of pointer values, as performed by memory injections
163  (see module [Mem]). *)
164
165Require Import Mem.
166
167Section EVENT_MATCH_INJECT.
168
169Variable f: meminj.
170
171Remark eventval_match_inject:
172  forall ev ty v1,  eventval_match ev ty v1 ->
173  forall v2, val_inject f v1 v2 ->
174  eventval_match ev ty v2.
175Proof.
176  induction 1; intros; inversion H; constructor.
177Qed.
178
179Remark eventval_list_match_inject:
180  forall evl tyl vl1,  eventval_list_match evl tyl vl1 ->
181  forall vl2, val_list_inject f vl1 vl2 ->
182  eventval_list_match evl tyl vl2.
183Proof.
184  induction 1; intros.
185  inversion H; constructor.
186  inversion H1; constructor.
187  eapply eventval_match_inject; eauto.
188  eauto.
189Qed.
190
191Lemma event_match_inject:
192  forall ef args1 t res args2,
193  event_match ef args1 t res ->
194  val_list_inject f args1 args2 ->
195  event_match ef args2 t res /\ val_inject f res res.
196Proof.
197  intros. inversion H; subst.
198  split. constructor. eapply eventval_list_match_inject; eauto. auto.
199  inversion H2; constructor.
200Qed.
201
202End EVENT_MATCH_INJECT.
203
204(** The following section shows that [event_match] is stable under
205  replacement of [Vundef] values by more defined values. *)
206
207Section EVENT_MATCH_LESSDEF.
208
209Remark eventval_match_lessdef:
210  forall ev ty v1,  eventval_match ev ty v1 ->
211  forall v2, Val.lessdef v1 v2 ->
212  eventval_match ev ty v2.
213Proof.
214  induction 1; intros; inv H; constructor.
215Qed.
216
217Remark eventval_list_match_moredef:
218  forall evl tyl vl1, eventval_list_match evl tyl vl1 ->
219  forall vl2, Val.lessdef_list vl1 vl2 ->
220  eventval_list_match evl tyl vl2.
221Proof.
222  induction 1; intros.
223  inversion H; constructor.
224  inversion H1; constructor.
225  eapply eventval_match_lessdef; eauto.
226  eauto.
227Qed.
228
229Lemma event_match_lessdef:
230  forall ef args1 t res1 args2,
231  event_match ef args1 t res1 ->
232  Val.lessdef_list args1 args2 ->
233  exists res2, event_match ef args2 t res2 /\ Val.lessdef res1 res2.
234Proof.
235  intros. inversion H; subst. exists res1; split.
236  constructor. eapply eventval_list_match_moredef; eauto. auto.
237  auto.
238Qed.
239
240End EVENT_MATCH_LESSDEF.
241
242(** Bisimilarity between infinite traces. *)
243
244CoInductive traceinf_sim: traceinf -> traceinf -> Prop :=
245  | traceinf_sim_cons: forall e T1 T2,
246      traceinf_sim T1 T2 ->
247      traceinf_sim (Econsinf e T1) (Econsinf e T2).
248
249Lemma traceinf_sim_refl:
250  forall T, traceinf_sim T T.
251Proof.
252  cofix COINDHYP; intros.
253  destruct T. constructor. apply COINDHYP.
254Qed.
255 
256Lemma traceinf_sim_sym:
257  forall T1 T2, traceinf_sim T1 T2 -> traceinf_sim T2 T1.
258Proof.
259  cofix COINDHYP; intros. inv H; constructor; auto.
260Qed.
261
262Lemma traceinf_sim_trans:
263  forall T1 T2 T3,
264  traceinf_sim T1 T2 -> traceinf_sim T2 T3 -> traceinf_sim T1 T3.
265Proof.
266  cofix COINDHYP;intros. inv H; inv H0; constructor; eauto.
267Qed.
268
269(** The "is prefix of" relation between a finite and an infinite trace. *)
270
271Inductive traceinf_prefix: trace -> traceinf -> Prop :=
272  | traceinf_prefix_nil: forall T,
273      traceinf_prefix nil T
274  | traceinf_prefix_cons: forall e t1 T2,
275      traceinf_prefix t1 T2 ->
276      traceinf_prefix (e :: t1) (Econsinf e T2).
277
278(*
279Lemma traceinf_prefix_compat:
280  forall T1 T2 T1' T2',
281  traceinf_prefix T1 T2 -> traceinf_sim T1 T1' -> traceinf_sim T2 T2' ->
282  traceinf_prefix T1' T2'.
283Proof.
284  cofix COINDHYP; intros.
285  inv H; inv H0; inv H1; constructor; eapply COINDHYP; eauto.
286Qed.
287
288Transparent trace E0 Eapp Eappinf.
289*)
290
291Lemma traceinf_prefix_app:
292  forall t1 T2 t,
293  traceinf_prefix t1 T2 ->
294  traceinf_prefix (t ** t1) (t *** T2).
295Proof.
296  induction t; simpl; intros. auto.
297  change ((a :: t) ** t1) with (a :: (t ** t1)).
298  change ((a :: t) *** T2) with (Econsinf a (t *** T2)).
299  constructor. auto.
300Qed.
301
302*)
Note: See TracBrowser for help on using the repository browser.