diff --git a/cfrontend/Cil2Csyntax.ml b/cfrontend/Cil2Csyntax.ml
index e5690aac3b85e08c6045ae46aa8c0f565f367b14..822f6cb045e41b5bc7e07d5a944b64ab5daa8787 100644
--- a/cfrontend/Cil2Csyntax.ml
+++ b/cfrontend/Cil2Csyntax.ml
@@ -201,11 +201,12 @@ and eval_cast ty v =
| TPtr(_, _), CWStr s -> v (* tolerance? *)
| _, _ -> raise NotConst
-(** Handler for #pragma directives --
- overriden in machine-dependent CPragmas module *)
-
-let process_pragma = ref (fun (a: Cil.attribute) -> false)
+(** Hooks -- overriden in machine-dependent CPragmas module *)
+let process_pragma_hook = ref (fun (a: Cil.attribute) -> false)
+let define_variable_hook = ref (fun (id: ident) (v: Cil.varinfo) -> ())
+let define_function_hook = ref (fun (id: ident) (v: Cil.varinfo) -> ())
+let define_stringlit_hook = ref (fun (id: ident) (v: Cil.varinfo) -> ())
(** The parameter to the translation functor: it specifies the
translation for integer and float types. *)
@@ -296,6 +297,7 @@ let name_for_string_literal s =
v.vstorage <- Static;
v.vreferenced <- true;
Hashtbl.add varinfo_atom id v;
+ !define_stringlit_hook id v;
Hashtbl.add stringTable s id;
id
@@ -1012,6 +1014,7 @@ let convertGFun fdec =
current_function := None;
let id = intern_string v.vname in
Hashtbl.add varinfo_atom id v;
+ !define_function_hook id v;
Datatypes.Coq_pair
(id,
Internal { fn_return=ret; fn_params=args; fn_vars=varList; fn_body=s })
@@ -1144,6 +1147,7 @@ let convertGVar v i =
updateLoc(v.vdecl);
let id = intern_string v.vname in
Hashtbl.add varinfo_atom id v;
+ !define_variable_hook id v;
Datatypes.Coq_pair (Datatypes.Coq_pair(id, convertInitInfo v.vtype i),
convertTyp v.vtype)
@@ -1214,7 +1218,7 @@ let rec processGlobals = function
unsupported "inline assembly"
| GPragma (Attr(name, _) as attr, loc) ->
updateLoc(loc);
- if not (!process_pragma attr) then
+ if not (!process_pragma_hook attr) then
warning ("#pragma `" ^ name ^ "' directive ignored");
processGlobals l
| GText _ -> processGlobals l (* comments are ignored *)
@@ -1264,16 +1268,16 @@ let atom_is_static a =
with Not_found ->
false
+let var_is_readonly v =
+ let a = typeAttrs v.vtype in
+ if hasAttribute "volatile" a then false else
+ if hasAttribute "const" a then true else
+ match Cil.unrollType v.vtype with
+ | TArray(ty, _, _) ->
+ let a' = typeAttrs ty in
+ hasAttribute "const" a' && not (hasAttribute "volatile" a')
+ | _ -> false
+
let atom_is_readonly a =
- try
- let v = Hashtbl.find varinfo_atom a in
- let a = typeAttrs v.vtype in
- if hasAttribute "volatile" a then false else
- if hasAttribute "const" a then true else
- match Cil.unrollType v.vtype with
- | TArray(ty, _, _) ->
- let a' = typeAttrs ty in
- hasAttribute "const" a' && not (hasAttribute "volatile" a')
- | _ -> false
- with Not_found ->
- false
+ try var_is_readonly (Hashtbl.find varinfo_atom a)
+ with Not_found -> false
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index c6f6e8fe2820347c326e39975b8f89933ac0da3a..ddcfaac43a994492f985faf4c7fd775ce5b7ef7f 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -24,3 +24,9 @@ let option_E = ref false
let option_S = ref false
let option_c = ref false
let option_v = ref false
+let option_small_data =
+ ref (if Configuration.arch = "powerpc"
+ && Configuration.variant = "eabi"
+ && Configuration.system = "diab"
+ then 8 else 0)
+let option_small_const = ref (!option_small_data)
diff --git a/driver/Driver.ml b/driver/Driver.ml
index b818680481f4bdfe74aebdd4f796c84125297189..aed0221919eeec6ed0bce785c6f879f78c56cf46 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -247,10 +247,6 @@ let process_cminor_file sourcename =
(* Command-line parsing *)
-let starts_with s1 s2 =
- String.length s1 >= String.length s2 &&
- String.sub s1 0 (String.length s2) = s2
-
let usage_string =
"ccomp [options] <source files>
Recognized source files:
@@ -269,6 +265,8 @@ Preprocessing options:
Compilation options:
-flonglong Treat 'long long' as 'long' and 'long double' as 'double'
-fmadd Use fused multiply-add and multiply-sub instructions
+ -fsmall-data <n> Set maximal size <n> for allocation in small data area
+ -fsmall-const <n> Set maximal size <n> for allocation in small constant area
-dcil Save CIL-processed source in <file>.cil.c
-dclight Save generated Clight in <file>.light.c
-dasm Save generated assembly in <file>.s
@@ -281,86 +279,88 @@ General options:
-v Print external commands before invoking them
"
-let rec parse_cmdline i =
- if i < Array.length Sys.argv then begin
- let s = Sys.argv.(i) in
- if starts_with s "-I" || starts_with s "-D" || starts_with s "-U"
- then begin
- prepro_options := s :: !prepro_options;
- parse_cmdline (i + 1)
- end else
- if starts_with s "-l" || starts_with s "-L" then begin
- linker_options := s :: !linker_options;
- parse_cmdline (i + 1)
- end else
- if s = "-o" && i + 1 < Array.length Sys.argv then begin
- exe_name := Sys.argv.(i + 1);
- parse_cmdline (i + 2)
- end else
- if s = "-stdlib" && i + 1 < Array.length Sys.argv then begin
- stdlib_path := Sys.argv.(i + 1);
- parse_cmdline (i + 2)
- end else
- if s = "-flonglong" then begin
- option_flonglong := true;
- parse_cmdline (i + 1)
- end else
- if s = "-fmadd" then begin
- option_fmadd := true;
- parse_cmdline (i + 1)
- end else
- if s = "-dcil" then begin
- option_dcil := true;
- parse_cmdline (i + 1)
- end else
- if s = "-dclight" then begin
- option_dclight := true;
- parse_cmdline (i + 1)
- end else
- if s = "-dasm" then begin
- option_dasm := true;
- parse_cmdline (i + 1)
- end else
- if s = "-E" then begin
- option_E := true;
- parse_cmdline (i + 1)
- end else
- if s = "-S" then begin
- option_S := true;
- parse_cmdline (i + 1)
- end else
- if s = "-c" then begin
- option_c := true;
- parse_cmdline (i + 1)
- end else
- if s = "-v" then begin
- option_v := true;
- parse_cmdline (i + 1)
- end else
- if Filename.check_suffix s ".c" then begin
+type action =
+ | Set of bool ref
+ | Self of (string -> unit)
+ | String of (string -> unit)
+ | Integer of (int -> unit)
+
+let rec find_action s = function
+ | [] -> None
+ | (re, act) :: rem ->
+ if Str.string_match re s 0 then Some act else find_action s rem
+
+let parse_cmdline spec usage =
+ let acts = List.map (fun (pat, act) -> (Str.regexp pat, act)) spec in
+ let error () =
+ eprintf "Usage: %s" usage;
+ exit 2 in
+ let rec parse i =
+ if i < Array.length Sys.argv then begin
+ let s = Sys.argv.(i) in
+ match find_action s acts with
+ | None ->
+ if s <> "-help" && s <> "--help"
+ then eprintf "Unknown argument `%s'\n" s;
+ error ()
+ | Some(Set r) ->
+ r := true; parse (i+1)
+ | Some(Self fn) ->
+ fn s; parse (i+1)
+ | Some(String fn) ->
+ if i + 1 < Array.length Sys.argv then begin
+ fn Sys.argv.(i+1); parse (i+2)
+ end else begin
+ eprintf "Option `%s' expects an argument\n" s; error()
+ end
+ | Some(Integer fn) ->
+ if i + 1 < Array.length Sys.argv then begin
+ let n =
+ try
+ int_of_string Sys.argv.(i+1)
+ with Failure _ ->
+ eprintf "Argument to option `%s' must be an integer\n" s;
+ error()
+ in
+ fn n; parse (i+2)
+ end else begin
+ eprintf "Option `%s' expects an argument\n" s; error()
+ end
+ end
+ in parse 1
+
+let cmdline_actions = [
+ "-[IDU].", Self(fun s -> prepro_options := s :: !prepro_options);
+ "-[lL].", Self(fun s -> linker_options := s :: !linker_options);
+ "-o$", String(fun s -> exe_name := s);
+ "-stdlib$", String(fun s -> stdlib_path := s);
+ "-flonglong$", Set option_flonglong;
+ "-fmadd$", Set option_fmadd;
+ "-fsmall-data$", Integer(fun n -> option_small_data := n);
+ "-fsmall-const$", Integer(fun n -> option_small_const := n);
+ "-dcil$", Set option_dcil;
+ "-dclight$", Set option_dclight;
+ "-dasm$", Set option_dasm;
+ "-E$", Set option_E;
+ "-S$", Set option_S;
+ "-c$", Set option_c;
+ "-v$", Set option_v;
+ ".*\\.c$", Self (fun s ->
let objfile = process_c_file s in
- linker_options := objfile :: !linker_options;
- parse_cmdline (i + 1)
- end else
- if Filename.check_suffix s ".cm" then begin
+ linker_options := objfile :: !linker_options);
+ ".*\\.cm$", Self (fun s ->
let objfile = process_cminor_file s in
- linker_options := objfile :: !linker_options;
- parse_cmdline (i + 1)
- end else
- if Filename.check_suffix s ".o" || Filename.check_suffix s ".a" then begin
- linker_options := s :: !linker_options;
- parse_cmdline (i + 1)
- end else begin
- eprintf "Unknown argument `%s'\n" s;
- eprintf "Usage: %s" usage_string;
- exit 2
- end
- end
+ linker_options := objfile :: !linker_options);
+ ".*\\.[oa]$", Self (fun s ->
+ linker_options := s :: !linker_options)
+]
let _ =
Cil.initCIL();
CPragmas.initialize();
- parse_cmdline 1;
- if not (!option_c || !option_S || !option_E) then begin
+ parse_cmdline cmdline_actions usage_string;
+ if !linker_options <> []
+ && not (!option_c || !option_S || !option_E)
+ then begin
linker !exe_name !linker_options
end
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index d9c6531472afa601a92f50bb5bd7e9856dcd03c3..50a847442daa5f77253b3aa719a344c98055d785 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -175,26 +175,23 @@ let section oc name =
(* Names of sections *)
-let (text, data, const_data, sdata, float_literal) =
+let (text, data, const_data, float_literal) =
match target with
| MacOS ->
(".text",
".data",
".const",
- ".data", (* unused *)
".const_data")
| Linux ->
(".text",
".data",
".rodata",
- ".data", (* unused *)
".section .rodata.cst8,\"aM\",@progbits,8")
| Diab ->
(".text",
".data",
- ".data", (* or: .rodata? *)
- ".sdata", (* to check *)
- ".data") (* or: .rodata? *)
+ ".text",
+ ".text")
(* Encoding masks for rlwinm instructions *)
@@ -496,7 +493,7 @@ let print_function oc name code =
Hashtbl.clear current_function_labels;
section oc
(match CPragmas.section_for_atom name true with
- | Some s -> ".section\t" ^ s
+ | Some s -> s
| None -> text);
fprintf oc " .align 2\n";
if not (Cil2Csyntax.atom_is_static name) then
@@ -713,14 +710,11 @@ let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) =
match init_data with [Init_space _] -> false | _ -> true in
let sec =
match CPragmas.section_for_atom name init with
- | Some s -> ".section\t" ^ s
+ | Some s -> s
| None ->
- if CPragmas.atom_is_small_data name (coqint_of_camlint 0l) then
- sdata
- else if Cil2Csyntax.atom_is_readonly name then
- const_data
- else
- data
+ if Cil2Csyntax.atom_is_readonly name
+ then const_data
+ else data
in
section oc sec;
fprintf oc " .align 3\n";
diff --git a/powerpc/eabi/CPragmas.ml b/powerpc/eabi/CPragmas.ml
index 9d2eb8a4b953427b9808f08050d11f23c4a4bdae..d4b79b5257e95e8d8fc6e7ad6cb76cdff19c38f6 100644
--- a/powerpc/eabi/CPragmas.ml
+++ b/powerpc/eabi/CPragmas.ml
@@ -22,31 +22,72 @@ open Camlcoq
type section_info = {
sec_name_init: string;
sec_name_uninit: string;
+ sec_acc_mode: string;
sec_near_access: bool
}
+let default_section_info = {
+ sec_name_init = ".data";
+ sec_name_uninit = ".data"; (* COMM? *)
+ sec_acc_mode = "RW";
+ sec_near_access = false
+}
+
let section_table : (string, section_info) Hashtbl.t =
Hashtbl.create 17
-let use_section_table : (AST.ident, section_info) Hashtbl.t =
- Hashtbl.create 51
+(* Built-in sections *)
+
+let _ =
+ let rodata =
+ if Configuration.system = "linux" then ".rodata" else ".text" in
+ List.iter (fun (n, si) -> Hashtbl.add section_table n si) [
+ "CODE", {sec_name_init = ".text";
+ sec_name_uninit = ".text";
+ sec_acc_mode = "RX";
+ sec_near_access = false};
+ "DATA", {sec_name_init = ".data";
+ sec_name_uninit = ".data"; (* COMM? *)
+ sec_acc_mode = "RW";
+ sec_near_access = false};
+ "SDATA", {sec_name_init = ".sdata";
+ sec_name_uninit = ".sbss";
+ sec_acc_mode = "RW";
+ sec_near_access = true};
+ "CONST", {sec_name_init = rodata;
+ sec_name_uninit = rodata;
+ sec_acc_mode = "R";
+ sec_near_access = false};
+ "SCONST",{sec_name_init = ".sdata2";
+ sec_name_uninit = ".sdata2";
+ sec_acc_mode = "R";
+ sec_near_access = true};
+ "STRING",{sec_name_init = rodata;
+ sec_name_uninit = rodata;
+ sec_acc_mode = "R";
+ sec_near_access = false}
+ ]
let process_section_pragma classname istring ustring addrmode accmode =
- let is_near = (addrmode = "near-absolute") || (addrmode = "near-data") in
- let is_writable = String.contains accmode 'W'
- and is_executable = String.contains accmode 'X' in
- let sec_type =
- match is_writable, is_executable with
- | true, true -> 'm' (* text+data *)
- | true, false -> 'd' (* data *)
- | false, true -> 'c' (* text *)
- | false, false -> 'r' (* const *)
- in
- let info =
- { sec_name_init = sprintf "%s,,%c" istring sec_type;
- sec_name_uninit = sprintf "%s,,%c" ustring sec_type;
- sec_near_access = is_near } in
- Hashtbl.add section_table classname info
+ let old_si =
+ try Hashtbl.find section_table classname
+ with Not_found -> default_section_info in
+ let si =
+ { sec_name_init =
+ if istring = "" then old_si.sec_name_init else istring;
+ sec_name_uninit =
+ if ustring = "" then old_si.sec_name_uninit else ustring;
+ sec_acc_mode =
+ if accmode = "" then old_si.sec_acc_mode else accmode;
+ sec_near_access =
+ if addrmode = ""
+ then old_si.sec_near_access
+ else (addrmode = "near-code") || (addrmode = "near-data") } in
+ Hashtbl.add section_table classname si
+
+
+let use_section_table : (AST.ident, section_info) Hashtbl.t =
+ Hashtbl.create 51
let process_use_section_pragma classname id =
try
@@ -55,18 +96,42 @@ let process_use_section_pragma classname id =
with Not_found ->
Cil2Csyntax.error (sprintf "unknown section name `%s'" classname)
+let default_use_section id classname =
+ if not (Hashtbl.mem use_section_table id) then begin
+ let info =
+ try Hashtbl.find section_table classname
+ with Not_found -> assert false in
+ Hashtbl.add use_section_table id info
+ end
+
+let define_function id v =
+ default_use_section id "CODE"
+
+let define_stringlit id v =
+ default_use_section id "STRING"
+
+let define_variable id v =
+ let sz = Cil.bitsSizeOf v.vtype / 8 in
+ let sect =
+ if Cil2Csyntax.var_is_readonly v then
+ if sz <= !Clflags.option_small_const then "SCONST" else "CONST"
+ else
+ if sz <= !Clflags.option_small_data then "SDATA" else "DATA" in
+ default_use_section id sect
+
(* CIL does not parse the "section" and "use_section" pragmas, which
have irregular syntax, so we parse them using regexps *)
let re_start_pragma_section = Str.regexp "section\\b"
-let re_pragma_section = Str.regexp
- "section[ \t]+\
- \\([A-Za-z_][A-Za-z_0-9]*\\)[ \t]+\
- \"\\([^\"]*\\)\"[ \t]+\
- \"\\([^\"]*\\)\"[ \t]+\
- \\([a-z-]+\\)[ \t]+\
- \\([A-Z]+\\)"
+let re_pragma_section = Str.regexp(
+ "section[ \t]+"
+^ "\\([A-Za-z_][A-Za-z_0-9]*\\)[ \t]+" (* class_name *)
+^ "\\(\"[^\"]*\"\\)?[ \t]*" (* istring *)
+^ "\\(\"[^\"]*\"\\)?[ \t]*" (* ustring *)
+^ "\\(standard\\|near-absolute\\|far-absolute\\|near-data\\|far-data\\|near-code\\|far-code\\)?[ \t]*" (* addressing mode *)
+^ "\\([RWXON]*\\)" (* access mode *)
+)
let re_start_pragma_use_section = Str.regexp "use_section\\b"
@@ -101,34 +166,51 @@ let process_pragma (Attr(name, _)) =
false
let initialize () =
- Cil2Csyntax.process_pragma := process_pragma
+ Cil2Csyntax.process_pragma_hook := process_pragma;
+ Cil2Csyntax.define_variable_hook := define_variable;
+ Cil2Csyntax.define_function_hook := define_function;
+ Cil2Csyntax.define_stringlit_hook := define_stringlit
(* PowerPC-specific: say if an atom is in a small data area *)
let atom_is_small_data a ofs =
- match Configuration.system with
- | "diab" ->
- begin try
- let v = Hashtbl.find Cil2Csyntax.varinfo_atom a in
- let sz = Cil.bitsSizeOf v.vtype / 8 in
- let ofs = camlint_of_coqint ofs in
- if ofs >= 0l && ofs < Int32.of_int sz then begin
- try (Hashtbl.find use_section_table a).sec_near_access
- with Not_found -> sz <= 8
- end else
- false
+ begin try
+ let v = Hashtbl.find Cil2Csyntax.varinfo_atom a in
+ let sz = Cil.bitsSizeOf v.vtype / 8 in
+ let ofs = camlint_of_coqint ofs in
+ if ofs >= 0l && ofs < Int32.of_int sz then begin
+ try
+ (Hashtbl.find use_section_table a).sec_near_access
with Not_found ->
- false
- end
- | _ ->
+ if Cil2Csyntax.var_is_readonly v
+ then sz <= !Clflags.option_small_const
+ else sz <= !Clflags.option_small_data
+ end else
false
+ with Not_found ->
+ false
+ end
(* PowerPC-specific: determine section to use for a particular symbol *)
let section_for_atom a init =
try
let sinfo = Hashtbl.find use_section_table a in
- Some(if init then sinfo.sec_name_init else sinfo.sec_name_uninit)
- with Not_found ->
- None
-
+ let sname =
+ if init then sinfo.sec_name_init else sinfo.sec_name_uninit in
+ if not (String.contains sname '\"') then
+ Some sname
+ else begin
+ (* The following is Diab-specific... *)
+ let accmode = sinfo.sec_acc_mode in
+ let is_writable = String.contains accmode 'W'
+ and is_executable = String.contains accmode 'X' in
+ let stype =
+ match is_writable, is_executable with
+ | true, true -> 'm' (* text+data *)
+ | true, false -> 'd' (* data *)
+ | false, true -> 'c' (* text *)
+ | false, false -> 'r' (* const *)
+ in Some(sprintf ".section\t%s,,%c" sname stype)
+ end
+ with Not_found -> None