Parse an external declaration.
An external declaration is
either a function definition,
which starts with a non-empty sequence of declaration specifiers,
or a declaration,
which also starts with a non-empty sequence of declaration specifiers,
unless it is a static assert declaration,
which starts with the keyword
No declaration specifier starts with the keyword
Otherwise, we read one or more declaration specifiers, since those are present both in declarations and in function definitions. Then we must have a declarator in either case, but based on what follows it, we can decide whether we have a declarator or a function definition.
If GCC extensions are supported, we must also taken into account
the possible presence of attributes and assembler name specifiers,
as well as of an
Function:
(defun parse-external-declaration (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-external-declaration)) (declare (ignorable __function__)) (b* (((reterr) (irr-extdecl) (irr-span) (irr-parstate)) ((erp token span pstate) (read-token pstate))) (cond ((token-keywordp token "_Static_assert") (b* (((erp statassert span pstate) (parse-static-assert-declaration span pstate))) (retok (extdecl-decl (decl-statassert statassert)) span pstate))) (t (b* (((mv extension pstate) (if (and (token-keywordp token "__extension__") (parstate->gcc pstate)) (mv t pstate) (mv nil (if token (unread-token pstate) pstate)))) ((erp declspecs span pstate) (parse-declaration-specifiers nil pstate)) ((erp token2 span2 pstate) (read-token pstate))) (cond ((token-punctuatorp token2 ";") (retok (extdecl-decl (make-decl-decl :extension extension :specs declspecs :init nil :asm? nil :attrib nil)) (span-join span span2) pstate)) ((and (or (token-keywordp token2 "asm") (token-keywordp token2 "__asm__")) (parstate->gcc pstate)) (b* ((uscores (token-keywordp token2 "__asm__")) ((erp asmspec & pstate) (parse-asm-name-specifier uscores span2 pstate)) ((erp attrspecs & pstate) (parse-*-attribute-specifier pstate)) ((erp last-span pstate) (read-punctuator ";" pstate))) (retok (extdecl-decl (make-decl-decl :extension extension :specs declspecs :init nil :asm? asmspec :attrib attrspecs)) (span-join span last-span) pstate))) ((and (token-keywordp token2 "__attribute__") (parstate->gcc pstate)) (b* ((pstate (unread-token pstate)) ((erp attrspecs & pstate) (parse-*-attribute-specifier pstate)) ((erp last-span pstate) (read-punctuator ";" pstate))) (retok (extdecl-decl (make-decl-decl :extension extension :specs declspecs :init nil :asm? nil :attrib attrspecs)) (span-join span last-span) pstate))) (t (b* ((pstate (if token2 (unread-token pstate) pstate)) ((erp declor & pstate) (parse-declarator pstate)) ((erp token3 span3 pstate) (read-token pstate))) (cond ((token-punctuatorp token3 "=") (b* (((erp initer & pstate) (parse-initializer pstate)) ((erp token4 span4 pstate) (read-token pstate))) (cond ((token-punctuatorp token4 ";") (retok (extdecl-decl (make-decl-decl :extension extension :specs declspecs :init (list (make-initdeclor :declor declor :init? initer)) :asm? nil :attrib nil)) (span-join span span4) pstate)) ((token-punctuatorp token4 ",") (b* (((erp initdeclors & pstate) (parse-init-declarator-list pstate)) ((erp asmspec? & pstate) (if (parstate->gcc pstate) (parse-?-asm-name-specifier pstate) (retok nil (irr-span) pstate))) ((erp attrspecs & pstate) (if (parstate->gcc pstate) (parse-*-attribute-specifier pstate) (retok nil (irr-span) pstate))) ((erp last-span pstate) (read-punctuator ";" pstate))) (retok (extdecl-decl (make-decl-decl :extension extension :specs declspecs :init (cons (make-initdeclor :declor declor :init? initer) initdeclors) :asm? asmspec? :attrib attrspecs)) (span-join span last-span) pstate))) ((and (or (token-keywordp token4 "asm") (token-keywordp token4 "__asm__")) (parstate->gcc pstate)) (b* ((uscore (token-keywordp token4 "__asm__")) ((erp asmspec & pstate) (parse-asm-name-specifier uscore span4 pstate)) ((erp attrspecs & pstate) (parse-*-attribute-specifier pstate)) ((erp last-span pstate) (read-punctuator ";" pstate))) (retok (extdecl-decl (make-decl-decl :extension extension :specs declspecs :init (list (make-initdeclor :declor declor :init? initer)) :asm? asmspec :attrib attrspecs)) (span-join span last-span) pstate))) ((and (token-keywordp token4 "__attribute__") (parstate->gcc pstate)) (b* ((pstate (unread-token pstate)) ((erp attrspecs & pstate) (parse-*-attribute-specifier pstate)) ((erp last-span pstate) (read-punctuator ";" pstate))) (retok (extdecl-decl (make-decl-decl :extension extension :specs declspecs :init (list (make-initdeclor :declor declor :init? initer)) :asm? nil :attrib attrspecs)) (span-join span last-span) pstate))) (t (reterr-msg :where (position-to-msg (span->start span4)) :expected "a semicolon or a comma" :found (token-to-msg token4)))))) ((token-punctuatorp token3 ";") (retok (extdecl-decl (make-decl-decl :extension extension :specs declspecs :init (list (make-initdeclor :declor declor :init? nil)) :asm? nil :attrib nil)) (span-join span span3) pstate)) ((token-punctuatorp token3 ",") (b* (((erp initdeclors & pstate) (parse-init-declarator-list pstate)) ((erp asmspec? & pstate) (parse-?-asm-name-specifier pstate)) ((erp attrspecs & pstate) (if (parstate->gcc pstate) (parse-*-attribute-specifier pstate) (retok nil (irr-span) pstate))) ((erp last-span pstate) (read-punctuator ";" pstate))) (retok (extdecl-decl (make-decl-decl :extension extension :specs declspecs :init (cons (make-initdeclor :declor declor :init? nil) initdeclors) :asm? asmspec? :attrib attrspecs)) (span-join span last-span) pstate))) ((and (or (token-keywordp token3 "asm") (token-keywordp token3 "__asm__")) (parstate->gcc pstate)) (b* ((uscores (token-keywordp token3 "__asm__")) ((erp asmspec & pstate) (parse-asm-name-specifier uscores span3 pstate)) ((erp attrspecs & pstate) (parse-*-attribute-specifier pstate)) ((erp last-span pstate) (read-punctuator ";" pstate))) (retok (extdecl-decl (make-decl-decl :extension extension :specs declspecs :init (list (make-initdeclor :declor declor :init? nil)) :asm? asmspec :attrib attrspecs)) (span-join span last-span) pstate))) ((and (token-keywordp token3 "__attribute__") (parstate->gcc pstate)) (b* ((pstate (unread-token pstate)) ((erp attrspecs & pstate) (parse-*-attribute-specifier pstate)) ((erp last-span pstate) (read-punctuator ";" pstate))) (retok (extdecl-decl (make-decl-decl :extension extension :specs declspecs :init (list (make-initdeclor :declor declor :init? nil)) :asm? nil :attrib attrspecs)) (span-join span last-span) pstate))) ((token-punctuatorp token3 "{") (b* ((pstate (unread-token pstate)) ((erp stmt last-span pstate) (parse-statement pstate))) (retok (extdecl-fundef (make-fundef :extension extension :spec declspecs :declor declor :decls nil :body stmt)) (span-join span last-span) pstate))) (t (b* ((pstate (if token3 (unread-token pstate) pstate)) ((erp decls & pstate) (parse-declaration-list pstate)) ((erp token4 span4 pstate) (read-token pstate)) ((unless (token-punctuatorp token4 "{")) (reterr-msg :where (position-to-msg (span->start span4)) :expected "an open curly brace" :found (token-to-msg token4))) (pstate (unread-token pstate)) ((erp stmt last-span pstate) (parse-statement pstate))) (retok (extdecl-fundef (make-fundef :extension extension :spec declspecs :declor declor :decls decls :body stmt)) (span-join span last-span) pstate)))))))))))))
Theorem:
(defthm extdeclp-of-parse-external-declaration.extdecl (b* (((mv acl2::?erp ?extdecl ?span ?new-pstate) (parse-external-declaration pstate))) (extdeclp extdecl)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-parse-external-declaration.span (b* (((mv acl2::?erp ?extdecl ?span ?new-pstate) (parse-external-declaration pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-external-declaration.new-pstate (b* (((mv acl2::?erp ?extdecl ?span ?new-pstate) (parse-external-declaration pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-external-declaration-uncond (b* (((mv acl2::?erp ?extdecl ?span ?new-pstate) (parse-external-declaration pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-external-declaration-cond (b* (((mv acl2::?erp ?extdecl ?span ?new-pstate) (parse-external-declaration pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)