From 4fe1615434342219e91ca7212c4d3cab30815099 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 31 Aug 2016 16:42:33 -0700 Subject: [PATCH] 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 | 26 +++++--- .../initialization/abduce_structured_types.c | 42 +++++++++++++ .../c/infer/ArrayOfStructsAbductionTest.java | 62 +++++++++++++++++++ infer/tests/utils/InferResults.java | 1 + 4 files changed, 123 insertions(+), 8 deletions(-) create mode 100644 infer/tests/codetoanalyze/c/errors/initialization/abduce_structured_types.c create mode 100644 infer/tests/endtoend/c/infer/ArrayOfStructsAbductionTest.java diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index c1efa31e0..1d52cb56c 100644 --- a/infer/src/backend/rearrange.ml +++ b/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.Tvoid, [Sil.Off_index e] - | Typ.Tfun _, [Sil.Off_index e] | Typ.Tptr _, [Sil.Off_index e] -> + | (Typ.Tint _ | Tfloat _ | Tvoid | Tfun _ | Tptr _), (Sil.Off_index e)::off' -> (* 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 [] - else iter_rearrange pname tenv (Prop.lexp_normalize_prop prop' lexp) typ prop' iter' inst in + if Prover.check_inconsistency prop' then + [] + 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' -> diff --git a/infer/tests/codetoanalyze/c/errors/initialization/abduce_structured_types.c b/infer/tests/codetoanalyze/c/errors/initialization/abduce_structured_types.c new file mode 100644 index 000000000..8a4c966ed --- /dev/null +++ b/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; +} diff --git a/infer/tests/endtoend/c/infer/ArrayOfStructsAbductionTest.java b/infer/tests/endtoend/c/infer/ArrayOfStructsAbductionTest.java new file mode 100644 index 000000000..f7860ddba --- /dev/null +++ b/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 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 extraOptions = + new ImmutableList.Builder() + .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)); + } + +} diff --git a/infer/tests/utils/InferResults.java b/infer/tests/utils/InferResults.java index 93bd9ebc2..943cb6c3d 100644 --- a/infer/tests/utils/InferResults.java +++ b/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];