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

1 files changed, 131 insertions, 125 deletions

diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 3b5dbc5..61599cf 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 "@[<hov 2>("
+  else fprintf p "@[<hov 2>";
+  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 "@[<hov 2>%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 "@[<hov 0>%a@ %s %a@]"
-                print_expr_prec (level, e1)
-                (name_binop op)
-                print_expr_prec (level, e2)
-  | Ecast(ty, e1) ->
-      fprintf p "@[<hov 2>(%s)@,%a@]"
-                (name_type ty)
-                print_expr_prec (level, e1)
-  | Econdition(e1, e2, e3) ->
-      fprintf p "@[<hov 0>%a@ ? %a@ : %a@]"
-                print_expr_prec (level, e1)
-                print_expr_prec (level, e2)
-                print_expr_prec (level, e3)
-  | Eandbool(e1, e2) ->
-      fprintf p "@[<hov 0>%a@ && %a@]"
-                print_expr_prec (level, e1)
-                print_expr_prec (level, e2)
-  | Eorbool(e1, e2) ->
-      fprintf p "@[<hov 0>%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@[<hov 1>(%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 "@[<hv 2>%a =@ %a;@]" print_expr e1 print_expr e2
-  | Scall(None, e1, el) ->
-      fprintf p "@[<hv 2>%a@,(@[<hov 0>%a@]);@]"
-                print_expr e1
-                print_expr_list (true, el)
-  | Scall(Some lhs, e1, el) ->
-      fprintf p "@[<hv 2>%a =@ %a@,(@[<hov 0>%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 "@[<hv 2>%a@,(@[<hov 0>%a@])@]"
-                print_expr e1
-                print_expr_list (true, el)
-  | Scall(Some lhs, e1, el) ->
-      fprintf p "@[<hv 2>%a =@ %a@,(@[<hov 0>%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