From f3cf0ec0f69adde2fa4e1c5da3e6568c74b80a7c Mon Sep 17 00:00:00 2001
From: Mehdi Bouaziz <mbouaziz@fb.com>
Date: Thu, 10 May 2018 11:12:09 -0700
Subject: [PATCH] [Inferbo/cost][java] Model for __get_array_length

Summary:
Java arrays have an internal length that can be retrieved with the internal `__get_array_length`.
Here is a model for it.

Reviewed By: jvillard

Differential Revision: D7931572

fbshipit-source-id: fd4c179
---
 infer/src/bufferoverrun/bufferOverrunModels.ml | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml
index 306d2e6b4..0bd13a6e5 100644
--- a/infer/src/bufferoverrun/bufferOverrunModels.ml
+++ b/infer/src/bufferoverrun/bufferOverrunModels.ml
@@ -193,6 +193,17 @@ let infer_print e =
   {exec; check= no_check}
 
 
+let get_array_length array_exp =
+  let exec {ret} mem =
+    let arr = Sem.eval_arr array_exp mem in
+    let traces = Dom.Val.get_traces arr in
+    let length = arr |> Dom.Val.get_array_blk |> ArrayBlk.sizeof in
+    let result = Dom.Val.of_itv ~traces length in
+    model_by_value result ret mem
+  in
+  {exec; check= no_check}
+
+
 let set_array_length array length_exp =
   let exec {pname; node_hash; location} mem =
     match array with
@@ -331,6 +342,7 @@ module Call = struct
       ; -"__new_array" <>$ capt_exp $+...$--> malloc
       ; -"__placement_new" <>$ any_arg $+ capt_exp $!--> placement_new
       ; -"realloc" <>$ capt_exp $+ capt_exp $+...$--> realloc
+      ; -"__get_array_length" <>$ capt_exp $!--> get_array_length
       ; -"__set_array_length" <>$ capt_arg $+ capt_exp $!--> set_array_length
       ; -"strlen" <>--> by_value Dom.Val.Itv.nat
       ; -"boost" &:: "split" $ capt_arg_of_typ (-"std" &:: "vector") $+ any_arg $+ any_arg