[sledge] Interpret negative bounds as unbounded

Summary:
With this diff, passing `sledge -b -1` performs an unbounded
exploration.

Reviewed By: jvillard

Differential Revision: D27828758

fbshipit-source-id: 0a396308f

sledge/cli/sledge_cli.ml

@@ -97,7 +97,9 @@ let analyze =
   let%map_open bound =
     flag "bound"
       (optional_with_default 1 int)
-      ~doc:"<int> stop execution exploration at depth <int>"
+      ~doc:
+        "<int> stop execution exploration at depth <int>, a negative bound \
+         is never hit and leads to unbounded exploration"
   and function_summaries =
     flag "function-summaries" no_arg
       ~doc:"use function summaries (in development)"

sledge/sledge-help.txt

@@ -107,7 +107,8 @@ Analyze code in one or more LLVM bitcode files. This is a convenience wrapper fo
 === flags ===
 
   [-append-report]       append to report file
-  [-bound <int>]         stop execution exploration at depth <int>
+  [-bound <int>]         stop execution exploration at depth <int>, a negative
+                         bound is never hit and leads to unbounded exploration
   [-colors]              enable printing in colors
   [-domain <string>]     select abstract domain; must be one of "sh" (default,
                          symbolic heap domain), "globals" (used-globals domain),
@@ -186,7 +187,8 @@ The <input> file must be binary LLAIR, such as produced by `sledge translate`.
 === flags ===
 
   [-append-report]       append to report file
-  [-bound <int>]         stop execution exploration at depth <int>
+  [-bound <int>]         stop execution exploration at depth <int>, a negative
+                         bound is never hit and leads to unbounded exploration
   [-colors]              enable printing in colors
   [-domain <string>]     select abstract domain; must be one of "sh" (default,
                          symbolic heap domain), "globals" (used-globals domain),

sledge/src/control.ml

@@ -288,8 +288,9 @@ module Make (Config : Config) (D : Domain) (Queue : Queue) = struct
       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 <= Config.bound then enqueue depth edge state depths queue
-      else prune depth edge queue
+      if 0 <= Config.bound && Config.bound < depth then
+        prune depth edge queue
+      else enqueue depth edge state depths queue
 
     let init state curr =
       add ~retreating:false Stack.empty state curr Depths.empty