[sledge] Add command line option for execution bound

Summary: Instead of a compile-time constant.

Reviewed By: ngorogiannis

Differential Revision: D15468707

fbshipit-source-id: 0a2668a18

sledge/src/config.ml

@@ -29,7 +29,9 @@ let trace_conv =
   (parse, print)
 
 type t =
-  { compile_only: bool [@aka ["c"]]
+  { bound: int [@aka ["b"]] [@default 1]
+        (** Specify bound on execution exploration *)
+  ; compile_only: bool [@aka ["c"]]
         (** Do not analyze: terminate after translating input LLVM to LLAIR. *)
   ; input: string [@pos 0] [@docv "input.bc"]
         (** LLVM bitcode file to analyze, in either binary $(b,.bc) or
@@ -53,6 +55,6 @@ let run main =
   |> function
   | `Error _ -> Caml.exit 1
   | `Help | `Version -> Caml.exit 0
-  | `Ok {compile_only; input; output; trace} ->
+  | `Ok {bound; compile_only; input; output; trace} ->
       Trace.init ~config:trace () ;
-      main ~input ~output ~compile_only
+      main ~bound ~compile_only ~input ~output

sledge/src/config.mli

@@ -8,7 +8,12 @@
 (** Configuration options *)
 
 val run :
-  (input:string -> output:string option -> compile_only:bool -> 'a) -> 'a
+     (   bound:int
+      -> compile_only:bool
+      -> input:string
+      -> output:string option
+      -> 'a)
+  -> 'a
 (** [run main] parses command line options, performs some imperative
     initialization, and then executes [main] passing the configuration
     options. *)

sledge/src/control.ml

@@ -9,7 +9,7 @@
 
     The analysis' semantics of control flow. *)
 
-let bound = 10
+let bound = ref 1
 
 module Stack : sig
   type t
@@ -217,7 +217,7 @@ end = struct
     let edge = {Edge.dst= curr; src= prev; stk} in
     let depth = Option.value (Depths.find depths edge) ~default:0 in
     let depth = if retreating then depth + 1 else depth in
-    if depth > bound then (
+    if depth > !bound then (
       [%Trace.info "prune: %i: %a" depth Edge.pp edge] ;
       work )
     else
@@ -377,10 +377,11 @@ let harness : Llair.t -> Work.t option =
            block)
   | _ -> None
 
-let exec_pgm : Llair.t -> unit =
- fun pgm ->
+let exec_pgm : bound:int -> Llair.t -> unit =
+ fun ~bound:bnd pgm ->
   [%Trace.call fun {pf} -> pf "@]@,@["]
   ;
+  bound := bnd ;
   ( match harness pgm with
   | Some work -> Work.run ~f:(exec_block pgm) work
   | None -> fail "no applicable harness" () )

sledge/src/control.mli

@@ -7,4 +7,4 @@
 
 (** The analysis' semantics of control flow. *)
 
-val exec_pgm : Llair.t -> unit
+val exec_pgm : bound:int -> Llair.t -> unit

sledge/src/sledge.ml

@@ -7,7 +7,7 @@
 
 (** Sledge executable entry point *)
 
-let main ~input ~output ~compile_only =
+let main ~bound ~compile_only ~input ~output =
   try
     let program =
       if String.is_suffix input ~suffix:".llair" then
@@ -26,7 +26,9 @@ let main ~input ~output ~compile_only =
           Out_channel.with_file filename ~f:(fun oc ->
               let fs = Format.formatter_of_out_channel oc in
               Format.fprintf fs "%a@." Llair.pp program ) ) ;
-    if not compile_only then ( Control.exec_pgm program ; Trace.flush () ) ;
+    if not compile_only then (
+      Control.exec_pgm ~bound program ;
+      Trace.flush () ) ;
     Format.printf "@\nRESULT: Success@."
   with exn ->
     let bt = Caml.Printexc.get_raw_backtrace () in