[Bufferoverrun] symbolic value for parameter

Reviewed By: mbouaziz

Differential Revision: D5002459

fbshipit-source-id: a6261ae

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -152,80 +152,98 @@ struct
             ~inst_num ~dimension:(dimension + 1) mem
       | _ -> mem
 
-  let declare_symbolic_array
+  let counter_gen init =
+    let num_ref = ref init in
+    let get_num () =
+      let v = !num_ref in
+      num_ref := v + 1;
+      v
+    in
+    get_num
+
+  let declare_symbolic_val
     : Typ.Procname.t -> Tenv.t -> CFG.node -> Loc.t -> Typ.t -> inst_num:int
-    -> sym_num:int -> dimension:int -> Dom.Mem.astate -> Dom.Mem.astate * int
-    = fun pname tenv node loc typ ~inst_num ~sym_num ~dimension mem ->
-      let offset = Itv.make_sym pname sym_num in
-      let size = Itv.make_sym pname (sym_num + 2) in
-      let arr =
-        Sem.eval_array_alloc pname node typ offset size inst_num dimension
-      in
-      let elem_val = Dom.Val.make_sym pname (sym_num + 4) in
-      let arr_loc = arr |> Dom.Val.get_array_blk |> ArrayBlk.get_pow_loc in
-      let mem =
-        mem
-        |> Dom.Mem.add_heap loc arr
-        |> Dom.Mem.strong_update_heap arr_loc elem_val
-      in
-      let decl_fld (mem, sym_num) (fn, typ, _) =
-        let loc =
-          mem |> Dom.Mem.find_heap loc |> Dom.Val.get_array_locs |> PowLoc.choose
+    -> new_sym_num: (unit -> int) -> Domain.t -> Domain.t
+    = fun pname tenv node loc typ ~inst_num ~new_sym_num mem ->
+      let max_depth = 2 in
+      let new_alloc_num = counter_gen 1 in
+      let rec decl_sym_fld ~depth loc typ mem =
+        if depth > max_depth then mem else
+          let depth = depth + 1 in
+          match typ.Typ.desc with
+          | Typ.Tint ikind ->
+              let unsigned = Typ.ikind_is_unsigned ikind in
+              let sym_num = new_sym_num () in
+              let _ = new_sym_num () in
+              let v = Dom.Val.make_sym ~unsigned pname sym_num in
+              Dom.Mem.add_heap loc v mem
+          | Typ.Tfloat _ ->
+              let sym_num = new_sym_num () in
+              let _ = new_sym_num () in
+              let v = Dom.Val.make_sym pname sym_num in
+              Dom.Mem.add_heap loc v mem
+          | Typ.Tptr (typ, _) ->
+              decl_sym_arr ~depth loc typ mem
+          | Typ.Tarray (typ, opt_int_lit, _) ->
+              let opt_size = Option.map ~f:Itv.of_int_lit opt_int_lit in
+              let opt_offset = Some Itv.zero in
+              decl_sym_arr ~depth loc typ ~opt_offset ~opt_size mem
+          | Typ.Tstruct typename ->
+              let decl_fld mem (fn, typ, _) =
+                let loc_fld = Loc.append_field loc fn in
+                decl_sym_fld ~depth loc_fld typ mem
+              in
+              let decl_flds str =
+                List.fold ~f:decl_fld ~init:mem str.Typ.Struct.fields
+              in
+              let opt_struct = Tenv.lookup tenv typename in
+              Option.value_map opt_struct ~default:mem ~f:decl_flds
+          | _ ->
+              if Config.bo_debug >= 3 then
+                L.(debug BufferOverrun Verbose) "/!\\ decl_fld of unhandled type: %a at %a@."
+                  (Typ.pp Pp.text) typ
+                  Location.pp (CFG.loc node);
+              mem
+
+      and decl_sym_arr ~depth loc typ ?(opt_offset=None) ?(opt_size=None) mem =
+        let option_value opt_x default_f =
+          match opt_x with
+          | Some x -> x
+          | None -> default_f ()
         in
-        let field = Loc.append_field loc fn in
-        match typ.Typ.desc with
-        | Typ.Tint ikind ->
-            let unsigned = Typ.ikind_is_unsigned ikind in
-            let v = Dom.Val.make_sym ~unsigned pname sym_num in
-            (Dom.Mem.add_heap field v mem, sym_num + 2)
-        | Typ.Tfloat _ ->
-            let v = Dom.Val.make_sym pname sym_num in
-            (Dom.Mem.add_heap field v mem, sym_num + 2)
-        | Typ.Tptr (typ, _) ->
-            let offset = Itv.make_sym pname sym_num in
-            let size = Itv.make_sym pname (sym_num + 2) in
-            let v =
-              Sem.eval_array_alloc pname node typ offset size inst_num dimension
-            in
-            (Dom.Mem.add_heap field v mem, sym_num + 4)
-        | _ ->
-            L.(debug BufferOverrun Verbose) "/!\\ decl_fld of unhandled type: %a at %a@."
-              (Typ.pp Pp.text) typ
-              Location.pp (CFG.loc node);
-            (mem, sym_num)
+        let itv_make_sym () =
+          let sym_num = new_sym_num () in
+          let _ = new_sym_num () in
+          Itv.make_sym pname sym_num
+        in
+        let offset = option_value opt_offset itv_make_sym in
+        let size = option_value opt_size itv_make_sym in
+        let alloc_num = new_alloc_num () in
+        let arr =
+          Sem.eval_array_alloc pname node typ offset size inst_num alloc_num
+        in
+        let mem = Dom.Mem.add_heap loc arr mem in
+        let deref_loc =
+          Loc.of_allocsite (Sem.get_allocsite pname node inst_num alloc_num)
+        in
+        decl_sym_fld ~depth deref_loc typ mem
       in
-      match typ.Typ.desc with
-      | Typ.Tstruct typename ->
-          (match Tenv.lookup tenv typename with
-           | Some str ->
-               List.fold ~f:decl_fld ~init:(mem, sym_num + 6) str.Typ.Struct.fields
-           | _ -> (mem, sym_num + 6))
-      | _ -> (mem, sym_num + 6)
+      decl_sym_fld ~depth:0 loc typ mem
 
   let declare_symbolic_parameter
     : Procdesc.t -> Tenv.t -> CFG.node -> int -> Dom.Mem.astate -> Dom.Mem.astate
     = fun pdesc tenv node inst_num mem ->
       let pname = Procdesc.get_proc_name pdesc in
-      let add_formal (mem, inst_num, sym_num) (pvar, typ) =
-        match typ.Typ.desc with
-        | Typ.Tint ikind ->
-            let unsigned = Typ.ikind_is_unsigned ikind in
-            let v = Dom.Val.make_sym ~unsigned pname sym_num in
-            let mem = Dom.Mem.add_heap (Loc.of_pvar pvar) v mem in
-            (mem, inst_num + 1, sym_num + 2)
-        | Typ.Tptr (typ, _) ->
-            let (mem, sym_num) =
-              declare_symbolic_array pname tenv node (Loc.of_pvar pvar) typ
-                ~inst_num ~sym_num ~dimension:1 mem
-            in
-            (mem, inst_num + 1, sym_num)
-        | _ ->
-            L.(debug BufferOverrun Verbose) "declare_symbolic_parameter of unhandled type: %a@."
-              (Typ.pp Pp.text) typ;
-            (mem, inst_num, sym_num) (* TODO: add other cases if necessary *)
+      let new_sym_num = counter_gen 0 in
+      let add_formal (mem, inst_num) (pvar, typ) =
+        let loc = Loc.of_pvar pvar in
+        let mem =
+          declare_symbolic_val pname tenv node loc typ ~inst_num ~new_sym_num mem
+        in
+        (mem, inst_num + 1)
       in
-      List.fold ~f:add_formal ~init:(mem, inst_num, 0) (Sem.get_formals pdesc)
-      |> fst3
+      List.fold ~f:add_formal ~init:(mem, inst_num) (Sem.get_formals pdesc)
+      |> fst
 
   let instantiate_ret ret callee_pname callee_exit_mem subst_map mem =
     match ret with
@@ -365,15 +383,17 @@ struct
         | Exp.Var _ ->
             let arr = Sem.eval exp mem loc |> Dom.Val.get_array_blk in
             Some (arr, Itv.zero, true)
-        | Exp.Lindex (e1, e2)
-        | Exp.BinOp (Binop.PlusA, e1, e2) ->
-            let arr = Sem.eval e1 mem loc |> Dom.Val.get_array_blk in
+        | Exp.Lindex (e1, e2) ->
+            let locs = Sem.eval_locs e1 mem loc |> Dom.Val.get_all_locs in
+            let arr = Dom.Mem.find_set locs mem |> Dom.Val.get_array_blk in
             let idx = Sem.eval e2 mem loc |> Dom.Val.get_itv in
             Some (arr, idx, true)
-        | Exp.BinOp (Binop.MinusA, e1, e2) ->
+        | Exp.BinOp (Binop.PlusA as bop, e1, e2)
+        | Exp.BinOp (Binop.MinusA as bop, e1, e2) ->
             let arr = Sem.eval e1 mem loc |> Dom.Val.get_array_blk in
             let idx = Sem.eval e2 mem loc |> Dom.Val.get_itv in
-            Some (arr, idx, false)
+            let is_plus = Binop.equal bop Binop.PlusA in
+            Some (arr, idx, is_plus)
         | _ -> None
       in
       match array_access with

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -621,6 +621,10 @@ struct
   let find_heap_set : PowLoc.t -> t -> Val.t
     = fun k m -> Heap.find_set k m.heap
 
+  let find_set : PowLoc.t -> t -> Val.t
+    = fun k m ->
+      Val.join (find_stack_set k m) (find_heap_set k m)
+
   let find_alias : Ident.t -> t -> Pvar.t option
     = fun k m -> Alias.find k m.alias
 
@@ -711,6 +715,10 @@ module Mem = struct
     = fun k ->
       f_lift_default Val.bot (MemReach.find_heap_set k)
 
+  let find_set : PowLoc.t -> t -> Val.t
+    = fun k ->
+      f_lift_default Val.bot (MemReach.find_set k)
+
   let find_alias : Ident.t -> t -> Pvar.t option
     = fun k ->
       f_lift_default None (MemReach.find_alias k)

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -214,6 +214,33 @@ struct
       | Binop.LOr -> Val.lor_sem v1 v2
       | Binop.PtrFld -> raise Not_implemented
 
+  let rec eval_locs : Exp.t -> Mem.astate -> Location.t -> Val.t
+    = fun exp mem loc ->
+      match exp with
+      | Exp.Var id ->
+          (match Mem.find_alias id mem with
+           | Some pvar ->
+               Var.of_pvar pvar |> Loc.of_var |> PowLoc.singleton |> Val.of_pow_loc
+           | None -> Val.bot)
+      | Exp.Lvar pvar ->
+          pvar |> Loc.of_pvar |> PowLoc.singleton |> Val.of_pow_loc
+      | Exp.BinOp (bop, e1, e2) -> eval_binop bop e1 e2 mem loc
+      | Exp.Cast (_, e) -> eval_locs e mem loc
+      | Exp.Lfield (e, fn, _) ->
+          eval e mem loc
+          |> Val.get_all_locs
+          |> Fn.flip PowLoc.append_field fn
+          |> Val.of_pow_loc
+      | Exp.Lindex (e1, e2) ->
+          let arr = eval e1 mem loc in
+          let idx = eval e2 mem loc in
+          Val.plus_pi arr idx
+      | Exp.Const _
+      | Exp.UnOp _
+      | Exp.Sizeof _
+      | Exp.Exn _
+      | Exp.Closure _ -> Val.bot
+
   let get_allocsite : Typ.Procname.t -> CFG.node -> int -> int -> string
     = fun proc_name node inst_num dimension ->
       let proc_name = Typ.Procname.to_string proc_name in
@@ -400,6 +427,7 @@ struct
     = fun pairs ->
       let add_pair map (formal, actual) =
         match formal with
+        | Itv.Bound.Linear (_, se1) when Itv.SymLinear.is_zero se1 -> map
         | Itv.Bound.Linear (0, se1) when Itv.SymLinear.cardinal se1 > 0 ->
             let (symbol, coeff) = Itv.SymLinear.choose se1 in
             if Int.equal coeff 1

infer/src/bufferoverrun/itv.ml

@@ -879,7 +879,9 @@ let ub : t -> Bound.t
 let of_int : int -> astate
   = fun n -> NonBottom (ItvPure.of_int n)
 
-let of_int_lit n = of_int (IntLit.to_int n)
+let of_int_lit n =
+  try of_int (IntLit.to_int n) with
+  | _ -> top
 
 let is_bot : t -> bool
   = fun x -> equal x Bottom

infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp

@@ -0,0 +1,27 @@
+/*
+ * 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.
+ */
+class my_class {
+  int idx;
+  int arr[10];
+
+  void set_a(int n) { idx = n; }
+
+  int id(int n) { return n; }
+
+ public:
+  int access_Bad() {
+    set_a(10);
+    return arr[idx];
+  }
+
+  int access2_Bad() {
+    int n = 10;
+    return arr[id(n)];
+  }
+};

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

@@ -1,13 +1,17 @@
+codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10]]
+codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10]]
 codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN, [Offset: [-1, -1] Size: [10, 10]]
 codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<LMB<TFM>*,std::allocator<LMB<TFM>*>>_operator[]()` ]
 codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `ral()` ]
+codetoanalyze/cpp/bufferoverrun/repro1.cpp, it_it, 0, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [16, 16]]
+codetoanalyze/cpp/bufferoverrun/repro1.cpp, it_it, 0, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [16, 16]]
 codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN, [Offset: [0, +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: [max(0, s$6), s$7] Size: [max(0, s$6), s$7] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `int_vector_access_at()` ]
+codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN, [Offset: [max(0, s$4), s$5] Size: [max(0, s$4), s$5] @ 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/vector.cpp, constructor_Good_FP, 2, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<Int_no_copy,std::allocator<Int_no_copy>>_operator[]()` ]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN, [Offset: [1, 1] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<int,std::allocator<int>>_at()` ]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN, [Offset: [max(0, s$14), s$15] Size: [max(0, s$14), s$15] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN, [Offset: [max(0, s$12), s$13] Size: [max(0, s$12), s$13] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN, [Offset: [1, 1] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Good_FP, 3, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<int,std::allocator<int>>_operator[]()` ]