diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml index 849e0f384..ce2a64ae5 100644 --- a/infer/src/bufferoverrun/arrayBlk.ml +++ b/infer/src/bufferoverrun/arrayBlk.ml @@ -50,8 +50,14 @@ module ArrInfo = struct match (prev, next) with | ( C {offset= offset1; size= size1; stride= stride1} , C {offset= offset2; size= size2; stride= stride2} ) -> + let offset = + let thresholds = + if Itv.eq size1 size2 then Option.to_list (Itv.is_const size1) else [] + in + Itv.widen_thresholds ~thresholds ~prev:offset1 ~next:offset2 ~num_iters + in C - { offset= Itv.widen ~prev:offset1 ~next:offset2 ~num_iters + { offset ; size= Itv.widen ~prev:size1 ~next:size2 ~num_iters ; stride= Itv.widen ~prev:stride1 ~next:stride2 ~num_iters } | Java {length= length1}, Java {length= length2} -> diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index df501b046..732d177c7 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -641,8 +641,44 @@ module Bound = struct let zero : t = Linear (Z.zero, SymLinear.zero) - let widen_l : t -> t -> t = - fun x y -> + module Thresholds : sig + type bound = t + + type t + + val make_inc : Z.t list -> t + + val make_dec : Z.t list -> t + + val widen : + cond:(threshold:bound -> bound -> bool) -> default:bound -> bound -> bound -> t -> bound + end = struct + type bound = t + + type t = bound list + + let default_thresholds = [Z.zero] + + let make ~compare thresholds = + List.dedup_and_sort ~compare (default_thresholds @ thresholds) |> List.map ~f:of_big_int + + + (* It makes a list of thresholds that will be applied with the increasing order. *) + let make_inc = make ~compare:Z.compare + + (* It makes a list of thresholds that will be applied with the decreasing order. *) + let make_dec = make ~compare:(fun x y -> -Z.compare x y) + + let rec widen ~cond ~default x y = function + | [] -> + default + | threshold :: thresholds -> + if cond ~threshold x && cond ~threshold y then threshold + else widen ~default ~cond x y thresholds + end + + let widen_l_thresholds : thresholds:Z.t list -> t -> t -> t = + fun ~thresholds x y -> match (x, y) with | PInf, _ | _, PInf -> L.(die InternalError) "Lower bound cannot be +oo." @@ -653,11 +689,16 @@ module Bound = struct when Z.equal n1 n2 && SymLinear.is_mone_symbol_of s1 s2 -> y | _ -> - if le x y then x else if le zero x && le zero y then zero else MInf + if le x y then x + else + let cond ~threshold x = le threshold x in + Thresholds.widen ~cond ~default:MInf x y (Thresholds.make_dec thresholds) - let widen_u : t -> t -> t = - fun x y -> + let widen_l : t -> t -> t = fun x y -> widen_l_thresholds ~thresholds:[] x y + + let widen_u_thresholds : thresholds:Z.t list -> t -> t -> t = + fun ~thresholds x y -> match (x, y) with | MInf, _ | _, MInf -> L.(die InternalError) "Upper bound cannot be -oo." @@ -668,8 +709,13 @@ module Bound = struct when Z.equal n1 n2 && SymLinear.is_mone_symbol_of s1 s2 -> y | _ -> - if le y x then x else if le x zero && le y zero then zero else PInf + if le y x then x + else + let cond ~threshold x = le x threshold in + Thresholds.widen ~cond ~default:PInf x y (Thresholds.make_inc thresholds) + + let widen_u : t -> t -> t = fun x y -> widen_u_thresholds ~thresholds:[] x y let one : t = Linear (Z.one, SymLinear.zero) diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli index e796e0ae7..dba60155d 100644 --- a/infer/src/bufferoverrun/bounds.mli +++ b/infer/src/bufferoverrun/bounds.mli @@ -77,8 +77,12 @@ module Bound : sig val widen_l : t -> t -> t + val widen_l_thresholds : thresholds:Z.t list -> t -> t -> t + val widen_u : t -> t -> t + val widen_u_thresholds : thresholds:Z.t list -> t -> t -> t + val zero : t val one : t diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 498966a4d..c587a21d4 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -94,6 +94,11 @@ module ItvPure = struct fun ~prev:(l1, u1) ~next:(l2, u2) ~num_iters:_ -> (Bound.widen_l l1 l2, Bound.widen_u u1 u2) + let widen_thresholds : thresholds:Z.t list -> prev:t -> next:t -> num_iters:int -> t = + fun ~thresholds ~prev:(l1, u1) ~next:(l2, u2) ~num_iters:_ -> + (Bound.widen_l_thresholds ~thresholds l1 l2, Bound.widen_u_thresholds ~thresholds u1 u2) + + let pp_mark : markup:bool -> F.formatter -> t -> unit = fun ~markup fmt (l, u) -> if Bound.equal l u then Bound.pp_mark ~markup fmt l @@ -437,6 +442,20 @@ end include AbstractDomain.BottomLifted (ItvPure) +let widen_thresholds ~thresholds ~prev:prev0 ~next:next0 ~num_iters = + if phys_equal prev0 next0 then prev0 + else + match (prev0, next0) with + | Bottom, _ -> + next0 + | _, Bottom -> + prev0 + | NonBottom prev, NonBottom next -> + PhysEqual.optim2 + ~res:(NonBottom (ItvPure.widen_thresholds ~thresholds ~prev ~next ~num_iters)) + prev0 next0 + + let compare : t -> t -> int = fun x y -> match (x, y) with diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 826b6f143..63f635634 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -102,6 +102,8 @@ end include module type of AbstractDomain.BottomLifted (ItvPure) +val widen_thresholds : thresholds:Z.t list -> prev:t -> next:t -> num_iters:int -> t + val compare : t -> t -> int val bot : t diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 432b81e50..05286e15c 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -78,9 +78,7 @@ codetoanalyze/cpp/bufferoverrun/repro1.cpp, ral_FP, 3, BUFFER_OVERRUN_S2, no_buc codetoanalyze/cpp/bufferoverrun/repro1.cpp, ral_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->b.infer_size`,Call,Parameter `this->b.infer_size`,Call,Parameter `this->infer_size`,Call,,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64] codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Parameter `v->_size`,Call,,Parameter `i`,,Parameter `this->_size`,Array declaration,Assignment,Array access: Offset: v->_size Size: v->_size by call to `int_vector_access_at` ] codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter1_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] -codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter2_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [,Array declaration,Through,Array access: Offset: [0, +oo] Size: 5] codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter2_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] -codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter2_Good_FP, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [,Array declaration,Through,Array access: Offset: [0, +oo] Size: 11] codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter3_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter_back_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter_front_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/std_array.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/std_array.cpp index fec534896..357a5a7f9 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/std_array.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/std_array.cpp @@ -68,8 +68,7 @@ void array_iter1_Bad() { a[a[0]] = 0; } -// TODO: Inferbo should give a preciser widening threshold. -void array_iter2_Good_FP() { +void array_iter2_Good() { std::array a; for (auto it = a.begin(); it != a.end(); ++it) { *it = 10;