Merge remote-tracking branch 'origin/mppa-profiling' into mppa-features

3 files changed, 75 insertions, 15 deletions

diff --git a/common/AST.v b/common/AST.v
index eb34d675..268e13d5 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -464,6 +464,11 @@ Qed.
 
 (** * External functions *)
 
+(* Identifiers for profiling information *)
+Parameter profiling_id : Type.
+Axiom profiling_id_eq : forall (x y : profiling_id), {x=y} + {x<>y}.
+Definition profiling_kind := Z.t.
+
 (** For most languages, the functions composing the program are either
   internal functions, defined within the language, or external functions,
   defined outside.  External functions include system calls but also
@@ -514,10 +519,13 @@ Inductive external_function : Type :=
          used with caution, as it can invalidate the semantic
          preservation theorem.  Generated only if [-finline-asm] is
          given. *)
-  | EF_debug (kind: positive) (text: ident) (targs: list typ).
+  | EF_debug (kind: positive) (text: ident) (targs: list typ)
      (** Transport debugging information from the front-end to the generated
          assembly.  Takes zero, one or several arguments like [EF_annot].
          Unlike [EF_annot], produces no observable event. *)
+  | EF_profiling (id: profiling_id) (kind : profiling_kind).
+     (** Count one profiling event for this identifier and kind.
+         Takes no argument. Produces no observable event. *)
 
 (** The type signature of an external function. *)
 
@@ -535,6 +543,7 @@ Definition ef_sig (ef: external_function): signature :=
   | EF_annot_val kind text targ => mksignature (targ :: nil) targ cc_default
   | EF_inline_asm text sg clob => sg
   | EF_debug kind text targs => mksignature targs Tvoid cc_default
+  | EF_profiling id kind => mksignature nil Tvoid cc_default
   end.
 
 (** Whether an external function should be inlined by the compiler. *)
@@ -553,6 +562,7 @@ Definition ef_inline (ef: external_function) : bool :=
   | EF_annot_val kind Text rg => true
   | EF_inline_asm text sg clob => true
   | EF_debug kind text targs => true
+  | EF_profiling id kind => true
   end.
 
 (** Whether an external function must reload its arguments. *)
@@ -568,7 +578,7 @@ Definition ef_reloads (ef: external_function) : bool :=
 
 Definition external_function_eq: forall (ef1 ef2: external_function), {ef1=ef2} + {ef1<>ef2}.
 Proof.
-  generalize ident_eq string_dec signature_eq chunk_eq typ_eq list_eq_dec zeq Int.eq_dec; intros.
+  generalize profiling_id_eq ident_eq string_dec signature_eq chunk_eq typ_eq list_eq_dec zeq Int.eq_dec; intros.
   decide equality.
 Defined.
 Global Opaque external_function_eq.
diff --git a/common/Events.v b/common/Events.v
index 28bb992a..033e2e03 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -1378,6 +1378,11 @@ Inductive extcall_debug_sem (ge: Senv.t):
   | extcall_debug_sem_intro: forall vargs m,
       extcall_debug_sem ge vargs m E0 Vundef m.
 
+Inductive extcall_profiling_sem (ge: Senv.t):
+              list val -> mem -> trace -> val -> mem -> Prop :=
+  | extcall_profiling_sem_intro: forall vargs m,
+      extcall_profiling_sem ge vargs m E0 Vundef m.
+
 Lemma extcall_debug_ok:
   forall targs,
   extcall_properties extcall_debug_sem
@@ -1412,6 +1417,40 @@ Proof.
   split. constructor. auto.
 Qed.
 
+Lemma extcall_profiling_ok:
+  forall targs,
+  extcall_properties extcall_profiling_sem
+                     (mksignature targs Tvoid cc_default).
+Proof.
+  intros; constructor; intros.
+(* well typed *)
+- inv H. simpl. auto.
+(* symbols *)
+- inv H0. econstructor; eauto.
+(* valid blocks *)
+- inv H; auto.
+(* perms *)
+- inv H; auto.
+(* readonly *)
+- inv H; auto.
+(* mem extends *)
+- inv H.
+  exists Vundef; exists m1'; intuition.
+  econstructor; eauto.
+(* mem injects *)
+- inv H0.
+  exists f; exists Vundef; exists m1'; intuition.
+  econstructor; eauto.
+  red; intros; congruence.
+(* trace length *)
+- inv H; simpl; omega.
+(* receptive *)
+- inv H; inv H0. exists Vundef, m1; constructor.
+(* determ *)
+- inv H; inv H0.
+  split. constructor. auto.
+Qed.
+
 (** ** Semantics of known built-in functions. *)
 
 (** Some built-in functions and runtime support functions have known semantics
@@ -1530,6 +1569,7 @@ Definition external_call (ef: external_function): extcall_sem :=
   | EF_annot_val kind txt targ => extcall_annot_val_sem txt targ
   | EF_inline_asm txt sg clb => inline_assembly_sem txt sg
   | EF_debug kind txt targs => extcall_debug_sem
+  | EF_profiling id kind  => extcall_profiling_sem
   end.
 
 Theorem external_call_spec:
@@ -1537,18 +1577,19 @@ Theorem external_call_spec:
   extcall_properties (external_call ef) (ef_sig ef).
 Proof.
   intros. unfold external_call, ef_sig; destruct ef.
-  apply external_functions_properties.
-  apply builtin_or_external_sem_ok.
-  apply builtin_or_external_sem_ok.
-  apply volatile_load_ok.
-  apply volatile_store_ok.
-  apply extcall_malloc_ok.
-  apply extcall_free_ok.
-  apply extcall_memcpy_ok.
-  apply extcall_annot_ok.
-  apply extcall_annot_val_ok.
-  apply inline_assembly_properties.
-  apply extcall_debug_ok.
+- apply external_functions_properties.
+- apply builtin_or_external_sem_ok.
+- apply builtin_or_external_sem_ok.
+- apply volatile_load_ok.
+- apply volatile_store_ok.
+- apply extcall_malloc_ok.
+- apply extcall_free_ok.
+- apply extcall_memcpy_ok.
+- apply extcall_annot_ok.
+- apply extcall_annot_val_ok.
+- apply inline_assembly_properties.
+- apply extcall_debug_ok.
+- apply extcall_profiling_ok.
 Qed.
 
 Definition external_call_well_typed_gen ef := ec_well_typed (external_call_spec ef).
diff --git a/common/PrintAST.ml b/common/PrintAST.ml
index 3f718428..38bbfa47 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.ml
@@ -47,6 +47,13 @@ let name_of_chunk = function
   | Many32 -> "any32"
   | Many64 -> "any64"
 
+let spp_profiling_id () (x : Digest.t) : string =
+  let s = Buffer.create 32 in
+  for i=0 to 15 do
+    Printf.bprintf s "%02x" (Char.code (String.get x i))
+  done;
+  Buffer.contents s;;
+
 let name_of_external = function
   | EF_external(name, sg) -> sprintf "extern %S" (camlstring_of_coqstring name)
   | EF_builtin(name, sg) -> sprintf "builtin %S" (camlstring_of_coqstring name)
@@ -61,7 +68,9 @@ let name_of_external = function
   | EF_annot_val(kind,text, targ) ->  sprintf "annot_val %S" (camlstring_of_coqstring text)
   | EF_inline_asm(text, sg, clob) -> sprintf "inline_asm %S" (camlstring_of_coqstring text)
   | EF_debug(kind, text, targs) ->
-      sprintf "debug%d %S" (P.to_int kind) (extern_atom text)
+     sprintf "debug%d %S" (P.to_int kind) (extern_atom text)
+  | EF_profiling(id, kind) ->
+     sprintf "profiling %a %d" spp_profiling_id id (Z.to_int kind)
 
 let rec print_builtin_arg px oc = function
   | BA x -> px oc x