From 1b5db339bb05f773a6a132be4c0b8cea54d50461 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 17 Apr 2015 16:30:43 +0200 Subject: Experiment: support a subset of GCC's extended asm statements. --- cparser/C.mli | 6 +++++- cparser/Cabs.v | 8 +++++++- cparser/Cabshelper.ml | 2 +- cparser/Cprint.ml | 38 +++++++++++++++++++++++++++++++++-- cparser/Elab.ml | 35 ++++++++++++++++++++++---------- cparser/Parser.vy | 54 ++++++++++++++++++++++++++++++++++++++++++++++---- cparser/Rename.ml | 8 +++++++- cparser/pre_parser.mly | 38 ++++++++++++++++++++++++++++++++++- 8 files changed, 168 insertions(+), 21 deletions(-) (limited to 'cparser') diff --git a/cparser/C.mli b/cparser/C.mli index 71ab1d4d..72e1f787 100644 --- a/cparser/C.mli +++ b/cparser/C.mli @@ -190,6 +190,10 @@ and init = | Init_struct of ident * (field * init) list | Init_union of ident * field * init +(** GCC extended asm *) + +type asm_operand = string option * string * exp + (** Statements *) type stmt = { sdesc: stmt_desc; sloc: location } @@ -210,7 +214,7 @@ and stmt_desc = | Sreturn of exp option | Sblock of stmt list | Sdecl of decl - | Sasm of string + | Sasm of attributes * string * asm_operand list * asm_operand list * string list and slabel = | Slabel of string diff --git a/cparser/Cabs.v b/cparser/Cabs.v index 920f4603..6d9e95d5 100644 --- a/cparser/Cabs.v +++ b/cparser/Cabs.v @@ -180,6 +180,12 @@ Definition init_name_group := (list spec_elem * list init_name)%type. (* e.g.: int x, y; *) Definition name_group := (list spec_elem * list name)%type. +(* GCC extended asm *) +Inductive asm_operand := +| ASMOPERAND: option string -> bool -> list char_code -> expression -> asm_operand. + +Definition asm_flag := (bool * list char_code)%type. + (* ** Declaration definition (at toplevel) *) @@ -209,7 +215,7 @@ with statement := | DEFAULT : statement -> cabsloc -> statement | LABEL : string -> statement -> cabsloc -> statement | GOTO : string -> cabsloc -> statement - | ASM : bool -> list char_code -> cabsloc -> statement + | ASM : list cvspec -> bool -> list char_code -> list asm_operand -> list asm_operand -> list asm_flag -> cabsloc -> statement | DEFINITION : definition -> statement (*definition or declaration of a variable or type*) with for_clause := diff --git a/cparser/Cabshelper.ml b/cparser/Cabshelper.ml index 9d4a91f6..5e6a19d0 100644 --- a/cparser/Cabshelper.ml +++ b/cparser/Cabshelper.ml @@ -70,7 +70,7 @@ begin | LABEL(_,_,loc) -> loc | GOTO(_,loc) -> loc | DEFINITION d -> get_definitionloc d - | ASM(_,_,loc) -> loc + | ASM(_,_,_,_,_,_,loc) -> loc end let string_of_cabsloc l = diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml index ee8002d4..4ceaa016 100644 --- a/cparser/Cprint.ml +++ b/cparser/Cprint.ml @@ -364,6 +364,27 @@ let full_decl pp (sto, id, ty, int) = end; fprintf pp ";@]" +let asm_operand pp (label, constr, e) = + begin match label with + | None -> () + | Some l -> fprintf pp "[%s] " l + end; + fprintf pp "%a (%a)" const (CStr constr) exp (0, e) + +let asm_operands pp = function + | [] -> () + | op1 :: ops -> + fprintf pp "@[%a" asm_operand op1; + List.iter (fun op -> fprintf pp ",@ %a" asm_operand op) ops; + fprintf pp "@]" + +let asm_flags pp = function + | [] -> () + | fl1 :: fls -> + fprintf pp "@[%a" const (CStr fl1); + List.iter (fun fl -> fprintf pp ",@ %a" const (CStr fl)) fls; + fprintf pp "@]" + exception Not_expr let rec exp_of_stmt s = @@ -429,8 +450,21 @@ let rec stmt pp s = fprintf pp "@[{@ %a@;<0 -2>}@]" stmt_block s | Sdecl d -> full_decl pp d - | Sasm txt -> - fprintf pp "asm(%a);" const (CStr txt) + | Sasm(attrs, txt, [], [], []) -> + fprintf pp "asm%a(%a);" attributes attrs const (CStr txt) + | Sasm(attrs, txt, outputs, inputs, []) -> + fprintf pp "asm%a(@[%a@ :%a@ :%a@]);" + attributes attrs + const (CStr txt) + asm_operands outputs + asm_operands inputs + | Sasm(attrs, txt, outputs, inputs, flags) -> + fprintf pp "asm%a(@[%a@ :%a@ :%a@ : %a@]);" + attributes attrs + const (CStr txt) + asm_operands outputs + asm_operands inputs + asm_flags flags and slabel pp = function | Slabel s -> diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 612103a6..a1dd552b 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -270,6 +270,11 @@ let elab_constant loc = function | CONST_STRING(wide, s) -> elab_string_literal loc wide s +let elab_simple_string loc wide chars = + match elab_string_literal loc wide chars with + | CStr s -> s + | _ -> error loc "wide character string not allowed here"; "" + (** * Elaboration of type expressions, type specifiers, name declarations *) @@ -498,13 +503,16 @@ and elab_cvspec env = function | CV_RESTRICT -> [ARestrict] | CV_ATTR attr -> elab_attribute env attr +and elab_cvspecs env cv_specs = + List.fold_left add_attributes [] (List.map (elab_cvspec env) cv_specs) + (* Elaboration of a type declarator. C99 section 6.7.5. *) and elab_type_declarator loc env ty = function | Cabs.JUSTBASE -> (ty, env) | Cabs.ARRAY(d, cv_specs, sz) -> - let a = List.fold_left add_attributes [] (List.map (elab_cvspec env) cv_specs) in + let a = elab_cvspecs env cv_specs in let sz' = match sz with | None -> @@ -520,7 +528,7 @@ and elab_type_declarator loc env ty = function Some 1L in (* produces better error messages later *) elab_type_declarator loc env (TArray(ty, sz', a)) d | Cabs.PTR(cv_specs, d) -> - let a = List.fold_left add_attributes [] (List.map (elab_cvspec env) cv_specs) in + let a = elab_cvspecs env cv_specs in elab_type_declarator loc env (TPtr(ty, a)) d | Cabs.PROTO(d, (params, vararg)) -> begin match unroll env ty with @@ -1933,6 +1941,13 @@ and elab_definitions local env = function let (decl2, env2) = elab_definitions local env1 dl in (decl1 @ decl2, env2) +(* Extended asm *) + +let elab_asm_operand loc env (ASMOPERAND(label, wide, chars, e)) = + let s = elab_simple_string loc wide chars in + let e' = elab_expr loc env e in + (label, s, e') + (* Contexts for elaborating statements *) @@ -2118,14 +2133,14 @@ let rec elab_stmt env ctx s = { sdesc = Sskip; sloc = elab_loc loc } (* Traditional extensions *) - | ASM(wide, chars, loc) -> - begin match elab_string_literal loc wide chars with - | CStr s -> - { sdesc = Sasm s; sloc = elab_loc loc } - | _ -> - error loc "wide strings not supported in asm statement"; - sskip - end + | ASM(cv_specs, wide, chars, outputs, inputs, flags, loc) -> + let a = elab_cvspecs env cv_specs in + let s = elab_simple_string loc wide chars in + let outputs = List.map (elab_asm_operand loc env) outputs in + let inputs = List.map (elab_asm_operand loc env) inputs in + let flags = List.map (fun (w,c) -> elab_simple_string loc w c) flags in + { sdesc = Sasm(a, s, outputs, inputs, flags); + sloc = elab_loc loc } (* Unsupported *) | DEFINITION def -> diff --git a/cparser/Parser.vy b/cparser/Parser.vy index a058a8d1..7c0bfb55 100644 --- a/cparser/Parser.vy +++ b/cparser/Parser.vy @@ -97,6 +97,12 @@ Require Import List. %type gcc_attribute_word %type old_function_declarator direct_old_function_declarator %type identifier_list +%type asm_flags +%type