summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--cparser/Bitfields.ml48
-rw-r--r--cparser/Cutil.ml12
-rw-r--r--cparser/Makefile2
-rw-r--r--cparser/PackedStructs.ml41
-rw-r--r--cparser/Parse.ml8
-rw-r--r--cparser/SimplVolatile.ml138
-rw-r--r--cparser/StructAssign.ml97
-rw-r--r--cparser/StructByValue.ml20
-rw-r--r--cparser/Transform.ml48
-rw-r--r--cparser/Transform.mli20
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) ->