Implementing Rust's borrow checked pointers

Implementing Rust's borrow checked pointers

[Lucretia]

Hi,

Been talking to someone on Telegraph and he was saying Ada should implement this, just wondering whether Ada could? I posed a slight change to access type specification to do this, what do people think?

type P is restricted access X;

Restricted in this case would mean that once assigned it cannot be re-assigned into or out of with out some sort of move operation, which could be implemented as an attribute on the access type.

A : P := L'Access;
B : P := A'Move; --  A cannot no longer be used.

begin
   A.all ... ; -- raises exception.


I don't know enough about all this to put a complete proposal together, but I think I've got the basics understood.

Luke.

Re: Implementing Rust's borrow checked pointers

[Dmitry A. Kazakov]

On 2019-09-24 11:05, Lucretia wrote:

> Been talking to someone on Telegraph and he was saying Ada should implement this, just wondering whether Ada could? I posed a slight change to access type specification to do this, what do people think?
> 
> type P is restricted access X;
> 
> Restricted in this case would mean that once assigned it cannot be re-assigned into or out of with out some sort of move operation, which could be implemented as an attribute on the access type.
> 
> A : P := L'Access;
> B : P := A'Move; --  A cannot no longer be used.
> 
> begin
>     A.all ... ; -- raises exception.
> 
> 
> I don't know enough about all this to put a complete proposal together, but I think I've got the basics understood.

Since run-time checks are involved the whole idea does not make sense to me.

Semantically it makes no sense either. Why copying should have this 
effect on pointer when, as in your example, unrelated to scopes (or 
unchecked deallocation)?

A more realistic example might help.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Implementing Rust's borrow checked pointers

[Optikos]

On Tuesday, September 24, 2019 at 4:05:45 AM UTC-5, Lucretia wrote:
> Hi,
> 
> Been talking to someone on Telegraph and he was saying Ada should implement this, just wondering
> whether Ada could? I posed a slight change to access type specification to do this, what do people
> think?
> 
> type P is restricted access X;
> 
> Restricted in this case would mean that once assigned it cannot be re-assigned into or out of with out
> some sort of move operation, which could be implemented as an attribute on the access type.
> 
> A : P := L'Access;
> B : P := A'Move; --  A cannot no longer be used.
> 
> begin
>    A.all ... ; -- raises exception.

No, to be as useful as Rust's borrow checker, instead of raising exception, it needs to be a compile-time error.  The compiler needs to maintain a whole-program directed graph at compile-time, not defer a detection-based localized analysis to run-time.

> I don't know enough about all this to put a complete proposal together, but I think I've got the basics
> understood.
> 
> Luke.

Re: Implementing Rust's borrow checked pointers

[Lucretia]

On Tuesday, 24 September 2019 12:23:30 UTC+1, Optikos  wrote:

> > begin
> >    A.all ... ; -- raises exception.
> 
> No, to be as useful as Rust's borrow checker, instead of raising exception, it needs to be a compile-time error.  The compiler needs to maintain a whole-program directed graph at compile-time, not defer a detection-based localized analysis to run-time.

Yes, the compiler would raise that exception at compile time. This idea that all exceptions are raised at runtime is false and you should check the AARM.

Re: Implementing Rust's borrow checked pointers

[Lucretia]

Seems there is an AI for this already.

Re: Implementing Rust's borrow checked pointers

[Optikos]

On Tuesday, September 24, 2019 at 7:02:26 AM UTC-5, Lucretia wrote:
> On Tuesday, 24 September 2019 12:23:30 UTC+1, Optikos  wrote:
> 
> > > begin
> > >    A.all ... ; -- raises exception.
> > 
> > No, to be as useful as Rust's borrow checker, instead of raising exception, it needs to be a compile-time
> > error.  The compiler needs to maintain a whole-program directed graph at compile-time, not defer a
> > detection-based localized analysis to run-time.
> 
> Yes, the compiler would raise that exception at compile time. This idea that all exceptions are raised at
> runtime is false and you should check the AARM.

Well, at some vague generalized concept level, I & the AARM agree with your stated principle, but at a narrow technocratic reading of the actual text of the AARM as written you are incorrect.  The proper term-of-art for what you are referring to is “error” not “exception”.  I just checked; each usage throughout the entire AARM of the term “exception” are
1) utilized in the context of run-time •error•
or
2) the English-language general dictionary definition of exclusion from the topic being discussed, such as “There are a few exceptions to this general principle” in the side note in §2.8.

“§1.1.5 Classification of •Errors•

“The language definition classifies errors into several different categories:

“● •Errors• that are required to be detected ••prior to run time•• by every Ada implementation;

“These errors correspond to any violation of a rule given in this International Standard, other than
those listed below. In particular, violation of any rule that uses the terms shall, allowed,
permitted, legal, or illegal belongs to this category. Any program that contains such an error is not
a legal Ada program; …

“The rules are further classified as either •compile•-time rules†, or •post-compilation• rules†, depending
on whether a violation has to be detected at the time a compilation unit is submitted to the
compiler, or may be postponed until the time a compilation unit is incorporated into a partition of
a program.

“● Errors that are required to be detected at run time by the execution of an Ada program;

“The corresponding error situations are associated with the names of the predefined exceptions.
Every Ada compiler is required to generate code that raises the corresponding exception if such an error situation arises during program execution. [If such an •error• situation is certain to arise in
every execution of a construct, then an implementation is •••allowed (although not required)••• to
report this fact at •compilation• time.‡]

“● Bounded errors;

“The language rules define certain kinds of errors that need •not• be detected either •prior to• or
during run time, but if not detected, the range of possible effects shall be bounded. The errors of
this category are called bounded errors. The possible effects of a given bounded error are
specified for each such error, but in any case one possible effect of a bounded error is the raising
of the exception Program_Error.

“● Erroneous execution …”

† I'll amend my prior comment's “compile-time error” to include “post-compilation error” at link-time as well to support an implementation that stitches together each compilation-unit's borrow-checker directed graphs to build up a whole-program borrow-checker directed graph at link-time, as per “post-compilation error” in the 2nd ¶ under the 1st ● above.

‡ Note the absence of the term “exception” in this sentence which would have been a really good time to utilize it if your definition of exception held.  Note the presence of the term “error” in this sentence instead.

Re: Implementing Rust's borrow checked pointers

[Jeffrey R. Carter]

On 9/24/19 11:05 AM, Lucretia wrote:
> 
> type P is restricted access X;
> 
> Restricted in this case would mean that once assigned it cannot be re-assigned into or out of with out some sort of move operation, which could be implemented as an attribute on the access type.

What's wrong with "limited"?

There's already work on including something like Rust's borrow checking into 
Ada, but given how rarely access types are needed, and how easy it usually is to 
confine them to a restricted scope when they are, I don't see that it's worth 
the effort.

-- 
Jeff Carter
"Drown in a vat of whiskey. Death, where is thy sting?"
Never Give a Sucker an Even Break
106

Re: Implementing Rust's borrow checked pointers

[Simon Wright]

Lucretia <laguest9000@googlemail.com> writes:

> On Tuesday, 24 September 2019 12:23:30 UTC+1, Optikos  wrote:
>
>> > begin
>> >    A.all ... ; -- raises exception.
>> 
>> No, to be as useful as Rust's borrow checker, instead of raising
>> exception, it needs to be a compile-time error.  The compiler needs
>> to maintain a whole-program directed graph at compile-time, not
>> defer a detection-based localized analysis to run-time.
>
> Yes, the compiler would raise that exception at compile time. This
> idea that all exceptions are raised at runtime is false and you should
> check the AARM.

GNAT could (guessing here, but following the way it handles CE detected
at compile time) raise a *warning* to the effect that an exception ould
be raised at run time. And if compiling with warning => error (-gnatwe)
that would do the job. To an extent.

Re: Implementing Rust's borrow checked pointers

[Keith Thompson]

Lucretia <laguest9000@googlemail.com> writes:
> On Tuesday, 24 September 2019 12:23:30 UTC+1, Optikos  wrote:
>
>> > begin
>> >    A.all ... ; -- raises exception.
>> 
>> No, to be as useful as Rust's borrow checker, instead of raising
>> exception, it needs to be a compile-time error.  The compiler needs
>> to maintain a whole-program directed graph at compile-time, not defer
>> a detection-based localized analysis to run-time.
>
> Yes, the compiler would raise that exception at compile time. This
> idea that all exceptions are raised at runtime is false and you should
> check the AARM.

Can you provide a specific citation?

Certainly a compiler can diagnose an error at compile time, but I've
never heard that referred to as an "exception".  And a compiler can
generate code that unconditionally raises an exception, but that code is
executed at run time.

(I've seen compile-time exceptions, but they were compiler bugs, not
diagnostics for the program being compiled.)

-- 
Keith Thompson (The_Other_Keith) kst-u@mib.org  <http://www.ghoti.net/~kst>
Will write code for food.
void Void(void) { Void(); } /* The recursive call of the void */

Re: Implementing Rust's borrow checked pointers

[Optikos]

On Tuesday, September 24, 2019 at 2:13:33 PM UTC-5, Keith Thompson wrote:
> Lucretia <laguest9000@googlemail.com> writes:
> > On Tuesday, 24 September 2019 12:23:30 UTC+1, Optikos  wrote:
> >
> >> > begin
> >> >    A.all ... ; -- raises exception.
> >> 
> >> No, to be as useful as Rust's borrow checker, instead of raising
> >> exception, it needs to be a compile-time error.  The compiler needs
> >> to maintain a whole-program directed graph at compile-time, not defer
> >> a detection-based localized analysis to run-time.
> >
> > Yes, the compiler would raise that exception at compile time. This
> > idea that all exceptions are raised at runtime is false and you should
> > check the AARM.
> 
> Can you provide a specific citation?
> 
> Certainly a compiler can diagnose an error at compile time, but I've
> never heard that referred to as an "exception".  And a compiler can
> generate code that unconditionally raises an exception, but that code is
> executed at run time.
> 
> (I've seen compile-time exceptions, but they were compiler bugs, not
> diagnostics for the program being compiled.)
> 
> -- 
> Keith Thompson (The_Other_Keith) kst-u@mib.org  <http://www.ghoti.net/~kst>
> Will write code for food.
> void Void(void) { Void(); } /* The recursive call of the void */

Keith, I already did in a prior posting above, but you apparently blocked me, so your loss.  Here is the answer to your question again for all other readers:  §1.1.5 Classification of •Errors “If such an •error• situation is certain to arise in every execution of a construct, then an implementation is •••allowed (although not required)••• to report this fact at •compilation• time.” 

Re: Implementing Rust's borrow checked pointers

[Keith Thompson]

Optikos <optikos@verizon.net> writes:
> On Tuesday, September 24, 2019 at 2:13:33 PM UTC-5, Keith Thompson wrote:
>> Lucretia <laguest9000@googlemail.com> writes:
[...]
>> > Yes, the compiler would raise that exception at compile time. This
>> > idea that all exceptions are raised at runtime is false and you should
>> > check the AARM.
>> 
>> Can you provide a specific citation?
>> 
>> Certainly a compiler can diagnose an error at compile time, but I've
>> never heard that referred to as an "exception".  And a compiler can
>> generate code that unconditionally raises an exception, but that code is
>> executed at run time.
>> 
>> (I've seen compile-time exceptions, but they were compiler bugs, not
>> diagnostics for the program being compiled.)
>
> Keith, I already did in a prior posting above, but you apparently
> blocked me, so your loss.

I have not blocked you.  It's entirely possible that I missed your
earlier article (I don't follow this newsgroup all that closely),
or that I read it but didn't think it supported the assertion.

>                            Here is the answer to your question again
> for all other readers: §1.1.5 Classification of •Errors “If such an
> •error• situation is certain to arise in every execution of a
> construct, then an implementation is •••allowed (although not
> required)••• to report this fact at •compilation• time.”

That doesn't describe raising an exception at compilation time.
It describes (optionally) *reporting* at compilation time that an
exception is certain to be raised at run time.

Again, the claim (from Lucretia, not from you) was:

    Yes, the compiler would raise that exception at compile
    time. This idea that all exceptions are raised at runtime is
    false and you should check the AARM.

Printing a warning message is not raising an exception.

-- 
Keith Thompson (The_Other_Keith) kst-u@mib.org  <http://www.ghoti.net/~kst>
Will write code for food.
void Void(void) { Void(); } /* The recursive call of the void */

Re: Implementing Rust's borrow checked pointers

[Optikos]

On Tuesday, September 24, 2019 at 3:31:15 PM UTC-5, Keith Thompson wrote:
> Optikos writes:
> > On Tuesday, September 24, 2019 at 2:13:33 PM UTC-5, Keith Thompson wrote:
> >> Lucretia <laguest9000@googlemail.com> writes:
> [...]
> >> > Yes, the compiler would raise that exception at compile time. This
> >> > idea that all exceptions are raised at runtime is false and you should
> >> > check the AARM.
> >> 
> >> Can you provide a specific citation?
> >> 
> >> Certainly a compiler can diagnose an error at compile time, but I've
> >> never heard that referred to as an "exception".  And a compiler can
> >> generate code that unconditionally raises an exception, but that code is
> >> executed at run time.
> >> 
> >> (I've seen compile-time exceptions, but they were compiler bugs, not
> >> diagnostics for the program being compiled.)
> >
> > Keith, I already did in a prior posting above, but you apparently
> > blocked me, so your loss.
> 
> I have not blocked you.  It's entirely possible that I missed your
> earlier article (I don't follow this newsgroup all that closely),
> or that I read it but didn't think it supported the assertion.
> 
> >                            Here is the answer to your question again
> > for all other readers: §1.1.5 Classification of •Errors “If such an
> > •error• situation is certain to arise in every execution of a
> > construct, then an implementation is •••allowed (although not
> > required)••• to report this fact at •compilation• time.”
> 
> That doesn't describe raising an exception at compilation time.
> It describes (optionally) *reporting* at compilation time that an
> exception is certain to be raised at run time.
> 
> Again, the claim (from Lucretia, not from you) was:
> 
>     Yes, the compiler would raise that exception at compile
>     time. This idea that all exceptions are raised at runtime is
>     false and you should check the AARM.

I already answered that in my 9:08AM reply today.  I demonstrated via extensive quotation from AARM that Luke utilized the incorrect term-of-art.  According to the AARM as written, Luke meant “error” (as quoted from AARM) when he wrote “exception” (as quoted from c.l.a).  With a relatively minor change from Luke's “raise exception” to emit error message at compile-time, Luke's statement is otherwise correct.

> Printing a warning message is not raising an exception.

Re: Implementing Rust's borrow checked pointers

[Keith Thompson]

Optikos <optikos@verizon.net> writes:
> On Tuesday, September 24, 2019 at 3:31:15 PM UTC-5, Keith Thompson wrote:
[...]
>> Again, the claim (from Lucretia, not from you) was:
>> 
>>     Yes, the compiler would raise that exception at compile
>>     time. This idea that all exceptions are raised at runtime is
>>     false and you should check the AARM.
>
> I already answered that in my 9:08AM reply today.  I demonstrated via
> extensive quotation from AARM that Luke utilized the incorrect
> term-of-art.  According to the AARM as written, Luke meant “error” (as
> quoted from AARM) when he wrote “exception” (as quoted from c.l.a).
> With a relatively minor change from Luke's “raise exception” to emit
> error message at compile-time, Luke's statement is otherwise correct.
>
>> Printing a warning message is not raising an exception.

Ah, so you're agreeing with me.

I asked Lucretia to support the assertion that exceptions can be
raised during compilation.  I'm not sure your response was helpful.
I'd be interested in seeing a response *from Lucretia*. (Yes,
this is a public newsgroup and anyone can reply to anything, but
my question was intended to be directed to Lucretia.)

I think Lucretia simply made a mistake, but given the apparent
strength of the assertion I'd like to see a clarification.

-- 
Keith Thompson (The_Other_Keith) kst-u@mib.org  <http://www.ghoti.net/~kst>
Will write code for food.
void Void(void) { Void(); } /* The recursive call of the void */

Re: Implementing Rust's borrow checked pointers

[Lucretia]

On Tuesday, 24 September 2019 20:13:33 UTC+1, Keith Thompson  wrote:
> Lucretia <no> writes:
> > On Tuesday, 24 September 2019 12:23:30 UTC+1, Optikos  wrote:
> >
> >> > begin
> >> >    A.all ... ; -- raises exception.
> >> 
> >> No, to be as useful as Rust's borrow checker, instead of raising
> >> exception, it needs to be a compile-time error.  The compiler needs
> >> to maintain a whole-program directed graph at compile-time, not defer
> >> a detection-based localized analysis to run-time.
> >
> > Yes, the compiler would raise that exception at compile time. This
> > idea that all exceptions are raised at runtime is false and you should
> > check the AARM.
> 
> Can you provide a specific citation?

No, I'm fairly sure I saw it in one of the AARM's under compilation requirements years ago, but I cannot find it now.

> Certainly a compiler can diagnose an error at compile time, but I've
> never heard that referred to as an "exception".  And a compiler can
> generate code that unconditionally raises an exception, but that code is
> executed at run time.

I read it as the environment raises an exception like program_error on a compilation error.

Re: Implementing Rust's borrow checked pointers

[Keith Thompson]

Lucretia <laguest9000@googlemail.com> writes:
> On Tuesday, 24 September 2019 20:13:33 UTC+1, Keith Thompson  wrote:
>> Lucretia <no> writes:
>> > On Tuesday, 24 September 2019 12:23:30 UTC+1, Optikos  wrote:
>> >
>> >> > begin
>> >> >    A.all ... ; -- raises exception.
>> >> 
>> >> No, to be as useful as Rust's borrow checker, instead of raising
>> >> exception, it needs to be a compile-time error.  The compiler needs
>> >> to maintain a whole-program directed graph at compile-time, not defer
>> >> a detection-based localized analysis to run-time.
>> >
>> > Yes, the compiler would raise that exception at compile time. This
>> > idea that all exceptions are raised at runtime is false and you should
>> > check the AARM.
>> 
>> Can you provide a specific citation?
>
> No, I'm fairly sure I saw it in one of the AARM's under compilation
> requirements years ago, but I cannot find it now.
>
>> Certainly a compiler can diagnose an error at compile time, but I've
>> never heard that referred to as an "exception".  And a compiler can
>> generate code that unconditionally raises an exception, but that code is
>> executed at run time.
>
> I read it as the environment raises an exception like program_error on
> a compilation error.

Normally a compilation error prevents the generation of an executable,
so there's no environment in which an exception could be raised.

I suspect you're thinking of this (quoting the 2012 RM):

    Implementation Advice

    If an implementation detects a bounded error or erroneous execution,
    it should raise Program_Error.

"Erroneous execution" refers to an error that the implementation
is not required to detect or diagnose (called "undefined behavior"
in some other languages).  "Bounded errors" are similar, but are
limited in what can happen if the error occurs.

The "implementation" raising Program_Error doesn't imply a
compile-time exception.  Rather the compiler can generate code
that will (unconditionally) raise Program_Error at run time.
And the compiler may also issue a compile-time warning (as it can
about anything).

Unless I've missed something, there is no such thing as a
compile-time exception.  (A compiler implemented in Ada -- or C++,
for that matter -- might/throw raise an exception, but that's
a compiler bug if it's not handled.  The Ada standard makes no
assumptions about how a compiler is implemented.)

-- 
Keith Thompson (The_Other_Keith) kst-u@mib.org  <http://www.ghoti.net/~kst>
Will write code for food.
void Void(void) { Void(); } /* The recursive call of the void */

Re: Implementing Rust's borrow checked pointers

[J-P. Rosen]

Le 25/09/2019 à 00:09, Lucretia a écrit :
>> Can you provide a specific citation?
> No, I'm fairly sure I saw it in one of the AARM's under compilation requirements years ago, but I cannot find it now.
> 
You may be confused by 4.9(34/3):
"The expression is illegal if its evaluation fails a language-defined
check other than Overflow_Check. For the purposes of this evaluation,
the assertion policy is assumed to be Check."

This means that it is an error if a static expression (evaluated at
compile-time) would raise an exception.

-- 
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00
http://www.adalog.fr

Re: Implementing Rust's borrow checked pointers

[Simon Wright]

"J-P. Rosen" <rosen@adalog.fr> writes:

> Le 25/09/2019 à 00:09, Lucretia a écrit :
>>> Can you provide a specific citation?
>> No, I'm fairly sure I saw it in one of the AARM's under compilation
>> requirements years ago, but I cannot find it now.
>> 
> You may be confused by 4.9(34/3):
> "The expression is illegal if its evaluation fails a language-defined
> check other than Overflow_Check. For the purposes of this evaluation,
> the assertion policy is assumed to be Check."
>
> This means that it is an error if a static expression (evaluated at
> compile-time) would raise an exception.

As in

     1. package Compile_Time is
     2.
     3.    Bad : constant Integer := Integer'Last * 2;
                                                  |
        >>> value not in range of type "Standard.Integer"
        >>> static expression fails Constraint_Check

     4.
     5. end Compile_Time;

 5 lines: 2 errors
gnatmake: "compile_time.ads" compilation error

Re: Implementing Rust's borrow checked pointers

[Florian Weimer]

* Jeffrey R. Carter:

> There's already work on including something like Rust's borrow
> checking into Ada, but given how rarely access types are needed, and
> how easy it usually is to confine them to a restricted scope when
> they are, I don't see that it's worth the effort.

On the other hand, access types are not the only source of unsoundness
in Ada.  There is at least one other problem, involving records with
discriminants with defaults and aliasing.

Re: Implementing Rust's borrow checked pointers

[Stephen Leake]

On Tuesday, September 24, 2019 at 5:23:54 AM UTC-7, Lucretia wrote:
> Seems there is an AI for this already.

http://www.ada-auth.org/ai-files/grab_bag/AI12-0240-1v7-stt.TXT

This technique is also now in SPARK, which allows SPARK programs to use access types (in a limited way). See the SPARK reference manual https://docs.adacore.com/spark2014-docs/html/lrm/declarations-and-types.html#access-types