From 462bf68f463e3c1c1073742b082cdbe8bd05402b Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Mon, 15 Aug 2016 16:16:52 -0700 Subject: [PATCH] killing is_bottom Reviewed By: jberdine Differential Revision: D3719406 fbshipit-source-id: fdc97f9 --- infer/src/checkers/abstractDomain.ml | 23 ++-------------------- infer/src/checkers/accessPathDomains.ml | 2 -- infer/src/checkers/copyPropagation.ml | 2 -- infer/src/unit/abstractInterpreterTests.ml | 2 -- 4 files changed, 2 insertions(+), 27 deletions(-) diff --git a/infer/src/checkers/abstractDomain.ml b/infer/src/checkers/abstractDomain.ml index 8eb759388..39c0db90c 100644 --- a/infer/src/checkers/abstractDomain.ml +++ b/infer/src/checkers/abstractDomain.ml @@ -15,7 +15,6 @@ module type S = sig type astate val initial : astate - val is_bottom : astate -> bool val (<=) : lhs:astate -> rhs:astate -> bool (* fst \sqsubseteq snd? *) val join : astate -> astate -> astate val widen : prev:astate -> next:astate -> num_iters:int -> astate @@ -28,9 +27,6 @@ module BottomLifted (Domain : S) = struct | Bottom | NonBottom of Domain.astate - let is_bottom astate = - astate = Bottom - let initial = NonBottom Domain.initial let (<=) ~lhs ~rhs = @@ -69,29 +65,18 @@ end module Pair (Domain1 : S) (Domain2 : S) = struct type astate = Domain1.astate * Domain2.astate - let is_bottom (astate1, astate2) = - Domain1.is_bottom astate1 || Domain2.is_bottom astate2 - let initial = Domain1.initial, Domain2.initial let (<=) ~lhs ~rhs = if lhs == rhs then true else - match is_bottom lhs, is_bottom rhs with - | true, _ -> true - | _, true -> false - | _ -> - Domain1.(<=) ~lhs:(fst lhs) ~rhs:(fst rhs) && Domain2.(<=) ~lhs:(snd lhs) ~rhs:(snd rhs) + Domain1.(<=) ~lhs:(fst lhs) ~rhs:(fst rhs) && Domain2.(<=) ~lhs:(snd lhs) ~rhs:(snd rhs) let join astate1 astate2 = if astate1 == astate2 then astate1 - else - match is_bottom astate1, is_bottom astate2 with - | true, _ -> astate2 - | _, true -> astate1 - | _ -> Domain1.join (fst astate1) (fst astate2), Domain2.join (snd astate1) (snd astate2) + else Domain1.join (fst astate1) (fst astate2), Domain2.join (snd astate1) (snd astate2) let widen ~prev ~next ~num_iters = if prev == next @@ -112,8 +97,6 @@ module FiniteSet (S : PrettyPrintable.PPSet) = struct let initial = empty - let is_bottom _ = false - let (<=) ~lhs ~rhs = if lhs == rhs then true @@ -135,8 +118,6 @@ module Map (M : PrettyPrintable.PPMap) (ValueDomain : S) = struct let initial = M.empty - let is_bottom _ = false - (** true if all keys in [lhs] are in [rhs], and each lhs value <= corresponding rhs value *) let (<=) ~lhs ~rhs = if lhs == rhs diff --git a/infer/src/checkers/accessPathDomains.ml b/infer/src/checkers/accessPathDomains.ml index 3e7ecca3d..a9d9c60e9 100644 --- a/infer/src/checkers/accessPathDomains.ml +++ b/infer/src/checkers/accessPathDomains.ml @@ -22,8 +22,6 @@ module Set = struct let initial = APSet.empty - let is_bottom _ = false - let pp = APSet.pp let normalize aps = diff --git a/infer/src/checkers/copyPropagation.ml b/infer/src/checkers/copyPropagation.ml index 8547f78dd..95bf9564a 100644 --- a/infer/src/checkers/copyPropagation.ml +++ b/infer/src/checkers/copyPropagation.ml @@ -18,8 +18,6 @@ module Domain = struct let initial = Var.Map.empty - let is_bottom _ = false - (* return true if the key-value bindings in [rhs] are a subset of the key-value bindings in [lhs] *) let (<=) ~lhs ~rhs = diff --git a/infer/src/unit/abstractInterpreterTests.ml b/infer/src/unit/abstractInterpreterTests.ml index 73953307c..600e11499 100644 --- a/infer/src/unit/abstractInterpreterTests.ml +++ b/infer/src/unit/abstractInterpreterTests.ml @@ -29,8 +29,6 @@ module PathCountDomain = struct let initial = make_path_count 1 - let is_bottom _ = false - let (<=) ~lhs ~rhs = match lhs, rhs with | PathCount c1, PathCount c2 -> c1 <= c2 | _, Top -> true