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 --- arm/Machregs.v | 34 ++++++++++++++++++++++++++++++++++ arm/Machregsaux.ml | 35 +++++++++-------------------------- arm/Machregsaux.mli | 1 - 3 files changed, 43 insertions(+), 27 deletions(-) (limited to 'arm') diff --git a/arm/Machregs.v b/arm/Machregs.v index f373b434..f46f2904 100644 --- a/arm/Machregs.v +++ b/arm/Machregs.v @@ -10,6 +10,7 @@ (* *) (* *********************************************************************) +Require Import String. Require Import Coqlib. Require Import Maps. Require Import AST. @@ -75,6 +76,28 @@ End IndexedMreg. Definition is_stack_reg (r: mreg) : bool := false. +(** ** Names of registers *) + +Local Open Scope string_scope. + +Definition register_names := + ("R0", R0) :: ("R1", R1) :: ("R2", R2) :: ("R3", R3) :: + ("R4", R4) :: ("R5", R5) :: ("R6", R6) :: ("R7", R7) :: + ("R8", R8) :: ("R9", R9) :: ("R10", R10) :: ("R11", R11) :: + ("R12", R12) :: + ("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) :: 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 := @@ -95,9 +118,20 @@ Definition destroyed_by_cond (cond: condition): list mreg := Definition destroyed_by_jumptable: list mreg := 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_memcpy sz al => if zle sz 32 then F7 :: nil else R2 :: R3 :: R12 :: nil + | EF_inline_asm txt sg clob => destroyed_by_clobber clob | _ => nil end. diff --git a/arm/Machregsaux.ml b/arm/Machregsaux.ml index 44e6b192..d59ec8b8 100644 --- a/arm/Machregsaux.ml +++ b/arm/Machregsaux.ml @@ -12,41 +12,24 @@ (** Auxiliary functions on machine registers *) +open Camlcoq open Machregs -let register_names = [ - ("R0", R0); ("R1", R1); ("R2", R2); ("R3", R3); - ("R4", R4); ("R5", R5); ("R6", R6); ("R7", R7); - ("R8", R8); ("R9", R9); ("R10", R10); ("R11", R11); - ("R12", R12); - ("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) -] +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 = [ "R14" ] 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/arm/Machregsaux.mli b/arm/Machregsaux.mli index f0feec96..d4877a62 100644 --- a/arm/Machregsaux.mli +++ b/arm/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. --- arm/PrintOp.ml | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) (limited to 'arm') diff --git a/arm/PrintOp.ml b/arm/PrintOp.ml index 96d13943..886f6de3 100644 --- a/arm/PrintOp.ml +++ b/arm/PrintOp.ml @@ -52,6 +52,14 @@ let print_condition reg pp = function fprintf pp "%a %sf 0.0" reg r1 (comparison_name c) | (Cnotcompfzero c, [r1]) -> fprintf pp "%a not(%sf) 0.0" reg r1 (comparison_name c) + | (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 + | (Ccompfszero c, [r1]) -> + fprintf pp "%a %sfs 0.0" reg r1 (comparison_name c) + | (Cnotcompfszero c, [r1]) -> + fprintf pp "%a not(%sfs) 0.0" reg r1 (comparison_name c) | _ -> fprintf pp "" @@ -59,6 +67,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, [] -> @@ -100,9 +109,21 @@ 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 | Ointoffloat, [r1] -> fprintf pp "intoffloat(%a)" reg r1 + | Ointuoffloat, [r1] -> fprintf pp "intuoffloat(%a)" reg r1 | Ofloatofint, [r1] -> fprintf pp "floatofint(%a)" reg r1 + | Ofloatofintu, [r1] -> fprintf pp "floatofintu(%a)" reg r1 + | Ointofsingle, [r1] -> fprintf pp "intofsingle(%a)" reg r1 + | Ointuofsingle, [r1] -> fprintf pp "intuofsingle(%a)" reg r1 + | Osingleofint, [r1] -> fprintf pp "singleofint(%a)" reg r1 + | Osingleofintu, [r1] -> fprintf pp "singleofintu(%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 -- 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. --- arm/TargetPrinter.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'arm') diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index c77572db..505c3265 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -300,7 +300,7 @@ module Target (Opt: PRINTER_OPTIONS) : 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) @@ -320,12 +320,12 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = (int_of_string (Str.matched_group 2 txt)) end else begin fprintf oc "%s annotation: " comment; - PrintAnnot.print_annot_stmt preg "sp" oc txt targs args + print_annot_stmt preg "sp" 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 0 else (fprintf oc " mov %a, %a\n" ireg dst ireg src; 1) @@ -1005,7 +1005,7 @@ module Target (Opt: PRINTER_OPTIONS) : 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; 5 (* hoping this is an upper bound... *) | _ -> -- cgit