From 577d4679da88203f802696e81b9a5b1590f063c8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Wed, 29 Jul 2020 23:26:30 -0700 Subject: [PATCH] [absint][pulse] Remove NeverJoin Summary: There used to be `JoinAfter n` mode where we would try to join `n` states instead of always making disjunctions. It got deleted in D14258485 and Pulse's underlying (pre-disjuncts) domain doesn't even have a join operation. `NeverJoin` mode is not useful in Pulse anymore: pulse will diverge or OOM if we don't limit the number of disjuncts. It is also not used by any other analyzer. Let's remove it. Reviewed By: jvillard Differential Revision: D22817425 fbshipit-source-id: 1e658f11d --- infer/src/absint/AbstractInterpreter.ml | 9 +++------ infer/src/absint/TransferFunctions.ml | 2 +- infer/src/absint/TransferFunctions.mli | 3 +-- infer/src/pulse/Pulse.ml | 4 +--- 4 files changed, 6 insertions(+), 12 deletions(-) diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index 38bdcb42b..1b23f524b 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -132,12 +132,9 @@ struct fun lhs rhs -> if phys_equal lhs rhs then lhs else - match DConfig.join_policy with - | `NeverJoin -> - List.rev_append rhs lhs - | `UnderApproximateAfter n -> - let lhs_length = List.length lhs in - if lhs_length >= n then lhs else list_rev_append rhs lhs (n - lhs_length) + let (`UnderApproximateAfter n) = DConfig.join_policy in + let lhs_length = List.length lhs in + if lhs_length >= n then lhs else list_rev_append rhs lhs (n - lhs_length) (** check if elements of [disj] appear in [of_] in the same order, using pointer equality on diff --git a/infer/src/absint/TransferFunctions.ml b/infer/src/absint/TransferFunctions.ml index 6f79c860d..954197c7c 100644 --- a/infer/src/absint/TransferFunctions.ml +++ b/infer/src/absint/TransferFunctions.ml @@ -34,7 +34,7 @@ module type MakeHIL = functor (C : ProcCfg.S) -> sig end module type DisjunctiveConfig = sig - val join_policy : [`UnderApproximateAfter of int | `NeverJoin] + val join_policy : [`UnderApproximateAfter of int] val widen_policy : [`UnderApproximateAfterNumIterations of int] end diff --git a/infer/src/absint/TransferFunctions.mli b/infer/src/absint/TransferFunctions.mli index 6c99c7805..e6482f508 100644 --- a/infer/src/absint/TransferFunctions.mli +++ b/infer/src/absint/TransferFunctions.mli @@ -46,8 +46,7 @@ module type DisjunctiveConfig = sig [ `UnderApproximateAfter of int (** When the set of disjuncts gets bigger than [n] then just stop adding new states to it, drop any further states on the floor. This corresponds to an under-approximation/bounded - approach. *) - | `NeverJoin (** keep accumulating states *) ] + approach. *) ] val widen_policy : [`UnderApproximateAfterNumIterations of int] end diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 8bb805539..69e543112 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -294,9 +294,7 @@ module DisjunctiveAnalyzer = AbstractInterpreter.MakeDisjunctive (PulseTransferFunctions) (struct - let join_policy = - match Config.pulse_max_disjuncts with 0 -> `NeverJoin | n -> `UnderApproximateAfter n - + let join_policy = `UnderApproximateAfter Config.pulse_max_disjuncts let widen_policy = `UnderApproximateAfterNumIterations Config.pulse_widen_threshold end)