Merge branch 'master' into json_export

5 files changed, 65 insertions, 41 deletions

diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v
index f7ed7793..3b7cbb76 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -10,6 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+Require Import String.
 Require Import Coqlib.
 Require Import Maps.
 Require Import AST.
@@ -97,6 +98,36 @@ End IndexedMreg.
 
 Definition is_stack_reg (r: mreg) : bool := false.
 
+(** ** Names of registers *)
+
+Local Open Scope string_scope.
+
+Definition register_names :=
+  ("R3", R3) ::  ("R4", R4) ::  ("R5", R5) ::  ("R6", R6) ::
+  ("R7", R7) ::  ("R8", R8) ::  ("R9", R9) ::  ("R10", R10) ::
+  ("R11", R11) :: ("R12", R12) ::
+  ("R14", R14) :: ("R15", R15) :: ("R16", R16) ::
+  ("R17", R17) :: ("R18", R18) :: ("R19", R19) :: ("R20", R20) ::
+  ("R21", R21) :: ("R22", R22) :: ("R23", R23) :: ("R24", R24) ::
+  ("R25", R25) :: ("R26", R26) :: ("R27", R27) :: ("R28", R28) ::
+  ("R29", R29) :: ("R30", R30) :: ("R31", R31) ::
+  ("F0", F0) :: ("F1", F1) ::  ("F2", F2) ::  ("F3", F3) ::  ("F4", F4) ::
+  ("F5", F5) ::  ("F6", F6) ::  ("F7", F7) ::  ("F8", F8) ::
+  ("F9", F9) ::  ("F10", F10) :: ("F11", F11) :: ("F12", F12) ::
+  ("F13", F13) :: ("F14", F14) :: ("F15", F15) ::
+  ("F16", F16) :: ("F17", F17) :: ("F18", F18) :: ("F19", F19) ::
+  ("F20", F20) :: ("F21", F21) :: ("F22", F22) :: ("F23", F23) ::
+  ("F24", F24) :: ("F25", F25) :: ("F26", F26) :: ("F27", F27) ::
+  ("F28", F28) :: ("F29", F29) :: ("F30", F30) :: ("F31", F31) :: nil.
+
+Definition register_by_name (s: string) : option mreg :=
+  let fix assoc (l: list (string * mreg)) : option mreg :=
+    match l with
+    | nil => None
+    | (s1, r1) :: l' => if string_dec s s1 then Some r1 else assoc l'
+    end
+  in assoc register_names.
+
 (** ** Destroyed registers, preferred registers *)
 
 Definition destroyed_by_op (op: operation): list mreg :=
@@ -119,6 +150,16 @@ Definition destroyed_by_cond (cond: condition): list mreg :=
 Definition destroyed_by_jumptable: list mreg :=
   R12 :: nil.
 
+Fixpoint destroyed_by_clobber (cl: list string): list mreg :=
+  match cl with
+  | nil => nil
+  | c1 :: cl =>
+      match register_by_name c1 with
+      | Some r => r :: destroyed_by_clobber cl
+      | None   => destroyed_by_clobber cl
+      end
+  end.
+
 Definition destroyed_by_builtin (ef: external_function): list mreg :=
   match ef with
   | EF_builtin _ _ => F13 :: nil
@@ -128,6 +169,7 @@ Definition destroyed_by_builtin (ef: external_function): list mreg :=
   | EF_vstore_global Mint64 _ _ => R10 :: R11 :: R12 :: nil
   | EF_vstore_global _ _ _ => R11 :: R12 :: nil
   | EF_memcpy _ _ => R11 :: R12 :: F13 :: nil
+  | EF_inline_asm txt sg clob => destroyed_by_clobber clob
   | _ => nil
   end.
 
diff --git a/powerpc/Machregsaux.ml b/powerpc/Machregsaux.ml
index ba111089..8c3017ff 100644
--- a/powerpc/Machregsaux.ml
+++ b/powerpc/Machregsaux.ml
@@ -12,49 +12,24 @@
 
 (** Auxiliary functions on machine registers *)
 
+open Camlcoq
 open Machregs
 
-let register_names = [
-  ("R3", R3);  ("R4", R4);  ("R5", R5);  ("R6", R6);
-  ("R7", R7);  ("R8", R8);  ("R9", R9);  ("R10", R10);
-  ("R11", R11); ("R12", R12);
-  ("R14", R14); ("R15", R15); ("R16", R16);
-  ("R17", R17); ("R18", R18); ("R19", R19); ("R20", R20);
-  ("R21", R21); ("R22", R22); ("R23", R23); ("R24", R24);
-  ("R25", R25); ("R26", R26); ("R27", R27); ("R28", R28);
-  ("R29", R29); ("R30", R30); ("R31", R31);
-  ("F0", F0); ("F1", F1);  ("F2", F2);  ("F3", F3);  ("F4", F4);
-  ("F5", F5);  ("F6", F6);  ("F7", F7);  ("F8", F8);
-  ("F9", F9);  ("F10", F10); ("F11", F11); ("F12", F12);
-  ("F13", F13); ("F14", F14); ("F15", F15);
-  ("F16", F16); ("F17", F17); ("F18", F18); ("F19", F19);
-  ("F20", F20); ("F21", F21); ("F22", F22); ("F23", F23);
-  ("F24", F24); ("F25", F25); ("F26", F26); ("F27", F27);
-  ("F28", F28); ("F29", F29); ("F30", F30); ("F31", F31)
-]
+let register_names : (mreg, string) Hashtbl.t = Hashtbl.create 31
+
+let _ =
+  List.iter
+    (fun (s, r) -> Hashtbl.add register_names r (camlstring_of_coqstring s))
+    Machregs.register_names
 
 let scratch_register_names = [ "R0" ]
 
 let name_of_register r =
-  let rec rev_assoc = function
-  | [] -> None
-  | (a, b) :: rem -> if b = r then Some a else rev_assoc rem
-  in rev_assoc register_names
+  try Some (Hashtbl.find register_names r) with Not_found -> None
 
 let register_by_name s =
-  try
-    Some(List.assoc (String.uppercase s) register_names)
-  with Not_found ->
-    None
+  Machregs.register_by_name (coqstring_of_camlstring (String.uppercase s))
 
 let can_reserve_register r =
   List.mem r Conventions1.int_callee_save_regs
   || List.mem r Conventions1.float_callee_save_regs
-
-let mregs_of_clobber idl =
-  List.fold_left
-    (fun l c ->
-      match register_by_name (Camlcoq.extern_atom c) with
-      | Some r -> r :: l
-      | None -> l)
-    [] idl
diff --git a/powerpc/Machregsaux.mli b/powerpc/Machregsaux.mli
index f0feec96..d4877a62 100644
--- a/powerpc/Machregsaux.mli
+++ b/powerpc/Machregsaux.mli
@@ -16,4 +16,3 @@ val name_of_register: Machregs.mreg -> string option
 val register_by_name: string -> Machregs.mreg option
 val scratch_register_names: string list
 val can_reserve_register: Machregs.mreg -> bool
-val mregs_of_clobber: Camlcoq.atom list -> Machregs.mreg list
diff --git a/powerpc/PrintOp.ml b/powerpc/PrintOp.ml
index 664280f9..b0213014 100644
--- a/powerpc/PrintOp.ml
+++ b/powerpc/PrintOp.ml
@@ -49,6 +49,7 @@ let print_operation reg pp = function
   | Omove, [r1] -> reg pp r1
   | Ointconst n, [] -> fprintf pp "%ld" (camlint_of_coqint n)
   | Ofloatconst n, [] -> fprintf pp "%F" (camlfloat_of_coqfloat n)
+  | Osingleconst n, [] -> fprintf pp "%Ff" (camlfloat_of_coqfloat32 n)
   | Oaddrsymbol(id, ofs), [] ->
       fprintf pp "\"%s\" + %ld" (extern_atom id) (camlint_of_coqint ofs)
   | Oaddrstack ofs, [] ->
@@ -95,7 +96,14 @@ let print_operation reg pp = function
   | Osubf, [r1;r2] -> fprintf pp "%a -f %a" reg r1 reg r2
   | Omulf, [r1;r2] -> fprintf pp "%a *f %a" reg r1 reg r2
   | Odivf, [r1;r2] -> fprintf pp "%a /f %a" reg r1 reg r2
+  | Onegfs, [r1] -> fprintf pp "negfs(%a)" reg r1
+  | Oabsfs, [r1] -> fprintf pp "absfs(%a)" reg r1
+  | Oaddfs, [r1;r2] -> fprintf pp "%a +fs %a" reg r1 reg r2
+  | Osubfs, [r1;r2] -> fprintf pp "%a -fs %a" reg r1 reg r2
+  | Omulfs, [r1;r2] -> fprintf pp "%a *fs %a" reg r1 reg r2
+  | Odivfs, [r1;r2] -> fprintf pp "%a /fs %a" reg r1 reg r2
   | Osingleoffloat, [r1] -> fprintf pp "singleoffloat(%a)" reg r1
+  | Ofloatofsingle, [r1] -> fprintf pp "floatofsingle(%a)" reg r1
   | Ointoffloat, [r1] -> fprintf pp "intoffloat(%a)" reg r1
   | Ofloatofwords, [r1;r2] -> fprintf pp "floatofwords(%a,%a)" reg r1 reg r2
   | Omakelong, [r1;r2] -> fprintf pp "makelong(%a,%a)" reg r1 reg r2
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index b05b29c0..3789d62e 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -132,7 +132,7 @@ module Linux_System : SYSTEM =
 
 
     let print_file_line oc file line =
-      PrintAnnot.print_file_line oc comment file line
+      print_file_line oc comment file line
     
     (* Emit .cfi directives *)      
     let cfi_startproc = cfi_startproc
@@ -203,7 +203,7 @@ module Diab_System : SYSTEM =
       | Section_debug_abbrev -> ".debug_abbrev,,n"
 
     let print_file_line oc file line =
-      PrintAnnot.print_file_line_d2 oc comment file line
+      print_file_line_d2 oc comment file line
 
     (* Emit .cfi directives *)
     let cfi_startproc oc = ()
@@ -240,10 +240,10 @@ module Diab_System : SYSTEM =
           end_addr := label_end;
           fprintf oc "%a:\n" label label_end;
           fprintf oc "	.text\n";
-          PrintAnnot.StringSet.iter (fun file ->
+          StringSet.iter (fun file ->
             let label = new_label () in
             Hashtbl.add filenum file label;
-            fprintf oc ".L%d:	.d2filenum \"%s\"\n" label file) !PrintAnnot.all_files;
+            fprintf oc ".L%d:	.d2filenum \"%s\"\n" label file) !all_files;
           fprintf oc "	.d2_line_end\n"
         end
 
@@ -331,7 +331,7 @@ module Target (System : SYSTEM):TARGET =
           (int_of_string (Str.matched_group 2 txt))
       end else begin
         fprintf oc "%s annotation: " comment;
-        PrintAnnot.print_annot_stmt preg_annot "R1" oc txt targs args
+        print_annot_stmt preg_annot "R1" oc txt targs args
       end
 
     (* Determine if the displacement of a conditional branch fits the short form *)
@@ -652,7 +652,7 @@ module Target (System : SYSTEM):TARGET =
           begin match ef with
           | EF_inline_asm(txt, sg, clob) ->
               fprintf oc "%s begin inline assembly\n\t" comment;
-              PrintAnnot.print_inline_asm preg oc (extern_atom txt) sg args res;
+              print_inline_asm preg oc (extern_atom txt) sg args res;
               fprintf oc "%s end inline assembly\n" comment
           | _ ->
               assert false