val print_nonmodified_input
      (n: nat)
      (of_arg: (reg_nat n -> reg_64))
      (regs_mod reserved_regs: (reg_64 -> bool))
      (a: td)
      (i: nat{i < n})
      (reg_names: (reg_64 -> string))
      (counter: nat)
      (arg_names: (nat -> string))
    : list string & (reg_64 -> string) & nat
let print_nonmodified_input
  (n:nat) (of_arg:reg_nat n -> reg_64) (regs_mod:reg_64 -> bool) (reserved_regs:reg_64 -> bool)
  (a:td) (i:nat{i < n}) (reg_names:reg_64 -> string) (counter:nat) (arg_names:nat -> string) : list string & (reg_64 -> string) & nat =
   if regs_mod (of_arg i) then ([], reg_names, counter) else
     (["\"r\" (" ^ arg_names i ^ (if reserved_regs (of_arg i) then "_r)" else  ")")],
     (fun r -> if r = of_arg i && not (reserved_regs r) then string_of_int counter else reg_names r),
     counter + 1)
val print_nonmodified_input
      (n: nat)
      (of_arg: (reg_nat n -> reg_64))
      (regs_mod reserved_regs: (reg_64 -> bool))
      (a: td)
      (i: nat{i < n})
      (reg_names: (reg_64 -> string))
      (counter: nat)
      (arg_names: (nat -> string))
    : list string & (reg_64 -> string) & nat
let print_nonmodified_input
      (n: nat)
      (of_arg: (reg_nat n -> reg_64))
      (regs_mod reserved_regs: (reg_64 -> bool))
      (a: td)
      (i: nat{i < n})
      (reg_names: (reg_64 -> string))
      (counter: nat)
      (arg_names: (nat -> string))
    : list string & (reg_64 -> string) & nat =
if regs_mod (of_arg i)
then ([], reg_names, counter)
else
  (["\"r\" (" ^ arg_names i ^ (if reserved_regs (of_arg i) then "_r)" else ")")],
    (fun r -> if r = of_arg i && not (reserved_regs r) then string_of_int counter else reg_names r),
    counter + 1)
Vale.X64.Print_Inline_s.fst.checked
Vale.X64.Print_s.fst.checked Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Instruction_s.fsti.checked Vale.X64.Bytes_Code_s.fst.checked Vale.Interop.X64.fsti.checked Vale.Interop.Base.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.IO.fst.checked FStar.All.fst.checked
Vale.X64.Print_Inline_s.fst
Prims.nat Vale.Interop.X64.reg_nat Vale.X64.Machine_s.reg_64 Prims.bool Vale.Interop.Base.td Prims.b2t Prims.op_LessThan Prims.string FStar.Pervasives.Native.Mktuple3 Prims.list Prims.Nil Prims.Cons Prims.op_Hat Prims.op_AmpAmp Prims.op_Equality Prims.op_Negation Prims.string_of_int Prims.op_Addition FStar.Pervasives.Native.tuple3
module Vale.X64.Print_Inline_s

open FStar.Mul
open FStar.List.Tot
open Vale.X64.Machine_s
open Vale.X64.Bytes_Code_s
open Vale.X64.Machine_Semantics_s
open Vale.X64.Instruction_s
open FStar.IO
open Vale.Interop.Base
open Vale.Interop.X64
module P = Vale.X64.Print_s

let print_rettype (ret_val:option string) = match ret_val with
  | None -> "void"
  | Some _ -> "uint64_t"

let print_basetype (t:base_typ) = match t with
  | TUInt8 -> "uint8_t"
  | TUInt16 -> "uint16_t"
  | TUInt32 -> "uint32_t"
  | TUInt64 -> "uint64_t"
  | TUInt128 -> "ERROR"

// Returns "uint8_t arg2" or "uint64_t* arg0" for instance
let print_arg (a:td) (i:nat) (names:nat -> string) = match a with
  | TD_Base src -> print_basetype src ^ " " ^ names i
  | TD_Buffer src _ _ | TD_ImmBuffer src _ _ -> print_basetype src ^ " *" ^ names i

// Prints a list of args with their types, separated by a comma
let rec print_args (args:list td) (i:nat) (names:nat -> string) = match args with
  | [] -> ""
  | [a] -> print_arg a i names
  | a::q -> print_arg a i names ^ ", " ^ print_args q (i+1) names

let rec build_reserved_args_outs (l:list instr_out) (reserved:reg_64 -> bool)
  : Tot (reg_64 -> bool)
  (decreases l) =
  fun r ->
  match l with
  | [] -> reserved r
  | hd::tl ->
    let (_, op) = hd in
    let reserved : (reg_64 -> bool) = (fun r ->
      match op with
      | IOpIm (IOp64One (OReg reg)) ->
          // Implicit register, adding it to "reserved" registers
          if r = reg then true else reserved r
      | _ -> reserved r)
    in build_reserved_args_outs tl reserved r

let rec build_reserved_args_ins (l:list instr_operand) (reserved:reg_64 -> bool)
  : Tot (reg_64 -> bool)
  (decreases l) =
  fun r ->
  match l with
  | [] -> reserved r
  | hd::tl ->
    let reserved : (reg_64 -> bool) = (fun r ->
      match hd with
      | IOpIm (IOp64One (OReg reg)) ->
          // Implicit register, adding it to "reserved" registers
          if r = reg then true else reserved r
      | _ -> reserved r)
    in build_reserved_args_ins tl reserved r

// Traverses code, looking for instructions implicitly using registers.
// When found, mark such registers as reserved so that they are not used during implicit allocation
let rec build_reserved_args (c:code) (reserved:reg_64 -> bool)
  : Tot (reg_64 -> bool)
  (decreases c) =
  fun r ->
   (match c with
  | Ins ins ->  begin
      match ins with
      | Instr i _ _ ->
          let reserved = build_reserved_args_outs i.outs reserved in
          let reserved = build_reserved_args_ins (InstrTypeRecord?.args i) reserved in
          reserved r
      | _ -> reserved r
    end
  | Block l ->  (build_reserved_args_block l reserved) r
  | IfElse cond ifTrue ifFalse ->
      let reservedT = build_reserved_args ifTrue reserved in
      build_reserved_args ifFalse reservedT r
  | While cond body -> build_reserved_args body reserved r
)

and build_reserved_args_block (l:list code) (reserved:reg_64 -> bool)
  : Tot (reg_64 -> bool)
  (decreases l) =
  fun r -> (
  match l with
  | [] -> reserved r
  | hd::tl ->
    let reserved = build_reserved_args hd reserved in
    build_reserved_args_block tl reserved r
  )

// Prints `"=&r" (name)` if an output is specified
let print_output_ret ret_val (reg_names:reg_64 -> string) (counter:nat) : list string & (reg_64 -> string) & nat
  = match ret_val with
  | None -> [], reg_names, counter
  | Some name -> (["\"=&r\" (" ^ name ^ ")"],
      // If r = rax then address it as current arg number
      (fun r -> if r = 0 then string_of_int counter else reg_names r),
      counter + 1)

// If the register in which a is passed is modified, we should specify `"+&r" (name)`
let print_modified_input
  (n:nat) (a:td) (i:nat{i < n}) (of_arg:reg_nat n -> reg_64) (regs_mod:reg_64 -> bool) (reserved_regs:reg_64 -> bool)
  (reg_names:reg_64 -> string) (counter:nat) (arg_names:nat -> string) : list string & (reg_64 -> string) & nat =
   if regs_mod (of_arg i) then
    (["\"+&r\" (" ^ arg_names i ^ (if reserved_regs (of_arg i) then "_r)" else ")")],
     (fun r -> if r = of_arg i && not (reserved_regs r) then string_of_int counter else reg_names r),
     counter + 1
     ) else ([], reg_names, counter)

// Get a list of strings corresponding to modified inputs
let rec get_modified_input_strings
  (n:nat) (of_arg:reg_nat n -> reg_64) (regs_mod:reg_64 -> bool) (reserved_regs:reg_64 -> bool)
  (args:list td) (i:nat{i + List.Tot.length args <= n}) (ret_val:option string)
  (reg_names:reg_64 -> string) (counter:nat) (arg_names:nat -> string) : list string & (reg_64 -> string) & nat
  = match args with
  | [] -> print_output_ret ret_val reg_names counter
  | a::q ->
      let output, reg_names, counter = print_modified_input n a i of_arg regs_mod reserved_regs reg_names counter arg_names in
      let outputs, reg_names, counter = get_modified_input_strings n of_arg regs_mod reserved_regs q (i+1) ret_val reg_names counter arg_names in
      output @ outputs, reg_names, counter

// Print the list of modified inputs, separated by commas
let print_modified_inputs
  (n:nat)
  (of_arg:reg_nat n -> reg_64)
  (regs_mod:reg_64 -> bool)
  (reserved_regs:reg_64 -> bool)
  (args:list td{List.Tot.length args <= n})
  (ret_val:option string)
  (reg_names:reg_64 -> string)
  (counter:nat)
  (arg_names:nat -> string) =
  let rec aux = function
  | [] -> "\n"
  | [a] -> a ^ "\n"
  | a :: q -> a ^ ", " ^ aux q
  in
  let outputs, output_reg_names, output_nbr = get_modified_input_strings n of_arg regs_mod reserved_regs args 0 ret_val reg_names counter arg_names in
  aux outputs, output_reg_names, output_nbr

// If the register in which an arg is passed is not modified, we should specify it as `"r" (name)`
let print_nonmodified_input
  (n:nat) (of_arg:reg_nat n -> reg_64) (regs_mod:reg_64 -> bool) (reserved_regs:reg_64 -> bool)
val print_nonmodified_input
      (n: nat)
      (of_arg: (reg_nat n -> reg_64))
      (regs_mod reserved_regs: (reg_64 -> bool))
      (a: td)
      (i: nat{i < n})
      (reg_names: (reg_64 -> string))
      (counter: nat)
      (arg_names: (nat -> string))
    : list string & (reg_64 -> string) & nat

    n: Prims.nat ->
    of_arg: (_: Vale.Interop.X64.reg_nat n -> Vale.X64.Machine_s.reg_64) ->
    regs_mod: (_: Vale.X64.Machine_s.reg_64 -> Prims.bool) ->
    reserved_regs: (_: Vale.X64.Machine_s.reg_64 -> Prims.bool) ->
    a: Vale.Interop.Base.td ->
    i: Prims.nat{i < n} ->
    reg_names: (_: Vale.X64.Machine_s.reg_64 -> Prims.string) ->
    counter: Prims.nat ->
    arg_names: (_: Prims.nat -> Prims.string)
  -> (Prims.list Prims.string * (_: Vale.X64.Machine_s.reg_64 -> Prims.string)) * Prims.nat