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

5 files changed, 195 insertions, 54 deletions

diff --git a/ia32/Asm.v b/ia32/Asm.v
index 0c4a153..f3809c4 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -186,7 +186,12 @@ Inductive instruction: Type :=
   | Plabel(l: label)
   | Pallocframe(sz: Z)(ofs_ra ofs_link: int)
   | Pfreeframe(sz: Z)(ofs_ra ofs_link: int)
-  | Pbuiltin(ef: external_function)(args: list preg)(res: preg).
+  | Pbuiltin(ef: external_function)(args: list preg)(res: preg)
+  | Pannot(ef: external_function)(args: list annot_param)
+
+with annot_param : Type :=
+  | APreg: preg -> annot_param
+  | APstack: memory_chunk -> Z -> annot_param.
 
 Definition code := list instruction.
 Definition fundef := AST.fundef code.
@@ -655,6 +660,8 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       end
   | Pbuiltin ef args res =>
       Stuck                             (**r treated specially below *)
+  | Pannot ef args =>
+      Stuck                             (**r treated specially below *)
   end.
 
 (** Translation of the LTL/Linear/Mach view of machine registers
@@ -696,20 +703,27 @@ Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop :=
       Mem.loadv Mfloat64 m (Val.add (rs (IR ESP)) (Vint (Int.repr bofs))) = Some v ->
       extcall_arg rs m (S (Outgoing ofs Tfloat)) v.
 
-Inductive extcall_args (rs: regset) (m: mem): list loc -> list val -> Prop :=
-  | extcall_args_nil:
-      extcall_args rs m nil nil
-  | extcall_args_cons: forall l1 ll v1 vl,
-      extcall_arg rs m l1 v1 -> extcall_args rs m ll vl ->
-      extcall_args rs m (l1 :: ll) (v1 :: vl).
-
 Definition extcall_arguments
     (rs: regset) (m: mem) (sg: signature) (args: list val) : Prop :=
-  extcall_args rs m (loc_arguments sg) args.
+  list_forall2 (extcall_arg rs m) (loc_arguments sg) args.
 
 Definition loc_external_result (sg: signature) : preg :=
   preg_of (loc_result sg).
 
+(** Extract the values of the arguments of an annotation. *)
+
+Inductive annot_arg (rs: regset) (m: mem): annot_param -> val -> Prop :=
+  | annot_arg_reg: forall r,
+      annot_arg rs m (APreg r) (rs r)
+  | annot_arg_stack: forall chunk ofs stk base v,
+      rs (IR ESP) = Vptr stk base ->
+      Mem.load chunk m stk (Int.unsigned base + ofs) = Some v ->
+      annot_arg rs m (APstack chunk ofs) v.
+
+Definition annot_arguments
+    (rs: regset) (m: mem) (params: list annot_param) (args: list val) : Prop :=
+  list_forall2 (annot_arg rs m) params args.
+
 (** Execution of the instruction at [rs#PC]. *)
 
 Inductive state: Type :=
@@ -734,13 +748,22 @@ Inductive step: state -> trace -> state -> Prop :=
                                 #XMM6 <- Vundef #XMM7 <- Vundef
                                 #ST0 <- Vundef
                                 #res <- v)) m')
+  | exec_step_annot:
+      forall b ofs c ef args rs m vargs t v m',
+      rs PC = Vptr b ofs ->
+      Genv.find_funct_ptr ge b = Some (Internal c) ->
+      find_instr (Int.unsigned ofs) c = Some (Pannot ef args) ->
+      annot_arguments rs m args vargs ->
+      external_call ef ge vargs m t v m' ->
+      step (State rs m) t
+           (State (nextinstr rs) m')
   | exec_step_external:
       forall b ef args res rs m t rs' m',
       rs PC = Vptr b Int.zero ->
       Genv.find_funct_ptr ge b = Some (External ef) ->
       external_call ef ge args m t res m' ->
-      extcall_arguments rs m ef.(ef_sig) args ->
-      rs' = (rs#(loc_external_result ef.(ef_sig)) <- res
+      extcall_arguments rs m (ef_sig ef) args ->
+      rs' = (rs#(loc_external_result (ef_sig ef)) <- res
                #PC <- (rs RA)) ->
       step (State rs m) t (State rs' m').
 
diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v
index 0e14dee..c87167b 100644
--- a/ia32/Asmgen.v
+++ b/ia32/Asmgen.v
@@ -441,6 +441,14 @@ Definition transl_store (chunk: memory_chunk)
       do r <- freg_of src; OK(Pmovsd_mf am r :: k)
   end.
 
+(** Translation of arguments to annotations *)
+
+Definition transl_annot_param (p: Mach.annot_param) : Asm.annot_param :=
+  match p with
+  | Mach.APreg r => APreg (preg_of r)
+  | Mach.APstack chunk ofs => APstack chunk ofs
+  end.
+
 (** Translation of a Mach instruction. *)
 
 Definition transl_instr (f: Mach.function) (i: Mach.instruction)
@@ -486,6 +494,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
           Pret :: k)
   | Mbuiltin ef args res =>
       OK (Pbuiltin ef (List.map preg_of args) (preg_of res) :: k)
+  | Mannot ef args =>
+      OK (Pannot ef (map transl_annot_param args) :: k)
   end.
 
 (** Translation of a code sequence *)
diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v
index 304b5da..a9b9f3b 100644
--- a/ia32/Asmgenproof.v
+++ b/ia32/Asmgenproof.v
@@ -479,6 +479,7 @@ Opaque loadind.
   destruct s0; monadInv H; auto.
   destruct s0; monadInv H; auto. 
   monadInv H; auto.
+  monadInv H; auto.
   inv H; simpl. destruct (peq lbl l). congruence. auto. 
   monadInv H; auto.
   eapply trans_eq. eapply transl_cond_label; eauto. auto. 
@@ -1009,6 +1010,36 @@ Proof.
   congruence.
 Qed.
 
+Lemma exec_Mannot_prop:
+  forall (s : list stackframe) (f : block) (sp : val)
+         (ms : Mach.regset) (m : mem) (ef : external_function)
+         (args : list Mach.annot_param) (b : list Mach.instruction)
+         (vargs: list val) (t : trace) (v : val) (m' : mem),
+  Machsem.annot_arguments ms m sp args vargs ->
+  external_call ef ge vargs m t v m' ->
+  exec_instr_prop (Machsem.State s f sp (Mannot ef args :: b) ms m) t
+                  (Machsem.State s f sp b ms m').
+Proof.
+  intros; red; intros; inv MS.
+  inv AT. monadInv H4. 
+  exploit functions_transl; eauto. intro FN.
+  generalize (transf_function_no_overflow _ _ H3); intro NOOV.
+  exploit annot_arguments_match; eauto. intros [vargs' [P Q]]. 
+  exploit external_call_mem_extends; eauto.
+  intros [vres' [m2' [A [B [C D]]]]].
+  left. econstructor; split. apply plus_one. 
+  eapply exec_step_annot. eauto. eauto.
+  eapply find_instr_tail; eauto. eauto.
+  eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact varinfo_preserved.
+  eapply match_states_intro with (ep := false); eauto with coqlib.
+  unfold nextinstr. rewrite Pregmap.gss. 
+  rewrite <- H1; simpl. econstructor; eauto.
+  eapply code_tail_next_int; eauto. 
+  apply agree_nextinstr. auto.
+  congruence.
+Qed.
+
 Lemma exec_Mcond_true_prop:
   forall (s : list stackframe) (fb : block) (f : function) (sp : val)
          (cond : condition) (args : list mreg) (lbl : Mach.label)
@@ -1224,6 +1255,7 @@ Proof
            exec_Mcall_prop
            exec_Mtailcall_prop
            exec_Mbuiltin_prop
+           exec_Mannot_prop
            exec_Mgoto_prop
            exec_Mcond_true_prop
            exec_Mcond_false_prop
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v
index eb107ea..b3e7aaa 100644
--- a/ia32/Asmgenproof1.v
+++ b/ia32/Asmgenproof1.v
@@ -369,13 +369,13 @@ Qed.
 Lemma extcall_args_match:
   forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' ->
   forall ll vl,
-  Machsem.extcall_args ms m sp ll vl ->
-  exists vl', Asm.extcall_args rs m' ll vl' /\ Val.lessdef_list vl vl'.
+  list_forall2 (Machsem.extcall_arg ms m sp) ll vl ->
+  exists vl', list_forall2 (Asm.extcall_arg rs m') ll vl' /\ Val.lessdef_list vl vl'.
 Proof.
   induction 3.
   exists (@nil val); split; constructor.
   exploit extcall_arg_match; eauto. intros [v1' [A B]].
-  exploit IHextcall_args; eauto. intros [vl' [C D]].
+  destruct IHlist_forall2 as [vl' [C D]].
   exists(v1' :: vl'); split. constructor; auto. constructor; auto.
 Qed.
 
@@ -390,6 +390,40 @@ Proof.
   eapply extcall_args_match; eauto.
 Qed.
 
+(** Translation of arguments to annotations. *)
+
+Lemma annot_arg_match:
+  forall ms sp rs m m' p v,
+  agree ms sp rs ->
+  Mem.extends m m' ->
+  Machsem.annot_arg ms m sp p v ->
+  exists v', Asm.annot_arg rs m' (transl_annot_param p) v' /\ Val.lessdef v v'.
+Proof.
+  intros. inv H1; simpl.
+(* reg *)
+  exists (rs (preg_of r)); split. 
+  unfold preg_of. destruct (mreg_type r); constructor. 
+  eapply preg_val; eauto.
+(* stack *)
+  exploit Mem.load_extends; eauto. intros [v' [A B]].
+  exists v'; split; auto. 
+  inv H. econstructor; eauto. 
+Qed.
+
+Lemma annot_arguments_match:
+  forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' ->
+  forall pl vl,
+  Machsem.annot_arguments ms m sp pl vl ->
+  exists vl', Asm.annot_arguments rs m' (map transl_annot_param pl) vl'
+           /\ Val.lessdef_list vl vl'.
+Proof.
+  induction 3; intros. 
+  exists (@nil val); split. constructor. constructor.
+  exploit annot_arg_match; eauto. intros [v1' [A B]].
+  destruct IHlist_forall2 as [vl' [C D]].
+  exists (v1' :: vl'); split; constructor; auto.
+Qed.
+
 (** * Execution of straight-line code *)
 
 Section STRAIGHTLINE.
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index 9facf85..c9ee970 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -17,6 +17,7 @@ open Datatypes
 open Camlcoq
 open Sections
 open AST
+open Memdata
 open Asm
 
 (* Recognition of target ABI and asm syntax *)
@@ -217,20 +218,20 @@ let need_masks = ref false
 
 (* Built-in functions *)
 
-(* Built-ins.  They come in two flavors: 
+(* Built-ins.  They come in three flavors: 
+   - annotation statements: take their arguments in registers or stack
+     locations; generate no code;
    - inlined by the compiler: take their arguments in arbitrary
      registers; preserve all registers except ECX, EDX, XMM6 and XMM7
    - inlined while printing asm code; take their arguments in
      locations dictated by the calling conventions; preserve
      callee-save regs only. *)
 
-(* Handling of __builtin_annotation *)
-
-let re_builtin_annotation = Str.regexp "__builtin_annotation_\"\\(.*\\)\"$"
+(* Handling of annotations *)
 
 let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*"
 
-let print_annotation oc txt args res =
+let print_annot_text print_arg oc txt args =
   fprintf oc "%s annotation: " comment;
   let print_fragment = function
   | Str.Text s ->
@@ -240,28 +241,36 @@ let print_annotation oc txt args res =
   | Str.Delim s ->
       let n = int_of_string (String.sub s 1 (String.length s - 1)) in
       try
-        preg oc (List.nth args (n-1))
+        print_arg oc (List.nth args (n-1))
       with Failure _ ->
         fprintf oc "<bad parameter %s>" s in
   List.iter print_fragment (Str.full_split re_annot_param txt);
-  fprintf oc "\n";
+  fprintf oc "\n"
+
+let print_annot_stmt oc txt args =
+  let print_annot_param oc = function
+  | APreg r -> preg oc r
+  | APstack(chunk, ofs) ->
+      fprintf oc "mem(ESP + %a, %a)" coqint ofs coqint (size_chunk chunk) in
+  print_annot_text print_annot_param oc txt args
+
+let print_annot_val oc txt args res =
+  print_annot_text preg oc txt args;
   match args, res with
-  | [], _ -> ()
   | IR src :: _, IR dst ->
       if dst <> src then fprintf oc "	movl	%a, %a\n" ireg src ireg dst
   | FR src :: _, FR dst ->
       if dst <> src then fprintf oc "	movsd	%a, %a\n" freg src freg dst
   | _, _ -> assert false
 
-(* Handling of __builtin_memcpy_alX_szY *)
-
-let re_builtin_memcpy =
-   Str.regexp "__builtin_memcpy\\(_al\\([248]\\)\\)?_sz\\([0-9]+\\)$"
+(* Handling of memcpy *)
 
 (* Unaligned memory accesses are quite fast on IA32, so use large
    memory accesses regardless of alignment. *)
 
-let print_builtin_memcpy oc sz dst src =
+let print_builtin_memcpy oc sz al args =
+  let (dst, src) =
+    match args with [IR d; IR s] -> (d, s) | _ -> assert false in
   let tmp =
     if src <> ECX && dst <> ECX then ECX
     else if src <> EDX && dst <> EDX then EDX
@@ -284,54 +293,73 @@ let print_builtin_memcpy oc sz dst src =
       fprintf oc "	movb	%a, %d(%a)\n" ireg8 tmp ofs ireg dst;
       copy (ofs + 1) (sz - 1)
     end in
+  fprintf oc "%s begin builtin __builtin_memcpy, size = %d, alignment = %d\n"
+          comment sz al;
   if tmp = EAX && sz mod 4 <> 0 then
     fprintf oc "	movd	%a, %a\n" ireg EAX freg XMM7;
   copy 0 sz;
   if tmp = EAX && sz mod 4 <> 0 then
-    fprintf oc "	movd	%a, %a\n" freg XMM7 ireg EAX
+    fprintf oc "	movd	%a, %a\n" freg XMM7 ireg EAX;
+  fprintf oc "%s end builtin __builtin_memcpy\n" comment
 
-(* Handling of compiler-inlined builtins *)
+(* Handling of volatile reads and writes *)
 
-let print_builtin_inlined oc name args res =
-  fprintf oc "%s begin builtin %s\n" comment name;
-  begin match name, args, res with
-  (* Volatile reads *)
-  | "__builtin_volatile_read_int8unsigned", [IR addr], IR res ->
+let print_builtin_vload oc chunk args res =
+  fprintf oc "%s begin builtin __builtin_volatile_read\n" comment;
+  begin match chunk, args, res with
+  | Mint8unsigned, [IR addr], IR res ->
       fprintf oc "	movzbl	0(%a), %a\n" ireg addr ireg res
-  | "__builtin_volatile_read_int8signed", [IR addr], IR res ->
+  | Mint8signed, [IR addr], IR res ->
       fprintf oc "	movsbl	0(%a), %a\n" ireg addr ireg res
-  | "__builtin_volatile_read_int16unsigned", [IR addr], IR res ->
+  | Mint16unsigned, [IR addr], IR res ->
       fprintf oc "	movzwl	0(%a), %a\n" ireg addr ireg res
-  | "__builtin_volatile_read_int16signed", [IR addr], IR res ->
+  | Mint16signed, [IR addr], IR res ->
       fprintf oc "	movswl	0(%a), %a\n" ireg addr ireg res
-  | ("__builtin_volatile_read_int32"|"__builtin_volatile_read_pointer"), [IR addr], IR res ->
+  | Mint32, [IR addr], IR res ->
       fprintf oc "	movl	0(%a), %a\n" ireg addr ireg res
-  | "__builtin_volatile_read_float32", [IR addr], FR res ->
+  | Mfloat32, [IR addr], FR res ->
       fprintf oc "	cvtss2sd 0(%a), %a\n" ireg addr freg res
-  | "__builtin_volatile_read_float64", [IR addr], FR res ->
+  | Mfloat64, [IR addr], FR res ->
       fprintf oc "	movsd	0(%a), %a\n" ireg addr freg res
-  (* Volatile writes *)
-  | ("__builtin_volatile_write_int8unsigned"|"__builtin_volatile_write_int8signed"), [IR addr; IR src], _ ->
+  | _ ->
+      assert false
+  end;
+  fprintf oc "%s end builtin __builtin_volatile_read\n" comment
+
+let print_builtin_vstore oc chunk args =
+  fprintf oc "%s begin builtin __builtin_volatile_write\n" comment;
+  begin match chunk, args with
+  | (Mint8signed | Mint8unsigned), [IR addr; IR src] ->
       if Asmgen.low_ireg src then
         fprintf oc "	movb	%a, 0(%a)\n" ireg8 src ireg addr
       else begin
         fprintf oc "	movl	%a, %%ecx\n" ireg src;
         fprintf oc "	movb	%%cl, 0(%a)\n" ireg addr
       end
-  | ("__builtin_volatile_write_int16unsigned"|"__builtin_volatile_write_int16signed"), [IR addr; IR src], _ ->
+  | (Mint16signed | Mint16unsigned), [IR addr; IR src] ->
       if Asmgen.low_ireg src then
         fprintf oc "	movw	%a, 0(%a)\n" ireg16 src ireg addr
       else begin
         fprintf oc "	movl	%a, %%ecx\n" ireg src;
         fprintf oc "	movw	%%cx, 0(%a)\n" ireg addr
       end
-  | ("__builtin_volatile_write_int32"|"__builtin_volatile_write_pointer"), [IR addr; IR src], _ ->
+  | Mint32, [IR addr; IR src] ->
       fprintf oc "	movl	%a, 0(%a)\n" ireg src ireg addr
-  | "__builtin_volatile_write_float32", [IR addr; FR src], _ ->
+  | Mfloat32, [IR addr; FR src] ->
       fprintf oc "	cvtsd2ss %a, %%xmm7\n" freg src;
       fprintf oc "	movss	%%xmm7, 0(%a)\n" ireg addr
-  | "__builtin_volatile_write_float64", [IR addr; FR src], _ ->
+  | Mfloat64, [IR addr; FR src] ->
       fprintf oc "	movsd	%a, 0(%a)\n" freg src ireg addr
+  | _ ->
+      assert false
+  end;
+  fprintf oc "%s end builtin __builtin_volatile_write\n" comment
+
+(* Handling of compiler-inlined builtins *)
+
+let print_builtin_inline oc name args res =
+  fprintf oc "%s begin builtin %s\n" comment name;
+  begin match name, args, res with
   (* Memory accesses *)
   | "__builtin_read_int16_reversed", [IR a1], IR res ->
       let tmp = if Asmgen.low_ireg res then res else ECX in
@@ -380,10 +408,6 @@ let print_builtin_inlined oc name args res =
         fprintf oc "	movsd	%a, %a\n" freg a1 freg res;
         fprintf oc "	minsd	%a, %a\n" freg a2 freg res
       end
-  (* Inlined memcpy *)
-  | name, [IR dst; IR src], _ when Str.string_match re_builtin_memcpy name 0 ->
-      let sz = int_of_string (Str.matched_group 3 name) in
-      print_builtin_memcpy oc sz dst src
   (* Catch-all *)  
   | _ ->
       invalid_arg ("unrecognized builtin " ^ name)
@@ -655,10 +679,28 @@ let print_instruction oc = function
       let sz = sp_adjustment sz in
       fprintf oc "	addl	$%ld, %%esp\n" sz
   | Pbuiltin(ef, args, res) ->
-      let name = extern_atom ef.ef_id in
-      if Str.string_match re_builtin_annotation name 0
-      then print_annotation oc (Str.matched_group 1 name) args res
-      else print_builtin_inlined oc name args res
+      begin match ef with
+      | EF_builtin(name, sg) ->
+          print_builtin_inline oc (extern_atom name) args res
+      | EF_vload chunk ->
+          print_builtin_vload oc chunk args res
+      | EF_vstore chunk ->
+          print_builtin_vstore oc chunk args
+      | EF_memcpy(sz, al) ->
+          print_builtin_memcpy oc (Int32.to_int (camlint_of_coqint sz))
+                                  (Int32.to_int (camlint_of_coqint al)) args
+      | EF_annot_val(txt, targ) ->
+          print_annot_val oc (extern_atom txt) args res
+      | _ ->
+          assert false
+      end
+  | Pannot(ef, args) ->
+      begin match ef with
+      | EF_annot(txt, targs) ->
+          print_annot_stmt oc (extern_atom txt) args
+      | _ ->
+          assert false
+      end
 
 let print_literal oc (lbl, n) =
   fprintf oc "%a:	.quad	0x%Lx\n" label lbl n