From d5b7130eb5e0b0a000d28550a56d9587fd757f59 Mon Sep 17 00:00:00 2001
From: Sungkeun Cho <scho@fb.com>
Date: Mon, 18 May 2020 05:11:37 -0700
Subject: [PATCH] [pulse] Fix limitation of disjuncts

Reviewed By: jvillard

Differential Revision: D21617803

fbshipit-source-id: be4cf5147
---
 infer/src/absint/AbstractInterpreter.ml | 39 +++++++++++++------------
 1 file changed, 21 insertions(+), 18 deletions(-)

diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml
index 4883aea20..904f94d0e 100644
--- a/infer/src/absint/AbstractInterpreter.ml
+++ b/infer/src/absint/AbstractInterpreter.ml
@@ -125,25 +125,19 @@ struct
           |> not )
 
 
-    (** 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] *)
-      List.rev_append rev_rhs_not_in_lhs lhs
-
-
     let join : t -> t -> t =
-     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
+      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
+          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)
 
 
     (** check if elements of [disj] appear in [of_] in the same order, using pointer equality on
@@ -162,6 +156,15 @@ 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