[inferbo] Instantiate symbolic locations in function parameters

Summary: It instantiates not only symbols for bound but also symbols for locations at function calls.

Reviewed By: mbouaziz

Differential Revision: D13231291

fbshipit-source-id: ce23a943b

infer/src/bufferoverrun/absLoc.ml

@@ -70,6 +70,8 @@ module Allocsite = struct
   let unknown = Unknown
 
   let get_path = function Unknown -> None | Param path -> Some path | Known {path} -> path
+
+  let get_param_path = function Param path -> Some path | Unknown | Known _ -> None
 end
 
 module Loc = struct
@@ -138,6 +140,15 @@ module Loc = struct
         Allocsite.get_path allocsite
     | Field (l, fn) ->
         Option.map (get_path l) ~f:(fun p -> Symb.SymbolPath.field p fn)
+
+
+  let rec get_param_path = function
+    | Var _ ->
+        None
+    | Allocsite allocsite ->
+        Allocsite.get_param_path allocsite
+    | Field (l, fn) ->
+        Option.map (get_param_path l) ~f:(fun p -> Symb.SymbolPath.field p fn)
 end
 
 module PowLoc = struct
@@ -163,6 +174,16 @@ module PowLoc = struct
 
 
   type eval_locpath = Symb.SymbolPath.partial -> t
+
+  let subst x (eval_locpath : eval_locpath) =
+    let subst1 l acc =
+      match Loc.get_param_path l with
+      | None ->
+          add l acc
+      | Some path ->
+          join acc (eval_locpath path)
+    in
+    fold subst1 x empty
 end
 
 (** unsound but ok for bug catching *)

infer/src/bufferoverrun/arrayBlk.ml

@@ -153,8 +153,19 @@ let get_pow_loc : t -> PowLoc.t =
   fold pow_loc_of_allocsite array PowLoc.bot
 
 
-let subst : t -> Bound.eval_sym -> t =
- fun a eval_sym -> map (fun info -> ArrInfo.subst info eval_sym) a
+let subst : t -> Bound.eval_sym -> PowLoc.eval_locpath -> t =
+ fun a eval_sym eval_locpath ->
+  let subst1 l info acc =
+    let info' = ArrInfo.subst info eval_sym in
+    match Allocsite.get_param_path l with
+    | None ->
+        add l info' acc
+    | Some path ->
+        let locs = eval_locpath path in
+        let add_allocsite l acc = match l with Loc.Allocsite a -> add a info' acc | _ -> acc in
+        PowLoc.fold add_allocsite locs acc
+  in
+  fold subst1 a empty
 
 
 let get_symbols : t -> Itv.SymbolSet.t =

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -317,7 +317,7 @@ module Val = struct
 
 
   let subst : t -> eval_sym_trace -> Location.t -> t =
-   fun x {eval_sym; trace_of_sym} location ->
+   fun x {eval_sym; trace_of_sym; eval_locpath} location ->
     let symbols = get_symbols x in
     let traces_caller =
       Itv.SymbolSet.fold
@@ -325,7 +325,11 @@ module Val = struct
         symbols TraceSet.empty
     in
     let traces = TraceSet.call location ~traces_caller ~traces_callee:x.traces in
-    {x with itv= Itv.subst x.itv eval_sym; arrayblk= ArrayBlk.subst x.arrayblk eval_sym; traces}
+    { x with
+      itv= Itv.subst x.itv eval_sym
+    ; powloc= PowLoc.subst x.powloc eval_locpath
+    ; arrayblk= ArrayBlk.subst x.arrayblk eval_sym eval_locpath
+    ; traces }
     (* normalize bottom *)
     |> normalize
 

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -333,16 +333,23 @@ let rec eval_sympath_partial params p mem =
 
 
 and eval_locpath params p mem =
-  match p with
-  | Symb.SymbolPath.Pvar _ ->
-      let v = eval_sympath_partial params p mem in
-      Val.get_all_locs v
-  | Symb.SymbolPath.Deref (_, p) ->
-      let v = eval_sympath_partial params p mem in
-      Val.get_all_locs v
-  | Symb.SymbolPath.Field (fn, p) ->
-      let locs = eval_locpath params p mem in
-      PowLoc.append_field ~fn locs
+  let res =
+    match p with
+    | Symb.SymbolPath.Pvar _ ->
+        let v = eval_sympath_partial params p mem in
+        Val.get_all_locs v
+    | Symb.SymbolPath.Deref (_, p) ->
+        let v = eval_sympath_partial params p mem in
+        Val.get_all_locs v
+    | Symb.SymbolPath.Field (fn, p) ->
+        let locs = eval_locpath params p mem in
+        PowLoc.append_field ~fn locs
+  in
+  if PowLoc.is_empty res then (
+    L.(debug BufferOverrun Verbose)
+      "Location value for %a is not found.@\n" Symb.SymbolPath.pp_partial p ;
+    PowLoc.unknown )
+  else res
 
 
 let eval_sympath params sympath mem =

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

@@ -3,7 +3,9 @@ codetoanalyze/c/bufferoverrun/arith.c, band_negative_Bad, 8, BUFFER_OVERRUN_L2,
 codetoanalyze/c/bufferoverrun/arith.c, band_negative_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
 codetoanalyze/c/bufferoverrun/arith.c, band_positive_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Call,Assignment,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 8] Size: 5]
 codetoanalyze/c/bufferoverrun/arith.c, band_positive_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 2 Size: 2]
-codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Call,<LHS trace>,Parameter `cp[*]`,Assignment,Binary operation: ([58, 102] - 87):unsigned64 by call to `scan_hex_Good` ]
+codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __variable_initialization,Call,<LHS trace>,Parameter `cp[*]`,Assignment,Binary operation: ([58, +oo] - 97):unsigned64 by call to `scan_hex_Good` ]
+codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __variable_initialization,Call,<LHS trace>,Parameter `cp[*]`,Assignment,Binary operation: ([58, 102] - 87):unsigned64 by call to `scan_hex_Good` ]
+codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: __variable_initialization,Call,<LHS trace>,Parameter `cp[*]`,Assignment,Binary operation: ([-oo, +oo] - 48):unsigned64 by call to `scan_hex_Good` ]
 codetoanalyze/c/bufferoverrun/arith.c, call_two_safety_conditions2_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,<LHS trace>,Call,Assignment,Assignment,<RHS trace>,Parameter `s`,Binary operation: ([0, +oo] + 15):unsigned32 by call to `two_safety_conditions2_Bad` ]
 codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_ge1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,Parameter `x`,<RHS trace>,Parameter `y`,Binary operation: (0 - 1):unsigned32 by call to `unsigned_prune_ge1_Good` ]
 codetoanalyze/c/bufferoverrun/arith.c, div_const2_FP, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Parameter `n`,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 1]

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

@@ -296,7 +296,7 @@ class my_class6 {
 
   void dummy_function() {}
 
-  void set_x_two_Good_FP() {
+  void set_x_two_Good() {
     int arr[5];
     *x = 0;
     dummy_function();

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

@@ -20,8 +20,7 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_new_overload2_Bad, 2,
 codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_param_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Length trace>,Parameter `x[*].b`,Array access: Offset: 3 Size: 3 by call to `flexible_array_param_access` ]
 codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_call_set_x_three_Bad, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 3]
 codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_call_set_x_three_Good_FP, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 5]
-codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_set_x_two_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 5]
-codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_set_x_two_Good_FP, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 5]
+codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_set_x_two_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 5 Size: 5]
 codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,Call,Parameter `n`,Assignment,<Length trace>,Call,Parameter `this[*].arr`,Array access: Offset: 10 Size: 10]
 codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Call,Parameter `n`,Assignment,<Length trace>,Call,Parameter `this[*].arr`,Array access: Offset: 10 Size: 10]
 codetoanalyze/cpp/bufferoverrun/class.cpp, new_nothrow_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5]