Ada.Strings.Fixed.Count raises Storage_Error

Ada.Strings.Fixed.Count raises Storage_Error

[Xavier Petit]

Hello, I would like to know if it is normal or a known bug.

function Count
   (Source  : String;
    Pattern : String;
    Mapping : Maps.Character_Mapping := Maps.Identity) return Natural;

When Source'Last = Positive'Last and Pattern'Length = 1, I get
Storage_Error, it seems this is because the checks are suppressed in
this GNAT runtime function ? So with checks it would result a
Constraint_Error ?

Internally, the exit condition is tested after the index incrementation, 
so in this specific case the “Ind” index tries to store Positive'Last + 
1. I think.

Here the code :

with Ada.Strings.Fixed, Ada.Integer_Text_IO;
use  Ada.Strings.Fixed, Ada.Integer_Text_IO;

procedure Test_Count is
    S : constant String (Positive'Last - 2 .. Positive'Last) := "Ada";
begin
    Put (Count (Source => S,                         Pattern => "AA"));
    Put (Count (Source => S (S'First .. S'Last - 1), Pattern => "A"));
    Put (Count (Source => S,                         Pattern => "A"));
end;

Output on gnat-gcc 5.3.1 :

           0          1

raised STORAGE_ERROR : stack overflow or erroneous memory access


Thanks by advance

-- 
Xavier Petit

Re: Ada.Strings.Fixed.Count raises Storage_Error

[Tero Koskinen]

Hi,

12.5.2016, 14.36, Xavier Petit wrote:
> Hello, I would like to know if it is normal or a known bug.
>
> function Count
>    (Source  : String;
>     Pattern : String;
>     Mapping : Maps.Character_Mapping := Maps.Identity) return Natural;
>
> When Source'Last = Positive'Last and Pattern'Length = 1, I get
> Storage_Error, it seems this is because the checks are suppressed in
> this GNAT runtime function ? So with checks it would result a
> Constraint_Error ?
...
>
> Here the code :
>
> with Ada.Strings.Fixed, Ada.Integer_Text_IO;
> use  Ada.Strings.Fixed, Ada.Integer_Text_IO;
>
> procedure Test_Count is
>     S : constant String (Positive'Last - 2 .. Positive'Last) := "Ada";
> begin
>     Put (Count (Source => S,                         Pattern => "AA"));
>     Put (Count (Source => S (S'First .. S'Last - 1), Pattern => "A"));
>     Put (Count (Source => S,                         Pattern => "A"));
> end;
>
> Output on gnat-gcc 5.3.1 :
>
>            0          1
>
> raised STORAGE_ERROR : stack overflow or erroneous memory access

When compiled with Janus/Ada the output is following:
C:\Work\xavier-fixed-count\obj> test_cou
      0     1     1
C:\Work\xavier-fixed-count\obj>

I would say that Janus/Ada is correct here and you have found a bug from 
GNAT.


>
> Thanks by advance
>

Yours,
  Tero

Re: Ada.Strings.Fixed.Count raises Storage_Error

[Georg Bauhaus]

On 12.05.16 13:36, Xavier Petit wrote:

> with Ada.Strings.Fixed, Ada.Integer_Text_IO;
> use  Ada.Strings.Fixed, Ada.Integer_Text_IO;
>
> procedure Test_Count is
>     S : constant String (Positive'Last - 2 .. Positive'Last) := "Ada";
> begin
>     Put (Count (Source => S,                         Pattern => "AA"));
>     Put (Count (Source => S (S'First .. S'Last - 1), Pattern => "A"));
>     Put (Count (Source => S,                         Pattern => "A"));
> end;
>
> Output on gnat-gcc 5.3.1 :
>
>            0          1
>
> raised STORAGE_ERROR : stack overflow or erroneous memory access

Compiling such that the RTS is recompiled will result in

raised CONSTRAINT_ERROR : a-strsea.adb:102 overflow check failed

The message points at a line in the implementation of
Ada.Strings.Search.Count, for the third of the calls. It reads

      Ind := Ind + 1;

where Ind looks seems to be go along with the Index of your S,
IINM. Effectively (PL1 = Pattern'Length - 1 being 0), then loop
there boils down to this:

    while Ind <= Source'Last loop
       if Pattern = Source (Ind .. Ind) then
          ...
       else
          Ind := Ind + 1;
       end if;
    end loop;

And this would explains the overflow.

Just the slip-up that Ada subtypes were designed to help prevent?


-- 
"HOTDOGS ARE NOT BOOKMARKS"
Springfield Elementary teaching staff

Re: Ada.Strings.Fixed.Count raises Storage_Error

[Victor Porton]

GNAT 6.1.1 on Debian Linux "testing":

$ ./test_count 
          0          1

raised STORAGE_ERROR : stack overflow or erroneous memory access

Let's decide who of us will report the bug, so that the report won't happen 
to be duplicate?

Georg Bauhaus wrote:
> On 12.05.16 13:36, Xavier Petit wrote:
> 
>> with Ada.Strings.Fixed, Ada.Integer_Text_IO;
>> use  Ada.Strings.Fixed, Ada.Integer_Text_IO;
>>
>> procedure Test_Count is
>>     S : constant String (Positive'Last - 2 .. Positive'Last) := "Ada";
>> begin
>>     Put (Count (Source => S,                         Pattern => "AA"));
>>     Put (Count (Source => S (S'First .. S'Last - 1), Pattern => "A"));
>>     Put (Count (Source => S,                         Pattern => "A"));
>> end;
>>
>> Output on gnat-gcc 5.3.1 :
>>
>>            0          1
>>
>> raised STORAGE_ERROR : stack overflow or erroneous memory access
> 
> Compiling such that the RTS is recompiled will result in
> 
> raised CONSTRAINT_ERROR : a-strsea.adb:102 overflow check failed
> 
> The message points at a line in the implementation of
> Ada.Strings.Search.Count, for the third of the calls. It reads
> 
>       Ind := Ind + 1;
> 
> where Ind looks seems to be go along with the Index of your S,
> IINM. Effectively (PL1 = Pattern'Length - 1 being 0), then loop
> there boils down to this:
> 
>     while Ind <= Source'Last loop
>        if Pattern = Source (Ind .. Ind) then
>           ...
>        else
>           Ind := Ind + 1;
>        end if;
>     end loop;
> 
> And this would explains the overflow.
> 
> Just the slip-up that Ada subtypes were designed to help prevent?
> 
> 
-- 
Victor Porton - http://portonvictor.org

Re: Ada.Strings.Fixed.Count raises Storage_Error

[rieachus]

On Sunday, June 26, 2016 at 5:18:49 PM UTC-4, Victor Porton wrote:
 
> Let's decide who of us will report the bug, so that the report won't happen 
> to be duplicate?

How about no one reports this non-existent error?  This is a category of problem that the ARG decided long ago should be considered pathologies.   The original case was a program that checked whether a task returned by a function was Terminated.  (The "correct" answer was True, but the program was totally useless for anything other than making compiler developers lives miserable.)

A string which ends at Integer'Last is either huge enough to raise Storage_Error anyway, or a clever compiler test that exists only to make compiler developers lives miserable.  I'm retired now, so I can say that without insulting customers.  And as Randy pointed out anything is allowed to raise Storage_Error.  That might not be user friendly, but in this case (Strings ending at Integer'Last) no sensible user is going to run into the problem.

Re: Ada.Strings.Fixed.Count raises Storage_Error

[Jeffrey R. Carter]

On 06/26/2016 04:23 PM, rieachus@comcast.net wrote:
> 
> How about no one reports this non-existent error?  This is a category of
> problem that the ARG decided long ago should be considered pathologies.   The
> original case was a program that checked whether a task returned by a
> function was Terminated.  (The "correct" answer was True, but the program was
> totally useless for anything other than making compiler developers lives
> miserable.)
> 
> A string which ends at Integer'Last is either huge enough to raise
> Storage_Error anyway, or a clever compiler test that exists only to make
> compiler developers lives miserable.  I'm retired now, so I can say that
> without insulting customers.  And as Randy pointed out anything is allowed to
> raise Storage_Error.  That might not be user friendly, but in this case
> (Strings ending at Integer'Last) no sensible user is going to run into the
> problem.

While I mostly agree, this one, given the code presented earlier, is a 1-line
change to correct, which hardly seems like it would make developers' lives
miserable:

    while Ind <= Source'Last loop
       if Pattern = Source (Ind .. Ind) then
          ...
       else
          Ind := Ind + 1;
       end if;
    end loop;

Add

exit when Ind = Integer'Last;

after "else". I see no reason this code shouldn't correctly handle this corner case.

-- 
Jeff Carter
"[T]he Musgroves had had the ill fortune
of a very troublesome, hopeless son, and
the good fortune to lose him before he
reached his twentieth year ..."
Persuasion
154

Re: Ada.Strings.Fixed.Count raises Storage_Error

[rieachus]

On Sunday, June 26, 2016 at 8:21:29 PM UTC-4, Jeffrey R. Carter wrote:
 
> While I mostly agree, this one, given the code presented earlier, is a 1-line
> change to correct, which hardly seems like it would make developers' lives
> miserable:
> 
>     while Ind <= Source'Last loop
>        if Pattern = Source (Ind .. Ind) then
>           ...
>        else
>           Ind := Ind + 1;
>        end if;
>     end loop;
> 
> Add
> 
> exit when Ind = Integer'Last;
> 
> after "else". I see no reason this code shouldn't correctly handle this corner case.

It is not a one-line change.  There is documentation, adding cases to regression test libraries, and finally the effort on the developer's part to fix this without producing significantly slower code.  How many times will that extra line be executed if the string is large, but does not end at Integer'Last?  This is extremely important since it is a branch in an innermost loop.  If I were responsible for fixing this I would hoist the case of strings with S'Last = Integer'Last up as high as possible, even if it required (almost) duplicating a lot of code.

This tradeoff between performance and corner cases has been made before.  Try writing a loop that runs from X to Y for some non-static values, then test the code when X = Integer'First and Y = Integer'Last.  You may want to print a period for each 100 million times around the loop...

Do the same thing for a large unsigned array with static bounds of U'First and and U'Last.  This case should work as expected.  Why?  Because looping over the entire range of an unsigned type is something that occurs often in radar, hash tables, and other cases. On a 64-bit machine it probably will not exit if you have the largest possible unsigned type, though I don't know how you could tell. (Even if you could do each interation in a nanosecond, that would take over 500 years...)

Re: Ada.Strings.Fixed.Count raises Storage_Error

[Xavier Petit]

I’m sorry, I thought that Ada was a perfect software tool built upon a 
vast, incoherent and inconsistent bloatware.

I realize that Ada has to make compromises and is far away from 
perfection. It’s just a more advanced programming language with the 
right goals. It produces less buggued software.

I agree with you that the string given in the example is too big, it’s 
the max size ! I encountered this error with a weird benchmark.

But following the principles and philosophy behind Ada I think that the 
behavior in the GNAT compiler should be either documented (to not have a 
string with Positive'Last length), either corrected, with for example 
the code proposed above by Jeffrey R. Carter.

Every parameters of a subprogram should be anticipated and produce a 
coherent behavior. It’s hard but Ada is especially here to make it easier.

-- 
Xavier Petit

Re: Ada.Strings.Fixed.Count raises Storage_Error

[rieachus]

On Sunday, June 26, 2016 at 8:51:21 PM UTC-4, Xavier Petit wrote:
 
> Every parameters of a subprogram should be anticipated and produce a 
> coherent behavior. It’s hard but Ada is especially here to make it easier.

Gödel, Escher, Bach: An Eternal Golden Braid, is a 1979 book by Douglas Hofstadter that is now in its 20th edition.

It tries, among other things to explain the reality revealed by Gödel's proofs.  One of those consequences is that you can't build a perfect compiler.  In fact, the gnat in Ada Core Technologies logo is a cute reminder that every compiler must have at least one bug.  Not, these things are so complex they can never be perfect, but even some very simple software tools are subject to Gödel's findings--no system above a rudimentary complexity (embedding of Peano arithmetic) can be bug-free.

Worse, the Halting Problem is a very simple proof that you cannot write a program that will perfectly determine whether a given software program will halt.  (Or not halt, if you work on embedded systems like I did.)

So trying for perfection in compilers, programming languages, and even many software programs is a mug's game.  You can't do it, you don't know where other corner cases are, and you can't even document all of the bugs.  Yes, it is possible to "prove" software correctness for some programs.  But for those same programs, you have just moved the target, from perfect software to perfect requirements.

The Airbus 320 had a major software bug in spite of the correctness proof tools used.  If a plane cross the last waypoint before the destination, the flight guidance system would put the airplane in the correct glidepath for the chosen runway as quickly as possible, even if that location was under a few thousand feet of granite.  Strasbourg suddenly dove straight down.  Oops! Perfect software implementation of a bad requirement. (https://www.flightglobal.com/news/articles/air-france-ceo-jean-cyril-spinetta-defends-rejection-of-gpws-equipment-on-air-inter-a320-fleet-despite-fatal-1992-st-odile-mountainside-crash-210280/ The obfuscation thrown about by Airbus and the French government still continues.  But at least the bug in "flight path angle mode" in the flight controller got fixed.  This list will show you why I still won't fly on an Airbus 310,20, or 21: https://en.wikipedia.org/wiki/Accidents_and_incidents_involving_the_Airbus_A320_family )  

Re: Ada.Strings.Fixed.Count raises Storage_Error

[Xavier Petit]

Le 27/06/2016 à 06:48, rieachus@comcast.net a écrit :
> On Sunday, June 26, 2016 at 8:51:21 PM UTC-4, Xavier Petit wrote:
>
>> Every parameters of a subprogram should be anticipated and produce a
>> coherent behavior. It’s hard but Ada is especially here to make it easier.
>
> Gödel, Escher, Bach: An Eternal Golden Braid, is a 1979 book by Douglas Hofstadter that is now in its 20th edition.
>
> It tries, among other things to explain the reality revealed by Gödel's proofs.  One of those consequences is that you can't build a perfect compiler.  In fact, the gnat in Ada Core Technologies logo is a cute reminder that every compiler must have at least one bug.  Not, these things are so complex they can never be perfect, but even some very simple software tools are subject to Gödel's findings--no system above a rudimentary complexity (embedding of Peano arithmetic) can be bug-free.
>
> Worse, the Halting Problem is a very simple proof that you cannot write a program that will perfectly determine whether a given software program will halt.  (Or not halt, if you work on embedded systems like I did.)
>
> So trying for perfection in compilers, programming languages, and even many software programs is a mug's game.  You can't do it, you don't know where other corner cases are, and you can't even document all of the bugs.  Yes, it is possible to "prove" software correctness for some programs.  But for those same programs, you have just moved the target, from perfect software to perfect requirements.
>
> The Airbus 320 had a major software bug in spite of the correctness proof tools used.  If a plane cross the last waypoint before the destination, the flight guidance system would put the airplane in the correct glidepath for the chosen runway as quickly as possible, even if that location was under a few thousand feet of granite.  Strasbourg suddenly dove straight down.  Oops! Perfect software implementation of a bad requirement. (https://www.flightglobal.com/news/articles/air-france-ceo-jean-cyril-spinetta-defends-rejection-of-gpws-equipment-on-air-inter-a320-fleet-despite-fatal-1992-st-odile-mountainside-crash-210280/ The obfuscation thrown about by Airbus and the French government still continues.  But at least the bug in "flight path angle mode" in the flight controller got fixed.  This list will show you why I still won't fly on an Airbus 310,20, or 21: https://en.wikipedia.org/wiki/Accidents_and_incidents_involving_the_Airbus_A320_family )
>
>

Thank you for the very interesting informations and explanations, I 
think I understand.

After tests, as you said the performance penalty is very important (from 
5 to 33% depending optimization options) if we do the test inside the loop.

But this is not only a special case, it’s a unique case, so the source 
code solution should be something like :

if Source'Last = Positive'Last and then Pattern'Length = 1 then
     return Boolean'Pos (Source (Source'Last) = Pattern (Pattern'First));
end if;

inserted between the empty pattern exception and the loops of Count.

A function “Count_Wrapper” that has the specification of 
Ada.Strings.Fixed.Count and code :

if Source'Last = Positive'Last and then Pattern'Length = 1 then
    return Boolean'Pos (Source (Source'Last) = Pattern (Pattern'First));
else
    return Ada.Strings.Fixed.Count (Source, Pattern, Mapping);
end if;

On intel64 & cortex A7 (raspberry pi 2), with(out) options, this 
function called with Ada.Command_Line.Argument (1) pattern and hundred 
millions of random size strings sources has no big overhead.

Do you think those unique and limit cases are worth a modification ?

-- 
Xavier Petit

Re: Ada.Strings.Fixed.Count raises Storage_Error

[Niklas Holsti]

On 16-06-27 07:48 , rieachus@comcast.net wrote:
> On Sunday, June 26, 2016 at 8:51:21 PM UTC-4, Xavier Petit wrote:
>
>> Every parameters of a subprogram should be anticipated and produce
>> a coherent behavior. It’s hard but Ada is especially here to make
>> it easier.
>
> Gödel, Escher, Bach: An Eternal Golden Braid, is a 1979 book by
> Douglas Hofstadter that is now in its 20th edition.
>
> It tries, among other things to explain the reality revealed by
> Gödel's proofs.  One of those consequences is that you can't build a
> perfect compiler.

That depends on what you mean by a "perfect" compiler. Please explain.

> In fact, the gnat in Ada Core Technologies logo is
> a cute reminder that every compiler must have at least one bug.

I do not believe that statement. It would mean that efforts to produce 
verified compilers, for example CompCert 
(http://compcert.inria.fr/index.html), are fundamentally misguided.

> Worse, the Halting Problem is a very simple proof that you cannot
> write a program that will perfectly determine whether a given
> software program will halt.  (Or not halt, if you work on embedded
> systems like I did.)

What has that do with the issue?

Yes, there is no algorithm that can determine if any given program halts 
or not.

Nevertheless, there are plenty of programs for which termination, or 
non-termination, can be proved and has been proved. And one of the 
skills required of a programmer is to write programs (compilers or 
applications) that terminate when required, or that keep running forever 
if that is required, and to present argument or proof that the program 
indeed has the desired behaviour.

> So trying for perfection in compilers, programming languages, and
> even many software programs is a mug's game.  You can't do it, you
> don't know where other corner cases are, and you can't even document
> all of the bugs.  Yes, it is possible to "prove" software correctness
> for some programs.  But for those same programs, you have just moved
> the target, from perfect software to perfect requirements.

Oh, that old argument. Yes, requirements are human creations, and 
therefore informal at source. Nevertheless, there are many methods to 
examine, review, verify, and validate requirements, both informal and 
formal ones. They are not perfect, but are often useful.

An analogous argument is that if a bridge is required to carry a load of 
100 tons, the engineers do not have to make any analysis to determine 
how thick the pillars should be, because perhaps the requirement is in 
error, and the real requirement is 80 tons, or 150 tons, or something 
else, so there is no point in trying to prove that the design will carry 
100 tons. Silly.

I'm astonished that you seem to be saying that Gödel's results mean that 
this clear and simple bug in a library function should not be reported 
to AdaCore. Really. Perhaps you are afraid that this is the last bug in 
GNAT, and as you believe that every compiler must have at least one bug, 
removing this bug would mean that GNAT would no longer be a compiler :-)

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .

Re: Ada.Strings.Fixed.Count raises Storage_Error

[Jeffrey R. Carter]

On 06/29/2016 11:49 AM, Niklas Holsti wrote:
> 
> I'm astonished that you seem to be saying that Gödel's results mean that this
> clear and simple bug in a library function should not be reported to AdaCore.
> Really. Perhaps you are afraid that this is the last bug in GNAT, and as you
> believe that every compiler must have at least one bug, removing this bug would
> mean that GNAT would no longer be a compiler :-)

This is not an error in the compiler; it's an error in a general-purpose
library. Fixing it will not change the number of errors in the compiler.

We're told that the ARG has decided that some corner cases are too difficult for
compiler writers to get right, so the ARG won't require that they be handled
correctly. The argument that this permission means the function in question
doesn't need to be correct is wrong because the error in question isn't
something the compiler has difficulty compiling. It's an error by the
implementor of the subprogram that the compiler compiles correctly.

The argument that correcting the error would have a negative effect on the
performance of the subprogram, and that it's more important that it be fast than
that it be correct is wrong because correctness is always more important than
performance for a general-purpose library. It's expected that a general-purpose
library's performance may not be acceptable for some applications. Such
applications know that a general-purpose library may not meet their performance
needs.

-- 
Jeff Carter
"What's the amount of the insult?"
Never Give a Sucker an Even Break
104

Re: Ada.Strings.Fixed.Count raises Storage_Error

[Dmitry A. Kazakov]

On 2016-06-29 20:49, Niklas Holsti wrote:

> I'm astonished that you seem to be saying that Gödel's results mean that
> this clear and simple bug in a library function should not be reported
> to AdaCore.

Goedel results don't apply to programs anyway, because you are not 
required to decide anything using the program at hand. You are free to 
use *another* program, so you can break out.

Nor the Halting problem does apply. For any program having a finite 
number of states, one clearly can decide in finite time with finite 
storage whether the program halts. The Halting problem arise only if you 
wanted to have *one* program to decide it for all programs. In 
connection to this let's observe the fact that tests are developed *new* 
for each testee.

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

Re: Ada.Strings.Fixed.Count raises Storage_Error

[rieachus]

On Wednesday, June 29, 2016 at 3:57:47 PM UTC-4, Dmitry A. Kazakov wrote:

> Goedel results don't apply to programs anyway, because you are not 
> required to decide anything using the program at hand. You are free to 
> use *another* program, so you can break out.

Sigh! Gödel proved not just that there are systems where some functions cannot be computed correctly, but that there are functions which cannot be computed correctly by any system.  There are systems which are not powerful enough to try to compute these functions, but those systems are very limited.  Regular expressions are an example of such a limited system, Ada compilers are not.
 
> Nor the Halting problem does apply. For any program having a finite 
> number of states, one clearly can decide in finite time with finite 
> storage whether the program halts.

Since when have Ada compilers dealt with only finite states?*  There are programming languages which do have such limits, but Fortran, PL/I, Ada, C++, and other general purpose programming languages are not among them.  It is nice to think you live inside a little box, but Ada compilers can (and do) deal with programs in chunks called compilation units, and programs can be extended over multiple physical processors, each of which can accept external files as input.

To be explicit, theorem proving systems are attempts to solve the halting problem.  You hope that your theorem prover will give a correct answer or give up, but the reality is that there are programs that are never handed to theorem provers because they will execute "forever" without finding an answer.

Ada 80 had a statement that compilers were expected to find a valid elaboration order, and if one did not exist, the program was illegal.  So I, tongue in cheek, wrote a program which was legal if--and only if--Format's Last Theorem was false.  Oops!  Rules were changed so that compilers can leave those edge cases until run-time, and for most programs compilers will find an elaboration order which does not need to check for elaboration errors.  (So now you can compile that program, and a theorem prover that can handle FLT can prove that it never halts, or maybe prove that it halts when your bignum package runs out of file storage. ;-)

* You may contend that your personal computer has a finite number of states, but well before you can finish enumerating them, you will upgrade the processor, memory, and/or disks (whether mechanical or solid state).  And then there are services like Drop Box which enable you to store data "in the cloud."  So the time when computers had a finite set of states is long past.  (Even Univac I, with 1000 words of memory, had ten tape drives, and an operator to mount new tapes when required.)

Re: Ada.Strings.Fixed.Count raises Storage_Error

[Dmitry A. Kazakov]

On 01/07/2016 13:48, rieachus@comcast.net wrote:
> On Wednesday, June 29, 2016 at 3:57:47 PM UTC-4, Dmitry A. Kazakov wrote:
>
>> Goedel results don't apply to programs anyway, because you are not
>> required to decide anything using the program at hand. You are free to
>> use *another* program, so you can break out.
>
> Sigh! Gödel proved not just that there are systems where some
> functions cannot be computed correctly, but that there are functions
> which cannot be computed correctly by any system.

No. Goedel incompleteness does not mean that. Incompleteness is not 
transitive. If A is not provable in the formal system S that alone does 
not require it to be unprovable in Q.

And, furthermore, completeness is not same as consistency (absence of 
paradoxes). Most of the statements are just not spellable in the formal 
system at hand. Nobody worries about that, after all, they were designed 
to prevent such statements to appear there. So, if the Liar's paradox 
were incomputable, who cares.

> There are systems
> which are not powerful enough to try to compute these functions,

This is irrelevant. The behavior attributed to the bug of String index 
range is clearly:

1. Well-defined
2. Computable
3. Provable using very weak apparatus

>> Nor the Halting problem does apply. For any program having a finite
>> number of states, one clearly can decide in finite time with finite
>> storage whether the program halts.
>
> Since when have Ada compilers dealt with only finite states?*

They clearly do. Each Ada compiler has the upper limit of the program 
size it is capable to compile. Both the compiler and its outcome have a 
finite number of states.

> * You may contend that your personal computer has a finite number of
> states, but well before you can finish enumerating them, you will
> upgrade the processor, memory, and/or disks (whether mechanical or solid
> state). And then there are services like Drop Box which enable you to
> store data "in the cloud." So the time when computers had a finite set
> of states is long past. (Even Univac I, with 1000 words of memory, had
> ten tape drives, and an operator to mount new tapes when required.)

It does not matter, because you were arguing about *theoretical* 
undecidability, not about *practical* one. Theoretically it is clearly 
decidable and provable. Practicality is a whole different matter.

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

Re: Ada.Strings.Fixed.Count raises Storage_Error

[Simon Wright]

rieachus@comcast.net writes:

> On Sunday, June 26, 2016 at 5:18:49 PM UTC-4, Victor Porton wrote:
>  
>> Let's decide who of us will report the bug, so that the report won't happen 
>> to be duplicate?
>
> How about no one reports this non-existent error?  This is a category
> of problem that the ARG decided long ago should be considered
> pathologies.  The original case was a program that checked whether a
> task returned by a function was Terminated.  (The "correct" answer was
> True, but the program was totally useless for anything other than
> making compiler developers lives miserable.)
>
> A string which ends at Integer'Last is either huge enough to raise
> Storage_Error anyway, or a clever compiler test that exists only to
> make compiler developers lives miserable.  I'm retired now, so I can
> say that without insulting customers.  And as Randy pointed out
> anything is allowed to raise Storage_Error.  That might not be user
> friendly, but in this case (Strings ending at Integer'Last) no
> sensible user is going to run into the problem.

Who knows, AdaCore recently reported (in their blog) an obscure
customer-reported problem in Text_IO which resulted in them doing a
formal analysis and finding 2 further bugs ... if that approach
continues, this obscure problem might get fixed.

Re: Ada.Strings.Fixed.Count raises Storage_Error

[Georg Bauhaus]

On 27.06.16 10:29, Simon Wright wrote:
> Who knows, AdaCore recently reported (in their blog) an obscure
> customer-reported problem in Text_IO which resulted in them doing a
> formal analysis and finding 2 further bugs ... if that approach
> continues, this obscure problem might get fixed.

This approach could lead to, at least, a statement of the
assumptions of the algorithm in question. Perhaps even
to a special case routine that doesn't make the "normal"
routine run unnecessarily slow by frequently testing
equality with Positive'Last.


-- 
"HOTDOGS ARE NOT BOOKMARKS"
Springfield Elementary teaching staff

Re: Ada.Strings.Fixed.Count raises Storage_Error

[Niklas Holsti]

On 16-06-27 02:23 , rieachus@comcast.net wrote:
> On Sunday, June 26, 2016 at 5:18:49 PM UTC-4, Victor Porton wrote:
>
>> Let's decide who of us will report the bug, so that the report
>> won't happen to be duplicate?
>
> How about no one reports this non-existent error?

There are IMO three bugs/errors here:

1. That AdaCore delivers a default RTS compiled with checks off, without 
having ensured (by CodePeer &c) that checks cannot fail. This bug is 
similar to AdaCore's original choice to have overflow checks disabled by 
default (as I understand it, they are now enabled by default) but is 
harder to work around for the average GNAT user. I understand that the 
motivation is performance, but Ada is about correctness and reliability, 
not about getting wrong answers quickly.

2. That an integer overflow manifests itself as a Storage_Error 
exception, which is misleading. However, an overflow with checks off is 
erroneous execution, I believe, so perhaps nothing can or should be done 
about this bug.

3. The coding error in the library function Ada.Strings.Fixed.Count, 
which is a very common and simple kind of error, and should surely be 
corrected.

> This is a category
> of problem that the ARG decided long ago should be considered
> pathologies.   The original case was a program that checked whether a
> task returned by a function was Terminated.

I don't see any connection between these problems. Can you give a 
reference for the "original case", an AI number perhaps?

> A string which ends at Integer'Last is either huge enough to raise
> Storage_Error anyway, or a clever compiler test that exists only to
> make compiler developers lives miserable.

Such strings can also occur in tests of application programs, to check 
that _their_ index arithmetic works without overflows. These test cases 
may even be required, and automatically generated, to cover boundary values.

Writing loop code so that the counter and index arithmetic cannot cause 
overflow should be normal practice for Ada programmers. If that makes us 
miserable, we should be doing something else. And today we even have 
tools like CodePeer that can find such mistakes by static analysis.

We make fun of C programs falling over when a coding error causes 
wrap-around in a loop counter, for example. We expect Ada to be better.

> And as Randy pointed out anything is allowed to raise Storage_Error.

That Storage_Error is raised here is surely not intentional, but an 
unexpected and misleading consequence of the erroneous behaviour of the 
library function.

> but in this case (Strings ending at Integer'Last) no
> sensible user is going to run into the problem.

There are sensible uses of such Strings.

If your position is that predefined library subprograms should not be 
expected to work for a String S with S'Last = Integer'Last, then it 
would have been a simple matter for the ARG to define String with an 
index subtype extending only to Integer'Last - 1.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .

Re: Ada.Strings.Fixed.Count raises Storage_Error

[J-P. Rosen]

Le 29/06/2016 à 10:15, Niklas Holsti a écrit :
>> This is a category
>> of problem that the ARG decided long ago should be considered
>> pathologies.   The original case was a program that checked whether a
>> task returned by a function was Terminated.
> 
> I don't see any connection between these problems. Can you give a
> reference for the "original case", an AI number perhaps?
It was an example of a "pathology", because this one was the first case
of a pathology in the language. It was discovered long before there were
AIs (1983 or 1984), and named after the poor guy who tripped on it
first: Rosen's Pathology.

-- 
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: Ada.Strings.Fixed.Count raises Storage_Error

[Niklas Holsti]

On 16-06-29 12:13 , J-P. Rosen wrote:
> Le 29/06/2016 à 10:15, Niklas Holsti a écrit :
>>> This is a category
>>> of problem that the ARG decided long ago should be considered
>>> pathologies.   The original case was a program that checked whether a
>>> task returned by a function was Terminated.
>>
>> I don't see any connection between these problems. Can you give a
>> reference for the "original case", an AI number perhaps?
> It was an example of a "pathology", because this one was the first case
> of a pathology in the language. It was discovered long before there were
> AIs (1983 or 1984), and named after the poor guy who tripped on it
> first: Rosen's Pathology.

Thanks for this information, Jean-Paul. According to your post in 
http://computer-programming-forum.com/44-ada/cdf3e22c34c4de36.htm, this 
"pathology" was present in Ada 83, but was cured in Ada 95: "It was 
related to a function returning a local  task object, which is no more 
allowed."

This suggests to me that the definition of Ada 83 was either ambiguous 
in this case, or required too much effort from the implementation for 
this feature compared to the benefits of the feature, and consequently 
the language was changed to eliminate the feature.

Thus, Rosen's pathology was not tolerated, which seems to be what Robert 
Eachus is suggesting, but eliminated.

The analogous elimination in this case (String with 'Last = 
Integer'Last) would be to change the language to define the index 
subtype of String to run from 1 to Integer'Last - 1. The alternative, to 
correct the library routine to work even in this case, seems better to me.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .

Re: Ada.Strings.Fixed.Count raises Storage_Error

[J-P. Rosen]

Le 29/06/2016 à 19:43, Niklas Holsti a écrit :
> Thanks for this information, Jean-Paul. According to your post in
> http://computer-programming-forum.com/44-ada/cdf3e22c34c4de36.htm, this
> "pathology" was present in Ada 83, but was cured in Ada 95: "It was
> related to a function returning a local  task object, which is no more
> allowed."
> 
> This suggests to me that the definition of Ada 83 was either ambiguous
> in this case, or required too much effort from the implementation for
> this feature compared to the benefits of the feature, and consequently
> the language was changed to eliminate the feature.
No, an unexpected consequence of other rules. The logical place to
return the space occupied by tasks (including the TCB) is when you leave
its master; however, a function (that returned a task type) could return
a local task as the return value; therefore, the identity of the task
could propagate outside of its master, implying some information had to
be kept, and no place to free it.

When I reported the problem to Ichbiah, he told me that this was a
problem for me, but that he was sure it would be no problem for his
compiler. I think he thought that this case could not be tested. But I
did write the test for it...

> Thus, Rosen's pathology was not tolerated, which seems to be what Robert
> Eachus is suggesting, but eliminated.
It was eliminated as a side effect of not allowing the return of a local
limited object.

> The analogous elimination in this case (String with 'Last =
> Integer'Last) would be to change the language to define the index
> subtype of String to run from 1 to Integer'Last - 1. The alternative, to
> correct the library routine to work even in this case, seems better to me.
> 
I don't think there is an analogy with this case. A string indexed up to
Integer'Last is a limit case, not a pathology. And with careful
programming, the cost of handling correctly limit cases is often minimal
(often overestimated until you measure it).

-- 
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: Ada.Strings.Fixed.Count raises Storage_Error

[Robert A Duff]

Niklas Holsti <niklas.holsti@tidorum.invalid> writes:

> Thanks for this information, Jean-Paul. 

Jean-Pierre.

> ...According to your post in
> http://computer-programming-forum.com/44-ada/cdf3e22c34c4de36.htm, this
> "pathology" was present in Ada 83, but was cured in Ada 95: "It was
> related to a function returning a local  task object, which is no more
> allowed."

Yes, but that was a bad design.  Ada 2005 fixed the problem in 
the right way.  It's unfortunate that we had  to introduce
incompatibilities along the way, instead of figuring out the right way
in the first place.

> This suggests to me that the definition of Ada 83 was either ambiguous
> in this case, ...

No, it was not ambiguous.  It might have surprised the language
designers, but the Ada 83 RM was clear: you could return a task
outside its master, and that task must be terminated by that time.

>...or required too much effort from the implementation for
> this feature compared to the benefits of the feature, ...

The benefits were exactly zero, so ANY implementation effort was "too
much".  But the real problem was that without heroic efforts,
implementations would be forced to leak memory.

I know of one Ada 83 implementation that counted the tasks as they were
terminated.  For the first 10, it did not free memory.  After that, it
did.  It just so happens that the ACVC test for this malfeature created
10 tasks, and made sure they still existed (in the terminated state)
after the function return.

>...and consequently
> the language was changed to eliminate the feature.

Yes, but the issue was bigger than just tasks.  Function return is
always by copy in Ada 83, and limited types (including those containing
tasks) should not be copied, but the RM required them to be copied
anyway.  Limited types didn't really work right until Ada 2005.

- Bob

Re: Ada.Strings.Fixed.Count raises Storage_Error

[Niklas Holsti]

On 16-06-29 23:30 , Robert A Duff wrote:
> Niklas Holsti <niklas.holsti@tidorum.invalid> writes:
>
>> Thanks for this information, Jean-Paul.
>
> Jean-Pierre.

My apologies to J-P. I blame a cosmic ray hitting a brain cell.

Regarding Rosen's pathology, your explanation shows that it was a severe 
one and really required a change in the language definition. A different 
kind of thing than the possible problems of Strings extending to 
Integer'Last.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .

Re: Ada.Strings.Fixed.Count raises Storage_Error

[rieachus]

On Thursday, June 30, 2016 at 1:38:50 AM UTC-4, Niklas Holsti wrote:

> Regarding Rosen's pathology, your explanation shows that it was a severe 
> one and really required a change in the language definition. A different 
> kind of thing than the possible problems of Strings extending to 
> Integer'Last.

No it is not.  There was a huge amount of wrangling about the consequences of the type Integer being 16-bits in size in Ada 83.  The classic issue was that code for loops generated normally would never terminate for a loop over Integer'Range.  (Strings were fine because they began at +1.)

Over the next few years, it became common for even Ada compilers for 16-bit word size systems to support a 32-bit Integer type. Then came machines with 64-bit integer registers and operations, and now, RM 3.5.4(11), Integer is a constrained subtype, and 64-bit registers can be used to count Integer loops without a problem.  But the problem does come back for 64-bit or 128-bit or whatever types.  No one is going to write a test which would outlast the physical machine, so we can ignore the issue--sort of.  You can go write a loop that runs from System.Min_Int .. System.Max_Int and inspect the code generated to see if it is correct.

I consider this issue to be a subcase of this pathology.  On machines with 64-bit registers and a 32-bit Integer type, the generated code should be fine.

Re: Ada.Strings.Fixed.Count raises Storage_Error

[J-P. Rosen]

Le 01/07/2016 à 12:40, rieachus@comcast.net a écrit :
> No it is not.  There was a huge amount of wrangling about the
> consequences of the type Integer being 16-bits in size in Ada 83.
> The classic issue was that code for loops generated normally would
> never terminate for a loop over Integer'Range.  (Strings were fine
> because they began at +1.)

I don't remember anything like that. And there is no problem for
generating correct code for a loop that spans over all values of a type,
you just have to exit in the middle - without efficiency penalty.
-- 
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: Ada.Strings.Fixed.Count raises Storage_Error

[rieachus]

On Friday, July 1, 2016 at 6:55:50 AM UTC-4, J-P. Rosen wrote:

> I don't remember anything like that.

Different hat. (Management)  When Ada (80) was new, it was just assumed that minicomputers and PCs would have a 16-bit Integer type.  Then it turned out that Ada compilers couldn't really fit in a machine with too limited an address space.  So those of us who worked for hardware companies had to do the soul searching about which hardware compilers needed to run on, and which targets could be included.  The choice between 16-bit and 32-bit Integer types was possibly just a symptom, but by 1984 it was pretty much in the rear view mirror.  No one really wanted to buy compilers where Integer was 16-bits, even for the (MIL STD) 1750A.
 
>                                       And there is no problem for
> generating correct code for a loop that spans over all values of a type,
> you just have to exit in the middle - without efficiency penalty.

You have a different definition of efficiency than I do.  On a modern processor I want to be able to execute tight loops in one clock cycle per iteration.  This usually requires three or more instructions that can be executed in parallel.  The efficient workaround is to have a single loop iteration before the actual loop code.  The better way is just to run the loop in a 64-bit register if that is an option. ;-)

Re: Ada.Strings.Fixed.Count raises Storage_Error

[G.B.]

On 01.07.16 14:17, rieachus@comcast.net wrote:
> The better way is just to run the loop in a 64-bit register if that is an option.;-)

GNAT's implementation of containers (as started by Matt Heaney)
had the index subtypes have just one more value than elements
that could be stored. Maybe that's another sign of the multi-
paradigm language Ada ;-)

Re: Ada.Strings.Fixed.Count raises Storage_Error

[Victor Porton]

I've reported the bug:

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=71674

Victor Porton wrote:
> GNAT 6.1.1 on Debian Linux "testing":
> 
> $ ./test_count
>           0          1
> 
> raised STORAGE_ERROR : stack overflow or erroneous memory access
> 
> Let's decide who of us will report the bug, so that the report won't
> happen to be duplicate?
> 
> Georg Bauhaus wrote:
>> On 12.05.16 13:36, Xavier Petit wrote:
>> 
>>> with Ada.Strings.Fixed, Ada.Integer_Text_IO;
>>> use  Ada.Strings.Fixed, Ada.Integer_Text_IO;
>>>
>>> procedure Test_Count is
>>>     S : constant String (Positive'Last - 2 .. Positive'Last) := "Ada";
>>> begin
>>>     Put (Count (Source => S,                         Pattern => "AA"));
>>>     Put (Count (Source => S (S'First .. S'Last - 1), Pattern => "A"));
>>>     Put (Count (Source => S,                         Pattern => "A"));
>>> end;
>>>
>>> Output on gnat-gcc 5.3.1 :
>>>
>>>            0          1
>>>
>>> raised STORAGE_ERROR : stack overflow or erroneous memory access
>> 
>> Compiling such that the RTS is recompiled will result in
>> 
>> raised CONSTRAINT_ERROR : a-strsea.adb:102 overflow check failed
>> 
>> The message points at a line in the implementation of
>> Ada.Strings.Search.Count, for the third of the calls. It reads
>> 
>>       Ind := Ind + 1;
>> 
>> where Ind looks seems to be go along with the Index of your S,
>> IINM. Effectively (PL1 = Pattern'Length - 1 being 0), then loop
>> there boils down to this:
>> 
>>     while Ind <= Source'Last loop
>>        if Pattern = Source (Ind .. Ind) then
>>           ...
>>        else
>>           Ind := Ind + 1;
>>        end if;
>>     end loop;
>> 
>> And this would explains the overflow.
>> 
>> Just the slip-up that Ada subtypes were designed to help prevent?
>> 
>> 
-- 
Victor Porton - http://portonvictor.org

Re: Ada.Strings.Fixed.Count raises Storage_Error

[Randy Brukardt]

Well, *anything* in Ada is allowed to raise Storage_Error (even the null 
statement!), so formally the behavior is correct.

OTOH, there doesn't seem to be any actual running out of memory here, so it 
is most likely a bug (especially as the other responses suggest that the 
main problem is that the checks are suppressed in the library code). And 
it's unlikely that the implementer expected this code to raise 
Storage_Error.

                            Randy.

"Xavier Petit" <xpetit@becoast.fr> wrote in message 
news:57346ac8$0$4570$426a74cc@news.free.fr...
> Hello, I would like to know if it is normal or a known bug.
>
> function Count
>   (Source  : String;
>    Pattern : String;
>    Mapping : Maps.Character_Mapping := Maps.Identity) return Natural;
>
> When Source'Last = Positive'Last and Pattern'Length = 1, I get
> Storage_Error, it seems this is because the checks are suppressed in
> this GNAT runtime function ? So with checks it would result a
> Constraint_Error ?
>
> Internally, the exit condition is tested after the index incrementation, 
> so in this specific case the "Ind" index tries to store Positive'Last + 1. 
> I think.
>
> Here the code :
>
> with Ada.Strings.Fixed, Ada.Integer_Text_IO;
> use  Ada.Strings.Fixed, Ada.Integer_Text_IO;
>
> procedure Test_Count is
>    S : constant String (Positive'Last - 2 .. Positive'Last) := "Ada";
> begin
>    Put (Count (Source => S,                         Pattern => "AA"));
>    Put (Count (Source => S (S'First .. S'Last - 1), Pattern => "A"));
>    Put (Count (Source => S,                         Pattern => "A"));
> end;
>
> Output on gnat-gcc 5.3.1 :
>
>           0          1
>
> raised STORAGE_ERROR : stack overflow or erroneous memory access
>
>
> Thanks by advance
>
> -- 
> Xavier Petit