[infer] Load global array constant

Summary: This diff enables loading array contents of global constant.

Reviewed By: ezgicicek

Differential Revision: D19329014

fbshipit-source-id: 9dfae2754

infer/src/bufferoverrun/bufferOverrunAnalysis.ml

@@ -276,19 +276,12 @@ module TransferFunctions = struct
         None
 
 
-  let exec_instr : Dom.Mem.t -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.t =
-   fun mem {summary; tenv; extras= {get_summary; get_formals; oenv= {integer_type_widths}}} node
-       instr ->
-    match instr with
-    | Load {id} when Ident.is_none id ->
-        mem
-    | Load {id; e= Exp.Lvar pvar; loc= location}
-      when Pvar.is_compile_constant pvar || Pvar.is_ice pvar -> (
+  let load_global_constant get_summary id pvar location mem ~find_from_initializer =
     match Pvar.get_initializer_pname pvar with
     | Some callee_pname -> (
       match get_summary callee_pname with
       | Some callee_mem ->
-            let v = Dom.Mem.find (Loc.of_pvar pvar) callee_mem in
+          let v = find_from_initializer callee_mem in
           Dom.Mem.add_stack (Loc.of_id id) v mem
       | None ->
           L.d_printfln_escaped "/!\\ Unknown initializer of global constant %a" (Pvar.pp Pp.text)
@@ -297,7 +290,25 @@ module TransferFunctions = struct
     | None ->
         L.d_printfln_escaped "/!\\ Failed to get initializer name of global constant %a"
           (Pvar.pp Pp.text) pvar ;
-          Dom.Mem.add_unknown id ~location mem )
+        Dom.Mem.add_unknown id ~location mem
+
+
+  let exec_instr : Dom.Mem.t -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.t =
+   fun mem {summary; tenv; extras= {get_summary; get_formals; oenv= {integer_type_widths}}} node
+       instr ->
+    match instr with
+    | Load {id} when Ident.is_none id ->
+        mem
+    | Load {id; e= Exp.Lvar pvar; loc= location}
+      when Pvar.is_compile_constant pvar || Pvar.is_ice pvar ->
+        load_global_constant get_summary id 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, _); loc= location}
+      when Pvar.is_compile_constant pvar || Pvar.is_ice pvar ->
+        load_global_constant get_summary id 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
+            Dom.Mem.find_set locs callee_mem )
     | Load {id; e= exp; typ; loc= location} -> (
         let model_env =
           let pname = Summary.get_proc_name summary in

infer/tests/codetoanalyze/cpp/bufferoverrun/global.cpp

@@ -0,0 +1,19 @@
+/*
+ * 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 constexpr int ConstantGlobal[] = {5};
+
+void access_constant_global_Bad() {
+  int a[5];
+  a[ConstantGlobal[0]] = 3;
+}
+
+static int StaticGlobal[][3] = {
+    {0, 0, 0}, {0, 0, 0}, {0, 0, 0}, {0, 0, 0}, {0, 0, 0}};
+
+void access_static_global1_Bad_FN() { int* p = StaticGlobal[10]; }
+
+void access_static_global2_Bad_FN() { int a = StaticGlobal[0][10]; }

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

@@ -49,6 +49,7 @@ codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::FP_do_not_ignore_e
 codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 0 Size: 0]
 codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: -1 Size: 10]
 codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_loop_with_init_S_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Call,Parameter `length`,Assignment,<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
+codetoanalyze/cpp/bufferoverrun/global.cpp, access_constant_global_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 5 Size: 5]
 codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: 5 Size: 5]
 codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_flexible_array_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 7 Size: 5]
 codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct1_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: 5 Size: 5]