How to trace chain of pointers with checking NULL?

[Kiwamu Okabe]

Hi all,

Now I'm trying to trace chain of pointers with checking NULL.

https://github.com/jats-ug/practice-ats/blob/dd46010122b1705fd2d0aa9323172695924adcff/pointer_chain/main.dats
https://github.com/jats-ug/practice-ats/blob/dd46010122b1705fd2d0aa9323172695924adcff/pointer_chain/dentry.c
https://github.com/jats-ug/practice-ats/blob/dd46010122b1705fd2d0aa9323172695924adcff/pointer_chain/dentry.h

But the code has following error.

/home/kiwamu/src/practice-ats/pointer_chain/main.dats: 980(line=42,
offs=21) -- 1056(line=43, offs=47): error(3): mismatch of static terms
(tyleq):
The actual term is: S2Efun(FUN; lin=0; eff=S2EFFset(1); npf=-1;
S2Ecst(dentry_t_p); S2Ecst(int))
The needed term is: S2Ecst(ptr_type)

I think it's caused by cast envless function.
I would like to check if the envless function is NULL.

How to trace chain of pointers with checking NULL?

Thank's,
--
Kiwamu Okabe at METASEPI DESIGN

[Hongwei Xi]

In this case, you need to use 'topize' to turn a function into a pointer:

val _ =
if b
then let
  prval () = opt_unsome (f)
  val res = f (get_dentry_p ())
  prval () = topize(f)
in
  res
end // then
else let
  prval () = opt_unnone (f)
in 0 end // else

--
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/CAEvX6d%3DdFk%3DA9GYY7ZePy2gtGWMqnZgyaDmwbqnXYOndgeLDAQ%40mail.gmail.com.

[Kiwamu Okabe]

Wow! It's magic.

praxi topize {a:t@ype} (x: !INV(a) >> a?): void

On Fri, Jun 26, 2015 at 12:54 AM, Hongwei Xi <gmh...@gmail.com> wrote:
> In this case, you need to use 'topize' to turn a function into a pointer:

[Kiwamu Okabe]

Hi Hongwei,

Finally, I get following code using template.
It may be useful for me to rewrite Linux kernel.

https://github.com/jats-ug/practice-ats/blob/469f888704ed6d4e5b743fdf36ecbbb36dd54f02/pointer_chain/main.dats#L25

fun{s,f:type}
tracestruct (from: s, trace: (s -> f), function: &f? >> opt (f, b)):
#[b:bool] bool(b) = let
val f = trace from
in
if $UN.cast{ptr}(f) = the_null_ptr then let
prval () = opt_none{f}(function)
in
false
end
else let
val () = function := f
prval () = opt_some{f}(function)
in
true
end
end

[Kiwamu Okabe]

Hi all,

Can't ATS compiler allow following style?

https://github.com/jats-ug/practice-ats/blob/b46f993a94874e353876f2b76a4a20cf9548b9fe/pointer_chain2/main.dats

typedef f_statfs = ptr -> int

vtypedef super_operations_t = $extype_struct"struct super_operations" of {
statfs= f_statfs
}
vtypedef super_block_t = $extype_struct"struct super_block" of {
s_op= {l:addr}(super_operations_t@l | ptr(l))
}
vtypedef dentry_t = $extype_struct"struct dentry" of {
d_sb= {l:addr}(super_block_t@l | ptr(l))
}

extern fun get_dentry_p (): [l:addr] (dentry_t@l | ptr(l)) = "mac#"
extern fun get_dentry_p_null (): [l:addr] (dentry_t@l | ptr(l)) = "mac#"

implement main0 () = {
val (pfdentry | dentry) = get_dentry_p ()
val (pfsb | sb) = dentry->d_sb
val (pfsop | sop) = sb->s_op
val _ = sop->statfs dentry
val _ = $UN.castvwtp0{ptr}((pfsop | sop))
val _ = $UN.castvwtp0{ptr}((pfsb | sb))
val _ = $UN.castvwtp0{ptr}((pfdentry | dentry))
}

Thank's,
--
Kiwamu Okabe at METASEPI DESIGN

[Hongwei Xi]

Why not the following interface:

fun{s.f:t0ype}

tracestruct(...)

--
Kiwamu Okabe

--
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/CAEvX6dnA1C5V%3DE8FQm4uUQ4Z1oA0qcB0D%2ByOCp%3D6iGe-DG-y9A%40mail.gmail.com.

[Hongwei Xi]

>>s_op= {l:addr}(super_operations_t@l | ptr(l))

This is likely a mistake. I think you need:

s_op= [l:addr](super_operations_t@l | ptr(l))

--
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/CAEvX6dkFkEJq0Gvwdj67W7KVtsh1Mqp-_bAnYibf0Zm7oFVcyg%40mail.gmail.com.

[Kiwamu Okabe]

On Sat, Jun 27, 2015 at 12:26 AM, Hongwei Xi <gmh...@gmail.com> wrote:
> Why not the following interface:
>
> fun{s.f:t0ype}
> tracestruct(...)

Thank's, I didn't know that envless function is "t@ype".
How to find out that? $showtype say the envless function is...

$ make
/home/kiwamu/src/ATS-Postiats/bin/patscc main.dats dentry.c
**SHOWTYPE[UP]**(/home/kiwamu/src/practice-ats/pointer_chain/main.dats:
1173(line=47, offs=33) -- 1174(line=47, offs=34)): S2Efun(FUN; lin=0;
eff=S2EFFset(1); npf=-1; S2Ecst(dentry_t_p); S2Ecst(int)):
S2RTbas(S2RTBASimp(0; type))

Which string say that envless function is "t@ype"?

Also, why doesn't occur error on type checking while envless function is
used as "type"? My code with envless function as "type" has no error on
both compile time and run tine.

Regards,

[Kiwamu Okabe]

Hi Hongwei,

On Sat, Jun 27, 2015 at 2:55 AM, Hongwei Xi <gmh...@gmail.com> wrote:
>>>s_op= {l:addr}(super_operations_t@l | ptr(l))
>
> This is likely a mistake. I think you need:
>
> s_op= [l:addr](super_operations_t@l | ptr(l))

Thank's. It's my mistake.

https://github.com/jats-ug/practice-ats/blob/eadbc1861341b927bc8de80776067dc779135b9b/pointer_chain2/main.dats

However, my code has compile error at GCC side.

$ patscc main.dats dentry.c
main_dats.c: In function ‘mainats_void_0’:
main_dats.c:304:1: warning: implicit declaration of function
‘get_dentry_p’ [-Wimplicit-function-declaration]
ATSINSmove(tmp1, get_dentry_p()) ;
^
In file included from main_dats.c:15:0:
/home/kiwamu/src/ATS-Postiats/ccomp/runtime/pats_ccomp_instrset.h:260:35:
warning: assignment makes pointer from integer without a cast
#define ATSINSmove(tmp, val) (tmp = val)
^
main_dats.c:304:1: note: in expansion of macro ‘ATSINSmove’
ATSINSmove(tmp1, get_dentry_p()) ;
^
/home/kiwamu/src/ATS-Postiats/ccomp/runtime/pats_ccomp_instrset.h:203:29:
error: dereferencing pointer to incomplete type
#define ATSderef(pmv, hit) (*(hit*)pmv)
^
--snip--

Doesn't ATS compiler support this style?

Regards,

[gmhwxi]

If 's' and 'f' are supposed to be function types, then you should
use 's,f:type'. In any case, 'type' is treated as a subsort of 't@ype'.

[gmhwxi]

>>extern fun get_dentry_p (): [l:addr] (dentry_t@l | ptr(l)) = "mac#"

I assume that 'get_dentry_p' is implemented in dentry.c. You need to
make its C-interface available in ATS in order to call it in ATS.

[Kiwamu Okabe]

On Tue, Jun 30, 2015 at 12:34 AM, gmhwxi <gmh...@gmail.com> wrote:
>>>extern fun get_dentry_p (): [l:addr] (dentry_t@l | ptr(l)) = "mac#"
>
> I assume that 'get_dentry_p' is implemented in dentry.c. You need to
> make its C-interface available in ATS in order to call it in ATS.

Sorry, it's my mistake, and has no relation with at-view.
It's fixed with following patch.

https://github.com/jats-ug/practice-ats/commit/1c88395644e3e11cdb29b4332c5eb345b0c63e05

Thank's,

[Yannick Duchêne]

Where does the word “topize” come from? I guess it is not related to the logical symbol named top and I don’t see another candidate meaning for “top”. Similarly, a comment in ATS2 source talks about topization for uninitialized view and typization for initialized view.