		Search-engine friendly clone of the ACL2 documentation.

Atj-pre-translation-array-analysis

Atj-analyze-arrays-in-formals+body

Array analysis of ACL2 function bodies.

Signature
(atj-analyze-arrays-in-formals+body formals body out-arrays wrld) → nothing
Arguments: formals — Guard (symbol-listp formals).; body — Guard (pseudo-termp body).; out-arrays — Guard (symbol-listp out-arrays).; wrld — Guard (plist-worldp wrld).
Returns: nothing — Type (null nothing).

This is the top level of the array analysis. We analyze the body of the function, and compare the inferred arrays with the ones declared for the function (via atj-main-function-type and atj-other-function-type). The inferred arrays must be the same as the declared ones, except that the inferred ones may have names for newly created arrays. More precisely, for each position in the lists: if the declared array name at that position is not nil then the inferred array name at that position must be the same; if the declared array name at that position is nil, then the inferred array name at that position may be either nil or a new array name that is not among the function's formal parameters. In the latter case, it means that the function body has directly or indirectly created a new array and assigned it to a variable, which is then returned as result of array analysis, but the declared array names are only the ones that match some formal parameter names. Note that we need to remove the types from the formal parameters in order to properly compare them with the inferred variables, which do not have type annotations.

These checks tie the intraprocedural array analysis (performed by atj-analyze-arrays-in-term) with the output arrays assigned by the user to the functions. Recall that atj-main-function-type and atj-other-function-type check the correctness of the declared types but not of the declared output arrays, aside from relatively simple constraints such as the fact that the non-nil output arrays are unique, correspond to some formal parameters with the same array types, etc. By checking that the inferred arrays are consistent with the declared ones, which are used to analyze the callers of the function, we ensure that all the arrays potentially modified by the function are returned by the function, so that the callers have to receive them and return them as well. This is similar to ACL2's stobj analysis.

This atj-analyze-arrays-in-formals+body returns nothing, but its execution stops with a hard error if the array analysis fails.

Definitions and Theorems

Function: atj-analyze-arrays-in-formals+body-aux

(defun atj-analyze-arrays-in-formals+body-aux
       (uformals inferred declared)
 (declare (xargs :guard (and (symbol-listp uformals)
                             (symbol-listp inferred)
                             (symbol-listp declared))))
 (declare (xargs :guard (= (len inferred) (len declared))))
 (let ((__function__ 'atj-analyze-arrays-in-formals+body-aux))
  (declare (ignorable __function__))
  (or
   (endp inferred)
   (b* ((inf (car inferred))
        (decl (car declared)))
    (and
     (or (eq inf decl)
         (and (null decl)
              (not (member-eq inf uformals))))
     (atj-analyze-arrays-in-formals+body-aux uformals (cdr inferred)
                                             (cdr declared)))))))

Theorem: booleanp-of-atj-analyze-arrays-in-formals+body-aux

(defthm booleanp-of-atj-analyze-arrays-in-formals+body-aux
  (b* ((yes/no (atj-analyze-arrays-in-formals+body-aux
                    uformals inferred declared)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Function: atj-analyze-arrays-in-formals+body

(defun atj-analyze-arrays-in-formals+body
       (formals body out-arrays wrld)
 (declare (xargs :guard (and (symbol-listp formals)
                             (pseudo-termp body)
                             (symbol-listp out-arrays)
                             (plist-worldp wrld))))
 (let ((__function__ 'atj-analyze-arrays-in-formals+body))
  (declare (ignorable __function__))
  (b*
   (((mv arrays &)
     (atj-analyze-arrays-in-term body wrld))
    ((unless (= (len arrays) (len out-arrays)))
     (raise
      "Internal error: ~
                the length of the inferred arrays ~x0 ~
                differs from the length of the declared arrays ~x1."
      arrays out-arrays))
    (uformals (atj-type-unannotate-vars formals))
    (pass (atj-analyze-arrays-in-formals+body-aux
               uformals arrays out-arrays)))
   (if pass nil
    (raise
     "Array analysis failure: ~
              the function with formals ~x0 and body ~x1 ~
              returns the inferred arrays ~x2, ~
              which are inconsistent with the declared arrays ~x3."
     formals body arrays out-arrays)))))

Theorem: null-of-atj-analyze-arrays-in-formals+body

(defthm null-of-atj-analyze-arrays-in-formals+body
  (b* ((nothing (atj-analyze-arrays-in-formals+body
                     formals body out-arrays wrld)))
    (null nothing))
  :rule-classes :rewrite)