Update clightgen with respect to new representation of composites.

3 files changed, 151 insertions, 232 deletions

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 "@]@."