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

[inferbo] Revise widen of bounds

Browse Source 
Summary:
This diff revises widening functions of bounds that have a linear form and a min/max form.
For example, for lower bounds,

* 3 ▽ (1+min(2, x)) = (1+min(2, x))
* 3+x ▽ (3+min(2, x)) = (3+min(2, x))

Reviewed By: jvillard

Differential Revision: D17420786

fbshipit-source-id: ff9eebed3
master
Sungkeun Cho 5 years ago committed by Facebook Github Bot
parent 3543c89c19
commit 21c890f23d
5 changed files with 33 additions and 6 deletions
Show Stats Download Patch File Download Diff File

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

@ -163,9 +163,9 @@ module SymLinear = struct
is_one_symbol_of_common get_mone_symbol_opt
let is_signed_one_symbol_of : weak:bool -> Sign.t -> Symb.Symbol.t -> t -> bool =
fun ~weak sign s x ->
match sign with Plus -> is_one_symbol_of ~weak s x | Minus -> is_mone_symbol_of ~weak s x
let is_signed_one_symbol_of : ?weak:bool -> Sign.t -> Symb.Symbol.t -> t -> bool =
fun ?weak sign s x ->
match sign with Plus -> is_one_symbol_of ?weak s x | Minus -> is_mone_symbol_of ?weak s x
let get_symbols : t -> Symb.SymbolSet.t =
@ -770,6 +770,14 @@ module Bound = struct
| MinMax (n1, Minus, Min, _, s1), Linear (n2, s2)
when Z.equal n1 n2 && SymLinear.is_mone_symbol_of s1 s2 ->
y
| Linear (n1, s1), MinMax (n2, (Plus as sign1), Min, n3, _)
| Linear (n1, s1), MinMax (n2, (Minus as sign1), Max, n3, _)
when Z.equal n1 (Sign.eval_big_int sign1 n2 n3) && SymLinear.is_empty s1 ->
y
| Linear (n1, s1), MinMax (n2, (Plus as sign1), Min, _, s2)
| Linear (n1, s1), MinMax (n2, (Minus as sign1), Max, _, s2)
when Z.equal n1 n2 && SymLinear.is_signed_one_symbol_of sign1 s2 s1 ->
y
| _ ->
if le x y then x
else
@ -790,6 +798,14 @@ module Bound = struct
| MinMax (n1, Minus, Max, _, s1), Linear (n2, s2)
when Z.equal n1 n2 && SymLinear.is_mone_symbol_of s1 s2 ->
y
| Linear (n1, s1), MinMax (n2, (Plus as sign1), Max, n3, _)
| Linear (n1, s1), MinMax (n2, (Minus as sign1), Min, n3, _)
when Z.equal n1 (Sign.eval_big_int sign1 n2 n3) && SymLinear.is_empty s1 ->
y
| Linear (n1, s1), MinMax (n2, (Plus as sign1), Max, _, s2)
| Linear (n1, s1), MinMax (n2, (Minus as sign1), Min, _, s2)
when Z.equal n1 n2 && SymLinear.is_signed_one_symbol_of sign1 s2 s1 ->
y
| _ ->
if le y x then x
else

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

@ -311,6 +311,6 @@ codetoanalyze/c/bufferoverrun/unrolling.c, call_do_two_times2_Good_FP, 0, BUFFER
codetoanalyze/c/bufferoverrun/unrolling.c, call_do_two_times_Good_FP, 0, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,<Offset trace>,Parameter `n`,<Length trace>,Array declaration,Array access: Offset: [0, 4] Size: 1 by call to `do_two_times_Good` ]
codetoanalyze/c/bufferoverrun/while_loop.c, diverge_on_narrowing, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
codetoanalyze/c/bufferoverrun/while_loop.c, join_minmax_with_sum_signed_Good_FP, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([-oo, +oo] + 1):signed32]
codetoanalyze/c/bufferoverrun/while_loop.c, join_minmax_with_sum_signed_Good_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `y`,<RHS trace>,Parameter `y`,Binary operation: (x + [-oo, +oo]):signed32]
codetoanalyze/c/bufferoverrun/while_loop.c, join_minmax_with_sum_signed_Good_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `y`,<RHS trace>,Parameter `y`,Binary operation: (x + [min(0, y), max(0, y)]):signed32]
codetoanalyze/c/bufferoverrun/while_loop.c, join_minmax_with_sum_signed_Good_FP, 12, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Parameter `y`,<Length trace>,Assignment,Array declaration,Array access: Offset: [0, +oo] Size: [0, +oo]]
codetoanalyze/c/bufferoverrun/while_loop.c, while_loop, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: [0, 10] Size: 10]

11
infer/tests/codetoanalyze/c/bufferoverrun/while_loop.c
Unescape View File

@ -58,3 +58,14 @@ void join_minmax_with_sum_signed_Good_FP(int x, int y) {
}
a[i] = 2;
}
void preciser_widen_Good(int x) {
int idx = 0;
int arr[10];
while (idx < 10) {
arr[idx] = 0;
if (unknown()) {
idx = x;
}
}
}

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

@ -21,7 +21,7 @@ codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 3, INTEGER_OVER
codetoanalyze/c/performance/cost_test.c, alias_OK, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Binary operation: ([-oo, +oo] + 1):signed32]
codetoanalyze/c/performance/cost_test.c, call_infinite, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Call to infinite,Unbounded loop,Loop at line 146, column 3]
codetoanalyze/c/performance/cost_test.c, call_while_upto20_minus100_bad, 0, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 606, O(1), degree = 0]
codetoanalyze/c/performance/cost_test.c, ignore_character_symbols_constant_FP, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 155, column 3]
codetoanalyze/c/performance/cost_test.c, ignore_character_symbols_constant_FP, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 4 ⋅ (122-min(97, c)), O((-c + 122)), degree = 1,{122-min(97, c)},Loop at line 155, column 3]
codetoanalyze/c/performance/cost_test.c, infinite, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 146, column 3]
codetoanalyze/c/performance/cost_test.c, infinite, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Assignment,Binary operation: ([-oo, +oo] + [0, +oo]):signed32]
codetoanalyze/c/performance/cost_test.c, infinite_FN, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Assignment,Binary operation: ([-oo, +oo] + [0, +oo]):signed32]

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

@ -114,7 +114,7 @@ codetoanalyze/java/performance/IntTest.java, IntTest.static_Integer_top():void,
codetoanalyze/java/performance/IntTest.java, IntTest.valueOf_linear(int):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ p + 3 ⋅ (1+max(0, p)), O(p), degree = 1,{1+max(0, p)},Loop at line 20,{p},Loop at line 20]
codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 3 ⋅ (k - 1) + 4 ⋅ (max(1, k)), O(k), degree = 1,{max(1, k)},Loop at line 58,{k - 1},Loop at line 58]
codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 31]
codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `x`,<RHS trace>,Parameter `x`,Binary operation: (size + [-oo, +oo]):signed32]
codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `x`,<RHS trace>,Parameter `x`,Binary operation: (size + [min(0, x), max(0, x)]):signed32]
codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `x`,Binary operation: ([0, +oo] + 1):signed32]
codetoanalyze/java/performance/Invariant.java, Invariant.list_size_invariant(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ items.length + 3 ⋅ (items.length + 1), O(items.length), degree = 1,{items.length + 1},Loop at line 66,{items.length},Loop at line 66]
codetoanalyze/java/performance/Invariant.java, Invariant.local_not_invariant_FP(int):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 3 + 12 ⋅ (size + 5) + 7 ⋅ (size + 5) × (5+min(1, size)) + 4 ⋅ (5+min(0, size)), O(size²), degree = 2,{5+min(0, size)},Loop at line 46,{5+min(1, size)},Loop at line 46,{size + 5},Loop at line 46]

Write Preview
Loading…
Cancel
Save