packages feed

afv 0.0.1 → 0.0.2

raw patch · 8 files changed

+114/−56 lines, 8 files

Files

RELEASE-NOTES view
@@ -8,3 +8,8 @@ - Uses yices new 'quickCheckY'. - Fixed bug affecting 'assume'. +afv 0.0.2    01/17/10++- Support for function arguments.  Still no support for return values.+- Stronger type checking.+
afv.cabal view
@@ -1,11 +1,13 @@ name:    afv-version: 0.0.1+version: 0.0.2  category: Formal Methods -synopsis: Model checking Atom generated C.+synopsis: Infinite state model checking of iterative C programs. -description: A model checker for Atom generated, or similar, C code.+description: AFV is an infinite state model checker that+             verifies iterative C programs by k-induction.+             AFV uses Yices as the backend SMT solver.  author:     Tom Hawkins <tomahawkins@gmail.com> maintainer: Tom Hawkins <tomahawkins@gmail.com>
src/AFV.hs view
@@ -8,7 +8,7 @@ import Parse import Verify -version = "0.0.1"+version = "0.0.2"  main :: IO () main = do
src/Compile.hs view
@@ -45,7 +45,7 @@ type M = StateT MDB IO  data MDB = MDB-  { nextId  :: Int+  { nextId' :: Int   , stack   :: [Ident]   , enabled :: E   , model   :: Model@@ -53,12 +53,17 @@  initMDB :: MDB initMDB = MDB-  { nextId  = 0+  { nextId' = 0   , stack   = []   , enabled = true   , model   = Model { variables = [], actions = [] }   } +nextId :: M Int+nextId = do+  m <- get+  put m { nextId' = nextId' m + 1 }+  return $ nextId' m   -- | Environment for resolving identifiers.@@ -126,13 +131,13 @@     (s, n) <- callPath     m <- get     let x = imply (enabled m) (head a) n-    newAction $ Assert x s 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 n+    newAction $ Assume x s     return x  -- | Adds new action.@@ -265,6 +270,8 @@       (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"     where     p = posOf n@@ -300,6 +307,7 @@         v = State $ VS name typ init $ posOf n         init = case typ of           Void -> unexpected d "void type for variable declaration"+          Ptr _ -> notSupported d "pointer types"           Bool -> CBool (cInt /= 0) $ posOf n'           Integer _  -> M.CInteger cInt $ posOf n'           Rational _ -> CRational cRat $ posOf n'@@ -322,9 +330,8 @@         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')+            i <- nextId+            return $ Local name typ i (posOf e')         assign True (posOf e') v e         addVar env v       _ -> notSupported i "variable declaration"@@ -333,20 +340,37 @@  evalFunc :: Env -> CFunDef -> M Env evalFunc env f =  do-  when (typ /= Void || not (null args)) $ notSupported f "non void f() function (How lame is this?)"+  when (typ /= Void) $ notSupported f "non void function"   return env { values = EnvFunction name (Function (length args) func) : values env }   where-  (specs, (Ident name _ _), args, stat) = functionInfo f+  (specs, (Ident name _ _), args', stat) = functionInfo f   (_, typ) = typeInfo specs-  func _ = do --XXX+  args = concatMap funcArgs args'+  func args' = do+    env <- foldM bindArg env $ zip args args'     evalStat env stat-    return false+    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+  then addVar env (Volatile name typ (posOf n))+  else do+    i <- nextId+    let v = Local name typ i (posOf n)+    assign True (posOf n) v a+    addVar env v +funcArgs :: CDecl -> [(Ident, (TypeInfo, Type))]+funcArgs (CDecl specs decls n) = map f decls+  where+  t = typeInfo specs+  f (Just (CDeclr (Just i) [] Nothing [] _), Nothing, Nothing) = (i, t)+  f _ = notSupported n "function argument"    + -- | Assgins a value to a variable. assign :: Bool -> Position -> V -> E -> M () assign decl n v a = case v of@@ -360,9 +384,8 @@ 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 }+  i <- nextId+  let v = Tmp (typeOf a) i n   assign True n v a   return $ Var v @@ -377,7 +400,7 @@  -- | 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 (CFunDef specs (CDeclr (Just ident) [(CFunDeclr (Right (args, False)) _ _)] Nothing [] _) [] stmt _) = (specs, ident, args, stmt)  --XXX What is the False? functionInfo f = notSupported f "function"
src/Error.hs view
@@ -2,6 +2,7 @@   ( err   , notSupported   , unexpected+  , position   , debug   , debug'   ) where@@ -10,12 +11,10 @@ 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+err a m = error $ position a ++ ": " ++ m  notSupported :: Pos a => a -> String -> b-notSupported a m = err a $ " not supported: " ++ m+notSupported a m = err a $ "not supported: " ++ m  unexpected :: Pos a => a -> String -> b unexpected a m = err a $ "unexpected: " ++ m@@ -25,3 +24,8 @@  debug' :: Show a => String -> a -> b -> b debug' m a b = unsafePerformIO (putStrLn (m ++ ": " ++ show a) >> return b)++position :: Pos a => a -> String+position a = f ++ ":" ++ show l ++ ":" ++ show c+  where+  Position f l c = posOf a
src/Model.hs view
@@ -1,6 +1,7 @@ module Model   ( Type        (..)   , IntegerType (..)+  , FloatType   (..)   , TypeOf      (..)   , Const       (..)   , VS          (..)@@ -12,6 +13,7 @@   , false   , isRational   , isInteger+  , typeCheckModel   , unify   ) where @@ -21,11 +23,14 @@  data IntegerType = U8 | U16 | U32 | U64 | S8 | S16 | S32 | S64 deriving (Show, Eq) +data FloatType = Float | Double deriving (Show, Eq)+ data Type   = Void+  | Ptr Type   | Bool   | Integer  (Maybe IntegerType)-  | Rational (Maybe Bool)          -- isDouble+  | Rational (Maybe FloatType)   deriving Eq  isInteger :: Type -> Bool@@ -39,6 +44,7 @@ instance Show Type where   show a = case a of     Void -> "void"+    Ptr a -> show a ++ " *"     Bool -> "bool"     Integer Nothing -> "unspecified integer type"     Integer (Just a) -> case a of@@ -51,23 +57,23 @@       S32 -> "signed long"       S64 -> "signed long long"     Rational Nothing -> "unspecified floating type"-    Rational (Just True)  -> "double"-    Rational (Just False) -> "float"+    Rational (Just Double) -> "double"+    Rational (Just Float)  -> "float"  class TypeOf a where typeOf :: a -> Type  instance TypeOf Type where typeOf = id  data Const-  = CBool Bool Position-  | CInteger Integer Position+  = 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+    CBool     _ _ -> Bool+    CInteger  _ _ -> Integer  Nothing     CRational _ _ -> Rational Nothing  instance Pos Const where@@ -104,14 +110,6 @@     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@@ -127,6 +125,8 @@   | Lt  E E Position   | Eq  E E Position   | Mux E E E Position+  | Ref   E Position+  | Deref E Position   deriving (Show, Eq)  instance Pos E where@@ -144,6 +144,8 @@     Lt  _ _ a -> a     Eq  _ _ a -> a     Mux _ _ _ a -> a+    Ref _ a -> a+    Deref _ a -> a  instance TypeOf E where   typeOf a = case a of@@ -159,7 +161,11 @@     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)+    Mux a b c _ -> seq (unify' Bool (typeOf a)) $ unify' (typeOf b) (typeOf c)+    Ref a _ -> Ptr $ typeOf a+    Deref a p -> case typeOf a of+      Ptr a -> a+      t -> err p $ "type violation: expecting pointer type, but got " ++ show t     where     unify' = unify a @@ -179,8 +185,17 @@   (Rational Nothing, a@(Rational _)) -> a   (a@(Rational _), Rational Nothing) -> a -  (a, b) -> unexpected n $ "type violation: " ++ show a ++ " incompatiable with " ++ show b+  (a, b) -> err n $ "type violation: " ++ show a ++ " incompatiable with " ++ show b +typeCheckModel :: Model -> Model+typeCheckModel m = m { actions = map typeCheckAction $ actions m }++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+ true :: E true = Const $ CBool True nopos @@ -191,8 +206,8 @@  data Action   = Assign V E-  | Assert E [String] Position-  | Assume E [String] Position+  | Assert E [String]+  | Assume E [String]   deriving (Show, Eq)  data Model = Model
src/Utils.hs view
@@ -77,8 +77,8 @@     (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+    (0, 0, 0, 0, 0, 0, 0, 0, 1, 0) -> Rational $ Just Float+    (0, 0, 0, 0, 0, 0, 0, 0, 0, 1) -> Rational $ Just Double      a -> notSupported (head specs) $ "type signature: " ++ show a
src/Verify.hs view
@@ -7,6 +7,7 @@ import System.IO import Text.Printf +import Error import Model  -- | Verify a model with k-induction.@@ -15,15 +16,16 @@ verify yices maxK m = do   mapM_ (verifyModel yices format maxK) models   where-  assertions = [ a | a@(Assert _ _ _) <- actions m ]-  models = map (trimModel . trimAssertions m) assertions-  format = "verifying %-" ++ show (maximum [ length (intercalate "." n) | (Assert _ n _) <- actions m ]) ++ "s    "+  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    "  -- | 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 b@(Assert _ _) = a == b   keep _ = True  -- | Trim all unneeded stuff from a model.@@ -38,21 +40,23 @@   execStateT (check env0 1) env0   return ()   where-  [path] = [ path | Assert _ path _ <- actions m ]+  [path] = [ 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    -> liftIO $ printf "FAILED: disproved basis in k = %d\n" k+      Problem -> return ()       Pass -> do         resultStep <- checkStep         case resultStep of-          Fail -> check env0 (k + 1)-          Pass -> liftIO $ printf "passed: proved step in k = %d\n" k+          Fail    -> check env0 (k + 1)+          Problem -> return ()+          Pass    -> liftIO $ printf "passed: proved step in k = %d\n" k         -data Result = Pass | Fail+data Result = Pass | Fail | Problem  -- | Check induction step. checkStep :: Y Result@@ -72,6 +76,7 @@ result a = case a of   Sat _   -> Fail   UnSat _ -> Pass+  InCon _ -> Problem   _ -> error $ "unexpected yices results: " ++ show a  @@ -86,11 +91,11 @@     v <- addVar v     Env y i table cmds asserts <- get     put $ Env y i table (ASSERT (VarE v := e) : cmds) asserts-  Assert a _ _ -> do+  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+  Assume a _ -> do     a <- expr Bool a     Env y i table cmds asserts <- get     put $ Env y i table (ASSERT a : cmds) asserts@@ -160,6 +165,9 @@     c <- expr t' c     return $ IF a b c +  Ref _ _ -> notSupported a "address-of operator"+  Deref _ _ -> notSupported a "indirection operator"+ exprConst :: Type -> Const -> ExpY exprConst t a = case a of    CBool     a _ -> LitB a@@ -201,7 +209,8 @@  typeY :: TypeOf a => a -> String typeY a = case typeOf a of-  Void       -> error "Verify.typeY: void time"+  Void       -> error "Verify.typeY: void"+  Ptr _      -> error "Verify.typeY: ptr"   Bool       -> "bool"   Integer  _ -> "int"   Rational _ -> "real"