* GNAT.Serial_Communication and Streams @ 2015-11-22 21:40 rrr.eee.27 2015-11-22 21:52 ` Simon Wright 2015-11-22 21:54 ` Jeffrey R. Carter 0 siblings, 2 replies; 16+ messages in thread From: rrr.eee.27 @ 2015-11-22 21:40 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: GNAT.Serial_Communication and Streams 2015-11-22 21:40 GNAT.Serial_Communication and Streams rrr.eee.27 @ 2015-11-22 21:52 ` Simon Wright 2015-11-22 21:54 ` Jeffrey R. Carter 1 sibling, 0 replies; 16+ messages in thread From: Simon Wright @ 2015-11-22 21:52 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: GNAT.Serial_Communication and Streams 2015-11-22 21:40 GNAT.Serial_Communication and Streams rrr.eee.27 2015-11-22 21:52 ` Simon Wright @ 2015-11-22 21:54 ` Jeffrey R. Carter 2015-11-24 1:29 ` Randy Brukardt 2015-11-24 8:28 ` Dmitry A. Kazakov 1 sibling, 2 replies; 16+ messages in thread From: Jeffrey R. Carter @ 2015-11-22 21:54 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: GNAT.Serial_Communication and Streams 2015-11-22 21:54 ` Jeffrey R. Carter @ 2015-11-24 1:29 ` Randy Brukardt 2015-11-24 16:09 ` Jeffrey R. Carter 2015-11-24 8:28 ` Dmitry A. Kazakov 1 sibling, 1 reply; 16+ messages in thread From: Randy Brukardt @ 2015-11-24 1:29 UTC (permalink / raw) "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. ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: GNAT.Serial_Communication and Streams 2015-11-24 1:29 ` Randy Brukardt @ 2015-11-24 16:09 ` Jeffrey R. Carter 0 siblings, 0 replies; 16+ messages in thread From: Jeffrey R. Carter @ 2015-11-24 16:09 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: GNAT.Serial_Communication and Streams 2015-11-22 21:54 ` Jeffrey R. Carter 2015-11-24 1:29 ` Randy Brukardt @ 2015-11-24 8:28 ` Dmitry A. Kazakov 2015-11-24 10:28 ` Simon Wright 1 sibling, 1 reply; 16+ messages in thread From: Dmitry A. Kazakov @ 2015-11-24 8:28 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: GNAT.Serial_Communication and Streams 2015-11-24 8:28 ` Dmitry A. Kazakov @ 2015-11-24 10:28 ` Simon Wright 2015-11-24 10:45 ` Dmitry A. Kazakov 0 siblings, 1 reply; 16+ messages in thread From: Simon Wright @ 2015-11-24 10:28 UTC (permalink / raw) "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! ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: GNAT.Serial_Communication and Streams 2015-11-24 10:28 ` Simon Wright @ 2015-11-24 10:45 ` Dmitry A. Kazakov 2015-11-25 6:24 ` Shark8 0 siblings, 1 reply; 16+ messages in thread From: Dmitry A. Kazakov @ 2015-11-24 10:45 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: GNAT.Serial_Communication and Streams 2015-11-24 10:45 ` Dmitry A. Kazakov @ 2015-11-25 6:24 ` Shark8 2015-11-25 8:07 ` Simon Wright 2015-11-25 8:52 ` Dmitry A. Kazakov 0 siblings, 2 replies; 16+ messages in thread From: Shark8 @ 2015-11-25 6:24 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: GNAT.Serial_Communication and Streams 2015-11-25 6:24 ` Shark8 @ 2015-11-25 8:07 ` Simon Wright 2015-11-25 8:52 ` Dmitry A. Kazakov 1 sibling, 0 replies; 16+ messages in thread From: Simon Wright @ 2015-11-25 8:07 UTC (permalink / raw) 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!) ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: GNAT.Serial_Communication and Streams 2015-11-25 6:24 ` Shark8 2015-11-25 8:07 ` Simon Wright @ 2015-11-25 8:52 ` Dmitry A. Kazakov 2015-11-25 12:45 ` Shark8 1 sibling, 1 reply; 16+ messages in thread From: Dmitry A. Kazakov @ 2015-11-25 8:52 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: GNAT.Serial_Communication and Streams 2015-11-25 8:52 ` Dmitry A. Kazakov @ 2015-11-25 12:45 ` Shark8 2015-11-25 17:43 ` Dmitry A. Kazakov 0 siblings, 1 reply; 16+ messages in thread From: Shark8 @ 2015-11-25 12:45 UTC (permalink / raw) 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? ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: GNAT.Serial_Communication and Streams 2015-11-25 12:45 ` Shark8 @ 2015-11-25 17:43 ` Dmitry A. Kazakov 2015-11-29 8:45 ` Shark8 0 siblings, 1 reply; 16+ messages in thread From: Dmitry A. Kazakov @ 2015-11-25 17:43 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: GNAT.Serial_Communication and Streams 2015-11-25 17:43 ` Dmitry A. Kazakov @ 2015-11-29 8:45 ` Shark8 2015-11-29 9:33 ` Dmitry A. Kazakov 0 siblings, 1 reply; 16+ messages in thread From: Shark8 @ 2015-11-29 8:45 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: GNAT.Serial_Communication and Streams 2015-11-29 8:45 ` Shark8 @ 2015-11-29 9:33 ` Dmitry A. Kazakov 2015-11-29 11:34 ` Simon Wright 0 siblings, 1 reply; 16+ messages in thread From: Dmitry A. Kazakov @ 2015-11-29 9:33 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: GNAT.Serial_Communication and Streams 2015-11-29 9:33 ` Dmitry A. Kazakov @ 2015-11-29 11:34 ` Simon Wright 0 siblings, 0 replies; 16+ messages in thread From: Simon Wright @ 2015-11-29 11:34 UTC (permalink / raw) "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). ^ permalink raw reply [flat|nested] 16+ messages in thread
end of thread, other threads:[~2015-11-29 11:34 UTC | newest] Thread overview: 16+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2015-11-22 21:40 GNAT.Serial_Communication and Streams rrr.eee.27 2015-11-22 21:52 ` Simon Wright 2015-11-22 21:54 ` Jeffrey R. Carter 2015-11-24 1:29 ` Randy Brukardt 2015-11-24 16:09 ` Jeffrey R. Carter 2015-11-24 8:28 ` Dmitry A. Kazakov 2015-11-24 10:28 ` Simon Wright 2015-11-24 10:45 ` Dmitry A. Kazakov 2015-11-25 6:24 ` Shark8 2015-11-25 8:07 ` Simon Wright 2015-11-25 8:52 ` Dmitry A. Kazakov 2015-11-25 12:45 ` Shark8 2015-11-25 17:43 ` Dmitry A. Kazakov 2015-11-29 8:45 ` Shark8 2015-11-29 9:33 ` Dmitry A. Kazakov 2015-11-29 11:34 ` Simon Wright
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox