diff options
| -rw-r--r-- | .gitignore | 3 | ||||
| -rw-r--r-- | Makefile.extr | 6 | ||||
| -rw-r--r-- | arm/TargetPrinter.ml | 2 | ||||
| -rw-r--r-- | backend/PrintAsmaux.ml | 6 | ||||
| -rw-r--r-- | cfrontend/C2C.ml | 29 | ||||
| -rw-r--r-- | cparser/Cleanup.ml | 5 | ||||
| -rw-r--r-- | cparser/Cutil.ml | 3 | ||||
| -rw-r--r-- | cparser/Lexer.mll | 9 | ||||
| -rw-r--r-- | cparser/Parse.ml | 2 | ||||
| -rw-r--r-- | cparser/StructReturn.ml | 4 | ||||
| -rw-r--r-- | debug/Debug.ml | 3 | ||||
| -rw-r--r-- | debug/Debug.mli | 2 | ||||
| -rw-r--r-- | debug/DebugInformation.ml | 10 | ||||
| -rw-r--r-- | debug/DebugInit.ml | 1 | ||||
| -rw-r--r-- | debug/DwarfPrinter.ml | 1 | ||||
| -rw-r--r-- | driver/Clflags.ml | 4 | ||||
| -rw-r--r-- | driver/Driver.ml | 38 | ||||
| -rw-r--r-- | ia32/Asmexpand.ml | 3 | ||||
| -rw-r--r-- | ia32/CBuiltins.ml | 3 | ||||
| -rw-r--r-- | ia32/TargetPrinter.ml | 2 | ||||
| -rw-r--r-- | lib/Readconfig.mll | 3 | ||||
| -rw-r--r-- | powerpc/Asm.v | 4 | ||||
| -rw-r--r-- | powerpc/AsmToJSON.ml | 1 | ||||
| -rw-r--r-- | powerpc/Asmexpand.ml | 68 | ||||
| -rw-r--r-- | powerpc/CBuiltins.ml | 20 | ||||
| -rw-r--r-- | powerpc/Machregs.v | 12 | ||||
| -rw-r--r-- | powerpc/TargetPrinter.ml | 11 | ||||
| -rw-r--r-- | runtime/arm/sysdeps.h | 4 | ||||
| -rw-r--r-- | runtime/include/stddef.h | 15 |
29 files changed, 194 insertions, 80 deletions
@@ -8,6 +8,9 @@ *.cmx *.cma *.cmxa +*.cmti +*.cmt +*.merlin # Emacs saves *~ # Executables and configuration diff --git a/Makefile.extr b/Makefile.extr index 3e37914e..971725f8 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -42,7 +42,7 @@ WARNINGS=-w -3 extraction/%.cmx: WARNINGS +=-w -20 extraction/%.cmo: WARNINGS +=-w -20 -COMPFLAGS=-g $(INCLUDES) $(MENHIR_INCLUDES) $(WARNINGS) +COMPFLAGS+=-g $(INCLUDES) $(MENHIR_INCLUDES) $(WARNINGS) # Using .opt compilers if available @@ -117,7 +117,7 @@ endif clean: rm -f $(EXECUTABLES) rm -f $(GENERATED) - for d in $(DIRS); do rm -f $$d/*.cm[iox] $$d/*.o; done + for d in $(DIRS); do rm -f $$d/*.cm[iotx] $$d/*cmti $$d/*.o; done rm -f backend/CMparser.automaton $(MAKE) -C cparser clean @@ -126,5 +126,3 @@ clean: depend: $(GENERATED) @echo "Analyzing OCaml dependencies" @$(OCAMLDEP) $(foreach d,$(DIRS),$(wildcard $(d)/*.mli $(d)/*.ml)) $(GENERATED) >.depend.extr || { rm -f .depend.extr; exit 2; } - - diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 9f2c66cf..22d41c4d 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -902,7 +902,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = fprintf oc " .%s\n" (if !Clflags.option_mthumb then "thumb" else "arm"); if !Clflags.option_g then begin section oc Section_text; - fprintf oc " .cfi_sections .debug_frame\n" + cfi_section oc end diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 4a612c26..0ca5b8e0 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -129,6 +129,12 @@ let cfi_rel_offset = else (fun _ _ _ -> ()) +let cfi_section = + if Configuration.asm_supports_cfi then + (fun oc -> fprintf oc " .cfi_sections .debug_frame\n") + else + (fun _ -> ()) + (* Basic printing functions *) let coqint oc n = fprintf oc "%ld" (camlint_of_coqint n) diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 8c7ec6d8..e4001e6b 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -466,6 +466,21 @@ let convertFkind = function if not !Clflags.option_flongdouble then unsupported "'long double' type"; F64 +let checkFunctionType env tres targs = + if not !Clflags.option_fstruct_passing then begin + if Cutil.is_composite_type env tres then + unsupported "function returning a struct or union (consider adding option -fstruct-passing)"; + begin match targs with + | None -> () + | Some l -> + List.iter + (fun (id, ty) -> + if Cutil.is_composite_type env ty then + unsupported "function parameter of struct or union type (consider adding option -fstruct-passing)") + l + end + end + let rec convertTyp env t = match t with | C.TVoid a -> Tvoid @@ -487,8 +502,7 @@ let rec convertTyp env t = | C.TArray(ty, Some sz, a) -> Tarray(convertTyp env ty, convertInt sz, convertAttr a) | C.TFun(tres, targs, va, a) -> - if Cutil.is_composite_type env tres then - unsupported "return type is a struct or union (consider adding option -fstruct-return)"; + checkFunctionType env tres targs; Tfunction(begin match targs with | None -> Tnil | Some tl -> convertParams env tl @@ -549,11 +563,6 @@ let string_of_type ty = Format.pp_print_flush fb (); Buffer.contents b -let supported_return_type env ty = - match Cutil.unroll env ty with - | C.TStruct _ | C.TUnion _ -> false - | _ -> true - let is_longlong env ty = match Cutil.unroll env ty with | C.TInt((C.ILongLong|C.IULongLong), _) -> true @@ -826,12 +835,11 @@ let rec convertExpr env e = targs, convertExprList env args, tres) | C.ECall(fn, args) -> - if not (supported_return_type env e.etyp) then - unsupported ("function returning a result of type " ^ string_of_type e.etyp ^ " (consider adding option -fstruct-return)"); begin match projFunType env fn.etyp with | None -> error "wrong type for function part of a call" | Some(tres, targs, va) -> + checkFunctionType env tres targs; if targs = None && not !Clflags.option_funprototyped then unsupported "call to unprototyped function (consider adding option -funprototyped)"; if va && not !Clflags.option_fvararg_calls then @@ -1039,8 +1047,7 @@ and convertSwitch env is_64 = function (** Function definitions *) let convertFundef loc env fd = - if Cutil.is_composite_type env fd.fd_ret then - unsupported "function returning a struct or union (consider adding option -fstruct-return)"; + checkFunctionType env fd.fd_ret (Some fd.fd_params); if fd.fd_vararg && not !Clflags.option_fvararg_calls then unsupported "variable-argument function (consider adding option -fvararg-calls)"; let ret = diff --git a/cparser/Cleanup.ml b/cparser/Cleanup.ml index c8a900d5..fe674d9b 100644 --- a/cparser/Cleanup.ml +++ b/cparser/Cleanup.ml @@ -186,7 +186,7 @@ let saturate p = let remove_unused_debug = function | Gdecl (_,id,_,_) -> Debug.remove_unused id - | Gfundef f -> Debug.remove_unused f.fd_name + | Gfundef f -> Debug.remove_unused_function f.fd_name | _ -> () let rec simpl_globdecls accu = function @@ -212,6 +212,3 @@ let program p = let p' = simpl_globdecls [] p in referenced := IdentSet.empty; p' - - - diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 1b0bf65d..1109cf79 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -310,6 +310,9 @@ let combine_types mode env t1 t2 = TUnion(comp_base s1 s2, comp_attr m a1 a2) | TEnum(s1, a1), TEnum(s2, a2) -> TEnum(comp_base s1 s2, comp_attr m a1 a2) + | TEnum(s,a1), TInt(enum_ikind,a2) + | TInt(enum_ikind,a2), TEnum (s,a1) -> + TEnum(s,comp_attr m a1 a2) | _, _ -> raise Incompat diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll index 6fac15e8..bcf2ada0 100644 --- a/cparser/Lexer.mll +++ b/cparser/Lexer.mll @@ -23,6 +23,7 @@ open Camlcoq module SSet = Set.Make(String) let lexicon : (string, Cabs.cabsloc -> token) Hashtbl.t = Hashtbl.create 17 +let ignored_keyworkds : SSet.t ref = ref SSet.empty let () = List.iter (fun (key, builder) -> Hashtbl.add lexicon key builder) @@ -81,7 +82,10 @@ let () = ("unsigned", fun loc -> UNSIGNED loc); ("void", fun loc -> VOID loc); ("volatile", fun loc -> VOLATILE loc); - ("while", fun loc -> WHILE loc)] + ("while", fun loc -> WHILE loc)]; + if Configuration.system <> "diab" then + (* We can ignore the __extension__ GCC keyword. *) + ignored_keyworkds := SSet.add "__extension__" !ignored_keyworkds let init_ctx = SSet.singleton "__builtin_va_list" let types_context : SSet.t ref = ref init_ctx @@ -325,6 +329,9 @@ rule initial = parse | "," { COMMA(currentLoc lexbuf) } | "." { DOT(currentLoc lexbuf) } | identifier as id { + if SSet.mem id !ignored_keyworkds then + initial lexbuf + else try Hashtbl.find lexicon id (currentLoc lexbuf) with Not_found -> PRE_NAME id } | eof { EOF } diff --git a/cparser/Parse.ml b/cparser/Parse.ml index 1d92d5a5..c125e653 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -39,7 +39,7 @@ let parse_transformations s = !t let read_file sourcefile = - let ic = open_in sourcefile in + let ic = open_in_bin sourcefile in let n = in_channel_length ic in let text = really_input_string ic n in close_in ic; diff --git a/cparser/StructReturn.ml b/cparser/StructReturn.ml index 82c0a04c..4e019380 100644 --- a/cparser/StructReturn.ml +++ b/cparser/StructReturn.ml @@ -582,11 +582,11 @@ let program p = struct_passing_style := if !Clflags.option_interp then SP_ref_callee - else !Clflags.option_fstruct_passing_style; + else Configuration.struct_passing_style; struct_return_style := if !Clflags.option_interp then SR_ref - else !Clflags.option_fstruct_return_style; + else Configuration.struct_return_style; Transform.program ~decl:transf_decl ~fundef:transf_fundef diff --git a/debug/Debug.ml b/debug/Debug.ml index 789ecb70..775a0903 100644 --- a/debug/Debug.ml +++ b/debug/Debug.ml @@ -48,6 +48,7 @@ type implem = compute_gnu_file_enum: (string -> unit) -> unit; exists_section: section_name -> bool; remove_unused: ident -> unit; + remove_unused_function: ident -> unit; variable_printed: string -> unit; add_diab_info: section_name -> int -> int -> int -> unit; } @@ -79,6 +80,7 @@ let default_implem = compute_gnu_file_enum = (fun _ -> ()); exists_section = (fun _ -> true); remove_unused = (fun _ -> ()); + remove_unused_function = (fun _ -> ()); variable_printed = (fun _ -> ()); add_diab_info = (fun _ _ _ _ -> ()); } @@ -110,5 +112,6 @@ let exists_section sec = !implem.exists_section sec let compute_diab_file_enum end_l entry_l line_e = !implem.compute_diab_file_enum end_l entry_l line_e let compute_gnu_file_enum f = !implem.compute_gnu_file_enum f let remove_unused ident = !implem.remove_unused ident +let remove_unused_function ident = !implem.remove_unused_function ident let variable_printed ident = !implem.variable_printed ident let add_diab_info sec line_start debug_info low_pc = !implem.add_diab_info sec line_start debug_info low_pc diff --git a/debug/Debug.mli b/debug/Debug.mli index 614fe84b..387491c2 100644 --- a/debug/Debug.mli +++ b/debug/Debug.mli @@ -46,6 +46,7 @@ type implem = compute_gnu_file_enum: (string -> unit) -> unit; exists_section: section_name -> bool; remove_unused: ident -> unit; + remove_unused_function: ident -> unit; variable_printed: string -> unit; add_diab_info: section_name -> int -> int -> int -> unit; } @@ -79,5 +80,6 @@ val compute_diab_file_enum: (section_name -> int) -> (string-> int) -> (unit -> val compute_gnu_file_enum: (string -> unit) -> unit val exists_section: section_name -> bool val remove_unused: ident -> unit +val remove_unused_function: ident -> unit val variable_printed: string -> unit val add_diab_info: section_name -> int -> int -> int -> unit diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml index ed00ea0d..be322a55 100644 --- a/debug/DebugInformation.ml +++ b/debug/DebugInformation.ml @@ -295,6 +295,16 @@ let gen_comp_typ sou id at = let remove_unused id = try let id' = Hashtbl.find stamp_to_definition id.stamp in + let var = Hashtbl.find definitions id' in + match var with + | Function _ -> () + | _ -> Hashtbl.remove definitions id'; + Hashtbl.remove stamp_to_definition id.stamp + with Not_found -> () + +let remove_unused_function id = + try + let id' = Hashtbl.find stamp_to_definition id.stamp in Hashtbl.remove definitions id'; Hashtbl.remove stamp_to_definition id.stamp with Not_found -> () diff --git a/debug/DebugInit.ml b/debug/DebugInit.ml index 455112ed..17a90536 100644 --- a/debug/DebugInit.ml +++ b/debug/DebugInit.ml @@ -45,6 +45,7 @@ let default_debug = compute_gnu_file_enum = DebugInformation.compute_gnu_file_enum; exists_section = DebugInformation.exists_section; remove_unused = DebugInformation.remove_unused; + remove_unused_function = DebugInformation.remove_unused_function; variable_printed = DebugInformation.variable_printed; add_diab_info = (fun _ _ _ _ -> ()); } diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml index 7469c4af..ef44a2d5 100644 --- a/debug/DwarfPrinter.ml +++ b/debug/DwarfPrinter.ml @@ -658,6 +658,7 @@ module DwarfPrinter(Target: DWARF_TARGET): print_label oc line_start; list_opt s (fun () -> section oc Section_debug_str; + let s = List.sort (fun (a,_) (b,_) -> Pervasives.compare a b) s in List.iter (fun (id,s) -> print_label oc (loc_to_label id); fprintf oc " .asciz \"%s\"\n" s) s) diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 6c2cc661..b67fd638 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -16,9 +16,7 @@ let prepro_options = ref ([]: string list) let linker_options = ref ([]: string list) let assembler_options = ref ([]: string list) let option_flongdouble = ref false -let option_fstruct_return = ref false -let option_fstruct_return_style = ref Configuration.struct_return_style -let option_fstruct_passing_style = ref Configuration.struct_passing_style +let option_fstruct_passing = ref false let option_fbitfields = ref false let option_fvararg_calls = ref true let option_funprototyped = ref true diff --git a/driver/Driver.ml b/driver/Driver.ml index c9c16eac..db3031b4 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -120,7 +120,7 @@ let parse_c_file sourcename ifile = (* Simplification options *) let simplifs = "b" (* blocks: mandatory *) - ^ (if !option_fstruct_return then "s" else "") + ^ (if !option_fstruct_passing then "s" else "") ^ (if !option_fbitfields then "f" else "") ^ (if !option_fpacked_structs then "p" else "") in @@ -425,11 +425,9 @@ Preprocessing options: Language support options (use -fno-<opt> to turn off -f<opt>) : -fbitfields Emulate bit fields in structs [off] -flongdouble Treat 'long double' as 'double' [off] - -fstruct-return Emulate returning structs and unions by value [off] - -fstruct-return=<convention> - Set the calling conventions used to return structs by value - -fstruct-passing=<convention> - Set the calling conventions used to pass structs by value + -fstruct-passing Support passing structs and unions by value as function + results or function arguments [off] + -fstruct-return Like -fstruct-passing (deprecated) -fvararg-calls Support calls to variable-argument functions [on] -funprototyped Support calls to old-style functions without prototypes [on] -fpacked-structs Emulate packed structs [off] @@ -502,7 +500,7 @@ let print_version_and_exit _ = let language_support_options = [ option_fbitfields; option_flongdouble; - option_fstruct_return; option_fvararg_calls; option_funprototyped; + option_fstruct_passing; option_fvararg_calls; option_funprototyped; option_fpacked_structs; option_finline_asm ] @@ -612,33 +610,13 @@ let cmdline_actions = Exact "-quiet", Self (fun _ -> Interp.trace := 0); Exact "-trace", Self (fun _ -> Interp.trace := 2); Exact "-random", Self (fun _ -> Interp.mode := Interp.Random); - Exact "-all", Self (fun _ -> Interp.mode := Interp.All); -(* Special -f options *) - Exact "-fstruct-passing=ref-callee", - Self (fun _ -> option_fstruct_passing_style := Configuration.SP_ref_callee); - Exact "-fstruct-passing=ref-caller", - Self (fun _ -> option_fstruct_return := true; - option_fstruct_passing_style := Configuration.SP_ref_caller); - Exact "-fstruct-passing=ints", - Self (fun _ -> option_fstruct_return := true; - option_fstruct_passing_style := Configuration.SP_split_args); - Exact "-fstruct-return=ref", - Self (fun _ -> option_fstruct_return := true; - option_fstruct_return_style := Configuration.SR_ref); - Exact "-fstruct-return=int1248", - Self (fun _ -> option_fstruct_return := true; - option_fstruct_return_style := Configuration.SR_int1248); - Exact "-fstruct-return=int1-4", - Self (fun _ -> option_fstruct_return := true; - option_fstruct_return_style := Configuration.SR_int1to4); - Exact "-fstruct-return=int1-8", - Self (fun _ -> option_fstruct_return := true; - option_fstruct_return_style := Configuration.SR_int1to8) + Exact "-all", Self (fun _ -> Interp.mode := Interp.All) ] (* -f options: come in -f and -fno- variants *) (* Language support options *) @ f_opt "longdouble" option_flongdouble - @ f_opt "struct-return" option_fstruct_return + @ f_opt "struct-return" option_fstruct_passing + @ f_opt "struct-passing" option_fstruct_passing @ f_opt "bitfields" option_fbitfields @ f_opt "vararg-calls" option_fvararg_calls @ f_opt "unprototyped" option_funprototyped diff --git a/ia32/Asmexpand.ml b/ia32/Asmexpand.ml index dcea9de4..d7b554dc 100644 --- a/ia32/Asmexpand.ml +++ b/ia32/Asmexpand.ml @@ -343,6 +343,9 @@ let expand_builtin_inline name args res = (* Synchronization *) | "__builtin_membar", [], _ -> () + (* no operation *) + | "__builtin_nop", [], _ -> + emit (Pxchg_rr (EAX,EAX)) (* Catch-all *) | _ -> raise (Error ("unrecognized builtin " ^ name)) diff --git a/ia32/CBuiltins.ml b/ia32/CBuiltins.ml index 125e71d5..771d2786 100644 --- a/ia32/CBuiltins.ml +++ b/ia32/CBuiltins.ml @@ -65,6 +65,9 @@ let builtins = { (TVoid [], [TPtr(TInt(IUShort, []), []); TInt(IUShort, [])], false); "__builtin_write32_reversed", (TVoid [], [TPtr(TInt(IUInt, []), []); TInt(IUInt, [])], false); + (* no operation *) + "__builtin_nop", + (TVoid [], [], false); ] } diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index 4c436c45..f12843d2 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -759,7 +759,7 @@ module Target(System: SYSTEM):TARGET = need_masks := false; if !Clflags.option_g then begin section oc Section_text; - fprintf oc " .cfi_sections .debug_frame\n" + if Configuration.system <> "bsd" then cfi_section oc end let print_epilogue oc = diff --git a/lib/Readconfig.mll b/lib/Readconfig.mll index ec2f6bb0..6cb3409d 100644 --- a/lib/Readconfig.mll +++ b/lib/Readconfig.mll @@ -82,7 +82,7 @@ and doublequote = parse (* The entry point *) let read_config_file filename = - let ic = open_in filename in + let ic = open_in_bin filename in let lexbuf = Lexing.from_channel ic in Lexing.(lexbuf.lex_start_p <- {lexbuf.lex_start_p with pos_fname = filename}); try @@ -108,4 +108,3 @@ let _ = *) } - diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 228977c2..a9b60fbd 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -259,6 +259,7 @@ Inductive instruction : Type := | Pori: ireg -> ireg -> constant -> instruction (**r or with immediate *) | Poris: ireg -> ireg -> constant -> instruction (**r or with immediate high *) | Prldicl: ireg -> ireg -> int -> int -> instruction (**r rotate and mask left (PPC64) *) + | Prldicr: ireg -> ireg -> int -> int -> instruction (**r rotate and mask right (PPC64) *) | Prlwinm: ireg -> ireg -> int -> int -> instruction (**r rotate and mask *) | Prlwimi: ireg -> ireg -> int -> int -> instruction (**r rotate and insert *) | Pslw: ireg -> ireg -> ireg -> instruction (**r shift left *) @@ -267,7 +268,7 @@ Inductive instruction : Type := | Psrw: ireg -> ireg -> ireg -> instruction (**r shift right unsigned *) | Pstb: ireg -> constant -> ireg -> instruction (**r store 8-bit int *) | Pstbx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) - | Pstdu: ireg -> constant -> ireg -> instruction (**r store 64-bit integer with update (PPC64) *) + | Pstdu: ireg -> constant -> ireg -> instruction (**r store 64-bit integer with update (PPC64) *) | Pstfd: freg -> constant -> ireg -> instruction (**r store 64-bit float *) | Pstfdu: freg -> constant -> ireg -> instruction (**r store 64-bit float with update *) | Pstfdx: freg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) @@ -925,6 +926,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pmfspr _ _ | Pmtspr _ _ | Prldicl _ _ _ _ + | Prldicr _ _ _ _ | Pstdu _ _ _ | Pstwbrx _ _ _ | Pstwcx_ _ _ _ diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 02d2dc84..42ad4f97 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -287,6 +287,7 @@ let p_instruction oc ic = | Pori (ir1,ir2,c) -> instruction "Pori" [Ireg ir1; Ireg ir2; Constant c] | Poris (ir1,ir2,c) -> instruction "Poris" [Ireg ir1; Ireg ir2; Constant c] | Prldicl (ir1,ir2,ic1,ic2) -> instruction "Prldicl" [Ireg ir1; Ireg ir2; Constant (Cint ic1); Constant (Cint ic2)] + | Prldicr (ir1,ir2,ic1,ic2) -> instruction "Prldicr" [Ireg ir1; Ireg ir2; Constant (Cint ic1); Constant (Cint ic2)] | Prlwinm (ir1,ir2,ic1,ic2) -> instruction "Prlwinm" [Ireg ir1; Ireg ir2; Constant (Cint ic1); Constant (Cint ic2)] | Prlwimi (ir1,ir2,ic1,ic2) ->instruction "Prlwimi" [Ireg ir1; Ireg ir2; Constant (Cint ic1); Constant (Cint ic2)] | Pslw (ir1,ir2,ir3) -> instruction "Pslw" [Ireg ir1; Ireg ir2; Ireg ir3] diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 35aa02d5..ca166fd1 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -38,6 +38,8 @@ let _2 = coqint_of_camlint 2l let _4 = coqint_of_camlint 4l let _6 = coqint_of_camlint 6l let _8 = coqint_of_camlint 8l +let _31 = coqint_of_camlint 31l +let _32 = coqint_of_camlint 32l let _m4 = coqint_of_camlint (-4l) let _m8 = coqint_of_camlint (-8l) @@ -334,6 +336,19 @@ let expand_builtin_va_start r = let expand_int64_arith conflict rl fn = if conflict then (fn GPR0; emit (Pmr(rl, GPR0))) else fn rl +(* Convert integer constant into GPR with corresponding number *) +let int_to_int_reg = function + | 0 -> Some GPR0 | 1 -> Some GPR1 | 2 -> Some GPR2 | 3 -> Some GPR3 + | 4 -> Some GPR4 | 5 -> Some GPR5 | 6 -> Some GPR6 | 7 -> Some GPR7 + | 8 -> Some GPR8 | 9 -> Some GPR9 | 10 -> Some GPR10 | 11 -> Some GPR11 + | 12 -> Some GPR12 | 13 -> Some GPR13 | 14 -> Some GPR14 | 15 -> Some GPR15 + | 16 -> Some GPR16 | 17 -> Some GPR17 | 18 -> Some GPR18 | 19 -> Some GPR19 + | 20 -> Some GPR20 | 21 -> Some GPR21 | 22 -> Some GPR22 | 23 -> Some GPR23 + | 24 -> Some GPR24 | 25 -> Some GPR25 | 26 -> Some GPR26 | 27 -> Some GPR27 + | 28 -> Some GPR28 | 29 -> Some GPR29 | 30 -> Some GPR30 | 31 -> Some GPR31 + | _ -> None + + (* Handling of compiler-inlined builtins *) let expand_builtin_inline name args res = @@ -344,8 +359,18 @@ let expand_builtin_inline name args res = emit (Pmulhw(res, a1, a2)) | "__builtin_mulhwu", [BA(IR a1); BA(IR a2)], BR(IR res) -> emit (Pmulhwu(res, a1, a2)) - | "__builtin_clz", [BA(IR a1)], BR(IR res) -> + | ("__builtin_clz" | "__builtin_clzl"), [BA(IR a1)], BR(IR res) -> emit (Pcntlzw(res, a1)) + | "__builtin_clzll", [BA_splitlong(BA(IR ah), BA(IR al))], BR(IR res) -> + let lbl = new_label () in + emit (Pcntlzw(res, ah)); + (* less than 32 bits zero? *) + emit (Pcmpwi (res, Cint _32)); + emit (Pbf (CRbit_2, lbl)); + (* high bits all zero, count bits in low word and increment by 32 *) + emit (Pcntlzw(res, al)); + emit (Paddi(res, res, Cint _32)); + emit (Plabel lbl) | "__builtin_cmpb", [BA(IR a1); BA(IR a2)], BR(IR res) -> emit (Pcmpb (res,a1,a2)) | ("__builtin_bswap" | "__builtin_bswap32"), [BA(IR a1)], BR(IR res) -> @@ -428,11 +453,11 @@ let expand_builtin_inline name args res = emit (Pisync) | "__builtin_lwsync", [], _ -> emit (Plwsync) - | "__builtin_mbar", [BA_int mo], _ -> + | "__builtin_mbar", [BA_int mo], _ -> if not (mo = _0 || mo = _1) then raise (Error "the argument of __builtin_mbar must be 0 or 1"); emit (Pmbar mo) - | "__builin_mbar",_, _ -> + | "__builin_mbar", _, _ -> raise (Error "the argument of __builtin_mbar must be a constant"); | "__builtin_trap", [], _ -> emit (Ptrap) @@ -480,6 +505,33 @@ let expand_builtin_inline name args res = emit (Pmtspr(n, a1)) | "__builtin_set_spr", _, _ -> raise (Error "the first argument of __builtin_set_spr must be a constant") + (* Special registers in 32bit hybrid mode *) + | "__builtin_get_spr64", [BA_int n], BR_splitlong(BR(IR rh), BR(IR rl)) -> + if Archi.ppc64 then begin + emit (Pmfspr(rl, n)); + emit (Prldicl(rh, rl, _32, _32)); + emit (Prldicl(rl, rl, _0, _32)) + end else + raise (Error "__builtin_get_spr64 is only supported for PPC64 targets") + | "__builtin_get_spr64", _, _ -> + raise (Error "the argument of __builtin_get_spr64 must be a constant") + | "__builtin_set_spr64", [BA_int n; BA_splitlong(BA(IR ah), BA(IR al))], _ -> + if Archi.ppc64 then begin + emit (Prldicr(GPR10, ah, _32, _31)); + emit (Prldicl(al, al, _0, _32)); + emit (Por(GPR10, GPR10, al)); + emit (Pmtspr(n, GPR10)) + end else + raise (Error "__builtin_set_spr64 is only supported for PPC64 targets") + | "__builtin_set_spr64", _, _ -> + raise (Error "the first argument of __builtin_set_spr64 must be a constant") + (* Move registers *) + | "__builtin_mr", [BA_int dst; BA_int src], _ -> + (match int_to_int_reg (Z.to_int dst), int_to_int_reg (Z.to_int src) with + | Some dst, Some src -> emit (Pori (dst, src, Cint _0)) + | _, _ -> raise (Error "the arguments of __builtin_mr must be in the range of 0..31")) + | "__builtin_mr", _, _ -> + raise (Error "the arguments of __builtin_mr must be constants") (* Frame and return address *) | "__builtin_call_frame", _,BR (IR res) -> let sz = !current_function_stacksize @@ -490,8 +542,8 @@ let expand_builtin_inline name args res = emit (Plwz(res, Cint ofs, GPR1)) | "__builtin_return_address",_,BR (IR res) -> emit (Plwz (res, Cint! retaddr_offset,GPR1)) - (* isel *) - | "__builtin_isel", [BA (IR a1); BA (IR a2); BA (IR a3)],BR (IR res) -> + (* Integer selection *) + | ("__builtin_isel" | "__builtin_uisel"), [BA (IR a1); BA (IR a2); BA (IR a3)],BR (IR res) -> if eref then begin emit (Pcmpwi (a1,Cint (Int.zero))); emit (Pisel (res,a3,a2,CRbit_2)) @@ -510,6 +562,9 @@ let expand_builtin_inline name args res = end; emit (Por (res, res, GPR0)) end + (* no operation *) + | "__builtin_nop", [], _ -> + emit (Pori (GPR0, GPR0, Cint _0)) (* atomic operations *) | "__builtin_atomic_exchange", [BA (IR a1); BA (IR a2); BA (IR a3)],_ -> emit (Plwz (GPR10,Cint _0,a2)); @@ -632,7 +687,7 @@ let expand_instruction instr = emit (Pcfi_adjust _m8) | Pfcfiu(r1, r2) -> assert (Archi.ppc64); - emit (Prldicl(GPR0, r2, _0, coqint_of_camlint 32l)); + emit (Prldicl(GPR0, r2, _0, _32)); emit (Pstdu(GPR0, Cint _m8, GPR1)); emit (Pcfi_adjust _8); emit (Plfd(r1, Cint _0, GPR1)); @@ -686,6 +741,7 @@ let expand_instruction instr = | _ -> emit instr + (* Translate to the integer identifier of the register as the EABI specifies *) diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index 106ba4d0..ec3a633b 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -30,6 +30,10 @@ let builtins = { (TInt(IUInt, []), [TInt(IUInt, []); TInt(IUInt, [])], false); "__builtin_clz", (TInt(IUInt, []), [TInt(IUInt, [])], false); + "__builtin_clzl", + (TInt(IUInt, []), [TInt(IULong, [])], false); + "__builtin_clzll", + (TInt(IUInt, []), [TInt(IULongLong, [])], false); "__builtin_bswap", (TInt(IUInt, []), [TInt(IUInt, [])], false); "__builtin_bswap32", @@ -91,7 +95,7 @@ let builtins = { (TVoid [], [TInt(IInt, [])], false); "__builtin_trap", (TVoid [], [], false); - (* Cache isntructions *) + (* Cache instructions *) "__builtin_dcbf", (TVoid [],[TPtr(TVoid [], [])],false); "__builtin_dcbi", @@ -111,6 +115,14 @@ let builtins = { (TInt(IUInt, []), [TInt(IInt, [])], false); "__builtin_set_spr", (TVoid [], [TInt(IInt, []); TInt(IUInt, [])], false); + (* Access to special registers in 32bit hybrid mode*) + "__builtin_get_spr64", + (TInt(IULongLong, []), [TInt(IInt, [])], false); + "__builtin_set_spr64", + (TVoid [], [TInt(IInt, []); TInt(IULongLong, [])], false); + (* Move register *) + "__builtin_mr", + (TVoid [], [TInt(IInt, []); TInt(IInt, [])], false); (* Frame and return address *) "__builtin_call_frame", (TPtr (TVoid [],[]),[],false); @@ -119,6 +131,12 @@ let builtins = { (* isel *) "__builtin_isel", (TInt (IInt, []),[TInt(IBool, []);TInt(IInt, []);TInt(IInt, [])],false); + (* uisel *) + "__builtin_uisel", + (TInt (IUInt, []),[TInt(IBool, []);TInt(IUInt, []);TInt(IUInt, [])],false); + (* no operation *) + "__builtin_nop", + (TVoid [], [], false); (* atomic operations *) "__builtin_atomic_exchange", (TVoid [], [TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[])],false); diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index fe209627..4ee6493c 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -163,7 +163,8 @@ Fixpoint destroyed_by_clobber (cl: list string): list mreg := Definition destroyed_by_builtin (ef: external_function): list mreg := match ef with | EF_builtin id sg => - if string_dec id "__builtin_atomic_exchange" then R10::nil + if string_dec id "__builtin_set_spr64" then R10::nil + else if string_dec id "__builtin_atomic_exchange" then R10::nil else if string_dec id "__builtin_atomic_compare_exchange" then R10::R11::nil else F13 :: nil | EF_vload _ => R11 :: nil @@ -220,11 +221,14 @@ Definition builtin_constraints (ef: external_function) : match ef with | EF_builtin id sg => if string_dec id "__builtin_get_spr" then OK_const :: nil + else if string_dec id "__builtin_get_spr64" then OK_const :: nil else if string_dec id "__builtin_set_spr" then OK_const :: OK_default :: nil + else if string_dec id "__builtin_set_spr64" then OK_const :: OK_default :: nil else if string_dec id "__builtin_prefetch" then OK_default :: OK_const :: OK_const :: nil - else if string_dec id "__builtin_dcbtls" then OK_default::OK_const::nil - else if string_dec id "__builtin_icbtls" then OK_default::OK_const::nil - else if string_dec id "__builtin_mbar" then OK_const::nil + else if string_dec id "__builtin_dcbtls" then OK_default :: OK_const :: nil + else if string_dec id "__builtin_icbtls" then OK_default :: OK_const :: nil + else if string_dec id "__builtin_mbar" then OK_const :: nil + else if string_dec id "__builtin_mr" then OK_const :: OK_const :: nil else nil | EF_vload _ => OK_addrany :: nil | EF_vstore _ => OK_addrany :: OK_default :: nil diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 73cb12f5..3d183972 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -151,9 +151,9 @@ module Linux_System : SYSTEM = let print_prologue oc = if !Clflags.option_g then begin - section oc Section_text; - fprintf oc " .cfi_sections .debug_frame\n" - end + section oc Section_text; + cfi_section oc + end let print_epilogue oc = if !Clflags.option_g then @@ -647,6 +647,9 @@ module Target (System : SYSTEM):TARGET = | Prldicl(r1, r2, c1, c2) -> fprintf oc " rldicl %a, %a, %ld, %ld\n" ireg r1 ireg r2 (camlint_of_coqint c1) (camlint_of_coqint c2) + | Prldicr(r1, r2, c1, c2) -> + fprintf oc " rldicr %a, %a, %ld, %ld\n" + ireg r1 ireg r2 (camlint_of_coqint c1) (camlint_of_coqint c2) | Prlwinm(r1, r2, c1, c2) -> let (mb, me) = rolm_mask (camlint_of_coqint c2) in fprintf oc " rlwinm %a, %a, %ld, %d, %d %s 0x%lx\n" @@ -789,7 +792,7 @@ module Target (System : SYSTEM):TARGET = let nlo = Int64.to_int32 n and nhi = Int64.to_int32(Int64.shift_right_logical n 32) in fprintf oc "%a: .long 0x%lx, 0x%lx\n" label lbl nhi nlo - + let print_literal32 oc (lbl, n) = fprintf oc "%a: .long 0x%lx\n" label lbl n diff --git a/runtime/arm/sysdeps.h b/runtime/arm/sysdeps.h index 85404cf7..3d6a702c 100644 --- a/runtime/arm/sysdeps.h +++ b/runtime/arm/sysdeps.h @@ -17,7 +17,7 @@ // * Neither the name of the <organization> nor the // names of its contributors may be used to endorse or promote products // derived from this software without specific prior written permission. -// +// // THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS // "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT // LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR @@ -34,7 +34,7 @@ // System dependencies -#if defined(MODEL_armv7r) +#if defined(MODEL_armv7m) // Thumb2-only #define THUMB #else diff --git a/runtime/include/stddef.h b/runtime/include/stddef.h index 31edf4ef..f61e87b4 100644 --- a/runtime/include/stddef.h +++ b/runtime/include/stddef.h @@ -13,7 +13,7 @@ * * Neither the name of the <organization> nor the * names of its contributors may be used to endorse or promote products * derived from this software without specific prior written permission. - * + * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR @@ -90,6 +90,18 @@ typedef signed int wchar_t; #endif #endif +#if defined (__need_wint_t) +#ifndef _WINT_T +#define _WINT_T + +#ifndef __WINT_TYPE__ +#define __WINT_TYPE__ unsigned int +#endif +typedef __WINT_TYPE__ wint_t; +#endif +#undef __need_wint_t +#endif + #if defined(_STDDEF_H) || defined(__need_NULL) #ifndef NULL #define NULL 0 @@ -102,4 +114,3 @@ typedef signed int wchar_t; #endif #endif - |