(* *********************************************************************)
(*                                                                     *)
(*              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 "%%R%d" pos')
    (StringMap.add (name_of_label ~modifier:"Q" lbl pos) (sprintf "%%Q%d" pos')
       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' + 1)
                      (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, 1)
        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 ->
      let c' = String.uppercase c in
      if Machregsaux.register_by_name c' <> None
      || List.mem c' Machregsaux.scratch_register_names
      || 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')