-
Notifications
You must be signed in to change notification settings - Fork 27
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Zilin Chen
authored and
Zilin Chen
committed
Mar 6, 2018
1 parent
3f6e6ab
commit c29487d
Showing
1 changed file
with
11 additions
and
65 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,79 +1,25 @@ | ||
| type ExState | ||
| type Array a | ||
| type WordArray a | ||
| type VfsMountInfo | ||
| type RR c a b = (c, <Success a | Error b>) | ||
| type Option a = <Some a | None ()> | ||
| type BlockOffset | ||
| type Indirect | ||
| type Chain | ||
| type BlockPtr | ||
| type OSBuffer | ||
|
|
||
| type FsState = { | ||
| super : Ext2Superblock, | ||
| super_buf : OSBuffer, | ||
| superblock_num : U32, | ||
| group_count : U32, | ||
| inode_tables_per_group : U32, | ||
| flags : U32, | ||
| cur_overhead : U32, | ||
| group_desc_array : Array OSBuffer, | ||
| prealloc_offsets : Option (WordArray BlockOffset), -- for Path | ||
| prealloc_indirects : Option (Array Indirect), -- for Chain | ||
| prealloc_chain : Option (Chain), | ||
| prealloc_blockptrs : Option (WordArray BlockPtr) -- for block allocation | ||
| } | ||
|
|
||
| type Ext2Superblock = { | ||
| inode_count : U32, | ||
| magic : U16 | ||
| } | ||
|
|
||
| osbuffer_create: ExState -> RR ExState OSBuffer () | ||
| malloc_FsState: ExState -> RR ExState (FsState take (..)) () | ||
| get_superblock_num: (ExState, (Array (WordArray U8))!) -> (ExState, U32) | ||
| osbuffer_read_block: (#{ex: ExState, buf: OSBuffer, blk: U32}) -> RR (ExState, OSBuffer) () () | ||
| deserialise_Ext2Superblock: (ExState, OSBuffer!, U32) -> RR ExState (Ext2Superblock, U32) () | ||
|
|
||
| free_Ext2Superblock : (ExState, Ext2Superblock take (..)) -> ExState | ||
| free_Ext2Superblock' : (ExState, Ext2Superblock) -> ExState | ||
| free_FsState: (ExState, FsState take (..)) -> ExState | ||
| osbuffer_destroy: (ExState, OSBuffer) -> (ExState) | ||
|
|
||
|
|
||
| fs_mount: #{ex: ExState, options: (Array (WordArray U8))!} -> RR ExState #{state: FsState, mountinfo: #VfsMountInfo} U32 | ||
| fs_mount #{ex, options} = | ||
| let (ex, res) = malloc_FsState ex | ||
| in res | ||
| | Success state_t -> | ||
| let (ex, res) = osbuffer_create ex | ||
| in res | ||
| | Success buf_super -> | ||
| let (ex, sb_num) = get_superblock_num (ex, options) !options | ||
| -- and state_t = state_t { superblock_num = sb_num } | ||
| and ((ex, buf_super), res) = osbuffer_read_block #{ex, buf = buf_super, blk = sb_num} | ||
| in res | ||
| | Success () -> | ||
| let (ex, res) = deserialise_Ext2Superblock (ex, buf_super, 0) !buf_super | ||
| in res | ||
| | Success (super, _) -> | ||
| let super' = super {inode_count = 1, magic = 2} | ||
| and ex = free_Ext2Superblock (ex,super') | ||
| and ex = free_FsState (ex, state_t) | ||
| and ex = osbuffer_destroy (ex, buf_super) | ||
| in (ex, Error 1) | ||
| | Error () -> | ||
| let ex = osbuffer_destroy (ex, buf_super) | ||
| and ex = free_FsState (ex, state_t) | ||
| in (ex, Error 1) | ||
| | Error () -> | ||
| let ex = osbuffer_destroy (ex, buf_super) | ||
| and ex = free_FsState (ex, state_t) | ||
| in (ex, Error 1) | ||
| | Error () -> | ||
| let ex = free_FsState (ex, state_t) | ||
| in (ex, Error 1) | ||
| | Error () -> | ||
| (ex, Error 1) | ||
|
|
||
| foo : #{ex: ExState, buf_super : OSBuffer} -> ExState | ||
| foo #{ex, buf_super} = | ||
| let (ex, res) = deserialise_Ext2Superblock (ex, buf_super, 0) !buf_super | ||
| in res | ||
| | Success (super, _) -> | ||
| -- let super' = super {inode_count = 1, magic = 2} -- infers super' to be all taken, wrong! | ||
| -- and ex = free_Ext2Superblock (ex, super') | ||
| let ex = free_Ext2Superblock (ex, super) -- super is all-untaken | ||
| in ex | ||
| | Error () -> ex | ||
|
|