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
|
open Cil
(* Contributed by Nathan Cooprider *)
let isOne e =
isInteger e = Some Int64.one
(* written by Zach *)
let is_volatile_tp tp =
List.exists (function (Attr("volatile",_)) -> true
| _ -> false) (typeAttrs tp)
(* written by Zach *)
let is_volatile_vi vi =
let vi_vol =
List.exists (function (Attr("volatile",_)) -> true
| _ -> false) vi.vattr in
let typ_vol = is_volatile_tp vi.vtype in
vi_vol || typ_vol
(*****************************************************************************
* A collection of useful functions that were not already in CIL as far as I
* could tell. However, I have been surprised before . . .
****************************************************************************)
type sign = Signed | Unsigned
exception Not_an_integer
(*****************************************************************************
* A bunch of functions for accessing integers. Originally written for
* somebody who didn't know CIL and just wanted to mess with it at the
* OCaml level.
****************************************************************************)
let unbox_int_type (ye : typ) : (int * sign) =
let tp = unrollType ye in
let s =
match tp with
TInt (i, _) ->
if (isSigned i) then
Signed
else
Unsigned
| _ -> raise Not_an_integer
in
(bitsSizeOf tp), s
(* depricated. Use isInteger directly instead *)
let unbox_int_exp (e : exp) : int64 =
match isInteger e with
None -> raise Not_an_integer
| Some (x) -> x
let box_int_to_exp (n : int64) (ye : typ) : exp =
let tp = unrollType ye in
match tp with
TInt (i, _) ->
kinteger64 i n
| _ -> raise Not_an_integer
let cil_to_ocaml_int (e : exp) : (int64 * int * sign) =
let v, s = unbox_int_type (typeOf e) in
unbox_int_exp (e), v, s
exception Weird_bitwidth
(* (int64 * int * sign) : exp *)
let ocaml_int_to_cil v n s =
let char_size = bitsSizeOf charType in
let int_size = bitsSizeOf intType in
let short_size = bitsSizeOf (TInt(IShort,[]))in
let long_size = bitsSizeOf longType in
let longlong_size = bitsSizeOf (TInt(ILongLong,[])) in
let i =
match s with
Signed ->
if (n = char_size) then
ISChar
else if (n = int_size) then
IInt
else if (n = short_size) then
IShort
else if (n = long_size) then
ILong
else if (n = longlong_size) then
ILongLong
else
raise Weird_bitwidth
| Unsigned ->
if (n = char_size) then
IUChar
else if (n = int_size) then
IUInt
else if (n = short_size) then
IUShort
else if (n = long_size) then
IULong
else if (n = longlong_size) then
IULongLong
else
raise Weird_bitwidth
in
kinteger64 i v
(*****************************************************************************
* a couple of type functions that I thought would be useful:
****************************************************************************)
let rec isCompositeType tp =
match tp with
TComp _ -> true
| TPtr(x, _) -> isCompositeType x
| TArray(x,_,_) -> isCompositeType x
| TFun(x,_,_,_) -> isCompositeType x
| TNamed (x,_) -> isCompositeType x.ttype
| _ -> false
(** START OF deepHasAttribute ************************************************)
let visited = ref []
class attribute_checker target rflag = object (self)
inherit nopCilVisitor
method vtype t =
match t with
TComp(cinfo, a) ->
if(not (List.exists (fun x -> cinfo.cname = x) !visited )) then begin
visited := cinfo.cname :: !visited;
List.iter
(fun f ->
if (hasAttribute target f.fattr) then
rflag := true
else
ignore(visitCilType (new attribute_checker target rflag)
f.ftype)) cinfo.cfields;
end;
DoChildren
| TNamed(t1, a) ->
if(not (List.exists (fun x -> t1.tname = x) !visited )) then begin
visited := t1.tname :: !visited;
ignore(visitCilType (new attribute_checker target rflag) t1.ttype);
end;
DoChildren
| _ ->
DoChildren
method vattr (Attr(name,params)) =
if (name = target) then rflag := true;
DoChildren
end
let deepHasAttribute s t =
let found = ref false in
visited := [];
ignore(visitCilType (new attribute_checker s found) t);
!found
(** END OF deepHasAttribute **************************************************)
(** Stuff from ptranal, slightly modified ************************************)
(*****************************************************************************
* A transformation to make every instruction be in its own statement.
****************************************************************************)
class callBBVisitor = object
inherit nopCilVisitor
method vstmt s =
match s.skind with
Instr(il) -> begin
if (List.length il > 1) then
let list_of_stmts = List.map (fun one_inst ->
mkStmtOneInstr one_inst) il in
let block = mkBlock list_of_stmts in
s.skind <- Block block;
ChangeTo(s)
else
SkipChildren
end
| _ -> DoChildren
method vvdec _ = SkipChildren
method vexpr _ = SkipChildren
method vlval _ = SkipChildren
method vtype _ = SkipChildren
end
let one_instruction_per_statement f =
let thisVisitor = new callBBVisitor in
visitCilFileSameGlobals thisVisitor f
(*****************************************************************************
* A transformation that gives each variable a unique identifier.
****************************************************************************)
class vidVisitor = object
inherit nopCilVisitor
val count = ref 0
method vvdec vi =
vi.vid <- !count ;
incr count ; SkipChildren
end
let globally_unique_vids f =
let thisVisitor = new vidVisitor in
visitCilFileSameGlobals thisVisitor f
(** End of stuff from ptranal ************************************************)
class sidVisitor = object
inherit nopCilVisitor
val count = ref 0
method vstmt s =
s.sid <- !count ;
incr count ;
DoChildren
end
let globally_unique_sids f =
let thisVisitor = new sidVisitor in
visitCilFileSameGlobals thisVisitor f
(** Comparing expressions without a Out_of_memory error **********************)
let compare_exp x y =
compare x y
|
