From 2add2954daf28cfabd98b6a8873d703216e83d28 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Wed, 11 Jan 2017 13:54:45 -0800 Subject: [PATCH] [checkers] factor out FormalMap into its own module Summary: This will be useful in upcoming changes to the thread-safety analysis as well. Reviewed By: dkgi Differential Revision: D4402146 fbshipit-source-id: c750127 --- infer/src/checkers/FormalMap.ml | 37 +++++++++++++++++++++ infer/src/checkers/FormalMap.mli | 28 ++++++++++++++++ infer/src/quandary/TaintAnalysis.ml | 51 +++++++++-------------------- infer/src/unit/TaintTests.ml | 2 +- 4 files changed, 82 insertions(+), 36 deletions(-) create mode 100644 infer/src/checkers/FormalMap.ml create mode 100644 infer/src/checkers/FormalMap.mli diff --git a/infer/src/checkers/FormalMap.ml b/infer/src/checkers/FormalMap.ml new file mode 100644 index 000000000..d63cf9f98 --- /dev/null +++ b/infer/src/checkers/FormalMap.ml @@ -0,0 +1,37 @@ +(* + * Copyright (c) 2017 - 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. + *) + +open! IStd + +module F = Format +module L = Logging + +type t = int AccessPath.BaseMap.t + +let make pdesc = + let pname = Procdesc.get_proc_name pdesc in + let attrs = Procdesc.get_attributes pdesc in + let formals_with_nums = + IList.mapi + (fun index (name, typ) -> + let pvar = Pvar.mk name pname in + AccessPath.base_of_pvar pvar typ, index) + attrs.ProcAttributes.formals in + IList.fold_left + (fun formal_map (base, index) -> AccessPath.BaseMap.add base index formal_map) + AccessPath.BaseMap.empty + formals_with_nums + +let empty = AccessPath.BaseMap.empty + +let is_formal = AccessPath.BaseMap.mem + +let get_formal_index base t = + try Some (AccessPath.BaseMap.find base t) + with Not_found -> None diff --git a/infer/src/checkers/FormalMap.mli b/infer/src/checkers/FormalMap.mli new file mode 100644 index 000000000..84e1cb61e --- /dev/null +++ b/infer/src/checkers/FormalMap.mli @@ -0,0 +1,28 @@ +(* + * Copyright (c) 2017 - 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. + *) + +open! IStd + +module F = Format +module L = Logging + +(** a map from a formal to its positional index *) +type t + +(** create a formal map for the given procdesc *) +val make : Procdesc.t -> t + +(** the empty formal map *) +val empty : t + +(** return true if the given base var is a formal according to the given formal map *) +val is_formal : AccessPath.base -> t -> bool + +(** return the index for the given base var if it is a formal, or None if it is not *) +val get_formal_index : AccessPath.base -> t -> int option diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index d1838d986..bb6e182dd 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -19,9 +19,6 @@ module Make (TaintSpecification : TaintSpec.S) = struct module TaintDomain = TaintSpecification.AccessTree module IdMapDomain = IdAccessPathMapDomain - (** a map from a formal to its position *) - type formal_map = int AccessPath.BaseMap.t - module Summary = Summary.Make(struct type summary = QuandarySummary.t @@ -88,14 +85,14 @@ module Make (TaintSpecification : TaintSpec.S) = struct module CFG = CFG module Domain = Domain - type extras = formal_map + type extras = FormalMap.t let resolve_id id_map id = try Some (IdMapDomain.find id id_map) with Not_found -> None (* get the node associated with [access_path] in [access_tree] *) - let access_path_get_node access_path access_tree (proc_data : formal_map ProcData.t) loc = + let access_path_get_node access_path access_tree (proc_data : FormalMap.t ProcData.t) loc = match TaintDomain.get_node access_path access_tree with | Some _ as node_opt -> node_opt @@ -108,13 +105,13 @@ module Make (TaintSpecification : TaintSpec.S) = struct (TraceDomain.Source.make_footprint footprint_ap call_site) in Some (TaintDomain.make_normal_leaf trace) in let root, _ = AccessPath.extract access_path in - try - let formal_index = AccessPath.BaseMap.find root proc_data.extras in - make_footprint_trace (make_footprint_access_path formal_index access_path) - with Not_found -> - if is_global root - then make_footprint_trace access_path - else None + match FormalMap.get_formal_index root proc_data.extras with + | Some formal_index -> + make_footprint_trace (make_footprint_access_path formal_index access_path) + | None -> + if is_global root + then make_footprint_trace access_path + else None (* get the trace associated with [access_path] in [access_tree]. *) let access_path_get_trace access_path access_tree proc_data loc = @@ -159,7 +156,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct TaintDomain.add_trace id_ap trace access_tree (** log any new reportable source-sink flows in [trace] *) - let report_trace trace cur_site (proc_data : formal_map ProcData.t) = + let report_trace trace cur_site (proc_data : FormalMap.t ProcData.t) = let trace_of_pname pname = match Summary.read_summary proc_data.pdesc pname with | Some summary -> @@ -315,7 +312,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct caller_access_tree in { astate_in with access_tree; } - let exec_instr (astate : Domain.astate) (proc_data : formal_map ProcData.t) _ instr = + let exec_instr (astate : Domain.astate) (proc_data : FormalMap.t ProcData.t) _ instr = let f_resolve_id = resolve_id astate.id_map in match instr with | Sil.Load (lhs_id, rhs_exp, rhs_typ, _) -> @@ -494,11 +491,9 @@ module Make (TaintSpecification : TaintSpec.S) = struct AccessPath.BaseMap.fold (fun base node acc -> let base' = - try - let formal_index = AccessPath.BaseMap.find base formal_map in - make_footprint_var formal_index, snd base - with Not_found -> - base in + match FormalMap.get_formal_index base formal_map with + | Some formal_index -> make_footprint_var formal_index, snd base + | None -> base in AccessPath.BaseMap.add base' node acc) access_tree TaintDomain.empty in @@ -526,7 +521,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct then Domain.empty else { Domain.empty with Domain.access_tree; } in - let compute_post (proc_data : formal_map ProcData.t) = + let compute_post (proc_data : FormalMap.t ProcData.t) = if not (Procdesc.did_preanalysis proc_data.pdesc) then begin @@ -541,20 +536,6 @@ module Make (TaintSpecification : TaintSpec.S) = struct if Procdesc.Node.get_succs (Procdesc.get_start_node proc_data.pdesc) <> [] then failwith "Couldn't compute post" else None in - - let make_extras pdesc = - let pname = Procdesc.get_proc_name pdesc in - let attrs = Procdesc.get_attributes pdesc in - let formals_with_nums = - IList.mapi - (fun index (name, typ) -> - let pvar = Pvar.mk name pname in - AccessPath.base_of_pvar pvar typ, index) - attrs.ProcAttributes.formals in - IList.fold_left - (fun formal_map (base, index) -> AccessPath.BaseMap.add base index formal_map) - AccessPath.BaseMap.empty - formals_with_nums in - + let make_extras = FormalMap.make in ignore(Interprocedural.compute_and_store_post ~compute_post ~make_extras callback) end diff --git a/infer/src/unit/TaintTests.ml b/infer/src/unit/TaintTests.ml index 8a7e08bfe..1f5c81e63 100644 --- a/infer/src/unit/TaintTests.ml +++ b/infer/src/unit/TaintTests.ml @@ -257,6 +257,6 @@ let tests = ] |> TestInterpreter.create_tests ~pp_opt:pp_sparse - AccessPath.BaseMap.empty + FormalMap.empty ~initial:MockTaintAnalysis.Domain.empty in "taint_test_suite">:::test_list