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 (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-external-declaration)) (declare (ignorable __function__)) (b* (((reterr) (irr-extdecl) (irr-span) parstate) ((erp token span parstate) (read-token parstate))) (cond ((token-keywordp token "_Static_assert") (b* (((erp statassert span parstate) (parse-static-assert-declaration span parstate))) (retok (extdecl-decl (decl-statassert statassert)) span parstate))) (t (b* (((mv extension parstate) (if (and (token-keywordp token "__extension__") (parstate->gcc parstate)) (mv t parstate) (b* ((parstate (if token (unread-token parstate) parstate))) (mv nil parstate)))) ((erp declspecs span parstate) (parse-declaration-specifiers nil parstate)) ((erp token2 span2 parstate) (read-token parstate))) (cond ((token-punctuatorp token2 ";") (retok (extdecl-decl (make-decl-decl :extension extension :specs declspecs :init nil :asm? nil :attrib nil)) (span-join span span2) parstate)) ((and (or (token-keywordp token2 "asm") (token-keywordp token2 "__asm") (token-keywordp token2 "__asm__")) (parstate->gcc parstate)) (b* ((uscores (cond ((token-keywordp token2 "asm") (keyword-uscores-none)) ((token-keywordp token2 "__asm") (keyword-uscores-start)) ((token-keywordp token2 "__asm__") (keyword-uscores-both)))) ((erp asmspec & parstate) (parse-asm-name-specifier uscores span2 parstate)) ((erp attrspecs & parstate) (parse-*-attribute-specifier parstate)) ((erp last-span parstate) (read-punctuator ";" parstate))) (retok (extdecl-decl (make-decl-decl :extension extension :specs declspecs :init nil :asm? asmspec :attrib attrspecs)) (span-join span last-span) parstate))) ((and (token-keywordp token2 "__attribute__") (parstate->gcc parstate)) (b* ((parstate (unread-token parstate)) ((erp attrspecs & parstate) (parse-*-attribute-specifier parstate)) ((erp last-span parstate) (read-punctuator ";" parstate))) (retok (extdecl-decl (make-decl-decl :extension extension :specs declspecs :init nil :asm? nil :attrib attrspecs)) (span-join span last-span) parstate))) (t (b* ((parstate (if token2 (unread-token parstate) parstate)) ((erp declor & parstate) (parse-declarator parstate)) ((erp token3 span3 parstate) (read-token parstate))) (cond ((token-punctuatorp token3 "=") (b* (((erp initer & parstate) (parse-initializer parstate)) ((erp token4 span4 parstate) (read-token parstate))) (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) parstate)) ((token-punctuatorp token4 ",") (b* (((erp initdeclors & parstate) (parse-init-declarator-list parstate)) ((erp asmspec? & parstate) (if (parstate->gcc parstate) (parse-?-asm-name-specifier parstate) (retok nil (irr-span) parstate))) ((erp attrspecs & parstate) (if (parstate->gcc parstate) (parse-*-attribute-specifier parstate) (retok nil (irr-span) parstate))) ((erp last-span parstate) (read-punctuator ";" parstate))) (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) parstate))) ((and (or (token-keywordp token4 "asm") (token-keywordp token4 "__asm") (token-keywordp token4 "__asm__")) (parstate->gcc parstate)) (b* ((uscore (cond ((token-keywordp token4 "asm") (keyword-uscores-none)) ((token-keywordp token4 "__asm") (keyword-uscores-start)) ((token-keywordp token4 "__asm__") (keyword-uscores-both)))) ((erp asmspec & parstate) (parse-asm-name-specifier uscore span4 parstate)) ((erp attrspecs & parstate) (parse-*-attribute-specifier parstate)) ((erp last-span parstate) (read-punctuator ";" parstate))) (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) parstate))) ((and (token-keywordp token4 "__attribute__") (parstate->gcc parstate)) (b* ((parstate (unread-token parstate)) ((erp attrspecs & parstate) (parse-*-attribute-specifier parstate)) ((erp last-span parstate) (read-punctuator ";" parstate))) (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) parstate))) (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) parstate)) ((token-punctuatorp token3 ",") (b* (((erp initdeclors & parstate) (parse-init-declarator-list parstate)) ((erp asmspec? & parstate) (parse-?-asm-name-specifier parstate)) ((erp attrspecs & parstate) (if (parstate->gcc parstate) (parse-*-attribute-specifier parstate) (retok nil (irr-span) parstate))) ((erp last-span parstate) (read-punctuator ";" parstate))) (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) parstate))) ((and (or (token-keywordp token3 "asm") (token-keywordp token3 "__asm") (token-keywordp token3 "__asm__")) (parstate->gcc parstate)) (b* ((uscores (cond ((token-keywordp token3 "asm") (keyword-uscores-none)) ((token-keywordp token3 "__asm") (keyword-uscores-start)) ((token-keywordp token3 "__asm__") (keyword-uscores-both)))) ((erp asmspec & parstate) (parse-asm-name-specifier uscores span3 parstate)) ((erp attrspecs & parstate) (parse-*-attribute-specifier parstate)) ((erp last-span parstate) (read-punctuator ";" parstate))) (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) parstate))) ((and (token-keywordp token3 "__attribute__") (parstate->gcc parstate)) (b* ((parstate (unread-token parstate)) ((erp attrspecs & parstate) (parse-*-attribute-specifier parstate)) ((erp last-span parstate) (read-punctuator ";" parstate))) (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) parstate))) ((token-punctuatorp token3 "{") (b* ((parstate (unread-token parstate)) ((erp stmt last-span parstate) (parse-statement parstate))) (retok (extdecl-fundef (make-fundef :extension extension :spec declspecs :declor declor :decls nil :body stmt)) (span-join span last-span) parstate))) (t (b* ((parstate (if token3 (unread-token parstate) parstate)) ((erp decls & parstate) (parse-declaration-list parstate)) ((erp token4 span4 parstate) (read-token parstate)) ((unless (token-punctuatorp token4 "{")) (reterr-msg :where (position-to-msg (span->start span4)) :expected "an open curly brace" :found (token-to-msg token4))) (parstate (unread-token parstate)) ((erp stmt last-span parstate) (parse-statement parstate))) (retok (extdecl-fundef (make-fundef :extension extension :spec declspecs :declor declor :decls decls :body stmt)) (span-join span last-span) parstate)))))))))))))
Theorem:
(defthm extdeclp-of-parse-external-declaration.extdecl (b* (((mv acl2::?erp ?extdecl ?span ?new-parstate) (parse-external-declaration parstate))) (extdeclp extdecl)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-parse-external-declaration.span (b* (((mv acl2::?erp ?extdecl ?span ?new-parstate) (parse-external-declaration parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-external-declaration.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?extdecl ?span ?new-parstate) (parse-external-declaration parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-external-declaration-uncond (b* (((mv acl2::?erp ?extdecl ?span ?new-parstate) (parse-external-declaration parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-external-declaration-cond (b* (((mv acl2::?erp ?extdecl ?span ?new-parstate) (parse-external-declaration parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)