From 90a5a5912fcdfdc83eed8237ed890ae022736083 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Mon, 2 May 2016 18:20:22 -0700 Subject: [PATCH] allowing extra data to be packaged along with procCfg Reviewed By: jeremydubreil Differential Revision: D3234490 fb-gh-sync-id: fefeafb fbshipit-source-id: fefeafb --- infer/src/backend/preanal.ml | 2 +- infer/src/checkers/abstractInterpreter.ml | 4 ++-- infer/src/checkers/addressTaken.ml | 1 + infer/src/checkers/annotationReachability.ml | 3 ++- infer/src/checkers/copyPropagation.ml | 4 ++-- infer/src/checkers/liveness.ml | 3 ++- infer/src/checkers/procData.ml | 12 ++++++++++-- infer/src/checkers/procData.mli | 18 ++++++++++++++++++ infer/src/checkers/transferFunctions.ml | 6 +++--- infer/src/unit/abstractInterpreterTests.ml | 1 + infer/src/unit/analyzerTester.ml | 5 +++-- 11 files changed, 45 insertions(+), 14 deletions(-) create mode 100644 infer/src/checkers/procData.mli diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index 142ff1ef2..a8eb70634 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -293,7 +293,7 @@ let analyze_and_annotate_proc cfg tenv pname pdesc = if !Config.curr_language = Config.Java then Vset.empty else - match AddressTaken.Analyzer.compute_post (ProcData.make pdesc tenv) with + match AddressTaken.Analyzer.compute_post (ProcData.make_default pdesc tenv) with | Some post -> post | None -> Vset.empty in diff --git a/infer/src/checkers/abstractInterpreter.ml b/infer/src/checkers/abstractInterpreter.ml index a93870a15..71c4b3b11 100644 --- a/infer/src/checkers/abstractInterpreter.ml +++ b/infer/src/checkers/abstractInterpreter.ml @@ -119,10 +119,10 @@ module Make module Interprocedural (Summ : Summary.S with type summary = A.astate) = struct - let checker { Callbacks.get_proc_desc; proc_desc; proc_name; tenv; } = + let checker { Callbacks.get_proc_desc; proc_desc; proc_name; tenv; } extras = let post_opt = ref None in let analyze_ondemand pdesc = - match compute_post (ProcData.make pdesc tenv) with + match compute_post (ProcData.make pdesc tenv extras) with | Some post -> Summ.write_summary (Cfg.Procdesc.get_proc_name pdesc) post; post_opt := Some post diff --git a/infer/src/checkers/addressTaken.ml b/infer/src/checkers/addressTaken.ml index 0cf7ba8a6..53b1b42e1 100644 --- a/infer/src/checkers/addressTaken.ml +++ b/infer/src/checkers/addressTaken.ml @@ -19,6 +19,7 @@ module Domain = AbstractDomain.FiniteSet(PvarSet) module TransferFunctions = struct type astate = Domain.astate + type extras = ProcData.no_extras let rec add_address_taken_pvars exp astate = match exp with | Sil.Lvar pvar -> diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml index 325089e62..369edac38 100644 --- a/infer/src/checkers/annotationReachability.ml +++ b/infer/src/checkers/annotationReachability.ml @@ -303,6 +303,7 @@ let report_allocations pname loc calls = module TransferFunctions = struct type astate = Domain.astate + type extras = ProcData.no_extras (* This is specific to the @NoAllocation and @PerformanceCritical checker and the "unlikely" method is used to guard branches that are expected to run sufficiently @@ -398,7 +399,7 @@ module Interprocedural = struct PatternMatch.proc_iter_overridden_methods check_expensive_subtyping_rules tenv proc_name; - match checker proc_data with + match checker proc_data ProcData.empty_extras with | Some astate -> begin match astate with diff --git a/infer/src/checkers/copyPropagation.ml b/infer/src/checkers/copyPropagation.ml index a501b8bf0..fd61b0237 100644 --- a/infer/src/checkers/copyPropagation.ml +++ b/infer/src/checkers/copyPropagation.ml @@ -80,8 +80,8 @@ module Domain = struct end module TransferFunctions = struct - type astate = Domain.astate + type extras = ProcData.no_extras let exec_instr astate _ = function | Sil.Letderef (lhs_id, Sil.Var rhs_id, _, _) -> @@ -127,4 +127,4 @@ module Analyzer = (TransferFunctions) let checker { Callbacks.proc_desc; tenv; } = - ignore(Analyzer.exec_pdesc (ProcData.make proc_desc tenv)) + ignore(Analyzer.exec_pdesc (ProcData.make_default proc_desc tenv)) diff --git a/infer/src/checkers/liveness.ml b/infer/src/checkers/liveness.ml index 5fe1f0913..e4d62c792 100644 --- a/infer/src/checkers/liveness.ml +++ b/infer/src/checkers/liveness.ml @@ -20,6 +20,7 @@ module Domain = AbstractDomain.FiniteSet(Var.Set) read, kill the variable when it is assigned *) module TransferFunctions = struct type astate = Domain.astate + type extras = ProcData.no_extras (* add all of the vars read in [exp] to the live set *) let exp_add_live exp astate = @@ -67,4 +68,4 @@ module Analyzer = (TransferFunctions) let checker { Callbacks.proc_desc; tenv; } = - ignore(Analyzer.exec_pdesc (ProcData.make proc_desc tenv)) + ignore(Analyzer.exec_pdesc (ProcData.make_default proc_desc tenv)) diff --git a/infer/src/checkers/procData.ml b/infer/src/checkers/procData.ml index 288a32732..56352c9d6 100644 --- a/infer/src/checkers/procData.ml +++ b/infer/src/checkers/procData.ml @@ -9,6 +9,14 @@ open! Utils -type t = { pdesc : Cfg.Procdesc.t; tenv : Tenv.t } +type 'a t = { pdesc : Cfg.Procdesc.t; tenv : Tenv.t; extras : 'a; } -let make pdesc tenv = { pdesc; tenv } +type no_extras = unit + +let empty_extras = () + +let make pdesc tenv extras = + { pdesc; tenv; extras; } + +let make_default pdesc tenv = + make pdesc tenv empty_extras diff --git a/infer/src/checkers/procData.mli b/infer/src/checkers/procData.mli new file mode 100644 index 000000000..34bff92e3 --- /dev/null +++ b/infer/src/checkers/procData.mli @@ -0,0 +1,18 @@ +(* + * 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 'a t = { pdesc : Cfg.Procdesc.t; tenv : Tenv.t; extras : 'a; } + +type no_extras + +val empty_extras : no_extras + +val make : Cfg.Procdesc.t -> Tenv.t -> 'a -> 'a t + +val make_default : Cfg.Procdesc.t -> Tenv.t -> no_extras t diff --git a/infer/src/checkers/transferFunctions.ml b/infer/src/checkers/transferFunctions.ml index cb3b81975..8f13a96f2 100644 --- a/infer/src/checkers/transferFunctions.ml +++ b/infer/src/checkers/transferFunctions.ml @@ -11,9 +11,9 @@ open! Utils module type S = sig - type astate + type astate (* abstract state to propagate *) + type extras (* read-only extra state (results of previous analyses, globals, etc.) *) (* {A} instr {A'}. [caller_pdesc] is the procdesc of the current procedure *) - val exec_instr : astate -> ProcData.t -> Sil.instr -> astate - + val exec_instr : astate -> extras ProcData.t -> Sil.instr -> astate end diff --git a/infer/src/unit/abstractInterpreterTests.ml b/infer/src/unit/abstractInterpreterTests.ml index 230ed69a6..7037d9f1b 100644 --- a/infer/src/unit/abstractInterpreterTests.ml +++ b/infer/src/unit/abstractInterpreterTests.ml @@ -50,6 +50,7 @@ end module PathCountTransferFunctions = struct type astate = PathCountDomain.astate + type extras = ProcData.no_extras (* just propagate the current path count *) let exec_instr astate _ _ = astate diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index 22c2625d7..376b992a3 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -136,7 +136,8 @@ module Make (C : ProcCfg.Wrapper with type node = Cfg.Node.t) (S : Scheduler.S) (A : AbstractDomain.S) - (T : TransferFunctions.S with type astate = A.astate) = struct + (T : TransferFunctions.S + with type astate = A.astate and type extras = ProcData.no_extras) = struct open StructuredSil @@ -225,7 +226,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 (ProcData.make pdesc (Tenv.create ())) in + let inv_map = I.exec_pdesc (ProcData.make_default pdesc (Tenv.create ())) in let collect_invariant_mismatches node_id (inv_str, inv_label) error_msgs_acc = let post_str =