SimplVolatile: new pass to eliminate read-modify-write ops over volatiles

Elsewhere: refactoring, moving common code into Cutil and Transform
  (to be continued)


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1716 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

10 files changed, 265 insertions, 169 deletions

diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml
index ff4c0c6..d16f91f 100644
--- a/cparser/Bitfields.ml
+++ b/cparser/Bitfields.ml
@@ -251,8 +251,6 @@ let rec is_bitfield_access env e =
 
 (* Expressions *)
 
-type context = Val | Effects
-
 let transf_expr env ctx e =
 
   let rec texp ctx e =
@@ -329,7 +327,7 @@ let transf_expr env ctx e =
       {edesc = EUnop(Odot bf.bf_carrier, texp Val e); etyp = bf.bf_carrier_typ}
 
   and transf_assign ctx e1 bf e2 =
-    bind_lvalue (texp Val e1) (fun base ->
+    bind_lvalue env (texp Val e1) (fun base ->
       let carrier =
         {edesc = EUnop(Odot bf.bf_carrier, base); etyp = bf.bf_carrier_typ} in
       let asg =
@@ -337,7 +335,7 @@ let transf_expr env ctx e =
       if ctx = Val then ecomma asg (bitfield_extract bf carrier) else asg)
 
   and transf_assignop ctx op e1 bf e2 tyres =
-    bind_lvalue (texp Val e1) (fun base ->
+    bind_lvalue env (texp Val e1) (fun base ->
       let carrier =
         {edesc = EUnop(Odot bf.bf_carrier, base); etyp = bf.bf_carrier_typ} in
       let rhs =
@@ -355,7 +353,7 @@ let transf_expr env ctx e =
     if ctx = Effects then
       transf_pre ctx op e1 bf tyfield
     else begin
-      bind_lvalue (texp Val e1) (fun base ->
+      bind_lvalue env (texp Val e1) (fun base ->
         let carrier =
           {edesc = EUnop(Odot bf.bf_carrier, base); etyp = bf.bf_carrier_typ} in
         let temp = new_temp tyfield in
@@ -372,47 +370,13 @@ let transf_expr env ctx e =
 
 (* Statements *)
 
-let rec transf_stmt env s =
-  match s.sdesc with
-  | Sskip -> s
-  | Sdo e ->
-      {sdesc = Sdo(transf_expr env Effects e); sloc = s.sloc}
-  | Sseq(s1, s2) -> 
-      {sdesc = Sseq(transf_stmt env s1, transf_stmt env s2); sloc = s.sloc }
-  | Sif(e, s1, s2) ->
-      {sdesc = Sif(transf_expr env Val e, transf_stmt env s1, transf_stmt env s2);
-       sloc = s.sloc}
-  | Swhile(e, s1) ->
-      {sdesc = Swhile(transf_expr env Val e, transf_stmt env s1);
-       sloc = s.sloc}
-  | Sdowhile(s1, e) ->
-      {sdesc = Sdowhile(transf_stmt env s1, transf_expr env Val e);
-       sloc = s.sloc}
-  | Sfor(s1, e, s2, s3) ->
-      {sdesc = Sfor(transf_stmt env s1, transf_expr env Val e,
-                    transf_stmt env s2, transf_stmt env s3);
-       sloc = s.sloc}
-  | Sbreak -> s
-  | Scontinue -> s
-  | Sswitch(e, s1) ->
-      {sdesc = Sswitch(transf_expr env Val e, transf_stmt env s1);
-       sloc = s.sloc}
-  | Slabeled(lbl, s) ->
-      {sdesc = Slabeled(lbl, transf_stmt env s); sloc = s.sloc}
-  | Sgoto lbl -> s
-  | Sreturn None -> s
-  | Sreturn (Some e) ->
-      {sdesc = Sreturn(Some(transf_expr env Val e)); sloc = s.sloc}
-  | Sblock _ | Sdecl _ ->
-      assert false     (* should not occur in unblocked code *)
+let transf_stmt env s =
+  Transform.stmt (fun loc env ctx e -> transf_expr env ctx e) env s
 
 (* Functions *)
 
 let transf_fundef env f =
-  reset_temps();
-  let newbody = transf_stmt env f.fd_body in
-  let temps = get_temps() in  
-  { f with fd_locals = f.fd_locals @ temps; fd_body = newbody }
+  Transform.fundef transf_stmt env f
 
 (* Initializers *)
 
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 2e664df..103dda4 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -709,9 +709,9 @@ let floatconst v fk =
 let nullconst =
   { edesc = EConst(CInt(0L, ptr_t_ikind, "0")); etyp = TPtr(TVoid [], []) }
 
-(* Construct an address-of expression *)
+(* Construct a cast expression *)
 
-let eaddrof e = { edesc = EUnop(Oaddrof, e); etyp = TPtr(e.etyp, []) }
+let ecast e ty = { edesc = ECast(ty, e); etyp = ty }
 
 (* Construct an assignment expression *)
 
@@ -721,6 +721,14 @@ let eassign e1 e2 = { edesc = EBinop(Oassign, e1, e2, e1.etyp); etyp = e1.etyp }
 
 let ecomma e1 e2 = { edesc = EBinop(Ocomma, e1, e2, e2.etyp); etyp = e2.etyp }
 
+(* Construct an address-of expression.  Can be applied not just to
+   an l-value but also to a sequence. *)
+
+let rec eaddrof e =
+  match e.edesc with
+  | EBinop(Ocomma, e1, e2, _) -> ecomma e1 (eaddrof e2)
+  | _ -> { edesc = EUnop(Oaddrof, e); etyp = TPtr(e.etyp, []) }
+
 (* Construct a sequence *)
 
 let sseq loc s1 s2 =
diff --git a/cparser/Makefile b/cparser/Makefile
index 9767b48..527cdd3 100644
--- a/cparser/Makefile
+++ b/cparser/Makefile
@@ -16,7 +16,7 @@ SRCS=Errors.ml Cabs.ml Cabshelper.ml Parse_aux.ml Parser.ml Lexer.ml \
   Cleanup.ml Elab.ml Rename.ml \
   Transform.ml \
   Unblock.ml SimplExpr.ml AddCasts.ml StructByValue.ml StructAssign.ml \
-  Bitfields.ml PackedStructs.ml \
+  Bitfields.ml PackedStructs.ml SimplVolatile.ml \
   Parse.ml
 
 COBJS=uint64.o
diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml
index edd45ff..4b5d0e1 100644
--- a/cparser/PackedStructs.ml
+++ b/cparser/PackedStructs.ml
@@ -20,6 +20,7 @@ open C
 open Cutil
 open Env
 open Errors
+open Transform
 
 type field_info = {
   fi_offset: int;                       (* byte offset within struct *)
@@ -177,8 +178,6 @@ let bswap_write loc env lhs rhs ik =
 
 (* Expressions *)
 
-type context = Val | Effects
-
 let transf_expr loc env ctx e =
 
   let is_packed_access ty fieldname =
@@ -284,45 +283,13 @@ let transf_expr loc env ctx e =
 
 (* Statements *)
 
-let rec transf_stmt env s =
-  match s.sdesc with
-  | Sskip -> s
-  | Sdo e ->
-      {sdesc = Sdo(transf_expr s.sloc env Effects e); sloc = s.sloc}
-  | Sseq(s1, s2) -> 
-      {sdesc = Sseq(transf_stmt env s1, transf_stmt env s2); sloc = s.sloc }
-  | Sif(e, s1, s2) ->
-      {sdesc = Sif(transf_expr s.sloc env Val e,
-                   transf_stmt env s1, transf_stmt env s2);
-       sloc = s.sloc}
-  | Swhile(e, s1) ->
-      {sdesc = Swhile(transf_expr s.sloc env Val e, transf_stmt env s1);
-       sloc = s.sloc}
-  | Sdowhile(s1, e) ->
-      {sdesc = Sdowhile(transf_stmt env s1, transf_expr s.sloc env Val e);
-       sloc = s.sloc}
-  | Sfor(s1, e, s2, s3) ->
-      {sdesc = Sfor(transf_stmt env s1, transf_expr s.sloc env Val e,
-                    transf_stmt env s2, transf_stmt env s3);
-       sloc = s.sloc}
-  | Sbreak -> s
-  | Scontinue -> s
-  | Sswitch(e, s1) ->
-      {sdesc = Sswitch(transf_expr s.sloc env Val e,
-                       transf_stmt env s1); sloc = s.sloc}
-  | Slabeled(lbl, s) ->
-      {sdesc = Slabeled(lbl, transf_stmt env s); sloc = s.sloc}
-  | Sgoto lbl -> s
-  | Sreturn None -> s
-  | Sreturn (Some e) ->
-      {sdesc = Sreturn(Some(transf_expr s.sloc env Val e)); sloc = s.sloc}
-  | Sblock _ | Sdecl _ ->
-      assert false     (* should not occur in unblocked code *)
+let transf_stmt env s =
+  Transform.stmt transf_expr env s
 
 (* Functions *)
 
 let transf_fundef env f =
-  { f with fd_body = transf_stmt env f.fd_body }
+  Transform.fundef transf_stmt env f
 
 (* Initializers *)
 
diff --git a/cparser/Parse.ml b/cparser/Parse.ml
index abef83c..dcd01e9 100644
--- a/cparser/Parse.ml
+++ b/cparser/Parse.ml
@@ -21,13 +21,14 @@ let transform_program t p =
   let run_pass pass flag p = if CharSet.mem flag t then pass p else p in
   Rename.program
   (run_pass (AddCasts.program ~all:(CharSet.mem 'C' t)) 'c'
-  (run_pass (SimplExpr.program ~volatile:(CharSet.mem 'v' t)) 'e'
+  (run_pass (SimplExpr.program ~volatile:(CharSet.mem 'V' t)) 'e'
+  (run_pass SimplVolatile.program 'v'
   (run_pass StructAssign.program 'S'
   (run_pass StructByValue.program 's'
   (run_pass PackedStructs.program 'p'
   (run_pass Bitfields.program 'f'
   (run_pass Unblock.program 'b'
-  p)))))))
+  p))))))))
 
 let parse_transformations s =
   let t = ref CharSet.empty in
@@ -39,7 +40,8 @@ let parse_transformations s =
             | 'C' -> set "ecC"
             | 's' -> set "s"
             | 'S' -> set "bsS"
-            | 'v' -> set "ev"
+            | 'v' -> set "v"
+            | 'V' -> set "eV"
             | 'f' -> set "bf"
             | 'p' -> set "bp"
             |  _  -> ())
diff --git a/cparser/SimplVolatile.ml b/cparser/SimplVolatile.ml
new file mode 100644
index 0000000..c6ebd34
--- /dev/null
+++ b/cparser/SimplVolatile.ml
@@ -0,0 +1,138 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Elimination of read-modify-write operators (+=, ++, etc) applied
+   to volatile expressions. *)
+
+open Printf
+open C
+open Cutil
+open Transform
+
+(* Expansion of read-write-modify constructs. *)
+
+(** [l = r]. *)
+
+let mk_assign ctx l r =
+  match ctx with
+  | Effects ->
+      eassign l r
+  | Val ->
+      let tmp = new_temp l.etyp in
+      ecomma (eassign tmp r) (ecomma (eassign l tmp) tmp)
+
+(** [l op= r].  Warning: [l] is evaluated twice. *)
+
+let mk_assignop ctx op l r ty =
+  let op' =
+    match op with
+    | Oadd_assign -> Oadd | Osub_assign -> Osub
+    | Omul_assign -> Omul | Odiv_assign -> Odiv | Omod_assign -> Omod
+    | Oand_assign -> Oand | Oor_assign -> Oor   | Oxor_assign -> Oxor
+    | Oshl_assign -> Oshl | Oshr_assign -> Oshr
+    | _ -> assert false in
+  let res = {edesc = EBinop(op', l, r, ty); etyp = ty} in
+  match ctx with
+  | Effects ->
+      eassign l res
+  | Val ->
+      let tmp = new_temp l.etyp in
+      ecomma (eassign tmp res) (ecomma (eassign l tmp) tmp)
+
+(** [++l] or [--l].  Warning: [l] is evaluated twice. *)
+
+let mk_preincrdecr ctx op l ty =
+  let op' =
+    match op with
+    | Opreincr -> Oadd_assign
+    | Opredecr -> Osub_assign
+    | _ -> assert false in  
+  mk_assignop ctx op' l (intconst 1L IInt) ty
+
+(** [l++] or [l--].  Warning: [l] is evaluated twice. *)
+
+let mk_postincrdecr ctx op l ty =
+  let op' =
+    match op with
+    | Opostincr -> Oadd
+    | Opostdecr -> Osub
+    | _ -> assert false in  
+  match ctx with
+  | Effects ->
+      let newval = {edesc = EBinop(op', l, intconst 1L IInt, ty); etyp = ty} in
+      eassign l newval
+  | Val ->
+      let tmp = new_temp l.etyp in
+      let newval = {edesc = EBinop(op', tmp, intconst 1L IInt, ty); etyp = ty} in
+      ecomma (eassign tmp l) (ecomma (eassign l newval) tmp)
+
+(* Rewriting of expressions *)
+
+let transf_expr loc env ctx e =
+
+  let is_volatile ty =
+    List.mem AVolatile (attributes_of_type env ty) in
+
+  let rec texp ctx e =
+    match e.edesc with
+    | EConst _ -> e
+    | ESizeof _ -> e
+    | EVar _ -> e
+    | EUnop((Opreincr|Opredecr as op), e1) when is_volatile e1.etyp ->
+        bind_lvalue env (texp Val e1)
+          (fun l -> mk_preincrdecr ctx op l (unary_conversion env l.etyp))
+    | EUnop((Opostincr|Opostdecr as op), e1) when is_volatile e1.etyp ->
+        bind_lvalue env (texp Val e1)
+          (fun l -> mk_postincrdecr ctx op l (unary_conversion env l.etyp))
+    | EUnop(op, e1) ->
+        {edesc = EUnop(op, texp Val e1); etyp = e.etyp}
+    | EBinop(Oassign, e1, e2, ty) when is_volatile e1.etyp ->
+        mk_assign ctx (texp Val e1) (texp Val e2)
+    | EBinop((Oadd_assign | Osub_assign | Omul_assign
+              | Odiv_assign | Omod_assign
+              | Oand_assign | Oor_assign | Oxor_assign
+              | Oshl_assign | Oshr_assign) as op, e1, e2, ty)
+      when is_volatile e1.etyp ->
+        bind_lvalue env (texp Val e1)
+          (fun l -> mk_assignop ctx op l (texp Val e2) ty)
+    | EBinop(Ocomma, e1, e2, ty) ->
+        {edesc = EBinop(Ocomma, texp Effects e1, texp ctx e2, ty);
+         etyp = e.etyp}
+    | EBinop(op, e1, e2, ty) ->
+        {edesc = EBinop(op, texp Val e1, texp Val e2, ty); etyp = e.etyp}
+    | EConditional(e1, e2, e3) ->
+        {edesc = EConditional(texp Val e1, texp ctx e2, texp ctx e3);
+         etyp = e.etyp}
+    | ECast(ty, e1) ->
+        {edesc = ECast(ty, texp Val e1); etyp = e.etyp}
+    | ECall(e1, el) ->
+        {edesc = ECall(texp Val e1, List.map (texp Val) el); etyp = e.etyp}
+
+  in texp ctx e
+
+(* Statements *)
+
+let transf_stmt env s =
+  Transform.stmt transf_expr env s
+
+(* Functions *)
+
+let transf_fundef env f =
+  Transform.fundef transf_stmt env f
+
+(* Programs *)
+
+let program p =
+  Transform.program ~fundef:transf_fundef p
diff --git a/cparser/StructAssign.ml b/cparser/StructAssign.ml
index 5c989a3..d9ad8f5 100644
--- a/cparser/StructAssign.ml
+++ b/cparser/StructAssign.ml
@@ -62,17 +62,11 @@ let find_memcpy env =
   with Env.Error _ ->
     (default_memcpy(), false)
 
-(* Smart constructors that "bubble up" sequence expressions *)
+(* Smart constructor that "bubble up" sequence expressions *)
 
-let rec addrof e =
+let rec edot f e ty =
   match e.edesc with
-  | EBinop(Ocomma, e1, e2, _) -> ecomma e1 (addrof e2)
-  | EUnop(Oderef, e1) -> e1
-  | _ -> eaddrof e
-
-let rec dot f e ty =
-  match e.edesc with
-  | EBinop(Ocomma, e1, e2, _) -> ecomma e1 (dot f e2 ty)
+  | EBinop(Ocomma, e1, e2, _) -> ecomma e1 (edot f e2 ty)
   | _ -> { edesc = EUnop(Odot f, e); etyp = ty }
 
 (* Translate an assignment [lhs = rhs] between composite types.
@@ -83,8 +77,8 @@ let transf_assign env lhs rhs =
      match Cutil.alignof env lhs.etyp with Some al -> al | None -> 1 in
   let ((ident, ty), four_args) = find_memcpy env in
   let memcpy = {edesc = EVar(ident); etyp = ty} in
-  let e_lhs = addrof lhs
-  and e_rhs = addrof rhs
+  let e_lhs = eaddrof lhs
+  and e_rhs = eaddrof rhs
   and e_size = {edesc = ESizeof(lhs.etyp); etyp = TInt(size_t_ikind, [])}
   and e_align = intconst (Int64.of_int al) size_t_ikind in
   let args =
@@ -95,13 +89,12 @@ let transf_assign env lhs rhs =
 
 (* Transformation of expressions. *)
 
-type context = Val | Effects
-
-let rec transf_expr env ctx e =
+let transf_expr loc env ctx e =
+  let rec texp ctx e =
   match e.edesc with
   | EBinop(Oassign, lhs, rhs, _) when is_composite_type env lhs.etyp ->
-      let lhs' = transf_expr env Val lhs in
-      let rhs' = transf_expr env Val rhs in
+      let lhs' = texp Val lhs in
+      let rhs' = texp Val rhs in
       begin match ctx with
       | Effects ->
           transf_assign env lhs' rhs'
@@ -115,76 +108,52 @@ let rec transf_expr env ctx e =
       then nullconst
       else e
   | EUnop(Oaddrof, e1) ->
-      addrof (transf_expr env Val e1)
+      eaddrof (texp Val e1)
   | EUnop(Oderef, e1) ->
       if ctx = Effects && is_composite_type env e.etyp
-      then transf_expr env Effects e1
-      else {edesc = EUnop(Oderef, transf_expr env Val e1); etyp = e.etyp}
+      then texp Effects e1
+      else {edesc = EUnop(Oderef, texp Val e1); etyp = e.etyp}
   | EUnop(Odot f, e1) ->
       if ctx = Effects && is_composite_type env e.etyp
-      then transf_expr env Effects e1
-      else dot f (transf_expr env Val e1) e.etyp
+      then texp Effects e1
+      else edot f (texp Val e1) e.etyp
   | EUnop(Oarrow f, e1) ->
       if ctx = Effects && is_composite_type env e.etyp
-      then transf_expr env Effects e1
-      else {edesc = EUnop(Oarrow f, transf_expr env Val e1); etyp = e.etyp}
+      then texp Effects e1
+      else {edesc = EUnop(Oarrow f, texp Val e1); etyp = e.etyp}
   | EUnop(op, e1) ->
-      {edesc = EUnop(op, transf_expr env Val e1); etyp = e.etyp}
+      {edesc = EUnop(op, texp Val e1); etyp = e.etyp}
   | EBinop(Oindex, e1, e2, ty) ->
       if ctx = Effects && is_composite_type env e.etyp
-      then ecomma (transf_expr env Effects e1) (transf_expr env Effects e2)
-      else {edesc = EBinop(Oindex, transf_expr env Val e1, transf_expr env Val e2, ty); etyp = e.etyp}
+      then ecomma (texp Effects e1) (texp Effects e2)
+      else {edesc = EBinop(Oindex, texp Val e1, texp Val e2, ty); etyp = e.etyp}
   | EBinop(Ocomma, e1, e2, ty) ->
-      ecomma (transf_expr env Effects e1) (transf_expr env ctx e2)
+      ecomma (texp Effects e1) (texp ctx e2)
   | EBinop(op, e1, e2, ty) ->
-      {edesc = EBinop(op, transf_expr env Val e1,
-                          transf_expr env Val e2, ty);
+      {edesc = EBinop(op, texp Val e1, texp Val e2, ty);
        etyp = e.etyp}
   | EConditional(e1, e2, e3) ->
-      {edesc = EConditional(transf_expr env Val e1,
-                            transf_expr env ctx e2, transf_expr env ctx e3);
+      {edesc = EConditional(texp Val e1, texp ctx e2, texp ctx e3);
        etyp = e.etyp}
   | ECast(ty, e1) ->
-      {edesc = ECast(ty, transf_expr env Val e1); etyp = e.etyp}
+      {edesc = ECast(ty, texp Val e1); etyp = e.etyp}
   | ECall(e1, el) ->
-      {edesc = ECall(transf_expr env Val e1,
-                     List.map (transf_expr env Val) el);
+      {edesc = ECall(texp Val e1,
+                     List.map (texp Val) el);
        etyp = e.etyp}
+  in texp ctx e
 
 (* Transformation of statements *)
 
-let rec transf_stmt env s =
-  match s.sdesc with
-  | Sskip -> s
-  | Sdo e -> {s with sdesc = Sdo(transf_expr env Effects e)}
-  | Sseq(s1, s2) ->
-      {s with sdesc = Sseq(transf_stmt env s1, transf_stmt env s2)}
-  | Sif(e, s1, s2) ->
-      {s with sdesc = Sif(transf_expr env Val e,
-                          transf_stmt env s1, transf_stmt env s2)}
-  | Swhile(e, s1) ->
-      {s with sdesc = Swhile(transf_expr env Val e, transf_stmt env s1)}
-  | Sdowhile(s1, e) ->
-      {s with sdesc = Sdowhile(transf_stmt env s1, transf_expr env Val e)}
-  | Sfor(s1, e, s2, s3) ->
-      {s with sdesc = Sfor(transf_stmt env s1, transf_expr env Val e,
-                           transf_stmt env s2, transf_stmt env s3)}
-  | Sbreak -> s
-  | Scontinue -> s
-  | Sswitch(e, s1) ->
-      {s with sdesc = Sswitch(transf_expr env Val e, transf_stmt env s1)}
-  | Slabeled(lbl, s1) ->
-      {s with sdesc = Slabeled(lbl, transf_stmt env s1)}
-  | Sgoto lbl -> s
-  | Sreturn None -> s
-  | Sreturn (Some e) -> {s with sdesc = Sreturn(Some(transf_expr env Val e))}
-  | Sblock _ | Sdecl _ -> assert false (* not in unblocked code *)
+let transf_stmt env s =
+  Transform.stmt transf_expr env s
+
+(* Transformation of function definitions *)
 
 let transf_fundef env f =
-  reset_temps();
-  let newbody = transf_stmt env f.fd_body in
-  let temps = get_temps() in
-  {f with fd_locals = f.fd_locals @ temps; fd_body = newbody}
+  Transform.fundef transf_stmt env f
+
+(* Transformation of programs *)
 
 let program p =
   memcpy_decl := None;
diff --git a/cparser/StructByValue.ml b/cparser/StructByValue.ml
index 07a6acf..1b74ec5 100644
--- a/cparser/StructByValue.ml
+++ b/cparser/StructByValue.ml
@@ -55,18 +55,8 @@ and transf_funarg env (id, t) =
   then (id, TPtr(add_attributes_type [AConst] t, []))
   else (id, t)
 
-(* Smart constructor that "bubble up" sequence expressions *)
-
-let rec addrof e =
-  match e.edesc with
-  | EBinop(Ocomma, e1, e2, _) -> ecomma e1 (addrof e2)
-  | EUnop(Oderef, e1) -> e1
-  | _ -> eaddrof e
-
 (* Expressions: transform calls + rewrite the types *)
 
-type context = Val | Effects
-
 let rec transf_expr env ctx e =
   let newty = transf_type env e.etyp in
   match e.edesc with
@@ -109,7 +99,7 @@ let rec transf_expr env ctx e =
 
 and transf_arg env e =
   let e' = transf_expr env Val e in
-  if is_composite_type env e'.etyp then addrof e' else e'
+  if is_composite_type env e'.etyp then eaddrof e' else e'
 
 (* Function calls returning a composite: add first argument.
     ctx = Effects:   lv = f(...)     -> f(&lv, ...)
@@ -125,17 +115,17 @@ and transf_composite_call env ctx opt_lhs fn args ty =
   match ctx, opt_lhs with
   | Effects, None ->
       let tmp = new_temp ~name:"_res" ty in
-      {edesc = ECall(fn, addrof tmp :: args); etyp = TVoid []}
+      {edesc = ECall(fn, eaddrof tmp :: args); etyp = TVoid []}
   | Effects, Some lhs ->
       let lhs = transf_expr env Val lhs in
-      {edesc = ECall(fn, addrof lhs :: args); etyp = TVoid []}
+      {edesc = ECall(fn, eaddrof lhs :: args); etyp = TVoid []}
   | Val, None ->
       let tmp = new_temp ~name:"_res" ty in
-      ecomma {edesc = ECall(fn, addrof tmp :: args); etyp = TVoid []} tmp
+      ecomma {edesc = ECall(fn, eaddrof tmp :: args); etyp = TVoid []} tmp
   | Val, Some lhs ->
       let lhs = transf_expr env Val lhs in
       let tmp = new_temp ~name:"_res" ty in
-      ecomma (ecomma {edesc = ECall(fn, addrof tmp :: args); etyp = TVoid []}
+      ecomma (ecomma {edesc = ECall(fn, eaddrof tmp :: args); etyp = TVoid []}
                      (eassign lhs tmp))
              tmp
 
diff --git a/cparser/Transform.ml b/cparser/Transform.ml
index 1cafaba..8bdf2e2 100644
--- a/cparser/Transform.ml
+++ b/cparser/Transform.ml
@@ -53,12 +53,54 @@ let bind_lvalue env e fn =
     fn e
   else begin
     let tmp = new_temp (TPtr(e.etyp, [])) in
-    ecomma (eassign tmp (addrof e))
+    ecomma (eassign tmp (eaddrof e))
            (fn {edesc = EUnop(Oderef, tmp); etyp = e.etyp})
   end
 
-
-(* Generic transformation *)
+(* Generic transformation of a statement, transforming expressions within
+   and preserving the statement structure.  Applies only to unblocked code. *)
+
+type context = Val | Effects
+
+let stmt trexpr env s =
+  let rec stm s =
+  match s.sdesc with
+  | Sskip -> s
+  | Sdo e ->
+      {s with sdesc = Sdo(trexpr s.sloc env Effects e)}
+  | Sseq(s1, s2) -> 
+      {s with sdesc = Sseq(stm s1, stm s2)}
+  | Sif(e, s1, s2) ->
+      {s with sdesc = Sif(trexpr s.sloc env Val e, stm s1, stm s2)}
+  | Swhile(e, s1) ->
+      {s with sdesc = Swhile(trexpr s.sloc env Val e, stm s1)}
+  | Sdowhile(s1, e) ->
+      {s with sdesc = Sdowhile(stm s1, trexpr s.sloc env Val e)}
+  | Sfor(s1, e, s2, s3) ->
+      {s with sdesc = Sfor(stm s1, trexpr s.sloc env Val e, stm s2, stm s3)}
+  | Sbreak -> s
+  | Scontinue -> s
+  | Sswitch(e, s1) ->
+      {s with sdesc = Sswitch(trexpr s.sloc env Val e, stm s1)}
+  | Slabeled(lbl, s) ->
+      {s with sdesc = Slabeled(lbl, stm s)}
+  | Sgoto lbl -> s
+  | Sreturn None -> s
+  | Sreturn (Some e) ->
+      {s with sdesc = Sreturn(Some(trexpr s.sloc env Val e))}
+  | Sblock _ | Sdecl _ ->
+      assert false     (* should not occur in unblocked code *)
+  in stm s
+
+(* Generic transformation of a function definition *)
+
+let fundef trstmt env f =
+  reset_temps();
+  let newbody = trstmt env f.fd_body in
+  let temps = get_temps() in
+  {f with fd_locals = f.fd_locals @ temps; fd_body = newbody}
+
+(* Generic transformation of a program *)
 
 let program
     ?(decl = fun env d -> d)
diff --git a/cparser/Transform.mli b/cparser/Transform.mli
index 8f2c5f8..8215997 100644
--- a/cparser/Transform.mli
+++ b/cparser/Transform.mli
@@ -13,13 +13,29 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(* Generic program transformation *)
-
+(** Creation of fresh temporary variables. *)
 val reset_temps : unit -> unit
 val new_temp_var : ?name:string -> C.typ -> C.ident
 val new_temp : ?name:string -> C.typ -> C.exp
 val get_temps : unit -> C.decl list
 
+(** Avoiding repeated evaluation of a l-value *)
+
+val bind_lvalue: Env.t -> C.exp -> (C.exp -> C.exp) -> C.exp
+
+(** Generic transformation of a statement *)
+
+type context = Val | Effects
+
+val stmt : (C.location -> Env.t -> context -> C.exp -> C.exp) ->
+           Env.t -> C.stmt -> C.stmt
+
+(** Generic transformation of a function definition *)
+
+val fundef : (Env.t -> C.stmt -> C.stmt) -> Env.t -> C.fundef -> C.fundef
+
+(** Generic transformation of a program *)
+
 val program :
   ?decl:(Env.t -> C.decl -> C.decl) ->
   ?fundef:(Env.t -> C.fundef -> C.fundef) ->