From 92b9a7d72e666292fe68ba0d16e754a566230d67 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 17 Dec 2024 04:52:28 -0800 Subject: [PATCH] [pulse][join] do not treat calls with an over-approx result as unknown Summary: When running in over-approximation mode, a call's effect can be purely in the over-approx part of the state and the previous heuristic would think we failed to apply the call in that case and scramble the state instead. Reviewed By: hajduakos Differential Revision: D67276580 Privacy Context Container: L1208441 fbshipit-source-id: c0773b20c35547e2decdcd1094ef7dbd503bbd88 --- infer/src/pulse/PulseCallOperations.ml | 4 +++- infer/src/pulse/PulseNonDisjunctiveDomain.ml | 2 ++ infer/src/pulse/PulseNonDisjunctiveDomain.mli | 2 ++ 3 files changed, 7 insertions(+), 1 deletion(-) diff --git a/infer/src/pulse/PulseCallOperations.ml b/infer/src/pulse/PulseCallOperations.ml index 1d649627d0..5abafd7153 100644 --- a/infer/src/pulse/PulseCallOperations.ml +++ b/infer/src/pulse/PulseCallOperations.ml @@ -968,7 +968,9 @@ let call ?disjunct_limit ({InterproceduralAnalysis.analyze_dependency} as analys iter_call ~max_iteration ~nth_iteration:0 ~is_pulse_specialization_limit_not_reached already_given summary.PulseSummary.main astate in - let has_continue_program = has_continue_program res in + let has_continue_program = + has_continue_program res || not (NonDisjDomain.astate_is_bottom non_disj) + in if has_continue_program then GlobalForStats.node_is_not_stuck () ; let res, non_disj = if diff --git a/infer/src/pulse/PulseNonDisjunctiveDomain.ml b/infer/src/pulse/PulseNonDisjunctiveDomain.ml index d7ba57ff61..89d65da8db 100644 --- a/infer/src/pulse/PulseNonDisjunctiveDomain.ml +++ b/infer/src/pulse/PulseNonDisjunctiveDomain.ml @@ -868,6 +868,8 @@ let join_to_astate astate non_disj = {non_disj with astate= OverApproxDomain.join non_disj.astate astate} +let astate_is_bottom {astate} = OverApproxDomain.is_bottom astate + type summary = { transitive_info: InterDom.t ; has_dropped_disjuncts: AbstractDomain.BooleanOr.t diff --git a/infer/src/pulse/PulseNonDisjunctiveDomain.mli b/infer/src/pulse/PulseNonDisjunctiveDomain.mli index 2f7d19430f..34b0547eb8 100644 --- a/infer/src/pulse/PulseNonDisjunctiveDomain.mli +++ b/infer/src/pulse/PulseNonDisjunctiveDomain.mli @@ -50,6 +50,8 @@ val exec : val join_to_astate : (AbductiveDomain.t * PathContext.t) AbstractDomain.Types.bottom_lifted -> t -> t +val astate_is_bottom : t -> bool + val for_disjunct_exec_instr : t -> t val pp_with_kind : Pp.print_kind -> F.formatter -> t -> unit