From 2e8cb343d494f51d446b84ef83e2e7d01123ff40 Mon Sep 17 00:00:00 2001
From: Mehdi Bouaziz <mbouaziz@fb.com>
Date: Wed, 14 Mar 2018 07:02:19 -0700
Subject: [PATCH] [Inferbo] Itv.mli

Reviewed By: skcho

Differential Revision: D7255738

fbshipit-source-id: cef7878
---
 .../bufferOverrunProofObligations.ml          |   5 +-
 .../bufferoverrun/bufferOverrunSemantics.ml   |  14 +-
 infer/src/bufferoverrun/itv.ml                |   2 +
 infer/src/bufferoverrun/itv.mli               | 208 ++++++++++++++++++
 4 files changed, 216 insertions(+), 13 deletions(-)
 create mode 100644 infer/src/bufferoverrun/itv.mli

diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
index c706cb84f..25991766e 100644
--- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
+++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
@@ -164,9 +164,8 @@ module ArrayAccessCondition = struct
 
   let filter1 : t -> bool =
    fun c ->
-    ItvPure.is_top c.idx || ItvPure.is_top c.size || Itv.Bound.eq (ItvPure.lb c.idx) Itv.Bound.MInf
-    || Itv.Bound.eq (ItvPure.lb c.size) Itv.Bound.MInf
-    || ItvPure.is_nat c.idx && ItvPure.is_nat c.size
+    ItvPure.is_top c.idx || ItvPure.is_top c.size || ItvPure.is_lb_infty c.idx
+    || ItvPure.is_lb_infty c.size || ItvPure.is_nat c.idx && ItvPure.is_nat c.size
 
 
   let filter2 : t -> bool =
diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
index 547dc85cc..301572d6b 100644
--- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml
+++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
@@ -539,16 +539,10 @@ module Make (CFG : ProcCfg.S) = struct
         -> Itv.Bound.t bottom_lifted Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t =
    fun pairs ->
     let add_pair (bound_map, trace_map) (formal, actual, traces) =
-      match formal with
-      | Itv.Bound.Linear (_, se1) when Itv.SymLinear.is_zero se1 ->
-          (bound_map, trace_map)
-      | Itv.Bound.Linear (0, se1) ->
-          let symbol = Itv.SymLinear.get_one_symbol se1 in
-          (Itv.SubstMap.add symbol actual bound_map, Itv.SubstMap.add symbol traces trace_map)
-      | Itv.Bound.MinMax (0, Itv.Bound.Plus, Itv.Bound.Max, 0, symbol) ->
-          (Itv.SubstMap.add symbol actual bound_map, Itv.SubstMap.add symbol traces trace_map)
-      | _ ->
-          assert false
+      if Itv.Bound.is_const formal |> Option.is_some then (bound_map, trace_map)
+      else
+        let symbol = Itv.Bound.get_one_symbol formal in
+        (Itv.SubstMap.add symbol actual bound_map, Itv.SubstMap.add symbol traces trace_map)
     in
     List.fold ~f:add_pair ~init:(Itv.SubstMap.empty, Itv.SubstMap.empty) pairs
 
diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml
index 468cf998d..4fcaa1dac 100644
--- a/infer/src/bufferoverrun/itv.ml
+++ b/infer/src/bufferoverrun/itv.ml
@@ -831,6 +831,8 @@ module ItvPure = struct
 
   let ub : t -> Bound.t = snd
 
+  let is_lb_infty : t -> bool = function MInf, _ -> true | _ -> false
+
   let is_finite : t -> bool =
    fun (l, u) ->
     match (Bound.is_const l, Bound.is_const u) with Some _, Some _ -> true | _, _ -> false
diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli
new file mode 100644
index 000000000..43f4ef4a5
--- /dev/null
+++ b/infer/src/bufferoverrun/itv.mli
@@ -0,0 +1,208 @@
+(*
+ * Copyright (c) 2018 - 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.
+ *)
+
+open! IStd
+open! AbstractDomain.Types
+module F = Format
+
+module Symbol : sig
+  type t
+end
+
+module SubstMap : Caml.Map.S with type key = Symbol.t
+
+module Bound : sig
+  type t [@@deriving compare]
+
+  val pp : F.formatter -> t -> unit
+
+  val zero : t
+
+  val is_const : t -> int option
+
+  val is_not_infty : t -> bool
+
+  val is_symbolic : t -> bool
+
+  val get_one_symbol : t -> Symbol.t
+
+  val gt : t -> t -> bool
+
+  val le : t -> t -> bool
+
+  val lt : t -> t -> bool
+end
+
+module ItvPure : sig
+  type astate [@@deriving compare]
+
+  type t = astate
+
+  val pp : F.formatter -> t -> unit
+
+  val mone : t
+
+  val zero : t
+
+  val of_int : int -> t
+
+  val lb : t -> Bound.t
+
+  val ub : t -> Bound.t
+
+  val is_false : t -> bool
+
+  val is_finite : t -> bool
+
+  val is_invalid : t -> bool
+
+  val is_lb_infty : t -> bool
+
+  val is_nat : t -> bool
+
+  val is_one : t -> bool
+
+  val is_symbolic : t -> bool
+
+  val is_top : t -> bool
+
+  val is_true : t -> bool
+
+  val is_zero : t -> bool
+
+  val ( <= ) : lhs:t -> rhs:t -> bool
+
+  val equal : t -> t -> bool
+
+  val have_similar_bounds : t -> t -> bool
+
+  val make_positive : t -> t
+
+  val join : t -> t -> t
+
+  val le_sem : t -> t -> t
+
+  val lt_sem : t -> t -> t
+
+  val widen : prev:t -> next:t -> num_iters:int -> t
+
+  val xcompare :
+    lhs:t -> rhs:t
+    -> [ `Equal
+       | `LeftSmallerThanRight
+       | `RightSmallerThanLeft
+       | `NotComparable
+       | `LeftSubsumesRight
+       | `RightSubsumesLeft ]
+
+  val get_symbols : t -> Symbol.t list
+
+  val subst : t -> Bound.t bottom_lifted SubstMap.t -> t bottom_lifted
+end
+
+include module type of AbstractDomain.BottomLifted (ItvPure)
+
+type t = astate [@@deriving compare]
+
+val bot : t
+(** _|_ *)
+
+val false_sem : t
+(** 0 *)
+
+val m1_255 : t
+(** [-1, 255] *)
+
+val nat : t
+(** [0, +oo] *)
+
+val one : t
+(** 1 *)
+
+val pos : t
+(** [1, +oo] *)
+
+val top : t
+(** [-oo, +oo] *)
+
+val unknown_bool : t
+(** [0, 1] *)
+
+val zero : t
+(** 0 *)
+
+val of_int : int -> t
+
+val of_int_lit : IntLit.t -> t
+
+val of_int64 : Int64.t -> t
+
+val make_sym : ?unsigned:bool -> Typ.Procname.t -> (unit -> int) -> t
+
+val lb : t -> Bound.t
+
+val ub : t -> Bound.t
+
+val is_false : t -> bool
+
+val lnot : t -> t
+
+val neg : t -> t
+
+val normalize : t -> t
+
+val get_symbols : t -> Symbol.t list
+
+val eq : t -> t -> bool
+
+val le : lhs:t -> rhs:t -> bool
+
+val _range : t -> Bound.t
+
+val div : t -> t -> t
+
+val minus : t -> t -> t
+
+val mult : t -> t -> t
+
+val plus : t -> t -> t
+
+val shiftlt : t -> t -> t
+
+val shiftrt : t -> t -> t
+
+val eq_sem : t -> t -> t
+
+val ge_sem : t -> t -> t
+
+val gt_sem : t -> t -> t
+
+val land_sem : t -> t -> t
+
+val le_sem : t -> t -> t
+
+val lor_sem : t -> t -> t
+
+val lt_sem : t -> t -> t
+
+val min_sem : t -> t -> t
+
+val mod_sem : t -> t -> t
+
+val ne_sem : t -> t -> t
+
+val prune_zero : t -> t
+
+val prune_comp : Binop.t -> t -> t -> t
+
+val prune_eq : t -> t -> t
+
+val prune_ne : t -> t -> t
+
+val subst : t -> Bound.t bottom_lifted SubstMap.t -> t