1 | |
---|
2 | open Clight |
---|
3 | |
---|
4 | |
---|
5 | (* TODO: Alignment constraints? *) |
---|
6 | let rec size_of_ctype = function |
---|
7 | | Tvoid -> 0 |
---|
8 | | Tint (I8,_) -> 1 |
---|
9 | | Tint (I16,_) -> 2 |
---|
10 | | Tint (I32,_) -> 4 |
---|
11 | | Tfloat _ -> assert false (* Not supported *) |
---|
12 | | Tpointer (sp,_) -> Memory.size_of_region sp |
---|
13 | | Tarray (sp,t,s) -> s*(size_of_ctype t) |
---|
14 | | Tfunction (_,_) -> assert false (* Not supported *) |
---|
15 | | Tstruct (_,lst) -> |
---|
16 | List.fold_left (fun n (_,ty) -> n + (size_of_ctype ty)) 0 lst |
---|
17 | | Tunion (_,lst) -> |
---|
18 | List.fold_left |
---|
19 | (fun n (_,ty) -> |
---|
20 | let sz = (size_of_ctype ty) in (if n>sz then n else sz) |
---|
21 | ) 0 lst |
---|
22 | | Tcomp_ptr (sp,_) -> Memory.size_of_region sp |
---|
23 | |
---|
24 | |
---|
25 | let rec memory_q_of_ctype = function |
---|
26 | | Tvoid -> assert false |
---|
27 | | Tint (I8,Signed) -> Memory.MQ_int8signed |
---|
28 | | Tint (I8,Unsigned) -> Memory.MQ_int8unsigned |
---|
29 | | Tint (I16,Signed) -> Memory.MQ_int16signed |
---|
30 | | Tint (I16,Unsigned) -> Memory.MQ_int16unsigned |
---|
31 | | Tint (I32,Signed) -> Memory.MQ_int32 |
---|
32 | | Tint (I32,Unsigned) -> assert false (* Not supported *) |
---|
33 | | Tfloat _ -> assert false (* Not supported *) |
---|
34 | | Tpointer (sp,_) -> Memory.mq_of_region sp |
---|
35 | | Tarray (sp,c,s) -> Memory.mq_of_region sp |
---|
36 | | Tfunction (_,_) -> assert false (* should not happen thanks to CIL *) |
---|
37 | | Tstruct (_,_) -> assert false (* should not happen thanks to CIL *) |
---|
38 | | Tunion (_,_) -> assert false (* should not happen thanks to CIL *) |
---|
39 | | Tcomp_ptr (sp,_) -> Memory.mq_of_region sp |
---|
40 | |
---|
41 | |
---|
42 | let is_int_type = function |
---|
43 | | Tint (_,_) -> true |
---|
44 | | _ -> false |
---|
45 | |
---|
46 | let is_float_type = function |
---|
47 | | Tfloat _ -> true |
---|
48 | | _ -> false |
---|
49 | |
---|
50 | let is_pointer_type = function |
---|
51 | | Tpointer _ | Tarray _ | Tcomp_ptr _ -> true |
---|
52 | | _ -> false |
---|
53 | |
---|
54 | let is_stack_type = function |
---|
55 | | Tarray _ | Tstruct _ | Tunion _ -> true |
---|
56 | | _ -> false |
---|
57 | |
---|
58 | let is_struct = function |
---|
59 | | Tstruct _ | Tunion _ -> true |
---|
60 | | _ -> false |
---|
61 | |
---|
62 | let is_ptr_to_struct = function |
---|
63 | | Tpointer (_,t) when is_struct t -> true |
---|
64 | | Tcomp_ptr _ -> true |
---|
65 | | _ -> false |
---|
66 | |
---|
67 | let is_function = function |
---|
68 | | Tfunction _ -> true |
---|
69 | | _ -> false |
---|
70 | |
---|
71 | let region_of_pointer_type = function |
---|
72 | | Tpointer (sp,_) | Tarray (sp,_,_) | Tcomp_ptr (sp,_) -> sp |
---|
73 | | _ -> assert false (* do not use on those arguments *) |
---|