package goblint-cil
A front-end for the C programming language that facilitates program analysis and transformation
Install
Dune Dependency
Authors
Maintainers
Sources
goblint-cil-2.0.1.tbz
sha256=5f81cb3f25c09770e77b5eb4092e6621e456122b6d1219dcc304c062075f9572
sha512=31bb753031e0ef321a2ef065373009270881b1cce7f23167b378845188aed9cb49f18a165edd2e11f751f2c7a7b84ab5ac1da50ba1f5cb975e6e8a97157838ed
doc/src/goblint-cil.liveness/liveness.ml.html
Source file liveness.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
(* Calculate which variables are live at each statement. *) open GoblintCil open Feature open Pretty module Usedef = Usedef (* expose for zrapp *) module DF = Dataflow module UD = Usedef module IH = Inthash module E = Errormsg let debug = ref false (* 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)) let live_label = ref "" let live_func = ref "" module VS = UD.VS let debug_print () vs = (VS.fold (fun vi d -> d ++ text "name: " ++ text vi.vname ++ text " id: " ++ num vi.vid ++ text " ") vs nil) ++ line let min_print () vs = (VS.fold (fun vi d -> d ++ text vi.vname ++ text "(" ++ d_type () vi.vtype ++ text ")" ++ text ",") vs nil) ++ line let printer = ref debug_print module LiveFlow = struct let name = "Liveness" let debug = debug type t = VS.t let pretty () vs = let fn = !printer in fn () vs let stmtStartData = IH.create 32 let funcExitData = VS.empty let combineStmtStartData (stm:stmt) ~(old:t) (now:t) = if not(VS.compare old now = 0) then Some(VS.union old now) else None let combineSuccessors = VS.union let doStmt stmt = if !debug then ignore(E.log "looking at: %a\n" d_stmt stmt); let handle_stm vs = match stmt.skind with Instr _ -> vs | s -> let u, d = UD.computeUseDefStmtKind s in VS.union u (VS.diff vs d) in DF.Post handle_stm let doInstr i vs = let transform vs' = if (!ignore_inst) i then vs' else let u,d = UD.computeUseDefInstr i in VS.union u (VS.diff vs' d) in DF.Post transform let filterStmt stm1 stm2 = true end module L = DF.BackwardsDataFlow(LiveFlow) (* XXX: This does not compute the best ordering to give to the work-list algorithm. *) let all_stmts = ref [] class nullAdderClass = object(self) inherit nopCilVisitor method! vstmt s = all_stmts := s :: (!all_stmts); IH.add LiveFlow.stmtStartData s.sid VS.empty; DoChildren end let null_adder fdec = ignore(visitCilFunction (new nullAdderClass) fdec); !all_stmts let computeLiveness fdec = IH.clear LiveFlow.stmtStartData; UD.onlyNoOffsetsAreDefs := false; all_stmts := []; let a = null_adder fdec in try L.compute a with E.Error -> begin ignore(E.log "Liveness failed on function:\n %a\n" d_global (GFun(fdec,locUnknown))); E.s "Bug in Liveness compute" end let getLiveSet sid = try Some(IH.find LiveFlow.stmtStartData sid) with Not_found -> None let getLiveness (s:stmt) = Inthash.find LiveFlow.stmtStartData s.sid let getPostLiveness (s:stmt) : LiveFlow.t = let foldLiveness live s = VS.union live (getLiveness s) in List.fold_left foldLiveness VS.empty s.succs let instrLiveness (il : instr list) (stm : stmt) (vs : VS.t) (out: bool) : VS.t list = let proc_one vsl i = match vsl with | [] -> if (!ignore_inst) i then vs::vsl else let u,d = UD.computeUseDefInstr i in (VS.union u (VS.diff vs d))::vsl | vs'::rst -> if (!ignore_inst) i then vs'::vsl else let u,d = UD.computeUseDefInstr i in (VS.union u (VS.diff vs' d))::vsl in let liveout = getPostLiveness stm in let folded = List.fold_left proc_one [liveout] (List.rev il) in if out then List.tl folded else folded (* Inherit from this to visit with liveness info at instructions. If out is true, then gives liveness after instructions. If out is false, then gives liveness before instructions. *) class livenessVisitorClass (out : bool) = object(self) inherit nopCilVisitor val mutable sid = -1 val mutable liv_dat_lst = [] val mutable cur_liv_dat = None method! vstmt stm = sid <- stm.sid; match getLiveSet sid with | None -> begin if !debug then E.log "livVis: stm %d has no data\n" sid; cur_liv_dat <- None; DoChildren end | Some vs -> begin match stm.skind with | Instr il -> begin liv_dat_lst <- instrLiveness il stm vs out; DoChildren end | _ -> begin cur_liv_dat <- None; DoChildren end end method! vinst i = try let data = List.hd liv_dat_lst in cur_liv_dat <- Some(data); liv_dat_lst <- List.tl liv_dat_lst; if !debug then E.log "livVis: at %a, data is %a\n" d_instr i debug_print data; DoChildren with Failure _ -> if !debug then E.log "livnessVisitor: il liv_dat_lst mismatch\n"; DoChildren end (* Inherit from this to visit instructions with data about which variables are newly dead after the instruction in post_dead_vars (and which variables are dead *before* each /statement/, also, confusingly, in post_dead_vars). post_live_vars contains vars that are newly live after each instruction *) class deadnessVisitorClass = object(self) inherit nopCilVisitor val mutable sid = -1 val mutable liv_dat_lst = [] val mutable cur_liv_dat = None val mutable post_dead_vars = VS.empty val mutable post_live_vars = VS.empty method! vstmt stm = sid <- stm.sid; match getLiveSet sid with | None -> begin if !debug then E.log "deadVis: stm %d has no data\n" sid; cur_liv_dat <- None; post_dead_vars <- VS.empty; post_live_vars <- VS.empty; DoChildren end | Some vs -> begin let (dead,live) = List.fold_left (fun (dead,live) stm -> let dvs = (* things can die in non instr statements *) match stm.skind with | Instr _ | Block _ -> VS.diff (getPostLiveness stm) vs | _ -> VS.diff (VS.union (getLiveness stm) (getPostLiveness stm)) vs in VS.union dead dvs, VS.union live (getPostLiveness stm)) (VS.empty, VS.empty) stm.preds in if !debug then E.log "deadVis: before %a, %a die, %a come to live\n" d_stmt stm debug_print dead debug_print live; post_dead_vars <- dead; post_live_vars <- VS.diff vs live; match stm.skind with | Instr il -> begin liv_dat_lst <- instrLiveness il stm vs true; DoChildren end | _ -> begin cur_liv_dat <- None; DoChildren end end method! vinst i = try let data = List.hd liv_dat_lst in cur_liv_dat <- Some(data); liv_dat_lst <- List.tl liv_dat_lst; let u,d = UD.computeUseDefInstr i in let inlive = VS.union u (VS.diff data d) in (* if both defined and used, then both dies and comes to life *) let ud = VS.inter u d in post_dead_vars <- VS.union (VS.diff inlive data) ud; post_live_vars <- VS.union (VS.diff data inlive) ud; if !debug then E.log "deadVis: at %a, liveout: %a, inlive: %a, post_dead_vars: %a\n" d_instr i debug_print data debug_print inlive debug_print post_dead_vars; DoChildren with Failure _ -> if !debug then E.log "deadnessVisitor: il liv_dat_lst mismatch\n"; post_dead_vars <- VS.empty; post_live_vars <- VS.empty; DoChildren end let print_everything () = let d = IH.fold (fun i vs d -> d ++ num i ++ text ": " ++ LiveFlow.pretty () vs) LiveFlow.stmtStartData nil in ignore(printf "%t" (fun () -> d)) let match_label lbl = match lbl with Label(str,_,b) -> if !debug then ignore(E.log "Liveness: label seen: %s\n" str); (*b && *)(String.compare str (!live_label) = 0) | _ -> false class doFeatureClass = object(self) inherit nopCilVisitor method! vfunc fd = if String.compare fd.svar.vname (!live_func) = 0 then (Cfg.clearCFGinfo fd; ignore(Cfg.cfgFun fd); computeLiveness fd; if String.compare (!live_label) "" = 0 then (printer := min_print; print_everything(); SkipChildren) else DoChildren) else SkipChildren method! vstmt s = if List.exists match_label s.labels then try let vs = IH.find LiveFlow.stmtStartData s.sid in (printer := min_print; ignore(printf "%a" LiveFlow.pretty vs); SkipChildren) with Not_found -> if !debug then ignore(E.log "Liveness: stmt: %d not found\n" s.sid); DoChildren else (if List.length s.labels = 0 then if !debug then ignore(E.log "Liveness: no label at sid=%d\n" s.sid); DoChildren) end let do_live_feature (f:file) = visitCilFile (new doFeatureClass) f let feature = { fd_name = "Liveness"; fd_enabled = false; fd_description = "Spit out live variables at a label"; fd_extraopt = [ "--live_label", Arg.String (fun s -> live_label := s), " Output the variables live at this label"; "--live_func", Arg.String (fun s -> live_func := s), " Output the variables live at each statement in this function."; "--live_debug", Arg.Unit (fun n -> debug := true), " Print lots of debugging info";]; fd_doit = do_live_feature; fd_post_check = false } let () = Feature.register feature
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>