source: Deliverables/D2.3/8051-memoryspaces-branch/cparser/StructAssign.ml @ 460

Last change on this file since 460 was 460, checked in by campbell, 9 years ago

Port memory spaces changes to latest prototype compiler.

File size: 5.6 KB
Line 
1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*                                                                     *)
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.     *)
13(*                                                                     *)
14(* *********************************************************************)
15
16(* Expand assignments between structs and between unions *)
17
18(* Assumes: simplified code.
19   Preserves: simplified code, unblocked code *)
20
21open C
22open Cutil
23open Env
24open Errors
25
26let maxsize = ref 8
27
28let need_memcpy = ref (None: ident option)
29
30let memcpy_type =
31  TFun(TPtr(Any,TVoid [], []),
32       Some [(Env.fresh_ident "", TPtr(Any,TVoid [], []));
33             (Env.fresh_ident "", TPtr(Any,TVoid [AConst], []));
34             (Env.fresh_ident "", TInt(size_t_ikind, []))],
35       false, [])
36
37let memcpy_ident () =
38  match !need_memcpy with
39  | None ->
40      let id = Env.fresh_ident "memcpy" in
41      need_memcpy := Some id;
42      id
43  | Some id ->
44      id
45
46let space_of_ty = function
47| TArray(space, _, _, _)
48| TPtr(space, _, _) -> space
49| _ -> Any
50
51let transf_assign env loc lhs rhs =
52
53  let num_assign = ref 0 in
54
55  let assign l r =
56    incr num_assign;
57    if !num_assign > !maxsize
58    then raise Exit
59    else sassign loc l r in
60
61  let rec transf l r =
62    match unroll env l.etyp with
63    | TStruct(id, attr) ->
64        let ci = Env.find_struct env id in
65        if ci.ci_sizeof = None then
66          error "%a: Error: incomplete struct '%s'" formatloc loc id.name;
67        transf_struct l r ci.ci_members
68    | TUnion(id, attr) ->
69        raise Exit
70    | TArray(space, ty_elt, Some sz, attr) ->
71        transf_array space l (space_of_ty (unroll env r.etyp)) r ty_elt 0L sz
72    | TArray(space, ty_elt, None, attr) ->
73        error "%a: Error: array of unknown size" formatloc loc;
74        sskip                           (* will be ignored later *)
75    | _ ->
76        assign l r
77
78  and transf_struct l r = function
79    | [] -> sskip
80    | f :: fl ->
81        sseq loc (transf {edesc = EUnop(Odot f.fld_name, l); etyp = f.fld_typ; espace = l.espace}
82                         {edesc = EUnop(Odot f.fld_name, r); etyp = f.fld_typ; espace = r.espace})
83                 (transf_struct l r fl)
84
85  and transf_array lsp l rsp r ty idx sz =
86    if idx >= sz then sskip else begin
87      let e = intconst idx size_t_ikind in
88      sseq loc (transf {edesc = EBinop(Oindex, l, e, ty); etyp = ty; espace = lsp}
89                       {edesc = EBinop(Oindex, r, e, ty); etyp = ty; espace = rsp})
90               (transf_array lsp l rsp r ty (Int64.add idx 1L) sz)
91    end
92  in
93
94  try
95    transf lhs rhs
96  with Exit ->
97    let memcpy = {edesc = EVar(memcpy_ident()); etyp = memcpy_type; espace = Any} in
98    (* XXX: casts required? *)
99    let e_lhs = {edesc = EUnop(Oaddrof, lhs); etyp = TPtr(Any, lhs.etyp, []); espace = Any} in
100    let e_rhs = {edesc = EUnop(Oaddrof, rhs); etyp = TPtr(Any, rhs.etyp, []); espace = Any} in
101    let e_size = {edesc = ESizeof(lhs.etyp); etyp = TInt(size_t_ikind, []); espace = Any} in
102    {sdesc = Sdo {edesc = ECall(memcpy, [e_lhs; e_rhs; e_size]);
103                  etyp = TVoid[]; espace = Any};
104     sloc = loc}
105
106let rec transf_stmt env s =
107  match s.sdesc with
108  | Sskip -> s
109  | Sdo {edesc = EBinop(Oassign, lhs, rhs, _)}
110    when is_composite_type env lhs.etyp ->
111      transf_assign env s.sloc lhs rhs
112  | Sdo _ -> s
113  | Sseq(s1, s2) ->
114      {s with sdesc = Sseq(transf_stmt env s1, transf_stmt env s2)}
115  | Sif(e, s1, s2) ->
116      {s with sdesc = Sif(e, transf_stmt env s1, transf_stmt env s2)}
117  | Swhile(e, s1) ->
118      {s with sdesc = Swhile(e, transf_stmt env s1)}
119  | Sdowhile(s1, e) ->
120      {s with sdesc = Sdowhile(transf_stmt env s1, e)}
121  | Sfor(s1, e, s2, s3) ->
122      {s with sdesc = Sfor(transf_stmt env s1, e,
123                           transf_stmt env s2, transf_stmt env s3)}
124  | Sbreak -> s
125  | Scontinue -> s
126  | Sswitch(e, s1) ->
127      {s with sdesc = Sswitch(e, transf_stmt env s1)}
128  | Slabeled(lbl, s1) ->
129      {s with sdesc = Slabeled(lbl, transf_stmt env s1)}
130  | Sgoto lbl -> s
131  | Sreturn _ -> s
132  | Sblock sl ->
133      {s with sdesc = Sblock(List.map (transf_stmt env) sl)}
134  | Sdecl d -> s
135
136let transf_fundef env fd =
137  {fd with fd_body = transf_stmt env fd.fd_body}
138
139let program p =
140  need_memcpy := None;
141  let p' = Transform.program ~fundef:transf_fundef p in
142  match !need_memcpy with
143  | None -> p'
144  | Some id ->
145      {gdesc = Gdecl(Code, (Storage_extern, id, memcpy_type, None)); gloc = no_loc}
146      :: p'
147
148(* Horrible hack *)
149(***
150  let has_memcpy = ref false in
151  need_memcpy := None;
152  List.iter
153    (function {gdesc = Gdecl(_, ({name = "memcpy"} as id), _, _)} ->
154                   need_memcpy := Some id; has_memcpy := true
155            | _ -> ())
156    p;
157  let p' = Transform.program ~fundef:transf_fundef p in
158  match !need_memcpy with
159  | Some id when not !has_memcpy ->
160      {gdesc = Gdecl(Storage_extern, id, memcpy_type, None); gloc = no_loc}
161      :: p'
162  | _ -> p'
163***)
Note: See TracBrowser for help on using the repository browser.