Procedure call parameter-passing abstraction

[ailrst]

This adds a transform (behind the flag --parameter-form) which lifts all registers to local variables passed via procedure parameters.

Procedures now have a list of formal input parameters and output parameters, as well as a default mapping from these parameters to the actual parameters for use at calls to these procedures (this is set up by the front end and procedure form transform, and used by the spec loader and output pass).

• input parameters: are immutable parameters which are referred to by name in basil IR (not positional), their bindings must always be passed through the 'actualParams' field of DirectCall.
• output parameters: are also referred to by name, but can never be referred to in the program, they are bound through the mapping from name to expression inside Return() statements (unlike boogie we can return local variables rather than having a special variable). The Directcall then binds these to its mapping outParams, from formal out param name to lexpr variable.

So now we have

procedure target(a_in, b_in, c_in) returns (a_out, b_out, c_out):
    a, b, c := a_in, b_in, c_in
    ...
    return(a,b,c)

returns have the following meaning, where the a_out etc. are the formal out parameters of the procedure.

return(a,b,c) ===
    a_out, b_out, c_out = a, b c; 
    return

Similarly, calls provide the actual in parameters (a,b,c), and the actual return parameters (a', b', c').

DirectCall(target, label, (a', b', c'), (a, b, c) ===
    a_in, b_in, c_in = a, b c;
    call target
    a', b', c' = a_out, b_out, c_out

• when parameter-form is disabled

  • parameters are only used by the spec loader, then removed from the ir. to e.g. in specs main_argc is replaced by R0[31:0] and the parameters attached to procedures are removed
  • it would be better to pass these outside the procedures formal parameters, e.g. procname_result is silly as it slices the register and is excluded from the outparam list and handled as a special case in the spec loader.

• when enabled

  • ANR is used to add registers to the formal input parameter list, e.g. all named 'R0_in', and assignments are added to assign these to the regular register variables at the start of the procedure
  • all variables assigned in the procedure are returned through the return statement.
  • all variables are changed to locals

• use LocalVar to describe the parameters.

                  var formalInParam: mutable.SortedSet[LocalVar],
                  var formalOutParam: mutable.SortedSet[LocalVar],
                  var inParamDefaultBinding: immutable.SortedMap[LocalVar, Expr],           // for call site
                  var outParamDefaultBinding: immutable.SortedMap[LocalVar, Variable], // for call site

Generally this is motivated by the static analysis and program transforms, as parameter passing means the ssa form and interpretation def/use chains work across procedure calls more naturally. We probably don't want to enable this by default now, but I will try building the analysis on top of it and refine it as needed, but this provides the basis. I may implement the inverse transform too if it makes sense.