[inferbo] Extend bound domain to express multiplication of bounds

Summary: This diff extends the bound domain to express multiplication of bounds in some simple cases.

Reviewed By: ezgicicek

Differential Revision: D18745246

fbshipit-source-id: 4f2dcb42c

infer/src/bufferoverrun/bounds.ml

@@ -225,14 +225,18 @@ module Bound = struct
      fun fmt -> function Min -> F.pp_print_string fmt "min" | Max -> F.pp_print_string fmt "max"
   end
 
-  (* MinMax constructs a bound that is in the "int [+|-] [min|max](int, Symb.Symbol)" format.
-     e.g. `MinMax (1, Minus, Max, 2, s)` means "1 - max (2, s)". *)
   type t =
-    | MInf
+    | MInf  (** -oo *)
     | Linear of Z.t * SymLinear.t
+        (** [Linear (c, se)] represents [c+se] where [se] is Σ(c⋅x). *)
     | MinMax of Z.t * Sign.t * MinMax.t * Z.t * Symb.Symbol.t
-    | MinMaxB of MinMax.t * t * t
-    | PInf
+        (** [MinMax] represents a bound of "int [+|-] [min|max](int, symbol)" format.  For example,
+            [MinMax (1, Minus, Max, 2, s)] represents [1-max(2,s)]. *)
+    | MinMaxB of MinMax.t * t * t  (** [MinMaxB] represents a min/max of two bounds. *)
+    | MultB of Z.t * t * t
+        (** [MultB] represents a multiplication of two bounds.  For example, [MultB (1, x, y)]
+            represents [1 + x × y]. *)
+    | PInf  (** +oo *)
   [@@deriving compare]
 
   type eval_sym = t Symb.Symbol.eval
@@ -252,24 +256,30 @@ module Bound = struct
 
 
   let rec pp_mark : markup:bool -> F.formatter -> t -> unit =
-   fun ~markup f -> function
-    | MInf ->
-        F.pp_print_string f "-oo"
-    | PInf ->
-        F.pp_print_string f "+oo"
-    | Linear (c, x) ->
-        if SymLinear.is_zero x then Z.pp_print f c
-        else (
-          SymLinear.pp ~markup ~is_beginning:true f x ;
-          if not Z.(equal c zero) then
-            if Z.gt c Z.zero then F.fprintf f " + %a" Z.pp_print c
-            else F.fprintf f " - %a" Z.pp_print (Z.neg c) )
-    | MinMax (c, sign, m, d, x) ->
-        if Z.(equal c zero) then (Sign.pp ~need_plus:false) f sign
-        else F.fprintf f "%a%a" Z.pp_print c (Sign.pp ~need_plus:true) sign ;
-        F.fprintf f "%a(%a, %a)" MinMax.pp m Z.pp_print d (Symb.Symbol.pp_mark ~markup) x
-    | MinMaxB (m, x, y) ->
-        F.fprintf f "%a(%a, %a)" MinMax.pp m (pp_mark ~markup) x (pp_mark ~markup) y
+    let pp_c f c =
+      if not Z.(equal c zero) then
+        if Z.gt c Z.zero then F.fprintf f " + %a" Z.pp_print c
+        else F.fprintf f " - %a" Z.pp_print (Z.neg c)
+    in
+    fun ~markup f -> function
+      | MInf ->
+          F.pp_print_string f "-oo"
+      | PInf ->
+          F.pp_print_string f "+oo"
+      | Linear (c, x) ->
+          if SymLinear.is_zero x then Z.pp_print f c
+          else (
+            SymLinear.pp ~markup ~is_beginning:true f x ;
+            pp_c f c )
+      | MinMax (c, sign, m, d, x) ->
+          if Z.(equal c zero) then (Sign.pp ~need_plus:false) f sign
+          else F.fprintf f "%a%a" Z.pp_print c (Sign.pp ~need_plus:true) sign ;
+          F.fprintf f "%a(%a, %a)" MinMax.pp m Z.pp_print d (Symb.Symbol.pp_mark ~markup) x
+      | MinMaxB (m, x, y) ->
+          F.fprintf f "%a(%a, %a)" MinMax.pp m (pp_mark ~markup) x (pp_mark ~markup) y
+      | MultB (c, x, y) ->
+          F.fprintf f "%a%s%a%a" (pp_mark ~markup) x SpecialChars.multiplication_sign
+            (pp_mark ~markup) y pp_c c
 
 
   let pp = pp_mark ~markup:false
@@ -358,7 +368,7 @@ module Bound = struct
         not (SymLinear.is_empty se)
     | MinMax _ ->
         true
-    | MinMaxB (_, x, y) ->
+    | MinMaxB (_, x, y) | MultB (_, x, y) ->
         is_symbolic x || is_symbolic y
 
 
@@ -376,6 +386,11 @@ module Bound = struct
     else MinMax (c, sign, m, d, s)
 
 
+  let mk_MultB (n, x, y) =
+    (* NOTE: We have some simplication opportunities here. *)
+    MultB (n, x, y)
+
+
   let big_int_ub_of_minmax = function
     | MinMax (c, Plus, Min, d, _) ->
         Some Z.(c + d)
@@ -385,7 +400,7 @@ module Bound = struct
         Some c
     | MinMax _ ->
         None
-    | MinMaxB _ | MInf | PInf | Linear _ ->
+    | MinMaxB _ | MultB _ | MInf | PInf | Linear _ ->
         assert false
 
 
@@ -398,7 +413,7 @@ module Bound = struct
         Some c
     | MinMax _ ->
         None
-    | MinMaxB _ | MInf | PInf | Linear _ ->
+    | MinMaxB _ | MultB _ | MInf | PInf | Linear _ ->
         assert false
 
 
@@ -410,7 +425,7 @@ module Bound = struct
 
 
   let rec big_int_lb = function
-    | MInf ->
+    | MInf | MultB _ ->
         None
     | PInf ->
         assert false
@@ -425,7 +440,7 @@ module Bound = struct
   let rec big_int_ub = function
     | MInf ->
         assert false
-    | PInf ->
+    | PInf | MultB _ ->
         None
     | MinMax _ as b ->
         big_int_ub_of_minmax b
@@ -442,7 +457,7 @@ module Bound = struct
         Some (Linear (c, SymLinear.singleton_minus_one x))
     | MinMax _ ->
         None
-    | MinMaxB _ | MInf | PInf | Linear _ ->
+    | MinMaxB _ | MultB _ | MInf | PInf | Linear _ ->
         assert false
 
 
@@ -453,7 +468,7 @@ module Bound = struct
         Some (Linear (c, SymLinear.singleton_minus_one x))
     | MinMax _ ->
         None
-    | MinMaxB _ | MInf | PInf | Linear _ ->
+    | MinMaxB _ | MultB _ | MInf | PInf | Linear _ ->
         assert false
 
 
@@ -476,6 +491,11 @@ module Bound = struct
         true
     | _, MInf | PInf, _ ->
         false
+    | MultB (xc, x1, x2), MultB (yc, y1, y2) ->
+        (* NOTE: We define the order for only straightforward cases. *)
+        Z.leq xc yc && equal x1 y1 && equal x2 y2
+    | MultB _, _ | _, MultB _ ->
+        false
     | Linear (c0, x0), Linear (c1, x1) ->
         c0 <= c1 && SymLinear.le x0 x1
     | MinMax _, MinMax _ when le_minmax_by_int x y ->
@@ -517,6 +537,11 @@ module Bound = struct
     match (x, y) with
     | MInf, Linear _ | MInf, MinMax _ | MInf, PInf | Linear _, PInf | MinMax _, PInf ->
         true
+    | MultB (xc, x1, x2), MultB (yc, y1, y2) ->
+        (* NOTE: We define the order for only straightforward cases. *)
+        Z.lt xc yc && equal x1 y1 && equal x2 y2
+    | MultB _, _ | _, MultB _ ->
+        false
     | Linear (c, x), _ ->
         le (Linear (Z.succ c, x)) y
     | MinMax (c, sign, min_max, d, x), _ ->
@@ -567,6 +592,8 @@ module Bound = struct
         mk_MinMax (Z.neg c, Sign.neg sign, min_max, d, x)
     | MinMaxB (m, x, y) ->
         mk_MinMaxB (MinMax.neg m, neg x, neg y)
+    | MultB (c, x, y) ->
+        mk_MultB (Z.neg c, neg x, y)
 
 
   let exact_min : otherwise:(t -> t -> t) -> t -> t -> t =
@@ -881,6 +908,9 @@ module Bound = struct
           mk_MinMax (c, Sign.neg sign, MinMax.neg min_max, d, x1)
       | MinMaxB (m, x, y), z ->
           mk_MinMaxB (m, plus_exact ~weak ~otherwise x z, plus_exact ~weak ~otherwise y z)
+      | (MultB (c, x1, x2), Linear (d, se) | Linear (d, se), MultB (c, x1, x2))
+        when SymLinear.is_zero se ->
+          mk_MultB (Z.add c d, x1, x2)
       | _ ->
           otherwise x y
 
@@ -943,6 +973,8 @@ module Bound = struct
               of_bound_end bound_end )
       | MinMaxB (m, x, y) ->
           mk_MinMaxB (m, mult_const bound_end n x, mult_const bound_end n y)
+      | MultB _ ->
+          of_bound_end bound_end
 
 
   let mult_const_l = mult_const Symb.BoundEnd.LowerBound
@@ -1000,7 +1032,7 @@ module Bound = struct
         SymLinear.get_symbols se
     | MinMax (_, _, _, _, s) ->
         Symb.SymbolSet.singleton s
-    | MinMaxB (_, x, y) ->
+    | MinMaxB (_, x, y) | MultB (_, x, y) ->
         Symb.SymbolSet.union (get_symbols x) (get_symbols y)
 
 
@@ -1076,9 +1108,11 @@ module Bound = struct
           | NonBottom x' ->
               let res =
                 match (sign, min_max, x') with
-                | Plus, Min, (MInf | MinMaxB _) | Minus, Max, (PInf | MinMaxB _) ->
+                | Plus, Min, (MInf | MinMaxB _ | MultB _) | Minus, Max, (PInf | MinMaxB _ | MultB _)
+                  ->
                     MInf
-                | Plus, Max, (PInf | MinMaxB _) | Minus, Min, (MInf | MinMaxB _) ->
+                | Plus, Max, (PInf | MinMaxB _ | MultB _) | Minus, Min, (MInf | MinMaxB _ | MultB _)
+                  ->
                     PInf
                 | sign, Min, PInf | sign, Max, MInf ->
                     of_big_int (Sign.eval_big_int sign c d)
@@ -1125,12 +1159,23 @@ module Bound = struct
                               (big_int_of_minmax bound_end x' |> Option.value ~default:d))) )
               in
               NonBottom res )
-      | MinMaxB (m, x, y) -> (
-        match (subst ~subst_pos x eval_sym, subst ~subst_pos y eval_sym) with
-        | Bottom, _ | _, Bottom ->
-            Bottom
-        | NonBottom x, NonBottom y ->
-            NonBottom (mk_MinMaxB (m, x, y)) )
+      | MinMaxB (m, x, y) ->
+          subst2_merge ~subst_pos x y eval_sym ~f:(fun x y -> mk_MinMaxB (m, x, y))
+      | MultB (c, x, y) when le zero x && le zero y ->
+          subst2_merge ~subst_pos x y eval_sym ~f:(fun x y -> mk_MultB (c, x, y))
+      | MultB (c, x, y) when le x zero && le y zero ->
+          let subst_pos = Symb.BoundEnd.neg subst_pos in
+          subst2_merge ~subst_pos x y eval_sym ~f:(fun x y -> mk_MultB (c, x, y))
+      | MultB _ ->
+          NonBottom (of_bound_end subst_pos)
+
+
+  and subst2_merge ~subst_pos x y eval_sym ~f =
+    match (subst ~subst_pos x eval_sym, subst ~subst_pos y eval_sym) with
+    | Bottom, _ | _, Bottom ->
+        Bottom
+    | NonBottom x, NonBottom y ->
+        NonBottom (f x y)
 
 
   let subst_lb x eval_sym = subst ~subst_pos:Symb.BoundEnd.LowerBound x eval_sym
@@ -1157,6 +1202,10 @@ module Bound = struct
         let a' = simplify_bound_ends_from_paths a in
         let b' = simplify_bound_ends_from_paths b in
         if phys_equal a a' && phys_equal b b' then x else mk_MinMaxB (m, a', b')
+    | MultB (c, a, b) ->
+        let a' = simplify_bound_ends_from_paths a in
+        let b' = simplify_bound_ends_from_paths b in
+        if phys_equal a a' && phys_equal b b' then x else mk_MultB (c, a', b')
 
 
   let get_same_one_symbol b1 b2 =
@@ -1167,6 +1216,8 @@ module Bound = struct
         None
 
 
+  let is_same_one_symbol b1 b2 = Option.is_some (get_same_one_symbol b1 b2)
+
   let rec exists_str ~f = function
     | MInf | PInf ->
         false
@@ -1174,7 +1225,7 @@ module Bound = struct
         SymLinear.exists_str ~f s
     | MinMax (_, _, _, _, s) ->
         Symb.Symbol.exists_str ~f s
-    | MinMaxB (_, x, y) ->
+    | MinMaxB (_, x, y) | MultB (_, x, y) ->
         exists_str ~f x || exists_str ~f y
 end
 
@@ -1297,4 +1348,8 @@ module NonNegativeBound = struct
         Constant NonNegativeInt.zero
     | NonBottom b ->
         of_bound b ~trace:(BoundTrace.call ~callee_pname ~location callee_trace) |> classify
+
+
+  let split_mult (b, trace) =
+    match b with Bound.MultB (_, b1, b2) -> Some ((b1, trace), (b2, trace)) | _ -> None
 end

infer/src/bufferoverrun/bounds.mli

@@ -11,6 +11,10 @@ module F = Format
 module Bound : sig
   type t
 
+  val mk_MultB : Z.t * t * t -> t
+  (** It makes a bound of [Bound.MultB], which represents a multiplication of two bounds.  For
+     example, [MultB (1, x, y)] represents [1 + x × y].  *)
+
   type eval_sym = t Symb.Symbol.eval
 
   val compare : t -> t -> int
@@ -123,6 +127,10 @@ module Bound : sig
   val simplify_min_one : t -> t
 
   val get_same_one_symbol : t -> t -> Symb.SymbolPath.t option
+  (** It returns a symbol [s] when the two bounds are all linear expressions of the symbol [1⋅s]. *)
+
+  val is_same_one_symbol : t -> t -> bool
+  (** It returns [true] when the two bounds are linear expressions of the same one symbol [1⋅s]. *)
 
   val exists_str : f:(string -> bool) -> t -> bool
 end
@@ -174,4 +182,6 @@ module NonNegativeBound : sig
     -> t
     -> Bound.eval_sym
     -> (Ints.NonNegativeInt.t, t, BoundTrace.t) valclass
+
+  val split_mult : t -> (t * t) option
 end

infer/src/bufferoverrun/itv.ml

@@ -186,6 +186,8 @@ module ItvPure = struct
 
   let is_le_mone : t -> bool = fun (_, ub) -> Bound.le ub Bound.mone
 
+  let is_same_one_symbol (l, u) = Bound.is_same_one_symbol l u
+
   let range : Location.t -> t -> ItvRange.t =
    fun loop_head_loc (lb, ub) -> ItvRange.of_bounds ~loop_head_loc ~lb ~ub
 
@@ -269,7 +271,9 @@ module ItvPure = struct
     | Some n, _ ->
         mult_const n y
     | None, None ->
-        top
+        if is_same_one_symbol x && is_same_one_symbol y then
+          (Bound.mk_MultB (Z.zero, lb x, lb y), Bound.mk_MultB (Z.zero, ub x, ub y))
+        else top
 
 
   let div : t -> t -> t = fun x y -> match get_const y with None -> top | Some n -> div_const x n

infer/src/bufferoverrun/polynomials.ml

@@ -72,6 +72,8 @@ module type NonNegativeSymbol = sig
     -> (NonNegativeInt.t, t, Bounds.BoundTrace.t) Bounds.valclass
 
   val pp : hum:bool -> F.formatter -> t -> unit
+
+  val split_mult : t -> (t * t) option
 end
 
 module type NonNegativeSymbolWithDegreeKind = sig
@@ -84,6 +86,8 @@ module type NonNegativeSymbolWithDegreeKind = sig
   val degree_kind : t -> DegreeKind.t
 
   val symbol : t -> t0
+
+  val split_mult : t -> (t * t) option
 end
 
 module MakeSymbolWithDegreeKind (S : NonNegativeSymbol) :
@@ -130,6 +134,9 @@ module MakeSymbolWithDegreeKind (S : NonNegativeSymbol) :
   let degree_kind {degree_kind} = degree_kind
 
   let symbol {symbol} = symbol
+
+  let split_mult {degree_kind; symbol} =
+    Option.map (S.split_mult symbol) ~f:(fun (s1, s2) -> (make degree_kind s1, make degree_kind s2))
 end
 
 module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
@@ -209,15 +216,6 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
 
   let of_int_exn : int -> t = fun i -> i |> NonNegativeInt.of_int_exn |> of_non_negative_int
 
-  let of_valclass : (NonNegativeInt.t, S.t, 't) Bounds.valclass -> (t, 't) below_above = function
-    | ValTop trace ->
-        Above trace
-    | Constant i ->
-        Below (of_non_negative_int i)
-    | Symbolic s ->
-        Below {const= NonNegativeInt.zero; terms= M.singleton s one}
-
-
   let is_zero : t -> bool = fun {const; terms} -> NonNegativeInt.is_zero const && M.is_empty terms
 
   let is_one : t -> bool = fun {const; terms} -> NonNegativeInt.is_one const && M.is_empty terms
@@ -272,6 +270,24 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
       mult_const p1 p2.const |> M.fold (fun s p acc -> plus (mult_symb (mult p p1) s) acc) p2.terms
 
 
+  let rec of_valclass : (NonNegativeInt.t, S.t, 't) Bounds.valclass -> (t, 't) below_above =
+    function
+    | ValTop trace ->
+        Above trace
+    | Constant i ->
+        Below (of_non_negative_int i)
+    | Symbolic s -> (
+      match S.split_mult s with
+      | None ->
+          Below {const= NonNegativeInt.zero; terms= M.singleton s one}
+      | Some (s1, s2) -> (
+        match (of_valclass (S.classify s1), of_valclass (S.classify s2)) with
+        | Below s1, Below s2 ->
+            Below (mult s1 s2)
+        | (Above _ as t), _ | _, (Above _ as t) ->
+            t ) )
+
+
   let rec int_lb {const; terms} =
     M.fold
       (fun symbol polynomial acc ->

infer/tests/codetoanalyze/cpp/quandaryBO/codec.cpp

@@ -46,7 +46,7 @@ uint64_t getP_Bad(uint64_t w) {
   auto w4m1o15p1 = w4m1o15 + 1; // BUG: can overflow
   return w4m1o15p1;
 }
-uint64_t checkedMultiply_Good_FP(uint64_t a, uint64_t b) {
+uint64_t checkedMultiply_Good(uint64_t a, uint64_t b) {
   __uint128_t mul = ((__uint128_t)a) * b; // OK: no overflow
   if ((mul >> 64) != 0) {
     throw std::runtime_error("Detected overflow in checked multiplcation");
@@ -54,11 +54,11 @@ uint64_t checkedMultiply_Good_FP(uint64_t a, uint64_t b) {
   auto result = (uint64_t)mul; // OK: within the bounds
   return result;
 }
-void foo_Bad_FN() {
+void foo_Bad_FN_FP() {
   int w = __infer_taint_source();
   int h = __infer_taint_source();
   auto p = getP_Bad(w); // MISSED BUG: casting signed int64 -> unsigned int64
-  auto s = checkedMultiply_Good_FP(h, p); // OK
+  auto s = checkedMultiply_Good(h, p); // OK, FP
   auto d = std::make_unique<uint8_t[]>(s); // OK
 }
 } // namespace Codec_Bad2

infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t1

@@ -1,4 +1,4 @@
-codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::foo_Bad_FN, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,<LHS trace>,Parameter `w`,Assignment,Binary operation: ([0, +oo] - 1):unsigned64 by call to `Codec_Bad2::getP_Bad` ]
+codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::foo_Bad_FN_FP, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,<LHS trace>,Parameter `w`,Assignment,Binary operation: ([0, +oo] - 1):unsigned64 by call to `Codec_Bad2::getP_Bad` ]
 codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad::foo_Bad_FN, 4, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,<LHS trace>,Parameter `w`,Assignment,Binary operation: ([0, +oo] - 1):unsigned32 by call to `Codec_Bad::getP_Bad` ]
 codetoanalyze/cpp/quandaryBO/tainted_index.cpp, basic_bad, 3, TAINTED_BUFFER_ACCESS, no_bucket, ERROR, [Return from __infer_taint_source,Call to __array_access with tainted index 0,-----------,<Offset trace>,Unknown value from: __infer_taint_source,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 10]
 codetoanalyze/cpp/quandaryBO/tainted_index.cpp, memory_alloc_bad2, 3, TAINTED_MEMORY_ALLOCATION, no_bucket, ERROR, [Return from __infer_taint_source,Call to __set_array_length with tainted index 1,-----------,Unknown value from: __infer_taint_source,Assignment,Allocation: Length: [-oo, 2147483647]]

infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t2

@@ -1,4 +1,4 @@
-codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::foo_Bad_FN, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,<LHS trace>,Parameter `w`,Assignment,Binary operation: ([0, +oo] - 1):unsigned64 by call to `Codec_Bad2::getP_Bad` ]
+codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::foo_Bad_FN_FP, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,<LHS trace>,Parameter `w`,Assignment,Binary operation: ([0, +oo] - 1):unsigned64 by call to `Codec_Bad2::getP_Bad` ]
 codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad::foo_Bad_FN, 4, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,<LHS trace>,Parameter `w`,Assignment,Binary operation: ([0, +oo] - 1):unsigned32 by call to `Codec_Bad::getP_Bad` ]
 codetoanalyze/cpp/quandaryBO/tainted_index.cpp, basic_bad, 3, TAINTED_BUFFER_ACCESS, no_bucket, ERROR, [Return from __infer_taint_source,Call to __array_access with tainted index 0,-----------,<Offset trace>,Unknown value from: __infer_taint_source,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 10]
 codetoanalyze/cpp/quandaryBO/tainted_index.cpp, basic_bad, 3, UNTRUSTED_BUFFER_ACCESS, no_bucket, ERROR, [Return from __infer_taint_source,Call to __array_access with tainted index 0]

infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t3

@@ -1,4 +1,4 @@
-codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::foo_Bad_FN, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,<LHS trace>,Parameter `w`,Assignment,Binary operation: ([0, +oo] - 1):unsigned64 by call to `Codec_Bad2::getP_Bad` ]
+codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::foo_Bad_FN_FP, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,<LHS trace>,Parameter `w`,Assignment,Binary operation: ([0, +oo] - 1):unsigned64 by call to `Codec_Bad2::getP_Bad` ]
 codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad::foo_Bad_FN, 4, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,<LHS trace>,Parameter `w`,Assignment,Binary operation: ([0, +oo] - 1):unsigned32 by call to `Codec_Bad::getP_Bad` ]
 codetoanalyze/cpp/quandaryBO/tainted_index.cpp, basic_bad, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Offset trace>,Unknown value from: __infer_taint_source,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 10]
 codetoanalyze/cpp/quandaryBO/tainted_index.cpp, basic_bad, 3, TAINTED_BUFFER_ACCESS, no_bucket, ERROR, [Return from __infer_taint_source,Call to __array_access with tainted index 0,-----------,<Offset trace>,Unknown value from: __infer_taint_source,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 10]

infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t4

@@ -1,7 +1,7 @@
-codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::checkedMultiply_Good_FP, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `a`,<RHS trace>,Parameter `b`,Binary operation: (a × b):unsigned32]
-codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::checkedMultiply_Good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
-codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::foo_Bad_FN, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,<LHS trace>,Parameter `w`,Assignment,Binary operation: ([0, +oo] - 1):unsigned64 by call to `Codec_Bad2::getP_Bad` ]
-codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::foo_Bad_FN, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,<LHS trace>,Parameter `w`,Binary operation: ([0, +oo] × 4):unsigned64 by call to `Codec_Bad2::getP_Bad` ]
+codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::checkedMultiply_Good, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
+codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::foo_Bad_FN_FP, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,<LHS trace>,Parameter `w`,Assignment,Binary operation: ([0, +oo] - 1):unsigned64 by call to `Codec_Bad2::getP_Bad` ]
+codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::foo_Bad_FN_FP, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,<LHS trace>,Parameter `w`,Binary operation: ([0, +oo] × 4):unsigned64 by call to `Codec_Bad2::getP_Bad` ]
+codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::foo_Bad_FN_FP, 4, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,<LHS trace>,Parameter `a`,<RHS trace>,Parameter `b`,Binary operation: ([0, +oo] × [0, +oo]):unsigned32 by call to `Codec_Bad2::checkedMultiply_Good` ]
 codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::getP_Bad, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `w`,Assignment,Assignment,Assignment,Binary operation: ([-oo, +oo] + 1):unsigned64]
 codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad::foo_Bad_FN, 4, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,<LHS trace>,Parameter `w`,Assignment,Binary operation: ([0, +oo] - 1):unsigned32 by call to `Codec_Bad::getP_Bad` ]
 codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad::foo_Bad_FN, 5, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Unknown value from: __infer_taint_source,Assignment,<RHS trace>,Call,Parameter `w`,Assignment,Assignment,Assignment,Assignment,Assignment,Assignment,Binary operation: ([-oo, +oo] × [-oo, +oo]):unsigned32]

infer/tests/codetoanalyze/java/performance/CantHandle.java

@@ -26,8 +26,8 @@ class CantHandle {
       i++;
     }
   }
-  // Expected: x^2, got T
-  void quadratic_FP(int x) {
+  // Expected: x^2, got x^2
+  void quadratic(int x) {
     for (int i = 0; i < x * x; i++) {}
   }
 }

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

@@ -206,6 +206,10 @@ public class Cost_test {
   void band_constant(int x) {
     for (int i = 0; i < (int) (x & 0xff); i++) {}
   }
+
+  void mult_symbols_quadratic(int x, int y) {
+    for (int i = 0; i < x * y; i++) {}
+  }
 }
 
 class CloneTest {

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

@@ -57,9 +57,7 @@ codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.substitute_arra
 codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_constant(int):int, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 7 ⋅ p, O(p), degree = 1,{p},call to int Break.break_loop(int,int),Loop at line 12]
 codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_loop(int,int):int, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 7 ⋅ p, O(p), degree = 1,{p},Loop at line 12]
 codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 4 ⋅ maxI + 3 ⋅ maxI × (min(12, maxJ)) + 5 ⋅ maxI × (12-max(0, maxJ)) + 5 ⋅ (min(11, maxI)) × (min(11, maxJ)), O(maxI × maxJ), degree = 2,{min(11, maxJ)},Loop at line 37,{min(11, maxI)},Loop at line 35,{12-max(0, maxJ)},Loop at line 35,{min(12, maxJ)},Loop at line 37,{maxI},Loop at line 35]
-codetoanalyze/java/performance/CantHandle.java, CantHandle.quadratic_FP(int):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 31]
-codetoanalyze/java/performance/CantHandle.java, CantHandle.quadratic_FP(int):void, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `x`,<RHS trace>,Parameter `x`,Binary operation: (x × x):signed32]
-codetoanalyze/java/performance/CantHandle.java, CantHandle.quadratic_FP(int):void, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `x`,Binary operation: ([0, +oo] + 1):signed32]
+codetoanalyze/java/performance/CantHandle.java, CantHandle.quadratic(int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 6 ⋅ x², O(x²), degree = 2,{x},Loop at line 31,{x},Loop at line 31]
 codetoanalyze/java/performance/CantHandle.java, CantHandle.square_root_FP(int):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 17]
 codetoanalyze/java/performance/CantHandle.java, CantHandle.square_root_FP(int):void, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Assignment,Binary operation: ([0, +oo] × [0, +oo]):signed32]
 codetoanalyze/java/performance/CantHandle.java, CantHandle.square_root_FP(int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
@@ -101,6 +99,7 @@ codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Co
 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]
 codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.loop_on_unknown_global_linear():void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ codetoanalyze.java.performance.Cost_test.global + 5 ⋅ (1+max(0, codetoanalyze.java.performance.Cost_test.global)), O(codetoanalyze.java.performance.Cost_test.global), degree = 1,{1+max(0, codetoanalyze.java.performance.Cost_test.global)},Loop at line 203,{codetoanalyze.java.performance.Cost_test.global},Loop at line 203]
 codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.main_bad():int, 7, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 205, O(1), degree = 0]
+codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.mult_symbols_quadratic(int,int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 6 ⋅ x × y, O(x × y), degree = 2,{y},Loop at line 211,{x},Loop at line 211]
 codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.if_bad(int):void, 6, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 613, O(1), degree = 0]
 codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.if_bad_loop():int, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 201, O(1), degree = 0]
 codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.if_bad_loop():int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
@@ -169,7 +168,6 @@ codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 250, O(1), degree = 0]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 25 ⋅ (length - 1), O(length), degree = 1,{length - 1},Loop at line 44]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 3 + 59 ⋅ (length - 1) × (length - 1) + 8 ⋅ length, O(length × length), degree = 2,{length},Loop at line 54,{length - 1},Loop at line 55,{length - 1},Loop at line 54]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `a[*]`,<RHS trace>,Parameter `b[*]`,Binary operation: (a[*] × b[*]):signed64]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.length_of_linked_list_linear_FP(codetoanalyze.java.performance.Loops$MyLinkedList):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded value x,call to void Loops.linear(int),Loop at line 86]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.length_of_linked_list_linear_FP(codetoanalyze.java.performance.Loops$MyLinkedList):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.linear(int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ x, O(x), degree = 1,{x},Loop at line 86]