cparser/Unblock.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 (* Simplification of blocks and initializers within functions *)
  17
  18 (* Assumes: nothing
  19    Produces: unblocked code *)
  20
  21 open C
  22 open Cutil
  23 open Errors
  24
  25 (* Convert an initializer to a list of assignments.
  26    Prepend those assignments to the given statement. *)
  27
  28 let sdoseq loc e s =
  29   sseq loc {sdesc = Sdo e; sloc = loc} s
  30
  31 let rec local_initializer loc env path init k =
  32   match init with
  33   | Init_single e ->
  34       sdoseq loc
  35         { edesc = EBinop(Oassign, path, e, path.etyp); etyp = path.etyp }
  36         k
  37   | Init_array il ->
  38       let ty_elt =
  39         match unroll env path.etyp with
  40         | TArray(ty_elt, _, _) -> ty_elt
  41         | _ -> fatal_error "%aWrong type for array initializer"
  42                            formatloc loc in
  43       let rec array_init pos = function
  44         | [] -> k
  45         | i :: il ->
  46             local_initializer loc env
  47               { edesc = EBinop(Oindex, path, intconst pos IInt, TPtr(ty_elt, []));
  48                 etyp = ty_elt }
  49               i
  50               (array_init (Int64.succ pos) il) in
  51       array_init 0L il
  52   | Init_struct(id, fil) ->
  53       let field_init (fld, i) k =
  54         local_initializer loc env
  55           { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ }
  56           i k in
  57       List.fold_right field_init fil k
  58   | Init_union(id, fld, i) ->
  59       local_initializer loc env
  60         { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ }
  61         i k
  62
  63 (* Record new variables to be locally defined *)
  64
  65 let local_variables = ref ([]: decl list)
  66
  67 (* Note: "const int x = y - 1;" is legal, but we turn it into
  68    "const int x; x = y - 1;", which is not.  Therefore, remove
  69    top-level 'const' attribute.  Also remove it on element type of
  70    array type. *)
  71
  72 let remove_const env ty = remove_attributes_type env [AConst] ty
  73
  74 (* Process a variable declaration.
  75    The variable is entered in [local_variables].
  76    The initializer, if any, is converted into assignments and
  77    prepended to [k]. *)
  78
  79 let process_decl loc env (sto, id, ty, optinit) k =
  80   let ty' = remove_const env ty in
  81   local_variables := (sto, id, ty', None) :: !local_variables;
  82   match optinit with
  83   | None -> k
  84   | Some init ->
  85       local_initializer loc env { edesc = EVar id; etyp = ty' } init k
  86
  87 (* Simplification of blocks within a statement *)
  88
  89 let rec unblock_stmt env s =
  90   match s.sdesc with
  91   | Sskip -> s
  92   | Sdo e -> s
  93   | Sseq(s1, s2) ->
  94       {s with sdesc = Sseq(unblock_stmt env s1, unblock_stmt env s2)}
  95   | Sif(e, s1, s2) ->
  96       {s with sdesc = Sif(e, unblock_stmt env s1, unblock_stmt env s2)}
  97   | Swhile(e, s1) ->
  98       {s with sdesc = Swhile(e, unblock_stmt env s1)}
  99   | Sdowhile(s1, e) ->
 100       {s with sdesc = Sdowhile(unblock_stmt env s1, e)}
 101   | Sfor(s1, e, s2, s3) ->
 102       {s with sdesc = Sfor(unblock_stmt env s1, e, unblock_stmt env s2, unblock_stmt env s3)}
 103   | Sbreak -> s
 104   | Scontinue -> s
 105   | Sswitch(e, s1) ->
 106       {s with sdesc = Sswitch(e, unblock_stmt env s1)}
 107   | Slabeled(lbl, s1) ->
 108       {s with sdesc = Slabeled(lbl, unblock_stmt env s1)}
 109   | Sgoto lbl -> s
 110   | Sreturn opte -> s
 111   | Sblock sl -> unblock_block env sl
 112   | Sdecl d -> assert false
 113
 114 and unblock_block env = function
 115   | [] -> sskip
 116   | {sdesc = Sdecl d; sloc = loc} :: sl ->
 117       process_decl loc env d (unblock_block env sl)
 118   | s :: sl ->
 119       sseq s.sloc (unblock_stmt env s) (unblock_block env sl)
 120
 121 (* Simplification of blocks within a function *)
 122
 123 let unblock_fundef env f =
 124   local_variables := [];
 125   let body = unblock_stmt env f.fd_body in
 126   let decls = !local_variables in
 127   local_variables := [];
 128   { f with fd_locals = f.fd_locals @ decls; fd_body = body }
 129
 130 (* Entry point *)
 131
 132 let program p =
 133   Transform.program ~fundef:unblock_fundef p