[inferbo] Add mli files

Summary: All files in inferbo has mli files now.

Reviewed By: ngorogiannis

Differential Revision: D19094964

fbshipit-source-id: 9e9172013

infer/src/bufferoverrun/bufferOverrunAnalysisSummary.mli

@@ -0,0 +1,12 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+type t = BufferOverrunDomain.Mem.no_oenv_t
+
+val pp : Format.formatter -> t -> unit

infer/src/bufferoverrun/bufferOverrunCheckerSummary.mli

@@ -0,0 +1,12 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+type t = BufferOverrunProofObligations.ConditionSet.summary_t
+
+val pp : Format.formatter -> t -> unit

infer/src/bufferoverrun/bufferOverrunField.mli

@@ -0,0 +1,34 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+open! IStd
+
+val pp :
+     pp_lhs:(Format.formatter -> 'a -> unit)
+  -> sep:string
+  -> Format.formatter
+  -> 'a
+  -> Typ.Fieldname.t
+  -> unit
+(** A parameterized pretty printer for field appended values *)
+
+val get_type : Typ.Fieldname.t -> Typ.t option
+(** Get type of field that is constructed in this module. This does not work in Java at the moment. *)
+
+val c_strlen : unit -> Typ.Fieldname.t
+(** Field for C string's length *)
+
+val cpp_vector_elem : vec_typ:Typ.t -> elt_typ:Typ.t -> Typ.Fieldname.t
+(** Field for C++ vector's elements *)
+
+val java_collection_internal_array : Typ.Fieldname.t
+(** Field for Java collection's elements *)
+
+val is_cpp_vector_elem : Typ.Fieldname.t -> bool
+(** Check if the field is for C++ vector's elements *)
+
+val is_java_collection_internal_array : Typ.Fieldname.t -> bool
+(** Check if the field is for Java collection's elements *)

infer/src/bufferoverrun/bufferOverrunModels.mli

@@ -0,0 +1,58 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+(* Type of abstract semantic function of execution *)
+type exec_fun =
+     BufferOverrunUtils.ModelEnv.model_env
+  -> ret:Ident.t * Typ.t
+  -> BufferOverrunDomain.Mem.t
+  -> BufferOverrunDomain.Mem.t
+
+(* Type of checking function *)
+type check_fun =
+     BufferOverrunUtils.ModelEnv.model_env
+  -> BufferOverrunDomain.Mem.t
+  -> BufferOverrunProofObligations.ConditionSet.checked_t
+  -> BufferOverrunProofObligations.ConditionSet.checked_t
+
+type model = {exec: exec_fun; check: check_fun}
+
+module Collection : sig
+  val create_collection :
+       BufferOverrunUtils.ModelEnv.model_env
+    -> ret:Ident.t * Typ.t
+    -> BufferOverrunDomain.Mem.t
+    -> length:Itv.t
+    -> BufferOverrunDomain.Mem.t
+  (** Create a collection value with the [length] and assign it to [ret] *)
+
+  val eval_collection_length : Exp.t -> BufferOverrunDomain.Mem.t -> BufferOverrunDomain.Val.t
+  (** Evaluate length of Java collection *)
+end
+
+module JavaString : sig
+  val get_length :
+       BufferOverrunUtils.ModelEnv.model_env
+    -> Exp.t
+    -> BufferOverrunDomain.Mem.t
+    -> BufferOverrunDomain.Val.t
+  (** Get length of Java string *)
+
+  val constructor_from_char_ptr :
+       BufferOverrunUtils.ModelEnv.model_env
+    -> AbsLoc.PowLoc.t
+    -> Exp.t
+    -> BufferOverrunDomain.Mem.t
+    -> BufferOverrunDomain.Mem.t
+  (** Construct Java string from constant string *)
+end
+
+module Call : sig
+  val dispatch : (Tenv.t, model, unit) ProcnameDispatcher.Call.dispatcher
+end

infer/src/bufferoverrun/bufferOverrunOndemandEnv.mli

@@ -0,0 +1,19 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+(** Environment for on-demand symbol evaluation *)
+type t =
+  { tenv: Tenv.t  (** type environment *)
+  ; typ_of_param_path: Symb.SymbolPath.partial -> Typ.t option  (** type of parameter *)
+  ; may_last_field: Symb.SymbolPath.partial -> bool
+        (** if the path is a last field of a class in C++ *)
+  ; entry_location: Location.t  (** location of entry node *)
+  ; integer_type_widths: Typ.IntegerWidths.t  (** bit sizes of integer types *) }
+
+val mk : Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t -> t

infer/src/bufferoverrun/bufferOverrunSemantics.mli

@@ -0,0 +1,84 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+val is_stack_exp : Exp.t -> BufferOverrunDomain.Mem.t -> bool
+(** Check if an expression is a stack variable such as [n$0] or local variable for C array *)
+
+val eval : Typ.IntegerWidths.t -> Exp.t -> BufferOverrunDomain.Mem.t -> BufferOverrunDomain.Val.t
+(** Evalute an expression *)
+
+val eval_locs : Exp.t -> BufferOverrunDomain.Mem.t -> AbsLoc.PowLoc.t
+(** [eval_locs exp mem] is like [eval exp mem |> Val.get_all_locs] but takes some shortcuts to avoid
+    computing useless and/or problematic intermediate values *)
+
+val eval_arr :
+  Typ.IntegerWidths.t -> Exp.t -> BufferOverrunDomain.Mem.t -> BufferOverrunDomain.Val.t
+(** Return the array value of the input expression. For example, when [x] is a program variable,
+    [eval_arr x] returns array blocks the [x] is pointing to, on the other hand, [eval x] returns
+    the abstract location of [x]. *)
+
+val eval_lindex :
+  Typ.IntegerWidths.t -> Exp.t -> Exp.t -> BufferOverrunDomain.Mem.t -> BufferOverrunDomain.Val.t
+(** Evaluate array location with index, i.e.,
+    [eval_lindex integer_type_widths array_exp index_exp mem] *)
+
+val eval_array_locs_length :
+  AbsLoc.PowLoc.t -> _ BufferOverrunDomain.Mem.t0 -> BufferOverrunDomain.Val.t
+(** Evaluate length of array locations *)
+
+val conservative_array_length :
+     ?traces:BufferOverrunTrace.Set.t
+  -> AbsLoc.PowLoc.t
+  -> _ BufferOverrunDomain.Mem.t0
+  -> BufferOverrunDomain.Val.t
+(** Evaluate the array length conservatively, which is useful when there are multiple array
+    locations and their lengths are joined to top. For example, if the [arr_locs] points to two
+    arrays [a] and [b] and if their lengths are [a.length] and [b.length], this function evaluates
+    its length as [\[0, a.length.ub + b.length.ub\]]. *)
+
+(** Several modes of ondemand evaluations *)
+type eval_mode =
+  | EvalNormal
+      (** Given a symbolic value of an unknown function [Symb.SymbolPath.Callsite], it returns a
+          symbolic interval value. *)
+  | EvalPOCond
+      (** Given a symbolic value of an unknown function, it returns the top interval value. This is
+          used when substituting condition expressions of proof obligations. *)
+  | EvalPOReachability
+      (** This is similar to [EvalPOCond], but it returns the bottom location, instead of the
+          unknown location, when a location to substitute is not found. This is used when
+          substituting reachabilities of proof obligations. *)
+  | EvalCost
+      (** This is similar to [EvalNormal], but it is designed to be used in substitutions of the
+          cost results, avoiding precision loss by joining of symbolic values. Normal join of two
+          different symbolic values, [s1] and [s2], becomes top due to the limitation of our domain.
+          On the other hand, in this mode, it returns an upperbound [s1+s2] for the case, because
+          the cost values only care about the upperbounds. *)
+
+val mk_eval_sym_trace :
+     Typ.IntegerWidths.t
+  -> (Pvar.t * Typ.t) list
+  -> (Exp.t * Typ.t) list
+  -> BufferOverrunDomain.Mem.t
+  -> mode:eval_mode
+  -> BufferOverrunDomain.eval_sym_trace
+(** Make [eval_sym] function for on-demand symbol evaluation *)
+
+val mk_eval_sym_cost :
+     Typ.IntegerWidths.t
+  -> (Pvar.t * Typ.t) list
+  -> (Exp.t * Typ.t) list
+  -> BufferOverrunDomain.Mem.t
+  -> Bounds.Bound.eval_sym
+(** Make [eval_sym] function of [EvalCost] mode for on-demand symbol evaluation *)
+
+module Prune : sig
+  val prune : Typ.IntegerWidths.t -> Exp.t -> BufferOverrunDomain.Mem.t -> BufferOverrunDomain.Mem.t
+  (** Prune memory with the given condition expression *)
+end

infer/src/bufferoverrun/bufferOverrunTrace.mli

@@ -0,0 +1,74 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+(** Library function names that may be risky *)
+type lib_fun = Snprintf | Strndup | Vsnprintf
+
+val snprintf : lib_fun
+
+val strndup : lib_fun
+
+val vsnprintf : lib_fun
+
+(** Final unknown function in trace *)
+type final = UnknownFrom of Typ.Procname.t option
+
+(** Trace elements *)
+type elem =
+  | ArrayDeclaration
+  | JavaIntDecleration
+  | Assign of AbsLoc.PowLoc.t
+  | Global of AbsLoc.Loc.t
+  | Parameter of AbsLoc.Loc.t
+  | Through of {risky_fun: lib_fun option}
+
+val through : risky_fun:lib_fun option -> elem
+
+module Set : sig
+  include AbstractDomain.WithBottom
+
+  val singleton : Location.t -> elem -> t
+
+  val singleton_final : Location.t -> final -> t
+
+  val add_elem : Location.t -> elem -> t -> t
+
+  val call : Location.t -> traces_caller:t -> traces_callee:t -> t
+  (** Merge traces of [traces_caller] and [traces_callee] *)
+end
+
+(** Trace set with issue information *)
+module Issue : sig
+  include PrettyPrintable.PrintableOrderedType
+
+  type binary = ArrayAccess | Binop
+
+  val binary : Location.t -> binary -> Set.t -> Set.t -> t
+  (** Construct issue trace of binary operation. When [binary] is [ArrayAccess], the former [Set.t]
+      typed parameter is [offset] and the latter is [length] of array access. *)
+
+  val alloc : Location.t -> Set.t -> t
+  (** Construct issue trace of allocation *)
+
+  val call : Location.t -> Set.t -> t -> t
+  (** Merge caller's trace set and callee's issue, i.e., [call location caller callee] *)
+
+  val has_risky : t -> bool
+  (** Check if the issue trace includes risky function calls by [Through] *)
+
+  val has_unknown : t -> bool
+  (** Check if the issue trace includes unknown function calls *)
+
+  val exists_str : f:(string -> bool) -> t -> bool
+  (** Check if the issue trace includes an abstract location that satisfies [f] *)
+
+  val make_err_trace : description:string -> t -> (string * Errlog.loc_trace) list
+  (** Convert to the common [Errlog] format. The return value is a list of labelled
+      [Errlog.loc_trace]s. *)
+end

infer/src/bufferoverrun/bufferOverrunTypModels.mli

@@ -0,0 +1,16 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+type typ_model =
+  | CArray of {element_typ: Typ.t; deref_kind: Symb.SymbolPath.deref_kind; length: IntLit.t}
+  | CppStdVector
+  | JavaCollection
+  | JavaInteger
+
+val dispatch : (Tenv.t, typ_model, unit) ProcnameDispatcher.TypName.dispatcher