		Search-engine friendly clone of the ACL2 documentation.

Atc-statement-generation

Atc-gen-block-item-list-one

Generate a list of C block items that consists of a given item.

Signature
(atc-gen-block-item-list-one term type item item-limit item-events item-thm stmt-value new-compst new-context new-inscope gin state) → gout
Arguments: term — Guard (pseudo-termp term).; type — Guard (typep type).; item — Guard (block-itemp item).; item-limit — Guard (pseudo-termp item-limit).; item-events — Guard (pseudo-event-form-listp item-events).; item-thm — Guard (symbolp item-thm).; stmt-value — An untranslated term.; new-compst — An untranslated term.; new-context — Guard (atc-contextp new-context).; new-inscope — Guard (atc-symbol-varinfo-alist-listp new-inscope).; gin — Guard (stmt-ginp gin).
Returns: gout — Type (stmt-goutp gout).

This is used to lift generated block items to generated block item lists. Besides the (singleton) block item list, we also generate a theorem saying that exec-block-item-list applied to the quoted block item list yields an mv pair consisting of a statement value term and a possibly updated computation state; these are the same as the ones for the single item theorem.

The limit for the block item list is 1 more than the limit for the block item, because we need 1 to go from exec-block-item-list to exec-block-item.

When this function is called on a block item that is an if that returns void, new-compst is an if* whose branches have the form (exit-scope ...) (after expanding lets). The combination of the rules compustatep-of-exit-scope and compustatep-of-if*-when-both-compustatep serves to show that compustatep holds on the if*, as needed during the proof, without having to expand the if*.

The new-inscope input is the variable table just after the block item.

Definitions and Theorems

Function: atc-gen-block-item-list-one

(defun atc-gen-block-item-list-one
       (term type item item-limit item-events
             item-thm stmt-value new-compst
             new-context new-inscope gin state)
 (declare (xargs :stobjs (state)))
 (declare
     (xargs :guard (and (pseudo-termp term)
                        (typep type)
                        (block-itemp item)
                        (pseudo-termp item-limit)
                        (pseudo-event-form-listp item-events)
                        (symbolp item-thm)
                        (atc-contextp new-context)
                        (atc-symbol-varinfo-alist-listp new-inscope)
                        (stmt-ginp gin))))
 (let ((__function__ 'atc-gen-block-item-list-one))
  (declare (ignorable __function__))
  (b*
   (((stmt-gin gin) gin)
    (wrld (w state))
    (items (list item))
    (items-limit (pseudo-term-fncall '+
                                     (list (pseudo-term-quote 1)
                                           item-limit)))
    ((when (not gin.proofs))
     (make-stmt-gout :items items
                     :type type
                     :term term
                     :context new-context
                     :inscope new-inscope
                     :limit items-limit
                     :events item-events
                     :thm-name nil
                     :thm-index gin.thm-index
                     :names-to-avoid gin.names-to-avoid))
    (name (pack gin.fn '-correct- gin.thm-index))
    (thm-index (1+ gin.thm-index))
    ((mv name names-to-avoid)
     (fresh-logical-name-with-$s-suffix
          name nil gin.names-to-avoid wrld))
    (voidp (type-case type :void))
    (exec-formula
     (cons
         'equal
         (cons (cons 'exec-block-item-list
                     (cons (cons 'quote (cons items 'nil))
                           (cons gin.compst-var
                                 (cons gin.fenv-var
                                       (cons gin.limit-var 'nil)))))
               (cons (cons 'mv
                           (cons stmt-value (cons new-compst 'nil)))
                     'nil))))
    (exec-formula
         (atc-contextualize exec-formula gin.context
                            gin.fn gin.fn-guard gin.compst-var
                            gin.limit-var items-limit t wrld))
    (uterm (untranslate$ term nil state))
    ((mv type-formula &)
     (atc-gen-term-type-formula
          uterm type
          gin.affect gin.inscope gin.prec-tags))
    (type-formula
         (atc-contextualize type-formula gin.context gin.fn
                            gin.fn-guard nil nil nil nil wrld))
    (formula (cons 'and
                   (cons exec-formula (cons type-formula 'nil))))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         (cons
          'quote
          (cons
           (cons
            'exec-block-item-list-when-consp
            (cons
             'not-zp-of-limit-variable
             (cons
              'mv-nth-of-cons
              (cons
               '(:e zp)
               (cons
                'value-optionp-when-valuep
                (cons
                 '(:e value-optionp)
                 (cons
                  '(:e valuep)
                  (append
                   (and
                    (not voidp)
                    (list
                       (atc-type-to-valuep-thm type gin.prec-tags)))
                   (cons
                    item-thm
                    '(exec-block-item-list-of-nil
                      return-type-of-stmt-value-return
                      return-type-of-stmt-value-none
                      stmt-value-return->value?-of-stmt-value-return
                      stmt-value-return-of-value-option-fix-value?
                      value-option-fix-when-value-optionp
                      not-zp-of-limit-minus-const
                      compustatep-of-exit-scope
                      compustatep-of-update-object
                      compustatep-of-update-static-var
                      compustatep-of-if*-when-both-compustatep
                      uchar-array-length-of-uchar-array-write
                      schar-array-length-of-schar-array-write
                      ushort-array-length-of-ushort-array-write
                      sshort-array-length-of-sshort-array-write
                      uint-array-length-of-uint-array-write
                      sint-array-length-of-sint-array-write
                      ulong-array-length-of-ulong-array-write
                      slong-array-length-of-slong-array-write
                      ullong-array-length-of-ullong-array-write
                      sllong-array-length-of-sllong-array-write))))))))))
           'nil))
         'nil)))
      'nil))
    ((mv event &)
     (evmac-generate-defthm name
                            :formula formula
                            :hints hints
                            :enable nil)))
   (make-stmt-gout :items items
                   :type type
                   :term term
                   :context new-context
                   :inscope new-inscope
                   :limit items-limit
                   :events (append item-events (list event))
                   :thm-name name
                   :thm-index thm-index
                   :names-to-avoid names-to-avoid))))

Theorem: stmt-goutp-of-atc-gen-block-item-list-one

(defthm stmt-goutp-of-atc-gen-block-item-list-one
  (b* ((gout (atc-gen-block-item-list-one
                  term type item item-limit item-events
                  item-thm stmt-value new-compst
                  new-context new-inscope gin state)))
    (stmt-goutp gout))
  :rule-classes :rewrite)