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/AddCasts.ml | 243 ---------------------------------------------------- 1 file changed, 243 deletions(-) delete mode 100644 cparser/AddCasts.ml (limited to 'cparser/AddCasts.ml') 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 -- cgit