Skip to content

Commit

Permalink
bilby: typechecks!
Browse files Browse the repository at this point in the history
  • Loading branch information
@ajaysusarla
Zilin Chen authored and ajaysusarla committed Nov 28, 2016
1 parent af04176 commit 9988a43
Show file tree
Hide file tree
Showing 2 changed files with 19 additions and 28 deletions.
22 changes: 7 additions & 15 deletions impl/bilby/cogent/src/fsop.cogent
View file
Original file line number Diff line number Diff line change
Expand Up @@ -508,16 +508,15 @@ dentarr_read_and_del (ex, mount_st, ostore_st, vdir, name) =
| Error ex ->
-- invariant on ostore_read
_cogent_assert False ;
let dentarr_obj {..} = dentarr_obj
and ex = freeObj(ex, dentarr_obj)
let ex = freeObj(ex, dentarr_obj)
in ((ex, ostore_st), Error eInval)
| Success (ex, dentarr) ->
let (ex, dentarr) = dentarr_del_dentry(ex, dentarr, name)
and ((ex, dentarr_obj), r) = dentarr_del_calculate_sz_change(ex, dentarr_obj, dentarr)
in r
| Error e ->
_cogent_debug "dentarr_read_and_del: dentarr_del_calculate_sz_change: failed\n" ;
let dentarr_obj {ounion,..} = dentarr_obj
let dentarr_obj {ounion} = dentarr_obj
and ex = deep_freeObjUnion(ex, ounion)
and ex = freeObj(ex, dentarr_obj)
in ((ex, ostore_st), Error e)
Expand Down Expand Up @@ -1749,8 +1748,7 @@ fsop_iget #{ex, fs_st = fs_st {ostore_st}, inum, vnode} =
in extract_inode_from_union (ex, ounion)
| Error ex ->
_cogent_assert False ;
let obj {..} = obj
and ex = freeObj(ex, obj)
let ex = freeObj(ex, obj)
in (#{ex, fs_st, vnode}, Error eInval)
| Success (ex, oi) ->
let vnode = vfs_inode_set_ino (vnode, inum_from_obj_id oi.id) !oi
Expand Down Expand Up @@ -1793,12 +1791,10 @@ read_block(ex, fs_st {ostore_st}, vnode, buf, block) =
in extract_data_from_union(ex, ounion)
| Error ex ->
_cogent_assert False ;
let obj {..} = obj
and ex = freeObj(ex, obj)
let ex = freeObj(ex, obj)
in ((ex, fs_st, buf), Error eInval)
| Success (ex, od) ->
let obj {..} = obj
and ex = freeObj(ex, obj)
let ex = freeObj(ex, obj)
and size = wordarray_length[U8] (od.odata) !od
in if size > bilbyFsBlockSize then
_cogent_debug "bad object data" ;
Expand Down Expand Up @@ -2460,10 +2456,8 @@ fsop_init #{ex,fs_st,name} =
and ex = wubi_close (ex, ubivol)
in ostore_init(ex, mount_st, ostore_st) !mount_st
| Error (err, ex, ostore_st) ->
let mount_st {obj_sup,vol,dev,super,..} = mount_st
and fsop_st {..} = fsop_st
let mount_st {obj_sup,vol,dev,super} = mount_st
and ex = deep_freeObjSuper(ex, super)
and obj_sup {..} = obj_sup
and ex = freeObj(ex, obj_sup)
and ex = freeMountState(ex, mount_st)
and ex = freeFsopState(ex, fsop_st)
Expand Down Expand Up @@ -2492,15 +2486,13 @@ fsop_unmount #{ex,fs_st} =
fsop_clean: FsopFsP -> ExState
fsop_clean #{ex,fs_st} =
let fs_st {fsop_st, mount_st, ostore_st} = fs_st
and mount_st {vol,dev,obj_sup,super,..} = mount_st
and mount_st {vol,dev,obj_sup,super} = mount_st
and ex = deep_freeObjSuper(ex, super)
and obj_sup {..} = obj_sup
and ex = freeObj(ex, obj_sup)
and ex = freeUbiVolInfo(ex, vol)
and ex = freeUbiDevInfo(ex, dev)
and ex = freeMountState(ex, mount_st)
and ex = ostore_clean(ex, ostore_st)
and fsop_st {..} = fsop_st
and ex = freeFsopState(ex, fsop_st)
and ex = freeFsState(ex, fs_st)
in ex
25 changes: 12 additions & 13 deletions impl/bilby/cogent/src/ostore.cogent
View file
Original file line number Diff line number Diff line change
Expand Up @@ -184,7 +184,7 @@ ostore_read_sum(ex, mount_st, ostore_st {rbuf}, ebnum) =
((ex, ostore_st), Success sum_offs)

ostore_clean: (ExState, OstoreState) -> ExState
ostore_clean(ex, ostore_st {rbuf,wbuf,opad,pools,fsm_st,index_st,ubi_vol,summary,sum_obj,..}) =
ostore_clean(ex, ostore_st {rbuf,wbuf,opad,pools,fsm_st,index_st,ubi_vol,summary,sum_obj}) =
let ex = buf_free(ex, rbuf)
and ex = buf_free(ex, wbuf)
and ex = deep_freeObj(ex, opad)
Expand All @@ -200,17 +200,17 @@ ostore_clean(ex, ostore_st {rbuf,wbuf,opad,pools,fsm_st,index_st,ubi_vol,summary
and ex = freeOstoreState(ex, ostore_st)
in ex

get_obj_oid: (Obj!) -> ObjId
get_obj_oid(obj) =
get_obj_oid: Obj! -> ObjId
get_obj_oid obj =
obj.ounion
| TObjInode o -> o.id
| TObjData o -> o.id
| TObjDentarr o -> o.id
| TObjDel o -> o.id
| _ -> nilObjId

print_obj_type: (Obj!) -> ()
print_obj_type(obj) =
print_obj_type: Obj! -> ()
print_obj_type obj =
obj.ounion
| TObjInode o -> _cogent_debug "inode"
| TObjData o -> _cogent_debug "data"
Expand Down Expand Up @@ -867,7 +867,7 @@ ostore_read (ex, mount_st, ostore_st, oid) =
_cogent_debug "Obj not found in index " ;
_cogent_debug_u64_hex oid ;
_cogent_debug "\n" ;
((ex, ostore_st), error err)
((ex, ostore_st), error[Obj] err)
| Success addr ->
let wbuf_eb = ostore_st.wbuf_eb !ostore_st
-- if we are trying to read an object that is in the current write-buffer
Expand All @@ -878,24 +878,24 @@ ostore_read (ex, mount_st, ostore_st, oid) =
| Error (e, ex) ->
_cogent_debug "ostore_read: deserialise_Obj_crc from buffer failed\n" ;
let wbuf = wbuf {bound=mount_st.super.eb_size}
in ((ex, ostore_st {wbuf}), error e)
in ((ex, ostore_st {wbuf}), error[Obj] e)
| Success (ex, obj, sz) ->
let wbuf = wbuf {bound=mount_st.super.eb_size}
in ((ex, ostore_st {wbuf}), success obj)
in ((ex, ostore_st {wbuf}), success[Obj, ErrCode] obj)
else
-- We need to read the object from medium
let ostore_st {rbuf} = ostore_st
and ((ex, rbuf), r) = read_obj_pages_in_buf (ex, mount_st, ostore_st.ubi_vol, rbuf, addr) !ostore_st
in r
| Error e ->
_cogent_debug "ostore_read: read_obj_pages_in_buf failed.\n" ;
((ex, ostore_st {rbuf}), error e)
((ex, ostore_st {rbuf}), error[Obj] e)
| Success () ->
deserialise_Obj (ex, rbuf, addr.offs) !rbuf
| Error (e, ex) ->
_cogent_debug "ostore_read: deserialise_Obj_crc from flash failed.\n" ;
((ex, ostore_st {rbuf}), error e)
| Success (ex, obj, sz) -> ((ex, ostore_st {rbuf}), success obj)
((ex, ostore_st {rbuf}), error[Obj] e)
| Success (ex, obj, sz) -> ((ex, ostore_st {rbuf}), success[Obj, ErrCode] obj)
)
in r
| Success obj ->
Expand All @@ -909,7 +909,7 @@ ostore_read (ex, mount_st, ostore_st, oid) =
_cogent_assert False ;
-- Fs should go in read-only mode as we have detected
-- an inconsistency between index and medium
((deep_freeObj(ex, obj), ostore_st), Error eRoFs)
((deep_freeObj (ex, obj), ostore_st), Error eRoFs)
| Error e -> ((ex, ostore_st), Error e)

read_obj_pages_in_buf: (ExState, MountState!, UbiVol!, Buffer, ObjAddr!) -> RR (ExState, Buffer) () ErrCode
Expand Down Expand Up @@ -1526,7 +1526,6 @@ ostore_write_super (ex, mount_st, ostore_st) =

and ostore_st = ostore_st {wbuf_eb=bilbyFsSuperEbNum,
used=mount_st.super_offs, sync_offs=mount_st.super_offs} !mount_st
and obj {..} = obj
and obj = obj_init_super(obj, next_sqnum, mount_st.super_offs) !mount_st
and ostore_st = ostore_st {next_sqnum = next_sqnum+1}
and ostore_st {wbuf} = ostore_st
Expand Down

0 comments on commit 9988a43

Please sign in to comment.