Merge pull request #40 from AbsInt/inline-asm

GCC-style extended inline asm.

The subset implemented is:

- zero or one output
- output constraints "=r" (to register) or "=m" (to memory)
- zero, one or several inputs
- input constraints "r" (in register), "m" (in memory), "i" and "n" (compile-time integer constant)
- clobbered registers (the 3rd argument)
- both anonymous (%3) and named (%[name]) operands
- modifiers %R and %Q to refer to the most significant / least significant part of a register pair holding a 64-bit integer. (Undocumented GCC ARM feature.)

All asm statements are treated as "volatile", possibly modifying memory and condition codes.

10 files changed, 371 insertions, 22 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/Cleanup.ml b/cparser/Cleanup.ml
index 09eaff9b..254f6fed 100644
--- a/cparser/Cleanup.ml
+++ b/cparser/Cleanup.ml
@@ -78,6 +78,8 @@ let add_decl (sto, id, ty, init) =
   add_typ ty;
   match init with None -> () | Some i -> add_init i
 
+let add_asm_operand (lbl, cstr, e) = add_exp e
+
 let rec add_stmt s =
   match s.sdesc with
   | Sskip -> ()
@@ -98,7 +100,9 @@ let rec add_stmt s =
   | Sreturn(Some e) -> add_exp e
   | Sblock sl -> List.iter add_stmt sl
   | Sdecl d -> add_decl d
-  | Sasm _ -> ()
+  | Sasm(attr, template, outputs, inputs, flags) ->
+      List.iter add_asm_operand outputs;
+      List.iter add_asm_operand inputs
 
 let add_fundef f =
   add_typ f.fd_ret;
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/ExtendedAsm.ml b/cparser/ExtendedAsm.ml
new file mode 100644
index 00000000..8751291b
--- /dev/null
+++ b/cparser/ExtendedAsm.ml
@@ -0,0 +1,198 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Partial emulation of GCC's extended inline assembly (experimental). *)
+
+(* The [transf_asm] function in this module takes a full GCC-style
+   extended asm statement and puts it in the form supported by
+   CompCert, namely:
+   - 0 or 1 output of kind "r" 
+   - 0, 1 or several inputs of kind "r".
+   Inputs and outputs of kind "m" (memory location) are emulated
+   by taking the address of the operand and treating it as
+   an input of kind "r".
+   Inputs of kind "i" and "n" (integer immediates) are evaluated
+   at compile-time and textually substituted in the asm template.
+
+   Extended asm statements that do not fit the forms above are rejected
+   with diagnostics. *)
+
+open Printf
+open Machine
+open C
+open Cutil
+open Env
+open Cerrors
+
+(* Renaming of labeled and numbered operands *)
+
+module StringMap = Map.Make(String)
+
+let name_of_label ?(modifier = "") lbl pos =
+  match lbl with
+  | None ->  (* numbered argument *)
+      sprintf "%%%s%d" modifier pos
+  | Some l -> (* named argument *)
+      sprintf "%%%s[%s]" modifier l
+
+let set_label_reg lbl pos pos' subst =
+  StringMap.add (name_of_label lbl pos) (sprintf "%%%d" pos') subst
+
+(* These are the modifiers used by GCC for ARM:
+      %Rxxx is the most significant half of a register pair
+      %Qxxx is the least significant half of a register pair.
+   They are not documented, and it is unclear whether other GCC ports
+   have this feature and with which syntax. *)
+
+let set_label_regpair lbl pos pos' subst =
+  StringMap.add (name_of_label ~modifier:"R" lbl pos) (sprintf "%%%d" pos')
+    (StringMap.add (name_of_label ~modifier:"Q" lbl pos)
+                   (sprintf "%%%d" (pos' + 1))
+                   subst)
+
+let set_label_mem lbl pos pos' subst =
+  StringMap.add (name_of_label lbl pos)
+                (CBuiltins.asm_mem_argument (sprintf "%%%d" pos'))
+                subst
+
+let set_label_const lbl pos n subst =
+  StringMap.add (name_of_label lbl pos) (sprintf "%Ld" n) subst
+
+(* Operands of 64-bit integer type get split into a pair of registers
+   on 32-bit platforms *)
+
+let is_reg_pair env ty =
+  match unroll env ty with
+  | TInt(ik, _) -> sizeof_ikind ik > !config.sizeof_ptr
+  | _ -> false
+
+(* Transform the input operands:
+     - add "&" for inputs of kind "m"
+     - evaluate constants for inputs of kind "i" and "n" *)
+
+let re_valid_input = Str.regexp "[a-zA-Z]+$"
+
+let rec transf_inputs loc env accu pos pos' subst = function
+  | [] ->
+      (List.rev accu, subst)
+  | (lbl, cstr, e) :: inputs ->
+      let valid = Str.string_match re_valid_input cstr 0 in
+      if valid && String.contains cstr 'r' then
+        if is_reg_pair env e.etyp then
+          transf_inputs loc env (e :: accu) (pos + 1) (pos' + 2)
+                      (set_label_regpair lbl pos pos' subst) inputs
+        else
+          transf_inputs loc env (e :: accu) (pos + 1) (pos' + 1)
+                      (set_label_reg lbl pos pos' subst) inputs
+      else
+      if valid && String.contains cstr 'm' then
+        transf_inputs loc env (eaddrof e :: accu) (pos + 1) (pos' + 1)
+                    (set_label_mem lbl pos pos' subst) inputs
+      else
+      if valid && (String.contains cstr 'i'
+                   || String.contains cstr 'n') then begin
+        let n =
+          match Ceval.integer_expr env e with
+          | Some n -> n
+          | None -> error "%aError: asm argument of kind '%s' is not a constant"
+                          formatloc loc cstr;
+                    0L in
+        transf_inputs loc env accu (pos + 1) pos'
+                      (set_label_const lbl pos n subst) inputs
+      end else begin
+        error "%aUnsupported feature: asm argument of kind '%s'"
+              formatloc loc cstr;
+        transf_inputs loc env (e :: accu) (pos + 1) (pos' + 1)
+                    (set_label_reg lbl pos pos' subst) inputs
+      end
+  
+(* Transform the output operands:
+     - outputs of kind "=m" become an input (equal to the address of the output)
+*)
+
+let re_valid_output = Str.regexp "=[a-zA-Z]+$"
+
+let transf_outputs loc env = function
+  | [] ->
+      (None, [], StringMap.empty, 0, 0)
+  | [(lbl, cstr, e)] ->
+      if not (is_modifiable_lvalue env e) then
+        error "%aError: asm output is not a modifiable l-value" formatloc loc;
+      let valid = Str.string_match re_valid_output cstr 0 in
+      if valid && String.contains cstr 'r' then
+        if is_reg_pair env e.etyp then
+          (Some e, [], set_label_regpair lbl 0 0 StringMap.empty, 1, 2)
+        else
+          (Some e, [], set_label_reg lbl 0 0 StringMap.empty, 1, 1)
+      else
+      if valid && String.contains cstr 'm' then
+        (None, [eaddrof e],
+           set_label_mem lbl 0 0 StringMap.empty, 1, 1)
+      else begin
+        error "%aUnsupported feature: asm result of kind '%s'"
+              formatloc loc cstr;
+        (None, [], set_label_reg lbl 0 0 StringMap.empty, 1, 1)
+      end
+  | outputs ->
+      error "%aUnsupported feature: asm statement with 2 or more outputs"
+            formatloc loc;
+      (* Bind the outputs so that we don't get another error 
+         when substituting the text *)
+      let rec bind_outputs pos subst = function
+      | [] -> (None, [], subst, pos, pos)
+      | (lbl, cstr, e) :: outputs ->
+          bind_outputs (pos + 1) (set_label_reg lbl pos pos subst) outputs
+      in bind_outputs 0 StringMap.empty outputs
+
+(* Check the clobber list *)
+
+let check_clobbers loc clob =
+  List.iter
+    (fun c ->
+      if Machregsaux.register_by_name c <> None
+      || c = "memory" || c = "cc"
+      then ()
+      else error "%aError: unrecognized asm register clobber '%s'" 
+                 formatloc loc c)
+    clob
+
+(* Renaming of the %nnn and %[ident] placeholders in the asm text *)
+
+let re_asm_placeholder =
+  Str.regexp "\\(%[QR]?\\([0-9]+\\|\\[[a-zA-Z_][a-zA-Z_0-9]*\\]\\)\\|%%\\)"
+
+let rename_placeholders loc template subst =       
+  let rename p =
+    if p = "%%" then p else
+      try
+        StringMap.find p subst
+      with Not_found ->
+        error "%aError: '%s' in asm text does not designate any operand"
+              formatloc loc p;
+        "%<error>"
+  in
+    Str.global_substitute re_asm_placeholder
+      (fun txt -> rename (Str.matched_group 1 txt))
+      template
+
+(* All together *)
+
+let transf_asm loc env template outputs inputs clobbers =
+  let (outputs', inputs1, subst1, pos, pos') =
+    transf_outputs loc env outputs in
+  let (inputs', subst) =
+    transf_inputs loc env inputs1 pos pos' subst1 inputs in
+  check_clobbers loc clobbers;
+  (rename_placeholders loc template subst, outputs', inputs')
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: