		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-fundef

Validate a function definition.

Signature
(valid-fundef fundef table ienv) → (mv erp new-fundef new-table)
Arguments: fundef — Guard (fundefp fundef).; table — Guard (valid-tablep table).; ienv — Guard (ienvp ienv).
Returns: new-fundef — Type (fundefp new-fundef).; new-table — Type (valid-tablep new-table).

For now we ignore all the GCC extensions. We validate the declaration specifiers, then the declarator. It is an error if the validation of the declarator returns a non-empty set of types, because it means that there are statement expressions with return statements in them, which can only happen inside a function's body. We validate the storage class specifiers. It is an error if the declaration is for a typedef. We also ensure that the type is the function type [C:6.9.1/2].

As with declarations, the scope of the function name starts just after its declarator; it must be added to the file scope of the validation table. However, recall that the validation of the declarator pushes a new scope for the outermost block of the function definition. Thus, instead of using valid-add-ord to add the function, we use valid-add-ord-file-scope. But before adding it, we need to look it up, and again in the file scope, not the block scope (it is in fact legal for a function parameter to have the same name as the function: its scope is the block, and it hides the function name there); so we use valid-lookup-ord-file-scope instead of the usual valid-lookup-ord.

If the name of the function is not found in the file scope, we add it to the file scope, with the appropriate information. Note that the definition status is defined, since we are validating a function definition. If the name is found already, and does not denote a function, it is an error; it is also an error if the linkages do not match. And it is an error if the function is alread defined. If all the checks pass, we add the function to the table, which overwrites the previous entry, but the only information actually overwritten is the definition status, from undefined to defiend, which is appropriate.

The declarations between declarator and body should be present if and only if the function declarator has a list of identifiers, and there should be exactly one declaration per identifier [C:6.9.1/5] [C:6.9.1/6]. For now we do not check those constraints, but we validate any declarations (ensuring they return no types), which will add entries to the block scope in the validation table.

We ensure that the body is a compound statement, and we validate directly the block items; this way, we do not push an extra scope, because the outer scope must include the parameters. In our approximate type system, the function type alone does not give us enough information to check the types returned by the body against the return type of the function, to enforce the constraints in [C:6.8.6.4/1]; so for now we discard the set of return types obtained by validating the body.

Finally we pop the scope of the function body. Recall that the function itself stays in the validation table, because we have added it to the file scope.

Definitions and Theorems

Function: valid-fundef

(defun valid-fundef (fundef table ienv)
 (declare (xargs :guard (and (fundefp fundef)
                             (valid-tablep table)
                             (ienvp ienv))))
 (declare (xargs :guard (fundef-unambp fundef)))
 (let ((__function__ 'valid-fundef))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     (irr-fundef)
     (irr-valid-table))
    ((fundef fundef) fundef)
    ((erp new-spec type storspecs types table)
     (valid-decl-spec-list fundef.spec nil nil nil table ienv))
    ((erp new-declor
          & type ident more-types table)
     (valid-declor fundef.declor t type table ienv))
    ((unless (and (emptyp types)
                  (emptyp more-types)))
     (reterr
      (msg
       "The declarator of the function definition ~x0 ~
                      contains return statements."
       (fundef-fix fundef))))
    ((erp typedefp linkage &)
     (valid-stor-spec-list storspecs ident type t table))
    ((when typedefp)
     (reterr
      (msg
       "The function definition ~x0 ~
                      declares a 'typedef' name instead of a function."
       (fundef-fix fundef))))
    ((unless (type-case type :function))
     (reterr (msg "The function definition ~x0 has type ~x1."
                  (fundef-fix fundef)
                  type)))
    (info? (valid-lookup-ord-file-scope ident table))
    ((erp table)
     (b*
      (((reterr) (irr-valid-table))
       ((when (not info?))
        (retok (valid-add-ord-file-scope
                    ident
                    (make-valid-ord-info-objfun
                         :type (type-function)
                         :linkage linkage
                         :defstatus (valid-defstatus-defined))
                    table)))
       (info info?)
       ((unless (valid-ord-info-case info :objfun))
        (reterr
         (msg
          "The name of the function definition ~x0 ~
                            is already in the file scope, ~
                            but is not a function; ~
                            its associated information is ~x1."
          (fundef-fix fundef)
          info)))
       ((valid-ord-info-objfun info) info)
       ((unless (type-case info.type :function))
        (reterr
         (msg
          "The name of the function definition ~x0 ~
                            is already in the file scope, ~
                            but it has type ~x1."
          (fundef-fix fundef)
          info.type)))
       ((unless (equal linkage info.linkage))
        (reterr
         (msg
          "The function definition ~x0 has linkage ~s1, ~
                            which is inconsistent with the linkage ~s2 ~
                            already present in the validation table."
          (fundef-fix fundef)
          (if (linkage-case linkage :external)
              "external"
            "internal")
          (if (linkage-case info.linkage :external)
              "external"
            "internal"))))
       ((when (valid-defstatus-case info.defstatus :defined))
        (reterr
         (msg
          "The function definition ~x0 ~
                            is a redefinition of the function."
          (fundef-fix fundef)))))
      (retok (valid-add-ord-file-scope
                  ident
                  (make-valid-ord-info-objfun
                       :type (type-function)
                       :linkage linkage
                       :defstatus (valid-defstatus-defined))
                  table))))
    ((erp new-decls types table)
     (valid-decl-list fundef.decls table ienv))
    ((unless (emptyp types))
     (reterr
      (msg
       "The declarations of the function definition ~x0 ~
                      contain return statements."
       (fundef-fix fundef))))
    ((unless (stmt-case fundef.body :compound))
     (reterr
      (msg
       "The function definition ~x0 ~
                      does not have a compound statement as body."
       (fundef-fix fundef))))
    (items (stmt-compound->items fundef.body))
    ((erp new-items & & table)
     (valid-block-item-list items table ienv))
    (table (valid-pop-scope table)))
   (retok (make-fundef :extension fundef.extension
                       :spec new-spec
                       :declor new-declor
                       :asm? fundef.asm?
                       :attribs fundef.attribs
                       :decls new-decls
                       :body (stmt-compound new-items))
          table))))

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

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

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

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

Theorem: valid-fundef-of-fundef-fix-fundef

(defthm valid-fundef-of-fundef-fix-fundef
  (equal (valid-fundef (fundef-fix fundef)
                       table ienv)
         (valid-fundef fundef table ienv)))

Theorem: valid-fundef-fundef-equiv-congruence-on-fundef

(defthm valid-fundef-fundef-equiv-congruence-on-fundef
  (implies (fundef-equiv fundef fundef-equiv)
           (equal (valid-fundef fundef table ienv)
                  (valid-fundef fundef-equiv table ienv)))
  :rule-classes :congruence)

Theorem: valid-fundef-of-valid-table-fix-table

(defthm valid-fundef-of-valid-table-fix-table
  (equal (valid-fundef fundef (valid-table-fix table)
                       ienv)
         (valid-fundef fundef table ienv)))

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

(defthm valid-fundef-valid-table-equiv-congruence-on-table
  (implies (valid-table-equiv table table-equiv)
           (equal (valid-fundef fundef table ienv)
                  (valid-fundef fundef table-equiv ienv)))
  :rule-classes :congruence)

Theorem: valid-fundef-of-ienv-fix-ienv

(defthm valid-fundef-of-ienv-fix-ienv
  (equal (valid-fundef fundef table (ienv-fix ienv))
         (valid-fundef fundef table ienv)))

Theorem: valid-fundef-ienv-equiv-congruence-on-ienv

(defthm valid-fundef-ienv-equiv-congruence-on-ienv
  (implies (ienv-equiv ienv ienv-equiv)
           (equal (valid-fundef fundef table ienv)
                  (valid-fundef fundef table ienv-equiv)))
  :rule-classes :congruence)