Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > comp.lang.forth > #15078 > unrolled thread
| Started by | visualforth@rocketmail.com |
|---|---|
| First post | 2012-08-21 21:43 -0700 |
| Last post | 2012-08-22 07:37 -0700 |
| Articles | 20 on this page of 163 — 19 participants |
Back to article view | Back to comp.lang.forth
Comparative Productivity of Programming Languages visualforth@rocketmail.com - 2012-08-21 21:43 -0700
Re: Comparative Productivity of Programming Languages "A. K." <akk@nospam.org> - 2012-08-22 07:07 +0200
Re: Comparative Productivity of Programming Languages Andrew Haley <andrew29@littlepinkcloud.invalid> - 2012-08-22 03:35 -0500
Re: Comparative Productivity of Programming Languages John Passaniti <john.passaniti@gmail.com> - 2012-08-22 14:06 -0700
Function Points (was: Comparative Productivity of Programming Languages) anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-23 14:50 +0000
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-23 11:43 -0700
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-25 14:13 +0000
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-25 10:12 -0700
Re: Function Points Doug Hoffman <glidedog@gmail.com> - 2012-08-25 15:39 -0400
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-25 15:09 -0700
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-08-25 12:34 -1000
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-25 16:43 -0700
Re: Function Points jacko <jackokring@gmail.com> - 2012-08-25 18:05 -0700
Re: Function Points jacko <jackokring@gmail.com> - 2012-08-25 20:34 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-08-26 03:24 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-25 22:44 -0700
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-08-25 21:19 -1000
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-26 00:36 -0700
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-08-25 21:50 -1000
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-26 01:08 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-08-26 23:20 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-26 19:33 -0700
Re: Function Points Andrew Haley <andrew29@littlepinkcloud.invalid> - 2012-08-27 13:34 -0500
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-08-27 22:38 +0200
Re: Function Points Andrew Haley <andrew29@littlepinkcloud.invalid> - 2012-08-28 02:45 -0500
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-27 18:14 -0700
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-27 18:24 -0700
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-30 14:22 +0000
Re: Function Points Andrew Haley <andrew29@littlepinkcloud.invalid> - 2012-08-28 03:07 -0500
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-28 08:18 -0700
Re: Function Points Andrew Haley <andrew29@littlepinkcloud.invalid> - 2012-08-28 12:15 -0500
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-28 23:05 -0700
Re: Function Points Andrew Haley <andrew29@littlepinkcloud.invalid> - 2012-08-29 03:55 -0500
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-08-27 22:28 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-27 20:26 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-08-28 23:17 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-29 01:13 -0700
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-29 02:23 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-08-30 02:59 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-29 22:18 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-08-30 20:44 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-31 01:29 -0700
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-31 09:33 +0000
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-08-30 02:58 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-29 19:39 -0700
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-30 14:10 +0000
Re: Function Points gavino_himself <visploveslisp@gmail.com> - 2012-08-30 20:08 -0700
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-08-30 17:47 -1000
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-08-27 13:43 -1000
Re: Function Points "Paul E. Bennett" <Paul_E.Bennett@topmail.co.uk> - 2012-08-27 12:14 +0100
Re: Function Points Mark Wills <markrobertwills@yahoo.co.uk> - 2012-08-27 05:12 -0700
Re: Function Points "Paul E. Bennett" <Paul_E.Bennett@topmail.co.uk> - 2012-08-27 15:52 +0100
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-26 13:09 +0000
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-27 20:52 -0700
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-30 14:08 +0000
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-30 10:43 -0700
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-08-30 08:25 -1000
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-08-30 22:42 +0200
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-08-31 01:23 -0400
Re: Function Points Andrew Haley <andrew29@littlepinkcloud.invalid> - 2012-08-31 03:08 -0500
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-08-31 18:56 -0400
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-01 02:35 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-31 23:52 -0700
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-01 14:27 +0000
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-01 14:18 +0000
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-01 17:45 +0200
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-01 16:14 +0000
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-01 19:13 +0200
Re: Function Points Andrew Haley <andrew29@littlepinkcloud.invalid> - 2012-09-02 03:19 -0500
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-01 16:18 -0400
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-02 03:04 +0200
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-02 04:02 -0400
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-02 17:40 +0200
Re: Function Points jim@rainbarrel.com - 2012-09-02 10:32 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-02 20:49 +0200
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-02 16:33 -0400
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-02 17:03 -0400
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-09-02 09:02 -1000
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-02 16:35 -0400
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-09-02 13:42 -1000
Re: Function Points jim@rainbarrel.com - 2012-09-02 16:54 -0700
Re: Function Points Mark Wills <markrobertwills@yahoo.co.uk> - 2012-09-03 00:29 -0700
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-03 01:30 -0400
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-09-02 21:21 -1000
Re: Function Points jim@rainbarrel.com - 2012-09-03 10:37 -0700
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-04 07:14 +0000
Re: Function Points Coos Haak <chforth@hccnet.nl> - 2012-09-03 21:12 +0200
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-03 17:32 -0400
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-03 17:51 -0400
Re: Function Points John Passaniti <john.passaniti@gmail.com> - 2012-09-03 22:37 -0700
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-04 04:25 -0400
Re: Function Points John Passaniti <john.passaniti@gmail.com> - 2012-09-04 07:35 -0700
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-05 02:13 -0400
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-09-04 20:18 -1000
Re: Function Points John Passaniti <john.passaniti@gmail.com> - 2012-09-05 10:56 -0700
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-05 16:11 -0400
Re: Function Points John Passaniti <john.passaniti@gmail.com> - 2012-09-05 14:07 -0700
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-02 16:27 -0400
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-03 00:52 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-09-02 16:28 -0700
Re: Function Points jim@rainbarrel.com - 2012-09-02 16:48 -0700
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-02 20:21 -0400
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-09-02 14:45 -1000
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-03 01:12 -0400
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-09-02 21:26 -1000
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-03 01:06 -0400
Re: Function Points Mark Wills <markrobertwills@yahoo.co.uk> - 2012-08-31 03:29 -0700
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-31 10:35 +0000
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-08-31 18:49 -0400
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-01 14:49 +0000
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-09-01 08:36 -1000
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-01 16:11 -0400
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-03 01:58 +0200
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-01 17:54 +0200
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-01 16:19 -0400
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-02 03:05 +0200
Re: Function Points Coos Haak <chforth@hccnet.nl> - 2012-08-31 23:10 +0200
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-08-31 15:50 -1000
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-09-01 10:31 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-01 21:52 +0200
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-01 16:36 -0400
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-09-01 14:36 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-02 03:30 +0200
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-02 23:15 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-09-02 15:02 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-03 01:50 +0200
Re: Function Points jim@rainbarrel.com - 2012-09-02 16:57 -0700
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-09-03 23:11 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-04 14:30 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-09-04 10:14 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-04 22:10 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-09-06 00:19 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-06 17:48 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-09-06 12:01 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-06 22:02 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-09-06 14:19 -0700
Heap (was: Function Points) anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-07 11:30 +0000
Re: Heap (was: Function Points) Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-07 18:12 +0200
Re: Heap (was: Function Points) anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-07 16:48 +0000
Re: Heap (was: Function Points) Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-07 21:34 +0200
Re: Heap Gerry Jackson <gerry@jackson9000.fsnet.co.uk> - 2012-09-07 22:04 +0100
Re: Heap anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-08 11:52 +0000
Re: Heap Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-08 22:48 +0200
Re: Heap (was: Function Points) anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-08 12:11 +0000
priority queue (was: Function Points) anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-03 11:46 +0000
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-03 15:03 +0200
Re: Function Points mhx@iae.nl (Marcel Hendrix) - 2012-09-03 22:36 +0200
Re: Function Points mhx@iae.nl (Marcel Hendrix) - 2012-09-06 20:27 +0200
Re: Function Points Andrew Haley <andrew29@littlepinkcloud.invalid> - 2012-09-02 04:00 -0500
Re: Function Points visualforth@rocketmail.com - 2012-09-03 10:40 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-03 20:26 +0200
Re: Function Points Doug Hoffman <glidedog@gmail.com> - 2012-08-27 11:49 -0400
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-27 09:16 -0700
Re: Function Points Josh Grams <josh@qualdan.com> - 2012-08-28 22:46 +0000
Re: Function Points jacko <jackokring@gmail.com> - 2012-08-28 16:06 -0700
Re: Function Points Doug Hoffman <glidedog@gmail.com> - 2012-08-28 20:50 -0400
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-26 12:59 +0000
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-26 22:24 -0700
Re: Function Points (was: Comparative Productivity of Programming Languages) John Passaniti <john.passaniti@gmail.com> - 2012-08-23 15:02 -0700
Re: Function Points (was: Comparative Productivity of Programming Languages) anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-25 14:57 +0000
Re: Comparative Productivity of Programming Languages "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-08-22 08:07 -0400
Re: Comparative Productivity of Programming Languages visualforth@rocketmail.com - 2012-08-22 08:12 -0700
Re: Comparative Productivity of Programming Languages visualforth@rocketmail.com - 2012-08-22 07:37 -0700
Page 6 of 9 — ← Prev page 1 2 3 4 5 [6] 7 8 9 Next page →
| From | jim@rainbarrel.com |
|---|---|
| Date | 2012-09-02 16:48 -0700 |
| Subject | Re: Function Points |
| Message-ID | <0ac6c8ab-d4e6-46da-bef2-1ed32164f6c1@googlegroups.com> |
| In reply to | #15404 |
>
> Yes, don't know what happend. Maybe a buffer overflow ;-). You don't
>
> know what is "sufficiently large", you are just guessing. And that's a
>
> bad idea. There are two sane ways to deal with buffer sizes: Either
>
> pass them along with the buffer pointer, or adjust the buffer size as
>
> required. I prefer the latter, because it doesn't waste memory in the
>
> typical case (short buffer sufficient), and doesn't fail, as long as
>
> there's enough memory.
>
Diaperglu does both at the same time.
In Diaperglu Forth I have a NEW-BUFFER (or is it NEWBUFFER?) command which returns a buffer id.
Then there are commands to let you fetch from, store into, and push onto the end of the buffer. If the buffer needs to grow, it grows. If there isn't enough memory, or you try to access off the end of the buffer using one of the buffer commands, you get an error but the buffer's memory is never overflowed.
And if you need to, you can find out how long the buffer is.
This system also allows you to break up memory allocated from the system into smaller chunks, which is handy because last time I checked Linux and FreeBSD allocated memory in sizes of 1k chunks, Mac OS X in 4k chunks, and Windows in chunks of 8bytes.
If you want to limit how much a buffer can grow, or how much it grows when it needs to grow, you can do that also when you create the buffer.
All these problems you guys are arguing about are solved. So now lets make it part of the Forth standard.
Oh, and if you are trying to implement a hash, I just added hierarchical lists to Diaperglu Forth, which is a superset of a hash, and if you use the access functions provided, you can't overflow any memory buffers. Granted, the memory usage is not optimal since I used packed arrays... will fix that in the future.
Why not make this part of the Forth standard too? Then Forth can become the first programming language with responsible memory usage as part of it's basic tool set instead of pushing those issues onto the shoulders of the programmer community who each have to discover and solve these problems on their own and for the most part just ignore them.
>
> > I already told you _how_ a C
>
> > programmer knows the buffer is sufficiently large, repeatedly. How
>
> > does a Forth programmer know the destination buffer at 'c-addr2' is
>
> > sufficiently large?
>
>
>
> By checking the length which came together with the addr in an addr len
>
> pair.
>
>
>
> > Same reason, yes?
Then every programmer has to build a set of routines that check these things... sounds like something that could become part of the standard and built in as an extension to Forth. Maybe a set of 'buffer handling' words?
>
>
> Not at all. Forth programs are factored to quite small entities, so
>
> such sort of a-prior knowledge which you always insist on ("I know how
>
> large my malloced block is"), is not useful in a Forth program.
>
> Actually, it's also not useful in a C program, because C programs tend
>
> to be moderately factored, too (not into the same small entities as a
>
> Forth program, but they are still factored).
>
Not sure what you mean by 'factored to quite small entities' does that mean Forth is only used for solving small problems? or that Forth program is broken up into many subroutines of small length?
> Unfortunately, C strings are not memory blocks. It would be nice if
>
> they were, because then the whole issue would quickly go away. All
>
> strings, all buffers in C would be addr len pairs, and the knowledge of
>
> their size wouldn't be lost.
And what happens if the system runs out of memory while you are using them?
> Yes. Well, you can argue that an attacker who is allowed to fill in
>
> arbitrary values in a globally used table in PHP is a problem in any
>
> case, so removing that capability (which apparently didn't break
>
> programs) is a good idea.
>
>
>
> >> > I'm not sure if these are the type of hash functions they need, but
>
> >> > these two public hash functions are good:
>
> >> >
>
> >> > Austin Appleby's MurmurHash2
>
> >> > Bob Jenkins' hashlittle() from lookup3.c
Wouldn't it be nice if these modules were already programmed and tested and available in a public Forth repository? And since it's such a common function that many people will use.... why not have it be an extension to the Forth standard?
But then you guys would have to find something else to argue about.
[toc] | [prev] | [next] | [standalone]
| From | "Rod Pemberton" <do_not_have@notemailnot.cmm> |
|---|---|
| Date | 2012-09-02 20:21 -0400 |
| Subject | Re: Function Points |
| Message-ID | <k20t0r$qsj$1@speranza.aioe.org> |
| In reply to | #15404 |
"Bernd Paysan" <bernd.paysan@gmx.de> wrote in message news:2365622.2KXcLuKiTj@sunwukong.fritz.box... > Rod Pemberton wrote: > >> Forth had counted strings, and dismissed that idea later, going to > >> the > >> addr len stack pattern instead. Counted strings and zero-terminated > >> strings share a common stupid thing: You can't point to substrings. > >> Byte-counted strings limit the string size to up to 255 characters, > >> which is also stupid. > >> > > > > I don't know what you mean. > > I now understand that you don't understand. Try harder. > > > Both sub1 and sub2 point to substrings of string bp. > > > > char bp[]="Hello!"; > > char *sub1,*sub2; > > > > sub1=bp+3; > > sub2=&bp[2]; > > Ok, for the slow thinkers: Let's say we have a forth command line, > consisting of the string > > ": foo bar 2dup over type ;" > > We now want to point to the substring "foo", because that's our name to > define. In Forth, this is just an string+2 3 as addr len pair. In C, > you need to make a copy. > That situation is of low use. C has strtok() to parse strings. You also have other options in C besides copying the internal substring. You can use strtok(). You can also manually change the the final character of the substring to to a null, use the substring, and restore the character when done. > > Did you mean a completely internal substring? > > Yes. You should think first and then start to babble. > And, again with the unecessary insults. You didn't _say_ an internal substring. You said: "You can't point to substrings." You placed no restrictions on which type of substring C couldn't point to in your claim. I clearly demonstrated that wasn't true. I demonstrated that you can point to certain types of substrings in C. > > E.g., "ell" from "Hello!"? That's why C has 'n' string functions... > > I don't actually think that copying a substring to make use of it is a > clever idea. You end up with all the hassles that causes C programs to > go astray: Uh, I need a buffer for that, and I need the buffer before I > know the length... That just shows you don't know C very well. Honestly, I don't think I've *ever* needed a substring in C. Use of substrings in BASIC was quite common. Typically, you'll use strrchr(), or rarely strchr(), to find a delimiter, then change it to null. Basically, in C, you can perform almost all string operations with strrchr(), strcpy(), strcat(), and the ability to set a null character within the string. If you can't, you're doing something incorrectly. > In Forth, you know how much MOVE will > copy *before it starts copying*, 1) Yes, but you don't know the destination buffer's size for Forth's MOVE. 2) Yes, the same is true for strcpy() and strncpy(). For strncpy(), it copies exactly 'n' characters, padding with null's if needed. For strcpy(), it copies strlen() characters. Call strlen() if you need to know. > [...] as you tell it how much it should copy. Ditto for strncpy() and strcpy(). You tell strncpy() to copy 'n' characters. You tell strcpy() to copy the entire string, which is strlen() characters. > In C, strcpy() doesn't even tell you after it did so, it is implicit. > strcpy() copies the entire string. It's length is known via strlen() or the string allocation via malloc() or the string declaration. > > Ignoring the insult, that's not _exactly_ the root cause. The buffer > > size is known in C. > > Unfortunately only at the point where you declare the buffer. Once you > start passing it around, this information is lost. No, it's rarely lost. It's generally available globally as a preprocessor #define which can be used almost anywhere an integer value is used. > And that's the difference to Forth: With the recommended style of > passing addr len buffers, this information is not lost. > The 'addr len' form has other flaws. The len value doesn't have to match the string's actual length, e.g., len could be 5, but the string could be six in length. If too small, it truncates the string. If too large, it overflows a buffer. With a null terminator, strlen() will always return the correct length. PL/1 uses counted strings. It is one of the language's flaws. > > Forth is no different here. > > If you ignore the usual style how to deal with buffers, yes, you can do > the same bad things as in C. But in C, it's not ignoring well- > established practice, there it *is* established pratice to pass around > pointers without size as buffers. > How is that any different from MOVE? MOVE doesn't receive the destination buffer size. > > This is no different from not knowing the destination buffer size in > > C when you should know it and when it's available to you. > > In a moderately factored C program, the buffer size is not available to > you when you need it. Because due to C's braindead "we pass buffers as > pointers, and don't tell anybody how long they are", this information > gets lost too quickly. > Forth doesn't pass the buffer size either. All Forth words you mentioned pass the count to be moved or copied, not the actual buffer size. Why do you call C braindead and not Forth too? > >> No, the key is that there is no "sufficiently large", because the > >> attacker can always make his attack vector larger. > > > > How is Forth unaffected by this? (It's not.) > > By passing the size of buffers around, and making it possible to write > correct code. > Show me where MOVE passes the buffer size. MOVE passes a count, not the source or destination buffer size. > > getenv() is not standard C. > > This is a rather silly argument. getenv() is both part of C89 and C99. > Wow, I learned one thing from you: getenv() is an unneeded and useless function, but then again so is stdlib.h. > > Even so, it returns a pointer to a > > _string_. Any sane programmer would then check it's length via > > strlen() prior to strcpy() and strcat() to make sure it fits the > > buffer. > > Unfortunately, we have only insane programmers around. > You suggested doing so. How do you know your insane? > >> [...] and that it contains executable code, allowing > >> the user to gain privilege. > >> > > > > I see nothing which transfers execution to the string. In your > > example, it's always a string. It's possible there is a hidden buffer > > overflow, but if coded correctly, 'path' is more than long enough to > > handle the strcpy() > > and strcat(). > > No. You don't know if path is long enough, Why not? It was declared or malloc'd somewhere. A quantity was required to do that. Typically, a #define is used for an array's size. If not, an integer can save it's size. Or, sizeof() can be used to determine it's size. > [...] and the standard coding > style doesn't give you any way to even check. Typically, it's a #define in an include file, the system include file that defines 'path' and must be included in order to use 'path'... > [...] path may be a buffer > provided by some function above in the call tree, like > > char path[60]; /* should be enough, programmer's sloppy reasoning */ > tilde_expand(path, "~/.mystupidprogramrc"); > Yes, that would stupid. > > The maximum length of a system variable is known. > > No. > Yes. > http://stackoverflow.com/questions/1078031/what-is-the-maximum-size-of- > an-environment-variable-value > > People there created surprisingly large environment variables when > trying to find the limit. It's still a string. getenv() can only do a few things with it when the user requests it: point to wherever it's stored in OS memory, allocate space for it and copy it to application space and/or truncate it. Either way, for it to be valid C, strlen() must work for it. > It is at least operating system dependent, > and a portable program might run fine on one OS, but be vulnerable to > buffer overflows on another. > I don't see how this is any different from anything else C or Forth use to interface the host OS. IIRC, C even defines such things as implementation dependent. However, the sizes of OS objects are generally provide in an include, at least for C. I don't know about all OSes, but many do. > > Sorry, the allocation parameter to malloc() is known in advance. > > But it is known to some completely different part of the program, which > - by conventional C style - choose to not tell anybody else. > How is that different from ALLOT allocationg a buffer in Forth, and then some other Forth word calling MOVE to write into that buffer? > You don't know what is "sufficiently large", you are just guessing. No, you need a specific quantity to declare or allocate. I.e., it's known. > > I already told you _how_ a C > > programmer knows the buffer is sufficiently large, repeatedly. How > > does a Forth programmer know the destination buffer at 'c-addr2' is > > sufficiently large? > > By checking the length which came together with the addr in an > addr len pair. There is no 'addr len' pair for the destination buffer of MOVE. There is only an 'addr'. > Forth passes the size of the destination buffer around as addr len pair Where? > Unfortunately, C strings are not memory blocks. It would be nice if > they were, because then the whole issue would quickly go away. All > strings, all buffers in C would be addr len pairs, and the knowledge of > their size wouldn't be lost. > You keep ignoring the fact that _two_ buffers are in use, and the fact that Forth doesn't pass the length of either. > MOVE is a low-level building block, if you want to make a buffer-to- > buffer copy (both with addr len) that doesn't overflow, you write > something like > > : copy ( addr1 len1 addr2 len2 -- ) rot umin move ; > > That's on the edge of becoming a word of its own, so usually, you write > that explicitely, not as a word. I.e., you have to write a safe Forth version of MOVE and pass around an extra argument... > [...] > >> Regardless of how you create your hash function, its key is > >> reduced to a few bits (in the order of 10), and therefore, you can > >> quickly generate a whole lot of colissions. > >> > > True. However, their defective implementation doesn't change their > > need for fewer collisions. > > How do you know that they have too many collissions? I'm not going to > look at PHP's source code [...] It said so in the link you provided, twice. > An attacker hand-crafted a set of strings so that they would end up in a > single bucket of PHP's hash table, this doesn't indicate that they have > too many collisions in the general case. > True. But, they do under the attack case. That's were they're having a problem. > All reasonable hash functions pass a chi² test on non-random data (e.g. > a dictionary), and should have about the same number of collisions. > That's how you test if your hash function is good. > There are quite a few hash tests to determine if a hash is "good" or not. The problem is that they frequently test the hash for some situation which isn't necessary for a real world hash to have. I.e., why do I need "avalanche" behavior or no "funneling", low collisions on binary data, or good chi2, if I want low collisions on a known set of non-binary, string data (non-uniform data)? That's were brute-force testing comes into play. Rod Pemberton
[toc] | [prev] | [next] | [standalone]
| From | "Elizabeth D. Rather" <erather@forth.com> |
|---|---|
| Date | 2012-09-02 14:45 -1000 |
| Subject | Re: Function Points |
| Message-ID | <GYednf6q89ZZYN7NnZ2dnUVZ_u6dnZ2d@supernews.com> |
| In reply to | #15414 |
On 9/2/12 2:21 PM, Rod Pemberton wrote:
> "Bernd Paysan" <bernd.paysan@gmx.de> wrote in message
> news:2365622.2KXcLuKiTj@sunwukong.fritz.box...
...
>
>> In Forth, you know how much MOVE will
>> copy *before it starts copying*,
>
> 1) Yes, but you don't know the destination buffer's size for Forth's MOVE.
You had better know! That responsibility is squarely on the programmer,
just as it's the programmer's responsibility not to ! into a CVARIABLE
or 2! into a single cell.
...
>> And that's the difference to Forth: With the recommended style of
>> passing addr len buffers, this information is not lost.
>>
>
> The 'addr len' form has other flaws. The len value doesn't have to match
> the string's actual length, e.g., len could be 5, but the string could be
> six in length. If too small, it truncates the string. If too large, it
> overflows a buffer. With a null terminator, strlen() will always return the
> correct length.
The programmer is in full control here. If you want to copy or move the
first 5 bytes of a 6-byte string, there's no reason you shouldn't be
able to. It is equally the programmer's responsibility to know how big
the destination space is.
"With great freedom goes great responsibility."
...
> There is no 'addr len' pair for the destination buffer of MOVE. There is
> only an 'addr'.
>
>> Forth passes the size of the destination buffer around as addr len pair
>
> Where?
If you *want* to make buffers that return an addr len pair when invoked,
you're perfectly free to do so:
: BUFFER ( len -- ) CREATE DUP , ALLOT
DOES> ( -- addr len ) DUP 1+ SWAP @ ;
Then you can use such buffers with a 'copy' word like the one below.
...
>> MOVE is a low-level building block, if you want to make a buffer-to-
>> buffer copy (both with addr len) that doesn't overflow, you write
>> something like
>>
>> : copy ( addr1 len1 addr2 len2 -- ) rot umin move ;
>>
>> That's on the edge of becoming a word of its own, so usually, you write
>> that explicitely, not as a word.
>
> I.e., you have to write a safe Forth version of MOVE and pass around an
> extra argument...
Sure. It's trivially easy to do that. The fact is, folks don't.
Cheers,
Elizabeth
--
==================================================
Elizabeth D. Rather (US & Canada) 800-55-FORTH
FORTH Inc. +1 310.999.6784
5959 West Century Blvd. Suite 700
Los Angeles, CA 90045
http://www.forth.com
"Forth-based products and Services for real-time
applications since 1973."
==================================================
[toc] | [prev] | [next] | [standalone]
| From | "Rod Pemberton" <do_not_have@notemailnot.cmm> |
|---|---|
| Date | 2012-09-03 01:12 -0400 |
| Subject | Re: Function Points |
| Message-ID | <k21e30$pca$1@speranza.aioe.org> |
| In reply to | #15415 |
"Elizabeth D. Rather" <erather@forth.com> wrote in message news:GYednf6q89ZZYN7NnZ2dnUVZ_u6dnZ2d@supernews.com... > On 9/2/12 2:21 PM, Rod Pemberton wrote: > > "Bernd Paysan" <bernd.paysan@gmx.de> wrote in message > > news:2365622.2KXcLuKiTj@sunwukong.fritz.box... > ... > > > >> In Forth, you know how much MOVE will > >> copy *before it starts copying*, > > > > 1) Yes, but you don't know the destination buffer's size for Forth's > > MOVE. > > You had better know! That responsibility is squarely on the programmer, > just as it's the programmer's responsibility not to ! into a CVARIABLE > or 2! into a single cell. > Sorry. What was meant here and was correctly stated for numerous prior posts to Bernd, is that the destination buffer's size unknown from MOVE's parameters. Bernd has been saying that MOVE CMOVE> et. al. know the sizes of the buffer they move or write into. They don't. They aren't passed the destination's buffer size. They are passed a quantity to move. They aren't passed the source's buffer size either. He's been complaining about C's functions passing addresses around without passing around the size of the buffer. I've been telling him C's string functions have the same problems as Forth. He just won't accept that. Rod Pemberton
[toc] | [prev] | [next] | [standalone]
| From | "Elizabeth D. Rather" <erather@forth.com> |
|---|---|
| Date | 2012-09-02 21:26 -1000 |
| Subject | Re: Function Points |
| Message-ID | <O-idncDimO8CxtnNnZ2dnUVZ_g2dnZ2d@supernews.com> |
| In reply to | #15417 |
On 9/2/12 7:12 PM, Rod Pemberton wrote: > "Elizabeth D. Rather" <erather@forth.com> wrote in message > news:GYednf6q89ZZYN7NnZ2dnUVZ_u6dnZ2d@supernews.com... >> On 9/2/12 2:21 PM, Rod Pemberton wrote: >>> "Bernd Paysan" <bernd.paysan@gmx.de> wrote in message >>> news:2365622.2KXcLuKiTj@sunwukong.fritz.box... >> ... >>> >>>> In Forth, you know how much MOVE will >>>> copy *before it starts copying*, >>> >>> 1) Yes, but you don't know the destination buffer's size for Forth's >>> MOVE. >> >> You had better know! That responsibility is squarely on the programmer, >> just as it's the programmer's responsibility not to ! into a CVARIABLE >> or 2! into a single cell. >> > > Sorry. What was meant here and was correctly stated for numerous prior > posts to Bernd, is that the destination buffer's size unknown from MOVE's > parameters. Bernd has been saying that MOVE CMOVE> et. al. know the sizes > of the buffer they move or write into. They don't. They aren't passed the > destination's buffer size. They are passed a quantity to move. They aren't > passed the source's buffer size either. > > He's been complaining about C's functions passing addresses around without > passing around the size of the buffer. I've been telling him C's string > functions have the same problems as Forth. He just won't accept that. It is correct that Forth doesn't "know" the size of the destination buffer, unless you've implemented something like the code I posted which returns addr len when you reference a buffer, and then use a move whose parameters are ( addr1 len1 addr2 len2 -- ). But in normal usage, it isn't expected to. The *programmer* is responsible for knowing how many address units are to be moved and whether the destination space is appropriately sized. That is as it should be, IMO. Cheers, Elizabeth -- ================================================== Elizabeth D. Rather (US & Canada) 800-55-FORTH FORTH Inc. +1 310.999.6784 5959 West Century Blvd. Suite 700 Los Angeles, CA 90045 http://www.forth.com "Forth-based products and Services for real-time applications since 1973." ==================================================
[toc] | [prev] | [next] | [standalone]
| From | "Rod Pemberton" <do_not_have@notemailnot.cmm> |
|---|---|
| Date | 2012-09-03 01:06 -0400 |
| Subject | Re: Function Points |
| Message-ID | <k21dnc$oqn$1@speranza.aioe.org> |
| In reply to | #15414 |
"Rod Pemberton" <do_not_have@notemailnot.cmm> wrote in message news:k20t0r$qsj$1@speranza.aioe.org... [some of _my_ typo's] > six in length. If too small, it truncates the string. If too large, it If it's too small If it's too large > You suggested doing so. How do you know your insane? you're > Yes, that would stupid. would be stupid. > dependent. However, the sizes of OS objects are generally provide in an provided > How is that different from ALLOT allocationg a buffer in Forth, and then allocating > True. But, they do under the attack case. That's were they're having a where Rod Pemberton
[toc] | [prev] | [next] | [standalone]
| From | Mark Wills <markrobertwills@yahoo.co.uk> |
|---|---|
| Date | 2012-08-31 03:29 -0700 |
| Subject | Re: Function Points |
| Message-ID | <0db22181-f310-4f01-89af-6ec4cf68e99d@u15g2000yql.googlegroups.com> |
| In reply to | #15280 |
On Aug 30, 9:42 pm, Bernd Paysan <bernd.pay...@gmx.de> wrote: > But C's main problem is one fundamental mistake: buffers are passed > around as pointers, without length. This is a direct invitation to > buffer overflows. The problem of C is not just a lack of type > information, it is the lack of a very vital information: the lack of > knowing how big a buffer actually is. > > Forth doesn't know about types, but its buffer operations all know about > the size of the buffer. > Hmmm... I'm going to have to call you on that one, Bernd! CALL! I agree re C's shortcomings, but I don't see that Forth is any better: CREATE BUFFER 300 CHARS ALLOT How a does a subsequent definition referencing BUFFER know how big BUFFER is? Remember: Forth sets you free. You're free to fuck up in any way you want ;-) This is blessing or curse. Just depends on personal preference and experience, I suppose. If we had a dedicated word for creating buffers that took a parameter on creation then the problem would be essentially solved: : BUFFER ( interpretation: size "name" -- children: -- address size) CREATE DUP , ALLOT ALIGN DOES> DUP @ SWAP 1 CELLS+ SWAP ; Well, 'solved' in the sense that children of BUFFER report their allocation size on the stack, in addition to their buffer address when referenced, so there would be no excuse for lazy programmers to allow their code to read/write beyond the end of a buffer. The above makes their usage in loops reasonably 'safe': 100 BUFFER MyBuf : SeeBuffer MyBuf 0 DO DUP I + C@ . LOOP DROP ; That's probably as safe as we can get without using dedicated buffer fetch and store words/primitives that do bounds checks. It's nice that we can 'roll our own' buffer handling words such as the above, however, there's nothing about the above that couldn't be reproduced in C with a simple struct, which makes me think that C's somewhat bad reputation (with regard to buffer overflows/overruns) is not really down to the languge itself, but rather just pure lazy programming! I have previously lamented over the lack of 'true' buffers in Forth, but the ease with which one can roll their own is possibly why it is an area that hasn't been standardised.
[toc] | [prev] | [next] | [standalone]
| From | anton@mips.complang.tuwien.ac.at (Anton Ertl) |
|---|---|
| Date | 2012-08-31 10:35 +0000 |
| Subject | Re: Function Points |
| Message-ID | <2012Aug31.123502@mips.complang.tuwien.ac.at> |
| In reply to | #15309 |
Mark Wills <markrobertwills@yahoo.co.uk> writes:
>On Aug 30, 9:42=A0pm, Bernd Paysan <bernd.pay...@gmx.de> wrote:
>> Forth doesn't know about types, but its buffer operations all know about
>> the size of the buffer.
>>
>
>Hmmm... I'm going to have to call you on that one, Bernd!
>
>CALL!
>
>I agree re C's shortcomings, but I don't see that Forth is any better:
>
>CREATE BUFFER 300 CHARS ALLOT
>
>How a does a subsequent definition referencing BUFFER know how big
>BUFFER is?
You pass the length. The difference is that Forth-94 words all take
the length, while C has standard functions like gets(), strcpy(),
strcat() that are not passed the size of the target buffer. For
gets() there is no way to use it safely, but at least there is the
replacement fgets(). OTOH, while strcpy() and strcat() can be used
safely in theory, this is quite cumbersome, so it is often not done,
or not done correctly, and they are the source of many buffer
overflows.
In Forth-200x there is a word that writes a varying amount of data to
memory without passing a data size:
|XC!+ ( xchar xc-addr1 -- xc-addr2 ) XCHAR
|Stores the xchar at xc-addr1. xc-addr2 points to the first memory
|location after the stored xchar.
The justification is that the size of the written data is limited to
four bytes; and there is also an alternative that should be safer
against buffer overflows:
|XC!+? ( xchar xc-addr1 u1 -- xc-addr2 u2 flag ) XCHAR
|Stores the xchar into the string buffer specified by xc-addr1 u1.
|xc-addr2 u2 is the remaining string buffer. If the xchar did fit into
|the buffer, flag is true, otherwise flag is false, and xc-addr2 u2
|equal xc-addr1 u1. XC!+? is safe for buffer overflows.
- 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 2012: http://www.euroforth.org/ef12/
[toc] | [prev] | [next] | [standalone]
| From | "Rod Pemberton" <do_not_have@notemailnot.cmm> |
|---|---|
| Date | 2012-08-31 18:49 -0400 |
| Subject | Re: Function Points |
| Message-ID | <k1resn$io5$1@speranza.aioe.org> |
| In reply to | #15312 |
"Anton Ertl" <anton@mips.complang.tuwien.ac.at> wrote in message news:2012Aug31.123502@mips.complang.tuwien.ac.at... > Mark Wills <markrobertwills@yahoo.co.uk> writes: > >On Aug 30, 9:42=A0pm, Bernd Paysan <bernd.pay...@gmx.de> wrote: ... > >> Forth doesn't know about types, but its buffer operations all know > >> about the size of the buffer. > > > >How a does a subsequent definition referencing BUFFER know how big > >BUFFER is? > > You pass the length. The difference is that Forth-94 words all take > the length, [...] Ok. > [...] while C has standard functions like gets(), strcpy(), > strcat() that are not passed the size of the target buffer. For > gets() there is no way to use it safely, but at least there is the > replacement fgets(). False. You seem to have a trivial or cursory understanding of the issue. 1) gets() is only unsafe when passed input which exceeds the input buffer's length. The standard input stream in C is redirectable to inputs other than the potentially unlimited input from the user's keyboard. I.e., a file where the data line lengths are known in advance to fit within the input buffer. 2) fgets() is unsafe too. It can also be passed input which exceeds the input buffer's length. There is nothing requiring the length passed to fgets() to be smaller or no more than the size of the input buffer. > OTOH, while strcpy() and strcat() can be used safely in theory, > this is quite cumbersome, so it is often not done, or not done > correctly, [...] False. They are not cumbersome nor frequently misused. I've never had a need for strncpy() or strncat() or other "safety" functions to prevent buffer overflows. You shouldn't get buffer overflows if you make sure the input buffer is large enough, and avoid using gets(). > [...] and they are the source of many buffer overflows. False. They _can_ be the source of _some_ buffer overflows. I think you're basing this claim of "many" on the fact that someone created strlcpy() and strlcat(). Whether they are the source of many, or whether "many" is reserved for gets() is debatable. I've not seen gets() used much, although it's decried as the major problem. FYI, some years ago a security paper identified these as issues in C: 1) 15 C functions suffer buffer overflow problems: gets() cuserid() scanf() fscanf() sscanf() vscanf() vsscanf() vfscanf() sprintf() strcat() strcpy() streadd() strecpy() vsprintf() strtrns() 2) 8 C functions suffer from format string vulnerabilities printf() fprintf() sprintf() snprintf() vprintf() vfprintf() vsprintf() vsnprintf() Except for gets(), the functions above with buffer overflows shouldn't have buffer overflows if used correctly with a large enough buffer. The functions above with format string vulnerabilities affect the majority of C implementations since most use a common stack for both control-flow and other data to implement recursion. These exploits modify the control-flow data on the stack. The solution to that is to *not* fix the functions. The solution is to use two stacks, ala Forth. Unlike Forth, C doesn't need to allow users access to any control-flow. So, by simply by providing a separate control-flow stack, the most damaging of C's exploits stop occuring. But, I don't see how any of this is that much different from Forth. Forth has a number of problems that can be exploited too. Allowing users to directly access the control-flow stack via >R R> R@ allows for a variety control-flow attacks. This is much easier to do in Forth than in C. Forth provides the mechanism to do so cleanly. C must be abused to do so. ALLOTing negative quantities could allow for dictionary attacks. Use of ' (tick) returning the execution address of dictionary words could allow for a dictionary attacks too. Use of ! (store) without ALLOT or , (comma) into the dictionary could allow for executable code to be stored and "hidden" there temporarily and therefore go undetected. Rod Pemberton
[toc] | [prev] | [next] | [standalone]
| From | anton@mips.complang.tuwien.ac.at (Anton Ertl) |
|---|---|
| Date | 2012-09-01 14:49 +0000 |
| Subject | Re: Function Points |
| Message-ID | <2012Sep1.164922@mips.complang.tuwien.ac.at> |
| In reply to | #15343 |
"Rod Pemberton" <do_not_have@notemailnot.cmm> writes:
>"Anton Ertl" <anton@mips.complang.tuwien.ac.at> wrote in message
>news:2012Aug31.123502@mips.complang.tuwien.ac.at...
>2) fgets() is unsafe too. It can also be passed input which exceeds the
>input buffer's length. There is nothing requiring the length passed to
>fgets() to be smaller or no more than the size of the input buffer.
>
>> OTOH, while strcpy() and strcat() can be used safely in theory,
>> this is quite cumbersome, so it is often not done, or not done
>> correctly, [...]
>
>False.
>
>They are not cumbersome nor frequently misused. I've never had a need for
>strncpy() or strncat() or other "safety" functions to prevent buffer
>overflows.
Sure, strncpy() and strncat() suck even more than strcpy() and strcat().
>> [...] and they are the source of many buffer overflows.
>
>False.
>
>They _can_ be the source of _some_ buffer overflows. I think you're basing
>this claim of "many" on the fact that someone created strlcpy() and
>strlcat().
I am actually basing this on reading reports on vulnerabilities that
mentioned unsafe use of strcpy() or strcat() as cause for the
vulnerability. At first I wondered why these functions would cause a
buffer overflow, given that the source string(s) is/are already in
memory and have passed the input checks on the inputs, but after some
time, I saw how typical C idioms might lead to such vulnerabilities.
>The solution to that is to *not* fix the functions. The
>solution is to use two stacks, ala Forth.
That will make attacks a little harder, but is not a proper solution.
As long as there are arbitrarily indirect pointers to code (and the
code is eventually executed through that indirection chain), a buffer
overflow that can manipulate such a pointer can make the program try
to execute code at any address. An example of such an indirect
pointer is the class pointer in C++ objects; in C, and function
pointers, pointers to structs that contain (among other things) a
function pointer, pointers to structs that contain pointers like the
one described above, etc.
>But, I don't see how any of this is that much different from Forth. Forth
>has a number of problems that can be exploited too. Allowing users to
>directly access the control-flow stack via >R R> R@ allows for a variety
>control-flow attacks.
>R R> R@ accesses the return stack, not the control-flow stack.
If you let write your application such that an untrusted end user can
manipulate the return stack arbitrarily, sure, you have opened up a
big hole. Most applications don't allow arbitrary manipulations of
the return stack to end-users, though.
If the development personell is not trusted, then Forth is definitely
not the right language for the project, but I doubt that any
general-purpose programming can be done in such a setting, whatever
the language. I guess that paranoid organizations have developed
methods to ensure they can trust the development personell as a whole,
even though they trust no single one person, but that's a pretty
exotic setting.
- 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 2012: http://www.euroforth.org/ef12/
[toc] | [prev] | [next] | [standalone]
| From | "Elizabeth D. Rather" <erather@forth.com> |
|---|---|
| Date | 2012-09-01 08:36 -1000 |
| Subject | Re: Function Points |
| Message-ID | <ZMGdnVl0C7BfyN_NnZ2dnUVZ_rOdnZ2d@supernews.com> |
| In reply to | #15363 |
On 9/1/12 4:49 AM, Anton Ertl wrote: > "Rod Pemberton" <do_not_have@notemailnot.cmm> writes: ... >> But, I don't see how any of this is that much different from Forth. Forth >> has a number of problems that can be exploited too. Allowing users to >> directly access the control-flow stack via >R R> R@ allows for a variety >> control-flow attacks. > >> R R> R@ accesses the return stack, not the control-flow stack. > > If you let write your application such that an untrusted end user can > manipulate the return stack arbitrarily, sure, you have opened up a > big hole. Most applications don't allow arbitrary manipulations of > the return stack to end-users, though. > > If the development personell is not trusted, then Forth is definitely > not the right language for the project, but I doubt that any > general-purpose programming can be done in such a setting, whatever > the language. I guess that paranoid organizations have developed > methods to ensure they can trust the development personell as a whole, > even though they trust no single one person, but that's a pretty > exotic setting. In general, Forth applications should not (and most do not) allow user access to the Forth interpreter or compiler. There are many ways to achieve this with complete security, ranging from a sealed wordlist at the top of the application to removing these features from a cross-compiled program altogether. Cheers, Elizabeth -- ================================================== Elizabeth D. Rather (US & Canada) 800-55-FORTH FORTH Inc. +1 310.999.6784 5959 West Century Blvd. Suite 700 Los Angeles, CA 90045 http://www.forth.com "Forth-based products and Services for real-time applications since 1973." ==================================================
[toc] | [prev] | [next] | [standalone]
| From | "Rod Pemberton" <do_not_have@notemailnot.cmm> |
|---|---|
| Date | 2012-09-01 16:11 -0400 |
| Subject | Re: Function Points |
| Message-ID | <k1tpvh$sof$1@speranza.aioe.org> |
| In reply to | #15363 |
"Anton Ertl" <anton@mips.complang.tuwien.ac.at> wrote in message news:2012Sep1.164922@mips.complang.tuwien.ac.at... > "Rod Pemberton" <do_not_have@notemailnot.cmm> writes: > >"Anton Ertl" <anton@mips.complang.tuwien.ac.at> wrote in message > >news:2012Aug31.123502@mips.complang.tuwien.ac.at... ... > >> [...] and they are the source of many buffer overflows. > > > >False. > > > >They _can_ be the source of _some_ buffer overflows. I think you're > > basing this claim of "many" on the fact that someone created strlcpy() > > and strlcat(). > > I am actually basing this on reading reports on vulnerabilities that > mentioned unsafe use of strcpy() or strcat() as cause for the > vulnerability. At first I wondered why these functions would cause a > buffer overflow, given that the source string(s) is/are already in > memory and have passed the input checks on the inputs, but after some > time, I saw how typical C idioms might lead to such vulnerabilities. From what I've seen, Forth's faults appear to be almost identical to those you believe are dangerous for C. Are you saying I can't CMOVE> doesn't copy into a buffer of unknown size just like C's strcpy()? CMOVE> doesn't take a size for the destination buffer. It takes a size for the source buffer. Look it up. I.e., someone can overflow the destination in Forth just like in C. Where's Forth fixed version of CMOVE> ? > >The solution to that is to *not* fix the functions. The > >solution is to use two stacks, ala Forth. > > That will make attacks a little harder, but is not a proper solution. Given the constraint of someone designing a new language, I'd agree that it isn't a proper solution to the problem. However, it is a proper solution to a language which has been in use for at least four decades. It doesn't interfere with the existing language. I seem to recall you and others here making the same basic argument in regards to "preserve the existing name" when asked why Forth creates new odd names for updated versions of Forth words. > As long as there are arbitrarily indirect pointers to code (and the > code is eventually executed through that indirection chain), a buffer > overflow that can manipulate such a pointer can make the program try > to execute code at any address. How is the XT from ' (tick) any different from a function pointer in C? How is storing an XT in a word to be executed any different from a function pointer in a struct in C? If it's changed by being overwritten it can execute any arbitrary Forth code and non-Forth code too. This Chinese attributed proverb comes to mind: "Don't complain about the snow on your neighbor's roof when your own doorstep is unclean.". I.e., it seems like you're complaining about C's problems when Forth has the same problems. Also, that comes with the constraint that there is no protection of code spaces from being written with data, and data spaces being prevented from executing code. That was true for decades, but not anymore. Modern microprocessor architectures have execution prevention. > > But, I don't see how any of this is that much different from Forth. > > Forth has a number of problems that can be exploited too. Allowing > > users to directly access the control-flow stack via >R R> R@ allows > > for a variety control-flow attacks. > > >R R> R@ accesses the return stack, not the control-flow stack. > ... which is typically the control-flow stack for Forth interpreters. Let's say you have two users: one with a C compiler on an OS coded in C and another with a Forth compiler on an OS coded in Forth (assume one exists). C doesn't provide direct access to it's control-flow. One must abuse C functions to create a breach. Forth typically did (or does) provide direct access via R> >R to control-flow. I.e., no abuse needed. > If you let write your application such that an untrusted end user can > manipulate the return stack arbitrarily, sure, you have opened up a > big hole. That's true for C too, in the sense that the end user can't manipulate C's control flow for a compiled application, if coded correctly. Someone has to make a mistake, or the OS allows untrusted code. > Most applications don't allow arbitrary manipulations of > the return stack to end-users, though. That's true for C too, in the sense that the end user can't manipulate C's control flow for a compiled application, if coded correctly. Someone has to make a mistake, or the OS allows untrusted code. Rod Pemberton
[toc] | [prev] | [next] | [standalone]
| From | Bernd Paysan <bernd.paysan@gmx.de> |
|---|---|
| Date | 2012-09-03 01:58 +0200 |
| Subject | Re: Function Points |
| Message-ID | <3217043.VBbpktjF1C@sunwukong.fritz.box> |
| In reply to | #15373 |
Rod Pemberton wrote: > Where's Forth fixed version of CMOVE> ? I give it another try: There is a "fixed" version of C, called Go. Go has a number of nice features you don't find as such in C, which resemble Forth. E.g. return multiple values. Or query the length of an array. Or create a sub"string" into the array, called "slice", which just behaves like an array, still has a length, and the 0 element is the start of the slice. That's how we *usually* deal with strings, arrays, buffers, etc. in Forth: We pass address *and* length around. That's the right way to do, passing only the address around is the wrong way to do. You are however free to shoot yourself into your foot in Forth if you like to. -- Bernd Paysan "If you want it done right, you have to do it yourself" http://bernd-paysan.de/
[toc] | [prev] | [next] | [standalone]
| From | Bernd Paysan <bernd.paysan@gmx.de> |
|---|---|
| Date | 2012-09-01 17:54 +0200 |
| Subject | Re: Function Points |
| Message-ID | <2093985.0hIZugUjCQ@sunwukong.fritz.box> |
| In reply to | #15343 |
Rod Pemberton wrote: > But, I don't see how any of this is that much different from Forth. > Forth > has a number of problems that can be exploited too. Allowing users to > directly access the control-flow stack via >R R> R@ allows for a > variety > control-flow attacks. This is much easier to do in Forth than in C. That's silly. If you allow an attacker to compile arbitrary Forth code while running the program, he won't need to use control-flow tricks to gain control. The point in C is that you can gain control by simply having an unexpectedly large field somewhere in a file or an input stream, and boom, your program goes astray. > Forth > provides the mechanism to do so cleanly. C must be abused to do so. Indeed, in C you couldn't even do what I described above: Let the attacker compile arbitrary code from source. In Forth, you can. If you deliberately want to expose the compiler to the end user, yes, it's possible. If you do, you better should sandbox the complete program. > ALLOTing negative quantities could allow for dictionary attacks. Use > of ' (tick) returning the execution address of dictionary words could > allow for a > dictionary attacks too. Use of ! (store) without ALLOT or , (comma) > into the dictionary could allow for executable code to be stored and > "hidden" there temporarily and therefore go undetected. And you allow input from unknown origin to do all these things? -- Bernd Paysan "If you want it done right, you have to do it yourself" http://bernd-paysan.de/
[toc] | [prev] | [next] | [standalone]
| From | "Rod Pemberton" <do_not_have@notemailnot.cmm> |
|---|---|
| Date | 2012-09-01 16:19 -0400 |
| Subject | Re: Function Points |
| Message-ID | <k1tqfr$u9l$1@speranza.aioe.org> |
| In reply to | #15365 |
"Bernd Paysan" <bernd.paysan@gmx.de> wrote in message news:2093985.0hIZugUjCQ@sunwukong.fritz.box... > Rod Pemberton wrote: > > But, I don't see how any of this is that much different from Forth. > > Forth > > has a number of problems that can be exploited too. Allowing users to > > directly access the control-flow stack via >R R> R@ allows for a > > variety > > control-flow attacks. This is much easier to do in Forth than in C. > > That's silly. If you allow an attacker to compile arbitrary Forth code > while running the program, he won't need to use control-flow tricks to > gain control. The same is true of C. You've changed the meaning of "gain control" above from that below. Above, you mean to gain control in any sense, but below you mean in the sense of taking control away from an operating system or application. > The point in C is that you can gain control by simply > having an unexpectedly large field somewhere in a file > or an input stream, and boom, your program goes astray. That's true for C only if someone made a coding mistake, or uses gets(). If coded correctly, that doesn't happen, except for gets(). Forth has unbounded user input too: KEY. Forth uses addresses to identify buffers and code: PAD, address returned by words created by VARIABLE etc. Anton just complained about function pointers in C being abused. E.g., how is ' (tick) any different from a function pointer in C? I'm clearly not familiar with all of Forth, and especially not ANSI Forth. However, it seems to me that Forth has almost identical issues to C and a few more. > > ALLOTing negative quantities could allow for dictionary attacks. Use > > of ' (tick) returning the execution address of dictionary words could > > allow for a > > dictionary attacks too. Use of ! (store) without ALLOT or , (comma) > > into the dictionary could allow for executable code to be stored and > > "hidden" there temporarily and therefore go undetected. > > And you allow input from unknown origin to do all these things? > If it's interpreted Forth, how do you not? If it's compiled Forth and the end user has access to the compiler, how do you not? Rod Pemberton
[toc] | [prev] | [next] | [standalone]
| From | Bernd Paysan <bernd.paysan@gmx.de> |
|---|---|
| Date | 2012-09-02 03:05 +0200 |
| Subject | Re: Function Points |
| Message-ID | <1469952.zgSDYajGMJ@sunwukong.fritz.box> |
| In reply to | #15375 |
Rod Pemberton wrote: > Forth has unbounded user input too: KEY KEY is definitely bounded to return exactly *one* key input. -- Bernd Paysan "If you want it done right, you have to do it yourself" http://bernd-paysan.de/
[toc] | [prev] | [next] | [standalone]
| From | Coos Haak <chforth@hccnet.nl> |
|---|---|
| Date | 2012-08-31 23:10 +0200 |
| Subject | Re: Function Points |
| Message-ID | <1mkoywfgs335o$.1tp512yk0foq0$.dlg@40tude.net> |
| In reply to | #15309 |
Op Fri, 31 Aug 2012 03:29:38 -0700 (PDT) schreef Mark Wills: <snip> >: BUFFER ( interpretation: size "name" -- children: -- address size) > CREATE DUP , ALLOT ALIGN DOES> DUP @ SWAP 1 CELLS+ SWAP ; Why use ALIGN here? If this word is followed by a word that uses CREATE then its data field is always aligned, like the data comma'ed (DUP ,) Perhaps you wanted .. DUP , ALIGNED ALLOT DOES> .. -- Coos CHForth, 16 bit DOS applications http://home.hccnet.nl/j.j.haak/forth.html
[toc] | [prev] | [next] | [standalone]
| From | "Elizabeth D. Rather" <erather@forth.com> |
|---|---|
| Date | 2012-08-31 15:50 -1000 |
| Subject | Re: Function Points |
| Message-ID | <8a-dnalZ7eF19NzNnZ2dnUVZ_hWdnZ2d@supernews.com> |
| In reply to | #15309 |
On 8/31/12 12:29 AM, Mark Wills wrote:
...
> If we had a dedicated word for creating buffers that took a parameter
> on creation then the problem would be essentially solved:
>
> : BUFFER ( interpretation: size "name" -- children: -- address size)
> CREATE DUP , ALLOT ALIGN DOES> DUP @ SWAP 1 CELLS+ SWAP ;
>
> Well, 'solved' in the sense that children of BUFFER report their
> allocation size on the stack, in addition to their buffer address when
> referenced, so there would be no excuse for lazy programmers to allow
> their code to read/write beyond the end of a buffer.
>
> The above makes their usage in loops reasonably 'safe':
>
> 100 BUFFER MyBuf
> : SeeBuffer MyBuf 0 DO DUP I + C@ . LOOP DROP ;
>
> That's probably as safe as we can get without using dedicated buffer
> fetch and store words/primitives that do bounds checks.
Here's a simpler way (cell-wise example):
: BUFFER ( size -- ) CREATE DUP , CELLS ALLOT
DOES> ( i -- a ) DUP @ >R ( i a ) OVER 0 R> WITHIN IF \ Legal
SWAP 1+ CELLS + ELSE 10 THROW THEN ;
This takes an index and returns the indexed cell's address. Example:
10 CONSTANT SIZE
SIZE BUFFER MY-STUFF
: SHOW ( -- ) SIZE 0 DO I MY-STUFF @ . LOOP ;
Then you always supply the index, and the check will be provided.
Doesn't require external variables or error-checking routines. You
should, of course, define your throw code as a nicely named constant.
Of course you aren't prevented from saying:
0 MY-STUFF 100 ERASE
...but you're protected against most common errors.
> It's nice that we can 'roll our own' buffer handling words such as the
> above, however, there's nothing about the above that couldn't be
> reproduced in C with a simple struct, which makes me think that C's
> somewhat bad reputation (with regard to buffer overflows/overruns) is
> not really down to the languge itself, but rather just pure lazy
> programming!
>
> I have previously lamented over the lack of 'true' buffers in Forth,
> but the ease with which one can roll their own is possibly why it is
> an area that hasn't been standardised.
Bingo, that's exactly why. Every particular situation has slightly
different needs and constraints, and you can tailor your buffer designs
specifically to those.
Cheers,
Elizabeth
--
==================================================
Elizabeth D. Rather (US & Canada) 800-55-FORTH
FORTH Inc. +1 310.999.6784
5959 West Century Blvd. Suite 700
Los Angeles, CA 90045
http://www.forth.com
"Forth-based products and Services for real-time
applications since 1973."
==================================================
[toc] | [prev] | [next] | [standalone]
| From | Paul Rubin <no.email@nospam.invalid> |
|---|---|
| Date | 2012-09-01 10:31 -0700 |
| Subject | Re: Function Points |
| Message-ID | <7xwr0d8xab.fsf@ruckus.brouhaha.com> |
| In reply to | #15280 |
Bernd Paysan <bernd.paysan@gmx.de> writes:
>> "This program must never dereference a null pointer for any input" is
>> simple enough to specify
> But C's main problem is one fundamental mistake: buffers are passed
> around as pointers, without length.
Leaving aside the tangent about subscript checking (which is a difficult
problem in any language), remember the example I gave was about null
pointers, not subscript errors. Java checks subscripts, but it also has
null pointers and null pointer exceptions (NPE). ML and Haskell get rid
of NPE by using option types instead of null pointers.
Similarly for array subscripts: in FP style, one typically does array
operations using higher-order functions like map and fold, eliminating
quite a few potential subscript errors by simply getting rid of the
subscripts. There are of course places where subscripts are still
needed, and those are subject to the usual hazards.
>> [Balanced trees] let you ... traverse the keys in order.
> In what order? Alphabetical order? Does that matter? Do you really
> want all fruits from apples to bananas listed?
Sure, that is very normal in query systems. Think of a bug tracker
where you can view all the open bugs in order of newest first, most
recently updated first, highest priority first, name of reporter
(alphabetical), name of person assigned to fix the bug, etc. Most of
those fields can be updated at any time.
> Database implementers like B-trees particularly, because they can easily
> be made transaction-safe. I.e. when you do a transaction, you copy the
> parts of the tree which contain the new state, and then you only update
> the root pointer
Yes, this is similar to the persistence feature of AVL or red-black
trees as used in functional programming.
> For me, this sort of B-trees or priority queues are problems which you
> face during university, because they are popular data structures. In
> "real life", they don't happen that often. If you really need them, you
> write them once, and then they are part of your toolbox.
Why would I write them even once? There are highly tuned library
implementations already, so I use those, and I do use them often.
> The priority queue I wrote (for MINOS) didn't get a complicated data
> structure, because the usual case is that there aren't many events
> waiting. .... It is O(n), but the constant overhead is very low.
Yeah, that's something like what I ended up doing in the Python program
I mentioned. It's good enough for the program's current workload, so
fine. But I'd prefer to have been able to call a library routine that
did the right thing even for large N. I've been wondering, for example,
how Forth multitaskers handle event scheduling when there are a large
number of tasks, and how many tasks the traditional systems typically
ran. It certainly seems realistic to want to handle N>10000 in today's
high concurrency systems.
> I've made some thought about how I would implement the priority queue of
> a gate-level simulator, and my preferred data structure would be an
> array with a fixed time scale,
If you don't have to reschedule events after they've been added, it
sounds best to use a traditional binary heap. Those are space-efficient
and easy to implement. The Python library doc has a reasonable
description of how they work ("theory" section at end):
http://docs.python.org/library/heapq.html
> if your fixed time scale is less than the minimum delay..
> With the "constant time scale per schedule bucket = minimum delay"
> equation mentioned above, I'd be curious how that would look in Coq.
I'm not sure I understand the problem, but it sounds like:
1) you want to have buckets of size h, which means that if there's
an event at time t0, the next bucket starts at t1 for some
t1 <= t0+h.
2) if the event at time t0 spawns a new event, the new event is
at time t0+dt for some dt>=h.
This doesn't sound terribly hard to formalize. Then, given dt>=h, you
want to prove t0+dt>=t0+h, which should be trivial in any reasonable
proof system. I don't yet know how to actually do anything like that in
Coq, though.
There is an article "The Seventeen Provers of the World" showing proofs
that sqrt(2) is irrational in that many systems:
http://www.cs.ru.nl/~freek/comparison/
[toc] | [prev] | [next] | [standalone]
| From | Bernd Paysan <bernd.paysan@gmx.de> |
|---|---|
| Date | 2012-09-01 21:52 +0200 |
| Subject | Re: Function Points |
| Message-ID | <2000935.ViCZX3HiHH@sunwukong.fritz.box> |
| In reply to | #15368 |
Paul Rubin wrote:
> Leaving aside the tangent about subscript checking (which is a
> difficult problem in any language), remember the example I gave was
> about null
> pointers, not subscript errors. Java checks subscripts, but it also
> has
> null pointers and null pointer exceptions (NPE). ML and Haskell get
> rid of NPE by using option types instead of null pointers.
C somewhat has NPEs, too, through signals and setsigjmp. C's exception
handling is not really up to date ;-). Lisp-like languages always had a
NIL thing, which wasn't quite the same as a null pointer.
> Similarly for array subscripts: in FP style, one typically does array
> operations using higher-order functions like map and fold, eliminating
> quite a few potential subscript errors by simply getting rid of the
> subscripts.
Yes, that's generally a good idea to do it that way. In Forth, we use
"design patterns" like
( addr u ) bounds ?DO
I ...
<size> +LOOP
which aren't prone to off-by-one errors like C's
for(i=0; i<n; i++) {
...
}
statement (many people write "i<=n", because they count from 1..n, but
in fact, C counts from 0..n-1).
> There are of course places where subscripts are still
> needed, and those are subject to the usual hazards.
Of course. Either prove that the index always will match the bound or
check...
>>> [Balanced trees] let you ... traverse the keys in order.
>> In what order? Alphabetical order? Does that matter? Do you really
>> want all fruits from apples to bananas listed?
>
> Sure, that is very normal in query systems. Think of a bug tracker
> where you can view all the open bugs in order of newest first, most
> recently updated first, highest priority first, name of reporter
> (alphabetical), name of person assigned to fix the bug, etc. Most of
> those fields can be updated at any time.
Yes, but that are sorted indices, which remain sorted all the time, so
all you need is to have a insert and delete operation into them which
isn't costly.
Example: Forth's dictionary has a "newest first" order, not only in
search, but also when you list it with WORDS. So in Gforth, we keep the
linked list of all words as "index" into the dictionary. Access goes
through the hash, though. Such an index is quite compact (one cell per
item), and if you want to list all apples to bananas, you search for
apples and bananas in the hash, and then walk the "sorted by name" list
starting with apples until you match bananas.
You might use a B-tree or some similar data structure to keep these
indices sorted, but you don't actually use them to search for elements,
because the hash is faster.
> Why would I write them even once? There are highly tuned library
> implementations already, so I use those, and I do use them often.
Yes, in fact, usually, you treat such building blocks as given. In
Forth maybe not... so you may need to write them *once*.
> Yeah, that's something like what I ended up doing in the Python
> program
> I mentioned. It's good enough for the program's current workload, so
> fine. But I'd prefer to have been able to call a library routine that
> did the right thing even for large N.
Even when it's the wrong thing for small N? The small-N priority queue
has a very small constant overhead, and very small code size, so it is
better for small Ns than a binary heap.
> I've been wondering, for
> example, how Forth multitaskers handle event scheduling when there are
> a large number of tasks, and how many tasks the traditional systems
> typically
> ran. It certainly seems realistic to want to handle N>10000 in
> today's high concurrency systems.
The traditional Forth multitaskers ran on single-core systems. The one
I wrote for bigForth has two double-linked queues: active and sleeping,
so event scheduling (wake up a task) is a O(1) operation. Traditional
multitaskers are round-robin, so there is not much need for locks or
similar thoughts. If you want single core, but many tasks (each of
which does only a little thing and then goes to sleep again), the
traditional Forth multitasker is much better than POSIX threads, which
aren't all that lightweight.
> If you don't have to reschedule events after they've been added, it
> sounds best to use a traditional binary heap. Those are
> space-efficient
> and easy to implement. The Python library doc has a reasonable
> description of how they work ("theory" section at end):
>
> http://docs.python.org/library/heapq.html
Yes, they also have the nice property that you don't have to care about
their balance, only to reestablish the invariance. A heap is partially
sorted, i.e. you don't actually know where the largest element is, but
you always know where the smallest element is. Maybe I should write one
this evening, it's always useful to have such data structures at hand.
>> if your fixed time scale is less than the minimum delay..
>> With the "constant time scale per schedule bucket = minimum delay"
>> equation mentioned above, I'd be curious how that would look in Coq.
>
> I'm not sure I understand the problem, but it sounds like:
> 1) you want to have buckets of size h, which means that if there's
> an event at time t0, the next bucket starts at t1 for some
> t1 <= t0+h.
> 2) if the event at time t0 spawns a new event, the new event is
> at time t0+dt for some dt>=h.
>
> This doesn't sound terribly hard to formalize. Then, given dt>=h, you
> want to prove t0+dt>=t0+h, which should be trivial in any reasonable
> proof system. I don't yet know how to actually do anything like that
> in Coq, though.
Yes, I think it should not be hard to formalize, which is why I would be
courious how it looks in Coq.
> There is an article "The Seventeen Provers of the World" showing
> proofs that sqrt(2) is irrational in that many systems:
>
> http://www.cs.ru.nl/~freek/comparison/
Nice comparison.
--
Bernd Paysan
"If you want it done right, you have to do it yourself"
http://bernd-paysan.de/
[toc] | [prev] | [next] | [standalone]
Page 6 of 9 — ← Prev page 1 2 3 4 5 [6] 7 8 9 Next page →
Back to top | Article view | comp.lang.forth
csiph-web