afv 0.0.0 → 0.0.1
raw patch · 7 files changed
+123/−150 lines, 7 filesdep ~bytestringdep ~language-cdep ~yices
Dependency ranges changed: bytestring, language-c, yices
Files
- RELEASE-NOTES +6/−0
- afv.cabal +4/−4
- src/AFV.hs +7/−0
- src/Compile.hs +23/−11
- src/Parse.hs +0/−1
- src/Utils.hs +0/−1
- src/Verify.hs +83/−133
RELEASE-NOTES view
@@ -2,3 +2,9 @@ - Initial release. +afv 0.0.1 01/14/10++- Checks for duplicate top-level names.+- Uses yices new 'quickCheckY'.+- Fixed bug affecting 'assume'.+
afv.cabal view
@@ -1,5 +1,5 @@ name: afv-version: 0.0.0+version: 0.0.1 category: Formal Methods @@ -37,12 +37,12 @@ build-depends: base >= 4 && < 5,- bytestring >= 0.9.1 && < 0.9.2,+ bytestring >= 0.9 && < 1.0, mtl >= 1.1 && < 1.2, directory >= 1.0 && < 1.1, process >= 1.0 && < 1.1,- language-c >= 0.3 && < 0.4,- yices >= 0.0.0.4 && < 0.1+ language-c >= 0.3.1.1,+ yices >= 0.0.0.6 ghc-options: -W extensions:
src/AFV.hs view
@@ -8,12 +8,15 @@ import Parse import Verify +version = "0.0.1"+ main :: IO () main = do args <- getArgs case args of [] -> help (a:_) | elem a ["help", "-h", "--help", "-help"] -> help+ | elem a ["version", "-v", "--version"] -> putStrLn $ "afv " ++ version ["example"] -> example ["header"] -> header ("verify":function:args) -> do@@ -23,6 +26,7 @@ verify (yices a) (k a) model _ -> help + data Args = Args { yices :: FilePath , k :: Int@@ -119,6 +123,9 @@ [ "" , "NAME" , " afv - Atom's Formal Verifier"+ , ""+ , "VERSION"+ , " " ++ version , "" , "SYNOPSIS" , " afv verify function-name [-k max-k] [--yices=path-to-yices] [--gcc=path-to-gcc] {-Idir} {-Dmacro[=def]} c-file {c-file}"
src/Compile.hs view
@@ -21,16 +21,27 @@ -- | Rewrites a program to a single statement. Requires no recursive functions and unique declarations for all top level declarations. rewrite :: String -> [CTranslUnit] -> CStat-rewrite name units = if not $ null asms then notSupported (head asms) "inline assembly" else CCompound [] (vars ++ funcs ++ [CBlockStmt call]) none+rewrite name units = if not $ null asms+ then notSupported (head asms) "inline assembly"+ else if not $ null duplicateNames+ then error $ "duplicate top-level names found (hiding names with static is not supported): " ++ show duplicateNames+ else CCompound [] (vars ++ funcs ++ [CBlockStmt call]) none where items = [ a | CTranslUnit items _ <- units, a <- items ]- vars = [ CBlockDecl (CDecl (CStorageSpec (CStatic none) : specs) a b) | CDeclExt (CDecl specs a b) <- items ] -- Make top level vars static.- funcs = map CNestedFunDef $ sortFunctions [ a | CFDefExt a <- items ]+ varDefs = [ a | CDeclExt a <- items ]+ vars = [ CBlockDecl (CDecl (CStorageSpec (CStatic none) : specs) a b) | CDecl specs a b <- varDefs ] -- Make top level vars static.+ funcDefs = [ a | CFDefExt a <- items ]+ funcs = map CNestedFunDef $ sortFunctions funcDefs asms = [ a | CAsmExt a <- items ] call :: CStat call = CExpr (Just $ CCall (CVar (Ident name 0 none) none) [] none) none- -- XXX Need to check for top level name conflicts.+ duplicateNames = duplicates $ [ name | f <- funcDefs, let (_, (Ident name _ _), _, _) = functionInfo f ] ++ concat [ [ name | (Just (CDeclr (Just (Ident name _ _)) _ _ _ _), _, _) <- a ] | CDecl _ a _ <- varDefs ] +duplicates :: Eq a => [a] -> [a]+duplicates [] = []+duplicates (a:b) | elem a b = a : duplicates b+ | otherwise = duplicates b+ type M = StateT MDB IO data MDB = MDB@@ -215,9 +226,9 @@ CGeqOp -> f $ \ a b n -> Not (Lt a b n) n CEqOp -> f Eq CNeqOp -> f $ \ a b n -> Not (Eq a b n) n- CAndOp -> f And- CXorOp -> f $ \ a b n -> Or (And a (Not b n) n) (And (Not a n) b n) n- COrOp -> f Or+ CAndOp -> notSupported a "(&)"+ CXorOp -> notSupported a "(^)"+ COrOp -> notSupported a "(|)" CLndOp -> do a <- evalExpr env a (b, a) <- branch n' a (evalExpr env b) (return a)@@ -251,7 +262,7 @@ b <- latch p $ Var a assign False p a $ Sub (Var a) one p return b- (CPlusOp, a) -> return $ Add zero a p+ (CPlusOp, a) -> return a (CMinOp, a) -> return $ Sub zero a p (CNegOp, a) -> return $ Not a p _ -> notSupported n "unary operator"@@ -284,8 +295,7 @@ evalDecl' env (a, b, c) = case a of Just (CDeclr (Just i@(Ident name _ n)) [] Nothing [] _) -> case (b, c) of (Nothing, Nothing) -> evalDecl' env (a, Just $ CInitExpr (CConst (CIntConst (cInteger 0) n)) n, Nothing)- (Just (CInitExpr c@(CConst const) n'), Nothing) | isStatic typInfo && not (isVolatile typInfo) -> addVar env v- | otherwise -> evalDecl' env (a, Nothing, Just c)+ (Just (CInitExpr (CConst const) n'), Nothing) | isStatic typInfo && not (isVolatile typInfo) -> addVar env v where v = State $ VS name typ init $ posOf n init = case typ of@@ -305,6 +315,8 @@ CFloatConst (CFloat a) _ -> fromIntegral (read a :: Integer) _ -> unexpected const "non numeric initialization" + (Just (CInitExpr c _), Nothing) -> evalDecl' env (a, Nothing, Just c)+ (Nothing, Just e') -> do e <- evalExpr env e' v <- if isVolatile typInfo@@ -321,7 +333,7 @@ evalFunc :: Env -> CFunDef -> M Env evalFunc env f = do- when (typ /= Void || not (null args)) $ notSupported f "non void f(void) function (How lame is this?)"+ when (typ /= Void || not (null args)) $ notSupported f "non void f() function (How lame is this?)" return env { values = EnvFunction name (Function (length args) func) : values env } where (specs, (Ident name _ _), args, stat) = functionInfo f
src/Parse.hs view
@@ -4,7 +4,6 @@ import Language.C.System.GCC import Language.C.System.Preprocess import System.Exit-import System.IO parse :: FilePath -> [FilePath] -> [(String,String)] -> FilePath -> IO CTranslUnit parse gcc includes defines file = do
src/Utils.hs view
@@ -4,7 +4,6 @@ , isVisable ) where -import Data.List import Language.C import Error
src/Verify.hs view
@@ -1,9 +1,7 @@ module Verify (verify) where -import Control.Monad-import Data.IORef+import Control.Monad.State hiding (State) import Data.List-import Data.Maybe import Math.SMT.Yices.Pipe import Math.SMT.Yices.Syntax import System.IO@@ -15,12 +13,11 @@ verify :: FilePath -> Int -> Model -> IO () verify _ maxK _ | maxK < 1 = error "max k can not be less than 1" verify yices maxK m = do- y <- createYicesPipe yices []- mapM_ (verifyModel y maxK) models- exitY y+ mapM_ (verifyModel yices format maxK) models where assertions = [ a | a@(Assert _ _ _) <- actions m ] models = map (trimModel . trimAssertions m) assertions+ format = "verifying %-" ++ show (maximum [ length (intercalate "." n) | (Assert _ n _) <- actions m ]) ++ "s " -- | Remove all assertions except one. trimAssertions :: Model -> Action -> Model@@ -34,113 +31,95 @@ trimModel = id --XXX -- | Verify a trimmed model.-verifyModel :: YicesIPC -> Int -> Model -> IO ()-verifyModel y maxK m = do- printf "verifying assertion %s ...\n" (intercalate "." path) >> hFlush stdout- withLogic y $ do- initEnv <- initEnv y m- check initEnv initEnv [] 1+verifyModel :: FilePath -> String -> Int -> Model -> IO ()+verifyModel y format maxK m = do+ printf format (intercalate "." path) >> hFlush stdout+ env0 <- initEnv y m+ execStateT (check env0 1) env0+ return () where [path] = [ path | Assert _ path _ <- actions m ]- check :: Env -> Env -> [ExpY] -> Int -> IO ()- check _ _ _ k | k > maxK = printf "inconclusive: unable to proved step up to max k = %d\n" maxK- check initEnv env asserts k = do- (env, assert) <- transition y m env- resultBasis <- checkBasis y m initEnv (assert : asserts)+ check :: Env -> Int -> Y ()+ check _ k | k > maxK = liftIO $ printf "inconclusive: unable to proved step up to max k = %d\n" maxK+ check env0 k = do+ transition m+ resultBasis <- checkBasis m env0 case resultBasis of- Fail -> printf "FAILED: disproved basis in k = %d\n" k+ Fail -> liftIO $ printf "FAILED: disproved basis in k = %d\n" k Pass -> do- resultStep <- checkStep y assert+ resultStep <- checkStep case resultStep of- Fail -> withLogic y $ check initEnv env (assert : asserts) (k + 1)- Pass -> printf "passed: proved step in k = %d\n" k+ Fail -> check env0 (k + 1)+ Pass -> liftIO $ printf "passed: proved step in k = %d\n" k data Result = Pass | Fail -- | Check induction step.-checkStep :: YicesIPC -> ExpY -> IO Result-checkStep y assert = do- r <- withLogic y $ do- runCmds y [ASSERT $ NOT assert]- checkLogic y+checkStep :: Y Result+checkStep = do+ Env y _ _ cmds asserts <- get+ r <- liftIO $ quickCheckY y [] $ reverse $ [ASSERT $ NOT $ head asserts] ++ cmds return $ result r -- | Check induction basis.-checkBasis :: YicesIPC -> Model -> Env -> [ExpY] -> IO Result-checkBasis y m env asserts = do- r <- withLogic y $ do- runCmds y [ ASSERT $ VarE (getVar env (State a)) := exprConst t c | a@(VS _ t c _) <- variables m ]- runCmds y [ASSERT $ NOT $ AND asserts]- checkLogic y+checkBasis :: Model -> Env -> Y Result+checkBasis m env0 = do+ Env y _ _ cmds asserts <- get+ r <- liftIO $ quickCheckY y [] $ reverse $ [ASSERT $ NOT $ AND asserts] ++ [ ASSERT $ VarE (getVar' env0 (State a)) := exprConst t c | a@(VS _ t c _) <- variables m ] ++ cmds return $ result r result :: ResY -> Result result a = case a of Sat _ -> Fail UnSat _ -> Pass- InCon _ -> Pass+ _ -> error $ "unexpected yices results: " ++ show a --- | Does operation in a new stack.-withLogic :: YicesIPC -> IO a -> IO a-withLogic y a = do- runCmds y [PUSH]- a <- a- runCmds y [POP]- return a -- | Transition relation. Returns assertion.-transition :: YicesIPC -> Model -> Env -> IO (Env, ExpY) -- (new env, assertion)-transition y m env = do- (env', assert) <- foldM (action y) (env, LitB True) (actions m)- --runCmds y [ ASSERT (VarE (getVar env $ State a) := VarE (getVar env' $ State a)) | a <- variables m ]- return (env', assert)+transition :: Model -> Y ()+transition m = mapM_ action $ actions m -action :: YicesIPC -> (Env, ExpY) -> Action -> IO (Env, ExpY)-action y (env, assert) a = case a of+action :: Action -> Y ()+action a = case a of Assign v e -> do- e <- expr y env (typeOf v) e- env <- addVar y env v- runCmds y [ASSERT $ VarE (getVar env v) := e]- return (env, assert)+ e <- expr (typeOf v) e+ v <- addVar v+ Env y i table cmds asserts <- get+ put $ Env y i table (ASSERT (VarE v := e) : cmds) asserts Assert a _ _ -> do- a <- expr y env Bool a- return (env, AND [assert, a])+ a <- expr Bool a+ Env y i table cmds asserts <- get+ put $ Env y i table cmds (a : asserts) Assume a _ _ -> do- a <- expr y env Bool a- runCmds y [ASSERT a]- return (env, assert)--expr :: YicesIPC -> Env -> Type -> E -> IO ExpY-expr y env t a = case a of- Var a@(Volatile _ _ _) -> do- env <- addVar y env a- return $ VarE $ getVar env a- Var a -> return $ VarE $ getVar env a+ a <- expr Bool a+ Env y i table cmds asserts <- get+ put $ Env y i table (ASSERT a : cmds) asserts +expr :: Type -> E -> Y ExpY+expr t a = case a of+ Var a@(Volatile _ _ _) -> addVar a >>= return . VarE+ Var a -> getVar a >>= return . VarE Const a -> return $ exprConst t a-- Not a _ -> do- a <- expr y env Bool a- return $ NOT a+ Not a _ -> expr Bool a >>= return . NOT And a b _ -> do- a <- expr y env Bool a- b <- expr y env Bool b+ a <- expr Bool a+ b <- expr Bool b return $ AND [a, b] Or a b _ -> do- a <- expr y env Bool a- b <- expr y env Bool b+ a <- expr Bool a+ b <- expr Bool b return $ OR [a, b] Mul a b _ -> do- a <- expr y env t a- b <- expr y env t b+ a <- expr t a+ b <- expr t b return $ a :*: b Div a b _ -> do- a <- expr y env t a- b <- expr y env t b+ a <- expr t a+ b <- expr t b return $ op a b where op = case t of@@ -148,37 +127,37 @@ _ -> (:/:) Mod a b _ -> do- a <- expr y env t a- b <- expr y env t b+ a <- expr t a+ b <- expr t b return $ MOD a b Add a b _ -> do- a <- expr y env t a- b <- expr y env t b+ a <- expr t a+ b <- expr t b return $ a :+: b Sub a b _ -> do- a <- expr y env t a- b <- expr y env t b+ a <- expr t a+ b <- expr t b return $ a :-: b Lt a b n -> do let t' = unify n (typeOf a) (typeOf b)- a <- expr y env t' a- b <- expr y env t' b+ a <- expr t' a+ b <- expr t' b return $ a :< b Eq a b n -> do let t' = unify n (typeOf a) (typeOf b)- a <- expr y env t' a- b <- expr y env t' b+ a <- expr t' a+ b <- expr t' b return $ a := b Mux a b c n -> do let t' = unify n (typeOf b) (typeOf c)- a <- expr y env Bool a- b <- expr y env t' b- c <- expr y env t' c+ a <- expr Bool a+ b <- expr t' b+ c <- expr t' c return $ IF a b c exprConst :: Type -> Const -> ExpY@@ -190,23 +169,27 @@ +type Y = StateT Env IO -data Env = Env NextId [(V, String)] -- Env nextId table+data Env = Env FilePath Int [(V, String)] [CmdY] [ExpY] -- Env nextId table cmds assertions -initEnv :: YicesIPC -> Model -> IO Env-initEnv y m = do- nid <- newNextId- foldM (addVar y) (Env nid []) $ map State $ variables m+initEnv :: FilePath -> Model -> IO Env+initEnv y m = execStateT (mapM_ addVar $ map State $ variables m) (Env y 0 [] [] []) -addVar :: YicesIPC -> Env -> V -> IO Env-addVar y (Env nid table) v = do- i <- nextId nid+addVar :: V -> Y String+addVar v = do+ Env y i table cmds asserts <- get let name = printf "n%d" i- runCmds y [DEFINE (name, VarT $ typeY v) Nothing]- return $ Env nid $ replace (v, name) table+ put $ Env y (i + 1) (replace (v, name) table) (DEFINE (name, VarT $ typeY v) Nothing : cmds) asserts+ return name -getVar :: Env -> V -> String-getVar (Env _ table) v = case lookup v table of+getVar :: V -> Y String+getVar v = do+ env <- get+ return $ getVar' env v++getVar' :: Env -> V -> String+getVar' (Env _ _ table _ _) v = case lookup v table of Just a -> a Nothing -> error $ "Verify.getVar: variable not found: " ++ show v ++ " in " ++ show (fst $ unzip table) @@ -216,44 +199,11 @@ | otherwise = (a', b') : replace (a, b) c ---- typeY :: TypeOf a => a -> String typeY a = case typeOf a of Void -> error "Verify.typeY: void time" Bool -> "bool" Integer _ -> "int" Rational _ -> "real"----newtype NextId = NextId (IORef Int)--newNextId :: IO NextId-newNextId = newIORef 0 >>= (return . NextId)--nextId :: NextId -> IO Int-nextId (NextId a) = do- i <- readIORef a- writeIORef a $ i + 1- return i---verbose :: Bool-verbose = False--runCmds :: YicesIPC -> [CmdY] -> IO ()-runCmds y cmds = do- when verbose $ mapM_ (putStrLn . show) cmds- runCmdsY' y cmds--checkLogic :: YicesIPC -> IO ResY-checkLogic y = do- when verbose $ do- putStrLn "(check)"- hFlush stdout- checkY y