summary refs log tree commit diff
path: root/proto/bak.ml
blob: cd1aff284c97f618290faa1259eada63f6270b21 (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
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