agez vs addr > null

11 views
Skip to first unread message

David Smith

unread,
May 22, 2021, 5:53:31 PM5/22/21
to ats-lang-users

I find a lot of code like this:


absvtype

json_object_vtype (l:addr) = ptr

vtypedef

json_object (l:addr) = json_object_vtype (l)

vtypedef

json_object0 = [l:agez] json_object (l)

vtypedef
json_object1 = [l:addr | l > null] json_object (l)

I have multiple questions about this:

1. What is the difference between [l:agez] and [l:addr | l > null]?
2. What do the 0 and 1 signify?
3. Is the vtypedef for json_object here required? Can't the absvtype already be used for everything?

Thanks in advance.

Dambaev Alexander

unread,
May 22, 2021, 8:02:04 PM5/22/21
to ats-lan...@googlegroups.com
Hi,

1. agez stands for "address greater or equal zero". so it is like [l: addr | l >= null]. which is different from [l:addr | l > null], which is 'agz';
2. json_object0 defines a short cat to a json_object that can have null address. json_object1 in its turn, defines json_object that can only have address, greater than null;
3. json_object0 and json_object1 here just a shortcuts for cases, when you don't want to define, say:

```
fn
  my_foo0
  {l:agz}
   (json: !json_object(l)
   ):
   void
implement my_foo0 {l} ( json) = ... (* here l is available for use in the body *)
```
you can write the same as:
```
fn
  my_foo1
   (json: !json_object1
   ):
   void
implement my_foo1 (json) = ... (* here you have no l here available *)
```
the difference here is that 'l' is hidden from you in the body of `my_foo1`

Dambaev Alexander

unread,
May 22, 2021, 8:08:26 PM5/22/21
to ats-lan...@googlegroups.com
./prelude/basics_pre.sats:sortdef agz = { l:addr | l > null }
./prelude/basics_pre.sats:sortdef agez = { l:addr | l >= null }
./prelude/basics_pre.sats:sortdef alez = { l:addr | l <= null }

it seems, that addr can be less than null, by the way :)

Elijah Stone

unread,
May 22, 2021, 9:02:19 PM5/22/21
to ats-lan...@googlegroups.com
On Sun, 23 May 2021, Dambaev Alexander wrote:

> ./prelude/basics_pre.sats:sortdef alez = { l:addr | l <= null }
>
> it seems, that addr can be less than null, by the way :)

On AMD64, it is fairly sensible to think of addresses as signed values.

There is a set of addresses that are 'non-canonical' and cannot be
used--they will never map to anything. If you think about addresses as
signed, these non-canonical addresses are in the _middle_ of the space of
representable pointers; so the actual usable address space is segmented,
with one half at the bottom and one half at the top.

But a simpler way to think about it is that an address is a 48-bit
_signed_ integer, which is sign-extended to 64 bits.

See wikipedia https://en.wikipedia.org/wiki/X86-64#Canonical_form_addresses

(Though note that you're not very likely to ever encounter a negative
address; usually the kernel lives in the 'top half' of the address space
and userspace lives in the 'bottom half'.)

-E

Elijah Stone

unread,
May 22, 2021, 9:06:02 PM5/22/21
to ats-lan...@googlegroups.com
On Sat, 22 May 2021, Elijah Stone wrote:

> If you think about addresses as signed

Err, sorry, this should read 'if you think about addresses as _un_signed'.

David Smith

unread,
May 23, 2021, 6:03:32 AM5/23/21
to ats-lan...@googlegroups.com
Ah, my brain somehow went > and ≥ is the same.

Thanks to both of you!

--
You received this message because you are subscribed to a topic in the Google Groups "ats-lang-users" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/ats-lang-users/nPSM1AijcUc/unsubscribe.
To unsubscribe from this group and all its topics, send an email to ats-lang-user...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/5fc3f033-fdf2-6ea-4ca3-b4dde849630%40elronnd.net.

gmhwxi

unread,
May 24, 2021, 1:58:10 AM5/24/21
to ats-lang-users

At this point, 'addr' is mapped to 'int' in ATS2 as far as constraint-solving is of the concern.
We could try to make sure that a pointer of the type ptr(l) can never be constructed for any
negative l.

For instance, ptr_diff can be given the following type:

fun ptr_diff{l1,l2:addr | l1 >= l2} (p1: ptr(l1), p2: ptr(l2)): ptr(l1-l2)
Reply all
Reply to author
Forward
0 new messages