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.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 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 @@ -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, []) 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 @@ -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 diff --git a/Data/SBV/Plugin/Examples/MicroController.hs b/Data/SBV/Plugin/Examples/MicroController.hs --- a/Data/SBV/Plugin/Examples/MicroController.hs +++ b/Data/SBV/Plugin/Examples/MicroController.hs @@ -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 diff --git a/sbvPlugin.cabal b/sbvPlugin.cabal --- a/sbvPlugin.cabal +++ b/sbvPlugin.cabal @@ -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 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 diff --git a/tests/GoldFiles/T16.hs.golden b/tests/GoldFiles/T16.hs.golden --- a/tests/GoldFiles/T16.hs.golden +++ b/tests/GoldFiles/T16.hs.golden @@ -3,5 +3,5 @@ [Z3] Falsifiable. Counter-example: age = Age!val!0 :: Age [SBV] Counter-example might be bogus due to uninterpreted constant: - [] ds_d6ci :: Int + [] ds_d6ck :: Int [SBV] Failed. (Use option 'IgnoreFailure' to continue.) diff --git a/tests/GoldFiles/T43.hs.golden b/tests/GoldFiles/T43.hs.golden new file mode 100644 --- /dev/null +++ b/tests/GoldFiles/T43.hs.golden @@ -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: [ :: SInt64, + :: SInt64, + :: SInt64, + :: SInt64] + vs Length 3: [ :: SInt64, :: SInt64, :: SInt64] diff --git a/tests/GoldFiles/T44.hs.golden b/tests/GoldFiles/T44.hs.golden new file mode 100644 --- /dev/null +++ b/tests/GoldFiles/T44.hs.golden @@ -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