		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-fundef

Check a function definition.

Signature
(check-fundef fundef funtab vartab tagenv) → new-funtab
Arguments: fundef — Guard (fundefp fundef).; funtab — Guard (fun-tablep funtab).; vartab — Guard (var-tablep vartab).; tagenv — Guard (tag-envp tagenv).
Returns: new-funtab — Type (fun-table-resultp new-funtab).

We check the type specifier sequence and declarator, obtaining the variable table that includes the parameters. Importantly, the block items are checked in this variable table, which has the types for the function parameters, without creating a new scope for the block (i.e. the compound statement): the reason is that the scope of function parameters terminates at the end of the associated block [C:6.2.1/4].

The variable table passed as parameter to this ACL2 function always consists of just the current file scope, i.e. the file-scope variables that precede the function definition in the translation unit.

We ensure that the return types of the body match the return types of the function. Currently, this means that the set of return types must be a singleton with the function's return type; this may be relaxed in the future.

We also extend the function table with the new function. It is an error if a function with the same name is already in the table. In general, this must be done before checking the body: the function is in scope, in its own body.

The scope of a function identifier goes from its declaration to the end of the translation unit [C:6.2.1/4]. Thus, as we go through the function definitions in the translation unit in order, we extend the function table.

Definitions and Theorems

Function: check-fundef

(defun check-fundef (fundef funtab vartab tagenv)
 (declare (xargs :guard (and (fundefp fundef)
                             (fun-tablep funtab)
                             (var-tablep vartab)
                             (tag-envp tagenv))))
 (let ((__function__ 'check-fundef))
  (declare (ignorable __function__))
  (b*
   (((fundef fundef) fundef)
    ((mv name params out-tyname)
     (tyspec+declor-to-ident+params+tyname
          fundef.tyspec fundef.declor))
    ((okf out-type)
     (check-tyname out-tyname tagenv))
    ((okf vartab)
     (check-fun-declor fundef.declor vartab tagenv))
    ((mv & in-tynames)
     (param-declon-list-to-ident+tyname-lists params))
    (in-types (type-name-list-to-type-list in-tynames))
    (in-types (adjust-type-list in-types))
    ((okf funtab)
     (fun-table-add-fun name in-types out-type t funtab))
    ((okf stype)
     (check-block-item-list fundef.body funtab vartab tagenv))
    ((unless (equal (types+vartab->return-types stype)
                    (insert out-type nil)))
     (reserrf (list :fundef-return-mistype name
                    :required out-type
                    :inferred (types+vartab->return-types stype)))))
   funtab)))

Theorem: fun-table-resultp-of-check-fundef

(defthm fun-table-resultp-of-check-fundef
  (b* ((new-funtab (check-fundef fundef funtab vartab tagenv)))
    (fun-table-resultp new-funtab))
  :rule-classes :rewrite)

Theorem: check-fundef-of-fundef-fix-fundef

(defthm check-fundef-of-fundef-fix-fundef
  (equal (check-fundef (fundef-fix fundef)
                       funtab vartab tagenv)
         (check-fundef fundef funtab vartab tagenv)))

Theorem: check-fundef-fundef-equiv-congruence-on-fundef

(defthm check-fundef-fundef-equiv-congruence-on-fundef
  (implies (fundef-equiv fundef fundef-equiv)
           (equal (check-fundef fundef funtab vartab tagenv)
                  (check-fundef fundef-equiv funtab vartab tagenv)))
  :rule-classes :congruence)

Theorem: check-fundef-of-fun-table-fix-funtab

(defthm check-fundef-of-fun-table-fix-funtab
  (equal (check-fundef fundef (fun-table-fix funtab)
                       vartab tagenv)
         (check-fundef fundef funtab vartab tagenv)))

Theorem: check-fundef-fun-table-equiv-congruence-on-funtab

(defthm check-fundef-fun-table-equiv-congruence-on-funtab
  (implies (fun-table-equiv funtab funtab-equiv)
           (equal (check-fundef fundef funtab vartab tagenv)
                  (check-fundef fundef funtab-equiv vartab tagenv)))
  :rule-classes :congruence)

Theorem: check-fundef-of-var-table-fix-vartab

(defthm check-fundef-of-var-table-fix-vartab
  (equal (check-fundef fundef funtab (var-table-fix vartab)
                       tagenv)
         (check-fundef fundef funtab vartab tagenv)))

Theorem: check-fundef-var-table-equiv-congruence-on-vartab

(defthm check-fundef-var-table-equiv-congruence-on-vartab
  (implies (var-table-equiv vartab vartab-equiv)
           (equal (check-fundef fundef funtab vartab tagenv)
                  (check-fundef fundef funtab vartab-equiv tagenv)))
  :rule-classes :congruence)

Theorem: check-fundef-of-tag-env-fix-tagenv

(defthm check-fundef-of-tag-env-fix-tagenv
  (equal (check-fundef fundef
                       funtab vartab (tag-env-fix tagenv))
         (check-fundef fundef funtab vartab tagenv)))

Theorem: check-fundef-tag-env-equiv-congruence-on-tagenv

(defthm check-fundef-tag-env-equiv-congruence-on-tagenv
  (implies (tag-env-equiv tagenv tagenv-equiv)
           (equal (check-fundef fundef funtab vartab tagenv)
                  (check-fundef fundef funtab vartab tagenv-equiv)))
  :rule-classes :congruence)