afv 0.0.3 → 0.0.4
raw patch · 6 files changed
+225/−153 lines, 6 files
Files
- RELEASE-NOTES +14/−9
- afv.cabal +1/−1
- src/AFV.hs +1/−1
- src/Compile.hs +57/−68
- src/Model.hs +19/−10
- src/Verify.hs +133/−64
RELEASE-NOTES view
@@ -1,20 +1,25 @@-afv 0.0.0 01/12/10+afv 0.0.4 01/21/10 -- Initial release.+- Moved branches into model.+- Improved counter example generation. -afv 0.0.1 01/14/10+afv 0.0.3 01/19/10 -- Checks for duplicate top-level names.-- Uses yices new 'quickCheckY'.-- Fixed bug affecting 'assume'.+- Bug fix to --yices command option.+- Added basic counter example generation. afv 0.0.2 01/17/10 - Support for function arguments. Still no support for return values. - Stronger type checking. -afv 0.0.3 01/19/10+afv 0.0.1 01/14/10 -- Bug fix to --yices command option.-- Added basic counter example generation.+- Checks for duplicate top-level names.+- Uses yices new 'quickCheckY'.+- Fixed bug affecting 'assume'.++afv 0.0.0 01/12/10++- Initial release.
afv.cabal view
@@ -1,5 +1,5 @@ name: afv-version: 0.0.3+version: 0.0.4 category: Formal Methods
src/AFV.hs view
@@ -8,7 +8,7 @@ import Parse import Verify -version = "0.0.3"+version = "0.0.4" main :: IO () main = do
src/Compile.hs view
@@ -24,7 +24,7 @@ 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+ then error $ "duplicate top-level names found (hiding names with static is not supported): " ++ show duplicateNames --XXX Should not allow top level static decls. An improper name reference in one file could reference a static variable in another. else CCompound [] (vars ++ funcs ++ [CBlockStmt call]) none where items = [ a | CTranslUnit items _ <- units, a <- items ]@@ -47,7 +47,6 @@ data MDB = MDB { nextId' :: Int , stack :: [Ident]- , enabled :: E , model :: Model } @@ -55,7 +54,6 @@ initMDB = MDB { nextId' = 0 , stack = []- , enabled = true , model = Model { variables = [], actions = [] } } @@ -90,17 +88,17 @@ m = [ a | EnvFunction n a <- values env, n == name ] -- | Creates a branch.-branch :: Position -> E -> M a -> M a -> M (a, a)+branch :: Position -> V -> M a -> M a -> M (a, a) branch n a onTrue onFalse = do- a <- latchBranch n a m1 <- get- put m1 { enabled = And (enabled m1) a n }+ put m1 { model = (model m1) { actions = [] } } r1 <- onTrue m2 <- get- put m2 { enabled = And (enabled m1) (Not a n) n }+ put m1 { model = (model m2) { actions = [] } } r2 <- onFalse m3 <- get- put m3 { enabled = enabled m1 }+ put m3 { model = (model m3) { actions = actions $ model m1 } }+ newAction $ Branch a (reverse $ actions $ model m2) (reverse $ actions $ model m3) n return (r1, r2) -- | Push an identifier onto the call stack, do something, then pop it off.@@ -113,11 +111,11 @@ put m { stack = tail $ stack m } return a -callPath :: M ([String], Position)+callPath :: M String callPath = do m <- get let s = stack m- return ([ n | Ident n _ _ <- reverse s ], posOf $ head s)+ return $ intercalate "." [ n | Ident n _ _ <- reverse $ tail s ] -- | The initial environment defines the assert and assume functions. initEnv :: Env@@ -128,18 +126,18 @@ ] } where- assert a = do- (s, n) <- callPath- m <- get- let x = imply (enabled m) (head a) n- newAction $ Assert x s- return x- assume a = do- (s, n) <- callPath- m <- get- let x = imply (enabled m) (head a) n- newAction $ Assume x s- return x+ assert a' = do+ let a = head a'+ s <- callPath+ x <- latch (posOf a) a+ newAction $ Assert x s (posOf a)+ return $ Var x+ assume a' = do+ let a = head a'+ s <- callPath+ x <- latch (posOf a) a+ newAction $ Assume x s (posOf a)+ return $ Var x -- | Adds new action. newAction :: Action -> M ()@@ -177,7 +175,7 @@ f (a:b) = callStack a $ f b CIf a b Nothing n -> evalStat env $ CIf a b (Just $ CCompound [] [] n) n CIf a b (Just c) n -> do- a <- evalExpr env a+ a <- evalExpr env a >>= latch (posOf n) branch (posOf n) a (evalStat env b) (evalStat env c) return () _ -> notSupported a "statement"@@ -189,13 +187,13 @@ CNestedFunDef a -> evalFunc env a evalExpr :: Env -> CExpr -> M E-evalExpr env a = latch (posOf a) =<< case a of+evalExpr env a = case a of CAssign op a b n -> case op of CAssignOp -> do a' <- evalExpr env a b' <- evalExpr env b case a' of- Var v -> assign False (posOf n) v b' >> return a'+ Var v -> assign (posOf n) v b' >> return a' _ -> unexpected a "non variable in left hand of assignment" CMulAssOp -> f CMulOp CDivAssOp -> f CDivOp@@ -211,12 +209,12 @@ f :: CBinaryOp -> M E f op = evalExpr env (CAssign CAssignOp a (CBinary op a b n) n) CCond a (Just b) c n -> do- a <- evalExpr env a+ a <- evalExpr env a >>= latch (posOf a) (b, c) <- branch (posOf n) a (evalExpr env b) (evalExpr env c)- return $ Mux a b c $ posOf n+ return $ Mux (Var a) b c $ posOf n CCond a Nothing b n -> do- a <- evalExpr env a- (a, b) <- branch (posOf n) a (return a) (evalExpr env b)+ a <- evalExpr env a >>= latch (posOf a)+ (a, b) <- branch (posOf n) a (return $ Var a) (evalExpr env b) return $ Mux a a b $ posOf n CBinary op a b n -> case op of CMulOp -> f Mul@@ -236,12 +234,12 @@ CXorOp -> notSupported a "(^)" COrOp -> notSupported a "(|)" CLndOp -> do- a <- evalExpr env a- (b, a) <- branch n' a (evalExpr env b) (return a)+ a <- evalExpr env a >>= latch (posOf a)+ (b, a) <- branch n' a (evalExpr env b) (return $ Var a) return $ Mux a b a n' CLorOp -> do- a <- evalExpr env a- (a, b) <- branch n' a (return a) (evalExpr env b)+ a <- evalExpr env a >>= latch (posOf a)+ (a, b) <- branch n' a (return $ Var a) (evalExpr env b) return $ Mux a a b n' where n' = posOf n@@ -255,19 +253,19 @@ a <- evalExpr env a case (op, a) of (CPreIncOp, Var a) -> do- assign False p a $ Add (Var a) one p+ assign p a $ Add (Var a) one p return $ Var a (CPreDecOp, Var a) -> do- assign False p a $ Sub (Var a) one p+ assign p a $ Sub (Var a) one p return $ Var a (CPostIncOp, Var a) -> do b <- latch p $ Var a- assign False p a $ Add (Var a) one p- return b+ assign p a $ Add (Var a) one p+ return $ Var b (CPostDecOp, Var a) -> do b <- latch p $ Var a- assign False p a $ Sub (Var a) one p- return b+ assign p a $ Sub (Var a) one p+ return $ Var b (CPlusOp, a) -> return a (CMinOp, a) -> return $ Sub zero a p (CNegOp, a) -> return $ Not a p@@ -333,7 +331,7 @@ else do i <- nextId return $ Local name typ i (posOf e')- assign True (posOf e') v e+ declare (posOf e') v e addVar env v _ -> notSupported i "variable declaration" _ -> notSupported d "arrays, pointers, or functional pointers (So what good is this tool anyway?)"@@ -358,7 +356,7 @@ else do i <- nextId let v = Local name typ i (posOf n)- assign True (posOf n) v a+ declare (posOf n) v a addVar env v funcArgs :: CDecl -> [(Ident, (TypeInfo, Type))]@@ -371,39 +369,30 @@ +-- | Declares a new variable with a value.+declare :: Position -> V -> E -> M ()+declare n v a = case v of+ Volatile _ _ _ -> return ()+ _ -> newAction $ Declare v a n --- | Assgins a value to a variable.-assign :: Bool -> Position -> V -> E -> M ()-assign decl n v a = case v of+-- | Assigns a value to an existing variable.+assign :: Position -> V -> E -> M ()+assign n v a = case v of Volatile _ _ _ -> return ()- _ -> do- m <- get- newAction $ Assign v $ if decl then a else Mux (enabled m) a (Var v) n --XXX Is this correct for local and tmp variables?+ _ -> newAction $ Assign v a n --- | Latch a value at a point in time and return the expression of the latch variable.-latch :: Position -> E -> M E-latch _ (Var a) = return (Var a)-latch _ (Const a) = return (Const a)+-- | Latch a value at a point in time.+latch :: Position -> E -> M V -- XXX When is it appropriate to latch and when not?+--latch _ (Var a) = return a latch n a = do i <- nextId let v = Tmp (typeOf a) i n- assign True n v a- return $ Var v---- | Latch a value for a branch point.-latchBranch :: Position -> E -> M E-latchBranch n a = do- i <- nextId- let v = Branch (typeOf a) i n- assign True n v a- return $ Var v---- | Logical implication. Assumes Bool inputs.-imply :: E -> E -> Position -> E-imply a b n = Or (Not a n) b n---+ case typeOf a of+ Integer Nothing -> error "Compile.latch1"+ Rational Nothing -> error "Compile.latch2"+ _ -> do+ declare n v a+ return v
src/Model.hs view
@@ -94,7 +94,6 @@ | Volatile String Type Position | Local String Type Int Position | Tmp Type Int Position- | Branch Type Int Position deriving (Show, Eq) instance TypeOf V where@@ -103,7 +102,6 @@ Volatile _ a _ -> a Local _ a _ _ -> a Tmp a _ _ -> a- Branch a _ _ -> a instance Pos V where posOf a = case a of@@ -111,7 +109,6 @@ Volatile _ _ n -> n Local _ _ _ n -> n Tmp _ _ n -> n- Branch _ _ n -> n -- | Expressions. data E@@ -156,7 +153,7 @@ Const a -> typeOf a Not a _ -> unify' Bool (typeOf a) And a b _ -> unify' Bool $ unify' (typeOf a) (typeOf b)- Or a b _ -> unify' (typeOf a) (typeOf b)+ Or a b _ -> unify' Bool $ unify' (typeOf a) (typeOf b) Mul a b _ -> unify' (typeOf a) (typeOf b) Div a b _ -> unify' (typeOf a) (typeOf b) Mod a b _ -> unify' (typeOf a) (typeOf b)@@ -195,9 +192,11 @@ typeCheckAction :: Action -> Action typeCheckAction a = case a of- Assign v a -> seq (unify a (typeOf v) (typeOf a)) $ Assign v a- Assert a n -> seq (unify a Bool (typeOf a)) $ Assert a n- Assume a n -> seq (unify a Bool (typeOf a)) $ Assume a n+ Declare v a p -> seq (unify a (typeOf v) (typeOf a)) $ Declare v a p+ Assign v a p -> seq (unify a (typeOf v) (typeOf a)) $ Assign v a p+ Assert a n p -> seq (unify a Bool (typeOf a)) $ Assert a n p+ Assume a n p -> seq (unify a Bool (typeOf a)) $ Assume a n p+ Branch a b c p -> seq (unify a Bool (typeOf a)) $ Branch a (map typeCheckAction b) (map typeCheckAction c) p true :: E true = Const $ CBool True nopos@@ -208,10 +207,20 @@ instance Pos Position where posOf = id data Action- = Assign V E- | Assert E [String]- | Assume E [String]+ = Declare V E Position+ | Assign V E Position+ | Assert V String Position+ | Assume V String Position+ | Branch V [Action] [Action] Position deriving (Show, Eq)++instance Pos Action where+ posOf a = case a of+ Declare _ _ a -> a+ Assign _ _ a -> a+ Assert _ _ a -> a+ Assume _ _ a -> a+ Branch _ _ _ a -> a data Model = Model { variables :: [VS]
src/Verify.hs view
@@ -1,7 +1,7 @@ module Verify (verify) where import Control.Monad.State hiding (State)-import Data.List+import Language.C.Data.Position import Math.SMT.Yices.Pipe import Math.SMT.Yices.Syntax import System.IO@@ -17,43 +17,53 @@ mapM_ (verifyModel yices format maxK) models where model = typeCheckModel m- assertions = [ a | a@(Assert _ _) <- actions model ]- models = map (trimModel . trimAssertions model) assertions- format = "verifying %-" ++ show (maximum [ length (intercalate "." n) | (Assert _ n) <- actions model ]) ++ "s "+ models = [ (name, trimModel model { actions = actions }) | (name, actions) <- trimAssertions (actions model) ]+ format = "verifying %-" ++ show (maximum [ length n | (n, _) <- models ]) ++ "s " -- | Remove all assertions except one.-trimAssertions :: Model -> Action -> Model-trimAssertions m a = m { actions = filter keep $ actions m }- where- keep b@(Assert _ _) = a == b- keep _ = True+trimAssertions :: [Action] -> [(String, [Action])]+trimAssertions [] = []+trimAssertions (a:b) = case a of+ Assert _ n _ -> (n, a : removeAssertions b) : trimAssertions b+ Branch c t f p -> [ (name, Branch c actions (removeAssertions f) p : removeAssertions b) | (name, actions) <- trimAssertions t ]+ ++ [ (name, Branch c (removeAssertions t) actions p : removeAssertions b) | (name, actions) <- trimAssertions f ]+ ++ [ (name, Branch c (removeAssertions t) (removeAssertions f) p : actions) | (name, actions) <- trimAssertions b ]+ _ -> [ (name, a : actions) | (name, actions) <- trimAssertions b ] +-- | Remove all assertions.+removeAssertions :: [Action] -> [Action]+removeAssertions [] = []+removeAssertions (a:b) = case a of+ Assert _ _ _ -> removeAssertions b+ Branch c t f p -> Branch c (removeAssertions t) (removeAssertions f) p : removeAssertions b+ _ -> a : removeAssertions b+ -- | Trim all unneeded stuff from a model. trimModel :: Model -> Model trimModel = id --XXX -- | Verify a trimmed model.-verifyModel :: FilePath -> String -> Int -> Model -> IO ()-verifyModel y format maxK m = do- printf format name >> hFlush stdout+verifyModel :: FilePath -> String -> Int -> (String, Model) -> IO ()+verifyModel y format maxK (name, m) = do+ printf format name+ hFlush stdout env0 <- initEnv y m execStateT (check env0 1) env0 return () where- name = intercalate "." $ head [ path | Assert _ path <- actions m ] check :: Env -> Int -> Y () check env0 k = do transition m resultBasis <- checkBasis m env0 case resultBasis of- Fail a -> liftIO (printf "FAILED: disproved basis in k = %d (see trace)\n" k) >> trace name a- Problem -> return ()+ Fail a -> liftIO (printf "FAILED: disproved basis in k = %d (see trace)\n" k) >> writeTrace name a+ Problem -> error "Verify.check1" Pass -> do resultStep <- checkStep case resultStep of Fail a | k < maxK -> check env0 (k + 1)- | otherwise -> liftIO (printf "inconclusive: unable to proved step up to max k = %d (see trace)\n" k) >> trace name a- Problem -> return ()+ | otherwise -> liftIO (printf "inconclusive: unable to proved step up to max k = %d (see trace)\n" k) >> writeTrace name a+ Problem -> error "Verify.check2" Pass -> liftIO $ printf "passed: proved step in k = %d\n" k data Result = Pass | Fail [ExpY] | Problem@@ -61,15 +71,17 @@ -- | Check induction step. checkStep :: Y Result checkStep = do- Env y _ _ cmds asserts <- get- r <- liftIO $ quickCheckY y [] $ reverse $ [ASSERT $ NOT $ head asserts] ++ cmds+ env <- get+ let cmds' = reverse $ [CHECK] ++ [ASSERT $ NOT $ head $ asserts env] ++ cmds env+ r <- liftIO $ quickCheckY' (yices env) [] $ cmds' return $ result r -- | Check induction basis. 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+ env <- get+ let cmds' = reverse $ [CHECK] ++ [ASSERT $ NOT $ AND $ asserts env] ++ [ ASSERT $ VarE (getVar' env0 (State a)) := exprConst t c | a@(VS _ t c _) <- variables m ] ++ cmds env+ r <- liftIO $ quickCheckY' (yices env) [] cmds' return $ result r result :: ResY -> Result@@ -82,24 +94,52 @@ -- | Transition relation. Returns assertion. transition :: Model -> Y ()-transition m = mapM_ action $ actions m+transition m = mapM_ (action $ LitB True) $ actions m -action :: Action -> Y ()-action a = case a of- Assign v e -> do+assign :: Position -> V -> String -> Y ()+assign p v n = do+ env <- get+ case v of+ State (VS name _ _ _) -> put env { trace = Assign' p name n : trace env }+ Local name _ _ _ -> put env { trace = Assign' p name n : trace env }+ _ -> return ()+ +action :: ExpY -> Action -> Y ()+action enabled a = case a of+ Declare v e p -> do 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 Bool a- Env y i table cmds asserts <- get- put $ Env y i table cmds (a : asserts)- Assume a _ -> do- a <- expr Bool a- Env y i table cmds asserts <- get- put $ Env y i table (ASSERT a : cmds) asserts+ v' <- addVar v+ env <- get+ put env { cmds = ASSERT (VarE v' := e) : cmds env }+ assign p v v'+ Assign v e p -> do+ e <- expr (typeOf v) e+ vLast <- getVar v+ v' <- addVar v+ env <- get+ put env { cmds = ASSERT (VarE v' := IF enabled e (VarE vLast)) : cmds env }+ assign p v v'+ Assert a n p -> do+ a <- getVar a+ env <- get+ put env { asserts = (enabled :=> VarE a) : asserts env, trace = Assert' p n a : trace env }+ Assume a _ _ -> do+ a <- getVar a+ env <- get+ put env { cmds = ASSERT (enabled :=> VarE a) : cmds env }+ Branch a onTrue onFalse p -> do+ a' <- getVar a+ env0 <- get+ put env0 { trace = [] }+ mapM_ (action $ AND [enabled, VarE a']) onTrue+ env1 <- get+ put env1 { trace = [] }+ mapM_ (action $ AND [enabled, NOT $ VarE a']) onFalse+ env2 <- get+ put env2 { trace = Branch' p a' (reverse $ trace env1) (reverse $ trace env2) : trace env0 }+ + expr :: Type -> E -> Y ExpY expr t a = case a of Var a@(Volatile _ _ _) -> addVar a >>= return . VarE@@ -169,26 +209,45 @@ Deref _ _ -> notSupported a "indirection operator" exprConst :: Type -> Const -> ExpY-exprConst t a = case a of - CBool a _ -> LitB a- CInteger a _ | t == Bool -> LitB $ a /= 0- | otherwise -> LitI a- CRational a _ -> LitR a+exprConst t a = case t of+ --Integer Nothing -> error "Verify.exprConst1"+ --Rational Nothing -> error "Verify.exprConst2"+ _ -> case a of + CBool a _ -> LitB a+ CInteger a _ | t == Bool -> LitB $ a /= 0+ | otherwise -> LitI a+ CRational a _ -> LitR a type Y = StateT Env IO -data Env = Env FilePath Int [(V, String)] [CmdY] [ExpY] -- Env yices nextId table cmds assertions+data Env = Env+ { yices :: FilePath+ , nextId :: Int+ , vars :: [(V, String)]+ , cmds :: [CmdY]+ , asserts :: [ExpY]+ , trace :: [Trace]+ }+ +data Trace = Assign' Position String String | Assert' Position String String | Branch' Position String [Trace] [Trace] initEnv :: FilePath -> Model -> IO Env-initEnv y m = execStateT (mapM_ addVar $ map State $ variables m) (Env y 0 [] [] [])+initEnv y m = execStateT (mapM_ f $ variables m) (Env y 0 [] [] [] [])+ where+ f :: VS -> Y ()+ f a = do+ n <- addVar v+ assign (posOf v) v n+ where+ v = State a addVar :: V -> Y String addVar v = do- Env y i table cmds asserts <- get- let name = printf "n%d" i- put $ Env y (i + 1) ((v, name) : table) (DEFINE (name, VarT $ typeY v) Nothing : cmds) asserts+ env <- get+ let name = printf "n%d" $ nextId env+ put env { nextId = nextId env + 1, vars = (v, name) : vars env, cmds = DEFINE (name, VarT $ typeY v) Nothing : cmds env } return name getVar :: V -> Y String@@ -197,9 +256,9 @@ return $ getVar' env v getVar' :: Env -> V -> String-getVar' (Env _ _ table _ _) v = case lookup v table of+getVar' env v = case lookup v $ vars env of Just a -> a- Nothing -> error $ "Verify.getVar: variable not found: " ++ show v ++ " in " ++ show (fst $ unzip table)+ Nothing -> error $ "Verify.getVar: variable not found: " ++ show v ++ " in " ++ show (vars env) typeY :: TypeOf a => a -> String typeY a = case typeOf a of@@ -209,21 +268,31 @@ Integer _ -> "int" Rational _ -> "real" -trace :: String -> [ExpY] -> Y ()-trace name vars = do- Env _ _ table _ _ <- get- liftIO $ writeFile (name ++ ".trace") $ concatMap (traceVar vars) $ reverse table--traceVar :: [ExpY] -> (V, String) -> String-traceVar vars (a, n) = case a of- State (VS name _ _ p) -> "global state " ++ name ++ "(" ++ position p ++ ") = " ++ value ++ ";\n"- Branch _ _ p -> "branch (" ++ position p ++ ") = " ++ value ++ ";\n"- _ -> ""+writeTrace :: String -> [ExpY] -> Y ()+writeTrace name table' = do+ env <- get+ let format p = printf ("%-" ++ show (maximum $ map maxPosWidth $ trace env) ++ "s ") $ position p+ liftIO $ writeFile (name ++ ".trace") $ concatMap (f format) $ reverse $ trace env where- value = case lookup n table of- Nothing -> error $ "Variable not found: " ++ show a- Just a -> a- table = [ (n, show v) | VarE n := LitB v <- vars ]- ++ [ (n, show v) | VarE n := LitI v <- vars ]- ++ [ (n, show v) | VarE n := LitR v <- vars ]+ 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 :: (Position -> String) -> Trace -> String+ f format a = case a of+ Assign' p name var -> case lookup var table of+ Nothing -> ""+ Just value -> format p ++ name ++ " = " ++ value ++ ";\n"+ Assert' p name var -> case lookup var table of+ Just "true" -> format p ++ "assertion passed: " ++ name ++ "\n"+ Just "false" -> format p ++ "assertion FAILED: " ++ name ++ "\n"+ _ -> ""+ Branch' p cond onTrue onFalse -> case lookup cond table of+ Just "true" -> format p ++ "branch true\n" ++ concatMap (f format) onTrue+ Just "false" -> format p ++ "branch false\n" ++ concatMap (f format) onFalse+ _ -> "" + maxPosWidth :: Trace -> Int+ maxPosWidth a = case a of+ Assign' p _ _ -> length $ position p+ Assert' p _ _ -> length $ position p+ Branch' p _ a b -> maximum $ [length (position p)] ++ map maxPosWidth a ++ map maxPosWidth b