package goblint-cil

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file availexpslv.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
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
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
(* compute available expressions, although in a somewhat
   non-traditional way. the abstract state is a mapping from
   lvalues to expressions as opposed to a set of
   expressions *)
open GoblintCil
open Pretty
open Expcompare
open Liveness

module E = Errormsg
module DF = Dataflow
module UD = Usedef
module IH = Inthash
module H = Hashtbl
module U = Util
module S = Stats

exception Unimplemented of string

let debug = ref false
let doTime = ref false


let time s f a =
  if !doTime then
    S.time s f a
  else f a

(*
   When ignore_inst returns true, then
   the instruction in question has no
   effects on the abstract state.
   When ignore_call returns true, then
   the instruction only has side-effects
   from the assignment if there is one.
 *)
let ignore_inst = ref (fun i -> false)
let ignore_call = ref (fun i -> false)

let registerIgnoreInst (f : instr -> bool) : unit =
  let f' = !ignore_inst in
  ignore_inst := (fun i -> (f i) || (f' i))

let registerIgnoreCall (f : instr -> bool) : unit =
  let f' = !ignore_call in
  ignore_call := (fun i -> (f i) || (f' i))


module LvExpHash =
  H.Make(struct
    type t = lval
    let equal lv1 lv2 = compareLval lv1 lv2
    let hash = H.hash
  end)

(* exp LvExpHash.t -> exp LvExpHash.t -> bool *)
let lvh_equals lvh1 lvh2 =
  if not(LvExpHash.length lvh1 = LvExpHash.length lvh2)
  then false
  else LvExpHash.fold (fun lv e b ->
    if not b then b else
    try let e2 = LvExpHash.find lvh2 lv in
    if not(compareExpStripCasts e e2)
    then false
    else true
    with Not_found -> false)
      lvh1 true

let lvh_pretty () lvh = LvExpHash.fold (fun lv e d ->
  d ++ line ++ (d_lval () lv) ++ text " -> " ++ (d_exp () e))
    lvh nil


(* the result must be the intersection of eh1 and eh2 *)
(* exp IH.t -> exp IH.t -> exp IH.t *)
let lvh_combine lvh1 lvh2 =
  if !debug then ignore(E.log "lvh_combine: combining %a\n and\n %a\n"
			  lvh_pretty lvh1 lvh_pretty lvh2);
  let lvh' = LvExpHash.copy lvh1 in (* eh' gets all of eh1 *)
  LvExpHash.iter (fun lv e1 ->
    try let e2l = LvExpHash.find_all lvh2 lv in
    if not(List.exists (fun e2 -> compareExpStripCasts e1 e2) e2l)
    (* remove things from eh' that eh2 doesn't have *)
    then let e1l = LvExpHash.find_all lvh' lv in
    let e1l' = List.filter (fun e -> not(compareExpStripCasts e e1)) e1l in
    LvExpHash.remove lvh' lv;
    List.iter (fun e -> LvExpHash.add lvh' lv e) e1l'
    with Not_found ->
      LvExpHash.remove lvh' lv) lvh1;
  if !debug then ignore(E.log "with result %a\n"
			  lvh_pretty lvh');
  lvh'


(* On a memory write, kill expressions containing memory reads
   variables whose address has been taken, and globals. *)
class memReadOrAddrOfFinderClass br = object(self)
  inherit nopCilVisitor

  method! vexpr e = match e with
  | AddrOf(Mem _, _)
  | StartOf(Mem _, _)
  | Lval(Mem _, _) -> begin
      br := true;
      SkipChildren
  end
  | AddrOf(Var vi, NoOffset) ->
      (* Writing to memory won't change the address of something *)
      SkipChildren
  | _ -> DoChildren

  method! vvrbl vi =
    if vi.vaddrof || vi.vglob then
      (br := true;
       SkipChildren)
    else DoChildren

end


(* exp -> bool *)
let exp_has_mem_read e =
  let br = ref false in
  let vis = new memReadOrAddrOfFinderClass br in
  ignore(visitCilExpr vis e);
  !br

let lval_has_mem_read lv =
  let br = ref false in
  let vis = new memReadOrAddrOfFinderClass br in
  ignore(visitCilLval vis lv);
  !br

let offset_has_mem_read off =
    let br = ref false in
    let vis = new memReadOrAddrOfFinderClass br in
    ignore(visitCilOffset vis off);
    !br

let lvh_kill_mem lvh =
  LvExpHash.iter (fun lv e ->
    match lv with
    | (Mem _, _) -> LvExpHash.remove lvh lv
    | _ ->
        if exp_has_mem_read e || lval_has_mem_read lv
        then LvExpHash.remove lvh lv)
    lvh

(* need to kill exps containing a particular vi sometimes *)
class viFinderClass vi br = object(self)
  inherit nopCilVisitor

  method! vvrbl vi' =
    if vi.vid = vi'.vid
    then (br := true; SkipChildren)
    else DoChildren

end

let instr_has_vi vi i =
  let br = ref false in
  let vis = new viFinderClass vi br in
  ignore(visitCilInstr vis i);
  !br

let exp_has_vi vi e =
  let br = ref false in
  let vis = new viFinderClass vi br in
  ignore(visitCilExpr vis e);
  !br

let lval_has_vi vi lv =
  let br = ref false in
  let vis = new viFinderClass vi br in
  ignore(visitCilLval vis lv);
  !br

let lvh_kill_vi lvh vi =
  LvExpHash.iter (fun lv e ->
    if exp_has_vi vi e || lval_has_vi vi lv
    then LvExpHash.remove lvh lv)
    lvh

(* need to kill exps containing a particular lval sometimes *)
class lvalFinderClass lv br = object(self)
  inherit nopCilVisitor

  method! vlval l =
    if compareLval l lv
    then (br := true; SkipChildren)
    else DoChildren

end

let exp_has_lval lv e =
  let br = ref false in
  let vis = new lvalFinderClass lv br in
  ignore(visitCilExpr vis e);
  !br

let lval_has_lval lv (host,hostoff) =
  let br = ref false in
  let vis = new lvalFinderClass lv br in
  (match host with
  | Mem e -> ignore(visitCilExpr vis e)
  | _ -> ());
  ignore(visitCilOffset vis hostoff);
  !br

let lvh_kill_lval lvh lv =
  LvExpHash.iter (fun lv' e ->
    if exp_has_lval lv e || lval_has_lval lv lv'
    then LvExpHash.remove lvh lv')
    lvh


class volatileFinderClass br = object(self)
  inherit nopCilVisitor

  method! vexpr e =
    if (hasAttribute "volatile" (typeAttrs (typeOf e)))
    then (br := true; SkipChildren)
    else DoChildren
end

let exp_is_volatile e : bool =
  let br = ref false in
  let vis = new volatileFinderClass br in
  ignore(visitCilExpr vis e);
  !br

(* let varHash = IH.create 32 *)

class addrOfOrGlobalFinderClass br = object(self)
  inherit nopCilVisitor

  method! vvrbl vi =
    if vi.vaddrof || vi.vglob
    then (br := true; SkipChildren)
    else DoChildren

end

let exp_has_addrof_or_global e =
    let br = ref false in
    let vis = new addrOfOrGlobalFinderClass br in
    ignore(visitCilExpr vis e);
    !br

let lval_has_addrof_or_global lv =
  let br = ref false in
  let vis = new addrOfOrGlobalFinderClass br in
  ignore(visitCilLval vis lv);
  !br

let lvh_kill_addrof_or_global lvh =
  LvExpHash.iter (fun lv e ->
    if lval_has_addrof_or_global lv
    then LvExpHash.remove lvh lv)
    lvh


let lvh_handle_inst i lvh =
  if (!ignore_inst) i then lvh else
  match i with
    Set(lv,e,_,_) -> begin
      match lv with
      | (Mem _, _) -> begin
	  LvExpHash.replace lvh lv e;
	  lvh_kill_mem lvh;
	  lvh_kill_addrof_or_global lvh;
	  lvh
      end
      | _ when not (exp_is_volatile e) -> begin
	  (* ignore x = x *)
	  if compareExpStripCasts (Lval lv) e then lvh
	  else begin
	    LvExpHash.replace lvh lv e;
	    lvh_kill_lval lvh lv;
	    lvh
	  end
      end
      | _ -> begin (* e is volatile *)
        (* must remove mapping for lv *)
	    if !debug then ignore(E.log "lvh_handle_inst: %a is volatile. killing %a\n"
		    d_exp e d_lval lv);
	    LvExpHash.remove lvh lv;
	    lvh_kill_lval lvh lv;
	    lvh
      end
    end
  | Call(Some lv,_,_,_,_) -> begin
      LvExpHash.remove lvh lv;
      lvh_kill_lval lvh lv;
      if not((!ignore_call) i) then begin
        lvh_kill_mem lvh;
	    lvh_kill_addrof_or_global lvh
      end;
      lvh
  end
  | Call(_,_,_,_,_) -> begin
      if not((!ignore_call) i) then begin
	lvh_kill_mem lvh;
	lvh_kill_addrof_or_global lvh;
      end;
      lvh
  end
  | Asm(_,_,_,_,_,_) -> begin
      let _,d = UD.computeUseDefInstr i in
      UD.VS.iter (fun vi ->
	lvh_kill_vi lvh vi) d;
      lvh
  end
  | VarDecl _ ->   raise (Unimplemented "VarDecl") (* VarDecl instruction is not supported for availexpslv, to make availexpslv work for programs without VLA *)
                                                   (* make sure to set alwaysGenerateVarDecl in cabs2cil.ml to false. To support VLA, implement this.  *)

module AvailableExps =
  struct

    let name = "Available Expressions"

    let debug = debug

    (* mapping from var id to expression *)
    type t = exp LvExpHash.t

    let copy = LvExpHash.copy

    let stmtStartData = IH.create 64

    let pretty = lvh_pretty

    let computeFirstPredecessor stm lvh = lvh

    let combinePredecessors (stm:stmt) ~(old:t) (lvh:t) =
      if time "lvh_equals" (lvh_equals old) lvh then None else
      Some(time "lvh_combine" (lvh_combine old) lvh)

    let doInstr i lvh =
      let action = lvh_handle_inst i in
      DF.Post(action)

    let doStmt stm astate = DF.SDefault

    let doGuard c astate = DF.GDefault

    let filterStmt stm = true

  end

module AE = DF.ForwardsDataFlow(AvailableExps)


(*
   Computes AEs for function fd.


 *)
let computeAEs fd =
  try let slst = fd.sbody.bstmts in
  let first_stm = List.hd slst in
  (*time "make_var_hash" make_var_hash fd;*)
  IH.clear AvailableExps.stmtStartData;
  IH.add AvailableExps.stmtStartData first_stm.sid (LvExpHash.create 4);
  time "compute" AE.compute [first_stm]
  with Failure _ -> if !debug then ignore(E.log "fn w/ no stmts?\n")
  | Not_found -> if !debug then ignore(E.log "no data for first_stm?\n")


(* get the AE data for a statement *)
let getAEs sid =
  try Some(IH.find AvailableExps.stmtStartData sid)
  with Not_found -> None

(* get the AE data for an instruction list *)
let instrAEs il sid lvh out =
  if !debug then ignore(E.log "instrAEs\n");
  let proc_one hil i =
    match hil with
      [] -> let lvh' = LvExpHash.copy lvh in
      let lvh'' = lvh_handle_inst i lvh' in
       lvh''::hil
    | lvh'::ehrst as l ->
	let lvh' = LvExpHash.copy lvh' in
	let lvh'' = lvh_handle_inst i lvh' in
	lvh''::l
  in
  let folded = List.fold_left proc_one [lvh] il in
  let foldednotout = List.rev (List.tl folded) in
  foldednotout

class aeVisitorClass = object(self)
  inherit nopCilVisitor

  val mutable sid = -1

  val mutable ae_dat_lst = []

  val mutable cur_ae_dat = None

  method! vstmt stm =
    sid <- stm.sid;
    match getAEs sid with
      None ->
	if !debug then ignore(E.log "aeVis: stm %d has no data\n" sid);
	cur_ae_dat <- None;
	DoChildren
    | Some eh ->
	match stm.skind with
	  Instr il ->
	    if !debug then ignore(E.log "aeVist: visit il\n");
	    ae_dat_lst <- time "instrAEs" (instrAEs il stm.sid eh) false;
	    DoChildren
	| _ ->
	    if !debug then ignore(E.log "aeVisit: visit non-il\n");
	    cur_ae_dat <- None;
	    DoChildren

  method! vinst i =
    if !debug then ignore(E.log "aeVist: before %a, ae_dat_lst is %d long\n"
			    d_instr i (List.length ae_dat_lst));
    try
      let data = List.hd ae_dat_lst in
      cur_ae_dat <- Some(data);
      ae_dat_lst <- List.tl ae_dat_lst;
      if !debug then ignore(E.log "aeVisit: data is %a\n" lvh_pretty data);
      DoChildren
    with Failure _ ->
      if !debug then ignore(E.log "aeVis: il ae_dat_lst mismatch\n");
      DoChildren

  method get_cur_eh () =
    match cur_ae_dat with
      None -> getAEs sid
    | Some eh -> Some eh

end
OCaml

Innovation. Community. Security.