From aef3797837face6768dfd858253244a8c7cc1d55 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 2 Dec 2019 03:18:28 -0800 Subject: [PATCH] [inferbo] Add arrayBlk.mli Reviewed By: ezgicicek Differential Revision: D18750209 fbshipit-source-id: 67e0b9d4e --- infer/src/bufferoverrun/arrayBlk.ml | 8 +- infer/src/bufferoverrun/arrayBlk.mli | 95 +++++++++++++++++++ .../src/bufferoverrun/bufferOverrunDomain.ml | 2 +- .../src/bufferoverrun/bufferOverrunModels.ml | 6 +- .../bufferoverrun/bufferOverrunSemantics.ml | 8 +- infer/src/bufferoverrun/bufferOverrunUtils.ml | 6 +- 6 files changed, 110 insertions(+), 15 deletions(-) create mode 100644 infer/src/bufferoverrun/arrayBlk.mli diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml index b8106ff00..215e48990 100644 --- a/infer/src/bufferoverrun/arrayBlk.ml +++ b/infer/src/bufferoverrun/arrayBlk.ml @@ -247,9 +247,9 @@ module ArrInfo = struct Top - let offsetof = function C {offset} -> offset | Java _ -> Itv.zero | Top -> Itv.top + let get_offset = function C {offset} -> offset | Java _ -> Itv.zero | Top -> Itv.top - let sizeof = function C {size} -> size | Java {length} -> length | Top -> Itv.top + let get_size = function C {size} -> size | Java {length} -> length | Top -> Itv.top let byte_size = function | C {size; stride} -> @@ -304,9 +304,9 @@ let join_itv : cost_mode:bool -> f:(ArrInfo.t -> Itv.t) -> t -> Itv.t = fold (fun _ arr -> join (f arr)) a init -let offsetof ?(cost_mode = false) = join_itv ~cost_mode ~f:ArrInfo.offsetof +let get_offset ?(cost_mode = false) = join_itv ~cost_mode ~f:ArrInfo.get_offset -let sizeof ?(cost_mode = false) = join_itv ~cost_mode ~f:ArrInfo.sizeof +let get_size ?(cost_mode = false) = join_itv ~cost_mode ~f:ArrInfo.get_size let plus_offset : t -> Itv.t -> t = fun arr i -> map (fun a -> ArrInfo.plus_offset a i) arr diff --git a/infer/src/bufferoverrun/arrayBlk.mli b/infer/src/bufferoverrun/arrayBlk.mli new file mode 100644 index 000000000..7e4277a34 --- /dev/null +++ b/infer/src/bufferoverrun/arrayBlk.mli @@ -0,0 +1,95 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * 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 ArrInfo : sig + type t + + val byte_size : t -> Itv.t + (** Return size of array block as bytes *) + + val get_offset : t -> Itv.t + (** Return current offset of array block *) + + val get_size : t -> Itv.t + (** Return size of array block, i.e., number of cells *) +end + +include AbstractDomain.MapS with type key = AbsLoc.Allocsite.t and type value = ArrInfo.t + +val compare : t -> t -> int + +val bot : t + +val make_c : AbsLoc.Allocsite.t -> offset:Itv.t -> size:Itv.t -> stride:Itv.t -> t +(** Make an array block for C *) + +val make_java : AbsLoc.Allocsite.t -> length:Itv.t -> t +(** Make an array block for Java *) + +val unknown : t + +val get_pow_loc : t -> AbsLoc.PowLoc.t +(** Return all allocsites as [PowLoc.t] *) + +val is_bot : t -> bool + +val is_symbolic : t -> bool +(** Check if there is a symbolic integer value in its offset or size *) + +val lift_cmp_itv : (Itv.t -> Itv.t -> Boolean.t) -> Boolean.EqualOrder.t -> t -> t -> Boolean.t +(** Lift a comparison of [Itv.t] and [Loc.t] to that of [t]. The comparison for [Itv.t] is used for + integer values such as offset and size, and the comparison for [Loc.t] is used for allocsites. *) + +val transform_length : f:(Itv.t -> Itv.t) -> t -> t +(** Apply [f] to all sizes *) + +val prune_comp : Binop.t -> t -> t -> t +(** [prune_comp comp x y] returns a pruned value of [x] by [comp] and [y]. [comp] should be + [Binop.Le], [Ge], [Lt], or [Gt]. *) + +val prune_eq : t -> t -> t +(** [prune_eq x y] returns a pruned value of [x] by [== y]. *) + +val prune_ne : t -> t -> t +(** [prune_ne x y] returns a pruned value of [x] by [!= y]. *) + +val minus_offset : t -> Itv.t -> t + +val plus_offset : t -> Itv.t -> t + +val diff : t -> t -> Itv.t +(** Return difference of offsets between given array blocks *) + +val normalize : t -> t +(** Normalize all interval values such as offset and size in it. Thus, if an interval value is + invalid, the interval value is replaced with bottom. *) + +val subst : t -> Bounds.Bound.eval_sym -> AbsLoc.PowLoc.eval_locpath -> AbsLoc.PowLoc.t * t +(** Substitute symbolic abstract locations and symbolic interval value in the array block. + [eval_sym] is to get substituted interval values and [eval_locpath] is to get substituted + abstract locaion values. It also returns a set of abstract locations containing non-allocsite + locations from the substitution results. Since the key of [ArrayBlk.t] is [AbsLoc.Allocsite.t], + they cannot be written in this domain. *) + +val set_length : Itv.t -> t -> t + +val set_offset : Itv.t -> t -> t + +val set_stride : Z.t -> t -> t + +val get_symbols : t -> Symb.SymbolSet.t +(** Return all symbols for integer values in it *) + +val get_offset : ?cost_mode:bool -> t -> Itv.t +(** Return offset of the array block. If [cost_mode] is [true], it returns a conservative + (bigger than correct one), but not correct offset results. *) + +val get_size : ?cost_mode:bool -> t -> Itv.t +(** Return size of the array block. If [cost_mode] is [true], it returns a conservative (bigger + than correct one), but not correct size results. *) diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 8b0dc9452..8b8be2ed4 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -505,7 +505,7 @@ module Val = struct {x with traces} - let array_sizeof {arrayblk} = ArrayBlk.sizeof arrayblk + let array_sizeof {arrayblk} = ArrayBlk.get_size arrayblk let set_array_length : Location.t -> length:t -> t -> t = fun location ~length v -> diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 3c1ce879c..2d8999451 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -100,7 +100,7 @@ let fgets str_exp num_exp = let traces = Trace.Set.join (Dom.Val.get_traces str_v) (Dom.Val.get_traces num_v) in let update_strlen1 allocsite arrinfo acc = let strlen = - let offset = ArrayBlk.ArrInfo.offsetof arrinfo in + let offset = ArrayBlk.ArrInfo.get_offset arrinfo in let num = Dom.Val.get_itv num_v in Itv.plus offset (Itv.set_lb_zero (Itv.decr num)) in @@ -471,7 +471,7 @@ module CFArray = struct let length e = let exec {integer_type_widths} ~ret:(ret_id, _) mem = let v = Sem.eval_arr integer_type_widths e mem in - let length = Dom.Val.of_itv (ArrayBlk.sizeof (Dom.Val.get_array_blk v)) in + let length = Dom.Val.of_itv (ArrayBlk.get_size (Dom.Val.get_array_blk v)) in Dom.Mem.add_stack (Loc.of_id ret_id) length mem in {exec; check= no_check} @@ -673,7 +673,7 @@ module StdVector = struct let deref_of_vec = deref_of model_env elt_typ vec_arg mem in let array_v = Dom.Mem.find_set deref_of_vec mem in let traces = Dom.Val.get_traces array_v in - let size = ArrayBlk.sizeof (Dom.Val.get_array_blk array_v) in + let size = ArrayBlk.get_size (Dom.Val.get_array_blk array_v) in let empty = Dom.Val.of_itv ~traces (Itv.of_bool (Itv.le_sem size Itv.zero)) in let mem = model_by_value empty id mem in match PowLoc.is_singleton_or_more deref_of_vec with diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 77519e442..070ebb266 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -441,10 +441,10 @@ let eval_sympath ~mode params sympath mem = (Val.get_itv v, Val.get_traces v) | Symb.SymbolPath.Offset {p} -> let v = eval_sympath_partial ~mode params p mem in - (ArrayBlk.offsetof ~cost_mode:(is_cost_mode mode) (Val.get_array_blk v), Val.get_traces v) + (ArrayBlk.get_offset ~cost_mode:(is_cost_mode mode) (Val.get_array_blk v), Val.get_traces v) | Symb.SymbolPath.Length {p} -> let v = eval_sympath_partial ~mode params p mem in - (ArrayBlk.sizeof ~cost_mode:(is_cost_mode mode) (Val.get_array_blk v), Val.get_traces v) + (ArrayBlk.get_size ~cost_mode:(is_cost_mode mode) (Val.get_array_blk v), Val.get_traces v) let mk_eval_sym_trace integer_type_widths (callee_formals : (Pvar.t * Typ.t) list) @@ -498,7 +498,7 @@ let eval_array_locs_length arr_locs mem = else let arr = Mem.find_set arr_locs mem in let traces = Val.get_traces arr in - let length = Val.get_array_blk arr |> ArrayBlk.sizeof in + let length = Val.get_array_blk arr |> ArrayBlk.get_size in match Itv.get_bound length Symb.BoundEnd.UpperBound with | NonBottom b when not (Bounds.Bound.is_pinf b) -> Val.of_itv ~traces length @@ -645,7 +645,7 @@ module Prune = struct ~f:(fun astate (alias_typ, lv, i, java_tmp) -> let array_v = Mem.find lv mem in let lhs = - Val.get_array_blk array_v |> ArrayBlk.sizeof + Val.get_array_blk array_v |> ArrayBlk.get_size |> Itv.plus (Itv.of_int_lit i) |> Val.of_itv |> Val.set_itv_updated_by_addition in diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 895bcc24f..0930f7366 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -231,7 +231,7 @@ module Exec = struct let src_itv = Dom.Val.get_itv src in let set_c_strlen1 allocsite arrinfo acc = let loc = Loc.of_allocsite allocsite in - let idx = Dom.Val.of_itv ~traces (ArrayBlk.ArrInfo.offsetof arrinfo) in + let idx = Dom.Val.of_itv ~traces (ArrayBlk.ArrInfo.get_offset arrinfo) in if Itv.leq ~lhs:Itv.zero ~rhs:src_itv then Dom.Mem.set_first_idx_of_null loc idx acc else Dom.Mem.unset_first_idx_of_null loc idx acc in @@ -256,7 +256,7 @@ module Check = struct let offsetof arr_info = - match ArrayBlk.ArrInfo.offsetof arr_info with + match ArrayBlk.ArrInfo.get_offset arr_info with | Bottom -> (* Java's collection has no offset. *) Itv.ItvPure.zero @@ -280,7 +280,7 @@ module Check = struct op idx_sym_exp offset_sym_exp ) in let array_access1 allocsite arr_info acc = - let size = ArrayBlk.ArrInfo.sizeof arr_info in + let size = ArrayBlk.ArrInfo.get_size arr_info in let offset = offsetof arr_info in log_array_access allocsite size offset idx ; check_access ~size ~idx ~offset ~size_sym_exp ~idx_sym_exp ~relation ~arr_traces ~idx_traces