From cc1e18e124bd59345f984bb64a73752e1bcbe0dc Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Wed, 27 Feb 2019 18:29:13 -0800 Subject: [PATCH] [inferbo] Differentiate proof obligations by allocsites Summary: This diff differentiates proof obligations by allocsites. Sizes and offsets of arrays were joined when making proof obligations. Reviewed By: mbouaziz Differential Revision: D14163149 fbshipit-source-id: cb6608c16 --- infer/src/bufferoverrun/arrayBlk.ml | 2 - infer/src/bufferoverrun/bufferOverrunUtils.ml | 77 +++++++++++-------- .../codetoanalyze/c/bufferoverrun/issues.exp | 4 +- .../codetoanalyze/c/bufferoverrun/trivial.c | 24 ++++++ 4 files changed, 73 insertions(+), 34 deletions(-) diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml index ce2a64ae5..54cec6e9b 100644 --- a/infer/src/bufferoverrun/arrayBlk.ml +++ b/infer/src/bufferoverrun/arrayBlk.ml @@ -287,8 +287,6 @@ let offsetof = join_itv ~f:ArrInfo.offsetof let sizeof = join_itv ~f:ArrInfo.sizeof -let sizeof_byte = join_itv ~f:ArrInfo.byte_size - let plus_offset : t -> Itv.t -> t = fun arr i -> map (fun a -> ArrInfo.plus_offset a i) arr let minus_offset : t -> Itv.t -> t = fun arr i -> map (fun a -> ArrInfo.minus_offset a i) arr diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index e55786704..bf23402a3 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -212,44 +212,54 @@ module Exec = struct end module Check = struct - let check_access ~size ~idx ~size_sym_exp ~idx_sym_exp ~relation ~arr ~idx_traces ~last_included - ~latest_prune location cond_set = + let check_access ~size ~idx ~offset ~size_sym_exp ~idx_sym_exp ~relation ~arr_traces ~idx_traces + ~last_included ~latest_prune location cond_set = match (size, idx) with | NonBottom length, NonBottom idx -> - let offset = - match ArrayBlk.offsetof (Dom.Val.get_array_blk arr) with - | Bottom -> - (* Java's collection has no offset. *) - Itv.ItvPure.zero - | NonBottom offset -> - offset - in - let arr_traces = Dom.Val.get_traces arr in PO.ConditionSet.add_array_access location ~size:length ~offset ~idx ~size_sym_exp ~idx_sym_exp ~relation ~last_included ~idx_traces ~arr_traces ~latest_prune cond_set | _ -> cond_set + let log_array_access allocsite size offset idx = + L.(debug BufferOverrun Verbose) + "@[Add condition :@,array: %a@, size: %a@, idx: %a + %a@,@]@." Allocsite.pp allocsite + Itv.pp size Itv.ItvPure.pp offset Itv.pp idx + + + let offsetof arr_info = + match ArrayBlk.ArrInfo.offsetof arr_info with + | Bottom -> + (* Java's collection has no offset. *) + Itv.ItvPure.zero + | NonBottom offset -> + offset + + let array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus ~last_included ~latest_prune location cond_set = - let arr_blk = Dom.Val.get_array_blk arr in - let size = ArrayBlk.sizeof arr_blk in - let size_sym_exp = Relation.SymExp.of_sym (Dom.Val.get_size_sym arr) in - let idx_itv = Dom.Val.get_itv idx in let idx_traces = Dom.Val.get_traces idx in - let idx = if is_plus then idx_itv else Itv.neg idx_itv in + let idx = + let idx_itv = Dom.Val.get_itv idx in + if is_plus then idx_itv else Itv.neg idx_itv + in + let arr_traces = Dom.Val.get_traces arr in + let size_sym_exp = Relation.SymExp.of_sym (Dom.Val.get_size_sym arr) in let idx_sym_exp = let offset_sym_exp = Relation.SymExp.of_sym (Dom.Val.get_offset_sym arr) in Option.map2 offset_sym_exp idx_sym_exp ~f:(fun offset_sym_exp idx_sym_exp -> let op = if is_plus then Relation.SymExp.plus else Relation.SymExp.minus in op idx_sym_exp offset_sym_exp ) in - L.(debug BufferOverrun Verbose) - "@[Add condition :@,array: %a@, idx: %a + %a@,@]@." ArrayBlk.pp arr_blk Itv.pp - (ArrayBlk.offsetof arr_blk) Itv.pp idx ; - check_access ~size ~idx ~size_sym_exp ~idx_sym_exp ~relation ~arr ~idx_traces ~last_included - ~latest_prune location cond_set + let array_access1 allocsite arr_info acc = + let size = ArrayBlk.ArrInfo.sizeof arr_info in + let offset = offsetof arr_info in + log_array_access allocsite size offset idx ; + check_access ~size ~idx ~offset ~size_sym_exp ~idx_sym_exp ~relation ~arr_traces ~idx_traces + ~last_included ~latest_prune location acc + in + ArrayBlk.fold array_access1 (Dom.Val.get_array_blk arr) cond_set let lindex integer_type_widths ~array_exp ~index_exp ~last_included mem location cond_set = @@ -264,17 +274,22 @@ module Check = struct location cond_set - let array_access_byte ~arr ~idx ~relation ~is_plus ~last_included location cond_set = - let arr_blk = Dom.Val.get_array_blk arr in - let size = ArrayBlk.sizeof_byte arr_blk in - let idx_itv = Dom.Val.get_itv idx in + let array_access_byte ~arr ~idx ~relation ~is_plus ~last_included ~latest_prune location cond_set + = let idx_traces = Dom.Val.get_traces idx in - let idx = if is_plus then idx_itv else Itv.neg idx_itv in - L.(debug BufferOverrun Verbose) - "@[Add condition :@,array: %a@, idx: %a + %a@,@]@." ArrayBlk.pp arr_blk Itv.pp - (ArrayBlk.offsetof arr_blk) Itv.pp idx ; - check_access ~size ~idx ~size_sym_exp:None ~idx_sym_exp:None ~relation ~arr ~idx_traces - ~last_included location cond_set + let idx = + let idx_itv = Dom.Val.get_itv idx in + if is_plus then idx_itv else Itv.neg idx_itv + in + let arr_traces = Dom.Val.get_traces arr in + let array_access_byte1 allocsite arr_info acc = + let size = ArrayBlk.ArrInfo.byte_size arr_info in + let offset = offsetof arr_info in + log_array_access allocsite size offset idx ; + check_access ~size ~idx ~offset ~size_sym_exp:None ~idx_sym_exp:None ~relation ~arr_traces + ~idx_traces ~last_included ~latest_prune location acc + in + ArrayBlk.fold array_access_byte1 (Dom.Val.get_array_blk arr) cond_set let lindex_byte integer_type_widths ~array_exp ~byte_index_exp ~last_included mem location diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index a3d9e9369..237bc8632 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -101,7 +101,7 @@ codetoanalyze/c/bufferoverrun/external.c, extern_bad, 5, BUFFER_OVERRUN_U5, no_b codetoanalyze/c/bufferoverrun/external.c, extern_bad, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 30 Size: 10] codetoanalyze/c/bufferoverrun/for_loop.c, call_initialize_arr_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Array declaration,Call,,Assignment,,Parameter `*arr`,Array access: Offset: [0, 19] Size: 10 by call to `initialize_arr` ] codetoanalyze/c/bufferoverrun/for_loop.c, call_two_loops_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,Call,Parameter `m`,Assignment,,Array declaration,Array access: Offset: 15 Size: 10] -codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Assignment,,Call,Array declaration,Assignment,Assignment,Assignment,Array access: Offset: [0, 9] Size: [5, 10]] +codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Call,Array declaration,Assignment,Assignment,Assignment,Array access: Offset: [0, 9] Size: 5] codetoanalyze/c/bufferoverrun/for_loop.c, threshold_by_comparison_1_Bad, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, 99] Size: 50] codetoanalyze/c/bufferoverrun/for_loop.c, threshold_by_comparison_2_Bad, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/for_loop.c, threshold_by_comparison_2_Bad, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, 99] Size: 50] @@ -287,6 +287,8 @@ codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 1, CONDITION_ALWAYS_TRU codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 1 Size: 0] codetoanalyze/c/bufferoverrun/sizeof.c, static_stride_bad, 5, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/sizeof.c, static_stride_bad, 7, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 1 Size: 0] +codetoanalyze/c/bufferoverrun/trivial.c, differentiate_array_info_Bad, 8, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 5 Size: 5] +codetoanalyze/c/bufferoverrun/trivial.c, differentiate_array_info_Bad, 8, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 10 (⇐ 5 + 5) Size: 10] codetoanalyze/c/bufferoverrun/trivial.c, malloc_zero_Bad, 2, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Allocation: Length: 0] codetoanalyze/c/bufferoverrun/trivial.c, trivial_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_once_intentional_good, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/trivial.c b/infer/tests/codetoanalyze/c/bufferoverrun/trivial.c index 3d7ac6c75..f0b6f565c 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/trivial.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/trivial.c @@ -17,3 +17,27 @@ void malloc_zero_Bad() { x = malloc(0); x = malloc(1); } + +int unknown_function(); + +void differentiate_array_info_Good() { + int* p; + if (unknown_function()) { + p = (int*)malloc(sizeof(int) * 5); + } else { + p = (int*)malloc(sizeof(int) * 10); + p = p + 5; + } + p[4] = 0; +} + +void differentiate_array_info_Bad() { + int* p; + if (unknown_function()) { + p = (int*)malloc(sizeof(int) * 5); + } else { + p = (int*)malloc(sizeof(int) * 10); + p = p + 5; + } + p[5] = 0; +}