diff --git a/RELEASE-NOTES b/RELEASE-NOTES --- a/RELEASE-NOTES +++ b/RELEASE-NOTES @@ -13,3 +13,8 @@ - Support for function arguments. Still no support for return values. - Stronger type checking. +afv 0.0.3 01/19/10 + +- Bug fix to --yices command option. +- Added basic counter example generation. + diff --git a/afv.cabal b/afv.cabal --- a/afv.cabal +++ b/afv.cabal @@ -1,5 +1,5 @@ name: afv -version: 0.0.2 +version: 0.0.3 category: Formal Methods diff --git a/src/AFV.hs b/src/AFV.hs --- a/src/AFV.hs +++ b/src/AFV.hs @@ -8,7 +8,7 @@ import Parse import Verify -version = "0.0.2" +version = "0.0.3" main :: IO () main = do @@ -39,7 +39,7 @@ parseArgs :: Args -> [String] -> Args parseArgs a b = case b of [] -> a - arg : args | isYices -> parseArgs a { gcc = pathYices } args + arg : args | isYices -> parseArgs a { yices = pathYices } args | isGCC -> parseArgs a { gcc = pathGCC } args | isInclude -> parseArgs a { includes = includes a ++ [drop 2 arg] } args | isDefine -> parseArgs a { defines = defines a ++ [(name, value)] } args diff --git a/src/Compile.hs b/src/Compile.hs --- a/src/Compile.hs +++ b/src/Compile.hs @@ -92,6 +92,7 @@ -- | Creates a branch. branch :: Position -> E -> 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 } r1 <- onTrue @@ -160,7 +161,7 @@ State (VS a _ _ _) -> a Volatile a _ _ -> a Local a _ _ _ -> a - Tmp _ _ _ -> error "Compile.addVar: should not call addVar with Tmp" + _ -> error "Compile.addVar: should not call addVar with Tmp or Branch" @@ -386,6 +387,14 @@ 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 diff --git a/src/Model.hs b/src/Model.hs --- a/src/Model.hs +++ b/src/Model.hs @@ -91,9 +91,10 @@ -- | Variables. data V = State VS - | Volatile String Type Position - | Local String Type Int Position - | Tmp Type Int Position + | Volatile String Type Position + | Local String Type Int Position + | Tmp Type Int Position + | Branch Type Int Position deriving (Show, Eq) instance TypeOf V where @@ -102,6 +103,7 @@ Volatile _ a _ -> a Local _ a _ _ -> a Tmp a _ _ -> a + Branch a _ _ -> a instance Pos V where posOf a = case a of @@ -109,6 +111,7 @@ Volatile _ _ n -> n Local _ _ _ n -> n Tmp _ _ n -> n + Branch _ _ n -> n -- | Expressions. data E diff --git a/src/Verify.hs b/src/Verify.hs --- a/src/Verify.hs +++ b/src/Verify.hs @@ -35,28 +35,28 @@ -- | Verify a trimmed model. verifyModel :: FilePath -> String -> Int -> Model -> IO () verifyModel y format maxK m = do - printf format (intercalate "." path) >> hFlush stdout + printf format name >> hFlush stdout env0 <- initEnv y m execStateT (check env0 1) env0 return () where - [path] = [ path | Assert _ path <- actions m ] + name = intercalate "." $ head [ path | Assert _ path <- actions m ] 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 -> liftIO $ printf "FAILED: disproved basis in k = %d\n" k + Fail a -> liftIO (printf "FAILED: disproved basis in k = %d (see trace)\n" k) >> trace name a Problem -> return () Pass -> do resultStep <- checkStep case resultStep of - Fail -> check env0 (k + 1) + 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 () Pass -> liftIO $ printf "passed: proved step in k = %d\n" k -data Result = Pass | Fail | Problem +data Result = Pass | Fail [ExpY] | Problem -- | Check induction step. checkStep :: Y Result @@ -74,7 +74,7 @@ result :: ResY -> Result result a = case a of - Sat _ -> Fail + Sat a -> Fail a UnSat _ -> Pass InCon _ -> Problem _ -> error $ "unexpected yices results: " ++ show a @@ -179,7 +179,7 @@ type Y = StateT Env IO -data Env = Env FilePath Int [(V, String)] [CmdY] [ExpY] -- Env nextId table cmds assertions +data Env = Env FilePath Int [(V, String)] [CmdY] [ExpY] -- Env yices nextId table cmds assertions initEnv :: FilePath -> Model -> IO Env initEnv y m = execStateT (mapM_ addVar $ map State $ variables m) (Env y 0 [] [] []) @@ -188,7 +188,7 @@ addVar v = do Env y i table cmds asserts <- get let name = printf "n%d" i - put $ Env y (i + 1) (replace (v, name) table) (DEFINE (name, VarT $ typeY v) Nothing : cmds) asserts + put $ Env y (i + 1) ((v, name) : table) (DEFINE (name, VarT $ typeY v) Nothing : cmds) asserts return name getVar :: V -> Y String @@ -201,12 +201,6 @@ Just a -> a Nothing -> error $ "Verify.getVar: variable not found: " ++ show v ++ " in " ++ show (fst $ unzip table) -replace :: Eq a => (a, b) -> [(a, b)] -> [(a, b)] -replace a [] = [a] -replace (a, b) ((a', b') : c) | a == a' = (a, b) : c - | otherwise = (a', b') : replace (a, b) c - - typeY :: TypeOf a => a -> String typeY a = case typeOf a of Void -> error "Verify.typeY: void" @@ -215,4 +209,21 @@ 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" + _ -> "" + 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 ]