diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,15 @@ * Hackage: * GitHub: -* Latest Hackage released version: 0.5, 2015-12-26 +* Latest Hackage released version: 0.6, 2015-01-01 + +### Version 0.6, 2016-01-01 + + * Support for list expressions of the form [x .. y] and + [x, y .. z]; so long as the x, y, and z are all concrete. + * Simplify some of the expressions in BitTricks using + the new list-construction support. + * Added more proofs to the BitTricks example ### Version 0.5, 2015-12-26 diff --git a/COPYRIGHT b/COPYRIGHT --- a/COPYRIGHT +++ b/COPYRIGHT @@ -1,4 +1,4 @@ -Copyright (c) 2010-2015, Levent Erkok (erkokl@gmail.com) +Copyright (c) 2015-2016, Levent Erkok (erkokl@gmail.com) All rights reserved. The sbvPlugin is distributed with the BSD3 license. See the LICENSE file diff --git a/Data/SBV/Plugin/Analyze.hs b/Data/SBV/Plugin/Analyze.hs --- a/Data/SBV/Plugin/Analyze.hs +++ b/Data/SBV/Plugin/Analyze.hs @@ -16,7 +16,7 @@ import GhcPlugins import Control.Monad.Reader -import System.Exit hiding (die) +import System.Exit import Data.IORef @@ -45,7 +45,7 @@ bind (b, e) = mapM_ work (sbvAnnotation b) where work (SBV opts) | Just s <- hasSkip opts - = liftIO $ putStrLn $ "[SBV] " ++ showSpan cfg (pickSpan [varSpan b]) ++ " Skipping " ++ show (showSDoc (flags cfgEnv) (ppr b)) ++ ": " ++ s + = liftIO $ putStrLn $ "[SBV] " ++ showSpan (flags cfgEnv) (pickSpan [varSpan b]) ++ " Skipping " ++ show (showSDoc (flags cfgEnv) (ppr b)) ++ ": " ++ s | Uninterpret `elem` opts = return () | True @@ -67,13 +67,6 @@ bad e = do print e return False --- | Sometimes life is hard. Giving up is an option. -die :: Config -> [SrcSpan] -> String -> [String] -> a -die cfg locs w es = error $ concatMap ("\n" ++) $ tag ("Skipping proof. " ++ w ++ ":") : map tab es - where marker = "[SBV] " ++ showSpan cfg (pickSpan locs) - tag s = marker ++ " " ++ s - tab s = replicate (length marker) ' ' ++ " " ++ s - -- | Returns True if proof went thru proveIt :: Config -> [SBVOption] -> Var -> CoreExpr -> IO Bool proveIt cfg@Config{cfgEnv, sbvAnnotation} opts topBind topExpr = do @@ -84,7 +77,7 @@ | qCheck = Left `fmap` S.svQuickCheck prop | True = Right `fmap` S.proveWithAny [s{S.verbose = verbose} | s <- solverConfigs] prop topLoc = varSpan topBind - loc = "[SBV] " ++ showSpan cfg topLoc + loc = "[SBV] " ++ showSpan (flags cfgEnv) topLoc slvrTag = ", using " ++ tag ++ "." where tag = case solverConfigs of [] -> "no solvers" -- can't really happen @@ -126,17 +119,26 @@ where debug = Debug `elem` opts + -- | Sometimes life is hard. Giving up is an option. + cantHandle :: String -> [String] -> Eval a + cantHandle w es = do Env{flags, curLoc} <- ask + let marker = "[SBV] " ++ showSpan flags (pickSpan curLoc) + tag s = marker ++ " " ++ s + tab s = replicate (length marker) ' ' ++ " " ++ s + error $ concatMap ("\n" ++) $ tag ("Skipping proof. " ++ w ++ ":") : map tab es + res initEnv topLoc = do v <- runReaderT (symEval topExpr) initEnv { curLoc = [topLoc] , mbListSize = listToMaybe [n | ListSize n <- opts] + , bailOut = cantHandle } case v of Base r -> return r r -> error $ "Impossible happened. Final result reduced to a non-base value: " ++ showSDocUnsafe (ppr r) tbd :: String -> [String] -> Eval Val - tbd w ws = do Env{curLoc} <- ask - die cfg curLoc w ws + tbd w ws = do Env{bailOut} <- ask + bailOut w ws sh o = showSDoc (flags cfgEnv) (ppr o) @@ -145,8 +147,8 @@ -- number of symbolic arguments symEval :: CoreExpr -> Eval Val symEval e = do let (bs, body) = collectBinders (pushLetLambda e) - Env{curLoc} <- ask - bodyType <- getType (pickSpan curLoc) (exprType body) + curEnv@Env{bailOut} <- ask + bodyType <- getType (pickSpan (curLoc curEnv)) (exprType body) -- Figure out if there were some unmentioned variables; happens if the top -- level wasn't fully saturated. @@ -157,7 +159,8 @@ case finalType of KBase S.KBool -> do -- First collect the named arguments: argKs <- mapM (\b -> getType (getSrcSpan b) (varType b) >>= \bt -> return (b, bt)) bs - let mkVar ((b, k), mbN) = do sv <- mkSym cfg (Just b) (varSpan b) (Just (idType b)) k (mbN `mplus` Just (sh b)) + let mkVar ((b, k), mbN) = do sv <- local (\env -> env{curLoc = varSpan b : curLoc env}) + $ mkSym cfg (Just b) (Just (idType b)) k (mbN `mplus` Just (sh b)) return ((b, k), sv) bArgs <- mapM mkVar (zip argKs (concat [map Just ns | Names ns <- opts] ++ repeat Nothing)) @@ -166,16 +169,16 @@ -- If there are extraArgs; then create symbolics and apply to the result: let feed [] sres = return sres - feed (k:ks) (Func _ f) = do sv <- mkSym cfg Nothing (pickSpan curLoc) Nothing k Nothing + feed (k:ks) (Func _ f) = do sv <- mkSym cfg Nothing Nothing k Nothing f sv >>= feed ks feed ks v = error $ "Impossible! Left with extra args to apply on a non-function: " ++ sh (ks, v) feed extraArgs bRes - _ -> die cfg curLoc "Non-boolean property declaration" (concat [ ["Found : " ++ sh (exprType e)] - , ["Returning: " ++ sh (exprType body) | not (null bs)] - , ["Expected : Bool" ++ if null bs then "" else " result"] - ]) + _ -> bailOut "Non-boolean property declaration" (concat [ ["Found : " ++ sh (exprType e)] + , ["Returning: " ++ sh (exprType body) | not (null bs)] + , ["Expected : Bool" ++ if null bs then "" else " result"] + ]) where -- Sometimes the core has a wrapper let, floated out on top. Float that in. pushLetLambda (Let b (Lam x bd)) = Lam x (pushLetLambda (Let b bd)) pushLetLambda o = o @@ -202,10 +205,10 @@ Just b -> return b Nothing -> case v `M.lookup` coreMap of Just (l, b) -> if isUninterpretedBinding v - then uninterpret cfg False t v + then uninterpret False t v else local (\env -> env{curLoc = l : curLoc env}) $ go b Nothing -> debugTrace ("Uninterpreting: " ++ sh (v, k, nub $ sort $ map (fst . fst) (M.toList envMap))) - $ uninterpret cfg False t v + $ uninterpret False t v tgo t e@(Lit l) = do Env{machWordSize} <- ask case l of @@ -259,6 +262,20 @@ Just f -> debugTrace ("Special located: " ++ sh (orig, f)) $ return f Nothing -> case reduced of + -- special case for exponentiation; there must be a better way to do this + App (App (App (App (Var v) (Type t1)) (Type t2)) dict1) dict2 | isReallyADictionary dict1 && isReallyADictionary dict2 -> do + Env{envMap} <- ask + let vSpan = getSrcSpan v + k1 <- getType vSpan t1 + k2 <- getType vSpan t2 + let kExp = KFun k1 (KFun k1 k2) + case (v, kExp) `M.lookup` envMap of + Just b -> debugTrace ("Located exp(^): " ++ sh (reduced, kExp)) $ return b + _ -> do Env{coreMap} <- ask + case v `M.lookup` coreMap of + Just (l, e) -> local (\env -> env{curLoc = l : curLoc env}) $ tgo tFun (App (App (App (App e (Type t1)) (Type t2)) dict1) dict2) + Nothing -> tgo tFun (Var v) + -- special case for split and join; there must be a better way to do this App (App (App (Var v) (Type t1)) (Type t2)) dict | isReallyADictionary dict -> do Env{envMap} <- ask @@ -316,11 +333,13 @@ -- simple if-then-else chain with the last element on the DEFAULT, or whatever comes last. tgo _ e@(Case ce caseBinder caseType alts) = do sce <- go ce - let caseTooComplicated l w [] = die cfg l ("Unsupported case-expression (" ++ w ++ ")") [sh e] - caseTooComplicated l w xs = die cfg l ("Unsupported case-expression (" ++ w ++ ")") $ [sh e, "While Analyzing:"] ++ xs + let caseTooComplicated w [] = tbd ("Unsupported case-expression (" ++ w ++ ")") [sh e] + caseTooComplicated w xs = tbd ("Unsupported case-expression (" ++ w ++ ")") $ [sh e, "While Analyzing:"] ++ xs isDefault (DEFAULT, _, _) = True isDefault _ = False (defs, nonDefs) = partition isDefault alts + + walk [] = caseTooComplicated "with-non-exhaustive-match" [] -- can't really happen walk ((p, bs, rhs) : rest) = do -- try to get a "good" location for this alternative, if possible: let eLoc = case (rhs, bs) of @@ -333,18 +352,16 @@ Just (m, bs') -> do let result = local (\env -> env{curLoc = eLoc : curLoc env, envMap = foldr (uncurry M.insert) (envMap env) bs'}) $ go rhs if null rest then result - else do Env{curLoc} <- ask - choose (caseTooComplicated (eLoc : curLoc) "with-complicated-alternatives-during-merging") m result (walk rest) - Nothing -> do Env{curLoc} <- ask - caseTooComplicated (eLoc : curLoc) "with-complicated-match" ["MATCH " ++ sh (ce, p), " --> " ++ sh rhs] - walk [] = do Env{curLoc} <- ask - caseTooComplicated curLoc "with-non-exhaustive-match" [] -- can't really happen + else choose (caseTooComplicated "with-complicated-alternatives-during-merging") m result (walk rest) + Nothing -> caseTooComplicated "with-complicated-match" ["MATCH " ++ sh (ce, p), " --> " ++ sh rhs] + k <- getType (getSrcSpan caseBinder) caseType local (\env -> env{envMap = M.insert (caseBinder, k) sce (envMap env)}) $ walk (nonDefs ++ defs) + where choose bailOut t tb fb = case S.svAsBool t of Nothing -> do stb <- tb sfb <- fb - return $ iteVal bailOut t stb sfb + iteVal bailOut t stb sfb Just True -> tb Just False -> fb match :: SrcSpan -> Val -> AltCon -> [Var] -> Eval (Maybe (S.SVal, [((Var, SKind), Val)])) @@ -409,8 +426,8 @@ isReallyADictionary _ = False -- Create a symbolic variable. -mkSym :: Config -> Maybe Var -> SrcSpan -> Maybe Type -> SKind -> Maybe String -> Eval Val -mkSym cfg@Config{cfgEnv} mbBind curLoc mbBType = sym +mkSym :: Config -> Maybe Var -> Maybe Type -> SKind -> Maybe String -> Eval Val +mkSym Config{cfgEnv} mbBind mbBType = sym where sh o = showSDoc (flags cfgEnv) (ppr o) tinfo k = case mbBType of @@ -424,29 +441,31 @@ vs <- zipWithM sym ks ns return $ Tup vs - sym (KLst ks) nm = do Env{mbListSize} <- ask - let ls = fromMaybe bad mbListSize - bad = die cfg [curLoc] "List-argument found, with no size info" + sym (KLst ks) nm = do Env{mbListSize, bailOut} <- ask + ls <- case mbListSize of + Just i -> return i + Nothing -> bailOut "List-argument found, with no size info" [ "Name: " ++ fromMaybe "anonymous" nm , tinfo (KLst ks) , "Hint: Use the \"ListSize\" annotation" ] - ns = map (\i -> (++ ("_" ++ show i)) `fmap` nm) [1 .. ls] + let ns = map (\i -> (++ ("_" ++ show i)) `fmap` nm) [1 .. ls] vs <- zipWithM sym (replicate ls ks) ns return (Lst vs) sym k@KFun{} nm = case mbBind of - Just v -> uninterpret cfg True (varType v) v - _ -> die cfg [curLoc] "Unsupported unnamed higher-order symbolic input" - [ "Name: " ++ fromMaybe "" nm - , tinfo k - , "Hint: Name all higher-order inputs explicitly" - ] + Just v -> uninterpret True (varType v) v + _ -> do Env{bailOut} <- ask + bailOut "Unsupported unnamed higher-order symbolic input" + [ "Name: " ++ fromMaybe "" nm + , tinfo k + , "Hint: Name all higher-order inputs explicitly" + ] -- | Uninterpret an expression -uninterpret :: Config -> Bool -> Type -> Var -> Eval Val -uninterpret cfg isInput t var = do +uninterpret :: Bool -> Type -> Var -> Eval Val +uninterpret isInput t var = do Env{rUninterpreted, flags} <- ask prevUninterpreted <- liftIO $ readIORef rUninterpreted case (var, t) `lookup` prevUninterpreted of @@ -462,13 +481,9 @@ liftIO $ modifyIORef rUninterpreted (((var, t), (isInput, nm, fVal)) :) return fVal where walk :: [SKind] -> (String, SKind) -> [Val] -> Eval Val - walk [] (nm, k) args = do Env{curLoc, mbListSize} <- ask - - let ls = fromMaybe bad mbListSize - bad = die cfg curLoc "List-argument found in uninterpreted function, with no size info" - ["Hint: Use the \"ListSize\" annotation"] + walk [] (nm, k) args = do Env{mbListSize, bailOut} <- ask - mkArg :: Val -> [S.SVal] + let mkArg :: Val -> [S.SVal] mkArg (Base v) = [v] mkArg (Tup vs) = concatMap mkArg vs mkArg (Lst vs) = concatMap mkArg vs @@ -476,16 +491,23 @@ bArgs = concatMap mkArg (reverse args) - mkRes :: String -> SKind -> [S.SVal] - mkRes n (KBase b) = [S.svUninterpreted b n Nothing bArgs] - mkRes n (KTup bs) = concat $ zipWith mkRes [n ++ "_" ++ show i | i <- [(1 :: Int) .. ]] bs - mkRes n (KLst b) = concat [mkRes (n ++ "_" ++ show i) b | i <- [(1 :: Int) .. ls]] - mkRes _ sk = error $ "Not yet supported uninterpreted function with a higher-order result: " ++ showSDocUnsafe (ppr sk) + mkRes :: String -> SKind -> Eval [S.SVal] + mkRes n (KBase b) = return [S.svUninterpreted b n Nothing bArgs] + mkRes n (KTup bs) = concat `fmap` zipWithM mkRes [n ++ "_" ++ show i | i <- [(1 :: Int) .. ]] bs + mkRes n (KLst b) = do ls <- case mbListSize of + Just i -> return i + Nothing -> bailOut "List-argument found in uninterpreted function, with no size info" + ["Hint: Use the \"ListSize\" annotation"] + concat `fmap` zipWithM mkRes [n ++ "_" ++ show i | i <- [(1 :: Int) .. ls]] (repeat b) + mkRes n sk@KFun{} = bailOut "Not yet supported uninterpreted function with a higher-order result" + [ "Name: " ++ n + , "Kind: " ++ showSDocUnsafe (ppr sk) + ] - res = map Base $ mkRes nm k - case res of + res <- mkRes nm k + case map Base res of [x] -> return x - _ -> return $ Tup res + xs -> return $ Tup xs walk (_:ks) nmk args = return $ Func Nothing $ \a -> walk ks nmk (a:args) wrap [] f = f @@ -560,3 +582,5 @@ let k = S.KUserSort nm $ Left $ "originating from sbvPlugin: " ++ showSDoc flags (ppr sp) liftIO $ modifyIORef rUITypes ((bt, k) :) return k + +{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-} diff --git a/Data/SBV/Plugin/Common.hs b/Data/SBV/Plugin/Common.hs --- a/Data/SBV/Plugin/Common.hs +++ b/Data/SBV/Plugin/Common.hs @@ -9,9 +9,11 @@ -- Common data-structures/utilities ----------------------------------------------------------------------------- +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeSynonymInstances #-} -{-# LANGUAGE FlexibleInstances #-} + {-# OPTIONS_GHC -fno-warn-orphans #-} module Data.SBV.Plugin.Common where @@ -51,6 +53,7 @@ , envMap :: M.Map (Var, SKind) Val , destMap :: M.Map Var (Val -> [(Var, SKind)] -> (S.SVal, [((Var, SKind), Val)])) , coreMap :: M.Map Var (SrcSpan, CoreExpr) + , bailOut :: forall a. String -> [String] -> Eval a } @@ -125,16 +128,16 @@ eqVal = liftEqVal S.svEqual -- | Symbolic if-then-else over values. -iteVal :: ([String] -> Val) -> S.SVal -> Val -> Val -> Val +iteVal :: ([String] -> Eval Val) -> S.SVal -> Val -> Val -> Eval Val iteVal bailOut t v1 v2 = k v1 v2 - where k (Base a) (Base b) = Base $ S.svIte t a b - k (Tup as) (Tup bs) | length as == length bs = Tup $ zipWith k as bs - k (Lst as) (Lst bs) | length as == length bs = Lst $ zipWith k as bs + where k (Base a) (Base b) = return $ Base $ S.svIte t a b + k (Tup as) (Tup bs) | length as == length bs = Tup `fmap` zipWithM k as bs + k (Lst as) (Lst bs) | length as == length bs = Lst `fmap` zipWithM k as bs | True = bailOut [ "Alternatives are producing lists of differing sizes:" , " Length " ++ show (length as) ++ ": " ++ showSDocUnsafe (ppr (Lst as)) , "vs Length " ++ show (length bs) ++ ": " ++ showSDocUnsafe (ppr (Lst bs)) ] - k (Func n1 f) (Func n2 g) = Func (n1 `mplus` n2) $ \a -> f a >>= \fa -> g a >>= \ga -> return (k fa ga) + k (Func n1 f) (Func n2 g) = return $ Func (n1 `mplus` n2) $ \a -> f a >>= \fa -> g a >>= \ga -> k fa ga k _ _ = bailOut [ "Unsupported if-then-else/case with alternatives:" , " Value:" ++ showSDocUnsafe (ppr v1) , " vs:" ++ showSDocUnsafe (ppr v2) @@ -159,8 +162,8 @@ [] -> noSrcSpan -- | Show a GHC span in user-friendly form -showSpan :: Config -> SrcSpan -> String -showSpan Config{cfgEnv} s = showSDoc (flags cfgEnv) (ppr s) +showSpan :: DynFlags -> SrcSpan -> String +showSpan flags s = showSDoc flags (ppr s) -- | This comes mighty handy! Wonder why GHC doesn't have it already: instance Show CoreExpr where diff --git a/Data/SBV/Plugin/Env.hs b/Data/SBV/Plugin/Env.hs --- a/Data/SBV/Plugin/Env.hs +++ b/Data/SBV/Plugin/Env.hs @@ -10,6 +10,7 @@ ----------------------------------------------------------------------------- {-# LANGUAGE MagicHash #-} +{-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE TemplateHaskell #-} module Data.SBV.Plugin.Env (buildTCEnv, buildFunEnv, buildDests, buildSpecials, uninterestingTypes) where @@ -21,14 +22,16 @@ import qualified Data.Map as M import qualified Language.Haskell.TH as TH +import Control.Monad.Reader + import Data.Int import Data.Word import Data.Bits -import Data.Maybe (fromMaybe) +import Data.Maybe (fromMaybe, isJust) import Data.Ratio -import qualified Data.SBV as S hiding (proveWith, proveWithAny) -import qualified Data.SBV.Dynamic as S +import qualified Data.SBV as S hiding (proveWith, proveWithAny) +import qualified Data.SBV.Dynamic as S import Data.SBV.Plugin.Common @@ -113,6 +116,10 @@ -- bv-joins ++ [ ('(S.#), tJoin s, lift2 S.svJoin) | s <- [8, 16, 32]] + -- constructing "fixed-size" lists + ++ [ ('enumFromTo, tEnumFromTo (KBase k), sEnumFromTo) | k <- arithKinds ] + ++ [ ('enumFromThenTo, tEnumFromThenTo (KBase k), sEnumFromThenTo) | k <- arithKinds ] + where -- Bit-vectors bvKinds = [S.KBounded s sz | s <- [False, True], sz <- [8, 16, 32, 64]] @@ -143,6 +150,7 @@ , ('(-), S.svMinus) , ('(*), S.svTimes) , ('(/), S.svDivide) + , ('(^), S.svExp) , ('quot, S.svQuot) , ('rem, S.svRem) ] @@ -279,6 +287,14 @@ where a = KBase (S.KBounded False n) r = KBase (S.KBounded False (n*2)) +-- | Type of enumFromTo: [x .. y] +tEnumFromTo :: SKind -> SKind +tEnumFromTo a = KFun a (KFun a (KLst a)) + +-- | Type of enumFromThenTo: [x .. y] +tEnumFromThenTo :: SKind -> SKind +tEnumFromThenTo a = KFun a (KFun a (KFun a (KLst a))) + -- | Lift a unary SBV function that via kind/integer lift1Int :: (Integer -> S.SVal) -> Val lift1Int f = Func Nothing g @@ -318,6 +334,40 @@ liftEq baseEq = Func Nothing g where g (Typ _) = return $ Func Nothing g g v1 = return $ Func Nothing $ \v2 -> return $ Base $ liftEqVal baseEq v1 v2 + +-- | Lifting enumFromTo: [x .. y] +sEnumFromTo :: Val +sEnumFromTo = Func Nothing (g []) + where g [x] y = enumList x Nothing y + g args (Typ _) = return $ Func Nothing (g args) + g args v = return $ Func Nothing (g (v:args)) + +-- | Lifting sEnumFromThenTo: [x, y .. z] +sEnumFromThenTo :: Val +sEnumFromThenTo = Func Nothing (g []) + where g [x, y] z = enumList y (Just x) z + g args (Typ _) = return $ Func Nothing (g args) + g args v = return $ Func Nothing (g (v:args)) + +-- | Implement [x .. y] or [x, y .. z]; provided the inputs are concrete +enumList :: Val -> Maybe Val -> Val -> Eval Val +enumList bf mbs bt + | Just bs <- mbs, Just f <- extract bf, Just s <- extract bs, Just t <- extract bt = mkLst $ S.svEnumFromThenTo f (Just s) t + | Just f <- extract bf, Just t <- extract bt = mkLst $ S.svEnumFromThenTo f Nothing t + | True = cantHandle + where extract (Base b) = Just b + extract _ = error $ "SBVPlugin.enumList: Impossible happened: " ++ showSDocUnsafe (ppr (bf, mbs, bt)) + mkLst (Just xs) = return $ Lst $ map Base xs + mkLst _ = cantHandle + cantHandle = do Env{bailOut} <- ask + bailOut "Found unsupported list comprehension expression" + (concat [ [ "From: " ++ showSDocUnsafe (ppr bf) ] + , [ "Then: " ++ showSDocUnsafe (ppr bs) | Just bs <- [mbs]] + , [ "To : " ++ showSDocUnsafe (ppr bt) + , "Kind: " ++ (if isJust mbs then "[x, y .. z]" else "[x .. y]") + , "Hint: The plugin only allows finite comprehensions with concrete boundaries." + ] + ]) thToGHC :: (TH.Name, a, b) -> CoreM ((Id, a), b) thToGHC (n, k, sfn) = do f <- grabTH lookupId n diff --git a/Data/SBV/Plugin/Examples/BitTricks.hs b/Data/SBV/Plugin/Examples/BitTricks.hs --- a/Data/SBV/Plugin/Examples/BitTricks.hs +++ b/Data/SBV/Plugin/Examples/BitTricks.hs @@ -19,6 +19,13 @@ import Data.Bits import Data.Word +import Prelude hiding(elem) + +-- | SBVPlugin can only see definitions in the current module. So we define `elem` ourselves. +elem :: Eq a => a -> [a] -> Bool +elem _ [] = False +elem k (x:xs) = k == x || elem k xs + -- | Returns 1 if bool is @True@ oneIf :: Num a => Bool -> a oneIf True = 1 @@ -56,18 +63,45 @@ -- | Formalizes {-# ANN powerOfTwoCorrect theorem #-} powerOfTwoCorrect :: Word32 -> Bool -powerOfTwoCorrect v = f == search powers +powerOfTwoCorrect v = f == (v `elem` [2^i | i <- [(0 :: Word32) .. 31]]) where f = (v /= 0) && ((v .&. (v-1)) == 0) - powers :: [Word32] - powers = [ 1, 2, 4, 8, 16, 32, 64, 128 - , 256, 512, 1024, 2048, 4096, 8192, 16384, 32768 - , 65536, 131072, 262144, 524288, 1048576, 2097152, 4194304, 8388608 - , 16777216, 33554432, 67108864, 134217728, 268435456, 536870912, 1073741824, 2147483648 - ] +-- | Formalizes +{-# ANN maskedMergeCorrect theorem #-} +maskedMergeCorrect :: Word32 -> Word32 -> Word32 -> Bool +maskedMergeCorrect a b mask = slow == fast + where slow = (a .&. complement mask) .|. (b .&. mask) + fast = a `xor` ((a `xor` b) .&. mask) - search :: [Word32] -> Bool - search [] = False - search (x:xs) - | x == v = True - | True = search xs +-- | Formalizes +{-# ANN roundPowerOfTwoCorrect theorem #-} +roundPowerOfTwoCorrect :: Word32 -> Bool +roundPowerOfTwoCorrect v = f == find [2^i | i <- [(0 :: Word32) .. 31]] + where f = let v1 = v - 1 + v2 = v1 .|. (v1 `shiftR` 1) + v3 = v2 .|. (v2 `shiftR` 2) + v4 = v3 .|. (v3 `shiftR` 4) + v5 = v4 .|. (v4 `shiftR` 8) + v6 = v5 .|. (v5 `shiftR` 16) + v7 = v6 + 1 + v8 = v7 + oneIf (v7 == 0) + in v8 + + -- walk down the powers and return the closest one up + find :: [Word32] -> Word32 + find [] = 1 + find (x:xs) + | v > x = find xs + | True = x + +-- | Formalizes +{-# ANN zeroInWord theorem #-} +zeroInWord :: Word32 -> Bool +zeroInWord v = hasZero == fastHasZero + where b3 = (v .&. 0xFF000000) == 0 + b2 = (v .&. 0x00FF0000) == 0 + b1 = (v .&. 0x0000FF00) == 0 + b0 = (v .&. 0x000000FF) == 0 + hasZero = b3 || b2 || b1 || b0 + + fastHasZero = ((v - 0x01010101) .&. complement v .&. 0x80808080) /= 0 diff --git a/Data/SBV/Plugin/Plugin.hs b/Data/SBV/Plugin/Plugin.hs --- a/Data/SBV/Plugin/Plugin.hs +++ b/Data/SBV/Plugin/Plugin.hs @@ -78,6 +78,7 @@ , tcMap = baseTCs , envMap = baseEnv , destMap = baseDests + , bailOut = \s ss -> error $ unlines (s:ss) , coreMap = M.fromList [(b, (varSpan b, e)) | (b, e) <- flattenBinds mg_binds] } } diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,6 +1,6 @@ sbvPlugin: SMT based analyzer for Haskell -Copyright (c) 2015, Levent Erkok (erkokl@gmail.com) +Copyright (c) 2015-2016, Levent Erkok (erkokl@gmail.com) All rights reserved. Redistribution and use in source and binary forms, with or without diff --git a/sbvPlugin.cabal b/sbvPlugin.cabal --- a/sbvPlugin.cabal +++ b/sbvPlugin.cabal @@ -1,5 +1,5 @@ Name : sbvPlugin -Version : 0.5 +Version : 0.6 Category : Formal methods, Theorem provers, Math, SMT, Symbolic Computation Synopsis : Formally prove properties of Haskell programs using SBV/SMT Description : GHC plugin for proving properties over Haskell functions using SMT solvers, based @@ -29,7 +29,7 @@ , Data.SBV.Plugin.Examples.MergeSort , Data.SBV.Plugin.Examples.MicroController , Data.SBV.Plugin.Examples.BitTricks - build-depends : base >= 4.8 && < 5, ghc, ghc-prim, containers, sbv >= 5.7, mtl, template-haskell + build-depends : base >= 4.8 && < 5, ghc, ghc-prim, containers, sbv >= 5.8, mtl, template-haskell Other-modules : Data.SBV.Plugin.Analyze , Data.SBV.Plugin.Data , Data.SBV.Plugin.Common