From 8d990d6470f0ff8746856f6b2a5a5a0296606423 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Sun, 18 Nov 2018 08:25:08 -0800 Subject: [PATCH] [inferbo] Move Boolean to their own module Reviewed By: skcho Differential Revision: D13111801 fbshipit-source-id: 6eca0e1c9 --- infer/src/bufferoverrun/boolean.ml | 41 +++++++++++++++++++ infer/src/bufferoverrun/boolean.mli | 22 ++++++++++ .../src/bufferoverrun/bufferOverrunChecker.ml | 6 +-- .../src/bufferoverrun/bufferOverrunDomain.ml | 6 +-- .../src/bufferoverrun/bufferOverrunModels.ml | 4 +- .../bufferOverrunProofObligations.ml | 21 +++++----- infer/src/bufferoverrun/bufferOverrunUtils.ml | 12 +++--- .../src/bufferoverrun/bufferOverrunUtils.mli | 8 ++-- infer/src/bufferoverrun/itv.ml | 36 +++------------- infer/src/bufferoverrun/itv.mli | 16 -------- 10 files changed, 97 insertions(+), 75 deletions(-) create mode 100644 infer/src/bufferoverrun/boolean.ml create mode 100644 infer/src/bufferoverrun/boolean.mli diff --git a/infer/src/bufferoverrun/boolean.ml b/infer/src/bufferoverrun/boolean.ml new file mode 100644 index 000000000..1806a866f --- /dev/null +++ b/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 diff --git a/infer/src/bufferoverrun/boolean.mli b/infer/src/bufferoverrun/boolean.mli new file mode 100644 index 000000000..7a3351189 --- /dev/null +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 501655bad..a82816e8f 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index dc0478d55..6f8530138 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/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} diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 6721d1333..e0c8685e7 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/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_alloc_num:Itv.Counter.t + -> new_sym_num:Counter.t + -> new_alloc_num:Counter.t -> Dom.Mem.astate -> Dom.Mem.astate diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index c38feb57b..9ffeca001 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/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 - else if Itv.Boolean.is_true lpos then + if not (Boolean.equal lpos rpos) then `NotComparable + 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 - else if Itv.Boolean.is_true lidxpos then + if not (Boolean.equal lidxpos ridxpos) then `NotComparable + 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 - Itv.Boolean.true_ + if Relation.le_sat_opt (Some Relation.SymExp.zero) c.idx_sym_exp c.relation then 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 diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index a75c13099..275cdcd39 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/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_alloc_num:Itv.Counter.t + -> new_sym_num: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 -> diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index 32daea9a9..f502496fc 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/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_alloc_num:Itv.Counter.t + -> new_sym_num: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 diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 53897d1ee..3a137dcc7 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/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 = - fun x -> if is_true x then Boolean.False else if is_false x then Boolean.True else Boolean.Top + let to_bool : t -> Boolean.t = + 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 = - 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 land_sem : t -> t -> Boolean.t = fun x y -> Boolean.and_ (to_bool x) (to_bool y) + 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) diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index b5ed7883b..432820359 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/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