[inferbo] Limit depth of abstract location

Summary:
This diff limits the depth of abstract location by a constant.

problem: Inferbo generated too many of abstract locations, especially when struct types had many pointer fields and Inferbo was not able to analyze the objects precisely. Since the number of generated abstract locations were exponential to the number of fields, it resulted in OOM in the end.

(reported by zyh1121 in https://github.com/facebook/infer/issues/1246)

Reviewed By: jvillard

Differential Revision: D20818471

fbshipit-source-id: f8af27e5c

infer/man/man1/infer-analyze.txt

@@ -336,6 +336,10 @@ BUFFER OVERRUN OPTIONS
        --bo-debug int
            Debug level for buffer-overrun checker (0-4)
 
+       --bo-field-depth-limit int
+           Limit of field depth of abstract location in buffer-overrun
+           checker
+
        --bo-service-handler-request
            Activates: [EXPERIMENTAL] Use taint flow of service handler
            requests in buffer overflow checking. (Conversely:

infer/man/man1/infer-full.txt

@@ -129,6 +129,10 @@ OPTIONS
        --bo-debug int
            Debug level for buffer-overrun checker (0-4)           See also infer-analyze(1).
 
+       --bo-field-depth-limit int
+           Limit of field depth of abstract location in buffer-overrun
+           checker           See also infer-analyze(1).
+
        --bo-service-handler-request
            Activates: [EXPERIMENTAL] Use taint flow of service handler
            requests in buffer overflow checking. (Conversely:
@@ -1161,6 +1165,9 @@ INTERNAL OPTIONS
            Activates: Mode for analyzing the biabduction models (Conversely:
            --no-biabduction-models-mode)
 
+       --bo-field-depth-limit-reset
+           Cancel the effect of --bo-field-depth-limit.
+
        --bootclasspath-reset
            Cancel the effect of --bootclasspath.
 

infer/man/man1/infer.txt

@@ -129,6 +129,10 @@ OPTIONS
        --bo-debug int
            Debug level for buffer-overrun checker (0-4)           See also infer-analyze(1).
 
+       --bo-field-depth-limit int
+           Limit of field depth of abstract location in buffer-overrun
+           checker           See also infer-analyze(1).
+
        --bo-service-handler-request
            Activates: [EXPERIMENTAL] Use taint flow of service handler
            requests in buffer overflow checking. (Conversely:

infer/src/base/Config.ml

@@ -1003,6 +1003,7 @@ and custom_symbols =
 
 and ( biabduction_models_mode
     , bo_debug
+    , bo_field_depth_limit
     , bo_service_handler_request
     , deduplicate
     , developer_mode
@@ -1037,6 +1038,10 @@ and ( biabduction_models_mode
     CLOpt.mk_int ~default:0 ~long:"bo-debug"
       ~in_help:InferCommand.[(Analyze, manual_buffer_overrun)]
       "Debug level for buffer-overrun checker (0-4)"
+  and bo_field_depth_limit =
+    CLOpt.mk_int_opt ~long:"bo-field-depth-limit"
+      ~in_help:InferCommand.[(Analyze, manual_buffer_overrun)]
+      "Limit of field depth of abstract location in buffer-overrun checker"
   and bo_service_handler_request =
     CLOpt.mk_bool ~long:"bo-service-handler-request"
       ~in_help:InferCommand.[(Analyze, manual_buffer_overrun)]
@@ -1163,6 +1168,7 @@ and ( biabduction_models_mode
   in
   ( biabduction_models_mode
   , bo_debug
+  , bo_field_depth_limit
   , bo_service_handler_request
   , deduplicate
   , developer_mode
@@ -2583,6 +2589,8 @@ and bootclasspath = !bootclasspath
 
 and bo_debug = !bo_debug
 
+and bo_field_depth_limit = !bo_field_depth_limit
+
 and bo_service_handler_request = !bo_service_handler_request
 
 and buck = !buck

infer/src/base/Config.mli

@@ -221,6 +221,8 @@ val biabduction_models_mode : bool
 
 val bo_debug : int
 
+val bo_field_depth_limit : int option
+
 val bo_service_handler_request : bool
 
 val bootclasspath : string option

infer/src/bufferoverrun/absLoc.ml

@@ -142,34 +142,37 @@ module Loc = struct
 
       let of_allocsite a = Allocsite a
 
-      let append_field ?typ l0 ~fn =
+      let append_star_field l0 ~fn =
         let rec aux = function
           | Var _ | Allocsite _ ->
-              Field {prefix= l0; fn; typ}
+              StarField {prefix= l0; last_field= fn}
           | StarField {last_field} as l when Fieldname.equal fn last_field ->
               l
           | StarField {prefix} ->
               StarField {prefix; last_field= fn}
-          | Field {fn= fn'} when Fieldname.equal fn fn' ->
-              StarField {prefix= l0; last_field= fn}
           | Field {prefix= l} ->
               aux l
         in
         aux l0
 
 
-      let append_star_field l0 ~fn =
+      let append_field ?typ l0 ~fn =
-        let rec aux = function
+        let rec aux ~depth l =
+          if Symb.SymbolPath.is_field_depth_beyond_limit depth then append_star_field l0 ~fn
+          else
+            match l with
             | Var _ | Allocsite _ ->
-              StarField {prefix= l0; last_field= fn}
+                Field {prefix= l0; fn; typ}
             | StarField {last_field} as l when Fieldname.equal fn last_field ->
                 l
             | StarField {prefix} ->
                 StarField {prefix; last_field= fn}
+            | Field {fn= fn'} when Fieldname.equal fn fn' ->
+                StarField {prefix= l0; last_field= fn}
             | Field {prefix= l} ->
-              aux l
+                aux ~depth:(depth + 1) l
         in
-        aux l0
+        aux ~depth:0 l0
     end :
       sig
         type t = private

infer/src/bufferoverrun/symb.ml

@@ -27,6 +27,14 @@ module SymbolPath = struct
 
   let compare_field_typ _ _ = 0
 
+  let is_field_depth_beyond_limit =
+    match Config.bo_field_depth_limit with
+    | None ->
+        fun _depth -> false
+    | Some limit ->
+        fun depth -> depth > limit
+
+
   include (* Enforce invariants on Field and StarField *) (
     struct
       type partial =
@@ -58,19 +66,22 @@ module SymbolPath = struct
 
 
       let field ?typ p0 fn =
-        let rec aux = function
+        let rec aux ~depth p =
+          if is_field_depth_beyond_limit depth then star_field p0 fn
+          else
+            match p with
             | Pvar _ | Callsite _ ->
                 Field {fn; prefix= p0; typ}
             | Field {fn= fn'} when Fieldname.equal fn fn' ->
                 StarField {last_field= fn; prefix= p0}
             | Field {prefix= p} | Deref (_, p) ->
-              aux p
+                aux ~depth:(depth + 1) p
             | StarField {last_field} as p when Fieldname.equal fn last_field ->
                 p
             | StarField {prefix} ->
                 StarField {last_field= fn; prefix}
         in
-        aux p0
+        aux ~depth:0 p0
     end :
       sig
         type partial = private

infer/src/bufferoverrun/symb.mli

@@ -88,6 +88,8 @@ module SymbolPath : sig
   val is_cpp_vector_elem : partial -> bool
 
   val is_global_partial : partial -> bool
+
+  val is_field_depth_beyond_limit : int -> bool
 end
 
 module Symbol : sig

infer/tests/codetoanalyze/c/bufferoverrun/Makefile

@@ -8,7 +8,8 @@
 TESTS_DIR = ../../..
 
 CLANG_OPTIONS = -c
-INFER_OPTIONS = -F --project-root $(TESTS_DIR) --bufferoverrun-only --function-pointer-specialization
+INFER_OPTIONS = -F --project-root $(TESTS_DIR) --bufferoverrun-only \
+                --function-pointer-specialization --bo-field-depth-limit 6
 INFERPRINT_OPTIONS = --issues-tests
 
 SOURCES = $(wildcard *.c)

infer/tests/codetoanalyze/c/bufferoverrun/get_field.c

@@ -89,3 +89,56 @@ int call_get_v2_Bad() {
   next->v = 0;
   a[get_v2(l)] = 0;
 }
+
+struct t1 {
+  struct t1* a;
+  struct t1* b;
+  struct t1* c;
+  struct t1* d;
+  struct t1* e;
+  struct t1* f;
+  struct t1* g;
+  struct t1* h;
+  struct t1* i;
+  struct t1* j;
+};
+
+int unknown;
+
+// The analysis should be terminated within a reasonable amount of time.
+void make_many_locations(struct t1* x) {
+  while (1) {
+    switch (unknown) {
+      case 0:
+        x = x->a;
+        break;
+      case 1:
+        x = x->b;
+        break;
+      case 2:
+        x = x->c;
+        break;
+      case 3:
+        x = x->d;
+        break;
+      case 4:
+        x = x->e;
+        break;
+      case 5:
+        x = x->f;
+        break;
+      case 6:
+        x = x->g;
+        break;
+      case 7:
+        x = x->h;
+        break;
+      case 8:
+        x = x->i;
+        break;
+      default:
+        x = x->j;
+        break;
+    }
+  }
+}

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

@@ -126,6 +126,7 @@ codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_cond_Bad, 6, BUFFER_OV
 codetoanalyze/c/bufferoverrun/get_field.c, call_get_v2_Bad, 8, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 10]
 codetoanalyze/c/bufferoverrun/get_field.c, call_get_v2_Good_FP, 8, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 10]
 codetoanalyze/c/bufferoverrun/get_field.c, call_get_v_Bad, 8, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,Call,Parameter `l->next->prev->v`,Assignment,<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
+codetoanalyze/c/bufferoverrun/get_field.c, make_many_locations, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]