From 5f5b3de91a1a6a794ad2212e2e779de07fd274d1 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 22 Aug 2019 03:11:10 -0700 Subject: [PATCH] [inferbo] Pruning collection.size in Java Summary: It prunes the size of collections when the size function is called in the condition expression. The diff extended the alias domain to understand temporary variables of SIL from Java. Depends on D16761461 Reviewed By: ezgicicek Differential Revision: D16761611 fbshipit-source-id: 849c5c71c --- infer/src/bufferoverrun/absLoc.ml | 2 + .../src/bufferoverrun/bufferOverrunDomain.ml | 108 ++++++++++++++---- .../src/bufferoverrun/bufferOverrunModels.ml | 7 +- .../bufferoverrun/bufferOverrunSemantics.ml | 11 +- infer/src/istd/IOption.ml | 2 + infer/src/istd/IOption.mli | 3 + .../java/bufferoverrun/Array.java | 32 ++++++ .../java/bufferoverrun/issues.exp | 1 + 8 files changed, 140 insertions(+), 26 deletions(-) diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index f6c8fbcf1..e441004aa 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -257,6 +257,8 @@ module Loc = struct false + let is_frontend_tmp = function Var x -> not (Var.appears_in_source_code x) | _ -> false + let rec is_pretty = function | Var _ -> true diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index b9685efb4..3f8074b63 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -689,6 +689,7 @@ module AliasTarget = struct | Size of Loc.t | Fgets of Loc.t | Nullity of Loc.t + | Top [@@deriving compare] let equal = [%compare.equal: t] @@ -707,6 +708,8 @@ module AliasTarget = struct F.fprintf fmt "fgets(%a)" Loc.pp l | Nullity l -> F.fprintf fmt "nullity(%a)" Loc.pp l + | Top -> + F.fprintf fmt "T" let fgets l = Fgets l @@ -715,10 +718,12 @@ module AliasTarget = struct let get_loc = function | Simple l | SimplePlusA (l, _) | Empty l | Size l | Fgets l | Nullity l -> - l + Some l + | Top -> + None - let use l x = Loc.equal l (get_loc x) + let use_loc l x = Option.value_map (get_loc x) ~default:false ~f:(Loc.equal l) let loc_map x ~f = match x with @@ -734,18 +739,17 @@ module AliasTarget = struct Option.map (f l) ~f:(fun l -> Fgets l) | Nullity l -> Option.map (f l) ~f:(fun l -> Nullity l) + | Top -> + Some Top let ( <= ) ~lhs ~rhs = equal lhs rhs - let join x y = - assert (equal x y) ; - x - + let join x y = if equal x y then x else Top let widen ~prev ~next ~num_iters:_ = join prev next - let is_unknown x = Loc.is_unknown (get_loc x) + let is_unknown x = Option.value_map (get_loc x) ~default:false ~f:Loc.is_unknown end (* Relations between values of logical variables(registers) and program variables @@ -767,23 +771,76 @@ end AliasTarget.Empty relation, but is used when there is a program variable [i] for the length of the array. *) module AliasMap = struct - include AbstractDomain.Map (Ident) (AliasTarget) + module Key = struct + type t = IdentKey of Ident.t | JavaTmp of Loc.t [@@deriving compare] + + let of_id id = IdentKey id + + let of_java_tmp l = JavaTmp l + + let pp f = function IdentKey id -> Ident.pp f id | JavaTmp l -> Loc.pp f l + + let use_loc l = function JavaTmp l' -> Loc.equal l l' | IdentKey _ -> false + end + + include AbstractDomain.InvertedMap (Key) (AliasTarget) + + let some_non_top = function AliasTarget.Top -> None | v -> Some v + + let add k v m = match some_non_top v with None -> remove k m | Some v -> add k v m + + let join x y = + let join_v _key vx vy = + IOption.map2 vx vy ~f:(fun vx vy -> AliasTarget.join vx vy |> some_non_top) + in + merge join_v x y + + + let widen ~prev:x ~next:y ~num_iters = + let widen_v _key vx vy = + IOption.map2 vx vy ~f:(fun vx vy -> + AliasTarget.widen ~prev:vx ~next:vy ~num_iters |> some_non_top ) + in + merge widen_v x y + let pp : F.formatter -> t -> unit = fun fmt x -> if not (is_empty x) then let pp_sep fmt () = F.fprintf fmt ", @," in - let pp1 fmt (k, v) = F.fprintf fmt "%a=%a" Ident.pp k AliasTarget.pp v in + let pp1 fmt (k, v) = F.fprintf fmt "%a=%a" Key.pp k AliasTarget.pp v in F.pp_print_list ~pp_sep pp1 fmt (bindings x) + let find_id : Ident.t -> t -> AliasTarget.t option = fun id x -> find_opt (Key.of_id id) x + + let find_java_tmp : Loc.t -> t -> AliasTarget.t option = + fun id x -> find_opt (Key.of_java_tmp id) x + + let load : Ident.t -> AliasTarget.t -> t -> t = - fun id a x -> if not (AliasTarget.is_unknown a) then add id a x else x + fun id tgt x -> + if AliasTarget.is_unknown tgt then x + else + let tgt = + match tgt with + | AliasTarget.Simple loc when Language.curr_language_is Java -> + Option.value (find_java_tmp loc x) ~default:tgt + | _ -> + tgt + in + add (Key.of_id id) tgt x + + let forget : Loc.t -> t -> t = + fun l m -> filter (fun k y -> (not (Key.use_loc l k)) && not (AliasTarget.use_loc l y)) m - let forget : Loc.t -> t -> t = fun l m -> filter (fun _ y -> not (AliasTarget.use l y)) m - let find : Ident.t -> t -> AliasTarget.t option = find_opt + let store : Loc.t -> Ident.t -> t -> t = + fun l id x -> + if Language.curr_language_is Java && Loc.is_frontend_tmp l then + Option.value_map (find_id id x) ~default:x ~f:(fun tgt -> add (Key.of_java_tmp l) tgt x) + else x end module AliasRet = struct @@ -823,7 +880,7 @@ module Alias = struct let bind_map : (AliasMap.t -> 'a) -> t -> 'a = fun f a -> f a.map - let find : Ident.t -> t -> AliasTarget.t option = fun x -> bind_map (AliasMap.find x) + let find_id : Ident.t -> t -> AliasTarget.t option = fun x -> bind_map (AliasMap.find_id x) let find_ret : t -> AliasTarget.t option = fun x -> AliasRet.get x.ret @@ -833,9 +890,12 @@ module Alias = struct fun loc e a -> let a = lift_map (AliasMap.forget loc) a in match e with - | Exp.Var l when Loc.is_return loc -> - let update_ret retl = {a with ret= AliasRet.v retl} in - Option.value_map (find l a) ~default:a ~f:update_ret + | Exp.Var l -> + let a = lift_map (AliasMap.store loc l) a in + if Loc.is_return loc then + let update_ret retl = {a with ret= AliasRet.v retl} in + Option.value_map (find_id l a) ~default:a ~f:update_ret + else a | Exp.BinOp (Binop.PlusA _, Exp.Var id, Exp.Const (Const.Cint i)) | Exp.BinOp (Binop.PlusA _, Exp.Const (Const.Cint i), Exp.Var id) -> lift_map (AliasMap.load id (AliasTarget.SimplePlusA (loc, IntLit.neg i))) a @@ -866,7 +926,8 @@ module Alias = struct a - let remove_temp : Ident.t -> t -> t = fun temp -> lift_map (AliasMap.remove temp) + let remove_temp : Ident.t -> t -> t = + fun temp -> lift_map (AliasMap.remove (AliasMap.Key.of_id temp)) end module CoreVal = struct @@ -1350,22 +1411,27 @@ module MemReach = struct PowLoc.fold find_join locs Val.bot - let find_alias : Ident.t -> _ t0 -> AliasTarget.t option = fun k m -> Alias.find k m.alias + let find_alias : Ident.t -> _ t0 -> AliasTarget.t option = fun k m -> Alias.find_id k m.alias let find_simple_alias : Ident.t -> _ t0 -> (Loc.t * IntLit.t option) option = fun k m -> - match Alias.find k m.alias with + match Alias.find_id k m.alias with | Some (AliasTarget.Simple l) -> Some (l, None) | Some (AliasTarget.SimplePlusA (l, i)) -> Some (l, Some i) - | Some (AliasTarget.Empty _ | AliasTarget.Size _ | AliasTarget.Fgets _ | AliasTarget.Nullity _) + | Some + ( AliasTarget.Empty _ + | AliasTarget.Size _ + | AliasTarget.Fgets _ + | AliasTarget.Nullity _ + | AliasTarget.Top ) | None -> None let find_size_alias : Ident.t -> _ t0 -> Loc.t option = - fun k m -> match Alias.find k m.alias with Some (AliasTarget.Size l) -> Some l | _ -> None + fun k m -> match Alias.find_id k m.alias with Some (AliasTarget.Size l) -> Some l | _ -> None let find_ret_alias : _ t0 -> AliasTarget.t option = fun m -> Alias.find_ret m.alias diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 236a58b83..05731732c 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -892,7 +892,12 @@ module Collection = struct let size coll_exp = let exec _ ~ret:(ret_id, _) mem = let result = eval_collection_length coll_exp mem in - model_by_value result ret_id mem + let mem = model_by_value result ret_id mem in + match PowLoc.is_singleton_or_more (eval_collection_internal_array_locs coll_exp mem) with + | IContainer.Singleton loc -> + Dom.Mem.load_size_alias ret_id loc mem + | IContainer.Empty | IContainer.More -> + mem in {exec; check= no_check} diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index d6d830142..7691fac24 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -30,7 +30,9 @@ let rec must_alias : Exp.t -> Exp.t -> Mem.t -> bool = | Exp.Var x1, Exp.Var x2 -> ( match (Mem.find_alias x1 m, Mem.find_alias x2 m) with | Some x1', Some x2' -> - AliasTarget.equal x1' x2' && not (Mem.is_rep_multi_loc (AliasTarget.get_loc x1') m) + AliasTarget.equal x1' x2' + && Option.value_map (AliasTarget.get_loc x1') ~default:false ~f:(fun l -> + not (Mem.is_rep_multi_loc l m) ) | _, _ -> false ) | Exp.UnOp (uop1, e1', _), Exp.UnOp (uop2, e2', _) -> @@ -313,7 +315,8 @@ let rec eval_arr : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Val.t = | AliasTarget.Size _ | AliasTarget.Empty _ | AliasTarget.Fgets _ - | AliasTarget.Nullity _ ) + | AliasTarget.Nullity _ + | Top ) | None -> Val.bot ) | Exp.Lvar pvar -> @@ -513,7 +516,7 @@ module Prune = struct let v = Mem.find lv mem in let v' = Val.prune_eq_zero v in update_mem_in_prune lv v' astate - | Some (AliasTarget.SimplePlusA _ | AliasTarget.Size _) | None -> + | Some (AliasTarget.SimplePlusA _ | AliasTarget.Size _ | Top) | None -> astate ) | Exp.UnOp (Unop.LNot, Exp.Var x, _) -> ( match Mem.find_alias x mem with @@ -530,7 +533,7 @@ module Prune = struct let itv_v = Itv.prune_comp Binop.Ge (Val.get_itv v) Itv.one in let v' = Val.modify_itv itv_v v in update_mem_in_prune lv v' astate - | Some (AliasTarget.SimplePlusA _ | AliasTarget.Size _ | AliasTarget.Fgets _) | None -> + | Some (AliasTarget.SimplePlusA _ | AliasTarget.Size _ | AliasTarget.Fgets _ | Top) | None -> astate ) | _ -> astate diff --git a/infer/src/istd/IOption.ml b/infer/src/istd/IOption.ml index 478d01a86..51ba16943 100644 --- a/infer/src/istd/IOption.ml +++ b/infer/src/istd/IOption.ml @@ -14,3 +14,5 @@ let value_default_f ~f = function None -> f () | Some v -> v let if_none_evalopt ~f x = match x with None -> f () | Some _ -> x let if_none_eval = value_default_f + +let map2 x y ~f = match (x, y) with None, _ | _, None -> None | Some x, Some y -> f x y diff --git a/infer/src/istd/IOption.mli b/infer/src/istd/IOption.mli index 6b06d7037..16f2e273a 100644 --- a/infer/src/istd/IOption.mli +++ b/infer/src/istd/IOption.mli @@ -22,3 +22,6 @@ val if_none_eval : f:(unit -> 'a) -> 'a option -> 'a (** [if_none_eval ~f x] evaluates to [y] if [x=Some y] else to [f ()]. Useful for terminating chains built with [if_none_evalopt]. This is exactly the same as [value_default_f] but with a better name. *) + +val map2 : 'a option -> 'b option -> f:('a -> 'b -> 'c option) -> 'c option +(** Like [Option.map2] but [f] may return [None]. *) diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/Array.java b/infer/tests/codetoanalyze/java/bufferoverrun/Array.java index 532d36b93..8f52d04f2 100644 --- a/infer/tests/codetoanalyze/java/bufferoverrun/Array.java +++ b/infer/tests/codetoanalyze/java/bufferoverrun/Array.java @@ -68,4 +68,36 @@ class Array { void positive_alloc_Good() { a = new ArrayList<>(10); } + + void iterate_collection_Good(ArrayList a) { + if (a.size() > 10) { + int x = a.get(9); + } + } + + void call_iterate_collection_Good() { + ArrayList x = new ArrayList(); + x.add(0); + x.add(0); + x.add(0); + x.add(0); + x.add(0); + this.iterate_collection_Good(x); + } + + void iterate_collection_Bad(ArrayList a) { + if (a.size() >= 5) { + int x = a.get(5); + } + } + + void call_iterate_collection_Bad() { + ArrayList x = new ArrayList(); + x.add(0); + x.add(0); + x.add(0); + x.add(0); + x.add(0); + this.iterate_collection_Bad(x); + } } diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp index 1e35a1372..8300352a5 100644 --- a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp @@ -1,3 +1,4 @@ +codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.call_iterate_collection_Bad():void, 7, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Through,Through,Through,Through,Through,Call,,Array declaration,Array access: Offset: 5 Size: 5 by call to `void Array.iterate_collection_Bad(ArrayList)` ] codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.collection_remove_from_empty_Bad():java.util.ArrayList, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 0 Size: 0] codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.negative_alloc_Bad():void, 1, INFERBO_ALLOC_IS_NEGATIVE, no_bucket, ERROR, [Allocation: Length: -1] codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning1_Bad():void, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]