diff options
Diffstat (limited to 'proto/bak.ml')
-rw-r--r-- | proto/bak.ml | 132 |
1 files changed, 132 insertions, 0 deletions
diff --git a/proto/bak.ml b/proto/bak.ml new file mode 100644 index 0000000..cd1aff2 --- /dev/null +++ b/proto/bak.ml @@ -0,0 +1,132 @@ +type id = int +type ty = + | TInt of bool * int + | TArr of int * ty + | TPtr of ty + | TVoid +type con = CInt of int +type cnd = Ge | Le | Gt | Lt | Ne | Eq +type ins = + | IAlloc of ty + | IMem of id + | ISto of id * id + | IAdd of id * id + | ISub of id * id + | ICon of ty * con + | IBr of id * cnd * id * id + | IJmp of id + | IPhi of ty * id * id + +let isint = function TInt _ -> true | _ -> false +let isbranch = function IBr _ | IJmp _ -> true | _ -> false + +exception Type of string +let tychk blk = + let typs = Array.make (Array.length blk) TVoid in + let blks = ref [] in + let jmp src dst = + let rec f = function + | (blk, srcs) :: tl when blk = dst -> + (blk, src :: srcs) :: tl + | b :: tl when fst b < dst -> b :: f tl + | l -> + let srcs = + if dst = 0 then [src] else + if isbranch blk.(dst-1) + then [src] else [dst-1; src] in + (dst, srcs) :: l in + blks := f !blks in + let f i = (* do easy type checks *) + let chn n = + if n >= i || n < 0 then + raise (Type "broken data dependency") in + function + | IPhi (ty, _, _) -> + if ty = TVoid then + raise (Type "invalid void phi"); + typs.(i) <- ty + | ICon (ty, _) -> typs.(i) <- ty + | IAlloc ty -> + if ty = TVoid then + raise (Type "invalid void alloc"); + typs.(i) <- TPtr ty + | IMem n -> + chn n; + (match typs.(n) with + | TPtr ty -> typs.(i) <- ty + | _ -> raise (Type "invalid dereference") + ) + | ISto (a, b) -> + chn a; chn b; + if typs.(a) <> TPtr typs.(b) then + raise (Type "invalid store") + | IAdd (a, b) -> + chn a; chn b; + if not (isint typs.(b)) then + raise (Type "second add operand not integral"); + (match typs.(a) with + | (TPtr _) as t -> typs.(i) <- t + | (TInt _) as t -> + if t <> typs.(b) then + raise (Type "invalid heterogeneous addition"); + typs.(i) <- t + | _ -> raise (Type "invalid type for addition") + ) + | ISub (a, b) -> + chn a; chn b; + (match typs.(a), typs.(b) with + | (TPtr _ as ta), (TPtr _ as tb) -> + if ta <> tb then + raise (Type "substracted pointers have different types"); + typs.(i) <- TInt (true, 64) + | (TInt _ as ta), (TInt _ as tb) -> + if ta <> tb then + raise (Type "invalid heterogeneous substraction"); + typs.(i) <- ta + | _ -> raise (Type "invalid type for substraction") + ) + | IBr (_, _, _, dst) -> jmp i dst; jmp i (i+1) + | IJmp dst -> jmp i dst in + Array.iteri f blk; + let f = function (* check types at phi nodes *) + | IPhi (_, a, b) -> + if typs.(a) <> typs.(b) then + raise (Type "ill-typed phi node") + | _ -> () in + Array.iter f blk; + let bbase i = + let rec f base = function + | [] -> base + | (b, _) :: _ when b > i -> base + | (b, _) :: tl -> f b tl in + f 0 !blks in + let f i = function (* check validity of ssa *) + | IPhi (_, a, b) -> + let callers = + List.map bbase (List.assoc (bbase i) !blks) in + let ba = bbase a and bb = bbase b in + if ba = bb + || not (List.mem ba callers) + || not (List.mem bb callers) + then + raise (Type "invalid phi node"); + | IAdd (a, b) | ISub (a, b) | ISto (a, b) | IBr (a, _, b, _) -> + let bi = bbase i in + if bbase a <> bi || bbase b <> bi then + raise (Type "operands of non-phy not in current block") + | IMem a -> + if bbase a <> bbase i then + raise (Type "operands of non-phy not in current block") + | IJmp _ | ICon _ | IAlloc _ -> () in + Array.iteri f blk + + (* tests *) +let _ = + let int = TInt (true, 32) in + let p0 = [| + (* 0 *) ICon (int, CInt 1); + (* 1 *) ICon (int, CInt 42); + (* 2 *) IPhi (int, 0, 2); + (* 3 *) IAdd (1, 2); + (* 4 *) IJmp 1 + |] in tychk p0 |