diff --git a/infer/src/checkers/accessPath.ml b/infer/src/checkers/accessPath.ml index 72d4804cf..162f51628 100644 --- a/infer/src/checkers/accessPath.ml +++ b/infer/src/checkers/accessPath.ml @@ -203,6 +203,10 @@ let is_prefix ((base1, path1) as ap1) ((base2, path2) as ap2) = let extract = function | Exact ap | Abstracted ap -> ap +let to_footprint formal_index access_path = + let _, base_typ = fst (extract access_path) in + with_base (Var.of_formal_index formal_index, base_typ) access_path + let is_exact = function | Exact _ -> true | Abstracted _ -> false diff --git a/infer/src/checkers/accessPath.mli b/infer/src/checkers/accessPath.mli index 4e8a4ee66..b5fdb7025 100644 --- a/infer/src/checkers/accessPath.mli +++ b/infer/src/checkers/accessPath.mli @@ -74,6 +74,9 @@ val of_exp : Exp.t -> Typ.t -> f_resolve_id:(Var.t -> Raw.t option) -> Raw.t lis (** convert [lhs_exp] to a raw access path, resolving identifiers using [f_resolve_id] *) val of_lhs_exp : Exp.t -> Typ.t -> f_resolve_id:(Var.t -> Raw.t option) -> Raw.t option +(** replace the base var with a footprint variable rooted at formal index [formal_index] *) +val to_footprint : int -> t -> t + (** append new accesses to an existing access path; e.g., `append_access x.f [g, h]` produces `x.f.g.h` *) val append : Raw.t -> access list -> Raw.t diff --git a/infer/src/checkers/var.ml b/infer/src/checkers/var.ml index 452350da2..3591cb0ae 100644 --- a/infer/src/checkers/var.ml +++ b/infer/src/checkers/var.ml @@ -24,10 +24,25 @@ let of_id id = let of_pvar pvar = ProgramVar pvar +let of_formal_index formal_index = + of_id (Ident.create_footprint Ident.name_spec formal_index) + let to_exp = function | ProgramVar pvar -> Exp.Lvar pvar | LogicalVar id -> Exp.Var id +let is_global = function + | ProgramVar pvar -> Pvar.is_global pvar + | LogicalVar _ -> false + +let is_return = function + | ProgramVar pvar -> Pvar.is_return pvar + | LogicalVar _ -> false + +let is_footprint = function + | ProgramVar _ -> false + | LogicalVar id -> Ident.is_footprint id + let pp fmt = function | ProgramVar pv -> (Pvar.pp Pp.text) fmt pv | LogicalVar id -> (Ident.pp Pp.text) fmt id diff --git a/infer/src/checkers/var.mli b/infer/src/checkers/var.mli index b341e71fc..0c34380eb 100644 --- a/infer/src/checkers/var.mli +++ b/infer/src/checkers/var.mli @@ -22,8 +22,17 @@ val of_id : Ident.t -> t val of_pvar : Pvar.t -> t +(** Create a variable representing the ith formal of the current procedure *) +val of_formal_index : int -> t + val to_exp : t -> Exp.t +val is_global : t -> bool + +val is_return : t -> bool + +val is_footprint : t -> bool + val pp : Format.formatter -> t -> unit module Map : PrettyPrintable.PPMap with type key = t diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index 0f87c7909..ebad92b50 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -30,25 +30,6 @@ module Make (TaintSpecification : TaintSpec.S) = struct module Domain = TaintDomain - let is_global (var, _) = match var with - | Var.ProgramVar pvar -> Pvar.is_global pvar - | Var.LogicalVar _ -> false - - let is_return (var, _) = match var with - | Var.ProgramVar pvar -> Pvar.is_return pvar - | Var.LogicalVar _ -> false - - let is_footprint (var, _) = match var with - | Var.ProgramVar _ -> false - | Var.LogicalVar id -> Ident.is_footprint id - - let make_footprint_var formal_index = - Var.of_id (Ident.create_footprint Ident.name_spec formal_index) - - let make_footprint_access_path formal_index access_path = - let _, base_typ = fst (AccessPath.extract access_path) in - AccessPath.with_base (make_footprint_var formal_index, base_typ) access_path - type extras = { formal_map : FormalMap.t; summary : Specs.summary; } module TransferFunctions (CFG : ProcCfg.S) = struct @@ -70,9 +51,9 @@ module Make (TaintSpecification : TaintSpec.S) = struct let root, _ = AccessPath.extract access_path in match FormalMap.get_formal_index root proc_data.extras.formal_map with | Some formal_index -> - make_footprint_trace (make_footprint_access_path formal_index access_path) + make_footprint_trace (AccessPath.to_footprint formal_index access_path) | None -> - if is_global root + if Var.is_global (fst root) then make_footprint_trace access_path else None @@ -198,10 +179,10 @@ module Make (TaintSpecification : TaintSpec.S) = struct let pp_access_path_opt fmt = function | None -> F.fprintf fmt "" | Some access_path -> - let raw_access_path = AccessPath.extract access_path in + let base, _ = AccessPath.extract access_path in F.fprintf fmt " with tainted data %a" AccessPath.pp - (if is_footprint (fst raw_access_path) + (if Var.is_footprint (fst base) then (* TODO: resolve footprint identifier to formal name *) access_path @@ -580,9 +561,9 @@ module Make (TaintSpecification : TaintSpec.S) = struct let with_footprint_vars = AccessPath.BaseMap.fold (fun base ((trace, subtree) as node) acc -> - if is_global base || is_return base + if Var.is_global (fst base) || Var.is_return (fst base) then AccessPath.BaseMap.add base node acc - else if is_footprint base + else if Var.is_footprint (fst base) then if is_empty_node node then @@ -596,7 +577,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct else match FormalMap.get_formal_index base formal_map with | Some formal_index -> - let base' = make_footprint_var formal_index, snd base in + let base' = Var.of_formal_index formal_index, snd base in let joined_node = try TaintDomain.node_join (AccessPath.BaseMap.find base' acc) node with Not_found -> node in