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.

Author: xavierleroy

.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

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

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...  *)
           | _ ->

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
 

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

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;

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) ->

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
 

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:

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)
 

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.
 

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:

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

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