		Search-engine friendly clone of the ACL2 documentation.

Term-checkers-atc

Atc-check-struct-write-scalar

Check if a let binding may represent a structure write of a scalar member.

Signature
(atc-check-struct-write-scalar var val prec-tags) → (mv erp yes/no fn mem tag member mem-type)
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).; mem — Type (pseudo-termp mem).; tag — Type (identp tag).; member — Type (identp member).; mem-type — Type (typep mem-type).

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

(let ((<struct> (struct-<tag>-write-<member> <mem> <struct>))) ...)

where <struct> is a variable 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>, <mem> is an expression that yields the member 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 member argument is returned for further processing. We also return the tag, the member name, and the member type.

Similarly to atc-check-struct-read-scalar, 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-scalar

(defun atc-check-struct-write-scalar (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-scalar))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     nil nil nil (irr-ident)
     (irr-ident)
     (irr-type))
    ((acl2::fun (no))
     (retok nil nil nil (irr-ident)
            (irr-ident)
            (irr-type)))
    ((mv okp fn args)
     (fty-check-fn-call val))
    ((unless okp) (no))
    ((mv okp struct tag write member)
     (atc-check-symbol-4part fn))
    ((unless (and okp
                  (equal (symbol-name struct) "STRUCT")
                  (equal (symbol-name write) "WRITE")))
     (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-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 (list-lenp 2 args))
     (reterr
          (raise "Internal error: ~x0 not applied to 2 arguments."
                 fn)))
    (mem (first args))
    ((unless (equal (second args) var))
     (reterr
      (raise
           "Internal error: ~x0 is not applied to the variable ~x1."
           fn var))))
   (retok t fn mem tag member mem-type))))

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

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

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

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

Theorem: pseudo-termp-of-atc-check-struct-write-scalar.mem

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

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

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

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

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

Theorem: typep-of-atc-check-struct-write-scalar.mem-type

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

Theorem: pseudo-term-count-of-atc-check-struct-write-scalar

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