passing caller pdesc into the transfer functions

Summary:public It's useful for the transfer functions to understand what the current procedure is. Applications include debugging, implementing context-sensitivity, asking which program variables are parameters, and the list goes on.

In the future, we'll almost certainly want to pass the tenv to the transfer functions as well.

Reviewed By: jberdine

Differential Revision: D3104997

fb-gh-sync-id: 1c0df8f
fbshipit-source-id: 1c0df8f

infer/src/checkers/abstractInterpreter.ml

@@ -25,11 +25,11 @@ module Make
   (* invariant map from node id -> abstract state representing postcondition for node id *)
   type inv_map = state M.t
 
-  let exec_node node astate_pre work_queue inv_map =
+  let exec_node node astate_pre work_queue inv_map pdesc =
     let exec_instrs astate_acc instr =
       if A.is_bottom astate_acc
       then astate_acc
-      else T.exec_instr astate_acc instr in
+      else T.exec_instr astate_acc pdesc instr in
     let node_id = C.node_id node in
     L.out "Doing analysis of node %a from pre %a@." C.pp_node_id node_id A.pp astate_pre;
     let instrs = C.instrs node in
@@ -62,10 +62,10 @@ module Make
         M.add node_id { post=astate_post; visit_count; } inv_map in
       inv_map', S.schedule_succs work_queue node
 
-  let rec exec_worklist work_queue inv_map =
+  let rec exec_worklist work_queue inv_map pdesc =
     match S.pop work_queue with
     | Some (_, [], work_queue') ->
-        exec_worklist work_queue' inv_map
+        exec_worklist work_queue' inv_map pdesc
     | Some (node, visited_pred :: visited_preds, work_queue') ->
         let get_post pred_id =
           (M.find pred_id inv_map).post in
@@ -73,25 +73,25 @@ module Make
         let join_pred_posts astate_acc pred_id =
           A.join (get_post pred_id) astate_acc in
         let astate_pre = IList.fold_left join_pred_posts (get_post visited_pred) visited_preds in
-        let inv_map', work_queue'' = exec_node node astate_pre work_queue' inv_map in
-        exec_worklist work_queue'' inv_map'
+        let inv_map', work_queue'' = exec_node node astate_pre work_queue' inv_map pdesc in
+        exec_worklist work_queue'' inv_map' pdesc
     | None -> inv_map
 
   (* compute and return an invariant map for [cfg] *)
-  let exec_cfg cfg =
+  let exec_cfg cfg pdesc =
     let start_node = C.start_node cfg in
-    let inv_map', work_queue' = exec_node start_node A.initial (S.empty cfg) M.empty in
-    exec_worklist work_queue' inv_map'
+    let inv_map', work_queue' = exec_node start_node A.initial (S.empty cfg) M.empty pdesc in
+    exec_worklist work_queue' inv_map' pdesc
 
   (* compute and return an invariant map for [pdesc] *)
   let exec_pdesc pdesc =
     L.out "Starting analysis of %a@." Procname.pp (Cfg.Procdesc.get_proc_name pdesc);
-    exec_cfg (C.from_pdesc pdesc)
+    exec_cfg (C.from_pdesc pdesc) pdesc
 
   (* compute and return the postcondition of [pdesc] *)
   let compute_post pdesc =
     let cfg = C.from_pdesc pdesc in
-    let inv_map = exec_cfg cfg in
+    let inv_map = exec_cfg cfg pdesc in
     let end_state =
       try M.find (C.node_id (C.exit_node cfg)) inv_map
       with Not_found ->

infer/src/checkers/addressTaken.ml

@@ -31,7 +31,7 @@ module TransferFunctions = struct
     | Var _ | Sizeof _ ->
         astate
 
-  let exec_instr astate = function
+  let exec_instr astate _ = function
     | Sil.Set (_, Tptr _, rhs_exp, _) ->
         add_address_taken_pvars rhs_exp astate
     | Sil.Call (_, _, actuals, _, _) ->

infer/src/checkers/copyPropagation.ml

@@ -100,7 +100,7 @@ module TransferFunctions = struct
 
   type astate = Domain.astate
 
-  let exec_instr astate = function
+  let exec_instr astate _ = function
     | Sil.Letderef (lhs_id, Sil.Var rhs_id, _, _) ->
         (* note: logical vars are SSA, don't need to worry about overwriting existing bindings *)
         Domain.gen (LogicalVar lhs_id) (LogicalVar rhs_id) astate

infer/src/checkers/summary.ml

@@ -21,8 +21,9 @@ module type S = sig
 
   (* write the summary for [name] to persistent storage *)
   val write_summary : Procname.t -> summary -> unit
-  (* read and return the summary for [pname]. does the analysis to create the summary if needed *)
-  val read_summary : Procname.t -> summary option
+  (* read and return the summary for [callee_pname] called from [caller_pdesc]. does the analysis to
+     create the summary if needed *)
+  val read_summary : Cfg.Procdesc.t -> Procname.t -> summary option
 end
 
 module Make (H : Helper) = struct
@@ -37,13 +38,9 @@ module Make (H : Helper) = struct
         Printf.sprintf "Summary for %s should exist, but does not!@." (Procname.to_string pname)
         |> failwith
 
-  let read_summary pname =
-    (* this is reprehensible. but the caller_pdesc is only used for debug printing *)
-    (* TODO: fix the ondemand API so we can choose to pass a pdesc option *)
-    let dummy_caller_pdesc =
-      Cfg.Procdesc.create (Cfg.Node.create_cfg ()) (ProcAttributes.default pname Config.Java) in
-    Ondemand.analyze_proc_name ~propagate_exceptions:false dummy_caller_pdesc pname;
-    match Specs.get_summary pname with
+  let read_summary caller_pdesc callee_pname =
+    Ondemand.analyze_proc_name ~propagate_exceptions:false caller_pdesc callee_pname;
+    match Specs.get_summary callee_pname with
     | None -> None
     | Some summary -> Some (H.read_from_payload summary.Specs.payload)
 end

infer/src/checkers/transferFunctions.ml

@@ -11,7 +11,7 @@
 module type TransferFunctions = sig
   type astate
 
-  (* {A} instr {A'} *)
-  val exec_instr : astate -> Sil.instr -> astate
+  (* {A} instr {A'}. [caller_pdesc] is the procdesc of the current procedure *)
+  val exec_instr : astate -> Cfg.Procdesc.t -> Sil.instr -> astate
 
 end

infer/src/unit/abstractInterpreterTests.ml

@@ -50,7 +50,7 @@ module PathCountTransferFunctions = struct
   type astate = PathCountDomain.astate
 
   (* just propagate the current path count *)
-  let exec_instr astate _ = astate
+  let exec_instr astate _ _ = astate
 end