[sledge] Refactor Used globals analysis results type and query

Summary:
The Used globals (pre-)analysis produces results queried by
Control. This diff adds a type definition for these and moves the
query into the Used_globals module.

Reviewed By: bennostein

Differential Revision: D17856879

fbshipit-source-id: 0211b82d7

sledge/src/control.ml

@@ -13,8 +13,7 @@ type exec_opts =
   { bound: int
   ; skip_throw: bool
   ; function_summaries: bool
-  ; globals: [`Per_function of Reg.Set.t Reg.Map.t | `Declared of Reg.Set.t]
-  }
+  ; globals: Used_globals.r }
 
 module Make (Dom : Domain_sig.Dom) = struct
   module Stack : sig
@@ -248,23 +247,6 @@ module Make (Dom : Domain_sig.Dom) = struct
       | None -> [%Trace.info "queue empty"] ; ()
   end
 
-  let used_globals : exec_opts -> Reg.t -> Reg.Set.t =
-   fun opts fn ->
-    [%Trace.call fun {pf} -> pf "%a" Reg.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 "
-            Reg.pp fn () ) )
-    |>
-    [%Trace.retn fun {pf} r -> pf "%a" Reg.Set.pp r]
-
   let exec_jump stk state block Llair.{dst; retreating} =
     Work.add ~prev:block ~retreating stk state dst
 
@@ -330,7 +312,7 @@ module Make (Dom : Domain_sig.Dom) = struct
     let summarize post_state =
       if not opts.function_summaries then post_state
       else
-        let globals = used_globals opts name.reg in
+        let globals = Used_globals.by_function opts.globals name.reg in
         let function_summary, post_state =
           Dom.create_summary ~locals post_state
             ~formals:(Set.union (Reg.Set.of_list formals) globals)
@@ -452,7 +434,8 @@ 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}
-                      (used_globals opts callee.name.reg) )
+                      (Used_globals.by_function opts.globals callee.name.reg)
+                )
                 |> Work.seq x ) )
     | Return {exp} -> exec_return ~opts stk state block exp
     | Throw {exc} ->
@@ -485,8 +468,8 @@ module Make (Dom : Domain_sig.Dom) = struct
           (Work.init
              (fst
                 (Dom.call ~summaries:opts.function_summaries
-                   ~globals:(used_globals opts reg) ~actuals:[]
-                   ~areturn:None ~formals:[] ~freturn ~locals
+                   ~globals:(Used_globals.by_function opts.globals reg)
+                   ~actuals:[] ~areturn:None ~formals:[] ~freturn ~locals
                    (Dom.init pgm.globals)))
              entry)
     | _ -> None

sledge/src/control.mli

@@ -11,9 +11,7 @@ type exec_opts =
   { bound: int  (** Loop/recursion unrolling bound *)
   ; skip_throw: bool  (** Treat throw as unreachable *)
   ; function_summaries: bool  (** Use function summarisation *)
-  ; globals: [`Per_function of Reg.Set.t Reg.Map.t | `Declared of Reg.Set.t]
-        (** Either a per-function used-globals map or a program-wide set *)
-  }
+  ; globals: Used_globals.r }
 
 module Make (Dom : Domain_sig.Dom) : sig
   val exec_pgm : exec_opts -> Llair.t -> unit

sledge/src/domain/dune.in

@@ -6,7 +6,7 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-let deps = ["import"; "llair_"]
+let deps = ["import"; "trace"; "llair_"]
 
 ;;
 Jbuild_plugin.V1.send

sledge/src/domain/used_globals.ml

@@ -80,3 +80,24 @@ type summary = t
 let pp_summary = pp
 let create_summary ~locals:_ ~formals:_ state = (state, state)
 let apply_summary st summ = Some (Set.union st summ)
+
+(** Query *)
+
+type r = Per_function of Reg.Set.t Reg.Map.t | Declared of Reg.Set.t
+
+let by_function : r -> Reg.t -> t =
+ fun s fn ->
+  [%Trace.call fun {pf} -> pf "%a" Reg.pp fn]
+  ;
+  ( match s 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 "
+          Reg.pp fn () ) )
+  |>
+  [%Trace.retn fun {pf} r -> pf "%a" Reg.Set.pp r]

sledge/src/domain/used_globals.mli

@@ -8,3 +8,10 @@
 (** Used-globals abstract domain *)
 
 include Domain_sig.Dom with type summary = Reg.Set.t
+
+type r =
+  | Per_function of Reg.Set.t Reg.Map.t
+      (** per-function used-globals map *)
+  | Declared of Reg.Set.t  (** program-wide set *)
+
+val by_function : r -> Reg.t -> summary

sledge/src/sledge.ml

@@ -69,19 +69,19 @@ let unmarshal file () =
     ~f:(fun ic -> (Marshal.from_channel ic : Llair.t))
     file
 
-let used_globals pgm preanalyze =
+let used_globals pgm preanalyze : Used_globals.r =
   if preanalyze then
     let summary_table =
       Used_globals_executor.compute_summaries
         { bound= 1
         ; skip_throw= false
         ; function_summaries= true
-        ; globals= `Declared Reg.Set.empty }
+        ; globals= Declared Reg.Set.empty }
         pgm
     in
-    `Per_function (Map.map summary_table ~f:Reg.Set.union_list)
+    Per_function (Map.map summary_table ~f:Reg.Set.union_list)
   else
-    `Declared
+    Declared
       (Vector.fold pgm.globals ~init:Reg.Set.empty ~f:(fun acc g ->
            Set.add acc g.reg ))