source: src/Clight/compcert-1.7.1-matita.patch @ 1603

Last change on this file since 1603 was 11, checked in by campbell, 9 years ago

Fill in some axioms to aid executablity.
Implement global variable lookups and funtion returns.
Update compcert patch to use binary representation.

File size: 18.4 KB
  • cfrontend/PrintMatitaSyntax.ml

    diff -N '--exclude=Configuration.ml' '--exclude=test' '--exclude=runtime' '--exclude=*~' '--exclude=extraction' '--exclude=Makefile.config' '--exclude=ccomp' '--exclude=_build' '--exclude=*.vo' '--exclude=*.glob' -ur compcert-1.7.1/cfrontend/PrintMatitaSyntax.ml compcert-1.7.1-matitaout/cfrontend/PrintMatitaSyntax.ml
    old new  
     1(* *********************************************************************)
     2(*                                                                     *)
     3(*              The Compcert verified compiler                         *)
     4(*                                                                     *)
     5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
     6(*                                                                     *)
     7(*  Copyright Institut National de Recherche en Informatique et en     *)
     8(*  Automatique.  All rights reserved.  This file is distributed       *)
     9(*  under the terms of the GNU General Public License as published by  *)
     10(*  the Free Software Foundation, either version 2 of the License, or  *)
     11(*  (at your option) any later version.  This file is also distributed *)
     12(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
     13(*                                                                     *)
     14(* *********************************************************************)
     15
     16(** Pretty-printer for Csyntax *)
     17
     18open Format
     19open Camlcoq
     20open Datatypes
     21open AST
     22open Csyntax
     23
     24let print_list f fmt l =
     25  let rec aux fmt = function
     26      | [] -> ()
     27      | [x] -> f fmt x
     28      | h::t -> f fmt h; fprintf fmt ";@ "; aux fmt t
     29  in
     30  fprintf fmt "@[[%a]@]" aux l
     31
     32let name_unop = function
     33  | Onotbool -> "Onotbool"
     34  | Onotint  -> "Onotint"
     35  | Oneg     -> "Oneg"
     36
     37
     38let name_binop = function
     39  | Oadd -> "Oadd"
     40  | Osub -> "Osub"
     41  | Omul -> "Omul"
     42  | Odiv -> "Odiv"
     43  | Omod -> "Omod"
     44  | Oand -> "Oand"
     45  | Oor  -> "Oor"
     46  | Oxor -> "Oxor"
     47  | Oshl -> "Oshl"
     48  | Oshr -> "Oshr"
     49  | Oeq  -> "Oeq"
     50  | One  -> "One"
     51  | Olt  -> "Olt"
     52  | Ogt  -> "Ogt"
     53  | Ole  -> "Ole"
     54  | Oge  -> "Oge"
     55
     56let name_inttype sz sg =
     57  match sz, sg with
     58  | I8, Signed    -> "I8 Signed   "
     59  | I8, Unsigned  -> "I8 Unsigned "
     60  | I16, Signed   -> "I16 Signed  "
     61  | I16, Unsigned -> "I16 Unsigned"
     62  | I32, Signed   -> "I32 Signed  "
     63  | I32, Unsigned -> "I32 Unsigned"
     64
     65let name_floattype sz =
     66  match sz with
     67  | F32 -> "F32"
     68  | F64 -> "F64"
     69
     70(* Collecting the names and fields of structs and unions *)
     71
     72module StructUnionSet = Set.Make(struct
     73  type t = string * fieldlist
     74  let compare (n1, _ : t) (n2, _ : t) = compare n1 n2
     75end)
     76
     77let struct_unions = ref StructUnionSet.empty
     78
     79let register_struct_union id fld =
     80  struct_unions := StructUnionSet.add (extern_atom id, fld) !struct_unions
     81
     82(* Declarator (identifier + type) *)
     83
     84let name_optid id =
     85  if id = "" then "" else " " ^ id
     86
     87let parenthesize_if_pointer id =
     88  if String.length id > 0 && id.[0] = '*' then "(" ^ id ^ ")" else id
     89
     90let rec name_cdecl id ty =
     91  match ty with
     92  | Tvoid ->
     93      "void" ^ name_optid id
     94  | Tint(sz, sg) ->
     95      name_inttype sz sg ^ name_optid id
     96  | Tfloat sz ->
     97      name_floattype sz ^ name_optid id
     98  | Tpointer t ->
     99      name_cdecl ("*" ^ id) t
     100  | Tarray(t, n) ->
     101      name_cdecl
     102        (sprintf "%s[%ld]" (parenthesize_if_pointer id) (camlint_of_coqint n))
     103        t
     104  | Tfunction(args, res) ->
     105      let b = Buffer.create 20 in
     106      if id = ""
     107      then Buffer.add_string b "(*)"
     108      else Buffer.add_string b (parenthesize_if_pointer id);
     109      Buffer.add_char b '(';
     110      begin match args with
     111      | Tnil ->
     112          Buffer.add_string b "void"
     113      | _ ->
     114          let rec add_args first = function
     115          | Tnil -> ()
     116          | Tcons(t1, tl) ->
     117              if not first then Buffer.add_string b ", ";
     118              Buffer.add_string b (name_cdecl "" t1);
     119              add_args false tl in
     120          add_args true args
     121      end;
     122      Buffer.add_char b ')';
     123      name_cdecl (Buffer.contents b) res
     124  | Tstruct(name, fld) ->
     125      extern_atom name ^ name_optid id
     126  | Tunion(name, fld) ->
     127      extern_atom name ^ name_optid id
     128  | Tcomp_ptr name ->
     129      extern_atom name ^ " *" ^ id
     130
     131(* Type *)
     132
     133let rec stype ty =
     134  match ty with
     135  | Tvoid -> "Tvoid"
     136  | Tint(sz, sg) -> "(Tint " ^ name_inttype sz sg ^ ")"
     137  | Tfloat sz -> "(Tfloat " ^ name_floattype sz ^ ")"
     138  | Tpointer t -> "(Tpointer " ^ stype t ^ ")"
     139  | Tarray(t, n) -> "(Tarray " ^ stype t ^ " " ^ (Int32.to_string (camlint_of_coqint n)) ^ ")"
     140  | Tfunction(args, res) -> "(Tfunction " ^ typelist args ^ " " ^ stype res ^ ")"
     141  | Tstruct(name, fld) ->
     142      fieldlist "(Tstruct (succ_pos_of_nat " name fld
     143  | Tunion(name, fld) ->
     144      fieldlist "(Tunion (succ_pos_of_nat " name fld
     145  | Tcomp_ptr name ->
     146      "(Tcomp_ptr (succ_pos_of_nat " ^ Int32.to_string (camlint_of_positive name) ^ "))"
     147 and typelist l =
     148    let b = Buffer.create 20 in
     149      let rec add_types = function
     150        | Tnil -> Buffer.add_string b "Tnil"
     151        | Tcons(t1, tl) ->
     152            Buffer.add_string b "(Tcons ";
     153            Buffer.add_string b (stype t1);
     154            Buffer.add_char b ' ';
     155            add_types tl;
     156            Buffer.add_char b ')'
     157      in add_types l;
     158        Buffer.contents b
     159 and fieldlist s name l =
     160    let b = Buffer.create 20 in
     161      Buffer.add_string b s;
     162      Buffer.add_string b (Int32.to_string (camlint_of_positive name));
     163      Buffer.add_string b ") ";
     164      let rec add_fields = function
     165        | Fnil -> Buffer.add_string b "Fnil"
     166        | Fcons(id, ty, tl) ->
     167            Buffer.add_string b "(Fcons (succ_pos_of_nat ";
     168            Buffer.add_string b (Int32.to_string (camlint_of_positive id));
     169            Buffer.add_string b ") ";
     170            Buffer.add_string b (stype ty);
     171            Buffer.add_char b ' ';
     172            add_fields tl;
     173            Buffer.add_char b ')'
     174      in add_fields l;
     175        Buffer.add_char b ')';
     176        Buffer.contents b
     177
     178let name_type ty = name_cdecl "" ty
     179
     180(* Expressions *)
     181
     182let rec print_expr p (Expr (eb, ty)) =
     183  fprintf p "@[<hov 2>(Expr ";
     184  begin
     185  match eb with
     186  | Econst_int n ->
     187      fprintf p "(Econst_int (repr %ld))" (camlint_of_coqint n)
     188  | Econst_float f ->
     189      fprintf p "(Econst_float %F)" f
     190  | Evar id ->
     191      fprintf p "(Evar (succ_pos_of_nat %ld))" (camlint_of_positive id)
     192  | Eunop(op, e1) ->
     193      fprintf p "(Eunop %s %a)" (name_unop op) print_expr e1
     194  | Ederef e ->
     195      fprintf p "(Ederef@ %a)" print_expr e
     196  | Eaddrof e ->
     197      fprintf p "(Eaddrof@ %a)" print_expr e
     198  | Ebinop(op, e1, e2) ->
     199      fprintf p "(Ebinop@ %s@ %a@ %a)"
     200                (name_binop op)
     201                print_expr e1
     202                print_expr e2
     203  | Ecast(ty, e1) ->
     204      fprintf p "(Ecast %s@ %a)"
     205                (stype ty)
     206                print_expr e1
     207  | Econdition(e1, e2, e3) ->
     208      fprintf p "(Econdition %a@ %a@ %a)"
     209                print_expr e1
     210                print_expr e2
     211                print_expr e3
     212  | Eandbool(e1, e2) ->
     213      fprintf p "(Eandbool %a@ %a)"
     214                print_expr e1
     215                print_expr e2
     216  | Eorbool(e1, e2) ->
     217      fprintf p "(Eorbool %a@ %a)"
     218                print_expr e1
     219                print_expr e2
     220  | Esizeof ty ->
     221      fprintf p "(Esizeof %s)" (stype ty)
     222  | Efield(e1, id) ->
     223      fprintf p "(Efield %a (succ_pos_of_nat %li))" print_expr e1 (camlint_of_positive id)
     224  end;
     225  fprintf p " %s)@]" (stype ty)
     226
     227let rec print_expr_list p (first, el) =
     228  match el with
     229  | [] -> ()
     230  | e1 :: et ->
     231      if not first then fprintf p ",@ ";
     232      print_expr p e1;
     233      print_expr_list p (false, et)
     234
     235let rec print_stmt p s =
     236  match s with
     237  | Sskip ->
     238      fprintf p "Sskip"
     239  | Sassign(e1, e2) ->
     240      fprintf p "@[<hv 2>(Sassign %a@ %a)@]" print_expr e1 print_expr e2
     241  | Scall(None, e1, el) ->
     242      fprintf p "@[<hv 2>(Scall (None ?) %a @[<hov 0>%a@])@]"
     243                print_expr e1
     244                (print_list print_expr) el
     245  | Scall(Some lhs, e1, el) ->
     246      fprintf p "@[<hv 2>(Scall (Some ? %a)@ %a@ @[<hov 0>%a@])@]"
     247                print_expr lhs
     248                print_expr e1
     249                (print_list print_expr) el
     250  | Ssequence(s1, s2) ->
     251      fprintf p "(Ssequence@ %a@ %a)" print_stmt s1 print_stmt s2
     252  | Sifthenelse(e, s1, s2) ->
     253      fprintf p "@[<v 2>(Sifthenelse %a@ %a@ %a)@]"
     254              print_expr e
     255              print_stmt s1
     256              print_stmt s2
     257  | Swhile(e, s) ->
     258      fprintf p "@[<v 2>(Swhile %a@ %a)@]"
     259              print_expr e
     260              print_stmt s
     261  | Sdowhile(e, s) ->
     262      fprintf p "@[<v 2>S(dowhile %a@ %a)@]"
     263              print_expr e
     264              print_stmt s
     265  | Sfor(s_init, e, s_iter, s_body) ->
     266      fprintf p "@[<v 2>(Sfor %a@ %a@ %a@\n%a@;<0 -2>)@]"
     267              print_stmt s_init
     268              print_expr e
     269              print_stmt s_iter
     270              print_stmt s_body
     271  | Sbreak ->
     272      fprintf p "Sbreak"
     273  | Scontinue ->
     274      fprintf p "Scontinue"
     275  | Sswitch(e, cases) ->
     276      fprintf p "@[<v 2>(Sswitch %a (@ %a@;<0 -2>))@]"
     277              print_expr e
     278              print_cases cases
     279  | Sreturn None ->
     280      fprintf p "(Sreturn (None ?))"
     281  | Sreturn (Some e) ->
     282      fprintf p "(Sreturn (Some ? %a))" print_expr e
     283  | Slabel(lbl, s1) ->
     284      fprintf p "(Slabel (succ_pos_of_nat %li)@ %a)" (camlint_of_positive lbl) print_stmt s1
     285  | Sgoto lbl ->
     286      fprintf p "(Sgoto (succ_pos_of_nat %li))" (camlint_of_positive lbl)
     287
     288and print_cases p cases =
     289  match cases with
     290  | LSdefault s ->
     291      fprintf p "@[<v 2>LSdefault@ %a@]" print_stmt s
     292  | LScase(lbl, s, rem) ->
     293      fprintf p "@[<v 2>(LScase %ld:@ %a@ %a@]"
     294              (camlint_of_coqint lbl)
     295              print_stmt s
     296              print_cases rem
     297
     298let name_function_parameters params =
     299  let b = Buffer.create 20 in
     300  Buffer.add_char b '[';
     301    let rec add_params first = function
     302      | [] -> ()
     303      | Coq_pair(id, ty) :: rem ->
     304          if not first then Buffer.add_string b "; ";
     305          Buffer.add_string b "mk_pair ?? (succ_pos_of_nat ";
     306          Buffer.add_string b (Int32.to_string (camlint_of_positive id));
     307          Buffer.add_string b ") ";
     308          Buffer.add_string b (stype ty);
     309          add_params false rem in
     310      add_params true params;
     311      Buffer.add_char b ']';
     312      Buffer.contents b
     313
     314let print_function p f =
     315  fprintf p "@[<v 2>mk_function %s %s %s@ " (stype f.fn_return)
     316    (name_function_parameters f.fn_params)
     317    (name_function_parameters f.fn_vars);
     318  print_stmt p f.fn_body;
     319  fprintf p "@;<0 -2>@]@ @ "
     320
     321let print_fundef p (Coq_pair(id, fd)) =
     322  fprintf p "@[<v 2>mk_pair ?? (succ_pos_of_nat %li) " (camlint_of_positive id);
     323  match fd with
     324  | External(id', args, res) ->
     325      fprintf p "(External (succ_pos_of_nat %li) %s %s)@]" (camlint_of_positive id) (typelist args) (stype res)
     326  | Internal f ->
     327      fprintf p "(Internal (@ %a@;<0 -2>))@]" print_function f
     328
     329let string_of_init id =
     330  let b = Buffer.create (List.length id) in
     331  let add_init = function
     332  | Init_int8 n ->
     333      let c = Int32.to_int (camlint_of_coqint n) in
     334      if c >= 32 && c <= 126 && c <> Char.code '\"' && c <> Char.code '\\'
     335      then Buffer.add_char b (Char.chr c)
     336      else Buffer.add_string b (Printf.sprintf "\\%03o" c)
     337  | _ ->
     338      assert false
     339  in List.iter add_init id; Buffer.contents b
     340
     341let chop_last_nul id =
     342  match List.rev id with
     343  | Init_int8 BinInt.Z0 :: tl -> List.rev tl
     344  | _ -> id
     345
     346let print_init p = function
     347  | Init_int8 n -> fprintf p "(Init_int8 (repr %ld))@ " (camlint_of_coqint n)
     348  | Init_int16 n -> fprintf p "(Init_int16 (repr %ld))@ " (camlint_of_coqint n)
     349  | Init_int32 n -> fprintf p "(Init_int32 (repr %ld))@ " (camlint_of_coqint n)
     350  | Init_float32 n -> fprintf p "(Init_float32 %F)@ " n
     351  | Init_float64 n -> fprintf p "(Iinit_float64 %F)@ " n
     352  | Init_space n -> fprintf p "(Init_space %ld)@ " (camlint_of_coqint n)
     353  | Init_addrof(symb, ofs) -> fprintf p "(Init_addrof %ld (repr %ld))" (camlint_of_positive symb) (camlint_of_coqint ofs)
     354
     355let re_string_literal = Str.regexp "__stringlit_[0-9]+"
     356
     357let print_globvar p (Coq_pair(Coq_pair(id, init), ty)) =
     358  fprintf p "@[<hov 2>(mk_pair ?? (mk_pair ?? (succ_pos_of_nat %li)@ %a)@ %s)@]"
     359    (camlint_of_positive id)
     360    (print_list print_init) init
     361    (stype ty)
     362
     363(* Collect struct and union types *)
     364
     365let rec collect_type = function
     366  | Tvoid -> ()
     367  | Tint(sz, sg) -> ()
     368  | Tfloat sz -> ()
     369  | Tpointer t -> collect_type t
     370  | Tarray(t, n) -> collect_type t
     371  | Tfunction(args, res) -> collect_type_list args; collect_type res
     372  | Tstruct(id, fld) -> register_struct_union id fld; collect_fields fld
     373  | Tunion(id, fld) -> register_struct_union id fld; collect_fields fld
     374  | Tcomp_ptr _ -> ()
     375
     376and collect_type_list = function
     377  | Tnil -> ()
     378  | Tcons(hd, tl) -> collect_type hd; collect_type_list tl
     379
     380and collect_fields = function
     381  | Fnil -> ()
     382  | Fcons(id, hd, tl) -> collect_type hd; collect_fields tl
     383
     384let rec collect_expr (Expr(ed, ty)) =
     385  match ed with
     386  | Econst_int n -> ()
     387  | Econst_float f -> ()
     388  | Evar id -> ()
     389  | Eunop(op, e1) -> collect_expr e1
     390  | Ederef e -> collect_expr e
     391  | Eaddrof e -> collect_expr e
     392  | Ebinop(op, e1, e2) -> collect_expr e1; collect_expr e2
     393  | Ecast(ty, e1) -> collect_type ty; collect_expr e1
     394  | Econdition(e1, e2, e3) -> collect_expr e1; collect_expr e2; collect_expr e3
     395  | Eandbool(e1, e2) -> collect_expr e1; collect_expr e2
     396  | Eorbool(e1, e2) -> collect_expr e1; collect_expr e2
     397  | Esizeof ty -> collect_type ty
     398  | Efield(e1, id) -> collect_expr e1
     399
     400let rec collect_expr_list = function
     401  | [] -> ()
     402  | hd :: tl -> collect_expr hd; collect_expr_list tl
     403
     404let rec collect_stmt = function
     405  | Sskip -> ()
     406  | Sassign(e1, e2) -> collect_expr e1; collect_expr e2
     407  | Scall(None, e1, el) -> collect_expr e1; collect_expr_list el
     408  | Scall(Some lhs, e1, el) -> collect_expr lhs; collect_expr e1; collect_expr_list el
     409  | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2
     410  | Sifthenelse(e, s1, s2) -> collect_expr e; collect_stmt s1; collect_stmt s2
     411  | Swhile(e, s) -> collect_expr e; collect_stmt s
     412  | Sdowhile(e, s) -> collect_stmt s; collect_expr e
     413  | Sfor(s_init, e, s_iter, s_body) ->
     414      collect_stmt s_init; collect_expr e;
     415      collect_stmt s_iter; collect_stmt s_body
     416  | Sbreak -> ()
     417  | Scontinue -> ()
     418  | Sswitch(e, cases) -> collect_expr e; collect_cases cases
     419  | Sreturn None -> ()
     420  | Sreturn (Some e) -> collect_expr e
     421  | Slabel(lbl, s) -> collect_stmt s
     422  | Sgoto lbl -> ()
     423
     424and collect_cases = function
     425  | LSdefault s -> collect_stmt s
     426  | LScase(lbl, s, rem) -> collect_stmt s; collect_cases rem
     427
     428let collect_function f =
     429  collect_type f.fn_return;
     430  List.iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_params;
     431  List.iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_vars;
     432  collect_stmt f.fn_body
     433
     434let collect_fundef (Coq_pair(id, fd)) =
     435  match fd with
     436  | External(_, args, res) -> collect_type_list args; collect_type res
     437  | Internal f -> collect_function f
     438
     439let collect_globvar (Coq_pair(Coq_pair(id, init), ty)) =
     440  collect_type ty
     441
     442let collect_program p =
     443  List.iter collect_globvar p.prog_vars;
     444  List.iter collect_fundef p.prog_funct
     445
     446let declare_struct_or_union p (name, fld) =
     447  fprintf p "%s;@ @ " name
     448
     449let print_struct_or_union p (name, fld) =
     450  fprintf p "@[<v 2>%s {" name;
     451  let rec print_fields = function
     452  | Fnil -> ()
     453  | Fcons(id, ty, rem) ->
     454      fprintf p "@ %s;" (name_cdecl (extern_atom id) ty);
     455      print_fields rem in
     456  print_fields fld;
     457  fprintf p "@;<0 -2>};@]@ "
     458
     459let print_program p prog =
     460  struct_unions := StructUnionSet.empty;
     461  collect_program prog;
     462  fprintf p "include \"Csyntax.ma\".@\n@\n";
     463  fprintf p "@[<v 2>ndefinition myprog := mk_program fundef type@ ";
     464(*  StructUnionSet.iter (declare_struct_or_union p) !struct_unions;
     465  StructUnionSet.iter (print_struct_or_union p) !struct_unions;*)
     466  print_list print_fundef p prog.prog_funct;
     467  fprintf p "@\n(succ_pos_of_nat %li)@\n" (camlint_of_positive (Hashtbl.find atom_of_string "main"));
     468  print_list print_globvar p prog.prog_vars;
     469  fprintf p "@;<0 -2>.@]@."
     470
     471
  • driver/Clflags.ml

    diff -N '--exclude=Configuration.ml' '--exclude=test' '--exclude=runtime' '--exclude=*~' '--exclude=extraction' '--exclude=Makefile.config' '--exclude=ccomp' '--exclude=_build' '--exclude=*.vo' '--exclude=*.glob' -ur compcert-1.7.1/driver/Clflags.ml compcert-1.7.1-matitaout/driver/Clflags.ml
    old new  
    2323let option_fmadd = ref false
    2424let option_dparse = ref false
    2525let option_dclight = ref false
     26let option_dmatita = ref false
    2627let option_dasm = ref false
    2728let option_E = ref false
    2829let option_S = ref false
  • driver/Driver.ml

    diff -N '--exclude=Configuration.ml' '--exclude=test' '--exclude=runtime' '--exclude=*~' '--exclude=extraction' '--exclude=Makefile.config' '--exclude=ccomp' '--exclude=_build' '--exclude=*.vo' '--exclude=*.glob' -ur compcert-1.7.1/driver/Driver.ml compcert-1.7.1-matitaout/driver/Driver.ml
    old new  
    9393    PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax;
    9494    close_out oc
    9595  end;
     96  (* Save program in matita syntax if requested *)
     97  if !option_dmatita then begin
     98    let ofile = sourcename ^ ".ma" in
     99    let oc = open_out ofile in
     100    PrintMatitaSyntax.print_program (Format.formatter_of_out_channel oc) csyntax;
     101    close_out oc
     102  end;
    96103  (* Convert to Asm *)
    97104  let ppc =
    98105    match Compiler.transf_c_program csyntax with
     
    227234Tracing options:
    228235  -dparse        Save C file after parsing and elaboration in <file>.parse.c
    229236  -dclight       Save generated Clight in <file>.light.c
     237  -dmatita       Save generated Clight as matita syntax in <file>.c.ma
    230238  -dasm          Save generated assembly in <file>.s
    231239Linking options:
    232240  -l<lib>        Link library <lib>
     
    303311  "-stdlib$", String(fun s -> stdlib_path := s);
    304312  "-dparse$", Set option_dparse;
    305313  "-dclight$", Set option_dclight;
     314  "-dmatita$", Set option_dmatita;
    306315  "-dasm$", Set option_dasm;
    307316  "-E$", Set option_E;
    308317  "-S$", Set option_S;
Note: See TracBrowser for help on using the repository browser.