clightgen: add option -normalize to ensure that memory loads never occur "deep" inside expressions

For example, with this option,

      tmp = *(x + 0) + *(x + 1)

in the original Clight is rewritten to

      tmp1 = *(x + 0)
      tmp2 = *(x + 1)
      tmp = tmp1 + tmp2

with two temporaries tmp1 and tmp2 introduced to name the intermediate results of memory loads.

Squashed commit of the following:
commit 3fb69dae567b1305383b74ce1707945f91369a46
commit 0071654b77a239c00bcbb92a5845447b2c4e9d2a
commit c220ed303d9f3f36cc03c347a77b065a9362c0e7

2 files changed, 177 insertions, 2 deletions

diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml
index eddb36e2..4af90179 100644
--- a/exportclight/Clightgen.ml
+++ b/exportclight/Clightgen.ml
@@ -23,6 +23,10 @@ open Frontend
 
 let stdlib_path = ref Configuration.stdlib_path
 
+(* clightgen-specific options *)
+
+let option_normalize = ref false
+
 (* From CompCert C AST to Clight *)
 
 let compile_c_ast sourcename csyntax ofile =
@@ -30,7 +34,10 @@ let compile_c_ast sourcename csyntax ofile =
     match SimplExpr.transl_program csyntax with
     | Errors.OK p ->
         begin match SimplLocals.transf_program p with
-        | Errors.OK p' -> p'
+        | Errors.OK p' ->
+            if !option_normalize
+            then Clightnorm.norm_program p'
+            else p'
         | Errors.Error msg ->
             print_error stderr msg;
             exit 2
@@ -79,6 +86,7 @@ let usage_string =
 Recognized source files:\n\
 \  .c             C source file\n\
 Processing options:\n\
+\  -normalize     Normalize the generated Clight code w.r.t. loads in expressions\n\
 \  -E             Preprocess only, send result to standard output\n"^
 prepro_help ^
 "Language support options (use -fno-<opt> to turn off -f<opt>) :\n\
@@ -124,7 +132,8 @@ let cmdline_actions =
   Exact "-version", Unit print_version_and_exit;
   Exact "--version", Unit print_version_and_exit;
 (* Processing options *)
-  Exact "-E", Set option_E;]
+  Exact "-E", Set option_E;
+  Exact "-normalize", Set option_normalize]
 (* Preprocessing options *)
   @ prepro_actions @
 (* Language support options -- more below *)
diff --git a/exportclight/Clightnorm.ml b/exportclight/Clightnorm.ml
new file mode 100644
index 00000000..4b01d777
--- /dev/null
+++ b/exportclight/Clightnorm.ml
@@ -0,0 +1,166 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Clight-to-Clight rewriting to name memory loads *)
+
+(* The effect of this rewriting is to ensure that Clight expressions
+  whose evaluation involves a memory load (i.e. a lvalue-to-rvalue
+  conversion with By_value access mode) are always bound to a temporary
+  and never occur deep inside another expression.  For example,
+
+      tmp = *(x + 0) + *(x + 1)
+
+  in the original Clight is rewritten to
+
+      tmp1 = *(x + 0)
+      tmp2 = *(x + 1)
+      tmp = tmp1 + tmp2
+*)
+
+open Camlcoq
+open Ctypes
+open Clight
+
+let gen_next : AST.ident ref = ref P.one
+let gen_trail : (AST.ident * coq_type) list ref = ref []
+
+let gensym ty =
+  let id = !gen_next in
+  gen_next := P.succ id;
+  gen_trail := (id, ty) :: !gen_trail;
+  id
+
+let is_lvalue = function
+  | Evar _ | Ederef _ | Efield _ -> true
+  | _ -> false
+
+let accesses_memory e =
+  is_lvalue e &&
+  match access_mode (typeof e) with By_value _ -> true | _ -> false
+
+(** Normalization of an expression.  Return a normalized expression
+  and a list of statements to be executed before evaluating the expression. *)
+
+let rec norm_expr e =
+  let (sl, e') = norm_expr_1 e in
+  if accesses_memory e then begin
+    let ty = typeof e in
+    let id = gensym ty in
+    (sl @ [Sset(id, e')], Etempvar(id, ty))
+  end else
+    (sl, e')
+
+and norm_expr_1 e =
+  match e with
+  | Econst_int _ | Econst_float _ | Econst_single _ | Econst_long _ -> ([], e)
+  | Evar _ | Etempvar _ -> ([], e)
+  | Ederef(e1, t) ->
+      let (sl, e1') = norm_expr e1 in (sl, Ederef(e1', t))
+  | Eaddrof(e1, t) ->
+      let (sl, e1') = norm_expr_lvalue e1 in (sl, Eaddrof(e1', t))
+  | Eunop(op, e1, t) ->
+      let (sl, e1') = norm_expr e1 in (sl, Eunop(op, e1', t))
+  | Ebinop(op, e1, e2, t) ->
+      let (sl1, e1') = norm_expr e1 in
+      let (sl2, e2') = norm_expr e2 in
+      (sl1 @ sl2, Ebinop(op, e1', e2', t))
+  | Ecast(e1, t) ->
+      let (sl, e1') = norm_expr e1 in (sl, Ecast(e1', t))
+  | Efield(e1, id, t) ->
+      let (sl, e1') = norm_expr e1 in (sl, Efield(e1', id, t))
+  | Esizeof _ | Ealignof _ -> ([], e)
+
+(** An expression in l-value position has no memory dereference at top level,
+  by definition of l-values.  Hence, use the [norm_expr_1] variant.. *)
+and norm_expr_lvalue e = norm_expr_1 e
+
+(** In a [Sset id e] statement, the [e] expression can contain a memory
+  dereference at top level.  Hence, use the [norm_expr_1] variant. *)
+let norm_expr_set_top = norm_expr_1
+
+let rec norm_expr_list el =
+  match el with
+  | [] -> ([], [])
+  | e1 :: el ->
+      let (sl1, e1') = norm_expr e1 in
+      let (sl2, el') = norm_expr_list el in
+      (sl1 @ sl2, e1' :: el')
+
+let rec add_sequence sl s =
+  match sl with
+  | [] -> s
+  | s1 :: sl -> Ssequence(s1, add_sequence sl s)
+
+let rec norm_stmt s =
+  match s with
+  | Sskip -> s
+  | Sassign(e1, e2) ->
+      let (sl1, e1') = norm_expr_lvalue e1 in
+      let (sl2, e2') = norm_expr e2 in
+      add_sequence (sl1 @ sl2) (Sassign(e1', e2'))
+  | Sset(id, e) ->
+      let (sl, e') = norm_expr_set_top e in
+      add_sequence sl (Sset(id, e'))
+  | Scall(optid, e, el) ->
+      let (sl1, e') = norm_expr e in
+      let (sl2, el') = norm_expr_list el in
+      add_sequence (sl1 @ sl2) (Scall(optid, e', el'))  
+  | Sbuiltin(optid, ef, tyl, el) ->
+      let (sl, el') = norm_expr_list el in
+      add_sequence sl (Sbuiltin(optid, ef, tyl, el'))
+  | Ssequence(s1, s2) ->
+      Ssequence(norm_stmt s1, norm_stmt s2)
+  | Sifthenelse(e, s1, s2) ->
+      let (sl, e') = norm_expr e in
+      add_sequence sl (Sifthenelse(e', norm_stmt s1, norm_stmt s2))
+  | Sloop(s1, s2) ->
+      Sloop(norm_stmt s1, norm_stmt s2)
+  | Sbreak | Scontinue | Sreturn None -> s
+  | Sreturn (Some e) ->
+      let (sl, e') = norm_expr e in
+      add_sequence sl (Sreturn(Some e'))
+  | Sswitch(e, ls) ->
+      let (sl, e') = norm_expr e in
+      add_sequence sl (Sswitch(e, norm_lbl_stmt ls))
+  | Slabel(lbl, s1) ->
+      Slabel(lbl, norm_stmt s1)
+  | Sgoto lbl -> s
+
+and norm_lbl_stmt ls =
+  match ls with
+  | LSnil -> LSnil
+  | LScons(n, s, ls) -> LScons(n, norm_stmt s, norm_lbl_stmt ls)
+
+let next_var curr (v, _) = if P.lt v curr then curr else P.succ v
+
+let next_var_list vars start = List.fold_left next_var start vars
+
+let norm_function f =
+  gen_next := next_var_list f.fn_params
+                (next_var_list f.fn_vars
+                   (next_var_list f.fn_temps
+                     (Camlcoq.first_unused_ident ())));
+  gen_trail := [];
+  let s' = norm_stmt f.fn_body in
+  let new_temps = !gen_trail in
+  { f with fn_body = s'; fn_temps = f.fn_temps @ new_temps }
+
+let norm_fundef = function
+  | Internal f -> Internal (norm_function f)
+  | External _ as fd -> fd
+
+let norm_program p =
+  let p1 = AST.transform_program norm_fundef (program_of_program p) in
+  { p with prog_defs = p1.AST.prog_defs }