Bitwise operations

[Shea Levy]

Hi all,

Does ATS support any bitwise operations on ints in the statics?

~Shea

[Hongwei Xi]

Right now, constraints involving bitwise operations can be
generated., but the built-in constraint-solver in ATS cannot handle
such constraints.

Will Blair should have something to say on this issue. He has managed
to use Microsoft's Z3 to do constraint-solving for ATS. Z3 can
readily handle bitwise operations.

~Shea

--
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/20140901051852.GE2219%40nixos.hsd1.nh.comcast.net.

[Shea Levy]

Hm, how do I spell the operations? I've got something like this to
represent the arguments to the 'socket' function, which on Linux allows
the 'type' argument to be bitwise-ored with certain modifiers (the ATS_
prefix indicates a macro taken from a C include):

> dataprop domain(int) = AF_UNIX (ATS_AF_UNIX) (* TODO include other address families *)
>
> dataprop type_base(int) = SOCK_STREAM (ATS_SOCK_STREAM) (* TODO include other socket types *)
>
> dataprop type_modifier(int) = SOCK_NONBLOCK (ATS_SOCK_NONBLOCK) | SOCK_CLOEXEC (ATS_SOCK_CLOEXEC)
>
> dataprop type(int) =
> | {t: int} base (t) of (type_base(t))
> | {t, m: int} or ((t | m)) of (type(t), type_modifier(m))
>
> (* TODO include protocol argument *)
> (* TODO error handling *)
> fn socket {d, t: int} (domain d, type t | int d, int t): [fd: int] (filedes fd | int fd)

This fails with:

> the static expression needs to be impredicative but is assigned the sort [S2RTbas(S2RTBASpre(int))]

twice (apparently one for the t and one for the m in ((t | m)). If I
replace 't | m' with 't * m', it compiles fine (though with the wrong
semantics, of course).

~Shea

> To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrdCOS8MuVo9zs6d4gQXe3a%2BFB3TKAu5k1s0zA622VcZw%40mail.gmail.com.

[Hongwei Xi]

You can introduce a static function as follows:

// lor for bitwise or

stacst lor_int_int : (int, int) -> int

stadef lor = lor_int_int // aliasing

dataprop type(int) =
   | {t: int} base (t) of (type_base(t))

   | {t, m: int} or (lor(t, m)) of (type(t), type_modifier(m))

Here is some code that may be helpful:

https://github.com/githwxi/ATS-Postiats/blob/master/prelude/basics_pre.sats

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/20140901180806.GA2216%40nixos.hsd1.nh.comcast.net.

[Hongwei Xi]

lor is already given the infix status. So write (t lor m) instead.

[Shea Levy]

Ah, I see. How do I implement the static function? All of the ones in
the prelude appear to be built in.

~Shea

> > https://groups.google.com/d/msgid/ats-lang-users/20140901180806.GA2216%40nixos.hsd1.nh.comcast.net

> > .
> >
>
> --
> 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/CAPPSPLqSbU0L6b%3DsoCfKrV3yTPrzsxZNjodf6nB_tUqXkYXGVA%40mail.gmail.com.

[gmhwxi]

No, static functions cannot be implemented in ATS.
You need a constraint-solver to interpret them. The built-in
constraint-solver for ATS does not handle bitwise operations.
Z3 does. Maybe Will Blair will let us know how to do it when
he is back.

[Blair, William]

> Hm, how do I spell the operations? I've got something like this to
> represent the arguments to the 'socket' function, which on Linux allows
> the 'type' argument to be bitwise-ored with certain modifiers (the ATS_
> prefix indicates a macro taken from a C include):

Right now using bitwise operators in the statics is a bit experimental with an
external constraint solver. I'm working on getting the solver into the main
ATS contrib repo so others may use it as well.

As far as syntax goes, you probably won't want to use the "int" sort
since any static int
term is considered a natural number without bound. Instead, we can use
a new sort
called a bit vector that models machine integers. This sort is
provided by most SMT
solvers so we can use it in the ATS statics.

If I understand your requirement correctly, suppose we have the
following type at our
disposal. This is hardly official, but it illustrates how I think you
could implement the example
you provided. This currently won't work in ATS right now.

abst@ype int (bv:bv16) = int

This associates a static signed 16 bit vector with the normal integer
type. Of course, the choice of
what size bit vector to use is machine dependent, but that's a
separate issue. We can rewrite your
example using the new bv16 sort in the statics using the lor operator
described by Hongwei.

dataprop domain(bv16) = AF_UNIX (ATS_AF_UNIX) (* TODO include other
address families *)

dataprop type_base(bv16) = SOCK_STREAM (ATS_SOCK_STREAM) (* TODO

include other socket types *)

dataprop type_modifier(bv16) = SOCK_NONBLOCK (ATS_SOCK_NONBLOCK) |
SOCK_CLOEXEC (ATS_SOCK_CLOEXEC)

dataprop type(bv16) =
| {t: bv16} base (t) of (type_base(bv16))
| {t, m: bv16} or ((t lor m)) of (type(t), type_modifier(m))

fn socket {d, t: bv16} (domain d, type t | int d, int t): [fd: int]
(filedes fd | int fd)

I need to finish adding more support for bit vectors in the external
constraint solver, but I'll post an announcement when
it's ready to use.

Thanks,
Will

On Mon, Sep 1, 2014 at 2:08 PM, Shea Levy <sh...@shealevy.com> wrote:

[Shea Levy]

Hi Will,

This sounds great! Let me know if you need any help testing.

~Shea

> To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEuDxfTb7QXJd4TvwcVAF70gMwZ3Rdsv%3D%3DwVOKDaJqOTs1vJOQ%40mail.gmail.com.

[William Blair]

Hi Shea,

That would be great. We can maybe try an example with the socket interface like you gave when it's ready.

Thanks,

Will

[Shea Levy]

Sounds good! Note that for now I've replaced the dataprops with subset
sorts [1] to avoid having to pass explicit proofs [2], but I suppose
there's no way to define subset sorts recursively, right? I'd need that
when adding back in the lor operator.

[1]: https://github.com/shlevy/socket-activate/blob/5617383608ac67cdc6e7d9e9f81f45914fb3fa3b/static/fd.sats#L20-L22
[2]: https://github.com/shlevy/socket-activate/blob/5617383608ac67cdc6e7d9e9f81f45914fb3fa3b/dynamic/socket-activate.dats#L15

~Shea

> > > >> > email to ats-lang-user...@googlegroups.com <javascript:>.

> > > >> > To post to this group, send email to ats-lan...@googlegroups.com

> > <javascript:>.

> > > >> > 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/20140901051852.GE2219%40nixos.hsd1.nh.comcast.net
> > > >> > .
> > > >> >
> > > >>
> > > >> --
> > > >> 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 <javascript:>.

> > > >> To post to this group, send email to ats-lan...@googlegroups.com

> > <javascript:>.

> > > >> 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/CAPPSPLrdCOS8MuVo9zs6d4gQXe3a%2BFB3TKAu5k1s0zA622VcZw%40mail.gmail.com.
> >
> > >
> > > --
> > > 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 <javascript:>.

> > > To post to this group, send email to ats-lan...@googlegroups.com

> > <javascript:>.

> > > 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/CAEuDxfTb7QXJd4TvwcVAF70gMwZ3Rdsv%3D%3DwVOKDaJqOTs1vJOQ%40mail.gmail.com.
> >
> >
>

> --
> 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/8f8b84f6-72e6-49d3-bfdd-f99863e29430%40googlegroups.com.

[Yannick Duchêne]

I just had the same question and just read this thread.

So for now, it seems better to do it with classical arithmetic operations: additions and subtractions, and appropriates tests with lower than, greater than, etc, and constants (as #define) for bits sets.

By the way, I also wondered if there is a sort for unsigned integers. I mean a sort, not a subset sort.

[gmhwxi]

There is no sort for unsigned integers.