Can't chain "opt" between functions?

gmhwxi · February 27, 2015, 3:48pm

I think the cause is that you missed the following two lines:

prval () = opt_some(sbuf) // in the then-branch

prval () = opt_none{kstatfs_t}(sbuf) // in the else-branchOn Fri, Feb 27, 2015 at 6:45 AM, Kiwamu Okabe kiw...@debian.or.jp wrote:

Hi all,

Can’t chain “opt” between functions?
I have tried to write body of vfs_ustat function.

https://github.com/metasepi/linux-bohai-s2/blob/3299f651b9a61d60e36bef4b41216e02658c2784/metasepi/fs/DATS/statfs.dats#L30

fun user_get_super (dev: dev_t): [l:addr] (option_v(super_block_t@l, l

null) | ptr(l)) = “mac#”

extern fun statfs_by_dentry
(dentry: dentry_t_p, sbuf: &kstatfs_t? >> opt (kstatfs_t, i==0)):
#[i:int | i != 0] int(i) = “mac#”

fun vfs_ustat_ats
(dev: dev_t, sbuf: &kstatfs_t? >> opt (kstatfs_t, i==0)): #[i:int | i != 0] int(i) = r where {
val (pfopt | p) = user_get_super(dev)
val r = if (p > the_null_ptr) then let
prval Some_v (pf) = pfopt
val e = statfs_by_dentry(p->s_root, sbuf);
val () = drop_super(pf | p)
in
e
end else let
prval None_v () = pfopt
in
(~ EINVAL)
end
}

However, it causes compile error.

Travis CI - Test and Deploy with Confidence

/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:
1319(line=33, offs=38) – 1460(line=39, offs=8): error(3): mismatch of
static terms (tyleq):
The actual term is: S2Eapp(S2Ecst(opt_vt0ype_bool_vt0ype);
S2Ecst(kstatfs_t), S2Eapp(S2Ecst(==); S2Evar(i$3302$3304(7381)),
S2Eintinf(0)))
The needed term is: S2Etyrec(fltext(struct kstatfs); npf=-1;
f_type=S2Etop(knd=0; S2Ecst(lint)), f_bsize=S2Etop(knd=0;
S2Ecst(lint)), f_blocks=S2Etop(knd=0; S2Ecst(uint64_t)),
f_bfree=S2Etop(knd=0; S2Ecst(uint64_t)), f_bavail=S2Etop(knd=0;
S2Ecst(uint64_t)), f_files=S2Etop(knd=0; S2Ecst(uint64_t)),
f_ffree=S2Etop(knd=0; S2Ecst(uint64_t)), f_fsid=S2Etop(knd=0;
S2Ecst(kernel_fsid_t)), f_namelen=S2Etop(knd=0; S2Ecst(lint)),
f_frsize=S2Etop(knd=0; S2Ecst(lint)), f_flags=S2Etop(knd=0;
S2Ecst(lint)), f_spare=S2Etop(knd=0; S2Etyarr(S2Ecst(lint);
S2Eintinf(4))))
/home/kiwamu/src/linux-bohai-s2/metasepi/fs/DATS/statfs.dats:
1319(line=33, offs=38) – 1460(line=39, offs=8): error(3): mismatch of
static terms (tyleq):
The actual term is: S2Eat(S2Eapp(S2Ecst(opt_vt0ype_bool_vt0ype);
S2Ecst(kstatfs_t), S2Eapp(S2Ecst(==); S2Evar(i$3302$3304(7381)),
S2Eintinf(0))); S2Evar(sbuf(7372)))
The needed term is: S2Eat(S2Etyrec(fltext(struct kstatfs); npf=-1;
f_type=S2Etop(knd=0; S2Ecst(lint)), f_bsize=S2Etop(knd=0;
S2Ecst(lint)), f_blocks=S2Etop(knd=0; S2Ecst(uint64_t)),
f_bfree=S2Etop(knd=0; S2Ecst(uint64_t)), f_bavail=S2Etop(knd=0;
S2Ecst(uint64_t)), f_files=S2Etop(knd=0; S2Ecst(uint64_t)),
f_ffree=S2Etop(knd=0; S2Ecst(uint64_t)), f_fsid=S2Etop(knd=0;
S2Ecst(kernel_fsid_t)), f_namelen=S2Etop(knd=0; S2Ecst(lint)),
f_frsize=S2Etop(knd=0; S2Ecst(lint)), f_flags=S2Etop(knd=0;
S2Ecst(lint)), f_spare=S2Etop(knd=0; S2Etyarr(S2Ecst(lint);
S2Eintinf(4)))); S2Evar(sbuf(7372)))

Dependent and linear types are hard work for me, even now.

Best regards,

Kiwamu Okabe at METASEPI DESIGN

–
You received this message because you are subscribed to the Google Groups
“ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send an
email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dmc0usZP2%3DyT25f%3DthXnS4vGBWZr4A9Yv_ztwtwwk%2BPsQ%40mail.gmail.com
.

gmhwxi · March 2, 2015, 1:06pm

Yes, the following line in my code should be dropped:

prval () = opt_some(sbuf)On Monday, March 2, 2015 at 8:00:21 AM UTC-5, Kiwamu Okabe wrote:

Hi Hongwei,

On Sat, Feb 28, 2015 at 12:55 AM, Hongwei Xi <gmh...@gmail.com <javascript:>> wrote:

I suggest the following style:

fun vfs_ustat_ats
(dev: dev_t, sbuf: &kstatfs_t? >> opt (kstatfs_t, i==0)): #[i:int | i != 0] int(i) = let
val (pfopt | p) = user_get_super(dev)
in
if (p > 0) then let
prval Some_v (pf) = pfopt
val e = statfs_by_dentry(p->s_root, sbuf);
val () = drop_super(pf | p)
prval () = opt_some(sbuf)
in
e
end else let
prval None_v () = pfopt
prval () = opt_none{kstatfs_t}()
in
(~ EINVAL)
end
end

I found following code can be compiled by patsopt.

https://github.com/metasepi/linux-bohai-s2/blob/c2e49683f16bd59163a206ebdf6914f6993c532f/metasepi/fs/DATS/statfs.dats#L30

extern fun statfs_by_dentry
(dentry: dentry_t_p, sbuf: &kstatfs_t? >> opt (kstatfs_t, i==0)):
#[i:int | i != 0] int(i) = “mac#”

fun vfs_ustat_ats
(dev: dev_t, sbuf: &kstatfs_t? >> opt (kstatfs_t, i==0)): #[i:int | i != 0] int(i) = let
val (pfopt | p) = user_get_super(dev)
in
if (p > 0) then let
prval Some_v (pf) = pfopt
val e = statfs_by_dentry(p->s_root, sbuf);
val () = drop_super(pf | p)
in
e
end else let
prval None_v () = pfopt
prval () = opt_none{kstatfs_t}(sbuf)
in
(~ EINVAL)
end
end

extern fun syscall_ustat_ats (dev: dev_t, ubuf: ptr): int = “sta#”
implement syscall_ustat_ats (dev, ubuf) = r where {
fun copy_tmp (sbuf: &kstatfs_t): int = r where {
var tmp: ustat_t
val _ = memset(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_user(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
end else let
prval () = opt_unsome(sbuf)
in
copy_tmp(sbuf)
end
}

It’s not yet compilable on C language side.
It’s caused by bad pointer issue.
However, I think easy to fix it.

Thank’s,

Kiwamu Okabe at METASEPI DESIGN

gmhwxi · March 2, 2015, 1:00pm

Sorry, I did not read your code carefully.

This is incorrect:

extern fun statfs_by_dentry(dentry: dentry_t_p, sbuf: &kstatfs_t? >> opt (
kstatfs_t, i==0)): #[i:int | i != 0] int(i) = “mac#”

If the returned value is non-zero, it means the function always fails.

It should probably be:

extern fun statfs_by_dentry
(dentry: dentry_t_p, sbuf: &kstatfs_t? >> opt (kstatfs_t, i==0)): #[i:int | i <= 0] int(i) = "mac#"On Monday, March 2, 2015 at 7:01:05 AM UTC-5, Kiwamu Okabe wrote:

Hi Hongwei,
I think I should explain more.

On Mon, Mar 2, 2015 at 8:49 PM, Kiwamu Okabe <kiw…@debian.or.jp <javascript:>> wrote:

“statfs_by_dentry” function is called by “vfs_ustat_ats” that is
called by “syscall_ustat_ats”.
Your patch decides it on “vfs_ustat_ats” function.

Today, I’m trying to re-write Linux kernel C code into ATS2.

The statfs_by_dentry function in ATS has only interface, and it’s
following ATS interface.

https://github.com/metasepi/linux-bohai-s2/blob/83c6a38ab73ae3aa8a5a12afda7babbb76e01e38/metasepi/fs/DATS/statfs.dats#L24

On original Linux code, statfs_by_dentry function is called by
vfs_ustat function that has following C code.

https://github.com/metasepi/linux-bohai-s2/blob/83c6a38ab73ae3aa8a5a12afda7babbb76e01e38/fs/statfs.c#L216

The vfs_ustat function is called by ustat system call that has following C
code.

https://github.com/metasepi/linux-bohai-s2/blob/83c6a38ab73ae3aa8a5a12afda7babbb76e01e38/fs/statfs.c#L228

I would like to re-write the vfs_ustat function with ATS2. Then, these
code should have same meaning.

https://github.com/metasepi/linux-bohai-s2/blob/83c6a38ab73ae3aa8a5a12afda7babbb76e01e38/fs/statfs.c#L216

https://github.com/metasepi/linux-bohai-s2/blob/83c6a38ab73ae3aa8a5a12afda7babbb76e01e38/metasepi/fs/DATS/statfs.dats#L30

However, passing opt is hard for me, today…

Best regards,

Kiwamu Okabe at METASEPI DESIGN

gmhwxi · February 27, 2015, 3:55pm

I suggest the following style:

fun vfs_ustat_ats
(dev: dev_t, sbuf: &kstatfs_t? >> opt (kstatfs_t, i==0)): #[i:int | i != 0] int(i) = let
val (pfopt | p) = user_get_super(dev)
in
if (p > 0) then let
prval Some_v (pf) = pfopt
val e = statfs_by_dentry(p->s_root, sbuf);
val () = drop_super(pf | p)
prval () = opt_some(sbuf)
in
e
end else let
prval None_v () = pfopt
prval () = opt_none{kstatfs_t}()
in
(~ EINVAL)
end
end

Using if-expressions (or case-expressions) in the middle of a function
often complicates type-checking
a lot.On Fri, Feb 27, 2015 at 10:48 AM, Hongwei Xi gmh...@gmail.com wrote:

I think the cause is that you missed the following two lines:

prval () = opt_some(sbuf) // in the then-branch

prval () = opt_none{kstatfs_t}(sbuf) // in the else-branch

On Fri, Feb 27, 2015 at 6:45 AM, Kiwamu Okabe kiw...@debian.or.jp wrote:

Hi all,

Can’t chain “opt” between functions?
I have tried to write body of vfs_ustat function.

https://github.com/metasepi/linux-bohai-s2/blob/3299f651b9a61d60e36bef4b41216e02658c2784/metasepi/fs/DATS/statfs.dats#L30

fun user_get_super (dev: dev_t): [l:addr] (option_v(super_block_t@l, l

null) | ptr(l)) = “mac#”

extern fun statfs_by_dentry
(dentry: dentry_t_p, sbuf: &kstatfs_t? >> opt (kstatfs_t, i==0)):
#[i:int | i != 0] int(i) = “mac#”

fun vfs_ustat_ats
(dev: dev_t, sbuf: &kstatfs_t? >> opt (kstatfs_t, i==0)): #[i:int | i != 0] int(i) = r where {
val (pfopt | p) = user_get_super(dev)
val r = if (p > the_null_ptr) then let
prval Some_v (pf) = pfopt
val e = statfs_by_dentry(p->s_root, sbuf);
val () = drop_super(pf | p)
in
e
end else let
prval None_v () = pfopt
in
(~ EINVAL)
end
}

However, it causes compile error.

Travis CI - Test and Deploy with Confidence

/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:
1319(line=33, offs=38) – 1460(line=39, offs=8): error(3): mismatch of
static terms (tyleq):
The actual term is: S2Eapp(S2Ecst(opt_vt0ype_bool_vt0ype);
S2Ecst(kstatfs_t), S2Eapp(S2Ecst(==); S2Evar(i$3302$3304(7381)),
S2Eintinf(0)))
The needed term is: S2Etyrec(fltext(struct kstatfs); npf=-1;
f_type=S2Etop(knd=0; S2Ecst(lint)), f_bsize=S2Etop(knd=0;
S2Ecst(lint)), f_blocks=S2Etop(knd=0; S2Ecst(uint64_t)),
f_bfree=S2Etop(knd=0; S2Ecst(uint64_t)), f_bavail=S2Etop(knd=0;
S2Ecst(uint64_t)), f_files=S2Etop(knd=0; S2Ecst(uint64_t)),
f_ffree=S2Etop(knd=0; S2Ecst(uint64_t)), f_fsid=S2Etop(knd=0;
S2Ecst(kernel_fsid_t)), f_namelen=S2Etop(knd=0; S2Ecst(lint)),
f_frsize=S2Etop(knd=0; S2Ecst(lint)), f_flags=S2Etop(knd=0;
S2Ecst(lint)), f_spare=S2Etop(knd=0; S2Etyarr(S2Ecst(lint);
S2Eintinf(4))))
/home/kiwamu/src/linux-bohai-s2/metasepi/fs/DATS/statfs.dats:
1319(line=33, offs=38) – 1460(line=39, offs=8): error(3): mismatch of
static terms (tyleq):
The actual term is: S2Eat(S2Eapp(S2Ecst(opt_vt0ype_bool_vt0ype);
S2Ecst(kstatfs_t), S2Eapp(S2Ecst(==); S2Evar(i$3302$3304(7381)),
S2Eintinf(0))); S2Evar(sbuf(7372)))
The needed term is: S2Eat(S2Etyrec(fltext(struct kstatfs); npf=-1;
f_type=S2Etop(knd=0; S2Ecst(lint)), f_bsize=S2Etop(knd=0;
S2Ecst(lint)), f_blocks=S2Etop(knd=0; S2Ecst(uint64_t)),
f_bfree=S2Etop(knd=0; S2Ecst(uint64_t)), f_bavail=S2Etop(knd=0;
S2Ecst(uint64_t)), f_files=S2Etop(knd=0; S2Ecst(uint64_t)),
f_ffree=S2Etop(knd=0; S2Ecst(uint64_t)), f_fsid=S2Etop(knd=0;
S2Ecst(kernel_fsid_t)), f_namelen=S2Etop(knd=0; S2Ecst(lint)),
f_frsize=S2Etop(knd=0; S2Ecst(lint)), f_flags=S2Etop(knd=0;
S2Ecst(lint)), f_spare=S2Etop(knd=0; S2Etyarr(S2Ecst(lint);
S2Eintinf(4)))); S2Evar(sbuf(7372)))

Dependent and linear types are hard work for me, even now.

Best regards,

Kiwamu Okabe at METASEPI DESIGN

–
You received this message because you are subscribed to the Google Groups
“ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send an
email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dmc0usZP2%3DyT25f%3DthXnS4vGBWZr4A9Yv_ztwtwwk%2BPsQ%40mail.gmail.com
.

Topic		Replies	Views
How to use use option_v and pointer? Google Group	6	450	February 26, 2015
How to trace chain of pointers with checking NULL? Google Group	4	411	June 29, 2015
Segfault Google Group	2	286	March 10, 2013
Refval compile failure with sats/dats file Google Group	1	355	October 28, 2015
Some more questions on Arrays Google Group	5	378	February 24, 2014

Can't chain "opt" between functions?

Best regards,

Thank’s,

Best regards,

Best regards,

Related Topics