[sledge] Parameterize Control.Make over the scheduler queue

Summary: Preparation for allowing a choice among several scheduler strategies.

Reviewed By: jvillard

Differential Revision: D27828759

fbshipit-source-id: 63d6ec203

sledge/cli/sledge_cli.ml

@@ -82,7 +82,9 @@ let used_globals pgm entry_points preanalyze : Domain_intf.used_globals =
       let entry_points = entry_points
       let globals = Domain_intf.Declared Llair.Global.Set.empty
     end in
-    let module Analysis = Control.Make (Opts) (Domain_used_globals) in
+    let module Analysis =
+      Control.Make (Opts) (Domain_used_globals) (Control.PriorityQueue)
+    in
     let summary_table = Analysis.compute_summaries pgm in
     Per_function
       (Llair.Function.Map.map summary_table ~f:Llair.Global.Set.union_list)
@@ -141,7 +143,8 @@ let analyze =
       | `unit -> (module Domain_unit)
     in
     let module Dom = (val dom) in
-    let module Analysis = Control.Make (Opts) (Dom) in
+    let module Analysis = Control.Make (Opts) (Dom) (Control.PriorityQueue)
+    in
     Domain_sh.simplify_states := not no_simplify_states ;
     Option.iter dump_query ~f:(fun n -> Solver.dump_query := n) ;
     at_exit (fun () -> Report.coverage pgm) ;

sledge/src/control.ml

@@ -9,13 +9,15 @@
 
     The analysis' semantics of control flow. *)
 
-module PriorityQueue (Elt : sig
+module type Elt = sig
   type t [@@deriving compare, equal, sexp_of]
 
   val pp : t pp
   val joinable : t -> t -> bool
-end) : sig
-  type elt = Elt.t
+end
+
+module type QueueS = sig
+  type elt
 
   (** a "queue" of elements, which need not be FIFO *)
   type t
@@ -33,7 +35,11 @@ end) : sig
       where [e] is the selected element in [q], [es] are other elements in
       [q] with the same destination as [e], and [q'] is [q] without [e] and
       [es]. *)
-end = struct
+end
+
+module type Queue = functor (Elt : Elt) -> QueueS with type elt = Elt.t
+
+module PriorityQueue (Elt : Elt) : QueueS with type elt = Elt.t = struct
   type elt = Elt.t
 
   module Elts = Set.Make (Elt)
@@ -68,7 +74,11 @@ end = struct
       Some (top, elts, {queue; removed})
 end
 
-module Make (Opts : Domain_intf.Opts) (Dom : Domain_intf.Dom) = struct
+module Make
+    (Opts : Domain_intf.Opts)
+    (Dom : Domain_intf.Dom)
+    (Queue : Queue) =
+struct
   module Stack : sig
     type t
 
@@ -245,7 +255,7 @@ module Make (Opts : Domain_intf.Opts) (Dom : Domain_intf.Dom) = struct
       let joinable x y = Llair.Block.equal x.edge.dst y.edge.dst
     end
 
-    module Queue = PriorityQueue (Elt)
+    module Queue = Queue (Elt)
 
     let enqueue depth edge state depths queue =
       [%Trace.info

sledge/src/control.mli

@@ -7,7 +7,11 @@
 
 (** The analysis' semantics of control flow. *)
 
-module Make (_ : Domain_intf.Opts) (Dom : Domain_intf.Dom) : sig
+module type Queue
+
+module PriorityQueue : Queue
+
+module Make (_ : Domain_intf.Opts) (Dom : Domain_intf.Dom) (_ : Queue) : sig
   val exec_pgm : Llair.program -> unit
 
   val compute_summaries :