Initial snarf.

[shack.git] / arch / mir / util / mir_memory.ml

(*
   Insert Reserve and CopyOnWrite instructions into the MIR
   Copyright (C) 2001 Justin David Smith, Caltech

   This program is free software; you can redistribute it and/or
   modify it 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 program is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with this program; if not, write to the Free Software
   Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
 *)


(*
   WARNING  WARNING  WARNING  WARNING  WARNING  WARNING

   If you modify this file, you NEED to run the test/fc/memory
   test cases.  Obscure errors tend to pop up in this file when
   new MIR primitives are added (especially when the primitive
   is an alloc op) (both Jason and myself have been bitten by
   this at least once).  Only test/fc/memory really exercises
   the Reserve statements to ensure they are correct.
      -Justin, 2002.02.09

   WARNING  WARNING  WARNING  WARNING  WARNING  WARNING
 *)


(*
   WARNING  WARNING  WARNING  WARNING  WARNING  WARNING

   There is a serious logical flaw in Reserve statement scheduling.
   Consider the following snippet of code, for example:

      let v_index = ptr[off] in
      /* assume ptr is now dead */ /*1*/
      let v = PtrOfIndex v_index in
      ...

   Suppose ptr is dead after it is used; but v is live for awhile.
   If a Reserve statement is placed after v is bound, then everything
   is fine; we list v as a live pointer, but ptr is not listed because
   it is dead.  Here's the problem:  Suppose a Reserve statement is
   scheduled at /*1*/.  Note that ptr is already dead; furthermore,
   while we will decode v_index into a pointer real soon, it is NOT
   YET A POINTER, and will NOT be included in the reserve live ptrs!
   Therefore, we end up with code like this:

      let v_index = ptr[off] in
      Reserve([], #bytes, #ptrs);
      let v = PtrOfIndex v_index in
      ...

   Note that in this code, v is a pointer, but it was NOT listed in
   the most recent reserve; furthermore, ptr is dead in the reserve
   so if the only reference to v was in ptr, it is possible that v
   will be garbage-collected, causing a probable segfault when we
   attempt to use v.  This is bad!

   The problem here is that between the two let's, v is a ``live''
   pointer in the sense that the block will be referenced, but it is
   not yet a real pointer in a register, so Reserve statements placed
   here will miss block v as a live block.  Currently, this is not a
   problem -- this type of expression only occurs when we're reading
   a pointer from memory, and the dereference is always followed by
   the PtrOfIndex operation -- there is nothing that will cause a
   reserve to be scheduled here *IF* res_cross_conditionals is true.
   So we are okay.

   However, if Reserve scheduling gets more sophisticated, or if the
   res_cross_conditionals is set to false, it is possible that a
   Reserve will be scheduled between the two lets, which will cause
   serious problems.  There are also a few other contexts where this
   problem shows up (e.g. the SysMigrate faults), so be careful!

   A short-term hack if this problem occurs is to prevent the Reserve
   from crossing a certain boundary; e.g. place a Reserve of zero bytes
   after the second let.  This will prevent a Reserve from being
   scheduled between the lets, but we pay a performance penalty for
   doing this.  A better solution would be to mark the two lets as
   being a ``unit'' in the sense that no instructions can interleave
   with them.

   Damn, this is a subtle bug.  We need a proper solution to it.
      -Justin, 2002.01.15
 *)


(* Useful modules *)
open Debug
open Symbol
open Frame_type
open Sizeof_const

open Mir
open Mir_ds
open Mir_pos
open Mir_exn
open Mir_memory_sig

module Pos = MakePos (struct let name = "Mir_memory" end)
open Pos


module MirMemory (Frame : BackendSig) : MirMemorySig =
struct
   module MirUtil = Mir_util.MirUtil (Frame)
   module MirEnv = Mir_env.MirEnv (Frame)
   open Frame
   open MirUtil


   (***  Utilities  ***)


   let exp_pos pos =
      string_pos "Mir_memory" (exp_pos pos)

   let raw_block_header_size = Rawint.of_int precision_native_int false block_header_size


   (***  Propagation policies  ***)


   (* These constants control the propagation policies of Reserve and
      CopyOnWrite statements.  Note that later optimizations may attempt
      to further refine Reserve/COW placement, so here we only need a
      rough metric.  At this time it is not yet clear which policy will
      be best.

      The cross_conditionals variables determine whether a statement
      should be propagated above a conditional boundary -- if false,
      then any pending Reserve/COW will be placed only once we're CERTAIN
      the statement is needed; if true, then these statements may cross
      boundaries where it is LIKELY the statement is needed. *)
   let res_cross_conditionals    =  true
   let cow_cross_conditionals    =  true

   (* If cow_local_set is set, then we attempt to track LOCAL pointers
      (pointers which we know are allocated within the current atomic
      scope, or aliases of similar pointers).  These pointers do not
      need to be checked. *)
   let cow_local_set             =  true


   (***  Variable Environments  ***)


   (* Symbol sets *)
   let env_empty = SymbolSet.empty
   let env_add = SymbolSet.add
   let env_mem = SymbolSet.mem
   let env_remove env v =
      try SymbolSet.remove env v with
         Not_found -> env
   let env_fold = SymbolSet.fold
   let env_union = SymbolSet.union


   (* Live sets *)
   let live_empty = env_empty
   let live_union = env_union
   let live_list = SymbolSet.to_list
   let live_remove = env_remove


   (* Variable type environments *)
   let venv_find = SymbolTable.find
   let venv_lookup venv pos v =
      try venv_find venv v with
         Not_found -> raise (MirException (pos, UnboundVar v))


   (* variable_is_pointer *)
   let variable_is_pointer venv v =
      try
         let ac = venv_find venv v in
            atom_class_may_be_pointer ac
      with
         Not_found ->
            (* Note: some variables (e.g. global variables,
               variables in context) are not added to the
               venv.  These variables should be ignored anywho
               since they are usually handled separately and
               can contain pointers that are outside of the
               normal heap.  *)
            false


   (***  Atom Functions, and Live Set  ***)


   (* var_in_atom
      Returns true iff the specified variable name occurs within
      the atom specified. *)
   let rec var_in_atom v = function
      AtomVar (_, v')
    | AtomFunVar (_, v') ->
         Symbol.eq v v'
    | AtomInt _
    | AtomRawInt _
    | AtomFloat _ ->
         false
    | AtomUnop (_, a) ->
         var_in_atom v a
    | AtomBinop (_, a1, a2) ->
         var_in_atom v a1 || var_in_atom v a2


   (* live_add_var
      Adds a variable to the live environment, *if* the variable
      is a pointer variable as dictated by the variable environment. *)
   let live_add_var venv globals pos live v =
      let pos = string_pos "live_add_var" pos in
         if variable_is_pointer venv v && not (SymbolTable.mem globals v) then
            env_add live v
         else
            live

   let live_add_vars venv globals pos = List.fold_left (live_add_var venv globals pos)


   (* live_add_atom
      Adds variables occurring in this atom to the live set. *)
   let rec live_add_atom venv globals pos live a =
      let pos = string_pos "live_add_atom" pos in
         match a with
            AtomVar (_, v)
          | AtomFunVar (_, v) ->
               live_add_var venv globals pos live v
          | AtomInt _
          | AtomRawInt _
          | AtomFloat _ ->
               live
          | AtomUnop (_, a) ->
               live_add_atom venv globals pos live a
          | AtomBinop (_, a1, a2) ->
               live_add_atom venv globals pos (live_add_atom venv globals pos live a1) a2

   let live_add_atoms venv globals pos = List.fold_left (live_add_atom venv globals pos)


   (* live_add_alloc_op
      Adds variables occurring in this alloc operation to live set. *)
   let live_add_alloc_op venv globals pos live op =
      let pos = string_pos "live_add_alloc_op" pos in
         match op with
            AllocTuple atoms
          | AllocArray atoms
          | AllocUnion (_, atoms) ->
               live_add_atoms venv globals pos live atoms
          | AllocMArray (atoms, a) ->
               live_add_atoms venv globals pos (live_add_atom venv globals pos live a) atoms
          | AllocMalloc a ->
               live_add_atom venv globals pos live a


   (***  Copy-on-Write Management  ***)


   (* cow_empty_reserve
      Used by COW because we don't want to deal with reserve logic yet,
      at this point.  Instead we take the lazy route and create a dummy
      reserve info until reserve_expr can be run.  *)
   let cow_zero = AtomRawInt (Rawint.of_int Rawint.Int32 false 0)
   let cow_empty_reserve = (new_symbol_string "uninitialized_cow_reserve", [], cow_zero, cow_zero)


   (* cow_binding_occurrence
      A binding occurrence of a variable has occurred.  If this var
      appears in the list of written pointers, we must insert a
      CopyOnWrite check *now*. *)
   let cow_binding_occurrence venv pos loc v wrptrs e =
      let pos = string_pos "cow_binding_occurrence" pos in
         if env_mem wrptrs v then
            (* Binding occurrence here *)
            let ac = venv_lookup venv pos v in
            let wrptrs = env_remove wrptrs v in
            let e = CopyOnWrite (cow_empty_reserve, AtomVar (ac, v), e) in
               wrptrs, make_exp loc e
         else
            (* Binding occurrence does not affect us *)
            wrptrs, e


   (* cow_set_mem
      Process a setmem expression.  The atom is the pointer that is
      actually being written to.  Pointers in the local set are assumed
      to have been allocated within the current atomic scope, and are
      therefore never added to wrptrs.  *)
   let cow_set_mem loc a wrptrs local e =
      match a with
         AtomVar (_, v) ->
            if cow_local_set && env_mem local v then
               (* Do not add this local pointer. *)
               wrptrs, e
            else
               env_add wrptrs v, e
       | _ ->
            (* Arbitrary expression; we have to do the COW here *)
            let e = CopyOnWrite (cow_empty_reserve, a, e) in
               wrptrs, make_exp loc e


   (* cow_expr
      Inserts copy-on-write operations into the expression given.  The
      function returns a list of pointers which are written to, but have
      not yet been checked for copy-on-write, at a given level.  When we
      hit a binding occurence of a variable in this list, we must insert
      a CopyOnWrite check for the pointer.  The reserve information (which
      includes the current set of live pointers) is not computed here; you
      *must* run reserve_expr after running this function.

      Note that in the current implementation, a list of local allocations
      is maintained; this list must be cleared across an atomic boundary.
      For any pointer in this list, we KNOW that we have allocated it within
      the current atomic scope, therefore we don't need to check for COW.
      These pointers are therefore not added to the wrptrs list. *)
   let rec cow_expr venv local e =
      let pos = string_pos "cow_expr" (exp_pos e) in
      let loc = loc_of_exp e in
         match dest_exp_core e with
            LetAtom (v, ac, a, e) ->
               let wrptrs, e = cow_expr venv local e in
               let wrptrs, e = cow_binding_occurrence venv pos loc v wrptrs e in
                  wrptrs, make_exp loc (LetAtom (v, ac, a, e))
          | TailCall (op, f, atoms) ->
               env_empty, make_exp loc (TailCall (op, f, atoms))
          | Match (a, ac, cases) ->
               cow_match_expr venv local pos loc a ac cases
          | IfThenElse (op, a1, a2, e1, e2) ->
               cow_ifthenelse_expr venv local pos loc op a1 a2 e1 e2
          | IfType (obj, names, name, v, e1, e2) ->
               cow_iftype_expr venv local pos loc obj names name v e1 e2
          | LetExternal (v, ac, f, atoms, e) ->
               let wrptrs, e = cow_expr venv local e in
               let wrptrs, e = cow_binding_occurrence venv pos loc v wrptrs e in
                  wrptrs, make_exp loc (LetExternal (v, ac, f, atoms, e))
          | LetExternalReserve (rinfo, v, ac, f, atoms, e) ->
               let wrptrs, e = cow_expr venv local e in
               let wrptrs, e = cow_binding_occurrence venv pos loc v wrptrs e in
                  wrptrs, make_exp loc (LetExternalReserve (rinfo, v, ac, f, atoms, e))
          | Reserve (reserve_info, e) ->
               let wrptrs, e = cow_expr venv local e in
                  wrptrs, make_exp loc (Reserve (reserve_info, e))
          | LetAlloc (v, op, e) ->
               let local = env_add local v in
               let wrptrs, e = cow_expr venv local e in
               let wrptrs, e = cow_binding_occurrence venv pos loc v wrptrs e in
                  wrptrs, make_exp loc (LetAlloc (v, op, e))
          | SetMem (ac, ptrty, a1, a2, a3, e) ->
               let wrptrs, e = cow_expr venv local e in
               let wrptrs, e = cow_set_mem loc a1 wrptrs local e in
                  wrptrs, make_exp loc (SetMem (ac, ptrty, a1, a2, a3, e))
          | SetGlobal (ac, v, a, e) ->
               (* BUG: have to decide what to do here --jyh *)
               let wrptrs, e = cow_expr venv local e in
                  wrptrs, make_exp loc (SetGlobal (ac, v, a, e))
          | BoundsCheck (label, ptrty, ptr, start, stop, e) ->
               let wrptrs, e = cow_expr venv local e in
                  wrptrs, make_exp loc (BoundsCheck (label, ptrty, ptr, start, stop, e))
          | LowerBoundsCheck (label, ptrty, ptr, start, e) ->
               let wrptrs, e = cow_expr venv local e in
                  wrptrs, make_exp loc (LowerBoundsCheck (label, ptrty, ptr, start, e))
          | UpperBoundsCheck (label, ptrty, ptr, stop, e) ->
               let wrptrs, e = cow_expr venv local e in
                  wrptrs, make_exp loc (UpperBoundsCheck (label, ptrty, ptr, stop, e))
          | PointerIndexCheck (label, ptrty, v, ac, index, e) ->
               let wrptrs, e = cow_expr venv local e in
               let wrptrs, e = cow_binding_occurrence venv pos loc v wrptrs e in
                  wrptrs, make_exp loc (PointerIndexCheck (label, ptrty, v, ac, index, e))
          | FunctionIndexCheck (label, funty, v, ac, index, e) ->
               let wrptrs, e = cow_expr venv local e in
               let wrptrs, e = cow_binding_occurrence venv pos loc v wrptrs e in
                  wrptrs, make_exp loc (FunctionIndexCheck (label, funty, v, ac, index, e))
          | Memcpy (ptrty, dst_base, dst_off, src_base, src_off, size, e) ->
               let wrptrs, e = cow_expr venv local e in
               let wrptrs, e = cow_set_mem loc dst_base wrptrs local e in
                  wrptrs, make_exp loc (Memcpy (ptrty, dst_base, dst_off, src_base, src_off, size, e))
          | Debug (info, e) ->
               let wrptrs, e = cow_expr venv local e in
                  wrptrs, make_exp loc (Debug (info, e))
          | PrintDebug (v1, v2, atoms, e) ->
               let wrptrs, e = cow_expr venv local e in
                  wrptrs, make_exp loc (PrintDebug (v1, v2, atoms, e))
          | CommentFIR (fir, e) ->
               let wrptrs, e = cow_expr venv local e in
                  wrptrs, make_exp loc (CommentFIR (fir, e))
          | SysMigrate (label, dptr, doff, f, env) ->
               env_empty, make_exp loc (SysMigrate (label, dptr, doff, f, env))
          | Atomic (f, i, e) ->
               env_empty, make_exp loc (Atomic (f, i, e))
          | AtomicRollback (level, i) ->
               env_empty, make_exp loc (AtomicRollback (level, i))
          | AtomicCommit (level, e) ->
               (* I'm currently paranoid, and don't allow COW to
                  interact across an atomic COMMIT boundary. *)
               let e = cow_top_expr venv env_empty e in
                  env_empty, make_exp loc (AtomicCommit (level, e))
          | CopyOnWrite (reserve_info, ptr, e) ->
               let wrptrs, e = cow_expr venv local e in
                  wrptrs, make_exp loc (CopyOnWrite (reserve_info, ptr, e))
          | SpecialCall _ ->
               raise (MirException (pos, InternalError "SpecialCall not allowed by this point"))


   (* cow_match_expr
      Handles a conditional expression in COW analysis. *)
   and cow_match_expr venv local pos loc a ac cases =
      let pos = string_pos "cow_match_expr" pos in
      let process_case (wrptrs, cases) (i, e) =
         let wrptrs', e = cow_cond_top_expr venv local e in
         let wrptrs = env_union wrptrs wrptrs' in
         let cases = (i, e) :: cases in
            wrptrs, cases
      in (* End of process_case *)
      let wrptrs, cases = List.fold_left process_case (env_empty, []) cases in
      let cases = List.rev cases in
         wrptrs, make_exp loc (Match (a, ac, cases))


   (* cow_ifthenelse_expr
      Handles a conditional expression in COW analysis. *)
   and cow_ifthenelse_expr venv local pos loc op a1 a2 e1 e2 =
      let pos = string_pos "cow_ifthenelse_expr" pos in
      let wrptrs1, e1 = cow_cond_top_expr venv local e1 in
      let wrptrs2, e2 = cow_cond_top_expr venv local e2 in
      let wrptrs = env_union wrptrs1 wrptrs2 in
         wrptrs, make_exp loc (IfThenElse (op, a1, a2, e1, e2))


   (* cow_iftype_expr
      Handles a conditional type expression in COW analysis. *)
   and cow_iftype_expr venv local pos loc obj names name v e1 e2 =
      let pos = string_pos "cow_iftype_expr" pos in
      let wrptrs1, e1 = cow_cond_top_expr venv local e1 in
      let wrptrs2, e2 = cow_cond_top_expr venv local e2 in
      (* Note:  v is a binding occurrence for e1 ONLY *)
      let wrptrs1, e1 = cow_binding_occurrence venv pos loc v wrptrs1 e1 in
      let wrptrs = env_union wrptrs1 wrptrs2 in
         wrptrs, make_exp loc (IfType (obj, names, name, v, e1, e2))


   (* cow_top_expr
      Similar to above function, except we assume e is the top-most
      expression in its scope (unconditional block, function, etc).
      All pending COW's must be prepended here. *)
   and cow_top_expr venv local e =
      let pos = string_pos "cow_top_expr" (exp_pos e) in
      let wrptrs, e = cow_expr venv local e in
      let loc = loc_of_exp e in
      let prepend_cow_check e ptr =
         let ac = venv_lookup venv pos ptr in
            make_exp loc (CopyOnWrite (cow_empty_reserve, AtomVar (ac, ptr), e))
      in
         env_fold prepend_cow_check e wrptrs


   (* cow_cond_top_expr
      Similar to cow_top_expr, except this is used at the top of a
      conditional block.  This code checks to see if we are allowed
      to cross conditional boundaries. *)
   and cow_cond_top_expr venv local e =
      if cow_cross_conditionals then
         cow_expr venv local e
      else
         env_empty, cow_top_expr venv local e


   (* cow_top_expr
      Interface to copy-on-write system. *)
   let cow_top_expr venv e = cow_top_expr venv env_empty e


   (***  Reserve Expressions  ***)


   (* res_arith
      Defines simple arithmetic on reserve expressions. *)
   type res_arith =
      Add of res_arith list
    | Mul of res_arith list
    | Max of res_arith list
    | Value of atom


   (* Define the default state, indicating no reservation needed *)
   let raw_zero = Rawint.of_int precision_pointer false 0
   let raw_one = Rawint.of_int precision_pointer false 1
   let raw_header = Rawint.of_int precision_native_int false block_header_size
   let reserve_null = Value (AtomRawInt raw_zero), Value (AtomRawInt raw_zero)

   (* Some convenient sizes for the headers and whatnot *)
   let size_zero   = Value (AtomRawInt raw_zero)
   let size_one    = Value (AtomRawInt raw_one)
   let size_header = Value (AtomRawInt raw_header)


   (* res_add
      res_max
      Adds a new addition or maximization operation to reserve. *)
   let res_add res1 res2 =
      match res1, res2 with
         Add ls1, Add ls2 ->
            Add (ls1 @ ls2)
       | Add ls1, _ ->
            Add (res2 :: ls1)
       | _, Add ls2 ->
            Add (res1 :: ls2)
       | _ ->
            Add [res1; res2]

   let res_mul res1 res2 =
      match res1, res2 with
         Mul ls1, Mul ls2 ->
            Mul (ls1 @ ls2)
       | Mul ls1, _ ->
            Mul (res2 :: ls1)
       | _, Mul ls2 ->
            Mul (res1 :: ls2)
       | _ ->
            Mul [res1; res2]

   let res_max res1 res2 =
      match res1, res2 with
         Max ls1, Max ls2 ->
            Max (ls1 @ ls2)
       | Max ls1, _ ->
            Max (res2 :: ls1)
       | _, Max ls2 ->
            Max (res1 :: ls2)
       | _ ->
            Max [res1; res2]


   (* res_simplify
      Simplifies a reserve expression by folding constant operations
      where possible, and simplifying the remaining expressions. *)
   let rec res_simplify res =
      (* Fold the constant values together.  arithop is the arithmetic
         operator to apply to the constants, and ident is the identity
         value for the operator.  construct is the res_arith constructor
         corresponding to this operation.  *)
      let fold_constants arithop ident ls construct =
         let ls = List.map res_simplify ls in
         let result, ls = List.fold_left (fun (result, ls) res ->
            match res with
               Value (AtomRawInt i) ->
                  arithop result i, ls
             | _ ->
                  result, res :: ls) (ident, []) ls
         in
            if ls = [] then
               Value (AtomRawInt result)
            else if Rawint.compare result ident = 0 then
               construct ls
            else
               construct (Value (AtomRawInt result) :: ls)
      in
         match res with
            Add ls ->
               fold_constants Rawint.add raw_zero ls (fun ls -> Add ls)
          | Mul ls ->
               fold_constants Rawint.mul raw_one  ls (fun ls -> Mul ls)
          | Max ls ->
               fold_constants Rawint.max raw_zero ls (fun ls -> Max ls)
          | Value a ->
               Value a


   (* atom_of_res
      Transforms a simple res expression into an atom expression. *)
   let rec atom_of_res res =
      let res = res_simplify res in
      let rec atom_of_list op = function
         res :: [] ->
            atom_of_res res
       | res :: ls ->
            AtomBinop (op, atom_of_res res, atom_of_list op ls)
       | [] ->
            AtomRawInt raw_zero
      in
         match res with
            Add ls ->
               atom_of_list (PlusOp ac_native_unsigned) ls
          | Mul ls ->
               atom_of_list (MulOp ac_native_unsigned) ls
          | Max ls ->
               atom_of_list (MaxOp ac_native_unsigned) ls
          | Value a ->
               a


   (* var_in_res
      Returns true if the named variable occurs in res.  This is
      used in Reserve statement scheduling to determine if we can
      propagate a Reserve upward past a variable binding occurrence. *)
   let rec var_in_res v = function
      Add ls
    | Mul ls
    | Max ls ->
         List.exists (var_in_res v) ls
    | Value a ->
         var_in_atom v a


   (* sizeof_alloc_op
      Determines the size of the alloc operation, for use by reserve.
      A pair is returned, of the total bytes required and the number
      of pointer entries required. *)
   let sizeof_alloc_op = function
      AllocTuple atoms
    | AllocArray atoms
    | AllocUnion (_, atoms) ->
         (* ML blocks contain a pointer/int for each of the args.
            These blocks _are_ saved in the pointer table, so
            we reserve space for them.  *)
         let size_tuple = sizeof_atom_list atoms in
         let size_tuple = Int32.add size_tuple (Int32.of_int block_header_size) in
         let size_tuple = Rawint.of_int32 precision_pointer false size_tuple in
            Value (AtomRawInt size_tuple), size_one
    | AllocMalloc (AtomRawInt i) ->
         (* The atom specifies a constant number of bytes to alloc.
            This is an indexed pointer, so we need a ptr space. *)
         let size = Rawint.add i raw_block_header_size in
            Value (AtomRawInt size), size_one
    | AllocMalloc a ->
         (* The atom specifies a variable number of bytes to alloc.
            This is an indexed pointer, so we need a ptr space. *)
         Add [Value a; size_header], size_one
    | AllocMArray (dimens, _) ->
         (* The dimens specifies a multi-dimensional array.
            Add together the total size.  *)
         let rec collect dimens =
            match dimens with
               a :: dimens ->
                  let bytes, ptrs = collect dimens in
                  let bytes = Add [Mul [Value a; bytes]; size_header] in
                  let ptrs = Add [Mul [Value a; ptrs]; size_one] in
                     bytes, ptrs
             | [] ->
                  reserve_null
         in
            collect dimens


   (* build_reserve_info
      Builds the reserve info from resmem, resptr information
      and the live pointers list.  You can also provide a base
      name for the unique label that is generated here. *)
   let build_reserve_info name live (resmem, resptr) =
      let resmem = atom_of_res resmem in
      let resptr = atom_of_res resptr in
      let label = new_symbol_string name in
      let live = live_list live in
         (label, live, resmem, resptr)


   (* build_reserve_expr
      Constructs a reserve expression (if warranted) *)
   let build_reserve_expr live (resmem, resptr) e =
      let resmem = res_simplify resmem in
      let resptr = res_simplify resptr in
      let loc = loc_of_exp e in
         match resmem, resptr with
            Value (AtomRawInt i), Value (AtomRawInt j)
            when Rawint.compare i raw_zero = 0 && Rawint.compare j raw_zero = 0 ->
               (* No reserve required here *)
               e
          | _ ->
               let rinfo = build_reserve_info "reserve" live (resmem, resptr) in
                  make_exp loc (Reserve (rinfo, e))


   (* reserve_binding_occurrence
      A binding occurrence of v occurs here.  Check to see if v is used
      anywhere in the reserve expression; if so, then we must emit a
      new reserve statement here. *)
   let reserve_binding_occurrence live (resmem, resptr) v e =
      if var_in_res v resmem || var_in_res v resptr then
         (* Variable occurs in reserve expression; must emit Reserve *)
         let e = build_reserve_expr live (resmem, resptr) e in
         let live = live_remove live v in
            live, reserve_null, e
      else
         (* Variable does not occur; we can pass the reserve up *)
         let live = live_remove live v in
            live, (resmem, resptr), e


   (***  Reserve (Expressions)  ***)


   (* reserve_expr
      Inserts memory operations into the expression given.  Several sets
      of information are maintained here, to be explicit on what they are:
       * venv (passed down) contains the set of variables with their types
       * live (passed up) contains information on what variables are live.
       * resmem (passed up) - memory reservation requirements from below.
         This is a list of atoms containing size expressions.  When any
         variable mentioned in the list is bound (going up), we must insert
         a new reserve expression.
       * resptr (passed up) - a number indicating the number of pointers
         required by expressions below.  *)
   let rec reserve_expr venv globals e =
      let pos = string_pos "reserve_expr" (exp_pos e) in
      let loc = loc_of_exp e in
         match dest_exp_core e with
            LetAtom (v, ac, a, e) ->
               let live, res, e = reserve_expr venv globals e in
               let live, res, e = reserve_binding_occurrence live res v e in
               let live = live_add_atom venv globals pos live a in
                  live, res, make_exp loc (LetAtom (v, ac, a, e))
          | TailCall (op, f, atoms) ->
               let live = live_add_atoms venv globals pos live_empty atoms in
                  live, reserve_null, make_exp loc (TailCall (op, f, atoms))
          | Match (a, ac, cases) ->
               reserve_match_expr venv globals pos loc a ac cases
          | IfThenElse (op, a1, a2, e1, e2) ->
               reserve_ifthenelse_expr venv globals pos loc op a1 a2 e1 e2
          | IfType (obj, names, name, v, e1, e2) ->
               reserve_iftype_expr venv globals pos loc obj names name v e1 e2
          | LetExternal (v, ac, f, atoms, e) ->
               let live, res, e = reserve_expr venv globals e in
               let live, res, e = reserve_binding_occurrence live res v e in
               let live = live_add_atoms venv globals pos live atoms in
                  live, res, make_exp loc (LetExternal (v, ac, f, atoms, e))
          | LetExternalReserve (rinfo, v, ac, f, atoms, e) ->
               reserve_external_reserve_expr venv globals pos loc rinfo v ac f atoms e
          | Reserve (rinfo, e) ->
               let _, _, mem, ptr = rinfo in
               let live, e = reserve_top_expr venv globals e in
               let live = live_add_atoms venv globals pos live [mem; ptr] in
                  live, reserve_null, make_exp loc (Reserve (rinfo, e))
          | LetAlloc (v, op, e) ->
               reserve_alloc_expr venv globals pos loc v op e
          | SetMem (ac, ptrty, a1, a2, a3, e) ->
               let live, res, e = reserve_expr venv globals e in
               let live = live_add_atoms venv globals pos live [a1; a2; a3] in
                  live, res, make_exp loc (SetMem (ac, ptrty, a1, a2, a3, e))
          | SetGlobal (ac, v, a, e) ->
               let live, res, e = reserve_expr venv globals e in
               let live = live_add_atom venv globals pos live a in
                  live, res, make_exp loc (SetGlobal (ac, v, a, e))
          | BoundsCheck (label, ptrty, ptr, start, stop, e) ->
               let live, res, e = reserve_expr venv globals e in
               let live = live_add_atoms venv globals pos live [ptr; start; stop] in
                  live, res, make_exp loc (BoundsCheck (label, ptrty, ptr, start, stop, e))
          | LowerBoundsCheck (label, ptrty, ptr, start, e) ->
               let live, res, e = reserve_expr venv globals e in
               let live = live_add_atoms venv globals pos live [ptr; start] in
                  live, res, make_exp loc (LowerBoundsCheck (label, ptrty, ptr, start, e))
          | UpperBoundsCheck (label, ptrty, ptr, stop, e) ->
               let live, res, e = reserve_expr venv globals e in
               let live = live_add_atoms venv globals pos live [ptr; stop] in
                  live, res, make_exp loc (UpperBoundsCheck (label, ptrty, ptr, stop, e))
          | PointerIndexCheck (label, ptrty, v, ac, index, e) ->
               let live, res, e = reserve_expr venv globals e in
               let live, res, e = reserve_binding_occurrence live res v e in
               let live = live_add_atom venv globals pos live index in
                  live, res, make_exp loc (PointerIndexCheck (label, ptrty, v, ac, index, e))
          | FunctionIndexCheck (label, funty, v, ac, index, e) ->
               let live, res, e = reserve_expr venv globals e in
               let live, res, e = reserve_binding_occurrence live res v e in
               let live = live_add_atom venv globals pos live index in
                  live, res, make_exp loc (FunctionIndexCheck (label, funty, v, ac, index, e))
          | Memcpy (ptrty, dst_base, dst_off, src_base, src_off, size, e) ->
               let live, res, e = reserve_expr venv globals e in
               let live = live_add_atoms venv globals pos live [dst_base; dst_off; src_base; src_off; size] in
                  live, res, make_exp loc (Memcpy (ptrty, dst_base, dst_off, src_base, src_off, size, e))
          | Debug (info, e) ->
               let live, res, e = reserve_expr venv globals e in
                  live, res, make_exp loc (Debug (info, e))
          | PrintDebug (v1, v2, atoms, e) ->
               let live, res, e = reserve_expr venv globals e in
               let live = live_add_atoms venv globals pos live atoms in
               let live = live_add_vars venv globals pos live [v1; v2] in
                  live, res, make_exp loc (PrintDebug (v1, v2, atoms, e))
          | CommentFIR (fir, e) ->
               let live, res, e = reserve_expr venv globals e in
                  live, res, make_exp loc (CommentFIR (fir, e))
          | SysMigrate (label, dptr, doff, f, env) ->
               let live = live_add_atoms venv globals pos live_empty [dptr; doff; env] in
                  live, reserve_null, make_exp loc (SysMigrate (label, dptr, doff, f, env))
          | Atomic (f, i, e) ->
               let live = live_add_atoms venv globals pos live_empty [i; e] in
                  live, reserve_null, make_exp loc (Atomic (f, i, e))
          | AtomicRollback (level, i) ->
               let live = live_add_atoms venv globals pos live_empty [level; i] in
                  live, reserve_null, make_exp loc (AtomicRollback (level, i))
          | AtomicCommit (level, e) ->
               let live, res, e = reserve_expr venv globals e in
               let live = live_add_atom venv globals pos live level in
                  live, res, make_exp loc (AtomicCommit (level, e))
          | CopyOnWrite (rinfo, ptr, e) ->
               reserve_copyonwrite_expr venv globals pos loc rinfo ptr e
          | SpecialCall _ ->
               raise (MirException (pos, InternalError "SpecialCall not allowed by this point"))


   (* reserve_match_expr
      Match statements (like other conditional expressions) require
      a maximization operation. *)
   and reserve_match_expr venv globals pos loc a ac cases =
      let pos = string_pos "reserve_match_expr" pos in

      (* process_case
         Processes an individual case.  The live set will be the
         union of live sets of each case; the reserves are the
         maximizations of each individual case. *)
      let process_case (live, (resmem, resptr), cases) (i, e) =
         let live', res', e = reserve_cond_top_expr venv globals e in
         let resmem', resptr' = res' in
         let live = live_union live live' in
         let resmem = res_max resmem resmem' in
         let resptr = res_max resptr resptr' in
         let cases = (i, e) :: cases in
            live, (resmem, resptr), cases
      in (* End of process_case *)

      (* Processes all cases to pass up. *)
      let fold_src = live_empty, reserve_null, [] in
      let live, res, cases = List.fold_left process_case fold_src cases in
      let cases = List.rev cases in
      let live = live_add_atom venv globals pos live a in
         live, res, make_exp loc (Match (a, ac, cases))


   (* reserve_ifthenelse_expr
      Similar to above code, except we only have two cases here. *)
   and reserve_ifthenelse_expr venv globals pos loc op a1 a2 e1 e2 =
      let pos = string_pos "reserve_ifthenelse_expr" pos in
      let live1, res1, e1 = reserve_cond_top_expr venv globals e1 in
      let live2, res2, e2 = reserve_cond_top_expr venv globals e2 in
      let resmem1, resptr1 = res1 in
      let resmem2, resptr2 = res2 in
      let live = live_union live1 live2 in
      let live = live_add_atoms venv globals pos live [a1; a2] in
      let resmem = res_max resmem1 resmem2 in
      let resptr = res_max resptr1 resptr2 in
         live, (resmem, resptr), make_exp loc (IfThenElse (op, a1, a2, e1, e2))


   (* reserve_iftype_expr
      Similar to above code for ifthenelse, except for two concerns:
         1. There is a binding occurrence of v here, along e1.
         2. There is an implicit allocation of 2 words (plus header)
            along the e1 branch; note this means we must do the
            reserve UNCONDITIONALLY to ensure memory has been set
            aside if we attempt the allocation here.  *)
   and reserve_iftype_expr venv globals pos loc obj names name v e1 e2 =
      let pos = string_pos "reserve_iftype_expr" pos in

      (* Get the live sets and current reserves for each branch *)
      let live1, res1, e1 = reserve_cond_top_expr venv globals e1 in
      let live2, res2, e2 = reserve_cond_top_expr venv globals e2 in

      (* Note the binding occurence of v along e1 branch *)
      let live1, res1, e1 = reserve_binding_occurrence live1 res1 v e1 in

      (* Unify the live information and add the new atoms *)
      let live = live_union live1 live2 in
      let live = live_add_atoms venv globals pos live [obj; names; name] in

      (* Unify the reserve information for each branch *)
      let resmem1, resptr1 = res1 in
      let resmem2, resptr2 = res2 in
      let resmem = res_max resmem1 resmem2 in
      let resptr = res_max resptr1 resptr2 in

      (* NOW we can add the implicit allocation of 8 bytes plus header *)
      let tuple_size = Rawint.of_int precision_native_int false (2 * sizeof_int32) in
      let resmem' = Value (AtomRawInt (Rawint.add tuple_size raw_header)) in
      let resptr' = Value (AtomRawInt raw_one) in
      let resmem = res_add resmem resmem' in
      let resptr = res_add resptr resptr' in
         live, (resmem, resptr), make_exp loc (IfType (obj, names, name, v, e1, e2))


   (* reserve_alloc_expr
      Reservation has to be enhanced to take into account this
      allocation operation. *)
   and reserve_alloc_expr venv globals pos loc v op e =
      let pos = string_pos "reserve_alloc_expr" pos in

      (* Compute live and reserves for rest of program *)
      let live, res, e = reserve_expr venv globals e in
      let live, res, e = reserve_binding_occurrence live res v e in

      (* Update live set to include atoms in alloc operator *)
      let live = live_add_alloc_op venv globals pos live op in

      (* Update reserve parametres to include this allocation *)
      let resmem, resptr = res in
      let resmem', resptr' = sizeof_alloc_op op in
      let resmem = res_add resmem resmem' in
      let resptr = res_add resptr resptr' in
         live, (resmem, resptr), make_exp loc (LetAlloc (v, op, e))


   (* reserve_copyonwrite_expr
      Copy-on-write can allocate new memory in the heap; the COW
      code will call GC if it needs to alloc more memory, but to
      do this we have to know how much memory is going to be
      allocated further down (we need the reserve parametres).
      The GC isn't guaranteed to be called, so any reserve params
      from here have to be passed up, as well.  *)
   and reserve_copyonwrite_expr venv globals pos loc rinfo ptr e =
      let pos = string_pos "reserve_copyonwrite_expr" pos in
      let live, res, e = reserve_expr venv globals e in

      (* Generate the reserve_info record *)
      let rinfo = build_reserve_info "copy_on_write" live res in

      (* Update the live set to contain this atom *)
      let live = live_add_atom venv globals pos live ptr in
         live, res, make_exp loc (CopyOnWrite (rinfo, ptr, e))


   (* reserve_external_reserve_expr
      This external call may require a garbage collection.

      BUG JYH: this is incorrect.  We need to force a reserve
      after the external call.  The reserve_expr should be
      reserve_top_expr, but I'm confused about the reserve
      binding occurrences...
      
      JDS TEMP: I think I have fixed this.

      To explain more: LetExternalReserve is a reserve barrier.
      Since we don't know if the extcall will allocate, we
      must assume that it leaves no free space on the heap.
      That means we need a new reserve before the body e.  *)
   and reserve_external_reserve_expr venv globals pos loc rinfo v ac f atoms e =
      let pos = string_pos "reserve_external_reserve_expr" pos in
      let live, e = reserve_top_expr venv globals e in

      (* reserve_top_expr forces a Reserve statement before e, so we have
         no allocation request to pass up at this point.  Therefore we will
         revert to reserve_null. *)
      let res = reserve_null in
      let live, res, e = reserve_binding_occurrence live res v e in

      (* Generate the reserve_info record *)
      let rinfo = build_reserve_info "external_reserve" live res in

      (* Update the live set to include the arguments *)
      let live = live_add_atoms venv globals pos live atoms in
         live, res, make_exp loc (LetExternalReserve (rinfo, v, ac, f, atoms, e))


   (* reserve_top_expr
      Similar to above function, but forces a reserve expression
      at the beginning of the expression list.  Use for the first
      expression of a function, or when another barrier forces
      us to place a reserve here.  The live set is still returned. *)
   and reserve_top_expr venv globals e =
      let live, res, e = reserve_expr venv globals e in
      let e = build_reserve_expr live res e in
         live, e


   (* reserve_cond_top_expr
      Conditional expressions use this at the top of each case.
      This checks whether reserves are permitted to cross a cond
      boundary. *)
   and reserve_cond_top_expr venv globals e =
      if res_cross_conditionals then
         reserve_expr venv globals e
      else
         let live, e = reserve_top_expr venv globals e in
            live, reserve_null, e


   (***  Interface Code  ***)


   (* mir_memory
      Adds copy-on-write and reserve instructions to a MIR expression *)
   let mir_memory venv globals e =
      let e = cow_top_expr venv e in
      let _, e = reserve_top_expr venv globals e in
         e


   (* memory *)
   let memory prog =
      let funs = prog.prog_funs in
      let globals = prog.prog_globals in
      let venv = MirEnv.mir_venv_prog prog in
      let memory_fun _ (line, args, e) =
         let e = mir_memory venv globals e in
            (line, args, e)
      in
      let funs = SymbolTable.mapi memory_fun funs in
      let prog = { prog with prog_funs = funs } in
         if debug Mir_state.debug_print_mir then
            Mir_print.debug_prog "After memory" prog;
         prog

   let memory = Fir_state.profile "Mir_memory.memory" memory


end (* struct *)