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 - backend/Bounds.v | 7 +------ backend/Regalloc.ml | 6 ++---- cfrontend/C2C.ml | 2 +- cfrontend/PrintCsyntax.ml | 4 ++-- common/AST.v | 4 ++-- cparser/ExtendedAsm.ml | 7 ++++--- extraction/extraction.v | 3 --- ia32/Machregs.v | 30 +++++++++++++++++++++++++++++- ia32/Machregsaux.ml | 31 +++++++++---------------------- ia32/Machregsaux.mli | 1 - powerpc/Machregs.v | 42 ++++++++++++++++++++++++++++++++++++++++++ powerpc/Machregsaux.ml | 43 +++++++++---------------------------------- powerpc/Machregsaux.mli | 1 - test/regression/extasm.c | 6 +++--- 17 files changed, 147 insertions(+), 110 deletions(-) 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 diff --git a/backend/Bounds.v b/backend/Bounds.v index 7528b66e..04c1328d 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -87,8 +87,6 @@ Section BOUNDS. Variable f: function. -Parameter mregs_of_clobber: list ident -> list mreg. - (** In the proof of the [Stacking] pass, we only need to bound the registers written by an instruction. Therefore, this function returns these registers, ignoring registers used only as @@ -103,7 +101,6 @@ Definition regs_of_instr (i: instruction) : list mreg := | Lstore chunk addr args src => nil | Lcall sig ros => nil | Ltailcall sig ros => nil - | Lbuiltin (EF_inline_asm txt typs clob) args res => res ++ mregs_of_clobber clob | Lbuiltin ef args res => res ++ destroyed_by_builtin ef | Lannot ef args => nil | Llabel lbl => nil @@ -354,9 +351,7 @@ Proof. (* call *) eapply size_arguments_bound; eauto. (* builtin *) - apply H1. destruct e; apply in_or_app; auto. - change (destroyed_by_builtin (EF_inline_asm text sg clobbers)) with (@nil mreg) in H2. - simpl in H2; tauto. + apply H1. apply in_or_app; auto. (* annot *) apply H0. rewrite slots_of_locs_charact; auto. Qed. diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml index c286e946..aa4efc53 100644 --- a/backend/Regalloc.ml +++ b/backend/Regalloc.ml @@ -585,13 +585,11 @@ let add_interfs_instr g instr live = (* like a move *) IRC.add_pref g arg res | EF_inline_asm(txt, sg, clob), _, _ -> - (* clobbered regs interfere with live set - and also with res and args for GCC compatibility *) + (* clobbered regs interfere with res and args for GCC compatibility *) List.iter (fun c -> - match Machregsaux.register_by_name (extern_atom c) with + match Machregs.register_by_name c with | None -> () | Some mr -> - add_interfs_destroyed g across [mr]; add_interfs_list_mreg g args mr; if sg.sig_res <> None then add_interfs_list_mreg g res mr) clob diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 94f13aa1..6ecdb14e 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -847,7 +847,7 @@ let convertAsm loc env txt outputs inputs clobber = let (txt', output', inputs') = ExtendedAsm.transf_asm loc env txt outputs inputs clobber in let clobber' = - List.map intern_string clobber in + List.map (fun s -> coqstring_of_camlstring (String.uppercase s)) clobber in let ty_res = match output' with None -> TVoid [] | Some e -> e.etyp in (* Build the Ebuiltin expression *) diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 39de282b..bde61cc7 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -299,9 +299,9 @@ and extended_asm p txt res args clob = begin match clob with | [] -> () | c1 :: cl -> - fprintf p "@ : @[%S" (extern_atom c1); + fprintf p "@ : @[%S" (camlstring_of_coqstring c1); List.iter - (fun c -> fprintf p ",@ %S" (extern_atom c)) + (fun c -> fprintf p ",@ %S" (camlstring_of_coqstring c)) cl; fprintf p "@]" end; diff --git a/common/AST.v b/common/AST.v index 2550844b..08a19789 100644 --- a/common/AST.v +++ b/common/AST.v @@ -584,7 +584,7 @@ Inductive external_function : Type := (** Another form of annotation that takes one argument, produces an event carrying the text and the value of this argument, and returns the value of the argument. *) - | EF_inline_asm (text: ident) (sg: signature) (clobbers: list ident). + | EF_inline_asm (text: ident) (sg: signature) (clobbers: list String.string). (** Inline [asm] statements. Semantically, treated like an annotation with no parameters ([EF_annot text nil]). To be used with caution, as it can invalidate the semantic @@ -642,7 +642,7 @@ Proof. generalize ident_eq signature_eq chunk_eq typ_eq zeq Int.eq_dec; intros. decide equality. apply list_eq_dec. auto. - apply list_eq_dec. auto. + apply list_eq_dec. apply String.string_dec. Defined. Global Opaque external_function_eq. diff --git a/cparser/ExtendedAsm.ml b/cparser/ExtendedAsm.ml index 94d23102..fbf8d569 100644 --- a/cparser/ExtendedAsm.ml +++ b/cparser/ExtendedAsm.ml @@ -161,9 +161,10 @@ let transf_outputs loc env = function let check_clobbers loc clob = List.iter (fun c -> - if Machregsaux.register_by_name c <> None - || List.mem c Machregsaux.scratch_register_names - || c = "memory" || c = "cc" + let c' = String.uppercase c in + if Machregsaux.register_by_name c' <> None + || List.mem c' Machregsaux.scratch_register_names + || c' = "MEMORY" || c' = "CC" then () else error "%aError: unrecognized asm register clobber '%s'" formatloc loc c) diff --git a/extraction/extraction.v b/extraction/extraction.v index 4c400036..f7e99545 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -77,9 +77,6 @@ Extract Constant Allocation.regalloc => "Regalloc.regalloc". (* Linearize *) Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux". -(* Bounds *) -Extract Constant Bounds.mregs_of_clobber => "Machregsaux.mregs_of_clobber". - (* SimplExpr *) Extract Constant SimplExpr.first_unused_ident => "Camlcoq.first_unused_ident". Extraction Inline SimplExpr.ret SimplExpr.error SimplExpr.bind SimplExpr.bind2. 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/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/test/regression/extasm.c b/test/regression/extasm.c index 4925392e..00a1cd57 100644 --- a/test/regression/extasm.c +++ b/test/regression/extasm.c @@ -1,7 +1,7 @@ /* Testing extended asm. To run the test, compile with -S and grep "TEST" in the generated .s */ -int clobbers(int x) +int clobbers(int x, int z) { int y; asm("TEST0 out:%0 in:%1" : "=r"(y) : "r"(x) : "cc" @@ -10,10 +10,10 @@ int clobbers(int x) #elif defined(__arm__) , "r0", "r1", "r4" #elif defined(__PPC__) - , "r3", "r4", "r31" + , "r0", "r3", "r4", "r31" #endif ); - return y; + return y + z; } int main() -- 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 +++++++++++++++++++++ ia32/PrintOp.ml | 12 ++++++++++++ powerpc/PrintOp.ml | 8 ++++++++ 3 files changed, 41 insertions(+) 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 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/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 ad613e10f78bfe11e2df2ec055bcd02406456476 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 13 May 2015 18:56:53 +0200 Subject: Changed the enter_or_refine_ident function to produce an error if a non-static declaration is followed by a static declaration/definition. --- cparser/Elab.ml | 20 ++++++++++++++------ 1 file changed, 14 insertions(+), 6 deletions(-) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 10af10a1..4e8ef214 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1801,12 +1801,20 @@ let enter_or_refine_ident local loc env s sto ty = | None -> warning loc "redefinition of '%s' with incompatible type" s; ty in let new_sto = - if old_sto = Storage_extern then sto else - if sto = Storage_extern then old_sto else - if old_sto = sto then sto else begin - warning loc "redefinition of '%s' with incompatible storage class" s; - sto - end in + (* The only case not allowed is removing static *) + match old_sto,sto with + | Storage_static,Storage_static + | Storage_extern,Storage_extern + | Storage_register,Storage_register + | Storage_default,Storage_default -> sto + | _,Storage_static -> + error loc "static redefinition of '%s' after non-static definition" s; sto + | Storage_static,_ -> Storage_static (* Static stays static *) + | Storage_extern,_ -> sto + | _,Storage_extern -> old_sto + | _,Storage_register + | Storage_register,_ -> Storage_register + in (id, new_sto, Env.add_ident env id new_sto new_ty) | Some(id, II_enum v) when Env.in_current_scope env id -> error loc "illegal redefinition of enumerator '%s'" s; -- 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 +-- backend/PrintAnnot.ml | 182 ----------------------------------------------- backend/PrintAsm.ml | 6 +- backend/PrintAsmaux.ml | 160 +++++++++++++++++++++++++++++++++++++++++ debug/CtoDwarf.ml | 2 +- ia32/TargetPrinter.ml | 8 +-- powerpc/TargetPrinter.ml | 12 ++-- 7 files changed, 178 insertions(+), 200 deletions(-) delete mode 100644 backend/PrintAnnot.ml 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... *) | _ -> diff --git a/backend/PrintAnnot.ml b/backend/PrintAnnot.ml deleted file mode 100644 index 88f5d8d6..00000000 --- a/backend/PrintAnnot.ml +++ /dev/null @@ -1,182 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(* Printing annotations in asm syntax *) - -open Printf -open Datatypes -open Integers -open Floats -open Camlcoq -open AST -open Memdata -open Asm - -(** All files used in the debug entries *) -module StringSet = Set.Make(String) -let all_files : StringSet.t ref = ref StringSet.empty -let add_file file = - all_files := StringSet.add file !all_files - - -(** Line number annotations *) - -let filename_info : (string, int * Printlines.filebuf option) Hashtbl.t - = Hashtbl.create 7 - -let last_file = ref "" - -let reset_filenames () = - Hashtbl.clear filename_info; last_file := "" - -let close_filenames () = - Hashtbl.iter - (fun file (num, fb) -> - match fb with Some b -> Printlines.close b | None -> ()) - filename_info; - reset_filenames() - -let enter_filename f = - let num = Hashtbl.length filename_info + 1 in - let filebuf = - if !Clflags.option_S || !Clflags.option_dasm then begin - try Some (Printlines.openfile f) - with Sys_error _ -> None - end else None in - Hashtbl.add filename_info f (num, filebuf); - (num, filebuf) - -(* Add file and line debug location, using GNU assembler-style DWARF2 - directives *) - -let print_file_line oc pref file line = - if !Clflags.option_g && file <> "" then begin - let (filenum, filebuf) = - try - Hashtbl.find filename_info file - with Not_found -> - let (filenum, filebuf as res) = enter_filename file in - fprintf oc " .file %d %S\n" filenum file; - res in - fprintf oc " .loc %d %d\n" filenum line; - match filebuf with - | None -> () - | Some fb -> Printlines.copy oc pref fb line line - end - -(* Add file and line debug location, using DWARF2 directives in the style - of Diab C 5 *) - -let print_file_line_d2 oc pref file line = - if !Clflags.option_g && file <> "" then begin - let (_, filebuf) = - try - Hashtbl.find filename_info file - with Not_found -> - enter_filename file in - if file <> !last_file then begin - fprintf oc " .d2file %S\n" file; - last_file := file - end; - fprintf oc " .d2line %d\n" line; - match filebuf with - | None -> () - | Some fb -> Printlines.copy oc pref fb line line - end - -(** "True" annotations *) - -let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*" - -let rec print_annot print_preg sp_reg_name oc = function - | AA_base x -> print_preg oc x - | AA_int n -> fprintf oc "%ld" (camlint_of_coqint n) - | AA_long n -> fprintf oc "%Ld" (camlint64_of_coqint n) - | AA_float n -> fprintf oc "%.18g" (camlfloat_of_coqfloat n) - | AA_single n -> fprintf oc "%.18g" (camlfloat_of_coqfloat32 n) - | AA_loadstack(chunk, ofs) -> - fprintf oc "mem(%s + %ld, %ld)" - sp_reg_name - (camlint_of_coqint ofs) - (camlint_of_coqint (size_chunk chunk)) - | AA_addrstack ofs -> - fprintf oc "(%s + %ld)" - sp_reg_name - (camlint_of_coqint ofs) - | AA_loadglobal(chunk, id, ofs) -> - fprintf oc "mem(\"%s\" + %ld, %ld)" - (extern_atom id) - (camlint_of_coqint ofs) - (camlint_of_coqint (size_chunk chunk)) - | AA_addrglobal(id, ofs) -> - fprintf oc "(\"%s\" + %ld)" - (extern_atom id) - (camlint_of_coqint ofs) - | AA_longofwords(hi, lo) -> - fprintf oc "(%a * 0x100000000 + %a)" - (print_annot print_preg sp_reg_name) hi - (print_annot print_preg sp_reg_name) lo - -let print_annot_text print_preg sp_reg_name oc txt args = - let print_fragment = function - | Str.Text s -> - output_string oc s - | Str.Delim "%%" -> - output_char oc '%' - | Str.Delim s -> - let n = int_of_string (String.sub s 1 (String.length s - 1)) in - try - print_annot print_preg sp_reg_name oc (List.nth args (n-1)) - with Failure _ -> - fprintf oc "" s in - List.iter print_fragment (Str.full_split re_annot_param txt); - fprintf oc "\n" - -let print_annot_stmt print_preg sp_reg_name oc txt tys args = - print_annot_text print_preg sp_reg_name oc txt args - -let print_annot_val print_preg oc txt args = - print_annot_text print_preg "" oc txt - (List.map (fun r -> AA_base r) args) - -(** Inline assembly *) - -let re_asm_param = Str.regexp "%%\\|%[0-9]+" - -let print_inline_asm print_preg oc txt sg args res = - let operands = - if sg.sig_res = None then args else res @ args in - let print_fragment = function - | Str.Text s -> - output_string oc s - | Str.Delim "%%" -> - output_char oc '%' - | Str.Delim s -> - let n = int_of_string (String.sub s 1 (String.length s - 1)) in - try - print_preg oc (List.nth operands n) - with Failure _ -> - fprintf oc "" s in - List.iter print_fragment (Str.full_split re_asm_param txt); - fprintf oc "\n" - - -(** Print CompCert version and command-line as asm comment *) - -let print_version_and_options oc comment = - fprintf oc "%s File generated by CompCert %s\n" comment Configuration.version; - fprintf oc "%s Command line:" comment; - for i = 1 to Array.length Sys.argv - 1 do - fprintf oc " %s" Sys.argv.(i) - done; - fprintf oc "\n" - diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml index 0438a40f..e91b4e03 100644 --- a/backend/PrintAsm.ml +++ b/backend/PrintAsm.ml @@ -130,12 +130,12 @@ module Printer(Target:TARGET) = let print_program oc p db = let module Target = (val (sel_target ()):TARGET) in let module Printer = Printer(Target) in - PrintAnnot.reset_filenames (); - PrintAnnot.print_version_and_options oc Target.comment; + reset_filenames (); + print_version_and_options oc Target.comment; Target.print_prologue oc; List.iter (Printer.print_globdef oc) p.prog_defs; Target.print_epilogue oc; - PrintAnnot.close_filenames (); + close_filenames (); if !Clflags.option_g && Configuration.advanced_debug then begin match db with diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 8bc961ef..497760c1 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -16,6 +16,7 @@ open Asm open Camlcoq open DwarfTypes open Datatypes +open Memdata open Printf open Sections @@ -140,3 +141,162 @@ let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$" (* Basic printing functions *) let coqint oc n = fprintf oc "%ld" (camlint_of_coqint n) + +(* Printing annotations in asm syntax *) +(** All files used in the debug entries *) +module StringSet = Set.Make(String) +let all_files : StringSet.t ref = ref StringSet.empty +let add_file file = + all_files := StringSet.add file !all_files + + +let filename_info : (string, int * Printlines.filebuf option) Hashtbl.t + = Hashtbl.create 7 + +let last_file = ref "" + +let reset_filenames () = + Hashtbl.clear filename_info; last_file := "" + +let close_filenames () = + Hashtbl.iter + (fun file (num, fb) -> + match fb with Some b -> Printlines.close b | None -> ()) + filename_info; + reset_filenames() + +let enter_filename f = + let num = Hashtbl.length filename_info + 1 in + let filebuf = + if !Clflags.option_S || !Clflags.option_dasm then begin + try Some (Printlines.openfile f) + with Sys_error _ -> None + end else None in + Hashtbl.add filename_info f (num, filebuf); + (num, filebuf) + +(* Add file and line debug location, using GNU assembler-style DWARF2 + directives *) + +let print_file_line oc pref file line = + if !Clflags.option_g && file <> "" then begin + let (filenum, filebuf) = + try + Hashtbl.find filename_info file + with Not_found -> + let (filenum, filebuf as res) = enter_filename file in + fprintf oc " .file %d %S\n" filenum file; + res in + fprintf oc " .loc %d %d\n" filenum line; + match filebuf with + | None -> () + | Some fb -> Printlines.copy oc pref fb line line + end + +(* Add file and line debug location, using DWARF2 directives in the style + of Diab C 5 *) + +let print_file_line_d2 oc pref file line = + if !Clflags.option_g && file <> "" then begin + let (_, filebuf) = + try + Hashtbl.find filename_info file + with Not_found -> + enter_filename file in + if file <> !last_file then begin + fprintf oc " .d2file %S\n" file; + last_file := file + end; + fprintf oc " .d2line %d\n" line; + match filebuf with + | None -> () + | Some fb -> Printlines.copy oc pref fb line line + end + + +(** "True" annotations *) + +let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*" + +let rec print_annot print_preg sp_reg_name oc = function + | AA_base x -> print_preg oc x + | AA_int n -> fprintf oc "%ld" (camlint_of_coqint n) + | AA_long n -> fprintf oc "%Ld" (camlint64_of_coqint n) + | AA_float n -> fprintf oc "%.18g" (camlfloat_of_coqfloat n) + | AA_single n -> fprintf oc "%.18g" (camlfloat_of_coqfloat32 n) + | AA_loadstack(chunk, ofs) -> + fprintf oc "mem(%s + %ld, %ld)" + sp_reg_name + (camlint_of_coqint ofs) + (camlint_of_coqint (size_chunk chunk)) + | AA_addrstack ofs -> + fprintf oc "(%s + %ld)" + sp_reg_name + (camlint_of_coqint ofs) + | AA_loadglobal(chunk, id, ofs) -> + fprintf oc "mem(\"%s\" + %ld, %ld)" + (extern_atom id) + (camlint_of_coqint ofs) + (camlint_of_coqint (size_chunk chunk)) + | AA_addrglobal(id, ofs) -> + fprintf oc "(\"%s\" + %ld)" + (extern_atom id) + (camlint_of_coqint ofs) + | AA_longofwords(hi, lo) -> + fprintf oc "(%a * 0x100000000 + %a)" + (print_annot print_preg sp_reg_name) hi + (print_annot print_preg sp_reg_name) lo + +let print_annot_text print_preg sp_reg_name oc txt args = + let print_fragment = function + | Str.Text s -> + output_string oc s + | Str.Delim "%%" -> + output_char oc '%' + | Str.Delim s -> + let n = int_of_string (String.sub s 1 (String.length s - 1)) in + try + print_annot print_preg sp_reg_name oc (List.nth args (n-1)) + with Failure _ -> + fprintf oc "" s in + List.iter print_fragment (Str.full_split re_annot_param txt); + fprintf oc "\n" + +let print_annot_stmt print_preg sp_reg_name oc txt tys args = + print_annot_text print_preg sp_reg_name oc txt args + +let print_annot_val print_preg oc txt args = + print_annot_text print_preg "" oc txt + (List.map (fun r -> AA_base r) args) + +(** Inline assembly *) + +let re_asm_param = Str.regexp "%%\\|%[0-9]+" + +let print_inline_asm print_preg oc txt sg args res = + let operands = + if sg.sig_res = None then args else res @ args in + let print_fragment = function + | Str.Text s -> + output_string oc s + | Str.Delim "%%" -> + output_char oc '%' + | Str.Delim s -> + let n = int_of_string (String.sub s 1 (String.length s - 1)) in + try + print_preg oc (List.nth operands n) + with Failure _ -> + fprintf oc "" s in + List.iter print_fragment (Str.full_split re_asm_param txt); + fprintf oc "\n" + + +(** Print CompCert version and command-line as asm comment *) + +let print_version_and_options oc comment = + fprintf oc "%s File generated by CompCert %s\n" comment Configuration.version; + fprintf oc "%s Command line:" comment; + for i = 1 to Array.length Sys.argv - 1 do + fprintf oc " %s" Sys.argv.(i) + done; + fprintf oc "\n" diff --git a/debug/CtoDwarf.ml b/debug/CtoDwarf.ml index b1eea8f3..a352e99f 100644 --- a/debug/CtoDwarf.ml +++ b/debug/CtoDwarf.ml @@ -459,7 +459,7 @@ let union_to_dwarf (n,at,m) env gloc = (* Translate global declarations to there dwarf representation *) let globdecl_to_dwarf env (typs,decls) decl = - PrintAnnot.add_file (fst decl.gloc); + PrintAsmaux.add_file (fst decl.gloc); match decl.gdesc with | Gtypedef (n,t) -> let ret = typedef_to_dwarf (n,t) decl.gloc in typs@ret,decls 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 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 From 5d017f110f6c23c29a182465ab7832a944c0ba26 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 14 May 2015 12:53:02 +0200 Subject: Make a register as storage specify to a fatal error. --- cparser/Elab.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 4e8ef214..fe74a786 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1862,7 +1862,7 @@ let enter_decdefs local loc env sto dl = let elab_fundef env spec name body loc = let (s, sto, inline, ty, env1) = elab_name env spec name in if sto = Storage_register then - error loc "a function definition cannot have 'register' storage class"; + fatal_error loc "a function definition cannot have 'register' storage class"; (* Fix up the type. We can have params = None but only for an old-style parameterless function "int f() {...}" *) let ty = -- cgit