package goblint-cil

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

Source file availexps.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
(* compute available expressions, although in a somewhat
   non-traditional way. the abstract state is a mapping from
   variable ids 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 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))


(* exp IH.t -> exp IH.t -> bool *)
let eh_equals eh1 eh2 =
  if not(IH.length eh1 = IH.length eh2)
  then false
  else IH.fold (fun vid e b ->
    if not b then b else
    try let e2 = IH.find eh2 vid in
    if not(compareExpStripCasts e e2)
    then false
    else true
    with Not_found -> false)
      eh1 true

let eh_pretty () eh = line ++ seq ~sep:line ~doit:(fun (vid,e) ->
  text "AE:vid:" ++ num vid ++ text ": " ++
    (d_exp () e)) ~elements:(IH.tolist eh)

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


(* 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
  | 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 eh_kill_mem eh =
  IH.iter (fun vid e ->
    if exp_has_mem_read e
    then IH.remove eh vid)
    eh

(* 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 exp_has_vi vi e =
  let br = ref false in
  let vis = new viFinderClass vi br in
  ignore(visitCilExpr vis e);
  !br

let eh_kill_vi eh vi =
  IH.iter (fun vid e ->
    if exp_has_vi vi e
    then IH.remove eh vid)
    eh

(* 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 eh_kill_lval eh lv =
  IH.iter (fun vid e ->
    if exp_has_lval lv e
    then IH.remove eh vid)
    eh


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

let eh_kill_addrof_or_global eh =
  if !debug then ignore(E.log "eh_kill: in eh_kill\n");
  IH.iter (fun vid e ->
    try let vi = IH.find varHash vid in
    if vi.vaddrof
    then begin
      if !debug then ignore(E.log "eh_kill: %s has its address taken\n"
			      vi.vname);
      IH.remove eh vid
    end
    else if vi.vglob
    then begin
      if !debug then ignore(E.log "eh_kill: %s is global\n"
			   vi.vname);
      IH.remove eh vid
    end
    with Not_found -> ()) eh

let eh_handle_inst i eh =
  if (!ignore_inst) i then eh else
  match i with
    (* if a pointer write, kill things with read in them.
       also kill mappings from vars that have had their address taken,
       and globals.
       otherwise kill things with lv in them and add e *)
    Set(lv,e,_,_) -> (match lv with
      (Mem _, _) ->
	(eh_kill_mem eh;
	 eh_kill_addrof_or_global eh;
	 eh)
    | (Var vi, NoOffset) when not (exp_is_volatile e) ->
	(match e with
	  Lval(Var vi', NoOffset) -> (* ignore x = x *)
	    if vi'.vid = vi.vid then eh else
	    (IH.replace eh vi.vid e;
	     eh_kill_vi eh vi;
	     eh)
	| _ ->
	    (IH.replace eh vi.vid e;
	     eh_kill_vi eh vi;
	     eh))
    | (Var vi, _ ) -> begin
	(* must remove mapping for vi *)
	IH.remove eh vi.vid;
	eh_kill_lval eh lv;
	eh
    end)
  | Call(Some(Var vi,NoOffset),_,_,_,_) ->
      (IH.remove eh vi.vid;
       eh_kill_vi eh vi;
       if not((!ignore_call) i) then begin
	 eh_kill_mem eh;
	 eh_kill_addrof_or_global eh
       end;
       eh)
  | Call(_,_,_,_,_) ->
      (eh_kill_mem eh;
       eh_kill_addrof_or_global eh;
       eh)
  | Asm(_,_,_,_,_,_) ->
      let _,d = UD.computeUseDefInstr i in
      (UD.VS.iter (fun vi ->
	eh_kill_vi eh vi) d;
       eh)
  | VarDecl _ ->   raise (Unimplemented "VarDecl") (* VarDecl instruction is not supported for availexps, to make availexps 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 IH.t

    let copy = IH.copy

    let stmtStartData = IH.create 64

    let pretty = eh_pretty

    let computeFirstPredecessor stm eh = eh

    let combinePredecessors (stm:stmt) ~(old:t) (eh:t) =
      if time "eh_equals" (eh_equals old) eh then None else
      Some(time "eh_combine" (eh_combine old) eh)

    let doInstr i eh =
      let action = eh_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)

(* make an exp IH.t with everything in it,
   also, fill in varHash while we're here.
 *)
class varHashMakerClass = object(self)
  inherit nopCilVisitor

  method! vvrbl vi =
    (if not(IH.mem varHash vi.vid)
    then
      (if !debug && vi.vglob then ignore(E.log "%s is global\n" vi.vname);
       if !debug && not(vi.vglob) then ignore(E.log "%s is not global\n" vi.vname);
       IH.add varHash vi.vid vi));
    DoChildren

end

let varHashMaker = new varHashMakerClass

let make_var_hash fd =
  IH.clear varHash;
  ignore(visitCilFunction varHashMaker fd)

(*
   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 (IH.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 eh out =
  let proc_one hil i =
    match hil with
      [] -> let eh' = IH.copy eh in
      let eh'' = eh_handle_inst i eh' in
       eh''::hil
    | eh'::ehrst as l ->
	let eh' = IH.copy eh' in
	let eh'' = eh_handle_inst i eh' in
	eh''::l
  in
  let folded = List.fold_left proc_one [eh] 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" eh_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.