pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[inferbo] Add fgets model

Browse Source 
Summary: It adds the fgets model.

Reviewed By: mbouaziz

Differential Revision: D13634754

fbshipit-source-id: 147745483
master
Sungkeun Cho 6 years ago committed by Facebook Github Bot
parent 58cdefc118
commit 9bd1191669
7 changed files with 85 additions and 2 deletions
Show Stats Download Patch File Download Diff File

2
infer/src/bufferoverrun/bufferOverrunDomain.ml
Unescape View File

@ -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

25
infer/src/bufferoverrun/bufferOverrunModels.ml
Unescape View File

@ -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

4
infer/src/bufferoverrun/itv.ml
Unescape View File

@ -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

3
infer/src/bufferoverrun/itv.mli
Unescape View File

@ -107,6 +107,9 @@ val compare : t -> t -> int
val bot : t
(** _|_ *)
val zero_255 : t
(** [0, 255] *)
val m1_255 : t
(** [-1, 255] *)

41
infer/tests/codetoanalyze/c/bufferoverrun/array_content.c
Unescape View File

@ -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 <stdio.h>
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;
}

8
infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
Unescape View File

@ -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, [<Offset trace>,Array declaration,<Length trace>,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, [<Offset trace>,Array declaration,<Length trace>,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, [<Offset trace>,Array declaration,<Length trace>,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, [<LHS trace>,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, [<Offset trace>,Array declaration,<Length trace>,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, [<LHS trace>,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, [<Length trace>,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, [<Offset trace>,Array declaration,<Length trace>,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, [<Offset trace>,Assignment,<Length trace>,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, [<Offset trace>,Array declaration,Assignment,<Length trace>,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, [<Length trace>,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,<Offset trace>,Parameter `x`,<Length trace>,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,<Offset trace>,Parameter `*x`,<Length trace>,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, [<Offset trace>,Parameter `x`,<Length trace>,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, [<Offset trace>,Array declaration,Assignment,<Length trace>,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, [<Length trace>,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,<Length trace>,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, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]

4
infer/tests/codetoanalyze/c/bufferoverrun/pointer_arith.c
Unescape View File

@ -60,7 +60,7 @@ void call_pointer_arith4_Bad() {
#include <stdio.h>
#include <stdlib.h>
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);

Write Preview
Loading…
Cancel
Save