[HIL][1/4] make `Access.t` polymorphic in the array access

Summary:
This will be useful for proper support of array indexes in pulse and in
HIL in general.

Reviewed By: mbouaziz

Differential Revision: D13377642

fbshipit-source-id: e431121fb

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 ->

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
 

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, [] ->