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