GNAT.Serial_Communication and Streams

GNAT.Serial_Communication and Streams

[rrr.eee.27]

I want to send text strings via a serial line (actually, it is a USB device that presents itself as a serial CDC device).

For sending text snippets I had to declare the following routine:

   procedure Send_Command (Cmd : String)
   is
      Output_Max_Length : constant Ada.Streams.Stream_Element_Offset := 50;
      Output : Ada.Streams.Stream_Element_Array (1 .. Output_Max_Length);
   begin
      for I in 1 .. Cmd'Length loop
         Output (Ada.Streams.Stream_Element_Offset(I)) := Character'Pos(Cmd (Cmd'First + I - 1));
      end loop;
      Output (Cmd'Length+1) := Character'Pos(ASCII.LF);
      GNAT.Serial_Communication.Write (P, Output(1..Cmd'Length+1));
   end Send_Command;


That works but feels completely strange to me. I'm sure that I'm missing something here. There must be an easier way to fill the output buffer with a standard string.

RE

Re: GNAT.Serial_Communication and Streams

[Simon Wright]

rrr.eee.27@gmail.com writes:

> I want to send text strings via a serial line (actually, it is a USB
> device that presents itself as a serial CDC device).
>
> For sending text snippets I had to declare the following routine:
>
>    procedure Send_Command (Cmd : String)
>    is
>       Output_Max_Length : constant Ada.Streams.Stream_Element_Offset := 50;
>       Output : Ada.Streams.Stream_Element_Array (1 .. Output_Max_Length);
>    begin
>       for I in 1 .. Cmd'Length loop
>          Output (Ada.Streams.Stream_Element_Offset(I)) := Character'Pos(Cmd (Cmd'First + I - 1));
>       end loop;
>       Output (Cmd'Length+1) := Character'Pos(ASCII.LF);
>       GNAT.Serial_Communication.Write (P, Output(1..Cmd'Length+1));
>    end Send_Command;
>
>
> That works but feels completely strange to me. I'm sure that I'm
> missing something here. There must be an easier way to fill the output
> buffer with a standard string.

The clue is that

   type Serial_Port is new Ada.Streams.Root_Stream_Type with private;

which means that you aren't supposed to use the local Read/Write; they
are for the implementation of the 'Read/'Write type attributes (ARM
13.3.2),

   String'Write (P'Access, Cmd & ASCII.LF);

BTW, you should probably have declared

   Output : Ada.Streams.Stream_Element_Array (1 .. Cmd'Length + 1);

avoiding the need for Output_Max_Length.

Re: GNAT.Serial_Communication and Streams

[Jeffrey R. Carter]

On 11/22/2015 02:40 PM, rrr.eee.27@gmail.com wrote:
>    procedure Send_Command (Cmd : String)
>    is
>       Output_Max_Length : constant Ada.Streams.Stream_Element_Offset := 50;
>       Output : Ada.Streams.Stream_Element_Array (1 .. Output_Max_Length);
>    begin
>       for I in 1 .. Cmd'Length loop
>          Output (Ada.Streams.Stream_Element_Offset(I)) := Character'Pos(Cmd (Cmd'First + I - 1));
>       end loop;
>       Output (Cmd'Length+1) := Character'Pos(ASCII.LF);

What happens when Cmd'Length > 49?

>       GNAT.Serial_Communication.Write (P, Output(1..Cmd'Length+1));
>    end Send_Command;
> 
> 
> That works but feels completely strange to me. I'm sure that I'm missing something here. There must be an easier way to fill the output buffer with a standard string.

What about

procedure Send (Cmd : in String) is
   Local  : constant String := Cmd & Ada.Characters.Latin_1.LF;
   Output : constant Ada.Streams.Stream_Element_Array (1 .. Local'Length);
   pragma Import (Ada, Output);
   for Output'Address use Local'Address;
begin -- Send
   GNAT.Serial_Communication.Write (P, Output)?
end Send;

?

-- 
Jeff Carter
"When danger reared its ugly head, he bravely
turned his tail and fled."
Monty Python and the Holy Grail
60

Re: GNAT.Serial_Communication and Streams

[Randy Brukardt]

"Jeffrey R. Carter" <spam.jrcarter.not@spam.not.acm.org> wrote in message 
news:n2tddf$eue$1@dont-email.me...
...
> What about
>
> procedure Send (Cmd : in String) is
>   Local  : constant String := Cmd & Ada.Characters.Latin_1.LF;
>   Output : constant Ada.Streams.Stream_Element_Array (1 .. Local'Length);
>   pragma Import (Ada, Output);
>   for Output'Address use Local'Address;
> begin -- Send
>   GNAT.Serial_Communication.Write (P, Output)?
> end Send;
>
> ?

Probably works on GNAT, but it's not portable Ada code. For one thing, it 
assumes that Implementation Advice 13.3(14) is followed (Janus/Ada does not 
follow that advice - after all, it is just advice, not a requirement). It 
also assumes that Local is not optimized at all (there is advice that Output 
not be optimized, but that doesn't apply to Local, and like all advice, it 
can be ignored).

Might not matter in this case (which is clearly GNAT-specific), but 
generally this is a pattern to avoid.

                     Randy.

Re: GNAT.Serial_Communication and Streams

[Dmitry A. Kazakov]

On Sun, 22 Nov 2015 14:54:04 -0700, Jeffrey R. Carter wrote:

> What about
> 
> procedure Send (Cmd : in String) is
>    Local  : constant String := Cmd & Ada.Characters.Latin_1.LF;
>    Output : constant Ada.Streams.Stream_Element_Array (1 .. Local'Length);
>    pragma Import (Ada, Output);
>    for Output'Address use Local'Address;
> begin -- Send
>    GNAT.Serial_Communication.Write (P, Output)?
> end Send;

If you wanted optimize it, then Cmd and LF should be written in separate
calls rather than making a local copies.

A case when a copying makes sense is in a packet-oriented protocol. Which
is not the case here since streams are used. Maybe it is still
packet-oriented because of the USB device class, but then interfacing it
through a stream is inappropriate.

P.S. I don't see anything wrong with the original code. Stream attributes
not to be trusted in general. An explicit conversion is clearer and
cleaner, IMO.

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

Re: GNAT.Serial_Communication and Streams

[Simon Wright]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

> I don't see anything wrong with the original code. Stream attributes
> not to be trusted in general. An explicit conversion is clearer and
> cleaner, IMO.

GNAT used to write strings to streams character-by-character, which is
seriously non-optimal (practically; if an exception occurs, who cares on
which character it happened?!)

But if you can't trust your compiler to write a string to a stream, what
can you trust it to do?

I wholly agree with "trust, but verify", though!

Re: GNAT.Serial_Communication and Streams

[Dmitry A. Kazakov]

On Tue, 24 Nov 2015 10:28:20 +0000, Simon Wright wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> I don't see anything wrong with the original code. Stream attributes
>> not to be trusted in general. An explicit conversion is clearer and
>> cleaner, IMO.
> 
> GNAT used to write strings to streams character-by-character, which is
> seriously non-optimal (practically; if an exception occurs, who cares on
> which character it happened?!)

(Well, I/O errors cannot be recovered from anyway. So an exception in the
middle is not that big problem)

> But if you can't trust your compiler to write a string to a stream, what
> can you trust it to do?

Everything else. Stream attributes are not required to be portable or work
in a certain way. That makes them no-no for all I/O, except memory and
files never moved across the OS boundary.

If an attribute should be used then always overridden with a trusted
implementation.

Of course there are shades of trust. Character'Write is expected to be fine
almost anywhere. Integer'Write is expected to be patently wrong.

> I wholly agree with "trust, but verify", though!

You can verify given compiler for given machine. You cannot do that in
general.

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

Re: GNAT.Serial_Communication and Streams

[Jeffrey R. Carter]

On 11/23/2015 06:29 PM, Randy Brukardt wrote:
> 
> Probably works on GNAT, but it's not portable Ada code. For one thing, it 
> assumes that Implementation Advice 13.3(14) is followed (Janus/Ada does not 
> follow that advice - after all, it is just advice, not a requirement). It 
> also assumes that Local is not optimized at all (there is advice that Output 
> not be optimized, but that doesn't apply to Local, and like all advice, it 
> can be ignored).
> 
> Might not matter in this case (which is clearly GNAT-specific), but 
> generally this is a pattern to avoid.

I agree, but since the OP was clearly writing GNAT-specific code, I saw no
problem with giving GNAT-specific advice.

-- 
Jeff Carter
"Now look, Col. Batguano, if that really is your name."
Dr. Strangelove
31

Re: GNAT.Serial_Communication and Streams

[Shark8]

On Tuesday, November 24, 2015 at 3:45:52 AM UTC-7, Dmitry A. Kazakov wrote:
> On Tue, 24 Nov 2015 10:28:20 +0000, Simon Wright wrote:
> > I wholly agree with "trust, but verify", though!
> 
> You can verify given compiler for given machine. You cannot do that in
> general.

Whyever not?
Let us suppose that the compiler is represented by a function F(Text) -> Object;
furthermore, let F be a compositional function such that:
function FE(text) -> token_stream
function CP(token_stream) -> intermediate_form
function BE(intermediate_form) -> Object
and
function F = BE(CP(FE))

Now, obviously we can have the front-end take the text (be it in ASCII, EBDIC, or one of the UTF formats) and produce tokens which are a record of [Token_ID, Lexeme] where Lexeme is a standard textual form (let's say UTF32-BE). Now obviously we could split this so that FE = Encode_UTF(Decode_Particular(File)) -- this is to say that, conceptually, the front-end (FE) will only receive the proper UTF32-BE regardless of the particular encoding... nothing here should be dependent on the underlying architecture.

Let us now consider CP*, here we have a function taking a stream of tokens and returning the proper IR; obviously this could be verified and also should be independent of the underlying architecture.

Finally, considering the back-end (BE) we have essentially the same problem as the above CP, with the addition that the execution of the result is correct. So it seems the only possible break in applying verification is the HW/BE divide, that the emitted code /does/ what it is supposed to do, but given that HW manufacturers have used formal methods verification to prove the HW (for some HW), it is certainly possible on the HW level as well.

Going back to the idea of Forth, where every word (Forth's name for function) is defined as a either a list of words or some (usually very small) machine-code to be executed we could define a minimal set of words and implement the rest of Forth's standard dictionary in them --which means that to port the entire [verified] compiler we'd just have to rewrite the aforementioned words, and feed the compiler's source to itself-- this reduces our machine-dependent verification-burden to only the instructions used in that small set of words that all the other words are written in.

So, hooking the idea of having verified IR emition, if we use Forth as our IR then [once the entire compiler is verified] so long as we've verified the instructions used in our minimal dictionary on our new target we have a verified compiler.

Sure it's a lot of work, but I see no reason to consider it impossible.




* -- Arguably CP is the 'heart' of the compiler and can itself be viewed as a series of transformations; and it itself can conceptually be broken down into a aeries of transformations.

Re: GNAT.Serial_Communication and Streams

[Simon Wright]

Shark8 <onewingedshark@gmail.com> writes:

> On Tuesday, November 24, 2015 at 3:45:52 AM UTC-7, Dmitry A. Kazakov wrote:
>> On Tue, 24 Nov 2015 10:28:20 +0000, Simon Wright wrote:
>> > I wholly agree with "trust, but verify", though!
>> 
>> You can verify given compiler for given machine. You cannot do that
>> in general.
>
> Whyever not?

You might be able to do it for some ideal compiler, but I'd be mightily
impressed if someone managed it for GCC.

Anyway, if someone wanted to use GNAT's streams for an Atmel SAM3X-based
system, they'd want to check them out on _that_ platform, and they
wouldn't care whether they worked on PowerPC (we used an XDR version of
GNAT's stream attributes for communication between PowerPC and x86 with
no problems. But I have to say it was for recording for analysis rather
than for anything immediately mission-critical!)

Re: GNAT.Serial_Communication and Streams

[Dmitry A. Kazakov]

On Tue, 24 Nov 2015 22:24:48 -0800 (PST), Shark8 wrote:

> On Tuesday, November 24, 2015 at 3:45:52 AM UTC-7, Dmitry A. Kazakov wrote:
>> On Tue, 24 Nov 2015 10:28:20 +0000, Simon Wright wrote:
>>> I wholly agree with "trust, but verify", though!
>> 
>> You can verify given compiler for given machine. You cannot do that in
>> general.
> 
> Whyever not?

Because you need a compiler to verify things it does. A portable program is
a program exposing the same behavior for a set of compilers some of which
may not yet exist. Same applies to the target machines.

[ skipping compiler validation techniques ]

You can validate compilers only against mandated behavior. Stream attribute
to produce same sequences of stream elements across all Ada compilers is
just not required.

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

Re: GNAT.Serial_Communication and Streams

[Shark8]

On Wednesday, November 25, 2015 at 1:52:46 AM UTC-7, Dmitry A. Kazakov wrote:
> 
> You can validate compilers only against mandated behavior. Stream attribute
> to produce same sequences of stream elements across all Ada compilers is
> just not required.

That's rather irrelevant: that Stream'Input is allowed to have an implementation-defined representation for its stream is immaterial to your claim that the compiler cannot be verified [as correct, via proof] in-general. It's along the same lines as someone saying that a program which is never run cannot be proven correct, an obvious fallacy.

That there might be errors in the compiler, or that the language might not otherwise exist, are not germane to the actual proof. Neither do alternate representations necessarily invalidate the compiler... or are you going to claim that e.g. a one's-complement computer cannot have a verified Ada compiler because internally the [internal] representation of the integers would be different?

Re: GNAT.Serial_Communication and Streams

[Dmitry A. Kazakov]

On Wed, 25 Nov 2015 04:45:38 -0800 (PST), Shark8 wrote:

> On Wednesday, November 25, 2015 at 1:52:46 AM UTC-7, Dmitry A. Kazakov wrote:
>> 
>> You can validate compilers only against mandated behavior. Stream attribute
>> to produce same sequences of stream elements across all Ada compilers is
>> just not required.
> 
> That's rather irrelevant: that Stream'Input is allowed to have an
> implementation-defined representation for its stream is immaterial to your
> claim that the compiler cannot be verified

This immediately follows from being "implementation-defined."
Implementation-defined = [forall] not defined.

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

Re: GNAT.Serial_Communication and Streams

[Shark8]

On Wednesday, November 25, 2015 at 10:43:27 AM UTC-7, Dmitry A. Kazakov wrote:
> This immediately follows from being "implementation-defined."
> Implementation-defined = [forall] not defined.

Ridiculous.
Just because the standard makes [e.g.] the Address type implementation defined does not mean that the Address type has no definition, or that absolutely any possible implementation conforms to all requirements. For example the actual range of Standard.Integer is implementation defined, but it cannot be 0..255 because that would not meet the minimum range requirements for Standard.Integer.

Re: GNAT.Serial_Communication and Streams

[Dmitry A. Kazakov]

On Sun, 29 Nov 2015 00:45:22 -0800 (PST), Shark8 wrote:

> On Wednesday, November 25, 2015 at 10:43:27 AM UTC-7, Dmitry A. Kazakov wrote:
>> This immediately follows from being "implementation-defined."
>> Implementation-defined = [forall] not defined.
> 
> Ridiculous.

Ridiculous statements have ridiculous consequences...

> Just because the standard makes [e.g.] the Address type implementation
> defined does not mean that the Address type has no definition,

It means exactly this. You confuse two things:

A. definition given by the standard

B. definition given by an implementation of the standard

B must be conformant to A [B => A]. The reverse is wrong [not (B <= A)]

> or that absolutely any possible implementation conforms to all requirements.

Why absolute? Only the variation of legal implementations which would make
a portable implementation of some given requirement impossible.

For example, you cannot have a requirement for Address to accommodate 3GB
address space. That does *not* follow from ARM.

So, if you need your program to satisfy this requirement and be portable,
you will have to implement your own Address type.

Similarly, if the requirement is to have portable stream I/O, you must
override stream attributes. Just so.

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

Re: GNAT.Serial_Communication and Streams

[Simon Wright]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

> Similarly, if the requirement is to have portable stream I/O, you must
> override stream attributes. Just so.

With GNAT on both sides, you would stand a pretty good chance of
portable stream IO by replacing s-stratt.adb by s-stratt-xdr.adb and
rebuilding the library (it used to be that the gnatmake -a flag would do
this, but gprbuild doesn't have that option).