diff options
| -rw-r--r-- | Makefile | 4 | ||||
| -rw-r--r-- | Makefile.extr | 14 | ||||
| -rw-r--r-- | driver/Configuration.ml | 125 | ||||
| -rw-r--r-- | driver/Driver.ml | 88 | ||||
| -rw-r--r-- | exportclight/Clightdefs.v | 13 | ||||
| -rw-r--r-- | exportclight/Clightgen.ml | 200 | ||||
| -rw-r--r-- | exportclight/ExportClight.ml | 170 | ||||
| -rw-r--r-- | lib/Readconfig.mli | 39 | ||||
| -rw-r--r-- | lib/Readconfig.mll | 111 |
9 files changed, 430 insertions, 334 deletions
@@ -174,9 +174,9 @@ doc/coq2html.ml: doc/coq2html.mll ocamllex -q doc/coq2html.mll tools/ndfun: tools/ndfun.ml - ocamlopt -o tools/ndfun str.cmxa tools/ndfun.ml $(LINKERSPEC) + ocamlopt -o tools/ndfun str.cmxa tools/ndfun.ml tools/modorder: tools/modorder.ml - ocamlopt -o tools/modorder str.cmxa tools/modorder.ml $(LINKERSPEC) + ocamlopt -o tools/modorder str.cmxa tools/modorder.ml latexdoc: cd doc; $(COQDOC) --latex -o doc/doc.tex -g $(FILES) diff --git a/Makefile.extr b/Makefile.extr index 2afd6e31..83ef3e2b 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -75,9 +75,11 @@ OCAMLLEX=ocamllex -q MODORDER=tools/modorder .depend.extr PARSERS=backend/CMparser.mly cparser/pre_parser.mly -LEXERS=backend/CMlexer.mll cparser/Lexer.mll lib/Tokenize.mll +LEXERS=backend/CMlexer.mll cparser/Lexer.mll \ + lib/Tokenize.mll lib/Readconfig.mll -LIBS=str.cmxa +LIBS=str.cmxa unix.cmxa +CHECKLINK_LIBS=str.cmxa EXECUTABLES=ccomp ccomp.byte cchecklink cchecklink.byte clightgen clightgen.byte GENERATED=$(PARSERS:.mly=.mli) $(PARSERS:.mly=.ml) $(LEXERS:.mll=.ml) @@ -90,11 +92,11 @@ CCOMP_OBJS:=$(shell $(MODORDER) driver/Driver.cmx) ccomp: $(CCOMP_OBJS) @echo "Linking $@" - @$(OCAMLOPT) -o $@ $(LIBS) $+ $(LINKERSPEC) + @$(OCAMLOPT) -o $@ $(LIBS) $+ ccomp.byte: $(CCOMP_OBJS:.cmx=.cmo) @echo "Linking $@" - @$(OCAMLC) -o $@ $(LIBS:.cmxa=.cma) $+ $(LINKERSPEC) + @$(OCAMLC) -o $@ $(LIBS:.cmxa=.cma) $+ ifeq ($(CCHECKLINK),true) @@ -102,11 +104,11 @@ CCHECKLINK_OBJS:=$(shell $(MODORDER) checklink/Validator.cmx) cchecklink: $(CCHECKLINK_OBJS) @echo "Linking $@" - @$(OCAMLOPT_P4) -linkpkg -o $@ $(LIBS) $+ + @$(OCAMLOPT_P4) -linkpkg -o $@ $(CHECKLINK_LIBS) $+ cchecklink.byte: $(CCHECKLINK_OBJS:.cmx=.cmo) @echo "Linking $@" - @$(OCAMLC_P4) -linkpkg -o $@ $(LIBS:.cmxa=.cma) $+ + @$(OCAMLC_P4) -linkpkg -o $@ $(CHECKLINK_LIBS:.cmxa=.cma) $+ endif diff --git a/driver/Configuration.ml b/driver/Configuration.ml index e73125f7..0012dc0c 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -10,86 +10,87 @@ (* *) (* *********************************************************************) +open Printf -let config_vars: (string, string) Hashtbl.t = Hashtbl.create 10 +(* Locate the .ini file, which is either in the same directory as + the executable or in the directory ../share *) +let ini_file_name = + try + Sys.getenv "COMPCERT_CONFIG" + with Not_found -> + let exe_dir = Filename.dirname Sys.executable_name in + let exe_ini = Filename.concat exe_dir "compcert.ini" in + let share_dir = + Filename.concat (Filename.concat exe_dir Filename.parent_dir_name) + "share" in + let share_ini = Filename.concat share_dir "compcert.ini" in + if Sys.file_exists exe_ini then exe_ini + else if Sys.file_exists share_ini then share_ini + else begin + eprintf "Cannot find compcert.ini configuration file.\n"; + exit 2 + end + +(* Read in the .ini file *) -(* Read in the .ini file, which is either in the same directory or in the directory ../share *) let _ = try - let file = - try - let env_file = Sys.getenv "COMPCERT_CONFIG" in - open_in env_file - with Not_found -> - let dir = Sys.getcwd () - and name = Sys.executable_name in - let dirname = if Filename.is_relative name then - Filename.dirname (Filename.concat dir name) - else - Filename.dirname name - in - let share_dir = Filename.concat (Filename.concat dirname Filename.parent_dir_name) "share" in - try - open_in (Filename.concat dirname "compcert.ini") - with Sys_error _ -> - open_in (Filename.concat share_dir "compcert.ini") - in - (try - let ini_line = Str.regexp "\\([^=]+\\)=\\(.+\\)" in - while true do - let line = input_line file in - if Str.string_match ini_line line 0 then - let key = Str.matched_group 1 line - and value = Str.matched_group 2 line in - Hashtbl.add config_vars key value - else - Printf.eprintf "Wrong value %s in .ini file.\n" line - done - with End_of_file -> close_in file) - with Sys_error msg -> Printf.eprintf "Unable to open .ini file\n" + Readconfig.read_config_file ini_file_name + with + | Readconfig.Error(file, lineno, msg) -> + eprintf "Error reading configuration file %s.\n" ini_file_name; + eprintf "%s:%d:%s\n" file lineno msg; + exit 2 + | Sys_error msg -> + eprintf "Error reading configuration file %s.\n" ini_file_name; + eprintf "%s\n" msg; + exit 2 let get_config key = - try - Hashtbl.find config_vars key - with Not_found -> - Printf.eprintf "Configuration option `%s' is not set\n" key; exit 2 + match Readconfig.key_val key with + | Some v -> v + | None -> eprintf "Configuration option `%s' is not set\n" key; exit 2 -let bad_config key v = - Printf.eprintf "Invalid value `%s' for configuation option `%s'\n" v key; exit 2 +let bad_config key vl = + eprintf "Invalid value `%s' for configuration option `%s'\n" + (String.concat " " vl) key; + exit 2 -let prepro = get_config "prepro" -let asm = get_config "asm" -let linker = get_config "linker" -let arch = - let v = get_config "arch" in - (match v with - | "powerpc" - | "arm" - | "ia32" -> () - | _ -> bad_config "arch" v); - v +let get_config_string key = + match get_config key with + | [v] -> v + | vl -> bad_config key vl -let model = get_config "model" -let abi = get_config "abi" -let system = get_config "system" +let get_config_list key = + match get_config key with + | [] -> bad_config key [] + | vl -> vl + +let prepro = get_config_list "prepro" +let asm = get_config_list "asm" +let linker = get_config_list "linker" +let arch = + match get_config_string "arch" with + | "powerpc"|"arm"|"ia32" as a -> a + | v -> bad_config "arch" [v] +let model = get_config_string "model" +let abi = get_config_string "abi" +let system = get_config_string "system" let has_runtime_lib = - match get_config "has_runtime_lib" with + match get_config_string "has_runtime_lib" with | "true" -> true | "false" -> false - | v -> bad_config "has_runtime_lib" v - - + | v -> bad_config "has_runtime_lib" [v] let stdlib_path = if has_runtime_lib then - get_config "stdlib_path" + get_config_string "stdlib_path" else "" - let asm_supports_cfi = - match get_config "asm_supports_cfi" with + match get_config_string "asm_supports_cfi" with | "true" -> true | "false" -> false - | v -> bad_config "asm_supports_cfi" v + | v -> bad_config "asm_supports_cfi" [v] -let version = get_config "version" +let version = get_config_string "version" diff --git a/driver/Driver.ml b/driver/Driver.ml index 5d4c2f9c..d22dd77c 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -20,17 +20,38 @@ open Timing let stdlib_path = ref Configuration.stdlib_path -let command cmd = +(* Invocation of external tools *) + +let command ?stdout args = if !option_v then begin - prerr_string "+ "; prerr_string cmd; prerr_endline "" + eprintf "+ %s" (String.concat " " args); + begin match stdout with + | None -> () + | Some f -> eprintf " > %s" f + end; + prerr_endline "" end; - Sys.command cmd - -let quote_options opts = - String.concat " " (List.rev_map Filename.quote opts) - -let quote_arguments args = - String.concat " " (List.map Filename.quote args) + let argv = Array.of_list args in + assert (Array.length argv > 0); + try + let fd_out = + match stdout with + | None -> Unix.stdout + | Some f -> + Unix.openfile f [Unix.O_WRONLY; Unix.O_CREAT; Unix.O_TRUNC] 0o666 in + let pid = + Unix.create_process argv.(0) argv Unix.stdin fd_out Unix.stderr in + let (_, status) = + Unix.waitpid [] pid in + if stdout <> None then Unix.close fd_out; + match status with + | Unix.WEXITED rc -> rc + | Unix.WSIGNALED n | Unix.WSTOPPED n -> + eprintf "Command '%s' killed on a signal.\n" argv.(0); -1 + with Unix.Unix_error(err, fn, param) -> + eprintf "Error executing '%s': %s: %s %s\n" + argv.(0) fn (Unix.error_message err) param; + -1 let safe_remove file = try Sys.remove file with Sys_error _ -> () @@ -68,16 +89,17 @@ let output_filename_default default_file = let preprocess ifile ofile = let output = - if ofile = "-" then "" else sprintf "> %s" ofile in - let cmd = - sprintf "%s -D__COMPCERT__ %s %s %s %s" - Configuration.prepro - (if Configuration.has_runtime_lib - then sprintf "-I%s" !stdlib_path - else "") - (quote_options !prepro_options) - ifile output in - if command cmd <> 0 then begin + if ofile = "-" then None else Some ofile in + let cmd = List.concat [ + Configuration.prepro; + ["-D__COMPCERT__"]; + (if Configuration.has_runtime_lib + then ["-I" ^ !stdlib_path] + else []); + List.rev !prepro_options; + [ifile] + ] in + if command ?stdout:output cmd <> 0 then begin if ofile <> "-" then safe_remove ofile; eprintf "Error during preprocessing.\n"; exit 2 @@ -208,11 +230,13 @@ let compile_cminor_file ifile ofile = (* From asm to object file *) let assemble ifile ofile = - let cmd = - sprintf "%s -o %s %s %s" - Configuration.asm ofile (quote_options !assembler_options) ifile in - let retcode = command cmd in - if retcode <> 0 then begin + let cmd = List.concat [ + Configuration.asm; + ["-o"; ofile]; + List.rev !assembler_options; + [ifile] + ] in + if command cmd <> 0 then begin safe_remove ofile; eprintf "Error during assembling.\n"; exit 2 @@ -221,14 +245,14 @@ let assemble ifile ofile = (* Linking *) let linker exe_name files = - let cmd = - sprintf "%s -o %s %s %s" - Configuration.linker - (Filename.quote exe_name) - (quote_arguments files) - (if Configuration.has_runtime_lib - then sprintf "-L%s -lcompcert" !stdlib_path - else "") in + let cmd = List.concat [ + Configuration.linker; + ["-o"; exe_name]; + files; + (if Configuration.has_runtime_lib + then ["-L" ^ !stdlib_path; "-lcompcert"] + else []) + ] in if command cmd <> 0 then exit 2 (* Processing of a .c file *) diff --git a/exportclight/Clightdefs.v b/exportclight/Clightdefs.v index 28d0cc8f..a75c95a5 100644 --- a/exportclight/Clightdefs.v +++ b/exportclight/Clightdefs.v @@ -23,6 +23,8 @@ Require Export AST. Require Export Ctypes. Require Export Cop. Require Export Clight. +Require Import Maps. +Require Import Errors. Definition tvoid := Tvoid. Definition tschar := Tint I8 Signed noattr. @@ -50,9 +52,8 @@ Definition tattr (a: attr) (ty: type) := | Tpointer elt _ => Tpointer elt a | Tarray elt sz _ => Tarray elt sz a | Tfunction args res cc => Tfunction args res cc - | Tstruct id fld _ => Tstruct id fld a - | Tunion id fld _ => Tunion id fld a - | Tcomp_ptr id _ => Tcomp_ptr id a + | Tstruct id _ => Tstruct id a + | Tunion id _ => Tunion id a end. Definition tvolatile (ty: type) := tattr volatile_attr ty. @@ -62,3 +63,9 @@ Definition talignas (n: N) (ty: type) := Definition tvolatile_alignas (n: N) (ty: type) := tattr {| attr_volatile := true; attr_alignas := Some n |} ty. + +Definition make_composite_env (comps: list composite_definition): composite_env := + match build_composite_env comps with + | OK e => e + | Error _ => PTree.empty _ + end. diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml index 53eb96fd..c1009b4f 100644 --- a/exportclight/Clightgen.ml +++ b/exportclight/Clightgen.ml @@ -14,24 +14,45 @@ (* *********************************************************************) open Printf +open Commandline open Clflags (* Location of the compatibility library *) -let stdlib_path = ref( - try - Sys.getenv "COMPCERT_LIBRARY" - with Not_found -> - Configuration.stdlib_path) +let stdlib_path = ref Configuration.stdlib_path + +(* Invocation of external tools *) -let command cmd = +let command ?stdout args = if !option_v then begin - prerr_string "+ "; prerr_string cmd; prerr_endline "" + eprintf "+ %s" (String.concat " " args); + begin match stdout with + | None -> () + | Some f -> eprintf " > %s" f + end; + prerr_endline "" end; - Sys.command cmd - -let quote_options opts = - String.concat " " (List.rev_map Filename.quote opts) + let argv = Array.of_list args in + assert (Array.length argv > 0); + try + let fd_out = + match stdout with + | None -> Unix.stdout + | Some f -> + Unix.openfile f [Unix.O_WRONLY; Unix.O_CREAT; Unix.O_TRUNC] 0o666 in + let pid = + Unix.create_process argv.(0) argv Unix.stdin fd_out Unix.stderr in + let (_, status) = + Unix.waitpid [] pid in + if stdout <> None then Unix.close fd_out; + match status with + | Unix.WEXITED rc -> rc + | Unix.WSIGNALED n | Unix.WSTOPPED n -> + eprintf "Command '%s' killed on a signal.\n" argv.(0); -1 + with Unix.Unix_error(err, fn, param) -> + eprintf "Error executing '%s': %s: %s %s\n" + argv.(0) fn (Unix.error_message err) param; + -1 let safe_remove file = try Sys.remove file with Sys_error _ -> () @@ -47,20 +68,32 @@ let print_error oc msg = List.iter print_one_error msg; output_char oc '\n' +(* Determine names for output files. We use -o option if specified + and if this is the final destination file (not a dump file). + Otherwise, we generate a file in the current directory. *) + +let output_filename ?(final = false) source_file source_suffix output_suffix = + match !option_o with + | Some file when final -> file + | _ -> + Filename.basename (Filename.chop_suffix source_file source_suffix) + ^ output_suffix + (* From C to preprocessed C *) let preprocess ifile ofile = let output = - if ofile = "-" then "" else sprintf "> %s" ofile in - let cmd = - sprintf "%s -D__COMPCERT__ %s %s %s %s" - Configuration.prepro - (if Configuration.has_runtime_lib - then sprintf "-I%s" !stdlib_path - else "") - (quote_options !prepro_options) - ifile output in - if command cmd <> 0 then begin + if ofile = "-" then None else Some ofile in + let cmd = List.concat [ + Configuration.prepro; + ["-D__COMPCERT__"]; + (if Configuration.has_runtime_lib + then ["-I" ^ !stdlib_path] + else []); + List.rev !prepro_options; + [ifile] + ] in + if command ?stdout:output cmd <> 0 then begin if ofile <> "-" then safe_remove ofile; eprintf "Error during preprocessing.\n"; exit 2 @@ -82,24 +115,22 @@ let parse_c_file sourcename ifile = match Parse.preprocessed_file simplifs sourcename ifile with | None -> exit 2 | Some p -> p in - (* Remove preprocessed file (always a temp file) *) - safe_remove ifile; (* Save C AST if requested *) if !option_dparse then begin - let ofile = Filename.chop_suffix sourcename ".c" ^ ".parsed.c" in + let ofile = output_filename sourcename ".c" ".parsed.c" in let oc = open_out ofile in Cprint.program (Format.formatter_of_out_channel oc) ast; close_out oc end; (* Conversion to Csyntax *) let csyntax = - match C2C.convertProgram ast with + match Timing.time "CompCert C generation" C2C.convertProgram ast with | None -> exit 2 | Some p -> p in flush stderr; (* Save CompCert C AST if requested *) if !option_dcmedium then begin - let ofile = Filename.chop_suffix sourcename ".c" ^ ".compcert.c" in + let ofile = output_filename sourcename ".c" ".compcert.c" in let oc = open_out ofile in PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax; close_out oc @@ -157,59 +188,6 @@ let explode_comma_option s = | [] -> assert false | hd :: tl -> tl -type action = - | Set of bool ref - | Unset 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 "%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(Unset r) -> - r := false; 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 usage_string = "The CompCert Clight generator Usage: clightgen [options] <source files> @@ -238,36 +216,63 @@ General options: -v Print external commands before invoking them " +let print_usage_and_exit _ = + printf "%s" usage_string; exit 0 + let language_support_options = [ option_fbitfields; option_flongdouble; - option_fstruct_return; option_fvararg_calls; option_fpacked_structs + option_fstruct_return; option_fvararg_calls; option_funprototyped; + option_fpacked_structs; option_finline_asm ] +let set_all opts = List.iter (fun r -> r := true) opts +let unset_all opts = List.iter (fun r -> r := false) opts + let cmdline_actions = let f_opt name ref = - ["-f" ^ name ^ "$", Set ref; "-fno-" ^ name ^ "$", Unset ref] in + [Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] in [ - "-I$", String(fun s -> prepro_options := s :: "-I" :: !prepro_options); - "-D$", String(fun s -> prepro_options := s :: "-D" :: !prepro_options); - "-U$", String(fun s -> prepro_options := s :: "-U" :: !prepro_options); - "-[IDU].", Self(fun s -> prepro_options := s :: !prepro_options); - "-dparse$", Set option_dparse; - "-dc$", Set option_dcmedium; - "-dclight$", Set option_dclight; - "-E$", Set option_E; - ".*\\.c$", Self (fun s -> process_c_file s); - "-Wp,", Self (fun s -> - prepro_options := List.rev_append (explode_comma_option s) !prepro_options); - "-fall$", Self (fun _ -> - List.iter (fun r -> r := true) language_support_options); - "-fnone$", Self (fun _ -> - List.iter (fun r -> r := false) language_support_options); +(* Getting help *) + Exact "-help", Self print_usage_and_exit; + Exact "--help", Self print_usage_and_exit; +(* Processing options *) + Exact "-E", Set option_E; +(* Preprocessing options *) + Exact "-I", String(fun s -> prepro_options := s :: "-I" :: !prepro_options); + Prefix "-I", Self(fun s -> prepro_options := s :: !prepro_options); + Exact "-D", String(fun s -> prepro_options := s :: "-D" :: !prepro_options); + Prefix "-D", Self(fun s -> prepro_options := s :: !prepro_options); + Exact "-U", String(fun s -> prepro_options := s :: "-U" :: !prepro_options); + Prefix "-U", Self(fun s -> prepro_options := s :: !prepro_options); + Prefix "-Wp,", Self (fun s -> + prepro_options := List.rev_append (explode_comma_option s) !prepro_options); +(* Language support options -- more below *) + Exact "-fall", Self (fun _ -> set_all language_support_options); + Exact "-fnone", Self (fun _ -> unset_all language_support_options); +(* Tracing options *) + Exact "-dparse", Set option_dparse; + Exact "-dc", Set option_dcmedium; + Exact "-dclight", Set option_dclight; +(* General options *) + Exact "-v", Set option_v; + Exact "-stdlib", String(fun s -> stdlib_path := s); ] +(* -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 "bitfields" option_fbitfields @ f_opt "vararg-calls" option_fvararg_calls + @ f_opt "unprototyped" option_funprototyped @ f_opt "packed-structs" option_fpacked_structs + @ f_opt "inline-asm" option_finline_asm + @ [ +(* Catch options that are not handled *) + Prefix "-", Self (fun s -> + eprintf "Unknown option `%s'\n" s; exit 2); +(* File arguments *) + Suffix ".c", Self (fun s -> process_c_file s); + ] let _ = Gc.set { (Gc.get()) with @@ -284,4 +289,5 @@ let _ = end; Builtins.set C2C.builtins; CPragmas.initialize(); - parse_cmdline cmdline_actions usage_string + parse_cmdline cmdline_actions + diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index e4d1ce53..51dd0757 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -132,9 +132,20 @@ let coqfloat p n = let coqsingle p n = fprintf p "(Float32.of_bits %a)" coqint (Floats.Float32.to_bits n) -(* Types *) +let coqN p n = + fprintf p "%ld%%N" (N.to_int32 n) + +(* Raw attributes *) -let use_struct_names = ref true +let attribute p a = + if a = noattr then + fprintf p "noattr" + else + fprintf p "{| attr_volatile := %B; attr_alignas := %a |}" + a.attr_volatile + (print_option coqN) a.attr_alignas + +(* Types *) let rec typ p t = match attr_of_type t with @@ -143,9 +154,9 @@ let rec typ p t = | { attr_volatile = true; attr_alignas = None} -> fprintf p "(tvolatile %a)" rtyp t | { attr_volatile = false; attr_alignas = Some n} -> - fprintf p "(talignas %ld%%N %a)" (N.to_int32 n) rtyp t + fprintf p "(talignas %a %a)" coqN n rtyp t | { attr_volatile = true; attr_alignas = Some n} -> - fprintf p "(tvolatile_alignas %ld%%N %a)" (N.to_int32 n) rtyp t + fprintf p "(tvolatile_alignas %a %a)" coqN n rtyp t and rtyp p = function | Tvoid -> fprintf p "tvoid" @@ -176,16 +187,10 @@ and rtyp p = function | Tfunction(targs, tres, cc) -> fprintf p "@[<hov 2>(Tfunction@ %a@ %a@ %a)@]" typlist targs typ tres callconv cc - | Tstruct(id, flds, _) -> - if !use_struct_names - then fprintf p "t%a" ident id - else fprintf p "@[<hov 2>(Tstruct %a@ %a@ noattr)@]" ident id fieldlist flds - | Tunion(id, flds, _) -> - if !use_struct_names - then fprintf p "t%a" ident id - else fprintf p "@[<hov 2>(Tunion %a@ %a@ noattr)@]" ident id fieldlist flds - | Tcomp_ptr(id, _) -> - fprintf p "(Tcomp_ptr %a noattr)" ident id + | Tstruct(id, _) -> + fprintf p "(Tstruct %a noattr)" ident id + | Tunion(id, _) -> + fprintf p "(Tunion %a noattr)" ident id and typlist p = function | Tnil -> @@ -193,12 +198,6 @@ and typlist p = function | Tcons(t, tl) -> fprintf p "@[<hov 2>(Tcons@ %a@ %a)@]" typ t typlist tl -and fieldlist p = function - | Fnil -> - fprintf p "Fnil" - | Fcons(id, t, fl) -> - fprintf p "@[<hov 2>(Fcons %a@ %a@ %a)@]" ident id typ t fieldlist fl - and callconv p cc = if cc = cc_default then fprintf p "cc_default" @@ -323,6 +322,10 @@ let rec expr p = function (name_binop op) expr a1 expr a2 typ t | Ecast(a1, t) -> fprintf p "@[<hov 2>(Ecast@ %a@ %a)@]" expr a1 typ t + | Esizeof(t1, t) -> + fprintf p "(Esizeof %a %a)" typ t1 typ t + | Ealignof(t1, t) -> + fprintf p "(Ealignof %a %a)" typ t1 typ t (* Statements *) @@ -420,115 +423,14 @@ let print_ident_globdef p = function | (id, Gvar v) -> fprintf p "(%a, Gvar v_%s)" ident id (extern_atom id) -(* Collecting the names and fields of structs and unions *) - -module TypeSet = Set.Make(struct - type t = coq_type - let compare = Pervasives.compare -end) - -let struct_unions = ref TypeSet.empty - -let register_struct_union ty = - struct_unions := TypeSet.add ty !struct_unions - -let rec collect_type = function - | Tvoid -> () - | Tint _ -> () - | Tlong _ -> () - | Tfloat _ -> () - | Tpointer(t, _) -> collect_type t - | Tarray(t, _, _) -> collect_type t - | Tfunction(args, res, _) -> collect_type_list args; collect_type res - | Tstruct(id, fld, _) -> - register_struct_union (Tstruct(id, fld, noattr)) (*; collect_fields fld*) - | Tunion(id, fld, _) -> - register_struct_union (Tunion(id, fld, noattr)) (*; collect_fields fld*) - | Tcomp_ptr _ -> () - -and collect_type_list = function - | Tnil -> () - | Tcons(hd, tl) -> collect_type hd; collect_type_list tl - -and collect_fields = function - | Fnil -> () - | Fcons(id, hd, tl) -> collect_type hd; collect_fields tl - -let rec collect_expr e = - collect_type (typeof e); - match e with - | Econst_int _ -> () - | Econst_float _ -> () - | Econst_long _ -> () - | Econst_single _ -> () - | Evar _ -> () - | Etempvar _ -> () - | Ederef(r, _) -> collect_expr r - | Efield(l, _, _) -> collect_expr l - | Eaddrof(l, _) -> collect_expr l - | Eunop(_, r, _) -> collect_expr r - | Ebinop(_, r1, r2, _) -> collect_expr r1; collect_expr r2 - | Ecast(r, _) -> collect_expr r - -let rec collect_exprlist = function - | [] -> () - | r1 :: rl -> collect_expr r1; collect_exprlist rl - -let rec temp_of_expr = function - | Etempvar(tmp, _) -> Some tmp - | Ecast(e, _) -> temp_of_expr e - | _ -> None +(* Composite definitions *) -let rec collect_stmt = function - | Sskip -> () - | Sassign(e1, e2) -> collect_expr e1; collect_expr e2 - | Sset(id, e2) -> - begin match temp_of_expr e2 with - | Some tmp -> name_temporary tmp id - | None -> () - end; - collect_expr e2 - | Scall(optid, e1, el) -> collect_expr e1; collect_exprlist el - | Sbuiltin(optid, ef, tyl, el) -> collect_exprlist el - | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2 - | Sifthenelse(e, s1, s2) -> collect_expr e; collect_stmt s1; collect_stmt s2 - | Sloop(s1, s2) -> collect_stmt s1; collect_stmt s2 - | Sbreak -> () - | Scontinue -> () - | Sswitch(e, cases) -> collect_expr e; collect_cases cases - | Sreturn None -> () - | Sreturn (Some e) -> collect_expr e - | Slabel(lbl, s) -> collect_stmt s - | Sgoto lbl -> () - -and collect_cases = function - | LSnil -> () - | LScons(lbl, s, rem) -> collect_stmt s; collect_cases rem - -let collect_function f = - collect_type f.fn_return; - List.iter (fun (id, ty) -> collect_type ty) f.fn_params; - List.iter (fun (id, ty) -> collect_type ty) f.fn_vars; - List.iter (fun (id, ty) -> collect_type ty) f.fn_temps; - collect_stmt f.fn_body - -let collect_globdef (id, gd) = - match gd with - | Gfun(External(_, args, res, _)) -> collect_type_list args; collect_type res - | Gfun(Internal f) -> collect_function f - | Gvar v -> collect_type v.gvar_info - -let define_struct p ty = - match ty with - | Tstruct(id, _, _) | Tunion(id, _, _) -> - fprintf p "@[<hv 2>Definition t%a :=@ %a.@]@ " ident id typ ty - | _ -> assert false - -let define_structs p prog = - use_struct_names := false; - TypeSet.iter (define_struct p) !struct_unions; - use_struct_names := true; - fprintf p "@ " +let print_composite_definition p (Composite(id, su, m, a)) = + fprintf p "@[<hv 2>Composite %a %s@ %a@ %a@]" + ident id + (match su with Struct -> "Struct" | Union -> "Union") + (print_list (print_pair ident typ)) m + attribute a (* Assertion processing *) @@ -605,14 +507,18 @@ let print_program p prog = fprintf p "%s" prologue; Hashtbl.clear temp_names; all_temp_names := StringSet.empty; - struct_unions := TypeSet.empty; - List.iter collect_globdef prog.prog_defs; define_idents p; - define_structs p prog; List.iter (print_globdef p) prog.prog_defs; + fprintf p "Definition composites : list composite_definition :=@ "; + print_list print_composite_definition p prog.prog_types; + fprintf p ".@ @ "; fprintf p "Definition prog : Clight.program := {|@ "; fprintf p "prog_defs :=@ %a;@ " (print_list print_ident_globdef) prog.prog_defs; - fprintf p "prog_main := %a@ " ident prog.prog_main; + fprintf p "prog_public :=@ %a;@ " (print_list ident) prog.prog_public; + fprintf p "prog_main := %a;@ " ident prog.prog_main; + fprintf p "prog_types := composites;@ "; + fprintf p "prog_comp_env := make_composite_env composites;@ "; + fprintf p "prog_comp_env_eq := refl_equal _@ "; fprintf p "|}.@ "; print_assertions p; fprintf p "@]@." diff --git a/lib/Readconfig.mli b/lib/Readconfig.mli new file mode 100644 index 00000000..c81e7786 --- /dev/null +++ b/lib/Readconfig.mli @@ -0,0 +1,39 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(* Reading configuration files *) + +(* The format of a configuration file is a list of lines + variable=value + The "value" on the right hand side is a list of whitespace-separated + words. Quoting is honored with the same rules as POSIX shell: + \<newline> for multi-line values + single quotes no escapes within + double quotes \$ \` \<doublequote> \\ \<newline> as escapes + Finally, lines starting with '#' are comments. +*) + +val read_config_file: string -> unit + (** Read (key, value) pairs from the given file name. Raise [Error] + if file is ill-formed. *) + +val key_val: string -> string list option + (** [key_val k] returns the value associated with key [k], if any. + Otherwise, [None] is returned. *) + +exception Error of string * int * string + (** Raised in case of error. + First argument is file name, second argument is line number, + third argument is an explanation of the error. *) diff --git a/lib/Readconfig.mll b/lib/Readconfig.mll new file mode 100644 index 00000000..27ef32cf --- /dev/null +++ b/lib/Readconfig.mll @@ -0,0 +1,111 @@ +{ + +(* Recording key=val bindings *) + +let key_val_tbl : (string, string list) Hashtbl.t = Hashtbl.create 17 + +let key_val key = + try Some(Hashtbl.find key_val_tbl key) with Not_found -> None + +(* Auxiliaries for parsing *) + +let buf = Buffer.create 32 + +let stash inword words = + if inword then begin + let w = Buffer.contents buf in + Buffer.clear buf; + w :: words + end else + words + +(* Error reporting *) + +exception Error of string * int * string + +let error msg lexbuf = + Lexing.(raise (Error(lexbuf.lex_curr_p.pos_fname, + lexbuf.lex_curr_p.pos_lnum, + msg))) + +let ill_formed_line lexbuf = error "Ill-formed line" lexbuf +let unterminated_quote lexbuf = error "Unterminated quote" lexbuf +let lone_backslash lexbuf = error "Lone \\ (backslash) at end of file" lexbuf + +} + +let whitespace = [' ' '\t' '\012' '\r'] +let newline = '\r'* '\n' +let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '0'-'9' '_' '.']* + +rule begline = parse + | '#' [^ '\n']* ('\n' | eof) + { Lexing.new_line lexbuf; begline lexbuf } + | whitespace* (ident as key) whitespace* '=' + { let words = unquoted false [] lexbuf in + Hashtbl.add key_val_tbl key (List.rev words); + begline lexbuf } + | eof + { () } + | _ + { ill_formed_line lexbuf } + +and unquoted inword words = parse + | '\n' | eof { Lexing.new_line lexbuf; stash inword words } + | whitespace+ { unquoted false (stash inword words) lexbuf } + | '\\' newline { Lexing.new_line lexbuf; unquoted inword words lexbuf } + | '\\' (_ as c) { Buffer.add_char buf c; unquoted true words lexbuf } + | '\\' eof { lone_backslash lexbuf } + | '\'' { singlequote lexbuf; unquoted true words lexbuf } + | '\"' { doublequote lexbuf; unquoted true words lexbuf } + | _ as c { Buffer.add_char buf c; unquoted true words lexbuf } + +and singlequote = parse + | eof { unterminated_quote lexbuf } + | '\'' { () } + | newline { Lexing.new_line lexbuf; + Buffer.add_char buf '\n'; singlequote lexbuf } + | _ as c { Buffer.add_char buf c; singlequote lexbuf } + +and doublequote = parse + | eof { unterminated_quote lexbuf } + | '\"' { () } + | '\\' newline { Lexing.new_line lexbuf; doublequote lexbuf } + | '\\' (['$' '`' '\"' '\\'] as c) + { Buffer.add_char buf c; doublequote lexbuf } + | newline { Lexing.new_line lexbuf; + Buffer.add_char buf '\n'; doublequote lexbuf } + | _ as c { Buffer.add_char buf c; doublequote lexbuf } + +{ + +(* The entry point *) + +let read_config_file filename = + let ic = open_in filename in + let lexbuf = Lexing.from_channel ic in + Lexing.(lexbuf.lex_start_p <- {lexbuf.lex_start_p with pos_fname = filename}); + try + Hashtbl.clear key_val_tbl; + begline lexbuf; + close_in ic + with x -> + close_in ic; raise x + +(* Test harness *) +(* +open Printf + +let _ = + Hashtbl.clear key_val_tbl; + begline (Lexing.from_channel stdin); + Hashtbl.iter + (fun key value -> + printf "%s =" key; + List.iter (fun v -> printf " |%s|" v) value; + printf "\n") + key_val_tbl +*) + +} + |