From 16402cddc09da7975e545c3f8945408c3311ff99 Mon Sep 17 00:00:00 2001
From: Cristiano Calcagno <cristianoc@fb.com>
Date: Wed, 24 Feb 2016 11:31:27 -0800
Subject: [PATCH] Save global state for abstraction for on-demand.

Reviewed By: sblackshear

Differential Revision: D2971122

fb-gh-sync-id: f7600f0
shipit-source-id: f7600f0
---
 infer/src/backend/abs.ml          | 288 +++++-------------------------
 infer/src/backend/abs.mli         |  32 ++--
 infer/src/backend/config.ml       |  19 +-
 infer/src/backend/dom.ml          |  29 ---
 infer/src/backend/fork.ml         |  29 +--
 infer/src/backend/fork.mli        |   2 +-
 infer/src/backend/inferanalyze.ml |  20 +--
 infer/src/backend/interproc.ml    | 128 +++++--------
 infer/src/backend/interproc.mli   |  15 --
 infer/src/backend/ondemand.ml     |   6 +
 infer/src/backend/symExec.ml      |  45 +++--
 infer/src/backend/utils.ml        |  25 ++-
 infer/src/backend/utils.mli       |   8 +
 13 files changed, 182 insertions(+), 464 deletions(-)

diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml
index fe7a7119e..53f84dddd 100644
--- a/infer/src/backend/abs.ml
+++ b/infer/src/backend/abs.ml
@@ -562,14 +562,34 @@ let discover_para_dll tenv p =
     | None -> paras
     | Some para -> if already_defined para paras then paras else para :: paras in
   IList.fold_left f [] candidates
-(******************  Start of Predicate Discovery  ******************)
+(******************  End of Predicate Discovery  ******************)
 
 (****************** Start of the ADT abs_rules ******************)
-type para_ty = SLL of Sil.hpara | DLL of Sil.hpara_dll
 
+(** Type of parameter for abstraction rules *)
+type para_ty =
+  | SLL of Sil.hpara
+  | DLL of Sil.hpara_dll
+
+(** Rule set: a list of rules of a given type *)
 type rule_set = para_ty * rule list
 
-type abs_rules = { mutable ar_default : rule_set list }
+type rules = rule_set list
+
+module Global =
+struct
+  let current_rules : rules ref =
+    ref []
+end
+
+let get_current_rules () =
+  !Global.current_rules
+
+let set_current_rules rules =
+  Global.current_rules := rules
+
+let reset_current_rules () =
+  Global.current_rules := []
 
 let eqs_sub subst eqs =
   IList.map (fun (e1, e2) -> (Sil.exp_sub subst e1, Sil.exp_sub subst e2)) eqs
@@ -658,30 +678,6 @@ let hpara_special_cases_dll hpara : Sil.hpara_dll list =
   let special_cases = sigma_special_cases hpara.Sil.evars_dll hpara.Sil.body_dll in
   IList.map update_para special_cases
 
-let abs_rules : abs_rules = { ar_default = [] }
-
-let abs_rules_reset () =
-  abs_rules.ar_default <- []
-
-let abs_rules_add rule_set : unit =
-  (*
-  let _ = match (fst rule_set) with
-  | SLL hpara -> L.out "@.@....Added Para: %a@.@." pp_hpara hpara
-  | DLL _ -> ()
-  in
-  *)
-  abs_rules.ar_default <- abs_rules.ar_default@[rule_set]
-
-let abs_rules_add_sll (para: Sil.hpara) : unit =
-  let rules = mk_rules_for_sll para in
-  let rule_set = (SLL para, rules) in
-  abs_rules_add rule_set
-
-let abs_rules_add_dll (para: Sil.hpara_dll) : unit =
-  let rules = mk_rules_for_dll para in
-  let rule_set = (DLL para, rules) in
-  abs_rules_add rule_set
-
 let abs_rules_apply_rsets (rsets: rule_set list) (p_in: Prop.normal Prop.t) : Prop.normal Prop.t =
   let apply_rule (changed, p) r =
     match (sigma_rewrite p r) with
@@ -700,7 +696,7 @@ let abs_rules_apply_rsets (rsets: rule_set list) (p_in: Prop.normal Prop.t) : Pr
 
 let abs_rules_apply_lists tenv (p_in: Prop.normal Prop.t) : Prop.normal Prop.t =
   let new_rsets = ref [] in
-  let def_rsets = abs_rules.ar_default in
+  let old_rsets = get_current_rules () in
   let rec discover_then_abstract p =
     let (closed_paras_sll, closed_paras_dll) =
       let paras_sll = discover_para tenv p in
@@ -723,18 +719,26 @@ let abs_rules_apply_lists tenv (p_in: Prop.normal Prop.t) : Prop.normal Prop.t =
         (closed_paras_sll, closed_paras_dll)
       end in
     let (todo_paras_sll, todo_paras_dll) =
-      let eq_sll para = function (SLL para', _) -> Match.hpara_iso para para' | _ -> false in
-      let eq_dll para = function (DLL para', _) -> Match.hpara_dll_iso para para' | _ -> false in
+      let eq_sll para rset = match rset with
+        | (SLL para', _) -> Match.hpara_iso para para'
+        | _ -> false in
+      let eq_dll para rset = match rset with
+        | (DLL para', _) -> Match.hpara_dll_iso para para'
+        | _ -> false in
       let filter_sll para =
-        not (IList.exists (eq_sll para) def_rsets) && not (IList.exists (eq_sll para) !new_rsets) in
+        not (IList.exists (eq_sll para) old_rsets) &&
+        not (IList.exists (eq_sll para) !new_rsets) in
       let filter_dll para =
-        not (IList.exists (eq_dll para) def_rsets) && not (IList.exists (eq_dll para) !new_rsets) in
+        not (IList.exists (eq_dll para) old_rsets) &&
+        not (IList.exists (eq_dll para) !new_rsets) in
       let todo_paras_sll = IList.filter filter_sll closed_paras_sll in
       let todo_paras_dll = IList.filter filter_dll closed_paras_dll in
       (todo_paras_sll, todo_paras_dll) in
     let f_recurse () =
-      let todo_rsets_sll = IList.map (fun para -> (SLL para, mk_rules_for_sll para)) todo_paras_sll in
-      let todo_rsets_dll = IList.map (fun para -> (DLL para, mk_rules_for_dll para)) todo_paras_dll in
+      let todo_rsets_sll =
+        IList.map (fun para -> (SLL para, mk_rules_for_sll para)) todo_paras_sll in
+      let todo_rsets_dll =
+        IList.map (fun para -> (DLL para, mk_rules_for_dll para)) todo_paras_dll in
       new_rsets := !new_rsets @ todo_rsets_sll @ todo_rsets_dll;
       let p' = abs_rules_apply_rsets todo_rsets_sll p in
       let p'' = abs_rules_apply_rsets todo_rsets_dll p' in
@@ -742,203 +746,16 @@ let abs_rules_apply_lists tenv (p_in: Prop.normal Prop.t) : Prop.normal Prop.t =
     match todo_paras_sll, todo_paras_dll with
     | [], [] -> p
     | _ -> f_recurse () in
-  let p1 = abs_rules_apply_rsets def_rsets p_in in
-  let p2 = if !Config.on_the_fly then discover_then_abstract p1 else p1
-  in
-  abs_rules.ar_default <- (def_rsets@(!new_rsets));
+  let p1 = abs_rules_apply_rsets old_rsets p_in in
+  let p2 = discover_then_abstract p1 in
+  let new_rules = old_rsets @ !new_rsets in
+  set_current_rules new_rules;
   p2
 
 let abs_rules_apply tenv (p_in: Prop.normal Prop.t) : Prop.normal Prop.t =
   abs_rules_apply_lists tenv p_in
 (****************** End of the ADT abs_rules ******************)
 
-(****************** Start of fns that add rules during preprocessing ******************)
-let is_simply_recursive tenv tname =
-  let typ = match Sil.tenv_lookup tenv tname with
-    | None -> assert false
-    | Some typ -> typ in
-  let filter (_, t, _) = match t with
-    | Sil.Tvar _ | Sil.Tint _ | Sil.Tfloat _ | Sil.Tvoid | Sil.Tfun _ | Sil.Tenum _ ->
-        false
-    | Sil.Tptr (Sil.Tvar tname', _) ->
-        Typename.equal tname tname'
-    | Sil.Tptr _ | Sil.Tstruct _ | Sil.Tarray _ ->
-        false in
-  match typ with
-  | Sil.Tvar _ ->
-      assert false (* there should be no indirection *)
-  | Sil.Tint _ | Sil.Tfloat _ | Sil.Tvoid | Sil.Tfun _ | Sil.Tptr _ | Sil.Tenum _ ->
-      None
-  | Sil.Tstruct { Sil.instance_fields } ->
-      begin
-        match (IList.filter filter instance_fields) with
-        | [(fld, _, _)] -> Some fld
-        | _ -> None
-      end
-  | Sil.Tarray _ ->
-      None
-
-let create_hpara_from_tname_flds tenv tname nfld sflds eflds inst =
-  let typ = match Sil.tenv_lookup tenv tname with
-    | Some typ -> typ
-    | None -> assert false in
-  let id_base = Ident.create_fresh Ident.kprimed in
-  let id_next = Ident.create_fresh Ident.kprimed in
-  let ids_shared = IList.map (fun _ -> Ident.create_fresh Ident.kprimed) sflds in
-  let ids_exist = IList.map (fun _ -> Ident.create_fresh Ident.kprimed) eflds in
-  let exp_base = Sil.Var id_base in
-  let fld_sexps =
-    let ids = id_next :: (ids_shared @ ids_exist) in
-    let flds = nfld :: (sflds @ eflds) in
-    let f fld id = (fld, Sil.Eexp (Sil.Var id, inst)) in
-    try IList.map2 f flds ids with Invalid_argument _ -> assert false in
-  let strexp_para = Sil.Estruct (fld_sexps, inst) in
-  let ptsto_para = Prop.mk_ptsto exp_base strexp_para (Sil.Sizeof (typ, Sil.Subtype.exact)) in
-  Prop.mk_hpara id_base id_next ids_shared ids_exist [ptsto_para]
-
-let create_dll_hpara_from_tname_flds tenv tname flink blink sflds eflds inst =
-  let typ = match Sil.tenv_lookup tenv tname with
-    | Some typ -> typ
-    | None -> assert false in
-  let id_iF = Ident.create_fresh Ident.kprimed in
-  let id_oB = Ident.create_fresh Ident.kprimed in
-  let id_oF = Ident.create_fresh Ident.kprimed in
-  let ids_shared = IList.map (fun _ -> Ident.create_fresh Ident.kprimed) sflds in
-  let ids_exist = IList.map (fun _ -> Ident.create_fresh Ident.kprimed) eflds in
-  let exp_iF = Sil.Var id_iF in
-  let fld_sexps =
-    let ids = id_oF:: id_oB :: (ids_shared @ ids_exist) in
-    let flds = flink:: blink:: (sflds @ eflds) in
-    let f fld id = (fld, Sil.Eexp (Sil.Var id, inst)) in
-    try IList.map2 f flds ids with Invalid_argument _ -> assert false in
-  let strexp_para = Sil.Estruct (fld_sexps, inst) in
-  let ptsto_para = Prop.mk_ptsto exp_iF strexp_para (Sil.Sizeof (typ, Sil.Subtype.exact)) in
-  Prop.mk_dll_hpara id_iF id_oB id_oF ids_shared ids_exist [ptsto_para]
-
-let create_hpara_two_ptsto tname1 tenv nfld1 dfld tname2 nfld2 inst =
-  let typ1 = match Sil.tenv_lookup tenv tname1 with
-    | Some typ -> typ
-    | None -> assert false in
-  let typ2 = match Sil.tenv_lookup tenv tname2 with
-    | Some typ -> typ
-    | None -> assert false in
-  let id_base = Ident.create_fresh Ident.kprimed in
-  let id_next = Ident.create_fresh Ident.kprimed in
-  let id_exist = Ident.create_fresh Ident.kprimed in
-  let exp_base = Sil.Var id_base in
-  let exp_exist = Sil.Var id_exist in
-  let fld_sexps1 =
-    let ids = [id_next; id_exist] in
-    let flds = [nfld1; dfld] in
-    let f fld id = (fld, Sil.Eexp (Sil.Var id, inst)) in
-    try IList.map2 f flds ids with Invalid_argument _ -> assert false in
-  let fld_sexps2 =
-    [(nfld2, Sil.Eexp (Sil.exp_zero, inst))] in
-  let strexp_para1 = Sil.Estruct (fld_sexps1, inst) in
-  let strexp_para2 = Sil.Estruct (fld_sexps2, inst) in
-  let ptsto_para1 = Prop.mk_ptsto exp_base strexp_para1 (Sil.Sizeof (typ1, Sil.Subtype.exact)) in
-  let ptsto_para2 = Prop.mk_ptsto exp_exist strexp_para2 (Sil.Sizeof (typ2, Sil.Subtype.exact)) in
-  Prop.mk_hpara id_base id_next [] [id_exist] [ptsto_para1; ptsto_para2]
-
-let create_hpara_dll_two_ptsto tenv tname1 flink_fld1 blink_fld1 dfld tname2 nfld2 inst =
-  let typ1 = match Sil.tenv_lookup tenv tname1 with
-    | Some typ -> typ
-    | None -> assert false in
-  let typ2 = match Sil.tenv_lookup tenv tname2 with
-    | Some typ -> typ
-    | None -> assert false in
-  let id_cell = Ident.create_fresh Ident.kprimed in
-  let id_blink = Ident.create_fresh Ident.kprimed in
-  let id_flink = Ident.create_fresh Ident.kprimed in
-  let id_exist = Ident.create_fresh Ident.kprimed in
-  let exp_cell = Sil.Var id_cell in
-  let exp_exist = Sil.Var id_exist in
-  let fld_sexps1 =
-    let ids = [ id_blink; id_flink; id_exist] in
-    let flds = [ blink_fld1; flink_fld1; dfld] in
-    let f fld id = (fld, Sil.Eexp (Sil.Var id, inst)) in
-    try IList.map2 f flds ids with Invalid_argument _ -> assert false in
-  let fld_sexps2 =
-    [(nfld2, Sil.Eexp (Sil.exp_zero, inst))] in
-  let strexp_para1 = Sil.Estruct (fld_sexps1, inst) in
-  let strexp_para2 = Sil.Estruct (fld_sexps2, inst) in
-  let ptsto_para1 = Prop.mk_ptsto exp_cell strexp_para1 (Sil.Sizeof (typ1, Sil.Subtype.exact)) in
-  let ptsto_para2 = Prop.mk_ptsto exp_exist strexp_para2 (Sil.Sizeof (typ2, Sil.Subtype.exact)) in
-  Prop.mk_dll_hpara id_cell id_blink id_flink [] [id_exist] [ptsto_para1; ptsto_para2]
-
-let create_hpara_from_tname_twoflds_hpara tenv tname fld_next fld_down para inst =
-  let typ = match Sil.tenv_lookup tenv tname with
-    | Some typ -> typ
-    | None -> assert false in
-  let id_base = Ident.create_fresh Ident.kprimed in
-  let id_next = Ident.create_fresh Ident.kprimed in
-  let id_down = Ident.create_fresh Ident.kprimed in
-  let exp_base = Sil.Var id_base in
-  let exp_next = Sil.Var id_next in
-  let exp_down = Sil.Var id_down in
-  let strexp = Sil.Estruct ([(fld_next, Sil.Eexp (exp_next, inst)); (fld_down, Sil.Eexp (exp_down, inst))], inst) in
-  let ptsto = Prop.mk_ptsto exp_base strexp (Sil.Sizeof (typ, Sil.Subtype.exact)) in
-  let lseg = Prop.mk_lseg Sil.Lseg_PE para exp_down Sil.exp_zero [] in
-  let body = [ptsto; lseg] in
-  Prop.mk_hpara id_base id_next [] [id_down] body
-
-let create_hpara_dll_from_tname_twoflds_hpara tenv tname fld_flink fld_blink fld_down para inst =
-  let typ = match Sil.tenv_lookup tenv tname with
-    | Some typ -> typ
-    | None -> assert false in
-  let id_cell = Ident.create_fresh Ident.kprimed in
-  let id_blink = Ident.create_fresh Ident.kprimed in
-  let id_flink = Ident.create_fresh Ident.kprimed in
-  let id_down = Ident.create_fresh Ident.kprimed in
-  let exp_cell = Sil.Var id_cell in
-  let exp_blink = Sil.Var id_blink in
-  let exp_flink = Sil.Var id_flink in
-  let exp_down = Sil.Var id_down in
-  let strexp = Sil.Estruct ([(fld_blink, Sil.Eexp (exp_blink, inst)); (fld_flink, Sil.Eexp (exp_flink, inst)); (fld_down, Sil.Eexp (exp_down, inst))], inst) in
-  let ptsto = Prop.mk_ptsto exp_cell strexp (Sil.Sizeof (typ, Sil.Subtype.exact)) in
-  let lseg = Prop.mk_lseg Sil.Lseg_PE para exp_down Sil.exp_zero [] in
-  let body = [ptsto; lseg] in
-  Prop.mk_dll_hpara id_cell id_blink id_flink [] [id_down] body
-
-let tname_list = Typename.TN_typedef (Mangled.from_string "list")
-let name_down = Ident.create_fieldname (Mangled.from_string "down") 0
-let tname_HSlist2 = Typename.TN_typedef (Mangled.from_string "HSlist2")
-let name_next = Ident.create_fieldname (Mangled.from_string "next") 0
-
-let tname_dllist = Typename.TN_typedef (Mangled.from_string "dllist")
-let name_Flink = Ident.create_fieldname (Mangled.from_string "Flink") 0
-let name_Blink = Ident.create_fieldname (Mangled.from_string "Blink") 0
-let tname_HOdllist = Typename.TN_typedef (Mangled.from_string "HOdllist")
-
-let create_absrules_from_tdecl tenv tname =
-  if (not (!Config.on_the_fly)) && Typename.equal tname tname_HSlist2 then
-    (* L.out "@[.... Adding Abstraction Rules for Nested Lists ....@\n@."; *)
-    let para1 = create_hpara_from_tname_flds tenv tname_list name_down [] [] Sil.inst_abstraction in
-    let para2 = create_hpara_from_tname_flds tenv tname_HSlist2 name_next [name_down] [] Sil.inst_abstraction in
-    let para_nested = create_hpara_from_tname_twoflds_hpara tenv tname_HSlist2 name_next name_down para1 Sil.inst_abstraction in
-    let para_nested_base = create_hpara_two_ptsto tname_HSlist2 tenv name_next name_down tname_list name_down Sil.inst_abstraction in
-    IList.iter abs_rules_add_sll [para_nested_base; para2; para_nested]
-  else if (not (!Config.on_the_fly)) && Typename.equal tname tname_dllist then
-    (* L.out "@[.... Adding Abstraction Rules for Doubly-linked Lists ....@\n@."; *)
-    let para = create_dll_hpara_from_tname_flds tenv tname_dllist name_Flink name_Blink [] [] Sil.inst_abstraction in
-    abs_rules_add_dll para
-  else if (not (!Config.on_the_fly)) && Typename.equal tname tname_HOdllist then
-    (* L.out "@[.... Adding Abstraction Rules for High-Order Doubly-linked Lists ....@\n@."; *)
-    let para1 = create_hpara_from_tname_flds tenv tname_list name_down [] [] Sil.inst_abstraction in
-    let para2 = create_dll_hpara_from_tname_flds tenv tname_HOdllist name_Flink name_Blink [name_down] [] Sil.inst_abstraction in
-    let para_nested = create_hpara_dll_from_tname_twoflds_hpara tenv tname_HOdllist name_Flink name_Blink name_down para1 Sil.inst_abstraction in
-    let para_nested_base = create_hpara_dll_two_ptsto tenv tname_HOdllist name_Flink name_Blink name_down tname_list name_down Sil.inst_abstraction in
-    IList.iter abs_rules_add_dll [para_nested_base; para2; para_nested]
-  else if (not (!Config.on_the_fly)) then
-    match is_simply_recursive tenv tname with
-    | None -> ()
-    | Some (fld) ->
-        (* L.out "@[.... Adding Abstraction Rules ....@\n@."; *)
-        let para = create_hpara_from_tname_flds tenv tname fld [] [] Sil.inst_abstraction in
-        abs_rules_add_sll para
-  else ()
-(****************** End of fns that add rules during preprocessing ******************)
-
 (****************** Start of Main Abstraction Functions ******************)
 let abstract_pure_part p ~(from_abstract_footprint: bool) =
   let do_pure pure =
@@ -1446,24 +1263,3 @@ let lifted_abstract pname tenv pset =
   abstracted_pset
 
 (***************** End of Main Abstraction Functions *****************)
-
-(*
-(** return a reachability function based on whether an id appears in several hpreds *)
-let reachable_when_in_several_hpreds sigma : Ident.t -> bool =
-  (* map id to hpreds in which it occurs *)
-  let (id_hpred_map : HpredSet.t IdMap.t ref) = ref IdMap.empty in
-  let add_id_hpred id hpred =
-    try
-      let hpred_set = IdMap.find id !id_hpred_map in
-      id_hpred_map := IdMap.add id (HpredSet.add hpred hpred_set) !id_hpred_map
-    with
-    | Not_found -> id_hpred_map := IdMap.add id (HpredSet.singleton hpred) !id_hpred_map in
-  let add_hpred hpred =
-    let fav = Sil.fav_new () in
-    Sil.hpred_fav_add fav hpred;
-    IList.iter (fun id -> add_id_hpred id hpred) (Sil.fav_to_list fav) in
-  let id_in_several_hpreds id =
-    HpredSet.cardinal (IdMap.find id !id_hpred_map) > 1 in
-  IList.iter add_hpred sigma;
-  id_in_several_hpreds
-*)
diff --git a/infer/src/backend/abs.mli b/infer/src/backend/abs.mli
index f233a0008..ed2057864 100644
--- a/infer/src/backend/abs.mli
+++ b/infer/src/backend/abs.mli
@@ -10,26 +10,34 @@
 
 (** Implementation of Abstraction Functions *)
 
-(** Create abstraction rules from the definition of a type *)
-val create_absrules_from_tdecl : Sil.tenv -> Typename.t -> unit
-
-(** Check whether the prop contains junk.
-    If it does, and [Config.allowleak] is true, remove the junk, otherwise raise a Leak exception. *)
-val abstract_junk : ?original_prop:Prop.normal Prop.t -> Procname.t -> Sil.tenv -> Prop.normal Prop.t -> Prop.normal Prop.t
-
-(** Remove redundant elements in an array, and check for junk afterwards *)
-val remove_redundant_array_elements :
-  Procname.t -> Sil.tenv -> Prop.normal Prop.t -> Prop.normal Prop.t
+(** Abstraction rules discovered *)
+type rules
 
 (** Abstract a proposition. *)
 val abstract : Procname.t -> Sil.tenv -> 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. *)
+val abstract_junk :
+  ?original_prop:Prop.normal Prop.t ->
+  Procname.t -> Sil.tenv -> Prop.normal Prop.t -> Prop.normal Prop.t
+
 (** Abstract a proposition but don't pay a SymOp *)
 val abstract_no_symop : Procname.t -> Sil.tenv -> Prop.normal Prop.t -> Prop.normal Prop.t
 
+(** Get the current rules discoveres *)
+val get_current_rules : unit -> rules
+
 (** Abstract each proposition in [propset] *)
 val lifted_abstract : Procname.t -> Sil.tenv -> Propset.t -> Propset.t
 
-val abs_rules_reset : unit -> unit
+(** Remove redundant elements in an array, and check for junk afterwards *)
+val remove_redundant_array_elements :
+  Procname.t -> Sil.tenv -> Prop.normal Prop.t -> Prop.normal Prop.t
+
+(** Reset the abstraction rules discovered *)
+val reset_current_rules : unit -> unit
 
-val get_cycle : Sil.hpred -> Prop.normal Prop.t -> ((Sil.strexp * Sil.typ) * Ident.fieldname * Sil.strexp) list
+(** Set the current rules discovered *)
+val set_current_rules : rules -> unit
diff --git a/infer/src/backend/config.ml b/infer/src/backend/config.ml
index 987389734..db61cee9d 100644
--- a/infer/src/backend/config.ml
+++ b/infer/src/backend/config.ml
@@ -134,7 +134,12 @@ let abs_struct = ref 1
     1 = evaluate all expressions abstractly.
     2 = 1 + abstract constant integer values during join.
 *)
-let abs_val = ref 2
+let abs_val_default = 2
+let abs_val =
+  ref abs_val_default
+
+let reset_abs_val () =
+  abs_val := abs_val_default
 
 (** if true, completely ignore the possibility that errors can be caused by unknown procedures
  * during the symbolic execution phase *)
@@ -244,18 +249,9 @@ let nelseg = ref false
 (** Flag to activate nonstop mode: the analysis continues after in encounters errors *)
 let nonstop = ref false
 
-(** Flag for the on-the-fly predicate discovery *)
-let on_the_fly = ref true
-
 (** if true, skip the re-execution phase *)
 let only_footprint = ref false
 
-(** flag: only analyze procedures which were analyzed before but have no specs *)
-let only_nospecs = ref false
-
-(** flag: only analyze procedures dependent on previous skips which now have a .specs file *)
-let only_skips = ref false
-
 (** if true, user simple pretty printing *)
 let pp_simple = ref true
 
@@ -268,9 +264,6 @@ let print_using_diff = ref true
 (** path of the project results directory *)
 let results_dir = ref default_results_dir
 
-(** If not "", only consider functions recursively called by function [!slice_fun] *)
-let slice_fun = ref ""
-
 (** Flag to tune the level of abstracting the postconditions of specs discovered
     by the footprint analysis.
     0 = nothing special.
diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml
index 88909decf..f9df2a00d 100644
--- a/infer/src/backend/dom.ml
+++ b/infer/src/backend/dom.ml
@@ -2023,32 +2023,3 @@ let propset_meet_generate_pre pset =
     let plist_old = Propset.to_proplist pset in
     let plist_new = Propset.to_proplist pset_new in
     plist_new @ plist_old
-
-(*
-let epset_add e e' set =
-  match (Sil.exp_compare e e') with
-  | i when i <= 0 -> EPset.add (e, e') set
-  | _ -> EPset.add (e', e) set
-
-let run_without_absval f e1 e2 =
-  let old_abs_val = !Config.abs_val in
-  let new_abs_val = if old_abs_val = 0 then 0 else 1 in
-  try
-    begin
-      Config.abs_val := new_abs_val;
-      let e = f e1 e2 in
-      Config.abs_val := old_abs_val;
-      e
-    end
-  with exn ->
-    begin
-      Config.abs_val := old_abs_val;
-      raise exn
-    end
-
-let exp_partial_join_without_absval e1 e2 =
-  run_without_absval exp_partial_join e1 e2
-
-let exp_partial_meet_without_absval e1 e2 =
-  run_without_absval exp_partial_meet e1 e2
-*)
diff --git a/infer/src/backend/fork.ml b/infer/src/backend/fork.ml
index 0aa556759..45237f1ca 100644
--- a/infer/src/backend/fork.ml
+++ b/infer/src/backend/fork.ml
@@ -348,25 +348,6 @@ let main_algorithm exe_env analyze_proc filter_out process_result : unit =
       (proc_is_done call_graph) (Cg.get_nonrecursive_dependents call_graph pname) &&
     (Specs.get_timestamp (Specs.get_summary_unsafe "main_algorithm" pname) = 0
      || not (proc_is_up_to_date call_graph pname)) in
-  let filter_out_ondemand pname =
-    let to_analyze =
-      if !Config.ondemand_enabled then
-        try
-          let cfg = Exe_env.get_cfg exe_env pname in
-          match Cfg.Procdesc.find_from_name cfg pname with
-          | Some pdesc ->
-              let reactive_changed =
-                if !Config.reactive_mode
-                then (Cfg.Procdesc.get_attributes pdesc).ProcAttributes.changed
-                else true in
-              reactive_changed && (* in reactive mode, only analyze changed procedures *)
-              Ondemand.procedure_should_be_analyzed pdesc pname
-          | None ->
-              true
-        with Not_found -> true
-      else
-        true in
-    not to_analyze in
   let process_one_proc ((pname, _) as elem) =
     DB.current_source :=
       (Specs.get_summary_unsafe "main_algorithm" pname)
@@ -379,15 +360,14 @@ let main_algorithm exe_env analyze_proc filter_out process_result : unit =
           (Specs.pp_summary pe_text whole_seconds)
           (Specs.get_summary_unsafe "main_algorithm" pname)
       end;
-    if filter_out call_graph pname ||
-       filter_out_ondemand pname
+    if filter_out exe_env pname
     then
       post_process_procs exe_env [pname]
     else
       begin
         max_timeout := max (Specs.get_iterations pname) !max_timeout;
         Specs.update_dependency_map pname;
-        process_result exe_env elem (analyze_proc exe_env elem);
+        process_result exe_env elem (analyze_proc exe_env pname);
       end in
   while not (WeightedPnameSet.is_empty !G.wpnames_todo) do
     begin
@@ -413,7 +393,7 @@ type analyze_proc = Exe_env.t -> Procname.t -> Specs.summary
 
 type process_result = Exe_env.t -> WeightedPname.t -> Specs.summary -> unit
 
-type filter_out = Cg.t -> Procname.t -> bool
+type filter_out = Exe_env.t -> Procname.t -> bool
 
 (** Execute [analyze_proc] respecting dependencies between procedures,
     and apply [process_result] to the result of the analysis.
@@ -452,5 +432,4 @@ let interprocedural_algorithm
         let exn' = Exceptions.Internal_error (Localise.verbatim_desc err_str) in
         Reporting.log_error pname exn';
         post_process_procs exe_env [pname] in
-  main_algorithm
-    exe_env (fun exe_env (n, _) -> analyze_proc exe_env n) filter_out process_result
+  main_algorithm exe_env analyze_proc filter_out process_result
diff --git a/infer/src/backend/fork.mli b/infer/src/backend/fork.mli
index 68eb99187..8890a6af5 100644
--- a/infer/src/backend/fork.mli
+++ b/infer/src/backend/fork.mli
@@ -38,7 +38,7 @@ type analyze_proc = Exe_env.t -> Procname.t -> Specs.summary
 
 type process_result = Exe_env.t -> (Procname.t * Cg.in_out_calls) -> Specs.summary -> unit
 
-type filter_out = Cg.t -> Procname.t -> bool
+type filter_out = Exe_env.t -> Procname.t -> bool
 
 (** Execute [analyze_proc] respecting dependencies between procedures,
     and apply [process_result] to the result of the analysis.
diff --git a/infer/src/backend/inferanalyze.ml b/infer/src/backend/inferanalyze.ml
index 0f68c3342..018f90909 100644
--- a/infer/src/backend/inferanalyze.ml
+++ b/infer/src/backend/inferanalyze.ml
@@ -159,13 +159,13 @@ let arg_desc =
         Arg.Set_int iterations_cmdline,
         Some "n",
         "set the max number of operations for each function, \
-        expressed as a multiple of symbolic operations (default n=1)"
+         expressed as a multiple of symbolic operations (default n=1)"
         ;
         "-nonstop",
         Arg.Set Config.nonstop,
         None,
         "activate the nonstop mode: the analysis continues after finding errors. \
-        With this option the analysis can become less precise."
+         With this option the analysis can become less precise."
         ;
         "-out_file",
         Arg.Set_string out_file_cmdline,
@@ -186,7 +186,7 @@ let arg_desc =
         Arg.String source_path,
         Some "path",
         "specify the absolute path to the root of the source files. \
-        Used to interpret relative paths when using option -exclude."
+         Used to interpret relative paths when using option -exclude."
         ;
         (* TODO: merge with the -project_root option *)
         "-java",
@@ -218,7 +218,7 @@ let arg_desc =
         Arg.Set_string ml_buckets_arg,
         Some "ml_buckets",
         "memory leak buckets to be checked, separated by commas. \
-        The possible buckets are cf (Core Foundation), arc, narc (No arc), cpp, unknown_origin"
+         The possible buckets are cf (Core Foundation), arc, narc (No arc), cpp, unknown_origin"
         ;
       ] in
     Arg.create_options_desc false "Analysis Options" desc in
@@ -235,7 +235,7 @@ let arg_desc =
         Arg.Set Config.angelic_execution,
         None,
         "activate angelic execution: \
-        The analysis ignores errors caused by unknown procedure calls."
+         The analysis ignores errors caused by unknown procedure calls."
         ;
         "-checkers",
         Arg.Unit (fun () -> checkers := true; Config.intraprocedural := true),
@@ -280,16 +280,6 @@ let arg_desc =
         Some "n",
         "set the max number of procedures in each cluster (default n=2000)"
         ;
-        "-only_nospecs",
-        Arg.Set Config.only_nospecs,
-        None,
-        " only analyze procedures which were analyzed before but have no specs"
-        ;
-        "-only_skips",
-        Arg.Set Config.only_skips,
-        None,
-        " only analyze procedures dependent on previous skips which now have a .specs file"
-        ;
         "-seconds_per_iteration",
         Arg.Set_int seconds_per_iteration,
         Some "n",
diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml
index ab09c2d77..bef19bd69 100644
--- a/infer/src/backend/interproc.ml
+++ b/infer/src/backend/interproc.ml
@@ -158,25 +158,25 @@ let path_set_checkout_todo (wl : Worklist.t) (node: Cfg.node) : Paths.PathSet.t
 (* =============== END of the edge_set object =============== *)
 
 let collect_do_abstract_pre pname tenv (pset : Propset.t) : Propset.t =
-  if !Config.footprint then begin
-    Config.footprint := false;
-    let pset' = Abs.lifted_abstract pname tenv pset in
-    Config.footprint := true;
-    pset'
-  end
-  else Abs.lifted_abstract pname tenv pset
+  if !Config.footprint
+  then
+    run_with_footprint_false
+      (Abs.lifted_abstract pname tenv)
+      pset
+  else
+    Abs.lifted_abstract pname tenv pset
 
 let collect_do_abstract_post pname tenv (pathset : Paths.PathSet.t) : Paths.PathSet.t =
   let abs_option p =
     if Prover.check_inconsistency p then None
     else Some (Abs.abstract pname tenv p) in
-  if !Config.footprint then begin
-    Config.footprint := false;
-    let pathset' = Paths.PathSet.map_option abs_option pathset in
-    Config.footprint := true;
-    pathset'
-  end
-  else Paths.PathSet.map_option abs_option pathset
+  if !Config.footprint
+  then
+    run_with_footprint_false
+      (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
@@ -196,12 +196,13 @@ let do_meet_pre pset =
 (** Find the preconditions in the current spec table, apply meet then join, and return the joined preconditions *)
 let collect_preconditions pname tenv proc_name : Prop.normal Specs.Jprop.t list =
   let collect_do_abstract_one tenv prop =
-    if !Config.footprint then begin
-      Config.footprint := false;
-      let prop' = Abs.abstract_no_symop tenv prop in
-      Config.footprint := true;
-      prop' end
-    else Abs.abstract_no_symop tenv prop in
+    if !Config.footprint
+    then
+      run_with_footprint_false
+        (Abs.abstract_no_symop tenv)
+        prop
+    else
+      Abs.abstract_no_symop tenv prop in
   let pres = IList.map (fun spec -> Specs.Jprop.to_prop spec.Specs.pre) (Specs.get_specs proc_name) in
   let pset = Propset.from_proplist pres in
   let pset' =
@@ -969,12 +970,13 @@ let set_current_language proc_desc =
   let language = (Cfg.Procdesc.get_attributes proc_desc).ProcAttributes.language in
   Config.curr_language := language
 
-(** reset counters before analysing a procedure *)
-let reset_global_counters proc_desc =
+(** reset global values before analysing a procedure *)
+let reset_global_values proc_desc =
+  Config.reset_abs_val ();
   Ident.NameGenerator.reset ();
   SymOp.reset_total ();
   reset_prop_metrics ();
-  Abs.abs_rules_reset ();
+  Abs.reset_current_rules ();
   set_current_language proc_desc
 
 (* Collect all pairs of the kind (precondition, runtime exception) from a summary *)
@@ -1112,7 +1114,7 @@ let analyze_proc exe_env (proc_name: Procname.t) : Specs.summary =
   let proc_desc = match Cfg.Procdesc.find_from_name cfg proc_name with
     | Some proc_desc -> proc_desc
     | None -> assert false in
-  reset_global_counters proc_desc;
+  reset_global_values proc_desc;
   let go, get_results = perform_analysis_phase cfg tenv proc_name proc_desc in
   let res = Fork.Timeout.exe_timeout (Specs.get_iterations proc_name) go () in
   let specs, phase = get_results () in
@@ -1179,52 +1181,25 @@ let process_result (exe_env: Exe_env.t) (proc_name, calls) (_summ: Specs.summary
   let procs_done = Fork.procs_become_done call_graph proc_name in
   Fork.post_process_procs exe_env procs_done
 
-(** Return true if the analysis of [proc_name] should be
-    skipped. Called by the parent process before attempting to analyze a
-    proc. *)
-let filter_out (call_graph: Cg.t) (proc_name: Procname.t) : bool =
-  if !Config.trace_anal then L.err "===filter_out@.";
-  let slice_out = (* filter out if slicing is active and [proc_name] not in slice *)
-    (!Config.slice_fun <> "") &&
-    (Procname.compare (Procname.from_string_c_fun !Config.slice_fun) proc_name != 0) &&
-    (Cg.node_defined call_graph proc_name) &&
-    not (Cg.calls_recursively call_graph (Procname.from_string_c_fun !Config.slice_fun) proc_name) in
-  slice_out
-
-let check_skipped_procs procs_and_defined_children =
-  let skipped_procs = ref Procname.Set.empty in
-  let proc_check_skips (pname, _) =
-    let process_skip () =
-      let call_stats =
-        (Specs.get_summary_unsafe "check_skipped_procs" pname).Specs.stats.Specs.call_stats in
-      let do_tr_elem pn = function
-        | Specs.CallStats.CR_skip, _ ->
-            skipped_procs := Procname.Set.add pn !skipped_procs
-        | _ -> () in
-      let do_call (pn, _) (tr: Specs.CallStats.trace) = IList.iter (do_tr_elem pn) tr in
-      Specs.CallStats.iter do_call call_stats in
-    if Specs.summary_exists pname then process_skip () in
-  IList.iter proc_check_skips procs_and_defined_children;
-  let skipped_procs_with_summary =
-    Procname.Set.filter Specs.summary_exists !skipped_procs in
-  skipped_procs_with_summary
-
-(** create a function to filter procedures which were skips but now have a .specs file *)
-let filter_skipped_procs cg procs_and_defined_children =
-  let skipped_procs_with_summary = check_skipped_procs procs_and_defined_children in
-  let filter (pname, _) =
-    let calls_recurs pn =
-      let r = try Cg.calls_recursively cg pname pn with Not_found -> false in
-      L.err "calls recursively %a %a: %b@." Procname.pp pname Procname.pp pn r;
-      r in
-    Procname.Set.exists calls_recurs skipped_procs_with_summary in
-  filter
-
-(** create a function to filter procedures which were analyzed before but had no specs *)
-let filter_nospecs (pname, _) =
-  if Specs.summary_exists pname
-  then Specs.get_specs pname = []
-  else false
+let filter_out_ondemand exe_env proc_name =
+  let to_analyze =
+    if !Config.ondemand_enabled then
+      try
+        let cfg = Exe_env.get_cfg exe_env proc_name in
+        match Cfg.Procdesc.find_from_name cfg proc_name with
+        | Some pdesc ->
+            let reactive_changed =
+              if !Config.reactive_mode
+              then (Cfg.Procdesc.get_attributes pdesc).ProcAttributes.changed
+              else true in
+            reactive_changed && (* in reactive mode, only analyze changed procedures *)
+            Ondemand.procedure_should_be_analyzed pdesc proc_name
+        | None ->
+            true
+      with Not_found -> true
+    else
+      true in
+  not to_analyze
 
 (** Perform the analysis of an exe_env *)
 let do_analysis exe_env =
@@ -1248,22 +1223,15 @@ let do_analysis exe_env =
     let attributes =
       { (Cfg.Procdesc.get_attributes pdesc) with
         ProcAttributes.err_log = static_err_log; } in
+    Specs.init_summary (dep, nodes, proc_flags, calls, None, attributes) in
 
-    Specs.init_summary
-      (dep, nodes, proc_flags,
-       calls, None, attributes) in
-  let filter =
-    if !Config.only_skips then (filter_skipped_procs cg procs_and_defined_children)
-    else if !Config.only_nospecs then filter_nospecs
-    else (fun _ -> true) in
   IList.iter
     (fun ((pn, _) as x) ->
        let should_init () =
          Config.analyze_models ||
          not !Config.ondemand_enabled ||
          Specs.get_summary pn = None in
-       if filter x &&
-          should_init ()
+       if should_init ()
        then init_proc x)
     procs_and_defined_children;
 
@@ -1287,7 +1255,7 @@ let do_analysis exe_env =
     { Ondemand.analyze_ondemand; get_proc_desc; } in
 
   Ondemand.set_callbacks callbacks;
-  Fork.interprocedural_algorithm exe_env analyze_proc process_result filter_out;
+  Fork.interprocedural_algorithm exe_env analyze_proc process_result filter_out_ondemand;
   Ondemand.unset_callbacks ()
 
 
diff --git a/infer/src/backend/interproc.mli b/infer/src/backend/interproc.mli
index 0c8316107..d060ed6af 100644
--- a/infer/src/backend/interproc.mli
+++ b/infer/src/backend/interproc.mli
@@ -10,21 +10,6 @@
 
 (** Interprocedural Analysis *)
 
-(** Analyze [proc_name] and return the updated summary. Use module
-    {!Timeout } to call {!perform_analysis_phase } with a time limit, and
-    then return the updated summary. Executed as a child process. *)
-val analyze_proc : Exe_env.t -> Procname.t -> Specs.summary
-
-(** Process the result of the analysis of [proc_name]: update the
-    returned summary and add it to the spec table. Executed in the
-    parent process as soon as a child process returns a result. *)
-val process_result : Exe_env.t -> (Procname.t * Cg.in_out_calls) -> Specs.summary -> unit
-
-(** Return true if the analysis of [proc_name] should be
-    skipped. Called by the parent process before attempting to analyze a
-    proc. *)
-val filter_out : Cg.t -> Procname.t -> bool
-
 (** Perform the analysis of an exe_env *)
 val do_analysis : Exe_env.t -> unit
 
diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml
index f6796c1a2..e4fb58831 100644
--- a/infer/src/backend/ondemand.ml
+++ b/infer/src/backend/ondemand.ml
@@ -87,6 +87,8 @@ let procedure_should_be_analyzed curr_pdesc proc_name =
 
 type global_state =
   {
+    abs_val : int;
+    abstraction_rules : Abs.rules;
     current_source : DB.source_file;
     delayed_prints : L.print_action list;
     footprint_mode : bool;
@@ -97,6 +99,8 @@ type global_state =
 
 let save_global_state () =
   {
+    abs_val = !Config.abs_val;
+    abstraction_rules = Abs.get_current_rules ();
     current_source = !DB.current_source;
     delayed_prints = L.get_delayed_prints ();
     footprint_mode = !Config.footprint;
@@ -106,6 +110,8 @@ let save_global_state () =
   }
 
 let restore_global_state st =
+  Config.abs_val := st.abs_val;
+  Abs.set_current_rules st.abstraction_rules;
   DB.current_source := st.current_source;
   L.set_delayed_prints st.delayed_prints;
   Config.footprint := st.footprint_mode;
diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml
index 888cd6349..c0f8afa20 100644
--- a/infer/src/backend/symExec.ml
+++ b/infer/src/backend/symExec.ml
@@ -501,16 +501,6 @@ let check_already_dereferenced pname cond prop =
       Reporting.log_warning pname ~pre: pre_opt exn
   | None -> ()
 
-let run_with_abs_val_eq_zero f =
-  let abs_val_old = !Config.abs_val in
-  Config.abs_val := 0;
-  let res = try f () with
-    | exn ->
-        Config.abs_val := abs_val_old;
-        raise exn in
-  Config.abs_val := abs_val_old;
-  res
-
 (** Check whether symbolic execution de-allocated a stack variable or a constant string, raising an exception in that case *)
 let check_deallocate_static_memory prop_after =
   let check_deallocated_attribute = function
@@ -1204,14 +1194,12 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
   | Sil.Declare_locals (ptl, _) ->
       let sigma_locals =
         let add_None (x, y) = (x, Sil.Sizeof (y, Sil.Subtype.exact), None) in
-        let fp_mode = !Config.footprint in
-        Config.footprint := false; (* no footprint vars for locals *)
-        let sigma_locals =
+        let sigma_locals () =
           IList.map
             (Prop.mk_ptsto_lvar (Some tenv) Prop.Fld_init Sil.inst_initial)
             (IList.map add_None ptl) in
-        Config.footprint := fp_mode;
-        sigma_locals in
+        run_with_footprint_false (* no footprint vars for locals *)
+          sigma_locals () in
       let sigma' = Prop.get_sigma _prop @ sigma_locals in
       let prop' = Prop.normalize (Prop.replace_sigma sigma' _prop) in
       ret_old_path [prop']
@@ -1598,17 +1586,25 @@ and sym_exec_wrapper handle_exn cfg tenv pdesc instr ((prop: Prop.normal Prop.t)
       let curr_node = State.get_node () in
       match Cfg.Node.get_kind curr_node with
       | Cfg.Node.Prune_node _ when not (node_has_abstraction curr_node) ->
-          (* don't check for leaks in prune nodes, unless there is abstraction anyway, but force them into either branch *)
+          (* don't check for leaks in prune nodes, unless there is abstraction anyway,*)
+          (* but force them into either branch *)
           p'
       | _ ->
           check_deallocate_static_memory (Abs.abstract_junk ~original_prop: p pname tenv p') in
     L.d_str "Instruction "; Sil.d_instr instr; L.d_ln ();
     let prop', fav_normal = pre_process_prop prop in
-    let res_list = run_with_abs_val_eq_zero (* no exp abstraction during sym exe *)
-        (fun () ->
-           sym_exec cfg tenv pdesc instr prop' path) in
-    let res_list_nojunk = IList.map (fun (p, path) -> (post_process_result fav_normal p path, path)) res_list in
-    let results = IList.map (fun (p, path) -> (Prop.prop_rename_primed_footprint_vars p, path)) res_list_nojunk in
+    let res_list =
+      run_with_abs_val_equal_zero (* no exp abstraction during sym exe *)
+        (fun () -> sym_exec cfg tenv pdesc instr prop' path)
+        () in
+    let res_list_nojunk =
+      IList.map
+        (fun (p, path) -> (post_process_result fav_normal p path, path))
+        res_list in
+    let results =
+      IList.map
+        (fun (p, path) -> (Prop.prop_rename_primed_footprint_vars p, path))
+        res_list_nojunk in
     L.d_strln "Instruction Returns";
     Propgraph.d_proplist prop (IList.map fst results); L.d_ln ();
     State.mark_instr_ok ();
@@ -1616,8 +1612,11 @@ and sym_exec_wrapper handle_exn cfg tenv pdesc instr ((prop: Prop.normal Prop.t)
   with exn when Exceptions.handle_exception exn && !Config.footprint ->
     handle_exn exn; (* calls State.mark_instr_fail *)
     if !Config.nonstop
-    then (Paths.PathSet.from_renamed_list [(prop, path)]) (* in nonstop mode treat the instruction as skip *)
-    else Paths.PathSet.empty
+    then
+      (* in nonstop mode treat the instruction as skip *)
+      (Paths.PathSet.from_renamed_list [(prop, path)])
+    else
+      Paths.PathSet.empty
 
 (** {2 Lifted Abstract Transfer Functions} *)
 
diff --git a/infer/src/backend/utils.ml b/infer/src/backend/utils.ml
index d8aa1e6e3..08bd0b347 100644
--- a/infer/src/backend/utils.ml
+++ b/infer/src/backend/utils.ml
@@ -757,11 +757,6 @@ let reserved_arg_desc =
     Some "n",
     "set right margin for the pretty printing functions"
     ;
-    "-slice_fun",
-    Arg.Set_string Config.slice_fun,
-    None,
-    "analyze only functions recursively called by function given as argument"
-    ;
     "-spec_abs_level",
     Arg.Set_int Config.spec_abs_level,
     Some "n",
@@ -981,3 +976,23 @@ let string_append_crc_cutoff ?(cutoff=100) ?(key="") name =
     let name_for_crc = name ^ key in
     string_crc_hex32 name_for_crc in
   name_up_to_cutoff ^ "." ^ crc_str
+
+let run_with_val reference value f x =
+  let saved = !reference in
+  let restore () =
+    reference := saved in
+  try
+    reference := value;
+    let res = f x in
+    restore ();
+    res
+  with
+  | exn ->
+      restore ();
+      raise exn
+
+let run_with_footprint_false f x =
+  run_with_val Config.footprint false f x
+
+let run_with_abs_val_equal_zero f x =
+  run_with_val Config.abs_val 0 f x
diff --git a/infer/src/backend/utils.mli b/infer/src/backend/utils.mli
index 92a1fa8fc..3db9cb5bb 100644
--- a/infer/src/backend/utils.mli
+++ b/infer/src/backend/utils.mli
@@ -367,3 +367,11 @@ val analyzers: analyzer list
 val string_of_analyzer: analyzer -> string
 
 val analyzer_of_string: string -> analyzer
+
+(** Call f x with Config.footprint set to false.
+    Restore the initial value of footprint also in case of exception. *)
+val run_with_footprint_false : ('a -> 'b) -> 'a -> 'b
+
+(** Call f x with Config.abs_val set to zero.
+    Restore the initial value also in case of exception. *)
+val run_with_abs_val_equal_zero : ('a -> 'b) -> 'a -> 'b