afv 0.0.2 → 0.0.3

raw patch · 6 files changed

+50/−22 lines, 6 files

Files

RELEASE-NOTES +5/−0
afv.cabal +1/−1
src/AFV.hs +2/−2
src/Compile.hs +10/−1
src/Model.hs +6/−3
src/Verify.hs +26/−15

RELEASE-NOTES view

@@ -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.+

afv.cabal view

@@ -1,5 +1,5 @@ name:    afv-version: 0.0.2+version: 0.0.3  category: Formal Methods

src/AFV.hs view

@@ -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

src/Compile.hs view

@@ -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

src/Model.hs view

@@ -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

src/Verify.hs view

@@ -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 ]