Merge branch 'master' into json_export

5 files changed, 54 insertions, 28 deletions

diff --git a/ia32/Machregs.v b/ia32/Machregs.v
index a9f2b6c4..65e27599 100644
--- a/ia32/Machregs.v
+++ b/ia32/Machregs.v
@@ -69,6 +69,25 @@ End IndexedMreg.
 Definition is_stack_reg (r: mreg) : bool :=
   match r with FP0 => true | _ => false end.
 
+(** ** Names of registers *)
+
+Local Open Scope string_scope.
+
+Definition register_names :=
+  ("EAX", AX) :: ("EBX", BX) :: ("ECX", CX) :: ("EDX", DX) ::
+  ("ESI", SI) :: ("EDI", DI) :: ("EBP", BP) ::
+  ("XMM0", X0) :: ("XMM1", X1) :: ("XMM2", X2) :: ("XMM3", X3) ::
+  ("XMM4", X4) :: ("XMM5", X5) :: ("XMM6", X6) :: ("XMM7", X7) ::
+  ("ST0", FP0) :: 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 :=
@@ -100,7 +119,15 @@ Definition destroyed_by_cond (cond: condition): list mreg :=
 Definition destroyed_by_jumptable: list mreg :=
   nil.
 
-Local Open Scope string_scope.
+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 builtin_write16_reversed := ident_of_string "__builtin_write16_reversed".
 Definition builtin_write32_reversed := ident_of_string "__builtin_write32_reversed".
@@ -115,6 +142,7 @@ Definition destroyed_by_builtin (ef: external_function): list mreg :=
       if ident_eq id builtin_write16_reversed
       || ident_eq id builtin_write32_reversed
       then CX :: DX :: nil else nil
+  | EF_inline_asm txt sg clob => destroyed_by_clobber clob
   | _ => nil
   end.
 
diff --git a/ia32/Machregsaux.ml b/ia32/Machregsaux.ml
index 5e98b58b..6485e752 100644
--- a/ia32/Machregsaux.ml
+++ b/ia32/Machregsaux.ml
@@ -12,38 +12,25 @@
 
 (** Auxiliary functions on machine registers *)
 
+open Camlcoq
 open Machregs
 
-let register_names = [
-  ("EAX", AX); ("EBX", BX); ("ECX", CX); ("EDX", DX);
-  ("ESI", SI); ("EDI", DI); ("EBP", BP);
-  ("XMM0", X0); ("XMM1", X1); ("XMM2", X2); ("XMM3", X3);
-  ("XMM4", X4); ("XMM5", X5); ("XMM6", X6); ("XMM7", X7);
-  ("ST0", FP0)
-]
+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 = []
 
 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/ia32/Machregsaux.mli b/ia32/Machregsaux.mli
index f0feec96..d4877a62 100644
--- a/ia32/Machregsaux.mli
+++ b/ia32/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/ia32/PrintOp.ml b/ia32/PrintOp.ml
index fb9a7cc5..1f7f4a65 100644
--- a/ia32/PrintOp.ml
+++ b/ia32/PrintOp.ml
@@ -38,6 +38,10 @@ let print_condition reg pp = function
       fprintf pp "%a %sf %a" reg r1 (comparison_name c) reg r2
   | (Cnotcompf c, [r1;r2]) ->
       fprintf pp "%a not(%sf) %a" reg r1 (comparison_name c) reg r2
+  | (Ccompfs c, [r1;r2]) ->
+      fprintf pp "%a %sfs %a" reg r1 (comparison_name c) reg r2
+  | (Cnotcompfs c, [r1;r2]) ->
+      fprintf pp "%a not(%sfs) %a" reg r1 (comparison_name c) reg r2
   | (Cmaskzero n, [r1]) ->
       fprintf pp "%a & 0x%lx == 0" reg r1 (camlint_of_coqint n)
   | (Cmasknotzero n, [r1]) ->
@@ -100,10 +104,18 @@ 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
   | Ofloatofint, [r1] -> fprintf pp "floatofint(%a)" reg r1
+  | Ointofsingle, [r1] -> fprintf pp "intofsingle(%a)" reg r1
+  | Osingleofint, [r1] -> fprintf pp "singleofint(%a)" reg r1
   | Omakelong, [r1;r2] -> fprintf pp "makelong(%a,%a)" reg r1 reg r2
   | Olowlong, [r1] -> fprintf pp "lowlong(%a)" reg r1
   | Ohighlong, [r1] -> fprintf pp "highlong(%a)" reg r1
diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml
index ca07a172..a53a8fbd 100644
--- a/ia32/TargetPrinter.ml
+++ b/ia32/TargetPrinter.ml
@@ -323,7 +323,7 @@ module Target(System: SYSTEM):TARGET =
 (* Emit .file / .loc debugging directives *)
 
     let print_file_line oc file line =
-      PrintAnnot.print_file_line oc comment file line
+      print_file_line oc comment file line
 
     let print_location oc loc =
       if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc)
@@ -345,12 +345,12 @@ 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 "%esp" oc txt targs args
+        print_annot_stmt preg "%esp" oc txt targs args
       end
 
     let print_annot_val oc txt args res =
       fprintf oc "%s annotation: " comment;
-      PrintAnnot.print_annot_val preg oc txt args;
+      print_annot_val 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
@@ -873,7 +873,7 @@ module Target(System: SYSTEM):TARGET =
               print_annot_val oc (extern_atom txt) args res
           | 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