diff options
| -rw-r--r-- | Changelog | 3 | ||||
| -rw-r--r-- | arm/PrintAsm.ml | 4 | ||||
| -rw-r--r-- | cfrontend/C2C.ml | 23 | ||||
| -rw-r--r-- | cfrontend/Cexec.v | 7 | ||||
| -rw-r--r-- | common/AST.v | 10 | ||||
| -rw-r--r-- | common/Events.v | 2 | ||||
| -rw-r--r-- | common/PrintAST.ml | 1 | ||||
| -rw-r--r-- | cparser/Bitfields.ml | 24 | ||||
| -rw-r--r-- | cparser/C.mli | 9 | ||||
| -rw-r--r-- | cparser/Ceval.ml | 4 | ||||
| -rw-r--r-- | cparser/Cleanup.ml | 11 | ||||
| -rw-r--r-- | cparser/Cprint.ml | 12 | ||||
| -rw-r--r-- | cparser/Cutil.ml | 50 | ||||
| -rw-r--r-- | cparser/Cutil.mli | 3 | ||||
| -rw-r--r-- | cparser/Elab.ml | 76 | ||||
| -rw-r--r-- | cparser/Env.ml | 38 | ||||
| -rw-r--r-- | cparser/Env.mli | 11 | ||||
| -rw-r--r-- | cparser/PackedStructs.ml | 4 | ||||
| -rw-r--r-- | cparser/Rename.ml | 10 | ||||
| -rw-r--r-- | cparser/StructReturn.ml | 1 | ||||
| -rw-r--r-- | cparser/Transform.ml | 9 | ||||
| -rw-r--r-- | cparser/Transform.mli | 6 | ||||
| -rw-r--r-- | cparser/Unblock.ml | 1 | ||||
| -rw-r--r-- | driver/Clflags.ml | 1 | ||||
| -rw-r--r-- | driver/Driver.ml | 5 | ||||
| -rw-r--r-- | ia32/PrintAsm.ml | 4 | ||||
| -rw-r--r-- | powerpc/PrintAsm.ml | 4 | ||||
| -rw-r--r-- | test/regression/Makefile | 2 |
28 files changed, 259 insertions, 76 deletions
@@ -10,6 +10,9 @@ Language semantics: - Comparison between function pointers is now correctly defined in the semantics of CompCert C (it was previously undefined behavior, by mistake). +- Bit-fields of 'enum' type are now treated as either unsigned or signed, + whichever is able to represent all values of the enum. + (Previously: always signed.) - The "&&" and "||" operators are now primitive in CompCert C and are given explicit semantic rules, instead of being expressed in terms of "_ ? _ : _" as in previous CompCert releases. diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 60d0fa4..0cee786 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -637,6 +637,10 @@ let print_instruction oc = function (Int32.to_int (camlint_of_coqint al)) args | EF_annot_val(txt, targ) -> print_annot_val oc (extern_atom txt) args res + | EF_inline_asm txt -> + fprintf oc "%s begin inline assembly\n" comment; + fprintf oc " %s\n" (extern_atom txt); + fprintf oc "%s end inline assembly\n" comment | _ -> assert false end diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 2cdcc03..aa9eca0 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -293,6 +293,9 @@ let convertTyp env t = with Env.Error e -> error (Env.error_message e); Fnil in Tunion(intern_string("union " ^ id.name), flds, convertAttr a) + | C.TEnum(id, a) -> + let (sg, sz) = convertIkind Cutil.enum_ikind in + Tint(sz, sg, convertAttr a) and convertParams seen = function | [] -> Tnil @@ -332,6 +335,12 @@ let first_class_value env ty = | C.TInt((C.ILongLong|C.IULongLong), _) -> false | _ -> true +let supported_return_type env ty = + match Cutil.unroll env ty with + | C.TInt((C.ILongLong|C.IULongLong), _) -> false + | C.TStruct _ | C.TUnion _ -> false + | _ -> true + (** Floating point constants *) let z_of_str hex str fst = @@ -499,6 +508,8 @@ let rec convertExpr env e = | C.EConditional(e1, e2, e3) -> Econdition(convertExpr env e1, convertExpr env e2, convertExpr env e3, ty) | C.ECast(ty1, e1) -> + if not (first_class_value env ty1) then + unsupported ("cast to type " ^ string_of_type ty1); Ecast(convertExpr env e1, convertTyp env ty1) | C.ECall({edesc = C.EVar {name = "__builtin_annot"}}, args) -> @@ -527,6 +538,8 @@ let rec convertExpr env e = make_builtin_memcpy (convertExprList env args) | C.ECall(fn, args) -> + if not (supported_return_type env e.etyp) then + unsupported ("function returning a result of type " ^ string_of_type e.etyp); match projFunType env fn.etyp with | None -> error "wrong type for function part of a call"; ezero @@ -660,6 +673,10 @@ let rec convertStmt env s = unsupported "nested blocks"; Sskip | C.Sdecl _ -> unsupported "inner declarations"; Sskip + | C.Sasm txt -> + if not !Clflags.option_finline_asm then + unsupported "inline 'asm' statement (consider adding option -finline-asm)"; + Sdo (Ebuiltin (EF_inline_asm (intern_string txt), Tnil, Enil, Tvoid)) and convertSwitch env = function | [] -> @@ -820,7 +837,7 @@ let rec convertGlobdecls env res gl = | TFun(_, Some _, false, _) -> convertGlobdecls env (convertFundecl env d :: res) gl' | TFun(_, None, false, _) -> - error "function declaration without prototype"; + error ("'" ^ id.name ^ "' is declared without a function prototype"); convertGlobdecls env res gl' | TFun(_, _, true, _) -> convertGlobdecls env res gl' @@ -842,7 +859,7 @@ let rec convertGlobdecls env res gl = warning ("'#pragma " ^ s ^ "' directive ignored"); convertGlobdecls env res gl' -(** Build environment of typedefs and structs *) +(** Build environment of typedefs, structs, unions and enums *) let rec translEnv env = function | [] -> env @@ -855,6 +872,8 @@ let rec translEnv env = function Env.add_composite env id (Cutil.composite_info_def env su attr fld) | C.Gtypedef(id, ty) -> Env.add_typedef env id ty + | C.Genumdef(id, attr, members) -> + Env.add_enum env id {ei_members = members; ei_attr = attr} | _ -> env in translEnv env' gl diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index b6ea1e0..c768118 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -506,6 +506,7 @@ Definition do_external (ef: external_function): | EF_memcpy sz al => do_ef_memcpy sz al | EF_annot text targs => do_ef_annot text targs | EF_annot_val text targ => do_ef_annot_val text targ + | EF_inline_asm text => do_ef_annot text nil end. Lemma do_ef_external_sound: @@ -575,6 +576,10 @@ Proof with try congruence. unfold do_ef_annot_val. destruct vargs... destruct vargs... mydestr. split. constructor. apply eventval_of_val_sound; auto. econstructor. constructor; eauto. constructor. +(* EF_inline_asm *) + unfold do_ef_annot. destruct vargs; simpl... mydestr. + split. constructor. constructor. + econstructor. constructor; eauto. constructor. Qed. Lemma do_ef_external_complete: @@ -633,6 +638,8 @@ Proof. (* EF_annot_val *) inv H; unfold do_ef_annot_val. inv H0. inv H6. inv H4. rewrite (eventval_of_val_complete _ _ _ H1). auto. +(* EF_inline_asm *) + inv H; unfold do_ef_annot. inv H0. inv H6. inv H4. inv H1. simpl. auto. Qed. (** * Reduction of expressions *) diff --git a/common/AST.v b/common/AST.v index ccc9dbf..40da732 100644 --- a/common/AST.v +++ b/common/AST.v @@ -447,10 +447,16 @@ Inductive external_function : Type := (** A programmer-supplied annotation. Takes zero, one or several arguments, produces an event carrying the text and the values of these arguments, and returns no value. *) - | EF_annot_val (text:ident) (targ: typ). + | EF_annot_val (text: ident) (targ: typ) (** Another form of annotation that takes one argument, produces an event carrying the text and the value of this argument, and returns the value of the argument. *) + | EF_inline_asm (text: ident). + (** Inline [asm] statements. Semantically, treated like an + annotation with no parameters ([EF_annot text nil]). To be + used with caution, as it can invalidate the semantic + preservation theorem. Generated only if [-finline-asm] is + given. *) (** The type signature of an external function. *) @@ -467,6 +473,7 @@ Definition ef_sig (ef: external_function): signature := | EF_memcpy sz al => mksignature (Tint :: Tint :: nil) None | EF_annot text targs => mksignature targs None | EF_annot_val text targ => mksignature (targ :: nil) (Some targ) + | EF_inline_asm text => mksignature nil None end. (** Whether an external function should be inlined by the compiler. *) @@ -484,6 +491,7 @@ Definition ef_inline (ef: external_function) : bool := | EF_memcpy sz al => true | EF_annot text targs => true | EF_annot_val text targ => true + | EF_inline_asm text => true end. (** Whether an external function must reload its arguments. *) diff --git a/common/Events.v b/common/Events.v index b36a86f..fd1acd0 100644 --- a/common/Events.v +++ b/common/Events.v @@ -1582,6 +1582,7 @@ Definition external_call (ef: external_function): extcall_sem := | EF_memcpy sz al => extcall_memcpy_sem sz al | EF_annot txt targs => extcall_annot_sem txt targs | EF_annot_val txt targ=> extcall_annot_val_sem txt targ + | EF_inline_asm txt => extcall_annot_sem txt nil end. Theorem external_call_spec: @@ -1600,6 +1601,7 @@ Proof. apply extcall_memcpy_ok. apply extcall_annot_ok. apply extcall_annot_val_ok. + apply extcall_annot_ok. Qed. Definition external_call_well_typed ef := ec_well_typed (external_call_spec ef). diff --git a/common/PrintAST.ml b/common/PrintAST.ml index 971bf77..6a66c30 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -45,3 +45,4 @@ let name_of_external = function sprintf "memcpy size %ld align %ld " (camlint_of_z sz) (camlint_of_z al) | EF_annot(text, targs) -> sprintf "annot %S" (extern_atom text) | EF_annot_val(text, targ) -> sprintf "annot_val %S" (extern_atom text) + | EF_inline_asm text -> sprintf "inline_asm %S" (extern_atom text) diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml index 257f6c8..937a61f 100644 --- a/cparser/Bitfields.ml +++ b/cparser/Bitfields.ml @@ -46,7 +46,7 @@ type bitfield_info = let bitfield_table = (Hashtbl.create 57: (ident * string, bitfield_info) Hashtbl.t) -(* Packing algorithm -- keep consistent with [Cutil.pack_bitfield]! *) +(* Signedness issues *) let unsigned_ikind_for_carrier nbits = if nbits <= 8 then IUChar else @@ -56,7 +56,26 @@ let unsigned_ikind_for_carrier nbits = if nbits <= 8 * !config.sizeof_longlong then IULongLong else assert false -let pack_bitfields env id ml = +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 + then false + 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; + false + end + +(* Packing algorithm -- keep consistent with [Cutil.pack_bitfield]! *) + +let pack_bitfields env sid ml = let rec pack accu pos = function | [] -> (pos, accu, []) @@ -72,6 +91,7 @@ let pack_bitfields env id ml = 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 diff --git a/cparser/C.mli b/cparser/C.mli index 8e73bc5..ce58504 100644 --- a/cparser/C.mli +++ b/cparser/C.mli @@ -150,6 +150,7 @@ type typ = | TNamed of ident * attributes | TStruct of ident * attributes | TUnion of ident * attributes + | TEnum of ident * attributes (** Expressions *) @@ -187,6 +188,7 @@ and stmt_desc = | Sreturn of exp option | Sblock of stmt list | Sdecl of decl + | Sasm of string and slabel = | Slabel of string @@ -218,6 +220,10 @@ type struct_or_union = | Struct | Union +(** Enumerator *) + +type enumerator = ident * int64 * exp option + (** Function definitions *) type fundef = { @@ -244,7 +250,8 @@ and globdecl_desc = | Gcompositedef of struct_or_union * ident * attributes * field list (* struct/union definition *) | Gtypedef of ident * typ (* typedef *) - | Genumdef of ident * (ident * exp option) list (* enum definition *) + | Genumdef of ident * attributes * enumerator list + (* enum definition *) | Gpragma of string (* #pragma directive *) type program = globdecl list diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml index 621fbbf..5770e27 100644 --- a/cparser/Ceval.ml +++ b/cparser/Ceval.ml @@ -71,6 +71,7 @@ let constant = function let is_signed env ty = match unroll env ty with | TInt(ik, _) -> is_signed_ikind ik + | TEnum(_, _) -> is_signed_ikind enum_ikind | _ -> false let cast env ty_to ty_from v = @@ -87,6 +88,8 @@ let cast env ty_to ty_from v = I (normalize_int n ptr_t_ikind) | TPtr(ty, _), (S _ | WS _) -> v + | TEnum(_, _), I n -> + I (normalize_int n enum_ikind) | _, _ -> raise Notconst @@ -255,5 +258,6 @@ let constant_expr env ty e = | TPtr(_, _), I 0L -> Some(CInt(0L, IInt, "")) | TPtr(_, _), S s -> Some(CStr s) | TPtr(_, _), WS s -> Some(CWStr s) + | TEnum(_, _), I n -> Some(CInt(n, enum_ikind, "")) | _ -> None with Notconst -> None diff --git a/cparser/Cleanup.ml b/cparser/Cleanup.ml index 54dfd67..00ff662 100644 --- a/cparser/Cleanup.ml +++ b/cparser/Cleanup.ml @@ -47,6 +47,7 @@ let rec add_typ = function | TNamed(id, _) -> addref id | TStruct(id, _) -> addref id | TUnion(id, _) -> addref id + | TEnum(id, _) -> addref id | _ -> () and add_vars vl = @@ -96,6 +97,7 @@ let rec add_stmt s = | Sreturn(Some e) -> add_exp e | Sblock sl -> List.iter add_stmt sl | Sdecl d -> add_decl d + | Sasm _ -> () let add_fundef f = add_typ f.fd_ret; @@ -107,7 +109,7 @@ let add_field f = add_typ f.fld_typ let add_enum e = List.iter - (fun (id, opt_e) -> match opt_e with Some e -> add_exp e | None -> ()) + (fun (id, v, opt_e) -> match opt_e with Some e -> add_exp e | None -> ()) e (* Saturate the set of referenced identifiers, starting with externally @@ -152,8 +154,8 @@ let rec add_needed_globdecls accu = function if needed id then (add_typ ty; add_needed_globdecls accu rem) else add_needed_globdecls (g :: accu) rem - | Genumdef(id, enu) -> - if List.exists (fun (id, _) -> needed id) enu + | Genumdef(id, _, enu) -> + if needed id || List.exists (fun (id, _, _) -> needed id) enu then (add_enum enu; add_needed_globdecls accu rem) else add_needed_globdecls (g :: accu) rem | _ -> @@ -180,7 +182,8 @@ let rec simpl_globdecls accu = function | Gcompositedecl(_, id, _) -> needed id | Gcompositedef(_, id, _, flds) -> needed id | Gtypedef(id, ty) -> needed id - | Genumdef(id, enu) -> List.exists (fun (id, _) -> needed id) enu + | Genumdef(id, _, enu) -> + needed id || List.exists (fun (id, _, _) -> needed id) enu | Gpragma s -> true in if need then simpl_globdecls (g :: accu) rem diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml index 2548f3b..e97f041 100644 --- a/cparser/Cprint.ml +++ b/cparser/Cprint.ml @@ -172,6 +172,8 @@ let rec dcl pp ty n = fprintf pp "struct %a%a%t" ident id attributes a n | TUnion(id, a) -> fprintf pp "union %a%a%t" ident id attributes a n + | TEnum(id, a) -> + fprintf pp "enum %a%a%t" ident id attributes a n let typ pp ty = dcl pp ty (fun _ -> ()) @@ -424,6 +426,8 @@ let rec stmt pp s = fprintf pp "@[<v 2>{@ %a@;<0 -2>}@]" stmt_block s | Sdecl d -> full_decl pp d + | Sasm txt -> + fprintf pp "asm(%a);" const (CStr txt) and slabel pp = function | Slabel s -> @@ -486,17 +490,17 @@ let globdecl pp g = fprintf pp "@;<0 -2>};@]@ @ " | Gtypedef(id, ty) -> fprintf pp "@[<hov 2>typedef %a;@]@ @ " simple_decl (id, ty) - | Genumdef(id, fields) -> - fprintf pp "@[<v 2>enum %a {" ident id; + | Genumdef(id, attrs, vals) -> + fprintf pp "@[<v 2>enum%a %a {" attributes attrs ident id; List.iter - (fun (name, opt_e) -> + (fun (name, v, opt_e) -> fprintf pp "@ %a" ident name; begin match opt_e with | None -> () | Some e -> fprintf pp " = %a" exp (0, e) end; fprintf pp ",") - fields; + vals; fprintf pp "@;<0 -2>};@]@ @ " | Gpragma s -> fprintf pp "#pragma %s@ @ " s diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index d84b9c9..212303a 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -86,6 +86,7 @@ a) | TNamed(s, a) -> TNamed(s, add_attributes attr a) | TStruct(s, a) -> TStruct(s, add_attributes attr a) | TUnion(s, a) -> TUnion(s, add_attributes attr a) + | TEnum(s, a) -> TEnum(s, add_attributes attr a) (* Unrolling of typedef *) @@ -111,6 +112,8 @@ let rec attributes_of_type env t = let ci = Env.find_struct env s in add_attributes ci.ci_attr a | TUnion(s, a) -> let ci = Env.find_union env s in add_attributes ci.ci_attr a + | TEnum(s, a) -> + let ei = Env.find_enum env s in add_attributes ei.ei_attr a (* Changing the attributes of a type (at top-level) *) (* Same hack as above for array types. *) @@ -130,6 +133,7 @@ let rec change_attributes_type env (f: attributes -> attributes) t = if t2 = t1 then t else t2 (* avoid useless expansion *) | TStruct(s, a) -> TStruct(s, f a) | TUnion(s, a) -> TUnion(s, f a) + | TEnum(s, a) -> TEnum(s, f a) let remove_attributes_type env attr t = change_attributes_type env (fun a -> remove_attributes a attr) t @@ -199,6 +203,8 @@ let combine_types ?(noattrs = false) env t1 t2 = TStruct(comp_base s1 s2, comp_attr a1 a2) | TUnion(s1, a1), TUnion(s2, a2) -> TUnion(comp_base s1 s2, comp_attr a1 a2) + | TEnum(s1, a1), TEnum(s2, a2) -> + TEnum(comp_base s1 s2, comp_attr a1 a2) | _, _ -> raise Incompat @@ -251,6 +257,8 @@ let alignof_fkind = function (* Return natural alignment of given type, or None if the type is incomplete *) +let enum_ikind = IInt + let rec alignof env t = match t with | TVoid _ -> !config.alignof_void @@ -264,6 +272,7 @@ let rec alignof env t = let ci = Env.find_struct env name in ci.ci_alignof | TUnion(name, _) -> let ci = Env.find_union env name in ci.ci_alignof + | TEnum(_, _) -> Some(alignof_ikind enum_ikind) (* Compute the natural alignment of a struct or union. *) @@ -330,6 +339,7 @@ let rec sizeof env t = let ci = Env.find_struct env name in ci.ci_sizeof | TUnion(name, _) -> let ci = Env.find_union env name in ci.ci_sizeof + | TEnum(_, _) -> Some(sizeof_ikind enum_ikind) (* Compute the size of a union. It is the size is the max of the sizes of fields, rounded up to the @@ -394,6 +404,15 @@ let composite_info_def env su attr m = end; ci_attr = attr } +(* Is an integer [v] representable in [n] bits, signed or unsigned? *) + +let int_representable v nbits sgn = + if nbits >= 64 then true else + if sgn then + let p = Int64.shift_left 1L (nbits - 1) in Int64.neg p <= v && v < p + else + 0L <= v && v < Int64.shift_left 1L nbits + (* Type of a function definition *) let fundef_typ fd = @@ -445,12 +464,14 @@ let is_void_type env t = let is_integer_type env t = match unroll env t with | TInt(_, _) -> true + | TEnum(_, _) -> true | _ -> false let is_arith_type env t = match unroll env t with | TInt(_, _) -> true | TFloat(_, _) -> true + | TEnum(_, _) -> true | _ -> false let is_pointer_type env t = @@ -465,6 +486,7 @@ let is_scalar_type env t = | TPtr _ -> true | TArray _ -> true (* assume implicit decay *) | TFun _ -> true (* assume implicit decay *) + | TEnum(_, _) -> true | _ -> false let is_composite_type env t = @@ -514,6 +536,8 @@ let unary_conversion env t = | IInt | IUInt | ILong | IULong | ILongLong | IULongLong -> TInt(kind, attr) end + (* Enums are like signed ints *) + | TEnum(id, attr) -> TInt(enum_ikind, attr) (* Arrays and functions decay automatically to pointers *) | TArray(ty, _, _) -> TPtr(ty, []) | TFun _ as ty -> TPtr(ty, []) @@ -593,13 +617,14 @@ let type_of_member env fld = match fld.fld_bitfield with | None -> fld.fld_typ | Some w -> - match unroll env fld.fld_typ with - | TInt(ik, attr) -> - if w < sizeof_ikind ik * 8 - then TInt(signed_ikind_of ik, attr) - else fld.fld_typ - | _ -> - assert false + let (ik, attr) = + match unroll env fld.fld_typ with + | TInt(ik, attr) -> (ik, attr) + | TEnum(_, attr) -> (enum_ikind, attr) + | _ -> assert false in + if w < sizeof_ikind ik * 8 + then TInt(signed_ikind_of ik, attr) + else fld.fld_typ (** Special types *) @@ -619,15 +644,14 @@ let wchar_ikind = find_matching_unsigned_ikind !config.sizeof_wchar let size_t_ikind = find_matching_unsigned_ikind !config.sizeof_size_t let ptr_t_ikind = find_matching_unsigned_ikind !config.sizeof_ptr let ptrdiff_t_ikind = find_matching_signed_ikind !config.sizeof_ptrdiff_t -let enum_ikind = IInt (** The type of a constant *) let type_of_constant = function | CInt(_, ik, _) -> TInt(ik, []) | CFloat(_, fk) -> TFloat(fk, []) - | CStr _ -> TPtr(TInt(IChar, []), []) (* XXX or array? const? *) - | CWStr _ -> TPtr(TInt(wchar_ikind, []), []) (* XXX or array? const? *) + | CStr _ -> TPtr(TInt(IChar, []), []) + | CWStr _ -> TPtr(TInt(wchar_ikind, []), []) | CEnum(_, _) -> TInt(IInt, []) (* Check that a C expression is a lvalue *) @@ -676,7 +700,7 @@ let valid_assignment_attr afrom ato = let valid_assignment env from tto = match pointer_decay env from.etyp, pointer_decay env tto with - | (TInt _ | TFloat _), (TInt _ | TFloat _) -> true + | (TInt _ | TFloat _ | TEnum _), (TInt _ | TFloat _ | TEnum _) -> true | TInt _, TPtr _ -> is_literal_0 from | TPtr(ty, _), TPtr(ty', _) -> valid_assignment_attr (attributes_of_type env ty) @@ -697,9 +721,9 @@ let valid_cast env tfrom tto = | _, TVoid _ -> true (* from any int-or-pointer (with array and functions decaying to pointers) to any int-or-pointer *) - | (TInt _ | TPtr _ | TArray _ | TFun _), (TInt _ | TPtr _) -> true + | (TInt _ | TPtr _ | TArray _ | TFun _ | TEnum _), (TInt _ | TPtr _ | TEnum _) -> true (* between int and float types *) - | (TInt _ | TFloat _), (TInt _ | TFloat _) -> true + | (TInt _ | TFloat _ | TEnum _), (TInt _ | TFloat _ | TEnum _) -> true | _, _ -> false end diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index 6488117..54b6304 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -160,6 +160,9 @@ val valid_cast : Env.t -> typ -> typ -> bool (* Check that a cast from the first type to the second is allowed. *) val fundef_typ: fundef -> typ (* Return the function type for the given function definition. *) +val int_representable: int64 -> int -> bool -> bool + (* Is the given int64 representable with the given number of bits and + signedness? *) (* Constructors *) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 0e7b549..6807d0c 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -425,10 +425,9 @@ let rec elab_specifier ?(only = false) loc env specifier = (!sto, !inline, TUnion(id', !attr), env') | [Cabs.Tenum(id, optmembers, a)] -> - let env' = - elab_enum loc id optmembers env in - let attr' = add_attributes !attr (elab_attributes loc env a) in - (!sto, !inline, TInt(enum_ikind, attr'), env') + let (id', env') = + elab_enum loc id optmembers a env in + (!sto, !inline, TEnum(id', !attr), env') | [Cabs.TtypeofE _] -> fatal_error loc "GCC __typeof__ not supported" @@ -549,28 +548,29 @@ and elab_field_group env (spec, fieldlist) = let ik = match unroll env' ty with | TInt(ik, _) -> ik + | TEnum(_, _) -> enum_ikind | _ -> ILongLong (* trigger next error message *) in if integer_rank ik > integer_rank IInt then error loc - "the type of a bit field must be an integer type \ - no bigger than 'int'"; + "the type of '%s' must be an integer type \ + no bigger than 'int'" id; match Ceval.integer_expr env' (!elab_expr_f loc env sz) with | Some n -> if n < 0L then begin - error loc "bit size of member %s (%Ld) is negative" id n; + error loc "bit size of '%s' (%Ld) is negative" id n; None end else if n > Int64.of_int(sizeof_ikind ik * 8) then begin - error loc "bit size of member %s (%Ld) is too large" id n; + error loc "bit size of '%s' (%Ld) exceeds its type" id n; None end else if n = 0L && id <> "" then begin - error loc "member %s has zero size" id; + error loc "member '%s' has zero size" id; None end else Some(Int64.to_int n) | None -> - error loc "bit size of member %s is not a compile-time constant" id; + error loc "bit size of '%s' is not a compile-time constant" id; None in { fld_name = id; fld_typ = ty; fld_bitfield = optbitsize' } in @@ -673,14 +673,21 @@ and elab_enum_item env (s, exp, loc) nextval = (nextval, Some exp') in if redef Env.lookup_ident env s <> None then error loc "redefinition of enumerator '%s'" s; + if not (int_representable v (8 * sizeof_ikind enum_ikind) (is_signed_ikind enum_ikind)) then + warning loc "the value of '%s' is not representable with type %a" + s Cprint.typ (TInt(enum_ikind, [])); let (id, env') = Env.enter_enum_item env s v in - ((id, exp'), Int64.succ v, env') + ((id, v, exp'), Int64.succ v, env') (* Elaboration of an enumeration declaration *) -and elab_enum loc tag optmembers env = +and elab_enum loc tag optmembers attrs env = + let attrs' = + elab_attributes loc env attrs in match optmembers with - | None -> env + | None -> + let (tag', info) = wrap Env.lookup_enum loc env tag in (tag', env) + (* XXX this will cause an error for incomplete enum definitions. *) | Some members -> let rec elab_members env nextval = function | [] -> ([], env) @@ -689,9 +696,10 @@ and elab_enum loc tag optmembers env = let (dcl2, env2) = elab_members env1 nextval1 tl in (dcl1 :: dcl2, env2) in let (dcls, env') = elab_members env 0L members in - let tag' = Env.fresh_ident tag in - emit_elab (elab_loc loc) (Genumdef(tag', dcls)); - env' + let info = { ei_members = dcls; ei_attr = attrs' } in + let (tag', env'') = Env.enter_enum env' tag info in + emit_elab (elab_loc loc) (Genumdef(tag', attrs', dcls)); + (tag', env'') (* Elaboration of a naked type, e.g. in a cast *) @@ -739,8 +747,8 @@ let elab_expr loc env a = let b1 = elab a1 in let b2 = elab a2 in let tres = match (unroll env b1.etyp, unroll env b2.etyp) with - | (TPtr(t, _) | TArray(t, _, _)), TInt _ -> t - | TInt _, (TPtr(t, _) | TArray(t, _, _)) -> t + | (TPtr(t, _) | TArray(t, _, _)), (TInt _ | TEnum _) -> t + | (TInt _ | TEnum _), (TPtr(t, _) | TArray(t, _, _)) -> t | t1, t2 -> error "incorrect types for array subscripting" in { edesc = EBinop(Oindex, b1, b2, TPtr(tres, [])); etyp = tres } @@ -801,6 +809,7 @@ let elab_expr loc env a = having declared it *) match a1 with | VARIABLE n when not (Env.ident_is_bound env n) -> + warning "implicit declaration of function '%s'" n; let ty = TFun(TInt(IInt, []), None, false, []) in (* Emit an extern declaration for it *) let id = Env.fresh_ident n in @@ -944,8 +953,8 @@ let elab_expr loc env a = else begin let (ty, attr) = match unroll env b1.etyp, unroll env b2.etyp with - | (TPtr(ty, a) | TArray(ty, _, a)), TInt _ -> (ty, a) - | TInt _, (TPtr(ty, a) | TArray(ty, _, a)) -> (ty, a) + | (TPtr(ty, a) | TArray(ty, _, a)), (TInt _ | TEnum _) -> (ty, a) + | (TInt _ | TEnum _), (TPtr(ty, a) | TArray(ty, _, a)) -> (ty, a) | _, _ -> error "type error in binary '+'" in if not (pointer_arithmetic_ok env ty) then err "illegal pointer arithmetic in binary '+'"; @@ -962,11 +971,11 @@ let elab_expr loc env a = (tyres, tyres) end else begin match unroll env b1.etyp, unroll env b2.etyp with - | (TPtr(ty, a) | TArray(ty, _, a)), TInt _ -> + | (TPtr(ty, a) | TArray(ty, _, a)), (TInt _ | TEnum _) -> if not (pointer_arithmetic_ok env ty) then err "illegal pointer arithmetic in binary '-'"; (TPtr(ty, a), TPtr(ty, a)) - | TInt _, (TPtr(ty, a) | TArray(ty, _, a)) -> + | (TInt _ | TEnum _), (TPtr(ty, a) | TArray(ty, _, a)) -> if not (pointer_arithmetic_ok env ty) then err "illegal pointer arithmetic in binary '-'"; (TPtr(ty, a), TPtr(ty, a)) @@ -1022,7 +1031,7 @@ let elab_expr loc env a = if not (is_scalar_type env b1.etyp) then err ("the first argument of '? :' is not a scalar type"); begin match pointer_decay env b2.etyp, pointer_decay env b3.etyp with - | (TInt _ | TFloat _), (TInt _ | TFloat _) -> + | (TInt _ | TFloat _ | TEnum _), (TInt _ | TFloat _ | TEnum _) -> { edesc = EConditional(b1, b2, b3); etyp = binary_conversion env b2.etyp b3.etyp } | TPtr(ty1, a1), TPtr(ty2, a2) -> @@ -1170,7 +1179,7 @@ let elab_expr loc env a = let b2 = elab a2 in let resdesc = match pointer_decay env b1.etyp, pointer_decay env b2.etyp with - | (TInt _ | TFloat _), (TInt _ | TFloat _) -> + | (TInt _ | TFloat _ | TEnum _), (TInt _ | TFloat _ | TEnum _) -> EBinop(op, b1, b2, binary_conversion env b1.etyp b2.etyp) | TInt _, TPtr(ty, _) when is_literal_0 b1 -> EBinop(op, nullconst, b2, TPtr(ty, [])) @@ -1186,8 +1195,8 @@ let elab_expr loc env a = if not (compatible_types ~noattrs:true env ty1 ty2) then warning "comparison between incompatible pointer types"; EBinop(op, b1, b2, TPtr(ty1, [])) - | TPtr _, TInt _ - | TInt _, TPtr _ -> + | TPtr _, (TInt _ | TEnum _) + | (TInt _ | TEnum _), TPtr _ -> warning "comparison between integer and pointer"; EBinop(op, b1, b2, TPtr(TVoid [], [])) | ty1, ty2 -> @@ -1374,7 +1383,7 @@ let rec elab_init loc env ty ile = let (i, rem) = elab_init loc env fld1.fld_typ ile in (Init_union(id, fld1, i), rem) end - | TInt _ | TFloat _ | TPtr _ -> + | TInt _ | TFloat _ | TPtr _ | TEnum _ -> begin match ile with (* scalar = elt *) | SINGLE_INIT a :: ile1 -> @@ -1384,7 +1393,7 @@ let rec elab_init loc env ty ile = (* scalar = nothing (within a bigger compound initializer) *) | (NO_INIT :: ile1) | ([] as ile1) -> begin match unroll env ty with - | TInt _ -> (Init_single (intconst 0L IInt), ile1) + | TInt _ | TEnum _ -> (Init_single (intconst 0L IInt), ile1) | TFloat _ -> (Init_single floatconst0, ile1) | TPtr _ -> (Init_single nullconst, ile1) | _ -> assert false @@ -1399,7 +1408,7 @@ let elab_initial loc env ty ie = match unroll env ty, ie with | _, NO_INIT -> None (* scalar or composite = expr *) - | (TInt _ | TFloat _ | TPtr _ | TStruct _ | TUnion _), SINGLE_INIT a -> + | (TInt _ | TFloat _ | TPtr _ | TStruct _ | TUnion _ | TEnum _), SINGLE_INIT a -> let a' = elab_expr loc env a in check_init_type loc env a' ty; Some (Init_single a') @@ -1777,6 +1786,12 @@ let rec elab_stmt env ctx s = | NOP loc -> { sdesc = Sskip; sloc = elab_loc loc } +(* Traditional extensions *) + | ASM(attr, txt, details, loc) -> + if details <> None then + error loc "GCC's extended 'asm' statements are not supported"; + { sdesc = Sasm(String.concat "" txt); sloc = elab_loc loc } + (* Unsupported *) | DEFINITION def -> error (get_definitionloc def) "ill-placed definition"; @@ -1784,9 +1799,6 @@ let rec elab_stmt env ctx s = | COMPGOTO(a, loc) -> error loc "GCC's computed 'goto' is not supported"; sskip - | ASM(_, _, _, loc) -> - error loc "'asm' statement is not supported"; - sskip | TRY_EXCEPT(_, _, _, loc) -> error loc "'try ... except' statement is not supported"; sskip diff --git a/cparser/Env.ml b/cparser/Env.ml index 164fe59..355a996 100644 --- a/cparser/Env.ml +++ b/cparser/Env.ml @@ -72,26 +72,35 @@ type composite_info = { type ident_info = | II_ident of storage * typ - | II_enum of int64 (* value of the enum *) + | II_enum of int64 (* value of enumerator *) (* Infos associated with a typedef *) type typedef_info = typ +(* Infos associated with an enum *) + +type enum_info = { + ei_members: enumerator list; (* list of all members *) + ei_attr: attributes (* attributes, if any *) +} + (* Environments *) type t = { env_scope: int; env_ident: ident_info IdentMap.t; env_tag: composite_info IdentMap.t; - env_typedef: typedef_info IdentMap.t + env_typedef: typedef_info IdentMap.t; + env_enum: enum_info IdentMap.t } let empty = { env_scope = 0; env_ident = IdentMap.empty; env_tag = IdentMap.empty; - env_typedef = IdentMap.empty + env_typedef = IdentMap.empty; + env_enum = IdentMap.empty } (* Enter a new scope. *) @@ -143,6 +152,12 @@ let lookup_typedef env s = with Not_found -> raise(Error(Unbound_typedef s)) +let lookup_enum env s = + try + IdentMap.lookup s env.env_enum + with Not_found -> + raise(Error(Unbound_tag(s, "enum"))) + (* Checking if a source name is bound *) let ident_is_bound env s = StringMap.mem s env.env_ident @@ -200,6 +215,12 @@ let find_typedef env id = with Not_found -> raise(Error(Unbound_typedef(id.name))) +let find_enum env id = + try + IdentMap.find id env.env_enum + with Not_found -> + raise(Error(Unbound_tag(id.name, "enum"))) + (* Inserting things by source name, with generation of a translated name *) let enter_ident env s sto ty = @@ -219,6 +240,10 @@ let enter_typedef env s info = let id = fresh_ident s in (id, { env with env_typedef = IdentMap.add id info env.env_typedef }) +let enter_enum env s info = + let id = fresh_ident s in + (id, { env with env_enum = IdentMap.add id info env.env_enum }) + (* Inserting things by translated name *) let add_ident env id sto ty = @@ -230,6 +255,13 @@ let add_composite env id ci = let add_typedef env id info = { env with env_typedef = IdentMap.add id info env.env_typedef } +let add_enum env id info = + let add_enum_item env (id, v, exp) = + { env with env_ident = IdentMap.add id (II_enum v) env.env_ident } in + List.fold_left add_enum_item + { env with env_enum = IdentMap.add id info env.env_enum } + info.ei_members + (* Error reporting *) open Printf diff --git a/cparser/Env.mli b/cparser/Env.mli index 01f95ca..b650f0f 100644 --- a/cparser/Env.mli +++ b/cparser/Env.mli @@ -36,6 +36,11 @@ type ident_info = II_ident of C.storage * C.typ | II_enum of int64 type typedef_info = C.typ +type enum_info = { + ei_members: C.enumerator list; (* list of all members *) + ei_attr: C.attributes (* attributes, if any *) +} + type t val empty : t @@ -44,28 +49,30 @@ val new_scope : t -> t val in_current_scope : t -> C.ident -> bool val lookup_ident : t -> string -> C.ident * ident_info -val lookup_tag : t -> string -> C.ident * composite_info val lookup_struct : t -> string -> C.ident * composite_info val lookup_union : t -> string -> C.ident * composite_info val lookup_composite : t -> string -> (C.ident * composite_info) option val lookup_typedef : t -> string -> C.ident * typedef_info +val lookup_enum : t -> string -> C.ident * enum_info val ident_is_bound : t -> string -> bool val find_ident : t -> C.ident -> ident_info -val find_tag : t -> C.ident -> composite_info val find_struct : t -> C.ident -> composite_info val find_union : t -> C.ident -> composite_info val find_member : C.field list -> string -> C.field val find_struct_member : t -> C.ident * string -> C.field val find_union_member : t -> C.ident * string -> C.field val find_typedef : t -> C.ident -> typedef_info +val find_enum : t -> C.ident -> enum_info val enter_ident : t -> string -> C.storage -> C.typ -> C.ident * t val enter_composite : t -> string -> composite_info -> C.ident * t val enter_enum_item : t -> string -> int64 -> C.ident * t val enter_typedef : t -> string -> typedef_info -> C.ident * t +val enter_enum : t -> string -> enum_info -> C.ident * t val add_ident : t -> C.ident -> C.storage -> C.typ -> t val add_composite : t -> C.ident -> composite_info -> t val add_typedef : t -> C.ident -> typedef_info -> t +val add_enum : t -> C.ident -> enum_info -> t diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml index 0dbc7cb..b1af7f6 100644 --- a/cparser/PackedStructs.ml +++ b/cparser/PackedStructs.ml @@ -60,6 +60,7 @@ let align x boundary = let rec can_byte_swap env ty = match unroll env ty with | TInt(ik, _) -> (true, sizeof_ikind ik > 1) + | TEnum(_, _) -> (true, sizeof_ikind enum_ikind > 1) | TPtr(_, _) -> (true, true) (* tolerance? *) | TArray(ty_elt, _, _) -> can_byte_swap env ty_elt | _ -> (false, false) @@ -162,6 +163,7 @@ let lookup_function loc env name = let accessor_type loc env ty = match unroll env ty with | TInt(ik,_) -> (8 * sizeof_ikind ik, TInt(unsigned_ikind_of ik,[])) + | TEnum(_,_) -> (8 * sizeof_ikind enum_ikind, TInt(unsigned_ikind_of enum_ikind,[])) | TPtr _ -> (8 * !config.sizeof_ptr, TInt(ptr_t_ikind,[])) | _ -> error "%a: unsupported type for byte-swapped field access" formatloc loc; @@ -376,6 +378,8 @@ let init_packed_struct loc env struct_id struct_sz initdata = match (unroll env ty, init) with | (TInt(ik, _), Init_single e) -> enter_scalar pos e (sizeof_ikind ik) bigendian + | (TEnum(_, _), Init_single e) -> + enter_scalar pos e (sizeof_ikind enum_ikind) bigendian | (TPtr _, Init_single e) -> enter_scalar pos e ((!Machine.config).sizeof_ptr) bigendian | (TArray(ty_elt, _, _), Init_array il) -> diff --git a/cparser/Rename.ml b/cparser/Rename.ml index 034df24..59b7bd7 100644 --- a/cparser/Rename.ml +++ b/cparser/Rename.ml @@ -96,6 +96,7 @@ let rec typ env = function | TNamed(id, a) -> TNamed(ident env id, a) | TStruct(id, a) -> TStruct(ident env id, a) | TUnion(id, a) -> TUnion(ident env id, a) + | TEnum(id, a) -> TEnum(ident env id, a) | ty -> ty and param env (id, ty) = @@ -168,6 +169,7 @@ and stmt_desc env = function | Sreturn a -> Sreturn (optexp env a) | Sblock sl -> let (sl', _) = mmap stmt_or_decl env sl in Sblock sl' | Sdecl d -> assert false + | Sasm txt -> Sasm txt and stmt_or_decl env s = match s.sdesc with @@ -195,9 +197,9 @@ let fundef env f = fd_body = stmt env2 f.fd_body }, env0 ) -let enum env (id, opte) = +let enum env (id, v, opte) = let (id', env') = rename env id in - ((id', optexp env' opte), env') + ((id', v, optexp env' opte), env') let rec globdecl env g = let (desc', env') = globdecl_desc env g.gdesc in @@ -219,10 +221,10 @@ and globdecl_desc env = function | Gtypedef(id, ty) -> let (id', env') = rename env id in (Gtypedef(id', typ env' ty), env') - | Genumdef(id, members) -> + | Genumdef(id, attr, members) -> let (id', env') = rename env id in let (members', env'') = mmap enum env' members in - (Genumdef(id', members'), env'') + (Genumdef(id', attr, members'), env'') | Gpragma s -> (Gpragma s, env) diff --git a/cparser/StructReturn.ml b/cparser/StructReturn.ml index dd985b1..ef3e591 100644 --- a/cparser/StructReturn.ml +++ b/cparser/StructReturn.ml @@ -182,6 +182,7 @@ let rec transf_stmt s = {s with sdesc = Sblock(List.map transf_stmt sl)} | Sdecl d -> {s with sdesc = Sdecl(transf_decl env d)} + | Sasm _ -> s in transf_stmt body diff --git a/cparser/Transform.ml b/cparser/Transform.ml index 0e7357b..3b6f10f 100644 --- a/cparser/Transform.ml +++ b/cparser/Transform.ml @@ -166,6 +166,7 @@ let stmt trexpr env s = | Sreturn None -> s | Sreturn (Some e) -> {s with sdesc = Sreturn(Some(trexpr s.sloc env Val e))} + | Sasm _ -> s | Sblock _ | Sdecl _ -> assert false (* should not occur in unblocked code *) in stm s @@ -185,7 +186,7 @@ let program ?(fundef = fun env fd -> fd) ?(composite = fun env su id attr fl -> (attr, fl)) ?(typedef = fun env id ty -> ty) - ?(enum = fun env id members -> members) + ?(enum = fun env id attr members -> (attr, members)) ?(pragma = fun env s -> s) p = @@ -208,8 +209,10 @@ let program Env.add_composite env id (composite_info_def env su attr fl)) | Gtypedef(id, ty) -> (Gtypedef(id, typedef env id ty), Env.add_typedef env id ty) - | Genumdef(id, members) -> - (Genumdef(id, enum env id members), env) + | Genumdef(id, attr, members) -> + let (attr', members') = enum env id attr members in + (Genumdef(id, attr', members'), + Env.add_enum env id {ei_members = members; ei_attr = attr}) | Gpragma s -> (Gpragma(pragma env s), env) in diff --git a/cparser/Transform.mli b/cparser/Transform.mli index 5736abc..718a2f9 100644 --- a/cparser/Transform.mli +++ b/cparser/Transform.mli @@ -65,9 +65,9 @@ val program : ?composite:(Env.t -> C.struct_or_union -> C.ident -> C.attributes -> C.field list -> C.attributes * C.field list) -> - ?typedef:(Env.t -> C.ident -> Env.typedef_info -> Env.typedef_info) -> - ?enum:(Env.t -> C.ident -> (C.ident * C.exp option) list -> - (C.ident * C.exp option) list) -> + ?typedef:(Env.t -> C.ident -> C.typ -> C.typ) -> + ?enum:(Env.t -> C.ident -> C.attributes -> C.enumerator list -> + C.attributes * C.enumerator list) -> ?pragma:(Env.t -> string -> string) -> C.program -> C.program diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml index abdc5d5..c40da18 100644 --- a/cparser/Unblock.ml +++ b/cparser/Unblock.ml @@ -110,6 +110,7 @@ let rec unblock_stmt env s = | Sreturn opte -> s | Sblock sl -> unblock_block env sl | Sdecl d -> assert false + | Sasm _ -> s and unblock_block env = function | [] -> sskip diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 96c7901..d38a398 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -24,6 +24,7 @@ let option_fpacked_structs = ref false let option_fsse = ref true let option_ffloatconstprop = ref 2 let option_falignfunctions = ref (None: int option) +let option_finline_asm = ref false let option_dparse = ref false let option_dcmedium = ref false let option_dclight = ref false diff --git a/driver/Driver.ml b/driver/Driver.ml index 87007a7..7fe3f64 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -391,6 +391,7 @@ Language support options (use -fno-<opt> to turn off -f<opt>) : -fstruct-return Emulate returning structs and unions by value [off] -fvararg-calls Emulate calls to variable-argument functions [on] -fpacked-structs Emulate packed structs [off] + -finline-asm Support inline 'asm' statements [off] -fall Activate all language support options above -fnone Turn off all language support options above Code generation options: (use -fno-<opt> to turn off -f<opt>) : @@ -433,7 +434,8 @@ Interpreter mode: let language_support_options = [ option_fbitfields; option_flonglong; option_flongdouble; - option_fstruct_return; option_fvararg_calls; option_fpacked_structs + option_fstruct_return; option_fvararg_calls; option_fpacked_structs; + option_finline_asm ] let cmdline_actions = @@ -505,6 +507,7 @@ let cmdline_actions = @ f_opt "bitfields" option_fbitfields @ f_opt "vararg-calls" option_fvararg_calls @ f_opt "packed-structs" option_fpacked_structs + @ f_opt "inline-asm" option_finline_asm @ f_opt "sse" option_fsse let _ = diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 08bd2f5..da08de8 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -714,6 +714,10 @@ let print_instruction oc = function (Int32.to_int (camlint_of_coqint al)) args | EF_annot_val(txt, targ) -> print_annot_val oc (extern_atom txt) args res + | EF_inline_asm txt -> + fprintf oc "%s begin inline assembly\n" comment; + fprintf oc " %s\n" (extern_atom txt); + fprintf oc "%s end inline assembly\n" comment | _ -> assert false end diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 3ef3c74..a20448c 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -747,6 +747,10 @@ let print_instruction oc tbl pc = function (Int32.to_int (camlint_of_coqint al)) args | EF_annot_val(txt, targ) -> print_annot_val oc (extern_atom txt) args res + | EF_inline_asm txt -> + fprintf oc "%s begin inline assembly\n" comment; + fprintf oc " %s\n" (extern_atom txt); + fprintf oc "%s end inline assembly\n" comment | _ -> assert false end diff --git a/test/regression/Makefile b/test/regression/Makefile index e8fb236..0a9212d 100644 --- a/test/regression/Makefile +++ b/test/regression/Makefile @@ -8,7 +8,7 @@ LIBS=$(LIBMATH) # Can run and have reference output in Results TESTS=attribs1 bitfields1 bitfields2 bitfields3 bitfields4 \ - bitfields5 bitfields6 bitfields7 \ + bitfields5 bitfields6 bitfields7 bitfields8 \ expr1 expr6 funptr2 initializers volatile1 volatile2 volatile3 \ funct3 expr5 struct7 struct8 struct11 casts1 casts2 char1 \ sizeof1 sizeof2 packedstruct1 packedstruct2 \ |