sbvPlugin 0.5 → 0.6
raw patch · 9 files changed
+207/−87 lines, 9 filesdep ~sbv
Dependency ranges changed: sbv
Files
- CHANGES.md +9/−1
- COPYRIGHT +1/−1
- Data/SBV/Plugin/Analyze.hs +83/−59
- Data/SBV/Plugin/Common.hs +11/−8
- Data/SBV/Plugin/Env.hs +53/−3
- Data/SBV/Plugin/Examples/BitTricks.hs +46/−12
- Data/SBV/Plugin/Plugin.hs +1/−0
- LICENSE +1/−1
- sbvPlugin.cabal +2/−2
CHANGES.md view
@@ -1,7 +1,15 @@ * Hackage: <http://hackage.haskell.org/package/sbvPlugin> * GitHub: <http://github.com/LeventErkok/sbvPlugin> -* 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
COPYRIGHT view
@@ -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
Data/SBV/Plugin/Analyze.hs view
@@ -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 "<anonymous>" 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 "<anonymous>" 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) #-}
Data/SBV/Plugin/Common.hs view
@@ -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
Data/SBV/Plugin/Env.hs view
@@ -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
Data/SBV/Plugin/Examples/BitTricks.hs view
@@ -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 <http://graphics.stanford.edu/~seander/bithacks.html#DetermineIfPowerOf2> {-# 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 <http://graphics.stanford.edu/~seander/bithacks.html#MaskedMerge>+{-# 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 <http://graphics.stanford.edu/~seander/bithacks.html#RoundUpPowerOf2>+{-# 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 <http://graphics.stanford.edu/~seander/bithacks.html#ZeroInWord>+{-# 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
Data/SBV/Plugin/Plugin.hs view
@@ -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] } }
LICENSE view
@@ -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
sbvPlugin.cabal view
@@ -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