From a6b6bf31121d975c915c01f501618d97df7879fb Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 9 May 2015 09:00:51 +0200 Subject: Extended inline asm: revised treatment of clobbered registers. - Treat clobbered registers as being destroyed by EF_inline_asm builtins (which is the truth, semantically). - To enable the above, represent clobbers as Coq strings rather than idents and move register_by_name from Machregsaux.ml to Machregs.v. - Side benefit: more efficient implementation of Machregsaux.name_of_register. -# Please enter the commit message for your changes. Lines starting --- powerpc/Machregs.v | 42 ++++++++++++++++++++++++++++++++++++++++++ powerpc/Machregsaux.ml | 43 +++++++++---------------------------------- powerpc/Machregsaux.mli | 1 - 3 files changed, 51 insertions(+), 35 deletions(-) (limited to 'powerpc') 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 -- cgit From ced4ff38f1309f05c9b750bde241bf87b83745fa Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 9 May 2015 09:43:54 +0200 Subject: Updated PrintOp for the single-precision FP operations. --- powerpc/PrintOp.ml | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'powerpc') 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 -- cgit From 5634dce892b238afba7deed1d220e1faf71f99ea Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 14 May 2015 11:41:14 +0200 Subject: Merged PrintAnnot into PrintAsmaux. --- powerpc/TargetPrinter.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'powerpc') 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 -- cgit