aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--backend/CSE.v2
-rw-r--r--backend/CSEproof.v1
-rw-r--r--cfrontend/Cexec.v9
-rw-r--r--common/AST.v10
-rw-r--r--common/Events.v65
-rw-r--r--common/PrintAST.ml4
-rw-r--r--mppa_k1c/Asmexpand.ml1
7 files changed, 77 insertions, 15 deletions
diff --git a/backend/CSE.v b/backend/CSE.v
index 1936d4e4..9ba50a34 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -493,7 +493,7 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb
| _ =>
empty_numbering
end
- | EF_vload _ | EF_annot _ _ _ | EF_annot_val _ _ _ | EF_debug _ _ _ =>
+ | EF_vload _ | EF_annot _ _ _ | EF_annot_val _ _ _ | EF_debug _ _ _ | EF_profiling _ =>
set_res_unknown before res
end
| Icond cond args ifso ifnot _ =>
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index 5bbb7508..a7465cee 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -1318,6 +1318,7 @@ Proof.
+ apply CASE2; inv H1; auto.
+ apply CASE1.
+ apply CASE2; inv H1; auto.
+ + apply CASE2; inv H1; auto.
* apply set_res_lessdef; auto.
- (* Icond *)
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index b08c3ad7..609689a7 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -509,6 +509,10 @@ Definition do_ef_debug (kind: positive) (text: ident) (targs: list typ)
(w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
Some(w, E0, Vundef, m).
+Definition do_ef_profiling (id : profiling_id)
+ (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
+ Some(w, E0, Vundef, m).
+
Definition do_builtin_or_external (name: string) (sg: signature)
(w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
match lookup_builtin_function name sg with
@@ -531,6 +535,7 @@ Definition do_external (ef: external_function):
| EF_annot_val kind text targ => do_ef_annot_val text targ
| EF_inline_asm text sg clob => do_inline_assembly text sg ge
| EF_debug kind text targs => do_ef_debug kind text targs
+ | EF_profiling id => do_ef_profiling id
end.
Lemma do_ef_external_sound:
@@ -598,6 +603,8 @@ Proof with try congruence.
eapply do_inline_assembly_sound; eauto.
- (* EF_debug *)
unfold do_ef_debug. mydestr. split; constructor.
+- (* EF_profiling *)
+ unfold do_ef_profiling. mydestr. split; constructor.
Qed.
Lemma do_ef_external_complete:
@@ -652,6 +659,8 @@ Proof.
eapply do_inline_assembly_complete; eauto.
- (* EF_debug *)
inv H. inv H0. reflexivity.
+- (* EF_profiling *)
+ inv H. inv H0. reflexivity.
Qed.
(** * Reduction of expressions *)
diff --git a/common/AST.v b/common/AST.v
index eb34d675..595ace01 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -464,6 +464,9 @@ Qed.
(** * External functions *)
+(* Identifiers for profiling information *)
+Definition profiling_id := 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 +517,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).
+ (** Count one profiling event for this identifier.
+ Takes no argument. Produces no observable event. *)
(** The type signature of an external function. *)
@@ -535,6 +541,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 => mksignature nil Tvoid cc_default
end.
(** Whether an external function should be inlined by the compiler. *)
@@ -553,6 +560,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 => true
end.
(** Whether an external function must reload its arguments. *)
diff --git a/common/Events.v b/common/Events.v
index 28bb992a..16efd89c 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 => 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..7f15bc91 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.ml
@@ -61,7 +61,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) ->
+ sprintf "profiling %LX" (Z.to_int64 id)
let rec print_builtin_arg px oc = function
| BA x -> px oc x
diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml
index 8ab10bc5..e388d2aa 100644
--- a/mppa_k1c/Asmexpand.ml
+++ b/mppa_k1c/Asmexpand.ml
@@ -591,6 +591,7 @@ let expand_instruction instr =
| EF_external _ -> failwith "asmexpand: external"
| EF_inline_asm _ -> emit instr
| EF_runtime _ -> failwith "asmexpand: runtime"
+ | EF_profiling _ -> emit instr
end
| _ ->
emit instr
generated by cgit (git 2.34.1) at 2024-05-20 08:24:03 +0000