From 25b9b003178002360d666919f2e49e7f5f4a36e2 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Feb 2012 19:14:14 +0000 Subject: Merge of the "volatile" branch: - native treatment of volatile accesses in CompCert C's semantics - translation of volatile accesses to built-ins in SimplExpr - native treatment of struct assignment and passing struct parameter by value - only passing struct result by value remains emulated - in cparser, remove emulations that are no longer used - added C99's type _Bool and used it to express || and && more efficiently. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1814 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cparser/.depend | 34 +-- cparser/AddCasts.ml | 243 -------------------- cparser/AddCasts.mli | 16 -- cparser/Elab.ml | 4 +- cparser/Makefile | 4 +- cparser/Parse.ml | 14 +- cparser/SimplExpr.ml | 568 ---------------------------------------------- cparser/SimplExpr.mli | 20 -- cparser/SimplVolatile.ml | 81 ------- cparser/StructAssign.ml | 165 -------------- cparser/StructAssign.mli | 18 -- cparser/StructByValue.ml | 298 ------------------------ cparser/StructByValue.mli | 16 -- cparser/StructReturn.ml | 223 ++++++++++++++++++ cparser/StructReturn.mli | 16 ++ 15 files changed, 254 insertions(+), 1466 deletions(-) delete mode 100644 cparser/AddCasts.ml delete mode 100644 cparser/AddCasts.mli delete mode 100644 cparser/SimplExpr.ml delete mode 100644 cparser/SimplExpr.mli delete mode 100644 cparser/SimplVolatile.ml delete mode 100644 cparser/StructAssign.ml delete mode 100644 cparser/StructAssign.mli delete mode 100644 cparser/StructByValue.ml delete mode 100644 cparser/StructByValue.mli create mode 100644 cparser/StructReturn.ml create mode 100644 cparser/StructReturn.mli (limited to 'cparser') diff --git a/cparser/.depend b/cparser/.depend index 51f3b5e..4a7f538 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 eb3fa08..0000000 --- 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 318ecc6..0000000 --- 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 870385d..2da1936 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 527cdd3..da2c28b 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 dcd01e9..2c467a7 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 4184d95..0000000 --- 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 cdeb30c..0000000 --- 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 ef7a3a0..0000000 --- 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 d9ad8f5..0000000 --- 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 5549282..0000000 --- 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/StructByValue.ml deleted file mode 100644 index 1b74ec5..0000000 --- a/cparser/StructByValue.ml +++ /dev/null @@ -1,298 +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. *) -(* *) -(* *********************************************************************) - -(* Eliminate by-value passing of structs and unions. *) - -(* Assumes: nothing. - Preserves: unblocked code *) - -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 * - Try to preserve original typedef names when no change. -*) - -let rec transf_type env t = - match unroll env t with - | TFun(tres, None, vararg, attr) -> - let tres' = transf_type env tres in - TFun((if is_composite_type env tres then TVoid [] else tres'), - None, vararg, attr) - | TFun(tres, Some args, vararg, attr) -> - let args' = List.map (transf_funarg env) args in - let tres' = transf_type env tres in - if is_composite_type env tres then begin - let res = Env.fresh_ident "_res" in - TFun(TVoid [], Some((res, TPtr(tres', [])) :: args'), vararg, attr) - end else - TFun(tres', Some args', vararg, attr) - | TPtr(t1, attr) -> - let t1' = transf_type env t1 in - if t1' = t1 then t else TPtr(transf_type env t1, attr) - | TArray(t1, sz, attr) -> - let t1' = transf_type env t1 in - 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) - -(* Expressions: transform calls + rewrite the types *) - -let rec transf_expr env ctx e = - let newty = transf_type env e.etyp in - match e.edesc with - | EConst c -> - {edesc = EConst c; etyp = newty} - | ESizeof ty -> - {edesc = ESizeof (transf_type env ty); etyp = newty} - | EVar x -> - {edesc = EVar x; etyp = newty} - | EUnop(op, e1) -> - {edesc = EUnop(op, transf_expr env Val e1); etyp = newty} - | EBinop(Oassign, lhs, {edesc = ECall(fn, args)}, ty) - when is_composite_type env ty -> - transf_composite_call env ctx (Some lhs) fn args ty - | EBinop(Ocomma, e1, e2, ty) -> - {edesc = EBinop(Ocomma, transf_expr env Effects e1, - transf_expr env ctx e2, - transf_type env ty); - etyp = newty} - | EBinop(op, e1, e2, ty) -> - {edesc = EBinop(op, transf_expr env Val e1, - transf_expr env Val e2, - transf_type env ty); - etyp = newty} - | EConditional(e1, e2, e3) -> - {edesc = EConditional(transf_expr env Val e1, - transf_expr env ctx e2, - transf_expr env ctx e3); - etyp = newty} - | ECast(ty, e1) -> - {edesc = ECast(transf_type env ty, transf_expr env Val e1); etyp = newty} - | ECall(fn, args) -> - 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); - 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, ...) - f(...) -> f(&newtemp, ...) - ctx = Val: lv = f(...) -> f(&newtemp, ...), lv = newtemp, 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 - match ctx, opt_lhs with - | Effects, None -> - let tmp = new_temp ~name:"_res" ty in - {edesc = ECall(fn, eaddrof tmp :: args); etyp = TVoid []} - | Effects, Some lhs -> - let lhs = transf_expr env Val lhs in - {edesc = ECall(fn, eaddrof lhs :: args); etyp = TVoid []} - | Val, None -> - let tmp = new_temp ~name:"_res" ty in - 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, 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} - -(* Initializers *) - -let rec transf_init env = function - | Init_single e -> - Init_single (float_comma(transf_expr env Val e)) - | Init_array il -> - Init_array (List.map (transf_init env) il) - | Init_struct(id, fil) -> - Init_struct (id, List.map (fun (fld, i) -> (fld, transf_init env i)) fil) - | Init_union(id, fld, i) -> - Init_union(id, fld, transf_init env i) - -(* Declarations *) - -let transf_decl env (sto, id, ty, init) = - (sto, id, transf_type env ty, - match init with None -> None | Some i -> Some (transf_init env i)) - -(* Transformation of statements and function bodies *) - -let transf_funbody env body optres = - -let transf_expr ctx e = float_comma(transf_expr env ctx e) in - -(* Function returns: if return type is struct or union, - return x -> _res = x; return -*) - -let rec transf_stmt s = - match s.sdesc with - | Sskip -> s - | Sdo e -> - {s with sdesc = Sdo(transf_expr Effects e)} - | Sseq(s1, s2) -> - {s with sdesc = Sseq(transf_stmt s1, transf_stmt s2)} - | Sif(e, s1, s2) -> - {s with sdesc = Sif(transf_expr Val e, - transf_stmt s1, transf_stmt s2)} - | Swhile(e, s1) -> - {s with sdesc = Swhile(transf_expr Val e, transf_stmt s1)} - | Sdowhile(s1, e) -> - {s with sdesc = Sdowhile(transf_stmt s1, transf_expr Val e)} - | Sfor(s1, e, s2, s3) -> - {s with sdesc = Sfor(transf_stmt s1, transf_expr Val e, - transf_stmt s2, transf_stmt s3)} - | Sbreak -> s - | Scontinue -> s - | Sswitch(e, s1) -> - {s with sdesc = Sswitch(transf_expr Val e, transf_stmt s1)} - | Slabeled(lbl, s1) -> - {s with sdesc = Slabeled(lbl, transf_stmt s1)} - | Sgoto lbl -> s - | Sreturn None -> s - | Sreturn(Some e) -> - let e = transf_expr Val e in - begin match optres with - | None -> - {s with sdesc = Sreturn(Some e)} - | Some dst -> - sseq s.sloc - (sassign s.sloc dst e) - {sdesc = Sreturn None; sloc = s.sloc} - end - | Sblock sl -> - {s with sdesc = Sblock(List.map transf_stmt sl)} - | Sdecl d -> - {s with sdesc = Sdecl(transf_decl env d)} - -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 (ret1, params1, body1) = - if is_composite_type env ret then begin - let vres = Env.fresh_ident "_res" in - let tres = TPtr(ret, []) in - let eres = {edesc = EVar vres; etyp = tres} in - let eeres = {edesc = EUnop(Oderef, eres); etyp = ret} in - (TVoid [], - (vres, tres) :: params, - 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} - -(* Composites *) - -let transf_composite env su id attr fl = - (attr, List.map (fun f -> {f with fld_typ = transf_type env f.fld_typ}) fl) - -(* Entry point *) - -let program p = - Transform.program - ~decl:transf_decl - ~fundef:transf_fundef - ~composite:transf_composite - ~typedef:(fun env id ty -> transf_type env ty) - p diff --git a/cparser/StructByValue.mli b/cparser/StructByValue.mli deleted file mode 100644 index 45899a4..0000000 --- a/cparser/StructByValue.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: C.program -> C.program diff --git a/cparser/StructReturn.ml b/cparser/StructReturn.ml new file mode 100644 index 0000000..2a4bbc1 --- /dev/null +++ b/cparser/StructReturn.ml @@ -0,0 +1,223 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(* 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 result types, struct s -> void + add 1st parameter struct s * + Try to preserve original typedef names when no change. +*) + +let rec transf_type env t = + match unroll env t with + | TFun(tres, None, vararg, attr) -> + let tres' = transf_type env tres in + TFun((if is_composite_type env tres then TVoid [] else tres'), + None, vararg, attr) + | TFun(tres, Some args, vararg, attr) -> + let args' = List.map (transf_funarg env) args in + let tres' = transf_type env tres in + if is_composite_type env tres then begin + let res = Env.fresh_ident "_res" in + TFun(TVoid [], Some((res, TPtr(tres', [])) :: args'), vararg, attr) + end else + TFun(tres', Some args', vararg, attr) + | TPtr(t1, attr) -> + let t1' = transf_type env t1 in + if t1' = t1 then t else TPtr(transf_type env t1, attr) + | TArray(t1, sz, attr) -> + let t1' = transf_type env t1 in + if t1' = t1 then t else TArray(transf_type env t1, sz, attr) + | _ -> t + +and transf_funarg env (id, t) = (id, transf_type env t) + +(* Expressions: transform calls + rewrite the types *) + +let rec transf_expr env ctx e = + let newty = transf_type env e.etyp in + match e.edesc with + | EConst c -> + {edesc = EConst c; etyp = newty} + | ESizeof ty -> + {edesc = ESizeof (transf_type env ty); etyp = newty} + | EVar x -> + {edesc = EVar x; etyp = newty} + | EUnop(op, e1) -> + {edesc = EUnop(op, transf_expr env Val e1); etyp = newty} + | EBinop(Oassign, lhs, {edesc = ECall(fn, args)}, ty) + when is_composite_type env ty -> + transf_composite_call env ctx (Some lhs) fn args ty + | EBinop(Ocomma, e1, e2, ty) -> + {edesc = EBinop(Ocomma, transf_expr env Effects e1, + transf_expr env ctx e2, + transf_type env ty); + etyp = newty} + | EBinop(op, e1, e2, ty) -> + {edesc = EBinop(op, transf_expr env Val e1, + transf_expr env Val e2, + transf_type env ty); + etyp = newty} + | EConditional(e1, e2, e3) -> + {edesc = EConditional(transf_expr env Val e1, + transf_expr env ctx e2, + transf_expr env ctx e3); + etyp = newty} + | ECast(ty, e1) -> + {edesc = ECast(transf_type env ty, transf_expr env Val e1); etyp = newty} + | ECall(fn, args) -> + 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_expr env Val) args); + etyp = newty} + +(* Function calls returning a composite: add first argument. + ctx = Effects: lv = f(...) -> f(&lv, ...) [copy optimization] + f(...) -> f(&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_expr env Val) args in + match ctx, opt_lhs with + | Effects, None -> + let tmp = new_temp ~name:"_res" ty in + {edesc = ECall(fn, eaddrof tmp :: args); etyp = TVoid []} + | Effects, Some lhs -> + let lhs = transf_expr env Val lhs in + {edesc = ECall(fn, eaddrof lhs :: args); etyp = TVoid []} + | Val, None -> + let tmp = new_temp ~name:"_res" ty in + 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 {edesc = ECall(fn, eaddrof tmp :: args); etyp = TVoid []} + (eassign lhs tmp) + +(* Initializers *) + +let rec transf_init env = function + | Init_single e -> + Init_single (transf_expr env Val e) + | Init_array il -> + Init_array (List.map (transf_init env) il) + | Init_struct(id, fil) -> + Init_struct (id, List.map (fun (fld, i) -> (fld, transf_init env i)) fil) + | Init_union(id, fld, i) -> + Init_union(id, fld, transf_init env i) + +(* Declarations *) + +let transf_decl env (sto, id, ty, init) = + (sto, id, transf_type env ty, + match init with None -> None | Some i -> Some (transf_init env i)) + +(* Transformation of statements and function bodies *) + +let transf_funbody env body optres = + +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 +*) + +let rec transf_stmt s = + match s.sdesc with + | Sskip -> s + | Sdo e -> + {s with sdesc = Sdo(transf_expr Effects e)} + | Sseq(s1, s2) -> + {s with sdesc = Sseq(transf_stmt s1, transf_stmt s2)} + | Sif(e, s1, s2) -> + {s with sdesc = Sif(transf_expr Val e, + transf_stmt s1, transf_stmt s2)} + | Swhile(e, s1) -> + {s with sdesc = Swhile(transf_expr Val e, transf_stmt s1)} + | Sdowhile(s1, e) -> + {s with sdesc = Sdowhile(transf_stmt s1, transf_expr Val e)} + | Sfor(s1, e, s2, s3) -> + {s with sdesc = Sfor(transf_stmt s1, transf_expr Val e, + transf_stmt s2, transf_stmt s3)} + | Sbreak -> s + | Scontinue -> s + | Sswitch(e, s1) -> + {s with sdesc = Sswitch(transf_expr Val e, transf_stmt s1)} + | Slabeled(lbl, s1) -> + {s with sdesc = Slabeled(lbl, transf_stmt s1)} + | Sgoto lbl -> s + | Sreturn None -> s + | Sreturn(Some e) -> + let e = transf_expr Val e in + begin match optres with + | None -> + {s with sdesc = Sreturn(Some e)} + | Some dst -> + sseq s.sloc + (sassign s.sloc dst e) + {sdesc = Sreturn None; sloc = s.sloc} + end + | Sblock sl -> + {s with sdesc = Sblock(List.map transf_stmt sl)} + | Sdecl d -> + {s with sdesc = Sdecl(transf_decl env d)} + +in + transf_stmt body + +let transf_fundef env f = + reset_temps(); + let ret = transf_type env f.fd_ret 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 + let tres = TPtr(ret, []) in + let eres = {edesc = EVar vres; etyp = tres} in + let eeres = {edesc = EUnop(Oderef, eres); etyp = ret} in + (TVoid [], + (vres, tres) :: params, + transf_funbody env f.fd_body (Some eeres)) + end else + (ret, params, transf_funbody env f.fd_body None) in + let temps = get_temps() in + {f with fd_ret = ret1; fd_params = params1; + fd_locals = f.fd_locals @ temps; fd_body = body1} + +(* Composites *) + +let transf_composite env su id attr fl = + (attr, List.map (fun f -> {f with fld_typ = transf_type env f.fld_typ}) fl) + +(* Entry point *) + +let program p = + Transform.program + ~decl:transf_decl + ~fundef:transf_fundef + ~composite:transf_composite + ~typedef:(fun env id ty -> transf_type env ty) + p diff --git a/cparser/StructReturn.mli b/cparser/StructReturn.mli new file mode 100644 index 0000000..45899a4 --- /dev/null +++ b/cparser/StructReturn.mli @@ -0,0 +1,16 @@ +(* *********************************************************************) +(* *) +(* 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: C.program -> C.program -- cgit v1.2.3