[sledge] Add entry-points config to Control.exec_opts

Reviewed By: jvillard

Differential Revision: D20322873

fbshipit-source-id: 338657b34

sledge/src/control.ml

@@ -13,6 +13,7 @@ type exec_opts =
   { bound: int
   ; skip_throw: bool
   ; function_summaries: bool
+  ; entry_points: string list
   ; globals: Used_globals.r }
 
 module Make (Dom : Domain_sig.Dom) = struct
@@ -337,8 +338,7 @@ module Make (Dom : Domain_sig.Dom) = struct
         (* Create and store a function summary for main *)
         if
           opts.function_summaries
-          && List.exists
+          && List.exists opts.entry_points
-               (Config.find_list "entry-points")
                ~f:(String.equal (Reg.name name.reg))
         then summarize exit_state |> (ignore : Dom.t -> unit) ;
         Work.skip )
@@ -463,8 +463,7 @@ module Make (Dom : Domain_sig.Dom) = struct
 
   let harness : exec_opts -> Llair.t -> (int -> Work.t) option =
    fun opts pgm ->
-    let entry_points = Config.find_list "entry-points" in
+    List.find_map ~f:(Llair.Func.find pgm.functions) opts.entry_points
-    List.find_map ~f:(Llair.Func.find pgm.functions) entry_points
     |> function
     | Some {name= {reg}; formals= []; freturn; locals; entry} ->
         Some

sledge/src/control.mli

@@ -11,6 +11,7 @@ type exec_opts =
   { bound: int  (** Loop/recursion unrolling bound *)
   ; skip_throw: bool  (** Treat throw as unreachable *)
   ; function_summaries: bool  (** Use function summarisation *)
+  ; entry_points: string list
   ; globals: Used_globals.r }
 
 module Make (Dom : Domain_sig.Dom) : sig

sledge/src/sledge.ml

@@ -77,6 +77,7 @@ let used_globals pgm preanalyze : Used_globals.r =
         { bound= 1
         ; skip_throw= false
         ; function_summaries= true
+        ; entry_points= Config.find_list "entry-points"
         ; globals= Declared Reg.Set.empty }
         pgm
     in
@@ -119,9 +120,10 @@ let analyze =
   fun program () ->
     let pgm = program () in
     let globals = used_globals pgm preanalyze_globals in
+    let entry_points = Config.find_list "entry-points" in
     let skip_throw = not exceptions in
     Sh_domain.simplify_states := not no_simplify_states ;
-    exec {bound; skip_throw; function_summaries; globals} pgm
+    exec {bound; skip_throw; function_summaries; entry_points; globals} pgm
 
 let analyze_cmd =
   let summary = "analyze LLAIR code" in