From f1d236b83003eda71e12840732d159fd23b1b771 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 29 Apr 2014 13:58:18 +0000 Subject: 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 --- cparser/Elab.ml | 681 +++++++++++++++++++++++++++++++------------------------- 1 file changed, 375 insertions(+), 306 deletions(-) (limited to 'cparser/Elab.ml') diff --git a/cparser/Elab.ml b/cparser/Elab.ml index ecc97a7..780cf09 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -18,7 +18,6 @@ (* Numbered references are to sections of the ISO C99 standard *) open Format -open Cerrors open Machine open Cabs open Cabshelper @@ -54,6 +53,7 @@ let elab_loc l = (l.filename, l.lineno) let top_declarations = ref ([] : globdecl list) let emit_elab loc td = + let loc = elab_loc loc in top_declarations := { gdesc = td; gloc = loc } :: !top_declarations let reset() = top_declarations := [] @@ -64,10 +64,6 @@ let elaborated_program () = (* Reverse it and eliminate unreferenced declarations *) Cleanup.program p -(* Location stuff *) - -let loc_of_name (_, _, _, loc) = loc - (* Monadic map for functions env -> 'a -> 'b * env *) let rec mmap f env = function @@ -91,8 +87,8 @@ let redef fn env arg = let elab_expr_f : (cabsloc -> Env.t -> Cabs.expression -> C.exp) ref = ref (fun _ _ _ -> assert false) -let elab_funbody_f : (cabsloc -> C.typ -> Env.t -> Cabs.block -> C.stmt) ref - = ref (fun _ _ _ _ -> assert false) +let elab_funbody_f : (C.typ -> Env.t -> statement -> C.stmt) ref + = ref (fun _ _ _ -> assert false) (** * Elaboration of constants - C99 section 6.4.4 *) @@ -199,8 +195,8 @@ let elab_int_constant loc s0 = let elab_float_constant loc f = let ty = match f.suffix_FI with - | Some 'l' | Some 'L' -> FLongDouble - | Some 'f' | Some 'F' -> FFloat + | Some ("l"|"L") -> FLongDouble + | Some ("f"|"F") -> FFloat | None -> FDouble | _ -> assert false (* The lexer should not accept anything else. *) in @@ -212,27 +208,106 @@ let elab_float_constant loc f = in (v, ty) -let elab_char_constant loc sz cl = +let parse_next_char s pos loc = + if s.[pos] = '\\' then + match s.[pos+1] with + | '\'' -> (Int64.of_int (Char.code '\''), pos+2) + | '\"' -> (Int64.of_int (Char.code '\"'), pos+2) + | '?' -> (Int64.of_int (Char.code '?'), pos+2) + | '\\' -> (Int64.of_int (Char.code '\\'), pos+2) + | 'a' -> (7L, pos+2) + | 'b' -> (Int64.of_int (Char.code '\b'), pos+2) + | 'f' -> (12L, pos+2) + | 'n' -> (Int64.of_int (Char.code '\n'), pos+2) + | 'r' -> (Int64.of_int (Char.code '\r'), pos+2) + | 't' -> (Int64.of_int (Char.code '\t'), pos+2) + | 'v' -> (11L, pos+2) + | '0'..'9' -> + let next = ref (pos+1) in + while !next < String.length s && s.[!next] >= '0' && s.[!next] <= '9' do + incr next + done; + (parse_int 8 (String.sub s (pos+1) (!next-pos-1)), !next) + | 'x' -> + let next = ref (pos+2) in + while !next < String.length s && ( + (s.[!next] >= '0' && s.[!next] <= '9') || + (s.[!next] >= 'a' && s.[!next] <= 'f') || + (s.[!next] >= 'A' && s.[!next] <= 'F')) + do + incr next + done; + (begin + try parse_int 16 (String.uppercase (String.sub s (pos+2) (!next-pos-2))) + with Overflow -> + error loc "overflow in hexadecimal escape sequence"; 0L end, + !next) + | 'u' -> + (parse_int 16 (String.uppercase (String.sub s (pos+2) 4)), pos+6) + | 'U' -> + (parse_int 16 (String.uppercase (String.sub s (pos+2) 8)), pos+10) + | _ -> assert false + else (Int64.of_int (Char.code s.[pos]), pos+1) + +let elab_char_constant loc s = + let (s, sz) = + match s.[0], s.[1] with + | 'L', '\'' -> chop_first s 2, !config.sizeof_wchar + | '\'', _ -> chop_first s 1, 1 + | _ -> assert false + in + assert (s.[String.length s-1] = '\''); + let s = chop_last s 1 in let nbits = 8 * sz in (* Treat multi-char constants as a number in base 2^nbits *) let max_digit = Int64.shift_left 1L nbits in let max_val = Int64.shift_left 1L (64 - nbits) in - let v = - List.fold_left - (fun acc d -> - if acc >= max_val then - error loc "character constant overflows"; - if d >= max_digit then - warning loc "escape sequence out of range"; - Int64.add (Int64.shift_left acc nbits) d) - 0L cl in + let rec parse pos accu nchar = + if accu >= max_val then + error loc "character constant overflows"; + if pos = String.length s then accu, nchar + else + let (c, pos) = parse_next_char s pos loc in + if c >= max_digit then + warning loc "escape sequence out of range"; + let accu = Int64.add (Int64.shift_left accu nbits) c in + parse pos accu (nchar+1) + in + let v, nchar = parse 0 0L 0 in if not (integer_representable v IInt) then error loc "character constant cannot be represented at type 'int'"; (* C99 6.4.4.4 item 10: single character -> represent at type char *) - if List.length cl = 1 + if nchar = 1 then Ceval.normalize_int v IChar else v +let elab_string_literal loc s = + let (wide, pos) = if s.[0] = 'L' then ref true, 2 else ref false, 1 in + assert (s.[pos-1] = '\"'); + let rec parse pos accu = + if s.[pos] = '\"' then + if pos = String.length s - 1 then accu + else + let pos = if s.[pos+1] = 'L' then (wide := true; pos+3) else pos+2 in + assert(s.[pos-1] = '\"'); + parse pos accu + else + let (char, pos) = parse_next_char s pos loc in + parse pos (char::accu) + in + let l = List.rev (parse pos []) in + let nbbits = if !wide then 8 * !config.sizeof_wchar else 8 in + List.iter (fun c -> + if c < 0L || c >= Int64.shift_left 1L nbbits then + error loc "character overflows") l; + if !wide then + CWStr l + else + let res = String.create (List.length l) in + List.iteri (fun i c -> + res.[i] <- Char.chr (Int64.to_int c)) l; + CStr res + let elab_constant loc = function | CONST_INT s -> let (v, ik) = elab_int_constant loc s in @@ -240,12 +315,10 @@ let elab_constant loc = function | CONST_FLOAT f -> let (v, fk) = elab_float_constant loc f in CFloat(v, fk) - | CONST_CHAR cl -> - CInt(elab_char_constant loc 1 cl, IInt, "") - | CONST_WCHAR cl -> - CInt(elab_char_constant loc !config.sizeof_wchar cl, IInt, "") - | CONST_STRING s -> CStr s - | CONST_WSTRING s -> CWStr s + | CONST_CHAR s -> + CInt(elab_char_constant loc s, IInt, "") + | CONST_STRING s -> + elab_string_literal loc s (** * Elaboration of type expressions, type specifiers, name declarations *) @@ -271,17 +344,23 @@ let elab_attr_arg loc env a = | Some(CStr s) -> AString s | _ -> raise Wrong_attr_arg +let elab_gcc_attr_word = function + | GCC_ATTR_IDENT s -> s + | GCC_ATTR_CONST -> "const" + | GCC_ATTR_PACKED -> "__packed__" + let elab_gcc_attr loc env = function - | VARIABLE v -> + | GCC_ATTR_EMPTY -> [] + | GCC_ATTR_NOARGS w -> + let v = elab_gcc_attr_word w in [Attr(v, [])] - | CALL(VARIABLE v, args) -> + | GCC_ATTR_ARGS (w, args) -> + let v = elab_gcc_attr_word w in begin try [Attr(v, List.map (elab_attr_arg loc env) args)] with Wrong_attr_arg -> warning loc "cannot parse '%s' attribute, ignored" v; [] end - | _ -> - warning loc "ill-formed attribute, ignored"; [] let is_power_of_two n = n > 0L && Int64.(logand n (pred n)) = 0L @@ -294,25 +373,25 @@ let extract_alignas loc a = end | _ -> a -let elab_attribute loc env = function - | ("const", []) -> [AConst] - | ("restrict", []) -> [ARestrict] - | ("volatile", []) -> [AVolatile] - | ("_Alignas", [a]) -> +let elab_attribute env = function + | GCC_ATTR (l, loc) -> + List.fold_left add_attributes [] + (List.map (fun attr -> [attr]) + (List.map (extract_alignas loc) + (List.flatten + (List.map (elab_gcc_attr loc env) l)))) + | PACKED_ATTR (args, loc) -> + [Attr("__packed__", List.map (elab_attr_arg loc env) args)] + | ALIGNAS_ATTR ([a], loc) -> begin match elab_attr_arg loc env a with | AInt n when is_power_of_two n -> [AAlignas (Int64.to_int n)] | _ -> warning loc "bad _Alignas value, ignored"; [] end - | (("__attribute" | "__attribute__"), l) -> - List.map (extract_alignas loc) - (List.flatten (List.map (elab_gcc_attr loc env) l)) - | ("__packed__", args) -> - [Attr("__packed__", List.map (elab_attr_arg loc env) args)] - | ("__asm__", _) -> [] (* MacOS X noise *) - | (name, _) -> warning loc "`%s' annotation ignored" name; [] + | ALIGNAS_ATTR (_, loc) -> + warning loc "_Alignas takes exactly one parameter, ignored"; [] -let elab_attributes loc env al = - List.fold_left add_attributes [] (List.map (elab_attribute loc env) al) +let elab_attributes env al = + List.fold_left add_attributes [] (List.map (elab_attribute env) al) (* Auxiliary for typespec elaboration *) @@ -324,7 +403,6 @@ let typespec_rank = function (* Don't change this *) | Cabs.Tshort -> 4 | Cabs.Tlong -> 5 | Cabs.Tint -> 6 - | Cabs.Tint64 -> 7 | Cabs.Tfloat -> 8 | Cabs.Tdouble -> 9 | Cabs.T_Bool -> 10 @@ -332,8 +410,8 @@ let typespec_rank = function (* Don't change this *) let typespec_order t1 t2 = compare (typespec_rank t1) (typespec_rank t2) -(* Elaboration of a type specifier. Returns 4-tuple: - (storage class, "inline" flag, elaborated type, new env) +(* Elaboration of a type specifier. Returns 5-tuple: + (storage class, "inline" flag, "typedef" flag, elaborated type, new env) Optional argument "only" is true if this is a standalone struct or union declaration, without variable names. C99 section 6.7.2. @@ -347,35 +425,31 @@ let rec elab_specifier ?(only = false) loc env specifier = let sto = ref Storage_default and inline = ref false and attr = ref [] - and tyspecs = ref [] in + and tyspecs = ref [] + and typedef = ref false in let do_specifier = function - | SpecTypedef -> () | SpecCV cv -> - let a = - match cv with - | CV_CONST -> AConst - | CV_VOLATILE -> AVolatile - | CV_RESTRICT -> ARestrict in - attr := add_attributes [a] !attr - | SpecAttr a -> - attr := add_attributes (elab_attributes loc env [a]) !attr + attr := add_attributes (elab_cvspec env cv) !attr | SpecStorage st -> - if !sto <> Storage_default then + if !sto <> Storage_default && st <> TYPEDEF then error loc "multiple storage specifiers"; begin match st with - | NO_STORAGE -> () | AUTO -> () | STATIC -> sto := Storage_static | EXTERN -> sto := Storage_extern | REGISTER -> sto := Storage_register + | TYPEDEF -> + if !typedef then + error loc "multiple uses of 'typedef'"; + typedef := true end | SpecInline -> inline := true | SpecType tys -> tyspecs := tys :: !tyspecs in List.iter do_specifier specifier; - let simple ty = (!sto, !inline, add_attributes_type !attr ty, env) in + let simple ty = (!sto, !inline, !typedef, add_attributes_type !attr ty, env) in (* As done in CIL, partition !attr into type-related attributes, which are returned, and other attributes, which are left in !attr. @@ -430,11 +504,6 @@ let rec elab_specifier ?(only = false) loc env specifier = | [Cabs.Tunsigned; Cabs.Tlong; Cabs.Tlong] -> simple (TInt(IULongLong, [])) | [Cabs.Tunsigned; Cabs.Tlong; Cabs.Tlong; Cabs.Tint] -> simple (TInt(IULongLong, [])) - (* int64 is a MSVC extension *) - | [Cabs.Tint64] -> simple (TInt(ILongLong, [])) - | [Cabs.Tsigned; Cabs.Tint64] -> simple (TInt(ILongLong, [])) - | [Cabs.Tunsigned; Cabs.Tint64] -> simple (TInt(IULongLong, [])) - | [Cabs.Tfloat] -> simple (TFloat(FFloat, [])) | [Cabs.Tdouble] -> simple (TFloat(FDouble, [])) @@ -446,52 +515,51 @@ let rec elab_specifier ?(only = false) loc env specifier = let (id', info) = wrap Env.lookup_typedef loc env id in simple (TNamed(id', [])) - | [Cabs.Tstruct(id, optmembers, a)] -> + | [Cabs.Tstruct_union(STRUCT, id, optmembers, a)] -> let a' = - add_attributes (get_type_attrs()) (elab_attributes loc env a) in + add_attributes (get_type_attrs()) (elab_attributes env a) in let (id', env') = elab_struct_or_union only Struct loc id optmembers a' env in - (!sto, !inline, TStruct(id', !attr), env') + (!sto, !inline, !typedef, TStruct(id', !attr), env') - | [Cabs.Tunion(id, optmembers, a)] -> + | [Cabs.Tstruct_union(UNION, id, optmembers, a)] -> let a' = - add_attributes (get_type_attrs()) (elab_attributes loc env a) in + add_attributes (get_type_attrs()) (elab_attributes env a) in let (id', env') = elab_struct_or_union only Union loc id optmembers a' env in - (!sto, !inline, TUnion(id', !attr), env') + (!sto, !inline, !typedef, TUnion(id', !attr), env') | [Cabs.Tenum(id, optmembers, a)] -> let a' = - add_attributes (get_type_attrs()) (elab_attributes loc env a) in - let (id', env') = + add_attributes (get_type_attrs()) (elab_attributes env a) in + let (id', env') = elab_enum loc id optmembers a' env in - (!sto, !inline, TEnum(id', !attr), env') - - | [Cabs.TtypeofE _] -> - fatal_error loc "GCC __typeof__ not supported" - | [Cabs.TtypeofT _] -> - fatal_error loc "GCC __typeof__ not supported" + (!sto, !inline, !typedef, TEnum(id', !attr), env') (* Specifier doesn't make sense *) | _ -> fatal_error loc "illegal combination of type specifiers" +(* Elaboration of a type qualifier. *) + +and elab_cvspec env = function + | CV_CONST -> [AConst] + | CV_VOLATILE -> [AVolatile] + | CV_RESTRICT -> [ARestrict] + | CV_ATTR attr -> elab_attribute env attr + (* Elaboration of a type declarator. C99 section 6.7.5. *) and elab_type_declarator loc env ty = function | Cabs.JUSTBASE -> (ty, env) - | Cabs.PARENTYPE(attr1, d, attr2) -> - (* XXX ignoring the distinction between attrs after and before *) - let a = elab_attributes loc env (attr1 @ attr2) in - elab_type_declarator loc env (add_attributes_type a ty) d - | Cabs.ARRAY(d, attr, sz) -> - let a = elab_attributes loc env attr in + | Cabs.ARRAY(d, cv_specs, sz) -> + let a = List.fold_left add_attributes [] (List.map (elab_cvspec env) cv_specs) in let sz' = match sz with - | Cabs.NOTHING -> + | None -> None - | _ -> + | Some sz -> match Ceval.integer_expr env (!elab_expr_f loc env sz) with | Some n -> if n < 0L then error loc "array size is negative"; @@ -501,10 +569,10 @@ and elab_type_declarator loc env ty = function error loc "array size is not a compile-time constant"; Some 1L in (* produces better error messages later *) elab_type_declarator loc env (TArray(ty, sz', a)) d - | Cabs.PTR(attr, d) -> - let a = elab_attributes loc env attr in - elab_type_declarator loc env (TPtr(ty, a)) d - | Cabs.PROTO(d, params, vararg) -> + | Cabs.PTR(cv_specs, d) -> + let a = List.fold_left add_attributes [] (List.map (elab_cvspec env) cv_specs) in + elab_type_declarator loc env (TPtr(ty, a)) d + | Cabs.PROTO(d, (params, vararg)) -> begin match unroll env ty with | TArray _ | TFun _ -> error loc "illegal function return type@ %a" Cprint.typ ty @@ -529,13 +597,20 @@ and elab_parameters env params = (* Elaboration of a function parameter *) -and elab_parameter env (spec, name) = - let (id, sto, inl, ty, env1) = elab_name env spec name in +and elab_parameter env (PARAM (spec, id, decl, attr, loc)) = + let (sto, inl, tydef, bty, env1) = elab_specifier loc env spec in + if tydef then + error loc "'typedef' used in function parameter"; + let (ty, env2) = elab_type_declarator loc env1 bty decl in + let ty = add_attributes_type (elab_attributes env attr) ty in if sto <> Storage_default && sto <> Storage_register then - error (loc_of_name name) + error loc "'extern' or 'static' storage not supported for function parameter"; + if inl then + error loc "'inline' is forbidden here"; + let id = match id with None -> "" | Some id -> id in if id <> "" && redef Env.lookup_ident env id <> None then - error (loc_of_name name) "redefinition of parameter '%s'" id; + error loc "redefinition of parameter '%s'" id; (* replace array and function types by pointer types *) let ty1 = argument_conversion env1 ty in let (id', env2) = Env.enter_ident env1 id sto ty1 in @@ -543,45 +618,61 @@ and elab_parameter env (spec, name) = (* Elaboration of a (specifier, Cabs "name") pair *) -and elab_name env spec (id, decl, attr, loc) = - let (sto, inl, bty, env') = elab_specifier loc env spec in +and elab_name env spec (Name (id, decl, attr, loc)) = + let (sto, inl, tydef, bty, env') = elab_specifier loc env spec in + if tydef then + error loc "'typedef' is forbidden here"; let (ty, env'') = elab_type_declarator loc env' bty decl in - let a = elab_attributes loc env attr in + let a = elab_attributes env attr in (id, sto, inl, add_attributes_type a ty, env'') (* Elaboration of a name group. C99 section 6.7.6 *) and elab_name_group loc env (spec, namelist) = - let (sto, inl, bty, env') = + let (sto, inl, tydef, bty, env') = elab_specifier loc env spec in - let elab_one_name env (id, decl, attr, loc) = + if tydef then + error loc "'typedef' is forbidden here"; + if inl then + error loc "'inline' is forbidden here"; + let elab_one_name env (Name (id, decl, attr, loc)) = let (ty, env1) = elab_type_declarator loc env bty decl in - let a = elab_attributes loc env attr in - ((id, sto, add_attributes_type a ty), env1) in - mmap elab_one_name env' namelist + let a = elab_attributes env attr in + ((id, add_attributes_type a ty), env1) in + (mmap elab_one_name env' namelist, sto) (* Elaboration of an init-name group *) and elab_init_name_group loc env (spec, namelist) = - let (sto, inl, bty, env') = - elab_specifier loc env spec in - let elab_one_name env ((id, decl, attr, loc), init) = + let (sto, inl, tydef, bty, env') = + elab_specifier ~only:(namelist=[]) loc env spec in + if inl then + error loc "'inline' is forbidden here"; + let elab_one_name env (Init_name (Name (id, decl, attr, loc), init)) = let (ty, env1) = elab_type_declarator loc env bty decl in - let a = elab_attributes loc env attr in - ((id, sto, add_attributes_type a ty, init), env1) in - mmap elab_one_name env' namelist + let a = elab_attributes env attr in + ((id, add_attributes_type a ty, init), env1) in + (mmap elab_one_name env' namelist, sto, tydef) (* Elaboration of a field group *) -and elab_field_group loc env (spec, fieldlist) = - let (names, env') = +and elab_field_group env (Field_group (spec, fieldlist, loc)) = + let fieldlist = List.map ( + function + | (None, x) -> (Name ("", JUSTBASE, [], cabslu), x) + | (Some n, x) -> (n, x)) + fieldlist + in + + let ((names, env'), sto) = elab_name_group loc env (spec, List.map fst fieldlist) in - let elab_bitfield ((_, _, _, loc), optbitsize) (id, sto, ty) = - if sto <> Storage_default then - error loc "member '%s' has non-default storage" id; + if sto <> Storage_default then + error loc "non-default storage in struct or union"; + + let elab_bitfield (Name (_, _, _, loc), optbitsize) (id, ty) = let optbitsize' = match optbitsize with | None -> None @@ -623,7 +714,7 @@ and elab_field_group loc env (spec, fieldlist) = (* Elaboration of a struct or union. C99 section 6.7.2.1 *) and elab_struct_or_union_info kind loc env members attrs = - let (m, env') = mmap (elab_field_group loc) env members in + let (m, env') = mmap elab_field_group env members in let m = List.flatten m in (* Check for incomplete types *) let rec check_incomplete = function @@ -644,8 +735,12 @@ and elab_struct_or_union only kind loc tag optmembers attrs env = let warn_attrs () = if attrs <> [] then warning loc "attributes over struct/union ignored in this context" in - let optbinding = - if tag = "" then None else Env.lookup_composite env tag in + let optbinding, tag = + match tag with + | None -> None, "" + | Some s -> + Env.lookup_composite env s, s + in match optbinding, optmembers with | Some(tag', ci), None when (not only) || Env.in_current_scope env tag' -> @@ -663,8 +758,7 @@ and elab_struct_or_union only kind loc tag optmembers attrs env = (* finishing the definition of an incomplete struct or union *) let (ci', env') = elab_struct_or_union_info kind loc env members attrs in (* Emit a global definition for it *) - emit_elab (elab_loc loc) - (Gcompositedef(kind, tag', attrs, ci'.ci_members)); + emit_elab loc (Gcompositedef(kind, tag', attrs, ci'.ci_members)); (* Replace infos but keep same ident *) (tag', Env.add_composite env' tag' ci') | Some(tag', {ci_sizeof = Some _}), Some _ @@ -679,8 +773,7 @@ and elab_struct_or_union only kind loc tag optmembers attrs env = (* enter it with a new name *) let (tag', env') = Env.enter_composite env tag ci in (* emit it *) - emit_elab (elab_loc loc) - (Gcompositedecl(kind, tag', attrs)); + emit_elab loc (Gcompositedecl(kind, tag', attrs)); (tag', env') | _, Some members -> (* definition of a complete struct or union *) @@ -688,25 +781,23 @@ and elab_struct_or_union only kind loc tag optmembers attrs env = (* enter it, incomplete, with a new name *) let (tag', env') = Env.enter_composite env tag ci1 in (* emit a declaration so that inner structs and unions can refer to it *) - emit_elab (elab_loc loc) - (Gcompositedecl(kind, tag', attrs)); + emit_elab loc (Gcompositedecl(kind, tag', attrs)); (* elaborate the members *) let (ci2, env'') = elab_struct_or_union_info kind loc env' members attrs in (* emit a definition *) - emit_elab (elab_loc loc) - (Gcompositedef(kind, tag', attrs, ci2.ci_members)); + emit_elab loc (Gcompositedef(kind, tag', attrs, ci2.ci_members)); (* Replace infos but keep same ident *) (tag', Env.add_composite env'' tag' ci2) (* Elaboration of an enum item. C99 section 6.7.2.2 *) -and elab_enum_item env (s, exp, loc) nextval = +and elab_enum_item env ((s, exp), loc) nextval = let (v, exp') = match exp with - | NOTHING -> + | None -> (nextval, None) - | _ -> + | Some exp -> let exp' = !elab_expr_f loc env exp in match Ceval.integer_expr env exp' with | Some n -> (n, Some exp') @@ -725,6 +816,7 @@ and elab_enum_item env (s, exp, loc) nextval = (* Elaboration of an enumeration declaration. C99 section 6.7.2.2 *) and elab_enum loc tag optmembers attrs env = + let tag = match tag with None -> "" | Some s -> s in match optmembers with | None -> let (tag', info) = wrap Env.lookup_enum loc env tag in (tag', env) @@ -739,16 +831,16 @@ and elab_enum loc tag optmembers attrs env = let (dcls, env') = elab_members env 0L members in let info = { ei_members = dcls; ei_attr = attrs } in let (tag', env'') = Env.enter_enum env' tag info in - emit_elab (elab_loc loc) (Genumdef(tag', attrs, dcls)); + emit_elab loc (Genumdef(tag', attrs, dcls)); (tag', env'') (* Elaboration of a naked type, e.g. in a cast *) let elab_type loc env spec decl = - let (sto, inl, bty, env') = elab_specifier loc env spec in + let (sto, inl, tydef, bty, env') = elab_specifier loc env spec in let (ty, env'') = elab_type_declarator loc env' bty decl in - if sto <> Storage_default || inl then - error loc "'extern', 'static', 'register' and 'inline' are meaningless in cast"; + if sto <> Storage_default || inl || tydef then + error loc "'typedef', 'extern', 'static', 'register' and 'inline' are meaningless in cast"; ty @@ -762,9 +854,6 @@ let elab_expr loc env a = let rec elab = function - | NOTHING -> - error "empty expression" - (* 6.5.1 Primary expressions *) | VARIABLE s -> @@ -779,9 +868,6 @@ let elab_expr loc env a = let cst' = elab_constant loc cst in { edesc = EConst cst'; etyp = type_of_constant cst' } - | PAREN e -> - elab e - (* 6.5.2 Postfix expressions *) | INDEX(a1, a2) -> (* e1[e2] *) @@ -833,22 +919,27 @@ let elab_expr loc env a = (elaboration) --> __builtin_va_start(ap) va_arg(ap, ty) (preprocessing) --> __builtin_va_arg(ap, ty) - (parsing) --> __builtin_va_arg(ap, sizeof(ty)) + (elaboration) --> __builtin_va_arg(ap, sizeof(ty)) *) | CALL((VARIABLE "__builtin_va_start" as a1), [a2; a3]) -> let b1 = elab a1 and b2 = elab a2 and _b3 = elab a3 in { edesc = ECall(b1, [b2]); etyp = TVoid [] } - | CALL((VARIABLE "__builtin_va_arg" as a1), - [a2; (TYPE_SIZEOF _) as a3]) -> - let b1 = elab a1 and b2 = elab a2 and b3 = elab a3 in + + | BUILTIN_VA_ARG (a2, a3) -> + let ident = + match wrap Env.lookup_ident loc env "__builtin_va_arg" with + | (id, II_ident(sto, ty)) -> { edesc = EVar id; etyp = ty } + | _ -> assert false + in + let b2 = elab a2 and b3 = elab (TYPE_SIZEOF a3) in let ty = match b3.edesc with ESizeof ty -> ty | _ -> assert false in let ty' = default_argument_conversion env ty in if not (compatible_types env ty ty') then warning "'%a' is promoted to '%a' when passed through '...'.@ You should pass '%a', not '%a', to 'va_arg'" Cprint.typ ty Cprint.typ ty' Cprint.typ ty' Cprint.typ ty; - { edesc = ECall(b1, [b2; b3]); etyp = ty } + { edesc = ECall(ident, [b2; b3]); etyp = ty } | CALL(a1, al) -> let b1 = @@ -860,7 +951,7 @@ let elab_expr loc env a = let ty = TFun(TInt(IInt, []), None, false, []) in (* Emit an extern declaration for it *) let id = Env.fresh_ident n in - emit_elab (elab_loc loc) (Gdecl(Storage_extern, id, ty, None)); + emit_elab loc (Gdecl(Storage_extern, id, ty, None)); { edesc = EVar id; etyp = ty } | _ -> elab a1 in let bl = List.map elab al in @@ -1163,22 +1254,10 @@ let elab_expr loc env a = (* 6.5.17 Sequential expressions *) - | COMMA [] -> - error "empty sequential expression" - | COMMA (a1 :: al) -> (* watch for left associativity *) - let rec elab_comma accu = function - | [] -> accu - | a :: l -> - let b = elab a in - elab_comma { edesc = EBinop(Ocomma, accu, b, b.etyp); etyp = b.etyp } l - in elab_comma (elab a1) al - -(* Extensions that we do not handle *) - - | LABELADDR _ -> - error "GCC's &&label construct is not supported" - | GNU_BODY _ -> - error "GCC's statements within expressions are not supported" + | BINARY(COMMA, a1, a2) -> + let b1 = elab a1 in + let b2 = elab a2 in + { edesc = EBinop (Ocomma, b1, b2, b2.etyp); etyp = b2.etyp } (* Elaboration of pre- or post- increment/decrement *) and elab_pre_post_incr_decr op msg a1 = @@ -1294,12 +1373,12 @@ let elab_expr loc env a = let _ = elab_expr_f := elab_expr let elab_opt_expr loc env = function - | NOTHING -> None - | a -> Some (elab_expr loc env a) + | None -> None + | Some a -> Some (elab_expr loc env a) let elab_for_expr loc env = function - | NOTHING -> { sdesc = Sskip; sloc = elab_loc loc } - | a -> { sdesc = Sdo (elab_expr loc env a); sloc = elab_loc loc } + | None -> { sdesc = Sskip; sloc = elab_loc loc } + | Some a -> { sdesc = Sdo (elab_expr loc env a); sloc = elab_loc loc } (* Elaboration of initializers. C99 section 6.7.8 *) @@ -1522,9 +1601,9 @@ end let rec elab_designator loc env zi desig = match desig with - | NEXT_INIT -> + | [] -> zi - | INFIELD_INIT(name, desig') -> + | INFIELD_INIT name :: desig' -> begin match I.member env zi name with | Some zi' -> elab_designator loc env zi' desig' @@ -1532,7 +1611,7 @@ let rec elab_designator loc env zi desig = error loc "%s has no member named %s" (I.name zi) name; raise Exit end - | ATINDEX_INIT(a, desig') -> + | ATINDEX_INIT a :: desig' -> begin match Ceval.integer_expr env (elab_expr loc env a) with | None -> error loc "array element designator for %s is not a compile-time constant" @@ -1547,9 +1626,6 @@ let rec elab_designator loc env zi desig = n (I.name zi); raise Exit end - | ATINDEXRANGE_INIT(e1, e2) -> - error loc "GCC array range designators are not supported"; - raise Exit (* Elaboration of an initialization expression. Return the corresponding initializer. *) @@ -1566,7 +1642,7 @@ let rec elab_list zi il first = (* All initialization items consumed. *) I.to_init zi | (desig, item) :: il' -> - if desig = NEXT_INIT then begin + if desig = [] then begin match (if first then I.first env zi else I.next zi) with | None -> @@ -1584,22 +1660,28 @@ let rec elab_list zi il first = and elab_item zi item il = let ty = I.typeof zi in match item, unroll env ty with - (* Special case char array = "string literal" *) + (* Special case char array = "string literal" + or wchar array = L"wide string literal" *) | (SINGLE_INIT (CONSTANT (CONST_STRING s)) | COMPOUND_INIT [_, SINGLE_INIT(CONSTANT (CONST_STRING s))]), - TArray(TInt((IChar|IUChar|ISChar), _), sz, _) -> - if not (I.index_below (Int64.of_int(String.length s - 1)) sz) then - warning loc "initializer string for array of chars %s is too long" - (I.name zi); - elab_list (I.set zi (init_char_array_string sz s)) il false - (* Special case int array = L"wide string literal" *) - | (SINGLE_INIT (CONSTANT (CONST_WSTRING s)) - | COMPOUND_INIT [_, SINGLE_INIT(CONSTANT (CONST_WSTRING s))]), - TArray(TInt(_, _), sz, _) -> - if not (I.index_below (Int64.of_int(List.length s - 1)) sz) then - warning loc "initializer string for array of wide chars %s is too long" - (I.name zi); - elab_list (I.set zi (init_int_array_wstring sz s)) il false + TArray(TInt(ik, _), sz, _) -> + begin match elab_string_literal loc s with + | CStr s -> + if ik <> IChar && ik <> IUChar && ik <> ISChar then + error loc "initialization of an array of non-char elements with a string literal"; + if not (I.index_below (Int64.of_int(String.length s - 1)) sz) then + warning loc "initializer string for array of chars %s is too long" + (I.name zi); + elab_list (I.set zi (init_char_array_string sz s)) il false + | CWStr s -> + if ik <> wchar_ikind then + error loc "initialization of an array of non-wchar_t elements with a wide string literal"; + if not (I.index_below (Int64.of_int(List.length s - 1)) sz) then + warning loc "initializer string for array of wide chars %s is too long" + (I.name zi); + elab_list (I.set zi (init_int_array_wstring sz s)) il false + | _ -> assert false + end (* Brace-enclosed compound initializer *) | COMPOUND_INIT il', _ -> (* Process the brace-enclosed stuff, obtaining its initializer *) @@ -1681,15 +1763,17 @@ let elab_initializer loc env root ty ie = (* Elaboration of top-level and local definitions *) -let enter_typedef loc env (s, sto, ty) = +let enter_typedefs loc env sto dl = if sto <> Storage_default then error loc "Non-default storage on 'typedef' definition"; - if redef Env.lookup_typedef env s <> None then - error loc "redefinition of typedef '%s'" s; - let (id, env') = - Env.enter_typedef env s ty in - emit_elab (elab_loc loc) (Gtypedef(id, ty)); - env' + List.fold_left (fun env (s, ty, init) -> + if init <> NO_INIT then + error loc "initializer in typedef"; + if redef Env.lookup_typedef env s <> None then + error loc "redefinition of typedef '%s'" s; + let (id, env') = Env.enter_typedef env s ty in + emit_elab loc (Gtypedef(id, ty)); + env') env dl let enter_or_refine_ident local loc env s sto ty = match redef Env.lookup_ident env s with @@ -1719,47 +1803,44 @@ let enter_or_refine_ident local loc env s sto ty = | _ -> Env.enter_ident env s sto ty -let rec enter_decdefs local loc env = function - | [] -> - ([], env) - | (s, sto, ty, init) :: rem -> - (* Sanity checks on storage class *) - begin match sto with - | Storage_extern -> - if init <> NO_INIT then error loc - "'extern' declaration cannot have an initializer" - | Storage_register -> - if not local then error loc "'register' on global declaration" - | _ -> () - end; - (* function declarations are always extern *) - let sto' = - match unroll env ty with TFun _ -> Storage_extern | _ -> sto in - (* enter ident in environment with declared type, because - initializer can refer to the ident *) - let (id, env1) = enter_or_refine_ident local loc env s sto' ty in - (* process the initializer *) - let (ty', init') = elab_initializer loc env1 s ty init in - (* update environment with refined type *) - let env2 = Env.add_ident env1 id sto' ty' in - (* check for incomplete type *) - if local && sto' <> Storage_extern - && wrap incomplete_type loc env ty' then - error loc "'%s' has incomplete type" s; - if local && sto' <> Storage_extern && sto' <> Storage_static then begin - (* Local definition *) - let (decls, env3) = enter_decdefs local loc env2 rem in - ((sto', id, ty', init') :: decls, env3) - end else begin - (* Global definition *) - emit_elab (elab_loc loc) (Gdecl(sto', id, ty', init')); - enter_decdefs local loc env2 rem - end +let enter_decdefs local loc env sto dl = + (* Sanity checks on storage class *) + if sto = Storage_register && not local then + error loc "'register' on global declaration"; + if sto <> Storage_default && dl = [] then + warning loc "Storage class specifier on empty declaration"; + let rec enter_decdef (decls, env) (s, ty, init) = + if sto = Storage_extern && init <> NO_INIT then + error loc "'extern' declaration cannot have an initializer"; + (* function declarations are always extern *) + let sto' = + match unroll env ty with TFun _ -> Storage_extern | _ -> sto in + (* enter ident in environment with declared type, because + initializer can refer to the ident *) + let (id, env1) = enter_or_refine_ident local loc env s sto' ty in + (* process the initializer *) + let (ty', init') = elab_initializer loc env1 s ty init in + (* update environment with refined type *) + let env2 = Env.add_ident env1 id sto' ty' in + (* check for incomplete type *) + if local && sto' <> Storage_extern + && wrap incomplete_type loc env ty' then + error loc "'%s' has incomplete type" s; + if local && sto' <> Storage_extern && sto' <> Storage_static then + (* Local definition *) + ((sto', id, ty', init') :: decls, env2) + else begin + (* Global definition *) + emit_elab loc (Gdecl(sto', id, ty', init')); + (decls, env2) + end in + let (decls, env') = List.fold_left enter_decdef ([], env) dl in + (List.rev decls, env') -let elab_fundef env (spec, name) body loc1 loc2 = +let elab_fundef env spec name body loc = let (s, sto, inline, ty, env1) = elab_name env spec name in if sto = Storage_register then - error loc1 "a function definition cannot have 'register' storage class"; + error loc "a function definition cannot have 'register' storage class"; (* Fix up the type. We can have params = None but only for an old-style parameterless function "int f() {...}" *) let ty = @@ -1770,15 +1851,15 @@ let elab_fundef env (spec, name) body loc1 loc2 = let (ty_ret, params, vararg, attr) = match ty with | TFun(ty_ret, Some params, vararg, attr) -> (ty_ret, params, vararg, attr) - | _ -> fatal_error loc1 "wrong type for function definition" in + | _ -> fatal_error loc "wrong type for function definition" in (* Enter function in the environment, for recursive references *) - let (fun_id, env1) = enter_or_refine_ident false loc1 env s sto ty in + let (fun_id, env1) = enter_or_refine_ident false loc env s sto ty in (* Enter parameters in the environment *) let env2 = List.fold_left (fun e (id, ty) -> Env.add_ident e id Storage_default ty) (Env.new_scope env1) params in (* Elaborate function body *) - let body' = !elab_funbody_f loc2 ty_ret env2 body in + let body' = !elab_funbody_f ty_ret env2 body in (* Build and emit function definition *) let fn = { fd_storage = sto; @@ -1790,50 +1871,33 @@ let elab_fundef env (spec, name) body loc1 loc2 = fd_vararg = vararg; fd_locals = []; fd_body = body' } in - emit_elab (elab_loc loc1) (Gfundef fn); + emit_elab loc (Gfundef fn); env1 let rec elab_definition (local: bool) (env: Env.t) (def: Cabs.definition) : decl list * Env.t = match def with (* "int f(int x) { ... }" *) - | FUNDEF(spec_name, body, loc1, loc2) -> - if local then error loc1 "local definition of a function"; - let env1 = elab_fundef env spec_name body loc1 loc2 in + | FUNDEF(spec, name, body, loc) -> + if local then error loc "local definition of a function"; + let env1 = elab_fundef env spec name body loc in ([], env1) (* "int x = 12, y[10], *z" *) | DECDEF(init_name_group, loc) -> - let (dl, env1) = elab_init_name_group loc env init_name_group in - enter_decdefs local loc env1 dl - - (* "typedef int * x, y[10]; " *) - | TYPEDEF(namegroup, loc) -> - let (dl, env1) = elab_name_group loc env namegroup in - let env2 = List.fold_left (enter_typedef loc) env1 dl in - ([], env2) - - (* "struct s { ...};" or "union u;" *) - | ONLYTYPEDEF(spec, loc) -> - let (sto, inl, ty, env') = elab_specifier ~only:true loc env spec in - if sto <> Storage_default || inl then - error loc "Non-default storage or 'inline' on 'struct' or 'union' declaration"; - ([], env') - - (* global asm statement *) - | GLOBASM(_, loc) -> - error loc "Top-level 'asm' statement is not supported"; - ([], env) + let ((dl, env1), sto, tydef) = + elab_init_name_group loc env init_name_group in + if tydef then + let env2 = enter_typedefs loc env1 sto dl + in ([], env2) + else + enter_decdefs local loc env1 sto dl (* pragma *) | PRAGMA(s, loc) -> - emit_elab (elab_loc loc) (Gpragma s); + emit_elab loc (Gpragma s); ([], env) - (* extern "C" { ... } *) - | LINKAGE(_, loc, defs) -> - elab_definitions local env defs - and elab_definitions local env = function | [] -> ([], env) | d1 :: dl -> @@ -1853,11 +1917,12 @@ type stmt_context = { ctx_continue: bool (**r is 'continue' allowed? *) } -let block_labels b = +let stmt_labels stmt = let lbls = ref StringSet.empty in let rec do_stmt = function | BLOCK(b, _) -> do_block b - | IF(_, s1, s2, _) -> do_stmt s1; do_stmt s2 + | If(_, s1, Some s2, _) -> do_stmt s1; do_stmt s2 + | If(_, s1, None, _) -> do_stmt s1 | WHILE(_, s1, _) -> do_stmt s1 | DOWHILE(_, s1, _) -> do_stmt s1 | FOR(_, _, _, s1, _) -> do_stmt s1 @@ -1870,23 +1935,13 @@ let block_labels b = lbls := StringSet.add lbl !lbls; do_stmt s1 | _ -> () - and do_block b = List.iter do_stmt b.bstmts - in do_block b; !lbls + and do_block b = List.iter do_stmt b + in do_stmt stmt; !lbls let ctx_loop ctx = { ctx with ctx_break = true; ctx_continue = true } let ctx_switch ctx = { ctx with ctx_break = true } -(* Extract list of Cabs statements from a Cabs block *) - -let block_body loc b = - if b.blabels <> [] then - error loc "GCC's '__label__' declaration is not supported"; - if b.battrs <> [] then - warning loc "ignoring attributes on this block"; - b.bstmts - - (* Elaboration of statements *) let rec elab_stmt env ctx s = @@ -1912,10 +1967,6 @@ let rec elab_stmt env ctx s = end; { sdesc = Slabeled(Scase a', elab_stmt env ctx s1); sloc = elab_loc loc } - | CASERANGE(_, _, _, loc) -> - error loc "GCC's 'case' with range of values is not supported"; - sskip - | DEFAULT(s1, loc) -> { sdesc = Slabeled(Sdefault, elab_stmt env ctx s1); sloc = elab_loc loc } @@ -1926,12 +1977,16 @@ let rec elab_stmt env ctx s = (* 6.8.4 Conditional statements *) - | IF(a, s1, s2, loc) -> + | If(a, s1, s2, loc) -> let a' = elab_expr loc env a in if not (is_scalar_type env a'.etyp) then error loc "the condition of 'if' does not have scalar type"; let s1' = elab_stmt env ctx s1 in - let s2' = elab_stmt env ctx s2 in + let s2' = + match s2 with + | None -> sskip + | Some s2 -> elab_stmt env ctx s2 + in { sdesc = Sif(a', s1', s2'); sloc = elab_loc loc } (* 6.8.5 Iterative statements *) @@ -1953,17 +2008,20 @@ let rec elab_stmt env ctx s = | FOR(fc, a2, a3, s1, loc) -> let (a1', env', decls') = match fc with - | FC_EXP a1 -> - (elab_for_expr loc env a1, env, None) - | FC_DECL def -> + | Some (FC_EXP a1) -> + (elab_for_expr loc env (Some a1), env, None) + | None -> + (elab_for_expr loc env None, env, None) + | Some (FC_DECL def) -> let (dcl, env') = elab_definition true (Env.new_scope env) def in let loc = elab_loc (get_definitionloc def) in (sskip, env', Some(List.map (fun d -> {sdesc = Sdecl d; sloc = loc}) dcl)) in let a2' = - if a2 = NOTHING - then intconst 1L IInt - else elab_expr loc env' a2 in + match a2 with + | None -> intconst 1L IInt + | Some a2 -> elab_expr loc env' a2 + in if not (is_scalar_type env' a2'.etyp) then error loc "the condition of 'for' does not have scalar type"; let a3' = elab_for_expr loc env' a3 in @@ -2031,27 +2089,22 @@ let rec elab_stmt env ctx s = { sdesc = Sskip; sloc = elab_loc loc } (* Traditional extensions *) - | ASM(attr, txt, details, loc) -> - if details <> None then - error loc "GCC's extended 'asm' statements are not supported"; - { sdesc = Sasm(String.concat "" txt); sloc = elab_loc loc } + | ASM(txt, loc) -> + begin match txt with + | CONST_STRING s -> + { sdesc = Sasm s; sloc = elab_loc loc } + | _ -> + error loc "ill-defined asm statement"; + sskip + end (* Unsupported *) | DEFINITION def -> error (get_definitionloc def) "ill-placed definition"; sskip - | COMPGOTO(a, loc) -> - error loc "GCC's computed 'goto' is not supported"; - sskip - | TRY_EXCEPT(_, _, _, loc) -> - error loc "'try ... except' statement is not supported"; - sskip - | TRY_FINALLY(_, _, loc) -> - error loc "'try ... finally' statement is not supported"; - sskip - + and elab_block loc env ctx b = - let b' = elab_block_body (Env.new_scope env) ctx (block_body loc b) in + let b' = elab_block_body (Env.new_scope env) ctx b in { sdesc = Sblock b'; sloc = elab_loc loc } and elab_block_body env ctx sl = @@ -2069,13 +2122,13 @@ and elab_block_body env ctx sl = (* Elaboration of a function body. Return the corresponding C statement. *) -let elab_funbody loc return_typ env b = +let elab_funbody return_typ env b = let ctx = { ctx_return_typ = return_typ; - ctx_labels = block_labels b; + ctx_labels = stmt_labels b; ctx_break = false; ctx_continue = false } in - elab_block loc env ctx b + elab_stmt env ctx b (* Filling in forward declaration *) let _ = elab_funbody_f := elab_funbody @@ -2087,4 +2140,20 @@ let elab_file prog = reset(); ignore (elab_definitions false (Builtins.environment()) prog); elaborated_program() +(* + let rec inf = Datatypes.S inf in + let ast:Cabs.definition list = + Obj.magic + (match Parser.translation_unit_file inf (Lexer.tokens_stream lb) with + | Parser.Parser.Inter.Fail_pr -> + (* Theoretically impossible : implies inconsistencies + between grammars. *) + Cerrors.fatal_error "Internal error while parsing" + | Parser.Parser.Inter.Timeout_pr -> assert false + | Parser.Parser.Inter.Parsed_pr (ast, _ ) -> ast) + in + reset(); + ignore (elab_definitions false (Builtins.environment()) ast); + elaborated_program() +*) -- cgit v1.2.3