[inferbo] add instantiation for parameters (call-by-ptr/ref)

Reviewed By: mbouaziz

Differential Revision: D5155025

fbshipit-source-id: c0b4161

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -223,10 +223,52 @@ struct
       List.fold ~f:add_formal ~init:(mem, inst_num, 0) (Sem.get_formals pdesc)
       |> fst3
 
-  let instantiate_ret
+  let instantiate_ret ret callee_pname callee_exit_mem subst_map mem =
-    : Tenv.t -> Procdesc.t option -> Typ.Procname.t -> (Exp.t * Typ.t) list
+    match ret with
-      -> Dom.Mem.astate -> Dom.Summary.t -> Location.t -> Dom.Val.astate
+    | Some (id, _) ->
-    = fun tenv callee_pdesc callee_pname params caller_mem summary loc ->
+        let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar callee_pname) in
+        let ret_val = Dom.Mem.find_heap ret_loc callee_exit_mem in
+        let ret_var = Loc.of_var (Var.of_id id) in
+        Dom.Val.subst ret_val subst_map
+        |> Fn.flip (Dom.Mem.add_stack ret_var) mem
+    | None -> mem
+
+  let instantiate_param tenv pdesc params callee_entry_mem callee_exit_mem subst_map location mem =
+    let formals = Sem.get_formals pdesc in
+    let actuals = List.map ~f:(fun (a, _) -> Sem.eval a mem location) params in
+    let f mem formal actual =
+      match (snd formal).Typ.desc with
+      | Typ.Tptr (typ, _) ->
+          (match typ.Typ.desc with
+           | Typ.Tstruct typename ->
+               (match Tenv.lookup tenv typename with
+                | Some str ->
+                    let formal_locs = Dom.Mem.find_heap (Loc.of_pvar (fst formal)) callee_entry_mem
+                                      |> Dom.Val.get_array_blk |> ArrayBlk.get_pow_loc in
+                    let instantiate_fld mem (fn, _, _) =
+                      let formal_fields = PowLoc.append_field formal_locs fn in
+                      let v = Dom.Mem.find_heap_set formal_fields callee_exit_mem in
+                      let actual_fields = PowLoc.append_field (Dom.Val.get_all_locs actual) fn in
+                      Dom.Val.subst v subst_map
+                      |> Fn.flip (Dom.Mem.strong_update_heap actual_fields) mem
+                    in
+                    List.fold ~f:instantiate_fld ~init:mem str.Typ.Struct.fields
+                | _ -> mem)
+           | _ ->
+               let formal_locs = Dom.Mem.find_heap (Loc.of_pvar (fst formal)) callee_entry_mem
+                                 |> Dom.Val.get_array_blk |> ArrayBlk.get_pow_loc in
+               let v = Dom.Mem.find_heap_set formal_locs callee_exit_mem in
+               let actual_locs = Dom.Val.get_all_locs actual in
+               Dom.Val.subst v subst_map
+               |> Fn.flip (Dom.Mem.strong_update_heap actual_locs) mem)
+      | _ -> mem
+    in
+    try List.fold2_exn formals actuals ~init:mem ~f with Invalid_argument _ -> mem
+
+  let instantiate_mem
+    : Tenv.t -> (Ident.t * Typ.t) option -> Procdesc.t option -> Typ.Procname.t
+      -> (Exp.t * Typ.t) list -> Dom.Mem.astate -> Dom.Summary.t -> Location.t -> Dom.Mem.astate
+    = fun tenv ret callee_pdesc callee_pname params caller_mem summary loc ->
       let callee_entry_mem = Dom.Summary.get_input summary in
       let callee_exit_mem = Dom.Summary.get_output summary in
       match callee_pdesc with
@@ -234,11 +276,9 @@ struct
           let subst_map =
             Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem loc
           in
-          let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar callee_pname) in
+          instantiate_ret ret callee_pname callee_exit_mem subst_map caller_mem
-          let ret_val = Dom.Mem.find_heap ret_loc callee_exit_mem in
+          |> instantiate_param tenv pdesc params callee_entry_mem callee_exit_mem subst_map loc
-          Dom.Val.subst ret_val subst_map
+      | None -> caller_mem
-          |> Dom.Val.normalize    (* normalize bottom *)
-      | _ -> Dom.Val.Itv.top
 
   let print_debug_info : Sil.instr -> Dom.Mem.astate -> Dom.Mem.astate -> unit
     = fun instr pre post ->
@@ -270,13 +310,7 @@ struct
             (match Summary.read_summary pdesc callee_pname with
              | Some summary ->
                  let callee = extras callee_pname in
-                 let ret_val =
+                 instantiate_mem tenv ret callee callee_pname params mem summary loc
-                   instantiate_ret tenv callee callee_pname params mem summary loc
-                 in
-                 (match ret with
-                  | Some (id, _) ->
-                      Dom.Mem.add_stack (Loc.of_var (Var.of_id id)) ret_val mem
-                  | _ -> mem)
              | None ->
                  handle_unknown_call pname ret callee_pname params node mem loc)
         | Declare_locals (locals, _) ->

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -385,11 +385,6 @@ struct
       then { bot with itv = Itv.top }
       else { bot with itv = ArrayBlk.diff x.arrayblk y.arrayblk }
 
-  let subst : t -> Itv.Bound.t Itv.SubstMap.t -> t
-    = fun x subst_map ->
-      { x with itv = Itv.subst x.itv subst_map;
-               arrayblk = ArrayBlk.subst x.arrayblk subst_map }
-
   let get_symbols : t -> Itv.Symbol.t list
     = fun x ->
       List.append (Itv.get_symbols x.itv) (ArrayBlk.get_symbols x.arrayblk)
@@ -398,6 +393,12 @@ struct
     = fun x ->
       { x with itv = Itv.normalize x.itv; arrayblk = ArrayBlk.normalize x.arrayblk }
 
+  let subst : t -> Itv.Bound.t Itv.SubstMap.t -> t
+    = fun x subst_map ->
+      { x with itv = Itv.subst x.itv subst_map;
+               arrayblk = ArrayBlk.subst x.arrayblk subst_map }
+      |> normalize  (* normalize bottom *)
+
   let pp_summary : F.formatter -> t -> unit
     = fun fmt x -> F.fprintf fmt "(%a, %a)" Itv.pp x.itv ArrayBlk.pp x.arrayblk
 

infer/tests/codetoanalyze/c/bufferoverrun/function_call.c

@@ -12,6 +12,10 @@
 
 #include <stdlib.h>
 
+struct S {
+  int field;
+};
+
 void arr_access(int* arr, char* p, int i) {
   int x = arr[0];
   arr[x] = 1; /* BUG */
@@ -29,16 +33,46 @@ void ptr_set_to_zero(int* x) {
   *x = 0;
 }
 
-void call_by_ptr_good_FP() {
+void struct_ptr_set_to_zero(struct S* s) { s->field = 0; }
+
+void call_by_ptr_good() {
   int arr[10];
   int i = 99;
   ptr_set_to_zero(&i);
   arr[i] = 123;
 }
 
-void call_by_ptr_bad_FN() {
+void call_by_arr_good() {
+  int arr[10];
+  ptr_set_to_zero(&arr);
+  arr[arr[0]] = 123;
+}
+
+void call_by_struct_ptr_good() {
+  int arr[10];
+  struct S* s = (struct S*)malloc(sizeof(struct S));
+  s->field = 99;
+  struct_ptr_set_to_zero(s);
+  arr[s->field] = 123;
+}
+
+void call_by_ptr_bad() {
   int arr[10];
   int i = 5;
   ptr_set_to_zero(&i);
   arr[i - 1] = 123;
 }
+
+void call_by_arr_bad() {
+  int arr[10];
+  ptr_set_to_zero(&arr);
+  arr[arr[0] - 1] = 123;
+}
+
+void call_by_struct_ptr_bad() {
+  int arr[10];
+  struct S* sp = (struct S*)malloc(sizeof(struct S));
+  sp->field = 5;
+  struct_ptr_set_to_zero(sp);
+  arr[sp->field - 1] = 123;
+}

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

@@ -6,9 +6,11 @@ codetoanalyze/c/bufferoverrun/do_while.c, do_while, 2, BUFFER_OVERRUN, [Offset:
 codetoanalyze/c/bufferoverrun/do_while.c, do_while, 3, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/do_while.c:18:5 by call `do_while_sub()` ]
 codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN, [Offset: [0, 9] Size: [5, 10]]
 codetoanalyze/c/bufferoverrun/for_loop.c, safealloc, 10, UNREACHABLE_CODE, []
-codetoanalyze/c/bufferoverrun/function_call.c, call_by_ptr_good_FP, 4, BUFFER_OVERRUN, [Offset: [99, 99] Size: [10, 10]]
+codetoanalyze/c/bufferoverrun/function_call.c, call_by_arr_bad, 3, BUFFER_OVERRUN, [Offset: [-1, -1] Size: [10, 10]]
-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, call_by_ptr_bad, 4, BUFFER_OVERRUN, [Offset: [-1, -1] Size: [10, 10]]
-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/function_call.c, call_by_struct_ptr_bad, 5, BUFFER_OVERRUN, [Offset: [-1, -1] Size: [10, 10]]
+codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN, [Offset: [100, 100] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:21:3 by call `arr_access()` ]
+codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN, [Offset: [20, 20] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:22: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/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN, [Offset: [10, +oo] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/inf_loop.c, inf_loop, 4, CONDITION_ALWAYS_TRUE, []

infer/tests/codetoanalyze/cpp/bufferoverrun/function_call.cpp

@@ -7,18 +7,24 @@
  * of patent rights can be found in the PATENTS file in the same directory.
  */
 
+struct S {
+  int field;
+};
+
 void ref_set_to_zero(int& x) {
   x = 0;
 }
 
-void call_by_ref_good_FP() {
+void struct_ref_set_to_zero(struct S& s) { s.field = 0; }
+
+void call_by_ref_good() {
   int arr[10];
   int i = 99;
   ref_set_to_zero(i);
   arr[i] = 123;
 }
 
-void call_by_ref_bad_FN() {
+void call_by_ref_bad() {
   int arr[10];
   int i = 5;
   ref_set_to_zero(i);

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

@@ -1,4 +1,4 @@
-codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_good_FP, 4, BUFFER_OVERRUN, [Offset: [99, 99] 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/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]]