From 86f550317f21bdf59139fbdbf2e2ced3ab11e574 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 29 Jul 2020 09:14:32 -0700 Subject: [PATCH] [pulse] avoid explosion of disjuncts in large nodes Summary: This avoids wasting potentially large amount of work in some pathological situations. Suppose `foo()` has D specs/disjuncts in its Pulse summary, and consider a node that calls `foo()` N times, starting with just one disjunct: ``` [x] foo() [x1, ..., xD] foo() [y1, ..., yD^2] foo() ... ``` At the end we get `D^N` disjuncts. Except, currently (before this diff), we prune the number of disjuncts to the limit L at each step, so really what happens is that we (very) quickly reach the L limit, then perform `L*D` work at each step (where we take "apply one pre/post pair to the current state" to be one unit of work), thus doing `O(L*D*n)` amount of work. Instead, this diff counts how many disjuncts we get after each instruction is executed, and we already reched the limit L then doesn't bother accumulating more disjuncts (as they'd get discarded any way), and crucially also doesn't bother executing the current instruction on these extra disjuncts. This means we only do `O(L*n)` work now, which is exactly how we expect pulse to scale: execute each instruction (in loop-free code) at most L times. This helps with new arithmetic domains that are more expensive and exhibit huge slowdowns without this diff but no slowdown with this diff (at least on a few examples). Reviewed By: skcho Differential Revision: D22815241 fbshipit-source-id: ce9928e7c --- infer/src/absint/AbstractInterpreter.ml | 23 +++++++++++++++++------ 1 file changed, 17 insertions(+), 6 deletions(-) diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index 904f94d0e..38bdcb42b 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -186,12 +186,23 @@ struct let exec_instr pre_disjuncts analysis_data node instr = List.foldi pre_disjuncts ~init:[] ~f:(fun i post_disjuncts pre_disjunct -> - L.d_printfln "@[Executing instruction from disjunct #%d@;" i ; - let disjuncts' = T.exec_instr pre_disjunct analysis_data node instr in - ( if Config.write_html then - let n = List.length disjuncts' in - L.d_printfln "@]@\n@[Got %d disjunct%s back@]" n (if Int.equal n 1 then "" else "s") ) ; - Domain.join post_disjuncts disjuncts' ) + let should_skip = + match DConfig.join_policy with + | `NeverJoin -> + false + | `UnderApproximateAfter n -> + List.length post_disjuncts >= n + in + if should_skip then ( + L.d_printfln "@[Reached max disjuncts limit, skipping disjunct #%d@;@]" i ; + post_disjuncts ) + else ( + L.d_printfln "@[Executing instruction from disjunct #%d@;" i ; + let disjuncts' = T.exec_instr pre_disjunct analysis_data node instr in + ( if Config.write_html then + let n = List.length disjuncts' in + L.d_printfln "@]@\n@[Got %d disjunct%s back@]" n (if Int.equal n 1 then "" else "s") ) ; + Domain.join post_disjuncts disjuncts' ) ) let exec_node_instrs old_state_opt ~exec_instr pre instrs =