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 --- cfrontend/PrintCsyntax.ml | 256 ++++++++++++++++++++++++---------------------- 1 file changed, 131 insertions(+), 125 deletions(-) (limited to 'cfrontend/PrintCsyntax.ml') diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 3b5dbc53..61599cff 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -18,6 +18,7 @@ open Format open Camlcoq open Datatypes +open Values open AST open Csyntax @@ -25,7 +26,6 @@ let name_unop = function | Onotbool -> "!" | Onotint -> "~" | Oneg -> "-" - | Ofabs -> "__builtin_fabs" let name_binop = function | Oadd -> "+" @@ -124,108 +124,112 @@ let rec name_cdecl id ty = let name_type ty = name_cdecl "" ty +(* Precedences and associativity (H&S section 7.2) *) + +type associativity = LtoR | RtoL | NA + +let rec precedence = function + | Eloc _ -> assert false + | Evar _ -> (16, NA) + | Ederef _ -> (15, RtoL) + | Efield _ -> (16, LtoR) + | Eval _ -> (16, NA) + | Evalof(l, _) -> precedence l + | Esizeof _ -> (15, RtoL) + | Ecall _ -> (16, LtoR) + | Epostincr _ -> (16, LtoR) + | Eunop _ -> (15, RtoL) + | Eaddrof _ -> (15, RtoL) + | Ecast _ -> (14, RtoL) + | Ebinop((Omul|Odiv|Omod), _, _, _) -> (13, LtoR) + | Ebinop((Oadd|Osub), _, _, _) -> (12, LtoR) + | Ebinop((Oshl|Oshr), _, _, _) -> (11, LtoR) + | Ebinop((Olt|Ogt|Ole|Oge), _, _, _) -> (10, LtoR) + | Ebinop((Oeq|One), _, _, _) -> (9, LtoR) + | Ebinop(Oand, _, _, _) -> (8, LtoR) + | Ebinop(Oxor, _, _, _) -> (7, LtoR) + | Ebinop(Oor, _, _, _) -> (6, LtoR) + | Econdition _ -> (3, RtoL) + | Eassign _ -> (2, RtoL) + | Eassignop _ -> (2, RtoL) + | Ecomma _ -> (1, LtoR) + | Eparen _ -> assert false + (* Expressions *) -let parenthesis_level (Expr (e, ty)) = - match e with - | Econst_int _ -> 0 - | Econst_float _ -> 0 - | Evar _ -> 0 - | Eunop(Ofabs, _) -> -10 (* force parentheses around argument *) - | 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 - | Econdition(_, _, _) -> 80 - | 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 -> +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 + | Eloc _ -> + assert false + | Evar(id, _) -> + fprintf p "%s" (extern_atom id) + | Ederef(a1, _) -> + fprintf p "*%a" expr (prec', a1) + | Efield(a1, f, _) -> + fprintf p "%a.%s" expr (prec', a1) (extern_atom f) + | Evalof(l, _) -> + expr p (prec, l) + | Eval(Vint n, _) -> fprintf p "%ld" (camlint_of_coqint n) - | Econst_float f -> + | Eval(Vfloat 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 (Expr (Ebinop(Oadd, e1, e2), _)) -> - fprintf p "@[%a@,[%a]@]" - print_expr_prec (level, e1) - print_expr_prec (level, e2) - | Ederef (Expr (Efield(e1, id), _)) -> - fprintf p "%a->%s" print_expr_prec (level, e1) (extern_atom id) - | 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) - | Econdition(e1, e2, e3) -> - fprintf p "@[%a@ ? %a@ : %a@]" - print_expr_prec (level, e1) - print_expr_prec (level, e2) - print_expr_prec (level, e3) - | 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 -> + | Eval(_, _) -> + assert false + | 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 - -let rec print_expr_list p (first, el) = - match el with - | [] -> () - | e1 :: et -> + | Eunop(op, a1, _) -> + fprintf p "%s%a" (name_unop op) expr (prec', a1) + | Eaddrof(a1, _) -> + fprintf p "&%a" expr (prec', a1) + | Epostincr(id, a1, _) -> + fprintf p "%a%s" expr (prec', a1) + (match id with Incr -> "++" | Decr -> "--") + | Ebinop(op, a1, a2, _) -> + fprintf p "%a@ %s %a" + expr (prec1, a1) (name_binop op) expr (prec2, a2) + | Ecast(a1, ty) -> + fprintf p "(%s) %a" (name_type ty) expr (prec', a1) + | Eassign(a1, a2, _) -> + fprintf p "%a =@ %a" expr (prec1, a1) expr (prec2, a2) + | Eassignop(op, a1, a2, _, _) -> + fprintf p "%a %s=@ %a" expr (prec1, a1) (name_binop op) expr (prec2, a2) + | Econdition(a1, a2, a3, _) -> + fprintf p "%a@ ? %a@ : %a" expr (4, a1) expr (4, a2) expr (4, a3) + | Ecomma(a1, a2, _) -> + fprintf p "%a,@ %a" expr (prec1, a1) expr (prec2, a2) + | Ecall(a1, al, _) -> + fprintf p "%a@[(%a)@]" expr (prec', a1) exprlist (true, al) + | Eparen _ -> + assert false + end; + if prec' < prec then fprintf p ")@]" else fprintf p "@]" + +and exprlist p (first, rl) = + match rl with + | Enil -> () + | Econs(r, rl) -> if not first then fprintf p ",@ "; - print_expr p e1; - print_expr_list p (false, et) + expr p (2, r); + exprlist p (false, rl) + +let print_expr p e = expr p (0, e) + +(* Statements *) let rec print_stmt p s = match s with | Sskip -> fprintf p "/*skip*/;" - | Sassign(e1, e2) -> - fprintf p "@[%a =@ %a;@]" print_expr e1 print_expr e2 - | Scall(None, e1, el) -> - fprintf p "@[%a@,(@[%a@]);@]" - print_expr e1 - print_expr_list (true, el) - | Scall(Some lhs, e1, el) -> - fprintf p "@[%a =@ %a@,(@[%a@]);@]" - print_expr lhs - print_expr e1 - print_expr_list (true, el) + | Sdo e -> + fprintf p "%a;" print_expr e | Ssequence(s1, s2) -> fprintf p "%a@ %a" print_stmt s1 print_stmt s2 | Sifthenelse(e, s1, Sskip) -> @@ -288,19 +292,10 @@ and print_stmt_for p s = match s with | Sskip -> fprintf p "/*nothing*/" - | Sassign(e1, e2) -> - fprintf p "%a = %a" print_expr e1 print_expr e2 + | Sdo e -> + print_expr p e | Ssequence(s1, s2) -> fprintf p "%a, %a" print_stmt_for s1 print_stmt_for s2 - | Scall(None, e1, el) -> - fprintf p "@[%a@,(@[%a@])@]" - print_expr e1 - print_expr_list (true, el) - | Scall(Some lhs, e1, el) -> - fprintf p "@[%a =@ %a@,(@[%a@])@]" - print_expr lhs - print_expr e1 - print_expr_list (true, el) | _ -> fprintf p "({ %a })" print_stmt s @@ -422,31 +417,34 @@ 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_expr = function + | Eloc _ -> assert false + | Evar _ -> () + | Ederef(r, _) -> collect_expr r + | Efield(l, _, _) -> collect_expr l + | Eval _ -> () + | Evalof(l, _) -> collect_expr l + | Eaddrof(l, _) -> collect_expr l + | Eunop(_, r, _) -> collect_expr r + | Ebinop(_, r1, r2, _) -> collect_expr r1; collect_expr r2 + | Ecast(r, _) -> collect_expr r + | Econdition(r1, r2, r3, _) -> + collect_expr r1; collect_expr r2; collect_expr r3 + | Esizeof _ -> () + | Eassign(l, r, _) -> collect_expr l; collect_expr r + | Eassignop(_, l, r, _, _) -> collect_expr l; collect_expr r + | Epostincr(_, l, _) -> collect_expr l + | Ecomma(r1, r2, _) -> collect_expr r1; collect_expr r2 + | Ecall(r1, rl, _) -> collect_expr r1; collect_exprlist rl + | Eparen _ -> assert false + +and collect_exprlist = function + | Enil -> () + | Econs(r1, rl) -> collect_expr r1; collect_exprlist rl 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 + | Sdo e -> collect_expr e | 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 @@ -507,4 +505,12 @@ let print_program p prog = 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