1 (* *********************************************************************)
3 (* The Compcert verified compiler *)
5 (* Xavier Leroy, INRIA Paris-Rocquencourt *)
7 (* Copyright Institut National de Recherche en Informatique et en *)
8 (* Automatique. All rights reserved. This file is distributed *)
9 (* under the terms of the GNU General Public License as published by *)
10 (* the Free Software Foundation, either version 2 of the License, or *)
11 (* (at your option) any later version. This file is also distributed *)
12 (* under the terms of the INRIA Non-Commercial License Agreement. *)
14 (* *********************************************************************)
16 (* Expand assignments between structs and between unions *)
18 (* Assumes: simplified code.
19 Preserves: simplified code, unblocked code *)
28 let need_memcpy = ref (None: ident option)
31 TFun(TPtr(TVoid [], []),
32 Some [(Env.fresh_ident "", TPtr(TVoid [], []));
33 (Env.fresh_ident "", TPtr(TVoid [AConst], []));
34 (Env.fresh_ident "", TInt(size_t_ikind, []))],
38 match !need_memcpy with
40 let id = Env.fresh_ident "memcpy" in
41 need_memcpy := Some id;
46 let transf_assign env loc lhs rhs =
48 let num_assign = ref 0 in
52 if !num_assign > !maxsize
54 else sassign loc l r in
57 match unroll env l.etyp with
58 | TStruct(id, attr) ->
59 let ci = Env.find_struct env id in
60 if ci.ci_sizeof = None then
61 error "%a: Error: incomplete struct '%s'" formatloc loc id.name;
62 transf_struct l r ci.ci_members
65 | TArray(ty_elt, Some sz, attr) ->
66 transf_array l r ty_elt 0L sz
67 | TArray(ty_elt, None, attr) ->
68 error "%a: Error: array of unknown size" formatloc loc;
69 sskip (* will be ignored later *)
73 and transf_struct l r = function
76 sseq loc (transf {edesc = EUnop(Odot f.fld_name, l); etyp = f.fld_typ}
77 {edesc = EUnop(Odot f.fld_name, r); etyp = f.fld_typ})
78 (transf_struct l r fl)
80 and transf_array l r ty idx sz =
81 if idx >= sz then sskip else begin
82 let e = intconst idx size_t_ikind in
83 sseq loc (transf {edesc = EBinop(Oindex, l, e, ty); etyp = ty}
84 {edesc = EBinop(Oindex, r, e, ty); etyp = ty})
85 (transf_array l r ty (Int64.add idx 1L) sz)
92 let memcpy = {edesc = EVar(memcpy_ident()); etyp = memcpy_type} in
93 let e_lhs = {edesc = EUnop(Oaddrof, lhs); etyp = TPtr(lhs.etyp, [])} in
94 let e_rhs = {edesc = EUnop(Oaddrof, rhs); etyp = TPtr(rhs.etyp, [])} in
95 let e_size = {edesc = ESizeof(lhs.etyp); etyp = TInt(size_t_ikind, [])} in
96 {sdesc = Sdo {edesc = ECall(memcpy, [e_lhs; e_rhs; e_size]);
100 let rec transf_stmt env s =
103 | Sdo {edesc = EBinop(Oassign, lhs, rhs, _)}
104 when is_composite_type env lhs.etyp ->
105 transf_assign env s.sloc lhs rhs
108 {s with sdesc = Sseq(transf_stmt env s1, transf_stmt env s2)}
110 {s with sdesc = Sif(e, transf_stmt env s1, transf_stmt env s2)}
112 {s with sdesc = Swhile(e, transf_stmt env s1)}
114 {s with sdesc = Sdowhile(transf_stmt env s1, e)}
115 | Sfor(s1, e, s2, s3) ->
116 {s with sdesc = Sfor(transf_stmt env s1, e,
117 transf_stmt env s2, transf_stmt env s3)}
121 {s with sdesc = Sswitch(e, transf_stmt env s1)}
122 | Slabeled(lbl, s1) ->
123 {s with sdesc = Slabeled(lbl, transf_stmt env s1)}
127 {s with sdesc = Sblock(List.map (transf_stmt env) sl)}
130 let transf_fundef env fd =
131 {fd with fd_body = transf_stmt env fd.fd_body}
135 let p' = Transform.program ~fundef:transf_fundef p in
136 match !need_memcpy with
139 {gdesc = Gdecl(Storage_extern, id, memcpy_type, None); gloc = no_loc}
144 let has_memcpy = ref false in
147 (function {gdesc = Gdecl(_, ({name = "memcpy"} as id), _, _)} ->
148 need_memcpy := Some id; has_memcpy := true
151 let p' = Transform.program ~fundef:transf_fundef p in
152 match !need_memcpy with
153 | Some id when not !has_memcpy ->
154 {gdesc = Gdecl(Storage_extern, id, memcpy_type, None); gloc = no_loc}