Experiment: support a subset of GCC's extended asm statements.

8 files changed, 168 insertions, 21 deletions

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 "@[<hov 0>%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 "@[<hov 0>%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 "@[<v 2>{@ %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(@[<hov 0>%a@ :%a@ :%a@]);"
+                 attributes attrs
+                 const (CStr txt)
+                 asm_operands outputs
+                 asm_operands inputs
+  | Sasm(attrs, txt, outputs, inputs, flags) ->
+      fprintf pp "asm%a(@[<hov 0>%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> gcc_attribute_word
 %type<name * list string> old_function_declarator direct_old_function_declarator
 %type<list string (* Reverse order *)> identifier_list
+%type<list asm_flag> asm_flags
+%type<option string> asm_op_name
+%type<asm_operand> asm_operand
+%type<list asm_operand> asm_operands asm_operands_ne
+%type<list asm_operand * list asm_operand * list asm_flag> asm_arguments
+%type<list cvspec> asm_attributes
 
 %start<list definition> translation_unit_file
 %%
@@ -820,10 +826,50 @@ jump_statement:
 
 (* Non-standard *)
 asm_statement:
-| loc = ASM LPAREN template = STRING_LITERAL RPAREN SEMICOLON
-    { let '(wide, chars, _) := template in ASM wide chars loc }
-| loc = ASM VOLATILE LPAREN template = STRING_LITERAL RPAREN SEMICOLON
-    { let '(wide, chars, _) := template in ASM wide chars loc }
+| loc = ASM attr = asm_attributes LPAREN template = STRING_LITERAL args = asm_arguments RPAREN SEMICOLON
+    { let '(wide, chars, _) := template in
+      let '(outputs, inputs, flags) := args in
+      ASM attr wide chars outputs inputs flags loc }
+
+asm_attributes:
+| /* empty */
+     { [] }
+| CONST attr = asm_attributes
+     { CV_CONST :: attr }
+| VOLATILE attr = asm_attributes 
+     { CV_VOLATILE :: attr }
+
+asm_arguments:
+| /* empty */
+     { ([], [], []) }
+| COLON o = asm_operands
+     { (o, [], []) }
+| COLON o = asm_operands COLON i = asm_operands
+     { (o, i, []) }
+| COLON o = asm_operands COLON i = asm_operands COLON f = asm_flags
+     { (o, i, f) }
+
+asm_operands:
+| /* empty */                                   { [] }
+| ol = asm_operands_ne                          { rev' ol }
+
+asm_operands_ne:
+| ol = asm_operands_ne COMMA o = asm_operand    { o :: ol }
+| o = asm_operand                               { [o] }
+
+asm_operand:
+| n = asm_op_name cstr = STRING_LITERAL LPAREN e = expression RPAREN
+    { let '(wide, s, loc) := cstr in ASMOPERAND n wide s (fst e) }
+
+asm_op_name:
+| /* empty */                         { None }
+| LBRACK n = OTHER_NAME RBRACK        { Some (fst n) }
+
+asm_flags:
+| f = STRING_LITERAL
+    { let '(wide, s, loc) := f in (wide, s) :: nil }
+| f = STRING_LITERAL COMMA fl = asm_flags
+    { let '(wide, s, loc) := f in (wide, s) :: fl }
 
 (* 6.9 *)
 translation_unit_file:
diff --git a/cparser/Rename.ml b/cparser/Rename.ml
index 2b7ec2ca..0d533b56 100644
--- a/cparser/Rename.ml
+++ b/cparser/Rename.ml
@@ -150,6 +150,8 @@ let decl env (sto, id, ty, int) =
     match int with None -> None | Some i -> Some(init env' i)),
    env')
 
+let asm_operand env (lbl, cstr, e) = (lbl, cstr, exp env e)
+
 let rec stmt env s =
   { sdesc = stmt_desc env s.sdesc; sloc = s.sloc }
 
@@ -170,7 +172,11 @@ 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
+  | Sasm(attr, txt, outputs, inputs, flags) ->
+       Sasm(attr, txt,
+            List.map (asm_operand env) outputs,
+            List.map (asm_operand env) inputs,
+            flags)
 
 and stmt_or_decl env s =
   match s.sdesc with
diff --git a/cparser/pre_parser.mly b/cparser/pre_parser.mly
index ef356d3a..44a06f8a 100644
--- a/cparser/pre_parser.mly
+++ b/cparser/pre_parser.mly
@@ -616,7 +616,43 @@ jump_statement:
     {}
 
 asm_statement:
-| ASM VOLATILE? LPAREN string_literals_list RPAREN SEMICOLON
+| ASM asm_attributes LPAREN string_literals_list asm_arguments RPAREN SEMICOLON
+    {}
+
+asm_attributes:
+| /* empty */
+| CONST asm_attributes    
+| VOLATILE asm_attributes
+    {}
+
+asm_arguments:
+| /* empty */
+| COLON asm_operands
+| COLON asm_operands COLON asm_operands
+| COLON asm_operands COLON asm_operands COLON asm_flags
+    {}
+
+asm_operands:
+| /* empty */
+| asm_operands_ne
+    {}
+
+asm_operands_ne:
+| asm_operands_ne COMMA asm_operand
+| asm_operand
+    {}
+
+asm_operand:
+| asm_op_name string_literals_list LPAREN expression RPAREN
+    {}
+
+asm_op_name:
+| /*empty*/                             {}
+| LBRACK i = general_identifier RBRACK  { set_id_type i OtherId }
+
+asm_flags:
+| string_literals_list
+| string_literals_list COMMA asm_flags
     {}
 
 translation_unit_file: