Fusion de la branche "traces":

- Ajout de traces d'evenements d'E/S dans les semantiques
- Ajout constructions switch et allocation dynamique
- Initialisation des variables globales
- Portage Coq 8.1 beta
Debut d'integration du front-end C:
- Traduction Clight -> Csharpminor dans cfrontend/
- Modifications de Csharpminor et Globalenvs en consequence.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@72 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 75 insertions, 48 deletions

diff --git a/backend/RTL.v b/backend/RTL.v
index ac9a4159..4a3f8e8c 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -4,12 +4,13 @@
   after Cminor.
 *)
 
-Require Import Relations.
+(*Require Import Relations.*)
 Require Import Coqlib.
 Require Import Maps.
 Require Import AST.
 Require Import Integers.
 Require Import Values.
+Require Import Events.
 Require Import Mem.
 Require Import Globalenvs.
 Require Import Op.
@@ -54,6 +55,10 @@ Inductive instruction: Set :=
           function name), giving it the values of registers [args] 
           as arguments.  It stores the return value in [dest] and branches
           to [succ]. *)
+  | Ialloc: reg -> reg -> node -> instruction
+      (** [Ialloc arg dest succ] allocates a fresh block of size
+          the contents of register [arg], stores a pointer to this
+          block in [dest], and branches to [succ]. *)
   | Icond: condition -> list reg -> node -> node -> instruction
       (** [Icond cond args ifso ifnot] evaluates the boolean condition
           [cond] over the values of registers [args].  If the condition
@@ -85,11 +90,19 @@ Record function: Set := mkfunction {
     in the CFG.  [fn_code_wf] asserts that all instructions of the function
     have nodes no greater than [fn_nextpc]. *)
 
-Definition program := AST.program function.
+Definition fundef := AST.fundef function.
+
+Definition program := AST.program fundef.
+
+Definition funsig (fd: fundef) :=
+  match fd with
+  | Internal f => f.(fn_sig)
+  | External ef => ef.(ef_sig)
+  end.
 
 (** * Operational semantics *)
 
-Definition genv := Genv.t function.
+Definition genv := Genv.t fundef.
 Definition regset := Regmap.t val.
 
 Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset :=
@@ -102,7 +115,8 @@ Section RELSEM.
 
 Variable ge: genv.
 
-Definition find_function (ros: reg + ident) (rs: regset) : option function :=
+Definition find_function
+      (ros: reg + ident) (rs: regset) : option fundef :=
   match ros with
   | inl r => Genv.find_funct ge rs#r
   | inr symb =>
@@ -132,66 +146,73 @@ Definition find_function (ros: reg + ident) (rs: regset) : option function :=
   and memory state [m].  The final state is [pc'], [rs'] and [m']. *)
 
 Inductive exec_instr: code -> val ->
-                      node -> regset -> mem ->
+                      node -> regset -> mem -> trace ->
                       node -> regset -> mem -> Prop :=
   | exec_Inop:
       forall c sp pc rs m pc',
       c!pc = Some(Inop pc') ->
-      exec_instr c sp  pc rs m  pc' rs m
+      exec_instr c sp  pc rs m  E0 pc' rs m
   | exec_Iop:
       forall c sp pc rs m op args res pc' v,
       c!pc = Some(Iop op args res pc') ->
       eval_operation ge sp op rs##args = Some v ->
-      exec_instr c sp  pc rs m  pc' (rs#res <- v) m
+      exec_instr c sp  pc rs m  E0 pc' (rs#res <- v) m
   | exec_Iload:
       forall c sp pc rs m chunk addr args dst pc' a v,
       c!pc = Some(Iload chunk addr args dst pc') ->
       eval_addressing ge sp addr rs##args = Some a ->
       Mem.loadv chunk m a = Some v ->
-      exec_instr c sp  pc rs m  pc' (rs#dst <- v) m
+      exec_instr c sp  pc rs m  E0 pc' (rs#dst <- v) m
   | exec_Istore:
       forall c sp pc rs m chunk addr args src pc' a m',
       c!pc = Some(Istore chunk addr args src pc') ->
       eval_addressing ge sp addr rs##args = Some a ->
       Mem.storev chunk m a rs#src = Some m' ->
-      exec_instr c sp  pc rs m  pc' rs m'
+      exec_instr c sp  pc rs m  E0 pc' rs m'
   | exec_Icall:
-      forall c sp pc rs m sig ros args res pc' f vres m',
+      forall c sp pc rs m sig ros args res pc' f vres m' t,
       c!pc = Some(Icall sig ros args res pc') ->
       find_function ros rs = Some f ->
-      sig = f.(fn_sig) ->
-      exec_function f rs##args m vres m' ->
-      exec_instr c sp  pc rs m  pc' (rs#res <- vres) m'
+      funsig f = sig ->
+      exec_function f rs##args m t vres m' ->
+      exec_instr c sp  pc rs m  t pc' (rs#res <- vres) m'
+  | exec_Ialloc:
+      forall c sp pc rs m pc' arg res sz m' b,
+      c!pc = Some(Ialloc arg res pc') ->
+      rs#arg = Vint sz ->
+      Mem.alloc m 0 (Int.signed sz) = (m', b) ->
+      exec_instr c sp  pc rs m E0 pc' (rs#res <- (Vptr b Int.zero)) m'
   | exec_Icond_true:
       forall c sp pc rs m cond args ifso ifnot,
       c!pc = Some(Icond cond args ifso ifnot) ->
       eval_condition cond rs##args = Some true ->
-      exec_instr c sp  pc rs m  ifso rs m
+      exec_instr c sp  pc rs m  E0 ifso rs m
   | exec_Icond_false:
       forall c sp pc rs m cond args ifso ifnot,
       c!pc = Some(Icond cond args ifso ifnot) ->
       eval_condition cond rs##args = Some false ->
-      exec_instr c sp  pc rs m  ifnot rs m
+      exec_instr c sp  pc rs m  E0 ifnot rs m
 
 (** [exec_instrs ge c sp pc rs m pc' rs' m'] is the reflexive
   transitive closure of [exec_instr].  It corresponds to the execution
   of zero, one or finitely many transitions. *)
 
 with exec_instrs: code -> val ->
-                  node -> regset -> mem ->
+                  node -> regset -> mem -> trace ->
                   node -> regset -> mem -> Prop :=
   | exec_refl:
       forall c sp pc rs m,
-      exec_instrs c sp pc rs m pc rs m
+      exec_instrs c sp pc rs m E0 pc rs m
   | exec_one:
-      forall c sp pc rs m pc' rs' m',
-      exec_instr c sp pc rs m pc' rs' m' ->
-      exec_instrs c sp pc rs m pc' rs' m'
+      forall c sp pc rs m t pc' rs' m',
+      exec_instr c sp pc rs m t pc' rs' m' ->
+      exec_instrs c sp pc rs m t pc' rs' m'
   | exec_trans:
-      forall c sp pc1 rs1 m1 pc2 rs2 m2 pc3 rs3 m3,
-      exec_instrs c sp pc1 rs1 m1 pc2 rs2 m2 ->
-      exec_instrs c sp pc2 rs2 m2 pc3 rs3 m3 ->
-      exec_instrs c sp pc1 rs1 m1 pc3 rs3 m3
+      forall c sp pc1 rs1 m1 t1 pc2 rs2 m2 t2 pc3 rs3 m3 t3,
+      exec_instrs c sp pc1 rs1 m1 t1 pc2 rs2 m2 ->
+      exec_instrs c sp pc2 rs2 m2 t2 pc3 rs3 m3 ->
+      t3 = t1 ** t2 ->
+      exec_instrs c sp pc1 rs1 m1 t3 pc3 rs3 m3
 
 (** [exec_function ge f args m res m'] executes a function application.
   [f] is the called function, [args] the values of its arguments,
@@ -205,17 +226,21 @@ with exec_instrs: code -> val ->
   (Non-parameter registers are initialized to [Vundef].)  Before returning,
   the stack activation block is freed. *)
 
-with exec_function: function -> list val -> mem ->
-                                val -> mem -> Prop :=
-  | exec_funct:
-      forall f m m1 stk args pc rs m2 or vres,
+with exec_function: fundef -> list val -> mem -> trace ->
+                              val -> mem -> Prop :=
+  | exec_funct_internal:
+      forall f m m1 stk args t pc rs m2 or vres,
       Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) ->
-      exec_instrs f.(fn_code) (Vptr stk Int.zero)
+      exec_instrs f.(fn_code) (Vptr stk Int.zero) 
                   f.(fn_entrypoint) (init_regs args f.(fn_params)) m1
-                  pc rs m2 ->
+                  t pc rs m2 ->
       f.(fn_code)!pc = Some(Ireturn or) ->
       vres = regmap_optget or Vundef rs ->
-      exec_function f args m vres (Mem.free m2 stk).
+      exec_function (Internal f) args m t vres (Mem.free m2 stk)
+  | exec_funct_external:
+      forall ef args m t res,
+      event_match ef args t res ->
+      exec_function (External ef) args m t res m.
 
 Scheme exec_instr_ind_3 := Minimality for exec_instr Sort Prop
   with exec_instrs_ind_3 := Minimality for exec_instrs Sort Prop
@@ -224,12 +249,13 @@ Scheme exec_instr_ind_3 := Minimality for exec_instr Sort Prop
 (** Some derived execution rules. *)
 
 Lemma exec_step:
-  forall c sp pc1 rs1 m1 pc2 rs2 m2 pc3 rs3 m3,
-  exec_instr c sp pc1 rs1 m1 pc2 rs2 m2 ->
-  exec_instrs c sp pc2 rs2 m2 pc3 rs3 m3 ->
-  exec_instrs c sp pc1 rs1 m1 pc3 rs3 m3.
+  forall c sp pc1 rs1 m1 t1 pc2 rs2 m2 t2 pc3 rs3 m3 t3,
+  exec_instr c sp pc1 rs1 m1 t1 pc2 rs2 m2 ->
+  exec_instrs c sp pc2 rs2 m2 t2 pc3 rs3 m3 ->
+  t3 = t1 ** t2 ->
+  exec_instrs c sp pc1 rs1 m1 t3 pc3 rs3 m3.
 Proof.
-  intros. eapply exec_trans. apply exec_one. eauto. eauto.
+  intros. eapply exec_trans. apply exec_one. eauto. eauto. auto.
 Qed.
 
 Lemma exec_Iop':
@@ -237,7 +263,7 @@ Lemma exec_Iop':
   c!pc = Some(Iop op args res pc') ->
   eval_operation ge sp op rs##args = Some v ->
   rs' = (rs#res <- v) ->
-  exec_instr c sp  pc rs m  pc' rs' m.
+  exec_instr c sp  pc rs m  E0 pc' rs' m.
 Proof.
   intros. subst rs'. eapply exec_Iop; eauto.
 Qed.
@@ -248,7 +274,7 @@ Lemma exec_Iload':
   eval_addressing ge sp addr rs##args = Some a ->
   Mem.loadv chunk m a = Some v ->
   rs' = (rs#dst <- v) ->
-  exec_instr c sp  pc rs m  pc' rs' m.
+  exec_instr c sp  pc rs m E0 pc' rs' m.
 Proof.
   intros. subst rs'. eapply exec_Iload; eauto.
 Qed.
@@ -257,16 +283,16 @@ Qed.
   is defined in the CFG. *)
 
 Lemma exec_instr_present:
-  forall c sp pc rs m pc' rs' m',
-  exec_instr c sp  pc rs m  pc' rs' m' ->
+  forall c sp pc rs m t pc' rs' m',
+  exec_instr c sp  pc rs m  t pc' rs' m' ->
   c!pc <> None.
 Proof.
   induction 1; congruence.
 Qed.
 
 Lemma exec_instrs_present:
-  forall c sp pc rs m pc' rs' m',
-  exec_instrs c sp  pc rs m  pc' rs' m' ->
+  forall c sp pc rs m t pc' rs' m',
+  exec_instrs c sp  pc rs m  t pc' rs' m' ->
   c!pc' <> None -> c!pc <> None.
 Proof.
   induction 1; intros.
@@ -280,14 +306,14 @@ End RELSEM.
 (** Execution of whole programs.  As in Cminor, we call the ``main'' function
   with no arguments and observe its return value. *)
 
-Definition exec_program (p: program) (r: val) : Prop :=
+Definition exec_program (p: program) (t: trace) (r: val) : Prop :=
   let ge := Genv.globalenv p in
   let m0 := Genv.init_mem p in
   exists b, exists f, exists m,
   Genv.find_symbol ge p.(prog_main) = Some b /\
   Genv.find_funct_ptr ge b = Some f /\
-  f.(fn_sig) = mksignature nil (Some Tint) /\
-  exec_function ge f nil m0 r m.
+  funsig f = mksignature nil (Some Tint) /\
+  exec_function ge f nil m0 t r m.
 
 (** * Operations on RTL abstract syntax *)
 
@@ -304,14 +330,15 @@ Definition successors (f: function) (pc: node) : list node :=
       | Iload chunk addr args dst s => s :: nil
       | Istore chunk addr args src s => s :: nil
       | Icall sig ros args res s => s :: nil
+      | Ialloc arg res s => s :: nil
       | Icond cond args ifso ifnot => ifso :: ifnot :: nil
       | Ireturn optarg => nil
       end
   end.
 
 Lemma successors_correct:
-  forall ge f sp pc rs m pc' rs' m',
-  exec_instr ge f.(fn_code) sp pc rs m pc' rs' m' ->
+  forall ge f sp pc rs m t pc' rs' m',
+  exec_instr ge f.(fn_code) sp pc rs m t pc' rs' m' ->
   In pc' (successors f pc).
 Proof.
   intros ge f. unfold successors. generalize (fn_code f).
@@ -345,5 +372,5 @@ Definition transf_function (f: function) : function :=
     f.(fn_entrypoint)
     f.(fn_nextpc)
     (transf_code_wf f.(fn_code) f.(fn_nextpc) f.(fn_code_wf)).
-    
+
 End TRANSF.