		Search-engine friendly clone of the ACL2 documentation.

Atc-theorem-generation

Atc-gen-new-inscope

Generate an updated symbol table according to given criteria.

Signature
(atc-gen-new-inscope fn fn-guard inscope new-context compst-var rules prec-tags thm-index names-to-avoid wrld) → (mv new-inscope events names-to-avoid)
Arguments: fn — Guard (symbolp fn).; fn-guard — Guard (symbolp fn-guard).; inscope — Guard (atc-symbol-varinfo-alist-listp inscope).; new-context — Guard (atc-contextp new-context).; compst-var — Guard (symbolp compst-var).; rules — Guard (true-listp rules).; prec-tags — Guard (atc-string-taginfo-alistp prec-tags).; thm-index — Guard (posp thm-index).; names-to-avoid — Guard (symbol-listp names-to-avoid).; wrld — Guard (plist-worldp wrld).
Returns: new-inscope — Type (atc-symbol-varinfo-alist-listp new-inscope), given (atc-symbol-varinfo-alist-listp inscope).; events — Type (pseudo-event-form-listp events).; names-to-avoid — Type (symbol-listp names-to-avoid), given (symbol-listp names-to-avoid).

The initial symbol table is generated by atc-gen-init-inscope; see the documentation of that function. As we process ACL2 terms that represent C constructs, sometimes we need to generate an updated symbol table, which is mostly the same as the one just before the update, but with new theorems about the variables in it. For instance, when entering a scope, the new symbol table is almost the same, with the addition of a new empty scope; but the theorems about the variables in scope must be rephrased to be about the computation state updated with the new scope.

This ACL2 function goes through the given symbol table inscope and constructs an updated symbol table new-inscope from it, with the same scopes and variables, but different theorems (see below). Callers of this ACL2 function can further update the returned symbol table; for instance, when encountering a new variable declaration, the caller of this ACL2 function adds the new variable.

The input context new-context is already the new context, created by the caller of this ACL2 function by updating the previous context, e.g. by adding a computation state binding for entering a scope.

The theorems of the updated symbol table are generated here. They say that reading each C variable yields the corresponding ACL2 variable or the -ptr ACL2 variable, in the computation state updated according to the (new) context. Each new theorem is proved from the old theorem, using rules passed to this ACL2 function, since the rules may differ depending on the specifics of the updated context and computation state.

Since the generated theorem names involve the names of the variables, which are always distinct in a symbol table generated by ATC, we use the same theorem index for all the theorems.

Definitions and Theorems

Function: atc-gen-new-inscope-aux

(defun atc-gen-new-inscope-aux
       (fn fn-guard
           scope new-context compst-var rules
           prec-tags thm-index names-to-avoid wrld)
 (declare (xargs :guard (and (symbolp fn)
                             (symbolp fn-guard)
                             (atc-symbol-varinfo-alistp scope)
                             (atc-contextp new-context)
                             (symbolp compst-var)
                             (true-listp rules)
                             (atc-string-taginfo-alistp prec-tags)
                             (posp thm-index)
                             (symbol-listp names-to-avoid)
                             (plist-worldp wrld))))
 (let ((__function__ 'atc-gen-new-inscope-aux))
  (declare (ignorable __function__))
  (b*
   (((when (endp scope))
     (mv nil nil names-to-avoid))
    ((cons var info) (car scope))
    (type (atc-var-info->type info))
    (thm (atc-var-info->thm info))
    (externalp (atc-var-info->externalp info))
    (type-pred (atc-type-to-recognizer type prec-tags))
    (new-thm (pack fn '- var '-in-scope- thm-index))
    ((mv new-thm names-to-avoid)
     (fresh-logical-name-with-$s-suffix
          new-thm nil names-to-avoid wrld))
    (var/varptr (if (and (or (type-case type :pointer)
                             (type-case type :array))
                         (not externalp))
                    (add-suffix-to-fn var "-PTR")
                  var))
    (formula1
     (cons
      'and
      (cons
       (cons 'objdesign-of-var
             (cons (cons 'ident
                         (cons (symbol-name var) 'nil))
                   (cons compst-var 'nil)))
       (cons
        (cons
         'equal
         (cons
          (cons
              'read-object
              (cons (cons 'objdesign-of-var
                          (cons (cons 'ident
                                      (cons (symbol-name var) 'nil))
                                (cons compst-var 'nil)))
                    (cons compst-var 'nil)))
          (cons var/varptr 'nil)))
        (and
         (or (type-case type :pointer)
             (type-case type :array))
         (not externalp)
         (cons
            (cons 'equal
                  (cons (cons 'read-object
                              (cons (add-suffix-to-fn var "-OBJDES")
                                    (cons compst-var 'nil)))
                        (cons var 'nil)))
            'nil))))))
    (formula1
         (atc-contextualize formula1 new-context
                            fn fn-guard compst-var nil nil t wrld))
    (formula2 (cons type-pred (cons var 'nil)))
    (formula2 (atc-contextualize formula2 new-context
                                 fn fn-guard nil nil nil nil wrld))
    (formula (cons 'and
                   (cons formula1 (cons formula2 'nil))))
    (hints
         (cons (cons '"Goal"
                     (cons ':in-theory
                           (cons (cons 'quote
                                       (cons (cons thm rules) 'nil))
                                 'nil)))
               'nil))
    ((mv event &)
     (evmac-generate-defthm new-thm
                            :formula formula
                            :hints hints
                            :enable nil))
    (new-info (change-atc-var-info info :thm new-thm))
    (rest (cdr scope))
    ((mv new-rest events names-to-avoid)
     (atc-gen-new-inscope-aux fn fn-guard rest
                              new-context compst-var rules prec-tags
                              thm-index names-to-avoid wrld)))
   (mv (acons var new-info new-rest)
       (cons event events)
       names-to-avoid))))

Theorem: atc-symbol-varinfo-alistp-of-atc-gen-new-inscope-aux.new-scope

(defthm
     atc-symbol-varinfo-alistp-of-atc-gen-new-inscope-aux.new-scope
 (implies
  (atc-symbol-varinfo-alistp scope)
  (b*
   (((mv ?new-scope ?events ?names-to-avoid)
     (atc-gen-new-inscope-aux fn fn-guard scope
                              new-context compst-var rules prec-tags
                              thm-index names-to-avoid wrld)))
   (atc-symbol-varinfo-alistp new-scope)))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-atc-gen-new-inscope-aux.events

(defthm pseudo-event-form-listp-of-atc-gen-new-inscope-aux.events
  (b*
   (((mv ?new-scope ?events ?names-to-avoid)
     (atc-gen-new-inscope-aux fn fn-guard scope
                              new-context compst-var rules prec-tags
                              thm-index names-to-avoid wrld)))
   (pseudo-event-form-listp events))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-gen-new-inscope-aux.names-to-avoid

(defthm symbol-listp-of-atc-gen-new-inscope-aux.names-to-avoid
 (implies
  (symbol-listp names-to-avoid)
  (b*
   (((mv ?new-scope ?events ?names-to-avoid)
     (atc-gen-new-inscope-aux fn fn-guard scope
                              new-context compst-var rules prec-tags
                              thm-index names-to-avoid wrld)))
   (symbol-listp names-to-avoid)))
 :rule-classes :rewrite)

Function: atc-gen-new-inscope

(defun atc-gen-new-inscope
       (fn fn-guard
           inscope new-context compst-var rules
           prec-tags thm-index names-to-avoid wrld)
 (declare
      (xargs :guard (and (symbolp fn)
                         (symbolp fn-guard)
                         (atc-symbol-varinfo-alist-listp inscope)
                         (atc-contextp new-context)
                         (symbolp compst-var)
                         (true-listp rules)
                         (atc-string-taginfo-alistp prec-tags)
                         (posp thm-index)
                         (symbol-listp names-to-avoid)
                         (plist-worldp wrld))))
 (let ((__function__ 'atc-gen-new-inscope))
  (declare (ignorable __function__))
  (b*
   (((when (endp inscope))
     (mv nil nil names-to-avoid))
    (scope (car inscope))
    ((mv new-scope events names-to-avoid)
     (atc-gen-new-inscope-aux fn fn-guard scope
                              new-context compst-var rules prec-tags
                              thm-index names-to-avoid wrld))
    (scopes (cdr inscope))
    ((mv new-scopes more-events names-to-avoid)
     (atc-gen-new-inscope fn fn-guard scopes
                          new-context compst-var rules prec-tags
                          thm-index names-to-avoid wrld)))
   (mv (cons new-scope new-scopes)
       (append events more-events)
       names-to-avoid))))

Theorem: atc-symbol-varinfo-alist-listp-of-atc-gen-new-inscope.new-inscope

(defthm
  atc-symbol-varinfo-alist-listp-of-atc-gen-new-inscope.new-inscope
 (implies
   (atc-symbol-varinfo-alist-listp inscope)
   (b* (((mv ?new-inscope ?events ?names-to-avoid)
         (atc-gen-new-inscope fn fn-guard inscope
                              new-context compst-var rules prec-tags
                              thm-index names-to-avoid wrld)))
     (atc-symbol-varinfo-alist-listp new-inscope)))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-atc-gen-new-inscope.events

(defthm pseudo-event-form-listp-of-atc-gen-new-inscope.events
  (b* (((mv ?new-inscope ?events ?names-to-avoid)
        (atc-gen-new-inscope fn fn-guard inscope
                             new-context compst-var rules prec-tags
                             thm-index names-to-avoid wrld)))
    (pseudo-event-form-listp events))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-gen-new-inscope.names-to-avoid

(defthm symbol-listp-of-atc-gen-new-inscope.names-to-avoid
 (implies
   (symbol-listp names-to-avoid)
   (b* (((mv ?new-inscope ?events ?names-to-avoid)
         (atc-gen-new-inscope fn fn-guard inscope
                              new-context compst-var rules prec-tags
                              thm-index names-to-avoid wrld)))
     (symbol-listp names-to-avoid)))
 :rule-classes :rewrite)