[uninit] Fix a bug on nested struct initialization

Summary:
`add_edge_on_src` is to prepare a stack location for a local variable.  Before this diff, it was
called several times for each fields.

Reviewed By: jvillard

Differential Revision: D26543715

fbshipit-source-id: 49ebf2b65

infer/src/pulse/PulseAbductiveDomain.ml

@@ -486,18 +486,18 @@ let rec set_uninitialized_post tenv src typ location (post : PostDomain.t) =
         (* Ignore single field structs: see D26146578 *)
         post
     | Some {fields} ->
-        List.fold fields ~init:post ~f:(fun (acc : PostDomain.t) (field, field_typ, _) ->
+        let stack, addr = add_edge_on_src src location (post :> base_domain).stack in
+        let init = PostDomain.update ~stack post in
+        List.fold fields ~init ~f:(fun (acc : PostDomain.t) (field, field_typ, _) ->
             if Fieldname.is_internal field then acc
             else
-              let {stack; heap} = (acc :> base_domain) in
-              let stack, addr = add_edge_on_src src location stack in
               let field_addr = AbstractValue.mk_fresh () in
               let history = [ValueHistory.StructFieldAddressCreated (field, location)] in
               let heap =
                 BaseMemory.add_edge addr (HilExp.Access.FieldAccess field) (field_addr, history)
-                  heap
+                  (acc :> base_domain).heap
               in
-              PostDomain.update ~stack ~heap acc
+              PostDomain.update ~heap acc
               |> set_uninitialized_post tenv (`Malloc field_addr) field_typ location ) )
   | Tarray _ | Tvoid | Tfun | TVar _ ->
       (* We ignore tricky types to mark uninitialized addresses. *)

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

@@ -15,4 +15,5 @@ codetoanalyze/c/pulse/uninit.c, interprocedural_read_in_callee_bad, 2, PULSE_UNI
 codetoanalyze/c/pulse/uninit.c, interprocedural_struct_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [struct field address `f2` created,read to uninitialized value occurs here]
 codetoanalyze/c/pulse/uninit.c, interprocedural_uninit_in_callee_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [passed as argument to `uninit`,return from call to `uninit`,assigned,read to uninitialized value occurs here]
 codetoanalyze/c/pulse/uninit.c, malloc_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [allocated by call to `malloc` (modelled),assigned,read to uninitialized value occurs here]
+codetoanalyze/c/pulse/uninit.c, nested_struct_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [struct field address `f1` created,when calling `read_g1_f1` here,parameter `x` of read_g1_f1,read to uninitialized value occurs here]
 codetoanalyze/c/pulse/uninit.c, self_assign_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `x` declared here,read to uninitialized value occurs here]

infer/tests/codetoanalyze/c/pulse/uninit.c

@@ -140,3 +140,22 @@ void local_array_bad_FN() {
   char c = o[1];
   free(o);
 }
+
+struct uninit_nested {
+  struct uninit_s g1;
+  int g2;
+};
+
+void read_g1_f1(struct uninit_nested* x) { int y = x->g1.f1; }
+
+void nested_struct_good() {
+  struct uninit_nested x;
+  x.g1.f1 = 42;
+  read_g1_f1(&x);
+}
+
+void nested_struct_bad() {
+  struct uninit_nested x;
+  x.g1.f2 = 42;
+  read_g1_f1(&x);
+}