sbvPlugin 0.3 → 0.4
raw patch · 8 files changed
+81/−23 lines, 8 files
Files
- CHANGES.md +9/−1
- Data/SBV/Plugin/Analyze.hs +19/−15
- Data/SBV/Plugin/Common.hs +17/−1
- Data/SBV/Plugin/Examples/MicroController.hs +1/−1
- sbvPlugin.cabal +4/−4
- tests/GoldFiles/T16.hs.golden +1/−1
- tests/GoldFiles/T43.hs.golden +21/−0
- tests/GoldFiles/T44.hs.golden +9/−0
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.3, 2015-12-21+* Latest Hackage released version: 0.4, 2015-12-24++### Version 0.4, 2015-12-24++ * Support for case-alternatives producing lists/tuples+ and functions. In the list case, we require that both+ alternatives produce equal-length lists, as otherwise+ there is no way to merge the two results.+ * More test cases. ### Version 0.3, 2015-12-21
Data/SBV/Plugin/Analyze.hs view
@@ -316,30 +316,34 @@ -- 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 isDefault (DEFAULT, _, _) = True+ Env{curLoc} <- ask+ let caseTooComplicated l w [] = die l ("Unsupported case-expression (" ++ w ++ ")") [sh e]+ caseTooComplicated l w xs = die l ("Unsupported case-expression (" ++ w ++ ")") $ [sh e, "While Analyzing:"] ++ xs+ isDefault (DEFAULT, _, _) = True isDefault _ = False (defs, nonDefs) = partition isDefault alts walk ((p, bs, rhs) : rest) =- do mr <- match (bindSpan caseBinder) sce p bs+ do -- try to get a "good" location for this alternative, if possible:+ let eLoc = case (rhs, bs) of+ (Tick t _, _ ) -> tickSpan t curLoc+ (_, b:_) -> bindSpan b+ _ -> curLoc+ mr <- match eLoc sce p bs case mr of Just (m, bs') -> do let result = local (\env -> env{envMap = foldr (uncurry M.insert) (envMap env) bs'}) $ go rhs if null rest then result- else choose m result (walk rest)- Nothing -> caseTooComplicated "with-complicated-match" ["MATCH " ++ sh (ce, p), " --> " ++ sh rhs]- walk [] = caseTooComplicated "with-non-exhaustive-match" [] -- can't really happen+ else choose (caseTooComplicated eLoc "with-complicated-alternatives-during-merging") m result (walk rest)+ Nothing -> caseTooComplicated eLoc "with-complicated-match" ["MATCH " ++ sh (ce, p), " --> " ++ sh rhs]+ walk [] = caseTooComplicated curLoc "with-non-exhaustive-match" [] -- can't really happen k <- getType (getSrcSpan caseBinder) caseType local (\env -> env{envMap = M.insert (caseBinder, k) sce (envMap env)}) $ walk (nonDefs ++ defs)- where caseTooComplicated w [] = tbd ("Unsupported case-expression (" ++ w ++ ")") [sh e]- caseTooComplicated w xs = tbd ("Unsupported case-expression (" ++ w ++ ")") $ [sh e, "While Analyzing:"] ++ xs- choose t tb fb = case S.svAsBool t of- Nothing -> do stb <- tb- sfb <- fb- case (stb, sfb) of- (Base a, Base b) -> return $ Base $ S.svIte t a b- _ -> caseTooComplicated "with-non-base-alternatives" []- Just True -> tb- Just False -> fb+ where choose bailOut t tb fb = case S.svAsBool t of+ Nothing -> do stb <- tb+ sfb <- fb+ return $ iteVal bailOut t stb sfb+ Just True -> tb+ Just False -> fb match :: SrcSpan -> Val -> AltCon -> [Var] -> Eval (Maybe (S.SVal, [((Var, SKind), Val)])) match sp a c bs = case c of DEFAULT -> return $ Just (S.svTrue, [])
Data/SBV/Plugin/Common.hs view
@@ -117,9 +117,25 @@ k (Lst as) (Lst bs) = foldr S.svAnd (S.svBool (length as == length bs)) (zipWith k as bs) k _ _ = error $ "Impossible happened: liftEq received unexpected arguments: " ++ showSDocUnsafe (ppr (v1, v2)) --- | Symbolic equality over variables+-- | Symbolic equality over values eqVal :: Val -> Val -> S.SVal eqVal = liftEqVal S.svEqual++-- | Symbolic if-then-else over values.+iteVal :: ([String] -> Val) -> S.SVal -> Val -> Val -> 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+ | 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 _ _ = bailOut [ "Unsupported if-then-else/case with alternatives:"+ , " Value:" ++ showSDocUnsafe (ppr v1)+ , " vs:" ++ showSDocUnsafe (ppr v2)+ ] -- | Compute the span given a Tick. Returns the old-span if the tick span useless. tickSpan :: Tickish t -> SrcSpan -> SrcSpan
Data/SBV/Plugin/Examples/MicroController.hs view
@@ -88,7 +88,7 @@ -- * A correct implementation ----------------------------------------------------------------------------- --- | A "good" implementation, properly handling the off-by-one error of the original:+-- | A "good" implementation, properly handling the off-by-one error of the original. computeLastGood :: Int -> Bool -> Int -> Int computeLastGood range manual timeSince | range > safetyDistance = 0
sbvPlugin.cabal view
@@ -1,11 +1,11 @@ Name : sbvPlugin-Version : 0.3+Version : 0.4 Category : Formal methods, Theorem provers, Math, SMT, Symbolic Computation-Synopsis : Analyze Haskell expressions using SBV/SMT-Description : GHC plugin for analyzing expressions using SMT solvers, based+Synopsis : Formally prove properties of Haskell programs using SBV/SMT+Description : GHC plugin for proving properties over Haskell functions using SMT solvers, based on the <http://hackage.haskell.org/package/sbv SBV> package. .- See "Data.SBV.Plugin" for a quick example, or the modules under "Data.SBV.Plugin.Examples"+ See "Data.SBV.Plugin" for a quick example, or the modules under 'Data.SBV.Plugin.Examples' for more details. License : BSD3 License-file : LICENSE
tests/GoldFiles/T16.hs.golden view
@@ -3,5 +3,5 @@ [Z3] Falsifiable. Counter-example: age = Age!val!0 :: Age [SBV] Counter-example might be bogus due to uninterpreted constant:- [<no location info>] ds_d6ci :: Int+ [<no location info>] ds_d6ck :: Int [SBV] Failed. (Use option 'IgnoreFailure' to continue.)
+ tests/GoldFiles/T43.hs.golden view
@@ -0,0 +1,21 @@++[SBV] tests/T43.hs:13:1 Proving "t", using Z3.+[Z3] Q.E.D.++[SBV] tests/T43.hs:19:1 Proving "r", using Z3.++[SBV] tests/T43.hs:19:1 Skipping proof. Unsupported case-expression (with-complicated-alternatives-during-merging):+ case == @ Int $fEqInt x (I# 0) of _ [Occ=Dead] {+ False ->+ (\ _ [Occ=Dead, OS=OneShot] ->+ : @ Int x (: @ Int x (: @ Int x (: @ Int x ([] @ Int)))))+ void#;+ True -> : @ Int x (: @ Int x (: @ Int x ([] @ Int)))+}+ While Analyzing:+ Alternatives are producing lists of differing sizes:+ Length 4: [<symbolic> :: SInt64,+ <symbolic> :: SInt64,+ <symbolic> :: SInt64,+ <symbolic> :: SInt64]+ vs Length 3: [<symbolic> :: SInt64, <symbolic> :: SInt64, <symbolic> :: SInt64]
+ tests/GoldFiles/T44.hs.golden view
@@ -0,0 +1,9 @@++[SBV] tests/T44.hs:12:1 Proving "t", using Z3.+[Z3] Q.E.D.++[SBV] tests/T44.hs:20:1 Proving "r", using Z3.+[Z3] Falsifiable. Counter-example:+ b = False :: Bool+ x = 0 :: Integer+ y = -1 :: Integer