From cfe4c62e472a12b89e075ae375538c6b4f8bc202 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 6 Apr 2020 08:35:28 -0700 Subject: [PATCH] [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 | 4 ++ infer/man/man1/infer-full.txt | 7 +++ infer/man/man1/infer.txt | 4 ++ infer/src/base/Config.ml | 8 +++ infer/src/base/Config.mli | 2 + infer/src/bufferoverrun/absLoc.ml | 33 ++++++------ infer/src/bufferoverrun/symb.ml | 35 +++++++----- infer/src/bufferoverrun/symb.mli | 2 + .../codetoanalyze/c/bufferoverrun/Makefile | 3 +- .../codetoanalyze/c/bufferoverrun/get_field.c | 53 +++++++++++++++++++ .../codetoanalyze/c/bufferoverrun/issues.exp | 1 + 11 files changed, 124 insertions(+), 28 deletions(-) diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index ed05c4942..3353e4cd6 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/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: diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 668dba217..3b7c76bf3 100644 --- a/infer/man/man1/infer-full.txt +++ b/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. diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 39498333d..91e3b8c55 100644 --- a/infer/man/man1/infer.txt +++ b/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: diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index c2f301cb0..cde2d1392 100644 --- a/infer/src/base/Config.ml +++ b/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 diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 0bccfc7ea..12d1a872a 100644 --- a/infer/src/base/Config.mli +++ b/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 diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index 59c7e46e0..7c118354f 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/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 rec aux = function - | Var _ | Allocsite _ -> - 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 {prefix= l} -> - aux l + let append_field ?typ l0 ~fn = + 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 _ -> + 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 ~depth:(depth + 1) l in - aux l0 + aux ~depth:0 l0 end : sig type t = private diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml index 1096d6cd7..12a0c386b 100644 --- a/infer/src/bufferoverrun/symb.ml +++ b/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 - | 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 - | StarField {last_field} as p when Fieldname.equal fn last_field -> - p - | StarField {prefix} -> - StarField {last_field= fn; prefix} + 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 ~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 diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli index 8a34a3f68..26f0a3575 100644 --- a/infer/src/bufferoverrun/symb.mli +++ b/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 diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/Makefile b/infer/tests/codetoanalyze/c/bufferoverrun/Makefile index 285942803..2988e6797 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/Makefile +++ b/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) diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/get_field.c b/infer/tests/codetoanalyze/c/bufferoverrun/get_field.c index 571f0efc1..75d60ad3b 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/get_field.c +++ b/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; + } + } +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index ade81dd73..b5df0c09b 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/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, [,Call,Assignment,,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, [,Call,Assignment,,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, [,Assignment,Call,Parameter `l->next->prev->v`,Assignment,,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, [,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, [,Array declaration,Array access: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10]