Can't chain "opt" between functions?

[Kiwamu Okabe]

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.

https://travis-ci.org/metasepi/linux-bohai-s2/builds/52408252

/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

[Hongwei Xi]

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

--
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.

[Hongwei Xi]

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.

[Kiwamu Okabe]

Hi Hongwei,

On Sat, Feb 28, 2015 at 12:55 AM, Hongwei Xi <gmh...@gmail.com> 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
>
> Using if-expressions (or case-expressions) in the middle of a function often
> complicates type-checking
> a lot.

Umm... It does not make sense on my code.

https://travis-ci.org/metasepi/linux-bohai-s2/builds/52727637

/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:

1461(line=41, offs=7) -- 1462(line=41, offs=8): error(3): the linear
dynamic variable [sbuf$view$1705(-1)] is preserved but with an
incompatible type.
/home/kiwamu/src/linux-bohai-s2/metasepi/fs/DATS/statfs.dats:
1461(line=41, offs=7) -- 1462(line=41, 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=S2Ecst(lint), f_bsize=S2Ecst(lint), f_blocks=S2Ecst(uint64_t),
f_bfree=S2Ecst(uint64_t), f_bavail=S2Ecst(uint64_t),
f_files=S2Ecst(uint64_t), f_ffree=S2Ecst(uint64_t),
f_fsid=S2Ecst(kernel_fsid_t), f_namelen=S2Ecst(lint),
f_frsize=S2Ecst(lint), f_flags=S2Ecst(lint),
f_spare=S2Etyarr(S2Ecst(lint); S2Eintinf(4)))

Regards,

[Kiwamu Okabe]

Hi Hongwei,

On Sat, Feb 28, 2015 at 12: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

I think my code want to decide some or none at "statfs_by_dentry" function.

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

"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.

Is it correct?

[Kiwamu Okabe]

Hi Hongwei,
I think I should explain more.

On Mon, Mar 2, 2015 at 8:49 PM, Kiwamu Okabe <kiw...@debian.or.jp> 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...

[Kiwamu Okabe]

Hi Hongwei,

On Sat, Feb 28, 2015 at 12:55 AM, Hongwei Xi <gmh...@gmail.com> 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,

[gmhwxi]

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#"
 

[gmhwxi]

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

prval () = opt_some(sbuf)

[Kiwamu Okabe]

After reading ATS-Postiats/libc/sys/SATS/stat.sats, I think your new code is right.

On Mon, Mar 2, 2015 at 10:00 PM, gmhwxi <gmh...@gmail.com> wrote:

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#"