Weird Bug in Get_Line

Weird Bug in Get_Line

[Brian Kolden]

I came across an interesting issue in the Get_Line function. When piping in a file (using the linux cammand '<') GNAT "raises ADA.IO_EXCEPTIONS.END_ERROR : a-tigeli.adb:96". 

However, the interesting issue is this only happens for a very small number of line lengths. I've noticed the exception is only thrown on lines with length 500, 501, 1000, 1001. Lines bigger or smaller don't seem to raise the issue, even other multiples of 500. This only is effected when using a file as input, copying and pasting the line into the terminal does not seem to trigger it.

So, is this an GNAT issue or an OS issue?


with Ada.Text_IO; use Ada.Text_IO;
procedure Test is
	type String_Pointer is access all String;
	S : String := Get_Line;
begin
	null;
end Test;

Re: Weird Bug in Get_Line

[Brian Drummond]

On Wed, 26 Apr 2017 00:38:55 -0700, Brian Kolden wrote:

> I came across an interesting issue in the Get_Line function. When piping
> in a file (using the linux cammand '<') GNAT "raises
> ADA.IO_EXCEPTIONS.END_ERROR : a-tigeli.adb:96".
> 
> However, the interesting issue is this only happens for a very small
> number of line lengths. I've noticed the exception is only thrown on
> lines with length 500, 501, 1000, 1001. Lines bigger or smaller don't
> seem to raise the issue, even other multiples of 500. This only is
> effected when using a file as input, copying and pasting the line into
> the terminal does not seem to trigger it.
> 
> So, is this an GNAT issue or an OS issue?
> 
> 
> with Ada.Text_IO; use Ada.Text_IO;
> procedure Test is
> 	type String_Pointer is access all String;
> 	S : String := Get_Line;
> begin
> 	null;
> end Test;

Which Gnat? Which Linux?

-- Brian

Re: Weird Bug in Get_Line

[Brian Kolden]

> Which Gnat? Which Linux?

GNAT 5.4.0 on Ubuntu 16.04
and confirmed on
GNAT 4.8 on Ubuntu 14.04

Re: Weird Bug in Get_Line

[Brian Kolden]

I forgot to mention the line has to be the very last line, otherwise there would be no EOF character to read. No newline character should be there, vim auto inserts one by default, for example. I was also able to trigger it on Redhat 5.11.0.9 running GNAT 4.1.2.

Re: Weird Bug in Get_Line

[Simon Wright]

Brian Kolden <bakolden5@gmail.com> writes:

> I came across an interesting issue in the Get_Line function. When
> piping in a file (using the linux cammand '<') GNAT "raises
> ADA.IO_EXCEPTIONS.END_ERROR : a-tigeli.adb:96".
>
> However, the interesting issue is this only happens for a very small
> number of line lengths. I've noticed the exception is only thrown on
> lines with length 500, 501, 1000, 1001. Lines bigger or smaller don't
> seem to raise the issue, even other multiples of 500. This only is
> effected when using a file as input, copying and pasting the line into
> the terminal does not seem to trigger it.
>
> So, is this an GNAT issue or an OS issue?

A GNAT issue, most likely.

Check out http://blog.adacore.com/formal-verification-of-legacy-code

Re: Weird Bug in Get_Line

[Jeffrey R. Carter]

On 04/26/2017 09:38 AM, Brian Kolden wrote:
> I came across an interesting issue in the Get_Line function. When piping in a
> file (using the linux cammand '<') GNAT "raises ADA.IO_EXCEPTIONS.END_ERROR :
> a-tigeli.adb:96".
>
> However, the interesting issue is this only happens for a very small number
> of line lengths. I've noticed the exception is only thrown on lines with
> length 500, 501, 1000, 1001. Lines bigger or smaller don't seem to raise the
> issue, even other multiples of 500. This only is effected when using a file
> as input, copying and pasting the line into the terminal does not seem to
> trigger it.

And also

> I forgot to mention the line has to be the very last line, otherwise there
> would be no EOF character to read. No newline character should be there, vim
> auto inserts one by default, for example. I was also able to trigger it on
> Redhat 5.11.0.9 running GNAT 4.1.2.

According to the ARM (A.10), Text_IO operates on "text files" as defined there. 
Part of that definition is that "the end of a line is marked by a _line 
terminator_" and "the end of a file is marked by the combination of a line 
terminator immediately followed by a page terminator and then a _file 
terminator_" [A.10(7)]. So technically, an implementation of Text_IO is not 
required to work on files that aren't valid Text_IO text files, and the error is 
that your file is not a valid Text_IO text file.

However, such an implementation of Text_IO is pretty useless on most systems, 
and compiler writers usually try hard to make sure that Text_IO works on foreign 
files. AdaCore certainly does. Still, if you produce files without a final line 
terminator, it's usually a good idea to find out why and fix that.

-- 
Jeff Carter
"Hold your temper. Count ten.... Now let 'er go.
You got a good aim."
Never Give a Sucker an Even Break
105

Re: Weird Bug in Get_Line

[Brian Kolden]

 
> According to the ARM (A.10), Text_IO operates on "text files" as defined there. 
> Part of that definition is that "the end of a line is marked by a _line 
> terminator_" and "the end of a file is marked by the combination of a line 
> terminator immediately followed by a page terminator and then a _file 
> terminator_" [A.10(7)]. So technically, an implementation of Text_IO is not 
> required to work on files that aren't valid Text_IO text files, and the error is 
> that your file is not a valid Text_IO text file.
> 
> However, such an implementation of Text_IO is pretty useless on most systems, 
> and compiler writers usually try hard to make sure that Text_IO works on foreign 
> files.

That's fair, however, the functionality of Text_IO is currently inconsistent. I feel that it should either be reworked to always throw the exception or not. At the moment, it comes across as a logical error since it will only complain at a few, very specific line lengths.

Re: Weird Bug in Get_Line

[Jeffrey R. Carter]

On 04/26/2017 09:32 PM, Brian Kolden wrote:
>
> That's fair, however, the functionality of Text_IO is currently inconsistent.
> I feel that it should either be reworked to always throw the exception or
> not. At the moment, it comes across as a logical error since it will only
> complain at a few, very specific line lengths.

What you've found is, as Wright pointed out, an error in GNAT's attempt to 
handle foreign files reasonably that has already been corrected, at least in the 
Pro version.

TBH, handling last lines without a line terminator as if they had a line 
terminator is not easy. Much thought was needed to get PragmARC.Text_IO, which 
handles Mac (CR), Unix (LF), and Windows (CR-LF) line terminators, to do it.

-- 
Jeff Carter
"Hold your temper. Count ten.... Now let 'er go.
You got a good aim."
Never Give a Sucker an Even Break
105

Re: Weird Bug in Get_Line

[moy]

On Wednesday, April 26, 2017 at 10:44:07 PM UTC+2, Jeffrey R. Carter wrote:

> What you've found is, as Wright pointed out, an error in GNAT's attempt to 
> handle foreign files reasonably that has already been corrected, at least in the 
> Pro version.

It has been fixed in early 2016 for the Pro version, and the fix was included in GNAT GPL 2016 issued last year. So 10 years later than the release date of GNAT 5.04 on which Brian reported the issue!

> TBH, handling last lines without a line terminator as if they had a line 
> terminator is not easy. Much thought was needed to get PragmARC.Text_IO, which 
> handles Mac (CR), Unix (LF), and Windows (CR-LF) line terminators, to do it.

The sublety of the code was the reason we went through formal verification, to make sure there were no more bugs in our implementation of Get_Line. And there were some. See the blog post Simon mentioned: http://blog.adacore.com/formal-verification-of-legacy-code