From 9c7c84cc40eaacc1e2c13091165785cddecba5ad Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 29 Jun 2010 08:27:14 +0000
Subject: 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
---
 backend/RTLtyping.v | 30 ++++++++++++++++++++++++++----
 1 file changed, 26 insertions(+), 4 deletions(-)

(limited to 'backend/RTLtyping.v')

diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 68f38c0d..533c47a9 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -25,7 +25,7 @@ Require Import Integers.
 Require Import Events.
 Require Import Smallstep.
 Require Import RTL.
-Require Conventions.
+Require Import Conventions.
 
 (** * The type system *)
 
@@ -104,8 +104,15 @@ Inductive wt_instr : instruction -> Prop :=
       match ros with inl r => env r = Tint | inr s => True end ->
       sig.(sig_res) = funct.(fn_sig).(sig_res) ->
       List.map env args = sig.(sig_args) ->
-      Conventions.tailcall_possible sig ->
+      tailcall_possible sig ->
       wt_instr (Itailcall sig ros args)
+  | wt_Ibuiltin:
+      forall ef args res s,
+      List.map env args = (ef_sig ef).(sig_args) ->
+      env res = proj_sig_res (ef_sig ef) ->
+      arity_ok (ef_sig ef).(sig_args) = true ->
+      valid_successor s ->
+      wt_instr (Ibuiltin ef args res s)
   | wt_Icond:
       forall cond args s1 s2,
       List.map env args = type_of_condition cond ->
@@ -225,7 +232,12 @@ Definition check_instr (i: instruction) : bool :=
       match ros with inl r => check_reg r Tint | inr s => true end
       && check_regs args sig.(sig_args)
       && opt_typ_eq sig.(sig_res) funct.(fn_sig).(sig_res)
-      && Conventions.tailcall_is_possible sig
+      && tailcall_is_possible sig
+  | Ibuiltin ef args res s =>
+      check_regs args (ef_sig ef).(sig_args)
+      && check_reg res (proj_sig_res (ef_sig ef))
+      && arity_ok (ef_sig ef).(sig_args)
+      && check_successor s
   | Icond cond args s1 s2 =>
       check_regs args (type_of_condition cond)
       && check_successor s1
@@ -331,7 +343,13 @@ Proof.
   destruct s0; auto. apply check_reg_correct; auto.
   eapply proj_sumbool_true; eauto.
   apply check_regs_correct; auto.
-  apply Conventions.tailcall_is_possible_correct; auto.
+  apply tailcall_is_possible_correct; auto.
+  (* builtin *)
+  constructor.
+  apply check_regs_correct; auto.
+  apply check_reg_correct; auto.
+  auto.
+  apply check_successor_correct; auto.
   (* cond *)
   constructor. apply check_regs_correct; auto.
   apply check_successor_correct; auto.
@@ -541,6 +559,10 @@ Proof.
   econstructor; eauto.
   rewrite H6; auto.
   rewrite <- H7. apply wt_regset_list. auto.
+  (* Ibuiltin *)
+  econstructor; eauto.
+  apply wt_regset_assign. auto. 
+  rewrite H6. eapply external_call_well_typed; eauto. 
   (* Icond *)
   econstructor; eauto.
   econstructor; eauto.
-- 
cgit