cparser/StructAssign.ml

   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
  21 open C
  22 open Cutil
  23 open Env
  24 open Errors
  25
  26 let maxsize = ref 8
  27
  28 let need_memcpy = ref (None: ident option)
  29
  30 let memcpy_type =
  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, []))],
  35        false, [])
  36
  37 let 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
  46 let transf_assign env loc lhs rhs =
  47
  48   let num_assign = ref 0 in
  49
  50   let assign l r =
  51     incr num_assign;
  52     if !num_assign > !maxsize
  53     then raise Exit
  54     else sassign loc l r in
  55
  56   let rec transf l r =
  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
  63     | TUnion(id, attr) ->
  64         raise Exit
  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 *)
  70     | _ ->
  71         assign l r
  72
  73   and transf_struct l r = function
  74     | [] -> sskip
  75     | f :: fl ->
  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)
  79
  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)
  86     end
  87   in
  88
  89   try
  90     transf lhs rhs
  91   with Exit ->
  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]);
  97                   etyp = TVoid[]};
  98      sloc = loc}
  99
 100 let rec transf_stmt env s =
 101   match s.sdesc with
 102   | Sskip -> s
 103   | Sdo {edesc = EBinop(Oassign, lhs, rhs, _)}
 104     when is_composite_type env lhs.etyp ->
 105       transf_assign env s.sloc lhs rhs
 106   | Sdo _ -> s
 107   | Sseq(s1, s2) ->
 108       {s with sdesc = Sseq(transf_stmt env s1, transf_stmt env s2)}
 109   | Sif(e, s1, s2) ->
 110       {s with sdesc = Sif(e, transf_stmt env s1, transf_stmt env s2)}
 111   | Swhile(e, s1) ->
 112       {s with sdesc = Swhile(e, transf_stmt env s1)}
 113   | Sdowhile(s1, e) ->
 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)}
 118   | Sbreak -> s
 119   | Scontinue -> s
 120   | Sswitch(e, s1) ->
 121       {s with sdesc = Sswitch(e, transf_stmt env s1)}
 122   | Slabeled(lbl, s1) ->
 123       {s with sdesc = Slabeled(lbl, transf_stmt env s1)}
 124   | Sgoto lbl -> s
 125   | Sreturn _ -> s
 126   | Sblock sl ->
 127       {s with sdesc = Sblock(List.map (transf_stmt env) sl)}
 128   | Sdecl d -> s
 129
 130 let transf_fundef env fd =
 131   {fd with fd_body = transf_stmt env fd.fd_body}
 132
 133 let program p =
 134   need_memcpy := None;
 135   let p' = Transform.program ~fundef:transf_fundef p in
 136   match !need_memcpy with
 137   | None -> p'
 138   | Some id ->
 139       {gdesc = Gdecl(Storage_extern, id, memcpy_type, None); gloc = no_loc}
 140       :: p'
 141
 142 (* Horrible hack *)
 143 (***
 144   let has_memcpy = ref false in
 145   need_memcpy := None;
 146   List.iter
 147     (function {gdesc = Gdecl(_, ({name = "memcpy"} as id), _, _)} ->
 148                    need_memcpy := Some id; has_memcpy := true
 149             | _ -> ())
 150     p;
 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}
 155       :: p'
 156   | _ -> p'
 157 ***)