[biabduction] Simplify postconditions after re-execution.

Summary:
This applies some simplifications that were previously
done after footprint (and therefore lost), and some
simplifications that require looking at both pre and
post.

Reviewed By: ngorogiannis

Differential Revision: D19035494

fbshipit-source-id: bad79534a

infer/src/IR/Ident.ml

@@ -256,3 +256,9 @@ let hashqueue_of_sequence ?init s =
 
 
 let set_of_sequence ?(init = Set.empty) s = Sequence.fold s ~init ~f:(fun ids id -> Set.add id ids)
+
+let counts_of_sequence seq =
+  let h = Hash.create (Sequence.length seq) in
+  let get id = Option.value (Hash.find_opt h id) ~default:0 in
+  let bump id = Hash.replace h id (1 + get id) in
+  Sequence.iter ~f:bump seq ; get

infer/src/IR/Ident.mli

@@ -139,3 +139,5 @@ val to_string : t -> string
 val hashqueue_of_sequence : ?init:unit HashQueue.t -> t Sequence.t -> unit HashQueue.t
 
 val set_of_sequence : ?init:Set.t -> t Sequence.t -> Set.t
+
+val counts_of_sequence : t Sequence.t -> t -> int

infer/src/biabduction/Abs.ml

@@ -1152,6 +1152,92 @@ let check_junk pname tenv prop =
   else Prop.normalize tenv (Prop.set prop ~sigma:sigma_new ~sigma_fp:sigma_fp_new)
 
 
+(** Removes (pure) atoms (such as v=E) containing a variable v that (a) has no other occurrence and
+    (b) [count v] is 0. The default count is the constant 0. One should use the argument count if
+    the proposition being simplified should make sense in a larger scope, which is not seen;
+    [count v] should give the number of occurrences of v in the context. *)
+let remove_pure_garbage tenv ?(count = fun _ -> 0) prop =
+  if Prop.has_footprint prop then L.d_warning "Abs.remove_pure_garbage ignores footprint" ;
+  (* Normalization may change counts of occurrences. Which free variables we drop depends on counts.
+     Dropping variables involves exposing the Prop.t, so we must necessarily re-normalize. Since we change
+     counts again, other variables may become dropable. We start with normalization, which empirically leads
+     to more dropping. *)
+  let changed = ref false in
+  let rec go prop =
+    let propcount = prop |> Prop.free_vars |> Ident.counts_of_sequence in
+    let prop = Prop.set prop ~pi:(Prop.get_pure prop) ~sub:Sil.sub_empty in
+    let drop id = Int.equal 1 (count id + propcount id) in
+    let keep atom = not (Sequence.exists ~f:drop (Sil.atom_free_vars atom)) in
+    let pi = List.filter ~f:keep prop.Prop.pi in
+    let dropped = List.length pi < List.length prop.Prop.pi in
+    changed := !changed || dropped ;
+    let prop = Prop.set ~pi prop in
+    let prop = Prop.normalize tenv prop in
+    if dropped then go prop else prop
+  in
+  (go prop, !changed)
+
+
+(* During re-execution, free variables in Prop.t have the whole spec as their scope. Thus, most
+functions in Prop abstain from dropping free variables. Here, however, we can do it. Let's call an
+atom an orphan when it contains a variable v that does not occur anywhere else in the spec. Orphans
+can be dropped. Alpha-renaming can create orphans. Thus, we will perform a best-effort fixpoint
+computation (rename, drop)*, stopping when the last drop is a no-op. *)
+let abstract_spec pname tenv spec =
+  let open BiabductionSummary in
+  let rename spec = spec_normalize tenv spec in
+  let drop spec =
+    let changed = ref false in
+    let precount = spec.pre |> Jprop.to_prop |> Prop.free_vars |> Ident.counts_of_sequence in
+    let update_post (p, path) =
+      let p, dropped = remove_pure_garbage tenv p ~count:precount in
+      changed := !changed || dropped ;
+      (p, path)
+    in
+    let posts = List.map ~f:update_post spec.posts in
+    let spec = {spec with posts} in
+    (spec, !changed)
+  in
+  let rec loop spec =
+    let s1 = rename spec in
+    let s2, changed = drop (expose s1) in
+    if changed then loop s2 else s1
+  in
+  let collapse_posts spec =
+    let spec = expose spec in
+    let implies (prop1, _path1) (prop2, _path2) =
+      (* TODO(rgrigore): [Prover.check_implication] gives up immediately if the consequence contains
+         a disequality. As a workaround, here we drop pure facts from the consequent that are known to
+         be true. *)
+      let module AtomSet = Caml.Set.Make (struct
+        type t = Sil.atom
+
+        let compare = Sil.compare_atom
+      end) in
+      let pre_pure =
+        let pre = Jprop.to_prop spec.pre in
+        AtomSet.of_list (Prop.get_pure pre)
+      in
+      let prop1_pure = AtomSet.of_list (Prop.get_pure prop1) in
+      let known = AtomSet.union pre_pure prop1_pure in
+      let toprove = AtomSet.of_list prop2.Prop.pi in
+      let toprove = AtomSet.diff toprove known in
+      let prop2 = Prop.set prop2 ~pi:(AtomSet.elements toprove) in
+      Prover.check_implication pname tenv prop1 prop2
+    in
+    let rec filter kept x unseen =
+      (* INV: if a is kept and b is kept or unseen then (not (implies a b)).
+         We keep x unless that would break the invariant. *)
+      let others = List.rev_append kept unseen in
+      let kept = if List.exists ~f:(implies x) others then kept else x :: kept in
+      match unseen with [] -> kept | y :: unseen -> filter kept y unseen
+    in
+    let posts = match spec.posts with [] | [_] -> spec.posts | p :: posts -> filter [] p posts in
+    {spec with posts}
+  in
+  rename (collapse_posts (loop spec))
+
+
 (** Check whether the prop contains junk. If it does, and [Config.allowleak] is true, remove the
     junk, otherwise raise a Leak exception. *)
 let abstract_junk pname tenv prop =

infer/src/biabduction/Abs.mli

@@ -16,6 +16,11 @@ type rules
 val abstract : Typ.Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t
 (** Abstract a proposition. *)
 
+val abstract_spec :
+  Typ.Procname.t -> Tenv.t -> Prop.normal BiabductionSummary.spec -> BiabductionSummary.NormSpec.t
+(** Normalizes names and applies simplifications, soem of which require looking at both pre and
+    post. *)
+
 val abstract_junk : Typ.Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t
 (** Check whether the prop contains junk. If it does, and [Config.allowleak] is true, remove the
     junk, otherwise raise a Leak exception. *)

infer/src/biabduction/BiabductionSummary.ml

@@ -126,6 +126,13 @@ module Jprop = struct
     do_filter [] jpl
 
 
+  let shallow_map ~f = function
+    | Prop (n, p) ->
+        Prop (n, f p)
+    | Joined (n, p, jp1, jp2) ->
+        Joined (n, f p, jp1, jp2)
+
+
   let rec map (f : 'a Prop.t -> 'b Prop.t) = function
     | Prop (n, p) ->
         Prop (n, f p)
@@ -168,17 +175,17 @@ module NormSpec : sig
 
   val normalize : Tenv.t -> Prop.normal spec -> t
 
-  val tospecs : t list -> Prop.normal spec list
-
   val compact : Sil.sharing_env -> t -> t
   (** Return a compact representation of the spec *)
 
+  val tospec : t -> Prop.normal spec
+
   val erase_join_info_pre : Tenv.t -> t -> t
   (** Erase join info from pre of spec *)
 end = struct
   type t = Prop.normal spec
 
-  let tospecs specs = specs
+  let tospec spec = spec
 
   let gen_free_vars tenv (spec : Prop.normal spec) =
     let open Sequence.Generator in
@@ -197,7 +204,6 @@ end = struct
     ; visited= spec.visited }
 
 
-  (** Convert spec into normal form w.r.t. variable renaming *)
   let normalize tenv (spec : Prop.normal spec) : Prop.normal spec =
     let idlist = free_vars tenv spec |> Ident.hashqueue_of_sequence |> Ident.HashQueue.keys in
     let count = ref 0 in
@@ -225,11 +231,13 @@ end = struct
     normalize tenv spec'
 end
 
-(** Convert spec into normal form w.r.t. variable renaming *)
+(** Convert spec into normal form *)
 let spec_normalize = NormSpec.normalize
 
+let expose = NormSpec.tospec
+
 (** Cast a list of normalized specs to a list of specs *)
-let normalized_specs_to_specs = NormSpec.tospecs
+let normalized_specs_to_specs = List.map ~f:NormSpec.tospec
 
 type phase = FOOTPRINT | RE_EXECUTION [@@deriving compare]
 
@@ -279,11 +287,14 @@ let pp_specs pe fmt specs =
           F.fprintf fmt "%a<br>@\n" (pp_spec0 pe (Some (cnt + 1, total))) spec )
 
 
-let get_specs_from_preposts preposts = Option.value_map ~f:NormSpec.tospecs ~default:[] preposts
+let get_specs_from_preposts preposts =
+  Option.value_map ~f:(List.map ~f:NormSpec.tospec) ~default:[] preposts
+
 
 type t = {preposts: NormSpec.t list; phase: phase}
 
 let opt_get_phase = function None -> FOOTPRINT | Some {phase} -> phase
 
 let pp pe fmt {preposts; phase} =
-  F.fprintf fmt "phase= %s@\n%a" (string_of_phase phase) (pp_specs pe) (NormSpec.tospecs preposts)
+  F.fprintf fmt "phase= %s@\n%a" (string_of_phase phase) (pp_specs pe)
+    (List.map ~f:NormSpec.tospec preposts)

infer/src/biabduction/BiabductionSummary.mli

@@ -37,6 +37,9 @@ module Jprop : sig
   val map : ('a Prop.t -> 'b Prop.t) -> 'a t -> 'b t
   (** map the function to each prop in the jprop, pointwise *)
 
+  val shallow_map : f:('a Prop.t -> 'a Prop.t) -> 'a t -> 'a t
+  (** map f over the top-level prop *)
+
   val to_prop : 'a t -> 'a Prop.t
   (** Extract the toplevel jprop of a prop *)
 end
@@ -62,13 +65,15 @@ module NormSpec : sig
   (** Erase join info from pre of spec *)
 end
 
+val expose : NormSpec.t -> Prop.normal spec
+
 val normalized_specs_to_specs : NormSpec.t list -> Prop.normal spec list
 (** Cast a list of normalized specs to a list of specs *)
 
 val pp_spec : Format.formatter -> _ spec -> unit
 
 val spec_normalize : Tenv.t -> Prop.normal spec -> NormSpec.t
-(** Convert spec into normal form w.r.t. variable renaming *)
+(** Convert spec into normal form. *)
 
 type phase = FOOTPRINT | RE_EXECUTION
 

infer/src/biabduction/Prop.ml

@@ -47,6 +47,8 @@ module Core : sig
     ; pi_fp: pi  (** abduced pure part *) }
   [@@deriving compare]
 
+  val has_footprint : 'a t -> bool
+
   val prop_emp : normal t
   (** Proposition [true /\ emp]. *)
 
@@ -72,6 +74,8 @@ end = struct
     ; pi_fp: pi  (** abduced pure part *) }
   [@@deriving compare]
 
+  let has_footprint {sigma_fp; pi_fp} = not (List.is_empty sigma_fp && List.is_empty pi_fp)
+
   (** Proposition [true /\ emp]. *)
   let prop_emp : normal t = {sub= Sil.sub_empty; pi= []; sigma= []; pi_fp= []; sigma_fp= []}
 

infer/src/biabduction/Prop.mli

@@ -43,6 +43,9 @@ type struct_init_mode = No_init | Fld_init
 
 (** {2 Basic Functions for propositions} *)
 
+val has_footprint : 'a t -> bool
+(** sigma_fp is nonempty or pi_fp is nonempty *)
+
 val compare_prop : 'a t -> 'a t -> int
 (** Compare propositions *)
 

infer/src/biabduction/interproc.ml

@@ -789,14 +789,7 @@ let execute_filter_prop summary exe_env tenv proc_cfg
       (plist, visited)
     in
     let pre =
-      let p =
-        PropUtil.remove_locals_ret tenv pdesc (BiabductionSummary.Jprop.to_prop precondition)
-      in
-      match precondition with
-      | BiabductionSummary.Jprop.Prop (n, _) ->
-          BiabductionSummary.Jprop.Prop (n, p)
-      | BiabductionSummary.Jprop.Joined (n, _, jp1, jp2) ->
-          BiabductionSummary.Jprop.Joined (n, p, jp1, jp2)
+      BiabductionSummary.Jprop.shallow_map ~f:(PropUtil.remove_locals_ret tenv pdesc) precondition
     in
     let spec = BiabductionSummary.{pre; posts; visited} in
     L.d_decrease_indent () ; do_after_node init_node ; Some spec
@@ -867,7 +860,7 @@ let perform_analysis_phase exe_env tenv (summary : Summary.t) (proc_cfg : ProcCf
               (Localise.verbatim_desc "Leak_while_collecting_specs_after_footprint")
           in
           Reporting.log_issue_deprecated_using_state Exceptions.Error pname exn ;
-          (* retuning no specs *) []
+          (* returning no specs *) []
       in
       (specs, BiabductionSummary.FOOTPRINT)
     in
@@ -1050,8 +1043,9 @@ let update_specs tenv prev_summary phase (new_specs : BiabductionSummary.NormSpe
   in
   let res = ref [] in
   let convert pre (post_set, visited) =
+    let pname = Summary.get_proc_name prev_summary in
     res :=
-      BiabductionSummary.spec_normalize tenv
+      Abs.abstract_spec pname tenv
         BiabductionSummary.{pre; posts= Paths.PathSet.elements post_set; visited}
       :: !res
   in

infer/tests/build_systems/ant/issues.exp

@@ -114,7 +114,7 @@ codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.Nu
 codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefNullableRet(boolean):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure derefNullableRet(...),start of procedure nullableRet(...),Taking true branch,return from a call to Object NullPointerExceptions.nullableRet(boolean)]
 codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefUndefNullableRet():void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure derefUndefNullableRet(),Skipping undefNullableRet(): unknown method,Definition of undefNullableRet()]
 codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefUndefNullableRetWrapper():void, 1, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure derefUndefNullableRetWrapper(),start of procedure undefNullableWrapper(),Skipping undefNullableRet(): unknown method,Definition of undefNullableRet(),return from a call to Object NullPointerExceptions.undefNullableWrapper()]
-codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterLoopOnList(codetoanalyze.java.infer.NullPointerExceptions$L):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure dereferenceAfterLoopOnList(...),start of procedure returnsNullAfterLoopOnList(...),Taking true branch,Taking false branch,return from a call to Object NullPointerExceptions.returnsNullAfterLoopOnList(NullPointerExceptions$L)]
+codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterLoopOnList(codetoanalyze.java.infer.NullPointerExceptions$L):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure dereferenceAfterLoopOnList(...),start of procedure returnsNullAfterLoopOnList(...),Taking true branch,Taking true branch,Taking false branch,return from a call to Object NullPointerExceptions.returnsNullAfterLoopOnList(NullPointerExceptions$L)]
 codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterUnlock1(java.util.concurrent.locks.Lock):void, 4, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure dereferenceAfterUnlock1(...),Skipping toString(): unknown method]
 codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterUnlock2(java.util.concurrent.locks.Lock):void, 6, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure dereferenceAfterUnlock2(...),Skipping toString(): unknown method]
 codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.hashmapNPE(java.util.HashMap,java.lang.Object):java.lang.String, 1, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hashmapNPE(...)]

infer/tests/codetoanalyze/java/infer/issues.exp

@@ -119,7 +119,7 @@ codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.Nu
 codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefNullableRet(boolean):void, 2, NULL_DEREFERENCE, B2, ERROR, [start of procedure derefNullableRet(...),start of procedure nullableRet(...),Taking true branch,return from a call to Object NullPointerExceptions.nullableRet(boolean)]
 codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefUndefNullableRet():void, 2, NULL_DEREFERENCE, B1, ERROR, [start of procedure derefUndefNullableRet(),Skipping undefNullableRet(): unknown method,Definition of undefNullableRet()]
 codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefUndefNullableRetWrapper():void, 1, NULL_DEREFERENCE, B1, ERROR, [start of procedure derefUndefNullableRetWrapper(),start of procedure undefNullableWrapper(),Skipping undefNullableRet(): unknown method,Definition of undefNullableRet(),return from a call to Object NullPointerExceptions.undefNullableWrapper()]
-codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterLoopOnList(codetoanalyze.java.infer.NullPointerExceptions$L):void, 2, NULL_DEREFERENCE, B2, ERROR, [start of procedure dereferenceAfterLoopOnList(...),start of procedure returnsNullAfterLoopOnList(...),Taking true branch,Taking false branch,return from a call to Object NullPointerExceptions.returnsNullAfterLoopOnList(NullPointerExceptions$L)]
+codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterLoopOnList(codetoanalyze.java.infer.NullPointerExceptions$L):void, 2, NULL_DEREFERENCE, B2, ERROR, [start of procedure dereferenceAfterLoopOnList(...),start of procedure returnsNullAfterLoopOnList(...),Taking true branch,Taking true branch,Taking false branch,return from a call to Object NullPointerExceptions.returnsNullAfterLoopOnList(NullPointerExceptions$L)]
 codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterUnlock1(java.util.concurrent.locks.Lock):void, 4, NULL_DEREFERENCE, B1, ERROR, [start of procedure dereferenceAfterUnlock1(...),Skipping toString(): unknown method]
 codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterUnlock2(java.util.concurrent.locks.Lock):void, 6, NULL_DEREFERENCE, B1, ERROR, [start of procedure dereferenceAfterUnlock2(...),Skipping toString(): unknown method]
 codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.hashmapNPE(java.util.HashMap,java.lang.Object):java.lang.String, 1, NULL_DEREFERENCE, B2, ERROR, [start of procedure hashmapNPE(...)]