[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

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

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]

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 <stdio.h>
+#include <stdlib.h>
+
+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;
+}