diff options
Diffstat (limited to 'cparser/ExtendedAsm.ml')
-rw-r--r-- | cparser/ExtendedAsm.ml | 198 |
1 files changed, 198 insertions, 0 deletions
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') |