		Search-engine friendly clone of the ACL2 documentation.

Atc-expression-generation

Atc-gen-expr-struct-read-array

Generate a C expression from an ACL2 term that represents a structure array read.

Signature
(atc-gen-expr-struct-read-array fn index-term index-expr index-type index-events index-thm struct-term struct-expr struct-type struct-events struct-thm tag member elem-type flexiblep gin state) → (mv erp gout)
Arguments: fn — Guard (symbolp fn).; index-term — Guard (pseudo-termp index-term).; index-expr — Guard (exprp index-expr).; index-type — Guard (typep index-type).; index-events — Guard (pseudo-event-form-listp index-events).; index-thm — Guard (symbolp index-thm).; struct-term — Guard (pseudo-termp struct-term).; struct-expr — Guard (exprp struct-expr).; struct-type — Guard (typep struct-type).; struct-events — Guard (pseudo-event-form-listp struct-events).; struct-thm — Guard (symbolp struct-thm).; tag — Guard (identp tag).; member — Guard (identp member).; elem-type — Guard (typep elem-type).; flexiblep — Guard (booleanp flexiblep).; gin — Guard (expr-ginp gin).
Returns: gout — Type (expr-goutp gout).

Definitions and Theorems

Function: atc-gen-expr-struct-read-array

(defun atc-gen-expr-struct-read-array
       (fn index-term
           index-expr index-type index-events
           index-thm struct-term struct-expr
           struct-type struct-events struct-thm tag
           member elem-type flexiblep gin state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp fn)
                             (pseudo-termp index-term)
                             (exprp index-expr)
                             (typep index-type)
                             (pseudo-event-form-listp index-events)
                             (symbolp index-thm)
                             (pseudo-termp struct-term)
                             (exprp struct-expr)
                             (typep struct-type)
                             (pseudo-event-form-listp struct-events)
                             (symbolp struct-thm)
                             (identp tag)
                             (identp member)
                             (typep elem-type)
                             (booleanp flexiblep)
                             (expr-ginp gin))))
 (let ((__function__ 'atc-gen-expr-struct-read-array))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-expr-gout))
    ((expr-gin gin) gin)
    (wrld (w state))
    ((when (eq fn 'quote))
     (reterr (raise "Internal error: QUOTE function.")))
    (term (cons fn
                (cons index-term (cons struct-term 'nil))))
    ((unless (type-integerp index-type))
     (reterr
      (msg
       "The reading of a ~x0 structure with array member ~x1 ~
               is applied to an index expression term ~x2 returning ~x3, ~
               but a C integer operand is expected. ~
               This is indicative of provably dead code, ~
               given that the code is guard-verified."
       (type-struct tag)
       member index-term index-type)))
    ((unless (symbolp struct-term))
     (reterr
      (raise
       "Internal error: ~
                        structure read ~x0 applied to non-variable ~x1."
       fn struct-term)))
    (index-uterm (untranslate$ index-term nil state)))
   (cond
    ((equal struct-type (type-struct tag))
     (b*
      ((expr
        (make-expr-arrsub :arr (make-expr-member :target struct-expr
                                                 :name member)
                          :sub index-expr))
       ((when (not gin.proofs))
        (retok
         (make-expr-gout :expr expr
                         :type elem-type
                         :term term
                         :events (append index-events struct-events)
                         :thm-name nil
                         :thm-index gin.thm-index
                         :names-to-avoid gin.names-to-avoid)))
       (struct-tag-p
            (atc-type-to-recognizer struct-type gin.prec-tags))
       ((mv okp-lemma-event
            okp-lemma-name thm-index names-to-avoid)
        (b*
         ((okp-lemma-name (pack gin.fn '-expr-
                                gin.thm-index '-okp-lemma))
          ((mv okp-lemma-name names-to-avoid)
           (fresh-logical-name-with-$s-suffix
                okp-lemma-name
                nil gin.names-to-avoid wrld))
          (struct-tag
               (defstruct-info->fixtype
                    (atc-tag-info->defstruct
                         (atc-get-tag-info tag gin.prec-tags))))
          (struct-tag-member-index-okp
               (packn-pos (list struct-tag '-
                                (ident->name member)
                                '-index-okp)
                          struct-tag))
          (okp-lemma-formula (cons struct-tag-member-index-okp
                                   (cons index-uterm 'nil)))
          (okp-lemma-formula
             (atc-contextualize okp-lemma-formula gin.context gin.fn
                                gin.fn-guard nil nil nil nil wrld))
          (okp-lemma-hints
           (cons
            (cons
             '"Goal"
             (cons
              ':in-theory
              (cons
               (cons
                'quote
                (cons (cons gin.fn-guard '(if* test* declar assign))
                      'nil))
               (cons ':use
                     (cons (cons ':guard-theorem
                                 (cons gin.fn 'nil))
                           'nil)))))
            'nil))
          ((mv okp-lemma-event &)
           (evmac-generate-defthm okp-lemma-name
                                  :formula okp-lemma-formula
                                  :hints okp-lemma-hints
                                  :enable nil)))
         (mv okp-lemma-event
             okp-lemma-name (1+ gin.thm-index)
             names-to-avoid)))
       (exec-member-read-when-struct-tag-p-and-member-element
            (pack 'exec-member-read-when-
                  struct-tag-p '-and-
                  (ident->name member)
                  '-element))
       (index-typep
            (atc-type-to-recognizer index-type gin.prec-tags))
       (cintegerp-when-index-type
            (pack 'cintegerp-when- index-typep))
       (var-info (atc-get-var struct-term gin.inscope))
       ((unless var-info)
        (reterr (raise "Internal error: variable ~x0 not found."
                       struct-term)))
       (var-thm (atc-var-info->thm var-info))
       (elem-typep (atc-type-to-recognizer elem-type gin.prec-tags))
       (elem-typep-of-fn (packn-pos (list elem-typep '-of- fn)
                                    fn))
       (hints
        (cons
         (cons
          '"Goal"
          (cons
           ':in-theory
           (cons
            (cons
             'quote
             (cons
              (cons
               'exec-expr-pure-when-arrsub-of-member
               (cons
                '(:e expr-kind)
                (cons
                 '(:e expr-arrsub->arr)
                 (cons
                  '(:e expr-arrsub->sub)
                  (cons
                   '(:e expr-member->target)
                   (cons
                    '(:e expr-member->name)
                    (cons
                     index-thm
                     (cons
                      struct-thm
                      (cons
                       'expr-valuep-of-expr-value
                       (cons
                        'exec-arrsub-of-member-of-const-identifier
                        (cons
                         '(:e identp)
                         (cons
                          '(:e ident->name)
                          (cons
                           exec-member-read-when-struct-tag-p-and-member-element
                           (cons
                            cintegerp-when-index-type
                            (cons
                             okp-lemma-name
                             (cons
                              'objdesignp-when-objdesign-optionp
                              (cons
                               'objdesign-optionp-of-objdesign-of-var
                               (cons
                                var-thm
                                (cons
                                  'value-integer->get-when-cintegerp
                                  (cons elem-typep-of-fn
                                        'nil))))))))))))))))))))
              'nil))
            'nil)))
         'nil))
       (objdes
        (cons
         'objdesign-element
         (cons
          (cons
           'objdesign-member
           (cons
            (cons
             'objdesign-of-var
             (cons
              (cons
                  'ident
                  (cons (cons 'quote
                              (cons (symbol-name struct-term) 'nil))
                        'nil))
              (cons gin.compst-var 'nil)))
            (cons
                 (cons 'ident
                       (cons (cons 'quote
                                   (cons (ident->name member) 'nil))
                             'nil))
                 'nil)))
          (cons (cons 'integer-from-cinteger
                      (cons index-term 'nil))
                'nil))))
       ((mv thm-event
            thm-name thm-index names-to-avoid)
        (atc-gen-expr-pure-correct-thm
             gin.fn gin.fn-guard gin.context
             expr elem-type term term objdes
             gin.compst-var hints nil gin.prec-tags
             thm-index names-to-avoid state)))
      (retok (make-expr-gout
                  :expr expr
                  :type elem-type
                  :term term
                  :events (append index-events struct-events
                                  (list okp-lemma-event thm-event))
                  :thm-name thm-name
                  :thm-index thm-index
                  :names-to-avoid names-to-avoid))))
    ((equal struct-type
            (type-pointer (type-struct tag)))
     (b*
      ((expr (make-expr-arrsub
                  :arr (make-expr-memberp :target struct-expr
                                          :name member)
                  :sub index-expr))
       ((when (not gin.proofs))
        (retok
         (make-expr-gout :expr expr
                         :type elem-type
                         :term term
                         :events (append index-events struct-events)
                         :thm-name nil
                         :thm-index gin.thm-index
                         :names-to-avoid gin.names-to-avoid)))
       ((mv okp-lemma-event
            okp-lemma-name thm-index names-to-avoid)
        (b*
         ((okp-lemma-name (pack gin.fn '-expr-
                                gin.thm-index '-okp-lemma))
          ((mv okp-lemma-name names-to-avoid)
           (fresh-logical-name-with-$s-suffix
                okp-lemma-name
                nil gin.names-to-avoid wrld))
          (struct-tag
               (defstruct-info->fixtype
                    (atc-tag-info->defstruct
                         (atc-get-tag-info tag gin.prec-tags))))
          (struct-tag-member-index-okp
               (packn-pos (list struct-tag '-
                                (ident->name member)
                                '-index-okp)
                          struct-tag))
          (index-uterm (untranslate$ index-term nil state))
          (okp-lemma-formula
               (if flexiblep
                   (cons struct-tag-member-index-okp
                         (cons index-uterm (cons struct-term 'nil)))
                 (cons struct-tag-member-index-okp
                       (cons index-uterm 'nil))))
          (okp-lemma-formula
             (atc-contextualize okp-lemma-formula gin.context gin.fn
                                gin.fn-guard nil nil nil nil wrld))
          (okp-lemma-hints
           (cons
            (cons
             '"Goal"
             (cons
              ':in-theory
              (cons
               (cons
                'quote
                (cons (cons gin.fn-guard '(if* test* declar assign))
                      'nil))
               (cons ':use
                     (cons (cons ':guard-theorem
                                 (cons gin.fn 'nil))
                           'nil)))))
            'nil))
          ((mv okp-lemma-event &)
           (evmac-generate-defthm okp-lemma-name
                                  :formula okp-lemma-formula
                                  :hints okp-lemma-hints
                                  :enable nil)))
         (mv okp-lemma-event
             okp-lemma-name (1+ gin.thm-index)
             names-to-avoid)))
       (struct-tag-p
            (atc-type-to-recognizer (type-pointer->to struct-type)
                                    gin.prec-tags))
       (exec-memberp-read-when-struct-tag-p-and-member-element
            (pack 'exec-memberp-read-when-
                  struct-tag-p '-and-
                  (ident->name member)
                  '-element))
       (index-typep
            (atc-type-to-recognizer index-type gin.prec-tags))
       (cintegerp-when-index-type
            (pack 'cintegerp-when- index-typep))
       (elem-typep (atc-type-to-recognizer elem-type gin.prec-tags))
       (elem-typep-of-fn (packn-pos (list elem-typep '-of- fn)
                                    fn))
       (hints
        (cons
         (cons
          '"Goal"
          (cons
           ':in-theory
           (cons
            (cons
             'quote
             (cons
              (cons
               'exec-expr-pure-when-arrsub-of-memberp
               (cons
                '(:e expr-kind)
                (cons
                 '(:e expr-arrsub->arr)
                 (cons
                  '(:e expr-arrsub->sub)
                  (cons
                   '(:e expr-memberp->target)
                   (cons
                    '(:e expr-memberp->name)
                    (cons
                     index-thm
                     (cons
                      struct-thm
                      (cons
                       'expr-valuep-of-expr-value
                       (cons
                        'exec-arrsub-of-memberp-of-const-identifier
                        (cons
                         '(:e identp)
                         (cons
                          '(:e ident->name)
                          (cons
                           exec-memberp-read-when-struct-tag-p-and-member-element
                           (cons
                            'read-object-of-add-var
                            (cons
                             'read-object-of-add-frame
                             (cons
                              cintegerp-when-index-type
                              (cons
                               okp-lemma-name
                               (cons
                                  'value-integer->get-when-cintegerp
                                  (cons elem-typep-of-fn
                                        'nil)))))))))))))))))))
              'nil))
            'nil)))
         'nil))
       (objdes
        (cons
         'objdesign-element
         (cons
          (cons
           'objdesign-member
           (cons
            (add-suffix-to-fn struct-term "-OBJDES")
            (cons
                 (cons 'ident
                       (cons (cons 'quote
                                   (cons (ident->name member) 'nil))
                             'nil))
                 'nil)))
          (cons (cons 'integer-from-cinteger
                      (cons index-term 'nil))
                'nil))))
       ((mv thm-event
            thm-name thm-index names-to-avoid)
        (atc-gen-expr-pure-correct-thm
             gin.fn gin.fn-guard gin.context
             expr elem-type term term objdes
             gin.compst-var hints nil gin.prec-tags
             thm-index names-to-avoid state)))
      (retok (make-expr-gout
                  :expr expr
                  :type elem-type
                  :term term
                  :events (append index-events struct-events
                                  (list okp-lemma-event thm-event))
                  :thm-name thm-name
                  :thm-index thm-index
                  :names-to-avoid names-to-avoid))))
    (t
     (reterr
      (msg
       "The reading of ~x0 structure with array member ~x1 ~
                    is applied to an expression term ~x2 returning ~x3, ~
                    but an operand of type ~x4 or ~x5 is expected. ~
                    This is indicative of provably dead code, ~
                    given that the code is guard-verified."
       tag member struct-term
       struct-type (type-struct tag)
       (type-pointer (type-struct tag)))))))))

Theorem: expr-goutp-of-atc-gen-expr-struct-read-array.gout

(defthm expr-goutp-of-atc-gen-expr-struct-read-array.gout
  (b* (((mv acl2::?erp ?gout)
        (atc-gen-expr-struct-read-array
             fn index-term
             index-expr index-type index-events
             index-thm struct-term struct-expr
             struct-type struct-events struct-thm tag
             member elem-type flexiblep gin state)))
    (expr-goutp gout))
  :rule-classes :rewrite)