Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong.

Use EF_debug instead of EF_annot for line number annotations.

Introduce PrintAsmaux.print_debug_info (very incomplete).

powerpc/Asmexpand: revise expand_memcpy_small.

15 files changed, 55 insertions, 50 deletions

diff --git a/backend/Allocation.v b/backend/Allocation.v
index 5499c1c5..196a4075 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -697,7 +697,7 @@ Fixpoint add_equations_builtin_arg
   match arg, arg' with
   | BA r, BA l =>
       Some (add_equation (Eq Full r l) e)
-  | BA r, BA_longofwords (BA lhi) (BA llo) =>
+  | BA r, BA_splitlong (BA lhi) (BA llo) =>
       assertion (typ_eq (env r) Tlong);
       Some (add_equation (Eq Low r llo) (add_equation (Eq High r lhi) e))
   | BA_int n, BA_int n' =>
@@ -724,7 +724,7 @@ Fixpoint add_equations_builtin_arg
       assertion (ident_eq id id');
       assertion (Int.eq_dec ofs ofs');
       Some e
-  | BA_longofwords hi lo, BA_longofwords hi' lo' =>
+  | BA_splitlong hi lo, BA_splitlong hi' lo' =>
       do e1 <- add_equations_builtin_arg env hi hi' e;
       add_equations_builtin_arg env lo lo' e1
   | _, _ =>
@@ -763,7 +763,7 @@ Definition remove_equations_builtin_res
     (env: regenv) (res: builtin_res reg) (res': builtin_res mreg) (e: eqs) : option eqs :=
   match res, res' with
   | BR r, BR r' => Some (remove_equation (Eq Full r (R r')) e)
-  | BR r, BR_longofwords (BR rhi) (BR rlo) =>
+  | BR r, BR_splitlong (BR rhi) (BR rlo) =>
       assertion (typ_eq (env r) Tlong);
       if mreg_eq rhi rlo then None else
         Some (remove_equation (Eq Low r (R rlo))
diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index ad1cbd14..6a43eccd 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -270,9 +270,9 @@ Inductive eval_builtin_arg: builtin_arg expr -> val -> Prop :=
       eval_builtin_arg (BA_loadglobal chunk id ofs) v
   | eval_BA_addrglobal: forall id ofs,
       eval_builtin_arg (BA_addrglobal id ofs) (Genv.symbol_address ge id ofs)
-  | eval_BA_longofwords: forall a1 a2 v1 v2,
+  | eval_BA_splitlong: forall a1 a2 v1 v2,
       eval_expr nil a1 v1 -> eval_expr nil a2 v2 ->
-      eval_builtin_arg (BA_longofwords (BA a1) (BA a2)) (Val.longofwords v1 v2).
+      eval_builtin_arg (BA_splitlong (BA a1) (BA a2)) (Val.longofwords v1 v2).
 
 End EVAL_EXPR.
 
diff --git a/backend/Constprop.v b/backend/Constprop.v
index 3a238b95..cd844d30 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -113,10 +113,10 @@ Fixpoint builtin_arg_reduction (ae: AE.t) (a: builtin_arg reg) :=
       | FS n => if Compopts.generate_float_constants tt then BA_single n else a
       | _ => a
       end
-  | BA_longofwords hi lo =>
+  | BA_splitlong hi lo =>
       match builtin_arg_reduction ae hi, builtin_arg_reduction ae lo with
       | BA_int nhi, BA_int nlo => BA_long (Int64.ofwords nhi nlo)
-      | hi', lo' => BA_longofwords hi' lo'
+      | hi', lo' => BA_splitlong hi' lo'
       end
   | _ => a
   end.
diff --git a/backend/Deadcode.v b/backend/Deadcode.v
index 32bc26fb..9bf17d1d 100644
--- a/backend/Deadcode.v
+++ b/backend/Deadcode.v
@@ -78,7 +78,7 @@ Fixpoint transfer_builtin_arg (nv: nval) (na: NA.t) (a: builtin_arg reg) : NA.t
   | BA_addrstack _ | BA_addrglobal _ _ => (ne, nm)
   | BA_loadstack chunk ofs => (ne, nmem_add nm (Stk ofs) (size_chunk chunk))
   | BA_loadglobal chunk id ofs => (ne, nmem_add nm (Gl id ofs) (size_chunk chunk))
-  | BA_longofwords hi lo =>
+  | BA_splitlong hi lo =>
       transfer_builtin_arg All (transfer_builtin_arg All na hi) lo
   end.
 
diff --git a/backend/Inlining.v b/backend/Inlining.v
index 98436bf5..08f2bfc4 100644
--- a/backend/Inlining.v
+++ b/backend/Inlining.v
@@ -208,7 +208,7 @@ Fixpoint sbuiltinarg (ctx: context) (a: builtin_arg reg) : builtin_arg reg :=
   | BA x => BA (sreg ctx x)
   | BA_loadstack chunk ofs => BA_loadstack chunk (Int.add ofs (Int.repr ctx.(dstk)))
   | BA_addrstack ofs => BA_addrstack (Int.add ofs (Int.repr ctx.(dstk)))
-  | BA_longofwords hi lo => BA_longofwords (sbuiltinarg ctx hi) (sbuiltinarg ctx lo)
+  | BA_splitlong hi lo => BA_splitlong (sbuiltinarg ctx hi) (sbuiltinarg ctx lo)
   | _ => a
   end.
 
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 2c8de98e..62a0c585 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -59,7 +59,7 @@ Fixpoint wt_builtin_res (ty: typ) (res: builtin_res mreg) : bool :=
   match res with
   | BR r => subtype ty (mreg_type r)
   | BR_none => true
-  | BR_longofwords hi lo => wt_builtin_res Tint hi && wt_builtin_res Tint lo
+  | BR_splitlong hi lo => wt_builtin_res Tint hi && wt_builtin_res Tint lo
   end.
 
 Definition wt_instr (i: instruction) : bool :=
diff --git a/backend/Locations.v b/backend/Locations.v
index 4ec24a14..439cd2dc 100644
--- a/backend/Locations.v
+++ b/backend/Locations.v
@@ -381,7 +381,7 @@ Module Locmap.
     match res with
     | BR r => set (R r) v m
     | BR_none => m
-    | BR_longofwords hi lo => 
+    | BR_splitlong hi lo => 
         setres lo (Val.loword v) (setres hi (Val.hiword v) m)
     end.
 
diff --git a/backend/Mach.v b/backend/Mach.v
index 08fe7c0a..8853d9da 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -166,7 +166,7 @@ Fixpoint set_res (res: builtin_res mreg) (v: val) (rs: regset) : regset :=
   match res with
   | BR r => Regmap.set r v rs
   | BR_none => rs
-  | BR_longofwords hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs)
+  | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs)
   end.
 
 Definition is_label (lbl: label) (instr: instruction) : bool :=
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index b842f86d..883b5477 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -135,9 +135,6 @@ let cfi_rel_offset =
   else
     (fun _ _ _ -> ())
 
-(* For handling of annotations *)
-let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$"
-
 (* Basic printing functions *)
 let coqint oc n =
   fprintf oc "%ld" (camlint_of_coqint n)
@@ -213,8 +210,7 @@ let print_file_line_d2 oc pref file line =
     | Some fb -> Printlines.copy oc pref fb line line
   end
 
-					    
-(** "True" annotations *)
+(** Programmer-supplied annotations (__builtin_annot). *)
 
 let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*"
 
@@ -242,7 +238,7 @@ let rec print_annot print_preg sp_reg_name oc = function
       fprintf oc "(\"%s\" + %ld)"
          (extern_atom id)
          (camlint_of_coqint ofs)
-  | BA_longofwords(hi, lo) ->
+  | BA_splitlong(hi, lo) ->
       fprintf oc "(%a * 0x100000000 + %a)"
         (print_annot print_preg sp_reg_name) hi
         (print_annot print_preg sp_reg_name) lo
@@ -262,18 +258,27 @@ let print_annot_text print_preg sp_reg_name oc txt args =
   List.iter print_fragment (Str.full_split re_annot_param txt);
   fprintf oc "\n"
 
-let print_annot_stmt print_preg sp_reg_name oc txt tys args =
-  print_annot_text print_preg sp_reg_name oc txt args
+(* Printing of [EF_debug] info.  To be completed. *)
 
-let print_annot_val print_preg oc txt args =
-  print_annot_text print_preg "<internal error>" oc txt
-    (List.map (fun r -> BA r) args)
+let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$"
 
+let print_debug_info comment print_line print_preg sp_name oc kind txt args =
+  if kind = 1 && Str.string_match re_file_line txt 0 then begin
+    print_line oc (Str.matched_group 1 txt)
+                  (int_of_string (Str.matched_group 2 txt))
+  end else begin
+    fprintf oc "%s debug%d: %s" comment kind txt;
+    List.iter
+      (fun a -> fprintf oc " %a" (print_annot print_preg sp_name) a)
+      args;
+    fprintf oc "\n"
+  end
+					    
 (** Inline assembly *)
 
 let print_asm_argument print_preg oc modifier = function
   | BA r -> print_preg oc r
-  | BA_longofwords(BA hi, BA lo) ->
+  | BA_splitlong(BA hi, BA lo) ->
       begin match modifier with
       | "R" -> print_preg oc hi
       | "Q" -> print_preg oc lo
@@ -284,7 +289,7 @@ let print_asm_argument print_preg oc modifier = function
 
 let builtin_arg_of_res = function
   | BR r -> BA r
-  | BR_longofwords(BR hi, BR lo) -> BA_longofwords(BA hi, BA lo)
+  | BR_splitlong(BR hi, BR lo) -> BA_splitlong(BA hi, BA lo)
   | _ -> assert false
 
 let re_asm_param_1 = Str.regexp "%%\\|%[QR]?[0-9]+"
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index 45ad8e19..d818de58 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -401,10 +401,10 @@ Fixpoint convert_builtin_arg {A: Type} (a: builtin_arg expr) (rl: list A) : buil
   | BA_addrstack ofs => (BA_addrstack ofs, rl)
   | BA_loadglobal chunk id ofs => (BA_loadglobal chunk id ofs, rl)
   | BA_addrglobal id ofs => (BA_addrglobal id ofs, rl)
-  | BA_longofwords hi lo =>
+  | BA_splitlong hi lo =>
       let (hi', rl1) := convert_builtin_arg hi rl in
       let (lo', rl2) := convert_builtin_arg lo rl1 in
-      (BA_longofwords hi' lo', rl2)
+      (BA_splitlong hi' lo', rl2)
   end.
 
 Fixpoint convert_builtin_args {A: Type} (al: list (builtin_arg expr)) (rl: list A) : list (builtin_arg A) :=
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 8635ed53..8b30b44f 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -76,7 +76,7 @@ Definition type_of_builtin_arg (a: builtin_arg reg) : typ :=
   | BA_addrstack ofs => Tint
   | BA_loadglobal chunk id ofs => type_of_chunk chunk
   | BA_addrglobal id ofs => Tint
-  | BA_longofwords hi lo => Tlong
+  | BA_splitlong hi lo => Tlong
   end.
 
 Definition type_of_builtin_res (r: builtin_res reg) : typ :=
@@ -245,7 +245,7 @@ Definition type_builtin_arg (e: S.typenv) (a: builtin_arg reg) (ty: typ) : res S
   | BA_addrstack ofs => type_expect e ty Tint
   | BA_loadglobal chunk id ofs => type_expect e ty (type_of_chunk chunk)
   | BA_addrglobal id ofs => type_expect e ty Tint
-  | BA_longofwords hi lo => type_expect e ty Tlong
+  | BA_splitlong hi lo => type_expect e ty Tlong
   end.
 
 Fixpoint type_builtin_args (e: S.typenv) (al: list (builtin_arg reg)) (tyl: list typ) : res S.typenv :=
diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml
index b901076e..76288fb5 100644
--- a/backend/Regalloc.ml
+++ b/backend/Regalloc.ml
@@ -117,7 +117,7 @@ let xparmove srcs dsts k =
 let rec convert_builtin_arg tyenv = function
   | BA r ->
       begin match tyenv r with
-      | Tlong -> BA_longofwords(BA(V(r, Tint)), BA(V(twin_reg r, Tint)))
+      | Tlong -> BA_splitlong(BA(V(r, Tint)), BA(V(twin_reg r, Tint)))
       | ty    -> BA(V(r, ty))
       end
   | BA_int n -> BA_int n
@@ -128,26 +128,26 @@ let rec convert_builtin_arg tyenv = function
   | BA_addrstack(ofs) -> BA_addrstack(ofs)
   | BA_loadglobal(chunk, id, ofs) -> BA_loadglobal(chunk, id, ofs)
   | BA_addrglobal(id, ofs) -> BA_addrglobal(id, ofs)
-  | BA_longofwords(hi, lo) ->
-      BA_longofwords(convert_builtin_arg tyenv hi, convert_builtin_arg tyenv lo)
+  | BA_splitlong(hi, lo) ->
+      BA_splitlong(convert_builtin_arg tyenv hi, convert_builtin_arg tyenv lo)
 
 let convert_builtin_res tyenv = function
   | BR r ->
       begin match tyenv r with
-      | Tlong -> BR_longofwords(BR(V(r, Tint)), BR(V(twin_reg r, Tint)))
+      | Tlong -> BR_splitlong(BR(V(r, Tint)), BR(V(twin_reg r, Tint)))
       | ty    -> BR(V(r, ty))
       end
   | BR_none -> BR_none
-  | BR_longofwords _ -> assert false
+  | BR_splitlong _ -> assert false
 
 let rec constrain_builtin_arg a cl =
   match a, cl with
   | BA x, None :: cl' -> (a, cl')
   | BA x, Some mr :: cl' -> (BA (L(R mr)), cl')
-  | BA_longofwords(hi, lo), _ ->
+  | BA_splitlong(hi, lo), _ ->
       let (hi', cl1) = constrain_builtin_arg hi cl in
       let (lo', cl2) = constrain_builtin_arg lo cl1 in
-      (BA_longofwords(hi', lo'), cl2)
+      (BA_splitlong(hi', lo'), cl2)
   | _, _ -> (a, cl)
 
 let rec constrain_builtin_args al cl =
@@ -162,10 +162,10 @@ let rec constrain_builtin_res a cl =
   match a, cl with
   | BR x, None :: cl' -> (a, cl')
   | BR x, Some mr :: cl' -> (BR (L(R mr)), cl')
-  | BR_longofwords(hi, lo), _ ->
+  | BR_splitlong(hi, lo), _ ->
       let (hi', cl1) = constrain_builtin_res hi cl in
       let (lo', cl2) = constrain_builtin_res lo cl1 in
-      (BR_longofwords(hi', lo'), cl2)
+      (BR_splitlong(hi', lo'), cl2)
   | _, _ -> (a, cl)
 
 (* Return the XTL basic block corresponding to the given RTL instruction.
@@ -294,7 +294,7 @@ let vset_addros vos after =
 let rec vset_addarg a after =
   match a with
   | BA v -> VSet.add v after
-  | BA_longofwords(hi, lo) -> vset_addarg hi (vset_addarg lo after)
+  | BA_splitlong(hi, lo) -> vset_addarg hi (vset_addarg lo after)
   | _ -> after
 
 let vset_addargs al after = List.fold_right vset_addarg al after
@@ -303,7 +303,7 @@ let rec vset_removeres r after =
   match r with
   | BR v -> VSet.remove v after
   | BR_none -> after
-  | BR_longofwords(hi, lo) -> vset_removeres hi (vset_removeres lo after)
+  | BR_splitlong(hi, lo) -> vset_removeres hi (vset_removeres lo after)
 
 let live_before instr after =
   match instr with
@@ -392,7 +392,7 @@ let rec dce_parmove srcs dsts after =
 
 let rec keep_builtin_arg after = function
   | BA v -> VSet.mem v after
-  | BA_longofwords(hi, lo) ->
+  | BA_splitlong(hi, lo) ->
       keep_builtin_arg after hi && keep_builtin_arg after lo
   | _ -> true
 
@@ -800,10 +800,10 @@ let rec reload_arg tospill eqs = function
   | BA v ->
       let (t, c1, eqs1) = reload_var tospill eqs v in
       (BA t, c1, eqs1)
-  | BA_longofwords(hi, lo) ->
+  | BA_splitlong(hi, lo) ->
       let (hi', c1, eqs1) = reload_arg tospill eqs hi in
       let (lo', c2, eqs2) = reload_arg tospill eqs1 lo in
-      (BA_longofwords(hi', lo'), c1 @ c2, eqs2)
+      (BA_splitlong(hi', lo'), c1 @ c2, eqs2)
   | a -> (a, [], eqs)
 
 let rec reload_args tospill eqs = function
@@ -827,10 +827,10 @@ let rec save_res tospill eqs = function
       (BR t, c1, eqs1)
   | BR_none ->
       (BR_none, [], eqs)
-  | BR_longofwords(hi, lo) ->
+  | BR_splitlong(hi, lo) ->
       let (hi', c1, eqs1) = save_res tospill eqs hi in
       let (lo', c2, eqs2) = save_res tospill eqs1 lo in
-      (BR_longofwords(hi', lo'), c1 @ c2, eqs2)
+      (BR_splitlong(hi', lo'), c1 @ c2, eqs2)
 
 (* Trimming equations when we have too many or when they are too old.
    The goal is to limit the live range of unspillable temporaries.
diff --git a/backend/Stacking.v b/backend/Stacking.v
index caf0ae59..ef96e4b3 100644
--- a/backend/Stacking.v
+++ b/backend/Stacking.v
@@ -146,8 +146,8 @@ Fixpoint transl_builtin_arg (fe: frame_env) (a: builtin_arg loc) : builtin_arg m
       BA_addrstack (Int.add ofs (Int.repr fe.(fe_stack_data)))
   | BA_loadglobal chunk id ofs => BA_loadglobal chunk id ofs
   | BA_addrglobal id ofs => BA_addrglobal id ofs
-  | BA_longofwords hi lo => 
-      BA_longofwords (transl_builtin_arg fe hi) (transl_builtin_arg fe lo)
+  | BA_splitlong hi lo => 
+      BA_splitlong (transl_builtin_arg fe hi) (transl_builtin_arg fe lo)
   end.
 
 (** Translation of a Linear instruction.  Prepends the corresponding
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index 3b0e7133..22121075 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -71,7 +71,7 @@ Fixpoint abuiltin_arg (ae: aenv) (am: amem) (rm: romem) (ba: builtin_arg reg) :
   | BA_addrstack ofs => Ptr (Stk ofs)
   | BA_loadglobal chunk id ofs => loadv chunk rm am (Ptr (Gl id ofs))
   | BA_addrglobal id ofs => Ptr (Gl id ofs)
-  | BA_longofwords hi lo => longofwords (abuiltin_arg ae am rm hi) (abuiltin_arg ae am rm lo)
+  | BA_splitlong hi lo => longofwords (abuiltin_arg ae am rm hi) (abuiltin_arg ae am rm lo)
   end.
 
 Definition set_builtin_res (br: builtin_res reg) (av: aval) (ae: aenv) : aenv :=
diff --git a/backend/XTL.ml b/backend/XTL.ml
index e05b90d1..dde9bdb0 100644
--- a/backend/XTL.ml
+++ b/backend/XTL.ml
@@ -127,7 +127,7 @@ let unify_var_type v1 v2 =
 let rec type_builtin_arg a ty =
   match a with
   | BA v -> set_var_type v ty
-  | BA_longofwords(a1, a2) -> type_builtin_arg a1 Tint; type_builtin_arg a2 Tint
+  | BA_splitlong(a1, a2) -> type_builtin_arg a1 Tint; type_builtin_arg a2 Tint
   | _ -> ()
 
 let rec type_builtin_args al tyl =
@@ -139,7 +139,7 @@ let rec type_builtin_args al tyl =
 let rec type_builtin_res a ty =
   match a with
   | BR v -> set_var_type v ty
-  | BR_longofwords(a1, a2) -> type_builtin_res a1 Tint; type_builtin_res a2 Tint
+  | BR_splitlong(a1, a2) -> type_builtin_res a1 Tint; type_builtin_res a2 Tint
   | _ -> ()
 
 let type_instr = function