[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/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;

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

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 "@[<v 0>Logical Variables :@,"; *)
       F.fprintf fmt "@[<hov 2>{ @," ;
       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)
 

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

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]]

infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp

@@ -121,3 +121,15 @@ void call_safe_access4_Good_FP() {
   std::vector<int> v;
   safe_access4(v);
 }
+
+void safe_access5(std::vector<int> v) {
+  if (v.empty()) {
+  } else {
+    v[0] = 1;
+  }
+}
+
+void call_safe_access5_Good() {
+  std::vector<int> v;
+  safe_access5(v);
+}