		Search-engine friendly clone of the ACL2 documentation.

Atj-pre-translation

Atj-pre-translation-array-analysis

Pre-translation step performed by ATJ: single-threadedness analysis of Java primitive arrays.

In order to generate Java code that correctly destructively updates (primitive) arrays, we perform a stobj-like analysis to establish that arrays are treated single-threadedly in the ACL2 functions that are translated to Java.

Unlike the other pre-translation steps, this analysis does not modify the ACL2 function bodies. However, this analysis is best carried out between the type annotation pre-translation step and the variable reuse pre-translation step. The reason why this analysis should be carried out after the type annotation step is that we need the type annotations to determine where the arrays are, and subject them to the analysis. The reason why this analysis should be carried out before the variable reuse step is that this step may mark and differentiate array variables that the analysis needs to ensure that they denote the same array so that the array is treated single-threadedly.

This array analysis is similar to ACL2's stobj analysis in the sense that it imposes the same draconian constraints on the use of arrays, namely that the same name is consistently used for each array, that functions with array inputs are passed those names, that every array possibly modified by a function is bound to the same name and is also returned by the surrounding function, and so on.

However, this array analysis also differs from the stobj analysis, because stobjs are global variables whose names must be consistently used by all the functions that manipulate them. In contrast, (representations of) Java arrays in ACL2 functions do not have global names, but their names are local to the functions. Consider a function f that takes two arrays as inputs and returns them (possibly modified) as outputs, and a function g that takes two array inputs a and b and calls f on them: we need to know how the two array outputs of g correspond to the array inputs of g, so that we can check that f properly binds the possibly modified array a to the variable a and the possibly modified array b to the variable b. In ACL2's stobj analysis, g will have the stobjs-out property that says which results are which stobjs, using their global names (except the case in which g is the same as or mutually recursive with f, in which case ACL2 presumably uses the non-recursive branches of the clique to determine the output stobjs of the functions). In our array analysis, we need something like the stobjs-out property: we do that beforehand (i.e. before the array analysis) via atj-main-function-type and atj-other-function-type, which allow the specification of output array names. But since array names are not global as pointed out above, output array names in the ATJ function type tables alone do not suffice. We need to take into account the ``mapping'' between input array names (which are the formal parameters of a function) and the output array names. For the example f above, perhaps its two array formal arguments are x and y: based on which output array has name x vs. y, we can determine the mapping. Thus, when we analyze g, which passes a and b to f, we match a and b to x and y, and we determine which results of f must be bound to a and b in g. Note that this approach works also if g is mutually recursive with or the same as f (in the latter case the variables a and b would be the same as x and y then), because all functions must have type and array name information before the array analysis takes place. If the type and array name information is incorrect/inconsistent, the array analysis will reveal that.

Another complication of this array analysis, which does not happen with stobjs, is that some functions may create new arrays (directly or indirectly). These are arrays are not passed as inputs, but returned as outputs afresh. As such, they do not correspond to any inputs, so there is no name mapping. This is why atj-main-function-type and atj-other-function-type allow unnamed array outputs, whose meaning is that they must be newly created arrays; the array analysis checks that. If f returns new arrays, and g calls f, then the array analysis must ensure that these new arrays are bound to variables distinct from each other and from the ones of the input arrays. In contrast, stobjs are not created by calling functions; they are declared, essentially as global variables, and created beforehand.

Subtopics

Atj-analyze-arrays-in-term: Array analysis of ACL2 terms.
Atj-analyze-arrays-in-formals+body: Array analysis of ACL2 function bodies.