Source file typing.ml
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
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
open Utils
open Wsize
open Prog
exception TyError of L.i_loc * string
let error loc fmt =
let buf = Buffer.create 127 in
let bfmt = Format.formatter_of_buffer buf in
Format.kfprintf
(fun _ ->
Format.pp_print_flush bfmt ();
raise (TyError (loc, Buffer.contents buf)))
bfmt fmt
let ty_var (x:var_i) =
let ty = (L.unloc x).v_ty in
begin match ty with
| Arr(_, n) ->
if (n < 1) then
error (L.i_loc0 (L.unloc x).v_dloc)
"the variable %a has type %a, its array size should be positive"
(Printer.pp_var ~debug:false) (L.unloc x) PrintCommon.pp_ty ty
| _ -> ()
end;
ty
let ty_gvar (x:int ggvar) = ty_var x.gv
let check_array loc e te =
match te with
| Arr _ -> ()
| _ ->
error loc
"the expression %a has type %a while an array is expected"
(Printer.pp_expr ~debug:false) e PrintCommon.pp_ty te
let subtype t1 t2 =
match t1, t2 with
| Bty (U ws1), Bty (U ws2) -> wsize_le ws1 ws2
| Bty bty1, Bty bty2 -> bty1 = bty2
| Arr(ws1,len1), Arr(ws2,len2) -> arr_size ws1 len1 == arr_size ws2 len2
| _, _ -> false
let check_type loc e te ty =
if not (subtype ty te) then
error loc "the expression %a has type %a while %a is expected"
(Printer.pp_expr ~debug:false) e
PrintCommon.pp_ty te PrintCommon.pp_ty ty
let check_int loc e te = check_type loc e te tint
let check_ptr pd loc e te = check_type loc e te (tu pd)
let check_length loc len =
if len <= 0 then
error loc "the length should be strictly positive"
let type_of_op1 op =
let tin,tout = E.type_of_op1 op in
Conv.ty_of_cty tin, Conv.ty_of_cty tout
let type_of_op2 op =
let (tin1,tin2),tout = E.type_of_op2 op in
(Conv.ty_of_cty tin1, Conv.ty_of_cty tin2), Conv.ty_of_cty tout
let type_of_opN op =
let tins, tout = E.type_of_opN op in
List.map Conv.ty_of_cty tins, Conv.ty_of_cty tout
let type_of_sopn loc pd asmOp op =
let valid = Sopn.i_valid (Sopn.get_instr_desc pd asmOp op) in
if not valid then error loc "invalid operator, please report";
List.map Conv.ty_of_cty (Sopn.sopn_tin pd asmOp op),
List.map Conv.ty_of_cty (Sopn.sopn_tout pd asmOp op)
let rec ty_expr pd loc (e:expr) =
match e with
| Pconst _ -> tint
| Pbool _ -> tbool
| Parr_init len -> Arr (U8, len)
| Pvar x -> ty_gvar x
| Pget(_al, _aa,ws,x,e) ->
ty_get_set pd loc ws x e
| Psub(_aa, ws, len, x, e) ->
ty_get_set_sub pd loc ws len x e
| Pload(_, ws,e) ->
ty_load_store pd loc ws e
| Papp1(op,e) ->
let tin, tout = type_of_op1 op in
check_expr pd loc e tin;
tout
| Papp2(op,e1,e2) ->
let (tin1, tin2), tout = type_of_op2 op in
check_expr pd loc e1 tin1;
check_expr pd loc e2 tin2;
tout
| PappN(op,es) ->
let tins, tout = type_of_opN op in
check_exprs pd loc es tins;
tout
| Pif(ty,b,e1,e2) ->
check_expr pd loc b tbool;
check_expr pd loc e1 ty;
check_expr pd loc e2 ty;
ty
and check_expr pd loc e ty =
let te = ty_expr pd loc e in
check_type loc e te ty
and check_exprs pd loc es tys =
let len = List.length tys in
if List.length es <> len then
error loc "invalid number of expressions %i expected" len;
List.iter2 (check_expr pd loc) es tys
and ty_load_store pd loc ws e =
let te = ty_expr pd loc e in
check_ptr pd loc e te;
tu ws
and ty_get_set pd loc ws x e =
let tx = ty_gvar x in
let te = ty_expr pd loc e in
check_array loc (Pvar x) tx;
check_int loc e te;
tu ws
and ty_get_set_sub pd loc ws len x e =
let tx = ty_gvar x in
let te = ty_expr pd loc e in
check_array loc (Pvar x) tx;
check_int loc e te;
check_length loc len;
Arr(ws, len)
let ty_lval pd loc = function
| Lnone (_, ty) -> ty
| Lvar x -> ty_var x
| Lmem(_, ws,_,e) -> ty_load_store pd loc ws e
| Laset(_al,_aa,ws,x,e) -> ty_get_set pd loc ws (gkvar x) e
| Lasub(_aa,ws,len,x,e) -> ty_get_set_sub pd loc ws len (gkvar x) e
let check_lval pd loc x ty =
let tx = ty_lval pd loc x in
if not (subtype tx ty) then
error loc "the left value %a has type %a while %a is expected"
(Printer.pp_lval ~debug:false) x
PrintCommon.pp_ty tx PrintCommon.pp_ty ty
let check_lvals pd loc xs tys =
let len = List.length tys in
if List.length xs <> len then
error loc "invalid number of left values %i expected" len;
List.iter2 (check_lval pd loc) xs tys
let getfun env fn =
try Hf.find env fn with Not_found -> assert false
let rec check_instr pd asmOp env i =
let loc = i.i_loc in
match i.i_desc with
| Cassgn(x,_,ty,e) ->
check_expr pd loc e ty;
check_lval pd loc x ty
| Copn(xs,_,op,es) ->
let tins, tout = type_of_sopn loc pd asmOp op in
check_exprs pd loc es tins;
check_lvals pd loc xs tout
| Csyscall(xs, o, es) ->
let s = Syscall.syscall_sig_u o in
let tins = List.map Conv.ty_of_cty s.scs_tin in
let tout = List.map Conv.ty_of_cty s.scs_tout in
check_exprs pd loc es tins;
check_lvals pd loc xs tout
| Cif(e,c1,c2) ->
check_expr pd loc e tbool;
check_cmd pd asmOp env c1;
check_cmd pd asmOp env c2
| Cfor(i,(_,e1,e2),c) ->
check_expr pd loc (Pvar (gkvar i)) tint;
check_expr pd loc e1 tint;
check_expr pd loc e2 tint;
check_cmd pd asmOp env c
| Cwhile(_, c1, e, _, c2) ->
check_expr pd loc e tbool;
check_cmd pd asmOp env c1;
check_cmd pd asmOp env c2
| Ccall(xs,fn,es) ->
let fd = getfun env fn in
check_exprs pd loc es fd.f_tyin;
check_lvals pd loc xs fd.f_tyout
and check_cmd pd asmOp env c =
List.iter (check_instr pd asmOp env) c
let check_fun pd asmOp env fd =
let args = List.map (fun x -> Pvar (gkvar (L.mk_loc x.v_dloc x))) fd.f_args in
let res = List.map (fun x -> Pvar (gkvar x)) fd.f_ret in
let i_loc = L.i_loc0 fd.f_loc in
check_exprs pd i_loc args fd.f_tyin;
check_exprs pd i_loc res fd.f_tyout;
check_cmd pd asmOp env fd.f_body;
Hf.add env fd.f_name fd
let check_prog pd asmOp (_,funcs) =
let env = Hf.create 107 in
List.iter (check_fun pd asmOp env) (List.rev funcs)