1----------------------------------------------------------------------------- 2-- | 3-- Module : Data.SBV.Core.Operations 4-- Copyright : (c) Levent Erkok 5-- License : BSD3 6-- Maintainer: erkokl@gmail.com 7-- Stability : experimental 8-- 9-- Constructors and basic operations on symbolic values 10----------------------------------------------------------------------------- 11 12{-# LANGUAGE BangPatterns #-} 13 14{-# OPTIONS_GHC -Wall -Werror #-} 15 16module Data.SBV.Core.Operations 17 ( 18 -- ** Basic constructors 19 svTrue, svFalse, svBool 20 , svInteger, svFloat, svDouble, svFloatingPoint, svReal, svEnumFromThenTo, svString, svChar 21 -- ** Basic destructors 22 , svAsBool, svAsInteger, svNumerator, svDenominator 23 -- ** Basic operations 24 , svPlus, svTimes, svMinus, svUNeg, svAbs 25 , svDivide, svQuot, svRem, svQuotRem 26 , svEqual, svNotEqual, svStrongEqual, svSetEqual 27 , svLessThan, svGreaterThan, svLessEq, svGreaterEq, svStructuralLessThan 28 , svAnd, svOr, svXOr, svNot 29 , svShl, svShr, svRol, svRor 30 , svExtract, svJoin 31 , svIte, svLazyIte, svSymbolicMerge 32 , svSelect 33 , svSign, svUnsign, svSetBit, svWordFromBE, svWordFromLE 34 , svExp, svFromIntegral 35 -- ** Overflows 36 , svMkOverflow 37 -- ** Derived operations 38 , svToWord1, svFromWord1, svTestBit 39 , svShiftLeft, svShiftRight 40 , svRotateLeft, svRotateRight 41 , svBarrelRotateLeft, svBarrelRotateRight 42 , svBlastLE, svBlastBE 43 , svAddConstant, svIncrement, svDecrement 44 -- ** Basic array operations 45 , SArr(..), readSArr, writeSArr, mergeSArr, newSArr, eqSArr 46 , SFunArr(..), readSFunArr, writeSFunArr, mergeSFunArr, newSFunArr 47 -- Utils 48 , mkSymOp 49 ) 50 where 51 52import Data.Bits (Bits(..)) 53import Data.List (genericIndex, genericLength, genericTake) 54 55import qualified Data.IORef as R (modifyIORef', newIORef, readIORef) 56import qualified Data.Map.Strict as Map (toList, fromList, lookup) 57import qualified Data.IntMap.Strict as IMap (IntMap, empty, toAscList, fromAscList, lookup, size, insert, delete) 58 59import Data.SBV.Core.AlgReals 60import Data.SBV.Core.Kind 61import Data.SBV.Core.Concrete 62import Data.SBV.Core.Symbolic 63import Data.SBV.Core.SizedFloats 64 65import Data.Ratio 66 67import Data.SBV.Utils.Numeric (fpIsEqualObjectH) 68 69-------------------------------------------------------------------------------- 70-- Basic constructors 71 72-- | Boolean True. 73svTrue :: SVal 74svTrue = SVal KBool (Left trueCV) 75 76-- | Boolean False. 77svFalse :: SVal 78svFalse = SVal KBool (Left falseCV) 79 80-- | Convert from a Boolean. 81svBool :: Bool -> SVal 82svBool b = if b then svTrue else svFalse 83 84-- | Convert from an Integer. 85svInteger :: Kind -> Integer -> SVal 86svInteger k n = SVal k (Left $! mkConstCV k n) 87 88-- | Convert from a Float 89svFloat :: Float -> SVal 90svFloat f = SVal KFloat (Left $! CV KFloat (CFloat f)) 91 92-- | Convert from a Double 93svDouble :: Double -> SVal 94svDouble d = SVal KDouble (Left $! CV KDouble (CDouble d)) 95 96-- | Convert from a generalized floating point 97svFloatingPoint :: FP -> SVal 98svFloatingPoint f@(FP eb sb _) = SVal k (Left $! CV k (CFP f)) 99 where k = KFP eb sb 100 101-- | Convert from a String 102svString :: String -> SVal 103svString s = SVal KString (Left $! CV KString (CString s)) 104 105-- | Convert from a Char 106svChar :: Char -> SVal 107svChar c = SVal KChar (Left $! CV KChar (CChar c)) 108 109-- | Convert from a Rational 110svReal :: Rational -> SVal 111svReal d = SVal KReal (Left $! CV KReal (CAlgReal (fromRational d))) 112 113-------------------------------------------------------------------------------- 114-- Basic destructors 115 116-- | Extract a bool, by properly interpreting the integer stored. 117svAsBool :: SVal -> Maybe Bool 118svAsBool (SVal _ (Left cv)) = Just (cvToBool cv) 119svAsBool _ = Nothing 120 121-- | Extract an integer from a concrete value. 122svAsInteger :: SVal -> Maybe Integer 123svAsInteger (SVal _ (Left (CV _ (CInteger n)))) = Just n 124svAsInteger _ = Nothing 125 126-- | Grab the numerator of an SReal, if available 127svNumerator :: SVal -> Maybe Integer 128svNumerator (SVal KReal (Left (CV KReal (CAlgReal (AlgRational True r))))) = Just $ numerator r 129svNumerator _ = Nothing 130 131-- | Grab the denominator of an SReal, if available 132svDenominator :: SVal -> Maybe Integer 133svDenominator (SVal KReal (Left (CV KReal (CAlgReal (AlgRational True r))))) = Just $ denominator r 134svDenominator _ = Nothing 135 136------------------------------------------------------------------------------------- 137-- | Constructing [x, y, .. z] and [x .. y]. Only works when all arguments are concrete and integral and the result is guaranteed finite 138-- Note that the it isn't "obviously" clear why the following works; after all we're doing the construction over Integer's and mapping 139-- it back to other types such as SIntN/SWordN. The reason is that the values we receive are guaranteed to be in their domains; and thus 140-- the lifting to Integers preserves the bounds; and then going back is just fine. So, things like @[1, 5 .. 200] :: [SInt8]@ work just 141-- fine (end evaluate to empty list), since we see @[1, 5 .. -56]@ in the @Integer@ domain. Also note the explicit check for @s /= f@ 142-- below to make sure we don't stutter and produce an infinite list. 143svEnumFromThenTo :: SVal -> Maybe SVal -> SVal -> Maybe [SVal] 144svEnumFromThenTo bf mbs bt 145 | Just bs <- mbs, Just f <- svAsInteger bf, Just s <- svAsInteger bs, Just t <- svAsInteger bt, s /= f = Just $ map (svInteger (kindOf bf)) [f, s .. t] 146 | Nothing <- mbs, Just f <- svAsInteger bf, Just t <- svAsInteger bt = Just $ map (svInteger (kindOf bf)) [f .. t] 147 | True = Nothing 148 149------------------------------------------------------------------------------------- 150-- Basic operations 151 152-- | Addition. 153svPlus :: SVal -> SVal -> SVal 154svPlus x y 155 | isConcreteZero x = y 156 | isConcreteZero y = x 157 | True = liftSym2 (mkSymOp Plus) [rationalCheck] (+) (+) (+) (+) (+) x y 158 159-- | Multiplication. 160svTimes :: SVal -> SVal -> SVal 161svTimes x y 162 | isConcreteZero x = x 163 | isConcreteZero y = y 164 | isConcreteOne x = y 165 | isConcreteOne y = x 166 | True = liftSym2 (mkSymOp Times) [rationalCheck] (*) (*) (*) (*) (*) x y 167 168-- | Subtraction. 169svMinus :: SVal -> SVal -> SVal 170svMinus x y 171 | isConcreteZero y = x 172 | True = liftSym2 (mkSymOp Minus) [rationalCheck] (-) (-) (-) (-) (-) x y 173 174-- | Unary minus. We handle arbitrary-FP's specially here, just for the negated literals. 175svUNeg :: SVal -> SVal 176svUNeg = liftSym1 (mkSymOp1 UNeg) negate negate negate negate negate 177 178-- | Absolute value. 179svAbs :: SVal -> SVal 180svAbs = liftSym1 (mkSymOp1 Abs) abs abs abs abs abs 181 182-- | Division. 183svDivide :: SVal -> SVal -> SVal 184svDivide = liftSym2 (mkSymOp Quot) [rationalCheck] (/) idiv (/) (/) (/) 185 where idiv x 0 = x 186 idiv x y = x `div` y 187 188-- | Exponentiation. 189svExp :: SVal -> SVal -> SVal 190svExp b e 191 | Just x <- svAsInteger e 192 = if x >= 0 then let go n v 193 | n == 0 = one 194 | even n = go (n `div` 2) (svTimes v v) 195 | True = svTimes v $ go (n `div` 2) (svTimes v v) 196 in go x b 197 else error $ "svExp: exponentiation: negative exponent: " ++ show x 198 | not (isBounded e) || hasSign e 199 = error $ "svExp: exponentiation only works with unsigned bounded symbolic exponents, kind: " ++ show (kindOf e) 200 | True 201 = prod $ zipWith (\use n -> svIte use n one) 202 (svBlastLE e) 203 (iterate (\x -> svTimes x x) b) 204 where prod = foldr svTimes one 205 one = svInteger (kindOf b) 1 206 207-- | Bit-blast: Little-endian. Assumes the input is a bit-vector. 208svBlastLE :: SVal -> [SVal] 209svBlastLE x = map (svTestBit x) [0 .. intSizeOf x - 1] 210 211-- | Set a given bit at index 212svSetBit :: SVal -> Int -> SVal 213svSetBit x i = x `svOr` svInteger (kindOf x) (bit i :: Integer) 214 215-- | Bit-blast: Big-endian. Assumes the input is a bit-vector. 216svBlastBE :: SVal -> [SVal] 217svBlastBE = reverse . svBlastLE 218 219-- | Un-bit-blast from big-endian representation to a word of the right size. 220-- The input is assumed to be unsigned. 221svWordFromLE :: [SVal] -> SVal 222svWordFromLE bs = go zero 0 bs 223 where zero = svInteger (KBounded False (length bs)) 0 224 go !acc _ [] = acc 225 go !acc !i (x:xs) = go (svIte x (svSetBit acc i) acc) (i+1) xs 226 227-- | Un-bit-blast from little-endian representation to a word of the right size. 228-- The input is assumed to be unsigned. 229svWordFromBE :: [SVal] -> SVal 230svWordFromBE = svWordFromLE . reverse 231 232-- | Add a constant value: 233svAddConstant :: Integral a => SVal -> a -> SVal 234svAddConstant x i = x `svPlus` svInteger (kindOf x) (fromIntegral i) 235 236-- | Increment: 237svIncrement :: SVal -> SVal 238svIncrement x = svAddConstant x (1::Integer) 239 240-- | Decrement: 241svDecrement :: SVal -> SVal 242svDecrement x = svAddConstant x (-1 :: Integer) 243 244-- | Quotient: Overloaded operation whose meaning depends on the kind at which 245-- it is used: For unbounded integers, it corresponds to the SMT-Lib 246-- "div" operator ("Euclidean" division, which always has a 247-- non-negative remainder). For unsigned bitvectors, it is "bvudiv"; 248-- and for signed bitvectors it is "bvsdiv", which rounds toward zero. 249-- Division by 0 is defined s.t. @x/0 = 0@, which holds even when @x@ itself is @0@. 250svQuot :: SVal -> SVal -> SVal 251svQuot x y 252 | isConcreteZero x = x 253 | isConcreteZero y = svInteger (kindOf x) 0 254 | isConcreteOne y = x 255 | True = liftSym2 (mkSymOp Quot) [nonzeroCheck] 256 (noReal "quot") quot' (noFloat "quot") (noDouble "quot") (noFP "quot") x y 257 where 258 quot' a b | kindOf x == KUnbounded = div a (abs b) * signum b 259 | otherwise = quot a b 260 261-- | Remainder: Overloaded operation whose meaning depends on the kind at which 262-- it is used: For unbounded integers, it corresponds to the SMT-Lib 263-- "mod" operator (always non-negative). For unsigned bitvectors, it 264-- is "bvurem"; and for signed bitvectors it is "bvsrem", which rounds 265-- toward zero (sign of remainder matches that of @x@). Division by 0 is 266-- defined s.t. @x/0 = 0@, which holds even when @x@ itself is @0@. 267svRem :: SVal -> SVal -> SVal 268svRem x y 269 | isConcreteZero x = x 270 | isConcreteZero y = x 271 | isConcreteOne y = svInteger (kindOf x) 0 272 | True = liftSym2 (mkSymOp Rem) [nonzeroCheck] 273 (noReal "rem") rem' (noFloat "rem") (noDouble "rem") (noFP "rem") x y 274 where 275 rem' a b | kindOf x == KUnbounded = mod a (abs b) 276 | otherwise = rem a b 277 278-- | Combination of quot and rem 279svQuotRem :: SVal -> SVal -> (SVal, SVal) 280svQuotRem x y = (x `svQuot` y, x `svRem` y) 281 282-- | Optimize away x == true and x /= false to x; otherwise just do eqOpt 283eqOptBool :: Op -> SV -> SV -> SV -> Maybe SV 284eqOptBool op w x y 285 | k == KBool && op == Equal && x == trueSV = Just y -- true .== y --> y 286 | k == KBool && op == Equal && y == trueSV = Just x -- x .== true --> x 287 | k == KBool && op == NotEqual && x == falseSV = Just y -- false ./= y --> y 288 | k == KBool && op == NotEqual && y == falseSV = Just x -- x ./= false --> x 289 | True = eqOpt w x y -- fallback 290 where k = swKind x 291 292-- | Equality. 293svEqual :: SVal -> SVal -> SVal 294svEqual a b 295 | isSet a && isSet b 296 = svSetEqual a b 297 | True 298 = liftSym2B (mkSymOpSC (eqOptBool Equal trueSV) Equal) rationalCheck (==) (==) (==) (==) (==) (==) (==) (==) (==) (==) (==) (==) a b 299 300-- | Inequality. 301svNotEqual :: SVal -> SVal -> SVal 302svNotEqual a b 303 | isSet a && isSet b 304 = svNot $ svEqual a b 305 | True 306 = liftSym2B (mkSymOpSC (eqOptBool NotEqual falseSV) NotEqual) rationalCheck (/=) (/=) (/=) (/=) (/=) (/=) (/=) (/=) (/=) (/=) (/=) (/=) a b 307 308-- | Set equality. Note that we only do constant folding if we get both a regular or both a 309-- complement set. Otherwise we get a symbolic value even if they might be completely concrete. 310svSetEqual :: SVal -> SVal -> SVal 311svSetEqual sa sb 312 | not (isSet sa && isSet sb && kindOf sa == kindOf sb) 313 = error $ "Data.SBV.svSetEqual: Called on ill-typed args: " ++ show (kindOf sa, kindOf sb) 314 | Just (RegularSet a) <- getSet sa, Just (RegularSet b) <- getSet sb 315 = svBool (a == b) 316 | Just (ComplementSet a) <- getSet sa, Just (ComplementSet b) <- getSet sb 317 = svBool (a == b) 318 | True 319 = SVal KBool $ Right $ cache r 320 where getSet (SVal _ (Left (CV _ (CSet s)))) = Just s 321 getSet _ = Nothing 322 323 r st = do sva <- svToSV st sa 324 svb <- svToSV st sb 325 newExpr st KBool $ SBVApp (SetOp SetEqual) [sva, svb] 326 327-- | Strong equality. Only matters on floats, where it says @NaN@ equals @NaN@ and @+0@ and @-0@ are different. 328-- Otherwise equivalent to `svEqual`. 329svStrongEqual :: SVal -> SVal -> SVal 330svStrongEqual x y | isFloat x, Just f1 <- getF x, Just f2 <- getF y = svBool $ f1 `fpIsEqualObjectH` f2 331 | isDouble x, Just f1 <- getD x, Just f2 <- getD y = svBool $ f1 `fpIsEqualObjectH` f2 332 | isFP x, Just f1 <- getFP x, Just f2 <- getFP y = svBool $ f1 `fpIsEqualObjectH` f2 333 | isFloat x || isDouble x || isFP x = SVal KBool $ Right $ cache r 334 | True = svEqual x y 335 where getF (SVal _ (Left (CV _ (CFloat f)))) = Just f 336 getF _ = Nothing 337 338 getD (SVal _ (Left (CV _ (CDouble d)))) = Just d 339 getD _ = Nothing 340 341 getFP (SVal _ (Left (CV _ (CFP f)))) = Just f 342 getFP _ = Nothing 343 344 r st = do sx <- svToSV st x 345 sy <- svToSV st y 346 newExpr st KBool (SBVApp (IEEEFP FP_ObjEqual) [sx, sy]) 347 348-- | Less than. 349svLessThan :: SVal -> SVal -> SVal 350svLessThan x y 351 | isConcreteMax x = svFalse 352 | isConcreteMin y = svFalse 353 | True = liftSym2B (mkSymOpSC (eqOpt falseSV) LessThan) rationalCheck (<) (<) (<) (<) (<) (<) (<) (<) (<) (<) (<) (uiLift "<" (<)) x y 354 355-- | Greater than. 356svGreaterThan :: SVal -> SVal -> SVal 357svGreaterThan x y 358 | isConcreteMin x = svFalse 359 | isConcreteMax y = svFalse 360 | True = liftSym2B (mkSymOpSC (eqOpt falseSV) GreaterThan) rationalCheck (>) (>) (>) (>) (>) (>) (>) (>) (>) (>) (>) (uiLift ">" (>)) x y 361 362-- | Less than or equal to. 363svLessEq :: SVal -> SVal -> SVal 364svLessEq x y 365 | isConcreteMin x = svTrue 366 | isConcreteMax y = svTrue 367 | True = liftSym2B (mkSymOpSC (eqOpt trueSV) LessEq) rationalCheck (<=) (<=) (<=) (<=) (<=) (<=) (<=) (<=) (<=) (<=) (<=) (uiLift "<=" (<=)) x y 368 369-- | Greater than or equal to. 370svGreaterEq :: SVal -> SVal -> SVal 371svGreaterEq x y 372 | isConcreteMax x = svTrue 373 | isConcreteMin y = svTrue 374 | True = liftSym2B (mkSymOpSC (eqOpt trueSV) GreaterEq) rationalCheck (>=) (>=) (>=) (>=) (>=) (>=) (>=) (>=) (>=) (>=) (>=) (uiLift ">=" (>=)) x y 375 376-- | Bitwise and. 377svAnd :: SVal -> SVal -> SVal 378svAnd x y 379 | isConcreteZero x = x 380 | isConcreteOnes x = y 381 | isConcreteZero y = y 382 | isConcreteOnes y = x 383 | True = liftSym2 (mkSymOpSC opt And) [] (noReal ".&.") (.&.) (noFloat ".&.") (noDouble ".&.") (noFP ".&.") x y 384 where opt a b 385 | a == falseSV || b == falseSV = Just falseSV 386 | a == trueSV = Just b 387 | b == trueSV = Just a 388 | True = Nothing 389 390-- | Bitwise or. 391svOr :: SVal -> SVal -> SVal 392svOr x y 393 | isConcreteZero x = y 394 | isConcreteOnes x = x 395 | isConcreteZero y = x 396 | isConcreteOnes y = y 397 | True = liftSym2 (mkSymOpSC opt Or) [] 398 (noReal ".|.") (.|.) (noFloat ".|.") (noDouble ".|.") (noFP ".|.") x y 399 where opt a b 400 | a == trueSV || b == trueSV = Just trueSV 401 | a == falseSV = Just b 402 | b == falseSV = Just a 403 | True = Nothing 404 405-- | Bitwise xor. 406svXOr :: SVal -> SVal -> SVal 407svXOr x y 408 | isConcreteZero x = y 409 | isConcreteOnes x = svNot y 410 | isConcreteZero y = x 411 | isConcreteOnes y = svNot x 412 | True = liftSym2 (mkSymOpSC opt XOr) [] 413 (noReal "xor") xor (noFloat "xor") (noDouble "xor") (noFP "xor") x y 414 where opt a b 415 | a == b && swKind a == KBool = Just falseSV 416 | a == falseSV = Just b 417 | b == falseSV = Just a 418 | True = Nothing 419 420-- | Bitwise complement. 421svNot :: SVal -> SVal 422svNot = liftSym1 (mkSymOp1SC opt Not) 423 (noRealUnary "complement") complement 424 (noFloatUnary "complement") (noDoubleUnary "complement") (noFPUnary "complement") 425 where opt a 426 | a == falseSV = Just trueSV 427 | a == trueSV = Just falseSV 428 | True = Nothing 429 430-- | Shift left by a constant amount. Translates to the "bvshl" 431-- operation in SMT-Lib. 432-- 433-- NB. Haskell spec says the behavior is undefined if the shift amount 434-- is negative. We arbitrarily return the value unchanged if this is the case. 435svShl :: SVal -> Int -> SVal 436svShl x i 437 | i <= 0 438 = x 439 | isBounded x, i >= intSizeOf x 440 = svInteger k 0 441 | True 442 = x `svShiftLeft` svInteger k (fromIntegral i) 443 where k = kindOf x 444 445-- | Shift right by a constant amount. Translates to either "bvlshr" 446-- (logical shift right) or "bvashr" (arithmetic shift right) in 447-- SMT-Lib, depending on whether @x@ is a signed bitvector. 448-- 449-- NB. Haskell spec says the behavior is undefined if the shift amount 450-- is negative. We arbitrarily return the value unchanged if this is the case. 451svShr :: SVal -> Int -> SVal 452svShr x i 453 | i <= 0 454 = x 455 | isBounded x, i >= intSizeOf x 456 = if not (hasSign x) 457 then z 458 else svIte (x `svLessThan` z) neg1 z 459 | True 460 = x `svShiftRight` svInteger k (fromIntegral i) 461 where k = kindOf x 462 z = svInteger k 0 463 neg1 = svInteger k (-1) 464 465-- | Rotate-left, by a constant. 466-- 467-- NB. Haskell spec says the behavior is undefined if the shift amount 468-- is negative. We arbitrarily return the value unchanged if this is the case. 469svRol :: SVal -> Int -> SVal 470svRol x i 471 | i <= 0 472 = x 473 | True 474 = case kindOf x of 475 KBounded _ sz -> liftSym1 (mkSymOp1 (Rol (i `mod` sz))) 476 (noRealUnary "rotateL") (rot True sz i) 477 (noFloatUnary "rotateL") (noDoubleUnary "rotateL") (noFPUnary "rotateL") x 478 _ -> svShl x i -- for unbounded Integers, rotateL is the same as shiftL in Haskell 479 480-- | Rotate-right, by a constant. 481-- 482-- NB. Haskell spec says the behavior is undefined if the shift amount 483-- is negative. We arbitrarily return the value unchanged if this is the case. 484svRor :: SVal -> Int -> SVal 485svRor x i 486 | i <= 0 487 = x 488 | True 489 = case kindOf x of 490 KBounded _ sz -> liftSym1 (mkSymOp1 (Ror (i `mod` sz))) 491 (noRealUnary "rotateR") (rot False sz i) 492 (noFloatUnary "rotateR") (noDoubleUnary "rotateR") (noFPUnary "rotateR") x 493 _ -> svShr x i -- for unbounded integers, rotateR is the same as shiftR in Haskell 494 495-- | Generic rotation. Since the underlying representation is just Integers, rotations has to be 496-- careful on the bit-size. 497rot :: Bool -> Int -> Int -> Integer -> Integer 498rot toLeft sz amt x 499 | sz < 2 = x 500 | True = norm x y' `shiftL` y .|. norm (x `shiftR` y') y 501 where (y, y') | toLeft = (amt `mod` sz, sz - y) 502 | True = (sz - y', amt `mod` sz) 503 norm v s = v .&. ((1 `shiftL` s) - 1) 504 505-- | Extract bit-sequences. 506svExtract :: Int -> Int -> SVal -> SVal 507svExtract i j x@(SVal (KBounded s _) _) 508 | i < j 509 = SVal k (Left $! CV k (CInteger 0)) 510 | SVal _ (Left (CV _ (CInteger v))) <- x 511 = SVal k (Left $! normCV (CV k (CInteger (v `shiftR` j)))) 512 | True 513 = SVal k (Right (cache y)) 514 where k = KBounded s (i - j + 1) 515 y st = do sv <- svToSV st x 516 newExpr st k (SBVApp (Extract i j) [sv]) 517svExtract _ _ _ = error "extract: non-bitvector type" 518 519-- | Join two words, by concatenating 520svJoin :: SVal -> SVal -> SVal 521svJoin x@(SVal (KBounded s i) a) y@(SVal (KBounded _ j) b) 522 | i == 0 = y 523 | j == 0 = x 524 | Left (CV _ (CInteger m)) <- a, Left (CV _ (CInteger n)) <- b 525 = SVal k (Left $! CV k (CInteger (m `shiftL` j .|. n))) 526 | True 527 = SVal k (Right (cache z)) 528 where 529 k = KBounded s (i + j) 530 z st = do xsw <- svToSV st x 531 ysw <- svToSV st y 532 newExpr st k (SBVApp Join [xsw, ysw]) 533svJoin _ _ = error "svJoin: non-bitvector type" 534 535-- | If-then-else. This one will force branches. 536svIte :: SVal -> SVal -> SVal -> SVal 537svIte t a b = svSymbolicMerge (kindOf a) True t a b 538 539-- | Lazy If-then-else. This one will delay forcing the branches unless it's really necessary. 540svLazyIte :: Kind -> SVal -> SVal -> SVal -> SVal 541svLazyIte k t a b = svSymbolicMerge k False t a b 542 543-- | Merge two symbolic values, at kind @k@, possibly @force@'ing the branches to make 544-- sure they do not evaluate to the same result. 545svSymbolicMerge :: Kind -> Bool -> SVal -> SVal -> SVal -> SVal 546svSymbolicMerge k force t a b 547 | Just r <- svAsBool t 548 = if r then a else b 549 | force, rationalSBVCheck a b, sameResult a b 550 = a 551 | True 552 = SVal k $ Right $ cache c 553 where sameResult (SVal _ (Left c1)) (SVal _ (Left c2)) = c1 == c2 554 sameResult _ _ = False 555 556 c st = do swt <- svToSV st t 557 case () of 558 () | swt == trueSV -> svToSV st a -- these two cases should never be needed as we expect symbolicMerge to be 559 () | swt == falseSV -> svToSV st b -- called with symbolic tests, but just in case.. 560 () -> do {- It is tempting to record the choice of the test expression here as we branch down to the 'then' and 'else' branches. That is, 561 when we evaluate 'a', we can make use of the fact that the test expression is True, and similarly we can use the fact that it 562 is False when b is evaluated. In certain cases this can cut down on symbolic simulation significantly, for instance if 563 repetitive decisions are made in a recursive loop. Unfortunately, the implementation of this idea is quite tricky, due to 564 our sharing based implementation. As the 'then' branch is evaluated, we will create many expressions that are likely going 565 to be "reused" when the 'else' branch is executed. But, it would be *dead wrong* to share those values, as they were "cached" 566 under the incorrect assumptions. To wit, consider the following: 567 568 foo x y = ite (y .== 0) k (k+1) 569 where k = ite (y .== 0) x (x+1) 570 571 When we reduce the 'then' branch of the first ite, we'd record the assumption that y is 0. But while reducing the 'then' branch, we'd 572 like to share @k@, which would evaluate (correctly) to @x@ under the given assumption. When we backtrack and evaluate the 'else' 573 branch of the first ite, we'd see @k@ is needed again, and we'd look it up from our sharing map to find (incorrectly) that its value 574 is @x@, which was stored there under the assumption that y was 0, which no longer holds. Clearly, this is unsound. 575 576 A sound implementation would have to precisely track which assumptions were active at the time expressions get shared. That is, 577 in the above example, we should record that the value of @k@ was cached under the assumption that @y@ is 0. While sound, this 578 approach unfortunately leads to significant loss of valid sharing when the value itself had nothing to do with the assumption itself. 579 To wit, consider: 580 581 foo x y = ite (y .== 0) k (k+1) 582 where k = x+5 583 584 If we tracked the assumptions, we would recompute @k@ twice, since the branch assumptions would differ. Clearly, there is no need to 585 re-compute @k@ in this case since its value is independent of @y@. Note that the whole SBV performance story is based on aggressive sharing, 586 and losing that would have other significant ramifications. 587 588 The "proper" solution would be to track, with each shared computation, precisely which assumptions it actually *depends* on, rather 589 than blindly recording all the assumptions present at that time. SBV's symbolic simulation engine clearly has all the info needed to do this 590 properly, but the implementation is not straightforward at all. For each subexpression, we would need to chase down its dependencies 591 transitively, which can require a lot of scanning of the generated program causing major slow-down; thus potentially defeating the 592 whole purpose of sharing in the first place. 593 594 Design choice: Keep it simple, and simply do not track the assumption at all. This will maximize sharing, at the cost of evaluating 595 unreachable branches. I think the simplicity is more important at this point than efficiency. 596 597 Also note that the user can avoid most such issues by properly combining if-then-else's with common conditions together. That is, the 598 first program above should be written like this: 599 600 foo x y = ite (y .== 0) x (x+2) 601 602 In general, the following transformations should be done whenever possible: 603 604 ite e1 (ite e1 e2 e3) e4 --> ite e1 e2 e4 605 ite e1 e2 (ite e1 e3 e4) --> ite e1 e2 e4 606 607 This is in accordance with the general rule-of-thumb stating conditionals should be avoided as much as possible. However, we might prefer 608 the following: 609 610 ite e1 (f e2 e4) (f e3 e5) --> f (ite e1 e2 e3) (ite e1 e4 e5) 611 612 especially if this expression happens to be inside 'f's body itself (i.e., when f is recursive), since it reduces the number of 613 recursive calls. Clearly, programming with symbolic simulation in mind is another kind of beast altogether. 614 -} 615 let sta = st `extendSValPathCondition` svAnd t 616 let stb = st `extendSValPathCondition` svAnd (svNot t) 617 swa <- svToSV sta a -- evaluate 'then' branch 618 swb <- svToSV stb b -- evaluate 'else' branch 619 620 -- merge, but simplify for certain boolean cases: 621 case () of 622 () | swa == swb -> return swa -- if t then a else a ==> a 623 () | swa == trueSV && swb == falseSV -> return swt -- if t then true else false ==> t 624 () | swa == falseSV && swb == trueSV -> newExpr st k (SBVApp Not [swt]) -- if t then false else true ==> not t 625 () | swa == trueSV -> newExpr st k (SBVApp Or [swt, swb]) -- if t then true else b ==> t OR b 626 () | swa == falseSV -> do swt' <- newExpr st KBool (SBVApp Not [swt]) 627 newExpr st k (SBVApp And [swt', swb]) -- if t then false else b ==> t' AND b 628 () | swb == trueSV -> do swt' <- newExpr st KBool (SBVApp Not [swt]) 629 newExpr st k (SBVApp Or [swt', swa]) -- if t then a else true ==> t' OR a 630 () | swb == falseSV -> newExpr st k (SBVApp And [swt, swa]) -- if t then a else false ==> t AND a 631 () -> newExpr st k (SBVApp Ite [swt, swa, swb]) 632 633-- | Total indexing operation. @svSelect xs default index@ is 634-- intuitively the same as @xs !! index@, except it evaluates to 635-- @default@ if @index@ overflows. Translates to SMT-Lib tables. 636svSelect :: [SVal] -> SVal -> SVal -> SVal 637svSelect xs err ind 638 | SVal _ (Left c) <- ind = 639 case cvVal c of 640 CInteger i -> if i < 0 || i >= genericLength xs 641 then err 642 else xs `genericIndex` i 643 _ -> error $ "SBV.select: unsupported " ++ show (kindOf ind) ++ " valued select/index expression" 644svSelect xsOrig err ind = xs `seq` SVal kElt (Right (cache r)) 645 where 646 kInd = kindOf ind 647 kElt = kindOf err 648 -- Based on the index size, we need to limit the elements. For 649 -- instance if the index is 8 bits, but there are 257 elements, 650 -- that last element will never be used and we can chop it off. 651 xs = case kInd of 652 KBounded False i -> genericTake ((2::Integer) ^ i) xsOrig 653 KBounded True i -> genericTake ((2::Integer) ^ (i-1)) xsOrig 654 KUnbounded -> xsOrig 655 _ -> error $ "SBV.select: unsupported " ++ show kInd ++ " valued select/index expression" 656 r st = do sws <- mapM (svToSV st) xs 657 swe <- svToSV st err 658 if all (== swe) sws -- off-chance that all elts are the same 659 then return swe 660 else do idx <- getTableIndex st kInd kElt sws 661 swi <- svToSV st ind 662 let len = length xs 663 -- NB. No need to worry here that the index 664 -- might be < 0; as the SMTLib translation 665 -- takes care of that automatically 666 newExpr st kElt (SBVApp (LkUp (idx, kInd, kElt, len) swi swe) []) 667 668-- Change the sign of a bit-vector quantity. Fails if passed a non-bv 669svChangeSign :: Bool -> SVal -> SVal 670svChangeSign s x 671 | not (isBounded x) = error $ "Data.SBV." ++ nm ++ ": Received non bit-vector kind: " ++ show (kindOf x) 672 | Just n <- svAsInteger x = svInteger k n 673 | True = SVal k (Right (cache y)) 674 where 675 nm = if s then "svSign" else "svUnsign" 676 677 k = KBounded s (intSizeOf x) 678 y st = do xsw <- svToSV st x 679 newExpr st k (SBVApp (Extract (intSizeOf x - 1) 0) [xsw]) 680 681-- | Convert a symbolic bitvector from unsigned to signed. 682svSign :: SVal -> SVal 683svSign = svChangeSign True 684 685-- | Convert a symbolic bitvector from signed to unsigned. 686svUnsign :: SVal -> SVal 687svUnsign = svChangeSign False 688 689-- | Convert a symbolic bitvector from one integral kind to another. 690svFromIntegral :: Kind -> SVal -> SVal 691svFromIntegral kTo x 692 | Just v <- svAsInteger x 693 = svInteger kTo v 694 | True 695 = result 696 where result = SVal kTo (Right (cache y)) 697 kFrom = kindOf x 698 y st = do xsw <- svToSV st x 699 newExpr st kTo (SBVApp (KindCast kFrom kTo) [xsw]) 700 701-------------------------------------------------------------------------------- 702-- Derived operations 703 704-- | Convert an SVal from kind Bool to an unsigned bitvector of size 1. 705svToWord1 :: SVal -> SVal 706svToWord1 b = svSymbolicMerge k True b (svInteger k 1) (svInteger k 0) 707 where k = KBounded False 1 708 709-- | Convert an SVal from a bitvector of size 1 (signed or unsigned) to kind Bool. 710svFromWord1 :: SVal -> SVal 711svFromWord1 x = svNotEqual x (svInteger k 0) 712 where k = kindOf x 713 714-- | Test the value of a bit. Note that we do an extract here 715-- as opposed to masking and checking against zero, as we found 716-- extraction to be much faster with large bit-vectors. 717svTestBit :: SVal -> Int -> SVal 718svTestBit x i 719 | i < intSizeOf x = svFromWord1 (svExtract i i x) 720 | True = svFalse 721 722-- | Generalization of 'svShl', where the shift-amount is symbolic. 723svShiftLeft :: SVal -> SVal -> SVal 724svShiftLeft = svShift True 725 726-- | Generalization of 'svShr', where the shift-amount is symbolic. 727-- 728-- NB. If the shiftee is signed, then this is an arithmetic shift; 729-- otherwise it's logical. 730svShiftRight :: SVal -> SVal -> SVal 731svShiftRight = svShift False 732 733-- | Generic shifting of bounded quantities. The shift amount must be non-negative and within the bounds of the argument 734-- for bit vectors. For negative shift amounts, the result is returned unchanged. For overshifts, left-shift produces 0, 735-- right shift produces 0 or -1 depending on the result being signed. 736svShift :: Bool -> SVal -> SVal -> SVal 737svShift toLeft x i 738 | Just r <- constFoldValue 739 = r 740 | cannotOverShift 741 = svIte (i `svLessThan` svInteger ki 0) -- Negative shift, no change 742 x 743 regularShiftValue 744 | True 745 = svIte (i `svLessThan` svInteger ki 0) -- Negative shift, no change 746 x 747 $ svIte (i `svGreaterEq` svInteger ki (fromIntegral (intSizeOf x))) -- Overshift, by at least the bit-width of x 748 overShiftValue 749 regularShiftValue 750 751 where nm | toLeft = "shiftLeft" 752 | True = "shiftRight" 753 754 kx = kindOf x 755 ki = kindOf i 756 757 -- Constant fold the result if possible. If either quantity is unbounded, then we only support constants 758 -- as there's no easy/meaningful way to map this combo to SMTLib. Should be rarely needed, if ever! 759 -- We also perform basic sanity check here so that if we go past here, we know we have bitvectors only. 760 constFoldValue 761 | Just iv <- getConst i, iv == 0 762 = Just x 763 764 | Just xv <- getConst x, xv == 0 765 = Just x 766 767 | Just xv <- getConst x, Just iv <- getConst i 768 = Just $ SVal kx . Left $! normCV $ CV kx (CInteger (xv `opC` shiftAmount iv)) 769 770 | isUnbounded x || isUnbounded i 771 = bailOut $ "Not yet implemented unbounded/non-constants shifts for " ++ show (kx, ki) ++ ", please file a request!" 772 773 | not (isBounded x && isBounded i) 774 = bailOut $ "Unexpected kinds: " ++ show (kx, ki) 775 776 | True 777 = Nothing 778 779 where bailOut m = error $ "SBV." ++ nm ++ ": " ++ m 780 781 getConst (SVal _ (Left (CV _ (CInteger val)))) = Just val 782 getConst _ = Nothing 783 784 opC | toLeft = shiftL 785 | True = shiftR 786 787 -- like fromIntegral, but more paranoid 788 shiftAmount :: Integer -> Int 789 shiftAmount iv 790 | iv <= 0 = 0 791 | isUnbounded i, iv > fromIntegral (maxBound :: Int) = bailOut $ "Unsupported constant unbounded shift with amount: " ++ show iv 792 | isUnbounded x = fromIntegral iv 793 | iv >= fromIntegral ub = ub 794 | not (isBounded x && isBounded i) = bailOut $ "Unsupported kinds: " ++ show (kx, ki) 795 | True = fromIntegral iv 796 where ub = intSizeOf x 797 798 -- Overshift is not possible if the bit-size of x won't even fit into the bit-vector size 799 -- of i. Note that this is a *necessary* check, Consider for instance if we're shifting a 800 -- 32-bit value using a 1-bit shift amount (which can happen if the value is 1 with minimal 801 -- shift widths). We would compare 1 >= 32, but stuffing 32 into bit-vector of size 1 would 802 -- overflow. See http://github.com/LeventErkok/sbv/issues/323 for this case. Thus, we 803 -- make sure that the bit-vector would fit as a value. 804 cannotOverShift = maxRepresentable <= fromIntegral (intSizeOf x) 805 where maxRepresentable :: Integer 806 maxRepresentable 807 | hasSign i = bit (intSizeOf i - 1) - 1 808 | True = bit (intSizeOf i ) - 1 809 810 -- An overshift occurs if we're shifting by more than or equal to the bit-width of x 811 -- For shift-left: this value is always 0 812 -- For shift-right: 813 -- If x is unsigned: 0 814 -- If x is signed and is less than 0, then -1 else 0 815 overShiftValue | toLeft = zx 816 | hasSign x = svIte (x `svLessThan` zx) neg1 zx 817 | True = zx 818 where zx = svInteger kx 0 819 neg1 = svInteger kx (-1) 820 821 -- Regular shift, we know that the shift value fits into the bit-width of x, since it's between 0 and sizeOf x. So, we can just 822 -- turn it into a properly sized argument and ship it to SMTLib 823 regularShiftValue = SVal kx $ Right $ cache result 824 where result st = do sw1 <- svToSV st x 825 sw2 <- svToSV st i 826 827 let op | toLeft = Shl 828 | True = Shr 829 830 adjustedShift <- if kx == ki 831 then return sw2 832 else newExpr st kx (SBVApp (KindCast ki kx) [sw2]) 833 834 newExpr st kx (SBVApp op [sw1, adjustedShift]) 835 836-- | Generalization of 'svRol', where the rotation amount is symbolic. 837-- If the first argument is not bounded, then the this is the same as shift. 838svRotateLeft :: SVal -> SVal -> SVal 839svRotateLeft x i 840 | not (isBounded x) 841 = svShiftLeft x i 842 | isBounded i && bit si <= toInteger sx -- wrap-around not possible 843 = svIte (svLessThan i zi) 844 (svSelect [x `svRor` k | k <- [0 .. bit si - 1]] z (svUNeg i)) 845 (svSelect [x `svRol` k | k <- [0 .. bit si - 1]] z i) 846 | True 847 = svIte (svLessThan i zi) 848 (svSelect [x `svRor` k | k <- [0 .. sx - 1]] z (svUNeg i `svRem` n)) 849 (svSelect [x `svRol` k | k <- [0 .. sx - 1]] z ( i `svRem` n)) 850 where sx = intSizeOf x 851 si = intSizeOf i 852 z = svInteger (kindOf x) 0 853 zi = svInteger (kindOf i) 0 854 n = svInteger (kindOf i) (toInteger sx) 855 856-- | A variant of 'svRotateLeft' that uses a barrel-rotate design, which can lead to 857-- better verification code. Only works when both arguments are finite and the second 858-- argument is unsigned. 859svBarrelRotateLeft :: SVal -> SVal -> SVal 860svBarrelRotateLeft x i 861 | not (isBounded x && isBounded i && not (hasSign i)) 862 = error $ "Data.SBV.Dynamic.svBarrelRotateLeft: Arguments must be bounded with second argument unsigned. Received: " ++ show (x, i) 863 | Just iv <- svAsInteger i 864 = svRol x $ fromIntegral (iv `rem` fromIntegral (intSizeOf x)) 865 | True 866 = barrelRotate svRol x i 867 868-- | A variant of 'svRotateLeft' that uses a barrel-rotate design, which can lead to 869-- better verification code. Only works when both arguments are finite and the second 870-- argument is unsigned. 871svBarrelRotateRight :: SVal -> SVal -> SVal 872svBarrelRotateRight x i 873 | not (isBounded x && isBounded i && not (hasSign i)) 874 = error $ "Data.SBV.Dynamic.svBarrelRotateRight: Arguments must be bounded with second argument unsigned. Received: " ++ show (x, i) 875 | Just iv <- svAsInteger i 876 = svRor x $ fromIntegral (iv `rem` fromIntegral (intSizeOf x)) 877 | True 878 = barrelRotate svRor x i 879 880-- Barrel rotation, by bit-blasting the argument: 881barrelRotate :: (SVal -> Int -> SVal) -> SVal -> SVal -> SVal 882barrelRotate f a c = loop blasted a 883 where loop :: [(SVal, Integer)] -> SVal -> SVal 884 loop [] acc = acc 885 loop ((b, v) : rest) acc = loop rest (svIte b (f acc (fromInteger v)) acc) 886 887 sa = toInteger $ intSizeOf a 888 n = svInteger (kindOf c) sa 889 890 -- Reduce by the modulus amount, we need not care about the 891 -- any part larger than the value of the bit-size of the 892 -- argument as it is identity for rotations 893 reducedC = c `svRem` n 894 895 -- blast little-endian, and zip with bit-position 896 blasted = takeWhile significant $ zip (svBlastLE reducedC) [2^i | i <- [(0::Integer)..]] 897 898 -- Any term whose bit-position is larger than our input size 899 -- is insignificant, since the reduction would've put 0's in those 900 -- bits. For instance, if a is 32 bits, and c is 5 bits, then we 901 -- need not look at any position i s.t. 2^i > 32 902 significant (_, pos) = pos < sa 903 904-- | Generalization of 'svRor', where the rotation amount is symbolic. 905-- If the first argument is not bounded, then the this is the same as shift. 906svRotateRight :: SVal -> SVal -> SVal 907svRotateRight x i 908 | not (isBounded x) 909 = svShiftRight x i 910 | isBounded i && bit si <= toInteger sx -- wrap-around not possible 911 = svIte (svLessThan i zi) 912 (svSelect [x `svRol` k | k <- [0 .. bit si - 1]] z (svUNeg i)) 913 (svSelect [x `svRor` k | k <- [0 .. bit si - 1]] z i) 914 | True 915 = svIte (svLessThan i zi) 916 (svSelect [x `svRol` k | k <- [0 .. sx - 1]] z (svUNeg i `svRem` n)) 917 (svSelect [x `svRor` k | k <- [0 .. sx - 1]] z ( i `svRem` n)) 918 where sx = intSizeOf x 919 si = intSizeOf i 920 z = svInteger (kindOf x) 0 921 zi = svInteger (kindOf i) 0 922 n = svInteger (kindOf i) (toInteger sx) 923 924-------------------------------------------------------------------------------- 925-- | Overflow detection. 926svMkOverflow :: OvOp -> SVal -> SVal -> SVal 927svMkOverflow o x y = SVal KBool (Right (cache r)) 928 where r st = do sx <- svToSV st x 929 sy <- svToSV st y 930 newExpr st KBool $ SBVApp (OverflowOp o) [sx, sy] 931 932--------------------------------------------------------------------------------- 933-- * Symbolic Arrays 934--------------------------------------------------------------------------------- 935 936-- | Arrays in terms of SMT-Lib arrays 937data SArr = SArr (Kind, Kind) (Cached ArrayIndex) 938 939-- | Read the array element at @a@ 940readSArr :: SArr -> SVal -> SVal 941readSArr (SArr (_, bk) f) a = SVal bk $ Right $ cache r 942 where r st = do arr <- uncacheAI f st 943 i <- svToSV st a 944 newExpr st bk (SBVApp (ArrRead arr) [i]) 945 946-- | Update the element at @a@ to be @b@ 947writeSArr :: SArr -> SVal -> SVal -> SArr 948writeSArr (SArr ainfo f) a b = SArr ainfo $ cache g 949 where g st = do arr <- uncacheAI f st 950 addr <- svToSV st a 951 val <- svToSV st b 952 amap <- R.readIORef (rArrayMap st) 953 954 let j = ArrayIndex $ IMap.size amap 955 upd = IMap.insert (unArrayIndex j) ("array_" ++ show j, ainfo, ArrayMutate arr addr val) 956 957 j `seq` modifyState st rArrayMap upd $ modifyIncState st rNewArrs upd 958 return j 959 960-- | Merge two given arrays on the symbolic condition 961-- Intuitively: @mergeArrays cond a b = if cond then a else b@. 962-- Merging pushes the if-then-else choice down on to elements 963mergeSArr :: SVal -> SArr -> SArr -> SArr 964mergeSArr t (SArr ainfo a) (SArr _ b) = SArr ainfo $ cache h 965 where h st = do ai <- uncacheAI a st 966 bi <- uncacheAI b st 967 ts <- svToSV st t 968 amap <- R.readIORef (rArrayMap st) 969 970 let k = ArrayIndex $ IMap.size amap 971 upd = IMap.insert (unArrayIndex k) ("array_" ++ show k, ainfo, ArrayMerge ts ai bi) 972 973 k `seq` modifyState st rArrayMap upd $ modifyIncState st rNewArrs upd 974 return k 975 976-- | Create a named new array 977newSArr :: State -> (Kind, Kind) -> (Int -> String) -> Maybe SVal -> IO SArr 978newSArr st ainfo mkNm mbDef = do 979 amap <- R.readIORef $ rArrayMap st 980 981 mbSWDef <- case mbDef of 982 Nothing -> return Nothing 983 Just sv -> Just <$> svToSV st sv 984 985 let i = ArrayIndex $ IMap.size amap 986 nm = mkNm (unArrayIndex i) 987 upd = IMap.insert (unArrayIndex i) (nm, ainfo, ArrayFree mbSWDef) 988 989 registerLabel "SArray declaration" st nm 990 991 modifyState st rArrayMap upd $ modifyIncState st rNewArrs upd 992 return $ SArr ainfo $ cache $ const $ return i 993 994-- | Compare two arrays for equality 995eqSArr :: SArr -> SArr -> SVal 996eqSArr (SArr _ a) (SArr _ b) = SVal KBool $ Right $ cache c 997 where c st = do ai <- uncacheAI a st 998 bi <- uncacheAI b st 999 newExpr st KBool (SBVApp (ArrEq ai bi) []) 1000 1001-- | Arrays managed internally 1002data SFunArr = SFunArr (Kind, Kind) (Cached FArrayIndex) 1003 1004-- | Convert a node-id to an SVal 1005nodeIdToSVal :: Kind -> Int -> SVal 1006nodeIdToSVal k i = swToSVal $ SV k (NodeId i) 1007 1008-- | Convert an 'SV' to an 'SVal' 1009swToSVal :: SV -> SVal 1010swToSVal sv@(SV k _) = SVal k $ Right $ cache $ const $ return sv 1011 1012-- | A variant of SVal equality, but taking into account of constants 1013-- NB. The rationalCheck is paranoid perhaps, but is necessary in case 1014-- we have some funky polynomial roots in there. We do allow for 1015-- floating-points here though. Why? Because the Eq instance of 'CV' 1016-- does the right thing by using object equality. (i.e., it does 1017-- the right thing for NaN/+0/-0 etc.) A straightforward equality 1018-- here would be wrong for floats! 1019svEqualWithConsts :: (SVal, Maybe CV) -> (SVal, Maybe CV) -> SVal 1020svEqualWithConsts sv1 sv2 = case (grabCV sv1, grabCV sv2) of 1021 (Just cv, Just cv') | rationalCheck cv cv' -> if cv == cv' then svTrue else svFalse 1022 _ -> fst sv1 `svEqual` fst sv2 1023 where grabCV (_, Just cv) = Just cv 1024 grabCV (SVal _ (Left cv), _ ) = Just cv 1025 grabCV _ = Nothing 1026 1027-- | Read the array element at @a@. For efficiency purposes, we create a memo-table 1028-- as we go along, as otherwise we suffer significant performance penalties. See: 1029-- <http://github.com/LeventErkok/sbv/issues/402> and 1030-- <http://github.com/LeventErkok/sbv/issues/396>. 1031readSFunArr :: SFunArr -> SVal -> SVal 1032readSFunArr (SFunArr (ak, bk) f) address 1033 | kindOf address /= ak 1034 = error $ "Data.SBV.readSFunArr: Impossible happened, accesing with address type: " ++ show (kindOf address) ++ ", expected: " ++ show ak 1035 | True 1036 = SVal bk $ Right $ cache r 1037 where r st = do fArrayIndex <- uncacheFAI f st 1038 fArrMap <- R.readIORef (rFArrayMap st) 1039 1040 constMap <- R.readIORef (rconstMap st) 1041 let consts = Map.fromList [(i, cv) | (cv, SV _ (NodeId i)) <- Map.toList constMap] 1042 1043 case unFArrayIndex fArrayIndex `IMap.lookup` fArrMap of 1044 Nothing -> error $ "Data.SBV.readSFunArr: Impossible happened while trying to access SFunArray, can't find index: " ++ show fArrayIndex 1045 Just (uninitializedRead, rCache) -> do 1046 memoTable <- R.readIORef rCache 1047 SV _ (NodeId addressNodeId) <- svToSV st address 1048 1049 -- If we hit the cache, return the result right away. If we miss, we need to 1050 -- walk through each element to "merge" all possible reads as we do not know 1051 -- whether the symbolic access may end up the same as one of the earlier ones 1052 -- in the cache. 1053 case addressNodeId `IMap.lookup` memoTable of 1054 Just v -> return v -- cache hit! 1055 1056 Nothing -> -- cache miss; walk down the cache items to form the chain of reads: 1057 do let aInfo = (address, addressNodeId `Map.lookup` consts) 1058 1059 find :: [(Int, SV)] -> SVal 1060 find [] = uninitializedRead address 1061 find ((i, v) : ivs) = svIte (svEqualWithConsts (nodeIdToSVal ak i, i `Map.lookup` consts) aInfo) (swToSVal v) (find ivs) 1062 1063 finalValue = find (IMap.toAscList memoTable) 1064 1065 finalSW <- svToSV st finalValue 1066 1067 -- Cache the result, so next time we can retrieve it faster if we look it up with the same address! 1068 -- The following line is really the whole point of having caching in SFunArray! 1069 R.modifyIORef' rCache (IMap.insert addressNodeId finalSW) 1070 1071 return finalSW 1072 1073-- | Update the element at @address@ to be @b@ 1074writeSFunArr :: SFunArr -> SVal -> SVal -> SFunArr 1075writeSFunArr (SFunArr (ak, bk) f) address b 1076 | kindOf address /= ak 1077 = error $ "Data.SBV.writeSFunArr: Impossible happened, accesing with address type: " ++ show (kindOf address) ++ ", expected: " ++ show ak 1078 | kindOf b /= bk 1079 = error $ "Data.SBV.writeSFunArr: Impossible happened, accesing with address type: " ++ show (kindOf b) ++ ", expected: " ++ show bk 1080 | True 1081 = SFunArr (ak, bk) $ cache g 1082 where g st = do fArrayIndex <- uncacheFAI f st 1083 fArrMap <- R.readIORef (rFArrayMap st) 1084 constMap <- R.readIORef (rconstMap st) 1085 1086 let consts = Map.fromList [(i, cv) | (cv, SV _ (NodeId i)) <- Map.toList constMap] 1087 1088 case unFArrayIndex fArrayIndex `IMap.lookup` fArrMap of 1089 Nothing -> error $ "Data.SBV.writeSFunArr: Impossible happened while trying to access SFunArray, can't find index: " ++ show fArrayIndex 1090 1091 Just (aUi, rCache) -> do 1092 memoTable <- R.readIORef rCache 1093 SV _ (NodeId addressNodeId) <- svToSV st address 1094 val <- svToSV st b 1095 1096 -- There are two cases: 1097 -- 1098 -- (1) We hit the cache, and old value is the same as new: No write necessary, just return the array 1099 -- (2) We hit the cache, values are different OR we miss the cache. We need to insert this value into 1100 -- the cache, overriding the original if it was there. Note that we also have to walk the cache 1101 -- to update each element, as this write can symbolically be the same as some other addresses. 1102 -- 1103 -- Below, we determine which case we're in and then insert the value at the end and continue 1104 cont <- case addressNodeId `IMap.lookup` memoTable of 1105 Just oldVal -- Cache hit 1106 | val == oldVal -> return $ Left fArrayIndex -- Case 1 1107 1108 _ -> do -- Cache miss, or value is different. 1109 1110 let aInfo = (address, addressNodeId `Map.lookup` consts) 1111 1112 -- NB. The order of modifications here is important as we 1113 -- keep the keys in ascending order. (Since we'll call fromAscList later on.) 1114 walk :: [(Int, SV)] -> [(Int, SV)] -> IO [(Int, SV)] 1115 walk [] sofar = return $ reverse sofar 1116 walk ((i, s):iss) sofar = modify i s >>= \s' -> walk iss ((i, s') : sofar) 1117 1118 -- At the cached address i, currently storing value s. Conditionally update it to `b` (new value) 1119 -- if the addresses match. Otherwise keep it the same. 1120 modify :: Int -> SV -> IO SV 1121 modify i s = svToSV st $ svIte (svEqualWithConsts (nodeIdToSVal ak i, i `Map.lookup` consts) aInfo) b (swToSVal s) 1122 1123 Right . IMap.fromAscList <$> walk (IMap.toAscList (IMap.delete addressNodeId memoTable)) [] 1124 1125 case cont of 1126 Left j -> return j -- There was a hit, and value was unchanged, nothing to do 1127 1128 Right mt -> do -- There was a hit, and the value was different; or there was a miss. Insert the new value 1129 -- and create a new array. Note that we keep the aUi the same: Just because we modified 1130 -- an array, it doesn't mean we change the uninitialized reads: they still come from the same place. 1131 -- 1132 newMemoTable <- R.newIORef $ IMap.insert addressNodeId val mt 1133 1134 let j = FArrayIndex $ IMap.size fArrMap 1135 upd = IMap.insert (unFArrayIndex j) (aUi, newMemoTable) 1136 1137 j `seq` modifyState st rFArrayMap upd (return ()) 1138 return j 1139 1140-- | Merge two given arrays on the symbolic condition 1141-- Intuitively: @mergeArrays cond a b = if cond then a else b@. 1142-- Merging pushes the if-then-else choice down on to elements 1143mergeSFunArr :: SVal -> SFunArr -> SFunArr -> SFunArr 1144mergeSFunArr t array1@(SFunArr ainfo@(sourceKind, targetKind) a) array2@(SFunArr binfo b) 1145 | ainfo /= binfo 1146 = error $ "Data.SBV.mergeSFunArr: Impossible happened, merging incompatbile arrays: " ++ show (ainfo, binfo) 1147 | Just test <- svAsBool t 1148 = if test then array1 else array2 1149 | True 1150 = SFunArr ainfo $ cache c 1151 where c st = do ai <- uncacheFAI a st 1152 bi <- uncacheFAI b st 1153 1154 constMap <- R.readIORef (rconstMap st) 1155 let consts = Map.fromList [(i, cv) | (cv, SV _ (NodeId i)) <- Map.toList constMap] 1156 1157 -- Catch the degenerate case of merging an array with itself. One 1158 -- can argue this is pointless, but actually it comes up when one 1159 -- is merging composite structures (through a Mergeable class instance) 1160 -- that has an array component that didn't change. So, pays off in practice! 1161 if unFArrayIndex ai == unFArrayIndex bi 1162 then return ai -- merging with itself, noop 1163 else do fArrMap <- R.readIORef (rFArrayMap st) 1164 1165 case (unFArrayIndex ai `IMap.lookup` fArrMap, unFArrayIndex bi `IMap.lookup` fArrMap) of 1166 (Nothing, _) -> error $ "Data.SBV.mergeSFunArr: Impossible happened while trying to access SFunArray, can't find index: " ++ show ai 1167 (_, Nothing) -> error $ "Data.SBV.mergeSFunArr: Impossible happened while trying to access SFunArray, can't find index: " ++ show bi 1168 (Just (aUi, raCache), Just (bUi, rbCache)) -> do 1169 1170 -- This is where the complication happens. We need to merge the caches. If the same 1171 -- key appears in both, then that's the easy case: Just merge the entries. But if 1172 -- a key only appears in one but not the other? Just like in the read/write cases, 1173 -- we have to consider the possibility that the missing key can be any one of the 1174 -- other elements in the cache. So, for each non-matching key in either memo-table, 1175 -- we traverse the other and create a chain of look-up values. 1176 aMemo <- R.readIORef raCache 1177 bMemo <- R.readIORef rbCache 1178 1179 let aMemoT = IMap.toAscList aMemo 1180 bMemoT = IMap.toAscList bMemo 1181 1182 -- gen takes a uninitialized-read creator, a key, and the choices from the "other" 1183 -- cache that this key may map to. And creates a new SV that corresponds to the 1184 -- merged value: 1185 gen :: (SVal -> SVal) -> Int -> [(Int, SV)] -> IO SV 1186 gen mk k choices = svToSV st $ walk choices 1187 where kInfo = (nodeIdToSVal sourceKind k, k `Map.lookup` consts) 1188 1189 walk :: [(Int, SV)] -> SVal 1190 walk [] = mk (fst kInfo) 1191 walk ((i, v) : ivs) = svIte (svEqualWithConsts (nodeIdToSVal sourceKind i, i `Map.lookup` consts) kInfo) 1192 (swToSVal v) 1193 (walk ivs) 1194 1195 -- Insert into an existing map the new key value by merging according to the test 1196 fill :: Int -> SV -> SV -> IMap.IntMap SV -> IO (IMap.IntMap SV) 1197 fill k (SV _ (NodeId ni1)) (SV _ (NodeId ni2)) m = do v <- svToSV st (svIte t sval1 sval2) 1198 return $ IMap.insert k v m 1199 where sval1 = nodeIdToSVal targetKind ni1 1200 sval2 = nodeIdToSVal targetKind ni2 1201 1202 -- Walk down the memo-tables in tandem. If we find a common key: Simply fill it in. If we find 1203 -- a key only in one, generate the corresponding read from the other cache, and do the fill. 1204 merge [] [] sofar = return sofar 1205 merge ((k1, v1) : as) [] sofar = gen bUi k1 bMemoT >>= \v2 -> fill k1 v1 v2 sofar >>= merge as [] 1206 merge [] ((k2, v2) : bs) sofar = gen aUi k2 aMemoT >>= \v1 -> fill k2 v1 v2 sofar >>= merge [] bs 1207 merge ass@((k1, v1) : as) bss@((k2, v2) : bs) sofar 1208 | k1 < k2 = gen bUi k1 bMemoT >>= \nv2 -> fill k1 v1 nv2 sofar >>= merge as bss 1209 | k1 > k2 = gen aUi k2 aMemoT >>= \nv1 -> fill k2 nv1 v2 sofar >>= merge ass bs 1210 | True = fill k1 v1 v2 sofar >>= merge as bs 1211 1212 mergedMap <- merge aMemoT bMemoT IMap.empty 1213 memoMerged <- R.newIORef mergedMap 1214 1215 -- Craft a new uninitializer. Note that we do *not* create a new initializer here, 1216 -- but simply merge the two initializers which will inherit their original unread 1217 -- references should the test be a constant. 1218 let mkUninitialized i = svIte t (aUi i) (bUi i) 1219 1220 -- Add it to our collection: 1221 let j = FArrayIndex $ IMap.size fArrMap 1222 upd = IMap.insert (unFArrayIndex j) (mkUninitialized, memoMerged) 1223 1224 j `seq` modifyState st rFArrayMap upd (return ()) 1225 1226 return j 1227 1228-- | Create a named new array 1229newSFunArr :: State -> (Kind, Kind) -> (Int -> String) -> Maybe SVal -> IO SFunArr 1230newSFunArr st (ak, bk) mkNm mbDef = do 1231 fArrMap <- R.readIORef (rFArrayMap st) 1232 memoTable <- R.newIORef IMap.empty 1233 1234 let j = FArrayIndex $ IMap.size fArrMap 1235 nm = mkNm (unFArrayIndex j) 1236 mkUninitialized i = case mbDef of 1237 Just def -> def 1238 _ -> svUninterpreted bk (nm ++ "_uninitializedRead") Nothing [i] 1239 1240 upd = IMap.insert (unFArrayIndex j) (mkUninitialized, memoTable) 1241 1242 registerLabel "SFunArray declaration" st nm 1243 j `seq` modifyState st rFArrayMap upd (return ()) 1244 1245 return $ SFunArr (ak, bk) $ cache $ const $ return j 1246 1247-------------------------------------------------------------------------------- 1248-- Utility functions 1249 1250noUnint :: (Maybe Int, String) -> a 1251noUnint x = error $ "Unexpected operation called on uninterpreted/enumerated value: " ++ show x 1252 1253noUnint2 :: (Maybe Int, String) -> (Maybe Int, String) -> a 1254noUnint2 x y = error $ "Unexpected binary operation called on uninterpreted/enumerated values: " ++ show (x, y) 1255 1256noCharLift :: Char -> a 1257noCharLift x = error $ "Unexpected operation called on char: " ++ show x 1258 1259noStringLift :: String -> a 1260noStringLift x = error $ "Unexpected operation called on string: " ++ show x 1261 1262noCharLift2 :: Char -> Char -> a 1263noCharLift2 x y = error $ "Unexpected binary operation called on chars: " ++ show (x, y) 1264 1265noStringLift2 :: String -> String -> a 1266noStringLift2 x y = error $ "Unexpected binary operation called on strings: " ++ show (x, y) 1267 1268liftSym1 :: (State -> Kind -> SV -> IO SV) -> (AlgReal -> AlgReal) -> (Integer -> Integer) -> (Float -> Float) -> (Double -> Double) -> (FP -> FP) -> SVal -> SVal 1269liftSym1 _ opCR opCI opCF opCD opFP (SVal k (Left a)) = SVal k . Left $! mapCV opCR opCI opCF opCD opFP noCharLift noStringLift noUnint a 1270liftSym1 opS _ _ _ _ _ a@(SVal k _) = SVal k $ Right $ cache c 1271 where c st = do sva <- svToSV st a 1272 opS st k sva 1273 1274{- A note on constant folding. 1275 1276There are cases where we miss out on certain constant foldings. On May 8 2018, Matt Peddie pointed this 1277out, as the C code he was getting had redundancies. I was aware that could be missing constant foldings 1278due to missed out optimizations, or some other code snafu, but till Matt pointed it out I haven't realized 1279that we could be hiding constants inside an if-then-else. The example is: 1280 1281 proveWith z3{verbose=True} $ \x -> 0 .< ite (x .== (x::SWord8)) 1 (2::SWord8) 1282 1283If you try this, you'll see that it generates (shortened): 1284 1285 (define-fun s1 () (_ BitVec 8) #x00) 1286 (define-fun s2 () (_ BitVec 8) #x01) 1287 (define-fun s3 () Bool (bvult s1 s2)) 1288 1289But clearly we have all the info for s3 to be computed! The issue here is that the reduction of @x .== x@ to @true@ 1290happens after we start computing the if-then-else, hence we are already committed to an SV at that point. The call 1291to ite eventually recognizes this, but at that point it picks up the now constants from SV's, missing the constant 1292folding opportunity. 1293 1294We can fix this, by looking up the constants table in liftSV2, along the lines of: 1295 1296 1297 liftSV2 :: (CV -> CV -> Bool) -> (CV -> CV -> CV) -> (State -> Kind -> SV -> SV -> IO SV) -> Kind -> SVal -> SVal -> Cached SV 1298 liftSV2 okCV opCV opS k a b = cache c 1299 where c st = do sw1 <- svToSV st a 1300 sw2 <- svToSV st b 1301 cmap <- readIORef (rconstMap st) 1302 let cv1 = [cv | ((_, cv), sv) <- M.toList cmap, sv == sv1] 1303 cv2 = [cv | ((_, cv), sv) <- M.toList cmap, sv == sv2] 1304 case (cv1, cv2) of 1305 ([x], [y]) | okCV x y -> newConst st $ opCV x y 1306 _ -> opS st k sv1 sv2 1307 1308(with obvious modifications to call sites to get the proper arguments.) 1309 1310But this means that we have to grab the constant list for every symbolically lifted operation, also do the 1311same for other places, etc.; for the rare opportunity of catching a @x .== x@ optimization. Even then, the 1312constants for the branches would still be generated. (i.e., in the above example we would still generate 1313@s1@ and @s2@, but would skip @s3@.) 1314 1315It seems to me that the price to pay is rather high, as this is hardly the most common case; so we're opting 1316here to ignore these cases. 1317 1318See http://github.com/LeventErkok/sbv/issues/379 for some further discussion. 1319-} 1320liftSV2 :: (State -> Kind -> SV -> SV -> IO SV) -> Kind -> SVal -> SVal -> Cached SV 1321liftSV2 opS k a b = cache c 1322 where c st = do sw1 <- svToSV st a 1323 sw2 <- svToSV st b 1324 opS st k sw1 sw2 1325 1326liftSym2 :: (State -> Kind -> SV -> SV -> IO SV) 1327 -> [CV -> CV -> Bool] 1328 -> (AlgReal -> AlgReal -> AlgReal) 1329 -> (Integer -> Integer -> Integer) 1330 -> (Float -> Float -> Float) 1331 -> (Double -> Double -> Double) 1332 -> (FP -> FP -> FP) 1333 -> SVal -> SVal -> SVal 1334liftSym2 _ okCV opCR opCI opCF opCD opFP (SVal k (Left a)) (SVal _ (Left b)) | and [f a b | f <- okCV] = SVal k . Left $! mapCV2 opCR opCI opCF opCD opFP noCharLift2 noStringLift2 noUnint2 a b 1335liftSym2 opS _ _ _ _ _ _ a@(SVal k _) b = SVal k $ Right $ liftSV2 opS k a b 1336 1337liftSym2B :: (State -> Kind -> SV -> SV -> IO SV) 1338 -> (CV -> CV -> Bool) 1339 -> (AlgReal -> AlgReal -> Bool) 1340 -> (Integer -> Integer -> Bool) 1341 -> (Float -> Float -> Bool) 1342 -> (Double -> Double -> Bool) 1343 -> (FP -> FP -> Bool) 1344 -> (Char -> Char -> Bool) 1345 -> (String -> String -> Bool) 1346 -> ([CVal] -> [CVal] -> Bool) 1347 -> ([CVal] -> [CVal] -> Bool) 1348 -> (Maybe CVal -> Maybe CVal -> Bool) 1349 -> (Either CVal CVal -> Either CVal CVal -> Bool) 1350 -> ((Maybe Int, String) -> (Maybe Int, String) -> Bool) 1351 -> SVal -> SVal -> SVal 1352liftSym2B _ okCV opCR opCI opCF opCD opAF opCC opCS opCSeq opCTup opCMaybe opCEither opUI (SVal _ (Left a)) (SVal _ (Left b)) | okCV a b = svBool (liftCV2 opCR opCI opCF opCD opAF opCC opCS opCSeq opCTup opCMaybe opCEither opUI a b) 1353liftSym2B opS _ _ _ _ _ _ _ _ _ _ _ _ _ a b = SVal KBool $ Right $ liftSV2 opS KBool a b 1354 1355-- | Create a symbolic two argument operation; with shortcut optimizations 1356mkSymOpSC :: (SV -> SV -> Maybe SV) -> Op -> State -> Kind -> SV -> SV -> IO SV 1357mkSymOpSC shortCut op st k a b = maybe (newExpr st k (SBVApp op [a, b])) return (shortCut a b) 1358 1359-- | Create a symbolic two argument operation; no shortcut optimizations 1360mkSymOp :: Op -> State -> Kind -> SV -> SV -> IO SV 1361mkSymOp = mkSymOpSC (const (const Nothing)) 1362 1363mkSymOp1SC :: (SV -> Maybe SV) -> Op -> State -> Kind -> SV -> IO SV 1364mkSymOp1SC shortCut op st k a = maybe (newExpr st k (SBVApp op [a])) return (shortCut a) 1365 1366mkSymOp1 :: Op -> State -> Kind -> SV -> IO SV 1367mkSymOp1 = mkSymOp1SC (const Nothing) 1368 1369-- | eqOpt says the references are to the same SV, thus we can optimize. Note that 1370-- we explicitly disallow KFloat/KDouble/KFloat here. Why? Because it's *NOT* true that 1371-- NaN == NaN, NaN >= NaN, and so-forth. So, we have to make sure we don't optimize 1372-- floats and doubles, in case the argument turns out to be NaN. 1373eqOpt :: SV -> SV -> SV -> Maybe SV 1374eqOpt w x y = case swKind x of 1375 KFloat -> Nothing 1376 KDouble -> Nothing 1377 KFP{} -> Nothing 1378 _ -> if x == y then Just w else Nothing 1379 1380-- For uninterpreted/enumerated values, we carefully lift through the constructor index for comparisons: 1381uiLift :: String -> (Int -> Int -> Bool) -> (Maybe Int, String) -> (Maybe Int, String) -> Bool 1382uiLift _ cmp (Just i, _) (Just j, _) = i `cmp` j 1383uiLift w _ a b = error $ "Data.SBV.Core.Operations: Impossible happened while trying to lift " ++ w ++ " over " ++ show (a, b) 1384 1385-- | Predicate to check if a value is concrete 1386isConcrete :: SVal -> Bool 1387isConcrete (SVal _ Left{}) = True 1388isConcrete _ = False 1389 1390-- | Predicate for optimizing word operations like (+) and (*). 1391-- NB. We specifically do *not* match for Double/Float; because 1392-- FP-arithmetic doesn't obey traditional rules. For instance, 1393-- 0 * x = 0 fails if x happens to be NaN or +/- Infinity. So, 1394-- we merely return False when given a floating-point value here. 1395isConcreteZero :: SVal -> Bool 1396isConcreteZero (SVal _ (Left (CV _ (CInteger n)))) = n == 0 1397isConcreteZero (SVal KReal (Left (CV KReal (CAlgReal v)))) = isExactRational v && v == 0 1398isConcreteZero _ = False 1399 1400-- | Predicate for optimizing word operations like (+) and (*). 1401-- NB. See comment on 'isConcreteZero' for why we don't match 1402-- for Float/Double values here. 1403isConcreteOne :: SVal -> Bool 1404isConcreteOne (SVal _ (Left (CV _ (CInteger 1)))) = True 1405isConcreteOne (SVal KReal (Left (CV KReal (CAlgReal v)))) = isExactRational v && v == 1 1406isConcreteOne _ = False 1407 1408-- | Predicate for optimizing bitwise operations. The unbounded integer case of checking 1409-- against -1 might look dubious, but that's how Haskell treats 'Integer' as a member 1410-- of the Bits class, try @(-1 :: Integer) `testBit` i@ for any @i@ and you'll get 'True'. 1411isConcreteOnes :: SVal -> Bool 1412isConcreteOnes (SVal _ (Left (CV (KBounded b w) (CInteger n)))) = n == if b then -1 else bit w - 1 1413isConcreteOnes (SVal _ (Left (CV KUnbounded (CInteger n)))) = n == -1 -- see comment above 1414isConcreteOnes (SVal _ (Left (CV KBool (CInteger n)))) = n == 1 1415isConcreteOnes _ = False 1416 1417-- | Predicate for optimizing comparisons. 1418isConcreteMax :: SVal -> Bool 1419isConcreteMax (SVal _ (Left (CV (KBounded False w) (CInteger n)))) = n == bit w - 1 1420isConcreteMax (SVal _ (Left (CV (KBounded True w) (CInteger n)))) = n == bit (w - 1) - 1 1421isConcreteMax (SVal _ (Left (CV KBool (CInteger n)))) = n == 1 1422isConcreteMax _ = False 1423 1424-- | Predicate for optimizing comparisons. 1425isConcreteMin :: SVal -> Bool 1426isConcreteMin (SVal _ (Left (CV (KBounded False _) (CInteger n)))) = n == 0 1427isConcreteMin (SVal _ (Left (CV (KBounded True w) (CInteger n)))) = n == - bit (w - 1) 1428isConcreteMin (SVal _ (Left (CV KBool (CInteger n)))) = n == 0 1429isConcreteMin _ = False 1430 1431-- | Most operations on concrete rationals require a compatibility check to avoid faulting 1432-- on algebraic reals. 1433rationalCheck :: CV -> CV -> Bool 1434rationalCheck a b = case (cvVal a, cvVal b) of 1435 (CAlgReal x, CAlgReal y) -> isExactRational x && isExactRational y 1436 _ -> True 1437 1438-- | Quot/Rem operations require a nonzero check on the divisor. 1439nonzeroCheck :: CV -> CV -> Bool 1440nonzeroCheck _ b = cvVal b /= CInteger 0 1441 1442-- | Same as rationalCheck, except for SBV's 1443rationalSBVCheck :: SVal -> SVal -> Bool 1444rationalSBVCheck (SVal KReal (Left a)) (SVal KReal (Left b)) = rationalCheck a b 1445rationalSBVCheck _ _ = True 1446 1447noReal :: String -> AlgReal -> AlgReal -> AlgReal 1448noReal o a b = error $ "SBV.AlgReal." ++ o ++ ": Unexpected arguments: " ++ show (a, b) 1449 1450noFloat :: String -> Float -> Float -> Float 1451noFloat o a b = error $ "SBV.Float." ++ o ++ ": Unexpected arguments: " ++ show (a, b) 1452 1453noDouble :: String -> Double -> Double -> Double 1454noDouble o a b = error $ "SBV.Double." ++ o ++ ": Unexpected arguments: " ++ show (a, b) 1455 1456noFP :: String -> FP -> FP -> FP 1457noFP o a b = error $ "SBV.FPR." ++ o ++ ": Unexpected arguments: " ++ show (a, b) 1458 1459noRealUnary :: String -> AlgReal -> AlgReal 1460noRealUnary o a = error $ "SBV.AlgReal." ++ o ++ ": Unexpected argument: " ++ show a 1461 1462noFloatUnary :: String -> Float -> Float 1463noFloatUnary o a = error $ "SBV.Float." ++ o ++ ": Unexpected argument: " ++ show a 1464 1465noDoubleUnary :: String -> Double -> Double 1466noDoubleUnary o a = error $ "SBV.Double." ++ o ++ ": Unexpected argument: " ++ show a 1467 1468 1469noFPUnary :: String -> FP -> FP 1470noFPUnary o a = error $ "SBV.FPR." ++ o ++ ": Unexpected argument: " ++ show a 1471 1472-- | Given a composite structure, figure out how to compare for less than 1473svStructuralLessThan :: SVal -> SVal -> SVal 1474svStructuralLessThan x y 1475 | isConcrete x && isConcrete y 1476 = x `svLessThan` y 1477 | KTuple{} <- kx 1478 = tupleLT x y 1479 | KMaybe{} <- kx 1480 = maybeLT x y 1481 | KEither{} <- kx 1482 = eitherLT x y 1483 | True 1484 = x `svLessThan` y 1485 where kx = kindOf x 1486 1487-- | Structural less-than for tuples 1488tupleLT :: SVal -> SVal -> SVal 1489tupleLT x y = SVal KBool $ Right $ cache res 1490 where ks = case kindOf x of 1491 KTuple xs -> xs 1492 k -> error $ "Data.SBV: Impossible happened, tupleLT called with: " ++ show (k, x, y) 1493 1494 n = length ks 1495 1496 res st = do sx <- svToSV st x 1497 sy <- svToSV st y 1498 1499 let chkElt i ek = let xi = SVal ek $ Right $ cache $ \_ -> newExpr st ek $ SBVApp (TupleAccess i n) [sx] 1500 yi = SVal ek $ Right $ cache $ \_ -> newExpr st ek $ SBVApp (TupleAccess i n) [sy] 1501 lt = xi `svStructuralLessThan` yi 1502 eq = xi `svEqual` yi 1503 in (lt, eq) 1504 1505 walk [] = svFalse 1506 walk [(lti, _)] = lti 1507 walk ((lti, eqi) : rest) = lti `svOr` (eqi `svAnd` walk rest) 1508 1509 svToSV st $ walk $ zipWith chkElt [1..] ks 1510 1511-- | Structural less-than for maybes 1512maybeLT :: SVal -> SVal -> SVal 1513maybeLT x y = sMaybeCase ( sMaybeCase svFalse (const svTrue) y) 1514 (\jx -> sMaybeCase svFalse (jx `svStructuralLessThan`) y) 1515 x 1516 where ka = case kindOf x of 1517 KMaybe k' -> k' 1518 k -> error $ "Data.SBV: Impossible happened, maybeLT called with: " ++ show (k, x, y) 1519 1520 sMaybeCase brNothing brJust s = SVal KBool $ Right $ cache res 1521 where res st = do sv <- svToSV st s 1522 1523 let justVal = SVal ka $ Right $ cache $ \_ -> newExpr st ka $ SBVApp MaybeAccess [sv] 1524 justRes = brJust justVal 1525 1526 br1 <- svToSV st brNothing 1527 br2 <- svToSV st justRes 1528 1529 -- Do we have a value? 1530 noVal <- newExpr st KBool $ SBVApp (MaybeIs ka False) [sv] 1531 newExpr st KBool $ SBVApp Ite [noVal, br1, br2] 1532 1533-- | Structural less-than for either 1534eitherLT :: SVal -> SVal -> SVal 1535eitherLT x y = sEitherCase (\lx -> sEitherCase (lx `svStructuralLessThan`) (const svTrue) y) 1536 (\rx -> sEitherCase (const svFalse) (rx `svStructuralLessThan`) y) 1537 x 1538 where (ka, kb) = case kindOf x of 1539 KEither k1 k2 -> (k1, k2) 1540 k -> error $ "Data.SBV: Impossible happened, eitherLT called with: " ++ show (k, x, y) 1541 1542 sEitherCase brA brB sab = SVal KBool $ Right $ cache res 1543 where res st = do abv <- svToSV st sab 1544 1545 let leftVal = SVal ka $ Right $ cache $ \_ -> newExpr st ka $ SBVApp (EitherAccess False) [abv] 1546 rightVal = SVal kb $ Right $ cache $ \_ -> newExpr st kb $ SBVApp (EitherAccess True) [abv] 1547 1548 leftRes = brA leftVal 1549 rightRes = brB rightVal 1550 1551 br1 <- svToSV st leftRes 1552 br2 <- svToSV st rightRes 1553 1554 -- Which branch are we in? Return the appropriate value: 1555 onLeft <- newExpr st KBool $ SBVApp (EitherIs ka kb False) [abv] 1556 newExpr st KBool $ SBVApp Ite [onLeft, br1, br2] 1557 1558{-# ANN svIte ("HLint: ignore Eta reduce" :: String) #-} 1559{-# ANN svLazyIte ("HLint: ignore Eta reduce" :: String) #-} 1560{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-} 1561