diff --git a/sledge/cli/sledge_cli.ml b/sledge/cli/sledge_cli.ml index e5d2d8b9f..79943fdac 100644 --- a/sledge/cli/sledge_cli.ml +++ b/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) ; diff --git a/sledge/src/control.ml b/sledge/src/control.ml index 679e3e491..5beed0529 100644 --- a/sledge/src/control.ml +++ b/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 diff --git a/sledge/src/control.mli b/sledge/src/control.mli index 17b5070fc..275010a1f 100644 --- a/sledge/src/control.mli +++ b/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 :