search

frankpfenning / C0

C0 Language
4 stars 0 forks source link

Unsafe programs with \length #26

Closed robsimmons closed 11 years ago

robsimmons commented 11 years ago

Currently, unsafe programs do not have any way of handling \length, because the length is quite simply not stored with the array.

But that causes the linker to go wrong when compiling a program in the unsafe runtime with -d and \length in contracts, which can't possibly be the right answer.

Options:

The second option seems like the right one, but it also seems like it might be the most work.

This error causes many failures if we make checkunsafe.

frankpfenning commented 11 years ago

I think the right answer is to disallow -d.

The unsafe runtime only exists for speeding up code you have thoroughly tested, so -d is unnecessary here. I believe in the early days of the regression test, we qualified those that would not work with the unsafe runtime, but it would be nice to have a more general solution like your first bullet.

On Sun, Dec 9, 2012 at 1:53 AM, Robert J. Simmons notifications@github.comwrote:

Currently, unsafe programs do not have any way of handling \length, because the length is quite simply not stored with the array.

But that causes the linker to go wrong when compiling a program in the unsafe runtime with -d and \length in contracts, which can't possibly be the right answer.

Options:

  • Disallow -d with the unsafe runtime
  • Disallow \length with the unsafe runtime
  • Define \length in the unsafe runtime to say something silly, like 0

The second option seems like the right one, but it also seems like it might be the most work.

This error causes many failures if we make checkunsafe.

— Reply to this email directly or view it on GitHubhttps://github.com/frankpfenning/C0/issues/26.

robsimmons commented 11 years ago

Revision 182 disallows the -runsafe and -d combination. The regression test still has the ability to disallow certain tests (safe => return 12), and we could now add something like

!safe => error; safe => return 12

since the -d and -runsafe combination will cause a compiler error every time.