Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > comp.lang.forth > #56536 > unrolled thread
| Started by | krishna.myneni@ccreweb.org |
|---|---|
| First post | 2017-04-01 06:36 -0700 |
| Last post | 2017-04-06 10:53 -0700 |
| Articles | 20 on this page of 127 — 22 participants |
Back to article view | Back to comp.lang.forth
LLVM and Forth krishna.myneni@ccreweb.org - 2017-04-01 06:36 -0700
Re: LLVM and Forth anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2017-04-01 14:57 +0000
Re: LLVM and Forth krishna.myneni@ccreweb.org - 2017-04-01 11:55 -0700
Re: LLVM and Forth anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2017-04-02 15:24 +0000
Re: LLVM and Forth rickman <gnuarm@gmail.com> - 2017-04-01 11:21 -0400
Re: LLVM and Forth krishna.myneni@ccreweb.org - 2017-04-01 11:57 -0700
Re: LLVM and Forth Andrew Haley <andrew29@littlepinkcloud.invalid> - 2017-04-02 04:02 -0500
Re: LLVM and Forth krishna.myneni@ccreweb.org - 2017-04-02 06:35 -0700
Re: LLVM and Forth anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2017-04-02 14:41 +0000
Re: LLVM and Forth minforth@arcor.de - 2017-04-03 01:09 -0700
Re: LLVM and Forth krishna.myneni@ccreweb.org - 2017-04-03 05:32 -0700
Re: LLVM and Forth anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2017-04-03 13:52 +0000
Re: LLVM and Forth minforth@arcor.de - 2017-04-03 07:59 -0700
Re: LLVM and Forth anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2017-04-03 16:08 +0000
Re: LLVM and Forth Andrew Haley <andrew29@littlepinkcloud.invalid> - 2017-04-03 12:22 -0500
Re: LLVM and Forth Paul Rubin <no.email@nospam.invalid> - 2017-04-03 20:10 -0700
Re: LLVM and Forth minforth@arcor.de - 2017-04-03 22:19 -0700
Re: LLVM and Forth albert@cherry.spenarnc.xs4all.nl (Albert van der Horst) - 2017-04-04 16:12 +0200
Re: LLVM and Forth Walter Banks <walter@bytecraft.com> - 2017-04-05 17:27 -0400
Re: LLVM and Forth anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2017-04-03 14:29 +0000
Re: LLVM and Forth Andrew Haley <andrew29@littlepinkcloud.invalid> - 2017-04-03 03:17 -0500
Re: LLVM and Forth minforth@arcor.de - 2017-04-03 05:04 -0700
Re: LLVM and Forth anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2017-04-03 12:55 +0000
Re: LLVM and Forth Andrew Haley <andrew29@littlepinkcloud.invalid> - 2017-04-03 10:08 -0500
Re: LLVM and Forth anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2017-04-03 17:05 +0000
Re: LLVM and Forth Andrew Haley <andrew29@littlepinkcloud.invalid> - 2017-04-04 11:29 -0500
Re: LLVM and Forth albert@cherry.spenarnc.xs4all.nl (Albert van der Horst) - 2017-04-04 19:11 +0200
Re: LLVM and Forth Paul Rubin <no.email@nospam.invalid> - 2017-04-04 21:29 -0700
Re: LLVM and Forth anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2017-04-05 15:01 +0000
Re: LLVM and Forth Alex <alex@rivadpm.com> - 2017-04-05 18:42 +0100
Re: LLVM and Forth Andrew Haley <andrew29@littlepinkcloud.invalid> - 2017-04-06 04:01 -0500
Re: LLVM and Forth Spiros Bousbouras <spibou@gmail.com> - 2017-04-06 18:48 +0000
Re: LLVM and Forth Joel Rees <joel.rees@gmail.com> - 2017-04-06 18:42 -0700
Re: LLVM and Forth Andrew Haley <andrew29@littlepinkcloud.invalid> - 2017-04-07 04:02 -0500
Re: LLVM and Forth Joel Rees <joel.rees@gmail.com> - 2017-04-08 21:18 -0700
Re: LLVM and Forth Spiros Bousbouras <spibou@gmail.com> - 2017-04-08 22:43 +0000
Re: LLVM and Forth Joel Rees <joel.rees@gmail.com> - 2017-04-08 20:54 -0700
Re: LLVM and Forth anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2017-04-09 14:53 +0000
Re: LLVM and Forth Spiros Bousbouras <spibou@gmail.com> - 2017-04-10 00:38 +0000
Re: LLVM and Forth James Kuyper <jameskuyper@verizon.net> - 2017-04-09 22:46 -0400
Re: LLVM and Forth Robert Wessel <robertwessel2@yahoo.com> - 2017-04-09 22:27 -0500
Re: LLVM and Forth Spiros Bousbouras <spibou@gmail.com> - 2017-04-10 12:36 +0000
Re: LLVM and Forth Ben Bacarisse <ben.usenet@bsb.me.uk> - 2017-04-10 14:09 +0100
Re: LLVM and Forth Spiros Bousbouras <spibou@gmail.com> - 2017-04-10 13:07 +0000
Re: LLVM and Forth Ben Bacarisse <ben.usenet@bsb.me.uk> - 2017-04-10 16:18 +0100
Re: LLVM and Forth "James R. Kuyper" <jameskuyper@verizon.net> - 2017-04-10 11:51 -0400
Re: LLVM and Forth Spiros Bousbouras <spibou@gmail.com> - 2017-04-12 21:32 +0000
Re: LLVM and Forth "James R. Kuyper" <jameskuyper@verizon.net> - 2017-04-12 18:29 -0400
Re: LLVM and Forth hughaguilar96@gmail.com - 2017-04-12 15:29 -0700
Re: LLVM and Forth albert@cherry.spenarnc.xs4all.nl (Albert van der Horst) - 2017-04-13 02:55 +0200
Re: LLVM and Forth Joel Rees <joel.rees@gmail.com> - 2017-04-10 18:38 -0700
Re: LLVM and Forth Andrew Haley <andrew29@littlepinkcloud.invalid> - 2017-04-10 11:54 -0500
Re: LLVM and Forth Paul Rubin <no.email@nospam.invalid> - 2017-04-10 10:17 -0700
Re: LLVM and Forth Alex <alex@rivadpm.com> - 2017-04-03 17:02 +0100
Re: LLVM and Forth hughaguilar96@gmail.com - 2017-04-03 10:03 -0700
Re: LLVM and Forth krishna.myneni@ccreweb.org - 2017-04-04 03:25 -0700
Re: LLVM and Forth Spiros Bousbouras <spibou@gmail.com> - 2017-04-04 11:24 +0000
Re: LLVM and Forth krishna.myneni@ccreweb.org - 2017-04-04 04:55 -0700
Re: LLVM and Forth Spiros Bousbouras <spibou@gmail.com> - 2017-04-04 12:28 +0000
Re: LLVM and Forth anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2017-04-04 16:16 +0000
Re: LLVM and Forth albert@cherry.spenarnc.xs4all.nl (Albert van der Horst) - 2017-04-04 15:38 +0200
Re: LLVM and Forth albert@cherry.spenarnc.xs4all.nl (Albert van der Horst) - 2017-04-04 16:06 +0200
Re: LLVM and Forth krishna.myneni@ccreweb.org - 2017-04-04 17:57 -0700
Re: LLVM and Forth Rod Pemberton <NeedNotReplyHere@xrsevnneqk.cem> - 2017-04-05 00:44 -0400
Re: LLVM and Forth minforth@arcor.de - 2017-04-05 00:00 -0700
Re: LLVM and Forth krishna.myneni@ccreweb.org - 2017-04-05 08:47 -0700
Re: LLVM and Forth Andrew Haley <andrew29@littlepinkcloud.invalid> - 2017-04-05 11:04 -0500
Re: LLVM and Forth john <anon@example.com> - 2017-04-05 18:04 +0100
Re: LLVM and Forth hughaguilar96@gmail.com - 2017-04-05 13:04 -0700
Re: LLVM and Forth Paul Rubin <no.email@nospam.invalid> - 2017-04-05 18:20 -0700
Re: LLVM and Forth krishna.myneni@ccreweb.org - 2017-04-05 20:14 -0700
Re: LLVM and Forth Spiros Bousbouras <spibou@gmail.com> - 2017-04-06 12:33 +0000
Re: LLVM and Forth krishna.myneni@ccreweb.org - 2017-04-06 10:49 -0700
Re: LLVM and Forth Alex <alex@rivadpm.com> - 2017-04-06 18:55 +0100
Re: LLVM and Forth Spiros Bousbouras <spibou@gmail.com> - 2017-04-06 20:41 +0000
Re: LLVM and Forth Alex <alex@rivadpm.com> - 2017-04-06 21:47 +0100
Re: LLVM and Forth Alex <alex@rivadpm.com> - 2017-04-06 21:56 +0100
Re: LLVM and Forth Rod Pemberton <NeedNotReplyHere@xrsevnneqk.cem> - 2017-04-06 23:59 -0400
Re: LLVM and Forth Joel Rees <joel.rees@gmail.com> - 2017-04-06 17:10 -0700
Re: LLVM and Forth Rod Pemberton <NeedNotReplyHere@xrsevnneqk.cem> - 2017-04-07 03:33 -0400
Re: LLVM and Forth Spiros Bousbouras <spibou@gmail.com> - 2017-04-08 22:48 +0000
Re: LLVM and Forth Rod Pemberton <NeedNotReplyHere@xrsevnneqk.cem> - 2017-04-09 15:06 -0400
Re: LLVM and Forth Joel Rees <joel.rees@gmail.com> - 2017-04-08 22:45 -0700
Re: LLVM and Forth anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2017-04-09 14:27 +0000
Re: LLVM and Forth Joel Rees <joel.rees@gmail.com> - 2017-04-09 21:26 -0700
Re: LLVM and Forth Rod Pemberton <NeedNotReplyHere@xrsevnneqk.cem> - 2017-04-09 13:35 -0400
Re: LLVM and Forth Paul Rubin <no.email@nospam.invalid> - 2017-04-09 14:07 -0700
Re: LLVM and Forth minforth@arcor.de - 2017-04-05 12:16 -0700
Re: LLVM and Forth krishna.myneni@ccreweb.org - 2017-04-05 20:27 -0700
Re: LLVM and Forth Rod Pemberton <NeedNotReplyHere@xrsevnneqk.cem> - 2017-04-06 05:24 -0400
Re: LLVM and Forth krishna.myneni@ccreweb.org - 2017-04-06 03:26 -0700
Re: LLVM and Forth minforth@arcor.de - 2017-04-06 04:05 -0700
Re: LLVM and Forth Andrew Haley <andrew29@littlepinkcloud.invalid> - 2017-04-06 06:50 -0500
Re: LLVM and Forth Rod Pemberton <NeedNotReplyHere@xrsevnneqk.cem> - 2017-04-06 05:23 -0400
Re: LLVM and Forth Andrew Haley <andrew29@littlepinkcloud.invalid> - 2017-04-06 04:44 -0500
Re: LLVM and Forth Alex <alex@rivadpm.com> - 2017-04-06 10:57 +0100
Re: LLVM and Forth peter.m.falth@gmail.com - 2017-04-05 05:29 -0700
Re: LLVM and Forth "Rudy Velthuis" <newsgroups@rvelthuis.de> - 2017-04-14 02:04 +0000
Re: LLVM and Forth albert@cherry.spenarnc.xs4all.nl (Albert van der Horst) - 2017-04-15 14:03 +0200
Re: LLVM and Forth "Rudy Velthuis" <newsgroups@rvelthuis.de> - 2017-04-16 00:44 +0000
Re: LLVM and Forth alex@rivadpm.com - 2017-04-16 05:53 -0700
Re: LLVM and Forth anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2017-04-16 15:43 +0000
Re: LLVM and Forth "Rudy Velthuis" <newsgroups@rvelthuis.de> - 2017-04-16 22:27 +0000
Re: LLVM and Forth albert@cherry.spenarnc.xs4all.nl (Albert van der Horst) - 2017-04-18 02:45 +0200
Re: LLVM and Forth Alex <alex@rivadpm.com> - 2017-04-18 18:26 +0100
Re: LLVM and Forth albert@cherry.spenarnc.xs4all.nl (Albert van der Horst) - 2017-04-20 19:51 +0200
Re: LLVM and Forth Alex <alex@rivadpm.com> - 2017-04-20 19:08 +0100
Re: LLVM and Forth albert@cherry.spenarnc.xs4all.nl (Albert van der Horst) - 2017-04-20 20:42 +0200
Re: LLVM and Forth Alex <alex@rivadpm.com> - 2017-04-20 20:29 +0100
Re: LLVM and Forth Alex <alex@rivadpm.com> - 2017-04-20 20:48 +0100
Re: LLVM and Forth "Rudy Velthuis" <newsgroups@rvelthuis.de> - 2017-04-21 11:49 +0000
Re: LLVM and Forth Rod Pemberton <NeedNotReplyHere@xrsevnneqk.cem> - 2017-04-03 20:39 -0400
Re: LLVM and Forth Alex <alex@rivadpm.com> - 2017-04-02 21:15 +0100
Re: LLVM and Forth hughaguilar96@gmail.com - 2017-04-02 15:18 -0700
Re: LLVM and Forth Alex <alex@rivadpm.com> - 2017-04-03 13:07 +0100
Re: LLVM and Forth hughaguilar96@gmail.com - 2017-04-03 09:45 -0700
Re: LLVM and Forth Alex <alex@rivadpm.com> - 2017-04-03 22:52 +0100
Re: LLVM and Forth hughaguilar96@gmail.com - 2017-04-03 15:25 -0700
Re: LLVM and Forth Alex <alex@rivadpm.com> - 2017-04-06 09:35 +0100
Re: LLVM and Forth antispam@math.uni.wroc.pl - 2017-04-06 01:36 +0000
Re: LLVM and Forth minforth@arcor.de - 2017-04-05 22:00 -0700
Re: LLVM and Forth Alex <alex@rivadpm.com> - 2017-04-06 09:52 +0100
Re: LLVM and Forth hughaguilar96@gmail.com - 2017-04-06 20:15 -0700
Re: LLVM and Forth krishna.myneni@ccreweb.org - 2017-04-03 05:20 -0700
Re: LLVM and Forth Alex <alex@rivadpm.com> - 2017-04-03 17:11 +0100
Re: LLVM and Forth Alex <alex@rivadpm.com> - 2017-04-06 17:43 +0100
Re: LLVM and Forth krishna.myneni@ccreweb.org - 2017-04-06 10:53 -0700
Page 2 of 7 — ← Prev page 1 [2] 3 4 5 6 7 Next page →
| From | Andrew Haley <andrew29@littlepinkcloud.invalid> |
|---|---|
| Date | 2017-04-03 03:17 -0500 |
| Message-ID | <qOKdneQNfs-vmH_FnZ2dnUU7-UednZ2d@supernews.com> |
| In reply to | #56586 |
krishna.myneni@ccreweb.org wrote: > On Sunday, April 2, 2017 at 4:02:26 AM UTC-5, Andrew Haley wrote: >> krishna.myneni@ccreweb.org wrote: >> > >> > Supposedly Java virtual machines have been developed with LLVM. >> >> It is very difficult, partly for the reasons described: LLVM uses C >> semantics for its intermedieate language, so if your language is along >> way from C this can be problematic. Optimizing without specific >> language semantics is somewhere between hard and impossible. > > The fundamental question appears to be independent of LLVM: > > If one were to write a Forth to C translator, how likely is it that > the translator would result in C code which is considered undefined > in the new C standard, i.e. how problematic would "nasal demons" be > in the translated code? Single-threaded, it wouldn't be problematic at all. The nasal daemons tend to happen if you're pushing the envelope of optimization. As long as you translated into well-defined C, which isn't difficult, you'd be fine. I don't think there are any Forth constructs that wouldn't translate easily. The real problem occurs when you're trying to generate highly efficient C. Multi-threading would be harder, at least in theory. Andrew.
[toc] | [prev] | [next] | [standalone]
| From | minforth@arcor.de |
|---|---|
| Date | 2017-04-03 05:04 -0700 |
| Message-ID | <8a1c6eda-9eb1-4971-97e6-75b78e6c1333@googlegroups.com> |
| In reply to | #56650 |
Am Montag, 3. April 2017 10:17:59 UTC+2 schrieb Andrew Haley: > krishna.myneni@ccreweb.org wrote: > > On Sunday, April 2, 2017 at 4:02:26 AM UTC-5, Andrew Haley wrote: > >> krishna.myneni@ccreweb.org wrote: > >> > > >> > Supposedly Java virtual machines have been developed with LLVM. > >> > >> It is very difficult, partly for the reasons described: LLVM uses C > >> semantics for its intermedieate language, so if your language is along > >> way from C this can be problematic. Optimizing without specific > >> language semantics is somewhere between hard and impossible. > > > > The fundamental question appears to be independent of LLVM: > > > > If one were to write a Forth to C translator, how likely is it that > > the translator would result in C code which is considered undefined > > in the new C standard, i.e. how problematic would "nasal demons" be > > in the translated code? > > Single-threaded, it wouldn't be problematic at all. The nasal daemons > tend to happen if you're pushing the envelope of optimization. As > long as you translated into well-defined C, which isn't difficult, > you'd be fine. I don't think there are any Forth constructs that > wouldn't translate easily. The real problem occurs when you're trying > to generate highly efficient C. > > Multi-threading would be harder, at least in theory. > > Andrew. There is no highly efficient C per se, only good algorithms and good code compilers. Only occasionally I do some disassembling or profiling of the final code. As last ressort there is always the possibility to put some assembler lines within the C code. But this was _never_ required to solve low-performance issues, but to write special hardware drivers.
[toc] | [prev] | [next] | [standalone]
| From | anton@mips.complang.tuwien.ac.at (Anton Ertl) |
|---|---|
| Date | 2017-04-03 12:55 +0000 |
| Message-ID | <2017Apr3.145550@mips.complang.tuwien.ac.at> |
| In reply to | #56650 |
Andrew Haley <andrew29@littlepinkcloud.invalid> writes:
>krishna.myneni@ccreweb.org wrote:
>> If one were to write a Forth to C translator, how likely is it that
>> the translator would result in C code which is considered undefined
>> in the new C standard, i.e. how problematic would "nasal demons" be
>> in the translated code?
>
>Single-threaded, it wouldn't be problematic at all. The nasal daemons
>tend to happen if you're pushing the envelope of optimization. As
>long as you translated into well-defined C, which isn't difficult,
>you'd be fine. I don't think there are any Forth constructs that
>wouldn't translate easily. The real problem occurs when you're trying
>to generate highly efficient C.
Bullshit. Bullshit. Bullshit. Bullshit. Bullshit. A whole
paragraph of bullshit, with every single sentence being bullshit. You
don't have to believe me, in the following I refute them by one:
1) All the nasal demon examples I came across have been in
single-threaded programs. (You can find some of them in
<http://www.complang.tuwien.ac.at/kps2015/proceedings/KPS_2015_submission_29.pdf>,
and more in the referenced papers).
2) Nasal demon compilers "optimized" away the memset() that was
intended to prevent Heartbleed, and the programmers did not put this
memset() in to push the envelope of optimization. Likewise,
programmers do not put in bounds checks to push the envelope of
optimization, yet nasal demon compilers often "optimize" these bounds
checks away. Actually, most of the examples of nasal demons I know of
have nothing to do with "pushing the envelope of optimization".
3) If it is not difficult to produce well-defined C, you would expect
that at least the hardcore members of the nasal demon church, the
developers of GCC and Clang/LLVM, would be able to do it, yet both of
these compilers exercised undefined behaviour even when compiling an
empty program with optimization off.
4) Anything to do with treating cells as either addresses or as
integers can easily turn into undefined behaviour. Dealing with
memory can also easily incur undefined behaviour. Implementing Forth
addresses as C constructs without incurring undefined behaviour is
also challenging, and certainly not easy (e.g., how do you implement
ALLOCATE and "-"?).
5) Nasal demon compilers "optimized" away the memset() that was
intended to prevent Heartbleed, and the programmers did not put this
memset() in to generate highly efficient C. Likewise, programmers do
not put in bounds checks to generate highly-efficient C, yet nasal
demon compilers often "optimize" these bounds checks away. Actually,
most of the examples of nasal demons I know of have nothing to do with
"highly-efficient C".
It may be, though, that "highly-efficient" C programs that "push the
envelope of optimization" may be even more frequently afflicted by
nasal demons than the rest. You suggest to avoid going there. Yet
nasal demon fans claim (without empirical evidence) that nasal demons
are a good thing for efficiency reasons. This does not compute.
- anton
--
M. Anton Ertl http://www.complang.tuwien.ac.at/anton/home.html
comp.lang.forth FAQs: http://www.complang.tuwien.ac.at/forth/faq/toc.html
New standard: http://www.forth200x.org/forth200x.html
EuroForth 2016: http://www.euroforth.org/ef16/
[toc] | [prev] | [next] | [standalone]
| From | Andrew Haley <andrew29@littlepinkcloud.invalid> |
|---|---|
| Date | 2017-04-03 10:08 -0500 |
| Message-ID | <NNSdnXwvutwb-H_FnZ2dnUU7-XXNnZ2d@supernews.com> |
| In reply to | #56659 |
Anton Ertl <anton@mips.complang.tuwien.ac.at> wrote: > Andrew Haley <andrew29@littlepinkcloud.invalid> writes: >>krishna.myneni@ccreweb.org wrote: >>> If one were to write a Forth to C translator, how likely is it that >>> the translator would result in C code which is considered undefined >>> in the new C standard, i.e. how problematic would "nasal demons" be >>> in the translated code? >> >>Single-threaded, it wouldn't be problematic at all. The nasal daemons >>tend to happen if you're pushing the envelope of optimization. As >>long as you translated into well-defined C, which isn't difficult, >>you'd be fine. I don't think there are any Forth constructs that >>wouldn't translate easily. The real problem occurs when you're trying >>to generate highly efficient C. > > Bullshit. Bullshit. Bullshit. Bullshit. Bullshit. A whole > paragraph of bullshit, with every single sentence being bullshit. You > don't have to believe me, in the following I refute them by one: LOL! Bullshit yourself. > 1) All the nasal demon examples I came across have been in > single-threaded programs. (You can find some of them in > <http://www.complang.tuwien.ac.at/kps2015/proceedings/KPS_2015_submission_29.pdf>, > and more in the referenced papers). > > 2) Nasal demon compilers "optimized" away the memset() that was > intended to prevent Heartbleed, and the programmers did not put this > memset() in to push the envelope of optimization. Likewise, > programmers do not put in bounds checks to push the envelope of > optimization, yet nasal demon compilers often "optimize" these bounds > checks away. Actually, most of the examples of nasal demons I know of > have nothing to do with "pushing the envelope of optimization". I've seen the Heartbleed bug, and it was was a missing bounds check. It was fixed by adding the bounds check. I can't find any reference to a miscompiled memset. > 3) If it is not difficult to produce well-defined C, you would expect > that at least the hardcore members of the nasal demon church, the > developers of GCC and Clang/LLVM, would be able to do it, yet both of > these compilers exercised undefined behaviour even when compiling an > empty program with optimization off. Nobody is perfect. There are bugs in all large programs. There's nothing special about undefined behaviour: it's just another kind of error. > 4) Anything to do with treating cells as either addresses or as > integers can easily turn into undefined behaviour. Dealing with > memory can also easily incur undefined behaviour. Implementing Forth > addresses as C constructs without incurring undefined behaviour is > also challenging, and certainly not easy (e.g., how do you implement > ALLOCATE and "-"?). I'd do it like this: Forth cells are unsigned ints, allocated on top of a byte array which is data space. All integer arithmetic is modulo N, where N is the word size. Division has to be handled by careful conversion, to make sure there aren't any overflows. That's a little bit fiddly, but all perfectly practicable. What problem do you forsee with ALLOCATE? The only integer types seen in memory by C are bytes and unsigned ints. I suppose there might be some corner cases if you, say, store an int which you then read as a floating-point type, but I don't think that is fully defined by Forth either. > 5) Nasal demon compilers "optimized" away the memset() that was > intended to prevent Heartbleed, and the programmers did not put this > memset() in to generate highly efficient C. Likewise, programmers do > not put in bounds checks to generate highly-efficient C, yet nasal > demon compilers often "optimize" these bounds checks away. Actually, > most of the examples of nasal demons I know of have nothing to do with > "highly-efficient C". So don't write undefined programs, then. The question, as you seem to have forgotten it, was: >>> If one were to write a Forth to C translator, how likely is it that >>> the translator would result in C code which is considered undefined >>> in the new C standard, i.e. how problematic would "nasal demons" be >>> in the translated code? And the correct answer is that it wouldn't be problematic at all. There's no need for a Forth translator to have undefined behaviour. Of course it is likely that any program of this complexity will have bugs to begin with, and some of these bugs will probably exhibit undefined behaviour. However, it's then just a matter of fixing the bugs, and you're done. And there's an undefined behaviour checker in GCC to help with that. Andrew.
[toc] | [prev] | [next] | [standalone]
| From | anton@mips.complang.tuwien.ac.at (Anton Ertl) |
|---|---|
| Date | 2017-04-03 17:05 +0000 |
| Message-ID | <2017Apr3.190545@mips.complang.tuwien.ac.at> |
| In reply to | #56664 |
Andrew Haley <andrew29@littlepinkcloud.invalid> writes:
>Anton Ertl <anton@mips.complang.tuwien.ac.at> wrote:
>> 2) Nasal demon compilers "optimized" away the memset() that was
>> intended to prevent Heartbleed, and the programmers did not put this
>> memset() in to push the envelope of optimization. Likewise,
>> programmers do not put in bounds checks to push the envelope of
>> optimization, yet nasal demon compilers often "optimize" these bounds
>> checks away. Actually, most of the examples of nasal demons I know of
>> have nothing to do with "pushing the envelope of optimization".
>
>I've seen the Heartbleed bug, and it was was a missing bounds check.
>It was fixed by adding the bounds check. I can't find any reference
>to a miscompiled memset.
I am sorry, I confused Heartbleed with an OpenSSH bug
<https://lwn.net/Articles/672465/>, where GCC "optimized" away the
memset() that was intended to mitigate the effects that other
vulnerabilities had.
>> 3) If it is not difficult to produce well-defined C, you would expect
>> that at least the hardcore members of the nasal demon church, the
>> developers of GCC and Clang/LLVM, would be able to do it, yet both of
>> these compilers exercised undefined behaviour even when compiling an
>> empty program with optimization off.
>
>Nobody is perfect. There are bugs in all large programs. There's
>nothing special about undefined behaviour: it's just another kind of
>error.
As I wrote: "well-defined C, which isn't difficult" is bullshit.
>> 4) Anything to do with treating cells as either addresses or as
>> integers can easily turn into undefined behaviour. Dealing with
>> memory can also easily incur undefined behaviour. Implementing Forth
>> addresses as C constructs without incurring undefined behaviour is
>> also challenging, and certainly not easy (e.g., how do you implement
>> ALLOCATE and "-"?).
>
>I'd do it like this: Forth cells are unsigned ints, allocated on top
>of a byte array which is data space. All integer arithmetic is modulo
>N, where N is the word size. Division has to be handled by careful
>conversion, to make sure there aren't any overflows. That's a little
>bit fiddly, but all perfectly practicable.
>
>What problem do you forsee with ALLOCATE?
How do you translate it "easily"?
>The only integer types seen
>in memory by C are bytes and unsigned ints.
How do you implement @ and C@?
>> 5) Nasal demon compilers "optimized" away the memset() that was
>> intended to prevent Heartbleed, and the programmers did not put this
>> memset() in to generate highly efficient C. Likewise, programmers do
>> not put in bounds checks to generate highly-efficient C, yet nasal
>> demon compilers often "optimize" these bounds checks away. Actually,
>> most of the examples of nasal demons I know of have nothing to do with
>> "highly-efficient C".
>
>So don't write undefined programs, then. The question, as you seem to
>have forgotten it, was:
>
>>>> If one were to write a Forth to C translator, how likely is it that
>>>> the translator would result in C code which is considered undefined
>>>> in the new C standard, i.e. how problematic would "nasal demons" be
>>>> in the translated code?
>
>And the correct answer is that it wouldn't be problematic at all.
>There's no need for a Forth translator to have undefined behaviour.
>
>Of course it is likely that any program of this complexity will have
>bugs to begin with, and some of these bugs will probably exhibit
>undefined behaviour. However, it's then just a matter of fixing the
>bugs, and you're done. And there's an undefined behaviour checker in
>GCC to help with that.
And after all this effort (which I wouldn't call "not problematic at
all" nor "not difficult"; it's not just like a -Wall test, instead you
have lots of mutually exclusive -fsanitize flags, and then the
undefined behaviours only show up at run-time with appropriate
inputs), at the end you have a program with undefined behaviours that
have not been caught by the checker in GCC. But sure, if you love
nasal demons, you also find that not problematic at all.
- anton
--
M. Anton Ertl http://www.complang.tuwien.ac.at/anton/home.html
comp.lang.forth FAQs: http://www.complang.tuwien.ac.at/forth/faq/toc.html
New standard: http://www.forth200x.org/forth200x.html
EuroForth 2016: http://www.euroforth.org/ef16/
[toc] | [prev] | [next] | [standalone]
| From | Andrew Haley <andrew29@littlepinkcloud.invalid> |
|---|---|
| Date | 2017-04-04 11:29 -0500 |
| Message-ID | <a-SdnVgDEexEVH7FnZ2dnUU7-RHNnZ2d@supernews.com> |
| In reply to | #56672 |
Anton Ertl <anton@mips.complang.tuwien.ac.at> wrote: > Andrew Haley <andrew29@littlepinkcloud.invalid> writes: >>Anton Ertl <anton@mips.complang.tuwien.ac.at> wrote: >> >>Nobody is perfect. There are bugs in all large programs. There's >>nothing special about undefined behaviour: it's just another kind of >>error. > > As I wrote: "well-defined C, which isn't difficult" is bullshit. Note that "not difficult" wasn't in the OP's question. But "C which isn't difficult" doesn't smell much better. C is what it is; C is not an easy language. >>> 4) Anything to do with treating cells as either addresses or as >>> integers can easily turn into undefined behaviour. Dealing with >>> memory can also easily incur undefined behaviour. Implementing Forth >>> addresses as C constructs without incurring undefined behaviour is >>> also challenging, and certainly not easy (e.g., how do you implement >>> ALLOCATE and "-"?). >> >>I'd do it like this: Forth cells are unsigned ints, allocated on top My error: this should have been "unsigned integers of the same size as size_t and intptr_t" not "unsigned ints".) >>of a byte array which is data space. All integer arithmetic is modulo >>N, where N is the word size. Division has to be handled by careful >>conversion, to make sure there aren't any overflows. That's a little >>bit fiddly, but all perfectly practicable. >> >>What problem do you forsee with ALLOCATE? > > How do you translate it "easily"? I'd be tempted to allocate all of Forth's data space into a single char array, and implement ALLOCATE with a custom allocator in that space. That fits nicely with Forth's flat memory space. But it certainly could be done with malloc(), although care would have to be taken not to hit UB comparing pointers to malloc'd data and Forth's data space. >>The only integer types seen in memory by C are bytes and unsigned >>ints. > > How do you implement @ and C@? Simple memory reads. It's legitimate to alias character types and other types, so a suitably aligned character address can be cast to a size_t* or a uintptr_t*. I think it'd probably make the most sense to use uintptr_t for Forth cells. Of course, this requires a system to be able to cast freely between uintptr_t and and pointer types, but that is implementation- defined rather than undefined behaviour. Every C compiler I care about (or, in fact, know about) supports it. Alternatively, Forth addresses could be integers and used as indexes into the data array; this might be more convenient, if slightly slower. >>Of course it is likely that any program of this complexity will have >>bugs to begin with, and some of these bugs will probably exhibit >>undefined behaviour. However, it's then just a matter of fixing the >>bugs, and you're done. And there's an undefined behaviour checker in >>GCC to help with that. > > And after all this effort (which I wouldn't call "not problematic at > all" nor "not difficult"; it's not just like a -Wall test, instead you > have lots of mutually exclusive -fsanitize flags, and then the > undefined behaviours only show up at run-time with appropriate > inputs), at the end you have a program with undefined behaviours that > have not been caught by the checker in GCC. I think you'd be fine with "-fsanitize=undefined". I agree that it wouldn't catch everything: there are no magic bullets. > But sure, if you love nasal demons, you also find that not > problematic at all. Andrew.
[toc] | [prev] | [next] | [standalone]
| From | albert@cherry.spenarnc.xs4all.nl (Albert van der Horst) |
|---|---|
| Date | 2017-04-04 19:11 +0200 |
| Message-ID | <oc0k4g$kea$1@cherry.spenarnc.xs4all.nl> |
| In reply to | #56718 |
In article <a-SdnVgDEexEVH7FnZ2dnUU7-RHNnZ2d@supernews.com>, Andrew Haley <andrew29@littlepinkcloud.invalid> wrote: <SNIP> >Simple memory reads. It's legitimate to alias character types and >other types, so a suitably aligned character address can be cast to a >size_t* or a uintptr_t*. > >I think it'd probably make the most sense to use uintptr_t for Forth >cells. Of course, this requires a system to be able to cast freely >between uintptr_t and and pointer types, but that is implementation- >defined rather than undefined behaviour. Every C compiler I care >about (or, in fact, know about) supports it. Casts to a different type are problematic. As I said before, the proper c-idiom is unions. This probably results in less problems because you tell the c-compiler precisely what is going on. <SNIP> >Andrew. -- Albert van der Horst, UTRECHT,THE NETHERLANDS Economic growth -- being exponential -- ultimately falters. albert@spe&ar&c.xs4all.nl &=n http://home.hccnet.nl/a.w.m.van.der.horst
[toc] | [prev] | [next] | [standalone]
| From | Paul Rubin <no.email@nospam.invalid> |
|---|---|
| Date | 2017-04-04 21:29 -0700 |
| Message-ID | <874ly3bhod.fsf@nightsong.com> |
| In reply to | #56718 |
Andrew Haley <andrew29@littlepinkcloud.invalid> writes: > I think you'd be fine with "-fsanitize=undefined". I agree that it > wouldn't catch everything: there are no magic bullets. http://blog.regehr.org/archives/523 might help some.
[toc] | [prev] | [next] | [standalone]
| From | anton@mips.complang.tuwien.ac.at (Anton Ertl) |
|---|---|
| Date | 2017-04-05 15:01 +0000 |
| Message-ID | <2017Apr5.170145@mips.complang.tuwien.ac.at> |
| In reply to | #56718 |
Andrew Haley <andrew29@littlepinkcloud.invalid> writes:
>Anton Ertl <anton@mips.complang.tuwien.ac.at> wrote:
>> Andrew Haley <andrew29@littlepinkcloud.invalid> writes:
>>>Anton Ertl <anton@mips.complang.tuwien.ac.at> wrote:
>>>
>>>Nobody is perfect. There are bugs in all large programs. There's
>>>nothing special about undefined behaviour: it's just another kind of
>>>error.
>>
>> As I wrote: "well-defined C, which isn't difficult" is bullshit.
>
>Note that "not difficult" wasn't in the OP's question.
Not in these words. Anyway, you found it necessary to make that claim
in your answer.
>But "C which
>isn't difficult" doesn't smell much better. C is what it is; C is not
>an easy language.
I know it does not smell much better to you. That's because the only
C that you accept as C is "well-defined C"; for everything else you
pretend that you don't know what it means.
Translating Forth into traditional C (that compiles as intended by PCC
and early versions of GCC) is indeed not difficult; after all,
traditional C and Forth are semantically close to each other. Take a
look at Gforth or forth2c to get an idea on how to do it.
The resulting code is, of course, full of undefined behaviour, like
most of the other C code around; and in this case I think it's
impossible to get rid of the undefined behaviour without losing
functionality and performance, and even if you are willing to pay that
price, it requires significantly more effort, and in the end, you will
probably still have some undefined behaviour somewhere.
In general, programming is not easy, but there are different levels of
difficulty:
1) Programmers tend to be able to satisfy the requirements that the
users use a lot, and/or care about a lot. Corner cases, less so (and
in the Forth community, some people celebrate being wrong in corner
cases, no matter how easy it would have been to do the right thing;
actually, that's very similar to the attitude that gives us nasal
demons).
2) Programmers are pretty bad at dealing with cases that do not occur
during the course of normal operations. That's why security
vulnerabilities occur so often and are so long-lived. Writing tests
for unusual cases helps a little, but only shines a light on the cases
that are tested. There is no guarantee that tests cover everything.
Even with automated fuzz testing these days, the amount of automation
is limited: a specialized setup for a certain system call or something
caught things that the general fuzz tester had not caught.
3) Complete correctness proofs of programs are outside the competence
of nearly all programmers (and pretty pointless, because they would
prove only the correctness wrt the specification, which itself may be
buggy).
Now, to write a C program that is guaranteed to never exercise
undefined behaviour requires competences on the level 3. The
much-hyped sanitizers of GCC and Clang allow finding some (not all)
undefined behaviours using the well-established testing methodology.
So you will find undefined behaviours in the cases exercized by normal
users, but you will tend not to find undefined behaviour in those
cases exercized by an attacker; it's as difficult as finding the all
the vulnerabilities in the first place. E.g., in the OpenSSH case, if
you thought about the vulnerability, you would fix it right away,
rather than writing a test case that exploited it, and waiting for the
sanitizer to report that freed memory was accessed (if the sanitizer
actually does check that), and then fixing it.
>>>> 4) Anything to do with treating cells as either addresses or as
>>>> integers can easily turn into undefined behaviour. Dealing with
>>>> memory can also easily incur undefined behaviour. Implementing Forth
>>>> addresses as C constructs without incurring undefined behaviour is
>>>> also challenging, and certainly not easy (e.g., how do you implement
>>>> ALLOCATE and "-"?).
>>>
>>>I'd do it like this: Forth cells are unsigned ints, allocated on top
>
>My error: this should have been "unsigned integers of the same size as
>size_t and intptr_t" not "unsigned ints".)
>
>>>of a byte array which is data space. All integer arithmetic is modulo
>>>N, where N is the word size. Division has to be handled by careful
>>>conversion, to make sure there aren't any overflows. That's a little
>>>bit fiddly, but all perfectly practicable.
>>>
>>>What problem do you forsee with ALLOCATE?
>>
>> How do you translate it "easily"?
>
>I'd be tempted to allocate all of Forth's data space into a single
>char array, and implement ALLOCATE with a custom allocator in that
>space.
That's "easy" in your book? The resulting Forth system would be
severely restricted: E.g., you cannot use it to call system calls like
mmap() and make use of the results (but then, that's undefined
in the C standard anyway).
> That fits nicely with Forth's flat memory space. But it
>certainly could be done with malloc(), although care would have to be
>taken not to hit UB comparing pointers to malloc'd data and Forth's
>data space.
Right. Anything but "not difficult"; I don't think it's possible.
Subtraction is also a problem.
>> How do you implement @ and C@?
>
>Simple memory reads.
What C code?
>It's legitimate to alias character types and
>other types, so a suitably aligned character address can be cast to a
>size_t* or a uintptr_t*.
That contradicts things I have read about accessing casted pointers.
>I think it'd probably make the most sense to use uintptr_t for Forth
>cells. Of course, this requires a system to be able to cast freely
>between uintptr_t and and pointer types, but that is implementation-
>defined rather than undefined behaviour. Every C compiler I care
>about (or, in fact, know about) supports it.
It's interesting how quick you come off your high horse once things
like writing actual C code come into play. "It works as intended on
the compilers and/or machines the programmer used" has been my
yardstick for determining the correctness of programs all along, yet
nasal demon fans insist that most (possibly all) of these programs are
"buggy".
>Alternatively, Forth addresses could be integers and used as indexes
>into the data array; this might be more convenient, if slightly
>slower.
Convenient in what way? Win32Forth once used relative pointers to
achieve relocatability. They soon returned to absolute pointers.
>>>Of course it is likely that any program of this complexity will have
>>>bugs to begin with, and some of these bugs will probably exhibit
>>>undefined behaviour. However, it's then just a matter of fixing the
>>>bugs, and you're done. And there's an undefined behaviour checker in
>>>GCC to help with that.
>>
>> And after all this effort (which I wouldn't call "not problematic at
>> all" nor "not difficult"; it's not just like a -Wall test, instead you
>> have lots of mutually exclusive -fsanitize flags, and then the
>> undefined behaviours only show up at run-time with appropriate
>> inputs), at the end you have a program with undefined behaviours that
>> have not been caught by the checker in GCC.
>
>I think you'd be fine with "-fsanitize=undefined". I agree that it
>wouldn't catch everything: there are no magic bullets.
I.e., it's not "not difficult" to write "well-defined C".
Looking at
<https://gcc.gnu.org/onlinedocs/gcc/Instrumentation-Options.html>, I
see
|-fsanitize=all is not allowed, as some sanitizers cannot be used together.
- anton
--
M. Anton Ertl http://www.complang.tuwien.ac.at/anton/home.html
comp.lang.forth FAQs: http://www.complang.tuwien.ac.at/forth/faq/toc.html
New standard: http://www.forth200x.org/forth200x.html
EuroForth 2016: http://www.euroforth.org/ef16/
[toc] | [prev] | [next] | [standalone]
| From | Alex <alex@rivadpm.com> |
|---|---|
| Date | 2017-04-05 18:42 +0100 |
| Message-ID | <oc3a55$k0$1@dont-email.me> |
| In reply to | #56753 |
On 4/5/2017 16:01, Anton Ertl wrote: > Convenient in what way? Win32Forth once used relative pointers to > achieve relocatability. They soon returned to absolute pointers. The decision was mine, and the reasons were pretty simple. 1. Relocation was a requirement of the C wrapper that loaded the Forth image by allocating a lump of storage but with no guarantee of getting the same address every time. With a proper EXE format for the image, absolute addresses were possible, and the Windows loader is instructed to use a specific load address (normally $40000). 2. Every external access to the OS required those parameters that were pointers to be relocated/derelocated on each access. It is painful coding with REL>ABS and ABS>REL. 3. Run time relocation required the permanent reservation of a register. The x86 in 32 bit mode is not overendowed with them. -- Alex
[toc] | [prev] | [next] | [standalone]
| From | Andrew Haley <andrew29@littlepinkcloud.invalid> |
|---|---|
| Date | 2017-04-06 04:01 -0500 |
| Message-ID | <T_Odnc4vKuR0nnvFnZ2dnUU7-fvNnZ2d@supernews.com> |
| In reply to | #56753 |
Anton Ertl <anton@mips.complang.tuwien.ac.at> wrote: > Andrew Haley <andrew29@littlepinkcloud.invalid> writes: >>Anton Ertl <anton@mips.complang.tuwien.ac.at> wrote: >>> Andrew Haley <andrew29@littlepinkcloud.invalid> writes: >>>>Anton Ertl <anton@mips.complang.tuwien.ac.at> wrote: >>>> >>>>Nobody is perfect. There are bugs in all large programs. There's >>>>nothing special about undefined behaviour: it's just another kind of >>>>error. >>> >>> As I wrote: "well-defined C, which isn't difficult" is bullshit. >> >>Note that "not difficult" wasn't in the OP's question. > > Not in these words. Anyway, you found it necessary to make that claim > in your answer. > >>But "C which isn't difficult" doesn't smell much better. C is what >>it is; C is not an easy language. > > I know it does not smell much better to you. That's because the only > C that you accept as C is "well-defined C"; for everything else you > pretend that you don't know what it means. Au contraire, I know that it does not mean anything as a C program. It might mean something on an actual implementation, running on particular hardware, if you decide that such an operational definition satisfies you. But we must separate our concerns: language specifications exist independently of implementations. > Now, to write a C program that is guaranteed to never exercise > undefined behaviour requires competences on the level 3. That is precisely the same problem as writing a program in any language which is guaranteed to be correct. >>I'd be tempted to allocate all of Forth's data space into a single >>char array, and implement ALLOCATE with a custom allocator in that >>space. > > That's "easy" in your book? No. But it's not a huge part of implementing a Forth-to-C translator for the entire standard Forth language and all of the optional wordsets. > The resulting Forth system would be severely restricted: E.g., you > cannot use it to call system calls like mmap() and make use of the > results (but then, that's undefined in the C standard anyway). You can't call mmap() from standard Forth or standard C anyway. But if POSIX is allowed, a lot more possibilities become available. With POSIX it would be a lot easier: you could mmap() a single flat space for all of Forth's memory and remap parts of that as required. > Right. Anything but "not difficult"; I don't think it's possible. It is possible. You'd have to modify @ and ! to know about the diferent spaces. >>> How do you implement @ and C@? >> >>Simple memory reads. > > What C code? I'm not going to write the damn thing for you. >>It's legitimate to alias character types and other types, so a >>suitably aligned character address can be cast to a size_t* or a >>uintptr_t*. > > That contradicts things I have read about accessing casted pointers. Then what you have read is wrong. You can't cast between pointers to incompatible types and access the data. >>I think it'd probably make the most sense to use uintptr_t for Forth >>cells. Of course, this requires a system to be able to cast freely >>between uintptr_t and and pointer types, but that is implementation- >>defined rather than undefined behaviour. Every C compiler I care >>about (or, in fact, know about) supports it. > > It's interesting how quick you come off your high horse once things > like writing actual C code come into play. "It works as intended on > the compilers and/or machines the programmer used" has been my > yardstick for determining the correctness of programs all along, yet > nasal demon fans insist that most (possibly all) of these programs > are "buggy". The question was unambiguously limited to undefined behaviour. It was not about translating Forth into totally portable C. Using implementation-defined behaviour is just fine. But implementation- defined behaviour does not mean "it seemed to work the last time I tried it." Andrew.
[toc] | [prev] | [next] | [standalone]
| From | Spiros Bousbouras <spibou@gmail.com> |
|---|---|
| Date | 2017-04-06 18:48 +0000 |
| Message-ID | <s4wFA.637264$3a3.286206@fx43.am4> |
| In reply to | #56753 |
On Wed, 05 Apr 2017 15:01:45 GMT
anton@mips.complang.tuwien.ac.at (Anton Ertl) wrote:
> Andrew Haley <andrew29@littlepinkcloud.invalid> writes:
>
> Translating Forth into traditional C (that compiles as intended by PCC
> and early versions of GCC) is indeed not difficult; after all,
> traditional C and Forth are semantically close to each other. Take a
> look at Gforth or forth2c to get an idea on how to do it.
>
> The resulting code is, of course, full of undefined behaviour, like
> most of the other C code around; and in this case I think it's
> impossible to get rid of the undefined behaviour without losing
> functionality and performance, and even if you are willing to pay that
> price, it requires significantly more effort, and in the end, you will
> probably still have some undefined behaviour somewhere.
Here we need to make a distinction : I will term "weak undefined behaviour"
(WUB) C code which is not defined according to the C standard and "strong
undefined behaviour" (SUB) C code which is not defined according to
*anything* where "anything" could mean some standard which enhances the C
standard (like POSIX) and also relevant documentation of the compiler or
libraries one uses or whatever. Our main conern here is predictable behaviour
of the code so I believe the deciding concept is SUB rather than WUB. So if
"The resulting code is, of course, full of undefined behaviour" means WUB
then that's probably correct (there's a lot of useful stuff you can't do just
by <C according to the standard>) but if you mean SUB then I doubt it. In any
case , if code has SUB then I cannot imagine on what basis one may think it
works and it will reliably continue to do so in the future : even if it
passes testing , then that's by coincidence. So if a code exhibits SUB then
it's buggy and it needs to be fixed.
> In general, programming is not easy, but there are different levels of
> difficulty:
>
> 1) Programmers tend to be able to satisfy the requirements that the
> users use a lot, and/or care about a lot. Corner cases, less so (and
> in the Forth community, some people celebrate being wrong in corner
> cases, no matter how easy it would have been to do the right thing;
> actually, that's very similar to the attitude that gives us nasal
> demons).
>
> 2) Programmers are pretty bad at dealing with cases that do not occur
> during the course of normal operations. That's why security
> vulnerabilities occur so often and are so long-lived. Writing tests
> for unusual cases helps a little, but only shines a light on the cases
> that are tested. There is no guarantee that tests cover everything.
> Even with automated fuzz testing these days, the amount of automation
> is limited: a specialized setup for a certain system call or something
> caught things that the general fuzz tester had not caught.
>
> 3) Complete correctness proofs of programs are outside the competence
> of nearly all programmers (and pretty pointless, because they would
> prove only the correctness wrt the specification, which itself may be
> buggy).
>
> Now, to write a C program that is guaranteed to never exercise
> undefined behaviour requires competences on the level 3.
Not in the slightest. Consider the following piece of C code :
int is_leap_year(unsigned int year) {
return 1 ;
}
It's trivial to see that this is defined but , judging from the function's
name , it's almost certainly buggy. A complete correctness proof is many
orders of magnitude harder than simply ensuring defined behaviour.
> The
> much-hyped sanitizers of GCC and Clang allow finding some (not all)
> undefined behaviours using the well-established testing methodology.
>
> So you will find undefined behaviours in the cases exercized by normal
> users, but you will tend not to find undefined behaviour in those
> cases exercized by an attacker; it's as difficult as finding the all
> the vulnerabilities in the first place. E.g., in the OpenSSH case, if
> you thought about the vulnerability, you would fix it right away,
> rather than writing a test case that exploited it, and waiting for the
> sanitizer to report that freed memory was accessed (if the sanitizer
> actually does check that), and then fixing it.
The best write-up I could find on the vulnerability is at
https://www.qualys.com/2016/01/14/cve-2016-0777-cve-2016-0778/openssh-cve-2016-0777-cve-2016-0778.txt .
The crucial bug occurred much earlier than compiler optimisations eliminating
code which wrote 0's on some memory. From the previous link
- "out_start == out_last" (lines 205-206): no data was ever written to
out_buf (and both out_start and out_last are still equal to 0) because
no data was ever sent to the server after roaming_reply() was called,
but the client sends (leaks) the entire uninitialized out_buf to the
server (line 214), as if out_buf_size bytes of data were available.
This would still be a bug (albeit a less serious one) even if the memory had
been zeroed because it sends bogus information to the server. An analogous
bug would be sending over the network unencrypted data which should have been
encrypted. In both cases , to see the bugs one needs to think on the level of
what the application wants and does not want to do , not on the low level
details of the programming language. Some low level detail may accidentally
eliminate some bug caused by a high level thinking oversight but this is
entirely random so it could just as well make it worse.
Another bug was with not handling correctly C arithmetic (see the page).
Finally the not zeroing of memory happened because (from the link)
Unfortunately, an optimizing compiler may remove this
memset() or bzero() call, because the buffer is written to, but never
again read from (an optimization known as Dead Store Elimination).
so it's not due to undefined behaviour. So your reasoning is totally wrong both
in terms of the large picture *and* the details.
> >I'd be tempted to allocate all of Forth's data space into a single
> >char array, and implement ALLOCATE with a custom allocator in that
> >space.
>
> That's "easy" in your book? The resulting Forth system would be
> severely restricted: E.g., you cannot use it to call system calls like
> mmap() and make use of the results (but then, that's undefined
> in the C standard anyway).
>
> > That fits nicely with Forth's flat memory space. But it
> >certainly could be done with malloc(), although care would have to be
> >taken not to hit UB comparing pointers to malloc'd data and Forth's
> >data space.
>
> Right. Anything but "not difficult"; I don't think it's possible.
> Subtraction is also a problem.
>
> >> How do you implement @ and C@?
> >
> >Simple memory reads.
>
> What C code?
>
> >It's legitimate to alias character types and
> >other types, so a suitably aligned character address can be cast to a
> >size_t* or a uintptr_t*.
>
> That contradicts things I have read about accessing casted pointers.
I couldn't tell you off the top of my head but I'm sure you could get the
answer on comp.lang.c very quickly. Looking at the big picture , it could
be that C is not a suitable back-end for Forth after all even if you got
lucky for a number of years and your code (which presumably was exhibiting
SUB) worked as intended. Note that this may turn out to be an opportunity for
Forth : it may be that Forth itself is a more suitable back-end than C for other
programming languages and if so then this needs to be advertised. A
*constructive* thing to do (as opposed to complaining) would be to describe
what guarantees with regard to C pointer comparisons on top of the C standard
would be needed to do what you want to do. Then you could ask on comp.lang.c
or some compiler mailing list whether these additional guarantees can be
offered by using some appropriate flag and if not how easy would be to implement
them as an extension.
> >I think it'd probably make the most sense to use uintptr_t for Forth
> >cells. Of course, this requires a system to be able to cast freely
> >between uintptr_t and and pointer types, but that is implementation-
> >defined rather than undefined behaviour. Every C compiler I care
> >about (or, in fact, know about) supports it.
>
> It's interesting how quick you come off your high horse once things
> like writing actual C code come into play. "It works as intended on
> the compilers and/or machines the programmer used" has been my
> yardstick for determining the correctness of programs all along, yet
> nasal demon fans insist that most (possibly all) of these programs are
> "buggy".
He didn't get off any high horse. Implementation defined behaviour is
stronger than "It works as intended on the compilers and/or machines the
programmer used" which may simply be by accident (and if it's SUB then it
almost certainly is by accident). As for this being your yardstick , that's
just shocking especially coming from someone who teaches computer science and
would be expected to teach students correct thinking. Testing is a necessary
but not sufficient condition to trust code : one must also have abstract
reasons (i.e. reasons which follow from some standard , specification or
relevant documentation) to think that the code will behave as intended.
Otherwise it's just programming superstition.
And speaking of "nasal demon fans" , I don't think such a thing exists.
Undefined behaviour is an unfortunate side effect of 3 factors :
1. The desire to allow implementors optimisations.
2. Inability to reconcile previous (i.e. before the standard) existing practices
therefore any attempt to define the behaviour more narrowly would unfairly
privilege some implementations (or architectures) over others.
3. The desire to not make the standard too large.
(Note that the above 3 factors apply to most programming languages , not just
C.) But noone *likes* undefined behaviour , it is just a trade off. The talk
of nasal demons is to drive home the point (especially to new programmers)
that when dealing with undefined behaviour (that is SUB) there's no
"reasonable" behaviour one can expect therefore *** Just say no *** .If
programmers get convinced to avoid undefined behaviour then this ultimately
will make code more predictable not less. But then there are always some
stubborn ones like yourself or
http://www.open-chess.org/viewtopic.php?f=5&t=2519 where Robert Hyatt
insists that SUB should still do what he wants just because it did in the past.
--
I can tell what you're thinking. Did he click Send or Save Now? Well, to tell you the
truth, in all the excitement of composing that angry email, I kind of lost track myself.
Good thing we can easily undo a sent mail! Oh wait, we totally can't.
https://blog.codinghorror.com/the-opposite-of-fitts-law/
[toc] | [prev] | [next] | [standalone]
| From | Joel Rees <joel.rees@gmail.com> |
|---|---|
| Date | 2017-04-06 18:42 -0700 |
| Message-ID | <2e244166-da19-410e-9f13-332e1c0fc5b8@googlegroups.com> |
| In reply to | #56789 |
On Friday, April 7, 2017 at 3:48:57 AM UTC+9, Spiros Bousbouras wrote:
> On Wed, 05 Apr 2017 15:01:45 GMT
> anton(something)@(something).(something)(Anton Ertl) wrote:
> > Andrew Haley <andrew(something)@(something).(something)> writes:
> >
> > Translating Forth into traditional C (that compiles as intended by PCC
> > and early versions of GCC) is indeed not difficult; after all,
> > traditional C and Forth are semantically close to each other. Take a
> > look at Gforth or forth2c to get an idea on how to do it.
> >
> > The resulting code is, of course, full of undefined behaviour, like
> > most of the other C code around; and in this case I think it's
> > impossible to get rid of the undefined behaviour without losing
> > functionality and performance, and even if you are willing to pay that
> > price, it requires significantly more effort, and in the end, you will
> > probably still have some undefined behaviour somewhere.
>
> Here we need to make a distinction : I will term "weak undefined behaviour"
> (WUB) C code which is not defined according to the C standard and "strong
> undefined behaviour" (SUB) C code which is not defined according to
> *anything* where "anything" could mean some standard which enhances the C
> standard (like POSIX) and also relevant documentation of the compiler or
> libraries one uses or whatever.
I'm not up-to-date on the C standard. Does the standard make the same distinction?
If not, sorry to be a demon breather of human languages, but you just introduced UB into the discussion.
> Our main conern here is predictable behaviour
> of the code so I believe the deciding concept is SUB rather than WUB.
And who do you represent in making that the deciding concept?
> So if
> "The resulting code is, of course, full of undefined behaviour" means WUB
> then that's probably correct (there's a lot of useful stuff you can't do just
> by <C according to the standard>) but if you mean SUB then I doubt it. In any
> case , if code has SUB then I cannot imagine on what basis one may think it
> works and it will reliably continue to do so in the future : even if it
> passes testing , then that's by coincidence. So if a code exhibits SUB then
> it's buggy and it needs to be fixed.
Having criticized you for making the distinction, I'll agree with your intent, partially. But only if you go look up my bif-c project and read the header file that I use to clear the problems Anton is frustrated about, and the configuration code I use to generate that header file. (... which I now discover, on current 64 bit machines, has some potential UB that occurs because the compiler writers have trouble understanding whether a C int should ever be 64 bits on a nominally 64 bit architecture, and make an assumption that didn't match mine, and I'm still not sure their assumption matches the future realities better than mine.)
And then you may contemplate how that header perverts some of the hidden corners of my interpreter, and whether the bugs it introduces now are worth the reward of illuminating those corners some years from now when I can finally turn my attention back to the code for a day or two.
> > In general, programming is not easy, but there are different levels of
> > difficulty:
> >
> > 1) Programmers tend to be able to satisfy the requirements that the
> > users use a lot, and/or care about a lot. Corner cases, less so (and
> > in the Forth community, some people celebrate being wrong in corner
> > cases, no matter how easy it would have been to do the right thing;
> > actually, that's very similar to the attitude that gives us nasal
> > demons).
> >
> > 2) Programmers are pretty bad at dealing with cases that do not occur
> > during the course of normal operations. That's why security
> > vulnerabilities occur so often and are so long-lived. Writing tests
> > for unusual cases helps a little, but only shines a light on the cases
> > that are tested. There is no guarantee that tests cover everything.
> > Even with automated fuzz testing these days, the amount of automation
> > is limited: a specialized setup for a certain system call or something
> > caught things that the general fuzz tester had not caught.
> >
> > 3) Complete correctness proofs of programs are outside the competence
> > of nearly all programmers (and pretty pointless, because they would
> > prove only the correctness wrt the specification, which itself may be
> > buggy).
> >
> > Now, to write a C program that is guaranteed to never exercise
> > undefined behaviour requires competences on the level 3.
>
> Not in the slightest. Consider the following piece of C code :
>
> int is_leap_year(unsigned int year) {
> return 1 ;
> }
>
> It's trivial to see that this is defined but , judging from the function's
> name , it's almost certainly buggy. A complete correctness proof is many
> orders of magnitude harder than simply ensuring defined behaviour.
But that doesn't mean that correctness is any closer to being achievable.
Rather, it requires the compiler writers (and standards committees) to act on a level that is a bit beyond mere hero -- perhaps a worthy goal, but not achievable.
> > The
> > much-hyped sanitizers of GCC and Clang allow finding some (not all)
> > undefined behaviours using the well-established testing methodology.
> >
> > So you will find undefined behaviours in the cases exercized by normal
> > users, but you will tend not to find undefined behaviour in those
> > cases exercized by an attacker; it's as difficult as finding the all
> > the vulnerabilities in the first place. E.g., in the OpenSSH case, if
> > you thought about the vulnerability, you would fix it right away,
> > rather than writing a test case that exploited it, and waiting for the
> > sanitizer to report that freed memory was accessed (if the sanitizer
> > actually does check that), and then fixing it.
>
> The best write-up I could find on the vulnerability is at
> https://www.qualys.com/2016/01/14/cve-2016-0777-cve-2016-0778/openssh-cve-2016-0777-cve-2016-0778.txt .
>
> The crucial bug occurred much earlier than compiler optimisations eliminating
> code which wrote 0's on some memory. From the previous link
>
> - "out_start == out_last" (lines 205-206): no data was ever written to
> out_buf (and both out_start and out_last are still equal to 0) because
> no data was ever sent to the server after roaming_reply() was called,
> but the client sends (leaks) the entire uninitialized out_buf to the
> server (line 214), as if out_buf_size bytes of data were available.
>
> This would still be a bug (albeit a less serious one) even if the memory had
> been zeroed because it sends bogus information to the server. An analogous
> bug would be sending over the network unencrypted data which should have been
> encrypted. In both cases , to see the bugs one needs to think on the level of
> what the application wants and does not want to do , not on the low level
> details of the programming language. Some low level detail may accidentally
> eliminate some bug caused by a high level thinking oversight but this is
> entirely random so it could just as well make it worse.
>
> Another bug was with not handling correctly C arithmetic (see the page).
> Finally the not zeroing of memory happened because (from the link)
>
> Unfortunately, an optimizing compiler may remove this
> memset() or bzero() call, because the buffer is written to, but never
> again read from (an optimization known as Dead Store Elimination).
>
> so it's not due to undefined behaviour. So your reasoning is totally wrong both
> in terms of the large picture *and* the details.
I'm shooting from the hip, and my memory is sure to be faulty, but my memory is that the compiler's assumption that this was valid dead store elimination was derived from an interpretation elsewhere of UB.
Now, there is a potential for conflating the general principle of UB with the dead-code optimizations that became significantly more aggressive around that time.
But I'm not sure the conflation is entirely spurious.
K&R C and the first ANSI standard acknowledged that a compiler should never try to interpret too far beyond a pointer, because, especially in a multiprocessing run-time, the compiler had no way of knowing what was happening to the memory being pointed to when the code was not accessing it.
Microsoft insisted they could predict such things in their OS. We know why. We also know what happens later.
Intel makes their market by helping Microsoft do stupid things. So Intel wants us to believe Microsoft's charismatic delusions of omnipotence, and they find it convenient to optimize their hardware to do so. And fudge around the problems with the next shrink in the die and the accompanying speed bump, which, by the way, hasn't happened in several years, and, by the way, is a significant part of the motivation for trying to get the compiler to juice every last ounce of performance from a CPU that has serious bugs in its spec.
In other words, from one point of view, the question of dead store is not separable from the question of what happens when a pointer to undefined memory is sniffed (which is one of the bogies of UB) or of what happens when a pointer to an object in one allocation area is compared to a pointer to an object in another allocation area (which is another).
(Yes, I still grudge Intel those four-bit pointer jaggies, along with the imposition of the LSB addressing perversion. We are finally becoming able, as an industry, to describe why Intel was wrong when they said it wouldn't matter, but we now have a huge burden of false assumptions in an entire industry to overcome, to get rid of the effects of those two specific false optimizations.)
> > >I'd be tempted to allocate all of Forth's data space into a single
> > >char array, and implement ALLOCATE with a custom allocator in that
> > >space.
> >
> > That's "easy" in your book? The resulting Forth system would be
> > severely restricted: E.g., you cannot use it to call system calls like
> > mmap() and make use of the results (but then, that's undefined
> > in the C standard anyway).
> >
> > > That fits nicely with Forth's flat memory space. But it
> > >certainly could be done with malloc(), although care would have to be
> > >taken not to hit UB comparing pointers to malloc'd data and Forth's
> > >data space.
> >
> > Right. Anything but "not difficult"; I don't think it's possible.
> > Subtraction is also a problem.
> >
> > >> How do you implement @ and C@?
> > >
> > >Simple memory reads.
> >
> > What C code?
> >
> > >It's legitimate to alias character types and
> > >other types, so a suitably aligned character address can be cast to a
> > >size_t* or a uintptr_t*.
> >
> > That contradicts things I have read about accessing casted pointers.
>
> I couldn't tell you off the top of my head but I'm sure you could get the
> answer on comp.lang.c very quickly. Looking at the big picture , it could
> be that C is not a suitable back-end for Forth after all even if you got
> lucky for a number of years and your code (which presumably was exhibiting
> SUB) worked as intended.
I'll again refer you to the source code for my bif-c project, the same place I mentioned above.
There are some extent bugs in my source code which are derived from something in that huge union I made to get around the problem Anton is pointing at. And I kind of implied it above, but that union is itself a straitjacket that prevented me from pushing that project forward into the realm of production-usable code.
Maybe, if I'd been able to get someone to pay me while I thought about it, I could have found a way around the straitjacket.
As it was, getting it that far took time away from my family which my children are now paying for. (And I am paying for in terms of going back to help them learn things now that I should have been helping them learn when they were much younger. I'm fortunate to have the chance to do so. Not all engineers who are parents end up having the chance.)
> Note that this may turn out to be an opportunity for
> Forth : it may be that Forth itself is a more suitable back-end than C for other
> programming languages and if so then this needs to be advertised.
One of the hidden features of Forth is the difficulty of imposing a standard on any level of the language families. It would be nice, perhaps, but it would have to have a different name than Forth.
Uhm, they would have different names than Forth.
(Which is really the solution that should have been used with C -- split the standard into three or more separate languages with separate target classes of run-time environments. If C had a split context stack like Forth, and kept its symbol table on-line like Forth, and provided default access to the debugger like Forth, and had a per-user segment like many versions of Forth, etc., maybe it would have been more obvious that they shouldn't be trying to conflate all the standards into one.)
> A
> *constructive* thing to do (as opposed to complaining) would be to describe
> what guarantees with regard to C pointer comparisons on top of the C standard
> would be needed to do what you want to do. Then you could ask on comp.lang.c
> or some compiler mailing list whether these additional guarantees can be
> offered by using some appropriate flag and if not how easy would be to implement
> them as an extension.
I think that was what he was trying to do. Didn't you see that when you read his paper?
The prragmas have generally been available in the past. Some of them are no longer available, due to the insistence that standard-undefined behavior is equivalent to non-existing behavior. (See the confusion about the SSH bug you mention above. The authors of ssh are no less critical of the arrogance of the current batch of compiler engineers than Anton, and if you were looking for a group who understand the implications of compiler semantics on security, the authors of ssh are about as qualified as any group of engineers on the planet. BTW, the authors of ssh were never confused about this. The compiler engineers have just plain gone random.)
> > >I think it'd probably make the most sense to use uintptr_t for Forth
> > >cells. Of course, this requires a system to be able to cast freely
> > >between uintptr_t and and pointer types, but that is implementation-
> > >defined rather than undefined behaviour. Every C compiler I care
> > >about (or, in fact, know about) supports it.
> >
> > It's interesting how quick you come off your high horse once things
> > like writing actual C code come into play. "It works as intended on
> > the compilers and/or machines the programmer used" has been my
> > yardstick for determining the correctness of programs all along, yet
> > nasal demon fans insist that most (possibly all) of these programs are
> > "buggy".
>
> He didn't get off any high horse. Implementation defined behaviour is
> stronger than "It works as intended on the compilers and/or machines the
> programmer used" which may simply be by accident (and if it's SUB then it
> almost certainly is by accident
When a pointer was an integer, what worked because a pointer was an integer was not by accident.
Pointers are still integers.
We, as a community have some deeper understanding about the nature of integers than we did before.
But the standards have declared now that pointers are not integers compatible with computation integers, and that makes problems, and if the compiler engineers keep dumping code that is UB under the assumption that pointers are not integers, well, in several years, all C compilers will be very quick.
Every program will compile to NOOP.
> ). As for this being your yardstick , that's
> just shocking especially coming from someone who teaches computer science and
> would be expected to teach students correct thinking. Testing is a necessary
> but not sufficient condition to trust code : one must also have abstract
> reasons (i.e. reasons which follow from some standard , specification or
> relevant documentation) to think that the code will behave as intended.
> Otherwise it's just programming superstition.
Abstract vs. real. Where do you set the fulcrum to get the balance?
Balance is the wrong question. Having both halfway doesn't really work very well.
> And speaking of "nasal demon fans" , I don't think such a thing exists.
I'm guessing he gets that idiom from a more polite restatement of the monkeys flying out of the dark place idiom that was used as the general proxy symbol for talking about UB in certain subgroups of our industry in the not-so-distant past.
> Undefined behaviour is an unfortunate side effect of 3 factors :
>
> 1. The desire to allow implementors optimisations.
Restated as Intel's need to find some way to keep claiming that their patent-laden archaic architecture can still be kept up to speed, if nothing else.
> 2. Inability to reconcile previous (i.e. before the standard) existing practices
> therefore any attempt to define the behaviour more narrowly would unfairly
> privilege some implementations (or architectures) over others.
An unwillingness to acknowledge that the requirements of various industries who have found a commonality in C now need to refine their interests in the common language.
> 3. The desire to not make the standard too large.
What?
It was already too large as of ANSI C.
> (Note that the above 3 factors apply to most programming languages , not just
> C.) But noone *likes* undefined behaviour , it is just a trade off.
So every application program now has to correctly guide rockets into orbit, correctly interpret inane tax law, correctly play chess, correctly diagnose your mother's health issues, correctly perform open-heart surgery on my friend, and correctly tend the baby in the nursery? (Just for starters.)
If we can't learn to deal with context, we are, as a society and a race, completely unworthy of the technologies that allow us to define anything beyond a context-free grammar.
> The talk
> of nasal demons is to drive home the point (especially to new programmers)
> that when dealing with undefined behaviour (that is SUB) there's no
> "reasonable" behaviour one can expect therefore *** Just say no *** .
Why should admitting that pointers are integers be equated with random unprotected sex or crack cocaine?
> If
> programmers get convinced to avoid undefined behaviour then this ultimately
> will make code more predictable not less. But then there are always some
> stubborn ones like yourself or
> http://www.open-chess.org/viewtopic.php?f=5&t=2519 where Robert Hyatt
> insists that SUB should still do what he wants just because it did in the past.
>
> --
> I can tell what you're thinking. Did he click Send or Save Now? Well, to tell you the
> truth, in all the excitement of composing that angry email, I kind of lost track myself.
> Good thing we can easily undo a sent mail! Oh wait, we totally can't.
> https://blog.codinghorror.com/the-opposite-of-fitts-law/
Is that your siggy?
Are you even subliminally aware of the irony implicit?
--
Joel Rees
http://reiisi.blogspot.com
[toc] | [prev] | [next] | [standalone]
| From | Andrew Haley <andrew29@littlepinkcloud.invalid> |
|---|---|
| Date | 2017-04-07 04:02 -0500 |
| Message-ID | <OtednXt3y5cIyHrFnZ2dnUU7-eWdnZ2d@supernews.com> |
| In reply to | #56796 |
Joel Rees <joel.rees@gmail.com> wrote: > > K&R C and the first ANSI standard acknowledged that a compiler > should never try to interpret too far beyond a pointer, because, > especially in a multiprocessing run-time, the compiler had no way of > knowing what was happening to the memory being pointed to when the > code was not accessing it. I don't believe it. Chapter and verse of the first ANSI standard, please. Andrew.
[toc] | [prev] | [next] | [standalone]
| From | Joel Rees <joel.rees@gmail.com> |
|---|---|
| Date | 2017-04-08 21:18 -0700 |
| Message-ID | <cbeec18c-d0ee-4b89-8a85-e2c7720854fb@googlegroups.com> |
| In reply to | #56807 |
On Friday, April 7, 2017 at 6:02:19 PM UTC+9, Andrew Haley wrote: > Joel Rees <joel.rees@(something).(something)> wrote: > > > > K&R C and the first ANSI standard acknowledged that a compiler > > should never try to interpret too far beyond a pointer, because, > > especially in a multiprocessing run-time, the compiler had no way of > > knowing what was happening to the memory being pointed to when the > > code was not accessing it. > > I don't believe it. Chapter and verse of the first ANSI standard, > please. > > Andrew. I might be misremembering just when they decided to allow Microsoft to pretend that it is possible to always know what a pointer is pointing at. It might have been ANSI C that provided the volatile keyword to specifically prevent the compiler from looking deeper than it should. There was, of course, no standard for K&R, but quite a lot of discussion concerning optimization lamented the fact that C pointers could point to hardware registers and shared data and other things that could change behind the compiler's back. And that therefore, ForTran allowed parallel processing on array elements where C did not. It would have been far more correct, and have postponed a lot of standard-rot, to have provided, instead, a "non-volatile" keyword to tell the compiler it could decide it wouldn't need to repeat a dereference of such as pixels[ 10 ] every time it occurred. Local optimizations are much safer and can be tightened to a far greater degree than global optimizations. -- Joel Rees
[toc] | [prev] | [next] | [standalone]
| From | Spiros Bousbouras <spibou@gmail.com> |
|---|---|
| Date | 2017-04-08 22:43 +0000 |
| Message-ID | <iIdGA.333623$2K7.288660@fx18.am4> |
| In reply to | #56796 |
On Thu, 6 Apr 2017 18:42:30 -0700 (PDT) Joel Rees <joel.rees@gmail.com> wrote: I'll give a more complete answer tomorrow but for the time being... > Having criticized you for making the distinction, I'll agree with your intent, > partially. But only if you go look up my bif-c project and read the header file that > I use to clear the problems Anton is frustrated about, and the configuration code I > use to generate that header file. (... which I now discover, on current 64 bit > machines, has some potential UB that occurs because the compiler writers have > trouble understanding whether a C int should ever be 64 bits on a nominally 64 bit > architecture, and make an assumption that didn't match mine, and I'm still not sure > their assumption matches the future realities better than mine.) You could have provided a link you know. I will guess that you mean https://sourceforge.net/projects/bif-c/files/latest/download .But I see several *.h files so I don't know what "the header file" is. Also if you want my input you must explain which parts of your code correspond to which of Anton's complaints. Surely you don't expect me to try all possible combinations of lines in your code with claims in Anton's paper and see if I come up with a match which makes sense. By the way , README.TXT seems to be missing text at the end (assuming I got the correct download).
[toc] | [prev] | [next] | [standalone]
| From | Joel Rees <joel.rees@gmail.com> |
|---|---|
| Date | 2017-04-08 20:54 -0700 |
| Message-ID | <c0faf2e3-2355-418a-9b5e-085f161a5ce9@googlegroups.com> |
| In reply to | #56880 |
On Sunday, April 9, 2017 at 7:43:28 AM UTC+9, Spiros Bousbouras wrote:
> On Thu, 6 Apr 2017 18:42:30 -0700 (PDT)
> Joel Rees <joel.rees@(something).(something)> wrote:
>
> I'll give a more complete answer tomorrow but for the time being...
>
> > Having criticized you for making the distinction, I'll agree with your intent,
> > partially. But only if you go look up my bif-c project and read the header file that
> > I use to clear the problems Anton is frustrated about,
Sorry, I had forgotten that I had not finished moving that part of the code into more meaningfully named files.
The union is in
https://sourceforge.net/p/bif-c/code/52/tree/trunk/bifu_i.h
> > and the configuration code I
> > use to generate that header file.
The configurations are in configs/celltype.h, which is generated by
https://sourceforge.net/p/bif-c/code/52/tree/trunk/configs/makecelltype.c
> > (... which I now discover, on current 64 bit
> > machines, has some potential UB that occurs because the compiler writers have
> > trouble understanding whether a C int should ever be 64 bits on a nominally 64 bit
> > architecture, and make an assumption that didn't match mine, and I'm still not sure
> > their assumption matches the future realities better than mine.)
>
> You could have provided a link you know.
8-*
> I will guess that you mean
> https://sourceforge.net/projects/bif-c/files/latest/download .But I see
> several *.h files so I don't know what "the header file" is. Also if
> you want my input you must explain which parts of your code correspond
> to which of Anton's complaints. Surely you don't expect me to try all
> possible combinations of lines in your code with claims in Anton's paper
> and see if I come up with a match which makes sense.
I had intended to move it into either biftypes.h or bifsym.h, and ran out of time while I was holding a debate with myself on the question. (No one else has joined the project, so I have to debate such things with myself, you see. ;)
> By the way , README.TXT seems to be missing text at the end (assuming I got
> the correct download).
Hmm. Now I need to make some time to do some magnetic domain dumpster diving. Or maybe just write a new readme, since the plans I had then are now quite apparently unachievable.
I assume you will do the make in config/, to get the generated header. For the list, the generated header looks like this on my AMD64 running Debian Wheezy, compiled with gcc 4.7.2:
----------------------------
/*
** celltype.h
** bif-c
**
** Template created by Joel Rees on 2013/06/18.
** Copyright 2013 __Reiisi_Kenkyuu__. All rights reserved.
**
** Type information for cell proto-type.
*/
#if !defined CELLTYPE_H /* recursive inclusion blocker */
#define CELLTYPE_H
typedef char * prCharPtr_p;
typedef void * prVoidPtr_p;
typedef void (* icode_f )( void );
#define PROBE_POINTER_BYTE 8
#define PROBE_POINTER_BIT 64
#define PROBE_POINTER_TYPE icode_f
typedef unsigned char ubyte_t;
typedef signed char sbyte_t;
/* For now, assuming two's complement: */
#define UBYTE_MAX ((ubyte_t) 0xff)
#define BITSPERBYTE 8
#define BYTE_HIGH_BIT ((ubyte_t) 0x80)
#define SBYTE_MAX ((sbyte_t) 0x7f)
#define SBYTE_MIN ((sbyte_t) BYTE_HIGH_BIT)
typedef unsigned short ushortw_t;
typedef signed short sshortw_t;
/* For now, assuming two's complement: */
#define USHORTW_MAX ((ushortw_t) 0xffff)
#define BITSPERSHORTW 16
#define SHORTW_HIGH_BIT ((ushortw_t) 0x8000)
#define SSHORTW_MAX ((sshortw_t) 0x7fff)
#define SSHORTW_MIN ((sshortw_t) SHORTW_HIGH_BIT)
typedef unsigned int uintw_t;
typedef signed int sintw_t;
/* For now, assuming two's complement: */
#define UINTW_MAX ((uintw_t) 0xffffffff)
#define BITSPERINTW 32
#define INTW_HIGH_BIT ((uintw_t) 0x80000000)
#define SINTW_MAX ((sintw_t) 0x7fffffff)
#define SINTW_MIN ((sintw_t) INTW_HIGH_BIT)
typedef unsigned long ulongw_t;
typedef signed long slongw_t;
/* For now, assuming two's complement: */
#define ULONGW_MAX ((ulongw_t) 0xffffffffffffffffL)
#define BITSPERLONGW 64
#define LONGW_HIGH_BIT ((ulongw_t) 0x8000000000000000L)
#define SLONGW_MAX ((slongw_t) 0x7fffffffffffffffL)
#define SLONGW_MIN ((slongw_t) LONGW_HIGH_BIT)
/* *** long long type supported on this architecture. *** */
typedef unsigned long long ullongw_t;
typedef signed long long sllongw_t;
/* For now, assuming two's complement: */
#define ULLONGW_MAX ((ullongw_t) 0xffffffffffffffffLL)
#define BITSPERLLONGW 64
#define LLONGW_HIGH_BIT ((ullongw_t) 0x8000000000000000LL)
#define SLLONGW_MAX ((sllongw_t) 0x7fffffffffffffffLL)
#define SLLONGW_MIN ((sllongw_t) LLONGW_HIGH_BIT)
#define SINGLE_C_CELL_DOUBLE
/* This is the primitive cell,
** not the target cell.
*/
typedef slongw_t probe_scell_t;
typedef ulongw_t probe_ucell_t;
#define PROBE_CELL_BYTE 8
#define PROBE_CELL_BIT BITSPERLONGW
#define PROBE_CELL_HIGH_BIT ((probe_ucell_t) LONGW_HIGH_BIT)
#define PROBE_UCELL_MAX ((probe_ucell_t) ULONGW_MAX)
#define PROBE_SCELL_MAX ((probe_scell_t) SLONGW_MAX)
#define PROBE_SCELL_MIN ((probe_scell_t) SLONGW_MIN)
/* A manufactured double has to be constructed on the target.
** All we can do here is provide the context.
**
** Cells are never smaller than C int.
*/
#endif /* defined CELLTYPE_H recursive inclusion blocker */
---------------------
--
Joel Rees
http://reiisi.blogspot.jp/p/novels-i-am-writing.html
[toc] | [prev] | [next] | [standalone]
| From | anton@mips.complang.tuwien.ac.at (Anton Ertl) |
|---|---|
| Date | 2017-04-09 14:53 +0000 |
| Message-ID | <2017Apr9.165301@mips.complang.tuwien.ac.at> |
| In reply to | #56789 |
Spiros Bousbouras <spibou@gmail.com> writes:
>On Wed, 05 Apr 2017 15:01:45 GMT
>anton@mips.complang.tuwien.ac.at (Anton Ertl) wrote:
>> Andrew Haley <andrew29@littlepinkcloud.invalid> writes:
>>
>> Translating Forth into traditional C (that compiles as intended by PCC
>> and early versions of GCC) is indeed not difficult; after all,
>> traditional C and Forth are semantically close to each other. Take a
>> look at Gforth or forth2c to get an idea on how to do it.
>>
>> The resulting code is, of course, full of undefined behaviour, like
>> most of the other C code around; and in this case I think it's
>> impossible to get rid of the undefined behaviour without losing
>> functionality and performance, and even if you are willing to pay that
>> price, it requires significantly more effort, and in the end, you will
>> probably still have some undefined behaviour somewhere.
>
>Here we need to make a distinction : I will term "weak undefined behaviour"
>(WUB) C code which is not defined according to the C standard and "strong
>undefined behaviour" (SUB) C code which is not defined according to
>*anything* where "anything" could mean some standard which enhances the C
>standard (like POSIX) and also relevant documentation of the compiler or
>libraries one uses or whatever. Our main conern here is predictable behaviour
>of the code so I believe the deciding concept is SUB rather than WUB.
I don't think that this distinction helps in this discussion, because
1) Different people consider different things to be "not defined
according to *anything*". E.g., assembly language and most Forth
programmers consider signed integer overflow to have a pretty
natural definition (wraparound aka modulo arithmetics), some more
mathematically-inclined people think they deserve nasal demons.
2) Nasal demon fans want license to produce nasal demons for every
undefined behaviour. E.g., in the general case both gcc and
Clang/LLVM generate code for 2s-complement arithmetic with
wraparound for signed integer addition, subtraction, and
multiplication, so you might classify it as WUB. Nasal demon fans
still want to keep signed integer overflow undefined even in those
compilers so that they make use of it for "optimizations".
3) People aware of the evils of nasal demons don't want them anywhere,
no matter what undefined behaviour there is. E.g., for an
out-of-bounds array read, I expect either an unspecified, but
stable value, or a segmentation violation/general protection fault;
that's not fully defined, but it excludes nasal demons. E.g., I
don't expect it to turn a counted loop into an endless loop (and
this is actually a nasal demon "optimization" that occurs in
practice).
>In any
>case , if code has SUB then I cannot imagine on what basis one may think it
>works and it will reliably continue to do so in the future : even if it
>passes testing , then that's by coincidence. So if a code exhibits SUB then
>it's buggy and it needs to be fixed.
Of course that depends on what you consider SUB. Anyway, here's an
example.
int d[16];
int SATD (void)
{
int satd = 0, dd, k;
for (dd=d[k=0]; k<16; dd=d[++k]) {
satd += (dd < 0 ? -dd : dd);
}
return satd;
}
If there is some other global data defined earlier and later in the
program, then d[16] is a mapped (i.e., readable) memory location. And
if it is an unmapped memory location, you get a SIGSEGV, not some
nasal demon.
>> 3) Complete correctness proofs of programs are outside the competence
>> of nearly all programmers (and pretty pointless, because they would
>> prove only the correctness wrt the specification, which itself may be
>> buggy).
>>
>> Now, to write a C program that is guaranteed to never exercise
>> undefined behaviour requires competences on the level 3.
>
>Not in the slightest. Consider the following piece of C code :
>
> int is_leap_year(unsigned int year) {
> return 1 ;
> }
>
>It's trivial to see that this is defined but , judging from the function's
>name , it's almost certainly buggy. A complete correctness proof is many
>orders of magnitude harder than simply ensuring defined behaviour.
I don't think it is trivial to see that this is defined. I once
<2015May1.155805@mips.complang.tuwien.ac.at> wrote:
|It seems to me that
|
| if ((size_t)(dest-src) < len)
|
|is a more efficient way to test whether dest is inside [src, src+len).
|
|Of course, since this code contains more than three tokens, it is
|likely to contain undefined behaviour
That was mostly in jest, but a post or two later, someone explained
that yes, this code is undefined. So while I do not see anything
undefined about the code you posted, just let the language lawyers at
it, and they will point it out.
In any case, in your example it is trivial to see that it does not
satisfy the requirement that is implied by the name, so even if it
really is trivial to see that it is defined, it only shows that both
correctness and definedness are trivial to determine for trivial
programs.
>> So you will find undefined behaviours in the cases exercized by normal
>> users, but you will tend not to find undefined behaviour in those
>> cases exercized by an attacker; it's as difficult as finding the all
>> the vulnerabilities in the first place. E.g., in the OpenSSH case, if
>> you thought about the vulnerability, you would fix it right away,
>> rather than writing a test case that exploited it, and waiting for the
>> sanitizer to report that freed memory was accessed (if the sanitizer
>> actually does check that), and then fixing it.
>
>The best write-up I could find on the vulnerability is at
>https://www.qualys.com/2016/01/14/cve-2016-0777-cve-2016-0778/openssh-cve-2016-0777-cve-2016-0778.txt .
>
>The crucial bug occurred much earlier than compiler optimisations eliminating
>code which wrote 0's on some memory. From the previous link
>
> - "out_start == out_last" (lines 205-206): no data was ever written to
> out_buf (and both out_start and out_last are still equal to 0) because
> no data was ever sent to the server after roaming_reply() was called,
> but the client sends (leaks) the entire uninitialized out_buf to the
> server (line 214), as if out_buf_size bytes of data were available.
>
>This would still be a bug (albeit a less serious one) even if the memory had
>been zeroed because it sends bogus information to the server. An analogous
>bug would be sending over the network unencrypted data which should have been
>encrypted. In both cases , to see the bugs one needs to think on the level of
>what the application wants and does not want to do , not on the low level
>details of the programming language. Some low level detail may accidentally
>eliminate some bug caused by a high level thinking oversight but this is
>entirely random so it could just as well make it worse.
>
>Another bug was with not handling correctly C arithmetic (see the page).
>Finally the not zeroing of memory happened because (from the link)
>
> Unfortunately, an optimizing compiler may remove this
> memset() or bzero() call, because the buffer is written to, but never
> again read from (an optimization known as Dead Store Elimination).
>
>so it's not due to undefined behaviour.
But actually the bug resulted in reading from the buffer. So the
assumption by the compiler that the buffer is never again read from is
wrong, and applying dead-store elimination to this memset() is wrong;
in other words, the compiler is buggy.
But of course the GCC maintainers don't accept this as a bug: They say
that reading from the buffer after the free() is undefined behaviour,
therefore does not happen, and therefore they are in their rights to
conjure up nasal demons and "optimize" the memset()/bzero() away. And
this is not an issue that could turn out one way or the other, this
memset()/bzero() is there exactly for mitigating information leaks,
such as the one that is the main reason of the CVE.
It is telling that you do not understand how the nasal-demon
interpretation of C allowed the compiler to "optimize" the
memset()/bzero() away. So much for Andrew Haley's claim that it is
"not difficult" to write "well-defined" C, and your defense of that
stance.
>I couldn't tell you off the top of my head but I'm sure you could get the
>answer on comp.lang.c very quickly. Looking at the big picture , it could
>be that C is not a suitable back-end for Forth after all even if you got
>lucky for a number of years and your code (which presumably was exhibiting
>SUB) worked as intended.
I think that nasal-demon C is not a suitable language for anything.
> Note that this may turn out to be an opportunity for
>Forth : it may be that Forth itself is a more suitable back-end than C for other
>programming languages
Yes.
>A
>*constructive* thing to do (as opposed to complaining) would be to describe
>what guarantees with regard to C pointer comparisons on top of the C standard
>would be needed to do what you want to do. Then you could ask on comp.lang.c
>or some compiler mailing list whether these additional guarantees can be
>offered by using some appropriate flag and if not how easy would be to implement
>them as an extension.
If you think that's a promising approach, go ahead. My experience is
that they always tell you to go to the C standards committee.
>Undefined behaviour is an unfortunate side effect of 3 factors :
>
>1. The desire to allow implementors optimisations.
>2. Inability to reconcile previous (i.e. before the standard) existing practices
> therefore any attempt to define the behaviour more narrowly would unfairly
> privilege some implementations (or architectures) over others.
>3. The desire to not make the standard too large.
That was all fine and dandy in the good old days of PCC and early GCC,
but in recent years the compiler maintainers went insane and use them
as justification for miscompiling (they call it "optimizing") as many
programs as possible, with some exceptions, in particular, standard
benchmarks. Paying customers are probably also not treated as badly
as the rest of us; hmm, so nasal demons may be part of the business
models.
> But noone *likes* undefined behaviour , it is just a trade off.
The GCC and Clang compiler maintainers love it. For them reason 2 and
3 don't apply, yet with every release they miscompile more and more
cases that are undefined in the standard for reasons 2 and 3; e.g.,
signed integer overflow.
>If
>programmers get convinced to avoid undefined behaviour then this ultimately
>will make code more predictable not less.
So you love nasal demons, too.
Many programmers are convinced. But because there is actually no good
way to write code without undefined behaviour, we will get programs by
convinced programmers that have fewer undefined behaviours, but it
will still be there; and the next release of the compiler breaks some
code, the convinced programmers get busy fixing it, and the next
release breaks some more code. Bottom line: slightly faster
benchmarks, more programs that break, and more work for the C
programmers without any benefit.
Of course, if you are a programmer from a paying customer, you may be
able to exert enough pressure that they don't break your program. Or
if you are a programmer from a company that distributes binaries only,
you just use a compiler version that works, and don't downgrade to
newer versions. It's free software that's written by volunteers that
is hit the hardest by nasal demons. That is probably in line with the
sponsors of Clang/LLVM, but for GCC, I doubt it.
>But then there are always some
>stubborn ones like yourself or
>http://www.open-chess.org/viewtopic.php?f=5&t=2519 where Robert Hyatt
>insists that SUB should still do what he wants just because it did in the past.
So you think that using strcpy to do an overlapping backwards copy is
SUB, i.e., "not defined according to *anything*". Interesting.
- anton
--
M. Anton Ertl http://www.complang.tuwien.ac.at/anton/home.html
comp.lang.forth FAQs: http://www.complang.tuwien.ac.at/forth/faq/toc.html
New standard: http://www.forth200x.org/forth200x.html
EuroForth 2016: http://www.euroforth.org/ef16/
[toc] | [prev] | [next] | [standalone]
| From | Spiros Bousbouras <spibou@gmail.com> |
|---|---|
| Date | 2017-04-10 00:38 +0000 |
| Message-ID | <xuAGA.661090$nT1.467590@fx44.am4> |
| In reply to | #56939 |
[ Crossposted to comp.lang.c since we need some C lawyers ;-) ]
On Sun, 09 Apr 2017 14:53:01 GMT
anton@mips.complang.tuwien.ac.at (Anton Ertl) wrote:
> Spiros Bousbouras <spibou@gmail.com> writes:
> >On Wed, 05 Apr 2017 15:01:45 GMT
> >anton@mips.complang.tuwien.ac.at (Anton Ertl) wrote:
> >> Andrew Haley <andrew29@littlepinkcloud.invalid> writes:
> >>
> >> Translating Forth into traditional C (that compiles as intended by PCC
> >> and early versions of GCC) is indeed not difficult; after all,
> >> traditional C and Forth are semantically close to each other. Take a
> >> look at Gforth or forth2c to get an idea on how to do it.
> >>
> >> The resulting code is, of course, full of undefined behaviour, like
> >> most of the other C code around; and in this case I think it's
> >> impossible to get rid of the undefined behaviour without losing
> >> functionality and performance, and even if you are willing to pay that
> >> price, it requires significantly more effort, and in the end, you will
> >> probably still have some undefined behaviour somewhere.
> >
> >Here we need to make a distinction : I will term "weak undefined behaviour"
> >(WUB) C code which is not defined according to the C standard and "strong
> >undefined behaviour" (SUB) C code which is not defined according to
> >*anything* where "anything" could mean some standard which enhances the C
> >standard (like POSIX) and also relevant documentation of the compiler or
> >libraries one uses or whatever. Our main conern here is predictable behaviour
> >of the code so I believe the deciding concept is SUB rather than WUB.
>
> I don't think that this distinction helps in this discussion, because
>
> 1) Different people consider different things to be "not defined
> according to *anything*". E.g., assembly language and most Forth
> programmers consider signed integer overflow to have a pretty
> natural definition (wraparound aka modulo arithmetics), some more
> mathematically-inclined people think they deserve nasal demons.
I guess I wasn't clear enough. By "anything" I mean anything related to the context.
So if I'm translating some C code (note that "translating" doesn't necessarily mean
compiling ; C is usually compiled but there are C interpreters) relevant stuff are
- C standard.
- Translator documentation. For example by using the appropriate options one may get
additional guarantees beyond the C standard like -fwrapv gcc supports and
which makes signed integer oveflow defined.
- If one uses headers or functions or macros , etc. which do not appear in the C
standard then these must be defined somewhere else like in some other standard
or they must be part of some library and be defined in the documentation of the
library.
- There may more which is relevant. I don't see how Forth or assembly are relevant
unless one calls an external process which is written into one of these languages.
Mathematics is relevant only to the extent that the related documentation or
standard(s) says that it's relevant. For example it follows from the C standard
that for integers x and y of the same type T , if the mathematically correct result
of x+y fits into T then that's what x+y evaluates to. But if it didn't specify
this then one should not have assumed that the mathematical definition of + is
relevant even if they felt that it would be the natural way to define C's +
operator.
The underlying principle is that one must have some rational reason to expect
code to behave in a certain way. For example if I have C code which includes
frooboz(123) ;
I must have have some rational reason to expect this to translate without errors and
do something specific I have in mind. Since the C standard does not define frooboz()
, this reason must come from somewhere else. So we definitely need some stronger
concept than WUB. What counts as "pretty natural definition" for signed integer
oveflow (or anything else) seems subjective to me and I don't even see how it is
relevant whether someone is a Forth programmer or assembly programmer (of which
architecture ?) or mathematically inclined. Even in mathematics , what x+y means
depends on the context. The definition is different if x and y are elements of ℤ
(integers) as opposed to say ℤ/5ℤ .So what is defined in some context depends
on the context rather than the overall knowledge and experiences one has. To get to
one of your favorite examples , if your C code has signed integer oveflow what's
your rational reason to expect that it will do something specific (like wraparound)?
The reason cannot be the C standard because the C standard says it's undefined
behaviour. If your compiler documentation does not say that it will produce assembly
which does wraparound then you have no reason to expect the code to behave in a
predictable manner so that code needs to be changed. You say above "to get rid of
the undefined behaviour without losing functionality and performance". Without
rational reason to believe that your code will do what you want then you don't
actually have functionality ; if it seems to behave the way you want then it is just
a coincidence and the behaviour may go away without warning like if you use a
different version of compiler. So there's nothing to lose (apart perhaps from
occasions where you urgently want to achieve something and you're willing to kludge
it) , either you fix the code or you have nothing you can depend on.
> 2) Nasal demon fans want license to produce nasal demons for every
> undefined behaviour. E.g., in the general case both gcc and
> Clang/LLVM generate code for 2s-complement arithmetic with
> wraparound for signed integer addition, subtraction, and
> multiplication, so you might classify it as WUB. Nasal demon fans
> still want to keep signed integer overflow undefined even in those
> compilers so that they make use of it for "optimizations".
As I said in a previous post , I don't believe there are "nasal demon fans". As for
wanting license I find this puzzling because I don't believe they need a license.
For example , one might decide to write a C compiler which supports all other parts
of the C standard but not the for statement. One does not need any kind of license
to do this , one simply needs (from a moral point of view) to be honest about what
they offer. And then other people can decide if they want to use the compiler or
not. But if they decide to use it then their expectations must be based on what the
compiler does claim to offer , not on what they would wish it to offer. They might
wish that it also supported the for statement but since it doesn't claim to do so
then they shouldn't use for in their code (if they want to translate their code
with this compiler).
By the way , regarding gcc and signed integer operations , what do you mean "general
case" ? My impression is that without using -ftrapv or -fwrapv then oveflow for
signed integer operations is undefined.
> 3) People aware of the evils of nasal demons don't want them anywhere,
> no matter what undefined behaviour there is. E.g., for an
> out-of-bounds array read, I expect either an unspecified, but
> stable value, or a segmentation violation/general protection fault;
> that's not fully defined, but it excludes nasal demons. E.g., I
> don't expect it to turn a counted loop into an endless loop (and
> this is actually a nasal demon "optimization" that occurs in
> practice).
>
> >In any
> >case , if code has SUB then I cannot imagine on what basis one may think it
> >works and it will reliably continue to do so in the future : even if it
> >passes testing , then that's by coincidence. So if a code exhibits SUB then
> >it's buggy and it needs to be fixed.
>
> Of course that depends on what you consider SUB. Anyway, here's an
> example.
>
> int d[16];
>
> int SATD (void)
> {
> int satd = 0, dd, k;
> for (dd=d[k=0]; k<16; dd=d[++k]) {
> satd += (dd < 0 ? -dd : dd);
> }
> return satd;
> }
>
> If there is some other global data defined earlier and later in the
> program, then d[16] is a mapped (i.e., readable) memory location. And
> if it is an unmapped memory location, you get a SIGSEGV, not some
> nasal demon.
Are you translating this with a C translator which defines in its documentation
things like "mapped memory location" ? If not then these terms are meaningless (in
the specific context of using this specific code with this specific translator) , it
is SUB and you can't have any expectations whatsoever regarding how this code will
behave. I certainly wouldn't. I take it you would ? If yes on what basis ?
> >> 3) Complete correctness proofs of programs are outside the competence
> >> of nearly all programmers (and pretty pointless, because they would
> >> prove only the correctness wrt the specification, which itself may be
> >> buggy).
> >>
> >> Now, to write a C program that is guaranteed to never exercise
> >> undefined behaviour requires competences on the level 3.
> >
> >Not in the slightest. Consider the following piece of C code :
> >
> > int is_leap_year(unsigned int year) {
> > return 1 ;
> > }
> >
> >It's trivial to see that this is defined but , judging from the function's
> >name , it's almost certainly buggy. A complete correctness proof is many
> >orders of magnitude harder than simply ensuring defined behaviour.
>
> I don't think it is trivial to see that this is defined.
Well , I'm not going to locate and quote all the parts of the C standard which
support my view but I have no doubts that it is defined.
> I once
> <2015May1.155805@mips.complang.tuwien.ac.at> wrote:
>
> |It seems to me that
> |
> | if ((size_t)(dest-src) < len)
> |
> |is a more efficient way to test whether dest is inside [src, src+len).
> |
> |Of course, since this code contains more than three tokens, it is
> |likely to contain undefined behaviour
>
> That was mostly in jest, but a post or two later, someone explained
> that yes, this code is undefined. So while I do not see anything
> undefined about the code you posted, just let the language lawyers at
> it, and they will point it out.
Ok , we'll see what the language lawyers say.
> In any case, in your example it is trivial to see that it does not
> satisfy the requirement that is implied by the name, so even if it
> really is trivial to see that it is defined, it only shows that both
> correctness and definedness are trivial to determine for trivial
> programs.
My point was simply to provide a counterexample to your statement
Now, to write a C program that is guaranteed to never exercise
undefined behaviour requires competences on the level 3.
> >> So you will find undefined behaviours in the cases exercized by normal
> >> users, but you will tend not to find undefined behaviour in those
> >> cases exercized by an attacker; it's as difficult as finding the all
> >> the vulnerabilities in the first place. E.g., in the OpenSSH case, if
> >> you thought about the vulnerability, you would fix it right away,
> >> rather than writing a test case that exploited it, and waiting for the
> >> sanitizer to report that freed memory was accessed (if the sanitizer
> >> actually does check that), and then fixing it.
> >
> >The best write-up I could find on the vulnerability is at
> >https://www.qualys.com/2016/01/14/cve-2016-0777-cve-2016-0778/openssh-cve-2016-0777-cve-2016-0778.txt .
> >
> >The crucial bug occurred much earlier than compiler optimisations eliminating
> >code which wrote 0's on some memory. From the previous link
> >
> > - "out_start == out_last" (lines 205-206): no data was ever written to
> > out_buf (and both out_start and out_last are still equal to 0) because
> > no data was ever sent to the server after roaming_reply() was called,
> > but the client sends (leaks) the entire uninitialized out_buf to the
> > server (line 214), as if out_buf_size bytes of data were available.
> >
> >This would still be a bug (albeit a less serious one) even if the memory had
> >been zeroed because it sends bogus information to the server. An analogous
> >bug would be sending over the network unencrypted data which should have been
> >encrypted. In both cases , to see the bugs one needs to think on the level of
> >what the application wants and does not want to do , not on the low level
> >details of the programming language. Some low level detail may accidentally
> >eliminate some bug caused by a high level thinking oversight but this is
> >entirely random so it could just as well make it worse.
> >
> >Another bug was with not handling correctly C arithmetic (see the page).
> >Finally the not zeroing of memory happened because (from the link)
> >
> > Unfortunately, an optimizing compiler may remove this
> > memset() or bzero() call, because the buffer is written to, but never
> > again read from (an optimization known as Dead Store Elimination).
> >
> >so it's not due to undefined behaviour.
>
> But actually the bug resulted in reading from the buffer. So the
> assumption by the compiler that the buffer is never again read from is
> wrong, and applying dead-store elimination to this memset() is wrong;
> in other words, the compiler is buggy.
>
> But of course the GCC maintainers don't accept this as a bug: They say
> that reading from the buffer after the free() is undefined behaviour,
> therefore does not happen, and therefore they are in their rights to
> conjure up nasal demons and "optimize" the memset()/bzero() away. And
> this is not an issue that could turn out one way or the other, this
> memset()/bzero() is there exactly for mitigating information leaks,
> such as the one that is the main reason of the CVE.
I provided a reference above and it does not support your claims that this
is what caused the bug. Do you have a reference which says otherwise ?
> It is telling that you do not understand how the nasal-demon
> interpretation of C allowed the compiler to "optimize" the
> memset()/bzero() away. So much for Andrew Haley's claim that it is
> "not difficult" to write "well-defined" C, and your defense of that
> stance.
I understand what you're claiming but you haven't provided any reference that this
is what caused the bug in the case of OpenSSH.
> >I couldn't tell you off the top of my head but I'm sure you could get the
> >answer on comp.lang.c very quickly. Looking at the big picture , it could
> >be that C is not a suitable back-end for Forth after all even if you got
> >lucky for a number of years and your code (which presumably was exhibiting
> >SUB) worked as intended.
>
> I think that nasal-demon C is not a suitable language for anything.
I use it all the time with perfectly predictable results. I have my complaints
but they are not caused by undefined behaviour.
> > Note that this may turn out to be an opportunity for
> >Forth : it may be that Forth itself is a more suitable back-end than C for other
> >programming languages
>
> Yes.
>
> >A
> >*constructive* thing to do (as opposed to complaining) would be to describe
> >what guarantees with regard to C pointer comparisons on top of the C standard
> >would be needed to do what you want to do. Then you could ask on comp.lang.c
> >or some compiler mailing list whether these additional guarantees can be
> >offered by using some appropriate flag and if not how easy would be to implement
> >them as an extension.
>
> If you think that's a promising approach, go ahead. My experience is
> that they always tell you to go to the C standards committee.
Before you go to the C standards committee you need to have a specific proposal. I
take it that for C to be a suitable back end for implementing Forth , you want
comparison of C pointers pointing to different objects to be defined. Could you
provide a set of axioms that such comparisons ought to satisfy to be adequate for
your purposes ? If not then even if C compiler writers or the C standards committee
wanted to accommodate you , they have no way to do so. You can't expect them to read
your mind , can you ? "Do the natural thing" is not a meaningful definition. I don't
think that the following from your paper is a meaningful definition either :
C* A language (or family of languages) where language constructs correspond
directly to things that the hardware does. E.g., * corresponds to what a
hardware multiply instruction does. In terms of the C standard, conforming
programs are written in C .
I couldn't provide such a set of axioms because I've never implemented a Forth so I
don't know in what ways standard C as a back end is lacking.
> >Undefined behaviour is an unfortunate side effect of 3 factors :
> >
> >1. The desire to allow implementors optimisations.
> >2. Inability to reconcile previous (i.e. before the standard) existing practices
> > therefore any attempt to define the behaviour more narrowly would unfairly
> > privilege some implementations (or architectures) over others.
> >3. The desire to not make the standard too large.
>
> That was all fine and dandy in the good old days of PCC and early GCC,
> but in recent years the compiler maintainers went insane and use them
> as justification for miscompiling (they call it "optimizing") as many
> programs as possible, with some exceptions, in particular, standard
> benchmarks. Paying customers are probably also not treated as badly
> as the rest of us; hmm, so nasal demons may be part of the business
> models.
If it's SUB then it's impossible to miscompile it because correct compilation is not
defined.
> > But noone *likes* undefined behaviour , it is just a trade off.
>
> The GCC and Clang compiler maintainers love it. For them reason 2 and
> 3 don't apply, yet with every release they miscompile more and more
> cases that are undefined in the standard for reasons 2 and 3; e.g.,
> signed integer overflow.
gcc provides 2 different options for getting predictable behaviour for signed
integer overflow. So this contradicts your statement.
> >If
> >programmers get convinced to avoid undefined behaviour then this ultimately
> >will make code more predictable not less.
>
> So you love nasal demons, too.
I avoid SUB so they are indifferent to me. For the point I was making , you snipped
relevant context. I said
The talk of nasal demons is to drive home the point (especially to new
programmers) that when dealing with undefined behaviour (that is SUB) there's no
"reasonable" behaviour one can expect therefore *** Just say no *** .If
programmers get convinced to avoid undefined behaviour then this ultimately will
make code more predictable not less.
To add to the above , as a metaphor which is used as an educational tool , I
consider it unfortunate because it ignores the fact that a computer exists and
operates in the real world so it can only cause things which are physically
possible. There are other ways to drive home the point that SUB is unpredictable
without mentioning physical impossibilities.
> Many programmers are convinced. But because there is actually no good
> way to write code without undefined behaviour, we will get programs by
> convinced programmers that have fewer undefined behaviours, but it
> will still be there; and the next release of the compiler breaks some
> code, the convinced programmers get busy fixing it, and the next
> release breaks some more code. Bottom line: slightly faster
> benchmarks, more programs that break, and more work for the C
> programmers without any benefit.
There is a way to write code without SUB and that is to be familiar with the
standards and documentation which is relevant to the code one writes. Bugs may exist
of course but this would be the case just as much even with no undefined behaviour.
[...]
> >But then there are always some
> >stubborn ones like yourself or
> >http://www.open-chess.org/viewtopic.php?f=5&t=2519 where Robert Hyatt
> >insists that SUB should still do what he wants just because it did in the past.
>
> So you think that using strcpy to do an overlapping backwards copy is
> SUB, i.e., "not defined according to *anything*". Interesting.
I read the thread a while ago and I can't be bothered to reread it but I don't think
that Hyatt said that he was using a C library which , as an extension to the C
standard , defined strcpy() for overlapping objects. If that's the case then the
behaviour was not defined according to anything relevant to the code he was writing
so I would classify it as SUB and I don't believe that he had any rational reason to
expect a specific behaviour (but he thought otherwise). What one might consider
"natural" or useful behaviour for strcpy() does not affect the definition of SUB. I
will present a more general principle :
For the tools you use , you cannot expect what has not been promised to you.
A C compiler is a tool and so is a C library (whether it's the standard C library or
some other) ; they were written by humans. If those humans do not tell you for
example "we made sure that strcpy() copies correctly even overlapping objects" then
you have no rational reason to expect it.
--
This, of course, is a straw man. As the Stanford Encyclopedia of Philosophy observes
Moral relativism has the unusual distinction - both within philosophy and outside
it - of being attributed to others, almost always as a criticism, far more often than
it is explicitly professed by anyone.
http://www.mathpages.com/home/kmath557/kmath557.htm
[toc] | [prev] | [next] | [standalone]
| From | James Kuyper <jameskuyper@verizon.net> |
|---|---|
| Date | 2017-04-09 22:46 -0400 |
| Message-ID | <ocerfl$5j4$1@dont-email.me> |
| In reply to | #56957 |
On 04/09/2017 08:38 PM, Spiros Bousbouras wrote: > [ Crossposted to comp.lang.c since we need some C lawyers ;-) ] > > On Sun, 09 Apr 2017 14:53:01 GMT > anton@mips.complang.tuwien.ac.at (Anton Ertl) wrote: ... >> I once >> <2015May1.155805@mips.complang.tuwien.ac.at> wrote: >> >> |It seems to me that >> | >> | if ((size_t)(dest-src) < len) >> | >> |is a more efficient way to test whether dest is inside [src, src+len). >> | >> |Of course, since this code contains more than three tokens, it is >> |likely to contain undefined behaviour >> >> That was mostly in jest, but a post or two later, someone explained >> that yes, this code is undefined. So while I do not see anything >> undefined about the code you posted, just let the language lawyers at >> it, and they will point it out. > > Ok , we'll see what the language lawyers say. It would help to know what the relevant data types are, but the comment about "dest is inside [src, src+len] suggests that dest and src are both pointers. The C standard defines subtraction of pointers in terms of positions in the SAME array. If src and dest don't both point into or one past the end of the same array, subtraction of those pointers has undefined behavior (6.5.6p9). Consider an implementation of C targeting a machine with a segment-offset architecture, where every pointer into a given object (including pointers to sub-objects) has the same segment value (which implies that no object can be bigger than a single segment), while pointers into completely unrelated objects will, in general, have different segments. On such a machine, the fact that this behavior is undefined means that a fully conforming implementation of C is allowed to implement pointer subtraction by simply subtracting the offsets and IGNORING the segment numbers. Feel free to figure out the implications that would have for your dest-size test. ... >>> A >>> *constructive* thing to do (as opposed to complaining) would be to describe >>> what guarantees with regard to C pointer comparisons on top of the C standard >>> would be needed to do what you want to do. Then you could ask on comp.lang.c >>> or some compiler mailing list whether these additional guarantees can be >>> offered by using some appropriate flag and if not how easy would be to implement >>> them as an extension. >> >> If you think that's a promising approach, go ahead. My experience is >> that they always tell you to go to the C standards committee. Redirecting you to the standards committee would be an inappropriate response to a inquiry about the existence or feasibility of an extension to C. Are you sure you didn't word your inquiry in such a way that it sounded like you were asking for a change to the standard itself? > Before you go to the C standards committee you need to have a specific proposal. I > take it that for C to be a suitable back end for implementing Forth , you want > comparison of C pointers pointing to different objects to be defined. Could you Note: C++ requires that std::less<T*> must provide a total ordering of all pointers of type T*, even if the "<" operator does not provide such an ordering (20.9.5p14). C++ has a sufficiently strong shared heritage with C that the fact that the C++ standard can successfully impose this requirement strongly suggests that the C standard could impose a similar requirement. However, it's telling that C++ did NOT impose this requirement on the "<" operator itself, but only on std::less<T*>. That's because there are some systems where meeting this requirement makes std::less<T*>(p,q) substantially slower than p<q.
[toc] | [prev] | [next] | [standalone]
Page 2 of 7 — ← Prev page 1 [2] 3 4 5 6 7 Next page →
Back to top | Article view | comp.lang.forth
csiph-web