package goblint-cil
A front-end for the C programming language that facilitates program analysis and transformation
Install
Dune Dependency
Authors
Maintainers
Sources
1.8.0.tar.gz
md5=796ad26120b5c6b939a57e8623088aef
sha512=01a58ac6d928afead21c8a97af5865715114cd0562234d1d4aef9e4ac5d91415d040a15927c52cb896dbb39a53e915627f498ebe2d026a548c3ff597682041b2
doc/src/goblint-cil.zrapp/availexps.ml.html
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 Cil open Pretty open Expcompare 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
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>