From 593ce3f7c5647e284cd2fdc3dd3ed41be9563982 Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 7 Sep 2006 15:30:24 +0000 Subject: Integration du front-end CIL developpe par Thomas Moniot git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@84 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- caml/PrintCsyntax.ml | 434 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 434 insertions(+) create mode 100644 caml/PrintCsyntax.ml (limited to 'caml/PrintCsyntax.ml') diff --git a/caml/PrintCsyntax.ml b/caml/PrintCsyntax.ml new file mode 100644 index 0000000..ff2af16 --- /dev/null +++ b/caml/PrintCsyntax.ml @@ -0,0 +1,434 @@ +(** Pretty-printer for Csyntax *) + +open Format +open Camlcoq +open CList +open Datatypes +open AST +open Csyntax + +let name_unop = function + | Onotbool -> "!" + | Onotint -> "~" + | Oneg -> "-" + + +let name_binop = function + | Oadd -> "+" + | Osub -> "-" + | Omul -> "*" + | Odiv -> "/" + | Omod -> "%" + | Oand -> "&" + | Oor -> "|" + | Oxor -> "^" + | Oshl -> "<<" + | Oshr -> ">>" + | Oeq -> "==" + | One -> "!=" + | Olt -> "<" + | Ogt -> ">" + | Ole -> "<=" + | Oge -> ">=" + +let name_inttype sz sg = + match sz, sg with + | I8, Signed -> "signed char" + | I8, Unsigned -> "unsigned char" + | I16, Signed -> "short" + | I16, Unsigned -> "unsigned short" + | I32, Signed -> "int" + | I32, Unsigned -> "unsigned int" + +let name_floattype sz = + match sz with + | F32 -> "float" + | F64 -> "double" + +(* Naming of structs and unions *) + +type su_kind = Struct | Union + +let struct_union_names = ref [] +let struct_union_name_counter = ref 0 + +let register_struct_union kind fld = + if not (List.mem_assoc (kind, fld) !struct_union_names) then begin + incr struct_union_name_counter; + let s = + match kind with + | Struct -> sprintf "s%d" !struct_union_name_counter + | Union -> sprintf "u%d" !struct_union_name_counter in + struct_union_names := ((kind, fld), s) :: !struct_union_names + end + +let struct_union_name kind fld = + try List.assoc (kind, fld) !struct_union_names with Not_found -> "" + +(* 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 '('; + 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; + Buffer.add_char b ')'; + name_cdecl (Buffer.contents b) res + | Tstruct fld -> + "struct " ^ struct_union_name Struct fld ^ name_optid id + | Tunion fld -> + "union " ^ struct_union_name Union fld ^ name_optid id + +(* Type *) + +let name_type ty = name_cdecl "" ty + +(* Expressions *) + +let parenthesis_level (Expr (e, ty)) = + match e with + | Econst_int _ -> 0 + | Econst_float _ -> 0 + | Evar _ -> 0 + | Eunop(_, _) -> 30 + | Ederef _ -> 20 + | Eaddrof _ -> 30 + | Ebinop(op, _, _) -> + begin match op with + | Oand | Oor | Oxor -> 75 + | Oeq | One | Olt | Ogt | Ole | Oge -> 70 + | Oadd | Osub | Oshl | Oshr -> 60 + | Omul | Odiv | Omod -> 40 + end + | Ecast _ -> 30 + | Eindex(_, _) -> 20 + | Ecall(_, _) -> 20 + | Eandbool(_, _) -> 80 + | Eorbool(_, _) -> 80 + | Esizeof _ -> 20 + | Efield _ -> 20 + +let rec print_expr p (Expr (eb, ty) as e) = + let level = parenthesis_level e in + match eb with + | Econst_int n -> + fprintf p "%ld" (camlint_of_coqint n) + | Econst_float f -> + fprintf p "%F" f + | Evar id -> + fprintf p "%s" (extern_atom id) + | Eunop(op, e1) -> + fprintf p "%s%a" (name_unop op) print_expr_prec (level, e1) + | Ederef e -> + fprintf p "*%a" print_expr_prec (level, e) + | Eaddrof e -> + fprintf p "&%a" print_expr_prec (level, e) + | Ebinop(op, e1, e2) -> + fprintf p "@[%a@ %s %a@]" + print_expr_prec (level, e1) + (name_binop op) + print_expr_prec (level, e2) + | Ecast(ty, e1) -> + fprintf p "@[(%s)@,%a@]" + (name_type ty) + print_expr_prec (level, e1) + | Eindex(e1, e2) -> + fprintf p "@[%a@,[%a]@]" + print_expr_prec (level, e1) + print_expr_prec (level, e2) + | Ecall(e1, el) -> + fprintf p "@[%a@,(@[%a@])@]" + print_expr_prec (level, e1) + print_expr_list (true, el) + | Eandbool(e1, e2) -> + fprintf p "@[%a@ && %a@]" + print_expr_prec (level, e1) + print_expr_prec (level, e2) + | Eorbool(e1, e2) -> + fprintf p "@[%a@ || %a@]" + print_expr_prec (level, e1) + print_expr_prec (level, e2) + | Esizeof ty -> + fprintf p "sizeof(%s)" (name_type ty) + | Efield(e1, id) -> + fprintf p "%a.%s" print_expr_prec (level, e1) (extern_atom id) + +and print_expr_prec p (context_prec, e) = + let this_prec = parenthesis_level e in + if this_prec >= context_prec + then fprintf p "(%a)" print_expr e + else print_expr p e + +and print_expr_list p (first, el) = + match el with + | Enil -> () + | Econs(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 "/*skip*/;" + | Sexpr e -> + fprintf p "%a;" print_expr e + | Sassign(e1, e2) -> + fprintf p "@[%a =@ %a;@]" print_expr e1 print_expr e2 + | Ssequence(s1, s2) -> + fprintf p "%a@ %a" print_stmt s1 print_stmt s2 + | Sifthenelse(e, s1, Sskip) -> + fprintf p "@[if (%a) {@ %a@;<0 -2>}@]" + print_expr e + print_stmt s1 + | Sifthenelse(e, s1, s2) -> + fprintf p "@[if (%a) {@ %a@;<0 -2>} else {@ %a@;<0 -2>}@]" + print_expr e + print_stmt s1 + print_stmt s2 + | Swhile(e, s) -> + fprintf p "@[while (%a) {@ %a@;<0 -2>}@]" + print_expr e + print_stmt s + | Sdowhile(e, s) -> + fprintf p "@[do {@ %a@;<0 -2>} while(%a);@]" + print_stmt s + print_expr e + | Sfor(s_init, e, s_iter, s_body) -> + fprintf p "@[for (@[%a;@ %a;@ %a) {@]@ %a@;<0 -2>}@]" + print_stmt_for s_init + print_expr e + print_stmt_for s_iter + print_stmt s_body + | Sbreak -> + fprintf p "break;" + | Scontinue -> + fprintf p "continue;" + | Sswitch(e, cases) -> + fprintf p "@[switch (%a) {@ %a@;<0 -2>}@]" + print_expr e + print_cases cases + | Sreturn None -> + fprintf p "return;" + | Sreturn (Some e) -> + fprintf p "return %a;" print_expr e + +and print_cases p cases = + match cases with + | LSdefault Sskip -> + () + | LSdefault s -> + fprintf p "@[default:@ %a@]" print_stmt s + | LScase(lbl, Sskip, rem) -> + fprintf p "case %ld:@ %a" + (camlint_of_coqint lbl) + print_cases rem + | LScase(lbl, s, rem) -> + fprintf p "@[case %ld:@ %a@]@ %a" + (camlint_of_coqint lbl) + print_stmt s + print_cases rem + +and print_stmt_for p s = + match s with + | Sskip -> + fprintf p "/*nothing*/" + | Sexpr e -> + fprintf p "%a" print_expr e + | Sassign(e1, e2) -> + fprintf p "%a = %a" print_expr e1 print_expr e2 + | Ssequence(s1, s2) -> + fprintf p "%a, %a" print_stmt_for s1 print_stmt_for s2 + | _ -> + fprintf p "" + +let name_function_parameters fun_name params = + let b = Buffer.create 20 in + Buffer.add_string b fun_name; + Buffer.add_char b '('; + let rec add_params first = function + | Coq_nil -> () + | Coq_cons(Coq_pair(id, ty), rem) -> + if not first then Buffer.add_string b ", "; + Buffer.add_string b (name_cdecl (extern_atom id) ty); + add_params false rem in + add_params true params; + Buffer.add_char b ')'; + Buffer.contents b + +let print_function p id f = + fprintf p "%s@ " + (name_cdecl (name_function_parameters (extern_atom id) + f.fn_params) + f.fn_return); + fprintf p "@[{@ "; + coqlist_iter + (fun (Coq_pair(id, ty)) -> + fprintf p "%s;@ " (name_cdecl (extern_atom id) ty)) + f.fn_vars; + print_stmt p f.fn_body; + fprintf p "@;<0 -2>}@]@ @ " + +let print_fundef p (Coq_pair(id, fd)) = + match fd with + | External(_, args, res) -> + fprintf p "extern %s;@ " + (name_cdecl (extern_atom id) (Tfunction(args, res))) + | Internal f -> + print_function p id f + +let print_init p = function + | Init_int8 n -> fprintf p "%ld,@ " (camlint_of_coqint n) + | Init_int16 n -> fprintf p "%ld,@ " (camlint_of_coqint n) + | Init_int32 n -> fprintf p "%ld,@ " (camlint_of_coqint n) + | Init_float32 n -> fprintf p "%F,@ " n + | Init_float64 n -> fprintf p "%F,@ " n + | Init_space n -> fprintf p "/* skip %ld*/@ " (camlint_of_coqint n) + +let print_globvar p (Coq_pair(Coq_pair(id, init), ty)) = + match init with + | Coq_nil -> + fprintf p "extern %s;@ " + (name_cdecl (extern_atom id) ty) + | Coq_cons(Init_space _, Coq_nil) -> + fprintf p "%s;@ " + (name_cdecl (extern_atom id) ty) + | _ -> + fprintf p "@[%s = {@ " + (name_cdecl (extern_atom id) ty); + coqlist_iter (print_init p) init; + fprintf p "};@]@ " + +(* 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 fld -> register_struct_union Struct fld; collect_fields fld + | Tunion fld -> register_struct_union Union fld; collect_fields fld + +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 + | Eindex(e1, e2) -> collect_expr e1; collect_expr e2 + | Ecall(e1, el) -> collect_expr e1; collect_expr_list el + | 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 + +and collect_expr_list = function + | Enil -> () + | Econs(hd, tl) -> collect_expr hd; collect_expr_list tl + +let rec collect_stmt = function + | Sskip -> () + | Sexpr e -> collect_expr e + | Sassign(e1, e2) -> collect_expr e1; collect_expr e2 + | 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 + +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; + coqlist_iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_params; + coqlist_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 = + coqlist_iter collect_globvar p.prog_vars; + coqlist_iter collect_fundef p.prog_funct + +let print_struct_or_union p ((kind, fld), name) = + fprintf p "@[%s %s{@ " + (match kind with Struct -> "struct" | Union -> "union") + 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_union_names := []; + struct_union_name_counter := 0; + collect_program prog; + fprintf p "@["; + List.iter (print_struct_or_union p) !struct_union_names; + fprintf p "@ "; + coqlist_iter (print_globvar p) prog.prog_vars; + fprintf p "@ "; + coqlist_iter (print_fundef p) prog.prog_funct; + fprintf p "@]@." + + -- cgit v1.2.3