[inferbo] Pointer comparison

Reviewed By: skcho

Differential Revision: D13066771

fbshipit-source-id: 134b27db8

infer/src/bufferoverrun/absLoc.ml

@@ -21,6 +21,18 @@ module Allocsite = struct
         ; path: Symb.SymbolPath.partial option }
   [@@deriving compare]
 
+  let eq as1 as2 =
+    match (as1, as2) with
+    | Unknown, _ | _, Unknown ->
+        Boolean.Top
+    | Known {path= Some _}, Known {path= Some _} ->
+        (* Known with a path are parameters, parameters may alias *) Boolean.Top
+    | Known {path= Some _}, Known {path= None} | Known {path= None}, Known {path= Some _} ->
+        Boolean.False
+    | Known {path= None}, Known {path= None} ->
+        Boolean.of_bool ([%compare.equal: t] as1 as2)
+
+
   let pp fmt = function
     | Unknown ->
         F.fprintf fmt "Unknown"
@@ -57,6 +69,10 @@ module Loc = struct
 
   let equal = [%compare.equal: t]
 
+  let eq l1 l2 =
+    match (l1, l2) with Allocsite as1, Allocsite as2 -> Allocsite.eq as1 as2 | _ -> Boolean.Top
+
+
   let unknown = Allocsite Allocsite.unknown
 
   let rec pp fmt = function
@@ -127,6 +143,14 @@ module PowLoc = struct
   let append_field ploc ~fn =
     if is_bot ploc then singleton Loc.unknown
     else fold (fun l -> add (Loc.append_field l ~fn)) ploc empty
+
+
+  let lift_cmp cmp_loc ploc1 ploc2 =
+    match (is_singleton_or_more ploc1, is_singleton_or_more ploc2) with
+    | IContainer.Singleton loc1, IContainer.Singleton loc2 ->
+        Boolean.EqualOrder.of_equal cmp_loc (Loc.eq loc1 loc2)
+    | _ ->
+        Boolean.Top
 end
 
 (** unsound but ok for bug catching *)

infer/src/bufferoverrun/arrayBlk.ml

@@ -103,6 +103,12 @@ module ArrInfo = struct
         else
           let set itv = Itv.div_const (Itv.mult_const itv stride) new_stride in
           {offset= set offset; size= set size; stride= Itv.of_big_int new_stride} )
+
+
+  let lift_cmp_itv cmp_itv arr1 arr2 =
+    if Itv.eq arr1.stride arr2.stride && Itv.eq arr1.size arr2.size then
+      cmp_itv arr1.offset arr2.offset
+    else Boolean.Top
 end
 
 include AbstractDomain.Map (Allocsite) (ArrInfo)
@@ -184,3 +190,13 @@ let prune_ne : astate -> astate -> astate = fun a1 a2 -> do_prune ArrInfo.prune_
 let set_length : Itv.t -> astate -> astate = fun length a -> map (ArrInfo.set_length length) a
 
 let set_stride : Z.t -> astate -> astate = fun stride a -> map (ArrInfo.set_stride stride) a
+
+let lift_cmp_itv cmp_itv cmp_loc arr1 arr2 =
+  match (is_singleton_or_more arr1, is_singleton_or_more arr2) with
+  | IContainer.Singleton (as1, ai1), IContainer.Singleton (as2, ai2) ->
+      Boolean.EqualOrder.(
+        of_equal
+          {on_equal= ArrInfo.lift_cmp_itv cmp_itv ai1 ai2; on_not_equal= cmp_loc.on_not_equal}
+          (Allocsite.eq as1 as2))
+  | _ ->
+      Boolean.Top

infer/src/bufferoverrun/boolean.ml

@@ -11,6 +11,8 @@ type t = Bottom | False | True | Top [@@deriving compare]
 
 let equal = [%compare.equal: t]
 
+let of_bool = function false -> False | true -> True
+
 let is_false = function False -> true | _ -> false
 
 let is_true = function True -> true | _ -> false
@@ -39,3 +41,31 @@ let or_ x y =
       True
   | Top, Top ->
       Top
+
+
+module EqualOrder = struct
+  type b = t
+
+  type t = {on_equal: b; on_not_equal: b}
+
+  let eq = {on_equal= True; on_not_equal= False}
+
+  let ne = {on_equal= False; on_not_equal= True}
+
+  let strict_cmp = {on_equal= False; on_not_equal= Top}
+
+  let loose_cmp = {on_equal= True; on_not_equal= Top}
+
+  let top = {on_equal= Top; on_not_equal= Top}
+
+  let of_equal t equal =
+    match equal with
+    | Bottom ->
+        Bottom
+    | True ->
+        t.on_equal
+    | False ->
+        t.on_not_equal
+    | Top ->
+        (* join t.on_equal t.on_not_equal is always Top *) Top
+end

infer/src/bufferoverrun/boolean.mli

@@ -9,6 +9,8 @@ open! IStd
 
 type t = Bottom | False | True | Top
 
+val of_bool : bool -> t
+
 val equal : t -> t -> bool
 
 val is_false : t -> bool
@@ -20,3 +22,27 @@ val not_ : t -> t
 val and_ : t -> t -> t
 
 val or_ : t -> t -> t
+
+module EqualOrder : sig
+  (**
+  This module provides abstract transfer functions for comparisons on unordered values, only based on equality, like abstract locations.
+*)
+
+  type b = t
+
+  type t = {on_equal: b; on_not_equal: b}
+
+  val eq : t
+
+  val ne : t
+
+  val strict_cmp : t
+  (** > or < *)
+
+  val loose_cmp : t
+  (** >= or <= *)
+
+  val top : t
+
+  val of_equal : t -> b -> b
+end

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -182,11 +182,26 @@ module Val = struct
     {bot with itv= f x.itv y.itv; traces= f_trace x.traces y.traces}
 
 
-  let has_pointer : t -> bool = fun x -> not (PowLoc.is_bot x.powloc && ArrayBlk.is_bot x.arrayblk)
-
-  let lift_cmp_itv : (Itv.t -> Itv.t -> Boolean.t) -> t -> t -> t =
-   fun f x y ->
-    let b = if has_pointer x || has_pointer y then Boolean.Top else f x.itv y.itv in
+  let lift_cmp_itv : (Itv.t -> Itv.t -> Boolean.t) -> Boolean.EqualOrder.t -> t -> t -> t =
+   fun cmp_itv cmp_loc x y ->
+    let b =
+      match
+        ( x.itv
+        , PowLoc.is_bot x.powloc
+        , ArrayBlk.is_bot x.arrayblk
+        , y.itv
+        , PowLoc.is_bot y.powloc
+        , ArrayBlk.is_bot y.arrayblk )
+      with
+      | NonBottom _, true, true, NonBottom _, true, true ->
+          cmp_itv x.itv y.itv
+      | Bottom, false, true, Bottom, false, true ->
+          PowLoc.lift_cmp cmp_loc x.powloc y.powloc
+      | Bottom, true, false, Bottom, true, false ->
+          ArrayBlk.lift_cmp_itv cmp_itv cmp_loc x.arrayblk y.arrayblk
+      | _ ->
+          Boolean.Top
+    in
     let itv = Itv.of_bool b in
     {bot with itv; traces= TraceSet.join x.traces y.traces}
 
@@ -209,21 +224,21 @@ module Val = struct
 
   let band_sem = lift_itv Itv.band_sem
 
-  let lt_sem : t -> t -> t = lift_cmp_itv Itv.lt_sem
+  let lt_sem : t -> t -> t = lift_cmp_itv Itv.lt_sem Boolean.EqualOrder.strict_cmp
 
-  let gt_sem : t -> t -> t = lift_cmp_itv Itv.gt_sem
+  let gt_sem : t -> t -> t = lift_cmp_itv Itv.gt_sem Boolean.EqualOrder.strict_cmp
 
-  let le_sem : t -> t -> t = lift_cmp_itv Itv.le_sem
+  let le_sem : t -> t -> t = lift_cmp_itv Itv.le_sem Boolean.EqualOrder.loose_cmp
 
-  let ge_sem : t -> t -> t = lift_cmp_itv Itv.ge_sem
+  let ge_sem : t -> t -> t = lift_cmp_itv Itv.ge_sem Boolean.EqualOrder.loose_cmp
 
-  let eq_sem : t -> t -> t = lift_cmp_itv Itv.eq_sem
+  let eq_sem : t -> t -> t = lift_cmp_itv Itv.eq_sem Boolean.EqualOrder.eq
 
-  let ne_sem : t -> t -> t = lift_cmp_itv Itv.ne_sem
+  let ne_sem : t -> t -> t = lift_cmp_itv Itv.ne_sem Boolean.EqualOrder.ne
 
-  let land_sem : t -> t -> t = lift_cmp_itv Itv.land_sem
+  let land_sem : t -> t -> t = lift_cmp_itv Itv.land_sem Boolean.EqualOrder.top
 
-  let lor_sem : t -> t -> t = lift_cmp_itv Itv.lor_sem
+  let lor_sem : t -> t -> t = lift_cmp_itv Itv.lor_sem Boolean.EqualOrder.top
 
   (* TODO: get rid of those cases *)
   let warn_against_pruning_multiple_values : t -> t =

infer/tests/codetoanalyze/c/bufferoverrun/global.c

@@ -16,12 +16,18 @@ const int global_const_zero = 0;
 
 enum { global_const = global_const_zero };
 
-void compare_global_const_enum_bad_FN() {
+void compare_global_const_enum_Bad() {
   char arr[10];
   if (global_const < 10)
     arr[10] = 1;
 }
 
+void compare_global_const_enum_Good_FP() {
+  char arr[10];
+  if (global_const > 10)
+    arr[10] = 1;
+}
+
 const int global_const_ten = 10;
 
 void use_global_const_ten_Good() {

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

@@ -72,8 +72,8 @@ codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_
 codetoanalyze/c/bufferoverrun/get_field.c, FP_call_get_field_Good, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Call,Call,Parameter `x[*].field`,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 5]
 codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_Bad, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Call,Call,Parameter `x[*].field`,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 5]
 codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_cond_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
-codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_bad_FN, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
-codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_bad_FN, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
+codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
+codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/global.c, use_global_const_ten_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
 codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
@@ -158,6 +158,8 @@ codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith3_Bad, 2, BUFFE
 codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith4_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `x`,<Length trace>,Array declaration,Array access: Offset: 10 (⇐ 100 + -90) Size: 5 by call to `FN_pointer_arith4_Bad` ]
 codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
+codetoanalyze/c/bufferoverrun/prune_alias.c, bad_if_alias, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
+codetoanalyze/c/bufferoverrun/prune_alias.c, bad_if_not_alias, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
 codetoanalyze/c/bufferoverrun/prune_alias.c, call_prune_arrblk_ne_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `x`,Array access: Offset: 5 Size: 5 by call to `prune_arrblk_ne` ]
 codetoanalyze/c/bufferoverrun/prune_alias.c, loop_prune2_Good_FP, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `length`,<Length trace>,Parameter `length`,Array declaration,Array access: Offset: [-length + length + 1, length] Size: length]
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]

infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c

@@ -193,3 +193,37 @@ void nested_loop_prune_Good(int length) {
     }
   }
 }
+
+void bad_if_alias(int* x, int* y) {
+  char a[1];
+  if (x == y) {
+    a[1] = 'A';
+  }
+}
+
+void call_bad_if_alias_Bad_AlreadyReported() {
+  int x;
+  bad_if_alias(x, x);
+}
+
+void call_bad_if_alias_Good() {
+  int x, y;
+  bad_if_alias(x, y);
+}
+
+void bad_if_not_alias(int* x, int* y) {
+  char a[1];
+  if (x != y) {
+    a[1] = 'B';
+  }
+}
+
+void call_bad_if_not_alias_Good() {
+  int x;
+  bad_if_not_alias(x, x);
+}
+
+void call_bad_if_not_alias_Bad_AlreadyReported() {
+  int x, y;
+  bad_if_not_alias(x, y);
+}

infer/tests/codetoanalyze/java/performance/Loops.java

@@ -66,7 +66,7 @@ public class Loops {
     public float[] f;
   }
 
-  static boolean similar_SHOULD_NOT_REPORT_CONDITION_ALWAYS_TRUE_OR_FALSE(C[] x, C[] y) {
+  static boolean similar(C[] x, C[] y) {
     if (x == null || y == null || x.length != y.length) {
       return false;
     }

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

@@ -150,8 +150,10 @@ 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)² + 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, [<LHS trace>,Assignment,Binary operation: ([0, +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, [Here]
-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, [Here]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 14 + 33 ⋅ x.length.ub, degree = 1]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 13 + 33 ⋅ x.length.ub, degree = 1]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 14 + 33 ⋅ x.length.ub, degree = 1]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 13 + 33 ⋅ x.length.ub, degree = 1]
 codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 798, degree = 0]
 codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 798, degree = 0]