Support for inlined built-ins.

AST: add ef_inline flag to external functions.
Selection: recognize calls to inlined built-ins and inline them as Sbuiltin.
CminorSel to Asm: added Sbuiltin/Ibuiltin instruction.
PrintAsm: adapted expansion of builtins.
C2Clight: adapted detection of builtins.
Conventions: refactored in a machine-independent part (backend/Conventions)
  and a machine-dependent part (ARCH/SYS/Conventions1).


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

7 files changed, 131 insertions, 103 deletions

diff --git a/cfrontend/C2Clight.ml b/cfrontend/C2Clight.ml
index 2f61d53..035840b 100644
--- a/cfrontend/C2Clight.ml
+++ b/cfrontend/C2Clight.ml
@@ -3,6 +3,7 @@ open Printf
 open Cparser
 open Cparser.C
 open Cparser.Env
+open Cparser.Builtins
 
 open Camlcoq
 open AST
@@ -37,6 +38,72 @@ let warning msg =
   eprintf "%aWarning: %s\n" Cutil.printloc !currentLocation msg
 
 
+(** ** The builtin environment *)
+
+let builtins_generic = {
+  typedefs = [
+    (* keeps GCC-specific headers happy, harmless for others *)
+    "__builtin_va_list", C.TPtr(C.TVoid [], [])
+  ];
+  functions = [
+    (* Floating-point absolute value *)
+    "__builtin_fabs",
+      (TFloat(FDouble, []), [TFloat(FDouble, [])], false);
+    (* The volatile read/volatile write functions *)
+    "__builtin_volatile_read_int8unsigned",
+        (TInt(IUChar, []), [TPtr(TVoid [], [])], false);
+    "__builtin_volatile_read_int8signed",
+        (TInt(ISChar, []), [TPtr(TVoid [], [])], false);
+    "__builtin_volatile_read_int16unsigned",
+        (TInt(IUShort, []), [TPtr(TVoid [], [])], false);
+    "__builtin_volatile_read_int16signed",
+        (TInt(IShort, []), [TPtr(TVoid [], [])], false);
+    "__builtin_volatile_read_int32",
+        (TInt(IInt, []), [TPtr(TVoid [], [])], false);
+    "__builtin_volatile_read_float32",
+        (TFloat(FFloat, []), [TPtr(TVoid [], [])], false);
+    "__builtin_volatile_read_float64",
+         (TFloat(FDouble, []), [TPtr(TVoid [], [])], false);
+    "__builtin_volatile_read_pointer",
+         (TPtr(TVoid [], []), [TPtr(TVoid [], [])], false);
+    "__builtin_volatile_write_int8unsigned",
+        (TVoid [], [TPtr(TVoid [], []); TInt(IUChar, [])], false);
+    "__builtin_volatile_write_int8signed",
+        (TVoid [], [TPtr(TVoid [], []); TInt(ISChar, [])], false);
+    "__builtin_volatile_write_int16unsigned",
+        (TVoid [], [TPtr(TVoid [], []); TInt(IUShort, [])], false);
+    "__builtin_volatile_write_int16signed",
+        (TVoid [], [TPtr(TVoid [], []); TInt(IShort, [])], false);
+    "__builtin_volatile_write_int32",
+        (TVoid [], [TPtr(TVoid [], []); TInt(IInt, [])], false);
+    "__builtin_volatile_write_float32",
+        (TVoid [], [TPtr(TVoid [], []); TFloat(FFloat, [])], false);
+    "__builtin_volatile_write_float64",
+         (TVoid [], [TPtr(TVoid [], []); TFloat(FDouble, [])], false);
+    "__builtin_volatile_write_pointer",
+         (TVoid [], [TPtr(TVoid [], []); TPtr(TVoid [], [])], false);
+    (* Block copy *)
+    "__builtin_memcpy",
+         (TVoid [],
+           [TPtr(TVoid [], []); 
+            TPtr(TVoid [AConst], []); 
+            TInt(Cutil.size_t_ikind, [])],
+          false);
+    "__builtin_memcpy_words",
+         (TVoid [],
+           [TPtr(TVoid [], []); 
+            TPtr(TVoid [AConst], []); 
+            TInt(Cutil.size_t_ikind, [])],
+          false)
+  ]
+}
+
+(* Add processor-dependent builtins *)
+
+let builtins =
+  { typedefs = builtins_generic.typedefs @ CBuiltins.builtins.typedefs;
+    functions = builtins_generic.functions @ CBuiltins.builtins.functions }
+
 (** ** Functions used to handle string literals *)
 
 let stringNum = ref 0   (* number of next global for string literals *)
@@ -104,7 +171,10 @@ let declare_stub_function stub_name stub_type =
   match stub_type with
   | Tfunction(targs, tres) ->
       Datatypes.Coq_pair(intern_string stub_name,
-                         External(intern_string stub_name, targs, tres))
+                         External({ ef_id = intern_string stub_name;
+                                    ef_sig = signature_of_type targs tres;
+                                    ef_inline = false },
+                                  targs, tres))
   | _ -> assert false
 
 let declare_stub_functions k =
@@ -370,6 +440,8 @@ let volatile_write_fun ty =
 let convertTopExpr env e =
   match e.edesc with
   | C.EBinop(C.Oassign, lhs, {edesc = C.ECall(fn, args)}, _) ->
+      convertFuncall env (Some (convertExpr env lhs)) fn args
+(****
       (* Recognize __builtin_fabs and turn it into Clight operator *)
       begin match fn, args with
       | {edesc = C.EVar {name = "__builtin_fabs"}}, [arg1] ->
@@ -378,6 +450,7 @@ let convertTopExpr env e =
       | _ ->
           convertFuncall env (Some (convertExpr env lhs)) fn args
       end
+*****)
   | C.EBinop(C.Oassign, lhs, rhs, _) ->
       if Cutil.is_composite_type env lhs.etyp then
         unsupported "assignment between structs or between unions";
@@ -535,13 +608,23 @@ let convertFundef env fd =
 
 (** External function declaration *)
 
+let noninlined_builtin_functions = [
+    "__builtin_memcpy";
+    "__builtin_memcpy_words"
+]
+
 let convertFundecl env (sto, id, ty, optinit) =
-  match convertTyp env ty with
-  | Tfunction(args, res) ->
-      let id' = intern_string id.name in
-      Datatypes.Coq_pair(id', External(id', args, res))
-  | _ ->
-      assert false
+  let (args, res) =
+    match convertTyp env ty with
+    | Tfunction(args, res) -> (args, res)
+    | _ -> assert false in
+  let id' = intern_string id.name in
+  let ef =
+    { ef_id = id';
+      ef_sig = signature_of_type args res;
+      ef_inline = List.mem_assoc id.name builtins.functions
+          && not (List.mem id.name noninlined_builtin_functions) } in
+  Datatypes.Coq_pair(id', External(ef, args, res))
 
 (** Initializers *)
 
@@ -816,70 +899,3 @@ let atom_alignof a =
   with Not_found ->
     None
 
-(** ** The builtin environment *)
-
-open Cparser.Builtins
-
-let builtins_generic = {
-  typedefs = [
-    (* keeps GCC-specific headers happy, harmless for others *)
-    "__builtin_va_list", C.TPtr(C.TVoid [], [])
-  ];
-  functions = [
-    (* Floating-point absolute value *)
-    "__builtin_fabs",
-      (TFloat(FDouble, []), [TFloat(FDouble, [])], false);
-    (* The volatile read/volatile write functions *)
-    "__builtin_volatile_read_int8unsigned",
-        (TInt(IUChar, []), [TPtr(TVoid [], [])], false);
-    "__builtin_volatile_read_int8signed",
-        (TInt(ISChar, []), [TPtr(TVoid [], [])], false);
-    "__builtin_volatile_read_int16unsigned",
-        (TInt(IUShort, []), [TPtr(TVoid [], [])], false);
-    "__builtin_volatile_read_int16signed",
-        (TInt(IShort, []), [TPtr(TVoid [], [])], false);
-    "__builtin_volatile_read_int32",
-        (TInt(IInt, []), [TPtr(TVoid [], [])], false);
-    "__builtin_volatile_read_float32",
-        (TFloat(FFloat, []), [TPtr(TVoid [], [])], false);
-    "__builtin_volatile_read_float64",
-         (TFloat(FDouble, []), [TPtr(TVoid [], [])], false);
-    "__builtin_volatile_read_pointer",
-         (TPtr(TVoid [], []), [TPtr(TVoid [], [])], false);
-    "__builtin_volatile_write_int8unsigned",
-        (TVoid [], [TPtr(TVoid [], []); TInt(IUChar, [])], false);
-    "__builtin_volatile_write_int8signed",
-        (TVoid [], [TPtr(TVoid [], []); TInt(ISChar, [])], false);
-    "__builtin_volatile_write_int16unsigned",
-        (TVoid [], [TPtr(TVoid [], []); TInt(IUShort, [])], false);
-    "__builtin_volatile_write_int16signed",
-        (TVoid [], [TPtr(TVoid [], []); TInt(IShort, [])], false);
-    "__builtin_volatile_write_int32",
-        (TVoid [], [TPtr(TVoid [], []); TInt(IInt, [])], false);
-    "__builtin_volatile_write_float32",
-        (TVoid [], [TPtr(TVoid [], []); TFloat(FFloat, [])], false);
-    "__builtin_volatile_write_float64",
-         (TVoid [], [TPtr(TVoid [], []); TFloat(FDouble, [])], false);
-    "__builtin_volatile_write_pointer",
-         (TVoid [], [TPtr(TVoid [], []); TPtr(TVoid [], [])], false);
-    (* Block copy *)
-    "__builtin_memcpy",
-         (TVoid [],
-           [TPtr(TVoid [], []); 
-            TPtr(TVoid [AConst], []); 
-            TInt(Cutil.size_t_ikind, [])],
-          false);
-    "__builtin_memcpy_words",
-         (TVoid [],
-           [TPtr(TVoid [], []); 
-            TPtr(TVoid [AConst], []); 
-            TInt(Cutil.size_t_ikind, [])],
-          false)
-  ]
-}
-
-(* Add processor-dependent builtins *)
-
-let builtins =
-  { typedefs = builtins_generic.typedefs @ CBuiltins.builtins.typedefs;
-    functions = builtins_generic.functions @ CBuiltins.builtins.functions }
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 4288409..212c2ad 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -900,9 +900,9 @@ Inductive step: state -> trace -> state -> Prop :=
       step (Callstate (Internal f) vargs k m)
         E0 (State f f.(fn_body) k e m2)
 
-  | step_external_function: forall id targs tres vargs k m vres t m',
-      external_call (external_function id targs tres) ge vargs m t vres m' ->
-      step (Callstate (External id targs tres) vargs k m)
+  | step_external_function: forall ef targs tres vargs k m vres t m',
+      external_call ef  ge vargs m t vres m' ->
+      step (Callstate (External ef targs tres) vargs k m)
          t (Returnstate vres k m')
 
   | step_returnstate_0: forall v f e k m,
@@ -1105,9 +1105,9 @@ with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop :=
       outcome_result_value out f.(fn_return) vres ->
       Mem.free_list m3 (blocks_of_env e) = Some m4 ->
       eval_funcall m (Internal f) vargs t m4 vres
-  | eval_funcall_external: forall m id targs tres vargs t vres m',
-      external_call (external_function id targs tres) ge vargs m t vres m' ->
-      eval_funcall m (External id targs tres) vargs t m' vres.
+  | eval_funcall_external: forall m ef targs tres vargs t vres m',
+      external_call ef ge vargs m t vres m' ->
+      eval_funcall m (External ef targs tres) vargs t m' vres.
 
 Scheme exec_stmt_ind2 := Minimality for exec_stmt Sort Prop
   with eval_funcall_ind2 := Minimality for eval_funcall Sort Prop.
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index cc81d0f..56bef55 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -620,8 +620,8 @@ Definition transl_fundef (f: Csyntax.fundef) : res fundef :=
   match f with
   | Csyntax.Internal g => 
       do tg <- transl_function g; OK(AST.Internal tg)
-  | Csyntax.External id args res =>
-      OK(AST.External (external_function id args res))
+  | Csyntax.External ef args res =>
+      OK(AST.External ef)
   end.
 
 (** ** Translation of programs *)
diff --git a/cfrontend/Cshmgenproof1.v b/cfrontend/Cshmgenproof1.v
index ebc188e..73a3824 100644
--- a/cfrontend/Cshmgenproof1.v
+++ b/cfrontend/Cshmgenproof1.v
@@ -55,27 +55,30 @@ Proof.
 Qed.
 
 Lemma transl_fundef_sig1:
-  forall f tf args res,
+  forall tenv f tf args res,
+  wt_fundef tenv f ->
   transl_fundef f = OK tf ->
   classify_fun (type_of_fundef f) = fun_case_f args res ->
   funsig tf = signature_of_type args res.
 Proof.
-  intros. destruct f; monadInv H. 
+  intros. inv H; monadInv H0.
   monadInv EQ. simpl.  
-  simpl in H0. inversion H0.
+  simpl in H1. inversion H1.
   unfold fn_sig; simpl. unfold signature_of_type. f_equal. 
   apply transl_params_types; auto.
-  simpl. simpl in H0. congruence.
+  simpl. simpl in H1. inv H1. destruct (ef_sig ef); simpl in *. 
+  unfold signature_of_type. congruence.
 Qed.
 
 Lemma transl_fundef_sig2:
-  forall f tf args res,
+  forall tenv f tf args res,
+  wt_fundef tenv f ->
   transl_fundef f = OK tf ->
   type_of_fundef f = Tfunction args res ->
   funsig tf = signature_of_type args res.
 Proof.
   intros. eapply transl_fundef_sig1; eauto.
-  rewrite H0; reflexivity.
+  rewrite H1; reflexivity.
 Qed.
 
 Lemma var_kind_by_value:
diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v
index fb1edbe..0e9e5b1 100644
--- a/cfrontend/Cshmgenproof3.v
+++ b/cfrontend/Cshmgenproof3.v
@@ -1249,7 +1249,8 @@ Proof.
   apply plus_one. econstructor; eauto. 
   exploit transl_expr_correct; eauto.
   exploit transl_exprlist_correct; eauto.
-  eapply transl_fundef_sig1; eauto. congruence.
+  eapply transl_fundef_sig1; eauto. eapply functions_well_typed; eauto.
+  congruence.
   econstructor; eauto. eapply functions_well_typed; eauto. 
   econstructor; eauto. simpl. auto. 
 
@@ -1263,7 +1264,8 @@ Proof.
   apply plus_one. econstructor; eauto. 
   exploit transl_expr_correct; eauto.
   exploit transl_exprlist_correct; eauto.
-  eapply transl_fundef_sig1; eauto. congruence.
+  eapply transl_fundef_sig1; eauto. eapply functions_well_typed; eauto.
+  congruence.
   econstructor; eauto. eapply functions_well_typed; eauto.
   econstructor; eauto. simpl; auto. 
 
@@ -1595,10 +1597,15 @@ Proof.
     eapply Genv.find_funct_ptr_symbol_inversion; eauto.
   destruct H as [targs D].
   assert (targs = Tnil). 
-    inv H0. inv H10. simpl in D. unfold type_of_function in D. rewrite <- H5 in D. 
+    inv H0.
+    (* internal function *)
+    inv H10. simpl in D. unfold type_of_function in D. rewrite <- H5 in D. 
     simpl in D. congruence.
+    (* external function *)
     simpl in D. inv D.
-    exploit external_call_arity; eauto. destruct targs; simpl; congruence.
+    exploit external_call_arity; eauto. intro ARITY.
+    exploit function_ptr_well_typed; eauto. intro WT. inv WT.
+    rewrite H5 in ARITY. destruct targs; simpl in ARITY; congruence.
   subst targs. 
   assert (funsig tf = signature_of_type Tnil (Tint I32 Signed)).
     eapply transl_fundef_sig2; eauto. 
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index c82aa9e..9d0791e 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -210,7 +210,7 @@ Record function : Type := mkfunction {
 
 Inductive fundef : Type :=
   | Internal: function -> fundef
-  | External: ident -> typelist -> type -> fundef.
+  | External: external_function -> typelist -> type -> fundef.
 
 (** ** Programs *)
 
@@ -639,7 +639,3 @@ Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ :=
 
 Definition signature_of_type (args: typelist) (res: type) : signature :=
   mksignature (typlist_of_typelist args) (opttyp_of_type res).
-
-Definition external_function
-    (id: ident) (targs: typelist) (tres: type) : AST.external_function :=
-  mkextfun id (signature_of_type targs tres).
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index b147fbd..8e089f1 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -155,8 +155,10 @@ Inductive wt_fundef: typenv -> fundef -> Prop :=
   | wt_fundef_Internal: forall env f,
       wt_function env f ->
       wt_fundef env (Internal f)
-  | wt_fundef_External: forall env id args res,
-      wt_fundef env (External id args res).
+  | wt_fundef_External: forall env ef args res,
+      (ef_sig ef).(sig_args) = typlist_of_typelist args ->
+      (ef_sig ef).(sig_res) = opttyp_of_type res ->
+      wt_fundef env (External ef args res).
 
 Definition add_global_var
      (env: typenv) (id_v: ident * globvar type) : typenv :=
@@ -410,8 +412,12 @@ Qed.
 Definition typecheck_fundef (main: ident) (env: typenv) (id_fd: ident * fundef) : bool :=
   let (id, fd) := id_fd in
   match fd with
-  | Internal f => typecheck_function env f
-  | External _ _ _ => true
+  | Internal f =>
+      typecheck_function env f
+  | External ef targs tres =>
+      let s := ef_sig ef in
+      list_eq_dec typ_eq s.(sig_args) (typlist_of_typelist targs) 
+      && opt_typ_eq s.(sig_res) (opttyp_of_type tres)
   end &&
   if ident_eq id main
   then match type_of_fundef fd with
@@ -430,8 +436,8 @@ Proof.
   intros. unfold typecheck_fundef in H; TrueInv.
   split. 
     destruct fd.
-    constructor. apply typecheck_function_correct; auto. 
-    constructor.
+    constructor. apply typecheck_function_correct; auto.
+    TrueInv. constructor; eapply proj_sumbool_true; eauto.
   intro. destruct (ident_eq id main). 
   destruct (type_of_fundef fd); try discriminate. 
   exists t; decEq; auto. apply eq_type_correct; auto.