[inferbo] Avoid array field is evaluated to the unknown location

Summary: It avoids that locations of array fields are evaluated to the `unknown` location incorrectly by addressing the case in the `eval_lindex` function.

Reviewed By: mbouaziz

Differential Revision: D7152736

fbshipit-source-id: 2dc825e

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -206,7 +206,7 @@ module Make (CFG : ProcCfg.S) = struct
       | Exp.Cast (_, e) ->
           eval e mem
       | Exp.Lfield (e, fn, _) ->
-          eval e mem |> Val.get_array_locs |> PowLoc.append_field ~fn |> Val.of_pow_loc
+          eval e mem |> Val.get_all_locs |> PowLoc.append_field ~fn |> Val.of_pow_loc
       | Exp.Lindex (e1, e2) ->
           eval_lindex e1 e2 mem
       | Exp.Sizeof {nbytes= Some size} ->
@@ -217,13 +217,23 @@ module Make (CFG : ProcCfg.S) = struct
           Val.Itv.top
 
 
+  (* NOTE: multidimensional array is not supported yet *)
   and eval_lindex array_exp index_exp mem =
-    let arr = Val.plus_pi (eval array_exp mem) (eval index_exp mem) in
+    let array_v, index_v = (eval array_exp mem, eval index_exp mem) in
-    let ploc =
+    let arr = Val.plus_pi array_v index_v in
-      if ArrayBlk.is_bot (Val.get_array_blk arr) then PowLoc.unknown else Val.get_all_locs arr
+    if ArrayBlk.is_bot (Val.get_array_blk arr) then
-    in
+      match array_exp with
-    (* NOTE: multidimensional array is not supported yet *)
+      | Exp.Lfield _ when not (PowLoc.is_bot (Val.get_pow_loc array_v)) ->
-    Val.join (Val.of_pow_loc ploc) arr
+          (* It handles the case accessing an array field of struct,
+             e.g., x.f[n] .  Since our abstract domain distinguishes
+             memory sections for each array fields in struct, it finds
+             the memory section using the abstract memory, though the
+             memory lookup is not required to evaluate the address of
+             x.f[n] in the concrete semantics.  *)
+          Mem.find_set (Val.get_pow_loc array_v) mem
+      | _ ->
+          Val.of_pow_loc PowLoc.unknown
+    else arr
 
 
   and eval_unop : Unop.t -> Exp.t -> Mem.astate -> Val.t =

infer/tests/codetoanalyze/c/bufferoverrun/array_field.c

@@ -0,0 +1,25 @@
+/*
+ * Copyright (c) 2018 - 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.
+ */
+struct S1 {
+  int f[2];
+};
+
+void array_field_access_Good(struct S1 x, struct S1 y) {
+  int a[10];
+  x.f[0] = 1;
+  y.f[0] = 20;
+  a[x.f[0]] = 0;
+}
+
+void array_field_access_Bad(struct S1 x, struct S1 y) {
+  int a[10];
+  y.f[0] = 20;
+  x.f[0] = 1;
+  a[y.f[0]] = 0;
+}

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

@@ -1,6 +1,7 @@
 codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Bad, 2, BUFFER_OVERRUN_L3, [ArrayDeclaration,ArrayAccess: Offset: [-4, 4] Size: [5, 5]]
 codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_neg_Bad, 2, BUFFER_OVERRUN_L3, [ArrayDeclaration,ArrayAccess: Offset: [-4, 4] Size: [5, 5]]
 codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN_L2, [Offset: [3xs$0 + 1, 3xs$1 + 1] Size: [3xs$0 + 1, 3xs$1 + 1]]
+codetoanalyze/c/bufferoverrun/array_field.c, array_field_access_Bad, 4, BUFFER_OVERRUN_L1, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [20, 20] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 4, CONDITION_ALWAYS_TRUE, []
 codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 13, CONDITION_ALWAYS_TRUE, []
 codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 16, BUFFER_OVERRUN_L2, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: [10, 10]]