From bd136ac24e9315e4c709f0a3c29e62a5c1ff8bbf Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Wed, 6 Feb 2019 23:14:10 -0800 Subject: [PATCH] [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 --- .../src/bufferoverrun/bufferOverrunDomain.ml | 33 +++++++++++++++++-- .../src/bufferoverrun/bufferOverrunModels.ml | 1 + .../bufferoverrun/bufferOverrunSemantics.ml | 8 +++-- .../c/bufferoverrun/array_content.c | 2 +- .../codetoanalyze/c/bufferoverrun/issues.exp | 6 ++-- 5 files changed, 40 insertions(+), 10 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index f88491bc4..b605a8527 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/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) diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index fb01dd1c5..357ab0d00 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 248b9140b..92d9f013d 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/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 diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c b/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c index 980fe874a..11c89cf32 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c +++ b/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; diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 6311bf755..a76ecb190 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/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, [,Array declaration,,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, [,Array declaration,,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, [,Array declaration,,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, [,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, [,Array declaration,,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, [,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, [,Array declaration,,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, [,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, [,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]