impl/fs/bilby/quickcheck/readpage_example/readpage.cogent

include <gum/common/buffer.cogent>
include <gum/common/common.cogent>
include <gum/common/wordarray.cogent>
include <gum/fs/linux/vfs.cogent>
include <gum/kernel/linux/errno.cogent>

type FsInode = { a: U32 }

type OstoreState
newOstoreState: (SysState) -> R (SysState, OstoreState take (..)) SysState
freeOstoreState: (SysState, OstoreState take (..)) -> SysState

type MountState
newMountState: SysState -> R (SysState, MountState take (..)) SysState
freeMountState: (SysState, MountState take (..)) -> SysState

type FsState = { fsop_st : FsopState
               , mount_st : MountState
               , ostore_st : OstoreState } 
newFsState: (SysState) -> R (SysState, FsState take (..)) SysState
freeFsState: (SysState, FsState take (..)) -> SysState

type FsopState
newFsopState: SysState -> R (SysState, FsopState take (..)) SysState
freeFsopState: (SysState, FsopState take (..)) -> SysState


bilbyFsBlockSize : U32
bilbyFsBlockSize = 4096

bilbyFsBlockShift : U32
bilbyFsBlockShift = 12


type FsopReadPageP = #{ex:SysState, fs_st: FsState, vnode: VfsInode, block: OSPageOffset, addr: Buffer}
type FsopReadPageRR = #{ex:SysState, fs_st: FsState, vnode: VfsInode, addr: Buffer}

fsop_readpage: FsopReadPageP -> RR FsopReadPageRR () ErrCode 
fsop_readpage #{ex, fs_st, vnode, block, addr} =
  -- block has to fit in u32
  let size = vfs_inode_get_size(vnode) !vnode
  and limit = size >> upcast bilbyFsBlockShift
  in if block > limit then
   let addr = buf_memset(addr, 0, bilbyFsBlockSize, 0)
   in (#{ex, fs_st, vnode, addr}, Error eNoEnt)
  else if block == limit && (size % upcast bilbyFsBlockSize == 0) then
    (#{ex, fs_st, vnode, addr}, Success ())
  else
   let ((ex, fs_st, addr), r) = read_block(ex, fs_st, vnode, addr, block) !vnode
   in (#{ex, fs_st, vnode, addr}, r) 

read_block:(SysState, FsState, VfsInode!, Buffer, OSPageOffset) -> RR (SysState, FsState, Buffer) () ErrCode
read_block(ex, fs_st {ostore_st}, vnode, buf, block) =
  let oid = obj_id_data_mk(vfs_inode_get_ino(vnode), u64_to_u32(block)) !vnode
  and ((ex, ostore_st), r) = ostore_read(ex, fs_st.mount_st, ostore_st, oid) !fs_st
  and fs_st = fs_st {ostore_st}
  in r
  | Error e ->
    if e == eNoEnt then
      let buf = buf_memset(buf, 0, bilbyFsBlockSize, 0)
      in ((ex, fs_st, buf), Success ())
    else
      ((ex, fs_st, buf), Error e)
  | Success (obj {ounion}) ->
    extract_data_from_union(ex, ounion)
    | Error ex ->
      cogent_assert False ;
      let ex = freeObj(ex, obj)
      in ((ex, fs_st, buf), Error eInval) 
    | Success (ex, od) ->
      let ex = freeObj(ex, obj)
      and size = wordarray_length[U8] (od.odata) !od
      in if size > bilbyFsBlockSize then
        cogent_debug "bad object data" ;
        let ex = deep_freeObjData(ex, od)
        in ((ex, fs_st, buf), Error eInval)
      else
        let buf {data} = buf
        and data = wordarray_copy[U8] (data, od.odata, 0, 0, size) !od
        and buf = buf {data}
        and buf = buf_memset (buf, size, bilbyFsBlockSize - size, 0)
        and ex = deep_freeObjData(ex, od)
        in ((ex, fs_st, buf), Success ())

ostore_read: (SysState, MountState!, OstoreState, ObjId) -> RR (SysState, OstoreState) Obj ErrCode

extract_data_from_union:(SysState, ObjUnion) -> R (SysState, ObjData) SysState

bilbyFsXinfoShift : U64
bilbyFsXinfoShift = 29

bilbyFsObjTypeInode : U8
bilbyFsObjTypeInode = 0

bilbyFsObjTypeData : U8
bilbyFsObjTypeData = 1

bilbyFsOidMaskData : U64
bilbyFsOidMaskData = upcast bilbyFsObjTypeData << bilbyFsXinfoShift

bilbyFsOidMaskInode : U64
bilbyFsOidMaskInode = upcast bilbyFsObjTypeInode << bilbyFsXinfoShift

{-# cinline obj_id_data_mk #-}
obj_id_data_mk: (VfsIno, U32) -> ObjId
obj_id_data_mk(ino, blk) =
   obj_id_inode_mk ino .|. bilbyFsOidMaskData .|. upcast blk

{-# cinline obj_id_inode_mk #-}
obj_id_inode_mk: VfsIno -> ObjId
obj_id_inode_mk ino =
  (upcast ino << 32) .|. bilbyFsOidMaskInode

type Obj = {
       magic : U32,
       crc : U32,
       sqnum : U64,
       offs : U32, -- in-mem only field
       len : U32,
       trans : ObjTrans,
       otype : ObjType,
       ounion : ObjUnion
}

freeObj: (SysState, Obj take(..)) -> SysState

type ObjUnion = <TObjDentarr ObjDentarr
  | TObjInode ObjInode
  | TObjData ObjData
  | TObjDel #ObjDel
  | TObjSuper ObjSuper
  | TObjSummary ObjSummary
  | TObjPad ()>

type ObjType = U8
type ObjTrans = U8
type ObjId = U64
type ObjIdDentarr = U64
type ObjIdData = U64
type ObjIdInode = U64
type ObjDel
type ObjDentarr
type ObjSummary
type ObjSuper
type ObjInode

type ObjData = #{
  id : ObjId,
  odata : WordArray U8
}

{-# cinline deep_freeObjData #-}
deep_freeObjData: (SysState, ObjData) -> SysState