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

@@ -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
 

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 *)

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

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]

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 <stdlib.h>
+
+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() {}