From c5cbd3142ebe7f32cecb23f11a9ea217d331e54e Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 22 Feb 2021 03:22:03 -0800 Subject: [PATCH] [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 | 10 +++++----- infer/tests/codetoanalyze/c/pulse/issues.exp | 1 + infer/tests/codetoanalyze/c/pulse/uninit.c | 19 +++++++++++++++++++ 3 files changed, 25 insertions(+), 5 deletions(-) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 62720191c..d844fcaa9 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/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. *) diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp index bc47dfc8f..3282e724e 100644 --- a/infer/tests/codetoanalyze/c/pulse/issues.exp +++ b/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] diff --git a/infer/tests/codetoanalyze/c/pulse/uninit.c b/infer/tests/codetoanalyze/c/pulse/uninit.c index 95d04bd05..182870d47 100644 --- a/infer/tests/codetoanalyze/c/pulse/uninit.c +++ b/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); +}