[pulse] Add naive model for array length in Java

Summary:
Model array length in Java as returning an unknown interval [0, +inf] for now.

Ideally, we can deal with the size in a more precise manner in the future like in InferBo.

Reviewed By: skcho

Differential Revision: D19312123

fbshipit-source-id: 8c51059a4

infer/src/bufferoverrun/itv.mli

@@ -29,6 +29,8 @@ module ItvPure : sig
 
   val zero : t
 
+  val nat : t
+
   val of_int : int -> t
 
   val lb : t -> Bound.t

infer/src/pulse/PulseArithmetic.ml

@@ -416,6 +416,8 @@ let abduce_binop_constraints ~negated (bop : Binop.t) (a1 : t) (a2 : t) =
       Satisfiable (None, None)
 
 
+let zero_inf = between (Int IntLit.zero) PlusInfinity
+
 let abduce_binop_is_true ~negated bop v1 v2 =
   Logging.d_printfln "abduce_binop_is_true ~negated:%b %s (%a) (%a)" negated (Binop.str Pp.text bop)
     (Pp.option pp) v1 (Pp.option pp) v2 ;

infer/src/pulse/PulseArithmetic.mli

@@ -35,3 +35,5 @@ val abduce_binop_is_true : negated:bool -> Binop.t -> t option -> t option -> ab
 val binop : Binop.t -> t -> t -> t option
 
 val unop : Unop.t -> t -> t option
+
+val zero_inf : t

infer/src/pulse/PulseModels.ml

@@ -48,6 +48,17 @@ module Misc = struct
     Ok [PulseOperations.write_id ret_id (ret_addr, []) astate]
 
 
+  let return_unknown_size : model =
+   fun ~caller_summary:_ location ~ret:(ret_id, _) astate ->
+    let ret_addr = AbstractValue.mk_fresh () in
+    let astate =
+      Memory.add_attribute ret_addr (BoItv Itv.ItvPure.nat) astate
+      |> Memory.add_attribute ret_addr
+           (Arithmetic (Arithmetic.zero_inf, Immediate {location; history= []}))
+    in
+    Ok [PulseOperations.write_id ret_id (ret_addr, []) astate]
+
+
   let skip : model = fun ~caller_summary:_ _ ~ret:_ astate -> Ok [astate]
 
   let nondet ~fn_name : model =
@@ -354,6 +365,7 @@ module ProcNameDispatcher = struct
       ; +match_builtin BuiltinDecl.__cast <>$ capt_arg_payload $+...$--> Misc.id_first_arg
       ; +match_builtin BuiltinDecl.abort <>--> Misc.early_exit
       ; +match_builtin BuiltinDecl.exit <>--> Misc.early_exit
+      ; +match_builtin BuiltinDecl.__get_array_length <>--> Misc.return_unknown_size
       ; (* consider that all fbstrings are small strings to avoid false positives due to manual
            ref-counting *)
         -"folly" &:: "fbstring_core" &:: "category" &--> Misc.return_int Int64.zero

infer/tests/codetoanalyze/java/impurity/PurityModeled.java

@@ -15,4 +15,8 @@ class PurityModeled {
     // copies an array from the specified source array
     System.arraycopy(src, 0, dst, 0, 1);
   }
+
+  public void array_length_loop_pure(Integer[] array) {
+    for (int i = 0; i < array.length; i++) {}
+  }
 }