source: Deliverables/D3.1/C-semantics/compcert-1.7.1-matita.patch @ 502

Last change on this file since 502 was 11, checked in by campbell, 10 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.