[inferbo] Fix xcompare of Itv

Reviewed By: mbouaziz

Differential Revision: D10851762

fbshipit-source-id: 20e26cc30

infer/src/bufferoverrun/itv.ml

@@ -465,27 +465,27 @@ module ItvPure = struct
     | `Equal, `Equal ->
         `Equal
     | `NotComparable, _ | _, `NotComparable -> (
-      match Bound.xcompare ~lhs:u1 ~rhs:l2 with
+      match (Bound.xcompare ~lhs:u1 ~rhs:l2, Bound.xcompare ~lhs:u2 ~rhs:l1) with
-      | `LeftSmallerThanRight ->
+      | `Equal, `Equal ->
+          `Equal (* weird, though *)
+      | (`Equal | `LeftSmallerThanRight), _ ->
           `LeftSmallerThanRight
-      | u1l2 -> (
+      | _, (`Equal | `LeftSmallerThanRight) ->
-        match (Bound.xcompare ~lhs:u2 ~rhs:l1, u1l2) with
+          `RightSmallerThanLeft
-        | `LeftSmallerThanRight, _ ->
+      | (`NotComparable | `RightSmallerThanLeft), (`NotComparable | `RightSmallerThanLeft) ->
-            `RightSmallerThanLeft
+          `NotComparable )
-        | `Equal, `Equal ->
+    | `Equal, `LeftSmallerThanRight
-            `Equal (* weird, though *)
+    | `RightSmallerThanLeft, `Equal
-        | _, `Equal ->
-            `LeftSmallerThanRight
-        | _ ->
-            `NotComparable ) )
-    | (`LeftSmallerThanRight | `Equal), (`LeftSmallerThanRight | `Equal) ->
-        `LeftSmallerThanRight
-    | (`RightSmallerThanLeft | `Equal), (`RightSmallerThanLeft | `Equal) ->
-        `RightSmallerThanLeft
-    | `LeftSmallerThanRight, `RightSmallerThanLeft ->
-        `LeftSubsumesRight
     | `RightSmallerThanLeft, `LeftSmallerThanRight ->
         `RightSubsumesLeft
+    | `Equal, `RightSmallerThanLeft
+    | `LeftSmallerThanRight, `Equal
+    | `LeftSmallerThanRight, `RightSmallerThanLeft ->
+        `LeftSubsumesRight
+    | `LeftSmallerThanRight, `LeftSmallerThanRight ->
+        `LeftSmallerThanRight
+    | `RightSmallerThanLeft, `RightSmallerThanLeft ->
+        `RightSmallerThanLeft
 
 
   let join : t -> t -> t =

infer/tests/codetoanalyze/c/bufferoverrun/issues.exp

@@ -69,7 +69,6 @@ codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_O
 codetoanalyze/c/bufferoverrun/global.c, use_global_const_ten_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 10 Size: 5]
 codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32]
 codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
-codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Assignment,Binop: ([1, +oo] + 1):signed32]
 codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 11, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/inf_loop.c, inf_loop, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []

infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp

@@ -69,8 +69,6 @@ codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3
 codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Call,Binop: (4 * [0, +oo]):unsigned64]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Parameter: __n,Call,Parameter: __n,Assignment,Call,Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,Return,Assignment,Call,Return,Return,ArrayAccess: Offset: [-oo, +oo] Size: 5]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Call,Call,Call,Call,Call,Binop: ([0, +oo] + 1):unsigned64]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 8, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Binop: ([1, +oo] + 1):unsigned64]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Binop: ([2, +oo] + 1):unsigned64]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Binop: ([3, +oo] + 42):unsigned64]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Binop: (4 * [45, +oo]):unsigned64]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,Parameter: __il,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]

infer/tests/codetoanalyze/java/performance/issues.exp

@@ -147,7 +147,6 @@ codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 * (length.ub + -1)^2 + 8 * length.ub, degree = 2]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 8, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([10, +oo] + 1):signed32]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar_SHOULD_NOT_REPORT_CONDITION_ALWAYS_TRUE_OR_FALSE(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar_SHOULD_NOT_REPORT_CONDITION_ALWAYS_TRUE_OR_FALSE(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 5, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
 codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []