the_null_ptr is the dynamic constant of type ptr null
(I recently tripped over this while porting some ATS1 code to ATS2)On Sunday, February 22, 2015 at 6:03:45 PM UTC+6, Kiwamu Okabe wrote:
Hi all,
I try to use option_v.
extern fun user_get_super (dev: dev_t): [l:addr]
(option_v(super_block_t@l, l > null) | ptr(l)) = “mac#”
extern fun vfs_ustat_ats (dev: dev_t): Option_vt(@(uint64_t, uint64_t)) =
“sta#”
implement vfs_ustat_ats (dev) = r where {
var sbuf: kstatfs_t
val (pfopt | p) = user_get_super(dev)
val r = if (p > null) then let // <= Error occurs here!
prval Some_v (pf) = pfopt
val () = drop_super(pf | p)
in
end else let
prval None_v () = pfopt
in
None_vt()
end
}
However this catches an error…
/home/kiwamu/src/ATS-Postiats/bin/patsopt -o fs/statfs_dats.c -d
metasepi/fs/DATS/statfs.dats
/home/kiwamu/src/linux-bohai-s2/metasepi/fs/DATS/statfs.dats:
1090(line=28, offs=19) – 1094(line=28, offs=23): error(2): the
dynamic identifier [null] is unrecognized.
patsopt(TRANS2): there are [1] errors in total.
exit(ATS): uncaught exception:
_2home_2kiwamu_2src_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)
metasepi/scripts/Makefile.ats:13: recipe for target ‘fs/statfs_dats.c’
failed
I see this pattern at
ATS-Postiats/utils/atsynmark/DATS/pats2xhtml_main.dats:
val [l:addr] (pfopt | p) =
$STDIO.fopen_err (basename, file_mode_w)
// end of [val]
in
//
if p > null then let
prval Some_v (pf) = pfopt
val filp = __cast (pf | p) where {
extern castfn __cast (pf: FILE w @ l | p: ptr l):<> FILEref
} // end of [val]
in
cmdstate_set_outchan (state, OUTCHANptr (filp))
end else let
prval None_v () = pfopt
val () = state.nerror := state.nerror + 1
in
cmdstate_set_outchan (state, OUTCHANref (stderr_ref))
end // end of [if]
Basically, each ‘var’ is given a so-called master type.
In your example, the master type for sbuf is kstatfs_t.
When the if-expression is being typechecked, sbuf is
assumed to have the type kstatfs_t at the end of both
then-branch and else-branch. But this is not true in your code.
To put it differently, your code would have leaked a resource
if kstatfs_t were a linear type.On Thursday, February 26, 2015 at 2:26:26 PM UTC-5, Kiwamu Okabe wrote:
Hi Hongwei,
On Thu, Feb 26, 2015 at 11:38 PM, Hongwei Xi <gmh...@gmail.com <javascript:>> wrote:
Try to change
var sbuf: kstatfs_t
into
var sbuf: kstatfs_t?
I got compilable code.
However, I think the compile error doesn’t explain “?” missing.
/home/kiwamu/src/ATS-Postiats/bin/patsopt -o fs/statfs_dats.c -d
metasepi/fs/DATS/statfs.dats
/home/kiwamu/src/linux-bohai-s2/metasepi/fs/DATS/statfs.dats:
1570(line=39, offs=27) – 1634(line=43, offs=8): error(3): mismatch of
static terms (tyleq):
The actual term is: S2Etop(knd=0; S2Eapp(S2Ecst(g0int_t0ype);
S2Ecst(lint_kind)))
The needed term is: S2Eapp(S2Ecst(g0int_t0ype); S2Ecst(lint_kind))
/home/kiwamu/src/linux-bohai-s2/metasepi/fs/DATS/statfs.dats:
1570(line=39, offs=27) – 1634(line=43, offs=8): error(3): mismatch of
static terms (tyleq):
The actual term is: S2Etop(knd=0; S2Eapp(S2Ecst(g0int_t0ype);
S2Ecst(lint_kind)))
The needed term is: S2Eapp(S2Ecst(g0int_t0ype); S2Ecst(lint_kind))
They point let binding…
var sbuf: kstatfs_t
val e = vfs_ustat(new_decode_dev(dev), sbuf)
val r = (if e != 0 then let // <= Line 39
prval () = opt_unnone(sbuf)
in
e:int
end else let
prval () = opt_unsome(sbuf)
in
copy_tmp(sbuf)
end):int
extern fun vfs_ustat
(dev: dev_t, sbuf: &kstatfs_t? >> opt (kstatfs_t, i==0)): #[i:int | i
!= 0] int(i) = "mac#"
extern fun syscall_ustat_ats (dev: dev_t, ubuf: ustat_t_p): int = "sta#"
implement syscall_ustat_ats (dev, ubuf) = r where {
fun copy_tmp (sbuf: &kstatfs_t): int = r where {
var tmp: ustat_t
val _ = memset0(addr@tmp, 0, sizeof<ustat_t>)
val () = tmp.f_tfree := $UN.cast(sbuf.f_bfree)
val () = tmp.f_tinode := $UN.cast(sbuf.f_ffree)
val r = if copy_to_user0($UN.cast ubuf, addr@tmp, $UN.cast
sizeof<ustat_t>) != 0
then (~ EFAULT) else 0
}
var sbuf: kstatfs_t
val e = vfs_ustat(new_decode_dev(dev), sbuf)
val r = (if e != 0 then let
prval () = opt_unnone(sbuf)
in
e:int
end else let
prval () = opt_unsome(sbuf)
in
copy_tmp(sbuf)
end):int
}
/home/kiwamu/src/ATS-Postiats/bin/patsopt -o fs/statfs_dats.c -d
metasepi/fs/DATS/statfs.dats
/home/kiwamu/src/linux-bohai-s2/metasepi/fs/DATS/statfs.dats:
1570(line=39, offs=27) – 1634(line=43, offs=8): error(3): mismatch of
static terms (tyleq):
The actual term is: S2Etop(knd=0; S2Eapp(S2Ecst(g0int_t0ype);
S2Ecst(lint_kind)))
The needed term is: S2Eapp(S2Ecst(g0int_t0ype); S2Ecst(lint_kind))
/home/kiwamu/src/linux-bohai-s2/metasepi/fs/DATS/statfs.dats:
1570(line=39, offs=27) – 1634(line=43, offs=8): error(3): mismatch of
static terms (tyleq):
–snip–
