From eb86c9cc178b59c022bd723c735d10ca9b49e924 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 21 Apr 2021 10:25:54 -0700 Subject: [PATCH] [pulse] dedup states during join MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Summary: This is mostly useful to avoid duplicating error states, which are propagated unchanged through both branches of, say, conditionals, and can end up duplicated if the join is not careful: ``` {[Abort(Error 1), Abort(Error 2), Continue σ']} if (..) { .. } else { .. } {JOIN([Abort(Error 1), Abort(Error 2), Continue σ_then], [Abort(Error 1), Abort(Error 2), Continue σ_else])} {[Abort(Error 1), Abort(Error 2), Continue σ_then, Continue σ_else]} ``` Whereas before this diff we got ``` {[Abort(Error 1), Abort(Error 2), Continue σ_then, Abort(Error 1), Abort(Error 2), Continue σ_else]} ``` Detect states that do not change simply using `phys_equal` as they should literally not change. Refactor the code to be able to re-use the same logic in the stronger join used in widening, that compares states using the domain's `leq` relation to establish implication. Reviewed By: ezgicicek Differential Revision: D27908529 fbshipit-source-id: b461165da --- infer/src/absint/AbstractInterpreter.ml | 63 +++++++++++++++---------- 1 file changed, 39 insertions(+), 24 deletions(-) diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index 820ea4586..31a4bfd58 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -119,23 +119,47 @@ struct (** a list [\[x1; x2; ...; xN\]] represents a disjunction [x1 ∨ x2 ∨ ... ∨ xN] *) type t = T.Domain.t list - let rev_filter_not_over_approximated disjuncts ~not_in = - List.rev_filter disjuncts ~f:(fun disjunct -> - List.exists not_in ~f:(fun disj_not_in -> T.Domain.leq ~lhs:disjunct ~rhs:disj_not_in) - |> not ) + (* a bit too specialised to go into {!IList} *) + let length_if_leq n l = + let rec aux length n l = + if n < 0 then None + else match l with [] -> Some length | _ :: tl -> aux (length + 1) (n - 1) tl + in + aux 0 n l + + + let append_no_duplicates_up_to leq n from ~into = + let rec aux n acc from = + match from with + | hd :: tl when n > 0 -> + (* check with respect to the original [into] and not [acc] as we assume lists of + disjuncts are already deduplicated *) + if List.exists into ~f:(fun into_disj -> leq ~lhs:hd ~rhs:into_disj) then + (* [hd] is already implied by one of the states in [into]; skip it + ([(a=>b) => (a\/b <=> b)]) *) + aux n acc tl + else aux (n - 1) (hd :: acc) tl + | _ -> + (* [from] is empty or [n = 0], either way we are done *) acc + in + aux n into from - let join : t -> t -> t = - let rec list_rev_append l1 l2 n = - match l1 with hd :: tl when n > 0 -> list_rev_append tl (hd :: l2) (n - 1) | _ -> l2 - in - fun lhs rhs -> - if phys_equal lhs rhs then lhs - else - 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) + (** Ignore states in [lhs] that are over-approximated in [rhs] and vice-versa. Favors keeping + states in [lhs]. *) + let join_up_to leq lhs rhs = + if phys_equal lhs rhs then lhs + else + let (`UnderApproximateAfter n) = DConfig.join_policy in + match length_if_leq n lhs with + | None -> + (* already at max disjuncts *) lhs + | Some lhs_length -> + (* this filters only in one direction for now, could be worth doing both ways *) + append_no_duplicates_up_to leq (n - lhs_length) rhs ~into:lhs + + let join lhs rhs = join_up_to (fun ~lhs ~rhs -> phys_equal lhs rhs) lhs rhs (** check if elements of [disj] appear in [of_] in the same order, using pointer equality on abstract states to compare elements quickly *) @@ -153,15 +177,6 @@ struct let leq ~lhs ~rhs = phys_equal lhs rhs || is_trivial_subset lhs ~of_:rhs - (** Ignore states in [lhs] that are over-approximated in [rhs] and vice-versa. Favors keeping - states in [lhs]. *) - let join_up_to_imply lhs rhs = - let rev_rhs_not_in_lhs = rev_filter_not_over_approximated rhs ~not_in:lhs in - (* cheeky: this is only used in pulse, whose (<=) is actually a symmetric relation so there's - no need to filter out elements of [lhs] *) - join lhs rev_rhs_not_in_lhs - - let widen ~prev ~next ~num_iters = let (`UnderApproximateAfterNumIterations max_iter) = DConfig.widen_policy in if phys_equal prev next then prev @@ -169,7 +184,7 @@ struct L.d_printfln "Iteration %d is greater than max iter %d, stopping." num_iters max_iter ; prev ) else - let post = join_up_to_imply prev next in + let post = join_up_to T.Domain.leq prev next in if leq ~lhs:post ~rhs:prev then prev else post