diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index b47f5b24c..f280f7039 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -24,9 +24,16 @@ type eval_sym_trace = ; trace_of_sym: Symb.Symbol.t -> Trace.Set.t ; eval_locpath: PowLoc.eval_locpath } +module ItvThresholds = AbstractDomain.FiniteSet (struct + include Z + + let pp = pp_print +end) + module Val = struct type t = { itv: Itv.t + ; itv_thresholds: ItvThresholds.t ; sym: Relation.Sym.t ; powloc: PowLoc.t ; arrayblk: ArrayBlk.t @@ -37,6 +44,7 @@ module Val = struct let bot : t = { itv= Itv.bot + ; itv_thresholds= ItvThresholds.empty ; sym= Relation.Sym.bot ; powloc= PowLoc.bot ; arrayblk= ArrayBlk.bot @@ -47,6 +55,10 @@ module Val = struct let pp fmt x = + let itv_thresholds_pp fmt itv_thresholds = + if Config.bo_debug >= 3 && not (ItvThresholds.is_empty itv_thresholds) then + F.fprintf fmt " (thresholds:%a)" ItvThresholds.pp itv_thresholds + in let relation_sym_pp fmt sym = if Option.is_some Config.bo_relational_domain then F.fprintf fmt ", %a" Relation.Sym.pp sym in @@ -54,9 +66,9 @@ module Val = struct if Config.bo_debug >= 1 then F.fprintf fmt ", %a" TraceSet.pp traces in let represents_multiple_values_str = if x.represents_multiple_values then "M" else "" in - F.fprintf fmt "%s(%a%a, %a, %a%a%a%a)" represents_multiple_values_str Itv.pp x.itv - relation_sym_pp x.sym PowLoc.pp x.powloc ArrayBlk.pp x.arrayblk relation_sym_pp x.offset_sym - relation_sym_pp x.size_sym trace_pp x.traces + F.fprintf fmt "%s(%a%a%a, %a, %a%a%a%a)" represents_multiple_values_str Itv.pp x.itv + itv_thresholds_pp x.itv_thresholds relation_sym_pp x.sym PowLoc.pp x.powloc ArrayBlk.pp + x.arrayblk relation_sym_pp x.offset_sym relation_sym_pp x.size_sym trace_pp x.traces let sets_represents_multiple_values : represents_multiple_values:bool -> t -> t = @@ -67,6 +79,7 @@ module Val = struct fun ~callee_pname ~location -> let traces = Trace.(Set.singleton_final location (UnknownFrom callee_pname)) in { itv= Itv.top + ; itv_thresholds= ItvThresholds.empty ; sym= Relation.Sym.top ; powloc= PowLoc.unknown ; arrayblk= ArrayBlk.unknown @@ -80,6 +93,7 @@ module Val = struct if phys_equal lhs rhs then true else Itv.( <= ) ~lhs:lhs.itv ~rhs:rhs.itv + && ItvThresholds.( <= ) ~lhs:lhs.itv_thresholds ~rhs:rhs.itv_thresholds && Relation.Sym.( <= ) ~lhs:lhs.sym ~rhs:rhs.sym && PowLoc.( <= ) ~lhs:lhs.powloc ~rhs:rhs.powloc && ArrayBlk.( <= ) ~lhs:lhs.arrayblk ~rhs:rhs.arrayblk @@ -91,7 +105,12 @@ module Val = struct let widen ~prev ~next ~num_iters = if phys_equal prev next then prev else - { itv= Itv.widen ~prev:prev.itv ~next:next.itv ~num_iters + let itv_thresholds = ItvThresholds.join prev.itv_thresholds next.itv_thresholds in + { itv= + Itv.widen_thresholds + ~thresholds:(ItvThresholds.elements itv_thresholds) + ~prev:prev.itv ~next:next.itv ~num_iters + ; itv_thresholds ; sym= Relation.Sym.widen ~prev:prev.sym ~next:next.sym ~num_iters ; powloc= PowLoc.widen ~prev:prev.powloc ~next:next.powloc ~num_iters ; arrayblk= ArrayBlk.widen ~prev:prev.arrayblk ~next:next.arrayblk ~num_iters @@ -107,6 +126,7 @@ module Val = struct if phys_equal x y then x else { itv= Itv.join x.itv y.itv + ; itv_thresholds= ItvThresholds.join x.itv_thresholds y.itv_thresholds ; sym= Relation.Sym.join x.sym y.sym ; powloc= PowLoc.join x.powloc y.powloc ; arrayblk= ArrayBlk.join x.arrayblk y.arrayblk @@ -192,6 +212,7 @@ module Val = struct let lift_itv : (Itv.t -> Itv.t -> Itv.t) -> ?f_trace:_ -> t -> t -> t = fun f ?f_trace x y -> let itv = f x.itv y.itv in + let itv_thresholds = ItvThresholds.join x.itv_thresholds y.itv_thresholds in let traces = match f_trace with | Some f_trace -> @@ -205,7 +226,7 @@ module Val = struct | true, true | false, false -> TraceSet.join x.traces y.traces ) in - {bot with itv; traces} + {bot with itv; itv_thresholds; traces} let lift_cmp_itv : (Itv.t -> Itv.t -> Boolean.t) -> Boolean.EqualOrder.t -> t -> t -> t = @@ -291,13 +312,23 @@ module Val = struct (Itv.t -> Itv.t -> Itv.t) -> (ArrayBlk.t -> ArrayBlk.t -> ArrayBlk.t) -> t -> t -> t = fun f g x y -> let itv = f x.itv y.itv in + let itv_thresholds = + Option.value_map (Itv.is_const y.itv) ~default:x.itv_thresholds ~f:(fun z -> + x.itv_thresholds + |> ItvThresholds.add Z.(z - one) + |> ItvThresholds.add z + |> ItvThresholds.add Z.(z + one) ) + in let arrayblk = g x.arrayblk y.arrayblk in - if phys_equal itv x.itv && phys_equal arrayblk x.arrayblk then - (* x hasn't changed, don't join traces *) + if + phys_equal itv x.itv + && phys_equal itv_thresholds x.itv_thresholds + && phys_equal arrayblk x.arrayblk + then (* x hasn't changed, don't join traces *) x else warn_against_pruning_multiple_values - {x with itv; arrayblk; traces= TraceSet.join x.traces y.traces} + {x with itv; itv_thresholds; arrayblk; traces= TraceSet.join x.traces y.traces} let prune_eq_zero : t -> t = lift_prune1 Itv.prune_eq_zero diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/for_loop.c b/infer/tests/codetoanalyze/c/bufferoverrun/for_loop.c index 02be909e5..22bec2a5e 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/for_loop.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/for_loop.c @@ -96,3 +96,41 @@ void call_initialize_arr_Bad() { int arr[10]; initialize_arr(arr, 20); } + +void threshold_by_comparison_1_Good() { + int arr[100]; + for (int i = 0; i != 100; i++) { + arr[i] = 0; + } +} + +void threshold_by_comparison_1_Bad() { + int arr[50]; + for (int i = 0; i != 100; i++) { + arr[i] = 0; + } +} + +void threshold_by_comparison_2_Good() { + int arr[100]; + int j = 0; + while (1) { // widening threshold for j should be 99, not 100 + j++; + if (j == 100) { + j = 0; + } + arr[j] = 0; + } +} + +void threshold_by_comparison_2_Bad() { + int arr[50]; + int j = 0; + while (1) { // widening threshold for j should be 99, not 100 + j++; + if (j == 100) { + j = 0; + } + arr[j] = 0; + } +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 27bbb732b..1fc1e8d08 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -102,6 +102,10 @@ codetoanalyze/c/bufferoverrun/external.c, extern_bad, 10, BUFFER_OVERRUN_L1, no_ codetoanalyze/c/bufferoverrun/for_loop.c, call_initialize_arr_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Array declaration,Call,,Assignment,,Parameter `*arr`,Array access: Offset: [0, 19] Size: 10 by call to `initialize_arr` ] codetoanalyze/c/bufferoverrun/for_loop.c, call_two_loops_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,Call,Parameter `m`,Assignment,,Array declaration,Array access: Offset: 15 Size: 10] codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Assignment,,Call,Array declaration,Assignment,Assignment,Assignment,Array access: Offset: [0, 9] Size: [5, 10]] +codetoanalyze/c/bufferoverrun/for_loop.c, threshold_by_comparison_1_Bad, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, 99] Size: 50] +codetoanalyze/c/bufferoverrun/for_loop.c, threshold_by_comparison_2_Bad, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] +codetoanalyze/c/bufferoverrun/for_loop.c, threshold_by_comparison_2_Bad, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, 99] Size: 50] +codetoanalyze/c/bufferoverrun/for_loop.c, threshold_by_comparison_2_Good, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/function_call.c, call_access_index_4_on_local_array_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,,Parameter `*arr`,Array access: Offset: 4 Size: 4 by call to `access_index_4` ] codetoanalyze/c/bufferoverrun/function_call.c, call_access_index_4_on_malloced_array_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,,Parameter `*arr`,Array access: Offset: 4 Size: 4 by call to `access_index_4` ] codetoanalyze/c/bufferoverrun/function_call.c, call_by_arr_bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Call,Assignment,,Array declaration,Array access: Offset: -1 Size: 10] diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp index 6e994047a..5e4332f20 100644 --- a/infer/tests/codetoanalyze/c/performance/issues.exp +++ b/infer/tests/codetoanalyze/c/performance/issues.exp @@ -26,7 +26,7 @@ codetoanalyze/c/performance/cost_test.c, loop2_bad, 2, EXPENSIVE_EXECUTION_TIME_ codetoanalyze/c/performance/cost_test.c, main_bad, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 214, degree = 0] codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 6 ⋅ (-m + 20), degree = 1,{-m + 20},Loop at line 117, column 3] codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 235, degree = 0] -codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([3, +oo] + 1):signed32] +codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/c/performance/cost_test_deps.c, loop_despite_inferbo, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1307, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep1, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 609, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep1, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 5140904af..e47859276 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -68,7 +68,7 @@ codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Co codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.main_bad():int, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 205, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.if_bad(int):void, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 613, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.if_bad_loop():int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 201, 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, [,Assignment,Binary operation: ([3, +oo] + 1):signed32] +codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.if_bad_loop():int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_despite_inferbo(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1303, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_no_dep1(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 605, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_no_dep1(int):int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32]