Question about SPARK flow error.

Question about SPARK flow error.

[Peter C. Chapin]

My example isn't complete enough to compile, but I could work up a complete
example if necessary. Hopefully this will be accurate and complete enough...

Consider the following procedure:

procedure Add_Item
   (Item : in Some_Type; Index : out Index_Type) is

   Found : Boolean;
begin
   Found := False;

   -- Let's see if the Item already exists in the storage.
   for I in Index_Type range Index_Type'First .. Size loop
      if Storage(I) = Item then
         Index := I;     -- It does. Return the current position.
         Found := True;
         exit;
      end if;
   end loop;

   if not Found then
      -- The Item does not already exist. Install it in the next slot.
      Storage(Next_Index) := Item;
      Index := Next_Index;    -- Return where we installed it.

      -- Play around with Size and Next_Index to set them up for next time
      -- (not shown).
   end if;
end Add_Item;

SPARK gives me an error, "Flow Error 602 - The undefined initial value of
Index may be used in the derivation of Index." I understand this to mean that
there is a path through the procedure where Index (being an out parameter) is
never given a value. So SPARK might be thinking, "Okay... the loop might run
to completion without ever setting Index inside the inner conditional
statement. Then it might skip over the next conditional statement and thus
never set Index at all."

However, if I'm not mistaken that can't actually happen. If the conditional
statement inside the loop never runs, Found will still be False and the
second conditional will definitely execute. Index will receive a value either
inside the loop or later.

Am I missing something or is this reasoning outside of the abilities of
SPARK's flow analysis? Is there some other idiomatic way I should be handling
this sort of situation?

Thanks

Peter

Re: Question about SPARK flow error.

[Phil Thornley]

On 19 June, 17:58, "Peter C. Chapin" <pcc482...@gmail.com> wrote:
[...]
> However, if I'm not mistaken that can't actually happen. If the conditional
> statement inside the loop never runs, Found will still be False and the
> second conditional will definitely execute. Index will receive a value either
> inside the loop or later.
>
> Am I missing something or is this reasoning outside of the abilities of
> SPARK's flow analysis? Is there some other idiomatic way I should be handling
> this sort of situation?

This is, really, outside what the Examiner does in flow analysis - it
doesn't look at the executability of paths when reporting flow errors.
(That's why the error says "... may be used ...".)

So there is a path through the flow graph of the procedure, even
though it can never be executed in practice.

One way to get rid of the error is to introduce a 'Local_Index' that
is set in the loop; then set Index to that value after the loop if
Found is True (and your existing code if False).

Alternatively, you can add an accept annotation for the error.

There shouldn't be any risk of the accept annotation allowing an error
through as, if there is a 'real' path through the code that doesn't
set Index then there should be an unprovable VC generated by the exit
run-time check VC for that path.  So the non-existence of an
unprovable VC supports the accept annotation.
(However I want to try this on some real code before making a firm
statement, Ill try that sometime soon.)

Cheers,

Phil

Re: Question about SPARK flow error.

[Gavino]

"Phil Thornley" <phil.jpthornley@gmail.com> wrote in message
news:fd3e54b4-bff0-470a-8409-f48c3289a2f3@x27g2000yqb.googlegroups.com...
> One way to get rid of the error is to introduce a 'Local_Index' that
> is set in the loop; then set Index to that value after the loop if
> Found is True (and your existing code if False).

Doesn't that just push the flow error onto Local_Index?
After all, the loop body itself may (in principle) never be executed.

Re: Question about SPARK flow error.

[Phil Thornley]

On 19 June, 19:23, "Gavino" <inva...@invalid.invalid> wrote:
> "Phil Thornley" <phil.jpthorn...@gmail.com> wrote in message
>
> news:fd3e54b4-bff0-470a-8409-f48c3289a2f3@x27g2000yqb.googlegroups.com...
>
> > One way to get rid of the error is to introduce a 'Local_Index' that
> > is set in the loop; then set Index to that value after the loop if
> > Found is True (and your existing code if False).
>
> Doesn't that just push the flow error onto Local_Index?
> After all, the loop body itself may (in principle) never be executed.

Ummm, yes, you're probably right :-(

(Just shows that I should have stuck to my normal policy of not
pronouncing on what the Examiner will do without checking it first on
real code).

Cheers,

Phil

Re: Question about SPARK flow error.

[Gavino]

"Peter C. Chapin" <pcc482719@gmail.com> wrote in message
news:4c1cf6a3$0$30803$4d3efbfe@news.sover.net...
> Am I missing something or is this reasoning outside of the abilities of
> SPARK's flow analysis? Is there some other idiomatic way I should be
handling
> this sort of situation?
Flow analysis is only concerned with syntactically possible paths through
the code and does not consider semantic aspects such as this.
For that level of analysis, you need to use the SPARK proof tools.

You could shut the Examiner up by initialising Index (eg to
Index_type'First), but it doesn't seem a satisfactory solution.

Re: Question about SPARK flow error.

[Phil Thornley]

On 19 June, 19:14, "Gavino" <inva...@invalid.invalid> wrote:
[...]
> You could shut the Examiner up by initialising Index (eg to
> Index_type'First), but it doesn't seem a satisfactory solution.

The problem with this solution (which Peter Amey always referred to as
a 'junk initialisation' - an excellent name) is that it can hide a
genuine data flow error if there really is a path that does not give
Index a value.

Cheers,

Phil

Re: Question about SPARK flow error.

[Phil Thornley]

On 19 June, 17:58, "Peter C. Chapin" <pcc482...@gmail.com> wrote:
[...]
Well, I was also wrong about using the non-existence of an unprovable
VC as evidence to support an accept annotation!

Using your code, the Simplifier proves all the VCs - and it still does
even if I remove either of the assignments to Index (and so create a
genuine data flow error).

The 'exit' VCs for a procedure are "trivially true" unless there is a
post-condition.  All exported values are assumed to be valid at this
point because the RTC analysis ***assumes that there are no data-flow
errors*** - i.e.:
1. all exports must have been assigned a value (otherwise there will
be a data-flow error), and
2. all values assigned must be valid otherwise there will be an
unprovable VC.

So it seems to me that:
The best way to deal with the error is an accept annotation.
Such an annotation is a potential risk as it may hide a genuine data
flow error (if not now then maybe when the code is changed at some
point in the future).

Consequently it makes sense to force a check on the relevant value by
adding a check annotation.

So, how about adding the following at the end of your procedure:
   --# accept F, 602, Index, Index,
   --#        "The following check ensures that there is no actual
error.";
   --# check Index in Index_Type;
end Add_Item;

This eliminates the reported flow error, and creates an unprovable VC
if there is any genuine data flow error for Index.
(It also needs a assertion in the loop: --# assert not Found;)

HTH

Phil

Re: Question about SPARK flow error.

[Peter C. Chapin]

Phil Thornley wrote:

> The best way to deal with the error is an accept annotation.
> Such an annotation is a potential risk as it may hide a genuine data
> flow error (if not now then maybe when the code is changed at some
> point in the future).

Thanks for the suggestion. It sounds reasonable. What I did (at least for now)
is more like a "junk initialization" although perhaps not complete junk. If
the item is not found then Index gets Next_Index. So I started the procedure
off with

        Index := Next_Index;

and removed that assignment from the condition when the item is not found. If
the item is found inside the loop, Index gets overridden by a different
value. Note that Next_Index is definitely initialized properly; my
annotations declare it as a global in out variable and I have an
initialization procedure (elsewhere) that sets it up.

I can see the danger to this... if I forgot to set Index inside the loop (or
if that assignment gets removed later) the Examiner won't notice the problem.
However, at least I can initialize Index to a semantically meaningful value.

Peter

Re: Question about SPARK flow error.

[Phil Thornley]

On 20 June, 01:37, "Peter C. Chapin" <pcc482...@gmail.com> wrote:
> Phil Thornley wrote:
> > The best way to deal with the error is an accept annotation.
> > Such an annotation is a potential risk as it may hide a genuine data
> > flow error (if not now then maybe when the code is changed at some
> > point in the future).
>
> Thanks for the suggestion. It sounds reasonable. What I did (at least for now)
> is more like a "junk initialization" although perhaps not complete junk. If
> the item is not found then Index gets Next_Index. So I started the procedure
> off with
>
>         Index := Next_Index;
>
> and removed that assignment from the condition when the item is not found. If
> the item is found inside the loop, Index gets overridden by a different
> value. Note that Next_Index is definitely initialized properly; my
> annotations declare it as a global in out variable and I have an
> initialization procedure (elsewhere) that sets it up.

That sounds like a reasonable solution in this case.

> I can see the danger to this... if I forgot to set Index inside the loop (or
> if that assignment gets removed later) the Examiner won't notice the problem.
> However, at least I can initialize Index to a semantically meaningful value.

I think that there is sometimes a tendency to expect more of the
Examiner than it can deliver - eliminating flow errors does not
guarantee correctness of the code, it just reduces the opportunities
for errors.

There may be some mileage in using check annotations to justify the
use of accept annotations for data flow errors - I'm going to think
about that one a little more.

Cheers,

Phil