From 716c2070951d87c6d79096e1c2b525cdbe1295a9 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 21 Apr 2021 15:35:49 -0700 Subject: [PATCH] [sledge] Move analysis config options from Domain_intf to Control_intf Summary: The configuration options for the analysis are used only/principally in Control, they do not belong in the interface of domains. Also, the definition of the used_globals type for the results of the used globals pre-analysis belongs to the Domain_used_globals module. Reviewed By: jvillard Differential Revision: D27828752 fbshipit-source-id: e42de74e0 --- sledge/cli/sledge_cli.ml | 19 +++++++++-------- sledge/src/control.ml | 34 +++++++++++++++--------------- sledge/src/control.mli | 4 +++- sledge/src/control_intf.ml | 20 ++++++++++++++++++ sledge/src/domain_intf.ml | 18 ---------------- sledge/src/domain_used_globals.ml | 6 +++++- sledge/src/domain_used_globals.mli | 8 ++++++- 7 files changed, 62 insertions(+), 47 deletions(-) create mode 100644 sledge/src/control_intf.ml diff --git a/sledge/cli/sledge_cli.ml b/sledge/cli/sledge_cli.ml index 79943fdac..22dab1b87 100644 --- a/sledge/cli/sledge_cli.ml +++ b/sledge/cli/sledge_cli.ml @@ -74,22 +74,22 @@ let unmarshal file () = let entry_points = Config.find_list "entry-points" -let used_globals pgm entry_points preanalyze : Domain_intf.used_globals = +let used_globals pgm entry_points preanalyze = + let module UG = Domain_used_globals in if preanalyze then - let module Opts = struct + let module Config = struct let bound = 1 let function_summaries = true let entry_points = entry_points - let globals = Domain_intf.Declared Llair.Global.Set.empty + let globals = UG.Declared Llair.Global.Set.empty end in - let module Analysis = - Control.Make (Opts) (Domain_used_globals) (Control.PriorityQueue) + let module Analysis = Control.Make (Config) (UG) (Control.PriorityQueue) in let summary_table = Analysis.compute_summaries pgm in - Per_function + UG.Per_function (Llair.Function.Map.map summary_table ~f:Llair.Global.Set.union_list) else - Declared + UG.Declared (Llair.Global.Set.of_iter (Iter.map ~f:(fun g -> g.name) (IArray.to_iter pgm.globals))) @@ -129,7 +129,7 @@ let analyze = Timer.enabled := stats ; let pgm = program () in let globals = used_globals pgm entry_points preanalyze_globals in - let module Opts = struct + let module Config = struct let bound = bound let function_summaries = function_summaries let entry_points = entry_points @@ -143,7 +143,8 @@ let analyze = | `unit -> (module Domain_unit) in let module Dom = (val dom) in - let module Analysis = Control.Make (Opts) (Dom) (Control.PriorityQueue) + let module Analysis = + Control.Make (Config) (Dom) (Control.PriorityQueue) in Domain_sh.simplify_states := not no_simplify_states ; Option.iter dump_query ~f:(fun n -> Solver.dump_query := n) ; diff --git a/sledge/src/control.ml b/sledge/src/control.ml index 87d1c76d5..1fb3ad56a 100644 --- a/sledge/src/control.ml +++ b/sledge/src/control.ml @@ -9,6 +9,8 @@ The analysis' semantics of control flow. *) +open Control_intf + module type Elt = sig type t [@@deriving compare, equal, sexp_of] @@ -74,10 +76,7 @@ module PriorityQueue (Elt : Elt) : QueueS with type elt = Elt.t = struct Some (top, elts, {queue; removed}) end -module Make - (Opts : Domain_intf.Opts) - (Dom : Domain_intf.Dom) - (Queue : Queue) = +module Make (Config : Config) (Dom : Domain_intf.Dom) (Queue : Queue) = struct module Stack : sig type t @@ -265,7 +264,7 @@ struct let prune depth edge queue = [%Trace.info " %i: %a" depth Edge.pp edge] ; - Report.hit_bound Opts.bound ; + Report.hit_bound Config.bound ; queue let dequeue queue = @@ -289,7 +288,7 @@ struct let edge = {Edge.dst= curr; src= prev; stk} in let depth = Option.value (Depths.find edge depths) ~default:0 in let depth = if retreating then depth + 1 else depth in - if depth <= Opts.bound then enqueue depth edge state depths queue + if depth <= Config.bound then enqueue depth edge state depths queue else prune depth edge queue let init state curr = @@ -336,14 +335,14 @@ struct Llair.Function.pp return.dst.parent.name Dom.pp state] ; let dnf_states = - if Opts.function_summaries then Dom.dnf state else [state] + if Config.function_summaries then Dom.dnf state else [state] in let domain_call = Dom.call ~globals ~actuals ~areturn ~formals ~freturn ~locals in List.fold dnf_states Work.skip ~f:(fun state acc -> match - if not Opts.function_summaries then None + if not Config.function_summaries then None else let state = fst (domain_call ~summaries:false state) in let* summary = Llair.Function.Tbl.find summary_table name in @@ -351,7 +350,7 @@ struct with | None -> let state, from_call = - domain_call ~summaries:Opts.function_summaries state + domain_call ~summaries:Config.function_summaries state in let stk = Stack.push_call call from_call stk in Work.seq acc @@ -371,7 +370,7 @@ struct [%Trace.call fun {pf} -> pf "@ from: %a" Llair.Function.pp name] ; let summarize post_state = - if not Opts.function_summaries then post_state + if not Config.function_summaries then post_state else let function_summary, post_state = Dom.create_summary ~locals ~formals post_state @@ -394,7 +393,7 @@ struct let retn_state = Dom.retn formals freturn from_call post_state in exec_jump stk retn_state block retn_site | None -> - if Opts.function_summaries then + if Config.function_summaries then summarize exit_state |> (ignore : Dom.t -> unit) ; Work.skip ) |> @@ -457,7 +456,7 @@ struct |> Work.seq x ) | Call ({callee} as call) -> exec_call stk state block call - (Domain_used_globals.by_function Opts.globals callee.name) + (Domain_used_globals.by_function Config.globals callee.name) | ICall ({callee; areturn; return} as call) -> ( let lookup name = Llair.Func.find name pgm.functions in match Dom.resolve_callee lookup callee state with @@ -465,7 +464,8 @@ struct | callees -> List.fold callees Work.skip ~f:(fun callee x -> exec_call stk state block {call with callee} - (Domain_used_globals.by_function Opts.globals callee.name) + (Domain_used_globals.by_function Config.globals + callee.name) |> Work.seq x ) ) | Return {exp} -> exec_return stk state block exp | Throw {exc} -> exec_throw stk state block exc @@ -501,12 +501,12 @@ struct let call_entry_point : Llair.program -> Work.t option = fun pgm -> let+ {name; formals; freturn; locals; entry} = - List.find_map Opts.entry_points ~f:(fun entry_point -> + List.find_map Config.entry_points ~f:(fun entry_point -> let* func = Llair.Func.find entry_point pgm.functions in if IArray.is_empty func.formals then Some func else None ) in - let summaries = Opts.function_summaries in - let globals = Domain_used_globals.by_function Opts.globals name in + let summaries = Config.function_summaries in + let globals = Domain_used_globals.by_function Config.globals name in let actuals = IArray.empty in let areturn = None in let state, _ = @@ -522,7 +522,7 @@ struct | None -> fail "no entry point found" () let compute_summaries pgm : Dom.summary list Llair.Function.Map.t = - assert Opts.function_summaries ; + assert Config.function_summaries ; exec_pgm pgm ; Llair.Function.Tbl.fold summary_table Llair.Function.Map.empty ~f:(fun ~key ~data map -> diff --git a/sledge/src/control.mli b/sledge/src/control.mli index 275010a1f..de75bedf4 100644 --- a/sledge/src/control.mli +++ b/sledge/src/control.mli @@ -7,11 +7,13 @@ (** The analysis' semantics of control flow. *) +open Control_intf + module type Queue module PriorityQueue : Queue -module Make (_ : Domain_intf.Opts) (Dom : Domain_intf.Dom) (_ : Queue) : sig +module Make (_ : Config) (Dom : Domain_intf.Dom) (_ : Queue) : sig val exec_pgm : Llair.program -> unit val compute_summaries : diff --git a/sledge/src/control_intf.ml b/sledge/src/control_intf.ml new file mode 100644 index 000000000..852250307 --- /dev/null +++ b/sledge/src/control_intf.ml @@ -0,0 +1,20 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +module type Config = sig + val bound : int + (** Loop/recursion unrolling bound *) + + val function_summaries : bool + (** Use function summarization *) + + val entry_points : string list + (** C linkage names of entry points *) + + val globals : Domain_used_globals.used_globals + (** results of used globals pre-analysis *) +end diff --git a/sledge/src/domain_intf.ml b/sledge/src/domain_intf.ml index d373aab82..27be31f59 100644 --- a/sledge/src/domain_intf.ml +++ b/sledge/src/domain_intf.ml @@ -48,21 +48,3 @@ module type Dom = sig val apply_summary : t -> summary -> t option end - -type used_globals = - | Per_function of Llair.Global.Set.t Llair.Function.Map.t - (** per-function used-globals map *) - | Declared of Llair.Global.Set.t (** program-wide set *) - -module type Opts = sig - val bound : int - (** Loop/recursion unrolling bound *) - - val function_summaries : bool - (** Use function summarization *) - - val entry_points : string list - (** C linkage names of entry points *) - - val globals : used_globals -end diff --git a/sledge/src/domain_used_globals.ml b/sledge/src/domain_used_globals.ml index 016624e19..fcecfb7b6 100644 --- a/sledge/src/domain_used_globals.ml +++ b/sledge/src/domain_used_globals.ml @@ -62,7 +62,11 @@ let apply_summary st summ = Some (Llair.Global.Set.union st summ) (** Query *) -let by_function : Domain_intf.used_globals -> Llair.Function.t -> t = +type used_globals = + | Per_function of summary Llair.Function.Map.t + | Declared of summary + +let by_function : used_globals -> Llair.Function.t -> t = fun s fn -> [%Trace.call fun {pf} -> pf "@ %a" Llair.Function.pp fn] ; diff --git a/sledge/src/domain_used_globals.mli b/sledge/src/domain_used_globals.mli index ace20ab8e..18da2a916 100644 --- a/sledge/src/domain_used_globals.mli +++ b/sledge/src/domain_used_globals.mli @@ -9,4 +9,10 @@ include Domain_intf.Dom with type summary = Llair.Global.Set.t -val by_function : Domain_intf.used_globals -> Llair.Function.t -> summary +type used_globals = + | Per_function of Llair.Global.Set.t Llair.Function.Map.t + (** map of functions to globals they or their callees use *) + | Declared of Llair.Global.Set.t + (** set of declared globals used in the program *) + +val by_function : used_globals -> Llair.Function.t -> summary