Skip to content
Snippets Groups Projects
Commit 913c1bcc authored by xleroy's avatar xleroy
Browse files

Cleaned up handling of linker sections. 

Minor updates on ARM code generator.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1339 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
parent 9f04b743
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
arm/PrintAsm.ml
+ 17
− 11
View file @ 913c1bcc
...@@ -237,12 +237,13 @@ let print_builtin_function oc s = ...@@ -237,12 +237,13 @@ let print_builtin_function oc s =
let lbl1 = new_label() in let lbl1 = new_label() in
let lbl2 = new_label() in let lbl2 = new_label() in
fprintf oc " cmp %a, #0\n" ireg IR2; fprintf oc " cmp %a, #0\n" ireg IR2;
fprintf oc " beq %a\n" label lbl1; fprintf oc " beq .L%d\n" lbl1;
fprintf oc "%a: ldrb %a, [%a], #1\n" label lbl2 ireg IR3 ireg IR1; fprintf oc ".L%d: ldrb %a, [%a], #1\n" lbl2 ireg IR3 ireg IR1;
fprintf oc " subs %a, %a, #1\n" ireg IR2 ireg IR2; fprintf oc " subs %a, %a, #1\n" ireg IR2 ireg IR2;
fprintf oc " strb %a, [%a], #1\n" ireg IR3 ireg IR0; fprintf oc " strb %a, [%a], #1\n" ireg IR3 ireg IR0;
fprintf oc " bne %a\n" label lbl2; fprintf oc " bne .L%d\n" lbl2;
fprintf oc "%a:\n" label lbl1 fprintf oc ".L%d:\n" lbl1;
7
(* (*
let lbl = new_label() in let lbl = new_label() in
fprintf oc " cmp %a, #0\n" ireg IR2; fprintf oc " cmp %a, #0\n" ireg IR2;
...@@ -255,12 +256,13 @@ let print_builtin_function oc s = ...@@ -255,12 +256,13 @@ let print_builtin_function oc s =
let lbl1 = new_label() in let lbl1 = new_label() in
let lbl2 = new_label() in let lbl2 = new_label() in
fprintf oc " movs %a, %a, lsr #2\n" ireg IR2 ireg IR2; fprintf oc " movs %a, %a, lsr #2\n" ireg IR2 ireg IR2;
fprintf oc " beq %a\n" label lbl1; fprintf oc " beq .L%d\n" lbl1;
fprintf oc "%a: ldr %a, [%a], #4\n" label lbl2 ireg IR3 ireg IR1; fprintf oc ".L%d: ldr %a, [%a], #4\n" lbl2 ireg IR3 ireg IR1;
fprintf oc " subs %a, %a, #1\n" ireg IR2 ireg IR2; fprintf oc " subs %a, %a, #1\n" ireg IR2 ireg IR2;
fprintf oc " str %a, [%a], #4\n" ireg IR3 ireg IR0; fprintf oc " str %a, [%a], #4\n" ireg IR3 ireg IR0;
fprintf oc " bne %a\n" label lbl2; fprintf oc " bne .L%d\n" lbl2;
fprintf oc "%a:\n" label lbl1 fprintf oc ".L%d:\n" lbl1;
7
(* Catch-all *) (* Catch-all *)
| s -> | s ->
invalid_arg ("unrecognized builtin function " ^ s) invalid_arg ("unrecognized builtin function " ^ s)
...@@ -496,7 +498,8 @@ let print_function oc name code = ...@@ -496,7 +498,8 @@ let print_function oc name code =
currpos := 0; currpos := 0;
fprintf oc " .text\n"; fprintf oc " .text\n";
fprintf oc " .align 2\n"; fprintf oc " .align 2\n";
fprintf oc " .global %a\n" print_symb name; if not (C2Clight.atom_is_static name) then
fprintf oc " .global %a\n" print_symb name;
fprintf oc " .type %a, %%function\n" print_symb name; fprintf oc " .type %a, %%function\n" print_symb name;
fprintf oc "%a:\n" print_symb name; fprintf oc "%a:\n" print_symb name;
print_instructions oc (labels_of_code Labelset.empty code) code; print_instructions oc (labels_of_code Labelset.empty code) code;
...@@ -584,9 +587,12 @@ let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) = ...@@ -584,9 +587,12 @@ let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) =
match init_data with match init_data with
| [] -> () | [] -> ()
| _ -> | _ ->
fprintf oc " .data\n"; if C2Clight.atom_is_readonly name
then fprintf oc " .const\n"
else fprintf oc " .data\n";
fprintf oc " .align 2\n"; fprintf oc " .align 2\n";
fprintf oc " .global %a\n" print_symb name; if not (C2Clight.atom_is_static name) then
fprintf oc " .global %a\n" print_symb name;
fprintf oc " .type %a, %%object\n" print_symb name; fprintf oc " .type %a, %%object\n" print_symb name;
fprintf oc "%a:\n" print_symb name; fprintf oc "%a:\n" print_symb name;
print_init_data oc name init_data print_init_data oc name init_data
......
cfrontend/C2Clight.ml
+ 13
− 14
View file @ 913c1bcc
...@@ -16,9 +16,6 @@ let decl_atom : (AST.ident, Env.t * C.decl) Hashtbl.t = Hashtbl.create 103 ...@@ -16,9 +16,6 @@ let decl_atom : (AST.ident, Env.t * C.decl) Hashtbl.t = Hashtbl.create 103
(** Hooks -- overriden in machine-dependent CPragmas module *) (** Hooks -- overriden in machine-dependent CPragmas module *)
let process_pragma_hook = ref (fun (s: string) -> false) let process_pragma_hook = ref (fun (s: string) -> false)
let define_variable_hook = ref (fun (id: ident) (d: C.decl) -> ())
let define_function_hook = ref (fun (id: ident) (d: C.decl) -> ())
let define_stringlit_hook = ref (fun (id: ident) -> ())
(** ** Error handling *) (** ** Error handling *)
...@@ -57,7 +54,7 @@ let name_for_string_literal env s = ...@@ -57,7 +54,7 @@ let name_for_string_literal env s =
Env.fresh_ident name, Env.fresh_ident name,
C.TPtr(C.TInt(C.IChar,[C.AConst]),[]), C.TPtr(C.TInt(C.IChar,[C.AConst]),[]),
None)); None));
!define_stringlit_hook id; Sections.define_stringlit id;
Hashtbl.add stringTable s id; Hashtbl.add stringTable s id;
id id
...@@ -529,7 +526,7 @@ let convertFundef env fd = ...@@ -529,7 +526,7 @@ let convertFundef env fd =
let decl = let decl =
(fd.fd_storage, fd.fd_name, Cutil.fundef_typ fd, None) in (fd.fd_storage, fd.fd_name, Cutil.fundef_typ fd, None) in
Hashtbl.add decl_atom id' (env, decl); Hashtbl.add decl_atom id' (env, decl);
!define_function_hook id' decl; Sections.define_function id';
Datatypes.Coq_pair(id', Datatypes.Coq_pair(id',
Internal {fn_return = ret; fn_params = params; Internal {fn_return = ret; fn_params = params;
fn_vars = vars; fn_body = body'}) fn_vars = vars; fn_body = body'})
...@@ -649,6 +646,14 @@ let convertInit env ty init = ...@@ -649,6 +646,14 @@ let convertInit env ty init =
(** Global variable *) (** Global variable *)
let rec type_is_readonly env t =
let a = Cutil.attributes_of_type env t in
if List.mem C.AVolatile a then false else
if List.mem C.AConst a then true else
match Cutil.unroll env t with
| C.TArray(t', _, _) -> type_is_readonly env t'
| _ -> false
let convertGlobvar env (sto, id, ty, optinit as decl) = let convertGlobvar env (sto, id, ty, optinit as decl) =
let id' = intern_string id.name in let id' = intern_string id.name in
let ty' = convertTyp env ty in let ty' = convertTyp env ty in
...@@ -659,7 +664,9 @@ let convertGlobvar env (sto, id, ty, optinit as decl) = ...@@ -659,7 +664,9 @@ let convertGlobvar env (sto, id, ty, optinit as decl) =
| Some i -> | Some i ->
convertInit env ty i in convertInit env ty i in
Hashtbl.add decl_atom id' (env, decl); Hashtbl.add decl_atom id' (env, decl);
!define_variable_hook id' decl; Sections.define_variable id'
(match Cutil.sizeof env ty with Some sz -> sz | None -> max_int)
(type_is_readonly env ty);
Datatypes.Coq_pair(Datatypes.Coq_pair(id', init'), ty') Datatypes.Coq_pair(Datatypes.Coq_pair(id', init'), ty')
(** Convert a list of global declarations. (** Convert a list of global declarations.
...@@ -769,14 +776,6 @@ let convertProgram p = ...@@ -769,14 +776,6 @@ let convertProgram p =
(** ** Extracting information about global variables from their atom *) (** ** Extracting information about global variables from their atom *)
let rec type_is_readonly env t =
let a = Cutil.attributes_of_type env t in
if List.mem C.AVolatile a then false else
if List.mem C.AConst a then true else
match Cutil.unroll env t with
| C.TArray(t', _, _) -> type_is_readonly env t'
| _ -> false
let atom_is_static a = let atom_is_static a =
try try
let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in
......
common/Sections.ml 0 → 100644
+ 211
− 0
View file @ 913c1bcc
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU General Public License as published by *)
(* the Free Software Foundation, either version 2 of the License, or *)
(* (at your option) any later version. This file is also distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
open Camlcoq
module StringMap = Map.Make(String)
(* Handling of linker sections *)
type section_name =
| Section_text
| Section_data of bool (* true = init data, false = uninit data *)
| Section_small_data of bool
| Section_const
| Section_small_const
| Section_string
| Section_literal
| Section_jumptable
| Section_user of string * bool (*writable*) * bool (*executable*)
type section_info = {
sec_name_init: section_name;
sec_name_uninit: section_name;
sec_writable: bool;
sec_executable: bool;
sec_near_access: bool
}
let default_section_info = {
sec_name_init = Section_data true;
sec_name_uninit = Section_data false;
sec_writable = true;
sec_executable = false;
sec_near_access = false
}
(* Built-in sections *)
let builtin_sections = [
"CODE",
{sec_name_init = Section_text;
sec_name_uninit = Section_text;
sec_writable = false; sec_executable = true;
sec_near_access = false};
"DATA",
{sec_name_init = Section_data true;
sec_name_uninit = Section_data false;
sec_writable = true; sec_executable = false;
sec_near_access = false};
"SDATA",
{sec_name_init = Section_small_data true;
sec_name_uninit = Section_small_data false;
sec_writable = true; sec_executable = false;
sec_near_access = true};
"CONST",
{sec_name_init = Section_const;
sec_name_uninit = Section_const;
sec_writable = false; sec_executable = false;
sec_near_access = false};
"SCONST",
{sec_name_init = Section_small_const;
sec_name_uninit = Section_small_const;
sec_writable = false; sec_executable = false;
sec_near_access = true};
"STRING",
{sec_name_init = Section_string;
sec_name_uninit = Section_string;
sec_writable = false; sec_executable = false;
sec_near_access = false};
"LITERAL",
{sec_name_init = Section_literal;
sec_name_uninit = Section_literal;
sec_writable = false; sec_executable = false;
sec_near_access = false};
"JUMPTABLE",
{sec_name_init = Section_jumptable;
sec_name_uninit = Section_jumptable;
sec_writable = false; sec_executable = false;
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
(* The section to use for each global symbol: either explicitly
assigned using a "use_section" pragma, or inferred at definition
time. *)
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
(* Define or update a given section. *)
let define_section name ?iname ?uname ?writable ?executable ?near () =
let si =
try StringMap.find name !current_section_table
with Not_found -> default_section_info in
let writable =
match writable with Some b -> b | None -> si.sec_writable
and executable =
match executable with Some b -> b | None -> si.sec_executable
and near =
match near with Some b -> b | None -> si.sec_near_access in
let iname =
match iname with Some s -> Section_user(s, writable, executable)
| None -> si.sec_name_init in
let uname =
match uname with Some s -> Section_user(s, writable, executable)
| None -> si.sec_name_uninit in
let new_si =
{ sec_name_init = iname;
sec_name_uninit = uname;
sec_writable = writable;
sec_executable = executable;
sec_near_access = near } in
current_section_table := StringMap.add name new_si !current_section_table
(* Explicitly associate a section to a global symbol *)
let use_section_for id name =
try
let si = StringMap.find name !current_section_table 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
let define_function id =
default_use_section id "CODE"
let define_stringlit id =
default_use_section id "STRING"
let define_variable id size readonly =
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")
(* Determine section to use for a variable definition *)
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 definition *)
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
common/Sections.mli 0 → 100644
+ 43
− 0
View file @ 913c1bcc
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU General Public License as published by *)
(* the Free Software Foundation, either version 2 of the License, or *)
(* (at your option) any later version. This file is also distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
(* Handling of linker sections *)
type section_name =
| Section_text
| Section_data of bool (* true = init data, false = uninit data *)
| Section_small_data of bool
| Section_const
| Section_small_const
| Section_string
| Section_literal
| Section_jumptable
| Section_user of string * bool (*writable*) * bool (*executable*)
val initialize: unit -> unit
val define_section:
string -> ?iname:string -> ?uname:string
-> ?writable:bool -> ?executable:bool -> ?near:bool -> unit -> unit
val use_section_for: AST.ident -> string -> bool
val define_function: AST.ident -> unit
val define_variable: AST.ident -> int -> bool -> 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
driver/Driver.ml
+ 2
− 0
View file @ 913c1bcc
...@@ -61,6 +61,7 @@ let preprocess ifile ofile = ...@@ -61,6 +61,7 @@ let preprocess ifile ofile =
(* From preprocessed C to asm *) (* From preprocessed C to asm *)
let compile_c_file sourcename ifile ofile = let compile_c_file sourcename ifile ofile =
Sections.initialize();
(* Simplification options *) (* Simplification options *)
let simplifs = let simplifs =
"becv" (* blocks, impure exprs, implicit casts, volatiles: mandatory *) "becv" (* blocks, impure exprs, implicit casts, volatiles: mandatory *)
...@@ -108,6 +109,7 @@ let compile_c_file sourcename ifile ofile = ...@@ -108,6 +109,7 @@ let compile_c_file sourcename ifile ofile =
(* From Cminor to asm *) (* From Cminor to asm *)
let compile_cminor_file ifile ofile = let compile_cminor_file ifile ofile =
Sections.initialize();
let ic = open_in ifile in let ic = open_in ifile in
let lb = Lexing.from_channel ic in let lb = Lexing.from_channel ic in
try try
......
powerpc/PrintAsm.ml
+ 87
− 53
View file @ 913c1bcc
...@@ -15,6 +15,7 @@ ...@@ -15,6 +15,7 @@
open Printf open Printf
open Datatypes open Datatypes
open Camlcoq open Camlcoq
open Sections
open AST open AST
open Asm open Asm
...@@ -177,28 +178,58 @@ let creg oc r = ...@@ -177,28 +178,58 @@ let creg oc r =
| MacOS|Diab -> fprintf oc "cr%d" r | MacOS|Diab -> fprintf oc "cr%d" r
| Linux -> fprintf oc "%d" r | Linux -> fprintf oc "%d" r
let section oc name =
fprintf oc " %s\n" name
(* Names of sections *) (* Names of sections *)
let (text, data, const_data, float_literal) = let name_of_section_MacOS = function
| Section_text -> ".text"
| Section_data _ -> ".data"
| Section_small_data _ -> ".data"
| Section_const -> ".const"
| Section_small_const -> ".const"
| Section_string -> ".const"
| Section_literal -> ".const_data"
| Section_jumptable -> ".text"
| Section_user _ -> assert false
let name_of_section_Linux = function
| Section_text -> ".text"
| Section_data i -> if i then ".data" else ".bss"
| Section_small_data i -> if i then ".sdata" else ".sbss"
| Section_const -> ".rodata"
| Section_small_const -> ".sdata2"
| Section_string -> ".rodata"
| Section_literal -> ".section .rodata.cst8,\"aM\",@progbits,8"
| Section_jumptable -> ".text"
| Section_user(s, wr, ex) ->
sprintf ".section %s,\"a%s%s\",@progbits"
s (if wr then "w" else "") (if ex then "x" else "")
let name_of_section_Diab = function
| Section_text -> ".text"
| Section_data i -> if i then ".data" else ".bss"
| Section_small_data i -> if i then ".sdata" else ".sbss"
| Section_const -> ".text"
| Section_small_const -> ".sdata2"
| Section_string -> ".text"
| Section_literal -> ".text"
| Section_jumptable -> ".text"
| Section_user(s, wr, ex) ->
sprintf ".section %s,,%c"
s
(match wr, ex with
| true, true -> 'm' (* text+data *)
| true, false -> 'd' (* data *)
| false, true -> 'c' (* text *)
| false, false -> 'r') (* const *)
let name_of_section =
match target with match target with
| MacOS -> | MacOS -> name_of_section_MacOS
(".text", | Linux -> name_of_section_Linux
".data", | Diab -> name_of_section_Diab
".const",
".const_data") let section oc sec =
| Linux -> fprintf oc " %s\n" (name_of_section sec)
(".text",
".data",
".rodata",
".section .rodata.cst8,\"aM\",@progbits,8")
| Diab ->
(".text",
".data",
".text",
".text")
(* Encoding masks for rlwinm instructions *) (* Encoding masks for rlwinm instructions *)
...@@ -353,6 +384,9 @@ let print_builtin_function oc s = ...@@ -353,6 +384,9 @@ let print_builtin_function oc s =
module Labelset = Set.Make(struct type t = label let compare = compare end) module Labelset = Set.Make(struct type t = label let compare = compare end)
let float_literals : (int * int64) list ref = ref []
let jumptables : (int * label list) list ref = ref []
let print_instruction oc labels = function let print_instruction oc labels = function
| Padd(r1, r2, r3) -> | Padd(r1, r2, r3) ->
fprintf oc " add %a, %a, %a\n" ireg r1 ireg r2 ireg r3 fprintf oc " add %a, %a, %a\n" ireg r1 ireg r2 ireg r3
...@@ -410,10 +444,7 @@ let print_instruction oc labels = function ...@@ -410,10 +444,7 @@ let print_instruction oc labels = function
fprintf oc " lwz %a, %a(%a)\n" ireg GPR12 label_low lbl ireg GPR12; fprintf oc " lwz %a, %a(%a)\n" ireg GPR12 label_low lbl ireg GPR12;
fprintf oc " mtctr %a\n" ireg GPR12; fprintf oc " mtctr %a\n" ireg GPR12;
fprintf oc " bctr\n"; fprintf oc " bctr\n";
fprintf oc "%a:" label lbl; jumptables := (lbl, tbl) :: !jumptables;
List.iter
(fun l -> fprintf oc " .long %a\n" label (transl_label l))
tbl;
fprintf oc "%s end pseudoinstr btbl\n" comment fprintf oc "%s end pseudoinstr btbl\n" comment
| Pcmplw(r1, r2) -> | Pcmplw(r1, r2) ->
fprintf oc " cmplw %a, %a, %a\n" creg 0 ireg r1 ireg r2 fprintf oc " cmplw %a, %a, %a\n" creg 0 ireg r1 ireg r2
...@@ -471,9 +502,7 @@ let print_instruction oc labels = function ...@@ -471,9 +502,7 @@ let print_instruction oc labels = function
fprintf oc " lwz %a, 4(%a)\n" ireg r1 ireg GPR1; fprintf oc " lwz %a, 4(%a)\n" ireg r1 ireg GPR1;
fprintf oc " addis %a, %a, 0x8000\n" ireg r1 ireg r1; fprintf oc " addis %a, %a, 0x8000\n" ireg r1 ireg r1;
fprintf oc "%a: addi %a, %a, 8\n" label lbl3 ireg GPR1 ireg GPR1; fprintf oc "%a: addi %a, %a, 8\n" label lbl3 ireg GPR1 ireg GPR1;
section oc float_literal; float_literals := (lbl1, 0x41e00000_00000000L) :: !float_literals;
fprintf oc "%a: .long 0x41e00000, 0x00000000\n" label lbl1;
section oc text;
fprintf oc "%s end pseudoinstr fctiu\n" comment fprintf oc "%s end pseudoinstr fctiu\n" comment
| Pfdiv(r1, r2, r3) -> | Pfdiv(r1, r2, r3) ->
fprintf oc " fdiv %a, %a, %a\n" freg r1 freg r2 freg r3 fprintf oc " fdiv %a, %a, %a\n" freg r1 freg r2 freg r3
...@@ -503,9 +532,7 @@ let print_instruction oc labels = function ...@@ -503,9 +532,7 @@ let print_instruction oc labels = function
fprintf oc " lfd %a, 0(%a)\n" freg r1 ireg GPR1; fprintf oc " lfd %a, 0(%a)\n" freg r1 ireg GPR1;
fprintf oc " addi %a, %a, 8\n" ireg GPR1 ireg GPR1; fprintf oc " addi %a, %a, 8\n" ireg GPR1 ireg GPR1;
fprintf oc " fsub %a, %a, %a\n" freg r1 freg r1 freg FPR13; fprintf oc " fsub %a, %a, %a\n" freg r1 freg r1 freg FPR13;
section oc float_literal; float_literals := (lbl, 0x43300000_80000000L) :: !float_literals;
fprintf oc "%a: .long 0x43300000, 0x80000000\n" label lbl;
section oc text;
fprintf oc "%s end pseudoinstr ictf\n" comment fprintf oc "%s end pseudoinstr ictf\n" comment
| Piuctf(r1, r2) -> | Piuctf(r1, r2) ->
let lbl = new_label() in let lbl = new_label() in
...@@ -518,9 +545,7 @@ let print_instruction oc labels = function ...@@ -518,9 +545,7 @@ let print_instruction oc labels = function
fprintf oc " lfd %a, 0(%a)\n" freg r1 ireg GPR1; fprintf oc " lfd %a, 0(%a)\n" freg r1 ireg GPR1;
fprintf oc " addi %a, %a, 8\n" ireg GPR1 ireg GPR1; fprintf oc " addi %a, %a, 8\n" ireg GPR1 ireg GPR1;
fprintf oc " fsub %a, %a, %a\n" freg r1 freg r1 freg FPR13; fprintf oc " fsub %a, %a, %a\n" freg r1 freg r1 freg FPR13;
section oc float_literal; float_literals := (lbl, 0x43300000_00000000L) :: !float_literals;
fprintf oc "%a: .long 0x43300000, 0x00000000\n" label lbl;
section oc text;
fprintf oc "%s end pseudoinstr ictf\n" comment fprintf oc "%s end pseudoinstr ictf\n" comment
| Plbz(r1, c, r2) -> | Plbz(r1, c, r2) ->
fprintf oc " lbz %a, %a(%a)\n" ireg r1 constant c ireg r2 fprintf oc " lbz %a, %a(%a)\n" ireg r1 constant c ireg r2
...@@ -533,14 +558,8 @@ let print_instruction oc labels = function ...@@ -533,14 +558,8 @@ let print_instruction oc labels = function
| Plfi(r1, c) -> | Plfi(r1, c) ->
let lbl = new_label() in let lbl = new_label() in
fprintf oc " addis %a, 0, %a\n" ireg GPR12 label_high lbl; fprintf oc " addis %a, 0, %a\n" ireg GPR12 label_high lbl;
fprintf oc " lfd %a, %a(%a)\n" freg r1 label_low lbl ireg GPR12; fprintf oc " lfd %a, %a(%a) %s %.18g\n" freg r1 label_low lbl ireg GPR12 comment c;
section oc float_literal; float_literals := (lbl, Int64.bits_of_float c) :: !float_literals;
let n = Int64.bits_of_float c in
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 %s %.18g\n"
label lbl nhi nlo comment c;
section oc text
| Plfs(r1, c, r2) -> | Plfs(r1, c, r2) ->
fprintf oc " lfs %a, %a(%a)\n" freg r1 constant c ireg r2 fprintf oc " lfs %a, %a(%a)\n" freg r1 constant c ireg r2
| Plfsx(r1, r2, r3) -> | Plfsx(r1, r2, r3) ->
...@@ -633,6 +652,17 @@ let print_instruction oc labels = function ...@@ -633,6 +652,17 @@ let print_instruction oc labels = function
if Labelset.mem lbl labels then if Labelset.mem lbl labels then
fprintf oc "%a:\n" label (transl_label lbl) fprintf oc "%a:\n" label (transl_label lbl)
let print_literal oc (lbl, n) =
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_jumptable oc (lbl, tbl) =
fprintf oc "%a:" label lbl;
List.iter
(fun l -> fprintf oc " .long %a\n" label (transl_label l))
tbl
let rec labels_of_code accu = function let rec labels_of_code accu = function
| [] -> | [] ->
accu accu
...@@ -645,10 +675,10 @@ let rec labels_of_code accu = function ...@@ -645,10 +675,10 @@ let rec labels_of_code accu = function
let print_function oc name code = let print_function oc name code =
Hashtbl.clear current_function_labels; Hashtbl.clear current_function_labels;
section oc float_literals := [];
(match CPragmas.section_for_atom name true with jumptables := [];
| Some s -> s let (text, lit, jmptbl) = sections_for_function name in
| None -> text); section oc text;
fprintf oc " .align 2\n"; fprintf oc " .align 2\n";
if not (C2Clight.atom_is_static name) then if not (C2Clight.atom_is_static name) then
fprintf oc " .globl %a\n" symbol name; fprintf oc " .globl %a\n" symbol name;
...@@ -657,6 +687,16 @@ let print_function oc name code = ...@@ -657,6 +687,16 @@ let print_function oc name code =
if target <> MacOS then begin if target <> MacOS then begin
fprintf oc " .type %a, @function\n" symbol name; fprintf oc " .type %a, @function\n" symbol name;
fprintf oc " .size %a, . - %a\n" symbol name symbol name fprintf oc " .size %a, . - %a\n" symbol name symbol name
end;
if !float_literals <> [] then begin
section oc lit;
List.iter (print_literal oc) !float_literals;
float_literals := []
end;
if !jumptables <> [] then begin
section oc jmptbl;
List.iter (print_jumptable oc) !jumptables;
jumptables := []
end end
(* Generation of stub functions *) (* Generation of stub functions *)
...@@ -761,7 +801,7 @@ let non_variadic_stub oc name = ...@@ -761,7 +801,7 @@ let non_variadic_stub oc name =
let stub_function oc name ef = let stub_function oc name ef =
let name = extern_atom name in let name = extern_atom name in
fprintf oc " .text\n"; section oc Section_text;
fprintf oc " .align 2\n"; fprintf oc " .align 2\n";
fprintf oc "L%s$stub:\n" name; fprintf oc "L%s$stub:\n" name;
if Str.string_match re_variadic_stub name 0 if Str.string_match re_variadic_stub name 0
...@@ -777,7 +817,7 @@ end ...@@ -777,7 +817,7 @@ end
module Stubs_EABI = struct module Stubs_EABI = struct
let variadic_stub oc stub_name fun_name args = let variadic_stub oc stub_name fun_name args =
fprintf oc " .text\n"; section oc Section_text;
fprintf oc " .align 2\n"; fprintf oc " .align 2\n";
fprintf oc ".L%s$stub:\n" stub_name; fprintf oc ".L%s$stub:\n" stub_name;
(* bit 6 must be set if at least one argument is a float; clear otherwise *) (* bit 6 must be set if at least one argument is a float; clear otherwise *)
...@@ -829,7 +869,6 @@ let print_init oc = function ...@@ -829,7 +869,6 @@ let print_init oc = function
| Init_float32 n -> | Init_float32 n ->
fprintf oc " .long %ld %s %.18g\n" (Int32.bits_of_float n) comment n fprintf oc " .long %ld %s %.18g\n" (Int32.bits_of_float n) comment n
| Init_float64 n -> | Init_float64 n ->
(* .quad not working on all versions of the MacOSX assembler *)
let b = Int64.bits_of_float n in let b = Int64.bits_of_float n in
fprintf oc " .long %Ld, %Ld %s %.18g\n" fprintf oc " .long %Ld, %Ld %s %.18g\n"
(Int64.shift_right_logical b 32) (Int64.shift_right_logical b 32)
...@@ -857,12 +896,7 @@ let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) = ...@@ -857,12 +896,7 @@ let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) =
let init = let init =
match init_data with [Init_space _] -> false | _ -> true in match init_data with [Init_space _] -> false | _ -> true in
let sec = let sec =
match CPragmas.section_for_atom name init with Sections.section_for_variable name init
| Some s -> s
| None ->
if C2Clight.atom_is_readonly name
then const_data
else data
and align = and align =
match C2Clight.atom_alignof name with match C2Clight.atom_alignof name with
| Some a -> log2 a | Some a -> log2 a
......
powerpc/eabi/CPragmas.ml
+ 11
− 143
View file @ 913c1bcc
...@@ -19,111 +19,23 @@ open Printf ...@@ -19,111 +19,23 @@ open Printf
open Camlcoq open Camlcoq
open Cparser open Cparser
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
(* 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}
]
(* #pragma section *) (* #pragma section *)
let process_section_pragma classname istring ustring addrmode accmode = let process_section_pragma classname istring ustring addrmode accmode =
let old_si = Sections.define_section classname
try Hashtbl.find section_table classname ?iname: (if istring = "" then None else Some istring)
with Not_found -> default_section_info in ?uname: (if ustring = "" then None else Some ustring)
let si = ?writable: (if accmode = "" then None else Some(String.contains accmode 'W'))
{ sec_name_init = ?executable: (if accmode = "" then None else Some(String.contains accmode 'X'))
if istring = "" then old_si.sec_name_init else istring; ?near: (if addrmode = "" then None
sec_name_uninit = else Some(addrmode = "near-code" || addrmode = "near-data"))
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
(* #pragma use_section *) (* #pragma use_section *)
let use_section_table : (AST.ident, section_info) Hashtbl.t =
Hashtbl.create 51
let process_use_section_pragma classname id = let process_use_section_pragma classname id =
try if not (Sections.use_section_for (intern_string id) classname)
let info = Hashtbl.find section_table classname in then C2Clight.error (sprintf "unknown section name `%s'" classname)
Hashtbl.add use_section_table (intern_string id) info
with Not_found ->
C2Clight.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 d =
default_use_section id "CODE"
let define_stringlit id =
default_use_section id "STRING"
let define_variable id d =
let is_small limit =
match C2Clight.atom_sizeof id with
| None -> false
| Some sz -> sz <= limit in
let sect =
if C2Clight.atom_is_readonly id then
if is_small !Clflags.option_small_const then "SCONST" else "CONST"
else
if is_small !Clflags.option_small_data then "SDATA" else "DATA" in
default_use_section id sect
(* #pragma reserve_register *) (* #pragma reserve_register *)
...@@ -193,48 +105,4 @@ let process_pragma name = ...@@ -193,48 +105,4 @@ let process_pragma name =
false false
let initialize () = let initialize () =
C2Clight.process_pragma_hook := process_pragma; C2Clight.process_pragma_hook := process_pragma
C2Clight.define_variable_hook := define_variable;
C2Clight.define_function_hook := define_function;
C2Clight.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 C2Clight.atom_sizeof a with
| None -> false
| Some sz ->
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 ->
if C2Clight.atom_is_readonly a
then sz <= !Clflags.option_small_const
else sz <= !Clflags.option_small_data
end else
false
(* 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
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
powerpc/extractionMachdep.v
+ 1
− 1
View file @ 913c1bcc
...@@ -18,7 +18,7 @@ Extract Constant SelectOp.use_fused_mul => "(fun () -> !Clflags.option_fmadd)". ...@@ -18,7 +18,7 @@ Extract Constant SelectOp.use_fused_mul => "(fun () -> !Clflags.option_fmadd)".
(* Asm *) (* Asm *)
Extract Constant Asm.low_half => "fun _ -> assert false". Extract Constant Asm.low_half => "fun _ -> assert false".
Extract Constant Asm.high_half => "fun _ -> assert false". Extract Constant Asm.high_half => "fun _ -> assert false".
Extract Constant Asm.symbol_is_small_data => "CPragmas.atom_is_small_data". Extract Constant Asm.symbol_is_small_data => "Sections.atom_is_small_data".
Extract Constant Asm.small_data_area_offset => "fun _ _ _ -> assert false". Extract Constant Asm.small_data_area_offset => "fun _ _ _ -> assert false".
(* Suppression of stupidly big equality functions *) (* Suppression of stupidly big equality functions *)
......
powerpc/macosx/CPragmas.ml
+ 0
− 7
View file @ 913c1bcc
...@@ -19,10 +19,3 @@ ...@@ -19,10 +19,3 @@
let initialize () = () let initialize () = ()
(* PowerPC-specific: say if an atom is in a small data area *)
let atom_is_small_data a ofs = false
(* PowerPC-specific: determine section to use for a particular symbol *)
let section_for_atom a init = None
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment