packages feed

afv 0.0.4 → 0.1.0

raw patch · 6 files changed

+318/−234 lines, 6 files

Files

RELEASE-NOTES view
@@ -1,3 +1,10 @@+afv 0.1.0    01/24/10++- Moved functon calls and assignments to statement position only.+- Added checks for static top-level declarations, which are not supported.+- Checks start from 'main' function.  Automatically detects infinite loop.+- Disallows state modifying expressions.+ afv 0.0.4    01/21/10  - Moved branches into model.
afv.cabal view
@@ -1,5 +1,5 @@ name:    afv-version: 0.0.4+version: 0.1.0  category: Formal Methods
src/AFV.hs view
@@ -8,7 +8,7 @@ import Parse import Verify -version = "0.0.4"+version = "0.1.0"  main :: IO () main = do@@ -19,10 +19,10 @@           | elem a ["version", "-v", "--version"] -> putStrLn $ "afv " ++ version     ["example"] -> example     ["header"]  -> header-    ("verify":function:args) -> do+    ("verify":args) -> do       let a = parseArgs Args { yices = "yices", gcc = "gcc", k = 20, defines = [("AFV", "")], includes = ["."], inputs = [] } args       units <- sequence [ putStrLn ("parsing " ++ f ++ " ...") >> hFlush stdout >> parse (gcc a) (includes a) (defines a) f | f <- inputs a ]-      model <- compile function units+      model <- compile units       verify (yices a) (k a) model     _ -> help @@ -70,7 +70,7 @@ example = do   header   putStrLn "writing example design (example.c) ..."-  putStrLn "verify with:  afv verify example -k 15 example.c"+  putStrLn "verify with:  afv verify -k 15 example.c"   writeFile "example.c" $ unlines     [ "// Provides assert and assume functions."     , "#include \"afv.h\""@@ -114,6 +114,10 @@     , ""     , "}"     , ""+    , "void main() {"+    , "  while (1) example();"+    , "}"+    , ""     ]  @@ -128,17 +132,17 @@   , "  " ++ version   , ""   , "SYNOPSIS"-  , "  afv verify function-name [-k max-k] [--yices=path-to-yices] [--gcc=path-to-gcc] {-Idir} {-Dmacro[=def]} c-file {c-file}"+  , "  afv verify [-k max-k] [--yices=path-to-yices] [--gcc=path-to-gcc] {-Idir} {-Dmacro[=def]} c-file {c-file}"   , "  afv header"   , "  afv example"   , ""   , "DESCRIPTION"-  , "  Afv performs bounded model checking and k-induction on a repetitively called C function."+  , "  Afv performs bounded model checking and k-induction on C code with a signle infinite loop."   , "  Requires GCC for C preprocessing and the Yices SMT solver."   , ""   , "COMMANDS"-  , "  verify function-name [options] c-files ..."-  , "    Runs verification on the specified periodic function."+  , "  verify [options] c-files ..."+  , "    Runs verification."   , ""   , "    -k n          : Max k-induction depth."   , "    --yices=path  : Path to Yices solver."@@ -152,6 +156,6 @@   , ""   , "  example"   , "    Writes an example design (example.c).  Verify with:"-  , "      afv verify example -k 15 example.c"+  , "      afv verify -k 15 example.c"   , ""   ]
src/Compile.hs view
@@ -11,31 +11,35 @@ import Utils  -- | Compiles a program to a model for analysis.-compile :: String -> [CTranslUnit] -> IO Model-compile function units = do-  m <- execStateT (evalStat initEnv $ rewrite function units) initMDB-  return (model m) { actions = reverse $ actions (model m) }+compile :: [CTranslUnit] -> IO Model+compile units = do+  m <- execStateT (evalStat initEnv $ rewrite units) initMDB+  return (model m) { initActions = reverse $ initActions (model m), loopActions = reverse $ loopActions (model m) }  none :: NodeInfo none = internalNode  -- | 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+rewrite :: [CTranslUnit] -> CStat+rewrite 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  --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+    then error $ "duplicate top-level names found: " ++ intercalate ", " duplicateNames+    else if not $ null staticFuncDefs+      then notSupported (head staticFuncDefs) "top-level static declarations"+      else if not $ null staticVarDefs+        then notSupported (head staticVarDefs) "top-level static declarations"+        else CCompound [] (varDefs ++ funcDefs ++ [CBlockStmt call]) none   where   items = [ a | CTranslUnit items _ <- units, 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+  varDefs  = [ CBlockDecl a | CDeclExt a@(CDecl specs _ _) <- items, not $ isExtern $ fst $ typeInfo specs ]+  funcDefs = map CNestedFunDef $ sortFunctions [ a | CFDefExt a@(CFunDef specs _ _ _ _) <- items, not $ isExtern $ fst $ typeInfo specs ]   asms  = [ a | CAsmExt  a <- items ]   call :: CStat-  call = CExpr (Just $ CCall (CVar (Ident name 0 none) none) [] none) none-  duplicateNames = duplicates $ [ name | f <- funcDefs, let (_, (Ident name _ _), _, _) = functionInfo f ] ++ concat [ [ name | (Just (CDeclr (Just (Ident name _ _)) _ _ _ _), _, _) <- a ] | CDecl _ a _ <- varDefs ]+  call = CExpr (Just $ CCall (CVar (Ident "main" 0 none) none) [] none) none+  duplicateNames = duplicates $ [ name | CNestedFunDef f <- funcDefs, let (_, (Ident name _ _), _, _) = functionInfo f ] ++ concat [ [ name | (Just (CDeclr (Just (Ident name _ _)) _ _ _ _), _, _) <- a ] | CBlockDecl (CDecl _ a _) <- varDefs ]+  staticFuncDefs = [ a | CFDefExt a@(CFunDef specs _ _ _ _) <- items, isStatic $ fst $ typeInfo specs ]+  staticVarDefs  = [ a | CDeclExt a@(CDecl specs _ _) <- items, isStatic $ fst $ typeInfo specs ]  duplicates :: Eq a => [a] -> [a] duplicates [] = []@@ -46,15 +50,19 @@  data MDB = MDB   { nextId' :: Int+  , stage   :: Stage   , stack   :: [Ident]   , model   :: Model   } +data Stage = Init | Loop | Done deriving Eq+ initMDB :: MDB initMDB = MDB   { nextId' = 0+  , stage   = Init   , stack   = []-  , model   = Model { variables = [], actions = [] }+  , model   = Model { initActions = [], loopActions = [] }   }  nextId :: M Int@@ -63,43 +71,59 @@   put m { nextId' = nextId' m + 1 }   return $ nextId' m +setStage :: Stage -> M ()+setStage a = do+  m <- get+  put m { stage = a } +getStage :: M Stage+getStage = do+  m <- get+  return $ stage m+ -- | Environment for resolving identifiers.-data Env = Env-  { values  :: [Value]-  }+type Env = [Value] -data Value-  = EnvFunction String Function-  | EnvVariable String V+data Value = EnvFunction String Function | EnvVariable String V -data Function = Function Int ([E] -> M E)+data Function = Function Int ([E] -> M ())  -- | Looks of a variable in the environment. variable :: Env -> Ident -> V variable env i@(Ident name _ _) = if null m then err i $ "variable \"" ++ name ++ "\" not found" else head m   where-  m = [ a | EnvVariable n a <- values env, n == name ]+  m = [ a | EnvVariable n a <- env, n == name ]  -- | Looks of a function in the environment. function :: Env -> Ident -> Function function env i@(Ident name _ _) = if null m then err i $ "function \"" ++ name ++ "\" not found" else head m   where-  m = [ a | EnvFunction n a <- values env, n == name ]+  m = [ a | EnvFunction n a <- env, n == name ]  -- | Creates a branch.-branch :: Position -> V -> M a -> M a -> M (a, a)-branch n a onTrue onFalse = do+branch :: Position -> V -> M () -> M () -> M ()+branch p a onTrue onFalse = do   --XXX What happens if infinite loop is called within branch?   m1 <- get-  put m1 { model = (model m1) { actions = [] } }-  r1 <- onTrue+  case stage m1 of+    Init -> put m1 { model = (model m1) { initActions = [] } }+    Loop -> put m1 { model = (model m1) { loopActions = [] } }+    Done -> unexpected p "statements after infinite loop"+  onTrue   m2 <- get-  put m1 { model = (model m2) { actions = [] } }-  r2 <- onFalse+  case stage m2 of+    Init | stage m1 == Init -> put m1 { model = (model m2) { initActions = [] } }+    Loop | stage m1 == Loop -> put m1 { model = (model m2) { loopActions = [] } }+    _ -> unexpected p "infinite loop in branch"+  onFalse   m3 <- get-  put m3 { model = (model m3) { actions = actions $ model m1 } }-  newAction $ Branch a (reverse $ actions $ model m2) (reverse $ actions $ model m3) n-  return (r1, r2)+  case stage m3 of+    Init | stage m1 == Init && stage m2 == Init -> do+      put m3 { model = (model m3) { initActions = initActions $ model m1 } }+      newAction $ Branch a (reverse $ initActions $ model m2) (reverse $ initActions $ model m3) p+    Loop | stage m1 == Loop && stage m2 == Loop -> do+      put m3 { model = (model m3) { loopActions = loopActions $ model m1 } }+      newAction $ Branch a (reverse $ loopActions $ model m2) (reverse $ loopActions $ model m3) p+    _ -> unexpected p "infinite loop in branch"  -- | Push an identifier onto the call stack, do something, then pop it off. callStack :: Ident -> M a -> M a@@ -119,41 +143,31 @@  -- | The initial environment defines the assert and assume functions. initEnv :: Env-initEnv = Env-  { values =-    [ EnvFunction "assert" $ Function 1 assert-    , EnvFunction "assume" $ Function 1 assume-    ]-  }+initEnv = [EnvFunction "assert" $ Function 1 assert, EnvFunction "assume" $ Function 1 assume]   where   assert a' = do     let a = head a'     s <- callPath-    x <- latch (posOf a) a+    x <- latchBool (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+    x <- latchBool (posOf a) a     newAction $ Assume x s (posOf a)-    return $ Var x  -- | Adds new action. newAction :: Action -> M () newAction a = do   m <- get-  put m { model = (model m) { actions = a : actions (model m) }}+  case stage m of+    Init -> put m { model = (model m) { initActions = a : initActions (model m) }}+    Loop -> put m { model = (model m) { loopActions = a : loopActions (model m) }}+    Done -> error "Compile.newAction"  -- | Adds new variable. addVar :: Env -> V -> M Env-addVar env a = do-  case a of-    State a -> do-      m <- get-      put m { model = (model m) { variables = if elem a (variables $ model m) then variables $ model m else a : variables (model m) }}-    _ -> return ()-  return env { values = EnvVariable name a : values env }+addVar env a = return $ EnvVariable name a : env   where   name = case a of     State (VS a _ _ _)  -> a@@ -164,132 +178,109 @@   evalStat :: Env -> CStat -> M ()-evalStat env a = case a of-  CLabel i a [] _ -> callStack i $ evalStat env a-  CExpr Nothing _ -> return ()-  CExpr (Just a) _ -> evalExpr env a >> return ()-  CCompound ids items _ -> f ids-    where-    f :: [Ident] -> M ()-    f [] = foldM evalBlockItem env items >> return ()-    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 >>= latch (posOf n)-    branch (posOf n) a (evalStat env b) (evalStat env c)-    return ()-  _ -> notSupported a "statement"+evalStat env a = do+  stage <- getStage+  when (stage == Done) $ unexpected a "statements after infinite loop"+  case a of+    CFor (Left Nothing) Nothing Nothing a _              | stage == Init -> do setStage Loop >> evalStat env a >> setStage Done+    CWhile (CConst (CIntConst (CInteger 1 _ _) _)) a _ _ | stage == Init -> do setStage Loop >> evalStat env a >> setStage Done+    CLabel i a [] _ -> callStack i $ evalStat env a+    CCompound ids items _ -> f ids+      where+      f :: [Ident] -> M ()+      f [] = foldM evalBlockItem env items >> return ()+      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 <- latchBool (posOf n) $ evalExpr env a+      branch (posOf n) a (evalStat env b) (evalStat env c)+      return () +    CExpr Nothing _ -> return ()+    CExpr (Just (CAssign op a b n)) _ -> case op of+      CAssignOp -> case evalExpr env a of+        Var v -> assign (posOf n) v $ evalExpr env b+        _ -> unexpected a "non variable in left hand of assignment"+      CMulAssOp -> f CMulOp+      CDivAssOp -> f CDivOp+      CRmdAssOp -> f CRmdOp+      CAddAssOp -> f CAddOp+      CSubAssOp -> f CSubOp+      CShlAssOp -> f CShlOp+      CShrAssOp -> f CShrOp+      CAndAssOp -> f CAndOp+      CXorAssOp -> f CXorOp+      COrAssOp  -> f COrOp+      where+      f :: CBinaryOp -> M ()+      f op = evalStat env (CExpr (Just (CAssign CAssignOp a (CBinary op a b n) n)) n)++    CExpr (Just (CCall (CVar f _) args _)) _ -> do+      when (arity /= length args) $ unexpected f $ "function called with " ++ show (length args) ++ " arguments, but defined with " ++ show arity ++ " arguments"+      callStack f $ func $ map (evalExpr env) args+      where+      Function arity func = function env f++    CExpr (Just (CCall _ _ _)) _ -> notSupported a "non named function references"++    CExpr (Just (CUnary op a n1)) n2 | elem op [CPreIncOp, CPostIncOp] -> evalStat env (CExpr (Just (CAssign CAddAssOp a one n1)) n2)+                                     | elem op [CPreDecOp, CPostDecOp] -> evalStat env (CExpr (Just (CAssign CSubAssOp a one n1)) n2)+      where+      one = CConst $ CIntConst (cInteger 1) n1++    _ -> notSupported a "statement"+ evalBlockItem :: Env -> CBlockItem -> M Env evalBlockItem env a = case a of   CBlockStmt a    -> evalStat env a >> return env   CBlockDecl a    -> evalDecl env a   CNestedFunDef a -> evalFunc env a -evalExpr :: Env -> CExpr -> M E+-- No stateful operations for expressions.+evalExpr :: Env -> CExpr -> E 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 (posOf n) v b' >> return a'-        _ -> unexpected a "non variable in left hand of assignment"-    CMulAssOp -> f CMulOp-    CDivAssOp -> f CDivOp-    CRmdAssOp -> f CRmdOp-    CAddAssOp -> f CAddOp-    CSubAssOp -> f CSubOp-    CShlAssOp -> f CShlOp-    CShrAssOp -> f CShrOp-    CAndAssOp -> f CAndOp-    CXorAssOp -> f CXorOp-    COrAssOp  -> f COrOp-    where-    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 >>= latch (posOf a)-    (b, c) <- branch (posOf n) a (evalExpr env b) (evalExpr env c)-    return $ Mux (Var a) b c $ posOf n-  CCond a Nothing b n -> do-    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-    CDivOp -> f Div-    CRmdOp -> f Mod-    CAddOp -> f Add-    CSubOp -> f Sub+  CCond a (Just b) c n -> Mux (evalExpr env a) (evalExpr env b) (evalExpr env c) $ posOf n+  CCond a Nothing  b n -> Or (evalExpr env a) (evalExpr env b) $ posOf n+  CBinary op a' b' n -> case op of+    CMulOp -> Mul a b p+    CDivOp -> Div a b p+    CRmdOp -> Mod a b p+    CAddOp -> Add a b p+    CSubOp -> Sub a b p     CShlOp -> notSupported a "(<<)"     CShrOp -> notSupported a "(>>)"-    CLeOp  -> f Lt-    CGrOp  -> f $ \ a b n -> Lt b a n-    CLeqOp -> f $ \ a b n -> Not (Lt b a n) n-    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+    CLeOp  -> Lt a b p+    CGrOp  -> Lt b a p+    CLeqOp -> Not (Lt b a p) p+    CGeqOp -> Not (Lt a b p) p+    CEqOp  -> Eq a b p+    CNeqOp -> Not (Eq a b p) p     CAndOp -> notSupported a "(&)"     CXorOp -> notSupported a "(^)"     COrOp  -> notSupported a "(|)"-    CLndOp -> do-      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 >>= latch (posOf a)-      (a, b) <- branch n' a (return $ Var a) (evalExpr env b)-      return $ Mux a a b n'+    CLndOp -> And a b p+    CLorOp -> Or a b p     where-    n' = posOf n-    f :: (E -> E -> Position -> E) -> M E-    f op = do-      a <- evalExpr env a-      b <- evalExpr env b-      return $ op a b n'+    a = evalExpr env a'+    b = evalExpr env b'+    p = posOf n -  CUnary op a n -> do-    a <- evalExpr env a-    case (op, a) of-      (CPreIncOp, Var a) -> do-        assign p a $ Add (Var a) one p-        return $ Var a-      (CPreDecOp, Var a) -> do-        assign p a $ Sub (Var a) one p-        return $ Var a-      (CPostIncOp, Var a) -> do-        b <- latch p $ Var a-        assign p a $ Add (Var a) one p-        return $ Var b-      (CPostDecOp, Var a) -> do-        b <- latch p $ Var a-        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-      --(CAdrOp,  a) -> return $ Ref a p-      --(CIndOp,  a) -> return $ Deref a p-      _ -> notSupported n "unary operator"+  CUnary op a' n -> case op of+    CPlusOp -> a+    CMinOp  -> Sub zero a p+    CNegOp  -> Not a p+    --(CAdrOp,  a) -> return $ Ref a p+    --(CIndOp,  a) -> return $ Deref a p+    _ -> notSupported n "unary operator"     where+    a = evalExpr env a'     p = posOf n-    one  = Const $ M.CInteger 1 p     zero = Const $ M.CInteger 0 p -  CCall (CVar f _) args _ -> do-    args <- mapM (evalExpr env) args-    when (arity /= length args) $ unexpected f $ "function called with " ++ show (length args) ++ " arguments, but defined with " ++ show arity ++ " arguments"-    callStack f $ func args-    where-    Function arity func = function env f--  CCall _ _ _ -> notSupported a "non named function references"--  CVar i _ -> return $ Var $ variable env i+  CVar i _ -> Var $ variable env i   CConst a -> case a of-    CIntConst (CInteger a _ _) n -> return $ Const $ M.CInteger a $ posOf n-    CFloatConst (CFloat a) n -> return $ Const $ CRational (toRational (read a :: Double)) $ posOf n+    CIntConst (CInteger a _ _) n -> Const $ M.CInteger a $ posOf n+    CFloatConst (CFloat a) n -> Const $ CRational (toRational (read a :: Double)) $ posOf n     _ -> notSupported a "char or string constant"   _ -> notSupported a "expression"     @@ -324,15 +315,16 @@        (Just (CInitExpr c _), Nothing) -> evalDecl' env (a, Nothing, Just c) -      (Nothing, Just e') -> do-        e <- evalExpr env e'+      (Nothing, Just e) -> do         v <- if isVolatile typInfo           then return $ Volatile name typ $ posOf n           else do             i <- nextId-            return $ Local name typ i (posOf e')-        declare (posOf e') v e+            return $ Local name typ i p+        declare p v $ evalExpr env e         addVar env v+        where+        p = posOf e       _ -> notSupported i "variable declaration"     _ -> notSupported d "arrays, pointers, or functional pointers (So what good is this tool anyway?)"       @@ -340,7 +332,7 @@ evalFunc :: Env -> CFunDef -> M Env evalFunc env f =  do   when (typ /= Void) $ notSupported f "non void function"-  return env { values = EnvFunction name (Function (length args) func) : values env }+  return $ EnvFunction name (Function (length args) func) : env   where   (specs, (Ident name _ _), args', stat) = functionInfo f   (_, typ) = typeInfo specs@@ -348,7 +340,6 @@   func args' = do     env <- foldM bindArg env $ zip args args'     evalStat env stat-    return false --XXX No support for 'return'.  bindArg :: Env -> ((Ident, (TypeInfo, Type)), E) -> M Env bindArg env ((Ident name _ n, (typInfo, typ)), a) = if isVolatile typInfo@@ -382,17 +373,12 @@   _ -> newAction $ Assign v a n  -- | 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+latchBool :: Position -> E -> M V+latchBool n a = do   i <- nextId-  let v = Tmp (typeOf a) i n-  case typeOf a of-    Integer  Nothing -> error "Compile.latch1"-    Rational Nothing -> error "Compile.latch2"-    _ -> do-      declare n v a-      return v+  let v = Tmp Bool i n+  declare n v a+  return v   @@ -445,6 +431,7 @@     CIf a b (Just c) _ -> fe env a ++ fs env b ++ fs env c     CSwitch a b _ -> fe env a ++ fs env b     CWhile a b _ _ -> fe env a ++ fs env b+    CFor (Left Nothing) Nothing Nothing a _ -> fs env a     CFor _ _ _ _ _ -> notSupported a "for loops"     CGoto _ _ -> []     CGotoPtr a _ -> fe env a
src/Model.hs view
@@ -15,8 +15,11 @@   , isInteger   , typeCheckModel   , unify+  , eVars+  , variables   ) where +import Data.List import Language.C.Data.Position  import Error@@ -188,7 +191,7 @@   (a, b) -> err n $ "type violation: " ++ show a ++ " incompatiable with " ++ show b  typeCheckModel :: Model -> Model-typeCheckModel m = m { actions = map typeCheckAction $ actions m }+typeCheckModel m = m { initActions = map typeCheckAction $ initActions m, loopActions = map typeCheckAction $ loopActions m }  typeCheckAction :: Action -> Action typeCheckAction a = case a of@@ -204,6 +207,24 @@ false :: E false = Const $ CBool False nopos +eVars :: E -> [V]+eVars a = case a of+  Var a -> [a]+  Const _ -> []+  Not a _ -> eVars a+  And a b _ -> eVars a ++ eVars b+  Or  a b _ -> eVars a ++ eVars b+  Mul a b _ -> eVars a ++ eVars b+  Div a b _ -> eVars a ++ eVars b+  Mod a b _ -> eVars a ++ eVars b+  Add a b _ -> eVars a ++ eVars b+  Sub a b _ -> eVars a ++ eVars b+  Lt  a b _ -> eVars a ++ eVars b+  Eq  a b _ -> eVars a ++ eVars b+  Mux a b c _ -> eVars a ++ eVars b ++ eVars c+  Ref a _ -> eVars a+  Deref a _ -> eVars a+ instance Pos Position where posOf = id  data Action@@ -222,8 +243,22 @@     Assume  _ _ a -> a     Branch  _ _ _ a -> a +variables :: Model -> [VS]+variables m = nub $ concatMap vars $ initActions m ++ loopActions m+  where+  vars :: Action -> [VS]+  vars a = case a of+    Declare v e _ -> var v ++ [ a | State a <- eVars e ]+    Assign  v e _ -> var v ++ [ a | State a <- eVars e ]+    Assert  v _ _ -> var v+    Assume  v _ _ -> var v+    Branch  v a b _ -> var v ++ concatMap vars a ++ concatMap vars b+  var :: V -> [VS]+  var (State a) = [a]+  var _         = []+     data Model = Model-  { variables :: [VS]-  , actions   :: [Action]+  { initActions :: [Action]+  , loopActions :: [Action]   } deriving Show
src/Verify.hs view
@@ -13,12 +13,13 @@ -- | Verify a model with k-induction. verify :: FilePath -> Int -> Model -> IO () verify _ maxK _ | maxK < 1 = error "max k can not be less than 1"-verify yices maxK m = do-  mapM_ (verifyModel yices format maxK) models+verify yices maxK m' = mapM_ (verifyModel yices format maxK) models   where-  model = typeCheckModel m-  models = [ (name, trimModel model { actions = actions }) | (name, actions) <- trimAssertions (actions model) ]-  format = "verifying %-" ++ show (maximum [ length n | (n, _) <- models ]) ++ "s    "+  m = typeCheckModel m'+  initPlain = removeAssertions $ initActions m+  models = [ (name, m { initActions = actions,   loopActions = []      }) | (name, actions) <- trimAssertions $ initActions m ]+        ++ [ (name, m { initActions = initPlain, loopActions = actions }) | (name, actions) <- trimAssertions $ loopActions m ]+  format = "verifying %-" ++ show (maximum $ map length $ fst $ unzip models) ++ "s    "  -- | Remove all assertions except one. trimAssertions :: [Action] -> [(String, [Action])]@@ -40,29 +41,32 @@  -- | Trim all unneeded stuff from a model. trimModel :: Model -> Model-trimModel = id  --XXX+trimModel = id --XXX + -- | Verify a trimmed model. verifyModel :: FilePath -> String -> Int -> (String, Model) -> IO ()-verifyModel y format maxK (name, m) = do+verifyModel y format maxK (name, m') = do   printf format name   hFlush stdout   env0 <- initEnv y m-  execStateT (check env0 1) env0+  execStateT (actions (initActions m) >> doLoop >> check env0 1) env0   return ()   where+  m = trimModel m'   check :: Env -> Int -> Y ()   check env0 k = do-    transition m+    actions $ loopActions m     resultBasis <- checkBasis m env0     case resultBasis of-      Fail a  -> liftIO (printf "FAILED: disproved basis in k = %d (see trace)\n" k) >> writeTrace name a+      Fail a  -> liftIO (printf "FAILED: disproved basis in k = %d (see trace)\n" k) >> writeTrace True name a       Problem -> error "Verify.check1"-      Pass -> do+      Pass | null $ loopActions m -> liftIO $ printf "passed: assertion in initialization\n"+           | otherwise -> 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) >> writeTrace name a+                 | otherwise -> liftIO (printf "inconclusive: unable to proved step up to max k = %d (see trace)\n" k) >> writeTrace False name a           Problem -> error "Verify.check2"           Pass    -> liftIO $ printf "passed: proved step in k = %d\n" k         @@ -72,16 +76,21 @@ checkStep :: Y Result checkStep = do   env <- get-  let cmds' = reverse $ [CHECK] ++ [ASSERT $ NOT $ head $ asserts env] ++ cmds env-  r <- liftIO $ quickCheckY' (yices env) [] $ cmds'-  return $ result r+  if null $ asserts env+    then return Pass+    else do+      let cmds = vars env ++ loopCmds env ++ [ASSERT $ NOT $ head $ asserts env] ++ [CHECK]+      r <- liftIO $ quickCheckY' (yices env) [] cmds+      return $ result r  -- | Check induction basis. checkBasis :: Model -> Env -> Y Result checkBasis m env0 = do   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'+  let cmds = vars env ++ initCmds env ++ loopCmds env ++ [ASSERT $ NOT $ AND $ asserts env]+          ++ [ ASSERT $ VarE (getVar' env0 (State a)) := exprConst t c | a@(VS _ t c _) <- variables m ]+          ++ [CHECK]+  r <- liftIO $ quickCheckY' (yices env) [] cmds   return $ result r  result :: ResY -> Result@@ -92,16 +101,14 @@   _ -> error $ "unexpected yices results: " ++ show a  --- | Transition relation.  Returns assertion.-transition :: Model -> Y ()-transition m = mapM_ (action $ LitB True) $ actions m+actions :: [Action] -> Y ()+actions a = mapM_ (action $ LitB True) a  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 }+    State (VS name _ _ _) -> addTrace $ Assign' p name n+    Local name _ _ _      -> addTrace $ Assign' p name n     _ -> return ()      action :: ExpY -> Action -> Y ()@@ -109,34 +116,38 @@   Declare v e p -> do     e <- expr (typeOf v) e     v' <- addVar v-    env <- get-    put env { cmds = ASSERT (VarE v' := e) : cmds env }+    addCmd $ ASSERT (VarE v' := e)     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 }+    addCmd $ ASSERT (VarE v' := IF enabled e (VarE vLast))     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 }+    put env { asserts = (enabled :=> VarE a) : asserts env }+    addTrace $ Assert' p n a   Assume a _ _ -> do     a <- getVar a-    env <- get-    put env { cmds = ASSERT (enabled :=> VarE a) : cmds env }+    addCmd $ ASSERT (enabled :=> VarE a)   Branch a onTrue onFalse p -> do     a' <- getVar a     env0 <- get-    put env0 { trace = [] }+    if inLoop env0+      then put env0 { loopTrace = [] }+      else put env0 { initTrace = [] }     mapM_ (action $ AND [enabled,       VarE a']) onTrue     env1 <- get-    put env1 { trace = [] }+    if inLoop env1+      then put env1 { loopTrace = [] }+      else put env1 { initTrace = [] }     mapM_ (action $ AND [enabled, NOT $ VarE a']) onFalse     env2 <- get-    put env2 { trace = Branch' p a' (reverse $ trace env1) (reverse $ trace env2) : trace env0 }+    if inLoop env2+      then put env2 { loopTrace = Branch' p a' (reverse $ loopTrace env1) (reverse $ loopTrace env2) : loopTrace env0 }+      else put env2 { initTrace = Branch' p a' (reverse $ initTrace env1) (reverse $ initTrace env2) : initTrace env0 }     @@ -223,19 +234,38 @@ type Y = StateT Env IO  data Env = Env-  { yices   :: FilePath-  , nextId  :: Int-  , vars    :: [(V, String)]-  , cmds    :: [CmdY]-  , asserts :: [ExpY]-  , trace   :: [Trace]+  { yices     :: FilePath+  , nextId    :: Int+  , inLoop    :: Bool+  , names     :: [(V, String)]+  , vars      :: [CmdY]+  , initCmds  :: [CmdY]+  , loopCmds  :: [CmdY]+  , asserts   :: [ExpY]+  , initTrace :: [Trace]+  , loopTrace :: [Trace]   }  -data Trace = Assign' Position String String | Assert' Position String String | Branch' Position String [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_ f $ variables m) (Env y 0 [] [] [] [])+initEnv y m = execStateT (mapM_ f $ variables m) env   where+  env = Env+    { yices     = y+    , nextId    = 0+    , inLoop    = False+    , names     = []+    , vars      = []+    , initCmds  = []+    , loopCmds  = []+    , asserts   = []+    , initTrace = []+    , loopTrace = []+    }   f :: VS -> Y ()   f a = do     n <- addVar v@@ -243,22 +273,41 @@     where     v = State a +doLoop :: Y ()+doLoop = do+  env <- get+  put env { inLoop = True }+ addVar :: V -> Y String addVar v = do   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 }+  put env { nextId = nextId env + 1, names = (v, name) : names env, vars = DEFINE (name, VarT $ typeY v) Nothing : vars env }   return name +addCmd :: CmdY -> Y ()+addCmd cmd = do+  env <- get+  if inLoop env+    then put env { loopCmds = cmd : loopCmds env }+    else put env { initCmds = cmd : initCmds env }++addTrace :: Trace -> Y ()+addTrace t = do+  env <- get+  if inLoop env+    then put env { loopTrace = t : loopTrace env }+    else put env { initTrace = t : initTrace env }+ getVar :: V -> Y String getVar v = do   env <- get   return $ getVar' env v  getVar' :: Env -> V -> String-getVar' env v = case lookup v $ vars env of+getVar' env v = case lookup v $ names env of   Just a -> a-  Nothing -> error $ "Verify.getVar: variable not found: " ++ show v  ++ " in " ++ show (vars env)+  Nothing -> error $ "Verify.getVar: variable not found: " ++ show v  ++ " in " ++ show (names env)  typeY :: TypeOf a => a -> String typeY a = case typeOf a of@@ -268,12 +317,14 @@   Integer  _ -> "int"   Rational _ -> "real" -writeTrace :: String -> [ExpY] -> Y ()-writeTrace name table' = do+writeTrace :: Bool -> String -> [ExpY] -> Y ()+writeTrace withInit 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+  let format p = printf ("%-" ++ show (maximum $ map maxPosWidth $ (if withInit then initTrace env else []) ++ loopTrace env) ++ "s    ") $ position p+  liftIO $ writeFile (name ++ ".trace") $ (if withInit then trace format "init" (initTrace env) else "") ++ trace format "loop" (loopTrace env)   where+  trace :: (Position -> String) -> String -> [Trace] -> String+  trace format n t = n ++ ":\n" ++ concatMap (f format) (reverse t)   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' ]