arch/mir/util/mir_simplify.ml

   1 (*
   2    Simplifies the MIR.  This file rewrites some of the higher
   3    level MIR primitives into simpler expressions so we don't
   4    have to worry about them in the backend -- some of the safety
   5    checks and whatnot are harder to deal with in backend.  Note
   6    that this code may be called by the backend itself if they
   7    need to run an expression...
   8
   9    --
  10    Copyright (C) 2001 Justin David Smith, Caltech
  11
  12    This program is free software; you can redistribute it and/or
  13    modify it under the terms of the GNU General Public License
  14    as published by the Free Software Foundation; either version 2
  15    of the License, or (at your option) any later version.
  16
  17    This program is distributed in the hope that it will be useful,
  18    but WITHOUT ANY WARRANTY; without even the implied warranty of
  19    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  20    GNU General Public License for more details.
  21
  22    You should have received a copy of the GNU General Public License
  23    along with this program; if not, write to the Free Software
  24    Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
  25  *)
  26
  27
  28 (* Useful modules *)
  29 open Debug
  30 open Symbol
  31 open Interval_set
  32
  33 open Fir_set
  34
  35 open Frame_type
  36 open Sizeof_const
  37
  38 open Mir
  39 open Mir_ds
  40 open Mir_pos
  41 open Mir_exn
  42 open Mir_simplify_sig
  43
  44 module Pos = MakePos (struct let name = "Mir_simplify" end)
  45 open Pos
  46
  47
  48 (***  Policies  ***)
  49
  50
  51 module MirSimplify (Frame : BackendSig) : MirSimplifySig =
  52 struct
  53    module MirUtil = Mir_util.MirUtil (Frame)
  54    module MirArity = Mir_arity.MirArity (Frame)
  55    open Frame
  56    open MirUtil
  57    open MirArity
  58
  59    let exp_pos pos =
  60       string_pos "Mir_simplify" (exp_pos pos)
  61
  62
  63    (***  Simplification of Atoms  ***)
  64
  65
  66    (*
  67       These functions transform the complex *atom* expressions into simpler
  68       expressions that we can work with in the backend.  Note that simplifying
  69       atoms may require the addition of new *expression* statements, PRIOR to
  70       the use of the atom.  Because of this, we have to play a bit of a logic
  71       game here.
  72
  73       Each of these functions takes a function called e_cont, as well as the
  74       atom to be simplified.  The code computes the expression and a new,
  75       simplified atom expression -- the simplified atom is usually a variable
  76       that contains the result.  We call e_cont with *this* atom, and e_cont
  77       computes the rest of the program with the substituted atom.  We then
  78       prepend our expression to the result.  A new expression (with the
  79       substituted atoms) is returned.
  80     *)
  81
  82
  83    (* Specifies what operation to perform for *_of_index functions.
  84       The *_of_index functions take this operator to determine what
  85       type of code they are emitting. *)
  86    type op =
  87       Safe        (* Pointer is safe, no checks required *)
  88     | Unsafe      (* Pointer is unsafe, but no check required *)
  89     | UnsafeCheck (* Pointer is unsafe, please check it *)
  90
  91
  92    (* is_safe
  93       Returns true if the operation specified is ``safe''.  Note: this
  94       affects the memory representation only; if no safety checks were
  95       enabled, then we'll call everything safe so everything uses the
  96       simple representation. *)
  97    let is_safe = function
  98       Safe ->
  99          true
 100     | Unsafe
 101     | UnsafeCheck ->
 102          not (Fir_state.safety_enabled ())
 103
 104
 105    (* do_check
 106       Returns true if the operation specified wants to ``check''. *)
 107    let do_check = function
 108       Safe
 109     | Unsafe ->
 110          false
 111     | UnsafeCheck ->
 112          true
 113
 114
 115    (* pointer_of_index
 116       Express a hashed index->pointer operation, assuming the usual
 117       safety checks may be required in the code.  This uses the pointer
 118       table.  The op specifies whether this is a safe index->pointer
 119       conversion, or an unsafe.  The op also specifies whether checks
 120       should be done.  *)
 121    let pointer_of_index arity_tags pos loc ptrty op a_hashed_index e_cont =
 122       let pos = string_pos "pointer_of_index" pos in
 123       let v_index = new_symbol_string "index" in
 124       let v_index_test = new_symbol_string "index_test" in
 125       let v_pointer = new_symbol_string "pointer" in
 126       let v_bit = new_symbol_string "bit" in
 127       let ac_pointer = ACPointer ptrty in
 128       let a_cont = AtomVar (ac_pointer, v_pointer) in
 129       let e_cont = e_cont a_cont in
 130
 131       (* Construct the segfault expressions *)
 132       let seg_fault_index_expr =    (* Index was invalid *)
 133          make_exp loc (TailCall (ExternalCall, seg_fault_labels.(index_fault),
 134                    [a_hashed_index; AtomVar (ac_native_unsigned, v_index)]))
 135       in
 136       let seg_fault_pointer_expr =  (* Pointer in ptbl was invalid *)
 137          make_exp loc (TailCall (ExternalCall, seg_fault_labels.(pointer_index_fault),
 138                    [a_hashed_index;
 139                     AtomVar (ac_native_unsigned, v_index);
 140                     AtomVar (ac_pointer, v_pointer)]))
 141       in
 142
 143       (* STEP 1 - Compute index from hash. *)
 144       let build_step1 e =
 145          if is_safe op then
 146             (* Safe pointers do not hash their value, currently *)
 147             make_exp loc (LetAtom (v_index, ac_native_unsigned, a_hashed_index, e))
 148          else
 149             (* Convert an unsafe hashed index into a real index *)
 150             make_exp loc (LetAtom (v_index, ac_native_unsigned,
 151                      AtomBinop (AndOp ac_native_unsigned, AtomRawInt (Rawint.of_int Rawint.Int32 false 0xfffffffc),
 152                      AtomBinop (XorOp ac_native_unsigned, a_hashed_index, hash_native_unsigned)), e))
 153       in (* end of build_step1 *)
 154
 155       (* STEP 2 - Check that the index is valid. *)
 156       let build_step2 e =
 157          if do_check op then
 158             (* Check that it is a valid index *)
 159             make_exp loc (LetAtom (v_index_test, ac_native_bool,
 160                      AtomBinop (LtOp ac_native_unsigned,
 161                                 AtomVar (ac_native_unsigned, v_index),
 162                                 AtomVar (ac_native_unsigned, pointer_size)),
 163             make_exp loc (Match (AtomVar (ac_native_bool, v_index_test), ac_native_bool,
 164                    [RawIntSet native_false_set, seg_fault_index_expr;
 165                     RawIntSet native_true_set, e]))))
 166          else
 167             (* No check required. *)
 168             e
 169       in (* end of build_step2 *)
 170
 171       (* STEP 3 - Read from pointer table *)
 172       let build_step3 e =
 173          (* Read the pointer from the ptbl *)
 174          make_exp loc (LetAtom (v_pointer, ac_pointer,
 175                   AtomBinop (MemOp (ac_pointer, PtrAggr), AtomVar (ac_pointer_base, pointer_base),
 176                              AtomVar (ac_native_unsigned, v_index)), e))
 177       in (* end of build_step3 *)
 178
 179       (* STEP 4 - Check that the pointer is valid. *)
 180       let build_step4 e =
 181          if do_check op then
 182             (* Check that the pointer is valid *)
 183             make_exp loc (LetAtom (v_bit, ac_native_unsigned,
 184                      AtomBinop (AndOp ac_native_unsigned,
 185                                 AtomUnop (Int32OfPointerOp ptrty, AtomVar (ac_pointer, v_pointer)),
 186                                 AtomRawInt one_pointer),
 187             make_exp loc (Match (AtomVar (ac_native_unsigned, v_bit), ac_native_unsigned,
 188                    [RawIntSet one_pointer_set, seg_fault_pointer_expr;
 189                     RawIntSet zero_pointer_set, e]))))
 190          else
 191             (* No check required. *)
 192             e
 193       in (* end of build_step2 *)
 194
 195          (* Construct the index->pointer operation *)
 196          build_step1 (build_step2 (build_step3 (build_step4 e_cont)))
 197
 198
 199    (* function_of_index
 200       Express a hashed index->pointer operation, assuming the usual
 201       safety checks are required in the code.  This uses the function
 202       pointer table.  The op specifies whether this is a safe function
 203       conversion or unsafe, and also specifies whether checks should
 204       be done.  *)
 205    let function_of_index arity_tags pos loc funty op a_hashed_index e_cont =
 206       let pos = string_pos "function_of_index" pos in
 207       let v_index = new_symbol_string "index" in
 208       let v_index_test = new_symbol_string "index_test" in
 209       let v_pointer = new_symbol_string "pointer" in
 210       let ac_pointer = ACFunction funty in
 211       let v_arity_test = new_symbol_string "arity_test" in
 212       let v_arity_tag = new_symbol_string "arity_tag" in
 213       let ac_arity_tag = ac_native_unsigned in
 214       let a_cont = AtomVar (ac_pointer, v_pointer) in
 215       let e_cont = e_cont a_cont in
 216
 217       (* Compute the required arity tag for this function pointer. *)
 218       let arity_tag, _ = arity_lookup_by_funty arity_tags pos funty in
 219
 220       (* Construct the segfault expressions *)
 221       let seg_fault_index_expr =       (* Index was invalid *)
 222          make_exp loc (TailCall (ExternalCall, seg_fault_labels.(fun_index_fault),
 223                    [a_hashed_index; AtomVar (ac_native_unsigned, v_index)]))
 224       in
 225       let seg_fault_arity_tag_expr =   (* Arity tags not compatible *)
 226          make_exp loc (TailCall (ExternalCall, seg_fault_labels.(fun_arity_tag_fault),
 227                    [a_hashed_index; AtomVar (ac_native_unsigned, v_index);
 228                     AtomVar (ac_arity_tag, arity_tag); AtomVar (ac_arity_tag, v_arity_tag)]))
 229       in
 230
 231       (* STEP 1 - Compute index from hash *)
 232       let build_step1 e =
 233          if is_safe op then
 234             (* Safe pointers do not hash their indices, currently *)
 235             make_exp loc (LetAtom (v_index, ac_native_unsigned, a_hashed_index, e))
 236          else
 237             (* Unhash the unsafe function index *)
 238             make_exp loc (LetAtom (v_index, ac_native_unsigned,
 239                      AtomBinop (XorOp ac_native_unsigned, a_hashed_index, hash_fun_native_unsigned),
 240                      e))
 241       in (* end of build_step1 *)
 242
 243       (* STEP 2 - Check that the index is valid *)
 244       let build_step2 e =
 245          if do_check op then
 246             (* Check that it is a valid index *)
 247             make_exp loc (LetAtom (v_index_test, ac_native_bool,
 248                      AtomBinop (LtOp ac_native_unsigned,
 249                                 AtomVar (ac_native_unsigned, v_index),
 250                                 AtomVar (ac_native_unsigned, function_size)),
 251             make_exp loc (Match (AtomVar (ac_native_bool, v_index_test), ac_native_bool,
 252                    [RawIntSet native_false_set, seg_fault_index_expr;
 253                     RawIntSet native_true_set, e]))))
 254          else
 255             (* No check required. *)
 256             e
 257       in (* end of build_step2 *)
 258
 259       (* STEP 3 - Read from function table - pointers in the function
 260          table are always valid pointers, since they are in code seg. *)
 261       let build_step3 e =
 262          (* Read the pointer from the ptbl *)
 263          make_exp loc (LetAtom (v_pointer, ac_pointer,
 264                   AtomBinop (MemOp (ac_pointer, PtrAggr), AtomVar (ac_pointer_base, function_base),
 265                              AtomVar (ac_native_unsigned, v_index)),
 266                   e))
 267       in (* end of build_step3 *)
 268
 269       (* STEP 4 - Check that the arity tag is compatible. *)
 270       let build_step4 e =
 271          if Fir_state.safe_functions () then
 272             (* Get arity tag on the function header block. *)
 273             make_exp loc (LetAtom (v_arity_tag, ac_arity_tag,
 274                      AtomUnop (MemFunArityTagOp (funty, ac_arity_tag),
 275                                AtomVar (ac_pointer, v_pointer)),
 276             (* Check the arity tag *)
 277             make_exp loc (LetAtom (v_arity_test, ac_native_bool,
 278                      AtomBinop (EqOp ac_native_unsigned,
 279                                 AtomVar (ac_arity_tag, v_arity_tag),
 280                                 AtomVar (ac_arity_tag, arity_tag)),
 281             make_exp loc (Match (AtomVar (ac_arity_tag, v_arity_tag), ac_arity_tag,
 282                    [RawIntSet native_false_set, seg_fault_arity_tag_expr;
 283                     RawIntSet native_true_set, e]))))))
 284          else
 285             (* No arity check required *)
 286             e
 287       in (* end of build_step4 *)
 288
 289          (* Construct the final expression. *)
 290          build_step1 (build_step2 (build_step3 (build_step4 e_cont)))
 291
 292
 293    (* index_of_pointer
 294       Converts a pointer into an index.  The op specifies whether the
 295       conversion is using safe or unsafe representation.  *)
 296    let index_of_pointer arity_tags pos loc ptrty op a_pointer e_cont =
 297       let pos = string_pos "index_of_pointer" pos in
 298       let ac_index = ACRawInt (precision_native_int, unsigned_int) in
 299       let a_index = AtomUnop (MemIndexOp (ptrty, ac_index), a_pointer) in
 300          if is_safe op then
 301             e_cont a_index
 302          else
 303             e_cont (AtomBinop (XorOp ac_native_unsigned, a_index, hash_native_unsigned))
 304
 305
 306    (* index_of_function
 307       Converts a function pointer into an index.  The op specifies
 308       whether the conversion is using safe or unsafe representation. *)
 309    let index_of_function arity_tags pos loc funty op a_pointer e_cont =
 310       let pos = string_pos "index_of_function" pos in
 311       let ac_index = ACRawInt (precision_native_int, unsigned_int) in
 312       let a_index = AtomUnop (MemFunIndexOp (funty, ac_index), a_pointer) in
 313          if is_safe op then
 314             e_cont a_index
 315          else
 316             e_cont (AtomBinop (XorOp ac_native_unsigned, a_index, hash_fun_native_unsigned))
 317
 318
 319    (* mir_simplify_atom
 320       Simplifies the atom given.  *)
 321    let rec mir_simplify_atom arity_tags pos loc a e_cont =
 322       let pos = string_pos "mir_simplify_atom" pos in
 323          match a with
 324             AtomInt _
 325           | AtomRawInt _
 326           | AtomFloat _
 327           | AtomVar _
 328           | AtomFunVar _ ->
 329                e_cont a
 330           | AtomUnop (op, a) ->
 331                mir_simplify_unop_atom arity_tags pos loc op a e_cont
 332           | AtomBinop (op, a1, a2) ->
 333                mir_simplify_binop_atom arity_tags pos loc op a1 a2 e_cont
 334
 335
 336    (* mir_simplify_unop_atom
 337       Simplifies the unary operator given. *)
 338    and mir_simplify_unop_atom arity_tags pos loc op a e_cont =
 339       let pos = string_pos "mir_simplify_unop_atom" pos in
 340          mir_simplify_atom arity_tags pos loc a (fun a ->
 341             match op with
 342                SafePointerOfIndexOp ptrty ->
 343                   pointer_of_index arity_tags pos loc ptrty Safe a e_cont
 344              | UnsafePointerOfIndexOp ptrty ->
 345                   pointer_of_index arity_tags pos loc ptrty Unsafe a e_cont
 346              | SafeFunctionOfIndexOp funty ->
 347                   function_of_index arity_tags pos loc funty Safe a e_cont
 348              | UnsafeFunctionOfIndexOp funty ->
 349                   function_of_index arity_tags pos loc funty Unsafe a e_cont
 350              | SafeIndexOfPointerOp ptrty ->
 351                   index_of_pointer arity_tags pos loc ptrty Safe a e_cont
 352              | UnsafeIndexOfPointerOp ptrty ->
 353                   index_of_pointer arity_tags pos loc ptrty Unsafe a e_cont
 354              | SafeIndexOfFunctionOp funty ->
 355                   index_of_function arity_tags pos loc funty Safe a e_cont
 356              | UnsafeIndexOfFunctionOp funty ->
 357                   index_of_function arity_tags pos loc funty Unsafe a e_cont
 358              | _ ->
 359                   e_cont (AtomUnop (op, a)))
 360
 361
 362    (* mir_simplify_binop_atom
 363       Simplifies the binary operator given. *)
 364    and mir_simplify_binop_atom arity_tags pos loc op a1 a2 e_cont =
 365       let pos = string_pos "mir_simplify_binop_atom" pos in
 366          mir_simplify_atom arity_tags pos loc a1 (fun a1 ->
 367             mir_simplify_atom arity_tags pos loc a2 (fun a2 ->
 368                e_cont (AtomBinop (op, a1, a2))))
 369
 370
 371    (* mir_simplify_atom_list
 372       Simplifies a list of atoms, in order.  *)
 373    let mir_simplify_atom_list arity_tags pos loc atoms e_cont =
 374       let pos = string_pos "mir_simplify_atom_list" pos in
 375       let rec mir_simplify_atom_list arity_tags res = function
 376          a :: atoms ->
 377             mir_simplify_atom arity_tags pos loc a (fun a ->
 378                mir_simplify_atom_list arity_tags (a :: res) atoms)
 379        | [] ->
 380             e_cont (List.rev res)
 381       in
 382          mir_simplify_atom_list arity_tags [] atoms
 383
 384
 385    (* mir_simplify_atom_option
 386       Simplifies an optional atom.  *)
 387    let mir_simplify_atom_option arity_tags pos loc atom e_cont =
 388       let pos = string_pos "mir_simplify_atom_option" pos in
 389          match atom with
 390             Some atom ->
 391                mir_simplify_atom arity_tags pos loc atom (fun atom ->
 392                   e_cont (Some atom))
 393           | None ->
 394                e_cont None
 395
 396
 397    (***  Simplification of Expressions  ***)
 398
 399
 400    (* mir_simplify_expr
 401       Simplifies the expression given. *)
 402    let rec mir_simplify_expr arity_tags e =
 403       let pos = string_pos "mir_simplify_expr" (exp_pos e) in
 404       let loc = loc_of_exp e in
 405          match dest_exp_core e with
 406             LetAtom (v, ac, a, e) ->
 407                mir_simplify_atom arity_tags pos loc a (fun a ->
 408                   let e = mir_simplify_expr arity_tags e in
 409                      make_exp loc (LetAtom (v, ac, a, e)))
 410           | TailCall (op, f, atoms) ->
 411                mir_simplify_atom_list arity_tags pos loc atoms (fun atoms ->
 412                   make_exp loc (TailCall (op, f, atoms)))
 413           | IfThenElse (op, a1, a2, e1, e2) ->
 414                mir_simplify_atom arity_tags pos loc a1 (fun a1 ->
 415                   mir_simplify_atom arity_tags pos loc a2 (fun a2 ->
 416                      let e1 = mir_simplify_expr arity_tags e1 in
 417                      let e2 = mir_simplify_expr arity_tags e2 in
 418                         make_exp loc (IfThenElse (op, a1, a2, e1, e2))))
 419           | IfType (obj, names, name, v, e1, e2) ->
 420                mir_simplify_atom arity_tags pos loc obj (fun obj ->
 421                   mir_simplify_atom arity_tags pos loc names (fun names ->
 422                      mir_simplify_atom arity_tags pos loc name (fun name ->
 423                      let e1 = mir_simplify_expr arity_tags e1 in
 424                      let e2 = mir_simplify_expr arity_tags e2 in
 425                         make_exp loc (IfType (obj, names, name, v, e1, e2)))))
 426           | Match (a, ac, cases) ->
 427                mir_simplify_atom arity_tags pos loc a (fun a ->
 428                   let process_case (set, e) = (set, mir_simplify_expr arity_tags e) in
 429                   let cases = List.map process_case cases in
 430                      make_exp loc (Match (a, ac, cases)))
 431           | LetExternal (v, ac, f, atoms, e) ->
 432                mir_simplify_atom_list arity_tags pos loc atoms (fun atoms ->
 433                   let e = mir_simplify_expr arity_tags e in
 434                      make_exp loc (LetExternal (v, ac, f, atoms, e)))
 435           | LetExternalReserve ((label, vars, mem, ptr), v, ac, f, atoms, e) ->
 436                mir_simplify_atom_list arity_tags pos loc atoms (fun atoms ->
 437                mir_simplify_atom arity_tags pos loc mem (fun mem ->
 438                mir_simplify_atom arity_tags pos loc ptr (fun ptr ->
 439                   let e = mir_simplify_expr arity_tags e in
 440                      make_exp loc (LetExternalReserve ((label, vars, mem, ptr), v, ac, f, atoms, e)))))
 441           | Reserve ((label, vars, mem, ptr), e) ->
 442                mir_simplify_atom arity_tags pos loc mem (fun mem ->
 443                   mir_simplify_atom arity_tags pos loc ptr (fun ptr ->
 444                      let e = mir_simplify_expr arity_tags e in
 445                         make_exp loc (Reserve ((label, vars, mem, ptr), e))))
 446           | LetAlloc (v, AllocTuple atoms, e) ->
 447                mir_simplify_atom_list arity_tags pos loc atoms (fun atoms ->
 448                   let e = mir_simplify_expr arity_tags e in
 449                      make_exp loc (LetAlloc (v, AllocTuple atoms, e)))
 450           | LetAlloc (v, AllocArray atoms, e) ->
 451                mir_simplify_atom_list arity_tags pos loc atoms (fun atoms ->
 452                   let e = mir_simplify_expr arity_tags e in
 453                      make_exp loc (LetAlloc (v, AllocArray atoms, e)))
 454           | LetAlloc (v, AllocMArray (atoms, a), e) ->
 455                mir_simplify_atom arity_tags pos loc a (fun a ->
 456                   mir_simplify_atom_list arity_tags pos loc atoms (fun atoms ->
 457                      let e = mir_simplify_expr arity_tags e in
 458                         make_exp loc (LetAlloc (v, AllocMArray (atoms, a), e))))
 459           | LetAlloc (v, AllocUnion (tag, atoms), e) ->
 460                mir_simplify_atom_list arity_tags pos loc atoms (fun atoms ->
 461                   let e = mir_simplify_expr arity_tags e in
 462                      make_exp loc (LetAlloc (v, AllocUnion (tag, atoms), e)))
 463           | LetAlloc (v, AllocMalloc a, e) ->
 464                mir_simplify_atom arity_tags pos loc a (fun a ->
 465                   let e = mir_simplify_expr arity_tags e in
 466                      make_exp loc (LetAlloc (v, AllocMalloc a, e)))
 467           | SetMem (ac, op, a1, a2, a3, e) ->
 468                mir_simplify_atom arity_tags pos loc a1 (fun a1 ->
 469                   mir_simplify_atom arity_tags pos loc a2 (fun a2 ->
 470                      mir_simplify_atom arity_tags pos loc a3 (fun a3 ->
 471                         let e = mir_simplify_expr arity_tags e in
 472                            make_exp loc (SetMem (ac, op, a1, a2, a3, e)))))
 473           | SetGlobal (ac, v, a, e) ->
 474                mir_simplify_atom arity_tags pos loc a (fun a ->
 475                   let e = mir_simplify_expr arity_tags e in
 476                      make_exp loc (SetGlobal (ac, v, a, e)))
 477           | BoundsCheck (label, ptrty, ptr, start, stop, e) ->
 478                mir_simplify_bounds_check arity_tags pos loc label ptrty ptr start stop e
 479           | LowerBoundsCheck (label, ptrty, ptr, start, e) ->
 480                mir_simplify_lower_bounds_check arity_tags pos loc label ptrty ptr start e
 481           | UpperBoundsCheck (label, ptrty, ptr, stop, e) ->
 482                mir_simplify_upper_bounds_check arity_tags pos loc label ptrty ptr stop e
 483           | PointerIndexCheck (label, ptrty, v, ac, index, e) ->
 484                mir_simplify_atom arity_tags pos loc index (fun index ->
 485                   pointer_of_index arity_tags pos loc ptrty UnsafeCheck index (fun a ->
 486                      let e = mir_simplify_expr arity_tags e in
 487                         make_exp loc (LetAtom (v, ac, a, e))))
 488           | FunctionIndexCheck (label, funty, v, ac, index, e) ->
 489                mir_simplify_atom arity_tags pos loc index (fun index ->
 490                   function_of_index arity_tags pos loc funty UnsafeCheck index (fun a ->
 491                      let e = mir_simplify_expr arity_tags e in
 492                         make_exp loc (LetAtom (v, ac, a, e))))
 493           | Memcpy (op, a1, a2, a3, a4, a5, e) ->
 494                mir_simplify_atom arity_tags pos loc a1 (fun a1 ->
 495                   mir_simplify_atom arity_tags pos loc a2 (fun a2 ->
 496                      mir_simplify_atom arity_tags pos loc a3 (fun a3 ->
 497                         mir_simplify_atom arity_tags pos loc a4 (fun a4 ->
 498                            mir_simplify_atom arity_tags pos loc a5 (fun a5 ->
 499                               let e = mir_simplify_expr arity_tags e in
 500                                  make_exp loc (Memcpy (op, a1, a2, a3, a4, a5, e)))))))
 501           | Debug (info, e) ->
 502                let e = mir_simplify_expr arity_tags e in
 503                   make_exp loc (Debug (info, e))
 504           | PrintDebug (v1, v2, atoms, e) ->
 505                mir_simplify_atom_list arity_tags pos loc atoms (fun atoms ->
 506                   let e = mir_simplify_expr arity_tags e in
 507                      make_exp loc (PrintDebug (v1, v2, atoms, e)))
 508           | CommentFIR (fir, e) ->
 509                let e = mir_simplify_expr arity_tags e in
 510                   make_exp loc (CommentFIR (fir, e))
 511           | SysMigrate (label, dst_ptr, dst_off, f, env) ->
 512                mir_simplify_atom arity_tags pos loc dst_ptr (fun dst_ptr ->
 513                   mir_simplify_atom arity_tags pos loc dst_off (fun dst_off ->
 514                      mir_simplify_atom arity_tags pos loc env (fun env ->
 515                         make_exp loc (SysMigrate (label, dst_ptr, dst_off, f, env)))))
 516           | Atomic (f, i, env) ->
 517                mir_simplify_atom arity_tags pos loc i (fun i ->
 518                   mir_simplify_atom arity_tags pos loc env (fun env ->
 519                      make_exp loc (Atomic (f, i, env))))
 520           | AtomicRollback (level, i) ->
 521                mir_simplify_atom arity_tags pos loc level (fun level ->
 522                   mir_simplify_atom arity_tags pos loc i (fun i ->
 523                      make_exp loc (AtomicRollback (level, i))))
 524           | AtomicCommit (level, e) ->
 525                mir_simplify_atom arity_tags pos loc level (fun level ->
 526                   let e = mir_simplify_expr arity_tags e in
 527                      make_exp loc (AtomicCommit (level, e)))
 528           | CopyOnWrite ((label, vars, mem, ptr), copy_ptr, e) ->
 529                mir_simplify_atom arity_tags pos loc mem (fun mem ->
 530                   mir_simplify_atom arity_tags pos loc ptr (fun ptr ->
 531                      mir_simplify_atom arity_tags pos loc copy_ptr (fun copy_ptr ->
 532                         let e = mir_simplify_expr arity_tags e in
 533                            make_exp loc (CopyOnWrite ((label, vars, mem, ptr), copy_ptr, e)))))
 534           | SpecialCall _ ->
 535                raise (MirException (pos, InternalError "SpecialCall not allowed here"))
 536
 537
 538    (* mir_simplify_bounds_check_core
 539       Rewrites a *BoundsCheck expression into two bounds checks.
 540       both lower and upper bounds must be checked.  The <start> and
 541       <stop> arguments are atom option fields; a bounds check is
 542       done only if the corresponding argument matches Some (atom). *)
 543    and mir_simplify_bounds_check_core arity_tags pos loc label ptrty ptr start stop e =
 544       let pos = string_pos "mir_simplify_bounds_check_core" pos in
 545
 546       (* Setup a bunch of variables that we might need to use... *)
 547       let v_lower = new_symbol_string "lower_offset" in
 548       let v_upper = new_symbol_string "upper_offset" in
 549       let v_lower_test = new_symbol_string "lower_offset_test" in
 550       let v_upper_test = new_symbol_string "upper_offset_test" in
 551       let v_size = new_symbol_string "block_size" in
 552
 553       (* Seg fault expression for when something goes wrong. *)
 554       let seg_fault_expr =
 555          let e =
 556             match start, stop with
 557                Some start, Some stop ->
 558                   TailCall (ExternalCall, seg_fault_labels.(bounds_fault),
 559                             [ptr; start; stop; AtomVar (ac_native_unsigned, v_size)])
 560              | Some start, None ->
 561                   TailCall (ExternalCall, seg_fault_labels.(lower_bounds_fault),
 562                             [ptr; start; AtomVar (ac_native_unsigned, v_size)])
 563              | None, Some stop ->
 564                   TailCall (ExternalCall, seg_fault_labels.(upper_bounds_fault),
 565                             [ptr; stop; AtomVar (ac_native_unsigned, v_size)])
 566              | None, None ->
 567                   raise (MirException (pos, InternalError "Bounds check requested with no bounds specified!"))
 568          in
 569             make_exp loc e
 570       in
 571
 572       (* Simplify the atoms and final expression, first *)
 573       mir_simplify_atom arity_tags pos loc ptr (fun ptr ->
 574          mir_simplify_atom_option arity_tags pos loc start (fun start ->
 575             mir_simplify_atom_option arity_tags pos loc stop (fun stop ->
 576                let e = mir_simplify_expr arity_tags e in
 577
 578                (* Okay, now we can start rewriting the bounds check.  Note
 579                   that we need to check both the lower and UPPER bounds; if
 580                   we only check the upper bound, then it's possible to flow
 581                   into the header (hint: set size = 8, offset = -4).  NOTE:
 582                   In the case where lower and upper bounds are both constants,
 583                   one of these steps will be redundant.  We do UPPER bound
 584                   FIRST because that check is most exclusive, therefore we
 585                   can more easily catch the redundant conditional if this
 586                   conditional appears first! *)
 587                (* STEP 1 - Load values into temporary variables *)
 588                let build_step1 e =
 589                   let get_lower e =
 590                      match start with
 591                         Some start ->
 592                            make_exp loc (LetAtom (v_lower, ac_native_unsigned, start, e))
 593                       | None ->
 594                            e
 595                   in
 596                   let get_upper e =
 597                      match stop with
 598                         Some stop ->
 599                            make_exp loc (LetAtom (v_upper, ac_native_unsigned, stop, e))
 600                       | None ->
 601                            e
 602                   in
 603                   let size_ac = ACRawInt (precision_native_int, unsigned_int) in
 604                      make_exp loc (LetAtom (v_size, ac_native_unsigned,
 605                               AtomUnop (MemSizeOp (ptrty, size_ac), ptr),
 606                               get_lower (get_upper e)))
 607                in (* end of step1 *)
 608
 609                (* STEP 2 - check against the upper bound *)
 610                let build_step2 e =
 611                   match stop with
 612                      Some stop ->
 613                         (* NOTE: values are unsigned, therefore this value must
 614                            be less than OR EQUAL TO the size of the memory block.
 615                            If we run over the beginning of the block, then we
 616                            get a large (unsigned) value, so this check will work. *)
 617                         make_exp loc (LetAtom (v_upper_test, ac_native_bool,
 618                                  AtomBinop (LeOp ac_native_unsigned,
 619                                             AtomVar (ac_native_unsigned, v_upper),
 620                                             AtomVar (ac_native_unsigned, v_size)),
 621                         make_exp loc (Match (AtomVar (ac_native_bool, v_upper_test), ac_native_bool,
 622                                [RawIntSet native_false_set, seg_fault_expr;
 623                                 RawIntSet native_true_set, e]))))
 624                    | None ->
 625                         (* No upper bound to check *)
 626                         e
 627                in (* end of step2 *)
 628
 629                (* STEP 3 - check against the lower bound *)
 630                let build_step3 e =
 631                   match start with
 632                      Some start ->
 633                         (* NOTE: values are unsigned, therefore this value must be
 634                            strictly LESS THAN the size of the memory block. *)
 635                         make_exp loc (LetAtom (v_lower_test, ac_native_bool,
 636                                  AtomBinop (LtOp ac_native_unsigned,
 637                                             AtomVar (ac_native_unsigned, v_lower),
 638                                             AtomVar (ac_native_unsigned, v_size)),
 639                         make_exp loc (Match (AtomVar (ac_native_bool, v_lower_test), ac_native_bool,
 640                                [RawIntSet native_false_set, seg_fault_expr;
 641                                 RawIntSet native_true_set, e]))))
 642                    | None ->
 643                         (* No lower bound to check *)
 644                         e
 645                in (* end of step3 *)
 646
 647                   (* Construct the bounds check *)
 648                   build_step1 (build_step2 (build_step3 e)))))
 649
 650
 651    (* mir_simplify_bounds_check
 652       Checks both lower and upper bounds. *)
 653    and mir_simplify_bounds_check arity_tags pos loc label ptrty ptr start stop e =
 654       let pos = string_pos "mir_simplify_bounds_check" pos in
 655          mir_simplify_bounds_check_core arity_tags pos loc label ptrty ptr (Some start) (Some stop) e
 656
 657
 658    (* mir_simplify_lower_bounds_check
 659       Checks the lower bounds only. *)
 660    and mir_simplify_lower_bounds_check arity_tags pos loc label ptrty ptr start e =
 661       let pos = string_pos "mir_simplify_bounds_check" pos in
 662          mir_simplify_bounds_check_core arity_tags pos loc label ptrty ptr (Some start) None e
 663
 664
 665    (* mir_simplify_upper_bounds_check
 666       Checks the upper bounds only. *)
 667    and mir_simplify_upper_bounds_check arity_tags pos loc label ptrty ptr stop e =
 668       let pos = string_pos "mir_simplify_bounds_check" pos in
 669          mir_simplify_bounds_check_core arity_tags pos loc label ptrty ptr None (Some stop) e
 670
 671
 672    (***  Simplification of Programs  ***)
 673
 674
 675    (* simplify_prog
 676       Simplifies an entire program.  Note: this function currently only
 677       simplifies function bodies; it does not simplify atoms that appear
 678       in globals, or other locations.  *)
 679    let simplify_prog prog =
 680       let { prog_funs         = funs;
 681             prog_arity_tags   = arity_tags;
 682           } = prog
 683       in
 684       let simplify_fun (funs, arity_tags) f (line, args, e) =
 685          let e = mir_simplify_expr arity_tags e in
 686          let funs = SymbolTable.add funs f (line, args, e) in
 687             funs, arity_tags
 688       in
 689       let funs, arity_tags = SymbolTable.fold simplify_fun (SymbolTable.empty, arity_tags) funs in
 690          if debug Mir_state.debug_print_mir then
 691             Mir_print.debug_prog "After simplify" prog;
 692          { prog with
 693                prog_funs         = funs;
 694                prog_arity_tags   = arity_tags;
 695          }
 696
 697    let simplify_prog = Fir_state.profile "Mir_simplify.simplify_prog" simplify_prog
 698
 699    let simplify_expr = Fir_state.profile "Mir_simplify.simplify_expr" mir_simplify_expr
 700
 701
 702 end (* struct *)