		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-gen-pop-frame-thm

Generate the theorem about popping the frame at the end of a function execution.

Signature
(atc-gen-pop-frame-thm fn fn-guard body-term body-type body-correct-thm affect typed-formals compst-var prec-objs prec-tags context names-to-avoid wrld) → (mv thm-event thm-name names-to-avoid)
Arguments: fn — Guard (symbolp fn).; fn-guard — Guard (symbolp fn-guard).; body-term — An untranslated term.; body-type — Guard (typep body-type).; body-correct-thm — Guard (symbolp body-correct-thm).; affect — Guard (symbol-listp affect).; typed-formals — Guard (atc-symbol-varinfo-alistp typed-formals).; compst-var — Guard (symbolp compst-var).; prec-objs — Guard (atc-string-objinfo-alistp prec-objs).; prec-tags — Guard (atc-string-taginfo-alistp prec-tags).; context — Guard (atc-contextp context).; names-to-avoid — Guard (symbol-listp names-to-avoid).; wrld — Guard (plist-worldp wrld).
Returns: thm-event — Type (pseudo-event-formp thm-event).; thm-name — Type (symbolp thm-name).; names-to-avoid — Type (symbol-listp names-to-avoid), given (symbol-listp names-to-avoid).

This theorem says that popping the (top) frame in the computation state at the end of the function execution yields the initial computation state; this is only the case for the functions for which we support the generation of this theorem, of course; it is not true in general, and we will generalize this.

we ``save'' the initial computation state in a variable that we obtain by adding -init at the end of the symbol of the variable for the computation state. This does not interfere with any other variables, because of the dash which is disallowed in C variable names.

The context parameter of this ACL2 function is the context at the end of the function body; this is used to contextualize the computation state from where the frame is popped.

Definitions and Theorems

Function: atc-gen-pop-frame-thm-aux

(defun atc-gen-pop-frame-thm-aux (typed-formals)
 (declare (xargs :guard (atc-symbol-varinfo-alistp typed-formals)))
 (let ((__function__ 'atc-gen-pop-frame-thm-aux))
  (declare (ignorable __function__))
  (cond
       ((endp typed-formals) nil)
       (t (cons (atc-var-info->thm (cdar typed-formals))
                (atc-gen-pop-frame-thm-aux (cdr typed-formals)))))))

Theorem: symbol-listp-of-atc-gen-pop-frame-thm-aux

(defthm symbol-listp-of-atc-gen-pop-frame-thm-aux
  (b* ((thms (atc-gen-pop-frame-thm-aux typed-formals)))
    (symbol-listp thms))
  :rule-classes :rewrite)

Function: atc-gen-pop-frame-thm

(defun atc-gen-pop-frame-thm
       (fn fn-guard body-term
           body-type body-correct-thm affect
           typed-formals compst-var prec-objs
           prec-tags context names-to-avoid wrld)
 (declare
      (xargs :guard (and (symbolp fn)
                         (symbolp fn-guard)
                         (typep body-type)
                         (symbolp body-correct-thm)
                         (symbol-listp affect)
                         (atc-symbol-varinfo-alistp typed-formals)
                         (symbolp compst-var)
                         (atc-string-objinfo-alistp prec-objs)
                         (atc-string-taginfo-alistp prec-tags)
                         (atc-contextp context)
                         (symbol-listp names-to-avoid)
                         (plist-worldp wrld))))
 (let ((__function__ 'atc-gen-pop-frame-thm))
  (declare (ignorable __function__))
  (b*
   ((compst-init-var (pack compst-var '-init))
    (name (pack fn '-pop-frame))
    ((mv name names-to-avoid)
     (fresh-logical-name-with-$s-suffix
          name nil names-to-avoid wrld))
    (new-compst (atc-gen-fun-endstate affect typed-formals
                                      compst-init-var prec-objs))
    (binder
      (if (type-case body-type :void)
          (if (consp (cdr affect))
              (cons 'mv
                    (acl2::add-suffix-to-fn-lst affect "-NEW"))
            (add-suffix-to-fn (car affect) "-NEW"))
        (if (consp affect)
            (cons 'mv
                  (cons '&
                        (acl2::add-suffix-to-fn-lst affect "-NEW")))
          nil)))
    (formula (cons 'equal
                   (cons (cons 'pop-frame (cons compst-var 'nil))
                         (cons new-compst 'nil))))
    (formula
         (atc-contextualize formula context
                            fn fn-guard compst-var nil nil t wrld))
    (formula
     (cons 'let
           (cons (cons (cons compst-init-var (cons compst-var 'nil))
                       'nil)
                 (cons formula 'nil))))
    (formula
         (if binder
             (cons 'b*
                   (cons (cons (cons binder (cons body-term 'nil))
                               'nil)
                         (cons formula 'nil)))
           formula))
    (formals-thms (atc-gen-pop-frame-thm-aux typed-formals))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         (cons
          'quote
          (cons
           (cons
            'pop-frame-of-if*
            (cons
             'update-var-of-enter-scope
             (cons
              'update-var-of-add-var
              (cons
               'exit-scope-of-enter-scope
               (cons
                'exit-scope-of-add-var
                (cons
                 'compustate-frames-number-of-add-var-not-zero
                 (cons
                  'compustate-frames-number-of-enter-scope-not-zero
                  (cons
                   'compustate-frames-number-of-add-frame-not-zero
                   (cons
                    'compustatep-of-add-var
                    (cons
                     'compustatep-of-enter-scope
                     (cons
                      'pop-frame-of-add-var
                      (cons
                       'pop-frame-of-add-frame
                       (cons
                        'acl2::if*-when-same
                        (cons
                         'update-object-of-enter-scope
                         (cons
                          'compustatep-of-update-object
                          (cons
                           'compustate-frames-number-of-update-object
                           (cons
                            'update-object-of-add-var
                            (cons
                             'update-object-of-add-frame
                             (cons
                              'write-object-to-update-object
                              (cons
                               'write-object-okp-of-update-object-same
                               (cons
                                'write-object-okp-of-update-object-disjoint
                                (cons
                                 'write-object-okp-when-valuep-of-read-object-no-syntaxp
                                 (cons
                                  'write-object-okp-of-if*-val
                                  (append
                                   formals-thms
                                   (cons
                                    'valuep-when-ucharp
                                    (cons
                                     'valuep-when-scharp
                                     (cons
                                      'valuep-when-ushortp
                                      (cons
                                       'valuep-when-sshortp
                                       (cons
                                        'valuep-when-uintp
                                        (cons
                                         'valuep-when-sintp
                                         (cons
                                          'valuep-when-ulongp
                                          (cons
                                           'valuep-when-slongp
                                           (cons
                                            'valuep-when-ullongp
                                            (cons
                                             'valuep-when-sllongp
                                             (cons
                                              'valuep-when-uchar-arrayp
                                              (cons
                                               'valuep-when-schar-arrayp
                                               (cons
                                                'valuep-when-ushort-arrayp
                                                (cons
                                                 'valuep-when-sshort-arrayp
                                                 (cons
                                                  'valuep-when-uint-arrayp
                                                  (cons
                                                   'valuep-when-sint-arrayp
                                                   (cons
                                                    'valuep-when-ulong-arrayp
                                                    (cons
                                                     'valuep-when-slong-arrayp
                                                     (cons
                                                      'valuep-when-ullong-arrayp
                                                      (cons
                                                       'valuep-when-sllong-arrayp
                                                       (append
                                                        (atc-string-taginfo-alist-to-valuep-thms
                                                          prec-tags)
                                                        (cons
                                                         'type-of-value-when-ucharp
                                                         (cons
                                                          'type-of-value-when-scharp
                                                          (cons
                                                           'type-of-value-when-ushortp
                                                           (cons
                                                            'type-of-value-when-sshortp
                                                            (cons
                                                             'type-of-value-when-uintp
                                                             (cons
                                                              'type-of-value-when-sintp
                                                              (cons
                                                               'type-of-value-when-ulongp
                                                               (cons
                                                                'type-of-value-when-slongp
                                                                (cons
                                                                 'type-of-value-when-ullongp
                                                                 (cons
                                                                  'type-of-value-when-sllongp
                                                                  (cons
                                                                   'type-of-value-when-uchar-arrayp
                                                                   (cons
                                                                    'type-of-value-when-schar-arrayp
                                                                    (cons
                                                                     'type-of-value-when-ushort-arrayp
                                                                     (cons
                                                                     
 'type-of-value-when-sshort-arrayp
                                                                     
 (cons
                                                                     
  'type-of-value-when-uint-arrayp
                                                                     
  (cons
                                                                     
   'type-of-value-when-sint-arrayp
                                                                     
   (cons
                                                                     
    'type-of-value-when-ulong-arrayp
                                                                     
    (cons
                                                                     
     'type-of-value-when-slong-arrayp
                                                                     
     (cons
                                                                     
      'type-of-value-when-ullong-arrayp
                                                                     
      (cons
                                                                     
       'type-of-value-when-sllong-arrayp
                                                                     
       (append
                                                                     
        (atc-string-taginfo-alist-to-type-of-value-thms
                                                                     
         prec-tags)
                                                                     
        (cons
                                                                     
         'uchar-arrayp-of-uchar-array-write
                                                                     
         (cons
                                                                     
          'schar-arrayp-of-schar-array-write
                                                                     
          (cons
                                                                     
           'ushort-arrayp-of-ushort-array-write
                                                                     
           (cons
                                                                     
            'sshort-arrayp-of-sshort-array-write
                                                                     
            (cons
                                                                     
             'uint-arrayp-of-uint-array-write
                                                                     
             (cons
                                                                     
              'sint-arrayp-of-sint-array-write
                                                                     
              (cons
                                                                     
               'ulong-arrayp-of-ulong-array-write
                                                                     
               (cons
                                                                     
                'slong-arrayp-of-slong-array-write
                                                                     
                (cons
                                                                     
                 'ullong-arrayp-of-ullong-array-write
                                                                     
                 (cons
                                                                     
                  'sllong-arrayp-of-sllong-array-write
                                                                     
                  (cons
                                                                     
                   'value-array->length-when-uchar-arrayp
                                                                     
                   (cons
                                                                     
                    'value-array->length-when-schar-arrayp
                                                                     
                    (cons
                                                                     
                     'value-array->length-when-ushort-arrayp
                                                                     
                     (cons
                                                                     
                      'value-array->length-when-sshort-arrayp
                                                                     
                      (cons
                                                                     
                       'value-array->length-when-uint-arrayp
                                                                     
                       (cons
                                                                     
                        'value-array->length-when-sint-arrayp
                                                                     
                        (cons
                                                                     
                         'value-array->length-when-ulong-arrayp
                                                                     
                         (cons
                                                                     
                          'value-array->length-when-slong-arrayp
                                                                     
                          (cons
                                                                     
                           'value-array->length-when-ullong-arrayp
                                                                     
                           (cons
                                                                     
                            'value-array->length-when-sllong-arrayp
                                                                     
                            (cons
                                                                     
                             'uchar-array-length-of-uchar-array-write
                                                                     
                             (cons
                                                                     
                              'schar-array-length-of-schar-array-write
                                                                     
                              (cons
                                                                     
                               'ushort-array-length-of-ushort-array-write
                                                                     
                               (cons
                                                                     
                                'sshort-array-length-of-sshort-array-write
                                                                     
                                (cons
                                                                     
                                 'uint-array-length-of-uint-array-write
                                                                     
                                 (cons
                                                                     
                                  'sint-array-length-of-sint-array-write
                                                                     
                                  (cons
                                                                     
                                   'ulong-array-length-of-ulong-array-write
                                                                     
                                   (cons
                                                                     
                                    'slong-array-length-of-slong-array-write
                                                                     
                                    (cons
                                                                     
                                     'ullong-array-length-of-ullong-array-write
                                                                     
                                     (cons
                                                                     
                                      'sllong-array-length-of-sllong-array-write
                                                                     
                                      (cons
                                                                     
                                       'update-object-of-if*-val
                                                                     
                                       (cons
                                                                     
                                        'update-object-of-read-object-same
                                                                     
                                        (cons
                                                                     
                                         'update-object-of-update-object-same
                                                                     
                                         (cons
                                                                     
                                          'update-object-of-update-object-less-symbol
                                                                     
                                          (cons
                                                                     
                                           'update-object-of-update-object-less-ident
                                                                     
                                           (cons
                                                                     
                                            'update-object-of-update-var
                                                                     
                                            (cons
                                                                     
                                             'update-object-of-update-static-var
                                                                     
                                             (cons
                                                                     
                                              'update-static-var-of-add-var
                                                                     
                                              (cons
                                                                     
                                               'update-static-var-of-add-frame
                                                                     
                                               (cons
                                                                     
                                                'compustatep-of-update-static-var
                                                                     
                                                (cons
                                                                     
                                                 'write-static-var-to-update-static-var
                                                                     
                                                 (cons
                                                                     
                                                  'write-static-var-okp-when-valuep-of-read-static-var
                                                                     
                                                  (cons
                                                                     
                                                   'read-object-of-objdesign-static
                                                                     
                                                   (cons
                                                                     
                                                    'exit-scope-of-if*
                                                                     
                                                    (cons
                                                                     
                                                     'write-static-var-to-update-static-var
                                                                     
                                                     (cons
                                                                     
                                                      'update-static-var-of-enter-scope
                                                                     
                                                      (cons
                                                                     
                                                       'compustatep-of-add-frame
                                                                     
                                                       (cons
                                                                     
                                                        'update-static-var-of-if*-val
                                                                     
                                                        (cons
                                                                     
                                                         'object-disjointp-commutative
                                                                     
                                                         (cons
                                                                     
                                                          'mv-nth-of-cons
                                                                     
                                                          (cons
                                                                     
                                                           '(:e
                                                                     
                                                             zp)
                                                                     
                                                           (cons
                                                                     
                                                            body-correct-thm
                                                                     
                                                            'nil))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
           'nil))
         'nil)))
      '((and stable-under-simplificationp
             '(:in-theory '(if* mv-nth-of-cons (:e zp)))))))
    ((mv event &)
     (evmac-generate-defthm name
                            :formula formula
                            :hints hints
                            :enable nil)))
   (mv event name names-to-avoid))))

Theorem: pseudo-event-formp-of-atc-gen-pop-frame-thm.thm-event

(defthm pseudo-event-formp-of-atc-gen-pop-frame-thm.thm-event
  (b*
   (((mv ?thm-event ?thm-name ?names-to-avoid)
     (atc-gen-pop-frame-thm fn fn-guard body-term
                            body-type body-correct-thm affect
                            typed-formals compst-var prec-objs
                            prec-tags context names-to-avoid wrld)))
   (pseudo-event-formp thm-event))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-gen-pop-frame-thm.thm-name

(defthm symbolp-of-atc-gen-pop-frame-thm.thm-name
  (b*
   (((mv ?thm-event ?thm-name ?names-to-avoid)
     (atc-gen-pop-frame-thm fn fn-guard body-term
                            body-type body-correct-thm affect
                            typed-formals compst-var prec-objs
                            prec-tags context names-to-avoid wrld)))
   (symbolp thm-name))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-gen-pop-frame-thm.names-to-avoid

(defthm symbol-listp-of-atc-gen-pop-frame-thm.names-to-avoid
 (implies
  (symbol-listp names-to-avoid)
  (b*
   (((mv ?thm-event ?thm-name ?names-to-avoid)
     (atc-gen-pop-frame-thm fn fn-guard body-term
                            body-type body-correct-thm affect
                            typed-formals compst-var prec-objs
                            prec-tags context names-to-avoid wrld)))
   (symbol-listp names-to-avoid)))
 :rule-classes :rewrite)