| {- LANGUAGE DeriveAnyClass #-} |
| {-# LANGUAGE DisambiguateRecordFields #-} |
| {-# LANGUAGE DuplicateRecordFields #-} |
| {-# LANGUAGE FlexibleInstances #-} |
| {-# LANGUAGE ForeignFunctionInterface #-} |
| {-# LANGUAGE LambdaCase #-} |
| {-# LANGUAGE MultiWayIf #-} |
| {-# LANGUAGE NamedFieldPuns #-} |
| {-# LANGUAGE NoMonomorphismRestriction #-} |
| {-# LANGUAGE PartialTypeSignatures #-} |
| {-# LANGUAGE RebindableSyntax #-} |
| {- LANGUAGE ImplicitPrelude #-} |
| {-# LANGUAGE RecordWildCards #-} |
| {-# LANGUAGE ScopedTypeVariables #-} |
| {- LANGUAGE StandaloneDeriving #-} |
| {-# LANGUAGE TemplateHaskell #-} |
| {-# LANGUAGE TypeSynonymInstances #-} |
| |
| {-# OPTIONS_GHC -Wno-missing-fields #-} |
| {- OPTIONS_GHC -F -pgmFderive -optF-F #-} |
| |
| module Fsm where |
| |
| import Control.Monad.State |
| import Data.Set as S |
| import Foreign |
| import Foreign.C.String hiding (CString) |
| import Foreign.C.Types |
| import Foreign.Marshal.Alloc |
| import Foreign.Ptr |
| import Foreign.Storable |
| import Prelude |
| import Test.QuickCheck hiding (Success) |
| import Test.QuickCheck.Arbitrary |
| import Test.QuickCheck.Gen |
| import Test.QuickCheck.Monadic |
| |
| import CogentMonad hiding (return, (>>=), (>>)) |
| import qualified CogentMonad as CogentMonad |
| import Corres |
| import qualified FFI as FFI |
| import Fsm_Shallow_Desugar |
| -- import WordArray |
| import Util |
| |
| |
| run_cogent_fsm_init = do |
| mnt_st <- generate gen_MountState |
| fsm_st <- generate gen_FsmState |
| cogent_fsm_init mnt_st fsm_st |
| |
| |
| |
| hs_fsm_init_nd :: MountState -> FsmState -> Cogent_monad (Either ErrCode FsmState) |
| hs_fsm_init_nd mount_st fsm_st = do |
| let nb_eb' = nb_eb (super mount_st) |
| ((return $ Left eNoMem) `alternative` (return $ Right $ replicate (fromIntegral nb_eb') 0)) >>= \case |
| Left e -> return $ Left e |
| Right used_eb -> |
| ((return $ Left eNoMem) `alternative` (return $ Right $ replicate (fromIntegral nb_eb') 0)) >>= \case |
| Left e -> return $ Left e |
| Right dirty_space -> |
| let nb_free_eb = nb_eb' - bilbyFsFirstLogEbNum in |
| (return $ Left eNoMem) `alternative` (return $ Right $ fsm_st { used_eb, dirty_space, nb_free_eb }) |
| where (>>=) = (CogentMonad.>>=) |
| return = (CogentMonad.return) |
| (>>) = (CogentMonad.>>) |
| |
| hs_fsm_init :: MountState -> FsmState -> State [Bool] (Either ErrCode FsmState) |
| hs_fsm_init mount_st fsm_st = do |
| let nb_eb' = nb_eb (super mount_st) |
| d <- pop |
| if | not d -> return $ Left eNoMem |
| | otherwise -> do |
| let used_eb = replicate (fromIntegral nb_eb') 0 |
| d <- pop |
| if | not d -> return $ Left eNoMem |
| | otherwise -> do |
| let dirty_space = replicate (fromIntegral nb_eb') 0 |
| nb_free_eb = nb_eb' - bilbyFsFirstLogEbNum |
| return $ Right $ fsm_st { used_eb, dirty_space, nb_free_eb } |
| where |
| pop :: State [a] a |
| pop = get >>= \(d:ds) -> put ds >> return d |
| |
| cogent_fsm_init :: MountState -> FsmState -> IO (Either ErrCode FsmState, [Bool]) |
| cogent_fsm_init mount_st fsm_st = do |
| p_arg <- new =<< mk_fsm_init_arg mount_st fsm_st |
| p_ret <- c_fsm_init p_arg |
| -- putStrLn $ "p_ret = " ++ show p_ret |
| rets <- peek p_ret |
| -- putStrLn $ "ret = " ++ show ret |
| mk_fsm_init_ret rets |
| |
| foreign import ccall unsafe "fsm_wrapper_pp_inferred.c ffi_fsm_init" |
| c_fsm_init :: Ptr FFI.Ct21 -> IO (Ptr FFI.Cffi_fsm_init_ds) |
| |
| release_fsm_init :: Either ErrCode FsmState -> IO () |
| release_fsm_init (Left _) = return () |
| release_fsm_init (Right r) = conv_FsmState r >>= new >>= c_destroy_Ct20 |
| |
| foreign import ccall unsafe "fsm_wrapper_pp_inferred.c ffi_destroy_Ct20" |
| c_destroy_Ct20 :: Ptr FFI.Ct20 -> IO () |
| |
| |
| |
| {------------------------------------------------------------------------------- |
| |
| +-------------------------+ |
| | abstract Isabelle specs | |
| +-------------------------+ |
| ^ |
| | refines (proof) |
| | |
| +-------------------------+ generates +----------------------------+ |
| | Isabelle embedding |<~~~~~~~~~~~~~~~~| non-det version of Hs spec |<------+ |
| +-------------------------+ +----------------------------+ | |
| ^ | |
| | refines (qc) | |
| | | |
| +-----------------------------------+ | |
| | det version of Hs executable spec |<---+ generates with hints |
| +-----------------------------------+ | |
| ^ / |
| | refines (qc) / |
| | / |
| +-------------------------+ generates +-------------------+ / |
| | Cogent/C implementation | ~~~~~~~~~~~~~~~~~~>| Haskell embedding | (QC arbitrary gen here) |
| +-------------------------+ +-------------------+ | |
| ^ | |
| | generates | |
| \-----------------------------------------------------------------/ |
| |
| |
| -------------------------------------------------------------------------------} |
| |
| |
| |
| gen_MountState :: Gen MountState |
| gen_MountState = arbitrary |
| |
| gen_FsmState :: Gen FsmState |
| gen_FsmState = arbitrary |
| |
| -- the following two functions are for performance testing |
| prop_hs_fsm_init = monadicIO $ forAllM gen_MountState $ \mount_st -> |
| forAllM gen_FsmState $ \fsm_st -> run $ do |
| ra <- return $ hs_fsm_init_nd mount_st fsm_st |
| return $ ra `seq` True |
| |
| prop_cogent_fsm_init = monadicIO $ forAllM gen_MountState $ \mount_st -> |
| forAllM gen_FsmState $ \fsm_st -> run $ do |
| (rc,_) <- cogent_fsm_init mount_st fsm_st |
| release_fsm_init rc |
| return True |
| |
| {- This is an instance of the core corres theorem -} |
| prop_fsm_init_corres = monadicIO $ forAllM gen_MountState $ \mount_st -> |
| forAllM gen_FsmState $ \fsm_st -> run $ do |
| (rc,_) <- cogent_fsm_init mount_st fsm_st |
| ra <- return $ hs_fsm_init_nd mount_st fsm_st |
| r <- return $ corres fsm_init_ret_rel ra rc |
| release_fsm_init rc |
| return r |
| |
| fsm_init_ret_rel :: Either ErrCode FsmState -> Either ErrCode FsmState -> Bool |
| fsm_init_ret_rel (Left l1) (Left l2) = l1 == l2 |
| fsm_init_ret_rel (Right (R27 f1 f2 f3 f4)) (Right (R27 f1' f2' f3' f4')) = f1 == f1' && f2 == f2' && f3 == f3' |
| fsm_init_ret_rel _ _ = False |
| |
| |
| prop_fsm_init_corres' = monadicIO $ forAllM gen_MountState $ \mount_st -> |
| forAllM gen_FsmState $ \fsm_st -> run $ do |
| (ra,ds) <- cogent_fsm_init mount_st fsm_st |
| rc <- return $ evalState (hs_fsm_init mount_st fsm_st) ds |
| r <- return $ corres' fsm_init_ret_rel ra rc |
| release_fsm_init ra |
| return r |
| |
| prop_fsm_init_det_corres_det = forAll gen_MountState $ \mount_st -> |
| forAll gen_FsmState $ \fsm_st -> |
| forAll (vectorOf 2 (arbitrary :: Gen Bool)) $ \ds -> do |
| let rnd = hs_fsm_init_nd mount_st fsm_st |
| rd = evalState (hs_fsm_init mount_st fsm_st) ds |
| in corres fsm_init_ret_rel rnd rd |
| |
| {- Some trivial properties on top of the non-det Hs spec -} |
| prop_fsm_init_nb_free_eb = forAll gen_MountState $ \mount_st -> |
| forAll gen_FsmState $ \fsm_st -> |
| nb_eb (super mount_st) >= bilbyFsFirstLogEbNum ==> |
| let rs = hs_fsm_init_nd mount_st fsm_st |
| in all (\r -> case r of |
| Left _ -> True |
| Right s -> nb_free_eb s <= nb_eb (super mount_st)) rs |
| |
| -- //////////////////////////////////////////////////////////////////////////// |
| -- data conversion functions |
| |
| conv_ObjSuper :: ObjSuper -> IO FFI.Ct9 |
| conv_ObjSuper (R26 {..}) = |
| return $ FFI.Ct9 { FFI.nb_eb = fromIntegral nb_eb |
| , FFI.eb_size = fromIntegral eb_size |
| , FFI.io_size = fromIntegral io_size |
| , FFI.nb_reserved_gc = fromIntegral nb_reserved_gc |
| , FFI.nb_reserved_del = fromIntegral nb_reserved_del |
| , FFI.cur_eb = fromIntegral cur_eb |
| , FFI.cur_offs = fromIntegral cur_offs |
| , FFI.last_inum = fromIntegral last_inum |
| , FFI.next_sqnum = fromIntegral next_sqnum |
| } |
| |
| conv_ObjData :: ObjData -> IO FFI.Ct10 |
| conv_ObjData (R21 {..}) = do |
| p_odata <- new =<< conv_WordArray (return . fromIntegral) odata |
| return $ FFI.Ct10 (fromIntegral id) p_odata |
| |
| conv_ObjDel :: ObjDel -> IO FFI.Ct11 |
| conv_ObjDel (R19 x) = return $ FFI.Ct11 $ fromIntegral x |
| |
| conv_ObjDentry :: ObjDentry -> IO FFI.Ct12 |
| conv_ObjDentry (R24 {..}) = do |
| p_name <- new =<< conv_WordArray (return . fromIntegral) name |
| return $ FFI.Ct12 { FFI.ino = fromIntegral ino |
| , FFI.dtype = fromIntegral dtype |
| , FFI.nlen = fromIntegral nlen |
| , FFI.name = p_name |
| } |
| |
| conv_Array :: (Storable t') => (t -> IO t') -> Array t -> IO (FFI.CArray t') |
| conv_Array f xs = do |
| p_values <- newArray =<< mapM f xs |
| p_p_values <- new p_values |
| return $ FFI.CArray (CInt $ fromIntegral $ length xs) p_p_values |
| |
| conv_ObjDentarr :: ObjDentarr -> IO FFI.Ct13 |
| conv_ObjDentarr (R20 {..}) = do |
| p_entries <- new =<< conv_Array conv_ObjDentry entries |
| return $ FFI.Ct13 { id = fromIntegral id |
| , nb_dentry = fromIntegral nb_dentry |
| , entries = p_entries |
| } |
| |
| conv_ObjInode :: ObjInode -> IO FFI.Ct14 |
| conv_ObjInode (R22 {..}) = |
| return $ FFI.Ct14 { FFI.id = fromIntegral id |
| , FFI.size = fromIntegral size |
| , FFI.atime_sec = fromIntegral atime_sec |
| , FFI.ctime_sec = fromIntegral ctime_sec |
| , FFI.mtime_sec = fromIntegral mtime_sec |
| , FFI.nlink = fromIntegral nlink |
| , FFI.uid = fromIntegral uid |
| , FFI.gid = fromIntegral gid |
| , FFI.mode = fromIntegral mode |
| , FFI.flags = fromIntegral flags |
| } |
| |
| conv_WordArray :: (Storable t') => (t -> IO t') -> WordArray t -> IO (FFI.CWordArray t') |
| conv_WordArray f xs = FFI.CWordArray (fromIntegral $ length xs) <$> (newArray =<< mapM f xs) |
| |
| conv_ObjSumEntry :: ObjSumEntry -> IO (FFI.Ct15) |
| conv_ObjSumEntry (R23 {..}) = |
| return $ FFI.Ct15 { FFI.id = fromIntegral id |
| , FFI.sqnum = fromIntegral sqnum |
| , FFI.len = fromIntegral len |
| , FFI.del_flags_and_offs = fromIntegral del_flags_and_offs |
| , FFI.count = fromIntegral count |
| } |
| |
| conv_ObjSummary :: ObjSummary -> IO FFI.Ct16 |
| conv_ObjSummary (R28 {..}) = do |
| p_entries <- new =<< conv_WordArray conv_ObjSumEntry entries |
| return $ FFI.Ct16 { FFI.nb_sum_entry = fromIntegral nb_sum_entry |
| , FFI.entries = p_entries |
| , FFI.sum_offs = fromIntegral sum_offs |
| } |
| |
| conv_ObjUnion :: ObjUnion -> IO FFI.Ct17 |
| conv_ObjUnion ounion = do |
| let def_data = FFI.Ct10 {id = 0, odata = nullPtr} |
| def_del = FFI.Ct11 {id = 0} |
| def_dentarr = nullPtr |
| def_inode = nullPtr |
| def_pad = const_unit |
| def_summary = nullPtr |
| def_super = nullPtr |
| o = FFI.Ct17 undefined def_data def_del def_dentarr def_inode def_pad def_summary def_super |
| case ounion of |
| TObjData t -> conv_ObjData t >>= \x -> return $ o { FFI.tag = Ctag_t $ fromIntegral $ fromEnum FFI.tag_ENUM_TObjData , FFI.tObjData = x } |
| TObjDel t -> conv_ObjDel t >>= \x -> return $ o { FFI.tag = Ctag_t $ fromIntegral $ fromEnum FFI.tag_ENUM_TObjDel , FFI.tObjDel = x } |
| TObjDentarr t -> conv_ObjDentarr t >>= new >>= \x -> return $ o { FFI.tag = Ctag_t $ fromIntegral $ fromEnum FFI.tag_ENUM_TObjDentarr, FFI.tObjDentarr = x } |
| TObjInode t -> conv_ObjInode t >>= new >>= \x -> return $ o { FFI.tag = Ctag_t $ fromIntegral $ fromEnum FFI.tag_ENUM_TObjInode , FFI.tObjInode = x } |
| TObjPad t -> return $ o { FFI.tag = Ctag_t $ fromIntegral $ fromEnum FFI.tag_ENUM_TObjPad , FFI.tObjPad = const_unit } |
| TObjSummary t -> conv_ObjSummary t >>= new >>= \x -> return $ o { FFI.tag = Ctag_t $ fromIntegral $ fromEnum FFI.tag_ENUM_TObjSummary, FFI.tObjSummary = x } |
| TObjSuper t -> conv_ObjSuper t >>= new >>= \x -> return $ o { FFI.tag = Ctag_t $ fromIntegral $ fromEnum FFI.tag_ENUM_TObjSuper , FFI.tObjSuper = x } |
| |
| conv_Obj :: Obj -> IO FFI.Ct18 |
| conv_Obj (R25 {..}) = do |
| ounion' <- conv_ObjUnion ounion |
| return $ FFI.Ct18 { FFI.magic = fromIntegral magic |
| , FFI.crc = fromIntegral crc |
| , FFI.sqnum = fromIntegral sqnum |
| , FFI.offs = fromIntegral offs |
| , FFI.trans = fromIntegral trans |
| , FFI.otype = fromIntegral otype |
| , FFI.ounion = ounion' |
| } |
| |
| conv_UbiVolInfo :: UbiVolInfo -> IO FFI.CUbiVolInfo |
| conv_UbiVolInfo = return |
| |
| conv_UbiDevInfo :: UbiDevInfo -> IO FFI.CUbiDevInfo |
| conv_UbiDevInfo = return |
| |
| conv_MountState :: MountState -> IO FFI.Ct19 |
| conv_MountState (R11 {..}) = do |
| p_super <- new =<< conv_ObjSuper super |
| p_obj_sup <- new =<< conv_Obj obj_sup |
| p_vol <- new =<< conv_UbiVolInfo vol |
| p_dev <- new =<< conv_UbiDevInfo dev |
| return $ FFI.Ct19 { eb_recovery = fromIntegral eb_recovery |
| , eb_recovery_offs = fromIntegral eb_recovery_offs |
| , super = p_super |
| , obj_sup = p_obj_sup |
| , super_offs = fromIntegral super_offs |
| , vol = p_vol |
| , dev = p_dev |
| , no_summary = Cbool_t $ CUChar $ fromIntegral $ fromEnum no_summary |
| } |
| |
| conv_GimNode :: GimNode -> IO FFI.Ct3 |
| conv_GimNode (R10 {..}) = return $ FFI.Ct3 (fromIntegral count) (fromIntegral sqnum) |
| |
| -- Rbt is not refined |
| conv_Rbt :: (Storable k', Storable v') => (k -> IO k') -> (v -> IO v') -> Rbt k v -> IO (FFI.CRbt k' v') |
| conv_Rbt fk fv t = ttraverse fk =<< traverse fv t |
| |
| conv_FsmState :: FsmState -> IO FFI.Ct20 |
| conv_FsmState (R27 {..}) = do |
| p_used_eb <- new =<< conv_WordArray (return . fromIntegral) used_eb |
| p_dirty_space <- new =<< conv_WordArray (return . fromIntegral) dirty_space |
| p_gim <- new =<< conv_Rbt (return . fromIntegral) conv_GimNode gim |
| return $ FFI.Ct20 { nb_free_eb = fromIntegral nb_free_eb |
| , used_eb = p_used_eb |
| , dirty_space = p_dirty_space |
| , gim = p_gim |
| } |
| |
| mk_fsm_init_arg :: MountState -> FsmState -> IO FFI.Ct21 |
| mk_fsm_init_arg mount_st fsm_st = do |
| p_sys_st <- pDummyCSysState |
| p_mount_st <- new =<< conv_MountState mount_st |
| p_fsm_st <- new =<< conv_FsmState fsm_st |
| return $ FFI.Ct21 { p1 = p_sys_st, p2 = p_mount_st, p3 = p_fsm_st } |
| |
| conv_Ct22 :: FFI.Ct22 -> IO ErrCode |
| conv_Ct22 (FFI.Ct22 {..}) = return $ fromIntegral p1 |
| |
| conv_CWordArray :: (Storable t) => (t -> IO t') -> FFI.CWordArray t -> IO (WordArray t') |
| conv_CWordArray f (FFI.CWordArray {..}) = mapM f =<< peekArray (fromIntegral len) values |
| |
| conv_Ct3 :: FFI.Ct3 -> IO GimNode |
| conv_Ct3 (FFI.Ct3 {..}) = return $ R10 (fromIntegral count) (fromIntegral sqnum) |
| |
| conv_CRbt :: (Storable k, Storable v) => (k -> IO k') -> (v -> IO v') -> FFI.CRbt k v -> IO (Rbt k' v') |
| conv_CRbt fk fv t = ttraverse fk =<< traverse fv t |
| |
| conv_Ct20 :: FFI.Ct20 -> IO FsmState |
| conv_Ct20 (FFI.Ct20 {..}) = do |
| p_used_eb <- peek used_eb >>= conv_CWordArray (return . fromIntegral) |
| p_dirty_space <- peek dirty_space >>= conv_CWordArray (return . fromIntegral) |
| p_gim <- peek gim >>= conv_CRbt (return . fromIntegral) conv_Ct3 |
| return $ R27 (fromIntegral nb_free_eb) p_used_eb p_dirty_space p_gim |
| |
| conv_Ct23 :: FFI.Ct23 -> IO (Either ErrCode FsmState) |
| conv_Ct23 (FFI.Ct23 {..}) = do |
| let Ctag_t t = tag |
| if | fromIntegral t == fromEnum FFI.tag_ENUM_Error -> conv_Ct22 error >>= return . Left |
| | fromIntegral t == fromEnum FFI.tag_ENUM_Success -> (conv_Ct20 =<< peek success) >>= return . Right |
| | otherwise -> Prelude.error $ "Tag is " ++ show (fromIntegral t) |
| |
| conv_Ct24 :: FFI.Ct24 -> IO (Either ErrCode FsmState) |
| conv_Ct24 (FFI.Ct24 {..}) = conv_Ct23 p2 |
| |
| mk_fsm_init_ret :: FFI.Cffi_fsm_init_ds -> IO (Either ErrCode FsmState, [Bool]) |
| mk_fsm_init_ret (FFI.Cffi_fsm_init_ds p_ret p_ds) = do |
| ret <- peek p_ret |
| ret' <- conv_Ct24 ret |
| ds' <- peekArray 2 p_ds |
| return $ (ret', ds') |
| |
| |
| -- //////////////////////////////////////////////////////////////////////////// |
| -- main function |
| |
| return [] |
| main = $quickCheckAll |
| |
