From 9f9dbdb914043ddda5799c03699465c67231df00 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 26 Sep 2017 05:05:26 -0700 Subject: [PATCH] [Inferbo] Extend abstract domain for vector::empty Summary: The interval bound of the abstract domain is extended. `[min|max](int, symbol)` => `int [+|-] [min|max](int, symbol)` As a result, `vector::empty` can be modelled to return a more precise value: `1 - min(1, size)`. Reviewed By: mbouaziz Differential Revision: D5899404 fbshipit-source-id: c8c3f49 --- .../infer_model/vector_bufferoverrun.h | 6 +- .../src/bufferoverrun/bufferOverrunChecker.ml | 15 + .../bufferoverrun/bufferOverrunSemantics.ml | 2 +- infer/src/bufferoverrun/itv.ml | 448 ++++++++++++------ .../cpp/bufferoverrun/issues.exp | 3 + .../cpp/bufferoverrun/vector.cpp | 18 + 6 files changed, 334 insertions(+), 158 deletions(-) diff --git a/infer/models/cpp/include/infer_model/vector_bufferoverrun.h b/infer/models/cpp/include/infer_model/vector_bufferoverrun.h index c997359ce..bc907ba26 100644 --- a/infer/models/cpp/include/infer_model/vector_bufferoverrun.h +++ b/infer/models/cpp/include/infer_model/vector_bufferoverrun.h @@ -27,6 +27,10 @@ #include #endif +extern "C" { +int __inferbo_min(int, int); +} + INFER_NAMESPACE_STD_BEGIN struct bool_ref { @@ -212,7 +216,7 @@ class vector { size_type capacity() const noexcept {} - bool empty() const noexcept { return infer_size == 0; } + bool empty() const noexcept { return 1 - __inferbo_min(infer_size, 1); } size_type max_size() const noexcept; void reserve(size_type __n); void shrink_to_fit() noexcept; diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 64482afe5..d133d0f9e 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -80,6 +80,19 @@ module TransferFunctions (CFG : ProcCfg.S) = struct fun pname ret params node location mem -> model_malloc pname ret (List.tl_exn params) node location mem + let model_min + : (Ident.t * Typ.t) option -> (Exp.t * Typ.t) list -> Location.t -> Dom.Mem.astate + -> Dom.Mem.astate = + fun ret params location mem -> + match (ret, params) with + | Some (id, _), [(e1, _); (e2, _)] + -> let i1 = Sem.eval e1 mem location |> Dom.Val.get_itv in + let i2 = Sem.eval e2 mem location |> Dom.Val.get_itv in + let v = Itv.min_sem i1 i2 |> Dom.Val.of_itv in + mem |> Dom.Mem.add_stack (Loc.of_id id) v + | _ + -> mem + let model_by_value value ret mem = match ret with | Some (id, _) @@ -118,6 +131,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct -> CFG.node -> Dom.Mem.astate -> Location.t -> Dom.Mem.astate = fun pname ret callee_pname params node mem loc -> match Typ.Procname.get_method callee_pname with + | "__inferbo_min" + -> model_min ret params loc mem | "__exit" | "exit" -> Dom.Mem.Bottom | "fgetc" diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 00d1646d4..3e05ea122 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -492,7 +492,7 @@ module Make (CFG : ProcCfg.S) = struct if Int.equal coeff 1 then (Itv.SubstMap.add symbol actual bound_map, Itv.SubstMap.add symbol traces trace_map) else assert false - | Itv.Bound.MinMax (Itv.Bound.Max, 0, symbol) + | Itv.Bound.MinMax (0, Itv.Bound.Plus, Itv.Bound.Max, 0, symbol) -> (Itv.SubstMap.add symbol actual bound_map, Itv.SubstMap.add symbol traces trace_map) | _ -> assert false diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 5a03da61b..92019a4e3 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -16,6 +16,8 @@ module L = Logging let sym_size = ref 0 +exception Not_one_symbol + module Symbol = struct type t = Typ.Procname.t * int [@@deriving compare] @@ -58,6 +60,8 @@ module SymLinear = struct let initial : t = empty + let singleton : Symbol.t -> int -> t = M.singleton + let find : Symbol.t -> t -> int = fun s x -> try M.find s x @@ -132,34 +136,63 @@ module SymLinear = struct let div_const : t -> int -> t = fun x n -> M.map (( / ) n) x - (* Returns a symbol when the map contains only one symbol s with the - coefficient 1. *) - let one_symbol : t -> Symbol.t option = - fun x -> + (* Returns a symbol when the map contains only one symbol s with a + given coefficient. *) + let one_symbol_of_coeff : int -> t -> Symbol.t option = + fun coeff x -> let x = M.filter (fun _ v -> v <> 0) x in if Int.equal (M.cardinal x) 1 then let k, v = M.min_binding x in - if Int.equal v 1 then Some k else None + if Int.equal v coeff then Some k else None else None - let is_one_symbol : t -> bool = fun x -> match one_symbol x with Some _ -> true | None -> false + let get_one_symbol_opt : t -> Symbol.t option = one_symbol_of_coeff 1 + + let get_mone_symbol_opt : t -> Symbol.t option = one_symbol_of_coeff (-1) + + let get_one_symbol : t -> Symbol.t = + fun x -> match get_one_symbol_opt x with Some s -> s | None -> raise Not_one_symbol + + let get_mone_symbol : t -> Symbol.t = + fun x -> match get_mone_symbol_opt x with Some s -> s | None -> raise Not_one_symbol + + let is_one_symbol : t -> bool = + fun x -> match get_one_symbol_opt x with Some _ -> true | None -> false + + let is_mone_symbol : t -> bool = + fun x -> match get_mone_symbol_opt x with Some _ -> true | None -> false let get_symbols : t -> Symbol.t list = fun x -> List.map ~f:fst (M.bindings x) end module Bound = struct + type sign_t = Plus | Minus [@@deriving compare] + + let sign_equal = [%compare.equal : sign_t] + + let neg_sign = function Plus -> Minus | Minus -> Plus + + type min_max_t = Min | Max [@@deriving compare] + + let min_max_equal = [%compare.equal : min_max_t] + + let neg_min_max = function Min -> Max | Max -> Min + + (* MinMax constructs a bound that is in the "int [+|-] [min|max](int, symbol)" format. + e.g. `MinMax (1, Minus, Max, 2, s)` means "1 - max (2, s)". *) type t = | MInf | Linear of int * SymLinear.t - | MinMax of min_max_t * int * Symbol.t + | MinMax of int * sign_t * min_max_t * int * Symbol.t | PInf | Bot [@@deriving compare] - and min_max_t = Min | Max - let equal = [%compare.equal : t] + let pp_sign ~need_plus : F.formatter -> sign_t -> unit = + fun fmt -> function Plus -> if need_plus then F.fprintf fmt "+" | Minus -> F.fprintf fmt "-" + let pp_min_max : F.formatter -> min_max_t -> unit = fun fmt -> function Min -> F.fprintf fmt "min" | Max -> F.fprintf fmt "max" @@ -176,8 +209,10 @@ module Bound = struct -> if SymLinear.le x SymLinear.empty then F.fprintf fmt "%d" c else if Int.equal c 0 then F.fprintf fmt "%a" SymLinear.pp x else F.fprintf fmt "%a + %d" SymLinear.pp x c - | MinMax (m, c, x) - -> F.fprintf fmt "%a(%d, %a)" pp_min_max m c Symbol.pp x + | MinMax (c, sign, m, d, x) + -> if Int.equal c 0 then F.fprintf fmt "%a" (pp_sign ~need_plus:false) sign + else F.fprintf fmt "%d%a" c (pp_sign ~need_plus:true) sign ; + F.fprintf fmt "%a(%d, %a)" pp_min_max m d Symbol.pp x let of_int : int -> t = fun n -> Linear (n, SymLinear.empty) @@ -203,17 +238,27 @@ module Bound = struct fun s -> function | Linear (c, se) - -> Int.equal c 0 && opt_lift Symbol.eq (SymLinear.one_symbol se) (Some s) + -> Int.equal c 0 && opt_lift Symbol.eq (SymLinear.get_one_symbol_opt se) (Some s) | _ -> false - let one_symbol : t -> Symbol.t option = function - | Linear (c, se) when Int.equal c 0 - -> SymLinear.one_symbol se - | _ - -> None + let lift_get_one_symbol : (SymLinear.t -> Symbol.t option) -> t -> Symbol.t option = + fun f -> function Linear (c, se) when Int.equal c 0 -> f se | _ -> None + + let get_one_symbol_opt : t -> Symbol.t option = lift_get_one_symbol SymLinear.get_one_symbol_opt + + let get_mone_symbol_opt : t -> Symbol.t option = + lift_get_one_symbol SymLinear.get_mone_symbol_opt + + let get_one_symbol : t -> Symbol.t = + fun x -> match get_one_symbol_opt x with Some s -> s | None -> raise Not_one_symbol - let is_one_symbol : t -> bool = fun x -> one_symbol x <> None + let get_mone_symbol : t -> Symbol.t = + fun x -> match get_mone_symbol_opt x with Some s -> s | None -> raise Not_one_symbol + + let is_one_symbol : t -> bool = fun x -> get_one_symbol_opt x <> None + + let is_mone_symbol : t -> bool = fun x -> get_mone_symbol_opt x <> None let use_symbol : Symbol.t -> t -> bool = fun s -> @@ -222,7 +267,7 @@ module Bound = struct -> false | Linear (_, se) -> SymLinear.find s se <> 0 - | MinMax (_, _, s') + | MinMax (_, _, _, _, s') -> Symbol.eq s s' let subst1 : t -> t -> Symbol.t -> t -> t = @@ -238,24 +283,50 @@ module Bound = struct let se1 = SymLinear.add s 0 se1 in let se' = SymLinear.plus se1 (SymLinear.mult_const se2 coeff) in Linear (c', se') - | MinMax (Min, _, s'), MInf when Symbol.eq s s' + | MinMax (_, Plus, Min, _, _), MInf -> MInf - | MinMax (Max, c, s'), MInf when Symbol.eq s s' - -> Linear (c, SymLinear.zero) - | MinMax (Max, _, s'), PInf when Symbol.eq s s' + | MinMax (_, Minus, Min, _, _), MInf -> PInf - | MinMax (Min, c, s'), PInf when Symbol.eq s s' - -> Linear (c, SymLinear.zero) - | MinMax (Min, c1, s'), Linear (c2, se) when Symbol.eq s s' && SymLinear.is_zero se - -> Linear (min c1 c2, SymLinear.zero) - | MinMax (Max, c1, s'), Linear (c2, se) when Symbol.eq s s' && SymLinear.is_zero se - -> Linear (max c1 c2, SymLinear.zero) - | MinMax (m, c, s'), _ when Symbol.eq s s' && is_one_symbol y -> ( - match one_symbol y with Some s'' -> MinMax (m, c, s'') | _ -> assert false ) - | MinMax (Min, c1, s'), MinMax (Min, c2, s'') when Symbol.eq s s' - -> MinMax (Min, min c1 c2, s'') - | MinMax (Max, c1, s'), MinMax (Max, c2, s'') when Symbol.eq s s' - -> MinMax (Max, max c1 c2, s'') + | MinMax (_, Plus, Max, _, _), PInf + -> PInf + | MinMax (_, Minus, Max, _, _), PInf + -> MInf + | MinMax (c, Plus, Min, d, _), PInf + -> Linear (c + d, SymLinear.zero) + | MinMax (c, Minus, Min, d, _), PInf + -> Linear (c - d, SymLinear.zero) + | MinMax (c, Plus, Max, d, _), MInf + -> Linear (c + d, SymLinear.zero) + | MinMax (c, Minus, Max, d, _), MInf + -> Linear (c - d, SymLinear.zero) + | MinMax (c1, Plus, Min, d1, _), Linear (c2, se) when SymLinear.is_zero se + -> Linear (c1 + min d1 c2, SymLinear.zero) + | MinMax (c1, Minus, Min, d1, _), Linear (c2, se) when SymLinear.is_zero se + -> Linear (c1 - min d1 c2, SymLinear.zero) + | MinMax (c1, Plus, Max, d1, _), Linear (c2, se) when SymLinear.is_zero se + -> Linear (c1 + max d1 c2, SymLinear.zero) + | MinMax (c1, Minus, Max, d1, _), Linear (c2, se) when SymLinear.is_zero se + -> Linear (c1 - max d1 c2, SymLinear.zero) + | MinMax (c, sign, m, d, _), _ when is_one_symbol y + -> MinMax (c, sign, m, d, get_one_symbol y) + | MinMax (c, sign, m, d, _), _ when is_mone_symbol y + -> MinMax (c, neg_sign sign, neg_min_max m, -d, get_mone_symbol y) + | MinMax (c1, Plus, Min, d1, _), MinMax (c2, Plus, Min, d2, s') + -> MinMax (c1 + c2, Plus, Min, min (d1 - c2) d2, s') + | MinMax (c1, Plus, Max, d1, _), MinMax (c2, Plus, Max, d2, s') + -> MinMax (c1 + c2, Plus, Max, max (d1 - c2) d2, s') + | MinMax (c1, Minus, Min, d1, _), MinMax (c2, Plus, Min, d2, s') + -> MinMax (c1 - c2, Minus, Min, min (d1 - c2) d2, s') + | MinMax (c1, Minus, Max, d1, _), MinMax (c2, Plus, Max, d2, s') + -> MinMax (c1 - c2, Minus, Max, max (d1 - c2) d2, s') + | MinMax (c1, Plus, Min, d1, _), MinMax (c2, Minus, Max, d2, s') + -> MinMax (c1 + c2, Minus, Max, max (-d1 + c2) d2, s') + | MinMax (c1, Plus, Max, d1, _), MinMax (c2, Minus, Min, d2, s') + -> MinMax (c1 + c2, Minus, Min, min (-d1 + c2) d2, s') + | MinMax (c1, Minus, Min, d1, _), MinMax (c2, Minus, Max, d2, s') + -> MinMax (c1 - c2, Minus, Max, max (-d1 + c2) d2, s') + | MinMax (c1, Minus, Max, d1, _), MinMax (c2, Minus, Min, d2, s') + -> MinMax (c1 - c2, Minus, Min, min (-d1 + c2) d2, s') | _ -> default @@ -263,7 +334,54 @@ module Bound = struct let subst : t -> t -> t SubstMap.t -> t = fun default x map -> SubstMap.fold (fun s y x -> subst1 default x s y) map x - let le : t -> t -> bool = + let int_ub_of_minmax = function + | MinMax (c, Plus, Min, d, _) + -> Some (c + d) + | MinMax (c, Minus, Max, d, _) + -> Some (c - d) + | MinMax _ + -> None + | MInf | PInf | Linear _ | Bot + -> assert false + + let int_lb_of_minmax = function + | MinMax (c, Plus, Max, d, _) + -> Some (c + d) + | MinMax (c, Minus, Min, d, _) + -> Some (c - d) + | MinMax _ + -> None + | MInf | PInf | Linear _ | Bot + -> assert false + + let linear_ub_of_minmax = function + | MinMax (c, Plus, Min, _, x) + -> Some (Linear (c, SymLinear.singleton x 1)) + | MinMax (c, Minus, Max, _, x) + -> Some (Linear (c, SymLinear.singleton x (-1))) + | MinMax _ + -> None + | MInf | PInf | Linear _ | Bot + -> assert false + + let linear_lb_of_minmax = function + | MinMax (c, Plus, Max, _, x) + -> Some (Linear (c, SymLinear.singleton x 1)) + | MinMax (c, Minus, Min, _, x) + -> Some (Linear (c, SymLinear.singleton x (-1))) + | MinMax _ + -> None + | MInf | PInf | Linear _ | Bot + -> assert false + + let le_minmax_by_int x y = + match (int_ub_of_minmax x, int_lb_of_minmax y) with Some n, Some m -> n <= m | _, _ -> false + + let le_opt1 le opt_n m = Option.value_map opt_n ~default:false ~f:(fun n -> le n m) + + let le_opt2 le n opt_m = Option.value_map opt_m ~default:false ~f:(fun m -> le n m) + + let rec le : t -> t -> bool = fun x y -> assert (x <> Bot && y <> Bot) ; match (x, y) with @@ -273,16 +391,22 @@ module Bound = struct -> false | Linear (c0, x0), Linear (c1, x1) -> c0 <= c1 && SymLinear.eq x0 x1 - | MinMax (Min, c0, x0), MinMax (Min, c1, x1) | MinMax (Max, c0, x0), MinMax (Max, c1, x1) - -> c0 <= c1 && Symbol.eq x0 x1 - | MinMax (Min, c0, x0), Linear (c1, x1) - -> c0 <= c1 && SymLinear.is_zero x1 - || Int.equal c1 0 && opt_lift Symbol.eq (SymLinear.one_symbol x1) (Some x0) - | Linear (c1, x1), MinMax (Max, c0, x0) - -> c1 <= c0 && SymLinear.is_zero x1 - || Int.equal c1 0 && opt_lift Symbol.eq (SymLinear.one_symbol x1) (Some x0) - | MinMax (Min, c0, x0), MinMax (Max, c1, x1) - -> c0 <= c1 || Symbol.eq x0 x1 + | MinMax (c1, sign1, m1, d1, x1), MinMax (c2, sign2, m2, d2, x2) + when sign_equal sign1 sign2 && min_max_equal m1 m2 + -> c1 <= c2 && Int.equal d1 d2 && Symbol.eq x1 x2 + | MinMax _, MinMax _ when le_minmax_by_int x y + -> true + | MinMax (c1, Plus, Min, _, x1), MinMax (c2, Plus, Max, _, x2) + | MinMax (c1, Minus, Max, _, x1), MinMax (c2, Minus, Min, _, x2) + -> c1 <= c2 && Symbol.eq x1 x2 + | MinMax _, Linear (c, se) when SymLinear.is_zero se + -> le_opt1 ( <= ) (int_ub_of_minmax x) c + | MinMax _, Linear _ + -> le_opt1 le (linear_ub_of_minmax x) y + | Linear (c, se), MinMax _ when SymLinear.is_zero se + -> le_opt2 ( <= ) c (int_lb_of_minmax y) + | Linear _, MinMax _ + -> le_opt2 le x (linear_lb_of_minmax y) | _, _ -> false @@ -292,14 +416,10 @@ module Bound = struct match (x, y) with | MInf, Linear _ | MInf, MinMax _ | MInf, PInf | Linear _, PInf | MinMax _, PInf -> true - | Linear (c0, x0), Linear (c1, x1) - -> c0 < c1 && SymLinear.eq x0 x1 - | MinMax (Min, c0, _), Linear (c1, x1) - -> c0 < c1 && SymLinear.is_zero x1 - | Linear (c1, x1), MinMax (Max, c0, _) - -> c1 < c0 && SymLinear.is_zero x1 - | MinMax (Min, c0, _), MinMax (Max, c1, _) - -> c0 < c1 + | Linear (c, x), _ + -> le (Linear (c + 1, x)) y + | MinMax (c, sign, min_max, d, x), _ + -> le (MinMax (c + 1, sign, min_max, d, x)) y | _, _ -> false @@ -311,59 +431,77 @@ module Bound = struct else if equal x Bot || equal y Bot then false else le x y && le y x - let min : t -> t -> t = - fun x y -> + let remove_max_int : t -> t = + fun x -> + match x with + | MinMax (c, Plus, Max, _, s) + -> Linear (c, SymLinear.singleton s 1) + | MinMax (c, Minus, Min, _, s) + -> Linear (c, SymLinear.singleton s (-1)) + | _ + -> x + + let rec lb : ?default:t -> t -> t -> t = + fun ?(default= MInf) x y -> assert (x <> Bot && y <> Bot) ; if le x y then x else if le y x then y else match (x, y) with - | Linear (c0, x0), Linear (c1, x1) - when SymLinear.is_zero x0 && Int.equal c1 0 && SymLinear.is_one_symbol x1 -> ( - match SymLinear.one_symbol x1 with - | Some x' - -> MinMax (Min, c0, x') - | None - -> assert false ) - | Linear (c0, x0), Linear (c1, x1) - when SymLinear.is_zero x1 && Int.equal c0 0 && SymLinear.is_one_symbol x0 -> ( - match SymLinear.one_symbol x0 with - | Some x' - -> MinMax (Min, c1, x') - | None - -> assert false ) - | MinMax (Max, c0, _), Linear (c1, x1) - | Linear (c1, x1), MinMax (Max, c0, _) - when SymLinear.is_zero x1 && c0 < c1 - -> Linear (c0, x1) + | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_zero x1 && SymLinear.is_one_symbol x2 + -> MinMax (c2, Plus, Min, c1 - c2, SymLinear.get_one_symbol x2) + | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_one_symbol x1 && SymLinear.is_zero x2 + -> MinMax (c1, Plus, Min, c2 - c1, SymLinear.get_one_symbol x1) + | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_zero x1 && SymLinear.is_mone_symbol x2 + -> MinMax (c2, Minus, Max, c2 - c1, SymLinear.get_mone_symbol x2) + | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_mone_symbol x1 && SymLinear.is_zero x2 + -> MinMax (c1, Minus, Max, c1 - c2, SymLinear.get_mone_symbol x1) + | MinMax (c1, Plus, Min, d1, s), Linear (c2, se) + | Linear (c2, se), MinMax (c1, Plus, Min, d1, s) + when SymLinear.is_zero se + -> MinMax (c1, Plus, Min, min d1 (c2 - c1), s) + | MinMax (c1, Plus, Max, _, s), Linear (c2, se) + | Linear (c2, se), MinMax (c1, Plus, Max, _, s) + when SymLinear.is_zero se + -> MinMax (c1, Plus, Min, c2 - c1, s) + | MinMax (c1, Minus, Min, _, s), Linear (c2, se) + | Linear (c2, se), MinMax (c1, Minus, Min, _, s) + when SymLinear.is_zero se + -> MinMax (c1, Minus, Max, c1 - c2, s) + | MinMax (c1, Minus, Max, d1, s), Linear (c2, se) + | Linear (c2, se), MinMax (c1, Minus, Max, d1, s) + when SymLinear.is_zero se + -> MinMax (c1, Minus, Max, max d1 (c1 - c2), s) + | MinMax (_, Plus, Min, _, _), MinMax (_, Plus, Max, _, _) + | MinMax (_, Plus, Min, _, _), MinMax (_, Minus, Min, _, _) + | MinMax (_, Minus, Max, _, _), MinMax (_, Plus, Max, _, _) + | MinMax (_, Minus, Max, _, _), MinMax (_, Minus, Min, _, _) + -> lb ~default x (remove_max_int y) + | MinMax (_, Plus, Max, _, _), MinMax (_, Plus, Min, _, _) + | MinMax (_, Minus, Min, _, _), MinMax (_, Plus, Min, _, _) + | MinMax (_, Plus, Max, _, _), MinMax (_, Minus, Max, _, _) + | MinMax (_, Minus, Min, _, _), MinMax (_, Minus, Max, _, _) + -> lb ~default (remove_max_int x) y + | MinMax (c1, Plus, Max, d1, _), MinMax (c2, Plus, Max, d2, _) + -> Linear (min (c1 + d1) (c2 + d2), SymLinear.zero) | _, _ - -> MInf + -> default - let max : t -> t -> t = + let ub : t -> t -> t = fun x y -> assert (x <> Bot && y <> Bot) ; if le x y then y else if le y x then x else match (x, y) with - | Linear (c0, x0), Linear (c1, x1) - when SymLinear.is_zero x0 && Int.equal c1 0 && SymLinear.is_one_symbol x1 -> ( - match SymLinear.one_symbol x1 with - | Some x' - -> MinMax (Max, c0, x') - | None - -> assert false ) - | Linear (c0, x0), Linear (c1, x1) - when SymLinear.is_zero x1 && Int.equal c0 0 && SymLinear.is_one_symbol x0 -> ( - match SymLinear.one_symbol x0 with - | Some x' - -> MinMax (Max, c1, x') - | None - -> assert false ) - | MinMax (Min, c0, _), Linear (c1, x1) - | Linear (c1, x1), MinMax (Min, c0, _) - when SymLinear.is_zero x1 && c0 > c1 - -> Linear (c0, x1) + | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_zero x1 && SymLinear.is_one_symbol x2 + -> MinMax (c2, Plus, Max, c1 - c2, SymLinear.get_one_symbol x2) + | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_one_symbol x1 && SymLinear.is_zero x2 + -> MinMax (c1, Plus, Max, c2 - c1, SymLinear.get_one_symbol x1) + | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_zero x1 && SymLinear.is_mone_symbol x2 + -> MinMax (c2, Minus, Min, c2 - c1, SymLinear.get_mone_symbol x2) + | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_mone_symbol x1 && SymLinear.is_zero x2 + -> MinMax (c1, Minus, Min, c1 - c2, SymLinear.get_mone_symbol x1) | _, _ -> PInf @@ -409,8 +547,16 @@ module Bound = struct -> x | Linear (c1, x1), Linear (c2, x2) -> Linear (c1 + c2, SymLinear.plus x1 x2) - | MinMax (Max, c1, _), Linear (c2, x2) | Linear (c2, x2), MinMax (Max, c1, _) - -> Linear (c1 + c2, x2) + | MinMax (c1, sign, min_max, d1, x1), Linear (c2, x2) + | Linear (c2, x2), MinMax (c1, sign, min_max, d1, x1) + when SymLinear.is_zero x2 + -> MinMax (c1 + c2, sign, min_max, d1, x1) + | MinMax (c1, Plus, Max, d1, _), Linear (c2, x2) + | Linear (c2, x2), MinMax (c1, Plus, Max, d1, _) + -> Linear (c1 + d1 + c2, x2) + | MinMax (c1, Minus, Min, d1, _), Linear (c2, x2) + | Linear (c2, x2), MinMax (c1, Minus, Min, d1, _) + -> Linear (c1 - d1 + c2, x2) | _, _ -> MInf @@ -424,8 +570,16 @@ module Bound = struct -> x | Linear (c1, x1), Linear (c2, x2) -> Linear (c1 + c2, SymLinear.plus x1 x2) - | MinMax (Min, c1, _), Linear (c2, x2) | Linear (c2, x2), MinMax (Min, c1, _) - -> Linear (c1 + c2, x2) + | MinMax (c1, sign, min_max, d1, x1), Linear (c2, x2) + | Linear (c2, x2), MinMax (c1, sign, min_max, d1, x1) + when SymLinear.is_zero x2 + -> MinMax (c1 + c2, sign, min_max, d1, x1) + | MinMax (c1, Plus, Min, d1, _), Linear (c2, x2) + | Linear (c2, x2), MinMax (c1, Plus, Min, d1, _) + -> Linear (c1 + d1 + c2, x2) + | MinMax (c1, Minus, Max, d1, _), Linear (c2, x2) + | Linear (c2, x2), MinMax (c1, Minus, Max, d1, _) + -> Linear (c1 - d1 + c2, x2) | _, _ -> PInf @@ -467,34 +621,17 @@ module Bound = struct -> Some MInf | Linear (c, x) -> Some (Linear (-c, SymLinear.neg x)) - | MinMax _ - -> None + | MinMax (c, sign, min_max, d, x) + -> Some (MinMax (-c, neg_sign sign, min_max, d, x)) | Bot -> assert false - let make_min_max : min_max_t -> t -> t -> t option = - fun m x y -> - assert (x <> Bot && y <> Bot) ; - match (x, y) with - | Linear (cx, x'), Linear (cy, y') - when Int.equal cy 0 && SymLinear.is_zero x' && SymLinear.is_one_symbol y' -> ( - match SymLinear.one_symbol y' with Some s -> Some (MinMax (m, cx, s)) | None -> None ) - | Linear (cx, x'), Linear (cy, y') - when Int.equal cx 0 && SymLinear.is_zero y' && SymLinear.is_one_symbol x' -> ( - match SymLinear.one_symbol x' with Some s -> Some (MinMax (m, cy, s)) | None -> None ) - | _, _ - -> None - - let make_min : t -> t -> t option = make_min_max Min - - let make_max : t -> t -> t option = make_min_max Max - let get_symbols : t -> Symbol.t list = function | MInf | PInf -> [] | Linear (_, se) -> SymLinear.get_symbols se - | MinMax (_, _, s) + | MinMax (_, _, _, _, s) -> [s] | Bot -> assert false @@ -525,7 +662,7 @@ module ItvPure = struct let ( <= ) : lhs:t -> rhs:t -> bool = fun ~lhs:(l1, u1) ~rhs:(l2, u2) -> Bound.le l2 l1 && Bound.le u1 u2 - let join : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.min l1 l2, Bound.max u1 u2) + let join : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.lb l1 l2, Bound.ub u1 u2) let widen : prev:t -> next:t -> num_iters:int -> t = fun ~prev:(l1, u1) ~next:(l2, u2) ~num_iters:_ -> (Bound.widen_l l1 l2, Bound.widen_u u1 u2) @@ -549,7 +686,8 @@ module ItvPure = struct let make_sym : unsigned:bool -> Typ.Procname.t -> (unit -> int) -> t = fun ~unsigned pname new_sym_num -> let lower = - if unsigned then Bound.MinMax (Bound.Max, 0, Symbol.make pname (new_sym_num ())) + if unsigned then + Bound.MinMax (0, Bound.Plus, Bound.Max, 0, Symbol.make pname (new_sym_num ())) else Bound.of_sym (SymLinear.make pname (new_sym_num ())) in let upper = Bound.of_sym (SymLinear.make pname (new_sym_num ())) in @@ -712,6 +850,8 @@ module ItvPure = struct else if is_false x && is_false y then false_sem else unknown_bool + let min_sem : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.lb l1 l2, Bound.lb ~default:u1 u1 u2) + let invalid : t -> bool = fun (l, u) -> Bound.equal l Bound.Bot || Bound.equal u Bound.Bot || Bound.eq l Bound.PInf @@ -724,25 +864,22 @@ module ItvPure = struct -> (l1, u2) | (l1, Bound.Linear (c1, s1)), (_, Bound.Linear (c2, s2)) when SymLinear.eq s1 s2 -> (l1, Bound.Linear (min c1 c2, s1)) - | (l1, Bound.Linear (c, se)), (_, u) when SymLinear.is_zero se && Bound.is_one_symbol u -> ( - match Bound.one_symbol u with - | Some s - -> (l1, Bound.MinMax (Bound.Min, c, s)) - | None - -> assert false ) - | (l1, u), (_, Bound.Linear (c, se)) when SymLinear.is_zero se && Bound.is_one_symbol u -> ( - match Bound.one_symbol u with - | Some s - -> (l1, Bound.MinMax (Bound.Min, c, s)) - | None - -> assert false ) - | (l1, Bound.Linear (c1, se)), (_, Bound.MinMax (Bound.Min, c2, se')) - | (l1, Bound.MinMax (Bound.Min, c1, se')), (_, Bound.Linear (c2, se)) + | (l1, Bound.Linear (c, se)), (_, u) when SymLinear.is_zero se && Bound.is_one_symbol u + -> (l1, Bound.MinMax (0, Bound.Plus, Bound.Min, c, Bound.get_one_symbol u)) + | (l1, u), (_, Bound.Linear (c, se)) when SymLinear.is_zero se && Bound.is_one_symbol u + -> (l1, Bound.MinMax (0, Bound.Plus, Bound.Min, c, Bound.get_one_symbol u)) + | (l1, Bound.Linear (c, se)), (_, u) when SymLinear.is_zero se && Bound.is_mone_symbol u + -> (l1, Bound.MinMax (0, Bound.Minus, Bound.Max, -c, Bound.get_mone_symbol u)) + | (l1, u), (_, Bound.Linear (c, se)) when SymLinear.is_zero se && Bound.is_mone_symbol u + -> (l1, Bound.MinMax (0, Bound.Minus, Bound.Max, -c, Bound.get_mone_symbol u)) + | (l1, Bound.Linear (c1, se)), (_, Bound.MinMax (c2, Bound.Plus, Bound.Min, d2, se')) + | (l1, Bound.MinMax (c2, Bound.Plus, Bound.Min, d2, se')), (_, Bound.Linear (c1, se)) when SymLinear.is_zero se - -> (l1, Bound.MinMax (Bound.Min, min c1 c2, se')) - | (l1, Bound.MinMax (Bound.Min, c1, se1)), (_, Bound.MinMax (Bound.Min, c2, se2)) - when Symbol.eq se1 se2 - -> (l1, Bound.MinMax (Bound.Min, min c1 c2, se1)) + -> (l1, Bound.MinMax (c2, Bound.Plus, Bound.Min, min (c1 - c2) d2, se')) + | ( (l1, Bound.MinMax (c1, Bound.Plus, Bound.Min, d1, se1)) + , (_, Bound.MinMax (c2, Bound.Plus, Bound.Min, d2, se2)) ) + when Int.equal c1 c2 && Symbol.eq se1 se2 + -> (l1, Bound.MinMax (c1, Bound.Plus, Bound.Min, min d1 d2, se1)) | _ -> x @@ -753,25 +890,22 @@ module ItvPure = struct -> (l2, u1) | (Bound.Linear (c1, s1), u1), (Bound.Linear (c2, s2), _) when SymLinear.eq s1 s2 -> (Bound.Linear (max c1 c2, s1), u1) - | (Bound.Linear (c, se), u1), (l, _) when SymLinear.is_zero se && Bound.is_one_symbol l -> ( - match Bound.one_symbol l with - | Some s - -> (Bound.MinMax (Bound.Max, c, s), u1) - | None - -> assert false ) - | (l, u1), (Bound.Linear (c, se), _) when SymLinear.is_zero se && Bound.is_one_symbol l -> ( - match Bound.one_symbol l with - | Some s - -> (Bound.MinMax (Bound.Max, c, s), u1) - | None - -> assert false ) - | (Bound.Linear (c1, se), u1), (Bound.MinMax (Bound.Max, c2, se'), _) - | (Bound.MinMax (Bound.Max, c1, se'), u1), (Bound.Linear (c2, se), _) + | (Bound.Linear (c, se), u1), (l, _) when SymLinear.is_zero se && Bound.is_one_symbol l + -> (Bound.MinMax (0, Bound.Plus, Bound.Max, c, Bound.get_one_symbol l), u1) + | (l, u1), (Bound.Linear (c, se), _) when SymLinear.is_zero se && Bound.is_one_symbol l + -> (Bound.MinMax (0, Bound.Plus, Bound.Max, c, Bound.get_one_symbol l), u1) + | (Bound.Linear (c, se), u1), (l, _) when SymLinear.is_zero se && Bound.is_mone_symbol l + -> (Bound.MinMax (0, Bound.Minus, Bound.Min, c, Bound.get_mone_symbol l), u1) + | (l, u1), (Bound.Linear (c, se), _) when SymLinear.is_zero se && Bound.is_mone_symbol l + -> (Bound.MinMax (0, Bound.Minus, Bound.Min, c, Bound.get_mone_symbol l), u1) + | (Bound.Linear (c1, se), u1), (Bound.MinMax (c2, Bound.Plus, Bound.Max, d2, se'), _) + | (Bound.MinMax (c2, Bound.Plus, Bound.Max, d2, se'), u1), (Bound.Linear (c1, se), _) when SymLinear.is_zero se - -> (Bound.MinMax (Bound.Max, max c1 c2, se'), u1) - | (Bound.MinMax (Bound.Max, c1, se1), u1), (Bound.MinMax (Bound.Max, c2, se2), _) - when Symbol.eq se1 se2 - -> (Bound.MinMax (Bound.Max, max c1 c2, se1), u1) + -> (Bound.MinMax (c2, Bound.Plus, Bound.Max, max (c1 - c2) d2, se'), u1) + | ( (Bound.MinMax (c1, Bound.Plus, Bound.Max, d1, se1), u1) + , (Bound.MinMax (c2, Bound.Plus, Bound.Max, d2, se2), _) ) + when Int.equal c1 c2 && Symbol.eq se1 se2 + -> (Bound.MinMax (c1, Bound.Plus, Bound.Max, max d1 d2, se1), u1) | _ -> x @@ -964,6 +1098,8 @@ let land_sem : t -> t -> t = lift2 ItvPure.land_sem let lor_sem : t -> t -> t = lift2 ItvPure.lor_sem +let min_sem : t -> t -> t = lift2 ItvPure.min_sem + let prune_zero : t -> t = lift1 ItvPure.prune_zero let prune_comp : Binop.t -> t -> t -> t = fun comp -> lift2_opt (ItvPure.prune_comp comp) diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index a313b2a3f..a1482cda2 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -14,6 +14,7 @@ codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, BUFFER_OVERRUN, [Call codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN, [Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [42, 42] Size: [42, 42] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `my_vector_oob_Bad()` ] codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN, [Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [max(0, s$4), s$5] Size: [max(0, s$4), s$5] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `int_vector_access_at()` ] codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, call_safe_access4_Good_FP, 2, BUFFER_OVERRUN, [Call,Call,Assignment,Call,Call,Assignment,Return,Call,Assignment,Call,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, 0]] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, BUFFER_OVERRUN, [Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN, [Call,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 17, BUFFER_OVERRUN, [Call,Call,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, +oo]] @@ -21,3 +22,5 @@ codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERR codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN, [Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [max(0, s$12), s$13] Size: [max(0, s$12), s$13]] codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN, [Call,Call,Assignment,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [1, 1] Size: [1, 1]] codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, 0]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, safe_access3_Good, 2, CONDITION_ALWAYS_FALSE, [] +codetoanalyze/cpp/bufferoverrun/vector.cpp, safe_access3_Good, 2, CONDITION_ALWAYS_TRUE, [] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp index a93309667..9ca0d20e6 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp @@ -103,3 +103,21 @@ void just_test_model_FP(void) { int y = v3[0]; int z = v3.at(1); } + +void safe_access3_Good() { + std::vector v; + if (!v.empty()) { + v[0] = 1; + } +} + +void safe_access4(std::vector v) { + if (!v.empty()) { + v[0] = 1; + } +} + +void call_safe_access4_Good_FP() { + std::vector v; + safe_access4(v); +}