Require Import Coqlib.
Require Intv.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Events and traces
The observable behaviour of programs is stated in terms of
input/output events, which represent the actions of the program
that the external world can observe. CompCert leaves much flexibility as to
the exact content of events: the only requirement is that they
do not expose memory states nor pointer values
(other than pointers to global variables), because these
are not preserved literally during compilation. For concreteness,
we use the following type for events. Each event represents either:
-
A system call (e.g. an input/output operation), recording the
name of the system call, its parameters, and its result.
-
A volatile load from a global memory location, recording the chunk
and address being read and the value just read.
-
A volatile store to a global memory location, recording the chunk
and address being written and the value stored there.
-
An annotation, recording the text of the annotation and the values
of the arguments.
The values attached to these events are of the following form.
As mentioned above, we do not expose pointer values directly.
Pointers relative to a global variable are shown with the name
of the variable instead of the block identifier.
:
Type :=
|
EVint:
int ->
eventval
|
EVlong:
int64 ->
eventval
|
EVfloat:
float ->
eventval
|
EVsingle:
float32 ->
eventval
|
EVptr_global:
ident ->
int ->
eventval.
Inductive event:
Type :=
|
Event_syscall:
ident ->
list eventval ->
eventval ->
event
|
Event_vload:
memory_chunk ->
ident ->
int ->
eventval ->
event
|
Event_vstore:
memory_chunk ->
ident ->
int ->
eventval ->
event
|
Event_annot:
ident ->
list eventval ->
event.
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 Eapp (
t1 t2:
trace) :
trace :=
t1 ++
t2.
CoInductive traceinf :
Type :=
|
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).
Lemma E0_left:
forall t,
E0 **
t =
t.
Proof.
auto. Qed.
Lemma E0_right:
forall t,
t **
E0 =
t.
Proof.
Lemma Eapp_assoc:
forall t1 t2 t3, (
t1 **
t2) **
t3 =
t1 ** (
t2 **
t3).
Proof.
Lemma Eapp_E0_inv:
forall t1 t2,
t1 **
t2 =
E0 ->
t1 =
E0 /\
t2 =
E0.
Proof (@
app_eq_nil event).
Lemma E0_left_inf:
forall T,
E0 ***
T =
T.
Proof.
auto. 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
E0_left_inf Eappinf_assoc:
trace_rewrite.
Opaque trace E0 Eapp Eappinf.
The following traceEq tactic proves equalities between traces
or infinite traces.
Ltac substTraceHyp :=
match goal with
| [
H: (@
eq trace ?
x ?
y) |-
_ ] =>
subst x ||
clear H
end.
Ltac decomposeTraceEq :=
match goal with
| [ |- (
_ **
_) = (
_ **
_) ] =>
apply (
f_equal2 Eapp);
auto;
decomposeTraceEq
|
_ =>
auto
end.
Ltac traceEq :=
repeat substTraceHyp;
autorewrite with trace_rewrite;
decomposeTraceEq.
Bisimilarity between infinite traces.
CoInductive traceinf_sim:
traceinf ->
traceinf ->
Prop :=
|
traceinf_sim_cons:
forall e T1 T2,
traceinf_sim T1 T2 ->
traceinf_sim (
Econsinf e T1) (
Econsinf e T2).
Lemma traceinf_sim_refl:
forall T,
traceinf_sim T T.
Proof.
cofix COINDHYP; intros.
destruct T. constructor. apply COINDHYP.
Qed.
Lemma traceinf_sim_sym:
forall T1 T2,
traceinf_sim T1 T2 ->
traceinf_sim T2 T1.
Proof.
cofix COINDHYP; intros. inv H; constructor; auto.
Qed.
Lemma traceinf_sim_trans:
forall T1 T2 T3,
traceinf_sim T1 T2 ->
traceinf_sim T2 T3 ->
traceinf_sim T1 T3.
Proof.
cofix COINDHYP;intros. inv H; inv H0; constructor; eauto.
Qed.
CoInductive traceinf_sim':
traceinf ->
traceinf ->
Prop :=
|
traceinf_sim'
_cons:
forall t T1 T2,
t <>
E0 ->
traceinf_sim'
T1 T2 ->
traceinf_sim' (
t ***
T1) (
t ***
T2).
Lemma traceinf_sim'
_sim:
forall T1 T2,
traceinf_sim'
T1 T2 ->
traceinf_sim T1 T2.
Proof.
cofix COINDHYP;
intros.
inv H.
destruct t.
elim H0;
auto.
Transparent Eappinf.
Transparent E0.
simpl.
destruct t.
simpl.
constructor.
apply COINDHYP;
auto.
constructor.
apply COINDHYP.
constructor.
unfold E0;
congruence.
auto.
Qed.
An alternate presentation of infinite traces as
infinite concatenations of nonempty finite traces.
CoInductive traceinf':
Type :=
|
Econsinf':
forall (
t:
trace) (
T:
traceinf'),
t <>
E0 ->
traceinf'.
Program Definition split_traceinf' (
t:
trace) (
T:
traceinf') (
NE:
t <>
E0):
event *
traceinf' :=
match t with
|
nil =>
_
|
e ::
nil => (
e,
T)
|
e ::
t' => (
e,
Econsinf'
t'
T _)
end.
Next Obligation.
elimtype False.
elim NE.
auto.
Qed.
Next Obligation.
red; intro. elim (H e). rewrite H0. auto.
Qed.
CoFixpoint traceinf_of_traceinf' (
T':
traceinf') :
traceinf :=
match T'
with
|
Econsinf'
t T''
NOTEMPTY =>
let (
e,
tl) :=
split_traceinf'
t T''
NOTEMPTY in
Econsinf e (
traceinf_of_traceinf'
tl)
end.
Remark unroll_traceinf':
forall T,
T =
match T with Econsinf'
t T'
NE =>
Econsinf'
t T'
NE end.
Proof.
intros. destruct T; auto.
Qed.
Remark unroll_traceinf:
forall T,
T =
match T with Econsinf t T' =>
Econsinf t T'
end.
Proof.
intros. destruct T; auto.
Qed.
Lemma traceinf_traceinf'
_app:
forall t T NE,
traceinf_of_traceinf' (
Econsinf'
t T NE) =
t ***
traceinf_of_traceinf'
T.
Proof.
induction t.
intros.
elim NE.
auto.
intros.
simpl.
rewrite (
unroll_traceinf (
traceinf_of_traceinf' (
Econsinf' (
a ::
t)
T NE))).
simpl.
destruct t.
auto.
Transparent Eappinf.
simpl.
f_equal.
apply IHt.
Qed.
Prefixes of traces.
Definition trace_prefix (
t1 t2:
trace) :=
exists t3,
t2 =
t1 **
t3.
Definition traceinf_prefix (
t1:
trace) (
T2:
traceinf) :=
exists T3,
T2 =
t1 ***
T3.
Lemma trace_prefix_app:
forall t1 t2 t,
trace_prefix t1 t2 ->
trace_prefix (
t **
t1) (
t **
t2).
Proof.
intros. destruct H as [t3 EQ]. exists t3. traceEq.
Qed.
Lemma traceinf_prefix_app:
forall t1 T2 t,
traceinf_prefix t1 T2 ->
traceinf_prefix (
t **
t1) (
t ***
T2).
Proof.
intros. destruct H as [T3 EQ]. exists T3. subst T2. traceEq.
Qed.