From f83284ad7cdd293bd8fe2fa6bef430b804462478 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Tue, 1 Aug 2017 16:34:55 -0700 Subject: [PATCH] [access paths] make raw access paths the default, move abstraction into AccessPath.Abs module Summary: It's nice to have "raw" as the default kind of access path, since it's used much more often than the abstraction. This is also a prereq for supporting index expressions in access paths, since we'll need mutual recursion between accesses and access paths. Reviewed By: jeremydubreil Differential Revision: D5529807 fbshipit-source-id: cb3f521 --- infer/src/IR/HilExp.ml | 6 +- infer/src/IR/HilExp.mli | 6 +- infer/src/IR/HilInstr.ml | 10 +- infer/src/IR/HilInstr.mli | 8 +- infer/src/checkers/IdAccessPathMapDomain.ml | 9 +- infer/src/checkers/IdAccessPathMapDomain.mli | 2 +- infer/src/checkers/NullabilitySuggest.ml | 20 +- infer/src/checkers/Source.ml | 8 +- infer/src/checkers/Source.mli | 4 +- infer/src/checkers/ThreadSafety.ml | 12 +- infer/src/checkers/ThreadSafetyDomain.ml | 21 +- infer/src/checkers/ThreadSafetyDomain.mli | 26 +- infer/src/checkers/Trace.ml | 2 +- infer/src/checkers/accessPath.ml | 256 ++++++++++--------- infer/src/checkers/accessPath.mli | 118 ++++----- infer/src/checkers/accessPathDomains.ml | 18 +- infer/src/checkers/accessPathDomains.mli | 8 +- infer/src/checkers/accessTree.ml | 31 +-- infer/src/checkers/accessTree.mli | 12 +- infer/src/quandary/ClangTrace.ml | 2 +- infer/src/quandary/JavaTaintAnalysis.ml | 2 +- infer/src/quandary/TaintAnalysis.ml | 45 ++-- infer/src/unit/TaintTests.ml | 2 +- infer/src/unit/TraceTests.ml | 2 +- infer/src/unit/accessPathTestUtils.mli | 2 +- infer/src/unit/accessPathTests.ml | 51 ++-- infer/src/unit/accessTreeTests.ml | 43 ++-- 27 files changed, 368 insertions(+), 358 deletions(-) diff --git a/infer/src/IR/HilExp.ml b/infer/src/IR/HilExp.ml index d1b3f26de..b87697396 100644 --- a/infer/src/IR/HilExp.ml +++ b/infer/src/IR/HilExp.ml @@ -12,7 +12,7 @@ module F = Format module L = Logging type t = - | AccessPath of AccessPath.Raw.t + | AccessPath of AccessPath.t | UnaryOperator of Unop.t * t * Typ.t option | BinaryOperator of Binop.t * t * t | Exception of t @@ -24,7 +24,7 @@ type t = let rec pp fmt = function | AccessPath access_path - -> AccessPath.Raw.pp fmt access_path + -> AccessPath.pp fmt access_path | UnaryOperator (op, e, _) -> F.fprintf fmt "%s%a" (Unop.str op) pp e | BinaryOperator (op, e1, e2) @@ -43,7 +43,7 @@ let rec pp fmt = function let rec get_typ tenv = function | AccessPath access_path - -> AccessPath.Raw.get_typ access_path tenv + -> AccessPath.get_typ access_path tenv | UnaryOperator (_, _, typ_opt) -> typ_opt | BinaryOperator ((Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr), _, _) diff --git a/infer/src/IR/HilExp.mli b/infer/src/IR/HilExp.mli index 09ee3ce4b..5c3a1fbe4 100644 --- a/infer/src/IR/HilExp.mli +++ b/infer/src/IR/HilExp.mli @@ -11,7 +11,7 @@ open! IStd module F = Format type t = - | AccessPath of AccessPath.Raw.t (** access path (e.g., x.f.g or x[i]) *) + | AccessPath of AccessPath.t (** access path (e.g., x.f.g or x[i]) *) | UnaryOperator of Unop.t * t * Typ.t option (** Unary operator with type of the result if known *) | BinaryOperator of Binop.t * t * t (** Binary operator *) @@ -29,10 +29,10 @@ val pp : F.formatter -> t -> unit val get_typ : Tenv.t -> t -> Typ.t option (** Get the type of the expression. Warning: not fully implemented *) -val of_sil : f_resolve_id:(Var.t -> AccessPath.Raw.t option) -> Exp.t -> Typ.t -> t +val of_sil : f_resolve_id:(Var.t -> AccessPath.t option) -> Exp.t -> Typ.t -> t (** Convert SIL expression to HIL expression *) -val get_access_paths : t -> AccessPath.Raw.t list +val get_access_paths : t -> AccessPath.t list (** Get all the access paths used in the given HIL expression, including duplicates if a path is used more than once. *) diff --git a/infer/src/IR/HilInstr.ml b/infer/src/IR/HilInstr.ml index 4a3e8ebfd..bcf2f83aa 100644 --- a/infer/src/IR/HilInstr.ml +++ b/infer/src/IR/HilInstr.ml @@ -11,23 +11,23 @@ open! IStd module F = Format module L = Logging -type call = Direct of Typ.Procname.t | Indirect of AccessPath.Raw.t [@@deriving compare] +type call = Direct of Typ.Procname.t | Indirect of AccessPath.t [@@deriving compare] let pp_call fmt = function | Direct pname -> Typ.Procname.pp fmt pname | Indirect access_path - -> F.fprintf fmt "*%a" AccessPath.Raw.pp access_path + -> F.fprintf fmt "*%a" AccessPath.pp access_path type t = - | Assign of AccessPath.Raw.t * HilExp.t * Location.t + | Assign of AccessPath.t * HilExp.t * Location.t | Assume of HilExp.t * [`Then | `Else] * Sil.if_kind * Location.t | Call of AccessPath.base option * call * HilExp.t list * CallFlags.t * Location.t [@@deriving compare] let pp fmt = function | Assign (access_path, exp, loc) - -> F.fprintf fmt "%a := %a [%a]" AccessPath.Raw.pp access_path HilExp.pp exp Location.pp loc + -> F.fprintf fmt "%a := %a [%a]" AccessPath.pp access_path HilExp.pp exp Location.pp loc | Assume (exp, _, _, loc) -> F.fprintf fmt "assume %a [%a]" HilExp.pp exp Location.pp loc | Call (ret_opt, call, actuals, _, loc) @@ -35,7 +35,7 @@ let pp fmt = function let pp_actuals fmt = PrettyPrintable.pp_collection ~pp_item:HilExp.pp fmt in F.fprintf fmt "%a%a(%a) [%a]" pp_ret ret_opt pp_call call pp_actuals actuals Location.pp loc -type translation = Instr of t | Bind of Var.t * AccessPath.Raw.t | Unbind of Var.t list | Ignore +type translation = Instr of t | Bind of Var.t * AccessPath.t | Unbind of Var.t list | Ignore (* convert an SIL instruction into an HIL instruction. the [f_resolve_id] function should map an SSA temporary variable to the access path it represents. evaluating the HIL instruction should diff --git a/infer/src/IR/HilInstr.mli b/infer/src/IR/HilInstr.mli index 3686d2883..0da0e5e66 100644 --- a/infer/src/IR/HilInstr.mli +++ b/infer/src/IR/HilInstr.mli @@ -11,12 +11,12 @@ open! IStd module F = Format (** type of a procedure call; either direct or via function pointer *) -type call = Direct of Typ.Procname.t | Indirect of AccessPath.Raw.t [@@deriving compare] +type call = Direct of Typ.Procname.t | Indirect of AccessPath.t [@@deriving compare] val pp_call : F.formatter -> call -> unit type t = - | Assign of AccessPath.Raw.t * HilExp.t * Location.t (** LHS access path, RHS expression *) + | Assign of AccessPath.t * HilExp.t * Location.t (** LHS access path, RHS expression *) | Assume of HilExp.t * [`Then | `Else] * Sil.if_kind * Location.t (** Assumed expression, true_branch boolean, source of the assume (conditional, ternary, etc.) *) | Call of AccessPath.base option * call * HilExp.t list * CallFlags.t * Location.t @@ -28,9 +28,9 @@ val pp : F.formatter -> t -> unit (** Result of translating an SIL instruction *) type translation = | Instr of t (** HIL instruction to execute *) - | Bind of Var.t * AccessPath.Raw.t (** add binding to identifier map *) + | Bind of Var.t * AccessPath.t (** add binding to identifier map *) | Unbind of Var.t list (** remove binding from identifier map *) | Ignore (** no-op *) -val of_sil : f_resolve_id:(Var.t -> AccessPath.Raw.t option) -> Sil.instr -> translation +val of_sil : f_resolve_id:(Var.t -> AccessPath.t option) -> Sil.instr -> translation (** Convert an SIL instruction to an HIL instruction *) diff --git a/infer/src/checkers/IdAccessPathMapDomain.ml b/infer/src/checkers/IdAccessPathMapDomain.ml index 4a44868dc..124708f5d 100644 --- a/infer/src/checkers/IdAccessPathMapDomain.ml +++ b/infer/src/checkers/IdAccessPathMapDomain.ml @@ -10,20 +10,19 @@ open! IStd module IdMap = Var.Map -type astate = AccessPath.Raw.t IdMap.t +type astate = AccessPath.t IdMap.t include IdMap -let pp fmt astate = IdMap.pp ~pp_value:AccessPath.Raw.pp fmt astate +let pp fmt astate = IdMap.pp ~pp_value:AccessPath.pp fmt astate let check_invariant ap1 ap2 = function | Var.ProgramVar pvar when Pvar.is_ssa_frontend_tmp pvar -> (* Sawja reuses temporary variables which sometimes breaks this invariant *) () | id - -> if not (AccessPath.Raw.equal ap1 ap2) then - failwithf "Id %a maps to both %a and %a@." Var.pp id AccessPath.Raw.pp ap1 - AccessPath.Raw.pp ap2 + -> if not (AccessPath.equal ap1 ap2) then + failwithf "Id %a maps to both %a and %a@." Var.pp id AccessPath.pp ap1 AccessPath.pp ap2 let ( <= ) ~lhs ~rhs = if phys_equal lhs rhs then true diff --git a/infer/src/checkers/IdAccessPathMapDomain.mli b/infer/src/checkers/IdAccessPathMapDomain.mli index 4819b9149..4c63dce82 100644 --- a/infer/src/checkers/IdAccessPathMapDomain.mli +++ b/infer/src/checkers/IdAccessPathMapDomain.mli @@ -13,7 +13,7 @@ open! IStd module IdMap = Var.Map -type astate = AccessPath.Raw.t IdMap.t +type astate = AccessPath.t IdMap.t include module type of IdMap diff --git a/infer/src/checkers/NullabilitySuggest.ml b/infer/src/checkers/NullabilitySuggest.ml index 68bd05c1d..1f15c4b7c 100644 --- a/infer/src/checkers/NullabilitySuggest.ml +++ b/infer/src/checkers/NullabilitySuggest.ml @@ -13,9 +13,9 @@ module MF = MarkupFormatter module UseDefChain = struct type astate = - | DependsOn of (Location.t * AccessPath.Raw.t) - | NullDefCompare of (Location.t * AccessPath.Raw.t) - | NullDefAssign of (Location.t * AccessPath.Raw.t) + | DependsOn of (Location.t * AccessPath.t) + | NullDefCompare of (Location.t * AccessPath.t) + | NullDefAssign of (Location.t * AccessPath.t) [@@deriving compare] let ( <= ) ~lhs ~rhs = compare_astate lhs rhs <= 0 @@ -28,14 +28,14 @@ module UseDefChain = struct let pp fmt = function | NullDefAssign (loc, ap) - -> F.fprintf fmt "NullDefAssign(%a, %a)" Location.pp loc AccessPath.Raw.pp ap + -> F.fprintf fmt "NullDefAssign(%a, %a)" Location.pp loc AccessPath.pp ap | NullDefCompare (loc, ap) - -> F.fprintf fmt "NullDefCompare(%a, %a)" Location.pp loc AccessPath.Raw.pp ap + -> F.fprintf fmt "NullDefCompare(%a, %a)" Location.pp loc AccessPath.pp ap | DependsOn (loc, ap) - -> F.fprintf fmt "DependsOn(%a, %a)" Location.pp loc AccessPath.Raw.pp ap + -> F.fprintf fmt "DependsOn(%a, %a)" Location.pp loc AccessPath.pp ap end -module Domain = AbstractDomain.Map (AccessPath.Raw) (UseDefChain) +module Domain = AbstractDomain.Map (AccessPath) (UseDefChain) type extras = ProcData.no_extras @@ -46,7 +46,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct type nonrec extras = extras let is_access_nullable ap proc_data = - match AccessPath.Raw.get_field_and_annotation ap proc_data.ProcData.tenv with + match AccessPath.get_field_and_annotation ap proc_data.ProcData.tenv with | Some (_, annot_item) -> Annotations.ia_is_nullable annot_item | _ @@ -103,7 +103,7 @@ module Analyzer = AbstractInterpreter.Make (ProcCfg.Exceptional) (LowerHil.Make let make_error_trace astate ap ud = let name_of ap = - match AccessPath.Raw.get_last_access ap with + match AccessPath.get_last_access ap with | Some AccessPath.FieldAccess field_name -> "Field " ^ Typ.Fieldname.to_flat_string field_name | Some AccessPath.ArrayAccess _ @@ -147,7 +147,7 @@ let checker {Callbacks.summary; proc_desc; tenv} = let report astate (proc_data: extras ProcData.t) = let report_access_path ap udchain = let issue_kind = Localise.to_issue_id Localise.field_should_be_nullable in - match AccessPath.Raw.get_field_and_annotation ap proc_data.tenv with + match AccessPath.get_field_and_annotation ap proc_data.tenv with | Some (field_name, _) when Typ.Fieldname.Java.is_captured_parameter field_name -> (* Skip reporting when field comes from generated code *) () diff --git a/infer/src/checkers/Source.ml b/infer/src/checkers/Source.ml index af37659e0..00898116c 100644 --- a/infer/src/checkers/Source.ml +++ b/infer/src/checkers/Source.ml @@ -31,9 +31,9 @@ module type S = sig val is_footprint : t -> bool - val make_footprint : AccessPath.t -> Procdesc.t -> t + val make_footprint : AccessPath.Abs.t -> Procdesc.t -> t - val get_footprint_access_path : t -> AccessPath.t option + val get_footprint_access_path : t -> AccessPath.Abs.t option val get : CallSite.t -> HilExp.t list -> Tenv.t -> spec option @@ -45,14 +45,14 @@ module Make (Kind : Kind) = struct type kind = | Normal of Kind.t (** known source returned directly or transitively from a callee *) - | Footprint of AccessPath.t (** unknown source read from the environment *) + | Footprint of AccessPath.Abs.t (** unknown source read from the environment *) [@@deriving compare] let pp_kind fmt = function | Normal kind -> Kind.pp fmt kind | Footprint ap - -> F.fprintf fmt "Footprint(%a)" AccessPath.pp ap + -> F.fprintf fmt "Footprint(%a)" AccessPath.Abs.pp ap type t = {kind: kind; site: CallSite.t} [@@deriving compare] diff --git a/infer/src/checkers/Source.mli b/infer/src/checkers/Source.mli index 546fe587f..f42b153b5 100644 --- a/infer/src/checkers/Source.mli +++ b/infer/src/checkers/Source.mli @@ -36,10 +36,10 @@ module type S = sig val is_footprint : t -> bool (** return true if the current source is a footprint source *) - val make_footprint : AccessPath.t -> Procdesc.t -> t + val make_footprint : AccessPath.Abs.t -> Procdesc.t -> t (** create a footprint source for the value read from the given access path. *) - val get_footprint_access_path : t -> AccessPath.t option + val get_footprint_access_path : t -> AccessPath.Abs.t option (** return Some(access path) if the current source is a footprint source, None otherwise *) val get : CallSite.t -> HilExp.t list -> Tenv.t -> spec option diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index 1ed9cccdb..8a4dfdfce 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -326,7 +326,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (* we don't want to warn on accesses to the field if it is (a) thread-confined, or (b) volatile *) let is_safe_access access prefix_path tenv = - match (access, AccessPath.Raw.get_typ prefix_path tenv) with + match (access, AccessPath.get_typ prefix_path tenv) with | ( AccessPath.FieldAccess fieldname , Some ({Typ.desc= Tstruct typename} | {desc= Tptr ({desc= Tstruct typename}, _)}) ) -> ( match Tenv.lookup tenv typename with @@ -765,7 +765,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct AttributeMapDomain.has_attribute access_path Functional astate.attribute_map) rhs_access_paths && - match AccessPath.Raw.get_typ lhs_access_path tenv with + match AccessPath.get_typ lhs_access_path tenv with | Some {Typ.desc= Typ.Tint ILong | Tfloat FDouble} -> (* writes to longs and doubles are not guaranteed to be atomic in Java (http://docs.oracle.com/javase/specs/jls/se7/html/jls-17.html#jls-17.7), so there @@ -803,7 +803,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct [var] is set to true. return None if it has free variables that stop us from evaluating it *) and eval_bexp var = function - | HilExp.AccessPath ap when AccessPath.Raw.equal ap var + | HilExp.AccessPath ap when AccessPath.equal ap var -> Some true | HilExp.Constant c -> Some (not (Const.iszero_int_float c)) @@ -1086,7 +1086,7 @@ let get_all_accesses_with_pre pre_filter access_filter accesses = let get_all_accesses = get_all_accesses_with_pre (fun _ -> true) let pp_container_access fmt (access_path, access_pname) = - F.fprintf fmt "container %a via call to %s" (MF.wrap_monospaced AccessPath.Raw.pp) access_path + F.fprintf fmt "container %a via call to %s" (MF.wrap_monospaced AccessPath.pp) access_path (MF.monospaced_to_string (Typ.Procname.get_method access_pname)) let pp_access fmt sink = @@ -1462,7 +1462,7 @@ let may_alias_container tenv p1 p2 = (* this is much too noisy: we'll warn that accesses to *any* Map can race with accesses to any other Map, etc. Instead, do something simple and unsound: just assume that two accesses can be to the same container if they are to the same access path *) - match (AccessPath.Raw.get_typ p1 tenv, AccessPath.Raw.get_typ p2 tenv) with + match (AccessPath.get_typ p1 tenv, AccessPath.get_typ p2 tenv) with | Some {desc= Tptr ({desc= Tstruct tn1}, _)}, Some {desc= Tptr ({desc= Tstruct tn2}, _)} -> PatternMatch.is_subtype tenv tn1 tn2 || PatternMatch.is_subtype tenv tn2 tn1 | _ @@ -1480,7 +1480,7 @@ let may_alias_container tenv p1 p2 = the `this`'s as equal if their types are compatible *) AccessPath.equal_access_list (snd p1) (snd p2) | _ - -> AccessPath.Raw.equal p1 p2 + -> AccessPath.equal p1 p2 (* equivalence relation computing whether two access paths may refer to the same heap location. *) diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml index d604f28a9..0484fca9a 100644 --- a/infer/src/checkers/ThreadSafetyDomain.ml +++ b/infer/src/checkers/ThreadSafetyDomain.ml @@ -12,10 +12,10 @@ module F = Format module Access = struct type t = - | Read of AccessPath.Raw.t - | Write of AccessPath.Raw.t - | ContainerRead of AccessPath.Raw.t * Typ.Procname.t - | ContainerWrite of AccessPath.Raw.t * Typ.Procname.t + | Read of AccessPath.t + | Write of AccessPath.t + | ContainerRead of AccessPath.t * Typ.Procname.t + | ContainerWrite of AccessPath.t * Typ.Procname.t | InterfaceCall of Typ.Procname.t [@@deriving compare] @@ -35,14 +35,13 @@ module Access = struct let pp fmt = function | Read access_path - -> F.fprintf fmt "Read of %a" AccessPath.Raw.pp access_path + -> F.fprintf fmt "Read of %a" AccessPath.pp access_path | Write access_path - -> F.fprintf fmt "Write to %a" AccessPath.Raw.pp access_path + -> F.fprintf fmt "Write to %a" AccessPath.pp access_path | ContainerRead (access_path, pname) - -> F.fprintf fmt "Read of container %a via %a" AccessPath.Raw.pp access_path Typ.Procname.pp - pname + -> F.fprintf fmt "Read of container %a via %a" AccessPath.pp access_path Typ.Procname.pp pname | ContainerWrite (access_path, pname) - -> F.fprintf fmt "Write to container %a via %a" AccessPath.Raw.pp access_path Typ.Procname.pp + -> F.fprintf fmt "Write to container %a via %a" AccessPath.pp access_path Typ.Procname.pp pname | InterfaceCall pname -> F.fprintf fmt "Call to un-annotated interface method %a" Typ.Procname.pp pname @@ -151,7 +150,7 @@ end module AttributeSetDomain = AbstractDomain.InvertedSet (Attribute.Set) module AttributeMapDomain = struct - include AbstractDomain.InvertedMap (AccessPath.RawMap) (AttributeSetDomain) + include AbstractDomain.InvertedMap (AccessPath.Map) (AttributeSetDomain) let has_attribute access_path attribute t = try find access_path t |> AttributeSetDomain.mem attribute @@ -280,7 +279,7 @@ let empty = let threads = false in let locks = false in let accesses = AccessDomain.empty in - let attribute_map = AccessPath.RawMap.empty in + let attribute_map = AccessPath.Map.empty in let escapees = EscapeeDomain.empty in {thumbs_up; threads; locks; accesses; attribute_map; escapees} diff --git a/infer/src/checkers/ThreadSafetyDomain.mli b/infer/src/checkers/ThreadSafetyDomain.mli index 88abc7242..0e7e626d9 100644 --- a/infer/src/checkers/ThreadSafetyDomain.mli +++ b/infer/src/checkers/ThreadSafetyDomain.mli @@ -12,15 +12,15 @@ module F = Format module Access : sig type t = - | Read of AccessPath.Raw.t (** Field or array read *) - | Write of AccessPath.Raw.t (** Field or array write *) - | ContainerRead of AccessPath.Raw.t * Typ.Procname.t (** Read of container object *) - | ContainerWrite of AccessPath.Raw.t * Typ.Procname.t (** Write to container object *) + | Read of AccessPath.t (** Field or array read *) + | Write of AccessPath.t (** Field or array write *) + | ContainerRead of AccessPath.t * Typ.Procname.t (** Read of container object *) + | ContainerWrite of AccessPath.t * Typ.Procname.t (** Write to container object *) | InterfaceCall of Typ.Procname.t (** Call to method of interface not annotated with @ThreadSafe *) [@@deriving compare] - val get_access_path : t -> AccessPath.Raw.t option + val get_access_path : t -> AccessPath.t option val equal : t -> t -> bool @@ -77,17 +77,17 @@ end module AttributeSetDomain : module type of AbstractDomain.InvertedSet (Attribute.Set) module AttributeMapDomain : sig - include module type of AbstractDomain.InvertedMap (AccessPath.RawMap) (AttributeSetDomain) + include module type of AbstractDomain.InvertedMap (AccessPath.Map) (AttributeSetDomain) - val has_attribute : AccessPath.Raw.t -> Attribute.t -> astate -> bool + val has_attribute : AccessPath.t -> Attribute.t -> astate -> bool - val get_conditional_ownership_index : AccessPath.Raw.t -> astate -> int option + val get_conditional_ownership_index : AccessPath.t -> astate -> int option (** get the formal index of the the formal that must own the given access path (if any) *) - val get_choices : AccessPath.Raw.t -> astate -> Choice.t list + val get_choices : AccessPath.t -> astate -> Choice.t list (** get the choice attributes associated with the given access path *) - val add_attribute : AccessPath.Raw.t -> Attribute.t -> astate -> astate + val add_attribute : AccessPath.t -> Attribute.t -> astate -> astate end (** Excluders: Two things can provide for mutual exclusion: holding a lock, @@ -140,7 +140,7 @@ module Escapee : sig val pp : F.formatter -> t -> unit - val of_access_path : FormalMap.t -> AccessPath.Raw.t -> t + val of_access_path : FormalMap.t -> AccessPath.t -> t end (** set of formals or locals that may escape *) @@ -181,9 +181,9 @@ type summary = include AbstractDomain.WithBottom with type astate := astate val make_container_access : - AccessPath.Raw.t -> Typ.Procname.t -> is_write:bool -> Location.t -> TraceElem.t + AccessPath.t -> Typ.Procname.t -> is_write:bool -> Location.t -> TraceElem.t -val make_field_access : AccessPath.Raw.t -> is_write:bool -> Location.t -> TraceElem.t +val make_field_access : AccessPath.t -> is_write:bool -> Location.t -> TraceElem.t val make_unannotated_call_access : Typ.Procname.t -> Location.t -> TraceElem.t diff --git a/infer/src/checkers/Trace.ml b/infer/src/checkers/Trace.ml index a85a222e9..3fc5f3cf5 100644 --- a/infer/src/checkers/Trace.ml +++ b/infer/src/checkers/Trace.ml @@ -351,7 +351,7 @@ module Make (Spec : Spec) = struct let get_footprint_index source = match Source.get_footprint_access_path source with | Some access_path - -> AccessPath.get_footprint_index access_path + -> AccessPath.Abs.get_footprint_index access_path | None -> None diff --git a/infer/src/checkers/accessPath.ml b/infer/src/checkers/accessPath.ml index 0d7c69484..5561c108c 100644 --- a/infer/src/checkers/accessPath.ml +++ b/infer/src/checkers/accessPath.ml @@ -10,35 +10,35 @@ open! IStd module F = Format -type _typ = Typ.t +module Raw = struct + type _typ = Typ.t -let compare__typ _ _ = 0 + let compare__typ _ _ = 0 -(* ignore types while comparing bases. we can't trust the types from all of our frontends to be + (* ignore types while comparing bases. we can't trust the types from all of our frontends to be consistent, and the variable names should already be enough to distinguish the bases. *) -type base = Var.t * _typ [@@deriving compare] + type base = Var.t * _typ [@@deriving compare] -let equal_base = [%compare.equal : base] + let equal_base = [%compare.equal : base] -type access = ArrayAccess of Typ.t | FieldAccess of Typ.Fieldname.t [@@deriving compare] + type access = ArrayAccess of Typ.t | FieldAccess of Typ.Fieldname.t [@@deriving compare] -let equal_access = [%compare.equal : access] + let equal_access = [%compare.equal : access] -let equal_access_list l1 l2 = Int.equal (List.compare compare_access l1 l2) 0 + let equal_access_list l1 l2 = Int.equal (List.compare compare_access l1 l2) 0 -let pp_base fmt (pvar, _) = Var.pp fmt pvar + let pp_base fmt (pvar, _) = Var.pp fmt pvar -let pp_access fmt = function - | FieldAccess field_name - -> Typ.Fieldname.pp fmt field_name - | ArrayAccess _ - -> F.fprintf fmt "[_]" + let pp_access fmt = function + | FieldAccess field_name + -> Typ.Fieldname.pp fmt field_name + | ArrayAccess _ + -> F.fprintf fmt "[_]" -let pp_access_list fmt accesses = - let pp_sep _ _ = F.fprintf fmt "." in - F.pp_print_list ~pp_sep pp_access fmt accesses + let pp_access_list fmt accesses = + let pp_sep _ _ = F.fprintf fmt "." in + F.pp_print_list ~pp_sep pp_access fmt accesses -module Raw = struct type t = base * access list [@@deriving compare] let equal = [%compare.equal : t] @@ -109,6 +109,72 @@ module Raw = struct | _ -> None + let base_of_pvar pvar typ = (Var.of_pvar pvar, typ) + + let base_of_id id typ = (Var.of_id id, typ) + + let of_pvar pvar typ = (base_of_pvar pvar typ, []) + + let of_id id typ = (base_of_id id typ, []) + + let of_exp exp0 typ0 ~(f_resolve_id: Var.t -> t option) = + (* [typ] is the type of the last element of the access path (e.g., typeof(g) for x.f.g) *) + let rec of_exp_ exp typ accesses acc = + match exp with + | Exp.Var id -> ( + match f_resolve_id (Var.of_id id) with + | Some (base, base_accesses) + -> (base, base_accesses @ accesses) :: acc + | None + -> (base_of_id id typ, accesses) :: acc ) + | Exp.Lvar pvar when Pvar.is_ssa_frontend_tmp pvar -> ( + match f_resolve_id (Var.of_pvar pvar) with + | Some (base, base_accesses) + -> (base, base_accesses @ accesses) :: acc + | None + -> (base_of_pvar pvar typ, accesses) :: acc ) + | Exp.Lvar pvar + -> (base_of_pvar pvar typ, accesses) :: acc + | Exp.Lfield (root_exp, fld, root_exp_typ) + -> let field_access = FieldAccess fld in + of_exp_ root_exp root_exp_typ (field_access :: accesses) acc + | Exp.Lindex (root_exp, _) + -> let array_access = ArrayAccess typ in + let array_typ = Typ.mk (Tarray (typ, None, None)) in + of_exp_ root_exp array_typ (array_access :: accesses) acc + | Exp.Cast (cast_typ, cast_exp) + -> of_exp_ cast_exp cast_typ [] acc + | Exp.UnOp (_, unop_exp, _) + -> of_exp_ unop_exp typ [] acc + | Exp.Exn exn_exp + -> of_exp_ exn_exp typ [] acc + | Exp.BinOp (_, exp1, exp2) + -> of_exp_ exp1 typ [] acc |> of_exp_ exp2 typ [] + | Exp.Const _ | Closure _ | Sizeof _ + -> (* trying to make access path from an invalid expression *) + acc + in + of_exp_ exp0 typ0 [] [] + + let of_lhs_exp lhs_exp typ ~(f_resolve_id: Var.t -> t option) = + match of_exp lhs_exp typ ~f_resolve_id with [lhs_ap] -> Some lhs_ap | _ -> None + + let append (base, old_accesses) new_accesses = (base, old_accesses @ new_accesses) + + let rec is_prefix_path path1 path2 = + if phys_equal path1 path2 then true + else + match (path1, path2) with + | [], _ + -> true + | _, [] + -> false + | access1 :: p1, access2 :: p2 + -> equal_access access1 access2 && is_prefix_path p1 p2 + + let is_prefix (base1, path1 as ap1) (base2, path2 as ap2) = + if phys_equal ap1 ap2 then true else equal_base base1 base2 && is_prefix_path path1 path2 + let pp fmt = function | base, [] -> pp_base fmt base @@ -116,112 +182,52 @@ module Raw = struct -> F.fprintf fmt "%a.%a" pp_base base pp_access_list accesses end -type t = Abstracted of Raw.t | Exact of Raw.t [@@deriving compare] - -let equal = [%compare.equal : t] - -let base_of_pvar pvar typ = (Var.of_pvar pvar, typ) - -let base_of_id id typ = (Var.of_id id, typ) - -let of_pvar pvar typ = (base_of_pvar pvar typ, []) - -let of_id id typ = (base_of_id id typ, []) - -let of_exp exp0 typ0 ~(f_resolve_id: Var.t -> Raw.t option) = - (* [typ] is the type of the last element of the access path (e.g., typeof(g) for x.f.g) *) - let rec of_exp_ exp typ accesses acc = - match exp with - | Exp.Var id -> ( - match f_resolve_id (Var.of_id id) with - | Some (base, base_accesses) - -> (base, base_accesses @ accesses) :: acc - | None - -> (base_of_id id typ, accesses) :: acc ) - | Exp.Lvar pvar when Pvar.is_ssa_frontend_tmp pvar -> ( - match f_resolve_id (Var.of_pvar pvar) with - | Some (base, base_accesses) - -> (base, base_accesses @ accesses) :: acc - | None - -> (base_of_pvar pvar typ, accesses) :: acc ) - | Exp.Lvar pvar - -> (base_of_pvar pvar typ, accesses) :: acc - | Exp.Lfield (root_exp, fld, root_exp_typ) - -> let field_access = FieldAccess fld in - of_exp_ root_exp root_exp_typ (field_access :: accesses) acc - | Exp.Lindex (root_exp, _) - -> let array_access = ArrayAccess typ in - let array_typ = Typ.mk (Tarray (typ, None, None)) in - of_exp_ root_exp array_typ (array_access :: accesses) acc - | Exp.Cast (cast_typ, cast_exp) - -> of_exp_ cast_exp cast_typ [] acc - | Exp.UnOp (_, unop_exp, _) - -> of_exp_ unop_exp typ [] acc - | Exp.Exn exn_exp - -> of_exp_ exn_exp typ [] acc - | Exp.BinOp (_, exp1, exp2) - -> of_exp_ exp1 typ [] acc |> of_exp_ exp2 typ [] - | Exp.Const _ | Closure _ | Sizeof _ - -> (* trying to make access path from an invalid expression *) - acc - in - of_exp_ exp0 typ0 [] [] - -let of_lhs_exp lhs_exp typ ~(f_resolve_id: Var.t -> Raw.t option) = - match of_exp lhs_exp typ ~f_resolve_id with [lhs_ap] -> Some lhs_ap | _ -> None - -let append (base, old_accesses) new_accesses = (base, old_accesses @ new_accesses) - -let with_base base = function - | Exact (_, accesses) - -> Exact (base, accesses) - | Abstracted (_, accesses) - -> Abstracted (base, accesses) - -let rec is_prefix_path path1 path2 = - if phys_equal path1 path2 then true - else - match (path1, path2) with - | [], _ - -> true - | _, [] +module Abs = struct + type raw = Raw.t + + type t = Abstracted of Raw.t | Exact of Raw.t [@@deriving compare] + + let equal = [%compare.equal : t] + + let extract = function Exact ap | Abstracted ap -> ap + + let with_base base = function + | Exact (_, accesses) + -> Exact (base, accesses) + | Abstracted (_, accesses) + -> Abstracted (base, accesses) + + 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 get_footprint_index access_path = + let raw_access_path = extract access_path in + match raw_access_path with + | (Var.LogicalVar id, _), _ when Ident.is_footprint id + -> Some (Ident.get_stamp id) + | _ + -> None + + let is_exact = function Exact _ -> true | Abstracted _ -> false + + let ( <= ) ~lhs ~rhs = + match (lhs, rhs) with + | Abstracted _, Exact _ -> false - | access1 :: p1, access2 :: p2 - -> equal_access access1 access2 && is_prefix_path p1 p2 - -let is_prefix (base1, path1 as ap1) (base2, path2 as ap2) = - if phys_equal ap1 ap2 then true else equal_base base1 base2 && is_prefix_path path1 path2 - -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 get_footprint_index access_path = - let raw_access_path = extract access_path in - match raw_access_path with - | (Var.LogicalVar id, _), _ when Ident.is_footprint id - -> Some (Ident.get_stamp id) - | _ - -> None - -let is_exact = function Exact _ -> true | Abstracted _ -> false - -let ( <= ) ~lhs ~rhs = - match (lhs, rhs) with - | Abstracted _, Exact _ - -> false - | Exact lhs_ap, Exact rhs_ap - -> Raw.equal lhs_ap rhs_ap - | (Exact lhs_ap | Abstracted lhs_ap), Abstracted rhs_ap - -> is_prefix rhs_ap lhs_ap - -let pp fmt = function - | Exact access_path - -> Raw.pp fmt access_path - | Abstracted access_path - -> F.fprintf fmt "%a*" Raw.pp access_path + | Exact lhs_ap, Exact rhs_ap + -> Raw.equal lhs_ap rhs_ap + | (Exact lhs_ap | Abstracted lhs_ap), Abstracted rhs_ap + -> Raw.is_prefix rhs_ap lhs_ap + + let pp fmt = function + | Exact access_path + -> Raw.pp fmt access_path + | Abstracted access_path + -> F.fprintf fmt "%a*" Raw.pp access_path +end + +include Raw module BaseMap = PrettyPrintable.MakePPMap (struct type t = base @@ -239,5 +245,5 @@ module AccessMap = PrettyPrintable.MakePPMap (struct let pp = pp_access end) -module RawSet = PrettyPrintable.MakePPSet (Raw) -module RawMap = PrettyPrintable.MakePPMap (Raw) +module Set = PrettyPrintable.MakePPSet (Raw) +module Map = PrettyPrintable.MakePPMap (Raw) diff --git a/infer/src/checkers/accessPath.mli b/infer/src/checkers/accessPath.mli index e9f345236..6f1bc9bf7 100644 --- a/infer/src/checkers/accessPath.mli +++ b/infer/src/checkers/accessPath.mli @@ -20,101 +20,103 @@ type access = (* field name *) [@@deriving compare] -module Raw : sig - (** root var, and a list of accesses. closest to the root var is first that is, x.f.g is +(** root var, and a list of accesses. closest to the root var is first that is, x.f.g is representedas (x, [f; g]) *) - type t = base * access list [@@deriving compare] +type t = base * access list [@@deriving compare] - val truncate : t -> t - (** remove the last access of the access path if the access list is non-empty. returns the +val truncate : t -> t +(** remove the last access of the access path if the access list is non-empty. returns the original access path if the access list is empty *) - val get_last_access : t -> access option - (** get the last access in the list. returns None if the list is empty *) +val get_last_access : t -> access option +(** get the last access in the list. returns None if the list is empty *) - val get_field_and_annotation : t -> Tenv.t -> (Typ.Fieldname.t * Annot.Item.t) option - (** get the field name and the annotation of the last access in the list of accesses if +val get_field_and_annotation : t -> Tenv.t -> (Typ.Fieldname.t * Annot.Item.t) option +(** get the field name and the annotation of the last access in the list of accesses if the list is non-empty and the last access is a field access *) - val get_typ : t -> Tenv.t -> Typ.t option - (** get the typ of the last access in the list of accesses if the list is non-empty, or the base +val get_typ : t -> Tenv.t -> Typ.t option +(** get the typ of the last access in the list of accesses if the list is non-empty, or the base if the list is empty. that is, for x.f.g, return typ(g), and for x, return typ(x) *) - val equal : t -> t -> bool - - val pp : Format.formatter -> t -> unit -end - -type t = - | Abstracted of Raw.t (** abstraction of heap reachable from an access path, e.g. x.f* *) - | Exact of Raw.t (** precise representation of an access path, e.g. x.f.g *) - [@@deriving compare] - -val equal_base : base -> base -> bool - -val equal_access : access -> access -> bool - -val equal_access_list : access list -> access list -> bool - -val equal : t -> t -> bool - val base_of_pvar : Pvar.t -> Typ.t -> base (** create a base from a pvar *) val base_of_id : Ident.t -> Typ.t -> base (** create a base from an ident *) -val of_pvar : Pvar.t -> Typ.t -> Raw.t +val of_pvar : Pvar.t -> Typ.t -> t (** create an access path from a pvar *) -val of_id : Ident.t -> Typ.t -> Raw.t +val of_id : Ident.t -> Typ.t -> t (** create an access path from an ident *) -val of_exp : Exp.t -> Typ.t -> f_resolve_id:(Var.t -> Raw.t option) -> Raw.t list -(** extract the raw access paths that occur in [exp], 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 -(** convert [lhs_exp] to a raw access path, resolving identifiers using [f_resolve_id] *) +val of_exp : Exp.t -> Typ.t -> f_resolve_id:(Var.t -> t option) -> t list +(** extract the access paths that occur in [exp], resolving identifiers using [f_resolve_id] *) -val to_footprint : int -> t -> t -(** replace the base var with a footprint variable rooted at formal index [formal_index] *) +val of_lhs_exp : Exp.t -> Typ.t -> f_resolve_id:(Var.t -> t option) -> t option +(** convert [lhs_exp] to an access path, resolving identifiers using [f_resolve_id] *) -val get_footprint_index : t -> int option -(** return the formal index associated with the base of this access path if there is one, or None - otherwise *) - -val append : Raw.t -> access list -> Raw.t +val append : t -> access list -> t (** append new accesses to an existing access path; e.g., `append_access x.f [g, h]` produces `x.f.g.h` *) -val with_base : base -> t -> t -(** swap base of existing access path for [base_var] (e.g., `with_base_bvar x y.f.g` produces - `x.f.g` *) - -val is_prefix : Raw.t -> Raw.t -> bool +val is_prefix : t -> t -> bool (** return true if [ap1] is a prefix of [ap2]. returns true for equal access paths *) +val equal : t -> t -> bool + +val equal_base : base -> base -> bool + +val equal_access : access -> access -> bool + +val equal_access_list : access list -> access list -> bool + +val pp : Format.formatter -> t -> unit + +val pp_base : Format.formatter -> base -> unit + val pp_access : Format.formatter -> access -> unit val pp_access_list : Format.formatter -> access list -> unit -val extract : t -> Raw.t -(** extract a raw access path from its wrapper *) +module Abs : sig + type raw = t + + type t = + | Abstracted of raw (** abstraction of heap reachable from an access path, e.g. x.f* *) + | Exact of raw (** precise representation of an access path, e.g. x.f.g *) + [@@deriving compare] -val is_exact : t -> bool -(** return true if [t] is an exact representation of an access path, false if it's an abstraction *) + val equal : t -> t -> bool -val ( <= ) : lhs:t -> rhs:t -> bool -(** return true if \gamma(lhs) \subseteq \gamma(rhs) *) + val to_footprint : int -> t -> t + (** replace the base var with a footprint variable rooted at formal index [formal_index] *) -val pp_base : Format.formatter -> base -> unit + val get_footprint_index : t -> int option + (** return the formal index associated with the base of this access path if there is one, or None + otherwise *) -val pp : Format.formatter -> t -> unit + val with_base : base -> t -> t + (** swap base of existing access path for [base_var] (e.g., `with_base_bvar x y.f.g` produces + `x.f.g` *) + + val extract : t -> raw + (** extract a raw access path from its wrapper *) + + val is_exact : t -> bool + (** return true if [t] is an exact representation of an access path, false if it's an abstraction *) + + val ( <= ) : lhs:t -> rhs:t -> bool + (** return true if \gamma(lhs) \subseteq \gamma(rhs) *) + + val pp : Format.formatter -> t -> unit +end module BaseMap : PrettyPrintable.PPMap with type key = base module AccessMap : PrettyPrintable.PPMap with type key = access -module RawSet : PrettyPrintable.PPSet with type elt = Raw.t +module Set : PrettyPrintable.PPSet with type elt = t -module RawMap : PrettyPrintable.PPMap with type key = Raw.t +module Map : PrettyPrintable.PPMap with type key = t diff --git a/infer/src/checkers/accessPathDomains.ml b/infer/src/checkers/accessPathDomains.ml index db8662a7a..c2af61a4e 100644 --- a/infer/src/checkers/accessPathDomains.ml +++ b/infer/src/checkers/accessPathDomains.ml @@ -11,7 +11,7 @@ open! IStd module F = Format module Set = struct - module APSet = PrettyPrintable.MakePPSet (AccessPath) + module APSet = PrettyPrintable.MakePPSet (AccessPath.Abs) (** TODO (12086310): best-case behavior of some operations can be improved by adding "abstracted" bool recording whether an abstracted access path has been introduced *) @@ -24,7 +24,10 @@ module Set = struct let normalize aps = APSet.filter (fun lhs -> - not (APSet.exists (fun rhs -> not (phys_equal lhs rhs) && AccessPath.( <= ) ~lhs ~rhs) aps)) + not + (APSet.exists + (fun rhs -> not (phys_equal lhs rhs) && AccessPath.Abs.( <= ) ~lhs ~rhs) + aps)) aps let add = APSet.add @@ -32,11 +35,12 @@ module Set = struct let of_list = APSet.of_list let mem ap aps = - APSet.mem ap aps || APSet.exists (fun other_ap -> AccessPath.( <= ) ~lhs:ap ~rhs:other_ap) aps + APSet.mem ap aps + || APSet.exists (fun other_ap -> AccessPath.Abs.( <= ) ~lhs:ap ~rhs:other_ap) aps let mem_fuzzy ap aps = let has_overlap ap1 ap2 = - AccessPath.( <= ) ~lhs:ap1 ~rhs:ap2 || AccessPath.( <= ) ~lhs:ap2 ~rhs:ap1 + AccessPath.Abs.( <= ) ~lhs:ap1 ~rhs:ap2 || AccessPath.Abs.( <= ) ~lhs:ap2 ~rhs:ap1 in APSet.mem ap aps || APSet.exists (has_overlap ap) aps @@ -53,9 +57,9 @@ module Set = struct else let abstract_access_path ap aps = match ap with - | AccessPath.Exact exact_ap - -> APSet.add (AccessPath.Abstracted exact_ap) aps - | AccessPath.Abstracted _ + | AccessPath.Abs.Exact exact_ap + -> APSet.add (AccessPath.Abs.Abstracted exact_ap) aps + | AccessPath.Abs.Abstracted _ -> APSet.add ap aps in let diff_aps = APSet.diff next prev in diff --git a/infer/src/checkers/accessPathDomains.mli b/infer/src/checkers/accessPathDomains.mli index 6daa425b8..e1484d25c 100644 --- a/infer/src/checkers/accessPathDomains.mli +++ b/infer/src/checkers/accessPathDomains.mli @@ -19,17 +19,17 @@ open! IStd module Set : sig include AbstractDomain.WithBottom - val of_list : AccessPath.t list -> astate + val of_list : AccessPath.Abs.t list -> astate - val mem : AccessPath.t -> astate -> bool + val mem : AccessPath.Abs.t -> astate -> bool (** return true if \gamma({ap}) \subseteq \gamma(aps). note: this is worst-case linear in the size of the set *) - val mem_fuzzy : AccessPath.t -> astate -> bool + val mem_fuzzy : AccessPath.Abs.t -> astate -> bool (** more permissive version of [mem]; return true if \gamma({a}) \cap \gamma(aps) != {}. note: this is worst-case linear in the size of the set *) - val add : AccessPath.t -> astate -> astate + val add : AccessPath.Abs.t -> astate -> astate val normalize : astate -> astate (** simplify an access path set to its canonical representation by eliminating redundancies diff --git a/infer/src/checkers/accessTree.ml b/infer/src/checkers/accessTree.ml index 6f68cde53..0cd7a8127 100644 --- a/infer/src/checkers/accessTree.ml +++ b/infer/src/checkers/accessTree.ml @@ -34,19 +34,19 @@ module type S = sig val make_starred_leaf : TraceDomain.astate -> node - val get_node : AccessPath.t -> t -> node option + val get_node : AccessPath.Abs.t -> t -> node option - val get_trace : AccessPath.t -> t -> TraceDomain.astate option + val get_trace : AccessPath.Abs.t -> t -> TraceDomain.astate option - val add_node : AccessPath.t -> node -> t -> t + val add_node : AccessPath.Abs.t -> node -> t -> t - val add_trace : AccessPath.t -> TraceDomain.astate -> t -> t + val add_trace : AccessPath.Abs.t -> TraceDomain.astate -> t -> t val node_join : node -> node -> node - val fold : ('a -> AccessPath.t -> node -> 'a) -> t -> 'a -> 'a + val fold : ('a -> AccessPath.Abs.t -> node -> 'a) -> t -> 'a -> 'a - val trace_fold : ('a -> AccessPath.t -> TraceDomain.astate -> 'a) -> t -> 'a -> 'a + val trace_fold : ('a -> AccessPath.Abs.t -> TraceDomain.astate -> 'a) -> t -> 'a -> 'a val pp_node : F.formatter -> node -> unit end @@ -104,10 +104,10 @@ module Make (TraceDomain : AbstractDomain.WithBottom) = struct let base_trace, base_tree = BaseMap.find base tree in accesses_get_node accesses base_trace base_tree in - let base, accesses = AccessPath.extract ap in + let base, accesses = AccessPath.Abs.extract ap in match get_node_ base accesses tree with | trace, subtree - -> if AccessPath.is_exact ap then Some (trace, subtree) + -> if AccessPath.Abs.is_exact ap then Some (trace, subtree) else (* input query was [ap]*, and [trace] is the trace associated with [ap]. get the traces associated with the children of [ap] in [tree] and join them with [trace] *) @@ -222,8 +222,8 @@ module Make (TraceDomain : AbstractDomain.WithBottom) = struct access_tree_add_trace_ ~seen_array_access accesses node let add_node ap node_to_add tree = - let base, accesses = AccessPath.extract ap in - let is_exact = AccessPath.is_exact ap in + let base, accesses = AccessPath.Abs.extract ap in + let is_exact = AccessPath.Abs.is_exact ap in let base_node = try BaseMap.find base tree with Not_found -> make_normal_leaf TraceDomain.empty @@ -246,17 +246,18 @@ module Make (TraceDomain : AbstractDomain.WithBottom) = struct let cur_ap_raw = (base, accesses) in match tree with | Subtree access_map - -> let acc' = f acc (AccessPath.Exact cur_ap_raw) node in + -> let acc' = f acc (AccessPath.Abs.Exact cur_ap_raw) node in access_map_fold_ f base accesses access_map acc' | Star - -> f acc (AccessPath.Abstracted cur_ap_raw) node + -> f acc (AccessPath.Abs.Abstracted cur_ap_raw) node - let node_fold (f: 'a -> AccessPath.t -> node -> 'a) base node acc = node_fold_ f base [] node acc + let node_fold (f: 'a -> AccessPath.Abs.t -> node -> 'a) base node acc = + node_fold_ f base [] node acc - let fold (f: 'a -> AccessPath.t -> node -> 'a) tree acc_ = + let fold (f: 'a -> AccessPath.Abs.t -> node -> 'a) tree acc_ = BaseMap.fold (fun base node acc -> node_fold f base node acc) tree acc_ - let trace_fold (f: 'a -> AccessPath.t -> TraceDomain.astate -> 'a) = + let trace_fold (f: 'a -> AccessPath.Abs.t -> TraceDomain.astate -> 'a) = let f_ acc ap (trace, _) = f acc ap trace in fold f_ diff --git a/infer/src/checkers/accessTree.mli b/infer/src/checkers/accessTree.mli index 38868486c..39822d960 100644 --- a/infer/src/checkers/accessTree.mli +++ b/infer/src/checkers/accessTree.mli @@ -50,18 +50,18 @@ module type S = sig val make_starred_leaf : TraceDomain.astate -> node (** create a leaf node with a wildcard successor *) - val get_node : AccessPath.t -> t -> node option + val get_node : AccessPath.Abs.t -> t -> node option (** retrieve the node associated with the given access path *) - val get_trace : AccessPath.t -> t -> TraceDomain.astate option + val get_trace : AccessPath.Abs.t -> t -> TraceDomain.astate option (** retrieve the trace associated with the given access path *) - val add_node : AccessPath.t -> node -> t -> t + val add_node : AccessPath.Abs.t -> node -> t -> t (** add the given access path to the tree and associate its last access with with the given node. if any of the accesses in the path are not already present in the tree, they will be added with with empty traces associated with each of the inner nodes. *) - val add_trace : AccessPath.t -> TraceDomain.astate -> t -> t + val add_trace : AccessPath.Abs.t -> TraceDomain.astate -> t -> t (** add the given access path to the tree and associate its last access with with the given trace. if any of the accesses in the path are not already present in the tree, they will be added with with empty traces associated with each of the inner nodes. *) @@ -69,10 +69,10 @@ module type S = sig val node_join : node -> node -> node (** join two nodes *) - val fold : ('a -> AccessPath.t -> node -> 'a) -> t -> 'a -> 'a + val fold : ('a -> AccessPath.Abs.t -> node -> 'a) -> t -> 'a -> 'a (** apply a function to each (access path, node) pair in the tree. *) - val trace_fold : ('a -> AccessPath.t -> TraceDomain.astate -> 'a) -> t -> 'a -> 'a + val trace_fold : ('a -> AccessPath.Abs.t -> TraceDomain.astate -> 'a) -> t -> 'a -> 'a val pp_node : Format.formatter -> node -> unit end diff --git a/infer/src/quandary/ClangTrace.ml b/infer/src/quandary/ClangTrace.ml index 6d9bb9dd5..523c24d88 100644 --- a/infer/src/quandary/ClangTrace.ml +++ b/infer/src/quandary/ClangTrace.ml @@ -222,7 +222,7 @@ include Trace.Make (struct let is_gflag pvar = String.is_substring ~substring:"FLAGS_" (Pvar.get_simplified_name pvar) in - match Option.map ~f:AccessPath.extract (Source.get_footprint_access_path source) with + match Option.map ~f:AccessPath.Abs.extract (Source.get_footprint_access_path source) with | Some ((Var.ProgramVar pvar, _), _) when Pvar.is_global pvar && is_gflag pvar -> (* gflags globals come from the environment; treat them as sources *) true diff --git a/infer/src/quandary/JavaTaintAnalysis.ml b/infer/src/quandary/JavaTaintAnalysis.ml index f09857cdc..7ec8a5d9e 100644 --- a/infer/src/quandary/JavaTaintAnalysis.ml +++ b/infer/src/quandary/JavaTaintAnalysis.ml @@ -26,7 +26,7 @@ include TaintAnalysis.Make (struct let handle_unknown_call pname ret_typ_opt actuals tenv = let get_receiver_typ tenv = function | HilExp.AccessPath access_path - -> AccessPath.Raw.get_typ access_path tenv + -> AccessPath.get_typ access_path tenv | _ -> None in diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index d6227da85..0d9d9dace 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -48,10 +48,10 @@ module Make (TaintSpecification : TaintSpec.S) = struct in Some (TaintDomain.make_normal_leaf trace) in - let root, _ = AccessPath.extract access_path in + let root, _ = AccessPath.Abs.extract access_path in match FormalMap.get_formal_index root proc_data.extras.formal_map with | Some formal_index - -> make_footprint_trace (AccessPath.to_footprint formal_index access_path) + -> make_footprint_trace (AccessPath.Abs.to_footprint formal_index access_path) | None -> if Var.is_global (fst root) then make_footprint_trace access_path else None @@ -65,8 +65,8 @@ module Make (TaintSpecification : TaintSpec.S) = struct let exp_get_node_ ~abstracted raw_access_path access_tree proc_data = let access_path = - if abstracted then AccessPath.Abstracted raw_access_path - else AccessPath.Exact raw_access_path + if abstracted then AccessPath.Abs.Abstracted raw_access_path + else AccessPath.Abs.Exact raw_access_path in access_path_get_node access_path access_tree proc_data @@ -80,13 +80,13 @@ module Make (TaintSpecification : TaintSpec.S) = struct let add_return_source source ret_base access_tree = let trace = TraceDomain.of_source source in - let id_ap = AccessPath.Exact (ret_base, []) in + let id_ap = AccessPath.Abs.Exact (ret_base, []) in TaintDomain.add_trace id_ap trace access_tree let add_actual_source source index actuals access_tree proc_data = match List.nth_exn actuals index with | HilExp.AccessPath actual_ap_raw - -> let actual_ap = AccessPath.Exact actual_ap_raw in + -> let actual_ap = AccessPath.Abs.Exact actual_ap_raw in let trace = access_path_get_trace actual_ap access_tree proc_data in TaintDomain.add_trace actual_ap (TraceDomain.add_source source trace) access_tree | _ @@ -200,8 +200,8 @@ module Make (TaintSpecification : TaintSpec.S) = struct | None -> F.fprintf fmt "" | Some access_path - -> let base, _ = AccessPath.extract access_path in - F.fprintf fmt " with tainted data %a" AccessPath.pp + -> let base, _ = AccessPath.Abs.extract access_path in + F.fprintf fmt " with tainted data %a" AccessPath.Abs.pp ( if Var.is_footprint (fst base) then (* TODO: resolve footprint identifier to formal name *) access_path @@ -241,7 +241,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct match List.nth_exn actuals sink_index with | HilExp.AccessPath actual_ap_raw -> ( - let actual_ap = AccessPath.Abstracted actual_ap_raw in + let actual_ap = AccessPath.Abs.Abstracted actual_ap_raw in match access_path_get_node actual_ap access_tree_acc proc_data with | Some (actual_trace, _) -> let sink' = @@ -264,10 +264,10 @@ module Make (TaintSpecification : TaintSpec.S) = struct let apply_return ret_ap = match ret_opt with | Some base_var - -> Some (AccessPath.with_base base_var ret_ap) + -> Some (AccessPath.Abs.with_base base_var ret_ap) | None -> Logging.internal_error "Have summary for retval, but no ret id to bind it to: %a@\n" - AccessPath.pp ret_ap ; + AccessPath.Abs.pp ret_ap ; None in let get_actual_ap formal_index = @@ -276,11 +276,13 @@ module Make (TaintSpecification : TaintSpec.S) = struct ~default:None (List.nth actuals formal_index) in let project ~formal_ap ~actual_ap = - let projected_ap = AccessPath.append actual_ap (snd (AccessPath.extract formal_ap)) in - if AccessPath.is_exact formal_ap then AccessPath.Exact projected_ap - else AccessPath.Abstracted projected_ap + let projected_ap = + AccessPath.append actual_ap (snd (AccessPath.Abs.extract formal_ap)) + in + if AccessPath.Abs.is_exact formal_ap then AccessPath.Abs.Exact projected_ap + else AccessPath.Abs.Abstracted projected_ap in - let base_var, _ = fst (AccessPath.extract formal_ap) in + let base_var, _ = fst (AccessPath.Abs.extract formal_ap) in match base_var with | Var.ProgramVar pvar -> if Pvar.is_return pvar then apply_return formal_ap else Some formal_ap @@ -342,7 +344,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct let rhs_node = Option.value (hil_exp_get_node rhs_exp astate proc_data) ~default:TaintDomain.empty_node in - TaintDomain.add_node (AccessPath.Exact lhs_access_path) rhs_node astate + TaintDomain.add_node (AccessPath.Abs.Exact lhs_access_path) rhs_node astate in match instr with | Assign (((Var.ProgramVar pvar, _), []), HilExp.Exception _, _) when Pvar.is_return pvar @@ -391,7 +393,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct match TraceDomain.Source.get_footprint_access_path source with | Some access_path -> Option.exists - (AccessPath.Raw.get_typ (AccessPath.extract access_path) proc_data.tenv) + (AccessPath.get_typ (AccessPath.Abs.extract access_path) proc_data.tenv) ~f:should_taint_typ | None -> true) @@ -407,15 +409,16 @@ module Make (TaintSpecification : TaintSpec.S) = struct | _, [], _ -> astate_acc | TaintSpec.Propagate_to_return, actuals, Some ret_ap - -> propagate_to_access_path (AccessPath.Exact (ret_ap, [])) actuals astate_acc + -> propagate_to_access_path (AccessPath.Abs.Exact (ret_ap, [])) actuals astate_acc | ( TaintSpec.Propagate_to_receiver , (AccessPath receiver_ap) :: (_ :: _ as other_actuals) , _ ) - -> propagate_to_access_path (AccessPath.Exact receiver_ap) other_actuals astate_acc + -> propagate_to_access_path (AccessPath.Abs.Exact receiver_ap) other_actuals + astate_acc | TaintSpec.Propagate_to_actual actual_index, _, _ -> ( match List.nth actuals actual_index with | Some HilExp.AccessPath actual_ap - -> propagate_to_access_path (AccessPath.Exact actual_ap) actuals astate_acc + -> propagate_to_access_path (AccessPath.Abs.Exact actual_ap) actuals astate_acc | _ -> astate_acc ) | _ @@ -622,7 +625,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct ~f:(fun acc (name, typ, taint_opt) -> match taint_opt with | Some source - -> let base_ap = AccessPath.Exact (AccessPath.of_pvar (Pvar.mk name pname) typ) in + -> let base_ap = AccessPath.Abs.Exact (AccessPath.of_pvar (Pvar.mk name pname) typ) in TaintDomain.add_trace base_ap (TraceDomain.of_source source) acc | None -> acc) diff --git a/infer/src/unit/TaintTests.ml b/infer/src/unit/TaintTests.ml index 1965fced7..9acb1c2c3 100644 --- a/infer/src/unit/TaintTests.ml +++ b/infer/src/unit/TaintTests.ml @@ -83,7 +83,7 @@ let tests = F.fprintf fmt "(%a -> %a)" pp_sources (MockTrace.sources trace) pp_sinks (MockTrace.sinks trace) in - let pp_item fmt (ap, trace) = F.fprintf fmt "%a => %a" AccessPath.pp ap pp_trace trace in + let pp_item fmt (ap, trace) = F.fprintf fmt "%a => %a" AccessPath.Abs.pp ap pp_trace trace in (* flatten access tree into list of access paths with associated traces *) let trace_assocs = MockTaintAnalysis.TaintDomain.trace_fold diff --git a/infer/src/unit/TraceTests.ml b/infer/src/unit/TraceTests.ml index 1f89e45d9..aa8e25fd7 100644 --- a/infer/src/unit/TraceTests.ml +++ b/infer/src/unit/TraceTests.ml @@ -114,7 +114,7 @@ let tests = let append_ _ = let call_site = CallSite.dummy in let footprint_ap = - AccessPath.Exact (AccessPath.of_id (Ident.create_none ()) (Typ.mk Tvoid)) + AccessPath.Abs.Exact (AccessPath.of_id (Ident.create_none ()) (Typ.mk Tvoid)) in let dummy_pdesc = Cfg.create_proc_desc (Cfg.create_cfg ()) diff --git a/infer/src/unit/accessPathTestUtils.mli b/infer/src/unit/accessPathTestUtils.mli index e7ca56aa3..37fdfea5e 100644 --- a/infer/src/unit/accessPathTestUtils.mli +++ b/infer/src/unit/accessPathTestUtils.mli @@ -19,4 +19,4 @@ val make_field_access : string -> AccessPath.access val make_array_access : Typ.t -> AccessPath.access -val make_access_path : string -> string list -> AccessPath.Raw.t +val make_access_path : string -> string list -> AccessPath.t diff --git a/infer/src/unit/accessPathTests.ml b/infer/src/unit/accessPathTests.ml index ec9018187..ad9447557 100644 --- a/infer/src/unit/accessPathTests.ml +++ b/infer/src/unit/accessPathTests.ml @@ -25,32 +25,28 @@ let tests = let base = make_base "x" ~typ:dummy_arr_typ in (base, [make_array_access dummy_typ]) in - let x_exact = AccessPath.Exact x in - let y_exact = AccessPath.Exact y in - let x_abstract = AccessPath.Abstracted x in - let xF_exact = AccessPath.Exact xF in - let xFG_exact = AccessPath.Exact xFG in - let yF_exact = AccessPath.Exact yF in - let yF_abstract = AccessPath.Abstracted yF in + let x_exact = AccessPath.Abs.Exact x in + let y_exact = AccessPath.Abs.Exact y in + let x_abstract = AccessPath.Abs.Abstracted x in + let xF_exact = AccessPath.Abs.Exact xF in + let xFG_exact = AccessPath.Abs.Exact xFG in + let yF_exact = AccessPath.Abs.Exact yF in + let yF_abstract = AccessPath.Abs.Abstracted yF in let open OUnit2 in let equal_test = let equal_test_ _ = - assert_bool "equal works for bases" (AccessPath.Raw.equal x (make_access_path "x" [])) ; - assert_bool "equal works for paths" - (AccessPath.Raw.equal xFG (make_access_path "x" ["f"; "g"])) ; - assert_bool "disequality works for bases" (not (AccessPath.Raw.equal x y)) ; - assert_bool "disequality works for paths" (not (AccessPath.Raw.equal xF xFG)) + assert_bool "equal works for bases" (AccessPath.equal x (make_access_path "x" [])) ; + assert_bool "equal works for paths" (AccessPath.equal xFG (make_access_path "x" ["f"; "g"])) ; + assert_bool "disequality works for bases" (not (AccessPath.equal x y)) ; + assert_bool "disequality works for paths" (not (AccessPath.equal xF xFG)) in "equal" >:: equal_test_ in let append_test = let pp_diff fmt (actual, expected) = - F.fprintf fmt "Expected output %a but got %a" AccessPath.Raw.pp expected AccessPath.Raw.pp - actual - in - let assert_eq input expected = - assert_equal ~cmp:AccessPath.Raw.equal ~pp_diff input expected + F.fprintf fmt "Expected output %a but got %a" AccessPath.pp expected AccessPath.pp actual in + let assert_eq input expected = assert_equal ~cmp:AccessPath.equal ~pp_diff input expected in let append_test_ _ = assert_eq xF (AccessPath.append x [f_access]) ; assert_eq xFG (AccessPath.append xF [g_access]) @@ -85,9 +81,9 @@ let tests = let actual_ap = make_ap exp in let pp_diff fmt (actual_ap, expected_ap) = F.fprintf fmt "Expected to make access path %a from expression %a, but got %a" - AccessPath.Raw.pp expected_ap Exp.pp exp AccessPath.Raw.pp actual_ap + AccessPath.pp expected_ap Exp.pp exp AccessPath.pp actual_ap in - assert_equal ~cmp:AccessPath.Raw.equal ~pp_diff actual_ap expected_ap + assert_equal ~cmp:AccessPath.equal ~pp_diff actual_ap expected_ap in let of_exp_test_ _ = let f_fieldname = make_fieldname "f" in @@ -111,8 +107,7 @@ let tests = let binop_exp = Exp.le xF_exp xFG_exp in match AccessPath.of_exp binop_exp dummy_typ ~f_resolve_id with | [ap1; ap2] - -> assert_equal ~cmp:AccessPath.Raw.equal ap1 xFG ; - assert_equal ~cmp:AccessPath.Raw.equal ap2 xF + -> assert_equal ~cmp:AccessPath.equal ap1 xFG ; assert_equal ~cmp:AccessPath.equal ap2 xF | _ -> assert false in @@ -120,13 +115,13 @@ let tests = in let abstraction_test = let abstraction_test_ _ = - assert_bool "extract" (AccessPath.Raw.equal (AccessPath.extract xF_exact) xF) ; - assert_bool "is_exact" (AccessPath.is_exact x_exact) ; - assert_bool "not is_exact" (not (AccessPath.is_exact x_abstract)) ; - assert_bool "(<=)1" (AccessPath.( <= ) ~lhs:x_exact ~rhs:x_abstract) ; - assert_bool "(<=)2" (AccessPath.( <= ) ~lhs:xF_exact ~rhs:x_abstract) ; - assert_bool "not (<=)1" (not (AccessPath.( <= ) ~lhs:x_abstract ~rhs:x_exact)) ; - assert_bool "not (<=)2" (not (AccessPath.( <= ) ~lhs:x_abstract ~rhs:xF_exact)) + assert_bool "extract" (AccessPath.equal (AccessPath.Abs.extract xF_exact) xF) ; + assert_bool "is_exact" (AccessPath.Abs.is_exact x_exact) ; + assert_bool "not is_exact" (not (AccessPath.Abs.is_exact x_abstract)) ; + assert_bool "(<=)1" (AccessPath.Abs.( <= ) ~lhs:x_exact ~rhs:x_abstract) ; + assert_bool "(<=)2" (AccessPath.Abs.( <= ) ~lhs:xF_exact ~rhs:x_abstract) ; + assert_bool "not (<=)1" (not (AccessPath.Abs.( <= ) ~lhs:x_abstract ~rhs:x_exact)) ; + assert_bool "not (<=)2" (not (AccessPath.Abs.( <= ) ~lhs:x_abstract ~rhs:xF_exact)) in "abstraction" >:: abstraction_test_ in diff --git a/infer/src/unit/accessTreeTests.ml b/infer/src/unit/accessTreeTests.ml index 03763171f..7caec3ae8 100644 --- a/infer/src/unit/accessTreeTests.ml +++ b/infer/src/unit/accessTreeTests.ml @@ -64,29 +64,29 @@ let tests = let f = make_field_access "f" in let g = make_field_access "g" in let array = make_array_access (Typ.mk Tvoid) in - let x = AccessPath.Exact (make_access_path "x" []) in - let xF = AccessPath.Exact (make_access_path "x" ["f"]) in - let xG = AccessPath.Exact (make_access_path "x" ["g"]) in - let xFG = AccessPath.Exact (make_access_path "x" ["f"; "g"]) in - let y = AccessPath.Exact (make_access_path "y" []) in - let yF = AccessPath.Exact (make_access_path "y" ["f"]) in - let yG = AccessPath.Exact (make_access_path "y" ["g"]) in - let yFG = AccessPath.Exact (make_access_path "y" ["f"; "g"]) in - let z = AccessPath.Exact (make_access_path "z" []) in - let zF = AccessPath.Exact (make_access_path "z" ["f"]) in - let zFG = AccessPath.Exact (make_access_path "z" ["f"; "g"]) in - let xArr = AccessPath.Exact (make_base "x", [array]) in + let x = AccessPath.Abs.Exact (make_access_path "x" []) in + let xF = AccessPath.Abs.Exact (make_access_path "x" ["f"]) in + let xG = AccessPath.Abs.Exact (make_access_path "x" ["g"]) in + let xFG = AccessPath.Abs.Exact (make_access_path "x" ["f"; "g"]) in + let y = AccessPath.Abs.Exact (make_access_path "y" []) in + let yF = AccessPath.Abs.Exact (make_access_path "y" ["f"]) in + let yG = AccessPath.Abs.Exact (make_access_path "y" ["g"]) in + let yFG = AccessPath.Abs.Exact (make_access_path "y" ["f"; "g"]) in + let z = AccessPath.Abs.Exact (make_access_path "z" []) in + let zF = AccessPath.Abs.Exact (make_access_path "z" ["f"]) in + let zFG = AccessPath.Abs.Exact (make_access_path "z" ["f"; "g"]) in + let xArr = AccessPath.Abs.Exact (make_base "x", [array]) in let xArrF = let accesses = [array; make_field_access "f"] in - AccessPath.Exact (make_base "x", accesses) + AccessPath.Abs.Exact (make_base "x", accesses) in - let a_star = AccessPath.Abstracted (make_access_path "a" []) in - let x_star = AccessPath.Abstracted (make_access_path "x" []) in - let xF_star = AccessPath.Abstracted (make_access_path "x" ["f"]) in - let xG_star = AccessPath.Abstracted (make_access_path "x" ["g"]) in - let y_star = AccessPath.Abstracted (make_access_path "y" []) in - let yF_star = AccessPath.Abstracted (make_access_path "y" ["f"]) in - let z_star = AccessPath.Abstracted (make_access_path "z" []) in + let a_star = AccessPath.Abs.Abstracted (make_access_path "a" []) in + let x_star = AccessPath.Abs.Abstracted (make_access_path "x" []) in + let xF_star = AccessPath.Abs.Abstracted (make_access_path "x" ["f"]) in + let xG_star = AccessPath.Abs.Abstracted (make_access_path "x" ["g"]) in + let y_star = AccessPath.Abs.Abstracted (make_access_path "y" []) in + let yF_star = AccessPath.Abs.Abstracted (make_access_path "y" ["f"]) in + let z_star = AccessPath.Abs.Abstracted (make_access_path "z" []) in let x_trace = MockTraceDomain.singleton "x" in let y_trace = MockTraceDomain.singleton "y" in let z_trace = MockTraceDomain.singleton "z" in @@ -386,7 +386,8 @@ let tests = let ap_traces = Domain.trace_fold collect_ap_traces tree [] in let has_ap_trace_pair ap_in trace_in = List.exists - ~f:(fun (ap, trace) -> AccessPath.equal ap ap_in && MockTraceDomain.equal trace trace_in) + ~f:(fun (ap, trace) -> + AccessPath.Abs.equal ap ap_in && MockTraceDomain.equal trace trace_in) ap_traces in assert_bool "Should have six ap/trace pairs" (Int.equal (List.length ap_traces) 6) ;