[access paths] optional index expression for arrays

Summary:
Record the list of access paths (if any) used in the index expression for each array access.
This will make it possible to use array accesses as sinks in Quandary

Reviewed By: jeremydubreil

Differential Revision: D5531356

fbshipit-source-id: 8204909

infer/src/IR/HilExp.ml

@@ -99,7 +99,8 @@ let get_access_paths exp0 =
    temporary variable to the access path it represents. evaluating the HIL expression should
    produce the same result as evaluating the SIL expression and replacing the temporary variables
    using [f_resolve_id] *)
-let rec of_sil ~f_resolve_id (exp: Exp.t) typ =
+let of_sil ~include_array_indexes ~f_resolve_id exp typ =
+  let rec of_sil_ (exp: Exp.t) typ =
     match exp with
     | Var id
      -> let ap =
@@ -111,32 +112,31 @@ let rec of_sil ~f_resolve_id (exp: Exp.t) typ =
         in
         AccessPath ap
     | UnOp (op, e, typ_opt)
-   -> UnaryOperator (op, of_sil ~f_resolve_id e typ, typ_opt)
+     -> UnaryOperator (op, of_sil_ e typ, typ_opt)
     | BinOp (op, e0, e1)
-   -> BinaryOperator (op, of_sil ~f_resolve_id e0 typ, of_sil ~f_resolve_id e1 typ)
+     -> BinaryOperator (op, of_sil_ e0 typ, of_sil_ e1 typ)
     | Exn e
-   -> Exception (of_sil ~f_resolve_id e typ)
+     -> Exception (of_sil_ e typ)
     | Const c
      -> Constant c
     | Cast (cast_typ, e)
-   -> Cast (cast_typ, of_sil ~f_resolve_id e typ)
+     -> Cast (cast_typ, of_sil_ e typ)
     | Sizeof {typ; dynamic_length}
-   -> Sizeof (typ, Option.map ~f:(fun e -> of_sil ~f_resolve_id e typ) dynamic_length)
+     -> Sizeof (typ, Option.map ~f:(fun e -> of_sil_ e typ) dynamic_length)
     | Closure closure
      -> let environment =
           List.map
-          ~f:(fun (value, pvar, typ) ->
-            (AccessPath.base_of_pvar pvar typ, of_sil ~f_resolve_id value typ))
+            ~f:(fun (value, pvar, typ) -> (AccessPath.base_of_pvar pvar typ, of_sil_ value typ))
             closure.captured_vars
         in
         Closure (closure.name, environment)
     | Lfield (root_exp, fld, root_exp_typ) -> (
-    match AccessPath.of_lhs_exp exp typ ~f_resolve_id with
+      match AccessPath.of_lhs_exp ~include_array_indexes exp typ ~f_resolve_id with
       | Some access_path
        -> AccessPath access_path
       | None
        -> (* unsupported field expression: represent with a dummy variable *)
-        of_sil ~f_resolve_id
+          of_sil_
             (Exp.Lfield
                ( Var (Ident.create_normal (Ident.string_to_name (Exp.to_string root_exp)) 0)
                , fld
@@ -146,23 +146,24 @@ let rec of_sil ~f_resolve_id (exp: Exp.t) typ =
          for the string literal. if you actually need to see the value of the string literal in the
          analysis, you should probably be using SIL. this is unsound if the code modifies the
          literal, e.g. using `const_cast<char*>` *)
-      of_sil ~f_resolve_id
-        (Exp.Lindex (Var (Ident.create_normal (Ident.string_to_name s) 0), index_exp)) typ
+        of_sil_ (Exp.Lindex (Var (Ident.create_normal (Ident.string_to_name s) 0), index_exp)) typ
     | Lindex (root_exp, index_exp) -> (
-    match AccessPath.of_lhs_exp exp typ ~f_resolve_id with
+      match AccessPath.of_lhs_exp ~include_array_indexes exp typ ~f_resolve_id with
       | Some access_path
        -> AccessPath access_path
       | None
        -> (* unsupported index expression: represent with a dummy variable *)
-        of_sil ~f_resolve_id
+          of_sil_
             (Exp.Lindex
                ( Var (Ident.create_normal (Ident.string_to_name (Exp.to_string root_exp)) 0)
                , index_exp )) typ )
     | Lvar _ ->
-    match AccessPath.of_lhs_exp exp typ ~f_resolve_id with
+      match AccessPath.of_lhs_exp ~include_array_indexes exp typ ~f_resolve_id with
       | Some access_path
        -> AccessPath access_path
       | None
        -> failwithf "Couldn't convert var expression %a to access path" Exp.pp exp
+  in
+  of_sil_ exp typ
 
 let is_null_literal = function Constant Cint n -> IntLit.isnull n | _ -> false

infer/src/IR/HilExp.mli

@@ -29,7 +29,8 @@ 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.t option) -> Exp.t -> Typ.t -> t
+val of_sil :
+  include_array_indexes:bool -> 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.t list

infer/src/IR/HilInstr.ml

@@ -41,9 +41,10 @@ type translation = Instr of t | Bind of Var.t * AccessPath.t | Unbind of Var.t l
    temporary variable to the access path it represents. evaluating the HIL instruction should
    produce the same result as evaluating the SIL instruction and replacing the temporary variables
    using [f_resolve_id]. *)
-let of_sil ~f_resolve_id (instr: Sil.instr) =
+let of_sil ~include_array_indexes ~f_resolve_id (instr: Sil.instr) =
+  let exp_of_sil = HilExp.of_sil ~include_array_indexes ~f_resolve_id in
   let analyze_id_assignment lhs_id rhs_exp rhs_typ loc =
-    let rhs_hil_exp = HilExp.of_sil ~f_resolve_id rhs_exp rhs_typ in
+    let rhs_hil_exp = exp_of_sil rhs_exp rhs_typ in
     match HilExp.get_access_paths rhs_hil_exp with
     | [rhs_access_path]
      -> Bind (lhs_id, rhs_access_path)
@@ -65,7 +66,7 @@ let of_sil ~f_resolve_id (instr: Sil.instr) =
    -> analyze_id_assignment (Var.of_id ret_id) target_exp cast_typ loc
   | Store (lhs_exp, typ, rhs_exp, loc)
    -> let lhs_access_path =
-        match HilExp.of_sil ~f_resolve_id lhs_exp typ with
+        match exp_of_sil lhs_exp typ with
         | AccessPath ap
          -> ap
         | BinaryOperator (_, exp0, exp1) -> (
@@ -88,11 +89,11 @@ let of_sil ~f_resolve_id (instr: Sil.instr) =
         | _
          -> invalid_argf "Non-assignable LHS expression %a" Exp.pp lhs_exp
       in
-      Instr (Assign (lhs_access_path, HilExp.of_sil ~f_resolve_id rhs_exp typ, loc))
+      Instr (Assign (lhs_access_path, exp_of_sil rhs_exp typ, loc))
   | Call (ret_opt, call_exp, formals, loc, call_flags)
    -> let hil_ret = Option.map ~f:(fun (ret_id, ret_typ) -> (Var.of_id ret_id, ret_typ)) ret_opt in
       let hil_call =
-        match HilExp.of_sil ~f_resolve_id call_exp (Typ.mk Tvoid) with
+        match exp_of_sil call_exp (Typ.mk Tvoid) with
         | Constant Cfun procname
          -> Direct procname
         | AccessPath access_path
@@ -100,10 +101,10 @@ let of_sil ~f_resolve_id (instr: Sil.instr) =
         | call_exp
          -> invalid_argf "Unexpected call expression %a" HilExp.pp call_exp
       in
-      let formals = List.map ~f:(fun (exp, typ) -> HilExp.of_sil ~f_resolve_id exp typ) formals in
+      let formals = List.map ~f:(fun (exp, typ) -> exp_of_sil exp typ) formals in
       Instr (Call (hil_ret, hil_call, formals, call_flags, loc))
   | Prune (exp, loc, true_branch, if_kind)
-   -> let hil_exp = HilExp.of_sil ~f_resolve_id exp (Typ.mk (Tint IBool)) in
+   -> let hil_exp = exp_of_sil exp (Typ.mk (Tint IBool)) in
       let branch = if true_branch then `Then else `Else in
       Instr (Assume (hil_exp, branch, if_kind, loc))
   | Nullify (pvar, _)

infer/src/IR/HilInstr.mli

@@ -32,5 +32,7 @@ type translation =
   | Unbind of Var.t list  (** remove binding from identifier map *)
   | Ignore  (** no-op *)
 
-val of_sil : f_resolve_id:(Var.t -> AccessPath.t option) -> Sil.instr -> translation
+val of_sil :
+  include_array_indexes:bool -> f_resolve_id:(Var.t -> AccessPath.t option) -> Sil.instr
+  -> translation
 (** Convert an SIL instruction to an HIL instruction *)

infer/src/absint/LowerHil.ml

@@ -10,7 +10,19 @@
 open! IStd
 module L = Logging
 
-module Make (MakeTransferFunctions : TransferFunctions.MakeHIL) (CFG : ProcCfg.S) = struct
+module type HilConfig = sig
+  val include_array_indexes : bool
+end
+
+module DefaultConfig : HilConfig = struct
+  let include_array_indexes = false
+end
+
+module Make
+    (MakeTransferFunctions : TransferFunctions.MakeHIL)
+    (HilConfig : HilConfig)
+    (CFG : ProcCfg.S) =
+struct
   module TransferFunctions = MakeTransferFunctions (CFG)
   module CFG = TransferFunctions.CFG
   module Domain = AbstractDomain.Pair (TransferFunctions.Domain) (IdAccessPathMapDomain)
@@ -22,7 +34,9 @@ module Make (MakeTransferFunctions : TransferFunctions.MakeHIL) (CFG : ProcCfg.S
       try Some (IdAccessPathMapDomain.find id id_map)
       with Not_found -> None
     in
-    match HilInstr.of_sil ~f_resolve_id instr with
+    match
+      HilInstr.of_sil ~include_array_indexes:HilConfig.include_array_indexes ~f_resolve_id instr
+    with
     | Bind (id, access_path)
      -> let id_map' = IdAccessPathMapDomain.add id access_path id_map in
         if phys_equal id_map id_map' then astate else (actual_state, id_map')
@@ -44,3 +58,6 @@ module Make (MakeTransferFunctions : TransferFunctions.MakeHIL) (CFG : ProcCfg.S
     | Ignore
      -> astate
 end
+
+module MakeDefault (MakeTransferFunctions : TransferFunctions.MakeHIL) (CFG : ProcCfg.S) =
+  Make (MakeTransferFunctions) (DefaultConfig) (CFG)

infer/src/absint/LowerHil.mli

@@ -9,8 +9,18 @@
 
 open! IStd
 
+module type HilConfig = sig
+  val include_array_indexes : bool
+  (** if true, array index expressions will appear in access paths *)
+end
+
+module DefaultConfig : HilConfig
+
 (** Functor for turning HIL transfer functions into SIL transfer functions *)
-module Make (MakeTransferFunctions : TransferFunctions.MakeHIL) (CFG : ProcCfg.S) : sig
+module Make
+    (MakeTransferFunctions : TransferFunctions.MakeHIL)
+    (HilConfig : HilConfig)
+    (CFG : ProcCfg.S) : sig
   module TransferFunctions : module type of MakeTransferFunctions (CFG)
 
   module CFG : module type of TransferFunctions.CFG
@@ -22,3 +32,7 @@ module Make (MakeTransferFunctions : TransferFunctions.MakeHIL) (CFG : ProcCfg.S
 
   val exec_instr : Domain.astate -> extras ProcData.t -> CFG.node -> Sil.instr -> Domain.astate
 end
+
+module MakeDefault (MakeTransferFunctions : TransferFunctions.MakeHIL) (CFG : ProcCfg.S) : sig
+  include module type of Make (MakeTransferFunctions) (DefaultConfig) (CFG)
+end

infer/src/checkers/NullabilitySuggest.ml

@@ -99,7 +99,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         else astate
 end
 
-module Analyzer = AbstractInterpreter.Make (ProcCfg.Exceptional) (LowerHil.Make (TransferFunctions))
+module Analyzer =
+  AbstractInterpreter.Make (ProcCfg.Exceptional) (LowerHil.MakeDefault (TransferFunctions))
 
 let make_error_trace astate ap ud =
   let name_of ap =

infer/src/checkers/ThreadSafety.ml

@@ -861,7 +861,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
        -> astate
 end
 
-module Analyzer = AbstractInterpreter.Make (ProcCfg.Normal) (LowerHil.Make (TransferFunctions))
+module Analyzer =
+  AbstractInterpreter.Make (ProcCfg.Normal) (LowerHil.MakeDefault (TransferFunctions))
 
 (* similarly, we assume that immutable classes safely encapsulate their state *)
 let is_immutable_collection_class class_name tenv =
@@ -1480,12 +1481,12 @@ let may_alias tenv p1 p2 =
   | FieldAccess f1, FieldAccess f2
    -> Typ.Fieldname.equal f1 f2
   (* if arrays of objects that have an inheritance rel then they can alias *)
-  | ( ArrayAccess {desc= Tptr ({desc= Tstruct tn1}, _)}
-    , ArrayAccess {desc= Tptr ({desc= Tstruct tn2}, _)} )
+  | ( ArrayAccess ({desc= Tptr ({desc= Tstruct tn1}, _)}, _)
+    , ArrayAccess ({desc= Tptr ({desc= Tstruct tn2}, _)}, _) )
    -> if sound then PatternMatch.is_subtype tenv tn1 tn2 || PatternMatch.is_subtype tenv tn2 tn1
       else may_alias_container tenv p1 p2
   (* primitive type arrays can alias if the prim. type is the same *)
-  | ArrayAccess t1, ArrayAccess t2
+  | ArrayAccess (t1, _), ArrayAccess (t2, _)
    -> if sound then equal_desc t1.desc t2.desc else may_alias_container tenv p1 p2
 
 (* take a results table and quotient it by the may_alias relation *)

infer/src/checkers/accessPath.ml

@@ -21,7 +21,9 @@ module Raw = struct
 
   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 * t list | FieldAccess of Typ.Fieldname.t
+
+  and t = (base * access list) [@@deriving compare]
 
   let equal_access = [%compare.equal : access]
 
@@ -29,17 +31,23 @@ module Raw = struct
 
   let pp_base fmt (pvar, _) = Var.pp fmt pvar
 
-  let pp_access fmt = function
+  let rec pp_access fmt = function
     | FieldAccess field_name
      -> Typ.Fieldname.pp fmt field_name
-    | ArrayAccess _
+    | ArrayAccess (_, [])
      -> F.fprintf fmt "[_]"
+    | ArrayAccess (_, index_aps)
+     -> F.fprintf fmt "[%a]" (PrettyPrintable.pp_collection ~pp_item:pp) index_aps
 
-  let pp_access_list fmt accesses =
+  and pp_access_list fmt accesses =
     let pp_sep _ _ = F.fprintf fmt "." in
     F.pp_print_list ~pp_sep pp_access fmt accesses
 
-  type t = base * access list [@@deriving compare]
+  and pp fmt = function
+    | base, []
+     -> pp_base fmt base
+    | base, accesses
+     -> F.fprintf fmt "%a.%a" pp_base base pp_access_list accesses
 
   let equal = [%compare.equal : t]
 
@@ -57,7 +65,7 @@ module Raw = struct
   let get_access_type tenv base_typ = function
     | FieldAccess field_name
      -> Option.map (lookup_field_type_annot tenv base_typ field_name) ~f:fst
-    | ArrayAccess array_typ
+    | ArrayAccess (array_typ, _)
      -> Some array_typ
 
   (* For field access, get the field name and the annotation associated with it
@@ -117,7 +125,7 @@ module Raw = struct
 
   let of_id id typ = (base_of_id id typ, [])
 
-  let of_exp exp0 typ0 ~(f_resolve_id: Var.t -> t option) =
+  let of_exp ~include_array_indexes 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
@@ -138,8 +146,11 @@ module Raw = struct
       | 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
+      | Exp.Lindex (root_exp, index_exp)
+       -> let index_access_paths =
+            if include_array_indexes then of_exp_ index_exp typ [] [] else []
+          in
+          let array_access = ArrayAccess (typ, index_access_paths) 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)
@@ -156,8 +167,12 @@ module Raw = struct
     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 of_lhs_exp ~include_array_indexes lhs_exp typ ~(f_resolve_id: Var.t -> t option) =
+    match of_exp ~include_array_indexes 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)
 
@@ -174,12 +189,6 @@ module Raw = struct
 
   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
-    | base, accesses
-     -> F.fprintf fmt "%a.%a" pp_base base pp_access_list accesses
 end
 
 module Abs = struct

infer/src/checkers/accessPath.mli

@@ -14,15 +14,13 @@ open! IStd
 type base = Var.t * Typ.t [@@deriving compare]
 
 type access =
-  | ArrayAccess of Typ.t
-  (* array element type. index is unknown *)
-  | FieldAccess of Typ.Fieldname.t
-  (* field name *)
+  | ArrayAccess of Typ.t * t list  (** array element type with list of access paths in index *)
+  | FieldAccess of Typ.Fieldname.t  (** field name *)
   [@@deriving compare]
 
 (** 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]
+and 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
@@ -51,10 +49,12 @@ val of_pvar : Pvar.t -> Typ.t -> 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 -> t option) -> t list
-(** extract the access paths that occur in [exp], resolving identifiers using [f_resolve_id] *)
+val of_exp :
+  include_array_indexes:bool -> 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]. don't include index expressions in array accesses if [include_array_indexes] is false *)
 
-val of_lhs_exp : Exp.t -> Typ.t -> f_resolve_id:(Var.t -> t option) -> t option
+val of_lhs_exp :
+  include_array_indexes:bool -> 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 append : t -> access list -> t

infer/src/labs/ResourceLeaks.ml

@@ -96,7 +96,7 @@ module Analyzer =
        ignore them *)
     (ProcCfg.Normal)
     (* 5(a) *)
-    (LowerHil.Make (TransferFunctions))
+    (LowerHil.Make (TransferFunctions) (LowerHil.DefaultConfig))
 
 (* Callback for invoking the checker from the outside--registered in RegisterCheckers *)
 let checker {Callbacks.summary; proc_desc; tenv} : Specs.summary =

infer/src/quandary/TaintAnalysis.ml

@@ -539,7 +539,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
   end
 
   module Analyzer =
-    AbstractInterpreter.Make (ProcCfg.Exceptional) (LowerHil.Make (TransferFunctions))
+    AbstractInterpreter.Make (ProcCfg.Exceptional) (LowerHil.MakeDefault (TransferFunctions))
 
   let make_summary {ProcData.pdesc; extras= {formal_map}} access_tree =
     let is_java = Typ.Procname.is_java (Procdesc.get_proc_name pdesc) in

infer/src/unit/TaintTests.ml

@@ -56,7 +56,7 @@ module MockTaintAnalysis = TaintAnalysis.Make (struct
 end)
 
 module TestInterpreter =
-  AnalyzerTester.Make (ProcCfg.Normal) (LowerHil.Make (MockTaintAnalysis.TransferFunctions))
+  AnalyzerTester.Make (ProcCfg.Normal) (LowerHil.MakeDefault (MockTaintAnalysis.TransferFunctions))
 
 let tests =
   let open OUnit2 in

infer/src/unit/accessPathTestUtils.ml

@@ -17,7 +17,7 @@ let make_fieldname = Typ.Fieldname.Java.from_string
 
 let make_field_access access_str = AccessPath.FieldAccess (make_fieldname access_str)
 
-let make_array_access typ = AccessPath.ArrayAccess typ
+let make_array_access typ = AccessPath.ArrayAccess (typ, [])
 
 let make_access_path base_str access_strs =
   (make_base base_str, List.map ~f:make_field_access access_strs)

infer/src/unit/accessPathTests.ml

@@ -72,7 +72,7 @@ let tests =
     let dummy_typ = Typ.mk Tvoid in
     let check_make_ap exp expected_ap ~f_resolve_id =
       let make_ap exp =
-        match AccessPath.of_lhs_exp exp dummy_typ ~f_resolve_id with
+        match AccessPath.of_lhs_exp ~include_array_indexes:true exp dummy_typ ~f_resolve_id with
         | Some ap
          -> ap
         | None
@@ -105,7 +105,7 @@ let tests =
       check_make_ap xFG_exp_with_id xFG ~f_resolve_id:f_resolve_id_to_xF ;
       (* make sure we can grab access paths from compound expressions *)
       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 ~include_array_indexes:true binop_exp dummy_typ ~f_resolve_id with
       | [ap1; ap2]
        -> assert_equal ~cmp:AccessPath.equal ap1 xFG ; assert_equal ~cmp:AccessPath.equal ap2 xF
       | _