2 Pragma Semantics
Primitive methods written in a language other than Vortex RTL (e.g. C++) are called external primitives, since Vortex cannot reason about their behavior. Vortex needs to know their behavior, however, and this behavior is documented in a set of pragmas. Usually, pragmas can be omitted and Vortex will make conservative assumptions, but sometimes Vortex makes optimistic assumptions (that reflect the vast majority of cases), and some pragmas Vortex requires of all external primitives, at least when performing certain analyses such as interprocedural analysis. The following non-conservative characteristics are assumed of external primitives:
sends or sends_anything pragma is specified, an external primitive is assumed to not send any messages or otherwise invoke any methods or procedures compiled by Vortex.
has_nlr or has_no_nlr pragma is present, an external primitive is assumed to possibly result in a non-local return/exception exactly if one of its callees does.
has_side_effects or has_no_side_effects pragma is present, an external primitive is assumed to possibly modify exactly the union of those variables possibly modified by its callees.
To document less conservative behavior we support several pragmas on external primitive method declarations:
sends(v1 = m1([t11,t22],[t21]), m2([t11,t12,v1]), ...) specifies the messages sent by the external primitive. The argument vectors specify the argument class sets. The notation v1 = m1 º introduces a variable that represents the set of classes returned by m1. Each message has a list of vectors, each vector representing a set of classes for that argument. Each t in a vector may be unknown, the name of a formal variable, the name of a variable declared as a result of an earlier send in the sends pragma, or the name of a class.
sends_anything specifies that the method may send any message with any possible argument classes.
return_type(t1,t2,t3...tn) indicates that the primitive method is guaranteed to return one of t1...tn, with the same allowed form of the ti's as in the sends pragma.
does_not_return indicates that the primitive doesn't return normally (e.g., it always exits with a non-local return or error).
has_nlr indicates that the external method may result in a non-local return/exception (needed only if no callee may result in a non-local return). has_no_nlr indicates that the method does not end in a non-local return, even if one of its callees may, e.g. the primitive catches and suppresses all non-local returns.
has_no_side_effects indicates that the external primitive does not modify any variables, even if its callees might. has_side_effects indicates that the external primitive might modify (unknown) variables in addition to what its callees might modify.
formals_escape(...,t,...,f,...) indicates which formals of the method may escape, i.e., may be referenced by some other external primitive after this external primitive returns. The formals_escape pragma has a list of ts and/or fs, one per formal of the external primitive, with f indicating that the corresponding formal definitely doesn't escape. [A better syntax would list the names of possibly-escaping formals.]