diff options
| -rw-r--r-- | cparser/Bitfields.ml | 48 | ||||
| -rw-r--r-- | cparser/Cutil.ml | 12 | ||||
| -rw-r--r-- | cparser/Makefile | 2 | ||||
| -rw-r--r-- | cparser/PackedStructs.ml | 41 | ||||
| -rw-r--r-- | cparser/Parse.ml | 8 | ||||
| -rw-r--r-- | cparser/SimplVolatile.ml | 138 | ||||
| -rw-r--r-- | cparser/StructAssign.ml | 97 | ||||
| -rw-r--r-- | cparser/StructByValue.ml | 20 | ||||
| -rw-r--r-- | cparser/Transform.ml | 48 | ||||
| -rw-r--r-- | cparser/Transform.mli | 20 |
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) -> |