Skip to content

Commit

Permalink
cleanup transform, remove custom dep tracking
Browse files Browse the repository at this point in the history
  • Loading branch information
@just-max
just-max committed Mar 1, 2023
1 parent dc76dad commit 5ad50bb
Showing 1 changed file with 28 additions and 193 deletions.
221 changes: 28 additions & 193 deletions src/transform/deadCode.ml
View file
Original file line number Diff line number Diff line change
@@ -1,15 +1,9 @@
open BatPervasives open Stdlib
open Batteries
open GoblintCil

let f = Printf.sprintf
let pf fmt = Printf.ksprintf print_endline fmt
let df fmt = Pretty.gprintf (Pretty.sprint ~width:max_int) fmt
let dpf fmt = Pretty.gprintf (fun doc -> print_endline @@ Pretty.sprint ~width:max_int doc) fmt

(* what to do about goto to removed statements? probably just check if the target of a goto should be removed, if so remove the goto? <- don't do that.
but if the target is not live, the goto can't be live anyway *)

(** Filter statements out of a block (recursively). CFG fields (prev, next, etc.) are no longer valid after calling.
Returns true if anything is left in block, false if the block is now empty.
Invariants:
- f (goto label) ==> f (labelled stmt), i.e. if a goto statement is not filtered out, the target may not be filtered out either.
- block may not contain switch statements *)
Expand All @@ -21,135 +15,20 @@ let filter_map_block f (block : Cil.block) : bool =
and impl_stmt stmt =
if not (f stmt) then false
else
let skind', keep =
(* TODO: if sk is not changed in the end, simplify here *)
match (stmt.skind : stmtkind) with
| If (_, b1, b2, _, _) as sk ->
(* be careful to not short-circuit, since call to impl_block b2 is always needed for side-effects *)
sk, let keep_b1, keep_b2 = impl_block b1, impl_block b2 in keep_b1 || keep_b2
| Switch _ -> failwith "switch statements must be removed"
(* handling switch statements correctly would be very difficult; consider that the switch
labels may be located within arbitrarily nested statements within the switch statement's block
TODO: are switch statements always removed by goblint/CIL? *)
(* TODO: block and stmt list in Switch: each stmt in list points to the first statement for a case, filtering twice seems silly, and is probably not even correct!
Instead, we should filter the block, and then pick out the stmt for each case. *)
(* | Switch (e, b, stmts, l1, l2) -> *)
(* let keep_b = impl_block b in
let stmts' = List.filter impl_stmt stmts in
Switch (e, b, stmts', l1, l2), keep_b || stmts' <> [] *)
| Loop (b, _, _, _, _) as sk ->
sk, impl_block b
| Block b as sk ->
sk, impl_block b
| sk -> sk, true
in
stmt.skind <- skind';
keep
in
impl_block block

(* globinfo: the type of globals between which we want to track dependencies *)

type globinfo =
| GTypeInfo of (typeinfo [@equal (==)] [@hash Hashtbl.hash])
| GCompInfo of (compinfo [@equal (==)] [@hash Hashtbl.hash])
| GEnumInfo of (enuminfo [@equal (==)] [@hash Hashtbl.hash])
| GVarInfo of (varinfo [@equal (==)] [@hash Hashtbl.hash])
[@@deriving eq, hash]

let pretty_globinfo () = let open Pretty in function
| GTypeInfo ti -> text "GTypeInfo " ++ text ti.tname
| GCompInfo ci -> text "GCompInfo " ++ text ci.cname
| GEnumInfo ei -> text "GEnumInfo " ++ text ei.ename
| GVarInfo vi -> text "GVarInfo " ++ text vi.vname

module GlobinfoH =
Hashtbl.Make
(struct
type t = globinfo
let equal = equal_globinfo
let hash = hash_globinfo
end)

let globinfo_of_global = function
| GType (ti, _) -> Some (GTypeInfo ti)
| GCompTag (ci, _) | GCompTagDecl (ci, _) -> Some (GCompInfo ci)
| GEnumTag (ei, _) | GEnumTagDecl (ei, _) -> Some (GEnumInfo ei)
| GVarDecl (vi, _) | GVar (vi, _, _) | GFun ({ svar = vi; _ }, _) -> Some (GVarInfo vi)
| _ -> None

class globalReferenceTrackerVisitor = object (self)
inherit Cil.nopCilVisitor (* as nop *)

(** map of globals to the set of globals they reference *)
val glob_refs : (unit GlobinfoH.t) GlobinfoH.t = GlobinfoH.create 17

method get_references_raw () = glob_refs
method get_references () = GlobinfoH.to_seq glob_refs |> Seq.map (fun (k, v) -> k, GlobinfoH.to_seq_keys v)

(** context is the global we are currently iterating within *)
val context : global option ref = ref None

(** mark [glob_from] as referencing [glob_to] *)
method private add_ref glob_from glob_to =
let open GlobinfoH in
let ref_set =
match find_opt glob_refs glob_from with
| None -> create 3
| Some s -> s
in
replace ref_set glob_to ();
replace glob_refs glob_from ref_set

method private ctx_add_ref glob_to =
Option.bind !context globinfo_of_global
|> Option.iter (fun ctx -> self#add_ref ctx glob_to)

(* TODO: is the typeinfo in a global traversed? looks like yes *)
method! vglob g =
(* upon entering a new global, update the context *)
context := Some g;
DoChildren

method! vvrbl vi =
(* if variable is global, add reference from current context *)
if vi.vglob then self#ctx_add_ref (GVarInfo vi);
DoChildren

method! vtype t =
(match t with
| TNamed (ti, _) -> self#ctx_add_ref @@ GTypeInfo ti
| TComp (ci, _) -> self#ctx_add_ref @@ GCompInfo ci
| TEnum (ei, _) -> self#ctx_add_ref @@ GEnumInfo ei
| _ -> ());
DoChildren

end


let find_live_globinfo (live_from : global Seq.t) (references : globinfo -> globinfo Seq.t) =
let live = GlobinfoH.create 103 in
let rec impl = function
| [] -> ()
| gi :: gis ->
GlobinfoH.replace live gi ();
let new_refs =
references gi
|> Seq.filter (fun rgi -> not (GlobinfoH.mem live rgi))
|> List.of_seq
in
impl (List.rev_append new_refs gis)
match stmt.skind with
| If (_, b1, b2, _, _) ->
(* be careful to not short-circuit, since call to impl_block b2 is always needed for side-effects *)
let keep_b1, keep_b2 = impl_block b1, impl_block b2 in keep_b1 || keep_b2
| Switch _ -> failwith "switch statements must be removed"
(* handling switch statements correctly would be very difficult; consider that the switch
labels may be located within arbitrarily nested statements within the switch statement's block *)
| Loop (b, _, _, _, _) ->
impl_block b
| Block b ->
impl_block b
| sk -> true
in
impl (live_from |> Seq.filter_map globinfo_of_global |> List.of_seq);
live

let find_live_globinfo' live_from result =
find_live_globinfo
live_from
(fun gi ->
GlobinfoH.find_opt result gi
|> Option.to_seq
|> Seq.concat_map GlobinfoH.to_seq_keys)
impl_block block


module RemoveDeadCode : Transform.S = struct
Expand All @@ -161,75 +40,31 @@ module RemoveDeadCode : Transform.S = struct
(* whether a statement (might) still be live, and should therefore be kept *)
let stmt_live = Cilfacade0.get_stmtLoc %> loc_live in

(* let stmt_live stmt =
let loc = Cilfacade0.get_stmtLoc stmt in
let llive = loc_live loc in
dpf "stmt=%a loc=%a result=%b" dn_stmt stmt d_loc loc llive;
llive *)
(*
match stmtkind_location stmt.skind with
| Some loc -> loc_live loc
| None -> true *)

(* whether a global function (might) still be live, and should therefore be kept *)
let fundec_live (fd : fundec) = not @@ (ask @@ fd.svar.vdecl).f Queries.MustBeUncalled in

(* step 1: remove statements found to be dead *)
Cil.iterGlobals file
(function
| GFun (fd, _) -> filter_map_block stmt_live fd.sbody |> ignore
(* pf "global name=%s" fd.svar.vname;
let keep = in
pf "keep=%b" keep; *) (* TODO: use keep? discard function if keep is false. should not be necessary, function should be dead already *)
| GFun (fd, _) ->
(* invariants of filter_map_block satisfied: switch statements removed by CFG transform,
and a live label implies its target is live *)
filter_map_block stmt_live fd.sbody |> ignore
| _ -> ());

let global_live ~non_functions_live = function
| GFun (fd, _) -> let fdl = fundec_live fd in dpf "%s live=%b" fd.svar.vname fdl; fdl
| _ -> non_functions_live
in

if true then (
let open GoblintCil.Rmtmps in
(* dpf "using cil to remove dead globals, keepUnused=%b" !keepUnused; *)
let keepUnused0 = !keepUnused in
Fun.protect ~finally:(fun () -> keepUnused := keepUnused0) (fun () ->
keepUnused := false;
removeUnusedTemps (* ~isRoot:isCompleteProgramRoot *) ~isRoot:(global_live ~non_functions_live:false) file
)
(* let open GoblintCil in
let open Rmtmps in
Rmtmps.clearReferencedBits file;
Cfg.cfgFun |> ignore *)
(* GoblintCil.Cfg.clearFileCFG file;
GoblintCil.Cfg.clearCFGinfo *)
(* step 2: remove globals that are (transitively) unreferenced by live functions
- dead functions: removed by answering 'false' for isRoot
- unreferenced globals and types: removeUnusedTemps keeps only globals referenced by live functions *)
let open GoblintCil.Rmtmps in
let keepUnused0 = !keepUnused in
Fun.protect ~finally:(fun () -> keepUnused := keepUnused0) (fun () ->
keepUnused := false;
removeUnusedTemps ~isRoot:(function GFun (fd, _) -> fundec_live fd | _ -> false) file
)
else (
print_endline "using custom code to remove dead globals";

(* step 2: remove function globals found to be dead *)
file.globals <- List.filter (global_live ~non_functions_live:true) file.globals;

(* step 3: track dependencies between globals *)
let refsVisitor = new globalReferenceTrackerVisitor in
Cil.visitCilFileSameGlobals (refsVisitor :> Cil.cilVisitor) file;

(* step 4: find globals referenced by remaining (live) functions and remove them *)
let live_globinfo =
find_live_globinfo'
(file.globals |> List.to_seq |> Seq.filter (function GFun _ -> true | _ -> false))
(refsVisitor#get_references_raw ())
in
file.globals <-
List.filter
(fun g -> match globinfo_of_global g with
| Some gi -> GlobinfoH.mem live_globinfo gi
| None -> true (* dependencies for some types of globals (e.g. assembly) are not tracked, always keep them *)
)
file.globals
)
let requires_file_output = true

end

(* change name from remove_dead_code -> dead_code (?) *)
(* TODO: change name from remove_dead_code -> dead_code (?) *)
let _ = Transform.register "remove_dead_code" (module RemoveDeadCode)

0 comments on commit 5ad50bb

Please sign in to comment.