[inferbo] Check nested global array access

Summary: This diff fixes the array access checking function for nested global arrays. We had assumed that RHS of `store` statement in SIL does not include array access expression, but that is not true: for global arrays, SIL can have statements like `*LHS = GlobalArray[n][m]`.

Reviewed By: ezgicicek

Differential Revision: D19300153

fbshipit-source-id: 256325642

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -156,13 +156,14 @@ let check_binop :
 
 
 let check_expr_for_array_access :
-       Typ.IntegerWidths.t
+       ?sub_expr_only:bool
+    -> Typ.IntegerWidths.t
     -> Exp.t
     -> Location.t
     -> Dom.Mem.t
     -> PO.ConditionSet.checked_t
     -> PO.ConditionSet.checked_t =
- fun integer_type_widths exp location mem cond_set ->
+ fun ?(sub_expr_only = false) integer_type_widths exp location mem cond_set ->
   let rec check_sub_expr exp cond_set =
     match exp with
     | Exp.Lindex (array_exp, index_exp) ->
@@ -182,17 +183,19 @@ let check_expr_for_array_access :
         cond_set
   in
   let cond_set = check_sub_expr exp cond_set in
-  match exp with
-  | Exp.Var _ ->
-      let arr = Sem.eval integer_type_widths exp mem in
-      let idx = Dom.Val.Itv.zero in
-      let latest_prune = Dom.Mem.get_latest_prune mem in
-      BoUtils.Check.array_access ~arr ~idx ~is_plus:true ~last_included:false ~latest_prune location
+  if sub_expr_only then cond_set
+  else
+    match exp with
+    | Exp.Var _ ->
+        let arr = Sem.eval integer_type_widths exp mem in
+        let idx = Dom.Val.Itv.zero in
+        let latest_prune = Dom.Mem.get_latest_prune mem in
+        BoUtils.Check.array_access ~arr ~idx ~is_plus:true ~last_included:false ~latest_prune
+          location cond_set
+    | Exp.BinOp (bop, e1, e2) ->
+        check_binop integer_type_widths ~bop ~e1 ~e2 location mem cond_set
+    | _ ->
         cond_set
-  | Exp.BinOp (bop, e1, e2) ->
-      check_binop integer_type_widths ~bop ~e1 ~e2 location mem cond_set
-  | _ ->
-      cond_set
 
 
 let check_binop_for_integer_overflow integer_type_widths bop ~lhs ~rhs location mem cond_set =
@@ -276,6 +279,7 @@ let check_instr :
   | Sil.Store {e1= lexp; e2= rexp; loc= location} ->
       cond_set
       |> check_expr_for_array_access integer_type_widths lexp location mem
+      |> check_expr_for_array_access ~sub_expr_only:true integer_type_widths rexp location mem
       |> check_expr_for_integer_overflow integer_type_widths lexp location mem
       |> check_expr_for_integer_overflow integer_type_widths rexp location mem
   | Sil.Call (_, Const (Cfun callee_pname), params, location, _) -> (

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -318,7 +318,7 @@ let rec eval_arr : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Val.t =
       let locs = eval_locs e mem |> PowLoc.append_field ~fn in
       Mem.find_set locs mem
   | Exp.Lindex (e, _) ->
-      let locs = eval_locs e mem in
+      let locs = eval_arr integer_type_widths e mem |> Val.get_all_locs in
       Mem.find_set locs mem
   | Exp.Const _ | Exp.UnOp _ | Exp.Sizeof _ | Exp.Exn _ | Exp.Closure _ ->
       Val.bot

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

@@ -14,6 +14,6 @@ void access_constant_global_Bad() {
 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_global1_Bad() { int* p = StaticGlobal[10]; }
 
 void access_static_global2_Bad() { int a = StaticGlobal[0][10]; }

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

@@ -50,7 +50,8 @@ codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empt
 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/global.cpp, access_static_global2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
+codetoanalyze/cpp/bufferoverrun/global.cpp, access_static_global1_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
+codetoanalyze/cpp/bufferoverrun/global.cpp, access_static_global2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 3]
 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]