From 70ab21d33c28678c885f2644001dedab22cd8480 Mon Sep 17 00:00:00 2001 From: Julian Sutherland Date: Tue, 7 Aug 2018 03:02:58 -0700 Subject: [PATCH] Finished splitting itv.ml Reviewed By: mbouaziz Differential Revision: D9149354 fbshipit-source-id: 3e7355321 --- infer/src/bufferoverrun/arrayBlk.ml | 5 +- infer/src/bufferoverrun/bounds.ml | 824 +++++++++++++++ infer/src/bufferoverrun/bounds.mli | 137 +++ .../bufferOverrunProofObligations.ml | 33 +- infer/src/bufferoverrun/counter.ml | 24 + infer/src/bufferoverrun/counter.mli | 15 + infer/src/bufferoverrun/itv.ml | 985 +----------------- infer/src/bufferoverrun/itv.mli | 72 +- infer/src/bufferoverrun/symb.ml | 134 +++ infer/src/bufferoverrun/symb.mli | 75 ++ 10 files changed, 1268 insertions(+), 1036 deletions(-) create mode 100644 infer/src/bufferoverrun/bounds.ml create mode 100644 infer/src/bufferoverrun/bounds.mli create mode 100644 infer/src/bufferoverrun/counter.ml create mode 100644 infer/src/bufferoverrun/counter.mli create mode 100644 infer/src/bufferoverrun/symb.ml create mode 100644 infer/src/bufferoverrun/symb.mli diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml index c975bf8ea..cf3572e58 100644 --- a/infer/src/bufferoverrun/arrayBlk.ml +++ b/infer/src/bufferoverrun/arrayBlk.ml @@ -11,6 +11,7 @@ open! IStd open AbsLoc open! AbstractDomain.Types +module Bound = Bounds.Bound module ArrInfo = struct type t = {offset: Itv.t; size: Itv.t; stride: Itv.t} [@@deriving compare] @@ -55,7 +56,7 @@ module ArrInfo = struct let diff : t -> t -> Itv.astate = fun arr1 arr2 -> Itv.minus arr1.offset arr2.offset - let subst : t -> Itv.Bound.t bottom_lifted Itv.SymbolMap.t -> t = + let subst : t -> Bound.t bottom_lifted Itv.SymbolMap.t -> t = fun arr subst_map -> {arr with offset= Itv.subst arr.offset subst_map; size= Itv.subst arr.size subst_map} @@ -136,7 +137,7 @@ let get_pow_loc : astate -> PowLoc.t = fold pow_loc_of_allocsite array PowLoc.bot -let subst : astate -> Itv.Bound.t bottom_lifted Itv.SymbolMap.t -> astate = +let subst : astate -> Bound.t bottom_lifted Itv.SymbolMap.t -> astate = fun a subst_map -> map (fun info -> ArrInfo.subst info subst_map) a diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml new file mode 100644 index 000000000..b196a63c6 --- /dev/null +++ b/infer/src/bufferoverrun/bounds.ml @@ -0,0 +1,824 @@ +(* + * Copyright (c) 2017-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd +open! AbstractDomain.Types +module F = Format +module L = Logging + +exception Symbol_not_found of Symb.Symbol.t + +exception Not_One_Symbol + +open Ints + +module SymLinear = struct + module M = Symb.SymbolMap + + (** + Map from symbols to integer coefficients. + { x -> 2, y -> 5 } represents the value 2 * x + 5 * y + *) + type t = NonZeroInt.t M.t [@@deriving compare] + + let empty : t = M.empty + + let is_empty : t -> bool = fun x -> M.is_empty x + + let singleton_one : Symb.Symbol.t -> t = fun s -> M.singleton s NonZeroInt.one + + let singleton_minus_one : Symb.Symbol.t -> t = fun s -> M.singleton s NonZeroInt.minus_one + + let is_le_zero : t -> bool = + fun x -> M.for_all (fun s v -> Symb.Symbol.is_unsigned s && NonZeroInt.is_negative v) x + + + let is_ge_zero : t -> bool = + fun x -> M.for_all (fun s v -> Symb.Symbol.is_unsigned s && NonZeroInt.is_positive v) x + + + let le : t -> t -> bool = + fun x y -> + let le_one_pair s v1_opt v2_opt = + let v1 = NonZeroInt.opt_to_int v1_opt in + let v2 = NonZeroInt.opt_to_int v2_opt in + Int.equal v1 v2 || (Symb.Symbol.is_unsigned s && v1 <= v2) + in + M.for_all2 ~f:le_one_pair x y + + + let make + : unsigned:bool -> Typ.Procname.t -> Symb.SymbolTable.t -> Symb.SymbolPath.t -> Counter.t + -> t * t = + fun ~unsigned pname symbol_table path new_sym_num -> + let lb, ub = Symb.SymbolTable.lookup ~unsigned pname path symbol_table new_sym_num in + (singleton_one lb, singleton_one ub) + + + let eq : t -> t -> bool = + fun x y -> + let eq_pair _ (coeff1: NonZeroInt.t option) (coeff2: NonZeroInt.t option) = + [%compare.equal : int option] (coeff1 :> int option) (coeff2 :> int option) + in + M.for_all2 ~f:eq_pair x y + + + let pp1 : F.formatter -> Symb.Symbol.t * NonZeroInt.t -> unit = + fun fmt (s, c) -> + let c = (c :> int) in + if Int.equal c 1 then Symb.Symbol.pp fmt s + else if Int.equal c (-1) then F.fprintf fmt "-%a" Symb.Symbol.pp s + else F.fprintf fmt "%dx%a" c Symb.Symbol.pp s + + + let pp : F.formatter -> t -> unit = + fun fmt x -> + if M.is_empty x then F.pp_print_string fmt "empty" + else Pp.seq ~sep:" + " pp1 fmt (M.bindings x) + + + let zero : t = M.empty + + let is_zero : t -> bool = M.is_empty + + let neg : t -> t = fun x -> M.map NonZeroInt.( ~- ) x + + let plus : t -> t -> t = + fun x y -> + let plus_coeff _ c1 c2 = NonZeroInt.plus c1 c2 in + M.union plus_coeff x y + + + let mult_const : NonZeroInt.t -> t -> t = fun n x -> M.map (NonZeroInt.( * ) n) x + + let exact_div_const_exn : t -> NonZeroInt.t -> t = + fun x n -> M.map (fun c -> NonZeroInt.exact_div_exn c n) x + + + (* Returns a symbol when the map contains only one symbol s with a + given coefficient. *) + let one_symbol_of_coeff : NonZeroInt.t -> t -> Symb.Symbol.t option = + fun coeff x -> + match M.is_singleton x with + | Some (k, v) when Int.equal (v :> int) (coeff :> int) -> + Some k + | _ -> + None + + + let fold m ~init ~f = + let f s coeff acc = f acc s coeff in + M.fold f m init + + + let get_one_symbol_opt : t -> Symb.Symbol.t option = one_symbol_of_coeff NonZeroInt.one + + let get_mone_symbol_opt : t -> Symb.Symbol.t option = one_symbol_of_coeff NonZeroInt.minus_one + + let get_one_symbol : t -> Symb.Symbol.t = + fun x -> match get_one_symbol_opt x with Some s -> s | None -> raise Not_One_Symbol + + + let get_mone_symbol : t -> Symb.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 is_one_symbol_of : Symb.Symbol.t -> t -> bool = + fun s x -> + Option.value_map (get_one_symbol_opt x) ~default:false ~f:(fun s' -> Symb.Symbol.equal s s') + + + let is_mone_symbol_of : Symb.Symbol.t -> t -> bool = + fun s x -> + Option.value_map (get_mone_symbol_opt x) ~default:false ~f:(fun s' -> Symb.Symbol.equal s s') + + + let get_symbols : t -> Symb.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 + + (** When two following symbols are from the same path, simplify what would lead to a zero sum. E.g. 2 * x.lb - x.ub = x.lb *) + let simplify_bound_ends_from_paths : t -> t = + fun x -> + let f (prev_opt, to_add) symb coeff = + match prev_opt with + | Some (prev_coeff, prev_symb) + when Symb.Symbol.paths_equal prev_symb symb + && NonZeroInt.is_positive coeff <> NonZeroInt.is_positive prev_coeff -> + let add_coeff = + (if NonZeroInt.is_positive coeff then NonZeroInt.max else NonZeroInt.min) + prev_coeff (NonZeroInt.( ~- ) coeff) + in + let to_add = + to_add |> M.add symb add_coeff |> M.add prev_symb (NonZeroInt.( ~- ) add_coeff) + in + (None, to_add) + | _ -> + (Some (coeff, symb), to_add) + in + let _, to_add = fold x ~init:(None, zero) ~f in + plus x to_add +end + +module Bound = struct + type sign = Plus | Minus [@@deriving compare] + + module Sign = struct + type t = sign [@@deriving compare] + + let equal = [%compare.equal : t] + + let neg = function Plus -> Minus | Minus -> Plus + + let eval_int x i1 i2 = match x with Plus -> i1 + i2 | Minus -> i1 - i2 + + let pp ~need_plus : F.formatter -> t -> unit = + fun fmt -> function + | Plus -> + if need_plus then F.pp_print_char fmt '+' + | Minus -> + F.pp_print_char fmt '-' + end + + type min_max = Min | Max [@@deriving compare] + + module MinMax = struct + type t = min_max [@@deriving compare] + + let equal = [%compare.equal : t] + + let neg = function Min -> Max | Max -> Min + + let eval_int x i1 i2 = match x with Min -> min i1 i2 | Max -> max i1 i2 + + let pp : F.formatter -> t -> unit = + fun fmt -> function Min -> F.pp_print_string fmt "min" | Max -> F.pp_print_string fmt "max" + end + + (* MinMax constructs a bound that is in the "int [+|-] [min|max](int, Symb.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 int * Sign.t * MinMax.t * int * Symb.Symbol.t + | PInf + [@@deriving compare] + + let pp : F.formatter -> t -> unit = + fun fmt -> function + | MInf -> + F.pp_print_string fmt "-oo" + | PInf -> + F.pp_print_string fmt "+oo" + | Linear (c, x) -> + if SymLinear.is_zero x then F.pp_print_int fmt c + else if Int.equal c 0 then SymLinear.pp fmt x + else F.fprintf fmt "%a + %d" SymLinear.pp x c + | MinMax (c, sign, m, d, x) -> + if Int.equal c 0 then (Sign.pp ~need_plus:false) fmt sign + else F.fprintf fmt "%d%a" c (Sign.pp ~need_plus:true) sign ; + F.fprintf fmt "%a(%d, %a)" MinMax.pp m d Symb.Symbol.pp x + + + let of_bound_end = function Symb.BoundEnd.LowerBound -> MInf | Symb.BoundEnd.UpperBound -> PInf + + let of_int : int -> t = fun n -> Linear (n, SymLinear.empty) + + let minus_one = of_int (-1) + + let _255 = of_int 255 + + let of_sym : SymLinear.t -> t = fun s -> Linear (0, s) + + let is_symbolic : t -> bool = function + | MInf | PInf -> + false + | Linear (_, se) -> + not (SymLinear.is_empty se) + | MinMax _ -> + true + + + let lift_symlinear : (SymLinear.t -> 'a option) -> t -> 'a option = + fun f -> function Linear (0, se) -> f se | _ -> None + + + let get_one_symbol_opt : t -> Symb.Symbol.t option = lift_symlinear SymLinear.get_one_symbol_opt + + let get_mone_symbol_opt : t -> Symb.Symbol.t option = + lift_symlinear SymLinear.get_mone_symbol_opt + + + let get_one_symbol : t -> Symb.Symbol.t = + fun x -> match get_one_symbol_opt x with Some s -> s | None -> raise Not_One_Symbol + + + let get_mone_symbol : t -> Symb.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 mk_MinMax (c, sign, m, d, s) = + if Symb.Symbol.is_unsigned s && d <= 0 then + match m with + | Min -> + of_int (Sign.eval_int sign c d) + | Max -> + match sign with + | Plus -> + Linear (c, SymLinear.singleton_one s) + | Minus -> + Linear (c, SymLinear.singleton_minus_one s) + else MinMax (c, sign, m, d, s) + + + let int_ub_of_minmax = function + | MinMax (c, Plus, Min, d, _) -> + Some (c + d) + | MinMax (c, Minus, Max, d, s) when Symb.Symbol.is_unsigned s -> + Some (min c (c - d)) + | MinMax (c, Minus, Max, d, _) -> + Some (c - d) + | MinMax _ -> + None + | MInf | PInf | Linear _ -> + assert false + + + let int_lb_of_minmax = function + | MinMax (c, Plus, Max, d, s) when Symb.Symbol.is_unsigned s -> + Some (max c (c + d)) + | MinMax (c, Plus, Max, d, _) -> + Some (c + d) + | MinMax (c, Minus, Min, d, _) -> + Some (c - d) + | MinMax _ -> + None + | MInf | PInf | Linear _ -> + assert false + + + let int_of_minmax = function + | Symb.BoundEnd.LowerBound -> + int_lb_of_minmax + | Symb.BoundEnd.UpperBound -> + int_ub_of_minmax + + + 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)) + | MinMax (c, Minus, Max, _, x) -> + Some (Linear (c, SymLinear.singleton_minus_one x)) + | MinMax _ -> + None + | MInf | PInf | Linear _ -> + assert false + + + let linear_lb_of_minmax = function + | MinMax (c, Plus, Max, _, x) -> + Some (Linear (c, SymLinear.singleton_one x)) + | MinMax (c, Minus, Min, _, x) -> + Some (Linear (c, SymLinear.singleton_minus_one x)) + | MinMax _ -> + None + | MInf | PInf | Linear _ -> + 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 -> + match (x, y) with + | MInf, _ | _, PInf -> + true + | _, MInf | PInf, _ -> + false + | Linear (c0, x0), Linear (c1, x1) -> + c0 <= c1 && SymLinear.le x0 x1 + | MinMax (c1, sign1, m1, d1, x1), MinMax (c2, sign2, m2, d2, x2) + when Sign.equal sign1 sign2 && MinMax.equal m1 m2 -> + c1 <= c2 && Int.equal d1 d2 && Symb.Symbol.equal 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 && Symb.Symbol.equal x1 x2 + | MinMax _, Linear (c, se) -> + (SymLinear.is_ge_zero se && le_opt1 Int.( <= ) (int_ub_of_minmax x) c) + || le_opt1 le (linear_ub_of_minmax x) y + | Linear (c, se), MinMax _ -> + (SymLinear.is_le_zero se && le_opt2 Int.( <= ) c (int_lb_of_minmax y)) + || le_opt2 le x (linear_lb_of_minmax y) + | _, _ -> + false + + + let lt : t -> t -> bool = + fun x y -> + match (x, y) with + | MInf, Linear _ | MInf, MinMax _ | MInf, PInf | Linear _, PInf | MinMax _, PInf -> + true + | Linear (c, x), _ -> + le (Linear (c + 1, x)) y + | MinMax (c, sign, min_max, d, x), _ -> + le (mk_MinMax (c + 1, sign, min_max, d, x)) y + | _, _ -> + false + + + let gt : t -> t -> bool = fun x y -> lt y x + + let eq : t -> t -> bool = fun x y -> le x y && le y x + + let xcompare = PartialOrder.of_le ~le + + let remove_max_int : t -> t = + fun x -> + match x with + | MinMax (c, Plus, Max, _, s) -> + Linear (c, SymLinear.singleton_one s) + | MinMax (c, Minus, Min, _, s) -> + Linear (c, SymLinear.singleton_minus_one s) + | _ -> + x + + + let rec lb : default:t -> t -> t -> t = + fun ~default x y -> + if le x y then x + else if le y x then y + else + match (x, y) with + | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_zero x1 && SymLinear.is_one_symbol x2 -> + mk_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 -> + mk_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 -> + mk_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 -> + mk_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 -> + mk_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 -> + mk_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 -> + mk_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 -> + mk_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) + | _, _ -> + default + + + (** underapproximation of min b1 b2 *) + let min_l b1 b2 = lb ~default:MInf b1 b2 + + (** overapproximation of min b1 b2 *) + let min_u b1 b2 = + lb + ~default: + (* When the result is not representable, our best effort is to return the first argument. Any other deterministic heuristics would work too. *) + b1 b1 b2 + + + let ub : default:t -> t -> t -> t = + fun ~default x y -> + if le x y then y + else if le y x then x + else + match (x, y) with + | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_zero x1 && SymLinear.is_one_symbol x2 -> + mk_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 -> + mk_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 -> + mk_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 -> + mk_MinMax (c1, Minus, Min, c1 - c2, SymLinear.get_mone_symbol x1) + | _, _ -> + default + + + let max_u : t -> t -> t = ub ~default:PInf + + let widen_l : t -> t -> t = + fun x y -> + match (x, y) with + | PInf, _ | _, PInf -> + L.(die InternalError) "Lower bound cannot be +oo." + | MinMax (n1, Plus, Max, _, s1), Linear (n2, s2) + when Int.equal n1 n2 && SymLinear.is_one_symbol_of s1 s2 -> + y + | MinMax (n1, Minus, Min, _, s1), Linear (n2, s2) + when Int.equal n1 n2 && SymLinear.is_mone_symbol_of s1 s2 -> + y + | _ -> + if le x y then x else MInf + + + let widen_u : t -> t -> t = + fun x y -> + match (x, y) with + | MInf, _ | _, MInf -> + L.(die InternalError) "Upper bound cannot be -oo." + | MinMax (n1, Plus, Min, _, s1), Linear (n2, s2) + when Int.equal n1 n2 && SymLinear.is_one_symbol_of s1 s2 -> + y + | MinMax (n1, Minus, Max, _, s1), Linear (n2, s2) + when Int.equal n1 n2 && SymLinear.is_mone_symbol_of s1 s2 -> + y + | _ -> + if le y x then x else PInf + + + let zero : t = Linear (0, SymLinear.zero) + + let one : t = Linear (1, SymLinear.zero) + + let mone : t = Linear (-1, SymLinear.zero) + + let is_some_const : int -> t -> bool = + fun c x -> match x with Linear (c', y) -> Int.equal c c' && SymLinear.is_zero y | _ -> false + + + let is_zero : t -> bool = is_some_const 0 + + let is_const : t -> int option = + fun x -> match x with Linear (c, y) when SymLinear.is_zero y -> Some c | _ -> None + + + let plus_common : f:(t -> t -> t) -> t -> t -> t = + fun ~f x y -> + match (x, y) with + | _, _ when is_zero x -> + y + | _, _ when is_zero y -> + x + | Linear (c1, x1), Linear (c2, x2) -> + Linear (c1 + c2, SymLinear.plus x1 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 -> + mk_MinMax (c1 + c2, sign, min_max, d1, x1) + | _ -> + f x y + + + let plus_l : t -> t -> t = + plus_common ~f:(fun x y -> + match (x, y) with + | 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 ) + + + let plus_u : t -> t -> t = + plus_common ~f:(fun x y -> + match (x, y) with + | 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 ) + + + let plus = function Symb.BoundEnd.LowerBound -> plus_l | Symb.BoundEnd.UpperBound -> plus_u + + let mult_const : Symb.BoundEnd.t -> NonZeroInt.t -> t -> t = + fun bound_end n x -> + match x with + | MInf -> + if NonZeroInt.is_positive n then MInf else PInf + | PInf -> + if NonZeroInt.is_positive n then PInf else MInf + | Linear (c, x') -> + Linear (c * (n :> int), SymLinear.mult_const n x') + | MinMax _ -> + let int_bound = + let bound_end' = + if NonZeroInt.is_positive n then bound_end else Symb.BoundEnd.neg bound_end + in + int_of_minmax bound_end' x + in + match int_bound with Some i -> of_int (i * (n :> int)) | None -> of_bound_end bound_end + + + let mult_const_l = mult_const Symb.BoundEnd.LowerBound + + let mult_const_u = mult_const Symb.BoundEnd.UpperBound + + let neg : t -> t = function + | MInf -> + PInf + | PInf -> + MInf + | Linear (c, x) -> + Linear (-c, SymLinear.neg x) + | MinMax (c, sign, min_max, d, x) -> + mk_MinMax (-c, Sign.neg sign, min_max, d, x) + + + let div_const : t -> NonZeroInt.t -> t option = + fun x n -> + match x with + | MInf -> + Some (if NonZeroInt.is_positive n then MInf else PInf) + | PInf -> + Some (if NonZeroInt.is_positive n then PInf else MInf) + | Linear (c, x') when NonZeroInt.is_multiple c n -> ( + match SymLinear.exact_div_const_exn x' n with + | x'' -> + Some (Linear (c / (n :> int), x'')) + | exception NonZeroInt.DivisionNotExact -> + None ) + | _ -> + None + + + let get_symbols : t -> Symb.Symbol.t list = function + | MInf | PInf -> + [] + | Linear (_, se) -> + SymLinear.get_symbols se + | MinMax (_, _, _, _, s) -> + [s] + + + let are_similar b1 b2 = + match (b1, b2) with + | MInf, MInf -> + true + | PInf, PInf -> + true + | (Linear _ | MinMax _), (Linear _ | MinMax _) -> + true + | _ -> + false + + + let is_not_infty : t -> bool = function MInf | PInf -> false | _ -> true + + let lift1 : (t -> t) -> t bottom_lifted -> t bottom_lifted = + fun f x -> match x with Bottom -> Bottom | NonBottom x -> NonBottom (f x) + + + let lift2 : (t -> t -> t) -> t bottom_lifted -> t bottom_lifted -> t bottom_lifted = + fun f x y -> + match (x, y) with + | Bottom, _ | _, Bottom -> + Bottom + | NonBottom x, NonBottom y -> + NonBottom (f x y) + + + (** Substitutes ALL symbols in [x] with respect to [map]. Throws [Symbol_not_found] if a symbol in [x] can't be found in [map]. Under/over-Approximate as good as possible according to [subst_pos]. *) + let subst_exn + : subst_pos:Symb.BoundEnd.t -> t -> t bottom_lifted Symb.SymbolMap.t -> t bottom_lifted = + fun ~subst_pos x map -> + let get_exn s = + match Symb.SymbolMap.find s map with + | NonBottom x when Symb.Symbol.is_unsigned s -> + NonBottom (ub ~default:x zero x) + | x -> + x + in + let get_mult_const s coeff = + try + if NonZeroInt.is_one coeff then get_exn s + else if NonZeroInt.is_minus_one coeff then get_exn s |> lift1 neg + else + match Symb.SymbolMap.find s map with + | Bottom -> + Bottom + | NonBottom x -> + let x = mult_const subst_pos coeff x in + if Symb.Symbol.is_unsigned s then NonBottom (ub ~default:x zero x) else NonBottom x + with Caml.Not_found -> + (* For unsigned symbols, we can over/under-approximate with zero depending on [subst_pos] and the sign of the coefficient. *) + match (Symb.Symbol.is_unsigned s, subst_pos, NonZeroInt.is_positive coeff) with + | true, Symb.BoundEnd.LowerBound, true | true, Symb.BoundEnd.UpperBound, false -> + NonBottom zero + | _ -> + raise (Symbol_not_found s) + in + match x with + | MInf | PInf -> + NonBottom x + | Linear (c, se) -> + SymLinear.fold se ~init:(NonBottom (of_int c)) ~f:(fun acc s coeff -> + lift2 (plus subst_pos) acc (get_mult_const s coeff) ) + | MinMax (c, sign, min_max, d, s) -> + match get_exn s with + | Bottom -> + Bottom + | exception Caml.Not_found -> ( + match int_of_minmax subst_pos x with + | Some i -> + NonBottom (of_int i) + | None -> + raise (Symbol_not_found s) ) + | NonBottom x' -> + let res = + match (sign, min_max, x') with + | Plus, Min, MInf | Minus, Max, PInf -> + MInf + | Plus, Max, PInf | Minus, Min, MInf -> + PInf + | sign, Min, PInf | sign, Max, MInf -> + of_int (Sign.eval_int sign c d) + | _, _, Linear (c2, se) + -> ( + if SymLinear.is_zero se then + of_int (Sign.eval_int sign c (MinMax.eval_int min_max d c2)) + else if SymLinear.is_one_symbol se then + mk_MinMax + (Sign.eval_int sign c c2, sign, min_max, d - c2, SymLinear.get_one_symbol se) + else if SymLinear.is_mone_symbol se then + mk_MinMax + ( Sign.eval_int sign c c2 + , Sign.neg sign + , MinMax.neg min_max + , c2 - d + , SymLinear.get_mone_symbol se ) + else + match int_of_minmax subst_pos x with + | Some i -> + of_int i + | None -> + of_bound_end subst_pos ) + | _, _, MinMax (c2, sign2, min_max2, d2, s2) -> + match (min_max, sign2, min_max2) with + | Min, Plus, Min | Max, Plus, Max -> + let c' = Sign.eval_int sign c c2 in + let d' = MinMax.eval_int min_max (d - c2) d2 in + mk_MinMax (c', sign, min_max, d', s2) + | Min, Minus, Max | Max, Minus, Min -> + let c' = Sign.eval_int sign c c2 in + let d' = MinMax.eval_int min_max2 (c2 - d) d2 in + mk_MinMax (c', Sign.neg sign, min_max2, d', s2) + | _ -> + let bound_end = + match sign with Plus -> subst_pos | Minus -> Symb.BoundEnd.neg subst_pos + in + of_int + (Sign.eval_int sign c + (MinMax.eval_int min_max d + (int_of_minmax bound_end x' |> Option.value ~default:d))) + in + NonBottom res + + + let subst_lb_exn x map = subst_exn ~subst_pos:Symb.BoundEnd.LowerBound x map + + let subst_ub_exn x map = subst_exn ~subst_pos:Symb.BoundEnd.UpperBound x map + + let simplify_bound_ends_from_paths x = + match x with + | MInf | PInf | MinMax _ -> + x + | Linear (c, se) -> + let se' = SymLinear.simplify_bound_ends_from_paths se in + if phys_equal se se' then x else Linear (c, se') +end + +type ('c, 's) valclass = Constant of 'c | Symbolic of 's | ValTop + +(** A NonNegativeBound is a Bound that is either non-negative or symbolic but will be evaluated to a non-negative value once instantiated *) +module NonNegativeBound = struct + type t = Bound.t [@@deriving compare] + + let zero = Bound.zero + + let of_bound b = if Bound.le b Bound.zero then Bound.zero else b + + let classify = function + | Bound.PInf -> + ValTop + | Bound.MInf -> + assert false + | b -> + match Bound.is_const b with + | None -> + Symbolic b + | Some c -> + Constant (NonNegativeInt.of_int_exn c) +end diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli new file mode 100644 index 000000000..418f1f122 --- /dev/null +++ b/infer/src/bufferoverrun/bounds.mli @@ -0,0 +1,137 @@ +(* + * Copyright (c) 2017-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd +module F = Format + +exception Symbol_not_found of Symb.Symbol.t + +exception Not_One_Symbol + +module SymLinear : sig + module M = Symb.SymbolMap + + type t = Ints.NonZeroInt.t M.t + + val make : + unsigned:bool -> Typ.Procname.t -> Symb.SymbolTable.t -> Symb.SymbolPath.t -> Counter.t + -> t * t + + val eq : t -> t -> bool + + val is_zero : t -> bool +end + +module Bound : sig + type sign = Plus | Minus + + type min_max = Min | Max + + type t = + | MInf + | Linear of int * SymLinear.t + | MinMax of int * sign * min_max * int * Symb.Symbol.t + | PInf + + val compare : t -> t -> int + + val pp : F.formatter -> t -> unit + + val of_int : int -> t + + val minus_one : t + + val _255 : t + + val of_sym : SymLinear.t -> t + + val is_symbolic : t -> bool + + val get_one_symbol : t -> Symb.Symbol.t + + val get_mone_symbol : t -> Symb.Symbol.t + + val is_one_symbol : t -> bool + + val is_mone_symbol : t -> bool + + val mk_MinMax : int * sign * min_max * int * Symb.Symbol.t -> t + + val int_lb : t -> int sexp_option + + val int_ub : t -> int sexp_option + + val le : t -> t -> bool + + val lt : t -> t -> bool + + val gt : t -> t -> bool + + val eq : t -> t -> bool + + val xcompare : t PartialOrder.xcompare + + val min_l : t -> t -> t + + val min_u : t -> t -> t + + val max_u : t -> t -> t + + val widen_l : t -> t -> t + + val widen_u : t -> t -> t + + val zero : t + + val one : t + + val mone : t + + val is_zero : t -> bool + + val is_const : t -> int sexp_option + + val plus_l : t -> t -> t + + val plus_u : t -> t -> t + + val mult_const_l : Ints.NonZeroInt.t -> t -> t + + val mult_const_u : Ints.NonZeroInt.t -> t -> t + + val neg : t -> t + + val div_const : t -> Ints.NonZeroInt.t -> t sexp_option + + val get_symbols : t -> Symb.Symbol.t list + + val are_similar : t -> t -> bool + + val is_not_infty : t -> bool + + val subst_lb_exn : + t -> t AbstractDomain.Types.bottom_lifted Symb.SymbolMap.t + -> t AbstractDomain.Types.bottom_lifted + + val subst_ub_exn : + t -> t AbstractDomain.Types.bottom_lifted Symb.SymbolMap.t + -> t AbstractDomain.Types.bottom_lifted + + val simplify_bound_ends_from_paths : t -> t +end + +type ('c, 's) valclass = Constant of 'c | Symbolic of 's | ValTop + +module NonNegativeBound : sig + type t = Bound.t + + val zero : t + + val of_bound : t -> t + + val classify : t -> (Ints.NonNegativeInt.t, t) valclass +end diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index d7cde0b3c..10000675f 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -13,6 +13,7 @@ module ItvPure = Itv.ItvPure module Relation = BufferOverrunDomainRelation module MF = MarkupFormatter module ValTraceSet = BufferOverrunTrace.Set +module Bound = Bounds.Bound type checked_condition = {report_issue_type: IssueType.t option; propagate: bool} @@ -70,13 +71,13 @@ module AllocSizeCondition = struct match ItvPure.xcompare ~lhs:length ~rhs:ItvPure.mone with | `Equal | `LeftSmallerThanRight | `RightSubsumesLeft -> {report_issue_type= Some IssueType.inferbo_alloc_is_negative; propagate= false} - | `LeftSubsumesRight when Itv.Bound.is_not_infty (ItvPure.lb length) -> + | `LeftSubsumesRight when Bound.is_not_infty (ItvPure.lb length) -> {report_issue_type= Some IssueType.inferbo_alloc_may_be_negative; propagate= true} | cmp_mone -> match ItvPure.xcompare ~lhs:length ~rhs:itv_big with | `Equal | `RightSmallerThanLeft | `RightSubsumesLeft -> {report_issue_type= Some IssueType.inferbo_alloc_is_big; propagate= false} - | `LeftSubsumesRight when Itv.Bound.is_not_infty (ItvPure.ub length) -> + | `LeftSubsumesRight when Bound.is_not_infty (ItvPure.ub length) -> {report_issue_type= Some IssueType.inferbo_alloc_may_be_big; propagate= true} | cmp_big -> let propagate = @@ -196,27 +197,27 @@ module ArrayAccessCondition = struct (not (ItvPure.is_finite c.idx) || not (ItvPure.is_finite c.size)) && (* except the following cases *) not - ( Itv.Bound.is_not_infty (ItvPure.lb c.idx) + ( Bound.is_not_infty (ItvPure.lb c.idx) && (* idx non-infty lb < 0 *) - Itv.Bound.lt (ItvPure.lb c.idx) Itv.Bound.zero - || Itv.Bound.is_not_infty (ItvPure.lb c.idx) + Bound.lt (ItvPure.lb c.idx) Bound.zero + || Bound.is_not_infty (ItvPure.lb c.idx) && (* idx non-infty lb > size lb *) - Itv.Bound.gt (ItvPure.lb c.idx) (ItvPure.lb c.size) - || Itv.Bound.is_not_infty (ItvPure.lb c.idx) + Bound.gt (ItvPure.lb c.idx) (ItvPure.lb c.size) + || Bound.is_not_infty (ItvPure.lb c.idx) && (* idx non-infty lb > size ub *) - Itv.Bound.gt (ItvPure.lb c.idx) (ItvPure.ub c.size) - || Itv.Bound.is_not_infty (ItvPure.ub c.idx) + Bound.gt (ItvPure.lb c.idx) (ItvPure.ub c.size) + || Bound.is_not_infty (ItvPure.ub c.idx) && (* idx non-infty ub > size lb *) - Itv.Bound.gt (ItvPure.ub c.idx) (ItvPure.lb c.size) - || Itv.Bound.is_not_infty (ItvPure.ub c.idx) + Bound.gt (ItvPure.ub c.idx) (ItvPure.lb c.size) + || Bound.is_not_infty (ItvPure.ub c.idx) && (* idx non-infty ub > size ub *) - Itv.Bound.gt (ItvPure.ub c.idx) (ItvPure.ub c.size) ) + Bound.gt (ItvPure.ub c.idx) (ItvPure.ub c.size) ) (* check buffer overrun and return its confidence *) let check : is_arraylist_add:bool -> t -> checked_condition = fun ~is_arraylist_add c -> - (* idx = [il, iu], size = [sl, su], + (* idx = [il, iu], size = [sl, su], For arrays : we want to check that 0 <= idx < size For adding into arraylists: we want to check that 0 <= idx <= size *) let c' = set_size_pos c in @@ -238,13 +239,11 @@ module ArrayAccessCondition = struct {report_issue_type= Some IssueType.buffer_overrun_l1; propagate= false} (* su <= iu < +oo, most probably an error *) else if - Itv.Bound.is_not_infty (ItvPure.ub c.idx) - && Itv.Bound.le (ItvPure.ub c.size) (ItvPure.ub c.idx) + Bound.is_not_infty (ItvPure.ub c.idx) && Bound.le (ItvPure.ub c.size) (ItvPure.ub c.idx) then {report_issue_type= Some IssueType.buffer_overrun_l2; propagate= false} (* symbolic il >= sl, probably an error *) else if - Itv.Bound.is_symbolic (ItvPure.lb c.idx) - && Itv.Bound.le (ItvPure.lb c'.size) (ItvPure.lb c.idx) + Bound.is_symbolic (ItvPure.lb c.idx) && Bound.le (ItvPure.lb c'.size) (ItvPure.lb c.idx) then {report_issue_type= Some IssueType.buffer_overrun_s2; propagate= true} else (* other symbolic bounds are probably too noisy *) diff --git a/infer/src/bufferoverrun/counter.ml b/infer/src/bufferoverrun/counter.ml new file mode 100644 index 000000000..92d3513d8 --- /dev/null +++ b/infer/src/bufferoverrun/counter.ml @@ -0,0 +1,24 @@ +(* + * Copyright (c) 2017-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd +open! AbstractDomain.Types + +type t = unit -> int + +let make : int -> t = + fun init -> + let num_ref = ref init in + let get_num () = + let v = !num_ref in + num_ref := v + 1 ; + v + in + get_num + + +let next : t -> int = fun counter -> counter () diff --git a/infer/src/bufferoverrun/counter.mli b/infer/src/bufferoverrun/counter.mli new file mode 100644 index 000000000..7280f8e1a --- /dev/null +++ b/infer/src/bufferoverrun/counter.mli @@ -0,0 +1,15 @@ +(* + * Copyright (c) 2017-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd +open! AbstractDomain.Types + +type t + +val make : int -> t + +val next : t -> int diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 71b754804..212cd6dc9 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -12,23 +12,8 @@ open! IStd open! AbstractDomain.Types module F = Format module L = Logging - -module Counter = struct - type t = unit -> int - - let make : int -> t = - fun init -> - let num_ref = ref init in - let get_num () = - let v = !num_ref in - num_ref := v + 1 ; - v - in - get_num - - - let next : t -> int = fun counter -> counter () -end +module Bound = Bounds.Bound +module Counter = Counter module Boolean = struct type t = Bottom | False | True | Top [@@deriving compare] @@ -44,917 +29,11 @@ module Boolean = struct let is_true = function True -> true | _ -> false end -module BoundEnd = struct - type t = LowerBound | UpperBound [@@deriving compare] - - let neg = function LowerBound -> UpperBound | UpperBound -> LowerBound - - let to_string = function LowerBound -> "lb" | UpperBound -> "ub" -end - -module SymbolPath = struct - type partial = Pvar of Pvar.t | Index of partial | Field of Typ.Fieldname.t * partial - [@@deriving compare] - - type t = Normal of partial | Offset of partial | Length of partial [@@deriving compare] - - let equal = [%compare.equal : t] - - let of_pvar pvar = Pvar pvar - - let field p fn = Field (fn, p) - - let index p = Index p - - let normal p = Normal p - - let offset p = Offset p - - let length p = Length p - - let rec pp_partial fmt = function - | Pvar pvar -> - Pvar.pp_value fmt pvar - | Index p -> - F.fprintf fmt "%a[*]" pp_partial p - | Field (fn, p) -> - F.fprintf fmt "%a.%s" pp_partial p (Typ.Fieldname.to_flat_string fn) - - - let pp fmt = function - | Normal p -> - pp_partial fmt p - | Offset p -> - F.fprintf fmt "%a.offset" pp_partial p - | Length p -> - F.fprintf fmt "%a.length" pp_partial p -end - -module Symbol = struct - type t = - {id: int; pname: Typ.Procname.t; unsigned: bool; path: SymbolPath.t; bound_end: BoundEnd.t} - - let compare s1 s2 = - (* Symbols only make sense within a given function, so shouldn't be compared across function boundaries. *) - assert (phys_equal s1.pname s2.pname) ; - Int.compare s1.id s2.id - - - let equal = [%compare.equal : t] - - let paths_equal s1 s2 = SymbolPath.equal s1.path s2.path - - let make : unsigned:bool -> Typ.Procname.t -> SymbolPath.t -> BoundEnd.t -> int -> t = - fun ~unsigned pname path bound_end id -> {id; pname; unsigned; path; bound_end} - - - let pp : F.formatter -> t -> unit = - fun fmt {pname; id; unsigned; path; bound_end} -> - F.fprintf fmt "%a.%s" SymbolPath.pp path (BoundEnd.to_string bound_end) ; - if Config.bo_debug > 1 then - let symbol_name = if unsigned then 'u' else 's' in - F.fprintf fmt "(%s-%c$%d)" (Typ.Procname.to_string pname) symbol_name id - - - let is_unsigned : t -> bool = fun x -> x.unsigned -end - -module SymbolTable = struct - module M = PrettyPrintable.MakePPMap (SymbolPath) - - type summary_t = (Symbol.t * Symbol.t) M.t - - let find_opt = M.find_opt - - let pp = M.pp ~pp_value:(fun fmt (lb, ub) -> F.fprintf fmt "[%a, %a]" Symbol.pp lb Symbol.pp ub) - - type t = summary_t ref - - let empty () = ref M.empty - - let lookup ~unsigned pname path symbol_table new_sym_num = - match M.find_opt path !symbol_table with - | Some s -> - s - | None -> - let s = - ( Symbol.make ~unsigned pname path LowerBound (Counter.next new_sym_num) - , Symbol.make ~unsigned pname path UpperBound (Counter.next new_sym_num) ) - in - symbol_table := M.add path s !symbol_table ; - s - - - let summary_of x = !x -end - -exception Symbol_not_found of Symbol.t - -module SymbolMap = struct - include PrettyPrintable.MakePPMap (Symbol) - - let for_all2 : f:(key -> 'a option -> 'b option -> bool) -> 'a t -> 'b t -> bool = - fun ~f x y -> - match merge (fun k x y -> if f k x y then None else raise Exit) x y with - | _ -> - true - | exception Exit -> - false - - - let is_singleton : 'a t -> (key * 'a) option = - fun m -> - if is_empty m then None - else - let (kmin, _) as binding = min_binding m in - let kmax, _ = max_binding m in - if Symbol.equal kmin kmax then Some binding else None -end - open Ints - -exception Not_one_symbol - -module SymLinear = struct - module M = SymbolMap - - (** - Map from symbols to integer coefficients. - { x -> 2, y -> 5 } represents the value 2 * x + 5 * y - *) - type t = NonZeroInt.t M.t [@@deriving compare] - - let empty : t = M.empty - - let is_empty : t -> bool = fun x -> M.is_empty x - - let singleton_one : Symbol.t -> t = fun s -> M.singleton s NonZeroInt.one - - let singleton_minus_one : Symbol.t -> t = fun s -> M.singleton s NonZeroInt.minus_one - - let is_le_zero : t -> bool = - fun x -> M.for_all (fun s v -> Symbol.is_unsigned s && NonZeroInt.is_negative v) x - - - let is_ge_zero : t -> bool = - fun x -> M.for_all (fun s v -> Symbol.is_unsigned s && NonZeroInt.is_positive v) x - - - let le : t -> t -> bool = - fun x y -> - let le_one_pair s v1_opt v2_opt = - let v1 = NonZeroInt.opt_to_int v1_opt in - let v2 = NonZeroInt.opt_to_int v2_opt in - Int.equal v1 v2 || (Symbol.is_unsigned s && v1 <= v2) - in - M.for_all2 ~f:le_one_pair x y - - - let make : unsigned:bool -> Typ.Procname.t -> SymbolTable.t -> SymbolPath.t -> Counter.t -> t * t = - fun ~unsigned pname symbol_table path new_sym_num -> - let lb, ub = SymbolTable.lookup ~unsigned pname path symbol_table new_sym_num in - (singleton_one lb, singleton_one ub) - - - let eq : t -> t -> bool = - fun x y -> - let eq_pair _ (coeff1: NonZeroInt.t option) (coeff2: NonZeroInt.t option) = - [%compare.equal : int option] (coeff1 :> int option) (coeff2 :> int option) - in - M.for_all2 ~f:eq_pair x y - - - let pp1 : F.formatter -> Symbol.t * NonZeroInt.t -> unit = - fun fmt (s, c) -> - let c = (c :> int) in - if Int.equal c 1 then Symbol.pp fmt s - else if Int.equal c (-1) then F.fprintf fmt "-%a" Symbol.pp s - else F.fprintf fmt "%dx%a" c Symbol.pp s - - - let pp : F.formatter -> t -> unit = - fun fmt x -> - if M.is_empty x then F.pp_print_string fmt "empty" - else Pp.seq ~sep:" + " pp1 fmt (M.bindings x) - - - let zero : t = M.empty - - let is_zero : t -> bool = M.is_empty - - let neg : t -> t = fun x -> M.map NonZeroInt.( ~- ) x - - let plus : t -> t -> t = - fun x y -> - let plus_coeff _ c1 c2 = NonZeroInt.plus c1 c2 in - M.union plus_coeff x y - - - let mult_const : NonZeroInt.t -> t -> t = fun n x -> M.map (NonZeroInt.( * ) n) x - - let exact_div_const_exn : t -> NonZeroInt.t -> t = - fun x n -> M.map (fun c -> NonZeroInt.exact_div_exn c n) x - - - (* Returns a symbol when the map contains only one symbol s with a - given coefficient. *) - let one_symbol_of_coeff : NonZeroInt.t -> t -> Symbol.t option = - fun coeff x -> - match M.is_singleton x with - | Some (k, v) when Int.equal (v :> int) (coeff :> int) -> - Some k - | _ -> - None - - - let fold m ~init ~f = - let f s coeff acc = f acc s coeff in - M.fold f m init - - - let get_one_symbol_opt : t -> Symbol.t option = one_symbol_of_coeff NonZeroInt.one - - let get_mone_symbol_opt : t -> Symbol.t option = one_symbol_of_coeff NonZeroInt.minus_one - - 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 is_one_symbol_of : Symbol.t -> t -> bool = - fun s x -> - Option.value_map (get_one_symbol_opt x) ~default:false ~f:(fun s' -> Symbol.equal s s') - - - let is_mone_symbol_of : Symbol.t -> t -> bool = - fun s x -> - Option.value_map (get_mone_symbol_opt x) ~default:false ~f:(fun s' -> Symbol.equal s s') - - - 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 - - (** When two following symbols are from the same path, simplify what would lead to a zero sum. E.g. 2 * x.lb - x.ub = x.lb *) - let simplify_bound_ends_from_paths : t -> t = - fun x -> - let f (prev_opt, to_add) symb coeff = - match prev_opt with - | Some (prev_coeff, prev_symb) - when Symbol.paths_equal prev_symb symb - && NonZeroInt.is_positive coeff <> NonZeroInt.is_positive prev_coeff -> - let add_coeff = - (if NonZeroInt.is_positive coeff then NonZeroInt.max else NonZeroInt.min) - prev_coeff (NonZeroInt.( ~- ) coeff) - in - let to_add = - to_add |> M.add symb add_coeff |> M.add prev_symb (NonZeroInt.( ~- ) add_coeff) - in - (None, to_add) - | _ -> - (Some (coeff, symb), to_add) - in - let _, to_add = fold x ~init:(None, zero) ~f in - plus x to_add -end - -module Bound = struct - type sign = Plus | Minus [@@deriving compare] - - module Sign = struct - type t = sign [@@deriving compare] - - let equal = [%compare.equal : t] - - let neg = function Plus -> Minus | Minus -> Plus - - let eval_int x i1 i2 = match x with Plus -> i1 + i2 | Minus -> i1 - i2 - - let pp ~need_plus : F.formatter -> t -> unit = - fun fmt -> function - | Plus -> - if need_plus then F.pp_print_char fmt '+' - | Minus -> - F.pp_print_char fmt '-' - end - - type min_max = Min | Max [@@deriving compare] - - module MinMax = struct - type t = min_max [@@deriving compare] - - let equal = [%compare.equal : t] - - let neg = function Min -> Max | Max -> Min - - let eval_int x i1 i2 = match x with Min -> min i1 i2 | Max -> max i1 i2 - - let pp : F.formatter -> t -> unit = - fun fmt -> function Min -> F.pp_print_string fmt "min" | Max -> F.pp_print_string fmt "max" - end - - (* 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 int * Sign.t * MinMax.t * int * Symbol.t - | PInf - [@@deriving compare] - - let pp : F.formatter -> t -> unit = - fun fmt -> function - | MInf -> - F.pp_print_string fmt "-oo" - | PInf -> - F.pp_print_string fmt "+oo" - | Linear (c, x) -> - if SymLinear.is_zero x then F.pp_print_int fmt c - else if Int.equal c 0 then SymLinear.pp fmt x - else F.fprintf fmt "%a + %d" SymLinear.pp x c - | MinMax (c, sign, m, d, x) -> - if Int.equal c 0 then (Sign.pp ~need_plus:false) fmt sign - else F.fprintf fmt "%d%a" c (Sign.pp ~need_plus:true) sign ; - F.fprintf fmt "%a(%d, %a)" MinMax.pp m d Symbol.pp x - - - let of_bound_end = function BoundEnd.LowerBound -> MInf | BoundEnd.UpperBound -> PInf - - let of_int : int -> t = fun n -> Linear (n, SymLinear.empty) - - let minus_one = of_int (-1) - - let _255 = of_int 255 - - let of_sym : SymLinear.t -> t = fun s -> Linear (0, s) - - let is_symbolic : t -> bool = function - | MInf | PInf -> - false - | Linear (_, se) -> - not (SymLinear.is_empty se) - | MinMax _ -> - true - - - let lift_symlinear : (SymLinear.t -> 'a option) -> t -> 'a option = - fun f -> function Linear (0, se) -> f se | _ -> None - - - let get_one_symbol_opt : t -> Symbol.t option = lift_symlinear SymLinear.get_one_symbol_opt - - let get_mone_symbol_opt : t -> Symbol.t option = lift_symlinear 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 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 mk_MinMax (c, sign, m, d, s) = - if Symbol.is_unsigned s && d <= 0 then - match m with - | Min -> - of_int (Sign.eval_int sign c d) - | Max -> - match sign with - | Plus -> - Linear (c, SymLinear.singleton_one s) - | Minus -> - Linear (c, SymLinear.singleton_minus_one s) - else MinMax (c, sign, m, d, s) - - - let int_ub_of_minmax = function - | MinMax (c, Plus, Min, d, _) -> - Some (c + d) - | MinMax (c, Minus, Max, d, s) when Symbol.is_unsigned s -> - Some (min c (c - d)) - | MinMax (c, Minus, Max, d, _) -> - Some (c - d) - | MinMax _ -> - None - | MInf | PInf | Linear _ -> - assert false - - - let int_lb_of_minmax = function - | MinMax (c, Plus, Max, d, s) when Symbol.is_unsigned s -> - Some (max c (c + d)) - | MinMax (c, Plus, Max, d, _) -> - Some (c + d) - | MinMax (c, Minus, Min, d, _) -> - Some (c - d) - | MinMax _ -> - None - | MInf | PInf | Linear _ -> - assert false - - - let int_of_minmax = function - | BoundEnd.LowerBound -> - int_lb_of_minmax - | BoundEnd.UpperBound -> - int_ub_of_minmax - - - 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)) - | MinMax (c, Minus, Max, _, x) -> - Some (Linear (c, SymLinear.singleton_minus_one x)) - | MinMax _ -> - None - | MInf | PInf | Linear _ -> - assert false - - - let linear_lb_of_minmax = function - | MinMax (c, Plus, Max, _, x) -> - Some (Linear (c, SymLinear.singleton_one x)) - | MinMax (c, Minus, Min, _, x) -> - Some (Linear (c, SymLinear.singleton_minus_one x)) - | MinMax _ -> - None - | MInf | PInf | Linear _ -> - 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 -> - match (x, y) with - | MInf, _ | _, PInf -> - true - | _, MInf | PInf, _ -> - false - | Linear (c0, x0), Linear (c1, x1) -> - c0 <= c1 && SymLinear.le x0 x1 - | MinMax (c1, sign1, m1, d1, x1), MinMax (c2, sign2, m2, d2, x2) - when Sign.equal sign1 sign2 && MinMax.equal m1 m2 -> - c1 <= c2 && Int.equal d1 d2 && Symbol.equal 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.equal x1 x2 - | MinMax _, Linear (c, se) -> - (SymLinear.is_ge_zero se && le_opt1 Int.( <= ) (int_ub_of_minmax x) c) - || le_opt1 le (linear_ub_of_minmax x) y - | Linear (c, se), MinMax _ -> - (SymLinear.is_le_zero se && le_opt2 Int.( <= ) c (int_lb_of_minmax y)) - || le_opt2 le x (linear_lb_of_minmax y) - | _, _ -> - false - - - let lt : t -> t -> bool = - fun x y -> - match (x, y) with - | MInf, Linear _ | MInf, MinMax _ | MInf, PInf | Linear _, PInf | MinMax _, PInf -> - true - | Linear (c, x), _ -> - le (Linear (c + 1, x)) y - | MinMax (c, sign, min_max, d, x), _ -> - le (mk_MinMax (c + 1, sign, min_max, d, x)) y - | _, _ -> - false - - - let gt : t -> t -> bool = fun x y -> lt y x - - let eq : t -> t -> bool = fun x y -> le x y && le y x - - let xcompare = PartialOrder.of_le ~le - - let remove_max_int : t -> t = - fun x -> - match x with - | MinMax (c, Plus, Max, _, s) -> - Linear (c, SymLinear.singleton_one s) - | MinMax (c, Minus, Min, _, s) -> - Linear (c, SymLinear.singleton_minus_one s) - | _ -> - x - - - let rec lb : default:t -> t -> t -> t = - fun ~default x y -> - if le x y then x - else if le y x then y - else - match (x, y) with - | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_zero x1 && SymLinear.is_one_symbol x2 -> - mk_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 -> - mk_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 -> - mk_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 -> - mk_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 -> - mk_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 -> - mk_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 -> - mk_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 -> - mk_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) - | _, _ -> - default - - - (** underapproximation of min b1 b2 *) - let min_l b1 b2 = lb ~default:MInf b1 b2 - - (** overapproximation of min b1 b2 *) - let min_u b1 b2 = - lb - ~default: - (* When the result is not representable, our best effort is to return the first argument. Any other deterministic heuristics would work too. *) - b1 b1 b2 - - - let ub : default:t -> t -> t -> t = - fun ~default x y -> - if le x y then y - else if le y x then x - else - match (x, y) with - | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_zero x1 && SymLinear.is_one_symbol x2 -> - mk_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 -> - mk_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 -> - mk_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 -> - mk_MinMax (c1, Minus, Min, c1 - c2, SymLinear.get_mone_symbol x1) - | _, _ -> - default - - - let max_u : t -> t -> t = ub ~default:PInf - - let widen_l : t -> t -> t = - fun x y -> - match (x, y) with - | PInf, _ | _, PInf -> - L.(die InternalError) "Lower bound cannot be +oo." - | MinMax (n1, Plus, Max, _, s1), Linear (n2, s2) - when Int.equal n1 n2 && SymLinear.is_one_symbol_of s1 s2 -> - y - | MinMax (n1, Minus, Min, _, s1), Linear (n2, s2) - when Int.equal n1 n2 && SymLinear.is_mone_symbol_of s1 s2 -> - y - | _ -> - if le x y then x else MInf - - - let widen_u : t -> t -> t = - fun x y -> - match (x, y) with - | MInf, _ | _, MInf -> - L.(die InternalError) "Upper bound cannot be -oo." - | MinMax (n1, Plus, Min, _, s1), Linear (n2, s2) - when Int.equal n1 n2 && SymLinear.is_one_symbol_of s1 s2 -> - y - | MinMax (n1, Minus, Max, _, s1), Linear (n2, s2) - when Int.equal n1 n2 && SymLinear.is_mone_symbol_of s1 s2 -> - y - | _ -> - if le y x then x else PInf - - - let zero : t = Linear (0, SymLinear.zero) - - let one : t = Linear (1, SymLinear.zero) - - let mone : t = Linear (-1, SymLinear.zero) - - let is_some_const : int -> t -> bool = - fun c x -> match x with Linear (c', y) -> Int.equal c c' && SymLinear.is_zero y | _ -> false - - - let is_zero : t -> bool = is_some_const 0 - - let is_const : t -> int option = - fun x -> match x with Linear (c, y) when SymLinear.is_zero y -> Some c | _ -> None - - - let plus_common : f:(t -> t -> t) -> t -> t -> t = - fun ~f x y -> - match (x, y) with - | _, _ when is_zero x -> - y - | _, _ when is_zero y -> - x - | Linear (c1, x1), Linear (c2, x2) -> - Linear (c1 + c2, SymLinear.plus x1 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 -> - mk_MinMax (c1 + c2, sign, min_max, d1, x1) - | _ -> - f x y - - - let plus_l : t -> t -> t = - plus_common ~f:(fun x y -> - match (x, y) with - | 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 ) - - - let plus_u : t -> t -> t = - plus_common ~f:(fun x y -> - match (x, y) with - | 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 ) - - - let plus = function BoundEnd.LowerBound -> plus_l | BoundEnd.UpperBound -> plus_u - - let mult_const : BoundEnd.t -> NonZeroInt.t -> t -> t = - fun bound_end n x -> - match x with - | MInf -> - if NonZeroInt.is_positive n then MInf else PInf - | PInf -> - if NonZeroInt.is_positive n then PInf else MInf - | Linear (c, x') -> - Linear (c * (n :> int), SymLinear.mult_const n x') - | MinMax _ -> - let int_bound = - let bound_end' = - if NonZeroInt.is_positive n then bound_end else BoundEnd.neg bound_end - in - int_of_minmax bound_end' x - in - match int_bound with Some i -> of_int (i * (n :> int)) | None -> of_bound_end bound_end - - - let mult_const_l = mult_const BoundEnd.LowerBound - - let mult_const_u = mult_const BoundEnd.UpperBound - - let neg : t -> t = function - | MInf -> - PInf - | PInf -> - MInf - | Linear (c, x) -> - Linear (-c, SymLinear.neg x) - | MinMax (c, sign, min_max, d, x) -> - mk_MinMax (-c, Sign.neg sign, min_max, d, x) - - - let div_const : t -> NonZeroInt.t -> t option = - fun x n -> - match x with - | MInf -> - Some (if NonZeroInt.is_positive n then MInf else PInf) - | PInf -> - Some (if NonZeroInt.is_positive n then PInf else MInf) - | Linear (c, x') when NonZeroInt.is_multiple c n -> ( - match SymLinear.exact_div_const_exn x' n with - | x'' -> - Some (Linear (c / (n :> int), x'')) - | exception NonZeroInt.DivisionNotExact -> - None ) - | _ -> - None - - - let get_symbols : t -> Symbol.t list = function - | MInf | PInf -> - [] - | Linear (_, se) -> - SymLinear.get_symbols se - | MinMax (_, _, _, _, s) -> - [s] - - - let are_similar b1 b2 = - match (b1, b2) with - | MInf, MInf -> - true - | PInf, PInf -> - true - | (Linear _ | MinMax _), (Linear _ | MinMax _) -> - true - | _ -> - false - - - let is_not_infty : t -> bool = function MInf | PInf -> false | _ -> true - - let lift1 : (t -> t) -> t bottom_lifted -> t bottom_lifted = - fun f x -> match x with Bottom -> Bottom | NonBottom x -> NonBottom (f x) - - - let lift2 : (t -> t -> t) -> t bottom_lifted -> t bottom_lifted -> t bottom_lifted = - fun f x y -> - match (x, y) with - | Bottom, _ | _, Bottom -> - Bottom - | NonBottom x, NonBottom y -> - NonBottom (f x y) - - - (** Substitutes ALL symbols in [x] with respect to [map]. Throws [Symbol_not_found] if a symbol in [x] can't be found in [map]. Under/over-Approximate as good as possible according to [subst_pos]. *) - let subst_exn : subst_pos:BoundEnd.t -> t -> t bottom_lifted SymbolMap.t -> t bottom_lifted = - fun ~subst_pos x map -> - let get_exn s = - match SymbolMap.find s map with - | NonBottom x when Symbol.is_unsigned s -> - NonBottom (ub ~default:x zero x) - | x -> - x - in - let get_mult_const s coeff = - try - if NonZeroInt.is_one coeff then get_exn s - else if NonZeroInt.is_minus_one coeff then get_exn s |> lift1 neg - else - match SymbolMap.find s map with - | Bottom -> - Bottom - | NonBottom x -> - let x = mult_const subst_pos coeff x in - if Symbol.is_unsigned s then NonBottom (ub ~default:x zero x) else NonBottom x - with Caml.Not_found -> - (* For unsigned symbols, we can over/under-approximate with zero depending on [subst_pos] and the sign of the coefficient. *) - match (Symbol.is_unsigned s, subst_pos, NonZeroInt.is_positive coeff) with - | true, BoundEnd.LowerBound, true | true, BoundEnd.UpperBound, false -> - NonBottom zero - | _ -> - raise (Symbol_not_found s) - in - match x with - | MInf | PInf -> - NonBottom x - | Linear (c, se) -> - SymLinear.fold se ~init:(NonBottom (of_int c)) ~f:(fun acc s coeff -> - lift2 (plus subst_pos) acc (get_mult_const s coeff) ) - | MinMax (c, sign, min_max, d, s) -> - match get_exn s with - | Bottom -> - Bottom - | exception Caml.Not_found -> ( - match int_of_minmax subst_pos x with - | Some i -> - NonBottom (of_int i) - | None -> - raise (Symbol_not_found s) ) - | NonBottom x' -> - let res = - match (sign, min_max, x') with - | Plus, Min, MInf | Minus, Max, PInf -> - MInf - | Plus, Max, PInf | Minus, Min, MInf -> - PInf - | sign, Min, PInf | sign, Max, MInf -> - of_int (Sign.eval_int sign c d) - | _, _, Linear (c2, se) - -> ( - if SymLinear.is_zero se then - of_int (Sign.eval_int sign c (MinMax.eval_int min_max d c2)) - else if SymLinear.is_one_symbol se then - mk_MinMax - (Sign.eval_int sign c c2, sign, min_max, d - c2, SymLinear.get_one_symbol se) - else if SymLinear.is_mone_symbol se then - mk_MinMax - ( Sign.eval_int sign c c2 - , Sign.neg sign - , MinMax.neg min_max - , c2 - d - , SymLinear.get_mone_symbol se ) - else - match int_of_minmax subst_pos x with - | Some i -> - of_int i - | None -> - of_bound_end subst_pos ) - | _, _, MinMax (c2, sign2, min_max2, d2, s2) -> - match (min_max, sign2, min_max2) with - | Min, Plus, Min | Max, Plus, Max -> - let c' = Sign.eval_int sign c c2 in - let d' = MinMax.eval_int min_max (d - c2) d2 in - mk_MinMax (c', sign, min_max, d', s2) - | Min, Minus, Max | Max, Minus, Min -> - let c' = Sign.eval_int sign c c2 in - let d' = MinMax.eval_int min_max2 (c2 - d) d2 in - mk_MinMax (c', Sign.neg sign, min_max2, d', s2) - | _ -> - let bound_end = - match sign with Plus -> subst_pos | Minus -> BoundEnd.neg subst_pos - in - of_int - (Sign.eval_int sign c - (MinMax.eval_int min_max d - (int_of_minmax bound_end x' |> Option.value ~default:d))) - in - NonBottom res - - - let subst_lb_exn x map = subst_exn ~subst_pos:BoundEnd.LowerBound x map - - let subst_ub_exn x map = subst_exn ~subst_pos:BoundEnd.UpperBound x map - - let simplify_bound_ends_from_paths x = - match x with - | MInf | PInf | MinMax _ -> - x - | Linear (c, se) -> - let se' = SymLinear.simplify_bound_ends_from_paths se in - if phys_equal se se' then x else Linear (c, se') -end - -type ('c, 's) valclass = Constant of 'c | Symbolic of 's | ValTop +module SymbolMap = Symb.SymbolMap +module Symbol = Symb.Symbol +module SymbolPath = Symb.SymbolPath +module SymbolTable = Symb.SymbolTable (** A NonNegativeBound is a Bound that is either non-negative or symbolic but will be evaluated to a non-negative value once instantiated *) module NonNegativeBound = struct @@ -964,7 +43,7 @@ module NonNegativeBound = struct let zero = Bound.zero - let of_bound b = if Bound.le b Bound.zero then Bound.zero else b + let of_bound b = if Bound.le b zero then zero else b let int_lb b = Bound.int_lb b |> Option.bind ~f:NonNegativeInt.of_int @@ -975,21 +54,21 @@ module NonNegativeBound = struct let classify = function | Bound.PInf -> - ValTop + Bounds.ValTop | Bound.MInf -> assert false | b -> match Bound.is_const b with | None -> - Symbolic b + Bounds.Symbolic b | Some c -> - Constant (NonNegativeInt.of_int_exn c) + Bounds.Constant (NonNegativeInt.of_int_exn c) let subst_exn b map = match Bound.subst_ub_exn b map with | Bottom -> - Constant NonNegativeInt.zero + Bounds.Constant NonNegativeInt.zero | NonBottom b -> of_bound b |> classify end @@ -1001,7 +80,7 @@ module type NonNegativeSymbol = sig val int_ub : t -> NonNegativeInt.t option - val subst_exn : t -> Bound.t bottom_lifted SymbolMap.t -> (NonNegativeInt.t, t) valclass + val subst_exn : t -> Bound.t bottom_lifted SymbolMap.t -> (NonNegativeInt.t, t) Bounds.valclass (** may throw Symbol_not_found *) val pp : F.formatter -> t -> unit @@ -1086,7 +165,7 @@ module MakePolynomial (S : NonNegativeSymbol) = struct let of_int_exn : int -> t = fun i -> i |> NonNegativeInt.of_int_exn |> of_non_negative_int - let of_valclass : (NonNegativeInt.t, S.t) valclass -> t top_lifted = function + let of_valclass : (NonNegativeInt.t, S.t) Bounds.valclass -> t top_lifted = function | ValTop -> Top | Constant i -> @@ -1232,7 +311,7 @@ module MakePolynomial (S : NonNegativeSymbol) = struct | Symbolic s -> let p = subst p map in mult_symb p s |> plus acc - | exception Symbol_not_found _ -> + | exception Bounds.Symbol_not_found _ -> raise ReturnTop ) terms (of_non_negative_int const) in @@ -1282,7 +361,7 @@ module NonNegativePolynomial = struct let of_int_exn i = NonTop (NonNegativeNonTopPolynomial.of_int_exn i) let of_non_negative_bound b = - b |> NonNegativeBound.classify |> NonNegativeNonTopPolynomial.of_valclass + b |> Bounds.NonNegativeBound.classify |> NonNegativeNonTopPolynomial.of_valclass let is_symbolic = function Top -> false | NonTop p -> NonNegativeNonTopPolynomial.is_symbolic p @@ -1314,14 +393,14 @@ module NonNegativePolynomial = struct end module ItvRange = struct - type t = NonNegativeBound.t + type t = Bounds.NonNegativeBound.t - let zero : t = NonNegativeBound.zero + let zero : t = Bounds.NonNegativeBound.zero let of_bounds : lb:Bound.t -> ub:Bound.t -> t = fun ~lb ~ub -> Bound.plus_u ub Bound.one |> Bound.plus_u (Bound.neg lb) - |> Bound.simplify_bound_ends_from_paths |> NonNegativeBound.of_bound + |> Bound.simplify_bound_ends_from_paths |> Bounds.NonNegativeBound.of_bound let to_top_lifted_polynomial : t -> NonNegativePolynomial.astate = @@ -1356,7 +435,7 @@ module ItvPure = struct NonBottom (l, u) | _ -> Bottom - | exception Symbol_not_found _ -> + | exception Bounds.Symbol_not_found _ -> (* For now, let's be VERY aggressive. Under-approximate unknown symbols with Bottom. *) Bottom @@ -1411,7 +490,7 @@ module ItvPure = struct let make_sym : unsigned:bool -> Typ.Procname.t -> SymbolTable.t -> SymbolPath.t -> Counter.t -> t = fun ~unsigned pname symbol_table path new_sym_num -> - let lb, ub = SymLinear.make ~unsigned pname symbol_table path new_sym_num in + let lb, ub = Bounds.SymLinear.make ~unsigned pname symbol_table path new_sym_num in (Bound.of_sym lb, Bound.of_sym ub) @@ -1617,19 +696,19 @@ module ItvPure = struct match (x, y) with | (l1, Bound.PInf), (_, u2) -> (l1, u2) - | (l1, Bound.Linear (c1, s1)), (_, Bound.Linear (c2, s2)) when SymLinear.eq s1 s2 -> + | (l1, Bound.Linear (c1, s1)), (_, Bound.Linear (c2, s2)) when Bounds.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 -> + | (l1, Bound.Linear (c, se)), (_, u) when Bounds.SymLinear.is_zero se && Bound.is_one_symbol u -> (l1, Bound.mk_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, u), (_, Bound.Linear (c, se)) when Bounds.SymLinear.is_zero se && Bound.is_one_symbol u -> (l1, Bound.mk_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.Linear (c, se)), (_, u) when Bounds.SymLinear.is_zero se && Bound.is_mone_symbol u -> (l1, Bound.mk_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, u), (_, Bound.Linear (c, se)) when Bounds.SymLinear.is_zero se && Bound.is_mone_symbol u -> (l1, Bound.mk_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 -> + when Bounds.SymLinear.is_zero se -> (l1, Bound.mk_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)) ) @@ -1644,19 +723,19 @@ module ItvPure = struct match (x, y) with | (Bound.MInf, u1), (l2, _) -> (l2, u1) - | (Bound.Linear (c1, s1), u1), (Bound.Linear (c2, s2), _) when SymLinear.eq s1 s2 -> + | (Bound.Linear (c1, s1), u1), (Bound.Linear (c2, s2), _) when Bounds.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 -> + | (Bound.Linear (c, se), u1), (l, _) when Bounds.SymLinear.is_zero se && Bound.is_one_symbol l -> (Bound.mk_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 -> + | (l, u1), (Bound.Linear (c, se), _) when Bounds.SymLinear.is_zero se && Bound.is_one_symbol l -> (Bound.mk_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.Linear (c, se), u1), (l, _) when Bounds.SymLinear.is_zero se && Bound.is_mone_symbol l -> (Bound.mk_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 -> + | (l, u1), (Bound.Linear (c, se), _) when Bounds.SymLinear.is_zero se && Bound.is_mone_symbol l -> (Bound.mk_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 -> + when Bounds.SymLinear.is_zero se -> (Bound.mk_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), _) ) diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 38ea390bb..5c1fb2bc9 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -8,14 +8,8 @@ open! IStd open! AbstractDomain.Types module F = Format - -module Counter : sig - type t - - val make : int -> t - - val next : t -> int -end +module Bound = Bounds.Bound +module Counter = Counter module Boolean : sig type t @@ -31,61 +25,10 @@ module Boolean : sig val is_true : t -> bool end -module SymbolPath : sig - type partial [@@deriving compare] - - type t [@@deriving compare] - - val of_pvar : Pvar.t -> partial - - val index : partial -> partial - - val field : partial -> Typ.Fieldname.t -> partial - - val normal : partial -> t - - val offset : partial -> t - - val length : partial -> t -end - -module Symbol : sig - type t -end - -module SymbolTable : sig - type summary_t - - val pp : F.formatter -> summary_t -> unit - - val find_opt : SymbolPath.t -> summary_t -> (Symbol.t * Symbol.t) option - - type t - - val empty : unit -> t - - val summary_of : t -> summary_t -end - -module SymbolMap : PrettyPrintable.PPMap with type key = Symbol.t - -module Bound : sig - type t [@@deriving compare] - - val zero : t - - val is_const : t -> int option - - val is_not_infty : t -> bool - - val is_symbolic : t -> bool - - val gt : t -> t -> bool - - val le : t -> t -> bool - - val lt : t -> t -> bool -end +module SymbolMap = Symb.SymbolMap +module Symbol = Symb.Symbol +module SymbolPath = Symb.SymbolPath +module SymbolTable = Symb.SymbolTable module NonNegativePolynomial : sig include AbstractDomain.WithTop @@ -209,7 +152,8 @@ val of_int_lit : IntLit.t -> t val of_int64 : Int64.t -> t -val make_sym : ?unsigned:bool -> Typ.Procname.t -> SymbolTable.t -> SymbolPath.t -> Counter.t -> t +val make_sym : + ?unsigned:bool -> Typ.Procname.t -> Symb.SymbolTable.t -> Symb.SymbolPath.t -> Counter.t -> t val lb : t -> Bound.t diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml new file mode 100644 index 000000000..489d217d5 --- /dev/null +++ b/infer/src/bufferoverrun/symb.ml @@ -0,0 +1,134 @@ +(* + * Copyright (c) 2017-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) +open! IStd +open! AbstractDomain.Types +module F = Format + +module BoundEnd = struct + type t = LowerBound | UpperBound + + let neg = function LowerBound -> UpperBound | UpperBound -> LowerBound + + let to_string = function LowerBound -> "lb" | UpperBound -> "ub" +end + +module SymbolPath = struct + type partial = Pvar of Pvar.t | Index of partial | Field of Typ.Fieldname.t * partial + [@@deriving compare] + + type t = Normal of partial | Offset of partial | Length of partial [@@deriving compare] + + let equal = [%compare.equal : t] + + let of_pvar pvar = Pvar pvar + + let field p fn = Field (fn, p) + + let index p = Index p + + let normal p = Normal p + + let offset p = Offset p + + let length p = Length p + + let rec pp_partial fmt = function + | Pvar pvar -> + Pvar.pp_value fmt pvar + | Index p -> + F.fprintf fmt "%a[*]" pp_partial p + | Field (fn, p) -> + F.fprintf fmt "%a.%s" pp_partial p (Typ.Fieldname.to_flat_string fn) + + + let pp fmt = function + | Normal p -> + pp_partial fmt p + | Offset p -> + F.fprintf fmt "%a.offset" pp_partial p + | Length p -> + F.fprintf fmt "%a.length" pp_partial p +end + +module Symbol = struct + type t = + {id: int; pname: Typ.Procname.t; unsigned: bool; path: SymbolPath.t; bound_end: BoundEnd.t} + + let compare s1 s2 = + (* Symbols only make sense within a given function, so shouldn't be compared across function boundaries. *) + assert (phys_equal s1.pname s2.pname) ; + Int.compare s1.id s2.id + + + let equal = [%compare.equal : t] + + let paths_equal s1 s2 = SymbolPath.equal s1.path s2.path + + let make : unsigned:bool -> Typ.Procname.t -> SymbolPath.t -> BoundEnd.t -> int -> t = + fun ~unsigned pname path bound_end id -> {id; pname; unsigned; path; bound_end} + + + let pp : F.formatter -> t -> unit = + fun fmt {pname; id; unsigned; path; bound_end} -> + F.fprintf fmt "%a.%s" SymbolPath.pp path (BoundEnd.to_string bound_end) ; + if Config.bo_debug > 1 then + let symbol_name = if unsigned then 'u' else 's' in + F.fprintf fmt "(%s-%c$%d)" (Typ.Procname.to_string pname) symbol_name id + + + let is_unsigned : t -> bool = fun x -> x.unsigned +end + +module SymbolTable = struct + module M = PrettyPrintable.MakePPMap (SymbolPath) + + type summary_t = (Symbol.t * Symbol.t) M.t + + let find_opt = M.find_opt + + let pp = M.pp ~pp_value:(fun fmt (lb, ub) -> F.fprintf fmt "[%a, %a]" Symbol.pp lb Symbol.pp ub) + + type t = summary_t ref + + let empty () = ref M.empty + + let lookup ~unsigned pname path symbol_table new_sym_num = + match M.find_opt path !symbol_table with + | Some s -> + s + | None -> + let s = + ( Symbol.make ~unsigned pname path LowerBound (Counter.next new_sym_num) + , Symbol.make ~unsigned pname path UpperBound (Counter.next new_sym_num) ) + in + symbol_table := M.add path s !symbol_table ; + s + + + let summary_of x = !x +end + +module SymbolMap = struct + include PrettyPrintable.MakePPMap (Symbol) + + let for_all2 : f:(key -> 'a option -> 'b option -> bool) -> 'a t -> 'b t -> bool = + fun ~f x y -> + match merge (fun k x y -> if f k x y then None else raise Exit) x y with + | _ -> + true + | exception Exit -> + false + + + let is_singleton : 'a t -> (key * 'a) option = + fun m -> + if is_empty m then None + else + let (kmin, _) as binding = min_binding m in + let kmax, _ = max_binding m in + if Symbol.equal kmin kmax then Some binding else None +end diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli new file mode 100644 index 000000000..c406f1c3c --- /dev/null +++ b/infer/src/bufferoverrun/symb.mli @@ -0,0 +1,75 @@ +(* + * Copyright (c) 2017-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd +open! AbstractDomain.Types +module F = Format + +module BoundEnd : sig + type t = LowerBound | UpperBound + + val neg : t -> t +end + +module SymbolPath : sig + type partial + + type t + + val of_pvar : Pvar.t -> partial + + val index : partial -> partial + + val field : partial -> Typ.Fieldname.t -> partial + + val normal : partial -> t + + val offset : partial -> t + + val length : partial -> t +end + +module Symbol : sig + type t + + val compare : t -> t -> int + + val is_unsigned : t -> bool + + val pp : F.formatter -> t -> unit + + val equal : t -> t -> bool + + val paths_equal : t -> t -> bool +end + +module SymbolMap : sig + include PrettyPrintable.PPMap with type key = Symbol.t + + val for_all2 : f:(key -> 'a option -> 'b option -> bool) -> 'a t -> 'b t -> bool + + val is_singleton : 'a t -> (key * 'a) option +end + +module SymbolTable : sig + module M : PrettyPrintable.PPMap with type key = SymbolPath.t + + type summary_t + + val pp : F.formatter -> summary_t -> unit + + val find_opt : SymbolPath.t -> summary_t -> (Symbol.t * Symbol.t) option + + type t + + val empty : unit -> t + + val summary_of : t -> summary_t + + val lookup : + unsigned:bool -> Typ.Procname.t -> M.key -> t -> Counter.t -> SymbolMap.key * SymbolMap.key +end