diff options
Diffstat (limited to 'cparser')
-rw-r--r-- | cparser/.depend | 34 | ||||
-rw-r--r-- | cparser/AddCasts.ml | 243 | ||||
-rw-r--r-- | cparser/AddCasts.mli | 16 | ||||
-rw-r--r-- | cparser/Elab.ml | 4 | ||||
-rw-r--r-- | cparser/Makefile | 4 | ||||
-rw-r--r-- | cparser/Parse.ml | 14 | ||||
-rw-r--r-- | cparser/SimplExpr.ml | 568 | ||||
-rw-r--r-- | cparser/SimplExpr.mli | 20 | ||||
-rw-r--r-- | cparser/SimplVolatile.ml | 81 | ||||
-rw-r--r-- | cparser/StructAssign.ml | 165 | ||||
-rw-r--r-- | cparser/StructAssign.mli | 18 | ||||
-rw-r--r-- | cparser/StructReturn.ml (renamed from cparser/StructByValue.ml) | 107 | ||||
-rw-r--r-- | cparser/StructReturn.mli (renamed from cparser/StructByValue.mli) | 0 |
13 files changed, 31 insertions, 1243 deletions
diff --git a/cparser/.depend b/cparser/.depend index 51f3b5ea..4a7f5385 100644 --- a/cparser/.depend +++ b/cparser/.depend @@ -1,4 +1,3 @@ -AddCasts.cmi: C.cmi Bitfields.cmi: C.cmi Builtins.cmi: Env.cmi C.cmi C.cmi: @@ -12,18 +11,13 @@ Errors.cmi: GCC.cmi: Builtins.cmi Lexer.cmi: Parser.cmi Machine.cmi: -PackedStructs.cmi: C.cmi Parse.cmi: C.cmi Parse_aux.cmi: Parser.cmi: Cabs.cmo Rename.cmi: C.cmi -SimplExpr.cmi: C.cmi -StructAssign.cmi: C.cmi -StructByValue.cmi: C.cmi +StructReturn.cmi: C.cmi Transform.cmi: Env.cmi C.cmi Unblock.cmi: C.cmi -AddCasts.cmo: Transform.cmi Cutil.cmi C.cmi AddCasts.cmi -AddCasts.cmx: Transform.cmx Cutil.cmx C.cmi AddCasts.cmi Bitfields.cmo: Transform.cmi Machine.cmi Cutil.cmi C.cmi Bitfields.cmi Bitfields.cmx: Transform.cmx Machine.cmx Cutil.cmx C.cmi Bitfields.cmi Builtins.cmo: Env.cmi Cutil.cmi C.cmi Builtins.cmi @@ -59,31 +53,21 @@ Machine.cmx: Machine.cmi Main.cmo: Parse.cmi GCC.cmi Cprint.cmi Builtins.cmi Main.cmx: Parse.cmx GCC.cmx Cprint.cmx Builtins.cmx PackedStructs.cmo: Transform.cmi Machine.cmi Errors.cmi Env.cmi Cutil.cmi \ - C.cmi Builtins.cmi PackedStructs.cmi + Cprint.cmi C.cmi Builtins.cmi PackedStructs.cmx: Transform.cmx Machine.cmx Errors.cmx Env.cmx Cutil.cmx \ - C.cmi Builtins.cmx PackedStructs.cmi -Parse.cmo: Unblock.cmi StructByValue.cmi StructAssign.cmi SimplVolatile.cmo \ - SimplExpr.cmi Rename.cmi PackedStructs.cmi Errors.cmi Elab.cmi \ - Bitfields.cmi AddCasts.cmi Parse.cmi -Parse.cmx: Unblock.cmx StructByValue.cmx StructAssign.cmx SimplVolatile.cmx \ - SimplExpr.cmx Rename.cmx PackedStructs.cmx Errors.cmx Elab.cmx \ - Bitfields.cmx AddCasts.cmx Parse.cmi + Cprint.cmx C.cmi Builtins.cmx +Parse.cmo: Unblock.cmi StructReturn.cmi Rename.cmi PackedStructs.cmo \ + Errors.cmi Elab.cmi Bitfields.cmi Parse.cmi +Parse.cmx: Unblock.cmx StructReturn.cmx Rename.cmx PackedStructs.cmx \ + Errors.cmx Elab.cmx Bitfields.cmx Parse.cmi Parse_aux.cmo: Errors.cmi Cabshelper.cmo Parse_aux.cmi Parse_aux.cmx: Errors.cmx Cabshelper.cmx Parse_aux.cmi Parser.cmo: Parse_aux.cmi Cabshelper.cmo Cabs.cmo Parser.cmi Parser.cmx: Parse_aux.cmx Cabshelper.cmx Cabs.cmx Parser.cmi Rename.cmo: Errors.cmi Cutil.cmi C.cmi Builtins.cmi Rename.cmi Rename.cmx: Errors.cmx Cutil.cmx C.cmi Builtins.cmx Rename.cmi -SimplExpr.cmo: Transform.cmi Errors.cmi Cutil.cmi C.cmi SimplExpr.cmi -SimplExpr.cmx: Transform.cmx Errors.cmx Cutil.cmx C.cmi SimplExpr.cmi -SimplVolatile.cmo: Transform.cmi Cutil.cmi C.cmi -SimplVolatile.cmx: Transform.cmx Cutil.cmx C.cmi -StructAssign.cmo: Transform.cmi Machine.cmi Errors.cmi Env.cmi Cutil.cmi \ - C.cmi StructAssign.cmi -StructAssign.cmx: Transform.cmx Machine.cmx Errors.cmx Env.cmx Cutil.cmx \ - C.cmi StructAssign.cmi -StructByValue.cmo: Transform.cmi Env.cmi Cutil.cmi C.cmi StructByValue.cmi -StructByValue.cmx: Transform.cmx Env.cmx Cutil.cmx C.cmi StructByValue.cmi +StructReturn.cmo: Transform.cmi Env.cmi Cutil.cmi C.cmi StructReturn.cmi +StructReturn.cmx: Transform.cmx Env.cmx Cutil.cmx C.cmi StructReturn.cmi Transform.cmo: Env.cmi Cutil.cmi C.cmi Builtins.cmi Transform.cmi Transform.cmx: Env.cmx Cutil.cmx C.cmi Builtins.cmx Transform.cmi Unblock.cmo: Transform.cmi Errors.cmi Cutil.cmi C.cmi Unblock.cmi diff --git a/cparser/AddCasts.ml b/cparser/AddCasts.ml deleted file mode 100644 index eb3fa08a..00000000 --- a/cparser/AddCasts.ml +++ /dev/null @@ -1,243 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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. *) -(* *) -(* *********************************************************************) - -(* Materialize implicit casts *) - -(* Assumes: simplified code - Produces: simplified code - Preserves: unblocked code *) - -open C -open Cutil -open Transform - -(* We have the option of materializing all casts or leave "widening" - casts implicit. Widening casts are: -- from a small integer type to a larger integer type, - provided both types have the same signedness; -- from a small float type to a larger float type; -- from a pointer type to void *. -*) - -let omit_widening_casts = ref false - -let widening_cast env tfrom tto = - begin match unroll env tfrom, unroll env tto with - | TInt(k1, _), TInt(k2, _) -> - integer_rank k1 <= integer_rank k2 - && is_signed_ikind k1 = is_signed_ikind k2 - | TFloat(k1, _), TFloat(k2, _) -> - float_rank k1 <= float_rank k2 - | TPtr(ty1, _), TPtr(ty2, _) -> is_void_type env ty2 - | _, _ -> false - end - -let cast_not_needed env tfrom tto = - let tfrom = pointer_decay env tfrom - and tto = pointer_decay env tto in - compatible_types env tfrom tto - || (!omit_widening_casts && widening_cast env tfrom tto) - -let cast env e tto = - if cast_not_needed env e.etyp tto - then e - else {edesc = ECast(tto, e); etyp = tto} - -(* Note: this pass applies only to simplified expressions - because casts cannot be materialized in op= expressions... *) - -let rec add_expr env e = - match e.edesc with - | EConst _ -> e - | EVar _ -> e - | ESizeof _ -> e - | EUnop(op, e1) -> - let e1' = add_expr env e1 in - let desc = - match op with - | Ominus | Oplus | Onot -> - EUnop(op, cast env e1' e.etyp) - | Olognot | Oderef | Oaddrof - | Odot _ | Oarrow _ -> - EUnop(op, e1') - | Opreincr | Opredecr | Opostincr | Opostdecr -> - assert false (* not simplified *) - in { edesc = desc; etyp = e.etyp } - | EBinop(op, e1, e2, ty) -> - let e1' = add_expr env e1 in - let e2' = add_expr env e2 in - let desc = - match op with - | Oadd -> - if is_pointer_type env ty - then EBinop(Oadd, e1', e2', ty) - else EBinop(Oadd, cast env e1' ty, cast env e2' ty, ty) - | Osub -> - if is_pointer_type env ty - then EBinop(Osub, e1', e2', ty) - else EBinop(Osub, cast env e1' ty, cast env e2' ty, ty) - | Omul|Odiv|Omod|Oand|Oor|Oxor|Oeq|One|Olt|Ogt|Ole|Oge -> - EBinop(op, cast env e1' ty, cast env e2' ty, ty) - | Oshl|Oshr -> - EBinop(op, cast env e1' ty, e2', ty) - | Oindex | Ologand | Ologor | Ocomma -> - EBinop(op, e1', e2', ty) - | Oassign - | Oadd_assign|Osub_assign|Omul_assign|Odiv_assign|Omod_assign - | Oand_assign|Oor_assign|Oxor_assign|Oshl_assign|Oshr_assign -> - assert false (* not simplified *) - in { edesc = desc; etyp = e.etyp } - | EConditional(e1, e2, e3) -> - { edesc = - EConditional(add_expr env e1, add_expr env e2, add_expr env e3); - etyp = e.etyp } - | ECast(ty, e1) -> - { edesc = ECast(ty, add_expr env e1); etyp = e.etyp } - | ECall(e1, el) -> - assert false (* not simplified *) - -(* Arguments to a prototyped function *) - -let rec add_proto env args params = - match args, params with - | [], _ -> [] - | _::_, [] -> add_noproto env args - | arg1 :: argl, (_, ty_p) :: paraml -> - cast env (add_expr env arg1) ty_p :: - add_proto env argl paraml - -(* Arguments to a non-prototyped function *) - -and add_noproto env args = - match args with - | [] -> [] - | arg1 :: argl -> - cast env (add_expr env arg1) (default_argument_conversion env arg1.etyp) :: - add_noproto env argl - -(* Arguments to function calls in general *) - -let add_arguments env ty_fun args = - let ty_args = - match unroll env ty_fun with - | TFun(res, args, vararg, a) -> args - | TPtr(ty, a) -> - begin match unroll env ty with - | TFun(res, args, vararg, a) -> args - | _ -> assert false - end - | _ -> assert false in - match ty_args with - | None -> add_noproto env args - | Some targs -> add_proto env args targs - -(* Toplevel expressions (appearing in Sdo statements) *) - -let add_topexpr env loc e = - match e.edesc with - | EBinop(Oassign, lhs, {edesc = ECall(e1, el); etyp = ty}, _) -> - let ecall = - {edesc = ECall(add_expr env e1, add_arguments env e1.etyp el); - etyp = ty} in - if cast_not_needed env ty lhs.etyp then - sassign loc (add_expr env lhs) ecall - else begin - let tmp = new_temp (erase_attributes_type env ty) in - sseq loc (sassign loc tmp ecall) - (sassign loc (add_expr env lhs) (cast env tmp lhs.etyp)) - end - | EBinop(Oassign, lhs, rhs, _) -> - sassign loc (add_expr env lhs) (cast env (add_expr env rhs) lhs.etyp) - | ECall(e1, el) -> - let ecall = - {edesc = ECall(add_expr env e1, add_arguments env e1.etyp el); - etyp = e.etyp} in - {sdesc = Sdo ecall; sloc = loc} - | _ -> - assert false - -(* Initializers *) - -let rec add_init env tto = function - | Init_single e -> - Init_single (cast env (add_expr env e) tto) - | Init_array il -> - let ty_elt = - match unroll env tto with - | TArray(ty, _, _) -> ty | _ -> assert false in - Init_array (List.map (add_init env ty_elt) il) - | Init_struct(id, fil) -> - Init_struct (id, List.map - (fun (fld, i) -> (fld, add_init env fld.fld_typ i)) - fil) - | Init_union(id, fld, i) -> - Init_union(id, fld, add_init env fld.fld_typ i) - -(* Declarations *) - -let add_decl env (sto, id, ty, optinit) = - (sto, id, ty, - begin match optinit with - | None -> None - | Some init -> Some(add_init env ty init) - end) - -(* Statements *) - -let rec add_stmt env f s = - match s.sdesc with - | Sskip -> s - | Sdo e -> add_topexpr env s.sloc e - | Sseq(s1, s2) -> - {sdesc = Sseq(add_stmt env f s1, add_stmt env f s2); sloc = s.sloc } - | Sif(e, s1, s2) -> - {sdesc = Sif(add_expr env e, add_stmt env f s1, add_stmt env f s2); - sloc = s.sloc} - | Swhile(e, s1) -> - {sdesc = Swhile(add_expr env e, add_stmt env f s1); - sloc = s.sloc} - | Sdowhile(s1, e) -> - {sdesc = Sdowhile(add_stmt env f s1, add_expr env e); - sloc = s.sloc} - | Sfor(s1, e, s2, s3) -> - {sdesc = Sfor(add_stmt env f s1, add_expr env e, add_stmt env f s2, - add_stmt env f s3); - sloc = s.sloc} - | Sbreak -> s - | Scontinue -> s - | Sswitch(e, s1) -> - {sdesc = Sswitch(add_expr env e, add_stmt env f s1); sloc = s.sloc} - | Slabeled(lbl, s) -> - {sdesc = Slabeled(lbl, add_stmt env f s); sloc = s.sloc} - | Sgoto lbl -> s - | Sreturn None -> s - | Sreturn (Some e) -> - {sdesc = Sreturn(Some(cast env (add_expr env e) f.fd_ret)); sloc = s.sloc} - | Sblock sl -> - {sdesc = Sblock(List.map (add_stmt env f) sl); sloc = s.sloc} - | Sdecl d -> - {sdesc = Sdecl(add_decl env d); sloc = s.sloc} - -let add_fundef env f = - reset_temps(); - let body' = add_stmt env f f.fd_body in - let temps = get_temps () in - (* fd_locals have no initializers, so no need to transform them *) - { f with fd_locals = f.fd_locals @ temps; fd_body = body' } - - -let program ?(all = false) p = - omit_widening_casts := not all; - Transform.program ~decl:add_decl ~fundef:add_fundef p diff --git a/cparser/AddCasts.mli b/cparser/AddCasts.mli deleted file mode 100644 index 318ecc66..00000000 --- a/cparser/AddCasts.mli +++ /dev/null @@ -1,16 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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. *) -(* *) -(* *********************************************************************) - -val program: ?all: bool -> C.program -> C.program diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 870385de..2da19368 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1508,13 +1508,13 @@ let rec enter_decdefs local loc env = function (* check for incomplete type *) if sto' <> Storage_extern && incomplete_type env ty' then warning loc "'%s' has incomplete type" s; - if local && sto <> Storage_extern && sto <> Storage_static then begin + if local && sto' <> Storage_extern && sto' <> Storage_static then begin (* Local definition *) let (decls, env3) = enter_decdefs local loc env2 rem in ((sto', id, ty', init') :: decls, env3) end else begin (* Global definition *) - emit_elab (elab_loc loc) (Gdecl(sto, id, ty', init')); + emit_elab (elab_loc loc) (Gdecl(sto', id, ty', init')); enter_decdefs local loc env2 rem end diff --git a/cparser/Makefile b/cparser/Makefile index 527cdd32..da2c28b0 100644 --- a/cparser/Makefile +++ b/cparser/Makefile @@ -15,8 +15,8 @@ SRCS=Errors.ml Cabs.ml Cabshelper.ml Parse_aux.ml Parser.ml Lexer.ml \ Builtins.ml GCC.ml \ Cleanup.ml Elab.ml Rename.ml \ Transform.ml \ - Unblock.ml SimplExpr.ml AddCasts.ml StructByValue.ml StructAssign.ml \ - Bitfields.ml PackedStructs.ml SimplVolatile.ml \ + Unblock.ml StructReturn.ml \ + Bitfields.ml PackedStructs.ml \ Parse.ml COBJS=uint64.o diff --git a/cparser/Parse.ml b/cparser/Parse.ml index dcd01e93..2c467a76 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -20,28 +20,18 @@ module CharSet = Set.Make(struct type t = char let compare = compare end) 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 SimplVolatile.program 'v' - (run_pass StructAssign.program 'S' - (run_pass StructByValue.program 's' + (run_pass StructReturn.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 let set s = String.iter (fun c -> t := CharSet.add c !t) s in String.iter (function 'b' -> set "b" - | 'e' -> set "e" - | 'c' -> set "ec" - | 'C' -> set "ecC" | 's' -> set "s" - | 'S' -> set "bsS" - | 'v' -> set "v" - | 'V' -> set "eV" | 'f' -> set "bf" | 'p' -> set "bp" | _ -> ()) diff --git a/cparser/SimplExpr.ml b/cparser/SimplExpr.ml deleted file mode 100644 index 4184d954..00000000 --- a/cparser/SimplExpr.ml +++ /dev/null @@ -1,568 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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. *) -(* *) -(* *********************************************************************) - -(* Pulling side-effects out of expressions *) - -(* Assumes: nothing - Produces: simplified code *) - -open C -open Cutil -open Transform - -(* Grammar of simplified expressions: - e ::= EConst cst - | ESizeof ty - | EVar id - | EUnop pure-unop e - | EBinop pure-binop e e - | EConditional e e e - | ECast ty e - - Grammar of statements produced to reflect side-effects in expressions: - s ::= Sskip - | Sdo (EBinop Oassign e e) - | Sdo (EBinop Oassign e (ECall e e* )) - | Sdo (Ecall e el) - | Sseq s s - | Sif e s s -*) - -let rec is_simpl_expr e = - match e.edesc with - | EConst cst -> true - | ESizeof ty -> true - | EVar id -> true - | EUnop((Ominus|Oplus|Olognot|Onot|Oderef|Oaddrof), e1) -> - is_simpl_expr e1 - | EBinop((Oadd|Osub|Omul|Odiv|Omod|Oand|Oor|Oxor|Oshl|Oshr| - Oeq|One|Olt|Ogt|Ole|Oge|Oindex|Ologand|Ologor), e1, e2, _) -> - is_simpl_expr e1 && is_simpl_expr e2 - | EConditional(e1, e2, e3) -> - is_simpl_expr e1 && is_simpl_expr e2 && is_simpl_expr e3 - | ECast(ty, e1) -> - is_simpl_expr e1 - | _ -> - false - -(* "Destination" of a simplified expression *) - -type exp_destination = - | RHS (* evaluate as a r-value *) - | LHS (* evaluate as a l-value *) - | Drop (* drop its value, we only need the side-effects *) - | Set of exp (* assign it to the given simplified l.h.s. *) - -let voidconst = { nullconst with etyp = TVoid [] } - -(* Reads from volatile lvalues are also considered as side-effects if - [volatilize] is true. *) - -let volatilize = ref false - -(* [simpl_expr loc env e act] returns a pair [s, e'] of - a statement that performs the side-effects present in [e] and - a simplified, side-effect-free expression [e']. - If [act] is [RHS], [e'] evaluates to the same value as [e]. - If [act] is [LHS], [e'] evaluates to the same location as [e]. - If [act] is [Drop], [e'] is not meaningful and must be ignored. - If [act] is [Set lhs], [s] also performs an assignment - equivalent to [lhs = e]. [e'] is not meaningful. *) - -let simpl_expr loc env e act = - - (* Temporaries should not be [const] because we assign into them, - and need not be [volatile] because no one else is writing into them. - As for [restrict] it doesn't make sense anyway. *) - - let new_temp ty = - Transform.new_temp (erase_attributes_type env ty) in - - let eboolvalof e = - { edesc = EBinop(One, e, intconst 0L IInt, TInt(IInt, [])); - etyp = TInt(IInt, []) } in - - let sseq s1 s2 = Cutil.sseq loc s1 s2 in - - let sassign e1 e2 = - { sdesc = Sdo {edesc = EBinop(Oassign, e1, e2, e1.etyp); etyp = e1.etyp}; - sloc = loc } in - - let sif e s1 s2 = - { sdesc = Sif(e, s1, s2); sloc = loc } in - - let is_volatile_read e = - !volatilize - && List.mem AVolatile (attributes_of_type env e.etyp) - && is_lvalue e in - - let lhs_to_rhs e = - if is_volatile_read e - then (let t = new_temp e.etyp in (sassign t e, t)) - else (sskip, e) in - - let finish act s e = - match act with - | RHS -> - if is_volatile_read e - then (let t = new_temp e.etyp in (sseq s (sassign t e), t)) - else (s, e) - | LHS -> - (s, e) - | Drop -> - if is_volatile_read e - then (let t = new_temp e.etyp in (sseq s (sassign t e), voidconst)) - else (s, voidconst) - | Set lhs -> - if is_volatile_read e - then (let t = new_temp e.etyp in - (sseq s (sseq (sassign t e) (sassign lhs t)), voidconst)) - else (sseq s (sassign lhs e), voidconst) in - - let rec simpl e act = - match e.edesc with - - | EConst cst -> - finish act sskip e - - | ESizeof ty -> - finish act sskip e - - | EVar id -> - finish act sskip e - - | EUnop(op, e1) -> - - begin match op with - - | Ominus | Oplus | Olognot | Onot | Oderef | Oarrow _ -> - let (s1, e1') = simpl e1 RHS in - finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp} - - | Oaddrof -> - let (s1, e1') = simpl e1 LHS in - finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp} - - | Odot _ -> - let (s1, e1') = simpl e1 (if act = LHS then LHS else RHS) in - finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp} - - | Opreincr | Opredecr -> - let (s1, e1') = simpl e1 LHS in - let (s2, e2') = lhs_to_rhs e1' in - let op' = match op with Opreincr -> Oadd | _ -> Osub in - let ty = unary_conversion env e.etyp in - let e3 = - {edesc = EBinop(op', e2', intconst 1L IInt, ty); etyp = ty} in - begin match act with - | Drop -> - (sseq s1 (sseq s2 (sassign e1' e3)), voidconst) - | _ -> - let tmp = new_temp e.etyp in - finish act (sseq s1 (sseq s2 (sseq (sassign tmp e3) - (sassign e1' tmp)))) - tmp - end - - | Opostincr | Opostdecr -> - let (s1, e1') = simpl e1 LHS in - let op' = match op with Opostincr -> Oadd | _ -> Osub in - let ty = unary_conversion env e.etyp in - begin match act with - | Drop -> - let (s2, e2') = lhs_to_rhs e1' in - let e3 = - {edesc = EBinop(op', e2', intconst 1L IInt, ty); etyp = ty} in - (sseq s1 (sseq s2 (sassign e1' e3)), voidconst) - | _ -> - let tmp = new_temp e.etyp in - let e3 = - {edesc = EBinop(op', tmp, intconst 1L IInt, ty); etyp = ty} in - finish act (sseq s1 (sseq (sassign tmp e1') (sassign e1' e3))) - tmp - end - - end - - | EBinop(op, e1, e2, ty) -> - - begin match op with - - | Oadd | Osub | Omul | Odiv | Omod | Oand | Oor | Oxor - | Oshl | Oshr | Oeq | One | Olt | Ogt | Ole | Oge | Oindex -> - let (s1, e1') = simpl e1 RHS in - let (s2, e2') = simpl e2 RHS in - finish act (sseq s1 s2) - {edesc = EBinop(op, e1', e2', ty); etyp = e.etyp} - - | Oassign -> - if act = Drop && is_simpl_expr e1 then - simpl e2 (Set e1) - else begin - match act with - | Drop -> - let (s1, e1') = simpl e1 LHS in - let (s2, e2') = simpl e2 RHS in - (sseq s1 (sseq s2 (sassign e1' e2')), voidconst) - | _ -> - let tmp = new_temp e.etyp in - let (s1, e1') = simpl e1 LHS in - let (s2, e2') = simpl e2 (Set tmp) in - finish act (sseq s1 (sseq s2 (sassign e1' tmp))) - tmp - end - - | Oadd_assign | Osub_assign | Omul_assign | Odiv_assign - | Omod_assign | Oand_assign | Oor_assign | Oxor_assign - | Oshl_assign | Oshr_assign -> - let (s1, e1') = simpl e1 LHS in - let (s11, e11') = lhs_to_rhs e1' in - let (s2, e2') = simpl e2 RHS in - 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 e3 = - { edesc = EBinop(op', e11', e2', ty); etyp = ty } in - begin match act with - | Drop -> - (sseq s1 (sseq s11 (sseq s2 (sassign e1' e3))), voidconst) - | _ -> - let tmp = new_temp e.etyp in - finish act (sseq s1 (sseq s11 (sseq s2 - (sseq (sassign tmp e3) (sassign e1' tmp))))) - tmp - end - - | Ocomma -> - let (s1, _) = simpl e1 Drop in - let (s2, e2') = simpl e2 act in - (sseq s1 s2, e2') - - | Ologand -> - let (s1, e1') = simpl e1 RHS in - if is_simpl_expr e2 then begin - finish act s1 - {edesc = EBinop(Ologand, e1', e2, ty); etyp = e.etyp} - end else begin - match act with - | Drop -> - let (s2, _) = simpl e2 Drop in - (sseq s1 (sif e1' s2 sskip), voidconst) - | RHS | LHS -> (* LHS should not happen *) - let (s2, e2') = simpl e2 RHS in - let tmp = new_temp e.etyp in - (sseq s1 (sif e1' - (sseq s2 (sassign tmp (eboolvalof e2'))) - (sassign tmp (intconst 0L IInt))), - tmp) - | Set lv -> - let (s2, e2') = simpl e2 RHS in - (sseq s1 (sif e1' - (sseq s2 (sassign lv (eboolvalof e2'))) - (sassign lv (intconst 0L IInt))), - voidconst) - end - - | Ologor -> - let (s1, e1') = simpl e1 RHS in - if is_simpl_expr e2 then begin - finish act s1 - {edesc = EBinop(Ologor, e1', e2, ty); etyp = e.etyp} - end else begin - match act with - | Drop -> - let (s2, _) = simpl e2 Drop in - (sseq s1 (sif e1' sskip s2), voidconst) - | RHS | LHS -> (* LHS should not happen *) - let (s2, e2') = simpl e2 RHS in - let tmp = new_temp e.etyp in - (sseq s1 (sif e1' - (sassign tmp (intconst 1L IInt)) - (sseq s2 (sassign tmp (eboolvalof e2')))), - tmp) - | Set lv -> - let (s2, e2') = simpl e2 RHS in - (sseq s1 (sif e1' - (sassign lv (intconst 1L IInt)) - (sseq s2 (sassign lv (eboolvalof e2')))), - voidconst) - end - - end - - | EConditional(e1, e2, e3) -> - let (s1, e1') = simpl e1 RHS in - if is_simpl_expr e2 && is_simpl_expr e3 then begin - finish act s1 {edesc = EConditional(e1', e2, e3); etyp = e.etyp} - end else begin - match act with - | Drop -> - let (s2, _) = simpl e2 Drop in - let (s3, _) = simpl e3 Drop in - (sseq s1 (sif e1' s2 s3), voidconst) - | RHS | LHS -> (* LHS should not happen *) - let tmp = new_temp e.etyp in - let (s2, _) = simpl e2 (Set tmp) in - let (s3, _) = simpl e3 (Set tmp) in - (sseq s1 (sif e1' s2 s3), tmp) - | Set lv -> - let (s2, _) = simpl e2 (Set lv) in - let (s3, _) = simpl e3 (Set lv) in - (sseq s1 (sif e1' s2 s3), voidconst) - end - - | ECast(ty, e1) -> - if is_void_type env ty then begin - if act <> Drop then - Errors.warning "%acast to 'void' in a context expecting a value\n" - formatloc loc; - simpl e1 act - end else begin - let (s1, e1') = simpl e1 RHS in - finish act s1 {edesc = ECast(ty, e1'); etyp = e.etyp} - end - - | ECall(e1, el) -> - let (s1, e1') = simpl e1 RHS in - let (s2, el') = simpl_list el in - let e2 = { edesc = ECall(e1', el'); etyp = e.etyp } in - begin match act with - | Drop -> - (sseq s1 (sseq s2 {sdesc = Sdo e2; sloc=loc}), voidconst) - | Set({edesc = EVar _} as lhs) -> - (* CompCert wants the destination of a call to be a variable, - not a more complex lhs. In the latter case, we - fall through the catch-all case below *) - (sseq s1 (sseq s2 (sassign lhs e2)), voidconst) - | _ -> - let tmp = new_temp e.etyp in - finish act (sseq s1 (sseq s2 (sassign tmp e2))) tmp - end - - and simpl_list = function - | [] -> (sskip, []) - | e1 :: el -> - let (s1, e1') = simpl e1 RHS in - let (s2, el') = simpl_list el in - (sseq s1 s2, e1' :: el') - - in simpl e act - -(* Simplification of an initializer *) - -let simpl_initializer loc env i = - - let rec simpl_init = function - | Init_single e -> - let (s, e') = simpl_expr loc env e RHS in - (s, Init_single e) - | Init_array il -> - let rec simpl = function - | [] -> (sskip, []) - | i1 :: il -> - let (s1, i1') = simpl_init i1 in - let (s2, il') = simpl il in - (sseq loc s1 s2, i1' :: il') in - let (s, il') = simpl il in - (s, Init_array il') - | Init_struct(id, il) -> - let rec simpl = function - | [] -> (sskip, []) - | (f1, i1) :: il -> - let (s1, i1') = simpl_init i1 in - let (s2, il') = simpl il in - (sseq loc s1 s2, (f1, i1') :: il') in - let (s, il') = simpl il in - (s, Init_struct(id, il')) - | Init_union(id, f, i) -> - let (s, i') = simpl_init i in - (s, Init_union(id, f, i')) - - in simpl_init i - -(* Construct a simplified statement equivalent to [if (e) s1; else s2;]. - Optimizes the case where e contains [&&] or [||] or [?]. - [s1] or [s2] can be duplicated, so use only for small [s1] and [s2] - that do not define any labels. *) - -let rec simpl_if loc env e s1 s2 = - match e.edesc with - | EUnop(Olognot, e1) -> - simpl_if loc env e1 s2 s1 - | EBinop(Ologand, e1, e2, _) -> - simpl_if loc env e1 - (simpl_if loc env e2 s1 s2) - s2 - | EBinop(Ologor, e1, e2, _) -> - simpl_if loc env e1 - s1 - (simpl_if loc env e2 s1 s2) - | EConditional(e1, e2, e3) -> - simpl_if loc env e1 - (simpl_if loc env e2 s1 s2) - (simpl_if loc env e3 s1 s2) - | _ -> - let (s, e') = simpl_expr loc env e RHS in - sseq loc s {sdesc = Sif(e', s1, s2); sloc = loc} - -(* Trivial statements for which [simpl_if] is applicable *) - -let trivial_stmt s = - match s.sdesc with - | Sskip | Scontinue | Sbreak | Sgoto _ -> true - | _ -> false - -(* Construct a simplified statement equivalent to [if (!e) exit; ]. *) - -let break_if_false loc env e = - simpl_if loc env e - {sdesc = Sskip; sloc = loc} - {sdesc = Sbreak; sloc = loc} - -(* Simplification of a statement *) - -let simpl_statement env s = - - let rec simpl_stmt s = - match s.sdesc with - - | Sskip -> - s - - | Sdo e -> - let (s', _) = simpl_expr s.sloc env e Drop in - s' - - | Sseq(s1, s2) -> - {sdesc = Sseq(simpl_stmt s1, simpl_stmt s2); sloc = s.sloc} - - | Sif(e, s1, s2) -> - if trivial_stmt s1 && trivial_stmt s2 then - simpl_if s.sloc env e (simpl_stmt s1) (simpl_stmt s2) - else begin - let (s', e') = simpl_expr s.sloc env e RHS in - sseq s.sloc s' - {sdesc = Sif(e', simpl_stmt s1, simpl_stmt s2); - sloc = s.sloc} - end - - | Swhile(e, s1) -> - if is_simpl_expr e then - {sdesc = Swhile(e, simpl_stmt s1); sloc = s.sloc} - else - {sdesc = - Swhile(intconst 1L IInt, - sseq s.sloc (break_if_false s.sloc env e) - (simpl_stmt s1)); - sloc = s.sloc} - - | Sdowhile(s1, e) -> - if is_simpl_expr e then - {sdesc = Sdowhile(simpl_stmt s1, e); sloc = s.sloc} - else begin - let tmp = new_temp (TInt(IInt, [])) in - let (s', _) = simpl_expr s.sloc env e (Set tmp) in - let s_init = - {sdesc = Sdo {edesc = EBinop(Oassign, tmp, intconst 1L IInt, tmp.etyp); - etyp = tmp.etyp}; - sloc = s.sloc} in - {sdesc = Sfor(s_init, tmp, s', simpl_stmt s1); sloc = s.sloc} - end -(*** Alternate translation that unfortunately puts a "break" in the - "next" part of a "for", something that is not supported - by Clight semantics, and has unknown behavior in gcc. - {sdesc = - Sfor(sskip, - intconst 1L IInt, - break_if_false s.sloc env e, - simpl_stmt s1); - sloc = s.sloc} -***) - - | Sfor(s1, e, s2, s3) -> - if is_simpl_expr e then - {sdesc = Sfor(simpl_stmt s1, - e, - simpl_stmt s2, - simpl_stmt s3); - sloc = s.sloc} - else - let (s', e') = simpl_expr s.sloc env e RHS in - {sdesc = Sfor(sseq s.sloc (simpl_stmt s1) s', - e', - sseq s.sloc (simpl_stmt s2) s', - simpl_stmt s3); - sloc = s.sloc} - - | Sbreak -> - s - | Scontinue -> - s - - | Sswitch(e, s1) -> - let (s', e') = simpl_expr s.sloc env e RHS in - sseq s.sloc s' {sdesc = Sswitch(e', simpl_stmt s1); sloc = s.sloc} - - | Slabeled(lbl, s1) -> - {sdesc = Slabeled(lbl, simpl_stmt s1); sloc = s.sloc} - - | Sgoto lbl -> - s - - | Sreturn None -> - s - - | Sreturn (Some e) -> - let (s', e') = simpl_expr s.sloc env e RHS in - sseq s.sloc s' {sdesc = Sreturn(Some e'); sloc = s.sloc} - - | Sblock sl -> - {sdesc = Sblock(simpl_block sl); sloc = s.sloc} - - | Sdecl d -> assert false - - and simpl_block = function - | [] -> [] - | ({sdesc = Sdecl(sto, id, ty, None)} as s) :: sl -> - s :: simpl_block sl - | ({sdesc = Sdecl(sto, id, ty, Some i)} as s) :: sl -> - let (s', i') = simpl_initializer s.sloc env i in - let sl' = - {sdesc = Sdecl(sto, id, ty, Some i'); sloc = s.sloc} - :: simpl_block sl in - if s'.sdesc = Sskip then sl' else s' :: sl' - | s :: sl -> - simpl_stmt s :: simpl_block sl - - in simpl_stmt s - -(* Simplification of a function definition *) - -let simpl_fundef env f = - reset_temps(); - let body' = simpl_statement env f.fd_body in - let temps = get_temps() in - { f with fd_locals = f.fd_locals @ temps; fd_body = body' } - -(* Entry point *) - -let program ?(volatile = false) p = - volatilize := volatile; - Transform.program ~fundef:simpl_fundef p diff --git a/cparser/SimplExpr.mli b/cparser/SimplExpr.mli deleted file mode 100644 index cdeb30cf..00000000 --- a/cparser/SimplExpr.mli +++ /dev/null @@ -1,20 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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. *) -(* *) -(* *********************************************************************) - -(* Pulling side effects out of expressions. - If [volatile] is [true], treats reads from volatile rvalues - as side-effects *) - -val program: ?volatile: bool -> C.program -> C.program diff --git a/cparser/SimplVolatile.ml b/cparser/SimplVolatile.ml deleted file mode 100644 index ef7a3a06..00000000 --- a/cparser/SimplVolatile.ml +++ /dev/null @@ -1,81 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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 - -(* 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 -> - expand_preincrdecr ~read:(fun e -> e) ~write:eassign - env ctx op (texp Val e1) - | EUnop((Opostincr|Opostdecr as op), e1) when is_volatile e1.etyp -> - expand_postincrdecr ~read:(fun e -> e) ~write:eassign - env ctx op (texp Val e1) - | EUnop(op, e1) -> - {edesc = EUnop(op, texp Val e1); etyp = e.etyp} - | EBinop(Oassign, e1, e2, ty) when is_volatile e1.etyp -> - expand_assign ~write:eassign env 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 -> - expand_assignop ~read:(fun e -> e) ~write:eassign - env ctx op (texp Val e1) (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 deleted file mode 100644 index d9ad8f57..00000000 --- a/cparser/StructAssign.ml +++ /dev/null @@ -1,165 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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. *) -(* *) -(* *********************************************************************) - -(* Expand assignments between structs and between unions *) - -(* Assumes: unblocked code. - Preserves: unblocked code *) - -open C -open Machine -open Cutil -open Env -open Errors -open Transform - -(* Finding appropriate memcpy functions *) - -let memcpy_decl = ref (None : ident option) - -let memcpy_type = - TFun(TPtr(TVoid [], []), - Some [(Env.fresh_ident "", TPtr(TVoid [], [])); - (Env.fresh_ident "", TPtr(TVoid [AConst], [])); - (Env.fresh_ident "", TInt(size_t_ikind, []))], - false, []) - -let lookup_function env name = - match Env.lookup_ident env name with - | (id, II_ident(sto, ty)) -> (id, ty) - | (id, II_enum _) -> raise (Env.Error(Env.Unbound_identifier name)) - -let default_memcpy () = - match !memcpy_decl with - | Some id -> - (id, memcpy_type) - | None -> - let id = Env.fresh_ident "memcpy" in - memcpy_decl := Some id; - (id, memcpy_type) - -let find_memcpy env = - try - (lookup_function env "__builtin_memcpy_aligned", true) - with Env.Error _ -> - try - (lookup_function env "__builtin_memcpy", false) - with Env.Error _ -> - try - (lookup_function env "memcpy", false) - with Env.Error _ -> - (default_memcpy(), false) - -(* Smart constructor that "bubble up" sequence expressions *) - -let rec edot f e ty = - match e.edesc with - | 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. - [lhs] and [rhs] must be l-values. *) - -let transf_assign env lhs rhs = - let al = - 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 = 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 = - if four_args - then [e_lhs; e_rhs; e_size; e_align] - else [e_lhs; e_rhs; e_size] in - {edesc = ECall(memcpy, args); etyp = TVoid[]} - -(* Transformation of expressions. *) - -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' = texp Val lhs in - let rhs' = texp Val rhs in - begin match ctx with - | Effects -> - transf_assign env lhs' rhs' - | Val -> - bind_lvalue env lhs' (fun l -> ecomma (transf_assign env l rhs') l) - end - | EConst c -> e - | ESizeof ty -> e - | EVar x -> - if ctx = Effects && is_composite_type env e.etyp - then nullconst - else e - | EUnop(Oaddrof, e1) -> - eaddrof (texp Val e1) - | EUnop(Oderef, e1) -> - if ctx = Effects && is_composite_type env 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 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 texp Effects e1 - else {edesc = EUnop(Oarrow f, texp Val e1); etyp = e.etyp} - | EUnop(op, e1) -> - {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 (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 (texp Effects e1) (texp ctx e2) - | 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 - -(* Transformation of statements *) - -let transf_stmt env s = - Transform.stmt transf_expr env s - -(* Transformation of function definitions *) - -let transf_fundef env f = - Transform.fundef transf_stmt env f - -(* Transformation of programs *) - -let program p = - memcpy_decl := None; - let p' = Transform.program ~fundef:transf_fundef p in - match !memcpy_decl with - | None -> p' - | Some id -> - {gdesc = Gdecl(Storage_extern, id, memcpy_type, None); gloc = no_loc} - :: p' diff --git a/cparser/StructAssign.mli b/cparser/StructAssign.mli deleted file mode 100644 index 55492821..00000000 --- a/cparser/StructAssign.mli +++ /dev/null @@ -1,18 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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. *) -(* *) -(* *********************************************************************) - -(* Expand assignments between structs and between unions *) - -val program: C.program -> C.program diff --git a/cparser/StructByValue.ml b/cparser/StructReturn.ml index 1b74ec52..2a4bbc19 100644 --- a/cparser/StructByValue.ml +++ b/cparser/StructReturn.ml @@ -13,17 +13,14 @@ (* *) (* *********************************************************************) -(* Eliminate by-value passing of structs and unions. *) - -(* Assumes: nothing. - Preserves: unblocked code *) +(* Eliminate structs and unions being returned by value as function results *) +(* This is a simpler special case of [StructByValue]. *) open C open Cutil open Transform -(* In function argument types, struct s -> const struct s * - In function result types, struct s -> void + add 1st parameter struct s * +(* In function result types, struct s -> void + add 1st parameter struct s * Try to preserve original typedef names when no change. *) @@ -49,11 +46,7 @@ let rec transf_type env t = if t1' = t1 then t else TArray(transf_type env t1, sz, attr) | _ -> t -and transf_funarg env (id, t) = - let t = transf_type env t in - if is_composite_type env t - then (id, TPtr(add_attributes_type [AConst] t, [])) - else (id, t) +and transf_funarg env (id, t) = (id, transf_type env t) (* Expressions: transform calls + rewrite the types *) @@ -92,26 +85,21 @@ let rec transf_expr env ctx e = if is_composite_type env e.etyp then transf_composite_call env ctx None fn args e.etyp else - {edesc = ECall(transf_expr env Val fn, List.map (transf_arg env) args); + {edesc = ECall(transf_expr env Val fn, + List.map (transf_expr env Val) args); etyp = newty} -(* Function arguments: pass by reference those having composite type *) - -and transf_arg env e = - let e' = transf_expr env Val e in - 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, ...) + ctx = Effects: lv = f(...) -> f(&lv, ...) [copy optimization] f(...) -> f(&newtemp, ...) - ctx = Val: lv = f(...) -> f(&newtemp, ...), lv = newtemp, newtemp + ctx = Val: lv = f(...) -> f(&newtemp, ...), lv = newtemp f(...) -> f(&newtemp, ...), newtemp *) and transf_composite_call env ctx opt_lhs fn args ty = let ty = transf_type env ty in let fn = transf_expr env Val fn in - let args = List.map (transf_arg env) args in + let args = List.map (transf_expr env Val) args in match ctx, opt_lhs with | Effects, None -> let tmp = new_temp ~name:"_res" ty in @@ -125,54 +113,14 @@ and transf_composite_call env ctx opt_lhs fn args ty = | Val, Some lhs -> let lhs = transf_expr env Val lhs in let tmp = new_temp ~name:"_res" ty in - ecomma (ecomma {edesc = ECall(fn, eaddrof tmp :: args); etyp = TVoid []} - (eassign lhs tmp)) - tmp - -(* The transformation above can create ill-formed lhs containing ",", as in - f().x = y ---> (f(&tmp), tmp).x = y - f(g(x)); ---> f(&(g(&tmp),tmp)) - We fix this by floating the "," above the lhs, up to the nearest enclosing - rhs: - f().x = y ---> (f(&tmp), tmp).x = y --> f(&tmp), tmp.x = y - f(g(x)); ---> f(&(g(&tmp),tmp)) --> f((g(&tmp), &tmp)) -*) - -let rec float_comma e = - match e.edesc with - | EConst c -> e - | ESizeof ty -> e - | EVar x -> e - (* lvalue-consuming unops *) - | EUnop((Oaddrof|Opreincr|Opredecr|Opostincr|Opostdecr|Odot _) as op, - {edesc = EBinop(Ocomma, e1, e2, _)}) -> - ecomma (float_comma e1) - (float_comma {edesc = EUnop(op, e2); etyp = e.etyp}) - (* lvalue-consuming binops *) - | EBinop((Oassign|Oadd_assign|Osub_assign|Omul_assign|Odiv_assign - |Omod_assign|Oand_assign|Oor_assign|Oxor_assign - |Oshl_assign|Oshr_assign) as op, - {edesc = EBinop(Ocomma, e1, e2, _)}, e3, tyres) -> - ecomma (float_comma e1) - (float_comma {edesc = EBinop(op, e2, e3, tyres); etyp = e.etyp}) - (* other expressions *) - | EUnop(op, e1) -> - {edesc = EUnop(op, float_comma e1); etyp = e.etyp} - | EBinop(op, e1, e2, tyres) -> - {edesc = EBinop(op, float_comma e1, float_comma e2, tyres); etyp = e.etyp} - | EConditional(e1, e2, e3) -> - {edesc = EConditional(float_comma e1, float_comma e2, float_comma e3); - etyp = e.etyp} - | ECast(ty, e1) -> - {edesc = ECast(ty, float_comma e1); etyp = e.etyp} - | ECall(e1, el) -> - {edesc = ECall(float_comma e1, List.map float_comma el); etyp = e.etyp} + ecomma {edesc = ECall(fn, eaddrof tmp :: args); etyp = TVoid []} + (eassign lhs tmp) (* Initializers *) let rec transf_init env = function | Init_single e -> - Init_single (float_comma(transf_expr env Val e)) + Init_single (transf_expr env Val e) | Init_array il -> Init_array (List.map (transf_init env) il) | Init_struct(id, fil) -> @@ -190,7 +138,7 @@ let transf_decl env (sto, id, ty, init) = let transf_funbody env body optres = -let transf_expr ctx e = float_comma(transf_expr env ctx e) in +let transf_expr ctx e = transf_expr env ctx e in (* Function returns: if return type is struct or union, return x -> _res = x; return @@ -239,33 +187,11 @@ let rec transf_stmt s = in transf_stmt body -let transf_params loc env params = - let rec transf_prm = function - | [] -> - ([], [], sskip) - | (id, ty) :: params -> - let ty = transf_type env ty in - if is_composite_type env ty then begin - let id' = Env.fresh_ident id.name in - let ty' = TPtr(add_attributes_type [AConst] ty, []) in - let (params', decls, init) = transf_prm params in - ((id', ty') :: params', - (Storage_default, id, ty, None) :: decls, - sseq loc - (sassign loc {edesc = EVar id; etyp = ty} - {edesc = EUnop(Oderef, {edesc = EVar id'; etyp = ty'}); - etyp = ty}) - init) - end else begin - let (params', decls, init) = transf_prm params in - ((id, ty) :: params', decls, init) - end - in transf_prm params - let transf_fundef env f = reset_temps(); let ret = transf_type env f.fd_ret in - let (params, newdecls, init) = transf_params f.fd_body.sloc env f.fd_params in + let params = + List.map (fun (id, ty) -> (id, transf_type env ty)) f.fd_params in let (ret1, params1, body1) = if is_composite_type env ret then begin let vres = Env.fresh_ident "_res" in @@ -277,10 +203,9 @@ let transf_fundef env f = transf_funbody env f.fd_body (Some eeres)) end else (ret, params, transf_funbody env f.fd_body None) in - let body2 = sseq body1.sloc init body1 in let temps = get_temps() in {f with fd_ret = ret1; fd_params = params1; - fd_locals = newdecls @ f.fd_locals @ temps; fd_body = body2} + fd_locals = f.fd_locals @ temps; fd_body = body1} (* Composites *) diff --git a/cparser/StructByValue.mli b/cparser/StructReturn.mli index 45899a46..45899a46 100644 --- a/cparser/StructByValue.mli +++ b/cparser/StructReturn.mli |