From 8e09e86295e58d2ffd12c332a72da13ec24a2ed3 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 12 Nov 2020 16:38:49 -0800 Subject: [PATCH] [sledge] Creating summaries does not require the globals Summary: Localizing the entry of a procedure needs the globals (that the procedure uses), but later creating a summary does not. Reviewed By: jvillard Differential Revision: D24886570 fbshipit-source-id: 8a7b18c58 --- sledge/cli/domain_itv.ml | 2 +- sledge/src/control.ml | 3 +-- sledge/src/domain_intf.ml | 6 +----- sledge/src/domain_relation.ml | 7 +++---- sledge/src/domain_relation.mli | 3 +-- sledge/src/domain_sh.ml | 4 +--- sledge/src/domain_sh.mli | 3 +-- sledge/src/domain_unit.ml | 2 +- sledge/src/domain_used_globals.ml | 2 +- 9 files changed, 11 insertions(+), 21 deletions(-) diff --git a/sledge/cli/domain_itv.ml b/sledge/cli/domain_itv.ml index e13e0a591..2871f7329 100644 --- a/sledge/cli/domain_itv.ml +++ b/sledge/cli/domain_itv.ml @@ -311,4 +311,4 @@ type summary = t let pp_summary = pp let apply_summary _ _ = None -let create_summary ~globals:_ ~locals:_ ~formals:_ q = (q, q) +let create_summary ~locals:_ ~formals:_ q = (q, q) diff --git a/sledge/src/control.ml b/sledge/src/control.ml index 6adaa14ca..1a1af2d76 100644 --- a/sledge/src/control.ml +++ b/sledge/src/control.ml @@ -320,9 +320,8 @@ module Make (Dom : Domain_intf.Dom) = struct let summarize post_state = if not opts.function_summaries then post_state else - let globals = Domain_used_globals.by_function opts.globals name in let function_summary, post_state = - Dom.create_summary ~globals ~locals ~formals post_state + Dom.create_summary ~locals ~formals post_state in Llair.Function.Tbl.add_multi ~key:name ~data:function_summary summary_table ; diff --git a/sledge/src/domain_intf.ml b/sledge/src/domain_intf.ml index 0e24692f7..b403e369a 100644 --- a/sledge/src/domain_intf.ml +++ b/sledge/src/domain_intf.ml @@ -57,11 +57,7 @@ module type Dom = sig val pp_summary : summary pp val create_summary : - globals:Llair.Global.Set.t - -> locals:Llair.Reg.Set.t - -> formals:Llair.Reg.t list - -> t - -> summary * t + locals:Llair.Reg.Set.t -> formals:Llair.Reg.t list -> t -> summary * t val apply_summary : t -> summary -> t option end diff --git a/sledge/src/domain_relation.ml b/sledge/src/domain_relation.ml index c28bcbf72..94702c3a2 100644 --- a/sledge/src/domain_relation.ml +++ b/sledge/src/domain_relation.ml @@ -12,8 +12,7 @@ module type State_domain_sig = sig include Domain_intf.Dom val create_summary : - globals:Llair.Global.Set.t - -> locals:Llair.Reg.Set.t + locals:Llair.Reg.Set.t -> formals:Llair.Reg.t list -> entry:t -> current:t @@ -117,9 +116,9 @@ module Make (State_domain : State_domain_sig) = struct let pp_summary = State_domain.pp_summary - let create_summary ~globals ~locals ~formals (entry, current) = + let create_summary ~locals ~formals (entry, current) = let fs, next = - State_domain.create_summary ~globals ~locals ~formals ~entry ~current + State_domain.create_summary ~locals ~formals ~entry ~current in (fs, (entry, next)) diff --git a/sledge/src/domain_relation.mli b/sledge/src/domain_relation.mli index 0f1af3326..e48f08586 100644 --- a/sledge/src/domain_relation.mli +++ b/sledge/src/domain_relation.mli @@ -12,8 +12,7 @@ module type State_domain_sig = sig include Domain_intf.Dom val create_summary : - globals:Llair.Global.Set.t - -> locals:Llair.Reg.Set.t + locals:Llair.Reg.Set.t -> formals:Llair.Reg.t list -> entry:t -> current:t diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml index 452fa2f70..57de85232 100644 --- a/sledge/src/domain_sh.ml +++ b/sledge/src/domain_sh.ml @@ -244,17 +244,15 @@ let pp_summary fs {xs; foot; post} = Format.fprintf fs "@[xs: @[%a@]@ foot: %a@ post: %a @]" Var.Set.pp xs pp foot pp post -let create_summary ~globals ~locals ~formals ~entry ~current:(post : Sh.t) = +let create_summary ~locals ~formals ~entry ~current:(post : Sh.t) = [%Trace.call fun {pf} -> pf "formals %a@ entry: %a@ current: %a" (List.pp ",@ " Llair.Reg.pp) formals pp entry pp post] ; - let globals = X.globals globals in let formals = Var.Set.of_iter (Iter.map ~f:X.reg (List.to_iter formals)) in - let formals = Var.Set.union formals globals in let locals = X.regs locals in let foot = Sh.exists locals entry in let foot, subst = Sh.freshen ~wrt:(Var.Set.union foot.us post.us) foot in diff --git a/sledge/src/domain_sh.mli b/sledge/src/domain_sh.mli index 70249f754..aa99c8b39 100644 --- a/sledge/src/domain_sh.mli +++ b/sledge/src/domain_sh.mli @@ -10,8 +10,7 @@ include Domain_intf.Dom val create_summary : - globals:Llair.Global.Set.t - -> locals:Llair.Reg.Set.t + locals:Llair.Reg.Set.t -> formals:Llair.Reg.t list -> entry:t -> current:t diff --git a/sledge/src/domain_unit.ml b/sledge/src/domain_unit.ml index c8f6aeacd..5d0ffb849 100644 --- a/sledge/src/domain_unit.ml +++ b/sledge/src/domain_unit.ml @@ -39,5 +39,5 @@ let resolve_callee lookup ptr _ = type summary = unit let pp_summary fs () = Format.pp_print_string fs "()" -let create_summary ~globals:_ ~locals:_ ~formals:_ _ = ((), ()) +let create_summary ~locals:_ ~formals:_ _ = ((), ()) let apply_summary _ _ = Some () diff --git a/sledge/src/domain_used_globals.ml b/sledge/src/domain_used_globals.ml index 58accca28..1e23b9f4b 100644 --- a/sledge/src/domain_used_globals.ml +++ b/sledge/src/domain_used_globals.ml @@ -91,7 +91,7 @@ let resolve_callee lookup ptr st = type summary = t let pp_summary = pp -let create_summary ~globals:_ ~locals:_ ~formals:_ state = (state, state) +let create_summary ~locals:_ ~formals:_ state = (state, state) let apply_summary st summ = Some (Llair.Global.Set.union st summ) (** Query *)