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]