summary refs log tree commit diff
path: root/proto/bak.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proto/bak.ml')
-rw-r--r--proto/bak.ml132
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