From e1c2fb3a2f42de0282ab4f6114fc5cfb3ec29dff Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 19 Apr 2023 08:59:15 -0400 Subject: [PATCH] Revert "Simplify bvult by extracting sum common when sound. (#232)" This reverts commit 5a6864ace5a11c38eaeba763d98a38f2443fe83f. --- what4/doc/arithdomain.cry | 22 ---------- what4/src/What4/Expr/Builder.hs | 8 ---- what4/src/What4/Utils/BVDomain.hs | 6 --- what4/src/What4/Utils/BVDomain/Arith.hs | 55 ------------------------- what4/test/BVDomTests.hs | 3 -- 5 files changed, 94 deletions(-) diff --git a/what4/doc/arithdomain.cry b/what4/doc/arithdomain.cry index bf4cdd27..61a5768b 100644 --- a/what4/doc/arithdomain.cry +++ b/what4/doc/arithdomain.cry @@ -306,20 +306,6 @@ slt a b = (sbounds a).1 <$ (sbounds b).0 sle : {n} (fin n, n >= 1) => Dom n -> Dom n -> Bit sle a b = (sbounds a).1 <=$ (sbounds b).0 -ult_sum_common_equiv : {n} (fin n) => Dom n -> Dom n -> Dom n -> Bit -ult_sum_common_equiv a b c = - if al == ah /\ bl == bh /\ al == bl - then True - else if ~(carry cl c.sz) - then check_same_wrap_interval cl ch - else check_same_wrap_interval cl mask`{n} /\ check_same_wrap_interval 0 ch - where - (cl, ch) = (c.lo, c.lo + c.sz) - (al, ah) = ubounds a - (bl, bh) = ubounds b - check_same_wrap_interval lo hi = - ~(carry ah hi) /\ ~(carry bh hi) \/ carry al lo /\ carry bl lo - // A bitmask indicating which bits cannot be determined // given the interval information in the given domain unknowns : {n} (fin n, n >= 1) => Dom n -> [n] @@ -474,13 +460,6 @@ correct_ule : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Bit correct_ule a b x y = ule a b ==> mem a x ==> mem b y ==> x <= y -correct_ult_sum_common_equiv : - {n} (fin n, n >= 1) => Dom n -> Dom n -> Dom n -> [n] -> [n] -> [n] -> Bit -correct_ult_sum_common_equiv a b c x y z = - ult_sum_common_equiv a b c ==> - mem a x ==> mem b y ==> mem c z ==> - (x + z < y + z <==> x < y) - correct_bnot : {n} (fin n) => Dom n -> [n] -> Bit correct_bnot a x = mem a x <==> mem (bnot a) (~ x) @@ -526,7 +505,6 @@ property o1 = correct_slt`{16} property o2 = correct_sle`{16} property o3 = correct_ult`{16} property o4 = correct_ule`{16} -property o5 = correct_ult_sum_common_equiv`{4} //////////////////////////////////////////////////////////// // Operations preserve singletons diff --git a/what4/src/What4/Expr/Builder.hs b/what4/src/What4/Expr/Builder.hs index 245ae727..c41ca600 100644 --- a/what4/src/What4/Expr/Builder.hs +++ b/what4/src/What4/Expr/Builder.hs @@ -2400,14 +2400,6 @@ instance IsExprBuilder (ExprBuilder t st fs) where | x == y = return $! falsePred sym - | sr <- SR.SemiRingBVRepr SR.BVArithRepr (bvWidth x) - , (z, x', y') <- WSum.extractCommon (asWeightedSum sr x) (asWeightedSum sr y) - , not (WSum.isZero sr z) - , BVD.isUltSumCommonEquiv (WSum.sumAbsValue x') (WSum.sumAbsValue y') (WSum.sumAbsValue z) = do - xr <- semiRingSum sym x' - yr <- semiRingSum sym y' - bvUlt sym xr yr - | otherwise = do ut <- CFG.getOpt (sbUnaryThreshold sym) let ?unaryThreshold = fromInteger ut diff --git a/what4/src/What4/Utils/BVDomain.hs b/what4/src/What4/Utils/BVDomain.hs index b6f726ee..9bc4fb75 100644 --- a/what4/src/What4/Utils/BVDomain.hs +++ b/what4/src/What4/Utils/BVDomain.hs @@ -51,7 +51,6 @@ module What4.Utils.BVDomain , domainsOverlap , ubounds , sbounds - , isUltSumCommonEquiv , A.arithDomainData , B.bitbounds -- * Operations @@ -426,11 +425,6 @@ ubounds a = A.ubounds (asArithDomain a) sbounds :: (1 <= w) => NatRepr w -> BVDomain w -> (Integer, Integer) sbounds w a = A.sbounds w (asArithDomain a) --- | Check if (bvult (bvadd a c) (bvadd b c)) is equivalent to (bvult a b) -isUltSumCommonEquiv :: BVDomain w -> BVDomain w -> BVDomain w -> Bool -isUltSumCommonEquiv a b c = - A.isUltSumCommonEquiv (asArithDomain a) (asArithDomain b) (asArithDomain c) - -------------------------------------------------------------------------------- -- Operations diff --git a/what4/src/What4/Utils/BVDomain/Arith.hs b/what4/src/What4/Utils/BVDomain/Arith.hs index 09a06181..34655eda 100644 --- a/what4/src/What4/Utils/BVDomain/Arith.hs +++ b/what4/src/What4/Utils/BVDomain/Arith.hs @@ -11,7 +11,6 @@ domains. {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} -{-# LANGUAGE LambdaCase #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} @@ -31,7 +30,6 @@ module What4.Utils.BVDomain.Arith , eq , slt , ult - , isUltSumCommonEquiv , domainsOverlap , arithDomainData , bitbounds @@ -96,7 +94,6 @@ module What4.Utils.BVDomain.Arith , correct_eq , correct_ult , correct_slt - , correct_isUltSumCommonEquiv , correct_unknowns , correct_bitbounds ) where @@ -279,46 +276,6 @@ ult a b (a_min, a_max) = ubounds a (b_min, b_max) = ubounds b --- | Check if @(bvult (bvadd a c) (bvadd b c))@ is equivalent to @(bvult a b)@. --- --- This is true if and only if for all natural values @i_a@, @i_b@, @i_c@ in --- @a@, @b@, @c@, either both @i_a + i_c@ and @i_b + i_c@ are less than @2^w@, --- or both are not. We prove this by contradiction. If @i_a = i_b@, then the --- property is trivial. Assume that @i_a < i_b@. Then @i_a + i_c < i_b + i_c@. --- If exactly one of the additions is less than @2^w@, it must be the case that --- @i_a + i_c < 2^w@ and @0 <= i_b + i_c - 2^w < 2^w@. Since @i_b < 2^w@, it --- follows that @i_b + i_c < 2^w + i_c@, that @i_b + i_c - 2^w < i_c@, and that --- @i_b + i_c - 2^w < i_a + i_c@. Thus, for these values of @i_a@, @i_b@, @i_c@, --- @(bvult a b)@ is true, but @(bvult (bvadd a c) (bvadd b c))@ is false, which --- is a contradiction. --- --- We check this property by case analysis on whether @c@ is a single --- non-wrapping interval, or it wraps around and is a union of two non-wrapping --- intervals. For a non-wrapping (sub)interval @c'@ of @c@, there are four --- possible cases: --- 1. @a@ and @b@ contain a single value. --- 2. @(bvadd a c')@ and @(bvadd b c')@ do not wrap around for any values in --- @a@, @b@, @c'@. --- 3. @(bvadd a c')@ and @(bvadd b c')@ wrap around for all values in @a@, @b@, --- @c'@. --- --- This is used to simplify @bvult@. -isUltSumCommonEquiv :: Domain w -> Domain w -> Domain w -> Bool -isUltSumCommonEquiv a b c = if al == ah && bl == bh && al == bl - then True - else if cl + cw == ch - then checkSameWrapInterval cl ch - else checkSameWrapInterval cl mask && checkSameWrapInterval 0 ch - where - (mask, cl, cw) = case c of - BVDInterval mask' cl' cw' -> (mask', cl', cw') - BVDAny mask' -> (mask', 0, mask') - ch = (cl + cw) .&. mask - (al, ah) = ubounds a - (bl, bh) = ubounds b - checkSameWrapInterval lo hi = - ah + hi <= mask && bh + hi <= mask || mask < al + lo && mask < bl + lo - -------------------------------------------------------------------------------- -- Operations @@ -858,18 +815,6 @@ correct_slt n (a,x) (b,y) = Just False -> toSigned n x >= toSigned n y Nothing -> True -correct_isUltSumCommonEquiv :: - (1 <= n) => - NatRepr n -> - (Domain n, Integer) -> - (Domain n, Integer) -> - (Domain n, Integer) -> - Property -correct_isUltSumCommonEquiv n (a, x) (b, y) (c, z) = - member a x ==> member b y ==> member c z ==> - isUltSumCommonEquiv a b c ==> - ((toUnsigned n (x + z) < toUnsigned n (y + z)) == (toUnsigned n x < toUnsigned n y)) - correct_unknowns :: (1 <= n) => Domain n -> Integer -> Integer -> Property correct_unknowns a x y = member a x ==> member a y ==> ((x .|. u) == (y .|. u)) && (u .|. mask == mask) where diff --git a/what4/test/BVDomTests.hs b/what4/test/BVDomTests.hs index f3a25cf3..cecbaae4 100644 --- a/what4/test/BVDomTests.hs +++ b/what4/test/BVDomTests.hs @@ -182,9 +182,6 @@ arithDomainTests = testGroup "Arith Domain" , genTest "correct_slt" $ do SW n <- genWidth A.correct_slt n <$> A.genPair n <*> A.genPair n - , genTest "correct_isUltSumCommonEquiv" $ - do SW n <- genWidth - A.correct_isUltSumCommonEquiv n <$> A.genPair n <*> A.genPair n <*> A.genPair n , genTest "correct_unknowns" $ do SW n <- genWidth a <- A.genDomain n