		Search-engine friendly clone of the ACL2 documentation.

Atc-statement-generation

Atc-gen-block-item-stmt

Generate a C block item that consists of a given statement.

Signature
(atc-gen-block-item-stmt stmt stmt-limit stmt-events stmt-thm uterm? type result new-compst gin state) → (mv item item-limit item-events item-thm thm-index names-to-avoid)
Arguments: stmt — Guard (stmtp stmt).; stmt-limit — Guard (pseudo-termp stmt-limit).; stmt-events — Guard (pseudo-event-form-listp stmt-events).; stmt-thm — Guard (symbolp stmt-thm).; uterm? — An untranslated term.; type — Guard (typep type).; result — An untranslated term.; new-compst — An untranslated term.; gin — Guard (stmt-ginp gin).
Returns: item — Type (block-itemp item).; item-limit — Type (pseudo-termp item-limit).; item-events — Type (pseudo-event-form-listp item-events), given (pseudo-event-form-listp stmt-events).; item-thm — Type (symbolp item-thm).; thm-index — Type (posp thm-index).; names-to-avoid — Type (symbol-listp names-to-avoid).

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

If uterm? is not nil, we also generate, as part of the theorem, an assertion that the term returns a value, or values, of the expected type(s). Callers pass a non-nil uterm? when the blok item corresponds to a full ACL2 term (e.g. a conditional); while they pass nil otherwise (e.g. for an assignment).

The limit for the block item is 1 more than the limit for the statement, because we need 1 to go from exec-block-item to the :stmt case and exec-stmt.

Definitions and Theorems

Function: atc-gen-block-item-stmt

(defun atc-gen-block-item-stmt
       (stmt stmt-limit stmt-events stmt-thm
             uterm? type result new-compst gin state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (stmtp stmt)
                             (pseudo-termp stmt-limit)
                             (pseudo-event-form-listp stmt-events)
                             (symbolp stmt-thm)
                             (typep type)
                             (stmt-ginp gin))))
 (let ((__function__ 'atc-gen-block-item-stmt))
  (declare (ignorable __function__))
  (b*
   (((stmt-gin gin) gin)
    (wrld (w state))
    (item (block-item-stmt stmt))
    (item-limit (pseudo-term-fncall 'binary-+
                                    (list (pseudo-term-quote 1)
                                          stmt-limit)))
    (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))
    (exec-formula
     (cons
         'equal
         (cons (cons 'exec-block-item
                     (cons (cons 'quote (cons item 'nil))
                           (cons gin.compst-var
                                 (cons gin.fenv-var
                                       (cons gin.limit-var 'nil)))))
               (cons (cons 'mv
                           (cons result (cons new-compst 'nil)))
                     'nil))))
    (exec-formula
         (atc-contextualize exec-formula gin.context
                            gin.fn gin.fn-guard gin.compst-var
                            gin.limit-var item-limit t wrld))
    (formula
     (if uterm?
      (b*
       (((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)))
       (cons 'and
             (cons exec-formula (cons type-formula 'nil))))
      exec-formula))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         (cons
          'quote
          (cons
           (cons
            'exec-block-item-when-stmt
            (cons
             '(:e block-item-kind)
             (cons
              'not-zp-of-limit-variable
              (cons
               '(:e block-item-stmt->get)
               (cons
                stmt-thm
                '(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)))
   (mv item item-limit
       (append stmt-events (list event))
       name thm-index names-to-avoid))))

Theorem: block-itemp-of-atc-gen-block-item-stmt.item

(defthm block-itemp-of-atc-gen-block-item-stmt.item
  (b*
   (((mv ?item ?item-limit ?item-events
         ?item-thm ?thm-index ?names-to-avoid)
     (atc-gen-block-item-stmt stmt
                              stmt-limit stmt-events stmt-thm uterm?
                              type result new-compst gin state)))
   (block-itemp item))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-atc-gen-block-item-stmt.item-limit

(defthm pseudo-termp-of-atc-gen-block-item-stmt.item-limit
  (b*
   (((mv ?item ?item-limit ?item-events
         ?item-thm ?thm-index ?names-to-avoid)
     (atc-gen-block-item-stmt stmt
                              stmt-limit stmt-events stmt-thm uterm?
                              type result new-compst gin state)))
   (pseudo-termp item-limit))
  :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-atc-gen-block-item-stmt.item-events

(defthm
     pseudo-event-form-listp-of-atc-gen-block-item-stmt.item-events
 (implies
  (pseudo-event-form-listp stmt-events)
  (b*
   (((mv ?item ?item-limit ?item-events
         ?item-thm ?thm-index ?names-to-avoid)
     (atc-gen-block-item-stmt stmt
                              stmt-limit stmt-events stmt-thm uterm?
                              type result new-compst gin state)))
   (pseudo-event-form-listp item-events)))
 :rule-classes :rewrite)

Theorem: symbolp-of-atc-gen-block-item-stmt.item-thm

(defthm symbolp-of-atc-gen-block-item-stmt.item-thm
  (b*
   (((mv ?item ?item-limit ?item-events
         ?item-thm ?thm-index ?names-to-avoid)
     (atc-gen-block-item-stmt stmt
                              stmt-limit stmt-events stmt-thm uterm?
                              type result new-compst gin state)))
   (symbolp item-thm))
  :rule-classes :rewrite)

Theorem: posp-of-atc-gen-block-item-stmt.thm-index

(defthm posp-of-atc-gen-block-item-stmt.thm-index
  (b*
   (((mv ?item ?item-limit ?item-events
         ?item-thm ?thm-index ?names-to-avoid)
     (atc-gen-block-item-stmt stmt
                              stmt-limit stmt-events stmt-thm uterm?
                              type result new-compst gin state)))
   (posp thm-index))
  :rule-classes (:rewrite :type-prescription))

Theorem: symbol-listp-of-atc-gen-block-item-stmt.names-to-avoid

(defthm symbol-listp-of-atc-gen-block-item-stmt.names-to-avoid
  (b*
   (((mv ?item ?item-limit ?item-events
         ?item-thm ?thm-index ?names-to-avoid)
     (atc-gen-block-item-stmt stmt
                              stmt-limit stmt-events stmt-thm uterm?
                              type result new-compst gin state)))
   (symbol-listp names-to-avoid))
  :rule-classes :rewrite)