Commit f1d236b8 authored by xleroy's avatar xleroy
Browse files

Integration of Jacques-Henri Jourdan's verified parser.

(Merge of branch newparser.)


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2469 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
parent 39df8fb1
......@@ -146,4 +146,17 @@ flocq/Prop/Fprop_Sterbenz.vo flocq/Prop/Fprop_Sterbenz.glob flocq/Prop/Fprop_Ste
flocq/Appli/Fappli_rnd_odd.vo flocq/Appli/Fappli_rnd_odd.glob flocq/Appli/Fappli_rnd_odd.v.beautified: flocq/Appli/Fappli_rnd_odd.v flocq/Core/Fcore.vo flocq/Calc/Fcalc_ops.vo
flocq/Appli/Fappli_IEEE.vo flocq/Appli/Fappli_IEEE.glob flocq/Appli/Fappli_IEEE.v.beautified: flocq/Appli/Fappli_IEEE.v flocq/Core/Fcore.vo flocq/Core/Fcore_digits.vo flocq/Calc/Fcalc_digits.vo flocq/Calc/Fcalc_round.vo flocq/Calc/Fcalc_bracket.vo flocq/Calc/Fcalc_ops.vo flocq/Calc/Fcalc_div.vo flocq/Calc/Fcalc_sqrt.vo flocq/Prop/Fprop_relative.vo
flocq/Appli/Fappli_IEEE_bits.vo flocq/Appli/Fappli_IEEE_bits.glob flocq/Appli/Fappli_IEEE_bits.v.beautified: flocq/Appli/Fappli_IEEE_bits.v flocq/Core/Fcore.vo flocq/Core/Fcore_digits.vo flocq/Calc/Fcalc_digits.vo flocq/Appli/Fappli_IEEE.vo
cparser/validator/Alphabet.vo cparser/validator/Alphabet.glob cparser/validator/Alphabet.v.beautified: cparser/validator/Alphabet.v
cparser/validator/Interpreter_complete.vo cparser/validator/Interpreter_complete.glob cparser/validator/Interpreter_complete.v.beautified: cparser/validator/Interpreter_complete.v cparser/validator/Alphabet.vo cparser/validator/Grammar.vo cparser/validator/Automaton.vo cparser/validator/Interpreter.vo cparser/validator/Validator_complete.vo
cparser/validator/Interpreter.vo cparser/validator/Interpreter.glob cparser/validator/Interpreter.v.beautified: cparser/validator/Interpreter.v cparser/validator/Automaton.vo cparser/validator/Alphabet.vo
cparser/validator/Validator_complete.vo cparser/validator/Validator_complete.glob cparser/validator/Validator_complete.v.beautified: cparser/validator/Validator_complete.v cparser/validator/Automaton.vo cparser/validator/Alphabet.vo
cparser/validator/Automaton.vo cparser/validator/Automaton.glob cparser/validator/Automaton.v.beautified: cparser/validator/Automaton.v cparser/validator/Grammar.vo cparser/validator/Alphabet.vo
cparser/validator/Interpreter_correct.vo cparser/validator/Interpreter_correct.glob cparser/validator/Interpreter_correct.v.beautified: cparser/validator/Interpreter_correct.v cparser/validator/Alphabet.vo cparser/validator/Grammar.vo cparser/validator/Automaton.vo cparser/validator/Interpreter.vo
cparser/validator/Main.vo cparser/validator/Main.glob cparser/validator/Main.v.beautified: cparser/validator/Main.v cparser/validator/Grammar.vo cparser/validator/Automaton.vo cparser/validator/Interpreter_safe.vo cparser/validator/Interpreter_correct.vo cparser/validator/Interpreter_complete.vo
cparser/validator/Validator_safe.vo cparser/validator/Validator_safe.glob cparser/validator/Validator_safe.v.beautified: cparser/validator/Validator_safe.v cparser/validator/Automaton.vo cparser/validator/Alphabet.vo
cparser/validator/Grammar.vo cparser/validator/Grammar.glob cparser/validator/Grammar.v.beautified: cparser/validator/Grammar.v cparser/validator/Alphabet.vo cparser/validator/Tuples.vo
cparser/validator/Interpreter_safe.vo cparser/validator/Interpreter_safe.glob cparser/validator/Interpreter_safe.v.beautified: cparser/validator/Interpreter_safe.v cparser/validator/Alphabet.vo cparser/validator/Grammar.vo cparser/validator/Automaton.vo cparser/validator/Validator_safe.vo cparser/validator/Interpreter.vo
cparser/validator/Tuples.vo cparser/validator/Tuples.glob cparser/validator/Tuples.v.beautified: cparser/validator/Tuples.v
cparser/Cabs.vo cparser/Cabs.glob cparser/Cabs.v.beautified: cparser/Cabs.v
cparser/Parser.vo cparser/Parser.glob cparser/Parser.v.beautified: cparser/Parser.v cparser/Cabs.vo cparser/validator/Tuples.vo cparser/validator/Alphabet.vo cparser/validator/Grammar.vo cparser/validator/Automaton.vo cparser/validator/Main.vo
exportclight/Clightdefs.vo exportclight/Clightdefs.glob exportclight/Clightdefs.v.beautified: exportclight/Clightdefs.v lib/Integers.vo lib/Floats.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo
Language features:
- Support for C99 designated initializers. (ISO C99 section 6.7.8.)
- Traditional, pre-Standard function definitions are no longer supported, e.g.
int f(i) int i; { return i + 1; } // no longer supported
Use Standard form instead:
int f(int i) { return i + 1; }
Improvements in confidence:
- The parser is now formally verified against the ISO C99 grammar plus
CompCert's extensions. The verification proves that the parser
recognizes exactly the language specified by the grammar, and that
the grammar has no ambiguities. For more details, see the paper
"Validating LR(1) parsers" by Jacques-Henri Jourdan, François Pottier,
and Xavier Leroy, ESOP 2012, http://dx.doi.org/10.1007/978-3-642-28869-2_20
- More theorems proved about float<->integer conversions.
Optimizations:
......
......@@ -44,8 +44,7 @@ option) any later version:
backend/CMtypecheck.ml
backend/CMtypecheck.mli
all files in the cparser/ directory
(except those listed below which are under a BSD license)
all files in the cparser/ directory
all files in the exportclight/ directory
......@@ -69,15 +68,6 @@ The files contained in the runtime/ directory and its subdirectories
are Copyright 2013-2014 INRIA and distributed under the terms of the BSD
license, included below.
Finally, the following files are taken from the CIL library:
cparser/Cabs.ml
cparser/Lexer.mli
cparser/Lexer.mll
cparser/Parser.mly
These files are Copyright 2001-2005 George C. Necula, Scott McPeak,
Wes Weimer and Ben Liblit, and are distributed under the terms of the
BSD license, included below.
----------------------------------------------------------------------
INRIA Non-Commercial License Agreement for the CompCert verified compiler
......@@ -511,36 +501,6 @@ consider it more useful to permit linking proprietary applications with the
library. If this is what you want to do, use the GNU Lesser General
Public License instead of this License.
----------------------------------------------------------------------
BSD License
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:
1. Redistributions of source code must retain the above copyright notice,
this list of conditions and the following disclaimer.
2. Redistributions in binary form must reproduce the above copyright notice,
this list of conditions and the following disclaimer in the documentation
and/or other materials provided with the distribution.
3. The names of the contributors may not be used to endorse or promote
products derived from this software without specific prior written
permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
POSSIBILITY OF SUCH DAMAGE.
----------------------------------------------------------------------
GNU LESSER GENERAL PUBLIC LICENSE
......
......@@ -16,9 +16,9 @@
include Makefile.config
DIRS=lib common $(ARCH)/$(VARIANT) $(ARCH) backend cfrontend driver \
flocq/Core flocq/Prop flocq/Calc flocq/Appli exportclight
flocq/Core flocq/Prop flocq/Calc flocq/Appli exportclight cparser cparser/validator
RECDIRS=lib common backend cfrontend driver flocq exportclight
RECDIRS=lib common backend cfrontend driver flocq exportclight cparser
COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) -as compcert.$(d)) \
-I $(ARCH)/$(VARIANT) -as compcert.$(ARCH).$(VARIANT) \
......@@ -26,6 +26,7 @@ COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) -as compcert.$(d)) \
CAMLINCLUDES=$(patsubst %,-I %, $(DIRS)) -I extraction -I cparser
MENHIR=menhir
COQC="$(COQBIN)coqc" -q $(COQINCLUDES)
COQDEP="$(COQBIN)coqdep" $(COQINCLUDES)
COQDOC="$(COQBIN)coqdoc"
......@@ -109,13 +110,24 @@ CFRONTEND=Ctypes.v Cop.v Csyntax.v Csem.v Cstrategy.v Cexec.v \
Cshmgen.v Cshmgenproof.v \
Csharpminor.v Cminorgen.v Cminorgenproof.v
# LR(1) parser validator
PARSERVALIDATOR=Alphabet.v Interpreter_complete.v Interpreter.v \
Validator_complete.v Automaton.v Interpreter_correct.v Main.v \
Validator_safe.v Grammar.v Interpreter_safe.v Tuples.v
# Parser
PARSER=Cabs.v Parser.v
# Putting everything together (in driver/)
DRIVER=Compopts.v Compiler.v Complements.v
# All source files
FILES=$(LIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) $(FLOCQ)
FILES=$(LIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) $(FLOCQ) \
$(PARSERVALIDATOR) $(PARSER)
# Symbolic links vs. copy
......@@ -222,6 +234,9 @@ driver/Configuration.ml: Makefile.config VERSION
echo let version = "\"$$version\"") \
> driver/Configuration.ml
cparser/Parser.v: cparser/Parser.vy
$(MENHIR) --coq cparser/Parser.vy
depend: $(FILES) exportclight/Clightdefs.v
$(COQDEP) $^ \
| sed -e 's|$(ARCH)/$(VARIANT)/|$$(ARCH)/$$(VARIANT)/|g' \
......
true: use_menhir
<**/*.cmx>: debug
<**/*.native>: debug
<driver/Driver.*{byte,native}>: use_unix,use_str,use_Cparser
<exportclight/Clightgen.*{byte,native}>: use_unix,use_str,use_Cparser
<driver/Driver.*{byte,native}>: use_unix,use_str
<exportclight/Clightgen.*{byte,native}>: use_unix,use_str
<checklink/*.ml>: pkg_bitstring,warn_error_A
<checklink/Validator.*{byte,native}>: pkg_unix,pkg_str,pkg_bitstring,use_Cparser
<checklink/Validator.*{byte,native}>: pkg_unix,pkg_str,pkg_bitstring
......@@ -85,8 +85,6 @@ rule token = parse
| ">>l" { GREATERGREATERL }
| ">>lu" { GREATERGREATERLU }
| "if" { IF }
| "in" { IN }
| "inline" { INLINE }
| "int" { INT }
| "int16" { INT16 }
| "int16s" { INT16S }
......@@ -114,7 +112,6 @@ rule token = parse
| "<=lu" { LESSEQUALLU }
| "<<" { LESSLESS }
| "<<l" { LESSLESSL }
| "let" { LET }
| "long" { LONG }
| "longofint" { LONGOFINT }
| "longofintu" { LONGOFINTU }
......
......@@ -299,8 +299,6 @@ let mkmatch expr cases =
%token GREATERGREATERLU
%token <string> IDENT
%token IF
%token IN
%token INLINE
%token INT
%token INT16
%token INT16S
......@@ -329,7 +327,6 @@ let mkmatch expr cases =
%token LESSEQUALLU
%token LESSLESS
%token LESSLESSL
%token LET
%token LONG
%token <int64> LONGLIT
%token LONGOFINT
......@@ -378,10 +375,8 @@ let mkmatch expr cases =
%token WHILE
/* Precedences from low to high */
%left COMMA
%left p_let
%right EQUAL
%nonassoc p_THEN
%nonassoc ELSE
%left BAR BARL
%left CARET CARETL
%left AMPERSAND AMPERSANDL
......@@ -389,7 +384,7 @@ let mkmatch expr cases =
%left LESSLESS GREATERGREATER GREATERGREATERU LESSLESSL GREATERGREATERL GREATERGREATERLU
%left PLUS PLUSF PLUSL MINUS MINUSF MINUSL
%left STAR SLASH PERCENT STARF SLASHF SLASHU PERCENTU STARL SLASHL SLASHLU PERCENTL PERCENTLU
%nonassoc BANG TILDE TILDEL p_uminus ABSF INTOFFLOAT INTUOFFLOAT FLOATOFINT FLOATOFINTU INT8S INT8U INT16S INT16U FLOAT32 ALLOC INTOFLONG LONGOFINT LONGOFINTU LONGOFFLOAT LONGUOFFLOAT FLOATOFLONG FLOATOFLONGU
%nonassoc BANG TILDE TILDEL p_uminus ABSF INTOFFLOAT INTUOFFLOAT FLOATOFINT FLOATOFINTU INT8S INT8U INT16S INT16U FLOAT32 INTOFLONG LONGOFINT LONGOFINTU LONGOFFLOAT LONGUOFFLOAT FLOATOFLONG FLOATOFLONGU
%left LPAREN
/* Entry point */
......@@ -528,7 +523,7 @@ stmt:
| memory_chunk LBRACKET expr RBRACKET EQUAL expr SEMICOLON
{ mkstore $1 $3 $6 }
| IF LPAREN expr RPAREN stmts ELSE stmts { mkifthenelse $3 $5 $7 }
| IF LPAREN expr RPAREN stmts { mkifthenelse $3 $5 Sskip }
| IF LPAREN expr RPAREN stmts %prec p_THEN { mkifthenelse $3 $5 Sskip }
| LOOP stmts { Sloop($2) }
| LBRACELBRACE stmt_list RBRACERBRACE { Sblock($2) }
| EXIT SEMICOLON { Sexit O }
......@@ -672,7 +667,7 @@ expr_list:
;
expr_list_1:
expr %prec COMMA { $1 :: [] }
expr { $1 :: [] }
| expr COMMA expr_list_1 { $1 :: $3 }
;
......
......@@ -273,6 +273,9 @@ EOF
fi
# Avoid re-building cparser/Parser.v on the first run
touch cparser/Parser.v
# Summarize configuration
if test "$target" = "manual"; then
......
Bitfields.cmi: C.cmi
Builtins.cmi: Env.cmi C.cmi
C.cmi:
Cerrors.cmi:
Ceval.cmi: Env.cmi C.cmi
Cleanup.cmi: C.cmi
Cprint.cmi: C.cmi
Cutil.cmi: Env.cmi C.cmi
Elab.cmi: C.cmi
Env.cmi: C.cmi
GCC.cmi: Builtins.cmi
Lexer.cmi: Parser.cmi
Longlong.cmi: C.cmi
Machine.cmi:
PackedStructs.cmi: C.cmi
Parse.cmi: C.cmi
Parse_aux.cmi:
Parser.cmi: Cabs.cmo
Rename.cmi: C.cmi
StructReturn.cmi: C.cmi
Transform.cmi: Env.cmi C.cmi
Unblock.cmi: C.cmi
Bitfields.cmo: Transform.cmi Machine.cmi Env.cmi Cutil.cmi Cerrors.cmi C.cmi \
Bitfields.cmi
Bitfields.cmx: Transform.cmx Machine.cmx Env.cmx Cutil.cmx Cerrors.cmx C.cmi \
Bitfields.cmi
Builtins.cmo: Env.cmi Cutil.cmi C.cmi Builtins.cmi
Builtins.cmx: Env.cmx Cutil.cmx C.cmi Builtins.cmi
Cabs.cmo:
Cabs.cmx:
Cabshelper.cmo: Cabs.cmo
Cabshelper.cmx: Cabs.cmx
Cerrors.cmo: Cerrors.cmi
Cerrors.cmx: Cerrors.cmi
Ceval.cmo: Machine.cmi Cutil.cmi C.cmi Ceval.cmi
Ceval.cmx: Machine.cmx Cutil.cmx C.cmi Ceval.cmi
Cleanup.cmo: Cutil.cmi C.cmi Cleanup.cmi
Cleanup.cmx: Cutil.cmx C.cmi Cleanup.cmi
Cprint.cmo: C.cmi Cprint.cmi
Cprint.cmx: C.cmi Cprint.cmi
Cutil.cmo: Machine.cmi Env.cmi Cprint.cmi Cerrors.cmi C.cmi Cutil.cmi
Cutil.cmx: Machine.cmx Env.cmx Cprint.cmx Cerrors.cmx C.cmi Cutil.cmi
Elab.cmo: Parser.cmi Machine.cmi Lexer.cmi Env.cmi Cutil.cmi Cprint.cmi \
Cleanup.cmi Ceval.cmi Cerrors.cmi Cabshelper.cmo Cabs.cmo C.cmi \
Builtins.cmi Elab.cmi
Elab.cmx: Parser.cmx Machine.cmx Lexer.cmx Env.cmx Cutil.cmx Cprint.cmx \
Cleanup.cmx Ceval.cmx Cerrors.cmx Cabshelper.cmx Cabs.cmx C.cmi \
Builtins.cmx Elab.cmi
Env.cmo: C.cmi Env.cmi
Env.cmx: C.cmi Env.cmi
GCC.cmo: Cutil.cmi C.cmi Builtins.cmi GCC.cmi
GCC.cmx: Cutil.cmx C.cmi Builtins.cmx GCC.cmi
Lexer.cmo: Parser.cmi Parse_aux.cmi Cabshelper.cmo Cabs.cmo Lexer.cmi
Lexer.cmx: Parser.cmx Parse_aux.cmx Cabshelper.cmx Cabs.cmx Lexer.cmi
Longlong.cmo: Transform.cmi Env.cmi Cutil.cmi Cerrors.cmi C.cmi Longlong.cmi
Longlong.cmx: Transform.cmx Env.cmx Cutil.cmx Cerrors.cmx C.cmi Longlong.cmi
Machine.cmo: Machine.cmi
Machine.cmx: Machine.cmi
Main.cmo: Parse.cmi GCC.cmi Cprint.cmi Builtins.cmi
Main.cmx: Parse.cmx GCC.cmx Cprint.cmx Builtins.cmx
PackedStructs.cmo: Transform.cmi Machine.cmi Env.cmi Cutil.cmi Cprint.cmi \
Cerrors.cmi C.cmi Builtins.cmi PackedStructs.cmi
PackedStructs.cmx: Transform.cmx Machine.cmx Env.cmx Cutil.cmx Cprint.cmx \
Cerrors.cmx C.cmi Builtins.cmx PackedStructs.cmi
Parse.cmo: Unblock.cmi StructReturn.cmi Rename.cmi PackedStructs.cmi Elab.cmi \
Cerrors.cmi Bitfields.cmi Parse.cmi
Parse.cmx: Unblock.cmx StructReturn.cmx Rename.cmx PackedStructs.cmx Elab.cmx \
Cerrors.cmx Bitfields.cmx Parse.cmi
Parse_aux.cmo: Cerrors.cmi Cabshelper.cmo Parse_aux.cmi
Parse_aux.cmx: Cerrors.cmx Cabshelper.cmx Parse_aux.cmi
Parser.cmo: Parse_aux.cmi Cabshelper.cmo Cabs.cmo Parser.cmi
Parser.cmx: Parse_aux.cmx Cabshelper.cmx Cabs.cmx Parser.cmi
Rename.cmo: Cutil.cmi Cerrors.cmi C.cmi Builtins.cmi Rename.cmi
Rename.cmx: Cutil.cmx Cerrors.cmx C.cmi Builtins.cmx Rename.cmi
StructReturn.cmo: Transform.cmi Env.cmi Cutil.cmi C.cmi StructReturn.cmi
StructReturn.cmx: Transform.cmx Env.cmx Cutil.cmx C.cmi StructReturn.cmi
Transform.cmo: Env.cmi Cutil.cmi C.cmi Builtins.cmi Transform.cmi
Transform.cmx: Env.cmx Cutil.cmx C.cmi Builtins.cmx Transform.cmi
Unblock.cmo: Transform.cmi Cutil.cmi Cerrors.cmi C.cmi Unblock.cmi
Unblock.cmx: Transform.cmx Cutil.cmx Cerrors.cmx C.cmi Unblock.cmi
(*
*
* Copyright (c) 2001-2002,
* George C. Necula <necula@cs.berkeley.edu>
* Scott McPeak <smcpeak@cs.berkeley.edu>
* Wes Weimer <weimer@cs.berkeley.edu>
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* 1. Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
* 2. Redistributions in binary form must reproduce the above copyright
* notice, this list of conditions and the following disclaimer in the
* documentation and/or other materials provided with the distribution.
*
* 3. The names of the contributors may not be used to endorse or promote
* products derived from this software without specific prior written
* permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
* IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
* OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
* EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
* PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
* PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
* LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
* NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
* SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*
*)
(** This file was originally part of Hugues Casee's frontc 2.0, and has been
* extensively changed since.
**
** 1.0 3.22.99 Hugues Cassé First version.
** 2.0 George Necula 12/12/00: Many extensions
**)
(*
** Types
*)
type cabsloc = {
lineno : int;
filename: string;
byteno: int;
ident : int;
}
type typeSpecifier = (* Merge all specifiers into one type *)
Tvoid (* Type specifier ISO 6.7.2 *)
| Tchar
| Tshort
| Tint
| Tlong
| Tint64
| T_Bool
| Tfloat
| Tdouble
| Tsigned
| Tunsigned
| Tnamed of string
(* each of the following three kinds of specifiers contains a field
* or item list iff it corresponds to a definition (as opposed to
* a forward declaration or simple reference to the type); they
* also have a list of __attribute__s that appeared between the
* keyword and the type name (definitions only) *)
| Tstruct of string * field_group list option * attribute list
| Tunion of string * field_group list option * attribute list
| Tenum of string * enum_item list option * attribute list
| TtypeofE of expression (* GCC __typeof__ *)
| TtypeofT of specifier * decl_type (* GCC __typeof__ *)
and storage =
NO_STORAGE | AUTO | STATIC | EXTERN | REGISTER
and funspec =
INLINE | VIRTUAL | EXPLICIT
and cvspec =
CV_CONST | CV_VOLATILE | CV_RESTRICT
(* Type specifier elements. These appear at the start of a declaration *)
(* Everywhere they appear in this file, they appear as a 'spec_elem list', *)
(* which is not interpreted by cabs -- rather, this "word soup" is passed *)
(* on to the compiler. Thus, we can represent e.g. 'int long float x' even *)
(* though the compiler will of course choke. *)
and spec_elem =
SpecTypedef
| SpecCV of cvspec (* const/volatile *)
| SpecAttr of attribute (* __attribute__ *)
| SpecStorage of storage
| SpecInline
| SpecType of typeSpecifier
(* decided to go ahead and replace 'spec_elem list' with specifier *)
and specifier = spec_elem list
(* Declarator type. They modify the base type given in the specifier. Keep
* them in the order as they are printed (this means that the top level
* constructor for ARRAY and PTR is the inner-level in the meaning of the
* declared type) *)
and decl_type =
| JUSTBASE (* Prints the declared name *)
| PARENTYPE of attribute list * decl_type * attribute list
(* Prints "(attrs1 decl attrs2)".
* attrs2 are attributes of the
* declared identifier and it is as
* if they appeared at the very end
* of the declarator. attrs1 can
* contain attributes for the
* identifier or attributes for the
* enclosing type. *)
| ARRAY of decl_type * attribute list * expression
(* Prints "decl [ attrs exp ]".
* decl is never a PTR. *)
| PTR of attribute list * decl_type (* Prints "* attrs decl" *)
| PROTO of decl_type * single_name list * bool
(* Prints "decl (args[, ...])".
* decl is never a PTR.*)
(* The base type and the storage are common to all names. Each name might
* contain type or storage modifiers *)
(* e.g.: int x, y; *)
and name_group = specifier * name list
(* The optional expression is the bitfield *)
and field_group = specifier * (name * expression option) list
(* like name_group, except the declared variables are allowed to have initializers *)
(* e.g.: int x=1, y=2; *)
and init_name_group = specifier * init_name list
(* The decl_type is in the order in which they are printed. Only the name of
* the declared identifier is pulled out. The attributes are those that are
* printed after the declarator *)
(* e.g: in "int *x", "*x" is the declarator; "x" will be pulled out as *)
(* the string, and decl_type will be PTR([], JUSTBASE) *)
and name = string * decl_type * attribute list * cabsloc
(* A variable declarator ("name") with an initializer *)
and init_name = name * init_expression
(* Single names are for declarations that cannot come in groups, like
* function parameters and functions *)
and single_name = specifier * name
and enum_item = string * expression * cabsloc
(*
** Declaration definition (at toplevel)
*)
and definition =
FUNDEF of single_name * block * cabsloc * cabsloc
| DECDEF of init_name_group * cabsloc (* global variable(s), or function prototype *)
| TYPEDEF of name_group * cabsloc
| ONLYTYPEDEF of specifier * cabsloc
| GLOBASM of string * cabsloc
| PRAGMA of string * cabsloc
| LINKAGE of string * cabsloc * definition list (* extern "C" { ... } *)
(* the string is a file name, and then the list of toplevel forms *)
and file = string * definition list
(*
** statements
*)
(* A block contains a list of local label declarations ( GCC's ({ __label__
* l1, l2; ... }) ) , a list of definitions and a list of statements *)
and block =
{ blabels: string list;
battrs: attribute list;
bstmts: statement list
}
(* GCC asm directives have lots of extra information to guide the optimizer *)
and asm_details =
{ aoutputs: (string option * string * expression) list; (* optional name, constraints and expressions for outputs *)
ainputs: (string option * string * expression) list; (* optional name, constraints and expressions for inputs *)
aclobbers: string list (* clobbered registers *)
}
and statement =
NOP of cabsloc
| COMPUTATION of expression * cabsloc
| BLOCK of block * cabsloc
(* | SEQUENCE of statement * statement * cabsloc *)
| IF of expression * statement * statement * cabsloc
| WHILE of expression * statement * cabsloc
| DOWHILE of expression * statement * cabsloc
| FOR of for_clause * expression * expression * statement * cabsloc
| BREAK of cabsloc
| CONTINUE of cabsloc
| RETURN of expression * cabsloc
| SWITCH of expression * statement * cabsloc
| CASE of expression * statement * cabsloc
| CASERANGE of expression * expression * statement * cabsloc
| DEFAULT of statement * cabsloc
| LABEL of string * statement * cabsloc
| GOTO of string * cabsloc
| COMPGOTO of expression * cabsloc (* GCC's "goto *exp" *)
| DEFINITION of definition (*definition or declaration of a variable or type*)
| ASM of attribute list * (* typically only volatile and const *)
string list * (* template *)
asm_details option * (* extra details to guide GCC's optimizer *)
cabsloc
(** MS SEH *)
| TRY_EXCEPT of block * expression * block * cabsloc
| TRY_FINALLY of block * block * cabsloc
and for_clause =
FC_EXP of expression
| FC_DECL of definition
(*
** Expressions
*)
and binary_operator =
ADD | SUB | MUL | DIV | MOD
| AND | OR
| BAND | BOR | XOR | SHL | SHR
| EQ | NE | LT | GT | LE | GE
| ASSIGN
| ADD_ASSIGN | SUB_ASSIGN | MUL_ASSIGN | DIV_ASSIGN | MOD_ASSIGN
| BAND_ASSIGN | BOR_ASSIGN | XOR_ASSIGN | SHL_ASSIGN | SHR_ASSIGN
and unary_operator =
MINUS | PLUS | NOT | BNOT | MEMOF | ADDROF
| PREINCR | PREDECR | POSINCR | POSDECR
and expression =
NOTHING
| UNARY of unary_operator * expression
| LABELADDR of string (* GCC's && Label *)
| BINARY of binary_operator * expression * expression
| QUESTION of expression * expression * expression
(* A CAST can actually be a constructor expression *)
| CAST of (specifier * decl_type) * init_expression
(* There is a special form of CALL in which the function called is
__builtin_va_arg and the second argument is sizeof(T). This
should be printed as just T *)
| CALL of expression * expression list
| COMMA of expression list
| CONSTANT of constant
| PAREN of expression
| VARIABLE of string
| EXPR_SIZEOF of expression
| TYPE_SIZEOF of specifier * decl_type
| EXPR_ALIGNOF of expression
| TYPE_ALIGNOF of specifier * decl_type
| INDEX of expression * expression
| MEMBEROF of expression * string
| MEMBEROFPTR of expression * string
| GNU_BODY of block
and floatInfo = {
isHex_FI:bool;
integer_FI:string option;
fraction_FI:string option;
exponent_FI:string option;
suffix_FI:char option;
}
and constant =
| CONST_INT of string (* the textual representation *)
| CONST_FLOAT of floatInfo
| CONST_CHAR of int64 list
| CONST_WCHAR of int64 list
| CONST_STRING of string
| CONST_WSTRING of int64 list
(* ww: wstrings are stored as an int64 list at this point because
* we might need to feed the wide characters piece-wise into an
* array initializer (e.g., wchar_t foo[] = L"E\xabcd";). If that
* doesn't happen we will convert it to an (escaped) string before
* passing it to Cil. *)
and init_expression =
| NO_INIT
| SINGLE_INIT of expression
| COMPOUND_INIT of (initwhat * init_expression) list
and initwhat =
NEXT_INIT
| INFIELD_INIT of string * initwhat
| ATINDEX_INIT of expression * initwhat
| ATINDEXRANGE_INIT of expression * expression
(* Each attribute has a name and some
* optional arguments *)
and attribute = string * expression list