[inferbo][bugfix] Revise gathering safety conditions in sub-exp

Reviewed By: mbouaziz

Differential Revision: D7471891

fbshipit-source-id: 2b592b1

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -393,27 +393,33 @@ module Report = struct
         cond_set
 
 
-  let rec check_expr
+  let check_expr
       : Typ.Procname.t -> Exp.t -> Location.t -> Dom.Mem.astate -> PO.ConditionSet.t
         -> PO.ConditionSet.t =
    fun pname exp location mem cond_set ->
+    let rec check_sub_expr exp cond_set =
+      match exp with
+      | Exp.Lindex (array_exp, index_exp) ->
+          cond_set |> check_sub_expr array_exp |> check_sub_expr index_exp
+          |> BoUtils.Check.lindex ~array_exp ~index_exp mem pname location
+      | Exp.BinOp (_, e1, e2) ->
+          cond_set |> check_sub_expr e1 |> check_sub_expr e2
+      | Exp.Lfield (e, _, _) | Exp.UnOp (_, e, _) | Exp.Exn e | Exp.Cast (_, e) ->
+          check_sub_expr e cond_set
+      | Exp.Closure {captured_vars} ->
+          List.fold captured_vars ~init:cond_set ~f:(fun cond_set (e, _, _) ->
+              check_sub_expr e cond_set )
+      | Exp.Var _ | Exp.Lvar _ | Exp.Const _ | Exp.Sizeof _ ->
+          cond_set
+    in
+    let cond_set = check_sub_expr exp cond_set in
     match exp with
     | Exp.Var _ ->
         let arr = Sem.eval exp mem in
         BoUtils.Check.array_access ~arr ~idx:Dom.Val.Itv.zero ~is_plus:true pname location cond_set
-    | Exp.Lindex (array_exp, index_exp) ->
-        cond_set |> check_expr pname array_exp location mem
-        |> check_expr pname index_exp location mem
-        |> BoUtils.Check.lindex ~array_exp ~index_exp mem pname location
     | Exp.BinOp (bop, e1, e2) ->
-        cond_set |> check_expr pname e1 location mem |> check_expr pname e2 location mem
-        |> check_binop pname ~bop ~e1 ~e2 location mem
-    | Exp.Lfield (e, _, _) | Exp.UnOp (_, e, _) | Exp.Exn e | Exp.Cast (_, e) ->
-        check_expr pname e location mem cond_set
-    | Exp.Closure {captured_vars} ->
-        List.fold captured_vars ~init:cond_set ~f:(fun cond_set (e, _, _) ->
-            check_expr pname e location mem cond_set )
-    | Exp.Lvar _ | Exp.Const _ | Exp.Sizeof _ ->
+        check_binop pname ~bop ~e1 ~e2 location mem cond_set
+    | _ ->
         cond_set
 
 

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

@@ -50,7 +50,6 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_underrun_Bad, 2, BUFFER
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_no_overrun_Good_FP, 3, BUFFER_OVERRUN_L4, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_overrun_Bad, 3, BUFFER_OVERRUN_L4, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l5_external_Warn_Bad, 2, BUFFER_OVERRUN_U5, ERROR, [ArrayDeclaration,Unknown value from: unknown_function,ArrayAccess: Offset: [-oo, +oo] Size: [10, 10]]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, l5_external_Warn_Bad, 2, BUFFER_OVERRUN_U5, ERROR, [Unknown value from: unknown_function,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Bad, 3, BUFFER_OVERRUN_S2, ERROR, [Offset: [s$0, +oo] Size: [s$0, s$1]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Good_FP, 3, BUFFER_OVERRUN_S2, ERROR, [Offset: [s$0, +oo] Size: [s$0, s$1]]
 codetoanalyze/c/bufferoverrun/models.c, exit_bo_good_unreachable_bad, 2, UNREACHABLE_CODE, ERROR, []