Array analysis of ACL2 terms.
(atj-analyze-arrays-in-term term wrld) → (mv arrays 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
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
If the term being analyzed is a quoted constant,
we return the singleton list with
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
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,
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
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
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-
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-
Theorem:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)