		Search-engine friendly clone of the ACL2 documentation.

Term-checkers-atc

Atc-check-struct-write-array

Check if a let binding may represent a structure write of an element of an array member.

Signature
(atc-check-struct-write-array var val prec-tags) → (mv erp yes/no fn index elem tag member elem-type flexiblep)
Arguments: var — Guard (symbolp var).; val — Guard (pseudo-termp val).; prec-tags — Guard (atc-string-taginfo-alistp prec-tags).
Returns: yes/no — Type (booleanp yes/no).; fn — Type (symbolp fn).; index — Type (pseudo-termp index).; elem — Type (pseudo-termp elem).; tag — Type (identp tag).; member — Type (identp member).; elem-type — Type (typep elem-type).; flexiblep — Type (booleanp flexiblep).

A structure write of an element of an array member, i.e. an assignment to an element of an array structure member via a pointer to the structure, is represented by a let binding of the form

(let ((<struct>
            (struct-<tag>-write-<member>-element <index> <elem> <struct>)))
       ...)

where <struct> is a variable of structure type or of pointer type to a structure type, which must occur identically as both the let variable and as the last argument of struct-<tag>-write-<member>-element, <index> is an expression that yields an integer used as array index, <elem> is an expression that yields the member element value to write, and ... represents the code that follows the 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 index and member argument are returned for further processing. We also return the tag, the member name, and the member type.

Similarly to atc-check-struct-read-array, we consult the prec-tags alist, which must contain the C structure type associated to the writer.

Definitions and Theorems

Function: atc-check-struct-write-array

(defun atc-check-struct-write-array (var val prec-tags)
 (declare
      (xargs :guard (and (symbolp var)
                         (pseudo-termp val)
                         (atc-string-taginfo-alistp prec-tags))))
 (let ((__function__ 'atc-check-struct-write-array))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     nil nil nil nil (irr-ident)
     (irr-ident)
     (irr-type)
     nil)
    ((acl2::fun (no))
     (retok nil nil nil nil (irr-ident)
            (irr-ident)
            (irr-type)
            nil))
    ((mv okp fn args)
     (fty-check-fn-call val))
    ((unless okp) (no))
    ((mv okp struct tag write member element)
     (atc-check-symbol-5part fn))
    ((unless (and okp
                  (equal (symbol-name struct) "STRUCT")
                  (equal (symbol-name write) "WRITE")
                  (equal (symbol-name element)
                         "ELEMENT")))
     (no))
    (tag (symbol-name tag))
    (info (cdr (assoc-equal tag prec-tags)))
    ((unless info)
     (reterr (raise "Internal error: no structure with tag ~x0."
                    tag)))
    (info (atc-tag-info->defstruct info))
    ((unless (member-eq fn
                        (defstruct-info->writer-element-list info)))
     (reterr (raise "Internal error: no member writer ~x0."
                    fn)))
    (members (defstruct-member-info-list->memtype-list
                  (defstruct-info->members info)))
    (tag (defstruct-info->tag info))
    (member (symbol-name member))
    (member (ident member))
    (mem-type (member-type-lookup member members))
    ((unless mem-type)
     (reterr (raise "Internal error: no member type for ~x0."
                    member)))
    ((unless (type-case mem-type :array))
     (reterr (raise "Internal error: type of ~x0 is not array."
                    member)))
    (elem-type (type-array->of mem-type))
    (flexiblep (not (type-array->size mem-type)))
    ((unless (list-lenp 3 args))
     (reterr
          (raise "Internal error: ~x0 not applied to 3 arguments."
                 fn)))
    (index (first args))
    (mem (second args))
    ((unless (equal (third args) var))
     (reterr
      (raise
           "Internal error: ~x0 is not applied to the variable ~x1."
           fn var))))
   (retok t fn index
          mem tag member elem-type flexiblep))))

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

(defthm booleanp-of-atc-check-struct-write-array.yes/no
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?index ?elem acl2::?tag
            ?member ?elem-type ?flexiblep)
        (atc-check-struct-write-array var val prec-tags)))
    (booleanp yes/no))
  :rule-classes :rewrite)

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

(defthm symbolp-of-atc-check-struct-write-array.fn
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?index ?elem acl2::?tag
            ?member ?elem-type ?flexiblep)
        (atc-check-struct-write-array var val prec-tags)))
    (symbolp fn))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-atc-check-struct-write-array.index

(defthm pseudo-termp-of-atc-check-struct-write-array.index
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?index ?elem acl2::?tag
            ?member ?elem-type ?flexiblep)
        (atc-check-struct-write-array var val prec-tags)))
    (pseudo-termp index))
  :rule-classes :rewrite)

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

(defthm pseudo-termp-of-atc-check-struct-write-array.elem
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?index ?elem acl2::?tag
            ?member ?elem-type ?flexiblep)
        (atc-check-struct-write-array var val prec-tags)))
    (pseudo-termp elem))
  :rule-classes :rewrite)

Theorem: identp-of-atc-check-struct-write-array.tag

(defthm identp-of-atc-check-struct-write-array.tag
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?index ?elem acl2::?tag
            ?member ?elem-type ?flexiblep)
        (atc-check-struct-write-array var val prec-tags)))
    (identp tag))
  :rule-classes :rewrite)

Theorem: identp-of-atc-check-struct-write-array.member

(defthm identp-of-atc-check-struct-write-array.member
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?index ?elem acl2::?tag
            ?member ?elem-type ?flexiblep)
        (atc-check-struct-write-array var val prec-tags)))
    (identp member))
  :rule-classes :rewrite)

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

(defthm typep-of-atc-check-struct-write-array.elem-type
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?index ?elem acl2::?tag
            ?member ?elem-type ?flexiblep)
        (atc-check-struct-write-array var val prec-tags)))
    (typep elem-type))
  :rule-classes :rewrite)

Theorem: booleanp-of-atc-check-struct-write-array.flexiblep

(defthm booleanp-of-atc-check-struct-write-array.flexiblep
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?index ?elem acl2::?tag
            ?member ?elem-type ?flexiblep)
        (atc-check-struct-write-array var val prec-tags)))
    (booleanp flexiblep))
  :rule-classes :rewrite)

Theorem: pseudo-term-count-of-atc-check-struct-write-array-index

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

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

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