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, 212 insertions, 75 deletions

diff --git a/arm/Asm.v b/arm/Asm.v
index 051b7e47..7664f242 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -170,7 +170,12 @@ Inductive instruction : Type :=
   | Plabel: label -> instruction                   (**r define a code label *)
   | Ploadsymbol: ireg -> ident -> int -> instruction (**r load the address of a symbol *)
   | Pbtbl: ireg -> list label -> instruction       (**r N-way branch through a jump table *)
-  | Pbuiltin: external_function -> list preg -> preg -> instruction. (**r built-in *)
+  | Pbuiltin: external_function -> list preg -> preg -> instruction  (**r built-in function *)
+  | Pannot: external_function -> list annot_param -> instruction (**r annotation statement *)
+
+with annot_param : Type :=
+  | APreg: preg -> annot_param
+  | APstack: memory_chunk -> Z -> annot_param.
 
 (** The pseudo-instructions are the following:
 
@@ -531,6 +536,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       | _ => Error
       end
   | Pbuiltin ef args res => Error    (**r treated specially below *)
+  | Pannot ef args => Error          (**r treated specially below *)
   end.
 
 (** Translation of the LTL/Linear/Mach view of machine registers
@@ -584,20 +590,27 @@ Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop :=
       Mem.loadv Mfloat64 m (Val.add (rs (IR IR13)) (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 IR13) = 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 :=
@@ -618,6 +631,14 @@ Inductive step: state -> trace -> state -> Prop :=
       find_instr (Int.unsigned ofs) c = Some (Pbuiltin ef args res) ->
       external_call ef ge (map rs args) m t v m' ->
       step (State rs m) t (State (nextinstr(rs # 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 ->
diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index a1f8d960..91a636b1 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -436,6 +436,14 @@ Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) :=
   | Tfloat => storeind_float (freg_of src) base ofs 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) (k: code) :=
@@ -494,6 +502,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
         (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbsymb symb :: k)
   | Mbuiltin ef args res =>
       Pbuiltin ef (map preg_of args) (preg_of res) :: k
+  | Mannot ef args =>
+      Pannot ef (map transl_annot_param args) :: k
   | Mlabel lbl =>
       Plabel lbl :: k
   | Mgoto lbl =>
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index b7a7ff05..82e54c86 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -822,7 +822,8 @@ Proof.
 Qed.
 
 Lemma storev_8_signed_unsigned:
  forall m a v,
  Mem.storev Mint8signed m a v = Mem.storev Mint8unsigned m a v.
Proof.
  intros. unfold Mem.storev. 
-  destruct a; auto.
  apply Mem.store_signed_unsigned_8.
Qed.

Lemma storev_16_signed_unsigned:
  forall m a v,
  Mem.storev Mint16signed m a v = Mem.storev Mint16unsigned m a v.
Proof.
  intros. unfold Mem.storev. destruct a; auto.
  apply Mem.store_signed_unsigned_16.
Qed.
+  destruct a; auto. 
  apply Mem.store_signed_unsigned_8. 
Qed.
+
Lemma storev_16_signed_unsigned:
  forall m a v,
  Mem.storev Mint16signed m a v = Mem.storev Mint16unsigned m a v.
Proof.
  intros. unfold Mem.storev. destruct a; auto. 
  apply Mem.store_signed_unsigned_16. 
Qed.
 

 Lemma exec_Mstore_prop:
   forall (s : list stackframe) (fb : block) (sp : val)
@@ -1016,6 +1017,35 @@ Proof.
   intros. rewrite Pregmap.gso; auto.
 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. simpl in H3.
+  generalize (functions_transl _ _ FIND); intro FN.
+  generalize (functions_transl_no_overflow _ _ FIND); 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.
+  econstructor; eauto with coqlib.
+  unfold nextinstr. rewrite Pregmap.gss. 
+  rewrite <- H1; simpl. econstructor; auto.
+  eapply code_tail_next_int; eauto. 
+  apply agree_nextinstr. auto.
+Qed.
+
 Lemma exec_Mgoto_prop:
   forall (s : list stackframe) (fb : block) (f : function) (sp : val)
          (lbl : Mach.label) (c : list Mach.instruction) (ms : Mach.regset)
@@ -1335,6 +1365,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/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index 9312f309..d6ad203a 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -337,14 +337,14 @@ 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.
+  induction 3; intros. 
+  exists (@nil val); split. constructor. constructor.
   exploit extcall_arg_match; eauto. intros [v1' [A B]].
-  exploit IHextcall_args; eauto. intros [vl' [C D]].
-  exists(v1' :: vl'); split. constructor; auto. constructor; auto.
+  destruct IHlist_forall2 as [vl' [C D]].
+  exists (v1' :: vl'); split; constructor; auto.
 Qed.
 
 Lemma extcall_arguments_match:
@@ -358,6 +358,38 @@ 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. 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/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 4f5d1cd8..cc42f3c2 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -17,6 +17,7 @@ open Datatypes
 open Camlcoq
 open Sections
 open AST
+open Memdata
 open Asm
 
 (* On-the-fly label renaming *)
@@ -42,7 +43,9 @@ module IdentSet = Set.Make(struct type t = ident let compare = compare end)
 
 let extfuns = (ref IdentSet.empty)
 
-let need_stub ef = List.mem Tfloat ef.ef_sig.sig_args
+let need_stub = function
+  | EF_external(name, sg) -> List.mem Tfloat sg.sig_args
+  | _ -> false
 
 let record_extfun (Coq_pair(name, defn)) =
   match defn with
@@ -216,20 +219,21 @@ let call_helper oc fn dst arg1 arg2 =
   (* ... for a total of at most 7 instructions *)
   7
 
-(* 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 IR14
+     registers; preserve all registers the temporaries
+     (IR10, IR12, IR14, FP2, FP4)
    - 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 ->
@@ -239,28 +243,35 @@ 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";
-  begin match args, res with
-  | [], _ -> 0
+  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(R1 + %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 0 else (fprintf oc "	mr	%a, %a\n" ireg dst ireg src; 1)
+      if dst = src then 0 else (fprintf oc "	mov	%a, %a\n" ireg dst ireg src; 1)
   | FR src :: _, FR dst ->
-      if dst = src then 0 else (fprintf oc "	fmr	%a, %a\n" freg dst freg src; 1)
+      if dst = src then 0 else (fprintf oc "	mvfd	%a, %a\n" freg dst freg src; 1)
   | _, _ -> assert false
-  end
-
-(* Handling of __builtin_memcpy_alX_szY *)
 
-let re_builtin_memcpy =
-   Str.regexp "__builtin_memcpy\\(_al\\([248]\\)\\)?_sz\\([0-9]+\\)$"
+(* Handling of memcpy *)
 
 (* The ARM has strict alignment constraints. *)
 
-let print_builtin_memcpy oc sz al 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 rec copy ofs sz ninstr =
     if sz >= 4 && al >= 4 then begin
       fprintf oc "	ldr	%a, [%a, #%d]\n" ireg IR14 ireg src ofs;
@@ -276,49 +287,63 @@ let print_builtin_memcpy oc sz al dst src =
       copy (ofs + 1) (sz - 1) (ninstr + 2)
     end else
       ninstr in
-  copy 0 sz 0
+  fprintf oc "%s begin builtin __builtin_memcpy, size = %d, alignment = %d\n"
+          comment sz al;
+  let n = copy 0 sz 0 in
+  fprintf oc "%s end builtin __builtin_memcpy\n" comment; n
+
+let print_builtin_vload oc chunk args res =
+  fprintf oc "%s begin builtin __builtin_volatile_read\n" comment;
+  let n = 
+    begin match chunk, args, res with
+    | Mint8unsigned, [IR addr], IR res ->
+        fprintf oc "	ldrb	%a, [%a, #0]\n" ireg res ireg addr; 1
+    | Mint8signed, [IR addr], IR res ->
+        fprintf oc "	ldrsb	%a, [%a, #0]\n" ireg res ireg addr; 1
+    | Mint16unsigned, [IR addr], IR res ->
+        fprintf oc "	ldrh	%a, [%a, #0]\n" ireg res ireg addr; 1
+    | Mint16signed, [IR addr], IR res ->
+        fprintf oc "	ldrsh	%a, [%a, #0]\n" ireg res ireg addr; 1
+    | Mint32, [IR addr], IR res ->
+        fprintf oc "	ldr	%a, [%a, #0]\n" ireg res ireg addr; 1
+    | Mfloat32, [IR addr], FR res ->
+        fprintf oc "	ldfs	%a, [%a, #0]\n" freg res ireg addr;
+        fprintf oc "	mvfd	%a, %a\n" freg res freg res; 2
+    | Mfloat64, [IR addr], FR res ->
+        fprintf oc "	ldfd	%a, [%a, #0]\n" freg res ireg addr; 1
+    | _ ->
+        assert false
+    end in
+  fprintf oc "%s end builtin __builtin_volatile_read\n" comment; n
+
+let print_builtin_vstore oc chunk args =
+  fprintf oc "%s begin builtin __builtin_volatile_write\n" comment;
+  let n =
+    begin match chunk, args with
+    | (Mint8signed | Mint8unsigned), [IR addr; IR src] ->
+        fprintf oc "	strb	%a, [%a, #0]\n" ireg src ireg addr; 1
+    | (Mint16signed | Mint16unsigned), [IR addr; IR src] ->
+        fprintf oc "	strh	%a, [%a, #0]\n" ireg src ireg addr; 1
+    | Mint32, [IR addr; IR src] ->
+        fprintf oc "	str	%a, [%a, #0]\n" ireg src ireg addr; 1
+    | Mfloat32, [IR addr; FR src] ->
+        fprintf oc "	mvfs	%a, %a\n" freg FR2 freg src;
+        fprintf oc "	stfs	%a, [%a, #0]\n" freg FR2 ireg addr; 2
+    | Mfloat64, [IR addr; FR src] ->
+        fprintf oc "	stfd	%a, [%a, #0]\n" freg src ireg addr; 1
+    | _ ->
+        assert false
+    end in
+  fprintf oc "%s end builtin __builtin_volatile_write\n" comment; n
 
 (* Handling of compiler-inlined builtins *)
 
-let print_builtin_inlined oc name args res =
+let print_builtin_inline oc name args res =
   fprintf oc "%s begin %s\n" comment name;
   let n = match name, args, res with
-  (* Volatile reads *)
-  | "__builtin_volatile_read_int8unsigned", [IR addr], IR res ->
-      fprintf oc "	ldrb	%a, [%a, #0]\n" ireg res ireg addr; 1
-  | "__builtin_volatile_read_int8signed", [IR addr], IR res ->
-      fprintf oc "	ldrsb	%a, [%a, #0]\n" ireg res ireg addr; 1
-  | "__builtin_volatile_read_int16unsigned", [IR addr], IR res ->
-      fprintf oc "	ldrh	%a, [%a, #0]\n" ireg res ireg addr; 1
-  | "__builtin_volatile_read_int16signed", [IR addr], IR res ->
-      fprintf oc "	ldrsh	%a, [%a, #0]\n" ireg res ireg addr; 1
-  | ("__builtin_volatile_read_int32"|"__builtin_volatile_read_pointer"), [IR addr], IR res ->
-      fprintf oc "	ldr	%a, [%a, #0]\n" ireg res ireg addr; 1
-  | "__builtin_volatile_read_float32", [IR addr], FR res ->
-      fprintf oc "	ldfs	%a, [%a, #0]\n" freg res ireg addr;
-      fprintf oc "	mvfd	%a, %a\n" freg res freg res; 2
-  | "__builtin_volatile_read_float64", [IR addr], FR res ->
-      fprintf oc "	ldfd	%a, [%a, #0]\n" freg res ireg addr; 1
-  (* Volatile writes *)
-  | ("__builtin_volatile_write_int8unsigned"|"__builtin_volatile_write_int8signed"), [IR addr; IR src], _ ->
-      fprintf oc "	strb	%a, [%a, #0]\n" ireg src ireg addr; 1
-  | ("__builtin_volatile_write_int16unsigned"|"__builtin_volatile_write_int16signed"), [IR addr; IR src], _ ->
-      fprintf oc "	strh	%a, [%a, #0]\n" ireg src ireg addr; 1
-  | ("__builtin_volatile_write_int32"|"__builtin_volatile_write_pointer"), [IR addr; IR src], _ ->
-      fprintf oc "	str	%a, [%a, #0]\n" ireg src ireg addr; 1
-  | "__builtin_volatile_write_float32", [IR addr; FR src], _ ->
-      fprintf oc "	mvfs	%a, %a\n" freg FR2 freg src;
-      fprintf oc "	stfs	%a, [%a, #0]\n" freg FR2 ireg addr; 2
-  | "__builtin_volatile_write_float64", [IR addr; FR src], _ ->
-      fprintf oc "	stfd	%a, [%a, #0]\n" freg src ireg addr; 1
   (* Float arithmetic *)
   | "__builtin_fabs", [FR a1], FR res ->
       fprintf oc "	absd	%a, %a\n" freg res freg a1; 1
-  (* 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
-      let al = try int_of_string (Str.matched_group 2 name) with Not_found -> 1 in
-      print_builtin_memcpy oc sz al dst src
   (* Catch-all *)
   | _ ->
       invalid_arg ("unrecognized builtin " ^ name)
@@ -528,10 +553,28 @@ let print_instruction oc = function
         tbl;
       2 + List.length tbl
   | 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; 0
+      | _ ->
+          assert false
+      end
 
 let no_fallthrough = function
   | Pb _ -> true
@@ -617,7 +660,7 @@ let print_fundef oc (Coq_pair(name, defn)) =
       print_function oc name code
   | External ef ->
       if need_stub ef && not(is_builtin_function name)
-      then print_external_function oc name ef.ef_sig
+      then print_external_function oc name (ef_sig ef)
 
 (* Data *)