Add return types to procedures

[jubnzv]

This PR introduces the return keyword and the Return statement in the AST:

procedure foo() -> String
  a = my_string;
  return a;
end

Design decisions in the current implementation:

• return takes as an argument a single variable with the return value. It seems natural for me to use this approach in the ANF-based language.
• Don't support empty return statements (return;) for early exit when the procedure has no a return type. e.g. the following code is forbidden:

procedure no_return()
  match something with
  | 0 => (* do something *)
  | _ => return; (* typechecking error: cannot use an empty return for early exit *)
  end
end

• Gas cost of the return call is 1. We should discuss and document this constant.
• Use cram tests to check the typechecker because of scilla-checker: Use JSON output format for type checking errors #1196

TODO:

• Eval support
• Forbid usage of such procedures in Iterate statements
• Dynamic behavior tests

Closes #578

[jjcnn]

First of all, we need a fix to the concrete syntax for return statements.

Second, we need to restrict return types to non-maps, for consistency.

Third, I'd like a few more checks and tests:

• Code that follows a return statement is dead, so shouldn't be allowed (note that this may not be needed, depending on how we change the concrete return syntax). For tests, we should also test that this works inside match statements.
• For procedures with return types all branches of the procedure body should return a value. (Same caveat about return syntax as before)
• Test: A procedure with a return type that is an address type should be able to return a value of a more specific type than the specified return type, and should not be able to return a value of a more general type than the specified return type.
• Test: A returning procedure that calls another returning procedure. This is relevant to test because of the way EvalUtil.ml handles return values. Also add a test where the calls go returning->non-returning->returning, just in case.

[jjcnn]

We should add better error messages to all the new cases in ParserFaults.messages, but let's wait until all the syntax changes of v0.14 are ready.

[jubnzv]

Thanks for the review!

First of all, we need a fix to the concrete syntax for return statements.

We should discuss the better syntax, which will be more convenient to developers. I suppose, we want to left semantics and abstract syntax as they're implemented.

Second, we need to restrict return types to non-maps, for consistency.

Done.

Code that follows a return statement is dead, so shouldn't be allowed (note that this may not be needed, depending on how we change the concrete return syntax). For tests, we should also test that this works inside match statements.

Done for the current implementation.

For procedures with return types all branches of the procedure body should return a value. (Same caveat about return syntax as before)

Done.

Test: A procedure with a return type that is an address type should be able to return a value of a more specific type than the specified return type, and should not be able to return a value of a more general type than the specified return type.

Could you please provide a minimal example for this?
As I understood, the actual return address may do not contain fields specified in the procedure signature?

Test: A returning procedure that calls another returning procedure. This is relevant to test because of the way EvalUtil.ml handles return values. Also add a test where the calls go returning->non-returning->returning, just in case.

Done. The test for dynamic behavior of returns (procedure-return-1.scilla) was improved.

[jjcnn]

Test: A procedure with a return type that is an address type should be able to return a value of a more specific type than the specified return type, and should not be able to return a value of a more general type than the specified return type.

Could you please provide a minimal example for this?
As I understood, the actual return address may do not contain fields specified in the procedure signature?

No, it's the other way around: The actual return address must contain all the fields specified in the procedure signature, but may contain more fields. In other words, the actual address must be assignable to the address in the procedure signature.

I think you've implemented the typecheck correctly, but I'd like there to be a test case for it, e.g.:

procedure (x : ByStr20 with contract field y : Uint128, field y : Bool end) : ByStr20 with contract field x : Uint128 end
  _return := x
end

Also, ideally, a negative test the other way around, just to make sure we're using assignable the right way around.

It's not necessary to do extensive testing of type_assignable here, though, because we have fairly extensive test cases for that elsewhere.

[rrw-zilliqa]

Looks (broadly) good to me, in that I can't see any obvious bugs...