From e226cf8ec45ab6a00f8ab1e2328f59f5998c19e9 Mon Sep 17 00:00:00 2001 From: Radu Grigore Date: Thu, 14 Mar 2019 05:01:32 -0700 Subject: [PATCH] Fresh footprint variables in added frame. Summary: While adding a footprint frame during rearrangement, the footprint variables should be fresh with respect to the current state too, not only with respect to he footprint, because the frame is added to the state. Reviewed By: jberdine Differential Revision: D14401026 fbshipit-source-id: 20ea4485a --- infer/src/biabduction/Prop.ml | 23 ++++++----- infer/src/biabduction/Prop.mli | 11 ++--- infer/src/biabduction/Rearrange.ml | 12 ++---- .../codetoanalyze/c/biabduction/issues.exp | 1 + .../codetoanalyze/c/biabduction/nulluse.c | 41 +++++++++++++++++++ 5 files changed, 62 insertions(+), 26 deletions(-) create mode 100644 infer/tests/codetoanalyze/c/biabduction/nulluse.c diff --git a/infer/src/biabduction/Prop.ml b/infer/src/biabduction/Prop.ml index 4282897ae..85a4c1eb8 100644 --- a/infer/src/biabduction/Prop.ml +++ b/infer/src/biabduction/Prop.ml @@ -351,13 +351,6 @@ let sigma_gen_free_vars sigma = ISequence.gen_sequence_list sigma ~f:Sil.hpred_g let sigma_free_vars sigma = Sequence.Generator.run (sigma_gen_free_vars sigma) -(** Find free variables in the footprint part of the prop *) -let footprint_gen_free_vars {sigma_fp; pi_fp} = - Sequence.Generator.(sigma_gen_free_vars sigma_fp >>= fun () -> pi_gen_free_vars pi_fp) - - -let footprint_free_vars prop = Sequence.Generator.run (footprint_gen_free_vars prop) - let gen_free_vars {sigma; sigma_fp; sub; pi; pi_fp} = let open Sequence.Generator in sigma_gen_free_vars sigma @@ -370,6 +363,16 @@ let gen_free_vars {sigma; sigma_fp; sub; pi; pi_fp} = let free_vars prop = Sequence.Generator.run (gen_free_vars prop) +let seq_max_stamp predicate seq = + seq |> Sequence.filter ~f:predicate |> Sequence.map ~f:Ident.get_stamp + |> Sequence.max_elt ~compare:Int.compare + |> Option.value ~default:0 + + +let all_true _ = true + +let max_stamp ?(f = all_true) prop = seq_max_stamp f (free_vars prop) + let exposed_gen_free_vars prop = gen_free_vars (unsafe_cast_to_normal prop) let sorted_gen_free_vars prop = exposed_gen_free_vars (expose_sorted prop) @@ -2490,10 +2493,6 @@ let prop_iter_footprint_gen_free_vars {pit_sigma_fp; pit_pi_fp} = Sequence.Generator.(sigma_gen_free_vars pit_sigma_fp >>= fun () -> pi_gen_free_vars pit_pi_fp) -let prop_iter_footprint_free_vars iter = - Sequence.Generator.run (prop_iter_footprint_gen_free_vars iter) - - (** Find fav of the iterator *) let prop_iter_gen_free_vars ({pit_sub; pit_pi; pit_newpi; pit_old; pit_new; pit_curr} as iter) = let open Sequence.Generator in @@ -2512,6 +2511,8 @@ let prop_iter_gen_free_vars ({pit_sub; pit_pi; pit_newpi; pit_old; pit_new; pit_ let prop_iter_free_vars iter = Sequence.Generator.run (prop_iter_gen_free_vars iter) +let prop_iter_max_stamp ?(f = all_true) iter = seq_max_stamp f (prop_iter_free_vars iter) + (** Extract the sigma part of the footprint *) let prop_iter_get_footprint_sigma iter = iter.pit_sigma_fp diff --git a/infer/src/biabduction/Prop.mli b/infer/src/biabduction/Prop.mli index 7b57ba61b..d0069db2d 100644 --- a/infer/src/biabduction/Prop.mli +++ b/infer/src/biabduction/Prop.mli @@ -82,6 +82,8 @@ val d_prop : 'a t -> unit val d_proplist_with_typ : 'a t list -> unit +val max_stamp : ?f:(Ident.t -> bool) -> normal t -> int + val pi_free_vars : pi -> Ident.t Sequence.t val sigma_free_vars : sigma -> Ident.t Sequence.t @@ -90,8 +92,6 @@ val free_vars : normal t -> Ident.t Sequence.t val gen_free_vars : normal t -> (unit, Ident.t) Sequence.Generator.t -val footprint_free_vars : normal t -> Ident.t Sequence.t - val sorted_gen_free_vars : sorted t -> (unit, Ident.t) Sequence.Generator.t val non_pure_free_vars : normal t -> Ident.t Sequence.t @@ -295,11 +295,8 @@ val prop_iter_update_current : 'a prop_iter -> hpred -> 'a prop_iter val prop_iter_prev_then_insert : 'a prop_iter -> hpred -> 'a prop_iter (** Insert before the current element of the iterator. *) -val prop_iter_footprint_free_vars : 'a prop_iter -> Ident.t Sequence.t -(** Find fav of the footprint part of the iterator *) - -val prop_iter_free_vars : 'a prop_iter -> Ident.t Sequence.t -(** Find fav of the iterator *) +val prop_iter_max_stamp : ?f:(Ident.t -> bool) -> 'a prop_iter -> int +(** Find the maximum stamp of a free variable of a certain kind. *) val prop_iter_get_footprint_sigma : 'a prop_iter -> hpred list (** Extract the sigma part of the footprint *) diff --git a/infer/src/biabduction/Rearrange.ml b/infer/src/biabduction/Rearrange.ml index 700d2d6bc..4d7569a52 100644 --- a/infer/src/biabduction/Rearrange.ml +++ b/infer/src/biabduction/Rearrange.ml @@ -522,8 +522,6 @@ let prop_iter_check_fields_ptsto_shallow tenv iter lexp = check_offset se offset -let id_max_stamp curr_max id = max curr_max (Ident.get_stamp id) - (** [prop_iter_extend_ptsto iter lexp] extends the current psto predicate in [iter] with enough fields to follow the path in [lexp] -- field splitting model. It also materializes all @@ -534,7 +532,7 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst = Sil.d_exp lexp ; L.d_ln () ) ; let offset = Sil.exp_get_offsets lexp in - let max_stamp = Prop.prop_iter_free_vars iter |> Sequence.fold ~init:0 ~f:id_max_stamp in + let max_stamp = Prop.prop_iter_max_stamp iter in let extend_footprint_pred = function | Sil.Hpointsto (e, se, te) -> let atoms_se_te_list = @@ -677,7 +675,7 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst = 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_to_prop pname tenv prop (lexp, typ) inst = - let max_stamp = Prop.footprint_free_vars prop |> Sequence.fold ~init:0 ~f:id_max_stamp in + let max_stamp = Prop.max_stamp ~f:Ident.is_footprint prop in let ptsto, ptsto_foot, atoms = mk_ptsto_exp_footprint pname tenv prop (lexp, typ) (ref max_stamp) inst in @@ -1046,9 +1044,7 @@ let prop_iter_add_hpred_footprint pname tenv orig_prop iter (lexp, typ) inst = L.d_str "typ:" ; Typ.d_full typ ; L.d_ln () ) ; - let max_stamp = - Prop.prop_iter_footprint_free_vars iter |> Sequence.fold ~init:0 ~f:id_max_stamp - in + let max_stamp = Prop.prop_iter_max_stamp ~f:Ident.is_footprint iter in let ptsto, ptsto_foot, atoms = mk_ptsto_exp_footprint pname tenv orig_prop (lexp, typ) (ref max_stamp) inst in @@ -1127,7 +1123,7 @@ let iter_rearrange_ptsto pname tenv orig_prop iter lexp inst = check_field_splitting () ; match Prop.prop_iter_current tenv iter with | Sil.Hpointsto (e, se, te), offset -> - let max_stamp = Prop.prop_iter_free_vars iter |> Sequence.fold ~init:0 ~f:id_max_stamp in + let max_stamp = Prop.prop_iter_max_stamp iter in let atoms_se_te_list = strexp_extend_values pname tenv orig_prop false Ident.kprimed (ref max_stamp) se te offset inst diff --git a/infer/tests/codetoanalyze/c/biabduction/issues.exp b/infer/tests/codetoanalyze/c/biabduction/issues.exp index 224380184..5e2935d53 100644 --- a/infer/tests/codetoanalyze/c/biabduction/issues.exp +++ b/infer/tests/codetoanalyze/c/biabduction/issues.exp @@ -4,5 +4,6 @@ codetoanalyze/c/biabduction/example.c, foo, 2, NULL_DEREFERENCE, B1, ERROR, [sta codetoanalyze/c/biabduction/example.c, global_addr_alias_bad, 3, NULL_DEREFERENCE, B1, ERROR, [start of procedure global_addr_alias_bad(),Taking true branch] codetoanalyze/c/biabduction/example.c, local_addr_noalias_bad, 4, NULL_DEREFERENCE, B1, ERROR, [start of procedure local_addr_noalias_bad(),Taking true branch] codetoanalyze/c/biabduction/example.c, null_dereference_following_function_pointer_call_bad, 4, NULL_DEREFERENCE, B1, ERROR, [start of procedure null_dereference_following_function_pointer_call_bad(),Skipping __function_pointer__(): unresolved function pointer] +codetoanalyze/c/biabduction/nulluse.c, fail, 2, NULL_DEREFERENCE, B5, ERROR, [start of procedure fail(),Taking true branch] codetoanalyze/c/biabduction/shift.c, return_null_deref1_bad, 2, NULL_DEREFERENCE, B5, ERROR, [start of procedure return_null_deref1_bad(),start of procedure return_depends_on_lshift(),Taking true branch,return from a call to return_depends_on_lshift] codetoanalyze/c/biabduction/shift.c, return_null_deref2_bad, 2, NULL_DEREFERENCE, B5, ERROR, [start of procedure return_null_deref2_bad(),start of procedure return_depends_on_rshift(),Taking true branch,return from a call to return_depends_on_rshift] diff --git a/infer/tests/codetoanalyze/c/biabduction/nulluse.c b/infer/tests/codetoanalyze/c/biabduction/nulluse.c new file mode 100644 index 000000000..200ec4e46 --- /dev/null +++ b/infer/tests/codetoanalyze/c/biabduction/nulluse.c @@ -0,0 +1,41 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +#include + +void (*global)(void**); + +struct T { + void (*go)(); +}; + +struct S { + struct T* t; + void* x; +}; + +void doit(void** x) { + if (global != 0) { + global(x); + } +} + +void f(struct S* s) { + if (s == 0) + return; + doit(&s->x); + if (s->t->go) { // should *not* give NULL_TEST_AFTER_DEREFERENCE + s->t->go(); + } +} + +void fail(int* x) { + if (x == 0) { + *x = 1; // should give NULL_DEREFERENCE + } +} + +int main() {}