mirror of
https://github.com/GaloisInc/what4.git
synced 2024-10-06 00:22:49 +03:00
Various updates to the what4 integer, natural nubmer and bitvector theories.
This commit mainly does two things: * Add more robust support for the integer theory, including `div`, `mod`, `abs` and `divisible`. * Audit the semantics of the `integerToBV` operations, and fix lingering bugs. In the past, there were two different integer->BV operations, because we used a clamping semantics, and it made sense to have a signed versus unsigned distinction. Now, however, we are using a modulo `2^n` semantics, and there is only one operation. However, some places in the code were still using the clamped semantics. These placses have now been cleaned up, and everywhere should be using the modular arithmetic view. In addition, I've reduced the need to use the expensive BV->Integer and Integer->BV coersions somewhat by noticing when we round trip through those coercions more often and translating the result into statements of modular arithmetic instead. Along the way, I improved the abstract domain definitions for division and modulus.
This commit is contained in:
Rob Dockins
parent
5e31218fe4
commit
fd34b7e1d9
@ -284,22 +284,25 @@ bitblastExpr h ae = do
|
||||
------------------------------------------------------------------------
|
||||
-- Nat operations
|
||||
|
||||
NatDiv{} -> natFail
|
||||
SemiRingMul SemiRingNat _ _ -> natFail
|
||||
SemiRingSum SemiRingNat _ -> natFail
|
||||
SemiRingEq SemiRingNat _ _ -> natFail
|
||||
SemiRingLe SemiRingNat _ _ -> natFail
|
||||
SemiRingIte SemiRingNat _ _ _ -> natFail
|
||||
NatDiv{} -> natFail
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- Integer operations
|
||||
|
||||
IntMod{} -> intFail
|
||||
SemiRingMul SemiRingInt _ _ -> intFail
|
||||
SemiRingSum SemiRingInt _ -> intFail
|
||||
SemiRingEq SemiRingInt _ _ -> intFail
|
||||
SemiRingLe SemiRingInt _ _ -> intFail
|
||||
SemiRingIte SemiRingInt _ _ _ -> intFail
|
||||
IntAbs{} -> intFail
|
||||
IntDiv{} -> intFail
|
||||
IntMod{} -> intFail
|
||||
IntDivisible{} -> intFail
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- Real value operations
|
||||
@ -408,7 +411,6 @@ bitblastExpr h ae = do
|
||||
RealToInteger{} -> intFail
|
||||
|
||||
IntegerToNat{} -> natFail
|
||||
IntegerToSBV{} -> intFail
|
||||
IntegerToBV{} -> intFail
|
||||
|
||||
------------------------------------------------------------------------
|
||||
|
||||
@ -84,6 +84,12 @@ appTheory a0 =
|
||||
IntMod _ SemiRingLiteral{} -> LinearArithTheory
|
||||
IntMod{} -> NonlinearArithTheory
|
||||
|
||||
IntDiv _ SemiRingLiteral{} -> LinearArithTheory
|
||||
IntDiv{} -> NonlinearArithTheory
|
||||
|
||||
IntAbs{} -> LinearArithTheory
|
||||
IntDivisible{} -> LinearArithTheory
|
||||
|
||||
----------------------------
|
||||
-- Real operations
|
||||
|
||||
@ -140,7 +146,6 @@ appTheory a0 =
|
||||
RealToInteger{} -> LinearArithTheory
|
||||
|
||||
IntegerToNat{} -> LinearArithTheory
|
||||
IntegerToSBV{} -> BitvectorTheory
|
||||
IntegerToBV{} -> BitvectorTheory
|
||||
|
||||
---------------------
|
||||
|
||||
@ -377,11 +377,12 @@ data App (e :: BaseType -> *) (tp :: BaseType) where
|
||||
-- NatDiv x y is equivalent to intToNat (floor (RealDiv (natToReal x) (natToReal y)))
|
||||
NatDiv :: !(e BaseNatType) -> !(e BaseNatType) -> App e BaseNatType
|
||||
|
||||
RealDiv :: !(e BaseRealType) -> !(e BaseRealType) -> App e BaseRealType
|
||||
IntDiv :: !(e BaseIntegerType) -> !(e BaseIntegerType) -> App e BaseIntegerType
|
||||
IntMod :: !(e BaseIntegerType) -> !(e BaseIntegerType) -> App e BaseNatType
|
||||
IntAbs :: !(e BaseIntegerType) -> App e BaseNatType
|
||||
IntDivisible :: !(e BaseIntegerType) -> Natural -> App e BaseBoolType
|
||||
|
||||
-- @IntMod x y@ denotes the value of @x - y * floor(x ./ y)@.
|
||||
-- Is not defined when @y@ is zero.
|
||||
IntMod :: !(e BaseIntegerType) -> !(e BaseNatType) -> App e BaseNatType
|
||||
RealDiv :: !(e BaseRealType) -> !(e BaseRealType) -> App e BaseRealType
|
||||
|
||||
-- Returns @sqrt(x)@, result is not defined if @x@ is negative.
|
||||
RealSqrt :: !(e BaseRealType) -> App e BaseRealType
|
||||
@ -615,9 +616,7 @@ data App (e :: BaseType -> *) (tp :: BaseType) where
|
||||
BVToInteger :: (1 <= w) => !(e (BaseBVType w)) -> App e BaseIntegerType
|
||||
SBVToInteger :: (1 <= w) => !(e (BaseBVType w)) -> App e BaseIntegerType
|
||||
|
||||
-- Converts integer to signed bitvector (numbers are rounded to nearest representable result).
|
||||
IntegerToSBV :: (1 <= w) => !(e BaseIntegerType) -> NatRepr w -> App e (BaseBVType w)
|
||||
-- Converts integer to unsigned bitvector (numbers are rounded to nearest represented result).
|
||||
-- Converts integer to a bitvector. The number is interpreted modulo 2^n.
|
||||
IntegerToBV :: (1 <= w) => !(e BaseIntegerType) -> NatRepr w -> App e (BaseBVType w)
|
||||
|
||||
RoundReal :: !(e BaseRealType) -> App e BaseIntegerType
|
||||
@ -933,7 +932,11 @@ appType a =
|
||||
ArrayEq{} -> knownRepr
|
||||
|
||||
NatDiv{} -> knownRepr
|
||||
|
||||
IntDiv{} -> knownRepr
|
||||
IntMod{} -> knownRepr
|
||||
IntAbs{} -> knownRepr
|
||||
IntDivisible{} -> knownRepr
|
||||
|
||||
SemiRingEq{} -> knownRepr
|
||||
SemiRingLe{} -> knownRepr
|
||||
@ -994,7 +997,6 @@ appType a =
|
||||
SBVToInteger{} -> knownRepr
|
||||
|
||||
IntegerToNat{} -> knownRepr
|
||||
IntegerToSBV _ w -> BaseBVRepr w
|
||||
IntegerToBV _ w -> BaseBVRepr w
|
||||
|
||||
RealToInteger{} -> knownRepr
|
||||
@ -1220,7 +1222,10 @@ ppApp' a0 = do
|
||||
|
||||
NatDiv x y -> ppSExpr "natDiv" [x, y]
|
||||
|
||||
IntAbs x -> prettyApp "intAbs" [exprPrettyArg x]
|
||||
IntDiv x y -> prettyApp "intDiv" [exprPrettyArg x, exprPrettyArg y]
|
||||
IntMod x y -> prettyApp "intMod" [exprPrettyArg x, exprPrettyArg y]
|
||||
IntDivisible x k -> prettyApp "intDivisible" [exprPrettyArg x, showPrettyArg k]
|
||||
|
||||
SemiRingEq sr x y ->
|
||||
case sr of
|
||||
@ -1343,7 +1348,6 @@ ppApp' a0 = do
|
||||
CeilReal x -> ppSExpr "ceil" [x]
|
||||
|
||||
IntegerToNat x -> ppSExpr "integerToNat" [x]
|
||||
IntegerToSBV x w -> prettyApp "integerToSBV" [exprPrettyArg x, showPrettyArg w]
|
||||
IntegerToBV x w -> prettyApp "integerToBV" [exprPrettyArg x, showPrettyArg w]
|
||||
|
||||
RealToInteger x -> ppSExpr "realToInteger" [x]
|
||||
@ -2037,8 +2041,12 @@ abstractEval bvParams f a0 = do
|
||||
------------------------------------------------------------------------
|
||||
-- Arithmetic operations
|
||||
|
||||
NatDiv x _ -> (f x)
|
||||
IntMod _ y -> natRange 0 (pred <$> natRangeHigh (f y))
|
||||
NatDiv x y -> natRangeDiv (f x) (f y)
|
||||
|
||||
IntAbs x -> intAbsRange (f x)
|
||||
IntDiv x y -> intDivRange (f x) (f y)
|
||||
IntMod x y -> intModRange (f x) (f y)
|
||||
IntDivisible x n -> natCheckEq (NatSingleRange 0) (intModRange (f x) (SingleRange (toInteger n)))
|
||||
|
||||
SemiRingMul SemiRingInt x y -> mulRange (f x) (f y)
|
||||
SemiRingSum SemiRingInt s -> WSum.eval addRange smul SingleRange s
|
||||
@ -2047,7 +2055,7 @@ abstractEval bvParams f a0 = do
|
||||
|
||||
SemiRingMul SemiRingNat x y -> natRangeMul (f x) (f y)
|
||||
SemiRingSum SemiRingNat s -> WSum.eval natRangeAdd smul natSingleRange s
|
||||
where smul sm e = natRangeScalarMul (toInteger sm) (f e)
|
||||
where smul sm e = natRangeScalarMul sm (f e)
|
||||
SemiRingIte SemiRingNat _ x y -> natRangeJoin (f x) (f y)
|
||||
|
||||
SemiRingMul SemiRingReal x y -> ravMul (f x) (f y)
|
||||
@ -2107,7 +2115,7 @@ abstractEval bvParams f a0 = do
|
||||
|
||||
NatToInteger x -> natRangeToRange (f x)
|
||||
IntegerToReal x -> RAV (mapRange toRational (f x)) (Just True)
|
||||
BVToNat x -> natRange lx (Inclusive ux)
|
||||
BVToNat x -> natRange (fromInteger lx) (Inclusive (fromInteger ux))
|
||||
where Just (lx, ux) = BVD.ubounds (bvWidth x) (f x)
|
||||
BVToInteger x -> valueRange (Inclusive lx) (Inclusive ux)
|
||||
where Just (lx, ux) = BVD.ubounds (bvWidth x) (f x)
|
||||
@ -2118,17 +2126,9 @@ abstractEval bvParams f a0 = do
|
||||
CeilReal x -> mapRange ceiling (ravRange (f x))
|
||||
IntegerToNat x ->
|
||||
case f x of
|
||||
SingleRange c -> NatSingleRange (max 0 c)
|
||||
MultiRange Unbounded u -> natRange 0 u
|
||||
MultiRange (Inclusive l) u -> natRange (max 0 l) u
|
||||
IntegerToSBV x w -> BVD.range w l u
|
||||
where rng = f x
|
||||
l = case rangeLowBound rng of
|
||||
Unbounded -> minSigned w
|
||||
Inclusive v -> max (minSigned w) v
|
||||
u = case rangeHiBound rng of
|
||||
Unbounded -> maxSigned w
|
||||
Inclusive v -> min (maxSigned w) v
|
||||
SingleRange c -> NatSingleRange (fromInteger (max 0 c))
|
||||
MultiRange Unbounded u -> natRange 0 (fromInteger . max 0 <$> u)
|
||||
MultiRange (Inclusive l) u -> natRange (fromInteger (max 0 l)) (fromInteger . max 0 <$> u)
|
||||
IntegerToBV x w -> BVD.range w l u
|
||||
where rng = f x
|
||||
l = case rangeLowBound rng of
|
||||
@ -2619,9 +2619,14 @@ reduceApp sym a0 = do
|
||||
SemiRingMul SemiRingReal x y -> realMul sym x y
|
||||
SemiRingIte SemiRingReal c x y -> realIte sym c x y
|
||||
|
||||
NatDiv x y -> natDiv sym x y
|
||||
NatDiv x y -> natDiv sym x y
|
||||
|
||||
IntDiv x y -> intDiv sym x y
|
||||
IntMod x y -> intMod sym x y
|
||||
IntAbs x -> intAbs sym x
|
||||
IntDivisible x k -> intDivisible sym x k
|
||||
|
||||
RealDiv x y -> realDiv sym x y
|
||||
IntMod x y -> intMod sym x y
|
||||
RealSqrt x -> realSqrt sym x
|
||||
|
||||
Pi -> realPi sym
|
||||
@ -2676,7 +2681,6 @@ reduceApp sym a0 = do
|
||||
BVToNat x -> bvToNat sym x
|
||||
BVToInteger x -> bvToInteger sym x
|
||||
SBVToInteger x -> sbvToInteger sym x
|
||||
IntegerToSBV x w -> integerToSBV sym x w
|
||||
IntegerToBV x w -> integerToBV sym x w
|
||||
|
||||
RoundReal x -> realRound sym x
|
||||
@ -3490,8 +3494,6 @@ instance IsExprBuilder (ExprBuilder t st) where
|
||||
| Just b <- rangeCheckEq (exprAbsValue x) (exprAbsValue y)
|
||||
= return $ backendPred sym b
|
||||
|
||||
-- FIXME... implement reductions for unsigned bitvectors as well
|
||||
|
||||
-- Reduce to bitvector equality, when possible
|
||||
| Just (SBVToInteger xbv) <- asApp x
|
||||
, Just (SBVToInteger ybv) <- asApp y
|
||||
@ -3510,6 +3512,24 @@ instance IsExprBuilder (ExprBuilder t st) where
|
||||
y' <- bvSext sym wx ybv
|
||||
bvEq sym xbv y'
|
||||
|
||||
-- Reduce to bitvector equality, when possible
|
||||
| Just (BVToInteger xbv) <- asApp x
|
||||
, Just (BVToInteger ybv) <- asApp y
|
||||
= let wx = bvWidth xbv
|
||||
wy = bvWidth ybv
|
||||
-- Zero extend to largest bitvector and compare.
|
||||
in case compareNat wx wy of
|
||||
NatLT _ -> do
|
||||
Just LeqProof <- return (testLeq (incNat wx) wy)
|
||||
x' <- bvZext sym wy xbv
|
||||
bvEq sym x' ybv
|
||||
NatEQ ->
|
||||
bvEq sym xbv ybv
|
||||
NatGT _ -> do
|
||||
Just LeqProof <- return (testLeq (incNat wy) wx)
|
||||
y' <- bvZext sym wx ybv
|
||||
bvEq sym xbv y'
|
||||
|
||||
| Just (SBVToInteger xbv) <- asApp x
|
||||
, SemiRingLiteral _ yi _ <- y
|
||||
= let w = bvWidth xbv in
|
||||
@ -3524,6 +3544,20 @@ instance IsExprBuilder (ExprBuilder t st) where
|
||||
then return (falsePred sym)
|
||||
else bvEq sym ybv =<< bvLit sym w xi
|
||||
|
||||
| Just (BVToInteger xbv) <- asApp x
|
||||
, SemiRingLiteral _ yi _ <- y
|
||||
= let w = bvWidth xbv in
|
||||
if yi < minUnsigned w || yi > maxUnsigned w
|
||||
then return (falsePred sym)
|
||||
else bvEq sym xbv =<< bvLit sym w yi
|
||||
|
||||
| SemiRingLiteral _ xi _ <- x
|
||||
, Just (BVToInteger ybv) <- asApp x
|
||||
= let w = bvWidth ybv in
|
||||
if xi < minUnsigned w || xi > maxUnsigned w
|
||||
then return (falsePred sym)
|
||||
else bvEq sym ybv =<< bvLit sym w xi
|
||||
|
||||
| otherwise = semiRingEq sym SemiRingInt x y
|
||||
|
||||
intLe sym x y
|
||||
@ -3531,8 +3565,6 @@ instance IsExprBuilder (ExprBuilder t st) where
|
||||
| Just b <- rangeCheckLe (exprAbsValue x) (exprAbsValue y)
|
||||
= return $ backendPred sym b
|
||||
|
||||
-- FIXME... implement reductions for unsigned bitvectors also...
|
||||
|
||||
-- Check with two bitvectors.
|
||||
| Just (SBVToInteger xbv) <- asApp x
|
||||
, Just (SBVToInteger ybv) <- asApp y
|
||||
@ -3550,6 +3582,23 @@ instance IsExprBuilder (ExprBuilder t st) where
|
||||
y' <- bvSext sym wx ybv
|
||||
bvSle sym xbv y'
|
||||
|
||||
-- Check with two bitvectors.
|
||||
| Just (BVToInteger xbv) <- asApp x
|
||||
, Just (BVToInteger ybv) <- asApp y
|
||||
= do let wx = bvWidth xbv
|
||||
let wy = bvWidth ybv
|
||||
-- Zero extend to largest bitvector and compare.
|
||||
case compareNat wx wy of
|
||||
NatLT _ -> do
|
||||
Just LeqProof <- return (testLeq (incNat wx) wy)
|
||||
x' <- bvZext sym wy xbv
|
||||
bvUle sym x' ybv
|
||||
NatEQ -> bvUle sym xbv ybv
|
||||
NatGT _ -> do
|
||||
Just LeqProof <- return (testLeq (incNat wy) wx)
|
||||
y' <- bvZext sym wx ybv
|
||||
bvUle sym xbv y'
|
||||
|
||||
| Just (SBVToInteger xbv) <- asApp x
|
||||
, SemiRingLiteral _ yi _ <- y
|
||||
= let w = bvWidth xbv in
|
||||
@ -3564,6 +3613,20 @@ instance IsExprBuilder (ExprBuilder t st) where
|
||||
| xi > maxSigned w -> return (falsePred sym)
|
||||
| otherwise -> join (bvSle sym <$> bvLit sym w xi <*> pure ybv)
|
||||
|
||||
| Just (BVToInteger xbv) <- asApp x
|
||||
, SemiRingLiteral _ yi _ <- y
|
||||
= let w = bvWidth xbv in
|
||||
if | yi < minUnsigned w -> return (falsePred sym)
|
||||
| yi > maxUnsigned w -> return (truePred sym)
|
||||
| otherwise -> join (bvUle sym <$> pure xbv <*> bvLit sym w yi)
|
||||
|
||||
| SemiRingLiteral _ xi _ <- x
|
||||
, Just (BVToInteger ybv) <- asApp x
|
||||
= let w = bvWidth ybv in
|
||||
if | xi < minUnsigned w -> return (truePred sym)
|
||||
| xi > maxUnsigned w -> return (falsePred sym)
|
||||
| otherwise -> join (bvUle sym <$> bvLit sym w xi <*> pure ybv)
|
||||
|
||||
{- FIXME? how important are these reductions?
|
||||
|
||||
-- Compare to BV lower bound.
|
||||
@ -3588,19 +3651,64 @@ instance IsExprBuilder (ExprBuilder t st) where
|
||||
| otherwise
|
||||
= semiRingLe sym SemiRingInt x y
|
||||
|
||||
intAbs sym x
|
||||
| Just i <- asInteger x = natLit sym (fromInteger (abs i))
|
||||
| Just True <- rangeCheckLe (SingleRange 0) (exprAbsValue x) = integerToNat sym x
|
||||
| Just True <- rangeCheckLe (exprAbsValue x) (SingleRange 0) = integerToNat sym =<< intNeg sym x
|
||||
| otherwise = sbMakeExpr sym (IntAbs x)
|
||||
|
||||
intDiv sym x y
|
||||
-- Div by 0.
|
||||
| Just 0 <- asInteger y = intLit sym 0
|
||||
-- Div by 1.
|
||||
| Just 1 <- asInteger y = return x
|
||||
-- Div 0 by anything is zero.
|
||||
| Just 0 <- asInteger x = intLit sym 0
|
||||
-- As integers.
|
||||
| Just xi <- asInteger x, Just yi <- asInteger y =
|
||||
if yi >= 0 then
|
||||
intLit sym (xi `div` yi)
|
||||
else
|
||||
intLit sym (negate (xi `div` negate yi))
|
||||
-- Return int div
|
||||
| otherwise =
|
||||
sbMakeExpr sym (IntDiv x y)
|
||||
|
||||
intMod sym x y
|
||||
-- Not defined when division by 0.
|
||||
| Just 0 <- asNat y = return y
|
||||
-- Mod by 0.
|
||||
| Just 0 <- asInteger y = natLit sym 0
|
||||
-- Mod by 1.
|
||||
| Just 1 <- asNat y = natLit sym 0
|
||||
| Just 1 <- asInteger y = natLit sym 0
|
||||
-- Mod 0 by anything is zero.
|
||||
| Just 0 <- asInteger x = natLit sym 0
|
||||
-- As integers.
|
||||
| Just xi <- asInteger x, Just yi <- asNat y = do
|
||||
natLit sym (fromInteger (xi `mod` toInteger yi))
|
||||
| Just xi <- asInteger x, Just yi <- asInteger y =
|
||||
natLit sym (fromInteger (xi `mod` abs yi))
|
||||
| Just (SemiRingSum _sr xsum) <- asApp x, Just yi <- asInteger y =
|
||||
case WSum.reduceIntSumMod xsum (abs yi) of
|
||||
xsum' | Just xi <- WSum.asConstant xsum' ->
|
||||
natLit sym (fromInteger xi)
|
||||
| otherwise ->
|
||||
do x' <- intSum sym xsum'
|
||||
sbMakeExpr sym (IntMod x' y)
|
||||
-- Return int mod.
|
||||
| otherwise = do
|
||||
sbMakeExpr sym (IntMod x y)
|
||||
| otherwise =
|
||||
sbMakeExpr sym (IntMod x y)
|
||||
|
||||
intDivisible sym x k
|
||||
-- All numbers divisible by 0, per interface.
|
||||
| k == 0 = return (truePred sym)
|
||||
| k == 1 = return (truePred sym)
|
||||
| Just xi <- asInteger x = return $ backendPred sym (xi `mod` (toInteger k) == 0)
|
||||
| Just (SemiRingSum _sr xsum) <- asApp x =
|
||||
case WSum.reduceIntSumMod xsum (toInteger k) of
|
||||
xsum' | Just xi <- WSum.asConstant xsum' ->
|
||||
return $ backendPred sym (xi == 0)
|
||||
| otherwise ->
|
||||
do x' <- intSum sym xsum'
|
||||
sbMakeExpr sym (IntDivisible x' k)
|
||||
| otherwise =
|
||||
sbMakeExpr sym (IntDivisible x k)
|
||||
|
||||
---------------------------------------------------------------------
|
||||
-- Bitvector operations
|
||||
@ -4336,29 +4444,48 @@ instance IsExprBuilder (ExprBuilder t st) where
|
||||
sbMakeExpr sym (RealToInteger x)
|
||||
|
||||
bvToNat sym x
|
||||
| Just i <- asUnsignedBV x = natLit sym (fromInteger i)
|
||||
| Just i <- asUnsignedBV x =
|
||||
natLit sym (fromInteger i)
|
||||
| otherwise = sbMakeExpr sym (BVToNat x)
|
||||
|
||||
bvToInteger sym x
|
||||
| Just i <- asUnsignedBV x = intLit sym i
|
||||
| otherwise = sbMakeExpr sym (BVToInteger x)
|
||||
| Just i <- asUnsignedBV x =
|
||||
intLit sym i
|
||||
-- bvToInteger (integerToBv x w) == mod x (2^w)
|
||||
| Just (IntegerToBV xi w) <- asApp x =
|
||||
natToInteger sym =<< intMod sym xi =<< intLit sym (2^natValue w)
|
||||
| otherwise =
|
||||
sbMakeExpr sym (BVToInteger x)
|
||||
|
||||
sbvToInteger sym x
|
||||
| Just i <- asSignedBV x = intLit sym i
|
||||
| otherwise = sbMakeExpr sym (SBVToInteger x)
|
||||
|
||||
integerToSBV sym (SemiRingLiteral SemiRingInt i _) w =
|
||||
bvLit sym w i
|
||||
integerToSBV sym xr w
|
||||
| Just (SBVToInteger r) <- asApp xr = intSetWidth sym r w
|
||||
integerToSBV sym xr w =
|
||||
sbMakeExpr sym (IntegerToSBV xr w)
|
||||
| Just i <- asSignedBV x =
|
||||
intLit sym i
|
||||
-- sbvToInteger (integerToBv x w) == mod (x + 2^(w-1)) (2^w) - 2^(w-1)
|
||||
| Just (IntegerToBV xi w) <- asApp x =
|
||||
do halfmod <- intLit sym (2 ^ (natValue w - 1))
|
||||
modulus <- intLit sym (2 ^ natValue w)
|
||||
x' <- intAdd sym xi halfmod
|
||||
z <- natToInteger sym =<< intMod sym x' modulus
|
||||
intSub sym z halfmod
|
||||
| otherwise =
|
||||
sbMakeExpr sym (SBVToInteger x)
|
||||
|
||||
integerToBV sym xr w
|
||||
| SemiRingLiteral SemiRingInt i _ <- xr =
|
||||
bvLit sym w $ unsignedClamp w $ toInteger i
|
||||
bvLit sym w i
|
||||
|
||||
| Just (BVToInteger r) <- asApp xr =
|
||||
uintSetWidth sym r w
|
||||
case compareNat (bvWidth r) w of
|
||||
NatLT _ -> bvZext sym w r
|
||||
NatEQ -> return r
|
||||
NatGT _ -> bvTrunc sym w r
|
||||
|
||||
| Just (SBVToInteger r) <- asApp xr =
|
||||
case compareNat (bvWidth r) w of
|
||||
NatLT _ -> bvSext sym w r
|
||||
NatEQ -> return r
|
||||
NatGT _ -> bvTrunc sym w r
|
||||
|
||||
| otherwise =
|
||||
sbMakeExpr sym (IntegerToBV xr w)
|
||||
|
||||
|
||||
@ -223,6 +223,22 @@ evalGroundApp f0 a0 = do
|
||||
where g _ 0 = 0
|
||||
g u v = u `div` v
|
||||
|
||||
IntDiv x y -> g <$> f x <*> f y
|
||||
where
|
||||
g u v | v == 0 = 0
|
||||
| v > 0 = u `div` v
|
||||
| otherwise = negate (u `div` negate v)
|
||||
|
||||
IntMod x y -> intModu <$> f x <*> f y
|
||||
where intModu _ 0 = 0
|
||||
intModu i v = fromInteger (i `mod` abs v)
|
||||
|
||||
IntAbs x -> fromInteger . abs <$> f x
|
||||
|
||||
IntDivisible x k -> g <$> f x
|
||||
where
|
||||
g u = mod u (toInteger k) == 0
|
||||
|
||||
SemiRingEq SemiRingReal x y -> (==) <$> f x <*> f y
|
||||
SemiRingEq SemiRingInt x y -> (==) <$> f x <*> f y
|
||||
SemiRingEq SemiRingNat x y -> (==) <$> f x <*> f y
|
||||
@ -235,9 +251,6 @@ evalGroundApp f0 a0 = do
|
||||
where smul sm e = (sm *) <$> f e
|
||||
SemiRingMul SemiRingNat x y -> (*) <$> f x <*> f y
|
||||
|
||||
IntMod x y -> intModu <$> f x <*> f y
|
||||
where intModu _ 0 = 0
|
||||
intModu i v = fromInteger (i `mod` toInteger v)
|
||||
SemiRingSum SemiRingInt s -> WSum.eval (\x y -> (+) <$> x <*> y) smul pure s
|
||||
where smul sm e = (sm *) <$> f e
|
||||
SemiRingMul SemiRingInt x y -> (*) <$> f x <*> f y
|
||||
@ -394,8 +407,7 @@ evalGroundApp f0 a0 = do
|
||||
RealToInteger x -> floor <$> f x
|
||||
|
||||
IntegerToNat x -> fromInteger . max 0 <$> f x
|
||||
IntegerToSBV x w -> toUnsigned w . signedClamp w <$> f x
|
||||
IntegerToBV x w -> unsignedClamp w <$> f x
|
||||
IntegerToBV x w -> toUnsigned w <$> f x
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- Complex operations.
|
||||
|
||||
@ -42,6 +42,7 @@ module What4.Expr.WeightedSum
|
||||
, scale
|
||||
, eval
|
||||
, extractCommon
|
||||
, reduceIntSumMod
|
||||
) where
|
||||
|
||||
import Control.Lens
|
||||
@ -277,6 +278,22 @@ eval addFn smul rat w
|
||||
where merge (WrapF e) s r = addFn (smul s e) r
|
||||
{-# INLINABLE eval #-}
|
||||
|
||||
-- | Reduce a weighted sum of integers modulo a concrete integer.
|
||||
-- This reduces each of the coefficents modulo the given integer,
|
||||
-- removing any that are congruent to 0; the offset value is
|
||||
-- also reduced.
|
||||
reduceIntSumMod :: (OrdF f, HashableF f) =>
|
||||
WeightedSum f BaseIntegerType {- ^ The sum to reduce -} ->
|
||||
Integer {- ^ The modulus, must not be 0 -} ->
|
||||
WeightedSum f BaseIntegerType
|
||||
reduceIntSumMod ws k = unfilteredSum m (ws^.sumOffset `mod` k)
|
||||
where
|
||||
m = runIdentity (Map.traverseMaybeWithKey f (ws^.sumMap))
|
||||
f _key x
|
||||
| x' == 0 = return (Nothing)
|
||||
| otherwise = return (Just x')
|
||||
where x' = x `mod` k
|
||||
|
||||
|
||||
{-# INLINABLE extractCommon #-}
|
||||
|
||||
|
||||
@ -482,7 +482,8 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym) ) => IsExprBuilder sym whe
|
||||
natMod :: sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
|
||||
natMod sym x y = do
|
||||
xi <- natToInteger sym x
|
||||
intMod sym xi y
|
||||
yi <- natToInteger sym y
|
||||
intMod sym xi yi
|
||||
|
||||
-- | If-then-else applied to natural numbers.
|
||||
natIte :: sym -> Pred sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
|
||||
@ -529,9 +530,47 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym) ) => IsExprBuilder sym whe
|
||||
intLt :: sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
|
||||
intLt sym x y = notPred sym =<< intLe sym y x
|
||||
|
||||
-- | @intMod x y@ returns the value of @x - y * floor(x / y)@ when
|
||||
-- @y@ is not zero, and undefined when @y@ is zero.
|
||||
intMod :: sym -> SymInteger sym -> SymNat sym -> IO (SymNat sym)
|
||||
-- | Compute the absolute value of an integer. The result is the unique
|
||||
-- natural number with the same magnitude as the input integer.
|
||||
intAbs :: sym -> SymInteger sym -> IO (SymNat sym)
|
||||
|
||||
-- | @intDiv x y@ computes the integer division of @x@ by @y@. This division is
|
||||
-- interpreted the same way as the SMT-Lib integer theory, which states that
|
||||
-- @div@ and @mod@ are the unique Eucledian division operations satisfying the
|
||||
-- following for all @y /= 0@:
|
||||
--
|
||||
-- * @x * (div x y) + (mod x y) == x@
|
||||
-- * @ 0 <= mod x y < abs y@
|
||||
--
|
||||
-- The value of @intDiv x y@ is undefined when @y = 0@.
|
||||
--
|
||||
-- Integer division requires nonlinear support whenever the divisor is
|
||||
-- not a constant.
|
||||
--
|
||||
-- Note: @div x y@ is @floor (x/y)@ when @y@ is positive
|
||||
-- (regardless of sign of @x@) and @ceiling (x/y)@ when @y@ is
|
||||
-- negative. This is neither of the more common "round toward
|
||||
-- zero" nor "round toward -inf" definitions.
|
||||
--
|
||||
-- Some useful theorems that are true of this division/modulus pair:
|
||||
-- * @mod x y == mod x (- y) == mod x (abs y)@
|
||||
-- * @div x (-y) == -(div x y)@
|
||||
intDiv :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
|
||||
|
||||
-- | @intMod x y@ computes the integer modulus of @x@ by @y@. See 'intDiv' for
|
||||
-- more details.
|
||||
--
|
||||
-- The value of @intMod x y@ is undefined when @y = 0@.
|
||||
--
|
||||
-- Integer modulus requires nonlinear support whenever the divisor is
|
||||
-- not a constant.
|
||||
intMod :: sym -> SymInteger sym -> SymInteger sym -> IO (SymNat sym)
|
||||
|
||||
-- | @intDivisible x k@ is true whenever @x@ is an integer divisible
|
||||
-- by the known positive number @k@. We adopt a definition such
|
||||
-- that every number is divisible by zero, so
|
||||
-- @intDivisible x 0 = true@.
|
||||
intDivisible :: sym -> SymInteger sym -> Natural -> IO (Pred sym)
|
||||
|
||||
----------------------------------------------------------------------
|
||||
-- Bitvector operations
|
||||
@ -1100,14 +1139,16 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym) ) => IsExprBuilder sym whe
|
||||
-- | Round up to the nearest integer that is at least this value.
|
||||
realCeil :: sym -> SymReal sym -> IO (SymInteger sym)
|
||||
|
||||
-- | Convert an integer to a signed bitvector.
|
||||
-- | Convert an integer to a bitvector. The result is the unique bitvector
|
||||
-- whose value (signed or unsigned) is congruent to the input integer, modulo @2^w@.
|
||||
--
|
||||
-- Result is undefined if integer is outside of range.
|
||||
integerToSBV :: (1 <= w) => sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
|
||||
|
||||
-- | Convert an integer to an unsigned bitvector.
|
||||
--
|
||||
-- Result is undefined if integer is outside of range.
|
||||
-- This operation has the following properties:
|
||||
-- * @bvToInteger (integerToBv x w) == mod x (2^w)@
|
||||
-- * @bvToInteger (integerToBV x w) == x@ when @0 <= x < 2^w@.
|
||||
-- * @sbvToInteger (integerToBV x w) == mod (x + 2^(w-1)) (2^w) - 2^(w-1)@
|
||||
-- * @sbvToInteger (integerToBV x w) == x@ when @-2^(w-1) <= x < 2^(w-1)@
|
||||
-- * @integerToBV (bvToInteger y) w == y@ when @y@ is a @SymBV sym w@
|
||||
-- * @integerToBV (sbvToInteger y) w == y@ when @y@ is a @SymBV sym w@
|
||||
integerToBV :: (1 <= w) => sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
|
||||
|
||||
----------------------------------------------------------------------
|
||||
@ -1167,7 +1208,7 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym) ) => IsExprBuilder sym whe
|
||||
is_gt <- intLt sym max_sym i
|
||||
iteM bvIte sym is_gt (bvLit sym w max_val) $ do
|
||||
-- Do unclamped conversion.
|
||||
integerToSBV sym i w
|
||||
integerToBV sym i w
|
||||
|
||||
-- | Convert an integer to the nearest unsigned bitvector.
|
||||
--
|
||||
|
||||
@ -259,6 +259,12 @@ instance SMTLib2Tweaks a => SupportTermOps (Expr a) where
|
||||
|
||||
integerTerm i = toIntegerTerm i
|
||||
|
||||
intDiv x y = term_app "div" [x,y]
|
||||
intMod x y = term_app "mod" [x,y]
|
||||
intAbs x = term_app "abs" [x]
|
||||
intDivisible _ 0 = boolExpr True
|
||||
intDivisible x k = intMod x (integerTerm (toInteger k)) .== 0
|
||||
|
||||
rationalTerm r | d == 1 = toRealTerm n
|
||||
| otherwise = term_app "/" [toRealTerm n, toRealTerm d]
|
||||
where n = numerator r
|
||||
|
||||
@ -100,6 +100,7 @@ import qualified Data.Text.Lazy.Builder.Int as Builder (decimal)
|
||||
import qualified Data.Text.Lazy as Lazy
|
||||
import qualified Data.Text.Lazy.IO as Lazy
|
||||
import Data.Word
|
||||
import Numeric.Natural
|
||||
import System.IO
|
||||
import Text.PrettyPrint.ANSI.Leijen hiding ((<$>), (<>))
|
||||
import Data.ByteString(ByteString)
|
||||
@ -286,7 +287,7 @@ class Num v => SupportTermOps v where
|
||||
-- | Convert an integer expression to a real.
|
||||
termIntegerToReal :: v -> v
|
||||
|
||||
-- | Convert an integer expression to a real.
|
||||
-- | Convert a real expression to an integer.
|
||||
termRealToInteger :: v -> v
|
||||
|
||||
-- | Convert an integer to a term.
|
||||
@ -310,6 +311,12 @@ class Num v => SupportTermOps v where
|
||||
(.>=) :: v -> v -> v
|
||||
x .>= y = y .<= x
|
||||
|
||||
-- | Integer theory terms
|
||||
intAbs :: v -> v
|
||||
intDiv :: v -> v -> v
|
||||
intMod :: v -> v -> v
|
||||
intDivisible :: v -> Natural -> v
|
||||
|
||||
-- | Create expression from bitvector.
|
||||
bvTerm :: NatRepr w -> Integer -> v
|
||||
bvNeg :: v -> v
|
||||
@ -1108,8 +1115,8 @@ bindVar v x = do
|
||||
------------------------------------------------------------------------
|
||||
-- Evaluate applications.
|
||||
|
||||
-- 'bvNatTerm h w x' builds an integer term term that has the same
|
||||
-- value as the unsigned integer value of the bitvector 'x'.
|
||||
-- @bvIntTerm w x@ builds an integer term term that has the same
|
||||
-- value as the unsigned integer value of the bitvector @x@.
|
||||
-- This is done by explicitly decomposing the positional
|
||||
-- notation of the bitvector into a sum of powers of 2.
|
||||
bvIntTerm :: forall v w
|
||||
@ -1563,6 +1570,34 @@ appSMTExpr ae = do
|
||||
fail $ "Array types are not equal."
|
||||
freshBoundTerm BoolTypeMap $ asBase x .== asBase y
|
||||
|
||||
IntDiv xe ye -> do
|
||||
case ye of
|
||||
SemiRingLiteral SemiRingInt _ _ -> return ()
|
||||
_ -> checkNonlinearSupport i
|
||||
|
||||
x <- mkBaseExpr xe
|
||||
y <- mkBaseExpr ye
|
||||
|
||||
freshBoundTerm IntegerTypeMap (intDiv x y)
|
||||
|
||||
IntMod xe ye -> do
|
||||
case ye of
|
||||
SemiRingLiteral SemiRingInt _ _ -> return ()
|
||||
_ -> checkNonlinearSupport i
|
||||
|
||||
x <- mkBaseExpr xe
|
||||
y <- mkBaseExpr ye
|
||||
|
||||
freshBoundTerm NatTypeMap (intMod x y)
|
||||
|
||||
IntAbs xe -> do
|
||||
x <- mkBaseExpr xe
|
||||
freshBoundTerm NatTypeMap (intAbs x)
|
||||
|
||||
IntDivisible xe k -> do
|
||||
x <- mkBaseExpr xe
|
||||
freshBoundTerm BoolTypeMap (intDivisible x k)
|
||||
|
||||
NatDiv xe ye -> do
|
||||
case ye of
|
||||
SemiRingLiteral SemiRingNat _ _ -> return ()
|
||||
@ -1571,17 +1606,7 @@ appSMTExpr ae = do
|
||||
x <- mkBaseExpr xe
|
||||
y <- mkBaseExpr ye
|
||||
|
||||
nm <- freshConstant "nat div" NatTypeMap
|
||||
r <- asBase <$> freshConstant "nat div" NatTypeMap
|
||||
let q = asBase nm
|
||||
-- Assume x can be composed into quotient and remainder.
|
||||
addSideCondition "nat div" $ x .== y * q + r .|| y .== 0
|
||||
addSideCondition "nat div" $ q .>= 0
|
||||
-- Add assertion about range of remainder.
|
||||
addSideCondition "nat div" $ r .>= 0
|
||||
addSideCondition "nat div" $ r .< y .|| y .== 0
|
||||
-- Return name of variable.
|
||||
return nm
|
||||
freshBoundTerm NatTypeMap (intDiv x y)
|
||||
|
||||
------------------------------------------
|
||||
-- Real operations.
|
||||
@ -1641,25 +1666,6 @@ appSMTExpr ae = do
|
||||
r <- freshConstant "real divison" RealTypeMap
|
||||
addSideCondition "real division" $ (y * asBase r) .== x .|| y .== 0
|
||||
return r
|
||||
IntMod xe ye -> do
|
||||
case ye of
|
||||
SemiRingLiteral SemiRingNat _ _ -> return ()
|
||||
_ -> checkNonlinearSupport i
|
||||
|
||||
x <- mkBaseExpr xe
|
||||
y <- mkBaseExpr ye
|
||||
|
||||
q <- asBase <$> freshConstant "integer mod" NatTypeMap
|
||||
nm <- freshConstant "integer mod" NatTypeMap
|
||||
let r = asBase nm
|
||||
-- Assume x can be composed into quotient and remainder.
|
||||
addSideCondition "integer mod" $ x .== y * q + r .|| y .== 0
|
||||
-- Add assertion about range of remainder.
|
||||
-- Note that IntMod is not defined when y = 0.
|
||||
addSideCondition "integer mod" $ 0 .<= r
|
||||
addSideCondition "integer mod" $ r .< y .|| y .== 0
|
||||
-- Return name of variable.
|
||||
return nm
|
||||
|
||||
RealSqrt xe -> do
|
||||
checkNonlinearSupport i
|
||||
@ -2024,29 +2030,17 @@ appSMTExpr ae = do
|
||||
x <- mkExpr xe
|
||||
freshBoundTerm IntegerTypeMap $ sbvIntTerm (bvWidth xe) (asBase x)
|
||||
|
||||
IntegerToSBV xe w -> do
|
||||
x <- mkExpr xe
|
||||
|
||||
res <- freshConstant "integerToSBV" (BVTypeMap w)
|
||||
let xb = asBase x
|
||||
addSideCondition "integerToSBV" $
|
||||
xb .< fromInteger (minSigned w)
|
||||
.|| xb .> fromInteger (maxSigned w)
|
||||
.|| xb .== sbvIntTerm w (asBase res)
|
||||
return res
|
||||
|
||||
IntegerToBV xe w -> do
|
||||
checkLinearSupport i
|
||||
|
||||
x <- mkExpr xe
|
||||
let xb = asBase x
|
||||
|
||||
res <- freshConstant "integerToBV" (BVTypeMap w)
|
||||
let xb = asBase x
|
||||
-- To ensure there is some solution regardless of xe being negative, we
|
||||
-- accept any model where xb is out of range.
|
||||
addSideCondition "integerToBV" $
|
||||
xb .< 0
|
||||
.|| xb .> fromInteger (maxUnsigned w)
|
||||
.|| xb .== bvIntTerm w (asBase res)
|
||||
bvint <- freshBoundTerm IntegerTypeMap $ bvIntTerm w (asBase res)
|
||||
|
||||
addSideCondition "integerToBV" $
|
||||
(intDivisible (xb - (asBase bvint)) (2^natValue w))
|
||||
return res
|
||||
|
||||
Cplx c -> do
|
||||
|
||||
@ -182,6 +182,12 @@ instance SupportTermOps (Term (Connection s)) where
|
||||
|
||||
integerTerm i = T $ decimal i
|
||||
|
||||
intDiv x y = term_app "div" [x,y]
|
||||
intMod x y = term_app "mod" [x,y]
|
||||
intAbs x = term_app "abs" [x]
|
||||
intDivisible _ 0 = boolExpr True
|
||||
intDivisible x k = term_app "divides" [x, integerTerm (toInteger k)]
|
||||
|
||||
rationalTerm r | d == 1 = T $ decimal n
|
||||
| otherwise = T $ app "/" [decimal n, decimal d]
|
||||
where n = numerator r
|
||||
|
||||
@ -30,12 +30,17 @@ module What4.Utils.AbstractDomains
|
||||
, concreteRange
|
||||
, valueRange
|
||||
, addRange
|
||||
, negateRange
|
||||
, rangeScalarMul
|
||||
, mulRange
|
||||
, joinRange
|
||||
, asSingleRange
|
||||
, rangeCheckEq
|
||||
, rangeCheckLe
|
||||
-- * integer range operations
|
||||
, intAbsRange
|
||||
, intDivRange
|
||||
, intModRange
|
||||
-- * Boolean abstract value
|
||||
, absAnd
|
||||
, absOr
|
||||
@ -54,6 +59,7 @@ module What4.Utils.AbstractDomains
|
||||
, asSingleNatRange
|
||||
, unboundedNatRange
|
||||
, natRangeToRange
|
||||
, natRangeDiv
|
||||
-- * RealAbstractValue
|
||||
, RealAbstractValue(..)
|
||||
, ravSingle
|
||||
@ -144,6 +150,86 @@ data ValueRange tp
|
||||
| MultiRange !(ValueBound tp) !(ValueBound tp)
|
||||
-- ^ Indicates that the number is somewhere between the given upper and lower bound.
|
||||
|
||||
intAbsRange :: ValueRange Integer -> NatValueRange
|
||||
intAbsRange r = case r of
|
||||
SingleRange x -> NatSingleRange (fromInteger (abs x))
|
||||
MultiRange (Inclusive lo) hi | 0 <= lo -> NatMultiRange (fromInteger lo) (fromInteger <$> hi)
|
||||
MultiRange lo (Inclusive hi) | hi <= 0 -> NatMultiRange (fromInteger (negate hi)) (fromInteger . negate <$> lo)
|
||||
MultiRange lo hi -> NatMultiRange 0 ((\x y -> fromInteger $ max (abs x) (abs y)) <$> lo <*> hi)
|
||||
|
||||
-- | Compute an abstract range for integer division. We are using the SMTLib
|
||||
-- division operation, where the division is floor when the divisor is positive
|
||||
-- and ceiling when the divisor is negative. We compute the ranges assuming
|
||||
-- that division by 0 doesn't happen, and we are allowed to return nonsense
|
||||
-- ranges for these cases.
|
||||
intDivRange :: ValueRange Integer -> ValueRange Integer -> ValueRange Integer
|
||||
|
||||
intDivRange (SingleRange x) (SingleRange y)
|
||||
| y == 0 = SingleRange 0 -- NB, nonsense case
|
||||
| y > 0 = SingleRange (x `div` y)
|
||||
| otherwise = SingleRange (negate (x `div` negate y))
|
||||
|
||||
intDivRange (MultiRange lo hi) (SingleRange y)
|
||||
| y == 0 = SingleRange 0 -- NB, nonsense case
|
||||
| y > 0 = MultiRange
|
||||
((\x -> x `div` y) <$> lo)
|
||||
((\x -> x `div` y) <$> hi)
|
||||
| otherwise = negateRange $ MultiRange
|
||||
((\x -> x `div` negate y) <$> lo)
|
||||
((\x -> x `div` negate y) <$> hi)
|
||||
|
||||
intDivRange x (MultiRange (Inclusive lo) hi)
|
||||
-- NB, rule out division-by-zero case
|
||||
| 0 <= lo = intDivAux x (min 1 lo) (min 1 <$> hi)
|
||||
|
||||
intDivRange x (MultiRange lo (Inclusive hi))
|
||||
-- NB, rule out division-by-zero case
|
||||
| hi <= 0 = negateRange (intDivAux x (min 1 (negate hi)) (min 1 . negate <$> lo))
|
||||
|
||||
-- Unlike with real number range division, the ranges do not go all
|
||||
-- the way to infinity when the range contains 0. Instead, the
|
||||
-- bounds have largest magnitute when the divisor is 1 or -1.
|
||||
-- If we have reached this case, the interval should contain both of these
|
||||
-- numbers, so the result is the original range joined with its negation.
|
||||
intDivRange x _ = joinRange x (negateRange x)
|
||||
|
||||
|
||||
-- Here we get to assume 'lo' and 'hi' are strictly positive
|
||||
intDivAux ::
|
||||
ValueRange Integer ->
|
||||
Integer -> ValueBound Integer ->
|
||||
ValueRange Integer
|
||||
intDivAux x lo Unbounded = MultiRange lo' hi'
|
||||
where
|
||||
lo' = case rangeLowBound x of
|
||||
Unbounded -> Unbounded
|
||||
Inclusive z -> Inclusive (min 0 (div z lo))
|
||||
|
||||
hi' = case rangeHiBound x of
|
||||
Unbounded -> Unbounded
|
||||
Inclusive z -> Inclusive (max (-1) (div z lo))
|
||||
|
||||
intDivAux x lo (Inclusive hi) = MultiRange lo' hi'
|
||||
where
|
||||
lo' = case rangeLowBound x of
|
||||
Unbounded -> Unbounded
|
||||
Inclusive z -> Inclusive (min (div z hi) (div z lo))
|
||||
|
||||
hi' = case rangeHiBound x of
|
||||
Unbounded -> Unbounded
|
||||
Inclusive z -> Inclusive (max (div z hi) (div z lo))
|
||||
|
||||
intModRange :: ValueRange Integer -> ValueRange Integer -> NatValueRange
|
||||
intModRange (SingleRange x) (SingleRange y) = NatSingleRange (fromInteger (x `mod` abs y))
|
||||
intModRange (MultiRange (Inclusive lo) (Inclusive hi)) (SingleRange y)
|
||||
| hi' - lo' == hi - lo = NatMultiRange (fromInteger lo') (Inclusive (fromInteger hi'))
|
||||
where
|
||||
lo' = lo `mod` abs y
|
||||
hi' = hi `mod` abs y
|
||||
intModRange _ y = NatMultiRange 0 (pred <$> natRangeHigh (intAbsRange y))
|
||||
|
||||
|
||||
|
||||
addRange :: Num tp => ValueRange tp -> ValueRange tp -> ValueRange tp
|
||||
addRange (SingleRange x) (SingleRange y) = SingleRange (x+y)
|
||||
addRange (SingleRange x) (MultiRange ly uy) = MultiRange ((x+) <$> ly) ((x+) <$> uy)
|
||||
@ -162,7 +248,7 @@ rangeIsInteger (MultiRange (Inclusive l) (Inclusive u))
|
||||
, denominator u /= 1 = Just False
|
||||
rangeIsInteger _ = Nothing
|
||||
|
||||
-- | Multiply two ranges together.
|
||||
-- | Multiply a range by a scalar value
|
||||
rangeScalarMul :: (Ord tp, Num tp) => tp -> ValueRange tp -> ValueRange tp
|
||||
rangeScalarMul x (SingleRange y) = SingleRange (x*y)
|
||||
rangeScalarMul x (MultiRange ly uy)
|
||||
@ -170,6 +256,10 @@ rangeScalarMul x (MultiRange ly uy)
|
||||
| x == 0 = SingleRange 0
|
||||
| otherwise = assert (x > 0) $ MultiRange ((x*) <$> ly) ((x*) <$> uy)
|
||||
|
||||
negateRange :: (Num tp) => ValueRange tp -> ValueRange tp
|
||||
negateRange (SingleRange x) = SingleRange (negate x)
|
||||
negateRange (MultiRange lo hi) = MultiRange (negate <$> hi) (negate <$> lo)
|
||||
|
||||
-- | Multiply two ranges together.
|
||||
mulRange :: (Ord tp, Num tp) => ValueRange tp -> ValueRange tp -> ValueRange tp
|
||||
mulRange (SingleRange x) y = rangeScalarMul x y
|
||||
@ -370,20 +460,20 @@ absOr _ (Just True) = Just True
|
||||
absOr Nothing Nothing = Nothing
|
||||
|
||||
data NatValueRange
|
||||
= NatSingleRange !Integer
|
||||
| NatMultiRange !Integer !(ValueBound Integer)
|
||||
= NatSingleRange !Natural
|
||||
| NatMultiRange !Natural !(ValueBound Natural)
|
||||
|
||||
asSingleNatRange :: NatValueRange -> Maybe Natural
|
||||
asSingleNatRange (NatSingleRange x) = Just (fromInteger x)
|
||||
asSingleNatRange (NatSingleRange x) = Just x
|
||||
asSingleNatRange _ = Nothing
|
||||
|
||||
natRange :: Integer -> ValueBound Integer -> NatValueRange
|
||||
natRange :: Natural -> ValueBound Natural -> NatValueRange
|
||||
natRange x (Inclusive y)
|
||||
| x == y = NatSingleRange x
|
||||
natRange x y = NatMultiRange x y
|
||||
|
||||
natSingleRange :: Natural -> NatValueRange
|
||||
natSingleRange = NatSingleRange . toInteger
|
||||
natSingleRange = NatSingleRange
|
||||
|
||||
natRangeAdd :: NatValueRange -> NatValueRange -> NatValueRange
|
||||
natRangeAdd (NatSingleRange x) (NatSingleRange y) = NatSingleRange (x+y)
|
||||
@ -391,7 +481,7 @@ natRangeAdd (NatSingleRange x) (NatMultiRange loy hiy) = NatMultiRange (x
|
||||
natRangeAdd (NatMultiRange lox hix) (NatSingleRange y) = NatMultiRange (lox + y) ((+) <$> hix <*> pure y)
|
||||
natRangeAdd (NatMultiRange lox hix) (NatMultiRange loy hiy) = NatMultiRange (lox + loy) ((+) <$> hix <*> hiy)
|
||||
|
||||
natRangeScalarMul :: Integer -> NatValueRange -> NatValueRange
|
||||
natRangeScalarMul :: Natural -> NatValueRange -> NatValueRange
|
||||
natRangeScalarMul x (NatSingleRange y) = NatSingleRange (x * y)
|
||||
natRangeScalarMul x (NatMultiRange lo hi) = NatMultiRange (x * lo) ((x*) <$> hi)
|
||||
|
||||
@ -401,6 +491,16 @@ natRangeMul x (NatSingleRange y) = natRangeScalarMul y x
|
||||
natRangeMul (NatMultiRange lox hix) (NatMultiRange loy hiy) =
|
||||
NatMultiRange (lox * loy) ((*) <$> hix <*> hiy)
|
||||
|
||||
natRangeDiv :: NatValueRange -> NatValueRange -> NatValueRange
|
||||
natRangeDiv (NatSingleRange x) (NatSingleRange y) =
|
||||
NatSingleRange (x `div` y)
|
||||
natRangeDiv (NatMultiRange lo hi) (NatSingleRange y) =
|
||||
NatMultiRange (lo `div` y) ((`div` y) <$> hi)
|
||||
natRangeDiv x (NatMultiRange lo (Inclusive hi)) =
|
||||
NatMultiRange (div (natRangeLow x) hi) ((`div` lo) <$> natRangeHigh x)
|
||||
natRangeDiv x (NatMultiRange lo Unbounded) =
|
||||
NatMultiRange 0 ((`div` lo) <$> natRangeHigh x)
|
||||
|
||||
-- | Compute the smallest range containing both ranges.
|
||||
natRangeJoin :: NatValueRange -> NatValueRange -> NatValueRange
|
||||
natRangeJoin (NatSingleRange x) (NatSingleRange y)
|
||||
@ -411,11 +511,11 @@ natRangeJoin x y = NatMultiRange (min lx ly) (maxValueBound ux uy)
|
||||
ly = natRangeLow y
|
||||
uy = natRangeHigh y
|
||||
|
||||
natRangeLow :: NatValueRange -> Integer
|
||||
natRangeLow :: NatValueRange -> Natural
|
||||
natRangeLow (NatSingleRange x) = x
|
||||
natRangeLow (NatMultiRange lx _) = lx
|
||||
|
||||
natRangeHigh :: NatValueRange -> ValueBound Integer
|
||||
natRangeHigh :: NatValueRange -> ValueBound Natural
|
||||
natRangeHigh (NatSingleRange x) = Inclusive x
|
||||
natRangeHigh (NatMultiRange _ u) = u
|
||||
|
||||
@ -463,9 +563,8 @@ natJoinRange x y = NatMultiRange (min lx ly) (maxValueBound ux uy)
|
||||
uy = natRangeHigh y
|
||||
|
||||
natRangeToRange :: NatValueRange -> ValueRange Integer
|
||||
natRangeToRange (NatSingleRange x) = SingleRange x
|
||||
natRangeToRange (NatMultiRange l u) = MultiRange (Inclusive l) u
|
||||
|
||||
natRangeToRange (NatSingleRange x) = SingleRange (toInteger x)
|
||||
natRangeToRange (NatMultiRange l u) = MultiRange (Inclusive (toInteger l)) (toInteger <$> u)
|
||||
|
||||
|
||||
-- | An abstract value represents a disjoint st of values.
|
||||
|
||||
Loading…
Reference in New Issue
Block a user