infer_clone/infer/src/IR/Cfg.ml

(*
 * Copyright (c) 2009 - 2013 Monoidics ltd.
 * Copyright (c) 2013 - present Facebook, Inc.
 * All rights reserved.
 *
 * This source code is licensed under the BSD style license found in the
 * LICENSE file in the root directory of this source tree. An additional grant
 * of patent rights can be found in the PATENTS file in the same directory.
 *)

open! IStd
module L = Logging
module F = Format

(** data type for the control flow graph *)
type t = Procdesc.t Typ.Procname.Hash.t

(** create a new empty cfg *)
let create_cfg () = Typ.Procname.Hash.create 16

let add_proc_desc cfg pname pdesc = Typ.Procname.Hash.add cfg pname pdesc

let remove_proc_desc cfg pname = Typ.Procname.Hash.remove cfg pname

let iter_proc_desc cfg f = Typ.Procname.Hash.iter f cfg

let find_proc_desc_from_name cfg pname =
  try Some (Typ.Procname.Hash.find cfg pname) with Not_found -> None


(** Create a new procdesc *)
let create_proc_desc cfg (proc_attributes: ProcAttributes.t) =
  let pdesc = Procdesc.from_proc_attributes ~called_from_cfg:true proc_attributes in
  add_proc_desc cfg proc_attributes.proc_name pdesc ;
  pdesc


(** Iterate over all the nodes in the cfg *)
let iter_all_nodes ?(sorted= false) f cfg =
  let do_proc_desc _ (pdesc: Procdesc.t) =
    List.iter ~f:(fun node -> f pdesc node) (Procdesc.get_nodes pdesc)
  in
  if not sorted then iter_proc_desc cfg do_proc_desc
  else
    Typ.Procname.Hash.fold
      (fun _ pdesc desc_nodes ->
        List.fold
          ~f:(fun desc_nodes node -> (pdesc, node) :: desc_nodes)
          ~init:desc_nodes (Procdesc.get_nodes pdesc))
      cfg []
    |> List.sort ~cmp:[%compare : Procdesc.t * Procdesc.Node.t]
    |> List.iter ~f:(fun (d, n) -> f d n)


(** Get all the procdescs (defined and declared) *)
let get_all_procs cfg =
  let procs = ref [] in
  let f _ pdesc = procs := pdesc :: !procs in
  iter_proc_desc cfg f ; !procs


(** Get the procedures whose body is defined in this cfg *)
let get_defined_procs cfg = List.filter ~f:Procdesc.is_defined (get_all_procs cfg)

(** checks whether a cfg is connected or not *)
let check_cfg_connectedness cfg =
  let is_exit_node n =
    match Procdesc.Node.get_kind n with Procdesc.Node.Exit_node _ -> true | _ -> false
  in
  let broken_node n =
    let succs = Procdesc.Node.get_succs n in
    let preds = Procdesc.Node.get_preds n in
    match Procdesc.Node.get_kind n with
    | Procdesc.Node.Start_node _ ->
        Int.equal (List.length succs) 0 || List.length preds > 0
    | Procdesc.Node.Exit_node _ ->
        List.length succs > 0 || Int.equal (List.length preds) 0
    | Procdesc.Node.Stmt_node _ | Procdesc.Node.Prune_node _ | Procdesc.Node.Skip_node _ ->
        Int.equal (List.length succs) 0 || Int.equal (List.length preds) 0
    | Procdesc.Node.Join_node ->
      (* Join node has the exception that it may be without predecessors
         and pointing to an exit node *)
      (* if the if brances end with a return *)
      match succs with [n'] when is_exit_node n' -> false | _ -> Int.equal (List.length preds) 0
  in
  let do_pdesc pd =
    let pname = Procdesc.get_proc_name pd in
    let nodes = Procdesc.get_nodes pd in
    (* TODO (T20302015): also check the CFGs for the C-like procedures *)
    if not Config.keep_going && Typ.Procname.is_java pname && List.exists ~f:broken_node nodes then
      L.(die InternalError) "Broken CFG on %a" Typ.Procname.pp pname
  in
  let pdescs = get_all_procs cfg in
  List.iter ~f:do_pdesc pdescs


module type Data = sig
  val of_cfg : t -> Sqlite3.Data.t

  val of_source_file : SourceFile.t -> Sqlite3.Data.t

  val to_cfg : Sqlite3.Data.t -> t
end

module Data : Data = struct
  let of_source_file file = Sqlite3.Data.TEXT (SourceFile.to_string file)

  let of_cfg x = Sqlite3.Data.BLOB (Marshal.to_string x [])

  let to_cfg = function[@warning "-8"] Sqlite3.Data.BLOB b -> Marshal.from_string b 0
end

let get_load_statement =
  ResultsDatabase.register_statement "SELECT cfgs FROM cfg WHERE source_file = :k"


let load source =
  let load_stmt = get_load_statement () in
  Data.of_source_file source |> Sqlite3.bind load_stmt 1
  |> SqliteUtils.check_sqlite_error ~log:"load bind source file" ;
  SqliteUtils.sqlite_result_step ~finalize:false ~log:"Cfg.load" load_stmt
  |> Option.map ~f:Data.to_cfg


(** Save the .attr files for the procedures in the cfg. *)
let save_attributes source_file cfg =
  let save_proc pdesc =
    let attributes = Procdesc.get_attributes pdesc in
    let loc = attributes.loc in
    let attributes' =
      let loc' = if Location.equal loc Location.dummy then {loc with file= source_file} else loc in
      {attributes with loc= loc'; source_file_captured= source_file}
    in
    Attributes.store attributes'
  in
  List.iter ~f:save_proc (get_all_procs cfg)


(** Inline a synthetic (access or bridge) method. *)
let inline_synthetic_method ret_id etl pdesc loc_call : Sil.instr option =
  let modified = ref None in
  let found instr instr' =
    modified := Some instr' ;
    L.(debug Analysis Verbose)
      "XX inline_synthetic_method found instr: %a@." (Sil.pp_instr Pp.text) instr ;
    L.(debug Analysis Verbose)
      "XX inline_synthetic_method instr': %a@." (Sil.pp_instr Pp.text) instr'
  in
  let do_instr _ instr =
    match (instr, ret_id, etl) with
    | ( Sil.Load (_, Exp.Lfield (Exp.Var _, fn, ft), bt, _)
      , Some (ret_id, _)
      , [(* getter for fields *) (e1, _)] ) ->
        let instr' = Sil.Load (ret_id, Exp.Lfield (e1, fn, ft), bt, loc_call) in
        found instr instr'
    | Sil.Load (_, Exp.Lfield (Exp.Lvar pvar, fn, ft), bt, _), Some (ret_id, _), []
      when Pvar.is_global pvar ->
        (* getter for static fields *)
        let instr' = Sil.Load (ret_id, Exp.Lfield (Exp.Lvar pvar, fn, ft), bt, loc_call) in
        found instr instr'
    | Sil.Store (Exp.Lfield (_, fn, ft), bt, _, _), _, [(* setter for fields *) (e1, _); (e2, _)] ->
        let instr' = Sil.Store (Exp.Lfield (e1, fn, ft), bt, e2, loc_call) in
        found instr instr'
    | Sil.Store (Exp.Lfield (Exp.Lvar pvar, fn, ft), bt, _, _), _, [(e1, _)]
      when Pvar.is_global pvar ->
        (* setter for static fields *)
        let instr' = Sil.Store (Exp.Lfield (Exp.Lvar pvar, fn, ft), bt, e1, loc_call) in
        found instr instr'
    | Sil.Call (ret_id', Exp.Const Const.Cfun pn, etl', _, cf), _, _
      when Bool.equal (is_none ret_id) (is_none ret_id')
           && Int.equal (List.length etl') (List.length etl) ->
        let instr' = Sil.Call (ret_id, Exp.Const (Const.Cfun pn), etl, loc_call, cf) in
        found instr instr'
    | Sil.Call (ret_id', Exp.Const Const.Cfun pn, etl', _, cf), _, _
      when Bool.equal (is_none ret_id) (is_none ret_id')
           && Int.equal (List.length etl' + 1) (List.length etl) ->
        let etl1 =
          match List.rev etl with
          (* remove last element *)
          | _ :: l ->
              List.rev l
          | [] ->
              assert false
        in
        let instr' = Sil.Call (ret_id, Exp.Const (Const.Cfun pn), etl1, loc_call, cf) in
        found instr instr'
    | _ ->
        ()
  in
  Procdesc.iter_instrs do_instr pdesc ;
  !modified


(** Find synthetic (access or bridge) Java methods in the procedure and inline them in the cfg. *)
let proc_inline_synthetic_methods cfg pdesc : unit =
  let instr_inline_synthetic_method = function
    | Sil.Call (ret_id, Exp.Const Const.Cfun pn, etl, loc, _) -> (
      match find_proc_desc_from_name cfg pn with
      | Some pd ->
          let is_access = Typ.Procname.java_is_access_method pn in
          let attributes = Procdesc.get_attributes pd in
          let is_synthetic = attributes.is_synthetic_method in
          let is_bridge = attributes.is_bridge_method in
          if is_access || is_bridge || is_synthetic then inline_synthetic_method ret_id etl pd loc
          else None
      | None ->
          None )
    | _ ->
        None
  in
  let node_inline_synthetic_methods node =
    let modified = ref false in
    let do_instr instr =
      match instr_inline_synthetic_method instr with
      | None ->
          instr
      | Some instr' ->
          modified := true ;
          instr'
    in
    let instrs = Procdesc.Node.get_instrs node in
    let instrs' = List.map ~f:do_instr instrs in
    if !modified then Procdesc.Node.replace_instrs node instrs'
  in
  Procdesc.iter_nodes node_inline_synthetic_methods pdesc


(** Inline the java synthetic methods in the cfg *)
let inline_java_synthetic_methods cfg =
  let f pname pdesc = if Typ.Procname.is_java pname then proc_inline_synthetic_methods cfg pdesc in
  iter_proc_desc cfg f


(** compute the list of procedures added or changed in [cfg_new] over [cfg_old] *)
let mark_unchanged_pdescs cfg_new cfg_old =
  let pdescs_eq (pd1: Procdesc.t) (pd2: Procdesc.t) =
    (* map of exp names in pd1 -> exp names in pd2 *)
    let exp_map = ref Exp.Map.empty in
    (* map of node id's in pd1 -> node id's in pd2 *)
    let node_map = ref Procdesc.NodeMap.empty in
    (* formals are the same if their types are the same *)
    let formals_eq formals1 formals2 =
      List.equal ~equal:(fun (_, typ1) (_, typ2) -> Typ.equal typ1 typ2) formals1 formals2
    in
    let nodes_eq n1s n2s =
      (* nodes are the same if they have the same id, instructions, and succs/preds up to renaming
         with [exp_map] and [id_map] *)
      let node_eq (n1: Procdesc.Node.t) (n2: Procdesc.Node.t) =
        let compare_id (n1: Procdesc.Node.t) (n2: Procdesc.Node.t) =
          try
            let n1_mapping = Procdesc.NodeMap.find n1 !node_map in
            Procdesc.Node.compare n1_mapping n2
          with Not_found ->
            (* assume id's are equal and enforce by adding to [id_map] *)
            node_map := Procdesc.NodeMap.add n1 n2 !node_map ;
            0
        in
        let instrs_eq instrs1 instrs2 =
          List.equal
            ~equal:(fun i1 i2 ->
              let n, exp_map' = Sil.compare_structural_instr i1 i2 !exp_map in
              exp_map := exp_map' ;
              Int.equal n 0)
            instrs1 instrs2
        in
        Int.equal (compare_id n1 n2) 0
        && List.equal ~equal:Procdesc.Node.equal (Procdesc.Node.get_succs n1)
             (Procdesc.Node.get_succs n2)
        && List.equal ~equal:Procdesc.Node.equal (Procdesc.Node.get_preds n1)
             (Procdesc.Node.get_preds n2)
        && instrs_eq (Procdesc.Node.get_instrs n1) (Procdesc.Node.get_instrs n2)
      in
      try List.for_all2_exn ~f:node_eq n1s n2s with Invalid_argument _ -> false
    in
    let att1 = Procdesc.get_attributes pd1 and att2 = Procdesc.get_attributes pd2 in
    Bool.equal att1.is_defined att2.is_defined && Typ.equal att1.ret_type att2.ret_type
    && formals_eq att1.formals att2.formals
    && nodes_eq (Procdesc.get_nodes pd1) (Procdesc.get_nodes pd2)
  in
  let mark_pdesc_if_unchanged pname (new_pdesc: Procdesc.t) =
    try
      let old_pdesc = Typ.Procname.Hash.find cfg_old pname in
      let changed =
        (* in continue_capture mode keep the old changed bit *)
        Config.continue_capture && (Procdesc.get_attributes old_pdesc).changed
        || not (pdescs_eq old_pdesc new_pdesc)
      in
      (Procdesc.get_attributes new_pdesc).changed <- changed
    with Not_found -> ()
  in
  Typ.Procname.Hash.iter mark_pdesc_if_unchanged cfg_new


let get_store_statement =
  ResultsDatabase.register_statement "INSERT OR REPLACE INTO cfg VALUES (:source, :cfgs)"


let store source_file cfg =
  inline_java_synthetic_methods cfg ;
  ( if Config.incremental_procs then
      match load source_file with Some old_cfg -> mark_unchanged_pdescs cfg old_cfg | None -> () ) ;
  (* NOTE: it's important to write attribute files to disk before writing cfgs to disk.
     OndemandCapture module relies on it - it uses existance of the cfg as a barrier to make
     sure that all attributes were written to disk (but not necessarily flushed) *)
  save_attributes source_file cfg ;
  let store_stmt = get_store_statement () in
  Data.of_source_file source_file |> Sqlite3.bind store_stmt 1
  (* :source *)
  |> SqliteUtils.check_sqlite_error ~log:"store bind source file" ;
  Data.of_cfg cfg |> Sqlite3.bind store_stmt 2
  (* :cfg *)
  |> SqliteUtils.check_sqlite_error ~log:"store bind cfg" ;
  SqliteUtils.sqlite_unit_step ~finalize:false ~log:"Cfg.store" store_stmt


(** Applies convert_instr_list to all the instructions in all the nodes of the cfg *)
let convert_cfg ~callee_pdesc ~resolved_pdesc convert_instr_list =
  let resolved_pname = Procdesc.get_proc_name resolved_pdesc
  and callee_start_node = Procdesc.get_start_node callee_pdesc
  and callee_exit_node = Procdesc.get_exit_node callee_pdesc in
  let convert_node_kind = function
    | Procdesc.Node.Start_node _ ->
        Procdesc.Node.Start_node resolved_pname
    | Procdesc.Node.Exit_node _ ->
        Procdesc.Node.Exit_node resolved_pname
    | node_kind ->
        node_kind
  in
  let node_map = ref Procdesc.NodeMap.empty in
  let rec convert_node node =
    let loc = Procdesc.Node.get_loc node
    and kind = convert_node_kind (Procdesc.Node.get_kind node)
    and instrs = convert_instr_list (Procdesc.Node.get_instrs node) in
    Procdesc.create_node resolved_pdesc loc kind instrs
  and loop callee_nodes =
    match callee_nodes with
    | [] ->
        []
    | node :: other_node ->
        let converted_node =
          try Procdesc.NodeMap.find node !node_map with Not_found ->
            let new_node = convert_node node
            and successors = Procdesc.Node.get_succs node
            and exn_nodes = Procdesc.Node.get_exn node in
            node_map := Procdesc.NodeMap.add node new_node !node_map ;
            if Procdesc.Node.equal node callee_start_node then
              Procdesc.set_start_node resolved_pdesc new_node ;
            if Procdesc.Node.equal node callee_exit_node then
              Procdesc.set_exit_node resolved_pdesc new_node ;
            Procdesc.node_set_succs_exn callee_pdesc new_node (loop successors) (loop exn_nodes) ;
            new_node
        in
        converted_node :: loop other_node
  in
  ignore (loop [callee_start_node]) ;
  resolved_pdesc


(** clone a procedure description and apply the type substitutions where
      the parameters are used *)
let specialize_types_proc callee_pdesc resolved_pdesc substitutions =
  let resolved_pname = Procdesc.get_proc_name resolved_pdesc in
  let convert_pvar pvar = Pvar.mk (Pvar.get_name pvar) resolved_pname in
  let mk_ptr_typ typename =
    (* Only consider pointers from Java objects for now *)
    Typ.mk (Tptr (Typ.mk (Tstruct typename), Typ.Pk_pointer))
  in
  let convert_exp = function
    | Exp.Lvar origin_pvar ->
        Exp.Lvar (convert_pvar origin_pvar)
    | exp ->
        exp
  in
  let subst_map = ref Ident.IdentMap.empty in
  let redirect_typename origin_id =
    try Some (Ident.IdentMap.find origin_id !subst_map) with Not_found -> None
  in
  let convert_instr instrs = function
    | Sil.Load
        ( id
        , (Exp.Lvar origin_pvar as origin_exp)
        , {Typ.desc= Tptr ({desc= Tstruct origin_typename}, Pk_pointer)}
        , loc ) ->
        let specialized_typname =
          try Mangled.Map.find (Pvar.get_name origin_pvar) substitutions with Not_found ->
            origin_typename
        in
        subst_map := Ident.IdentMap.add id specialized_typname !subst_map ;
        Sil.Load (id, convert_exp origin_exp, mk_ptr_typ specialized_typname, loc) :: instrs
    | Sil.Load (id, (Exp.Var origin_id as origin_exp), ({Typ.desc= Tstruct _} as origin_typ), loc) ->
        let updated_typ : Typ.t =
          try Typ.mk ~default:origin_typ (Tstruct (Ident.IdentMap.find origin_id !subst_map))
          with Not_found -> origin_typ
        in
        Sil.Load (id, convert_exp origin_exp, updated_typ, loc) :: instrs
    | Sil.Load (id, origin_exp, origin_typ, loc) ->
        Sil.Load (id, convert_exp origin_exp, origin_typ, loc) :: instrs
    | Sil.Store (assignee_exp, origin_typ, origin_exp, loc) ->
        let set_instr =
          Sil.Store (convert_exp assignee_exp, origin_typ, convert_exp origin_exp, loc)
        in
        set_instr :: instrs
    | Sil.Call
        ( return_ids
        , Exp.Const Const.Cfun Typ.Procname.Java callee_pname_java
        , (Exp.Var id, _) :: origin_args
        , loc
        , call_flags )
      when call_flags.CallFlags.cf_virtual && redirect_typename id <> None ->
        let redirected_typename = Option.value_exn (redirect_typename id) in
        let redirected_typ = mk_ptr_typ redirected_typename in
        let redirected_pname =
          Typ.Procname.replace_class (Typ.Procname.Java callee_pname_java) redirected_typename
        in
        let args =
          let other_args = List.map ~f:(fun (exp, typ) -> (convert_exp exp, typ)) origin_args in
          (Exp.Var id, redirected_typ) :: other_args
        in
        let call_instr =
          Sil.Call (return_ids, Exp.Const (Const.Cfun redirected_pname), args, loc, call_flags)
        in
        call_instr :: instrs
    | Sil.Call (return_ids, origin_call_exp, origin_args, loc, call_flags) ->
        let converted_args = List.map ~f:(fun (exp, typ) -> (convert_exp exp, typ)) origin_args in
        let call_instr =
          Sil.Call (return_ids, convert_exp origin_call_exp, converted_args, loc, call_flags)
        in
        call_instr :: instrs
    | Sil.Prune (origin_exp, loc, is_true_branch, if_kind) ->
        Sil.Prune (convert_exp origin_exp, loc, is_true_branch, if_kind) :: instrs
    | Sil.Declare_locals (typed_vars, loc) ->
        let new_typed_vars =
          List.map ~f:(fun (pvar, typ) -> (convert_pvar pvar, typ)) typed_vars
        in
        Sil.Declare_locals (new_typed_vars, loc) :: instrs
    | Sil.Nullify _ | Abstract _ | Sil.Remove_temps _ ->
        (* these are generated instructions that will be replaced by the preanalysis *)
        instrs
  in
  let convert_instr_list instrs = List.fold ~f:convert_instr ~init:[] instrs |> List.rev in
  convert_cfg ~callee_pdesc ~resolved_pdesc convert_instr_list


(** Creates a copy of a procedure description and a list of type substitutions of the form
    (name, typ) where name is a parameter. The resulting proc desc is isomorphic but
    all the type of the parameters are replaced in the instructions according to the list.
    The virtual calls are also replaced to match the parameter types *)
let specialize_types callee_pdesc resolved_pname args =
  let callee_attributes = Procdesc.get_attributes callee_pdesc in
  let resolved_params, substitutions =
    List.fold2_exn
      ~f:(fun (params, subts) (param_name, param_typ) (_, arg_typ) ->
        match arg_typ.Typ.desc with
        | Tptr ({desc= Tstruct typename}, Pk_pointer) ->
            (* Replace the type of the parameter by the type of the argument *)
            ((param_name, arg_typ) :: params, Mangled.Map.add param_name typename subts)
        | _ ->
            ((param_name, param_typ) :: params, subts))
      ~init:([], Mangled.Map.empty) callee_attributes.formals args
  in
  let resolved_attributes =
    { callee_attributes with
      formals= List.rev resolved_params
    ; proc_name= resolved_pname
    ; is_specialized= true
    ; err_log= Errlog.empty () }
  in
  Attributes.store resolved_attributes ;
  let resolved_pdesc =
    let tmp_cfg = create_cfg () in
    create_proc_desc tmp_cfg resolved_attributes
  in
  specialize_types_proc callee_pdesc resolved_pdesc substitutions


let specialize_with_block_args_instrs resolved_pdesc substitutions =
  let resolved_pname = Procdesc.get_proc_name resolved_pdesc in
  let convert_pvar pvar = Pvar.mk (Pvar.get_name pvar) resolved_pname in
  let convert_exp exp =
    match exp with
    | Exp.Lvar origin_pvar ->
        let new_pvar = convert_pvar origin_pvar in
        Exp.Lvar new_pvar
    | _ ->
        exp
  in
  let convert_instr (instrs, id_map) instr =
    let convert_generic_call return_ids exp origin_args loc call_flags =
      let converted_args = List.map ~f:(fun (exp, typ) -> (convert_exp exp, typ)) origin_args in
      let call_instr = Sil.Call (return_ids, exp, converted_args, loc, call_flags) in
      (call_instr :: instrs, id_map)
    in
    match instr with
    | Sil.Load (id, Exp.Lvar block_param, _, _)
      when Mangled.Map.mem (Pvar.get_name block_param) substitutions ->
        let id_map = Ident.IdentMap.add id (Pvar.get_name block_param) id_map in
        (* we don't need the load the block param instruction anymore *)
        (instrs, id_map)
    | Sil.Load (id, origin_exp, origin_typ, loc) ->
        (Sil.Load (id, convert_exp origin_exp, origin_typ, loc) :: instrs, id_map)
    | Sil.Store (assignee_exp, origin_typ, origin_exp, loc) ->
        let set_instr =
          Sil.Store (convert_exp assignee_exp, origin_typ, convert_exp origin_exp, loc)
        in
        (set_instr :: instrs, id_map)
    | Sil.Call (return_ids, Exp.Var id, origin_args, loc, call_flags) -> (
      try
        let block_name, extra_formals =
          let block_var = Ident.IdentMap.find id id_map in
          Mangled.Map.find block_var substitutions
        in
        (* once we find the block in the map, it means that we need to subsitute it with the
        call to the concrete block, and pass the fresh formals as arguments *)
        let ids_typs, load_instrs =
          let captured_ids_instrs =
            List.map extra_formals ~f:(fun (var, typ) ->
                let id = Ident.create_fresh Ident.knormal in
                let pvar = Pvar.mk var resolved_pname in
                ((id, typ), Sil.Load (id, Exp.Lvar pvar, typ, loc)) )
          in
          List.unzip captured_ids_instrs
        in
        let call_instr =
          let id_exps = List.map ~f:(fun (id, typ) -> (Exp.Var id, typ)) ids_typs in
          let converted_args =
            List.map ~f:(fun (exp, typ) -> (convert_exp exp, typ)) origin_args
          in
          Sil.Call
            ( return_ids
            , Exp.Const (Const.Cfun block_name)
            , id_exps @ converted_args
            , loc
            , call_flags )
        in
        let remove_temps_instrs =
          let ids = List.map ~f:(fun (id, _) -> id) ids_typs in
          Sil.Remove_temps (ids, loc)
        in
        let instrs = remove_temps_instrs :: call_instr :: load_instrs @ instrs in
        (instrs, id_map)
      with Not_found -> convert_generic_call return_ids (Exp.Var id) origin_args loc call_flags )
    | Sil.Call (return_ids, origin_call_exp, origin_args, loc, call_flags) ->
        convert_generic_call return_ids origin_call_exp origin_args loc call_flags
    | Sil.Prune (origin_exp, loc, is_true_branch, if_kind) ->
        (Sil.Prune (convert_exp origin_exp, loc, is_true_branch, if_kind) :: instrs, id_map)
    | Sil.Declare_locals (typed_vars, loc) ->
        let new_typed_vars =
          List.map ~f:(fun (pvar, typ) -> (convert_pvar pvar, typ)) typed_vars
        in
        (Sil.Declare_locals (new_typed_vars, loc) :: instrs, id_map)
    | Sil.Nullify _ | Abstract _ | Sil.Remove_temps _ ->
        (* these are generated instructions that will be replaced by the preanalysis *)
        (instrs, id_map)
  in
  let convert_instr_list instrs =
    let instrs, _ = List.fold ~f:convert_instr ~init:([], Ident.IdentMap.empty) instrs in
    List.rev instrs
  in
  convert_instr_list


let specialize_with_block_args callee_pdesc pname_with_block_args block_args =
  let callee_attributes = Procdesc.get_attributes callee_pdesc in
  (* Substitution from a block parameter to the block name and the new formals
  that correspond to the captured variables *)
  let substitutions : (Typ.Procname.t * (Mangled.t * Typ.t) list) Mangled.Map.t =
    List.fold2_exn callee_attributes.formals block_args ~init:Mangled.Map.empty ~f:
      (fun subts (param_name, _) block_arg_opt ->
        match block_arg_opt with
        | Some (cl: Exp.closure) ->
            let formals_from_captured =
              List.map
                ~f:(fun (_, var, typ) ->
                  (* Here we create fresh names for the new formals, based on the names of the captured
                   variables annotated with the name of the caller method *)
                  (Pvar.get_name_of_local_with_procname var, typ))
                cl.captured_vars
            in
            Mangled.Map.add param_name (cl.name, formals_from_captured) subts
        | None ->
            subts )
  in
  (* Extend formals with fresh variables for the captured variables of the block arguments,
    without duplications. *)
  let new_formals_blocks_captured_vars, extended_formals_annots =
    let new_formals_blocks_captured_vars_with_annots =
      let formals_annots =
        List.zip_exn callee_attributes.formals (snd callee_attributes.method_annotation)
      in
      let append_no_duplicates_formals_and_annot list1 list2 =
        IList.append_no_duplicates
          (fun ((name1, _), _) ((name2, _), _) -> Mangled.equal name1 name2)
          list1 list2
      in
      List.fold formals_annots ~init:[] ~f:(fun acc ((param_name, typ), annot) ->
          try
            let _, captured = Mangled.Map.find param_name substitutions in
            append_no_duplicates_formals_and_annot acc
              (List.map captured ~f:(fun captured_var -> (captured_var, Annot.Item.empty)))
          with Not_found -> append_no_duplicates_formals_and_annot acc [((param_name, typ), annot)]
      )
    in
    List.unzip new_formals_blocks_captured_vars_with_annots
  in
  let source_file_captured =
    let pname = Procdesc.get_proc_name callee_pdesc in
    match Attributes.find_file_capturing_procedure pname with
    | Some (source_file, _) ->
        source_file
    | None ->
        Logging.die InternalError
          "specialize_with_block_args ahould only be called with defined procedures, but we cannot find the captured file of procname %a"
          Typ.Procname.pp pname
  in
  let resolved_attributes =
    { callee_attributes with
      proc_name= pname_with_block_args
    ; is_defined= true
    ; err_log= Errlog.empty ()
    ; formals= new_formals_blocks_captured_vars
    ; method_annotation= (fst callee_attributes.method_annotation, extended_formals_annots)
    ; source_file_captured }
  in
  Attributes.store resolved_attributes ;
  let resolved_pdesc =
    let tmp_cfg = create_cfg () in
    create_proc_desc tmp_cfg resolved_attributes
  in
  Logging.(debug Analysis Verbose)
    "signature of base method %a@." Procdesc.pp_signature callee_pdesc ;
  Logging.(debug Analysis Verbose)
    "signature of specialized method %a@." Procdesc.pp_signature resolved_pdesc ;
  convert_cfg ~callee_pdesc ~resolved_pdesc
    (specialize_with_block_args_instrs resolved_pdesc substitutions)


let pp_proc_signatures fmt cfg =
  F.fprintf fmt "METHOD SIGNATURES@\n@." ;
  let sorted_procs = List.sort ~cmp:Procdesc.compare (get_all_procs cfg) in
  List.iter ~f:(fun pdesc -> F.fprintf fmt "%a@." Procdesc.pp_signature pdesc) sorted_procs


let exists_for_source_file source =
  (* simplistic implementation that allocates the cfg as this is only used for reactive capture for now *)
  load source |> Option.is_some