		Search-engine friendly clone of the ACL2 documentation.

Atj-pre-translation-array-analysis

Atj-analyze-arrays-in-term

Array analysis of ACL2 terms.

Signature
(atj-analyze-arrays-in-term term wrld) → (mv arrays types)
Arguments: term — Guard (pseudo-termp term).; wrld — Guard (plist-worldp wrld).
Returns: arrays — Type (symbol-listp arrays).; types — Type (atj-type-listp types).

The array analysis assigns to each term a non-empty list of array names, corresponding to the array types returned by the term. Recall that the type annotation pre-translation step assigns a non-empty list of ATJ types to every term; the list is a singleton if the term is single-valued, otherwise the list's length is the number of results returned by the term. Some of these result types may be (Java primitive) arrays: in that case, the array analysis assigns array names to the corresponding results, while it assigns nil to non-array results: the list of symbols inferred by the array analysis has always the same length as the list of types inferred by the type annotations, i.e. every term's result gets an array name (nil, if the result is not an array). The array names are the names of the variables that hold the arrays. When a term returns a newly created array that is not yet bound to any variable, its array name, inferred by array analysis, is nil. All of this is, of course, related to the array names that can be specified in atj-main-function-type and atj-other-function-type: see their documentation and implementation.

As the array analysis calculates these array names for terms, it also checks that arrays are treated single-threadedly, similarly to stobjs. The constraints to be satisfied are fairly draconian, like stobjs. Each modified array must be always bound to the same array name inside a function. Different functions may use different names, because array variables are not global; but inside a function, the same name must be used. A function that takes an array argument can only be passed an array name, not a term whose value is an array. The exact constraints are explained below. If any of these constraints is not satisfied, the array analysis fails, causing an error that stops the analysis and ATJ. Currently these are hard errors, but they are distinct from the `internal errors' that are so indicated in the error messages of some ATJ code. The internal errors are expected to never happen; if they do, they are indicative of an implementation bug in ATJ. On the other hand, errors from the array analysis are expected to happen: they are a form of input validation, but one that is ``semantically deep'' and can only be performed during pre-translation, and not as part of input processing.

Recall that this array analysis takes place after the type annotations. Thus, terms are unwrapped as they are analyzed.

Besides the list of array names, the analysis of a term also returns the list of types of the term. This is simply obtained from the type annotations, but it is used by the array analysis, and so returning it explicitly is useful in the recursive calls of the analysis code.

If the term being analyzed is a variable, we look at its type. Since we handle mv-let specially (see below), we expect that all the variables that we encounter ``directly'' (i.e. not the mv-let variable mv) will have singleton type lists: we use atj-type-list-to-type to convert singletons to single types, which causes an error should the type list not be a singleton (this would indicate an implementation error). If the type of the variable is an array, the result of the array analysis is the singleton list with the name of the variable. Otherwise, the result of the array analysis is the singleton list with nil.

If the term being analyzed is a quoted constant, we return the singleton list with nil. A quoted constant is never an array: a quoted constant always has an :acl2 type, according to the type annotations.

If the term being analyzed is neither a variable nor a quoted constant, we check whether it is a (type-annotated) mv-let call. This is handled by the separate function atj-analyze-arrays-in-mv-let, whose first result is a boolean flag that indicates success of failure. In case of success, the calling function atj-analyze-arrays-in-term forwards the second result of atj-analyze-arrays-in-mv-let; in case of failure, atj-analyze-arrays-in-term handles the other kinds of function calls, including calls of lambda expressions other than mv-lets, which are already handled by atj-analyze-arrays-in-mv-let. The handling of mv-let calls is explained later; first we explain the handling of the other kinds of function calls.

If the term being analyzed is an if call, we recursively analyze its three arguments. If the test returns an array, the analysis fails: we do not allow arrays as if tests. The `then' and `else' branches must have the same inferred arrays, otherwise the analysis fails; that is, no matter which branch is taken, the same arrays must be returned.

If the term being analyzed is a call of a function other than if, we recursively analyze all the arguments. We do so with a separate function, atj-analyze-arrays-in-args, mutually recursive with atj-analyze-arrays-in-term. Each of these arguments must be necessarily single-valued (see also atj-type-annotate-term), so the two lists returned by atj-analyze-arrays-in-args are interpreted differently from atj-analyze-arrays-in-term: the former are the concatenations of the singleton lists inferred for each of the arguments, while the latter are lists that apply to the whole term. The array analysis fails if two of arguments have the same array name: this situation means that the same array is aliased (in Java) and possibly subjected to different modifications through the aliases. We pass a flag to atj-analyze-arrays-in-term indicating whether the function called is a lambda expression or a named function: in the latter case, we also ensure that arguments of array types are variables, and not other function calls (note that they cannot be quoted constants). That is, we disallow ``nested'' calls of functions that return arrays. For example, if f returns an array and g takes an array of the same type, we disallow calls (g ... (f ...) ...). Instead, one must assign each array returned by a named function to some variable, and only pass such variables to names functions. In the example of f and g just above, one must have (let (... (a (f ...)) ...) (g ... a ...)) for code generation to proceed. It is thus important that the restriction of being variables only applies to the array arguments of named functions, and not to the array arguments of lambda expressions; otherwise, the let form would be illegal as well. Recall that we are dealing with annotated terms here: so, when we say `variable' here, we really mean a call of a (conversion) function on a variable. This constraint on array arguments of named functions being variables, is not needed for the safety of destructive array updates; however, it is useful to simplify the subsequent ``inlining'' of array writing functions done in ATJ's post-translation. Note that stobjs have similar restrictions in ACL2.

If the term being analyzed is an mv call, we just return the list of array arguments. This is a multi-valued term.

If the term being analyzed is a call of an array creation function in *atj-jprimarr-new-init-fns*, we return a singleton list with nil, because it is a newly created, and thus still unnamed, array.

If the term being analyzed is a call of a function other than if and mv, we look up its formals, function type, and output arrays. The function type is chosen based on the types of the arguments, in the same way as in atj-type-annotate-term. We match the array formal parameters of the function to the array names inferred for the actual arguments (see the discussion in atj-pre-translation-array-analysis), creating an alist. Then we go through the function's output arrays (whose names match the array formal parameters that may be modified by the function and returned), and we use the alist mentioned just above to compute the output arrays of the call. For example, suppose that we have a call of f, and that f has two array formal parameters x and y. Suppose that the array names inferred for the corresponding actual arguments are a and b. Then we construct first the alist ((x . a) (y. b)), and then we go through the output arrays of $('f'), which may include x and y (not necessarily in that order), and for each element of the list we generate a if the element is x, b if the element is y, and nil otherwise. The latter nil may indicate either a non-array result or an array newly created by f (directly or indirectly). Note that all of this works also when a and/or b is nil, which means that we are passing newly created arrays to f: the results corresponding to x and y may then be nil, which indicates arrays that have been newly created, possibly modified, and not given names yet (names are given then they are bound to variables).

If the term being analyzed is a call of a lambda expression (but not of the mv-let form, which is explained below), we ensure that each array argument with a non-nil name is assigned (in the sense of let) to a variable with the same name: the variables are the formal parameters of the lambda expression. That is, we go through argument arrays and lambda's formal parameters, and ensure that they match as just explained. This is an important constraint checked by the array analysis, namely that (within each function), each array has a unique name. One cannot ``rename'' an array, just like one cannot ``rename'' a stobj: a stobj has the same name everywhere (not only within each function). It is of course permitted to assign non-arrays to variables liberally. Then we return the result of recursively analyzing the body of the lambda expression. Note that, because of the array naming consistency checks explained above, in the body of the lambda expressions the arrays have the same names as they did outside the body. Some newly created arrays outside the body may have a name inside the body, so that their single-threaded use can be checked inside the body.

To handle mv-let, we decompose it into its constituents. We recursively analyze the subterm that returns a multiple value, obtaining a list of output arrays. We ensure that all the non-nil elements of this list are bound to some variable in the mv-let; we ensure that by going through the list, with a variable that holds the current position in the list, and checking that for every non-nil element its position is among the indices returned by the decomposition of the mv-let. If some named array were modified and then dropped (i.e. not assigned to any variable by the mv-let), then its modifications could not be returned and it would mean that it may not be used single-threadedly. As we perform the above check that no arrays are dropped, we also check that the arrays with non-nil names are assigned to variables with the same names, as with other lambda expressions. Then, as with other lambda expressions, we return the result of recursively analyzing the body of the mv-let.

Theorem: return-type-of-atj-analyze-arrays-in-term.arrays

(defthm return-type-of-atj-analyze-arrays-in-term.arrays
  (b* (((mv ?arrays ?types)
        (atj-analyze-arrays-in-term term wrld)))
    (symbol-listp arrays))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-analyze-arrays-in-term.types

(defthm return-type-of-atj-analyze-arrays-in-term.types
  (b* (((mv ?arrays ?types)
        (atj-analyze-arrays-in-term term wrld)))
    (atj-type-listp types))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-analyze-arrays-in-args.arrays

(defthm return-type-of-atj-analyze-arrays-in-args.arrays
  (b* (((mv ?arrays ?types)
        (atj-analyze-arrays-in-args args lambdap wrld)))
    (and (symbol-listp arrays)
         (equal (len arrays) (len args))))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-analyze-arrays-in-args.types

(defthm return-type-of-atj-analyze-arrays-in-args.types
  (b* (((mv ?arrays ?types)
        (atj-analyze-arrays-in-args args lambdap wrld)))
    (and (atj-type-listp types)
         (equal (len types) (len args))))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-analyze-arrays-in-mv-let.success

(defthm return-type-of-atj-analyze-arrays-in-mv-let.success
  (b* (((mv ?success ?arrays ?types)
        (atj-analyze-arrays-in-mv-let term wrld)))
    (booleanp success))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-analyze-arrays-in-mv-let.arrays

(defthm return-type-of-atj-analyze-arrays-in-mv-let.arrays
  (b* (((mv ?success ?arrays ?types)
        (atj-analyze-arrays-in-mv-let term wrld)))
    (symbol-listp arrays))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-analyze-arrays-in-mv-let.types

(defthm return-type-of-atj-analyze-arrays-in-mv-let.types
  (b* (((mv ?success ?arrays ?types)
        (atj-analyze-arrays-in-mv-let term wrld)))
    (atj-type-listp types))
  :rule-classes :rewrite)

Theorem: consp-of-atj-analyze-arrays-in-term.arrays

(defthm consp-of-atj-analyze-arrays-in-term.arrays
  (b* (((mv ?arrays ?types)
        (atj-analyze-arrays-in-term term wrld)))
    (consp arrays))
  :rule-classes :type-prescription)

Theorem: consp-of-atj-analyze-arrays-in-args.arrays

(defthm consp-of-atj-analyze-arrays-in-args.arrays
  (implies (consp args)
           (b* (((mv ?arrays ?types)
                 (atj-analyze-arrays-in-args args lambdap wrld)))
             (consp arrays)))
  :rule-classes :type-prescription)

Theorem: consp-of-atj-analyze-arrays-in-mv-let.arrays

(defthm consp-of-atj-analyze-arrays-in-mv-let.arrays
  (implies (mv-nth 0
                   (atj-analyze-arrays-in-mv-let term wrld))
           (b* (((mv ?success ?arrays ?types)
                 (atj-analyze-arrays-in-mv-let term wrld)))
             (consp arrays)))
  :rule-classes :type-prescription)

Theorem: consp-of-atj-analyze-arrays-in-term.types

(defthm consp-of-atj-analyze-arrays-in-term.types
  (b* (((mv ?arrays ?types)
        (atj-analyze-arrays-in-term term wrld)))
    (consp types))
  :rule-classes :type-prescription)

Theorem: consp-of-atj-analyze-arrays-in-args.types

(defthm consp-of-atj-analyze-arrays-in-args.types
  (implies (consp args)
           (b* (((mv ?arrays ?types)
                 (atj-analyze-arrays-in-args args lambdap wrld)))
             (consp types)))
  :rule-classes :type-prescription)

Theorem: consp-of-atj-analyze-arrays-in-mv-let.types

(defthm consp-of-atj-analyze-arrays-in-mv-let.types
  (implies (mv-nth 0
                   (atj-analyze-arrays-in-mv-let term wrld))
           (b* (((mv ?success ?arrays ?types)
                 (atj-analyze-arrays-in-mv-let term wrld)))
             (consp types)))
  :rule-classes :type-prescription)

Subtopics

Atj-analyze-arrays-in-args
Atj-analyze-arrays-in-mv-let