source: Deliverables/D3.3/id-lookup-branch/Clight/compcert-1.7.1-matita.patch @ 3362

cfrontend/PrintMatitaSyntax.ml

@@ +1 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Pretty-printer for Csyntax *)
+
+open Format
+open Camlcoq
+open Datatypes
+open AST
+open Csyntax
+
+let print_list f fmt l =
+  let rec aux fmt = function
+      | [] -> ()
+      | [x] -> f fmt x
+      | h::t -> f fmt h; fprintf fmt ";@ "; aux fmt t
+  in
+  fprintf fmt "@[[%a]@]" aux l
+
+let name_unop = function
+  | Onotbool -> "Onotbool"
+  | Onotint  -> "Onotint"
+  | Oneg     -> "Oneg"
+
+
+let name_binop = function
+  | Oadd -> "Oadd"
+  | Osub -> "Osub"
+  | Omul -> "Omul"
+  | Odiv -> "Odiv"
+  | Omod -> "Omod"
+  | Oand -> "Oand"
+  | Oor  -> "Oor"
+  | Oxor -> "Oxor"
+  | Oshl -> "Oshl"
+  | Oshr -> "Oshr"
+  | Oeq  -> "Oeq"
+  | One  -> "One"
+  | Olt  -> "Olt"
+  | Ogt  -> "Ogt"
+  | Ole  -> "Ole"
+  | Oge  -> "Oge"
+
+let name_inttype sz sg =
+  match sz, sg with
+  | I8, Signed    -> "I8 Signed   "
+  | I8, Unsigned  -> "I8 Unsigned "
+  | I16, Signed   -> "I16 Signed  "
+  | I16, Unsigned -> "I16 Unsigned"
+  | I32, Signed   -> "I32 Signed  "
+  | I32, Unsigned -> "I32 Unsigned"
+
+let name_floattype sz =
+  match sz with
+  | F32 -> "F32"
+  | F64 -> "F64"
+
+(* Collecting the names and fields of structs and unions *)
+
+module StructUnionSet = Set.Make(struct
+  type t = string * fieldlist
+  let compare (n1, _ : t) (n2, _ : t) = compare n1 n2
+end)
+
+let struct_unions = ref StructUnionSet.empty
+
+let register_struct_union id fld =
+  struct_unions := StructUnionSet.add (extern_atom id, fld) !struct_unions
+
+(* Declarator (identifier + type) *)
+
+let name_optid id =
+  if id = "" then "" else " " ^ id
+
+let parenthesize_if_pointer id =
+  if String.length id > 0 && id.[0] = '*' then "(" ^ id ^ ")" else id
+
+let rec name_cdecl id ty =
+  match ty with
+  | Tvoid ->
+      "void" ^ name_optid id
+  | Tint(sz, sg) ->
+      name_inttype sz sg ^ name_optid id
+  | Tfloat sz ->
+      name_floattype sz ^ name_optid id
+  | Tpointer t ->
+      name_cdecl ("*" ^ id) t
+  | Tarray(t, n) ->
+      name_cdecl
+        (sprintf "%s[%ld]" (parenthesize_if_pointer id) (camlint_of_coqint n))
+        t
+  | Tfunction(args, res) ->
+      let b = Buffer.create 20 in
+      if id = ""
+      then Buffer.add_string b "(*)"
+      else Buffer.add_string b (parenthesize_if_pointer id);
+      Buffer.add_char b '(';
+      begin match args with
+      | Tnil ->
+          Buffer.add_string b "void"
+      | _ ->
+          let rec add_args first = function
+          | Tnil -> ()
+          | Tcons(t1, tl) ->
+              if not first then Buffer.add_string b ", ";
+              Buffer.add_string b (name_cdecl "" t1);
+              add_args false tl in
+          add_args true args
+      end;
+      Buffer.add_char b ')';
+      name_cdecl (Buffer.contents b) res
+  | Tstruct(name, fld) ->
+      extern_atom name ^ name_optid id
+  | Tunion(name, fld) ->
+      extern_atom name ^ name_optid id
+  | Tcomp_ptr name ->
+      extern_atom name ^ " *" ^ id
+
+(* Type *)
+
+let rec stype ty =
+  match ty with
+  | Tvoid -> "Tvoid"
+  | Tint(sz, sg) -> "(Tint " ^ name_inttype sz sg ^ ")"
+  | Tfloat sz -> "(Tfloat " ^ name_floattype sz ^ ")"
+  | Tpointer t -> "(Tpointer " ^ stype t ^ ")"
+  | Tarray(t, n) -> "(Tarray " ^ stype t ^ " " ^ (Int32.to_string (camlint_of_coqint n)) ^ ")"
+  | Tfunction(args, res) -> "(Tfunction " ^ typelist args ^ " " ^ stype res ^ ")"
+  | Tstruct(name, fld) ->
+      fieldlist "(Tstruct (succ_pos_of_nat " name fld
+  | Tunion(name, fld) ->
+      fieldlist "(Tunion (succ_pos_of_nat " name fld
+  | Tcomp_ptr name ->
+      "(Tcomp_ptr (succ_pos_of_nat " ^ Int32.to_string (camlint_of_positive name) ^ "))"
+ and typelist l =
+    let b = Buffer.create 20 in
+      let rec add_types = function
+        | Tnil -> Buffer.add_string b "Tnil"
+        | Tcons(t1, tl) ->
+            Buffer.add_string b "(Tcons ";
+            Buffer.add_string b (stype t1);
+            Buffer.add_char b ' ';
+            add_types tl;
+            Buffer.add_char b ')'
+      in add_types l;
+        Buffer.contents b
+ and fieldlist s name l =
+    let b = Buffer.create 20 in
+      Buffer.add_string b s;
+      Buffer.add_string b (Int32.to_string (camlint_of_positive name));
+      Buffer.add_string b ") ";
+      let rec add_fields = function
+        | Fnil -> Buffer.add_string b "Fnil"
+        | Fcons(id, ty, tl) ->
+            Buffer.add_string b "(Fcons (succ_pos_of_nat ";
+            Buffer.add_string b (Int32.to_string (camlint_of_positive id));
+            Buffer.add_string b ") ";
+            Buffer.add_string b (stype ty);
+            Buffer.add_char b ' ';
+            add_fields tl;
+            Buffer.add_char b ')'
+      in add_fields l;
+        Buffer.add_char b ')';
+        Buffer.contents b
+
+let name_type ty = name_cdecl "" ty
+
+(* Expressions *)
+
+let rec print_expr p (Expr (eb, ty)) =
+  fprintf p "@[<hov 2>(Expr ";
+  begin
+  match eb with
+  | Econst_int n ->
+      fprintf p "(Econst_int (repr %ld))" (camlint_of_coqint n)
+  | Econst_float f ->
+      fprintf p "(Econst_float %F)" f
+  | Evar id ->
+      fprintf p "(Evar (succ_pos_of_nat %ld))" (camlint_of_positive id)
+  | Eunop(op, e1) ->
+      fprintf p "(Eunop %s %a)" (name_unop op) print_expr e1
+  | Ederef e ->
+      fprintf p "(Ederef@ %a)" print_expr e
+  | Eaddrof e ->
+      fprintf p "(Eaddrof@ %a)" print_expr e
+  | Ebinop(op, e1, e2) ->
+      fprintf p "(Ebinop@ %s@ %a@ %a)"
+                (name_binop op)
+                print_expr e1
+                print_expr e2
+  | Ecast(ty, e1) ->
+      fprintf p "(Ecast %s@ %a)"
+                (stype ty)
+                print_expr e1
+  | Econdition(e1, e2, e3) ->
+      fprintf p "(Econdition %a@ %a@ %a)"
+                print_expr e1
+                print_expr e2
+                print_expr e3
+  | Eandbool(e1, e2) ->
+      fprintf p "(Eandbool %a@ %a)"
+                print_expr e1
+                print_expr e2
+  | Eorbool(e1, e2) ->
+      fprintf p "(Eorbool %a@ %a)"
+                print_expr e1
+                print_expr e2
+  | Esizeof ty ->
+      fprintf p "(Esizeof %s)" (stype ty)
+  | Efield(e1, id) ->
+      fprintf p "(Efield %a (succ_pos_of_nat %li))" print_expr e1 (camlint_of_positive id)
+  end;
+  fprintf p " %s)@]" (stype ty)
+
+let rec print_expr_list p (first, el) =
+  match el with
+  | [] -> ()
+  | e1 :: et ->
+      if not first then fprintf p ",@ ";
+      print_expr p e1;
+      print_expr_list p (false, et)
+
+let rec print_stmt p s =
+  match s with
+  | Sskip ->
+      fprintf p "Sskip"
+  | Sassign(e1, e2) ->
+      fprintf p "@[<hv 2>(Sassign %a@ %a)@]" print_expr e1 print_expr e2
+  | Scall(None, e1, el) ->
+      fprintf p "@[<hv 2>(Scall (None ?) %a @[<hov 0>%a@])@]"
+                print_expr e1
+                (print_list print_expr) el
+  | Scall(Some lhs, e1, el) ->
+      fprintf p "@[<hv 2>(Scall (Some ? %a)@ %a@ @[<hov 0>%a@])@]"
+                print_expr lhs
+                print_expr e1
+                (print_list print_expr) el
+  | Ssequence(s1, s2) ->
+      fprintf p "(Ssequence@ %a@ %a)" print_stmt s1 print_stmt s2
+  | Sifthenelse(e, s1, s2) ->
+      fprintf p "@[<v 2>(Sifthenelse %a@ %a@ %a)@]"
+              print_expr e
+              print_stmt s1
+              print_stmt s2
+  | Swhile(e, s) ->
+      fprintf p "@[<v 2>(Swhile %a@ %a)@]"
+              print_expr e
+              print_stmt s
+  | Sdowhile(e, s) ->
+      fprintf p "@[<v 2>S(dowhile %a@ %a)@]"
+              print_expr e
+              print_stmt s
+  | Sfor(s_init, e, s_iter, s_body) ->
+      fprintf p "@[<v 2>(Sfor %a@ %a@ %a@\n%a@;<0 -2>)@]"
+              print_stmt s_init
+              print_expr e
+              print_stmt s_iter
+              print_stmt s_body
+  | Sbreak ->
+      fprintf p "Sbreak"
+  | Scontinue ->
+      fprintf p "Scontinue"
+  | Sswitch(e, cases) ->
+      fprintf p "@[<v 2>(Sswitch %a (@ %a@;<0 -2>))@]"
+              print_expr e
+              print_cases cases
+  | Sreturn None ->
+      fprintf p "(Sreturn (None ?))"
+  | Sreturn (Some e) ->
+      fprintf p "(Sreturn (Some ? %a))" print_expr e
+  | Slabel(lbl, s1) ->
+      fprintf p "(Slabel (succ_pos_of_nat %li)@ %a)" (camlint_of_positive lbl) print_stmt s1
+  | Sgoto lbl ->
+      fprintf p "(Sgoto (succ_pos_of_nat %li))" (camlint_of_positive lbl)
+
+and print_cases p cases =
+  match cases with
+  | LSdefault s ->
+      fprintf p "@[<v 2>LSdefault@ %a@]" print_stmt s
+  | LScase(lbl, s, rem) ->
+      fprintf p "@[<v 2>(LScase %ld:@ %a@ %a@]"
+              (camlint_of_coqint lbl)
+              print_stmt s
+              print_cases rem
+
+let name_function_parameters params =
+  let b = Buffer.create 20 in
+  Buffer.add_char b '[';
+    let rec add_params first = function
+      | [] -> ()
+      | Coq_pair(id, ty) :: rem ->
+          if not first then Buffer.add_string b "; ";
+          Buffer.add_string b "mk_pair ?? (succ_pos_of_nat ";
+          Buffer.add_string b (Int32.to_string (camlint_of_positive id));
+          Buffer.add_string b ") ";
+          Buffer.add_string b (stype ty);
+          add_params false rem in
+      add_params true params;
+      Buffer.add_char b ']';
+      Buffer.contents b
+
+let print_function p f =
+  fprintf p "@[<v 2>mk_function %s %s %s@ " (stype f.fn_return)
+    (name_function_parameters f.fn_params)
+    (name_function_parameters f.fn_vars);
+  print_stmt p f.fn_body;
+  fprintf p "@;<0 -2>@]@ @ "
+
+let print_fundef p (Coq_pair(id, fd)) =
+  fprintf p "@[<v 2>mk_pair ?? (succ_pos_of_nat %li) " (camlint_of_positive id);
+  match fd with
+  | External(id', args, res) ->
+      fprintf p "(External (succ_pos_of_nat %li) %s %s)@]" (camlint_of_positive id) (typelist args) (stype res)
+  | Internal f ->
+      fprintf p "(Internal (@ %a@;<0 -2>))@]" print_function f
+
+let string_of_init id =
+  let b = Buffer.create (List.length id) in
+  let add_init = function
+  | Init_int8 n ->
+      let c = Int32.to_int (camlint_of_coqint n) in
+      if c >= 32 && c <= 126 && c <> Char.code '\"' && c <> Char.code '\\'
+      then Buffer.add_char b (Char.chr c)
+      else Buffer.add_string b (Printf.sprintf "\\%03o" c)
+  | _ ->
+      assert false
+  in List.iter add_init id; Buffer.contents b
+
+let chop_last_nul id =
+  match List.rev id with
+  | Init_int8 BinInt.Z0 :: tl -> List.rev tl
+  | _ -> id
+
+let print_init p = function
+  | Init_int8 n -> fprintf p "(Init_int8 (repr %ld))@ " (camlint_of_coqint n)
+  | Init_int16 n -> fprintf p "(Init_int16 (repr %ld))@ " (camlint_of_coqint n)
+  | Init_int32 n -> fprintf p "(Init_int32 (repr %ld))@ " (camlint_of_coqint n)
+  | Init_float32 n -> fprintf p "(Init_float32 %F)@ " n
+  | Init_float64 n -> fprintf p "(Iinit_float64 %F)@ " n
+  | Init_space n -> fprintf p "(Init_space %ld)@ " (camlint_of_coqint n)
+  | Init_addrof(symb, ofs) -> fprintf p "(Init_addrof %ld (repr %ld))" (camlint_of_positive symb) (camlint_of_coqint ofs)
+
+let re_string_literal = Str.regexp "__stringlit_[0-9]+"
+
+let print_globvar p (Coq_pair(Coq_pair(id, init), ty)) =
+  fprintf p "@[<hov 2>(mk_pair ?? (mk_pair ?? (succ_pos_of_nat %li)@ %a)@ %s)@]"
+    (camlint_of_positive id)
+    (print_list print_init) init
+    (stype ty)
+
+(* Collect struct and union types *)
+
+let rec collect_type = function
+  | Tvoid -> ()
+  | Tint(sz, sg) -> ()
+  | Tfloat sz -> ()
+  | Tpointer t -> collect_type t
+  | Tarray(t, n) -> collect_type t
+  | Tfunction(args, res) -> collect_type_list args; collect_type res
+  | Tstruct(id, fld) -> register_struct_union id fld; collect_fields fld
+  | Tunion(id, fld) -> register_struct_union id fld; 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 (Expr(ed, ty)) =
+  match ed with
+  | Econst_int n -> ()
+  | Econst_float f -> ()
+  | Evar id -> ()
+  | Eunop(op, e1) -> collect_expr e1
+  | Ederef e -> collect_expr e
+  | Eaddrof e -> collect_expr e
+  | Ebinop(op, e1, e2) -> collect_expr e1; collect_expr e2
+  | Ecast(ty, e1) -> collect_type ty; collect_expr e1
+  | Econdition(e1, e2, e3) -> collect_expr e1; collect_expr e2; collect_expr e3
+  | Eandbool(e1, e2) -> collect_expr e1; collect_expr e2
+  | Eorbool(e1, e2) -> collect_expr e1; collect_expr e2
+  | Esizeof ty -> collect_type ty
+  | Efield(e1, id) -> collect_expr e1
+
+let rec collect_expr_list = function
+  | [] -> ()
+  | hd :: tl -> collect_expr hd; collect_expr_list tl
+
+let rec collect_stmt = function
+  | Sskip -> ()
+  | Sassign(e1, e2) -> collect_expr e1; collect_expr e2
+  | Scall(None, e1, el) -> collect_expr e1; collect_expr_list el
+  | Scall(Some lhs, e1, el) -> collect_expr lhs; collect_expr e1; collect_expr_list el
+  | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2
+  | Sifthenelse(e, s1, s2) -> collect_expr e; collect_stmt s1; collect_stmt s2
+  | Swhile(e, s) -> collect_expr e; collect_stmt s
+  | Sdowhile(e, s) -> collect_stmt s; collect_expr e
+  | Sfor(s_init, e, s_iter, s_body) ->
+      collect_stmt s_init; collect_expr e;
+      collect_stmt s_iter; collect_stmt s_body
+  | 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
+  | LSdefault s -> collect_stmt s
+  | LScase(lbl, s, rem) -> collect_stmt s; collect_cases rem
+
+let collect_function f =
+  collect_type f.fn_return;
+  List.iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_params;
+  List.iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_vars;
+  collect_stmt f.fn_body
+
+let collect_fundef (Coq_pair(id, fd)) =
+  match fd with
+  | External(_, args, res) -> collect_type_list args; collect_type res
+  | Internal f -> collect_function f
+
+let collect_globvar (Coq_pair(Coq_pair(id, init), ty)) =
+  collect_type ty
+
+let collect_program p =
+  List.iter collect_globvar p.prog_vars;
+  List.iter collect_fundef p.prog_funct
+
+let declare_struct_or_union p (name, fld) =
+  fprintf p "%s;@ @ " name
+
+let print_struct_or_union p (name, fld) =
+  fprintf p "@[<v 2>%s {" name;
+  let rec print_fields = function
+  | Fnil -> ()
+  | Fcons(id, ty, rem) ->
+      fprintf p "@ %s;" (name_cdecl (extern_atom id) ty);
+      print_fields rem in
+  print_fields fld;
+  fprintf p "@;<0 -2>};@]@ "
+
+let print_program p prog =
+  struct_unions := StructUnionSet.empty;
+  collect_program prog;
+  fprintf p "include \"Csyntax.ma\".@\n@\n";
+  fprintf p "@[<v 2>ndefinition myprog := mk_program fundef type@ ";
+(*  StructUnionSet.iter (declare_struct_or_union p) !struct_unions;
+  StructUnionSet.iter (print_struct_or_union p) !struct_unions;*)
+  print_list print_fundef p prog.prog_funct;
+  fprintf p "@\n(succ_pos_of_nat %li)@\n" (camlint_of_positive (Hashtbl.find atom_of_string "main"));
+  print_list print_globvar p prog.prog_vars;
+  fprintf p "@;<0 -2>.@]@."
+
+

driver/Clflags.ml

@@ -23 +23 @@
 let option_fmadd = ref false
 let option_dparse = ref false
 let option_dclight = ref false
+let option_dmatita = ref false
 let option_dasm = ref false
 let option_E = ref false
 let option_S = ref false

driver/Driver.ml

@@ -93 +93 @@
     PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax;
     close_out oc
   end;
+  (* Save program in matita syntax if requested *)
+  if !option_dmatita then begin
+    let ofile = sourcename ^ ".ma" in
+    let oc = open_out ofile in
+    PrintMatitaSyntax.print_program (Format.formatter_of_out_channel oc) csyntax;
+    close_out oc
+  end;
   (* Convert to Asm *)
   let ppc =
     match Compiler.transf_c_program csyntax with
@@ -227 +234 @@
 Tracing options:
   -dparse        Save C file after parsing and elaboration in <file>.parse.c
   -dclight       Save generated Clight in <file>.light.c
+  -dmatita       Save generated Clight as matita syntax in <file>.c.ma
   -dasm          Save generated assembly in <file>.s
 Linking options:
   -l<lib>        Link library <lib>
@@ -303 +311 @@
   "-stdlib$", String(fun s -> stdlib_path := s);
   "-dparse$", Set option_dparse;
   "-dclight$", Set option_dclight;
+  "-dmatita$", Set option_dmatita;
   "-dasm$", Set option_dasm;
   "-E$", Set option_E;
   "-S$", Set option_S;