		Search-engine friendly clone of the ACL2 documentation.

Disambiguator

Dimb-fundef

Disambiguate a function definition.

Signature
(dimb-fundef fundef table gcc) → (mv erp new-fundef new-table)
Arguments: fundef — Guard (fundefp fundef).; table — Guard (dimb-tablep table).; gcc — Guard (booleanp gcc).
Returns: erp — Type (maybe-msgp erp).; new-fundef — Type (fundefp new-fundef).; new-table — Type (dimb-tablep new-table).

We process the declaration specifiers, obtaining the kind of the identifier declared by the declarator, which in valid code must be :objfun, but we do not check this explicitly.

Then we process the declarator, passing t as the fundefp flag, because we are processing the declarator of a defined function. In valid code, this declarator will include a function declarator with either parameter declarations or identifiers, after it has been processed. Because of the fundefp flag set to t, the disambiguation table returned from dimb-declor should contain a newly pushed scope for the function definition. But this may not be the case in invalid code, so we check that this is the case explicitly here; without this check, the disambiguator may throw hard errors due to a violated expectation that the disambiguator table is not empty (we observed this in an example of invalid code, which motivated the addition of the check just described).

So with the check on the the validation tables described above, we know that we have added a scope to the disambiguation table. If the (disambiguated) declarator has parameter declarations, those will have added the formal parameters of the function to that scope. If instead the (disambiguated) declarator has just identifiers, the new scope will be empty, but the declarator will be followed, in the function definition, by declarations for the identifiers (again, assuming the code is valid).

As with declarations, the scope of the function name starts just after its declarator; it must be added to the file scope of the disambiguation table. However, recall that the disambiguation of the declarator pushes a new scope for the outermost block of the function definition. Thus, instead of using dimb-add-ident-objfun to add the function, we use dimb-add-ident-objfun-file-scope.

We process any declarations, which add function parameters to the scope that was added when processing the declarator.

Then we add the declared function to the disambiguation table, so that it can be referenced from the body, in a recursive call.

We extend the disambiguation table with the identifier __func__ [C17:6.4.2.2]. If the GCC flag is enabled (i.e. GCC extensions are allowed), we further extend the table with the identifiers __FUNCTION__ and __PRETTY_FUNCTION__ (GCC manual, ``Function Names'').

After all of that, we disambiguate the body of the function definition. But we do not push a new scope for the block, because the scope pushed by dimb-declor is already the one for the function body.

At the end, we pop the scope for the function definition, and we add the function to the table, so that it is available in the rest of the translation unit.

Definitions and Theorems

Function: dimb-fundef

(defun dimb-fundef (fundef table gcc)
 (declare (xargs :guard (and (fundefp fundef)
                             (dimb-tablep table)
                             (booleanp gcc))))
 (let ((__function__ 'dimb-fundef))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-fundef) (irr-dimb-table))
    ((fundef fundef) fundef)
    ((erp new-spec & table)
     (dimb-decl-spec-list fundef.spec (dimb-kind-objfun)
                          table))
    (nscopes (len table))
    ((erp new-declor ident table)
     (dimb-declor fundef.declor t table))
    ((unless (= (len table) (1+ nscopes)))
     (retmsg$
      "The function definition ~x0 is invalid, ~
                  because the disambiguation table after the declarator ~
                  does not have one scope more than before the declarator. ~
                  This is indicative of invalid code."
      (fundef-fix fundef)))
    (table (dimb-add-ident-objfun-file-scope ident table)
)
    ((erp new-decls table)
     (dimb-decl-list fundef.decls table))
    (table (dimb-add-ident-objfun (ident "__func__")
                                  table)
)
    (table
     (if gcc
       (dimb-add-idents-objfun (list (ident "__FUNCTION__")
                                     (ident "__PRETTY_FUNCTION__"))
                               table)
       table)
)
    ((erp new-body table)
     (dimb-comp-stmt fundef.body t table))
    (table (dimb-pop-scope table))
    (table (dimb-add-ident ident (dimb-kind-objfun)
                           table)
))
   (retok (make-fundef :extension fundef.extension
                       :spec new-spec
                       :declor new-declor
                       :decls new-decls
                       :body new-body
                       :info fundef.info)
          table))))

Theorem: maybe-msgp-of-dimb-fundef.erp

(defthm maybe-msgp-of-dimb-fundef.erp
  (b* (((mv acl2::?erp ?new-fundef ?new-table)
        (dimb-fundef fundef table gcc)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: fundefp-of-dimb-fundef.new-fundef

(defthm fundefp-of-dimb-fundef.new-fundef
  (b* (((mv acl2::?erp ?new-fundef ?new-table)
        (dimb-fundef fundef table gcc)))
    (fundefp new-fundef))
  :rule-classes :rewrite)

Theorem: dimb-tablep-of-dimb-fundef.new-table

(defthm dimb-tablep-of-dimb-fundef.new-table
  (b* (((mv acl2::?erp ?new-fundef ?new-table)
        (dimb-fundef fundef table gcc)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: fundef-unambp-of-dimb-fundef

(defthm fundef-unambp-of-dimb-fundef
  (b* (((mv acl2::?erp ?new-fundef ?new-table)
        (dimb-fundef fundef table gcc)))
    (implies (not erp)
             (fundef-unambp new-fundef))))

Theorem: dimb-fundef-of-fundef-fix-fundef

(defthm dimb-fundef-of-fundef-fix-fundef
  (equal (dimb-fundef (fundef-fix fundef)
                      table gcc)
         (dimb-fundef fundef table gcc)))

Theorem: dimb-fundef-fundef-equiv-congruence-on-fundef

(defthm dimb-fundef-fundef-equiv-congruence-on-fundef
  (implies (fundef-equiv fundef fundef-equiv)
           (equal (dimb-fundef fundef table gcc)
                  (dimb-fundef fundef-equiv table gcc)))
  :rule-classes :congruence)

Theorem: dimb-fundef-of-dimb-table-fix-table

(defthm dimb-fundef-of-dimb-table-fix-table
  (equal (dimb-fundef fundef (dimb-table-fix table)
                      gcc)
         (dimb-fundef fundef table gcc)))

Theorem: dimb-fundef-dimb-table-equiv-congruence-on-table

(defthm dimb-fundef-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-fundef fundef table gcc)
                  (dimb-fundef fundef table-equiv gcc)))
  :rule-classes :congruence)

Theorem: dimb-fundef-of-bool-fix-gcc

(defthm dimb-fundef-of-bool-fix-gcc
  (equal (dimb-fundef fundef table (bool-fix gcc))
         (dimb-fundef fundef table gcc)))

Theorem: dimb-fundef-iff-congruence-on-gcc

(defthm dimb-fundef-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (dimb-fundef fundef table gcc)
                  (dimb-fundef fundef table gcc-equiv)))
  :rule-classes :congruence)