[pulse] dedup states during join

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

@@ -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 =
+    (* a bit too specialised to go into {!IList} *)
-      List.rev_filter disjuncts ~f:(fun disjunct ->
+    let length_if_leq n l =
-          List.exists not_in ~f:(fun disj_not_in -> T.Domain.leq ~lhs:disjunct ~rhs:disj_not_in)
+      let rec aux length n l =
-          |> not )
+        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 =
+    (** Ignore states in [lhs] that are over-approximated in [rhs] and vice-versa. Favors keeping
-      let rec list_rev_append l1 l2 n =
+        states in [lhs]. *)
-        match l1 with hd :: tl when n > 0 -> list_rev_append tl (hd :: l2) (n - 1) | _ -> l2
+    let join_up_to leq lhs rhs =
-      in
+      if phys_equal lhs rhs then lhs
-      fun lhs rhs ->
+      else
-        if phys_equal lhs rhs then lhs
+        let (`UnderApproximateAfter n) = DConfig.join_policy in
-        else
+        match length_if_leq n lhs with
-          let (`UnderApproximateAfter n) = DConfig.join_policy in
+        | None ->
-          let lhs_length = List.length lhs in
+            (* already at max disjuncts *) lhs
-          if lhs_length >= n then lhs else list_rev_append rhs lhs (n - lhs_length)
+        | 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