From a15858a0a8fcea82db02fe8c9bd2ed912210419f Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 18 Aug 2010 09:06:55 +0000 Subject: Merge of branches/full-expr-4: - Csyntax, Csem: source C language has side-effects within expressions, performs implicit casts, and has nondeterministic reduction semantics for expressions - Cstrategy: deterministic red. sem. for the above - Clight: the previous source C language, with pure expressions. Added: temporary variables + implicit casts. - New pass SimplExpr to pull side-effects out of expressions (previously done in untrusted Caml code in cparser/) - Csharpminor: added temporary variables to match Clight. - Cminorgen: adapted, removed cast optimization (moved to back-end) - CastOptim: RTL-level optimization of casts - cparser: transformations Bitfields, StructByValue and StructAssign now work on non-simplified expressions - Added pretty-printers for several intermediate languages, and matching -dxxx command-line flags. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1467 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/PrintCminor.ml | 285 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 285 insertions(+) create mode 100644 backend/PrintCminor.ml (limited to 'backend/PrintCminor.ml') diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml new file mode 100644 index 0000000..6a74506 --- /dev/null +++ b/backend/PrintCminor.ml @@ -0,0 +1,285 @@ +(* *********************************************************************) +(* *) +(* 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 Cminor *) + +open Format +open Camlcoq +open Datatypes +open BinPos +open Integers +open AST +open Cminor + +(* Precedences and associativity -- like those of C *) + +type associativity = LtoR | RtoL | NA + +let rec precedence = function + | Evar _ -> (16, NA) + | Econst _ -> (16, NA) + | Eunop _ -> (15, RtoL) + | Ebinop((Omul|Odiv|Odivu|Omod|Omodu|Omulf|Odivf), _, _) -> (13, LtoR) + | Ebinop((Oadd|Osub|Oaddf|Osubf), _, _) -> (12, LtoR) + | Ebinop((Oshl|Oshr|Oshru), _, _) -> (11, LtoR) + | Ebinop((Ocmp _|Ocmpu _|Ocmpf _), _, _) -> (10, LtoR) + | Ebinop(Oand, _, _) -> (8, LtoR) + | Ebinop(Oxor, _, _) -> (7, LtoR) + | Ebinop(Oor, _, _) -> (6, LtoR) + | Eload _ -> (15, RtoL) + | Econdition _ -> (3, RtoL) + +(* Naming idents. We assume we run after Cminorgen, which encoded idents. *) + +let ident_name id = + match id with + | Coq_xO n -> extern_atom n + | Coq_xI n -> Printf.sprintf "$%ld" (camlint_of_positive n) + | Coq_xH -> "$0" + +(* Naming operators *) + +let name_of_unop = function + | Ocast8unsigned -> "int8u" + | Ocast8signed -> "int8s" + | Ocast16unsigned -> "int16u" + | Ocast16signed -> "int16s" + | Onegint -> "-" + | Onotbool -> "!" + | Onotint -> "~" + | Onegf -> "-f" + | Oabsf -> "absf" + | Osingleoffloat -> "float32" + | Ointoffloat -> "intoffloat" + | Ointuoffloat -> "intuoffloat" + | Ofloatofint -> "floatofint" + | Ofloatofintu -> "floatofintu" + +let comparison_name = function + | Ceq -> "==" + | Cne -> "!=" + | Clt -> "<" + | Cle -> "<=" + | Cgt -> ">" + | Cge -> ">=" + +let name_of_binop = function + | Oadd -> "+" + | Osub -> "-" + | Omul -> "*" + | Odiv -> "/" + | Odivu -> "/u" + | Omod -> "%" + | Omodu -> "%u" + | Oand -> "&" + | Oor -> "|" + | Oxor -> "^" + | Oshl -> "<<" + | Oshr -> ">>" + | Oshru -> ">>u" + | Oaddf -> "+f" + | Osubf -> "-f" + | Omulf -> "*f" + | Odivf -> "/f" + | Ocmp c -> comparison_name c + | Ocmpu c -> comparison_name c ^ "u" + | Ocmpf c -> comparison_name c ^ "f" + +let name_of_chunk = function + | Mint8signed -> "int8signed" + | Mint8unsigned -> "int8unsigned" + | Mint16signed -> "int16signed" + | Mint16unsigned -> "int16unsigned" + | Mint32 -> "int32" + | Mfloat32 -> "float32" + | Mfloat64 -> "float64" + +(* Expressions *) + +let rec expr p (prec, e) = + let (prec', assoc) = precedence e in + let (prec1, prec2) = + if assoc = LtoR + then (prec', prec' + 1) + else (prec' + 1, prec') in + if prec' < prec + then fprintf p "@[(" + else fprintf p "@["; + begin match e with + | Evar id -> + fprintf p "%s" (ident_name id) + | Econst(Ointconst n) -> + fprintf p "%ld" (camlint_of_coqint n) + | Econst(Ofloatconst f) -> + fprintf p "%F" f + | Econst(Oaddrsymbol(id, ofs)) -> + let ofs = camlint_of_coqint ofs in + if ofs = 0l + then fprintf p "\"%s\"" (extern_atom id) + else fprintf p "(\"%s\" + %ld)" (extern_atom id) ofs + | Econst(Oaddrstack n) -> + fprintf p "&%ld" (camlint_of_coqint n) + | Eunop(op, a1) -> + fprintf p "%s %a" (name_of_unop op) expr (prec', a1) + | Ebinop(op, a1, a2) -> + fprintf p "%a@ %s %a" + expr (prec1, a1) (name_of_binop op) expr (prec2, a2) + | Eload(chunk, a1) -> + fprintf p "%s[%a]" (name_of_chunk chunk) expr (0, a1) + | Econdition(a1, a2, a3) -> + fprintf p "%a@ ? %a@ : %a" expr (4, a1) expr (4, a2) expr (4, a3) + end; + if prec' < prec then fprintf p ")@]" else fprintf p "@]" + +let print_expr p e = expr p (0, e) + +let rec print_expr_list p (first, rl) = + match rl with + | [] -> () + | r :: rl -> + if not first then fprintf p ",@ "; + expr p (2, r); + print_expr_list p (false, rl) + +(* Types *) + +let name_of_type = function + | Tint -> "int" + | Tfloat -> "float" + +let rec print_sig p = function + | {sig_args = []; sig_res = None} -> fprintf p "void" + | {sig_args = []; sig_res = Some ty} -> fprintf p "%s" (name_of_type ty) + | {sig_args = t1 :: tl; sig_res = tres} -> + fprintf p "%s ->@ " (name_of_type t1); + print_sig p {sig_args = tl; sig_res = tres} + +(* Statements *) + +let rec print_stmt p s = + match s with + | Sskip -> + fprintf p "/*skip*/;" + | Sassign(id, e2) -> + fprintf p "@[%s =@ %a;@]" (ident_name id) print_expr e2 + | Sstore(chunk, a1, a2) -> + fprintf p "@[%s[%a] =@ %a;@]" + (name_of_chunk chunk) print_expr a1 print_expr a2 + | Scall(None, sg, e1, el) -> + fprintf p "@[%a@,(@[%a@])@ : @[%a@];@]" + print_expr e1 + print_expr_list (true, el) + print_sig sg + | Scall(Some id, sg, e1, el) -> + fprintf p "@[%s =@ %a@,(@[%a@]);@] : @[%a@]" + (ident_name id) + print_expr e1 + print_expr_list (true, el) + print_sig sg + | Stailcall(sg, e1, el) -> + fprintf p "@[tailcall %a@,(@[%a@])@ : @[%a@];@]" + print_expr e1 + print_expr_list (true, el) + print_sig sg + | Sseq(Sskip, s2) -> + print_stmt p s2 + | Sseq(s1, Sskip) -> + print_stmt p s1 + | Sseq(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, Sskip, s2) -> + fprintf p "@[if (! %a) {@ %a@;<0 -2>}@]" + expr (15, e) + print_stmt s2 + | Sifthenelse(e, s1, s2) -> + fprintf p "@[if (%a) {@ %a@;<0 -2>} else {@ %a@;<0 -2>}@]" + print_expr e + print_stmt s1 + print_stmt s2 + | Sloop(s) -> + fprintf p "@[loop {@ %a@;<0 -2>}@]" + print_stmt s + | Sblock(s) -> + fprintf p "@[{{ %a@;<0 -3>}}@]" + print_stmt s + | Sexit n -> + fprintf p "exit %d;" (camlint_of_nat n + 1) + | Sswitch(e, cases, dfl) -> + fprintf p "@[switch (%a) {" print_expr e; + List.iter + (fun (Coq_pair(n, x)) -> + fprintf p "@ case %ld: exit %d;\n" + (camlint_of_coqint n) (camlint_of_nat x)) + cases; + fprintf p "@ default: exit %d;\n" (camlint_of_nat dfl); + fprintf p "@;<0 -2>}@]" + | Sreturn None -> + fprintf p "return;" + | Sreturn (Some e) -> + fprintf p "return %a;" print_expr e + | Slabel(lbl, s1) -> + fprintf p "%s:@ %a" (extern_atom lbl) print_stmt s1 + | Sgoto lbl -> + fprintf p "goto %s;" (extern_atom lbl) + +(* Functions *) + +let rec print_varlist p (vars, first) = + match vars with + | [] -> () + | v1 :: vl -> + if not first then fprintf p ",@ "; + fprintf p "%s" (ident_name v1); + print_varlist p (vl, false) + +let print_function p id f = + fprintf p "@[\"%s\"(@[%a@])@ : @[%a@]@]@ " + (extern_atom id) + print_varlist (f.fn_params, true) + print_sig f.fn_sig; + fprintf p "@[{@ "; + let stksz = camlint_of_z f.fn_stackspace in + if stksz <> 0l then + fprintf p "stack %ld;@ " stksz; + if f.fn_vars <> [] then + fprintf p "var @[%a;@]@ " print_varlist (f.fn_vars, true); + print_stmt p f.fn_body; + fprintf p "@;<0 -2>}@]@ " + +let print_fundef p (Coq_pair(id, fd)) = + match fd with + | External ef -> + () (* Todo? *) + | Internal f -> + print_function p id f + +let print_program p prog = + fprintf p "@["; + List.iter (print_fundef p) prog.prog_funct; + fprintf p "@]@." + +let destination : string option ref = ref None + +let print_if prog = + match !destination with + | None -> () + | Some f -> + let oc = open_out f in + print_program (formatter_of_out_channel oc) prog; + close_out oc -- cgit v1.2.3