| {-# LANGUAGE FlexibleContexts #-} |
| {-# LANGUAGE MultiWayIf #-} |
| {-# LANGUAGE RankNTypes #-} |
| |
| module AfsS where |
| |
| import CogentMonad as C |
| import qualified Fsop_Shallow_Desugar as D |
| import FunBucket |
| import List |
| import VfsT |
| import WordArrayT |
| |
| import Data.Bits |
| import qualified Data.Map as M |
| import Data.Maybe (fromJust) |
| import Data.Set as S (Set, singleton, map, fromList) |
| import Prelude as P |
| |
| type Byte = U8 |
| type Page = [U8] |
| type Dir = M.Map [U8] Ino |
| type File_data = [Page] |
| |
| data Afs_inode_type = IDir Dir |
| | IReg File_data |
| | ILnk [U8] |
| |
| -- TODO: a few afs_inode_is_ definitions |
| |
| data Afs_inode = Afs_inode { |
| i_type :: Afs_inode_type |
| , i_ino :: Ino |
| , i_nlink :: U32 |
| , i_size :: U64 |
| , i_mtime :: TimeT |
| , i_ctime :: TimeT |
| , i_uid :: U32 |
| , i_gid :: U32 |
| , i_mode :: Mode |
| , i_flags :: U32 |
| } |
| |
| |
| type Readdir_ctx = (U32, Dir) |
| |
| type Afs_map = M.Map Ino Afs_inode |
| |
| data Afs_state = Afs_state { |
| a_is_readonly :: Bool |
| , a_current_time :: TimeT |
| , a_medium_afs :: Afs_map |
| , a_medium_updates :: [Afs_map -> Afs_map] |
| } |
| |
| a_medium_afs_update :: (Afs_map -> Afs_map) -> Afs_state -> Afs_state |
| a_medium_afs_update f s = let Afs_state a b c d = s |
| in Afs_state a b (f c) d |
| |
| a_medium_updates_update :: ([Afs_map -> Afs_map] -> [Afs_map -> Afs_map]) -> Afs_state -> Afs_state |
| a_medium_updates_update f s = let Afs_state a b c d = s |
| in Afs_state a b c (f d) |
| |
| |
| a_afs_update_n :: Int -> Afs_map -> [Afs_map -> Afs_map] -> Afs_map |
| a_afs_update_n n afs_st updates = foldr P.id afs_st (take n updates) |
| |
| a_afs_updated :: Afs_map -> [Afs_map -> Afs_map] -> Afs_map |
| a_afs_updated afs_st updates = a_afs_update_n (length updates) afs_st updates |
| |
| updated_afs :: Afs_state -> Afs_map |
| updated_afs adata = a_afs_updated (a_medium_afs adata) (a_medium_updates adata) |
| |
| i_type_dir :: Afs_inode_type -> Dir |
| i_type_dir it = case it of IDir dir -> dir |
| |
| i_dir :: Afs_inode -> Dir |
| i_dir = i_type_dir . i_type |
| |
| i_dir_update :: (Dir -> Dir) -> Afs_inode -> Afs_inode |
| i_dir_update m i = i { i_type = IDir (m $ i_dir i) } |
| |
| i_type_data :: Afs_inode_type -> File_data |
| i_type_data it = case it of IReg dat -> dat -- change from `data` to `dat` to avoid keyword |
| |
| i_data :: Afs_inode -> File_data |
| i_data = i_type_data . i_type |
| |
| i_data_update :: (File_data -> File_data) -> Afs_inode -> Afs_inode |
| i_data_update m i = i { i_type = IReg (m $ i_data i) } |
| |
| i_type_path :: Afs_inode_type -> [Byte] |
| i_type_path it = case it of ILnk path -> path |
| |
| i_path :: Afs_inode -> [Byte] |
| i_path = i_type_path . i_type |
| |
| i_path_update :: ([Byte] -> [Byte]) -> Afs_inode -> Afs_inode |
| i_path_update m i = i { i_type = ILnk (m $ i_path i) } |
| |
| |
| i_size_from_afs_inode_type :: Afs_inode_type -> U64 |
| i_size_from_afs_inode_type (IDir dir) = undefined |
| i_size_from_afs_inode_type (IReg dat) = count (concat dat) |
| i_size_from_afs_inode_type (ILnk path) = count path |
| |
| i_size_from_type :: Afs_inode -> U64 |
| i_size_from_type = i_size_from_afs_inode_type . i_type |
| |
| afs_inode_to_vnode :: Afs_inode -> VfsInode |
| afs_inode_to_vnode i = VfsInode { |
| v_ino = i_ino i |
| , v_nlink = i_nlink i |
| , v_size = i_size i |
| , v_mtime = i_mtime i |
| , v_ctime = i_ctime i |
| , v_uid = i_uid i |
| , v_gid = i_gid i |
| , v_mode = i_mode i |
| , v_flags = i_flags i |
| } |
| |
| afs_inode_from_vnode :: Vnode -> Afs_inode |
| afs_inode_from_vnode v = Afs_inode { |
| i_type = if | v_mode v .&. s_IFREG /= 0 -> IReg [] |
| | v_mode v .&. s_IFDIR /= 0 -> IDir M.empty |
| | otherwise -> ILnk [] |
| , i_ino = v_ino v |
| , i_nlink = v_nlink v |
| , i_size = v_size v |
| , i_mtime = v_mtime v |
| , i_ctime = v_ctime v |
| , i_uid = v_uid v |
| , i_gid = v_gid v |
| , i_mode = v_mode v |
| , i_flags = v_flags v |
| } |
| |
| error_if_readonly :: Afs_state -> Cogent_monad (D.R Afs_state (D.ErrCode, Afs_state)) |
| error_if_readonly as = return $ if a_is_readonly as |
| then D.Error (eRoFs, as) |
| else D.Success as |
| |
| nondet_error :: Set D.ErrCode -> (D.ErrCode -> a) -> Cogent_monad a |
| nondet_error errs f = C.select errs >>= (return . f) |
| |
| afs_alloc_inum :: Afs_map -> Cogent_monad (D.R Ino ()) |
| afs_alloc_inum as = do |
| let avail_inums = S.map negate $ M.keysSet as |
| opt_inum <- select $ S.singleton Nothing `union` (Just `image` avail_inums) |
| return $ if opt_inum == Nothing then D.Error () else D.Success (fromJust opt_inum) |
| |
| afs_get_current_time :: Afs_state -> Cogent_monad (Afs_state, TimeT) |
| afs_get_current_time afs = do |
| time' <- return $ a_current_time afs |
| time <- select (S.fromList [ i | i <- [time' ..] ]) |
| return (afs {a_current_time = time}, time') |
| |
| afs_init_inode :: Afs_state -> Vnode -> Vnode -> D.VfsMode |
| -> Cogent_monad (D.R (Afs_state, Vnode) (Afs_state, Vnode)) |
| afs_init_inode adata vdir vnode mode = do |
| (adata, time) <- afs_get_current_time adata |
| uid <- return (v_uid vdir) |
| gid <- return (v_gid vdir) |
| vnode <- return (vnode {v_ctime = time, v_mtime = time, v_uid = uid, v_gid = gid, |
| v_mode = mode, v_nlink = 1, v_size = 0}) |
| r <- afs_alloc_inum (updated_afs adata) |
| return (case r of D.Error () -> D.Error (adata, vnode) |
| D.Success inum -> D.Success (adata, vnode {v_ino = inum})) |
| |
| read_afs_inode :: Afs_state -> Ino -> Cogent_monad (D.R Afs_inode ErrCode) |
| read_afs_inode adata ino = return (D.Success $ fromJust $ ino `M.lookup` updated_afs adata) `alternative` |
| nondet_error (fromList [eIO, eNoMem, eInval, eBadF]) D.Error |
| |
| afs_apply_updates_nondet :: Afs_state -> Cogent_monad Afs_state |
| afs_apply_updates_nondet afs = do |
| let upds = a_medium_updates afs |
| (to_apply, updates) <- fmap (\i -> splitAt i upds) (fromList [0 .. length upds - 1]) |
| return $ afs {a_medium_afs = fold P.id to_apply (a_medium_afs afs), |
| a_medium_updates = updates} |
| |
| afs_update :: Afs_state -> (Afs_map -> Afs_map) -> Cogent_monad (Afs_state, D.R () D.ErrCode) |
| afs_update afs upd = do |
| afs <- afs_apply_updates_nondet (afs {a_medium_updates = a_medium_updates afs ++ [upd]}) |
| if null $ a_medium_updates afs |
| then return (afs, D.Success ()) |
| else return (afs, D.Success ()) `alternative` |
| nondet_error (fromList $ [eIO, eNoSpc, eNoMem]) (\e -> (afs {a_medium_updates = butlast (a_medium_updates afs)}, D.Error e)) |
| |
| afs_create :: Afs_state -> Vnode -> D.WordArray U8 -> D.VfsMode -> Vnode |
| -> Cogent_monad ((Afs_state, Vnode, Vnode), D.R () D.ErrCode) |
| afs_create afs parentdir name mode vnode = |
| if a_is_readonly afs |
| then return ((afs, parentdir, vnode), D.Error eRoFs) |
| else do |
| r <- afs_init_inode afs parentdir vnode (mode .|. s_IFREG) |
| case r of |
| D.Error (afs, vnode) -> return ((afs, parentdir, vnode), D.Error eNFile) |
| D.Success (afs, vnode) -> do |
| r <- read_afs_inode afs (v_ino parentdir) |
| case r of |
| D.Error e -> return ((afs, parentdir, vnode), D.Error e) |
| D.Success dir -> do |
| r <- return (D.Success $ i_dir_update (\d -> M.adjust (\_ -> v_ino vnode) (alpha_wa name) d) dir) `alternative` return (D.Error eNameTooLong) |
| case r of |
| D.Error e -> return ((afs, parentdir, vnode), D.Error e) |
| D.Success dir -> do |
| r <- select (D.Success `image` fromList [ sz | sz <- [v_size parentdir .. ] ]) `alternative` |
| return (D.Error eOverflow) |
| case r of |
| D.Error e -> return ((afs, parentdir, vnode), D.Error e) |
| D.Success newsz -> do |
| time <- return $ v_ctime vnode |
| dir <- return $ dir {i_ctime = time, i_mtime = time} |
| inode <- return $ afs_inode_from_vnode vnode |
| (afs, r) <- afs_update afs (\f -> M.adjust (flip const inode) (i_ino inode) $ |
| M.adjust (flip const dir) (i_ino dir) f) |
| case r of |
| D.Error e -> return ((afs, parentdir, vnode), D.Error e) |
| D.Success () -> return ((afs, parentdir {v_ctime = time, v_mtime = time, v_size = newsz}, vnode), D.Success ()) |
| |
| afs_sync :: Afs_state -> Cogent_monad (Afs_state, D.R () D.ErrCode) |
| afs_sync afs = |
| if a_is_readonly afs |
| then return (afs, D.Error eRoFs) |
| else do |
| n <- select $ fromList [0 .. length (a_medium_updates afs)] |
| updates <- return $ a_medium_updates afs |
| (to_apply, updates) <- return (take n updates, drop n updates) |
| afs <- return $ a_medium_afs_update (fold (\upd med -> upd med) to_apply) afs |
| afs <- return $ a_medium_updates_update (\_ -> updates) afs |
| if null updates |
| then return (afs, D.Success ()) |
| else do |
| e <- select $ fromList [eIO, eNoMem, eNoSpc, eOverflow] |
| return (afs {a_is_readonly = (e == eIO)}, D.Error e) |
