[inferbo] Top for unanalyzed variables (e.g., global variables)

Summary: This commit fixes a problem that the buffer overrun checker incorrectly stops when a global variable (bottom) is involved in control flow. In the new version, abstract memories return Top for unanalyzed abstract variables. Reviewed By: mbouaziz Differential Revision: D5016447 fbshipit-source-id: 5132448
8 years ago · 984a81413a
parent d446f0f800
commit 984a81413a
7 changed files with 504 additions and 469 deletions
--- a/infer/src/bufferoverrun/absLoc.ml
+++ b/infer/src/bufferoverrun/absLoc.ml
@ -25,8 +25,10 @@ struct
    | Var of Var.t
    | Allocsite of Allocsite.t
    | Field of t * Fieldname.t
+    | Unknown
      [@@deriving compare]

+  let unknown = Unknown
  let rec pp fmt = function
    | Var v ->
      Var.pp F.str_formatter v;
@ -36,6 +38,7 @@ struct
      else F.fprintf fmt "%s" s
    | Allocsite a -> Allocsite.pp fmt a
    | Field (l, f) -> F.fprintf fmt "%a.%a" pp l Fieldname.pp f
+    | Unknown -> F.fprintf fmt "Unknown"
  let is_var = function Var _ -> true | _ -> false
  let is_logical_var = function
    | Var (Var.LogicalVar _) -> true
@ -59,7 +62,10 @@ struct
  let bot = empty
  let is_bot = is_empty

+  let unknown = singleton Loc.unknown
  let of_pvar pvar = singleton (Loc.of_pvar pvar)
  let of_id id = singleton (Loc.of_id id)
-  let append_field ploc fn = fold (fun l -> add (Loc.append_field l fn)) ploc empty
+  let append_field ploc fn =
+    if is_bot ploc then singleton Loc.unknown
+    else fold (fun l -> add (Loc.append_field l fn)) ploc empty
 end
--- a/infer/src/bufferoverrun/bufferOverrunChecker.ml
+++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml
@ -70,6 +70,14 @@ struct
    = fun pname ret params node mem ->
      model_malloc pname ret (List.tl_exn params) node mem

+  let model_fgetc : (Ident.t * Typ.t) option -> Dom.Mem.astate -> Dom.Mem.astate
+    = fun ret mem ->
+      match ret with
+      | Some (id, _) ->
+        let itv = Itv.make (Itv.Bound.of_int (-1)) Itv.Bound.PInf in
+        Dom.Mem.add_stack (Loc.of_id id) (Dom.Val.of_itv itv) mem
+      | _ -> mem
+
  let model_natual_itv : (Ident.t * Typ.t) option -> Dom.Mem.astate -> Dom.Mem.astate
    = fun ret mem ->
      match ret with
@ -103,8 +111,8 @@ struct
      | "malloc"
      | "__new_array" -> model_malloc pname ret params node mem
      | "realloc" -> model_realloc pname ret params node mem
-      | "strlen"
-      | "fgetc" -> model_natual_itv ret mem
+      | "strlen" -> model_natual_itv ret mem
+      | "fgetc" -> model_fgetc ret mem
      | "infer_print" -> model_infer_print params mem loc
      | _ -> model_unknown_itv ret mem

@ -148,7 +156,7 @@ struct
      in
      let decl_fld (mem, sym_num) (fn, typ, _) =
        let loc =
-          mem |> Dom.Mem.find_heap loc |> Dom.Val.get_all_locs |> PowLoc.choose
+          mem |> Dom.Mem.find_heap loc |> Dom.Val.get_array_locs |> PowLoc.choose
        in
        let field = Loc.append_field loc fn in
        match typ.Typ.desc with
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml
@ -29,30 +29,30 @@ struct
      trace : trace;
      id : string }
      [@@deriving compare]
-and trace = Intra of Typ.Procname.t
+  and trace = Intra of Typ.Procname.t
            | Inter of Typ.Procname.t * Typ.Procname.t * Location.t
-[@@deriving compare]
+                    [@@deriving compare]

-and astate = t
+  and astate = t

-let set_size_pos : t -> t
+  let set_size_pos : t -> t
    = fun c ->
      if Itv.Bound.lt (Itv.lb c.size) Itv.Bound.zero
      then { c with size = Itv.make Itv.Bound.zero (Itv.ub c.size) }
      else c

-let string_of_location : Location.t -> string
+  let string_of_location : Location.t -> string
    = fun loc ->
      let fname = SourceFile.to_string loc.Location.file in
      let pos = Location.to_string loc in
      F.fprintf F.str_formatter "%s:%s" fname pos;
      F.flush_str_formatter ()

-let pp_location : F.formatter -> t -> unit
+  let pp_location : F.formatter -> t -> unit
    = fun fmt c ->
      F.fprintf fmt "%s" (string_of_location c.loc)

-let pp : F.formatter -> t -> unit
+  let pp : F.formatter -> t -> unit
    = fun fmt c ->
      let c = set_size_pos c in
      if Config.bo_debug <= 1 then
@ -65,30 +65,31 @@ let pp : F.formatter -> t -> unit
            Itv.pp c.idx Itv.pp c.size pp_location c pname (string_of_location loc)
        | Intra _ -> F.fprintf fmt "%a < %a at %a" Itv.pp c.idx Itv.pp c.size pp_location c

-let get_location : t -> Location.t
+  let get_location : t -> Location.t
    = fun c -> c.loc

-let get_trace : t -> trace
+  let get_trace : t -> trace
    = fun c -> c.trace

-let get_proc_name : t -> Typ.Procname.t
+  let get_proc_name : t -> Typ.Procname.t
    = fun c -> c.proc_name

-let make : Typ.Procname.t -> Location.t -> string -> idx:Itv.t -> size:Itv.t -> t
+  let make : Typ.Procname.t -> Location.t -> string -> idx:Itv.t -> size:Itv.t -> t
    = fun proc_name loc id ~idx ~size ->
      { proc_name; idx; size; loc; id ; trace = Intra proc_name }

-let filter1 : t -> bool
+  let filter1 : t -> bool
    = fun c ->
      Itv.eq c.idx Itv.top || Itv.eq c.size Itv.top
      || Itv.Bound.eq (Itv.lb c.idx) Itv.Bound.MInf
      || Itv.Bound.eq (Itv.lb c.size) Itv.Bound.MInf
      || (Itv.eq c.idx Itv.nat && Itv.eq c.size Itv.nat)

-let filter2 : t -> bool
+  let filter2 : t -> bool
    = fun c ->
-    (not (Itv.is_finite c.idx) || not (Itv.is_finite c.size)) (* basically, alarms involving infinity are filtered *)
-    &&                                                        (* except the following cases:                       *)
+      (* basically, alarms involving infinity are filtered *)
+      (not (Itv.is_finite c.idx) || not (Itv.is_finite c.size))
+      &&                                                        (* except the following cases *)
      not ((Itv.Bound.is_not_infty (Itv.lb c.idx) &&            (* idx non-infty lb < 0 *)
            Itv.Bound.lt (Itv.lb c.idx) Itv.Bound.zero)
           ||
@ -104,8 +105,8 @@ let filter2 : t -> bool
           (Itv.Bound.is_not_infty (Itv.ub c.idx) &&            (* idx non-infty ub > size ub *)
            (Itv.Bound.gt (Itv.ub c.idx) (Itv.ub c.size))))

-(* check buffer overrun and return its confidence *)
-let check : t -> string option
+  (* check buffer overrun and return its confidence *)
+  let check : t -> string option
    = fun c ->
      (* idx = [il, iu], size = [sl, su], we want to check that 0 <= idx < size *)
      let c' = set_size_pos c in (* if sl < 0, use sl' = 0 *)
@ -135,10 +136,10 @@ let check : t -> string option
      else
        Some Localise.BucketLevel.b2

-let invalid : t -> bool
+  let invalid : t -> bool
    = fun x -> Itv.invalid x.idx || Itv.invalid x.size

-let to_string : t -> string
+  let to_string : t -> string
    = fun c ->
      let c = set_size_pos c in
      "Offset: " ^ Itv.to_string c.idx ^ " Size: " ^ Itv.to_string c.size
@ -149,7 +150,7 @@ let to_string : t -> string
        ^ MF.monospaced_to_string (Typ.Procname.to_string pname ^ "()") ^ " "
      | Intra _ -> "")

-let subst : t -> Itv.Bound.t Itv.SubstMap.t -> Typ.Procname.t -> Typ.Procname.t -> Location.t -> t
+  let subst : t -> Itv.Bound.t Itv.SubstMap.t -> Typ.Procname.t -> Typ.Procname.t -> Location.t -> t
    = fun c subst_map caller_pname callee_pname loc ->
      if Itv.is_symbolic c.idx || Itv.is_symbolic c.size then
        { c with idx = Itv.subst c.idx subst_map;
@ -277,6 +278,9 @@ struct
  let of_int : int -> t
    = fun n -> { bot with itv = Itv.of_int n }

+  let of_itv : Itv.t -> t
+    = fun itv -> { bot with itv }
+
  let of_pow_loc : PowLoc.t -> t
    = fun x -> { bot with powloc = x }

@ -496,7 +500,7 @@ struct
  let find : Loc.t -> astate -> Val.t
    = fun l m ->
      try find l m with
-      | Not_found -> Val.bot
+      | Not_found -> Val.top_itv

  let find_set : PowLoc.t -> astate -> Val.t
    = fun locs mem ->
@ -545,10 +549,10 @@ struct
        match M.find k rhs with
        | v' -> Pvar.equal v v'
        | exception Not_found -> false
-      in
-      M.for_all is_in_rhs lhs
+in
+M.for_all is_in_rhs lhs

-  let join : t -> t -> t
+let join : t -> t -> t
  = fun x y ->
    let join_v _ v1_opt v2_opt =
      match v1_opt, v2_opt with
@ -559,10 +563,10 @@ struct
    in
    M.merge join_v x y

-  let widen : prev:t -> next:t -> num_iters:int -> t
+let widen : prev:t -> next:t -> num_iters:int -> t
  = fun ~prev ~next ~num_iters:_ -> join prev next

-  let pp : F.formatter -> t -> unit
+let pp : F.formatter -> t -> unit
  = fun fmt x ->
    let pp_sep fmt () = F.fprintf fmt ", @," in
    let pp1 fmt (k, v) =
@ -574,19 +578,19 @@ struct
    F.fprintf fmt " }@]";
    F.fprintf fmt "@]"

-  let load : Ident.t -> Exp.t -> t -> t
+let load : Ident.t -> Exp.t -> t -> t
  = fun id exp m ->
    match exp with
    | Exp.Lvar x -> M.add id x m
    | _ -> m

-  let store : Exp.t -> Exp.t -> t -> t
+let store : Exp.t -> Exp.t -> t -> t
  = fun e _ m ->
    match e with
    | Exp.Lvar x -> M.filter (fun _ y -> not (Pvar.equal x y)) m
    | _ -> m

-  let find : Ident.t -> t -> Pvar.t option
+let find : Ident.t -> t -> Pvar.t option
  = fun k m -> try Some (M.find k m) with Not_found -> None
 end

--- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml
+++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
@ -157,13 +157,13 @@ struct
        | Exp.Cast (_, e) -> eval e mem loc
        | Exp.Lfield (e, fn, _) ->
          eval e mem loc
-            |> Val.get_all_locs
+          |> Val.get_array_locs
          |> Fn.flip PowLoc.append_field fn
          |> Val.of_pow_loc
        | Exp.Lindex (e1, _) ->
-            let arr = eval e1 mem loc in (* must have array blk *)
+          let arr = eval e1 mem loc |> Val.get_array_blk in (* must have array blk *)
          (* let idx = eval e2 mem loc in *)
-            let ploc = arr |> Val.get_array_blk |> ArrayBlk.get_pow_loc in
+          let ploc = if ArrayBlk.is_bot arr then PowLoc.unknown else ArrayBlk.get_pow_loc arr in
          (* if nested array, add the array blk *)
          let arr = Mem.find_heap_set ploc mem in
          Val.join (Val.of_pow_loc ploc) arr
@ -356,14 +356,14 @@ struct
      let get_size v = v |> Val.get_array_blk |> ArrayBlk.sizeof in
      let get_field_name (fn, _, _) = fn in
      let deref_field v fn mem =
-        Mem.find_heap_set (PowLoc.append_field (Val.get_all_locs v) fn) mem
+        Mem.find_heap_set (PowLoc.append_field (Val.get_array_locs v) fn) mem
      in
-      let deref_ptr v mem = Mem.find_heap_set (Val.get_all_locs v) mem in
+      let deref_ptr v mem = Mem.find_heap_set (Val.get_array_locs v) mem in
      let add_pair_itv itv1 itv2 l =
        let open Itv in
-        if itv1 <> bot && itv2 <> bot then
+        if itv1 <> bot && itv1 <> top && itv2 <> bot then
          (lb itv1, lb itv2) :: (ub itv1, ub itv2) :: l
-        else if itv1 <> bot && Itv.eq itv2 bot then
+        else if itv1 <> bot && itv1 <> top && Itv.eq itv2 bot then
          (lb itv1, Bound.Bot) :: (ub itv1, Bound.Bot) :: l
        else
          l
--- a/infer/tests/codetoanalyze/c/bufferoverrun/global.c
+++ b/infer/tests/codetoanalyze/c/bufferoverrun/global.c
@ -0,0 +1,15 @@
+/*
+ * Copyright (c) 2017 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+int global;
+
+void compare_global_variable_bad() {
+  char arr[10];
+  if (global < 10)
+    arr[10] = 1;
+}
--- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
+++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
@ -4,6 +4,7 @@ codetoanalyze/c/bufferoverrun/do_while.c, do_while, 3, BUFFER_OVERRUN, [Offset:
 codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN, [Offset: [0, 9] Size: [5, 10] @ codetoanalyze/c/bufferoverrun/for_loop.c:38:5]
 codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN, [Offset: [20, 20] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:18:3 by call `arr_access()` ]
 codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN, [Offset: [100, 100] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:17:3 by call `arr_access()` ]
+codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/global.c:14:5]
 codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN, [Offset: [10, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/goto_loop.c:24:3]
 codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN, [Offset: [0, 10] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop.c:20:7]
 codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop_with_label.c:19:5]
--- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
+++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
@ -1,3 +1,4 @@
+codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo] @ 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, [Offset: [s$6, s$7] Size: [s$6, s$7] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `int_vector_access_at()` ]
 codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10] @ codetoanalyze/cpp/bufferoverrun/trivial.cpp:15:3]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN, [Offset: [s$14, s$15] Size: [s$14, s$15] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:91:24 by call `std::vector<int,std::allocator<int>>_operator[]()` ]