fir/util/fir_assert.ml

   1 (*
   2  * Add assertions around all array and tuple accesses.
   3  *
   4  * ----------------------------------------------------------------
   5  *
   6  * @begin[license]
   7  * Copyright (C) 2002 Jason Hickey, Caltech
   8  *
   9  * This program is free software; you can redistribute it and/or
  10  * modify it under the terms of the GNU General Public License
  11  * as published by the Free Software Foundation; either version 2
  12  * of the License, or (at your option) any later version.
  13  *
  14  * This program is distributed in the hope that it will be useful,
  15  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  16  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  17  * GNU General Public License for more details.
  18  *
  19  * You should have received a copy of the GNU General Public License
  20  * along with this program; if not, write to the Free Software
  21  * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
  22  *
  23  * Author: Jason Hickey
  24  * @email{jyh@cs.caltech.edu}
  25  * @end[license]
  26  *)
  27 open Symbol
  28
  29 open Fir
  30 open Fir_ds
  31 open Fir_exn
  32 open Fir_pos
  33 open Fir_env
  34 open Fir_type
  35 open Fir_frame
  36 open Fir_standardize
  37
  38 open Sizeof_const
  39 open Sizeof_type
  40
  41 module Pos = MakePos (struct let name = "Fir_assert" end)
  42 open Pos
  43
  44 (*
  45  * Type for RawData subscripts.
  46  *)
  47 let pre_subscript = precision_subscript
  48 let ty_subscript = TyRawInt (pre_subscript, signed_subscript)
  49 let plus_subscript = PlusRawIntOp (pre_subscript, signed_subscript)
  50 let atom_word = AtomRawInt (Rawint.of_int pre_subscript signed_subscript sizeof_pointer)
  51
  52 let plus_pointer_op op = PlusPointerOp (op, pre_subscript, signed_subscript)
  53 let sub_script = RawIntIndex (pre_subscript, signed_subscript)
  54
  55 let subscript_of_int i =
  56    AtomRawInt (Rawint.of_int pre_subscript signed_subscript i)
  57
  58 let zero32 = Rawint.of_int pre_subscript signed_subscript 0
  59 let zero_subscript = subscript_of_int 0
  60 let one_subscript = subscript_of_int 1
  61
  62 (*
  63  * Adjust subscript operation to use a int32 index.
  64  *)
  65 let assert_rawint_index genv pos loc op a cont =
  66    let pos = string_pos "assert_rawint_index" pos in
  67       match op.sub_script with
  68          IntIndex ->
  69             let v_index = new_symbol_string "rawint_index" in
  70             let genv = genv_add_var genv v_index ty_subscript in
  71             let op = { op with sub_script = RawIntIndex (pre_subscript, signed_subscript) } in
  72                make_exp loc (LetAtom (v_index, ty_subscript, AtomUnop (RawIntOfIntOp (pre_subscript, signed_subscript), a),
  73                                       cont genv op (AtomVar v_index)))
  74        | RawIntIndex (pre, signed) ->
  75             let v_index = new_symbol_string "rawint_index" in
  76             let genv = genv_add_var genv v_index ty_subscript in
  77             let op = { op with sub_script = RawIntIndex (pre_subscript, signed_subscript) } in
  78                make_exp loc (LetAtom (v_index, ty_subscript, AtomUnop (RawIntOfRawIntOp (pre_subscript, signed_subscript, pre, signed), a),
  79                                       cont genv op (AtomVar v_index)))
  80
  81 (*
  82  * Adjust subscript operation to use a byte index.
  83  *)
  84 let assert_byte_index genv pos loc sub_index a cont =
  85    let pos = string_pos "assert_byte_index" pos in
  86       match sub_index with
  87          WordIndex ->
  88             let v_index = new_symbol_string "byte_index" in
  89             let genv = genv_add_var genv v_index ty_subscript in
  90                make_exp loc (LetAtom (v_index, ty_subscript, AtomBinop (MulRawIntOp (pre_subscript, signed_subscript), a, atom_word),
  91                                       cont genv (AtomVar v_index)))
  92        | ByteIndex ->
  93             cont genv a
  94
  95 let assert_byte_index_op genv pos loc op a cont =
  96    let pos = string_pos "assert_byte_index_op" pos in
  97       assert_byte_index genv pos loc op.sub_index a (fun genv a ->
  98             cont genv { op with sub_index = ByteIndex } a)
  99
 100 (*
 101  * Convert the length.
 102  *)
 103 let assert_length genv pos loc op a cont =
 104    let pos = string_pos "assert_length" pos in
 105       match a with
 106          AtomVar _ ->
 107             assert_rawint_index genv pos loc op a (fun genv op a ->
 108                   assert_byte_index_op genv pos loc op a cont)
 109        | AtomInt i
 110        | AtomEnum (_, i) ->
 111             let i = Rawint.of_int pre_subscript signed_subscript (i * sizeof_pointer) in
 112             let op = { op with sub_index = ByteIndex; sub_script = sub_script } in
 113                cont genv op (AtomRawInt i)
 114        | AtomRawInt i ->
 115             cont genv op (AtomRawInt (Rawint.of_rawint pre_subscript signed_subscript i))
 116        | AtomLabel _
 117        | AtomSizeof _ ->
 118             cont genv op a
 119        | AtomNil _
 120        | AtomFloat _
 121        | AtomConst _
 122        | AtomTyApply _
 123        | AtomTyPack _
 124        | AtomTyUnpack _
 125        | AtomFun _ ->
 126             raise (FirException (pos, StringAtomError ("not an integer", a)))
 127        | AtomUnop _
 128        | AtomBinop _ ->
 129             raise (FirException (pos, StringAtomError ("not implemented", a)))
 130
 131 (*
 132  * Adjust subscript to use TyPointer.
 133  *)
 134 let assert_pointer_index genv pos loc op v a cont =
 135    let pos = string_pos "assert_pointer_index" pos in
 136    let s = "ptr" in
 137    let v1 = new_symbol_string (s ^ "_base") in
 138    let v2 = new_symbol_string (s ^ "_ptr") in
 139    let block_op = op.sub_block in
 140    let ty = TyPointer block_op in
 141    let e = cont genv op a (AtomVar v2) zero_subscript in
 142    let e = make_exp loc (LetAtom (v2, ty, AtomBinop (plus_pointer_op block_op, AtomVar v1, a), e)) in
 143       make_exp loc (LetAtom (v1, ty, AtomUnop (PointerOfBlockOp block_op, v), e))
 144
 145 (*
 146  * Adjust the subscript operation.
 147  *)
 148 let assert_subscript genv pos loc op v a cont =
 149    let pos = string_pos "assert_subscript" pos in
 150       assert_length genv pos loc op a (fun genv op a ->
 151             match a with
 152                AtomVar _ ->
 153                   assert_pointer_index genv pos loc op v a cont
 154              | AtomRawInt _
 155              | AtomLabel _ ->
 156                   cont genv op a v a
 157              | _ ->
 158                   raise (FirException (pos, StringAtomError ("not an integer", a))))
 159
 160 (*
 161  * Expressions.
 162  *)
 163 let rec assert_exp fenv genv e =
 164    let pos = string_pos "assert_exp" (exp_pos e) in
 165    let loc = loc_of_exp e in
 166       match dest_exp_core e with
 167          LetAtom (v, ty, a, e) ->
 168             make_exp loc (LetAtom (v, ty, a, assert_exp fenv genv e))
 169        | LetExt (v, ty1, s, b, ty2, ty_args, args, e) ->
 170             make_exp loc (LetExt (v, ty1, s, b, ty2, ty_args, args, assert_exp fenv genv e))
 171        | TailCall _
 172        | SpecialCall _ ->
 173             e
 174        | Match (a, cases) ->
 175             make_exp loc (Match (a, List.map (fun (l, s, e) -> l, s, assert_exp fenv genv e) cases))
 176        | MatchDTuple (a, cases) ->
 177             make_exp loc (MatchDTuple (a, List.map (fun (l, a_opt, e) -> l, a_opt, assert_exp fenv genv e) cases))
 178        | TypeCase (a1, a2, v1, v2, e1, e2) ->
 179             make_exp loc (TypeCase (a1, a2, v1, v2, assert_exp fenv genv e1, assert_exp fenv genv e2))
 180        | LetAlloc (v, op, e) ->
 181             assert_alloc_exp fenv genv pos loc v op e
 182        | LetSubscript (op, v1, ty, v2, a, e) ->
 183             assert_subscript_exp fenv genv pos loc op v1 ty v2 a e
 184        | SetSubscript (op, label, v, a1, ty, a2, e) ->
 185             assert_set_subscript_exp fenv genv pos loc op label v a1 ty a2 e
 186        | Memcpy (op, label, v1, a1, v2, a2, a3, e) ->
 187             assert_memcpy_exp fenv genv pos loc op label v1 a1 v2 a2 a3 e
 188        | LetGlobal (op, v, ty, l, e) ->
 189             make_exp loc (LetGlobal (op, v, ty, l, assert_exp fenv genv e))
 190        | SetGlobal (op, label, v, ty, a, e) ->
 191             make_exp loc (SetGlobal (op, label, v, ty, a, assert_exp fenv genv e))
 192        | Assert (_, _, e) ->
 193             (* Ignore existing assertions *)
 194             assert_exp fenv genv e
 195        | Call (label, f, args, e) ->
 196             make_exp loc (Call (label, f, args, assert_exp fenv genv e))
 197        | Debug (info, e) ->
 198             make_exp loc (Debug (info, assert_exp fenv genv e))
 199
 200 (*
 201  * Add an allocation.
 202  * Make sure to reserve space.
 203  *)
 204 and assert_alloc_exp fenv genv pos loc v op e =
 205    let pos = string_pos "assert_alloc_exp" pos in
 206    let alloc size op =
 207       let label = new_symbol_string "reserve" in
 208       let e = make_exp loc (LetAlloc (v, op, assert_exp fenv genv e)) in
 209          make_exp loc (Assert (label, Reserve (size, one_subscript), e))
 210    in
 211       match op with
 212          AllocTuple (_, _, _, args)
 213        | AllocUnion (_, _, _, _, args)
 214        | AllocArray (_, args)
 215        | AllocDTuple (_, _, _, args) ->
 216             let size = List.length args * sizeof_pointer in
 217                alloc (subscript_of_int size) op
 218        | AllocVArray (ty, sub_index, size, init) ->
 219             assert_byte_index genv pos loc sub_index size (fun genv size ->
 220                   alloc size (AllocVArray (ty, ByteIndex, size, init)))
 221        | AllocMalloc (_, size) ->
 222             alloc size op
 223        | AllocFrame (v, _) ->
 224             alloc (AtomSizeof ([v], zero32)) op
 225
 226 (*
 227  * Add an assertion before a subscript.
 228  *    1. Check the array bounds
 229  *    2. Check the element type for TyRawData
 230  *)
 231 and assert_subscript_exp fenv genv pos loc op v1 ty v2 a2 e =
 232    let pos = string_pos "assert_subscript_exp" pos in
 233       assert_subscript genv pos loc op v2 a2 (fun genv op a2 v2' a2' ->
 234             (* Add a type check *)
 235             let e = make_exp loc (LetSubscript (op, v1, ty, v2', a2', assert_exp fenv genv e)) in
 236             let e =
 237                match op.sub_value with
 238                   PolySub
 239                 | BlockPointerSub
 240                 | RawPointerSub
 241                 | FunctionSub ->
 242                      let label = new_symbol_string "check_element" in
 243                         make_exp loc (Assert (label, ElementCheck (ty, op, v2, a2), e))
 244                 | _ ->
 245                      e
 246             in
 247
 248             (* Add a bounds check *)
 249             let size = subscript_of_int (sizeof_type genv pos 0 ty) in
 250             let v_limit = new_symbol_string "limit" in
 251             let label = new_symbol_string "check_bounds" in
 252             let e = make_exp loc (Assert (label, BoundsCheck (op, v2, a2, AtomVar v_limit), e)) in
 253                make_exp loc (LetAtom (v_limit, ty_subscript, AtomBinop (plus_subscript, a2, size), e)))
 254
 255 (*
 256  * Add an bounds-check assertion before an assignment.
 257  *)
 258 and assert_set_subscript_exp fenv genv pos loc op label v1 a1 ty a2 e =
 259    let pos = string_pos "assert_set_subscript_exp" pos in
 260       assert_subscript genv pos loc op v1 a1 (fun genv op a1 v1' a1' ->
 261             (* Add a bounds check *)
 262             let size = subscript_of_int (sizeof_type genv pos 0 ty) in
 263             let v_limit = new_symbol_string "limit" in
 264             let label' = new_symbol_string "check_bounds" in
 265             let e = make_exp loc (SetSubscript (op, label, v1', a1', ty, a2, assert_exp fenv genv e)) in
 266             let e = make_exp loc (Assert (label', BoundsCheck (op, v1, a1, AtomVar v_limit), e)) in
 267                make_exp loc (LetAtom (v_limit, ty_subscript, AtomBinop (plus_subscript, a1, size), e)))
 268
 269 (*
 270  * Add bounds-check assertions before a memcpy.
 271  *)
 272 and assert_memcpy_exp fenv genv pos loc op label v1 a1 v2 a2 a3 e =
 273    let pos = string_pos "assert_memcpy_exp" pos in
 274       assert_subscript genv pos loc op v1 a1 (fun genv _ a1 v1' a1' ->
 275       assert_subscript genv pos loc op v2 a2 (fun genv _ a2 v2' a2' ->
 276       assert_length genv pos loc op a3 (fun genv op a3 ->
 277             (* Add bounds checks *)
 278             let v_to_limit = new_symbol_string "to_limit" in
 279             let v_from_limit = new_symbol_string "from_limit" in
 280             let label_to = new_symbol_string "check_bounds_to" in
 281             let label_from = new_symbol_string "check_bounds_from" in
 282             let e = make_exp loc (Memcpy (op, label, v1', a1', v2', a2', a3, assert_exp fenv genv e)) in
 283             let e = make_exp loc (Assert (label_from, BoundsCheck (op, v2, a2, AtomVar v_from_limit), e)) in
 284             let e = make_exp loc (LetAtom  (v_from_limit, ty_subscript, AtomBinop (plus_subscript, a2, a3), e)) in
 285             let e = make_exp loc (Assert (label_to, BoundsCheck (op, v1, a1, AtomVar v_to_limit), e)) in
 286                make_exp loc (LetAtom  (v_to_limit, ty_subscript, AtomBinop (plus_subscript, a1, a3), e)))))
 287
 288 (*
 289  * Add assertions to the program.
 290  *)
 291 let assert_prog prog =
 292    let { prog_funs = funs;
 293          prog_types = tenv;
 294          prog_globals = globals;
 295          prog_names = names
 296        } = prog
 297    in
 298    let genv = prog_genv prog in
 299    let fenv = frame_prog prog in
 300
 301    (* Add assertions to all the function bodies *)
 302    let funs =
 303       SymbolTable.map (fun (info, ty, ty_vars, vars, e) ->
 304             info, ty, ty_vars, vars, assert_exp fenv genv e) funs
 305    in
 306
 307    (* Put the functions pack *)
 308    let prog = { prog with prog_funs = funs } in
 309       standardize_prog prog
 310
 311 (*!
 312  * @docoff
 313  *
 314  * -*-
 315  * Local Variables:
 316  * Caml-master: "compile"
 317  * End:
 318  * -*-
 319  *)