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.

4 files changed, 18 insertions, 25 deletions

diff --git a/ia32/Asm.v b/ia32/Asm.v
index 96a49005..979041ba 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -293,7 +293,7 @@ Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
   match res with
   | BR r => rs#r <- v
   | 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.
 
 Section RELSEM.
diff --git a/ia32/Asmexpand.ml b/ia32/Asmexpand.ml
index 8996794b..a2a7a9be 100644
--- a/ia32/Asmexpand.ml
+++ b/ia32/Asmexpand.ml
@@ -140,7 +140,7 @@ let expand_builtin_vload_common chunk addr res =
      emit (Pmovsw_rm (res,addr))
   | Mint32, BR(IR res) ->
      emit (Pmov_rm (res,addr))
-  | Mint64, BR_longofwords(BR(IR res1), BR(IR res2)) ->
+  | Mint64, BR_splitlong(BR(IR res1), BR(IR res2)) ->
      let addr' = offset_addressing addr _4 in
      if not (Asmgen.addressing_mentions addr res2) then begin
 	 emit (Pmov_rm (res2,addr));
@@ -176,7 +176,7 @@ let expand_builtin_vstore_common chunk addr src tmp =
      emit (Pmovw_mr (addr,src))
   | Mint32, BA(IR src) ->
      emit (Pmov_mr (addr,src))
-  | Mint64, BA_longofwords(BA(IR src1), BA(IR src2)) ->
+  | Mint64, BA_splitlong(BA(IR src1), BA(IR src2)) ->
      let addr' = offset_addressing addr _4 in
      emit (Pmov_mr (addr,src2));
      emit (Pmov_mr (addr',src1))
@@ -293,26 +293,26 @@ let expand_builtin_inline name args res =
         (fun r1 r2 r3 -> Pfnmsub213(r1, r2, r3))
         (fun r1 r2 r3 -> Pfnmsub231(r1, r2, r3))
   (* 64-bit integer arithmetic *)
-  | "__builtin_negl", [BA_longofwords(BA(IR ah), BA(IR al))],
-                      BR_longofwords(BR(IR rh), BR(IR rl)) ->
+  | "__builtin_negl", [BA_splitlong(BA(IR ah), BA(IR al))],
+                      BR_splitlong(BR(IR rh), BR(IR rl)) ->
      assert (ah = EDX && al = EAX && rh = EDX && rl = EAX);
      emit (Pneg EAX);
      emit (Padc_ri (EDX,_0));
      emit (Pneg EDX)
-  | "__builtin_addl", [BA_longofwords(BA(IR ah), BA(IR al));
-                       BA_longofwords(BA(IR bh), BA(IR bl))],
-                       BR_longofwords(BR(IR rh), BR(IR rl)) ->
+  | "__builtin_addl", [BA_splitlong(BA(IR ah), BA(IR al));
+                       BA_splitlong(BA(IR bh), BA(IR bl))],
+                       BR_splitlong(BR(IR rh), BR(IR rl)) ->
      assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX);
      emit (Padd_rr (EAX,EBX));
      emit (Padc_rr (EDX,ECX))
-  | "__builtin_subl", [BA_longofwords(BA(IR ah), BA(IR al));
-                       BA_longofwords(BA(IR bh), BA(IR bl))],
-                       BR_longofwords(BR(IR rh), BR(IR rl)) ->
+  | "__builtin_subl", [BA_splitlong(BA(IR ah), BA(IR al));
+                       BA_splitlong(BA(IR bh), BA(IR bl))],
+                       BR_splitlong(BR(IR rh), BR(IR rl)) ->
      assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX);
      emit (Psub_rr (EAX,EBX));
      emit (Psbb_rr (EDX,ECX))
   | "__builtin_mull", [BA(IR a); BA(IR b)],
-                      BR_longofwords(BR(IR rh), BR(IR rl)) ->
+                      BR_splitlong(BR(IR rh), BR(IR rl)) ->
      assert (a = EAX && b = EDX && rh = EDX && rl = EAX);
      emit (Pmul_r EDX)
   (* Memory accesses *)
diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp
index 744902ec..bc331b9c 100644
--- a/ia32/SelectOp.vp
+++ b/ia32/SelectOp.vp
@@ -516,7 +516,7 @@ Nondetfunction builtin_arg (e: expr) :=
   | Eop (Olea (Ainstack ofs)) Enil => BA_addrstack ofs
   | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) =>
         BA_long (Int64.ofwords h l)
-  | Eop Omakelong (h ::: l ::: Enil) => BA_longofwords (BA h) (BA l)
+  | Eop Omakelong (h ::: l ::: Enil) => BA_splitlong (BA h) (BA l)
   | Eload chunk (Aglobal id ofs) Enil => BA_loadglobal chunk id ofs
   | Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs
   | _ => BA e
diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml
index beddd1e8..9e4babb7 100644
--- a/ia32/TargetPrinter.ml
+++ b/ia32/TargetPrinter.ml
@@ -337,17 +337,6 @@ module Target(System: SYSTEM):TARGET =
    - inlined by the compiler: take their arguments in arbitrary
    registers; preserve all registers except ECX, EDX, XMM6 and XMM7. *)
 
-(* Handling of annotations *)
-
-    let print_annot_stmt oc txt targs args =
-      if Str.string_match re_file_line txt 0 then begin
-        print_file_line oc (Str.matched_group 1 txt)
-          (int_of_string (Str.matched_group 2 txt))
-      end else begin
-        fprintf oc "%s annotation: " comment;
-        print_annot_stmt preg "%esp" oc txt targs args
-      end
-
  (* Handling of varargs *)
 
     let print_builtin_va_start oc r =
@@ -658,7 +647,11 @@ module Target(System: SYSTEM):TARGET =
       | Pbuiltin(ef, args, res) ->
           begin match ef with
           | EF_annot(txt, targs) ->
-              print_annot_stmt oc (extern_atom txt) targs args
+              fprintf oc "%s annotation: " comment;
+              print_annot_text preg_annot "%esp" oc (extern_atom txt) args
+          | EF_debug(kind, txt, targs) ->
+              print_debug_info comment print_file_line preg "%esp" oc
+                               (P.to_int kind) (extern_atom txt) args
           | EF_inline_asm(txt, sg, clob) ->
               fprintf oc "%s begin inline assembly\n\t" comment;
               print_inline_asm preg oc (extern_atom txt) sg args res;