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

[inferbo] Use WTO abstract interpreter

Browse Source 
Reviewed By: jvillard

Differential Revision: D10072723

fbshipit-source-id: aabf3605e
master
Mehdi Bouaziz 6 years ago committed by Facebook Github Bot
parent f28faad627
commit 3dd97cc40f
15 changed files with 162 additions and 49 deletions
Show Stats Download Patch File Download Diff File

2
infer/src/bufferoverrun/bufferOverrunChecker.ml
Unescape View File

@ -239,7 +239,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
end
module CFG = ProcCfg.NormalOneInstrPerNode
module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions (CFG))
module Analyzer = AbstractInterpreter.MakeWTO (TransferFunctions (CFG))
type invariant_map = Analyzer.invariant_map

22
infer/tests/codetoanalyze/c/bufferoverrun/big_array.c
Unescape View File

@ -0,0 +1,22 @@
/*
* Copyright (c) 2018-present, Facebook, Inc.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*/
#define CHARS_21 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0,
#define CHARS_147 CHARS_21 CHARS_21 CHARS_21 CHARS_21 CHARS_21 CHARS_21 CHARS_21
#define CHARS_882 CHARS_147 CHARS_147 CHARS_147 CHARS_147 CHARS_147 CHARS_147
#define CHARS_5292 CHARS_882 CHARS_882 CHARS_882 CHARS_882 CHARS_882 CHARS_882
#define CHARS_26460 CHARS_5292 CHARS_5292 CHARS_5292 CHARS_5292 CHARS_5292
unsigned char* big_array() {
const unsigned char bytes[] = {CHARS_26460};
return bytes;
}
void use_big_array_bad() {
unsigned char* b = big_array();
b[999999999] = 'Y';
}

19
infer/tests/codetoanalyze/c/bufferoverrun/goto_loop.c
Unescape View File

@ -21,3 +21,22 @@ loop_start:
loop_end:
a[i] = 'a'; /* BUG */
}
void goto_infinite_loop() {
int i = 0;
L1:
i++;
if (i >= 0) { // Always true
goto L2;
} else {
goto L2;
}
L2:
i++;
if (i >= 0) { // Always true
goto L1;
} else {
goto L1;
}
// Exit node not reachable
}

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

@ -30,6 +30,7 @@ codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_ptr_good_FP, 2, COND
codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Offset: [3xlen.lb + 1, 3xlen.ub + 1] Size: [3xlen.lb + 1, 3xlen.ub + 1]]
codetoanalyze/c/bufferoverrun/array_field.c, array_field_access_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 20 Size: 10]
codetoanalyze/c/bufferoverrun/array_field.c, decreasing_pointer_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,Assignment,Assignment,ArrayAccess: Offset: -1 Size: 2]
codetoanalyze/c/bufferoverrun/big_array.c, use_big_array_bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Assignment,Return,Assignment,ArrayAccess: Offset: 999999999 Size: 26460]
codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32]
codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 13, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
@ -65,6 +66,10 @@ codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_cond_Bad, 4, BUFFER_OV
codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_bad_FN, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_bad_FN, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10]
codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32]
codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Assignment,Binop: ([1, +oo] + 1):signed32]
codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 11, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [10, +oo] Size: 10]
codetoanalyze/c/bufferoverrun/inf_loop.c, inf_loop, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
codetoanalyze/c/bufferoverrun/issue_kinds.c, False_Issue_Type_l3_unknown_function_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Assignment,Return,Binop: ([5, +oo] * 4):unsigned64]
@ -128,10 +133,11 @@ codetoanalyze/c/bufferoverrun/models.c, strncpy_bad2, 3, BUFFER_OVERRUN_L1, no_b
codetoanalyze/c/bufferoverrun/models.c, strncpy_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: -1 Size: 40]
codetoanalyze/c/bufferoverrun/models.c, strncpy_bad4, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 8 Size: 4]
codetoanalyze/c/bufferoverrun/models.c, strncpy_good5_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 5]
codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32]
codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: 10]
codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32]
codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop3_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: 10]
codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop4_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: 10]
codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: 10]
codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 7, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
codetoanalyze/c/bufferoverrun/pointer_arith.c, FP_pointer_arith5_Ok, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [3, 2043] Size: 1024]
codetoanalyze/c/bufferoverrun/pointer_arith.c, array_pointer_arith_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 10 Size: 10]
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` ]

34
infer/tests/codetoanalyze/c/bufferoverrun/nested_loop.c
Unescape View File

@ -19,3 +19,37 @@ void nested_loop() {
}
}
}
void nested_loop2_Ok() {
double arr[10];
int i, j;
for (i = 0; i < 10; i++) {
for (j = 5; j < 15; j++) {
arr[i] = 0.0;
arr[j - 5] = 0.0;
}
}
}
void nested_loop3_Bad() {
double arr[10];
int i, j;
for (i = 0; i <= 10; i++) {
for (j = 5; j < 15; j++) {
arr[i] = 0.0;
}
}
}
void nested_loop4_Bad() {
double arr[10];
int i, j;
for (i = 0; i < 10; i++) {
for (j = 5; j <= 15; j++) {
arr[j - 5] = 0.0;
}
}
}

2
infer/tests/codetoanalyze/c/bufferoverrun/nested_loop_with_label.c
Unescape View File

@ -15,7 +15,7 @@ void nested_loop_with_label() {
for (i = 0; i < 10; i++) {
outer_loop:
a[j] = 'a'; /* BUG */
for (j = 0; j <= 10; j++) {
for (j = 0; j <= 10; j++) { // Loop condition always true
if (j >= 10)
goto outer_loop;
}

7
infer/tests/codetoanalyze/c/performance/compound_loop_guard.c
Unescape View File

@ -33,7 +33,7 @@ int simulated_while_with_and(int p) {
int i = 0;
int k = 0;
LOOP_COND:
if (k == 0 && i < p) {
if (k == 0 && i < p) { // k == 0 always true
goto INCR;
} else {
goto RETURN;
@ -79,7 +79,8 @@ int nested_while_and_or(int p) {
return j;
}
/* k,j and i will be control variables for B */
/* j and i will be control variables for B */
/* Expected: 5 + 100 */
int simulated_nested_loop_with_and(int p) {
int k = 0;
int t = 5;
@ -88,7 +89,7 @@ int simulated_nested_loop_with_and(int p) {
B:
t = 3;
j++;
if (k == 0 && j < 100) {
if (k == 0 && j < 100) { // k == 0 always true
goto B; // continue;
}
}

7
infer/tests/codetoanalyze/c/performance/cost_test_deps.c
Unescape View File

@ -99,11 +99,7 @@ int loop_despite_inferbo(int p) {
return p;
}
// -- Below examples should have worked, but due to the imprecision/weakness
// in inferbo's relational analysis, they don't
// We can get program point A's execution count as 5, however
// due to the weakness in inferbo's relational analysis `i` is in [0, +oo]
/* Expected: 5 * 100 */
int nested_loop() {
int k = 0;
for (int i = 0; i < 5; i++) {
@ -182,6 +178,7 @@ RETURN:
}
/* Conditional inside goto loop */
/* Expected: 5 * 100 */
int simulated_nested_loop_cond_in_goto(int p) {
int k = 0;
int t = 5;

9
infer/tests/codetoanalyze/c/performance/invariant.c
Unescape View File

@ -33,8 +33,8 @@ void do_k_times_array(int n) {
}
}
/* Expected Theta(n * m), but can't handle nested loops over symbols yet */
void do_n_m_times_nested_FP(int n, int m) {
/* Expected Theta(n * m) */
void do_n_m_times_nested(int n, int m) {
int k = n;
int p = m;
for (int i = 0; i < k; i++) {
@ -43,9 +43,8 @@ void do_n_m_times_nested_FP(int n, int m) {
}
}
/* Expected Theta(m) but can't handle nested loops over symbols yet.
Also inner loop will have t as invariant */
void two_loops_nested_invariant_FP(int p) {
/* Expected ~ 3 * p. Also inner loop will have t as invariant */
void two_loops_nested_invariant(int p) {
int t = 0;
int m = p;
for (int i = 0; i < m; i++) {

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

@ -23,9 +23,14 @@ codetoanalyze/c/performance/compound_loop_guard.c, simplified_simulated_while_wi
codetoanalyze/c/performance/compound_loop_guard.c, simplified_simulated_while_with_and, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 602, degree = 0]
codetoanalyze/c/performance/compound_loop_guard.c, simplified_simulated_while_with_and, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 602, degree = 0]
codetoanalyze/c/performance/compound_loop_guard.c, simplified_simulated_while_with_and, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 604, degree = 0]
codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_and, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_and, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32]
codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_and, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3526, degree = 0]
codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_and, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3526, degree = 0]
codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_and, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3526, degree = 0]
codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_and, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32]
codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_and, 8, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_and, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3526, degree = 0]
codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_and, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3526, degree = 0]
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 7 + 7 * p.ub, degree = 1]
@ -65,18 +70,36 @@ codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep2, 3, EXPENSIVE_EXECUTI
codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep2, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 611, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep2, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32]
codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep2, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 613, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, nested_loop, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
codetoanalyze/c/performance/cost_test_deps.c, nested_loop, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32]
codetoanalyze/c/performance/cost_test_deps.c, nested_loop, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2544, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, nested_loop, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2544, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, nested_loop, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2544, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, nested_loop, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2544, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, nested_loop, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2544, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, nested_loop, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2546, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, real_while, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 215, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, real_while, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 215, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, real_while, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + [0, 29]):signed32]
codetoanalyze/c/performance/cost_test_deps.c, real_while, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 217, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32]
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_cond_in_goto, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_cond_in_goto, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32]
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_more_expensive, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_more_expensive, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32]
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2526, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2526, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2526, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32]
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2526, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop, 11, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2528, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_cond_in_goto, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3531, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_cond_in_goto, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3531, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_cond_in_goto, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3531, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_cond_in_goto, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3531, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_cond_in_goto, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3531, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_cond_in_goto, 11, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3531, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_cond_in_goto, 12, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3531, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_cond_in_goto, 18, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3533, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_more_expensive, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2531, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_more_expensive, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2531, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_more_expensive, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2531, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_more_expensive, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2531, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_more_expensive, 11, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2531, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_more_expensive, 14, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2533, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, simulated_while, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 215, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, simulated_while, 10, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 215, degree = 0]
codetoanalyze/c/performance/cost_test_deps.c, simulated_while, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + [0, 29]):signed32]
@ -96,10 +119,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 6 + 5 * n.ub, degree = 1]
codetoanalyze/c/performance/invariant.c, do_k_times_array, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 8 * n.ub, degree = 1]
codetoanalyze/c/performance/invariant.c, do_k_times_array, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 8 * n.ub, degree = 1]
codetoanalyze/c/performance/invariant.c, do_n_m_times_nested_FP, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
codetoanalyze/c/performance/invariant.c, do_n_m_times_nested_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32]
codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant_FP, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32]
codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 9 * n.ub + 5 * (max(1, n.ub)) * (1+max(0, m.ub)), degree = 2]
codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 9 * n.ub + 5 * (max(1, n.ub)) * (1+max(0, m.ub)), degree = 2]
codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 9 * n.ub + 5 * (max(1, n.ub)) * (1+max(0, m.ub)), degree = 2]
codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 9 * n.ub + 5 * (max(1, n.ub)) * (1+max(0, m.ub)), degree = 2]
codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 9 * n.ub + 5 * (max(1, n.ub)) * (1+max(0, m.ub)), degree = 2]
codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 8 * p.ub + 17 * (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 7 + 8 * p.ub + 17 * (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 7 + 8 * p.ub + 17 * (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 7 + 8 * p.ub + 17 * (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 7 + 8 * p.ub + 17 * (max(1, 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]

7
infer/tests/codetoanalyze/java/performance/Break.java
Unescape View File

@ -24,7 +24,12 @@ public class Break {
return break_loop(p, -1);
}
private static void break_outer_loop_FN(int maxI, int maxJ) {
/*
If maxI >= 1 and maxJ >= 1 and maxI + maxJ > 8 then Infinite loop
(but the CFG constraints never finds infinite loops)
Otherwise, O(maxI * maxJ)
*/
private static void break_outer_loop_MaybeInfinite(int maxI, int maxJ) {
int i = 0;
outerloop:
while (i < maxI) {

3
infer/tests/codetoanalyze/java/performance/Continue.java
Unescape View File

@ -7,7 +7,8 @@
package codetoanalyze.java.performance;
public class Continue {
int continue_outer_loop_FN() {
/* Expected 1000 * 1000 / 2 */
int continue_outer_loop() {
outer:
for (int i = 2; i < 1000; i++) {
for (int j = 2; j < i; j++) {

1
infer/tests/codetoanalyze/java/performance/Cost_test_deps.java
Unescape View File

@ -85,6 +85,7 @@ public class Cost_test_deps {
return p;
}
/* Expected: 5 * 100 */
private static int nested_loop() {
int k = 0;
for (int i = 0; i < 5; i++) {

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

@ -46,7 +46,7 @@ public class Loops {
}
}
static void dumbSort(long[] a, long[] b, int length) {
static void dumbSort_FP(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]) {

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

@ -40,9 +40,11 @@ codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_with_it
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_FN(int,int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_FN(int,int):void, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + [0, maxJ.ub + -1]):signed32]
codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_FN(int,int):void, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32]
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 + 9 * maxI.ub + 3 * maxJ.ub * (max(1, maxI.ub)) + 10 * (max(1, 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 + 9 * maxI.ub + 3 * maxJ.ub * (max(1, maxI.ub)) + 10 * (max(1, 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 + 9 * maxI.ub + 3 * maxJ.ub * (max(1, maxI.ub)) + 10 * (max(1, 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, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, -1+max(1, maxI.ub)] + [0, maxJ.ub + -1]):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 + 9 * maxI.ub + 3 * maxJ.ub * (max(1, maxI.ub)) + 10 * (max(1, 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, []
@ -59,8 +61,10 @@ 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, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.while_and_or(int):void, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.while_and_or(int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32]
codetoanalyze/java/performance/Continue.java, codetoanalyze.java.performance.Continue.continue_outer_loop_FN():int, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
codetoanalyze/java/performance/Continue.java, codetoanalyze.java.performance.Continue.continue_outer_loop_FN():int, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([2, +oo] + 1):signed32]
codetoanalyze/java/performance/Continue.java, codetoanalyze.java.performance.Continue.continue_outer_loop():int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7963050, degree = 0]
codetoanalyze/java/performance/Continue.java, codetoanalyze.java.performance.Continue.continue_outer_loop():int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7963049, degree = 0]
codetoanalyze/java/performance/Continue.java, codetoanalyze.java.performance.Continue.continue_outer_loop():int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7963049, degree = 0]
codetoanalyze/java/performance/Continue.java, codetoanalyze.java.performance.Continue.continue_outer_loop():int, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7963049, degree = 0]
codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.FN_loop2(int):int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 13 * k.ub, degree = 1]
codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.FN_loop2(int):int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 13 * k.ub, degree = 1]
codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.loop0_bad():int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1202, degree = 0]
@ -86,8 +90,9 @@ codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performan
codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_no_dep2(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 611, degree = 0]
codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_no_dep2(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 610, degree = 0]
codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_no_dep2(int):int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32]
codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.nested_loop():int, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.nested_loop():int, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32]
codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.nested_loop():int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2544, degree = 0]
codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.nested_loop():int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2543, degree = 0]
codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.nested_loop():int, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2543, degree = 0]
codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.real_while():int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 215, degree = 0]
codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.real_while():int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 214, degree = 0]
codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.real_while():int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + [0, 29]):signed32]
@ -134,14 +139,8 @@ codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.
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 3 + 76 * (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 4 + 76 * (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 + 76 * (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 + 76 * (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 + 76 * (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 + 76 * (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 + 76 * (length.ub + -1)^2 + 8 * length.ub, degree = 2]
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.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]

Write Preview
Loading…
Cancel
Save