pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[inferbo] Simplify and improve Itv.prune_comp

Browse Source 
Reviewed By: skcho

Differential Revision: D10386789

fbshipit-source-id: f9c7e33ef
master
Mehdi Bouaziz 6 years ago committed by Facebook Github Bot
parent 2824056af5
commit 3ee96263a7
10 changed files with 111 additions and 158 deletions
Show Stats Download Patch File Download Diff File

30
infer/src/bufferoverrun/bounds.ml
Unescape View File

@ -61,14 +61,6 @@ module SymLinear = struct
(singleton_one lb, singleton_one ub)
let eq : t -> t -> bool =
fun x y ->
let eq_pair _ (coeff1 : NonZeroInt.t option) (coeff2 : NonZeroInt.t option) =
[%compare.equal: Z.t option] (coeff1 :> Z.t option) (coeff2 :> Z.t option)
in
M.for_all2 ~f:eq_pair x y
let pp1 : F.formatter -> Symb.Symbol.t * NonZeroInt.t -> unit =
fun fmt (s, c) ->
let c = (c :> Z.t) in
@ -269,28 +261,6 @@ module Bound = struct
true
let lift_symlinear : (SymLinear.t -> 'a option) -> t -> 'a option =
fun f -> function Linear (n, se) when Z.(equal n zero) -> f se | _ -> None
let get_one_symbol_opt : t -> Symb.Symbol.t option = lift_symlinear SymLinear.get_one_symbol_opt
let get_mone_symbol_opt : t -> Symb.Symbol.t option =
lift_symlinear SymLinear.get_mone_symbol_opt
let get_one_symbol : t -> Symb.Symbol.t =
fun x -> match get_one_symbol_opt x with Some s -> s | None -> raise Not_One_Symbol
let get_mone_symbol : t -> Symb.Symbol.t =
fun x -> match get_mone_symbol_opt x with Some s -> s | None -> raise Not_One_Symbol
let is_one_symbol : t -> bool = fun x -> get_one_symbol_opt x <> None
let is_mone_symbol : t -> bool = fun x -> get_mone_symbol_opt x <> None
let mk_MinMax (c, sign, m, d, s) =
if Symb.Symbol.is_unsigned s && Z.(d <= zero) then
match m with

16
infer/src/bufferoverrun/bounds.mli
Unescape View File

@ -22,10 +22,6 @@ module SymLinear : sig
-> Symb.SymbolPath.t
-> Counter.t
-> t * t
val eq : t -> t -> bool
val is_zero : t -> bool
end
module Bound : sig
@ -57,16 +53,6 @@ module Bound : sig
val is_symbolic : t -> bool
val get_one_symbol : t -> Symb.Symbol.t
val get_mone_symbol : t -> Symb.Symbol.t
val is_one_symbol : t -> bool
val is_mone_symbol : t -> bool
val mk_MinMax : Z.t * sign * min_max * Z.t * Symb.Symbol.t -> t
val big_int_lb : t -> Z.t sexp_option
val big_int_ub : t -> Z.t sexp_option
@ -85,6 +71,8 @@ module Bound : sig
val overapprox_min : t -> t -> t
val underapprox_max : t -> t -> t
val overapprox_max : t -> t -> t
val widen_l : t -> t -> t

62
infer/src/bufferoverrun/itv.ml
Unescape View File

@ -740,67 +740,9 @@ module ItvPure = struct
Bottom
let prune_le : t -> t -> t =
fun x y ->
match (x, y) with
| (l1, Bound.PInf), (_, u2) ->
(l1, u2)
| (l1, Bound.Linear (c1, s1)), (_, Bound.Linear (c2, s2)) when Bounds.SymLinear.eq s1 s2 ->
(l1, Bound.Linear (Z.(min c1 c2), s1))
| (l1, Bound.Linear (c, se)), (_, u) when Bounds.SymLinear.is_zero se && Bound.is_one_symbol u
->
(l1, Bound.mk_MinMax (Z.zero, Bound.Plus, Bound.Min, c, Bound.get_one_symbol u))
| (l1, u), (_, Bound.Linear (c, se)) when Bounds.SymLinear.is_zero se && Bound.is_one_symbol u
->
(l1, Bound.mk_MinMax (Z.zero, Bound.Plus, Bound.Min, c, Bound.get_one_symbol u))
| (l1, Bound.Linear (c, se)), (_, u) when Bounds.SymLinear.is_zero se && Bound.is_mone_symbol u
->
(l1, Bound.mk_MinMax (Z.zero, Bound.Minus, Bound.Max, Z.neg c, Bound.get_mone_symbol u))
| (l1, u), (_, Bound.Linear (c, se)) when Bounds.SymLinear.is_zero se && Bound.is_mone_symbol u
->
(l1, Bound.mk_MinMax (Z.zero, Bound.Minus, Bound.Max, Z.neg c, Bound.get_mone_symbol u))
| (l1, Bound.Linear (c1, se)), (_, Bound.MinMax (c2, Bound.Plus, Bound.Min, d2, se'))
| (l1, Bound.MinMax (c2, Bound.Plus, Bound.Min, d2, se')), (_, Bound.Linear (c1, se))
when Bounds.SymLinear.is_zero se ->
(l1, Bound.mk_MinMax (c2, Bound.Plus, Bound.Min, Z.(min (c1 - c2) d2), se'))
| ( (l1, Bound.MinMax (c1, Bound.Plus, Bound.Min, d1, se1))
, (_, Bound.MinMax (c2, Bound.Plus, Bound.Min, d2, se2)) )
when Z.equal c1 c2 && Symbol.equal se1 se2 ->
(l1, Bound.mk_MinMax (c1, Bound.Plus, Bound.Min, Z.min d1 d2, se1))
| _ ->
x
let prune_ge : t -> t -> t =
fun x y ->
match (x, y) with
| (Bound.MInf, u1), (l2, _) ->
(l2, u1)
| (Bound.Linear (c1, s1), u1), (Bound.Linear (c2, s2), _) when Bounds.SymLinear.eq s1 s2 ->
(Bound.Linear (Z.max c1 c2, s1), u1)
| (Bound.Linear (c, se), u1), (l, _) when Bounds.SymLinear.is_zero se && Bound.is_one_symbol l
->
(Bound.mk_MinMax (Z.zero, Bound.Plus, Bound.Max, c, Bound.get_one_symbol l), u1)
| (l, u1), (Bound.Linear (c, se), _) when Bounds.SymLinear.is_zero se && Bound.is_one_symbol l
->
(Bound.mk_MinMax (Z.zero, Bound.Plus, Bound.Max, c, Bound.get_one_symbol l), u1)
| (Bound.Linear (c, se), u1), (l, _) when Bounds.SymLinear.is_zero se && Bound.is_mone_symbol l
->
(Bound.mk_MinMax (Z.zero, Bound.Minus, Bound.Min, c, Bound.get_mone_symbol l), u1)
| (l, u1), (Bound.Linear (c, se), _) when Bounds.SymLinear.is_zero se && Bound.is_mone_symbol l
->
(Bound.mk_MinMax (Z.zero, Bound.Minus, Bound.Min, c, Bound.get_mone_symbol l), u1)
| (Bound.Linear (c1, se), u1), (Bound.MinMax (c2, Bound.Plus, Bound.Max, d2, se'), _)
| (Bound.MinMax (c2, Bound.Plus, Bound.Max, d2, se'), u1), (Bound.Linear (c1, se), _)
when Bounds.SymLinear.is_zero se ->
(Bound.mk_MinMax (c2, Bound.Plus, Bound.Max, Z.(max (c1 - c2) d2), se'), u1)
| ( (Bound.MinMax (c1, Bound.Plus, Bound.Max, d1, se1), u1)
, (Bound.MinMax (c2, Bound.Plus, Bound.Max, d2, se2), _) )
when Z.equal c1 c2 && Symbol.equal se1 se2 ->
(Bound.mk_MinMax (c1, Bound.Plus, Bound.Max, Z.max d1 d2, se1), u1)
| _ ->
x
let prune_le : t -> t -> t = fun (l1, u1) (_, u2) -> (l1, Bound.overapprox_min u1 u2)
let prune_ge : t -> t -> t = fun (l1, u1) (l2, _) -> (Bound.underapprox_max l1 l2, u1)
let prune_lt : t -> t -> t = fun x y -> prune_le x (minus y one)

4
infer/tests/codetoanalyze/c/bufferoverrun/arith.c
Unescape View File

@ -273,7 +273,7 @@ void unsigned_prune_ge2_Good(unsigned int x, unsigned int y) {
}
}
void call_unsigned_prune_ge2_Good_FP() { unsigned_prune_ge2_Good(0, 1); }
void call_unsigned_prune_ge2_Good() { unsigned_prune_ge2_Good(0, 1); }
void unsigned_prune_ge3_Good(unsigned int x, unsigned int y) {
if (y > 0) {
@ -283,7 +283,7 @@ void unsigned_prune_ge3_Good(unsigned int x, unsigned int y) {
}
}
void call_unsigned_prune_ge3_Good_FP() { unsigned_prune_ge3_Good(0, 1); }
void call_unsigned_prune_ge3_Good() { unsigned_prune_ge3_Good(0, 1); }
void unsigned_prune_gt(unsigned int x, unsigned int y) {
if (x > 0) {

31
infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c
Unescape View File

@ -195,6 +195,37 @@ void l1_unknown_function_Bad() {
}
}
/*
We do not report the underrun here, in case the loop never runs (length <= 0).
But we should report it anyway.
*/
void loop_underrun_Bad_FN(int length) {
int i;
char a[length];
for (i = length - 1; i >= 0; i--) {
a[i - 1] = 'U';
}
}
void l2_loop_overflow_Bad(int length) {
int i;
char a[length];
for (i = length - 1; i >= 0; i--) {
a[i + 1] = 'O';
}
}
void l2_loop_overflow2_Bad(int length) {
int i;
char a[length];
for (i = length - 1; i >= 0; i--) {
a[length - i] = 'O';
}
}
/* Inferbo raises U5 alarm because
- the pair of offset:[10,10] and size:[5,+oo] is belong to L3
- the offset value is from an unknown function

8
infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
Unescape View File

@ -1,6 +1,4 @@
codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_ge1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 1):unsigned32 by call to `unsigned_prune_ge1_Good` ]
codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_ge2_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 1):unsigned32 by call to `unsigned_prune_ge2_Good` ]
codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_ge3_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 1):unsigned32 by call to `unsigned_prune_ge3_Good` ]
codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_zero1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 1):unsigned32 by call to `unsigned_prune_zero1_Good` ]
codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_zero2_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: y,Assignment,Binop: ([-oo, 0] - 1):unsigned32 by call to `unsigned_prune_zero2_Good` ]
codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (2000000000 + 2000000000):signed32]
@ -22,7 +20,7 @@ codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min_Bad, 2, BUFFER_OVERRUN_L2
codetoanalyze/c/bufferoverrun/arith.c, plus_one_Bad, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: unknown_int,Assignment,Binop: ([-oo, 9223372036854775807] + 1):signed64]
codetoanalyze/c/bufferoverrun/arith.c, use_int64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 15 Size: 10]
codetoanalyze/c/bufferoverrun/array_content.c, array_min_index_from_one_FP, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
codetoanalyze/c/bufferoverrun/array_content.c, call_array_min_index_from_one_good_FP, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: a,Assignment,ArrayAccess: Offset: [2, +oo] Size: 2 by call to `array_min_index_from_one_FP` ]
codetoanalyze/c/bufferoverrun/array_content.c, call_array_min_index_from_one_good_FP, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: a,Assignment,ArrayAccess: Offset: [1, +oo] Size: 2 by call to `array_min_index_from_one_FP` ]
codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr10_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_ptr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
@ -94,6 +92,8 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_no_overrun_Good_FP, 2,
codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_no_underrun_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [-1, 9] Size: 9]
codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 10] Size: 10]
codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_underrun_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [-1, 9] Size: 9]
codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_loop_overflow2_Bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Offset: [-length.ub + length.lb + 1, length.ub] Size: length]
codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_loop_overflow_Bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Offset: [1, length.ub] Size: length]
codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_symbolic_overrun_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Offset: n Size: n]
codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_no_overrun_Good_FP, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Offset: [0, 10] Size: [5, 15]]
codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_no_underrun_Good_FP, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [-1, 9] Size: 10]
@ -141,8 +141,6 @@ codetoanalyze/c/bufferoverrun/pointer_arith.c, array_pointer_arith_Bad, 3, BUFFE
codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith3_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: p,Parameter: x,ArrayAccess: Offset: 10 Size: 5 by call to `pointer_arith3` ]
codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith4_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: 10 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, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10]
codetoanalyze/c/bufferoverrun/prune_alias.c, FP_call_prune_minmax1_Ok, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: y,Binop: (0 - 1):unsigned32 by call to `prune_minmax1_Ok` ]
codetoanalyze/c/bufferoverrun/prune_alias.c, FP_call_prune_minmax2_Ok, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 2):unsigned32 by call to `prune_minmax2_Ok` ]
codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 1 Size: 1]
codetoanalyze/c/bufferoverrun/prune_alias.c, call_prune_arrblk_ne_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: x,ArrayAccess: 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: [-length.ub + length.lb + 1, length.ub] Size: length]

4
infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c
Unescape View File

@ -147,7 +147,7 @@ void prune_minmax1_Ok(unsigned int x, unsigned int y) {
}
}
void FP_call_prune_minmax1_Ok() { prune_minmax1_Ok(0, 0); }
void call_prune_minmax1_Ok() { prune_minmax1_Ok(0, 0); }
void prune_minmax2_Ok(unsigned int x, unsigned int y) {
if (x > y) {
@ -155,7 +155,7 @@ void prune_minmax2_Ok(unsigned int x, unsigned int y) {
}
}
void FP_call_prune_minmax2_Ok() { prune_minmax2_Ok(0, 2); }
void call_prune_minmax2_Ok() { prune_minmax2_Ok(0, 2); }
void loop_prune_Good(int length, int j) {
int i;

50
infer/tests/codetoanalyze/c/performance/issues.exp
Unescape View File

@ -1,12 +1,12 @@
codetoanalyze/c/performance/break.c, break_constant, 0, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 3 * p.ub + 4 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/break.c, break_loop, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 3 * p.ub + 4 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/break.c, break_loop, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 3 * p.ub + 4 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/break.c, break_loop, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 3 * p.ub + 4 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/break.c, break_loop, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 3 * p.ub + 4 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/break.c, break_loop_with_t, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 3 * p.ub + 4 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/break.c, break_loop_with_t, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 3 * p.ub + 4 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/break.c, break_loop_with_t, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 3 * p.ub + 4 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/break.c, break_loop_with_t, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 3 * p.ub + 4 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/break.c, break_constant, 0, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 5 * p.ub + 2 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/break.c, break_loop, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 * p.ub + 2 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/break.c, break_loop, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 * p.ub + 2 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/break.c, break_loop, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 * p.ub + 2 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/break.c, break_loop, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 * p.ub + 2 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/break.c, break_loop_with_t, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 * p.ub + 2 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/break.c, break_loop_with_t, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 * p.ub + 2 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/break.c, break_loop_with_t, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 * p.ub + 2 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/break.c, break_loop_with_t, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 5 * p.ub + 2 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 3 * m.ub + 4 * (1+max(0, m.ub)), degree = 1]
codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 3 * m.ub + 4 * (1+max(0, m.ub)), degree = 1]
@ -32,10 +32,10 @@ codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_an
codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_and, 12, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3528, degree = 0]
codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_shortcut, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 2 * p.ub + 5 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 2 * p.ub + 5 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 10, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 2 * p.ub + 5 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 13, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 2 * p.ub + 5 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 3 * p.ub + 4 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 3 * p.ub + 4 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 10, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 3 * p.ub + 4 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 13, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 3 * p.ub + 4 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32]
@ -108,8 +108,8 @@ codetoanalyze/c/performance/cost_test_deps.c, two_loops, 7, EXPENSIVE_EXECUTION_
codetoanalyze/c/performance/cost_test_deps.c, two_loops, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 546, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, two_loops, 10, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 548, degree = 0]
codetoanalyze/c/performance/instantiate.c, do_2K_times_Bad, 0, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 14006, degree = 0]
codetoanalyze/c/performance/instantiate.c, do_half_m2_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 * m.ub + 5 * m.ub * (max(0, m.ub)) + 2 * m.ub * (1+max(0, m.ub)) + 2 * (1+max(0, m.ub)), degree = 2]
codetoanalyze/c/performance/instantiate.c, do_half_m2_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 * m.ub + 5 * m.ub * (max(0, m.ub)) + 2 * m.ub * (1+max(0, m.ub)) + 2 * (1+max(0, m.ub)), degree = 2]
codetoanalyze/c/performance/instantiate.c, do_half_m2_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 * (m.ub + -1) * m.ub + 7 * m.ub + 2 * m.ub * (max(1, m.ub)) + 2 * (1+max(0, m.ub)), degree = 2]
codetoanalyze/c/performance/instantiate.c, do_half_m2_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 * (m.ub + -1) * m.ub + 7 * m.ub + 2 * m.ub * (max(1, m.ub)) + 2 * (1+max(0, m.ub)), degree = 2]
codetoanalyze/c/performance/instantiate.c, do_m2_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 * m.ub + 5 * m.ub^2 + 2 * m.ub * (1+max(0, m.ub)) + 2 * (1+max(0, m.ub)), degree = 2]
codetoanalyze/c/performance/instantiate.c, do_m2_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 * m.ub + 5 * m.ub^2 + 2 * m.ub * (1+max(0, m.ub)) + 2 * (1+max(0, m.ub)), degree = 2]
codetoanalyze/c/performance/instantiate.c, do_n_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 * n.ub + 2 * (1+max(0, n.ub)), degree = 1]
@ -118,16 +118,16 @@ codetoanalyze/c/performance/invariant.c, do_k_times, 2, EXPENSIVE_EXECUTION_TIME
codetoanalyze/c/performance/invariant.c, do_k_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 3 * n.ub + 2 * (1+max(0, n.ub)), degree = 1]
codetoanalyze/c/performance/invariant.c, do_k_times_array, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 6 * n.ub + 2 * (1+max(0, n.ub)), degree = 1]
codetoanalyze/c/performance/invariant.c, do_k_times_array, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 6 * n.ub + 2 * (1+max(0, n.ub)), degree = 1]
codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 3 * (max(1, n.ub)) * (1+max(0, m.ub)) + 2 * (1+max(1, n.ub)) * (2+max(0, m.ub)) + 7 * (2+max(1, n.ub)), degree = 2]
codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 3 * (max(1, n.ub)) * (1+max(0, m.ub)) + 2 * (1+max(1, n.ub)) * (2+max(0, m.ub)) + 7 * (2+max(1, n.ub)), degree = 2]
codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 3 * (max(1, n.ub)) * (1+max(0, m.ub)) + 2 * (1+max(1, n.ub)) * (2+max(0, m.ub)) + 7 * (2+max(1, n.ub)), degree = 2]
codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 3 * (max(1, n.ub)) * (1+max(0, m.ub)) + 2 * (1+max(1, n.ub)) * (2+max(0, m.ub)) + 7 * (2+max(1, n.ub)), degree = 2]
codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 3 * (max(1, n.ub)) * (1+max(0, m.ub)) + 2 * (1+max(1, n.ub)) * (2+max(0, m.ub)) + 7 * (2+max(1, n.ub)), degree = 2]
codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 * p.ub + 17 * (max(1, p.ub)) + 2 * (1+max(1, p.ub)), degree = 1]
codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 * p.ub + 17 * (max(1, p.ub)) + 2 * (1+max(1, p.ub)), degree = 1]
codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 * p.ub + 17 * (max(1, p.ub)) + 2 * (1+max(1, p.ub)), degree = 1]
codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 * p.ub + 17 * (max(1, p.ub)) + 2 * (1+max(1, p.ub)), degree = 1]
codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 * p.ub + 17 * (max(1, p.ub)) + 2 * (1+max(1, p.ub)), degree = 1]
codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 * n.ub + 3 * n.ub * m.ub + 2 * n.ub * (1+max(0, m.ub)) + 2 * (1+max(0, n.ub)), degree = 2]
codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 * n.ub + 3 * n.ub * m.ub + 2 * n.ub * (1+max(0, m.ub)) + 2 * (1+max(0, n.ub)), degree = 2]
codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 * n.ub + 3 * n.ub * m.ub + 2 * n.ub * (1+max(0, m.ub)) + 2 * (1+max(0, n.ub)), degree = 2]
codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 * n.ub + 3 * n.ub * m.ub + 2 * n.ub * (1+max(0, m.ub)) + 2 * (1+max(0, n.ub)), degree = 2]
codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 * n.ub + 3 * n.ub * m.ub + 2 * n.ub * (1+max(0, m.ub)) + 2 * (1+max(0, n.ub)), degree = 2]
codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 23 * p.ub + 2 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 23 * p.ub + 2 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 23 * p.ub + 2 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 23 * p.ub + 2 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 23 * p.ub + 2 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/c/performance/invariant.c, while_infinite_FN, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
codetoanalyze/c/performance/jump_inside_loop.c, jump_inside_loop, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2003, degree = 0]
codetoanalyze/c/performance/jump_inside_loop.c, jump_inside_loop, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2003, degree = 0]

19
infer/tests/codetoanalyze/java/performance/Loops.java
Unescape View File

@ -46,7 +46,7 @@ public class Loops {
}
}
static void dumbSort_FP(long[] a, long[] b, int length) {
static void dumbSort(long[] a, long[] b, int length) {
for (int i = length - 1; i >= 0; --i) {
for (int j = 0; j < i; ++j) {
if (a[j] * b[j + 1] > a[j + 1] * b[j]) {
@ -60,4 +60,21 @@ public class Loops {
}
}
}
public static class C {
public char c;
public float[] f;
}
static boolean similar_SHOULD_NOT_REPORT_CONDITION_ALWAYS_TRUE_OR_FALSE(C[] x, C[] y) {
if (x == null || y == null || x.length != y.length) {
return false;
}
for (int i = 0; i < x.length; i++) {
if (x[i].c != y[i].c || x[i].f.length != y[i].f.length) {
return false;
}
}
return true;
}
}

45
infer/tests/codetoanalyze/java/performance/issues.exp
Unescape View File

@ -1,7 +1,7 @@
codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_overrun_bad():void, 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [2, 8] Size: 8]
codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_weird_ok(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 12 * length.ub + 3 * (1+max(0, length.ub)), degree = 1]
codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_weird_ok(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 12 * length.ub + 3 * (1+max(0, length.ub)), degree = 1]
codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_weird_ok(long[],int):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 12 * length.ub + 3 * (1+max(0, length.ub)), degree = 1]
codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_weird_ok(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 15 * length.ub, degree = 1]
codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_weird_ok(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 15 * length.ub, degree = 1]
codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_weird_ok(long[],int):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 15 * length.ub, degree = 1]
codetoanalyze/java/performance/ArrayCost.java, ArrayCost.ArrayCost(int[]):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 5 * mag.length.ub, degree = 1]
codetoanalyze/java/performance/ArrayCost.java, ArrayCost.ArrayCost(int[]):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 * mag.length.ub, degree = 1]
codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):boolean, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 883, degree = 0]
@ -37,14 +37,13 @@ codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_while_h
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_while_has_next(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 2 * (list.length.ub + -1) + 4 * list.length.ub, degree = 1]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_with_iterator(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 9 * (list.length.ub + -1) + 4 * list.length.ub, degree = 1]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_with_iterator(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 9 * (list.length.ub + -1) + 4 * list.length.ub, degree = 1]
codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_constant(int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 4 * p.ub + 3 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_loop(int,int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 4 * p.ub + 3 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_loop(int,int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 4 * p.ub + 3 * (1+max(0, p.ub)), degree = 1]
codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 * (max(1, maxI.ub)) * (1+max(0, maxJ.ub)) + 8 * (1+max(1, maxI.ub)) * (2+max(0, maxJ.ub)) + 4 * (2+max(1, maxI.ub)), degree = 2]
codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 * (max(1, maxI.ub)) * (1+max(0, maxJ.ub)) + 8 * (1+max(1, maxI.ub)) * (2+max(0, maxJ.ub)) + 4 * (2+max(1, maxI.ub)), degree = 2]
codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 * (max(1, maxI.ub)) * (1+max(0, maxJ.ub)) + 8 * (1+max(1, maxI.ub)) * (2+max(0, maxJ.ub)) + 4 * (2+max(1, maxI.ub)), degree = 2]
codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, max(1, maxI.ub)] + [0, 1+max(0, maxJ.ub)]):signed32]
codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 * (max(1, maxI.ub)) * (1+max(0, maxJ.ub)) + 8 * (1+max(1, maxI.ub)) * (2+max(0, maxJ.ub)) + 4 * (2+max(1, maxI.ub)), degree = 2]
codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_constant(int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 7 * p.ub, degree = 1]
codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_loop(int,int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 7 * p.ub, degree = 1]
codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_loop(int,int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 * p.ub, degree = 1]
codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 4 * maxI.ub + 8 * maxI.ub * maxJ.ub + 5 * maxI.ub * (1+max(0, maxJ.ub)), degree = 2]
codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 4 * maxI.ub + 8 * maxI.ub * maxJ.ub + 5 * maxI.ub * (1+max(0, maxJ.ub)), degree = 2]
codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 4 * maxI.ub + 8 * maxI.ub * maxJ.ub + 5 * maxI.ub * (1+max(0, maxJ.ub)), degree = 2]
codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 4 * maxI.ub + 8 * maxI.ub * maxJ.ub + 5 * maxI.ub * (1+max(0, maxJ.ub)), degree = 2]
codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 5 * list.length.ub, degree = 1]
codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 * list.length.ub, degree = 1]
codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection_quad_FP(java.util.concurrent.ConcurrentLinkedQueue):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
@ -103,9 +102,9 @@ codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performan
codetoanalyze/java/performance/EvilCfg.java, EvilCfg.foo(int,int,boolean):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
codetoanalyze/java/performance/FieldAccess.java, codetoanalyze.java.performance.FieldAccess.iterate_upto_field_size(codetoanalyze.java.performance.FieldAccess$Test):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 6 * test.a.ub, degree = 1]
codetoanalyze/java/performance/FieldAccess.java, codetoanalyze.java.performance.FieldAccess.iterate_upto_field_size(codetoanalyze.java.performance.FieldAccess$Test):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 * test.a.ub, degree = 1]
codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 * (max(1, k.ub)), degree = 1]
codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 * (max(1, k.ub)), degree = 1]
codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 7 * (max(1, k.ub)), degree = 1]
codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 3 * (k.ub + -1) + 4 * (max(1, k.ub)), degree = 1]
codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 3 * (k.ub + -1) + 4 * (max(1, k.ub)), degree = 1]
codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 3 * (k.ub + -1) + 4 * (max(1, k.ub)), degree = 1]
codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: size,Binop: (size + [-oo, +oo]):signed32]
codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32]
@ -134,14 +133,22 @@ codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.util
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 250, degree = 0]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 251, degree = 0]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 250, degree = 0]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 26 * (length.ub + -1) + 3 * (max(1, length.ub)), degree = 1]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 26 * (length.ub + -1) + 3 * (max(1, length.ub)), degree = 1]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 26 * (length.ub + -1) + 3 * (max(1, length.ub)), degree = 1]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort_FP(long[],long[],int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort_FP(long[],long[],int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Binop: (a[*] * b[*]):signed64]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 29 * (length.ub + -1), degree = 1]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 29 * (length.ub + -1), degree = 1]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 29 * (length.ub + -1), degree = 1]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 71 * (length.ub + -1)^2 + 8 * length.ub, degree = 2]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 1, 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.dumbSort(long[],long[],int):void, 2, 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.dumbSort(long[],long[],int):void, 3, 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.dumbSort(long[],long[],int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Binop: (a[*] * b[*]):signed64]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 5, 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.dumbSort(long[],long[],int):void, 7, 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.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, []
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]

Write Preview
Loading…
Cancel
Save