Aliasing of by-ref arguments

Google Group
1

Say I have a function of the following signature:

fun f (x: &int, y: &int): void

And I’d like to prohibit calling it with the same argument:

val () = f (c, c)

where c is some variable. How to do that?

2

The following code typechecks in ATS2:

extern
fun
foo
(
&int >> int(1), &int >> int(2)
) : void

val () =
let var c: int = 0 in foo (c, c) end
// end of [val]

When I said “strictly speaking”, I meant programming in the core of ATS,
where the interface of foo translates into the following version:

fun
foo{l1,l2:addr} (pf1: !int@l1, !pf2: !int@l2 | ptr(l1), ptr(l2)): void

With this translated interface, f(c, c) cannot be translated accordingly.

However, ATS2 is not so strict. Being so strict is morally right but it
stifles programming.
Programming-first programming verification is what I really like to
advocate.On Saturday, March 14, 2015 at 2:06:36 PM UTC-4, Shea Levy wrote:

When you say that it assumes they are distinct, does that mean it’s a
compile-time error to alias them? Or is it just “undefined behavior” that
happens to be OK when they are read-only?

On Mar 14, 2015, at 2:01 PM, gmhwxi <gmh...@gmail.com <javascript:>> wrote:

Strictly speaking, the following interface assumes that x and y are
distinct:

fun f (x: &int, y: &int): void

Usually, the reason for f(c, c) being okay is that the views for x and y
are
only needed to be read-only.

Unsafely, you can do

val (pf, fpf | p2) = $UN.ptr0_vtake{int}(addr@c)
val () = f (c, !p2)
prval () = fpf (pf)

On Saturday, March 14, 2015 at 11:21:29 AM UTC-4, Artyom Shalkhakov wrote:

Say I have a function of the following signature:

fun f (x: &int, y: &int): void

And I’d like to prohibit calling it with the same argument:

val () = f (c, c)

where c is some variable. How to do that?

–
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/17202669-61e6-4254-9347-403069db24f2%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/17202669-61e6-4254-9347-403069db24f2%40googlegroups.com?utm_medium=email&utm_source=footer
.

3

The following code typechecks in ATS2:

extern
fun
foo
(
&int >> int(1), &int >> int(2)
) : void

val () =
let var c: int = 0 in foo (c, c) end
// end of [val]

When I said “strictly speaking”, I meant programming in the core of ATS,
where the interface of foo translates into the following version:

fun
foo{l1,l2:addr} (pf1: !int@l1, !pf2: !int@l2 | ptr(l1), ptr(l2)): void

With this translated interface, f(c, c) cannot be translated accordingly.

However, ATS2 is not so strict. Being so strict is morally right but it
stifles programming.
Programming-first programming verification is what I really like to
advocate.

OK, so I’ll use views and pointers in this case.

4

I think this case can be handled by taking ptrs + views. Since you shouldn’t ever be able to get two int @ l views for the same l, passing in int @ l1 and int @ l2 requires them to be different, right?> On Mar 14, 2015, at 11:21 AM, Artyom Shalkhakov artyom.s...@gmail.com wrote:

Say I have a function of the following signature:

fun f (x: &int, y: &int): void

And I’d like to prohibit calling it with the same argument:

val () = f (c, c)

where c is some variable. How to do that?

–
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 mailto:ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com mailto:ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users 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/bd8b79fe-1c78-4fd8-a392-ed7d05bd1eb8%40googlegroups.com https://groups.google.com/d/msgid/ats-lang-users/bd8b79fe-1c78-4fd8-a392-ed7d05bd1eb8%40googlegroups.com?utm_medium=email&utm_source=footer.

5

When you say that it assumes they are distinct, does that mean it’s a compile-time error to alias them? Or is it just “undefined behavior” that happens to be OK when they are read-only?> On Mar 14, 2015, at 2:01 PM, gmhwxi gmh...@gmail.com wrote:

Strictly speaking, the following interface assumes that x and y are distinct:

fun f (x: &int, y: &int): void

Usually, the reason for f(c, c) being okay is that the views for x and y are
only needed to be read-only.

Unsafely, you can do

val (pf, fpf | p2) = $UN.ptr0_vtake{int}(addr@c)
val () = f (c, !p2)
prval () = fpf (pf)

On Saturday, March 14, 2015 at 11:21:29 AM UTC-4, Artyom Shalkhakov wrote:
Say I have a function of the following signature:

fun f (x: &int, y: &int): void

And I’d like to prohibit calling it with the same argument:

val () = f (c, c)

where c is some variable. How to do that?

–
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 mailto:ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com mailto:ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users 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/17202669-61e6-4254-9347-403069db24f2%40googlegroups.com https://groups.google.com/d/msgid/ats-lang-users/17202669-61e6-4254-9347-403069db24f2%40googlegroups.com?utm_medium=email&utm_source=footer.

6

Strictly speaking, the following interface assumes that x and y are
distinct:

fun f (x: &int, y: &int): void

Usually, the reason for f(c, c) being okay is that the views for x and y are
only needed to be read-only.

Unsafely, you can do

val (pf, fpf | p2) = $UN.ptr0_vtake{int}(addr@c)
val () = f (c, !p2)
prval () = fpf (pf)On Saturday, March 14, 2015 at 11:21:29 AM UTC-4, Artyom Shalkhakov wrote:

Say I have a function of the following signature:

fun f (x: &int, y: &int): void

And I’d like to prohibit calling it with the same argument:

val () = f (c, c)

where c is some variable. How to do that?