From e44827b892b77b6910ba73c18883e8842f783687 Mon Sep 17 00:00:00 2001 From: Benno Stein Date: Wed, 25 Sep 2019 08:03:28 -0700 Subject: [PATCH] [sledge] Add option to apply used-globals as pre-analysis Summary: This diff adds a "-prenalyze-globals" flag to all analyze targets which, when set, computes used-globals sets for all reachable functions and then uses that information to track only relevant global variables at calls in the main analysis. Reviewed By: jberdine, jvillard Differential Revision: D17526746 fbshipit-source-id: 1a114285c --- sledge/sledge-help.txt | 3 + sledge/src/control.ml | 100 +++++++++++++++++++--------- sledge/src/control.mli | 6 +- sledge/src/domain/domain_sig.ml | 4 +- sledge/src/domain/relation.ml | 26 +++----- sledge/src/domain/unit.ml | 2 +- sledge/src/domain/used_globals.ml | 2 +- sledge/src/domain/used_globals.mli | 2 +- sledge/src/llair/exp.ml | 1 + sledge/src/llair/exp.mli | 1 + sledge/src/sledge.ml | 23 ++++++- sledge/src/symbheap/state_domain.ml | 12 +--- 12 files changed, 118 insertions(+), 64 deletions(-) diff --git a/sledge/sledge-help.txt b/sledge/sledge-help.txt index 5eab72cf4..8739ca57b 100644 --- a/sledge/sledge-help.txt +++ b/sledge/sledge-help.txt @@ -56,6 +56,7 @@ Analyze code in a buck target. This is a convenience wrapper for the sequence `s [-margin ] wrap debug tracing at columns [-modules ] write list of bitcode files to , or to standard output if is `-` + [-preanalyze-globals] pre-analyze global variables used by each function [-skip-throw] do not explore past throwing an exception [-trace ] enable debug tracing [-help] print this help text and exit @@ -136,6 +137,7 @@ Analyze code in one or more LLVM bitcode files. This is a convenience wrapper fo [-fuzzer] add a harness for libFuzzer targets [-llair-output ] write generated LLAIR to [-margin ] wrap debug tracing at columns + [-preanalyze-globals] pre-analyze global variables used by each function [-skip-throw] do not explore past throwing an exception [-trace ] enable debug tracing [-help] print this help text and exit @@ -178,6 +180,7 @@ The file must be binary LLAIR, such as produced by `sledge translate`. or "unit" (unit domain) [-function-summaries] use function summaries (in development) [-margin ] wrap debug tracing at columns + [-preanalyze-globals] pre-analyze global variables used by each function [-skip-throw] do not explore past throwing an exception [-trace ] enable debug tracing [-help] print this help text and exit diff --git a/sledge/src/control.ml b/sledge/src/control.ml index a428af6de..3dad80fe5 100644 --- a/sledge/src/control.ml +++ b/sledge/src/control.ml @@ -9,7 +9,12 @@ The analysis' semantics of control flow. *) -type exec_opts = {bound: int; skip_throw: bool; function_summaries: bool} +type exec_opts = + { bound: int + ; skip_throw: bool + ; function_summaries: bool + ; globals: [`Per_function of Var.Set.t Var.Map.t | `Declared of Var.Set.t] + } module Make (Dom : Domain_sig.Dom) = struct module Stack : sig @@ -237,6 +242,23 @@ module Make (Dom : Domain_sig.Dom) = struct | None -> [%Trace.info "queue empty"] ; () end + let used_globals : exec_opts -> Var.var -> Var.Set.t = + fun opts fn -> + [%Trace.call fun {pf} -> pf "%a" Var.pp fn] + ; + ( match opts.globals with + | `Declared set -> set + | `Per_function map -> ( + match Map.find map fn with + | Some gs -> gs + | None -> + fail + "main analysis reached function %a that was not reached by \ + used-globals pre-analysis " + Var.pp fn () ) ) + |> + [%Trace.retn fun {pf} r -> pf "%a" Var.Set.pp r] + let exec_jump stk state block Llair.{dst; retreating} = Work.add ~prev:block ~retreating stk state dst @@ -253,7 +275,8 @@ module Make (Dom : Domain_sig.Dom) = struct if opts.function_summaries then Dom.dnf state else [state] in let domain_call = - Dom.call args areturn params (Set.add_option freturn locals) globals + Dom.call ~globals args areturn params + ~locals:(Set.add_option freturn locals) in List.fold ~init:Work.skip dnf_states ~f:(fun acc state -> match @@ -295,40 +318,44 @@ module Make (Dom : Domain_sig.Dom) = struct (List.pp "@," Dom.pp_summary) data ) )] - let exec_return ~opts stk pre_state (block : Llair.block) exp globals = + let exec_return ~opts stk pre_state (block : Llair.block) exp = let Llair.{name; params; freturn; locals} = block.parent in [%Trace.call fun {pf} -> pf "from %a with pre_state %a" Var.pp name.var Dom.pp pre_state] ; + let summarize post_state = + if opts.function_summaries then ( + let globals = used_globals opts name.var in + let function_summary, post_state = + Dom.create_summary ~locals post_state + ~formals:(Set.union (Var.Set.of_list params) globals) + in + Hashtbl.add_multi summary_table ~key:name.var ~data:function_summary ; + pp_st () ; + post_state ) + else post_state + in + let exit_state = + match (freturn, exp) with + | Some freturn, Some return_val -> + Dom.exec_move pre_state freturn return_val + | None, None -> pre_state + | _ -> violates Llair.Func.invariant block.parent + in ( match Stack.pop_return stk with | Some (from_call, retn_site, stk) -> - let exit_state = - match (freturn, exp) with - | Some freturn, Some return_val -> - Dom.exec_move pre_state freturn return_val - | None, None -> pre_state - | _ -> violates Llair.Func.invariant block.parent - in - let post_state = Dom.post locals from_call exit_state in - let post_state = - if opts.function_summaries then ( - let globals = - Var.Set.of_vector - (Vector.map globals ~f:(fun (g : Global.t) -> g.var)) - in - let function_summary, post_state = - Dom.create_summary ~locals post_state - ~formals:(Set.union (Var.Set.of_list params) globals) - in - Hashtbl.add_multi summary_table ~key:name.var - ~data:function_summary ; - pp_st () ; - post_state ) - else post_state - in + let post_state = summarize (Dom.post locals from_call exit_state) in let retn_state = Dom.retn params freturn from_call post_state in exec_jump stk retn_state block retn_site - | None -> Work.skip ) + | None -> + (* Create and store a function summary for main *) + if + opts.function_summaries + && List.exists + (Config.find_list "entry-points") + ~f:(String.equal (Var.name name.var)) + then summarize exit_state |> (ignore : Dom.t -> unit) ; + Work.skip ) |> [%Trace.retn fun {pf} _ -> pf ""] @@ -419,9 +446,9 @@ module Make (Dom : Domain_sig.Dom) = struct exec_skip_func stk state block areturn return | None -> exec_call opts stk state block {call with callee} - pgm.globals ) + (used_globals opts callee.name.var) ) |> Work.seq x ) ) - | Return {exp} -> exec_return ~opts stk state block exp pgm.globals + | Return {exp} -> exec_return ~opts stk state block exp | Throw {exc} -> if opts.skip_throw then Work.skip else exec_throw stk state block exc @@ -449,12 +476,13 @@ module Make (Dom : Domain_sig.Dom) = struct List.find_map entry_points ~f:(fun name -> Llair.Func.find pgm.functions (Var.program ~global:() name) ) |> function - | Some {locals; params= []; entry} -> + | Some {name= {var}; locals; params= []; entry} -> Some (Work.init (fst - (Dom.call ~summaries:opts.function_summaries [] None [] - locals pgm.globals (Dom.init pgm.globals))) + (Dom.call ~summaries:opts.function_summaries + ~globals:(used_globals opts var) [] None [] ~locals + (Dom.init pgm.globals))) entry) | _ -> None @@ -467,4 +495,10 @@ module Make (Dom : Domain_sig.Dom) = struct | None -> fail "no applicable harness" () ) |> [%Trace.retn fun {pf} _ -> pf ""] + + let compute_summaries opts pgm : Dom.summary list Var.Map.t = + assert opts.function_summaries ; + exec_pgm opts pgm ; + Hashtbl.fold summary_table ~init:Var.Map.empty ~f:(fun ~key ~data map -> + match data with [] -> map | _ -> Map.set map ~key ~data ) end diff --git a/sledge/src/control.mli b/sledge/src/control.mli index 5ab2d6f4d..f7e1543bc 100644 --- a/sledge/src/control.mli +++ b/sledge/src/control.mli @@ -10,8 +10,12 @@ type exec_opts = { bound: int (** Loop/recursion unrolling bound *) ; skip_throw: bool (** Treat throw as unreachable *) - ; function_summaries: bool (** Use function summarisation *) } + ; function_summaries: bool (** Use function summarisation *) + ; globals: [`Per_function of Var.Set.t Var.Map.t | `Declared of Var.Set.t] + (** Either a per-function used-globals map or a program-wide set *) + } module Make (Dom : Domain_sig.Dom) : sig val exec_pgm : exec_opts -> Llair.t -> unit + val compute_summaries : exec_opts -> Llair.t -> Dom.summary list Var.Map.t end diff --git a/sledge/src/domain/domain_sig.ml b/sledge/src/domain/domain_sig.ml index 90894d8bf..a38400c25 100644 --- a/sledge/src/domain/domain_sig.ml +++ b/sledge/src/domain/domain_sig.ml @@ -31,11 +31,11 @@ module type Dom = sig val call : summaries:bool + -> globals:Var.Set.t -> Exp.t list -> Var.t option -> Var.t list - -> Var.Set.t - -> Global.t vector + -> locals:Var.Set.t -> t -> t * from_call diff --git a/sledge/src/domain/relation.ml b/sledge/src/domain/relation.ml index 6e7d68485..bb644f667 100644 --- a/sledge/src/domain/relation.ml +++ b/sledge/src/domain/relation.ml @@ -69,26 +69,22 @@ module Make (State_domain : State_domain_sig) = struct let recursion_beyond_bound = State_domain.recursion_beyond_bound - let call ~summaries actuals areturn formals locals globals_vec + let call ~summaries ~globals actuals areturn formals ~locals (entry, current) = - let globals = - Var.Set.of_vector - (Vector.map globals_vec ~f:(fun (g : Global.t) -> g.var)) - in - ([%Trace.call fun {pf} -> - pf - "@[@[actuals: (@[%a@])@ formals: (@[%a@])@]@ locals: {@[%a@]}@ \ - globals: {@[%a@]}@ current: %a@]" - (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Var.pp) - (List.rev formals) Var.Set.pp locals Var.Set.pp globals - State_domain.pp current] + [%Trace.call fun {pf} -> + pf + "@[@[actuals: (@[%a@])@ formals: (@[%a@])@]@ locals: {@[%a@]}@ \ + globals: {@[%a@]}@ current: %a@]" + (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Var.pp) + (List.rev formals) Var.Set.pp locals Var.Set.pp globals + State_domain.pp current] ; let caller_current, state_from_call = - State_domain.call ~summaries actuals areturn formals locals - globals_vec current + State_domain.call ~summaries ~globals actuals areturn formals ~locals + current in ( (caller_current, caller_current) - , {state_from_call; caller_entry= entry} )) + , {state_from_call; caller_entry= entry} ) |> [%Trace.retn fun {pf} (reln, _) -> pf "@,%a" pp reln] diff --git a/sledge/src/domain/unit.ml b/sledge/src/domain/unit.ml index 990932a8b..eaf392374 100644 --- a/sledge/src/domain/unit.ml +++ b/sledge/src/domain/unit.ml @@ -22,7 +22,7 @@ let exec_intrinsic ~skip_throw:_ _ _ _ _ : (t, unit) result option = None type from_call = unit [@@deriving compare, equal, sexp] -let call ~summaries:_ _ _ _ _ _ _ = ((), ()) +let call ~summaries:_ ~globals:_ _ _ _ ~locals:_ _ = ((), ()) let recursion_beyond_bound = `skip let post _ _ () = () let retn _ _ _ _ = () diff --git a/sledge/src/domain/used_globals.ml b/sledge/src/domain/used_globals.ml index ce7abffed..a6f78f34e 100644 --- a/sledge/src/domain/used_globals.ml +++ b/sledge/src/domain/used_globals.ml @@ -61,7 +61,7 @@ let exec_intrinsic ~skip_throw:_ st _ intrinsic actuals = type from_call = t [@@deriving sexp_of] (* Set abstract state to bottom (i.e. empty set) at function entry *) -let call ~summaries:_ actuals _ _ _ _ st = +let call ~summaries:_ ~globals:_ actuals _ _ ~locals:_ st = (empty, List.fold actuals ~init:st ~f:(fun s a -> used_globals ~init:s a)) let resolve_callee lookup ptr st = diff --git a/sledge/src/domain/used_globals.mli b/sledge/src/domain/used_globals.mli index bf5b74ca9..c20d91544 100644 --- a/sledge/src/domain/used_globals.mli +++ b/sledge/src/domain/used_globals.mli @@ -7,4 +7,4 @@ (** Used-globals abstract domain *) -include Domain_sig.Dom +include Domain_sig.Dom with type summary = Var.Set.t diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml index 4c49e811f..7bbcd7766 100644 --- a/sledge/src/llair/exp.ml +++ b/sledge/src/llair/exp.ml @@ -527,6 +527,7 @@ module Var = struct let empty = Set.empty (module T) let of_option = Option.fold ~f:Set.add ~init:empty let of_list = Set.of_list (module T) + let union_list = Set.union_list (module T) let of_vector = Set.of_vector (module T) end diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli index 7b76d1b4b..d65546bce 100644 --- a/sledge/src/llair/exp.mli +++ b/sledge/src/llair/exp.mli @@ -97,6 +97,7 @@ module Var : sig val empty : t val of_option : var option -> t val of_list : var list -> t + val union_list : t list -> t val of_vector : var vector -> t end diff --git a/sledge/src/sledge.ml b/sledge/src/sledge.ml index 8e8d2e34e..c38360a76 100644 --- a/sledge/src/sledge.ml +++ b/sledge/src/sledge.ml @@ -68,6 +68,22 @@ let unmarshal file () = ~f:(fun ic -> (Marshal.from_channel ic : Llair.t)) file +let used_globals pgm preanalyze = + if preanalyze then + let summary_table = + Used_globals_executor.compute_summaries + { bound= 1 + ; skip_throw= false + ; function_summaries= true + ; globals= `Declared Var.Set.empty } + pgm + in + `Per_function (Map.map summary_table ~f:Var.Set.union_list) + else + `Declared + (Vector.fold pgm.globals ~init:Var.Set.empty ~f:(fun acc g -> + Set.add acc g.var )) + let analyze = let%map_open bound = flag "bound" @@ -79,6 +95,9 @@ let analyze = and function_summaries = flag "function-summaries" no_arg ~doc:"use function summaries (in development)" + and preanalyze_globals = + flag "preanalyze-globals" no_arg + ~doc:"pre-analyze global variables used by each function" and exec = flag "domain" (optional_with_default Sh_executor.exec_pgm @@ -92,7 +111,9 @@ let analyze = \"unit\" (unit domain)" in fun program () -> - exec {bound; skip_throw; function_summaries} (program ()) + let pgm = program () in + let globals = used_globals pgm preanalyze_globals in + exec {bound; skip_throw; function_summaries; globals} pgm let analyze_cmd = let summary = "analyze LLAIR code" in diff --git a/sledge/src/symbheap/state_domain.ml b/sledge/src/symbheap/state_domain.ml index 7749970c4..783fbede5 100644 --- a/sledge/src/symbheap/state_domain.ml +++ b/sledge/src/symbheap/state_domain.ml @@ -74,15 +74,13 @@ type from_call = {areturn: Var.t option; subst: Var.Subst.t; frame: Sh.t} (** Express formula in terms of formals instead of actuals, and enter scope of locals: rename formals to fresh vars in formula and actuals, add equations between each formal and actual, and quantify fresh vars. *) -let call ~summaries actuals areturn formals locals globals_vec q = +let call ~summaries ~globals actuals areturn formals ~locals q = [%Trace.call fun {pf} -> pf "@[actuals: (@[%a@])@ formals: (@[%a@])@ locals: {@[%a@]}@ \ globals: {@[%a@]}@ q: %a@]" (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Var.pp) - (List.rev formals) Var.Set.pp locals - (Vector.pp ",@ " Llair_.Global.pp) - globals_vec pp q] + (List.rev formals) Var.Set.pp locals Var.Set.pp globals pp q] ; let q', freshen_locals = Sh.freshen q ~wrt:(Set.add_list formals locals) @@ -101,11 +99,7 @@ let call ~summaries actuals areturn formals locals globals_vec q = else (* Add the formals here to do garbage collection and then get rid of them *) - let formals_set = Var.Set.of_list formals - and globals = - Var.Set.of_vector - (Vector.map globals_vec ~f:(fun (g : Global.t) -> g.var)) - in + let formals_set = Var.Set.of_list formals in let function_summary_pre = garbage_collect q'' ~wrt:(Set.union formals_set globals) in