Type_Invariant and Finalize

Type_Invariant and Finalize

[Natasha Kerensikova]

Hello,

I have been trying out the new contrat-oriented aspects on Ada 2012, and
wondered how Type_Invariant interacts with user-defined finalization.

I have several types for which a Type_Invariant makes sense (and is
often already mostly implemented the old-fashionned way, with pragma
Assert at the end of subprograms), except after the first call to
Finalize.

The latest example is a sorted array of non-null
paccess-to-indefinite-type values, where the "sortedness" is a natural
type inveriant, but in Finalize I release the memory using an instance
of Unchecked_Deallocation.

I'm already a bit uneasy with not having "not null except after
Finalize" access types, but in the example above after the first call to
Finalize I get an array of either null or invalid access values, and the
natural type invariant can't be computed.

Searching through the ARM, I can't see any special treatment of the
Finalize procedure with regard to Type_Invariant aspect, so presumably
the type inveriant is also checked at the end of Finalize.

Have I missed something that allows Finalize to make an object not fit
the type invariant?

Or should I prepare for it, e.g. with an explicit boolean record
component that is False for the most of the lifetime of the object,
until the first call to Finalize?


Thanks in advance for your insights,
Natasha

Re: Type_Invariant and Finalize

[Simon Wright]

Natasha Kerensikova <lithiumcat@instinctive.eu> writes:

> The latest example is a sorted array of non-null
> paccess-to-indefinite-type values, where the "sortedness" is a natural
> type inveriant, but in Finalize I release the memory using an instance
> of Unchecked_Deallocation.

I don't think these can be null-excluding access types, because you
can't instantiate Unchecked_Deallocation for such a type?

> Or should I prepare for it, e.g. with an explicit boolean record
> component that is False for the most of the lifetime of the object,
> until the first call to Finalize?

This approach is normal, if finalization isn't naturally idempotent.
Sometimes one can use an already-present access value which, if null,
means the object has already been finalized.

Re: Type_Invariant and Finalize

[Natasha Kerensikova]

On 2014-07-17, Simon Wright <simon@pushface.org> wrote:
> Natasha Kerensikova <lithiumcat@instinctive.eu> writes:
>
>> The latest example is a sorted array of non-null
>> paccess-to-indefinite-type values, where the "sortedness" is a natural
>> type inveriant, but in Finalize I release the memory using an instance
>> of Unchecked_Deallocation.
>
> I don't think these can be null-excluding access types, because you
> can't instantiate Unchecked_Deallocation for such a type?

Probably, though I admit I haven't tried, because it feels so obvious it
somehow won't work.

In the part you quoted, "non-null" was not referring to null exclusion,
but rather to the fact that in normal operation the values in the array
happen to not be null.

I have been toying with the idea of putting the null exclusion in the
record component or array declaration:

   type Array_Of_Indefinite_Elements is array (Index range <>)
     of not null Element_Access;

   type Node is record
      Key : not null Key_Access;
      Element : not null Element_Access;
   end record;

Such declarations would have helped catch a few bugs I encountered, so I
find the idea desirable. However it makes Finalize a bit messy: I can
use an instance of Unchecked_Deallocation on an intermediate variable,
and then the array/record has an invalid access value instead of a null
one, which is fine as long as nothing tries to dereference or free it,
so I can't use directly a Type_Invariant (unless there is some special
provision about Finalize that I missed, which is the whole question of
the thread), and Finalize idempotency has to be ensured in some other
way (e.g. with a Finalized boolean component).

But these are a lot of hassle for a very limited corner case (whatever
happens between the first call to Finalize and the last use of the
object). So I wish there was some way to have not-null-except-during-
finalization access types, and Type_Invariant_Except_During_Finalization
and *_Predicate_Except_During__Finalization aspects.

Doesn't it make sense to weaken these restrictions/contracts in such a
very specific and limited part of the object lifetime?


Natasha

Re: Type_Invariant and Finalize

[Robert A Duff]

Natasha Kerensikova <lithiumcat@instinctive.eu> writes:

> I have been toying with the idea of putting the null exclusion in the
> record component or array declaration:
>
>    type Array_Of_Indefinite_Elements is array (Index range <>)
>      of not null Element_Access;
>
>    type Node is record
>       Key : not null Key_Access;
>       Element : not null Element_Access;
>    end record;

I suggest using predicates instead of "not null":

    type Optional_Element_Access is access all Element'Class;
    subtype Element_Access is Optional_Element_Access with
        Predicate => Element_Access /= null;

"Predicate" is gnat-specific.  Use "Dynamic_Predicate" if you want to be
portable.  You can mostly use Element_Access, but use
Optional_Element_Access in the rare cases (e.g. inside Finalize)
where you want to allow null.

One problem with "not null" is that you can't create an object, and then
initialize it later.  Consider:

    X : Positive;
    ... -- No reads of X here.
    X := Something(...); -- Here we initialize X to some value >= 1.
    ... -- Now we can read X.

That works fine.  But similar code doesn't work with "not null":

    X : Element_Access;
    ... -- No reads of X here.
    X := Something(...); -- Here we initialize X to some non-null value.
    ... -- Now we can read X.

If Element_Access is declared "not null", then the declaration of X
blows up.  Using a predicate instead, it works the same way as the
Positive example.

- Bob

Type_Invariant and instance creation (was: Type_Invariant and Finalize)

[Simon Wright]

I wrote this to play with some of the concepts Natasha discussed, since
I haven't used the contract aspects before. It's a bit more complicated
than I'd have hoped because of the need for Adjust.

As it stands, it executes as expected with GNAT GPL 2014 (that is, the
finalizations occur OK and don't trigger assertion failures, but the
creation of an empty object does).

With FSF GCC 4.9.0, however, the assertion fails in Create at

      return (Ada.Finalization.Controlled with V => new Integer'(Value));

I tried inserting Put_Lines in the test program to get an idea of the
flow:

   declare
      Tmp : Releasing_Not_Null.R := Releasing_Not_Null.Create (42);
   begin
      Put_Line ("in first declare block");
   end;
   Put_Line ("first declare block done");

and now blow me down if GNAT GPL 2014 doesn't fail just like FSF GCC!

What am I doing wrong? Which compiler (if either) is right?

-- gnatchop from here --
with Ada.Finalization;
package Releasing_Not_Null is
   type R is new Ada.Finalization.Controlled with private;
   function Create (Value : Integer) return R;
private
   type P is access Integer;
   type R is new Ada.Finalization.Controlled with record
      V : P;
   end record
      with Type_Invariant => R.V /= null;
   overriding
   procedure Adjust (This : in out R);
   overriding
   procedure Finalize (This : in out R);
end Releasing_Not_Null;
with Ada.Unchecked_Deallocation;
package body Releasing_Not_Null is
   function Create (Value : Integer) return R is
   begin
      return (Ada.Finalization.Controlled with V => new Integer'(Value));
   end Create;
   procedure Adjust (This : in out R) is
   begin
      This.V := new Integer'(This.V.all);
   end Adjust;
   procedure Finalize (This : in out R) is
      procedure Free is new Ada.Unchecked_Deallocation (Integer, P);
   begin
      if This.V /= null then
         Free (This.V);
      end if;
   end Finalize;
end Releasing_Not_Null;
with Releasing_Not_Null;
procedure Test_Releasing_Not_Null is
begin
   declare  -- this block is OK
      Tmp : Releasing_Not_Null.R := Releasing_Not_Null.Create (42);
   begin
      null;
   end;
   declare
      Tmp : Releasing_Not_Null.R;  -- Failed invariant here
   begin
      null;
   end;
end Test_Releasing_Not_Null;

Re: Type_Invariant and instance creation (was: Type_Invariant and Finalize)

[Randy Brukardt]

"Simon Wright" <simon@pushface.org> wrote in message 
news:lyy4vrwu4q.fsf@pushface.org...
...
> What am I doing wrong? Which compiler (if either) is right?

I'd guess that both are wrong, although it may not have to do with this 
example. :-) There's lots of issues with Type_Invariant (it seems SO 
simple); we've pretty much given up on making it bullet-proof. We just 
approved yet another AI on the topic (AI12-0042-1/09 -- 8 versions before 
this one!) and I suspect that we haven't found all of the problems. Both 
predicates and postconditions are in better shape, so I'd use them more than 
type invariants.

                                           Randy.

Re: Type_Invariant and instance creation

[Shark8]

On 21-Jul-14 17:29, Randy Brukardt wrote:
> I'd guess that both are wrong, although it may not have to do with this
> example.:-)  There's lots of issues with Type_Invariant (it seems SO
> simple); we've pretty much given up on making it bullet-proof. We just
> approved yet another AI on the topic (AI12-0042-1/09 -- 8 versions before
> this one!) and I suspect that we haven't found all of the problems. Both
> predicates and postconditions are in better shape, so I'd use them more than
> type invariants.


That's disappointing to hear.
I was poking around the WordPerfect SDK [WPD format], and was thinking 
Type_Invariant would be perfect for that.


     Type File_Header is record
         Padding_Prefix	: Interfaces.Unsigned_8;
         Signature	: String(1..3);
         Document_Offset	: Interfaces.Unsigned_32;
         --Product : Product_Type;
         Document_Type	: File_Types;
     end record
     with Type_Invariant =>
         File_Header.Padding_Prefix = 16#FF#
AND	File_Header.Signature = "WPC";