From e54db73bab98a837ddccbe5ffeb289fba820d03e Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Fri, 8 Apr 2016 13:47:11 -0700 Subject: [PATCH] pass tenv to the transfer functions Reviewed By: cristianoc Differential Revision: D3153716 fb-gh-sync-id: 855fc41 fbshipit-source-id: 855fc41 --- infer/src/backend/preanal.ml | 6 ++--- infer/src/checkers/abstractInterpreter.ml | 30 +++++++++++------------ infer/src/checkers/copyPropagation.ml | 3 ++- infer/src/checkers/liveness.ml | 3 ++- infer/src/checkers/procData.ml | 12 +++++++++ infer/src/checkers/transferFunctions.ml | 2 +- infer/src/unit/analyzerTester.ml | 2 +- 7 files changed, 36 insertions(+), 22 deletions(-) create mode 100644 infer/src/checkers/procData.ml diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index e2465f32f..3a7e8cdf8 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -281,7 +281,7 @@ let add_dead_pvars_after_conditionals_join cfg n deads = (** Find the set of dead variables for the procedure pname and add nullify instructions. The variables whose addresses may be taken are only considered just before the exit node. *) -let analyze_and_annotate_proc cfg pname pdesc = +let analyze_and_annotate_proc cfg tenv pname pdesc = let exit_node = Cfg.Procdesc.get_exit_node pdesc in let exit_node_is_succ node = match Cfg.Node.get_succs node with @@ -293,7 +293,7 @@ let analyze_and_annotate_proc cfg pname pdesc = if !Config.curr_language = Config.Java then Vset.empty else - match AddressTaken.Analyzer.compute_post pdesc with + match AddressTaken.Analyzer.compute_post (ProcData.make pdesc tenv) with | Some post -> post | None -> Vset.empty in @@ -445,7 +445,7 @@ let add_removetemps_instructions cfg = let doit ?(f_translate_typ=None) cfg cg tenv = add_removetemps_instructions cfg; AllPreds.mk_table cfg; - Cfg.iter_proc_desc cfg (analyze_and_annotate_proc cfg); + Cfg.iter_proc_desc cfg (analyze_and_annotate_proc cfg tenv); AllPreds.clear_table (); if !Config.curr_language = Config.Java then add_dispatch_calls cfg cg tenv f_translate_typ; diff --git a/infer/src/checkers/abstractInterpreter.ml b/infer/src/checkers/abstractInterpreter.ml index cad0305a0..69d64c34e 100644 --- a/infer/src/checkers/abstractInterpreter.ml +++ b/infer/src/checkers/abstractInterpreter.ml @@ -22,11 +22,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 pdesc = + let exec_node node astate_pre work_queue inv_map proc_data = let exec_instrs astate_acc instr = if A.is_bottom astate_acc then astate_acc - else T.exec_instr astate_acc pdesc instr in + else T.exec_instr astate_acc proc_data 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 @@ -59,10 +59,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 pdesc = + let rec exec_worklist work_queue inv_map proc_data = match S.pop work_queue with | Some (_, [], work_queue') -> - exec_worklist work_queue' inv_map pdesc + exec_worklist work_queue' inv_map proc_data | Some (node, visited_pred :: visited_preds, work_queue') -> let get_post pred_id = (M.find pred_id inv_map).post in @@ -70,25 +70,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 pdesc in - exec_worklist work_queue'' inv_map' pdesc + let inv_map', work_queue'' = exec_node node astate_pre work_queue' inv_map proc_data in + exec_worklist work_queue'' inv_map' proc_data | None -> inv_map (* compute and return an invariant map for [cfg] *) - let exec_cfg cfg pdesc = + let exec_cfg cfg proc_data = let start_node = C.start_node cfg in - 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 + let inv_map', work_queue' = exec_node start_node A.initial (S.empty cfg) M.empty proc_data in + exec_worklist work_queue' inv_map' proc_data (* compute and return an invariant map for [pdesc] *) - let exec_pdesc pdesc = + let exec_pdesc ({ ProcData.pdesc; } as proc_data) = L.out "Starting analysis of %a@." Procname.pp (Cfg.Procdesc.get_proc_name pdesc); - exec_cfg (C.from_pdesc pdesc) pdesc + exec_cfg (C.from_pdesc pdesc) proc_data (* compute and return the postcondition of [pdesc] *) - let compute_post pdesc = + let compute_post ({ ProcData.pdesc; } as proc_data) = let cfg = C.from_pdesc pdesc in - let inv_map = exec_cfg cfg pdesc in + let inv_map = exec_cfg cfg proc_data in try let end_state = M.find (C.node_id (C.exit_node cfg)) inv_map in Some (end_state.post) @@ -102,9 +102,9 @@ module Make module Interprocedural (Summ : Summary.S with type summary = A.astate) = struct - let checker { Callbacks.get_proc_desc; proc_desc; proc_name; } = + let checker { Callbacks.get_proc_desc; proc_desc; proc_name; tenv; } = let analyze_ondemand pdesc = - match compute_post pdesc with + match compute_post (ProcData.make pdesc tenv) with | Some post -> Summ.write_summary (Cfg.Procdesc.get_proc_name pdesc) post | None -> () in diff --git a/infer/src/checkers/copyPropagation.ml b/infer/src/checkers/copyPropagation.ml index 9523e9c19..99f925f0e 100644 --- a/infer/src/checkers/copyPropagation.ml +++ b/infer/src/checkers/copyPropagation.ml @@ -118,4 +118,5 @@ module Analyzer = (Domain) (TransferFunctions) -let checker { Callbacks.proc_desc; } = ignore(Analyzer.exec_pdesc proc_desc) +let checker { Callbacks.proc_desc; tenv; } = + ignore(Analyzer.exec_pdesc (ProcData.make proc_desc tenv)) diff --git a/infer/src/checkers/liveness.ml b/infer/src/checkers/liveness.ml index c561e0251..712718270 100644 --- a/infer/src/checkers/liveness.ml +++ b/infer/src/checkers/liveness.ml @@ -64,4 +64,5 @@ module Analyzer = (Domain) (TransferFunctions) -let checker { Callbacks.proc_desc; } = ignore(Analyzer.exec_pdesc proc_desc) +let checker { Callbacks.proc_desc; tenv; } = + ignore(Analyzer.exec_pdesc (ProcData.make proc_desc tenv)) diff --git a/infer/src/checkers/procData.ml b/infer/src/checkers/procData.ml new file mode 100644 index 000000000..53a834003 --- /dev/null +++ b/infer/src/checkers/procData.ml @@ -0,0 +1,12 @@ +(* + * Copyright (c) 2016 - 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. + *) + +type t = { pdesc : Cfg.Procdesc.t; tenv : Tenv.t } + +let make pdesc tenv = { pdesc; tenv } diff --git a/infer/src/checkers/transferFunctions.ml b/infer/src/checkers/transferFunctions.ml index c22021b62..0627081ff 100644 --- a/infer/src/checkers/transferFunctions.ml +++ b/infer/src/checkers/transferFunctions.ml @@ -12,6 +12,6 @@ module type S = sig type astate (* {A} instr {A'}. [caller_pdesc] is the procdesc of the current procedure *) - val exec_instr : astate -> Cfg.Procdesc.t -> Sil.instr -> astate + val exec_instr : astate -> ProcData.t -> Sil.instr -> astate end diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index 26d0f9363..97f6bf0e5 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -200,7 +200,7 @@ module Make let create_test test_program _ = let pdesc, assert_map = structured_program_to_cfg test_program in - let inv_map = I.exec_pdesc pdesc in + let inv_map = I.exec_pdesc (ProcData.make pdesc (Tenv.create ())) in let collect_invariant_mismatches node_id (inv_str, inv_label) error_msgs_acc = let post_str =