[inferbo] Collect array accesses from sub expressions

Summary: It collects array accesses from all sub expressions in commands.

Reviewed By: mbouaziz

Differential Revision: D7165098

fbshipit-source-id: 584dc80

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -316,7 +316,7 @@ module Report = struct
 
   type extras = Typ.Procname.t -> Procdesc.t option
 
-  let add_condition
+  let rec add_condition
       : Typ.Procname.t -> Exp.t -> Location.t -> Dom.Mem.astate -> PO.ConditionSet.t
         -> PO.ConditionSet.t =
    fun pname exp location mem cond_set ->
@@ -328,7 +328,9 @@ module Report = struct
         BoUtils.Check.array_access ~arr ~arr_traces ~idx:Itv.zero ~idx_traces:TraceSet.empty
           ~is_plus:true pname location cond_set
     | Exp.Lindex (array_exp, index_exp) ->
-        BoUtils.Check.lindex ~array_exp ~index_exp mem pname location cond_set
+        cond_set |> add_condition pname array_exp location mem
+        |> add_condition pname index_exp location mem
+        |> BoUtils.Check.lindex ~array_exp ~index_exp mem pname location
     | Exp.BinOp ((Binop.PlusA as bop), e1, e2) | Exp.BinOp ((Binop.MinusA as bop), e1, e2) ->
         let v_arr = Sem.eval e1 mem in
         let arr = Dom.Val.get_array_blk v_arr in
@@ -337,8 +339,15 @@ module Report = struct
         let idx = Dom.Val.get_itv v_idx in
         let idx_traces = Dom.Val.get_traces v_idx in
         let is_plus = Binop.equal bop Binop.PlusA in
-        BoUtils.Check.array_access ~arr ~arr_traces ~idx ~idx_traces ~is_plus pname location
-          cond_set
+        cond_set |> add_condition pname e1 location mem |> add_condition pname e2 location mem
+        |> BoUtils.Check.array_access ~arr ~arr_traces ~idx ~idx_traces ~is_plus pname location
+    | Exp.Lfield (e, _, _) | Exp.UnOp (_, e, _) | Exp.Exn e | Exp.Cast (_, e) ->
+        add_condition pname e location mem cond_set
+    | Exp.BinOp (_, e1, e2) ->
+        cond_set |> add_condition pname e1 location mem |> add_condition pname e2 location mem
+    | Exp.Closure {captured_vars} ->
+        List.fold captured_vars ~init:cond_set ~f:(fun cond_set (e, _, _) ->
+            add_condition pname e location mem cond_set )
     | _ ->
         cond_set
 

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

@@ -42,6 +42,7 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_overrun_Bad, 2, BUFFER_
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_underrun_Bad, 2, BUFFER_OVERRUN_L3, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [-1, 9] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_no_overrun_Good_FP, 3, BUFFER_OVERRUN_L4, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_overrun_Bad, 3, BUFFER_OVERRUN_L4, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10]]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, l5_external_Warn_Bad, 2, BUFFER_OVERRUN_L5, [Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l5_external_Warn_Bad, 2, BUFFER_OVERRUN_L5, [ArrayDeclaration,ArrayAccess: Offset: [-oo, +oo] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Bad, 3, BUFFER_OVERRUN_S2, [Offset: [s$0, +oo] Size: [s$0, s$1]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Good_FP, 3, BUFFER_OVERRUN_S2, [Offset: [s$0, +oo] Size: [s$0, s$1]]

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

@@ -15,6 +15,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, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [-1, -1] Size: [10, 10]]
 codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Bad, 4, BUFFER_OVERRUN_L1, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [5, 5] Size: [5, 5]]
 codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Good_FP, 6, BUFFER_OVERRUN_L5, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [5, 5]]
+codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct1_Bad, 4, BUFFER_OVERRUN_L1, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [5, 5] Size: [5, 5]]
+codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct2_Bad, 4, BUFFER_OVERRUN_L1, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [5, 5] Size: [5, 5]]
 codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 1, CONDITION_ALWAYS_TRUE, []
 codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 6, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [5, 5]]
 codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_goo, 1, CONDITION_ALWAYS_TRUE, []

infer/tests/codetoanalyze/cpp/bufferoverrun/realloc.cpp

@@ -42,7 +42,7 @@ void realloc_struct1_Good() {
   buf2[buf2[0].x[0]].x[0] = 0;
 }
 
-void realloc_struct1_Bad_FN() {
+void realloc_struct1_Bad() {
   struct S1* buf1 = (struct S1*)malloc(2 * sizeof(struct S1));
   buf1[0].x[0] = 5;
   struct S1* buf2 = (struct S1*)realloc(buf1, 5 * sizeof(struct S1));
@@ -64,7 +64,7 @@ void realloc_struct2_Good() {
   buf2[buf2[0].s.x].s.x = 0;
 }
 
-void realloc_struct2_Bad_FN() {
+void realloc_struct2_Bad() {
   struct S3* buf1 = (struct S3*)malloc(2 * sizeof(struct S3));
   buf1[0].s.x = 5;
   struct S3* buf2 = (struct S3*)realloc(buf1, 5 * sizeof(struct S3));