diff options
Diffstat (limited to 'cparser')
48 files changed, 327 insertions, 873 deletions
diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml deleted file mode 100644 index 7a00f719..00000000 --- a/cparser/Bitfields.ml +++ /dev/null @@ -1,580 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(* Elimination of bit fields in structs *) - -(* Assumes: nothing. *) - -open Machine -open C -open Cutil -open Transform - -(* Info associated to each bitfield *) - -type bitfield_info = - { bf_carrier: string; (* name of underlying regular field *) - bf_carrier_typ: typ; (* type of underlying regular field *) - bf_pos: int; (* start bit *) - bf_size: int; (* size in bit *) - bf_signed: bool; (* is field signed or unsigned? *) - bf_signed_res: bool; (* is result of extracting field signed or unsigned? *) - bf_bool: bool (* does field have type _Bool? *) - } - -(* invariants: - 0 <= pos < bitsizeof(int) - 0 < sz <= bitsizeof(int) - 0 < pos + sz <= bitsizeof(int) -*) - -let carrier_field bf = - { fld_name = bf.bf_carrier; fld_typ = bf.bf_carrier_typ; - fld_bitfield = None; fld_anonymous = false } - -(* Mapping (struct/union identifier, bitfield name) -> bitfield info *) - -let bitfield_table = - (Hashtbl.create 57: (ident * string, bitfield_info) Hashtbl.t) - -let is_bitfield structid fieldname = - Hashtbl.find_opt bitfield_table (structid, fieldname) - -(* Mapping struct/union identifier -> list of members after transformation, - including the carrier fields, but without the bit fields. - structs and unions containing no bit fields are not put in this table. *) - -let composite_transformed_members = - (Hashtbl.create 57: (ident, C.field list) Hashtbl.t) - -(* Signedness issues *) - -let unsigned_ikind_for_carrier nbits = - if nbits <= 8 then IUChar else - if nbits <= 8 * !config.sizeof_short then IUShort else - if nbits <= 8 * !config.sizeof_int then IUInt else - if nbits <= 8 * !config.sizeof_long then IULong else - if nbits <= 8 * !config.sizeof_longlong then IULongLong else - assert false - -let is_signed_enum_bitfield env sid fld eid n = - let info = Env.find_enum env eid in - if List.for_all (fun (_, v, _) -> int_representable v n false) info.Env.ei_members - then false - else if List.for_all (fun (_, v, _) -> int_representable v n true) info.Env.ei_members - then true - else begin - Diagnostics.warning Diagnostics.no_loc Diagnostics.Unnamed - "not all values of type 'enum %s' can be represented in bit-field '%s' of struct '%s' (%d bits are not enough)" - eid.C.name fld sid.C.name n; - false - end - -(* Packing algorithm -- keep consistent with [Cutil.pack_bitfield]! *) - -let pack_bitfields env sid ml = - let rec pack accu pos = function - | [] -> - (pos, accu, []) - | m :: ms as ml -> - match m.fld_bitfield with - | None -> (pos, accu, ml) - | Some n -> - if n = 0 then - (pos, accu, ms) (* bit width 0 means end of pack *) - else if pos + n > 8 * !config.sizeof_int then - (pos, accu, ml) (* doesn't fit in current word *) - else begin - let signed = - match unroll env m.fld_typ with - | TInt(ik, _) -> is_signed_ikind ik - | TEnum(eid, _) -> is_signed_enum_bitfield env sid m.fld_name eid n - | _ -> assert false (* should never happen, checked in Elab *) in - let signed2 = - match unroll env (type_of_member env m) with - | TInt(ik, _) -> is_signed_ikind ik - | _ -> assert false (* should never happen, checked in Elab *) in - let is_bool = - match unroll env m.fld_typ with - | TInt(IBool, _) -> true - | _ -> false in - - pack ((m.fld_name, pos, n, signed, signed2, is_bool) :: accu) - (pos + n) ms - end - in pack [] 0 ml - -let rec transf_struct_members env id count = function - | [] -> [] - | m :: ms as ml -> - if m.fld_bitfield = None then - m :: transf_struct_members env id count ms - else begin - let (nbits, bitfields, ml') = pack_bitfields env id ml in - if nbits = 0 then - (* Lone zero-size bitfield: just ignore *) - transf_struct_members env id count ml' - else begin - (* Create integer field of sufficient size for this bitfield group *) - let carrier = Printf.sprintf "__bf%d" count in - let carrier_ikind = unsigned_ikind_for_carrier nbits in - let carrier_typ = TInt(carrier_ikind, []) in - (* Enter each field with its bit position, size, signedness *) - List.iter - (fun (name, pos, sz, signed, signed2, is_bool) -> - if name <> "" then begin - let pos' = - if !config.bitfields_msb_first - then sizeof_ikind carrier_ikind * 8 - pos - sz - else pos in - Debug.set_bitfield_offset id name pos carrier (sizeof_ikind carrier_ikind); - Hashtbl.add bitfield_table - (id, name) - {bf_carrier = carrier; bf_carrier_typ = carrier_typ; - bf_pos = pos'; bf_size = sz; - bf_signed = signed; bf_signed_res = signed2; - bf_bool = is_bool} - end) - bitfields; - { fld_name = carrier; fld_typ = carrier_typ; fld_bitfield = None; fld_anonymous = false;} - :: transf_struct_members env id (count + 1) ml' - end - end - -let rec transf_union_members env id count = function - | [] -> [] - | m :: ms -> - (match m.fld_bitfield with - | None -> m::transf_union_members env id count ms - | Some nbits -> - let carrier = Printf.sprintf "__bf%d" count in - let carrier_ikind = unsigned_ikind_for_carrier nbits in - let carrier_typ = TInt(carrier_ikind, []) in - let signed = - match unroll env m.fld_typ with - | TInt(ik, _) -> is_signed_ikind ik - | TEnum(eid, _) -> is_signed_enum_bitfield env id m.fld_name eid nbits - | _ -> assert false (* should never happen, checked in Elab *) in - let signed2 = - match unroll env (type_of_member env m) with - | TInt(ik, _) -> is_signed_ikind ik - | _ -> assert false (* should never happen, checked in Elab *) in - let pos' = - if !config.bitfields_msb_first - then sizeof_ikind carrier_ikind * 8 - nbits - else 0 in - let is_bool = - match unroll env m.fld_typ with - | TInt(IBool, _) -> true - | _ -> false in - Hashtbl.add bitfield_table - (id, m.fld_name) - {bf_carrier = carrier; bf_carrier_typ = carrier_typ; - bf_pos = pos'; bf_size = nbits; - bf_signed = signed; bf_signed_res = signed2; - bf_bool = is_bool}; - { fld_name = carrier; fld_typ = carrier_typ; fld_bitfield = None; fld_anonymous = false;} - :: transf_union_members env id (count + 1) ms) - -let transf_composite env loc su id attr ml = - if List.for_all (fun f -> f.fld_bitfield = None) ml then - (attr, ml) - else begin - if find_custom_attributes ["packed";"__packed__"] attr <> [] then - Diagnostics.error loc "bitfields in packed structs not allowed"; - let ml' = - match su with - | Struct -> transf_struct_members env id 1 ml - | Union -> transf_union_members env id 1 ml in - Hashtbl.add composite_transformed_members id ml'; - (attr, ml') - end - -(* Bitfield manipulation expressions *) - -let left_shift_count bf = - intconst - (Int64.of_int (8 * !config.sizeof_int - (bf.bf_pos + bf.bf_size))) - IInt - -let right_shift_count bf = - intconst - (Int64.of_int (8 * !config.sizeof_int - bf.bf_size)) - IInt - -let uintconst_hex v = - { edesc = EConst(CInt(v, IUInt, Printf.sprintf "0x%LXU" v)); - etyp = TInt(IUInt, []) } - -let insertion_mask bf = - let m = - Int64.shift_left - (Int64.pred (Int64.shift_left 1L bf.bf_size)) - bf.bf_pos in - (* Give the mask an hexadecimal string representation, nicer to read *) - uintconst_hex m - -let eshift env op a b = - let ty = unary_conversion env a.etyp in - { edesc = EBinop(op, a, b, ty); etyp = ty } - -let ebinint env op a b = - let ty = binary_conversion env a.etyp b.etyp in - { edesc = EBinop(op, a, b, ty); etyp = ty } - -(* Extract the value of a bitfield *) - -(* Reference C code: - -unsigned int bitfield_unsigned_extract(unsigned int x, int ofs, int sz) -{ - return (x << (BITSIZE_UINT - (ofs + sz))) >> (BITSIZE_UINT - sz); -} - -signed int bitfield_signed_extract(unsigned int x, int ofs, int sz) -{ - return ((signed int) (x << (BITSIZE_UINT - (ofs + sz)))) - >> (BITSIZE_UINT - sz); -} - -*) - -let bitfield_extract env bf carrier = - let e1 = eshift env Oshl carrier (left_shift_count bf) in - let ty = TInt((if bf.bf_signed then IInt else IUInt), []) in - let e2 = ecast ty e1 in - let e3 = eshift env Oshr e2 (right_shift_count bf) in - if bf.bf_signed_res = bf.bf_signed - then e3 - else ecast (TInt((if bf.bf_signed_res then IInt else IUInt), [])) e3 - -(* Assign a bitfield within a carrier *) - -(* Reference C code: - -unsigned int bitfield_insert(unsigned int x, int ofs, int sz, unsigned int y) -{ - unsigned int mask = ((1U << sz) - 1) << ofs; - return (x & ~mask) | ((y << ofs) & mask); -} - -If the bitfield is of type _Bool, the new value (y above) must be converted -to _Bool to normalize it to 0 or 1. -*) - -let bitfield_assign env bf carrier newval = - let msk = insertion_mask bf in - let notmsk = {edesc = EUnop(Onot, msk); etyp = msk.etyp} in - let newval_casted = - ecast (TInt(IUInt,[])) - (if bf.bf_bool then ecast (TInt(IBool,[])) newval else newval) in - let newval_shifted = - eshift env Oshl newval_casted (intconst (Int64.of_int bf.bf_pos) IUInt) in - let newval_masked = ebinint env Oand newval_shifted msk - and oldval_masked = ebinint env Oand carrier notmsk in - ebinint env Oor oldval_masked newval_masked - -(* Initialize a bitfield *) - -(* Reference C code: - -unsigned int bitfield_init(int ofs, int sz, unsigned int y) -{ - unsigned int mask = (1U << sz) - 1; - return (y & mask) << ofs; -} - -If the bitfield is of type _Bool, the new value (y above) must be converted -to _Bool to normalize it to 0 or 1. -*) - -let bitfield_initializer bf i = - match i with - | Init_single e -> - let m = Int64.pred (Int64.shift_left 1L bf.bf_size) in - let e_cast = - if bf.bf_bool then ecast (TInt(IBool,[])) e else e in - let e_mask = uintconst_hex m in - let e_and = - {edesc = EBinop(Oand, e_cast, e_mask, TInt(IUInt,[])); - etyp = TInt(IUInt,[])} in - {edesc = EBinop(Oshl, e_and, intconst (Int64.of_int bf.bf_pos) IInt, - TInt(IUInt, [])); - etyp = TInt(IUInt, [])} - | _ -> - assert false - -(* Associate to the left so that it prints more nicely *) - -let or_expr_list = function - | [] -> intconst 0L IUInt - | [e] -> e - | e1 :: el -> - List.fold_left - (fun accu e -> - {edesc = EBinop(Oor, accu, e, TInt(IUInt,[])); - etyp = TInt(IUInt,[])}) - e1 el - -(* Initialize the carrier for consecutive bitfields *) - -let rec pack_bitfield_init id carrier fld_init_list = - match fld_init_list with - | [] -> ([], []) - | (fld, i) :: rem -> - match is_bitfield id fld.fld_name with - | None -> - ([], fld_init_list) - | Some bf -> - if bf.bf_carrier <> carrier then - ([], fld_init_list) - else begin - let (el, rem') = pack_bitfield_init id carrier rem in - (bitfield_initializer bf i :: el, rem') - end - -let rec transf_struct_init id fld_init_list = - match fld_init_list with - | [] -> [] - | (fld, i) :: rem -> - match is_bitfield id fld.fld_name with - | None -> - (fld, i) :: transf_struct_init id rem - | Some bf -> - let (el, rem') = - pack_bitfield_init id bf.bf_carrier fld_init_list in - (carrier_field bf, - Init_single {edesc = ECast(bf.bf_carrier_typ, or_expr_list el); - etyp = bf.bf_carrier_typ}) - :: transf_struct_init id rem' - -(* Add default initialization for carrier fields that are not listed in the output of - [transf_struct_init]. This happens with carrier fields that contain no named - bitfields, only anonymous bitfields. *) - -let rec completed_struct_init env actual expected = - match actual, expected with - | [], [] -> [] - | (f_a, i) :: actual', f_e :: expected' when f_a.fld_name = f_e.fld_name -> - (f_a, i) :: completed_struct_init env actual' expected' - | _, f_e :: expected' -> - (f_e, default_init env f_e.fld_typ) :: completed_struct_init env actual expected' - | _, [] -> - assert false - -(* Check whether a field access (e.f or e->f) is a bitfield access. - If so, return carrier expression (e and *e, respectively) - and bitfield_info *) - -let rec is_bitfield_access env e = - match e.edesc with - | EUnop(Odot fieldname, e1) -> - begin match unroll env e1.etyp with - | TUnion (id,_) - | TStruct(id, _) -> - (try Some(e1, Hashtbl.find bitfield_table (id, fieldname)) - with Not_found -> None) - | _ -> - None - end - | EUnop(Oarrow fieldname, e1) -> - begin match unroll env e1.etyp with - | TPtr(ty, _) | TArray(ty, _, _) -> - is_bitfield_access env - {edesc = EUnop(Odot fieldname, - {edesc = EUnop(Oderef, e1); etyp = ty}); - etyp = e.etyp} - | _ -> - None - end - | _ -> None - -(* Expressions *) - -let rec transf_exp env ctx e = - match e.edesc with - | EConst _ -> e - | ESizeof _ -> e - | EAlignof _ -> e - | EVar _ -> e - - | EUnop(Odot s, e1) -> - begin match is_bitfield_access env e with - | None -> - {edesc = EUnop(Odot s, transf_exp env Val e1); etyp = e.etyp} - | Some(ex, bf) -> - transf_read env ex bf - end - | EUnop(Oarrow s, e1) -> - begin match is_bitfield_access env e with - | None -> - {edesc = EUnop(Oarrow s, transf_exp env Val e1); etyp = e.etyp} - | Some(ex, bf) -> - transf_read env ex bf - end - | EUnop((Opreincr|Opredecr) as op, e1) -> - begin match is_bitfield_access env e1 with - | None -> - {edesc = EUnop(op, transf_exp env Val e1); etyp = e.etyp} - | Some(ex, bf) -> - transf_pre env ctx (op_for_incr_decr op) ex bf e1.etyp - end - | EUnop((Opostincr|Opostdecr) as op, e1) -> - begin match is_bitfield_access env e1 with - | None -> - {edesc = EUnop(op, transf_exp env Val e1); etyp = e.etyp} - | Some(ex, bf) -> - transf_post env ctx (op_for_incr_decr op) ex bf e1.etyp - end - | EUnop(op, e1) -> - {edesc = EUnop(op, transf_exp env Val e1); etyp = e.etyp} - - | EBinop(Oassign, e1, e2, ty) -> - begin match is_bitfield_access env e1 with - | None -> - {edesc = EBinop(Oassign, transf_exp env Val e1, - transf_exp env Val e2, ty); - etyp = e.etyp} - | Some(ex, bf) -> - transf_assign env ctx ex bf e2 - end - | EBinop((Oadd_assign|Osub_assign|Omul_assign|Odiv_assign - |Omod_assign|Oand_assign|Oor_assign|Oxor_assign - |Oshl_assign|Oshr_assign) as op, - e1, e2, ty) -> - begin match is_bitfield_access env e1 with - | None -> - {edesc = EBinop(op, transf_exp env Val e1, - transf_exp env Val e2, ty); etyp = e.etyp} - | Some(ex, bf) -> - transf_assignop env ctx (op_for_assignop op) ex bf e2 ty - end - | EBinop(Ocomma, e1, e2, ty) -> - {edesc = EBinop(Ocomma, transf_exp env Effects e1, - transf_exp env Val e2, ty); - etyp = e.etyp} - | EBinop(op, e1, e2, ty) -> - {edesc = EBinop(op, transf_exp env Val e1, transf_exp env Val e2, ty); - etyp = e.etyp} - - | EConditional(e1, e2, e3) -> - {edesc = EConditional(transf_exp env Val e1, - transf_exp env ctx e2, transf_exp env ctx e3); - etyp = e.etyp} - | ECast(ty, e1) -> - {edesc = ECast(ty, transf_exp env Val e1); etyp = e.etyp} - | ECompound(ty, i) -> - {edesc = ECompound(ty, transf_init env i); etyp = e.etyp} - | ECall(e1, el) -> - {edesc = ECall(transf_exp env Val e1, List.map (transf_exp env Val) el); - etyp = e.etyp} - -and transf_read env e bf = - bitfield_extract env bf - {edesc = EUnop(Odot bf.bf_carrier, transf_exp env Val e); - etyp = bf.bf_carrier_typ} - -and transf_assign env ctx e1 bf e2 = - bind_lvalue env (transf_exp env Val e1) (fun base -> - let carrier = - {edesc = EUnop(Odot bf.bf_carrier, base); etyp = bf.bf_carrier_typ} in - let asg = - eassign carrier (bitfield_assign env bf carrier (transf_exp env Val e2)) in - if ctx = Val then ecomma asg (bitfield_extract env bf carrier) else asg) - -and transf_assignop env ctx op e1 bf e2 tyres = - bind_lvalue env (transf_exp env Val e1) (fun base -> - let carrier = - {edesc = EUnop(Odot bf.bf_carrier, base); etyp = bf.bf_carrier_typ} in - let rhs = - {edesc = EBinop(op, bitfield_extract env bf carrier, transf_exp env Val e2, tyres); - etyp = tyres} in - let asg = - eassign carrier (bitfield_assign env bf carrier rhs) in - if ctx = Val then ecomma asg (bitfield_extract env bf carrier) else asg) - -and transf_pre env ctx op e1 bf tyfield = - transf_assignop env ctx op e1 bf (intconst 1L IInt) - (unary_conversion env tyfield) - -and transf_post env ctx op e1 bf tyfield = - if ctx = Effects then - transf_pre env ctx op e1 bf tyfield - else begin - bind_lvalue env (transf_exp env Val e1) (fun base -> - let carrier = - {edesc = EUnop(Odot bf.bf_carrier, base); etyp = bf.bf_carrier_typ} in - let temp = mk_temp env tyfield in - let tyres = unary_conversion env tyfield in - let settemp = eassign temp (bitfield_extract env bf carrier) in - let rhs = - {edesc = EBinop(op, temp, intconst 1L IInt, tyres); etyp = tyres} in - let asg = - eassign carrier (bitfield_assign env bf carrier rhs) in - ecomma (ecomma settemp asg) temp) - end - -(* Initializers *) - -and transf_init env i = - match i with - | Init_single e -> Init_single (transf_exp env Val e) - | Init_array il -> Init_array (List.rev (List.rev_map (transf_init env) il)) - | Init_struct(id, fld_init_list) -> - let fld_init_list' = - List.map (fun (f, i) -> (f, transf_init env i)) fld_init_list in - begin match Hashtbl.find composite_transformed_members id with - | exception Not_found -> - Init_struct(id, fld_init_list') - | ml -> - Init_struct(id, completed_struct_init env (transf_struct_init id fld_init_list') ml) - end - | Init_union(id, fld, i) -> - let i' = transf_init env i in - match is_bitfield id fld.fld_name with - | None -> - Init_union(id, fld, i') - | Some bf -> - Init_union(id, carrier_field bf, Init_single (bitfield_initializer bf i')) - -(* Declarations *) - -let transf_decl env loc (sto, id, ty, init_opt) = - (sto, id, ty, - match init_opt with None -> None | Some i -> Some(transf_init env i)) - -(* Statements *) - -let transf_stmt env s = - Transform.stmt - ~expr:(fun loc env ctx e -> transf_exp env ctx e) - ~decl:(fun env (sto, id, ty, init_opt) -> transf_decl env s.sloc (sto, id, ty, init_opt)) - env s - -(* Functions *) - -let transf_fundef env loc f = - Transform.fundef transf_stmt env f - -(* Programs *) - -let program p = - Hashtbl.clear bitfield_table; - Hashtbl.clear composite_transformed_members; - Transform.program - ~composite:transf_composite - ~decl: transf_decl - ~fundef:transf_fundef - p diff --git a/cparser/Bitfields.mli b/cparser/Bitfields.mli deleted file mode 100644 index 45899a46..00000000 --- a/cparser/Bitfields.mli +++ /dev/null @@ -1,16 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -val program: C.program -> C.program diff --git a/cparser/C.mli b/cparser/C.mli index 15717565..763a9277 100644 --- a/cparser/C.mli +++ b/cparser/C.mli @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/Cabs.v b/cparser/Cabs.v index ff046cba..accb95a0 100644 --- a/cparser/Cabs.v +++ b/cparser/Cabs.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/Cabshelper.ml b/cparser/Cabshelper.ml index 7cffef08..36f67283 100644 --- a/cparser/Cabshelper.ml +++ b/cparser/Cabshelper.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml index ecf83779..14f61e06 100644 --- a/cparser/Ceval.ml +++ b/cparser/Ceval.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/Ceval.mli b/cparser/Ceval.mli index 32a0ed91..5b9bb0d7 100644 --- a/cparser/Ceval.mli +++ b/cparser/Ceval.mli @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/Cflow.ml b/cparser/Cflow.ml index cc257189..061e958e 100644 --- a/cparser/Cflow.ml +++ b/cparser/Cflow.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -23,8 +24,12 @@ open Cutil module StringSet = Set.Make(String) (* Functions declared noreturn by the standard *) +(* We also add our own "__builtin_unreachable" function because, currently, + it is difficult to attach attributes to a built-in function. *) + let std_noreturn_functions = - ["longjmp";"exit";"_exit";"abort";"_Exit";"quick_exit";"thrd_exit"] + ["longjmp";"exit";"_exit";"abort";"_Exit";"quick_exit";"thrd_exit"; + "__builtin_unreachable"] (* Statements are abstracted as "flow transformers": functions from possible inputs to possible outcomes. diff --git a/cparser/Cflow.mli b/cparser/Cflow.mli index 0de245ae..8348b37e 100644 --- a/cparser/Cflow.mli +++ b/cparser/Cflow.mli @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/Checks.ml b/cparser/Checks.ml index 17caf19a..507488f2 100644 --- a/cparser/Checks.ml +++ b/cparser/Checks.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/Checks.mli b/cparser/Checks.mli index cfd7b04d..08ce4e9a 100644 --- a/cparser/Checks.mli +++ b/cparser/Checks.mli @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/Cleanup.ml b/cparser/Cleanup.ml index 63ac8ac1..62b00e04 100644 --- a/cparser/Cleanup.ml +++ b/cparser/Cleanup.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/Cleanup.mli b/cparser/Cleanup.mli index 818a51bc..c469936a 100644 --- a/cparser/Cleanup.mli +++ b/cparser/Cleanup.mli @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml index 9aeec421..93377989 100644 --- a/cparser/Cprint.ml +++ b/cparser/Cprint.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/Cprint.mli b/cparser/Cprint.mli index be7ce029..01175d36 100644 --- a/cparser/Cprint.mli +++ b/cparser/Cprint.mli @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 3467c092..d3a830ce 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -448,34 +449,6 @@ let rec equal_types env t1 t2 = let compatible_types mode env t1 t2 = match combine_types mode env t1 t2 with Some _ -> true | None -> false -(* Naive placement algorithm for bit fields, might not match that - of the compiler. *) - -let pack_bitfields ml = - let rec pack nbits = function - | [] -> - (nbits, []) - | m :: ms as ml -> - match m.fld_bitfield with - | None -> (nbits, ml) - | Some n -> - if n = 0 then - (nbits, ms) (* bit width 0 means end of pack *) - else if nbits + n > 8 * !config.sizeof_int then - (nbits, ml) (* doesn't fit in current word *) - else - pack (nbits + n) ms (* add to current word *) - in - let (nbits, ml') = pack 0 ml in - let (sz, al) = - (* A lone bitfield of width 0 consumes no space and aligns to 1 *) - if nbits = 0 then (0, 1) else - if nbits <= 8 then (1, 1) else - if nbits <= 16 then (2, 2) else - if nbits <= 32 then (4, 4) else - if nbits <= 64 then (8, 8) else assert false in - (sz, al, ml') - (* Natural alignment, in bytes *) let alignof_ikind = function @@ -519,15 +492,13 @@ let rec alignof env t = let alignof_struct_union env members = let rec align_rec al = function | [] -> Some al - | m :: rem as ml -> - if m.fld_bitfield = None then begin + | m :: rem -> + if m.fld_name = "" then + align_rec al rem + else match alignof env m.fld_typ with | None -> None | Some a -> align_rec (max a al) rem - end else begin - let (s, a, ml') = pack_bitfields ml in - align_rec (max a al) ml' - end in align_rec 1 members let align x boundary = @@ -604,43 +575,63 @@ let sizeof_union env members = Bitfields are taken into account for the size and offset computations but not given an offset. Not done here but in composite_info_def: rounding size to alignment. *) + let sizeof_layout_struct env members ma = - let align_offset ofs a = - align ofs (if ma > 0 && a > ma then ma else a) in - let rec sizeof_rec ofs accu = function + + let align_bit_offset pos a = + align pos (8 * (if ma > 0 && a > ma then ma else a)) in + + let record_field name pos = + assert (pos mod 8 = 0); + (name, pos / 8) in + + (* pos is the current position in bits *) + let rec sizeof_rec pos accu = function | [] -> - Some (ofs, accu) + Some (pos, accu) | [ { fld_typ = TArray(_, None, _) } as m ] -> (* C99: ty[] allowed as last field *) begin match alignof env m.fld_typ with | Some a -> - let ofs = align_offset ofs a in - Some (ofs, (m.fld_name, ofs) :: accu) + let pos = align_bit_offset pos a in + Some (pos, record_field m.fld_name pos :: accu) | None -> None end - | m :: rem as ml -> - if m.fld_bitfield = None then begin - match alignof env m.fld_typ, sizeof env m.fld_typ with - | Some a, Some s -> - let ofs = align_offset ofs a in - sizeof_rec (ofs + s) ((m.fld_name, ofs) :: accu) rem - | _, _ -> None - end else begin - let (s, a, ml') = pack_bitfields ml in - sizeof_rec (align_offset ofs a + s) accu ml' + | m :: rem -> + begin match alignof env m.fld_typ, sizeof env m.fld_typ with + | Some a, Some s -> + begin match m.fld_bitfield with + | None -> + let pos = align_bit_offset pos a in + sizeof_rec (pos + s * 8) + (record_field m.fld_name pos :: accu) + rem + | Some width -> + (* curr = beginning of storage unit, in bits + next = one past end of storage unit, in bits *) + let curr = pos / (a * 8) * (a * 8) in + let next = curr + s * 8 in + let pos' = + if width <= 0 then align pos (a * 8) + else if pos + width <= next then pos + width + else next + width in + sizeof_rec pos' accu rem + end + | _, _ -> + None end in sizeof_rec 0 [] members let sizeof_struct env members ma = match sizeof_layout_struct env members ma with | None -> None - | Some(sz, offsets) -> Some sz + | Some(bitsize, offsets) -> Some ((bitsize + 7) / 8) (* Compute the offsets of all non-bitfield members of a struct. *) let struct_layout env attrs members = let (ma, _, _) = packing_parameters attrs in match sizeof_layout_struct env members ma with - | Some(sz, offsets) -> offsets + | Some(bitsize, offsets) -> offsets | None -> [] (* Compute the offset of a struct member *) diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index 2ddee78c..17eb2207 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/Diagnostics.ml b/cparser/Diagnostics.ml index 86a5e522..483b0376 100644 --- a/cparser/Diagnostics.ml +++ b/cparser/Diagnostics.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/Diagnostics.mli b/cparser/Diagnostics.mli index 0f0a0ea5..1210353f 100644 --- a/cparser/Diagnostics.mli +++ b/cparser/Diagnostics.mli @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index bb9f8aca..a5b87e2e 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -1001,7 +1002,7 @@ and elab_field_group env = function | TInt(ik, _) -> ik | TEnum(_, _) -> enum_ikind | _ -> ILongLong (* trigger next error message *) in - if integer_rank ik > integer_rank IInt then begin + if sizeof_ikind ik > sizeof_ikind IInt then begin error loc "the type of bit-field '%a' must be an integer type no bigger than 'int'" pp_field id; None,env @@ -2871,7 +2872,10 @@ let elab_definition (for_loop: bool) (local: bool) (nonstatic_inline: bool) (* pragma *) | PRAGMA(s, loc) -> - emit_elab env loc (Gpragma s); + if local then + warning loc Unnamed "pragmas are ignored inside functions" + else + emit_elab env loc (Gpragma s); ([], env) (* static assertion *) diff --git a/cparser/Elab.mli b/cparser/Elab.mli index 59c5efc1..bca4f74d 100644 --- a/cparser/Elab.mli +++ b/cparser/Elab.mli @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/Env.ml b/cparser/Env.ml index 00806be1..7918c31f 100644 --- a/cparser/Env.ml +++ b/cparser/Env.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/Env.mli b/cparser/Env.mli index 589a76c7..7c1096cf 100644 --- a/cparser/Env.mli +++ b/cparser/Env.mli @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/ErrorReports.ml b/cparser/ErrorReports.ml index e8f0bee5..ac1e17ac 100644 --- a/cparser/ErrorReports.ml +++ b/cparser/ErrorReports.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/ErrorReports.mli b/cparser/ErrorReports.mli index dbaba5ff..c2160b49 100644 --- a/cparser/ErrorReports.mli +++ b/cparser/ErrorReports.mli @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/ExtendedAsm.ml b/cparser/ExtendedAsm.ml index df2da2a2..d34dd654 100644 --- a/cparser/ExtendedAsm.ml +++ b/cparser/ExtendedAsm.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/GCC.ml b/cparser/GCC.ml index 458e51d3..31385b45 100644 --- a/cparser/GCC.ml +++ b/cparser/GCC.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/GCC.mli b/cparser/GCC.mli index 174e5754..5b2ddbba 100644 --- a/cparser/GCC.mli +++ b/cparser/GCC.mli @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll index 881d411a..42980d30 100644 --- a/cparser/Lexer.mll +++ b/cparser/Lexer.mll @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -95,7 +96,8 @@ let () = (* We can ignore the __extension__ GCC keyword. *) ignored_keywords := SSet.add "__extension__" !ignored_keywords -let init_ctx = SSet.singleton "__builtin_va_list" +let init_ctx = SSet.of_list (List.map fst CBuiltins.builtins.C.builtin_typedefs) + let types_context : SSet.t ref = ref init_ctx let _ = @@ -391,7 +393,7 @@ and string_literal startp accu = parse (* We assume gcc -E syntax but try to tolerate variations. *) and hash = parse | whitespace_char_no_newline + - (decimal_constant as n) + (digit + as n) whitespace_char_no_newline * "\"" ([^ '\n' '\"']* as file) "\"" [^ '\n']* '\n' diff --git a/cparser/Machine.ml b/cparser/Machine.ml index 97bedb3b..c47ec594 100644 --- a/cparser/Machine.ml +++ b/cparser/Machine.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -178,12 +179,12 @@ let x86_32 = struct_passing_style = SP_split_args; struct_return_style = SR_ref} -let x86_32_macosx = +let x86_32_macos = {x86_32 with struct_passing_style = SP_split_args; struct_return_style = SR_int1248 } let x86_32_bsd = - x86_32_macosx + x86_32_macos let x86_64 = { i32lpll64 with name = "x86_64"; char_signed = true; @@ -242,6 +243,9 @@ let aarch64 = struct_passing_style = SP_ref_callee; (* Wrong *) struct_return_style = SR_ref } (* Wrong *) +let aarch64_apple = + { aarch64 with char_signed = true } + (* Add GCC extensions re: sizeof and alignof *) let gcc_extensions c = diff --git a/cparser/Machine.mli b/cparser/Machine.mli index ca7de17b..f9d347b9 100644 --- a/cparser/Machine.mli +++ b/cparser/Machine.mli @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -71,7 +72,7 @@ val ilp32ll64 : t val i32lpll64 : t val il32pll64 : t val x86_32 : t -val x86_32_macosx : t +val x86_32_macos : t val x86_32_bsd : t val x86_64 : t val win32 : t @@ -87,6 +88,7 @@ val arm_bigendian : t val rv32 : t val rv64 : t val aarch64 : t +val aarch64_apple : t val gcc_extensions : t -> t val compcert_interpreter : t -> t diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml index 4c70c7ae..f3a45785 100644 --- a/cparser/PackedStructs.ml +++ b/cparser/PackedStructs.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -60,10 +61,10 @@ let set_alignas_attr al attrs = (* Rewriting field declarations *) let transf_field_decl mfa swapped loc env struct_id f = - if f.fld_bitfield <> None then - error loc "bitfields in packed structs not allowed"; (* Register as byte-swapped if needed *) if swapped then begin + if f.fld_bitfield <> None then + error loc "byte-swapped bit fields are not supported"; let (can_swap, must_swap) = can_byte_swap env f.fld_typ in if not can_swap then fatal_error loc "cannot byte-swap field of type '%a'" @@ -73,6 +74,8 @@ let transf_field_decl mfa swapped loc env struct_id f = end; (* Reduce alignment if requested *) if mfa = 0 then f else begin + if f.fld_bitfield <> None then + error loc "bit fields in packed structs are not supported"; let al = safe_alignof loc env f.fld_typ in { f with fld_typ = change_attributes_type env (set_alignas_attr (min mfa al)) f.fld_typ } diff --git a/cparser/Parse.ml b/cparser/Parse.ml index d9f9aa1c..a54af0cc 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -17,7 +18,7 @@ module CharSet = Set.Make(struct type t = char let compare = compare end) -let transform_program t p name = +let transform_program t p = let run_pass pass flag p = if CharSet.mem flag t then begin let p = pass p in @@ -26,12 +27,11 @@ let transform_program t p name = end else p in - let p1 = (run_pass StructPassing.program 's' - (run_pass PackedStructs.program 'p' - (run_pass Unblock.program 'b' - (run_pass Bitfields.program 'f' - p)))) in - Rename.program p1 + p + |> run_pass Unblock.program 'b' + |> run_pass PackedStructs.program 'p' + |> run_pass StructPassing.program 's' + |> Rename.program let parse_transformations s = let t = ref CharSet.empty in @@ -39,7 +39,6 @@ let parse_transformations s = String.iter (function 'b' -> set "b" | 's' -> set "s" - | 'f' -> set "bf" | 'p' -> set "bp" | _ -> ()) s; @@ -52,34 +51,33 @@ let read_file sourcefile = close_in ic; text +let parse_string name text = + let log_fuel = Camlcoq.Nat.of_int 50 in + match + Parser.translation_unit_file log_fuel (Lexer.tokens_stream name text) + with + | Parser.MenhirLibParser.Inter.Parsed_pr (ast, _ ) -> + (ast: Cabs.definition list) + | _ -> (* Fail_pr or Fail_pr_full or Timeout_pr, depending + on the version of Menhir. + Fail_pr{,_full} means that there's an inconsistency + between the pre-parser and the parser. + Timeout_pr means that we ran for 2^50 steps. *) + Diagnostics.fatal_error Diagnostics.no_loc "internal error while parsing" + let preprocessed_file transfs name sourcefile = Diagnostics.reset(); + let check_errors x = + Diagnostics.check_errors(); x in (* Reading the whole file at once may seem costly, but seems to be the simplest / most robust way of accessing the text underlying a range of positions. This is used when printing an error message. Plus, I note that reading the whole file into memory leads to a speed increase: "make -C test" speeds up by 3 seconds out of 40 on my machine. *) - let text = read_file sourcefile in - let p = - let t = parse_transformations transfs in - let log_fuel = Camlcoq.Nat.of_int 50 in - let ast : Cabs.definition list = - (match Timing.time "Parsing" - (* The call to Lexer.tokens_stream results in the pre - parsing of the entire file. This is non-negligeabe, - so we cannot use Timing.time2 *) - (fun () -> - Parser.translation_unit_file log_fuel (Lexer.tokens_stream name text)) () - with - | Parser.MenhirLibParser.Inter.Fail_pr -> - (* Theoretically impossible : implies inconsistencies - between grammars. *) - Diagnostics.fatal_error Diagnostics.no_loc "internal error while parsing" - | Parser.MenhirLibParser.Inter.Timeout_pr -> assert false - | Parser.MenhirLibParser.Inter.Parsed_pr (ast, _ ) -> ast) in - let p1 = Timing.time "Elaboration" Elab.elab_file ast in - Diagnostics.check_errors (); - Timing.time2 "Emulations" transform_program t p1 name in - Diagnostics.check_errors(); - p + read_file sourcefile + |> Timing.time2 "Parsing" parse_string name + |> Timing.time "Elaboration" Elab.elab_file + |> check_errors + |> Timing.time2 "Emulations" transform_program (parse_transformations transfs) + |> check_errors diff --git a/cparser/Parse.mli b/cparser/Parse.mli index 433e2e73..c406d96c 100644 --- a/cparser/Parse.mli +++ b/cparser/Parse.mli @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/Parser.vy b/cparser/Parser.vy index 93d84ecf..f1abe3d9 100644 --- a/cparser/Parser.vy +++ b/cparser/Parser.vy @@ -6,10 +6,11 @@ /* */ /* Copyright Institut National de Recherche en Informatique et en */ /* Automatique. All rights reserved. This file is distributed */ -/* under the terms of the GNU General Public License as published by */ -/* the Free Software Foundation, either version 2 of the License, or */ -/* (at your option) any later version. This file is also distributed */ -/* under the terms of the INRIA Non-Commercial License Agreement. */ +/* under the terms of the GNU Lesser General Public License as */ +/* published by the Free Software Foundation, either version 2.1 of */ +/* the License, or (at your option) any later version. */ +/* This file is also distributed under the terms of the */ +/* INRIA Non-Commercial License Agreement. */ /* */ /* *********************************************************************/ diff --git a/cparser/Rename.ml b/cparser/Rename.ml index 64412194..96424bf8 100644 --- a/cparser/Rename.ml +++ b/cparser/Rename.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/Rename.mli b/cparser/Rename.mli index 818a51bc..c469936a 100644 --- a/cparser/Rename.mli +++ b/cparser/Rename.mli @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/StructPassing.ml b/cparser/StructPassing.ml index 222da367..f1f481d0 100644 --- a/cparser/StructPassing.ml +++ b/cparser/StructPassing.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/StructPassing.mli b/cparser/StructPassing.mli index 45899a46..3ac42495 100644 --- a/cparser/StructPassing.mli +++ b/cparser/StructPassing.mli @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/Transform.ml b/cparser/Transform.ml index a57d94c4..2ca235f1 100644 --- a/cparser/Transform.ml +++ b/cparser/Transform.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/Transform.mli b/cparser/Transform.mli index 220b7944..c00fd15c 100644 --- a/cparser/Transform.mli +++ b/cparser/Transform.mli @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml index d25f70c6..4b1f2262 100644 --- a/cparser/Unblock.ml +++ b/cparser/Unblock.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -31,6 +32,9 @@ let rec local_initializer env path init k = let (ty_elt, sz) = match unroll env path.etyp with | TArray(ty_elt, Some sz, _) -> (ty_elt, sz) + (* We accept empty array initializer for flexible array members, which + has size zero *) + | TArray(ty_elt, None, _) when il = [] -> (ty_elt, 0L) | _ -> Diagnostics.fatal_error Diagnostics.no_loc "wrong type for array initializer" in let rec array_init pos il = if pos >= sz then k else begin diff --git a/cparser/Unblock.mli b/cparser/Unblock.mli index e6bea9e4..bd807096 100644 --- a/cparser/Unblock.mli +++ b/cparser/Unblock.mli @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/deLexer.ml b/cparser/deLexer.ml index ee6976d4..e3ab3291 100644 --- a/cparser/deLexer.ml +++ b/cparser/deLexer.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/handcrafted.messages b/cparser/handcrafted.messages index 23e90b3e..db7318c4 100644 --- a/cparser/handcrafted.messages +++ b/cparser/handcrafted.messages @@ -7,10 +7,11 @@ # # # Copyright Institut National de Recherche en Informatique et en # # Automatique. All rights reserved. This file is distributed # -# under the terms of the GNU General Public License as published by # -# the Free Software Foundation, either version 2 of the License, or # -# (at your option) any later version. This file is also distributed # -# under the terms of the INRIA Non-Commercial License Agreement. # +# under the terms of the GNU Lesser General Public License as # +# published by the Free Software Foundation, either version 2.1 of # +# the License, or (at your option) any later version. # +# This file is also distributed under the terms of the # +# INRIA Non-Commercial License Agreement. # # # ####################################################################### diff --git a/cparser/pre_parser.mly b/cparser/pre_parser.mly index 4b62b235..cffbd192 100644 --- a/cparser/pre_parser.mly +++ b/cparser/pre_parser.mly @@ -7,10 +7,11 @@ /* */ /* Copyright Institut National de Recherche en Informatique et en */ /* Automatique. All rights reserved. This file is distributed */ -/* under the terms of the GNU General Public License as published by */ -/* the Free Software Foundation, either version 2 of the License, or */ -/* (at your option) any later version. This file is also distributed */ -/* under the terms of the INRIA Non-Commercial License Agreement. */ +/* under the terms of the GNU Lesser General Public License as */ +/* published by the Free Software Foundation, either version 2.1 of */ +/* the License, or (at your option) any later version. */ +/* This file is also distributed under the terms of the */ +/* INRIA Non-Commercial License Agreement. */ /* */ /* *********************************************************************/ diff --git a/cparser/pre_parser_aux.ml b/cparser/pre_parser_aux.ml index 4a4953ba..a35305ac 100644 --- a/cparser/pre_parser_aux.ml +++ b/cparser/pre_parser_aux.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/cparser/pre_parser_aux.mli b/cparser/pre_parser_aux.mli index f6b98a95..36e33bc5 100644 --- a/cparser/pre_parser_aux.mli +++ b/cparser/pre_parser_aux.mli @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) |