From 426881cde464691b61c5c49cf5038d21aace75fe Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 21 Apr 2015 10:21:06 +0200 Subject: Support for GCC-style extended asm, continued: - support "r", "m" and "i" constraints - support "%Q" and "%R" modifiers for register pairs - support register clobbers - split off analysis and transformation of asm statements in cparser/ExtendedAsm.ml --- cparser/ExtendedAsm.ml | 183 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 183 insertions(+) create mode 100644 cparser/ExtendedAsm.ml (limited to 'cparser/ExtendedAsm.ml') diff --git a/cparser/ExtendedAsm.ml b/cparser/ExtendedAsm.ml new file mode 100644 index 00000000..4cd5fc21 --- /dev/null +++ b/cparser/ExtendedAsm.ml @@ -0,0 +1,183 @@ +(* *********************************************************************) +(* *) +(* 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" *) + +let rec transf_inputs loc env accu pos pos' subst = function + | [] -> + (List.rev accu, subst) + | (lbl, cstr, e) :: inputs -> + match cstr with + | "r" -> + 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 + | "m" -> + transf_inputs loc env (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 "%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 + | _ -> + 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 + +(* Transform the output operands: + - outputs of kind "=m" become an input (equal to the address of the output) +*) + +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; + begin match cstr with + | "=r" -> + 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) + | "=m" -> + (None, [eaddrof e], + set_label_mem lbl 0 0 StringMap.empty, 1, 1) + | _ -> + error "%aUnsupported feature: asm result of kind '%s'" + formatloc loc cstr; + (None, [], set_label_reg lbl 0 0 StringMap.empty, 1, 1) + end + | _ -> + error "%aUnsupported feature: asm statement with 2 or more outputs" + formatloc loc; + (None, [], StringMap.empty, 0, 0) + +(* 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; + "%" + 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') -- cgit