Main methods should support a return value/process exit code

[robin-aws]

Split off from the resolved #1116 - I should have known better than to tack this on to an existing issue. :)

The design of this feature may actually be non-trivial: what is the optimal return type for a main method? Different environments support different ranges of values: the POSIX wait() syscall only provides the least significant 8 bits, but many other contexts support 32 bits, sometimes signed and sometimes unsigned.

At the one extreme we could allow a return type of int and assume each backend will raise a runtime error if an exit code is out-of-range for the particular environment. This would be unsatisfying for an otherwise tightly specified and verified system.

At the other extreme we could go for the lowest common denominator (and cover the vast majority of use cases) by only supporting a bool result, with false and true mapped consistently to 0 and 1. This would surely frustrate some users that would prefer more fidelity in communicating errors to parent processes, though.

[cpitclaudel]

At the other extreme we could go for the lowest common denominator (and cover the vast majority of use cases) by only supporting a bool result, with false and true mapped consistently to 0 and 1.

Are there any systems that don't support -128..128?

[davidcok]

Suggest that in Dafny it be 'int' Compilers can translate that as appropriate, but expect that 0 is normal operation, and signed or unsigned small int values are errors of various sorts.

[MikaelMayer]

I would prefer "int" as well so that someone wanting to use Dafny as a verified language to compile in theirs can use this without surprise. We don't guarantee anything more than the Dafny code normally, so anything beyond stating neutrally that the main method returns an int is currently out of scope.

As a precedent, we don't guarantee that the first argument passed to main is the name of the executable, sometimes it's the file being executed, depending on the run-time.

We could let implementers access some constants to decide what is the compiler and raise a different number based on that, down the road. It might even be feasible already through the use of {:extern}, anyway

[cpitclaudel]

Maybe we can warn on numbers outside of a safe range (which, upon looking at the BSD docs, seems to be 0..64 rather than 0..255). Or even disallow them — Main is never going be called from Dafny, so its return code is only relevant to interaction with external processes.

so anything beyond stating neutrally that the main method returns an int is currently out of scope.

Don't we need to say something about what happens to that number?

[MikaelMayer]

Don't we need to say something about what happens to that number?

Why?

[davidcok]

As a user I would expect that the return value from Dafny's Main would be the exit value of the executable program compiled in the target language. That is a reasonable expectation to state about the behavior of Dafny's various compilers.

[cpitclaudel]

Why?

What @davidcok said above: the point of this feature is to control the exit code of the program once compiled, right? If so, we should document how this new return parameter of main enables this, no?

[cpitclaudel]

Btw, one thing I just realized: currently we always return 0 from Dafny-compiled programs. If we change to allowing main to return an int, we probably want to make sure that that int obeys the definite-assignment rules. Otherwise we will have code like this:

method Main() returns (r: int) {
  print "Hi!\n";
}

With r left unassigned this could return anything, not just 0, which is a deviation from the behavior users may expect from other languages.

[MikaelMayer]

we probably want to make sure that that int obeys the definite-assignment rules

Good remark !

What @davidcok said above: the point of this feature is to control the exit code of the program once compiled, right?

Right, but how much does it differ from the exit code returned by the main method?

[cpitclaudel]

Right, but how much does it differ from the exit code returned by the main method?

Not sure whether I understand the question, sorry :/ Dafny ints are unbounded, and no OS supports unbounded return codes, so they will differ unless we restrict return codes, right?

[MikaelMayer]

I see. Here is my suggestion: We just truncate the returned biginteger / truncate to whatever number the normal type the method Main() needs, in every language. That way, we don't need to say something in general about all the languages. !t's practical :no need to enforce that the result of Main has to be within certain ranges.

[cpitclaudel]

This is odd: we don't do that with other functions that return ints.

[cpitclaudel]

If you were modeling an extern function called "SetExitCode", wouldn't you give it a type that reflects what it actually accepts? Typically we model externs as taking bounded ints when they do, rather than truncating inputs.

[davidcok]

But in the case of externs one has to tailor it differently, potentially, for every different target.

I like the simplicity of Mikael's proposal -- Main returns an int, and the target language does something sensible that the users might expect -- with no particular guarantees for values outside the target's range.

[cpitclaudel]

I like the simplicity of Mikael's proposal -- Main returns an int, and the target language does something sensible that the users might expect -- with no particular guarantees for values outside the target's range.

That comes close to "int overflow is unspecified", which I don't like too much if we're talking about Dafny :/ The consequences are likely less grave, but I wouldn't be surprised if in the future someone writes this:

method Main(args: seq<string>) returns (ret: int) {
  var numberOfErrors: int := DoWork(args);
  return numberOfErrors;
}

… and then finds themselves surprised when returning numberOfErrors == 256 causes the program to return 0 on the command line.

Adding a subset constraint will cost nothing in the vast majority of cases (where the return value is a constant), and will catch cases like the above.

[MikaelMayer]

I don't think one would ever use the int returned from main as a counter. Adding a subset constraint requires that we change the type of "int" to another one which needs to be explicitly introduced, either from a standard library file, or built-in. Or perhaps you were thinking about adding an implicit postcondition in the translator?