From 4920cce2f332dd7f7d34916a2b4c8d2caa9b2910 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Wed, 21 Apr 2021 15:36:01 -0700
Subject: [PATCH] [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 | 4 +++-
 sledge/sledge-help.txt   | 6 ++++--
 sledge/src/control.ml    | 5 +++--
 3 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/sledge/cli/sledge_cli.ml b/sledge/cli/sledge_cli.ml
index db17a42a4..727e3ac71 100644
--- a/sledge/cli/sledge_cli.ml
+++ b/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)"
diff --git a/sledge/sledge-help.txt b/sledge/sledge-help.txt
index 572265648..9823090bb 100644
--- a/sledge/sledge-help.txt
+++ b/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),
diff --git a/sledge/src/control.ml b/sledge/src/control.ml
index c13933b85..0963f8872 100644
--- a/sledge/src/control.ml
+++ b/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