[biabduction] Do not join postconditions after the footprint phase.

Summary:
The re-execution phase uses only the preconditions found by the footprint phase.  Thus, Infer should
not spend time optimizing POSTconditions. These are used only to find custom errors.

Reviewed By: jvillard

Differential Revision: D19035495

fbshipit-source-id: d52b82733

infer/man/man1/infer-full.txt

@@ -1725,12 +1725,6 @@ INTERNAL OPTIONS
        --sources-reset
            Set --sources to the empty list.
 
-       --spec-abs-level int
-           Set the level of abstracting the postconditions of discovered
-           specs:           - 0 = nothing special
-           - 1 = filter out redundant posts implied by other posts
-           
-
        --specs-library,-L +dir|jar
            Search for .spec files in given directory or jar file
 

infer/src/base/Config.ml

@@ -2221,14 +2221,6 @@ and starvation_whole_program =
     "Run whole-program starvation analysis"
 
 
-and spec_abs_level =
-  CLOpt.mk_int ~deprecated:["spec_abs_level"] ~long:"spec-abs-level" ~default:1 ~meta:"int"
-    {|Set the level of abstracting the postconditions of discovered specs:
-- 0 = nothing special
-- 1 = filter out redundant posts implied by other posts
-|}
-
-
 and specs_library =
   let specs_library =
     CLOpt.mk_path_list ~deprecated:["lib"] ~long:"specs-library" ~short:'L' ~meta:"dir|jar"
@@ -3194,8 +3186,6 @@ and sources = !sources
 
 and sourcepath = !sourcepath
 
-and spec_abs_level = !spec_abs_level
-
 and sqlite_cache_size = !sqlite_cache_size
 
 and sqlite_page_size = !sqlite_page_size

infer/src/base/Config.mli

@@ -652,8 +652,6 @@ val source_files_type_environment : bool
 
 val source_preview : bool
 
-val spec_abs_level : int
-
 val specs_library : string list
 
 val sqlite_cache_size : int

infer/src/biabduction/Dom.ml

@@ -2048,17 +2048,6 @@ let list_reduce name dd f list =
   reduce [] list
 
 
-let pathset_collapse_impl pname tenv pset =
-  let f x y =
-    if Prover.check_implication pname tenv x (Prop.expose y) then Some y
-    else if Prover.check_implication pname tenv y (Prop.expose x) then Some x
-    else None
-  in
-  let plist = Paths.PathSet.elements pset in
-  let plist' = list_reduce "JOIN_IMPL" Prop.d_prop f plist in
-  Paths.PathSet.from_renamed_list plist'
-
-
 let jprop_partial_join tenv mode jp1 jp2 =
   let p1, p2 =
     ( Prop.expose (BiabductionSummary.Jprop.to_prop jp1)
@@ -2103,13 +2092,6 @@ let proplist_collapse_pre tenv plist =
   List.map ~f:fst (proplist_collapse tenv JoinState.Pre plist')
 
 
-let pathset_collapse tenv pset =
-  let plist = Paths.PathSet.elements pset in
-  let plist' = proplist_collapse tenv JoinState.Post plist in
-  Paths.PathSet.from_renamed_list
-    (List.map ~f:(fun (p, path) -> (BiabductionSummary.Jprop.to_prop p, path)) plist')
-
-
 let pathset_join pname tenv (pset1 : Paths.PathSet.t) (pset2 : Paths.PathSet.t) :
     Paths.PathSet.t * Paths.PathSet.t =
   let mode = JoinState.Post in

infer/src/biabduction/Dom.mli

@@ -23,11 +23,6 @@ val pathset_join :
 val proplist_collapse_pre :
   Tenv.t -> Prop.normal Prop.t list -> Prop.normal BiabductionSummary.Jprop.t list
 
-val pathset_collapse : Tenv.t -> Paths.PathSet.t -> Paths.PathSet.t
-
-val pathset_collapse_impl : Typ.Procname.t -> Tenv.t -> Paths.PathSet.t -> Paths.PathSet.t
-(** reduce the pathset only based on implication checking. *)
-
 (** {2 Meet Operators} *)
 
 val propset_meet_generate_pre : Tenv.t -> Propset.t -> Prop.normal Prop.t list

infer/src/biabduction/interproc.ml

@@ -173,21 +173,18 @@ let collect_do_abstract_pre pname tenv (pset : Propset.t) : Propset.t =
 
 
 let collect_do_abstract_post pname tenv (pathset : Paths.PathSet.t) : Paths.PathSet.t =
-  let abs_option p =
+  if !BiabductionConfig.footprint then
+    L.die InternalError
+      "Interproc.collect_do_abstract_post ignores the _fp part of propositions, so it should only \
+       be used during re-execution." ;
+  let abstract_o p =
     if Prover.check_inconsistency tenv p then None else Some (Abs.abstract pname tenv p)
   in
-  if !BiabductionConfig.footprint then
+  Paths.PathSet.map_option abstract_o pathset
-    BiabductionConfig.run_in_re_execution_mode (Paths.PathSet.map_option abs_option) pathset
-  else Paths.PathSet.map_option abs_option pathset
 
 
 let do_join_pre plist = Dom.proplist_collapse_pre plist
 
-let do_join_post pname tenv (pset : Paths.PathSet.t) =
-  if Config.spec_abs_level <= 0 then Dom.pathset_collapse tenv pset
-  else Dom.pathset_collapse tenv (Dom.pathset_collapse_impl pname tenv pset)
-
-
 let do_meet_pre tenv pset =
   if Config.meet_level > 0 then Dom.propset_meet_generate_pre tenv pset
   else Propset.to_proplist pset
@@ -537,12 +534,6 @@ let collect_analysis_result tenv wl proc_cfg : Paths.PathSet.t =
   Paths.PathSet.map (remove_locals_formals_and_check tenv proc_cfg) pathset
 
 
-module Pmap = Caml.Map.Make (struct
-  type t = Prop.normal Prop.t
-
-  let compare = Prop.compare_prop
-end)
-
 let vset_add_path vset path =
   Paths.Path.fold_all_nodes_nocalls path ~init:vset ~f:(fun vset n -> Procdesc.NodeSet.add n vset)
 
@@ -570,9 +561,13 @@ let compute_visited vset =
   !res
 
 
-(** Extract specs from a pathset *)
+(* Extract specs from a pathset, after the footprint phase. The postconditions will be thrown away
+  by the re-execution phase, but they are first used to detect custom errors. *)
 let extract_specs tenv pdesc pathset : Prop.normal BiabductionSummary.spec list =
-  let pname = Procdesc.get_proc_name pdesc in
+  if not !BiabductionConfig.footprint then
+    L.die InternalError
+      "Interproc.extract_specs should not be used for footprint but not for re-execution, because \
+       it does not optimize postconditions." ;
   let sub =
     let fav =
       Paths.PathSet.fold
@@ -583,54 +578,35 @@ let extract_specs tenv pdesc pathset : Prop.normal BiabductionSummary.spec list
     let sub_list = List.map ~f:(fun id -> (id, Exp.Var (Ident.create_fresh Ident.knormal))) fav in
     Predicates.subst_of_list sub_list
   in
-  let pre_post_visited_list =
+  let pre_post_list =
-    let pplist = Paths.PathSet.elements pathset in
     let f (prop, path) =
-      let _, prop' = PropUtil.remove_locals_formals tenv pdesc prop in
+      let _remaining, prop = PropUtil.remove_locals_formals tenv pdesc prop in
-      let prop'' = Abs.abstract pname tenv prop' in
+      let prop = Abs.abstract (Procdesc.get_proc_name pdesc) tenv prop in
-      let pre, post = Prop.extract_spec prop'' in
+      let pre, post = Prop.extract_spec prop in
-      let pre' = Prop.normalize tenv (Prop.prop_sub sub pre) in
+      let pre = Prop.normalize tenv (Prop.prop_sub sub pre) in
-      let post' =
+      let post = PropUtil.remove_seed_vars tenv (Prop.prop_sub sub post) in
-        if Prover.check_inconsistency_base tenv prop then None
+      (pre, (post, path))
-        else Some (Prop.normalize tenv (Prop.prop_sub sub post), path)
+    in
-      in
+    let compare (prop1, _) (prop2, _) = Prop.compare_prop prop1 prop2 in
-      let visited =
+    let break a b = not (Int.equal 0 (compare a b)) in
-        let vset = vset_add_path Procdesc.NodeSet.empty path in
+    let separate ps =
-        compute_visited vset
+      let pre =
-      in
+        match ps with
-      (pre', post', visited)
+        | (pre, _) :: _ ->
-    in
+            pre
-    List.map ~f pplist
+        | [] ->
-  in
+            L.die InternalError "Interproc.extract_specs: List.group outputs empty list??"
-  let pre_post_map =
-    let add map (pre, post, visited) =
-      let current_posts, current_visited =
-        try Pmap.find pre map
-        with Caml.Not_found -> (Paths.PathSet.empty, BiabductionSummary.Visitedset.empty)
-      in
-      let new_posts =
-        match post with
-        | None ->
-            current_posts
-        | Some (post, path) ->
-            Paths.PathSet.add_renamed_prop post path current_posts
-      in
-      let new_visited = BiabductionSummary.Visitedset.union visited current_visited in
-      Pmap.add pre (new_posts, new_visited) map
       in
-    List.fold ~f:add ~init:Pmap.empty pre_post_visited_list
+      let pposts = List.map ~f:snd ps in
+      (pre, pposts)
     in
-  let specs = ref [] in
+    pathset |> Paths.PathSet.elements |> List.map ~f |> List.sort ~compare |> List.group ~break
-  let add_spec pre ((posts : Paths.PathSet.t), visited) =
+    |> List.map ~f:separate
-    let posts' =
-      List.map
-        ~f:(fun (p, path) -> (PropUtil.remove_seed_vars tenv p, path))
-        (Paths.PathSet.elements (do_join_post pname tenv posts))
   in
-    let spec = BiabductionSummary.{pre= Jprop.Prop (1, pre); posts= posts'; visited} in
+  let mk_spec (pre, posts) =
-    specs := spec :: !specs
+    BiabductionSummary.{pre= Jprop.Prop (1, pre); posts; visited= Visitedset.empty}
   in
-  Pmap.iter add_spec pre_post_map ; !specs
+  List.map ~f:mk_spec pre_post_list
 
 
 let collect_postconditions wl tenv proc_cfg : Paths.PathSet.t * BiabductionSummary.Visitedset.t =