agez vs addr > null

[David Smith]

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]

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]

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

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]

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]

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]

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)