[cost] Ignore boolean symbols in the cost results

Summary:
Since it is non-sense to get ranges of boolean values, this diff
ignores control values that only contain boolean symbols.

Depends on D16804802

Reviewed By: ezgicicek

Differential Revision: D16804808

fbshipit-source-id: ccb25db4d

infer/src/bufferoverrun/bounds.ml

@@ -298,18 +298,22 @@ module Bound = struct
 
   let of_sym : SymLinear.t -> t = fun s -> Linear (Z.zero, s)
 
-  let of_path path_of_partial make_symbol ~unsigned partial =
+  let of_path path_of_partial make_symbol ~unsigned ?boolean partial =
-    let s = make_symbol ~unsigned (path_of_partial partial) in
+    let s = make_symbol ~unsigned ?boolean (path_of_partial partial) in
     of_sym (SymLinear.singleton_one s)
 
 
   let of_normal_path = of_path Symb.SymbolPath.normal
 
-  let of_offset_path ~is_void = of_path (Symb.SymbolPath.offset ~is_void) ~unsigned:false
+  let of_offset_path ~is_void =
+    of_path (Symb.SymbolPath.offset ~is_void) ~unsigned:false ~boolean:false
 
-  let of_length_path ~is_void = of_path (Symb.SymbolPath.length ~is_void) ~unsigned:true
 
-  let of_modeled_path = of_path Symb.SymbolPath.modeled ~unsigned:true
+  let of_length_path ~is_void =
+    of_path (Symb.SymbolPath.length ~is_void) ~unsigned:true ~boolean:false
+
+
+  let of_modeled_path = of_path Symb.SymbolPath.modeled ~unsigned:true ~boolean:false
 
   let is_path_of ~f = function
     | Linear (n, se) when Z.(equal n zero) ->

infer/src/bufferoverrun/bounds.mli

@@ -35,7 +35,8 @@ module Bound : sig
 
   val pinf : t
 
-  val of_normal_path : Symb.Symbol.make_t -> unsigned:bool -> Symb.SymbolPath.partial -> t
+  val of_normal_path :
+    Symb.Symbol.make_t -> unsigned:bool -> ?boolean:bool -> Symb.SymbolPath.partial -> t
 
   val of_offset_path : is_void:bool -> Symb.Symbol.make_t -> Symb.SymbolPath.partial -> t
 

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -424,11 +424,11 @@ module Val = struct
       let trace = if Loc.is_global l then Trace.Global l else Trace.Parameter l in
       TraceSet.singleton location trace
     in
-    let itv_val () =
+    let itv_val ~boolean =
       let l = Loc.of_path path in
       let traces = traces_of_loc l in
       let unsigned = Typ.is_unsigned_int typ in
-      of_itv ~traces (Itv.of_normal_path ~unsigned path)
+      of_itv ~traces (Itv.of_normal_path ~unsigned ~boolean path)
     in
     let ptr_to_c_array_alloc deref_path size =
       let allocsite = Allocsite.make_symbol deref_path in
@@ -441,8 +441,10 @@ module Val = struct
       (if may_last_field then ", may_last_field" else "")
       (if is_java then ", is_java" else "") ;
     match typ.Typ.desc with
+    | Tint IBool ->
+        itv_val ~boolean:true
     | Tint _ | Tfloat _ | Tvoid | Tfun _ | TVar _ ->
-        itv_val ()
+        itv_val ~boolean:false
     | Tptr (elt, _) ->
         if is_java || SPath.is_this path then
           let deref_kind =
@@ -492,7 +494,7 @@ module Val = struct
           let length = Itv.of_length_path ~is_void:false path in
           of_java_array_alloc allocsite ~length ~traces
       | Some JavaInteger ->
-          itv_val ()
+          itv_val ~boolean:false
       | None ->
           let l = Loc.of_path path in
           let traces = traces_of_loc l in
@@ -611,8 +613,11 @@ module MemPure = struct
       (fun loc (_, v) acc ->
         match filter_loc loc with
         | Some loop_head_loc ->
-            v |> Val.get_itv |> Itv.range loop_head_loc |> Itv.ItvRange.to_top_lifted_polynomial
+            let itv = Val.get_itv v in
-            |> Polynomials.NonNegativePolynomial.mult acc
+            if Itv.has_only_boolean_symbols itv then acc
+            else
+              Itv.range loop_head_loc itv |> Itv.ItvRange.to_top_lifted_polynomial
+              |> Polynomials.NonNegativePolynomial.mult acc
         | None ->
             acc )
       mem Polynomials.NonNegativePolynomial.one

infer/src/bufferoverrun/itv.ml

@@ -414,6 +414,11 @@ module ItvPure = struct
    fun (l, u) -> SymbolSet.union (Bound.get_symbols l) (Bound.get_symbols u)
 
 
+  let has_only_boolean_symbols x =
+    let symbols = get_symbols x in
+    (not (SymbolSet.is_empty symbols)) && SymbolSet.for_all Symb.Symbol.is_boolean symbols
+
+
   let make_positive : t -> t =
    fun ((l, u) as x) -> if Bound.lt l Bound.zero then (Bound.zero, u) else x
 
@@ -433,7 +438,7 @@ module ItvPure = struct
       (b, b)
 
 
-  let of_normal_path ~unsigned = of_path (Bound.of_normal_path ~unsigned)
+  let of_normal_path ~unsigned ?boolean = of_path (Bound.of_normal_path ~unsigned ?boolean)
 
   let of_offset_path ~is_void = of_path (Bound.of_offset_path ~is_void)
 
@@ -666,7 +671,9 @@ let max_of_ikind integer_type_widths ikind =
   NonBottom (ItvPure.max_of_ikind integer_type_widths ikind)
 
 
-let of_normal_path ~unsigned path = NonBottom (ItvPure.of_normal_path ~unsigned path)
+let of_normal_path ~unsigned ?boolean path =
+  NonBottom (ItvPure.of_normal_path ~unsigned ?boolean path)
+
 
 let of_offset_path ~is_void path = NonBottom (ItvPure.of_offset_path ~is_void path)
 
@@ -677,3 +684,5 @@ let of_modeled_path path = NonBottom (ItvPure.of_modeled_path path)
 let is_offset_path_of path = bind1_gen ~bot:false (ItvPure.is_offset_path_of path)
 
 let is_length_path_of path = bind1_gen ~bot:false (ItvPure.is_length_path_of path)
+
+let has_only_boolean_symbols = bind1bool ItvPure.has_only_boolean_symbols

infer/src/bufferoverrun/itv.mli

@@ -231,7 +231,7 @@ val subst : t -> Bound.eval_sym -> t
 
 val max_of_ikind : Typ.IntegerWidths.t -> Typ.ikind -> t
 
-val of_normal_path : unsigned:bool -> Symb.SymbolPath.partial -> t
+val of_normal_path : unsigned:bool -> ?boolean:bool -> Symb.SymbolPath.partial -> t
 
 val of_offset_path : is_void:bool -> Symb.SymbolPath.partial -> t
 
@@ -242,3 +242,5 @@ val of_modeled_path : Symb.SymbolPath.partial -> t
 val is_offset_path_of : Symb.SymbolPath.partial -> t -> bool
 
 val is_length_path_of : Symb.SymbolPath.partial -> t -> bool
+
+val has_only_boolean_symbols : t -> bool

infer/src/bufferoverrun/symb.ml

@@ -247,14 +247,18 @@ module Symbol = struct
   let compare_extra_bool _ _ = 0
 
   type t =
-    | OneValue of {unsigned: extra_bool; path: SymbolPath.t}
+    | OneValue of {unsigned: extra_bool; boolean: extra_bool; path: SymbolPath.t}
-    | BoundEnd of {unsigned: extra_bool; path: SymbolPath.t; bound_end: BoundEnd.t}
+    | BoundEnd of
+        { unsigned: extra_bool
+        ; boolean: extra_bool
+        ; path: SymbolPath.t
+        ; bound_end: BoundEnd.t }
   [@@deriving compare]
 
   let pp : F.formatter -> t -> unit =
    fun fmt s ->
     match s with
-    | OneValue {unsigned; path} | BoundEnd {unsigned; path} ->
+    | OneValue {unsigned; boolean; path} | BoundEnd {unsigned; boolean; path} ->
         SymbolPath.pp fmt path ;
         ( if Config.developer_mode then
           match s with
@@ -262,7 +266,8 @@ module Symbol = struct
               Format.fprintf fmt ".%s" (BoundEnd.to_string bound_end)
           | OneValue _ ->
               () ) ;
-        if Config.bo_debug > 1 then F.fprintf fmt "(%c)" (if unsigned then 'u' else 's')
+        if Config.bo_debug > 1 then
+          F.fprintf fmt "(%c%s)" (if unsigned then 'u' else 's') (if boolean then "b" else "")
 
 
   let compare s1 s2 =
@@ -293,18 +298,22 @@ module Symbol = struct
         SymbolPath.equal path1 path2
 
 
-  type make_t = unsigned:bool -> SymbolPath.t -> t
+  type make_t = unsigned:bool -> ?boolean:bool -> SymbolPath.t -> t
+
+  let make_onevalue : make_t =
+   fun ~unsigned ?(boolean = false) path -> OneValue {unsigned; boolean; path}
 
-  let make_onevalue : make_t = fun ~unsigned path -> OneValue {unsigned; path}
 
   let make_boundend : BoundEnd.t -> make_t =
-   fun bound_end ~unsigned path -> BoundEnd {unsigned; path; bound_end}
+   fun bound_end ~unsigned ?(boolean = false) path -> BoundEnd {unsigned; boolean; path; bound_end}
 
 
   let pp_mark ~markup = if markup then MarkupFormatter.wrap_monospaced pp else pp
 
   let is_unsigned : t -> bool = function OneValue {unsigned} | BoundEnd {unsigned} -> unsigned
 
+  let is_boolean : t -> bool = function OneValue {boolean} | BoundEnd {boolean} -> boolean
+
   let path = function OneValue {path} | BoundEnd {path} -> path
 
   let assert_bound_end s be =

infer/src/bufferoverrun/symb.mli

@@ -100,6 +100,8 @@ module Symbol : sig
 
   val is_unsigned : t -> bool
 
+  val is_boolean : t -> bool
+
   val pp_mark : markup:bool -> F.formatter -> t -> unit
 
   val equal : t -> t -> bool
@@ -110,7 +112,7 @@ module Symbol : sig
 
   val assert_bound_end : t -> BoundEnd.t -> unit
 
-  type make_t = unsigned:bool -> SymbolPath.t -> t
+  type make_t = unsigned:bool -> ?boolean:bool -> SymbolPath.t -> t
 
   val make_onevalue : make_t
 

infer/tests/codetoanalyze/java/performance/Cost_test.java

@@ -119,4 +119,37 @@ public class Cost_test {
 
   // Cost: 1
   private static void unitCostFunction() {}
+
+  boolean rand() {
+    if (Math.random() > 0.5) {
+      return true;
+    } else {
+      return false;
+    }
+  }
+
+  // Cost: Linear to n, not b
+  void ignore_boolean_symbols_linear(boolean b, int n) {
+    for (int i = 0; b && i < n; i++) {
+      b = true;
+    }
+  }
+
+  // Cost should not include the symbol of b.
+  void ignore_boolean_symbols_constant1(boolean b) {
+    for (; b; ) {
+      if (rand()) {
+        b = true;
+      }
+    }
+  }
+
+  // Cost should not include the symbol of b.
+  void ignore_boolean_symbols_constant2(boolean b) {
+    for (; b; ) {
+      if (rand()) {
+        b = false;
+      }
+    }
+  }
 }

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

@@ -87,6 +87,7 @@ codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performanc
 codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.while_and_or(int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/java/performance/Continue.java, codetoanalyze.java.performance.Continue.continue_outer_loop():int, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7963049, O(1), degree = 0]
 codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.FN_loop2(int):int, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 13 ⋅ k, O(k), degree = 1,{k},Loop at line 90]
+codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.ignore_boolean_symbols_linear(boolean,int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 6 ⋅ n + 2 ⋅ (1+max(0, n)), O(n), degree = 1,{1+max(0, n)},Loop at line 133,{n},Loop at line 133]
 codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.loop0_bad():int, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 1202, O(1), degree = 0]
 codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.loop1_bad():int, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 1303, O(1), degree = 0]
 codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.loop3(int):int, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 237, O(1), degree = 0]