[inferbo] Pruning by vector::size

Summary:
It enables pruning of vector's size when the return value of the function call of `vector::size` is pruned.

Depends on D16687167

Reviewed By: ezgicicek

Differential Revision: D16687225

fbshipit-source-id: 793a21b3a

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -681,6 +681,7 @@ module AliasTarget = struct
     | Simple of Loc.t
     | SimplePlusA of Loc.t * IntLit.t
     | Empty of Loc.t
+    | Size of Loc.t
     | Fgets of Loc.t
     | Nullity of Loc.t
   [@@deriving compare]
@@ -695,6 +696,8 @@ module AliasTarget = struct
         else F.fprintf fmt "%a+%a" Loc.pp l IntLit.pp i
     | Empty l ->
         F.fprintf fmt "empty(%a)" Loc.pp l
+    | Size l ->
+        F.fprintf fmt "size(%a)" Loc.pp l
     | Fgets l ->
         F.fprintf fmt "fgets(%a)" Loc.pp l
     | Nullity l ->
@@ -705,7 +708,10 @@ module AliasTarget = struct
 
   let nullity l = Nullity l
 
-  let get_loc = function Simple l | SimplePlusA (l, _) | Empty l | Fgets l | Nullity l -> l
+  let get_loc = function
+    | Simple l | SimplePlusA (l, _) | Empty l | Size l | Fgets l | Nullity l ->
+        l
+
 
   let use l x = Loc.equal l (get_loc x)
 
@@ -717,6 +723,8 @@ module AliasTarget = struct
         Option.map (f l) ~f:(fun l -> SimplePlusA (l, i))
     | Empty l ->
         Option.map (f l) ~f:(fun l -> Empty l)
+    | Size l ->
+        Option.map (f l) ~f:(fun l -> Size l)
     | Fgets l ->
         Option.map (f l) ~f:(fun l -> Fgets l)
     | Nullity l ->
@@ -1346,10 +1354,15 @@ module MemReach = struct
         Some (l, None)
     | Some (AliasTarget.SimplePlusA (l, i)) ->
         Some (l, Some i)
-    | Some (AliasTarget.Empty _ | AliasTarget.Fgets _ | AliasTarget.Nullity _) | None ->
+    | Some (AliasTarget.Empty _ | AliasTarget.Size _ | AliasTarget.Fgets _ | AliasTarget.Nullity _)
+    | 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
+
+
   let find_ret_alias : _ t0 -> AliasTarget.t option = fun m -> Alias.find_ret m.alias
 
   let load_alias : Ident.t -> AliasTarget.t -> t -> t =
@@ -1656,6 +1669,10 @@ module Mem = struct
    fun k -> f_lift_default ~default:None (MemReach.find_simple_alias k)
 
 
+  let find_size_alias : Ident.t -> _ t0 -> Loc.t option =
+   fun k -> f_lift_default ~default:None (MemReach.find_size_alias k)
+
+
   let find_ret_alias : _ t0 -> AliasTarget.t option =
    fun m -> f_lift_default ~default:None MemReach.find_ret_alias m
 
@@ -1672,6 +1689,10 @@ module Mem = struct
    fun id loc -> load_alias id (AliasTarget.Empty loc)
 
 
+  let load_size_alias : Ident.t -> Loc.t -> t -> t =
+   fun id loc -> load_alias id (AliasTarget.Size loc)
+
+
   let store_simple_alias : Loc.t -> Exp.t -> t -> t =
    fun loc e -> map ~f:(MemReach.store_simple_alias loc e)
 

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -644,6 +644,10 @@ module StdBasicString = struct
 end
 
 module StdVector = struct
+  let deref_of vec_exp mem =
+    Dom.Val.get_all_locs (Dom.Mem.find_set (Sem.eval_locs vec_exp mem) mem)
+
+
   let get_classname vec_typ =
     match vec_typ.Typ.desc with
     | Typ.Tptr (vec_typ, _) -> (
@@ -695,9 +699,7 @@ module StdVector = struct
         let classname = get_classname vec_typ in
         PowLoc.append_field vec_locs ~fn:(BufferOverrunField.cpp_vector_elem ~classname elt_typ)
       in
-      let deref_of_src =
-        Dom.Mem.find_set (Sem.eval_locs src_exp mem) mem |> Dom.Val.get_all_locs
-      in
+      let deref_of_src = deref_of src_exp mem in
       mem
       |> Dom.Mem.update_mem vec_locs (Dom.Val.of_pow_loc ~traces deref_of_vec)
       |> Dom.Mem.update_mem deref_of_vec (Dom.Mem.find_set deref_of_src mem)
@@ -707,19 +709,15 @@ module StdVector = struct
 
   let at vec_exp index_exp =
     let exec {pname; location} ~ret:(id, _) mem =
-      let deref_of_vec = Dom.Mem.find_set (Sem.eval_locs vec_exp mem) mem in
       let array_v =
-        let locs = Dom.Val.get_all_locs deref_of_vec in
+        let locs = deref_of vec_exp mem in
         if PowLoc.is_bot locs then Dom.Val.unknown_from ~callee_pname:(Some pname) ~location
         else Dom.Mem.find_set locs mem
       in
       Dom.Mem.add_stack (Loc.of_id id) array_v mem
     and check {location; integer_type_widths} mem cond_set =
       let idx = Sem.eval integer_type_widths index_exp mem in
-      let arr =
-        let deref_of_vec = Dom.Mem.find_set (Sem.eval_locs vec_exp mem) mem in
-        Dom.Mem.find_set (Dom.Val.get_all_locs deref_of_vec) mem
-      in
+      let arr = Dom.Mem.find_set (deref_of vec_exp mem) mem in
       let relation = Dom.Mem.get_relation mem in
       let latest_prune = Dom.Mem.get_latest_prune mem in
       BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp:None ~relation ~is_plus:true
@@ -728,11 +726,16 @@ module StdVector = struct
     {exec; check}
 
 
+  let get_size vec_exp mem = eval_array_locs_length (deref_of vec_exp mem) mem
+
   let size vec_exp =
     let exec _ ~ret:(id, _) mem =
-      let deref_of_vec = Dom.Mem.find_set (Sem.eval_locs vec_exp mem) mem in
-      let size_v = eval_array_locs_length (Dom.Val.get_all_locs deref_of_vec) mem in
-      Dom.Mem.add_stack (Loc.of_id id) size_v mem
+      let mem = Dom.Mem.add_stack (Loc.of_id id) (get_size vec_exp mem) mem in
+      match PowLoc.is_singleton_or_more (deref_of vec_exp mem) with
+      | IContainer.Singleton loc ->
+          Dom.Mem.load_size_alias id loc mem
+      | IContainer.Empty | IContainer.More ->
+          mem
     in
     {exec; check= no_check}
 end

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -310,6 +310,7 @@ let rec eval_arr : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Val.t =
         Mem.find loc mem
     | Some
         ( AliasTarget.SimplePlusA _
+        | AliasTarget.Size _
         | AliasTarget.Empty _
         | AliasTarget.Fgets _
         | AliasTarget.Nullity _ )
@@ -512,7 +513,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 _) | None ->
+      | Some (AliasTarget.SimplePlusA _ | AliasTarget.Size _) | None ->
           astate )
     | Exp.UnOp (Unop.LNot, Exp.Var x, _) -> (
       match Mem.find_alias x mem with
@@ -529,59 +530,68 @@ 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.Fgets _) | None ->
+      | Some (AliasTarget.SimplePlusA _ | AliasTarget.Size _ | AliasTarget.Fgets _) | None ->
           astate )
     | _ ->
         astate
 
 
-  let rec prune_binop_left : Typ.IntegerWidths.t -> Exp.t -> t -> t =
-   fun integer_type_widths e ({mem} as astate) ->
-    match e with
-    | Exp.BinOp (comp, Exp.Cast (_, e1), e2) ->
-        prune_binop_left integer_type_widths (Exp.BinOp (comp, e1, e2)) astate
-    | Exp.BinOp ((Binop.Lt as comp), Exp.Var x, e')
-    | 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_simple_alias x mem with
-      | Some (lv, opt_i) ->
-          let lhs = Mem.find lv mem in
-          let rhs =
-            let v' = eval integer_type_widths e' mem in
-            Option.value_map opt_i ~default:v' ~f:(fun i -> Val.minus_a v' (Val.of_int_lit i))
-          in
-          let v = Val.prune_comp comp lhs rhs in
-          let pruning_exp = PruningExp.make comp ~lhs ~rhs in
-          update_mem_in_prune lv v ~pruning_exp astate
-      | None ->
-          astate )
-    | Exp.BinOp (Binop.Eq, Exp.Var x, e') -> (
-      match Mem.find_simple_alias x mem with
-      | Some (lv, opt_i) ->
-          let lhs = Mem.find lv mem in
-          let rhs =
-            let v' = eval integer_type_widths e' mem in
-            Option.value_map opt_i ~default:v' ~f:(fun i -> Val.minus_a v' (Val.of_int_lit i))
-          in
-          let v = Val.prune_eq lhs rhs in
-          let pruning_exp = PruningExp.make Binop.Eq ~lhs ~rhs in
-          update_mem_in_prune lv v ~pruning_exp astate
-      | None ->
-          astate )
-    | Exp.BinOp (Binop.Ne, Exp.Var x, e') -> (
-      match Mem.find_simple_alias x mem with
-      | Some (lv, opt_i) ->
+  let gen_prune_alias_functions ~prune_alias_core integer_type_widths comp x e astate =
+    let val_prune =
+      match comp with
+      | Binop.Lt | Binop.Gt | Binop.Le | Binop.Ge ->
+          Val.prune_comp comp
+      | Binop.Eq ->
+          Val.prune_eq
+      | Binop.Ne ->
+          Val.prune_ne
+      | _ ->
+          assert false
+    in
+    let make_pruning_exp = PruningExp.make comp in
+    prune_alias_core ~val_prune ~make_pruning_exp integer_type_widths x e astate
+
+
+  let prune_simple_alias =
+    let prune_alias_core ~val_prune ~make_pruning_exp integer_type_widths x e ({mem} as astate) =
+      Option.value_map (Mem.find_simple_alias x mem) ~default:astate ~f:(fun (lv, opt_i) ->
           let lhs = Mem.find lv mem in
           let rhs =
-            let v' = eval integer_type_widths e' mem in
+            let v' = eval integer_type_widths e mem in
             Option.value_map opt_i ~default:v' ~f:(fun i -> Val.minus_a v' (Val.of_int_lit i))
           in
-          let v = Val.prune_ne lhs rhs in
-          let pruning_exp = PruningExp.make Binop.Ne ~lhs ~rhs in
-          update_mem_in_prune lv v ~pruning_exp astate
-      | None ->
-          astate )
+          let v = val_prune lhs rhs in
+          let pruning_exp = make_pruning_exp ~lhs ~rhs in
+          update_mem_in_prune lv v ~pruning_exp astate )
+    in
+    gen_prune_alias_functions ~prune_alias_core
+
+
+  let prune_size_alias =
+    let prune_alias_core ~val_prune ~make_pruning_exp integer_type_widths x e ({mem} as astate) =
+      Option.value_map (Mem.find_size_alias x mem) ~default:astate ~f:(fun lv ->
+          let array_v = Mem.find lv mem in
+          let size = Val.get_array_blk array_v |> ArrayBlk.sizeof |> Val.of_itv in
+          let rhs = eval integer_type_widths e mem in
+          let size' = val_prune size rhs in
+          let array_v' = Val.set_array_length Location.dummy ~length:size' array_v in
+          let pruning_exp = make_pruning_exp ~lhs:size' ~rhs in
+          update_mem_in_prune lv array_v' ~pruning_exp astate )
+    in
+    gen_prune_alias_functions ~prune_alias_core
+
+
+  let rec prune_binop_left : Typ.IntegerWidths.t -> Exp.t -> t -> t =
+   fun integer_type_widths e astate ->
+    match e with
+    | Exp.BinOp (comp, Exp.Cast (_, e1), e2) ->
+        prune_binop_left integer_type_widths (Exp.BinOp (comp, e1, e2)) astate
+    | Exp.BinOp
+        (((Binop.Lt | Binop.Gt | Binop.Le | Binop.Ge | Binop.Eq | Binop.Ne) as comp), Exp.Var x, e')
+      ->
+        astate
+        |> prune_simple_alias integer_type_widths comp x e'
+        |> prune_size_alias integer_type_widths comp x e'
     | Exp.BinOp
         ( ((Binop.Lt | Binop.Gt | Binop.Le | Binop.Ge | Binop.Eq | Binop.Ne) as comp)
         , Exp.BinOp (Binop.PlusA t, e1, e2)

infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp

@@ -110,7 +110,6 @@ codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, no_b
 codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_call_safe_access2_Good, 2, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Array declaration,Assignment,Call,Parameter `*v->vector_elem`,Allocation: Length: 0 by call to `safe_access2` ]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_call_safe_access4_Good, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `*v->vector_elem`,Array access: Offset: 0 Size: 0 by call to `safe_access4` ]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_call_safe_access5_Good, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `*v->vector_elem`,Array access: Offset: 0 Size: 0 by call to `safe_access5` ]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_call_safe_access_Good, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `*v->vector_elem`,Array access: Offset: 9 Size: 5 by call to `safe_access` ]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_data_Good, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: std::vector<int,std::allocator<int>>::data,Assignment,Array access: Offset: [-oo, +oo] (⇐ [-oo, +oo] + 4) Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_push_back_Good, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 0 Size: 0]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_reserve_Good, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 0 Size: 0]

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

@@ -64,7 +64,7 @@ void safe_access(std::vector<int> v) {
   }
 }
 
-void FP_call_safe_access_Good() {
+void call_safe_access_Good() {
   std::vector<int> v(5, 0);
   safe_access(v);
 }