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

2 files changed, 101 insertions, 10 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index fd10efb4..7413c443 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -831,6 +831,97 @@ and convertExprList env el =
   | [] -> Enil
   | e1 :: el' -> Econs(convertExpr env e1, convertExprList env el')
 
+(** ** Extended assembly *)
+
+module StringMap = Map.Make(String)
+
+let re_asm_placeholder =
+  Str.regexp "\\(%[0-9]+\\|%\\[[a-zA-Z_][a-zA-Z_0-9]*\\]\\|%%\\)"
+
+let convertAsm env txt outputs inputs clobber =
+
+  (* On the fly renaming of labeled and numbered arguments *)
+  let name_of_label lbl pos =
+    match lbl with
+    | None   -> sprintf "%%%d" pos
+    | Some l -> sprintf "%%[%s]" l in
+  let set_label_reg lbl pos pos' subst =
+    StringMap.add (name_of_label lbl pos) (sprintf "%%%d" pos') subst
+  and set_label_mem lbl pos pos' subst =
+    StringMap.add (name_of_label lbl pos)
+                  (CBuiltins.asm_mem_argument (sprintf "%%%d" pos'))
+                  subst
+  and set_label_const lbl pos n subst =
+    StringMap.add (name_of_label lbl pos) (sprintf "%Ld" n) subst in
+
+  (* Fix up the input expressions:
+      - add "&" for inputs of kind "m"
+      - evaluate constants for inputs of kind "i" *)
+  let rec fixupInputs accu pos pos' subst = function
+  | [] ->
+      (List.rev accu, subst)
+  | (lbl, cstr, e) :: inputs ->
+      match cstr with
+      | "r" | "rm" ->
+        fixupInputs (e :: accu) (pos + 1) (pos' + 1)
+                    (set_label_reg lbl pos pos' subst) inputs
+      | "m" | "o" ->
+        fixupInputs (Cutil.eaddrof e :: accu) (pos + 1) (pos' + 1)
+                    (set_label_mem lbl pos pos' subst) inputs
+      | "i" | "n" ->
+        let n =
+          match Ceval.integer_expr env e with
+          | Some n -> n
+          | None -> error "asm argument of kind 'i'/'n' is not a constant"; 0L in
+        fixupInputs accu (pos + 1) pos'
+                    (set_label_const lbl pos n subst) inputs
+      | _ ->
+        unsupported ("asm argument of kind '" ^ cstr ^ "'");
+        ([], subst) in
+  
+  (* Check the output expressions *)
+  let (output', ty_res, (inputs', subst)) =
+    match outputs with
+    | [] ->
+        (None, TVoid [], fixupInputs [] 0 0 StringMap.empty inputs)
+    | [(lbl, cstr, e)] ->
+        if not (cstr = "=r" || cstr = "=rm") then
+          unsupported ("asm result of kind '" ^ cstr ^ "'");
+        (Some e, e.etyp,
+         fixupInputs [] 1 1 (set_label_reg lbl 0 0 StringMap.empty) inputs)
+    | _ ->
+        error "asm statement with 2 or more results";
+        (None, TVoid [], ([], StringMap.empty)) in
+
+  (* Check the clobber list *)
+  List.iter
+    (fun c ->
+      if not (c = "memory" || c = "cc") then
+        unsupported ("asm register clobber '" ^ c ^ "'"))
+    clobber;
+
+  (* Rename the %[ident] and %nnn placeholders in the asm text *)
+  let txt' =
+    Str.global_substitute re_asm_placeholder 
+      (fun txt -> let s = Str.matched_group 1 txt in
+                  try StringMap.find s subst with Not_found -> s)
+      txt 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),
+             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 =
@@ -940,11 +1031,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 env txt outputs inputs clobber))
 
 and convertSwitch ploc env is_64 = function
   | [] ->
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 7c00ab47..487c0df6 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 => do_inline_assembly text sg ge
   end.
 
 Lemma do_ef_external_sound: