give correct type to root exps of array dereferences

Summary:
This diff fixes two issues in the backend that were causing Bad_footprint
errors when abducing pointsto facts for expressions that start in an array
access and follow up with another structured access, eg `x[0].some_field`:
1. array accesses were assumed to come last in these expressions
2. the type of the root exp passed to the function that walks down the list of
  offsets to apply to it was wrong in the case of arrays: it was always the
  type of the whole expression instead of the root expr (eg the type of
  `x[0].some_field` instead of the type of `x`).

Reviewed By: sblackshear, jeremydubreil

Differential Revision: D3800566

fbshipit-source-id: 0511604

infer/src/backend/rearrange.ml

@@ -148,9 +148,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
     | Typ.Tint _, [] | Typ.Tfloat _, [] | Typ.Tvoid, [] | Typ.Tfun _, [] | Typ.Tptr _, [] ->
         let id = new_id () in
         ([], Sil.Eexp (Exp.Var id, inst), t)
-    | Typ.Tint _, [Sil.Off_index e] | Typ.Tfloat _, [Sil.Off_index e]
+    | (Typ.Tint _ | Tfloat _ | Tvoid | Tfun _ | Tptr _), (Sil.Off_index e)::off' ->
-    | Typ.Tvoid, [Sil.Off_index e]
-    | Typ.Tfun _, [Sil.Off_index e] | Typ.Tptr _, [Sil.Off_index e] ->
         (* In this case, we lift t to the t array. *)
         let t' = match t with
           | Typ.Tptr(t', _) -> t'
@@ -158,7 +156,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
         let len = Exp.Var (new_id ()) in
         let atoms', se', res_t' =
           create_struct_values
-            pname tenv orig_prop footprint_part kind max_stamp t' [] inst in
+            pname tenv orig_prop footprint_part kind max_stamp t' off' inst in
         let e' = Sil.array_clean_new_index footprint_part e in
         let se = Sil.Earray (len, [(e', se')], inst) in
         let res_t = Typ.Tarray (res_t', None) in
@@ -831,6 +829,11 @@ let add_guarded_by_constraints prop lexp pdesc =
     variables. This function ensures that [root(lexp): typ] is the
     current hpred of the iterator. typ is the type of the root of lexp. *)
 let prop_iter_add_hpred_footprint pname tenv orig_prop iter (lexp, typ) inst =
+  if Config.trace_rearrange then (
+    L.d_strln "entering prop_iter_add_hpred_footprint";
+    L.d_str "lexp: "; Sil.d_exp lexp; L.d_ln ();
+    L.d_str "typ:"; Typ.d_full typ; L.d_ln ();
+  );
   let max_stamp = fav_max_stamp (Prop.prop_iter_footprint_fav iter) in
   let ptsto, ptsto_foot, atoms =
     mk_ptsto_exp_footprint pname tenv orig_prop (lexp, typ) max_stamp inst in
@@ -1075,25 +1078,30 @@ let check_type_size pname prop texp off typ_from_instr =
 let rec iter_rearrange
     pname tenv lexp typ_from_instr prop iter
     inst: (Sil.offset list) Prop.prop_iter list =
-  let typ = match Sil.exp_get_offsets lexp with
+  let rec root_typ_of_offsets = function
     | Sil.Off_fld (f, ((Typ.Tstruct _) as struct_typ)) :: _ ->
         (* access through field: get the struct type from the field *)
         if Config.trace_rearrange then begin
           L.d_increase_indent 1;
           L.d_str "iter_rearrange: root of lexp accesses field "; L.d_strln (Ident.fieldname_to_string f);
-          L.d_str "  type from instruction: "; Typ.d_full typ_from_instr; L.d_ln();
           L.d_str "  struct type from field: "; Typ.d_full struct_typ; L.d_ln();
           L.d_decrease_indent 1;
           L.d_ln();
         end;
         struct_typ
+    | Sil.Off_index _ :: off
+      when !Config.curr_language = Config.Clang
+      (* TODO(t7651424): turn on for Java. Needs fixing in the frontend *) ->
+        Typ.Tarray (root_typ_of_offsets off, None)
     | _ ->
         typ_from_instr in
+  let typ = root_typ_of_offsets (Sil.exp_get_offsets lexp) in
   if Config.trace_rearrange then begin
     L.d_increase_indent 1;
     L.d_strln "entering iter_rearrange";
     L.d_str "lexp: "; Sil.d_exp lexp; L.d_ln ();
     L.d_str "typ: "; Typ.d_full typ; L.d_ln ();
+    L.d_str "type from instruction: "; Typ.d_full typ_from_instr; L.d_ln();
     L.d_strln "prop:"; Prop.d_prop prop; L.d_ln ();
     L.d_strln "iter:"; Prop.d_prop (Prop.prop_iter_to_prop iter);
     L.d_ln (); L.d_ln ()
@@ -1113,8 +1121,10 @@ let rec iter_rearrange
   let recurse_on_iters iters =
     let f_one_iter iter' =
       let prop' = Prop.prop_iter_to_prop iter' in
-      if Prover.check_inconsistency prop' then []
+      if Prover.check_inconsistency prop' then
-      else iter_rearrange pname tenv (Prop.lexp_normalize_prop prop' lexp) typ prop' iter' inst in
+        []
+      else
+        iter_rearrange pname tenv (Prop.lexp_normalize_prop prop' lexp) typ prop' iter' inst in
     let rec f_many_iters iters_lst = function
       | [] -> IList.flatten (IList.rev iters_lst)
       | iter':: iters' ->

infer/tests/codetoanalyze/c/errors/initialization/abduce_structured_types.c

@@ -0,0 +1,42 @@
+/*
+ * Copyright (c) 2016 - 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.
+ */
+
+typedef struct { int f1; } a_struct;
+
+typedef struct {
+  int f1;
+  a_struct array[10];
+} b_struct;
+
+void init_static() { static const b_struct x[] = {{1}}; }
+
+int array_of_struct(b_struct x[]) {
+  int j = x[0].array[5].f1;
+  int i = x[0].f1;
+  b_struct y = x[0];
+}
+
+int pointer_of_struct(b_struct* x) {
+  int i = (*x).f1;
+  b_struct y = *x;
+  int j = y.f1;
+}
+
+int array_of_array_of_struct(b_struct x[][100]) {
+  int i = x[32][52].f1;
+  b_struct* y = x[32];
+  b_struct z = x[32][52];
+  int j = z.f1;
+}
+
+int pointer_of_array_of_struct(b_struct* x[], int n) {
+  int i = (*x)[n].f1;
+  b_struct y = (*x)[n];
+  int j = y.f1;
+}

infer/tests/endtoend/c/infer/ArrayOfStructsAbductionTest.java

@@ -0,0 +1,62 @@
+/*
+ * Copyright (c) 2016 - 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.
+ */
+
+package endtoend.c.infer;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static utils.matchers.ResultContainsExactly.containsExactly;
+
+import com.google.common.collect.ImmutableList;
+
+import org.junit.BeforeClass;
+import org.junit.ClassRule;
+import org.junit.Test;
+
+import java.io.IOException;
+
+import utils.DebuggableTemporaryFolder;
+import utils.InferException;
+import utils.InferResults;
+import utils.InferRunner;
+
+public class ArrayOfStructsAbductionTest {
+
+  public static final String source_file =
+      "infer/tests/codetoanalyze/c/errors/initialization/abduce_structured_types.c";
+
+  private static ImmutableList<String> inferCmd;
+
+  public static final String BAD_FOOTPRINT = "Bad_footprint";
+
+  @ClassRule
+  public static DebuggableTemporaryFolder folder = new DebuggableTemporaryFolder();
+
+  @BeforeClass
+  public static void runInfer() throws InterruptedException, IOException {
+    ImmutableList<String> extraOptions =
+      new ImmutableList.Builder<String>()
+      .add("--developer-mode")
+      .build();
+    inferCmd = InferRunner.createCInferCommand(folder, source_file, extraOptions);
+  }
+
+  @Test
+  public void whenInferRunsOnAssertExampleThenNPENotFound()
+      throws InterruptedException, IOException, InferException {
+    InferResults inferResults = InferRunner.runInferC(inferCmd);
+    String[] no_procedures = {};
+
+    assertThat("Results should not contain a bad footprint error",
+               inferResults,
+               containsExactly(BAD_FOOTPRINT,
+                               source_file,
+                               no_procedures));
+  }
+
+}

infer/tests/utils/InferResults.java

@@ -67,6 +67,7 @@ public class InferResults {
             errorType.equals("DANGLING_POINTER_DEREFERENCE") ||
             errorType.equals("IVAR_NOT_NULL_CHECKED") ||
             errorType.equals("BAD_POINTER_COMPARISON") ||
+            errorType.equals("Bad_footprint") ||
             errorType.equals("MUTABLE_LOCAL_VARIABLE_IN_COMPONENT_FILE")) {
           Integer errorLine = Integer.parseInt(items[5].trim());
           String procedure = items[6];