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	483	February 26, 2015
Optional values in ATS Google Group	9	569	May 14, 2015
Disallowed function effects incurred: stropt_is_some Google Group	2	340	January 19, 2014
Real-time OS system state captured by ATS language (and questions) Google Group	12	1393	July 10, 2016
Defining new static terms of ullint values? Google Group	16	808	August 6, 2014

Can't chain "opt" between functions?

Best regards,

Thank’s,

Best regards,

Best regards,

Related topics