diff --git a/infer/src/IR/AccessExpression.ml b/infer/src/IR/AccessExpression.ml index b1c9633be..40ca7f821 100644 --- a/infer/src/IR/AccessExpression.ml +++ b/infer/src/IR/AccessExpression.ml @@ -101,34 +101,32 @@ let rec pp fmt = function module Access = struct - type nonrec t = + type 'array_index t = | FieldAccess of Typ.Fieldname.t - | ArrayAccess of typ_ * t list + | ArrayAccess of typ_ * 'array_index | TakeAddress | Dereference [@@deriving compare] - let pp fmt = function + let pp pp_array_index fmt = function | FieldAccess field_name -> Typ.Fieldname.pp fmt field_name - | ArrayAccess (_, []) -> - F.pp_print_string fmt "[_]" - | ArrayAccess (_, index_aps) -> - F.fprintf fmt "[%a]" (PrettyPrintable.pp_collection ~pp_item:pp) index_aps + | ArrayAccess (_, index) -> + F.fprintf fmt "[%a]" pp_array_index index | TakeAddress -> F.pp_print_string fmt "&" | Dereference -> F.pp_print_string fmt "*" end -let to_accesses ae = +let to_accesses ~f_array_offset ae = let rec aux accesses = function | Base base -> (base, accesses) | FieldOffset (ae, fld) -> aux (Access.FieldAccess fld :: accesses) ae - | ArrayOffset (ae, typ, index_aes) -> - aux (Access.ArrayAccess (typ, index_aes) :: accesses) ae + | ArrayOffset (ae, typ, indexes) -> + aux (Access.ArrayAccess (typ, f_array_offset indexes) :: accesses) ae | AddressOf ae -> aux (Access.TakeAddress :: accesses) ae | Dereference ae -> diff --git a/infer/src/IR/AccessExpression.mli b/infer/src/IR/AccessExpression.mli index 1bc6009b2..a0595b851 100644 --- a/infer/src/IR/AccessExpression.mli +++ b/infer/src/IR/AccessExpression.mli @@ -29,17 +29,18 @@ val dereference : t -> t (** guarantees that we never build [Dereference (AddressOf t)] expressions: these become [t] *) module Access : sig - type nonrec t = + type 'array_index t = | FieldAccess of Typ.Fieldname.t - | ArrayAccess of Typ.t * t list + | ArrayAccess of Typ.t * 'array_index | TakeAddress | Dereference [@@deriving compare] - val pp : Format.formatter -> t -> unit + val pp : (Format.formatter -> 'array_index -> unit) -> Format.formatter -> 'array_index t -> unit end -val to_accesses : t -> AccessPath.base * Access.t list +val to_accesses : + f_array_offset:(t list -> 'array_index) -> t -> AccessPath.base * 'array_index Access.t list val to_access_path : t -> AccessPath.t diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml index 4932d107a..91efb956f 100644 --- a/infer/src/checkers/PulseDomain.ml +++ b/infer/src/checkers/PulseDomain.ml @@ -64,7 +64,9 @@ end module Attributes = AbstractDomain.FiniteSet (Attribute) module Memory : sig - module Edges : module type of PrettyPrintable.MakePPMap (AccessExpression.Access) + module Access : PrettyPrintable.PrintableOrderedType with type t = unit AccessExpression.Access.t + + module Edges : PrettyPrintable.PPMap with type key = Access.t type edges = AbstractAddressSet.t Edges.t @@ -82,13 +84,11 @@ module Memory : sig val pp : F.formatter -> t -> unit - val add_edge : AbstractAddress.t -> AccessExpression.Access.t -> AbstractAddressSet.t -> t -> t + val add_edge : AbstractAddress.t -> Access.t -> AbstractAddressSet.t -> t -> t - val add_edge_and_back_edge : - AbstractAddress.t -> AccessExpression.Access.t -> AbstractAddressSet.t -> t -> t + val add_edge_and_back_edge : AbstractAddress.t -> Access.t -> AbstractAddressSet.t -> t -> t - val find_edge_opt : - AbstractAddress.t -> AccessExpression.Access.t -> t -> AbstractAddressSet.t option + val find_edge_opt : AbstractAddress.t -> Access.t -> t -> AbstractAddressSet.t option val add_attributes : AbstractAddress.t -> Attributes.t -> t -> t @@ -101,7 +101,13 @@ module Memory : sig val is_std_vector_reserved : AbstractAddressSet.t -> t -> bool end = struct - module Edges = PrettyPrintable.MakePPMap (AccessExpression.Access) + module Access = struct + type t = unit AccessExpression.Access.t [@@deriving compare] + + let pp = AccessExpression.Access.pp (fun _ () -> ()) + end + + module Edges = PrettyPrintable.MakePPMap (Access) type edges = AbstractAddressSet.t Edges.t @@ -130,7 +136,7 @@ end = struct (** [Dereference] edges induce a [TakeAddress] back edge and vice-versa, because [*(&x) = &( *x ) = x]. *) - let add_edge_and_back_edge addr_src (access : AccessExpression.Access.t) addrs_end memory = + let add_edge_and_back_edge addr_src (access : Access.t) addrs_end memory = let memory = add_edge addr_src access addrs_end memory in match access with | ArrayAccess _ | FieldAccess _ -> @@ -288,9 +294,7 @@ module Domain : AbstractDomain.S with type t = astate = struct let union_one_edge subst src_addr access dst_addr union_heap = let src_addr = to_canonical_address subst src_addr in let dst_addr = to_canonical_address_set subst dst_addr in - match - (Memory.find_edge_opt src_addr access union_heap, (access : AccessExpression.Access.t)) - with + match (Memory.find_edge_opt src_addr access union_heap, (access : Memory.Access.t)) with | Some dst_addr', _ when phys_equal dst_addr dst_addr' -> (* same edge *) (union_heap, `No_new_equality) @@ -577,10 +581,12 @@ module Operations = struct (** add addresses to the state to give a address to the destination of the given access path *) let walk_access_expr ~on_last astate access_expr location = - let (access_var, _), access_list = AccessExpression.to_accesses access_expr in + let (access_var, _), access_list = + AccessExpression.to_accesses ~f_array_offset:(fun _ -> ()) access_expr + in if Config.write_html then L.d_printfln "Accessing %a -> [%a]" Var.pp access_var - (Pp.seq ~sep:"," AccessExpression.Access.pp) + (Pp.seq ~sep:"," Memory.Access.pp) access_list ; match (on_last, access_list) with | `Overwrite new_addr, [] ->