From 378ac3925503e6efd24cc34796e85d95c031e72d Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 13 Sep 2015 11:44:32 +0200 Subject: Use PowerPC 64 bits instructions (when available) for int<->FP conversions. Also: implement __builtin_isel on non-EREF platforms with a branch-free instruction sequence. Also: extend ./configure so that it recognizes "ppc64-" and "e5500-" platforms in addition to "ppc-". --- powerpc/Asmexpand.ml | 53 ++++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 51 insertions(+), 2 deletions(-) (limited to 'powerpc/Asmexpand.ml') diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 3fffc037..49f796ca 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -23,6 +23,13 @@ open Asmexpandaux exception Error of string +(* FreeScale's EREF extensions *) + +let eref = + match Configuration.model with + | "e5500" -> true + | _ -> false + (* Useful constants and helper functions *) let _0 = Integers.Int.zero @@ -485,8 +492,24 @@ let expand_builtin_inline name args res = emit (Plwz (res, Cint! retaddr_offset,GPR1)) (* isel *) | "__builtin_isel", [BA (IR a1); BA (IR a2); BA (IR a3)],BR (IR res) -> - emit (Pcmpwi (a1,Cint (Int.zero))); - emit (Pisel (res,a3,a2,CRbit_2)) + if eref then begin + emit (Pcmpwi (a1,Cint (Int.zero))); + emit (Pisel (res,a3,a2,CRbit_2)) + end else if a2 = a3 then + emit (Pmr (res, a2)) + else begin + (* a1 has type _Bool, hence it is 0 or 1 *) + emit (Psubfic (GPR0, a1, Cint _0)); + (* r0 = 0xFFFF_FFFF if a1 is true, r0 = 0 if a1 is false *) + if res <> a3 then begin + emit (Pand_ (res, a2, GPR0)); + emit (Pandc (GPR0, a3, GPR0)) + end else begin + emit (Pandc (res, a3, GPR0)); + emit (Pand_ (GPR0, a2, GPR0)) + end; + emit (Por (res, res, GPR0)) + end (* Catch-all *) | _ -> raise (Error ("unrecognized builtin " ^ name)) @@ -547,6 +570,24 @@ let expand_instruction instr = emit (Paddi(GPR1, GPR1, Cint(coqint_of_camlint sz))) else emit (Plwz(GPR1, Cint ofs, GPR1)) + | Pfcfi(r1, r2) -> + assert (Archi.ppc64); + emit (Pextsw(GPR0, r2)); + emit (Pstdu(GPR0, Cint _m8, GPR1)); + emit (Pcfi_adjust _8); + emit (Plfd(r1, Cint _0, GPR1)); + emit (Pfcfid(r1, r1)); + emit (Paddi(GPR1, GPR1, Cint _8)); + emit (Pcfi_adjust _m8) + | Pfcfiu(r1, r2) -> + assert (Archi.ppc64); + emit (Prldicl(GPR0, r2, _0, coqint_of_camlint 32l)); + emit (Pstdu(GPR0, Cint _m8, GPR1)); + emit (Pcfi_adjust _8); + emit (Plfd(r1, Cint _0, GPR1)); + emit (Pfcfid(r1, r1)); + emit (Paddi(GPR1, GPR1, Cint _8)); + emit (Pcfi_adjust _m8) | Pfcti(r1, r2) -> emit (Pfctiwz(FPR13, r2)); emit (Pstfdu(FPR13, Cint _m8, GPR1)); @@ -554,6 +595,14 @@ let expand_instruction instr = emit (Plwz(r1, Cint _4, GPR1)); emit (Paddi(GPR1, GPR1, Cint _8)); emit (Pcfi_adjust _m8) + | Pfctiu(r1, r2) -> + assert (Archi.ppc64); + emit (Pfctidz(FPR13, r2)); + emit (Pstfdu(FPR13, Cint _m8, GPR1)); + emit (Pcfi_adjust _8); + emit (Plwz(r1, Cint _4, GPR1)); + emit (Paddi(GPR1, GPR1, Cint _8)); + emit (Pcfi_adjust _m8) | Pfmake(rd, r1, r2) -> emit (Pstwu(r1, Cint _m8, GPR1)); emit (Pcfi_adjust _8); -- cgit From ed1f32134283d3cd4f939a26dfd99992ec48da86 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 8 Oct 2015 13:27:50 +0200 Subject: Moved expandation of debug information to Asmexpandaux. The function is generalized to work for all backends and takes as additional arguments functions for the printing of the simple instructions and the translation function for the arguments. --- powerpc/Asmexpand.ml | 71 ++++------------------------------------------------ 1 file changed, 5 insertions(+), 66 deletions(-) (limited to 'powerpc/Asmexpand.ml') diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index a2cfb136..878c7e5d 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -668,7 +668,7 @@ let preg_to_dwarf_int = function let translate_annot annot = let rec aux = function - | BA x -> Some (BA (preg_to_dwarf_int x)) + | BA x -> Some (1,BA (preg_to_dwarf_int x)) | BA_int _ | BA_long _ | BA_float _ @@ -676,11 +676,11 @@ let translate_annot annot = | BA_loadglobal _ | BA_addrglobal _ | BA_loadstack _ -> None - | BA_addrstack ofs -> Some (BA_addrstack ofs) + | BA_addrstack ofs -> Some (1,BA_addrstack ofs) | BA_splitlong (hi,lo) -> begin match (aux hi,aux lo) with - | Some hi ,Some lo -> Some (BA_splitlong (hi,lo)) + | Some (_,hi) ,Some (_,lo) -> Some (1,BA_splitlong (hi,lo)) | _,_ -> None end in (match annot with @@ -692,73 +692,12 @@ let expand_scope id lbl oldscopes newscopes = and closing = List.filter (fun a -> not (List.mem a newscopes)) oldscopes in List.iter (fun i -> Debug.open_scope id i lbl) opening; List.iter (fun i -> Debug.close_scope id i lbl) closing - -let expand_instruction id l = - let get_lbl = function - | None -> - let lbl = new_label () in - emit (Plabel lbl); - lbl - | Some lbl -> lbl in - let rec aux lbl scopes = function - | [] -> let lbl = get_lbl lbl in - Debug.function_end id lbl - | (Pbuiltin(EF_debug (kind,txt,_x),args,_) as i)::rest -> - let kind = (P.to_int kind) in - begin - match kind with - | 1-> - emit i;aux lbl scopes rest - | 2 -> - aux lbl scopes rest - | 3 -> - begin - match translate_annot args with - | Some a -> - let lbl = get_lbl lbl in - Debug.start_live_range (id,txt) lbl (1,a); - aux (Some lbl) scopes rest - | None -> aux lbl scopes rest - end - | 4 -> - let lbl = get_lbl lbl in - Debug.end_live_range (id,txt) lbl; - aux (Some lbl) scopes rest - | 5 -> - begin - match translate_annot args with - | Some a-> - Debug.stack_variable (id,txt) (1,a); - aux lbl scopes rest - | _ -> aux lbl scopes rest - end - | 6 -> - let lbl = get_lbl lbl in - let scopes' = List.map (function BA_int x -> Int32.to_int (camlint_of_coqint x) | _ -> assert false) args in - expand_scope id lbl scopes scopes'; - aux (Some lbl) scopes' rest - | _ -> - aux None scopes rest - end - | i::rest -> expand_instruction_simple i; aux None scopes rest in - (* We need to move all closing debug annotations before the last real statement *) - let rec move_debug acc bcc = function - | (Pbuiltin(EF_debug (kind,_,_),_,_) as i)::rest -> - let kind = (P.to_int kind) in - if kind = 1 then - move_debug acc (i::bcc) rest (* Do not move debug line *) - else - move_debug (i::acc) bcc rest (* Move the debug annotations forward *) - | b::rest -> List.rev ((List.rev (b::bcc)@List.rev acc)@rest) (* We found the first non debug location *) - | [] -> List.rev acc (* This actually can never happen *) in - aux None [] (move_debug [] [] (List.rev l)) - - + let expand_function id fn = try set_current_function fn; if !Clflags.option_g then - expand_instruction id fn.fn_code + expand_debug id translate_annot expand_instruction_simple fn.fn_code else List.iter expand_instruction_simple fn.fn_code; Errors.OK (get_current_function ()) -- cgit From f0a5038b4e4220300637d3e9e918d9ec31623108 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 8 Oct 2015 15:33:47 +0200 Subject: Added versions of the tranform_* functions in AST to work with functions taking the ident as argument. This functions are currently not used inside the proven part but it is nice to have them already there, when they are used by some future pass. They also come equiped with the corresponding proofs. --- powerpc/Asmexpand.ml | 23 +---------------------- 1 file changed, 1 insertion(+), 22 deletions(-) (limited to 'powerpc/Asmexpand.ml') diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 878c7e5d..bf7e4c3e 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -713,26 +713,5 @@ let expand_fundef id = function | External ef -> Errors.OK (External ef) -let rec transform_partial_prog transfun p = - match p with - | [] -> Errors.OK [] - | (id,Gvar v)::l -> - (match transform_partial_prog transfun l with - | Errors.OK x -> Errors.OK ((id,Gvar v)::x) - | Errors.Error msg -> Errors.Error msg) - | (id,Gfun f)::l -> - (match transfun id f with - | Errors.OK tf -> - (match transform_partial_prog transfun l with - | Errors.OK x -> Errors.OK ((id,Gfun tf)::x) - | Errors.Error msg -> Errors.Error msg) - | Errors.Error msg -> - Errors.Error ((Errors.MSG (coqstring_of_camlstring "In function"))::((Errors.CTX - id) :: (Errors.MSG (coqstring_of_camlstring ": ") :: msg)))) - let expand_program (p: Asm.program) : Asm.program Errors.res = - match transform_partial_prog expand_fundef p.prog_defs with - | Errors.OK x-> - Errors.OK { prog_defs = x; prog_public = p.prog_public; prog_main = - p.prog_main } - | Errors.Error msg -> Errors.Error msg + AST.transform_partial_ident_program expand_fundef p -- cgit From 0ffd562ae1941e37471ac0c2b8f93bed1de26441 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 9 Oct 2015 11:06:24 +0200 Subject: Filled in the rest of the funciton needed for thte debug info under arm. The name_of_section function no returns the correct name for the debug sections, the prologue and epilogue directives are added and the labels for the live ranges are introduced in the Asmexpand pass. --- powerpc/Asmexpand.ml | 12 +++--------- 1 file changed, 3 insertions(+), 9 deletions(-) (limited to 'powerpc/Asmexpand.ml') diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index bf7e4c3e..fb569a00 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -563,7 +563,7 @@ let num_crbit = function | CRbit_3 -> 3 | CRbit_6 -> 6 -let expand_instruction_simple instr = +let expand_instruction instr = match instr with | Pallocframe(sz, ofs,retofs) -> let variadic = (!current_function).fn_sig.sig_cc.cc_vararg in @@ -687,19 +687,13 @@ let translate_annot annot = | [] -> None | a::_ -> aux a) -let expand_scope id lbl oldscopes newscopes = - let opening = List.filter (fun a -> not (List.mem a oldscopes)) newscopes - and closing = List.filter (fun a -> not (List.mem a newscopes)) oldscopes in - List.iter (fun i -> Debug.open_scope id i lbl) opening; - List.iter (fun i -> Debug.close_scope id i lbl) closing - let expand_function id fn = try set_current_function fn; if !Clflags.option_g then - expand_debug id translate_annot expand_instruction_simple fn.fn_code + expand_debug id translate_annot expand_instruction fn.fn_code else - List.iter expand_instruction_simple fn.fn_code; + List.iter expand_instruction fn.fn_code; Errors.OK (get_current_function ()) with Error s -> Errors.Error (Errors.msg (coqstring_of_camlstring s)) -- cgit From b0c47e12f2bbff0905ad853b90169df16d87f6be Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 9 Oct 2015 16:36:16 +0200 Subject: Filled in missing functions for debug information on ia32. Like for arm and ppc the functions for section names and start and end addresses of compilation units are defined and the print_annot function is moved to Asmexpandaux.ml. --- powerpc/Asmexpand.ml | 25 ++----------------------- 1 file changed, 2 insertions(+), 23 deletions(-) (limited to 'powerpc/Asmexpand.ml') diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index fb569a00..00234f9b 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -660,38 +660,17 @@ let float_reg_to_dwarf = function | FPR24 -> 56 | FPR25 -> 57 | FPR26 -> 58 | FPR27 -> 59 | FPR28 -> 60 | FPR29 -> 61 | FPR30 -> 62 | FPR31 -> 63 -let preg_to_dwarf_int = function +let preg_to_dwarf = function | IR r -> int_reg_to_dwarf r | FR r -> float_reg_to_dwarf r | _ -> assert false -let translate_annot annot = - let rec aux = function - | BA x -> Some (1,BA (preg_to_dwarf_int x)) - | BA_int _ - | BA_long _ - | BA_float _ - | BA_single _ - | BA_loadglobal _ - | BA_addrglobal _ - | BA_loadstack _ -> None - | BA_addrstack ofs -> Some (1,BA_addrstack ofs) - | BA_splitlong (hi,lo) -> - begin - match (aux hi,aux lo) with - | Some (_,hi) ,Some (_,lo) -> Some (1,BA_splitlong (hi,lo)) - | _,_ -> None - end in - (match annot with - | [] -> None - | a::_ -> aux a) - let expand_function id fn = try set_current_function fn; if !Clflags.option_g then - expand_debug id translate_annot expand_instruction fn.fn_code + expand_debug id 2 preg_to_dwarf expand_instruction fn.fn_code else List.iter expand_instruction fn.fn_code; Errors.OK (get_current_function ()) -- cgit From 7a6bb90048db7a254e959b1e3c308bac5fe6c418 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 11 Oct 2015 17:43:59 +0200 Subject: Use Coq strings instead of idents to name external and builtin functions. The AST.ident type represents source-level identifiers as unique positive numbers. However, the mapping identifiers <-> AST.ident differs between runs of CompCert on different source files. This is problematic when we need to produce or recognize external functions and builtin functions with fixed names, for example: * in $ARCH/Machregs.v to define the register conventions for builtin functions; * in the VST program logic from Princeton to treat thread primitives specially. So far, we used AST.ident_of_string to recover the ident associated with a string. However, this function is defined in OCaml and doesn't execute within Coq. This is a problem both for VST and for future executability of CompCert within Coq. This commit replaces "ident" by "string" in the arguments of EF_external, EF_builtin, EF_inline_asm, EF_annot, and EF_annot_val. This provides stable names for externals and builtins, as needed. For inline asm and annotations, it's a matter of taste, but using strings feels more natural. EF_debug keeps using idents, since some kinds of EF_debug annotations talk about program variables. --- powerpc/Asmexpand.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'powerpc/Asmexpand.ml') diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 00234f9b..c88f6b6d 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -620,7 +620,7 @@ let expand_instruction instr = | Pbuiltin(ef, args, res) -> begin match ef with | EF_builtin(name, sg) -> - expand_builtin_inline (extern_atom name) args res + expand_builtin_inline (camlstring_of_coqstring name) args res | EF_vload chunk -> expand_builtin_vload chunk args res | EF_vstore chunk -> -- cgit From 6f622eba1bb242bbbda107a2ad36245c69841360 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 12 Oct 2015 13:12:27 +0200 Subject: Fix minor typo introduced by refactoring of debug information. The base register for the stack allocated variables should be r1 and not r2 under powerpc. Bug 17392 --- powerpc/Asmexpand.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'powerpc/Asmexpand.ml') diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 9e22e4e0..2fedf0c7 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -719,7 +719,7 @@ let expand_function id fn = try set_current_function fn; if !Clflags.option_g then - expand_debug id 2 preg_to_dwarf expand_instruction fn.fn_code + expand_debug id 1 preg_to_dwarf expand_instruction fn.fn_code else List.iter expand_instruction fn.fn_code; Errors.OK (get_current_function ()) -- cgit From 1cb3d93ff278ebbd0c6967c5f9401a97f9b618b4 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 23 Oct 2015 11:06:11 +0200 Subject: Added special treatment for large stack size for ppc. Since the stacksize is casted to signed int in the alloc frame function large stacksize lead to assembler containing overflows. Bug 17473. --- powerpc/Asmexpand.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'powerpc/Asmexpand.ml') diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 161d12b7..35aa02d5 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -484,7 +484,7 @@ let expand_builtin_inline name args res = | "__builtin_call_frame", _,BR (IR res) -> let sz = !current_function_stacksize and ofs = !linkregister_offset in - if sz < 0x8000l then + if sz < 0x8000l && sz >= 0l then emit (Paddi(res, GPR1, Cint(coqint_of_camlint sz))) else emit (Plwz(res, Cint ofs, GPR1)) @@ -594,7 +594,7 @@ let expand_instruction instr = assert (ofs = _0); let sz = if variadic then Int32.add sz 96l else sz in let adj = Int32.neg sz in - if adj >= -0x8000l then + if adj >= -0x8000l && adj < 0l then emit (Pstwu(GPR1, Cint(coqint_of_camlint adj), GPR1)) else begin emit_loadimm GPR0 (coqint_of_camlint adj); @@ -617,7 +617,7 @@ let expand_instruction instr = let variadic = (!current_function).fn_sig.sig_cc.cc_vararg in let sz = camlint_of_coqint sz in let sz = if variadic then Int32.add sz 96l else sz in - if sz < 0x8000l then + if sz < 0x8000l && sz >= 0l then emit (Paddi(GPR1, GPR1, Cint(coqint_of_camlint sz))) else emit (Plwz(GPR1, Cint ofs, GPR1)) -- cgit