From 6592eb609f014329fc154ee5861470386528614d Mon Sep 17 00:00:00 2001 From: Benno Stein Date: Fri, 20 Sep 2019 06:27:34 -0700 Subject: [PATCH] [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 | 11 +++++-- sledge/src/domain/domain_sig.ml | 1 + sledge/src/domain/relation.ml | 2 ++ sledge/src/domain/unit.ml | 1 + sledge/src/domain/used_globals.ml | 1 + sledge/src/symbheap/state_domain.ml | 2 ++ sledge/test/exec/nonreducible_call_graph.c | 36 ++++++++++++++++++++++ 7 files changed, 51 insertions(+), 3 deletions(-) create mode 100644 sledge/test/exec/nonreducible_call_graph.c diff --git a/sledge/src/control.ml b/sledge/src/control.ml index bd6961623..a428af6de 100644 --- a/sledge/src/control.ml +++ b/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) -> diff --git a/sledge/src/domain/domain_sig.ml b/sledge/src/domain/domain_sig.ml index a645dcdde..90894d8bf 100644 --- a/sledge/src/domain/domain_sig.ml +++ b/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 diff --git a/sledge/src/domain/relation.ml b/sledge/src/domain/relation.ml index 2834c38a4..6e7d68485 100644 --- a/sledge/src/domain/relation.ml +++ b/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 = diff --git a/sledge/src/domain/unit.ml b/sledge/src/domain/unit.ml index 660c1fe21..990932a8b 100644 --- a/sledge/src/domain/unit.ml +++ b/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 () = [()] diff --git a/sledge/src/domain/used_globals.ml b/sledge/src/domain/used_globals.ml index 68e7f3966..c2fb0413a 100644 --- a/sledge/src/domain/used_globals.ml +++ b/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 diff --git a/sledge/src/symbheap/state_domain.ml b/sledge/src/symbheap/state_domain.ml index 5024c005a..7749970c4 100644 --- a/sledge/src/symbheap/state_domain.ml +++ b/sledge/src/symbheap/state_domain.ml @@ -125,6 +125,8 @@ let call ~summaries actuals areturn formals locals globals_vec q = pf "@[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} -> diff --git a/sledge/test/exec/nonreducible_call_graph.c b/sledge/test/exec/nonreducible_call_graph.c new file mode 100644 index 000000000..b64dbf504 --- /dev/null +++ b/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 + +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(); +}