[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

@@ -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)

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 ;

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

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))
 

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

sledge/src/domain_sh.ml

@@ -244,17 +244,15 @@ let pp_summary fs {xs; foot; post} =
   Format.fprintf fs "@[<v>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

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

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 ()

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 *)