Precondition failure on main() leads to segmentation fault

[robsimmons]

The policy of passing caller information as an extra argument (for reporting @requires failures) causes the runtime to attempt to access an invalid pointer in the event that the @requires for main() fails.

/* ruhroh.c0 */
int main() 
//@requires false;
{
  return 0;
}

bash-3.2$ cc0 ruhroh.c0 -d
bash-3.2$ ./a.out
Segmentation fault

[robsimmons]

Triggered in regression suite (r137):

tests/rjs-basic/ruhroh.c0

[robsimmons]

So, it's easy to see that this is a bug. But what's the fix? I feel our best choices may be:

• special case the main function itself
• special case all zero-argument functions (it makes no sense for a function with zero arguments to even have a precondition!!!)
• add a level of indirection - cause the runtime to call a different main(). this is less desirable because of the problem Carsten originally observed - we'd like the VM to produce code where main has no arguments, even with -d is flagged

[robarnold]

I would argue that you could have a precondition on a function with zero arguments if it had some secret global state. An example might be some IO library function operating on a stdin/out/err (readline? print?) which require !eof(<secretstate>). What if you wanted to express program argument dependencies in main?

Perhaps such dependencies can be hidden by the platform. For example: the socket API on windows requires you to call an initializer function before using any of them; should that be an invariant or implicitly called by wrappers around all socket functions? Note that Haskell requires you to invoke it explicitly on windows but doesn't check that you have when running on unix platforms (for better or worse).

[frankpfenning]

We already treat library functions specially by not augmenting the argument list with a caller location argument. Main is the other way that c0 programs interact with their environment so I think it is consistent not to add the extra argument to main.

• Frank

Sent from my iPhone

On Nov 23, 2012, at 11:15 PM, "Robert J. Simmons" notifications@github.com wrote:

So, it's easy to see that this is a bug. But what's the fix? I feel our best choices may be:

special case the main function itself special case all zero-argument functions (it makes no sense for a function with zero arguments to even have a precondition!!!) add a level of indirection - cause the runtime to call a different main(). this is less desirable because of the problem Carsten originally observed - we'd like the VM to produce code where main has no arguments, even with -d is flagged — Reply to this email directly or view it on GitHub.

[robsimmons]

Resolved this in revision 166 according to Frank's suggestion. The main function under -d has a local variable _caller that is initialized to (none) so that, in the case that a precondition of main fails, there is a fake caller to report.