From 9bd1191669203ebd0f635432152468512368d739 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 21 Jan 2019 00:59:37 -0800 Subject: [PATCH] [inferbo] Add fgets model Summary: It adds the fgets model. Reviewed By: mbouaziz Differential Revision: D13634754 fbshipit-source-id: 147745483 --- .../src/bufferoverrun/bufferOverrunDomain.ml | 2 + .../src/bufferoverrun/bufferOverrunModels.ml | 25 +++++++++++ infer/src/bufferoverrun/itv.ml | 4 ++ infer/src/bufferoverrun/itv.mli | 3 ++ .../c/bufferoverrun/array_content.c | 41 +++++++++++++++++++ .../codetoanalyze/c/bufferoverrun/issues.exp | 8 ++++ .../c/bufferoverrun/pointer_arith.c | 4 +- 7 files changed, 85 insertions(+), 2 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 4737de413..609248fb2 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -509,6 +509,8 @@ module Val = struct module Itv = struct + let zero_255 = of_itv Itv.zero_255 + let m1_255 = of_itv Itv.m1_255 let nat = of_itv Itv.nat diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 1196dc7b1..cfafdf2d2 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -64,6 +64,30 @@ let check_alloc_size size_exp {location; integer_type_widths} mem cond_set = PO.ConditionSet.add_alloc_size location ~length traces latest_prune cond_set +let fgets str_exp num_exp = + let exec {integer_type_widths} ~ret:(id, _) mem = + let str_v = Sem.eval integer_type_widths str_exp mem in + let num_v = Sem.eval integer_type_widths num_exp mem in + let traces = Trace.Set.join (Dom.Val.get_traces str_v) (Dom.Val.get_traces num_v) in + let update_strlen1 allocsite arrinfo acc = + let strlen = + let offset = ArrayBlk.ArrInfo.offsetof arrinfo in + let num = Dom.Val.get_itv num_v in + Itv.plus offset (Itv.set_lb_zero (Itv.decr num)) + in + Dom.Mem.set_first_idx_of_null allocsite (Dom.Val.of_itv ~traces strlen) acc + in + mem + |> Dom.Mem.update_mem (Sem.eval_locs str_exp mem) Dom.Val.Itv.zero_255 + |> ArrayBlk.fold update_strlen1 (Dom.Val.get_array_blk str_v) + |> Dom.Mem.add_stack (Loc.of_id id) {str_v with itv= Itv.zero} + and check {location; integer_type_widths} mem cond_set = + BoUtils.Check.lindex_byte integer_type_widths ~array_exp:str_exp ~byte_index_exp:num_exp + ~last_included:true mem location cond_set + in + {exec; check} + + let malloc size_exp = let exec ({pname; node_hash; location; tenv; integer_type_widths} as model_env) ~ret:(id, _) mem = @@ -544,6 +568,7 @@ module Call = struct ; -"__exit" <>--> bottom ; -"exit" <>--> bottom ; -"fgetc" <>--> by_value Dom.Val.Itv.m1_255 + ; -"fgets" <>$ capt_exp $+ capt_exp $+...$--> fgets ; -"infer_print" <>$ capt_exp $!--> infer_print ; -"malloc" <>$ capt_exp $+...$--> malloc ; -"calloc" <>$ capt_exp $+ capt_exp $!--> calloc diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 72a443253..498966a4d 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -115,6 +115,8 @@ module ItvPure = struct let mone = of_bound Bound.mone + let zero_255 = (Bound.zero, Bound._255) + let m1_255 = (Bound.minus_one, Bound._255) let nat = (Bound.zero, Bound.PInf) @@ -464,6 +466,8 @@ let get_bound itv (be : Symb.BoundEnd.t) = let false_sem = NonBottom ItvPure.false_sem +let zero_255 = NonBottom ItvPure.zero_255 + let m1_255 = NonBottom ItvPure.m1_255 let nat = NonBottom ItvPure.nat diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index f4e0b0aff..826b6f143 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -107,6 +107,9 @@ val compare : t -> t -> int val bot : t (** _|_ *) +val zero_255 : t +(** [0, 255] *) + val m1_255 : t (** [-1, 255] *) diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c b/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c index 9e8d09162..0abecb03f 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c @@ -4,6 +4,7 @@ * This source code is licensed under the MIT license found in the * LICENSE file in the root directory of this source tree. */ +#include int check_sorted_arr_good_FP(int a[], int length) { for (int i = 1; i < length; i++) { @@ -212,3 +213,43 @@ void strlen_malloc_2_Good_FP() { s[5] = '\0'; a[strlen(s)] = 0; } + +void fgets_null_check_Good_FP() { + char line[100]; + while (fgets(line, 100, stdin)) { + line[strlen(line) - 1] = 0; + } +} + +void fgets_null_check_Bad() { + char line[100]; + while (fgets(line, 100, stdin)) { + line[strlen(line) - 2] = 0; + } +} + +static char file_buf[] = "foo"; + +void fgets_may_not_change_str_Good_FP() { + FILE* stream = fmemopen(file_buf, strlen(file_buf), "r"); + fgetc(stream); + fgetc(stream); + fgetc(stream); + char buf[6] = "aaaaa"; + // end-of-file is encountered, thus [buf] should not change. + fgets(buf, 6, stream); + int a[5]; + a[9 - strlen(buf)] = 0; +} + +void fgets_may_not_change_str_Bad() { + FILE* stream = fmemopen(file_buf, strlen(file_buf), "r"); + fgetc(stream); + fgetc(stream); + fgetc(stream); + char buf[6] = "aaaaa"; + // end-of-file is encountered, thus [buf] should not change. + fgets(buf, 6, stream); + int a[5]; + a[strlen(buf)] = 0; +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index b9f144844..5f4363cdd 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -52,6 +52,12 @@ codetoanalyze/c/bufferoverrun/array_content.c, call_literal_string_parameter2_Ba codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr10_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_ptr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] +codetoanalyze/c/bufferoverrun/array_content.c, fgets_may_not_change_str_Bad, 9, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Array declaration,,Array declaration,Array access: Offset: [0, 5] Size: 5] +codetoanalyze/c/bufferoverrun/array_content.c, fgets_may_not_change_str_Good_FP, 9, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Array declaration,,Array declaration,Array access: Offset: [4, 9] Size: 5] +codetoanalyze/c/bufferoverrun/array_content.c, fgets_null_check_Bad, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Array declaration,,Array declaration,Array access: Offset: [-2, 97] Size: 100] +codetoanalyze/c/bufferoverrun/array_content.c, fgets_null_check_Bad, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [,Array declaration,Binary operation: ([0, 99] - 2):unsigned64] +codetoanalyze/c/bufferoverrun/array_content.c, fgets_null_check_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Array declaration,,Array declaration,Array access: Offset: [-1, 98] Size: 100] +codetoanalyze/c/bufferoverrun/array_content.c, fgets_null_check_Good_FP, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [,Array declaration,Binary operation: ([0, 99] - 1):unsigned64] codetoanalyze/c/bufferoverrun/array_content.c, literal_string_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/array_content.c, literal_string_bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Array declaration,Array access: Offset: [0, 111] Size: 1] codetoanalyze/c/bufferoverrun/array_content.c, strlen_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,,Array declaration,Array access: Offset: 5 Size: 5] @@ -203,10 +209,12 @@ codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop_narrowing_Good, 5, COND codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, 10] Size: 10] codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 7, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] +codetoanalyze/c/bufferoverrun/pointer_arith.c, FP_pointer_arith5_Ok, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Array declaration,Assignment,,Array declaration,Array access: Offset: [3, 2043] (⇐ [0, 1020] + [3, 1023]) Size: 1024] codetoanalyze/c/bufferoverrun/pointer_arith.c, array_pointer_arith_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 10 (⇐ 5 + 5) Size: 10] codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith3_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,,Parameter `x`,,Parameter `*p`,Array access: Offset: 10 (⇐ 100 + -90) Size: 5 by call to `pointer_arith3` ] codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith4_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,Call,,Parameter `*x`,,Array declaration,Array access: Offset: 10 (⇐ 100 + -90) Size: 5 by call to `FN_pointer_arith4_Bad` ] codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith4_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `x`,,Array declaration,Array access: Offset: 10 (⇐ x + -x + 10) Size: 5] +codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith5_Bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Array declaration,Assignment,,Array declaration,Array access: Offset: [4, 2044] (⇐ [0, 1020] + [4, 1024]) Size: 1024] codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/prune_alias.c, FP_call_prune_arrblk_eq_Ok, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,,Parameter `*x`,Array access: Offset: 5 Size: 5 by call to `prune_arrblk_eq_CAF` ] codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 1 Size: 1] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/pointer_arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/pointer_arith.c index b09fc733a..dc9738a40 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/pointer_arith.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/pointer_arith.c @@ -60,7 +60,7 @@ void call_pointer_arith4_Bad() { #include #include -void pointer_arith5_Ok() { +void FP_pointer_arith5_Ok() { char buf[1024]; fgets(buf, 1024, stdin); size_t len = strlen(buf); @@ -69,7 +69,7 @@ void pointer_arith5_Ok() { } } -void FN_pointer_arith5_Bad() { +void pointer_arith5_Bad() { char buf[1024]; fgets(buf, 1024, stdin); size_t len = strlen(buf);