		Search-engine friendly clone of the ACL2 documentation.

Term-checkers-atc

Atc-check-array-write

Check if a let binding may represent an array write.

Signature
(atc-check-array-write var val) → (mv erp yes/no fn sub elem elem-type)
Arguments: var — Guard (symbolp var).; val — Guard (pseudo-termp val).
Returns: yes/no — Type (booleanp yes/no).; fn — Type (symbolp fn).; sub — Type (pseudo-termp sub).; elem — Type (pseudo-termp elem).; elem-type — Type (typep elem-type).

An array write, i.e. an assignment to an array element, is represented by a let binding of the form

(let ((<arr> (<type>-array-write <arr> <sub> <elem>))) ...)

where <arr> is a variable of pointer type to an integer type, which must occur identically as both the let variable and as the first argument of <type>-array-write, <sub> is an expression that yields the index of the element to write, <elem> is an expression that yields the element to write, and ... represents the code that follows the array assignment. This function takes as arguments the variable and value of a let binder, and checks if they have the form described above. If they do, the components are returned for further processing. We also return the types of the index and element as gathered from the name of the array write function.

Definitions and Theorems

Function: atc-check-array-write

(defun atc-check-array-write (var val)
 (declare (xargs :guard (and (symbolp var) (pseudo-termp val))))
 (let ((__function__ 'atc-check-array-write))
  (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 val))
    ((unless okp) (no))
    ((mv okp fixtype array write)
     (atc-check-symbol-3part fn))
    (elem-type (fixtype-to-integer-type fixtype))
    ((unless (and okp elem-type (eq array 'array)
                  (eq write 'write)))
     (no))
    ((unless (equal (symbol-package-name fn) "C"))
     (reterr
      (msg
       "Invalid function ~x0 encountered: ~
                      it has the form of an array write, ~
                      but it is not in the \"C\" package."
       fn)))
    ((unless (list-lenp 3 args))
     (reterr
          (raise "Internal error: ~x0 not applied to 3 arguments."
                 fn)))
    ((unless (equal (first args) var))
     (reterr
      (raise
           "Internal error: ~x0 is not applied to the variable ~x1."
           fn var)))
    (sub (second args))
    (elem (third args)))
   (retok t fn sub elem elem-type))))

Theorem: booleanp-of-atc-check-array-write.yes/no

(defthm booleanp-of-atc-check-array-write.yes/no
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?sub ?elem ?elem-type)
        (atc-check-array-write var val)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-check-array-write.fn

(defthm symbolp-of-atc-check-array-write.fn
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?sub ?elem ?elem-type)
        (atc-check-array-write var val)))
    (symbolp fn))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-atc-check-array-write.sub

(defthm pseudo-termp-of-atc-check-array-write.sub
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?sub ?elem ?elem-type)
        (atc-check-array-write var val)))
    (pseudo-termp sub))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-atc-check-array-write.elem

(defthm pseudo-termp-of-atc-check-array-write.elem
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?sub ?elem ?elem-type)
        (atc-check-array-write var val)))
    (pseudo-termp elem))
  :rule-classes :rewrite)

Theorem: typep-of-atc-check-array-write.elem-type

(defthm typep-of-atc-check-array-write.elem-type
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?sub ?elem ?elem-type)
        (atc-check-array-write var val)))
    (typep elem-type))
  :rule-classes :rewrite)

Theorem: pseudo-term-count-of-atc-check-array-write-sub

(defthm pseudo-term-count-of-atc-check-array-write-sub
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?sub ?elem ?elem-type)
        (atc-check-array-write var val)))
    (implies yes/no
             (< (pseudo-term-count sub)
                (pseudo-term-count val))))
  :rule-classes :linear)

Theorem: pseudo-term-count-of-atc-check-array-write-elem

(defthm pseudo-term-count-of-atc-check-array-write-elem
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?sub ?elem ?elem-type)
        (atc-check-array-write var val)))
    (implies yes/no
             (< (pseudo-term-count elem)
                (pseudo-term-count val))))
  :rule-classes :linear)