pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[access paths] make raw access paths the default, move abstraction into AccessPath.Abs module

Browse Source 
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
master
Sam Blackshear 8 years ago committed by Facebook Github Bot
parent 25d9f940fe
commit f83284ad7c
27 changed files with 368 additions and 358 deletions
Show Stats Download Patch File Download Diff File

6
infer/src/IR/HilExp.ml
Unescape View File

@ -12,7 +12,7 @@ module F = Format
module L = Logging module L = Logging
type t = type t =
| AccessPath of AccessPath.Raw.t | AccessPath of AccessPath.t
| UnaryOperator of Unop.t * t * Typ.t option | UnaryOperator of Unop.t * t * Typ.t option
| BinaryOperator of Binop.t * t * t | BinaryOperator of Binop.t * t * t
| Exception of t | Exception of t
@ -24,7 +24,7 @@ type t =
let rec pp fmt = function let rec pp fmt = function
| AccessPath access_path | AccessPath access_path
-> AccessPath.Raw.pp fmt access_path -> AccessPath.pp fmt access_path
| UnaryOperator (op, e, _) | UnaryOperator (op, e, _)
-> F.fprintf fmt "%s%a" (Unop.str op) pp e -> F.fprintf fmt "%s%a" (Unop.str op) pp e
| BinaryOperator (op, e1, e2) | BinaryOperator (op, e1, e2)
@ -43,7 +43,7 @@ let rec pp fmt = function
let rec get_typ tenv = function let rec get_typ tenv = function
| AccessPath access_path | AccessPath access_path
-> AccessPath.Raw.get_typ access_path tenv -> AccessPath.get_typ access_path tenv
| UnaryOperator (_, _, typ_opt) | UnaryOperator (_, _, typ_opt)
-> typ_opt -> typ_opt
| BinaryOperator ((Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr), _, _) | BinaryOperator ((Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr), _, _)

6
infer/src/IR/HilExp.mli
Unescape View File

@ -11,7 +11,7 @@ open! IStd
module F = Format module F = Format
type t = 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 | UnaryOperator of Unop.t * t * Typ.t option
(** Unary operator with type of the result if known *) (** Unary operator with type of the result if known *)
| BinaryOperator of Binop.t * t * t (** Binary operator *) | 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 val get_typ : Tenv.t -> t -> Typ.t option
(** Get the type of the expression. Warning: not fully implemented *) (** 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 *) (** 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 (** Get all the access paths used in the given HIL expression, including duplicates if a path is
used more than once. *) used more than once. *)

10
infer/src/IR/HilInstr.ml
Unescape View File

@ -11,23 +11,23 @@ open! IStd
module F = Format module F = Format
module L = Logging 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 let pp_call fmt = function
| Direct pname | Direct pname
-> Typ.Procname.pp fmt pname -> Typ.Procname.pp fmt pname
| Indirect access_path | Indirect access_path
-> F.fprintf fmt "*%a" AccessPath.Raw.pp access_path -> F.fprintf fmt "*%a" AccessPath.pp access_path
type t = 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 | Assume of HilExp.t * [`Then | `Else] * Sil.if_kind * Location.t
| Call of AccessPath.base option * call * HilExp.t list * CallFlags.t * Location.t | Call of AccessPath.base option * call * HilExp.t list * CallFlags.t * Location.t
[@@deriving compare] [@@deriving compare]
let pp fmt = function let pp fmt = function
| Assign (access_path, exp, loc) | 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) | Assume (exp, _, _, loc)
-> F.fprintf fmt "assume %a [%a]" HilExp.pp exp Location.pp loc -> F.fprintf fmt "assume %a [%a]" HilExp.pp exp Location.pp loc
| Call (ret_opt, call, actuals, _, 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 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 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 (* 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 temporary variable to the access path it represents. evaluating the HIL instruction should

8
infer/src/IR/HilInstr.mli
Unescape View File

@ -11,12 +11,12 @@ open! IStd
module F = Format module F = Format
(** type of a procedure call; either direct or via function pointer *) (** 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 val pp_call : F.formatter -> call -> unit
type t = 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 | Assume of HilExp.t * [`Then | `Else] * Sil.if_kind * Location.t
(** Assumed expression, true_branch boolean, source of the assume (conditional, ternary, etc.) *) (** 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 | 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 *) (** Result of translating an SIL instruction *)
type translation = type translation =
| Instr of t (** HIL instruction to execute *) | 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 *) | Unbind of Var.t list (** remove binding from identifier map *)
| Ignore (** no-op *) | 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 *) (** Convert an SIL instruction to an HIL instruction *)

9
infer/src/checkers/IdAccessPathMapDomain.ml
Unescape View File

@ -10,20 +10,19 @@
open! IStd open! IStd
module IdMap = Var.Map module IdMap = Var.Map
type astate = AccessPath.Raw.t IdMap.t type astate = AccessPath.t IdMap.t
include IdMap 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 let check_invariant ap1 ap2 = function
| Var.ProgramVar pvar when Pvar.is_ssa_frontend_tmp pvar | Var.ProgramVar pvar when Pvar.is_ssa_frontend_tmp pvar
-> (* Sawja reuses temporary variables which sometimes breaks this invariant *) -> (* Sawja reuses temporary variables which sometimes breaks this invariant *)
() ()
| id | id
-> if not (AccessPath.Raw.equal ap1 ap2) then -> if not (AccessPath.equal ap1 ap2) then
failwithf "Id %a maps to both %a and %a@." Var.pp id AccessPath.Raw.pp ap1 failwithf "Id %a maps to both %a and %a@." Var.pp id AccessPath.pp ap1 AccessPath.pp ap2
AccessPath.Raw.pp ap2
let ( <= ) ~lhs ~rhs = let ( <= ) ~lhs ~rhs =
if phys_equal lhs rhs then true if phys_equal lhs rhs then true

2
infer/src/checkers/IdAccessPathMapDomain.mli
Unescape View File

@ -13,7 +13,7 @@ open! IStd
module IdMap = Var.Map module IdMap = Var.Map
type astate = AccessPath.Raw.t IdMap.t type astate = AccessPath.t IdMap.t
include module type of IdMap include module type of IdMap

20
infer/src/checkers/NullabilitySuggest.ml
Unescape View File

@ -13,9 +13,9 @@ module MF = MarkupFormatter
module UseDefChain = struct module UseDefChain = struct
type astate = type astate =
| DependsOn of (Location.t * AccessPath.Raw.t) | DependsOn of (Location.t * AccessPath.t)
| NullDefCompare of (Location.t * AccessPath.Raw.t) | NullDefCompare of (Location.t * AccessPath.t)
| NullDefAssign of (Location.t * AccessPath.Raw.t) | NullDefAssign of (Location.t * AccessPath.t)
[@@deriving compare] [@@deriving compare]
let ( <= ) ~lhs ~rhs = compare_astate lhs rhs <= 0 let ( <= ) ~lhs ~rhs = compare_astate lhs rhs <= 0
@ -28,14 +28,14 @@ module UseDefChain = struct
let pp fmt = function let pp fmt = function
| NullDefAssign (loc, ap) | 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) | 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) | 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 end
module Domain = AbstractDomain.Map (AccessPath.Raw) (UseDefChain) module Domain = AbstractDomain.Map (AccessPath) (UseDefChain)
type extras = ProcData.no_extras type extras = ProcData.no_extras
@ -46,7 +46,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
type nonrec extras = extras type nonrec extras = extras
let is_access_nullable ap proc_data = 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) | Some (_, annot_item)
-> Annotations.ia_is_nullable 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 make_error_trace astate ap ud =
let name_of ap = let name_of ap =
match AccessPath.Raw.get_last_access ap with match AccessPath.get_last_access ap with
| Some AccessPath.FieldAccess field_name | Some AccessPath.FieldAccess field_name
-> "Field " ^ Typ.Fieldname.to_flat_string field_name -> "Field " ^ Typ.Fieldname.to_flat_string field_name
| Some AccessPath.ArrayAccess _ | Some AccessPath.ArrayAccess _
@ -147,7 +147,7 @@ let checker {Callbacks.summary; proc_desc; tenv} =
let report astate (proc_data: extras ProcData.t) = let report astate (proc_data: extras ProcData.t) =
let report_access_path ap udchain = let report_access_path ap udchain =
let issue_kind = Localise.to_issue_id Localise.field_should_be_nullable in 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 | Some (field_name, _) when Typ.Fieldname.Java.is_captured_parameter field_name
-> (* Skip reporting when field comes from generated code *) -> (* Skip reporting when field comes from generated code *)
() ()

8
infer/src/checkers/Source.ml
Unescape View File

@ -31,9 +31,9 @@ module type S = sig
val is_footprint : t -> bool 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 val get : CallSite.t -> HilExp.t list -> Tenv.t -> spec option
@ -45,14 +45,14 @@ module Make (Kind : Kind) = struct
type kind = type kind =
| Normal of Kind.t (** known source returned directly or transitively from a callee *) | 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] [@@deriving compare]
let pp_kind fmt = function let pp_kind fmt = function
| Normal kind | Normal kind
-> Kind.pp fmt kind -> Kind.pp fmt kind
| Footprint ap | 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] type t = {kind: kind; site: CallSite.t} [@@deriving compare]

4
infer/src/checkers/Source.mli
Unescape View File

@ -36,10 +36,10 @@ module type S = sig
val is_footprint : t -> bool val is_footprint : t -> bool
(** return true if the current source is a footprint source *) (** 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. *) (** 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 *) (** 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 val get : CallSite.t -> HilExp.t list -> Tenv.t -> spec option

12
infer/src/checkers/ThreadSafety.ml
Unescape View File

@ -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 (* we don't want to warn on accesses to the field if it is (a) thread-confined, or
(b) volatile *) (b) volatile *)
let is_safe_access access prefix_path tenv = 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 | ( AccessPath.FieldAccess fieldname
, Some ({Typ.desc= Tstruct typename} | {desc= Tptr ({desc= Tstruct typename}, _)}) ) -> ( , Some ({Typ.desc= Tstruct typename} | {desc= Tptr ({desc= Tstruct typename}, _)}) ) -> (
match Tenv.lookup tenv typename with 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) AttributeMapDomain.has_attribute access_path Functional astate.attribute_map)
rhs_access_paths 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} | Some {Typ.desc= Typ.Tint ILong | Tfloat FDouble}
-> (* writes to longs and doubles are not guaranteed to be atomic in Java -> (* 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 (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 [var] is set to true. return None if it has free variables that stop us from
evaluating it *) evaluating it *)
and eval_bexp var = function and eval_bexp var = function
| HilExp.AccessPath ap when AccessPath.Raw.equal ap var | HilExp.AccessPath ap when AccessPath.equal ap var
-> Some true -> Some true
| HilExp.Constant c | HilExp.Constant c
-> Some (not (Const.iszero_int_float 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 get_all_accesses = get_all_accesses_with_pre (fun _ -> true)
let pp_container_access fmt (access_path, access_pname) = 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)) (MF.monospaced_to_string (Typ.Procname.get_method access_pname))
let pp_access fmt sink = 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 (* 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 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 *) 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}, _)} | Some {desc= Tptr ({desc= Tstruct tn1}, _)}, Some {desc= Tptr ({desc= Tstruct tn2}, _)}
-> PatternMatch.is_subtype tenv tn1 tn2 || PatternMatch.is_subtype tenv tn2 tn1 -> 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 *) the `this`'s as equal if their types are compatible *)
AccessPath.equal_access_list (snd p1) (snd p2) 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 (* equivalence relation computing whether two access paths may refer to the
same heap location. *) same heap location. *)

21
infer/src/checkers/ThreadSafetyDomain.ml
Unescape View File

@ -12,10 +12,10 @@ module F = Format
module Access = struct module Access = struct
type t = type t =
| Read of AccessPath.Raw.t | Read of AccessPath.t
| Write of AccessPath.Raw.t | Write of AccessPath.t
| ContainerRead of AccessPath.Raw.t * Typ.Procname.t | ContainerRead of AccessPath.t * Typ.Procname.t
| ContainerWrite of AccessPath.Raw.t * Typ.Procname.t | ContainerWrite of AccessPath.t * Typ.Procname.t
| InterfaceCall of Typ.Procname.t | InterfaceCall of Typ.Procname.t
[@@deriving compare] [@@deriving compare]
@ -35,14 +35,13 @@ module Access = struct
let pp fmt = function let pp fmt = function
| Read access_path | 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 | 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) | ContainerRead (access_path, pname)
-> F.fprintf fmt "Read of container %a via %a" AccessPath.Raw.pp access_path Typ.Procname.pp -> F.fprintf fmt "Read of container %a via %a" AccessPath.pp access_path Typ.Procname.pp pname
pname
| ContainerWrite (access_path, 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 pname
| InterfaceCall pname | InterfaceCall pname
-> F.fprintf fmt "Call to un-annotated interface method %a" Typ.Procname.pp 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 AttributeSetDomain = AbstractDomain.InvertedSet (Attribute.Set)
module AttributeMapDomain = struct module AttributeMapDomain = struct
include AbstractDomain.InvertedMap (AccessPath.RawMap) (AttributeSetDomain) include AbstractDomain.InvertedMap (AccessPath.Map) (AttributeSetDomain)
let has_attribute access_path attribute t = let has_attribute access_path attribute t =
try find access_path t |> AttributeSetDomain.mem attribute try find access_path t |> AttributeSetDomain.mem attribute
@ -280,7 +279,7 @@ let empty =
let threads = false in let threads = false in
let locks = false in let locks = false in
let accesses = AccessDomain.empty 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 let escapees = EscapeeDomain.empty in
{thumbs_up; threads; locks; accesses; attribute_map; escapees} {thumbs_up; threads; locks; accesses; attribute_map; escapees}

26
infer/src/checkers/ThreadSafetyDomain.mli
Unescape View File

@ -12,15 +12,15 @@ module F = Format
module Access : sig module Access : sig
type t = type t =
| Read of AccessPath.Raw.t (** Field or array read *) | Read of AccessPath.t (** Field or array read *)
| Write of AccessPath.Raw.t (** Field or array write *) | Write of AccessPath.t (** Field or array write *)
| ContainerRead of AccessPath.Raw.t * Typ.Procname.t (** Read of container object *) | ContainerRead of AccessPath.t * Typ.Procname.t (** Read of container object *)
| ContainerWrite of AccessPath.Raw.t * Typ.Procname.t (** Write to container object *) | ContainerWrite of AccessPath.t * Typ.Procname.t (** Write to container object *)
| InterfaceCall of Typ.Procname.t | InterfaceCall of Typ.Procname.t
(** Call to method of interface not annotated with @ThreadSafe *) (** Call to method of interface not annotated with @ThreadSafe *)
[@@deriving compare] [@@deriving compare]
val get_access_path : t -> AccessPath.Raw.t option val get_access_path : t -> AccessPath.t option
val equal : t -> t -> bool val equal : t -> t -> bool
@ -77,17 +77,17 @@ end
module AttributeSetDomain : module type of AbstractDomain.InvertedSet (Attribute.Set) module AttributeSetDomain : module type of AbstractDomain.InvertedSet (Attribute.Set)
module AttributeMapDomain : sig 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) *) (** 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 *) (** 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 end
(** Excluders: Two things can provide for mutual exclusion: holding a lock, (** 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 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 end
(** set of formals or locals that may escape *) (** set of formals or locals that may escape *)
@ -181,9 +181,9 @@ type summary =
include AbstractDomain.WithBottom with type astate := astate include AbstractDomain.WithBottom with type astate := astate
val make_container_access : 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 val make_unannotated_call_access : Typ.Procname.t -> Location.t -> TraceElem.t

2
infer/src/checkers/Trace.ml
Unescape View File

@ -351,7 +351,7 @@ module Make (Spec : Spec) = struct
let get_footprint_index source = let get_footprint_index source =
match Source.get_footprint_access_path source with match Source.get_footprint_access_path source with
| Some access_path | Some access_path
-> AccessPath.get_footprint_index access_path -> AccessPath.Abs.get_footprint_index access_path
| None | None
-> None -> None

256
infer/src/checkers/accessPath.ml
Unescape View File

@ -10,35 +10,35 @@
open! IStd open! IStd
module F = Format 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. *) 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 let pp_access fmt = function
| FieldAccess field_name | FieldAccess field_name
-> Typ.Fieldname.pp fmt field_name -> Typ.Fieldname.pp fmt field_name
| ArrayAccess _ | ArrayAccess _
-> F.fprintf fmt "[_]" -> F.fprintf fmt "[_]"
let pp_access_list fmt accesses = let pp_access_list fmt accesses =
let pp_sep _ _ = F.fprintf fmt "." in let pp_sep _ _ = F.fprintf fmt "." in
F.pp_print_list ~pp_sep pp_access fmt accesses F.pp_print_list ~pp_sep pp_access fmt accesses
module Raw = struct
type t = base * access list [@@deriving compare] type t = base * access list [@@deriving compare]
let equal = [%compare.equal : t] let equal = [%compare.equal : t]
@ -109,6 +109,72 @@ module Raw = struct
| _ | _
-> None -> 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 let pp fmt = function
| base, [] | base, []
-> pp_base fmt base -> pp_base fmt base
@ -116,112 +182,52 @@ module Raw = struct
-> F.fprintf fmt "%a.%a" pp_base base pp_access_list accesses -> F.fprintf fmt "%a.%a" pp_base base pp_access_list accesses
end end
type t = Abstracted of Raw.t | Exact of Raw.t [@@deriving compare] module Abs = struct
type raw = Raw.t
let equal = [%compare.equal : t]
type t = Abstracted of Raw.t | Exact of Raw.t [@@deriving compare]
let base_of_pvar pvar typ = (Var.of_pvar pvar, typ)
let equal = [%compare.equal : t]
let base_of_id id typ = (Var.of_id id, typ)
let extract = function Exact ap | Abstracted ap -> ap
let of_pvar pvar typ = (base_of_pvar pvar typ, [])
let with_base base = function
let of_id id typ = (base_of_id id typ, []) | Exact (_, accesses)
-> Exact (base, accesses)
let of_exp exp0 typ0 ~(f_resolve_id: Var.t -> Raw.t option) = | Abstracted (_, accesses)
(* [typ] is the type of the last element of the access path (e.g., typeof(g) for x.f.g) *) -> Abstracted (base, accesses)
let rec of_exp_ exp typ accesses acc =
match exp with let to_footprint formal_index access_path =
| Exp.Var id -> ( let _, base_typ = fst (extract access_path) in
match f_resolve_id (Var.of_id id) with with_base (Var.of_formal_index formal_index, base_typ) access_path
| Some (base, base_accesses)
-> (base, base_accesses @ accesses) :: acc let get_footprint_index access_path =
| None let raw_access_path = extract access_path in
-> (base_of_id id typ, accesses) :: acc ) match raw_access_path with
| Exp.Lvar pvar when Pvar.is_ssa_frontend_tmp pvar -> ( | (Var.LogicalVar id, _), _ when Ident.is_footprint id
match f_resolve_id (Var.of_pvar pvar) with -> Some (Ident.get_stamp id)
| Some (base, base_accesses) | _
-> (base, base_accesses @ accesses) :: acc -> None
| None
-> (base_of_pvar pvar typ, accesses) :: acc ) let is_exact = function Exact _ -> true | Abstracted _ -> false
| Exp.Lvar pvar
-> (base_of_pvar pvar typ, accesses) :: acc let ( <= ) ~lhs ~rhs =
| Exp.Lfield (root_exp, fld, root_exp_typ) match (lhs, rhs) with
-> let field_access = FieldAccess fld in | Abstracted _, Exact _
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
| _, []
-> false -> false
| access1 :: p1, access2 :: p2 | Exact lhs_ap, Exact rhs_ap
-> equal_access access1 access2 && is_prefix_path p1 p2 -> Raw.equal lhs_ap rhs_ap
| (Exact lhs_ap | Abstracted lhs_ap), Abstracted rhs_ap
let is_prefix (base1, path1 as ap1) (base2, path2 as ap2) = -> Raw.is_prefix rhs_ap lhs_ap
if phys_equal ap1 ap2 then true else equal_base base1 base2 && is_prefix_path path1 path2
let pp fmt = function
let extract = function Exact ap | Abstracted ap -> ap | Exact access_path
-> Raw.pp fmt access_path
let to_footprint formal_index access_path = | Abstracted access_path
let _, base_typ = fst (extract access_path) in -> F.fprintf fmt "%a*" Raw.pp access_path
with_base (Var.of_formal_index formal_index, base_typ) access_path end
let get_footprint_index access_path = include Raw
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
module BaseMap = PrettyPrintable.MakePPMap (struct module BaseMap = PrettyPrintable.MakePPMap (struct
type t = base type t = base
@ -239,5 +245,5 @@ module AccessMap = PrettyPrintable.MakePPMap (struct
let pp = pp_access let pp = pp_access
end) end)
module RawSet = PrettyPrintable.MakePPSet (Raw) module Set = PrettyPrintable.MakePPSet (Raw)
module RawMap = PrettyPrintable.MakePPMap (Raw) module Map = PrettyPrintable.MakePPMap (Raw)

118
infer/src/checkers/accessPath.mli
Unescape View File

@ -20,101 +20,103 @@ type access =
(* field name *) (* field name *)
[@@deriving compare] [@@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]) *) representedas (x, [f; g]) *)
type t = base * access list [@@deriving compare] type t = base * access list [@@deriving compare]
val truncate : t -> t val truncate : t -> t
(** remove the last access of the access path if the access list is non-empty. returns the (** 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 *) original access path if the access list is empty *)
val get_last_access : t -> access option val get_last_access : t -> access option
(** get the last access in the list. returns None if the list is empty *) (** 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 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 (** 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 *) the list is non-empty and the last access is a field access *)
val get_typ : t -> Tenv.t -> Typ.t option 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 (** 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) *) 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 val base_of_pvar : Pvar.t -> Typ.t -> base
(** create a base from a pvar *) (** create a base from a pvar *)
val base_of_id : Ident.t -> Typ.t -> base val base_of_id : Ident.t -> Typ.t -> base
(** create a base from an ident *) (** 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 *) (** 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 *) (** 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 val of_exp : Exp.t -> Typ.t -> f_resolve_id:(Var.t -> t option) -> t list
(** extract the raw access paths that occur in [exp], resolving identifiers using [f_resolve_id] *) (** extract the 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 to_footprint : int -> t -> t val of_lhs_exp : Exp.t -> Typ.t -> f_resolve_id:(Var.t -> t option) -> t option
(** replace the base var with a footprint variable rooted at formal index [formal_index] *) (** convert [lhs_exp] to an access path, resolving identifiers using [f_resolve_id] *)
val get_footprint_index : t -> int option val append : t -> access list -> t
(** 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
(** append new accesses to an existing access path; e.g., `append_access x.f [g, h]` produces (** append new accesses to an existing access path; e.g., `append_access x.f [g, h]` produces
`x.f.g.h` *) `x.f.g.h` *)
val with_base : base -> t -> t val is_prefix : t -> t -> bool
(** 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
(** return true if [ap1] is a prefix of [ap2]. returns true for equal access paths *) (** 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 : Format.formatter -> access -> unit
val pp_access_list : Format.formatter -> access list -> unit val pp_access_list : Format.formatter -> access list -> unit
val extract : t -> Raw.t module Abs : sig
(** extract a raw access path from its wrapper *) 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 val equal : t -> 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 val to_footprint : int -> t -> t
(** return true if \gamma(lhs) \subseteq \gamma(rhs) *) (** 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 BaseMap : PrettyPrintable.PPMap with type key = base
module AccessMap : PrettyPrintable.PPMap with type key = access 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

18
infer/src/checkers/accessPathDomains.ml
Unescape View File

@ -11,7 +11,7 @@ open! IStd
module F = Format module F = Format
module Set = struct 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" (** TODO (12086310): best-case behavior of some operations can be improved by adding "abstracted"
bool recording whether an abstracted access path has been introduced *) bool recording whether an abstracted access path has been introduced *)
@ -24,7 +24,10 @@ module Set = struct
let normalize aps = let normalize aps =
APSet.filter APSet.filter
(fun lhs -> (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 aps
let add = APSet.add let add = APSet.add
@ -32,11 +35,12 @@ module Set = struct
let of_list = APSet.of_list let of_list = APSet.of_list
let mem ap aps = 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 mem_fuzzy ap aps =
let has_overlap ap1 ap2 = 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 in
APSet.mem ap aps || APSet.exists (has_overlap ap) aps APSet.mem ap aps || APSet.exists (has_overlap ap) aps
@ -53,9 +57,9 @@ module Set = struct
else else
let abstract_access_path ap aps = let abstract_access_path ap aps =
match ap with match ap with
| AccessPath.Exact exact_ap | AccessPath.Abs.Exact exact_ap
-> APSet.add (AccessPath.Abstracted exact_ap) aps -> APSet.add (AccessPath.Abs.Abstracted exact_ap) aps
| AccessPath.Abstracted _ | AccessPath.Abs.Abstracted _
-> APSet.add ap aps -> APSet.add ap aps
in in
let diff_aps = APSet.diff next prev in let diff_aps = APSet.diff next prev in

8
infer/src/checkers/accessPathDomains.mli
Unescape View File

@ -19,17 +19,17 @@ open! IStd
module Set : sig module Set : sig
include AbstractDomain.WithBottom 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). (** return true if \gamma({ap}) \subseteq \gamma(aps).
note: this is worst-case linear in the size of the set *) 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) != {}. (** 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 *) 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 val normalize : astate -> astate
(** simplify an access path set to its canonical representation by eliminating redundancies (** simplify an access path set to its canonical representation by eliminating redundancies

31
infer/src/checkers/accessTree.ml
Unescape View File

@ -34,19 +34,19 @@ module type S = sig
val make_starred_leaf : TraceDomain.astate -> node 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 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 val pp_node : F.formatter -> node -> unit
end end
@ -104,10 +104,10 @@ module Make (TraceDomain : AbstractDomain.WithBottom) = struct
let base_trace, base_tree = BaseMap.find base tree in let base_trace, base_tree = BaseMap.find base tree in
accesses_get_node accesses base_trace base_tree accesses_get_node accesses base_trace base_tree
in in
let base, accesses = AccessPath.extract ap in let base, accesses = AccessPath.Abs.extract ap in
match get_node_ base accesses tree with match get_node_ base accesses tree with
| trace, subtree | trace, subtree
-> if AccessPath.is_exact ap then Some (trace, subtree) -> if AccessPath.Abs.is_exact ap then Some (trace, subtree)
else else
(* input query was [ap]*, and [trace] is the trace associated with [ap]. get the traces (* 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] *) 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 access_tree_add_trace_ ~seen_array_access accesses node
let add_node ap node_to_add tree = let add_node ap node_to_add tree =
let base, accesses = AccessPath.extract ap in let base, accesses = AccessPath.Abs.extract ap in
let is_exact = AccessPath.is_exact ap in let is_exact = AccessPath.Abs.is_exact ap in
let base_node = let base_node =
try BaseMap.find base tree try BaseMap.find base tree
with Not_found -> make_normal_leaf TraceDomain.empty 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 let cur_ap_raw = (base, accesses) in
match tree with match tree with
| Subtree access_map | 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' access_map_fold_ f base accesses access_map acc'
| Star | 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_ 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 let f_ acc ap (trace, _) = f acc ap trace in
fold f_ fold f_

12
infer/src/checkers/accessTree.mli
Unescape View File

@ -50,18 +50,18 @@ module type S = sig
val make_starred_leaf : TraceDomain.astate -> node val make_starred_leaf : TraceDomain.astate -> node
(** create a leaf node with a wildcard successor *) (** 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 *) (** 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 *) (** 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. (** 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 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. *) 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. (** 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 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. *) 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 val node_join : node -> node -> node
(** join two nodes *) (** 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. *) (** 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 val pp_node : Format.formatter -> node -> unit
end end

2
infer/src/quandary/ClangTrace.ml
Unescape View File

@ -222,7 +222,7 @@ include Trace.Make (struct
let is_gflag pvar = let is_gflag pvar =
String.is_substring ~substring:"FLAGS_" (Pvar.get_simplified_name pvar) String.is_substring ~substring:"FLAGS_" (Pvar.get_simplified_name pvar)
in 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 | Some ((Var.ProgramVar pvar, _), _) when Pvar.is_global pvar && is_gflag pvar
-> (* gflags globals come from the environment; treat them as sources *) -> (* gflags globals come from the environment; treat them as sources *)
true true

2
infer/src/quandary/JavaTaintAnalysis.ml
Unescape View File

@ -26,7 +26,7 @@ include TaintAnalysis.Make (struct
let handle_unknown_call pname ret_typ_opt actuals tenv = let handle_unknown_call pname ret_typ_opt actuals tenv =
let get_receiver_typ tenv = function let get_receiver_typ tenv = function
| HilExp.AccessPath access_path | HilExp.AccessPath access_path
-> AccessPath.Raw.get_typ access_path tenv -> AccessPath.get_typ access_path tenv
| _ | _
-> None -> None
in in

45
infer/src/quandary/TaintAnalysis.ml
Unescape View File

@ -48,10 +48,10 @@ module Make (TaintSpecification : TaintSpec.S) = struct
in in
Some (TaintDomain.make_normal_leaf trace) Some (TaintDomain.make_normal_leaf trace)
in 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 match FormalMap.get_formal_index root proc_data.extras.formal_map with
| Some formal_index | 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 | None
-> if Var.is_global (fst root) then make_footprint_trace access_path else 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 exp_get_node_ ~abstracted raw_access_path access_tree proc_data =
let access_path = let access_path =
if abstracted then AccessPath.Abstracted raw_access_path if abstracted then AccessPath.Abs.Abstracted raw_access_path
else AccessPath.Exact raw_access_path else AccessPath.Abs.Exact raw_access_path
in in
access_path_get_node access_path access_tree proc_data 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 add_return_source source ret_base access_tree =
let trace = TraceDomain.of_source source in 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 TaintDomain.add_trace id_ap trace access_tree
let add_actual_source source index actuals access_tree proc_data = let add_actual_source source index actuals access_tree proc_data =
match List.nth_exn actuals index with match List.nth_exn actuals index with
| HilExp.AccessPath actual_ap_raw | 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 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 TaintDomain.add_trace actual_ap (TraceDomain.add_source source trace) access_tree
| _ | _
@ -200,8 +200,8 @@ module Make (TaintSpecification : TaintSpec.S) = struct
| None | None
-> F.fprintf fmt "" -> F.fprintf fmt ""
| Some access_path | Some access_path
-> let base, _ = AccessPath.extract access_path in -> let base, _ = AccessPath.Abs.extract access_path in
F.fprintf fmt " with tainted data %a" AccessPath.pp F.fprintf fmt " with tainted data %a" AccessPath.Abs.pp
( if Var.is_footprint (fst base) then ( if Var.is_footprint (fst base) then
(* TODO: resolve footprint identifier to formal name *) (* TODO: resolve footprint identifier to formal name *)
access_path access_path
@ -241,7 +241,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
match List.nth_exn actuals sink_index with match List.nth_exn actuals sink_index with
| HilExp.AccessPath actual_ap_raw | 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 match access_path_get_node actual_ap access_tree_acc proc_data with
| Some (actual_trace, _) | Some (actual_trace, _)
-> let sink' = -> let sink' =
@ -264,10 +264,10 @@ module Make (TaintSpecification : TaintSpec.S) = struct
let apply_return ret_ap = let apply_return ret_ap =
match ret_opt with match ret_opt with
| Some base_var | Some base_var
-> Some (AccessPath.with_base base_var ret_ap) -> Some (AccessPath.Abs.with_base base_var ret_ap)
| None | None
-> Logging.internal_error "Have summary for retval, but no ret id to bind it to: %a@\n" -> 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 None
in in
let get_actual_ap formal_index = let get_actual_ap formal_index =
@ -276,11 +276,13 @@ module Make (TaintSpecification : TaintSpec.S) = struct
~default:None (List.nth actuals formal_index) ~default:None (List.nth actuals formal_index)
in in
let project ~formal_ap ~actual_ap = let project ~formal_ap ~actual_ap =
let projected_ap = AccessPath.append actual_ap (snd (AccessPath.extract formal_ap)) in let projected_ap =
if AccessPath.is_exact formal_ap then AccessPath.Exact projected_ap AccessPath.append actual_ap (snd (AccessPath.Abs.extract formal_ap))
else AccessPath.Abstracted projected_ap in
if AccessPath.Abs.is_exact formal_ap then AccessPath.Abs.Exact projected_ap
else AccessPath.Abs.Abstracted projected_ap
in in
let base_var, _ = fst (AccessPath.extract formal_ap) in let base_var, _ = fst (AccessPath.Abs.extract formal_ap) in
match base_var with match base_var with
| Var.ProgramVar pvar | Var.ProgramVar pvar
-> if Pvar.is_return pvar then apply_return formal_ap else Some formal_ap -> 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 = let rhs_node =
Option.value (hil_exp_get_node rhs_exp astate proc_data) ~default:TaintDomain.empty_node Option.value (hil_exp_get_node rhs_exp astate proc_data) ~default:TaintDomain.empty_node
in 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 in
match instr with match instr with
| Assign (((Var.ProgramVar pvar, _), []), HilExp.Exception _, _) when Pvar.is_return pvar | 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 match TraceDomain.Source.get_footprint_access_path source with
| Some access_path | Some access_path
-> Option.exists -> 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 ~f:should_taint_typ
| None | None
-> true) -> true)
@ -407,15 +409,16 @@ module Make (TaintSpecification : TaintSpec.S) = struct
| _, [], _ | _, [], _
-> astate_acc -> astate_acc
| TaintSpec.Propagate_to_return, actuals, Some ret_ap | 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 | ( TaintSpec.Propagate_to_receiver
, (AccessPath receiver_ap) :: (_ :: _ as other_actuals) , (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, _, _ -> ( | TaintSpec.Propagate_to_actual actual_index, _, _ -> (
match List.nth actuals actual_index with match List.nth actuals actual_index with
| Some HilExp.AccessPath actual_ap | 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 ) -> astate_acc )
| _ | _
@ -622,7 +625,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
~f:(fun acc (name, typ, taint_opt) -> ~f:(fun acc (name, typ, taint_opt) ->
match taint_opt with match taint_opt with
| Some source | 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 TaintDomain.add_trace base_ap (TraceDomain.of_source source) acc
| None | None
-> acc) -> acc)

2
infer/src/unit/TaintTests.ml
Unescape View File

@ -83,7 +83,7 @@ let tests =
F.fprintf fmt "(%a -> %a)" pp_sources (MockTrace.sources trace) pp_sinks F.fprintf fmt "(%a -> %a)" pp_sources (MockTrace.sources trace) pp_sinks
(MockTrace.sinks trace) (MockTrace.sinks trace)
in 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 *) (* flatten access tree into list of access paths with associated traces *)
let trace_assocs = let trace_assocs =
MockTaintAnalysis.TaintDomain.trace_fold MockTaintAnalysis.TaintDomain.trace_fold

2
infer/src/unit/TraceTests.ml
Unescape View File

@ -114,7 +114,7 @@ let tests =
let append_ _ = let append_ _ =
let call_site = CallSite.dummy in let call_site = CallSite.dummy in
let footprint_ap = 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 in
let dummy_pdesc = let dummy_pdesc =
Cfg.create_proc_desc (Cfg.create_cfg ()) Cfg.create_proc_desc (Cfg.create_cfg ())

2
infer/src/unit/accessPathTestUtils.mli
Unescape View File

@ -19,4 +19,4 @@ val make_field_access : string -> AccessPath.access
val make_array_access : Typ.t -> 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

51
infer/src/unit/accessPathTests.ml
Unescape View File

@ -25,32 +25,28 @@ let tests =
let base = make_base "x" ~typ:dummy_arr_typ in let base = make_base "x" ~typ:dummy_arr_typ in
(base, [make_array_access dummy_typ]) (base, [make_array_access dummy_typ])
in in
let x_exact = AccessPath.Exact x in let x_exact = AccessPath.Abs.Exact x in
let y_exact = AccessPath.Exact y in let y_exact = AccessPath.Abs.Exact y in
let x_abstract = AccessPath.Abstracted x in let x_abstract = AccessPath.Abs.Abstracted x in
let xF_exact = AccessPath.Exact xF in let xF_exact = AccessPath.Abs.Exact xF in
let xFG_exact = AccessPath.Exact xFG in let xFG_exact = AccessPath.Abs.Exact xFG in
let yF_exact = AccessPath.Exact yF in let yF_exact = AccessPath.Abs.Exact yF in
let yF_abstract = AccessPath.Abstracted yF in let yF_abstract = AccessPath.Abs.Abstracted yF in
let open OUnit2 in let open OUnit2 in
let equal_test = let equal_test =
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 bases" (AccessPath.equal x (make_access_path "x" [])) ;
assert_bool "equal works for paths" assert_bool "equal works for paths" (AccessPath.equal xFG (make_access_path "x" ["f"; "g"])) ;
(AccessPath.Raw.equal xFG (make_access_path "x" ["f"; "g"])) ; assert_bool "disequality works for bases" (not (AccessPath.equal x y)) ;
assert_bool "disequality works for bases" (not (AccessPath.Raw.equal x y)) ; assert_bool "disequality works for paths" (not (AccessPath.equal xF xFG))
assert_bool "disequality works for paths" (not (AccessPath.Raw.equal xF xFG))
in in
"equal" >:: equal_test_ "equal" >:: equal_test_
in in
let append_test = let append_test =
let pp_diff fmt (actual, expected) = let pp_diff fmt (actual, expected) =
F.fprintf fmt "Expected output %a but got %a" AccessPath.Raw.pp expected AccessPath.Raw.pp F.fprintf fmt "Expected output %a but got %a" AccessPath.pp expected AccessPath.pp actual
actual
in
let assert_eq input expected =
assert_equal ~cmp:AccessPath.Raw.equal ~pp_diff input expected
in in
let assert_eq input expected = assert_equal ~cmp:AccessPath.equal ~pp_diff input expected in
let append_test_ _ = let append_test_ _ =
assert_eq xF (AccessPath.append x [f_access]) ; assert_eq xF (AccessPath.append x [f_access]) ;
assert_eq xFG (AccessPath.append xF [g_access]) assert_eq xFG (AccessPath.append xF [g_access])
@ -85,9 +81,9 @@ let tests =
let actual_ap = make_ap exp in let actual_ap = make_ap exp in
let pp_diff fmt (actual_ap, expected_ap) = let pp_diff fmt (actual_ap, expected_ap) =
F.fprintf fmt "Expected to make access path %a from expression %a, but got %a" 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 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 in
let of_exp_test_ _ = let of_exp_test_ _ =
let f_fieldname = make_fieldname "f" in let f_fieldname = make_fieldname "f" in
@ -111,8 +107,7 @@ let tests =
let binop_exp = Exp.le xF_exp xFG_exp in let binop_exp = Exp.le xF_exp xFG_exp in
match AccessPath.of_exp binop_exp dummy_typ ~f_resolve_id with match AccessPath.of_exp binop_exp dummy_typ ~f_resolve_id with
| [ap1; ap2] | [ap1; ap2]
-> assert_equal ~cmp:AccessPath.Raw.equal ap1 xFG ; -> assert_equal ~cmp:AccessPath.equal ap1 xFG ; assert_equal ~cmp:AccessPath.equal ap2 xF
assert_equal ~cmp:AccessPath.Raw.equal ap2 xF
| _ | _
-> assert false -> assert false
in in
@ -120,13 +115,13 @@ let tests =
in in
let abstraction_test = let abstraction_test =
let abstraction_test_ _ = let abstraction_test_ _ =
assert_bool "extract" (AccessPath.Raw.equal (AccessPath.extract xF_exact) xF) ; assert_bool "extract" (AccessPath.equal (AccessPath.Abs.extract xF_exact) xF) ;
assert_bool "is_exact" (AccessPath.is_exact x_exact) ; assert_bool "is_exact" (AccessPath.Abs.is_exact x_exact) ;
assert_bool "not is_exact" (not (AccessPath.is_exact x_abstract)) ; assert_bool "not is_exact" (not (AccessPath.Abs.is_exact x_abstract)) ;
assert_bool "(<=)1" (AccessPath.( <= ) ~lhs:x_exact ~rhs:x_abstract) ; assert_bool "(<=)1" (AccessPath.Abs.( <= ) ~lhs:x_exact ~rhs:x_abstract) ;
assert_bool "(<=)2" (AccessPath.( <= ) ~lhs:xF_exact ~rhs:x_abstract) ; assert_bool "(<=)2" (AccessPath.Abs.( <= ) ~lhs:xF_exact ~rhs:x_abstract) ;
assert_bool "not (<=)1" (not (AccessPath.( <= ) ~lhs:x_abstract ~rhs:x_exact)) ; assert_bool "not (<=)1" (not (AccessPath.Abs.( <= ) ~lhs:x_abstract ~rhs:x_exact)) ;
assert_bool "not (<=)2" (not (AccessPath.( <= ) ~lhs:x_abstract ~rhs:xF_exact)) assert_bool "not (<=)2" (not (AccessPath.Abs.( <= ) ~lhs:x_abstract ~rhs:xF_exact))
in in
"abstraction" >:: abstraction_test_ "abstraction" >:: abstraction_test_
in in

43
infer/src/unit/accessTreeTests.ml
Unescape View File

@ -64,29 +64,29 @@ let tests =
let f = make_field_access "f" in let f = make_field_access "f" in
let g = make_field_access "g" in let g = make_field_access "g" in
let array = make_array_access (Typ.mk Tvoid) in let array = make_array_access (Typ.mk Tvoid) in
let x = AccessPath.Exact (make_access_path "x" []) in let x = AccessPath.Abs.Exact (make_access_path "x" []) in
let xF = AccessPath.Exact (make_access_path "x" ["f"]) in let xF = AccessPath.Abs.Exact (make_access_path "x" ["f"]) in
let xG = AccessPath.Exact (make_access_path "x" ["g"]) in let xG = AccessPath.Abs.Exact (make_access_path "x" ["g"]) in
let xFG = AccessPath.Exact (make_access_path "x" ["f"; "g"]) in let xFG = AccessPath.Abs.Exact (make_access_path "x" ["f"; "g"]) in
let y = AccessPath.Exact (make_access_path "y" []) in let y = AccessPath.Abs.Exact (make_access_path "y" []) in
let yF = AccessPath.Exact (make_access_path "y" ["f"]) in let yF = AccessPath.Abs.Exact (make_access_path "y" ["f"]) in
let yG = AccessPath.Exact (make_access_path "y" ["g"]) in let yG = AccessPath.Abs.Exact (make_access_path "y" ["g"]) in
let yFG = AccessPath.Exact (make_access_path "y" ["f"; "g"]) in let yFG = AccessPath.Abs.Exact (make_access_path "y" ["f"; "g"]) in
let z = AccessPath.Exact (make_access_path "z" []) in let z = AccessPath.Abs.Exact (make_access_path "z" []) in
let zF = AccessPath.Exact (make_access_path "z" ["f"]) in let zF = AccessPath.Abs.Exact (make_access_path "z" ["f"]) in
let zFG = AccessPath.Exact (make_access_path "z" ["f"; "g"]) in let zFG = AccessPath.Abs.Exact (make_access_path "z" ["f"; "g"]) in
let xArr = AccessPath.Exact (make_base "x", [array]) in let xArr = AccessPath.Abs.Exact (make_base "x", [array]) in
let xArrF = let xArrF =
let accesses = [array; make_field_access "f"] in let accesses = [array; make_field_access "f"] in
AccessPath.Exact (make_base "x", accesses) AccessPath.Abs.Exact (make_base "x", accesses)
in in
let a_star = AccessPath.Abstracted (make_access_path "a" []) in let a_star = AccessPath.Abs.Abstracted (make_access_path "a" []) in
let x_star = AccessPath.Abstracted (make_access_path "x" []) in let x_star = AccessPath.Abs.Abstracted (make_access_path "x" []) in
let xF_star = AccessPath.Abstracted (make_access_path "x" ["f"]) in let xF_star = AccessPath.Abs.Abstracted (make_access_path "x" ["f"]) in
let xG_star = AccessPath.Abstracted (make_access_path "x" ["g"]) in let xG_star = AccessPath.Abs.Abstracted (make_access_path "x" ["g"]) in
let y_star = AccessPath.Abstracted (make_access_path "y" []) in let y_star = AccessPath.Abs.Abstracted (make_access_path "y" []) in
let yF_star = AccessPath.Abstracted (make_access_path "y" ["f"]) in let yF_star = AccessPath.Abs.Abstracted (make_access_path "y" ["f"]) in
let z_star = AccessPath.Abstracted (make_access_path "z" []) in let z_star = AccessPath.Abs.Abstracted (make_access_path "z" []) in
let x_trace = MockTraceDomain.singleton "x" in let x_trace = MockTraceDomain.singleton "x" in
let y_trace = MockTraceDomain.singleton "y" in let y_trace = MockTraceDomain.singleton "y" in
let z_trace = MockTraceDomain.singleton "z" 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 ap_traces = Domain.trace_fold collect_ap_traces tree [] in
let has_ap_trace_pair ap_in trace_in = let has_ap_trace_pair ap_in trace_in =
List.exists 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 ap_traces
in in
assert_bool "Should have six ap/trace pairs" (Int.equal (List.length ap_traces) 6) ; assert_bool "Should have six ap/trace pairs" (Int.equal (List.length ap_traces) 6) ;

Write Preview
Loading…
Cancel
Save