diff options
| -rw-r--r-- | backend/Inliningaux.ml | 9 | ||||
| -rw-r--r-- | cfrontend/C2C.ml | 28 | ||||
| -rw-r--r-- | cparser/Elab.ml | 1 | ||||
| -rw-r--r-- | lib/JsonAST.ml | 2 |
4 files changed, 27 insertions, 13 deletions
diff --git a/backend/Inliningaux.ml b/backend/Inliningaux.ml index 164773ae..842e0c93 100644 --- a/backend/Inliningaux.ml +++ b/backend/Inliningaux.ml @@ -86,7 +86,10 @@ let static_called_once id io = (* To be considered: heuristics based on size of function? *) let should_inline (io: inlining_info) (id: ident) (f: coq_function) = - if !Clflags.option_finline then - C2C.atom_is_inline id || static_called_once id io - else + if !Clflags.option_finline then begin + match C2C.atom_inline id with + | C2C.Inline -> true + | C2C.Noinline -> false + | C2C.No_specifier -> static_called_once id io + end else false diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 4c75c2f2..173764e3 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -26,13 +26,18 @@ open Csyntax (** Record useful information about global variables and functions, and associate it with the corresponding atoms. *) +type inline_status = + | No_specifier (* No inline specifier and no noinline attribute *) + | Noinline (* The atom is declared with the noinline attribute *) + | Inline (* The atom is declared inline *) + type atom_info = { 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_access: Sections.access_mode; (* access mode, e.g. small data area *) - a_inline: bool; (* function declared inline? *) + a_inline: inline_status; (* function declared inline? *) a_loc: location (* source location *) } @@ -74,11 +79,11 @@ let atom_is_rel_data a ofs = with Not_found -> false -let atom_is_inline a = +let atom_inline a = try (Hashtbl.find decl_atom a).a_inline with Not_found -> - false + No_specifier (** Iso C99 defines inline definitions of functions as functions with inline specifier and without extern. These functions do @@ -89,7 +94,7 @@ let atom_is_iso_inline_definition a = try let i = Hashtbl.find decl_atom a in match i.a_storage with - | C.Storage_default -> i.a_inline + | C.Storage_default -> i.a_inline = Inline | _ -> false with Not_found -> false @@ -325,7 +330,7 @@ let name_for_string_literal s = a_alignment = Some 1; a_sections = [Sections.for_stringlit()]; a_access = Sections.Access_default; - a_inline = false; + a_inline = No_specifier; a_loc = Cutil.no_loc }; Hashtbl.add stringTable s id; id @@ -355,7 +360,7 @@ let name_for_wide_string_literal s = a_alignment = Some Machine.((!config).sizeof_wchar); a_sections = [Sections.for_stringlit()]; a_access = Sections.Access_default; - a_inline = false; + a_inline = No_specifier; a_loc = Cutil.no_loc }; Hashtbl.add wstringTable s id; id @@ -1148,13 +1153,20 @@ let convertFundef loc env fd = fd.fd_locals in let body' = convertStmt env fd.fd_body in let id' = intern_string fd.fd_name.name in + let noinline = Cutil.find_custom_attributes ["noinline";"__noinline__"] fd.fd_attrib <> [] in + let inline = if noinline || fd.fd_vararg then (* PR#15 *) + Noinline + else if fd.fd_inline then + Inline + else + No_specifier in Debug.atom_global fd.fd_name id'; Hashtbl.add decl_atom id' { a_storage = fd.fd_storage; a_alignment = None; a_sections = Sections.for_function env id' fd.fd_attrib; a_access = Sections.Access_default; - a_inline = fd.fd_inline && not fd.fd_vararg; (* PR#15 *) + a_inline = inline; a_loc = loc }; (id', AST.Gfun(Ctypes.Internal {fn_return = ret; @@ -1240,7 +1252,7 @@ let convertGlobvar loc env (sto, id, ty, optinit) = a_alignment = Some (Z.to_int al); a_sections = [section]; a_access = access; - a_inline = false; + a_inline = No_specifier; a_loc = loc }; let volatile = List.mem C.AVolatile attr in let readonly = List.mem C.AConst attr && not volatile in diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 60772eec..e846e301 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -2365,7 +2365,6 @@ let elab_fundef env spec name defs body loc = && can_return then warning loc Invalid_noreturn "function '%s' declared 'noreturn' should not return" s; (* Build and emit function definition *) - let inline = inline && find_custom_attributes ["noinline";"__noinline__"] attr = [] in let fn = { fd_storage = sto1; fd_inline = inline; diff --git a/lib/JsonAST.ml b/lib/JsonAST.ml index f3dd2dc6..73cac31e 100644 --- a/lib/JsonAST.ml +++ b/lib/JsonAST.ml @@ -59,7 +59,7 @@ let pp_int_opt pp = function let pp_fundef pp_inst pp (name,fn) = let alignment = atom_alignof name - and inline = atom_is_inline name + and inline = atom_inline name = Inline and static = atom_is_static name and c_section,l_section,j_section = match (atom_sections name) with [a;b;c] -> a,b,c | _ -> assert false in pp_jobject_start pp; |