source: src/common/Events.ma @ 2476

Last change on this file since 2476 was 2468, checked in by garnier, 7 years ago

Floats are gone from the front-end. Some trace amount might remain in RTL/RTLabs, but this should be easily fixable.
Also, work-in-progress in Clight/memoryInjections.ma

File size: 10.8 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*)
20(*include "AST.ma".*)
21(*include "Integers.ma".*)
22(*include "Floats.ma".*)
23include "common/Values.ma".
24include "basics/lists/list.ma".
25include "utilities/extralib.ma".
26include "common/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
39inductive eventval: Type[0] ≝
40  | EVint: ∀sz. bvint sz → eventval.
41(*  | EVfloat: float → eventval.*)
42
43inductive event : Type[0] ≝
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
50definition trace := list event.
51
52definition E0 : trace := nil ?.
53
54definition Echarge : costlabel → trace ≝
55λlabel. EVcost label :: (nil ?).
56
57definition Eextcall : ident → list eventval → eventval → trace ≝
58             λname: ident. λargs: list eventval. λres: eventval.
59  EVextcall name args res :: (nil ?).
60
61definition Eapp : trace → trace → trace ≝ λt1,t2. t1 @ t2.
62
63coinductive traceinf : Type[0] :=
64  | Econsinf: event -> traceinf -> traceinf.
65
66let 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(* Useful for testing programs. *)
73definition remove_costs : trace → trace ≝
74filter … (λe. match e with [ EVcost _ ⇒ false | _ ⇒ true ]).
75
76(* * Concatenation of traces is written [**] in the finite case
77  or [***] in the infinite case. *)
78
79notation "hvbox(l1 break ⧺ l2)"
80  right associative with precedence 47
81  for @{'doubleplus $l1 $l2 }.
82
83notation "hvbox(l1 break ⧻ l2)"
84  right associative with precedence 47
85  for @{'tripleplus $l1 $l2 }.
86
87interpretation "trace concatenation" 'doubleplus l1 l2 = (Eapp l1 l2).
88interpretation "infinite trace concatenation" 'tripleplus l1 l2 = (Eappinf l1 l2).
89(*
90Infix "**" := Eapp (at level 60, right associativity).
91Infix "***" := Eappinf (at level 60, right associativity).
92*)
93lemma E0_left: ∀t. E0 ⧺ t = t.
94//; qed.
95
96lemma E0_right: ∀t. t ⧺ E0 = t.
97@append_nil qed.
98
99lemma Eapp_assoc: ∀t1,t2,t3. (t1 ⧺ t2) ⧺ t3 = t1 ⧺ (t2 ⧺ t3).
100@associative_append qed.
101
102lemma Eapp_E0_inv: ∀t1,t2. t1 ⧺ t2 = E0 → t1 = E0 ∧ t2 = E0.
103@nil_append_nil_both qed.
104 
105lemma E0_left_inf: ∀T. E0 ⧻ T = T.
106//; qed.
107
108lemma Eappinf_assoc: ∀t1,t2,T. (t1 ⧺ t2) ⧻ T = t1 ⧻ (t2 ⧻ T).
109#t1 elim t1; #t2 #T normalize; //; qed.
110
111(*
112Hint Rewrite E0_left E0_right Eapp_assoc
113             E0_left_inf Eappinf_assoc: trace_rewrite.
114
115Opaque trace E0 Eextcall Eapp Eappinf.
116
117(** The following [traceEq] tactic proves equalities between traces
118  or infinite traces. *)
119
120Ltac substTraceHyp :=
121  match goal with
122  | [ H: (@eq trace ?x ?y) |- _ ] =>
123       subst x || clear H
124  end.
125
126Ltac decomposeTraceEq :=
127  match goal with
128  | [ |- (_ ** _) = (_ ** _) ] =>
129      apply (f_equal2 Eapp); auto; decomposeTraceEq
130  | _ =>
131      auto
132  end.
133
134Ltac traceEq :=
135  repeat substTraceHyp; autorewrite with trace_rewrite; decomposeTraceEq.
136*)
137
138(* Ported from CompCert 1.7.1 >>> *)
139
140(* * An alternate presentation of infinite traces as
141  infinite concatenations of nonempty finite traces. *)
142
143coinductive traceinf': Type[0] ≝
144  | Econsinf': ∀t: trace. ∀T: traceinf'. t ≠ E0 → traceinf'.
145
146definition split_traceinf' : ∀t:trace. traceinf' → t ≠ E0 → event × traceinf' ≝
147λt,T.
148  match t return λt0.t0 ≠ E0 → ? with
149  [ nil ⇒ ?
150  | cons e t' ⇒ λ_.
151     (match t' return λt0. t' = t0 → ? with
152     [ nil ⇒ λ_.〈e, T〉
153     | cons e' t'' ⇒ λE.〈e, Econsinf' t' T ?〉
154     ]) (refl ? t')
155  ].
156[ *; #NE @False_rect_Type0 @NE @refl
157| % #E' >E' in E; #E whd in E:(??%%); destruct (E);
158] qed.
159
160let corec traceinf_of_traceinf' (T': traceinf') : traceinf ≝
161  match T' with
162  [ Econsinf' t T'' NOTEMPTY ⇒
163      let 〈e,tl〉 ≝ split_traceinf' t T'' NOTEMPTY in
164      Econsinf e (traceinf_of_traceinf' tl)
165  ].
166
167lemma unroll_traceinf':
168  ∀T. T = match T with [ Econsinf' t T' NE ⇒ Econsinf' t T' NE ].
169#T cases T; //; qed.
170
171lemma unroll_traceinf:
172  ∀T. T = match T with [ Econsinf t T' ⇒ Econsinf t T' ].
173#T cases T #ev #tr @refl (* XXX //; *)
174qed.
175
176lemma traceinf_traceinfp_app:
177  ∀t,T,NE.
178  traceinf_of_traceinf' (Econsinf' t T NE) = t ⧻ traceinf_of_traceinf' T.
179#t elim t;
180[ #T #NE cases NE; #NE' @False_ind @NE' @refl
181| #h #t' cases t'; [ 2: #h' #t'' ] #IH #T #NE
182    >(unroll_traceinf (traceinf_of_traceinf' ?))
183    whd in ⊢ (??%?); //; >(IH …) @refl
184] qed.
185
186(* <<< *)
187
188(* * The predicate [event_match ef vargs t vres] expresses that
189  the event [t] is generated when invoking external function [ef]
190  with arguments [vargs], and obtaining [vres] as a return value
191  from the operating system. *)
192
193inductive eventval_match: eventval -> typ -> val -> Prop :=
194  | ev_match_int:
195      ∀sz,sg,i. eventval_match (EVint sz i) (ASTint sz sg) (Vint sz i)
196(*  | ev_match_float:
197      ∀f,sz. eventval_match (EVfloat f) (ASTfloat sz) (Vfloat f) *).
198
199inductive eventval_list_match: list eventval -> list typ -> list val -> Prop :=
200  | evl_match_nil:
201      eventval_list_match (nil ?) (nil ?) (nil ?)
202  | evl_match_cons:
203      ∀ev1,evl,ty1,tyl,v1,vl.
204      eventval_match ev1 ty1 v1 ->
205      eventval_list_match evl tyl vl ->
206      eventval_list_match (ev1::evl) (ty1::tyl) (v1::vl).
207
208inductive event_match:
209         external_function -> list val -> trace -> val -> Prop :=
210  event_match_intro:
211    ∀ef,vargs,vres,eargs,eres.
212    eventval_list_match eargs (sig_args (ef_sig ef)) vargs ->
213    eventval_match eres (proj_sig_res (ef_sig ef)) vres ->
214    event_match ef vargs (Eextcall (ef_id ef) eargs eres) vres.
215(*
216(** The following section shows that [event_match] is stable under
217  relocation of pointer values, as performed by memory injections
218  (see module [Mem]). *)
219
220Require Import Mem.
221
222Section EVENT_MATCH_INJECT.
223
224Variable f: meminj.
225
226Remark eventval_match_inject:
227  forall ev ty v1,  eventval_match ev ty v1 ->
228  forall v2, val_inject f v1 v2 ->
229  eventval_match ev ty v2.
230Proof.
231  induction 1; intros; inversion H; constructor.
232Qed.
233
234Remark eventval_list_match_inject:
235  forall evl tyl vl1,  eventval_list_match evl tyl vl1 ->
236  forall vl2, val_list_inject f vl1 vl2 ->
237  eventval_list_match evl tyl vl2.
238Proof.
239  induction 1; intros.
240  inversion H; constructor.
241  inversion H1; constructor.
242  eapply eventval_match_inject; eauto.
243  eauto.
244Qed.
245
246Lemma event_match_inject:
247  forall ef args1 t res args2,
248  event_match ef args1 t res ->
249  val_list_inject f args1 args2 ->
250  event_match ef args2 t res /\ val_inject f res res.
251Proof.
252  intros. inversion H; subst.
253  split. constructor. eapply eventval_list_match_inject; eauto. auto.
254  inversion H2; constructor.
255Qed.
256
257End EVENT_MATCH_INJECT.
258
259(** The following section shows that [event_match] is stable under
260  replacement of [Vundef] values by more defined values. *)
261
262Section EVENT_MATCH_LESSDEF.
263
264Remark eventval_match_lessdef:
265  forall ev ty v1,  eventval_match ev ty v1 ->
266  forall v2, Val.lessdef v1 v2 ->
267  eventval_match ev ty v2.
268Proof.
269  induction 1; intros; inv H; constructor.
270Qed.
271
272Remark eventval_list_match_moredef:
273  forall evl tyl vl1, eventval_list_match evl tyl vl1 ->
274  forall vl2, Val.lessdef_list vl1 vl2 ->
275  eventval_list_match evl tyl vl2.
276Proof.
277  induction 1; intros.
278  inversion H; constructor.
279  inversion H1; constructor.
280  eapply eventval_match_lessdef; eauto.
281  eauto.
282Qed.
283
284Lemma event_match_lessdef:
285  forall ef args1 t res1 args2,
286  event_match ef args1 t res1 ->
287  Val.lessdef_list args1 args2 ->
288  exists res2, event_match ef args2 t res2 /\ Val.lessdef res1 res2.
289Proof.
290  intros. inversion H; subst. exists res1; split.
291  constructor. eapply eventval_list_match_moredef; eauto. auto.
292  auto.
293Qed.
294
295End EVENT_MATCH_LESSDEF.
296
297(** Bisimilarity between infinite traces. *)
298
299CoInductive traceinf_sim: traceinf -> traceinf -> Prop :=
300  | traceinf_sim_cons: forall e T1 T2,
301      traceinf_sim T1 T2 ->
302      traceinf_sim (Econsinf e T1) (Econsinf e T2).
303
304Lemma traceinf_sim_refl:
305  forall T, traceinf_sim T T.
306Proof.
307  cofix COINDHYP; intros.
308  destruct T. constructor. apply COINDHYP.
309Qed.
310 
311Lemma traceinf_sim_sym:
312  forall T1 T2, traceinf_sim T1 T2 -> traceinf_sim T2 T1.
313Proof.
314  cofix COINDHYP; intros. inv H; constructor; auto.
315Qed.
316
317Lemma traceinf_sim_trans:
318  forall T1 T2 T3,
319  traceinf_sim T1 T2 -> traceinf_sim T2 T3 -> traceinf_sim T1 T3.
320Proof.
321  cofix COINDHYP;intros. inv H; inv H0; constructor; eauto.
322Qed.
323
324(** The "is prefix of" relation between a finite and an infinite trace. *)
325
326Inductive traceinf_prefix: trace -> traceinf -> Prop :=
327  | traceinf_prefix_nil: forall T,
328      traceinf_prefix nil T
329  | traceinf_prefix_cons: forall e t1 T2,
330      traceinf_prefix t1 T2 ->
331      traceinf_prefix (e :: t1) (Econsinf e T2).
332
333(*
334Lemma traceinf_prefix_compat:
335  forall T1 T2 T1' T2',
336  traceinf_prefix T1 T2 -> traceinf_sim T1 T1' -> traceinf_sim T2 T2' ->
337  traceinf_prefix T1' T2'.
338Proof.
339  cofix COINDHYP; intros.
340  inv H; inv H0; inv H1; constructor; eapply COINDHYP; eauto.
341Qed.
342
343Transparent trace E0 Eapp Eappinf.
344*)
345
346Lemma traceinf_prefix_app:
347  forall t1 T2 t,
348  traceinf_prefix t1 T2 ->
349  traceinf_prefix (t ** t1) (t *** T2).
350Proof.
351  induction t; simpl; intros. auto.
352  change ((a :: t) ** t1) with (a :: (t ** t1)).
353  change ((a :: t) *** T2) with (Econsinf a (t *** T2)).
354  constructor. auto.
355Qed.
356
357*)
Note: See TracBrowser for help on using the repository browser.