Hi all,
Does ATS support any bitwise operations on ints in the statics?
~Shea
Hi Will,
This sounds great! Let me know if you need any help testing.
~SheaOn Tue, Sep 02, 2014 at 09:44:02AM -0400, Blair, William wrote:
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) = intThis 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,
WillOn Mon, Sep 1, 2014 at 2:08 PM, Shea Levy sh...@shealevy.com wrote:
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
On Mon, Sep 01, 2014 at 01:33:32AM -0400, Hongwei Xi wrote:
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.On Mon, Sep 1, 2014 at 1:18 AM, Shea Levy sh...@shealevy.com wrote:
Hi all,
Does ATS support any bitwise operations on ints in the statics?
~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
.–
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/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.
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/CAEuDxfTb7QXJd4TvwcVAF70gMwZ3Rdsv%3D%3DwVOKDaJqOTs1vJOQ%40mail.gmail.com.
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.On Mon, Sep 1, 2014 at 1:18 AM, Shea Levy sh...@shealevy.com wrote:
Hi all,
Does ATS support any bitwise operations on ints in the statics?
~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
.
lor is already given the infix status. So write (t lor m) instead.On Mon, Sep 1, 2014 at 2:25 PM, Hongwei Xi gmh...@gmail.com wrote:
You can introduce a static function as follows:
// lor for bitwise or
stacst lor_int_int : (int, int) → int
stadef lor = lor_int_int // aliasingdataprop 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
On Mon, Sep 1, 2014 at 2:08 PM, Shea Levy sh...@shealevy.com wrote:
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
On Mon, Sep 01, 2014 at 01:33:32AM -0400, Hongwei Xi wrote:
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.On Mon, Sep 1, 2014 at 1:18 AM, Shea Levy sh...@shealevy.com wrote:
Hi all,
Does ATS support any bitwise operations on ints in the statics?
~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 visithttps://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.
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/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.
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/20140901180806.GA2216%40nixos.hsd1.nh.comcast.net
.
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.satsOn Mon, Sep 1, 2014 at 2:08 PM, Shea Levy sh...@shealevy.com wrote:
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
On Mon, Sep 01, 2014 at 01:33:32AM -0400, Hongwei Xi wrote:
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.On Mon, Sep 1, 2014 at 1:18 AM, Shea Levy sh...@shealevy.com wrote:
Hi all,
Does ATS support any bitwise operations on ints in the statics?
~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 visithttps://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.
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/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.
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/20140901180806.GA2216%40nixos.hsd1.nh.comcast.net
.
Ah, I see. How do I implement the static function? All of the ones in
the prelude appear to be built in.
~SheaOn Mon, Sep 01, 2014 at 02:25:07PM -0400, Hongwei Xi wrote:
You can introduce a static function as follows:
// lor for bitwise or
stacst lor_int_int : (int, int) → int
stadef lor = lor_int_int // aliasingdataprop 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
On Mon, Sep 1, 2014 at 2:08 PM, Shea Levy sh...@shealevy.com wrote:
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
On Mon, Sep 01, 2014 at 01:33:32AM -0400, Hongwei Xi wrote:
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.On Mon, Sep 1, 2014 at 1:18 AM, Shea Levy sh...@shealevy.com wrote:
Hi all,
Does ATS support any bitwise operations on ints in the statics?
~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 visithttps://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.
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/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.
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/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.
There is no sort for unsigned integers.On Saturday, December 12, 2015 at 9:21:43 AM UTC-5, Yannick Duchêne wrote:
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.Le lundi 1 septembre 2014 07:18:57 UTC+2, Shea Levy a écrit :
Hi all,
Does ATS support any bitwise operations on ints in the statics?
~Shea
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.On Monday, September 1, 2014 3:29:41 PM UTC-4, Shea Levy wrote:
Ah, I see. How do I implement the static function? All of the ones in
the prelude appear to be built in.~Shea
On Mon, Sep 01, 2014 at 02:25:07PM -0400, Hongwei Xi wrote:
You can introduce a static function as follows:
// lor for bitwise or
stacst lor_int_int : (int, int) → int
stadef lor = lor_int_int // aliasingdataprop 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
On Mon, Sep 1, 2014 at 2:08 PM, Shea Levy <sh...@shealevy.com <javascript:>> wrote:
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
On Mon, Sep 01, 2014 at 01:33:32AM -0400, Hongwei Xi wrote:
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.On Mon, Sep 1, 2014 at 1:18 AM, Shea Levy <sh...@shealevy.com <javascript:>> wrote:
Hi all,
Does ATS support any bitwise operations on ints in the statics?
~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...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@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...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com
<javascript:>.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit.
–
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...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com
<javascript:>.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visithttps://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...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@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/CAPPSPLqSbU0L6b%3DsoCfKrV3yTPrzsxZNjodf6nB_tUqXkYXGVA%40mail.gmail.com.
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.
~SheaOn Tue, Sep 02, 2014 at 11:42:10AM -0700, William Blair wrote:
Hi Shea,
That would be great. We can maybe try an example with the socket interface
like you gave when it’s ready.Thanks,
WillOn Tuesday, September 2, 2014 9:56:20 AM UTC-4, Shea Levy wrote:
Hi Will,
This sounds great! Let me know if you need any help testing.
~Shea
On Tue, Sep 02, 2014 at 09:44:02AM -0400, Blair, William wrote:
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) = intThis 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,
WillOn Mon, Sep 1, 2014 at 2:08 PM, Shea Levy <sh...@shealevy.com <javascript:>> wrote:
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
On Mon, Sep 01, 2014 at 01:33:32AM -0400, Hongwei Xi wrote:
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.On Mon, Sep 1, 2014 at 1:18 AM, Shea Levy <sh...@shealevy.com <javascript:>> wrote:
Hi all,
Does ATS support any bitwise operations on ints in the statics?
~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...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com
<javascript:>.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visithttps://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...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@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...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@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.
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.Le lundi 1 septembre 2014 07:18:57 UTC+2, Shea Levy a écrit :
Hi all,
Does ATS support any bitwise operations on ints in the statics?
~Shea
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,
WillOn Mon, Sep 1, 2014 at 2:08 PM, Shea Levy sh...@shealevy.com wrote:
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
On Mon, Sep 01, 2014 at 01:33:32AM -0400, Hongwei Xi wrote:
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.On Mon, Sep 1, 2014 at 1:18 AM, Shea Levy sh...@shealevy.com wrote:
Hi all,
Does ATS support any bitwise operations on ints in the statics?
~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
.–
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/CAPPSPLrdCOS8MuVo9zs6d4gQXe3a%2BFB3TKAu5k1s0zA622VcZw%40mail.gmail.com.
Hi Shea,
That would be great. We can maybe try an example with the socket interface
like you gave when it’s ready.
Thanks,
WillOn Tuesday, September 2, 2014 9:56:20 AM UTC-4, Shea Levy wrote:
Hi Will,
This sounds great! Let me know if you need any help testing.
~Shea
On Tue, Sep 02, 2014 at 09:44:02AM -0400, Blair, William wrote:
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) = intThis 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,
WillOn Mon, Sep 1, 2014 at 2:08 PM, Shea Levy <sh...@shealevy.com <javascript:>> wrote:
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
On Mon, Sep 01, 2014 at 01:33:32AM -0400, Hongwei Xi wrote:
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.On Mon, Sep 1, 2014 at 1:18 AM, Shea Levy <sh...@shealevy.com <javascript:>> wrote:
Hi all,
Does ATS support any bitwise operations on ints in the statics?
~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...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com
<javascript:>.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visithttps://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...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@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...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@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.
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).
~SheaOn Mon, Sep 01, 2014 at 01:33:32AM -0400, Hongwei Xi wrote:
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.On Mon, Sep 1, 2014 at 1:18 AM, Shea Levy sh...@shealevy.com wrote:
Hi all,
Does ATS support any bitwise operations on ints in the statics?
~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
.–
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/CAPPSPLrdCOS8MuVo9zs6d4gQXe3a%2BFB3TKAu5k1s0zA622VcZw%40mail.gmail.com.