		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-gen-init-inscope-static

Generate the static storage scope of the initial symbol table for a C function.

Signature
(atc-gen-init-inscope-static fn fn-guard typed-formals prec-tags compst-var context names-to-avoid wrld) → (mv scope events names-to-avoid)
Arguments: fn — Guard (symbolp fn).; fn-guard — Guard (symbolp fn-guard).; typed-formals — Guard (atc-symbol-varinfo-alistp typed-formals).; prec-tags — Guard (atc-string-taginfo-alistp prec-tags).; compst-var — Guard (symbolp compst-var).; context — Guard (atc-contextp context).; names-to-avoid — Guard (symbol-listp names-to-avoid).; wrld — Guard (plist-worldp wrld).
Returns: scope — Type (atc-symbol-varinfo-alistp scope), given (atc-symbol-varinfo-alistp typed-formals).; 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 consists of a scope for static storage and a scope for automatic storage. The former consists of the external objects passed as parameters to the ACL2 function that represents the C function (which in general is a subset of the external object in the program).

We go through the typed formals, and we select the ones representing external objects, generating an entry in the scope (alist) for each.

The -0 suffix that we use for the generated theorem name is motivated by the fact that these are the theorems for the initial symbol table; as we update the symbol table in the course of generating code, we use positive indices as suffixes.

Definitions and Theorems

Function: atc-gen-init-inscope-static

(defun atc-gen-init-inscope-static
       (fn fn-guard typed-formals prec-tags
           compst-var context names-to-avoid wrld)
 (declare
      (xargs :guard (and (symbolp fn)
                         (symbolp fn-guard)
                         (atc-symbol-varinfo-alistp typed-formals)
                         (atc-string-taginfo-alistp prec-tags)
                         (symbolp compst-var)
                         (atc-contextp context)
                         (symbol-listp names-to-avoid)
                         (plist-worldp wrld))))
 (let ((__function__ 'atc-gen-init-inscope-static))
  (declare (ignorable __function__))
  (b*
   (((when (endp typed-formals))
     (mv nil nil names-to-avoid))
    ((cons var info) (car typed-formals))
    (type (atc-var-info->type info))
    (var-thm (atc-var-info->thm info))
    (externalp (atc-var-info->externalp info))
    ((when (not externalp))
     (atc-gen-init-inscope-static
          fn fn-guard (cdr typed-formals)
          prec-tags
          compst-var context names-to-avoid wrld))
    (type-pred (atc-type-to-recognizer type prec-tags))
    (name (pack fn '- var '-in-scope-0))
    ((mv name names-to-avoid)
     (fresh-logical-name-with-$s-suffix
          name nil names-to-avoid wrld))
    (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 'nil)))
        'nil))))
    (formula1
         (atc-contextualize formula1 context
                            fn fn-guard compst-var nil nil t wrld))
    (formula2 (cons type-pred (cons var 'nil)))
    (formula2 (atc-contextualize formula2 context
                                 fn fn-guard nil nil nil nil wrld))
    (formula (cons 'and
                   (cons formula1 (cons formula2 'nil))))
    (valuep-when-type-pred (atc-type-to-valuep-thm type prec-tags))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         (cons
          'quote
          (cons
           (cons
            'objdesign-of-var-of-add-var-iff
            (cons
             'read-object-of-objdesign-of-var-of-add-var
             (cons
              var-thm
              (cons
               'ident-fix-when-identp
               (cons
                'identp-of-ident
                (cons
                 'equal-of-ident-and-ident
                 (cons
                  '(:e str-fix)
                  (cons
                      valuep-when-type-pred
                      '(objdesign-of-var-of-add-frame-when-read-object-static
                            (:t objdesign-static)
                            read-object-of-add-frame
                            return-type-of-objdesign-static)))))))))
           'nil))
         'nil)))
      'nil))
    ((mv event &)
     (evmac-generate-defthm name
                            :formula formula
                            :hints hints
                            :enable nil))
    ((mv scope-rest events-rest names-to-avoid)
     (atc-gen-init-inscope-static fn fn-guard (cdr typed-formals)
                                  prec-tags compst-var
                                  context names-to-avoid wrld)))
   (mv (cons (cons var
                   (make-atc-var-info :type type
                                      :thm name
                                      :externalp t))
             scope-rest)
       (cons event events-rest)
       names-to-avoid))))

Theorem: atc-symbol-varinfo-alistp-of-atc-gen-init-inscope-static.scope

(defthm
     atc-symbol-varinfo-alistp-of-atc-gen-init-inscope-static.scope
 (implies
  (atc-symbol-varinfo-alistp typed-formals)
  (b*
   (((mv ?scope ?events ?names-to-avoid)
     (atc-gen-init-inscope-static fn fn-guard
                                  typed-formals prec-tags compst-var
                                  context names-to-avoid wrld)))
   (atc-symbol-varinfo-alistp scope)))
 :rule-classes :rewrite)

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

(defthm
      pseudo-event-form-listp-of-atc-gen-init-inscope-static.events
  (b*
   (((mv ?scope ?events ?names-to-avoid)
     (atc-gen-init-inscope-static fn fn-guard
                                  typed-formals prec-tags compst-var
                                  context names-to-avoid wrld)))
   (pseudo-event-form-listp events))
  :rule-classes :rewrite)

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

(defthm symbol-listp-of-atc-gen-init-inscope-static.names-to-avoid
 (implies
  (symbol-listp names-to-avoid)
  (b*
   (((mv ?scope ?events ?names-to-avoid)
     (atc-gen-init-inscope-static fn fn-guard
                                  typed-formals prec-tags compst-var
                                  context names-to-avoid wrld)))
   (symbol-listp names-to-avoid)))
 :rule-classes :rewrite)