Skip to content

Commit

Permalink
ext2: new tc passed!!!
Browse files Browse the repository at this point in the history
  • Loading branch information
Zilin Chen authored and Zilin Chen committed Jan 22, 2018
1 parent dc7da46 commit b03d7f5
Show file tree
Hide file tree
Showing 4 changed files with 40 additions and 39 deletions.
7 changes: 4 additions & 3 deletions impl/fs/ext2/cogent/src/dread.cogent
Original file line number Diff line number Diff line change
Expand Up @@ -540,8 +540,9 @@ ext2_inode_by_name (ex, state, inode, name) =
--in ((ex, state, inode), Error err)
in ((ex, state, inode), Error eNoEnt)

fsop_dir_lookup: (#{ex: SysState, state: FsState, parent_inode: VfsInode, name: CString!, flags: VfsFlags}) -> RR #{ex: SysState, state: FsState, parent_inode: VfsInode} VfsInode U32
fsop_dir_lookup (#{ ex = ex, .. }) =
fsop_dir_lookup : #{ex: SysState, state: FsState, parent_inode: VfsInode, name: CString!, flags: VfsFlags}
-> RR #{ex: SysState, state: FsState, parent_inode: VfsInode} VfsInode U32
fsop_dir_lookup #{ex, state, parent_inode, name, flags} =
if wordarray_length [U8] name > const_maxNameLen then
(#{ex, state, parent_inode}, Error eNameTooLong)
else
Expand All @@ -555,7 +556,7 @@ fsop_dir_lookup (#{ ex = ex, .. }) =
in res
| Success inode ->
let _ = _cogent_log (dbg_EXT2_DIR_READ, "fsop_dir_lookup: gave ino ")
and _ = _cogent_log_u32 (dbg_EXT2_DIR_READ, vfs_inode_get_ino (inode)) !inode
and _ = _cogent_log_u32 (dbg_EXT2_DIR_READ, vfs_inode_get_ino inode) !inode
and _ = _cogent_log (dbg_EXT2_DIR_READ, "\n")
in (#{ex, state, parent_inode}, Success inode)
| Error err -> (#{ex, state, parent_inode}, Error err)
Expand Down
24 changes: 12 additions & 12 deletions impl/fs/ext2/cogent/src/dwrite.cogent
Original file line number Diff line number Diff line change
Expand Up @@ -581,30 +581,30 @@ fsop_dir_unlink (ex, state, parent, inode, name) =
-- wrapper should should dirty inode, setup inode ops
fsop_dir_create: (SysState, FsState, VfsInode, CString!, VfsMode) -> RR (SysState, FsState, VfsInode) VfsInode U32
fsop_dir_create (ex, state, parent_inode, name, mode) =
let _ = _cogent_log (dbg_EXT2_DIR_WRITE, ("fsop_dir_create: want to create with mode "))
and _ = _cogent_log_u32 (dbg_EXT2_DIR_WRITE, (mode))
and _ = _cogent_log (dbg_EXT2_DIR_WRITE, ("\n"))
let _ = _cogent_log (dbg_EXT2_DIR_WRITE, "fsop_dir_create: want to create with mode ")
and _ = _cogent_log_u32 (dbg_EXT2_DIR_WRITE, mode)
and _ = _cogent_log (dbg_EXT2_DIR_WRITE, "\n")
and ((ex, state), res) = ext2_inode_create (ex, state, parent_inode, mode) !parent_inode
in res
| Success (new_inode) ->
| Success new_inode ->
let new_inode = vfs_inode_set_ops (new_inode, ext2_reg_inode_ops)
and new_inode = vfs_inode_set_fileops (new_inode, ext2_reg_file_ops)

and _ = _cogent_log (dbg_EXT2_DIR_WRITE, ("fsop_dir_create: created new inode okay; adding to dir\n"))
and _ = _cogent_log (dbg_EXT2_DIR_WRITE, "fsop_dir_create: created new inode okay; adding to dir\n")
and ((ex, state, parent_inode), res) = ext2_dir_add (ex, state, parent_inode, new_inode, name) !new_inode
in res
| Success () ->
let _ = _cogent_log (dbg_EXT2_DIR_WRITE, ("fsop_dir_create: success!\n"))
and new_inode = vfs_inode_unlock_new (new_inode)
let _ = _cogent_log (dbg_EXT2_DIR_WRITE, "fsop_dir_create: success!\n")
and new_inode = vfs_inode_unlock_new new_inode

in ((ex, state, parent_inode), Success new_inode)
| Error (err) ->
let _ = _cogent_log (dbg_EXT2_DIR_WRITE, ("fsop_dir_create: adding new inode to dir failed\n"))
| Error err ->
let _ = _cogent_log (dbg_EXT2_DIR_WRITE, "fsop_dir_create: adding new inode to dir failed\n")

and ex = vfs_inode_bad (#{ex, inode = new_inode})
and ex = vfs_inode_bad #{ex, inode = new_inode}
in ((ex, state, parent_inode), Error err)
| Error (err) ->
let _ = _cogent_log (dbg_EXT2_DIR_WRITE, ("fsop_dir_create: inode creation failed\n"))
| Error err ->
let _ = _cogent_log (dbg_EXT2_DIR_WRITE, "fsop_dir_create: inode creation failed\n")
in ((ex, state, parent_inode), Error err)

------------------------------------------------------------------------------
Expand Down
5 changes: 2 additions & 3 deletions impl/fs/ext2/cogent/src/ialloc.cogent
Original file line number Diff line number Diff line change
Expand Up @@ -363,12 +363,11 @@ ext2_inode_create (ex, state, parent_inode, mode) =
in ((ex, state), Error eNoSpc)

-- this function only used from console for testing
fsop_inode_create: #{ex: SysState, state: FsState, parent_inode: VfsInode!, mode: VfsMode} -> RR #{ex: SysState, state: FsState} (VfsInode) (U32)
fsop_inode_create #{..} =
fsop_inode_create: #{ex: SysState, state: FsState, parent_inode: VfsInode!, mode: VfsMode} -> RR #{ex: SysState, state: FsState} VfsInode U32
fsop_inode_create #{ex, state, parent_inode, mode} =
let ((ex, state), res) = ext2_inode_create (ex, state, parent_inode, mode)
in (#{ex, state}, res)


fsop_inode_mknod: (SysState, FsState, VfsInode, CString!, VfsMode, #VfsDevice) -> RR (SysState, FsState, VfsInode) VfsInode U32
fsop_inode_mknod (ex, state, dir, name, mode, device) =
let ((ex, state), res) = ext2_inode_create (ex, state, dir, mode) !dir
Expand Down
43 changes: 22 additions & 21 deletions impl/fs/ext2/cogent/src/iread.cogent
Original file line number Diff line number Diff line change
Expand Up @@ -184,7 +184,7 @@ ino_block_addr_buffer_offset_from_inotable (state, inode_table, ino) =
and block_addr = inode_table + block_offset
in (block_addr, buffer_offset)

ext2_inode_get_buf: (SysState, FsState, U32) -> RR (SysState, FsState) (OSBuffer, U32) (U32)
ext2_inode_get_buf: (SysState, FsState, U32) -> RR (SysState, FsState) (OSBuffer, U32) U32
ext2_inode_get_buf (ex, state, inode_num) =
if inode_num == 2 || inode_num >= 11 then
let block_group_num = get_block_group_from_ino2 (state, inode_num) !state
Expand All @@ -195,27 +195,27 @@ ext2_inode_get_buf (ex, state, inode_num) =

-- and group_desc_t { .. } = group_desc
-- and ex = free_Ext2GroupDescriptor (ex, group_desc_t)
and _ = _cogent_log (dbg_EXT2_INODE_READ, ("ext2_inode_get_buf: inode "))
and _ = _cogent_log_u32 (dbg_EXT2_INODE_READ, (inode_num))
and _ = _cogent_log (dbg_EXT2_INODE_READ, (" is part of block group "))
and _ = _cogent_log_u32 (dbg_EXT2_INODE_READ, (block_group_num))
and _ = _cogent_log (dbg_EXT2_INODE_READ, ("\n"))
and _ = _cogent_log (dbg_EXT2_INODE_READ, "ext2_inode_get_buf: inode ")
and _ = _cogent_log_u32 (dbg_EXT2_INODE_READ, inode_num)
and _ = _cogent_log (dbg_EXT2_INODE_READ, " is part of block group ")
and _ = _cogent_log_u32 (dbg_EXT2_INODE_READ, block_group_num)
and _ = _cogent_log (dbg_EXT2_INODE_READ, "\n")
and (ex, res) = ext2_get_block (ex, block_addr)
in res
| Success buf_block ->
let _ = _cogent_log (dbg_EXT2_INODE_READ, ("ext2_inode_get_buf: located at block "))
and _ = _cogent_log_u32 (dbg_EXT2_INODE_READ, (block_addr))
and _ = _cogent_log (dbg_EXT2_INODE_READ, (", offset "))
and _ = _cogent_log_u32_hex (dbg_EXT2_INODE_READ, (buffer_offset))
and _ = _cogent_log (dbg_EXT2_INODE_READ, ("\n"))
let _ = _cogent_log (dbg_EXT2_INODE_READ, "ext2_inode_get_buf: located at block ")
and _ = _cogent_log_u32 (dbg_EXT2_INODE_READ, block_addr)
and _ = _cogent_log (dbg_EXT2_INODE_READ, ", offset ")
and _ = _cogent_log_u32_hex (dbg_EXT2_INODE_READ, buffer_offset)
and _ = _cogent_log (dbg_EXT2_INODE_READ, "\n")
in ((ex, state), Success (buf_block, buffer_offset))
| Error () ->
let _ = _cogent_log (dbg_EXT2_INODE_READ, ("ext2_inode_get_buf: couldn't get block "))
let _ = _cogent_log (dbg_EXT2_INODE_READ, "ext2_inode_get_buf: couldn't get block ")
and _ = _cogent_log_u32 (dbg_EXT2_INODE_READ, block_addr)
and _ = _cogent_log (dbg_EXT2_INODE_READ, "\n")
in ((ex, state), Error (eIO))
in ((ex, state), Error eIO)
| Error () ->
let _ = _cogent_warn ("ext2_inode_get_buf: couldn't get group descriptor\n")
let _ = _cogent_warn "ext2_inode_get_buf: couldn't get group descriptor\n"
and _ = _cogent_warn_u32 block_group_num
and _ = _cogent_warn "\n"

Expand All @@ -236,19 +236,20 @@ ext2_inode_get (ex, state, inode_num) =
in ((ex, state), Success inode)
| Error () ->
let ex = osbuffer_destroy (ex, buf_block)
and _ = _cogent_log (dbg_EXT2_INODE_READ, ("ext2_inode_get: failed to deserialise inode\n"))
and _ = _cogent_log (dbg_EXT2_INODE_READ, "ext2_inode_get: failed to deserialise inode\n")
in ((ex, state), Error eIO) -- FIXME: bad error code?
| Error (err) ->
let _ = _cogent_log (dbg_EXT2_INODE_READ, ("ext2_inode_get: could not get buf for inode\n"))
let _ = _cogent_log (dbg_EXT2_INODE_READ, "ext2_inode_get: could not get buf for inode\n")
in ((ex, state), Error err)

fsop_get_root_inode: (#{ex: SysState, state: FsState}) -> RR #{ex: SysState, state: FsState} (VfsInode) (U32)
fsop_get_root_inode (#{ .. }) =
fsop_get_root_inode: #{ex: SysState, state: FsState} -> RR #{ex: SysState, state: FsState} VfsInode U32
fsop_get_root_inode #{ex, state} =
let ((ex, state), res) = ext2_inode_get (ex, state, 2)
in (#{ex, state}, res)

ext2_inode_is_fast_symlink: (VfsInode!) -> Bool
ext2_inode_is_fast_symlink (inode) =
((vfs_inode_get_mode (inode) .&. s_IFMT) == vfs_type_link) && (vfs_inode_get_size (inode) <= 15)
ext2_inode_is_fast_symlink: VfsInode! -> Bool
ext2_inode_is_fast_symlink inode =
((vfs_inode_get_mode inode .&. s_IFMT) == vfs_type_link) && (vfs_inode_get_size inode <= 15)

-- inode_get_block lives in iwrite.cogent

0 comments on commit b03d7f5

Please sign in to comment.