Check if a term may represent an array read.
(atc-check-array-read term) → (mv erp yes/no fn arr sub elem-type)
If the term is a call of one of the ACL2 functions that represent C array read operations, we return the two argument terms.
We also return the element type of the array.
If the term does not have the form explained above, we return an indication of failure.
Function:
(defun atc-check-array-read (term) (declare (xargs :guard (pseudo-termp term))) (let ((__function__ 'atc-check-array-read)) (declare (ignorable __function__)) (b* (((reterr) nil nil nil nil (irr-type)) ((acl2::fun (no)) (retok nil nil nil nil (irr-type))) ((mv okp fn args) (fty-check-fn-call term)) ((unless okp) (no)) ((mv okp fixtype array read) (atc-check-symbol-3part fn)) (elem-type (fixtype-to-integer-type fixtype)) ((unless (and okp elem-type (eq array 'array) (eq read 'read))) (no)) ((unless (equal (symbol-package-name fn) "C")) (reterr (msg "Invalid function ~x0 encountered: ~ it has the form of an array read, ~ but it is not in the \"C\" package." fn))) ((unless (list-lenp 2 args)) (reterr (raise "Internal error: ~x0 not applied to 2 arguments." fn))) (arr (first args)) (sub (second args))) (retok t fn arr sub elem-type))))
Theorem:
(defthm booleanp-of-atc-check-array-read.yes/no (b* (((mv acl2::?erp ?yes/no ?fn ?arr ?sub ?elem-type) (atc-check-array-read term))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-atc-check-array-read.fn (b* (((mv acl2::?erp ?yes/no ?fn ?arr ?sub ?elem-type) (atc-check-array-read term))) (symbolp fn)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-termp-of-atc-check-array-read.arr (b* (((mv acl2::?erp ?yes/no ?fn ?arr ?sub ?elem-type) (atc-check-array-read term))) (pseudo-termp arr)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-termp-of-atc-check-array-read.sub (b* (((mv acl2::?erp ?yes/no ?fn ?arr ?sub ?elem-type) (atc-check-array-read term))) (pseudo-termp sub)) :rule-classes :rewrite)
Theorem:
(defthm typep-of-atc-check-array-read.elem-type (b* (((mv acl2::?erp ?yes/no ?fn ?arr ?sub ?elem-type) (atc-check-array-read term))) (typep elem-type)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-term-count-of-atc-check-array-read-arr (b* (((mv acl2::?erp ?yes/no ?fn ?arr ?sub ?elem-type) (atc-check-array-read term))) (implies yes/no (< (pseudo-term-count arr) (pseudo-term-count term)))) :rule-classes :linear)
Theorem:
(defthm pseudo-term-count-of-atc-check-array-read-sub (b* (((mv acl2::?erp ?yes/no ?fn ?arr ?sub ?elem-type) (atc-check-array-read term))) (implies yes/no (< (pseudo-term-count sub) (pseudo-term-count term)))) :rule-classes :linear)
Theorem:
(defthm type-nonchar-integerp-of-atc-check-array-read (b* (((mv acl2::?erp ?yes/no ?fn ?arr ?sub ?elem-type) (atc-check-array-read term))) (implies yes/no (type-nonchar-integerp elem-type))))