From f4b6746e0b66130af9a2439aeb9b8ee542fdc6c7 Mon Sep 17 00:00:00 2001
From: Mehdi Bouaziz <mbouaziz@fb.com>
Date: Thu, 26 Apr 2018 09:22:25 -0700
Subject: [PATCH] [inferbo][PO] Fully compare traces when deduplicating

Reviewed By: jvillard

Differential Revision: D7774197

fbshipit-source-id: 7bce9db
---
 .../bufferOverrunProofObligations.ml          | 21 +++++++++----------
 1 file changed, 10 insertions(+), 11 deletions(-)

diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
index b861fb9fe..85e54ed09 100644
--- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
+++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
@@ -318,8 +318,8 @@ module ConditionTrace = struct
 
   type t =
     { proc_name: Typ.Procname.t
-    ; location: Location.t
     ; cond_trace: cond_trace
+    ; location: Location.t
     ; val_traces: ValTraceSet.t }
   [@@deriving compare]
 
@@ -377,13 +377,16 @@ module ConditionWithTrace = struct
 
   let pp fmt {cond; trace} = F.fprintf fmt "%a %a" Condition.pp cond ConditionTrace.pp trace
 
-  let compare_by_location {trace= trace1} {trace= trace2} =
-    Location.compare (ConditionTrace.get_location trace1) (ConditionTrace.get_location trace2)
-
-
   let have_similar_bounds {cond= cond1} {cond= cond2} = Condition.have_similar_bounds cond1 cond2
 
-  let xcompare_cond ~lhs:{cond= lhs} ~rhs:{cond= rhs} = Condition.xcompare ~lhs ~rhs
+  let xcompare ~lhs ~rhs =
+    match Condition.xcompare ~lhs:lhs.cond ~rhs:rhs.cond with
+    | `Equal ->
+        if ConditionTrace.compare lhs.trace rhs.trace <= 0 then `LeftSubsumesRight
+        else `RightSubsumesLeft
+    | (`LeftSubsumesRight | `RightSubsumesLeft | `NotComparable) as cmp ->
+        cmp
+
 
   let subst (bound_map, trace_map) caller_pname callee_pname location cwt =
     match Condition.get_symbols cwt.cond with
@@ -437,11 +440,7 @@ module ConditionSet = struct
     (* we don't want to remove issues that would end up in a higher bucket,
      e.g. [a, b] < [c, d] is subsumed by [a, +oo] < [c, d] but the latter is less precise *)
     if ConditionWithTrace.have_similar_bounds existing new_ then
-      match ConditionWithTrace.xcompare_cond ~lhs:existing ~rhs:new_ with
-      | `Equal ->
-          (* keep the first one in the code *)
-          if ConditionWithTrace.compare_by_location existing new_ <= 0 then `DoNotAddAndStop
-          else `RemoveExistingAndContinue
+      match ConditionWithTrace.xcompare ~lhs:existing ~rhs:new_ with
       | `LeftSubsumesRight ->
           `DoNotAddAndStop
       | `RightSubsumesLeft ->