improve 0.2.1 → 0.2.2
raw patch · 3 files changed
+262/−90 lines, 3 files
Files
- Language/ImProve/Examples.hs +198/−0
- Language/ImProve/Verify.hs +61/−87
- improve.cabal +3/−3
+ Language/ImProve/Examples.hs view
@@ -0,0 +1,198 @@+-- | ImProve examples.+module Language.ImProve.Examples+ ( buildGCD+ , counter+ , verifyCounter+ , arbiterSpec+ , arbiter+ , arbiter1+ , arbiter2+ , arbiter3+ , verifyArbiters+ , buildArbiters+ , runAll+ ) where++import Language.ImProve++-- | Computes the greatest common divison of two integers.+-- Returns true if the computation is done, and the result.+gcd' :: E Int -> E Int -> Stmt (E Bool, E Int)+gcd' a b = do+ a0 <- int "a0" 0 -- Copy of input 'a'.+ b0 <- int "b0" 0 -- Copy of input 'b'.+ a1 <- int "a1" 0 -- Working copy of 'a'.+ b1 <- int "b1" 0 -- Working copy of 'b'.++ -- A new input to process.+ "startNew" -| if_ (a /=. ref a0 ||. b /=. ref b0) $ do+ a0 <== a+ b0 <== b+ a1 <== a+ b1 <== b++ -- Reduce a1.+ "reduceA" -| if_ (ref a1 >. ref b1) $ do+ a1 <== ref a1 - ref b1++ -- Reduce b1.+ "reduceB" -| if_ (ref b1 >. ref a1) $ do+ b1 <== ref b1 - ref a1++ -- Done if a1 == b1.+ return (ref a1 ==. ref b1, ref a1)+++-- | A top level wrapper for gcd'.+gcdMain :: Stmt ()+gcdMain = do+ let a = input int ["a"] -- Input variable 'a'.+ b = input int ["b"] -- Input variable 'b'.+ done <- bool "done" False -- Variable signalling completion.+ result <- int "result" 0 -- Result of GCD.++ -- Call gcd' in its own scope. (Scopes prevent variable name collisions.)+ (done', result') <- "gcd" -| gcd' a b++ -- Bind the results to the output variables.+ done <== done'+ result <== result'++-- | Build the gcdMain code (i.e. gcd.c, gcd.h).+buildGCD :: IO ()+buildGCD = code "gcd" gcdMain++++-- | A rolling counter verification example.+counter :: Stmt ()+counter = do+ -- The counter variable.+ counter <- int "counter" 0++ -- Specification.+ theorem "GreaterThanOrEqualTo0" 1 [] $ ref counter >=. 0+ theorem "LessThan10" 1 [] $ ref counter <=. 9++ -- Implementation.+ ifelse (ref counter ==. 9) (counter <== 0) (counter <== ref counter + 1)++-- | Verify the 'counter' example.+verifyCounter :: IO ()+verifyCounter = verify "yices" counter++++-- | Arbiter specification.+arbiterSpec :: (E Bool, E Bool, E Bool) -> (E Bool, E Bool, E Bool) -> Stmt ()+arbiterSpec (requestA, requestB, requestC) (grantA, grantB, grantC) = do++ -- Mutual exclusion. At most, only one requester granted at a time.+ theorem "OneHot" 1 [] $ grantA &&. not_ grantB &&. not_ grantC+ ||. not_ grantA &&. grantB &&. not_ grantC+ ||. not_ grantA &&. not_ grantB &&. grantC+ ||. not_ grantA &&. not_ grantB &&. not_ grantC+ + -- No grants without requests.+ theorem "NotRequestedA" 1 [] $ not_ requestA --> not_ grantA+ theorem "NotRequestedB" 1 [] $ not_ requestB --> not_ grantB+ theorem "NotRequestedC" 1 [] $ not_ requestC --> not_ grantC++ -- Grants to single requests.+ theorem "OnlyRequestA" 1 [] $ ( requestA &&. not_ requestB &&. not_ requestC) --> grantA+ theorem "OnlyRequestB" 1 [] $ (not_ requestA &&. requestB &&. not_ requestC) --> grantB+ theorem "OnlyRequestC" 1 [] $ (not_ requestA &&. not_ requestB &&. requestC) --> grantC++ -- Priority.+ theorem "Highest" 1 [] $ requestA --> grantA+ theorem "Medium" 1 [] $ (not_ requestA &&. requestB) --> grantB+ theorem "Lowest" 1 [] $ (not_ requestA &&. not_ requestB &&. requestC) --> grantC++ return ()++-- | An arbiter implementation.+arbiter1 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)+arbiter1 (requestA, requestB, requestC) = do+ let grantA = requestA+ grantB = requestB+ grantC = requestC+ return (grantA, grantB, grantC)++-- | An another arbiter implementation.+arbiter2 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)+arbiter2 (requestA, requestB, requestC) = do+ grantA <- bool "grantA" False+ grantB <- bool "grantB" False+ grantC <- bool "grantC" False++ "GrantA" -| if_ (requestA) (grantA <== true)+ "GrantB" -| if_ (not_ requestA &&. requestB) (grantB <== true)+ "GrantC" -| if_ (not_ requestA &&. not_ requestB &&. requestC) (grantC <== true)++ return (ref grantA, ref grantB, ref grantC)++-- | Yet another arbiter implementation.+arbiter3 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)+arbiter3 (requestA, requestB, requestC) = do+ let grantA = requestA+ grantB = not_ requestA &&. requestB+ grantC = not_ requestA &&. not_ requestB &&. requestC+ return (grantA, grantB, grantC)++-- | Binding an arbiter implemenation to the arbiter specification.+arbiter :: Name -> ((E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)) -> Stmt ()+arbiter name implementation = name -| do+ -- Create input variables.+ let requestA = input bool ["requestA"]+ requestB = input bool ["requestB"]+ requestC = input bool ["requestC"]+ let requests = (requestA, requestB, requestC)++ -- Instantiate implementation.+ grants@(grantA, grantB, grantC) <- "impl" -| implementation requests++ -- Bind specification.+ arbiterSpec requests grants++ -- Create output variables.+ bool' "grantA" grantA+ bool' "grantB" grantB+ bool' "grantC" grantC+ return ()++-- | Verify the different arbiter implementations.+verifyArbiters :: IO ()+verifyArbiters = do+ putStrLn "\nVerifying arbiter1 ..."+ verify "yices" $ arbiter "arbiter1" arbiter1++ putStrLn "\nVerifying arbiter2 ..."+ verify "yices" $ arbiter "arbiter2" arbiter2++ putStrLn "\nVerifying arbiter2 ..."+ verify "yices" $ arbiter "arbiter3" arbiter3++-- | Build the different arbiter implementations.+buildArbiters :: IO ()+buildArbiters = do+ putStrLn "\nBuilding arbiter1 (arbiter1.c/h) ..."+ code "arbiter1" $ arbiter "arbiter1" arbiter1++ putStrLn "\nBuilding arbiter2 (arbiter2.c/h) ..."+ code "arbiter2" $ arbiter "arbiter2" arbiter2++ putStrLn "\nBuilding arbiter3 (arbiter3.c/h) ..."+ code "arbiter3" $ arbiter "arbiter3" arbiter3++-- | Run all examples.+runAll :: IO ()+runAll = do+ putStrLn "\nBuilding GCD (gcd.c, gcd.h) ..."+ buildGCD+ putStrLn "\nVerifying counter ..."+ verifyCounter+ putStrLn "\nVerifying arbiters ..."+ verifyArbiters+ putStrLn "\nBuilding arbiters ..."+ buildArbiters+
Language/ImProve/Verify.hs view
@@ -1,6 +1,7 @@ module Language.ImProve.Verify (verify) where import Control.Monad.State+import Data.List import Math.SMT.Yices.Pipe import Math.SMT.Yices.Syntax import System.IO@@ -13,7 +14,7 @@ verify :: FilePath -> Statement -> IO () verify yices program = mapM_ (proveTheorem yices format program) $ theorems program where- format = "%-" ++ show (maximum [ length $ pathName $ theoremPath t program | (t, _, _, _) <- theorems program ]) ++ "s "+ format = "%-" ++ show (maximum' [ length $ pathName $ theoremPath t program | (t, _, _, _) <- theorems program ]) ++ "s " -- | Path of a theorem. theoremPath :: Int -> Statement -> Path@@ -28,7 +29,7 @@ _ -> Nothing f :: Statement -> Maybe Path f a = case a of- Theorem t' _ _ _ | t == t' -> Just [show t']+ Theorem t' _ _ _ | t == t' -> Just [] Sequence a b -> pair a b Branch _ a b -> pair a b Label name a -> do@@ -36,56 +37,6 @@ return $ name : path _ -> Nothing -{---- | Trim all unneeded stuff from a program.-trimProgram :: Int -> Statement -> Statement-trimProgram t program = trim program- where- vars = fixPoint []- fixPoint :: [UV] -> [UV]- fixPoint a = if sort (nub a) == sort (nub b) then sort (nub a) else fixPoint b- where- b = requiredVars base a- trim :: Statement -> Statement- trim a = case a of- Null -> Null- Assign b _ -> if elem (untype b) vars then a else Null- Branch a b c -> case (trim b, trim c) of- (Null, Null) -> Null- (b, c) -> Branch a b c- Sequence a b -> case (trim a, trim b) of- (Null, a) -> a- (a, Null) -> a- (a, b) -> Sequence a b- Assert a -> Assert a- Assume a -> if any (flip elem vars) (exprVars a) then Assume a else Null- Label name a -> case trim a of- Null -> Null- a -> Label name a--requiredVars :: Statement -> [UV] -> [UV]-requiredVars a required = case a of- Assign a b -> if elem (untype a) required then nub $ untype a : exprVars b ++ required else required- Branch a b c -> if any (flip elem $ modifiedVars b ++ modifiedVars c) required || (not $ null $ requiredVars b []) || (not $ null $ requiredVars c [])- then nub $ exprVars a ++ requiredVars b (requiredVars c required)- else required- Sequence a b -> requiredVars a (requiredVars b required)- Assert a -> nub $ exprVars a ++ required- Assume a -> if any (flip elem required) (exprVars a) then nub $ exprVars a ++ required else required- Label _ a -> requiredVars a required- Null -> required--modifiedVars :: Statement -> [UV]-modifiedVars a = case a of- Assign a _ -> [untype a]- Branch _ b c -> modifiedVars b ++ modifiedVars c- Sequence a b -> modifiedVars a ++ modifiedVars b- Assert _ -> []- Assume _ -> []- Label _ a -> modifiedVars a- Null -> []--}- -- | Prove a single theorem. proveTheorem :: FilePath -> String -> Statement -> (Int, Int, [Int], E Bool) -> IO () proveTheorem yices format program (id, k, lemmas, _) = do@@ -102,24 +53,26 @@ -- | k-induction. check :: FilePath -> Name -> Int -> [Int] -> Statement -> Env -> Int -> Y () check yices name theorem lemmas program env0 k = do- mapM_ step [0 .. k - 1]+ replicateM_ k step resultBasis <- checkBasis yices program env0 case resultBasis of- Fail a -> liftIO (printf "FAILED: disproved basis (see %s.trace)\n" name) >> writeTrace name a+ Fail a -> liftIO (printf "FAILED: disproved basis (see %s.trace)\n" name) >> writeTrace False name a Problem -> error "Verify.check1" Pass -> do- step k+ step resultStep <- checkStep yices case resultStep of- Fail a -> liftIO (printf "inconclusive: unable to proved step (see %s.trace)\n" name) >> writeTrace name a+ Fail a -> liftIO (printf "inconclusive: unable to proved step (see %s.trace)\n" name) >> writeTrace True name a Problem -> error "Verify.check2" Pass -> liftIO $ printf "proved\n" where- step :: Int -> Y ()- step i = do- addTrace $ Cycle' i- inputs program+ step :: Y ()+ step = do+ addTrace $ Step' 0+ sequence_ [ getVar' a >>= addTrace . State' (pathName path) | a@(input, path, _) <- sortBy f $ map varInfo $ stmtVars program, not input ]+ sequence_ [ addVar' a >>= addTrace . Input' (pathName path) | a@(input, path, _) <- sortBy f $ map varInfo $ stmtVars program, input ] evalStmt theorem lemmas (LitB True) program+ f (_, a, _) (_, b, _) = compare a b -- | Check induction step. checkStep :: FilePath -> Y Result@@ -143,10 +96,6 @@ ++ [CHECK] return $ result r --- | Insert new input variables.-inputs :: Statement -> Y ()-inputs program = sequence_ [ addVar' a >>= addTrace . Input' (pathName path) | a@(input, path, _) <- map varInfo $ stmtVars program, input ]- result :: ResY -> Result result a = case a of Sat a -> Fail a@@ -285,7 +234,7 @@ } initEnv :: Statement -> IO Env-initEnv program = execStateT (sequence_ [ addVar' a >>= addTrace . Init' (pathName path) | a@(input, path, _) <- map varInfo $ stmtVars program, not input ]) Env+initEnv program = execStateT (sequence_ [ addVar' a | a@(input, _, _) <- map varInfo $ stmtVars program, not input ]) Env { nextId = 0 , var = \ v -> error $ "variable not found in environment: " ++ pathName v , cmds = []@@ -294,8 +243,8 @@ } data Trace- = Init' Name Var- | Cycle' Int+ = Step' Int+ | State' Name Var | Input' Name Var | Assign' Name Var | Assert' Var@@ -335,41 +284,66 @@ env <- get put env { trace = t : trace env } -getVar :: AllE a => V a -> Y String-getVar v = do+getVar :: AllE a => V a -> Y Var+getVar v = getVar' $ varInfo v++getVar' :: VarInfo -> Y Var+getVar' v = do env <- get- return $ var env $ varInfo v+ return $ var env $ v -writeTrace :: String -> [ExpY] -> Y ()-writeTrace name table' = do+writeTrace :: Bool -> String -> [ExpY] -> Y ()+writeTrace dropFirst name table' = do env <- get- liftIO $ writeFile (name ++ ".trace") $ concatMap f $ reverse $ trace env+ let trace'' = reverse $ trace env+ trace' = reorderSteps 1 $ if dropFirst then dropWhile notStep $ tail trace'' else trace''+ format path indent = printf (printf "%%-%ds : %%s" $ maximum' $ 12 : map maxLabelWidth trace') (intercalate "." path) indent+ varFormat :: Name -> String+ varFormat = printf $ printf "%%-%ds" l+ where+ l = maximum $ 0 : map length ([ n | State' n _ <- trace' ] ++ [ n | Input' n _ <- trace' ])+ liftIO $ writeFile (name ++ ".trace") $ concatMap (f varFormat format [] "") trace' where+ notStep (Step' _) = False+ notStep _ = True++ reorderSteps :: Int -> [Trace] -> [Trace]+ reorderSteps _ [] = []+ reorderSteps n (Step' _ : a) = Step' n : reorderSteps (n + 1) a+ reorderSteps n (a : b) = a : reorderSteps n b+ table = [ (n, if v then "true" else "false") | VarE n := LitB v <- table' ] ++ [ (n, show v) | VarE n := LitI v <- table' ] ++ [ (n, show v) | VarE n := LitR v <- table' ]- f :: Trace -> String- f a = case a of- Init' path var -> case lookup var table of++ f :: (String -> String) -> (Path -> String -> String) -> Path -> String -> Trace -> String+ f varFormat format path' indent a = case a of+ Step' n -> "(step " ++ show n ++ ")\n"+ State' path var -> case lookup var table of Nothing -> ""- Just value -> "initialize " ++ path ++ " <== " ++ value ++ "\n"- Cycle' n -> "\nstep " ++ show n ++ "\n"+ Just value -> format ["(state)"] indent ++ varFormat path ++ " == " ++ value ++ "\n" Input' path var -> case lookup var table of Nothing -> ""- Just value -> "input " ++ path ++ " <== " ++ value ++ "\n"+ Just value -> format ["(input)"] indent ++ varFormat path ++ " <== " ++ value ++ "\n" Assign' path var -> case lookup var table of Nothing -> ""- Just value -> path ++ " <== " ++ value ++ "\n"+ Just value -> format path' indent ++ path ++ " <== " ++ value ++ "\n" Assert' var -> case lookup var table of- Just "true" -> "assertion passed\n"- Just "false" -> "assertion FAILED\n"+ Just "true" -> format path' indent ++ "theorem assertion passed\n"+ Just "false" -> format path' indent ++ "theorem assertion FAILED\n" _ -> "" Branch' cond onTrue onFalse -> case lookup cond table of- Just "true" -> "ifelse true:\n" ++ indent (concatMap f onTrue)- Just "false" -> "ifelse false:\n" ++ indent (concatMap f onFalse)+ Just "true" -> format path' indent ++ "ifelse true:\n" ++ concatMap (f varFormat format path' $ " " ++ indent) onTrue+ Just "false" -> format path' indent ++ "ifelse false:\n" ++ concatMap (f varFormat format path' $ " " ++ indent) onFalse _ -> ""- Label' name traces -> name ++ " |-\n" ++ indent (concatMap f traces)+ Label' name traces -> concatMap (f varFormat format (path' ++ [name]) indent) traces -indent :: String -> String-indent = unlines . map (" " ++) . lines+maxLabelWidth :: Trace -> Int+maxLabelWidth a = case a of+ Branch' _ a b -> maximum' $ map maxLabelWidth $ a ++ b+ Label' a b -> length a + 1 + maximum' (map maxLabelWidth b)+ _ -> 0 +maximum' :: [Int] -> Int+maximum' [] = 0+maximum' a = maximum a
improve.cabal view
@@ -1,5 +1,5 @@ name: improve-version: 0.2.1+version: 0.2.2 category: Language, Formal Methods, Embedded @@ -8,8 +8,7 @@ description: ImProve is an imperative programming language for high assurance applications. ImProve uses infinite state, unbounded model checking to verify programs adhere- to specifications, which are written in the form of assertion statements.- Yices (required) is the backend SMT solver.+ to specifications. Yices (required) is the backend SMT solver. author: Tom Hawkins <tomahawkins@gmail.com> maintainer: Tom Hawkins <tomahawkins@gmail.com>@@ -32,6 +31,7 @@ Language.ImProve Language.ImProve.Code Language.ImProve.Core+ Language.ImProve.Examples Language.ImProve.Tree Language.ImProve.Verify