Imported Upstream version 0.1

[pkg-cerco/acc-trusted.git] / cparser / StructAssign.ml

diff --git a/cparser/StructAssign.ml b/cparser/StructAssign.ml
new file mode 100644 (file)
index 0000000..f5cecfc
--- /dev/null
+++ b/cparser/StructAssign.ml
@@ -0,0 +1,157 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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: simplified code.
+   Preserves: simplified code, unblocked code *)
+
+open C
+open Cutil
+open Env
+open Errors
+
+let maxsize = ref 8
+
+let need_memcpy = 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 memcpy_ident () =
+  match !need_memcpy with
+  | None ->
+      let id = Env.fresh_ident "memcpy" in
+      need_memcpy := Some id;
+      id
+  | Some id ->
+      id 
+
+let transf_assign env loc lhs rhs =
+
+  let num_assign = ref 0 in
+
+  let assign l r =
+    incr num_assign;
+    if !num_assign > !maxsize 
+    then raise Exit
+    else sassign loc l r in
+
+  let rec transf l r =
+    match unroll env l.etyp with
+    | TStruct(id, attr) ->
+        let ci = Env.find_struct env id in
+        if ci.ci_sizeof = None then
+          error "%a: Error: incomplete struct '%s'" formatloc loc id.name;
+        transf_struct l r ci.ci_members
+    | TUnion(id, attr) ->
+        raise Exit
+    | TArray(ty_elt, Some sz, attr) ->
+        transf_array l r ty_elt 0L sz
+    | TArray(ty_elt, None, attr) ->
+        error "%a: Error: array of unknown size" formatloc loc;
+        sskip                           (* will be ignored later *)
+    | _ ->
+        assign l r
+
+  and transf_struct l r = function
+    | [] -> sskip
+    | f :: fl ->
+        sseq loc (transf {edesc = EUnop(Odot f.fld_name, l); etyp = f.fld_typ}
+                         {edesc = EUnop(Odot f.fld_name, r); etyp = f.fld_typ})
+                 (transf_struct l r fl)
+
+  and transf_array l r ty idx sz =
+    if idx >= sz then sskip else begin
+      let e = intconst idx size_t_ikind in
+      sseq loc (transf {edesc = EBinop(Oindex, l, e, ty); etyp = ty}
+                       {edesc = EBinop(Oindex, r, e, ty); etyp = ty})
+               (transf_array l r ty (Int64.add idx 1L) sz)
+    end
+  in
+
+  try
+    transf lhs rhs
+  with Exit ->
+    let memcpy = {edesc = EVar(memcpy_ident()); etyp = memcpy_type} in
+    let e_lhs = {edesc = EUnop(Oaddrof, lhs); etyp = TPtr(lhs.etyp, [])} in
+    let e_rhs = {edesc = EUnop(Oaddrof, rhs); etyp = TPtr(rhs.etyp, [])} in
+    let e_size = {edesc = ESizeof(lhs.etyp); etyp = TInt(size_t_ikind, [])} in
+    {sdesc = Sdo {edesc = ECall(memcpy, [e_lhs; e_rhs; e_size]);
+                  etyp = TVoid[]};
+     sloc = loc}
+
+let rec transf_stmt env s =
+  match s.sdesc with
+  | Sskip -> s
+  | Sdo {edesc = EBinop(Oassign, lhs, rhs, _)}
+    when is_composite_type env lhs.etyp ->
+      transf_assign env s.sloc lhs rhs
+  | Sdo _ -> s
+  | Sseq(s1, s2) ->
+      {s with sdesc = Sseq(transf_stmt env s1, transf_stmt env s2)}
+  | Sif(e, s1, s2) ->
+      {s with sdesc = Sif(e, transf_stmt env s1, transf_stmt env s2)}
+  | Swhile(e, s1) ->
+      {s with sdesc = Swhile(e, transf_stmt env s1)}
+  | Sdowhile(s1, e) ->
+      {s with sdesc = Sdowhile(transf_stmt env s1, e)}
+  | Sfor(s1, e, s2, s3) ->
+      {s with sdesc = Sfor(transf_stmt env s1, e,
+                           transf_stmt env s2, transf_stmt env s3)}
+  | Sbreak -> s
+  | Scontinue -> s
+  | Sswitch(e, s1) ->
+      {s with sdesc = Sswitch(e, transf_stmt env s1)}
+  | Slabeled(lbl, s1) ->
+      {s with sdesc = Slabeled(lbl, transf_stmt env s1)}
+  | Sgoto lbl -> s
+  | Sreturn _ -> s
+  | Sblock sl ->
+      {s with sdesc = Sblock(List.map (transf_stmt env) sl)}
+  | Sdecl d -> s
+
+let transf_fundef env fd =
+  {fd with fd_body = transf_stmt env fd.fd_body}
+
+let program p =
+  need_memcpy := None;
+  let p' = Transform.program ~fundef:transf_fundef p in
+  match !need_memcpy with
+  | None -> p'
+  | Some id ->
+      {gdesc = Gdecl(Storage_extern, id, memcpy_type, None); gloc = no_loc}
+      :: p'
+
+(* Horrible hack *)
+(***
+  let has_memcpy = ref false in
+  need_memcpy := None;
+  List.iter
+    (function {gdesc = Gdecl(_, ({name = "memcpy"} as id), _, _)} ->
+                   need_memcpy := Some id; has_memcpy := true
+            | _ -> ())
+    p;
+  let p' = Transform.program ~fundef:transf_fundef p in
+  match !need_memcpy with
+  | Some id when not !has_memcpy ->
+      {gdesc = Gdecl(Storage_extern, id, memcpy_type, None); gloc = no_loc}
+      :: p'
+  | _ -> p'
+***)