diff options
| -rw-r--r-- | Changelog | 35 | ||||
| -rw-r--r-- | arm/PrintAsm.ml | 11 | ||||
| -rw-r--r-- | cfrontend/C2C.ml | 129 | ||||
| -rw-r--r-- | common/Sections.ml | 181 | ||||
| -rw-r--r-- | common/Sections.mli | 12 | ||||
| -rw-r--r-- | ia32/PrintAsm.ml | 18 | ||||
| -rw-r--r-- | powerpc/PrintAsm.ml | 13 | ||||
| -rw-r--r-- | powerpc/extractionMachdep.v | 2 | ||||
| -rw-r--r-- | test/regression/pragmas.c | 1 |
9 files changed, 191 insertions, 211 deletions
@@ -1,3 +1,38 @@ +Release 1.10, 2012-02-15 +======================== + +Improvements in confidence: +- CompCert C now natively supports volatile types. Its semantics fully + specifies the meaning of volatile memory accesses. The translation + of volatile accesses to built-in function invocations is now proved correct. +- CompCert C now natively supports assignment between composite types + (structs or unions), passing composite types by value as function + parameters, and other instances of composites used as r-values, with + the exception of returning composites by value from a function. + (The latter remains emulated, using the -fstruct-return option.) + +Language features: +- Support for _Bool type from ISO C99. + +Performance improvements: +- Improvements in instruction selection, especially for integer casts + and their combinations with bitwise operations. +- Shorter, more efficient code generated for accessing volatile global + variables. +- Better code generated for && and || outside conditional tests. +- Improved register allocation for invocations of built-ins, + especially for annotations. +- In Cminor and down, make safe operators non-strict: they return Vundef + instead of getting stuck. This enables more optimizations. +- Cast optimization is no longer performed by a separate pass over + RTL, but equivalent optimization is done during Cminor generation + and during instruction selection. + +Other improvements: +- PowerPC/EABI: uninitialized global variables now go in common (bss) section. +- PowerPC: work around limited excursion of conditional branch instructions. + + Release 1.9.1, 2011-11-28 ========================= diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index a616cc2..634faae 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -677,7 +677,10 @@ let print_function oc name fn = Hashtbl.clear current_function_labels; reset_constants(); currpos := 0; - let (text, _, _) = sections_for_function name in + let text = + match C2C.atom_sections name with + | t :: _ -> t + | _ -> Section_text in section oc text; fprintf oc " .align 2\n"; if not (C2C.atom_is_static name) then @@ -733,10 +736,10 @@ let print_var oc (name, v) = match v.gvar_init with | [] -> () | _ -> - let init = - match v.gvar_init with [Init_space _] -> false | _ -> true in let sec = - Sections.section_for_variable name init + match C2C.atom_sections name with + | [s] -> s + | _ -> Section_data true and align = match C2C.atom_alignof name with | Some a -> log2 a diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 9703e0b..d7f4aff 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -28,14 +28,17 @@ open Values open Csyntax open Initializers -(** Record the declarations of global variables and associate them - with the corresponding atom. *) +(** Record useful information about global variables and functions, + and associate it with the corresponding atoms. *) type atom_info = - { a_storage: C.storage; - a_env: Env.t; - a_type: C.typ; - a_fundef: C.fundef option } + { a_storage: C.storage; (* storage class *) + a_alignment: int option; (* alignment *) + a_sections: Sections.section_name list; (* in which section to put it *) + (* 1 section for data, 3 sections (code/lit/jumptbl) for functions *) + a_small_data: bool; (* data in a small data area? *) + a_inline: bool (* function declared inline? *) +} let decl_atom : (AST.ident, atom_info) Hashtbl.t = Hashtbl.create 103 @@ -104,13 +107,12 @@ let name_for_string_literal env s = incr stringNum; let name = Printf.sprintf "__stringlit_%d" !stringNum in let id = intern_string name in - let sz = Int64.of_int (String.length s + 1) in Hashtbl.add decl_atom id { a_storage = C.Storage_static; - a_env = env; - a_type = C.TArray(C.TInt(C.IChar,[C.AConst]), Some sz, []); - a_fundef = None }; - Sections.define_stringlit id; + a_alignment = Some 1; + a_sections = [Sections.for_stringlit()]; + a_small_data = false; + a_inline = false }; Hashtbl.add stringTable s id; id @@ -329,46 +331,6 @@ let first_class_value env ty = | C.TInt((C.ILongLong|C.IULongLong), _) -> false | _ -> true -(************ REMOVED - -(* Handling of volatile *) - -let is_volatile_access env e = - List.mem C.AVolatile (Cutil.attributes_of_type env e.etyp) - && Cutil.is_lvalue e - && begin match Cutil.unroll env e.etyp with - | TFun _ | TArray _ -> false - | _ -> true - end - -let volatile_kind ty = - match ty with - | Tint(I8, Unsigned) -> ("int8unsigned", ty, Mint8unsigned) - | Tint(I8, Signed) -> ("int8signed", ty, Mint8signed) - | Tint(I16, Unsigned) -> ("int16unsigned", ty, Mint16unsigned) - | Tint(I16, Signed) -> ("int16signed", ty, Mint16signed) - | Tint(I32, _) -> ("int32", Tint(I32, Signed), Mint32) - | Tfloat F32 -> ("float32", ty, Mfloat32) - | Tfloat F64 -> ("float64", ty, Mfloat64) - | Tpointer _ -> ("pointer", Tpointer Tvoid, Mint32) - | _ -> - unsupported "operation on volatile struct or union"; ("", Tvoid, Mint32) - -let volatile_read_fun ty = - let (suffix, ty', chunk) = volatile_kind ty in - let targs = Tcons(Tpointer Tvoid, Tnil) in - let name = "__builtin_volatile_read_" ^ suffix in - register_special_external name (EF_vload chunk) targs ty'; - Evalof(Evar(intern_string name, Tfunction(targs, ty')), Tfunction(targs, ty')) - -let volatile_write_fun ty = - let (suffix, ty', chunk) = volatile_kind ty in - let targs = Tcons(Tpointer Tvoid, Tcons(ty', Tnil)) in - let name = "__builtin_volatile_write_" ^ suffix in - register_special_external name (EF_vstore chunk) targs Tvoid; - Evalof(Evar(intern_string name, Tfunction(targs, Tvoid)), Tfunction(targs, Tvoid)) -****************************) - (** Expressions *) let ezero = Eval(Vint(coqint_of_camlint 0l), type_int32s) @@ -692,10 +654,10 @@ let convertFundef env fd = let id' = intern_string fd.fd_name.name in Hashtbl.add decl_atom id' { a_storage = fd.fd_storage; - a_env = env; - a_type = Cutil.fundef_typ fd; - a_fundef = Some fd }; - Sections.define_function env id' fd.fd_ret; + a_alignment = None; + a_sections = Sections.for_function env id' fd.fd_ret; + a_small_data = false; + a_inline = fd.fd_inline }; (id', Internal {fn_return = ret; fn_params = params; fn_vars = vars; fn_body = body'}) @@ -753,21 +715,27 @@ let convertInitializer env ty i = let convertGlobvar env (sto, id, ty, optinit) = let id' = intern_string id.name in let ty' = convertTyp env ty in + let attr = Cutil.attributes_of_type env ty in let init' = match optinit with | None -> if sto = C.Storage_extern then [] else [Init_space(Csyntax.sizeof ty')] | Some i -> convertInitializer env ty i in + let align = + match Cutil.find_custom_attributes ["aligned"; "__aligned__"] attr with + | [[C.AInt n]] -> Some(Int64.to_int n) + | _ -> Cutil.alignof env ty in + let (section, near_access) = + Sections.for_variable env id' ty (optinit <> None) in Hashtbl.add decl_atom id' { a_storage = sto; - a_env = env; - a_type = ty; - a_fundef = None }; - Sections.define_variable env id' ty; - let a = Cutil.attributes_of_type env ty in - let volatile = List.mem C.AVolatile a in - let readonly = List.mem C.AConst a && not volatile in + a_alignment = align; + a_sections = [section]; + a_small_data = near_access; + a_inline = false }; + let volatile = List.mem C.AVolatile attr in + let readonly = List.mem C.AConst attr && not volatile in (id', {gvar_info = ty'; gvar_init = init'; gvar_readonly = readonly; gvar_volatile = volatile}) @@ -880,42 +848,33 @@ let convertProgram p = let atom_is_static a = try - match Hashtbl.find decl_atom a with - | { a_storage = C.Storage_static } -> true - (* We do not inline functions, but at least let's not make them globals *) - | { a_fundef = Some { fd_inline = true } } -> true - | _ -> false + let i = Hashtbl.find decl_atom a in + i.a_storage = C.Storage_static || i.a_inline + (* inline functions can remain in generated code, but at least + let's not make them global *) with Not_found -> false let atom_is_extern a = try - let i = Hashtbl.find decl_atom a in i.a_storage = C.Storage_extern + (Hashtbl.find decl_atom a).a_storage = C.Storage_extern with Not_found -> false -(* -let atom_is_readonly a = +let atom_alignof a = try - let i = Hashtbl.find decl_atom a in type_is_readonly i.a_env i.a_type + (Hashtbl.find decl_atom a).a_alignment with Not_found -> - false + None -let atom_sizeof a = +let atom_sections a = try - let i = Hashtbl.find decl_atom a in Cutil.sizeof i.a_env i.a_type + (Hashtbl.find decl_atom a).a_sections with Not_found -> - None -*) + [] -let atom_alignof a = +let atom_is_small_data a ofs = try - let i = Hashtbl.find decl_atom a in - match Cutil.find_custom_attributes - ["aligned"; "__aligned__"] - (Cutil.attributes_of_type i.a_env i.a_type) with - | [[C.AInt n]] -> Some(Int64.to_int n) - | _ -> Cutil.alignof i.a_env i.a_type + (Hashtbl.find decl_atom a).a_small_data with Not_found -> - None - + false diff --git a/common/Sections.ml b/common/Sections.ml index f37144a..3ee36e8 100644 --- a/common/Sections.ml +++ b/common/Sections.ml @@ -16,8 +16,6 @@ open Camlcoq open Cparser -module StringMap = Map.Make(String) - (* Handling of linker sections *) type section_name = @@ -92,40 +90,28 @@ let builtin_sections = [ sec_near_access = false} ] -let default_section_table = - List.fold_right - (fun (s, i) t -> StringMap.add s i t) - builtin_sections StringMap.empty - - (* The current mapping from section names to section info *) -let current_section_table : (section_info StringMap.t) ref = - ref StringMap.empty +let current_section_table : (string, section_info) Hashtbl.t = + Hashtbl.create 17 -(* The section to use for each global symbol: either explicitly - assigned using a "use_section" pragma, or inferred at definition - time. *) +(* The section assigned to a global symbol using a "use_section" pragma *) let use_section_table : (AST.ident, section_info) Hashtbl.t = Hashtbl.create 51 -(* For each global symbol, the mapping sect name -> sect info - current at the time it was defined *) - -let section_table_at_def : (AST.ident, section_info StringMap.t) Hashtbl.t = - Hashtbl.create 51 - let initialize () = - current_section_table := default_section_table; - Hashtbl.clear use_section_table; - Hashtbl.clear section_table_at_def + Hashtbl.clear current_section_table; + List.iter + (fun (s, i) -> Hashtbl.add current_section_table s i) + builtin_sections; + Hashtbl.clear use_section_table (* Define or update a given section. *) let define_section name ?iname ?uname ?writable ?executable ?near () = let si = - try StringMap.find name !current_section_table + try Hashtbl.find current_section_table name with Not_found -> default_section_info in let writable = match writable with Some b -> b | None -> si.sec_writable @@ -145,98 +131,91 @@ let define_section name ?iname ?uname ?writable ?executable ?near () = sec_writable = writable; sec_executable = executable; sec_near_access = near } in - current_section_table := StringMap.add name new_si !current_section_table + Hashtbl.replace current_section_table name new_si (* Explicitly associate a section to a global symbol *) let use_section_for id name = try - let si = StringMap.find name !current_section_table in + let si = Hashtbl.find current_section_table name in Hashtbl.add use_section_table id si; true with Not_found -> false -(* Default association of a section to a global symbol *) - -let default_use_section id name = - Hashtbl.add section_table_at_def id !current_section_table; - if not (Hashtbl.mem use_section_table id) then begin - let ok = use_section_for id name in - assert ok - end +(* Undeclared section attached to a global variable, GCC-style *) -(* Associate an undeclared section to a global symbol, GCC-style *) - -let use_gcc_section id name readonly exec = - Hashtbl.add section_table_at_def id !current_section_table; +let gcc_section name readonly exec = let sn = Section_user(name, not readonly, exec) in - let si = { sec_name_init = sn; sec_name_uninit = sn; - sec_writable = not readonly; sec_executable = exec; - sec_near_access = false } in - Hashtbl.add use_section_table id si + { sec_name_init = sn; sec_name_uninit = sn; + sec_writable = not readonly; sec_executable = exec; + sec_near_access = false } -(* Record sections for a variable definition *) +(* Determine section for a variable definition *) -let define_variable env id ty = +let for_variable env id ty init = let attr = Cutil.attributes_of_type env ty in let readonly = List.mem C.AConst attr && not(List.mem C.AVolatile attr) in - (* Check for a GCC-style "section" attribute *) - match Cutil.find_custom_attributes ["section"; "__section__"] attr with - | [[C.AString name]] -> - (* Use gcc-style section *) - use_gcc_section id name readonly false - | _ -> - (* Use default section appropriate for size and const-ness *) - let size = match Cutil.sizeof env ty with Some sz -> sz | None -> max_int in - default_use_section id - (if readonly - then if size <= !Clflags.option_small_const then "SCONST" else "CONST" - else if size <= !Clflags.option_small_data then "SDATA" else "DATA") - -(* Record sections for a function definition *) - -let define_function env id ty_res = + let si = + try + (* 1- Section explicitly associated with #use_section *) + Hashtbl.find use_section_table id + with Not_found -> + match Cutil.find_custom_attributes ["section"; "__section__"] attr with + | [[C.AString name]] -> + (* 2- Section given as an attribute, gcc-style *) + gcc_section name readonly false + | _ -> + (* 3- Default section appropriate for size and const-ness *) + let size = + match Cutil.sizeof env ty with Some sz -> sz | None -> max_int in + let name = + if readonly + then if size <= !Clflags.option_small_const then "SCONST" else "CONST" + else if size <= !Clflags.option_small_data then "SDATA" else "DATA" in + try + Hashtbl.find current_section_table name + with Not_found -> + assert false in + ((if init then si.sec_name_init else si.sec_name_uninit), si.sec_near_access) + +(* Determine sections for a function definition *) + +let for_function env id ty_res = let attr = Cutil.attributes_of_type env ty_res in - match Cutil.find_custom_attributes ["section"; "__section__"] attr with - | [[C.AString name]] -> - use_gcc_section id name true true - | _ -> - default_use_section id "CODE" - -(* Record sections for a string literal *) - -let define_stringlit id = - default_use_section id "STRING" - -(* Determine section to use for a variable *) - -let section_for_variable a initialized = - try - let si = Hashtbl.find use_section_table a in - if initialized then si.sec_name_init else si.sec_name_uninit - with Not_found -> - Section_data initialized - -(* Determine (text, literal, jumptable) sections to use for a function *) - -let sections_for_function a = - let s_text = - try (Hashtbl.find use_section_table a).sec_name_init - with Not_found -> Section_text in - let s_table = - try Hashtbl.find section_table_at_def a - with Not_found -> default_section_table in - let s_literal = - try (StringMap.find "LITERAL" s_table).sec_name_init - with Not_found -> Section_literal in - let s_jumptable = - try (StringMap.find "JUMPTABLE" s_table).sec_name_init - with Not_found -> Section_jumptable in - (s_text, s_literal, s_jumptable) - -(* Say if an atom is in a small data area *) - -let atom_is_small_data a ofs = - try (Hashtbl.find use_section_table a).sec_near_access - with Not_found -> false + let si_code = + try + (* 1- Section explicitly associated with #use_section *) + Hashtbl.find use_section_table id + with Not_found -> + match Cutil.find_custom_attributes ["section"; "__section__"] attr with + | [[C.AString name]] -> + (* 2- Section given as an attribute, gcc-style *) + gcc_section name true true + | _ -> + (* 3- Default section *) + try + Hashtbl.find current_section_table "CODE" + with Not_found -> + assert false in + let si_literal = + try + Hashtbl.find current_section_table "LITERAL" + with Not_found -> + assert false in + let si_jumptbl = + try + Hashtbl.find current_section_table "JUMPTABLE" + with Not_found -> + assert false in + [si_code.sec_name_init; si_literal.sec_name_init; si_jumptbl.sec_name_init] + +(* Determine section for a string literal *) + +let for_stringlit() = + let si = + try + Hashtbl.find current_section_table "STRING" + with Not_found -> + assert false in + si.sec_name_init diff --git a/common/Sections.mli b/common/Sections.mli index c6a7c96..a487f34 100644 --- a/common/Sections.mli +++ b/common/Sections.mli @@ -34,10 +34,8 @@ val define_section: -> ?writable:bool -> ?executable:bool -> ?near:bool -> unit -> unit val use_section_for: AST.ident -> string -> bool -val define_function: Cparser.Env.t -> AST.ident -> Cparser.C.typ -> unit -val define_variable: Cparser.Env.t -> AST.ident -> Cparser.C.typ -> unit -val define_stringlit: AST.ident -> unit - -val section_for_variable: AST.ident -> bool -> section_name -val sections_for_function: AST.ident -> section_name * section_name * section_name -val atom_is_small_data: AST.ident -> Integers.Int.int -> bool +val for_variable: Cparser.Env.t -> AST.ident -> Cparser.C.typ -> bool -> + section_name * bool +val for_function: Cparser.Env.t -> AST.ident -> Cparser.C.typ -> + section_name list +val for_stringlit: unit -> section_name diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 3ee0c6e..e9a44eb 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -139,9 +139,6 @@ let name_of_neg_condition = function | Cond_l -> "ge" | Cond_le -> "g" | Cond_ge -> "l" | Cond_g -> "le" | Cond_p -> "np" | Cond_np -> "p" -let section oc name = - fprintf oc " %s\n" name - (* Names of sections *) let name_of_section_ELF = function @@ -174,7 +171,9 @@ let name_of_section_Cygwin = function | Section_string -> ".section .rdata,\"dr\"" | Section_literal -> ".section .rdata,\"dr\"" | Section_jumptable -> ".text" - | Section_user _ -> assert false + | Section_user(s, wr, ex) -> + sprintf ".section %s, \"%s\"\n" + s (if ex then "xr" else if wr then "d" else "dr") let name_of_section = match target with @@ -743,7 +742,10 @@ let print_function oc name code = Hashtbl.clear current_function_labels; float_literals := []; jumptables := []; - let (text, lit, jmptbl) = sections_for_function name in + let (text, lit, jmptbl) = + match C2C.atom_sections name with + | [t;l;j] -> (t, l, j) + | _ -> (Section_text, Section_literal, Section_jumptable) in section oc text; print_align oc 16; if not (C2C.atom_is_static name) then @@ -802,10 +804,10 @@ let print_var oc (name, v) = match v.gvar_init with | [] -> () | _ -> - let init = - match v.gvar_init with [Init_space _] -> false | _ -> true in let sec = - Sections.section_for_variable name init + match C2C.atom_sections name with + | [s] -> s + | _ -> Section_data true and align = match C2C.atom_alignof name with | Some a -> a diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index ff7957d..f396a23 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -870,7 +870,10 @@ let print_function oc name code = Hashtbl.clear current_function_labels; float_literals := []; jumptables := []; - let (text, lit, jmptbl) = sections_for_function name in + let (text, lit, jmptbl) = + match C2C.atom_sections name with + | [t;l;j] -> (t, l, j) + | _ -> (Section_text, Section_literal, Section_jumptable) in section oc text; fprintf oc " .align 2\n"; if not (C2C.atom_is_static name) then @@ -1093,11 +1096,11 @@ let print_var oc (name, v) = match v.gvar_init with | [] -> () | _ -> - let init = - match v.gvar_init with [Init_space _] -> false | _ -> true in let sec = - Sections.section_for_variable name init in - let align = + match C2C.atom_sections name with + | [s] -> s + | _ -> Section_data true + and align = match C2C.atom_alignof name with | Some a -> log2 a | None -> 3 in (* 8-alignment is a safe default *) diff --git a/powerpc/extractionMachdep.v b/powerpc/extractionMachdep.v index a315e8f..cb4c3c2 100644 --- a/powerpc/extractionMachdep.v +++ b/powerpc/extractionMachdep.v @@ -18,7 +18,7 @@ Extract Constant SelectOp.use_fused_mul => "(fun () -> !Clflags.option_fmadd)". (* Asm *) Extract Constant Asm.low_half => "fun _ -> assert false". Extract Constant Asm.high_half => "fun _ -> assert false". -Extract Constant Asm.symbol_is_small_data => "Sections.atom_is_small_data". +Extract Constant Asm.symbol_is_small_data => "C2C.atom_is_small_data". Extract Constant Asm.small_data_area_offset => "fun _ _ _ -> assert false". (* Suppression of stupidly big equality functions *) diff --git a/test/regression/pragmas.c b/test/regression/pragmas.c index 36361cd..bc47dbb 100644 --- a/test/regression/pragmas.c +++ b/test/regression/pragmas.c @@ -45,6 +45,7 @@ const char t[5][5] = { 1, 2, 3 }; double h(int n) { + w[0] --; w[n] ++; return v; } |