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];