From f521e5fbc0b1692d47a9698b002f4e11d6c297bd Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Wed, 31 May 2017 06:10:42 -0700 Subject: [PATCH] [inferbo] Models for exit, fgetc Summary: - model `exit` as `Bottom` - model `fgetc` as returning `[-1; 255]` rather than `[-1; +oo]` - reduced the number of model functions for simple models Reviewed By: KihongHeo Differential Revision: D5137485 fbshipit-source-id: 943eeeb --- .../src/bufferoverrun/bufferOverrunChecker.ml | 36 ++++++--------- .../codetoanalyze/c/bufferoverrun/issues.exp | 2 + .../codetoanalyze/c/bufferoverrun/models.c | 45 +++++++++++++++++++ 3 files changed, 60 insertions(+), 23 deletions(-) create mode 100644 infer/tests/codetoanalyze/c/bufferoverrun/models.c diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 169cb67ed..522415760 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -67,25 +67,12 @@ struct = fun pname ret params node mem -> model_malloc pname ret (List.tl_exn params) node mem - let model_fgetc : (Ident.t * Typ.t) option -> Dom.Mem.astate -> Dom.Mem.astate - = fun ret mem -> - match ret with - | Some (id, _) -> - let itv = Itv.make (Itv.Bound.of_int (-1)) Itv.Bound.PInf in - Dom.Mem.add_stack (Loc.of_id id) (Dom.Val.of_itv itv) mem - | _ -> mem - - let model_natual_itv : (Ident.t * Typ.t) option -> Dom.Mem.astate -> Dom.Mem.astate - = fun ret mem -> - match ret with - | Some (id, _) -> Dom.Mem.add_stack (Loc.of_id id) Dom.Val.Itv.nat mem - | _ -> mem - - let model_unknown_itv : (Ident.t * Typ.t) option -> Dom.Mem.astate -> Dom.Mem.astate - = fun ret mem -> - match ret with - Some (id, _) -> Dom.Mem.add_stack (Loc.of_id id) Dom.Val.Itv.top mem - | None -> mem + let model_by_value value ret mem = + match ret with + | Some (id, _) -> + Dom.Mem.add_stack (Loc.of_id id) value mem + | None -> + mem let model_infer_print : (Exp.t * Typ.t) list -> Dom.Mem.astate -> Location.t -> Dom.Mem.astate @@ -120,14 +107,17 @@ struct -> Dom.Mem.astate = fun pname ret callee_pname params node mem loc -> match Typ.Procname.get_method callee_pname with + | "__exit" + | "exit" -> Dom.Mem.Bottom + | "fgetc" -> model_by_value Dom.Val.Itv.m1_255 ret mem + | "infer_print" -> model_infer_print params mem loc | "malloc" | "__new_array" -> model_malloc pname ret params node mem | "realloc" -> model_realloc pname ret params node mem - | "strlen" -> model_natual_itv ret mem - | "fgetc" -> model_fgetc ret mem - | "infer_print" -> model_infer_print params mem loc | "__set_array_length" -> model_infer_set_array_length pname node params mem loc - | _ -> model_unknown_itv ret mem + | "strlen" -> model_by_value Dom.Val.Itv.nat ret mem + | _ -> + model_by_value Dom.Val.Itv.top ret mem let rec declare_array : Typ.Procname.t -> CFG.node -> Loc.t -> Typ.t -> length:IntLit.t option -> ?stride:int diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 1a886422f..31c79cf3e 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -8,6 +8,8 @@ codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN, codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN, [Offset: [100, 100] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:17:3 by call `arr_access()` ] codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/global.c:14:5] codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN, [Offset: [10, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/goto_loop.c:24:3] +codetoanalyze/c/bufferoverrun/models.c, fgetc_255_bad, 4, BUFFER_OVERRUN, [Offset: [0, 255] Size: [255, 255] @ codetoanalyze/c/bufferoverrun/models.c:29:5] +codetoanalyze/c/bufferoverrun/models.c, fgetc_m1_bad, 3, BUFFER_OVERRUN, [Offset: [-1, 255] Size: [10000, 10000] @ codetoanalyze/c/bufferoverrun/models.c:22:3] codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN, [Offset: [0, 10] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop.c:20:7] codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop_with_label.c:19:5] codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/pointer_arith.c:14:5] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/models.c b/infer/tests/codetoanalyze/c/bufferoverrun/models.c new file mode 100644 index 000000000..7c25c5953 --- /dev/null +++ b/infer/tests/codetoanalyze/c/bufferoverrun/models.c @@ -0,0 +1,45 @@ +/* + * Copyright (c) 2017 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ +#include +#include + +void exit_good() { + int arr[1]; + exit(1); + // unreachable + arr[42] = 42; +} + +void fgetc_m1_bad(FILE* f) { + int arr[10000]; + int c = fgetc(f); + arr[c] = 42; +} + +void fgetc_255_bad(FILE* f) { + int arr[255]; + int c = fgetc(f); + if (c >= 0) { + arr[c] = 42; + } +} + +void fgetc_256_good(FILE* f) { + int arr[256]; + int c = fgetc(f); + if (c >= 0) { + arr[c] = 42; + } +} + +void fgetc_257_good(FILE* f) { + int arr[257]; + int c = fgetc(f); + arr[c + 1] = 42; +}