[inferbo] Add model of String::empty

Reviewed By: mbouaziz

Differential Revision: D13547863

fbshipit-source-id: 9e3497873

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -265,6 +265,11 @@ module Val = struct
    fun f x -> warn_against_pruning_multiple_values {x with itv= f x.itv}
 
 
+  let lift_prune_length1 : (Itv.t -> Itv.t) -> t -> t =
+   fun f x ->
+    warn_against_pruning_multiple_values {x with arrayblk= ArrayBlk.transform_length ~f x.arrayblk}
+
+
   let lift_prune2 :
       (Itv.t -> Itv.t -> Itv.t) -> (ArrayBlk.t -> ArrayBlk.t -> ArrayBlk.t) -> t -> t -> t =
    fun f g x y ->
@@ -282,6 +287,10 @@ module Val = struct
 
   let prune_ne_zero : t -> t = lift_prune1 Itv.prune_ne_zero
 
+  let prune_length_eq_zero : t -> t = lift_prune_length1 Itv.prune_eq_zero
+
+  let prune_length_ge_one : t -> t = lift_prune_length1 Itv.prune_ge_one
+
   let prune_comp : Binop.t -> t -> t -> t =
    fun c -> lift_prune2 (Itv.prune_comp c) (ArrayBlk.prune_comp c)
 
@@ -546,15 +555,22 @@ module MemPure = struct
 end
 
 module AliasTarget = struct
-  type t = Simple of Loc.t | Empty of Loc.t [@@deriving compare]
+  type t = Simple of Loc.t | Empty of Loc.t | Nullity 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 pp fmt = function
+    | Simple l ->
+        Loc.pp fmt l
+    | Empty l ->
+        F.fprintf fmt "empty(%a)" Loc.pp l
+    | Nullity l ->
+        F.fprintf fmt "nullity(%a)" Loc.pp l
+
 
-  let of_empty l = Empty l
+  let nullity l = Nullity l
 
-  let use l = function Simple l' | Empty l' -> Loc.equal l l'
+  let use l = function Simple l' | Empty l' | Nullity l' -> Loc.equal l l'
 
   let loc_map x ~f =
     match x with
@@ -562,6 +578,8 @@ module AliasTarget = struct
         Option.map (f l) ~f:(fun l -> Simple l)
     | Empty l ->
         Option.map (f l) ~f:(fun l -> Empty l)
+    | Nullity l ->
+        Option.map (f l) ~f:(fun l -> Nullity l)
 
 
   let ( <= ) ~lhs ~rhs = equal lhs rhs
@@ -574,20 +592,24 @@ module AliasTarget = struct
   let widen ~prev ~next ~num_iters:_ = join prev next
 end
 
-(* Relations between values of logical variables(registers) and
+(* Relations between values of logical variables(registers) and program variables
-   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.Simple relation": Since Sil distinguishes logical and
+   "AliasTarget.Empty relation": For pruning vector.length with vector::empty() results, we adopt a
-   program variables, we need a relation for pruning values of program
+   specific relation between %r and v, where %r=v.empty().  So, if %r!=0, v's array length
-   variables.  For example, a C statement "if(x){...}" is translated
+   ([v.length]) is pruned by v.length=0.  On the other hand, if %r==0, v's array length is pruned by
-   to "%r=load(x); if(%r){...}" in Sil.  At the load statement, we
+   v.length>=1.
-   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
+   "AliasTarget.Nullity relation": For pruning vector.length with vector::empty() results, we adopt
-   vector::empty() results, we adopt a specific relation between %r
+   a specific relation between %r and i, where %r=v.empty() and i=v.length.  So, if %r!=0, i is
-   and x, where %r=v.empty() and x=v.size.  So, if %r!=0, x is pruned
+   pruned by i=0.  On the other hand, if %r==0, i is pruned by i>=1.  This is similar to the
-   by x=0.  On the other hand, if %r==0, x is pruned by x>=1.  *)
+   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)
 
@@ -666,7 +688,7 @@ module Alias = struct
     let locs = Val.get_all_locs formal in
     match PowLoc.is_singleton_or_more locs with
     | IContainer.Singleton loc ->
-        {a with ret= AliasRet.v (AliasTarget.of_empty loc)}
+        {a with ret= AliasRet.v (AliasTarget.nullity loc)}
     | _ ->
         a
 
@@ -921,7 +943,7 @@ module MemReach = struct
     match Alias.find k m.alias with
     | Some (AliasTarget.Simple l) ->
         Some l
-    | Some (AliasTarget.Empty _) | None ->
+    | Some (AliasTarget.Empty _ | AliasTarget.Nullity _) | None ->
         None
 
 
@@ -1166,6 +1188,10 @@ module Mem = struct
    fun id loc -> load_alias id (AliasTarget.Simple loc)
 
 
+  let load_empty_alias : Ident.t -> Loc.t -> t -> t =
+   fun id loc -> load_alias id (AliasTarget.Empty 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

@@ -352,6 +352,23 @@ module StdBasicString = struct
       Dom.Mem.update_mem tgt_locs v mem
     in
     {exec; check= no_check}
+
+
+  let empty e =
+    let exec {integer_type_widths} ~ret:(ret_id, _) mem =
+      let v = Sem.eval integer_type_widths e mem in
+      let traces = Dom.Val.get_traces v in
+      let size = ArrayBlk.sizeof (Dom.Val.get_array_blk v) in
+      let empty = Dom.Val.of_itv ~traces (Itv.of_bool (Itv.le_sem size Itv.zero)) in
+      let mem = Dom.Mem.add_stack (Loc.of_id ret_id) empty mem in
+      match e with
+      | Exp.Var id ->
+          Option.value_map (Dom.Mem.find_simple_alias id mem) ~default:mem ~f:(fun l ->
+              Dom.Mem.load_empty_alias ret_id l mem )
+      | _ ->
+          mem
+    in
+    {exec; check= no_check}
 end
 
 (* Java's Collections are represented like arrays. But we don't care about the elements.
@@ -532,6 +549,7 @@ module Call = struct
         $+ capt_exp_of_prim_typ (Typ.mk (Typ.Tptr (Typ.mk (Typ.Tint Typ.IChar), Pk_pointer)))
         $+ capt_exp_of_prim_typ (Typ.mk (Typ.Tint Typ.size_t))
         $--> StdBasicString.constructor_from_char_ptr
+      ; -"std" &:: "basic_string" &:: "empty" $ capt_exp $--> StdBasicString.empty
       ; -"std" &:: "basic_string" &::.*--> no_model
       ; +PatternMatch.implements_collection
         &:: "get" <>$ capt_var_exn $+ capt_exp $--> Collection.get_or_set_at_index

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -302,7 +302,7 @@ let rec eval_arr : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Val.t =
     match Mem.find_alias id mem with
     | Some (AliasTarget.Simple loc) ->
         Mem.find loc mem
-    | Some (AliasTarget.Empty _) | None ->
+    | Some (AliasTarget.Empty _ | AliasTarget.Nullity _) | None ->
         Val.bot )
   | Exp.Lvar pvar ->
       Mem.find (Loc.of_pvar pvar) mem
@@ -446,6 +446,10 @@ module Prune = struct
           let v' = Val.prune_ne_zero v in
           update_mem_in_prune lv v' astate
       | Some (AliasTarget.Empty lv) ->
+          let v = Mem.find lv mem in
+          let v' = Val.prune_length_eq_zero v in
+          update_mem_in_prune lv v' astate
+      | Some (AliasTarget.Nullity lv) ->
           let v = Mem.find lv mem in
           let v' = Val.prune_eq_zero v in
           update_mem_in_prune lv v' astate
@@ -458,6 +462,10 @@ module Prune = struct
           let v' = Val.prune_eq_zero v in
           update_mem_in_prune lv v' astate
       | Some (AliasTarget.Empty lv) ->
+          let v = Mem.find lv mem in
+          let v' = Val.prune_length_ge_one v in
+          update_mem_in_prune lv v' astate
+      | Some (AliasTarget.Nullity lv) ->
           let v = Mem.find 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

infer/src/bufferoverrun/itv.ml

@@ -397,6 +397,8 @@ module ItvPure = struct
     if is_invalid (l, u) then NonBottom x else if Bound.eq l u then prune_diff x l else NonBottom x
 
 
+  let prune_ge_one : t -> t bottom_lifted = fun x -> prune_comp Binop.Ge x one
+
   let get_symbols : t -> SymbolSet.t =
    fun (l, u) -> SymbolSet.union (Bound.get_symbols l) (Bound.get_symbols u)
 
@@ -596,6 +598,8 @@ let prune_eq_zero : t -> t = bind1 ItvPure.prune_eq_zero
 
 let prune_ne_zero : t -> t = bind1 ItvPure.prune_ne_zero
 
+let prune_ge_one : t -> t = bind1 ItvPure.prune_ge_one
+
 let prune_comp : Binop.t -> t -> t -> t = fun comp -> bind2 (ItvPure.prune_comp comp)
 
 let prune_eq : t -> t -> t = bind2 ItvPure.prune_eq

infer/src/bufferoverrun/itv.mli

@@ -203,6 +203,8 @@ val prune_eq_zero : t -> t
 
 val prune_ne_zero : t -> t
 
+val prune_ge_one : t -> t
+
 val prune_comp : Binop.t -> t -> t -> t
 
 val prune_eq : t -> t -> t

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

@@ -75,6 +75,8 @@ codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int3_Bad, 3, INFERBO_ALLOC_IS
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int3_Bad, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [<RHS trace>,Assignment,Binary operation: (4 × 18446744073709551615):unsigned64]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, normal_array_bo, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 42 Size: 42]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 42 Size: 42]
+codetoanalyze/cpp/bufferoverrun/std_string.cpp, empty_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
+codetoanalyze/cpp/bufferoverrun/std_string.cpp, empty_Good, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, last_char1_Bad, 3, BUFFER_OVERRUN_R2, no_bucket, ERROR, [<Offset trace>,Risky value from: snprintf,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 1024]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, last_char1_Bad, 3, INTEGER_OVERFLOW_R2, no_bucket, ERROR, [<LHS trace>,Risky value from: snprintf,Assignment,Binary operation: ([-oo, +oo] - 1):signed32]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, last_char2_Bad, 6, BUFFER_OVERRUN_R2, no_bucket, ERROR, [<Offset trace>,Risky value from: vsnprintf,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 1024]

infer/tests/codetoanalyze/cpp/bufferoverrun/std_string.cpp

@@ -70,3 +70,19 @@ std::string to_string2_Good(const char* fmt, ...) {
   }
   return std::string(buf, n);
 }
+
+void empty_Good(std::string s) {
+  if (s.empty()) {
+    if (!s.empty()) {
+      int a[10];
+      a[10] = 0;
+    }
+  }
+}
+
+void empty_Bad(std::string s) {
+  if (s.empty()) {
+    int a[10];
+    a[10] = 0;
+  }
+}