		Search-engine friendly clone of the ACL2 documentation.

Atc-expression-generation

Atc-gen-expr-struct-read-scalar

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

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

Definitions and Theorems

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

(defun atc-gen-expr-struct-read-scalar
       (fn arg-term arg-expr arg-type arg-events
           arg-thm tag member mem-type gin state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp fn)
                             (pseudo-termp arg-term)
                             (exprp arg-expr)
                             (typep arg-type)
                             (pseudo-event-form-listp arg-events)
                             (symbolp arg-thm)
                             (identp tag)
                             (identp member)
                             (typep mem-type)
                             (expr-ginp gin))))
 (declare (xargs :guard (type-nonchar-integerp mem-type)))
 (let ((__function__ 'atc-gen-expr-struct-read-scalar))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-expr-gout))
    ((expr-gin gin) gin)
    (term (cons fn (cons arg-term 'nil)))
    ((unless (symbolp arg-term))
     (reterr
      (raise
       "Internal error: ~
                        structure read ~x0 applied to non-variable ~x1."
       fn arg-term))))
   (cond
    ((equal arg-type (type-struct tag))
     (b*
      ((expr (make-expr-member :target arg-expr
                               :name member))
       ((when (not gin.proofs))
        (retok (make-expr-gout :expr expr
                               :type mem-type
                               :term term
                               :events arg-events
                               :thm-name nil
                               :thm-index gin.thm-index
                               :names-to-avoid gin.names-to-avoid)))
       (recognizer (atc-type-to-recognizer arg-type gin.prec-tags))
       (exec-member-read-when-struct-tag-p-and-member
            (pack 'exec-member-read-when-
                  recognizer '-and-
                  (ident->name member)))
       (info (atc-get-var arg-term gin.inscope))
       ((unless info)
        (reterr (raise "Internal error: variable ~x0 not found."
                       arg-term)))
       (var-thm (atc-var-info->thm info))
       (mem-typep (atc-type-to-recognizer mem-type gin.prec-tags))
       (mem-typep-of-fn (packn-pos (list mem-typep '-of- fn)
                                   fn))
       (hints
        (cons
         (cons
          '"Goal"
          (cons
           ':in-theory
           (cons
            (cons
             'quote
             (cons
              (cons
               'exec-expr-pure-when-member
               (cons
                '(:e expr-kind)
                (cons
                 '(:e expr-member->target)
                 (cons
                  '(:e expr-member->name)
                  (cons
                   arg-thm
                   (cons
                    'expr-valuep-of-expr-value
                    (cons
                     exec-member-read-when-struct-tag-p-and-member
                     (cons
                      'exec-member-of-const-identifier
                      (cons
                       '(:e identp)
                       (cons
                        '(:e ident->name)
                        (cons
                         'objdesign-option-fix-when-objdesign-optionp
                         (cons
                          'objdesign-optionp-of-objdesign-of-var
                          (cons
                            var-thm
                            (cons mem-typep-of-fn 'nil))))))))))))))
              'nil))
            'nil)))
         'nil))
       (objdes
        (cons
         'objdesign-member
         (cons
          (cons
           'objdesign-of-var
           (cons
               (cons 'ident
                     (cons (cons 'quote
                                 (cons (symbol-name arg-term) 'nil))
                           'nil))
               (cons gin.compst-var 'nil)))
          (cons (cons 'ident
                      (cons (cons 'quote
                                  (cons (ident->name member) 'nil))
                            '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
             mem-type term term objdes gin.compst-var
             hints nil gin.prec-tags gin.thm-index
             gin.names-to-avoid state)))
      (retok
        (make-expr-gout :expr expr
                        :type mem-type
                        :term term
                        :events (append arg-events (list thm-event))
                        :thm-name thm-name
                        :thm-index thm-index
                        :names-to-avoid names-to-avoid))))
    ((equal arg-type
            (type-pointer (type-struct tag)))
     (b*
      ((expr (make-expr-memberp :target arg-expr
                                :name member))
       ((when (not gin.proofs))
        (retok (make-expr-gout :expr expr
                               :type mem-type
                               :term term
                               :events arg-events
                               :thm-name nil
                               :thm-index gin.thm-index
                               :names-to-avoid gin.names-to-avoid)))
       (arg-type (type-pointer->to arg-type))
       (recognizer (atc-type-to-recognizer arg-type gin.prec-tags))
       (exec-memberp-read-when-struct-point-p-and-x
            (pack 'exec-memberp-read-when-
                  recognizer '-and-
                  (ident->name member)))
       (mem-typep (atc-type-to-recognizer mem-type gin.prec-tags))
       (mem-typep-of-fn (packn-pos (list mem-typep '-of- fn)
                                   fn))
       (hints
        (cons
         (cons
          '"Goal"
          (cons
           ':in-theory
           (cons
            (cons
             'quote
             (cons
              (cons
               'exec-expr-pure-when-memberp
               (cons
                '(:e expr-kind)
                (cons
                 '(:e expr-memberp->target)
                 (cons
                  '(:e expr-memberp->name)
                  (cons
                   arg-thm
                   (cons
                    'expr-valuep-of-expr-value
                    (cons
                     exec-memberp-read-when-struct-point-p-and-x
                     (cons
                      'exec-memberp-of-const-identifier
                      (cons
                       '(:e identp)
                       (cons
                        '(:e ident->name)
                        (cons
                         'read-object-of-add-var
                         (cons
                          'read-object-of-add-frame
                          (cons
                           'read-object-of-update-object-same
                           (cons
                            'read-object-of-update-object-disjoint
                            (cons
                             'object-disjointp-commutative
                             (cons
                                mem-typep-of-fn 'nil))))))))))))))))
              'nil))
            'nil)))
         'nil))
       (objdes
        (cons
         'objdesign-member
         (cons
           (add-suffix-to-fn arg-term "-OBJDES")
           (cons (cons 'ident
                       (cons (cons 'quote
                                   (cons (ident->name member) 'nil))
                             '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
             mem-type term term objdes gin.compst-var
             hints nil gin.prec-tags gin.thm-index
             gin.names-to-avoid state)))
      (retok
        (make-expr-gout :expr expr
                        :type mem-type
                        :term term
                        :events (append arg-events (list thm-event))
                        :thm-name thm-name
                        :thm-index thm-index
                        :names-to-avoid names-to-avoid))))
    (t
     (reterr
      (msg
       "The reading of a ~x0 structure with member ~x1 ~
                    is applied to ~
                    an expression term ~x2 returning ~x3, ~
                    but a 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
       arg-term arg-type (type-struct tag)
       (type-pointer (type-struct tag)))))))))

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

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