Call preserved / ABI

[JTrenerry]

Thought I would move #145 to something that is open so it is easier to keep track of.

The SSA analysis also uses this since it is practically a direct port from BASIL. Do you want this removed?

We need a systematic approach to abi not hacks in each individual transform/analysis

Not sure how to remove the hacky part, but removing those registers from the return values fixes the issue of each transform/analysis needing to do it.

[agle]

Bincaml takes as input arbitrary IR programs so any transform or analysis which has special interpretations of specific variable names is inherently incorrect wrt to the semantics of the program (i.e. there could be no proof of its correctness using only the IR semantics).

For external procedures: in bincaml we have an explicit modifies set which we assume for the external procedures, the ABI assumption can be encoded using a transform which drops the known-preserved procedures, and is run before the parameter pass. Notably this is not implemented in the transform which injects the assumed modifies set itself as that should simply be all global mutable variables so as to be abi independent.

For defined procedures: The correctness condition for code transforms is that they preserve the semantics of the program. The typical path here is proving this with a sound static analysis, but its often beneficial to assume some structure exists like the abi and prove it later. In order to do this we can defer the proof by injecting an assertion which motivates the transform. In this case we can add to the end of every procedure an assertion that the returned value is equal to the input value and discard the output parameter (inlining the definition at the call site). This means we safely get a verification failure if the assumption did not hold for a given IR program. Such a transform is implemented at BASIL https://github.com/UQ-PAC/BASIL/blob/main/src/main/scala/ir/transforms/CalleePreservedParam.scala.

SSA does not use any heuristic like this but I assume you mean SVA which does. In this case yes it has the same problem but as its an inherent requirement of the analysis (rather than just a precision improvement) its more just a code organisation/maintainability issue. I would like to make this interpretation as a special register be driven by some explicit annotation, such as an attribute field designating a variable's use as SP, LR etc. which can be automatically annotated in a transform pass. In general I would like to define an aarch64 ABI module we can silo all these heuristics into.