Revised handling of annotation statements, and more generally built-in functions, and more generally external functions

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

2 files changed, 153 insertions, 63 deletions

diff --git a/common/AST.v b/common/AST.v
index bca0535..4f113c7 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -397,15 +397,84 @@ Qed.
 (** * External functions *)
 
 (** For most languages, the functions composing the program are either
-  internal functions, defined within the language, or external functions
-  (a.k.a. system calls) that emit an event when applied.  We define
-  a type for such functions and some generic transformation functions. *)
-
-Record external_function : Type := mkextfun {
-  ef_id: ident;
-  ef_sig: signature;
-  ef_inline: bool
-}.
+  internal functions, defined within the language, or external functions,
+  defined outside.  External functions include system calls but also
+  compiler built-in functions.  We define a type for external functions
+  and associated operations. *)
+
+Inductive external_function : Type :=
+  | EF_external (name: ident) (sg: signature)
+     (** A system call or library function.  Produces an event
+         in the trace. *)
+  | EF_builtin (name: ident) (sg: signature)
+     (** A compiler built-in function.  Behaves like an external, but
+         can be inlined by the compiler. *)
+  | EF_vload (chunk: memory_chunk)
+     (** A volatile read operation.  If the adress given as first argument
+         points within a volatile global variable, generate an
+         event and return the value found in this event.  Otherwise,
+         produce no event and behave like a regular memory load. *)
+  | EF_vstore (chunk: memory_chunk)
+     (** A volatile store operation.   If the adress given as first argument
+         points within a volatile global variable, generate an event.
+         Otherwise, produce no event and behave like a regular memory store. *)
+  | EF_malloc
+     (** Dynamic memory allocation.  Takes the requested size in bytes
+         as argument; returns a pointer to a fresh block of the given size.
+         Produces no observable event. *)
+  | EF_free
+     (** Dynamic memory deallocation.  Takes a pointer to a block
+         allocated by an [EF_malloc] external call and frees the
+         corresponding block.
+         Produces no observable event. *)
+  | EF_memcpy (sz: Z) (al: Z)
+     (** Block copy, of [sz] bytes, between addresses that are [al]-aligned. *)
+  | EF_annot (text: ident) (targs: list typ)
+     (** A programmer-supplied annotation.  Takes zero, one or several arguments,
+         produces an event carrying the text and the values of these arguments,
+         and returns no value. *)
+  | EF_annot_val (text:ident) (targ: typ).
+     (** Another form of annotation that takes one argument, produces
+         an event carrying the text and the value of this argument,
+         and returns the value of the argument. *)
+
+(** The type signature of an external function. *)
+
+Definition ef_sig (ef: external_function): signature :=
+  match ef with
+  | EF_external name sg => sg
+  | EF_builtin name sg => sg
+  | EF_vload chunk => mksignature (Tint :: nil) (Some (type_of_chunk chunk))
+  | EF_vstore chunk => mksignature (Tint :: type_of_chunk chunk :: nil) None
+  | EF_malloc => mksignature (Tint :: nil) (Some Tint)
+  | EF_free => mksignature (Tint :: nil) None
+  | EF_memcpy sz al => mksignature (Tint :: Tint :: nil) None
+  | EF_annot text targs => mksignature targs None
+  | EF_annot_val text targ => mksignature (targ :: nil) (Some targ)
+  end.
+
+(** Whether an external function should be inlined by the compiler. *)
+
+Definition ef_inline (ef: external_function) : bool :=
+  match ef with
+  | EF_external name sg => false
+  | EF_builtin name sg => true
+  | EF_vload chunk => true
+  | EF_vstore chunk => true
+  | EF_malloc => false
+  | EF_free => false
+  | EF_memcpy sz al => true
+  | EF_annot text targs => true
+  | EF_annot_val text targ => true
+  end.
+
+(** Whether an external function must reload its arguments. *)
+
+Definition ef_reloads (ef: external_function) : bool :=
+  match ef with
+  | EF_annot text targs => false
+  | _ => true
+  end.
 
 (** Function definitions are the union of internal and external functions. *)
 
diff --git a/common/Events.v b/common/Events.v
index b369d46..ac6c1a0 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -401,41 +401,6 @@ End EVENTVAL_INV.
 
 (** * Semantics of external functions *)
 
-(** Each external function is of one of the following kinds: *)
-
-Inductive extfun_kind: signature -> Type :=
-  | EF_syscall (name: ident) (sg: signature): extfun_kind sg
-     (** A system call.  Takes representable arguments (integers, floats,
-         pointers to globals), produces a representable result,
-         does not modify the memory, and produces an [Event_syscall] event
-         in the trace. *)
-  | EF_vload (chunk: memory_chunk): extfun_kind (mksignature (Tint :: nil) (Some (type_of_chunk chunk)))
-     (** A volatile read operation.  If the adress given as first argument
-         points within a volatile global variable, generate an [Event_vload]
-         event and return the value found in this event.  Otherwise,
-         produce no event and behave like a regular memory load. *)
-  | EF_vstore (chunk: memory_chunk): extfun_kind (mksignature (Tint :: type_of_chunk chunk :: nil) None)
-     (** A volatile store operation.   If the adress given as first argument
-         points within a volatile global variable, generate an [Event_vstore]
-         event.  Otherwise, produce no event and behave like a regular memory store. *)
-  | EF_malloc: extfun_kind (mksignature (Tint :: nil) (Some Tint))
-     (** Dynamic memory allocation.  Takes the requested size in bytes
-         as argument; returns a pointer to a fresh block of the given size.
-         Produces no observable event. *)
-  | EF_free: extfun_kind (mksignature (Tint :: nil) None)
-     (** Dynamic memory deallocation.  Takes a pointer to a block
-         allocated by an [EF_malloc] external call and frees the
-         corresponding block.
-         Produces no observable event. *)
-  | EF_annotation (text: ident) (sg: signature): extfun_kind sg.
-     (** A programmer-supplied annotation.  Takes representable arguments,
-         returns its first argument as result (or [Vundef] if no arguments),
-         does not modify the memory, and produces an [Event_annot]
-         event in the trace. *)
-
-Parameter classify_external_function: 
-  forall (ef: external_function), extfun_kind (ef.(ef_sig)).
-
 (** For each external function, its behavior is defined by a predicate relating:
 - the global environment
 - the values of the arguments passed to this function
@@ -934,6 +899,20 @@ Proof.
   inv H; inv H0. intuition congruence.
 Qed.
 
+(** ** Semantics of [memcpy] operations. *)
+
+(** To be done once [storebytes] is added to the [Memtype] interface. *)
+
+Definition extcall_memcpy_sem (sz al: Z) (F V: Type) (ge: Genv.t F V): list val -> mem -> trace -> val -> mem -> Prop :=
+  fun vargs m1 t vres m2 => False.
+
+Lemma extcall_memcpy_ok:
+  forall sz al,
+  extcall_properties (extcall_memcpy_sem sz al) (mksignature (Tint :: Tint :: nil) None).
+Proof.
+  intros. unfold extcall_memcpy_sem; constructor; contradiction.
+Qed.
+
 (** ** Semantics of system calls. *)
 
 Inductive extcall_io_sem (name: ident) (sg: signature) (F V: Type) (ge: Genv.t F V):
@@ -984,23 +963,19 @@ Qed.
 
 (** ** Semantics of annotation. *)
 
-Inductive extcall_annot_sem (text: ident) (sg: signature) (F V: Type) (ge: Genv.t F V):
+Inductive extcall_annot_sem (text: ident) (targs: list typ) (F V: Type) (ge: Genv.t F V):
               list val -> mem -> trace -> val -> mem -> Prop :=
-  | extcall_annot_sem_intro: forall vargs m args vres,
-      eventval_list_match ge args (sig_args sg) vargs ->
-      sig_res sg = match sig_args sg with nil => None | t1 :: _ => Some t1 end ->
-      vres = match vargs with nil => Vundef | v1 :: _ => v1 end ->
-      extcall_annot_sem text sg ge vargs m (Event_annot text args :: E0) vres m.
+  | extcall_annot_sem_intro: forall vargs m args,
+      eventval_list_match ge args targs vargs ->
+      extcall_annot_sem text targs ge vargs m (Event_annot text args :: E0) Vundef m.
 
 Lemma extcall_annot_ok:
-  forall text sg,
-  extcall_properties (extcall_annot_sem text sg) sg.
+  forall text targs,
+  extcall_properties (extcall_annot_sem text targs) (mksignature targs None).
 Proof.
   intros; constructor; intros.
 
-  inv H. unfold proj_sig_res. rewrite H1. inv H0. 
-  constructor.
-  eapply eventval_match_type; eauto.
+  inv H. simpl. auto.
 
   inv H. eapply eventval_list_match_length; eauto.
 
@@ -1012,17 +987,15 @@ Proof.
   inv H; auto.
 
   inv H.
-  exists (match vargs' with nil => Vundef | v1 :: _ => v1 end); exists m1'; intuition.
+  exists Vundef; exists m1'; intuition.
   econstructor; eauto.
   eapply eventval_list_match_lessdef; eauto.
-  inv H1; auto.
   red; auto.
 
   inv H0.
-  exists f; exists (match vargs' with nil => Vundef | v1 :: _ => v1 end); exists m1'; intuition.
+  exists f; exists Vundef; exists m1'; intuition.
   econstructor; eauto.
   eapply eventval_list_match_inject; eauto.
-  inv H2; auto.
   red; auto.
   red; auto.
   red; intros; congruence.
@@ -1032,6 +1005,48 @@ Proof.
   intuition.
 Qed.
 
+Inductive extcall_annot_val_sem (text: ident) (targ: typ) (F V: Type) (ge: Genv.t F V):
+              list val -> mem -> trace -> val -> mem -> Prop :=
+  | extcall_annot_val_sem_intro: forall varg m arg,
+      eventval_match ge arg targ varg ->
+      extcall_annot_val_sem text targ ge (varg :: nil) m (Event_annot text (arg :: nil) :: E0) varg m.
+
+Lemma extcall_annot_val_ok:
+  forall text targ,
+  extcall_properties (extcall_annot_val_sem text targ) (mksignature (targ :: nil) (Some targ)).
+Proof.
+  intros; constructor; intros.
+
+  inv H. unfold proj_sig_res; simpl. eapply eventval_match_type; eauto.
+
+  inv H. auto.
+
+  inv H1. econstructor; eauto. 
+  eapply eventval_match_preserved; eauto.
+
+  inv H; auto.
+
+  inv H; auto.
+
+  inv H. inv H1. inv H6. 
+  exists v2; exists m1'; intuition.
+  econstructor; eauto.
+  eapply eventval_match_lessdef; eauto.
+  red; auto.
+
+  inv H0. inv H2. inv H7.
+  exists f; exists v'; exists m1'; intuition.
+  econstructor; eauto.
+  eapply eventval_match_inject; eauto.
+  red; auto.
+  red; auto.
+  red; intros; congruence.
+
+  inv H; inv H0. simpl in H1.
+  assert (arg = arg0). eapply eventval_match_determ_2; eauto. subst arg0.
+  intuition.
+Qed.
+
 (** ** Combined semantics of external calls *)
 
 (** Combining the semantics given above for the various kinds of external calls,
@@ -1046,26 +1061,32 @@ Qed.
 This predicate is used in the semantics of all CompCert languages. *)
 
 Definition external_call (ef: external_function): extcall_sem :=
-  match classify_external_function ef with
-  | EF_syscall name sg   => extcall_io_sem name sg
+  match ef with
+  | EF_external name sg  => extcall_io_sem name sg
+  | EF_builtin name sg   => extcall_io_sem name sg
   | EF_vload chunk       => volatile_load_sem chunk
   | EF_vstore chunk      => volatile_store_sem chunk
   | EF_malloc            => extcall_malloc_sem 
   | EF_free              => extcall_free_sem
-  | EF_annotation txt sg => extcall_annot_sem txt sg
+  | EF_memcpy sz al      => extcall_memcpy_sem sz al
+  | EF_annot txt targs   => extcall_annot_sem txt targs
+  | EF_annot_val txt targ=> extcall_annot_val_sem txt targ
   end.
 
 Theorem external_call_spec:
   forall ef, 
   extcall_properties (external_call ef) (ef_sig ef).
 Proof.
-  intros. unfold external_call. destruct (classify_external_function ef). 
+  intros. unfold external_call, ef_sig. destruct ef.
+  apply extcall_io_ok.
   apply extcall_io_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.
 Qed.
 
 Definition external_call_well_typed ef := ec_well_typed (external_call_spec ef).