From c8b87ed0c887bbfffada8fcb50b251838831b243 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Thu, 31 Mar 2016 12:17:33 -0700 Subject: [PATCH] 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 | 22 +++++++++++----------- infer/src/checkers/addressTaken.ml | 2 +- infer/src/checkers/copyPropagation.ml | 2 +- infer/src/checkers/summary.ml | 15 ++++++--------- infer/src/checkers/transferFunctions.ml | 4 ++-- infer/src/unit/abstractInterpreterTests.ml | 2 +- 6 files changed, 22 insertions(+), 25 deletions(-) diff --git a/infer/src/checkers/abstractInterpreter.ml b/infer/src/checkers/abstractInterpreter.ml index dcf1e9e41..708729575 100644 --- a/infer/src/checkers/abstractInterpreter.ml +++ b/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 -> diff --git a/infer/src/checkers/addressTaken.ml b/infer/src/checkers/addressTaken.ml index 9265fc0a4..3c094b732 100644 --- a/infer/src/checkers/addressTaken.ml +++ b/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, _, _) -> diff --git a/infer/src/checkers/copyPropagation.ml b/infer/src/checkers/copyPropagation.ml index 7758391f3..6796e4559 100644 --- a/infer/src/checkers/copyPropagation.ml +++ b/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 diff --git a/infer/src/checkers/summary.ml b/infer/src/checkers/summary.ml index ee2d25425..35bbfedca 100644 --- a/infer/src/checkers/summary.ml +++ b/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 diff --git a/infer/src/checkers/transferFunctions.ml b/infer/src/checkers/transferFunctions.ml index 97ec1a711..dadf57318 100644 --- a/infer/src/checkers/transferFunctions.ml +++ b/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 diff --git a/infer/src/unit/abstractInterpreterTests.ml b/infer/src/unit/abstractInterpreterTests.ml index bc7ed5bf5..836e839f1 100644 --- a/infer/src/unit/abstractInterpreterTests.ml +++ b/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