Array analysis of ACL2 function bodies.
(atj-analyze-arrays-in-formals+body formals body out-arrays wrld) → 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
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-
This
Function:
(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:
(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:
(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:
(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)