		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-stor-spec-list

Validate a list of storage class specifiers.

Signature
(valid-stor-spec-list storspecs ident type fundefp table) → (mv erp typedefp linkage lifetime?)
Arguments: storspecs — Guard (stor-spec-listp storspecs).; ident — Guard (identp ident).; type — Guard (typep type).; fundefp — Guard (booleanp fundefp).; table — Guard (valid-tablep table).
Returns: erp — Type (maybe-msgp erp).; typedefp — Type (booleanp typedefp).; linkage — Type (linkagep linkage).; lifetime? — Type (lifetime-optionp lifetime?).

This function is called on the sub-list of storage class specifiers of a list of declaration specifiers, after determining the identifier being declared and its type, which are both passed as input to this function, along with the current validation table.

Only a few sequences of storage class specifiers are allowed [C17:6.7.1/2], also depending on whether the declaration is in a block or file scope [C17:6.7.1/3], which we can see from the validation table. Each allowed sequence of storage class specifiers may determine that a typedef name is being declared, or that an object or function is being declared, with a certain linkage and lifetime. So we return as results a flag saying that a typedef name is being declared, a linkage, and an optional lifetime. We explain all the possibilities below, for each allowed sequence of storage class specifiers.

If the storage class specifier sequence is typedef, a typedef name is being declared, so we return t as the typedef flag result. This is the only case in which this result is t; in all other cases, that result is nil, because in all other cases we are not declaring a typedef name. A typedef name (which is an identifier) has no linkage [C17:6.2.2/1] [C17:6.2.2/6]. Since lifetime (i.e. storage duration) only applies to objects [C17:6.2.4/1], we return nil as lifetime, i.e. no lifetime.

If the storage class specifier sequence is extern, linkage may be external or not, based on whether there is already a declaration of the same identifiers in scope or not and whether that previous declaration specifies a linkage or not [C17:6.2.2/4]. So we look up the identifier in the validation table. If nothing is found, then the linkage is external. If an object or function is found with external or internal linkage, then the linkage of the new declaration is the one of that object or function; the two declarations must refer to the same object or function, but we check elsewhere that the two declarations are consistent with each other. If an object or function is found with no linkage, or a typedef is found (which has no linkage [C17:6.2.2/6]), or an enumeration constant is found (which has no linkage [C17:6.2.2/6]), then the linkage of the new declaration is external; the two declarations must refer to different entities. In any case, the linkage is always either internal or external. If the type is that of a function, there is no lifetime, which only applies to objects [C17:6.2.4/1]. If the type is that of an object, the lifetime is static [C17:6.2.4/3], because as mentioned above the linkage is always internal or external.

If the storage class specifier sequence is extern _Thread_local or _Thread_local extern, then the type must not be that of a function [C17:6.7.1/4]. The lifetime is thread [C17:6.2.4/4], while the linkage is determined as in the extern case above.

If the storage class specifier sequence is static, things differ whether the identifier is declared in the file scope or in a block scope. If we are in the file scope, the linkage is internal [C17:6.2.2/3]. If we are in a block scope, it depends on whether we are declaring an object or a function. If it is an object, it has no linkage [C17:6.2.2/6], because it does not have extern. If it is a function it is an error [C17:6.7.1/7]. The lifetime is absent (i.e. nil) for a function, since lifetimes only apply to objects [C17:6.2.4/1]; it is static otherwise [C17:6.2.4/3].

If the storage class specifier sequence is static _Thread_local or _Thread_local static, then the type must not be that of a function [C17:6.7.1/4]. Linkage is determined as in the previous case. The lifetime is thread.

If the storage class specifier sequence is _Thread_local, the type must not be one of a function [C17:6.7.1/4]. Since we must have an object, the lifetime is thread. If we are in a block scope, it is an error, because in that case there must also be extern or static [C17:6.7.1/3]. Since we cannot be in a block scope, we must be in the file scope. [C17:6.2.2] does not seem to specify the linkage for this case, perhaps because _Thread_local was added at some point, but [C17:6.2.2] was not updated accordingly: [C17:6.2.2/5] specifies external linkage for the case of an object in a file scope without storage class specifiers, but this should be probably interpreted as including the _Thread_local case, which makes sense, and is consistent with some clearer wording in the newly released C23 standard.

If the storage class specifier sequence is auto or register, we must not be in a file scope [C17:6.9/2]; so we must be in a block scope. The type must not be one of a function. Thus, it has no linkage [C17:6.2.2/6]. The lifetime is automatic [C17:6.2.4/5].

If there are no storage class specifiers (i.e. the sequence is empty), things differ based on whether the identifier declares an object or a function, and whether we are in the file scope or a block scope. If the type is that of a function, linkage is determined as if it had the extern specifier [C17:6.2.2/5]; in this case, there is no lifetime. For an object with file scope, the linkage is external [C17:6.2.2/5], and thus the lifetime is static [C17:6.2.4/3]. For an object block scope, there is no linkage [C17:6.2.2/6], and the lifetime is automatic [C17:6.2.4/5].

We prove that if typedefp is t then lifetime? is nil and there is no linkage. We prove that if a function is being declared, then the linkage is always external or internal, and that the only possible sequences of storage class specifiers are extern, static, and nothing. We prove that if an object is declared in the file scope, then the linkage is always external or internal.

The fundefp input is t when this function is called on the storage class specifiers of a function definition. The reason is that, when this function is called in that situation, the validation table contains a block scope for the function body, but the storage class specifiers checked here are in the file scope: so checking the validation table to determine, for the purpose of validating the storage class specifiers, whether we are in a block or file scope, would give an incorrect result. So we use the fundefp flag to adjust the check. This flag is nil in all other situations.

Definitions and Theorems

Function: valid-stor-spec-list

(defun valid-stor-spec-list (storspecs ident type fundefp table)
 (declare (xargs :guard (and (stor-spec-listp storspecs)
                             (identp ident)
                             (typep type)
                             (booleanp fundefp)
                             (valid-tablep table))))
 (b* (((reterr) nil (irr-linkage) nil))
  (cond
   ((stor-spec-list-typedef-p storspecs)
    (retok t (linkage-none) nil))
   ((stor-spec-list-extern-p storspecs)
    (b*
     ((linkage
        (b*
         (((mv info? &)
           (valid-lookup-ord ident table))
          ((unless info?) (linkage-external))
          ((unless (valid-ord-info-case info? :objfun))
           (linkage-external))
          (previous-linkage (valid-ord-info-objfun->linkage info?)))
         (if (linkage-case previous-linkage :none)
             (linkage-external)
           previous-linkage)))
      (lifetime? (if (type-case type :function)
                     nil
                   (lifetime-static))))
     (retok nil linkage lifetime?)))
   ((stor-spec-list-extern-thread-p storspecs)
    (b*
     (((when (type-case type :function))
       (retmsg$
        "The storage class specifier '_Thread_local' ~
                      cannot be used in the declaration of the function ~x0."
        (ident-fix ident)))
      (linkage
        (b*
         (((mv info? &)
           (valid-lookup-ord ident table))
          ((unless info?) (linkage-external))
          ((unless (valid-ord-info-case info? :objfun))
           (linkage-external))
          (previous-linkage (valid-ord-info-objfun->linkage info?)))
         (if (linkage-case previous-linkage :none)
             (linkage-external)
           previous-linkage))))
     (retok nil linkage (lifetime-thread))))
   ((stor-spec-list-static-p storspecs)
    (b*
     ((block-scope-p (and (> (valid-table-num-scopes table) 1)
                          (not fundefp)))
      ((when (and block-scope-p
                  (type-case type :function)))
       (retmsg$
        "The storage class specifier 'static' ~
                      cannot be used in the declaration of the function ~x0."
        (ident-fix ident)))
      (linkage (if block-scope-p (linkage-none)
                 (linkage-internal)))
      (lifetime? (if (type-case type :function)
                     nil
                   (lifetime-static))))
     (retok nil linkage lifetime?)))
   ((stor-spec-list-static-thread-p storspecs)
    (b*
     (((when (type-case type :function))
       (retmsg$
        "The storage class specifier '_Thread_local' ~
                      cannot be used in the declaration of the function ~x0."
        (ident-fix ident)))
      (block-scope-p (and (> (valid-table-num-scopes table) 1)
                          (not fundefp)))
      (linkage (if block-scope-p (linkage-none)
                 (linkage-internal)))
      (lifetime? (lifetime-thread)))
     (retok nil linkage lifetime?)))
   ((stor-spec-list-thread-p storspecs)
    (b*
     (((when (type-case type :function))
       (retmsg$
        "The storage class specifier '_Thread_local' ~
                      cannot be used in the declaration of the function ~x0."
        (ident-fix ident)))
      ((when (and (> (valid-table-num-scopes table) 1)
                  (not fundefp)))
       (retmsg$
        "The storage class specifier '_Thread_local' ~
                      cannot be used in a block scope ~
                      without 'extern' or 'static', ~
                      for the declaration of the object ~x0."
        (ident-fix ident))))
     (retok nil (linkage-external)
            (lifetime-thread))))
   ((or (stor-spec-list-auto-p storspecs)
        (stor-spec-list-register-p storspecs))
    (b*
     (((when (type-case type :function))
       (retmsg$
        "The storage class specifier '~s0' ~
                      cannot be used in the declaration of the function ~x1."
        (if (stor-spec-list-auto-p storspecs)
            "auto"
          "register")
        (ident-fix ident)))
      ((unless (and (> (valid-table-num-scopes table) 1)
                    (not fundefp)))
       (retmsg$
        "The storage class specifier '~s0' ~
                      cannot be used in the file scope, for identifier ~x1."
        (if (stor-spec-list-auto-p storspecs)
            "auto"
          "register")
        (ident-fix ident))))
     (retok nil (linkage-none)
            (lifetime-auto))))
   ((endp storspecs)
    (if
     (type-case type :function)
     (b* (((mv info? &)
           (valid-lookup-ord ident table))
          ((unless info?)
           (retok nil (linkage-external) nil))
          ((unless (valid-ord-info-case info? :objfun))
           (retok nil (linkage-external) nil))
          (previous-linkage (valid-ord-info-objfun->linkage info?)))
       (if (linkage-case previous-linkage :none)
           (retok nil (linkage-external) nil)
         (retok nil previous-linkage nil)))
     (if (and (> (valid-table-num-scopes table) 1)
              (not fundefp))
         (retok nil (linkage-none)
                (lifetime-auto))
       (retok nil (linkage-external)
              (lifetime-static)))))
   (t
     (retmsg$ "The storage class specifier sequence ~x0 is invalid."
              (stor-spec-list-fix storspecs))))))

Theorem: maybe-msgp-of-valid-stor-spec-list.erp

(defthm maybe-msgp-of-valid-stor-spec-list.erp
  (b* (((mv acl2::?erp
            ?typedefp ?linkage ?lifetime?)
        (valid-stor-spec-list storspecs ident type fundefp table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: booleanp-of-valid-stor-spec-list.typedefp

(defthm booleanp-of-valid-stor-spec-list.typedefp
  (b* (((mv acl2::?erp
            ?typedefp ?linkage ?lifetime?)
        (valid-stor-spec-list storspecs ident type fundefp table)))
    (booleanp typedefp))
  :rule-classes :rewrite)

Theorem: linkagep-of-valid-stor-spec-list.linkage

(defthm linkagep-of-valid-stor-spec-list.linkage
  (b* (((mv acl2::?erp
            ?typedefp ?linkage ?lifetime?)
        (valid-stor-spec-list storspecs ident type fundefp table)))
    (linkagep linkage))
  :rule-classes :rewrite)

Theorem: lifetime-optionp-of-valid-stor-spec-list.lifetime?

(defthm lifetime-optionp-of-valid-stor-spec-list.lifetime?
  (b* (((mv acl2::?erp
            ?typedefp ?linkage ?lifetime?)
        (valid-stor-spec-list storspecs ident type fundefp table)))
    (lifetime-optionp lifetime?))
  :rule-classes :rewrite)

Theorem: no-lifetime-of-valid-stor-spec-list-when-typedef

(defthm no-lifetime-of-valid-stor-spec-list-when-typedef
  (b* (((mv acl2::?erp
            ?typedefp ?linkage ?lifetime?)
        (valid-stor-spec-list storspecs ident type fundefp table)))
    (implies typedefp (not lifetime?))))

Theorem: no-linkage-of-valid-stor-spec-list-when-typedef

(defthm no-linkage-of-valid-stor-spec-list-when-typedef
  (b* (((mv acl2::?erp
            ?typedefp ?linkage ?lifetime?)
        (valid-stor-spec-list storspecs ident type fundefp table)))
    (implies typedefp
             (equal (linkage-kind linkage) :none))))

Theorem: ext/int-linkage-of-valid-stor-spec-when-function

(defthm ext/int-linkage-of-valid-stor-spec-when-function
  (b* (((mv acl2::?erp
            ?typedefp ?linkage ?lifetime?)
        (valid-stor-spec-list storspecs ident type fundefp table)))
    (implies (and (not erp)
                  (not typedefp)
                  (type-case type :function))
             (not (equal (linkage-kind linkage) :none)))))

Theorem: ext/int-linkage-of-valid-stor-spec-list-when-file-object

(defthm ext/int-linkage-of-valid-stor-spec-list-when-file-object
  (b* (((mv acl2::?erp
            ?typedefp ?linkage ?lifetime?)
        (valid-stor-spec-list storspecs ident type fundefp table)))
    (implies (and (not erp)
                  (not typedefp)
                  (not (type-case type :function))
                  (equal (valid-table-num-scopes table)
                         1))
             (not (equal (linkage-kind linkage) :none)))))

Theorem: lifetime-of-valid-stor-spec-when-object

(defthm lifetime-of-valid-stor-spec-when-object
  (b* (((mv acl2::?erp
            ?typedefp ?linkage ?lifetime?)
        (valid-stor-spec-list storspecs ident type fundefp table)))
    (implies (and (not erp)
                  (not typedefp)
                  (not (type-case type :function)))
             lifetime?)))

Theorem: extern/static/none-when-valid-stor-spec-list-function

(defthm extern/static/none-when-valid-stor-spec-list-function
  (b* (((mv acl2::?erp
            ?typedefp ?linkage ?lifetime?)
        (valid-stor-spec-list storspecs ident type fundefp table)))
    (implies (and (not erp)
                  (not typedefp)
                  (type-case type :function))
             (or (stor-spec-list-extern-p storspecs)
                 (stor-spec-list-static-p storspecs)
                 (endp storspecs)))))

Theorem: valid-stor-spec-list-of-stor-spec-list-fix-storspecs

(defthm valid-stor-spec-list-of-stor-spec-list-fix-storspecs
  (equal (valid-stor-spec-list (stor-spec-list-fix storspecs)
                               ident type fundefp table)
         (valid-stor-spec-list storspecs ident type fundefp table)))

Theorem: valid-stor-spec-list-stor-spec-list-equiv-congruence-on-storspecs

(defthm
  valid-stor-spec-list-stor-spec-list-equiv-congruence-on-storspecs
 (implies
    (stor-spec-list-equiv storspecs storspecs-equiv)
    (equal (valid-stor-spec-list storspecs ident type fundefp table)
           (valid-stor-spec-list storspecs-equiv
                                 ident type fundefp table)))
 :rule-classes :congruence)

Theorem: valid-stor-spec-list-of-ident-fix-ident

(defthm valid-stor-spec-list-of-ident-fix-ident
  (equal (valid-stor-spec-list storspecs (ident-fix ident)
                               type fundefp table)
         (valid-stor-spec-list storspecs ident type fundefp table)))

Theorem: valid-stor-spec-list-ident-equiv-congruence-on-ident

(defthm valid-stor-spec-list-ident-equiv-congruence-on-ident
 (implies
    (ident-equiv ident ident-equiv)
    (equal (valid-stor-spec-list storspecs ident type fundefp table)
           (valid-stor-spec-list storspecs
                                 ident-equiv type fundefp table)))
 :rule-classes :congruence)

Theorem: valid-stor-spec-list-of-type-fix-type

(defthm valid-stor-spec-list-of-type-fix-type
  (equal (valid-stor-spec-list storspecs ident (type-fix type)
                               fundefp table)
         (valid-stor-spec-list storspecs ident type fundefp table)))

Theorem: valid-stor-spec-list-type-equiv-congruence-on-type

(defthm valid-stor-spec-list-type-equiv-congruence-on-type
 (implies
    (type-equiv type type-equiv)
    (equal (valid-stor-spec-list storspecs ident type fundefp table)
           (valid-stor-spec-list storspecs
                                 ident type-equiv fundefp table)))
 :rule-classes :congruence)

Theorem: valid-stor-spec-list-of-bool-fix-fundefp

(defthm valid-stor-spec-list-of-bool-fix-fundefp
  (equal
       (valid-stor-spec-list storspecs ident type (bool-fix fundefp)
                             table)
       (valid-stor-spec-list storspecs ident type fundefp table)))

Theorem: valid-stor-spec-list-iff-congruence-on-fundefp

(defthm valid-stor-spec-list-iff-congruence-on-fundefp
 (implies
    (iff fundefp fundefp-equiv)
    (equal (valid-stor-spec-list storspecs ident type fundefp table)
           (valid-stor-spec-list storspecs
                                 ident type fundefp-equiv table)))
 :rule-classes :congruence)

Theorem: valid-stor-spec-list-of-valid-table-fix-table

(defthm valid-stor-spec-list-of-valid-table-fix-table
  (equal (valid-stor-spec-list storspecs ident
                               type fundefp (valid-table-fix table))
         (valid-stor-spec-list storspecs ident type fundefp table)))

Theorem: valid-stor-spec-list-valid-table-equiv-congruence-on-table

(defthm valid-stor-spec-list-valid-table-equiv-congruence-on-table
 (implies
    (valid-table-equiv table table-equiv)
    (equal (valid-stor-spec-list storspecs ident type fundefp table)
           (valid-stor-spec-list storspecs
                                 ident type fundefp table-equiv)))
 :rule-classes :congruence)