From 54de59919ea1f5ebb08ac400572334b3a9c11205 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 9 Oct 2017 08:48:35 -0700 Subject: [PATCH] [inferbo] Prune vector's size by vector::empty() condition check Summary: A specific type of alias is added for the vector::empty() result and it is used at pruning. Now, there are two types of aliases: - "simple" alias: x=y - "empty" alias: x=v.empty() and y=v.size So, if x!=0, y is pruned by (y=0). Otherwise, i.e., x==0, y is pruned by (y>=1). Reviewed By: mbouaziz Differential Revision: D6004968 fbshipit-source-id: bb8d50d --- .../infer_model/vector_bufferoverrun.h | 4 +- .../src/bufferoverrun/bufferOverrunChecker.ml | 16 ++- .../src/bufferoverrun/bufferOverrunDomain.ml | 112 ++++++++++++++---- .../bufferoverrun/bufferOverrunSemantics.ml | 45 ++++--- .../cpp/bufferoverrun/issues.exp | 2 +- .../cpp/bufferoverrun/vector.cpp | 12 ++ 6 files changed, 147 insertions(+), 44 deletions(-) diff --git a/infer/models/cpp/include/infer_model/vector_bufferoverrun.h b/infer/models/cpp/include/infer_model/vector_bufferoverrun.h index bc907ba26..7e4cdcdb0 100644 --- a/infer/models/cpp/include/infer_model/vector_bufferoverrun.h +++ b/infer/models/cpp/include/infer_model/vector_bufferoverrun.h @@ -31,6 +31,8 @@ extern "C" { int __inferbo_min(int, int); } +bool __inferbo_empty(int* size) { return 1 - __inferbo_min(*size, 1); } + INFER_NAMESPACE_STD_BEGIN struct bool_ref { @@ -216,7 +218,7 @@ class vector { size_type capacity() const noexcept {} - bool empty() const noexcept { return 1 - __inferbo_min(infer_size, 1); } + bool empty() const noexcept { return __inferbo_empty((int*)&infer_size); } size_type max_size() const noexcept; void reserve(size_type __n); void shrink_to_fit() noexcept; diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index aa156c781..925927d33 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -349,13 +349,25 @@ module TransferFunctions (CFG : ProcCfg.S) = struct if Ident.is_none id then mem else let mem = Dom.Mem.add_stack (Loc.of_var (Var.of_id id)) v mem in - if PowLoc.is_singleton locs then Dom.Mem.load_alias id (PowLoc.min_elt locs) mem + if PowLoc.is_singleton locs then + Dom.Mem.load_simple_alias id (PowLoc.min_elt locs) mem else mem | Store (exp1, _, exp2, loc) -> let locs = Sem.eval exp1 mem loc |> Dom.Val.get_all_locs in let v = Sem.eval exp2 mem loc |> Dom.Val.add_trace_elem (Trace.Assign loc) in let mem = Dom.Mem.update_mem locs v mem in - if PowLoc.is_singleton locs then Dom.Mem.store_alias (PowLoc.min_elt locs) exp2 mem + if PowLoc.is_singleton locs then + let loc_v = PowLoc.min_elt locs in + match Typ.Procname.get_method pname with + | "__inferbo_empty" when Loc.is_return loc_v -> ( + match Sem.get_formals pdesc with + | [(formal, _)] + -> let formal_v = Dom.Mem.find_heap (Loc.of_pvar formal) mem in + Dom.Mem.store_empty_alias formal_v loc_v exp2 mem + | _ + -> assert false ) + | _ + -> Dom.Mem.store_simple_alias loc_v exp2 mem else mem | Prune (exp, loc, _, _) -> Sem.prune exp loc mem diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 1d9bd699e..67a5e638f 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -325,10 +325,40 @@ module Heap = struct if is_empty mem then Val.bot else snd (choose mem) end +module AliasTarget = struct + type t = Simple of Loc.t | Empty of Loc.t [@@deriving compare] + + let equal = [%compare.equal : t] + + let pp fmt = function Simple l -> Loc.pp fmt l | Empty l -> F.fprintf fmt "empty(%a)" Loc.pp l + + let of_simple l = Simple l + + let of_empty l = Empty l + + let use l = function Simple l' | Empty l' -> Loc.equal l l' + + let replace l = function Simple _ -> Simple l | Empty _ -> Empty l +end + +(* Relations between values of logical variables(registers) and + program variables + + "AliasTarget.Simple relation": Since Sil distinguishes logical and + program variables, we need a relation for pruning values of program + variables. For example, a C statement "if(x){...}" is translated + to "%r=load(x); if(%r){...}" in Sil. At the load statement, we + record the alias between the values of %r and x, then we can prune + not only the value of %r, but also that of x inside the if branch. + + "AliasTarget.Empty relation": For pruning vector.size with + vector::empty() results, we adopt a specific relation between %r + and x, where %r=v.empty() and x=v.size. So, if %r!=0, x is pruned + by x=0. On the other hand, if %r==0, x is pruned by x>=1. *) module AliasMap = struct module M = Caml.Map.Make (Ident) - type t = Loc.t M.t + type t = AliasTarget.t M.t type astate = t @@ -337,7 +367,7 @@ module AliasMap = struct let ( <= ) : lhs:t -> rhs:t -> bool = fun ~lhs ~rhs -> let is_in_rhs k v = - match M.find k rhs with v' -> Loc.equal v v' | exception Not_found -> false + match M.find k rhs with v' -> AliasTarget.equal v v' | exception Not_found -> false in M.for_all is_in_rhs lhs @@ -350,7 +380,7 @@ module AliasMap = struct | Some v, None | None, Some v -> Some v | Some v1, Some v2 - -> if Loc.equal v1 v2 then Some v1 else assert false + -> if AliasTarget.equal v1 v2 then Some v1 else assert false in M.merge join_v x y @@ -360,18 +390,19 @@ module AliasMap = struct let pp : F.formatter -> t -> unit = fun fmt x -> let pp_sep fmt () = F.fprintf fmt ", @," in - let pp1 fmt (k, v) = F.fprintf fmt "%a=%a" (Ident.pp Pp.text) k Loc.pp v in + let pp1 fmt (k, v) = F.fprintf fmt "%a=%a" (Ident.pp Pp.text) k AliasTarget.pp v in (* F.fprintf fmt "@[Logical Variables :@,"; *) F.fprintf fmt "@[{ @," ; F.pp_print_list ~pp_sep pp1 fmt (M.bindings x) ; F.fprintf fmt " }@]" ; F.fprintf fmt "@]" - let load : Ident.t -> Loc.t -> t -> t = fun id loc m -> M.add id loc m + let load : Ident.t -> AliasTarget.t -> t -> t = fun id loc m -> M.add id loc m - let store : Loc.t -> Exp.t -> t -> t = fun l _ m -> M.filter (fun _ y -> not (Loc.equal l y)) m + let store : Loc.t -> Exp.t -> t -> t = + fun l _ m -> M.filter (fun _ y -> not (AliasTarget.use l y)) m - let find : Ident.t -> t -> Loc.t option = + let find : Ident.t -> t -> AliasTarget.t option = fun k m -> try Some (M.find k m) with Not_found -> None @@ -383,7 +414,7 @@ module AliasMap = struct end module AliasRet = struct - type astate = Bot | L of Loc.t | Top + type astate = Bot | L of AliasTarget.t | Top let bot = Bot @@ -395,7 +426,7 @@ module AliasRet = struct | Top, _ | _, Bot -> false | L loc1, L loc2 - -> Loc.equal loc1 loc2 + -> AliasTarget.equal loc1 loc2 let join : astate -> astate -> astate = fun x y -> @@ -405,7 +436,7 @@ module AliasRet = struct | Bot, a | a, Bot -> a | L loc1, L loc2 - -> if Loc.equal loc1 loc2 then x else Top + -> if AliasTarget.equal loc1 loc2 then x else Top let widen : prev:astate -> next:astate -> num_iters:int -> astate = fun ~prev ~next ~num_iters:_ -> join prev next @@ -416,11 +447,11 @@ module AliasRet = struct | Top -> F.fprintf fmt "T" | L loc - -> Loc.pp fmt loc + -> AliasTarget.pp fmt loc | Bot -> F.fprintf fmt "_|_" - let find : astate -> Loc.t option = fun x -> match x with L loc -> Some loc | _ -> None + let find : astate -> AliasTarget.t option = fun x -> match x with L loc -> Some loc | _ -> None end module Alias = struct @@ -433,13 +464,14 @@ module Alias = struct let lift_v : (AliasMap.astate -> 'a) -> astate -> 'a = fun f a -> f (fst a) - let find : Ident.t -> astate -> Loc.t option = fun x -> lift_v (AliasMap.find x) + let find : Ident.t -> astate -> AliasTarget.t option = fun x -> lift_v (AliasMap.find x) - let find_ret : astate -> Loc.t option = fun x -> AliasRet.find (snd x) + let find_ret : astate -> AliasTarget.t option = fun x -> AliasRet.find (snd x) - let load : Ident.t -> Loc.t -> astate -> astate = fun id loc -> lift (AliasMap.load id loc) + let load : Ident.t -> AliasTarget.t -> astate -> astate = + fun id loc -> lift (AliasMap.load id loc) - let store : Loc.t -> Exp.t -> astate -> astate = + let store_simple : Loc.t -> Exp.t -> astate -> astate = fun loc e a -> let a = lift (AliasMap.store loc e) a in match e with @@ -449,6 +481,14 @@ module Alias = struct | _ -> a + let store_empty : Val.t -> Loc.t -> Exp.t -> astate -> astate = + fun formal loc e a -> + let a = lift (AliasMap.store loc e) a in + let locs = Val.get_all_locs formal in + if PowLoc.is_singleton locs then + (fst a, AliasRet.L (AliasTarget.of_empty (PowLoc.min_elt locs))) + else a + let remove_temps : Ident.t list -> astate -> astate = fun temps a -> (AliasMap.remove_temps temps (fst a), snd a) end @@ -502,15 +542,26 @@ module MemReach = struct let find_set : PowLoc.t -> t -> Val.t = fun k m -> Val.join (find_stack_set k m) (find_heap_set k m) - let find_alias : Ident.t -> t -> Loc.t option = fun k m -> Alias.find k m.alias + let find_alias : Ident.t -> t -> AliasTarget.t option = fun k m -> Alias.find k m.alias + + let find_simple_alias : Ident.t -> t -> Loc.t option = + fun k m -> + match Alias.find k m.alias with + | Some AliasTarget.Simple l + -> Some l + | Some AliasTarget.Empty _ | None + -> None - let find_ret_alias : t -> Loc.t option = fun m -> Alias.find_ret m.alias + let find_ret_alias : t -> AliasTarget.t option = fun m -> Alias.find_ret m.alias - let load_alias : Ident.t -> Loc.t -> t -> t = + let load_alias : Ident.t -> AliasTarget.t -> t -> t = fun id loc m -> {m with alias= Alias.load id loc m.alias} - let store_alias : Loc.t -> Exp.t -> t -> t = - fun loc e m -> {m with alias= Alias.store loc e m.alias} + let store_simple_alias : Loc.t -> Exp.t -> t -> t = + fun loc e m -> {m with alias= Alias.store_simple loc e m.alias} + + let store_empty_alias : Val.t -> Loc.t -> Exp.t -> t -> t = + fun formal loc e m -> {m with alias= Alias.store_empty formal loc e m.alias} let add_stack : Loc.t -> Val.t -> t -> t = fun k v m -> {m with stack= Stack.add k v m.stack} @@ -587,14 +638,25 @@ module Mem = struct let find_set : PowLoc.t -> t -> Val.t = fun k -> f_lift_default Val.bot (MemReach.find_set k) - let find_alias : Ident.t -> t -> Loc.t option = + let find_alias : Ident.t -> t -> AliasTarget.t option = fun k -> f_lift_default None (MemReach.find_alias k) - let find_ret_alias : t -> Loc.t option = f_lift_default None MemReach.find_ret_alias + let find_simple_alias : Ident.t -> t -> Loc.t option = + fun k -> f_lift_default None (MemReach.find_simple_alias k) + + let find_ret_alias : t -> AliasTarget.t option = f_lift_default None MemReach.find_ret_alias + + let load_alias : Ident.t -> AliasTarget.t -> t -> t = + fun id loc -> f_lift (MemReach.load_alias id loc) + + let load_simple_alias : Ident.t -> Loc.t -> t -> t = + fun id loc -> load_alias id (AliasTarget.Simple loc) - let load_alias : Ident.t -> Loc.t -> t -> t = fun id loc -> f_lift (MemReach.load_alias id loc) + let store_simple_alias : Loc.t -> Exp.t -> t -> t = + fun loc e -> f_lift (MemReach.store_simple_alias loc e) - let store_alias : Loc.t -> Exp.t -> t -> t = fun loc e -> f_lift (MemReach.store_alias loc e) + let store_empty_alias : Val.t -> Loc.t -> Exp.t -> t -> t = + fun formal loc e -> f_lift (MemReach.store_empty_alias formal loc e) let add_stack : Loc.t -> Val.t -> t -> t = fun k v -> f_lift (MemReach.add_stack k v) diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 79c1a7f8e..99a31a646 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -79,7 +79,7 @@ module Make (CFG : ProcCfg.S) = struct | Exp.Var x1, Exp.Var x2 -> ( match (Mem.find_alias x1 m, Mem.find_alias x2 m) with | Some x1', Some x2' - -> Loc.equal x1' x2' + -> AliasTarget.equal x1' x2' | _, _ -> false ) | Exp.UnOp (uop1, e1', _), Exp.UnOp (uop2, e2', _) @@ -275,9 +275,9 @@ module Make (CFG : ProcCfg.S) = struct match exp with | Exp.Var id -> ( match Mem.find_alias id mem with - | Some loc + | Some AliasTarget.Simple loc -> PowLoc.singleton loc |> Val.of_pow_loc - | None + | Some AliasTarget.Empty _ | None -> Val.bot ) | Exp.Lvar pvar -> pvar |> Loc.of_pvar |> PowLoc.singleton |> Val.of_pow_loc @@ -315,19 +315,29 @@ module Make (CFG : ProcCfg.S) = struct match e with | Exp.Var x -> ( match Mem.find_alias x mem with - | Some lv + | Some AliasTarget.Simple lv -> let v = Mem.find_heap lv mem in let v' = Val.prune_zero v in Mem.update_mem (PowLoc.singleton lv) v' mem + | Some AliasTarget.Empty lv + -> let v = Mem.find_heap lv mem in + let itv_v = Itv.prune_eq (Val.get_itv v) Itv.zero in + let v' = Val.modify_itv itv_v v in + Mem.update_mem (PowLoc.singleton lv) v' mem | None -> mem ) | Exp.UnOp (Unop.LNot, Exp.Var x, _) -> ( match Mem.find_alias x mem with - | Some lv + | Some AliasTarget.Simple lv -> let v = Mem.find_heap lv mem in let itv_v = Itv.prune_eq (Val.get_itv v) Itv.false_sem in let v' = Val.modify_itv itv_v v in Mem.update_mem (PowLoc.singleton lv) v' mem + | Some AliasTarget.Empty lv + -> let v = Mem.find_heap lv mem in + let itv_v = Itv.prune_comp Binop.Ge (Val.get_itv v) Itv.one in + let v' = Val.modify_itv itv_v v in + Mem.update_mem (PowLoc.singleton lv) v' mem | None -> mem ) | _ @@ -340,7 +350,7 @@ module Make (CFG : ProcCfg.S) = struct | Exp.BinOp ((Binop.Gt as comp), Exp.Var x, e') | Exp.BinOp ((Binop.Le as comp), Exp.Var x, e') | Exp.BinOp ((Binop.Ge as comp), Exp.Var x, e') -> ( - match Mem.find_alias x mem with + match Mem.find_simple_alias x mem with | Some lv -> let v = Mem.find_heap lv mem in let v' = Val.prune_comp comp v (eval e' mem loc) in @@ -348,7 +358,7 @@ module Make (CFG : ProcCfg.S) = struct | None -> mem ) | Exp.BinOp (Binop.Eq, Exp.Var x, e') -> ( - match Mem.find_alias x mem with + match Mem.find_simple_alias x mem with | Some lv -> let v = Mem.find_heap lv mem in let v' = Val.prune_eq v (eval e' mem loc) in @@ -356,7 +366,7 @@ module Make (CFG : ProcCfg.S) = struct | None -> mem ) | Exp.BinOp (Binop.Ne, Exp.Var x, e') -> ( - match Mem.find_alias x mem with + match Mem.find_simple_alias x mem with | Some lv -> let v = Mem.find_heap lv mem in let v' = Val.prune_ne v (eval e' mem loc) in @@ -419,8 +429,8 @@ module Make (CFG : ProcCfg.S) = struct let get_matching_pairs : Tenv.t -> Val.t -> Val.t -> Typ.t -> Mem.astate -> Mem.astate - -> callee_ret_alias:Loc.t option - -> (Itv.Bound.t * Itv.Bound.t bottom_lifted * TraceSet.t) list * Loc.t option = + -> callee_ret_alias:AliasTarget.t option + -> (Itv.Bound.t * Itv.Bound.t bottom_lifted * TraceSet.t) list * AliasTarget.t option = fun tenv formal actual typ caller_mem callee_mem ~callee_ret_alias -> let get_itv v = Val.get_itv v in let get_offset v = v |> Val.get_array_blk |> ArrayBlk.offsetof in @@ -428,14 +438,18 @@ module Make (CFG : ProcCfg.S) = struct let get_field_name (fn, _, _) = fn in let append_field v fn = PowLoc.append_field (Val.get_all_locs v) fn in let deref_field v fn mem = Mem.find_heap_set (append_field v fn) mem in - let deref_ptr v mem = Mem.find_heap_set (Val.get_array_locs v) mem in + let deref_ptr v mem = + let array_locs = Val.get_array_locs v in + let locs = if PowLoc.is_empty array_locs then Val.get_pow_loc v else array_locs in + Mem.find_heap_set locs mem + in let ret_alias = ref None in let add_ret_alias v1 v2 = match callee_ret_alias with | Some ret_loc -> if PowLoc.is_singleton v1 && PowLoc.is_singleton v2 - && Loc.equal (PowLoc.min_elt v1) ret_loc - then ret_alias := Some (PowLoc.min_elt v2) + && AliasTarget.use (PowLoc.min_elt v1) ret_loc + then ret_alias := Some (AliasTarget.replace (PowLoc.min_elt v2) ret_loc) | None -> () in @@ -515,8 +529,9 @@ module Make (CFG : ProcCfg.S) = struct let get_subst_map : Tenv.t -> Procdesc.t -> (Exp.t * 'a) list -> Mem.astate -> Mem.astate - -> callee_ret_alias:Loc.t option -> Location.t - -> (Itv.Bound.t bottom_lifted Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t) * Loc.t option = + -> callee_ret_alias:AliasTarget.t option -> Location.t + -> (Itv.Bound.t bottom_lifted Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t) + * AliasTarget.t option = fun tenv callee_pdesc params caller_mem callee_entry_mem ~callee_ret_alias loc -> let add_pair (formal, typ) actual (l, ret_alias) = let formal = Mem.find_heap (Loc.of_pvar formal) callee_entry_mem in diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 8f6548402..af33dd5ce 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -13,7 +13,7 @@ codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, BUFFER_OVERRUN_L5, [C codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN_L1, [Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [42, 42] Size: [42, 42] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `my_vector_oob_Bad()` ] codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, [Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [max(0, s$4), s$5] Size: [max(0, s$4), s$5] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `int_vector_access_at()` ] codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]] -codetoanalyze/cpp/bufferoverrun/vector.cpp, call_safe_access4_Good_FP, 2, BUFFER_OVERRUN_L1, [Call,Call,Assignment,Call,Call,Assignment,Return,Call,Assignment,Call,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, 0]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, call_safe_access4_Good_FP, 2, BUFFER_OVERRUN_L1, [Call,Call,Assignment,Call,Call,Assignment,Return,Call,Assignment,Call,Call,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, 0]] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, BUFFER_OVERRUN_L4, [Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_L5, [Call,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN_L3, [Call,Call,Call,Assignment,Call,Call,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [1, 1] Size: [0, +oo]] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp index 9ca0d20e6..fe7f89bd3 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp @@ -121,3 +121,15 @@ void call_safe_access4_Good_FP() { std::vector v; safe_access4(v); } + +void safe_access5(std::vector v) { + if (v.empty()) { + } else { + v[0] = 1; + } +} + +void call_safe_access5_Good() { + std::vector v; + safe_access5(v); +}