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
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
|
(*
*
* Copyright (c) 2005,
* George C. Necula <necula@cs.berkeley.edu>
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* 1. Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
* 2. Redistributions in binary form must reproduce the above copyright
* notice, this list of conditions and the following disclaimer in the
* documentation and/or other materials provided with the distribution.
*
* 3. The names of the contributors may not be used to endorse or promote
* products derived from this software without specific prior written
* permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
* IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
* OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
* EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
* PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
* PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
* LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
* NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
* SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*
*)
(** This is a module that inserts runtime checks for memory reads/writes and
* allocations *)
open Pretty
open Cil
module E = Errormsg
module H = Hashtbl
let doSfi = ref false
let doSfiReads = ref false
let doSfiWrites = ref true
(* A number of functions to be skipped *)
let skipFunctions : (string, unit) H.t = H.create 13
let mustSfiFunction (f: fundec) : bool =
not (H.mem skipFunctions f.svar.vname)
(** Some functions are known to be allocators *)
type dataLocation =
InResult (* Interesting data is in the return value *)
| InArg of int (* in the nth argument. Starts from 1. *)
| InArgTimesArg of int * int (* (for size) data is the product of two
* arguments *)
| PointedToByArg of int (* pointed to by nth argument *)
(** Compute the data based on the location and the actual argument list *)
let extractData (dl: dataLocation) (args: exp list) (res: lval option) : exp =
let getArg (n: int) =
try List.nth args (n - 1) (* Args are based at 1 *)
with _ -> E.s (E.bug "Cannot extract argument %d at %a"
n d_loc !currentLoc)
in
match dl with
InResult -> begin
match res with
None ->
E.s (E.bug "Cannot extract InResult data (at %a)" d_loc !currentLoc)
| Some r -> Lval r
end
| InArg n -> getArg n
| InArgTimesArg (n1, n2) ->
let a1 = getArg n1 in
let a2 = getArg n2 in
BinOp(Mult, mkCast ~e:a1 ~newt:longType,
mkCast ~e:a2 ~newt:longType, longType)
| PointedToByArg n ->
let a = getArg n in
Lval (mkMem a NoOffset)
(* for each allocator, where is the length and where is the result *)
let allocators: (string, (dataLocation * dataLocation)) H.t = H.create 13
let _ =
H.add allocators "malloc" (InArg 1, InResult);
H.add allocators "calloc" (InArgTimesArg (1, 2), InResult);
H.add allocators "realloc" (InArg 2, InResult)
(* for each deallocator, where is the data being deallocated *)
let deallocators: (string, dataLocation) H.t = H.create 13
let _=
H.add deallocators "free" (InArg 1);
H.add deallocators "realloc" (InArg 1)
(* Returns true if the given lvalue offset ends in a bitfield access. *)
let rec is_bitfield lo = match lo with
| NoOffset -> false
| Field(fi,NoOffset) -> not (fi.fbitfield = None)
| Field(_,lo) -> is_bitfield lo
| Index(_,lo) -> is_bitfield lo
(* Return an expression that evaluates to the address of the given lvalue.
* For most lvalues, this is merely AddrOf(lv). However, for bitfields
* we do some offset gymnastics.
*)
let addr_of_lv (lv: lval) =
let lh, lo = lv in
if is_bitfield lo then begin
(* we figure out what the address would be without the final bitfield
* access, and then we add in the offset of the bitfield from the
* beginning of its enclosing comp *)
let rec split_offset_and_bitfield lo = match lo with
| NoOffset -> failwith "logwrites: impossible"
| Field(fi,NoOffset) -> (NoOffset,fi)
| Field(e,lo) -> let a,b = split_offset_and_bitfield lo in
((Field(e,a)),b)
| Index(e,lo) -> let a,b = split_offset_and_bitfield lo in
((Index(e,a)),b)
in
let new_lv_offset, bf = split_offset_and_bitfield lo in
let new_lv = (lh, new_lv_offset) in
let enclosing_type = TComp(bf.fcomp, []) in
let bits_offset, bits_width =
bitsOffset enclosing_type (Field(bf,NoOffset)) in
let bytes_offset = bits_offset / 8 in
let lvPtr = mkCast ~e:(mkAddrOf (new_lv)) ~newt:(charPtrType) in
(BinOp(PlusPI, lvPtr, (integer bytes_offset), ulongType))
end else
(mkAddrOf (lh,lo))
let mustLogLval (forwrite: bool) (lv: lval) : bool =
match lv with
Var v, off -> (* Inside a variable. We assume the array offsets are fine *)
false
| Mem e, off ->
if forwrite && not !doSfiWrites then
false
else if not forwrite && not !doSfiReads then
false
(* If this is an lval of function type, we do not log it *)
else if isFunctionType (typeOfLval lv) then
false
else
true
(* Create prototypes for the logging functions *)
let mkProto (name: string) (args: (string * typ * attributes) list) =
let fdec = emptyFunction name in
fdec.svar.vtype <- TFun(voidType,
Some args, false, []);
fdec
let logReads = mkProto "logRead" [ ("addr", voidPtrType, []);
("what", charPtrType, []);
("file", charPtrType, []);
("line", intType, []) ]
let callLogRead (lv: lval) =
let what = Pretty.sprint 80 (d_lval () lv) in
Call(None,
Lval(Var(logReads.svar),NoOffset),
[ addr_of_lv lv; mkString what; mkString !currentLoc.file;
integer !currentLoc.line], !currentLoc )
let logWrites = mkProto "logWrite" [ ("addr", voidPtrType, []);
("what", charPtrType, []);
("file", charPtrType, []);
("line", intType, []) ]
let callLogWrite (lv: lval) =
let what = Pretty.sprint 80 (d_lval () lv) in
Call(None,
Lval(Var(logWrites.svar), NoOffset),
[ addr_of_lv lv; mkString what; mkString !currentLoc.file;
integer !currentLoc.line], !currentLoc )
let logStackFrame = mkProto "logStackFrame" [ ("func", charPtrType, []) ]
let callLogStack (fname: string) =
Call(None,
Lval(Var(logStackFrame.svar), NoOffset),
[ mkString fname; ], !currentLoc )
let logAlloc = mkProto "logAlloc" [ ("addr", voidPtrType, []);
("size", intType, []);
("file", charPtrType, []);
("line", intType, []) ]
let callLogAlloc (szloc: dataLocation)
(resLoc: dataLocation)
(args: exp list)
(res: lval option) =
let sz = extractData szloc args res in
let res = extractData resLoc args res in
Call(None,
Lval(Var(logAlloc.svar), NoOffset),
[ res; sz; mkString !currentLoc.file;
integer !currentLoc.line ], !currentLoc )
let logFree = mkProto "logFree" [ ("addr", voidPtrType, []);
("file", charPtrType, []);
("line", intType, []) ]
let callLogFree (dataloc: dataLocation)
(args: exp list)
(res: lval option) =
let data = extractData dataloc args res in
Call(None,
Lval(Var(logFree.svar), NoOffset),
[ data; mkString !currentLoc.file;
integer !currentLoc.line ], !currentLoc )
class sfiVisitorClass : Cil.cilVisitor = object (self)
inherit nopCilVisitor
method vexpr (e: exp) : exp visitAction =
match e with
Lval lv when mustLogLval false lv -> (* A read *)
self#queueInstr [ callLogRead lv ];
DoChildren
| _ -> DoChildren
method vinst (i: instr) : instr list visitAction =
match i with
Set(lv, e, l) when mustLogLval true lv ->
self#queueInstr [ callLogWrite lv ];
DoChildren
| Call(lvo, f, args, l) ->
(* Instrument the write *)
(match lvo with
Some lv when mustLogLval true lv ->
self#queueInstr [ callLogWrite lv ]
| _ -> ());
(* Do the expressions in the call, and then see if we need to
* instrument the function call *)
ChangeDoChildrenPost
([i],
(fun il ->
currentLoc := l;
match f with
Lval (Var fv, NoOffset) -> begin
(* Is it an allocator? *)
try
let szloc, resloc = H.find allocators fv.vname in
il @ [callLogAlloc szloc resloc args lvo]
with Not_found -> begin
(* Is it a deallocator? *)
try
let resloc = H.find deallocators fv.vname in
il @ [ callLogFree resloc args lvo ]
with Not_found ->
il
end
end
| _ -> il))
| _ -> DoChildren
method vfunc (fdec: fundec) =
(* Instead a stack log at the start of a function *)
ChangeDoChildrenPost
(fdec,
fun fdec ->
fdec.sbody <-
mkBlock
[ mkStmtOneInstr (callLogStack fdec.svar.vname);
mkStmt (Block fdec.sbody) ];
fdec)
end
let doit (f: file) =
let sfiVisitor = new sfiVisitorClass in
let compileLoc (l: location) = function
ACons("inres", []) -> InResult
| ACons("inarg", [AInt n]) -> InArg n
| ACons("inargxarg", [AInt n1; AInt n2]) -> InArgTimesArg (n1, n2)
| ACons("pointedby", [AInt n]) -> PointedToByArg n
| _ -> E.warn "Invalid location at %a" d_loc l;
InResult
in
iterGlobals f
(fun glob ->
match glob with
GFun(fdec, _) when mustSfiFunction fdec ->
ignore (visitCilFunction sfiVisitor fdec)
| GPragma(Attr("sfiignore", al), l) ->
List.iter
(function AStr fn -> H.add skipFunctions fn ()
| _ -> E.warn "Invalid argument in \"sfiignore\" pragma at %a"
d_loc l)
al
| GPragma(Attr("sfialloc", al), l) -> begin
match al with
AStr fname :: locsz :: locres :: [] ->
H.add allocators fname (compileLoc l locsz, compileLoc l locres)
| _ -> E.warn "Invalid sfialloc pragma at %a" d_loc l
end
| GPragma(Attr("sfifree", al), l) -> begin
match al with
AStr fname :: locwhat :: [] ->
H.add deallocators fname (compileLoc l locwhat)
| _ -> E.warn "Invalid sfifree pragma at %a" d_loc l
end
| _ -> ());
(* Now add the prototypes for the instrumentation functions *)
f.globals <-
GVarDecl (logReads.svar, locUnknown) ::
GVarDecl (logWrites.svar, locUnknown) ::
GVarDecl (logStackFrame.svar, locUnknown) ::
GVarDecl (logAlloc.svar, locUnknown) ::
GVarDecl (logFree.svar, locUnknown) :: f.globals
let feature : featureDescr =
{ fd_name = "sfi";
fd_enabled = doSfi;
fd_description = "instrument memory operations";
fd_extraopt = [
"--sfireads", Arg.Set doSfiReads, "SFI for reads";
"--sfiwrites", Arg.Set doSfiWrites, "SFI for writes";
];
fd_doit = doit;
fd_post_check = true;
}
|