		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-gen-init-inscope-auto

Generate the automatic storage scope of the initial symbol tale for a C function.

Signature
(atc-gen-init-inscope-auto 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 latter consists of the ACL2 function parameters that represent C function parameters (i.e. not external objects).

We go through the typed formals, and we select the ones not 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-auto

(defun atc-gen-init-inscope-auto
       (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-auto))
  (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 externalp)
     (atc-gen-init-inscope-auto
          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))
    (var/varptr (if (or (type-case type :pointer)
                        (type-case type :array))
                    (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))
         (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 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))))
    (not-flexiblep-thms
         (atc-type-to-notflexarrmem-thms type prec-tags))
    (valuep-when-type-pred (atc-type-to-valuep-thm type prec-tags))
    (value-kind-when-type-pred
         (atc-type-to-value-kind-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)
                  (append
                   not-flexiblep-thms
                   (cons
                    'remove-flexible-array-member-when-absent
                    (cons
                       'value-fix-when-valuep
                       (append (and (or (type-case type :pointer)
                                        (type-case type :array))
                                    '(read-object-of-add-var
                                          read-object-of-add-frame))
                               (cons valuep-when-type-pred
                                     (cons value-kind-when-type-pred
                                           'nil)))))))))))))
           '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-auto 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 nil))
             scope-rest)
       (cons event events-rest)
       names-to-avoid))))

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

(defthm atc-symbol-varinfo-alistp-of-atc-gen-init-inscope-auto.scope
 (implies
   (atc-symbol-varinfo-alistp typed-formals)
   (b*
     (((mv ?scope ?events ?names-to-avoid)
       (atc-gen-init-inscope-auto 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-auto.events

(defthm pseudo-event-form-listp-of-atc-gen-init-inscope-auto.events
 (b* (((mv ?scope ?events ?names-to-avoid)
       (atc-gen-init-inscope-auto 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-auto.names-to-avoid

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