[inferbo] Move Boolean to their own module

Reviewed By: skcho

Differential Revision: D13111801

fbshipit-source-id: 6eca0e1c9

infer/src/bufferoverrun/boolean.ml

@@ -0,0 +1,41 @@
+(*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * 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 = Bottom | False | True | Top [@@deriving compare]
+
+let equal = [%compare.equal: t]
+
+let is_false = function False -> true | _ -> false
+
+let is_true = function True -> true | _ -> false
+
+let not_ = function Bottom -> Bottom | False -> True | True -> False | Top -> Top
+
+let and_ x y =
+  match (x, y) with
+  | Bottom, _ | _, Bottom ->
+      Bottom
+  | False, _ | _, False ->
+      False
+  | True, b | b, True ->
+      b
+  | Top, Top ->
+      Top
+
+
+let or_ x y =
+  match (x, y) with
+  | Bottom, _ | _, Bottom ->
+      Bottom
+  | False, b | b, False ->
+      b
+  | True, _ | _, True ->
+      True
+  | Top, Top ->
+      Top

infer/src/bufferoverrun/boolean.mli

@@ -0,0 +1,22 @@
+(*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * 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 = Bottom | False | True | Top
+
+val equal : t -> t -> bool
+
+val is_false : t -> bool
+
+val is_true : t -> bool
+
+val not_ : t -> t
+
+val and_ : t -> t -> t
+
+val or_ : t -> t -> t

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -273,13 +273,13 @@ module Init = struct
       -> Loc.t
       -> Typ.typ
       -> inst_num:int
-      -> new_sym_num:Itv.Counter.t
+      -> new_sym_num:Counter.t
       -> Dom.Mem.t
       -> Dom.Mem.t =
    fun pname symbol_table path tenv ~node_hash location ~represents_multiple_values loc typ
        ~inst_num ~new_sym_num mem ->
     let max_depth = 2 in
-    let new_alloc_num = Itv.Counter.make 1 in
+    let new_alloc_num = Counter.make 1 in
     let rec decl_sym_val pname path tenv ~node_hash location ~represents_multiple_values ~depth
         ~may_last_field loc typ mem =
       if depth > max_depth then mem
@@ -374,7 +374,7 @@ module Init = struct
       -> Dom.Mem.astate =
    fun pname tenv ~node_hash location symbol_table ~represents_multiple_values ~inst_num formals
        mem ->
-    let new_sym_num = Itv.Counter.make 0 in
+    let new_sym_num = Counter.make 0 in
     let add_formal (mem, inst_num) (pvar, typ) =
       let loc = Loc.of_pvar pvar in
       let path = Itv.SymbolPath.of_pvar pvar in

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -160,7 +160,7 @@ module Val = struct
       -> Typ.Procname.t
       -> Itv.SymbolTable.t
       -> Itv.SymbolPath.partial
-      -> Itv.Counter.t
+      -> Counter.t
       -> Location.t
       -> t =
    fun ~represents_multiple_values ?(unsigned = false) loc pname symbol_table path new_sym_num
@@ -184,9 +184,9 @@ module Val = struct
 
   let has_pointer : t -> bool = fun x -> not (PowLoc.is_bot x.powloc && ArrayBlk.is_bot x.arrayblk)
 
-  let lift_cmp_itv : (Itv.t -> Itv.t -> Itv.Boolean.t) -> t -> t -> t =
+  let lift_cmp_itv : (Itv.t -> Itv.t -> Boolean.t) -> t -> t -> t =
    fun f x y ->
-    let b = if has_pointer x || has_pointer y then Itv.Boolean.top else f x.itv y.itv in
+    let b = if has_pointer x || has_pointer y then Boolean.Top else f x.itv y.itv in
     let itv = Itv.of_bool b in
     {bot with itv; traces= TraceSet.join x.traces y.traces}
 

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -52,8 +52,8 @@ type declare_symbolic_fun =
   -> depth:int
   -> Loc.t
   -> inst_num:int
-  -> new_sym_num:Itv.Counter.t
+  -> new_sym_num:Counter.t
-  -> new_alloc_num:Itv.Counter.t
+  -> new_alloc_num:Counter.t
   -> Dom.Mem.astate
   -> Dom.Mem.astate
 

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -43,14 +43,14 @@ module AllocSizeCondition = struct
     | (`LeftSmallerThanRight | `RightSmallerThanLeft) as cmp ->
         let lpos = ItvPure.le_sem ItvPure.zero lhs in
         let rpos = ItvPure.le_sem ItvPure.zero rhs in
-        if not (Itv.Boolean.equal lpos rpos) then `NotComparable
+        if not (Boolean.equal lpos rpos) then `NotComparable
-        else if Itv.Boolean.is_true lpos then
+        else if Boolean.is_true lpos then
           match cmp with
           | `LeftSmallerThanRight ->
               `RightSubsumesLeft
           | `RightSmallerThanLeft ->
               `LeftSubsumesRight
-        else if Itv.Boolean.is_false lpos then
+        else if Boolean.is_false lpos then
           match cmp with
           | `LeftSmallerThanRight ->
               `LeftSubsumesRight
@@ -192,8 +192,8 @@ module ArrayAccessCondition = struct
       | (`Equal | `RightSmallerThanLeft), (`Equal | `RightSmallerThanLeft), _ ->
           let lidxpos = ItvPure.le_sem (ItvPure.neg lidx) loff in
           let ridxpos = ItvPure.le_sem (ItvPure.neg ridx) roff in
-          if not (Itv.Boolean.equal lidxpos ridxpos) then `NotComparable
+          if not (Boolean.equal lidxpos ridxpos) then `NotComparable
-          else if Itv.Boolean.is_true lidxpos then
+          else if Boolean.is_true lidxpos then
             (* both idx >= 0 *)
             match (offcmp, idxcmp, sizcmp) with
             | ( (`Equal | `LeftSmallerThanRight)
@@ -206,7 +206,7 @@ module ArrayAccessCondition = struct
                 `LeftSubsumesRight
             | _ ->
                 `NotComparable
-          else if Itv.Boolean.is_false lidxpos then
+          else if Boolean.is_false lidxpos then
             (* both idx < 0, size doesn't matter *)
             match (offcmp, idxcmp) with
             | `Equal, `LeftSmallerThanRight | `LeftSmallerThanRight, `Equal ->
@@ -265,18 +265,17 @@ module ArrayAccessCondition = struct
     in
     (* if sl < 0, use sl' = 0 *)
     let not_overrun =
-      if Relation.lt_sat_opt c.idx_sym_exp c.size_sym_exp c.relation then Itv.Boolean.true_
+      if Relation.lt_sat_opt c.idx_sym_exp c.size_sym_exp c.relation then Boolean.True
       else ItvPure.lt_sem real_idx size
     in
     let not_underrun =
-      if Relation.le_sat_opt (Some Relation.SymExp.zero) c.idx_sym_exp c.relation then
+      if Relation.le_sat_opt (Some Relation.SymExp.zero) c.idx_sym_exp c.relation then Boolean.True
-        Itv.Boolean.true_
       else ItvPure.le_sem ItvPure.zero real_idx
     in
     (* il >= 0 and iu < sl, definitely not an error *)
-    if Itv.Boolean.is_true not_overrun && Itv.Boolean.is_true not_underrun then
+    if Boolean.is_true not_overrun && Boolean.is_true not_underrun then
       {report_issue_type= None; propagate= false} (* iu < 0 or il >= su, definitely an error *)
-    else if Itv.Boolean.is_false not_overrun || Itv.Boolean.is_false not_underrun then
+    else if Boolean.is_false not_overrun || Boolean.is_false not_underrun then
       {report_issue_type= Some IssueType.buffer_overrun_l1; propagate= false}
       (* su <= iu < +oo, most probably an error *)
     else if

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -142,8 +142,8 @@ module Exec = struct
       -> ?size:Itv.t
       -> ?stride:int
       -> inst_num:int
-      -> new_sym_num:Itv.Counter.t
+      -> new_sym_num:Counter.t
-      -> new_alloc_num:Itv.Counter.t
+      -> new_alloc_num:Counter.t
       -> Dom.Mem.astate
       -> Dom.Mem.astate =
    fun ~decl_sym_val array_kind pname symbol_table path tenv ~node_hash location
@@ -161,7 +161,7 @@ module Exec = struct
     in
     let deref_path = Itv.SymbolPath.index ~array_kind path in
     let allocsite =
-      let alloc_num = Itv.Counter.next new_alloc_num in
+      let alloc_num = Counter.next new_alloc_num in
       Allocsite.make pname ~node_hash ~inst_num ~dimension:alloc_num ~path:(Some deref_path)
     in
     let mem =
@@ -195,12 +195,12 @@ module Exec = struct
       -> Loc.t
       -> Typ.t
       -> inst_num:int
-      -> new_alloc_num:Itv.Counter.t
+      -> new_alloc_num:Counter.t
       -> Dom.Mem.astate
       -> Dom.Mem.astate =
    fun ~decl_sym_val pname path tenv ~node_hash location ~represents_multiple_values ~depth loc typ
        ~inst_num ~new_alloc_num mem ->
-    let alloc_num = Itv.Counter.next new_alloc_num in
+    let alloc_num = Counter.next new_alloc_num in
     let elem = Trace.SymAssign (loc, location) in
     let allocsite =
       Allocsite.make pname ~node_hash ~inst_num ~dimension:alloc_num ~path:(Some path)
@@ -223,7 +223,7 @@ module Exec = struct
       -> Location.t
       -> represents_multiple_values:bool
       -> Loc.t
-      -> new_sym_num:Itv.Counter.t
+      -> new_sym_num:Counter.t
       -> Dom.Mem.astate
       -> Dom.Mem.astate =
    fun pname symbol_table path location ~represents_multiple_values loc ~new_sym_num mem ->

infer/src/bufferoverrun/bufferOverrunUtils.mli

@@ -84,8 +84,8 @@ module Exec : sig
     -> ?size:Itv.t
     -> ?stride:int
     -> inst_num:int
-    -> new_sym_num:Itv.Counter.t
+    -> new_sym_num:Counter.t
-    -> new_alloc_num:Itv.Counter.t
+    -> new_alloc_num:Counter.t
     -> Dom.Mem.astate
     -> Dom.Mem.astate
 
@@ -101,7 +101,7 @@ module Exec : sig
     -> Loc.t
     -> Typ.t
     -> inst_num:int
-    -> new_alloc_num:Itv.Counter.t
+    -> new_alloc_num:Counter.t
     -> Dom.Mem.astate
     -> Dom.Mem.astate
 
@@ -112,7 +112,7 @@ module Exec : sig
     -> Location.t
     -> represents_multiple_values:bool
     -> Loc.t
-    -> new_sym_num:Itv.Counter.t
+    -> new_sym_num:Counter.t
     -> Dom.Mem.astate
     -> Dom.Mem.astate
 

infer/src/bufferoverrun/itv.ml

@@ -12,22 +12,6 @@ open! AbstractDomain.Types
 module F = Format
 module L = Logging
 module Bound = Bounds.Bound
-module Counter = Counter
-
-module Boolean = struct
-  type t = Bottom | False | True | Top [@@deriving compare]
-
-  let top = Top
-
-  let true_ = True
-
-  let equal = [%compare.equal: t]
-
-  let is_false = function False -> true | _ -> false
-
-  let is_true = function True -> true | _ -> false
-end
-
 open Ints
 module SymbolPath = Symb.SymbolPath
 module SymbolTable = Symb.SymbolTable
@@ -618,10 +602,12 @@ module ItvPure = struct
     (l', u')
 
 
-  let lnot : t -> Boolean.t =
+  let to_bool : t -> Boolean.t =
-   fun x -> if is_true x then Boolean.False else if is_false x then Boolean.True else Boolean.Top
+   fun x -> if is_false x then Boolean.False else if is_true x then Boolean.True else Boolean.Top
 
 
+  let lnot : t -> Boolean.t = fun x -> to_bool x |> Boolean.not_
+
   let plus : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.plus_l l1 l2, Bound.plus_u u1 u2)
 
   let minus : t -> t -> t = fun i1 i2 -> plus i1 (neg i2)
@@ -755,19 +741,9 @@ module ItvPure = struct
     else Boolean.Top
 
 
-  let land_sem : t -> t -> Boolean.t =
+  let land_sem : t -> t -> Boolean.t = fun x y -> Boolean.and_ (to_bool x) (to_bool y)
-   fun x y ->
-    if is_true x && is_true y then Boolean.True
-    else if is_false x || is_false y then Boolean.False
-    else Boolean.Top
-
-
-  let lor_sem : t -> t -> Boolean.t =
-   fun x y ->
-    if is_true x || is_true y then Boolean.True
-    else if is_false x && is_false y then Boolean.False
-    else Boolean.Top
 
+  let lor_sem : t -> t -> Boolean.t = fun x y -> Boolean.or_ (to_bool x) (to_bool y)
 
   let min_sem : t -> t -> t =
    fun (l1, u1) (l2, u2) -> (Bound.underapprox_min l1 l2, Bound.overapprox_min u1 u2)

infer/src/bufferoverrun/itv.mli

@@ -9,22 +9,6 @@ open! IStd
 open! AbstractDomain.Types
 module F = Format
 module Bound = Bounds.Bound
-module Counter = Counter
-
-module Boolean : sig
-  type t
-
-  val top : t
-
-  val true_ : t
-
-  val equal : t -> t -> bool
-
-  val is_false : t -> bool
-
-  val is_true : t -> bool
-end
-
 module SymbolPath = Symb.SymbolPath
 module SymbolTable = Symb.SymbolTable
 module SymbolSet = Symb.SymbolSet