[inferbo] Prune string length at "if(fgets(s, ...))"

Summary:
If the result of `fgets` is not-null, the length of `s` should be
bigger than or equal to 1.

Reviewed By: mbouaziz

Differential Revision: D13939994

fbshipit-source-id: 298fe33f4

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -301,6 +301,8 @@ module Val = struct
 
   let prune_ne_zero : t -> t = lift_prune1 Itv.prune_ne_zero
 
+  let prune_ge_one : t -> t = lift_prune1 Itv.prune_ge_one
+
   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
@@ -590,7 +592,8 @@ module MemPure = struct
 end
 
 module AliasTarget = struct
-  type t = Simple of Loc.t | Empty of Loc.t | Nullity of Loc.t [@@deriving compare]
+  type t = Simple of Loc.t | Empty of Loc.t | Fgets of Loc.t | Nullity of Loc.t
+  [@@deriving compare]
 
   let equal = [%compare.equal: t]
 
@@ -599,13 +602,17 @@ module AliasTarget = struct
         Loc.pp fmt l
     | Empty l ->
         F.fprintf fmt "empty(%a)" Loc.pp l
+    | Fgets l ->
+        F.fprintf fmt "fgets(%a)" Loc.pp l
     | Nullity l ->
         F.fprintf fmt "nullity(%a)" Loc.pp l
 
 
+  let fgets l = Fgets l
+
   let nullity l = Nullity l
 
-  let use l = function Simple l' | Empty l' | Nullity l' -> Loc.equal l l'
+  let use l = function Simple l' | Empty l' | Fgets l' | Nullity l' -> Loc.equal l l'
 
   let loc_map x ~f =
     match x with
@@ -613,6 +620,8 @@ module AliasTarget = struct
         Option.map (f l) ~f:(fun l -> Simple l)
     | Empty l ->
         Option.map (f l) ~f:(fun l -> Empty l)
+    | Fgets l ->
+        Option.map (f l) ~f:(fun l -> Fgets l)
     | Nullity l ->
         Option.map (f l) ~f:(fun l -> Nullity l)
 
@@ -728,6 +737,16 @@ module Alias = struct
         a
 
 
+  let fgets : Ident.t -> PowLoc.t -> t -> t =
+   fun id locs a ->
+    let a = PowLoc.fold (fun loc acc -> lift_map (AliasMap.store loc) acc) locs a in
+    match PowLoc.is_singleton_or_more locs with
+    | IContainer.Singleton loc ->
+        load id (AliasTarget.fgets loc) a
+    | _ ->
+        a
+
+
   let remove_temp : Ident.t -> t -> t = fun temp -> lift_map (AliasMap.remove temp)
 end
 
@@ -1125,7 +1144,7 @@ module MemReach = struct
     match Alias.find k m.alias with
     | Some (AliasTarget.Simple l) ->
         Some l
-    | Some (AliasTarget.Empty _ | AliasTarget.Nullity _) | None ->
+    | Some (AliasTarget.Empty _ | AliasTarget.Fgets _ | AliasTarget.Nullity _) | None ->
         None
 
 
@@ -1143,6 +1162,10 @@ module MemReach = struct
    fun formal loc m -> {m with alias= Alias.store_empty formal loc m.alias}
 
 
+  let fgets_alias : Ident.t -> PowLoc.t -> t -> t =
+   fun id locs m -> {m with alias= Alias.fgets id locs m.alias}
+
+
   let add_stack_loc : Loc.t -> t -> t = fun k m -> {m with stack_locs= StackLocs.add k m.stack_locs}
 
   let add_stack : Loc.t -> Val.t -> t -> t =
@@ -1405,6 +1428,10 @@ module Mem = struct
    fun formal loc -> map ~f:(MemReach.store_empty_alias formal loc)
 
 
+  let fgets_alias : Ident.t -> PowLoc.t -> t -> t =
+   fun id locs -> map ~f:(MemReach.fgets_alias id locs)
+
+
   let add_stack_loc : Loc.t -> t -> t = fun k -> map ~f:(MemReach.add_stack_loc k)
 
   let add_stack : Loc.t -> Val.t -> t -> t = fun k v -> map ~f:(MemReach.add_stack k v)

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -82,6 +82,7 @@ let fgets str_exp num_exp =
     |> Dom.Mem.update_mem (Sem.eval_locs str_exp mem) Dom.Val.Itv.zero_255
     |> ArrayBlk.fold update_strlen1 (Dom.Val.get_array_blk str_v)
     |> Dom.Mem.add_stack (Loc.of_id id) {str_v with itv= Itv.zero}
+    |> Dom.Mem.fgets_alias id (Dom.Val.get_all_locs str_v)
   and check {location; integer_type_widths} mem cond_set =
     BoUtils.Check.lindex_byte integer_type_widths ~array_exp:str_exp ~byte_index_exp:num_exp
       ~last_included:true mem location cond_set

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -307,7 +307,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 _ | AliasTarget.Nullity _) | None ->
+    | Some (AliasTarget.Empty _ | AliasTarget.Fgets _ | AliasTarget.Nullity _) | None ->
         Val.bot )
   | Exp.Lvar pvar ->
       Mem.find (Loc.of_pvar pvar) mem
@@ -466,6 +466,10 @@ module Prune = struct
           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.Fgets lv) ->
+          let strlen_loc = Loc.of_c_strlen lv in
+          let v' = Val.prune_ge_one (Mem.find strlen_loc mem) in
+          update_mem_in_prune strlen_loc v' astate
       | Some (AliasTarget.Nullity lv) ->
           let v = Mem.find lv mem in
           let v' = Val.prune_eq_zero v in
@@ -487,7 +491,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
-      | None ->
+      | Some (AliasTarget.Fgets _) | None ->
           astate )
     | _ ->
         astate

infer/tests/codetoanalyze/c/bufferoverrun/array_content.c

@@ -214,7 +214,7 @@ void strlen_malloc_2_Good_FP() {
   a[strlen(s)] = 0;
 }
 
-void fgets_null_check_Good_FP() {
+void fgets_null_check_Good() {
   char line[100];
   while (fgets(line, 100, stdin)) {
     line[strlen(line) - 1] = 0;

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

@@ -53,10 +53,8 @@ codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr_good_FP, 2, COND
 codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_ptr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/array_content.c, fgets_may_not_change_str_Bad, 9, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Array declaration,<Length trace>,Array declaration,Array access: Offset: [0, 5] Size: 5]
 codetoanalyze/c/bufferoverrun/array_content.c, fgets_may_not_change_str_Good_FP, 9, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Array declaration,<Length trace>,Array declaration,Array access: Offset: [4, 9] Size: 5]
-codetoanalyze/c/bufferoverrun/array_content.c, fgets_null_check_Bad, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Array declaration,<Length trace>,Array declaration,Array access: Offset: [-2, 97] Size: 100]
-codetoanalyze/c/bufferoverrun/array_content.c, fgets_null_check_Bad, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [<LHS trace>,Array declaration,Binary operation: ([0, 99] - 2):unsigned64]
-codetoanalyze/c/bufferoverrun/array_content.c, fgets_null_check_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Array declaration,<Length trace>,Array declaration,Array access: Offset: [-1, 98] Size: 100]
-codetoanalyze/c/bufferoverrun/array_content.c, fgets_null_check_Good_FP, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [<LHS trace>,Array declaration,Binary operation: ([0, 99] - 1):unsigned64]
+codetoanalyze/c/bufferoverrun/array_content.c, fgets_null_check_Bad, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Array declaration,<Length trace>,Array declaration,Array access: Offset: [-1, 97] Size: 100]
+codetoanalyze/c/bufferoverrun/array_content.c, fgets_null_check_Bad, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [<LHS trace>,Array declaration,Binary operation: ([1, 99] - 2):unsigned64]
 codetoanalyze/c/bufferoverrun/array_content.c, literal_string2_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/array_content.c, literal_string2_bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: [0, 111] Size: 1]
 codetoanalyze/c/bufferoverrun/array_content.c, literal_string_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]