[inferbo] Move get_formals from Domain to Procdesc

Reviewed By: jvillard

Differential Revision: D13449590

fbshipit-source-id: da435606a

infer/src/IR/Procdesc.ml

@@ -448,9 +448,16 @@ let set_attributes pdesc attributes = pdesc.attributes <- attributes
 
 let get_exit_node pdesc = pdesc.exit_node
 
+let get_proc_name pdesc = pdesc.attributes.proc_name
+
 (** Return name and type of formal parameters *)
 let get_formals pdesc = pdesc.attributes.formals
 
+let get_pvar_formals pdesc =
+  let proc_name = get_proc_name pdesc in
+  get_formals pdesc |> List.map ~f:(fun (name, typ) -> (Pvar.mk name proc_name, typ))
+
+
 let get_loc pdesc = pdesc.attributes.loc
 
 (** Return name and type of local variables *)
@@ -468,8 +475,6 @@ let get_nodes pdesc = pdesc.nodes
 
 let get_nodes_num pdesc = pdesc.nodes_num
 
-let get_proc_name pdesc = pdesc.attributes.proc_name
-
 (** Return the return type of the procedure *)
 let get_ret_type pdesc = pdesc.attributes.ret_type
 

infer/src/IR/Procdesc.mli

@@ -219,6 +219,9 @@ val get_exit_node : t -> Node.t
 val get_formals : t -> (Mangled.t * Typ.t) list
 (** Return name and type of formal parameters *)
 
+val get_pvar_formals : t -> (Pvar.t * Typ.t) list
+(** Return pvar and type of formal parameters *)
+
 val get_loc : t -> Location.t
 (** Return loc information for the procedure *)
 

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -75,7 +75,7 @@ module TransferFunctions = struct
 
   let instantiate_mem_reachable (ret_id, _) callee_pdesc callee_pname ~callee_exit_mem
       ({Dom.eval_locpath} as eval_sym_trace) mem location =
-    let formals = Dom.get_formals callee_pdesc in
+    let formals = Procdesc.get_pvar_formals callee_pdesc in
     let copy_reachable_locs_from locs mem =
       let copy loc acc =
         Option.value_map (Dom.Mem.find_opt loc callee_exit_mem) ~default:acc ~f:(fun v ->
@@ -207,7 +207,7 @@ module TransferFunctions = struct
                 let pname = Procdesc.get_proc_name pdesc in
                 match Typ.Procname.get_method pname with
                 | "__inferbo_empty" when Loc.is_return loc_v -> (
-                  match Dom.get_formals pdesc with
+                  match Procdesc.get_pvar_formals pdesc with
                   | [(formal, _)] ->
                       let formal_v = Dom.Mem.find (Loc.of_pvar formal) mem in
                       Dom.Mem.store_empty_alias formal_v loc_v mem

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -22,13 +22,9 @@ type eval_sym_trace =
   ; trace_of_sym: Symb.Symbol.t -> Trace.Set.t
   ; eval_locpath: PowLoc.eval_locpath }
 
-let get_formals : Procdesc.t -> (Pvar.t * Typ.t) list =
- fun pdesc ->
-  let proc_name = Procdesc.get_proc_name pdesc in
-  Procdesc.get_formals pdesc |> List.map ~f:(fun (name, typ) -> (Pvar.mk name proc_name, typ))
-
-
 module OndemandEnv = struct
+  module FormalTyps = Caml.Map.Make (Pvar)
+
   type t =
     { typ_of_param_path: SPath.partial -> Typ.t option
     ; may_last_field: SPath.partial -> bool
@@ -36,10 +32,9 @@ module OndemandEnv = struct
     ; integer_type_widths: Typ.IntegerWidths.t }
 
   let mk pdesc =
-    let module FormalTyps = Caml.Map.Make (Pvar) in
     let formal_typs =
-      List.fold (get_formals pdesc) ~init:FormalTyps.empty ~f:(fun acc (formal, typ) ->
-          FormalTyps.add formal typ acc )
+      List.fold (Procdesc.get_pvar_formals pdesc) ~init:FormalTyps.empty
+        ~f:(fun acc (formal, typ) -> FormalTyps.add formal typ acc )
     in
     fun tenv integer_type_widths ->
       let rec typ_of_param_path = function

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -393,7 +393,7 @@ let eval_sympath params sympath mem =
 
 let mk_eval_sym_trace integer_type_widths callee_pdesc actual_exps caller_mem =
   let params =
-    let formals = get_formals callee_pdesc in
+    let formals = Procdesc.get_pvar_formals callee_pdesc in
     let actuals = List.map ~f:(fun (a, _) -> eval integer_type_widths a caller_mem) actual_exps in
     ParamBindings.make formals actuals
   in
@@ -710,7 +710,7 @@ let get_subst_map :
     in
     List.rev_append new_rel_matching rel_l
   in
-  let formals = get_formals callee_pdesc in
+  let formals = Procdesc.get_pvar_formals callee_pdesc in
   let actuals =
     List.map ~f:(fun (a, _) -> (eval integer_type_widths a caller_mem, Some a)) params
   in

infer/src/checkers/reachingDefs.ml

@@ -59,7 +59,7 @@ end
 (* initialize formal parameters to have start node as reaching def *)
 let init_reaching_defs_with_formals pdesc =
   let start_node_defs = Defs.singleton (Procdesc.get_start_node pdesc) in
-  BufferOverrunDomain.get_formals pdesc
+  Procdesc.get_pvar_formals pdesc
   |> List.fold_left ~init:ReachingDefsMap.empty ~f:(fun acc (pvar, _) ->
          ReachingDefsMap.add (Var.of_pvar pvar) start_node_defs acc )