[sledge] Change execution options from a record to a module

Summary:
Currently the symbolic execution options, obtained from the command
line flags and preanalysis, are passed to the Control entry points as
a record, and then passed around within Control as needed. This diff
simplifies the code in Control by replacing the record mechanism with
an additional functor parameter containing the options. The main
benefit is that the bound option no longer needs to be part of the
analysis state.

This change does make the code in Sledge_cli slightly more
complicated, as it now performs a functor application using a
first-class module computed from the command line flags.

Reviewed By: jvillard

Differential Revision: D25196735

fbshipit-source-id: 80e5d5d62

sledge/cli/sledge_cli.ml

@@ -12,11 +12,6 @@ open Command.Let_syntax
 
 type 'a param = 'a Command.Param.t
 
-module Sh_executor = Control.Make (Domain_relation.Make (Domain_sh))
-module Unit_executor = Control.Make (Domain_unit)
-module Used_globals_executor = Control.Make (Domain_used_globals)
-module Itv_executor = Control.Make (Domain_itv)
-
 (* reverse application in the Command.Param applicative *)
 let ( |*> ) : 'a param -> ('a -> 'b) param -> 'b param =
  fun x f -> x |> Command.Param.apply f
@@ -78,16 +73,16 @@ let unmarshal file () =
 
 let entry_points = Config.find_list "entry-points"
 
-let used_globals pgm preanalyze : Domain_used_globals.r =
+let used_globals pgm entry_points preanalyze : Domain_intf.used_globals =
   if preanalyze then
-    let summary_table =
-      Used_globals_executor.compute_summaries
-        { bound= 1
-        ; function_summaries= true
-        ; entry_points
-        ; globals= Declared Llair.Global.Set.empty }
-        pgm
-    in
+    let module Opts = struct
+      let bound = 1
+      let function_summaries = true
+      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 summary_table = Analysis.compute_summaries pgm in
     Per_function
       (Llair.Function.Map.map summary_table ~f:Llair.Global.Set.union_list)
   else
@@ -106,14 +101,14 @@ let analyze =
   and preanalyze_globals =
     flag "preanalyze-globals" no_arg
       ~doc:"pre-analyze global variables used by each function"
-  and exec =
+  and domain =
     flag "domain"
-      (optional_with_default Sh_executor.exec_pgm
+      (optional_with_default `sh
          (Arg_type.of_alist_exn
-            [ ("sh", Sh_executor.exec_pgm)
-            ; ("globals", Used_globals_executor.exec_pgm)
-            ; ("unit", Unit_executor.exec_pgm)
-            ; ("itv", Itv_executor.exec_pgm) ]))
+            [ ("sh", `sh)
+            ; ("globals", `globals)
+            ; ("itv", `itv)
+            ; ("unit", `unit) ]))
       ~doc:
         "<string> select abstract domain; must be one of \"sh\" (default, \
          symbolic heap domain), \"globals\" (used-globals domain), or \
@@ -125,11 +120,26 @@ let analyze =
     flag "stats" no_arg ~doc:"output performance statistics to stderr"
   in
   fun program () ->
+    Timer.enabled := stats ;
     let pgm = program () in
-    let globals = used_globals pgm preanalyze_globals in
+    let globals = used_globals pgm entry_points preanalyze_globals in
+    let module Opts = struct
+      let bound = bound
+      let function_summaries = function_summaries
+      let entry_points = entry_points
+      let globals = globals
+    end in
+    let dom : (module Domain_intf.Dom) =
+      match domain with
+      | `sh -> (module Domain_relation.Make (Domain_sh))
+      | `globals -> (module Domain_used_globals)
+      | `itv -> (module Domain_itv)
+      | `unit -> (module Domain_unit)
+    in
+    let module Dom = (val dom) in
+    let module Analysis = Control.Make (Opts) (Dom) in
     Domain_sh.simplify_states := not no_simplify_states ;
-    Timer.enabled := stats ;
-    exec {bound; function_summaries; entry_points; globals} pgm ;
+    Analysis.exec_pgm pgm ;
     Report.coverage pgm ;
     Report.safe_or_unsafe ()
 

sledge/src/control.ml

@@ -9,13 +9,7 @@
 
     The analysis' semantics of control flow. *)
 
-type exec_opts =
-  { bound: int
-  ; function_summaries: bool
-  ; entry_points: string list
-  ; globals: Domain_used_globals.r }
-
-module Make (Dom : Domain_intf.Dom) = struct
+module Make (Opts : Domain_intf.Opts) (Dom : Domain_intf.Dom) = struct
   module Stack : sig
     type t
 
@@ -24,10 +18,7 @@ module Make (Dom : Domain_intf.Dom) = struct
     type as_inlined_location = t [@@deriving compare, sexp_of]
 
     val empty : t
-
-    val push_call :
-      Llair.func Llair.call -> bound:int -> Dom.from_call -> t -> t option
-
+    val push_call : Llair.func Llair.call -> Dom.from_call -> t -> t option
     val pop_return : t -> (Dom.from_call * Llair.jump * t) option
 
     val pop_throw :
@@ -107,7 +98,7 @@ module Make (Dom : Domain_intf.Dom) = struct
       (match jmp with None -> stk | Some jmp -> Throw (jmp, stk))
       |> check invariant
 
-    let push_call (Llair.{return; throw} as call) ~bound from_call stk =
+    let push_call (Llair.{return; throw} as call) from_call stk =
       [%Trace.call fun {pf} -> pf "%a" pp stk]
       ;
       let rec count_f_in_stack acc f = function
@@ -118,7 +109,7 @@ module Make (Dom : Domain_intf.Dom) = struct
         | _ -> acc
       in
       let n = count_f_in_stack 0 return stk in
-      ( if n > bound then (
+      ( if n > Opts.bound then (
         Report.hit_bound n ;
         None )
       else Some (push_throw throw (push_return call from_call stk)) )
@@ -146,7 +137,7 @@ module Make (Dom : Domain_intf.Dom) = struct
   module Work : sig
     type t
 
-    val init : Dom.t -> Llair.block -> int -> t
+    val init : Dom.t -> Llair.block -> t
 
     type x
 
@@ -264,32 +255,32 @@ module Make (Dom : Domain_intf.Dom) = struct
           Some (top, elts, {queue; removed})
     end
 
-    type t = PrioQueue.t * int
+    type t = PrioQueue.t
     type x = Depths.t -> t -> t
 
     let skip _ w = w
     let seq x y d w = y d (x d w)
 
-    let add ?prev ~retreating stk state curr depths (queue, bound) =
+    let add ?prev ~retreating stk state curr depths queue =
       let edge = {Edge.dst= curr; src= prev; stk} in
       let depth = Option.value (Depths.find edge depths) ~default:0 in
       let depth = if retreating then depth + 1 else depth in
-      if depth <= bound then (
+      if depth <= Opts.bound then (
         [%Trace.info
           "@[<6>enqueue %i: %a [%a]@ | %a@]" depth Edge.pp edge Stack.pp
             edge.stk PrioQueue.pp queue] ;
         let depths = Depths.add ~key:edge ~data:depth depths in
-        (PrioQueue.add {depth; edge; state; depths} queue, bound) )
+        PrioQueue.add {depth; edge; state; depths} queue )
       else (
         [%Trace.info "prune: %i: %a" depth Edge.pp edge] ;
-        Report.hit_bound bound ;
-        (queue, bound) )
+        Report.hit_bound Opts.bound ;
+        queue )
 
-    let init state curr bound =
+    let init state curr =
       add ~retreating:false Stack.empty state curr Depths.empty
-        (PrioQueue.create (), bound)
+        (PrioQueue.create ())
 
-    let rec run ~f (queue, bound) =
+    let rec run ~f queue =
       match PrioQueue.pop queue with
       | Some ({depth; edge; state; depths}, elts, queue) ->
           [%Trace.info
@@ -305,7 +296,7 @@ module Make (Dom : Domain_intf.Dom) = struct
                     (state, depths, queue)
                 | None -> (state, depths, queue) )
           in
-          run ~f (f edge.stk state edge.dst depths (queue, bound))
+          run ~f (f edge.stk state edge.dst depths queue)
       | None ->
           [%Trace.info "queue empty"] ;
           ()
@@ -316,7 +307,7 @@ module Make (Dom : Domain_intf.Dom) = struct
 
   let summary_table = Llair.Function.Tbl.create ()
 
-  let exec_call opts stk state block call globals =
+  let exec_call stk state block call globals =
     let Llair.{callee; actuals; areturn; return; recursive} = call in
     let Llair.{name; formals; freturn; locals; entry} = callee in
     [%Trace.call fun {pf} ->
@@ -324,14 +315,14 @@ module Make (Dom : Domain_intf.Dom) = struct
         Llair.Function.pp return.dst.parent.name Dom.pp state]
     ;
     let dnf_states =
-      if opts.function_summaries then Dom.dnf state else [state]
+      if Opts.function_summaries then Dom.dnf state else [state]
     in
     let domain_call =
       Dom.call ~globals ~actuals ~areturn ~formals ~freturn ~locals
     in
     List.fold dnf_states Work.skip ~f:(fun state acc ->
         match
-          if not opts.function_summaries then None
+          if not Opts.function_summaries then None
           else
             let maybe_summary_post =
               let state = fst (domain_call ~summaries:false state) in
@@ -345,12 +336,10 @@ module Make (Dom : Domain_intf.Dom) = struct
         with
         | None ->
             let state, from_call =
-              domain_call ~summaries:opts.function_summaries state
+              domain_call ~summaries:Opts.function_summaries state
             in
             Work.seq acc
-              ( match
-                  Stack.push_call call ~bound:opts.bound from_call stk
-                with
+              ( match Stack.push_call call from_call stk with
               | Some stk ->
                   Work.add stk ~prev:block ~retreating:recursive state entry
               | None -> (
@@ -373,11 +362,11 @@ module Make (Dom : Domain_intf.Dom) = struct
     let state = Option.fold ~f:Dom.exec_kill areturn state in
     exec_jump stk state block return
 
-  let exec_call opts stk state block
-      ({Llair.callee; areturn; return; _} as call) globals =
+  let exec_call stk state block ({Llair.callee; areturn; return; _} as call)
+      globals =
     if Llair.Func.is_undefined callee then
       exec_skip_func stk state block areturn return
-    else exec_call opts stk state block call globals
+    else exec_call stk state block call globals
 
   let pp_st () =
     [%Trace.printf
@@ -387,12 +376,12 @@ module Make (Dom : Domain_intf.Dom) = struct
                 (List.pp "@," Dom.pp_summary)
                 data ) )]
 
-  let exec_return ~opts stk pre_state (block : Llair.block) exp =
+  let exec_return stk pre_state (block : Llair.block) exp =
     let Llair.{name; formals; freturn; locals} = block.parent in
     [%Trace.call fun {pf} -> pf "from: %a" Llair.Function.pp name]
     ;
     let summarize post_state =
-      if not opts.function_summaries then post_state
+      if not Opts.function_summaries then post_state
       else
         let function_summary, post_state =
           Dom.create_summary ~locals ~formals post_state
@@ -417,10 +406,10 @@ module Make (Dom : Domain_intf.Dom) = struct
     | None ->
         (* Create and store a function summary for main *)
         if
-          opts.function_summaries
+          Opts.function_summaries
           && List.mem ~eq:String.equal
                (Llair.Function.name name)
-               opts.entry_points
+               Opts.entry_points
         then summarize exit_state |> (ignore : Dom.t -> unit) ;
         Work.skip )
     |>
@@ -449,14 +438,9 @@ module Make (Dom : Domain_intf.Dom) = struct
     |>
     [%Trace.retn fun {pf} _ -> pf ""]
 
-  let exec_term :
-         exec_opts
-      -> Llair.program
-      -> Stack.t
-      -> Dom.t
-      -> Llair.block
-      -> Work.x =
-   fun opts pgm stk state block ->
+  let exec_term : Llair.program -> Stack.t -> Dom.t -> Llair.block -> Work.x
+      =
+   fun pgm stk state block ->
     [%Trace.info
       "@[<2>exec term@\n@[%a@]@\n%a@]" Dom.pp state Llair.Term.pp block.term] ;
     Report.step_term block.term ;
@@ -487,18 +471,18 @@ module Make (Dom : Domain_intf.Dom) = struct
             | Some state -> exec_jump stk state block jump |> Work.seq x
             | None -> x )
     | Call ({callee} as call) ->
-        exec_call opts stk state block call
-          (Domain_used_globals.by_function opts.globals callee.name)
+        exec_call stk state block call
+          (Domain_used_globals.by_function Opts.globals callee.name)
     | ICall ({callee; areturn; return} as call) -> (
         let lookup name = Llair.Func.find name pgm.functions in
         match Dom.resolve_callee lookup callee state with
         | [] -> exec_skip_func stk state block areturn return
         | callees ->
             List.fold callees Work.skip ~f:(fun callee x ->
-                exec_call opts stk state block {call with callee}
-                  (Domain_used_globals.by_function opts.globals callee.name)
+                exec_call stk state block {call with callee}
+                  (Domain_used_globals.by_function Opts.globals callee.name)
                 |> Work.seq x ) )
-    | Return {exp} -> exec_return ~opts stk state block exp
+    | Return {exp} -> exec_return stk state block exp
     | Throw {exc} -> exec_throw stk state block exc
     | Unreachable -> Work.skip
 
@@ -513,13 +497,8 @@ module Make (Dom : Domain_intf.Dom) = struct
     | Some state -> Result.Ok state | None -> Result.Error (state, inst)
 
   let exec_block :
-         exec_opts
-      -> Llair.program
-      -> Stack.t
-      -> Dom.t
-      -> Llair.block
-      -> Work.x =
-   fun opts pgm stk state block ->
+      Llair.program -> Stack.t -> Dom.t -> Llair.block -> Work.x =
+   fun pgm stk state block ->
     [%trace]
       ~call:(fun {pf} ->
         pf "#%i %%%s in %a" block.sort_index block.lbl Llair.Function.pp
@@ -531,39 +510,39 @@ module Make (Dom : Domain_intf.Dom) = struct
     match
       Iter.fold_result ~f:exec_inst (IArray.to_iter block.cmnd) state
     with
-    | Ok state -> exec_term opts pgm stk state block
+    | Ok state -> exec_term pgm stk state block
     | Error (state, inst) ->
         Report.invalid_access_inst (Dom.report_fmt_thunk state) inst ;
         Work.skip
 
-  let harness : exec_opts -> Llair.program -> (int -> Work.t) option =
-   fun opts pgm ->
+  let harness : Llair.program -> Work.t option =
+   fun pgm ->
     List.find_map
       ~f:(fun entry_point -> Llair.Func.find entry_point pgm.functions)
-      opts.entry_points
+      Opts.entry_points
     |> function
     | Some {name; formals; freturn; locals; entry}
       when IArray.is_empty formals ->
         Some
           (Work.init
              (fst
-                (Dom.call ~summaries:opts.function_summaries
+                (Dom.call ~summaries:Opts.function_summaries
                    ~globals:
-                     (Domain_used_globals.by_function opts.globals name)
+                     (Domain_used_globals.by_function Opts.globals name)
                    ~actuals:IArray.empty ~areturn:None ~formals:IArray.empty
                    ~freturn ~locals (Dom.init pgm.globals)))
              entry)
     | _ -> None
 
-  let exec_pgm : exec_opts -> Llair.program -> unit =
-   fun opts pgm ->
-    match harness opts pgm with
-    | Some work -> Work.run ~f:(exec_block opts pgm) (work opts.bound)
+  let exec_pgm : Llair.program -> unit =
+   fun pgm ->
+    match harness pgm with
+    | Some work -> Work.run ~f:(exec_block pgm) work
     | None -> fail "no applicable harness" ()
 
-  let compute_summaries opts pgm : Dom.summary list Llair.Function.Map.t =
-    assert opts.function_summaries ;
-    exec_pgm opts pgm ;
+  let compute_summaries pgm : Dom.summary list Llair.Function.Map.t =
+    assert Opts.function_summaries ;
+    exec_pgm pgm ;
     Llair.Function.Tbl.fold summary_table Llair.Function.Map.empty
       ~f:(fun ~key ~data map ->
         match data with

sledge/src/control.mli

@@ -7,15 +7,9 @@
 
 (** The analysis' semantics of control flow. *)
 
-type exec_opts =
-  { bound: int  (** Loop/recursion unrolling bound *)
-  ; function_summaries: bool  (** Use function summarisation *)
-  ; entry_points: string list  (** C linkage names of entry points *)
-  ; globals: Domain_used_globals.r }
-
-module Make (Dom : Domain_intf.Dom) : sig
-  val exec_pgm : exec_opts -> Llair.program -> unit
+module Make (_ : Domain_intf.Opts) (Dom : Domain_intf.Dom) : sig
+  val exec_pgm : Llair.program -> unit
 
   val compute_summaries :
-    exec_opts -> Llair.program -> Dom.summary list Llair.Function.Map.t
+    Llair.program -> Dom.summary list Llair.Function.Map.t
 end

sledge/src/domain_intf.ml

@@ -50,3 +50,21 @@ module type Dom = sig
 
   val apply_summary : t -> summary -> t option
 end
+
+type used_globals =
+  | Per_function of Llair.Global.Set.t Llair.Function.Map.t
+      (** per-function used-globals map *)
+  | Declared of Llair.Global.Set.t  (** program-wide set *)
+
+module type Opts = sig
+  val bound : int
+  (** Loop/recursion unrolling bound *)
+
+  val function_summaries : bool
+  (** Use function summarization *)
+
+  val entry_points : string list
+  (** C linkage names of entry points *)
+
+  val globals : used_globals
+end

sledge/src/domain_used_globals.ml

@@ -64,11 +64,7 @@ let apply_summary st summ = Some (Llair.Global.Set.union st summ)
 
 (** Query *)
 
-type r =
-  | Per_function of Llair.Global.Set.t Llair.Function.Map.t
-  | Declared of Llair.Global.Set.t
-
-let by_function : r -> Llair.Function.t -> t =
+let by_function : Domain_intf.used_globals -> Llair.Function.t -> t =
  fun s fn ->
   [%Trace.call fun {pf} -> pf "%a" Llair.Function.pp fn]
   ;

sledge/src/domain_used_globals.mli

@@ -9,9 +9,4 @@
 
 include Domain_intf.Dom with type summary = Llair.Global.Set.t
 
-type r =
-  | Per_function of Llair.Global.Set.t Llair.Function.Map.t
-      (** per-function used-globals map *)
-  | Declared of Llair.Global.Set.t  (** program-wide set *)
-
-val by_function : r -> Llair.Function.t -> summary
+val by_function : Domain_intf.used_globals -> Llair.Function.t -> summary