From a8e84d165757390bfa740d3b6e425db813a754cb Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Mon, 25 Jun 2018 07:09:06 -0700 Subject: [PATCH] Cost: improve NonNegativePolynomial.(<=) Reviewed By: ezgicicek Differential Revision: D8531865 fbshipit-source-id: b5c9293 --- infer/src/bufferoverrun/itv.ml | 65 +++++++++++++++++++ .../codetoanalyze/c/performance/cost_test.c | 2 +- .../codetoanalyze/c/performance/issues.exp | 1 - 3 files changed, 66 insertions(+), 2 deletions(-) diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 9520b57e9..e5009199d 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -156,6 +156,8 @@ module Ints : sig val one : t + val of_int : int -> t option + val of_int_exn : int -> t val is_zero : t -> bool @@ -196,6 +198,8 @@ end = struct let is_one = function 1 -> true | _ -> false + let of_int i = if i < 0 then None else Some i + let of_int_exn i = assert (i >= 0) ; i @@ -372,6 +376,13 @@ module SymLinear = struct let get_symbols : t -> Symbol.t list = fun x -> M.fold (fun symbol _coeff acc -> symbol :: acc) x [] + + + (* we can give integer bounds (obviously 0) only when all symbols are unsigned *) + + let int_lb x = if is_ge_zero x then Some 0 else None + + let int_ub x = if is_le_zero x then Some 0 else None end module Bound = struct @@ -616,6 +627,28 @@ module Bound = struct assert false + let int_lb = function + | MInf -> + None + | PInf -> + assert false + | MinMax _ as b -> + int_lb_of_minmax b + | Linear (c, se) -> + SymLinear.int_lb se |> Option.map ~f:(( + ) c) + + + let int_ub = function + | MInf -> + assert false + | PInf -> + None + | MinMax _ as b -> + int_ub_of_minmax b + | Linear (c, se) -> + SymLinear.int_ub se |> Option.map ~f:(( + ) c) + + let linear_ub_of_minmax = function | MinMax (c, Plus, Min, _, x) -> Some (Linear (c, SymLinear.singleton_one x)) @@ -970,6 +1003,13 @@ module NonNegativeBound = struct let of_bound b = if Bound.le b Bound.zero then Bound.zero else b + let int_lb b = + Bound.int_lb b |> Option.bind ~f:NonNegativeInt.of_int + |> Option.value ~default:NonNegativeInt.zero + + + let int_ub b = Bound.int_ub b |> Option.map ~f:NonNegativeInt.of_int_exn + let classify = function | Bound.PInf -> ValTop @@ -994,6 +1034,10 @@ end module type NonNegativeSymbol = sig type t [@@deriving compare] + val int_lb : t -> NonNegativeInt.t + + val int_ub : t -> NonNegativeInt.t option + val subst : t -> Bound.t bottom_lifted SymbolMap.t -> (NonNegativeInt.t, t) valclass val pp : F.formatter -> t -> unit @@ -1141,12 +1185,33 @@ module MakePolynomial (S : NonNegativeSymbol) = struct mult_const p1 p2.const |> M.fold (fun s p acc -> plus (mult_symb (mult p p1) s) acc) p2.terms + let rec int_lb {const; terms} = + M.fold + (fun symbol polynomial acc -> + let s_lb = S.int_lb symbol in + let p_lb = int_lb polynomial in + NonNegativeInt.((s_lb * p_lb) + acc) ) + terms const + + + let rec int_ub {const; terms} = + M.fold + (fun symbol polynomial acc -> + Option.bind acc ~f:(fun acc -> + Option.bind (S.int_ub symbol) ~f:(fun s_ub -> + Option.map (int_ub polynomial) ~f:(fun p_ub -> NonNegativeInt.((s_ub * p_ub) + acc)) + ) ) ) + terms (Some const) + + (* assumes symbols are not comparable *) let rec ( <= ) : lhs:t -> rhs:t -> bool = fun ~lhs ~rhs -> phys_equal lhs rhs || NonNegativeInt.( <= ) ~lhs:lhs.const ~rhs:rhs.const && M.le ~le_elt:( <= ) lhs.terms rhs.terms + || Option.exists (int_ub lhs) ~f:(fun lhs_ub -> + NonNegativeInt.( <= ) ~lhs:lhs_ub ~rhs:(int_lb rhs) ) let rec xcompare ~lhs ~rhs = diff --git a/infer/tests/codetoanalyze/c/performance/cost_test.c b/infer/tests/codetoanalyze/c/performance/cost_test.c index 0e3cba0b5..785e7aa2c 100644 --- a/infer/tests/codetoanalyze/c/performance/cost_test.c +++ b/infer/tests/codetoanalyze/c/performance/cost_test.c @@ -125,4 +125,4 @@ void call_while_upto20_minus100_bad() { while_upto20_bad(-100); } void call_while_upto20_10_good() { while_upto20_bad(10); } -void call_while_upto20_unsigned_good_FP(unsigned x) { while_upto20_bad(x); } +void call_while_upto20_unsigned_good(unsigned x) { while_upto20_bad(x); } diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp index 6b370980b..6fe0dd644 100644 --- a/infer/tests/codetoanalyze/c/performance/issues.exp +++ b/infer/tests/codetoanalyze/c/performance/issues.exp @@ -33,7 +33,6 @@ codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 13, 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/cost_test.c, call_while_upto20_minus100_bad, 0, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 604] -codetoanalyze/c/performance/cost_test.c, call_while_upto20_unsigned_good_FP, 0, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 * (-u$0 + 20)] codetoanalyze/c/performance/cost_test.c, loop0_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1002] codetoanalyze/c/performance/cost_test.c, loop0_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1002] codetoanalyze/c/performance/cost_test.c, loop0_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1004]