From 4a4159e49186b1a6469a8c9a009f9d78b105e8e1 Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Tue, 5 Nov 2024 08:50:46 -0800 Subject: [PATCH] Split bmc into two bmcCover and bmcRefute This makes the intention more clear. Update the docs accordingly. --- CHANGES.md | 3 +- Data/SBV/Tools/BMC.hs | 90 +++++++++++++++---- Documentation/SBV/Examples/ProofTools/BMC.hs | 34 +++---- Documentation/SBV/Examples/Puzzles/DieHard.hs | 18 ++-- 4 files changed, 99 insertions(+), 46 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 0573233c..1852eb1a 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -41,7 +41,8 @@ generalizes the use cases, and it is easy to translate from existing applications. Simply change your old 'State -> [State]' function to 'State -> State -> SBool', which can be achieved by 'newTrans s1 s2 = s2 `sElem` oldTrans s1', though you probably want to code this in a more readable way - depending on the actual transition relation you want to model. + depending on the actual transition relation you want to model. Furthermore, the function bmc is now + split into two bmcRefute and bmcCover, to indicate use cases more clearly. * [BACKWARDS COMPATIBILITY] Removed the Fresh class, which was used as a proxy for the Queriable class as an easier to instantiate version. The extra functionality unfortunately made writing custom Queriable diff --git a/Data/SBV/Tools/BMC.hs b/Data/SBV/Tools/BMC.hs index fe5fa360..c3872be8 100644 --- a/Data/SBV/Tools/BMC.hs +++ b/Data/SBV/Tools/BMC.hs @@ -17,7 +17,7 @@ {-# OPTIONS_GHC -Wall -Werror #-} module Data.SBV.Tools.BMC ( - bmc, bmcWith + bmcRefute, bmcRefuteWith, bmcCover, bmcCoverWith ) where import Data.SBV @@ -25,12 +25,14 @@ import Data.SBV.Control import Control.Monad (when) --- | Bounded model checking, using the default solver. See "Documentation.SBV.Examples.ProofTools.BMC" --- for an example use case. --- --- Note that the BMC engine does *not* guarantee that the solution is unique. However, if it does --- find a solution at depth @i@, it is guaranteed that there are no shorter solutions. -bmc :: (Queriable IO st, res ~ QueryResult st) +-- | Are we covering or refuting? +data BMCKind = Refute + | Cover + +-- | Refutation using bounded model checking, using the default solver. This version tries to refute the goal +-- in a depth-first fashion. Note that this method can find a refutation, but will never find a "proof." +-- If it finds a refutation, it will be the shortest, though not necessarily unique. +bmcRefute :: (Queriable IO st, res ~ QueryResult st) => Maybe Int -- ^ Optional bound -> Bool -- ^ Verbose: prints iteration count -> Symbolic () -- ^ Setup code, if necessary. (Typically used for 'Data.SBV.setOption' calls. Pass @return ()@ if not needed.) @@ -38,11 +40,49 @@ bmc :: (Queriable IO st, res ~ QueryResult st) -> (st -> st -> SBool) -- ^ Transition relation -> (st -> SBool) -- ^ Goal to cover, i.e., we find a set of transitions that satisfy this predicate. -> IO (Either String (Int, [res])) -- ^ Either a result, or a satisfying path of given length and intermediate observations. -bmc = bmcWith defaultSMTCfg +bmcRefute = bmcRefuteWith defaultSMTCfg + +-- | Refutation using a given solver. +bmcRefuteWith :: (Queriable IO st, res ~ QueryResult st) + => SMTConfig -- ^ Solver to use + -> Maybe Int -- ^ Optional bound + -> Bool -- ^ Verbose: prints iteration count + -> Symbolic () -- ^ Setup code, if necessary. (Typically used for 'Data.SBV.setOption' calls. Pass @return ()@ if not needed.) + -> (st -> SBool) -- ^ Initial condition + -> (st -> st -> SBool) -- ^ Transition relation + -> (st -> SBool) -- ^ Goal to cover, i.e., we find a set of transitions that satisfy this predicate. + -> IO (Either String (Int, [res])) -- ^ Either a result, or a satisfying path of given length and intermediate observations. +bmcRefuteWith = bmcWith Refute --- | Bounded model checking, configurable with the solver +-- | Covers using bounded model checking, using the default solver. This version tries to cover the goal +-- in a depth-first fashion. Note that this method can find a cover, but will never find determine that a goal is +-- not coverable. If it finds a cover, it will be the shortest, though not necessarily unique. +bmcCover :: (Queriable IO st, res ~ QueryResult st) + => Maybe Int -- ^ Optional bound + -> Bool -- ^ Verbose: prints iteration count + -> Symbolic () -- ^ Setup code, if necessary. (Typically used for 'Data.SBV.setOption' calls. Pass @return ()@ if not needed.) + -> (st -> SBool) -- ^ Initial condition + -> (st -> st -> SBool) -- ^ Transition relation + -> (st -> SBool) -- ^ Goal to cover, i.e., we find a set of transitions that satisfy this predicate. + -> IO (Either String (Int, [res])) -- ^ Either a result, or a satisfying path of given length and intermediate observations. +bmcCover = bmcCoverWith defaultSMTCfg + +-- | Cover using a given solver. +bmcCoverWith :: (Queriable IO st, res ~ QueryResult st) + => SMTConfig -- ^ Solver to use + -> Maybe Int -- ^ Optional bound + -> Bool -- ^ Verbose: prints iteration count + -> Symbolic () -- ^ Setup code, if necessary. (Typically used for 'Data.SBV.setOption' calls. Pass @return ()@ if not needed.) + -> (st -> SBool) -- ^ Initial condition + -> (st -> st -> SBool) -- ^ Transition relation + -> (st -> SBool) -- ^ Goal to cover, i.e., we find a set of transitions that satisfy this predicate. + -> IO (Either String (Int, [res])) -- ^ Either a result, or a satisfying path of given length and intermediate observations. +bmcCoverWith = bmcWith Cover + +-- | Bounded model checking, configurable with the solver. Not exported; use 'bmcCover', 'bmcRefute' and their "with" variants. bmcWith :: (Queriable IO st, res ~ QueryResult st) - => SMTConfig + => BMCKind + -> SMTConfig -> Maybe Int -> Bool -> Symbolic () @@ -50,25 +90,37 @@ bmcWith :: (Queriable IO st, res ~ QueryResult st) -> (st -> st -> SBool) -> (st -> SBool) -> IO (Either String (Int, [res])) -bmcWith cfg mbLimit chatty setup initial trans goal +bmcWith kind cfg mbLimit chatty setup initial trans goal = runSMTWith cfg $ do setup query $ do state <- create constrain $ initial state go 0 state [] - where go i _ _ + where (what, badResult) = case kind of + Cover -> ("BMC Cover", "Cover can't be established.") + Refute -> ("BMC Refute", "Cannot refute the claim.") + + go i _ _ | Just l <- mbLimit, i >= l - = return $ Left $ "BMC limit of " ++ show l ++ " reached" - go i curState sofar = do when chatty $ io $ putStrLn $ "BMC: Iteration: " ++ show i + = return $ Left $ what ++ " limit of " ++ show l ++ " reached. " ++ badResult + + go i curState sofar = do when chatty $ io $ putStrLn $ what ++ ": Iteration: " ++ show i + push 1 - constrain $ goal curState + + let g = goal curState + constrain $ case kind of + Cover -> g -- Covering the goal + Refute -> sNot g -- Trying to refute the goal, so satisfy the negation + cs <- checkSat + case cs of - DSat{} -> error "BMC: Solver returned an unexpected delta-sat result." - Sat -> do when chatty $ io $ putStrLn $ "BMC: Solution found at iteration " ++ show i + DSat{} -> error $ what ++ ": Solver returned an unexpected delta-sat result." + Sat -> do when chatty $ io $ putStrLn $ what ++ ": Solution found at iteration " ++ show i ms <- mapM project (curState : sofar) return $ Right (i, reverse ms) - Unk -> do when chatty $ io $ putStrLn $ "BMC: Backend solver said unknown at iteration " ++ show i - return $ Left $ "BMC: Solver said unknown in iteration " ++ show i + Unk -> do when chatty $ io $ putStrLn $ what ++ ": Backend solver said unknown at iteration " ++ show i + return $ Left $ what ++ ": Solver said unknown in iteration " ++ show i Unsat -> do pop 1 nextState <- create constrain $ curState `trans` nextState diff --git a/Documentation/SBV/Examples/ProofTools/BMC.hs b/Documentation/SBV/Examples/ProofTools/BMC.hs index 65d42057..ca6efc3b 100644 --- a/Documentation/SBV/Examples/ProofTools/BMC.hs +++ b/Documentation/SBV/Examples/ProofTools/BMC.hs @@ -58,7 +58,7 @@ instance Queriable IO (S SInteger) where -- | We parameterize over the initial state for different variations. problem :: Int -> (S SInteger -> SBool) -> IO (Either String (Int, [S Integer])) -problem lim initial = bmc (Just lim) True setup initial trans goal +problem lim initial = bmcCover (Just lim) True setup initial trans goal where -- This is where we would put solver options, typically via -- calls to 'Data.SBV.setOption'. We do not need any for this problem, @@ -82,11 +82,11 @@ problem lim initial = bmc (Just lim) True setup initial trans goal -- | Example 1: We start from @x=0@, @y=10@, and search up to depth @10@. We have: -- -- >>> ex1 --- BMC: Iteration: 0 --- BMC: Iteration: 1 --- BMC: Iteration: 2 --- BMC: Iteration: 3 --- BMC: Solution found at iteration 3 +-- BMC Cover: Iteration: 0 +-- BMC Cover: Iteration: 1 +-- BMC Cover: Iteration: 2 +-- BMC Cover: Iteration: 3 +-- BMC Cover: Solution found at iteration 3 -- Right (3,[(0,10),(0,6),(0,2),(2,2)]) -- -- As expected, there's a solution in this case. Furthermore, since the BMC engine @@ -102,17 +102,17 @@ ex1 = problem 10 isInitial -- | Example 2: We start from @x=0@, @y=11@, and search up to depth @10@. We have: -- -- >>> ex2 --- BMC: Iteration: 0 --- BMC: Iteration: 1 --- BMC: Iteration: 2 --- BMC: Iteration: 3 --- BMC: Iteration: 4 --- BMC: Iteration: 5 --- BMC: Iteration: 6 --- BMC: Iteration: 7 --- BMC: Iteration: 8 --- BMC: Iteration: 9 --- Left "BMC limit of 10 reached" +-- BMC Cover: Iteration: 0 +-- BMC Cover: Iteration: 1 +-- BMC Cover: Iteration: 2 +-- BMC Cover: Iteration: 3 +-- BMC Cover: Iteration: 4 +-- BMC Cover: Iteration: 5 +-- BMC Cover: Iteration: 6 +-- BMC Cover: Iteration: 7 +-- BMC Cover: Iteration: 8 +-- BMC Cover: Iteration: 9 +-- Left "BMC Cover limit of 10 reached. Cover can't be established." -- -- As expected, there's no solution in this case. While SBV (and BMC) cannot establish -- that there is no solution at a larger depth, you can see that this will never be the diff --git a/Documentation/SBV/Examples/Puzzles/DieHard.hs b/Documentation/SBV/Examples/Puzzles/DieHard.hs index d6536a51..3f64701c 100644 --- a/Documentation/SBV/Examples/Puzzles/DieHard.hs +++ b/Documentation/SBV/Examples/Puzzles/DieHard.hs @@ -74,14 +74,14 @@ instance Queriable IO SState where -- | Solve the problem using a BMC search. We have: -- -- >>> dieHard --- BMC: Iteration: 0 --- BMC: Iteration: 1 --- BMC: Iteration: 2 --- BMC: Iteration: 3 --- BMC: Iteration: 4 --- BMC: Iteration: 5 --- BMC: Iteration: 6 --- BMC: Solution found at iteration 6 +-- BMC Cover: Iteration: 0 +-- BMC Cover: Iteration: 1 +-- BMC Cover: Iteration: 2 +-- BMC Cover: Iteration: 3 +-- BMC Cover: Iteration: 4 +-- BMC Cover: Iteration: 5 +-- BMC Cover: Iteration: 6 +-- BMC Cover: Solution found at iteration 6 -- Big: 0, Small: 0 (Initial) -- Big: 5, Small: 0 (FillBig) -- Big: 2, Small: 3 (BigToSmall) @@ -90,7 +90,7 @@ instance Queriable IO SState where -- Big: 5, Small: 2 (FillBig) -- Big: 4, Small: 3 (BigToSmall) dieHard :: IO () -dieHard = display =<< bmc Nothing True (pure ()) initial trans goal +dieHard = display =<< bmcCover Nothing True (pure ()) initial trans goal where -- we start from empty jugs, and try to reach a state where big has 4 gallons initial State{big, small, action} = (big, small, action) .== (0, 0, sInitial) goal State{big} = big .== 4