diff options
Diffstat (limited to 'cparser')
-rw-r--r-- | cparser/Bitfields.ml | 10 | ||||
-rw-r--r-- | cparser/Ceval.ml | 41 | ||||
-rw-r--r-- | cparser/Cutil.ml | 7 | ||||
-rw-r--r-- | cparser/Cutil.mli | 4 | ||||
-rw-r--r-- | cparser/Elab.ml | 34 | ||||
-rw-r--r-- | cparser/Env.ml | 11 | ||||
-rw-r--r-- | cparser/ExtendedAsm.ml | 1 | ||||
-rw-r--r-- | cparser/Lexer.mll | 5 | ||||
-rw-r--r-- | cparser/PackedStructs.ml | 12 | ||||
-rw-r--r-- | cparser/StructReturn.ml | 2 | ||||
-rw-r--r-- | cparser/Transform.ml | 4 | ||||
-rw-r--r-- | cparser/Transform.mli | 2 | ||||
-rw-r--r-- | cparser/Unblock.ml | 19 |
13 files changed, 58 insertions, 94 deletions
diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml index bbc39456..d55a6d36 100644 --- a/cparser/Bitfields.ml +++ b/cparser/Bitfields.ml @@ -19,7 +19,7 @@ open Printf open Machine -open C +open !C open Cutil open Transform @@ -60,12 +60,6 @@ let unsigned_ikind_for_carrier nbits = if nbits <= 8 * !config.sizeof_longlong then IULongLong else assert false -let fits_unsigned v n = - v >= 0L && v < Int64.shift_left 1L n - -let fits_signed v n = - let p = Int64.shift_left 1L (n-1) in v >= Int64.neg p && v < p - 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 @@ -73,7 +67,7 @@ let is_signed_enum_bitfield env sid fld eid n = else if List.for_all (fun (_, v, _) -> int_representable v n true) info.Env.ei_members then true else begin - Cerrors.warning "Warning: not all values of type 'enum %s' can be represented in bit-field '%s' of struct '%s' (%d bits are not enough)" eid.name fld sid.name n; + Cerrors.warning "Warning: not all values of type 'enum %s' can be represented in bit-field '%s' of struct '%s' (%d bits are not enough)" eid.name fld sid.C.name n; false end diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml index 74b535d4..c3d7eeeb 100644 --- a/cparser/Ceval.ml +++ b/cparser/Ceval.ml @@ -91,7 +91,7 @@ let is_signed env ty = | TEnum(_, _) -> is_signed_ikind enum_ikind | _ -> false -let cast env ty_to ty_from v = +let cast env ty_to v = match unroll env ty_to, v with | TInt(IBool, _), _ -> if boolean_value v then I 1L else I 0L @@ -118,12 +118,12 @@ let unop env op tyres ty v = | Olognot, _, _ -> if boolean_value v then I 0L else I 1L | Onot, _, I n -> I (Int64.lognot n) | _ -> raise Notconst - in cast env ty tyres res + in cast env ty res -let comparison env direction ptraction tyop ty1 v1 ty2 v2 = +let comparison env direction ptraction tyop v1 v2 = (* tyop = type at which the comparison is done *) let b = - match cast env tyop ty1 v1, cast env tyop ty2 v2 with + match cast env tyop v1, cast env tyop v2 with | I n1, I n2 -> if is_signed env tyop then direction (compare n1 n2) 0 @@ -143,25 +143,25 @@ let binop env op tyop tyres ty1 v1 ty2 v2 = match op with | Oadd -> if is_arith_type env ty1 && is_arith_type env ty2 then begin - match cast env tyop ty1 v1, cast env tyop ty2 v2 with + match cast env tyop v1, cast env tyop v2 with | I n1, I n2 -> I (Int64.add n1 n2) | _, _ -> raise Notconst end else raise Notconst | Osub -> if is_arith_type env ty1 && is_arith_type env ty2 then begin - match cast env tyop ty1 v1, cast env tyop ty2 v2 with + match cast env tyop v1, cast env tyop v2 with | I n1, I n2 -> I (Int64.sub n1 n2) | _, _ -> raise Notconst end else raise Notconst | Omul -> - begin match cast env tyop ty1 v1, cast env tyop ty2 v2 with + begin match cast env tyop v1, cast env tyop v2 with | I n1, I n2 -> I (Int64.mul n1 n2) | _, _ -> raise Notconst end | Odiv -> - begin match cast env tyop ty1 v1, cast env tyop ty2 v2 with + begin match cast env tyop v1, cast env tyop v2 with | I n1, I n2 -> if n2 = 0L then raise Notconst else if is_signed env tyop then I (Int64.div n1 n2) @@ -206,17 +206,17 @@ let binop env op tyop tyres ty1 v1 ty2 v2 = | _, _ -> raise Notconst end | Oeq -> - comparison env (=) (Some false) tyop ty1 v1 ty2 v2 + comparison env (=) (Some false) tyop v1 v2 | One -> - comparison env (<>) (Some true) tyop ty1 v1 ty2 v2 + comparison env (<>) (Some true) tyop v1 v2 | Olt -> - comparison env (<) None tyop ty1 v1 ty2 v2 + comparison env (<) None tyop v1 v2 | Ogt -> - comparison env (>) None tyop ty1 v1 ty2 v2 + comparison env (>) None tyop v1 v2 | Ole -> - comparison env (<=) None tyop ty1 v1 ty2 v2 + comparison env (<=) None tyop v1 v2 | Oge -> - comparison env (>=) None tyop ty1 v1 ty2 v2 + comparison env (>=) None tyop v1 v2 | Ocomma -> v2 | Ologand -> @@ -229,7 +229,7 @@ let binop env op tyop tyres ty1 v1 ty2 v2 = else if boolean_value v2 then I 1L else I 0L | _ -> raise Notconst (* force normalization of result, e.g. of double to float *) - in cast env tyres tyres res + in cast env tyres res let rec expr env e = match e.edesc with @@ -253,11 +253,10 @@ let rec expr env e = binop env op ty e.etyp e1.etyp (expr env e1) e2.etyp (expr env e2) | EConditional(e1, e2, e3) -> if boolean_value (expr env e1) - then cast env e.etyp e2.etyp (expr env e2) - else cast env e.etyp e3.etyp (expr env e3) - (* | ECast(TInt (_, _), EConst (CFloat (_, _))) -> TODO *) + then cast env e.etyp (expr env e2) + else cast env e.etyp (expr env e3) | ECast(ty, e1) -> - cast env ty e1.etyp (expr env e1) + cast env ty (expr env e1) | ECompound _ -> raise Notconst | ECall _ -> @@ -265,14 +264,14 @@ let rec expr env e = let integer_expr env e = try - match cast env (TInt(ILongLong, [])) e.etyp (expr env e) with + match cast env (TInt(ILongLong, [])) (expr env e) with | I n -> Some n | _ -> None with Notconst -> None let constant_expr env ty e = try - match unroll env ty, cast env ty e.etyp (expr env e) with + match unroll env ty, cast env ty (expr env e) with | TInt(ik, _), I n -> Some(CInt(n, ik, "")) | TPtr(_, _), I n -> Some(CInt(n, IInt, "")) | TPtr(_, _), S s -> Some(CStr s) diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index c15a7adf..1bbb8e98 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -15,7 +15,6 @@ (* Operations on C types and abstract syntax *) -open Printf open Cerrors open C open Env @@ -194,7 +193,7 @@ let strip_attributes_type t attr = (* Remove the last attribute from the toplevel and return the changed type *) let strip_last_attribute typ = - let rec hd_opt l = match l with + let hd_opt l = match l with [] -> None,[] | a::rest -> Some a,rest in match typ with @@ -561,7 +560,7 @@ let incomplete_type env t = (* Computing composite_info records *) -let composite_info_decl env su attr = +let composite_info_decl su attr = { ci_kind = su; ci_members = []; ci_alignof = None; ci_sizeof = None; ci_attr = attr } @@ -892,7 +891,7 @@ let is_literal_0 e = let is_debug_stmt s = let is_debug_call = function - | (ECall ({edesc = EVar id; _},_)) -> id.name = "__builtin_debug" + | (ECall ({edesc = EVar id; _},_)) -> id.C.name = "__builtin_debug" | _ -> false in match s.sdesc with | Sdo {edesc = e;_} -> diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index b353cba3..3dcfe4aa 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -102,13 +102,11 @@ val sizeof_ikind: ikind -> int (* Return the size of the given integer kind. *) val sizeof_fkind: fkind -> int (* Return the size of the given float kind. *) -val is_signed_ikind: ikind -> bool - (* Return true if the given integer kind is signed, false if unsigned. *) (* Computing composite_info records *) val composite_info_decl: - Env.t -> struct_or_union -> attributes -> Env.composite_info + struct_or_union -> attributes -> Env.composite_info val composite_info_def: Env.t -> struct_or_union -> attributes -> field list -> Env.composite_info val struct_layout: diff --git a/cparser/Elab.ml b/cparser/Elab.ml index d7a1212a..130f37cd 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -19,9 +19,9 @@ open Format open Machine -open Cabs +open !Cabs open Cabshelper -open C +open !C open Cutil open Env @@ -203,7 +203,7 @@ let elab_int_constant loc s0 = in (v, ty) -let elab_float_constant loc f = +let elab_float_constant f = let ty = match f.suffix_FI with | Some ("l"|"L") -> FLongDouble | Some ("f"|"F") -> FFloat @@ -253,11 +253,11 @@ let elab_string_literal loc wide chars = if wide then CWStr chars else begin - let res = String.create (List.length chars) in + let res = Bytes.create (List.length chars) in List.iteri - (fun i c -> res.[i] <- Char.unsafe_chr (Int64.to_int c)) + (fun i c -> Bytes.set res i (Char.unsafe_chr (Int64.to_int c))) chars; - CStr res + CStr (Bytes.to_string res) end let elab_constant loc = function @@ -265,7 +265,7 @@ let elab_constant loc = function let (v, ik) = elab_int_constant loc s in CInt(v, ik, s) | CONST_FLOAT f -> - let (v, fk) = elab_float_constant loc f in + let (v, fk) = elab_float_constant f in CFloat(v, fk) | CONST_CHAR(wide, s) -> CInt(elab_char_constant loc wide s, IInt, "") @@ -319,7 +319,7 @@ let elab_gcc_attr loc env = function warning loc "cannot parse '%s' attribute, ignored" v; [] end -let is_power_of_two n = n > 0L && Int64.(logand n (pred n)) = 0L +let is_power_of_two n = n > 0L && Int64.logand n (Int64.pred n) = 0L let extract_alignas loc a = match a with @@ -569,7 +569,7 @@ and elab_parameters env params = let (vars, _) = mmap elab_parameter (Env.new_scope env) params in (* Catch special case f(t) where t is void or a typedef to void *) match vars with - | [ ( {name=""}, t) ] when is_void_type env t -> [] + | [ ( {C.name=""}, t) ] when is_void_type env t -> [] | _ -> vars (* Elaboration of a function parameter *) @@ -578,7 +578,7 @@ 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 false decl in + let ((ty, _), _) = elab_type_declarator loc env1 bty false decl in let ty = add_attributes_type (elab_attributes env attr) ty in if sto <> Storage_default && sto <> Storage_register then error loc @@ -753,7 +753,7 @@ and elab_struct_or_union only kind loc tag optmembers attrs env = (* declaration of an incomplete struct or union *) if tag = "" then error loc "anonymous, incomplete struct or union"; - let ci = composite_info_decl env kind attrs in + let ci = composite_info_decl kind attrs in (* enter it with a new name *) let (tag', env') = Env.enter_composite env tag ci in (* emit it *) @@ -761,7 +761,7 @@ and elab_struct_or_union only kind loc tag optmembers attrs env = (tag', env') | _, Some members -> (* definition of a complete struct or union *) - let ci1 = composite_info_decl env kind attrs in + let ci1 = composite_info_decl kind attrs in (* 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 *) @@ -900,8 +900,6 @@ module I = struct * ident (* union type *) * field (* current member *) - type state = zipinit * init (* current point & init for this point *) - (* The initial state: default initialization, current point at top *) let top env name ty = (Ztop(name, ty), default_init env ty) @@ -1727,7 +1725,7 @@ let elab_expr loc env a = | (TInt _ | TEnum _), TPtr _ -> warning "comparison between integer and pointer"; EBinop(op, b1, b2, TPtr(TVoid [], [])) - | ty1, ty2 -> + | _, _ -> error "illegal comparison between types@ %a@ and %a" Cprint.typ b1.etyp Cprint.typ b2.etyp in { edesc = resdesc; etyp = TInt(IInt, []) } @@ -1860,7 +1858,7 @@ let enter_decdefs local loc env sto dl = fatal_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) = + let enter_decdef (decls, env) (s, ty, init) = let isfun = is_function_type env ty in if sto = Storage_extern && init <> NO_INIT then error loc "'extern' declaration cannot have an initializer"; @@ -1936,7 +1934,7 @@ let elab_fundef env spec name defs body loc = "Illegal declaration of function parameter" in let (kr_params_defs, env1) = mmap elab_kr_param_def env1 defs in let kr_params_defs = List.concat kr_params_defs in - let rec search_param_type param = + let search_param_type param = match List.filter (fun (p, _) -> p = param) kr_params_defs with | [] -> (* Parameter is not declared, defaults to "int" in ISO C90, @@ -1960,7 +1958,7 @@ let elab_fundef env spec name defs body loc = (ty_ret, params, vararg, attr) | _ -> fatal_error loc "wrong type for function definition" in (* Enter function in the environment, for recursive references *) - let (fun_id, sto1, env1,ty) = enter_or_refine_ident false loc env1 s sto ty in + let (fun_id, sto1, env1, _) = enter_or_refine_ident false loc env1 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) diff --git a/cparser/Env.ml b/cparser/Env.ml index 65df6cb9..dae79ef2 100644 --- a/cparser/Env.ml +++ b/cparser/Env.ml @@ -118,12 +118,6 @@ let lookup_ident env s = with Not_found -> raise(Error(Unbound_identifier s)) -let lookup_tag env s = - try - IdentMap.lookup s env.env_tag - with Not_found -> - raise(Error(Unbound_tag(s, "tag"))) - let lookup_struct env s = try let (id, ci as res) = IdentMap.lookup s env.env_tag in @@ -169,11 +163,6 @@ let find_ident env id = with Not_found -> raise(Error(Unbound_identifier(id.name))) -let find_tag env id = - try IdentMap.find id env.env_tag - with Not_found -> - raise(Error(Unbound_tag(id.name, "tag"))) - let find_struct env id = try let ci = IdentMap.find id env.env_tag in diff --git a/cparser/ExtendedAsm.ml b/cparser/ExtendedAsm.ml index 94fcda31..c3d80272 100644 --- a/cparser/ExtendedAsm.ml +++ b/cparser/ExtendedAsm.ml @@ -33,7 +33,6 @@ open Printf open Machine open C open Cutil -open Env open Cerrors (* Renaming of labeled and numbered operands *) diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll index bcf2ada0..871f2bf9 100644 --- a/cparser/Lexer.mll +++ b/cparser/Lexer.mll @@ -17,8 +17,7 @@ open Lexing open Pre_parser open Pre_parser_aux -open Cabshelper -open Camlcoq +open !Cabshelper module SSet = Set.Make(String) @@ -430,7 +429,7 @@ and singleline_comment = parse open Streams open Specif open Parser - open Aut.GramDefs + open !Aut.GramDefs (* This is the main entry point to the lexer. *) diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml index 6ea5d121..aafa1caa 100644 --- a/cparser/PackedStructs.ml +++ b/cparser/PackedStructs.ml @@ -127,7 +127,7 @@ let transf_composite loc env su id attrs ml = (* Accessor functions *) -let lookup_function loc env name = +let lookup_function env name = match Env.lookup_ident env name with | (id, II_ident(sto, ty)) -> (id, ty) | (id, II_enum _) -> raise (Env.Error(Env.Unbound_identifier name)) @@ -161,14 +161,14 @@ let bswap_read loc env lval = try if !use_reversed then begin let (id, fty) = - lookup_function loc env (sprintf "__builtin_read%d_reversed" bsize) in + lookup_function env (sprintf "__builtin_read%d_reversed" bsize) in let fn = {edesc = EVar id; etyp = fty} in let args = [ecast_opt env (TPtr(aty,[])) (eaddrof lval)] in let call = {edesc = ECall(fn, args); etyp = aty} in ecast_opt env ty call end else begin let (id, fty) = - lookup_function loc env (sprintf "__builtin_bswap%d" bsize) in + lookup_function env (sprintf "__builtin_bswap%d" bsize) in let fn = {edesc = EVar id; etyp = fty} in let args = [ecast_opt env aty lval] in let call = {edesc = ECall(fn, args); etyp = aty} in @@ -188,14 +188,14 @@ let bswap_write loc env lhs rhs = try if !use_reversed then begin let (id, fty) = - lookup_function loc env (sprintf "__builtin_write%d_reversed" bsize) in + lookup_function env (sprintf "__builtin_write%d_reversed" bsize) in let fn = {edesc = EVar id; etyp = fty} in let args = [ecast_opt env (TPtr(aty,[])) (eaddrof lhs); ecast_opt env aty rhs] in {edesc = ECall(fn, args); etyp = TVoid[]} end else begin let (id, fty) = - lookup_function loc env (sprintf "__builtin_bswap%d" bsize) in + lookup_function env (sprintf "__builtin_bswap%d" bsize) in let fn = {edesc = EVar id; etyp = fty} in let args = [ecast_opt env aty rhs] in let call = {edesc = ECall(fn, args); etyp = aty} in @@ -403,7 +403,7 @@ let rec transf_globdecls env accu = function | Union -> attr | Struct -> remove_custom_attributes ["packed";"__packed__"] attr in transf_globdecls - (Env.add_composite env id (composite_info_decl env su attr')) + (Env.add_composite env id (composite_info_decl su attr')) ({g with gdesc = Gcompositedecl(su, id, attr')} :: accu) gl | Gcompositedef(su, id, attr, fl) -> diff --git a/cparser/StructReturn.ml b/cparser/StructReturn.ml index 4e019380..04f0021a 100644 --- a/cparser/StructReturn.ml +++ b/cparser/StructReturn.ml @@ -19,7 +19,7 @@ open Machine open Configuration -open C +open !C open Cutil open Transform diff --git a/cparser/Transform.ml b/cparser/Transform.ml index 840234b8..0a2ce3bb 100644 --- a/cparser/Transform.ml +++ b/cparser/Transform.ml @@ -45,7 +45,7 @@ let new_temp ?(name = "t") ty = let attributes_to_remove_from_temp = add_attributes [AConst] [AVolatile] -let mk_temp env ?(name = "t") ty = +let mk_temp env ty = new_temp (remove_attributes_type env attributes_to_remove_from_temp ty) (* Bind a l-value to a temporary variable if it is not invariant. *) @@ -211,7 +211,7 @@ let program Env.add_ident env f.fd_name f.fd_storage (fundef_typ f)) | Gcompositedecl(su, id, attr) -> (Gcompositedecl(su, id, attr), - Env.add_composite env id (composite_info_decl env su attr)) + Env.add_composite env id (composite_info_decl su attr)) | Gcompositedef(su, id, attr, fl) -> let (attr', fl') = composite env su id attr fl in (Gcompositedef(su, id, attr', fl'), diff --git a/cparser/Transform.mli b/cparser/Transform.mli index a04896a9..dbd8e575 100644 --- a/cparser/Transform.mli +++ b/cparser/Transform.mli @@ -18,7 +18,7 @@ val reset_temps : unit -> unit val get_temps : unit -> C.decl list val new_temp_var : ?name:string -> C.typ -> C.ident val new_temp : ?name:string -> C.typ -> C.exp -val mk_temp : Env.t -> ?name:string -> C.typ -> C.exp +val mk_temp : Env.t -> C.typ -> C.exp (** Avoiding repeated evaluation of a l-value *) diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml index ef8bc91c..0669be6e 100644 --- a/cparser/Unblock.ml +++ b/cparser/Unblock.ml @@ -64,17 +64,6 @@ let add_inits_stmt loc inits s = (fun e s -> sseq loc {sdesc = Sdo e; sloc = loc} s) inits s -(* Prepend assignments to the given expression. *) -(* Associate to the left so that it prints more nicely *) - -let add_inits_expr inits e = - match inits with - | [] -> e - | i1 :: il -> - let comma a b = - { edesc = EBinop(Ocomma, a, b, b.etyp); etyp = b.etyp } in - comma (List.fold_left comma i1 il) e - (* Record new variables to be locally or globally defined *) let local_variables = ref ([]: decl list) @@ -357,7 +346,7 @@ let unblock_fundef env f = (* Simplification of compound literals within a top-level declaration *) -let unblock_decl loc env ((sto, id, ty, optinit) as d) = +let unblock_decl env ((sto, id, ty, optinit) as d) = match optinit with | None -> [d] | Some init -> @@ -375,8 +364,8 @@ let rec unblock_glob env accu = function | [] -> List.rev accu | g :: gl -> match g.gdesc with - | Gdecl((sto, id, ty, init) as d) -> - let dl = unblock_decl g.gloc env d in + | Gdecl d -> + let dl = unblock_decl env d in unblock_glob env (List.rev_append (List.map (fun d' -> {g with gdesc = Gdecl d'}) dl) @@ -387,7 +376,7 @@ let rec unblock_glob env accu = function unblock_glob env ({g with gdesc = Gfundef f'} :: accu) gl | Gcompositedecl(su, id, attr) -> unblock_glob - (Env.add_composite env id (composite_info_decl env su attr)) + (Env.add_composite env id (composite_info_decl su attr)) (g :: accu) gl | Gcompositedef(su, id, attr, fl) -> unblock_glob |