[inferbo] Handle global constant array loads in Obj-C

Summary: In Objective-C, `static const int var  = ..` is not recognized as ICE (integral constant expression) unlike C++. To handle such loads better, this diff adds a check for `constant_global_array` as a workaround.

Reviewed By: skcho

Differential Revision: D26369461

fbshipit-source-id: e2dae11f1

infer/src/IR/Pvar.ml

@@ -28,7 +28,8 @@ type pvar_kind =
       ; is_pod: bool
       ; is_static_local: bool
       ; is_static_global: bool
-      ; is_constant_array: bool }  (** global variable *)
+      ; is_constant_array: bool
+      ; is_const: bool }  (** global variable *)
   | Seed_var  (** variable used to store the initial value of formal parameters *)
 [@@deriving compare]
 
@@ -113,6 +114,8 @@ let is_constant_array pv =
   match pv.pv_kind with Global_var {is_constant_array} -> is_constant_array | _ -> false
 
 
+let is_const pv = match pv.pv_kind with Global_var {is_const} -> is_const | _ -> false
+
 (** Check if a pvar is the special "this" var *)
 let is_this pvar = Mangled.is_this (get_name pvar)
 
@@ -243,8 +246,8 @@ let mk_callee (name : Mangled.t) (proc_name : Procname.t) : t =
 
 (** create a global variable with the given name *)
 let mk_global ?(is_constexpr = false) ?(is_ice = false) ?(is_pod = true) ?(is_static_local = false)
-    ?(is_static_global = false) ?(is_constant_array = false) ?translation_unit (name : Mangled.t) :
-    t =
+    ?(is_static_global = false) ?(is_constant_array = false) ?(is_const = false) ?translation_unit
+    (name : Mangled.t) : t =
   { pv_hash= name_hash name
   ; pv_name= name
   ; pv_kind=
@@ -255,7 +258,8 @@ let mk_global ?(is_constexpr = false) ?(is_ice = false) ?(is_pod = true) ?(is_st
         ; is_pod
         ; is_static_local
         ; is_static_global
-        ; is_constant_array } }
+        ; is_constant_array
+        ; is_const } }
 
 
 (** create a fresh temporary variable local to procedure [pname]. for use in the frontends only! *)

infer/src/IR/Pvar.mli

@@ -60,6 +60,9 @@ val is_static_local : t -> bool
 val is_constant_array : t -> bool
 (** Check if the pvar has a constant array type *)
 
+val is_const : t -> bool
+(** Check if the pvar has a const type *)
+
 val is_local : t -> bool
 (** Check if the pvar is a (non-static) local var *)
 
@@ -115,6 +118,7 @@ val mk_global :
   -> ?is_static_local:bool
   -> ?is_static_global:bool
   -> ?is_constant_array:bool
+  -> ?is_const:bool
   -> ?translation_unit:SourceFile.t
   -> Mangled.t
   -> t

infer/src/bufferoverrun/bufferOverrunAnalysis.ml

@@ -326,7 +326,8 @@ module TransferFunctions = struct
         load_global_constant get_summary (id, typ) pvar location mem
           ~find_from_initializer:(fun callee_mem -> Dom.Mem.find (Loc.of_pvar pvar) callee_mem)
     | Load {id; e= Exp.Lindex (Exp.Lvar pvar, _); typ; loc= location}
-      when Pvar.is_compile_constant pvar || Pvar.is_ice pvar ->
+      when Pvar.is_compile_constant pvar || Pvar.is_ice pvar
+           || (Pvar.is_constant_array pvar && Pvar.is_const pvar) ->
         load_global_constant get_summary (id, typ) pvar location mem
           ~find_from_initializer:(fun callee_mem ->
             let locs = Dom.Mem.find (Loc.of_pvar pvar) callee_mem |> Dom.Val.get_all_locs in

infer/src/clang/cGeneral_utils.ml

@@ -139,12 +139,13 @@ let mk_sil_global_var {CFrontend_config.source_file} ?(mk_name = fun _ x -> x) d
     && (not var_decl_info.Clang_ast_t.vdi_is_static_data_member)
     && var_decl_info.Clang_ast_t.vdi_is_static
   in
+  let is_const = qt.Clang_ast_t.qt_is_const in
   let is_constant_array =
     Option.exists desugared_type ~f:(function Clang_ast_t.ConstantArrayType _ -> true | _ -> false)
   in
   Pvar.mk_global ~is_constexpr ~is_ice ~is_pod
     ~is_static_local:var_decl_info.Clang_ast_t.vdi_is_static_local ~is_static_global
-    ~is_constant_array ?translation_unit (mk_name name_string simple_name)
+    ~is_constant_array ?translation_unit (mk_name name_string simple_name) ~is_const
 
 
 let mk_sil_var trans_unit_ctx named_decl_info decl_info_qual_type_opt procname outer_procname =

infer/tests/codetoanalyze/objc/bufferoverrun/global.m

@@ -0,0 +1,18 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+static const int ConstantGlobal[] = {8};
+
+void access_constant_global_Bad() {
+  int a[5];
+  a[ConstantGlobal[0]] = 3;
+}
+
+int access_constant_global_via_assignment_Bad() {
+  int a[5];
+  const int* arr = ConstantGlobal;
+  return a[arr[0]];
+}

infer/tests/codetoanalyze/objc/bufferoverrun/issues.exp

@@ -1,2 +1,4 @@
 codetoanalyze/objc/bufferoverrun/block.m, Block.block_in_field_Bad, 7, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: 15 Size: 10]
+codetoanalyze/objc/bufferoverrun/global.m, access_constant_global_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 8 Size: 5]
+codetoanalyze/objc/bufferoverrun/global.m, access_constant_global_via_assignment_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 8 Size: 5]
 codetoanalyze/objc/bufferoverrun/return_struct.m, ReturnStruct.call_get_struct_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Call,Parameter `n`,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: 5 Size: 3]

infer/tests/codetoanalyze/objc/performance/cost-issues.exp

@@ -206,6 +206,8 @@ codetoanalyze/objc/performance/field_access.m, Test1.setX:, 3,  OnUIThread:false
 codetoanalyze/objc/performance/field_access.m, Test1.x, 3,  OnUIThread:false, []
 codetoanalyze/objc/performance/field_access.m, create_common_person_constant, 49,  OnUIThread:false, []
 codetoanalyze/objc/performance/field_access.m, iterate_upto_field_size_linear, 2 + 3 ⋅ test->_x.ub + 5 ⋅ (1+max(0, test->_x.ub)),  OnUIThread:false, [{1+max(0, test->_x.ub)},Loop,{test->_x.ub},Loop]
+codetoanalyze/objc/performance/global_test.m, __infer_globals_initializer_ConstantGlobal, 1,  OnUIThread:false, []
+codetoanalyze/objc/performance/global_test.m, access_constant_constant, 59,  OnUIThread:false, []
 codetoanalyze/objc/performance/instantiate.m, do_2_times_constant, 16,  OnUIThread:false, []
 codetoanalyze/objc/performance/instantiate.m, do_half_m2_times_quadratic, 2 + 4 ⋅ (m - 1) × m + 6 ⋅ m + 2 ⋅ m × (max(1, m)) + 2 ⋅ (1+max(0, m)),  OnUIThread:false, [{1+max(0, m)},Loop,{max(1, m)},Call to do_n_times,Loop,{m},Loop,{m},Loop,{m - 1},Call to do_n_times,Loop]
 codetoanalyze/objc/performance/instantiate.m, do_m2_times_quadratic, 2 + 6 ⋅ m + 4 ⋅ m × m + 2 ⋅ m × (1+max(0, m)) + 2 ⋅ (1+max(0, m)),  OnUIThread:false, [{1+max(0, m)},Loop,{1+max(0, m)},Call to do_n_times,Loop,{m},Call to do_n_times,Loop,{m},Loop]

infer/tests/codetoanalyze/objc/performance/global_test.m

@@ -0,0 +1,12 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+static const int ConstantGlobal[] = {10};
+
+void access_constant_constant() {
+  for (int i = 0; i <= ConstantGlobal[0]; i++) {
+  }
+}