Re: Help with Atomic_Components and whole array assignment

[Nick Williams <nickw@acm.org>]

Tucker Taft wrote:


>> The compound statement
>>    for I in A'Range loop
>>       A(I) := 0;
>>    end loop;
>> has information flow "derives A from A", which is significantly
>> different.

> I don't understand why this derives A from A.  Is this just
> a limitation of SPARK?  Clearly, we are assigning a new
> value to every component of A, making no use of the original
> values.

Well, yes; clearly, it is simple to prove that this loop assigns new 
values to every element of A, but in terms of information flow (as 
defined by Bergeretti and Carre, and as implemented in the SPARK 
Examiner) it 'derives A from A'.

The central intuition derives from the first iteration through the loop 
- in this case, the new value of A is derived from a constant loop 
range, a literal constant and A itself (since only one element has changed).

The limitation is that array elements are not 'first class' from the 
perspective of the flow analyser - even if this were theoretically 
viable, the practicalities of tracking flow relations for a ten million 
element array would, I suspect, be prohibitive.

However - as I understand it - it's not even technically useful to 
promote array elements in this way within the current framework; to do 
so makes flow analysis equivalent to execution:

   subtype A_Type is Integer range 1 .. 1000;
   type An_Array is array A_Type of Integer;

   A : An_Array;
   X : A_Type;
   function Complicated_Function returns A_Type;
   function Another_Complicated_Function returns Integer;

   ...

   X := Complicated_Function;
   A(X) := Another_Complicated_Function;

Without actually calculating X, all that can be said is that any given 
element of A might potentially be assigned to by the above statements. 
However it equally well might not, and (as such) for all relevant I, 
A(I) would be derived from A(I), and whatever variables are used in the 
derivation of the result of Another_Complicated_Function.

Although I'm sure there are some simple cases where performing flow 
analysis at the array element level gives more intuitively 'correct' 
analyses, I'm minded to think that it probably would not be a very 
useful addition - I'm sure Peter or Rod will pick me up if they disagree!

Cheers,

Nick
PxCS