[inferbo] Revise substitution of array block

Summary:
Given a pointer-typed parameter, Inferbo assumes that it is an array
block.  However, when a pointer is given as an actual parameter, it
failed the substitution of the array block value of the parameter, thus
which made some return values to bottom unexpectedly.

This diff revises the substitution of array block, so it can
substitute array block values with actual pointers correctly when it
is possible.

Reviewed By: mbouaziz

Differential Revision: D14663475

fbshipit-source-id: 0477de1ba

infer/src/bufferoverrun/arrayBlk.ml

@@ -133,6 +133,17 @@ module ArrInfo = struct
         AbstractDomain.TopLiftedUtils.pp_top f
 
 
+  let is_pointer : Symb.SymbolPath.partial -> t -> bool =
+   fun path arr ->
+    match (path, arr) with
+    | Deref ((Deref_COneValuePointer | Deref_CPointer), path), C {offset; size} ->
+        Itv.is_offset_path_of path offset && Itv.is_length_path_of path size
+    | Deref (Deref_JavaPointer, path), Java {length} ->
+        Itv.is_length_path_of path length
+    | _, _ ->
+        false
+
+
   let is_symbolic : t -> bool =
    fun arr ->
     match arr with
@@ -309,19 +320,30 @@ let get_pow_loc : t -> PowLoc.t =
   fold pow_loc_of_allocsite array PowLoc.bot
 
 
-let subst : t -> Bound.eval_sym -> PowLoc.eval_locpath -> t =
+let subst : t -> Bound.eval_sym -> PowLoc.eval_locpath -> PowLoc.t * t =
  fun a eval_sym eval_locpath ->
-  let subst1 l info acc =
+  let subst1 l info (powloc_acc, acc) =
     let info' = ArrInfo.subst info eval_sym in
     match Allocsite.get_param_path l with
     | None ->
-        add l info' acc
+        (powloc_acc, 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
+        let add_allocsite l (powloc_acc, acc) =
+          match l with
+          | Loc.Allocsite a ->
+              (powloc_acc, add a info' acc)
+          | _ ->
+              if ArrInfo.is_pointer path info then (PowLoc.add l powloc_acc, acc)
+              else (
+                if Config.bo_debug >= 3 then
+                  L.d_printfln_escaped "Substitution of array block failed: %a -> %a" Loc.pp l
+                    ArrInfo.pp info ;
+                (powloc_acc, acc) )
+        in
+        PowLoc.fold add_allocsite locs (powloc_acc, acc)
   in
-  fold subst1 a empty
+  fold subst1 a (PowLoc.empty, empty)
 
 
 let is_symbolic : t -> bool = fun a -> exists (fun _ ai -> ArrInfo.is_symbolic ai) a

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -398,10 +398,12 @@ module Val = struct
         symbols TraceSet.bottom
     in
     let traces = TraceSet.call location ~traces_caller ~traces_callee:x.traces in
+    let powloc = PowLoc.subst x.powloc eval_locpath in
+    let powloc_from_arrayblk, arrayblk = ArrayBlk.subst x.arrayblk eval_sym eval_locpath in
     { 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
+    ; powloc= PowLoc.join powloc powloc_from_arrayblk
+    ; arrayblk
     ; traces }
     (* normalize bottom *)
     |> normalize

infer/src/bufferoverrun/itv.ml

@@ -657,3 +657,7 @@ let of_normal_path ~unsigned path = NonBottom (ItvPure.of_normal_path ~unsigned
 let of_offset_path path = NonBottom (ItvPure.of_offset_path path)
 
 let of_length_path path = NonBottom (ItvPure.of_length_path path)
+
+let is_offset_path_of path x = eq (of_offset_path path) x
+
+let is_length_path_of path x = eq (of_length_path path) x

infer/src/bufferoverrun/itv.mli

@@ -234,3 +234,7 @@ val of_normal_path : unsigned:bool -> Symb.SymbolPath.partial -> t
 val of_offset_path : Symb.SymbolPath.partial -> t
 
 val of_length_path : Symb.SymbolPath.partial -> t
+
+val is_offset_path_of : Symb.SymbolPath.partial -> t -> bool
+
+val is_length_path_of : Symb.SymbolPath.partial -> t -> bool

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

@@ -160,3 +160,23 @@ void call_va_arg_int_Bad() {
   int a[10];
   va_arg_int(a, 10);
 }
+
+struct S* id_S(struct S* r) {
+  return r;
+}
+
+void call_id_S_Good_FP(struct S p) {
+  int a[10];
+  struct S* q = id_S(&p);
+  if (q == 0) {
+    a[10] = 0; // should be unreachable
+  }
+}
+
+void call_id_S_Bad(struct S p) {
+  int a[10];
+  struct S* q = id_S(&p);
+  if (q != 0) {
+    a[10] = 0; // should be reachable
+  }
+}

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

@@ -115,6 +115,8 @@ codetoanalyze/c/bufferoverrun/function_call.c, call_call_access_index_4_on_S3_Ba
 codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_bad1, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_bad1, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_good, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
+codetoanalyze/c/bufferoverrun/function_call.c, call_id_S_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
+codetoanalyze/c/bufferoverrun/function_call.c, call_id_S_Good_FP, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/function_call.c, call_va_arg_int_Bad, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Unknown value from: __builtin_va_arg,Assignment,<Length trace>,Parameter `*a`,Array access: Offset: [-oo, +oo] Size: 10 by call to `va_arg_int` ]
 codetoanalyze/c/bufferoverrun/function_call.c, call_va_arg_int_Good_FP, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Unknown value from: __builtin_va_arg,Assignment,<Length trace>,Parameter `*a`,Array access: Offset: [-oo, +oo] Size: 10 by call to `va_arg_int` ]
 codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Parameter `*arr`,Assignment,<Length trace>,Parameter `*arr`,Array access: Offset: 100 Size: 10 by call to `arr_access` ]