[cost] Ignore non-int symbols in the cost results

Summary:
Since it does not make sense to get ranges of non-integer values and
use them as approximate iteration numbers, this diff ignores control
values that only contain non-integer symbols.

Reviewed By: ezgicicek

Differential Revision: D17130967

fbshipit-source-id: f5ba58d52

infer/src/bufferoverrun/bounds.ml

@@ -304,22 +304,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 ?boolean partial =
-    let s = make_symbol ~unsigned ?boolean (path_of_partial partial) in
+  let of_path path_of_partial make_symbol ~unsigned ?non_int partial =
+    let s = make_symbol ~unsigned ?non_int (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 ~boolean:false
+    of_path (Symb.SymbolPath.offset ~is_void) ~unsigned:false ~non_int:false
 
 
   let of_length_path ~is_void =
-    of_path (Symb.SymbolPath.length ~is_void) ~unsigned:true ~boolean:false
+    of_path (Symb.SymbolPath.length ~is_void) ~unsigned:true ~non_int:false
 
 
-  let of_modeled_path = of_path Symb.SymbolPath.modeled ~unsigned:true ~boolean:false
+  let of_modeled_path = of_path Symb.SymbolPath.modeled ~unsigned:true ~non_int:false
 
   let is_path_of ~f = function
     | Linear (n, se) when Z.(equal n zero) ->

infer/src/bufferoverrun/bounds.mli

@@ -36,7 +36,7 @@ module Bound : sig
   val pinf : t
 
   val of_normal_path :
-    Symb.Symbol.make_t -> unsigned:bool -> ?boolean:bool -> Symb.SymbolPath.partial -> t
+    Symb.Symbol.make_t -> unsigned:bool -> ?non_int: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

@@ -433,11 +433,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 ~boolean =
+    let itv_val ~non_int =
       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 ~boolean path)
+      of_itv ~traces (Itv.of_normal_path ~unsigned ~non_int path)
     in
     let ptr_to_c_array_alloc deref_path size =
       let allocsite = Allocsite.make_symbol deref_path in
@@ -450,10 +450,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 ~boolean:false
+    | Tint IBool | Tfloat _ | Tfun _ | TVar _ ->
+        itv_val ~non_int:true
+    | Tint _ | Tvoid ->
+        itv_val ~non_int:false
     | Tptr (elt, _) ->
         if is_java || SPath.is_this path then
           let deref_kind =
@@ -503,7 +503,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 ~boolean:false
+          itv_val ~non_int:false
       | None ->
           let l = Loc.of_path path in
           let traces = traces_of_loc l in
@@ -623,7 +623,7 @@ module MemPure = struct
         match filter_loc loc with
         | Some loop_head_loc ->
             let itv = Val.get_itv v in
-            if Itv.has_only_boolean_symbols itv then acc
+            if Itv.has_only_non_int_symbols itv then acc
             else
               Itv.range loop_head_loc itv |> Itv.ItvRange.to_top_lifted_polynomial
               |> Polynomials.NonNegativePolynomial.mult acc

infer/src/bufferoverrun/itv.ml

@@ -416,9 +416,9 @@ module ItvPure = struct
    fun (l, u) -> SymbolSet.union (Bound.get_symbols l) (Bound.get_symbols u)
 
 
-  let has_only_boolean_symbols x =
+  let has_only_non_int_symbols x =
     let symbols = get_symbols x in
-    (not (SymbolSet.is_empty symbols)) && SymbolSet.for_all Symb.Symbol.is_boolean symbols
+    (not (SymbolSet.is_empty symbols)) && SymbolSet.for_all Symb.Symbol.is_non_int symbols
 
 
   let make_positive : t -> t =
@@ -440,7 +440,7 @@ module ItvPure = struct
       (b, b)
 
 
-  let of_normal_path ~unsigned ?boolean = of_path (Bound.of_normal_path ~unsigned ?boolean)
+  let of_normal_path ~unsigned ?non_int = of_path (Bound.of_normal_path ~unsigned ?non_int)
 
   let of_offset_path ~is_void = of_path (Bound.of_offset_path ~is_void)
 
@@ -673,8 +673,8 @@ let max_of_ikind integer_type_widths ikind =
   NonBottom (ItvPure.max_of_ikind integer_type_widths ikind)
 
 
-let of_normal_path ~unsigned ?boolean path =
-  NonBottom (ItvPure.of_normal_path ~unsigned ?boolean path)
+let of_normal_path ~unsigned ?non_int path =
+  NonBottom (ItvPure.of_normal_path ~unsigned ?non_int path)
 
 
 let of_offset_path ~is_void path = NonBottom (ItvPure.of_offset_path ~is_void path)
@@ -687,4 +687,4 @@ let is_offset_path_of path = bind1_gen ~bot:false (ItvPure.is_offset_path_of pat
 
 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
+let has_only_non_int_symbols = bind1bool ItvPure.has_only_non_int_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 -> ?boolean:bool -> Symb.SymbolPath.partial -> t
+val of_normal_path : unsigned:bool -> ?non_int:bool -> Symb.SymbolPath.partial -> t
 
 val of_offset_path : is_void:bool -> Symb.SymbolPath.partial -> t
 
@@ -243,4 +243,4 @@ 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
+val has_only_non_int_symbols : t -> bool

infer/src/bufferoverrun/symb.ml

@@ -252,11 +252,13 @@ module Symbol = struct
 
   let compare_extra_bool _ _ = 0
 
+  (* NOTE: non_int represents the symbols that are not integer type,
+     so that their ranges are not used in the cost checker.  *)
   type t =
-    | OneValue of {unsigned: extra_bool; boolean: extra_bool; path: SymbolPath.t}
+    | OneValue of {unsigned: extra_bool; non_int: extra_bool; path: SymbolPath.t}
     | BoundEnd of
         { unsigned: extra_bool
-        ; boolean: extra_bool
+        ; non_int: extra_bool
         ; path: SymbolPath.t
         ; bound_end: BoundEnd.t }
   [@@deriving compare]
@@ -264,7 +266,7 @@ module Symbol = struct
   let pp : F.formatter -> t -> unit =
    fun fmt s ->
     match s with
-    | OneValue {unsigned; boolean; path} | BoundEnd {unsigned; boolean; path} ->
+    | OneValue {unsigned; non_int; path} | BoundEnd {unsigned; non_int; path} ->
         SymbolPath.pp fmt path ;
         ( if Config.developer_mode then
           match s with
@@ -273,7 +275,7 @@ module Symbol = struct
           | OneValue _ ->
               () ) ;
         if Config.bo_debug > 1 then
-          F.fprintf fmt "(%c%s)" (if unsigned then 'u' else 's') (if boolean then "b" else "")
+          F.fprintf fmt "(%c%s)" (if unsigned then 'u' else 's') (if non_int then "n" else "")
 
 
   let compare s1 s2 =
@@ -304,21 +306,21 @@ module Symbol = struct
         SymbolPath.equal path1 path2
 
 
-  type make_t = unsigned:bool -> ?boolean:bool -> SymbolPath.t -> t
+  type make_t = unsigned:bool -> ?non_int:bool -> SymbolPath.t -> t
 
   let make_onevalue : make_t =
-   fun ~unsigned ?(boolean = false) path -> OneValue {unsigned; boolean; path}
+   fun ~unsigned ?(non_int = false) path -> OneValue {unsigned; non_int; path}
 
 
   let make_boundend : BoundEnd.t -> make_t =
-   fun bound_end ~unsigned ?(boolean = false) path -> BoundEnd {unsigned; boolean; path; bound_end}
+   fun bound_end ~unsigned ?(non_int = false) path -> BoundEnd {unsigned; non_int; 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 is_non_int : t -> bool = function OneValue {non_int} | BoundEnd {non_int} -> non_int
 
   let path = function OneValue {path} | BoundEnd {path} -> path
 

infer/src/bufferoverrun/symb.mli

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

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

@@ -152,4 +152,22 @@ public class Cost_test {
       }
     }
   }
+
+  // Cost should not include the symbol of f.
+  void ignore_float_symbols_constant(float f) {
+    for (; f < (float) 1.0; ) {
+      if (rand()) {
+        f = (float) 1.0;
+      }
+    }
+  }
+
+  // Cost should not include the symbol of d.
+  void ignore_double_symbols_constant(double d) {
+    for (; d < (double) 1.0; ) {
+      if (rand()) {
+        d = 1.0;
+      }
+    }
+  }
 }