Inferbo

Summary:
This commit is for Inferbo: Infer-based buffer overrun analyzer.
Closes facebook#549

Reviewed By: jvillard

Differential Revision: D4439297

Pulled By: sblackshear

fbshipit-source-id: ddfb5ba

CONTRIBUTORS

@@ -0,0 +1,3 @@
+Kihong Heo <khheo@ropas.snu.ac.kr>
+Sungkeun Cho <skcho@ropas.snu.ac.kr>
+Kwangkeun Yi <kwang@ropas.snu.ac.kr>

Makefile

@@ -38,7 +38,7 @@ endif
 
 DIRECT_TESTS=
 ifeq ($(BUILD_C_ANALYZERS),yes)
-DIRECT_TESTS += c_errors c_frontend cpp_checkers cpp_errors cpp_frontend cpp_quandary
+DIRECT_TESTS += c_errors c_frontend c_bufferoverrun cpp_checkers cpp_errors cpp_frontend cpp_quandary
 endif
 ifeq ($(BUILD_JAVA_ANALYZERS),yes)
 DIRECT_TESTS += \

infer/src/IR/Localise.ml

@@ -32,6 +32,7 @@ let analysis_stops = "ANALYSIS_STOPS"
 let array_out_of_bounds_l1 = "ARRAY_OUT_OF_BOUNDS_L1"
 let array_out_of_bounds_l2 = "ARRAY_OUT_OF_BOUNDS_L2"
 let array_out_of_bounds_l3 = "ARRAY_OUT_OF_BOUNDS_L3"
+let buffer_overrun = "BUFFER_OVERRUN"
 let class_cast_exception = "CLASS_CAST_EXCEPTION"
 let comparing_floats_for_equality = "COMPARING_FLOAT_FOR_EQUALITY"
 let condition_is_assignment = "CONDITION_IS_ASSIGNMENT"
@@ -718,6 +719,10 @@ let desc_leak hpred_type_opt value_str_opt resource_opt resource_action_opt loc
   { no_desc with descriptions = bucket_str :: xxx_allocated_to @ by_call_to @ is_not_rxxx_after;
                  tags = !tags }
 
+let desc_buffer_overrun bucket desc =
+  let err_desc = { no_desc with descriptions = [desc]; } in
+  error_desc_set_bucket err_desc bucket Config.show_buckets
+
 (** kind of precondition not met *)
 type pnm_kind =
   | Pnm_bounds

infer/src/IR/Localise.mli

@@ -30,6 +30,7 @@ val analysis_stops : t
 val array_out_of_bounds_l1 : t
 val array_out_of_bounds_l2 : t
 val array_out_of_bounds_l3 : t
+val buffer_overrun : t
 val class_cast_exception : t
 val comparing_floats_for_equality : t
 val condition_is_assignment : t
@@ -214,6 +215,8 @@ val desc_leak :
   Exp.t option -> string option -> PredSymb.resource option -> PredSymb.res_action option ->
   Location.t -> string option -> error_desc
 
+val desc_buffer_overrun : string -> string -> error_desc
+
 val desc_null_test_after_dereference : string -> int -> Location.t -> error_desc
 
 val java_unchecked_exn_desc : Procname.t -> Typename.t -> string -> error_desc

infer/src/IR/Procdesc.re

@@ -294,7 +294,8 @@ type t = {
   mutable nodes: list Node.t, /** list of nodes of this procedure */
   mutable nodes_num: int, /** number of nodes */
   mutable start_node: Node.t, /** start node of this procedure */
-  mutable exit_node: Node.t /** exit node of ths procedure */
+  mutable exit_node: Node.t, /** exit node of ths procedure */
+  mutable loop_heads: option NodeSet.t /** loop head nodes of this procedure */
 }
 [@@deriving compare];
 
@@ -307,7 +308,7 @@ let from_proc_attributes called_from_cfg::called_from_cfg attributes => {
   let pname_opt = Some attributes.ProcAttributes.proc_name;
   let start_node = Node.dummy pname_opt;
   let exit_node = Node.dummy pname_opt;
-  {attributes, nodes: [], nodes_num: 0, start_node, exit_node}
+  {attributes, nodes: [], nodes_num: 0, start_node, exit_node, loop_heads: None}
 };
 
 
@@ -518,3 +519,41 @@ let node_set_succs_exn pdesc (node: Node.t) succs exn =>
     set_succs_exn_base node' [exit_node] exn
   | _ => set_succs_exn_base node succs exn
   };
+
+
+/** Get loop heads for widening.
+    It collects all target nodes of back-edges in a depth-first
+    traversal.
+    */
+let get_loop_heads pdesc => {
+  let rec set_loop_head_rec visited heads wl =>
+    switch wl {
+    | [] => heads
+    | [(n, ancester), ...wl'] =>
+      if (NodeSet.mem n visited) {
+        if (NodeSet.mem n ancester) {
+          set_loop_head_rec visited (NodeSet.add n heads) wl'
+        } else {
+          set_loop_head_rec visited heads wl'
+        }
+      } else {
+        let ancester = NodeSet.add n ancester;
+        let succs = IList.append (Node.get_succs n) (Node.get_exn n);
+        let works = IList.map (fun m => (m, ancester)) succs;
+        set_loop_head_rec (NodeSet.add n visited) heads (IList.append works wl')
+      }
+    };
+  let start_wl = [(get_start_node pdesc, NodeSet.empty)];
+  let lh = set_loop_head_rec NodeSet.empty NodeSet.empty start_wl;
+  pdesc.loop_heads = Some lh;
+  lh
+};
+
+let is_loop_head pdesc (node: Node.t) => {
+  let lh =
+    switch pdesc.loop_heads {
+    | Some lh => lh
+    | None => get_loop_heads pdesc
+    };
+  NodeSet.mem node lh
+};

infer/src/IR/Procdesc.rei

@@ -166,6 +166,10 @@ let fold_calls: ('a => (Procname.t, Location.t) => 'a) => 'a => t => 'a;
 let fold_instrs: ('a => Node.t => Sil.instr => 'a) => 'a => t => 'a;
 
 
+/** fold over all nodes */
+let fold_nodes: ('a => Node.t => 'a) => 'a => t => 'a;
+
+
 /** Only call from Cfg. */
 let from_proc_attributes: called_from_cfg::bool => ProcAttributes.t => t;
 
@@ -274,3 +278,5 @@ let set_start_node: t => Node.t => unit;
 
 /** indicate that we have performed preanalysis on the CFG assoociated with [t] */
 let signal_did_preanalysis: t => unit;
+
+let is_loop_head: t => Node.t => bool;

infer/src/Makefile

@@ -121,7 +121,7 @@ else
 EXTRA_DEPS = opensource
 endif
 
-DEPENDENCIES = IR backend base checkers eradicate harness integration tp/fts quandary $(EXTRA_DEPS)
+DEPENDENCIES = IR backend base checkers eradicate harness integration tp/fts quandary bufferoverrun $(EXTRA_DEPS)
 
 # ocamlbuild command with options common to all build targets
 OCAMLBUILD_BASE = rebuild $(OCAMLBUILD_OPTIONS) -j $(NCPU) $(addprefix -I , $(DEPENDENCIES))

infer/src/backend/InferPrint.re

@@ -316,6 +316,7 @@ let should_report (issue_kind: Exceptions.err_kind) issue_type error_desc eclass
       | Checkers
       | Eradicate
       | Tracing => true
+      | Bufferoverrun
       | Capture
       | Compile
       | Crashcontext
@@ -347,7 +348,8 @@ let should_report (issue_kind: Exceptions.err_kind) issue_type error_desc eclass
             ];
           IList.mem Localise.equal issue_type null_deref_issue_types
         };
-        if issue_type_is_null_deref {
+        let issue_type_is_buffer_overrun = Localise.equal issue_type Localise.buffer_overrun;
+        if (issue_type_is_null_deref || issue_type_is_buffer_overrun) {
           let issue_bucket_is_high = {
             let issue_bucket = Localise.error_desc_get_bucket error_desc;
             let high_buckets = Localise.BucketLevel.[b1, b2];

infer/src/backend/infer.ml

@@ -319,7 +319,7 @@ let analyze driver_mode =
         false, false
     | _, (Capture | Compile) ->
         false, false
-    | _, (Infer | Eradicate | Checkers | Tracing | Crashcontext | Quandary | Threadsafety) ->
+    | _, (Infer | Eradicate | Checkers | Tracing | Crashcontext | Quandary | Threadsafety | Bufferoverrun) ->
         true, true
     | _, Linters ->
         false, true in

infer/src/backend/specs.ml

@@ -327,6 +327,7 @@ type payload =
     quandary : QuandarySummary.t option;
     siof : SiofDomain.astate option;
     threadsafety : ThreadSafetyDomain.summary option;
+    buffer_overrun : BufferOverrunDomain.Summary.t option;
   }
 
 type summary =
@@ -455,17 +456,18 @@ let pp_summary_no_stats_specs fmt summary =
   F.fprintf fmt "%a@\n" pp_pair (describe_phase summary);
   F.fprintf fmt "Dependency_map: @[%a@]@\n" pp_dependency_map summary.dependency_map
 
-let pp_payload pe fmt { preposts; typestate; crashcontext_frame; quandary; siof; threadsafety } =
+let pp_payload pe fmt { preposts; typestate; crashcontext_frame; quandary; siof; threadsafety; buffer_overrun } =
   let pp_opt pp fmt = function
     | Some x -> pp fmt x
     | None -> () in
-  F.fprintf fmt "%a%a%a%a%a%a@\n"
+  F.fprintf fmt "%a%a%a%a%a%a%a@\n"
     (pp_specs pe) (get_specs_from_preposts preposts)
     (pp_opt (TypeState.pp TypeState.unit_ext)) typestate
     (pp_opt Crashcontext.pp_stacktree) crashcontext_frame
     (pp_opt QuandarySummary.pp) quandary
     (pp_opt SiofDomain.pp) siof
     (pp_opt ThreadSafetyDomain.pp_summary) threadsafety
+    (pp_opt BufferOverrunDomain.Summary.pp) buffer_overrun
 
 
 let pp_summary_text ~whole_seconds fmt summary =
@@ -753,6 +755,7 @@ let empty_payload =
     quandary = None;
     siof = None;
     threadsafety = None;
+    buffer_overrun = None;
   }
 
 (** [init_summary (depend_list, nodes,

infer/src/backend/specs.mli

@@ -136,6 +136,7 @@ type payload =
     quandary : QuandarySummary.t option;
     siof : SiofDomain.astate option;
     threadsafety : ThreadSafetyDomain.summary option;
+    buffer_overrun : BufferOverrunDomain.Summary.t option;
   }
 
 (** Procedure summary *)

infer/src/base/Config.ml

@@ -18,16 +18,18 @@ module CLOpt = CommandLineOption
 module F = Format
 
 
-type analyzer = Capture | Compile | Infer | Eradicate | Checkers | Tracing
-              | Crashcontext | Linters | Quandary | Threadsafety [@@deriving compare]
+type analyzer =
+    Capture | Compile | Infer | Eradicate | Checkers | Tracing | Crashcontext | Linters | Quandary
+  | Threadsafety | Bufferoverrun [@@deriving compare]
 
 let equal_analyzer = [%compare.equal : analyzer]
 
 let string_to_analyzer =
   [("capture", Capture); ("compile", Compile);
    ("infer", Infer); ("eradicate", Eradicate); ("checkers", Checkers);
    ("tracing", Tracing); ("crashcontext", Crashcontext); ("linters", Linters);
-   ("quandary", Quandary); ("threadsafety", Threadsafety)]
+   ("quandary", Quandary); ("threadsafety", Threadsafety);
+   ("bufferoverrun", Bufferoverrun)]
 
 let string_of_analyzer a =
   IList.find (fun (_, a') -> equal_analyzer a a') string_to_analyzer |> fst
@@ -449,11 +451,11 @@ and analyzer =
     (* NOTE: if compilation fails here, it means you have added a new analyzer without updating the
        documentation of this option *)
     | Capture | Compile | Infer | Eradicate | Checkers | Tracing | Crashcontext | Linters
-    | Quandary | Threadsafety -> () in
+    | Quandary | Threadsafety | Bufferoverrun -> () in
   CLOpt.mk_symbol_opt ~deprecated:["analyzer"] ~long:"analyzer" ~short:"a"
     ~exes:CLOpt.[Driver]
     "Specify which analyzer to run (only one at a time is supported):\n\
-     - infer, eradicate, checkers, quandary, threadsafety: run the specified analysis\n\
+     - infer, eradicate, checkers, quandary, threadsafety, bufferoverrun: run the specified analysis\n\
      - capture: run capture phase only (no analysis)\n\
      - compile: run compilation command without interfering (not supported by all frontends)\n\
      - crashcontext, tracing: experimental (see --crashcontext and --tracing)\n\
@@ -490,6 +492,10 @@ and bootclasspath =
     ~exes:CLOpt.[Driver]
     "Specify the Java bootclasspath"
 
+and bo_debug =
+  CLOpt.mk_int ~default:0 ~long:"bo-debug"
+    ~exes:CLOpt.[Driver] "Debug mode for buffer-overrun checker"
+
 (** Automatically set when running from within Buck *)
 and buck =
   CLOpt.mk_bool ~long:"buck"
@@ -548,7 +554,7 @@ and check_duplicate_symbols =
     ~exes:CLOpt.[Analyze]
     "Check if a symbol with the same name is defined in more than one file."
 
-and checkers, crashcontext, eradicate, quandary, threadsafety =
+and checkers, crashcontext, eradicate, quandary, threadsafety, bufferoverrun =
   let checkers =
     CLOpt.mk_bool ~deprecated:["checkers"] ~long:"checkers"
       "Activate the checkers instead of the full analysis"
@@ -573,7 +579,12 @@ and checkers, crashcontext, eradicate, quandary, threadsafety =
       "Activate the thread safety analysis"
       [checkers] []
   in
-  (checkers, crashcontext, eradicate, quandary, threadsafety)
+  let bufferoverrun =
+    CLOpt.mk_bool_group ~deprecated:["bufferoverrun"] ~long:"bufferoverrn"
+      "Activate the buffer overrun analysis"
+      [checkers] []
+  in
+  (checkers, crashcontext, eradicate, quandary, threadsafety, bufferoverrun)
 
 and checkers_repeated_calls =
   CLOpt.mk_bool ~long:"checkers-repeated-calls"
@@ -1352,6 +1363,7 @@ let post_parsing_initialization () =
   | Some Eradicate -> checkers := true; eradicate := true
   | Some Quandary -> checkers := true; quandary := true
   | Some Threadsafety -> checkers := true; threadsafety := true
+  | Some Bufferoverrun -> checkers := true; bufferoverrun := true
   | Some Tracing -> tracing := true
   | Some (Capture | Compile | Infer | Linters) | None -> ()
 
@@ -1387,9 +1399,11 @@ and array_level = !array_level
 and ast_file = !ast_file
 and blacklist = !blacklist
 and bootclasspath = !bootclasspath
+and bo_debug = !bo_debug
 and buck = !buck
 and buck_build_args = !buck_build_args
 and buck_out = !buck_out
+and bufferoverrun = !bufferoverrun
 and bugs_csv = !bugs_csv
 and bugs_json = !bugs_json
 and frontend_tests = !frontend_tests

infer/src/base/Config.mli

@@ -15,8 +15,9 @@ open! IStd
 
 
 (** Various kind of analyzers *)
-type analyzer = Capture | Compile | Infer | Eradicate | Checkers | Tracing
-              | Crashcontext | Linters | Quandary | Threadsafety [@@deriving compare]
+type analyzer =
+    Capture | Compile | Infer | Eradicate | Checkers | Tracing | Crashcontext | Linters | Quandary
+  | Threadsafety | Bufferoverrun [@@deriving compare]
 
 val equal_analyzer : analyzer -> analyzer -> bool
 
@@ -149,9 +150,11 @@ val array_level : int
 val ast_file : string option
 val blacklist : string option
 val bootclasspath : string option
+val bo_debug : int
 val buck : bool
 val buck_build_args : string list
 val buck_out : string option
+val bufferoverrun : bool
 val bugs_csv : string option
 val bugs_json : string option
 val bugs_tests : string option

infer/src/bufferoverrun/absLoc.ml

@@ -0,0 +1,76 @@
+(*
+ * Copyright (c) 2016 - present
+ *
+ * Programming Research Laboratory (ROPAS)
+ * Seoul National University, Korea
+ * 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.
+ *)
+
+module F = Format
+
+module Allocsite =
+struct
+  include String
+  let pp fmt s = Format.fprintf fmt "%s" s
+  let make x = x
+end
+
+module Loc =
+struct
+  type t =
+    | Var of Var.t
+    | Allocsite of Allocsite.t
+    | Field of t * Ident.fieldname
+  [@@deriving compare]
+
+  let rec pp fmt = function
+    | Var v ->
+        Var.pp F.str_formatter v;
+        let s = F.flush_str_formatter () in
+        if s.[0] = '&' then
+          F.fprintf fmt "%s" (String.sub s 1 (String.length s - 1))
+        else F.fprintf fmt "%s" s
+    | Allocsite a -> Allocsite.pp fmt a
+    | Field (l, f) -> F.fprintf fmt "%a.%a" pp l Ident.pp_fieldname f
+  let is_var = function Var _ -> true | _ -> false
+  let is_pvar_in_reg v =
+    Var.pp F.str_formatter v;
+    let s = F.flush_str_formatter () in
+    s.[0] = '&'
+  let is_logical_var = function
+    | Var (Var.LogicalVar _) -> true
+    | _ -> false
+  let of_var v = Var v
+  let of_allocsite a = Allocsite a
+  let of_pvar pvar = Var (Var.of_pvar pvar)
+  let of_id id = Var (Var.of_id id)
+  let append_field l f = Field (l, f)
+
+  let is_return = function
+    | Var (Var.ProgramVar x) ->
+        Mangled.equal (Pvar.get_name x) Ident.name_return
+    | _ -> false
+end
+
+module PowLoc =
+struct
+  include AbstractDomain.FiniteSet
+      (struct
+        include Set.Make (struct type t = Loc.t [@@deriving compare] end)
+        let pp_element fmt e = Loc.pp fmt e
+        let pp fmt s =
+          Format.fprintf fmt "{";
+          iter (fun e -> Format.fprintf fmt "%a," pp_element e) s;
+          Format.fprintf fmt "}"
+      end)
+
+  let bot = empty
+
+  let of_pvar pvar = singleton (Loc.of_pvar pvar)
+  let of_id id = singleton (Loc.of_id id)
+  let append_field ploc fn = fold (fun l -> add (Loc.append_field l fn)) ploc empty
+end