[sledge] Add option to skip recursive calls at depth bound

Summary:
While the symbolic heap analysis ends its search upon hitting the
bound on recursion depth, the used-globals analysis should instead
simply skip recursive calls beyond the depth. Note that this is
unsound for arbitrary abstract domains, however, and the flag
controlling this feature should be used with caution.

Note that procedure calls are still not handled correctly, since
Used_globals.exec_intrinsic does not properly check whether callees
are intrinsic.  A forthcoming commit will fix that, as well.

Reviewed By: jberdine

Differential Revision: D17479753

fbshipit-source-id: aa92e0ef3

sledge/src/control.ml

@@ -246,7 +246,8 @@ module Make (Dom : Domain_sig.Dom) = struct
     let Llair.{callee; args; areturn; return; recursive} = call in
     let Llair.{name; params; freturn; locals; entry} = callee in
     [%Trace.call fun {pf} ->
-      pf "%a from %a" Var.pp name.var Var.pp return.dst.parent.name.var]
+      pf "%a from %a with state %a" Var.pp name.var Var.pp
+        return.dst.parent.name.var Dom.pp state]
     ;
     let dnf_states =
       if opts.function_summaries then Dom.dnf state else [state]
@@ -278,7 +279,10 @@ module Make (Dom : Domain_sig.Dom) = struct
                 with
               | Some stk ->
                   Work.add stk ~prev:block ~retreating:recursive state entry
-              | None -> Work.skip )
+              | None -> (
+                match Dom.recursion_beyond_bound with
+                | `skip -> Work.seq acc (exec_jump stk state block return)
+                | `prune -> Work.skip ) )
         | Some post -> Work.seq acc (exec_jump stk post block return) )
     |>
     [%Trace.retn fun {pf} _ -> pf ""]
@@ -293,7 +297,8 @@ module Make (Dom : Domain_sig.Dom) = struct
 
   let exec_return ~opts stk pre_state (block : Llair.block) exp globals =
     let Llair.{name; params; freturn; locals} = block.parent in
-    [%Trace.call fun {pf} -> pf "from %a" Var.pp name.var]
+    [%Trace.call fun {pf} ->
+      pf "from %a with pre_state %a" Var.pp name.var Dom.pp pre_state]
     ;
     ( match Stack.pop_return stk with
     | Some (from_call, retn_site, stk) ->

sledge/src/domain/domain_sig.ml

@@ -39,6 +39,7 @@ module type Dom = sig
     -> t
     -> t * from_call
 
+  val recursion_beyond_bound : [`skip | `prune]
   val post : Var.Set.t -> from_call -> t -> t
   val retn : Var.t list -> Var.t option -> from_call -> t -> t
   val dnf : t -> t list

sledge/src/domain/relation.ml

@@ -67,6 +67,8 @@ module Make (State_domain : State_domain_sig) = struct
     {state_from_call: State_domain.from_call; caller_entry: State_domain.t}
   [@@deriving sexp_of]
 
+  let recursion_beyond_bound = State_domain.recursion_beyond_bound
+
   let call ~summaries actuals areturn formals locals globals_vec
       (entry, current) =
     let globals =

sledge/src/domain/unit.ml

@@ -23,6 +23,7 @@ let exec_intrinsic ~skip_throw:_ _ _ _ _ : (t, unit) result option = None
 type from_call = unit [@@deriving compare, equal, sexp]
 
 let call ~summaries:_ _ _ _ _ _ _ = ((), ())
+let recursion_beyond_bound = `skip
 let post _ _ () = ()
 let retn _ _ _ _ = ()
 let dnf () = [()]

sledge/src/domain/used_globals.ml

@@ -19,6 +19,7 @@ let init globals =
   empty
 
 let join = Set.union
+let recursion_beyond_bound = `skip
 let is_false _ = false
 let post _ _ state = state
 let retn _ _ from_call post = Set.union from_call post

sledge/src/symbheap/state_domain.ml

@@ -125,6 +125,8 @@ let call ~summaries actuals areturn formals locals globals_vec q =
     pf "@[<v>subst: %a@ frame: %a@ q': %a@]" Var.Subst.pp subst pp frame pp
       q']
 
+let recursion_beyond_bound = `prune
+
 (** Leave scope of locals: existentially quantify locals. *)
 let post locals _ q =
   [%Trace.call fun {pf} ->

sledge/test/exec/nonreducible_call_graph.c

@@ -0,0 +1,36 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+#include <stdio.h>
+
+char* a = "I'm a string";
+char* b = "I'm a different string";
+char* c = "foo bar";
+char* d = "hello world";
+FILE* file;
+
+void f();
+void g();
+
+int main() {        // accesses: a,b,c,d
+  if (getc(file)) { // nondeterministic
+    f();
+  } else {
+    g();
+  }
+  char* s = a;
+  return 0;
+}
+
+void f() { // accesses: b, c, d
+  char* s1 = b;
+  g();
+  char* s2 = c;
+}
+void g() { // accesses: b, c, d
+  char* s = d;
+  f();
+}