packages feed

afv (empty) → 0.0.0

raw patch · 11 files changed

+1299/−0 lines, 11 filesdep +basedep +bytestringdep +directorysetup-changed

Dependencies added: base, bytestring, directory, language-c, mtl, process, yices

Files

+ LICENSE view
@@ -0,0 +1,27 @@+Copyright (c) Tom Hawkins 2009, 2010++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:+1. Redistributions of source code must retain the above copyright+   notice, this list of conditions and the following disclaimer.+2. Redistributions in binary form must reproduce the above copyright+   notice, this list of conditions and the following disclaimer in the+   documentation and/or other materials provided with the distribution.+3. Neither the name of the author nor the names of his contributors+   may be used to endorse or promote products derived from this software+   without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE+ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY+OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF+SUCH DAMAGE.
+ RELEASE-NOTES view
@@ -0,0 +1,4 @@+afv 0.0.0    01/12/10++- Initial release.+
+ Setup.lhs view
@@ -0,0 +1,8 @@+#! /usr/bin/env runhaskell++> module Main (main) where+>+> import Distribution.Simple (defaultMain)+>+> main :: IO ()+> main = defaultMain
+ afv.cabal view
@@ -0,0 +1,52 @@+name:    afv+version: 0.0.0++category: Formal Methods++synopsis: Model checking Atom generated C.++description: A model checker for Atom generated, or similar, C code.++author:     Tom Hawkins <tomahawkins@gmail.com>+maintainer: Tom Hawkins <tomahawkins@gmail.com>++stability: experimental++license:      BSD3+license-file: LICENSE++homepage: http://tomahawkins.org++build-type:    Simple+cabal-version: >= 1.6++extra-source-files:+  RELEASE-NOTES++executable afv+  hs-source-dirs:   src++  main-is:          AFV.hs++  other-modules:    Compile,+                    Error,+                    Model,+                    Parse,+                    Utils,+                    Verify++  build-depends:+    base          >= 4       && < 5,+    bytestring    >= 0.9.1   && < 0.9.2,+    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++  ghc-options:  -W+  extensions:++source-repository head+  type:     darcs+  location: http://patch-tag.com/r/tomahawkins/afv/pullrepo
+ src/AFV.hs view
@@ -0,0 +1,150 @@+module Main (main) where++import Data.List+import System.Environment+import System.IO++import Compile+import Parse+import Verify++main :: IO ()+main = do+  args <- getArgs+  case args of+    [] -> help+    (a:_) | elem a ["help", "-h", "--help", "-help"] -> help+    ["example"] -> example+    ["header"]  -> header+    ("verify":function: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+      verify (yices a) (k a) model+    _ -> help++data Args = Args+  { yices    :: FilePath+  , k        :: Int+  , gcc      :: FilePath+  , defines  :: [(String, String)]+  , includes :: [FilePath]+  , inputs   :: [FilePath]+  } deriving Show++parseArgs :: Args -> [String] -> Args+parseArgs a b = case b of+  [] -> a+  arg : args | isYices   -> parseArgs a { gcc = 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+    where+    isYices = isPrefixOf "--yices=" arg+    pathYices = drop 8 arg+    isGCC   = isPrefixOf "--gcc="   arg+    pathGCC = drop 6 arg+    isInclude = length arg > 2 && take 2 arg == "-I"+    isDefine  = length arg > 2 && take 2 arg == "-D"+    (name, value') = span (/= '=') $ drop 2 arg+    value = if length value' <= 1 then "1" else tail value'+  "-k" : k : args -> parseArgs a { k = read k } args+  files -> a { inputs = files }+ ++header :: IO ()+header = do+  putStrLn "writing AFV header file (afv.h) ..."+  writeFile "afv.h" $ unlines+    [ "#ifndef AFV"+    , "#include <assert.h>"+    , "#define assume assert"+    , "#endif"+    ]++example :: IO ()+example = do+  header+  putStrLn "writing example design (example.c) ..."+  putStrLn "verify with:  afv verify example -k 15 example.c"+  writeFile "example.c" $ unlines+    [ "// Provides assert and assume functions."+    , "#include \"afv.h\""+    , ""+    , "// Periodic function for verification.  Implements a simple rolling counter."+    , "void example () {"+    , ""+    , "  // The rolling counter."+    , "  static int counter = 0;"+    , ""+    , "  // Assertions."+    , "  GreaterThanOrEqualTo0: assert(counter >= 0);    // The 'counter' must always be greater than or equal to 0."+    , "  LessThan10:            assert(counter < 10);    // The 'counter' must always be less than 10."+    , ""+    , "  // Implementation 1."+    , "  if (counter == 10)"+    , "    counter = 0;"+    , "  else"+    , "    counter++;"+    , ""+    , "  // Implementation 2."+    , "  // if (counter == 9)"+    , "  //   counter = 0;"+    , "  // else"+    , "  //   counter = counter + 1;"+    , ""+    , "  // Implementation 3."+    , "  // if (counter >= 9)"+    , "  //   counter = 0;"+    , "  // else"+    , "  //   counter++;"+    , ""+    , "  // Implementation 4."+    , "  // if (counter >= 9 || counter < 0)"+    , "  //   counter = 0;"+    , "  // else"+    , "  //   counter++;"+    , ""+    , "  // Implementation 5."+    , "  // counter = (counter + 1) % 10;"+    , ""+    , "}"+    , ""+    ]++++help :: IO ()+help = putStrLn $ unlines+  [ ""+  , "NAME"+  , "  afv - Atom's Formal Verifier"+  , ""+  , "SYNOPSIS"+  , "  afv verify function-name [-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."+  , "  Requires GCC for C preprocessing and the Yices SMT solver."+  , ""+  , "COMMANDS"+  , "  verify function-name [options] c-files ..."+  , "    Runs verification on the specified periodic function."+  , ""+  , "    -k n          : Max k-induction depth."+  , "    --yices=path  : Path to Yices solver."+  , "    --gcc=path    : Path to GCC."+  , "    -Idir         : Add directory to includes search path."+  , "    -Dmacro       : Define a macro."+  , "    -Dmacro=def   : Define a macro with a value."+  , ""+  , "  header"+  , "    Writes AFV's header file (afv.h), which provides the 'assert' and 'assume' functions."+  , ""+  , "  example"+  , "    Writes an example design (example.c).  Verify with:"+  , "      afv verify example -k 15 example.c"+  , ""+  ]
+ src/Compile.hs view
@@ -0,0 +1,457 @@+module Compile (compile) where++import Control.Monad.State hiding (State)+import Data.List+import Language.C+import Language.C.Data.Ident++import Error+import Model hiding (CInteger)+import qualified Model as M+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) }++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 then notSupported (head asms) "inline assembly" 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 ]+  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.++type M = StateT MDB IO++data MDB = MDB+  { nextId  :: Int+  , stack   :: [Ident]+  , enabled :: E+  , model   :: Model+  }++initMDB :: MDB+initMDB = MDB+  { nextId  = 0+  , stack   = []+  , enabled = true+  , model   = Model { variables = [], actions = [] }+  }++++-- | Environment for resolving identifiers.+data Env = Env+  { values  :: [Value]+  }++data Value+  = EnvFunction String Function+  | EnvVariable String V++data Function = Function Int ([E] -> M E)++-- | 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 ]++-- | 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 ]++-- | Creates a branch.+branch :: Position -> E -> M a -> M a -> M (a, a)+branch n a onTrue onFalse = do+  m1 <- get+  put m1 { enabled = And (enabled m1) a n }+  r1 <- onTrue+  m2 <- get+  put m2 { enabled = And (enabled m1) (Not a n) n }+  r2 <- onFalse+  m3 <- get+  put m3 { enabled = enabled m1 }+  return (r1, r2)++-- | Push an identifier onto the call stack, do something, then pop it off.+callStack :: Ident -> M a -> M a+callStack id a = do+  m <- get+  put m { stack = id : stack m }+  a <- a+  m <- get+  put m { stack = tail $ stack m }+  return a++callPath :: M ([String], Position)+callPath = do+  m <- get+  let s = stack m+  return ([ n | Ident n _ _ <- reverse s ], posOf $ head s)++-- | The initial environment defines the assert and assume functions.+initEnv :: Env+initEnv = Env+  { values =+    [ EnvFunction "assert" $ Function 1 assert+    , EnvFunction "assume" $ Function 1 assume+    ]+  }+  where+  assert a = do+    (s, n) <- callPath+    m <- get+    let x = imply (enabled m) (head a) n+    newAction $ Assert x s n+    return x+  assume a = do+    (s, n) <- callPath+    m <- get+    let x = imply (enabled m) (head a) n+    newAction $ Assume x s n+    return x++-- | Adds new action.+newAction :: Action -> M ()+newAction a = do+  m <- get+  put m { model = (model m) { actions = a : actions (model m) }}++-- | 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 }+  where+  name = case a of+    State (VS a _ _ _)  -> a+    Volatile a _ _   -> a+    Local    a _ _ _ -> a+    Tmp      _ _ _   -> error "Compile.addVar: should not call addVar with Tmp"++++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+    branch (posOf n) a (evalStat env b) (evalStat env c)+    return ()+  _ -> 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+evalExpr env a = latch (posOf 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'+        _ -> 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+    (b, c) <- branch (posOf n) a (evalExpr env b) (evalExpr env c)+    return $ Mux 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)+    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+    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+    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+    CLndOp -> do+      a <- evalExpr env a+      (b, a) <- branch n' a (evalExpr env b) (return a)+      return $ Mux a b a n'+    CLorOp -> do+      a <- evalExpr env a+      (a, b) <- branch n' a (return a) (evalExpr env b)+      return $ Mux a a b n'+    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'++  CUnary op a n -> do+    a <- evalExpr env a+    case (op, a) of+      (CPreIncOp, Var a) -> do+        assign False p a $ Add (Var a) one p+        return $ Var a+      (CPreDecOp, Var a) -> do+        assign False 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+      (CPostDecOp, Var a) -> do+        b <- latch p $ Var a+        assign False p a $ Sub (Var a) one p+        return b+      (CPlusOp, a) -> return $ Add zero a p+      (CMinOp,  a) -> return $ Sub zero a p+      (CNegOp,  a) -> return $ Not a p+      _ -> notSupported n "unary operator"+    where+    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+  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+    _ -> notSupported a "char or string constant"+  _ -> notSupported a "expression"+    +evalDecl :: Env -> CDecl -> M Env+evalDecl env d@(CDecl specs decls _) = if isExtern typInfo then return env else foldM evalDecl' env decls+  where+  (typInfo, typ) = typeInfo specs+  evalDecl' :: Env -> (Maybe CDeclr, Maybe CInit, Maybe CExpr) -> M Env+  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)+        where+        v = State $ VS name typ init $ posOf n+        init = case typ of+          Void -> unexpected d "void type for variable declaration"+          Bool -> CBool (cInt /= 0) $ posOf n'+          Integer _  -> M.CInteger cInt $ posOf n'+          Rational _ -> CRational cRat $ posOf n'++        cInt :: Integer+        cInt = case const of+          CIntConst (CInteger a _ _) _ -> a+          _ -> unexpected const "non integer initialization"++        cRat :: Rational+        cRat = case const of+          CIntConst (CInteger a _ _) _ -> fromIntegral a+          CFloatConst (CFloat a) _     -> fromIntegral (read a :: Integer)+          _ -> unexpected const "non numeric initialization"++      (Nothing, Just e') -> do+        e <- evalExpr env e'+        v <- if isVolatile typInfo+          then return $ Volatile name typ $ posOf n+          else do+            m <- get+            put m { nextId = nextId m + 1 }+            return $ Local name typ (nextId m) (posOf e')+        assign True (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?)"+      ++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?)"+  return env { values = EnvFunction name (Function (length args) func) : values env }+  where+  (specs, (Ident name _ _), args, stat) = functionInfo f+  (_, typ) = typeInfo specs+  func _ = do --XXX+    evalStat env stat+    return false+++++++-- | Assgins a value to a variable.+assign :: Bool -> Position -> V -> E -> M ()+assign decl 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?++-- | 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 n a = do+  m <- get+  let v = Tmp (typeOf a) (nextId m) n+  put m { nextId = nextId m + 1 }+  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+++++++-- | Extract relavent info from a function declaration.+functionInfo :: CFunDef -> ([CDeclSpec], Ident, [CDecl], CStat)+functionInfo (CFunDef specs (CDeclr (Just ident) [(CFunDeclr (Right (args, False)) _ _)] Nothing [] _) [] stmt _) = (specs, ident, args, stmt)+functionInfo f = notSupported f "function"+++++-- | Topologically sorts functions based on dependencies.+sortFunctions :: [CFunDef] -> [CFunDef]+sortFunctions fs = case topo $ map functionDeps fs of+  Left a -> notSupported none $ "recursive functions somewhere among: " ++ show a+  Right a -> [ f | a <- a, f <- fs, functionName f == a ]++topo :: Eq a => [(a, [a])] -> Either [a] [a]+topo a = topo' [] a+  where+  topo' a [] = Right a+  topo' done waiting = if null next then Left $ fst $ unzip waiting else topo' (done ++ next) stillWaiting+    where+    next = [ a | (a, deps) <- waiting, all (flip elem done) deps ]+    stillWaiting = [ (a, deps) | (a, deps) <- waiting, notElem a next ]+++functionName :: CFunDef -> String+functionName f = name where (_, Ident name _ _, _, _) = functionInfo f++afvFunctionNames :: [String]+afvFunctionNames = ["assert", "assume"]++-- | Analyzes a function for dependencies.+functionDeps :: CFunDef -> (String, [String])+functionDeps f = (functionName f, filter (flip notElem afvFunctionNames) $ nub $ fb [] [CNestedFunDef f])+  where+  rewrite :: CFunDef -> CStat+  rewrite f = CCompound [] (map CBlockDecl args ++ [CBlockStmt stat]) none where (_, _, args, stat) = functionInfo f+  fs :: [String] -> CStat -> [String]+  fs env a = case a of+    CLabel _ a _ _ -> fs env a+    CCase a b _ -> fe env a ++ fs env b+    CCases a b c _ -> fe env a ++ fe env b ++ fs env c+    CDefault a _ -> fs env a+    CExpr (Just a ) _ -> fe env a+    CExpr Nothing _ -> []+    CCompound _ a _ -> fb env a+    CIf a b Nothing _ -> fe env a ++ fs env b+    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 _ _ _ _ _ -> notSupported a "for loops"+    CGoto _ _ -> []+    CGotoPtr a _ -> fe env a+    CCont _ -> []+    CBreak _ -> []+    CReturn Nothing _ -> []+    CReturn (Just a) _ -> fe env a+    CAsm _ _ -> []+  fe :: [String] -> CExpr -> [String]+  fe env a = case a of+    CComma a _ -> fe' a+    CAssign _ a b _ -> fe' [a, b]+    CCond a (Just b) c _ ->  fe' [a, b, c]+    CCond a Nothing b _ ->  fe' [a, b]+    CBinary _ a b _ -> fe' [a, b]+    CCast _ a _ -> fe env a --XXX does not check cast declaration.+    CUnary _ a _ -> fe env a+    --CSizeofExpr CExpr NodeInfo+    --CSizeofType CDecl NodeInfo+    --CAlignofExpr CExpr NodeInfo+    --CAlignofType CDecl NodeInfo+    --CComplexReal CExpr NodeInfo+    --CComplexImag CExpr NodeInfo+    CIndex a b _ -> fe' [a, b]+    CCall (CVar (Ident n _ _) _) args _ -> (if elem n env then [] else [n]) ++ fe' args+    CCall _ _ _ -> notSupported a "non-named function references"+    CMember a _ _ _ -> fe env a+    CVar _ _ -> []+    CConst _ -> []+    --CCompoundLit CDecl CInitList NodeInfo+    CStatExpr a _ -> fs env a+    CLabAddrExpr _ _ -> []+    --CBuiltinExpr CBuiltin+    _ -> notSupported a "expression"+    where+    fe' = concatMap $ fe env+  fb :: [String] -> [CBlockItem] -> [String]+  fb _ [] = []+  fb env (a:b) = case a of+    CBlockStmt a -> fs env a ++ fb env b+    CBlockDecl _ -> fb env b+    CNestedFunDef f -> fs env' (rewrite f) ++ fb env' b where env' = functionName f : env+
+ src/Error.hs view
@@ -0,0 +1,27 @@+module Error+  ( err+  , notSupported+  , unexpected+  , debug+  , debug'+  ) where++import Language.C+import System.IO.Unsafe++err :: Pos a => a -> String -> b+err a m = error $ format (posOf a) ++ ": " ++ m+  where+  format (Position name line col) = name ++ ":" ++ show line ++ ":" ++ show col++notSupported :: Pos a => a -> String -> b+notSupported a m = err a $ " not supported: " ++ m++unexpected :: Pos a => a -> String -> b+unexpected a m = err a $ "unexpected: " ++ m++debug :: Show a => String -> a -> a+debug m a = debug' m a a++debug' :: Show a => String -> a -> b -> b+debug' m a b = unsafePerformIO (putStrLn (m ++ ": " ++ show a) >> return b)
+ src/Model.hs view
@@ -0,0 +1,202 @@+module Model+  ( Type        (..)+  , IntegerType (..)+  , TypeOf      (..)+  , Const       (..)+  , VS          (..)+  , V           (..)+  , E           (..)+  , Action      (..)+  , Model       (..)+  , true+  , false+  , isRational+  , isInteger+  , unify+  ) where++import Language.C.Data.Position++import Error++data IntegerType = U8 | U16 | U32 | U64 | S8 | S16 | S32 | S64 deriving (Show, Eq)++data Type+  = Void+  | Bool+  | Integer  (Maybe IntegerType)+  | Rational (Maybe Bool)          -- isDouble+  deriving Eq++isInteger :: Type -> Bool+isInteger (Integer _) = True+isInteger _ = False++isRational :: Type -> Bool+isRational (Rational _) = True+isRational _ = False++instance Show Type where+  show a = case a of+    Void -> "void"+    Bool -> "bool"+    Integer Nothing -> "unspecified integer type"+    Integer (Just a) -> case a of+      U8  -> "unsigned char"+      U16 -> "unsigned short"+      U32 -> "unsigned long"+      U64 -> "unsigned long long"+      S8  -> "signed char"+      S16 -> "signed short"+      S32 -> "signed long"+      S64 -> "signed long long"+    Rational Nothing -> "unspecified floating type"+    Rational (Just True)  -> "double"+    Rational (Just False) -> "float"++class TypeOf a where typeOf :: a -> Type++instance TypeOf Type where typeOf = id++data Const+  = CBool Bool Position+  | CInteger Integer Position+  | CRational Rational Position+  deriving (Show, Eq)++instance TypeOf Const where+  typeOf a = case a of+    CBool _ _     -> Bool+    CInteger  _ _ -> Integer Nothing+    CRational _ _ -> Rational Nothing++instance Pos Const where+  posOf a = case a of+    CBool     _ a -> a+    CInteger  _ a -> a+    CRational _ a -> a++-- | User defined state variable (non-volatile top level variables or non-volatile static variables in functions).+data VS = VS String Type Const Position deriving (Show, Eq)++instance TypeOf VS where typeOf (VS _ t _ _) = t+instance Pos VS where posOf (VS _ _ _ n) = n++-- | Variables.+data V+  = State VS+  | Volatile String Type       Position+  | Local    String Type Int   Position+  | Tmp             Type Int   Position+  deriving (Show, Eq)+     +instance TypeOf V where+  typeOf a = case a of+    State a -> typeOf a+    Volatile _ a _   -> a+    Local    _ a _ _ -> a+    Tmp      a _ _   -> a++instance Pos V where+  posOf a = case a of+    State a -> posOf a+    Volatile _ _ n -> n+    Local _ _ _ n -> n+    Tmp _ _ n -> n++{-+instance Pos V where+  posOf a = case a of+    V        _ _ a   -> a+    Volatile _ _ a   -> a+    Local    _ _ a _ -> a+-}   ++-- | Expressions.+data E+  = Var V+  | Const Const+  | Not E Position+  | And E E Position+  | Or  E E Position+  | Mul E E Position+  | Div E E Position+  | Mod E E Position+  | Add E E Position+  | Sub E E Position+  | Lt  E E Position+  | Eq  E E Position+  | Mux E E E Position+  deriving (Show, Eq)++instance Pos E where+  posOf a = case a of+    Var a -> posOf a+    Const a -> posOf a+    Not _ a -> a+    And _ _ a -> a+    Or  _ _ a -> a+    Mul _ _ a -> a+    Div _ _ a -> a+    Mod _ _ a -> a+    Add _ _ a -> a+    Sub _ _ a -> a+    Lt  _ _ a -> a+    Eq  _ _ a -> a+    Mux _ _ _ a -> a++instance TypeOf E where+  typeOf a = case a of+    Var a       -> typeOf a+    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)+    Mul a b _   -> unify' (typeOf a) (typeOf b)+    Div a b _   -> unify' (typeOf a) (typeOf b)+    Mod a b _   -> unify' (typeOf a) (typeOf b)+    Add a b _   -> unify' (typeOf a) (typeOf b)+    Sub a b _   -> unify' (typeOf a) (typeOf b)+    Lt  a b _   -> seq (unify' (typeOf a) (typeOf b)) Bool+    Eq  a b _   -> seq (unify' (typeOf a) (typeOf b)) Bool+    Mux a b c _ -> seq (unify' (typeOf b) (typeOf c)) $ unify' Bool (typeOf a)+    where+    unify' = unify a++unify :: Pos a => a -> Type -> Type -> Type+unify n a b = case (a, b) of+  (a, b) | a == b -> a++  (Bool, Integer Nothing) -> Bool+  (Integer Nothing, Bool) -> Bool++  (Integer Nothing, a@(Integer _)) -> a+  (a@(Integer _), Integer Nothing) -> a++  (Integer Nothing, a@(Rational _)) -> a+  (a@(Rational _), Integer Nothing) -> a++  (Rational Nothing, a@(Rational _)) -> a+  (a@(Rational _), Rational Nothing) -> a++  (a, b) -> unexpected n $ "type violation: " ++ show a ++ " incompatiable with " ++ show b++true :: E+true = Const $ CBool True nopos++false :: E+false = Const $ CBool False nopos++instance Pos Position where posOf = id++data Action+  = Assign V E+  | Assert E [String] Position+  | Assume E [String] Position+  deriving (Show, Eq)++data Model = Model+  { variables :: [VS]+  , actions   :: [Action]+  } deriving Show+
+ src/Parse.hs view
@@ -0,0 +1,28 @@+module Parse (parse) where++import Language.C+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+  a <- preprocess gcc includes defines file+  case parseC a (initPos file) of+    Left e  -> putStrLn ("parsing error: " ++ show e) >> exitFailure+    Right a -> return a++preprocess :: FilePath -> [FilePath] -> [(String,String)] -> FilePath -> IO InputStream+preprocess gcc includes defines file = do+  a <- runPreprocessor (newGCC gcc) CppArgs+    { cppOptions = map IncludeDir includes ++ map (\ (a,b) -> Define a b) defines+    , extraOptions = []+    , cppTmpDir = Nothing+    , inputFile = file+    , outputFile = Nothing+    }+  case a of+    Left e  -> putStrLn "preprocessing error" >> exitWith e+    Right a -> return a+
+ src/Utils.hs view
@@ -0,0 +1,85 @@+module Utils+  ( TypeInfo (..)+  , typeInfo+  , isVisable+  ) where++import Data.List+import Language.C++import Error+import Model++data TypeInfo = TypeInfo+  { isConst+  , isVolatile+  , isStatic+  , isExtern    :: Bool+  }++isVisable :: TypeInfo -> Bool+isVisable t = not (isStatic t) && not (isExtern t)++typeInfo :: [CDeclSpec] -> (TypeInfo, Type)+typeInfo specs = (info, typ)+  where+  info = foldl f TypeInfo { isConst = False, isVolatile = False, isStatic = False, isExtern = False } specs+  f :: TypeInfo -> CDeclSpec -> TypeInfo+  f t a = case a of+    CStorageSpec a -> case a of+      CStatic _ -> t { isStatic = True }+      CExtern _ -> t { isExtern = True }+      _         -> notSupported a "storage class"+    CTypeQual a -> case a of+      CConstQual _ -> t { isConst    = True }+      CVolatQual _ -> t { isVolatile = True }+      _         -> notSupported a "type qualifier"+    CTypeSpec _ -> t+  voids    = [ a | CTypeSpec a@(CVoidType _) <- specs ]+  signed   = [ a | CTypeSpec a@(CSignedType _) <- specs ]+  unsigned = [ a | CTypeSpec a@(CUnsigType  _) <- specs ]+  bools    = [ a | CTypeSpec a@(CBoolType _) <- specs ]+  chars    = [ a | CTypeSpec a@(CCharType _) <- specs ]+  shorts   = [ a | CTypeSpec a@(CShortType _) <- specs ]+  longs    = [ a | CTypeSpec a@(CLongType _) <- specs ]+  ints     = [ a | CTypeSpec a@(CIntType _) <- specs ]+  floats   = [ a | CTypeSpec a@(CFloatType _) <- specs ]+  doubles  = [ a | CTypeSpec a@(CDoubleType _) <- specs ]+  typ = case (length voids, length signed, length unsigned, length bools, length chars, length shorts, length longs, length ints, length floats, length doubles) of+    (1, 0, 0, 0, 0, 0, 0, 0, 0, 0) -> Void++    (0, 0, 0, 1, 0, 0, 0, 0, 0, 0) -> Bool++    (0, 0, 0, 0, 1, 0, 0, 0, 0, 0) -> Integer $ Just S8+    (0, 1, 0, 0, 1, 0, 0, 0, 0, 0) -> Integer $ Just S8+    (0, 0, 1, 0, 1, 0, 0, 0, 0, 0) -> Integer $ Just U8++    (0, 0, 0, 0, 0, 1, 0, 0, 0, 0) -> Integer $ Just S16+    (0, 1, 0, 0, 0, 1, 0, 0, 0, 0) -> Integer $ Just S16+    (0, 0, 1, 0, 0, 1, 0, 0, 0, 0) -> Integer $ Just U16+    (0, 0, 0, 0, 0, 1, 0, 1, 0, 0) -> Integer $ Just S16+    (0, 1, 0, 0, 0, 1, 0, 1, 0, 0) -> Integer $ Just S16+    (0, 0, 1, 0, 0, 1, 0, 1, 0, 0) -> Integer $ Just U16++    (0, 0, 0, 0, 0, 0, 0, 1, 0, 0) -> Integer $ Just S32+    (0, 1, 0, 0, 0, 0, 0, 1, 0, 0) -> Integer $ Just S32+    (0, 0, 1, 0, 0, 0, 0, 1, 0, 0) -> Integer $ Just U32+    (0, 0, 0, 0, 0, 0, 1, 0, 0, 0) -> Integer $ Just S32+    (0, 1, 0, 0, 0, 0, 1, 0, 0, 0) -> Integer $ Just S32+    (0, 0, 1, 0, 0, 0, 1, 0, 0, 0) -> Integer $ Just U32+    (0, 0, 0, 0, 0, 0, 1, 1, 0, 0) -> Integer $ Just S32+    (0, 1, 0, 0, 0, 0, 1, 1, 0, 0) -> Integer $ Just S32+    (0, 0, 1, 0, 0, 0, 1, 1, 0, 0) -> Integer $ Just U32++    (0, 0, 0, 0, 0, 0, 2, 0, 0, 0) -> Integer $ Just S64+    (0, 1, 0, 0, 0, 0, 2, 0, 0, 0) -> Integer $ Just S64+    (0, 0, 1, 0, 0, 0, 2, 0, 0, 0) -> Integer $ Just U64+    (0, 0, 0, 0, 0, 0, 2, 1, 0, 0) -> Integer $ Just S64+    (0, 1, 0, 0, 0, 0, 2, 1, 0, 0) -> Integer $ Just S64+    (0, 0, 1, 0, 0, 0, 2, 1, 0, 0) -> Integer $ Just U64++    (0, 0, 0, 0, 0, 0, 0, 0, 1, 0) -> Rational $ Just False+    (0, 0, 0, 0, 0, 0, 0, 0, 0, 1) -> Rational $ Just True++    a -> notSupported (head specs) $ "type signature: " ++ show a+
+ src/Verify.hs view
@@ -0,0 +1,259 @@+module Verify (verify) where++import Control.Monad+import Data.IORef+import Data.List+import Data.Maybe+import Math.SMT.Yices.Pipe+import Math.SMT.Yices.Syntax+import System.IO+import Text.Printf++import Model++-- | 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+  y <- createYicesPipe yices []+  mapM_ (verifyModel y maxK) models+  exitY y+  where+  assertions = [ a | a@(Assert _ _ _) <- actions m ]+  models = map (trimModel . trimAssertions m) assertions++-- | 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++-- | Trim all unneeded stuff from a model.+trimModel :: Model -> Model+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+  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)+    case resultBasis of+      Fail -> printf "FAILED: disproved basis in k = %d\n" k+      Pass -> do+        resultStep <- checkStep y assert+        case resultStep of+          Fail -> withLogic y $ check initEnv env (assert : asserts) (k + 1)+          Pass -> 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+  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+  return $ result r++result :: ResY -> Result+result a = case a of+  Sat _   -> Fail+  UnSat _ -> Pass+  InCon _ -> Pass++-- | 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)++action :: YicesIPC -> (Env, ExpY) -> Action -> IO (Env, ExpY)+action y (env, assert) 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)+  Assert a _ _ -> do+    a <- expr y env Bool a+    return (env, AND [assert, a])+  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++  Const a -> return $ exprConst t a++  Not a _ -> do+    a <- expr y env Bool a+    return $ NOT a++  And a b _ -> do+    a <- expr y env Bool a+    b <- expr y env Bool b+    return $ AND [a, b]++  Or  a b _ -> do+    a <- expr y env Bool a+    b <- expr y env Bool b+    return $ OR  [a, b]++  Mul a b _ -> do+    a <- expr y env t a+    b <- expr y env t b+    return $ a :*: b+  +  Div a b _  -> do+    a <- expr y env t a+    b <- expr y env t b+    return $ op a b+    where+    op = case t of+      Integer _ -> DIV+      _         -> (:/:)++  Mod a b _ -> do+    a <- expr y env t a+    b <- expr y env t b+    return $ MOD a b++  Add a b _ -> do+    a <- expr y env t a+    b <- expr y env t b+    return $ a :+: b++  Sub a b _ -> do+    a <- expr y env t a+    b <- expr y env 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+    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+    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+    return $ IF a b c++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+++++data Env = Env NextId [(V, String)]  -- Env nextId table++initEnv :: YicesIPC -> Model -> IO Env+initEnv y m = do+  nid <- newNextId+  foldM (addVar y) (Env nid []) $ map State $ variables m++addVar :: YicesIPC -> Env -> V -> IO Env+addVar y (Env nid table) v = do+  i <- nextId nid+  let name = printf "n%d" i+  runCmds y [DEFINE (name, VarT $ typeY v) Nothing]+  return $ Env nid $ replace (v, name) table++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)++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 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++