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.

33 files changed, 604 insertions, 76 deletions

diff --git a/.depend b/.depend
index 0f786903..394d99ec 100644
--- a/.depend
+++ b/.depend
@@ -78,7 +78,7 @@ backend/Locations.vo backend/Locations.glob backend/Locations.v.beautified: back
 $(ARCH)/Conventions1.vo $(ARCH)/Conventions1.glob $(ARCH)/Conventions1.v.beautified: $(ARCH)/Conventions1.v lib/Coqlib.vo common/AST.vo common/Events.vo backend/Locations.vo
 backend/Conventions.vo backend/Conventions.glob backend/Conventions.v.beautified: backend/Conventions.v lib/Coqlib.vo common/AST.vo backend/Locations.vo $(ARCH)/Conventions1.vo
 backend/LTL.vo backend/LTL.glob backend/LTL.v.beautified: backend/LTL.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo
-backend/Allocation.vo backend/Allocation.glob backend/Allocation.v.beautified: backend/Allocation.v lib/FSetAVLplus.vo $(ARCH)/Archi.vo lib/Coqlib.vo lib/Ordered.vo common/Errors.vo lib/Maps.vo lib/Lattice.vo common/AST.vo lib/Integers.vo common/Memdata.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo backend/Locations.vo backend/Conventions.vo backend/RTLtyping.vo backend/LTL.vo
+backend/Allocation.vo backend/Allocation.glob backend/Allocation.v.beautified: backend/Allocation.v lib/FSetAVLplus.vo $(ARCH)/Archi.vo lib/Coqlib.vo lib/Ordered.vo common/Errors.vo lib/Maps.vo lib/Lattice.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Memdata.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo backend/Locations.vo backend/Conventions.vo backend/RTLtyping.vo backend/LTL.vo
 backend/Allocproof.vo backend/Allocproof.glob backend/Allocproof.v.beautified: backend/Allocproof.v $(ARCH)/Archi.vo lib/Coqlib.vo lib/Ordered.vo common/Errors.vo lib/Maps.vo lib/Lattice.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo backend/Locations.vo backend/Conventions.vo backend/LTL.vo backend/Allocation.vo
 backend/Tunneling.vo backend/Tunneling.glob backend/Tunneling.v.beautified: backend/Tunneling.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo backend/LTL.vo
 backend/Tunnelingproof.vo backend/Tunnelingproof.glob backend/Tunnelingproof.v.beautified: backend/Tunnelingproof.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/Tunneling.vo
@@ -107,7 +107,7 @@ cfrontend/Cstrategy.vo cfrontend/Cstrategy.glob cfrontend/Cstrategy.v.beautified
 cfrontend/Cexec.vo cfrontend/Cexec.glob cfrontend/Cexec.v.beautified: cfrontend/Cexec.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Determinism.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo
 cfrontend/Initializers.vo cfrontend/Initializers.glob cfrontend/Initializers.v.beautified: cfrontend/Initializers.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Globalenvs.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo
 cfrontend/Initializersproof.vo cfrontend/Initializersproof.glob cfrontend/Initializersproof.v.beautified: cfrontend/Initializersproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Initializers.vo
-cfrontend/SimplExpr.vo cfrontend/SimplExpr.glob cfrontend/SimplExpr.v.beautified: cfrontend/SimplExpr.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Clight.vo
+cfrontend/SimplExpr.vo cfrontend/SimplExpr.glob cfrontend/SimplExpr.v.beautified: cfrontend/SimplExpr.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Clight.vo
 cfrontend/SimplExprspec.vo cfrontend/SimplExprspec.glob cfrontend/SimplExprspec.v.beautified: cfrontend/SimplExprspec.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Memory.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo
 cfrontend/SimplExprproof.vo cfrontend/SimplExprproof.glob cfrontend/SimplExprproof.v.beautified: cfrontend/SimplExprproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo cfrontend/SimplExprspec.vo
 cfrontend/Clight.vo cfrontend/Clight.glob cfrontend/Clight.v.beautified: cfrontend/Clight.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo
diff --git a/arm/CBuiltins.ml b/arm/CBuiltins.ml
index 17aa5115..00de4df7 100644
--- a/arm/CBuiltins.ml
+++ b/arm/CBuiltins.ml
@@ -55,3 +55,7 @@ let builtins = {
 
 let size_va_list = 4
 let va_list_scalar = true
+
+(* Expand memory references inside extended asm statements.  Used in C2C. *)
+
+let asm_mem_argument arg = Printf.sprintf "[%s, #0]" arg
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index df17e595..c77572db 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -1003,9 +1003,9 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
                 (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);
+          | EF_inline_asm(txt, sg, clob) ->
+              fprintf oc "%s begin inline assembly\n\t" comment;
+              PrintAnnot.print_inline_asm preg oc (extern_atom txt) sg args res;
               fprintf oc "%s end inline assembly\n" comment;
               5 (* hoping this is an upper bound...  *)
           | _ ->
diff --git a/backend/CMparser.mly b/backend/CMparser.mly
index 69b70e72..f62e05d4 100644
--- a/backend/CMparser.mly
+++ b/backend/CMparser.mly
@@ -60,7 +60,7 @@ let mkef sg toks =
       if sg.sig_args = [] then raise Parsing.Parse_error;
       EF_annot_val(intern_string txt, List.hd sg.sig_args)
   | [EFT_tok "inline_asm"; EFT_string txt] ->
-      EF_inline_asm(intern_string txt)
+      EF_inline_asm(intern_string txt, sg, [])
   | _ ->
       raise Parsing.Parse_error
 
diff --git a/backend/CSE.v b/backend/CSE.v
index 2c0c5f33..e9006d4f 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -476,7 +476,7 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb
           empty_numbering
       | Ibuiltin ef args res s =>
           match ef with
-          | EF_external _ _ | EF_malloc | EF_free | EF_inline_asm _ =>
+          | EF_external _ _ | EF_malloc | EF_free | EF_inline_asm _ _ _ =>
               empty_numbering
           | EF_builtin _ _ | EF_vstore _ | EF_vstore_global _ _ _ =>
               set_unknown (kill_all_loads before) res
diff --git a/backend/PrintAnnot.ml b/backend/PrintAnnot.ml
index 995f22dd..88f5d8d6 100644
--- a/backend/PrintAnnot.ml
+++ b/backend/PrintAnnot.ml
@@ -148,7 +148,29 @@ let print_annot_val print_preg oc txt args =
   print_annot_text print_preg "<internal error>" oc txt
     (List.map (fun r -> AA_base r) args)
 
-(* Print CompCert version and command-line as asm comment *)
+(** Inline assembly *)
+
+let re_asm_param = Str.regexp "%%\\|%[0-9]+"
+
+let print_inline_asm print_preg oc txt sg args res =
+  let operands =
+    if sg.sig_res = None then args else res @ args in
+  let print_fragment = function
+  | Str.Text s ->
+      output_string oc s
+  | Str.Delim "%%" ->
+      output_char oc '%'
+  | Str.Delim s ->
+      let n = int_of_string (String.sub s 1 (String.length s - 1)) in
+      try
+        print_preg oc (List.nth operands n)
+      with Failure _ ->
+        fprintf oc "<bad parameter %s>" s in
+  List.iter print_fragment (Str.full_split re_asm_param txt);
+  fprintf oc "\n"
+
+
+(** Print CompCert version and command-line as asm comment *)
 
 let print_version_and_options oc comment =
   fprintf oc "%s File generated by CompCert %s\n" comment Configuration.version;
diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml
index 3a7f5d99..c286e946 100644
--- a/backend/Regalloc.ml
+++ b/backend/Regalloc.ml
@@ -510,6 +510,9 @@ let add_interfs_live g live v =
 let add_interfs_list g v vl =
   List.iter (IRC.add_interf g v) vl
 
+let add_interfs_list_mreg g vl mr =
+  List.iter (fun v -> IRC.add_interf g v (L (R mr))) vl
+
 let rec add_interfs_pairwise g = function
   | [] -> ()
   | v1 :: vl -> add_interfs_list g v1 vl; add_interfs_pairwise g vl
@@ -578,7 +581,20 @@ let add_interfs_instr g instr live =
       add_interfs_pairwise g res;
       add_interfs_destroyed g across (destroyed_by_builtin ef);
       begin match ef, args, res with
-      | EF_annot_val _, [arg], [res] -> IRC.add_pref g arg res (* like a move *)
+      | EF_annot_val _, [arg], [res] ->
+          (* like a move *)
+          IRC.add_pref g arg res
+      | EF_inline_asm(txt, sg, clob), _, _ ->
+          (* clobbered regs interfere with live set
+             and also with res and args for GCC compatibility *)
+          List.iter (fun c ->
+            match Machregsaux.register_by_name (extern_atom c) with
+            | None -> ()
+            | Some mr ->
+                add_interfs_destroyed g across [mr];
+                add_interfs_list_mreg g args mr;
+                if sg.sig_res <> None then add_interfs_list_mreg g res mr)
+            clob          
       | _ -> ()
       end
   | Xannot(ef, args) ->
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index fd10efb4..b6b9defe 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -114,18 +114,14 @@ let currentLocation = ref Cutil.no_loc
 
 let updateLoc l = currentLocation := l
 
-let numErrors = ref 0
-
 let error msg =
-  incr numErrors;
-  eprintf "%aError: %s\n" Cutil.printloc !currentLocation msg
+  Cerrors.error "%aError: %s" Cutil.formatloc !currentLocation msg
 
 let unsupported msg =
-  incr numErrors;
-  eprintf "%aUnsupported feature: %s\n" Cutil.printloc !currentLocation msg
+  Cerrors.error "%aUnsupported feature: %s" Cutil.formatloc !currentLocation msg
 
 let warning msg =
-  eprintf "%aWarning: %s\n" Cutil.printloc !currentLocation msg
+  Cerrors.warning "%aWarning: %s\n" Cutil.formatloc !currentLocation msg
 
 let string_of_errmsg msg =
   let string_of_err = function
@@ -831,6 +827,30 @@ and convertExprList env el =
   | [] -> Enil
   | e1 :: el' -> Econs(convertExpr env e1, convertExprList env el')
 
+(* Extended assembly *)
+
+let convertAsm loc env txt outputs inputs clobber =
+  let (txt', output', inputs') = 
+    ExtendedAsm.transf_asm loc env txt outputs inputs clobber in
+  let clobber' =
+    List.map intern_string clobber in
+  let ty_res =
+    match output' with None -> TVoid [] | Some e -> e.etyp in
+  (* Build the Ebuiltin expression *)
+  let e = 
+    let tinputs = convertTypArgs env [] inputs' in
+    let toutput = convertTyp env ty_res in
+    Ebuiltin(EF_inline_asm(intern_string txt', 
+                           signature_of_type tinputs toutput cc_default,
+                           clobber'),
+             tinputs,
+             convertExprList env inputs',
+             convertTyp env ty_res) in
+  (* Add an assignment to the output, if any *)
+  match output' with
+  | None -> e
+  | Some lhs -> Eassign (convertLvalue env lhs, e, typeof e)
+
 (* Separate the cases of a switch statement body *)
 
 type switchlabel =
@@ -891,7 +911,9 @@ let rec convertStmt ploc env s =
   | C.Sdo e ->
       add_lineno ploc s.sloc (swrap (Ctyping.sdo (convertExpr env e)))
   | C.Sseq(s1, s2) ->
-      Ssequence(convertStmt ploc env s1, convertStmt s1.sloc env s2)
+      let s1' = convertStmt ploc env s1 in
+      let s2' = convertStmt s1.sloc env s2 in
+      Ssequence(s1', s2')
   | C.Sif(e, s1, s2) ->
       let te = convertExpr env e in
       add_lineno ploc s.sloc 
@@ -940,11 +962,11 @@ let rec convertStmt ploc env s =
       unsupported "nested blocks"; Sskip
   | C.Sdecl _ ->
       unsupported "inner declarations"; Sskip
-  | C.Sasm txt ->
+  | C.Sasm(attrs, txt, outputs, inputs, clobber) ->
       if not !Clflags.option_finline_asm then
         unsupported "inline 'asm' statement (consider adding option -finline-asm)";
       add_lineno ploc s.sloc
-        (Sdo (Ebuiltin (EF_inline_asm (intern_string txt), Tnil, Enil, Tvoid)))
+        (Sdo (convertAsm s.sloc env txt outputs inputs clobber))
 
 and convertSwitch ploc env is_64 = function
   | [] ->
@@ -1211,7 +1233,7 @@ let public_globals gl =
 (** Convert a [C.program] into a [Csyntax.program] *)
 
 let convertProgram p =
-  numErrors := 0;
+  Cerrors.reset();
   stringNum := 0;
   Hashtbl.clear decl_atom;
   Hashtbl.clear stringTable;
@@ -1236,9 +1258,7 @@ let convertProgram p =
             prog_main = intern_string "main";
             prog_types = typs;
             prog_comp_env = ce } in
-        if !numErrors > 0
-        then None
-        else Some p'
+        if Cerrors.check_errors () then None else Some p'
   with Env.Error msg ->
     error (Env.error_message msg); None
 
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 7c00ab47..aba3c094 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -405,18 +405,18 @@ Hypothesis do_external_function_complete:
   do_external_function id sg ge w vargs m = Some(w', t, vres, m').
 
 Variable do_inline_assembly:
-  ident -> Senv.t -> world -> list val -> mem -> option (world * trace * val * mem).
+  ident -> signature -> Senv.t -> world -> list val -> mem -> option (world * trace * val * mem).
 
 Hypothesis do_inline_assembly_sound:
-  forall txt ge vargs m t vres m' w w',
-  do_inline_assembly txt ge w vargs m = Some(w', t, vres, m') ->
-  inline_assembly_sem txt ge vargs m t vres m' /\ possible_trace w t w'.
+  forall txt sg ge vargs m t vres m' w w',
+  do_inline_assembly txt sg ge w vargs m = Some(w', t, vres, m') ->
+  inline_assembly_sem txt sg ge vargs m t vres m' /\ possible_trace w t w'.
 
 Hypothesis do_inline_assembly_complete:
-  forall txt ge vargs m t vres m' w w',
-  inline_assembly_sem txt ge vargs m t vres m' ->
+  forall txt sg ge vargs m t vres m' w w',
+  inline_assembly_sem txt sg ge vargs m t vres m' ->
   possible_trace w t w' ->
-  do_inline_assembly txt ge w vargs m = Some(w', t, vres, m').
+  do_inline_assembly txt sg ge w vargs m = Some(w', t, vres, m').
 
 Definition do_ef_volatile_load (chunk: memory_chunk)
        (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
@@ -541,7 +541,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_inline_assembly text ge
+  | EF_inline_asm text sg clob => do_inline_assembly text sg ge
   end.
 
 Lemma do_ef_external_sound:
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 882272b8..39de282b 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -236,6 +236,8 @@ let rec expr p (prec, e) =
                  expr (prec1, a1) (name_binop op) expr (prec2, a2)
   | Ecast(a1, ty) ->
       fprintf p "(%s) %a" (name_type ty) expr (prec', a1)
+  | Eassign(res, Ebuiltin(EF_inline_asm(txt, sg, clob), _, args, _), _) ->
+      extended_asm p txt (Some res) args clob
   | Eassign(a1, a2, _) ->
       fprintf p "%a =@ %a" expr (prec1, a1) expr (prec2, a2)
   | Eassignop(op, a1, a2, _, _) ->
@@ -262,6 +264,8 @@ let rec expr p (prec, e) =
                 (extern_atom txt) exprlist (false, args)
   | Ebuiltin(EF_external(id, sg), _, args, _) ->
       fprintf p "%s@[<hov 1>(%a)@]" (extern_atom id) exprlist (true, args)
+  | Ebuiltin(EF_inline_asm(txt, sg, clob), _, args, _) ->
+      extended_asm p txt None args clob
   | Ebuiltin(_, _, args, _) ->
       fprintf p "<unknown builtin>@[<hov 1>(%a)@]" exprlist (true, args)
   | Eparen(a1, tycast, ty) ->
@@ -277,6 +281,32 @@ and exprlist p (first, rl) =
       expr p (2, r);
       exprlist p (false, rl)
 
+and extended_asm p txt res args clob =
+  fprintf p "asm volatile (@[<hv 0>%S" (extern_atom txt);
+  fprintf p "@ :";
+  begin match res with
+  | None -> ()
+  | Some e -> fprintf p " \"=r\"(%a)" expr (0, e)
+  end;
+  let rec inputs p (first, el) =
+    match el with
+    | Enil -> ()
+    | Econs(e1, el) ->
+        if not first then fprintf p ",@ ";
+        fprintf p "\"r\"(%a)" expr (0, e1);
+        inputs p (false, el) in
+  fprintf p "@ : @[<hov 0>%a@]" inputs (true, args);
+  begin match clob with
+  | [] -> ()
+  | c1 :: cl ->
+      fprintf p "@ : @[<hov 0>%S" (extern_atom c1);
+      List.iter
+        (fun c -> fprintf p ",@ %S" (extern_atom c))
+        cl;
+      fprintf p "@]"
+  end;
+  fprintf p ")@]"
+
 let print_expr p e = expr p (0, e)
 let print_exprlist p el = exprlist p (true, el)
 
diff --git a/common/AST.v b/common/AST.v
index d2926178..2550844b 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -584,7 +584,7 @@ Inductive external_function : Type :=
      (** 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).
+  | EF_inline_asm (text: ident) (sg: signature) (clobbers: list 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
@@ -606,7 +606,7 @@ Definition ef_sig (ef: external_function): signature :=
   | EF_memcpy sz al => mksignature (Tint :: Tint :: nil) None cc_default
   | EF_annot text targs => mksignature targs None cc_default
   | EF_annot_val text targ => mksignature (targ :: nil) (Some targ) cc_default
-  | EF_inline_asm text => mksignature nil None cc_default
+  | EF_inline_asm text sg clob => sg
   end.
 
 (** Whether an external function should be inlined by the compiler. *)
@@ -624,7 +624,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
+  | EF_inline_asm text sg clob => true
   end.
 
 (** Whether an external function must reload its arguments. *)
@@ -642,6 +642,7 @@ Proof.
   generalize ident_eq signature_eq chunk_eq typ_eq zeq Int.eq_dec; intros.
   decide equality.
   apply list_eq_dec. auto.
+  apply list_eq_dec. auto.
 Defined.
 Global Opaque external_function_eq.
 
diff --git a/common/Events.v b/common/Events.v
index 15bf4e12..3bec15db 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -1449,10 +1449,10 @@ Axiom external_functions_properties:
 
 (** We treat inline assembly similarly. *)
 
-Parameter inline_assembly_sem: ident -> extcall_sem.
+Parameter inline_assembly_sem: ident -> signature -> extcall_sem.
 
 Axiom inline_assembly_properties:
-  forall id, extcall_properties (inline_assembly_sem id) (mksignature nil None cc_default) nil.
+  forall id sg, extcall_properties (inline_assembly_sem id sg) sg nil.
 
 (** ** Combined semantics of external calls *)
 
@@ -1479,8 +1479,8 @@ Definition external_call (ef: external_function): extcall_sem :=
   | EF_free              => extcall_free_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    => inline_assembly_sem txt
+  | EF_annot_val txt targ => extcall_annot_val_sem txt targ
+  | EF_inline_asm txt sg clb => inline_assembly_sem txt sg
   end.
 
 Theorem external_call_spec:
diff --git a/common/PrintAST.ml b/common/PrintAST.ml
index 52aa963a..76305d02 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.ml
@@ -53,7 +53,7 @@ let name_of_external = function
       sprintf "memcpy size %s align %s " (Z.to_string sz) (Z.to_string 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)
+  | EF_inline_asm(text, sg, clob) -> sprintf "inline_asm %S" (extern_atom text)
 
 let rec print_annot_arg px oc = function
   | AA_base x -> px oc x
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:
diff --git a/driver/Interp.ml b/driver/Interp.ml
index 2725dbfe..b16d2cae 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -397,7 +397,7 @@ let do_external_function id sg ge w args m =
   | _ ->
       None
 
-let do_inline_assembly txt ge w args m = None
+let do_inline_assembly txt sg ge w args m = None
 
 (* Implementing external functions producing observable events *)
 
diff --git a/ia32/CBuiltins.ml b/ia32/CBuiltins.ml
index 765f5b18..b1be612b 100644
--- a/ia32/CBuiltins.ml
+++ b/ia32/CBuiltins.ml
@@ -70,3 +70,7 @@ let builtins = {
 
 let size_va_list = 4
 let va_list_scalar = true
+
+(* Expand memory references inside extended asm statements.  Used in C2C. *)
+
+let asm_mem_argument arg = Printf.sprintf "0(%s)" arg
diff --git a/ia32/Machregsaux.ml b/ia32/Machregsaux.ml
index 8403746a..3083cf3e 100644
--- a/ia32/Machregsaux.ml
+++ b/ia32/Machregsaux.ml
@@ -15,8 +15,8 @@
 open Machregs
 
 let register_names = [
-  ("AX", AX); ("BX", BX); ("CX", CX); ("DX", DX);
-  ("SI", SI); ("DI", DI); ("BP", BP);
+  ("EAX", AX); ("EBX", BX); ("ECX", CX); ("EDX", DX);
+  ("ESI", SI); ("EDI", DI); ("EBP", BP);
   ("XMM0", X0); ("XMM1", X1); ("XMM2", X2); ("XMM3", X3);
   ("XMM4", X4); ("XMM5", X5); ("XMM6", X6); ("XMM7", X7);
   ("ST0", FP0)
diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml
index 58b7aa37..ca07a172 100644
--- a/ia32/TargetPrinter.ml
+++ b/ia32/TargetPrinter.ml
@@ -871,9 +871,9 @@ module Target(System: SYSTEM):TARGET =
                 (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);
+          | EF_inline_asm(txt, sg, clob) ->
+              fprintf oc "%s begin inline assembly\n\t" comment;
+              PrintAnnot.print_inline_asm preg oc (extern_atom txt) sg args res;
               fprintf oc "%s end inline assembly\n" comment
           | _ ->
               assert false
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 47895cb1..aec8f66e 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -523,7 +523,7 @@ let expand_instruction instr =
           expand_builtin_memcpy (Z.to_int sz) (Z.to_int al) args
       | EF_annot_val(txt, targ) ->
           expand_annot_val txt targ args res
-      | EF_inline_asm txt ->
+      | EF_inline_asm(txt, sg, clob) ->
           emit instr
       | _ ->
           assert false
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml
index 8840d2c3..222a4d94 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -90,3 +90,7 @@ let builtins = {
 
 let size_va_list = 12
 let va_list_scalar = false
+
+(* Expand memory references inside extended asm statements.  Used in C2C. *)
+
+let asm_mem_argument arg = Printf.sprintf "0(%s)" arg
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index b3d228b3..b05b29c0 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -284,10 +284,14 @@ module Target (System : SYSTEM):TARGET =
     let ireg_or_zero oc r =
       if r = GPR0 then output_string oc "0" else ireg oc r
 
-    (* [preg] is only used for printing annotations.
-       Use the full register names [rN] and [fN] to avoid
-       ambiguity with constants. *)
     let preg oc = function
+      | IR r -> ireg oc r
+      | FR r -> freg oc r
+      | _    -> assert false
+
+    (* For printing annotations, use the full register names [rN] and [fN]
+       to avoid ambiguity with constants. *)
+    let preg_annot oc = function
       | IR r -> fprintf oc "r%s" (int_reg_name r)
       | FR r -> fprintf oc "f%s" (float_reg_name r)
       | _    -> assert false
@@ -327,7 +331,7 @@ module Target (System : SYSTEM):TARGET =
           (int_of_string (Str.matched_group 2 txt))
       end else begin
         fprintf oc "%s annotation: " comment;
-        PrintAnnot.print_annot_stmt preg "R1" oc txt targs args
+        PrintAnnot.print_annot_stmt preg_annot "R1" oc txt targs args
       end
 
     (* Determine if the displacement of a conditional branch fits the short form *)
@@ -646,9 +650,9 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "%a:\n" label (transl_label lbl)
       | Pbuiltin(ef, args, res) ->
           begin match ef with
-          | EF_inline_asm txt ->
-              fprintf oc "%s begin inline assembly\n" comment;
-              fprintf oc "	%s\n" (extern_atom txt);
+          | EF_inline_asm(txt, sg, clob) ->
+              fprintf oc "%s begin inline assembly\n\t" comment;
+              PrintAnnot.print_inline_asm preg oc (extern_atom txt) sg args res;
               fprintf oc "%s end inline assembly\n" comment
           | _ ->
               assert false
diff --git a/test/raytracer/config.h b/test/raytracer/config.h
index 49361dc5..009c125e 100644
--- a/test/raytracer/config.h
+++ b/test/raytracer/config.h
@@ -5,6 +5,10 @@
 #include <stdlib.h>
 #include <string.h>
 
+#ifndef M_PI
+# define M_PI 3.14159265358979323846
+#endif
+
 #ifdef SINGLE_PRECISION
 typedef float flt;
 #else
diff --git a/test/regression/Makefile b/test/regression/Makefile
index 206670b5..1ffe586c 100644
--- a/test/regression/Makefile
+++ b/test/regression/Makefile
@@ -36,7 +36,7 @@ TESTS_DIFF=NaNs
 EXTRAS=annot1 commaprec expr2 expr3 expr4 extern1 funct2 funptr1 \
   pragmas ptrs1 ptrs2 struct1 struct2 struct3 \
   struct4 struct5 struct6 struct9 struct10 types1 seqops \
-  singlefloats emptydecl
+  singlefloats emptydecl extasm
 
 # Test known to fail
 FAILURES=funct1
diff --git a/test/regression/extasm.c b/test/regression/extasm.c
new file mode 100644
index 00000000..a69b3e79
--- /dev/null
+++ b/test/regression/extasm.c
@@ -0,0 +1,70 @@
+/* Testing extended asm.
+   To run the test, compile with -S and grep "TEST" in the generated .s */
+
+int clobbers(int x)
+{
+  int y;
+  asm("TEST0 out:%0 in:%1" : "=r"(y) : "r"(x) : "cc"
+#if defined(__i386__)
+      , "eax", "edx", "ecx"
+#elif defined(__arm__)
+      , "r0", "r1", "r2"
+#elif defined(__PPC__)
+      , "r3", "r4", "r5"
+#endif
+);
+  return y;
+}
+
+int main()
+{
+  int x;
+  void * y;
+  long long z;
+  double f;
+  char c[16];
+
+  /* No inputs, no outputs */
+  asm("TEST1 %%");
+  /* r inputs */
+  asm("TEST2 in:%0" : : "r" (x));
+  asm("TEST3 in:%0,%1" : : "r" (x), "r" (f));
+  /* r output */
+  asm("TEST4 out:%0" : "=r" (x));
+  /* r inputs and outputs */
+  asm("TEST5 out:%0 in:%1" : "=r" (f) : "r" (y));
+  /* m inputs */
+  asm("TEST6 in:%0" : : "m" (c[2]));
+  asm("TEST7 out:%0 in:%1,%2" : "=r"(x) : "m" (c[0]), "r" (y));
+  /* m output */
+  asm("TEST8 out:%0 in:%1" : "=m" (c[4]) : "r" (f));
+  /* i input */
+  asm("TEST9 in:%0,%1,%2" : : "r"(x), "i"(sizeof(x) + 2), "r"(y));
+#ifdef FAILURES
+  asm("FAIL1 in:%0" : : "i"(x));
+#endif
+  /* 64-bit output */
+  asm("TEST10 out: high %R0,lo %Q0" : "=r" (z));
+  /* 64-bit input */
+  asm("TEST11 out:%0 in:%1,high %R2,lo %Q2,%3" 
+      : "=r"(x) : "r"(y), "r"(z), "r"(f));
+#ifdef FAILURES
+  asm("FAIL2 out:%0" : "=r"(z));
+  asm("FAIL3 in:%0" : : "r"(z));
+#endif
+  /* Named arguments */
+  asm("TEST12 a:%[a] b:%[b] c:%[c]" : : [a]"i"(12), [b]"i"(34), [c]"i"(56));
+  asm("TEST13 a:%[a] x:%[x]" : [x]"=r"(x) : [a]"i"(78));
+  asm("TEST14 a:%[a] in2:%1 c:%[c]" : : [a]"i"(12), "i"(34), [c]"i"(56));
+#ifdef FAILURES
+  asm("FAIL4 a:%[a]" : "=r"(x) : [z]"i"(0));
+#endif
+  /* Various failures */
+#ifdef FAILURES
+  asm("FAIL5 out:%0,%1" : "=r"(x), "=r"(y));
+  asm("FAIL6 in:%0" : : "g"(x));
+  asm("FAIL7 out:%0" : "=r" (x+1));
+#endif
+  return 0;
+}
+