(*
 * Copyright (c) 2009-2013, Monoidics ltd.
 * Copyright (c) Facebook, Inc. and its affiliates.
 *
 * This source code is licensed under the MIT license found in the
 * LICENSE file in the root directory of this source tree.
 *)

open! IStd

(** Implementation of Abstraction Functions *)

module L = Logging

(** {2 Abstraction} *)

type rule =
  { r_vars: Ident.t list
  ; r_root: Match.hpred_pat
  ; r_sigma: Match.hpred_pat list
  ; (* sigma should be in a specific order *)
    r_new_sigma: Predicates.hpred list
  ; r_new_pi: Prop.normal Prop.t -> Prop.normal Prop.t -> Predicates.subst -> Predicates.atom list
  ; r_condition: Prop.normal Prop.t -> Predicates.subst -> bool }

let sigma_rewrite tenv p r : Prop.normal Prop.t option =
  match Match.prop_match_with_impl tenv p r.r_condition r.r_vars r.r_root r.r_sigma with
  | None ->
      None
  | Some (sub, p_leftover) ->
      if not (r.r_condition p_leftover sub) then None
      else
        let res_pi = r.r_new_pi p p_leftover sub in
        let res_sigma = Prop.sigma_sub sub r.r_new_sigma in
        let p_with_res_pi = List.fold ~f:(Prop.prop_atom_and tenv) ~init:p_leftover res_pi in
        let p_new = Prop.prop_sigma_star p_with_res_pi res_sigma in
        Some (Prop.normalize tenv p_new)


(******************** Start of SLL abstraction rules  *****************)
let create_fresh_primeds_ls para =
  let id_base = Ident.create_fresh Ident.kprimed in
  let id_next = Ident.create_fresh Ident.kprimed in
  let id_end = Ident.create_fresh Ident.kprimed in
  let ids_shared =
    let svars = para.Predicates.svars in
    let f _ = Ident.create_fresh Ident.kprimed in
    List.map ~f svars
  in
  let ids_tuple = (id_base, id_next, id_end, ids_shared) in
  let exp_base = Exp.Var id_base in
  let exp_next = Exp.Var id_next in
  let exp_end = Exp.Var id_end in
  let exps_shared = List.map ~f:(fun id -> Exp.Var id) ids_shared in
  let exps_tuple = (exp_base, exp_next, exp_end, exps_shared) in
  (ids_tuple, exps_tuple)


let create_condition_ls ids_private id_base p_leftover (inst : Predicates.subst) =
  let insts_of_private_ids, insts_of_public_ids, inst_of_base =
    let f id' = List.exists ~f:(fun id'' -> Ident.equal id' id'') ids_private in
    let inst_private, inst_public = Predicates.sub_domain_partition f inst in
    let insts_of_public_ids = Predicates.sub_range inst_public in
    let inst_of_base =
      try Predicates.sub_find (Ident.equal id_base) inst_public
      with Not_found_s _ | Caml.Not_found -> assert false
    in
    let insts_of_private_ids = Predicates.sub_range inst_private in
    (insts_of_private_ids, insts_of_public_ids, inst_of_base)
  in
  (*
  let fav_inst_of_base = Sil.exp_fav_list inst_of_base in
  L.out "@[.... application of condition ....@\n@.";
  L.out "@[<4>  private ids : %a@\n@." pp_exp_list insts_of_private_ids;
  L.out "@[<4>  public ids : %a@\n@." pp_exp_list insts_of_public_ids;
  *)
  Exp.program_vars inst_of_base |> Sequence.is_empty
  && List.for_all ~f:(fun e -> Exp.program_vars e |> Sequence.is_empty) insts_of_private_ids
  &&
  let fav_insts_of_private_ids =
    Sequence.of_list insts_of_private_ids
    |> Sequence.concat_map ~f:Exp.free_vars
    |> Sequence.memoize
  in
  (not (Sequence.exists fav_insts_of_private_ids ~f:Ident.is_normal))
  &&
  let fav_insts_of_private_ids = Ident.set_of_sequence fav_insts_of_private_ids in
  let intersects_fav_insts_of_private_ids s =
    Sequence.exists s ~f:(fun id -> Ident.Set.mem id fav_insts_of_private_ids)
  in
  (* [fav_insts_of_private_ids] does not intersect the free vars in [p_leftover.sigma] *)
  Prop.sigma_free_vars p_leftover.Prop.sigma |> Fn.non intersects_fav_insts_of_private_ids
  && (* [fav_insts_of_private_ids] does not intersect the free vars in [insts_of_public_ids] *)
  List.for_all insts_of_public_ids ~f:(fun e ->
      Exp.free_vars e |> Fn.non intersects_fav_insts_of_private_ids )


let mk_rule_ptspts_ls tenv impl_ok1 impl_ok2 (para : Predicates.hpara) =
  let ids_tuple, exps_tuple = create_fresh_primeds_ls para in
  let id_base, id_next, id_end, ids_shared = ids_tuple in
  let exp_base, exp_next, exp_end, exps_shared = exps_tuple in
  let ids_exist_fst, para_fst = Predicates.hpara_instantiate para exp_base exp_next exps_shared in
  let para_fst_start, para_fst_rest =
    let mark_impl_flag hpred = {Match.hpred; Match.flag= impl_ok1} in
    match para_fst with
    | [] ->
        L.internal_error "@\n@\nERROR (Empty Para): %a@\n@." (Predicates.pp_hpara Pp.text) para ;
        assert false
    | hpred :: hpreds ->
        let hpat = mark_impl_flag hpred in
        let hpats = List.map ~f:mark_impl_flag hpreds in
        (hpat, hpats)
  in
  let ids_exist_snd, para_snd =
    let mark_impl_flag hpred = {Match.hpred; Match.flag= impl_ok2} in
    let ids, para_body = Predicates.hpara_instantiate para exp_next exp_end exps_shared in
    let para_body_hpats = List.map ~f:mark_impl_flag para_body in
    (ids, para_body_hpats)
  in
  let lseg_res = Prop.mk_lseg tenv Lseg_NE para exp_base exp_end exps_shared in
  let gen_pi_res _ _ (_ : Predicates.subst) = [] in
  let condition =
    let ids_private = id_next :: (ids_exist_fst @ ids_exist_snd) in
    create_condition_ls ids_private id_base
  in
  { r_vars= (id_base :: id_next :: id_end :: ids_shared) @ ids_exist_fst @ ids_exist_snd
  ; r_root= para_fst_start
  ; r_sigma= para_fst_rest @ para_snd
  ; r_new_sigma= [lseg_res]
  ; r_new_pi= gen_pi_res
  ; r_condition= condition }


let mk_rule_ptsls_ls tenv k2 impl_ok1 impl_ok2 para =
  let ids_tuple, exps_tuple = create_fresh_primeds_ls para in
  let id_base, id_next, id_end, ids_shared = ids_tuple in
  let exp_base, exp_next, exp_end, exps_shared = exps_tuple in
  let ids_exist, para_inst = Predicates.hpara_instantiate para exp_base exp_next exps_shared in
  let para_inst_start, para_inst_rest =
    match para_inst with
    | [] ->
        L.internal_error "@\n@\nERROR (Empty Para): %a@\n@." (Predicates.pp_hpara Pp.text) para ;
        assert false
    | hpred :: hpreds ->
        let allow_impl hpred = {Match.hpred; Match.flag= impl_ok1} in
        (allow_impl hpred, List.map ~f:allow_impl hpreds)
  in
  let lseg_pat =
    {Match.hpred= Prop.mk_lseg tenv k2 para exp_next exp_end exps_shared; Match.flag= impl_ok2}
  in
  let lseg_res = Prop.mk_lseg tenv Lseg_NE para exp_base exp_end exps_shared in
  let gen_pi_res _ _ (_ : Predicates.subst) = [] in
  let condition =
    let ids_private = id_next :: ids_exist in
    create_condition_ls ids_private id_base
  in
  { r_vars= (id_base :: id_next :: id_end :: ids_shared) @ ids_exist
  ; r_root= para_inst_start
  ; r_sigma= para_inst_rest @ [lseg_pat]
  ; r_new_pi= gen_pi_res
  ; r_new_sigma= [lseg_res]
  ; r_condition= condition }


let mk_rule_lspts_ls tenv k1 impl_ok1 impl_ok2 para =
  let ids_tuple, exps_tuple = create_fresh_primeds_ls para in
  let id_base, id_next, id_end, ids_shared = ids_tuple in
  let exp_base, exp_next, exp_end, exps_shared = exps_tuple in
  let lseg_pat =
    {Match.hpred= Prop.mk_lseg tenv k1 para exp_base exp_next exps_shared; Match.flag= impl_ok1}
  in
  let ids_exist, para_inst_pat =
    let ids, para_body = Predicates.hpara_instantiate para exp_next exp_end exps_shared in
    let allow_impl hpred = {Match.hpred; Match.flag= impl_ok2} in
    let para_body_pat = List.map ~f:allow_impl para_body in
    (ids, para_body_pat)
  in
  let lseg_res = Prop.mk_lseg tenv Lseg_NE para exp_base exp_end exps_shared in
  let gen_pi_res _ _ (_ : Predicates.subst) = [] in
  let condition =
    let ids_private = id_next :: ids_exist in
    create_condition_ls ids_private id_base
  in
  { r_vars= (id_base :: id_next :: id_end :: ids_shared) @ ids_exist
  ; r_root= lseg_pat
  ; r_sigma= para_inst_pat
  ; r_new_sigma= [lseg_res]
  ; r_new_pi= gen_pi_res
  ; r_condition= condition }


let lseg_kind_add (k1 : Predicates.lseg_kind) (k2 : Predicates.lseg_kind) : Predicates.lseg_kind =
  match (k1, k2) with
  | Lseg_NE, Lseg_NE | Lseg_NE, Lseg_PE | Lseg_PE, Lseg_NE ->
      Lseg_NE
  | Lseg_PE, Lseg_PE ->
      Lseg_PE


let mk_rule_lsls_ls tenv k1 k2 impl_ok1 impl_ok2 para =
  let ids_tuple, exps_tuple = create_fresh_primeds_ls para in
  let id_base, id_next, id_end, ids_shared = ids_tuple in
  let exp_base, exp_next, exp_end, exps_shared = exps_tuple in
  let lseg_fst_pat =
    {Match.hpred= Prop.mk_lseg tenv k1 para exp_base exp_next exps_shared; Match.flag= impl_ok1}
  in
  let lseg_snd_pat =
    {Match.hpred= Prop.mk_lseg tenv k2 para exp_next exp_end exps_shared; Match.flag= impl_ok2}
  in
  let k_res = lseg_kind_add k1 k2 in
  let lseg_res = Prop.mk_lseg tenv k_res para exp_base exp_end exps_shared in
  let gen_pi_res _ _ (_ : Predicates.subst) =
    []
    (*
  let inst_base, inst_next, inst_end =
  let find x = sub_find (equal x) inst in
  try
  (find id_base, find id_next, find id_end)
  with Not_found_s _ | Caml.Not_found -> assert false in
  let spooky_case _ =
  (equal_lseg_kind Lseg_PE k_res)
  && (check_allocatedness p_leftover inst_end)
  && ((check_disequal p_start inst_base inst_next)
  || (check_disequal p_start inst_next inst_end)) in
  let obvious_case _ =
  check_disequal p_start inst_base inst_end &&
  not (check_disequal p_leftover inst_base inst_end) in
  if not (spooky_case () || obvious_case ()) then []
  else [Aneq(inst_base, inst_end)]
  *)
  in
  let condition =
    let ids_private = [id_next] in
    create_condition_ls ids_private id_base
  in
  { r_vars= id_base :: id_next :: id_end :: ids_shared
  ; r_root= lseg_fst_pat
  ; r_sigma= [lseg_snd_pat]
  ; r_new_sigma= [lseg_res]
  ; r_new_pi= gen_pi_res
  ; r_condition= condition }


let mk_rules_for_sll tenv (para : Predicates.hpara) : rule list =
  if not Config.nelseg then
    let pts_pts = mk_rule_ptspts_ls tenv true true para in
    let pts_pels = mk_rule_ptsls_ls tenv Lseg_PE true false para in
    let pels_pts = mk_rule_lspts_ls tenv Lseg_PE false true para in
    let pels_nels = mk_rule_lsls_ls tenv Lseg_PE Lseg_NE false false para in
    let nels_pels = mk_rule_lsls_ls tenv Lseg_NE Lseg_PE false false para in
    let pels_pels = mk_rule_lsls_ls tenv Lseg_PE Lseg_PE false false para in
    [pts_pts; pts_pels; pels_pts; pels_nels; nels_pels; pels_pels]
  else
    let pts_pts = mk_rule_ptspts_ls tenv true true para in
    let pts_nels = mk_rule_ptsls_ls tenv Lseg_NE true false para in
    let nels_pts = mk_rule_lspts_ls tenv Lseg_NE false true para in
    let nels_nels = mk_rule_lsls_ls tenv Lseg_NE Lseg_NE false false para in
    [pts_pts; pts_nels; nels_pts; nels_nels]


(******************  End of SLL abstraction rules ******************)
(******************  Start of DLL abstraction rules  ******************)
let create_condition_dll = create_condition_ls

let mk_rule_ptspts_dll tenv impl_ok1 impl_ok2 para =
  let id_iF = Ident.create_fresh Ident.kprimed 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 =
    let svars = para.Predicates.svars_dll in
    let f _ = Ident.create_fresh Ident.kprimed in
    List.map ~f svars
  in
  let exp_iF = Exp.Var id_iF in
  let exp_iF' = Exp.Var id_iF' in
  let exp_oB = Exp.Var id_oB in
  let exp_oF = Exp.Var id_oF in
  let exps_shared = List.map ~f:(fun id -> Exp.Var id) ids_shared in
  let ids_exist_fst, para_fst =
    Predicates.hpara_dll_instantiate para exp_iF exp_oB exp_iF' exps_shared
  in
  let para_fst_start, para_fst_rest =
    let mark_impl_flag hpred = {Match.hpred; Match.flag= impl_ok1} in
    match para_fst with
    | [] ->
        L.internal_error "@\n@\nERROR (Empty DLL Para): %a@\n@." (Predicates.pp_hpara_dll Pp.text)
          para ;
        assert false
    | hpred :: hpreds ->
        let hpat = mark_impl_flag hpred in
        let hpats = List.map ~f:mark_impl_flag hpreds in
        (hpat, hpats)
  in
  let ids_exist_snd, para_snd =
    let mark_impl_flag hpred = {Match.hpred; Match.flag= impl_ok2} in
    let ids, para_body = Predicates.hpara_dll_instantiate para exp_iF' exp_iF exp_oF exps_shared in
    let para_body_hpats = List.map ~f:mark_impl_flag para_body in
    (ids, para_body_hpats)
  in
  let dllseg_res = Prop.mk_dllseg tenv Lseg_NE para exp_iF exp_oB exp_oF exp_iF' exps_shared in
  let gen_pi_res _ _ (_ : Predicates.subst) = [] in
  let condition =
    (* for the case of ptspts since iF'=iB therefore iF' cannot be private*)
    let ids_private = ids_exist_fst @ ids_exist_snd in
    create_condition_dll ids_private id_iF
  in
  (*
  L.out "r_root/para_fst_start=%a @.@." pp_hpat para_fst_start;
  L.out "para_fst_rest=%a @.@." pp_hpat_list para_fst_rest;
  L.out "para_snd=%a @.@." pp_hpat_list para_snd;
  L.out "dllseg_res=%a @.@." pp_hpred dllseg_res;
  *)
  { r_vars= (id_iF :: id_oB :: id_iF' :: id_oF :: ids_shared) @ ids_exist_fst @ ids_exist_snd
  ; r_root= para_fst_start
  ; r_sigma= para_fst_rest @ para_snd
  ; r_new_sigma= [dllseg_res]
  ; r_new_pi= gen_pi_res
  ; r_condition= condition }


let mk_rule_ptsdll_dll tenv k2 impl_ok1 impl_ok2 para =
  let id_iF = Ident.create_fresh Ident.kprimed 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 id_iB = Ident.create_fresh Ident.kprimed in
  let ids_shared =
    let svars = para.Predicates.svars_dll in
    let f _ = Ident.create_fresh Ident.kprimed in
    List.map ~f svars
  in
  let exp_iF = Exp.Var id_iF in
  let exp_iF' = Exp.Var id_iF' in
  let exp_oB = Exp.Var id_oB in
  let exp_oF = Exp.Var id_oF in
  let exp_iB = Exp.Var id_iB in
  let exps_shared = List.map ~f:(fun id -> Exp.Var id) ids_shared in
  let ids_exist, para_inst =
    Predicates.hpara_dll_instantiate para exp_iF exp_oB exp_iF' exps_shared
  in
  let para_inst_start, para_inst_rest =
    match para_inst with
    | [] ->
        assert false
    | hpred :: hpreds ->
        let allow_impl hpred = {Match.hpred; Match.flag= impl_ok1} in
        (allow_impl hpred, List.map ~f:allow_impl hpreds)
  in
  let dllseg_pat =
    { Match.hpred= Prop.mk_dllseg tenv k2 para exp_iF' exp_iF exp_oF exp_iB exps_shared
    ; Match.flag= impl_ok2 }
  in
  let dllseg_res = Prop.mk_dllseg tenv Lseg_NE para exp_iF exp_oB exp_oF exp_iB exps_shared in
  let gen_pi_res _ _ (_ : Predicates.subst) = [] in
  let condition =
    let ids_private = id_iF' :: ids_exist in
    create_condition_dll ids_private id_iF
  in
  { r_vars= (id_iF :: id_oB :: id_iF' :: id_oF :: id_iB :: ids_shared) @ ids_exist
  ; r_root= para_inst_start
  ; r_sigma= para_inst_rest @ [dllseg_pat]
  ; r_new_pi= gen_pi_res
  ; r_new_sigma= [dllseg_res]
  ; r_condition= condition }


let mk_rule_dllpts_dll tenv k1 impl_ok1 impl_ok2 para =
  let id_iF = Ident.create_fresh Ident.kprimed in
  let id_iF' = Ident.create_fresh Ident.kprimed in
  let id_oB = 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 =
    let svars = para.Predicates.svars_dll in
    let f _ = Ident.create_fresh Ident.kprimed in
    List.map ~f svars
  in
  let exp_iF = Exp.Var id_iF in
  let exp_iF' = Exp.Var id_iF' in
  let exp_oB = Exp.Var id_oB in
  let exp_oB' = Exp.Var id_oB' in
  let exp_oF = Exp.Var id_oF in
  let exps_shared = List.map ~f:(fun id -> Exp.Var id) ids_shared in
  let ids_exist, para_inst =
    Predicates.hpara_dll_instantiate para exp_iF' exp_oB' exp_oF exps_shared
  in
  let para_inst_pat =
    let allow_impl hpred = {Match.hpred; Match.flag= impl_ok2} in
    List.map ~f:allow_impl para_inst
  in
  let dllseg_pat =
    { Match.hpred= Prop.mk_dllseg tenv k1 para exp_iF exp_oB exp_iF' exp_oB' exps_shared
    ; Match.flag= impl_ok1 }
  in
  let dllseg_res = Prop.mk_dllseg tenv Lseg_NE para exp_iF exp_oB exp_oF exp_iF' exps_shared in
  let gen_pi_res _ _ (_ : Predicates.subst) = [] in
  let condition =
    let ids_private = id_oB' :: ids_exist in
    create_condition_dll ids_private id_iF
  in
  { r_vars= (id_iF :: id_oB :: id_iF' :: id_oB' :: id_oF :: ids_shared) @ ids_exist
  ; r_root= dllseg_pat
  ; r_sigma= para_inst_pat
  ; r_new_pi= gen_pi_res
  ; r_new_sigma= [dllseg_res]
  ; r_condition= condition }


let mk_rule_dlldll_dll tenv k1 k2 impl_ok1 impl_ok2 para =
  let id_iF = Ident.create_fresh Ident.kprimed in
  let id_iF' = Ident.create_fresh Ident.kprimed in
  let id_oB = 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 id_iB = Ident.create_fresh Ident.kprimed in
  let ids_shared =
    let svars = para.Predicates.svars_dll in
    let f _ = Ident.create_fresh Ident.kprimed in
    List.map ~f svars
  in
  let exp_iF = Exp.Var id_iF in
  let exp_iF' = Exp.Var id_iF' in
  let exp_oB = Exp.Var id_oB in
  let exp_oB' = Exp.Var id_oB' in
  let exp_oF = Exp.Var id_oF in
  let exp_iB = Exp.Var id_iB in
  let exps_shared = List.map ~f:(fun id -> Exp.Var id) ids_shared in
  let lseg_fst_pat =
    { Match.hpred= Prop.mk_dllseg tenv k1 para exp_iF exp_oB exp_iF' exp_oB' exps_shared
    ; Match.flag= impl_ok1 }
  in
  let lseg_snd_pat =
    { Match.hpred= Prop.mk_dllseg tenv k2 para exp_iF' exp_oB' exp_oF exp_iB exps_shared
    ; Match.flag= impl_ok2 }
  in
  let k_res = lseg_kind_add k1 k2 in
  let lseg_res = Prop.mk_dllseg tenv k_res para exp_iF exp_oB exp_oF exp_iB exps_shared in
  let gen_pi_res _ _ (_ : Predicates.subst) = [] in
  let condition =
    let ids_private = [id_iF'; id_oB'] in
    create_condition_dll ids_private id_iF
  in
  { r_vars= id_iF :: id_iF' :: id_oB :: id_oB' :: id_oF :: id_iB :: ids_shared
  ; r_root= lseg_fst_pat
  ; r_sigma= [lseg_snd_pat]
  ; r_new_sigma= [lseg_res]
  ; r_new_pi= gen_pi_res
  ; r_condition= condition }


let mk_rules_for_dll tenv (para : Predicates.hpara_dll) : rule list =
  if not Config.nelseg then
    let pts_pts = mk_rule_ptspts_dll tenv true true para in
    let pts_pedll = mk_rule_ptsdll_dll tenv Lseg_PE true false para in
    let pedll_pts = mk_rule_dllpts_dll tenv Lseg_PE false true para in
    let pedll_nedll = mk_rule_dlldll_dll tenv Lseg_PE Lseg_NE false false para in
    let nedll_pedll = mk_rule_dlldll_dll tenv Lseg_NE Lseg_PE false false para in
    let pedll_pedll = mk_rule_dlldll_dll tenv Lseg_PE Lseg_PE false false para in
    [pts_pts; pts_pedll; pedll_pts; pedll_nedll; nedll_pedll; pedll_pedll]
  else
    let ptspts_dll = mk_rule_ptspts_dll tenv true true para in
    let ptsdll_dll = mk_rule_ptsdll_dll tenv Lseg_NE true false para in
    let dllpts_dll = mk_rule_dllpts_dll tenv Lseg_NE false true para in
    let dlldll_dll = mk_rule_dlldll_dll tenv Lseg_NE Lseg_NE false false para in
    [ptspts_dll; ptsdll_dll; dllpts_dll; dlldll_dll]


(******************  End of DLL abstraction rules  ******************)
(******************  Start of Predicate Discovery  ******************)
let typ_get_recursive_flds tenv typ_exp =
  let filter typ (_, (t : Typ.t), _) =
    match t.desc with
    | Tstruct _ | Tint _ | Tfloat _ | Tvoid | Tfun | TVar _ ->
        false
    | Tptr (({desc= Tstruct _} as typ'), _) ->
        Typ.equal typ' typ
    | Tptr _ | Tarray _ ->
        false
  in
  match typ_exp with
  | Exp.Sizeof {typ} -> (
    match typ.desc with
    | Tstruct name -> (
      match Tenv.lookup tenv name with
      | Some {fields} ->
          List.map ~f:fst3 (List.filter ~f:(filter typ) fields)
      | None ->
          L.(debug Analysis Quiet)
            "@\ntyp_get_recursive_flds: unexpected %a unknown struct type: %a@." Exp.pp typ_exp
            Typ.Name.pp name ;
          [] (* ToDo: assert false *) )
    | Tint _ | Tvoid | Tfun | Tptr _ | Tfloat _ | Tarray _ | TVar _ ->
        [] )
  | Exp.Var _ ->
      [] (* type of |-> not known yet *)
  | Exp.Const _ ->
      []
  | _ ->
      L.internal_error "@\ntyp_get_recursive_flds: unexpected type expr: %a@." Exp.pp typ_exp ;
      assert false


let discover_para_roots tenv p root1 next1 root2 next2 : Predicates.hpara option =
  let eq_arg1 = Exp.equal root1 next1 in
  let eq_arg2 = Exp.equal root2 next2 in
  let precondition_check = (not eq_arg1) && not eq_arg2 in
  if not precondition_check then None
  else
    let corres = [(next1, next2)] in
    let todos = [(root1, root2)] in
    let sigma = p.Prop.sigma in
    match Match.find_partial_iso tenv (Prover.check_equal tenv p) corres todos sigma with
    | None ->
        None
    | Some (new_corres, new_sigma1, _, _) ->
        let hpara, _ = Match.hpara_create tenv new_corres new_sigma1 root1 next1 in
        Some hpara


let discover_para_dll_roots tenv p root1 blink1 flink1 root2 blink2 flink2 :
    Predicates.hpara_dll option =
  let eq_arg1 = Exp.equal root1 blink1 in
  let eq_arg1' = Exp.equal root1 flink1 in
  let eq_arg2 = Exp.equal root2 blink2 in
  let eq_arg2' = Exp.equal root2 flink2 in
  let precondition_check = not (eq_arg1 || eq_arg1' || eq_arg2 || eq_arg2') in
  if not precondition_check then None
  else
    let corres = [(blink1, blink2); (flink1, flink2)] in
    let todos = [(root1, root2)] in
    let sigma = p.Prop.sigma in
    match Match.find_partial_iso tenv (Prover.check_equal tenv p) corres todos sigma with
    | None ->
        None
    | Some (new_corres, new_sigma1, _, _) ->
        let hpara_dll, _ = Match.hpara_dll_create tenv new_corres new_sigma1 root1 blink1 flink1 in
        Some hpara_dll


let discover_para_candidates tenv p =
  let edges = ref [] in
  let add_edge edg = edges := edg :: !edges in
  let get_edges_strexp rec_flds root se =
    let is_rec_fld fld = List.exists ~f:(Fieldname.equal fld) rec_flds in
    match se with
    | Predicates.Eexp _ | Predicates.Earray _ ->
        ()
    | Predicates.Estruct (fsel, _) ->
        let fsel' = List.filter ~f:(fun (fld, _) -> is_rec_fld fld) fsel in
        let process (_, nextse) =
          match nextse with Predicates.Eexp (next, _) -> add_edge (root, next) | _ -> assert false
        in
        List.iter ~f:process fsel'
  in
  let rec get_edges_sigma = function
    | [] ->
        ()
    | Predicates.Hlseg _ :: sigma_rest | Predicates.Hdllseg _ :: sigma_rest ->
        get_edges_sigma sigma_rest
    | Predicates.Hpointsto (root, se, te) :: sigma_rest ->
        let rec_flds = typ_get_recursive_flds tenv te in
        get_edges_strexp rec_flds root se ; get_edges_sigma sigma_rest
  in
  let rec find_all_consecutive_edges found edges_seen = function
    | [] ->
        List.rev found
    | (e1, e2) :: edges_notseen ->
        let edges_others = List.rev_append edges_seen edges_notseen in
        let edges_matched = List.filter ~f:(fun (e1', _) -> Exp.equal e2 e1') edges_others in
        let new_found =
          let f found_acc (_, e3) = (e1, e2, e3) :: found_acc in
          List.fold ~f ~init:found edges_matched
        in
        let new_edges_seen = (e1, e2) :: edges_seen in
        find_all_consecutive_edges new_found new_edges_seen edges_notseen
  in
  let sigma = p.Prop.sigma in
  get_edges_sigma sigma ;
  find_all_consecutive_edges [] [] !edges


let discover_para_dll_candidates tenv p =
  let edges = ref [] in
  let add_edge edg = edges := edg :: !edges in
  let get_edges_strexp rec_flds root se =
    let is_rec_fld fld = List.exists ~f:(Fieldname.equal fld) rec_flds in
    match se with
    | Predicates.Eexp _ | Predicates.Earray _ ->
        ()
    | Predicates.Estruct (fsel, _) ->
        let fsel' = List.rev_filter ~f:(fun (fld, _) -> is_rec_fld fld) fsel in
        let convert_to_exp acc (_, se) =
          match se with Predicates.Eexp (e, _) -> e :: acc | _ -> assert false
        in
        let links = List.fold ~f:convert_to_exp ~init:[] fsel' in
        let rec iter_pairs = function
          | [] ->
              ()
          | x :: l ->
              List.iter ~f:(fun y -> add_edge (root, x, y)) l ;
              iter_pairs l
        in
        iter_pairs links
  in
  let rec get_edges_sigma = function
    | [] ->
        ()
    | Predicates.Hlseg _ :: sigma_rest | Predicates.Hdllseg _ :: sigma_rest ->
        get_edges_sigma sigma_rest
    | Predicates.Hpointsto (root, se, te) :: sigma_rest ->
        let rec_flds = typ_get_recursive_flds tenv te in
        get_edges_strexp rec_flds root se ; get_edges_sigma sigma_rest
  in
  let rec find_all_consecutive_edges found edges_seen = function
    | [] ->
        List.rev found
    | (iF, blink, flink) :: edges_notseen ->
        let edges_others = List.rev_append edges_seen edges_notseen in
        let edges_matched = List.filter ~f:(fun (e1', _, _) -> Exp.equal flink e1') edges_others in
        let new_found =
          let f found_acc (_, _, flink2) = (iF, blink, flink, flink2) :: found_acc in
          List.fold ~f ~init:found edges_matched
        in
        let new_edges_seen = (iF, blink, flink) :: edges_seen in
        find_all_consecutive_edges new_found new_edges_seen edges_notseen
  in
  let sigma = p.Prop.sigma in
  get_edges_sigma sigma ;
  find_all_consecutive_edges [] [] !edges


let discover_para tenv p =
  let candidates = discover_para_candidates tenv p in
  let already_defined para paras =
    List.exists ~f:(fun para' -> Match.hpara_iso tenv para para') paras
  in
  let f paras (root, next, out) =
    match discover_para_roots tenv p root next next out with
    | None ->
        paras
    | Some para ->
        if already_defined para paras then paras else para :: paras
  in
  List.fold ~f ~init:[] candidates


let discover_para_dll tenv p =
  (*
  L.out "@[.... Called discover_dll para ...@.";
  L.out "@[<4>  PROP : %a@\n@." pp_prop p;
  *)
  let candidates = discover_para_dll_candidates tenv p in
  let already_defined para paras =
    List.exists ~f:(fun para' -> Match.hpara_dll_iso tenv para para') paras
  in
  let f paras (iF, oB, iF', oF) =
    match discover_para_dll_roots tenv p iF oB iF' iF' iF oF with
    | None ->
        paras
    | Some para ->
        if already_defined para paras then paras else para :: paras
  in
  List.fold ~f ~init:[] candidates


(******************  End of Predicate Discovery  ******************)
(****************** Start of the ADT abs_rules ******************)

(** Type of parameter for abstraction rules *)
type para_ty = SLL of Predicates.hpara | DLL of Predicates.hpara_dll

(** Rule set: a list of rules of a given type *)
type rule_set = para_ty * rule 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 =
  List.map ~f:(fun (e1, e2) -> (Predicates.exp_sub subst e1, Predicates.exp_sub subst e2)) eqs


let eqs_solve ids_in eqs_in =
  let rec solve (sub : Predicates.subst) (eqs : (Exp.t * Exp.t) list) : Predicates.subst option =
    let do_default id e eqs_rest =
      if not (List.exists ~f:(fun id' -> Ident.equal id id') ids_in) then None
      else
        let sub' =
          match Predicates.extend_sub sub id e with
          | None ->
              L.internal_error "@\n@\nERROR : Buggy Implementation.@\n@." ;
              assert false
          | Some sub' ->
              sub'
        in
        let eqs_rest' = eqs_sub sub' eqs_rest in
        solve sub' eqs_rest'
    in
    match eqs with
    | [] ->
        Some sub
    | (e1, e2) :: eqs_rest when Exp.equal e1 e2 ->
        solve sub eqs_rest
    | (Exp.Var id1, (Exp.Const _ as e2)) :: eqs_rest ->
        do_default id1 e2 eqs_rest
    | ((Exp.Const _ as e1), (Exp.Var _ as e2)) :: eqs_rest ->
        solve sub ((e2, e1) :: eqs_rest)
    | ((Exp.Var id1 as e1), (Exp.Var id2 as e2)) :: eqs_rest ->
        let n = Ident.compare id1 id2 in
        if Int.equal n 0 then solve sub eqs_rest
        else if n > 0 then solve sub ((e2, e1) :: eqs_rest)
        else do_default id1 e2 eqs_rest
    | _ :: _ ->
        None
  in
  let compute_ids sub =
    let sub_list = Predicates.sub_to_list sub in
    let sub_dom = List.map ~f:fst sub_list in
    let filter id = not (List.exists ~f:(fun id' -> Ident.equal id id') sub_dom) in
    List.filter ~f:filter ids_in
  in
  match solve Predicates.sub_empty eqs_in with
  | None ->
      None
  | Some sub ->
      Some (compute_ids sub, sub)


let sigma_special_cases_eqs sigma =
  let rec f ids_acc eqs_acc sigma_acc = function
    | [] ->
        [(List.rev ids_acc, List.rev eqs_acc, List.rev sigma_acc)]
    | (Predicates.Hpointsto _ as hpred) :: sigma_rest ->
        f ids_acc eqs_acc (hpred :: sigma_acc) sigma_rest
    | (Predicates.Hlseg (_, para, e1, e2, es) as hpred) :: sigma_rest ->
        let empty_case = f ids_acc ((e1, e2) :: eqs_acc) sigma_acc sigma_rest in
        let pointsto_case =
          let eids, para_inst = Predicates.hpara_instantiate para e1 e2 es in
          f (eids @ ids_acc) eqs_acc sigma_acc (para_inst @ sigma_rest)
        in
        let general_case = f ids_acc eqs_acc (hpred :: sigma_acc) sigma_rest in
        empty_case @ pointsto_case @ general_case
    | (Predicates.Hdllseg (_, para, e1, e2, e3, e4, es) as hpred) :: sigma_rest ->
        let empty_case = f ids_acc ((e1, e3) :: (e2, e4) :: eqs_acc) sigma_acc sigma_rest in
        let pointsto_case =
          let eids, para_inst = Predicates.hpara_dll_instantiate para e1 e2 e3 es in
          f (eids @ ids_acc) eqs_acc sigma_acc (para_inst @ sigma_rest)
        in
        let general_case = f ids_acc eqs_acc (hpred :: sigma_acc) sigma_rest in
        empty_case @ pointsto_case @ general_case
  in
  f [] [] [] sigma


let sigma_special_cases ids sigma : (Ident.t list * Predicates.hpred list) list =
  let special_cases_eqs = sigma_special_cases_eqs sigma in
  let special_cases_rev =
    let f acc (eids_cur, eqs_cur, sigma_cur) =
      let ids_all = ids @ eids_cur in
      match eqs_solve ids_all eqs_cur with
      | None ->
          acc
      | Some (ids_res, sub) ->
          (ids_res, List.map ~f:(Predicates.hpred_sub sub) sigma_cur) :: acc
    in
    List.fold ~f ~init:[] special_cases_eqs
  in
  List.rev special_cases_rev


let hpara_special_cases hpara : Predicates.hpara list =
  let update_para (evars', body') = {hpara with Predicates.evars= evars'; Predicates.body= body'} in
  let special_cases = sigma_special_cases hpara.Predicates.evars hpara.Predicates.body in
  List.map ~f:update_para special_cases


let hpara_special_cases_dll hpara : Predicates.hpara_dll list =
  let update_para (evars', body') =
    {hpara with Predicates.evars_dll= evars'; Predicates.body_dll= body'}
  in
  let special_cases = sigma_special_cases hpara.Predicates.evars_dll hpara.Predicates.body_dll in
  List.map ~f:update_para special_cases


let abs_rules_apply_rsets tenv (rsets : rule_set list) (p_in : Prop.normal Prop.t) :
    Prop.normal Prop.t =
  let apply_rule (changed, p) r =
    match sigma_rewrite tenv p r with
    | None ->
        (changed, p)
    | Some p' ->
        (*
    L.out "@[.... abstraction (rewritten in abs_rules) ....@.";
    L.out "@[<4>  PROP:%a@\n@." pp_prop p';
    *)
        (true, p')
  in
  let rec apply_rule_set p rset =
    let _, rules = rset in
    let changed, p' = List.fold ~f:apply_rule ~init:(false, p) rules in
    if changed then apply_rule_set p' rset else p'
  in
  List.fold ~f:apply_rule_set ~init:p_in rsets


let abs_rules_apply_lists tenv (p_in : Prop.normal Prop.t) : Prop.normal Prop.t =
  let new_rsets = ref [] 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
      let paras_dll = discover_para_dll tenv p in
      let closed_paras_sll = List.concat_map ~f:hpara_special_cases paras_sll in
      let closed_paras_dll = List.concat_map ~f:hpara_special_cases_dll paras_dll in
      (closed_paras_sll, closed_paras_dll)
    in
    let todo_paras_sll, todo_paras_dll =
      let eq_sll para rset =
        match rset with SLL para', _ -> Match.hpara_iso tenv para para' | _ -> false
      in
      let eq_dll para rset =
        match rset with DLL para', _ -> Match.hpara_dll_iso tenv para para' | _ -> false
      in
      let filter_sll para =
        (not (List.exists ~f:(eq_sll para) old_rsets))
        && not (List.exists ~f:(eq_sll para) !new_rsets)
      in
      let filter_dll para =
        (not (List.exists ~f:(eq_dll para) old_rsets))
        && not (List.exists ~f:(eq_dll para) !new_rsets)
      in
      let todo_paras_sll = List.filter ~f:filter_sll closed_paras_sll in
      let todo_paras_dll = List.filter ~f:filter_dll closed_paras_dll in
      (todo_paras_sll, todo_paras_dll)
    in
    let f_recurse () =
      let todo_rsets_sll =
        List.map ~f:(fun para -> (SLL para, mk_rules_for_sll tenv para)) todo_paras_sll
      in
      let todo_rsets_dll =
        List.map ~f:(fun para -> (DLL para, mk_rules_for_dll tenv para)) todo_paras_dll
      in
      new_rsets := !new_rsets @ todo_rsets_sll @ todo_rsets_dll ;
      let p' = abs_rules_apply_rsets tenv todo_rsets_sll p in
      let p'' = abs_rules_apply_rsets tenv todo_rsets_dll p' in
      discover_then_abstract p''
    in
    match (todo_paras_sll, todo_paras_dll) with [], [] -> p | _ -> f_recurse ()
  in
  let p1 = abs_rules_apply_rsets tenv 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 Main Abstraction Functions ******************)
let abstract_pure_part tenv p ~(from_abstract_footprint : bool) =
  let do_pure pure =
    let pi_filtered =
      let sigma = p.Prop.sigma in
      let fav_sigma = Prop.sigma_free_vars sigma |> Ident.set_of_sequence in
      let fav_nonpure = Prop.non_pure_free_vars p |> Ident.set_of_sequence in
      (* vars in current and footprint sigma *)
      let filter atom =
        Predicates.atom_free_vars atom
        |> Sequence.for_all ~f:(fun id ->
               if Ident.is_primed id then Ident.Set.mem id fav_sigma
               else if Ident.is_footprint id then Ident.Set.mem id fav_nonpure
               else true )
      in
      List.filter ~f:filter pure
    in
    let new_pure =
      List.fold
        ~f:(fun pi a ->
          match (a : Predicates.atom) with
          (* we only use Lt and Le because Gt and Ge are inserted in terms of Lt and Le. *)
          | Aeq (Const (Cint i), BinOp (Lt, _, _))
          | Aeq (BinOp (Lt, _, _), Const (Cint i))
          | Aeq (Const (Cint i), BinOp (Le, _, _))
          | Aeq (BinOp (Le, _, _), Const (Cint i))
            when IntLit.isone i ->
              a :: pi
          | Aeq (Var name, e) when not (Ident.is_primed name) -> (
            match e with Var _ | Const _ -> a :: pi | _ -> pi )
          | Aneq (Var _, _) | Apred (_, Var _ :: _) | Anpred (_, Var _ :: _) ->
              a :: pi
          | Aeq _ | Aneq _ | Apred _ | Anpred _ ->
              pi )
        ~init:[] pi_filtered
    in
    List.rev new_pure
  in
  let new_pure = do_pure (Prop.get_pure p) in
  let eprop' = Prop.set p ~pi:new_pure ~sub:Predicates.sub_empty in
  let eprop'' =
    if !BiabductionConfig.footprint && not from_abstract_footprint then
      let new_pi_footprint = do_pure p.Prop.pi_fp in
      Prop.set eprop' ~pi_fp:new_pi_footprint
    else eprop'
  in
  Prop.normalize tenv eprop''


(** Collect symbolic garbage from pi and sigma *)
let abstract_gc tenv p =
  let pi = p.Prop.pi in
  let p_without_pi = Prop.normalize tenv (Prop.set p ~pi:[]) in
  let fav_p_without_pi = Prop.free_vars p_without_pi |> Ident.set_of_sequence in
  (* let weak_filter atom =
     let fav_atom = atom_fav atom in
     IList.intersect compare fav_p_without_pi fav_atom in *)
  let check fav_seq =
    Sequence.is_empty fav_seq
    || (* non-empty intersection with [fav_p_without_pi] *)
    Sequence.exists fav_seq ~f:(fun id -> Ident.Set.mem id fav_p_without_pi)
  in
  let strong_filter = function
    | Predicates.Aeq (e1, e2) | Predicates.Aneq (e1, e2) ->
        check (Exp.free_vars e1) && check (Exp.free_vars e2)
    | (Predicates.Apred _ | Anpred _) as a ->
        check (Predicates.atom_free_vars a)
  in
  let new_pi = List.filter ~f:strong_filter pi in
  let prop = Prop.normalize tenv (Prop.set p ~pi:new_pi) in
  match Prop.prop_iter_create prop with
  | None ->
      prop
  | Some iter ->
      Prop.prop_iter_to_prop tenv (Prop.prop_iter_gc_fields iter)


(** find the id's in sigma reachable from the given roots *)
let sigma_reachable root_fav sigma =
  let reach_set = ref root_fav in
  let edges = ref [] in
  let do_hpred hpred =
    let hp_fav_set = Predicates.hpred_free_vars hpred |> Ident.set_of_sequence in
    let add_entry e = edges := (e, hp_fav_set) :: !edges in
    List.iter ~f:add_entry (Predicates.hpred_entries hpred)
  in
  List.iter ~f:do_hpred sigma ;
  let edge_fires (e, _) =
    match e with
    | Exp.Var id ->
        if Ident.is_primed id || Ident.is_footprint id then Ident.Set.mem id !reach_set else true
    | _ ->
        true
  in
  let rec apply_once edges_to_revisit edges_todo modified =
    match edges_todo with
    | [] ->
        (edges_to_revisit, modified)
    | edge :: edges_todo' ->
        if edge_fires edge then (
          reach_set := Ident.Set.union (snd edge) !reach_set ;
          apply_once edges_to_revisit edges_todo' true )
        else apply_once (edge :: edges_to_revisit) edges_todo' modified
  in
  let rec find_fixpoint edges_todo =
    let edges_to_revisit, modified = apply_once [] edges_todo false in
    if modified then find_fixpoint edges_to_revisit
  in
  find_fixpoint !edges ;
  (* L.d_str "reachable: ";
     Ident.Set.iter (fun id -> Predicates.d_exp (Exp.Var id); L.d_str " ") !reach_set;
     L.d_ln (); *)
  !reach_set


let check_observer_is_unsubscribed_deallocation tenv prop e =
  let pvar_opt =
    match Attribute.get_resource tenv prop e with
    | Some (Apred (Aresource {ra_vpath= Some (Dpvar pvar)}, _)) ->
        Some pvar
    | _ ->
        None
  in
  let loc = State.get_loc_exn () in
  match Attribute.get_observer tenv prop e with
  | Some (Apred (Aobserver, _)) -> (
    match pvar_opt with
    | Some pvar when Config.nsnotification_center_checker_backend ->
        L.d_strln
          ( " ERROR: Object " ^ Pvar.to_string pvar
          ^ " is being deallocated while still registered in a notification center" ) ;
        let desc = Localise.desc_registered_observer_being_deallocated pvar loc in
        raise (Exceptions.Registered_observer_being_deallocated (desc, __POS__))
    | _ ->
        () )
  | _ ->
      ()


let check_junk pname tenv prop =
  let leaks_reported = ref [] in
  let remove_junk_once fp_part fav_root sigma =
    let id_considered_reachable =
      (* reachability function *)
      let reach_set = sigma_reachable fav_root sigma in
      fun id -> Ident.Set.mem id reach_set
    in
    let should_remove_hpred entries =
      let predicate = function
        | Exp.Var id ->
            (Ident.is_primed id || Ident.is_footprint id)
            && (not (Ident.Set.mem id fav_root))
            && not (id_considered_reachable id)
        | _ ->
            false
      in
      List.for_all ~f:predicate entries
    in
    let rec remove_junk_recursive sigma_done sigma_todo =
      match sigma_todo with
      | [] ->
          List.rev sigma_done
      | hpred :: sigma_todo' ->
          let entries = Predicates.hpred_entries hpred in
          if should_remove_hpred entries then (
            let part = if fp_part then "footprint" else "normal" in
            L.d_printfln ".... Prop with garbage in %s part ...." part ;
            L.d_increase_indent () ;
            L.d_strln "PROP:" ;
            Prop.d_prop prop ;
            L.d_ln () ;
            L.d_strln "PREDICATE:" ;
            Prop.d_sigma [hpred] ;
            L.d_ln () ;
            let alloc_attribute =
              (* find the alloc attribute of one of the roots of hpred, if it exists *)
              let res = ref None in
              let do_entry e =
                check_observer_is_unsubscribed_deallocation tenv prop e ;
                match Attribute.get_wontleak tenv prop e with
                | Some (Apred ((Awont_leak as a), _)) ->
                    L.d_strln "WONT_LEAK" ;
                    res := Some a
                | _ -> (
                  match Attribute.get_resource tenv prop e with
                  | Some (Apred ((Aresource {ra_kind= Racquire} as a), _)) ->
                      L.d_str "ATTRIBUTE: " ;
                      PredSymb.d_attribute a ;
                      L.d_ln () ;
                      res := Some a
                  | _ -> (
                    match Attribute.get_undef tenv prop e with
                    | Some (Apred ((Aundef _ as a), _)) ->
                        L.d_strln "UNDEF" ;
                        res := Some a
                    | _ ->
                        () ) )
              in
              List.iter ~f:do_entry entries ; !res
            in
            L.d_decrease_indent () ;
            let is_undefined =
              Option.value_map ~f:PredSymb.is_undef ~default:false alloc_attribute
            in
            let resource =
              match Errdesc.hpred_is_open_resource tenv prop hpred with
              | Some res ->
                  res
              | None ->
                  PredSymb.Rmemory PredSymb.Mmalloc
            in
            let ml_bucket_opt =
              match resource with
              | (PredSymb.Rmemory PredSymb.Mnew | PredSymb.Rmemory PredSymb.Mnew_array)
                when Language.curr_language_is Clang ->
                  Mleak_buckets.should_raise_cpp_leak
              | _ ->
                  None
            in
            let exn_leak =
              Exceptions.Leak
                ( fp_part
                , Errdesc.explain_leak tenv hpred prop alloc_attribute ml_bucket_opt
                , !Absarray.array_abstraction_performed
                , resource
                , __POS__ )
            in
            let ignore_resource, exn =
              match (alloc_attribute, resource) with
              | Some PredSymb.Awont_leak, Rmemory _ ->
                  (true, exn_leak)
              | Some _, Rmemory Mobjc ->
                  (true, exn_leak)
              | (Some _, Rmemory Mnew | Some _, Rmemory Mnew_array)
                when Language.curr_language_is Clang ->
                  (is_none ml_bucket_opt, exn_leak)
              | Some _, Rmemory _ ->
                  (Language.curr_language_is Java, exn_leak)
              | Some _, Rignore ->
                  (true, exn_leak)
              | Some _, Rfile ->
                  (false, exn_leak)
              | Some _, Rlock ->
                  (false, exn_leak)
              | _ ->
                  (Language.curr_language_is Java, exn_leak)
            in
            let already_reported () =
              let attr_opt_equal ao1 ao2 =
                match (ao1, ao2) with
                | None, None ->
                    true
                | Some a1, Some a2 ->
                    PredSymb.equal a1 a2
                | Some _, None | None, Some _ ->
                    false
              in
              (is_none alloc_attribute && not (List.is_empty !leaks_reported))
              || (* None attribute only reported if it's the first one *)
              List.mem ~equal:attr_opt_equal !leaks_reported alloc_attribute
            in
            let ignore_leak =
              !BiabductionConfig.allow_leak || ignore_resource || is_undefined
              || already_reported ()
            in
            let report_and_continue =
              Language.curr_language_is Java || !BiabductionConfig.footprint
            in
            let report_leak () =
              if not report_and_continue then raise exn
              else (
                Reporting.log_issue_deprecated_using_state Exceptions.Error pname exn ;
                leaks_reported := alloc_attribute :: !leaks_reported )
            in
            if not ignore_leak then report_leak () ;
            remove_junk_recursive sigma_done sigma_todo' )
          else remove_junk_recursive (hpred :: sigma_done) sigma_todo'
    in
    remove_junk_recursive [] sigma
  in
  let rec remove_junk fp_part fav_root sigma =
    (* call remove_junk_once until sigma stops shrinking *)
    let sigma' = remove_junk_once fp_part fav_root sigma in
    if Int.equal (List.length sigma') (List.length sigma) then sigma'
    else remove_junk fp_part fav_root sigma'
  in
  let sigma_new =
    let fav_sub = Predicates.subst_free_vars prop.Prop.sub |> Ident.set_of_sequence in
    let fav_sub_sigmafp =
      Prop.sigma_free_vars prop.Prop.sigma_fp |> Ident.set_of_sequence ~init:fav_sub
    in
    remove_junk false fav_sub_sigmafp prop.Prop.sigma
  in
  let sigma_fp_new = remove_junk true Ident.Set.empty prop.Prop.sigma_fp in
  if Prop.equal_sigma prop.Prop.sigma sigma_new && Prop.equal_sigma prop.Prop.sigma_fp sigma_fp_new
  then 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:Predicates.sub_empty in
    let drop id = Int.equal 1 (count id + propcount id) in
    let keep atom = not (Sequence.exists ~f:drop (Predicates.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 = Predicates.atom

        let compare = Predicates.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 =
  Absarray.array_abstraction_performed := false ;
  check_junk pname tenv prop


(** Remove redundant elements in an array, and check for junk afterwards *)
let remove_redundant_array_elements pname tenv prop =
  Absarray.array_abstraction_performed := false ;
  let prop' = Absarray.remove_redundant_elements tenv prop in
  check_junk pname tenv prop'


let abstract_prop pname tenv ~(rename_primed : bool) ~(from_abstract_footprint : bool) p =
  Absarray.array_abstraction_performed := false ;
  let pure_abs_p = abstract_pure_part tenv ~from_abstract_footprint:true p in
  let array_abs_p =
    if from_abstract_footprint then pure_abs_p
    else
      abstract_pure_part tenv ~from_abstract_footprint
        (Absarray.abstract_array_check tenv pure_abs_p)
  in
  let abs_p = abs_rules_apply tenv array_abs_p in
  let abs_p = abstract_gc tenv abs_p in
  (* abstraction might enable more gc *)
  let abs_p = check_junk pname tenv abs_p in
  let ren_abs_p =
    if rename_primed then Prop.prop_rename_primed_footprint_vars tenv abs_p else abs_p
  in
  ren_abs_p


let get_local_stack cur_sigma init_sigma =
  let filter_stack = function
    | Predicates.Hpointsto (Exp.Lvar _, _, _) ->
        true
    | Predicates.Hpointsto _ | Predicates.Hlseg _ | Predicates.Hdllseg _ ->
        false
  in
  let get_stack_var = function
    | Predicates.Hpointsto (Exp.Lvar pvar, _, _) ->
        pvar
    | Predicates.Hpointsto _ | Predicates.Hlseg _ | Predicates.Hdllseg _ ->
        assert false
  in
  let filter_local_stack olds = function
    | Predicates.Hpointsto (Exp.Lvar pvar, _, _) ->
        not (List.exists ~f:(Pvar.equal pvar) olds)
    | Predicates.Hpointsto _ | Predicates.Hlseg _ | Predicates.Hdllseg _ ->
        false
  in
  let init_stack = List.filter ~f:filter_stack init_sigma in
  let init_stack_pvars = List.map ~f:get_stack_var init_stack in
  let cur_local_stack = List.filter ~f:(filter_local_stack init_stack_pvars) cur_sigma in
  let cur_local_stack_pvars = List.map ~f:get_stack_var cur_local_stack in
  (cur_local_stack, cur_local_stack_pvars)


(** Extract the footprint, add a local stack and return it as a prop *)
let extract_footprint_for_abs (p : 'a Prop.t) : Prop.exposed Prop.t * Pvar.t list =
  let sigma = p.Prop.sigma in
  let pi_fp = p.Prop.pi_fp in
  let sigma_fp = p.Prop.sigma_fp in
  let local_stack, local_stack_pvars = get_local_stack sigma sigma_fp in
  let p0 = Prop.from_sigma (local_stack @ sigma_fp) in
  let p1 = Prop.set p0 ~pi:pi_fp in
  (p1, local_stack_pvars)


let remove_local_stack sigma pvars =
  let filter_non_stack = function
    | Predicates.Hpointsto (Exp.Lvar pvar, _, _) ->
        not (List.exists ~f:(Pvar.equal pvar) pvars)
    | Predicates.Hpointsto _ | Predicates.Hlseg _ | Predicates.Hdllseg _ ->
        true
  in
  List.filter ~f:filter_non_stack sigma


(** [prop_set_fooprint p p_foot] removes a local stack from [p_foot], and sets proposition [p_foot]
    as footprint of [p]. *)
let set_footprint_for_abs (p : 'a Prop.t) (p_foot : 'a Prop.t) local_stack_pvars :
    Prop.exposed Prop.t =
  let p_foot_pure = Prop.get_pure p_foot in
  let p_sigma_fp = p_foot.Prop.sigma in
  let pi = p_foot_pure in
  let sigma = remove_local_stack p_sigma_fp local_stack_pvars in
  Prop.set p ~pi_fp:pi ~sigma_fp:sigma


(** Abstract the footprint of prop *)
let abstract_footprint pname (tenv : Tenv.t) (prop : Prop.normal Prop.t) : Prop.normal Prop.t =
  let p, added_local_vars = extract_footprint_for_abs prop in
  let p_abs =
    abstract_prop pname tenv ~rename_primed:false ~from_abstract_footprint:true
      (Prop.normalize tenv p)
  in
  let prop' = set_footprint_for_abs prop p_abs added_local_vars in
  Prop.normalize tenv prop'


let abstract_ pname pay tenv p =
  if pay then SymOp.pay () ;
  (* pay one symop *)
  let p' = if !BiabductionConfig.footprint then abstract_footprint pname tenv p else p in
  abstract_prop pname tenv ~rename_primed:true ~from_abstract_footprint:false p'


let abstract pname tenv p = abstract_ pname true tenv p

let abstract_no_symop pname tenv p = abstract_ pname false tenv p

let lifted_abstract pname tenv pset =
  let f p = if Prover.check_inconsistency tenv p then None else Some (abstract pname tenv p) in
  let abstracted_pset = Propset.map_option tenv f pset in
  abstracted_pset

(***************** End of Main Abstraction Functions *****************)